--- a/src/HOL/SMT_Examples/SMT_Examples.certs Sun Dec 19 18:54:29 2010 +0100
+++ b/src/HOL/SMT_Examples/SMT_Examples.certs Sun Dec 19 18:55:21 2010 +0100
@@ -146,7 +146,65 @@
#74 := [and-elim #72]: #43
[mp #74 #88]: false
unsat
-b369848437710a3b368c375ee857c21adc3f6e30 1 0
+bc6de36d6c86b416e91711bb23067cc8250ac153 59 0
+#2 := false
+decl f1 :: S1
+#4 := f1
+decl f6 :: S1
+#15 := f6
+#16 := (= f6 f1)
+decl f5 :: S1
+#13 := f5
+#14 := (= f5 f1)
+#17 := (and #14 #16)
+decl f4 :: S1
+#10 := f4
+#11 := (= f4 f1)
+decl f3 :: S1
+#8 := f3
+#9 := (= f3 f1)
+#12 := (and #9 #11)
+#18 := (or #12 #17)
+#19 := (implies #18 #18)
+#20 := (not #19)
+#74 := (iff #20 false)
+#1 := true
+#69 := (not true)
+#72 := (iff #69 false)
+#73 := [rewrite]: #72
+#70 := (iff #20 #69)
+#67 := (iff #19 true)
+#53 := (= f1 f6)
+#50 := (= f1 f5)
+#56 := (and #50 #53)
+#44 := (= f1 f4)
+#41 := (= f1 f3)
+#47 := (and #41 #44)
+#59 := (or #47 #56)
+#62 := (implies #59 #59)
+#65 := (iff #62 true)
+#66 := [rewrite]: #65
+#63 := (iff #19 #62)
+#60 := (iff #18 #59)
+#57 := (iff #17 #56)
+#54 := (iff #16 #53)
+#55 := [rewrite]: #54
+#51 := (iff #14 #50)
+#52 := [rewrite]: #51
+#58 := [monotonicity #52 #55]: #57
+#48 := (iff #12 #47)
+#45 := (iff #11 #44)
+#46 := [rewrite]: #45
+#42 := (iff #9 #41)
+#43 := [rewrite]: #42
+#49 := [monotonicity #43 #46]: #48
+#61 := [monotonicity #49 #58]: #60
+#64 := [monotonicity #61 #61]: #63
+#68 := [trans #64 #66]: #67
+#71 := [monotonicity #68]: #70
+#75 := [trans #71 #73]: #74
+#40 := [asserted]: #20
+[mp #40 #75]: false
unsat
e334e079d0f61721e404e4ca140ce40c317189ba 94 0
#2 := false
@@ -3973,59 +4031,48 @@
#241 := [unit-resolution #190 #240]: #156
[th-lemma arith farkas -1 -1 1 1 #241 #218 #128 #239]: false
unsat
-a63737c6fce2a605078af85686032a125631e608 53 0
+c722596cfa285e209992f7087932c1ec15fd226b 42 0
#2 := false
decl f3 :: (-> S1 S2)
+decl f1 :: S1
+#4 := f1
+#13 := (f3 f1)
decl f2 :: S1
#5 := f2
-decl f1 :: S1
-#4 := f1
-#1 := true
-#13 := (ite true f1 f2)
-#14 := (f3 #13)
#9 := 3::Int
#8 := 2::Int
#10 := (< 2::Int 3::Int)
#11 := (ite #10 f1 f2)
#12 := (f3 #11)
-#15 := (= #12 #14)
-#16 := (not #15)
-#69 := (iff #16 false)
-#39 := (f3 f1)
-#42 := (= #12 #39)
-#45 := (not #42)
-#67 := (iff #45 false)
-#62 := (not true)
-#65 := (iff #62 false)
-#66 := [rewrite]: #65
-#63 := (iff #45 #62)
-#60 := (iff #42 true)
-#55 := (= #39 #39)
-#58 := (iff #55 true)
+#14 := (= #12 #13)
+#15 := (not #14)
+#60 := (iff #15 false)
+#1 := true
+#55 := (not true)
+#58 := (iff #55 false)
#59 := [rewrite]: #58
-#56 := (iff #42 #55)
-#52 := (= #11 f1)
-#37 := (= #13 f1)
-#38 := [rewrite]: #37
-#50 := (= #11 #13)
-#48 := (iff #10 true)
-#49 := [rewrite]: #48
-#51 := [monotonicity #49]: #50
-#53 := [trans #51 #38]: #52
-#54 := [monotonicity #53]: #42
+#56 := (iff #15 #55)
+#53 := (iff #14 true)
+#48 := (= #13 #13)
+#51 := (iff #48 true)
+#52 := [rewrite]: #51
+#49 := (iff #14 #48)
+#45 := (= #11 f1)
+#40 := (ite true f1 f2)
+#43 := (= #40 f1)
+#44 := [rewrite]: #43
+#41 := (= #11 #40)
+#38 := (iff #10 true)
+#39 := [rewrite]: #38
+#42 := [monotonicity #39]: #41
+#46 := [trans #42 #44]: #45
+#47 := [monotonicity #46]: #14
+#50 := [monotonicity #47]: #49
+#54 := [trans #50 #52]: #53
#57 := [monotonicity #54]: #56
#61 := [trans #57 #59]: #60
-#64 := [monotonicity #61]: #63
-#68 := [trans #64 #66]: #67
-#46 := (iff #16 #45)
-#43 := (iff #15 #42)
-#40 := (= #14 #39)
-#41 := [monotonicity #38]: #40
-#44 := [monotonicity #41]: #43
-#47 := [monotonicity #44]: #46
-#70 := [trans #47 #68]: #69
-#36 := [asserted]: #16
-[mp #36 #70]: false
+#35 := [asserted]: #15
+[mp #35 #61]: false
unsat
4d8a8a08b49cb28d987bdc1bcdbb3a144907bf45 54 0
#2 := false
@@ -4288,7 +4335,7 @@
#42 := [asserted]: #22
[mp #42 #79]: false
unsat
-900d439115908f4ef5998166e284e3a309f354ef 104 0
+78003574b5d95d4c28641909502b0f435784ad24 104 0
#2 := false
decl f1 :: S1
#4 := f1
@@ -7376,698 +7423,425 @@
#37 := [asserted]: #17
[mp #37 #73]: false
unsat
-75da1862a2fd162477f9d85292ff8ab2e18559e4 342 0
+f9ae47f5aef750f37ea2d9309845d7cf08946d8c 211 0
#2 := false
-#21 := 0::Int
+#12 := 0::Int
decl f3 :: Int
#8 := f3
-#419 := (<= f3 0::Int)
-#446 := (>= f3 0::Int)
-#753 := (not #446)
-#409 := (not #419)
-#754 := (or #409 #753)
-#715 := (not #754)
-#11 := 2::Int
-#443 := (mod f3 2::Int)
-#113 := -1::Int
-#444 := (* -1::Int #443)
-decl f4 :: (-> Int Int Int)
-#12 := (f4 f3 2::Int)
-#445 := (+ #12 #444)
-#442 := (= #445 0::Int)
-#705 := (not #442)
-#717 := (>= #445 0::Int)
-#647 := (not #717)
-#654 := [hypothesis]: #717
-#689 := (>= #443 0::Int)
-#1 := true
-#65 := [true-axiom]: true
-#665 := (or false #689)
-#643 := [th-lemma arith]: #665
-#644 := [unit-resolution #643 #65]: #689
-#95 := (>= #12 0::Int)
-#98 := (not #95)
-#9 := 1::Int
-#13 := (* 2::Int #12)
-#14 := (+ #13 1::Int)
-#15 := (+ f3 #14)
-#10 := (+ f3 1::Int)
-#16 := (<= #10 #15)
-#17 := (not #16)
-#103 := (iff #17 #98)
-#77 := (+ f3 #13)
-#78 := (+ 1::Int #77)
-#68 := (+ 1::Int f3)
-#83 := (<= #68 #78)
-#86 := (not #83)
-#101 := (iff #86 #98)
-#93 := (>= #13 0::Int)
-#89 := (not #93)
-#99 := (iff #89 #98)
-#96 := (iff #93 #95)
-#97 := [rewrite]: #96
-#100 := [monotonicity #97]: #99
-#90 := (iff #86 #89)
-#91 := (iff #83 #93)
-#92 := [rewrite]: #91
-#94 := [monotonicity #92]: #90
-#102 := [trans #94 #100]: #101
-#87 := (iff #17 #86)
-#84 := (iff #16 #83)
-#81 := (= #15 #78)
-#71 := (+ 1::Int #13)
-#74 := (+ f3 #71)
-#79 := (= #74 #78)
-#80 := [rewrite]: #79
-#75 := (= #15 #74)
-#72 := (= #14 #71)
-#73 := [rewrite]: #72
-#76 := [monotonicity #73]: #75
-#82 := [trans #76 #80]: #81
-#69 := (= #10 #68)
-#70 := [rewrite]: #69
-#85 := [monotonicity #70 #82]: #84
-#88 := [monotonicity #85]: #87
-#104 := [trans #88 #102]: #103
-#67 := [asserted]: #17
-#105 := [mp #67 #104]: #98
-#646 := [th-lemma arith farkas -1 1 1 #105 #644 #654]: false
-#648 := [lemma #646]: #647
-#660 := (or #705 #717)
-#661 := [th-lemma arith triangle-eq]: #660
-#662 := [unit-resolution #661 #648]: #705
-#637 := (or #715 #442)
-#741 := -2::Int
-#439 := (* -1::Int f3)
-#465 := (mod #439 -2::Int)
-#361 := (+ #12 #465)
-#460 := (= #361 0::Int)
-#739 := (ite #754 #442 #460)
-#763 := (= #12 0::Int)
-#764 := (= f3 0::Int)
-#450 := (ite #764 #763 #739)
-#19 := (:var 0 Int)
-#18 := (:var 1 Int)
-#39 := (f4 #18 #19)
-#775 := (pattern #39)
-#117 := (* -1::Int #19)
-#114 := (* -1::Int #18)
-#172 := (mod #114 #117)
-#287 := (+ #39 #172)
-#288 := (= #287 0::Int)
-#40 := (mod #18 #19)
-#284 := (* -1::Int #40)
-#285 := (+ #39 #284)
-#286 := (= #285 0::Int)
-#146 := (>= #18 0::Int)
-#139 := (<= #19 0::Int)
-#231 := (or #139 #146)
-#232 := (not #231)
-#135 := (<= #18 0::Int)
-#229 := (or #135 #139)
-#230 := (not #229)
-#235 := (or #230 #232)
-#289 := (ite #235 #286 #288)
-#283 := (= #39 0::Int)
-#22 := (= #18 0::Int)
-#290 := (ite #22 #283 #289)
-#282 := (= #18 #39)
-#23 := (= #19 0::Int)
-#291 := (ite #23 #282 #290)
-#776 := (forall (vars (?v0 Int) (?v1 Int)) (:pat #775) #291)
-#294 := (forall (vars (?v0 Int) (?v1 Int)) #291)
-#779 := (iff #294 #776)
-#777 := (iff #291 #291)
-#778 := [refl]: #777
-#780 := [quant-intro #778]: #779
-#178 := (* -1::Int #172)
-#251 := (ite #235 #40 #178)
-#254 := (ite #22 0::Int #251)
-#257 := (ite #23 #18 #254)
-#260 := (= #39 #257)
-#263 := (forall (vars (?v0 Int) (?v1 Int)) #260)
-#295 := (iff #263 #294)
-#292 := (iff #260 #291)
-#293 := [rewrite]: #292
-#296 := [quant-intro #293]: #295
-#147 := (not #146)
-#140 := (not #139)
-#150 := (and #140 #147)
+#122 := (<= f3 0::Int)
+#135 := (>= f3 0::Int)
#136 := (not #135)
-#143 := (and #136 #140)
-#153 := (or #143 #150)
-#198 := (ite #153 #40 #178)
-#201 := (ite #22 0::Int #198)
-#204 := (ite #23 #18 #201)
-#207 := (= #39 #204)
-#210 := (forall (vars (?v0 Int) (?v1 Int)) #207)
-#264 := (iff #210 #263)
-#261 := (iff #207 #260)
-#258 := (= #204 #257)
-#255 := (= #201 #254)
-#252 := (= #198 #251)
-#236 := (iff #153 #235)
-#233 := (iff #150 #232)
-#234 := [rewrite]: #233
-#223 := (iff #143 #230)
-#224 := [rewrite]: #223
-#237 := [monotonicity #224 #234]: #236
-#253 := [monotonicity #237]: #252
-#256 := [monotonicity #253]: #255
-#259 := [monotonicity #256]: #258
-#262 := [monotonicity #259]: #261
-#265 := [quant-intro #262]: #264
-#221 := (~ #210 #210)
-#220 := (~ #207 #207)
-#217 := [refl]: #220
-#222 := [nnf-pos #217]: #221
-#33 := (- #19)
-#32 := (- #18)
-#41 := (mod #32 #33)
-#42 := (- #41)
-#26 := (< 0::Int #19)
-#28 := (< #18 0::Int)
-#29 := (and #28 #26)
-#25 := (< 0::Int #18)
-#27 := (and #25 #26)
-#30 := (or #27 #29)
-#43 := (ite #30 #40 #42)
-#44 := (ite #22 0::Int #43)
-#45 := (ite #23 #18 #44)
-#46 := (= #39 #45)
-#47 := (forall (vars (?v0 Int) (?v1 Int)) #46)
-#213 := (iff #47 #210)
-#107 := (and #26 #28)
-#110 := (or #27 #107)
-#183 := (ite #110 #40 #178)
-#186 := (ite #22 0::Int #183)
-#189 := (ite #23 #18 #186)
-#192 := (= #39 #189)
-#195 := (forall (vars (?v0 Int) (?v1 Int)) #192)
-#211 := (iff #195 #210)
-#208 := (iff #192 #207)
-#205 := (= #189 #204)
-#202 := (= #186 #201)
-#199 := (= #183 #198)
-#154 := (iff #110 #153)
-#151 := (iff #107 #150)
-#148 := (iff #28 #147)
-#149 := [rewrite]: #148
-#141 := (iff #26 #140)
-#142 := [rewrite]: #141
-#152 := [monotonicity #142 #149]: #151
-#144 := (iff #27 #143)
-#137 := (iff #25 #136)
+#123 := (not #122)
+#146 := (or #123 #136)
+#195 := (not #146)
+#69 := -2::Int
+#65 := -1::Int
+#66 := (* -1::Int f3)
+#72 := (mod #66 -2::Int)
+#78 := (* -1::Int #72)
+#11 := 2::Int
+#21 := (mod f3 2::Int)
+#149 := (ite #146 #21 #78)
+#193 := (= #21 #149)
+#284 := (not #193)
+#14 := (= f3 0::Int)
+#152 := (ite #14 0::Int #149)
+#268 := (* -1::Int #152)
+#269 := (+ #21 #268)
+#270 := (<= #269 0::Int)
+#267 := (= #21 #152)
+#192 := (= #149 #152)
+#202 := (not #14)
+#191 := (= #152 0::Int)
+#209 := (not #191)
+#175 := (>= #152 0::Int)
+#178 := (not #175)
+#9 := 1::Int
+#23 := (- 2::Int)
+#22 := (- f3)
+#24 := (mod #22 #23)
+#25 := (- #24)
+#16 := (< 0::Int 2::Int)
+#18 := (< f3 0::Int)
+#19 := (and #18 #16)
+#15 := (< 0::Int f3)
+#17 := (and #15 #16)
+#20 := (or #17 #19)
+#26 := (ite #20 #21 #25)
+#27 := (ite #14 0::Int #26)
+#13 := (= 2::Int 0::Int)
+#28 := (ite #13 f3 #27)
+#29 := (* 2::Int #28)
+#30 := (+ #29 1::Int)
+#31 := (+ f3 #30)
+#10 := (+ f3 1::Int)
+#32 := (<= #10 #31)
+#33 := (not #32)
+#183 := (iff #33 #178)
+#59 := (and #16 #18)
+#62 := (or #17 #59)
+#83 := (ite #62 #21 #78)
+#86 := (ite #14 0::Int #83)
+#96 := (* 2::Int #86)
+#110 := (+ f3 #96)
+#111 := (+ 1::Int #110)
+#54 := (+ 1::Int f3)
+#116 := (<= #54 #111)
+#119 := (not #116)
+#181 := (iff #119 #178)
+#155 := (* 2::Int #152)
+#168 := (>= #155 0::Int)
+#172 := (not #168)
+#179 := (iff #172 #178)
+#176 := (iff #168 #175)
+#177 := [rewrite]: #176
+#180 := [monotonicity #177]: #179
+#173 := (iff #119 #172)
+#170 := (iff #116 #168)
+#158 := (+ f3 #155)
+#161 := (+ 1::Int #158)
+#164 := (<= #54 #161)
+#167 := (iff #164 #168)
+#169 := [rewrite]: #167
+#165 := (iff #116 #164)
+#162 := (= #111 #161)
+#159 := (= #110 #158)
+#156 := (= #96 #155)
+#153 := (= #86 #152)
+#150 := (= #83 #149)
+#147 := (iff #62 #146)
+#144 := (iff #59 #136)
+#1 := true
+#139 := (and true #136)
+#142 := (iff #139 #136)
+#143 := [rewrite]: #142
+#140 := (iff #59 #139)
+#137 := (iff #18 #136)
#138 := [rewrite]: #137
-#145 := [monotonicity #138 #142]: #144
-#155 := [monotonicity #145 #152]: #154
-#200 := [monotonicity #155]: #199
-#203 := [monotonicity #200]: #202
-#206 := [monotonicity #203]: #205
-#209 := [monotonicity #206]: #208
-#212 := [quant-intro #209]: #211
-#196 := (iff #47 #195)
-#193 := (iff #46 #192)
-#190 := (= #45 #189)
-#187 := (= #44 #186)
-#184 := (= #43 #183)
-#181 := (= #42 #178)
-#175 := (- #172)
-#179 := (= #175 #178)
-#180 := [rewrite]: #179
-#176 := (= #42 #175)
-#173 := (= #41 #172)
-#118 := (= #33 #117)
-#119 := [rewrite]: #118
-#115 := (= #32 #114)
-#116 := [rewrite]: #115
-#174 := [monotonicity #116 #119]: #173
-#177 := [monotonicity #174]: #176
-#182 := [trans #177 #180]: #181
-#111 := (iff #30 #110)
-#108 := (iff #29 #107)
-#109 := [rewrite]: #108
-#112 := [monotonicity #109]: #111
-#185 := [monotonicity #112 #182]: #184
-#188 := [monotonicity #185]: #187
-#191 := [monotonicity #188]: #190
-#194 := [monotonicity #191]: #193
-#197 := [quant-intro #194]: #196
-#214 := [trans #197 #212]: #213
-#171 := [asserted]: #47
-#215 := [mp #171 #214]: #210
-#218 := [mp~ #215 #222]: #210
-#266 := [mp #218 #265]: #263
-#297 := [mp #266 #296]: #294
-#781 := [mp #297 #780]: #776
-#734 := (not #776)
-#723 := (or #734 #450)
-#355 := (* -1::Int 2::Int)
-#440 := (mod #439 #355)
-#441 := (+ #12 #440)
-#432 := (= #441 0::Int)
-#425 := (<= 2::Int 0::Int)
-#760 := (or #425 #446)
-#762 := (not #760)
-#549 := (or #419 #425)
-#756 := (not #549)
-#430 := (or #756 #762)
-#431 := (ite #430 #442 #432)
-#765 := (ite #764 #763 #431)
-#766 := (= f3 #12)
-#761 := (= 2::Int 0::Int)
-#767 := (ite #761 #766 #765)
-#724 := (or #734 #767)
-#720 := (iff #724 #723)
-#726 := (iff #723 #723)
-#727 := [rewrite]: #726
-#733 := (iff #767 #450)
-#453 := (ite false #766 #450)
-#447 := (iff #453 #450)
-#729 := [rewrite]: #447
-#731 := (iff #767 #453)
-#451 := (iff #765 #450)
-#736 := (iff #431 #739)
-#461 := (iff #432 #460)
-#737 := (= #441 #361)
-#466 := (= #440 #465)
-#742 := (= #355 -2::Int)
-#464 := [rewrite]: #742
-#467 := [monotonicity #464]: #466
-#738 := [monotonicity #467]: #737
-#735 := [monotonicity #738]: #461
-#752 := (iff #430 #754)
-#393 := (iff #762 #753)
-#388 := (iff #760 #446)
-#747 := (or false #446)
-#744 := (iff #747 #446)
-#750 := [rewrite]: #744
-#748 := (iff #760 #747)
-#422 := (iff #425 false)
-#758 := [rewrite]: #422
-#749 := [monotonicity #758]: #748
-#751 := [trans #749 #750]: #388
-#394 := [monotonicity #751]: #393
-#745 := (iff #756 #409)
-#407 := (iff #549 #419)
-#418 := (or #419 false)
-#743 := (iff #418 #419)
-#406 := [rewrite]: #743
-#759 := (iff #549 #418)
-#402 := [monotonicity #758]: #759
-#408 := [trans #402 #406]: #407
-#746 := [monotonicity #408]: #745
-#755 := [monotonicity #746 #394]: #752
-#740 := [monotonicity #755 #735]: #736
-#452 := [monotonicity #740]: #451
-#757 := (iff #761 false)
-#417 := [rewrite]: #757
-#732 := [monotonicity #417 #452]: #731
-#730 := [trans #732 #729]: #733
-#721 := [monotonicity #730]: #720
-#722 := [trans #721 #727]: #720
-#725 := [quant-inst #8 #11]: #724
-#728 := [mp #725 #722]: #723
-#663 := [unit-resolution #728 #781]: #450
-#593 := (not #764)
-#592 := (not #450)
-#649 := (or #592 #593)
-#698 := (not #763)
-#664 := (or #698 #95)
-#688 := [th-lemma arith triangle-eq]: #664
-#682 := [unit-resolution #688 #105]: #698
-#552 := (or #592 #593 #763)
-#700 := [def-axiom]: #552
-#650 := [unit-resolution #700 #682]: #649
-#645 := [unit-resolution #650 #663]: #593
-#602 := (or #592 #764 #739)
-#697 := [def-axiom]: #602
-#651 := [unit-resolution #697 #645 #663]: #739
-#719 := (not #739)
-#548 := (or #719 #715 #442)
-#550 := [def-axiom]: #548
-#633 := [unit-resolution #550 #651]: #637
-#634 := [unit-resolution #633 #662]: #715
-#570 := (or #754 #419)
-#571 := [def-axiom]: #570
-#635 := [unit-resolution #571 #634]: #419
-#713 := (or #754 #446)
-#714 := [def-axiom]: #713
-#638 := [unit-resolution #714 #634]: #446
-#639 := (or #764 #409 #753)
-#640 := [th-lemma arith triangle-eq]: #639
-#641 := [unit-resolution #640 #645]: #754
-[unit-resolution #641 #638 #635]: false
-unsat
-3b8dfbe5d2104f714ba2e5d249bcf001c2c84dba 349 0
+#126 := (iff #16 true)
+#127 := [rewrite]: #126
+#141 := [monotonicity #127 #138]: #140
+#145 := [trans #141 #143]: #144
+#133 := (iff #17 #123)
+#128 := (and #123 true)
+#131 := (iff #128 #123)
+#132 := [rewrite]: #131
+#129 := (iff #17 #128)
+#124 := (iff #15 #123)
+#125 := [rewrite]: #124
+#130 := [monotonicity #125 #127]: #129
+#134 := [trans #130 #132]: #133
+#148 := [monotonicity #134 #145]: #147
+#151 := [monotonicity #148]: #150
+#154 := [monotonicity #151]: #153
+#157 := [monotonicity #154]: #156
+#160 := [monotonicity #157]: #159
+#163 := [monotonicity #160]: #162
+#166 := [monotonicity #163]: #165
+#171 := [trans #166 #169]: #170
+#174 := [monotonicity #171]: #173
+#182 := [trans #174 #180]: #181
+#120 := (iff #33 #119)
+#117 := (iff #32 #116)
+#114 := (= #31 #111)
+#102 := (+ 1::Int #96)
+#107 := (+ f3 #102)
+#112 := (= #107 #111)
+#113 := [rewrite]: #112
+#108 := (= #31 #107)
+#105 := (= #30 #102)
+#99 := (+ #96 1::Int)
+#103 := (= #99 #102)
+#104 := [rewrite]: #103
+#100 := (= #30 #99)
+#97 := (= #29 #96)
+#94 := (= #28 #86)
+#89 := (ite false f3 #86)
+#92 := (= #89 #86)
+#93 := [rewrite]: #92
+#90 := (= #28 #89)
+#87 := (= #27 #86)
+#84 := (= #26 #83)
+#81 := (= #25 #78)
+#75 := (- #72)
+#79 := (= #75 #78)
+#80 := [rewrite]: #79
+#76 := (= #25 #75)
+#73 := (= #24 #72)
+#70 := (= #23 -2::Int)
+#71 := [rewrite]: #70
+#67 := (= #22 #66)
+#68 := [rewrite]: #67
+#74 := [monotonicity #68 #71]: #73
+#77 := [monotonicity #74]: #76
+#82 := [trans #77 #80]: #81
+#63 := (iff #20 #62)
+#60 := (iff #19 #59)
+#61 := [rewrite]: #60
+#64 := [monotonicity #61]: #63
+#85 := [monotonicity #64 #82]: #84
+#88 := [monotonicity #85]: #87
+#57 := (iff #13 false)
+#58 := [rewrite]: #57
+#91 := [monotonicity #58 #88]: #90
+#95 := [trans #91 #93]: #94
+#98 := [monotonicity #95]: #97
+#101 := [monotonicity #98]: #100
+#106 := [trans #101 #104]: #105
+#109 := [monotonicity #106]: #108
+#115 := [trans #109 #113]: #114
+#55 := (= #10 #54)
+#56 := [rewrite]: #55
+#118 := [monotonicity #56 #115]: #117
+#121 := [monotonicity #118]: #120
+#184 := [trans #121 #182]: #183
+#53 := [asserted]: #33
+#185 := [mp #53 #184]: #178
+#208 := [hypothesis]: #191
+#210 := (or #209 #175)
+#211 := [th-lemma arith triangle-eq]: #210
+#212 := [unit-resolution #211 #208 #185]: false
+#213 := [lemma #212]: #209
+#203 := (or #202 #191)
+#204 := [def-axiom]: #203
+#272 := [unit-resolution #204 #213]: #202
+#205 := (or #14 #192)
+#206 := [def-axiom]: #205
+#273 := [unit-resolution #206 #272]: #192
+#274 := [hypothesis]: #193
+#275 := [trans #274 #273]: #267
+#276 := (not #267)
+#277 := (or #276 #270)
+#278 := [th-lemma arith triangle-eq]: #277
+#279 := [unit-resolution #278 #275]: #270
+#239 := (>= #21 0::Int)
+#51 := [true-axiom]: true
+#280 := (or false #239)
+#281 := [th-lemma arith]: #280
+#282 := [unit-resolution #281 #51]: #239
+#283 := [th-lemma arith farkas -1 1 1 #282 #185 #279]: false
+#285 := [lemma #283]: #284
+#198 := (or #195 #193)
+#199 := [def-axiom]: #198
+#262 := [unit-resolution #199 #285]: #195
+#189 := (or #146 #122)
+#190 := [def-axiom]: #189
+#263 := [unit-resolution #190 #262]: #122
+#187 := (or #146 #135)
+#188 := [def-axiom]: #187
+#264 := [unit-resolution #188 #262]: #135
+#265 := (or #14 #123 #136)
+#266 := [th-lemma arith triangle-eq]: #265
+#237 := [unit-resolution #266 #272]: #146
+[unit-resolution #237 #264 #263]: false
+unsat
+a9554a5e9a99c006412b9165d7d1ec39d927f284 207 0
#2 := false
-#20 := 0::Int
+#10 := 0::Int
decl f3 :: Int
#8 := f3
-#438 := (>= f3 0::Int)
-#758 := (<= f3 0::Int)
-#404 := (not #758)
-#747 := (not #438)
-#751 := (or #747 #404)
-#714 := (not #751)
+#112 := (<= f3 0::Int)
+#125 := (>= f3 0::Int)
+#126 := (not #125)
+#113 := (not #112)
+#136 := (or #113 #126)
+#184 := (not #136)
+#65 := -2::Int
+#61 := -1::Int
+#62 := (* -1::Int f3)
+#68 := (mod #62 -2::Int)
+#74 := (* -1::Int #68)
#9 := 2::Int
-#439 := (mod f3 2::Int)
-#108 := -1::Int
-#440 := (* -1::Int #439)
-decl f4 :: (-> Int Int Int)
-#10 := (f4 f3 2::Int)
-#368 := (+ #10 #440)
-#441 := (= #368 0::Int)
-#587 := (not #441)
-#544 := (<= #368 0::Int)
-#647 := (not #544)
-#655 := (>= #439 2::Int)
-#656 := (not #655)
+#19 := (mod f3 2::Int)
+#139 := (ite #136 #19 #74)
+#182 := (= #19 #139)
+#279 := (not #182)
+#251 := (>= #19 2::Int)
+#252 := (not #251)
#1 := true
-#64 := [true-axiom]: true
-#643 := (or false #656)
-#644 := [th-lemma arith]: #643
-#645 := [unit-resolution #644 #64]: #656
-#646 := [hypothesis]: #544
-#93 := (>= #10 2::Int)
-#13 := 3::Int
-#14 := (+ f3 3::Int)
-#11 := (+ #10 #10)
-#12 := (+ f3 #11)
-#15 := (< #12 #14)
-#16 := (not #15)
-#98 := (iff #16 #93)
-#73 := (+ 3::Int f3)
-#67 := (* 2::Int #10)
-#70 := (+ f3 #67)
-#76 := (< #70 #73)
-#79 := (not #76)
-#96 := (iff #79 #93)
-#86 := (>= #67 3::Int)
-#94 := (iff #86 #93)
-#95 := [rewrite]: #94
-#91 := (iff #79 #86)
-#84 := (not #86)
-#83 := (not #84)
-#89 := (iff #83 #86)
-#90 := [rewrite]: #89
-#87 := (iff #79 #83)
-#85 := (iff #76 #84)
-#82 := [rewrite]: #85
-#88 := [monotonicity #82]: #87
-#92 := [trans #88 #90]: #91
-#97 := [trans #92 #95]: #96
-#80 := (iff #16 #79)
-#77 := (iff #15 #76)
-#74 := (= #14 #73)
-#75 := [rewrite]: #74
-#71 := (= #12 #70)
-#68 := (= #11 #67)
-#69 := [rewrite]: #68
-#72 := [monotonicity #69]: #71
-#78 := [monotonicity #72 #75]: #77
-#81 := [monotonicity #78]: #80
-#99 := [trans #81 #97]: #98
-#66 := [asserted]: #16
-#100 := [mp #66 #99]: #93
-#641 := [th-lemma arith farkas -1 1 1 #100 #646 #645]: false
-#633 := [lemma #641]: #647
-#650 := (or #587 #544)
-#661 := [th-lemma arith triangle-eq]: #650
-#639 := [unit-resolution #661 #633]: #587
-#611 := (or #714 #441)
-#462 := -2::Int
-#435 := (* -1::Int f3)
-#733 := (mod #435 -2::Int)
-#457 := (+ #10 #733)
-#732 := (= #457 0::Int)
-#447 := (ite #751 #441 #732)
-#427 := (= #10 0::Int)
-#759 := (= f3 0::Int)
-#727 := (ite #759 #427 #447)
-#18 := (:var 0 Int)
-#17 := (:var 1 Int)
-#38 := (f4 #17 #18)
-#771 := (pattern #38)
-#112 := (* -1::Int #18)
-#109 := (* -1::Int #17)
-#167 := (mod #109 #112)
-#282 := (+ #38 #167)
-#283 := (= #282 0::Int)
-#39 := (mod #17 #18)
-#279 := (* -1::Int #39)
-#280 := (+ #38 #279)
-#281 := (= #280 0::Int)
-#141 := (>= #17 0::Int)
-#134 := (<= #18 0::Int)
-#226 := (or #134 #141)
-#227 := (not #226)
-#130 := (<= #17 0::Int)
-#224 := (or #130 #134)
-#225 := (not #224)
-#230 := (or #225 #227)
-#284 := (ite #230 #281 #283)
-#278 := (= #38 0::Int)
-#21 := (= #17 0::Int)
-#285 := (ite #21 #278 #284)
-#277 := (= #17 #38)
-#22 := (= #18 0::Int)
-#286 := (ite #22 #277 #285)
-#772 := (forall (vars (?v0 Int) (?v1 Int)) (:pat #771) #286)
-#289 := (forall (vars (?v0 Int) (?v1 Int)) #286)
-#775 := (iff #289 #772)
-#773 := (iff #286 #286)
-#774 := [refl]: #773
-#776 := [quant-intro #774]: #775
-#173 := (* -1::Int #167)
-#246 := (ite #230 #39 #173)
-#249 := (ite #21 0::Int #246)
-#252 := (ite #22 #17 #249)
-#255 := (= #38 #252)
-#258 := (forall (vars (?v0 Int) (?v1 Int)) #255)
-#290 := (iff #258 #289)
-#287 := (iff #255 #286)
-#288 := [rewrite]: #287
-#291 := [quant-intro #288]: #290
-#142 := (not #141)
-#135 := (not #134)
-#145 := (and #135 #142)
-#131 := (not #130)
-#138 := (and #131 #135)
-#148 := (or #138 #145)
-#193 := (ite #148 #39 #173)
-#196 := (ite #21 0::Int #193)
-#199 := (ite #22 #17 #196)
-#202 := (= #38 #199)
-#205 := (forall (vars (?v0 Int) (?v1 Int)) #202)
-#259 := (iff #205 #258)
-#256 := (iff #202 #255)
-#253 := (= #199 #252)
-#250 := (= #196 #249)
-#247 := (= #193 #246)
-#231 := (iff #148 #230)
-#228 := (iff #145 #227)
-#229 := [rewrite]: #228
-#218 := (iff #138 #225)
-#219 := [rewrite]: #218
-#232 := [monotonicity #219 #229]: #231
-#248 := [monotonicity #232]: #247
-#251 := [monotonicity #248]: #250
-#254 := [monotonicity #251]: #253
-#257 := [monotonicity #254]: #256
-#260 := [quant-intro #257]: #259
-#216 := (~ #205 #205)
-#215 := (~ #202 #202)
-#212 := [refl]: #215
-#217 := [nnf-pos #212]: #216
-#32 := (- #18)
-#31 := (- #17)
-#40 := (mod #31 #32)
-#41 := (- #40)
-#25 := (< 0::Int #18)
-#27 := (< #17 0::Int)
-#28 := (and #27 #25)
-#24 := (< 0::Int #17)
-#26 := (and #24 #25)
-#29 := (or #26 #28)
-#42 := (ite #29 #39 #41)
-#43 := (ite #21 0::Int #42)
-#44 := (ite #22 #17 #43)
-#45 := (= #38 #44)
-#46 := (forall (vars (?v0 Int) (?v1 Int)) #45)
-#208 := (iff #46 #205)
-#102 := (and #25 #27)
-#105 := (or #26 #102)
-#178 := (ite #105 #39 #173)
-#181 := (ite #21 0::Int #178)
-#184 := (ite #22 #17 #181)
-#187 := (= #38 #184)
-#190 := (forall (vars (?v0 Int) (?v1 Int)) #187)
-#206 := (iff #190 #205)
-#203 := (iff #187 #202)
-#200 := (= #184 #199)
-#197 := (= #181 #196)
-#194 := (= #178 #193)
-#149 := (iff #105 #148)
-#146 := (iff #102 #145)
-#143 := (iff #27 #142)
-#144 := [rewrite]: #143
-#136 := (iff #25 #135)
-#137 := [rewrite]: #136
-#147 := [monotonicity #137 #144]: #146
-#139 := (iff #26 #138)
-#132 := (iff #24 #131)
+#50 := [true-axiom]: true
+#267 := (or false #252)
+#268 := [th-lemma arith]: #267
+#269 := [unit-resolution #268 #50]: #252
+#12 := (= f3 0::Int)
+#142 := (ite #12 0::Int #139)
+#263 := (* -1::Int #142)
+#264 := (+ #19 #263)
+#266 := (>= #264 0::Int)
+#262 := (= #19 #142)
+#181 := (= #139 #142)
+#191 := (not #12)
+#180 := (= #142 0::Int)
+#204 := (not #180)
+#196 := (<= #142 0::Int)
+#198 := (not #196)
+#167 := (>= #142 2::Int)
+#29 := 3::Int
+#30 := (+ f3 3::Int)
+#21 := (- 2::Int)
+#20 := (- f3)
+#22 := (mod #20 #21)
+#23 := (- #22)
+#14 := (< 0::Int 2::Int)
+#16 := (< f3 0::Int)
+#17 := (and #16 #14)
+#13 := (< 0::Int f3)
+#15 := (and #13 #14)
+#18 := (or #15 #17)
+#24 := (ite #18 #19 #23)
+#25 := (ite #12 0::Int #24)
+#11 := (= 2::Int 0::Int)
+#26 := (ite #11 f3 #25)
+#27 := (+ #26 #26)
+#28 := (+ f3 #27)
+#31 := (< #28 #30)
+#32 := (not #31)
+#172 := (iff #32 #167)
+#103 := (+ 3::Int f3)
+#55 := (and #14 #16)
+#58 := (or #15 #55)
+#79 := (ite #58 #19 #74)
+#82 := (ite #12 0::Int #79)
+#95 := (* 2::Int #82)
+#100 := (+ f3 #95)
+#106 := (< #100 #103)
+#109 := (not #106)
+#170 := (iff #109 #167)
+#145 := (* 2::Int #142)
+#155 := (>= #145 3::Int)
+#168 := (iff #155 #167)
+#169 := [rewrite]: #168
+#165 := (iff #109 #155)
+#154 := (not #155)
+#160 := (not #154)
+#163 := (iff #160 #155)
+#164 := [rewrite]: #163
+#161 := (iff #109 #160)
+#158 := (iff #106 #154)
+#148 := (+ f3 #145)
+#151 := (< #148 #103)
+#156 := (iff #151 #154)
+#157 := [rewrite]: #156
+#152 := (iff #106 #151)
+#149 := (= #100 #148)
+#146 := (= #95 #145)
+#143 := (= #82 #142)
+#140 := (= #79 #139)
+#137 := (iff #58 #136)
+#134 := (iff #55 #126)
+#129 := (and true #126)
+#132 := (iff #129 #126)
#133 := [rewrite]: #132
-#140 := [monotonicity #133 #137]: #139
-#150 := [monotonicity #140 #147]: #149
-#195 := [monotonicity #150]: #194
-#198 := [monotonicity #195]: #197
-#201 := [monotonicity #198]: #200
-#204 := [monotonicity #201]: #203
-#207 := [quant-intro #204]: #206
-#191 := (iff #46 #190)
-#188 := (iff #45 #187)
-#185 := (= #44 #184)
-#182 := (= #43 #181)
-#179 := (= #42 #178)
-#176 := (= #41 #173)
-#170 := (- #167)
-#174 := (= #170 #173)
-#175 := [rewrite]: #174
-#171 := (= #41 #170)
-#168 := (= #40 #167)
-#113 := (= #32 #112)
-#114 := [rewrite]: #113
-#110 := (= #31 #109)
-#111 := [rewrite]: #110
-#169 := [monotonicity #111 #114]: #168
-#172 := [monotonicity #169]: #171
-#177 := [trans #172 #175]: #176
-#106 := (iff #29 #105)
-#103 := (iff #28 #102)
-#104 := [rewrite]: #103
-#107 := [monotonicity #104]: #106
-#180 := [monotonicity #107 #177]: #179
-#183 := [monotonicity #180]: #182
-#186 := [monotonicity #183]: #185
-#189 := [monotonicity #186]: #188
-#192 := [quant-intro #189]: #191
-#209 := [trans #192 #207]: #208
-#166 := [asserted]: #46
-#210 := [mp #166 #209]: #205
-#213 := [mp~ #210 #217]: #205
-#261 := [mp #213 #260]: #258
-#292 := [mp #261 #291]: #289
-#777 := [mp #292 #776]: #772
-#716 := (not #772)
-#717 := (or #716 #727)
-#350 := (* -1::Int 2::Int)
-#436 := (mod #435 #350)
-#437 := (+ #10 #436)
-#428 := (= #437 0::Int)
-#442 := (<= 2::Int 0::Int)
-#421 := (or #442 #438)
-#756 := (not #421)
-#415 := (or #758 #442)
-#545 := (not #415)
-#752 := (or #545 #756)
-#426 := (ite #752 #441 #428)
-#760 := (ite #759 #427 #426)
-#761 := (= f3 #10)
-#762 := (= 2::Int 0::Int)
-#757 := (ite #762 #761 #760)
-#722 := (or #716 #757)
-#718 := (iff #722 #717)
-#565 := (iff #717 #717)
-#566 := [rewrite]: #565
-#720 := (iff #757 #727)
-#725 := (ite false #761 #727)
-#730 := (iff #725 #727)
-#719 := [rewrite]: #730
-#729 := (iff #757 #725)
-#728 := (iff #760 #727)
-#448 := (iff #426 #447)
-#736 := (iff #428 #732)
-#731 := (= #437 #457)
-#734 := (= #436 #733)
-#463 := (= #350 -2::Int)
-#356 := [rewrite]: #463
-#456 := [monotonicity #356]: #734
-#735 := [monotonicity #456]: #731
-#446 := [monotonicity #735]: #736
-#460 := (iff #752 #751)
-#390 := (or #404 #747)
-#737 := (iff #390 #751)
-#738 := [rewrite]: #737
-#750 := (iff #752 #390)
-#749 := (iff #756 #747)
-#746 := (iff #421 #438)
-#742 := (or false #438)
-#745 := (iff #742 #438)
-#740 := [rewrite]: #745
-#743 := (iff #421 #742)
-#413 := (iff #442 false)
-#418 := [rewrite]: #413
-#744 := [monotonicity #418]: #743
-#384 := [trans #744 #740]: #746
-#389 := [monotonicity #384]: #749
-#405 := (iff #545 #404)
-#402 := (iff #415 #758)
-#754 := (or #758 false)
-#398 := (iff #754 #758)
-#739 := [rewrite]: #398
-#414 := (iff #415 #754)
-#755 := [monotonicity #418]: #414
-#403 := [trans #755 #739]: #402
-#741 := [monotonicity #403]: #405
-#748 := [monotonicity #741 #389]: #750
-#461 := [trans #748 #738]: #460
-#449 := [monotonicity #461 #446]: #448
-#443 := [monotonicity #449]: #728
-#763 := (iff #762 false)
-#753 := [rewrite]: #763
-#726 := [monotonicity #753 #443]: #729
-#721 := [trans #726 #719]: #720
-#724 := [monotonicity #721]: #718
-#567 := [trans #724 #566]: #718
-#723 := [quant-inst #8 #9]: #722
-#709 := [mp #723 #567]: #717
-#640 := [unit-resolution #709 #777]: #727
-#694 := (not #759)
-#693 := (not #727)
-#636 := (or #693 #694)
-#600 := (not #427)
-#710 := (<= #10 0::Int)
-#642 := (not #710)
-#672 := (not #93)
-#673 := (or #642 #672)
-#629 := [th-lemma arith farkas 1 1]: #673
-#630 := [unit-resolution #629 #100]: #642
-#631 := (or #600 #710)
-#634 := [th-lemma arith triangle-eq]: #631
-#635 := [unit-resolution #634 #630]: #600
-#697 := (or #693 #694 #427)
-#582 := [def-axiom]: #697
-#637 := [unit-resolution #582 #635]: #636
-#632 := [unit-resolution #637 #640]: #694
-#597 := (or #693 #759 #447)
-#599 := [def-axiom]: #597
-#638 := [unit-resolution #599 #632 #640]: #447
-#701 := (not #447)
-#703 := (or #701 #714 #441)
-#704 := [def-axiom]: #703
-#612 := [unit-resolution #704 #638]: #611
-#613 := [unit-resolution #612 #639]: #714
-#712 := (or #751 #438)
-#706 := [def-axiom]: #712
-#506 := [unit-resolution #706 #613]: #438
-#707 := (or #751 #758)
-#713 := [def-axiom]: #707
-#617 := [unit-resolution #713 #613]: #758
-#618 := (or #759 #404 #747)
-#619 := [th-lemma arith triangle-eq]: #618
-#624 := [unit-resolution #619 #632]: #390
-[unit-resolution #624 #617 #506]: false
+#130 := (iff #55 #129)
+#127 := (iff #16 #126)
+#128 := [rewrite]: #127
+#116 := (iff #14 true)
+#117 := [rewrite]: #116
+#131 := [monotonicity #117 #128]: #130
+#135 := [trans #131 #133]: #134
+#123 := (iff #15 #113)
+#118 := (and #113 true)
+#121 := (iff #118 #113)
+#122 := [rewrite]: #121
+#119 := (iff #15 #118)
+#114 := (iff #13 #113)
+#115 := [rewrite]: #114
+#120 := [monotonicity #115 #117]: #119
+#124 := [trans #120 #122]: #123
+#138 := [monotonicity #124 #135]: #137
+#141 := [monotonicity #138]: #140
+#144 := [monotonicity #141]: #143
+#147 := [monotonicity #144]: #146
+#150 := [monotonicity #147]: #149
+#153 := [monotonicity #150]: #152
+#159 := [trans #153 #157]: #158
+#162 := [monotonicity #159]: #161
+#166 := [trans #162 #164]: #165
+#171 := [trans #166 #169]: #170
+#110 := (iff #32 #109)
+#107 := (iff #31 #106)
+#104 := (= #30 #103)
+#105 := [rewrite]: #104
+#101 := (= #28 #100)
+#98 := (= #27 #95)
+#92 := (+ #82 #82)
+#96 := (= #92 #95)
+#97 := [rewrite]: #96
+#93 := (= #27 #92)
+#90 := (= #26 #82)
+#85 := (ite false f3 #82)
+#88 := (= #85 #82)
+#89 := [rewrite]: #88
+#86 := (= #26 #85)
+#83 := (= #25 #82)
+#80 := (= #24 #79)
+#77 := (= #23 #74)
+#71 := (- #68)
+#75 := (= #71 #74)
+#76 := [rewrite]: #75
+#72 := (= #23 #71)
+#69 := (= #22 #68)
+#66 := (= #21 -2::Int)
+#67 := [rewrite]: #66
+#63 := (= #20 #62)
+#64 := [rewrite]: #63
+#70 := [monotonicity #64 #67]: #69
+#73 := [monotonicity #70]: #72
+#78 := [trans #73 #76]: #77
+#59 := (iff #18 #58)
+#56 := (iff #17 #55)
+#57 := [rewrite]: #56
+#60 := [monotonicity #57]: #59
+#81 := [monotonicity #60 #78]: #80
+#84 := [monotonicity #81]: #83
+#53 := (iff #11 false)
+#54 := [rewrite]: #53
+#87 := [monotonicity #54 #84]: #86
+#91 := [trans #87 #89]: #90
+#94 := [monotonicity #91 #91]: #93
+#99 := [trans #94 #97]: #98
+#102 := [monotonicity #99]: #101
+#108 := [monotonicity #102 #105]: #107
+#111 := [monotonicity #108]: #110
+#173 := [trans #111 #171]: #172
+#52 := [asserted]: #32
+#174 := [mp #52 #173]: #167
+#199 := (not #167)
+#200 := (or #198 #199)
+#201 := [th-lemma arith farkas 1 1]: #200
+#202 := [unit-resolution #201 #174]: #198
+#203 := [hypothesis]: #180
+#205 := (or #204 #196)
+#206 := [th-lemma arith triangle-eq]: #205
+#207 := [unit-resolution #206 #203 #202]: false
+#208 := [lemma #207]: #204
+#192 := (or #191 #180)
+#193 := [def-axiom]: #192
+#270 := [unit-resolution #193 #208]: #191
+#194 := (or #12 #181)
+#195 := [def-axiom]: #194
+#271 := [unit-resolution #195 #270]: #181
+#272 := [hypothesis]: #182
+#273 := [trans #272 #271]: #262
+#274 := (not #262)
+#275 := (or #274 #266)
+#276 := [th-lemma arith triangle-eq]: #275
+#277 := [unit-resolution #276 #273]: #266
+#278 := [th-lemma arith farkas -1 -1 1 #174 #277 #269]: false
+#280 := [lemma #278]: #279
+#187 := (or #184 #182)
+#188 := [def-axiom]: #187
+#257 := [unit-resolution #188 #280]: #184
+#178 := (or #136 #112)
+#179 := [def-axiom]: #178
+#258 := [unit-resolution #179 #257]: #112
+#176 := (or #136 #125)
+#177 := [def-axiom]: #176
+#259 := [unit-resolution #177 #257]: #125
+#260 := (or #12 #113 #126)
+#261 := [th-lemma arith triangle-eq]: #260
+#232 := [unit-resolution #261 #270]: #136
+[unit-resolution #232 #259 #258]: false
unsat
cfa8a4e8b0964986b89eaf37e6038032e9b8b0d6 101 0
#2 := false
@@ -8171,936 +7945,783 @@
#123 := [th-lemma arith triangle-eq]: #122
[unit-resolution #123 #119 #112 #46]: false
unsat
-742e212b0179422ed718ceb7818522f48622510c 930 0
+cf727a25fbaea6abf5a0d302bf954b4ffa92b324 777 0
#2 := false
-#20 := 1::Int
-decl f3 :: (-> Int Int Int)
-#11 := 2::Int
-decl f5 :: Int
-#9 := f5
-#22 := (f3 f5 2::Int)
-#1103 := (<= #22 1::Int)
-#13 := 0::Int
-#574 := (mod f5 2::Int)
-#108 := -1::Int
-#575 := (* -1::Int #574)
-#576 := (+ #22 #575)
-#954 := (<= #576 0::Int)
-#577 := (= #576 0::Int)
-decl f4 :: Int
-#8 := f4
-#10 := (+ f4 f5)
-#461 := (>= #10 0::Int)
-#778 := (= #10 0::Int)
-#458 := (mod #10 2::Int)
-#459 := (* -1::Int #458)
-#12 := (f3 #10 2::Int)
-#460 := (+ #12 #459)
-#457 := (= #460 0::Int)
-#715 := (not #457)
-#720 := (<= #460 0::Int)
-#1107 := [hypothesis]: #457
-#1108 := (or #715 #720)
-#1109 := [th-lemma arith triangle-eq]: #1108
-#1110 := [unit-resolution #1109 #1107]: #720
-#722 := (>= #460 0::Int)
-#1111 := (or #715 #722)
-#1322 := [th-lemma arith triangle-eq]: #1111
-#1323 := [unit-resolution #1322 #1107]: #722
-#1193 := (not #720)
-#1239 := (not #722)
-#1348 := (or #1239 #1193)
-#1112 := (div f5 2::Int)
-#476 := -2::Int
-#1125 := (* -2::Int #1112)
-#1126 := (+ #575 #1125)
-#1127 := (+ f5 #1126)
-#1124 := (= #1127 0::Int)
-#1161 := (not #1124)
-#1276 := [hypothesis]: #1161
+#9 := 0::Int
+#30 := 4::Int
+decl f3 :: Int
+#11 := f3
+#546 := (div f3 4::Int)
+#208 := -4::Int
+#574 := (* -4::Int #546)
+#39 := (mod f3 4::Int)
+#107 := -1::Int
+#573 := (* -1::Int #39)
+#575 := (+ #573 #574)
+#576 := (+ f3 #575)
+#581 := (<= #576 0::Int)
+#572 := (= #576 0::Int)
#1 := true
-#72 := [true-axiom]: true
-#1154 := (or false #1124)
-#1159 := [th-lemma arith]: #1154
-#1277 := [unit-resolution #1159 #72 #1276]: false
-#1278 := [lemma #1277]: #1124
-#1274 := (or #1161 #1239 #1193)
-#1134 := (>= #574 0::Int)
-#1157 := (or false #1134)
-#1158 := [th-lemma arith]: #1157
-#1151 := [unit-resolution #1158 #72]: #1134
-#1224 := (>= #1127 0::Int)
-#1246 := [hypothesis]: #1124
-#1247 := (or #1161 #1224)
-#1248 := [th-lemma arith triangle-eq]: #1247
-#1249 := [unit-resolution #1248 #1246]: #1224
-#17 := 3::Int
-#15 := 4::Int
-#16 := (f3 f4 4::Int)
-#568 := (>= #16 3::Int)
-#18 := (= #16 3::Int)
-#75 := [asserted]: #18
-#967 := (not #18)
-#993 := (or #967 #568)
-#994 := [th-lemma arith triangle-eq]: #993
-#995 := [unit-resolution #994 #75]: #568
-#865 := (div f4 4::Int)
-#663 := -4::Int
-#881 := (* -4::Int #865)
-#696 := (mod f4 4::Int)
-#698 := (* -1::Int #696)
-#882 := (+ #698 #881)
-#883 := (+ f4 #882)
-#889 := (>= #883 0::Int)
-#880 := (= #883 0::Int)
-#971 := (or false #880)
-#972 := [th-lemma arith]: #971
-#973 := [unit-resolution #972 #72]: #880
-#974 := (not #880)
-#996 := (or #974 #889)
-#997 := [th-lemma arith triangle-eq]: #996
-#998 := [unit-resolution #997 #973]: #889
-#560 := (>= #12 0::Int)
-#14 := (= #12 0::Int)
-#74 := [asserted]: #14
-#622 := (not #14)
-#1230 := (or #622 #560)
-#1231 := [th-lemma arith triangle-eq]: #1230
-#1232 := [unit-resolution #1231 #74]: #560
-#811 := (div #10 2::Int)
-#828 := (* -2::Int #811)
-#829 := (+ #459 #828)
-#830 := (+ f5 #829)
-#831 := (+ f4 #830)
-#1106 := (>= #831 0::Int)
-#826 := (= #831 0::Int)
-#1167 := (or false #826)
-#1168 := [th-lemma arith]: #1167
-#1169 := [unit-resolution #1168 #72]: #826
-#1180 := (not #826)
-#1233 := (or #1180 #1106)
-#1234 := [th-lemma arith triangle-eq]: #1233
-#1235 := [unit-resolution #1234 #1169]: #1106
-#708 := (+ #16 #698)
-#600 := (>= #708 0::Int)
-#709 := (= #708 0::Int)
-#482 := (* -1::Int f4)
-#660 := (mod #482 -4::Int)
-#648 := (+ #16 #660)
-#653 := (= #648 0::Int)
-#710 := (>= f4 0::Int)
-#669 := (not #710)
-#701 := (<= f4 0::Int)
-#670 := (not #701)
-#659 := (or #670 #669)
-#656 := (ite #659 #709 #653)
-#689 := (= f4 0::Int)
-#590 := (not #689)
-#688 := (= #16 0::Int)
-#595 := (not #688)
-#428 := (= 3::Int 0::Int)
-#430 := (iff #428 false)
-#419 := [rewrite]: #430
-#425 := [hypothesis]: #688
-#426 := (= 3::Int #16)
-#427 := [symm #75]: #426
-#429 := [trans #427 #425]: #428
-#431 := [mp #429 #419]: false
-#412 := [lemma #431]: #595
-#1027 := (or #590 #688)
-#630 := (ite #689 #688 #656)
-#27 := (:var 0 Int)
-#26 := (:var 1 Int)
-#46 := (f3 #26 #27)
-#790 := (pattern #46)
-#112 := (* -1::Int #27)
-#109 := (* -1::Int #26)
-#173 := (mod #109 #112)
-#302 := (+ #46 #173)
-#303 := (= #302 0::Int)
-#47 := (mod #26 #27)
-#299 := (* -1::Int #47)
-#300 := (+ #46 #299)
-#301 := (= #300 0::Int)
-#147 := (>= #26 0::Int)
-#140 := (<= #27 0::Int)
-#246 := (or #140 #147)
-#247 := (not #246)
-#136 := (<= #26 0::Int)
-#242 := (or #136 #140)
-#243 := (not #242)
-#250 := (or #243 #247)
-#304 := (ite #250 #301 #303)
-#298 := (= #46 0::Int)
-#29 := (= #26 0::Int)
-#305 := (ite #29 #298 #304)
-#297 := (= #26 #46)
-#30 := (= #27 0::Int)
-#306 := (ite #30 #297 #305)
-#791 := (forall (vars (?v0 Int) (?v1 Int)) (:pat #790) #306)
-#309 := (forall (vars (?v0 Int) (?v1 Int)) #306)
-#794 := (iff #309 #791)
-#792 := (iff #306 #306)
-#793 := [refl]: #792
-#795 := [quant-intro #793]: #794
-#179 := (* -1::Int #173)
-#266 := (ite #250 #47 #179)
-#269 := (ite #29 0::Int #266)
-#272 := (ite #30 #26 #269)
-#275 := (= #46 #272)
-#278 := (forall (vars (?v0 Int) (?v1 Int)) #275)
-#310 := (iff #278 #309)
-#307 := (iff #275 #306)
-#308 := [rewrite]: #307
-#311 := [quant-intro #308]: #310
-#148 := (not #147)
-#141 := (not #140)
-#151 := (and #141 #148)
-#137 := (not #136)
-#144 := (and #137 #141)
-#154 := (or #144 #151)
-#199 := (ite #154 #47 #179)
-#202 := (ite #29 0::Int #199)
-#205 := (ite #30 #26 #202)
-#208 := (= #46 #205)
-#211 := (forall (vars (?v0 Int) (?v1 Int)) #208)
-#279 := (iff #211 #278)
-#276 := (iff #208 #275)
-#273 := (= #205 #272)
-#270 := (= #202 #269)
-#267 := (= #199 #266)
-#251 := (iff #154 #250)
-#248 := (iff #151 #247)
-#249 := [rewrite]: #248
-#244 := (iff #144 #243)
-#245 := [rewrite]: #244
-#252 := [monotonicity #245 #249]: #251
-#268 := [monotonicity #252]: #267
-#271 := [monotonicity #268]: #270
+#93 := [true-axiom]: true
+#721 := (or false #572)
+#722 := [th-lemma arith]: #721
+#723 := [unit-resolution #722 #93]: #572
+#724 := (not #572)
+#725 := (or #724 #581)
+#726 := [th-lemma arith triangle-eq]: #725
+#727 := [unit-resolution #726 #723]: #581
+#582 := (>= #576 0::Int)
+#728 := (or #724 #582)
+#729 := [th-lemma arith triangle-eq]: #728
+#730 := [unit-resolution #729 #723]: #582
+#600 := (>= #39 4::Int)
+#601 := (not #600)
+#731 := (or false #601)
+#732 := [th-lemma arith]: #731
+#733 := [unit-resolution #732 #93]: #601
+#47 := 3::Int
+#613 := (>= #39 3::Int)
+#872 := (= #39 3::Int)
+#108 := (* -1::Int f3)
+#211 := (mod #108 -4::Int)
+#217 := (* -1::Int #211)
+#258 := (>= f3 0::Int)
+#259 := (not #258)
+#245 := (<= f3 0::Int)
+#246 := (not #245)
+#269 := (or #246 #259)
+#272 := (ite #269 #39 #217)
+#32 := (= f3 0::Int)
+#275 := (ite #32 0::Int #272)
+#282 := (= #275 3::Int)
+#41 := (- 4::Int)
+#40 := (- f3)
+#42 := (mod #40 #41)
+#43 := (- #42)
+#34 := (< 0::Int 4::Int)
+#36 := (< f3 0::Int)
+#37 := (and #36 #34)
+#33 := (< 0::Int f3)
+#35 := (and #33 #34)
+#38 := (or #35 #37)
+#44 := (ite #38 #39 #43)
+#45 := (ite #32 0::Int #44)
+#31 := (= 4::Int 0::Int)
+#46 := (ite #31 f3 #45)
+#48 := (= #46 3::Int)
+#286 := (iff #48 #282)
+#200 := (and #34 #36)
+#203 := (or #35 #200)
+#222 := (ite #203 #39 #217)
+#197 := (= 0::Int f3)
+#225 := (ite #197 0::Int #222)
+#238 := (= 3::Int #225)
+#284 := (iff #238 #282)
+#278 := (= 3::Int #275)
+#281 := (iff #278 #282)
+#283 := [rewrite]: #281
+#279 := (iff #238 #278)
+#276 := (= #225 #275)
+#273 := (= #222 #272)
+#270 := (iff #203 #269)
+#267 := (iff #200 #259)
+#262 := (and true #259)
+#265 := (iff #262 #259)
+#266 := [rewrite]: #265
+#263 := (iff #200 #262)
+#260 := (iff #36 #259)
+#261 := [rewrite]: #260
+#249 := (iff #34 true)
+#250 := [rewrite]: #249
+#264 := [monotonicity #250 #261]: #263
+#268 := [trans #264 #266]: #267
+#256 := (iff #35 #246)
+#251 := (and #246 true)
+#254 := (iff #251 #246)
+#255 := [rewrite]: #254
+#252 := (iff #35 #251)
+#247 := (iff #33 #246)
+#248 := [rewrite]: #247
+#253 := [monotonicity #248 #250]: #252
+#257 := [trans #253 #255]: #256
+#271 := [monotonicity #257 #268]: #270
#274 := [monotonicity #271]: #273
-#277 := [monotonicity #274]: #276
-#280 := [quant-intro #277]: #279
-#221 := (~ #211 #211)
-#223 := (~ #208 #208)
-#220 := [refl]: #223
-#224 := [nnf-pos #220]: #221
-#40 := (- #27)
-#39 := (- #26)
-#48 := (mod #39 #40)
-#49 := (- #48)
-#33 := (< 0::Int #27)
-#35 := (< #26 0::Int)
-#36 := (and #35 #33)
-#32 := (< 0::Int #26)
-#34 := (and #32 #33)
-#37 := (or #34 #36)
-#50 := (ite #37 #47 #49)
-#51 := (ite #29 0::Int #50)
-#52 := (ite #30 #26 #51)
-#53 := (= #46 #52)
-#54 := (forall (vars (?v0 Int) (?v1 Int)) #53)
-#214 := (iff #54 #211)
-#102 := (and #33 #35)
-#105 := (or #34 #102)
-#184 := (ite #105 #47 #179)
-#93 := (= 0::Int #26)
-#187 := (ite #93 0::Int #184)
-#96 := (= 0::Int #27)
-#190 := (ite #96 #26 #187)
-#193 := (= #46 #190)
-#196 := (forall (vars (?v0 Int) (?v1 Int)) #193)
-#212 := (iff #196 #211)
-#209 := (iff #193 #208)
-#206 := (= #190 #205)
-#203 := (= #187 #202)
-#200 := (= #184 #199)
-#155 := (iff #105 #154)
-#152 := (iff #102 #151)
-#149 := (iff #35 #148)
-#150 := [rewrite]: #149
-#142 := (iff #33 #141)
-#143 := [rewrite]: #142
-#153 := [monotonicity #143 #150]: #152
-#145 := (iff #34 #144)
-#138 := (iff #32 #137)
-#139 := [rewrite]: #138
-#146 := [monotonicity #139 #143]: #145
-#156 := [monotonicity #146 #153]: #155
-#201 := [monotonicity #156]: #200
-#130 := (iff #93 #29)
-#131 := [rewrite]: #130
-#204 := [monotonicity #131 #201]: #203
-#132 := (iff #96 #30)
-#133 := [rewrite]: #132
-#207 := [monotonicity #133 #204]: #206
-#210 := [monotonicity #207]: #209
-#213 := [quant-intro #210]: #212
-#197 := (iff #54 #196)
-#194 := (iff #53 #193)
-#191 := (= #52 #190)
-#188 := (= #51 #187)
-#185 := (= #50 #184)
-#182 := (= #49 #179)
-#176 := (- #173)
-#180 := (= #176 #179)
-#181 := [rewrite]: #180
-#177 := (= #49 #176)
-#174 := (= #48 #173)
-#113 := (= #40 #112)
-#114 := [rewrite]: #113
-#110 := (= #39 #109)
-#111 := [rewrite]: #110
-#175 := [monotonicity #111 #114]: #174
-#178 := [monotonicity #175]: #177
-#183 := [trans #178 #181]: #182
-#106 := (iff #37 #105)
-#103 := (iff #36 #102)
-#104 := [rewrite]: #103
-#107 := [monotonicity #104]: #106
-#186 := [monotonicity #107 #183]: #185
-#94 := (iff #29 #93)
-#95 := [rewrite]: #94
-#189 := [monotonicity #95 #186]: #188
-#97 := (iff #30 #96)
-#98 := [rewrite]: #97
-#192 := [monotonicity #98 #189]: #191
-#195 := [monotonicity #192]: #194
-#198 := [quant-intro #195]: #197
-#215 := [trans #198 #213]: #214
-#172 := [asserted]: #54
-#216 := [mp #172 #215]: #211
-#225 := [mp~ #216 #224]: #211
-#281 := [mp #225 #280]: #278
-#312 := [mp #281 #311]: #309
-#796 := [mp #312 #795]: #791
-#584 := (not #791)
-#641 := (or #584 #630)
-#718 := (* -1::Int 4::Int)
-#705 := (mod #482 #718)
-#707 := (+ #16 #705)
-#699 := (= #707 0::Int)
-#706 := (<= 4::Int 0::Int)
-#711 := (or #706 #710)
-#700 := (not #711)
-#702 := (or #701 #706)
-#703 := (not #702)
-#697 := (or #703 #700)
-#704 := (ite #697 #709 #699)
-#691 := (ite #689 #688 #704)
-#692 := (= f4 #16)
-#693 := (= 4::Int 0::Int)
-#694 := (ite #693 #692 #691)
-#644 := (or #584 #694)
-#646 := (iff #644 #641)
-#647 := (iff #641 #641)
-#627 := [rewrite]: #647
-#639 := (iff #694 #630)
-#525 := (ite false #692 #630)
-#638 := (iff #525 #630)
-#643 := [rewrite]: #638
-#636 := (iff #694 #525)
-#631 := (iff #691 #630)
-#651 := (iff #704 #656)
-#654 := (iff #699 #653)
-#649 := (= #707 #648)
-#666 := (= #705 #660)
-#664 := (= #718 -4::Int)
-#665 := [rewrite]: #664
-#652 := [monotonicity #665]: #666
-#650 := [monotonicity #652]: #649
-#655 := [monotonicity #650]: #654
-#661 := (iff #697 #659)
-#680 := (iff #700 #669)
-#678 := (iff #711 #710)
-#673 := (or false #710)
-#676 := (iff #673 #710)
-#677 := [rewrite]: #676
-#674 := (iff #711 #673)
-#681 := (iff #706 false)
-#682 := [rewrite]: #681
-#675 := [monotonicity #682]: #674
-#679 := [trans #675 #677]: #678
-#658 := [monotonicity #679]: #680
-#671 := (iff #703 #670)
-#667 := (iff #702 #701)
-#684 := (or #701 false)
-#683 := (iff #684 #701)
-#687 := [rewrite]: #683
-#685 := (iff #702 #684)
-#686 := [monotonicity #682]: #685
-#668 := [trans #686 #687]: #667
-#672 := [monotonicity #668]: #671
-#662 := [monotonicity #672 #658]: #661
-#657 := [monotonicity #662 #655]: #651
-#632 := [monotonicity #657]: #631
-#690 := (iff #693 false)
-#695 := [rewrite]: #690
-#637 := [monotonicity #695 #632]: #636
-#640 := [trans #637 #643]: #639
-#642 := [monotonicity #640]: #646
-#573 := [trans #642 #627]: #646
-#645 := [quant-inst #8 #15]: #644
-#628 := [mp #645 #573]: #641
-#1048 := [unit-resolution #628 #796]: #630
-#589 := (not #630)
-#591 := (or #589 #590 #688)
-#592 := [def-axiom]: #591
-#1047 := [unit-resolution #592 #1048]: #1027
-#1043 := [unit-resolution #1047 #412]: #590
-#957 := (or #689 #656)
-#593 := (or #589 #689 #656)
-#594 := [def-axiom]: #593
-#964 := [unit-resolution #594 #1048]: #957
-#1033 := [unit-resolution #964 #1043]: #656
-#635 := (not #659)
-#860 := [hypothesis]: #635
-#609 := (or #659 #701)
-#633 := [def-axiom]: #609
-#861 := [unit-resolution #633 #860]: #701
-#634 := (or #659 #710)
-#629 := [def-axiom]: #634
-#862 := [unit-resolution #629 #860]: #710
-#863 := (or #689 #670 #669)
-#864 := [th-lemma arith triangle-eq]: #863
-#913 := [unit-resolution #864 #862 #861 #1043]: false
-#914 := [lemma #913]: #659
-#611 := (not #656)
-#613 := (or #611 #635 #709)
-#614 := [def-axiom]: #613
-#1165 := [unit-resolution #614 #914 #1033]: #709
-#605 := (not #709)
-#1054 := (or #605 #600)
-#1055 := [th-lemma arith triangle-eq]: #1054
-#1236 := [unit-resolution #1055 #1165]: #600
-#1237 := [hypothesis]: #722
-#1170 := (* -1::Int #1112)
-#1035 := (* -2::Int #865)
-#1171 := (+ #1035 #1170)
-#1155 := (* -1::Int #811)
-#1172 := (+ #1155 #1171)
-#1173 := (+ #698 #1172)
-#1174 := (+ #459 #1173)
-#1175 := (+ #16 #1174)
-#1176 := (+ #12 #1175)
-#1177 := (+ f5 #1176)
-#1178 := (+ f4 #1177)
-#1179 := (>= #1178 2::Int)
-#1191 := (not #1179)
-#955 := (>= #576 0::Int)
-#1184 := [hypothesis]: #720
-#1240 := (or #577 #1239 #1193)
-#561 := (<= #16 3::Int)
-#968 := (or #967 #561)
-#966 := [th-lemma arith triangle-eq]: #968
-#970 := [unit-resolution #966 #75]: #561
-#888 := (<= #883 0::Int)
-#975 := (or #974 #888)
-#976 := [th-lemma arith triangle-eq]: #975
-#982 := [unit-resolution #976 #973]: #888
-#580 := (<= f5 0::Int)
-#556 := (= f5 0::Int)
-#1059 := (not #577)
-#1146 := [hypothesis]: #1059
-#1222 := (or #556 #577)
-#376 := (* -1::Int f5)
-#521 := (mod #376 -2::Int)
-#523 := (+ #22 #521)
-#508 := (= #523 0::Int)
-#546 := (not #580)
-#578 := (>= f5 0::Int)
-#526 := (not #578)
-#536 := (or #526 #546)
-#511 := (ite #536 #577 #508)
-#1066 := (not #556)
-#1207 := [hypothesis]: #1066
-#1201 := (or #556 #511)
-#555 := (= #22 0::Int)
-#514 := (ite #556 #555 #511)
-#382 := (or #584 #514)
-#370 := (* -1::Int 2::Int)
-#570 := (mod #376 #370)
-#571 := (+ #22 #570)
-#572 := (= #571 0::Int)
-#440 := (<= 2::Int 0::Int)
-#579 := (or #440 #578)
-#562 := (not #579)
-#550 := (or #580 #440)
-#551 := (not #550)
-#552 := (or #551 #562)
-#553 := (ite #552 #577 #572)
-#557 := (ite #556 #555 #553)
-#400 := (= f5 #22)
-#781 := (= 2::Int 0::Int)
-#558 := (ite #781 #400 #557)
-#383 := (or #584 #558)
-#371 := (iff #383 #382)
-#375 := (iff #382 #382)
-#797 := [rewrite]: #375
-#498 := (iff #558 #514)
-#517 := (ite false #400 #514)
-#495 := (iff #517 #514)
-#497 := [rewrite]: #495
-#506 := (iff #558 #517)
-#515 := (iff #557 #514)
-#512 := (iff #553 #511)
-#509 := (iff #572 #508)
-#505 := (= #571 #523)
-#522 := (= #570 #521)
-#750 := (= #370 -2::Int)
-#754 := [rewrite]: #750
-#520 := [monotonicity #754]: #522
-#507 := [monotonicity #520]: #505
-#510 := [monotonicity #507]: #509
-#533 := (iff #552 #536)
-#531 := (or #546 #526)
-#529 := (iff #531 #536)
-#532 := [rewrite]: #529
-#535 := (iff #552 #531)
-#527 := (iff #562 #526)
-#534 := (iff #579 #578)
-#540 := (or false #578)
-#539 := (iff #540 #578)
-#544 := [rewrite]: #539
-#542 := (iff #579 #540)
-#758 := (iff #440 false)
-#421 := [rewrite]: #758
-#543 := [monotonicity #421]: #542
-#524 := [trans #543 #544]: #534
-#530 := [monotonicity #524]: #527
-#549 := (iff #551 #546)
-#547 := (iff #550 #580)
-#554 := (or #580 false)
-#541 := (iff #554 #580)
-#545 := [rewrite]: #541
-#559 := (iff #550 #554)
-#538 := [monotonicity #421]: #559
-#548 := [trans #538 #545]: #547
-#537 := [monotonicity #548]: #549
-#528 := [monotonicity #537 #530]: #535
-#519 := [trans #528 #532]: #533
-#513 := [monotonicity #519 #510]: #512
-#516 := [monotonicity #513]: #515
-#782 := (iff #781 false)
-#772 := [rewrite]: #782
-#518 := [monotonicity #772 #516]: #506
-#499 := [trans #518 #497]: #498
-#372 := [monotonicity #499]: #371
-#798 := [trans #372 #797]: #371
-#384 := [quant-inst #9 #11]: #383
-#799 := [mp #384 #798]: #382
-#1156 := [unit-resolution #799 #796]: #514
-#1028 := (not #514)
-#1034 := (or #1028 #556 #511)
-#1070 := [def-axiom]: #1034
-#1202 := [unit-resolution #1070 #1156]: #1201
-#1208 := [unit-resolution #1202 #1207]: #511
-#1205 := (or #578 #577)
-#1147 := [hypothesis]: #526
-#388 := (or #536 #578)
-#389 := [def-axiom]: #388
-#1148 := [unit-resolution #389 #1147]: #536
-#1149 := (or #1066 #578)
-#1150 := [th-lemma arith triangle-eq]: #1149
-#1133 := [unit-resolution #1150 #1147]: #1066
-#1203 := [unit-resolution #1202 #1133]: #511
-#917 := (not #536)
-#836 := (not #511)
-#1025 := (or #836 #917 #577)
-#1026 := [def-axiom]: #1025
-#1204 := [unit-resolution #1026 #1203 #1148 #1146]: false
-#1206 := [lemma #1204]: #1205
-#1209 := [unit-resolution #1206 #1146]: #578
-#1217 := (or #556 #546 #526)
-#1218 := [th-lemma arith triangle-eq]: #1217
-#1219 := [unit-resolution #1218 #1207 #1209]: #546
-#915 := (or #536 #580)
-#916 := [def-axiom]: #915
-#1220 := [unit-resolution #916 #1219]: #536
-#1221 := [unit-resolution #1026 #1220 #1208 #1146]: false
-#1223 := [lemma #1221]: #1222
-#1226 := [unit-resolution #1223 #1146]: #556
-#1227 := (or #1066 #580)
-#1228 := [th-lemma arith triangle-eq]: #1227
-#1229 := [unit-resolution #1228 #1226]: #580
-#599 := (<= #12 0::Int)
-#1186 := (or #622 #599)
-#1187 := [th-lemma arith triangle-eq]: #1186
-#1188 := [unit-resolution #1187 #74]: #599
-#1105 := (<= #831 0::Int)
-#1181 := (or #1180 #1105)
-#1182 := [th-lemma arith triangle-eq]: #1181
-#1183 := [unit-resolution #1182 #1169]: #1105
-#569 := (<= #708 0::Int)
-#1050 := (or #605 #569)
-#1051 := [th-lemma arith triangle-eq]: #1050
-#1166 := [unit-resolution #1051 #1165]: #569
-#1238 := [th-lemma arith gcd-test -1/2 -1/2 -1/2 -1/2 -1/2 -1/2 -1/2 -1/2 -1/2 -1/2 -1/2 -1/2 -1/2 -1/2 #1237 #1184 #1236 #1166 #1235 #1183 #1232 #1188 #1209 #1229 #998 #982 #995 #970]: false
-#1241 := [lemma #1238]: #1240
-#1250 := [unit-resolution #1241 #1237 #1184]: #577
-#1251 := (or #1059 #955)
-#1252 := [th-lemma arith triangle-eq]: #1251
-#1253 := [unit-resolution #1252 #1250]: #955
-#1104 := (>= #22 1::Int)
-#1152 := (not #1104)
-#1254 := (or #1059 #954)
-#1255 := [th-lemma arith triangle-eq]: #1254
-#1256 := [unit-resolution #1255 #1250]: #954
-#1140 := (>= #574 2::Int)
-#1141 := (not #1140)
-#1257 := (or false #1141)
-#1258 := [th-lemma arith]: #1257
-#1259 := [unit-resolution #1258 #72]: #1141
-#1260 := (not #954)
-#1261 := (or #1103 #1140 #1260)
-#1262 := [th-lemma arith assign-bounds 1 1]: #1261
-#1263 := [unit-resolution #1262 #1259 #1256]: #1103
-#1266 := (not #1103)
-#1269 := (or #1266 #1152)
-#23 := (= #22 1::Int)
-#219 := (not #23)
-#19 := (f3 f4 2::Int)
-#21 := (= #19 1::Int)
-#1097 := (or #635 #21)
-#918 := (div f4 2::Int)
-#1036 := (* -1::Int #918)
-#1037 := (+ #1035 #1036)
-#1038 := (+ #698 #1037)
-#483 := (mod f4 2::Int)
-#484 := (* -1::Int #483)
-#1039 := (+ #484 #1038)
-#1040 := (+ #16 #1039)
-#1041 := (+ f4 #1040)
-#1042 := (>= #1041 2::Int)
-#1030 := (not #1042)
-#1045 := [hypothesis]: #659
-#1049 := [unit-resolution #614 #1045 #1033]: #709
-#1052 := [unit-resolution #1051 #1049]: #569
-#988 := (not #569)
-#1031 := (or #1030 #988)
-#940 := (>= #483 0::Int)
-#1023 := (or false #940)
-#1024 := [th-lemma arith]: #1023
-#1021 := [unit-resolution #1024 #72]: #940
-#983 := [hypothesis]: #569
-#931 := (* -2::Int #918)
-#932 := (+ #484 #931)
-#933 := (+ f4 #932)
-#938 := (<= #933 0::Int)
-#930 := (= #933 0::Int)
-#1011 := (or false #930)
-#1010 := [th-lemma arith]: #1011
-#1009 := [unit-resolution #1010 #72]: #930
-#958 := (not #930)
-#959 := (or #958 #938)
-#965 := [th-lemma arith triangle-eq]: #959
-#963 := [unit-resolution #965 #1009]: #938
-#1022 := [hypothesis]: #1042
-#1029 := [th-lemma arith farkas -1 2 -1 -1 -1 1 #970 #1022 #982 #963 #983 #1021]: false
-#1032 := [lemma #1029]: #1031
-#1053 := [unit-resolution #1032 #1052]: #1030
-#1056 := [unit-resolution #1055 #1049]: #600
-#939 := (>= #933 0::Int)
-#1064 := (or #958 #939)
-#1065 := [th-lemma arith triangle-eq]: #1064
-#1068 := [unit-resolution #1065 #1009]: #939
-#485 := (+ #19 #484)
-#385 := (>= #485 0::Int)
-#477 := (= #485 0::Int)
-#500 := (mod #482 -2::Int)
-#504 := (+ #19 #500)
-#491 := (= #504 0::Int)
-#478 := (ite #659 #477 #491)
-#464 := (= #19 0::Int)
-#420 := (ite #689 #464 #478)
-#411 := (or #584 #420)
-#493 := (mod #482 #370)
-#492 := (+ #19 #493)
-#494 := (= #492 0::Int)
-#469 := (or #440 #710)
-#470 := (not #469)
-#471 := (or #701 #440)
-#463 := (not #471)
-#472 := (or #463 #470)
-#473 := (ite #472 #477 #494)
-#474 := (ite #689 #464 #473)
-#441 := (= f4 #19)
-#443 := (ite #781 #441 #474)
-#386 := (or #584 #443)
-#391 := (iff #386 #411)
-#398 := (iff #411 #411)
-#399 := [rewrite]: #398
-#410 := (iff #443 #420)
-#413 := (ite false #441 #420)
-#406 := (iff #413 #420)
-#407 := [rewrite]: #406
-#416 := (iff #443 #413)
-#414 := (iff #474 #420)
-#488 := (iff #473 #478)
-#486 := (iff #494 #491)
-#489 := (= #492 #504)
-#503 := (= #493 #500)
-#496 := [monotonicity #754]: #503
-#490 := [monotonicity #496]: #489
-#487 := [monotonicity #490]: #486
-#501 := (iff #472 #659)
-#438 := (iff #470 #669)
-#453 := (iff #469 #710)
-#452 := (iff #469 #673)
-#442 := [monotonicity #421]: #452
-#436 := [trans #442 #677]: #453
+#243 := (iff #197 #32)
+#244 := [rewrite]: #243
+#277 := [monotonicity #244 #274]: #276
+#280 := [monotonicity #277]: #279
+#285 := [trans #280 #283]: #284
+#241 := (iff #48 #238)
+#235 := (= #225 3::Int)
+#239 := (iff #235 #238)
+#240 := [rewrite]: #239
+#236 := (iff #48 #235)
+#233 := (= #46 #225)
+#228 := (ite false f3 #225)
+#231 := (= #228 #225)
+#232 := [rewrite]: #231
+#229 := (= #46 #228)
+#226 := (= #45 #225)
+#223 := (= #44 #222)
+#220 := (= #43 #217)
+#214 := (- #211)
+#218 := (= #214 #217)
+#219 := [rewrite]: #218
+#215 := (= #43 #214)
+#212 := (= #42 #211)
+#209 := (= #41 -4::Int)
+#210 := [rewrite]: #209
+#206 := (= #40 #108)
+#207 := [rewrite]: #206
+#213 := [monotonicity #207 #210]: #212
+#216 := [monotonicity #213]: #215
+#221 := [trans #216 #219]: #220
+#204 := (iff #38 #203)
+#201 := (iff #37 #200)
+#202 := [rewrite]: #201
+#205 := [monotonicity #202]: #204
+#224 := [monotonicity #205 #221]: #223
+#198 := (iff #32 #197)
+#199 := [rewrite]: #198
+#227 := [monotonicity #199 #224]: #226
+#195 := (iff #31 false)
+#196 := [rewrite]: #195
+#230 := [monotonicity #196 #227]: #229
+#234 := [trans #230 #232]: #233
+#237 := [monotonicity #234]: #236
+#242 := [trans #237 #240]: #241
+#287 := [trans #242 #285]: #286
+#194 := [asserted]: #48
+#288 := [mp #194 #287]: #282
+#883 := (= #39 #275)
+#495 := (= #272 #275)
+#509 := (not #32)
+#494 := (= #275 0::Int)
+#829 := (not #494)
+#608 := (= 3::Int 0::Int)
+#610 := (iff #608 false)
+#827 := [rewrite]: #610
+#606 := [hypothesis]: #494
+#607 := [symm #288]: #278
+#609 := [trans #607 #606]: #608
+#828 := [mp #609 #827]: false
+#830 := [lemma #828]: #829
+#510 := (or #509 #494)
+#511 := [def-axiom]: #510
+#831 := [unit-resolution #511 #830]: #509
+#512 := (or #32 #495)
+#513 := [def-axiom]: #512
+#881 := [unit-resolution #513 #831]: #495
+#496 := (= #39 #272)
+#502 := (not #269)
+#666 := [hypothesis]: #502
+#498 := (or #269 #245)
+#499 := [def-axiom]: #498
+#667 := [unit-resolution #499 #666]: #245
+#500 := (or #269 #258)
+#501 := [def-axiom]: #500
+#813 := [unit-resolution #501 #666]: #258
+#814 := (or #32 #246 #259)
+#832 := [th-lemma arith triangle-eq]: #814
+#865 := [unit-resolution #832 #813 #667 #831]: false
+#866 := [lemma #865]: #269
+#505 := (or #502 #496)
+#506 := [def-axiom]: #505
+#882 := [unit-resolution #506 #866]: #496
+#884 := [trans #882 #881]: #883
+#885 := [trans #884 #288]: #872
+#886 := (not #872)
+#887 := (or #886 #613)
+#888 := [th-lemma arith triangle-eq]: #887
+#889 := [unit-resolution #888 #885]: #613
+#8 := 2::Int
+decl f4 :: Int
+#12 := f4
+#13 := (+ f3 f4)
+#614 := (div #13 2::Int)
+#113 := -2::Int
+#632 := (* -2::Int #614)
+#21 := (mod #13 2::Int)
+#631 := (* -1::Int #21)
+#633 := (+ #631 #632)
+#634 := (+ f4 #633)
+#635 := (+ f3 #634)
+#639 := (<= #635 0::Int)
+#629 := (= #635 0::Int)
+#735 := (or false #629)
+#736 := [th-lemma arith]: #735
+#737 := [unit-resolution #736 #93]: #629
+#738 := (not #629)
+#739 := (or #738 #639)
+#740 := [th-lemma arith triangle-eq]: #739
+#741 := [unit-resolution #740 #737]: #639
+#640 := (>= #635 0::Int)
+#742 := (or #738 #640)
+#743 := [th-lemma arith triangle-eq]: #742
+#744 := [unit-resolution #743 #737]: #640
+#710 := (<= #21 0::Int)
+#709 := (= #21 0::Int)
+#109 := (* -1::Int f4)
+#110 := (+ #108 #109)
+#116 := (mod #110 -2::Int)
+#122 := (* -1::Int #116)
+#163 := (>= #13 0::Int)
+#164 := (not #163)
+#150 := (<= #13 0::Int)
+#151 := (not #150)
+#174 := (or #151 #164)
+#177 := (ite #174 #21 #122)
+#14 := (= #13 0::Int)
+#180 := (ite #14 0::Int #177)
+#187 := (= #180 0::Int)
+#23 := (- 2::Int)
+#22 := (- #13)
+#24 := (mod #22 #23)
+#25 := (- #24)
+#16 := (< 0::Int 2::Int)
+#18 := (< #13 0::Int)
+#19 := (and #18 #16)
+#15 := (< 0::Int #13)
+#17 := (and #15 #16)
+#20 := (or #17 #19)
+#26 := (ite #20 #21 #25)
+#27 := (ite #14 0::Int #26)
+#10 := (= 2::Int 0::Int)
+#28 := (ite #10 #13 #27)
+#29 := (= #28 0::Int)
+#191 := (iff #29 #187)
+#101 := (and #16 #18)
+#104 := (or #17 #101)
+#127 := (ite #104 #21 #122)
+#98 := (= 0::Int #13)
+#130 := (ite #98 0::Int #127)
+#143 := (= 0::Int #130)
+#189 := (iff #143 #187)
+#183 := (= 0::Int #180)
+#186 := (iff #183 #187)
+#188 := [rewrite]: #186
+#184 := (iff #143 #183)
+#181 := (= #130 #180)
+#178 := (= #127 #177)
+#175 := (iff #104 #174)
+#172 := (iff #101 #164)
+#167 := (and true #164)
+#170 := (iff #167 #164)
+#171 := [rewrite]: #170
+#168 := (iff #101 #167)
+#165 := (iff #18 #164)
+#166 := [rewrite]: #165
+#154 := (iff #16 true)
+#155 := [rewrite]: #154
+#169 := [monotonicity #155 #166]: #168
+#173 := [trans #169 #171]: #172
+#161 := (iff #17 #151)
+#156 := (and #151 true)
+#159 := (iff #156 #151)
+#160 := [rewrite]: #159
+#157 := (iff #17 #156)
+#152 := (iff #15 #151)
+#153 := [rewrite]: #152
+#158 := [monotonicity #153 #155]: #157
+#162 := [trans #158 #160]: #161
+#176 := [monotonicity #162 #173]: #175
+#179 := [monotonicity #176]: #178
+#148 := (iff #98 #14)
+#149 := [rewrite]: #148
+#182 := [monotonicity #149 #179]: #181
+#185 := [monotonicity #182]: #184
+#190 := [trans #185 #188]: #189
+#146 := (iff #29 #143)
+#140 := (= #130 0::Int)
+#144 := (iff #140 #143)
+#145 := [rewrite]: #144
+#141 := (iff #29 #140)
+#138 := (= #28 #130)
+#133 := (ite false #13 #130)
+#136 := (= #133 #130)
+#137 := [rewrite]: #136
+#134 := (= #28 #133)
+#131 := (= #27 #130)
+#128 := (= #26 #127)
+#125 := (= #25 #122)
+#119 := (- #116)
+#123 := (= #119 #122)
+#124 := [rewrite]: #123
+#120 := (= #25 #119)
+#117 := (= #24 #116)
+#114 := (= #23 -2::Int)
+#115 := [rewrite]: #114
+#111 := (= #22 #110)
+#112 := [rewrite]: #111
+#118 := [monotonicity #112 #115]: #117
+#121 := [monotonicity #118]: #120
+#126 := [trans #121 #124]: #125
+#105 := (iff #20 #104)
+#102 := (iff #19 #101)
+#103 := [rewrite]: #102
+#106 := [monotonicity #103]: #105
+#129 := [monotonicity #106 #126]: #128
+#99 := (iff #14 #98)
+#100 := [rewrite]: #99
+#132 := [monotonicity #100 #129]: #131
+#96 := (iff #10 false)
+#97 := [rewrite]: #96
+#135 := [monotonicity #97 #132]: #134
+#139 := [trans #135 #137]: #138
+#142 := [monotonicity #139]: #141
+#147 := [trans #142 #145]: #146
+#192 := [trans #147 #190]: #191
+#95 := [asserted]: #29
+#193 := [mp #95 #192]: #187
+#757 := (= #21 #180)
+#475 := (= #177 #180)
+#489 := (not #14)
+#423 := (>= f4 0::Int)
+#424 := (not #423)
+#412 := (<= f4 0::Int)
+#413 := (not #412)
+#434 := (or #413 #424)
+#534 := (not #434)
+#58 := 1::Int
+#66 := (mod f4 2::Int)
+#834 := (>= #66 1::Int)
+#837 := (not #834)
+#904 := (= #66 1::Int)
+#957 := (not #904)
+#345 := (mod #109 -2::Int)
+#351 := (* -1::Int #345)
+#437 := (ite #434 #66 #351)
+#60 := (= f4 0::Int)
+#440 := (ite #60 0::Int #437)
+#447 := (= #440 1::Int)
+#468 := (not #447)
+#958 := (iff #468 #957)
+#955 := (iff #447 #904)
+#953 := (iff #904 #447)
+#951 := (= #66 #440)
+#527 := (= #437 #440)
+#541 := (not #60)
+#552 := [hypothesis]: #434
+#895 := (or #541 #534)
+#558 := [hypothesis]: #60
+#553 := (or #541 #412)
+#554 := [th-lemma arith triangle-eq]: #553
+#555 := [unit-resolution #554 #558]: #412
+#559 := (or #541 #423)
+#892 := [th-lemma arith triangle-eq]: #559
+#893 := [unit-resolution #892 #558]: #423
+#535 := (or #534 #413 #424)
+#536 := [def-axiom]: #535
+#894 := [unit-resolution #536 #893 #555 #552]: false
+#896 := [lemma #894]: #895
+#947 := [unit-resolution #896 #552]: #541
+#544 := (or #60 #527)
+#545 := [def-axiom]: #544
+#948 := [unit-resolution #545 #947]: #527
+#528 := (= #66 #437)
+#537 := (or #534 #528)
+#538 := [def-axiom]: #537
+#946 := [unit-resolution #538 #552]: #528
+#952 := [trans #946 #948]: #951
+#954 := [monotonicity #952]: #953
+#956 := [symm #954]: #955
+#959 := [monotonicity #956]: #958
+#299 := (mod #108 -2::Int)
+#305 := (* -1::Int #299)
+#52 := (mod f3 2::Int)
+#396 := (ite #269 #52 #305)
+#399 := (ite #32 0::Int #396)
+#406 := (= #399 1::Int)
+#708 := (>= #52 1::Int)
+#669 := (div f3 2::Int)
+#683 := (* -2::Int #669)
+#682 := (* -1::Int #52)
+#684 := (+ #682 #683)
+#685 := (+ f3 #684)
+#556 := (<= #685 0::Int)
+#681 := (= #685 0::Int)
+#551 := (or false #681)
+#560 := [th-lemma arith]: #551
+#561 := [unit-resolution #560 #93]: #681
+#874 := (not #681)
+#875 := (or #874 #556)
+#876 := [th-lemma arith triangle-eq]: #875
+#877 := [unit-resolution #876 #561]: #556
+#557 := (>= #685 0::Int)
+#878 := (or #874 #557)
+#879 := [th-lemma arith triangle-eq]: #878
+#880 := [unit-resolution #879 #561]: #557
+#716 := (not #708)
+#717 := [hypothesis]: #716
+#692 := (>= #52 0::Int)
+#718 := (or false #692)
+#719 := [th-lemma arith]: #718
+#720 := [unit-resolution #719 #93]: #692
+#890 := [th-lemma arith gcd-test 1/4 1/4 1/4 1/4 -1/4 -1/4 -1/4 -1/4 #889 #733 #730 #727 #720 #717 #880 #877]: false
+#891 := [lemma #890]: #708
+#938 := (or #406 #716)
+#515 := (= #396 #399)
+#524 := (or #32 #515)
+#525 := [def-axiom]: #524
+#936 := [unit-resolution #525 #831]: #515
+#516 := (= #52 #396)
+#518 := (or #502 #516)
+#519 := [def-axiom]: #518
+#937 := [unit-resolution #519 #866]: #516
+#785 := (not #516)
+#784 := (not #515)
+#803 := (or #406 #784 #785 #716)
+#690 := (= #52 1::Int)
+#707 := (<= #52 1::Int)
+#788 := (not #707)
+#789 := [hypothesis]: #788
+#698 := (>= #52 2::Int)
+#699 := (not #698)
+#790 := (or false #699)
+#791 := [th-lemma arith]: #790
+#792 := [unit-resolution #791 #93]: #699
+#793 := [th-lemma arith farkas 1 1 #792 #789]: false
+#794 := [lemma #793]: #707
+#797 := [hypothesis]: #708
+#798 := (or #690 #788 #716)
+#799 := [th-lemma arith triangle-eq]: #798
+#800 := [unit-resolution #799 #797 #794]: #690
+#780 := (= #399 #52)
+#778 := (= #396 #52)
+#774 := [hypothesis]: #516
+#779 := [symm #774]: #778
+#776 := (= #399 #396)
+#775 := [hypothesis]: #515
+#777 := [symm #775]: #776
+#781 := [trans #777 #779]: #780
+#801 := [trans #781 #800]: #406
+#467 := (not #406)
+#796 := [hypothesis]: #467
+#802 := [unit-resolution #796 #801]: false
+#804 := [lemma #802]: #803
+#939 := [unit-resolution #804 #937 #936]: #938
+#944 := [unit-resolution #939 #891]: #406
+#461 := (or #467 #468)
+#451 := (and #406 #447)
+#454 := (not #451)
+#472 := (iff #454 #461)
+#462 := (not #461)
+#463 := (not #462)
+#470 := (iff #463 #461)
+#471 := [rewrite]: #470
+#464 := (iff #454 #463)
+#465 := (iff #451 #462)
+#466 := [rewrite]: #465
+#469 := [monotonicity #466]: #464
+#473 := [trans #469 #471]: #472
+#67 := (- f4)
+#68 := (mod #67 #23)
+#69 := (- #68)
+#63 := (< f4 0::Int)
+#64 := (and #63 #16)
+#61 := (< 0::Int f4)
+#62 := (and #61 #16)
+#65 := (or #62 #64)
+#70 := (ite #65 #66 #69)
+#71 := (ite #60 0::Int #70)
+#72 := (ite #10 f4 #71)
+#73 := (= #72 1::Int)
+#53 := (mod #40 #23)
+#54 := (- #53)
+#50 := (and #36 #16)
+#49 := (and #33 #16)
+#51 := (or #49 #50)
+#55 := (ite #51 #52 #54)
+#56 := (ite #32 0::Int #55)
+#57 := (ite #10 f3 #56)
+#59 := (= #57 1::Int)
+#74 := (and #59 #73)
+#75 := (not #74)
+#457 := (iff #75 #454)
+#337 := (and #16 #63)
+#334 := (and #16 #61)
+#340 := (or #334 #337)
+#356 := (ite #340 #66 #351)
+#331 := (= 0::Int f4)
+#359 := (ite #331 0::Int #356)
+#372 := (= 1::Int #359)
+#293 := (and #16 #36)
+#290 := (and #16 #33)
+#296 := (or #290 #293)
+#310 := (ite #296 #52 #305)
+#313 := (ite #197 0::Int #310)
+#326 := (= 1::Int #313)
+#377 := (and #326 #372)
+#380 := (not #377)
+#455 := (iff #380 #454)
+#452 := (iff #377 #451)
+#449 := (iff #372 #447)
+#443 := (= 1::Int #440)
+#446 := (iff #443 #447)
+#448 := [rewrite]: #446
+#444 := (iff #372 #443)
+#441 := (= #359 #440)
+#438 := (= #356 #437)
+#435 := (iff #340 #434)
+#432 := (iff #337 #424)
+#427 := (and true #424)
+#430 := (iff #427 #424)
+#431 := [rewrite]: #430
+#428 := (iff #337 #427)
+#425 := (iff #63 #424)
+#426 := [rewrite]: #425
+#429 := [monotonicity #155 #426]: #428
+#433 := [trans #429 #431]: #432
+#421 := (iff #334 #413)
+#416 := (and true #413)
+#419 := (iff #416 #413)
+#420 := [rewrite]: #419
+#417 := (iff #334 #416)
+#414 := (iff #61 #413)
+#415 := [rewrite]: #414
+#418 := [monotonicity #155 #415]: #417
+#422 := [trans #418 #420]: #421
+#436 := [monotonicity #422 #433]: #435
#439 := [monotonicity #436]: #438
-#450 := (iff #463 #670)
-#448 := (iff #471 #701)
-#444 := (iff #471 #684)
-#435 := [monotonicity #421]: #444
-#449 := [trans #435 #687]: #448
-#451 := [monotonicity #449]: #450
-#502 := [monotonicity #451 #439]: #501
-#418 := [monotonicity #502 #487]: #488
-#415 := [monotonicity #418]: #414
-#404 := [monotonicity #772 #415]: #416
-#405 := [trans #404 #407]: #410
-#396 := [monotonicity #405]: #391
-#401 := [trans #396 #399]: #391
-#390 := [quant-inst #8 #11]: #386
-#397 := [mp #390 #401]: #411
-#1069 := [unit-resolution #397 #796]: #420
-#379 := (not #420)
-#1072 := (or #379 #478)
-#373 := (or #379 #689 #478)
-#374 := [def-axiom]: #373
-#1073 := [unit-resolution #374 #1043]: #1072
-#1074 := [unit-resolution #1073 #1069]: #478
-#392 := (not #478)
-#393 := (or #392 #635 #477)
-#394 := [def-axiom]: #393
-#1075 := [unit-resolution #394 #1045 #1074]: #477
-#380 := (not #477)
-#1076 := (or #380 #385)
-#1077 := [th-lemma arith triangle-eq]: #1076
-#1078 := [unit-resolution #1077 #1075]: #385
-#801 := (>= #19 1::Int)
-#1015 := (not #801)
-#800 := (<= #19 1::Int)
-#946 := (>= #483 2::Int)
-#947 := (not #946)
-#1079 := (or false #947)
-#1080 := [th-lemma arith]: #1079
-#1081 := [unit-resolution #1080 #72]: #947
-#402 := (<= #485 0::Int)
-#1082 := (or #380 #402)
-#1083 := [th-lemma arith triangle-eq]: #1082
-#1084 := [unit-resolution #1083 #1075]: #402
-#1085 := (not #402)
-#1086 := (or #800 #946 #1085)
-#1087 := [th-lemma arith assign-bounds 1 1]: #1086
-#1088 := [unit-resolution #1087 #1084 #1081]: #800
-#1090 := (not #800)
-#1093 := (or #1090 #1015)
-#218 := (not #21)
-#1089 := [hypothesis]: #218
-#1091 := (or #21 #1090 #1015)
-#1092 := [th-lemma arith triangle-eq]: #1091
-#1094 := [unit-resolution #1092 #1089]: #1093
-#1095 := [unit-resolution #1094 #1088]: #1015
-#1096 := [th-lemma arith farkas -1/2 -1/2 1/2 -1/2 -1/2 -1/2 1 #995 #998 #1095 #1078 #1068 #1056 #1053]: false
-#1098 := [lemma #1096]: #1097
-#1264 := [unit-resolution #1098 #914]: #21
-#230 := (or #218 #219)
-#24 := (and #21 #23)
-#25 := (not #24)
-#239 := (iff #25 #230)
-#231 := (not #230)
-#234 := (not #231)
-#237 := (iff #234 #230)
-#238 := [rewrite]: #237
-#235 := (iff #25 #234)
-#232 := (iff #24 #231)
-#233 := [rewrite]: #232
-#236 := [monotonicity #233]: #235
-#240 := [trans #236 #238]: #239
-#76 := [asserted]: #25
-#241 := [mp #76 #240]: #230
-#1265 := [unit-resolution #241 #1264]: #219
-#1267 := (or #23 #1266 #1152)
-#1268 := [th-lemma arith triangle-eq]: #1267
-#1270 := [unit-resolution #1268 #1265]: #1269
-#1271 := [unit-resolution #1270 #1263]: #1152
-#1192 := (not #955)
-#1194 := (or #1191 #1192 #1193 #1104)
-#1153 := [hypothesis]: #1152
-#1132 := (<= #1127 0::Int)
-#1160 := [unit-resolution #1159 #72]: #1124
-#1162 := (or #1161 #1132)
-#1163 := [th-lemma arith triangle-eq]: #1162
-#1164 := [unit-resolution #1163 #1160]: #1132
-#1185 := [hypothesis]: #1179
-#1189 := [hypothesis]: #955
-#1190 := [th-lemma arith farkas -1 1 -2 1 1 1 1 1 1 1 #1189 #1188 #1185 #1184 #1183 #1166 #1164 #982 #970 #1153]: false
-#1195 := [lemma #1190]: #1194
-#1272 := [unit-resolution #1195 #1271 #1184 #1253]: #1191
-#1273 := [th-lemma arith farkas -2 1 1 1 1 1 1 1 1 #1272 #1237 #1236 #1235 #1232 #998 #995 #1249 #1151]: false
-#1275 := [lemma #1273]: #1274
-#1349 := [unit-resolution #1275 #1278]: #1348
-#1350 := [unit-resolution #1349 #1323 #1110]: false
-#1351 := [lemma #1350]: #715
-#1281 := (or #778 #457)
-#1225 := [hypothesis]: #715
-#752 := (+ #482 #376)
-#751 := (mod #752 -2::Int)
-#466 := (+ #12 #751)
-#746 := (= #466 0::Int)
-#770 := (not #461)
-#434 := (<= #10 0::Int)
-#764 := (not #434)
-#479 := (or #764 #770)
-#744 := (ite #479 #457 #746)
-#618 := (not #778)
-#802 := [hypothesis]: #618
-#1243 := (or #778 #744)
-#749 := (ite #778 #14 #744)
-#585 := (or #584 #749)
-#454 := (* -1::Int #10)
-#455 := (mod #454 #370)
-#456 := (+ #12 #455)
-#447 := (= #456 0::Int)
-#775 := (or #440 #461)
-#777 := (not #775)
-#564 := (or #434 #440)
-#771 := (not #564)
-#445 := (or #771 #777)
-#446 := (ite #445 #457 #447)
-#779 := (ite #778 #14 #446)
-#780 := (= #10 #12)
-#776 := (ite #781 #780 #779)
-#586 := (or #584 #776)
-#729 := (iff #586 #585)
-#731 := (iff #585 #585)
-#725 := [rewrite]: #731
-#737 := (iff #776 #749)
-#432 := (* -1::Int #12)
-#437 := (+ f5 #432)
-#773 := (+ f4 #437)
-#433 := (= #773 0::Int)
-#740 := (ite false #433 #749)
-#741 := (iff #740 #749)
-#742 := [rewrite]: #741
-#735 := (iff #776 #740)
-#738 := (iff #779 #749)
-#748 := (iff #446 #744)
-#747 := (iff #447 #746)
-#467 := (= #456 #466)
-#755 := (= #455 #751)
-#753 := (= #454 #752)
-#475 := [rewrite]: #753
-#465 := [monotonicity #475 #754]: #755
-#468 := [monotonicity #465]: #467
-#462 := [monotonicity #468]: #747
-#480 := (iff #445 #479)
-#756 := (iff #777 #770)
-#769 := (iff #775 #461)
-#403 := (or false #461)
-#408 := (iff #403 #461)
-#409 := [rewrite]: #408
-#766 := (iff #775 #403)
-#768 := [monotonicity #421]: #766
-#767 := [trans #768 #409]: #769
-#757 := [monotonicity #767]: #756
-#759 := (iff #771 #764)
-#762 := (iff #564 #434)
-#422 := (or #434 false)
-#760 := (iff #422 #434)
-#761 := [rewrite]: #760
-#423 := (iff #564 #422)
-#424 := [monotonicity #421]: #423
-#763 := [trans #424 #761]: #762
-#765 := [monotonicity #763]: #759
-#481 := [monotonicity #765 #757]: #480
-#745 := [monotonicity #481 #462]: #748
-#739 := [monotonicity #745]: #738
-#774 := (iff #780 #433)
-#417 := [rewrite]: #774
-#736 := [monotonicity #772 #417 #739]: #735
-#743 := [trans #736 #742]: #737
-#730 := [monotonicity #743]: #729
-#726 := [trans #730 #725]: #729
-#728 := [quant-inst #10 #11]: #586
-#732 := [mp #728 #726]: #585
-#1242 := [unit-resolution #732 #796]: #749
-#616 := (not #749)
-#620 := (or #616 #778 #744)
-#621 := [def-axiom]: #620
-#1244 := [unit-resolution #621 #1242]: #1243
-#1245 := [unit-resolution #1244 #802]: #744
-#809 := (or #479 #778)
-#565 := (not #479)
-#803 := [hypothesis]: #565
-#733 := (or #479 #434)
-#727 := [def-axiom]: #733
-#804 := [unit-resolution #727 #803]: #434
-#734 := (or #479 #461)
-#563 := [def-axiom]: #734
-#805 := [unit-resolution #563 #803]: #461
-#806 := (or #778 #764 #770)
-#807 := [th-lemma arith triangle-eq]: #806
-#808 := [unit-resolution #807 #805 #804 #802]: false
-#810 := [lemma #808]: #809
-#1279 := [unit-resolution #810 #802]: #479
-#724 := (not #744)
-#606 := (or #724 #565 #457)
-#607 := [def-axiom]: #606
-#1280 := [unit-resolution #607 #1279 #1245 #1225]: false
-#1282 := [lemma #1280]: #1281
-#1352 := [unit-resolution #1282 #1351]: #778
-#1353 := (or #618 #461)
-#1354 := [th-lemma arith triangle-eq]: #1353
-#1355 := [unit-resolution #1354 #1352]: #461
-#1356 := (or #618 #434)
-#1357 := [th-lemma arith triangle-eq]: #1356
-#1358 := [unit-resolution #1357 #1352]: #434
-#1346 := (or #577 #770 #764)
-#1295 := [hypothesis]: #434
-#1327 := (or #526 #764 #701)
-#1005 := [hypothesis]: #670
-#1289 := [hypothesis]: #578
-#1291 := [th-lemma arith farkas -1 1 1 #1295 #1289 #1005]: false
-#1328 := [lemma #1291]: #1327
-#1342 := [unit-resolution #1328 #1209 #1295]: #701
-#1343 := [unit-resolution #864 #1043]: #659
-#1344 := [unit-resolution #1343 #1342]: #669
-#1290 := [hypothesis]: #461
-#1345 := [th-lemma arith farkas -1 1 1 #1290 #1344 #1229]: false
-#1347 := [lemma #1345]: #1346
-#1359 := [unit-resolution #1347 #1358 #1355]: #577
-#1360 := [unit-resolution #1255 #1359]: #954
-#1361 := (or #1103 #1260)
-#1302 := [hypothesis]: #1140
-#1308 := [unit-resolution #1258 #72 #1302]: false
-#1321 := [lemma #1308]: #1141
-#1362 := [unit-resolution #1262 #1321]: #1361
-#1363 := [unit-resolution #1362 #1360]: #1103
-#1303 := (+ #698 #1171)
-#1326 := (+ #575 #1303)
-#1335 := (+ #16 #1326)
-#1336 := (+ f5 #1335)
-#1337 := (+ f4 #1336)
-#1338 := (>= #1337 2::Int)
-#1329 := (not #1338)
-#1330 := (or #1329 #764)
-#1294 := [unit-resolution #1163 #1278]: #1132
-#1310 := [hypothesis]: #1338
-#1309 := [th-lemma arith farkas 2 -1 -1 -1 -1 -1 1 #1310 #1295 #1166 #982 #970 #1294 #1151]: false
-#1331 := [lemma #1309]: #1330
-#1364 := [unit-resolution #1331 #1358]: #1329
-#1365 := [unit-resolution #1252 #1359]: #955
-#1340 := (or #1192 #1338 #770 #1104)
-#1332 := [unit-resolution #1248 #1278]: #1224
-#1325 := [th-lemma arith #1290 #1153 #1189 #1236 #998 #995 #1332]: #1338
-#1324 := [hypothesis]: #1329
-#1339 := [unit-resolution #1324 #1325]: false
-#1341 := [lemma #1339]: #1340
-#1366 := [unit-resolution #1341 #1365 #1355 #1364]: #1104
-[unit-resolution #1270 #1366 #1363]: false
+#410 := (iff #331 #60)
+#411 := [rewrite]: #410
+#442 := [monotonicity #411 #439]: #441
+#445 := [monotonicity #442]: #444
+#450 := [trans #445 #448]: #449
+#408 := (iff #326 #406)
+#402 := (= 1::Int #399)
+#405 := (iff #402 #406)
+#407 := [rewrite]: #405
+#403 := (iff #326 #402)
+#400 := (= #313 #399)
+#397 := (= #310 #396)
+#394 := (iff #296 #269)
+#392 := (iff #293 #259)
+#390 := (iff #293 #262)
+#391 := [monotonicity #155 #261]: #390
+#393 := [trans #391 #266]: #392
+#388 := (iff #290 #246)
+#383 := (and true #246)
+#386 := (iff #383 #246)
+#387 := [rewrite]: #386
+#384 := (iff #290 #383)
+#385 := [monotonicity #155 #248]: #384
+#389 := [trans #385 #387]: #388
+#395 := [monotonicity #389 #393]: #394
+#398 := [monotonicity #395]: #397
+#401 := [monotonicity #244 #398]: #400
+#404 := [monotonicity #401]: #403
+#409 := [trans #404 #407]: #408
+#453 := [monotonicity #409 #450]: #452
+#456 := [monotonicity #453]: #455
+#381 := (iff #75 #380)
+#378 := (iff #74 #377)
+#375 := (iff #73 #372)
+#369 := (= #359 1::Int)
+#373 := (iff #369 #372)
+#374 := [rewrite]: #373
+#370 := (iff #73 #369)
+#367 := (= #72 #359)
+#362 := (ite false f4 #359)
+#365 := (= #362 #359)
+#366 := [rewrite]: #365
+#363 := (= #72 #362)
+#360 := (= #71 #359)
+#357 := (= #70 #356)
+#354 := (= #69 #351)
+#348 := (- #345)
+#352 := (= #348 #351)
+#353 := [rewrite]: #352
+#349 := (= #69 #348)
+#346 := (= #68 #345)
+#343 := (= #67 #109)
+#344 := [rewrite]: #343
+#347 := [monotonicity #344 #115]: #346
+#350 := [monotonicity #347]: #349
+#355 := [trans #350 #353]: #354
+#341 := (iff #65 #340)
+#338 := (iff #64 #337)
+#339 := [rewrite]: #338
+#335 := (iff #62 #334)
+#336 := [rewrite]: #335
+#342 := [monotonicity #336 #339]: #341
+#358 := [monotonicity #342 #355]: #357
+#332 := (iff #60 #331)
+#333 := [rewrite]: #332
+#361 := [monotonicity #333 #358]: #360
+#364 := [monotonicity #97 #361]: #363
+#368 := [trans #364 #366]: #367
+#371 := [monotonicity #368]: #370
+#376 := [trans #371 #374]: #375
+#329 := (iff #59 #326)
+#323 := (= #313 1::Int)
+#327 := (iff #323 #326)
+#328 := [rewrite]: #327
+#324 := (iff #59 #323)
+#321 := (= #57 #313)
+#316 := (ite false f3 #313)
+#319 := (= #316 #313)
+#320 := [rewrite]: #319
+#317 := (= #57 #316)
+#314 := (= #56 #313)
+#311 := (= #55 #310)
+#308 := (= #54 #305)
+#302 := (- #299)
+#306 := (= #302 #305)
+#307 := [rewrite]: #306
+#303 := (= #54 #302)
+#300 := (= #53 #299)
+#301 := [monotonicity #207 #115]: #300
+#304 := [monotonicity #301]: #303
+#309 := [trans #304 #307]: #308
+#297 := (iff #51 #296)
+#294 := (iff #50 #293)
+#295 := [rewrite]: #294
+#291 := (iff #49 #290)
+#292 := [rewrite]: #291
+#298 := [monotonicity #292 #295]: #297
+#312 := [monotonicity #298 #309]: #311
+#315 := [monotonicity #199 #312]: #314
+#318 := [monotonicity #97 #315]: #317
+#322 := [trans #318 #320]: #321
+#325 := [monotonicity #322]: #324
+#330 := [trans #325 #328]: #329
+#379 := [monotonicity #330 #376]: #378
+#382 := [monotonicity #379]: #381
+#458 := [trans #382 #456]: #457
+#289 := [asserted]: #75
+#459 := [mp #289 #458]: #454
+#474 := [mp #459 #473]: #461
+#945 := [unit-resolution #474 #944]: #468
+#960 := [mp #945 #959]: #957
+#963 := (or #904 #837)
+#833 := (<= #66 1::Int)
+#858 := (not #833)
+#859 := [hypothesis]: #858
+#821 := (>= #66 2::Int)
+#822 := (not #821)
+#860 := (or false #822)
+#861 := [th-lemma arith]: #860
+#862 := [unit-resolution #861 #93]: #822
+#863 := [th-lemma arith farkas 1 1 #862 #859]: false
+#864 := [lemma #863]: #833
+#961 := (or #904 #858 #837)
+#962 := [th-lemma arith triangle-eq]: #961
+#964 := [unit-resolution #962 #864]: #963
+#965 := [unit-resolution #964 #960]: #837
+#909 := (or #151 #834)
+#906 := [hypothesis]: #150
+#838 := [hypothesis]: #837
+#931 := (or #163 #834)
+#705 := (div f4 2::Int)
+#806 := (* -2::Int #705)
+#805 := (* -1::Int #66)
+#807 := (+ #805 #806)
+#808 := (+ f4 #807)
+#897 := (<= #808 0::Int)
+#795 := (= #808 0::Int)
+#911 := (or false #795)
+#913 := [th-lemma arith]: #911
+#914 := [unit-resolution #913 #93]: #795
+#915 := (not #795)
+#916 := (or #915 #897)
+#917 := [th-lemma arith triangle-eq]: #916
+#918 := [unit-resolution #917 #914]: #897
+#898 := (>= #808 0::Int)
+#919 := (or #915 #898)
+#920 := [th-lemma arith triangle-eq]: #919
+#921 := [unit-resolution #920 #914]: #898
+#815 := (>= #66 0::Int)
+#839 := (or false #815)
+#840 := [th-lemma arith]: #839
+#841 := [unit-resolution #840 #93]: #815
+#922 := [hypothesis]: #164
+#751 := (or #489 #163)
+#752 := [th-lemma arith triangle-eq]: #751
+#923 := [unit-resolution #752 #922]: #489
+#492 := (or #14 #475)
+#493 := [def-axiom]: #492
+#924 := [unit-resolution #493 #923]: #475
+#476 := (= #21 #177)
+#480 := (or #174 #163)
+#481 := [def-axiom]: #480
+#925 := [unit-resolution #481 #922]: #174
+#482 := (not #174)
+#485 := (or #482 #476)
+#486 := [def-axiom]: #485
+#926 := [unit-resolution #486 #925]: #476
+#927 := [trans #926 #924]: #757
+#928 := [trans #927 #193]: #709
+#760 := (not #709)
+#761 := (or #760 #710)
+#762 := [th-lemma arith triangle-eq]: #761
+#929 := [unit-resolution #762 #928]: #710
+#641 := (>= #21 0::Int)
+#764 := (or false #641)
+#765 := [th-lemma arith]: #764
+#766 := [unit-resolution #765 #93]: #641
+#930 := [th-lemma arith gcd-test 1/2 1/2 1/2 1/2 -1/2 -1/2 -1/2 -1/2 -1/2 -1/2 -1/2 -1/2 #766 #929 #744 #741 #889 #733 #730 #727 #841 #838 #921 #918]: false
+#932 := [lemma #930]: #931
+#907 := [unit-resolution #932 #838]: #163
+#908 := [th-lemma arith gcd-test 1/2 1/2 1/2 1/2 -1/2 -1/2 1/2 1/2 1/2 1/2 #841 #838 #921 #918 #907 #906 #889 #733 #730 #727]: false
+#910 := [lemma #908]: #909
+#966 := [unit-resolution #910 #965]: #151
+#967 := (or #489 #150)
+#968 := [th-lemma arith triangle-eq]: #967
+#969 := [unit-resolution #968 #966]: #489
+#970 := [unit-resolution #493 #969]: #475
+#478 := (or #174 #150)
+#479 := [def-axiom]: #478
+#971 := [unit-resolution #479 #966]: #174
+#972 := [unit-resolution #486 #971]: #476
+#973 := [trans #972 #970]: #757
+#974 := [trans #973 #193]: #709
+#975 := [unit-resolution #762 #974]: #710
+#976 := [th-lemma arith gcd-test 1/2 1/2 1/2 1/2 1/2 1/2 1/2 1/2 1/2 1/2 1/2 1/2 #841 #965 #921 #918 #889 #733 #730 #727 #766 #975 #744 #741]: false
+#977 := [lemma #976]: #534
+#532 := (or #434 #423)
+#533 := [def-axiom]: #532
+#836 := [unit-resolution #533 #977]: #423
+#845 := (or #434 #258)
+#769 := (not #613)
+#770 := (or #434 #769 #258)
+#734 := [hypothesis]: #613
+#745 := [hypothesis]: #259
+#746 := [hypothesis]: #534
+#530 := (or #434 #412)
+#531 := [def-axiom]: #530
+#747 := [unit-resolution #531 #746]: #412
+#748 := (or #164 #258 #413)
+#749 := [th-lemma arith assign-bounds -1 -1]: #748
+#750 := [unit-resolution #749 #747 #745]: #164
+#753 := [unit-resolution #752 #750]: #489
+#754 := [unit-resolution #493 #753]: #475
+#755 := [unit-resolution #481 #750]: #174
+#756 := [unit-resolution #486 #755]: #476
+#758 := [trans #756 #754]: #757
+#759 := [trans #758 #193]: #709
+#763 := [unit-resolution #762 #759]: #710
+#767 := [unit-resolution #533 #746]: #423
+#768 := [th-lemma arith gcd-test -1/2 -1/2 1/2 1/2 1/2 1/2 -1/2 -1/2 -1/2 -1/2 #767 #747 #766 #763 #744 #741 #734 #733 #730 #727]: false
+#771 := [lemma #768]: #770
+#846 := [unit-resolution #771 #889]: #845
+#847 := [unit-resolution #846 #977]: #258
+#503 := (or #502 #246 #259)
+#504 := [def-axiom]: #503
+#844 := [unit-resolution #504 #866]: #269
+#848 := [unit-resolution #844 #847]: #246
+#849 := (or #151 #424 #245)
+#850 := [th-lemma arith assign-bounds -1 -1]: #849
+#851 := [unit-resolution #850 #848 #836]: #151
+#842 := [unit-resolution #968 #851]: #489
+#843 := [unit-resolution #493 #842]: #475
+#852 := [unit-resolution #479 #851]: #174
+#853 := [unit-resolution #486 #852]: #476
+#854 := [trans #853 #843]: #757
+#855 := [trans #854 #193]: #709
+#856 := [unit-resolution #762 #855]: #710
+#857 := [unit-resolution #531 #977]: #412
+[th-lemma arith gcd-test -1/2 -1/2 1/2 1/2 1/2 1/2 -1/2 -1/2 -1/2 -1/2 #836 #857 #766 #856 #744 #741 #889 #733 #730 #727]: false
unsat
c04d38458726eb1b2cafd52bd3881d6f8160666f 24 0
#2 := false
@@ -10440,288 +10061,318 @@
unsat
ERROR: line 11 column 83: invalid pattern.
-8f616b17d0807409dc26bfdf9593c5fcd06fb7e7 1 0
-unsat
-3eb9cf11ee8774c9212c37c265e7552f3b8f24a9 75 0
-#2 := false
-#10 := 1::Int
-decl f5 :: Int
-#12 := f5
-#16 := (+ f5 1::Int)
-decl f3 :: Int
-#8 := f3
-#17 := (* f3 #16)
-decl f4 :: Int
-#9 := f4
-#15 := (* f3 f4)
-#18 := (+ #15 #17)
-#11 := (+ f4 1::Int)
-#13 := (+ #11 f5)
-#14 := (* f3 #13)
-#19 := (= #14 #18)
-#20 := (not #19)
-#93 := (iff #20 false)
-#1 := true
-#88 := (not true)
-#91 := (iff #88 false)
-#92 := [rewrite]: #91
-#89 := (iff #20 #88)
-#86 := (iff #19 true)
-#56 := (* f3 f5)
-#57 := (+ #15 #56)
-#58 := (+ f3 #57)
-#81 := (= #58 #58)
-#84 := (iff #81 true)
-#85 := [rewrite]: #84
-#82 := (iff #19 #81)
-#79 := (= #18 #58)
-#69 := (+ f3 #56)
-#74 := (+ #15 #69)
-#77 := (= #74 #58)
-#78 := [rewrite]: #77
-#75 := (= #18 #74)
-#72 := (= #17 #69)
-#63 := (+ 1::Int f5)
-#66 := (* f3 #63)
-#70 := (= #66 #69)
-#71 := [rewrite]: #70
-#67 := (= #17 #66)
-#64 := (= #16 #63)
-#65 := [rewrite]: #64
-#68 := [monotonicity #65]: #67
-#73 := [trans #68 #71]: #72
-#76 := [monotonicity #73]: #75
-#80 := [trans #76 #78]: #79
-#61 := (= #14 #58)
-#47 := (+ f4 f5)
-#48 := (+ 1::Int #47)
-#53 := (* f3 #48)
-#59 := (= #53 #58)
-#60 := [rewrite]: #59
-#54 := (= #14 #53)
-#51 := (= #13 #48)
-#41 := (+ 1::Int f4)
-#44 := (+ #41 f5)
-#49 := (= #44 #48)
-#50 := [rewrite]: #49
-#45 := (= #13 #44)
-#42 := (= #11 #41)
-#43 := [rewrite]: #42
-#46 := [monotonicity #43]: #45
-#52 := [trans #46 #50]: #51
-#55 := [monotonicity #52]: #54
-#62 := [trans #55 #60]: #61
-#83 := [monotonicity #62 #80]: #82
-#87 := [trans #83 #85]: #86
-#90 := [monotonicity #87]: #89
-#94 := [trans #90 #92]: #93
-#40 := [asserted]: #20
-[mp #40 #94]: false
-unsat
-741a564e40e4b6610d1d47bdab19a223e004482a 62 0
+8aba3814871680009d1d0267516334493c303e78 175 0
#2 := false
-decl f4 :: Real
-#10 := f4
-decl f3 :: Real
-#8 := f3
-#16 := 2::Real
-#17 := (* 2::Real f3)
-#18 := (* #17 f4)
-#9 := 1::Real
-#13 := (- 1::Real f4)
-#14 := (* f3 #13)
-#11 := (+ 1::Real f4)
-#12 := (* f3 #11)
-#15 := (- #12 #14)
-#19 := (= #15 #18)
-#20 := (not #19)
-#81 := (iff #20 false)
-#1 := true
-#76 := (not true)
-#79 := (iff #76 false)
-#80 := [rewrite]: #79
-#77 := (iff #20 #76)
-#74 := (iff #19 true)
-#41 := (* f3 f4)
-#63 := (* 2::Real #41)
-#69 := (= #63 #63)
-#72 := (iff #69 true)
-#73 := [rewrite]: #72
-#70 := (iff #19 #69)
-#67 := (= #18 #63)
-#68 := [rewrite]: #67
-#65 := (= #15 #63)
-#45 := -1::Real
-#53 := (* -1::Real #41)
-#54 := (+ f3 #53)
-#42 := (+ f3 #41)
-#59 := (- #42 #54)
-#62 := (= #59 #63)
-#64 := [rewrite]: #62
-#60 := (= #15 #59)
-#57 := (= #14 #54)
-#46 := (* -1::Real f4)
-#47 := (+ 1::Real #46)
-#50 := (* f3 #47)
-#55 := (= #50 #54)
-#56 := [rewrite]: #55
-#51 := (= #14 #50)
-#48 := (= #13 #47)
-#49 := [rewrite]: #48
-#52 := [monotonicity #49]: #51
-#58 := [trans #52 #56]: #57
-#43 := (= #12 #42)
-#44 := [rewrite]: #43
-#61 := [monotonicity #44 #58]: #60
-#66 := [trans #61 #64]: #65
-#71 := [monotonicity #66 #68]: #70
-#75 := [trans #71 #73]: #74
-#78 := [monotonicity #75]: #77
-#82 := [trans #78 #80]: #81
-#40 := [asserted]: #20
-[mp #40 #82]: false
-unsat
-06d1bd5308956fb019ef1c09bf97c6326d872fd6 141 0
-#2 := false
-decl f6 :: Int
-#13 := f6
-decl f7 :: Int
-#17 := f7
-decl f5 :: Int
-#12 := f5
-#28 := (+ f5 f7)
-#29 := (+ #28 f6)
+#8 := 0::Int
decl f4 :: Int
-#10 := f4
-#9 := 1::Int
-#11 := (+ 1::Int f4)
-#30 := (* #11 #29)
-#25 := (* f7 f4)
-#23 := (* #11 f7)
-#14 := (+ f5 f6)
-#20 := 2::Int
-#21 := (* 2::Int #11)
-#22 := (* #21 #14)
-#24 := (+ #22 #23)
-#26 := (+ #24 #25)
-decl f3 :: Int
-#8 := f3
-#27 := (+ f3 #26)
-#31 := (- #27 #30)
-#18 := (* f4 f7)
-#15 := (* #11 #14)
-#16 := (+ f3 #15)
-#19 := (+ #16 #18)
-#32 := (= #19 #31)
-#33 := (not #32)
-#157 := (iff #33 false)
-#1 := true
-#152 := (not true)
-#155 := (iff #152 false)
-#156 := [rewrite]: #155
-#153 := (iff #33 #152)
-#150 := (iff #32 true)
-#55 := (* f4 f6)
-#54 := (* f4 f5)
+#18 := f4
+#138 := (<= f4 0::Int)
+#139 := (not #138)
+decl f5 :: Int
+#20 := f5
+#134 := (<= f5 0::Int)
+#135 := (not #134)
+decl f3 :: (-> Int Int Int)
+#21 := (f3 f4 f5)
+#123 := (<= #21 0::Int)
+#155 := (or #123 #135 #138)
+#160 := (not #155)
+#23 := (< 0::Int f5)
+#22 := (< 0::Int #21)
+#24 := (implies #22 #23)
+#19 := (< 0::Int f4)
+#25 := (implies #19 #24)
+#26 := (not #25)
+#163 := (iff #26 #160)
+#107 := (not #22)
+#108 := (or #107 #23)
+#114 := (not #19)
+#115 := (or #114 #108)
+#120 := (not #115)
+#161 := (iff #120 #160)
+#158 := (iff #115 #155)
+#149 := (or #123 #135)
+#152 := (or #138 #149)
+#156 := (iff #152 #155)
+#157 := [rewrite]: #156
+#153 := (iff #115 #152)
+#150 := (iff #108 #149)
+#136 := (iff #23 #135)
+#137 := [rewrite]: #136
+#132 := (iff #107 #123)
+#124 := (not #123)
+#127 := (not #124)
+#130 := (iff #127 #123)
+#131 := [rewrite]: #130
+#128 := (iff #107 #127)
+#125 := (iff #22 #124)
+#126 := [rewrite]: #125
+#129 := [monotonicity #126]: #128
+#133 := [trans #129 #131]: #132
+#151 := [monotonicity #133 #137]: #150
+#147 := (iff #114 #138)
+#142 := (not #139)
+#145 := (iff #142 #138)
+#146 := [rewrite]: #145
+#143 := (iff #114 #142)
+#140 := (iff #19 #139)
+#141 := [rewrite]: #140
+#144 := [monotonicity #141]: #143
+#148 := [trans #144 #146]: #147
+#154 := [monotonicity #148 #151]: #153
+#159 := [trans #154 #157]: #158
+#162 := [monotonicity #159]: #161
+#121 := (iff #26 #120)
+#118 := (iff #25 #115)
+#111 := (implies #19 #108)
+#116 := (iff #111 #115)
+#117 := [rewrite]: #116
+#112 := (iff #25 #111)
+#109 := (iff #24 #108)
+#110 := [rewrite]: #109
+#113 := [monotonicity #110]: #112
+#119 := [trans #113 #117]: #118
+#122 := [monotonicity #119]: #121
+#164 := [trans #122 #162]: #163
+#106 := [asserted]: #26
+#165 := [mp #106 #164]: #160
+#168 := [not-or-elim #165]: #139
+#167 := [not-or-elim #165]: #134
+#166 := [not-or-elim #165]: #124
+#10 := (:var 0 Int)
+#9 := (:var 1 Int)
+#11 := (f3 #9 #10)
+#647 := (pattern #11)
+#78 := (<= #11 0::Int)
+#74 := (<= #10 0::Int)
+#75 := (not #74)
+#63 := (<= #9 0::Int)
+#95 := (or #63 #75 #78)
+#648 := (forall (vars (?v0 Int) (?v1 Int)) (:pat #647) #95)
+#100 := (forall (vars (?v0 Int) (?v1 Int)) #95)
+#651 := (iff #100 #648)
+#649 := (iff #95 #95)
+#650 := [refl]: #649
+#652 := [quant-intro #650]: #651
+#182 := (~ #100 #100)
+#180 := (~ #95 #95)
+#181 := [refl]: #180
+#183 := [nnf-pos #181]: #182
+#14 := (< 0::Int #10)
+#13 := (< 0::Int #9)
+#15 := (implies #13 #14)
+#12 := (< 0::Int #11)
+#16 := (implies #12 #15)
+#17 := (forall (vars (?v0 Int) (?v1 Int)) #16)
+#103 := (iff #17 #100)
+#47 := (not #13)
+#48 := (or #47 #14)
+#54 := (not #12)
+#55 := (or #54 #48)
+#60 := (forall (vars (?v0 Int) (?v1 Int)) #55)
+#101 := (iff #60 #100)
+#98 := (iff #55 #95)
+#89 := (or #63 #75)
+#92 := (or #78 #89)
+#96 := (iff #92 #95)
+#97 := [rewrite]: #96
+#93 := (iff #55 #92)
+#90 := (iff #48 #89)
+#76 := (iff #14 #75)
+#77 := [rewrite]: #76
+#72 := (iff #47 #63)
+#64 := (not #63)
+#67 := (not #64)
+#70 := (iff #67 #63)
+#71 := [rewrite]: #70
+#68 := (iff #47 #67)
+#65 := (iff #13 #64)
+#66 := [rewrite]: #65
+#69 := [monotonicity #66]: #68
+#73 := [trans #69 #71]: #72
+#91 := [monotonicity #73 #77]: #90
+#87 := (iff #54 #78)
+#79 := (not #78)
+#82 := (not #79)
+#85 := (iff #82 #78)
+#86 := [rewrite]: #85
+#83 := (iff #54 #82)
+#80 := (iff #12 #79)
+#81 := [rewrite]: #80
+#84 := [monotonicity #81]: #83
+#88 := [trans #84 #86]: #87
+#94 := [monotonicity #88 #91]: #93
+#99 := [trans #94 #97]: #98
+#102 := [quant-intro #99]: #101
+#61 := (iff #17 #60)
+#58 := (iff #16 #55)
+#51 := (implies #12 #48)
+#56 := (iff #51 #55)
+#57 := [rewrite]: #56
+#52 := (iff #16 #51)
+#49 := (iff #15 #48)
+#50 := [rewrite]: #49
+#53 := [monotonicity #50]: #52
+#59 := [trans #53 #57]: #58
+#62 := [quant-intro #59]: #61
+#104 := [trans #62 #102]: #103
+#46 := [asserted]: #17
+#105 := [mp #46 #104]: #100
+#170 := [mp~ #105 #183]: #100
+#653 := [mp #170 #652]: #648
+#319 := (not #648)
+#310 := (or #319 #123 #135 #138)
+#232 := (or #138 #135 #123)
+#321 := (or #319 #232)
+#639 := (iff #321 #310)
+#250 := (or #319 #155)
+#324 := (iff #250 #310)
+#303 := [rewrite]: #324
+#323 := (iff #321 #250)
+#317 := (iff #232 #155)
+#318 := [rewrite]: #317
+#320 := [monotonicity #318]: #323
+#641 := [trans #320 #303]: #639
+#322 := [quant-inst #18 #20]: #321
+#297 := [mp #322 #641]: #310
+[unit-resolution #297 #653 #166 #167 #168]: false
+unsat
+0db52837dc3c07a6a4d5ca34a945edf7aeac1fdf 136 0
+#2 := false
+#58 := 0::Int
+decl f3 :: (-> Int Int Int)
+decl f6 :: Int
+#22 := f6
+#20 := 1::Int
+#80 := (+ 1::Int f6)
+decl f4 :: Int
+#18 := f4
+#83 := (f3 f4 #80)
+decl f5 :: Int
+#19 := f5
+#71 := (+ f5 f6)
+#72 := (+ 1::Int #71)
+#77 := (f3 f4 #72)
+#53 := -1::Int
+#99 := (* -1::Int #77)
+#100 := (+ #99 #83)
+#25 := (f3 f4 f5)
+#101 := (+ #25 #100)
+#97 := (= #101 0::Int)
+#98 := (not #97)
+#26 := (+ f6 1::Int)
+#27 := (f3 f4 #26)
+#28 := (+ #25 #27)
+#21 := (+ f5 1::Int)
+#23 := (+ #21 f6)
+#24 := (f3 f4 #23)
+#29 := (= #24 #28)
+#30 := (not #29)
+#104 := (iff #30 #98)
+#86 := (+ #25 #83)
+#89 := (= #77 #86)
+#92 := (not #89)
+#102 := (iff #92 #98)
+#96 := (iff #89 #97)
+#95 := [rewrite]: #96
+#103 := [monotonicity #95]: #102
+#93 := (iff #30 #92)
+#90 := (iff #29 #89)
+#87 := (= #28 #86)
+#84 := (= #27 #83)
+#81 := (= #26 #80)
+#82 := [rewrite]: #81
+#85 := [monotonicity #82]: #84
+#88 := [monotonicity #85]: #87
+#78 := (= #24 #77)
+#75 := (= #23 #72)
+#52 := (+ 1::Int f5)
+#68 := (+ #52 f6)
+#73 := (= #68 #72)
+#74 := [rewrite]: #73
+#69 := (= #23 #68)
+#66 := (= #21 #52)
+#67 := [rewrite]: #66
+#70 := [monotonicity #67]: #69
+#76 := [trans #70 #74]: #75
+#79 := [monotonicity #76]: #78
+#91 := [monotonicity #79 #88]: #90
+#94 := [monotonicity #91]: #93
+#105 := [trans #94 #103]: #104
+#51 := [asserted]: #30
+#106 := [mp #51 #105]: #98
+#10 := (:var 0 Int)
+#8 := (:var 2 Int)
+#14 := (f3 #8 #10)
+#9 := (:var 1 Int)
+#13 := (f3 #8 #9)
+#582 := (pattern #13 #14)
+#55 := (* -1::Int #14)
+#54 := (* -1::Int #13)
#56 := (+ #54 #55)
-#67 := (+ #18 #56)
-#68 := (+ f6 #67)
-#69 := (+ f5 #68)
-#70 := (+ f3 #69)
-#144 := (= #70 #70)
-#148 := (iff #144 true)
-#149 := [rewrite]: #148
-#143 := (iff #32 #144)
-#146 := (= #31 #70)
-#131 := (+ f7 #67)
-#132 := (+ f6 #131)
-#133 := (+ f5 #132)
-#85 := (* 2::Int #55)
-#83 := (* 2::Int #54)
-#86 := (+ #83 #85)
-#112 := (* 2::Int #18)
-#113 := (+ #112 #86)
-#114 := (+ f7 #113)
-#84 := (* 2::Int f6)
-#115 := (+ #84 #114)
-#82 := (* 2::Int f5)
-#116 := (+ #82 #115)
-#121 := (+ f3 #116)
-#138 := (- #121 #133)
-#141 := (= #138 #70)
-#147 := [rewrite]: #141
-#139 := (= #31 #138)
-#136 := (= #30 #133)
-#124 := (+ f6 f7)
-#125 := (+ f5 #124)
-#128 := (* #11 #125)
-#134 := (= #128 #133)
-#135 := [rewrite]: #134
-#129 := (= #30 #128)
-#126 := (= #29 #125)
-#127 := [rewrite]: #126
-#130 := [monotonicity #127]: #129
-#137 := [trans #130 #135]: #136
-#122 := (= #27 #121)
-#119 := (= #26 #116)
-#99 := (+ #18 #86)
-#100 := (+ f7 #99)
-#101 := (+ #84 #100)
-#102 := (+ #82 #101)
-#109 := (+ #102 #18)
-#117 := (= #109 #116)
-#118 := [rewrite]: #117
-#110 := (= #26 #109)
-#107 := (= #25 #18)
-#108 := [rewrite]: #107
-#105 := (= #24 #102)
-#93 := (+ f7 #18)
-#87 := (+ #84 #86)
-#88 := (+ #82 #87)
-#96 := (+ #88 #93)
-#103 := (= #96 #102)
-#104 := [rewrite]: #103
-#97 := (= #24 #96)
-#94 := (= #23 #93)
-#95 := [rewrite]: #94
-#91 := (= #22 #88)
-#75 := (* 2::Int f4)
-#76 := (+ 2::Int #75)
-#79 := (* #76 #14)
-#89 := (= #79 #88)
-#90 := [rewrite]: #89
-#80 := (= #22 #79)
-#77 := (= #21 #76)
-#78 := [rewrite]: #77
-#81 := [monotonicity #78]: #80
-#92 := [trans #81 #90]: #91
-#98 := [monotonicity #92 #95]: #97
-#106 := [trans #98 #104]: #105
-#111 := [monotonicity #106 #108]: #110
-#120 := [trans #111 #118]: #119
-#123 := [monotonicity #120]: #122
-#140 := [monotonicity #123 #137]: #139
-#145 := [trans #140 #147]: #146
-#73 := (= #19 #70)
-#57 := (+ f6 #56)
-#58 := (+ f5 #57)
-#61 := (+ f3 #58)
-#64 := (+ #61 #18)
-#71 := (= #64 #70)
-#72 := [rewrite]: #71
-#65 := (= #19 #64)
-#62 := (= #16 #61)
-#59 := (= #15 #58)
-#60 := [rewrite]: #59
-#63 := [monotonicity #60]: #62
-#66 := [monotonicity #63]: #65
-#74 := [trans #66 #72]: #73
-#142 := [monotonicity #74 #145]: #143
-#151 := [trans #142 #149]: #150
-#154 := [monotonicity #151]: #153
-#158 := [trans #154 #156]: #157
-#53 := [asserted]: #33
-[mp #53 #158]: false
+#11 := (+ #9 #10)
+#12 := (f3 #8 #11)
+#57 := (+ #12 #56)
+#59 := (= #57 0::Int)
+#583 := (forall (vars (?v0 Int) (?v1 Int) (?v2 Int)) (:pat #582) #59)
+#62 := (forall (vars (?v0 Int) (?v1 Int) (?v2 Int)) #59)
+#586 := (iff #62 #583)
+#584 := (iff #59 #59)
+#585 := [refl]: #584
+#587 := [quant-intro #585]: #586
+#116 := (~ #62 #62)
+#114 := (~ #59 #59)
+#115 := [refl]: #114
+#117 := [nnf-pos #115]: #116
+#15 := (+ #13 #14)
+#16 := (= #12 #15)
+#17 := (forall (vars (?v0 Int) (?v1 Int) (?v2 Int)) #16)
+#63 := (iff #17 #62)
+#60 := (iff #16 #59)
+#61 := [rewrite]: #60
+#64 := [quant-intro #61]: #63
+#50 := [asserted]: #17
+#65 := [mp #50 #64]: #62
+#108 := [mp~ #65 #117]: #62
+#588 := [mp #108 #587]: #583
+#560 := (not #583)
+#415 := (or #560 #97)
+#530 := (* -1::Int #83)
+#255 := (* -1::Int #25)
+#524 := (+ #255 #530)
+#525 := (+ f5 #80)
+#531 := (f3 f4 #525)
+#532 := (+ #531 #524)
+#526 := (= #532 0::Int)
+#417 := (or #560 #526)
+#411 := (iff #417 #415)
+#420 := (iff #415 #415)
+#421 := [rewrite]: #420
+#515 := (iff #526 #97)
+#522 := (+ #77 #530)
+#520 := (+ #255 #522)
+#366 := (= #520 0::Int)
+#511 := (iff #366 #97)
+#512 := [rewrite]: #511
+#514 := (iff #526 #366)
+#406 := (= #532 #520)
+#518 := (+ #77 #524)
+#523 := (= #518 #520)
+#405 := [rewrite]: #523
+#519 := (= #532 #518)
+#364 := (= #531 #77)
+#533 := (= #525 #72)
+#362 := [rewrite]: #533
+#365 := [monotonicity #362]: #364
+#521 := [monotonicity #365]: #519
+#407 := [trans #521 #405]: #406
+#416 := [monotonicity #407]: #514
+#400 := [trans #416 #512]: #515
+#419 := [monotonicity #400]: #411
+#422 := [trans #419 #421]: #411
+#418 := [quant-inst #18 #19 #80]: #417
+#423 := [mp #418 #422]: #415
+[unit-resolution #423 #588 #106]: false
unsat
13d222fc57300189e3c05b2df538ad53757b2feb 257 0
#2 := false
@@ -13271,7 +12922,7 @@
#94 := [not-or-elim #88]: #93
[mp #94 #115]: false
unsat
-5187d9076857b0889962948031701fbc3f0e1f5d 151 0
+b9360163b10b7a2a34fb792ababcc1898c7e5b1c 138 0
#2 := false
decl f3 :: (-> S2 S2)
decl f5 :: (-> Int S2)
@@ -13282,146 +12933,133 @@
#20 := (f6 #19)
#21 := (f5 #20)
#22 := (f3 #21)
-#71 := (= #21 #22)
-#117 := (not #71)
+#70 := (= #21 #22)
+#106 := (not #70)
decl f4 :: (-> S1 S1)
decl f1 :: S1
#4 := f1
-#77 := (f4 f1)
-#83 := (= f1 #77)
-#118 := (not #83)
-#590 := [hypothesis]: #118
+#24 := (f4 f1)
+#74 := (= f1 #24)
+#107 := (not #74)
+#579 := [hypothesis]: #107
#12 := (:var 0 S1)
#13 := (f4 #12)
-#609 := (pattern #13)
-#61 := (= f1 #12)
-#57 := (= f1 #13)
-#64 := (iff #57 #61)
-#610 := (forall (vars (?v0 S1)) (:pat #609) #64)
-#67 := (forall (vars (?v0 S1)) #64)
-#613 := (iff #67 #610)
-#611 := (iff #64 #64)
-#612 := [refl]: #611
-#614 := [quant-intro #612]: #613
-#105 := (~ #67 #67)
-#104 := (~ #64 #64)
-#115 := [refl]: #104
-#106 := [nnf-pos #115]: #105
+#598 := (pattern #13)
+#60 := (= f1 #12)
+#56 := (= f1 #13)
+#63 := (iff #56 #60)
+#599 := (forall (vars (?v0 S1)) (:pat #598) #63)
+#66 := (forall (vars (?v0 S1)) #63)
+#602 := (iff #66 #599)
+#600 := (iff #63 #63)
+#601 := [refl]: #600
+#603 := [quant-intro #601]: #602
+#94 := (~ #66 #66)
+#93 := (~ #63 #63)
+#104 := [refl]: #93
+#95 := [nnf-pos #104]: #94
#15 := (= #12 f1)
#14 := (= #13 f1)
#16 := (iff #14 #15)
#17 := (forall (vars (?v0 S1)) #16)
-#68 := (iff #17 #67)
-#65 := (iff #16 #64)
-#62 := (iff #15 #61)
-#63 := [rewrite]: #62
-#59 := (iff #14 #57)
-#60 := [rewrite]: #59
-#66 := [monotonicity #60 #63]: #65
-#69 := [quant-intro #66]: #68
-#56 := [asserted]: #17
-#72 := [mp #56 #69]: #67
-#116 := [mp~ #72 #106]: #67
-#615 := [mp #116 #614]: #610
-#276 := (not #610)
-#204 := (or #276 #83)
-#184 := (= f1 f1)
-#271 := (iff #83 #184)
-#277 := (or #276 #271)
-#278 := (iff #277 #204)
-#594 := (iff #204 #204)
-#596 := [rewrite]: #594
-#264 := (iff #271 #83)
+#67 := (iff #17 #66)
+#64 := (iff #16 #63)
+#61 := (iff #15 #60)
+#62 := [rewrite]: #61
+#58 := (iff #14 #56)
+#59 := [rewrite]: #58
+#65 := [monotonicity #59 #62]: #64
+#68 := [quant-intro #65]: #67
+#55 := [asserted]: #17
+#71 := [mp #55 #68]: #66
+#105 := [mp~ #71 #95]: #66
+#604 := [mp #105 #603]: #599
+#265 := (not #599)
+#193 := (or #265 #74)
+#173 := (= f1 f1)
+#260 := (iff #74 #173)
+#266 := (or #265 #260)
+#267 := (iff #266 #193)
+#583 := (iff #193 #193)
+#585 := [rewrite]: #583
+#253 := (iff #260 #74)
#1 := true
-#88 := (iff #83 true)
-#91 := (iff #88 #83)
-#92 := [rewrite]: #91
-#186 := (iff #271 #88)
-#185 := (iff #184 true)
-#272 := [rewrite]: #185
-#273 := [monotonicity #272]: #186
-#275 := [trans #273 #92]: #264
-#257 := [monotonicity #275]: #278
-#251 := [trans #257 #596]: #278
-#274 := [quant-inst #4]: #277
-#383 := [mp #274 #251]: #204
-#262 := [unit-resolution #383 #615 #590]: false
-#263 := [lemma #262]: #83
-#107 := (or #117 #118)
-#95 := (and #71 #83)
-#98 := (not #95)
-#124 := (iff #98 #107)
-#108 := (not #107)
-#119 := (not #108)
-#122 := (iff #119 #107)
-#123 := [rewrite]: #122
-#120 := (iff #98 #119)
-#109 := (iff #95 #108)
-#110 := [rewrite]: #109
-#121 := [monotonicity #110]: #120
-#125 := [trans #121 #123]: #124
-decl f2 :: S1
-#5 := f2
-#24 := (ite true f1 f2)
-#25 := (f4 #24)
-#26 := (= #25 f1)
-#27 := (iff #26 true)
+#77 := (iff #74 true)
+#80 := (iff #77 #74)
+#81 := [rewrite]: #80
+#175 := (iff #260 #77)
+#174 := (iff #173 true)
+#261 := [rewrite]: #174
+#262 := [monotonicity #261]: #175
+#264 := [trans #262 #81]: #253
+#246 := [monotonicity #264]: #267
+#240 := [trans #246 #585]: #267
+#263 := [quant-inst #4]: #266
+#372 := [mp #263 #240]: #193
+#251 := [unit-resolution #372 #604 #579]: false
+#252 := [lemma #251]: #74
+#96 := (or #106 #107)
+#84 := (and #70 #74)
+#87 := (not #84)
+#113 := (iff #87 #96)
+#97 := (not #96)
+#108 := (not #97)
+#111 := (iff #108 #96)
+#112 := [rewrite]: #111
+#109 := (iff #87 #108)
+#98 := (iff #84 #97)
+#99 := [rewrite]: #98
+#110 := [monotonicity #99]: #109
+#114 := [trans #110 #112]: #113
+#25 := (= #24 f1)
+#26 := (iff #25 true)
#23 := (= #22 #21)
-#28 := (and #23 #27)
-#29 := (not #28)
-#99 := (iff #29 #98)
-#96 := (iff #28 #95)
-#93 := (iff #27 #83)
-#89 := (iff #27 #88)
-#86 := (iff #26 #83)
-#80 := (= #77 f1)
-#84 := (iff #80 #83)
-#85 := [rewrite]: #84
-#81 := (iff #26 #80)
-#78 := (= #25 #77)
-#75 := (= #24 f1)
+#27 := (and #23 #26)
+#28 := (not #27)
+#88 := (iff #28 #87)
+#85 := (iff #27 #84)
+#82 := (iff #26 #74)
+#78 := (iff #26 #77)
+#75 := (iff #25 #74)
#76 := [rewrite]: #75
#79 := [monotonicity #76]: #78
-#82 := [monotonicity #79]: #81
-#87 := [trans #82 #85]: #86
-#90 := [monotonicity #87]: #89
-#94 := [trans #90 #92]: #93
-#73 := (iff #23 #71)
-#74 := [rewrite]: #73
-#97 := [monotonicity #74 #94]: #96
-#100 := [monotonicity #97]: #99
-#70 := [asserted]: #29
-#103 := [mp #70 #100]: #98
-#126 := [mp #103 #125]: #107
-#597 := [unit-resolution #126 #263]: #117
+#83 := [trans #79 #81]: #82
+#72 := (iff #23 #70)
+#73 := [rewrite]: #72
+#86 := [monotonicity #73 #83]: #85
+#89 := [monotonicity #86]: #88
+#69 := [asserted]: #28
+#92 := [mp #69 #89]: #87
+#115 := [mp #92 #114]: #96
+#586 := [unit-resolution #115 #252]: #106
#8 := (:var 0 S2)
#9 := (f3 #8)
-#602 := (pattern #9)
-#50 := (= #8 #9)
-#603 := (forall (vars (?v0 S2)) (:pat #602) #50)
-#53 := (forall (vars (?v0 S2)) #50)
-#606 := (iff #53 #603)
-#604 := (iff #50 #50)
-#605 := [refl]: #604
-#607 := [quant-intro #605]: #606
-#113 := (~ #53 #53)
-#111 := (~ #50 #50)
-#112 := [refl]: #111
-#114 := [nnf-pos #112]: #113
+#591 := (pattern #9)
+#49 := (= #8 #9)
+#592 := (forall (vars (?v0 S2)) (:pat #591) #49)
+#52 := (forall (vars (?v0 S2)) #49)
+#595 := (iff #52 #592)
+#593 := (iff #49 #49)
+#594 := [refl]: #593
+#596 := [quant-intro #594]: #595
+#102 := (~ #52 #52)
+#100 := (~ #49 #49)
+#101 := [refl]: #100
+#103 := [nnf-pos #101]: #102
#10 := (= #9 #8)
#11 := (forall (vars (?v0 S2)) #10)
-#54 := (iff #11 #53)
-#51 := (iff #10 #50)
-#52 := [rewrite]: #51
-#55 := [quant-intro #52]: #54
-#49 := [asserted]: #11
-#58 := [mp #49 #55]: #53
-#102 := [mp~ #58 #114]: #53
-#608 := [mp #102 #607]: #603
-#599 := (not #603)
-#600 := (or #599 #71)
-#595 := [quant-inst #21]: #600
-[unit-resolution #595 #608 #597]: false
+#53 := (iff #11 #52)
+#50 := (iff #10 #49)
+#51 := [rewrite]: #50
+#54 := [quant-intro #51]: #53
+#48 := [asserted]: #11
+#57 := [mp #48 #54]: #52
+#91 := [mp~ #57 #103]: #52
+#597 := [mp #91 #596]: #592
+#588 := (not #592)
+#589 := (or #588 #70)
+#584 := [quant-inst #21]: #589
+[unit-resolution #584 #597 #586]: false
unsat
81c1cc5fc7edfc96b965f4e15b374acf04ca9046 458 0
#2 := false
@@ -14296,7 +13934,7 @@
#105 := [asserted]: #29
[unit-resolution #105 #402]: false
unsat
-8f8fbc61d0925864fffd8945e68a0401b7416686 1 0
+526684221798fda6e81b23523c37671c2fd01b49 1 0
unsat
a7ba12fdd24a1cfe15f53475941aaf6855022b7f 76 0
#2 := false
@@ -14375,443 +14013,425 @@
#580 := [quant-inst #107]: #579
[unit-resolution #580 #971 #391]: false
unsat
-e4dd068db00f152c179631d20d9af452dbe0f45d 439 0
+24f7b95c280da62e693df186e53d1c34ad016474 421 0
#2 := false
decl f19 :: (-> S8 S3)
decl f22 :: (-> S1 S8)
decl f1 :: S1
#4 := f1
-#273 := (f22 f1)
-#276 := (f19 #273)
+#101 := (f22 f1)
+#102 := (f19 #101)
decl f17 :: (-> S7 S3)
decl f21 :: (-> Int S7)
#98 := 3::Int
#99 := (f21 3::Int)
#100 := (f17 #99)
-#279 := (= #100 #276)
+#103 := (= #100 #102)
decl f16 :: (-> S4 S3)
decl f8 :: (-> S1 S4 S4)
decl f10 :: S4
#35 := f10
-#900 := (f8 f1 f10)
-#902 := (f16 #900)
-#656 := (= #902 #276)
-#569 := (= #276 #902)
+#884 := (f8 f1 f10)
+#886 := (f16 #884)
+#640 := (= #886 #102)
+#553 := (= #102 #886)
#91 := (:var 0 S1)
#94 := (f8 #91 f10)
-#975 := (pattern #94)
+#959 := (pattern #94)
#92 := (f22 #91)
-#974 := (pattern #92)
+#958 := (pattern #92)
#95 := (f16 #94)
#93 := (f19 #92)
#96 := (= #93 #95)
-#976 := (forall (vars (?v0 S1)) (:pat #974 #975) #96)
+#960 := (forall (vars (?v0 S1)) (:pat #958 #959) #96)
#97 := (forall (vars (?v0 S1)) #96)
-#979 := (iff #97 #976)
-#977 := (iff #96 #96)
-#978 := [refl]: #977
-#980 := [quant-intro #978]: #979
-#402 := (~ #97 #97)
-#401 := (~ #96 #96)
-#398 := [refl]: #401
-#403 := [nnf-pos #398]: #402
-#268 := [asserted]: #97
-#399 := [mp~ #268 #403]: #97
-#981 := [mp #399 #980]: #976
-#904 := (not #976)
-#905 := (or #904 #569)
-#906 := [quant-inst #4]: #905
-#674 := [unit-resolution #906 #981]: #569
-#660 := [symm #674]: #656
-#645 := (= #100 #902)
+#963 := (iff #97 #960)
+#961 := (iff #96 #96)
+#962 := [refl]: #961
+#964 := [quant-intro #962]: #963
+#386 := (~ #97 #97)
+#385 := (~ #96 #96)
+#382 := [refl]: #385
+#387 := [nnf-pos #382]: #386
+#267 := [asserted]: #97
+#383 := [mp~ #267 #387]: #97
+#965 := [mp #383 #964]: #960
+#888 := (not #960)
+#889 := (or #888 #553)
+#890 := [quant-inst #4]: #889
+#658 := [unit-resolution #890 #965]: #553
+#644 := [symm #658]: #640
+#629 := (= #100 #886)
decl f7 :: (-> S4 S3)
-#865 := (f7 #900)
-#860 := (= #865 #902)
+#849 := (f7 #884)
+#844 := (= #849 #886)
#22 := (:var 0 S4)
#71 := (f16 #22)
-#959 := (pattern #71)
+#943 := (pattern #71)
#25 := (f7 #22)
-#958 := (pattern #25)
-#248 := (= #25 #71)
-#960 := (forall (vars (?v0 S4)) (:pat #958 #959) #248)
-#252 := (forall (vars (?v0 S4)) #248)
-#963 := (iff #252 #960)
-#961 := (iff #248 #248)
-#962 := [refl]: #961
-#964 := [quant-intro #962]: #963
-#390 := (~ #252 #252)
-#431 := (~ #248 #248)
-#432 := [refl]: #431
-#391 := [nnf-pos #432]: #390
+#942 := (pattern #25)
+#247 := (= #25 #71)
+#944 := (forall (vars (?v0 S4)) (:pat #942 #943) #247)
+#251 := (forall (vars (?v0 S4)) #247)
+#947 := (iff #251 #944)
+#945 := (iff #247 #247)
+#946 := [refl]: #945
+#948 := [quant-intro #946]: #947
+#374 := (~ #251 #251)
+#415 := (~ #247 #247)
+#416 := [refl]: #415
+#375 := [nnf-pos #416]: #374
#72 := (= #71 #25)
#73 := (forall (vars (?v0 S4)) #72)
-#253 := (iff #73 #252)
-#250 := (iff #72 #248)
-#251 := [rewrite]: #250
-#254 := [quant-intro #251]: #253
-#247 := [asserted]: #73
-#257 := [mp #247 #254]: #252
-#433 := [mp~ #257 #391]: #252
-#965 := [mp #433 #964]: #960
-#584 := (not #960)
-#709 := (or #584 #860)
-#710 := [quant-inst #900]: #709
-#671 := [unit-resolution #710 #965]: #860
-#646 := (= #100 #865)
+#252 := (iff #73 #251)
+#249 := (iff #72 #247)
+#250 := [rewrite]: #249
+#253 := [quant-intro #250]: #252
+#246 := [asserted]: #73
+#256 := [mp #246 #253]: #251
+#417 := [mp~ #256 #375]: #251
+#949 := [mp #417 #948]: #944
+#568 := (not #944)
+#693 := (or #568 #844)
+#694 := [quant-inst #884]: #693
+#655 := [unit-resolution #694 #949]: #844
+#630 := (= #100 #849)
decl f5 :: (-> Int S3)
decl f6 :: (-> S3 Int)
#36 := (f7 f10)
-#862 := (f6 #36)
+#846 := (f6 #36)
#15 := 1::Int
-#868 := (+ 1::Int #862)
-#711 := (f5 #868)
-#854 := (= #711 #865)
+#852 := (+ 1::Int #846)
+#695 := (f5 #852)
+#838 := (= #695 #849)
#21 := (:var 1 S1)
#23 := (f8 #21 #22)
-#915 := (pattern #23)
+#899 := (pattern #23)
#26 := (f6 #25)
-#165 := (+ 1::Int #26)
-#170 := (f5 #165)
+#164 := (+ 1::Int #26)
+#169 := (f5 #164)
#24 := (f7 #23)
-#173 := (= #24 #170)
-#916 := (forall (vars (?v0 S1) (?v1 S4)) (:pat #915) #173)
-#176 := (forall (vars (?v0 S1) (?v1 S4)) #173)
-#919 := (iff #176 #916)
-#917 := (iff #173 #173)
-#918 := [refl]: #917
-#920 := [quant-intro #918]: #919
-#374 := (~ #176 #176)
-#373 := (~ #173 #173)
-#418 := [refl]: #373
-#375 := [nnf-pos #418]: #374
+#172 := (= #24 #169)
+#900 := (forall (vars (?v0 S1) (?v1 S4)) (:pat #899) #172)
+#175 := (forall (vars (?v0 S1) (?v1 S4)) #172)
+#903 := (iff #175 #900)
+#901 := (iff #172 #172)
+#902 := [refl]: #901
+#904 := [quant-intro #902]: #903
+#358 := (~ #175 #175)
+#357 := (~ #172 #172)
+#402 := [refl]: #357
+#359 := [nnf-pos #402]: #358
#14 := 0::Int
#16 := (+ 0::Int 1::Int)
#27 := (+ #26 #16)
#28 := (f5 #27)
#29 := (= #24 #28)
#30 := (forall (vars (?v0 S1) (?v1 S4)) #29)
-#177 := (iff #30 #176)
-#174 := (iff #29 #173)
-#171 := (= #28 #170)
-#168 := (= #27 #165)
-#161 := (+ #26 1::Int)
-#166 := (= #161 #165)
-#167 := [rewrite]: #166
-#163 := (= #27 #161)
-#141 := (= #16 1::Int)
-#142 := [rewrite]: #141
-#164 := [monotonicity #142]: #163
-#169 := [trans #164 #167]: #168
-#172 := [monotonicity #169]: #171
-#175 := [monotonicity #172]: #174
-#178 := [quant-intro #175]: #177
-#160 := [asserted]: #30
-#181 := [mp #160 #178]: #176
-#419 := [mp~ #181 #375]: #176
-#921 := [mp #419 #920]: #916
-#850 := (not #916)
-#851 := (or #850 #854)
-#853 := (= #865 #711)
-#857 := (or #850 #853)
-#852 := (iff #857 #851)
-#688 := (iff #851 #851)
-#690 := [rewrite]: #688
-#855 := (iff #853 #854)
-#856 := [rewrite]: #855
-#859 := [monotonicity #856]: #852
-#691 := [trans #859 #690]: #852
-#858 := [quant-inst #4 #35]: #857
-#844 := [mp #858 #691]: #851
-#673 := [unit-resolution #844 #921]: #854
-#658 := (= #100 #711)
+#176 := (iff #30 #175)
+#173 := (iff #29 #172)
+#170 := (= #28 #169)
+#167 := (= #27 #164)
+#160 := (+ #26 1::Int)
+#165 := (= #160 #164)
+#166 := [rewrite]: #165
+#162 := (= #27 #160)
+#140 := (= #16 1::Int)
+#141 := [rewrite]: #140
+#163 := [monotonicity #141]: #162
+#168 := [trans #163 #166]: #167
+#171 := [monotonicity #168]: #170
+#174 := [monotonicity #171]: #173
+#177 := [quant-intro #174]: #176
+#159 := [asserted]: #30
+#180 := [mp #159 #177]: #175
+#403 := [mp~ #180 #359]: #175
+#905 := [mp #403 #904]: #900
+#834 := (not #900)
+#835 := (or #834 #838)
+#837 := (= #849 #695)
+#841 := (or #834 #837)
+#836 := (iff #841 #835)
+#672 := (iff #835 #835)
+#674 := [rewrite]: #672
+#839 := (iff #837 #838)
+#840 := [rewrite]: #839
+#843 := [monotonicity #840]: #836
+#675 := [trans #843 #674]: #836
+#842 := [quant-inst #4 #35]: #841
+#828 := [mp #842 #675]: #835
+#657 := [unit-resolution #828 #905]: #838
+#642 := (= #100 #695)
decl f3 :: (-> S2 S3)
decl f9 :: S2
#31 := f9
#32 := (f3 f9)
-#870 := (f6 #32)
-#874 := (+ 1::Int #870)
-#863 := (f5 #874)
-#652 := (= #863 #711)
-#664 := (= #711 #863)
-#670 := (= #868 #874)
-#663 := (= 1::Int #874)
-#703 := (= #874 1::Int)
-#847 := (<= #870 0::Int)
-#845 := (= #870 0::Int)
+#854 := (f6 #32)
+#858 := (+ 1::Int #854)
+#847 := (f5 #858)
+#636 := (= #847 #695)
+#648 := (= #695 #847)
+#654 := (= #852 #858)
+#647 := (= 1::Int #858)
+#687 := (= #858 1::Int)
+#831 := (<= #854 0::Int)
+#829 := (= #854 0::Int)
#33 := (f5 0::Int)
-#901 := (f6 #33)
-#898 := (= #901 0::Int)
+#885 := (f6 #33)
+#882 := (= #885 0::Int)
#84 := (:var 0 Int)
-#112 := (f5 #84)
-#990 := (pattern #112)
-#312 := (>= #84 0::Int)
-#313 := (not #312)
-#113 := (f6 #112)
-#294 := (= #84 #113)
-#319 := (or #294 #313)
-#991 := (forall (vars (?v0 Int)) (:pat #990) #319)
-#324 := (forall (vars (?v0 Int)) #319)
-#994 := (iff #324 #991)
-#992 := (iff #319 #319)
-#993 := [refl]: #992
-#995 := [quant-intro #993]: #994
-#408 := (~ #324 #324)
-#407 := (~ #319 #319)
-#394 := [refl]: #407
-#409 := [nnf-pos #394]: #408
-#114 := (= #113 #84)
-#111 := (<= 0::Int #84)
-#115 := (implies #111 #114)
-#116 := (forall (vars (?v0 Int)) #115)
-#327 := (iff #116 #324)
-#301 := (not #111)
-#302 := (or #301 #294)
-#307 := (forall (vars (?v0 Int)) #302)
-#325 := (iff #307 #324)
-#322 := (iff #302 #319)
-#316 := (or #313 #294)
-#320 := (iff #316 #319)
-#321 := [rewrite]: #320
-#317 := (iff #302 #316)
-#314 := (iff #301 #313)
-#310 := (iff #111 #312)
-#311 := [rewrite]: #310
-#315 := [monotonicity #311]: #314
-#318 := [monotonicity #315]: #317
-#323 := [trans #318 #321]: #322
-#326 := [quant-intro #323]: #325
-#308 := (iff #116 #307)
-#305 := (iff #115 #302)
-#298 := (implies #111 #294)
-#303 := (iff #298 #302)
-#304 := [rewrite]: #303
-#299 := (iff #115 #298)
-#296 := (iff #114 #294)
-#297 := [rewrite]: #296
-#300 := [monotonicity #297]: #299
-#306 := [trans #300 #304]: #305
-#309 := [quant-intro #306]: #308
-#328 := [trans #309 #326]: #327
-#293 := [asserted]: #116
-#329 := [mp #293 #328]: #324
-#395 := [mp~ #329 #409]: #324
-#996 := [mp #395 #995]: #991
-#891 := (not #991)
-#893 := (or #891 #898)
-#570 := (>= 0::Int 0::Int)
-#903 := (not #570)
-#907 := (= 0::Int #901)
-#897 := (or #907 #903)
-#532 := (or #891 #897)
-#894 := (iff #532 #893)
-#895 := (iff #893 #893)
-#881 := [rewrite]: #895
-#890 := (iff #897 #898)
-#886 := (or #898 false)
-#889 := (iff #886 #898)
-#884 := [rewrite]: #889
-#887 := (iff #897 #886)
-#548 := (iff #903 false)
+#111 := (f5 #84)
+#974 := (pattern #111)
+#296 := (>= #84 0::Int)
+#297 := (not #296)
+#112 := (f6 #111)
+#278 := (= #84 #112)
+#303 := (or #278 #297)
+#975 := (forall (vars (?v0 Int)) (:pat #974) #303)
+#308 := (forall (vars (?v0 Int)) #303)
+#978 := (iff #308 #975)
+#976 := (iff #303 #303)
+#977 := [refl]: #976
+#979 := [quant-intro #977]: #978
+#392 := (~ #308 #308)
+#391 := (~ #303 #303)
+#378 := [refl]: #391
+#393 := [nnf-pos #378]: #392
+#113 := (= #112 #84)
+#110 := (<= 0::Int #84)
+#114 := (implies #110 #113)
+#115 := (forall (vars (?v0 Int)) #114)
+#311 := (iff #115 #308)
+#285 := (not #110)
+#286 := (or #285 #278)
+#291 := (forall (vars (?v0 Int)) #286)
+#309 := (iff #291 #308)
+#306 := (iff #286 #303)
+#300 := (or #297 #278)
+#304 := (iff #300 #303)
+#305 := [rewrite]: #304
+#301 := (iff #286 #300)
+#298 := (iff #285 #297)
+#294 := (iff #110 #296)
+#295 := [rewrite]: #294
+#299 := [monotonicity #295]: #298
+#302 := [monotonicity #299]: #301
+#307 := [trans #302 #305]: #306
+#310 := [quant-intro #307]: #309
+#292 := (iff #115 #291)
+#289 := (iff #114 #286)
+#282 := (implies #110 #278)
+#287 := (iff #282 #286)
+#288 := [rewrite]: #287
+#283 := (iff #114 #282)
+#280 := (iff #113 #278)
+#281 := [rewrite]: #280
+#284 := [monotonicity #281]: #283
+#290 := [trans #284 #288]: #289
+#293 := [quant-intro #290]: #292
+#312 := [trans #293 #310]: #311
+#277 := [asserted]: #115
+#313 := [mp #277 #312]: #308
+#379 := [mp~ #313 #393]: #308
+#980 := [mp #379 #979]: #975
+#875 := (not #975)
+#877 := (or #875 #882)
+#554 := (>= 0::Int 0::Int)
+#887 := (not #554)
+#891 := (= 0::Int #885)
+#881 := (or #891 #887)
+#516 := (or #875 #881)
+#878 := (iff #516 #877)
+#879 := (iff #877 #877)
+#865 := [rewrite]: #879
+#874 := (iff #881 #882)
+#870 := (or #882 false)
+#873 := (iff #870 #882)
+#868 := [rewrite]: #873
+#871 := (iff #881 #870)
+#532 := (iff #887 false)
#1 := true
-#541 := (not true)
-#546 := (iff #541 false)
-#547 := [rewrite]: #546
-#883 := (iff #903 #541)
-#557 := (iff #570 true)
-#899 := [rewrite]: #557
-#545 := [monotonicity #899]: #883
-#885 := [trans #545 #547]: #548
-#556 := (iff #907 #898)
-#561 := [rewrite]: #556
-#888 := [monotonicity #561 #885]: #887
-#527 := [trans #888 #884]: #890
-#892 := [monotonicity #527]: #894
-#882 := [trans #892 #881]: #894
-#533 := [quant-inst #14]: #532
-#589 := [mp #533 #882]: #893
-#723 := [unit-resolution #589 #996]: #898
-#685 := (= #870 #901)
+#525 := (not true)
+#530 := (iff #525 false)
+#531 := [rewrite]: #530
+#867 := (iff #887 #525)
+#541 := (iff #554 true)
+#883 := [rewrite]: #541
+#529 := [monotonicity #883]: #867
+#869 := [trans #529 #531]: #532
+#540 := (iff #891 #882)
+#545 := [rewrite]: #540
+#872 := [monotonicity #545 #869]: #871
+#511 := [trans #872 #868]: #874
+#876 := [monotonicity #511]: #878
+#866 := [trans #876 #865]: #878
+#517 := [quant-inst #14]: #516
+#573 := [mp #517 #866]: #877
+#707 := [unit-resolution #573 #980]: #882
+#669 := (= #854 #885)
#34 := (= #32 #33)
-#179 := [asserted]: #34
-#686 := [monotonicity #179]: #685
-#693 := [trans #686 #723]: #845
-#695 := (not #845)
-#696 := (or #695 #847)
-#697 := [th-lemma arith triangle-eq]: #696
-#699 := [unit-resolution #697 #693]: #847
-#848 := (>= #870 0::Int)
-#700 := (or #695 #848)
-#701 := [th-lemma arith triangle-eq]: #700
-#702 := [unit-resolution #701 #693]: #848
-#704 := [th-lemma arith eq-propagate -1 -1 #702 #699]: #703
-#666 := [symm #704]: #663
-#679 := (= #868 1::Int)
-#849 := (<= #862 0::Int)
-#846 := (= #862 0::Int)
-#705 := (= #862 #901)
+#178 := [asserted]: #34
+#670 := [monotonicity #178]: #669
+#677 := [trans #670 #707]: #829
+#679 := (not #829)
+#680 := (or #679 #831)
+#681 := [th-lemma arith triangle-eq]: #680
+#683 := [unit-resolution #681 #677]: #831
+#832 := (>= #854 0::Int)
+#684 := (or #679 #832)
+#685 := [th-lemma arith triangle-eq]: #684
+#686 := [unit-resolution #685 #677]: #832
+#688 := [th-lemma arith eq-propagate -1 -1 #686 #683]: #687
+#650 := [symm #688]: #647
+#663 := (= #852 1::Int)
+#833 := (<= #846 0::Int)
+#830 := (= #846 0::Int)
+#689 := (= #846 #885)
#37 := (= #36 #33)
-#182 := (= #33 #36)
-#183 := (iff #37 #182)
-#184 := [rewrite]: #183
-#180 := [asserted]: #37
-#187 := [mp #180 #184]: #182
-#687 := [symm #187]: #37
-#675 := [monotonicity #687]: #705
-#676 := [trans #675 #723]: #846
-#677 := (not #846)
-#678 := (or #677 #849)
-#680 := [th-lemma arith triangle-eq]: #678
-#681 := [unit-resolution #680 #676]: #849
-#731 := (>= #862 0::Int)
-#682 := (or #677 #731)
-#524 := [th-lemma arith triangle-eq]: #682
-#683 := [unit-resolution #524 #676]: #731
-#684 := [th-lemma arith eq-propagate -1 -1 #683 #681]: #679
-#672 := [trans #684 #666]: #670
-#669 := [monotonicity #672]: #664
-#655 := [symm #669]: #652
-#654 := (= #100 #863)
+#181 := (= #33 #36)
+#182 := (iff #37 #181)
+#183 := [rewrite]: #182
+#179 := [asserted]: #37
+#186 := [mp #179 #183]: #181
+#671 := [symm #186]: #37
+#659 := [monotonicity #671]: #689
+#660 := [trans #659 #707]: #830
+#661 := (not #830)
+#662 := (or #661 #833)
+#664 := [th-lemma arith triangle-eq]: #662
+#665 := [unit-resolution #664 #660]: #833
+#715 := (>= #846 0::Int)
+#666 := (or #661 #715)
+#508 := [th-lemma arith triangle-eq]: #666
+#667 := [unit-resolution #508 #660]: #715
+#668 := [th-lemma arith eq-propagate -1 -1 #667 #665]: #663
+#656 := [trans #668 #650]: #654
+#653 := [monotonicity #656]: #648
+#639 := [symm #653]: #636
+#638 := (= #100 #847)
decl f4 :: (-> Int S2 S2)
-#579 := (f4 3::Int f9)
-#601 := (f3 #579)
-#864 := (= #601 #863)
+#563 := (f4 3::Int f9)
+#585 := (f3 #563)
+#848 := (= #585 #847)
#9 := (:var 0 S2)
#8 := (:var 1 Int)
#10 := (f4 #8 #9)
-#908 := (pattern #10)
+#892 := (pattern #10)
#12 := (f3 #9)
#13 := (f6 #12)
-#146 := (+ 1::Int #13)
-#151 := (f5 #146)
+#145 := (+ 1::Int #13)
+#150 := (f5 #145)
#11 := (f3 #10)
-#154 := (= #11 #151)
-#909 := (forall (vars (?v0 Int) (?v1 S2)) (:pat #908) #154)
-#157 := (forall (vars (?v0 Int) (?v1 S2)) #154)
-#912 := (iff #157 #909)
-#910 := (iff #154 #154)
-#911 := [refl]: #910
-#913 := [quant-intro #911]: #912
-#416 := (~ #157 #157)
-#414 := (~ #154 #154)
-#415 := [refl]: #414
-#417 := [nnf-pos #415]: #416
+#153 := (= #11 #150)
+#893 := (forall (vars (?v0 Int) (?v1 S2)) (:pat #892) #153)
+#156 := (forall (vars (?v0 Int) (?v1 S2)) #153)
+#896 := (iff #156 #893)
+#894 := (iff #153 #153)
+#895 := [refl]: #894
+#897 := [quant-intro #895]: #896
+#400 := (~ #156 #156)
+#398 := (~ #153 #153)
+#399 := [refl]: #398
+#401 := [nnf-pos #399]: #400
#17 := (+ #13 #16)
#18 := (f5 #17)
#19 := (= #11 #18)
#20 := (forall (vars (?v0 Int) (?v1 S2)) #19)
-#158 := (iff #20 #157)
-#155 := (iff #19 #154)
-#152 := (= #18 #151)
-#149 := (= #17 #146)
-#143 := (+ #13 1::Int)
-#147 := (= #143 #146)
-#148 := [rewrite]: #147
-#144 := (= #17 #143)
-#145 := [monotonicity #142]: #144
-#150 := [trans #145 #148]: #149
-#153 := [monotonicity #150]: #152
-#156 := [monotonicity #153]: #155
-#159 := [quant-intro #156]: #158
-#140 := [asserted]: #20
-#162 := [mp #140 #159]: #157
-#372 := [mp~ #162 #417]: #157
-#914 := [mp #372 #913]: #909
-#861 := (not #909)
-#866 := (or #861 #864)
-#867 := [quant-inst #98 #31]: #866
-#722 := [unit-resolution #867 #914]: #864
-#653 := (= #100 #601)
+#157 := (iff #20 #156)
+#154 := (iff #19 #153)
+#151 := (= #18 #150)
+#148 := (= #17 #145)
+#142 := (+ #13 1::Int)
+#146 := (= #142 #145)
+#147 := [rewrite]: #146
+#143 := (= #17 #142)
+#144 := [monotonicity #141]: #143
+#149 := [trans #144 #147]: #148
+#152 := [monotonicity #149]: #151
+#155 := [monotonicity #152]: #154
+#158 := [quant-intro #155]: #157
+#139 := [asserted]: #20
+#161 := [mp #139 #158]: #156
+#356 := [mp~ #161 #401]: #156
+#898 := [mp #356 #897]: #893
+#845 := (not #893)
+#850 := (or #845 #848)
+#851 := [quant-inst #98 #31]: #850
+#706 := [unit-resolution #851 #898]: #848
+#637 := (= #100 #585)
decl f15 :: (-> S2 S3)
-#583 := (f15 #579)
-#879 := (= #583 #601)
+#567 := (f15 #563)
+#863 := (= #567 #585)
#68 := (f15 #9)
-#951 := (pattern #68)
-#950 := (pattern #12)
-#240 := (= #12 #68)
-#952 := (forall (vars (?v0 S2)) (:pat #950 #951) #240)
-#244 := (forall (vars (?v0 S2)) #240)
-#955 := (iff #244 #952)
-#953 := (iff #240 #240)
-#954 := [refl]: #953
-#956 := [quant-intro #954]: #955
-#388 := (~ #244 #244)
-#428 := (~ #240 #240)
-#429 := [refl]: #428
-#389 := [nnf-pos #429]: #388
+#935 := (pattern #68)
+#934 := (pattern #12)
+#239 := (= #12 #68)
+#936 := (forall (vars (?v0 S2)) (:pat #934 #935) #239)
+#243 := (forall (vars (?v0 S2)) #239)
+#939 := (iff #243 #936)
+#937 := (iff #239 #239)
+#938 := [refl]: #937
+#940 := [quant-intro #938]: #939
+#372 := (~ #243 #243)
+#412 := (~ #239 #239)
+#413 := [refl]: #412
+#373 := [nnf-pos #413]: #372
#69 := (= #68 #12)
#70 := (forall (vars (?v0 S2)) #69)
-#245 := (iff #70 #244)
-#242 := (iff #69 #240)
-#243 := [rewrite]: #242
-#246 := [quant-intro #243]: #245
-#239 := [asserted]: #70
-#249 := [mp #239 #246]: #244
-#430 := [mp~ #249 #389]: #244
-#957 := [mp #430 #956]: #952
-#580 := (not #952)
-#590 := (or #580 #879)
-#875 := (= #601 #583)
-#591 := (or #580 #875)
-#593 := (iff #591 #590)
-#872 := (iff #590 #590)
-#586 := [rewrite]: #872
-#876 := (iff #875 #879)
-#880 := [rewrite]: #876
-#871 := [monotonicity #880]: #593
-#869 := [trans #871 #586]: #593
-#592 := [quant-inst #579]: #591
-#873 := [mp #592 #869]: #590
-#721 := [unit-resolution #873 #957]: #879
-#564 := (= #100 #583)
+#244 := (iff #70 #243)
+#241 := (iff #69 #239)
+#242 := [rewrite]: #241
+#245 := [quant-intro #242]: #244
+#238 := [asserted]: #70
+#248 := [mp #238 #245]: #243
+#414 := [mp~ #248 #373]: #243
+#941 := [mp #414 #940]: #936
+#564 := (not #936)
+#574 := (or #564 #863)
+#859 := (= #585 #567)
+#575 := (or #564 #859)
+#577 := (iff #575 #574)
+#856 := (iff #574 #574)
+#570 := [rewrite]: #856
+#860 := (iff #859 #863)
+#864 := [rewrite]: #860
+#855 := [monotonicity #864]: #577
+#853 := [trans #855 #570]: #577
+#576 := [quant-inst #563]: #575
+#857 := [mp #576 #853]: #574
+#705 := [unit-resolution #857 #941]: #863
+#548 := (= #100 #567)
#87 := (f4 #84 f9)
-#967 := (pattern #87)
+#951 := (pattern #87)
#85 := (f21 #84)
-#966 := (pattern #85)
+#950 := (pattern #85)
#88 := (f15 #87)
#86 := (f17 #85)
#89 := (= #86 #88)
-#968 := (forall (vars (?v0 Int)) (:pat #966 #967) #89)
+#952 := (forall (vars (?v0 Int)) (:pat #950 #951) #89)
#90 := (forall (vars (?v0 Int)) #89)
-#971 := (iff #90 #968)
-#969 := (iff #89 #89)
-#970 := [refl]: #969
-#972 := [quant-intro #970]: #971
-#392 := (~ #90 #90)
-#434 := (~ #89 #89)
-#435 := [refl]: #434
-#393 := [nnf-pos #435]: #392
-#267 := [asserted]: #90
-#400 := [mp~ #267 #393]: #90
-#973 := [mp #400 #972]: #968
-#558 := (not #968)
-#689 := (or #558 #564)
-#896 := [quant-inst #98]: #689
-#662 := [unit-resolution #896 #973]: #564
-#661 := [trans #662 #721]: #653
-#657 := [trans #661 #722]: #654
-#644 := [trans #657 #655]: #658
-#647 := [trans #644 #673]: #646
-#648 := [trans #647 #671]: #645
-#630 := [trans #648 #660]: #279
-#282 := (not #279)
-decl f2 :: S1
-#5 := f2
-#101 := (ite true f1 f2)
-#102 := (f22 #101)
-#103 := (f19 #102)
-#104 := (= #100 #103)
-#105 := (not #104)
-#283 := (iff #105 #282)
-#280 := (iff #104 #279)
-#277 := (= #103 #276)
-#274 := (= #102 #273)
-#271 := (= #101 f1)
-#272 := [rewrite]: #271
-#275 := [monotonicity #272]: #274
-#278 := [monotonicity #275]: #277
-#281 := [monotonicity #278]: #280
-#284 := [monotonicity #281]: #283
-#270 := [asserted]: #105
-#287 := [mp #270 #284]: #282
-[unit-resolution #287 #630]: false
-unsat
+#955 := (iff #90 #952)
+#953 := (iff #89 #89)
+#954 := [refl]: #953
+#956 := [quant-intro #954]: #955
+#376 := (~ #90 #90)
+#418 := (~ #89 #89)
+#419 := [refl]: #418
+#377 := [nnf-pos #419]: #376
+#266 := [asserted]: #90
+#384 := [mp~ #266 #377]: #90
+#957 := [mp #384 #956]: #952
+#542 := (not #952)
+#673 := (or #542 #548)
+#880 := [quant-inst #98]: #673
+#646 := [unit-resolution #880 #957]: #548
+#645 := [trans #646 #705]: #637
+#641 := [trans #645 #706]: #638
+#628 := [trans #641 #639]: #642
+#631 := [trans #628 #657]: #630
+#632 := [trans #631 #655]: #629
+#614 := [trans #632 #644]: #103
+#104 := (not #103)
+#269 := [asserted]: #104
+[unit-resolution #269 #614]: false
+unsat