src/HOL/Multivariate_Analysis/Integration.certs

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Multivariate_Analysis/Integration.certs	Wed May 12 23:54:06 2010 +0200
@@ -0,0 +1,4215 @@
+148c2437fb9e64ff4110383f54f5a9a720082439 428 0
+#2 := false
+decl f12 :: S2
+#42 := f12
+decl f5 :: S2
+#25 := f5
+#49 := (= f5 f12)
+decl f3 :: (-> int S2)
+decl f4 :: (-> S2 int)
+#43 := (f4 f12)
+#593 := (f3 #43)
+#691 := (= #593 f12)
+#594 := (= f12 #593)
+#8 := (:var 0 S2)
+#9 := (f4 #8)
+#546 := (pattern #9)
+#10 := (f3 #9)
+#98 := (= #8 #10)
+#547 := (forall (vars (?v0 S2)) (:pat #546) #98)
+#101 := (forall (vars (?v0 S2)) #98)
+#550 := (iff #101 #547)
+#548 := (iff #98 #98)
+#549 := [refl]: #548
+#551 := [quant-intro #549]: #550
+#461 := (~ #101 #101)
+#463 := (~ #98 #98)
+#464 := [refl]: #463
+#462 := [nnf-pos #464]: #461
+#11 := (= #10 #8)
+#12 := (forall (vars (?v0 S2)) #11)
+#102 := (iff #12 #101)
+#99 := (iff #11 #98)
+#100 := [rewrite]: #99
+#103 := [quant-intro #100]: #102
+#97 := [asserted]: #12
+#106 := [mp #97 #103]: #101
+#459 := [mp~ #106 #462]: #101
+#552 := [mp #459 #551]: #547
+#595 := (not #547)
+#600 := (or #595 #594)
+#601 := [quant-inst]: #600
+#685 := [unit-resolution #601 #552]: #594
+#692 := [symm #685]: #691
+#693 := (= f5 #593)
+#26 := (f4 f5)
+#591 := (f3 #26)
+#689 := (= #591 #593)
+#687 := (= #593 #591)
+#683 := (= #43 #26)
+#681 := (= #26 #43)
+#13 := 0::int
+#232 := -1::int
+#235 := (* -1::int #43)
+#236 := (+ #26 #235)
+#301 := (<= #236 0::int)
+#74 := (<= #26 #43)
+#398 := (iff #74 #301)
+#399 := [rewrite]: #398
+#352 := [asserted]: #74
+#400 := [mp #352 #399]: #301
+#234 := (>= #236 0::int)
+decl f6 :: (-> S3 S4 real)
+decl f8 :: (-> S2 S4)
+#29 := (f8 f5)
+decl f9 :: S3
+#31 := f9
+#32 := (f6 f9 #29)
+decl f11 :: S3
+#37 := f11
+#38 := (f6 f11 #29)
+#50 := (f8 f12)
+decl f7 :: S3
+#28 := f7
+#51 := (f6 f7 #50)
+#52 := (ite #49 #51 #38)
+#261 := (ite #234 #52 #32)
+#573 := (= #32 #261)
+#653 := (not #573)
+#199 := 0::real
+#197 := -1::real
+#270 := (* -1::real #261)
+#645 := (+ #32 #270)
+#647 := (>= #645 0::real)
+#650 := (not #647)
+#648 := [hypothesis]: #647
+decl f10 :: S3
+#34 := f10
+#35 := (f6 f10 #29)
+#271 := (+ #35 #270)
+#269 := (>= #271 0::real)
+#272 := (not #269)
+#30 := (f6 f7 #29)
+decl f13 :: S3
+#45 := f13
+#46 := (f6 f13 #29)
+#242 := (ite #234 #46 #30)
+#250 := (* -1::real #242)
+#251 := (+ #35 #250)
+#252 := (<= #251 0::real)
+#253 := (not #252)
+#277 := (and #253 #272)
+#44 := (< #26 #43)
+#53 := (ite #44 #32 #52)
+#54 := (< #35 #53)
+#47 := (ite #44 #30 #46)
+#48 := (< #47 #35)
+#55 := (and #48 #54)
+#278 := (iff #55 #277)
+#275 := (iff #54 #272)
+#266 := (< #35 #261)
+#273 := (iff #266 #272)
+#274 := [rewrite]: #273
+#267 := (iff #54 #266)
+#264 := (= #53 #261)
+#233 := (not #234)
+#258 := (ite #233 #32 #52)
+#262 := (= #258 #261)
+#263 := [rewrite]: #262
+#259 := (= #53 #258)
+#237 := (iff #44 #233)
+#238 := [rewrite]: #237
+#260 := [monotonicity #238]: #259
+#265 := [trans #260 #263]: #264
+#268 := [monotonicity #265]: #267
+#276 := [trans #268 #274]: #275
+#256 := (iff #48 #253)
+#247 := (< #242 #35)
+#254 := (iff #247 #253)
+#255 := [rewrite]: #254
+#248 := (iff #48 #247)
+#245 := (= #47 #242)
+#239 := (ite #233 #30 #46)
+#243 := (= #239 #242)
+#244 := [rewrite]: #243
+#240 := (= #47 #239)
+#241 := [monotonicity #238]: #240
+#246 := [trans #241 #244]: #245
+#249 := [monotonicity #246]: #248
+#257 := [trans #249 #255]: #256
+#279 := [monotonicity #257 #276]: #278
+#183 := [asserted]: #55
+#280 := [mp #183 #279]: #277
+#282 := [and-elim #280]: #272
+#201 := (* -1::real #35)
+#202 := (+ #32 #201)
+#200 := (>= #202 0::real)
+#198 := (not #200)
+#218 := (* -1::real #38)
+#219 := (+ #35 #218)
+#217 := (>= #219 0::real)
+#220 := (not #217)
+#225 := (and #198 #220)
+#27 := (< #26 #26)
+#39 := (ite #27 #32 #38)
+#40 := (< #35 #39)
+#33 := (ite #27 #30 #32)
+#36 := (< #33 #35)
+#41 := (and #36 #40)
+#226 := (iff #41 #225)
+#223 := (iff #40 #220)
+#214 := (< #35 #38)
+#221 := (iff #214 #220)
+#222 := [rewrite]: #221
+#215 := (iff #40 #214)
+#212 := (= #39 #38)
+#207 := (ite false #32 #38)
+#210 := (= #207 #38)
+#211 := [rewrite]: #210
+#208 := (= #39 #207)
+#185 := (iff #27 false)
+#186 := [rewrite]: #185
+#209 := [monotonicity #186]: #208
+#213 := [trans #209 #211]: #212
+#216 := [monotonicity #213]: #215
+#224 := [trans #216 #222]: #223
+#205 := (iff #36 #198)
+#194 := (< #32 #35)
+#203 := (iff #194 #198)
+#204 := [rewrite]: #203
+#195 := (iff #36 #194)
+#192 := (= #33 #32)
+#187 := (ite false #30 #32)
+#190 := (= #187 #32)
+#191 := [rewrite]: #190
+#188 := (= #33 #187)
+#189 := [monotonicity #186]: #188
+#193 := [trans #189 #191]: #192
+#196 := [monotonicity #193]: #195
+#206 := [trans #196 #204]: #205
+#227 := [monotonicity #206 #224]: #226
+#182 := [asserted]: #41
+#228 := [mp #182 #227]: #225
+#229 := [and-elim #228]: #198
+#649 := [th-lemma #229 #282 #648]: false
+#651 := [lemma #649]: #650
+#652 := [hypothesis]: #573
+#654 := (or #653 #647)
+#655 := [th-lemma]: #654
+#656 := [unit-resolution #655 #652 #651]: false
+#657 := [lemma #656]: #653
+#583 := (or #234 #573)
+#584 := [def-axiom]: #583
+#680 := [unit-resolution #584 #657]: #234
+#682 := [th-lemma #680 #400]: #681
+#684 := [symm #682]: #683
+#688 := [monotonicity #684]: #687
+#690 := [symm #688]: #689
+#592 := (= f5 #591)
+#596 := (or #595 #592)
+#597 := [quant-inst]: #596
+#686 := [unit-resolution #597 #552]: #592
+#694 := [trans #686 #690]: #693
+#695 := [trans #694 #692]: #49
+#576 := (not #49)
+#58 := (f6 f13 #50)
+#284 := (ite #49 #32 #58)
+#472 := (* -1::real #284)
+#637 := (+ #32 #472)
+#638 := (<= #637 0::real)
+#585 := (= #32 #284)
+#661 := [hypothesis]: #49
+#587 := (or #576 #585)
+#588 := [def-axiom]: #587
+#662 := [unit-resolution #588 #661]: #585
+#663 := (not #585)
+#664 := (or #663 #638)
+#665 := [th-lemma]: #664
+#666 := [unit-resolution #665 #662]: #638
+#61 := (f6 f10 #50)
+#368 := (* -1::real #61)
+#384 := (+ #51 #368)
+#385 := (<= #384 0::real)
+#386 := (not #385)
+#369 := (+ #58 #368)
+#367 := (>= #369 0::real)
+#366 := (not #367)
+#391 := (and #366 #386)
+#63 := (f6 f9 #50)
+#68 := (< #43 #43)
+#71 := (ite #68 #63 #51)
+#72 := (< #61 #71)
+#69 := (ite #68 #51 #58)
+#70 := (< #69 #61)
+#73 := (and #70 #72)
+#392 := (iff #73 #391)
+#389 := (iff #72 #386)
+#381 := (< #61 #51)
+#387 := (iff #381 #386)
+#388 := [rewrite]: #387
+#382 := (iff #72 #381)
+#379 := (= #71 #51)
+#374 := (ite false #63 #51)
+#377 := (= #374 #51)
+#378 := [rewrite]: #377
+#375 := (= #71 #374)
+#354 := (iff #68 false)
+#355 := [rewrite]: #354
+#376 := [monotonicity #355]: #375
+#380 := [trans #376 #378]: #379
+#383 := [monotonicity #380]: #382
+#390 := [trans #383 #388]: #389
+#372 := (iff #70 #366)
+#363 := (< #58 #61)
+#370 := (iff #363 #366)
+#371 := [rewrite]: #370
+#364 := (iff #70 #363)
+#361 := (= #69 #58)
+#356 := (ite false #51 #58)
+#359 := (= #356 #58)
+#360 := [rewrite]: #359
+#357 := (= #69 #356)
+#358 := [monotonicity #355]: #357
+#362 := [trans #358 #360]: #361
+#365 := [monotonicity #362]: #364
+#373 := [trans #365 #371]: #372
+#393 := [monotonicity #373 #390]: #392
+#351 := [asserted]: #73
+#394 := [mp #351 #393]: #391
+#396 := [and-elim #394]: #386
+#402 := (* -1::real #63)
+#403 := (+ #51 #402)
+#404 := (<= #403 0::real)
+#414 := (* -1::real #58)
+#415 := (+ #51 #414)
+#413 := (>= #415 0::real)
+#64 := (f6 f11 #50)
+#407 := (* -1::real #64)
+#408 := (+ #63 #407)
+#409 := (<= #408 0::real)
+#423 := (and #404 #409 #413)
+#77 := (<= #63 #64)
+#76 := (<= #51 #63)
+#78 := (and #76 #77)
+#75 := (<= #58 #51)
+#79 := (and #75 #78)
+#426 := (iff #79 #423)
+#417 := (and #404 #409)
+#420 := (and #413 #417)
+#424 := (iff #420 #423)
+#425 := [rewrite]: #424
+#421 := (iff #79 #420)
+#418 := (iff #78 #417)
+#410 := (iff #77 #409)
+#411 := [rewrite]: #410
+#405 := (iff #76 #404)
+#406 := [rewrite]: #405
+#419 := [monotonicity #406 #411]: #418
+#412 := (iff #75 #413)
+#416 := [rewrite]: #412
+#422 := [monotonicity #416 #419]: #421
+#427 := [trans #422 #425]: #426
+#353 := [asserted]: #79
+#428 := [mp #353 #427]: #423
+#429 := [and-elim #428]: #404
+#642 := (+ #32 #402)
+#644 := (>= #642 0::real)
+#641 := (= #32 #63)
+#671 := (= #63 #32)
+#669 := (= #50 #29)
+#667 := (= #29 #50)
+#668 := [monotonicity #661]: #667
+#670 := [symm #668]: #669
+#672 := [monotonicity #670]: #671
+#673 := [symm #672]: #641
+#674 := (not #641)
+#675 := (or #674 #644)
+#676 := [th-lemma]: #675
+#677 := [unit-resolution #676 #673]: #644
+#475 := (+ #61 #472)
+#478 := (<= #475 0::real)
+#451 := (not #478)
+#327 := (ite #301 #284 #51)
+#335 := (* -1::real #327)
+#336 := (+ #61 #335)
+#337 := (<= #336 0::real)
+#338 := (not #337)
+#452 := (iff #338 #451)
+#479 := (iff #337 #478)
+#476 := (= #336 #475)
+#473 := (= #335 #472)
+#470 := (= #327 #284)
+#1 := true
+#465 := (ite true #284 #51)
+#468 := (= #465 #284)
+#469 := [rewrite]: #468
+#466 := (= #327 #465)
+#457 := (iff #301 true)
+#458 := [iff-true #400]: #457
+#467 := [monotonicity #458]: #466
+#471 := [trans #467 #469]: #470
+#474 := [monotonicity #471]: #473
+#477 := [monotonicity #474]: #476
+#480 := [monotonicity #477]: #479
+#481 := [monotonicity #480]: #452
+#308 := (ite #301 #64 #63)
+#318 := (* -1::real #308)
+#319 := (+ #61 #318)
+#317 := (>= #319 0::real)
+#316 := (not #317)
+#343 := (and #316 #338)
+#56 := (< #43 #26)
+#65 := (ite #56 #63 #64)
+#66 := (< #61 #65)
+#57 := (= f12 f5)
+#59 := (ite #57 #32 #58)
+#60 := (ite #56 #51 #59)
+#62 := (< #60 #61)
+#67 := (and #62 #66)
+#346 := (iff #67 #343)
+#287 := (ite #56 #51 #284)
+#290 := (< #287 #61)
+#296 := (and #66 #290)
+#344 := (iff #296 #343)
+#341 := (iff #290 #338)
+#332 := (< #327 #61)
+#339 := (iff #332 #338)
+#340 := [rewrite]: #339
+#333 := (iff #290 #332)
+#330 := (= #287 #327)
+#302 := (not #301)
+#324 := (ite #302 #51 #284)
+#328 := (= #324 #327)
+#329 := [rewrite]: #328
+#325 := (= #287 #324)
+#303 := (iff #56 #302)
+#304 := [rewrite]: #303
+#326 := [monotonicity #304]: #325
+#331 := [trans #326 #329]: #330
+#334 := [monotonicity #331]: #333
+#342 := [trans #334 #340]: #341
+#322 := (iff #66 #316)
+#313 := (< #61 #308)
+#320 := (iff #313 #316)
+#321 := [rewrite]: #320
+#314 := (iff #66 #313)
+#311 := (= #65 #308)
+#305 := (ite #302 #63 #64)
+#309 := (= #305 #308)
+#310 := [rewrite]: #309
+#306 := (= #65 #305)
+#307 := [monotonicity #304]: #306
+#312 := [trans #307 #310]: #311
+#315 := [monotonicity #312]: #314
+#323 := [trans #315 #321]: #322
+#345 := [monotonicity #323 #342]: #344
+#299 := (iff #67 #296)
+#293 := (and #290 #66)
+#297 := (iff #293 #296)
+#298 := [rewrite]: #297
+#294 := (iff #67 #293)
+#291 := (iff #62 #290)
+#288 := (= #60 #287)
+#285 := (= #59 #284)
+#231 := (iff #57 #49)
+#283 := [rewrite]: #231
+#286 := [monotonicity #283]: #285
+#289 := [monotonicity #286]: #288
+#292 := [monotonicity #289]: #291
+#295 := [monotonicity #292]: #294
+#300 := [trans #295 #298]: #299
+#347 := [trans #300 #345]: #346
+#184 := [asserted]: #67
+#348 := [mp #184 #347]: #343
+#350 := [and-elim #348]: #338
+#482 := [mp #350 #481]: #451
+#678 := [th-lemma #482 #677 #429 #396 #666]: false
+#679 := [lemma #678]: #576
+[unit-resolution #679 #695]: false
+unsat
+3563da621b35b09e69b7f5fa5fa01c2868364b3e 422 0
+#2 := false
+decl f12 :: S2
+#42 := f12
+decl f5 :: S2
+#25 := f5
+#45 := (= f5 f12)
+decl f3 :: (-> int S2)
+decl f4 :: (-> S2 int)
+#43 := (f4 f12)
+#598 := (f3 #43)
+#696 := (= #598 f12)
+#599 := (= f12 #598)
+#8 := (:var 0 S2)
+#9 := (f4 #8)
+#551 := (pattern #9)
+#10 := (f3 #9)
+#98 := (= #8 #10)
+#552 := (forall (vars (?v0 S2)) (:pat #551) #98)
+#101 := (forall (vars (?v0 S2)) #98)
+#555 := (iff #101 #552)
+#553 := (iff #98 #98)
+#554 := [refl]: #553
+#556 := [quant-intro #554]: #555
+#455 := (~ #101 #101)
+#457 := (~ #98 #98)
+#458 := [refl]: #457
+#456 := [nnf-pos #458]: #455
+#11 := (= #10 #8)
+#12 := (forall (vars (?v0 S2)) #11)
+#102 := (iff #12 #101)
+#99 := (iff #11 #98)
+#100 := [rewrite]: #99
+#103 := [quant-intro #100]: #102
+#97 := [asserted]: #12
+#106 := [mp #97 #103]: #101
+#453 := [mp~ #106 #456]: #101
+#557 := [mp #453 #556]: #552
+#600 := (not #552)
+#605 := (or #600 #599)
+#606 := [quant-inst]: #605
+#690 := [unit-resolution #606 #557]: #599
+#697 := [symm #690]: #696
+#698 := (= f5 #598)
+#26 := (f4 f5)
+#596 := (f3 #26)
+#694 := (= #596 #598)
+#692 := (= #598 #596)
+#688 := (= #43 #26)
+#686 := (= #26 #43)
+#13 := 0::int
+#231 := -1::int
+#234 := (* -1::int #43)
+#235 := (+ #26 #234)
+#295 := (<= #235 0::int)
+#74 := (<= #26 #43)
+#393 := (iff #74 #295)
+#394 := [rewrite]: #393
+#346 := [asserted]: #74
+#395 := [mp #346 #394]: #295
+#233 := (>= #235 0::int)
+decl f6 :: (-> S3 S4 real)
+decl f8 :: (-> S2 S4)
+#29 := (f8 f5)
+decl f7 :: S3
+#28 := f7
+#30 := (f6 f7 #29)
+decl f9 :: S3
+#31 := f9
+#32 := (f6 f9 #29)
+#46 := (f8 f12)
+decl f11 :: S3
+#37 := f11
+#47 := (f6 f11 #46)
+#48 := (ite #45 #47 #32)
+#241 := (ite #233 #48 #30)
+#572 := (= #30 #241)
+#658 := (not #572)
+#199 := 0::real
+#197 := -1::real
+#249 := (* -1::real #241)
+#647 := (+ #30 #249)
+#648 := (<= #647 0::real)
+#652 := (not #648)
+#650 := [hypothesis]: #648
+decl f10 :: S3
+#34 := f10
+#35 := (f6 f10 #29)
+#250 := (+ #35 #249)
+#251 := (<= #250 0::real)
+#252 := (not #251)
+#38 := (f6 f11 #29)
+decl f13 :: S3
+#51 := f13
+#52 := (f6 f13 #29)
+#260 := (ite #233 #52 #38)
+#269 := (* -1::real #260)
+#270 := (+ #35 #269)
+#268 := (>= #270 0::real)
+#271 := (not #268)
+#276 := (and #252 #271)
+#44 := (< #26 #43)
+#53 := (ite #44 #38 #52)
+#54 := (< #35 #53)
+#49 := (ite #44 #30 #48)
+#50 := (< #49 #35)
+#55 := (and #50 #54)
+#277 := (iff #55 #276)
+#274 := (iff #54 #271)
+#265 := (< #35 #260)
+#272 := (iff #265 #271)
+#273 := [rewrite]: #272
+#266 := (iff #54 #265)
+#263 := (= #53 #260)
+#232 := (not #233)
+#257 := (ite #232 #38 #52)
+#261 := (= #257 #260)
+#262 := [rewrite]: #261
+#258 := (= #53 #257)
+#236 := (iff #44 #232)
+#237 := [rewrite]: #236
+#259 := [monotonicity #237]: #258
+#264 := [trans #259 #262]: #263
+#267 := [monotonicity #264]: #266
+#275 := [trans #267 #273]: #274
+#255 := (iff #50 #252)
+#246 := (< #241 #35)
+#253 := (iff #246 #252)
+#254 := [rewrite]: #253
+#247 := (iff #50 #246)
+#244 := (= #49 #241)
+#238 := (ite #232 #30 #48)
+#242 := (= #238 #241)
+#243 := [rewrite]: #242
+#239 := (= #49 #238)
+#240 := [monotonicity #237]: #239
+#245 := [trans #240 #243]: #244
+#248 := [monotonicity #245]: #247
+#256 := [trans #248 #254]: #255
+#278 := [monotonicity #256 #275]: #277
+#183 := [asserted]: #55
+#279 := [mp #183 #278]: #276
+#280 := [and-elim #279]: #252
+#201 := (* -1::real #35)
+#217 := (+ #30 #201)
+#218 := (<= #217 0::real)
+#219 := (not #218)
+#202 := (+ #32 #201)
+#200 := (>= #202 0::real)
+#198 := (not #200)
+#224 := (and #198 #219)
+#27 := (< #26 #26)
+#39 := (ite #27 #38 #30)
+#40 := (< #35 #39)
+#33 := (ite #27 #30 #32)
+#36 := (< #33 #35)
+#41 := (and #36 #40)
+#225 := (iff #41 #224)
+#222 := (iff #40 #219)
+#214 := (< #35 #30)
+#220 := (iff #214 #219)
+#221 := [rewrite]: #220
+#215 := (iff #40 #214)
+#212 := (= #39 #30)
+#207 := (ite false #38 #30)
+#210 := (= #207 #30)
+#211 := [rewrite]: #210
+#208 := (= #39 #207)
+#185 := (iff #27 false)
+#186 := [rewrite]: #185
+#209 := [monotonicity #186]: #208
+#213 := [trans #209 #211]: #212
+#216 := [monotonicity #213]: #215
+#223 := [trans #216 #221]: #222
+#205 := (iff #36 #198)
+#194 := (< #32 #35)
+#203 := (iff #194 #198)
+#204 := [rewrite]: #203
+#195 := (iff #36 #194)
+#192 := (= #33 #32)
+#187 := (ite false #30 #32)
+#190 := (= #187 #32)
+#191 := [rewrite]: #190
+#188 := (= #33 #187)
+#189 := [monotonicity #186]: #188
+#193 := [trans #189 #191]: #192
+#196 := [monotonicity #193]: #195
+#206 := [trans #196 #204]: #205
+#226 := [monotonicity #206 #223]: #225
+#182 := [asserted]: #41
+#227 := [mp #182 #226]: #224
+#229 := [and-elim #227]: #219
+#651 := [th-lemma #229 #280 #650]: false
+#653 := [lemma #651]: #652
+#657 := [hypothesis]: #572
+#659 := (or #658 #648)
+#660 := [th-lemma]: #659
+#661 := [unit-resolution #660 #657 #653]: false
+#662 := [lemma #661]: #658
+#582 := (or #233 #572)
+#583 := [def-axiom]: #582
+#685 := [unit-resolution #583 #662]: #233
+#687 := [th-lemma #685 #395]: #686
+#689 := [symm #687]: #688
+#693 := [monotonicity #689]: #692
+#695 := [symm #693]: #694
+#597 := (= f5 #596)
+#601 := (or #600 #597)
+#602 := [quant-inst]: #601
+#691 := [unit-resolution #602 #557]: #597
+#699 := [trans #691 #695]: #698
+#700 := [trans #699 #697]: #45
+#575 := (not #45)
+#63 := (f6 f13 #46)
+#283 := (ite #45 #30 #63)
+#466 := (* -1::real #283)
+#642 := (+ #30 #466)
+#644 := (>= #642 0::real)
+#590 := (= #30 #283)
+#666 := [hypothesis]: #45
+#592 := (or #575 #590)
+#593 := [def-axiom]: #592
+#667 := [unit-resolution #593 #666]: #590
+#668 := (not #590)
+#669 := (or #668 #644)
+#670 := [th-lemma]: #669
+#671 := [unit-resolution #670 #667]: #644
+#60 := (f6 f10 #46)
+#362 := (* -1::real #60)
+#363 := (+ #47 #362)
+#361 := (>= #363 0::real)
+#360 := (not #361)
+#379 := (* -1::real #63)
+#380 := (+ #60 #379)
+#378 := (>= #380 0::real)
+#381 := (not #378)
+#386 := (and #360 #381)
+#68 := (< #43 #43)
+#71 := (ite #68 #47 #63)
+#72 := (< #60 #71)
+#57 := (f6 f7 #46)
+#69 := (ite #68 #57 #47)
+#70 := (< #69 #60)
+#73 := (and #70 #72)
+#387 := (iff #73 #386)
+#384 := (iff #72 #381)
+#375 := (< #60 #63)
+#382 := (iff #375 #381)
+#383 := [rewrite]: #382
+#376 := (iff #72 #375)
+#373 := (= #71 #63)
+#368 := (ite false #47 #63)
+#371 := (= #368 #63)
+#372 := [rewrite]: #371
+#369 := (= #71 #368)
+#348 := (iff #68 false)
+#349 := [rewrite]: #348
+#370 := [monotonicity #349]: #369
+#374 := [trans #370 #372]: #373
+#377 := [monotonicity #374]: #376
+#385 := [trans #377 #383]: #384
+#366 := (iff #70 #360)
+#357 := (< #47 #60)
+#364 := (iff #357 #360)
+#365 := [rewrite]: #364
+#358 := (iff #70 #357)
+#355 := (= #69 #47)
+#350 := (ite false #57 #47)
+#353 := (= #350 #47)
+#354 := [rewrite]: #353
+#351 := (= #69 #350)
+#352 := [monotonicity #349]: #351
+#356 := [trans #352 #354]: #355
+#359 := [monotonicity #356]: #358
+#367 := [trans #359 #365]: #366
+#388 := [monotonicity #367 #385]: #387
+#345 := [asserted]: #73
+#389 := [mp #345 #388]: #386
+#390 := [and-elim #389]: #360
+#399 := (* -1::real #57)
+#400 := (+ #47 #399)
+#398 := (>= #400 0::real)
+#58 := (f6 f9 #46)
+#407 := (* -1::real #58)
+#408 := (+ #57 #407)
+#406 := (>= #408 0::real)
+#402 := (+ #47 #379)
+#403 := (<= #402 0::real)
+#417 := (and #398 #403 #406)
+#77 := (<= #47 #63)
+#76 := (<= #57 #47)
+#78 := (and #76 #77)
+#75 := (<= #58 #57)
+#79 := (and #75 #78)
+#420 := (iff #79 #417)
+#411 := (and #398 #403)
+#414 := (and #406 #411)
+#418 := (iff #414 #417)
+#419 := [rewrite]: #418
+#415 := (iff #79 #414)
+#412 := (iff #78 #411)
+#404 := (iff #77 #403)
+#405 := [rewrite]: #404
+#397 := (iff #76 #398)
+#401 := [rewrite]: #397
+#413 := [monotonicity #401 #405]: #412
+#409 := (iff #75 #406)
+#410 := [rewrite]: #409
+#416 := [monotonicity #410 #413]: #415
+#421 := [trans #416 #419]: #420
+#347 := [asserted]: #79
+#422 := [mp #347 #421]: #417
+#423 := [and-elim #422]: #398
+#655 := (+ #30 #399)
+#656 := (<= #655 0::real)
+#654 := (= #30 #57)
+#676 := (= #57 #30)
+#674 := (= #46 #29)
+#672 := (= #29 #46)
+#673 := [monotonicity #666]: #672
+#675 := [symm #673]: #674
+#677 := [monotonicity #675]: #676
+#678 := [symm #677]: #654
+#679 := (not #654)
+#680 := (or #679 #656)
+#681 := [th-lemma]: #680
+#682 := [unit-resolution #681 #678]: #656
+#469 := (+ #60 #466)
+#472 := (>= #469 0::real)
+#445 := (not #472)
+#321 := (ite #295 #283 #47)
+#331 := (* -1::real #321)
+#332 := (+ #60 #331)
+#330 := (>= #332 0::real)
+#329 := (not #330)
+#446 := (iff #329 #445)
+#473 := (iff #330 #472)
+#470 := (= #332 #469)
+#467 := (= #331 #466)
+#464 := (= #321 #283)
+#1 := true
+#459 := (ite true #283 #47)
+#462 := (= #459 #283)
+#463 := [rewrite]: #462
+#460 := (= #321 #459)
+#451 := (iff #295 true)
+#452 := [iff-true #395]: #451
+#461 := [monotonicity #452]: #460
+#465 := [trans #461 #463]: #464
+#468 := [monotonicity #465]: #467
+#471 := [monotonicity #468]: #470
+#474 := [monotonicity #471]: #473
+#475 := [monotonicity #474]: #446
+#302 := (ite #295 #58 #57)
+#310 := (* -1::real #302)
+#311 := (+ #60 #310)
+#312 := (<= #311 0::real)
+#313 := (not #312)
+#337 := (and #313 #329)
+#62 := (= f12 f5)
+#64 := (ite #62 #30 #63)
+#56 := (< #43 #26)
+#65 := (ite #56 #47 #64)
+#66 := (< #60 #65)
+#59 := (ite #56 #57 #58)
+#61 := (< #59 #60)
+#67 := (and #61 #66)
+#340 := (iff #67 #337)
+#286 := (ite #56 #47 #283)
+#289 := (< #60 #286)
+#292 := (and #61 #289)
+#338 := (iff #292 #337)
+#335 := (iff #289 #329)
+#326 := (< #60 #321)
+#333 := (iff #326 #329)
+#334 := [rewrite]: #333
+#327 := (iff #289 #326)
+#324 := (= #286 #321)
+#296 := (not #295)
+#318 := (ite #296 #47 #283)
+#322 := (= #318 #321)
+#323 := [rewrite]: #322
+#319 := (= #286 #318)
+#297 := (iff #56 #296)
+#298 := [rewrite]: #297
+#320 := [monotonicity #298]: #319
+#325 := [trans #320 #323]: #324
+#328 := [monotonicity #325]: #327
+#336 := [trans #328 #334]: #335
+#316 := (iff #61 #313)
+#307 := (< #302 #60)
+#314 := (iff #307 #313)
+#315 := [rewrite]: #314
+#308 := (iff #61 #307)
+#305 := (= #59 #302)
+#299 := (ite #296 #57 #58)
+#303 := (= #299 #302)
+#304 := [rewrite]: #303
+#300 := (= #59 #299)
+#301 := [monotonicity #298]: #300
+#306 := [trans #301 #304]: #305
+#309 := [monotonicity #306]: #308
+#317 := [trans #309 #315]: #316
+#339 := [monotonicity #317 #336]: #338
+#293 := (iff #67 #292)
+#290 := (iff #66 #289)
+#287 := (= #65 #286)
+#284 := (= #64 #283)
+#230 := (iff #62 #45)
+#282 := [rewrite]: #230
+#285 := [monotonicity #282]: #284
+#288 := [monotonicity #285]: #287
+#291 := [monotonicity #288]: #290
+#294 := [monotonicity #291]: #293
+#341 := [trans #294 #339]: #340
+#184 := [asserted]: #67
+#342 := [mp #184 #341]: #337
+#344 := [and-elim #342]: #329
+#476 := [mp #344 #475]: #445
+#683 := [th-lemma #476 #682 #423 #390 #671]: false
+#684 := [lemma #683]: #575
+[unit-resolution #684 #700]: false
+unsat
+84444fc7be1372d94ec0514d2ec99e1693c028e3 921 0
+#2 := false
+#58 := 0::int
+decl f5 :: (-> S4 int)
+decl f6 :: (-> S2 S4)
+decl f11 :: (-> S4 S2)
+decl f14 :: S4
+#30 := f14
+#34 := (f11 f14)
+#70 := (f6 #34)
+#605 := (f5 #70)
+#121 := -1::int
+#615 := (* -1::int #605)
+decl f7 :: S4
+#13 := f7
+#14 := (f5 f7)
+#662 := (+ #14 #615)
+#663 := (<= #662 0::int)
+decl f8 :: (-> S5 S2 real)
+decl f19 :: (-> S3 S5)
+decl f15 :: S3
+#40 := f15
+#86 := (f19 f15)
+#650 := (f8 #86 #34)
+decl f10 :: S5
+#19 := f10
+#35 := (f8 f10 #34)
+#651 := (= #35 #650)
+#690 := (not #651)
+decl f13 :: S3
+#28 := f13
+#81 := (f19 f13)
+#749 := (f8 #81 #34)
+#1233 := (= #650 #749)
+#1246 := (not #1233)
+#1335 := (iff #1246 #690)
+#1333 := (iff #1233 #651)
+#1328 := (= #650 #35)
+#1331 := (iff #1328 #651)
+#1332 := [commutativity]: #1331
+#1329 := (iff #1233 #1328)
+#1326 := (= #749 #35)
+#752 := (= #35 #749)
+decl f12 :: S5
+#22 := f12
+#696 := (f8 f12 #34)
+#751 := (= #696 #749)
+#281 := (= f14 #70)
+#755 := (ite #281 #752 #751)
+decl f9 :: S5
+#16 := f9
+#694 := (f8 f9 #34)
+#750 := (= #694 #749)
+#31 := (f5 f14)
+#616 := (+ #31 #615)
+#617 := (<= #616 0::int)
+#758 := (ite #617 #755 #750)
+#9 := (:var 0 S2)
+#17 := (f8 f9 #9)
+#538 := (pattern #17)
+#23 := (f8 f12 #9)
+#537 := (pattern #23)
+#82 := (f8 #81 #9)
+#545 := (pattern #82)
+#11 := (f6 #9)
+#535 := (pattern #11)
+#452 := (= #17 #82)
+#450 := (= #23 #82)
+#449 := (= #35 #82)
+#33 := (= #11 f14)
+#451 := (ite #33 #449 #450)
+#146 := (* -1::int #31)
+#12 := (f5 #11)
+#147 := (+ #12 #146)
+#145 := (>= #147 0::int)
+#453 := (ite #145 #451 #452)
+#546 := (forall (vars (?v0 S2)) (:pat #535 #545 #537 #538) #453)
+#456 := (forall (vars (?v0 S2)) #453)
+#549 := (iff #456 #546)
+#547 := (iff #453 #453)
+#548 := [refl]: #547
+#550 := [quant-intro #548]: #549
+#36 := (ite #33 #35 #23)
+#153 := (ite #145 #36 #17)
+#380 := (= #82 #153)
+#381 := (forall (vars (?v0 S2)) #380)
+#457 := (iff #381 #456)
+#454 := (iff #380 #453)
+#455 := [rewrite]: #454
+#458 := [quant-intro #455]: #457
+#366 := (~ #381 #381)
+#368 := (~ #380 #380)
+#365 := [refl]: #368
+#363 := [nnf-pos #365]: #366
+decl f3 :: (-> S3 S2 real)
+#29 := (f3 f13 #9)
+#158 := (= #29 #153)
+#161 := (forall (vars (?v0 S2)) #158)
+#382 := (iff #161 #381)
+#96 := (:var 1 S3)
+#99 := (f3 #96 #9)
+#97 := (f19 #96)
+#98 := (f8 #97 #9)
+#100 := (= #98 #99)
+#101 := (forall (vars (?v0 S3) (?v1 S2)) #100)
+#298 := [asserted]: #101
+#383 := [rewrite* #298]: #382
+#32 := (< #12 #31)
+#37 := (ite #32 #17 #36)
+#38 := (= #29 #37)
+#39 := (forall (vars (?v0 S2)) #38)
+#162 := (iff #39 #161)
+#159 := (iff #38 #158)
+#156 := (= #37 #153)
+#144 := (not #145)
+#150 := (ite #144 #17 #36)
+#154 := (= #150 #153)
+#155 := [rewrite]: #154
+#151 := (= #37 #150)
+#148 := (iff #32 #144)
+#149 := [rewrite]: #148
+#152 := [monotonicity #149]: #151
+#157 := [trans #152 #155]: #156
+#160 := [monotonicity #157]: #159
+#163 := [quant-intro #160]: #162
+#119 := [asserted]: #39
+#164 := [mp #119 #163]: #161
+#384 := [mp #164 #383]: #381
+#364 := [mp~ #384 #363]: #381
+#459 := [mp #364 #458]: #456
+#551 := [mp #459 #550]: #546
+#761 := (not #546)
+#762 := (or #761 #758)
+#71 := (= #70 f14)
+#753 := (ite #71 #752 #751)
+#606 := (+ #605 #146)
+#607 := (>= #606 0::int)
+#754 := (ite #607 #753 #750)
+#763 := (or #761 #754)
+#765 := (iff #763 #762)
+#767 := (iff #762 #762)
+#768 := [rewrite]: #767
+#759 := (iff #754 #758)
+#756 := (iff #753 #755)
+#282 := (iff #71 #281)
+#283 := [rewrite]: #282
+#757 := [monotonicity #283]: #756
+#620 := (iff #607 #617)
+#609 := (+ #146 #605)
+#612 := (>= #609 0::int)
+#618 := (iff #612 #617)
+#619 := [rewrite]: #618
+#613 := (iff #607 #612)
+#610 := (= #606 #609)
+#611 := [rewrite]: #610
+#614 := [monotonicity #611]: #613
+#621 := [trans #614 #619]: #620
+#760 := [monotonicity #621 #757]: #759
+#766 := [monotonicity #760]: #765
+#769 := [trans #766 #768]: #765
+#764 := [quant-inst]: #763
+#770 := [mp #764 #769]: #762
+#1317 := [unit-resolution #770 #551]: #758
+#981 := (= #31 #605)
+#1295 := (= #605 #31)
+#280 := [asserted]: #71
+#286 := [mp #280 #283]: #281
+#1290 := [symm #286]: #71
+#1296 := [monotonicity #1290]: #1295
+#1297 := [symm #1296]: #981
+#1318 := (not #981)
+#1319 := (or #1318 #617)
+#1320 := [th-lemma]: #1319
+#1321 := [unit-resolution #1320 #1297]: #617
+#639 := (not #617)
+#783 := (not #758)
+#784 := (or #783 #639 #755)
+#785 := [def-axiom]: #784
+#1322 := [unit-resolution #785 #1321 #1317]: #755
+#771 := (not #755)
+#1323 := (or #771 #752)
+#772 := (not #281)
+#773 := (or #771 #772 #752)
+#774 := [def-axiom]: #773
+#1324 := [unit-resolution #774 #286]: #1323
+#1325 := [unit-resolution #1324 #1322]: #752
+#1327 := [symm #1325]: #1326
+#1330 := [monotonicity #1327]: #1329
+#1334 := [trans #1330 #1332]: #1333
+#1336 := [monotonicity #1334]: #1335
+#303 := 0::real
+#301 := -1::real
+#1033 := (* -1::real #749)
+#1234 := (+ #650 #1033)
+#1236 := (>= #1234 0::real)
+#1243 := (not #1236)
+#1237 := [hypothesis]: #1236
+decl f20 :: S5
+#78 := f20
+#1034 := (f8 f20 #34)
+#1037 := (* -1::real #1034)
+#1048 := (+ #749 #1037)
+#1049 := (<= #1048 0::real)
+#1073 := (not #1049)
+decl f17 :: S3
+#48 := f17
+#76 := (f19 f17)
+#601 := (f8 #76 #34)
+#1038 := (+ #601 #1037)
+#1039 := (>= #1038 0::real)
+#1054 := (or #1039 #1049)
+#1057 := (not #1054)
+#79 := (f8 f20 #9)
+#588 := (pattern #79)
+#77 := (f8 #76 #9)
+#561 := (pattern #77)
+#310 := (* -1::real #82)
+#311 := (+ #79 #310)
+#309 := (>= #311 0::real)
+#305 := (* -1::real #79)
+#306 := (+ #77 #305)
+#304 := (>= #306 0::real)
+#422 := (or #304 #309)
+#423 := (not #422)
+#589 := (forall (vars (?v0 S2)) (:pat #561 #588 #545) #423)
+#426 := (forall (vars (?v0 S2)) #423)
+#592 := (iff #426 #589)
+#590 := (iff #423 #423)
+#591 := [refl]: #590
+#593 := [quant-intro #591]: #592
+#312 := (not #309)
+#302 := (not #304)
+#315 := (and #302 #312)
+#318 := (forall (vars (?v0 S2)) #315)
+#427 := (iff #318 #426)
+#424 := (iff #315 #423)
+#425 := [rewrite]: #424
+#428 := [quant-intro #425]: #427
+#414 := (~ #318 #318)
+#412 := (~ #315 #315)
+#413 := [refl]: #412
+#415 := [nnf-pos #413]: #414
+decl f4 :: S3
+#8 := f4
+#89 := (f19 f4)
+#90 := (f8 #89 #9)
+#328 := (* -1::real #90)
+#329 := (+ #79 #328)
+#327 := (>= #329 0::real)
+#330 := (not #327)
+#87 := (f8 #86 #9)
+#321 := (* -1::real #87)
+#322 := (+ #79 #321)
+#323 := (<= #322 0::real)
+#324 := (not #323)
+#333 := (and #324 #330)
+#336 := (forall (vars (?v0 S2)) #333)
+#339 := (and #318 #336)
+#91 := (< #79 #90)
+#88 := (< #87 #79)
+#92 := (and #88 #91)
+#93 := (forall (vars (?v0 S2)) #92)
+#83 := (< #79 #82)
+#80 := (< #77 #79)
+#84 := (and #80 #83)
+#85 := (forall (vars (?v0 S2)) #84)
+#94 := (and #85 #93)
+#340 := (iff #94 #339)
+#337 := (iff #93 #336)
+#334 := (iff #92 #333)
+#331 := (iff #91 #330)
+#332 := [rewrite]: #331
+#325 := (iff #88 #324)
+#326 := [rewrite]: #325
+#335 := [monotonicity #326 #332]: #334
+#338 := [quant-intro #335]: #337
+#319 := (iff #85 #318)
+#316 := (iff #84 #315)
+#313 := (iff #83 #312)
+#314 := [rewrite]: #313
+#307 := (iff #80 #302)
+#308 := [rewrite]: #307
+#317 := [monotonicity #308 #314]: #316
+#320 := [quant-intro #317]: #319
+#341 := [monotonicity #320 #338]: #340
+#297 := [asserted]: #94
+#342 := [mp #297 #341]: #339
+#343 := [and-elim #342]: #318
+#416 := [mp~ #343 #415]: #318
+#429 := [mp #416 #428]: #426
+#594 := [mp #429 #593]: #589
+#1060 := (not #589)
+#1061 := (or #1060 #1057)
+#1035 := (+ #1034 #1033)
+#1036 := (>= #1035 0::real)
+#1040 := (or #1039 #1036)
+#1041 := (not #1040)
+#1062 := (or #1060 #1041)
+#1064 := (iff #1062 #1061)
+#1066 := (iff #1061 #1061)
+#1067 := [rewrite]: #1066
+#1058 := (iff #1041 #1057)
+#1055 := (iff #1040 #1054)
+#1052 := (iff #1036 #1049)
+#1042 := (+ #1033 #1034)
+#1045 := (>= #1042 0::real)
+#1050 := (iff #1045 #1049)
+#1051 := [rewrite]: #1050
+#1046 := (iff #1036 #1045)
+#1043 := (= #1035 #1042)
+#1044 := [rewrite]: #1043
+#1047 := [monotonicity #1044]: #1046
+#1053 := [trans #1047 #1051]: #1052
+#1056 := [monotonicity #1053]: #1055
+#1059 := [monotonicity #1056]: #1058
+#1065 := [monotonicity #1059]: #1064
+#1068 := [trans #1065 #1067]: #1064
+#1063 := [quant-inst]: #1062
+#1069 := [mp #1063 #1068]: #1061
+#1238 := [unit-resolution #1069 #594]: #1057
+#1074 := (or #1054 #1073)
+#1075 := [def-axiom]: #1074
+#1239 := [unit-resolution #1075 #1238]: #1073
+#1150 := (+ #650 #1037)
+#1151 := (>= #1150 0::real)
+#1183 := (not #1151)
+#693 := (f8 #89 #34)
+#1162 := (+ #693 #1037)
+#1163 := (<= #1162 0::real)
+#1168 := (or #1151 #1163)
+#1171 := (not #1168)
+#536 := (pattern #90)
+#553 := (pattern #87)
+#430 := (or #323 #327)
+#431 := (not #430)
+#595 := (forall (vars (?v0 S2)) (:pat #588 #553 #536) #431)
+#434 := (forall (vars (?v0 S2)) #431)
+#598 := (iff #434 #595)
+#596 := (iff #431 #431)
+#597 := [refl]: #596
+#599 := [quant-intro #597]: #598
+#435 := (iff #336 #434)
+#432 := (iff #333 #431)
+#433 := [rewrite]: #432
+#436 := [quant-intro #433]: #435
+#419 := (~ #336 #336)
+#417 := (~ #333 #333)
+#418 := [refl]: #417
+#420 := [nnf-pos #418]: #419
+#344 := [and-elim #342]: #336
+#421 := [mp~ #344 #420]: #336
+#437 := [mp #421 #436]: #434
+#600 := [mp #437 #599]: #595
+#1118 := (not #595)
+#1174 := (or #1118 #1171)
+#1136 := (* -1::real #693)
+#1137 := (+ #1034 #1136)
+#1138 := (>= #1137 0::real)
+#1139 := (* -1::real #650)
+#1140 := (+ #1034 #1139)
+#1141 := (<= #1140 0::real)
+#1142 := (or #1141 #1138)
+#1143 := (not #1142)
+#1175 := (or #1118 #1143)
+#1177 := (iff #1175 #1174)
+#1179 := (iff #1174 #1174)
+#1180 := [rewrite]: #1179
+#1172 := (iff #1143 #1171)
+#1169 := (iff #1142 #1168)
+#1166 := (iff #1138 #1163)
+#1156 := (+ #1136 #1034)
+#1159 := (>= #1156 0::real)
+#1164 := (iff #1159 #1163)
+#1165 := [rewrite]: #1164
+#1160 := (iff #1138 #1159)
+#1157 := (= #1137 #1156)
+#1158 := [rewrite]: #1157
+#1161 := [monotonicity #1158]: #1160
+#1167 := [trans #1161 #1165]: #1166
+#1154 := (iff #1141 #1151)
+#1144 := (+ #1139 #1034)
+#1147 := (<= #1144 0::real)
+#1152 := (iff #1147 #1151)
+#1153 := [rewrite]: #1152
+#1148 := (iff #1141 #1147)
+#1145 := (= #1140 #1144)
+#1146 := [rewrite]: #1145
+#1149 := [monotonicity #1146]: #1148
+#1155 := [trans #1149 #1153]: #1154
+#1170 := [monotonicity #1155 #1167]: #1169
+#1173 := [monotonicity #1170]: #1172
+#1178 := [monotonicity #1173]: #1177
+#1181 := [trans #1178 #1180]: #1177
+#1176 := [quant-inst]: #1175
+#1182 := [mp #1176 #1181]: #1174
+#1240 := [unit-resolution #1182 #600]: #1171
+#1184 := (or #1168 #1183)
+#1185 := [def-axiom]: #1184
+#1241 := [unit-resolution #1185 #1240]: #1183
+#1242 := [th-lemma #1241 #1239 #1237]: false
+#1244 := [lemma #1242]: #1243
+#1247 := (or #1246 #1236)
+#1248 := [th-lemma]: #1247
+#1316 := [unit-resolution #1248 #1244]: #1246
+#1337 := [mp #1316 #1336]: #690
+#1339 := (or #663 #651)
+decl f16 :: S5
+#43 := f16
+#603 := (f8 f16 #34)
+#652 := (= #603 #650)
+#668 := (ite #663 #652 #651)
+#42 := (f8 f10 #9)
+#554 := (pattern #42)
+#44 := (f8 f16 #9)
+#552 := (pattern #44)
+#461 := (= #42 #87)
+#460 := (= #44 #87)
+#124 := (* -1::int #14)
+#125 := (+ #12 #124)
+#123 := (>= #125 0::int)
+#462 := (ite #123 #460 #461)
+#555 := (forall (vars (?v0 S2)) (:pat #535 #552 #553 #554) #462)
+#465 := (forall (vars (?v0 S2)) #462)
+#558 := (iff #465 #555)
+#556 := (iff #462 #462)
+#557 := [refl]: #556
+#559 := [quant-intro #557]: #558
+#169 := (ite #123 #44 #42)
+#385 := (= #87 #169)
+#386 := (forall (vars (?v0 S2)) #385)
+#466 := (iff #386 #465)
+#463 := (iff #385 #462)
+#464 := [rewrite]: #463
+#467 := [quant-intro #464]: #466
+#359 := (~ #386 #386)
+#361 := (~ #385 #385)
+#362 := [refl]: #361
+#360 := [nnf-pos #362]: #359
+#41 := (f3 f15 #9)
+#174 := (= #41 #169)
+#177 := (forall (vars (?v0 S2)) #174)
+#387 := (iff #177 #386)
+#388 := [rewrite* #298]: #387
+#15 := (< #12 #14)
+#45 := (ite #15 #42 #44)
+#46 := (= #41 #45)
+#47 := (forall (vars (?v0 S2)) #46)
+#178 := (iff #47 #177)
+#175 := (iff #46 #174)
+#172 := (= #45 #169)
+#122 := (not #123)
+#166 := (ite #122 #42 #44)
+#170 := (= #166 #169)
+#171 := [rewrite]: #170
+#167 := (= #45 #166)
+#126 := (iff #15 #122)
+#127 := [rewrite]: #126
+#168 := [monotonicity #127]: #167
+#173 := [trans #168 #171]: #172
+#176 := [monotonicity #173]: #175
+#179 := [quant-intro #176]: #178
+#120 := [asserted]: #47
+#180 := [mp #120 #179]: #177
+#389 := [mp #180 #388]: #386
+#357 := [mp~ #389 #360]: #386
+#468 := [mp #357 #467]: #465
+#560 := [mp #468 #559]: #555
+#671 := (not #555)
+#672 := (or #671 #668)
+#653 := (+ #605 #124)
+#654 := (>= #653 0::int)
+#655 := (ite #654 #652 #651)
+#673 := (or #671 #655)
+#675 := (iff #673 #672)
+#677 := (iff #672 #672)
+#678 := [rewrite]: #677
+#669 := (iff #655 #668)
+#666 := (iff #654 #663)
+#656 := (+ #124 #605)
+#659 := (>= #656 0::int)
+#664 := (iff #659 #663)
+#665 := [rewrite]: #664
+#660 := (iff #654 #659)
+#657 := (= #653 #656)
+#658 := [rewrite]: #657
+#661 := [monotonicity #658]: #660
+#667 := [trans #661 #665]: #666
+#670 := [monotonicity #667]: #669
+#676 := [monotonicity #670]: #675
+#679 := [trans #676 #678]: #675
+#674 := [quant-inst]: #673
+#680 := [mp #674 #679]: #672
+#1338 := [unit-resolution #680 #560]: #668
+#681 := (not #668)
+#685 := (or #681 #663 #651)
+#686 := [def-axiom]: #685
+#1340 := [unit-resolution #686 #1338]: #1339
+#1341 := [unit-resolution #1340 #1337]: #663
+#1286 := (+ #14 #146)
+#1287 := (<= #1286 0::int)
+#1376 := (not #1287)
+#1285 := (= #14 #31)
+#1314 := (not #1285)
+#290 := (= f7 f14)
+#702 := (= f7 #70)
+decl f18 :: (-> int S4)
+#985 := (f18 #605)
+#1305 := (= #985 #70)
+#986 := (= #70 #985)
+#53 := (:var 0 S4)
+#54 := (f5 #53)
+#568 := (pattern #54)
+#55 := (f18 #54)
+#181 := (= #53 #55)
+#569 := (forall (vars (?v0 S4)) (:pat #568) #181)
+#199 := (forall (vars (?v0 S4)) #181)
+#572 := (iff #199 #569)
+#570 := (iff #181 #181)
+#571 := [refl]: #570
+#573 := [quant-intro #571]: #572
+#399 := (~ #199 #199)
+#397 := (~ #181 #181)
+#398 := [refl]: #397
+#400 := [nnf-pos #398]: #399
+#56 := (= #55 #53)
+#57 := (forall (vars (?v0 S4)) #56)
+#200 := (iff #57 #199)
+#197 := (iff #56 #181)
+#198 := [rewrite]: #197
+#201 := [quant-intro #198]: #200
+#165 := [asserted]: #57
+#204 := [mp #165 #201]: #199
+#401 := [mp~ #204 #400]: #199
+#574 := [mp #401 #573]: #569
+#989 := (not #569)
+#990 := (or #989 #986)
+#991 := [quant-inst]: #990
+#1289 := [unit-resolution #991 #574]: #986
+#1306 := [symm #1289]: #1305
+#1309 := (= f7 #985)
+#20 := (f11 f7)
+#72 := (f6 #20)
+#797 := (f5 #72)
+#987 := (f18 #797)
+#1303 := (= #987 #985)
+#1300 := (= #797 #605)
+#1298 := (= #797 #31)
+#1291 := [hypothesis]: #1285
+#1293 := (= #797 #14)
+#73 := (= #72 f7)
+#285 := (= f7 #72)
+#287 := (iff #73 #285)
+#288 := [rewrite]: #287
+#284 := [asserted]: #73
+#291 := [mp #284 #288]: #285
+#1292 := [symm #291]: #73
+#1294 := [monotonicity #1292]: #1293
+#1299 := [trans #1294 #1291]: #1298
+#1301 := [trans #1299 #1297]: #1300
+#1304 := [monotonicity #1301]: #1303
+#1307 := (= f7 #987)
+#988 := (= #72 #987)
+#994 := (or #989 #988)
+#995 := [quant-inst]: #994
+#1302 := [unit-resolution #995 #574]: #988
+#1308 := [trans #291 #1302]: #1307
+#1310 := [trans #1308 #1304]: #1309
+#1311 := [trans #1310 #1306]: #702
+#1312 := [trans #1311 #1290]: #290
+#294 := (not #290)
+#74 := (= f14 f7)
+#75 := (not #74)
+#295 := (iff #75 #294)
+#292 := (iff #74 #290)
+#293 := [rewrite]: #292
+#296 := [monotonicity #293]: #295
+#289 := [asserted]: #75
+#299 := [mp #289 #296]: #294
+#1313 := [unit-resolution #299 #1312]: false
+#1315 := [lemma #1313]: #1314
+#1380 := (or #1285 #1376)
+#1288 := (>= #1286 0::int)
+#807 := (* -1::int #797)
+#808 := (+ #31 #807)
+#809 := (<= #808 0::int)
+#793 := (f8 #76 #20)
+#21 := (f8 f10 #20)
+#794 := (= #21 #793)
+#838 := (not #794)
+#883 := (f8 #89 #20)
+#1259 := (= #793 #883)
+#1272 := (not #1259)
+#1362 := (iff #1272 #838)
+#1360 := (iff #1259 #794)
+#1355 := (= #793 #21)
+#1358 := (iff #1355 #794)
+#1359 := [commutativity]: #1358
+#1356 := (iff #1259 #1355)
+#1353 := (= #883 #21)
+#888 := (= #21 #883)
+#886 := (f8 f12 #20)
+#891 := (= #883 #886)
+#894 := (ite #285 #888 #891)
+#884 := (f8 f9 #20)
+#897 := (= #883 #884)
+#853 := (+ #14 #807)
+#854 := (<= #853 0::int)
+#900 := (ite #854 #894 #897)
+#441 := (= #17 #90)
+#439 := (= #23 #90)
+#438 := (= #21 #90)
+#18 := (= #11 f7)
+#440 := (ite #18 #438 #439)
+#442 := (ite #123 #440 #441)
+#539 := (forall (vars (?v0 S2)) (:pat #535 #536 #537 #538) #442)
+#445 := (forall (vars (?v0 S2)) #442)
+#542 := (iff #445 #539)
+#540 := (iff #442 #442)
+#541 := [refl]: #540
+#543 := [quant-intro #541]: #542
+#24 := (ite #18 #21 #23)
+#131 := (ite #123 #24 #17)
+#375 := (= #90 #131)
+#376 := (forall (vars (?v0 S2)) #375)
+#446 := (iff #376 #445)
+#443 := (iff #375 #442)
+#444 := [rewrite]: #443
+#447 := [quant-intro #444]: #446
+#369 := (~ #376 #376)
+#371 := (~ #375 #375)
+#372 := [refl]: #371
+#370 := [nnf-pos #372]: #369
+#10 := (f3 f4 #9)
+#136 := (= #10 #131)
+#139 := (forall (vars (?v0 S2)) #136)
+#377 := (iff #139 #376)
+#378 := [rewrite* #298]: #377
+#25 := (ite #15 #17 #24)
+#26 := (= #10 #25)
+#27 := (forall (vars (?v0 S2)) #26)
+#140 := (iff #27 #139)
+#137 := (iff #26 #136)
+#134 := (= #25 #131)
+#128 := (ite #122 #17 #24)
+#132 := (= #128 #131)
+#133 := [rewrite]: #132
+#129 := (= #25 #128)
+#130 := [monotonicity #127]: #129
+#135 := [trans #130 #133]: #134
+#138 := [monotonicity #135]: #137
+#141 := [quant-intro #138]: #140
+#118 := [asserted]: #27
+#142 := [mp #118 #141]: #139
+#379 := [mp #142 #378]: #376
+#367 := [mp~ #379 #370]: #376
+#448 := [mp #367 #447]: #445
+#544 := [mp #448 #543]: #539
+#717 := (not #539)
+#903 := (or #717 #900)
+#885 := (= #884 #883)
+#887 := (= #886 #883)
+#889 := (ite #73 #888 #887)
+#844 := (+ #797 #124)
+#845 := (>= #844 0::int)
+#890 := (ite #845 #889 #885)
+#904 := (or #717 #890)
+#906 := (iff #904 #903)
+#908 := (iff #903 #903)
+#909 := [rewrite]: #908
+#901 := (iff #890 #900)
+#898 := (iff #885 #897)
+#899 := [rewrite]: #898
+#895 := (iff #889 #894)
+#892 := (iff #887 #891)
+#893 := [rewrite]: #892
+#896 := [monotonicity #288 #893]: #895
+#857 := (iff #845 #854)
+#847 := (+ #124 #797)
+#850 := (>= #847 0::int)
+#855 := (iff #850 #854)
+#856 := [rewrite]: #855
+#851 := (iff #845 #850)
+#848 := (= #844 #847)
+#849 := [rewrite]: #848
+#852 := [monotonicity #849]: #851
+#858 := [trans #852 #856]: #857
+#902 := [monotonicity #858 #896 #899]: #901
+#907 := [monotonicity #902]: #906
+#910 := [trans #907 #909]: #906
+#905 := [quant-inst]: #904
+#911 := [mp #905 #910]: #903
+#1343 := [unit-resolution #911 #544]: #900
+#983 := (= #14 #797)
+#1344 := [symm #1294]: #983
+#1345 := (not #983)
+#1346 := (or #1345 #854)
+#1347 := [th-lemma]: #1346
+#1348 := [unit-resolution #1347 #1344]: #854
+#872 := (not #854)
+#924 := (not #900)
+#925 := (or #924 #872 #894)
+#926 := [def-axiom]: #925
+#1349 := [unit-resolution #926 #1348 #1343]: #894
+#912 := (not #894)
+#1350 := (or #912 #888)
+#913 := (not #285)
+#914 := (or #912 #913 #888)
+#915 := [def-axiom]: #914
+#1351 := [unit-resolution #915 #291]: #1350
+#1352 := [unit-resolution #1351 #1349]: #888
+#1354 := [symm #1352]: #1353
+#1357 := [monotonicity #1354]: #1356
+#1361 := [trans #1357 #1359]: #1360
+#1363 := [monotonicity #1361]: #1362
+#1078 := (* -1::real #883)
+#1260 := (+ #793 #1078)
+#1262 := (>= #1260 0::real)
+#1269 := (not #1262)
+#1263 := [hypothesis]: #1262
+#1079 := (f8 f20 #20)
+#1093 := (* -1::real #1079)
+#1106 := (+ #883 #1093)
+#1107 := (<= #1106 0::real)
+#1131 := (not #1107)
+#841 := (f8 #86 #20)
+#1094 := (+ #841 #1093)
+#1095 := (>= #1094 0::real)
+#1112 := (or #1095 #1107)
+#1115 := (not #1112)
+#1119 := (or #1118 #1115)
+#1080 := (+ #1079 #1078)
+#1081 := (>= #1080 0::real)
+#1082 := (* -1::real #841)
+#1083 := (+ #1079 #1082)
+#1084 := (<= #1083 0::real)
+#1085 := (or #1084 #1081)
+#1086 := (not #1085)
+#1120 := (or #1118 #1086)
+#1122 := (iff #1120 #1119)
+#1124 := (iff #1119 #1119)
+#1125 := [rewrite]: #1124
+#1116 := (iff #1086 #1115)
+#1113 := (iff #1085 #1112)
+#1110 := (iff #1081 #1107)
+#1100 := (+ #1078 #1079)
+#1103 := (>= #1100 0::real)
+#1108 := (iff #1103 #1107)
+#1109 := [rewrite]: #1108
+#1104 := (iff #1081 #1103)
+#1101 := (= #1080 #1100)
+#1102 := [rewrite]: #1101
+#1105 := [monotonicity #1102]: #1104
+#1111 := [trans #1105 #1109]: #1110
+#1098 := (iff #1084 #1095)
+#1087 := (+ #1082 #1079)
+#1090 := (<= #1087 0::real)
+#1096 := (iff #1090 #1095)
+#1097 := [rewrite]: #1096
+#1091 := (iff #1084 #1090)
+#1088 := (= #1083 #1087)
+#1089 := [rewrite]: #1088
+#1092 := [monotonicity #1089]: #1091
+#1099 := [trans #1092 #1097]: #1098
+#1114 := [monotonicity #1099 #1111]: #1113
+#1117 := [monotonicity #1114]: #1116
+#1123 := [monotonicity #1117]: #1122
+#1126 := [trans #1123 #1125]: #1122
+#1121 := [quant-inst]: #1120
+#1127 := [mp #1121 #1126]: #1119
+#1264 := [unit-resolution #1127 #600]: #1115
+#1132 := (or #1112 #1131)
+#1133 := [def-axiom]: #1132
+#1265 := [unit-resolution #1133 #1264]: #1131
+#1194 := (+ #793 #1093)
+#1195 := (>= #1194 0::real)
+#1225 := (not #1195)
+#934 := (f8 #81 #20)
+#1204 := (+ #934 #1093)
+#1205 := (<= #1204 0::real)
+#1210 := (or #1195 #1205)
+#1213 := (not #1210)
+#1216 := (or #1060 #1213)
+#1191 := (* -1::real #934)
+#1192 := (+ #1079 #1191)
+#1193 := (>= #1192 0::real)
+#1196 := (or #1195 #1193)
+#1197 := (not #1196)
+#1217 := (or #1060 #1197)
+#1219 := (iff #1217 #1216)
+#1221 := (iff #1216 #1216)
+#1222 := [rewrite]: #1221
+#1214 := (iff #1197 #1213)
+#1211 := (iff #1196 #1210)
+#1208 := (iff #1193 #1205)
+#1198 := (+ #1191 #1079)
+#1201 := (>= #1198 0::real)
+#1206 := (iff #1201 #1205)
+#1207 := [rewrite]: #1206
+#1202 := (iff #1193 #1201)
+#1199 := (= #1192 #1198)
+#1200 := [rewrite]: #1199
+#1203 := [monotonicity #1200]: #1202
+#1209 := [trans #1203 #1207]: #1208
+#1212 := [monotonicity #1209]: #1211
+#1215 := [monotonicity #1212]: #1214
+#1220 := [monotonicity #1215]: #1219
+#1223 := [trans #1220 #1222]: #1219
+#1218 := [quant-inst]: #1217
+#1224 := [mp #1218 #1223]: #1216
+#1266 := [unit-resolution #1224 #594]: #1213
+#1226 := (or #1210 #1225)
+#1227 := [def-axiom]: #1226
+#1267 := [unit-resolution #1227 #1266]: #1225
+#1268 := [th-lemma #1267 #1265 #1263]: false
+#1270 := [lemma #1268]: #1269
+#1273 := (or #1272 #1262)
+#1274 := [th-lemma]: #1273
+#1342 := [unit-resolution #1274 #1270]: #1272
+#1364 := [mp #1342 #1363]: #838
+#1366 := (or #809 #794)
+#795 := (f8 f16 #20)
+#814 := (= #793 #795)
+#817 := (ite #809 #814 #794)
+#470 := (= #42 #77)
+#469 := (= #44 #77)
+#471 := (ite #145 #469 #470)
+#562 := (forall (vars (?v0 S2)) (:pat #535 #552 #561 #554) #471)
+#474 := (forall (vars (?v0 S2)) #471)
+#565 := (iff #474 #562)
+#563 := (iff #471 #471)
+#564 := [refl]: #563
+#566 := [quant-intro #564]: #565
+#185 := (ite #145 #44 #42)
+#390 := (= #77 #185)
+#391 := (forall (vars (?v0 S2)) #390)
+#475 := (iff #391 #474)
+#472 := (iff #390 #471)
+#473 := [rewrite]: #472
+#476 := [quant-intro #473]: #475
+#348 := (~ #391 #391)
+#358 := (~ #390 #390)
+#347 := [refl]: #358
+#395 := [nnf-pos #347]: #348
+#49 := (f3 f17 #9)
+#190 := (= #49 #185)
+#193 := (forall (vars (?v0 S2)) #190)
+#392 := (iff #193 #391)
+#393 := [rewrite* #298]: #392
+#50 := (ite #32 #42 #44)
+#51 := (= #49 #50)
+#52 := (forall (vars (?v0 S2)) #51)
+#194 := (iff #52 #193)
+#191 := (iff #51 #190)
+#188 := (= #50 #185)
+#182 := (ite #144 #42 #44)
+#186 := (= #182 #185)
+#187 := [rewrite]: #186
+#183 := (= #50 #182)
+#184 := [monotonicity #149]: #183
+#189 := [trans #184 #187]: #188
+#192 := [monotonicity #189]: #191
+#195 := [quant-intro #192]: #194
+#143 := [asserted]: #52
+#196 := [mp #143 #195]: #193
+#394 := [mp #196 #393]: #391
+#396 := [mp~ #394 #395]: #391
+#477 := [mp #396 #476]: #474
+#567 := [mp #477 #566]: #562
+#628 := (not #562)
+#820 := (or #628 #817)
+#796 := (= #795 #793)
+#798 := (+ #797 #146)
+#799 := (>= #798 0::int)
+#800 := (ite #799 #796 #794)
+#821 := (or #628 #800)
+#823 := (iff #821 #820)
+#825 := (iff #820 #820)
+#826 := [rewrite]: #825
+#818 := (iff #800 #817)
+#815 := (iff #796 #814)
+#816 := [rewrite]: #815
+#812 := (iff #799 #809)
+#801 := (+ #146 #797)
+#804 := (>= #801 0::int)
+#810 := (iff #804 #809)
+#811 := [rewrite]: #810
+#805 := (iff #799 #804)
+#802 := (= #798 #801)
+#803 := [rewrite]: #802
+#806 := [monotonicity #803]: #805
+#813 := [trans #806 #811]: #812
+#819 := [monotonicity #813 #816]: #818
+#824 := [monotonicity #819]: #823
+#827 := [trans #824 #826]: #823
+#822 := [quant-inst]: #821
+#828 := [mp #822 #827]: #820
+#1365 := [unit-resolution #828 #567]: #817
+#829 := (not #817)
+#833 := (or #829 #809 #794)
+#834 := [def-axiom]: #833
+#1367 := [unit-resolution #834 #1365]: #1366
+#1368 := [unit-resolution #1367 #1364]: #809
+#984 := (>= #853 0::int)
+#1369 := (or #1345 #984)
+#1370 := [th-lemma]: #1369
+#1371 := [unit-resolution #1370 #1344]: #984
+#830 := (not #809)
+#1372 := (not #984)
+#1373 := (or #1288 #1372 #830)
+#1374 := [th-lemma]: #1373
+#1375 := [unit-resolution #1374 #1371 #1368]: #1288
+#1377 := (not #1288)
+#1378 := (or #1285 #1376 #1377)
+#1379 := [th-lemma]: #1378
+#1381 := [unit-resolution #1379 #1375]: #1380
+#1382 := [unit-resolution #1381 #1315]: #1376
+#982 := (>= #616 0::int)
+#1383 := (or #1318 #982)
+#1384 := [th-lemma]: #1383
+#1385 := [unit-resolution #1384 #1297]: #982
+[th-lemma #1385 #1382 #1341]: false
+unsat
+85264eb8e7f8e85b6d7ee44a562fd15da499cae2 208 0
+#2 := false
+#37 := 0::real
+decl f13 :: (-> S6 S7 real)
+decl f17 :: S7
+#32 := f17
+decl f18 :: S6
+#34 := f18
+#35 := (f13 f18 f17)
+decl f14 :: (-> S8 S9 S6)
+decl f16 :: S9
+#30 := f16
+decl f15 :: (-> S2 S8)
+decl f5 :: S2
+#11 := f5
+#29 := (f15 f5)
+#31 := (f14 #29 f16)
+#33 := (f13 #31 f17)
+#96 := -1::real
+#107 := (* -1::real #33)
+#108 := (+ #107 #35)
+#97 := (* -1::real #35)
+#98 := (+ #33 #97)
+#135 := (>= #98 0::real)
+#142 := (ite #135 #98 #108)
+#150 := (* -1::real #142)
+#383 := (+ #108 #150)
+#384 := (<= #383 0::real)
+#369 := (= #108 #142)
+#136 := (not #135)
+decl f3 :: S2
+#8 := f3
+#47 := (f15 f3)
+#48 := (f14 #47 f16)
+#49 := (f13 #48 f17)
+#172 := (* -1::real #49)
+decl f19 :: S6
+#41 := f19
+#42 := (f13 f19 f17)
+#173 := (+ #42 #172)
+#116 := (* -1::real #42)
+#163 := (+ #116 #49)
+#184 := (<= #173 0::real)
+#191 := (ite #184 #163 #173)
+#199 := (* -1::real #191)
+#382 := (+ #173 #199)
+#385 := (<= #382 0::real)
+#375 := (= #173 #191)
+#185 := (not #184)
+#386 := [hypothesis]: #184
+#394 := (or #136 #185)
+#125 := -1/3::real
+#126 := (* -1/3::real #42)
+#200 := (+ #126 #199)
+#123 := 1/3::real
+#124 := (* 1/3::real #35)
+#201 := (+ #124 #200)
+#202 := (<= #201 0::real)
+#203 := (not #202)
+#44 := 3::real
+#43 := (- #35 #42)
+#45 := (/ #43 3::real)
+#50 := (- #49 #42)
+#52 := (- #50)
+#51 := (< #50 0::real)
+#53 := (ite #51 #52 #50)
+#54 := (< #53 #45)
+#208 := (iff #54 #203)
+#127 := (+ #124 #126)
+#166 := (< #163 0::real)
+#178 := (ite #166 #173 #163)
+#181 := (< #178 #127)
+#206 := (iff #181 #203)
+#196 := (< #191 #127)
+#204 := (iff #196 #203)
+#205 := [rewrite]: #204
+#197 := (iff #181 #196)
+#194 := (= #178 #191)
+#188 := (ite #185 #173 #163)
+#192 := (= #188 #191)
+#193 := [rewrite]: #192
+#189 := (= #178 #188)
+#186 := (iff #166 #185)
+#187 := [rewrite]: #186
+#190 := [monotonicity #187]: #189
+#195 := [trans #190 #193]: #194
+#198 := [monotonicity #195]: #197
+#207 := [trans #198 #205]: #206
+#182 := (iff #54 #181)
+#130 := (= #45 #127)
+#117 := (+ #35 #116)
+#120 := (/ #117 3::real)
+#128 := (= #120 #127)
+#129 := [rewrite]: #128
+#121 := (= #45 #120)
+#118 := (= #43 #117)
+#119 := [rewrite]: #118
+#122 := [monotonicity #119]: #121
+#131 := [trans #122 #129]: #130
+#179 := (= #53 #178)
+#164 := (= #50 #163)
+#165 := [rewrite]: #164
+#176 := (= #52 #173)
+#169 := (- #163)
+#174 := (= #169 #173)
+#175 := [rewrite]: #174
+#170 := (= #52 #169)
+#171 := [monotonicity #165]: #170
+#177 := [trans #171 #175]: #176
+#167 := (iff #51 #166)
+#168 := [monotonicity #165]: #167
+#180 := [monotonicity #168 #177 #165]: #179
+#183 := [monotonicity #180 #131]: #182
+#209 := [trans #183 #207]: #208
+#162 := [asserted]: #54
+#210 := [mp #162 #209]: #203
+#380 := (+ #163 #199)
+#381 := (<= #380 0::real)
+#374 := (= #163 #191)
+#376 := (or #185 #374)
+#377 := [def-axiom]: #376
+#387 := [unit-resolution #377 #386]: #374
+#388 := (not #374)
+#389 := (or #388 #381)
+#390 := [th-lemma]: #389
+#391 := [unit-resolution #390 #387]: #381
+#392 := [hypothesis]: #135
+#214 := (+ #33 #172)
+#215 := (<= #214 0::real)
+#55 := (<= #33 #49)
+#216 := (iff #55 #215)
+#217 := [rewrite]: #216
+#211 := [asserted]: #55
+#218 := [mp #211 #217]: #215
+#393 := [th-lemma #218 #392 #391 #210 #386]: false
+#395 := [lemma #393]: #394
+#396 := [unit-resolution #395 #386]: #136
+#151 := (+ #126 #150)
+#152 := (+ #124 #151)
+#153 := (<= #152 0::real)
+#154 := (not #153)
+#36 := (- #33 #35)
+#39 := (- #36)
+#38 := (< #36 0::real)
+#40 := (ite #38 #39 #36)
+#46 := (< #40 #45)
+#159 := (iff #46 #154)
+#101 := (< #98 0::real)
+#113 := (ite #101 #108 #98)
+#132 := (< #113 #127)
+#157 := (iff #132 #154)
+#147 := (< #142 #127)
+#155 := (iff #147 #154)
+#156 := [rewrite]: #155
+#148 := (iff #132 #147)
+#145 := (= #113 #142)
+#139 := (ite #136 #108 #98)
+#143 := (= #139 #142)
+#144 := [rewrite]: #143
+#140 := (= #113 #139)
+#137 := (iff #101 #136)
+#138 := [rewrite]: #137
+#141 := [monotonicity #138]: #140
+#146 := [trans #141 #144]: #145
+#149 := [monotonicity #146]: #148
+#158 := [trans #149 #156]: #157
+#133 := (iff #46 #132)
+#114 := (= #40 #113)
+#99 := (= #36 #98)
+#100 := [rewrite]: #99
+#111 := (= #39 #108)
+#104 := (- #98)
+#109 := (= #104 #108)
+#110 := [rewrite]: #109
+#105 := (= #39 #104)
+#106 := [monotonicity #100]: #105
+#112 := [trans #106 #110]: #111
+#102 := (iff #38 #101)
+#103 := [monotonicity #100]: #102
+#115 := [monotonicity #103 #112 #100]: #114
+#134 := [monotonicity #115 #131]: #133
+#160 := [trans #134 #158]: #159
+#95 := [asserted]: #46
+#161 := [mp #95 #160]: #154
+#372 := (or #135 #369)
+#373 := [def-axiom]: #372
+#397 := [unit-resolution #373 #396]: #369
+#398 := (not #369)
+#399 := (or #398 #384)
+#400 := [th-lemma]: #399
+#401 := [unit-resolution #400 #397]: #384
+#402 := [th-lemma #401 #161 #391 #210 #218 #396]: false
+#403 := [lemma #402]: #185
+#378 := (or #184 #375)
+#379 := [def-axiom]: #378
+#406 := [unit-resolution #379 #403]: #375
+#407 := (not #375)
+#408 := (or #407 #385)
+#409 := [th-lemma]: #408
+#410 := [unit-resolution #409 #406]: #385
+#412 := (not #215)
+#411 := (not #385)
+#413 := (or #136 #411 #412 #202 #184)
+#414 := [th-lemma]: #413
+#415 := [unit-resolution #414 #403 #210 #218 #410]: #136
+#416 := [unit-resolution #373 #415]: #369
+#417 := [unit-resolution #400 #416]: #384
+[th-lemma #410 #218 #210 #403 #161 #417]: false
+unsat
+93a49e3235fe928f7c40274d2cb077bbf82de367 333 0
+#2 := false
+#11 := 0::real
+decl ?v2!1 :: real
+#225 := ?v2!1
+decl ?v1!2 :: real
+#223 := ?v1!2
+#45 := -1::real
+#238 := (* -1::real ?v1!2)
+#260 := (+ #238 ?v2!1)
+#240 := (* -1::real ?v2!1)
+#266 := (+ ?v1!2 #240)
+#267 := (>= #266 0::real)
+#274 := (ite #267 #266 #260)
+#277 := (* -1::real #274)
+#74 := -1/3::real
+#233 := (* -1/3::real ?v2!1)
+#280 := (+ #233 #277)
+decl ?v3!0 :: real
+#224 := ?v3!0
+#72 := 1/3::real
+#235 := (* 1/3::real ?v3!0)
+#283 := (+ #235 #280)
+#286 := (<= #283 0::real)
+#302 := (not #286)
+decl ?v0!3 :: real
+#221 := ?v0!3
+#248 := (+ ?v0!3 #238)
+#249 := (<= #248 0::real)
+#250 := (not #249)
+#226 := (* -1::real ?v0!3)
+#227 := (+ #226 ?v3!0)
+#228 := (* -1::real ?v3!0)
+#229 := (+ ?v0!3 #228)
+#230 := (>= #229 0::real)
+#231 := (ite #230 #229 #227)
+#232 := (* -1::real #231)
+#234 := (+ #233 #232)
+#236 := (+ #235 #234)
+#237 := (<= #236 0::real)
+#292 := (or #237 #250 #286)
+#297 := (not #292)
+#239 := (+ ?v2!1 #238)
+#241 := (+ #240 ?v1!2)
+#242 := (<= #239 0::real)
+#243 := (ite #242 #241 #239)
+#244 := (* -1::real #243)
+#245 := (+ #233 #244)
+#246 := (+ #235 #245)
+#247 := (<= #246 0::real)
+#251 := (or #250 #247 #237)
+#252 := (not #251)
+#298 := (iff #252 #297)
+#295 := (iff #251 #292)
+#289 := (or #250 #286 #237)
+#293 := (iff #289 #292)
+#294 := [rewrite]: #293
+#290 := (iff #251 #289)
+#287 := (iff #247 #286)
+#284 := (= #246 #283)
+#281 := (= #245 #280)
+#278 := (= #244 #277)
+#275 := (= #243 #274)
+#261 := (= #239 #260)
+#262 := [rewrite]: #261
+#272 := (= #241 #266)
+#273 := [rewrite]: #272
+#270 := (iff #242 #267)
+#263 := (<= #260 0::real)
+#268 := (iff #263 #267)
+#269 := [rewrite]: #268
+#264 := (iff #242 #263)
+#265 := [monotonicity #262]: #264
+#271 := [trans #265 #269]: #270
+#276 := [monotonicity #271 #273 #262]: #275
+#279 := [monotonicity #276]: #278
+#282 := [monotonicity #279]: #281
+#285 := [monotonicity #282]: #284
+#288 := [monotonicity #285]: #287
+#291 := [monotonicity #288]: #290
+#296 := [trans #291 #294]: #295
+#299 := [monotonicity #296]: #298
+#9 := (:var 0 real)
+#8 := (:var 3 real)
+#56 := (* -1::real #8)
+#57 := (+ #56 #9)
+#46 := (* -1::real #9)
+#47 := (+ #8 #46)
+#170 := (>= #47 0::real)
+#177 := (ite #170 #47 #57)
+#185 := (* -1::real #177)
+#15 := (:var 1 real)
+#75 := (* -1/3::real #15)
+#186 := (+ #75 #185)
+#73 := (* 1/3::real #9)
+#187 := (+ #73 #186)
+#188 := (<= #187 0::real)
+#20 := (:var 2 real)
+#93 := (* -1::real #20)
+#94 := (+ #15 #93)
+#65 := (* -1::real #15)
+#84 := (+ #65 #20)
+#139 := (<= #94 0::real)
+#146 := (ite #139 #84 #94)
+#154 := (* -1::real #146)
+#155 := (+ #75 #154)
+#156 := (+ #73 #155)
+#157 := (<= #156 0::real)
+#132 := (+ #8 #93)
+#133 := (<= #132 0::real)
+#136 := (not #133)
+#207 := (or #136 #157 #188)
+#212 := (forall (vars (?v0 real) (?v1 real) (?v2 real) (?v3 real)) #207)
+#215 := (not #212)
+#253 := (~ #215 #252)
+#254 := [sk]: #253
+#26 := (<= #8 #20)
+#27 := (implies #26 false)
+#17 := 3::real
+#16 := (- #9 #15)
+#18 := (/ #16 3::real)
+#21 := (- #20 #15)
+#23 := (- #21)
+#22 := (< #21 0::real)
+#24 := (ite #22 #23 #21)
+#25 := (< #24 #18)
+#28 := (implies #25 #27)
+#10 := (- #8 #9)
+#13 := (- #10)
+#12 := (< #10 0::real)
+#14 := (ite #12 #13 #10)
+#19 := (< #14 #18)
+#29 := (implies #19 #28)
+#30 := (forall (vars (?v0 real) (?v1 real) (?v2 real) (?v3 real)) #29)
+#31 := (not #30)
+#218 := (iff #31 #215)
+#76 := (+ #73 #75)
+#87 := (< #84 0::real)
+#99 := (ite #87 #94 #84)
+#102 := (< #99 #76)
+#111 := (not #102)
+#105 := (not #26)
+#112 := (or #105 #111)
+#50 := (< #47 0::real)
+#62 := (ite #50 #57 #47)
+#81 := (< #62 #76)
+#120 := (not #81)
+#121 := (or #120 #112)
+#126 := (forall (vars (?v0 real) (?v1 real) (?v2 real) (?v3 real)) #121)
+#129 := (not #126)
+#216 := (iff #129 #215)
+#213 := (iff #126 #212)
+#210 := (iff #121 #207)
+#201 := (or #136 #157)
+#204 := (or #188 #201)
+#208 := (iff #204 #207)
+#209 := [rewrite]: #208
+#205 := (iff #121 #204)
+#202 := (iff #112 #201)
+#168 := (iff #111 #157)
+#158 := (not #157)
+#163 := (not #158)
+#166 := (iff #163 #157)
+#167 := [rewrite]: #166
+#164 := (iff #111 #163)
+#161 := (iff #102 #158)
+#151 := (< #146 #76)
+#159 := (iff #151 #158)
+#160 := [rewrite]: #159
+#152 := (iff #102 #151)
+#149 := (= #99 #146)
+#140 := (not #139)
+#143 := (ite #140 #94 #84)
+#147 := (= #143 #146)
+#148 := [rewrite]: #147
+#144 := (= #99 #143)
+#141 := (iff #87 #140)
+#142 := [rewrite]: #141
+#145 := [monotonicity #142]: #144
+#150 := [trans #145 #148]: #149
+#153 := [monotonicity #150]: #152
+#162 := [trans #153 #160]: #161
+#165 := [monotonicity #162]: #164
+#169 := [trans #165 #167]: #168
+#137 := (iff #105 #136)
+#134 := (iff #26 #133)
+#135 := [rewrite]: #134
+#138 := [monotonicity #135]: #137
+#203 := [monotonicity #138 #169]: #202
+#199 := (iff #120 #188)
+#189 := (not #188)
+#194 := (not #189)
+#197 := (iff #194 #188)
+#198 := [rewrite]: #197
+#195 := (iff #120 #194)
+#192 := (iff #81 #189)
+#182 := (< #177 #76)
+#190 := (iff #182 #189)
+#191 := [rewrite]: #190
+#183 := (iff #81 #182)
+#180 := (= #62 #177)
+#171 := (not #170)
+#174 := (ite #171 #57 #47)
+#178 := (= #174 #177)
+#179 := [rewrite]: #178
+#175 := (= #62 #174)
+#172 := (iff #50 #171)
+#173 := [rewrite]: #172
+#176 := [monotonicity #173]: #175
+#181 := [trans #176 #179]: #180
+#184 := [monotonicity #181]: #183
+#193 := [trans #184 #191]: #192
+#196 := [monotonicity #193]: #195
+#200 := [trans #196 #198]: #199
+#206 := [monotonicity #200 #203]: #205
+#211 := [trans #206 #209]: #210
+#214 := [quant-intro #211]: #213
+#217 := [monotonicity #214]: #216
+#130 := (iff #31 #129)
+#127 := (iff #30 #126)
+#124 := (iff #29 #121)
+#117 := (implies #81 #112)
+#122 := (iff #117 #121)
+#123 := [rewrite]: #122
+#118 := (iff #29 #117)
+#115 := (iff #28 #112)
+#108 := (implies #102 #105)
+#113 := (iff #108 #112)
+#114 := [rewrite]: #113
+#109 := (iff #28 #108)
+#106 := (iff #27 #105)
+#107 := [rewrite]: #106
+#103 := (iff #25 #102)
+#79 := (= #18 #76)
+#66 := (+ #9 #65)
+#69 := (/ #66 3::real)
+#77 := (= #69 #76)
+#78 := [rewrite]: #77
+#70 := (= #18 #69)
+#67 := (= #16 #66)
+#68 := [rewrite]: #67
+#71 := [monotonicity #68]: #70
+#80 := [trans #71 #78]: #79
+#100 := (= #24 #99)
+#85 := (= #21 #84)
+#86 := [rewrite]: #85
+#97 := (= #23 #94)
+#90 := (- #84)
+#95 := (= #90 #94)
+#96 := [rewrite]: #95
+#91 := (= #23 #90)
+#92 := [monotonicity #86]: #91
+#98 := [trans #92 #96]: #97
+#88 := (iff #22 #87)
+#89 := [monotonicity #86]: #88
+#101 := [monotonicity #89 #98 #86]: #100
+#104 := [monotonicity #101 #80]: #103
+#110 := [monotonicity #104 #107]: #109
+#116 := [trans #110 #114]: #115
+#82 := (iff #19 #81)
+#63 := (= #14 #62)
+#48 := (= #10 #47)
+#49 := [rewrite]: #48
+#60 := (= #13 #57)
+#53 := (- #47)
+#58 := (= #53 #57)
+#59 := [rewrite]: #58
+#54 := (= #13 #53)
+#55 := [monotonicity #49]: #54
+#61 := [trans #55 #59]: #60
+#51 := (iff #12 #50)
+#52 := [monotonicity #49]: #51
+#64 := [monotonicity #52 #61 #49]: #63
+#83 := [monotonicity #64 #80]: #82
+#119 := [monotonicity #83 #116]: #118
+#125 := [trans #119 #123]: #124
+#128 := [quant-intro #125]: #127
+#131 := [monotonicity #128]: #130
+#219 := [trans #131 #217]: #218
+#44 := [asserted]: #31
+#220 := [mp #44 #219]: #215
+#257 := [mp~ #220 #254]: #252
+#258 := [mp #257 #299]: #297
+#303 := [not-or-elim #258]: #302
+#301 := [not-or-elim #258]: #249
+#259 := (not #237)
+#300 := [not-or-elim #258]: #259
+#376 := (+ #227 #232)
+#377 := (<= #376 0::real)
+#360 := (= #227 #231)
+#361 := (not #230)
+#368 := (not #267)
+#379 := [hypothesis]: #368
+#387 := (or #361 #267)
+#373 := (+ #260 #277)
+#374 := (<= #373 0::real)
+#367 := (= #260 #274)
+#371 := (or #267 #367)
+#372 := [def-axiom]: #371
+#380 := [unit-resolution #372 #379]: #367
+#381 := (not #367)
+#382 := (or #381 #374)
+#383 := [th-lemma]: #382
+#384 := [unit-resolution #383 #380]: #374
+#385 := [hypothesis]: #230
+#386 := [th-lemma #385 #384 #303 #379 #301]: false
+#388 := [lemma #386]: #387
+#389 := [unit-resolution #388 #379]: #361
+#364 := (or #230 #360)
+#365 := [def-axiom]: #364
+#390 := [unit-resolution #365 #389]: #360
+#391 := (not #360)
+#392 := (or #391 #377)
+#393 := [th-lemma]: #392
+#394 := [unit-resolution #393 #390]: #377
+#395 := [th-lemma #384 #303 #379 #394 #300 #301]: false
+#396 := [lemma #395]: #267
+#399 := [hypothesis]: #361
+#400 := [unit-resolution #365 #399]: #360
+#401 := [unit-resolution #393 #400]: #377
+#375 := (+ #266 #277)
+#378 := (<= #375 0::real)
+#366 := (= #266 #274)
+#369 := (or #368 #366)
+#370 := [def-axiom]: #369
+#402 := [unit-resolution #370 #396]: #366
+#403 := (not #366)
+#404 := (or #403 #378)
+#405 := [th-lemma]: #404
+#406 := [unit-resolution #405 #402]: #378
+#407 := [th-lemma #406 #301 #401 #300 #399 #303]: false
+#408 := [lemma #407]: #230
+[th-lemma #406 #301 #408 #396 #303]: false
+unsat
+869cff425b5458015114ab900e59f8623c03a78b 165 0
+#2 := false
+#22 := 0::real
+decl f3 :: (-> S3 S2 real)
+decl ?v0!0 :: S2
+#118 := ?v0!0
+decl f5 :: S3
+#11 := f5
+#119 := (f3 f5 ?v0!0)
+#49 := -1::real
+#117 := (* -1::real #119)
+decl f4 :: S3
+#8 := f4
+#115 := (f3 f4 ?v0!0)
+#120 := (+ #115 #117)
+#121 := (>= #120 0::real)
+decl f6 :: (-> S2 S4 S1)
+decl f7 :: (-> S4 S4 S4)
+decl f9 :: (-> S2 S4 S4)
+decl f11 :: S4
+#17 := f11
+decl f10 :: S2
+#16 := f10
+#18 := (f9 f10 f11)
+decl f8 :: S4
+#15 := f8
+#19 := (f7 f8 #18)
+#123 := (f6 ?v0!0 #19)
+decl f1 :: S1
+#4 := f1
+#124 := (= f1 #123)
+#9 := (:var 0 S2)
+#12 := (f3 f5 #9)
+#81 := (* -1::real #12)
+#10 := (f3 f4 #9)
+#82 := (+ #10 #81)
+#83 := (>= #82 0::real)
+#84 := (not #83)
+#89 := (forall (vars (?v1 S2)) #84)
+#158 := (and #89 #121 #124)
+#122 := (not #121)
+#133 := (not #122)
+#125 := (not #124)
+#130 := (not #125)
+#143 := (and #130 #133 #89)
+#161 := (iff #143 #158)
+#155 := (and #124 #121 #89)
+#159 := (iff #155 #158)
+#160 := [rewrite]: #159
+#156 := (iff #143 #155)
+#153 := (iff #133 #121)
+#154 := [rewrite]: #153
+#151 := (iff #130 #124)
+#152 := [rewrite]: #151
+#157 := [monotonicity #152 #154]: #156
+#162 := [trans #157 #160]: #161
+#92 := (not #89)
+#20 := (f6 #9 #19)
+#46 := (= f1 #20)
+#60 := (not #46)
+#101 := (or #60 #84 #92)
+#106 := (forall (vars (?v0 S2)) #101)
+#109 := (not #106)
+#146 := (~ #109 #143)
+#126 := (or #125 #122 #92)
+#127 := (not #126)
+#144 := (~ #127 #143)
+#140 := (not #92)
+#141 := (~ #140 #89)
+#138 := (~ #89 #89)
+#136 := (~ #84 #84)
+#137 := [refl]: #136
+#139 := [nnf-pos #137]: #138
+#142 := [nnf-neg #139]: #141
+#134 := (~ #133 #133)
+#135 := [refl]: #134
+#131 := (~ #130 #130)
+#132 := [refl]: #131
+#145 := [nnf-neg #132 #135 #142]: #144
+#128 := (~ #109 #127)
+#129 := [sk]: #128
+#147 := [trans #129 #145]: #146
+#23 := (- #12 #10)
+#24 := (< 0::real #23)
+#21 := (= #20 f1)
+#25 := (implies #21 #24)
+#13 := (< #10 #12)
+#14 := (forall (vars (?v1 S2)) #13)
+#26 := (implies #14 #25)
+#27 := (forall (vars (?v0 S2)) #26)
+#28 := (not #27)
+#112 := (iff #28 #109)
+#50 := (* -1::real #10)
+#51 := (+ #50 #12)
+#54 := (< 0::real #51)
+#61 := (or #60 #54)
+#69 := (not #14)
+#70 := (or #69 #61)
+#75 := (forall (vars (?v0 S2)) #70)
+#78 := (not #75)
+#110 := (iff #78 #109)
+#107 := (iff #75 #106)
+#104 := (iff #70 #101)
+#95 := (or #60 #84)
+#98 := (or #92 #95)
+#102 := (iff #98 #101)
+#103 := [rewrite]: #102
+#99 := (iff #70 #98)
+#96 := (iff #61 #95)
+#85 := (iff #54 #84)
+#86 := [rewrite]: #85
+#97 := [monotonicity #86]: #96
+#93 := (iff #69 #92)
+#90 := (iff #14 #89)
+#87 := (iff #13 #84)
+#88 := [rewrite]: #87
+#91 := [quant-intro #88]: #90
+#94 := [monotonicity #91]: #93
+#100 := [monotonicity #94 #97]: #99
+#105 := [trans #100 #103]: #104
+#108 := [quant-intro #105]: #107
+#111 := [monotonicity #108]: #110
+#79 := (iff #28 #78)
+#76 := (iff #27 #75)
+#73 := (iff #26 #70)
+#66 := (implies #14 #61)
+#71 := (iff #66 #70)
+#72 := [rewrite]: #71
+#67 := (iff #26 #66)
+#64 := (iff #25 #61)
+#57 := (implies #46 #54)
+#62 := (iff #57 #61)
+#63 := [rewrite]: #62
+#58 := (iff #25 #57)
+#55 := (iff #24 #54)
+#52 := (= #23 #51)
+#53 := [rewrite]: #52
+#56 := [monotonicity #53]: #55
+#47 := (iff #21 #46)
+#48 := [rewrite]: #47
+#59 := [monotonicity #48 #56]: #58
+#65 := [trans #59 #63]: #64
+#68 := [monotonicity #65]: #67
+#74 := [trans #68 #72]: #73
+#77 := [quant-intro #74]: #76
+#80 := [monotonicity #77]: #79
+#113 := [trans #80 #111]: #112
+#45 := [asserted]: #28
+#114 := [mp #45 #113]: #109
+#148 := [mp~ #114 #147]: #143
+#149 := [mp #148 #162]: #158
+#163 := [and-elim #149]: #121
+#223 := (pattern #12)
+#222 := (pattern #10)
+#224 := (forall (vars (?v1 S2)) (:pat #222 #223) #84)
+#227 := (iff #89 #224)
+#225 := (iff #84 #84)
+#226 := [refl]: #225
+#228 := [quant-intro #226]: #227
+#150 := [and-elim #149]: #89
+#229 := [mp #150 #228]: #224
+#232 := (not #224)
+#233 := (or #232 #122)
+#234 := [quant-inst]: #233
+[unit-resolution #234 #229 #163]: false
+unsat
+2d6fbb869d4e1460704d418830e5da7d2659f315 57 0
+#2 := false
+decl f13 :: (-> S4 S4 S5)
+#44 := (:var 0 S4)
+#43 := (:var 1 S4)
+#45 := (f13 #43 #44)
+#252 := (pattern #45)
+#39 := 0::real
+decl f12 :: (-> S5 real)
+#46 := (f12 #45)
+#133 := (>= #46 0::real)
+#253 := (forall (vars (?v0 S4) (?v1 S4)) (:pat #252) #133)
+#135 := (forall (vars (?v0 S4) (?v1 S4)) #133)
+#256 := (iff #135 #253)
+#254 := (iff #133 #133)
+#255 := [refl]: #254
+#257 := [quant-intro #255]: #256
+#150 := (~ #135 #135)
+#139 := (~ #133 #133)
+#130 := [refl]: #139
+#151 := [nnf-pos #130]: #150
+#47 := (<= 0::real #46)
+#48 := (forall (vars (?v0 S4) (?v1 S4)) #47)
+#136 := (iff #48 #135)
+#132 := (iff #47 #133)
+#134 := [rewrite]: #132
+#137 := [quant-intro #134]: #136
+#129 := [asserted]: #48
+#138 := [mp #129 #137]: #135
+#152 := [mp~ #138 #151]: #135
+#258 := [mp #152 #257]: #253
+decl f14 :: (-> S3 S4)
+decl f4 :: S3
+#8 := f4
+#36 := (f14 f4)
+decl f10 :: S3
+#24 := f10
+#35 := (f14 f10)
+#37 := (f13 #35 #36)
+#38 := (f12 #37)
+#259 := (>= #38 0::real)
+#261 := (not #259)
+#41 := (= #38 0::real)
+#42 := (not #41)
+#128 := [asserted]: #42
+#267 := (or #41 #261)
+#40 := (<= #38 0::real)
+#127 := [asserted]: #40
+#260 := (not #40)
+#265 := (or #41 #260 #261)
+#266 := [th-lemma]: #265
+#268 := [unit-resolution #266 #127]: #267
+#269 := [unit-resolution #268 #128]: #261
+#262 := (not #253)
+#263 := (or #262 #259)
+#264 := [quant-inst]: #263
+[unit-resolution #264 #269 #258]: false
+unsat
+c9590f4753c4b6ca0ef0d09a97231631684bbcc1 91 0
+#2 := false
+#43 := 0::real
+decl f3 :: (-> S2 S3 real)
+decl f5 :: S3
+#9 := f5
+decl f6 :: S2
+#11 := f6
+#12 := (f3 f6 f5)
+#40 := -1::real
+#41 := (* -1::real #12)
+decl f4 :: S2
+#8 := f4
+#10 := (f3 f4 f5)
+#42 := (+ #10 #41)
+#135 := (>= #42 0::real)
+#160 := (not #135)
+#48 := (= #10 #12)
+#60 := (not #48)
+#19 := (= #12 #10)
+#20 := (not #19)
+#61 := (iff #20 #60)
+#58 := (iff #19 #48)
+#59 := [rewrite]: #58
+#62 := [monotonicity #59]: #61
+#39 := [asserted]: #20
+#65 := [mp #39 #62]: #60
+#163 := (or #48 #160)
+#44 := (<= #42 0::real)
+#13 := (<= #10 #12)
+#45 := (iff #13 #44)
+#46 := [rewrite]: #45
+#37 := [asserted]: #13
+#47 := [mp #37 #46]: #44
+#159 := (not #44)
+#161 := (or #48 #159 #160)
+#162 := [th-lemma]: #161
+#164 := [unit-resolution #162 #47]: #163
+#165 := [unit-resolution #164 #65]: #160
+#14 := (:var 0 S3)
+#16 := (f3 f4 #14)
+#128 := (pattern #16)
+#15 := (f3 f6 #14)
+#127 := (pattern #15)
+#49 := (* -1::real #16)
+#50 := (+ #15 #49)
+#51 := (<= #50 0::real)
+#129 := (forall (vars (?v0 S3)) (:pat #127 #128) #51)
+#54 := (forall (vars (?v0 S3)) #51)
+#132 := (iff #54 #129)
+#130 := (iff #51 #51)
+#131 := [refl]: #130
+#133 := [quant-intro #131]: #132
+#69 := (~ #54 #54)
+#71 := (~ #51 #51)
+#72 := [refl]: #71
+#70 := [nnf-pos #72]: #69
+#17 := (<= #15 #16)
+#18 := (forall (vars (?v0 S3)) #17)
+#55 := (iff #18 #54)
+#52 := (iff #17 #51)
+#53 := [rewrite]: #52
+#56 := [quant-intro #53]: #55
+#38 := [asserted]: #18
+#57 := [mp #38 #56]: #54
+#67 := [mp~ #57 #70]: #54
+#134 := [mp #67 #133]: #129
+#149 := (not #129)
+#150 := (or #149 #135)
+#136 := (* -1::real #10)
+#137 := (+ #12 #136)
+#138 := (<= #137 0::real)
+#151 := (or #149 #138)
+#153 := (iff #151 #150)
+#155 := (iff #150 #150)
+#156 := [rewrite]: #155
+#147 := (iff #138 #135)
+#139 := (+ #136 #12)
+#142 := (<= #139 0::real)
+#145 := (iff #142 #135)
+#146 := [rewrite]: #145
+#143 := (iff #138 #142)
+#140 := (= #137 #139)
+#141 := [rewrite]: #140
+#144 := [monotonicity #141]: #143
+#148 := [trans #144 #146]: #147
+#154 := [monotonicity #148]: #153
+#157 := [trans #154 #156]: #153
+#152 := [quant-inst]: #151
+#158 := [mp #152 #157]: #150
+[unit-resolution #158 #134 #165]: false
+unsat
+827be21ccd16905d74e993b95541879c4d3dbf92 271 0
+#2 := false
+#8 := 0::real
+decl f4 :: (-> S3 S2 real)
+decl f7 :: S2
+#19 := f7
+decl f5 :: S3
+#11 := f5
+#24 := (f4 f5 f7)
+decl f8 :: S3
+#21 := f8
+#22 := (f4 f8 f7)
+#66 := -1::real
+#87 := (* -1::real #22)
+#88 := (+ #87 #24)
+decl f3 :: real
+#9 := f3
+#148 := (* -1::real #24)
+#149 := (+ #22 #148)
+#150 := (+ f3 #149)
+#151 := (<= #150 0::real)
+#154 := (ite #151 f3 #88)
+#320 := (* -1::real #154)
+#321 := (+ f3 #320)
+#322 := (<= #321 0::real)
+#329 := (not #322)
+#65 := 1/2::real
+#157 := (* 1/2::real #154)
+#289 := (<= #157 0::real)
+#168 := (= #157 0::real)
+#178 := (<= #149 0::real)
+decl f6 :: S3
+#14 := f6
+#20 := (f4 f6 f7)
+#174 := (+ #20 #87)
+#175 := (<= #174 0::real)
+#181 := (and #175 #178)
+#184 := (not #181)
+#171 := (not #168)
+#80 := (* 1/2::real #24)
+#145 := (+ #87 #80)
+#79 := (* 1/2::real #20)
+#146 := (+ #79 #145)
+#143 := (>= #146 0::real)
+#141 := (not #143)
+#193 := (or #141 #171 #184)
+#198 := (not #193)
+#28 := 2::real
+#31 := (- #24 #22)
+#32 := (<= f3 #31)
+#33 := (ite #32 f3 #31)
+#34 := (/ #33 2::real)
+#35 := (+ #22 #34)
+#36 := (= #35 #22)
+#37 := (not #36)
+#27 := (+ #20 #24)
+#29 := (/ #27 2::real)
+#30 := (<= #22 #29)
+#38 := (implies #30 #37)
+#25 := (<= #22 #24)
+#23 := (<= #20 #22)
+#26 := (and #23 #25)
+#39 := (implies #26 #38)
+#40 := (not #39)
+#201 := (iff #40 #198)
+#91 := (<= f3 #88)
+#94 := (ite #91 f3 #88)
+#100 := (* 1/2::real #94)
+#105 := (+ #22 #100)
+#111 := (= #22 #105)
+#116 := (not #111)
+#81 := (+ #79 #80)
+#84 := (<= #22 #81)
+#122 := (not #84)
+#123 := (or #122 #116)
+#131 := (not #26)
+#132 := (or #131 #123)
+#137 := (not #132)
+#199 := (iff #137 #198)
+#196 := (iff #132 #193)
+#187 := (or #141 #171)
+#190 := (or #184 #187)
+#194 := (iff #190 #193)
+#195 := [rewrite]: #194
+#191 := (iff #132 #190)
+#188 := (iff #123 #187)
+#172 := (iff #116 #171)
+#169 := (iff #111 #168)
+#160 := (+ #22 #157)
+#163 := (= #22 #160)
+#166 := (iff #163 #168)
+#167 := [rewrite]: #166
+#164 := (iff #111 #163)
+#161 := (= #105 #160)
+#158 := (= #100 #157)
+#155 := (= #94 #154)
+#152 := (iff #91 #151)
+#153 := [rewrite]: #152
+#156 := [monotonicity #153]: #155
+#159 := [monotonicity #156]: #158
+#162 := [monotonicity #159]: #161
+#165 := [monotonicity #162]: #164
+#170 := [trans #165 #167]: #169
+#173 := [monotonicity #170]: #172
+#144 := (iff #122 #141)
+#140 := (iff #84 #143)
+#142 := [rewrite]: #140
+#147 := [monotonicity #142]: #144
+#189 := [monotonicity #147 #173]: #188
+#185 := (iff #131 #184)
+#182 := (iff #26 #181)
+#179 := (iff #25 #178)
+#180 := [rewrite]: #179
+#176 := (iff #23 #175)
+#177 := [rewrite]: #176
+#183 := [monotonicity #177 #180]: #182
+#186 := [monotonicity #183]: #185
+#192 := [monotonicity #186 #189]: #191
+#197 := [trans #192 #195]: #196
+#200 := [monotonicity #197]: #199
+#138 := (iff #40 #137)
+#135 := (iff #39 #132)
+#128 := (implies #26 #123)
+#133 := (iff #128 #132)
+#134 := [rewrite]: #133
+#129 := (iff #39 #128)
+#126 := (iff #38 #123)
+#119 := (implies #84 #116)
+#124 := (iff #119 #123)
+#125 := [rewrite]: #124
+#120 := (iff #38 #119)
+#117 := (iff #37 #116)
+#114 := (iff #36 #111)
+#108 := (= #105 #22)
+#112 := (iff #108 #111)
+#113 := [rewrite]: #112
+#109 := (iff #36 #108)
+#106 := (= #35 #105)
+#103 := (= #34 #100)
+#97 := (/ #94 2::real)
+#101 := (= #97 #100)
+#102 := [rewrite]: #101
+#98 := (= #34 #97)
+#95 := (= #33 #94)
+#89 := (= #31 #88)
+#90 := [rewrite]: #89
+#92 := (iff #32 #91)
+#93 := [monotonicity #90]: #92
+#96 := [monotonicity #93 #90]: #95
+#99 := [monotonicity #96]: #98
+#104 := [trans #99 #102]: #103
+#107 := [monotonicity #104]: #106
+#110 := [monotonicity #107]: #109
+#115 := [trans #110 #113]: #114
+#118 := [monotonicity #115]: #117
+#85 := (iff #30 #84)
+#82 := (= #29 #81)
+#83 := [rewrite]: #82
+#86 := [monotonicity #83]: #85
+#121 := [monotonicity #86 #118]: #120
+#127 := [trans #121 #125]: #126
+#130 := [monotonicity #127]: #129
+#136 := [trans #130 #134]: #135
+#139 := [monotonicity #136]: #138
+#202 := [trans #139 #200]: #201
+#59 := [asserted]: #40
+#203 := [mp #59 #202]: #198
+#205 := [not-or-elim #203]: #168
+#324 := (or #171 #289)
+#325 := [th-lemma]: #324
+#326 := [unit-resolution #325 #205]: #289
+#327 := [hypothesis]: #322
+#60 := (<= f3 0::real)
+#61 := (not #60)
+#10 := (< 0::real f3)
+#62 := (iff #10 #61)
+#63 := [rewrite]: #62
+#57 := [asserted]: #10
+#64 := [mp #57 #63]: #61
+#328 := [th-lemma #64 #327 #326]: false
+#330 := [lemma #328]: #329
+#282 := (= f3 #154)
+#283 := (= #88 #154)
+#339 := (not #283)
+#323 := (+ #88 #320)
+#331 := (<= #323 0::real)
+#336 := (not #331)
+#301 := (+ #20 #148)
+#302 := (>= #301 0::real)
+#307 := (not #302)
+#12 := (:var 0 S2)
+#15 := (f4 f6 #12)
+#275 := (pattern #15)
+#13 := (f4 f5 #12)
+#274 := (pattern #13)
+#67 := (* -1::real #15)
+#68 := (+ #13 #67)
+#69 := (<= #68 0::real)
+#218 := (not #69)
+#276 := (forall (vars (?v0 S2)) (:pat #274 #275) #218)
+#223 := (forall (vars (?v0 S2)) #218)
+#279 := (iff #223 #276)
+#277 := (iff #218 #218)
+#278 := [refl]: #277
+#280 := [quant-intro #278]: #279
+#72 := (exists (vars (?v0 S2)) #69)
+#75 := (not #72)
+#220 := (~ #75 #223)
+#219 := (~ #218 #218)
+#222 := [refl]: #219
+#221 := [nnf-neg #222]: #220
+#16 := (<= #13 #15)
+#17 := (exists (vars (?v0 S2)) #16)
+#18 := (not #17)
+#76 := (iff #18 #75)
+#73 := (iff #17 #72)
+#70 := (iff #16 #69)
+#71 := [rewrite]: #70
+#74 := [quant-intro #71]: #73
+#77 := [monotonicity #74]: #76
+#58 := [asserted]: #18
+#78 := [mp #58 #77]: #75
+#216 := [mp~ #78 #221]: #223
+#281 := [mp #216 #280]: #276
+#310 := (not #276)
+#311 := (or #310 #307)
+#291 := (* -1::real #20)
+#292 := (+ #24 #291)
+#293 := (<= #292 0::real)
+#294 := (not #293)
+#312 := (or #310 #294)
+#314 := (iff #312 #311)
+#316 := (iff #311 #311)
+#317 := [rewrite]: #316
+#308 := (iff #294 #307)
+#305 := (iff #293 #302)
+#295 := (+ #291 #24)
+#298 := (<= #295 0::real)
+#303 := (iff #298 #302)
+#304 := [rewrite]: #303
+#299 := (iff #293 #298)
+#296 := (= #292 #295)
+#297 := [rewrite]: #296
+#300 := [monotonicity #297]: #299
+#306 := [trans #300 #304]: #305
+#309 := [monotonicity #306]: #308
+#315 := [monotonicity #309]: #314
+#318 := [trans #315 #317]: #314
+#313 := [quant-inst]: #312
+#319 := [mp #313 #318]: #311
+#333 := [unit-resolution #319 #281]: #307
+#204 := [not-or-elim #203]: #143
+#334 := [hypothesis]: #331
+#335 := [th-lemma #334 #204 #333 #326]: false
+#337 := [lemma #335]: #336
+#338 := [hypothesis]: #283
+#340 := (or #339 #331)
+#341 := [th-lemma]: #340
+#342 := [unit-resolution #341 #338 #337]: false
+#343 := [lemma #342]: #339
+#287 := (or #151 #283)
+#288 := [def-axiom]: #287
+#344 := [unit-resolution #288 #343]: #151
+#284 := (not #151)
+#285 := (or #284 #282)
+#286 := [def-axiom]: #285
+#345 := [unit-resolution #286 #344]: #282
+#346 := (not #282)
+#347 := (or #346 #322)
+#348 := [th-lemma]: #347
+[unit-resolution #348 #345 #330]: false
+unsat
+17761be5b8c4a7d5d589dee9a6fb2f3f1c9050ee 288 0
+#2 := false
+#8 := 0::real
+decl f4 :: (-> S3 S2 real)
+decl f7 :: S2
+#19 := f7
+decl f8 :: S3
+#21 := f8
+#22 := (f4 f8 f7)
+decl f6 :: S3
+#14 := f6
+#20 := (f4 f6 f7)
+#73 := -1::real
+#118 := (* -1::real #20)
+#119 := (+ #118 #22)
+decl f3 :: real
+#9 := f3
+#97 := (* -1::real #22)
+#211 := (+ #20 #97)
+#212 := (+ f3 #211)
+#213 := (<= #212 0::real)
+#216 := (ite #213 f3 #119)
+#397 := (* -1::real #216)
+#398 := (+ f3 #397)
+#399 := (<= #398 0::real)
+#407 := (not #399)
+#72 := 1/2::real
+#287 := (* 1/2::real #216)
+#367 := (<= #287 0::real)
+#288 := (= #287 0::real)
+#139 := -1/2::real
+#219 := (* -1/2::real #216)
+#222 := (+ #22 #219)
+decl f5 :: S3
+#11 := f5
+#24 := (f4 f5 f7)
+#98 := (+ #97 #24)
+#196 := (* -1::real #24)
+#197 := (+ #22 #196)
+#198 := (+ f3 #197)
+#199 := (<= #198 0::real)
+#202 := (ite #199 f3 #98)
+#205 := (* 1/2::real #202)
+#208 := (+ #22 #205)
+#87 := (* 1/2::real #24)
+#185 := (+ #97 #87)
+#86 := (* 1/2::real #20)
+#186 := (+ #86 #185)
+#183 := (>= #186 0::real)
+#225 := (ite #183 #208 #222)
+#228 := (= #22 #225)
+#291 := (iff #228 #288)
+#284 := (= #22 #222)
+#289 := (iff #284 #288)
+#290 := [rewrite]: #289
+#285 := (iff #228 #284)
+#282 := (= #225 #222)
+#277 := (ite false #208 #222)
+#280 := (= #277 #222)
+#281 := [rewrite]: #280
+#278 := (= #225 #277)
+#275 := (iff #183 false)
+#182 := (not #183)
+#237 := (<= #197 0::real)
+#234 := (<= #211 0::real)
+#240 := (and #234 #237)
+#243 := (not #240)
+#231 := (not #228)
+#252 := (or #183 #231 #243)
+#257 := (not #252)
+#28 := 2::real
+#37 := (- #22 #20)
+#38 := (<= f3 #37)
+#39 := (ite #38 f3 #37)
+#40 := (/ #39 2::real)
+#41 := (- #22 #40)
+#32 := (- #24 #22)
+#33 := (<= f3 #32)
+#34 := (ite #33 f3 #32)
+#35 := (/ #34 2::real)
+#36 := (+ #22 #35)
+#27 := (+ #20 #24)
+#29 := (/ #27 2::real)
+#31 := (<= #22 #29)
+#42 := (ite #31 #36 #41)
+#43 := (= #42 #22)
+#44 := (not #43)
+#30 := (< #29 #22)
+#45 := (implies #30 #44)
+#25 := (<= #22 #24)
+#23 := (<= #20 #22)
+#26 := (and #23 #25)
+#46 := (implies #26 #45)
+#47 := (not #46)
+#260 := (iff #47 #257)
+#122 := (<= f3 #119)
+#125 := (ite #122 f3 #119)
+#140 := (* -1/2::real #125)
+#141 := (+ #22 #140)
+#101 := (<= f3 #98)
+#104 := (ite #101 f3 #98)
+#110 := (* 1/2::real #104)
+#115 := (+ #22 #110)
+#88 := (+ #86 #87)
+#94 := (<= #22 #88)
+#146 := (ite #94 #115 #141)
+#152 := (= #22 #146)
+#157 := (not #152)
+#91 := (< #88 #22)
+#163 := (not #91)
+#164 := (or #163 #157)
+#172 := (not #26)
+#173 := (or #172 #164)
+#178 := (not #173)
+#258 := (iff #178 #257)
+#255 := (iff #173 #252)
+#246 := (or #183 #231)
+#249 := (or #243 #246)
+#253 := (iff #249 #252)
+#254 := [rewrite]: #253
+#250 := (iff #173 #249)
+#247 := (iff #164 #246)
+#232 := (iff #157 #231)
+#229 := (iff #152 #228)
+#226 := (= #146 #225)
+#223 := (= #141 #222)
+#220 := (= #140 #219)
+#217 := (= #125 #216)
+#214 := (iff #122 #213)
+#215 := [rewrite]: #214
+#218 := [monotonicity #215]: #217
+#221 := [monotonicity #218]: #220
+#224 := [monotonicity #221]: #223
+#209 := (= #115 #208)
+#206 := (= #110 #205)
+#203 := (= #104 #202)
+#200 := (iff #101 #199)
+#201 := [rewrite]: #200
+#204 := [monotonicity #201]: #203
+#207 := [monotonicity #204]: #206
+#210 := [monotonicity #207]: #209
+#195 := (iff #94 #183)
+#194 := [rewrite]: #195
+#227 := [monotonicity #194 #210 #224]: #226
+#230 := [monotonicity #227]: #229
+#233 := [monotonicity #230]: #232
+#192 := (iff #163 #183)
+#187 := (not #182)
+#190 := (iff #187 #183)
+#191 := [rewrite]: #190
+#188 := (iff #163 #187)
+#181 := (iff #91 #182)
+#184 := [rewrite]: #181
+#189 := [monotonicity #184]: #188
+#193 := [trans #189 #191]: #192
+#248 := [monotonicity #193 #233]: #247
+#244 := (iff #172 #243)
+#241 := (iff #26 #240)
+#238 := (iff #25 #237)
+#239 := [rewrite]: #238
+#235 := (iff #23 #234)
+#236 := [rewrite]: #235
+#242 := [monotonicity #236 #239]: #241
+#245 := [monotonicity #242]: #244
+#251 := [monotonicity #245 #248]: #250
+#256 := [trans #251 #254]: #255
+#259 := [monotonicity #256]: #258
+#179 := (iff #47 #178)
+#176 := (iff #46 #173)
+#169 := (implies #26 #164)
+#174 := (iff #169 #173)
+#175 := [rewrite]: #174
+#170 := (iff #46 #169)
+#167 := (iff #45 #164)
+#160 := (implies #91 #157)
+#165 := (iff #160 #164)
+#166 := [rewrite]: #165
+#161 := (iff #45 #160)
+#158 := (iff #44 #157)
+#155 := (iff #43 #152)
+#149 := (= #146 #22)
+#153 := (iff #149 #152)
+#154 := [rewrite]: #153
+#150 := (iff #43 #149)
+#147 := (= #42 #146)
+#144 := (= #41 #141)
+#131 := (* 1/2::real #125)
+#136 := (- #22 #131)
+#142 := (= #136 #141)
+#143 := [rewrite]: #142
+#137 := (= #41 #136)
+#134 := (= #40 #131)
+#128 := (/ #125 2::real)
+#132 := (= #128 #131)
+#133 := [rewrite]: #132
+#129 := (= #40 #128)
+#126 := (= #39 #125)
+#120 := (= #37 #119)
+#121 := [rewrite]: #120
+#123 := (iff #38 #122)
+#124 := [monotonicity #121]: #123
+#127 := [monotonicity #124 #121]: #126
+#130 := [monotonicity #127]: #129
+#135 := [trans #130 #133]: #134
+#138 := [monotonicity #135]: #137
+#145 := [trans #138 #143]: #144
+#116 := (= #36 #115)
+#113 := (= #35 #110)
+#107 := (/ #104 2::real)
+#111 := (= #107 #110)
+#112 := [rewrite]: #111
+#108 := (= #35 #107)
+#105 := (= #34 #104)
+#99 := (= #32 #98)
+#100 := [rewrite]: #99
+#102 := (iff #33 #101)
+#103 := [monotonicity #100]: #102
+#106 := [monotonicity #103 #100]: #105
+#109 := [monotonicity #106]: #108
+#114 := [trans #109 #112]: #113
+#117 := [monotonicity #114]: #116
+#95 := (iff #31 #94)
+#89 := (= #29 #88)
+#90 := [rewrite]: #89
+#96 := [monotonicity #90]: #95
+#148 := [monotonicity #96 #117 #145]: #147
+#151 := [monotonicity #148]: #150
+#156 := [trans #151 #154]: #155
+#159 := [monotonicity #156]: #158
+#92 := (iff #30 #91)
+#93 := [monotonicity #90]: #92
+#162 := [monotonicity #93 #159]: #161
+#168 := [trans #162 #166]: #167
+#171 := [monotonicity #168]: #170
+#177 := [trans #171 #175]: #176
+#180 := [monotonicity #177]: #179
+#261 := [trans #180 #259]: #260
+#66 := [asserted]: #47
+#262 := [mp #66 #261]: #257
+#263 := [not-or-elim #262]: #182
+#276 := [iff-false #263]: #275
+#279 := [monotonicity #276]: #278
+#283 := [trans #279 #281]: #282
+#286 := [monotonicity #283]: #285
+#292 := [trans #286 #290]: #291
+#264 := [not-or-elim #262]: #228
+#293 := [mp #264 #292]: #288
+#401 := (not #288)
+#402 := (or #401 #367)
+#403 := [th-lemma]: #402
+#404 := [unit-resolution #403 #293]: #367
+#405 := [hypothesis]: #399
+#67 := (<= f3 0::real)
+#68 := (not #67)
+#10 := (< 0::real f3)
+#69 := (iff #10 #68)
+#70 := [rewrite]: #69
+#64 := [asserted]: #10
+#71 := [mp #64 #70]: #68
+#406 := [th-lemma #71 #405 #404]: false
+#408 := [lemma #406]: #407
+#360 := (= f3 #216)
+#361 := (= #119 #216)
+#416 := (not #361)
+#400 := (+ #119 #397)
+#409 := (<= #400 0::real)
+#413 := (not #409)
+#265 := [not-or-elim #262]: #240
+#267 := [and-elim #265]: #237
+#411 := [hypothesis]: #409
+#412 := [th-lemma #411 #267 #263 #404]: false
+#414 := [lemma #412]: #413
+#415 := [hypothesis]: #361
+#417 := (or #416 #409)
+#418 := [th-lemma]: #417
+#419 := [unit-resolution #418 #415 #414]: false
+#420 := [lemma #419]: #416
+#365 := (or #213 #361)
+#366 := [def-axiom]: #365
+#421 := [unit-resolution #366 #420]: #213
+#362 := (not #213)
+#363 := (or #362 #360)
+#364 := [def-axiom]: #363
+#422 := [unit-resolution #364 #421]: #360
+#423 := (not #360)
+#424 := (or #423 #399)
+#425 := [th-lemma]: #424
+[unit-resolution #425 #422 #408]: false
+unsat
+c62e7dbb8c21f248aba4bbd031c4a7dd170e0476 149 0
+#2 := false
+#23 := 0::real
+decl f3 :: (-> S2 S3 real)
+decl f5 :: S3
+#9 := f5
+decl f6 :: S2
+#11 := f6
+#12 := (f3 f6 f5)
+#49 := -1::real
+#161 := (* -1::real #12)
+decl f4 :: S2
+#8 := f4
+#10 := (f3 f4 f5)
+#208 := (+ #10 #161)
+#210 := (>= #208 0::real)
+#13 := (= #10 #12)
+#45 := [asserted]: #13
+#213 := (not #13)
+#214 := (or #213 #210)
+#215 := [th-lemma]: #214
+#216 := [unit-resolution #215 #45]: #210
+decl f7 :: S2
+#16 := f7
+#26 := (f3 f7 f5)
+#165 := (* -1::real #26)
+#166 := (+ #10 #165)
+#212 := (>= #166 0::real)
+#227 := (not #212)
+#211 := (= #10 #26)
+#221 := (not #211)
+#67 := (= #12 #26)
+#75 := (not #67)
+#222 := (iff #75 #221)
+#219 := (iff #67 #211)
+#217 := (iff #211 #67)
+#218 := [monotonicity #45]: #217
+#220 := [symm #218]: #219
+#223 := [monotonicity #220]: #222
+#27 := (= #26 #12)
+#28 := (not #27)
+#76 := (iff #28 #75)
+#73 := (iff #27 #67)
+#74 := [rewrite]: #73
+#77 := [monotonicity #74]: #76
+#48 := [asserted]: #28
+#80 := [mp #48 #77]: #75
+#224 := [mp #80 #223]: #221
+#230 := (or #211 #227)
+#167 := (<= #166 0::real)
+#177 := (+ #12 #165)
+#178 := (>= #177 0::real)
+#183 := (not #178)
+#168 := (not #167)
+#186 := (or #168 #183)
+#189 := (not #186)
+#14 := (:var 0 S3)
+#19 := (f3 f6 #14)
+#154 := (pattern #19)
+#17 := (f3 f7 #14)
+#153 := (pattern #17)
+#15 := (f3 f4 #14)
+#152 := (pattern #15)
+#55 := (* -1::real #19)
+#56 := (+ #17 #55)
+#57 := (<= #56 0::real)
+#82 := (not #57)
+#50 := (* -1::real #17)
+#51 := (+ #15 #50)
+#52 := (<= #51 0::real)
+#85 := (not #52)
+#83 := (or #85 #82)
+#81 := (not #83)
+#155 := (forall (vars (?v0 S3)) (:pat #152 #153 #154) #81)
+#91 := (forall (vars (?v0 S3)) #81)
+#158 := (iff #91 #155)
+#156 := (iff #81 #81)
+#157 := [refl]: #156
+#159 := [quant-intro #157]: #158
+#60 := (and #52 #57)
+#63 := (forall (vars (?v0 S3)) #60)
+#92 := (iff #63 #91)
+#78 := (iff #60 #81)
+#90 := [rewrite]: #78
+#93 := [quant-intro #90]: #92
+#86 := (~ #63 #63)
+#88 := (~ #60 #60)
+#89 := [refl]: #88
+#87 := [nnf-pos #89]: #86
+#20 := (<= #17 #19)
+#18 := (<= #15 #17)
+#21 := (and #18 #20)
+#22 := (forall (vars (?v0 S3)) #21)
+#64 := (iff #22 #63)
+#61 := (iff #21 #60)
+#58 := (iff #20 #57)
+#59 := [rewrite]: #58
+#53 := (iff #18 #52)
+#54 := [rewrite]: #53
+#62 := [monotonicity #54 #59]: #61
+#65 := [quant-intro #62]: #64
+#46 := [asserted]: #22
+#66 := [mp #46 #65]: #63
+#84 := [mp~ #66 #87]: #63
+#94 := [mp #84 #93]: #91
+#160 := [mp #94 #159]: #155
+#192 := (not #155)
+#193 := (or #192 #189)
+#162 := (+ #26 #161)
+#163 := (<= #162 0::real)
+#164 := (not #163)
+#169 := (or #168 #164)
+#170 := (not #169)
+#194 := (or #192 #170)
+#196 := (iff #194 #193)
+#198 := (iff #193 #193)
+#199 := [rewrite]: #198
+#190 := (iff #170 #189)
+#187 := (iff #169 #186)
+#184 := (iff #164 #183)
+#181 := (iff #163 #178)
+#171 := (+ #161 #26)
+#174 := (<= #171 0::real)
+#179 := (iff #174 #178)
+#180 := [rewrite]: #179
+#175 := (iff #163 #174)
+#172 := (= #162 #171)
+#173 := [rewrite]: #172
+#176 := [monotonicity #173]: #175
+#182 := [trans #176 #180]: #181
+#185 := [monotonicity #182]: #184
+#188 := [monotonicity #185]: #187
+#191 := [monotonicity #188]: #190
+#197 := [monotonicity #191]: #196
+#200 := [trans #197 #199]: #196
+#195 := [quant-inst]: #194
+#201 := [mp #195 #200]: #193
+#225 := [unit-resolution #201 #160]: #189
+#202 := (or #186 #167)
+#203 := [def-axiom]: #202
+#226 := [unit-resolution #203 #225]: #167
+#228 := (or #211 #168 #227)
+#229 := [th-lemma]: #228
+#231 := [unit-resolution #229 #226]: #230
+#232 := [unit-resolution #231 #224]: #227
+#204 := (or #186 #178)
+#205 := [def-axiom]: #204
+#233 := [unit-resolution #205 #225]: #178
+[th-lemma #233 #232 #216]: false
+unsat
+f2ad7d91f9a20a669bc2985b9542b252779b00c7 870 0
+#2 := false
+#11 := 0::real
+decl f5 :: real
+#26 := f5
+decl f3 :: real
+#9 := f3
+#76 := -1::real
+#77 := (* -1::real f3)
+#176 := (+ #77 f5)
+#124 := (* -1::real f5)
+#167 := (+ f3 #124)
+#260 := (>= #167 0::real)
+#267 := (ite #260 #167 #176)
+#275 := (* -1::real #267)
+decl f4 :: real
+#15 := f4
+#96 := 1/3::real
+#97 := (* 1/3::real f4)
+#276 := (+ #97 #275)
+#277 := (<= #276 0::real)
+#278 := (not #277)
+decl ?v0!5 :: real
+#448 := ?v0!5
+#459 := (* -1::real ?v0!5)
+#573 := (+ f3 #459)
+#567 := (+ #77 ?v0!5)
+#574 := (<= #573 0::real)
+#581 := (ite #574 #567 #573)
+#584 := (* -1::real #581)
+#587 := (+ #97 #584)
+#590 := (<= #587 0::real)
+#593 := (not #590)
+decl ?v2!3 :: real
+#442 := ?v2!3
+#477 := (* -1::real ?v2!3)
+#544 := (+ f5 #477)
+#538 := (+ #124 ?v2!3)
+#545 := (<= #544 0::real)
+#552 := (ite #545 #538 #544)
+#555 := (* -1::real #552)
+#558 := (+ #97 #555)
+#561 := (<= #558 0::real)
+#564 := (not #561)
+decl ?v4!1 :: real
+#446 := ?v4!1
+#532 := (+ ?v4!1 #459)
+#533 := (>= #532 0::real)
+decl ?v1!4 :: real
+#447 := ?v1!4
+#468 := (* -1::real ?v1!4)
+decl ?v5!0 :: real
+#445 := ?v5!0
+#520 := (+ ?v5!0 #468)
+#521 := (>= #520 0::real)
+#451 := (* -1::real ?v5!0)
+decl ?v3!2 :: real
+#444 := ?v3!2
+#499 := (+ ?v3!2 #451)
+#500 := (>= #499 0::real)
+#449 := (* -1::real ?v4!1)
+#497 := (+ ?v2!3 #449)
+#498 := (>= #497 0::real)
+#486 := (* -1::real ?v3!2)
+#487 := (+ f5 #486)
+#488 := (+ #124 ?v3!2)
+#489 := (<= #487 0::real)
+#490 := (ite #489 #488 #487)
+#491 := (* -1::real #490)
+#492 := (+ #97 #491)
+#493 := (<= #492 0::real)
+#494 := (not #493)
+#469 := (+ f3 #468)
+#470 := (+ #77 ?v1!4)
+#471 := (<= #469 0::real)
+#472 := (ite #471 #470 #469)
+#473 := (* -1::real #472)
+#474 := (+ #97 #473)
+#475 := (<= #474 0::real)
+#476 := (not #475)
+#599 := (and #278 #476 #494 #498 #500 #521 #533 #564 #593)
+#613 := (+ ?v5!0 #449)
+#607 := (+ #451 ?v4!1)
+#614 := (<= #613 0::real)
+#621 := (ite #614 #607 #613)
+#624 := (* -1::real #621)
+#627 := (+ f4 #624)
+#630 := (<= #627 0::real)
+#633 := (not #630)
+#604 := (not #599)
+#636 := (or #604 #633)
+#639 := (not #636)
+#450 := (+ #449 ?v5!0)
+#452 := (+ ?v4!1 #451)
+#453 := (>= #452 0::real)
+#454 := (ite #453 #452 #450)
+#455 := (* -1::real #454)
+#456 := (+ f4 #455)
+#457 := (<= #456 0::real)
+#458 := (not #457)
+#460 := (+ #459 f3)
+#461 := (+ ?v0!5 #77)
+#462 := (>= #461 0::real)
+#463 := (ite #462 #461 #460)
+#464 := (* -1::real #463)
+#465 := (+ #97 #464)
+#466 := (<= #465 0::real)
+#467 := (not #466)
+#478 := (+ #477 f5)
+#479 := (+ ?v2!3 #124)
+#480 := (>= #479 0::real)
+#481 := (ite #480 #479 #478)
+#482 := (* -1::real #481)
+#483 := (+ #97 #482)
+#484 := (<= #483 0::real)
+#485 := (not #484)
+#495 := (+ ?v0!5 #449)
+#496 := (<= #495 0::real)
+#501 := (+ ?v1!4 #451)
+#502 := (<= #501 0::real)
+#503 := (and #502 #500 #498 #496 #278 #494 #485 #476 #467)
+#504 := (not #503)
+#505 := (or #504 #458)
+#506 := (not #505)
+#640 := (iff #506 #639)
+#637 := (iff #505 #636)
+#634 := (iff #458 #633)
+#631 := (iff #457 #630)
+#628 := (= #456 #627)
+#625 := (= #455 #624)
+#622 := (= #454 #621)
+#619 := (= #450 #613)
+#620 := [rewrite]: #619
+#608 := (= #452 #607)
+#609 := [rewrite]: #608
+#617 := (iff #453 #614)
+#610 := (>= #607 0::real)
+#615 := (iff #610 #614)
+#616 := [rewrite]: #615
+#611 := (iff #453 #610)
+#612 := [monotonicity #609]: #611
+#618 := [trans #612 #616]: #617
+#623 := [monotonicity #618 #609 #620]: #622
+#626 := [monotonicity #623]: #625
+#629 := [monotonicity #626]: #628
+#632 := [monotonicity #629]: #631
+#635 := [monotonicity #632]: #634
+#605 := (iff #504 #604)
+#602 := (iff #503 #599)
+#596 := (and #521 #500 #498 #533 #278 #494 #564 #476 #593)
+#600 := (iff #596 #599)
+#601 := [rewrite]: #600
+#597 := (iff #503 #596)
+#594 := (iff #467 #593)
+#591 := (iff #466 #590)
+#588 := (= #465 #587)
+#585 := (= #464 #584)
+#582 := (= #463 #581)
+#579 := (= #460 #573)
+#580 := [rewrite]: #579
+#568 := (= #461 #567)
+#569 := [rewrite]: #568
+#577 := (iff #462 #574)
+#570 := (>= #567 0::real)
+#575 := (iff #570 #574)
+#576 := [rewrite]: #575
+#571 := (iff #462 #570)
+#572 := [monotonicity #569]: #571
+#578 := [trans #572 #576]: #577
+#583 := [monotonicity #578 #569 #580]: #582
+#586 := [monotonicity #583]: #585
+#589 := [monotonicity #586]: #588
+#592 := [monotonicity #589]: #591
+#595 := [monotonicity #592]: #594
+#565 := (iff #485 #564)
+#562 := (iff #484 #561)
+#559 := (= #483 #558)
+#556 := (= #482 #555)
+#553 := (= #481 #552)
+#550 := (= #478 #544)
+#551 := [rewrite]: #550
+#539 := (= #479 #538)
+#540 := [rewrite]: #539
+#548 := (iff #480 #545)
+#541 := (>= #538 0::real)
+#546 := (iff #541 #545)
+#547 := [rewrite]: #546
+#542 := (iff #480 #541)
+#543 := [monotonicity #540]: #542
+#549 := [trans #543 #547]: #548
+#554 := [monotonicity #549 #540 #551]: #553
+#557 := [monotonicity #554]: #556
+#560 := [monotonicity #557]: #559
+#563 := [monotonicity #560]: #562
+#566 := [monotonicity #563]: #565
+#536 := (iff #496 #533)
+#526 := (+ #449 ?v0!5)
+#529 := (<= #526 0::real)
+#534 := (iff #529 #533)
+#535 := [rewrite]: #534
+#530 := (iff #496 #529)
+#527 := (= #495 #526)
+#528 := [rewrite]: #527
+#531 := [monotonicity #528]: #530
+#537 := [trans #531 #535]: #536
+#524 := (iff #502 #521)
+#514 := (+ #451 ?v1!4)
+#517 := (<= #514 0::real)
+#522 := (iff #517 #521)
+#523 := [rewrite]: #522
+#518 := (iff #502 #517)
+#515 := (= #501 #514)
+#516 := [rewrite]: #515
+#519 := [monotonicity #516]: #518
+#525 := [trans #519 #523]: #524
+#598 := [monotonicity #525 #537 #566 #595]: #597
+#603 := [trans #598 #601]: #602
+#606 := [monotonicity #603]: #605
+#638 := [monotonicity #606 #635]: #637
+#641 := [monotonicity #638]: #640
+#46 := (:var 0 real)
+#43 := (:var 1 real)
+#217 := (* -1::real #43)
+#218 := (+ #217 #46)
+#207 := (* -1::real #46)
+#208 := (+ #43 #207)
+#407 := (>= #208 0::real)
+#414 := (ite #407 #208 #218)
+#422 := (* -1::real #414)
+#423 := (+ f4 #422)
+#424 := (<= #423 0::real)
+#425 := (not #424)
+#8 := (:var 5 real)
+#87 := (* -1::real #8)
+#88 := (+ #87 f3)
+#78 := (+ #8 #77)
+#352 := (>= #78 0::real)
+#359 := (ite #352 #78 #88)
+#367 := (* -1::real #359)
+#368 := (+ #97 #367)
+#369 := (<= #368 0::real)
+#370 := (not #369)
+#19 := (:var 4 real)
+#112 := (* -1::real #19)
+#113 := (+ f3 #112)
+#103 := (+ #77 #19)
+#329 := (<= #113 0::real)
+#336 := (ite #329 #103 #113)
+#344 := (* -1::real #336)
+#345 := (+ #97 #344)
+#346 := (<= #345 0::real)
+#347 := (not #346)
+#25 := (:var 3 real)
+#134 := (* -1::real #25)
+#135 := (+ #134 f5)
+#125 := (+ #25 #124)
+#306 := (>= #125 0::real)
+#313 := (ite #306 #125 #135)
+#321 := (* -1::real #313)
+#322 := (+ #97 #321)
+#323 := (<= #322 0::real)
+#324 := (not #323)
+#32 := (:var 2 real)
+#155 := (* -1::real #32)
+#156 := (+ f5 #155)
+#146 := (+ #124 #32)
+#283 := (<= #156 0::real)
+#290 := (ite #283 #146 #156)
+#298 := (* -1::real #290)
+#299 := (+ #97 #298)
+#300 := (<= #299 0::real)
+#301 := (not #300)
+#256 := (+ #8 #217)
+#257 := (<= #256 0::real)
+#253 := (+ #25 #217)
+#252 := (>= #253 0::real)
+#249 := (+ #32 #207)
+#248 := (>= #249 0::real)
+#244 := (+ #19 #207)
+#245 := (<= #244 0::real)
+#399 := (and #245 #248 #252 #257 #278 #301 #324 #347 #370)
+#404 := (not #399)
+#430 := (or #404 #425)
+#433 := (forall (vars (?v0 real) (?v1 real) (?v2 real) (?v3 real) (?v4 real) (?v5 real)) #430)
+#436 := (not #433)
+#507 := (~ #436 #506)
+#508 := [sk]: #507
+#57 := (- #43 #46)
+#59 := (- #57)
+#58 := (< #57 0::real)
+#60 := (ite #58 #59 #57)
+#61 := (< #60 f4)
+#48 := (<= #46 #32)
+#47 := (<= #19 #46)
+#49 := (and #47 #48)
+#45 := (<= #43 #25)
+#50 := (and #45 #49)
+#44 := (<= #8 #43)
+#51 := (and #44 #50)
+#16 := 3::real
+#17 := (/ f4 3::real)
+#38 := (- f3 f5)
+#40 := (- #38)
+#39 := (< #38 0::real)
+#41 := (ite #39 #40 #38)
+#42 := (< #41 #17)
+#52 := (and #42 #51)
+#33 := (- #32 f5)
+#35 := (- #33)
+#34 := (< #33 0::real)
+#36 := (ite #34 #35 #33)
+#37 := (< #36 #17)
+#53 := (and #37 #52)
+#27 := (- #25 f5)
+#29 := (- #27)
+#28 := (< #27 0::real)
+#30 := (ite #28 #29 #27)
+#31 := (< #30 #17)
+#54 := (and #31 #53)
+#20 := (- #19 f3)
+#22 := (- #20)
+#21 := (< #20 0::real)
+#23 := (ite #21 #22 #20)
+#24 := (< #23 #17)
+#55 := (and #24 #54)
+#10 := (- #8 f3)
+#13 := (- #10)
+#12 := (< #10 0::real)
+#14 := (ite #12 #13 #10)
+#18 := (< #14 #17)
+#56 := (and #18 #55)
+#62 := (implies #56 #61)
+#63 := (forall (vars (?v0 real) (?v1 real) (?v2 real) (?v3 real) (?v4 real) (?v5 real)) #62)
+#64 := (not #63)
+#439 := (iff #64 #436)
+#211 := (< #208 0::real)
+#223 := (ite #211 #218 #208)
+#226 := (< #223 f4)
+#170 := (< #167 0::real)
+#181 := (ite #170 #176 #167)
+#184 := (< #181 #97)
+#190 := (and #51 #184)
+#149 := (< #146 0::real)
+#161 := (ite #149 #156 #146)
+#164 := (< #161 #97)
+#195 := (and #164 #190)
+#128 := (< #125 0::real)
+#140 := (ite #128 #135 #125)
+#143 := (< #140 #97)
+#198 := (and #143 #195)
+#106 := (< #103 0::real)
+#118 := (ite #106 #113 #103)
+#121 := (< #118 #97)
+#201 := (and #121 #198)
+#81 := (< #78 0::real)
+#93 := (ite #81 #88 #78)
+#100 := (< #93 #97)
+#204 := (and #100 #201)
+#232 := (not #204)
+#233 := (or #232 #226)
+#238 := (forall (vars (?v0 real) (?v1 real) (?v2 real) (?v3 real) (?v4 real) (?v5 real)) #233)
+#241 := (not #238)
+#437 := (iff #241 #436)
+#434 := (iff #238 #433)
+#431 := (iff #233 #430)
+#428 := (iff #226 #425)
+#419 := (< #414 f4)
+#426 := (iff #419 #425)
+#427 := [rewrite]: #426
+#420 := (iff #226 #419)
+#417 := (= #223 #414)
+#408 := (not #407)
+#411 := (ite #408 #218 #208)
+#415 := (= #411 #414)
+#416 := [rewrite]: #415
+#412 := (= #223 #411)
+#409 := (iff #211 #408)
+#410 := [rewrite]: #409
+#413 := [monotonicity #410]: #412
+#418 := [trans #413 #416]: #417
+#421 := [monotonicity #418]: #420
+#429 := [trans #421 #427]: #428
+#405 := (iff #232 #404)
+#402 := (iff #204 #399)
+#375 := (and #245 #248)
+#378 := (and #252 #375)
+#381 := (and #257 #378)
+#384 := (and #381 #278)
+#387 := (and #301 #384)
+#390 := (and #324 #387)
+#393 := (and #347 #390)
+#396 := (and #370 #393)
+#400 := (iff #396 #399)
+#401 := [rewrite]: #400
+#397 := (iff #204 #396)
+#394 := (iff #201 #393)
+#391 := (iff #198 #390)
+#388 := (iff #195 #387)
+#385 := (iff #190 #384)
+#281 := (iff #184 #278)
+#272 := (< #267 #97)
+#279 := (iff #272 #278)
+#280 := [rewrite]: #279
+#273 := (iff #184 #272)
+#270 := (= #181 #267)
+#261 := (not #260)
+#264 := (ite #261 #176 #167)
+#268 := (= #264 #267)
+#269 := [rewrite]: #268
+#265 := (= #181 #264)
+#262 := (iff #170 #261)
+#263 := [rewrite]: #262
+#266 := [monotonicity #263]: #265
+#271 := [trans #266 #269]: #270
+#274 := [monotonicity #271]: #273
+#282 := [trans #274 #280]: #281
+#382 := (iff #51 #381)
+#379 := (iff #50 #378)
+#376 := (iff #49 #375)
+#250 := (iff #48 #248)
+#251 := [rewrite]: #250
+#246 := (iff #47 #245)
+#247 := [rewrite]: #246
+#377 := [monotonicity #247 #251]: #376
+#254 := (iff #45 #252)
+#255 := [rewrite]: #254
+#380 := [monotonicity #255 #377]: #379
+#258 := (iff #44 #257)
+#259 := [rewrite]: #258
+#383 := [monotonicity #259 #380]: #382
+#386 := [monotonicity #383 #282]: #385
+#304 := (iff #164 #301)
+#295 := (< #290 #97)
+#302 := (iff #295 #301)
+#303 := [rewrite]: #302
+#296 := (iff #164 #295)
+#293 := (= #161 #290)
+#284 := (not #283)
+#287 := (ite #284 #156 #146)
+#291 := (= #287 #290)
+#292 := [rewrite]: #291
+#288 := (= #161 #287)
+#285 := (iff #149 #284)
+#286 := [rewrite]: #285
+#289 := [monotonicity #286]: #288
+#294 := [trans #289 #292]: #293
+#297 := [monotonicity #294]: #296
+#305 := [trans #297 #303]: #304
+#389 := [monotonicity #305 #386]: #388
+#327 := (iff #143 #324)
+#318 := (< #313 #97)
+#325 := (iff #318 #324)
+#326 := [rewrite]: #325
+#319 := (iff #143 #318)
+#316 := (= #140 #313)
+#307 := (not #306)
+#310 := (ite #307 #135 #125)
+#314 := (= #310 #313)
+#315 := [rewrite]: #314
+#311 := (= #140 #310)
+#308 := (iff #128 #307)
+#309 := [rewrite]: #308
+#312 := [monotonicity #309]: #311
+#317 := [trans #312 #315]: #316
+#320 := [monotonicity #317]: #319
+#328 := [trans #320 #326]: #327
+#392 := [monotonicity #328 #389]: #391
+#350 := (iff #121 #347)
+#341 := (< #336 #97)
+#348 := (iff #341 #347)
+#349 := [rewrite]: #348
+#342 := (iff #121 #341)
+#339 := (= #118 #336)
+#330 := (not #329)
+#333 := (ite #330 #113 #103)
+#337 := (= #333 #336)
+#338 := [rewrite]: #337
+#334 := (= #118 #333)
+#331 := (iff #106 #330)
+#332 := [rewrite]: #331
+#335 := [monotonicity #332]: #334
+#340 := [trans #335 #338]: #339
+#343 := [monotonicity #340]: #342
+#351 := [trans #343 #349]: #350
+#395 := [monotonicity #351 #392]: #394
+#373 := (iff #100 #370)
+#364 := (< #359 #97)
+#371 := (iff #364 #370)
+#372 := [rewrite]: #371
+#365 := (iff #100 #364)
+#362 := (= #93 #359)
+#353 := (not #352)
+#356 := (ite #353 #88 #78)
+#360 := (= #356 #359)
+#361 := [rewrite]: #360
+#357 := (= #93 #356)
+#354 := (iff #81 #353)
+#355 := [rewrite]: #354
+#358 := [monotonicity #355]: #357
+#363 := [trans #358 #361]: #362
+#366 := [monotonicity #363]: #365
+#374 := [trans #366 #372]: #373
+#398 := [monotonicity #374 #395]: #397
+#403 := [trans #398 #401]: #402
+#406 := [monotonicity #403]: #405
+#432 := [monotonicity #406 #429]: #431
+#435 := [quant-intro #432]: #434
+#438 := [monotonicity #435]: #437
+#242 := (iff #64 #241)
+#239 := (iff #63 #238)
+#236 := (iff #62 #233)
+#229 := (implies #204 #226)
+#234 := (iff #229 #233)
+#235 := [rewrite]: #234
+#230 := (iff #62 #229)
+#227 := (iff #61 #226)
+#224 := (= #60 #223)
+#209 := (= #57 #208)
+#210 := [rewrite]: #209
+#221 := (= #59 #218)
+#214 := (- #208)
+#219 := (= #214 #218)
+#220 := [rewrite]: #219
+#215 := (= #59 #214)
+#216 := [monotonicity #210]: #215
+#222 := [trans #216 #220]: #221
+#212 := (iff #58 #211)
+#213 := [monotonicity #210]: #212
+#225 := [monotonicity #213 #222 #210]: #224
+#228 := [monotonicity #225]: #227
+#205 := (iff #56 #204)
+#202 := (iff #55 #201)
+#199 := (iff #54 #198)
+#196 := (iff #53 #195)
+#193 := (iff #52 #190)
+#187 := (and #184 #51)
+#191 := (iff #187 #190)
+#192 := [rewrite]: #191
+#188 := (iff #52 #187)
+#185 := (iff #42 #184)
+#98 := (= #17 #97)
+#99 := [rewrite]: #98
+#182 := (= #41 #181)
+#168 := (= #38 #167)
+#169 := [rewrite]: #168
+#179 := (= #40 #176)
+#173 := (- #167)
+#177 := (= #173 #176)
+#178 := [rewrite]: #177
+#174 := (= #40 #173)
+#175 := [monotonicity #169]: #174
+#180 := [trans #175 #178]: #179
+#171 := (iff #39 #170)
+#172 := [monotonicity #169]: #171
+#183 := [monotonicity #172 #180 #169]: #182
+#186 := [monotonicity #183 #99]: #185
+#189 := [monotonicity #186]: #188
+#194 := [trans #189 #192]: #193
+#165 := (iff #37 #164)
+#162 := (= #36 #161)
+#147 := (= #33 #146)
+#148 := [rewrite]: #147
+#159 := (= #35 #156)
+#152 := (- #146)
+#157 := (= #152 #156)
+#158 := [rewrite]: #157
+#153 := (= #35 #152)
+#154 := [monotonicity #148]: #153
+#160 := [trans #154 #158]: #159
+#150 := (iff #34 #149)
+#151 := [monotonicity #148]: #150
+#163 := [monotonicity #151 #160 #148]: #162
+#166 := [monotonicity #163 #99]: #165
+#197 := [monotonicity #166 #194]: #196
+#144 := (iff #31 #143)
+#141 := (= #30 #140)
+#126 := (= #27 #125)
+#127 := [rewrite]: #126
+#138 := (= #29 #135)
+#131 := (- #125)
+#136 := (= #131 #135)
+#137 := [rewrite]: #136
+#132 := (= #29 #131)
+#133 := [monotonicity #127]: #132
+#139 := [trans #133 #137]: #138
+#129 := (iff #28 #128)
+#130 := [monotonicity #127]: #129
+#142 := [monotonicity #130 #139 #127]: #141
+#145 := [monotonicity #142 #99]: #144
+#200 := [monotonicity #145 #197]: #199
+#122 := (iff #24 #121)
+#119 := (= #23 #118)
+#104 := (= #20 #103)
+#105 := [rewrite]: #104
+#116 := (= #22 #113)
+#109 := (- #103)
+#114 := (= #109 #113)
+#115 := [rewrite]: #114
+#110 := (= #22 #109)
+#111 := [monotonicity #105]: #110
+#117 := [trans #111 #115]: #116
+#107 := (iff #21 #106)
+#108 := [monotonicity #105]: #107
+#120 := [monotonicity #108 #117 #105]: #119
+#123 := [monotonicity #120 #99]: #122
+#203 := [monotonicity #123 #200]: #202
+#101 := (iff #18 #100)
+#94 := (= #14 #93)
+#79 := (= #10 #78)
+#80 := [rewrite]: #79
+#91 := (= #13 #88)
+#84 := (- #78)
+#89 := (= #84 #88)
+#90 := [rewrite]: #89
+#85 := (= #13 #84)
+#86 := [monotonicity #80]: #85
+#92 := [trans #86 #90]: #91
+#82 := (iff #12 #81)
+#83 := [monotonicity #80]: #82
+#95 := [monotonicity #83 #92 #80]: #94
+#102 := [monotonicity #95 #99]: #101
+#206 := [monotonicity #102 #203]: #205
+#231 := [monotonicity #206 #228]: #230
+#237 := [trans #231 #235]: #236
+#240 := [quant-intro #237]: #239
+#243 := [monotonicity #240]: #242
+#440 := [trans #243 #438]: #439
+#75 := [asserted]: #64
+#441 := [mp #75 #440]: #436
+#511 := [mp~ #441 #508]: #506
+#512 := [mp #511 #641]: #639
+#513 := [not-or-elim #512]: #599
+#642 := [and-elim #513]: #278
+#644 := [and-elim #513]: #494
+#891 := (+ #488 #491)
+#892 := (<= #891 0::real)
+#720 := (= #488 #490)
+#743 := (not #614)
+#741 := (= #607 #621)
+#884 := (not #741)
+#748 := (+ #607 #624)
+#750 := (>= #748 0::real)
+#778 := (not #750)
+#754 := (+ #538 #555)
+#755 := (<= #754 0::real)
+#777 := (not #755)
+#753 := (+ #573 #584)
+#756 := (<= #753 0::real)
+#735 := (= #573 #581)
+#736 := (not #574)
+#773 := [hypothesis]: #750
+#837 := (or #736 #778)
+#648 := [and-elim #513]: #533
+#645 := [and-elim #513]: #498
+#729 := (not #545)
+#727 := (= #538 #552)
+#814 := (not #727)
+#767 := [hypothesis]: #574
+#802 := (or #777 #778 #736)
+#763 := (+ #176 #275)
+#764 := (<= #763 0::real)
+#708 := (= #176 #267)
+#757 := (+ #469 #473)
+#758 := (<= #757 0::real)
+#714 := (= #469 #472)
+#715 := (not #471)
+#774 := [hypothesis]: #755
+#788 := (or #715 #777 #778 #736)
+#766 := [hypothesis]: #471
+#779 := (or #261 #736 #777 #778 #715)
+#649 := [and-elim #513]: #564
+#650 := [and-elim #513]: #593
+#751 := (+ #567 #584)
+#752 := (<= #751 0::real)
+#734 := (= #567 #581)
+#737 := (or #736 #734)
+#738 := [def-axiom]: #737
+#768 := [unit-resolution #738 #767]: #734
+#769 := (not #734)
+#770 := (or #769 #752)
+#771 := [th-lemma]: #770
+#772 := [unit-resolution #771 #768]: #752
+#651 := [not-or-elim #512]: #630
+#775 := [hypothesis]: #260
+#647 := [and-elim #513]: #521
+#776 := [th-lemma #767 #647 #775 #774 #645 #773 #651 #772 #650 #649 #766]: false
+#780 := [lemma #776]: #779
+#781 := [unit-resolution #780 #766 #774 #773 #767]: #261
+#711 := (or #260 #708)
+#712 := [def-axiom]: #711
+#782 := [unit-resolution #712 #781]: #708
+#783 := (not #708)
+#784 := (or #783 #764)
+#785 := [th-lemma]: #784
+#786 := [unit-resolution #785 #782]: #764
+#787 := [th-lemma #647 #774 #645 #773 #651 #649 #786 #642 #781 #766]: false
+#789 := [lemma #787]: #788
+#761 := [unit-resolution #789 #774 #773 #767]: #715
+#718 := (or #471 #714)
+#719 := [def-axiom]: #718
+#762 := [unit-resolution #719 #761]: #714
+#765 := (not #714)
+#790 := (or #765 #758)
+#791 := [th-lemma]: #790
+#792 := [unit-resolution #791 #762]: #758
+#643 := [and-elim #513]: #476
+#795 := (not #758)
+#794 := (not #498)
+#793 := (not #521)
+#796 := (or #261 #471 #793 #777 #794 #778 #633 #561 #795 #475)
+#797 := [th-lemma]: #796
+#798 := [unit-resolution #797 #761 #643 #645 #647 #649 #651 #773 #774 #792]: #261
+#799 := [unit-resolution #712 #798]: #708
+#800 := [unit-resolution #785 #799]: #764
+#801 := [th-lemma #647 #774 #645 #773 #651 #649 #792 #643 #642 #800]: false
+#803 := [lemma #801]: #802
+#826 := [unit-resolution #803 #767 #773]: #777
+#815 := (or #814 #755)
+#804 := [hypothesis]: #777
+#805 := [hypothesis]: #727
+#816 := [th-lemma]: #815
+#817 := [unit-resolution #816 #805 #804]: false
+#818 := [lemma #817]: #815
+#833 := [unit-resolution #818 #826]: #814
+#730 := (or #729 #727)
+#731 := [def-axiom]: #730
+#834 := [unit-resolution #731 #833]: #729
+#831 := (or #260 #545 #778)
+#806 := [hypothesis]: #261
+#810 := [hypothesis]: #729
+#812 := (or #545 #795 #778 #260)
+#807 := [unit-resolution #712 #806]: #708
+#808 := [unit-resolution #785 #807]: #764
+#809 := [hypothesis]: #758
+#811 := [th-lemma #810 #645 #809 #643 #647 #773 #651 #808 #642 #806]: false
+#813 := [lemma #811]: #812
+#827 := [unit-resolution #813 #806 #773 #810]: #795
+#821 := [hypothesis]: #795
+#822 := [hypothesis]: #714
+#823 := [unit-resolution #791 #822 #821]: false
+#824 := [lemma #823]: #790
+#828 := [unit-resolution #824 #827]: #765
+#829 := [unit-resolution #719 #828]: #471
+#830 := [th-lemma #808 #642 #829 #810 #645 #647 #773 #651 #806]: false
+#832 := [lemma #830]: #831
+#835 := [unit-resolution #832 #834 #773]: #260
+#836 := [th-lemma #767 #835 #834 #645 #648]: false
+#838 := [lemma #836]: #837
+#863 := [unit-resolution #838 #773]: #736
+#739 := (or #574 #735)
+#740 := [def-axiom]: #739
+#864 := [unit-resolution #740 #863]: #735
+#865 := (not #735)
+#866 := (or #865 #756)
+#867 := [th-lemma]: #866
+#868 := [unit-resolution #867 #864]: #756
+#852 := (or #260 #778)
+#845 := [unit-resolution #832 #806 #773]: #545
+#846 := [unit-resolution #731 #845]: #727
+#847 := [unit-resolution #818 #846]: #755
+#840 := (not #764)
+#841 := (or #795 #777 #778 #840)
+#825 := [hypothesis]: #764
+#839 := [th-lemma #774 #645 #647 #773 #651 #809 #643 #825 #642 #649]: false
+#842 := [lemma #839]: #841
+#848 := [unit-resolution #842 #847 #773 #808]: #795
+#849 := [unit-resolution #824 #848]: #765
+#850 := [unit-resolution #719 #849]: #471
+#851 := [th-lemma #847 #649 #645 #647 #773 #651 #808 #850 #806 #642]: false
+#853 := [lemma #851]: #852
+#859 := [unit-resolution #853 #773]: #260
+#870 := (or #471 #778)
+#856 := [hypothesis]: #715
+#857 := [unit-resolution #719 #856]: #714
+#858 := [unit-resolution #824 #857]: #758
+#860 := [unit-resolution #797 #858 #643 #645 #647 #649 #651 #773 #859 #856]: #777
+#861 := [unit-resolution #818 #860]: #814
+#862 := [unit-resolution #731 #861]: #729
+#869 := [th-lemma #643 #650 #863 #868 #859 #862 #645 #647 #773 #651 #858]: false
+#871 := [lemma #869]: #870
+#855 := [unit-resolution #871 #773]: #471
+#872 := (not #756)
+#873 := (or #777 #590 #574 #872 #561 #261 #794 #793 #778 #633 #715)
+#874 := [th-lemma]: #873
+#875 := [unit-resolution #874 #855 #645 #647 #649 #863 #650 #651 #773 #859 #868]: #777
+#876 := (or #545 #261 #794 #793 #778 #633 #715 #590 #574 #872)
+#877 := [th-lemma]: #876
+#878 := [unit-resolution #877 #855 #645 #647 #859 #863 #650 #651 #773 #868]: #545
+#879 := [unit-resolution #731 #878]: #727
+#880 := [unit-resolution #818 #879 #875]: false
+#881 := [lemma #880]: #778
+#883 := [hypothesis]: #741
+#885 := (or #884 #750)
+#886 := [th-lemma]: #885
+#887 := [unit-resolution #886 #883 #881]: false
+#888 := [lemma #887]: #884
+#744 := (or #743 #741)
+#745 := [def-axiom]: #744
+#894 := [unit-resolution #745 #888]: #743
+#930 := [hypothesis]: #736
+#935 := (or #489 #574)
+#931 := [unit-resolution #740 #930]: #735
+#893 := [hypothesis]: #872
+#915 := [hypothesis]: #735
+#916 := [unit-resolution #867 #915 #893]: false
+#917 := [lemma #916]: #866
+#932 := [unit-resolution #917 #931]: #756
+#749 := (+ #613 #624)
+#844 := (>= #749 0::real)
+#742 := (= #613 #621)
+#746 := (or #614 #742)
+#747 := [def-axiom]: #746
+#895 := [unit-resolution #747 #894]: #742
+#896 := (not #742)
+#897 := (or #896 #844)
+#898 := [th-lemma]: #897
+#899 := [unit-resolution #898 #895]: #844
+#913 := (or #872 #260)
+#900 := [hypothesis]: #756
+#646 := [and-elim #513]: #500
+#903 := (not #844)
+#902 := (not #533)
+#901 := (not #500)
+#904 := (or #489 #901 #260 #872 #840 #277 #590 #902 #903 #633)
+#905 := [th-lemma]: #904
+#906 := [unit-resolution #905 #900 #806 #646 #648 #650 #651 #808 #642 #899]: #489
+#722 := (not #489)
+#723 := (or #722 #720)
+#724 := [def-axiom]: #723
+#907 := [unit-resolution #724 #906]: #720
+#908 := (not #720)
+#909 := (or #908 #892)
+#910 := [th-lemma]: #909
+#911 := [unit-resolution #910 #907]: #892
+#912 := [th-lemma #911 #646 #900 #808 #650 #648 #899 #651 #644 #642]: false
+#914 := [lemma #912]: #913
+#890 := [unit-resolution #914 #806]: #872
+#918 := [unit-resolution #917 #890]: #865
+#919 := [unit-resolution #740 #918]: #574
+#920 := (or #489 #901 #260 #902 #903 #633 #840 #277 #736)
+#921 := [th-lemma]: #920
+#922 := [unit-resolution #921 #806 #642 #646 #648 #919 #651 #808 #899]: #489
+#923 := [unit-resolution #724 #922]: #720
+#924 := [unit-resolution #910 #923]: #892
+#925 := [th-lemma #924 #646 #806 #648 #899 #651 #808 #919 #644 #642]: false
+#926 := [lemma #925]: #260
+#933 := [hypothesis]: #722
+#934 := [th-lemma #646 #933 #926 #648 #899 #651 #932 #650 #930]: false
+#936 := [lemma #934]: #935
+#927 := [unit-resolution #936 #930]: #489
+#928 := [unit-resolution #724 #927]: #720
+#929 := [unit-resolution #910 #928]: #892
+#937 := [th-lemma #929 #644 #926 #932 #650 #646 #648 #899 #651 #927]: false
+#938 := [lemma #937]: #574
+#940 := (or #489 #261 #614 #901 #902 #736)
+#941 := [th-lemma]: #940
+#942 := [unit-resolution #941 #926 #646 #648 #938 #894]: #489
+#943 := [unit-resolution #724 #942]: #720
+#944 := [unit-resolution #910 #943]: #892
+#760 := (+ #167 #275)
+#819 := (<= #760 0::real)
+#707 := (= #167 #267)
+#709 := (or #261 #707)
+#710 := [def-axiom]: #709
+#945 := [unit-resolution #710 #926]: #707
+#946 := (not #707)
+#947 := (or #946 #819)
+#948 := [th-lemma]: #947
+#949 := [unit-resolution #948 #945]: #819
+[th-lemma #926 #949 #646 #648 #899 #651 #938 #944 #644 #642]: false
+unsat