test/regress/regress1/strings/cmu-prereg-fmf.smt2


1
2
3
4
5
6
7
8
9
10
11
12

; COMMAND-LINE: --strings-exp --strings-fmf
; EXPECT: sat
(set-logic ALL_SUPPORTED)
(set-info :status sat)

(declare-fun url () String)

(assert (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (not (not (= (ite (str.contains (str.++ (str.replace (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) 0 (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) "K" "k") (str.++ (str.replace (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) 0 (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) "K" "k") (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1))))) "Y") 1 0) 0)))) (not (not (= (ite (str.contains (str.++ (str.replace (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) 0 (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) "K" "k") (str.++ (str.replace (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) 0 (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) "K" "k") (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1))))) "X") 1 0) 0)))) (not (not (= (ite (str.contains (str.++ (str.replace (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) 0 (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) "K" "k") (str.++ (str.replace (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) 0 (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) "K" "k") (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1))))) "W") 1 0) 0)))) (not (not (= (ite (str.contains (str.++ (str.replace (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) 0 (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) "K" "k") (str.++ (str.replace (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) 0 (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) "K" "k") (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1))))) "V") 1 0) 0)))) (not (not (= (ite (str.contains (str.++ (str.replace (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) 0 (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) "K" "k") (str.++ (str.replace (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) 0 (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) "K" "k") (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1))))) "U") 1 0) 0)))) (not (not (= (ite (str.contains (str.++ (str.replace (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) 0 (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) "K" "k") (str.++ (str.replace (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) 0 (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) "K" "k") (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1))))) "T") 1 0) 0)))) (not (not (= (ite (str.contains (str.++ (str.replace (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) 0 (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) "K" "k") (str.++ (str.replace (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) 0 (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) "K" "k") (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1))))) "S") 1 0) 0)))) (not (not (= (ite (str.contains (str.++ (str.replace (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) 0 (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) "K" "k") (str.++ (str.replace (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) 0 (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) "K" "k") (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1))))) "R") 1 0) 0)))) (not (not (= (ite (str.contains (str.++ (str.replace (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) 0 (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) "K" "k") (str.++ (str.replace (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) 0 (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) "K" "k") (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1))))) "Q") 1 0) 0)))) (not (not (= (ite (str.contains (str.++ (str.replace (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) 0 (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) "K" "k") (str.++ (str.replace (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) 0 (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) "K" "k") (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1))))) "P") 1 0) 0)))) (not (not (= (ite (str.contains (str.++ (str.replace (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) 0 (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) "K" "k") (str.++ (str.replace (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) 0 (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) "K" "k") (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1))))) "O") 1 0) 0)))) (not (not (= (ite (str.contains (str.++ (str.replace (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) 0 (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) "K" "k") (str.++ (str.replace (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) 0 (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) "K" "k") (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1))))) "N") 1 0) 0)))) (not (not (= (ite (str.contains (str.++ (str.replace (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) 0 (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) "K" "k") (str.++ (str.replace (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) 0 (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) "K" "k") (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1))))) "M") 1 0) 0)))) (not (not (= (ite (str.contains (str.++ (str.replace (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) 0 (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) "K" "k") (str.++ (str.replace (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) 0 (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) "K" "k") (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1))))) "L") 1 0) 0)))) (not (not (= (ite (str.contains (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1))) "K") 1 0) 0)))) (not (= (ite (str.contains (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K") 1 0) 0))) (not (= (ite (str.contains (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K") 1 0) 0))) (not (not (= (ite (str.contains (str.substr url 0 (- (str.indexof url ":" 0) 0)) "J") 1 0) 0)))) (not (not (= (ite (str.contains (str.substr url 0 (- (str.indexof url ":" 0) 0)) "I") 1 0) 0)))) (not (not (= (ite (str.contains (str.substr url 0 (- (str.indexof url ":" 0) 0)) "H") 1 0) 0)))) (not (not (= (ite (str.contains (str.substr url 0 (- (str.indexof url ":" 0) 0)) "G") 1 0) 0)))) (not (not (= (ite (str.contains (str.substr url 0 (- (str.indexof url ":" 0) 0)) "F") 1 0) 0)))) (not (not (= (ite (str.contains (str.substr url 0 (- (str.indexof url ":" 0) 0)) "E") 1 0) 0)))) (not (not (= (ite (str.contains (str.substr url 0 (- (str.indexof url ":" 0) 0)) "D") 1 0) 0)))) (not (not (= (ite (str.contains (str.substr url 0 (- (str.indexof url ":" 0) 0)) "C") 1 0) 0)))) (not (not (= (ite (str.contains (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B") 1 0) 0)))) (not (not (= (ite (str.contains (str.substr url 0 (- (str.indexof url ":" 0) 0)) "A") 1 0) 0)))) (not (not (= (ite (not (= (str.len (str.substr url (+ (str.indexof url ":" 0) 1) (- (str.len url) (+ (str.indexof url ":" 0) 1)))) 0)) 1 0) 0)))) (not (not (= (ite (= (str.substr url 0 (- (str.indexof url ":" 0) 0)) "http") 1 0) 0)))) (not (= (ite (> (str.indexof url ":" 0) 0) 1 0) 0))) (not (= (ite (not (= (str.len url) 0)) 1 0) 0))) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) (>= (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) (>= (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) (>= (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) (>= (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) (>= (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) (>= (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) (>= (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) (>= (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) (>= (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) (>= (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) (>= (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) (>= (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) (>= (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) (>= (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) (>= (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof url ":" 0) 1) 0)) (>= (- (str.len url) (+ (str.indexof url ":" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)))

(check-sat)

;(get-value (url))