diff options
Diffstat (limited to 'test/regress/regress1/quantifiers')
10 files changed, 969 insertions, 5 deletions
diff --git a/test/regress/regress1/quantifiers/f993-loss-easy.smt2 b/test/regress/regress1/quantifiers/f993-loss-easy.smt2 new file mode 100644 index 000000000..775b63338 --- /dev/null +++ b/test/regress/regress1/quantifiers/f993-loss-easy.smt2 @@ -0,0 +1,73 @@ +(set-info :smt-lib-version 2.6) +(set-logic UFDT) +(set-info :status unsat) +(declare-sort A$ 0) +(declare-sort Nat$ 0) +(declare-sort Nat_nat_fun$ 0) +(declare-sort Enat_nat_fun$ 0) +(declare-sort Nat_bool_fun$ 0) +(declare-sort Nat_enat_fun$ 0) +(declare-sort Bool_bool_fun$ 0) +(declare-sort Enat_bool_fun$ 0) +(declare-sort Enat_enat_fun$ 0) +(declare-sort A_stream_bool_fun$ 0) +(declare-sort Nat_bool_fun_nat_fun$ 0) +(declare-sort Nat_nat_bool_fun_fun$ 0) +(declare-sort Bool_enat_bool_fun_fun$ 0) +(declare-sort Enat_enat_bool_fun_fun$ 0) +(declare-sort Nat_bool_fun_nat_bool_fun_fun$ 0) +(declare-datatypes ((Nat_option$ 0)(Enat$ 0)) (((none$) (some$ (the$ Nat$))) +((abs_enat$ (rep_enat$ Nat_option$))) +)) +(declare-sort A_stream$ 0) +(declare-fun shd$ (A_stream$) A$) +(declare-fun stl$ (A_stream$) A_stream$) +(declare-fun sCons$ (A$ A_stream$) A_stream$) +(declare-fun i$ () Nat$) +(declare-fun p$ () A_stream_bool_fun$) +(declare-fun ia$ () Nat$) +(declare-fun uu$ (Nat$) Nat_bool_fun$) +(declare-fun suc$ (Nat$) Nat$) +(declare-fun uua$ (Enat$) Nat_bool_fun$) +(declare-fun uub$ (Bool_bool_fun$) Nat_bool_fun_nat_bool_fun_fun$) +(declare-fun uuc$ (Enat$) Nat_bool_fun$) +(declare-fun uud$ () Nat_nat_fun$) +(declare-fun eSuc$ (Enat$) Enat$) +(declare-fun enat$ (Nat$) Enat$) +(declare-fun less$ (Nat$) Nat_bool_fun$) +(declare-fun plus$ (Enat$) Enat_enat_fun$) +(declare-fun less$a (Enat$) Enat_bool_fun$) +(declare-fun omega$ () A_stream$) +(declare-fun plus$a (Nat$) Nat_nat_fun$) +(declare-fun sdrop$ (Nat$ A_stream$) A_stream$) +(declare-fun omega$a () A_stream$) +(declare-fun sfirst$ (A_stream_bool_fun$ A_stream$) Enat$) +(declare-fun fun_app$ (Nat_bool_fun$ Nat$) Bool) +(declare-fun less_eq$ (Nat$) Nat_bool_fun$) +(declare-fun case_nat$ (Bool) Nat_bool_fun_nat_bool_fun_fun$) +(declare-fun fun_app$a (Enat_bool_fun$ Enat$) Bool) +(declare-fun fun_app$b (Bool_enat_bool_fun_fun$ Bool) Enat_bool_fun$) +(declare-fun fun_app$c (Nat_bool_fun_nat_bool_fun_fun$ Nat_bool_fun$) Nat_bool_fun$) +(declare-fun fun_app$d (Bool_bool_fun$ Bool) Bool) +(declare-fun fun_app$e (Nat_nat_fun$ Nat$) Nat$) +(declare-fun fun_app$f (A_stream_bool_fun$ A_stream$) Bool) +(declare-fun fun_app$g (Nat_enat_fun$ Nat$) Enat$) +(declare-fun fun_app$h (Enat_enat_fun$ Enat$) Enat$) +(declare-fun fun_app$i (Enat_nat_fun$ Enat$) Nat$) +(declare-fun fun_app$j (Enat_enat_bool_fun_fun$ Enat$) Enat_bool_fun$) +(declare-fun fun_app$k (Nat_nat_bool_fun_fun$ Nat$) Nat_bool_fun$) +(declare-fun fun_app$l (Nat_bool_fun_nat_fun$ Nat_bool_fun$) Nat$) +(declare-fun greatest$ (Enat_bool_fun$) Enat$) +(declare-fun less_eq$a (Enat$) Enat_bool_fun$) +(declare-fun rec_enat$ (Nat_bool_fun$) Bool_enat_bool_fun_fun$) +(declare-fun case_enat$ (Nat_bool_fun$) Bool_enat_bool_fun_fun$) +(declare-fun greatest$a () Nat_bool_fun_nat_fun$) +(declare-fun greatestM$ (Nat_nat_fun$) Nat_bool_fun_nat_fun$) +(assert (and +(forall ((?v0 Nat$) (?v1 A_stream_bool_fun$) (?v2 A_stream$)) (=> (fun_app$a (less$a (enat$ ?v0)) (sfirst$ ?v1 ?v2)) (not (fun_app$f ?v1 (sdrop$ ?v0 ?v2)))) ) +(not (fun_app$a (less_eq$a (sfirst$ p$ omega$)) (enat$ (suc$ ia$)))) +(fun_app$f p$ (sdrop$ (suc$ ia$) omega$)) +(forall ((?v0 Enat$) (?v1 Enat$)) (=> (not (fun_app$a (less$a ?v0) ?v1)) (fun_app$a (less_eq$a ?v1) ?v0)) ) +)) +(check-sat) +(exit) diff --git a/test/regress/regress1/quantifiers/infer-arith-trigger-eq.smt2 b/test/regress/regress1/quantifiers/infer-arith-trigger-eq.smt2 index 08d922a65..c19a18f73 100644 --- a/test/regress/regress1/quantifiers/infer-arith-trigger-eq.smt2 +++ b/test/regress/regress1/quantifiers/infer-arith-trigger-eq.smt2 @@ -1,5 +1,3 @@ -; COMMAND-LINE: --infer-arith-trigger-eq -; EXPECT: unsat (set-info :smt-lib-version 2.6) (set-logic UFLIA) (set-info :status unsat) diff --git a/test/regress/regress1/quantifiers/issue2970-string-var-elim.smt2 b/test/regress/regress1/quantifiers/issue2970-string-var-elim.smt2 new file mode 100644 index 000000000..31a57fc8b --- /dev/null +++ b/test/regress/regress1/quantifiers/issue2970-string-var-elim.smt2 @@ -0,0 +1,14 @@ +(set-logic ALL) +(set-info :status unsat) +(declare-fun s () String) +(declare-fun t () String) +(assert (! + (forall ((t1 String) (t2 String)) + (=> (= (str.++ t1 t2) t) (= (= t1 s) false)) + ) + :named a1)) +(assert (! + (not (= (str.prefixof s t) false)) :named a0)) + + +(check-sat) diff --git a/test/regress/regress1/quantifiers/issue993.smt2 b/test/regress/regress1/quantifiers/issue993.smt2 new file mode 100644 index 000000000..40c5538de --- /dev/null +++ b/test/regress/regress1/quantifiers/issue993.smt2 @@ -0,0 +1,108 @@ +(set-logic AUFBVDTNIRA) +(set-info :smt-lib-version 2.0) +(set-info :status unsat) +(declare-sort us_private 0) + +(declare-sort integer 0) + +(declare-fun to_rep1 (integer) Int) + +(declare-datatypes () +((us_split_fields + (mk___split_fields (rec__unit1__t1__c1 integer)(rec__ext__ us_private))))) + +(declare-datatypes () +((us_split_fields__ref + (mk___split_fields__ref (us_split_fields__content us_split_fields))))) +(define-fun us_split_fields__ref___projection ((a us_split_fields__ref)) us_split_fields + (us_split_fields__content a)) + +(declare-datatypes () +((us_rep (mk___rep (us_split_fields1 us_split_fields)(attr__tag Int))))) +(define-fun us_rep___projection ((a us_rep)) us_split_fields (us_split_fields1 + a)) + +(declare-fun is_zero (us_rep) Bool) + +(declare-fun is_zero__post_predicate (Bool us_rep) Bool) + +;; is_zero__def_axiom + (assert + (forall ((x us_rep)) + (! (=> (is_zero__post_predicate (is_zero x) x) + (= (= (is_zero x) true) + (= (to_rep1 (rec__unit1__t1__c1 (us_split_fields1 x))) 0))) :pattern ( + (is_zero x)) ))) + +(declare-datatypes () +((us_split_fields2 + (mk___split_fields1 + (rec__unit2__t2__c2 integer)(rec__unit1__t1__c11 integer)(rec__ext__1 us_private))))) + +(declare-datatypes () +((us_split_fields__ref1 + (mk___split_fields__ref1 (us_split_fields__content1 us_split_fields2))))) +(define-fun us_split_fields__ref_2__projection ((a us_split_fields__ref1)) us_split_fields2 + (us_split_fields__content1 a)) + +(declare-datatypes () +((us_rep1 (mk___rep1 (us_split_fields3 us_split_fields2)(attr__tag1 Int))))) +(define-fun us_rep_3__projection ((a us_rep1)) us_split_fields2 (us_split_fields3 + a)) + +(declare-fun hide_ext__ (integer us_private) us_private) + +(define-fun to_base ((a us_rep1)) us_rep (mk___rep + (mk___split_fields + (rec__unit1__t1__c11 + (us_split_fields3 a)) + (hide_ext__ + (rec__unit2__t2__c2 + (us_split_fields3 a)) + (rec__ext__1 (us_split_fields3 a)))) + (attr__tag1 a))) + +(declare-fun is_zero2 (us_rep1) Bool) + +(declare-fun is_zero__post_predicate2 (Bool us_rep1) Bool) + +;; is_zero__def_axiom + (assert + (forall ((x us_rep1)) + (! (=> (is_zero__post_predicate2 (is_zero2 x) x) + (= (= (is_zero2 x) true) + (and (= (is_zero (to_base x)) true) + (= (to_rep1 (rec__unit2__t2__c2 (us_split_fields3 x))) 0)))) :pattern ( + (is_zero2 x)) ))) + +(declare-fun x2__attr__tag () Int) + +(declare-fun x2__split_fields () integer) + +(declare-fun x2__split_fields1 () integer) + +(declare-fun x2__split_fields2 () us_private) + +;; H + (assert + (forall ((x2__split_fields3 us_split_fields2)) (is_zero__post_predicate2 + (is_zero2 (mk___rep1 x2__split_fields3 x2__attr__tag)) + (mk___rep1 x2__split_fields3 x2__attr__tag)))) + +;; H + (assert + (and (= (to_rep1 x2__split_fields1) 0) (= (to_rep1 x2__split_fields) 0))) + +;; Should be enough to imply following hypothesis + (assert + (forall ((x us_rep1)) (is_zero__post_predicate (is_zero (to_base x)) + (to_base x)))) + +(assert +;; WP_parameter_def + ;; File "main.adb", line 5, characters 0-0 + (not + (= (is_zero (to_base (mk___rep1 + (mk___split_fields1 x2__split_fields x2__split_fields1 + x2__split_fields2) x2__attr__tag))) true))) +(check-sat) diff --git a/test/regress/regress1/quantifiers/nl-pow-trick.smt2 b/test/regress/regress1/quantifiers/nl-pow-trick.smt2 index a369fd9f9..5152b89c4 100644 --- a/test/regress/regress1/quantifiers/nl-pow-trick.smt2 +++ b/test/regress/regress1/quantifiers/nl-pow-trick.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-all +; COMMAND-LINE: --cbqi-all --no-relational-triggers ; EXPECT: unsat (set-logic NIA) (declare-fun a () Int) diff --git a/test/regress/regress1/quantifiers/qbv-test-invert-bvcomp.smt2 b/test/regress/regress1/quantifiers/qbv-test-invert-bvcomp.smt2 index 3b55c0b9a..6bcc6501b 100644 --- a/test/regress/regress1/quantifiers/qbv-test-invert-bvcomp.smt2 +++ b/test/regress/regress1/quantifiers/qbv-test-invert-bvcomp.smt2 @@ -1,7 +1,6 @@ ; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full ; EXPECT: unsat (set-logic BV) -(set-info :status sat) (declare-fun a () (_ BitVec 8)) (declare-fun b () (_ BitVec 8)) (declare-fun c () (_ BitVec 1)) diff --git a/test/regress/regress1/quantifiers/qe.smt2 b/test/regress/regress1/quantifiers/qe.smt2 index 673ece05b..96cdd2497 100644 --- a/test/regress/regress1/quantifiers/qe.smt2 +++ b/test/regress/regress1/quantifiers/qe.smt2 @@ -1,7 +1,6 @@ ; COMMAND-LINE: ; EXPECT: (not (>= (+ a (* (- 1) b)) 1)) (set-logic LIA) -(set-info :status unsat) (declare-fun a () Int) (declare-fun b () Int) (get-qe (exists ((x Int)) (and (<= a x) (<= x b)))) diff --git a/test/regress/regress1/quantifiers/seu169+1.smt2 b/test/regress/regress1/quantifiers/seu169+1.smt2 new file mode 100644 index 000000000..08fd6025b --- /dev/null +++ b/test/regress/regress1/quantifiers/seu169+1.smt2 @@ -0,0 +1,29 @@ +; COMMAND-LINE: --relational-triggers +; EXPECT: unsat +(set-logic UF) +(declare-sort $$unsorted 0) +(declare-fun in ($$unsorted $$unsorted) Bool) +(declare-fun powerset ($$unsorted) $$unsorted) +(declare-fun subset ($$unsorted $$unsorted) Bool) +(declare-fun empty ($$unsorted) Bool) +(declare-fun element ($$unsorted $$unsorted) Bool) +(declare-fun empty_set () $$unsorted) +(set-info :filename "SEU169+1") +(assert (forall ((A $$unsorted) (B $$unsorted)) (or (not (in A B)) (not (in B A))) )) +(assert (forall ((A $$unsorted) (B $$unsorted)) (= (= B (powerset A)) (forall ((C $$unsorted)) (= (in C B) (subset C A)) )) )) +(assert (and (forall ((A $$unsorted) (B $$unsorted)) (or (empty A) (= (element B A) (in B A))) ) (forall ((A $$unsorted) (B $$unsorted)) (or (not (empty A)) (= (element B A) (empty B))) ))) +(assert (forall ((A $$unsorted) (B $$unsorted)) (= (subset A B) (forall ((C $$unsorted)) (or (not (in C A)) (in C B)) )) )) +(assert (forall ((A $$unsorted)) (not (forall ((B $$unsorted)) (not (element B A)) )) )) +(assert (forall ((A $$unsorted)) (not (empty (powerset A))) )) +(assert (empty empty_set)) +(assert (not (forall ((A $$unsorted) (B $$unsorted) (BOUND_VARIABLE_423 $$unsorted)) (or (not (element B (powerset A))) (not (in BOUND_VARIABLE_423 B)) (in BOUND_VARIABLE_423 A)) ))) +(assert (forall ((A $$unsorted)) (or (empty A) (not (forall ((B $$unsorted)) (or (not (element B (powerset A))) (empty B)) ))) )) +(assert (not (forall ((A $$unsorted)) (not (empty A)) ))) +(assert (not (forall ((A $$unsorted)) (empty A) ))) +(assert (forall ((A $$unsorted)) (subset A A) )) +(assert (forall ((A $$unsorted)) (or (not (empty A)) (= empty_set A)) )) +(assert (forall ((A $$unsorted) (B $$unsorted)) (or (not (in A B)) (not (empty B))) )) +(assert (forall ((A $$unsorted) (B $$unsorted)) (or (not (empty A)) (= A B) (not (empty B))) )) +(assert true) +(assert (and (forall ((A $$unsorted) (B $$unsorted)) (or (empty A) (= (element B A) (in B A))) ) (forall ((A $$unsorted) (B $$unsorted)) (or (not (empty A)) (= (element B A) (empty B))) ))) +(check-sat) diff --git a/test/regress/regress1/quantifiers/var-eq-trigger-simple.smt2 b/test/regress/regress1/quantifiers/var-eq-trigger-simple.smt2 new file mode 100644 index 000000000..971cde938 --- /dev/null +++ b/test/regress/regress1/quantifiers/var-eq-trigger-simple.smt2 @@ -0,0 +1,12 @@ +; COMMAND-LINE: --relational-triggers +; EXPECT: unsat +(set-logic ALL) +(declare-sort U 0) +(declare-fun a () U) +(declare-fun P (U U) Bool) +(assert (forall ((x U)) (= x a))) +(assert (forall ((x U) (y U)) (! (= x a) :pattern ((= x y))))) +(declare-fun b () U) +(declare-fun c () U) +(assert (not (= b c))) +(check-sat) diff --git a/test/regress/regress1/quantifiers/var-eq-trigger.smt2 b/test/regress/regress1/quantifiers/var-eq-trigger.smt2 new file mode 100644 index 000000000..bccc86e6f --- /dev/null +++ b/test/regress/regress1/quantifiers/var-eq-trigger.smt2 @@ -0,0 +1,732 @@ +; COMMAND-LINE: --relational-triggers +; EXPECT: unsat +(set-logic UFNIA) +(set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011. Translated to SMT2 by Andrew Reynolds and Morgan Deters.|) +(set-info :smt-lib-version 2.0) +(set-info :category "industrial") +(set-info :status unsat) +(declare-sort S1 0) +(declare-sort S2 0) +(declare-sort S3 0) +(declare-sort S4 0) +(declare-sort S5 0) +(declare-sort S6 0) +(declare-sort S7 0) +(declare-sort S8 0) +(declare-sort S9 0) +(declare-sort S10 0) +(declare-sort S11 0) +(declare-sort S12 0) +(declare-sort S13 0) +(declare-sort S14 0) +(declare-sort S15 0) +(declare-sort S16 0) +(declare-sort S17 0) +(declare-sort S18 0) +(declare-sort S19 0) +(declare-sort S20 0) +(declare-sort S21 0) +(declare-sort S22 0) +(declare-sort S23 0) +(declare-sort S24 0) +(declare-sort S25 0) +(declare-sort S26 0) +(declare-sort S27 0) +(declare-sort S28 0) +(declare-sort S29 0) +(declare-sort S30 0) +(declare-sort S31 0) +(declare-sort S32 0) +(declare-sort S33 0) +(declare-sort S34 0) +(declare-sort S35 0) +(declare-sort S36 0) +(declare-sort S37 0) +(declare-sort S38 0) +(declare-sort S39 0) +(declare-sort S40 0) +(declare-sort S41 0) +(declare-sort S42 0) +(declare-sort S43 0) +(declare-sort S44 0) +(declare-sort S45 0) +(declare-sort S46 0) +(declare-sort S47 0) +(declare-sort S48 0) +(declare-sort S49 0) +(declare-sort S50 0) +(declare-sort S51 0) +(declare-sort S52 0) +(declare-sort S53 0) +(declare-sort S54 0) +(declare-sort S55 0) +(declare-sort S56 0) +(declare-sort S57 0) +(declare-sort S58 0) +(declare-sort S59 0) +(declare-sort S60 0) +(declare-sort S61 0) +(declare-sort S62 0) +(declare-sort S63 0) +(declare-sort S64 0) +(declare-sort S65 0) +(declare-sort S66 0) +(declare-sort S67 0) +(declare-sort S68 0) +(declare-sort S69 0) +(declare-sort S70 0) +(declare-sort S71 0) +(declare-sort S72 0) +(declare-sort S73 0) +(declare-sort S74 0) +(declare-sort S75 0) +(declare-sort S76 0) +(declare-sort S77 0) +(declare-sort S78 0) +(declare-sort S79 0) +(declare-sort S80 0) +(declare-sort S81 0) +(declare-sort S82 0) +(declare-fun f1 () S1) +(declare-fun f2 () S1) +(declare-fun f3 (S3 S2) S1) +(declare-fun f4 (S4 S2) S3) +(declare-fun f5 () S4) +(declare-fun f6 (S6 S5) S1) +(declare-fun f7 (S7 S5) S6) +(declare-fun f8 () S7) +(declare-fun f9 (S9 S8) S1) +(declare-fun f10 (S10 S8) S9) +(declare-fun f11 () S10) +(declare-fun f12 (S11 Int) S1) +(declare-fun f13 (S12 Int) S11) +(declare-fun f14 () S12) +(declare-fun f15 (S14 S13) S1) +(declare-fun f16 () S14) +(declare-fun f17 () S15) +(declare-fun f18 () S2) +(declare-fun f19 (S16 S2) S2) +(declare-fun f20 (S17 S15) S16) +(declare-fun f21 () S17) +(declare-fun f22 () S5) +(declare-fun f23 (S19 S5) S5) +(declare-fun f24 (S20 S18) S19) +(declare-fun f25 () S20) +(declare-fun f26 () S8) +(declare-fun f27 (S21 S8) S8) +(declare-fun f28 (S22 S5) S21) +(declare-fun f29 () S22) +(declare-fun f30 (S23 S2) S16) +(declare-fun f31 () S23) +(declare-fun f32 (S24 S5) S19) +(declare-fun f33 () S24) +(declare-fun f34 (S25 S8) S21) +(declare-fun f35 () S25) +(declare-fun f36 () S17) +(declare-fun f37 () S20) +(declare-fun f38 () S22) +(declare-fun f39 (S26 S14) S2) +(declare-fun f40 (S27 S2) S26) +(declare-fun f41 () S27) +(declare-fun f42 (S13 S14) S1) +(declare-fun f43 (S28 Int) S13) +(declare-fun f44 () S28) +(declare-fun f45 (S29 S14) S5) +(declare-fun f46 (S30 S5) S29) +(declare-fun f47 () S30) +(declare-fun f48 (S31 S14) S8) +(declare-fun f49 (S32 S8) S31) +(declare-fun f50 () S32) +(declare-fun f51 (S2) S1) +(declare-fun f52 (S5) S1) +(declare-fun f53 (S8) S1) +(declare-fun f54 (S33 S2) S15) +(declare-fun f55 () S33) +(declare-fun f56 (S34 S5) S18) +(declare-fun f57 () S34) +(declare-fun f58 (S35 S8) S5) +(declare-fun f59 () S35) +(declare-fun f60 () S4) +(declare-fun f61 () S7) +(declare-fun f62 () S10) +(declare-fun f63 () S23) +(declare-fun f64 () S24) +(declare-fun f65 () S25) +(declare-fun f66 (S36 S15) S1) +(declare-fun f67 (S2) S36) +(declare-fun f68 (S37 S18) S1) +(declare-fun f69 (S5) S37) +(declare-fun f70 (S8) S6) +(declare-fun f71 (S36) S3) +(declare-fun f72 (S37) S6) +(declare-fun f73 (S6) S9) +(declare-fun f74 (S15) S3) +(declare-fun f75 (S5) S9) +(declare-fun f76 (S18) S6) +(declare-fun f77 () S16) +(declare-fun f78 () S19) +(declare-fun f79 () S21) +(declare-fun f80 (S39 S2) S5) +(declare-fun f81 (S40 S38) S39) +(declare-fun f82 () S40) +(declare-fun f83 (S38 S15) S5) +(declare-fun f84 (S42 S2) S8) +(declare-fun f85 (S43 S41) S42) +(declare-fun f86 () S43) +(declare-fun f87 (S41 S15) S8) +(declare-fun f88 (S45 S44) S16) +(declare-fun f89 () S45) +(declare-fun f90 (S44 S15) S2) +(declare-fun f91 (S46 S19) S35) +(declare-fun f92 () S46) +(declare-fun f93 (S48 S47) S21) +(declare-fun f94 () S48) +(declare-fun f95 (S47 S5) S8) +(declare-fun f96 (S50 S8) S2) +(declare-fun f97 (S51 S49) S50) +(declare-fun f98 () S51) +(declare-fun f99 (S49 S5) S2) +(declare-fun f100 (S53 S52) S19) +(declare-fun f101 () S53) +(declare-fun f102 (S52 S18) S5) +(declare-fun f103 (S55 S54) S47) +(declare-fun f104 () S55) +(declare-fun f105 (S54 S18) S8) +(declare-fun f106 (S57 S56) S49) +(declare-fun f107 () S57) +(declare-fun f108 (S56 S18) S2) +(declare-fun f109 () S21) +(declare-fun f110 () S16) +(declare-fun f111 () S19) +(declare-fun f112 () S12) +(declare-fun f113 (S14) S14) +(declare-fun f114 (S58 S13) S47) +(declare-fun f115 () S58) +(declare-fun f116 (S59 S13) S52) +(declare-fun f117 () S59) +(declare-fun f118 (S60 S13) S44) +(declare-fun f119 () S60) +(declare-fun f120 (S61 S13) Int) +(declare-fun f121 () S61) +(declare-fun f122 () S21) +(declare-fun f123 () S19) +(declare-fun f124 () S16) +(declare-fun f125 () S35) +(declare-fun f126 () S34) +(declare-fun f127 () S33) +(declare-fun f128 () S21) +(declare-fun f129 () S19) +(declare-fun f130 () S16) +(declare-fun f131 (S62 S13) S21) +(declare-fun f132 () S62) +(declare-fun f133 (S63 S13) S19) +(declare-fun f134 () S63) +(declare-fun f135 (S64 S13) S16) +(declare-fun f136 () S64) +(declare-fun f137 (S65 S6) S21) +(declare-fun f138 () S65) +(declare-fun f139 (S66 S37) S19) +(declare-fun f140 () S66) +(declare-fun f141 (S67 S36) S16) +(declare-fun f142 () S67) +(declare-fun f143 (S7) S10) +(declare-fun f144 (S68) S7) +(declare-fun f145 (S69) S4) +(declare-fun f146 (S68 S18) S37) +(declare-fun f147 (S69 S15) S36) +(declare-fun f148 () S66) +(declare-fun f149 () S65) +(declare-fun f150 () S67) +(declare-fun f151 (S70 Int) Int) +(declare-fun f152 () S70) +(declare-fun f153 () S28) +(declare-fun f154 (S13) S14) +(declare-fun f155 (S71 S8) S13) +(declare-fun f156 () S71) +(declare-fun f157 () S62) +(declare-fun f158 (S72 S5) S13) +(declare-fun f159 () S72) +(declare-fun f160 () S63) +(declare-fun f161 (S73 S2) S13) +(declare-fun f162 () S73) +(declare-fun f163 () S64) +(declare-fun f164 () S14) +(declare-fun f165 () S1) +(declare-fun f166 (S74 S5) S59) +(declare-fun f167 () S74) +(declare-fun f168 (S75 S8) S58) +(declare-fun f169 () S75) +(declare-fun f170 (S76 S2) S60) +(declare-fun f171 () S76) +(declare-fun f172 (S77 S13) S18) +(declare-fun f173 (S78 S5) S77) +(declare-fun f174 () S78) +(declare-fun f175 (S79 S13) S5) +(declare-fun f176 (S80 S8) S79) +(declare-fun f177 () S80) +(declare-fun f178 (S81 S13) S15) +(declare-fun f179 (S82 S2) S81) +(declare-fun f180 () S82) +(assert (not (= f1 f2))) +(assert (forall ((?v0 S2) (?v1 S2)) (= (= (f3 (f4 f5 ?v0) ?v1) f1) (= ?v0 ?v1)))) +(assert (forall ((?v0 S5) (?v1 S5)) (= (= (f6 (f7 f8 ?v0) ?v1) f1) (= ?v0 ?v1)))) +(assert (forall ((?v0 S8) (?v1 S8)) (= (= (f9 (f10 f11 ?v0) ?v1) f1) (= ?v0 ?v1)))) +(assert (forall ((?v0 Int) (?v1 Int)) (= (= (f12 (f13 f14 ?v0) ?v1) f1) (= ?v0 ?v1)))) +(assert (forall ((?v0 S13)) (= (= (f15 f16 ?v0) f1) false))) +(assert (not (exists ((?v0 S15)) (not (= ?v0 f17))))) +(assert (exists ((?v0 S15) (?v1 S15) (?v2 S15)) (distinct ?v0 ?v1 ?v2))) +(assert (exists ((?v0 S15) (?v1 S15) (?v2 S15)) (distinct ?v0 ?v1 ?v2))) +(assert (forall ((?v0 S15) (?v1 S15)) (=> (not (= ?v0 ?v1)) (exists ((?v2 S15)) (distinct ?v0 ?v1 ?v2))))) +(assert (forall ((?v0 S15) (?v1 S2)) (not (= f18 (f19 (f20 f21 ?v0) ?v1))))) +(assert (forall ((?v0 S18) (?v1 S5)) (not (= f22 (f23 (f24 f25 ?v0) ?v1))))) +(assert (forall ((?v0 S5) (?v1 S8)) (not (= f26 (f27 (f28 f29 ?v0) ?v1))))) +(assert (forall ((?v0 S15) (?v1 S2)) (not (= (f19 (f20 f21 ?v0) ?v1) f18)))) +(assert (forall ((?v0 S18) (?v1 S5)) (not (= (f23 (f24 f25 ?v0) ?v1) f22)))) +(assert (forall ((?v0 S5) (?v1 S8)) (not (= (f27 (f28 f29 ?v0) ?v1) f26)))) +(assert (forall ((?v0 S2)) (= (not (= ?v0 f18)) (exists ((?v1 S15) (?v2 S2)) (= ?v0 (f19 (f20 f21 ?v1) ?v2)))))) +(assert (forall ((?v0 S5)) (= (not (= ?v0 f22)) (exists ((?v1 S18) (?v2 S5)) (= ?v0 (f23 (f24 f25 ?v1) ?v2)))))) +(assert (forall ((?v0 S8)) (= (not (= ?v0 f26)) (exists ((?v1 S5) (?v2 S8)) (= ?v0 (f27 (f28 f29 ?v1) ?v2)))))) +(assert (forall ((?v0 S2)) (=> (=> (= ?v0 f18) false) (=> (forall ((?v1 S15) (?v2 S2)) (=> (= ?v0 (f19 (f20 f21 ?v1) ?v2)) false)) false)))) +(assert (forall ((?v0 S5)) (=> (=> (= ?v0 f22) false) (=> (forall ((?v1 S18) (?v2 S5)) (=> (= ?v0 (f23 (f24 f25 ?v1) ?v2)) false)) false)))) +(assert (forall ((?v0 S8)) (=> (=> (= ?v0 f26) false) (=> (forall ((?v1 S5) (?v2 S8)) (=> (= ?v0 (f27 (f28 f29 ?v1) ?v2)) false)) false)))) +(assert (forall ((?v0 S2) (?v1 S15)) (not (= ?v0 (f19 (f20 f21 ?v1) ?v0))))) +(assert (forall ((?v0 S8) (?v1 S5)) (not (= ?v0 (f27 (f28 f29 ?v1) ?v0))))) +(assert (forall ((?v0 S5) (?v1 S18)) (not (= ?v0 (f23 (f24 f25 ?v1) ?v0))))) +(assert (forall ((?v0 S15) (?v1 S2)) (not (= (f19 (f20 f21 ?v0) ?v1) ?v1)))) +(assert (forall ((?v0 S5) (?v1 S8)) (not (= (f27 (f28 f29 ?v0) ?v1) ?v1)))) +(assert (forall ((?v0 S18) (?v1 S5)) (not (= (f23 (f24 f25 ?v0) ?v1) ?v1)))) +(assert (forall ((?v0 S15) (?v1 S2) (?v2 S15) (?v3 S2)) (= (= (f19 (f20 f21 ?v0) ?v1) (f19 (f20 f21 ?v2) ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3))))) +(assert (forall ((?v0 S5) (?v1 S8) (?v2 S5) (?v3 S8)) (= (= (f27 (f28 f29 ?v0) ?v1) (f27 (f28 f29 ?v2) ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3))))) +(assert (forall ((?v0 S18) (?v1 S5) (?v2 S18) (?v3 S5)) (= (= (f23 (f24 f25 ?v0) ?v1) (f23 (f24 f25 ?v2) ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3))))) +(assert (forall ((?v0 S15) (?v1 S2)) (let ((?v_0 (f19 (f20 f21 ?v0) ?v1))) (= (f19 (f30 f31 ?v_0) f18) ?v_0)))) +(assert (forall ((?v0 S18) (?v1 S5)) (let ((?v_0 (f23 (f24 f25 ?v0) ?v1))) (= (f23 (f32 f33 ?v_0) f22) ?v_0)))) +(assert (forall ((?v0 S5) (?v1 S8)) (let ((?v_0 (f27 (f28 f29 ?v0) ?v1))) (= (f27 (f34 f35 ?v_0) f26) ?v_0)))) +(assert (forall ((?v0 S15)) (= (f19 (f20 f36 ?v0) f18) (f19 (f20 f21 ?v0) f18)))) +(assert (forall ((?v0 S18)) (= (f23 (f24 f37 ?v0) f22) (f23 (f24 f25 ?v0) f22)))) +(assert (forall ((?v0 S5)) (= (f27 (f28 f38 ?v0) f26) (f27 (f28 f29 ?v0) f26)))) +(assert (forall ((?v0 S2) (?v1 S3)) (=> (not (= ?v0 f18)) (=> (forall ((?v2 S15)) (= (f3 ?v1 (f19 (f20 f21 ?v2) f18)) f1)) (=> (forall ((?v2 S15) (?v3 S2)) (=> (not (= ?v3 f18)) (=> (= (f3 ?v1 ?v3) f1) (= (f3 ?v1 (f19 (f20 f21 ?v2) ?v3)) f1)))) (= (f3 ?v1 ?v0) f1)))))) +(assert (forall ((?v0 S5) (?v1 S6)) (=> (not (= ?v0 f22)) (=> (forall ((?v2 S18)) (= (f6 ?v1 (f23 (f24 f25 ?v2) f22)) f1)) (=> (forall ((?v2 S18) (?v3 S5)) (=> (not (= ?v3 f22)) (=> (= (f6 ?v1 ?v3) f1) (= (f6 ?v1 (f23 (f24 f25 ?v2) ?v3)) f1)))) (= (f6 ?v1 ?v0) f1)))))) +(assert (forall ((?v0 S8) (?v1 S9)) (=> (not (= ?v0 f26)) (=> (forall ((?v2 S5)) (= (f9 ?v1 (f27 (f28 f29 ?v2) f26)) f1)) (=> (forall ((?v2 S5) (?v3 S8)) (=> (not (= ?v3 f26)) (=> (= (f9 ?v1 ?v3) f1) (= (f9 ?v1 (f27 (f28 f29 ?v2) ?v3)) f1)))) (= (f9 ?v1 ?v0) f1)))))) +(assert (forall ((?v0 S15) (?v1 S14)) (let ((?v_0 (f19 (f20 f21 ?v0) f18))) (= (f39 (f40 f41 ?v_0) ?v1) (ite (= (f42 (f43 f44 0) ?v1) f1) ?v_0 f18))))) +(assert (forall ((?v0 S18) (?v1 S14)) (let ((?v_0 (f23 (f24 f25 ?v0) f22))) (= (f45 (f46 f47 ?v_0) ?v1) (ite (= (f42 (f43 f44 0) ?v1) f1) ?v_0 f22))))) +(assert (forall ((?v0 S5) (?v1 S14)) (let ((?v_0 (f27 (f28 f29 ?v0) f26))) (= (f48 (f49 f50 ?v_0) ?v1) (ite (= (f42 (f43 f44 0) ?v1) f1) ?v_0 f26))))) +(assert (forall ((?v0 S14)) (= (f39 (f40 f41 f18) ?v0) f18))) +(assert (forall ((?v0 S14)) (= (f45 (f46 f47 f22) ?v0) f22))) +(assert (forall ((?v0 S14)) (= (f48 (f49 f50 f26) ?v0) f26))) +(assert (forall ((?v0 S15) (?v1 S2) (?v2 S15) (?v3 S2)) (let ((?v_0 (f20 f21 ?v0)) (?v_1 (f20 f21 ?v2))) (= (f19 (f30 f31 (f19 ?v_0 ?v1)) (f19 ?v_1 ?v3)) (f19 ?v_0 (f19 ?v_1 (f19 (f30 f31 ?v1) ?v3))))))) +(assert (forall ((?v0 S5) (?v1 S8) (?v2 S5) (?v3 S8)) (let ((?v_0 (f28 f29 ?v0)) (?v_1 (f28 f29 ?v2))) (= (f27 (f34 f35 (f27 ?v_0 ?v1)) (f27 ?v_1 ?v3)) (f27 ?v_0 (f27 ?v_1 (f27 (f34 f35 ?v1) ?v3))))))) +(assert (forall ((?v0 S18) (?v1 S5) (?v2 S18) (?v3 S5)) (let ((?v_0 (f24 f25 ?v0)) (?v_1 (f24 f25 ?v2))) (= (f23 (f32 f33 (f23 ?v_0 ?v1)) (f23 ?v_1 ?v3)) (f23 ?v_0 (f23 ?v_1 (f23 (f32 f33 ?v1) ?v3))))))) +(assert (forall ((?v0 S2)) (= (f19 (f30 f31 ?v0) f18) ?v0))) +(assert (forall ((?v0 S5)) (= (f23 (f32 f33 ?v0) f22) ?v0))) +(assert (forall ((?v0 S8)) (= (f27 (f34 f35 ?v0) f26) ?v0))) +(assert (forall ((?v0 S2)) (= (f19 (f30 f31 f18) ?v0) ?v0))) +(assert (forall ((?v0 S5)) (= (f23 (f32 f33 f22) ?v0) ?v0))) +(assert (forall ((?v0 S8)) (= (f27 (f34 f35 f26) ?v0) ?v0))) +(assert (forall ((?v0 S2)) (= (= ?v0 f18) (= (f51 ?v0) f1)))) +(assert (forall ((?v0 S5)) (= (= ?v0 f22) (= (f52 ?v0) f1)))) +(assert (forall ((?v0 S8)) (= (= ?v0 f26) (= (f53 ?v0) f1)))) +(assert (forall ((?v0 S2)) (= (= (f51 ?v0) f1) (= ?v0 f18)))) +(assert (forall ((?v0 S5)) (= (= (f52 ?v0) f1) (= ?v0 f22)))) +(assert (forall ((?v0 S8)) (= (= (f53 ?v0) f1) (= ?v0 f26)))) +(assert (= (= (f51 f18) f1) true)) +(assert (= (= (f52 f22) f1) true)) +(assert (= (= (f53 f26) f1) true)) +(assert (forall ((?v0 S15) (?v1 S2)) (= (= (f51 (f19 (f20 f21 ?v0) ?v1)) f1) false))) +(assert (forall ((?v0 S5) (?v1 S8)) (= (= (f53 (f27 (f28 f29 ?v0) ?v1)) f1) false))) +(assert (forall ((?v0 S18) (?v1 S5)) (= (= (f52 (f23 (f24 f25 ?v0) ?v1)) f1) false))) +(assert (forall ((?v0 S2) (?v1 S15)) (=> (= ?v0 f18) (= (f54 f55 (f19 (f20 f21 ?v1) ?v0)) ?v1)))) +(assert (forall ((?v0 S5) (?v1 S18)) (=> (= ?v0 f22) (= (f56 f57 (f23 (f24 f25 ?v1) ?v0)) ?v1)))) +(assert (forall ((?v0 S8) (?v1 S5)) (=> (= ?v0 f26) (= (f58 f59 (f27 (f28 f29 ?v1) ?v0)) ?v1)))) +(assert (forall ((?v0 S15) (?v1 S2)) (= (f54 f55 (f19 (f20 f21 ?v0) ?v1)) (ite (= ?v1 f18) ?v0 (f54 f55 ?v1))))) +(assert (forall ((?v0 S18) (?v1 S5)) (= (f56 f57 (f23 (f24 f25 ?v0) ?v1)) (ite (= ?v1 f22) ?v0 (f56 f57 ?v1))))) +(assert (forall ((?v0 S5) (?v1 S8)) (= (f58 f59 (f27 (f28 f29 ?v0) ?v1)) (ite (= ?v1 f26) ?v0 (f58 f59 ?v1))))) +(assert (forall ((?v0 S2) (?v1 S15)) (=> (not (= ?v0 f18)) (= (f54 f55 (f19 (f20 f21 ?v1) ?v0)) (f54 f55 ?v0))))) +(assert (forall ((?v0 S5) (?v1 S18)) (=> (not (= ?v0 f22)) (= (f56 f57 (f23 (f24 f25 ?v1) ?v0)) (f56 f57 ?v0))))) +(assert (forall ((?v0 S8) (?v1 S5)) (=> (not (= ?v0 f26)) (= (f58 f59 (f27 (f28 f29 ?v1) ?v0)) (f58 f59 ?v0))))) +(assert (forall ((?v0 S2)) (= (= (f3 (f4 f60 ?v0) f18) f1) (= (f51 ?v0) f1)))) +(assert (forall ((?v0 S5)) (= (= (f6 (f7 f61 ?v0) f22) f1) (= (f52 ?v0) f1)))) +(assert (forall ((?v0 S8)) (= (= (f9 (f10 f62 ?v0) f26) f1) (= (f53 ?v0) f1)))) +(assert (forall ((?v0 S2) (?v1 S15)) (= (f54 f55 (f19 (f30 f63 ?v0) (f19 (f20 f21 ?v1) f18))) ?v1))) +(assert (forall ((?v0 S5) (?v1 S18)) (= (f56 f57 (f23 (f32 f64 ?v0) (f23 (f24 f25 ?v1) f22))) ?v1))) +(assert (forall ((?v0 S8) (?v1 S5)) (= (f58 f59 (f27 (f34 f65 ?v0) (f27 (f28 f29 ?v1) f26))) ?v1))) +(assert (forall ((?v0 S15)) (= (= (f66 (f67 f18) ?v0) f1) false))) +(assert (forall ((?v0 S18)) (= (= (f68 (f69 f22) ?v0) f1) false))) +(assert (forall ((?v0 S5)) (= (= (f6 (f70 f26) ?v0) f1) false))) +(assert (forall ((?v0 S36)) (= (= (f3 (f71 ?v0) f18) f1) false))) +(assert (forall ((?v0 S37)) (= (= (f6 (f72 ?v0) f22) f1) false))) +(assert (forall ((?v0 S6)) (= (= (f9 (f73 ?v0) f26) f1) false))) +(assert (forall ((?v0 S15) (?v1 S2)) (= (f3 (f74 ?v0) (f19 (f20 f21 ?v0) ?v1)) f1))) +(assert (forall ((?v0 S5) (?v1 S8)) (= (f9 (f75 ?v0) (f27 (f28 f29 ?v0) ?v1)) f1))) +(assert (forall ((?v0 S18) (?v1 S5)) (= (f6 (f76 ?v0) (f23 (f24 f25 ?v0) ?v1)) f1))) +(assert (forall ((?v0 S15) (?v1 S2) (?v2 S15)) (= (= (f66 (f67 (f19 (f20 f21 ?v0) ?v1)) ?v2) f1) (or (= ?v0 ?v2) (= (f66 (f67 ?v1) ?v2) f1))))) +(assert (forall ((?v0 S5) (?v1 S8) (?v2 S5)) (= (= (f6 (f70 (f27 (f28 f29 ?v0) ?v1)) ?v2) f1) (or (= ?v0 ?v2) (= (f6 (f70 ?v1) ?v2) f1))))) +(assert (forall ((?v0 S18) (?v1 S5) (?v2 S18)) (= (= (f68 (f69 (f23 (f24 f25 ?v0) ?v1)) ?v2) f1) (or (= ?v0 ?v2) (= (f68 (f69 ?v1) ?v2) f1))))) +(assert (forall ((?v0 S15) (?v1 S2) (?v2 S15)) (let ((?v_0 (f74 ?v0))) (=> (= (f3 ?v_0 ?v1) f1) (= (f3 ?v_0 (f19 (f20 f21 ?v2) ?v1)) f1))))) +(assert (forall ((?v0 S5) (?v1 S8) (?v2 S5)) (let ((?v_0 (f75 ?v0))) (=> (= (f9 ?v_0 ?v1) f1) (= (f9 ?v_0 (f27 (f28 f29 ?v2) ?v1)) f1))))) +(assert (forall ((?v0 S18) (?v1 S5) (?v2 S18)) (let ((?v_0 (f76 ?v0))) (=> (= (f6 ?v_0 ?v1) f1) (= (f6 ?v_0 (f23 (f24 f25 ?v2) ?v1)) f1))))) +(assert (forall ((?v0 S15) (?v1 S2)) (let ((?v_0 (f20 f21 ?v0))) (= (f19 f77 (f19 ?v_0 ?v1)) (ite (= ?v1 f18) f18 (f19 ?v_0 (f19 f77 ?v1))))))) +(assert (forall ((?v0 S18) (?v1 S5)) (let ((?v_0 (f24 f25 ?v0))) (= (f23 f78 (f23 ?v_0 ?v1)) (ite (= ?v1 f22) f22 (f23 ?v_0 (f23 f78 ?v1))))))) +(assert (forall ((?v0 S5) (?v1 S8)) (let ((?v_0 (f28 f29 ?v0))) (= (f27 f79 (f27 ?v_0 ?v1)) (ite (= ?v1 f26) f26 (f27 ?v_0 (f27 f79 ?v1))))))) +(assert (forall ((?v0 S2) (?v1 S2)) (let ((?v_0 (f30 f63 ?v0))) (= (f19 f77 (f19 ?v_0 ?v1)) (ite (= ?v1 f18) (f19 f77 ?v0) (f19 ?v_0 (f19 f77 ?v1))))))) +(assert (forall ((?v0 S5) (?v1 S5)) (let ((?v_0 (f32 f64 ?v0))) (= (f23 f78 (f23 ?v_0 ?v1)) (ite (= ?v1 f22) (f23 f78 ?v0) (f23 ?v_0 (f23 f78 ?v1))))))) +(assert (forall ((?v0 S8) (?v1 S8)) (let ((?v_0 (f34 f65 ?v0))) (= (f27 f79 (f27 ?v_0 ?v1)) (ite (= ?v1 f26) (f27 f79 ?v0) (f27 ?v_0 (f27 f79 ?v1))))))) +(assert (forall ((?v0 S5) (?v1 S5) (?v2 S5)) (let ((?v_0 (f32 f64 ?v0))) (= (f23 (f32 f64 (f23 ?v_0 ?v1)) ?v2) (f23 ?v_0 (f23 (f32 f64 ?v1) ?v2)))))) +(assert (forall ((?v0 S8) (?v1 S8) (?v2 S8)) (let ((?v_0 (f34 f65 ?v0))) (= (f27 (f34 f65 (f27 ?v_0 ?v1)) ?v2) (f27 ?v_0 (f27 (f34 f65 ?v1) ?v2)))))) +(assert (forall ((?v0 S2) (?v1 S2) (?v2 S2)) (let ((?v_0 (f30 f63 ?v0))) (= (f19 (f30 f63 (f19 ?v_0 ?v1)) ?v2) (f19 ?v_0 (f19 (f30 f63 ?v1) ?v2)))))) +(assert (forall ((?v0 S5) (?v1 S5) (?v2 S5) (?v3 S5)) (= (= (f23 (f32 f64 ?v0) ?v1) (f23 (f32 f64 ?v2) ?v3)) (exists ((?v4 S5)) (let ((?v_0 (f32 f64 ?v4))) (or (and (= ?v0 (f23 (f32 f64 ?v2) ?v4)) (= (f23 ?v_0 ?v1) ?v3)) (and (= (f23 (f32 f64 ?v0) ?v4) ?v2) (= ?v1 (f23 ?v_0 ?v3))))))))) +(assert (forall ((?v0 S8) (?v1 S8) (?v2 S8) (?v3 S8)) (= (= (f27 (f34 f65 ?v0) ?v1) (f27 (f34 f65 ?v2) ?v3)) (exists ((?v4 S8)) (let ((?v_0 (f34 f65 ?v4))) (or (and (= ?v0 (f27 (f34 f65 ?v2) ?v4)) (= (f27 ?v_0 ?v1) ?v3)) (and (= (f27 (f34 f65 ?v0) ?v4) ?v2) (= ?v1 (f27 ?v_0 ?v3))))))))) +(assert (forall ((?v0 S2) (?v1 S2) (?v2 S2) (?v3 S2)) (= (= (f19 (f30 f63 ?v0) ?v1) (f19 (f30 f63 ?v2) ?v3)) (exists ((?v4 S2)) (let ((?v_0 (f30 f63 ?v4))) (or (and (= ?v0 (f19 (f30 f63 ?v2) ?v4)) (= (f19 ?v_0 ?v1) ?v3)) (and (= (f19 (f30 f63 ?v0) ?v4) ?v2) (= ?v1 (f19 ?v_0 ?v3))))))))) +(assert (forall ((?v0 S5) (?v1 S5) (?v2 S5)) (let ((?v_0 (f32 f64 ?v0))) (= (= (f23 ?v_0 ?v1) (f23 ?v_0 ?v2)) (= ?v1 ?v2))))) +(assert (forall ((?v0 S8) (?v1 S8) (?v2 S8)) (let ((?v_0 (f34 f65 ?v0))) (= (= (f27 ?v_0 ?v1) (f27 ?v_0 ?v2)) (= ?v1 ?v2))))) +(assert (forall ((?v0 S2) (?v1 S2) (?v2 S2)) (let ((?v_0 (f30 f63 ?v0))) (= (= (f19 ?v_0 ?v1) (f19 ?v_0 ?v2)) (= ?v1 ?v2))))) +(assert (forall ((?v0 S5) (?v1 S5) (?v2 S5)) (= (= (f23 (f32 f64 ?v0) ?v1) (f23 (f32 f64 ?v2) ?v1)) (= ?v0 ?v2)))) +(assert (forall ((?v0 S8) (?v1 S8) (?v2 S8)) (= (= (f27 (f34 f65 ?v0) ?v1) (f27 (f34 f65 ?v2) ?v1)) (= ?v0 ?v2)))) +(assert (forall ((?v0 S2) (?v1 S2) (?v2 S2)) (= (= (f19 (f30 f63 ?v0) ?v1) (f19 (f30 f63 ?v2) ?v1)) (= ?v0 ?v2)))) +(assert (forall ((?v0 S5) (?v1 S5) (?v2 S5) (?v3 S5) (?v4 S5)) (let ((?v_0 (f32 f64 ?v0))) (=> (= (f23 ?v_0 ?v1) ?v2) (=> (= ?v3 (f23 (f32 f64 ?v1) ?v4)) (= (f23 ?v_0 ?v3) (f23 (f32 f64 ?v2) ?v4))))))) +(assert (forall ((?v0 S8) (?v1 S8) (?v2 S8) (?v3 S8) (?v4 S8)) (let ((?v_0 (f34 f65 ?v0))) (=> (= (f27 ?v_0 ?v1) ?v2) (=> (= ?v3 (f27 (f34 f65 ?v1) ?v4)) (= (f27 ?v_0 ?v3) (f27 (f34 f65 ?v2) ?v4))))))) +(assert (forall ((?v0 S2) (?v1 S2) (?v2 S2) (?v3 S2) (?v4 S2)) (let ((?v_0 (f30 f63 ?v0))) (=> (= (f19 ?v_0 ?v1) ?v2) (=> (= ?v3 (f19 (f30 f63 ?v1) ?v4)) (= (f19 ?v_0 ?v3) (f19 (f30 f63 ?v2) ?v4))))))) +(assert (forall ((?v0 S8) (?v1 S8)) (= (= (f9 (f10 f62 ?v0) ?v1) f1) (= ?v0 ?v1)))) +(assert (forall ((?v0 S5) (?v1 S5)) (= (= (f6 (f7 f61 ?v0) ?v1) f1) (= ?v0 ?v1)))) +(assert (forall ((?v0 S2) (?v1 S2)) (= (= (f3 (f4 f60 ?v0) ?v1) f1) (= ?v0 ?v1)))) +(assert (forall ((?v0 S2) (?v1 S15)) (= (f19 f77 (f19 (f30 f63 ?v0) (f19 (f20 f21 ?v1) f18))) ?v0))) +(assert (forall ((?v0 S5) (?v1 S18)) (= (f23 f78 (f23 (f32 f64 ?v0) (f23 (f24 f25 ?v1) f22))) ?v0))) +(assert (forall ((?v0 S8) (?v1 S5)) (= (f27 f79 (f27 (f34 f65 ?v0) (f27 (f28 f29 ?v1) f26))) ?v0))) +(assert (forall ((?v0 S15) (?v1 S2) (?v2 S2) (?v3 S2) (?v4 S2)) (let ((?v_0 (f20 f21 ?v0))) (=> (= (f19 ?v_0 ?v1) ?v2) (=> (= ?v3 (f19 (f30 f63 ?v1) ?v4)) (= (f19 ?v_0 ?v3) (f19 (f30 f63 ?v2) ?v4))))))) +(assert (forall ((?v0 S5) (?v1 S8) (?v2 S8) (?v3 S8) (?v4 S8)) (let ((?v_0 (f28 f29 ?v0))) (=> (= (f27 ?v_0 ?v1) ?v2) (=> (= ?v3 (f27 (f34 f65 ?v1) ?v4)) (= (f27 ?v_0 ?v3) (f27 (f34 f65 ?v2) ?v4))))))) +(assert (forall ((?v0 S18) (?v1 S5) (?v2 S5) (?v3 S5) (?v4 S5)) (let ((?v_0 (f24 f25 ?v0))) (=> (= (f23 ?v_0 ?v1) ?v2) (=> (= ?v3 (f23 (f32 f64 ?v1) ?v4)) (= (f23 ?v_0 ?v3) (f23 (f32 f64 ?v2) ?v4))))))) +(assert (forall ((?v0 S15) (?v1 S2) (?v2 S2)) (let ((?v_0 (f20 f21 ?v0))) (= (f19 (f30 f63 (f19 ?v_0 ?v1)) ?v2) (f19 ?v_0 (f19 (f30 f63 ?v1) ?v2)))))) +(assert (forall ((?v0 S5) (?v1 S8) (?v2 S8)) (let ((?v_0 (f28 f29 ?v0))) (= (f27 (f34 f65 (f27 ?v_0 ?v1)) ?v2) (f27 ?v_0 (f27 (f34 f65 ?v1) ?v2)))))) +(assert (forall ((?v0 S18) (?v1 S5) (?v2 S5)) (let ((?v_0 (f24 f25 ?v0))) (= (f23 (f32 f64 (f23 ?v_0 ?v1)) ?v2) (f23 ?v_0 (f23 (f32 f64 ?v1) ?v2)))))) +(assert (forall ((?v0 S2) (?v1 S2)) (=> (= ?v0 ?v1) (= ?v0 (f19 (f30 f63 f18) ?v1))))) +(assert (forall ((?v0 S5) (?v1 S5)) (=> (= ?v0 ?v1) (= ?v0 (f23 (f32 f64 f22) ?v1))))) +(assert (forall ((?v0 S8) (?v1 S8)) (=> (= ?v0 ?v1) (= ?v0 (f27 (f34 f65 f26) ?v1))))) +(assert (forall ((?v0 S2) (?v1 S2)) (= (= (f19 (f30 f63 ?v0) ?v1) ?v1) (= ?v0 f18)))) +(assert (forall ((?v0 S5) (?v1 S5)) (= (= (f23 (f32 f64 ?v0) ?v1) ?v1) (= ?v0 f22)))) +(assert (forall ((?v0 S8) (?v1 S8)) (= (= (f27 (f34 f65 ?v0) ?v1) ?v1) (= ?v0 f26)))) +(assert (forall ((?v0 S2) (?v1 S2)) (= (= (f19 (f30 f63 ?v0) ?v1) ?v0) (= ?v1 f18)))) +(assert (forall ((?v0 S5) (?v1 S5)) (= (= (f23 (f32 f64 ?v0) ?v1) ?v0) (= ?v1 f22)))) +(assert (forall ((?v0 S8) (?v1 S8)) (= (= (f27 (f34 f65 ?v0) ?v1) ?v0) (= ?v1 f26)))) +(assert (forall ((?v0 S2) (?v1 S2)) (= (= (f19 (f30 f63 ?v0) ?v1) f18) (and (= ?v0 f18) (= ?v1 f18))))) +(assert (forall ((?v0 S5) (?v1 S5)) (= (= (f23 (f32 f64 ?v0) ?v1) f22) (and (= ?v0 f22) (= ?v1 f22))))) +(assert (forall ((?v0 S8) (?v1 S8)) (= (= (f27 (f34 f65 ?v0) ?v1) f26) (and (= ?v0 f26) (= ?v1 f26))))) +(assert (forall ((?v0 S2) (?v1 S2)) (= (= ?v0 (f19 (f30 f63 ?v1) ?v0)) (= ?v1 f18)))) +(assert (forall ((?v0 S5) (?v1 S5)) (= (= ?v0 (f23 (f32 f64 ?v1) ?v0)) (= ?v1 f22)))) +(assert (forall ((?v0 S8) (?v1 S8)) (= (= ?v0 (f27 (f34 f65 ?v1) ?v0)) (= ?v1 f26)))) +(assert (forall ((?v0 S2) (?v1 S2)) (= (= ?v0 (f19 (f30 f63 ?v0) ?v1)) (= ?v1 f18)))) +(assert (forall ((?v0 S5) (?v1 S5)) (= (= ?v0 (f23 (f32 f64 ?v0) ?v1)) (= ?v1 f22)))) +(assert (forall ((?v0 S8) (?v1 S8)) (= (= ?v0 (f27 (f34 f65 ?v0) ?v1)) (= ?v1 f26)))) +(assert (forall ((?v0 S2)) (= (f19 (f30 f63 ?v0) f18) ?v0))) +(assert (forall ((?v0 S5)) (= (f23 (f32 f64 ?v0) f22) ?v0))) +(assert (forall ((?v0 S8)) (= (f27 (f34 f65 ?v0) f26) ?v0))) +(assert (forall ((?v0 S2) (?v1 S2)) (= (= f18 (f19 (f30 f63 ?v0) ?v1)) (and (= ?v0 f18) (= ?v1 f18))))) +(assert (forall ((?v0 S5) (?v1 S5)) (= (= f22 (f23 (f32 f64 ?v0) ?v1)) (and (= ?v0 f22) (= ?v1 f22))))) +(assert (forall ((?v0 S8) (?v1 S8)) (= (= f26 (f27 (f34 f65 ?v0) ?v1)) (and (= ?v0 f26) (= ?v1 f26))))) +(assert (forall ((?v0 S2)) (= (f19 (f30 f63 f18) ?v0) ?v0))) +(assert (forall ((?v0 S5)) (= (f23 (f32 f64 f22) ?v0) ?v0))) +(assert (forall ((?v0 S8)) (= (f27 (f34 f65 f26) ?v0) ?v0))) +(assert (= (f19 f77 f18) f18)) +(assert (= (f23 f78 f22) f22)) +(assert (= (f27 f79 f26) f26)) +(assert (forall ((?v0 S2)) (=> (not (= ?v0 f18)) (= (f19 (f30 f63 (f19 f77 ?v0)) (f19 (f20 f21 (f54 f55 ?v0)) f18)) ?v0)))) +(assert (forall ((?v0 S5)) (=> (not (= ?v0 f22)) (= (f23 (f32 f64 (f23 f78 ?v0)) (f23 (f24 f25 (f56 f57 ?v0)) f22)) ?v0)))) +(assert (forall ((?v0 S8)) (=> (not (= ?v0 f26)) (= (f27 (f34 f65 (f27 f79 ?v0)) (f27 (f28 f29 (f58 f59 ?v0)) f26)) ?v0)))) +(assert (forall ((?v0 S2) (?v1 S15) (?v2 S2)) (= (= (f19 (f30 f63 ?v0) (f19 (f20 f21 ?v1) f18)) ?v2) (and (not (= ?v2 f18)) (and (= (f19 f77 ?v2) ?v0) (= (f54 f55 ?v2) ?v1)))))) +(assert (forall ((?v0 S5) (?v1 S18) (?v2 S5)) (= (= (f23 (f32 f64 ?v0) (f23 (f24 f25 ?v1) f22)) ?v2) (and (not (= ?v2 f22)) (and (= (f23 f78 ?v2) ?v0) (= (f56 f57 ?v2) ?v1)))))) +(assert (forall ((?v0 S8) (?v1 S5) (?v2 S8)) (= (= (f27 (f34 f65 ?v0) (f27 (f28 f29 ?v1) f26)) ?v2) (and (not (= ?v2 f26)) (and (= (f27 f79 ?v2) ?v0) (= (f58 f59 ?v2) ?v1)))))) +(assert (forall ((?v0 S2) (?v1 S15) (?v2 S2) (?v3 S15)) (= (= (f19 (f30 f63 ?v0) (f19 (f20 f21 ?v1) f18)) (f19 (f30 f63 ?v2) (f19 (f20 f21 ?v3) f18))) (and (= ?v0 ?v2) (= ?v1 ?v3))))) +(assert (forall ((?v0 S5) (?v1 S18) (?v2 S5) (?v3 S18)) (= (= (f23 (f32 f64 ?v0) (f23 (f24 f25 ?v1) f22)) (f23 (f32 f64 ?v2) (f23 (f24 f25 ?v3) f22))) (and (= ?v0 ?v2) (= ?v1 ?v3))))) +(assert (forall ((?v0 S8) (?v1 S5) (?v2 S8) (?v3 S5)) (= (= (f27 (f34 f65 ?v0) (f27 (f28 f29 ?v1) f26)) (f27 (f34 f65 ?v2) (f27 (f28 f29 ?v3) f26))) (and (= ?v0 ?v2) (= ?v1 ?v3))))) +(assert (forall ((?v0 S15) (?v1 S2) (?v2 S2) (?v3 S2)) (let ((?v_0 (f19 (f20 f21 ?v0) ?v1))) (= (= ?v_0 (f19 (f30 f63 ?v2) ?v3)) (or (and (= ?v2 f18) (= ?v_0 ?v3)) (exists ((?v4 S2)) (and (= (f19 (f20 f21 ?v0) ?v4) ?v2) (= ?v1 (f19 (f30 f63 ?v4) ?v3))))))))) +(assert (forall ((?v0 S18) (?v1 S5) (?v2 S5) (?v3 S5)) (let ((?v_0 (f23 (f24 f25 ?v0) ?v1))) (= (= ?v_0 (f23 (f32 f64 ?v2) ?v3)) (or (and (= ?v2 f22) (= ?v_0 ?v3)) (exists ((?v4 S5)) (and (= (f23 (f24 f25 ?v0) ?v4) ?v2) (= ?v1 (f23 (f32 f64 ?v4) ?v3))))))))) +(assert (forall ((?v0 S5) (?v1 S8) (?v2 S8) (?v3 S8)) (let ((?v_0 (f27 (f28 f29 ?v0) ?v1))) (= (= ?v_0 (f27 (f34 f65 ?v2) ?v3)) (or (and (= ?v2 f26) (= ?v_0 ?v3)) (exists ((?v4 S8)) (and (= (f27 (f28 f29 ?v0) ?v4) ?v2) (= ?v1 (f27 (f34 f65 ?v4) ?v3))))))))) +(assert (forall ((?v0 S2) (?v1 S2) (?v2 S15) (?v3 S2)) (let ((?v_0 (f19 (f20 f21 ?v2) ?v3))) (= (= (f19 (f30 f63 ?v0) ?v1) ?v_0) (or (and (= ?v0 f18) (= ?v1 ?v_0)) (exists ((?v4 S2)) (and (= ?v0 (f19 (f20 f21 ?v2) ?v4)) (= (f19 (f30 f63 ?v4) ?v1) ?v3)))))))) +(assert (forall ((?v0 S5) (?v1 S5) (?v2 S18) (?v3 S5)) (let ((?v_0 (f23 (f24 f25 ?v2) ?v3))) (= (= (f23 (f32 f64 ?v0) ?v1) ?v_0) (or (and (= ?v0 f22) (= ?v1 ?v_0)) (exists ((?v4 S5)) (and (= ?v0 (f23 (f24 f25 ?v2) ?v4)) (= (f23 (f32 f64 ?v4) ?v1) ?v3)))))))) +(assert (forall ((?v0 S8) (?v1 S8) (?v2 S5) (?v3 S8)) (let ((?v_0 (f27 (f28 f29 ?v2) ?v3))) (= (= (f27 (f34 f65 ?v0) ?v1) ?v_0) (or (and (= ?v0 f26) (= ?v1 ?v_0)) (exists ((?v4 S8)) (and (= ?v0 (f27 (f28 f29 ?v2) ?v4)) (= (f27 (f34 f65 ?v4) ?v1) ?v3)))))))) +(assert (forall ((?v0 S2) (?v1 S2)) (= (f54 f55 (f19 (f30 f63 ?v0) ?v1)) (ite (= ?v1 f18) (f54 f55 ?v0) (f54 f55 ?v1))))) +(assert (forall ((?v0 S5) (?v1 S5)) (= (f56 f57 (f23 (f32 f64 ?v0) ?v1)) (ite (= ?v1 f22) (f56 f57 ?v0) (f56 f57 ?v1))))) +(assert (forall ((?v0 S8) (?v1 S8)) (= (f58 f59 (f27 (f34 f65 ?v0) ?v1)) (ite (= ?v1 f26) (f58 f59 ?v0) (f58 f59 ?v1))))) +(assert (forall ((?v0 S2) (?v1 S2)) (=> (not (= ?v0 f18)) (= (f54 f55 (f19 (f30 f63 ?v1) ?v0)) (f54 f55 ?v0))))) +(assert (forall ((?v0 S5) (?v1 S5)) (=> (not (= ?v0 f22)) (= (f56 f57 (f23 (f32 f64 ?v1) ?v0)) (f56 f57 ?v0))))) +(assert (forall ((?v0 S8) (?v1 S8)) (=> (not (= ?v0 f26)) (= (f58 f59 (f27 (f34 f65 ?v1) ?v0)) (f58 f59 ?v0))))) +(assert (forall ((?v0 S2) (?v1 S2)) (=> (= ?v0 f18) (= (f54 f55 (f19 (f30 f63 ?v1) ?v0)) (f54 f55 ?v1))))) +(assert (forall ((?v0 S5) (?v1 S5)) (=> (= ?v0 f22) (= (f56 f57 (f23 (f32 f64 ?v1) ?v0)) (f56 f57 ?v1))))) +(assert (forall ((?v0 S8) (?v1 S8)) (=> (= ?v0 f26) (= (f58 f59 (f27 (f34 f65 ?v1) ?v0)) (f58 f59 ?v1))))) +(assert (forall ((?v0 S38) (?v1 S15) (?v2 S2)) (let ((?v_0 (f81 f82 ?v0))) (= (f80 ?v_0 (f19 (f20 f21 ?v1) ?v2)) (f23 (f32 f64 (f83 ?v0 ?v1)) (f80 ?v_0 ?v2)))))) +(assert (forall ((?v0 S41) (?v1 S15) (?v2 S2)) (let ((?v_0 (f85 f86 ?v0))) (= (f84 ?v_0 (f19 (f20 f21 ?v1) ?v2)) (f27 (f34 f65 (f87 ?v0 ?v1)) (f84 ?v_0 ?v2)))))) +(assert (forall ((?v0 S44) (?v1 S15) (?v2 S2)) (let ((?v_0 (f88 f89 ?v0))) (= (f19 ?v_0 (f19 (f20 f21 ?v1) ?v2)) (f19 (f30 f63 (f90 ?v0 ?v1)) (f19 ?v_0 ?v2)))))) +(assert (forall ((?v0 S19) (?v1 S5) (?v2 S8)) (let ((?v_0 (f91 f92 ?v0))) (= (f58 ?v_0 (f27 (f28 f29 ?v1) ?v2)) (f23 (f32 f64 (f23 ?v0 ?v1)) (f58 ?v_0 ?v2)))))) +(assert (forall ((?v0 S47) (?v1 S5) (?v2 S8)) (let ((?v_0 (f93 f94 ?v0))) (= (f27 ?v_0 (f27 (f28 f29 ?v1) ?v2)) (f27 (f34 f65 (f95 ?v0 ?v1)) (f27 ?v_0 ?v2)))))) +(assert (forall ((?v0 S49) (?v1 S5) (?v2 S8)) (let ((?v_0 (f97 f98 ?v0))) (= (f96 ?v_0 (f27 (f28 f29 ?v1) ?v2)) (f19 (f30 f63 (f99 ?v0 ?v1)) (f96 ?v_0 ?v2)))))) +(assert (forall ((?v0 S52) (?v1 S18) (?v2 S5)) (let ((?v_0 (f100 f101 ?v0))) (= (f23 ?v_0 (f23 (f24 f25 ?v1) ?v2)) (f23 (f32 f64 (f102 ?v0 ?v1)) (f23 ?v_0 ?v2)))))) +(assert (forall ((?v0 S54) (?v1 S18) (?v2 S5)) (let ((?v_0 (f103 f104 ?v0))) (= (f95 ?v_0 (f23 (f24 f25 ?v1) ?v2)) (f27 (f34 f65 (f105 ?v0 ?v1)) (f95 ?v_0 ?v2)))))) +(assert (forall ((?v0 S56) (?v1 S18) (?v2 S5)) (let ((?v_0 (f106 f107 ?v0))) (= (f99 ?v_0 (f23 (f24 f25 ?v1) ?v2)) (f19 (f30 f63 (f108 ?v0 ?v1)) (f99 ?v_0 ?v2)))))) +(assert (forall ((?v0 S2)) (=> (=> (= ?v0 f18) false) (=> (forall ((?v1 S2) (?v2 S15)) (=> (= ?v0 (f19 (f30 f63 ?v1) (f19 (f20 f21 ?v2) f18))) false)) false)))) +(assert (forall ((?v0 S5)) (=> (=> (= ?v0 f22) false) (=> (forall ((?v1 S5) (?v2 S18)) (=> (= ?v0 (f23 (f32 f64 ?v1) (f23 (f24 f25 ?v2) f22))) false)) false)))) +(assert (forall ((?v0 S8)) (=> (=> (= ?v0 f26) false) (=> (forall ((?v1 S8) (?v2 S5)) (=> (= ?v0 (f27 (f34 f65 ?v1) (f27 (f28 f29 ?v2) f26))) false)) false)))) +(assert (forall ((?v0 S3) (?v1 S2)) (=> (= (f3 ?v0 f18) f1) (=> (forall ((?v2 S15) (?v3 S2)) (=> (= (f3 ?v0 ?v3) f1) (= (f3 ?v0 (f19 (f30 f63 ?v3) (f19 (f20 f21 ?v2) f18))) f1))) (= (f3 ?v0 ?v1) f1))))) +(assert (forall ((?v0 S6) (?v1 S5)) (=> (= (f6 ?v0 f22) f1) (=> (forall ((?v2 S18) (?v3 S5)) (=> (= (f6 ?v0 ?v3) f1) (= (f6 ?v0 (f23 (f32 f64 ?v3) (f23 (f24 f25 ?v2) f22))) f1))) (= (f6 ?v0 ?v1) f1))))) +(assert (forall ((?v0 S9) (?v1 S8)) (=> (= (f9 ?v0 f26) f1) (=> (forall ((?v2 S5) (?v3 S8)) (=> (= (f9 ?v0 ?v3) f1) (= (f9 ?v0 (f27 (f34 f65 ?v3) (f27 (f28 f29 ?v2) f26))) f1))) (= (f9 ?v0 ?v1) f1))))) +(assert (forall ((?v0 S15) (?v1 S2)) (let ((?v_0 (f20 f21 ?v0))) (and (= (f27 f109 f26) f26) (= (f19 f110 (f19 ?v_0 ?v1)) (f19 (f30 f63 ?v1) (f19 ?v_0 f18))))))) +(assert (forall ((?v0 S15) (?v1 S2)) (let ((?v_0 (f20 f21 ?v0))) (and (= (f23 f111 f22) f22) (= (f19 f110 (f19 ?v_0 ?v1)) (f19 (f30 f63 ?v1) (f19 ?v_0 f18))))))) +(assert (forall ((?v0 S15) (?v1 S2)) (let ((?v_0 (f20 f21 ?v0))) (and (= (f19 f110 f18) f18) (= (f19 f110 (f19 ?v_0 ?v1)) (f19 (f30 f63 ?v1) (f19 ?v_0 f18))))))) +(assert (forall ((?v0 S18) (?v1 S5)) (let ((?v_0 (f24 f25 ?v0))) (and (= (f27 f109 f26) f26) (= (f23 f111 (f23 ?v_0 ?v1)) (f23 (f32 f64 ?v1) (f23 ?v_0 f22))))))) +(assert (forall ((?v0 S18) (?v1 S5)) (let ((?v_0 (f24 f25 ?v0))) (and (= (f23 f111 f22) f22) (= (f23 f111 (f23 ?v_0 ?v1)) (f23 (f32 f64 ?v1) (f23 ?v_0 f22))))))) +(assert (forall ((?v0 S18) (?v1 S5)) (let ((?v_0 (f24 f25 ?v0))) (and (= (f19 f110 f18) f18) (= (f23 f111 (f23 ?v_0 ?v1)) (f23 (f32 f64 ?v1) (f23 ?v_0 f22))))))) +(assert (forall ((?v0 S5) (?v1 S8)) (let ((?v_0 (f28 f29 ?v0))) (and (= (f27 f109 f26) f26) (= (f27 f109 (f27 ?v_0 ?v1)) (f27 (f34 f65 ?v1) (f27 ?v_0 f26))))))) +(assert (forall ((?v0 S5) (?v1 S8)) (let ((?v_0 (f28 f29 ?v0))) (and (= (f23 f111 f22) f22) (= (f27 f109 (f27 ?v_0 ?v1)) (f27 (f34 f65 ?v1) (f27 ?v_0 f26))))))) +(assert (forall ((?v0 S5) (?v1 S8)) (let ((?v_0 (f28 f29 ?v0))) (and (= (f19 f110 f18) f18) (= (f27 f109 (f27 ?v_0 ?v1)) (f27 (f34 f65 ?v1) (f27 ?v_0 f26))))))) +(assert (= f11 f62)) +(assert (= f8 f61)) +(assert (= f5 f60)) +(assert (= f14 f112)) +(assert (forall ((?v0 S8) (?v1 S8)) (= (= (f9 (f10 f62 ?v0) ?v1) f1) (= ?v0 ?v1)))) +(assert (forall ((?v0 S5) (?v1 S5)) (= (= (f6 (f7 f61 ?v0) ?v1) f1) (= ?v0 ?v1)))) +(assert (forall ((?v0 S2) (?v1 S2)) (= (= (f3 (f4 f60 ?v0) ?v1) f1) (= ?v0 ?v1)))) +(assert (forall ((?v0 Int) (?v1 Int)) (= (= (f12 (f13 f112 ?v0) ?v1) f1) (= ?v0 ?v1)))) +(assert (forall ((?v0 S8)) (= (= (f9 (f10 f62 ?v0) ?v0) f1) true))) +(assert (forall ((?v0 S5)) (= (= (f6 (f7 f61 ?v0) ?v0) f1) true))) +(assert (forall ((?v0 S2)) (= (= (f3 (f4 f60 ?v0) ?v0) f1) true))) +(assert (forall ((?v0 Int)) (= (= (f12 (f13 f112 ?v0) ?v0) f1) true))) +(assert (forall ((?v0 S13) (?v1 S14)) (= (= (f42 ?v0 ?v1) f1) (= (f15 ?v1 ?v0) f1)))) +(assert (forall ((?v0 S14)) (= (f113 ?v0) ?v0))) +(assert (= f62 f11)) +(assert (= f61 f8)) +(assert (= f60 f5)) +(assert (= f112 f14)) +(assert (forall ((?v0 S13) (?v1 S5)) (let ((?v_1 (f95 (f114 f115 ?v0) ?v1)) (?v_0 (f28 f29 ?v1))) (= (f27 (f34 f65 ?v_1) (f27 ?v_0 f26)) (f27 ?v_0 ?v_1))))) +(assert (forall ((?v0 S13) (?v1 S18)) (let ((?v_1 (f102 (f116 f117 ?v0) ?v1)) (?v_0 (f24 f25 ?v1))) (= (f23 (f32 f64 ?v_1) (f23 ?v_0 f22)) (f23 ?v_0 ?v_1))))) +(assert (forall ((?v0 S13) (?v1 S15)) (let ((?v_1 (f90 (f118 f119 ?v0) ?v1)) (?v_0 (f20 f21 ?v1))) (= (f19 (f30 f63 ?v_1) (f19 ?v_0 f18)) (f19 ?v_0 ?v_1))))) +(assert (forall ((?v0 S13) (?v1 S18)) (= (f102 (f116 f117 (f43 f44 (+ (f120 f121 ?v0) 1))) ?v1) (f23 (f24 f25 ?v1) (f102 (f116 f117 ?v0) ?v1))))) +(assert (forall ((?v0 S13) (?v1 S5)) (= (f95 (f114 f115 (f43 f44 (+ (f120 f121 ?v0) 1))) ?v1) (f27 (f28 f29 ?v1) (f95 (f114 f115 ?v0) ?v1))))) +(assert (forall ((?v0 S13) (?v1 S15)) (= (f90 (f118 f119 (f43 f44 (+ (f120 f121 ?v0) 1))) ?v1) (f19 (f20 f21 ?v1) (f90 (f118 f119 ?v0) ?v1))))) +(assert (forall ((?v0 S5)) (= (f95 (f114 f115 (f43 f44 0)) ?v0) f26))) +(assert (forall ((?v0 S18)) (= (f102 (f116 f117 (f43 f44 0)) ?v0) f22))) +(assert (forall ((?v0 S15)) (= (f90 (f118 f119 (f43 f44 0)) ?v0) f18))) +(assert (forall ((?v0 S13) (?v1 S5)) (= (= f26 (f95 (f114 f115 ?v0) ?v1)) (= ?v0 (f43 f44 0))))) +(assert (forall ((?v0 S13) (?v1 S18)) (= (= f22 (f102 (f116 f117 ?v0) ?v1)) (= ?v0 (f43 f44 0))))) +(assert (forall ((?v0 S13) (?v1 S15)) (= (= f18 (f90 (f118 f119 ?v0) ?v1)) (= ?v0 (f43 f44 0))))) +(assert (forall ((?v0 S13) (?v1 S5)) (= (= (f95 (f114 f115 ?v0) ?v1) f26) (= ?v0 (f43 f44 0))))) +(assert (forall ((?v0 S13) (?v1 S18)) (= (= (f102 (f116 f117 ?v0) ?v1) f22) (= ?v0 (f43 f44 0))))) +(assert (forall ((?v0 S13) (?v1 S15)) (= (= (f90 (f118 f119 ?v0) ?v1) f18) (= ?v0 (f43 f44 0))))) +(assert (forall ((?v0 S8)) (= (= (f27 f109 ?v0) f26) (= ?v0 f26)))) +(assert (forall ((?v0 S5)) (= (= (f23 f111 ?v0) f22) (= ?v0 f22)))) +(assert (forall ((?v0 S2)) (= (= (f19 f110 ?v0) f18) (= ?v0 f18)))) +(assert (forall ((?v0 S13) (?v1 S18) (?v2 S5)) (let ((?v_1 (f32 f64 (f102 (f116 f117 ?v0) ?v1))) (?v_0 (f24 f25 ?v1))) (= (f23 ?v_1 (f23 ?v_0 ?v2)) (f23 ?v_0 (f23 ?v_1 ?v2)))))) +(assert (forall ((?v0 S13) (?v1 S5) (?v2 S8)) (let ((?v_1 (f34 f65 (f95 (f114 f115 ?v0) ?v1))) (?v_0 (f28 f29 ?v1))) (= (f27 ?v_1 (f27 ?v_0 ?v2)) (f27 ?v_0 (f27 ?v_1 ?v2)))))) +(assert (forall ((?v0 S13) (?v1 S15) (?v2 S2)) (let ((?v_1 (f30 f63 (f90 (f118 f119 ?v0) ?v1))) (?v_0 (f20 f21 ?v1))) (= (f19 ?v_1 (f19 ?v_0 ?v2)) (f19 ?v_0 (f19 ?v_1 ?v2)))))) +(assert (forall ((?v0 S18) (?v1 S5)) (= (= (f6 (f76 ?v0) ?v1) f1) (or (exists ((?v2 S18) (?v3 S5)) (and (= ?v0 ?v2) (= ?v1 (f23 (f24 f25 ?v2) ?v3)))) (exists ((?v2 S18) (?v3 S5) (?v4 S18)) (and (= ?v0 ?v2) (and (= ?v1 (f23 (f24 f25 ?v4) ?v3)) (= (f6 (f76 ?v2) ?v3) f1)))))))) +(assert (forall ((?v0 S5) (?v1 S8)) (= (= (f9 (f75 ?v0) ?v1) f1) (or (exists ((?v2 S5) (?v3 S8)) (and (= ?v0 ?v2) (= ?v1 (f27 (f28 f29 ?v2) ?v3)))) (exists ((?v2 S5) (?v3 S8) (?v4 S5)) (and (= ?v0 ?v2) (and (= ?v1 (f27 (f28 f29 ?v4) ?v3)) (= (f9 (f75 ?v2) ?v3) f1)))))))) +(assert (forall ((?v0 S15) (?v1 S2)) (= (= (f3 (f74 ?v0) ?v1) f1) (or (exists ((?v2 S15) (?v3 S2)) (and (= ?v0 ?v2) (= ?v1 (f19 (f20 f21 ?v2) ?v3)))) (exists ((?v2 S15) (?v3 S2) (?v4 S15)) (and (= ?v0 ?v2) (and (= ?v1 (f19 (f20 f21 ?v4) ?v3)) (= (f3 (f74 ?v2) ?v3) f1)))))))) +(assert (forall ((?v0 S5) (?v1 S8)) (let ((?v_0 (f28 f29 ?v0))) (= (f27 f122 (f27 ?v_0 ?v1)) (f27 (f34 f65 (f27 f122 ?v1)) (f27 ?v_0 f26)))))) +(assert (forall ((?v0 S18) (?v1 S5)) (let ((?v_0 (f24 f25 ?v0))) (= (f23 f123 (f23 ?v_0 ?v1)) (f23 (f32 f64 (f23 f123 ?v1)) (f23 ?v_0 f22)))))) +(assert (forall ((?v0 S15) (?v1 S2)) (let ((?v_0 (f20 f21 ?v0))) (= (f19 f124 (f19 ?v_0 ?v1)) (f19 (f30 f63 (f19 f124 ?v1)) (f19 ?v_0 f18)))))) +(assert (forall ((?v0 S8) (?v1 S5) (?v2 S8)) (let ((?v_0 (f28 f29 ?v1))) (= (= (f27 f122 ?v0) (f27 ?v_0 ?v2)) (= ?v0 (f27 (f34 f65 (f27 f122 ?v2)) (f27 ?v_0 f26))))))) +(assert (forall ((?v0 S5) (?v1 S18) (?v2 S5)) (let ((?v_0 (f24 f25 ?v1))) (= (= (f23 f123 ?v0) (f23 ?v_0 ?v2)) (= ?v0 (f23 (f32 f64 (f23 f123 ?v2)) (f23 ?v_0 f22))))))) +(assert (forall ((?v0 S2) (?v1 S15) (?v2 S2)) (let ((?v_0 (f20 f21 ?v1))) (= (= (f19 f124 ?v0) (f19 ?v_0 ?v2)) (= ?v0 (f19 (f30 f63 (f19 f124 ?v2)) (f19 ?v_0 f18))))))) +(assert (forall ((?v0 S8) (?v1 S8)) (=> (not (= ?v0 f26)) (= (f58 f125 (f27 (f34 f65 ?v0) ?v1)) (f58 f125 ?v0))))) +(assert (forall ((?v0 S5) (?v1 S5)) (=> (not (= ?v0 f22)) (= (f56 f126 (f23 (f32 f64 ?v0) ?v1)) (f56 f126 ?v0))))) +(assert (forall ((?v0 S2) (?v1 S2)) (=> (not (= ?v0 f18)) (= (f54 f127 (f19 (f30 f63 ?v0) ?v1)) (f54 f127 ?v0))))) +(assert (forall ((?v0 S8) (?v1 S8)) (= (f58 f125 (f27 (f34 f65 ?v0) ?v1)) (ite (= ?v0 f26) (f58 f125 ?v1) (f58 f125 ?v0))))) +(assert (forall ((?v0 S5) (?v1 S5)) (= (f56 f126 (f23 (f32 f64 ?v0) ?v1)) (ite (= ?v0 f22) (f56 f126 ?v1) (f56 f126 ?v0))))) +(assert (forall ((?v0 S2) (?v1 S2)) (= (f54 f127 (f19 (f30 f63 ?v0) ?v1)) (ite (= ?v0 f18) (f54 f127 ?v1) (f54 f127 ?v0))))) +(assert (forall ((?v0 S8)) (=> (not (= ?v0 f26)) (= (f27 f109 ?v0) (f27 (f34 f65 (f27 f128 ?v0)) (f27 (f28 f29 (f58 f125 ?v0)) f26)))))) +(assert (forall ((?v0 S5)) (=> (not (= ?v0 f22)) (= (f23 f111 ?v0) (f23 (f32 f64 (f23 f129 ?v0)) (f23 (f24 f25 (f56 f126 ?v0)) f22)))))) +(assert (forall ((?v0 S2)) (=> (not (= ?v0 f18)) (= (f19 f110 ?v0) (f19 (f30 f63 (f19 f130 ?v0)) (f19 (f20 f21 (f54 f127 ?v0)) f18)))))) +(assert (forall ((?v0 S8)) (= (= (f27 f122 ?v0) f26) (= ?v0 f26)))) +(assert (forall ((?v0 S5)) (= (= (f23 f123 ?v0) f22) (= ?v0 f22)))) +(assert (forall ((?v0 S2)) (= (= (f19 f124 ?v0) f18) (= ?v0 f18)))) +(assert (forall ((?v0 S8)) (= (= f26 (f27 f122 ?v0)) (= ?v0 f26)))) +(assert (forall ((?v0 S5)) (= (= f22 (f23 f123 ?v0)) (= ?v0 f22)))) +(assert (forall ((?v0 S2)) (= (= f18 (f19 f124 ?v0)) (= ?v0 f18)))) +(assert (= (f27 f122 f26) f26)) +(assert (= (f23 f123 f22) f22)) +(assert (= (f19 f124 f18) f18)) +(assert (forall ((?v0 S8)) (=> (not (= ?v0 f26)) (= (f58 f59 (f27 f122 ?v0)) (f58 f125 ?v0))))) +(assert (forall ((?v0 S5)) (=> (not (= ?v0 f22)) (= (f56 f57 (f23 f123 ?v0)) (f56 f126 ?v0))))) +(assert (forall ((?v0 S2)) (=> (not (= ?v0 f18)) (= (f54 f55 (f19 f124 ?v0)) (f54 f127 ?v0))))) +(assert (forall ((?v0 S8)) (=> (not (= ?v0 f26)) (= (f58 f125 (f27 f122 ?v0)) (f58 f59 ?v0))))) +(assert (forall ((?v0 S5)) (=> (not (= ?v0 f22)) (= (f56 f126 (f23 f123 ?v0)) (f56 f57 ?v0))))) +(assert (forall ((?v0 S2)) (=> (not (= ?v0 f18)) (= (f54 f127 (f19 f124 ?v0)) (f54 f55 ?v0))))) +(assert (forall ((?v0 S18) (?v1 S5)) (= (f23 f129 (f23 (f24 f25 ?v0) ?v1)) ?v1))) +(assert (forall ((?v0 S5) (?v1 S8)) (= (f27 f128 (f27 (f28 f29 ?v0) ?v1)) ?v1))) +(assert (forall ((?v0 S15) (?v1 S2)) (= (f19 f130 (f19 (f20 f21 ?v0) ?v1)) ?v1))) +(assert (= (f27 f128 f26) f26)) +(assert (= (f23 f129 f22) f22)) +(assert (= (f19 f130 f18) f18)) +(assert (forall ((?v0 S18) (?v1 S5)) (= (f56 f126 (f23 (f24 f25 ?v0) ?v1)) ?v0))) +(assert (forall ((?v0 S5) (?v1 S8)) (= (f58 f125 (f27 (f28 f29 ?v0) ?v1)) ?v0))) +(assert (forall ((?v0 S15) (?v1 S2)) (= (f54 f127 (f19 (f20 f21 ?v0) ?v1)) ?v0))) +(assert (forall ((?v0 S5) (?v1 S8)) (let ((?v_0 (f27 (f28 f29 ?v0) f26))) (= (= ?v_0 (f27 f122 ?v1)) (= ?v1 ?v_0))))) +(assert (forall ((?v0 S18) (?v1 S5)) (let ((?v_0 (f23 (f24 f25 ?v0) f22))) (= (= ?v_0 (f23 f123 ?v1)) (= ?v1 ?v_0))))) +(assert (forall ((?v0 S15) (?v1 S2)) (let ((?v_0 (f19 (f20 f21 ?v0) f18))) (= (= ?v_0 (f19 f124 ?v1)) (= ?v1 ?v_0))))) +(assert (forall ((?v0 S8) (?v1 S5)) (let ((?v_0 (f27 (f28 f29 ?v1) f26))) (= (= (f27 f122 ?v0) ?v_0) (= ?v0 ?v_0))))) +(assert (forall ((?v0 S5) (?v1 S18)) (let ((?v_0 (f23 (f24 f25 ?v1) f22))) (= (= (f23 f123 ?v0) ?v_0) (= ?v0 ?v_0))))) +(assert (forall ((?v0 S2) (?v1 S15)) (let ((?v_0 (f19 (f20 f21 ?v1) f18))) (= (= (f19 f124 ?v0) ?v_0) (= ?v0 ?v_0))))) +(assert (forall ((?v0 S8) (?v1 S8)) (=> (not (= ?v0 f26)) (= (f27 f128 (f27 (f34 f65 ?v0) ?v1)) (f27 (f34 f65 (f27 f128 ?v0)) ?v1))))) +(assert (forall ((?v0 S5) (?v1 S5)) (=> (not (= ?v0 f22)) (= (f23 f129 (f23 (f32 f64 ?v0) ?v1)) (f23 (f32 f64 (f23 f129 ?v0)) ?v1))))) +(assert (forall ((?v0 S2) (?v1 S2)) (=> (not (= ?v0 f18)) (= (f19 f130 (f19 (f30 f63 ?v0) ?v1)) (f19 (f30 f63 (f19 f130 ?v0)) ?v1))))) +(assert (forall ((?v0 S8) (?v1 S13)) (=> (not (= ?v0 f26)) (= (f27 (f131 f132 (f43 f44 (+ (f120 f121 ?v1) 1))) ?v0) (f27 (f28 f29 (f58 f125 ?v0)) (f27 (f131 f132 ?v1) (f27 f128 ?v0))))))) +(assert (forall ((?v0 S5) (?v1 S13)) (=> (not (= ?v0 f22)) (= (f23 (f133 f134 (f43 f44 (+ (f120 f121 ?v1) 1))) ?v0) (f23 (f24 f25 (f56 f126 ?v0)) (f23 (f133 f134 ?v1) (f23 f129 ?v0))))))) +(assert (forall ((?v0 S2) (?v1 S13)) (=> (not (= ?v0 f18)) (= (f19 (f135 f136 (f43 f44 (+ (f120 f121 ?v1) 1))) ?v0) (f19 (f20 f21 (f54 f127 ?v0)) (f19 (f135 f136 ?v1) (f19 f130 ?v0))))))) +(assert (forall ((?v0 S6) (?v1 S8)) (let ((?v_0 (f27 (f137 f138 ?v0) ?v1))) (=> (not (= ?v_0 f26)) (not (= (f6 ?v0 (f58 f125 ?v_0)) f1)))))) +(assert (forall ((?v0 S37) (?v1 S5)) (let ((?v_0 (f23 (f139 f140 ?v0) ?v1))) (=> (not (= ?v_0 f22)) (not (= (f68 ?v0 (f56 f126 ?v_0)) f1)))))) +(assert (forall ((?v0 S36) (?v1 S2)) (let ((?v_0 (f19 (f141 f142 ?v0) ?v1))) (=> (not (= ?v_0 f18)) (not (= (f66 ?v0 (f54 f127 ?v_0)) f1)))))) +(assert (forall ((?v0 S7)) (= (f9 (f10 (f143 ?v0) f26) f26) f1))) +(assert (forall ((?v0 S68)) (= (f6 (f7 (f144 ?v0) f22) f22) f1))) +(assert (forall ((?v0 S69)) (= (f3 (f4 (f145 ?v0) f18) f18) f1))) +(assert (forall ((?v0 S13) (?v1 S18) (?v2 S5)) (let ((?v_0 (f24 f25 ?v1))) (= (f23 (f133 f134 (f43 f44 (+ (f120 f121 ?v0) 1))) (f23 ?v_0 ?v2)) (f23 ?v_0 (f23 (f133 f134 ?v0) ?v2)))))) +(assert (forall ((?v0 S13) (?v1 S5) (?v2 S8)) (let ((?v_0 (f28 f29 ?v1))) (= (f27 (f131 f132 (f43 f44 (+ (f120 f121 ?v0) 1))) (f27 ?v_0 ?v2)) (f27 ?v_0 (f27 (f131 f132 ?v0) ?v2)))))) +(assert (forall ((?v0 S13) (?v1 S15) (?v2 S2)) (let ((?v_0 (f20 f21 ?v1))) (= (f19 (f135 f136 (f43 f44 (+ (f120 f121 ?v0) 1))) (f19 ?v_0 ?v2)) (f19 ?v_0 (f19 (f135 f136 ?v0) ?v2)))))) +(assert (forall ((?v0 S13) (?v1 S8)) (= (= (f27 (f131 f132 ?v0) ?v1) f26) (or (= ?v0 (f43 f44 0)) (= ?v1 f26))))) +(assert (forall ((?v0 S13) (?v1 S5)) (= (= (f23 (f133 f134 ?v0) ?v1) f22) (or (= ?v0 (f43 f44 0)) (= ?v1 f22))))) +(assert (forall ((?v0 S13) (?v1 S2)) (= (= (f19 (f135 f136 ?v0) ?v1) f18) (or (= ?v0 (f43 f44 0)) (= ?v1 f18))))) +(assert (forall ((?v0 S13)) (= (f27 (f131 f132 ?v0) f26) f26))) +(assert (forall ((?v0 S13)) (= (f23 (f133 f134 ?v0) f22) f22))) +(assert (forall ((?v0 S13)) (= (f19 (f135 f136 ?v0) f18) f18))) +(assert (forall ((?v0 S8)) (= (f27 (f131 f132 (f43 f44 0)) ?v0) f26))) +(assert (forall ((?v0 S5)) (= (f23 (f133 f134 (f43 f44 0)) ?v0) f22))) +(assert (forall ((?v0 S2)) (= (f19 (f135 f136 (f43 f44 0)) ?v0) f18))) +(assert (forall ((?v0 S37) (?v1 S18) (?v2 S5)) (let ((?v_0 (f139 f140 ?v0)) (?v_1 (f23 (f24 f25 ?v1) ?v2))) (= (f23 ?v_0 ?v_1) (ite (= (f68 ?v0 ?v1) f1) (f23 ?v_0 ?v2) ?v_1))))) +(assert (forall ((?v0 S6) (?v1 S5) (?v2 S8)) (let ((?v_0 (f137 f138 ?v0)) (?v_1 (f27 (f28 f29 ?v1) ?v2))) (= (f27 ?v_0 ?v_1) (ite (= (f6 ?v0 ?v1) f1) (f27 ?v_0 ?v2) ?v_1))))) +(assert (forall ((?v0 S36) (?v1 S15) (?v2 S2)) (let ((?v_0 (f141 f142 ?v0)) (?v_1 (f19 (f20 f21 ?v1) ?v2))) (= (f19 ?v_0 ?v_1) (ite (= (f66 ?v0 ?v1) f1) (f19 ?v_0 ?v2) ?v_1))))) +(assert (forall ((?v0 S6)) (= (f27 (f137 f138 ?v0) f26) f26))) +(assert (forall ((?v0 S37)) (= (f23 (f139 f140 ?v0) f22) f22))) +(assert (forall ((?v0 S36)) (= (f19 (f141 f142 ?v0) f18) f18))) +(assert (forall ((?v0 S5) (?v1 S8)) (let ((?v_0 (f28 f29 ?v0))) (= (f27 (f131 f132 (f43 f44 1)) (f27 ?v_0 ?v1)) (f27 ?v_0 f26))))) +(assert (forall ((?v0 S18) (?v1 S5)) (let ((?v_0 (f24 f25 ?v0))) (= (f23 (f133 f134 (f43 f44 1)) (f23 ?v_0 ?v1)) (f23 ?v_0 f22))))) +(assert (forall ((?v0 S15) (?v1 S2)) (let ((?v_0 (f20 f21 ?v0))) (= (f19 (f135 f136 (f43 f44 1)) (f19 ?v_0 ?v1)) (f19 ?v_0 f18))))) +(assert (forall ((?v0 S13) (?v1 S5) (?v2 S8)) (let ((?v_0 (f28 f29 ?v1))) (= (f27 (f131 f132 ?v0) (f27 ?v_0 ?v2)) (ite (= ?v0 (f43 f44 0)) f26 (f27 ?v_0 (f27 (f131 f132 (f43 f44 (- (f120 f121 ?v0) 1))) ?v2))))))) +(assert (forall ((?v0 S13) (?v1 S18) (?v2 S5)) (let ((?v_0 (f24 f25 ?v1))) (= (f23 (f133 f134 ?v0) (f23 ?v_0 ?v2)) (ite (= ?v0 (f43 f44 0)) f22 (f23 ?v_0 (f23 (f133 f134 (f43 f44 (- (f120 f121 ?v0) 1))) ?v2))))))) +(assert (forall ((?v0 S13) (?v1 S15) (?v2 S2)) (let ((?v_0 (f20 f21 ?v1))) (= (f19 (f135 f136 ?v0) (f19 ?v_0 ?v2)) (ite (= ?v0 (f43 f44 0)) f18 (f19 ?v_0 (f19 (f135 f136 (f43 f44 (- (f120 f121 ?v0) 1))) ?v2))))))) +(assert (forall ((?v0 S68) (?v1 S18) (?v2 S18) (?v3 S5) (?v4 S5)) (let ((?v_0 (f144 ?v0))) (=> (= (f68 (f146 ?v0 ?v1) ?v2) f1) (=> (= (f6 (f7 ?v_0 ?v3) ?v4) f1) (= (f6 (f7 ?v_0 (f23 (f24 f25 ?v1) ?v3)) (f23 (f24 f25 ?v2) ?v4)) f1)))))) +(assert (forall ((?v0 S7) (?v1 S5) (?v2 S5) (?v3 S8) (?v4 S8)) (let ((?v_0 (f143 ?v0))) (=> (= (f6 (f7 ?v0 ?v1) ?v2) f1) (=> (= (f9 (f10 ?v_0 ?v3) ?v4) f1) (= (f9 (f10 ?v_0 (f27 (f28 f29 ?v1) ?v3)) (f27 (f28 f29 ?v2) ?v4)) f1)))))) +(assert (forall ((?v0 S69) (?v1 S15) (?v2 S15) (?v3 S2) (?v4 S2)) (let ((?v_0 (f145 ?v0))) (=> (= (f66 (f147 ?v0 ?v1) ?v2) f1) (=> (= (f3 (f4 ?v_0 ?v3) ?v4) f1) (= (f3 (f4 ?v_0 (f19 (f20 f21 ?v1) ?v3)) (f19 (f20 f21 ?v2) ?v4)) f1)))))) +(assert (forall ((?v0 S7) (?v1 S8) (?v2 S8)) (= (= (f9 (f10 (f143 ?v0) ?v1) ?v2) f1) (or (and (= ?v1 f26) (= ?v2 f26)) (exists ((?v3 S5) (?v4 S5) (?v5 S8) (?v6 S8)) (and (= ?v1 (f27 (f28 f29 ?v3) ?v5)) (and (= ?v2 (f27 (f28 f29 ?v4) ?v6)) (and (= (f6 (f7 ?v0 ?v3) ?v4) f1) (= (f9 (f10 (f143 ?v0) ?v5) ?v6) f1))))))))) +(assert (forall ((?v0 S68) (?v1 S5) (?v2 S5)) (= (= (f6 (f7 (f144 ?v0) ?v1) ?v2) f1) (or (and (= ?v1 f22) (= ?v2 f22)) (exists ((?v3 S18) (?v4 S18) (?v5 S5) (?v6 S5)) (and (= ?v1 (f23 (f24 f25 ?v3) ?v5)) (and (= ?v2 (f23 (f24 f25 ?v4) ?v6)) (and (= (f68 (f146 ?v0 ?v3) ?v4) f1) (= (f6 (f7 (f144 ?v0) ?v5) ?v6) f1))))))))) +(assert (forall ((?v0 S69) (?v1 S2) (?v2 S2)) (= (= (f3 (f4 (f145 ?v0) ?v1) ?v2) f1) (or (and (= ?v1 f18) (= ?v2 f18)) (exists ((?v3 S15) (?v4 S15) (?v5 S2) (?v6 S2)) (and (= ?v1 (f19 (f20 f21 ?v3) ?v5)) (and (= ?v2 (f19 (f20 f21 ?v4) ?v6)) (and (= (f66 (f147 ?v0 ?v3) ?v4) f1) (= (f3 (f4 (f145 ?v0) ?v5) ?v6) f1))))))))) +(assert (forall ((?v0 S37) (?v1 S5) (?v2 S18) (?v3 S5)) (let ((?v_0 (f23 (f24 f25 ?v2) ?v3))) (= (= (f23 (f139 f140 ?v0) ?v1) ?v_0) (and (= ?v1 (f23 (f32 f64 (f23 (f139 f148 ?v0) ?v1)) ?v_0)) (not (= (f68 ?v0 ?v2) f1))))))) +(assert (forall ((?v0 S6) (?v1 S8) (?v2 S5) (?v3 S8)) (let ((?v_0 (f27 (f28 f29 ?v2) ?v3))) (= (= (f27 (f137 f138 ?v0) ?v1) ?v_0) (and (= ?v1 (f27 (f34 f65 (f27 (f137 f149 ?v0) ?v1)) ?v_0)) (not (= (f6 ?v0 ?v2) f1))))))) +(assert (forall ((?v0 S36) (?v1 S2) (?v2 S15) (?v3 S2)) (let ((?v_0 (f19 (f20 f21 ?v2) ?v3))) (= (= (f19 (f141 f142 ?v0) ?v1) ?v_0) (and (= ?v1 (f19 (f30 f63 (f19 (f141 f150 ?v0) ?v1)) ?v_0)) (not (= (f66 ?v0 ?v2) f1))))))) +(assert (forall ((?v0 Int) (?v1 S5) (?v2 S8)) (let ((?v_0 (f43 f44 (f151 f152 ?v0))) (?v_1 (f28 f29 ?v1))) (= (f27 (f131 f132 ?v_0) (f27 ?v_1 ?v2)) (ite (= ?v_0 (f43 f44 0)) f26 (f27 ?v_1 (f27 (f131 f132 (f43 f44 (- (f120 f121 (f43 f153 ?v0)) 1))) ?v2))))))) +(assert (forall ((?v0 Int) (?v1 S18) (?v2 S5)) (let ((?v_0 (f43 f44 (f151 f152 ?v0))) (?v_1 (f24 f25 ?v1))) (= (f23 (f133 f134 ?v_0) (f23 ?v_1 ?v2)) (ite (= ?v_0 (f43 f44 0)) f22 (f23 ?v_1 (f23 (f133 f134 (f43 f44 (- (f120 f121 (f43 f153 ?v0)) 1))) ?v2))))))) +(assert (forall ((?v0 Int) (?v1 S15) (?v2 S2)) (let ((?v_0 (f43 f44 (f151 f152 ?v0))) (?v_1 (f20 f21 ?v1))) (= (f19 (f135 f136 ?v_0) (f19 ?v_1 ?v2)) (ite (= ?v_0 (f43 f44 0)) f18 (f19 ?v_1 (f19 (f135 f136 (f43 f44 (- (f120 f121 (f43 f153 ?v0)) 1))) ?v2))))))) +(assert (forall ((?v0 S6)) (= (f27 (f137 f149 ?v0) f26) f26))) +(assert (forall ((?v0 S37)) (= (f23 (f139 f148 ?v0) f22) f22))) +(assert (forall ((?v0 S36)) (= (f19 (f141 f150 ?v0) f18) f18))) +(assert (forall ((?v0 S6) (?v1 S5) (?v2 S8)) (let ((?v_1 (f137 f149 ?v0)) (?v_0 (f28 f29 ?v1))) (= (f27 ?v_1 (f27 ?v_0 ?v2)) (ite (= (f6 ?v0 ?v1) f1) (f27 ?v_0 (f27 ?v_1 ?v2)) f26))))) +(assert (forall ((?v0 S37) (?v1 S18) (?v2 S5)) (let ((?v_1 (f139 f148 ?v0)) (?v_0 (f24 f25 ?v1))) (= (f23 ?v_1 (f23 ?v_0 ?v2)) (ite (= (f68 ?v0 ?v1) f1) (f23 ?v_0 (f23 ?v_1 ?v2)) f22))))) +(assert (forall ((?v0 S36) (?v1 S15) (?v2 S2)) (let ((?v_1 (f141 f150 ?v0)) (?v_0 (f20 f21 ?v1))) (= (f19 ?v_1 (f19 ?v_0 ?v2)) (ite (= (f66 ?v0 ?v1) f1) (f19 ?v_0 (f19 ?v_1 ?v2)) f18))))) +(assert (forall ((?v0 S37) (?v1 S18) (?v2 S5) (?v3 S5)) (let ((?v_0 (f139 f148 ?v0))) (=> (not (= (f68 ?v0 ?v1) f1)) (= (f23 ?v_0 (f23 (f32 f64 ?v2) (f23 (f24 f25 ?v1) ?v3))) (f23 ?v_0 ?v2)))))) +(assert (forall ((?v0 S6) (?v1 S5) (?v2 S8) (?v3 S8)) (let ((?v_0 (f137 f149 ?v0))) (=> (not (= (f6 ?v0 ?v1) f1)) (= (f27 ?v_0 (f27 (f34 f65 ?v2) (f27 (f28 f29 ?v1) ?v3))) (f27 ?v_0 ?v2)))))) +(assert (forall ((?v0 S36) (?v1 S15) (?v2 S2) (?v3 S2)) (let ((?v_0 (f141 f150 ?v0))) (=> (not (= (f66 ?v0 ?v1) f1)) (= (f19 ?v_0 (f19 (f30 f63 ?v2) (f19 (f20 f21 ?v1) ?v3))) (f19 ?v_0 ?v2)))))) +(assert (forall ((?v0 Int)) (let ((?v_0 (f120 f121 (f43 f153 ?v0)))) (=> (< 0 ?v_0) (= (f43 f44 (f151 f152 ?v0)) (f43 f44 (+ (f120 f121 (f43 f44 (- ?v_0 1))) 1))))))) +(assert (forall ((?v0 Int) (?v1 Int)) (= (= (f151 f152 ?v0) (f151 f152 ?v1)) (= ?v0 ?v1)))) +(assert (forall ((?v0 Int) (?v1 S13)) (let ((?v_0 (f43 f153 ?v0))) (= (= ?v_0 ?v1) (= ?v1 ?v_0))))) +(assert (forall ((?v0 Int) (?v1 Int)) (let ((?v_0 (f151 f152 ?v0))) (= (= ?v_0 ?v1) (= ?v1 ?v_0))))) +(assert (forall ((?v0 Int)) (let ((?v_0 (f43 f44 (f151 f152 ?v0)))) (= ?v_0 ?v_0)))) +(assert (forall ((?v0 Int)) (let ((?v_0 (f43 f44 (f151 f152 ?v0)))) (= ?v_0 ?v_0)))) +(assert (forall ((?v0 S13) (?v1 S13)) (= (= (f154 ?v0) (f154 ?v1)) (= ?v0 ?v1)))) +(assert (forall ((?v0 S13) (?v1 S8)) (let ((?v_0 (f120 f121 ?v0))) (=> (< ?v_0 (f120 f121 (f155 f156 ?v1))) (= (f27 (f34 f65 (f27 (f131 f132 ?v0) ?v1)) (f27 (f28 f29 (f58 f125 (f27 (f131 f157 ?v0) ?v1))) f26)) (f27 (f131 f132 (f43 f44 (+ ?v_0 1))) ?v1)))))) +(assert (forall ((?v0 S13) (?v1 S5)) (let ((?v_0 (f120 f121 ?v0))) (=> (< ?v_0 (f120 f121 (f158 f159 ?v1))) (= (f23 (f32 f64 (f23 (f133 f134 ?v0) ?v1)) (f23 (f24 f25 (f56 f126 (f23 (f133 f160 ?v0) ?v1))) f22)) (f23 (f133 f134 (f43 f44 (+ ?v_0 1))) ?v1)))))) +(assert (forall ((?v0 S13) (?v1 S2)) (let ((?v_0 (f120 f121 ?v0))) (=> (< ?v_0 (f120 f121 (f161 f162 ?v1))) (= (f19 (f30 f63 (f19 (f135 f136 ?v0) ?v1)) (f19 (f20 f21 (f54 f127 (f19 (f135 f163 ?v0) ?v1))) f18)) (f19 (f135 f136 (f43 f44 (+ ?v_0 1))) ?v1)))))) +(assert (forall ((?v0 S8)) (= (f48 (f49 f50 ?v0) f164) f26))) +(assert (forall ((?v0 S5)) (= (f45 (f46 f47 ?v0) f164) f22))) +(assert (forall ((?v0 S2)) (= (f39 (f40 f41 ?v0) f164) f18))) +(assert (forall ((?v0 Int) (?v1 Int)) (= (= (f12 (f13 f112 (f151 f152 ?v0)) (f151 f152 ?v1)) f1) (= (f12 (f13 f112 ?v0) ?v1) f1)))) +(assert (forall ((?v0 S13) (?v1 Int)) (let ((?v_0 (f151 f152 ?v1))) (= (= (f120 f121 ?v0) ?v_0) (and (= ?v0 (f43 f44 ?v_0)) (<= 0 ?v_0)))))) +(assert (forall ((?v0 Int) (?v1 Int)) (= (<= (f151 f152 ?v0) (f151 f152 ?v1)) (<= ?v0 ?v1)))) +(assert (forall ((?v0 Int) (?v1 Int)) (= (< (f151 f152 ?v0) (f151 f152 ?v1)) (< ?v0 ?v1)))) +(assert (forall ((?v0 Int) (?v1 Int)) (= (- (f151 f152 ?v0) (f151 f152 ?v1)) (f151 f152 (+ ?v0 (- ?v1)))))) +(assert (forall ((?v0 Int) (?v1 Int)) (= (* (f151 f152 ?v0) (f151 f152 ?v1)) (f151 f152 (* ?v0 ?v1))))) +(assert (forall ((?v0 Int) (?v1 Int)) (= (+ (f151 f152 ?v0) (f151 f152 ?v1)) (f151 f152 (+ ?v0 ?v1))))) +(assert (forall ((?v0 Int)) (= (- (f151 f152 ?v0)) (f151 f152 (- ?v0))))) +(assert (forall ((?v0 Int)) (= (f151 f152 ?v0) ?v0))) +(assert (= (f154 (f43 f44 0)) f164)) +(assert (forall ((?v0 S18) (?v1 S5)) (= (f158 f159 (f23 (f24 f25 ?v0) ?v1)) (f43 f44 (+ (f120 f121 (f158 f159 ?v1)) (+ 0 1)))))) +(assert (forall ((?v0 S5) (?v1 S8)) (= (f155 f156 (f27 (f28 f29 ?v0) ?v1)) (f43 f44 (+ (f120 f121 (f155 f156 ?v1)) (+ 0 1)))))) +(assert (forall ((?v0 S15) (?v1 S2)) (= (f161 f162 (f19 (f20 f21 ?v0) ?v1)) (f43 f44 (+ (f120 f121 (f161 f162 ?v1)) (+ 0 1)))))) +(assert (forall ((?v0 S5) (?v1 S5) (?v2 S18)) (=> (<= (f120 f121 (f158 f159 ?v0)) (f120 f121 (f158 f159 ?v1))) (= (= ?v0 (f23 (f24 f25 ?v2) ?v1)) false)))) +(assert (forall ((?v0 S8) (?v1 S8) (?v2 S5)) (=> (<= (f120 f121 (f155 f156 ?v0)) (f120 f121 (f155 f156 ?v1))) (= (= ?v0 (f27 (f28 f29 ?v2) ?v1)) false)))) +(assert (forall ((?v0 S2) (?v1 S2) (?v2 S15)) (=> (<= (f120 f121 (f161 f162 ?v0)) (f120 f121 (f161 f162 ?v1))) (= (= ?v0 (f19 (f20 f21 ?v2) ?v1)) false)))) +(assert (= (f155 f156 f26) (f43 f44 0))) +(assert (= (f158 f159 f22) (f43 f44 0))) +(assert (= (f161 f162 f18) (f43 f44 0))) +(assert (forall ((?v0 S8)) (= (< 0 (f120 f121 (f155 f156 ?v0))) (not (= ?v0 f26))))) +(assert (forall ((?v0 S5)) (= (< 0 (f120 f121 (f158 f159 ?v0))) (not (= ?v0 f22))))) +(assert (forall ((?v0 S2)) (= (< 0 (f120 f121 (f161 f162 ?v0))) (not (= ?v0 f18))))) +(assert (forall ((?v0 S8)) (= (= (f155 f156 ?v0) (f43 f44 0)) (= ?v0 f26)))) +(assert (forall ((?v0 S5)) (= (= (f158 f159 ?v0) (f43 f44 0)) (= ?v0 f22)))) +(assert (forall ((?v0 S2)) (= (= (f161 f162 ?v0) (f43 f44 0)) (= ?v0 f18)))) +(assert (forall ((?v0 S18) (?v1 S5)) (= (f23 (f133 f160 (f43 f44 1)) (f23 (f24 f25 ?v0) ?v1)) ?v1))) +(assert (forall ((?v0 S5) (?v1 S8)) (= (f27 (f131 f157 (f43 f44 1)) (f27 (f28 f29 ?v0) ?v1)) ?v1))) +(assert (forall ((?v0 S15) (?v1 S2)) (= (f19 (f135 f163 (f43 f44 1)) (f19 (f20 f21 ?v0) ?v1)) ?v1))) +(assert (forall ((?v0 S13) (?v1 S18) (?v2 S5)) (let ((?v_0 (f23 (f24 f25 ?v1) ?v2))) (= (f23 (f133 f160 ?v0) ?v_0) (ite (= ?v0 (f43 f44 0)) ?v_0 (f23 (f133 f160 (f43 f44 (- (f120 f121 ?v0) 1))) ?v2)))))) +(assert (forall ((?v0 S13) (?v1 S5) (?v2 S8)) (let ((?v_0 (f27 (f28 f29 ?v1) ?v2))) (= (f27 (f131 f157 ?v0) ?v_0) (ite (= ?v0 (f43 f44 0)) ?v_0 (f27 (f131 f157 (f43 f44 (- (f120 f121 ?v0) 1))) ?v2)))))) +(assert (forall ((?v0 S13) (?v1 S15) (?v2 S2)) (let ((?v_0 (f19 (f20 f21 ?v1) ?v2))) (= (f19 (f135 f163 ?v0) ?v_0) (ite (= ?v0 (f43 f44 0)) ?v_0 (f19 (f135 f163 (f43 f44 (- (f120 f121 ?v0) 1))) ?v2)))))) +(assert (forall ((?v0 S13) (?v1 S18) (?v2 S5)) (= (f23 (f133 f160 (f43 f44 (+ (f120 f121 ?v0) 1))) (f23 (f24 f25 ?v1) ?v2)) (f23 (f133 f160 ?v0) ?v2)))) +(assert (forall ((?v0 S13) (?v1 S5) (?v2 S8)) (= (f27 (f131 f157 (f43 f44 (+ (f120 f121 ?v0) 1))) (f27 (f28 f29 ?v1) ?v2)) (f27 (f131 f157 ?v0) ?v2)))) +(assert (forall ((?v0 S13) (?v1 S15) (?v2 S2)) (= (f19 (f135 f163 (f43 f44 (+ (f120 f121 ?v0) 1))) (f19 (f20 f21 ?v1) ?v2)) (f19 (f135 f163 ?v0) ?v2)))) +(assert (forall ((?v0 S13)) (= (f27 (f131 f157 ?v0) f26) f26))) +(assert (forall ((?v0 S13)) (= (f23 (f133 f160 ?v0) f22) f22))) +(assert (forall ((?v0 S13)) (= (f19 (f135 f163 ?v0) f18) f18))) +(assert (forall ((?v0 S8) (?v1 S13)) (=> (<= (f120 f121 (f155 f156 ?v0)) (f120 f121 ?v1)) (= (f27 (f131 f157 ?v1) ?v0) f26)))) +(assert (forall ((?v0 S5) (?v1 S13)) (=> (<= (f120 f121 (f158 f159 ?v0)) (f120 f121 ?v1)) (= (f23 (f133 f160 ?v1) ?v0) f22)))) +(assert (forall ((?v0 S2) (?v1 S13)) (=> (<= (f120 f121 (f161 f162 ?v0)) (f120 f121 ?v1)) (= (f19 (f135 f163 ?v1) ?v0) f18)))) +(assert (forall ((?v0 S13) (?v1 S8)) (= (= (f27 (f131 f157 ?v0) ?v1) f26) (<= (f120 f121 (f155 f156 ?v1)) (f120 f121 ?v0))))) +(assert (forall ((?v0 S13) (?v1 S5)) (= (= (f23 (f133 f160 ?v0) ?v1) f22) (<= (f120 f121 (f158 f159 ?v1)) (f120 f121 ?v0))))) +(assert (forall ((?v0 S13) (?v1 S2)) (= (= (f19 (f135 f163 ?v0) ?v1) f18) (<= (f120 f121 (f161 f162 ?v1)) (f120 f121 ?v0))))) +(assert (forall ((?v0 Int) (?v1 S18) (?v2 S5)) (let ((?v_0 (f43 f44 (f151 f152 ?v0))) (?v_1 (f23 (f24 f25 ?v1) ?v2))) (= (f23 (f133 f160 ?v_0) ?v_1) (ite (= ?v_0 (f43 f44 0)) ?v_1 (f23 (f133 f160 (f43 f44 (- (f120 f121 (f43 f153 ?v0)) 1))) ?v2)))))) +(assert (forall ((?v0 Int) (?v1 S5) (?v2 S8)) (let ((?v_0 (f43 f44 (f151 f152 ?v0))) (?v_1 (f27 (f28 f29 ?v1) ?v2))) (= (f27 (f131 f157 ?v_0) ?v_1) (ite (= ?v_0 (f43 f44 0)) ?v_1 (f27 (f131 f157 (f43 f44 (- (f120 f121 (f43 f153 ?v0)) 1))) ?v2)))))) +(assert (forall ((?v0 Int) (?v1 S15) (?v2 S2)) (let ((?v_0 (f43 f44 (f151 f152 ?v0))) (?v_1 (f19 (f20 f21 ?v1) ?v2))) (= (f19 (f135 f163 ?v_0) ?v_1) (ite (= ?v_0 (f43 f44 0)) ?v_1 (f19 (f135 f163 (f43 f44 (- (f120 f121 (f43 f153 ?v0)) 1))) ?v2)))))) +(assert (forall ((?v0 S13)) (=> (= (f42 ?v0 f164) f1) false))) +(assert (forall ((?v0 S13) (?v1 S5)) (= (= (f43 f44 (+ (f120 f121 ?v0) 1)) (f158 f159 ?v1)) (exists ((?v2 S18) (?v3 S5)) (and (= ?v1 (f23 (f24 f25 ?v2) ?v3)) (= (f158 f159 ?v3) ?v0)))))) +(assert (forall ((?v0 S13) (?v1 S8)) (= (= (f43 f44 (+ (f120 f121 ?v0) 1)) (f155 f156 ?v1)) (exists ((?v2 S5) (?v3 S8)) (and (= ?v1 (f27 (f28 f29 ?v2) ?v3)) (= (f155 f156 ?v3) ?v0)))))) +(assert (forall ((?v0 S13) (?v1 S2)) (= (= (f43 f44 (+ (f120 f121 ?v0) 1)) (f161 f162 ?v1)) (exists ((?v2 S15) (?v3 S2)) (and (= ?v1 (f19 (f20 f21 ?v2) ?v3)) (= (f161 f162 ?v3) ?v0)))))) +(assert (forall ((?v0 Int) (?v1 Int)) (= (= (f12 (f13 f112 ?v0) ?v1) f1) (= (- ?v0 ?v1) 0)))) +(assert (forall ((?v0 Int)) (= (= (f12 (f13 f112 ?v0) ?v0) f1) true))) +(assert (= f164 (f113 f16))) +(assert (forall ((?v0 S14)) (= (forall ((?v1 S13)) (not (= (f42 ?v1 ?v0) f1))) (= ?v0 f164)))) +(assert (forall ((?v0 S14)) (= (exists ((?v1 S13)) (= (f42 ?v1 ?v0) f1)) (not (= ?v0 f164))))) +(assert (forall ((?v0 S14)) (= (exists ((?v1 S13)) (and (= (f42 ?v1 f164) f1) (= (f15 ?v0 ?v1) f1))) false))) +(assert (forall ((?v0 S14)) (= (forall ((?v1 S13)) (=> (= (f42 ?v1 f164) f1) (= (f15 ?v0 ?v1) f1))) true))) +(assert (forall ((?v0 S14)) (= (= f164 (f113 ?v0)) (forall ((?v1 S13)) (not (= (f15 ?v0 ?v1) f1)))))) +(assert (forall ((?v0 S13)) (= (= (f42 ?v0 f164) f1) false))) +(assert (forall ((?v0 S14)) (= (= (f113 ?v0) f164) (forall ((?v1 S13)) (not (= (f15 ?v0 ?v1) f1)))))) +(assert (forall ((?v0 S14) (?v1 S13)) (=> (= ?v0 f164) (not (= (f42 ?v1 ?v0) f1))))) +(assert (forall ((?v0 S5) (?v1 S13)) (= (= (f158 f159 ?v0) (f43 f44 (+ (f120 f121 ?v1) 1))) (exists ((?v2 S18) (?v3 S5)) (and (= ?v0 (f23 (f24 f25 ?v2) ?v3)) (= (f158 f159 ?v3) ?v1)))))) +(assert (forall ((?v0 S8) (?v1 S13)) (= (= (f155 f156 ?v0) (f43 f44 (+ (f120 f121 ?v1) 1))) (exists ((?v2 S5) (?v3 S8)) (and (= ?v0 (f27 (f28 f29 ?v2) ?v3)) (= (f155 f156 ?v3) ?v1)))))) +(assert (forall ((?v0 S2) (?v1 S13)) (= (= (f161 f162 ?v0) (f43 f44 (+ (f120 f121 ?v1) 1))) (exists ((?v2 S15) (?v3 S2)) (and (= ?v0 (f19 (f20 f21 ?v2) ?v3)) (= (f161 f162 ?v3) ?v1)))))) +(assert (forall ((?v0 S13)) (= (= (f15 f164 ?v0) f1) (= f165 f1)))) +(assert (forall ((?v0 S13)) (= (= (f15 f164 ?v0) f1) (= f165 f1)))) +(assert (forall ((?v0 S13) (?v1 S5) (?v2 S18)) (let ((?v_0 (f120 f121 ?v0))) (=> (< ?v_0 (f120 f121 (f158 f159 ?v1))) (= (f102 (f116 (f166 f167 ?v1) ?v0) ?v2) (f23 (f32 f64 (f23 (f133 f134 ?v0) ?v1)) (f23 (f24 f25 ?v2) (f23 (f133 f160 (f43 f44 (+ ?v_0 1))) ?v1)))))))) +(assert (forall ((?v0 S13) (?v1 S8) (?v2 S5)) (let ((?v_0 (f120 f121 ?v0))) (=> (< ?v_0 (f120 f121 (f155 f156 ?v1))) (= (f95 (f114 (f168 f169 ?v1) ?v0) ?v2) (f27 (f34 f65 (f27 (f131 f132 ?v0) ?v1)) (f27 (f28 f29 ?v2) (f27 (f131 f157 (f43 f44 (+ ?v_0 1))) ?v1)))))))) +(assert (forall ((?v0 S13) (?v1 S2) (?v2 S15)) (let ((?v_0 (f120 f121 ?v0))) (=> (< ?v_0 (f120 f121 (f161 f162 ?v1))) (= (f90 (f118 (f170 f171 ?v1) ?v0) ?v2) (f19 (f30 f63 (f19 (f135 f136 ?v0) ?v1)) (f19 (f20 f21 ?v2) (f19 (f135 f163 (f43 f44 (+ ?v_0 1))) ?v1)))))))) +(assert (forall ((?v0 S13) (?v1 S5)) (let ((?v_0 (f120 f121 ?v0))) (=> (< ?v_0 (f120 f121 (f158 f159 ?v1))) (= ?v1 (f23 (f32 f64 (f23 (f133 f134 ?v0) ?v1)) (f23 (f24 f25 (f172 (f173 f174 ?v1) ?v0)) (f23 (f133 f160 (f43 f44 (+ ?v_0 1))) ?v1)))))))) +(assert (forall ((?v0 S13) (?v1 S8)) (let ((?v_0 (f120 f121 ?v0))) (=> (< ?v_0 (f120 f121 (f155 f156 ?v1))) (= ?v1 (f27 (f34 f65 (f27 (f131 f132 ?v0) ?v1)) (f27 (f28 f29 (f175 (f176 f177 ?v1) ?v0)) (f27 (f131 f157 (f43 f44 (+ ?v_0 1))) ?v1)))))))) +(assert (forall ((?v0 S13) (?v1 S2)) (let ((?v_0 (f120 f121 ?v0))) (=> (< ?v_0 (f120 f121 (f161 f162 ?v1))) (= ?v1 (f19 (f30 f63 (f19 (f135 f136 ?v0) ?v1)) (f19 (f20 f21 (f178 (f179 f180 ?v1) ?v0)) (f19 (f135 f163 (f43 f44 (+ ?v_0 1))) ?v1)))))))) +(assert (forall ((?v0 S5) (?v1 S18) (?v2 S5)) (= (f172 (f173 f174 (f23 (f32 f64 ?v0) (f23 (f24 f25 ?v1) ?v2))) (f158 f159 ?v0)) ?v1))) +(assert (forall ((?v0 S8) (?v1 S5) (?v2 S8)) (= (f175 (f176 f177 (f27 (f34 f65 ?v0) (f27 (f28 f29 ?v1) ?v2))) (f155 f156 ?v0)) ?v1))) +(assert (forall ((?v0 S2) (?v1 S15) (?v2 S2)) (= (f178 (f179 f180 (f19 (f30 f63 ?v0) (f19 (f20 f21 ?v1) ?v2))) (f161 f162 ?v0)) ?v1))) +(assert (forall ((?v0 S13) (?v1 S5)) (let ((?v_0 (f120 f121 ?v0))) (=> (< ?v_0 (f120 f121 (f158 f159 ?v1))) (= (f23 (f24 f25 (f172 (f173 f174 ?v1) ?v0)) (f23 (f133 f160 (f43 f44 (+ ?v_0 1))) ?v1)) (f23 (f133 f160 ?v0) ?v1)))))) +(assert (forall ((?v0 S13) (?v1 S8)) (let ((?v_0 (f120 f121 ?v0))) (=> (< ?v_0 (f120 f121 (f155 f156 ?v1))) (= (f27 (f28 f29 (f175 (f176 f177 ?v1) ?v0)) (f27 (f131 f157 (f43 f44 (+ ?v_0 1))) ?v1)) (f27 (f131 f157 ?v0) ?v1)))))) +(assert (forall ((?v0 S13) (?v1 S2)) (let ((?v_0 (f120 f121 ?v0))) (=> (< ?v_0 (f120 f121 (f161 f162 ?v1))) (= (f19 (f20 f21 (f178 (f179 f180 ?v1) ?v0)) (f19 (f135 f163 (f43 f44 (+ ?v_0 1))) ?v1)) (f19 (f135 f163 ?v0) ?v1)))))) +(assert (forall ((?v0 S8)) (=> (not (= ?v0 f26)) (= (f58 f59 ?v0) (f175 (f176 f177 ?v0) (f43 f44 (- (f120 f121 (f155 f156 ?v0)) 1))))))) +(assert (forall ((?v0 S5)) (=> (not (= ?v0 f22)) (= (f56 f57 ?v0) (f172 (f173 f174 ?v0) (f43 f44 (- (f120 f121 (f158 f159 ?v0)) 1))))))) +(assert (forall ((?v0 S2)) (=> (not (= ?v0 f18)) (= (f54 f55 ?v0) (f178 (f179 f180 ?v0) (f43 f44 (- (f120 f121 (f161 f162 ?v0)) 1))))))) +(assert (forall ((?v0 S13) (?v1 S18) (?v2 S5)) (let ((?v_0 (f120 f121 ?v0))) (=> (< 0 ?v_0) (= (f172 (f173 f174 (f23 (f24 f25 ?v1) ?v2)) ?v0) (f172 (f173 f174 ?v2) (f43 f44 (- ?v_0 1)))))))) +(assert (forall ((?v0 S13) (?v1 S5) (?v2 S8)) (let ((?v_0 (f120 f121 ?v0))) (=> (< 0 ?v_0) (= (f175 (f176 f177 (f27 (f28 f29 ?v1) ?v2)) ?v0) (f175 (f176 f177 ?v2) (f43 f44 (- ?v_0 1)))))))) +(assert (forall ((?v0 S13) (?v1 S15) (?v2 S2)) (let ((?v_0 (f120 f121 ?v0))) (=> (< 0 ?v_0) (= (f178 (f179 f180 (f19 (f20 f21 ?v1) ?v2)) ?v0) (f178 (f179 f180 ?v2) (f43 f44 (- ?v_0 1)))))))) +(assert (forall ((?v0 S18) (?v1 S5) (?v2 S13)) (= (f172 (f173 f174 (f23 (f24 f25 ?v0) ?v1)) (f43 f44 (+ (f120 f121 ?v2) 1))) (f172 (f173 f174 ?v1) ?v2)))) +(assert (forall ((?v0 S5) (?v1 S8) (?v2 S13)) (= (f175 (f176 f177 (f27 (f28 f29 ?v0) ?v1)) (f43 f44 (+ (f120 f121 ?v2) 1))) (f175 (f176 f177 ?v1) ?v2)))) +(assert (forall ((?v0 S15) (?v1 S2) (?v2 S13)) (= (f178 (f179 f180 (f19 (f20 f21 ?v0) ?v1)) (f43 f44 (+ (f120 f121 ?v2) 1))) (f178 (f179 f180 ?v1) ?v2)))) +(assert (forall ((?v0 S18) (?v1 S5) (?v2 S13)) (= (f172 (f173 f174 (f23 (f24 f25 ?v0) ?v1)) ?v2) (ite (= ?v2 (f43 f44 0)) ?v0 (f172 (f173 f174 ?v1) (f43 f44 (- (f120 f121 ?v2) 1))))))) +(assert (forall ((?v0 S5) (?v1 S8) (?v2 S13)) (= (f175 (f176 f177 (f27 (f28 f29 ?v0) ?v1)) ?v2) (ite (= ?v2 (f43 f44 0)) ?v0 (f175 (f176 f177 ?v1) (f43 f44 (- (f120 f121 ?v2) 1))))))) +(assert (forall ((?v0 S15) (?v1 S2) (?v2 S13)) (= (f178 (f179 f180 (f19 (f20 f21 ?v0) ?v1)) ?v2) (ite (= ?v2 (f43 f44 0)) ?v0 (f178 (f179 f180 ?v1) (f43 f44 (- (f120 f121 ?v2) 1))))))) +(assert (forall ((?v0 S18) (?v1 S5)) (= (f172 (f173 f174 (f23 (f24 f25 ?v0) ?v1)) (f43 f44 0)) ?v0))) +(assert (forall ((?v0 S5) (?v1 S8)) (= (f175 (f176 f177 (f27 (f28 f29 ?v0) ?v1)) (f43 f44 0)) ?v0))) +(assert (forall ((?v0 S15) (?v1 S2)) (= (f178 (f179 f180 (f19 (f20 f21 ?v0) ?v1)) (f43 f44 0)) ?v0))) +(assert (forall ((?v0 S13)) (= (f43 f44 (f120 f121 ?v0)) ?v0))) +(assert (forall ((?v0 Int)) (=> (<= 0 ?v0) (= (f120 f121 (f43 f44 ?v0)) ?v0)))) +(assert (forall ((?v0 Int)) (=> (< ?v0 0) (= (f120 f121 (f43 f44 ?v0)) 0)))) +(check-sat) +(exit) |