diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-24 09:56:12 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-24 09:56:12 -0500 |
commit | 3ea52a752bf9f67c294521ab0fe4d831c8d7f4dc (patch) | |
tree | e7ffbab65c9ffa4f65ec2bb8a9f8ba33d6222e59 /test/regress/regress1/strings | |
parent | 67ea40d24cbbcd3f490248754a6abc1989bacc7b (diff) |
Add some regressions. Minor.
Diffstat (limited to 'test/regress/regress1/strings')
-rw-r--r-- | test/regress/regress1/strings/Makefile.am | 4 | ||||
-rw-r--r-- | test/regress/regress1/strings/cmu-prereg-fmf.smt2 | 12 | ||||
-rw-r--r-- | test/regress/regress1/strings/cmu-repl-len-nterm.smt2 | 12 |
3 files changed, 27 insertions, 1 deletions
diff --git a/test/regress/regress1/strings/Makefile.am b/test/regress/regress1/strings/Makefile.am index 7830f14f1..716e664b1 100644 --- a/test/regress/regress1/strings/Makefile.am +++ b/test/regress/regress1/strings/Makefile.am @@ -18,7 +18,9 @@ endif # put it below in "TESTS +=" TESTS = \ cmu-5042-0707-2.smt2 \ - cmu-dis-0707-3.smt2 + cmu-dis-0707-3.smt2 \ + cmu-prereg-fmf.smt2 \ + cmu-repl-len-nterm.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress1/strings/cmu-prereg-fmf.smt2 b/test/regress/regress1/strings/cmu-prereg-fmf.smt2 new file mode 100644 index 000000000..0d6827cf7 --- /dev/null +++ b/test/regress/regress1/strings/cmu-prereg-fmf.smt2 @@ -0,0 +1,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)) diff --git a/test/regress/regress1/strings/cmu-repl-len-nterm.smt2 b/test/regress/regress1/strings/cmu-repl-len-nterm.smt2 new file mode 100644 index 000000000..004db77ed --- /dev/null +++ b/test/regress/regress1/strings/cmu-repl-len-nterm.smt2 @@ -0,0 +1,12 @@ +; COMMAND-LINE: --strings-exp +; 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 (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)) "B" 0) 1) 0)) "B" "b") (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)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 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)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1))) "B" 0) 1) 0)) "B" "b") (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 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)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1))) "B" 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)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 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)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1))) "B" 0) 1))))) "C") 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)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 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)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1))) "B" 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)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 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)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1))) "B" 0) 1))) "B") 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)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1))) "B") 1 0) 0))) (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))) (>= 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)) "B" 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)) "B" 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)) "B" 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)) "B" 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)) "B" 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)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1))) "B" 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)) "B" 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)) "B" 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)) "B" 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)) "B" 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)) "B" 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)) "B" 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)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1))) "B" 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)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 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)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1))) "B" 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)) "B" 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)) "B" 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)) "B" 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)) "B" 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)) "B" 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)) "B" 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)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1))) "B" 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)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 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)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1))) "B" 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)) "B" 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)) "B" 0) 1)) 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)) |