src/HOL/SMT/Examples/cert/z3_linarith_15.proof

+#2 := false
+#169 := 0::int
+decl uf_2 :: int
+#5 := uf_2
+#166 := -1::int
+#202 := (* -1::int uf_2)
+decl uf_1 :: int
+#4 := uf_1
+#203 := (+ uf_1 #202)
+#218 := (>= #203 0::int)
+decl uf_3 :: int
+#7 := uf_3
+#167 := (* -1::int uf_3)
+#168 := (+ uf_1 #167)
+#178 := (>= #168 0::int)
+#217 := (not #218)
+#204 := (<= #203 0::int)
+#205 := (not #204)
+#692 := [hypothesis]: #205
+#177 := (not #178)
+#693 := (or #177 #204)
+#170 := (<= #168 0::int)
+#191 := (+ uf_2 #167)
+#237 := (<= #191 0::int)
+#238 := (not #237)
+#171 := (not #170)
+#685 := [hypothesis]: #171
+#190 := (>= #191 0::int)
+#455 := (or #170 #190)
+#189 := (not #190)
+#197 := (and #171 #189)
+#354 := (not #197)
+#464 := (iff #354 #455)
+#456 := (not #455)
+#459 := (not #456)
+#462 := (iff #459 #455)
+#463 := [rewrite]: #462
+#460 := (iff #354 #459)
+#457 := (iff #197 #456)
+#458 := [rewrite]: #457
+#461 := [monotonicity #458]: #460
+#465 := [trans #461 #463]: #464
+#287 := (and #189 #217)
+#10 := (= uf_2 uf_3)
+#279 := (and #10 #217)
+#273 := (and #177 #238)
+#15 := (= uf_1 uf_3)
+#268 := (and #15 #238)
+#17 := (= uf_1 uf_2)
+#260 := (and #17 #189)
+#252 := (and #205 #238)
+#244 := (and #17 #238)
+#232 := (and #171 #217)
+#224 := (and #15 #217)
+#214 := (and #10 #205)
+#211 := (and #177 #205)
+#208 := (and #15 #205)
+#184 := (and #17 #177)
+#174 := (and #10 #171)
+#115 := (and #10 #17)
+#337 := (or #115 #174 #184 #197 #208 #211 #214 #224 #232 #244 #252 #260 #268 #273 #279 #287)
+#342 := (not #337)
+#21 := (= uf_2 uf_1)
+#27 := (= uf_3 uf_2)
+#34 := (and #27 #21)
+#23 := (< uf_3 uf_1)
+#33 := (and #10 #23)
+#35 := (or #33 #34)
+#12 := (< uf_1 uf_3)
+#32 := (and #21 #12)
+#36 := (or #32 #35)
+#8 := (< uf_2 uf_3)
+#31 := (and #8 #23)
+#37 := (or #31 #36)
+#25 := (= uf_3 uf_1)
+#19 := (< uf_2 uf_1)
+#30 := (and #19 #25)
+#38 := (or #30 #37)
+#29 := (and #19 #12)
+#39 := (or #29 #38)
+#28 := (and #27 #19)
+#40 := (or #28 #39)
+#6 := (< uf_1 uf_2)
+#26 := (and #25 #6)
+#41 := (or #26 #40)
+#24 := (and #23 #6)
+#42 := (or #24 #41)
+#13 := (< uf_3 uf_2)
+#22 := (and #13 #21)
+#43 := (or #22 #42)
+#20 := (and #13 #19)
+#44 := (or #20 #43)
+#18 := (and #17 #8)
+#45 := (or #18 #44)
+#16 := (and #15 #13)
+#46 := (or #16 #45)
+#14 := (and #12 #13)
+#47 := (or #14 #46)
+#11 := (and #6 #10)
+#48 := (or #11 #47)
+#9 := (and #6 #8)
+#49 := (or #9 #48)
+#50 := (not #49)
+#345 := (iff #50 #342)
+#118 := (or #33 #115)
+#110 := (and #12 #17)
+#121 := (or #110 #118)
+#124 := (or #31 #121)
+#102 := (and #15 #19)
+#127 := (or #102 #124)
+#96 := (and #12 #19)
+#130 := (or #96 #127)
+#93 := (and #10 #19)
+#133 := (or #93 #130)
+#86 := (and #6 #15)
+#136 := (or #86 #133)
+#78 := (and #6 #23)
+#139 := (or #78 #136)
+#75 := (and #13 #17)
+#142 := (or #75 #139)
+#145 := (or #20 #142)
+#70 := (and #8 #17)
+#148 := (or #70 #145)
+#67 := (and #13 #15)
+#151 := (or #67 #148)
+#154 := (or #14 #151)
+#157 := (or #11 #154)
+#160 := (or #9 #157)
+#163 := (not #160)
+#343 := (iff #163 #342)
+#340 := (iff #160 #337)
+#292 := (or #174 #115)
+#295 := (or #184 #292)
+#298 := (or #197 #295)
+#301 := (or #208 #298)
+#304 := (or #211 #301)
+#307 := (or #214 #304)
+#310 := (or #224 #307)
+#313 := (or #232 #310)
+#316 := (or #244 #313)
+#319 := (or #252 #316)
+#322 := (or #260 #319)
+#325 := (or #268 #322)
+#328 := (or #273 #325)
+#331 := (or #279 #328)
+#334 := (or #287 #331)
+#338 := (iff #334 #337)
+#339 := [rewrite]: #338
+#335 := (iff #160 #334)
+#332 := (iff #157 #331)
+#329 := (iff #154 #328)
+#326 := (iff #151 #325)
+#323 := (iff #148 #322)
+#320 := (iff #145 #319)
+#317 := (iff #142 #316)
+#314 := (iff #139 #313)
+#311 := (iff #136 #310)
+#308 := (iff #133 #307)
+#305 := (iff #130 #304)
+#302 := (iff #127 #301)
+#299 := (iff #124 #298)
+#296 := (iff #121 #295)
+#293 := (iff #118 #292)
+#175 := (iff #33 #174)
+#172 := (iff #23 #171)
+#173 := [rewrite]: #172
+#176 := [monotonicity #173]: #175
+#294 := [monotonicity #176]: #293
+#187 := (iff #110 #184)
+#181 := (and #177 #17)
+#185 := (iff #181 #184)
+#186 := [rewrite]: #185
+#182 := (iff #110 #181)
+#179 := (iff #12 #177)
+#180 := [rewrite]: #179
+#183 := [monotonicity #180]: #182
+#188 := [trans #183 #186]: #187
+#297 := [monotonicity #188 #294]: #296
+#200 := (iff #31 #197)
+#194 := (and #189 #171)
+#198 := (iff #194 #197)
+#199 := [rewrite]: #198
+#195 := (iff #31 #194)
+#192 := (iff #8 #189)
+#193 := [rewrite]: #192
+#196 := [monotonicity #193 #173]: #195
+#201 := [trans #196 #199]: #200
+#300 := [monotonicity #201 #297]: #299
+#209 := (iff #102 #208)
+#206 := (iff #19 #205)
+#207 := [rewrite]: #206
+#210 := [monotonicity #207]: #209
+#303 := [monotonicity #210 #300]: #302
+#212 := (iff #96 #211)
+#213 := [monotonicity #180 #207]: #212
+#306 := [monotonicity #213 #303]: #305
+#215 := (iff #93 #214)
+#216 := [monotonicity #207]: #215
+#309 := [monotonicity #216 #306]: #308
+#227 := (iff #86 #224)
+#221 := (and #217 #15)
+#225 := (iff #221 #224)
+#226 := [rewrite]: #225
+#222 := (iff #86 #221)
+#219 := (iff #6 #217)
+#220 := [rewrite]: #219
+#223 := [monotonicity #220]: #222
+#228 := [trans #223 #226]: #227
+#312 := [monotonicity #228 #309]: #311
+#235 := (iff #78 #232)
+#229 := (and #217 #171)
+#233 := (iff #229 #232)
+#234 := [rewrite]: #233
+#230 := (iff #78 #229)
+#231 := [monotonicity #220 #173]: #230
+#236 := [trans #231 #234]: #235
+#315 := [monotonicity #236 #312]: #314
+#247 := (iff #75 #244)
+#241 := (and #238 #17)
+#245 := (iff #241 #244)
+#246 := [rewrite]: #245
+#242 := (iff #75 #241)
+#239 := (iff #13 #238)
+#240 := [rewrite]: #239
+#243 := [monotonicity #240]: #242
+#248 := [trans #243 #246]: #247
+#318 := [monotonicity #248 #315]: #317
+#255 := (iff #20 #252)
+#249 := (and #238 #205)
+#253 := (iff #249 #252)
+#254 := [rewrite]: #253
+#250 := (iff #20 #249)
+#251 := [monotonicity #240 #207]: #250
+#256 := [trans #251 #254]: #255
+#321 := [monotonicity #256 #318]: #320
+#263 := (iff #70 #260)
+#257 := (and #189 #17)
+#261 := (iff #257 #260)
+#262 := [rewrite]: #261
+#258 := (iff #70 #257)
+#259 := [monotonicity #193]: #258
+#264 := [trans #259 #262]: #263
+#324 := [monotonicity #264 #321]: #323
+#271 := (iff #67 #268)
+#265 := (and #238 #15)
+#269 := (iff #265 #268)
+#270 := [rewrite]: #269
+#266 := (iff #67 #265)
+#267 := [monotonicity #240]: #266
+#272 := [trans #267 #270]: #271
+#327 := [monotonicity #272 #324]: #326
+#274 := (iff #14 #273)
+#275 := [monotonicity #180 #240]: #274
+#330 := [monotonicity #275 #327]: #329
+#282 := (iff #11 #279)
+#276 := (and #217 #10)
+#280 := (iff #276 #279)
+#281 := [rewrite]: #280
+#277 := (iff #11 #276)
+#278 := [monotonicity #220]: #277
+#283 := [trans #278 #281]: #282
+#333 := [monotonicity #283 #330]: #332
+#290 := (iff #9 #287)
+#284 := (and #217 #189)
+#288 := (iff #284 #287)
+#289 := [rewrite]: #288
+#285 := (iff #9 #284)
+#286 := [monotonicity #220 #193]: #285
+#291 := [trans #286 #289]: #290
+#336 := [monotonicity #291 #333]: #335
+#341 := [trans #336 #339]: #340
+#344 := [monotonicity #341]: #343
+#164 := (iff #50 #163)
+#161 := (iff #49 #160)
+#158 := (iff #48 #157)
+#155 := (iff #47 #154)
+#152 := (iff #46 #151)
+#149 := (iff #45 #148)
+#146 := (iff #44 #145)
+#143 := (iff #43 #142)
+#140 := (iff #42 #139)
+#137 := (iff #41 #136)
+#134 := (iff #40 #133)
+#131 := (iff #39 #130)
+#128 := (iff #38 #127)
+#125 := (iff #37 #124)
+#122 := (iff #36 #121)
+#119 := (iff #35 #118)
+#116 := (iff #34 #115)
+#73 := (iff #21 #17)
+#74 := [rewrite]: #73
+#91 := (iff #27 #10)
+#92 := [rewrite]: #91
+#117 := [monotonicity #92 #74]: #116
+#120 := [monotonicity #117]: #119
+#113 := (iff #32 #110)
+#107 := (and #17 #12)
+#111 := (iff #107 #110)
+#112 := [rewrite]: #111
+#108 := (iff #32 #107)
+#109 := [monotonicity #74]: #108
+#114 := [trans #109 #112]: #113
+#123 := [monotonicity #114 #120]: #122
+#126 := [monotonicity #123]: #125
+#105 := (iff #30 #102)
+#99 := (and #19 #15)
+#103 := (iff #99 #102)
+#104 := [rewrite]: #103
+#100 := (iff #30 #99)
+#81 := (iff #25 #15)
+#82 := [rewrite]: #81
+#101 := [monotonicity #82]: #100
+#106 := [trans #101 #104]: #105
+#129 := [monotonicity #106 #126]: #128
+#97 := (iff #29 #96)
+#98 := [rewrite]: #97
+#132 := [monotonicity #98 #129]: #131
+#94 := (iff #28 #93)
+#95 := [monotonicity #92]: #94
+#135 := [monotonicity #95 #132]: #134
+#89 := (iff #26 #86)
+#83 := (and #15 #6)
+#87 := (iff #83 #86)
+#88 := [rewrite]: #87
+#84 := (iff #26 #83)
+#85 := [monotonicity #82]: #84
+#90 := [trans #85 #88]: #89
+#138 := [monotonicity #90 #135]: #137
+#79 := (iff #24 #78)
+#80 := [rewrite]: #79
+#141 := [monotonicity #80 #138]: #140
+#76 := (iff #22 #75)
+#77 := [monotonicity #74]: #76
+#144 := [monotonicity #77 #141]: #143
+#147 := [monotonicity #144]: #146
+#71 := (iff #18 #70)
+#72 := [rewrite]: #71
+#150 := [monotonicity #72 #147]: #149
+#68 := (iff #16 #67)
+#69 := [rewrite]: #68
+#153 := [monotonicity #69 #150]: #152
+#156 := [monotonicity #153]: #155
+#159 := [monotonicity #156]: #158
+#162 := [monotonicity #159]: #161
+#165 := [monotonicity #162]: #164
+#346 := [trans #165 #344]: #345
+#66 := [asserted]: #50
+#347 := [mp #66 #346]: #342
+#355 := [not-or-elim #347]: #354
+#466 := [mp #355 #465]: #455
+#686 := [unit-resolution #466 #685]: #190
+#427 := (or #170 #189 #238)
+#350 := (not #174)
+#430 := (iff #350 #427)
+#382 := (or #189 #238)
+#414 := (or #170 #382)
+#428 := (iff #414 #427)
+#429 := [rewrite]: #428
+#425 := (iff #350 #414)
+#415 := (not #414)
+#420 := (not #415)
+#423 := (iff #420 #414)
+#424 := [rewrite]: #423
+#421 := (iff #350 #420)
+#418 := (iff #174 #415)
+#380 := (not #382)
+#411 := (and #380 #171)
+#416 := (iff #411 #415)
+#417 := [rewrite]: #416
+#412 := (iff #174 #411)
+#383 := (iff #10 #380)
+#384 := [rewrite]: #383
+#413 := [monotonicity #384]: #412
+#419 := [trans #413 #417]: #418
+#422 := [monotonicity #419]: #421
+#426 := [trans #422 #424]: #425
+#431 := [trans #426 #429]: #430
+#351 := [not-or-elim #347]: #350
+#432 := [mp #351 #431]: #427
+#687 := [unit-resolution #432 #686 #685]: #238
+#549 := (or #170 #218)
+#364 := (not #232)
+#558 := (iff #364 #549)
+#550 := (not #549)
+#553 := (not #550)
+#556 := (iff #553 #549)
+#557 := [rewrite]: #556
+#554 := (iff #364 #553)
+#551 := (iff #232 #550)
+#552 := [rewrite]: #551
+#555 := [monotonicity #552]: #554
+#559 := [trans #555 #557]: #558
+#365 := [not-or-elim #347]: #364
+#560 := [mp #365 #559]: #549
+#688 := [unit-resolution #560 #685]: #218
+#577 := (or #205 #217 #237)
+#366 := (not #244)
+#580 := (iff #366 #577)
+#385 := (or #205 #217)
+#564 := (or #237 #385)
+#578 := (iff #564 #577)
+#579 := [rewrite]: #578
+#575 := (iff #366 #564)
+#565 := (not #564)
+#570 := (not #565)
+#573 := (iff #570 #564)
+#574 := [rewrite]: #573
+#571 := (iff #366 #570)
+#568 := (iff #244 #565)
+#386 := (not #385)
+#561 := (and #386 #238)
+#566 := (iff #561 #565)
+#567 := [rewrite]: #566
+#562 := (iff #244 #561)
+#387 := (iff #17 #386)
+#388 := [rewrite]: #387
+#563 := [monotonicity #388]: #562
+#569 := [trans #563 #567]: #568
+#572 := [monotonicity #569]: #571
+#576 := [trans #572 #574]: #575
+#581 := [trans #576 #579]: #580
+#367 := [not-or-elim #347]: #366
+#582 := [mp #367 #581]: #577
+#689 := [unit-resolution #582 #688 #687]: #205
+#583 := (or #204 #237)
+#368 := (not #252)
+#592 := (iff #368 #583)
+#584 := (not #583)
+#587 := (not #584)
+#590 := (iff #587 #583)
+#591 := [rewrite]: #590
+#588 := (iff #368 #587)
+#585 := (iff #252 #584)
+#586 := [rewrite]: #585
+#589 := [monotonicity #586]: #588
+#593 := [trans #589 #591]: #592
+#369 := [not-or-elim #347]: #368
+#594 := [mp #369 #593]: #583
+#690 := [unit-resolution #594 #689 #687]: false
+#691 := [lemma #690]: #170
+#487 := (or #171 #177 #204)
+#356 := (not #208)
+#490 := (iff #356 #487)
+#467 := (or #171 #177)
+#474 := (or #204 #467)
+#488 := (iff #474 #487)
+#489 := [rewrite]: #488
+#485 := (iff #356 #474)
+#475 := (not #474)
+#480 := (not #475)
+#483 := (iff #480 #474)
+#484 := [rewrite]: #483
+#481 := (iff #356 #480)
+#478 := (iff #208 #475)
+#468 := (not #467)
+#471 := (and #468 #205)
+#476 := (iff #471 #475)
+#477 := [rewrite]: #476
+#472 := (iff #208 #471)
+#469 := (iff #15 #468)
+#470 := [rewrite]: #469
+#473 := [monotonicity #470]: #472
+#479 := [trans #473 #477]: #478
+#482 := [monotonicity #479]: #481
+#486 := [trans #482 #484]: #485
+#491 := [trans #486 #489]: #490
+#357 := [not-or-elim #347]: #356
+#492 := [mp #357 #491]: #487
+#694 := [unit-resolution #492 #691]: #693
+#695 := [unit-resolution #694 #692]: #177
+#493 := (or #178 #204)
+#358 := (not #211)
+#502 := (iff #358 #493)
+#494 := (not #493)
+#497 := (not #494)
+#500 := (iff #497 #493)
+#501 := [rewrite]: #500
+#498 := (iff #358 #497)
+#495 := (iff #211 #494)
+#496 := [rewrite]: #495
+#499 := [monotonicity #496]: #498
+#503 := [trans #499 #501]: #502
+#359 := [not-or-elim #347]: #358
+#504 := [mp #359 #503]: #493
+#696 := [unit-resolution #504 #695 #692]: false
+#697 := [lemma #696]: #204
+#698 := [hypothesis]: #177
+#449 := (or #178 #205 #217)
+#352 := (not #184)
+#452 := (iff #352 #449)
+#436 := (or #178 #385)
+#450 := (iff #436 #449)
+#451 := [rewrite]: #450
+#447 := (iff #352 #436)
+#437 := (not #436)
+#442 := (not #437)
+#445 := (iff #442 #436)
+#446 := [rewrite]: #445
+#443 := (iff #352 #442)
+#440 := (iff #184 #437)
+#433 := (and #386 #177)
+#438 := (iff #433 #437)
+#439 := [rewrite]: #438
+#434 := (iff #184 #433)
+#435 := [monotonicity #388]: #434
+#441 := [trans #435 #439]: #440
+#444 := [monotonicity #441]: #443
+#448 := [trans #444 #446]: #447
+#453 := [trans #448 #451]: #452
+#353 := [not-or-elim #347]: #352
+#454 := [mp #353 #453]: #449
+#699 := [unit-resolution #454 #698 #697]: #217
+#639 := (or #178 #237)
+#374 := (not #273)
+#648 := (iff #374 #639)
+#640 := (not #639)
+#643 := (not #640)
+#646 := (iff #643 #639)
+#647 := [rewrite]: #646
+#644 := (iff #374 #643)
+#641 := (iff #273 #640)
+#642 := [rewrite]: #641
+#645 := [monotonicity #642]: #644
+#649 := [trans #645 #647]: #648
+#375 := [not-or-elim #347]: #374
+#650 := [mp #375 #649]: #639
+#700 := [unit-resolution #650 #698]: #237
+#667 := (or #189 #218 #238)
+#376 := (not #279)
+#670 := (iff #376 #667)
+#654 := (or #218 #382)
+#668 := (iff #654 #667)
+#669 := [rewrite]: #668
+#665 := (iff #376 #654)
+#655 := (not #654)
+#660 := (not #655)
+#663 := (iff #660 #654)
+#664 := [rewrite]: #663
+#661 := (iff #376 #660)
+#658 := (iff #279 #655)
+#651 := (and #380 #217)
+#656 := (iff #651 #655)
+#657 := [rewrite]: #656
+#652 := (iff #279 #651)
+#653 := [monotonicity #384]: #652
+#659 := [trans #653 #657]: #658
+#662 := [monotonicity #659]: #661
+#666 := [trans #662 #664]: #665
+#671 := [trans #666 #669]: #670
+#377 := [not-or-elim #347]: #376
+#672 := [mp #377 #671]: #667
+#701 := [unit-resolution #672 #699 #700]: #189
+#673 := (or #190 #218)
+#378 := (not #287)
+#682 := (iff #378 #673)
+#674 := (not #673)
+#677 := (not #674)
+#680 := (iff #677 #673)
+#681 := [rewrite]: #680
+#678 := (iff #378 #677)
+#675 := (iff #287 #674)
+#676 := [rewrite]: #675
+#679 := [monotonicity #676]: #678
+#683 := [trans #679 #681]: #682
+#379 := [not-or-elim #347]: #378
+#684 := [mp #379 #683]: #673
+#702 := [unit-resolution #684 #701 #699]: false
+#703 := [lemma #702]: #178
+#704 := (or #177 #218)
+#543 := (or #171 #177 #218)
+#362 := (not #224)
+#546 := (iff #362 #543)
+#530 := (or #218 #467)
+#544 := (iff #530 #543)
+#545 := [rewrite]: #544
+#541 := (iff #362 #530)
+#531 := (not #530)
+#536 := (not #531)
+#539 := (iff #536 #530)
+#540 := [rewrite]: #539
+#537 := (iff #362 #536)
+#534 := (iff #224 #531)
+#527 := (and #468 #217)
+#532 := (iff #527 #531)
+#533 := [rewrite]: #532
+#528 := (iff #224 #527)
+#529 := [monotonicity #470]: #528
+#535 := [trans #529 #533]: #534
+#538 := [monotonicity #535]: #537
+#542 := [trans #538 #540]: #541
+#547 := [trans #542 #545]: #546
+#363 := [not-or-elim #347]: #362
+#548 := [mp #363 #547]: #543
+#705 := [unit-resolution #548 #691]: #704
+#706 := [unit-resolution #705 #703]: #218
+#707 := (or #177 #237)
+#633 := (or #171 #177 #237)
+#372 := (not #268)
+#636 := (iff #372 #633)
+#620 := (or #237 #467)
+#634 := (iff #620 #633)
+#635 := [rewrite]: #634
+#631 := (iff #372 #620)
+#621 := (not #620)
+#626 := (not #621)
+#629 := (iff #626 #620)
+#630 := [rewrite]: #629
+#627 := (iff #372 #626)
+#624 := (iff #268 #621)
+#617 := (and #468 #238)
+#622 := (iff #617 #621)
+#623 := [rewrite]: #622
+#618 := (iff #268 #617)
+#619 := [monotonicity #470]: #618
+#625 := [trans #619 #623]: #624
+#628 := [monotonicity #625]: #627
+#632 := [trans #628 #630]: #631
+#637 := [trans #632 #635]: #636
+#373 := [not-or-elim #347]: #372
+#638 := [mp #373 #637]: #633
+#708 := [unit-resolution #638 #691]: #707
+#709 := [unit-resolution #708 #703]: #237
+#611 := (or #190 #205 #217)
+#370 := (not #260)
+#614 := (iff #370 #611)
+#598 := (or #190 #385)
+#612 := (iff #598 #611)
+#613 := [rewrite]: #612
+#609 := (iff #370 #598)
+#599 := (not #598)
+#604 := (not #599)
+#607 := (iff #604 #598)
+#608 := [rewrite]: #607
+#605 := (iff #370 #604)
+#602 := (iff #260 #599)
+#595 := (and #386 #189)
+#600 := (iff #595 #599)
+#601 := [rewrite]: #600
+#596 := (iff #260 #595)
+#597 := [monotonicity #388]: #596
+#603 := [trans #597 #601]: #602
+#606 := [monotonicity #603]: #605
+#610 := [trans #606 #608]: #609
+#615 := [trans #610 #613]: #614
+#371 := [not-or-elim #347]: #370
+#616 := [mp #371 #615]: #611
+#710 := [unit-resolution #616 #706 #697]: #190
+#405 := (or #189 #205 #217 #238)
+#348 := (not #115)
+#408 := (iff #348 #405)
+#392 := (or #382 #385)
+#406 := (iff #392 #405)
+#407 := [rewrite]: #406
+#403 := (iff #348 #392)
+#393 := (not #392)
+#398 := (not #393)
+#401 := (iff #398 #392)
+#402 := [rewrite]: #401
+#399 := (iff #348 #398)
+#396 := (iff #115 #393)
+#389 := (and #380 #386)
+#394 := (iff #389 #393)
+#395 := [rewrite]: #394
+#390 := (iff #115 #389)
+#391 := [monotonicity #384 #388]: #390
+#397 := [trans #391 #395]: #396
+#400 := [monotonicity #397]: #399
+#404 := [trans #400 #402]: #403
+#409 := [trans #404 #407]: #408
+#349 := [not-or-elim #347]: #348
+#410 := [mp #349 #409]: #405
+[unit-resolution #410 #710 #709 #697 #706]: false
+unsat