(set-option :smt.arith.propagate_eqs false)
(set-option :rewriter.elim_and true)
(set-option :rewriter.local_ctx true)
(set-option :rewriter.sort_sums true)
(set-option :smt.threads 4)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const i1 Int)
(declare-const i4 Int)
(declare-const i5 Int)
(declare-const i6 Int)
(declare-const Str0 String)
(declare-const Str1 String)
(declare-const Str2 String)
(declare-const Str3 String)
(declare-const Str4 String)
(declare-const Str5 String)
(declare-const Str6 String)
(declare-const Str7 String)
(declare-const Str8 String)
(declare-const Str9 String)
(declare-const Str10 String)
(declare-const Str11 String)
(declare-const Str12 String)
(declare-const Str13 String)
(declare-const Str14 String)
(declare-const Str15 String)
(declare-const Str16 String)
(declare-const Str17 String)
(declare-const Str18 String)
(declare-const Str19 String)
(declare-const v10 Bool)
(declare-const v16 Bool)
(assert (>= (str.len Str15) i4))
(declare-const v17 Bool)
(declare-const v18 Bool)
(assert (>= (str.len Str5) (- i1)))
(declare-const v19 Bool)
(declare-const v20 Bool)
(assert (>= (str.len Str15) 0))
(declare-const v24 Bool)
(declare-const v25 Bool)
(declare-const v26 Bool)
(declare-const i10 Int)
(push 1)
(declare-const i11 Int)
(assert (>= (str.len (str.++ Str5 Str17)) 999))
(declare-const v27 Bool)
(declare-const i12 Int)
(declare-const v29 Bool)
(declare-const i13 Int)
(declare-const v30 Bool)
(assert (>= 0 0))
(declare-const v31 Bool)
(assert (or v7 v7 (str.<= Str17 (str.++ Str5 Str17))))
(assert (or (or v27 v10 v30 v6 (<= 932 i5) v5 (not v7) v29 (=> v4 v9) (= (abs 37) 999) (>= i1 98)) v4 (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5))))
(assert (or (or v27 v10 v30 v6 (<= 932 i5) v5 (not v7) v29 (=> v4 v9) (= (abs 37) 999) (>= i1 98)) (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5)) v0))
(assert (or v9 v4 v3))
(assert (or (= (abs 37) 999) (or v27 v10 v30 v6 (<= 932 i5) v5 (not v7) v29 (=> v4 v9) (= (abs 37) 999) (>= i1 98)) v3))
(assert (or v4 v26 v9))
(assert (or (<= 50 i1) (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16) v24))
(assert (or v9 v5 v1))
(assert (or v24 (<= 50 i1) v9))
(assert (or v24 v0 (or v6 (<= i4 i1 i5 i5) (<= 50 i1))))
(assert (or v2 v29 v4))
(assert (or v5 (or v27 v10 v30 v6 (<= 932 i5) v5 (not v7) v29 (=> v4 v9) (= (abs 37) 999) (>= i1 98)) v29))
(assert (or (or v27 v10 v30 v6 (<= 932 i5) v5 (not v7) v29 (=> v4 v9) (= (abs 37) 999) (>= i1 98)) (<= 50 i1) v0))
(assert (or v2 (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5)) (str.<= Str17 (str.++ Str5 Str17))))
(assert (or v26 v3 v24))
(assert (or (<= 50 i1) v5 (<= 50 i1)))
(assert (or v9 v2 (not v7)))
(assert (or v2 v3 v9))
(assert (or (or v27 v10 v30 v6 (<= 932 i5) v5 (not v7) v29 (=> v4 v9) (= (abs 37) 999) (>= i1 98)) (or v27 v10 v30 v6 (<= 932 i5) v5 (not v7) v29 (=> v4 v9) (= (abs 37) 999) (>= i1 98)) (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5))))
(assert (or v7 v26 (not v7)))
(assert (or v9 v4 v9))
(assert (or (or v27 v10 v30 v6 (<= 932 i5) v5 (not v7) v29 (=> v4 v9) (= (abs 37) 999) (>= i1 98)) (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16) v2))
(assert (or v1 (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5)) (not v30)))
(assert (or (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5)) v5 v2))
(assert (or v7 (str.<= Str17 (str.++ Str5 Str17)) v2))
(assert (or (not v7) (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16) (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16)))
(assert (or v26 (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16) v3))
(assert (or v29 v9 v9))
(assert (or (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16) (str.<= Str17 (str.++ Str5 Str17)) v7))
(assert (or v7 (= 0 999) (not v30)))
(assert (or (str.<= Str17 "") v4 (= 0 999)))
(assert (or v5 (not v30) (<= 50 i1)))
(assert (or (or v27 v10 v30 v6 (<= 932 i5) v5 (not v7) v29 (=> v4 v9) (= (abs 37) 999) (>= i1 98)) v5 v4))
(assert (or v3 v5 (str.<= Str17 (str.++ Str5 Str17))))
(assert (or (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5)) v1 (= (abs 37) 999)))
(assert (or v26 v4 (or v6 (<= i4 i1 i5 i5) (<= 50 i1))))
(assert (or (= (abs 37) 999) (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16) v9))
(assert (or (str.<= Str17 (str.++ Str5 Str17)) (not v7) (<= 50 i1)))
(assert (or v4 (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16) v24))
(assert (or v9 v24 v2))
(assert (or v5 v3 (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16)))
(assert (or v24 v24 (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16)))
(assert (or (<= 50 i1) (str.<= Str17 (str.++ Str5 Str17)) (= (abs 37) 999)))
(assert (or (= (abs 37) 999) (or v6 (<= i4 i1 i5 i5) (<= 50 i1)) v5))
(assert (or v3 (str.<= Str17 (str.++ Str5 Str17)) (str.<= Str17 (str.++ Str5 Str17))))
(assert (or v1 v0 v5))
(assert (or (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16) (not v7) v29))
(assert (or v29 (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5)) v3))
(assert (or (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16) v2 v7))
(assert (or v1 v0 v2))
(assert (or (= (abs 37) 999) v1 v1))
(assert (or (or v6 (<= i4 i1 i5 i5) (<= 50 i1)) v24 (<= 50 i1)))
(assert (or (or v6 (<= i4 i1 i5 i5) (<= 50 i1)) (not v30) v3))
(assert (or v26 (<= 50 i1) v1))
(assert (or (= (abs 37) 999) v24 v7))
(assert (or v1 v9 (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5))))
(assert (or (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5)) v7 (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5))))
(assert (or (or v6 (<= i4 i1 i5 i5) (<= 50 i1)) v29 (or v6 (<= i4 i1 i5 i5) (<= 50 i1))))
(assert (or (<= 50 i1) (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16) (= (abs 37) 999)))
(assert (or (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5)) v26 v9))
(assert (or (or v27 v10 v30 v6 (<= 932 i5) v5 (not v7) v29 (=> v4 v9) (= 0 999) (>= i1 98)) v9 (<= 50 i1)))
(assert (or v7 v7 v4))
(assert (or (= (abs 37) 999) v26 v9))
(assert (or (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5)) (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16) v29))
(assert (or (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16) (= (abs 37) 999) v1))
(assert (or v0 v0 v0))
(assert (or v1 (= (abs 37) 999) (<= 50 i1)))
(assert (or v29 (not v30) v9))
(assert (or v2 (not v7) (<= 50 i1)))
(assert (or (= 0 999) v26 v3))
(assert (or (or v6 (<= i4 i1 i5 i5) (<= 50 i1)) v24 v26))
(assert (or v4 v29 (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5))))
(assert (or v24 v3 v5))
(assert (or (or v6 (<= i4 i1 i5 i5) (<= 50 i1)) v7 (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5))))
(assert (or v1 v3 v0))
(assert (or v1 v1 (not v7)))
(assert (or v9 (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5)) v4))
(assert (or v26 v3 (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5))))
(assert (or (not v7) v7 (not v7)))
(assert (or v0 (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16) v3))
(assert (or (or v6 (<= i4 i1 i5 i5) (<= 50 i1)) v26 v26))
(assert (or v1 v9 (str.<= Str17 (str.++ Str5 Str17))))
(assert (or v2 v29 v0))
(assert (or (= (abs 37) 999) v3 v2))
(assert (or v1 v2 (not v7)))
(assert (or (or v6 (<= i4 i1 i5 i5) (<= 50 i1)) (= (abs 37) 999) (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16)))
(assert (or v0 v4 v5))
(assert (or (not v7) (not v7) v2))
(assert (or (= (abs 37) 999) v9 v29))
(assert (or (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16) v4 (not v7)))
(assert (or (or v6 (<= i4 i1 i5 i5) (<= 50 i1)) v1 (or v27 v10 v30 v6 (<= 932 i5) v5 (not v7) v29 (=> v4 v9) (= (abs 37) 999) (>= i1 98))))
(assert (or v7 v2 v1))
(assert (or (= (abs 37) 999) v5 (not v30)))
(assert (or (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5)) v1 v29))
(assert (or v3 v4 (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5))))
(assert (or (str.<= Str17 (str.++ Str5 Str17)) (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16) (or v6 (<= i4 i1 i5 i5) (<= 50 i1))))
(assert (or (not v30) (not v7) v24))
(assert (or v0 v3 v4))
(assert (or v26 v26 (<= 50 i1)))
(assert (or (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5)) (= 0 999) v3))
(assert (or v5 (<= 50 i1) v3))
(assert (or v9 (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5)) v0))
(assert (or (str.<= Str17 (str.++ Str5 Str17)) (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5)) (or v6 (<= i4 i1 i5 i5) (<= 50 i1))))
(assert (or v4 v3 (= (abs 37) 999)))
(assert (or v5 v4 v0))
(assert (or v7 v29 v2))
(assert (or (str.<= Str17 (str.++ Str5 Str17)) (<= 50 i1) v3))
(assert (or v3 v7 (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5))))
(assert (or (or v6 (<= i4 i1 i5 i5) (<= 50 i1)) v7 v1))
(assert (or v24 (or v27 v10 v30 v6 (<= 932 i5) v5 (not v7) v29 (=> v4 v9) (= 0 999) (>= i1 98)) v0))
(assert (or (str.<= Str17 "") (or v27 v10 v30 v6 (<= 932 i5) v5 (not v7) v29 (=> v4 v9) (= (abs 37) 999) (>= i1 98)) v1))
(assert (or (= (abs 37) 999) v3 v5))
(assert (or v29 v4 (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16)))
(assert (or v29 (not v30) (or v6 (<= i4 i1 i5 i5) (<= 50 i1))))
(assert (or v2 v3 v24))
(assert (or (or v6 (<= i4 i1 i5 i5) (<= 50 i1)) v7 v26))
(assert (or (str.<= Str17 "") v0 v9))
(assert (or v5 v5 v24))
(assert (or v26 v2 (not v30)))
(assert (or (or v27 v10 v30 v6 (<= 932 i5) v5 (not v7) v29 (=> v4 v9) (= (abs 37) 999) (>= i1 98)) v5 (= 0 999)))
(assert (or v1 v26 v2))
(assert (or v1 (<= 50 i1) (not v7)))
(assert (or v26 v24 v3))
(assert (or (<= 50 i1) v0 v2))
(assert (or (not v30) v9 (<= 50 i1)))
(assert (or (or v6 (<= i4 i1 i5 i5) (<= 50 i1)) v24 (= (abs 37) 999)))
(assert (or (<= 50 i1) v4 v9))
(assert (or (str.<= Str17 (str.++ Str5 Str17)) v29 v7))
(assert (or (<= 50 i1) v1 v0))
(assert (or v5 v7 v7))
(assert (or (= (abs 37) 999) (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5)) (not v7)))
(assert (or (or v6 (<= i4 i1 i5 i5) (<= 50 i1)) (or v6 (<= i4 i1 i5 i5) (<= 50 i1)) v7))
(assert (or v2 (<= 50 i1) (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16)))
(assert (or v1 v7 (<= 50 i1)))
(assert (or v5 (or v27 v10 v30 v6 (<= 932 i5) v5 (not v7) v29 (=> v4 v9) (= (abs 37) 999) (>= i1 98)) v0))
(assert (or v2 (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5)) (<= 50 i1)))
(assert (or (str.<= Str17 (str.++ Str5 Str17)) v4 v26))
(assert (or v26 (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5)) (<= 50 i1)))
(assert (or (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5)) v29 (or v6 (<= i4 i1 i5 i5) (<= 50 i1))))
(assert (or (or v6 (<= i4 i1 i5 i5) (<= 50 i1)) (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16) v9))
(assert (or (str.<= Str17 (str.++ Str5 Str17)) v9 (not v30)))
(assert (or (or v27 v10 v30 v6 (<= 932 i5) v5 (not v7) v29 (=> v4 v9) (= 0 999) (>= i1 98)) v26 v3))
(assert (or v9 (not v30) v26))
(assert (or v5 v26 (str.<= Str17 (str.++ Str5 Str17))))
(assert (or (or v6 (<= i4 i1 i5 i5) (<= 50 i1)) v9 (= (abs 37) 999)))
(assert (or (not v30) v7 v9))
(assert (or v5 (str.<= Str17 (str.++ Str5 Str17)) v2))
(assert (or v2 (or v6 (<= i4 i1 i5 i5) (<= 50 i1)) (not v7)))
(assert (or v0 (or v6 (<= i4 i1 i5 i5) (<= 50 i1)) v24))
(assert (or v24 (not v7) v4))
(assert (or (= (abs 37) 999) (or v27 v10 v30 v6 (<= 932 i5) v5 (not v7) v29 (=> v4 v9) (= (abs 37) 999) (>= i1 98)) v26))
(assert (or v5 v5 v5))
(assert (or v1 v26 v2))
(assert (or v4 (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16) v1))
(assert (or v7 (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16) (or v6 (<= i4 i1 i5 i5) (<= 50 i1))))
(assert (or v26 v1 (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5))))
(assert (or v24 v1 (str.<= Str17 (str.++ Str5 Str17))))
(assert (or v2 v4 (or v6 (<= i4 i1 i5 i5) (<= 50 i1))))
(assert (or v5 v29 (<= 50 i1)))
(assert (or (<= 50 i1) v2 v1))
(assert (or v29 (not v30) (or v27 v10 v30 v6 (<= 932 i5) v5 (not v7) v29 (=> v4 v9) (= 0 999) (>= i1 98))))
(assert (or v5 (not v7) (or v27 v10 v30 v6 (<= 932 i5) v5 (not v7) v29 (=> v4 v9) (= (abs 37) 999) (>= i1 98))))
(assert (or (not v7) (str.<= Str17 (str.++ Str5 Str17)) (or v6 (<= i4 i1 i5 i5) (<= 50 i1))))
(assert (or (or v6 (<= i4 i1 i5 i5) (<= 50 i1)) v2 v0))
(assert (or (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5)) v3 v1))
(assert (or v24 v24 v0))
(assert (or (= (abs 37) 999) (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16) (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5))))
(assert (or (or v6 (<= i4 i1 i5 i5) (<= 50 i1)) v0 (or v6 (<= i4 i1 i5 i5) (<= 50 i1))))
(assert (or (<= 50 i1) v26 (= (abs 37) 999)))
(assert (or (not v30) (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5)) v9))
(assert (or v26 v26 v7))
(assert (or v24 v1 (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5))))
(assert (or (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16) (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5)) (not v7)))
(assert (or v2 (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5)) v9))
(assert (or (= (abs 37) 999) v2 v4))
(assert (or v2 (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16) v0))
(assert (or (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5)) (<= 50 i1) v29))
(assert (or (not v7) v9 (<= 50 i1)))
(assert (or v4 (or v27 v10 v30 v6 (<= 932 i5) v5 (not v7) v29 (=> v4 v9) (= (abs 37) 999) (>= i1 98)) v5))
(assert (or (= 0 999) v29 (not v7)))
(assert (or (<= 50 i1) (<= 50 i1) v2))
(assert (or (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16) v26 (not v7)))
(assert (or v3 v5 (str.<= Str17 "")))
(assert (or (= (abs 37) 999) v0 (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5))))
(assert (or v2 v24 v9))
(assert (or v2 (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5)) (or v6 (<= i4 i1 i5 i5) (<= 50 i1))))
(assert (or v4 v1 (not v30)))
(assert (or v5 (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5)) (not v30)))
(assert (or (not v30) (<= 50 i1) v5))
(assert (or (or v27 v10 v30 v6 (<= 932 i5) v5 (not v7) v29 (=> v4 v9) (= (abs 37) 999) (>= i1 98)) v9 v1))
(assert (or (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16) (not v30) v1))
(assert (or v2 (or v27 v10 v30 v6 (<= 932 i5) v5 (not v7) v29 (=> v4 v9) (= (abs 37) 999) (>= i1 98)) (str.<= Str17 (str.++ Str5 Str17))))
(assert (or (not v7) v0 v9))
(assert (or (or v6 (<= i4 i1 i5 i5) (<= 50 i1)) v4 (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16)))
(assert (or (= (abs 37) 999) (<= 50 i1) v29))
(assert (or v3 (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16) (= (abs 37) 999)))
(assert (or (not v7) v4 v5))
(assert (or v26 v5 (= (abs 37) 999)))
(assert (or (<= 50 i1) (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5)) (<= 50 i1)))
(assert (or v2 v4 (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5))))
(assert (or v5 v26 (or v6 (<= i4 i1 i5 i5) (<= 50 i1))))
(assert (or v3 (str.<= Str17 (str.++ Str5 Str17)) v9))
(assert (or v5 (= 0 999) v2))
(assert (or v1 v5 v7))
(assert (or (= (abs 37) 999) (or v27 v10 v30 v6 (<= 932 i5) v5 (not v7) v29 (=> v4 v9) (= (abs 37) 999) (>= i1 98)) v4))
(assert (or v26 (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16) v9))
(assert (or v5 v7 v26))
(assert (or v3 v5 v5))
(assert (or v3 v5 (not v7)))
(assert (or v3 v5 (not v7)))
(assert (or (or v27 v10 v30 v6 (<= 932 i5) v5 (not v7) v29 (=> v4 v9) (= 0 999) (>= i1 98)) (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16) (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5))))
(assert (or v5 v5 v1))
(assert (or (or v27 v10 v30 v6 (<= 932 i5) v5 (not v7) v29 (=> v4 v9) (= (abs 37) 999) (>= i1 98)) v2 v29))
(assert (or v2 v0 (not v30)))
(assert (or v5 (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16) v3))
(assert (or v3 v3 (<= 50 i1)))
(assert (or (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16) v26 v3))
(assert (or v3 (= (abs 37) 999) (= (abs 37) 999)))
(assert (or (= (abs 37) 999) (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16) (or v27 v10 v30 v6 (<= 932 i5) v5 (not v7) v29 (=> v4 v9) (= (abs 37) 999) (>= i1 98))))
(assert (or (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5)) v1 v29))
(assert (or v9 (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5)) v3))
(assert (or (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5)) (<= 50 i1) v24))
(assert (or (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16) (str.<= Str17 (str.++ Str5 Str17)) (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16)))
(assert (or (or v6 (<= i4 i1 i5 i5) (<= 50 i1)) (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16) v3))
(assert (or v3 (<= 50 i1) v3))
(assert (or (not v30) v3 v26))
(assert (or v4 (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5)) (= (abs 37) 999)))
(assert (or (or v27 v10 v30 v6 (<= 932 i5) v5 (not v7) v29 (=> v4 v9) (= (abs 37) 999) (>= i1 98)) (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16) (or v6 (<= i4 i1 i5 i5) (<= 50 i1))))
(assert (or v24 v9 v2))
(assert (or (or v6 (<= i4 i1 i5 i5) (<= 50 i1)) v0 v5))
(assert (or v7 v7 (or v6 (<= i4 i1 i5 i5) (<= 50 i1))))
(assert (or (or v6 (<= i4 i1 i5 i5) (<= 50 i1)) (not v7) v26))
(assert (or v7 v7 (or v6 (<= i4 i1 i5 i5) (<= 50 i1))))
(assert (or v9 (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5)) v5))
(assert (or v1 v3 (<= 50 i1)))
(assert (or v2 (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16) v2))
(assert (or v3 v3 (not v30)))
(assert (or (not v30) (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16) (= (abs 37) 999)))
(assert (or v0 v2 (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16)))
(assert (or (str.<= Str17 (str.++ Str5 Str17)) (or v6 (<= i4 i1 i5 i5) (<= 50 i1)) v4))
(assert (or (= (abs 37) 999) v5 (or v27 v10 v30 v6 (<= 932 i5) v5 (not v7) v29 (=> v4 v9) (= (abs 37) 999) (>= i1 98))))
(assert (or (<= 50 i1) (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5)) (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16)))
(assert (or (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5)) v7 v24))
(assert (or v4 v9 v2))
(assert (or v24 (= (abs 37) 999) v26))
(assert (or (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16) (or v6 (<= i4 i1 i5 i5) (<= 50 i1)) (str.<= Str17 (str.++ Str5 Str17))))
(assert (or v4 (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16) (<= 50 i1)))
(assert (or v26 (str.<= Str17 (str.++ Str5 Str17)) v1))
(assert (or (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5)) v7 v5))
(assert (or (= 0 999) v5 v24))
(assert (or v1 (or v6 (<= i4 i1 i5 i5) (<= 50 i1)) (<= 50 i1)))
(assert (or v9 v24 v29))
(assert (or (not v30) (not v7) v0))
(assert (or (or v27 v10 v30 v6 (<= 932 i5) v5 (not v7) v29 (=> v4 v9) (= 0 999) (>= i1 98)) (or v27 v10 v30 v6 (<= 932 i5) v5 (not v7) v29 (=> v4 v9) (= (abs 37) 999) (>= i1 98)) v4))
(assert (or v4 v5 (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5))))
(assert (or v5 v9 (or v27 v10 v30 v6 (<= 932 i5) v5 (not v7) v29 (=> v4 v9) (= (abs 37) 999) (>= i1 98))))
(assert (or (or v6 (<= i4 i1 i5 i5) (<= 50 i1)) v3 (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5))))
(assert (or v2 v2 v5))
(assert (or v0 v2 (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5))))
(assert (or (or v27 v10 v30 v6 (<= 932 i5) v5 (not v7) v29 (=> v4 v9) (= (abs 37) 999) (>= i1 98)) v4 v5))
(assert (and (or (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5)) (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16) v29) (or v24 v9 v2) (or (not v30) v7 v9) (or (str.<= Str17 (str.++ Str5 Str17)) v4 v26) (or v1 v5 v7) (or v1 v3 v0) (or (= (abs 37) 999) v3 v2) (or v2 (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5)) v9) (or v0 v2 (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5)))))
(assert (=> (or (= 0 999) v29 (not v7)) (or (or v27 v10 v30 v6 (<= 932 i5) v5 (not v7) v29 (=> v4 v9) (= (abs 37) 999) (>= i1 98)) (and v2 (<= i4 i1 i5 i5) v20 v7 v6 v18 v2 v16) (or v6 (<= i4 i1 i5 i5) (<= 50 i1)))))
(assert (or (or (not v30) (not v7) v24) (or v5 (= 0 999) v2)))
(assert (and (or v9 (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5)) v5) (or v3 v4 (= v7 v4 v8 v9 v0 v4 (<= i4 i1 i5 i5)))))
(check-sat)