src/HOL/Multivariate_Analysis/Integration.cert

 #199 := (or #181 #173)
 #200 := [def-axiom]: #199
 #228 := [unit-resolution #200 #220]: #173
 [th-lemma #228 #227 #211]: false
 unsat
+610fb185d846b293ce6bb466b6770a65def3e59c 768 0
+#2 := false
+#7 := 0::real
+decl uf_2 :: real
+#5 := uf_2
+#75 := -1::real
+#76 := (* -1::real uf_2)
+decl uf_1 :: real
+#4 := uf_1
+#77 := (+ uf_1 #76)
+#316 := (>= #77 0::real)
+#317 := (not #316)
+decl uf_8 :: real
+#39 := uf_8
+#216 := (* -1::real uf_8)
+#220 := (+ uf_1 #216)
+#221 := (<= #220 0::real)
+#86 := (* -1::real uf_1)
+#87 := (+ #86 uf_2)
+#323 := (ite #316 #77 #87)
+#331 := (* -1::real #323)
+decl uf_3 :: real
+#11 := uf_3
+#95 := 1/3::real
+#96 := (* 1/3::real uf_3)
+#332 := (+ #96 #331)
+#333 := (<= #332 0::real)
+#334 := (not #333)
+decl uf_4 :: real
+#15 := uf_4
+#111 := (* -1::real uf_4)
+#112 := (+ uf_2 #111)
+#102 := (+ #76 uf_4)
+#293 := (<= #112 0::real)
+#300 := (ite #293 #102 #112)
+#308 := (* -1::real #300)
+#309 := (+ #96 #308)
+#310 := (<= #309 0::real)
+#311 := (not #310)
+decl uf_6 :: real
+#22 := uf_6
+decl uf_5 :: real
+#21 := uf_5
+#133 := (* -1::real uf_5)
+#134 := (+ #133 uf_6)
+#123 := (* -1::real uf_6)
+#124 := (+ uf_5 #123)
+#270 := (>= #124 0::real)
+#277 := (ite #270 #124 #134)
+#285 := (* -1::real #277)
+#286 := (+ #96 #285)
+#287 := (<= #286 0::real)
+#288 := (not #287)
+decl uf_7 :: real
+#28 := uf_7
+#154 := (* -1::real uf_7)
+#155 := (+ uf_6 #154)
+#145 := (+ #123 uf_7)
+#247 := (<= #155 0::real)
+#254 := (ite #247 #145 #155)
+#262 := (* -1::real #254)
+#263 := (+ #96 #262)
+#264 := (<= #263 0::real)
+#265 := (not #264)
+#175 := (+ #76 uf_6)
+#166 := (+ uf_2 #123)
+#224 := (>= #166 0::real)
+#231 := (ite #224 #166 #175)
+#239 := (* -1::real #231)
+#240 := (+ #96 #239)
+#241 := (<= #240 0::real)
+#242 := (not #241)
+#217 := (+ uf_5 #216)
+#215 := (>= #217 0::real)
+decl uf_9 :: real
+#42 := uf_9
+#206 := (* -1::real uf_9)
+#212 := (+ uf_7 #206)
+#211 := (>= #212 0::real)
+#207 := (+ uf_4 #206)
+#208 := (<= #207 0::real)
+#363 := (and #208 #211 #215 #221 #242 #265 #288 #311 #334)
+#44 := (<= uf_9 uf_7)
+#43 := (<= uf_4 uf_9)
+#45 := (and #43 #44)
+#41 := (<= uf_8 uf_5)
+#46 := (and #41 #45)
+#40 := (<= uf_1 uf_8)
+#47 := (and #40 #46)
+#12 := 3::real
+#13 := (/ uf_3 3::real)
+#34 := (- uf_2 uf_6)
+#36 := (- #34)
+#35 := (< #34 0::real)
+#37 := (ite #35 #36 #34)
+#38 := (< #37 #13)
+#48 := (and #38 #47)
+#29 := (- uf_7 uf_6)
+#31 := (- #29)
+#30 := (< #29 0::real)
+#32 := (ite #30 #31 #29)
+#33 := (< #32 #13)
+#49 := (and #33 #48)
+#23 := (- uf_5 uf_6)
+#25 := (- #23)
+#24 := (< #23 0::real)
+#26 := (ite #24 #25 #23)
+#27 := (< #26 #13)
+#50 := (and #27 #49)
+#16 := (- uf_4 uf_2)
+#18 := (- #16)
+#17 := (< #16 0::real)
+#19 := (ite #17 #18 #16)
+#20 := (< #19 #13)
+#51 := (and #20 #50)
+#6 := (- uf_1 uf_2)
+#9 := (- #6)
+#8 := (< #6 0::real)
+#10 := (ite #8 #9 #6)
+#14 := (< #10 #13)
+#52 := (and #14 #51)
+#368 := (iff #52 #363)
+#169 := (< #166 0::real)
+#180 := (ite #169 #175 #166)
+#183 := (< #180 #96)
+#189 := (and #47 #183)
+#148 := (< #145 0::real)
+#160 := (ite #148 #155 #145)
+#163 := (< #160 #96)
+#194 := (and #163 #189)
+#127 := (< #124 0::real)
+#139 := (ite #127 #134 #124)
+#142 := (< #139 #96)
+#197 := (and #142 #194)
+#105 := (< #102 0::real)
+#117 := (ite #105 #112 #102)
+#120 := (< #117 #96)
+#200 := (and #120 #197)
+#80 := (< #77 0::real)
+#92 := (ite #80 #87 #77)
+#99 := (< #92 #96)
+#203 := (and #99 #200)
+#366 := (iff #203 #363)
+#339 := (and #208 #211)
+#342 := (and #215 #339)
+#345 := (and #221 #342)
+#348 := (and #345 #242)
+#351 := (and #265 #348)
+#354 := (and #288 #351)
+#357 := (and #311 #354)
+#360 := (and #334 #357)
+#364 := (iff #360 #363)
+#365 := [rewrite]: #364
+#361 := (iff #203 #360)
+#358 := (iff #200 #357)
+#355 := (iff #197 #354)
+#352 := (iff #194 #351)
+#349 := (iff #189 #348)
+#245 := (iff #183 #242)
+#236 := (< #231 #96)
+#243 := (iff #236 #242)
+#244 := [rewrite]: #243
+#237 := (iff #183 #236)
+#234 := (= #180 #231)
+#225 := (not #224)
+#228 := (ite #225 #175 #166)
+#232 := (= #228 #231)
+#233 := [rewrite]: #232
+#229 := (= #180 #228)
+#226 := (iff #169 #225)
+#227 := [rewrite]: #226
+#230 := [monotonicity #227]: #229
+#235 := [trans #230 #233]: #234
+#238 := [monotonicity #235]: #237
+#246 := [trans #238 #244]: #245
+#346 := (iff #47 #345)
+#343 := (iff #46 #342)
+#340 := (iff #45 #339)
+#213 := (iff #44 #211)
+#214 := [rewrite]: #213
+#209 := (iff #43 #208)
+#210 := [rewrite]: #209
+#341 := [monotonicity #210 #214]: #340
+#218 := (iff #41 #215)
+#219 := [rewrite]: #218
+#344 := [monotonicity #219 #341]: #343
+#222 := (iff #40 #221)
+#223 := [rewrite]: #222
+#347 := [monotonicity #223 #344]: #346
+#350 := [monotonicity #347 #246]: #349
+#268 := (iff #163 #265)
+#259 := (< #254 #96)
+#266 := (iff #259 #265)
+#267 := [rewrite]: #266
+#260 := (iff #163 #259)
+#257 := (= #160 #254)
+#248 := (not #247)
+#251 := (ite #248 #155 #145)
+#255 := (= #251 #254)
+#256 := [rewrite]: #255
+#252 := (= #160 #251)
+#249 := (iff #148 #248)
+#250 := [rewrite]: #249
+#253 := [monotonicity #250]: #252
+#258 := [trans #253 #256]: #257
+#261 := [monotonicity #258]: #260
+#269 := [trans #261 #267]: #268
+#353 := [monotonicity #269 #350]: #352
+#291 := (iff #142 #288)
+#282 := (< #277 #96)
+#289 := (iff #282 #288)
+#290 := [rewrite]: #289
+#283 := (iff #142 #282)
+#280 := (= #139 #277)
+#271 := (not #270)
+#274 := (ite #271 #134 #124)
+#278 := (= #274 #277)
+#279 := [rewrite]: #278
+#275 := (= #139 #274)
+#272 := (iff #127 #271)
+#273 := [rewrite]: #272
+#276 := [monotonicity #273]: #275
+#281 := [trans #276 #279]: #280
+#284 := [monotonicity #281]: #283
+#292 := [trans #284 #290]: #291
+#356 := [monotonicity #292 #353]: #355
+#314 := (iff #120 #311)
+#305 := (< #300 #96)
+#312 := (iff #305 #311)
+#313 := [rewrite]: #312
+#306 := (iff #120 #305)
+#303 := (= #117 #300)
+#294 := (not #293)
+#297 := (ite #294 #112 #102)
+#301 := (= #297 #300)
+#302 := [rewrite]: #301
+#298 := (= #117 #297)
+#295 := (iff #105 #294)
+#296 := [rewrite]: #295
+#299 := [monotonicity #296]: #298
+#304 := [trans #299 #302]: #303
+#307 := [monotonicity #304]: #306
+#315 := [trans #307 #313]: #314
+#359 := [monotonicity #315 #356]: #358
+#337 := (iff #99 #334)
+#328 := (< #323 #96)
+#335 := (iff #328 #334)
+#336 := [rewrite]: #335
+#329 := (iff #99 #328)
+#326 := (= #92 #323)
+#320 := (ite #317 #87 #77)
+#324 := (= #320 #323)
+#325 := [rewrite]: #324
+#321 := (= #92 #320)
+#318 := (iff #80 #317)
+#319 := [rewrite]: #318
+#322 := [monotonicity #319]: #321
+#327 := [trans #322 #325]: #326
+#330 := [monotonicity #327]: #329
+#338 := [trans #330 #336]: #337
+#362 := [monotonicity #338 #359]: #361
+#367 := [trans #362 #365]: #366
+#204 := (iff #52 #203)
+#201 := (iff #51 #200)
+#198 := (iff #50 #197)
+#195 := (iff #49 #194)
+#192 := (iff #48 #189)
+#186 := (and #183 #47)
+#190 := (iff #186 #189)
+#191 := [rewrite]: #190
+#187 := (iff #48 #186)
+#184 := (iff #38 #183)
+#97 := (= #13 #96)
+#98 := [rewrite]: #97
+#181 := (= #37 #180)
+#167 := (= #34 #166)
+#168 := [rewrite]: #167
+#178 := (= #36 #175)
+#172 := (- #166)
+#176 := (= #172 #175)
+#177 := [rewrite]: #176
+#173 := (= #36 #172)
+#174 := [monotonicity #168]: #173
+#179 := [trans #174 #177]: #178
+#170 := (iff #35 #169)
+#171 := [monotonicity #168]: #170
+#182 := [monotonicity #171 #179 #168]: #181
+#185 := [monotonicity #182 #98]: #184
+#188 := [monotonicity #185]: #187
+#193 := [trans #188 #191]: #192
+#164 := (iff #33 #163)
+#161 := (= #32 #160)
+#146 := (= #29 #145)
+#147 := [rewrite]: #146
+#158 := (= #31 #155)
+#151 := (- #145)
+#156 := (= #151 #155)
+#157 := [rewrite]: #156
+#152 := (= #31 #151)
+#153 := [monotonicity #147]: #152
+#159 := [trans #153 #157]: #158
+#149 := (iff #30 #148)
+#150 := [monotonicity #147]: #149
+#162 := [monotonicity #150 #159 #147]: #161
+#165 := [monotonicity #162 #98]: #164
+#196 := [monotonicity #165 #193]: #195
+#143 := (iff #27 #142)
+#140 := (= #26 #139)
+#125 := (= #23 #124)
+#126 := [rewrite]: #125
+#137 := (= #25 #134)
+#130 := (- #124)
+#135 := (= #130 #134)
+#136 := [rewrite]: #135
+#131 := (= #25 #130)
+#132 := [monotonicity #126]: #131
+#138 := [trans #132 #136]: #137
+#128 := (iff #24 #127)
+#129 := [monotonicity #126]: #128
+#141 := [monotonicity #129 #138 #126]: #140
+#144 := [monotonicity #141 #98]: #143
+#199 := [monotonicity #144 #196]: #198
+#121 := (iff #20 #120)
+#118 := (= #19 #117)
+#103 := (= #16 #102)
+#104 := [rewrite]: #103
+#115 := (= #18 #112)
+#108 := (- #102)
+#113 := (= #108 #112)
+#114 := [rewrite]: #113
+#109 := (= #18 #108)
+#110 := [monotonicity #104]: #109
+#116 := [trans #110 #114]: #115
+#106 := (iff #17 #105)
+#107 := [monotonicity #104]: #106
+#119 := [monotonicity #107 #116 #104]: #118
+#122 := [monotonicity #119 #98]: #121
+#202 := [monotonicity #122 #199]: #201
+#100 := (iff #14 #99)
+#93 := (= #10 #92)
+#78 := (= #6 #77)
+#79 := [rewrite]: #78
+#90 := (= #9 #87)
+#83 := (- #77)
+#88 := (= #83 #87)
+#89 := [rewrite]: #88
+#84 := (= #9 #83)
+#85 := [monotonicity #79]: #84
+#91 := [trans #85 #89]: #90
+#81 := (iff #8 #80)
+#82 := [monotonicity #79]: #81
+#94 := [monotonicity #82 #91 #79]: #93
+#101 := [monotonicity #94 #98]: #100
+#205 := [monotonicity #101 #202]: #204
+#369 := [trans #205 #367]: #368
+#74 := [asserted]: #52
+#370 := [mp #74 #369]: #363
+#374 := [and-elim #370]: #221
+#373 := [and-elim #370]: #215
+#504 := (+ #96 #134)
+#514 := (<= #504 0::real)
+#635 := (not #514)
+#456 := -1/3::real
+#457 := (* -1/3::real uf_3)
+#544 := (+ #457 #111)
+#545 := (+ uf_2 #544)
+#546 := (>= #545 0::real)
+#390 := (+ #216 uf_9)
+#593 := (+ uf_3 #390)
+#603 := (<= #593 0::real)
+#381 := (+ uf_8 #206)
+#404 := (>= #381 0::real)
+#594 := (+ uf_3 #381)
+#604 := (<= #594 0::real)
+#736 := (not #604)
+#477 := (+ #96 #155)
+#487 := (<= #477 0::real)
+#733 := [hypothesis]: #604
+#564 := (+ #76 #96)
+#565 := (+ uf_1 #564)
+#577 := (<= #565 0::real)
+#767 := (or #577 #736)
+#658 := (not #577)
+#673 := [hypothesis]: #658
+#478 := (+ #96 #145)
+#488 := (<= #478 0::real)
+#628 := (not #488)
+#446 := (+ #96 #123)
+#447 := (+ uf_2 #446)
+#461 := (<= #447 0::real)
+#618 := (not #461)
+#754 := (or #224 #736)
+#625 := (not #487)
+#718 := [hypothesis]: #225
+#744 := (or #577 #736 #224)
+#681 := (or #224 #618)
+#458 := (+ #457 #123)
+#459 := (+ uf_2 #458)
+#460 := (>= #459 0::real)
+#462 := (ite #224 #460 #461)
+#467 := (not #462)
+#468 := (iff #242 #467)
+#465 := (iff #241 #462)
+#444 := (+ #96 uf_6)
+#445 := (+ #76 #444)
+#448 := (ite #224 #445 #447)
+#453 := (<= #448 0::real)
+#463 := (iff #453 #462)
+#464 := [rewrite]: #463
+#454 := (iff #241 #453)
+#451 := (= #240 #448)
+#439 := (ite #224 #175 #166)
+#441 := (+ #96 #439)
+#449 := (= #441 #448)
+#450 := [rewrite]: #449
+#442 := (= #240 #441)
+#437 := (= #239 #439)
+#440 := [rewrite]: #437
+#443 := [monotonicity #440]: #442
+#452 := [trans #443 #450]: #451
+#455 := [monotonicity #452]: #454
+#466 := [trans #455 #464]: #465
+#469 := [monotonicity #466]: #468
+#375 := [and-elim #370]: #242
+#470 := [mp #375 #469]: #467
+#619 := (or #462 #224 #618)
+#620 := [def-axiom]: #619
+#682 := [unit-resolution #620 #470]: #681
+#719 := [unit-resolution #682 #718]: #618
+#737 := (or #487 #461 #736 #577)
+#372 := [and-elim #370]: #211
+#734 := [hypothesis]: #625
+#675 := [hypothesis]: #618
+#735 := [th-lemma #675 #374 #734 #372 #733 #673]: false
+#738 := [lemma #735]: #737
+#739 := [unit-resolution #738 #673 #733 #719]: #487
+#740 := (or #248 #625)
+#489 := (ite #247 #487 #488)
+#494 := (not #489)
+#495 := (iff #265 #494)
+#492 := (iff #264 #489)
+#479 := (ite #247 #477 #478)
+#484 := (<= #479 0::real)
+#490 := (iff #484 #489)
+#491 := [rewrite]: #490
+#485 := (iff #264 #484)
+#482 := (= #263 #479)
+#471 := (ite #247 #155 #145)
+#474 := (+ #96 #471)
+#480 := (= #474 #479)
+#481 := [rewrite]: #480
+#475 := (= #263 #474)
+#472 := (= #262 #471)
+#473 := [rewrite]: #472
+#476 := [monotonicity #473]: #475
+#483 := [trans #476 #481]: #482
+#486 := [monotonicity #483]: #485
+#493 := [trans #486 #491]: #492
+#496 := [monotonicity #493]: #495
+#376 := [and-elim #370]: #265
+#497 := [mp #376 #496]: #494
+#626 := (or #489 #248 #625)
+#627 := [def-axiom]: #626
+#741 := [unit-resolution #627 #497]: #740
+#742 := [unit-resolution #741 #739]: #248
+#743 := [th-lemma #673 #719 #372 #733 #742 #718 #374]: false
+#745 := [lemma #743]: #744
+#746 := [unit-resolution #745 #718 #733]: #577
+#727 := (or #316 #658)
+#574 := (+ #76 #457)
+#575 := (+ uf_1 #574)
+#576 := (>= #575 0::real)
+#578 := (ite #316 #576 #577)
+#583 := (not #578)
+#584 := (iff #334 #583)
+#581 := (iff #333 #578)
+#562 := (+ uf_2 #96)
+#563 := (+ #86 #562)
+#566 := (ite #316 #563 #565)
+#571 := (<= #566 0::real)
+#579 := (iff #571 #578)
+#580 := [rewrite]: #579
+#572 := (iff #333 #571)
+#569 := (= #332 #566)
+#556 := (ite #316 #87 #77)
+#559 := (+ #96 #556)
+#567 := (= #559 #566)
+#568 := [rewrite]: #567
+#560 := (= #332 #559)
+#557 := (= #331 #556)
+#558 := [rewrite]: #557
+#561 := [monotonicity #558]: #560
+#570 := [trans #561 #568]: #569
+#573 := [monotonicity #570]: #572
+#582 := [trans #573 #580]: #581
+#585 := [monotonicity #582]: #584
+#379 := [and-elim #370]: #334
+#586 := [mp #379 #585]: #583
+#659 := (or #578 #316 #658)
+#660 := [def-axiom]: #659
+#728 := [unit-resolution #660 #586]: #727
+#747 := [unit-resolution #728 #746]: #316
+#748 := (not #211)
+#710 := (not #221)
+#749 := (or #247 #461 #710 #748 #736 #224 #317)
+#750 := [th-lemma]: #749
+#751 := [unit-resolution #750 #718 #374 #719 #372 #747 #733]: #247
+#752 := [unit-resolution #741 #751]: #625
+#753 := [th-lemma #719 #372 #733 #718 #747 #752 #374]: false
+#755 := [lemma #753]: #754
+#756 := [unit-resolution #755 #733]: #224
+#615 := (not #460)
+#757 := (or #225 #615)
+#616 := (or #462 #225 #615)
+#617 := [def-axiom]: #616
+#758 := [unit-resolution #617 #470]: #757
+#759 := [unit-resolution #758 #756]: #615
+#760 := (or #618 #460 #225)
+#761 := [th-lemma]: #760
+#762 := [unit-resolution #761 #759 #756]: #618
+#763 := [unit-resolution #738 #673 #733 #762]: #487
+#764 := [unit-resolution #741 #763]: #248
+#701 := (or #247 #628)
+#629 := (or #489 #247 #628)
+#630 := [def-axiom]: #629
+#702 := [unit-resolution #630 #497]: #701
+#765 := [unit-resolution #702 #764]: #628
+#766 := [th-lemma #756 #374 #372 #733 #764 #765 #673]: false
+#768 := [lemma #766]: #767
+#769 := [unit-resolution #768 #733]: #577
+#770 := [unit-resolution #728 #769]: #316
+#771 := (or #487 #710 #748 #736 #225 #317 #460)
+#772 := [th-lemma]: #771
+#773 := [unit-resolution #772 #756 #374 #759 #372 #770 #733]: #487
+#774 := (or #247 #460 #225 #710 #748 #736 #317)
+#775 := [th-lemma]: #774
+#776 := [unit-resolution #775 #756 #374 #759 #372 #770 #733]: #247
+#777 := [unit-resolution #741 #776 #773]: false
+#778 := [lemma #777]: #736
+#668 := (or #404 #604)
+#605 := (ite #404 #603 #604)
+#411 := (ite #404 #381 #390)
+#419 := (* -1::real #411)
+#420 := (+ uf_3 #419)
+#421 := (<= #420 0::real)
+#608 := (iff #421 #605)
+#595 := (ite #404 #593 #594)
+#600 := (<= #595 0::real)
+#606 := (iff #600 #605)
+#607 := [rewrite]: #606
+#601 := (iff #421 #600)
+#598 := (= #420 #595)
+#587 := (ite #404 #390 #381)
+#590 := (+ uf_3 #587)
+#596 := (= #590 #595)
+#597 := [rewrite]: #596
+#591 := (= #420 #590)
+#588 := (= #419 #587)
+#589 := [rewrite]: #588
+#592 := [monotonicity #589]: #591
+#599 := [trans #592 #597]: #598
+#602 := [monotonicity #599]: #601
+#609 := [trans #602 #607]: #608
+#53 := (- uf_8 uf_9)
+#55 := (- #53)
+#54 := (< #53 0::real)
+#56 := (ite #54 #55 #53)
+#57 := (< #56 uf_3)
+#58 := (not #57)
+#434 := (iff #58 #421)
+#384 := (< #381 0::real)
+#395 := (ite #384 #390 #381)
+#398 := (< #395 uf_3)
+#401 := (not #398)
+#432 := (iff #401 #421)
+#422 := (not #421)
+#427 := (not #422)
+#430 := (iff #427 #421)
+#431 := [rewrite]: #430
+#428 := (iff #401 #427)
+#425 := (iff #398 #422)
+#416 := (< #411 uf_3)
+#423 := (iff #416 #422)
+#424 := [rewrite]: #423
+#417 := (iff #398 #416)
+#414 := (= #395 #411)
+#405 := (not #404)
+#408 := (ite #405 #390 #381)
+#412 := (= #408 #411)
+#413 := [rewrite]: #412
+#409 := (= #395 #408)
+#406 := (iff #384 #405)
+#407 := [rewrite]: #406
+#410 := [monotonicity #407]: #409
+#415 := [trans #410 #413]: #414
+#418 := [monotonicity #415]: #417
+#426 := [trans #418 #424]: #425
+#429 := [monotonicity #426]: #428
+#433 := [trans #429 #431]: #432
+#402 := (iff #58 #401)
+#399 := (iff #57 #398)
+#396 := (= #56 #395)
+#382 := (= #53 #381)
+#383 := [rewrite]: #382
+#393 := (= #55 #390)
+#387 := (- #381)
+#391 := (= #387 #390)
+#392 := [rewrite]: #391
+#388 := (= #55 #387)
+#389 := [monotonicity #383]: #388
+#394 := [trans #389 #392]: #393
+#385 := (iff #54 #384)
+#386 := [monotonicity #383]: #385
+#397 := [monotonicity #386 #394 #383]: #396
+#400 := [monotonicity #397]: #399
+#403 := [monotonicity #400]: #402
+#435 := [trans #403 #433]: #434
+#380 := [asserted]: #58
+#436 := [mp #380 #435]: #421
+#610 := [mp #436 #609]: #605
+#661 := (not #605)
+#666 := (or #404 #604 #661)
+#667 := [def-axiom]: #666
+#669 := [unit-resolution #667 #610]: #668
+#700 := [unit-resolution #669 #778]: #404
+#664 := (or #405 #603)
+#662 := (or #405 #603 #661)
+#663 := [def-axiom]: #662
+#665 := [unit-resolution #663 #610]: #664
+#703 := [unit-resolution #665 #700]: #603
+#677 := (not #603)
+#731 := (or #677 #546)
+#648 := (not #546)
+#672 := [hypothesis]: #648
+#671 := [hypothesis]: #603
+#723 := (or #224 #677 #546)
+#689 := (or #461 #546 #677 #514)
+#687 := [hypothesis]: #635
+#371 := [and-elim #370]: #208
+#688 := [th-lemma #373 #672 #371 #671 #675 #687]: false
+#690 := [lemma #688]: #689
+#720 := [unit-resolution #690 #719 #671 #672]: #514
+#692 := (or #271 #635)
+#505 := (+ #96 #124)
+#515 := (<= #505 0::real)
+#516 := (ite #270 #514 #515)
+#521 := (not #516)
+#522 := (iff #288 #521)
+#519 := (iff #287 #516)
+#506 := (ite #270 #504 #505)
+#511 := (<= #506 0::real)
+#517 := (iff #511 #516)
+#518 := [rewrite]: #517
+#512 := (iff #287 #511)
+#509 := (= #286 #506)
+#498 := (ite #270 #134 #124)
+#501 := (+ #96 #498)
+#507 := (= #501 #506)
+#508 := [rewrite]: #507
+#502 := (= #286 #501)
+#499 := (= #285 #498)
+#500 := [rewrite]: #499
+#503 := [monotonicity #500]: #502
+#510 := [trans #503 #508]: #509
+#513 := [monotonicity #510]: #512
+#520 := [trans #513 #518]: #519
+#523 := [monotonicity #520]: #522
+#377 := [and-elim #370]: #288
+#524 := [mp #377 #523]: #521
+#636 := (or #516 #271 #635)
+#637 := [def-axiom]: #636
+#693 := [unit-resolution #637 #524]: #692
+#721 := [unit-resolution #693 #720]: #271
+#722 := [th-lemma #719 #373 #371 #671 #721 #718 #672]: false
+#724 := [lemma #722]: #723
+#725 := [unit-resolution #724 #671 #672]: #224
+#716 := (or #225 #317 #546 #677)
+#704 := [hypothesis]: #224
+#708 := [hypothesis]: #316
+#709 := (not #215)
+#711 := (or #270 #709 #317 #225 #710)
+#712 := [th-lemma]: #711
+#713 := [unit-resolution #712 #704 #374 #373 #708]: #270
+#714 := [unit-resolution #693 #713]: #635
+#715 := [th-lemma #708 #672 #371 #671 #714 #373 #704 #374]: false
+#717 := [lemma #715]: #716
+#726 := [unit-resolution #717 #725 #672 #671]: #317
+#729 := [unit-resolution #728 #726]: #658
+#698 := (or #316 #546 #677 #577)
+#674 := [hypothesis]: #317
+#685 := (or #270 #316 #577 #546 #677)
+#670 := [hypothesis]: #271
+#678 := (or #461 #316 #577 #546 #677 #270)
+#676 := [th-lemma #675 #674 #673 #672 #371 #671 #670 #373]: false
+#679 := [lemma #676]: #678
+#680 := [unit-resolution #679 #670 #673 #672 #671 #674]: #461
+#683 := [unit-resolution #682 #680]: #224
+#684 := [th-lemma #674 #673 #672 #371 #671 #670 #683 #373]: false
+#686 := [lemma #684]: #685
+#691 := [unit-resolution #686 #674 #673 #672 #671]: #270
+#694 := [unit-resolution #693 #691]: #635
+#695 := [unit-resolution #690 #694 #671 #672]: #461
+#696 := [unit-resolution #682 #695]: #224
+#697 := [th-lemma #373 #672 #371 #671 #696 #674 #673 #694]: false
+#699 := [lemma #697]: #698
+#730 := [unit-resolution #699 #729 #726 #671 #672]: false
+#732 := [lemma #730]: #731
+#705 := [unit-resolution #732 #703]: #546
+#706 := (or #293 #648)
+#531 := (+ #96 #111)
+#532 := (+ uf_2 #531)
+#543 := (<= #532 0::real)
+#547 := (ite #293 #543 #546)
+#552 := (not #547)
+#553 := (iff #311 #552)
+#550 := (iff #310 #547)
+#533 := (+ #96 uf_4)
+#534 := (+ #76 #533)
+#535 := (ite #293 #532 #534)
+#540 := (<= #535 0::real)
+#548 := (iff #540 #547)
+#549 := [rewrite]: #548
+#541 := (iff #310 #540)
+#538 := (= #309 #535)
+#525 := (ite #293 #112 #102)
+#528 := (+ #96 #525)
+#536 := (= #528 #535)
+#537 := [rewrite]: #536
+#529 := (= #309 #528)
+#526 := (= #308 #525)
+#527 := [rewrite]: #526
+#530 := [monotonicity #527]: #529
+#539 := [trans #530 #537]: #538
+#542 := [monotonicity #539]: #541
+#551 := [trans #542 #549]: #550
+#554 := [monotonicity #551]: #553
+#378 := [and-elim #370]: #311
+#555 := [mp #378 #554]: #552
+#649 := (or #547 #293 #648)
+#650 := [def-axiom]: #649
+#707 := [unit-resolution #650 #555]: #706
+#779 := [unit-resolution #707 #705]: #293
+#783 := (or #224 #270 #461)
+#780 := (not #208)
+#781 := (or #294 #709 #224 #780 #677 #270 #461)
+#782 := [th-lemma]: #781
+#784 := [unit-resolution #782 #373 #703 #779 #371]: #783
+#785 := [unit-resolution #784 #719 #718]: #270
+#786 := [unit-resolution #693 #785]: #635
+#787 := [th-lemma #718 #719 #786 #373 #371 #703 #779]: false
+#788 := [lemma #787]: #224
+#798 := (or #270 #317 #225)
+#799 := [unit-resolution #712 #374 #373]: #798
+#800 := [unit-resolution #799 #708 #788]: #270
+#801 := [unit-resolution #693 #800]: #635
+#802 := [th-lemma #708 #779 #371 #703 #788 #801 #373 #374]: false
+#803 := [lemma #802]: #317
+#804 := [unit-resolution #728 #803]: #658
+#796 := (or #316 #577)
+#789 := (or #514 #294 #225 #709 #780 #677 #577 #316)
+#790 := [th-lemma]: #789
+#791 := [unit-resolution #790 #674 #788 #371 #779 #373 #673 #703]: #514
+#792 := (or #270 #577 #316 #294 #225 #709 #780 #677)
+#793 := [th-lemma]: #792
+#794 := [unit-resolution #793 #674 #788 #371 #779 #373 #673 #703]: #270
+#795 := [unit-resolution #693 #794 #791]: false
+#797 := [lemma #795]: #796
+[unit-resolution #797 #804 #803]: false
+unsat