src/HOL/Multivariate_Analysis/Integration.certs

updated SMT certificates

5ee060971856d2def7cc6d40549073dace7efe45 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
6c73093b27236ef09bc4a53162dee78b6dc31895 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
c220892677421b557c184d2f3de28c1bae1b8341 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
ca942f6174c1f53254d5ef1b69b0e75f0d4027d4 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
504ce5f4f6961a0f59840c0aa303f063d46936a5 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
024080ea9e6de105c72225d6d55cc8b136a93933 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
116b1dd4c85396a326f34f6c1266b1ad85116049 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
74073317ccefcdf35878e5154f8155d12c8475cf 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
ada412db5ba79d588ff49226c319d0dae76f5f87 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
3f6125a99a8cb462db3a2586a1eae0021b892091 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
9ecd5f8eb0c8f78bd68a366175093e04632f1f73 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
2dea73fd0603d00ddaec5e14116c465addb0b89e 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