src/HOL/Multivariate_Analysis/Integration.certs

updated SMT certificates

148c2437fb9e64ff4110383f54f5a9a720082439 428 0
#2 := false
decl f12 :: S2
#42 := f12
decl f5 :: S2
#25 := f5
#49 := (= f5 f12)
decl f3 :: (-> int S2)
decl f4 :: (-> S2 int)
#43 := (f4 f12)
#593 := (f3 #43)
#691 := (= #593 f12)
#594 := (= f12 #593)
#8 := (:var 0 S2)
#9 := (f4 #8)
#546 := (pattern #9)
#10 := (f3 #9)
#98 := (= #8 #10)
#547 := (forall (vars (?v0 S2)) (:pat #546) #98)
#101 := (forall (vars (?v0 S2)) #98)
#550 := (iff #101 #547)
#548 := (iff #98 #98)
#549 := [refl]: #548
#551 := [quant-intro #549]: #550
#461 := (~ #101 #101)
#463 := (~ #98 #98)
#464 := [refl]: #463
#462 := [nnf-pos #464]: #461
#11 := (= #10 #8)
#12 := (forall (vars (?v0 S2)) #11)
#102 := (iff #12 #101)
#99 := (iff #11 #98)
#100 := [rewrite]: #99
#103 := [quant-intro #100]: #102
#97 := [asserted]: #12
#106 := [mp #97 #103]: #101
#459 := [mp~ #106 #462]: #101
#552 := [mp #459 #551]: #547
#595 := (not #547)
#600 := (or #595 #594)
#601 := [quant-inst]: #600
#685 := [unit-resolution #601 #552]: #594
#692 := [symm #685]: #691
#693 := (= f5 #593)
#26 := (f4 f5)
#591 := (f3 #26)
#689 := (= #591 #593)
#687 := (= #593 #591)
#683 := (= #43 #26)
#681 := (= #26 #43)
#13 := 0::int
#232 := -1::int
#235 := (* -1::int #43)
#236 := (+ #26 #235)
#301 := (<= #236 0::int)
#74 := (<= #26 #43)
#398 := (iff #74 #301)
#399 := [rewrite]: #398
#352 := [asserted]: #74
#400 := [mp #352 #399]: #301
#234 := (>= #236 0::int)
decl f6 :: (-> S3 S4 real)
decl f8 :: (-> S2 S4)
#29 := (f8 f5)
decl f9 :: S3
#31 := f9
#32 := (f6 f9 #29)
decl f11 :: S3
#37 := f11
#38 := (f6 f11 #29)
#50 := (f8 f12)
decl f7 :: S3
#28 := f7
#51 := (f6 f7 #50)
#52 := (ite #49 #51 #38)
#261 := (ite #234 #52 #32)
#573 := (= #32 #261)
#653 := (not #573)
#199 := 0::real
#197 := -1::real
#270 := (* -1::real #261)
#645 := (+ #32 #270)
#647 := (>= #645 0::real)
#650 := (not #647)
#648 := [hypothesis]: #647
decl f10 :: S3
#34 := f10
#35 := (f6 f10 #29)
#271 := (+ #35 #270)
#269 := (>= #271 0::real)
#272 := (not #269)
#30 := (f6 f7 #29)
decl f13 :: S3
#45 := f13
#46 := (f6 f13 #29)
#242 := (ite #234 #46 #30)
#250 := (* -1::real #242)
#251 := (+ #35 #250)
#252 := (<= #251 0::real)
#253 := (not #252)
#277 := (and #253 #272)
#44 := (< #26 #43)
#53 := (ite #44 #32 #52)
#54 := (< #35 #53)
#47 := (ite #44 #30 #46)
#48 := (< #47 #35)
#55 := (and #48 #54)
#278 := (iff #55 #277)
#275 := (iff #54 #272)
#266 := (< #35 #261)
#273 := (iff #266 #272)
#274 := [rewrite]: #273
#267 := (iff #54 #266)
#264 := (= #53 #261)
#233 := (not #234)
#258 := (ite #233 #32 #52)
#262 := (= #258 #261)
#263 := [rewrite]: #262
#259 := (= #53 #258)
#237 := (iff #44 #233)
#238 := [rewrite]: #237
#260 := [monotonicity #238]: #259
#265 := [trans #260 #263]: #264
#268 := [monotonicity #265]: #267
#276 := [trans #268 #274]: #275
#256 := (iff #48 #253)
#247 := (< #242 #35)
#254 := (iff #247 #253)
#255 := [rewrite]: #254
#248 := (iff #48 #247)
#245 := (= #47 #242)
#239 := (ite #233 #30 #46)
#243 := (= #239 #242)
#244 := [rewrite]: #243
#240 := (= #47 #239)
#241 := [monotonicity #238]: #240
#246 := [trans #241 #244]: #245
#249 := [monotonicity #246]: #248
#257 := [trans #249 #255]: #256
#279 := [monotonicity #257 #276]: #278
#183 := [asserted]: #55
#280 := [mp #183 #279]: #277
#282 := [and-elim #280]: #272
#201 := (* -1::real #35)
#202 := (+ #32 #201)
#200 := (>= #202 0::real)
#198 := (not #200)
#218 := (* -1::real #38)
#219 := (+ #35 #218)
#217 := (>= #219 0::real)
#220 := (not #217)
#225 := (and #198 #220)
#27 := (< #26 #26)
#39 := (ite #27 #32 #38)
#40 := (< #35 #39)
#33 := (ite #27 #30 #32)
#36 := (< #33 #35)
#41 := (and #36 #40)
#226 := (iff #41 #225)
#223 := (iff #40 #220)
#214 := (< #35 #38)
#221 := (iff #214 #220)
#222 := [rewrite]: #221
#215 := (iff #40 #214)
#212 := (= #39 #38)
#207 := (ite false #32 #38)
#210 := (= #207 #38)
#211 := [rewrite]: #210
#208 := (= #39 #207)
#185 := (iff #27 false)
#186 := [rewrite]: #185
#209 := [monotonicity #186]: #208
#213 := [trans #209 #211]: #212
#216 := [monotonicity #213]: #215
#224 := [trans #216 #222]: #223
#205 := (iff #36 #198)
#194 := (< #32 #35)
#203 := (iff #194 #198)
#204 := [rewrite]: #203
#195 := (iff #36 #194)
#192 := (= #33 #32)
#187 := (ite false #30 #32)
#190 := (= #187 #32)
#191 := [rewrite]: #190
#188 := (= #33 #187)
#189 := [monotonicity #186]: #188
#193 := [trans #189 #191]: #192
#196 := [monotonicity #193]: #195
#206 := [trans #196 #204]: #205
#227 := [monotonicity #206 #224]: #226
#182 := [asserted]: #41
#228 := [mp #182 #227]: #225
#229 := [and-elim #228]: #198
#649 := [th-lemma #229 #282 #648]: false
#651 := [lemma #649]: #650
#652 := [hypothesis]: #573
#654 := (or #653 #647)
#655 := [th-lemma]: #654
#656 := [unit-resolution #655 #652 #651]: false
#657 := [lemma #656]: #653
#583 := (or #234 #573)
#584 := [def-axiom]: #583
#680 := [unit-resolution #584 #657]: #234
#682 := [th-lemma #680 #400]: #681
#684 := [symm #682]: #683
#688 := [monotonicity #684]: #687
#690 := [symm #688]: #689
#592 := (= f5 #591)
#596 := (or #595 #592)
#597 := [quant-inst]: #596
#686 := [unit-resolution #597 #552]: #592
#694 := [trans #686 #690]: #693
#695 := [trans #694 #692]: #49
#576 := (not #49)
#58 := (f6 f13 #50)
#284 := (ite #49 #32 #58)
#472 := (* -1::real #284)
#637 := (+ #32 #472)
#638 := (<= #637 0::real)
#585 := (= #32 #284)
#661 := [hypothesis]: #49
#587 := (or #576 #585)
#588 := [def-axiom]: #587
#662 := [unit-resolution #588 #661]: #585
#663 := (not #585)
#664 := (or #663 #638)
#665 := [th-lemma]: #664
#666 := [unit-resolution #665 #662]: #638
#61 := (f6 f10 #50)
#368 := (* -1::real #61)
#384 := (+ #51 #368)
#385 := (<= #384 0::real)
#386 := (not #385)
#369 := (+ #58 #368)
#367 := (>= #369 0::real)
#366 := (not #367)
#391 := (and #366 #386)
#63 := (f6 f9 #50)
#68 := (< #43 #43)
#71 := (ite #68 #63 #51)
#72 := (< #61 #71)
#69 := (ite #68 #51 #58)
#70 := (< #69 #61)
#73 := (and #70 #72)
#392 := (iff #73 #391)
#389 := (iff #72 #386)
#381 := (< #61 #51)
#387 := (iff #381 #386)
#388 := [rewrite]: #387
#382 := (iff #72 #381)
#379 := (= #71 #51)
#374 := (ite false #63 #51)
#377 := (= #374 #51)
#378 := [rewrite]: #377
#375 := (= #71 #374)
#354 := (iff #68 false)
#355 := [rewrite]: #354
#376 := [monotonicity #355]: #375
#380 := [trans #376 #378]: #379
#383 := [monotonicity #380]: #382
#390 := [trans #383 #388]: #389
#372 := (iff #70 #366)
#363 := (< #58 #61)
#370 := (iff #363 #366)
#371 := [rewrite]: #370
#364 := (iff #70 #363)
#361 := (= #69 #58)
#356 := (ite false #51 #58)
#359 := (= #356 #58)
#360 := [rewrite]: #359
#357 := (= #69 #356)
#358 := [monotonicity #355]: #357
#362 := [trans #358 #360]: #361
#365 := [monotonicity #362]: #364
#373 := [trans #365 #371]: #372
#393 := [monotonicity #373 #390]: #392
#351 := [asserted]: #73
#394 := [mp #351 #393]: #391
#396 := [and-elim #394]: #386
#402 := (* -1::real #63)
#403 := (+ #51 #402)
#404 := (<= #403 0::real)
#414 := (* -1::real #58)
#415 := (+ #51 #414)
#413 := (>= #415 0::real)
#64 := (f6 f11 #50)
#407 := (* -1::real #64)
#408 := (+ #63 #407)
#409 := (<= #408 0::real)
#423 := (and #404 #409 #413)
#77 := (<= #63 #64)
#76 := (<= #51 #63)
#78 := (and #76 #77)
#75 := (<= #58 #51)
#79 := (and #75 #78)
#426 := (iff #79 #423)
#417 := (and #404 #409)
#420 := (and #413 #417)
#424 := (iff #420 #423)
#425 := [rewrite]: #424
#421 := (iff #79 #420)
#418 := (iff #78 #417)
#410 := (iff #77 #409)
#411 := [rewrite]: #410
#405 := (iff #76 #404)
#406 := [rewrite]: #405
#419 := [monotonicity #406 #411]: #418
#412 := (iff #75 #413)
#416 := [rewrite]: #412
#422 := [monotonicity #416 #419]: #421
#427 := [trans #422 #425]: #426
#353 := [asserted]: #79
#428 := [mp #353 #427]: #423
#429 := [and-elim #428]: #404
#642 := (+ #32 #402)
#644 := (>= #642 0::real)
#641 := (= #32 #63)
#671 := (= #63 #32)
#669 := (= #50 #29)
#667 := (= #29 #50)
#668 := [monotonicity #661]: #667
#670 := [symm #668]: #669
#672 := [monotonicity #670]: #671
#673 := [symm #672]: #641
#674 := (not #641)
#675 := (or #674 #644)
#676 := [th-lemma]: #675
#677 := [unit-resolution #676 #673]: #644
#475 := (+ #61 #472)
#478 := (<= #475 0::real)
#451 := (not #478)
#327 := (ite #301 #284 #51)
#335 := (* -1::real #327)
#336 := (+ #61 #335)
#337 := (<= #336 0::real)
#338 := (not #337)
#452 := (iff #338 #451)
#479 := (iff #337 #478)
#476 := (= #336 #475)
#473 := (= #335 #472)
#470 := (= #327 #284)
#1 := true
#465 := (ite true #284 #51)
#468 := (= #465 #284)
#469 := [rewrite]: #468
#466 := (= #327 #465)
#457 := (iff #301 true)
#458 := [iff-true #400]: #457
#467 := [monotonicity #458]: #466
#471 := [trans #467 #469]: #470
#474 := [monotonicity #471]: #473
#477 := [monotonicity #474]: #476
#480 := [monotonicity #477]: #479
#481 := [monotonicity #480]: #452
#308 := (ite #301 #64 #63)
#318 := (* -1::real #308)
#319 := (+ #61 #318)
#317 := (>= #319 0::real)
#316 := (not #317)
#343 := (and #316 #338)
#56 := (< #43 #26)
#65 := (ite #56 #63 #64)
#66 := (< #61 #65)
#57 := (= f12 f5)
#59 := (ite #57 #32 #58)
#60 := (ite #56 #51 #59)
#62 := (< #60 #61)
#67 := (and #62 #66)
#346 := (iff #67 #343)
#287 := (ite #56 #51 #284)
#290 := (< #287 #61)
#296 := (and #66 #290)
#344 := (iff #296 #343)
#341 := (iff #290 #338)
#332 := (< #327 #61)
#339 := (iff #332 #338)
#340 := [rewrite]: #339
#333 := (iff #290 #332)
#330 := (= #287 #327)
#302 := (not #301)
#324 := (ite #302 #51 #284)
#328 := (= #324 #327)
#329 := [rewrite]: #328
#325 := (= #287 #324)
#303 := (iff #56 #302)
#304 := [rewrite]: #303
#326 := [monotonicity #304]: #325
#331 := [trans #326 #329]: #330
#334 := [monotonicity #331]: #333
#342 := [trans #334 #340]: #341
#322 := (iff #66 #316)
#313 := (< #61 #308)
#320 := (iff #313 #316)
#321 := [rewrite]: #320
#314 := (iff #66 #313)
#311 := (= #65 #308)
#305 := (ite #302 #63 #64)
#309 := (= #305 #308)
#310 := [rewrite]: #309
#306 := (= #65 #305)
#307 := [monotonicity #304]: #306
#312 := [trans #307 #310]: #311
#315 := [monotonicity #312]: #314
#323 := [trans #315 #321]: #322
#345 := [monotonicity #323 #342]: #344
#299 := (iff #67 #296)
#293 := (and #290 #66)
#297 := (iff #293 #296)
#298 := [rewrite]: #297
#294 := (iff #67 #293)
#291 := (iff #62 #290)
#288 := (= #60 #287)
#285 := (= #59 #284)
#231 := (iff #57 #49)
#283 := [rewrite]: #231
#286 := [monotonicity #283]: #285
#289 := [monotonicity #286]: #288
#292 := [monotonicity #289]: #291
#295 := [monotonicity #292]: #294
#300 := [trans #295 #298]: #299
#347 := [trans #300 #345]: #346
#184 := [asserted]: #67
#348 := [mp #184 #347]: #343
#350 := [and-elim #348]: #338
#482 := [mp #350 #481]: #451
#678 := [th-lemma #482 #677 #429 #396 #666]: false
#679 := [lemma #678]: #576
[unit-resolution #679 #695]: false
unsat
3563da621b35b09e69b7f5fa5fa01c2868364b3e 422 0
#2 := false
decl f12 :: S2
#42 := f12
decl f5 :: S2
#25 := f5
#45 := (= f5 f12)
decl f3 :: (-> int S2)
decl f4 :: (-> S2 int)
#43 := (f4 f12)
#598 := (f3 #43)
#696 := (= #598 f12)
#599 := (= f12 #598)
#8 := (:var 0 S2)
#9 := (f4 #8)
#551 := (pattern #9)
#10 := (f3 #9)
#98 := (= #8 #10)
#552 := (forall (vars (?v0 S2)) (:pat #551) #98)
#101 := (forall (vars (?v0 S2)) #98)
#555 := (iff #101 #552)
#553 := (iff #98 #98)
#554 := [refl]: #553
#556 := [quant-intro #554]: #555
#455 := (~ #101 #101)
#457 := (~ #98 #98)
#458 := [refl]: #457
#456 := [nnf-pos #458]: #455
#11 := (= #10 #8)
#12 := (forall (vars (?v0 S2)) #11)
#102 := (iff #12 #101)
#99 := (iff #11 #98)
#100 := [rewrite]: #99
#103 := [quant-intro #100]: #102
#97 := [asserted]: #12
#106 := [mp #97 #103]: #101
#453 := [mp~ #106 #456]: #101
#557 := [mp #453 #556]: #552
#600 := (not #552)
#605 := (or #600 #599)
#606 := [quant-inst]: #605
#690 := [unit-resolution #606 #557]: #599
#697 := [symm #690]: #696
#698 := (= f5 #598)
#26 := (f4 f5)
#596 := (f3 #26)
#694 := (= #596 #598)
#692 := (= #598 #596)
#688 := (= #43 #26)
#686 := (= #26 #43)
#13 := 0::int
#231 := -1::int
#234 := (* -1::int #43)
#235 := (+ #26 #234)
#295 := (<= #235 0::int)
#74 := (<= #26 #43)
#393 := (iff #74 #295)
#394 := [rewrite]: #393
#346 := [asserted]: #74
#395 := [mp #346 #394]: #295
#233 := (>= #235 0::int)
decl f6 :: (-> S3 S4 real)
decl f8 :: (-> S2 S4)
#29 := (f8 f5)
decl f7 :: S3
#28 := f7
#30 := (f6 f7 #29)
decl f9 :: S3
#31 := f9
#32 := (f6 f9 #29)
#46 := (f8 f12)
decl f11 :: S3
#37 := f11
#47 := (f6 f11 #46)
#48 := (ite #45 #47 #32)
#241 := (ite #233 #48 #30)
#572 := (= #30 #241)
#658 := (not #572)
#199 := 0::real
#197 := -1::real
#249 := (* -1::real #241)
#647 := (+ #30 #249)
#648 := (<= #647 0::real)
#652 := (not #648)
#650 := [hypothesis]: #648
decl f10 :: S3
#34 := f10
#35 := (f6 f10 #29)
#250 := (+ #35 #249)
#251 := (<= #250 0::real)
#252 := (not #251)
#38 := (f6 f11 #29)
decl f13 :: S3
#51 := f13
#52 := (f6 f13 #29)
#260 := (ite #233 #52 #38)
#269 := (* -1::real #260)
#270 := (+ #35 #269)
#268 := (>= #270 0::real)
#271 := (not #268)
#276 := (and #252 #271)
#44 := (< #26 #43)
#53 := (ite #44 #38 #52)
#54 := (< #35 #53)
#49 := (ite #44 #30 #48)
#50 := (< #49 #35)
#55 := (and #50 #54)
#277 := (iff #55 #276)
#274 := (iff #54 #271)
#265 := (< #35 #260)
#272 := (iff #265 #271)
#273 := [rewrite]: #272
#266 := (iff #54 #265)
#263 := (= #53 #260)
#232 := (not #233)
#257 := (ite #232 #38 #52)
#261 := (= #257 #260)
#262 := [rewrite]: #261
#258 := (= #53 #257)
#236 := (iff #44 #232)
#237 := [rewrite]: #236
#259 := [monotonicity #237]: #258
#264 := [trans #259 #262]: #263
#267 := [monotonicity #264]: #266
#275 := [trans #267 #273]: #274
#255 := (iff #50 #252)
#246 := (< #241 #35)
#253 := (iff #246 #252)
#254 := [rewrite]: #253
#247 := (iff #50 #246)
#244 := (= #49 #241)
#238 := (ite #232 #30 #48)
#242 := (= #238 #241)
#243 := [rewrite]: #242
#239 := (= #49 #238)
#240 := [monotonicity #237]: #239
#245 := [trans #240 #243]: #244
#248 := [monotonicity #245]: #247
#256 := [trans #248 #254]: #255
#278 := [monotonicity #256 #275]: #277
#183 := [asserted]: #55
#279 := [mp #183 #278]: #276
#280 := [and-elim #279]: #252
#201 := (* -1::real #35)
#217 := (+ #30 #201)
#218 := (<= #217 0::real)
#219 := (not #218)
#202 := (+ #32 #201)
#200 := (>= #202 0::real)
#198 := (not #200)
#224 := (and #198 #219)
#27 := (< #26 #26)
#39 := (ite #27 #38 #30)
#40 := (< #35 #39)
#33 := (ite #27 #30 #32)
#36 := (< #33 #35)
#41 := (and #36 #40)
#225 := (iff #41 #224)
#222 := (iff #40 #219)
#214 := (< #35 #30)
#220 := (iff #214 #219)
#221 := [rewrite]: #220
#215 := (iff #40 #214)
#212 := (= #39 #30)
#207 := (ite false #38 #30)
#210 := (= #207 #30)
#211 := [rewrite]: #210
#208 := (= #39 #207)
#185 := (iff #27 false)
#186 := [rewrite]: #185
#209 := [monotonicity #186]: #208
#213 := [trans #209 #211]: #212
#216 := [monotonicity #213]: #215
#223 := [trans #216 #221]: #222
#205 := (iff #36 #198)
#194 := (< #32 #35)
#203 := (iff #194 #198)
#204 := [rewrite]: #203
#195 := (iff #36 #194)
#192 := (= #33 #32)
#187 := (ite false #30 #32)
#190 := (= #187 #32)
#191 := [rewrite]: #190
#188 := (= #33 #187)
#189 := [monotonicity #186]: #188
#193 := [trans #189 #191]: #192
#196 := [monotonicity #193]: #195
#206 := [trans #196 #204]: #205
#226 := [monotonicity #206 #223]: #225
#182 := [asserted]: #41
#227 := [mp #182 #226]: #224
#229 := [and-elim #227]: #219
#651 := [th-lemma #229 #280 #650]: false
#653 := [lemma #651]: #652
#657 := [hypothesis]: #572
#659 := (or #658 #648)
#660 := [th-lemma]: #659
#661 := [unit-resolution #660 #657 #653]: false
#662 := [lemma #661]: #658
#582 := (or #233 #572)
#583 := [def-axiom]: #582
#685 := [unit-resolution #583 #662]: #233
#687 := [th-lemma #685 #395]: #686
#689 := [symm #687]: #688
#693 := [monotonicity #689]: #692
#695 := [symm #693]: #694
#597 := (= f5 #596)
#601 := (or #600 #597)
#602 := [quant-inst]: #601
#691 := [unit-resolution #602 #557]: #597
#699 := [trans #691 #695]: #698
#700 := [trans #699 #697]: #45
#575 := (not #45)
#63 := (f6 f13 #46)
#283 := (ite #45 #30 #63)
#466 := (* -1::real #283)
#642 := (+ #30 #466)
#644 := (>= #642 0::real)
#590 := (= #30 #283)
#666 := [hypothesis]: #45
#592 := (or #575 #590)
#593 := [def-axiom]: #592
#667 := [unit-resolution #593 #666]: #590
#668 := (not #590)
#669 := (or #668 #644)
#670 := [th-lemma]: #669
#671 := [unit-resolution #670 #667]: #644
#60 := (f6 f10 #46)
#362 := (* -1::real #60)
#363 := (+ #47 #362)
#361 := (>= #363 0::real)
#360 := (not #361)
#379 := (* -1::real #63)
#380 := (+ #60 #379)
#378 := (>= #380 0::real)
#381 := (not #378)
#386 := (and #360 #381)
#68 := (< #43 #43)
#71 := (ite #68 #47 #63)
#72 := (< #60 #71)
#57 := (f6 f7 #46)
#69 := (ite #68 #57 #47)
#70 := (< #69 #60)
#73 := (and #70 #72)
#387 := (iff #73 #386)
#384 := (iff #72 #381)
#375 := (< #60 #63)
#382 := (iff #375 #381)
#383 := [rewrite]: #382
#376 := (iff #72 #375)
#373 := (= #71 #63)
#368 := (ite false #47 #63)
#371 := (= #368 #63)
#372 := [rewrite]: #371
#369 := (= #71 #368)
#348 := (iff #68 false)
#349 := [rewrite]: #348
#370 := [monotonicity #349]: #369
#374 := [trans #370 #372]: #373
#377 := [monotonicity #374]: #376
#385 := [trans #377 #383]: #384
#366 := (iff #70 #360)
#357 := (< #47 #60)
#364 := (iff #357 #360)
#365 := [rewrite]: #364
#358 := (iff #70 #357)
#355 := (= #69 #47)
#350 := (ite false #57 #47)
#353 := (= #350 #47)
#354 := [rewrite]: #353
#351 := (= #69 #350)
#352 := [monotonicity #349]: #351
#356 := [trans #352 #354]: #355
#359 := [monotonicity #356]: #358
#367 := [trans #359 #365]: #366
#388 := [monotonicity #367 #385]: #387
#345 := [asserted]: #73
#389 := [mp #345 #388]: #386
#390 := [and-elim #389]: #360
#399 := (* -1::real #57)
#400 := (+ #47 #399)
#398 := (>= #400 0::real)
#58 := (f6 f9 #46)
#407 := (* -1::real #58)
#408 := (+ #57 #407)
#406 := (>= #408 0::real)
#402 := (+ #47 #379)
#403 := (<= #402 0::real)
#417 := (and #398 #403 #406)
#77 := (<= #47 #63)
#76 := (<= #57 #47)
#78 := (and #76 #77)
#75 := (<= #58 #57)
#79 := (and #75 #78)
#420 := (iff #79 #417)
#411 := (and #398 #403)
#414 := (and #406 #411)
#418 := (iff #414 #417)
#419 := [rewrite]: #418
#415 := (iff #79 #414)
#412 := (iff #78 #411)
#404 := (iff #77 #403)
#405 := [rewrite]: #404
#397 := (iff #76 #398)
#401 := [rewrite]: #397
#413 := [monotonicity #401 #405]: #412
#409 := (iff #75 #406)
#410 := [rewrite]: #409
#416 := [monotonicity #410 #413]: #415
#421 := [trans #416 #419]: #420
#347 := [asserted]: #79
#422 := [mp #347 #421]: #417
#423 := [and-elim #422]: #398
#655 := (+ #30 #399)
#656 := (<= #655 0::real)
#654 := (= #30 #57)
#676 := (= #57 #30)
#674 := (= #46 #29)
#672 := (= #29 #46)
#673 := [monotonicity #666]: #672
#675 := [symm #673]: #674
#677 := [monotonicity #675]: #676
#678 := [symm #677]: #654
#679 := (not #654)
#680 := (or #679 #656)
#681 := [th-lemma]: #680
#682 := [unit-resolution #681 #678]: #656
#469 := (+ #60 #466)
#472 := (>= #469 0::real)
#445 := (not #472)
#321 := (ite #295 #283 #47)
#331 := (* -1::real #321)
#332 := (+ #60 #331)
#330 := (>= #332 0::real)
#329 := (not #330)
#446 := (iff #329 #445)
#473 := (iff #330 #472)
#470 := (= #332 #469)
#467 := (= #331 #466)
#464 := (= #321 #283)
#1 := true
#459 := (ite true #283 #47)
#462 := (= #459 #283)
#463 := [rewrite]: #462
#460 := (= #321 #459)
#451 := (iff #295 true)
#452 := [iff-true #395]: #451
#461 := [monotonicity #452]: #460
#465 := [trans #461 #463]: #464
#468 := [monotonicity #465]: #467
#471 := [monotonicity #468]: #470
#474 := [monotonicity #471]: #473
#475 := [monotonicity #474]: #446
#302 := (ite #295 #58 #57)
#310 := (* -1::real #302)
#311 := (+ #60 #310)
#312 := (<= #311 0::real)
#313 := (not #312)
#337 := (and #313 #329)
#62 := (= f12 f5)
#64 := (ite #62 #30 #63)
#56 := (< #43 #26)
#65 := (ite #56 #47 #64)
#66 := (< #60 #65)
#59 := (ite #56 #57 #58)
#61 := (< #59 #60)
#67 := (and #61 #66)
#340 := (iff #67 #337)
#286 := (ite #56 #47 #283)
#289 := (< #60 #286)
#292 := (and #61 #289)
#338 := (iff #292 #337)
#335 := (iff #289 #329)
#326 := (< #60 #321)
#333 := (iff #326 #329)
#334 := [rewrite]: #333
#327 := (iff #289 #326)
#324 := (= #286 #321)
#296 := (not #295)
#318 := (ite #296 #47 #283)
#322 := (= #318 #321)
#323 := [rewrite]: #322
#319 := (= #286 #318)
#297 := (iff #56 #296)
#298 := [rewrite]: #297
#320 := [monotonicity #298]: #319
#325 := [trans #320 #323]: #324
#328 := [monotonicity #325]: #327
#336 := [trans #328 #334]: #335
#316 := (iff #61 #313)
#307 := (< #302 #60)
#314 := (iff #307 #313)
#315 := [rewrite]: #314
#308 := (iff #61 #307)
#305 := (= #59 #302)
#299 := (ite #296 #57 #58)
#303 := (= #299 #302)
#304 := [rewrite]: #303
#300 := (= #59 #299)
#301 := [monotonicity #298]: #300
#306 := [trans #301 #304]: #305
#309 := [monotonicity #306]: #308
#317 := [trans #309 #315]: #316
#339 := [monotonicity #317 #336]: #338
#293 := (iff #67 #292)
#290 := (iff #66 #289)
#287 := (= #65 #286)
#284 := (= #64 #283)
#230 := (iff #62 #45)
#282 := [rewrite]: #230
#285 := [monotonicity #282]: #284
#288 := [monotonicity #285]: #287
#291 := [monotonicity #288]: #290
#294 := [monotonicity #291]: #293
#341 := [trans #294 #339]: #340
#184 := [asserted]: #67
#342 := [mp #184 #341]: #337
#344 := [and-elim #342]: #329
#476 := [mp #344 #475]: #445
#683 := [th-lemma #476 #682 #423 #390 #671]: false
#684 := [lemma #683]: #575
[unit-resolution #684 #700]: false
unsat
84444fc7be1372d94ec0514d2ec99e1693c028e3 921 0
#2 := false
#58 := 0::int
decl f5 :: (-> S4 int)
decl f6 :: (-> S2 S4)
decl f11 :: (-> S4 S2)
decl f14 :: S4
#30 := f14
#34 := (f11 f14)
#70 := (f6 #34)
#605 := (f5 #70)
#121 := -1::int
#615 := (* -1::int #605)
decl f7 :: S4
#13 := f7
#14 := (f5 f7)
#662 := (+ #14 #615)
#663 := (<= #662 0::int)
decl f8 :: (-> S5 S2 real)
decl f19 :: (-> S3 S5)
decl f15 :: S3
#40 := f15
#86 := (f19 f15)
#650 := (f8 #86 #34)
decl f10 :: S5
#19 := f10
#35 := (f8 f10 #34)
#651 := (= #35 #650)
#690 := (not #651)
decl f13 :: S3
#28 := f13
#81 := (f19 f13)
#749 := (f8 #81 #34)
#1233 := (= #650 #749)
#1246 := (not #1233)
#1335 := (iff #1246 #690)
#1333 := (iff #1233 #651)
#1328 := (= #650 #35)
#1331 := (iff #1328 #651)
#1332 := [commutativity]: #1331
#1329 := (iff #1233 #1328)
#1326 := (= #749 #35)
#752 := (= #35 #749)
decl f12 :: S5
#22 := f12
#696 := (f8 f12 #34)
#751 := (= #696 #749)
#281 := (= f14 #70)
#755 := (ite #281 #752 #751)
decl f9 :: S5
#16 := f9
#694 := (f8 f9 #34)
#750 := (= #694 #749)
#31 := (f5 f14)
#616 := (+ #31 #615)
#617 := (<= #616 0::int)
#758 := (ite #617 #755 #750)
#9 := (:var 0 S2)
#17 := (f8 f9 #9)
#538 := (pattern #17)
#23 := (f8 f12 #9)
#537 := (pattern #23)
#82 := (f8 #81 #9)
#545 := (pattern #82)
#11 := (f6 #9)
#535 := (pattern #11)
#452 := (= #17 #82)
#450 := (= #23 #82)
#449 := (= #35 #82)
#33 := (= #11 f14)
#451 := (ite #33 #449 #450)
#146 := (* -1::int #31)
#12 := (f5 #11)
#147 := (+ #12 #146)
#145 := (>= #147 0::int)
#453 := (ite #145 #451 #452)
#546 := (forall (vars (?v0 S2)) (:pat #535 #545 #537 #538) #453)
#456 := (forall (vars (?v0 S2)) #453)
#549 := (iff #456 #546)
#547 := (iff #453 #453)
#548 := [refl]: #547
#550 := [quant-intro #548]: #549
#36 := (ite #33 #35 #23)
#153 := (ite #145 #36 #17)
#380 := (= #82 #153)
#381 := (forall (vars (?v0 S2)) #380)
#457 := (iff #381 #456)
#454 := (iff #380 #453)
#455 := [rewrite]: #454
#458 := [quant-intro #455]: #457
#366 := (~ #381 #381)
#368 := (~ #380 #380)
#365 := [refl]: #368
#363 := [nnf-pos #365]: #366
decl f3 :: (-> S3 S2 real)
#29 := (f3 f13 #9)
#158 := (= #29 #153)
#161 := (forall (vars (?v0 S2)) #158)
#382 := (iff #161 #381)
#96 := (:var 1 S3)
#99 := (f3 #96 #9)
#97 := (f19 #96)
#98 := (f8 #97 #9)
#100 := (= #98 #99)
#101 := (forall (vars (?v0 S3) (?v1 S2)) #100)
#298 := [asserted]: #101
#383 := [rewrite* #298]: #382
#32 := (< #12 #31)
#37 := (ite #32 #17 #36)
#38 := (= #29 #37)
#39 := (forall (vars (?v0 S2)) #38)
#162 := (iff #39 #161)
#159 := (iff #38 #158)
#156 := (= #37 #153)
#144 := (not #145)
#150 := (ite #144 #17 #36)
#154 := (= #150 #153)
#155 := [rewrite]: #154
#151 := (= #37 #150)
#148 := (iff #32 #144)
#149 := [rewrite]: #148
#152 := [monotonicity #149]: #151
#157 := [trans #152 #155]: #156
#160 := [monotonicity #157]: #159
#163 := [quant-intro #160]: #162
#119 := [asserted]: #39
#164 := [mp #119 #163]: #161
#384 := [mp #164 #383]: #381
#364 := [mp~ #384 #363]: #381
#459 := [mp #364 #458]: #456
#551 := [mp #459 #550]: #546
#761 := (not #546)
#762 := (or #761 #758)
#71 := (= #70 f14)
#753 := (ite #71 #752 #751)
#606 := (+ #605 #146)
#607 := (>= #606 0::int)
#754 := (ite #607 #753 #750)
#763 := (or #761 #754)
#765 := (iff #763 #762)
#767 := (iff #762 #762)
#768 := [rewrite]: #767
#759 := (iff #754 #758)
#756 := (iff #753 #755)
#282 := (iff #71 #281)
#283 := [rewrite]: #282
#757 := [monotonicity #283]: #756
#620 := (iff #607 #617)
#609 := (+ #146 #605)
#612 := (>= #609 0::int)
#618 := (iff #612 #617)
#619 := [rewrite]: #618
#613 := (iff #607 #612)
#610 := (= #606 #609)
#611 := [rewrite]: #610
#614 := [monotonicity #611]: #613
#621 := [trans #614 #619]: #620
#760 := [monotonicity #621 #757]: #759
#766 := [monotonicity #760]: #765
#769 := [trans #766 #768]: #765
#764 := [quant-inst]: #763
#770 := [mp #764 #769]: #762
#1317 := [unit-resolution #770 #551]: #758
#981 := (= #31 #605)
#1295 := (= #605 #31)
#280 := [asserted]: #71
#286 := [mp #280 #283]: #281
#1290 := [symm #286]: #71
#1296 := [monotonicity #1290]: #1295
#1297 := [symm #1296]: #981
#1318 := (not #981)
#1319 := (or #1318 #617)
#1320 := [th-lemma]: #1319
#1321 := [unit-resolution #1320 #1297]: #617
#639 := (not #617)
#783 := (not #758)
#784 := (or #783 #639 #755)
#785 := [def-axiom]: #784
#1322 := [unit-resolution #785 #1321 #1317]: #755
#771 := (not #755)
#1323 := (or #771 #752)
#772 := (not #281)
#773 := (or #771 #772 #752)
#774 := [def-axiom]: #773
#1324 := [unit-resolution #774 #286]: #1323
#1325 := [unit-resolution #1324 #1322]: #752
#1327 := [symm #1325]: #1326
#1330 := [monotonicity #1327]: #1329
#1334 := [trans #1330 #1332]: #1333
#1336 := [monotonicity #1334]: #1335
#303 := 0::real
#301 := -1::real
#1033 := (* -1::real #749)
#1234 := (+ #650 #1033)
#1236 := (>= #1234 0::real)
#1243 := (not #1236)
#1237 := [hypothesis]: #1236
decl f20 :: S5
#78 := f20
#1034 := (f8 f20 #34)
#1037 := (* -1::real #1034)
#1048 := (+ #749 #1037)
#1049 := (<= #1048 0::real)
#1073 := (not #1049)
decl f17 :: S3
#48 := f17
#76 := (f19 f17)
#601 := (f8 #76 #34)
#1038 := (+ #601 #1037)
#1039 := (>= #1038 0::real)
#1054 := (or #1039 #1049)
#1057 := (not #1054)
#79 := (f8 f20 #9)
#588 := (pattern #79)
#77 := (f8 #76 #9)
#561 := (pattern #77)
#310 := (* -1::real #82)
#311 := (+ #79 #310)
#309 := (>= #311 0::real)
#305 := (* -1::real #79)
#306 := (+ #77 #305)
#304 := (>= #306 0::real)
#422 := (or #304 #309)
#423 := (not #422)
#589 := (forall (vars (?v0 S2)) (:pat #561 #588 #545) #423)
#426 := (forall (vars (?v0 S2)) #423)
#592 := (iff #426 #589)
#590 := (iff #423 #423)
#591 := [refl]: #590
#593 := [quant-intro #591]: #592
#312 := (not #309)
#302 := (not #304)
#315 := (and #302 #312)
#318 := (forall (vars (?v0 S2)) #315)
#427 := (iff #318 #426)
#424 := (iff #315 #423)
#425 := [rewrite]: #424
#428 := [quant-intro #425]: #427
#414 := (~ #318 #318)
#412 := (~ #315 #315)
#413 := [refl]: #412
#415 := [nnf-pos #413]: #414
decl f4 :: S3
#8 := f4
#89 := (f19 f4)
#90 := (f8 #89 #9)
#328 := (* -1::real #90)
#329 := (+ #79 #328)
#327 := (>= #329 0::real)
#330 := (not #327)
#87 := (f8 #86 #9)
#321 := (* -1::real #87)
#322 := (+ #79 #321)
#323 := (<= #322 0::real)
#324 := (not #323)
#333 := (and #324 #330)
#336 := (forall (vars (?v0 S2)) #333)
#339 := (and #318 #336)
#91 := (< #79 #90)
#88 := (< #87 #79)
#92 := (and #88 #91)
#93 := (forall (vars (?v0 S2)) #92)
#83 := (< #79 #82)
#80 := (< #77 #79)
#84 := (and #80 #83)
#85 := (forall (vars (?v0 S2)) #84)
#94 := (and #85 #93)
#340 := (iff #94 #339)
#337 := (iff #93 #336)
#334 := (iff #92 #333)
#331 := (iff #91 #330)
#332 := [rewrite]: #331
#325 := (iff #88 #324)
#326 := [rewrite]: #325
#335 := [monotonicity #326 #332]: #334
#338 := [quant-intro #335]: #337
#319 := (iff #85 #318)
#316 := (iff #84 #315)
#313 := (iff #83 #312)
#314 := [rewrite]: #313
#307 := (iff #80 #302)
#308 := [rewrite]: #307
#317 := [monotonicity #308 #314]: #316
#320 := [quant-intro #317]: #319
#341 := [monotonicity #320 #338]: #340
#297 := [asserted]: #94
#342 := [mp #297 #341]: #339
#343 := [and-elim #342]: #318
#416 := [mp~ #343 #415]: #318
#429 := [mp #416 #428]: #426
#594 := [mp #429 #593]: #589
#1060 := (not #589)
#1061 := (or #1060 #1057)
#1035 := (+ #1034 #1033)
#1036 := (>= #1035 0::real)
#1040 := (or #1039 #1036)
#1041 := (not #1040)
#1062 := (or #1060 #1041)
#1064 := (iff #1062 #1061)
#1066 := (iff #1061 #1061)
#1067 := [rewrite]: #1066
#1058 := (iff #1041 #1057)
#1055 := (iff #1040 #1054)
#1052 := (iff #1036 #1049)
#1042 := (+ #1033 #1034)
#1045 := (>= #1042 0::real)
#1050 := (iff #1045 #1049)
#1051 := [rewrite]: #1050
#1046 := (iff #1036 #1045)
#1043 := (= #1035 #1042)
#1044 := [rewrite]: #1043
#1047 := [monotonicity #1044]: #1046
#1053 := [trans #1047 #1051]: #1052
#1056 := [monotonicity #1053]: #1055
#1059 := [monotonicity #1056]: #1058
#1065 := [monotonicity #1059]: #1064
#1068 := [trans #1065 #1067]: #1064
#1063 := [quant-inst]: #1062
#1069 := [mp #1063 #1068]: #1061
#1238 := [unit-resolution #1069 #594]: #1057
#1074 := (or #1054 #1073)
#1075 := [def-axiom]: #1074
#1239 := [unit-resolution #1075 #1238]: #1073
#1150 := (+ #650 #1037)
#1151 := (>= #1150 0::real)
#1183 := (not #1151)
#693 := (f8 #89 #34)
#1162 := (+ #693 #1037)
#1163 := (<= #1162 0::real)
#1168 := (or #1151 #1163)
#1171 := (not #1168)
#536 := (pattern #90)
#553 := (pattern #87)
#430 := (or #323 #327)
#431 := (not #430)
#595 := (forall (vars (?v0 S2)) (:pat #588 #553 #536) #431)
#434 := (forall (vars (?v0 S2)) #431)
#598 := (iff #434 #595)
#596 := (iff #431 #431)
#597 := [refl]: #596
#599 := [quant-intro #597]: #598
#435 := (iff #336 #434)
#432 := (iff #333 #431)
#433 := [rewrite]: #432
#436 := [quant-intro #433]: #435
#419 := (~ #336 #336)
#417 := (~ #333 #333)
#418 := [refl]: #417
#420 := [nnf-pos #418]: #419
#344 := [and-elim #342]: #336
#421 := [mp~ #344 #420]: #336
#437 := [mp #421 #436]: #434
#600 := [mp #437 #599]: #595
#1118 := (not #595)
#1174 := (or #1118 #1171)
#1136 := (* -1::real #693)
#1137 := (+ #1034 #1136)
#1138 := (>= #1137 0::real)
#1139 := (* -1::real #650)
#1140 := (+ #1034 #1139)
#1141 := (<= #1140 0::real)
#1142 := (or #1141 #1138)
#1143 := (not #1142)
#1175 := (or #1118 #1143)
#1177 := (iff #1175 #1174)
#1179 := (iff #1174 #1174)
#1180 := [rewrite]: #1179
#1172 := (iff #1143 #1171)
#1169 := (iff #1142 #1168)
#1166 := (iff #1138 #1163)
#1156 := (+ #1136 #1034)
#1159 := (>= #1156 0::real)
#1164 := (iff #1159 #1163)
#1165 := [rewrite]: #1164
#1160 := (iff #1138 #1159)
#1157 := (= #1137 #1156)
#1158 := [rewrite]: #1157
#1161 := [monotonicity #1158]: #1160
#1167 := [trans #1161 #1165]: #1166
#1154 := (iff #1141 #1151)
#1144 := (+ #1139 #1034)
#1147 := (<= #1144 0::real)
#1152 := (iff #1147 #1151)
#1153 := [rewrite]: #1152
#1148 := (iff #1141 #1147)
#1145 := (= #1140 #1144)
#1146 := [rewrite]: #1145
#1149 := [monotonicity #1146]: #1148
#1155 := [trans #1149 #1153]: #1154
#1170 := [monotonicity #1155 #1167]: #1169
#1173 := [monotonicity #1170]: #1172
#1178 := [monotonicity #1173]: #1177
#1181 := [trans #1178 #1180]: #1177
#1176 := [quant-inst]: #1175
#1182 := [mp #1176 #1181]: #1174
#1240 := [unit-resolution #1182 #600]: #1171
#1184 := (or #1168 #1183)
#1185 := [def-axiom]: #1184
#1241 := [unit-resolution #1185 #1240]: #1183
#1242 := [th-lemma #1241 #1239 #1237]: false
#1244 := [lemma #1242]: #1243
#1247 := (or #1246 #1236)
#1248 := [th-lemma]: #1247
#1316 := [unit-resolution #1248 #1244]: #1246
#1337 := [mp #1316 #1336]: #690
#1339 := (or #663 #651)
decl f16 :: S5
#43 := f16
#603 := (f8 f16 #34)
#652 := (= #603 #650)
#668 := (ite #663 #652 #651)
#42 := (f8 f10 #9)
#554 := (pattern #42)
#44 := (f8 f16 #9)
#552 := (pattern #44)
#461 := (= #42 #87)
#460 := (= #44 #87)
#124 := (* -1::int #14)
#125 := (+ #12 #124)
#123 := (>= #125 0::int)
#462 := (ite #123 #460 #461)
#555 := (forall (vars (?v0 S2)) (:pat #535 #552 #553 #554) #462)
#465 := (forall (vars (?v0 S2)) #462)
#558 := (iff #465 #555)
#556 := (iff #462 #462)
#557 := [refl]: #556
#559 := [quant-intro #557]: #558
#169 := (ite #123 #44 #42)
#385 := (= #87 #169)
#386 := (forall (vars (?v0 S2)) #385)
#466 := (iff #386 #465)
#463 := (iff #385 #462)
#464 := [rewrite]: #463
#467 := [quant-intro #464]: #466
#359 := (~ #386 #386)
#361 := (~ #385 #385)
#362 := [refl]: #361
#360 := [nnf-pos #362]: #359
#41 := (f3 f15 #9)
#174 := (= #41 #169)
#177 := (forall (vars (?v0 S2)) #174)
#387 := (iff #177 #386)
#388 := [rewrite* #298]: #387
#15 := (< #12 #14)
#45 := (ite #15 #42 #44)
#46 := (= #41 #45)
#47 := (forall (vars (?v0 S2)) #46)
#178 := (iff #47 #177)
#175 := (iff #46 #174)
#172 := (= #45 #169)
#122 := (not #123)
#166 := (ite #122 #42 #44)
#170 := (= #166 #169)
#171 := [rewrite]: #170
#167 := (= #45 #166)
#126 := (iff #15 #122)
#127 := [rewrite]: #126
#168 := [monotonicity #127]: #167
#173 := [trans #168 #171]: #172
#176 := [monotonicity #173]: #175
#179 := [quant-intro #176]: #178
#120 := [asserted]: #47
#180 := [mp #120 #179]: #177
#389 := [mp #180 #388]: #386
#357 := [mp~ #389 #360]: #386
#468 := [mp #357 #467]: #465
#560 := [mp #468 #559]: #555
#671 := (not #555)
#672 := (or #671 #668)
#653 := (+ #605 #124)
#654 := (>= #653 0::int)
#655 := (ite #654 #652 #651)
#673 := (or #671 #655)
#675 := (iff #673 #672)
#677 := (iff #672 #672)
#678 := [rewrite]: #677
#669 := (iff #655 #668)
#666 := (iff #654 #663)
#656 := (+ #124 #605)
#659 := (>= #656 0::int)
#664 := (iff #659 #663)
#665 := [rewrite]: #664
#660 := (iff #654 #659)
#657 := (= #653 #656)
#658 := [rewrite]: #657
#661 := [monotonicity #658]: #660
#667 := [trans #661 #665]: #666
#670 := [monotonicity #667]: #669
#676 := [monotonicity #670]: #675
#679 := [trans #676 #678]: #675
#674 := [quant-inst]: #673
#680 := [mp #674 #679]: #672
#1338 := [unit-resolution #680 #560]: #668
#681 := (not #668)
#685 := (or #681 #663 #651)
#686 := [def-axiom]: #685
#1340 := [unit-resolution #686 #1338]: #1339
#1341 := [unit-resolution #1340 #1337]: #663
#1286 := (+ #14 #146)
#1287 := (<= #1286 0::int)
#1376 := (not #1287)
#1285 := (= #14 #31)
#1314 := (not #1285)
#290 := (= f7 f14)
#702 := (= f7 #70)
decl f18 :: (-> int S4)
#985 := (f18 #605)
#1305 := (= #985 #70)
#986 := (= #70 #985)
#53 := (:var 0 S4)
#54 := (f5 #53)
#568 := (pattern #54)
#55 := (f18 #54)
#181 := (= #53 #55)
#569 := (forall (vars (?v0 S4)) (:pat #568) #181)
#199 := (forall (vars (?v0 S4)) #181)
#572 := (iff #199 #569)
#570 := (iff #181 #181)
#571 := [refl]: #570
#573 := [quant-intro #571]: #572
#399 := (~ #199 #199)
#397 := (~ #181 #181)
#398 := [refl]: #397
#400 := [nnf-pos #398]: #399
#56 := (= #55 #53)
#57 := (forall (vars (?v0 S4)) #56)
#200 := (iff #57 #199)
#197 := (iff #56 #181)
#198 := [rewrite]: #197
#201 := [quant-intro #198]: #200
#165 := [asserted]: #57
#204 := [mp #165 #201]: #199
#401 := [mp~ #204 #400]: #199
#574 := [mp #401 #573]: #569
#989 := (not #569)
#990 := (or #989 #986)
#991 := [quant-inst]: #990
#1289 := [unit-resolution #991 #574]: #986
#1306 := [symm #1289]: #1305
#1309 := (= f7 #985)
#20 := (f11 f7)
#72 := (f6 #20)
#797 := (f5 #72)
#987 := (f18 #797)
#1303 := (= #987 #985)
#1300 := (= #797 #605)
#1298 := (= #797 #31)
#1291 := [hypothesis]: #1285
#1293 := (= #797 #14)
#73 := (= #72 f7)
#285 := (= f7 #72)
#287 := (iff #73 #285)
#288 := [rewrite]: #287
#284 := [asserted]: #73
#291 := [mp #284 #288]: #285
#1292 := [symm #291]: #73
#1294 := [monotonicity #1292]: #1293
#1299 := [trans #1294 #1291]: #1298
#1301 := [trans #1299 #1297]: #1300
#1304 := [monotonicity #1301]: #1303
#1307 := (= f7 #987)
#988 := (= #72 #987)
#994 := (or #989 #988)
#995 := [quant-inst]: #994
#1302 := [unit-resolution #995 #574]: #988
#1308 := [trans #291 #1302]: #1307
#1310 := [trans #1308 #1304]: #1309
#1311 := [trans #1310 #1306]: #702
#1312 := [trans #1311 #1290]: #290
#294 := (not #290)
#74 := (= f14 f7)
#75 := (not #74)
#295 := (iff #75 #294)
#292 := (iff #74 #290)
#293 := [rewrite]: #292
#296 := [monotonicity #293]: #295
#289 := [asserted]: #75
#299 := [mp #289 #296]: #294
#1313 := [unit-resolution #299 #1312]: false
#1315 := [lemma #1313]: #1314
#1380 := (or #1285 #1376)
#1288 := (>= #1286 0::int)
#807 := (* -1::int #797)
#808 := (+ #31 #807)
#809 := (<= #808 0::int)
#793 := (f8 #76 #20)
#21 := (f8 f10 #20)
#794 := (= #21 #793)
#838 := (not #794)
#883 := (f8 #89 #20)
#1259 := (= #793 #883)
#1272 := (not #1259)
#1362 := (iff #1272 #838)
#1360 := (iff #1259 #794)
#1355 := (= #793 #21)
#1358 := (iff #1355 #794)
#1359 := [commutativity]: #1358
#1356 := (iff #1259 #1355)
#1353 := (= #883 #21)
#888 := (= #21 #883)