Fixes for relational triggers (#2967)

4 files changed, 774 insertions, 1 deletions

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/seu169+1.smt2 b/test/regress/regress1/quantifiers/seu169+1.smt2
new file mode 100644
index 000000000..c7fb6cb27
--- /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)
+(meta-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)