src/HOL/SMT_Examples/SMT_Examples.certs

--- a/src/HOL/SMT_Examples/SMT_Examples.certs	Mon Dec 20 09:06:37 2010 +0100
+++ b/src/HOL/SMT_Examples/SMT_Examples.certs	Mon Dec 20 09:31:47 2010 +0100
@@ -7423,425 +7423,698 @@
 #37 := [asserted]: #17
 [mp #37 #73]: false
 unsat
-f9ae47f5aef750f37ea2d9309845d7cf08946d8c 211 0
-#2 := false
-#12 := 0::Int
+75da1862a2fd162477f9d85292ff8ab2e18559e4 342 0
+#2 := false
+#21 := 0::Int
 decl f3 :: Int
 #8 := f3
-#122 := (<= f3 0::Int)
-#135 := (>= f3 0::Int)
-#136 := (not #135)
-#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)
+#419 := (<= f3 0::Int)
+#446 := (>= f3 0::Int)
+#753 := (not #446)
+#409 := (not #419)
+#754 := (or #409 #753)
+#715 := (not #754)
 #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)
+#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
-#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)
+#13 := (* 2::Int #12)
+#14 := (+ #13 1::Int)
+#15 := (+ f3 #14)
 #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)
+#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)
+#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)
 #138 := [rewrite]: #137
-#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
-#10 := 0::Int
+#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
+#2 := false
+#20 := 0::Int
 decl f3 :: Int
 #8 := f3
-#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)
+#438 := (>= f3 0::Int)
+#758 := (<= f3 0::Int)
+#404 := (not #758)
+#747 := (not #438)
+#751 := (or #747 #404)
+#714 := (not #751)
 #9 := 2::Int
-#19 := (mod f3 2::Int)
-#139 := (ite #136 #19 #74)
-#182 := (= #19 #139)
-#279 := (not #182)
-#251 := (>= #19 2::Int)
-#252 := (not #251)
+#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)
 #1 := true
-#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)
+#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)
 #133 := [rewrite]: #132
-#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
+#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
 unsat
 cfa8a4e8b0964986b89eaf37e6038032e9b8b0d6 101 0
 #2 := false
@@ -7945,783 +8218,936 @@
 #123 := [th-lemma arith triangle-eq]: #122
 [unit-resolution #123 #119 #112 #46]: false
 unsat
-cf727a25fbaea6abf5a0d302bf954b4ffa92b324 777 0
-#2 := false
-#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
-#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
-#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
+742e212b0179422ed718ceb7818522f48622510c 930 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
-#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
+#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
+#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
+#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
 #439 := [monotonicity #436]: #438
-#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
+#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
 unsat
 c04d38458726eb1b2cafd52bd3881d6f8160666f 24 0
 #2 := false
@@ -10061,318 +10487,288 @@
 unsat
 ERROR: line 11 column 83: invalid pattern.
 
-8aba3814871680009d1d0267516334493c303e78 175 0
-#2 := false
-#8 := 0::Int
-decl f4 :: Int
-#18 := f4
-#138 := (<= f4 0::Int)
-#139 := (not #138)
+8f616b17d0807409dc26bfdf9593c5fcd06fb7e7 1 0
+unsat
+3eb9cf11ee8774c9212c37c265e7552f3b8f24a9 75 0
+#2 := false
+#10 := 1::Int
 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)
+#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
-#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)
+#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
-#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)
+#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
+#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
-#22 := f6
-#20 := 1::Int
-#80 := (+ 1::Int f6)
-decl f4 :: Int
-#18 := f4
-#83 := (f3 f4 #80)
+#13 := f6
+decl f7 :: Int
+#17 := f7
 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)
+#12 := f5
+#28 := (+ f5 f7)
+#29 := (+ #28 f6)
+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)
 #56 := (+ #54 #55)
-#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
+#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
 unsat
 13d222fc57300189e3c05b2df538ad53757b2feb 257 0
 #2 := false
@@ -13934,7 +14330,7 @@
 #105 := [asserted]: #29
 [unit-resolution #105 #402]: false
 unsat
-526684221798fda6e81b23523c37671c2fd01b49 1 0
+cbddab0a93fe2901d1f5dd30bb313d7532a1c531 1 0
 unsat
 a7ba12fdd24a1cfe15f53475941aaf6855022b7f 76 0
 #2 := false