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

renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on datatype.ML and datatype_rep_proofs.ML

#2 := false
decl up_54 :: bool
#126 := up_54
#317 := (not up_54)
decl up_60 :: bool
#145 := up_60
decl up_56 :: bool
#131 := up_56
#325 := (not up_56)
decl up_55 :: bool
#130 := up_55
decl up_46 :: bool
#108 := up_46
#291 := (not up_46)
decl up_35 :: bool
#81 := up_35
decl up_29 :: bool
#66 := up_29
decl up_32 :: bool
#72 := up_32
#235 := (not up_32)
decl up_34 :: bool
#77 := up_34
#243 := (not up_34)
decl up_33 :: bool
#76 := up_33
#250 := (not up_35)
#1611 := [hypothesis]: #250
decl up_24 :: bool
#54 := up_24
#209 := (not up_24)
decl up_13 :: bool
#28 := up_13
decl up_11 :: bool
#24 := up_11
#165 := (not up_11)
decl up_12 :: bool
#25 := up_12
#2327 := (or up_12 up_35)
#345 := (not up_60)
decl up_59 :: bool
#142 := up_59
decl up_19 :: bool
#40 := up_19
decl up_8 :: bool
#17 := up_8
#156 := (not up_8)
decl up_7 :: bool
#16 := up_7
#166 := (not up_12)
#1457 := [hypothesis]: #166
#2183 := (or up_7 up_12 up_35)
#155 := (not up_7)
#1612 := [hypothesis]: #155
decl up_10 :: bool
#21 := up_10
#161 := (not up_10)
decl up_20 :: bool
#44 := up_20
decl up_23 :: bool
#50 := up_23
#202 := (not up_23)
#2170 := (or up_34 up_7 up_35 up_12)
#1605 := [hypothesis]: #243
#2164 := (or up_29 up_34 up_7 up_35 up_12)
decl up_42 :: bool
#98 := up_42
#275 := (not up_42)
#226 := (not up_29)
#907 := [hypothesis]: #226
#2136 := (or up_29 up_12 up_7 up_35 up_32)
decl up_22 :: bool
#49 := up_22
#895 := [hypothesis]: #235
#1624 := (or up_29 up_22 up_12 up_32 up_35 up_7)
decl up_21 :: bool
#45 := up_21
decl up_31 :: bool
#71 := up_31
#234 := (not up_31)
decl up_9 :: bool
#20 := up_9
#201 := (not up_22)
#1456 := [hypothesis]: #201
#847 := (or #161 up_32 up_29 up_22 up_12)
#193 := (not up_20)
#1400 := [hypothesis]: up_10
#964 := (or #161 #193)
#197 := (or #193 #161)
#966 := (iff #197 #964)
#967 := [rewrite]: #966
#963 := [asserted]: #197
#970 := [mp #963 #967]: #964
#1399 := [unit-resolution #970 #1400]: #193
#500 := (or up_12 up_20 up_22 up_23)
#51 := (or up_20 up_12)
#52 := (or up_23 #51)
#53 := (or up_22 #52)
#503 := (iff #53 #500)
#491 := (or up_12 up_20)
#494 := (or up_23 #491)
#497 := (or up_22 #494)
#501 := (iff #497 #500)
#502 := [rewrite]: #501
#498 := (iff #53 #497)
#495 := (iff #52 #494)
#492 := (iff #51 #491)
#493 := [rewrite]: #492
#496 := [monotonicity #493]: #495
#499 := [monotonicity #496]: #498
#504 := [trans #499 #502]: #503
#490 := [asserted]: #53
#505 := [mp #490 #504]: #500
#900 := [unit-resolution #505 #1399 #1456 #1457]: up_23
#194 := (not up_21)
#974 := (or #161 #194)
#199 := (or #194 #161)
#976 := (iff #199 #974)
#977 := [rewrite]: #976
#973 := [asserted]: #199
#980 := [mp #973 #977]: #974
#902 := [unit-resolution #980 #1400]: #194
#574 := (or up_21 up_29 up_31 up_32)
#73 := (or up_29 up_21)
#74 := (or up_32 #73)
#75 := (or up_31 #74)
#577 := (iff #75 #574)
#565 := (or up_21 up_29)
#568 := (or up_32 #565)
#571 := (or up_31 #568)
#575 := (iff #571 #574)
#576 := [rewrite]: #575
#572 := (iff #75 #571)
#569 := (iff #74 #568)
#566 := (iff #73 #565)
#567 := [rewrite]: #566
#570 := [monotonicity #567]: #569
#573 := [monotonicity #570]: #572
#578 := [trans #573 #576]: #577
#564 := [asserted]: #75
#579 := [mp #564 #578]: #574
#851 := [unit-resolution #579 #902 #895 #907]: up_31
#1135 := (or #202 #234)
#249 := (or #234 #202)
#1137 := (iff #249 #1135)
#1138 := [rewrite]: #1137
#1134 := [asserted]: #249
#1141 := [mp #1134 #1138]: #1135
#858 := [unit-resolution #1141 #851 #900]: false
#853 := [lemma #858]: #847
#1613 := [unit-resolution #853 #907 #1456 #895 #1457]: #161
#405 := (or up_7 up_9 up_10)
#22 := (or up_10 up_7)
#23 := (or up_9 #22)
#408 := (iff #23 #405)
#399 := (or up_7 up_10)
#402 := (or up_9 #399)
#406 := (iff #402 #405)
#407 := [rewrite]: #406
#403 := (iff #23 #402)
#400 := (iff #22 #399)
#401 := [rewrite]: #400
#404 := [monotonicity #401]: #403
#409 := [trans #404 #407]: #408
#398 := [asserted]: #23
#410 := [mp #398 #409]: #405
#1614 := [unit-resolution #410 #1613 #1612]: up_9
#160 := (not up_9)
#881 := (or #160 #165)
#168 := (or #165 #160)
#882 := (iff #168 #881)
#883 := [rewrite]: #882
#879 := [asserted]: #168
#886 := [mp #879 #883]: #881
#1615 := [unit-resolution #886 #1614]: #165
#425 := (or up_11 up_13)
#29 := (or up_13 up_11)
#426 := (iff #29 #425)
#427 := [rewrite]: #426
#424 := [asserted]: #29
#430 := [mp #424 #427]: #425
#1616 := [unit-resolution #430 #1615]: up_13
#170 := (not up_13)
#1015 := (or #170 #209)
#211 := (or #209 #170)
#1017 := (iff #211 #1015)
#1018 := [rewrite]: #1017
#1014 := [asserted]: #211
#1021 := [mp #1014 #1018]: #1015
#1617 := [unit-resolution #1021 #1616]: #209
#603 := (or up_24 up_33 up_35)
#82 := (or up_33 up_24)
#83 := (or up_35 #82)
#606 := (iff #83 #603)
#597 := (or up_24 up_33)
#600 := (or up_35 #597)
#604 := (iff #600 #603)
#605 := [rewrite]: #604
#601 := (iff #83 #600)
#598 := (iff #82 #597)
#599 := [rewrite]: #598
#602 := [monotonicity #599]: #601
#607 := [trans #602 #605]: #606
#596 := [asserted]: #83
#608 := [mp #596 #607]: #603
#1618 := [unit-resolution #608 #1617 #1611]: up_33
#242 := (not up_33)
#1116 := (or #234 #242)
#245 := (or #242 #234)
#1117 := (iff #245 #1116)
#1118 := [rewrite]: #1117
#1114 := [asserted]: #245
#1121 := [mp #1114 #1118]: #1116
#1619 := [unit-resolution #1121 #1618]: #234
#1620 := [unit-resolution #579 #1619 #895 #907]: up_21
#1120 := (or #202 #242)
#246 := (or #242 #202)
#1122 := (iff #246 #1120)
#1123 := [rewrite]: #1122
#1119 := [asserted]: #246
#1126 := [mp #1119 #1123]: #1120
#1621 := [unit-resolution #1126 #1618]: #202
#1622 := [unit-resolution #505 #1621 #1456 #1457]: up_20
#195 := (or #193 #194)
#957 := [asserted]: #195
#1623 := [unit-resolution #957 #1622 #1620]: false
#1625 := [lemma #1623]: #1624
#2132 := [unit-resolution #1625 #907 #1611 #1457 #895 #1612]: up_22
#1978 := (or up_32 up_35 up_29 up_21 up_12 up_7)
#1972 := [unit-resolution #1625 #895 #907 #1457 #1611 #1612]: up_22
#1010 := (or #201 #209)
#210 := (or #209 #201)
#1012 := (iff #210 #1010)
#1013 := [rewrite]: #1012
#1009 := [asserted]: #210
#1016 := [mp #1009 #1013]: #1010
#1973 := [unit-resolution #1016 #1972]: #209
#1974 := [hypothesis]: #194
#1975 := [unit-resolution #579 #895 #907 #1974]: up_31
#1976 := [unit-resolution #1121 #1975]: #242
#1977 := [unit-resolution #608 #1976 #1973 #1611]: false
#1979 := [lemma #1977]: #1978
#2133 := [unit-resolution #1979 #907 #1611 #1457 #895 #1612]: up_21
#1682 := (or #194 up_7 up_12 up_23)
#1673 := [hypothesis]: #202
#1674 := [hypothesis]: up_21
#1675 := [unit-resolution #957 #1674]: #193
#1676 := [unit-resolution #505 #1675 #1457 #1673]: up_22
#1020 := (or #170 #201)
#212 := (or #201 #170)
#1022 := (iff #212 #1020)
#1023 := [rewrite]: #1022
#1019 := [asserted]: #212
#1026 := [mp #1019 #1023]: #1020
#1677 := [unit-resolution #1026 #1676]: #170
#1678 := [unit-resolution #980 #1674]: #161
#1679 := [unit-resolution #410 #1678 #1612]: up_9
#1680 := [unit-resolution #886 #1679]: #165
#1681 := [unit-resolution #430 #1680 #1677]: false
#1683 := [lemma #1681]: #1682
#2134 := [unit-resolution #1683 #2133 #1457 #1612]: up_23
#203 := (or #201 #202)
#983 := [asserted]: #203
#2135 := [unit-resolution #983 #2134 #2132]: false
#2137 := [lemma #2135]: #2136
#2156 := [unit-resolution #2137 #907 #1612 #1611 #1457]: up_32
#1224 := (or #235 #275)
#279 := (or #275 #235)
#1226 := (iff #279 #1224)
#1227 := [rewrite]: #1226
#1223 := [asserted]: #279
#1230 := [mp #1223 #1227]: #1224
#2157 := [unit-resolution #1230 #2156]: #275
#2158 := (or up_12 up_29 up_7 up_54)
decl up_26 :: bool
#58 := up_26
#214 := (not up_26)
decl up_15 :: bool
#31 := up_15
decl up_14 :: bool
#30 := up_14
#172 := (not up_14)
decl up_6 :: bool
#13 := up_6
decl up_5 :: bool
#12 := up_5
#150 := (not up_5)
decl up_25 :: bool
#57 := up_25
#2099 := [hypothesis]: up_5
#859 := (or #150 #155)
#158 := (or #155 #150)
#860 := (iff #158 #859)
#861 := [rewrite]: #860
#857 := [asserted]: #158
#864 := [mp #857 #861]: #859
#2100 := [unit-resolution #864 #2099]: #155
#863 := (or #150 #156)
#159 := (or #156 #150)
#865 := (iff #159 #863)
#866 := [rewrite]: #865
#862 := [asserted]: #159
#869 := [mp #862 #866]: #863
#2101 := [unit-resolution #869 #2099]: #156
#2097 := (or up_12 up_7 up_8)
#1626 := [hypothesis]: #156
#2054 := (or up_54 up_7 up_8)
decl up_16 :: bool
#34 := up_16
#1597 := [hypothesis]: #317
#1888 := (or up_16 up_8 up_7 up_54)
decl up_45 :: bool
#104 := up_45
#284 := (not up_45)
decl up_52 :: bool
#121 := up_52
#309 := (not up_52)
decl up_51 :: bool
#120 := up_51
#177 := (not up_16)
#1627 := [hypothesis]: #177
#1733 := (or up_51 up_7 up_54 up_8 up_16)
decl up_53 :: bool
#125 := up_53
#308 := (not up_51)
#1598 := [hypothesis]: #308
decl up_43 :: bool
#99 := up_43
#276 := (not up_43)
#1710 := (or up_32 up_16 up_8 up_7 up_51 up_54)
#1671 := (or up_35 up_16 up_8 up_32 up_7)
#1655 := (or #166 up_32 up_16 up_8 up_35 up_7)
#1642 := [hypothesis]: up_12
#885 := (or #160 #166)
#169 := (or #166 #160)
#887 := (iff #169 #885)
#888 := [rewrite]: #887
#884 := [asserted]: #169
#891 := [mp #884 #888]: #885
#1643 := [unit-resolution #891 #1642]: #160
#1644 := [unit-resolution #410 #1643 #1612]: up_10
#1645 := [unit-resolution #980 #1644]: #194
#167 := (or #165 #166)
#878 := [asserted]: #167
#1646 := [unit-resolution #878 #1642]: #165
#1647 := [unit-resolution #430 #1646]: up_13
#1648 := [unit-resolution #1021 #1647]: #209
#1649 := [unit-resolution #608 #1648 #1611]: up_33
#1650 := [unit-resolution #1121 #1649]: #234
decl up_18 :: bool
#39 := up_18
#185 := (not up_18)
#979 := (or #161 #185)
#200 := (or #185 #161)
#981 := (iff #200 #979)
#982 := [rewrite]: #981
#978 := [asserted]: #200
#985 := [mp #978 #982]: #979
#1651 := [unit-resolution #985 #1644]: #185
#468 := (or up_8 up_16 up_18 up_19)
#41 := (or up_16 up_8)
#42 := (or up_19 #41)
#43 := (or up_18 #42)
#471 := (iff #43 #468)
#459 := (or up_8 up_16)
#462 := (or up_19 #459)
#465 := (or up_18 #462)
#469 := (iff #465 #468)
#470 := [rewrite]: #469
#466 := (iff #43 #465)
#463 := (iff #42 #462)
#460 := (iff #41 #459)
#461 := [rewrite]: #460
#464 := [monotonicity #461]: #463
#467 := [monotonicity #464]: #466
#472 := [trans #467 #470]: #471
#458 := [asserted]: #43
#473 := [mp #458 #472]: #468
#1652 := [unit-resolution #473 #1651 #1627 #1626]: up_19
#186 := (not up_19)
#1068 := (or #186 #226)
#230 := (or #226 #186)
#1070 := (iff #230 #1068)
#1071 := [rewrite]: #1070
#1067 := [asserted]: #230
#1074 := [mp #1067 #1071]: #1068
#1653 := [unit-resolution #1074 #1652]: #226
#1654 := [unit-resolution #579 #1653 #1650 #895 #1645]: false
#1656 := [lemma #1654]: #1655
#1657 := [unit-resolution #1656 #1611 #1627 #1626 #895 #1612]: #166
#1640 := (or up_12 up_35 up_7 up_22 up_16 up_8 up_32)
#1628 := [unit-resolution #1625 #1457 #1456 #895 #1611 #1612]: up_29
#1629 := [unit-resolution #1074 #1628]: #186
#1630 := [unit-resolution #473 #1629 #1627 #1626]: up_18
#960 := (or #185 #193)
#196 := (or #193 #185)
#961 := (iff #196 #960)
#962 := [rewrite]: #961
#958 := [asserted]: #196
#965 := [mp #958 #962]: #960
#1631 := [unit-resolution #965 #1630]: #193
#1632 := [unit-resolution #505 #1631 #1456 #1457]: up_23
#1633 := [unit-resolution #1126 #1632]: #242
#1634 := [unit-resolution #608 #1633 #1611]: up_24
#1635 := [unit-resolution #985 #1630]: #161
#1636 := [unit-resolution #410 #1635 #1612]: up_9
#1637 := [unit-resolution #886 #1636]: #165
#1638 := [unit-resolution #430 #1637]: up_13
#1639 := [unit-resolution #1021 #1638 #1634]: false
#1641 := [lemma #1639]: #1640
#1658 := [unit-resolution #1641 #1657 #1612 #1611 #1627 #1626 #895]: up_22
#1659 := [unit-resolution #1016 #1658]: #209
#1660 := [unit-resolution #608 #1659 #1611]: up_33
#1661 := [unit-resolution #1121 #1660]: #234
#1662 := [unit-resolution #1026 #1658]: #170
#1663 := [unit-resolution #430 #1662]: up_11
#1664 := [unit-resolution #886 #1663]: #160
#1665 := [unit-resolution #410 #1664 #1612]: up_10
#1666 := [unit-resolution #980 #1665]: #194
#1667 := [unit-resolution #579 #1666 #895 #1661]: up_29
#1668 := [unit-resolution #985 #1665]: #185
#1669 := [unit-resolution #473 #1668 #1627 #1626]: up_19
#1670 := [unit-resolution #1074 #1669 #1667]: false
#1672 := [lemma #1670]: #1671
#1698 := [unit-resolution #1672 #895 #1626 #1627 #1612]: up_35
#1609 := (or #250 up_34 up_51 up_54)
#316 := (not up_53)
#1599 := [hypothesis]: up_35
#1275 := (or #250 #291)
#293 := (or #291 #250)
#1277 := (iff #293 #1275)
#1278 := [rewrite]: #1277
#1274 := [asserted]: #293
#1281 := [mp #1274 #1278]: #1275
#1600 := [unit-resolution #1281 #1599]: #291
#777 := (or up_46 up_55)
decl up_4 :: bool
#10 := up_4
#783 := (or up_4 up_46 up_55)
#1514 := (iff #783 #777)
#1509 := (or false up_46 up_55)
#1512 := (iff #1509 #777)
#1513 := [rewrite]: #1512
#1510 := (iff #783 #1509)
#1485 := (iff up_4 false)
#11 := (not up_4)
#1488 := (iff #11 #1485)
#1486 := (iff #1485 #11)
#1487 := [rewrite]: #1486
#1489 := [symm #1487]: #1488
#371 := [asserted]: #11
#1490 := [mp #371 #1489]: #1485
#1511 := [monotonicity #1490]: #1510
#1515 := [trans #1511 #1513]: #1514
#135 := (or up_55 up_46)
#136 := (or up_4 #135)
#786 := (iff #136 #783)
#780 := (or up_4 #777)
#784 := (iff #780 #783)
#785 := [rewrite]: #784
#781 := (iff #136 #780)
#778 := (iff #135 #777)
#779 := [rewrite]: #778
#782 := [monotonicity #779]: #781
#787 := [trans #782 #785]: #786
#776 := [asserted]: #136
#788 := [mp #776 #787]: #783
#1516 := [mp #788 #1515]: #777
#1601 := [unit-resolution #1516 #1600]: up_55
#324 := (not up_55)
#1376 := (or #316 #324)
#327 := (or #324 #316)
#1377 := (iff #327 #1376)
#1378 := [rewrite]: #1377
#1374 := [asserted]: #327
#1381 := [mp #1374 #1378]: #1376
#1602 := [unit-resolution #1381 #1601]: #316
#754 := (or up_43 up_51 up_53 up_54)
#127 := (or up_51 up_43)
#128 := (or up_54 #127)
#129 := (or up_53 #128)
#757 := (iff #129 #754)
#745 := (or up_43 up_51)
#748 := (or up_54 #745)
#751 := (or up_53 #748)
#755 := (iff #751 #754)
#756 := [rewrite]: #755
#752 := (iff #129 #751)
#749 := (iff #128 #748)
#746 := (iff #127 #745)
#747 := [rewrite]: #746
#750 := [monotonicity #747]: #749
#753 := [monotonicity #750]: #752
#758 := [trans #753 #756]: #757
#744 := [asserted]: #129
#759 := [mp #744 #758]: #754
#1603 := [unit-resolution #759 #1602 #1598 #1597]: up_43
decl up_44 :: bool
#103 := up_44
#283 := (not up_44)
#1280 := (or #250 #283)
#294 := (or #283 #250)
#1282 := (iff #294 #1280)
#1283 := [rewrite]: #1282
#1279 := [asserted]: #294
#1286 := [mp #1279 #1283]: #1280
#1604 := [unit-resolution #1286 #1599]: #283
#1380 := (or #284 #324)
#328 := (or #324 #284)
#1382 := (iff #328 #1380)
#1383 := [rewrite]: #1382
#1379 := [asserted]: #328
#1386 := [mp #1379 #1383]: #1380
#1606 := [unit-resolution #1386 #1601]: #284
#680 := (or up_34 up_42 up_44 up_45)
#105 := (or up_42 up_34)
#106 := (or up_45 #105)
#107 := (or up_44 #106)
#683 := (iff #107 #680)
#671 := (or up_34 up_42)
#674 := (or up_45 #671)
#677 := (or up_44 #674)
#681 := (iff #677 #680)
#682 := [rewrite]: #681
#678 := (iff #107 #677)
#675 := (iff #106 #674)
#672 := (iff #105 #671)
#673 := [rewrite]: #672
#676 := [monotonicity #673]: #675
#679 := [monotonicity #676]: #678
#684 := [trans #679 #682]: #683
#670 := [asserted]: #107
#685 := [mp #670 #684]: #680
#1607 := [unit-resolution #685 #1606 #1605 #1604]: up_42
#277 := (or #275 #276)
#1217 := [asserted]: #277
#1608 := [unit-resolution #1217 #1607 #1603]: false
#1610 := [lemma #1608]: #1609
#1699 := [unit-resolution #1610 #1698 #1598 #1597]: up_34
#1125 := (or #234 #243)
#247 := (or #243 #234)
#1127 := (iff #247 #1125)
#1128 := [rewrite]: #1127
#1124 := [asserted]: #247
#1131 := [mp #1124 #1128]: #1125
#1700 := [unit-resolution #1131 #1699]: #234
#1130 := (or #202 #243)
#248 := (or #243 #202)
#1132 := (iff #248 #1130)
#1133 := [rewrite]: #1132
#1129 := [asserted]: #248
#1136 := [mp #1129 #1133]: #1130
#1701 := [unit-resolution #1136 #1699]: #202
#1696 := (or up_12 up_7 up_23 up_16 up_8 up_32 up_31)
#1684 := [hypothesis]: #234
#1685 := [unit-resolution #1683 #1457 #1612 #1673]: #194
#1686 := [unit-resolution #579 #1685 #895 #1684]: up_29
#1687 := [unit-resolution #1074 #1686]: #186
#1688 := [unit-resolution #473 #1687 #1627 #1626]: up_18
#1689 := [unit-resolution #965 #1688]: #193
#1690 := [unit-resolution #505 #1689 #1457 #1673]: up_22
#1691 := [unit-resolution #1026 #1690]: #170
#1692 := [unit-resolution #985 #1688]: #161
#1693 := [unit-resolution #410 #1692 #1612]: up_9
#1694 := [unit-resolution #886 #1693]: #165
#1695 := [unit-resolution #430 #1694 #1691]: false
#1697 := [lemma #1695]: #1696
#1702 := [unit-resolution #1697 #1701 #1612 #1627 #1626 #895 #1700]: up_12
#1703 := [unit-resolution #891 #1702]: #160
#1704 := [unit-resolution #410 #1703 #1612]: up_10
#1705 := [unit-resolution #980 #1704]: #194
#1706 := [unit-resolution #579 #1705 #895 #1700]: up_29
#1707 := [unit-resolution #985 #1704]: #185
#1708 := [unit-resolution #473 #1707 #1627 #1626]: up_19
#1709 := [unit-resolution #1074 #1708 #1706]: false
#1711 := [lemma #1709]: #1710
#1712 := [unit-resolution #1711 #1598 #1626 #1612 #1627 #1597]: up_32
#1234 := (or #235 #276)
#281 := (or #276 #235)
#1236 := (iff #281 #1234)
#1237 := [rewrite]: #1236
#1233 := [asserted]: #281
#1240 := [mp #1233 #1237]: #1234
#1713 := [unit-resolution #1240 #1712]: #276
#1714 := [unit-resolution #759 #1713 #1598 #1597]: up_53
#1395 := (or #284 #316)
#331 := (or #316 #284)
#1397 := (iff #331 #1395)
#1398 := [rewrite]: #1397
#1394 := [asserted]: #331
#1401 := [mp #1394 #1398]: #1395
#1715 := [unit-resolution #1401 #1714]: #284
#1716 := [unit-resolution #1230 #1712]: #275
#1717 := [unit-resolution #1381 #1714]: #324
#1718 := [unit-resolution #1516 #1717]: up_46
#1270 := (or #283 #291)
#292 := (or #291 #283)
#1272 := (iff #292 #1270)
#1273 := [rewrite]: #1272
#1269 := [asserted]: #292
#1276 := [mp #1269 #1273]: #1270
#1719 := [unit-resolution #1276 #1718]: #283
#1720 := [unit-resolution #685 #1719 #1716 #1715]: up_34
#1721 := [unit-resolution #1136 #1720]: #202
#1722 := [unit-resolution #1281 #1718]: #250
#244 := (or #242 #243)
#1113 := [asserted]: #244
#1723 := [unit-resolution #1113 #1720]: #242
#1724 := [unit-resolution #608 #1723 #1722]: up_24
#1725 := [unit-resolution #1016 #1724]: #201
#1726 := [unit-resolution #1021 #1724]: #170
#1727 := [unit-resolution #430 #1726]: up_11
#1728 := [unit-resolution #878 #1727]: #166
#1729 := [unit-resolution #505 #1728 #1725 #1721]: up_20
#1730 := [unit-resolution #886 #1727]: #160
#1731 := [unit-resolution #410 #1730 #1612]: up_10
#1732 := [unit-resolution #970 #1731 #1729]: false
#1734 := [lemma #1732]: #1733
#1858 := [unit-resolution #1734 #1627 #1597 #1626 #1612]: up_51
#310 := (or #308 #309)
#1321 := [asserted]: #310
#1859 := [unit-resolution #1321 #1858]: #309
decl up_58 :: bool
#139 := up_58
#337 := (not up_58)
decl up_49 :: bool
#115 := up_49
#300 := (not up_49)
#1324 := (or #300 #308)
#311 := (or #308 #300)
#1325 := (iff #311 #1324)
#1326 := [rewrite]: #1325
#1322 := [asserted]: #311
#1329 := [mp #1322 #1326]: #1324
#1860 := [unit-resolution #1329 #1858]: #300
decl up_39 :: bool
#89 := up_39
#260 := (not up_39)
decl up_38 :: bool
#88 := up_38
decl up_40 :: bool
#93 := up_40
#267 := (not up_40)
decl up_41 :: bool
#94 := up_41
#268 := (not up_41)
#1328 := (or #268 #308)
#312 := (or #308 #268)
#1330 := (iff #312 #1328)
#1331 := [rewrite]: #1330
#1327 := [asserted]: #312
#1334 := [mp #1327 #1331]: #1328
#1861 := [unit-resolution #1334 #1858]: #268
#1771 := (or up_32 up_16 up_8 up_41 up_49 up_52 up_7)
#1735 := [unit-resolution #1281 #1698]: #291
#1736 := [unit-resolution #1516 #1735]: up_55
#1737 := [unit-resolution #1386 #1736]: #284
#1738 := [unit-resolution #1286 #1698]: #283
#259 := (not up_38)
decl up_50 :: bool
#116 := up_50
#301 := (not up_50)
#1739 := [hypothesis]: #309
#341 := (not up_59)
#326 := (or #324 #325)
#1373 := [asserted]: #326
#1740 := [unit-resolution #1373 #1736]: #325
#834 := (or up_56 up_60)
decl up_3 :: bool
#8 := up_3
#840 := (or up_3 up_56 up_60)
#1522 := (iff #840 #834)
#1517 := (or false up_56 up_60)
#1520 := (iff #1517 #834)
#1521 := [rewrite]: #1520
#1518 := (iff #840 #1517)
#1479 := (iff up_3 false)
#9 := (not up_3)
#1482 := (iff #9 #1479)
#1480 := (iff #1479 #9)
#1481 := [rewrite]: #1480
#1483 := [symm #1481]: #1482
#370 := [asserted]: #9
#1484 := [mp #370 #1483]: #1479
#1519 := [monotonicity #1484]: #1518
#1523 := [trans #1519 #1521]: #1522
#148 := (or up_60 up_56)
#149 := (or up_3 #148)
#843 := (iff #149 #840)
#837 := (or up_3 #834)
#841 := (iff #837 #840)
#842 := [rewrite]: #841
#838 := (iff #149 #837)
#835 := (iff #148 #834)
#836 := [rewrite]: #835
#839 := [monotonicity #836]: #838
#844 := [trans #839 #842]: #843
#833 := [asserted]: #149
#845 := [mp #833 #844]: #840
#1524 := [mp #845 #1523]: #834
#1741 := [unit-resolution #1524 #1740]: up_60
#1442 := (or #341 #345)
#346 := (or #345 #341)
#1444 := (iff #346 #1442)
#1445 := [rewrite]: #1444
#1441 := [asserted]: #346
#1448 := [mp #1441 #1445]: #1442
#1742 := [unit-resolution #1448 #1741]: #341
#814 := (or up_52 up_58 up_59)
#143 := (or up_58 up_52)
#144 := (or up_59 #143)
#817 := (iff #144 #814)
#808 := (or up_52 up_58)
#811 := (or up_59 #808)
#815 := (iff #811 #814)
#816 := [rewrite]: #815
#812 := (iff #144 #811)
#809 := (iff #143 #808)
#810 := [rewrite]: #809
#813 := [monotonicity #810]: #812
#818 := [trans #813 #816]: #817
#807 := [asserted]: #144
#819 := [mp #807 #818]: #814
#1743 := [unit-resolution #819 #1742 #1739]: up_58
#1417 := (or #301 #337)
#339 := (or #337 #301)
#1419 := (iff #339 #1417)
#1420 := [rewrite]: #1419
#1416 := [asserted]: #339
#1423 := [mp #1416 #1420]: #1417
#1744 := [unit-resolution #1423 #1743]: #301
#1745 := [hypothesis]: #300
decl up_47 :: bool
#111 := up_47
#295 := (not up_47)
decl up_48 :: bool
#112 := up_48
decl up_57 :: bool
#137 := up_57
#335 := (not up_57)
#1412 := (or #335 #337)
#338 := (or #337 #335)
#1414 := (iff #338 #1412)
#1415 := [rewrite]: #1414
#1411 := [asserted]: #338
#1418 := [mp #1411 #1415]: #1412
#1746 := [unit-resolution #1418 #1743]: #335
#790 := (or up_48 up_57)
#138 := (or up_57 up_48)
#791 := (iff #138 #790)
#792 := [rewrite]: #791
#789 := [asserted]: #138
#795 := [mp #789 #792]: #790
#1747 := [unit-resolution #795 #1746]: up_48
#296 := (not up_48)
#297 := (or #295 #296)
#1284 := [asserted]: #297
#1748 := [unit-resolution #1284 #1747]: #295
#722 := (or up_39 up_47 up_49 up_50)
#117 := (or up_47 up_39)
#118 := (or up_50 #117)
#119 := (or up_49 #118)
#725 := (iff #119 #722)
#713 := (or up_39 up_47)
#716 := (or up_50 #713)
#719 := (or up_49 #716)
#723 := (iff #719 #722)
#724 := [rewrite]: #723
#720 := (iff #119 #719)
#717 := (iff #118 #716)
#714 := (iff #117 #713)
#715 := [rewrite]: #714
#718 := [monotonicity #715]: #717
#721 := [monotonicity #718]: #720
#726 := [trans #721 #724]: #725
#712 := [asserted]: #119
#727 := [mp #712 #726]: #722
#1749 := [unit-resolution #727 #1748 #1745 #1744]: up_39
#261 := (or #259 #260)
#1165 := [asserted]: #261
#1750 := [unit-resolution #1165 #1749]: #259
#1751 := [hypothesis]: #268
decl up_30 :: bool
#67 := up_30
#227 := (not up_30)
decl up_27 :: bool
#61 := up_27
#213 := (not up_25)
decl up_37 :: bool
#85 := up_37
#255 := (not up_37)
#1291 := (or #255 #296)
#299 := (or #296 #255)
#1293 := (iff #299 #1291)
#1294 := [rewrite]: #1293
#1290 := [asserted]: #299
#1297 := [mp #1290 #1294]: #1291
#1752 := [unit-resolution #1297 #1747]: #255
decl up_36 :: bool
#84 := up_36
#254 := (not up_36)
#1177 := (or #254 #260)
#264 := (or #260 #254)
#1179 := (iff #264 #1177)
#1180 := [rewrite]: #1179
#1176 := [asserted]: #264
#1183 := [mp #1176 #1180]: #1177
#1753 := [unit-resolution #1183 #1749]: #254
#616 := (or up_26 up_36 up_37)
#86 := (or up_37 up_26)
#87 := (or up_36 #86)
#619 := (iff #87 #616)
#610 := (or up_26 up_37)
#613 := (or up_36 #610)
#617 := (iff #613 #616)
#618 := [rewrite]: #617
#614 := (iff #87 #613)
#611 := (iff #86 #610)
#612 := [rewrite]: #611
#615 := [monotonicity #612]: #614
#620 := [trans #615 #618]: #619
#609 := [asserted]: #87
#621 := [mp #609 #620]: #616
#1754 := [unit-resolution #621 #1753 #1752]: up_26
#215 := (or #213 #214)
#1024 := [asserted]: #215
#1755 := [unit-resolution #1024 #1754]: #213
decl up_28 :: bool
#62 := up_28
#219 := (not up_28)
#1182 := (or #219 #260)
#265 := (or #260 #219)
#1184 := (iff #265 #1182)
#1185 := [rewrite]: #1184
#1181 := [asserted]: #265
#1188 := [mp #1181 #1185]: #1182
#1756 := [unit-resolution #1188 #1749]: #219
decl up_17 :: bool
#35 := up_17
#178 := (not up_17)
#173 := (not up_15)
#1031 := (or #173 #214)
#217 := (or #214 #173)
#1033 := (iff #217 #1031)
#1034 := [rewrite]: #1033
#1030 := [asserted]: #217
#1037 := [mp #1030 #1034]: #1031
#1757 := [unit-resolution #1037 #1754]: #173
#1503 := (or up_14 up_15)
decl up_2 :: bool
#6 := up_2
#436 := (or up_2 up_14 up_15)
#1506 := (iff #436 #1503)
#1500 := (or false up_14 up_15)
#1504 := (iff #1500 #1503)
#1505 := [rewrite]: #1504
#1501 := (iff #436 #1500)
#1473 := (iff up_2 false)
#7 := (not up_2)
#1476 := (iff #7 #1473)
#1474 := (iff #1473 #7)
#1475 := [rewrite]: #1474
#1477 := [symm #1475]: #1476
#369 := [asserted]: #7
#1478 := [mp #369 #1477]: #1473
#1502 := [monotonicity #1478]: #1501
#1507 := [trans #1502 #1505]: #1506
#32 := (or up_15 up_2)
#33 := (or up_14 #32)
#439 := (iff #33 #436)
#429 := (or up_2 up_15)
#433 := (or up_14 #429)
#437 := (iff #433 #436)
#438 := [rewrite]: #437
#434 := (iff #33 #433)
#431 := (iff #32 #429)
#432 := [rewrite]: #431
#435 := [monotonicity #432]: #434
#440 := [trans #435 #438]: #439
#428 := [asserted]: #33
#441 := [mp #428 #440]: #436
#1508 := [mp #441 #1507]: #1503
#1758 := [unit-resolution #1508 #1757]: up_14
#917 := (or #172 #178)
#182 := (or #178 #172)
#919 := (iff #182 #917)
#920 := [rewrite]: #919
#916 := [asserted]: #182
#923 := [mp #916 #920]: #917
#1759 := [unit-resolution #923 #1758]: #178
#542 := (or up_17 up_25 up_27 up_28)
#63 := (or up_25 up_17)
#64 := (or up_28 #63)
#65 := (or up_27 #64)
#545 := (iff #65 #542)
#533 := (or up_17 up_25)
#536 := (or up_28 #533)
#539 := (or up_27 #536)
#543 := (iff #539 #542)
#544 := [rewrite]: #543
#540 := (iff #65 #539)
#537 := (iff #64 #536)
#534 := (iff #63 #533)
#535 := [rewrite]: #534
#538 := [monotonicity #535]: #537
#541 := [monotonicity #538]: #540
#546 := [trans #541 #544]: #545
#532 := [asserted]: #65
#547 := [mp #532 #546]: #542
#1760 := [unit-resolution #547 #1759 #1756 #1755]: up_27
#218 := (not up_27)
#1073 := (or #218 #227)
#231 := (or #227 #218)
#1075 := (iff #231 #1073)
#1076 := [rewrite]: #1075
#1072 := [asserted]: #231
#1079 := [mp #1072 #1076]: #1073
#1761 := [unit-resolution #1079 #1760]: #227
#648 := (or up_30 up_38 up_40 up_41)
#95 := (or up_38 up_30)
#96 := (or up_41 #95)
#97 := (or up_40 #96)
#651 := (iff #97 #648)
#639 := (or up_30 up_38)
#642 := (or up_41 #639)
#645 := (or up_40 #642)
#649 := (iff #645 #648)
#650 := [rewrite]: #649
#646 := (iff #97 #645)
#643 := (iff #96 #642)
#640 := (iff #95 #639)
#641 := [rewrite]: #640
#644 := [monotonicity #641]: #643
#647 := [monotonicity #644]: #646
#652 := [trans #647 #650]: #651
#638 := [asserted]: #97
#653 := [mp #638 #652]: #648
#1762 := [unit-resolution #653 #1761 #1751 #1750]: up_40
#1220 := (or #267 #275)
#278 := (or #275 #267)
#1221 := (iff #278 #1220)
#1222 := [rewrite]: #1221
#1218 := [asserted]: #278
#1225 := [mp #1218 #1222]: #1220
#1763 := [unit-resolution #1225 #1762]: #275
#1764 := [unit-resolution #685 #1763 #1738 #1737]: up_34
#1064 := (or #218 #226)
#229 := (or #226 #218)
#1065 := (iff #229 #1064)
#1066 := [rewrite]: #1065
#1062 := [asserted]: #229
#1069 := [mp #1062 #1066]: #1064
#1765 := [unit-resolution #1069 #1760]: #226
#1083 := (or #186 #218)
#233 := (or #218 #186)
#1085 := (iff #233 #1083)
#1086 := [rewrite]: #1085
#1082 := [asserted]: #233
#1089 := [mp #1082 #1086]: #1083
#1766 := [unit-resolution #1089 #1760]: #186
#1767 := [unit-resolution #473 #1766 #1627 #1626]: up_18
#969 := (or #185 #194)
#198 := (or #194 #185)
#971 := (iff #198 #969)
#972 := [rewrite]: #971
#968 := [asserted]: #198
#975 := [mp #968 #972]: #969
#1768 := [unit-resolution #975 #1767]: #194
#1769 := [unit-resolution #579 #1768 #895 #1765]: up_31
#1770 := [unit-resolution #1131 #1769 #1764]: false
#1772 := [lemma #1770]: #1771
#1862 := [unit-resolution #1772 #1627 #1626 #1861 #1860 #1859 #1612]: up_32
#1239 := (or #235 #267)
#282 := (or #267 #235)
#1241 := (iff #282 #1239)
#1242 := [rewrite]: #1241
#1238 := [asserted]: #282
#1245 := [mp #1238 #1242]: #1239
#1863 := [unit-resolution #1245 #1862]: #267
#1856 := (or up_12 up_52 up_49 up_41 up_16 up_8 up_7)
#1828 := [unit-resolution #1772 #1627 #1626 #1751 #1745 #1739 #1612]: up_32
#1829 := [unit-resolution #1245 #1828]: #267
#1830 := [unit-resolution #1230 #1828]: #275
#1826 := (or #170 up_41 up_40 up_16 up_8 up_49 up_12 up_52 up_42)
#1804 := [hypothesis]: up_13
#1805 := [unit-resolution #1026 #1804]: #201
#1806 := [unit-resolution #1021 #1804]: #209
#1798 := [hypothesis]: #275
#1782 := [hypothesis]: #267
#1802 := (or #242 up_42 up_52 up_49 up_41 up_40 up_16 up_8 up_12 up_22)
#1783 := [hypothesis]: up_33
#1784 := [unit-resolution #1126 #1783]: #202
#1785 := [unit-resolution #505 #1784 #1457 #1456]: up_20
#1786 := [unit-resolution #965 #1785]: #185
#1787 := [unit-resolution #473 #1786 #1627 #1626]: up_19
#1078 := (or #186 #227)
#232 := (or #227 #186)
#1080 := (iff #232 #1078)
#1081 := [rewrite]: #1080
#1077 := [asserted]: #232
#1084 := [mp #1077 #1081]: #1078
#1788 := [unit-resolution #1084 #1787]: #227
#1789 := [unit-resolution #653 #1788 #1751 #1782]: up_38
#1790 := [unit-resolution #1165 #1789]: #260
#1780 := (or #337 up_49 up_39)
#1773 := [hypothesis]: up_58
#1774 := [unit-resolution #1418 #1773]: #335
#1775 := [unit-resolution #795 #1774]: up_48
#1776 := [hypothesis]: #260
#1777 := [unit-resolution #1423 #1773]: #301
#1778 := [unit-resolution #727 #1777 #1745 #1776]: up_47
#1779 := [unit-resolution #1284 #1778 #1775]: false
#1781 := [lemma #1779]: #1780
#1791 := [unit-resolution #1781 #1790 #1745]: #337
#1792 := [unit-resolution #819 #1791 #1739]: up_59
#1793 := [unit-resolution #1448 #1792]: #345
#1794 := [unit-resolution #1524 #1793]: up_56
#1795 := [unit-resolution #1373 #1794]: #324
#1796 := [unit-resolution #1516 #1795]: up_46
#1797 := [unit-resolution #1113 #1783]: #243
#1390 := (or #284 #325)
#330 := (or #325 #284)
#1392 := (iff #330 #1390)
#1393 := [rewrite]: #1392
#1389 := [asserted]: #330
#1396 := [mp #1389 #1393]: #1390
#1799 := [unit-resolution #1396 #1794]: #284
#1800 := [unit-resolution #685 #1799 #1798 #1797]: up_44
#1801 := [unit-resolution #1276 #1800 #1796]: false
#1803 := [lemma #1801]: #1802
#1807 := [unit-resolution #1803 #1805 #1739 #1745 #1751 #1782 #1627 #1626 #1457 #1798]: #242
#1808 := [unit-resolution #608 #1807 #1806]: up_35
#1809 := [unit-resolution #1286 #1808]: #283
#1810 := [unit-resolution #1281 #1808]: #291
#1811 := [unit-resolution #1516 #1810]: up_55
#1812 := [unit-resolution #1386 #1811]: #284
#1813 := [unit-resolution #685 #1812 #1798 #1809]: up_34
#1814 := [unit-resolution #1136 #1813]: #202
#1815 := [unit-resolution #505 #1814 #1457 #1805]: up_20
#1816 := [unit-resolution #965 #1815]: #185
#1817 := [unit-resolution #473 #1816 #1627 #1626]: up_19
#1818 := [unit-resolution #1373 #1811]: #325
#1819 := [unit-resolution #1524 #1818]: up_60
#1820 := [unit-resolution #1448 #1819]: #341
#1821 := [unit-resolution #819 #1820 #1739]: up_58
#1822 := [unit-resolution #1781 #1821 #1745]: up_39
#1823 := [unit-resolution #1165 #1822]: #259
#1824 := [unit-resolution #653 #1823 #1751 #1782]: up_30
#1825 := [unit-resolution #1084 #1824 #1817]: false
#1827 := [lemma #1825]: #1826
#1831 := [unit-resolution #1827 #1457 #1829 #1627 #1626 #1745 #1751 #1739 #1830]: #170
#1832 := [unit-resolution #430 #1831]: up_11
#1833 := [unit-resolution #886 #1832]: #160
#1834 := [unit-resolution #410 #1833 #1612]: up_10
#1835 := [unit-resolution #985 #1834]: #185
#1836 := [unit-resolution #473 #1835 #1627 #1626]: up_19
#1837 := [unit-resolution #1084 #1836]: #227
#1838 := [unit-resolution #653 #1837 #1751 #1829]: up_38
#1839 := [unit-resolution #1165 #1838]: #260
#1840 := [unit-resolution #1781 #1839 #1745]: #337
#1841 := [unit-resolution #819 #1840 #1739]: up_59
#1842 := [unit-resolution #1448 #1841]: #345
#1843 := [unit-resolution #1524 #1842]: up_56
#1844 := [unit-resolution #1373 #1843]: #324
#1845 := [unit-resolution #1516 #1844]: up_46
#1846 := [unit-resolution #1281 #1845]: #250
#1847 := [unit-resolution #1396 #1843]: #284
#1848 := [unit-resolution #1276 #1845]: #283
#1849 := [unit-resolution #685 #1848 #1830 #1847]: up_34
#1850 := [unit-resolution #1113 #1849]: #242
#1851 := [unit-resolution #608 #1850 #1846]: up_24
#1852 := [unit-resolution #970 #1834]: #193
#1853 := [unit-resolution #1136 #1849]: #202
#1854 := [unit-resolution #505 #1853 #1457 #1852]: up_22
#1855 := [unit-resolution #1016 #1854 #1851]: false
#1857 := [lemma #1855]: #1856
#1864 := [unit-resolution #1857 #1859 #1860 #1861 #1627 #1626 #1612]: up_12
#1865 := [unit-resolution #891 #1864]: #160
#1866 := [unit-resolution #410 #1865 #1612]: up_10
#1867 := [unit-resolution #985 #1866]: #185
#1868 := [unit-resolution #473 #1867 #1627 #1626]: up_19
#1869 := [unit-resolution #1084 #1868]: #227
#1870 := [unit-resolution #653 #1869 #1861 #1863]: up_38
#1871 := [unit-resolution #1165 #1870]: #260
#1872 := [unit-resolution #1781 #1871 #1860]: #337
#1873 := [unit-resolution #819 #1872 #1859]: up_59
#1874 := [unit-resolution #1448 #1873]: #345
#1875 := [unit-resolution #1524 #1874]: up_56
#1876 := [unit-resolution #1396 #1875]: #284
#1877 := [unit-resolution #1230 #1862]: #275
#1878 := [unit-resolution #1373 #1875]: #324
#1879 := [unit-resolution #1516 #1878]: up_46
#1880 := [unit-resolution #1276 #1879]: #283
#1881 := [unit-resolution #685 #1880 #1877 #1876]: up_34
#1882 := [unit-resolution #878 #1864]: #165
#1883 := [unit-resolution #430 #1882]: up_13
#1884 := [unit-resolution #1021 #1883]: #209
#1885 := [unit-resolution #1281 #1879]: #250
#1886 := [unit-resolution #608 #1885 #1884]: up_33
#1887 := [unit-resolution #1113 #1886 #1881]: false
#1889 := [lemma #1887]: #1888
#2026 := [unit-resolution #1889 #1597 #1612 #1626]: up_16
#908 := (or #172 #177)
#180 := (or #177 #172)
#909 := (iff #180 #908)
#910 := [rewrite]: #909
#906 := [asserted]: #180
#913 := [mp #906 #910]: #908
#2027 := [unit-resolution #913 #2026]: #172
#2028 := [unit-resolution #1508 #2027]: up_15
#2029 := [unit-resolution #1037 #2028]: #214
#1027 := (or #173 #213)
#216 := (or #213 #173)
#1028 := (iff #216 #1027)
#1029 := [rewrite]: #1028
#1025 := [asserted]: #216
#1032 := [mp #1025 #1029]: #1027
#2030 := [unit-resolution #1032 #2028]: #213
#179 := (or #177 #178)
#905 := [asserted]: #179
#2031 := [unit-resolution #905 #2026]: #178
#1917 := (or #226 up_54 up_26 up_17 up_25)
#1890 := [hypothesis]: #214
#1891 := [hypothesis]: #213
#1892 := [hypothesis]: #178
#1893 := [hypothesis]: up_29
#1894 := [unit-resolution #1069 #1893]: #218
#1895 := [unit-resolution #547 #1894 #1892 #1891]: up_28
#1187 := (or #219 #254)
#266 := (or #254 #219)
#1189 := (iff #266 #1187)
#1190 := [rewrite]: #1189
#1186 := [asserted]: #266
#1193 := [mp #1186 #1190]: #1187
#1896 := [unit-resolution #1193 #1895]: #254
#1897 := [unit-resolution #621 #1896 #1890]: up_37
#1898 := [unit-resolution #1297 #1897]: #296
#1899 := [unit-resolution #795 #1898]: up_57
#1900 := [unit-resolution #1418 #1899]: #337
#1901 := [unit-resolution #1188 #1895]: #260
#1287 := (or #255 #295)
#298 := (or #295 #255)
#1288 := (iff #298 #1287)
#1289 := [rewrite]: #1288
#1285 := [asserted]: #298
#1292 := [mp #1285 #1289]: #1287
#1902 := [unit-resolution #1292 #1897]: #295
#1422 := (or #301 #335)
#340 := (or #335 #301)
#1424 := (iff #340 #1422)
#1425 := [rewrite]: #1424
#1421 := [asserted]: #340
#1428 := [mp #1421 #1425]: #1422
#1903 := [unit-resolution #1428 #1899]: #301
#1904 := [unit-resolution #727 #1903 #1902 #1901]: up_49
#1333 := (or #300 #309)
#313 := (or #309 #300)
#1335 := (iff #313 #1333)
#1336 := [rewrite]: #1335
#1332 := [asserted]: #313
#1339 := [mp #1332 #1336]: #1333
#1905 := [unit-resolution #1339 #1904]: #309
#1906 := [unit-resolution #819 #1905 #1900]: up_59
#1907 := [unit-resolution #1448 #1906]: #345
#1908 := [unit-resolution #1524 #1907]: up_56
#1909 := [unit-resolution #1329 #1904]: #308
#1172 := (or #219 #259)
#263 := (or #259 #219)
#1174 := (iff #263 #1172)
#1175 := [rewrite]: #1174
#1171 := [asserted]: #263
#1178 := [mp #1171 #1175]: #1172
#1910 := [unit-resolution #1178 #1895]: #259
#228 := (or #226 #227)
#1061 := [asserted]: #228
#1911 := [unit-resolution #1061 #1893]: #227
#1343 := (or #268 #300)
#315 := (or #300 #268)
#1345 := (iff #315 #1343)
#1346 := [rewrite]: #1345
#1342 := [asserted]: #315
#1349 := [mp #1342 #1346]: #1343
#1912 := [unit-resolution #1349 #1904]: #268
#1913 := [unit-resolution #653 #1912 #1911 #1910]: up_40
#1229 := (or #267 #276)
#280 := (or #276 #267)
#1231 := (iff #280 #1229)
#1232 := [rewrite]: #1231
#1228 := [asserted]: #280
#1235 := [mp #1228 #1232]: #1229
#1914 := [unit-resolution #1235 #1913]: #276
#1915 := [unit-resolution #759 #1914 #1909 #1597]: up_53
#1385 := (or #316 #325)
#329 := (or #325 #316)
#1387 := (iff #329 #1385)
#1388 := [rewrite]: #1387
#1384 := [asserted]: #329
#1391 := [mp #1384 #1388]: #1385
#1916 := [unit-resolution #1391 #1915 #1908]: false
#1918 := [lemma #1916]: #1917
#2032 := [unit-resolution #1918 #1597 #2029 #2031 #2030]: #226
#2010 := (or up_12 up_29 up_7 up_54 up_26)
#1993 := (or up_35 up_12 up_54 up_26 up_29 up_7)
#1955 := (or #170 up_54 up_26 up_29 up_12 up_35 up_7)
#1940 := [unit-resolution #1625 #1805 #907 #1457 #1611 #1612]: up_32
#1941 := [unit-resolution #1240 #1940]: #276
#1942 := [unit-resolution #1230 #1940]: #275
#1943 := [unit-resolution #608 #1806 #1611]: up_33
#1944 := [unit-resolution #1113 #1943]: #243
#1925 := (or #325 up_34 up_42)
#1919 := [hypothesis]: up_56
#1920 := [unit-resolution #1373 #1919]: #324
#1921 := [unit-resolution #1516 #1920]: up_46
#1922 := [unit-resolution #1396 #1919]: #284
#1923 := [unit-resolution #685 #1922 #1605 #1798]: up_44
#1924 := [unit-resolution #1276 #1923 #1921]: false
#1926 := [lemma #1924]: #1925
#1945 := [unit-resolution #1926 #1944 #1942]: #325
#1946 := [unit-resolution #1524 #1945]: up_60
#1947 := [unit-resolution #1448 #1946]: #341
#1938 := (or #308 up_26 up_59)
#1927 := [hypothesis]: up_51
#1928 := [unit-resolution #1329 #1927]: #300
#1929 := [hypothesis]: #341
#1930 := [unit-resolution #1321 #1927]: #309
#1931 := [unit-resolution #819 #1930 #1929]: up_58
#1932 := [unit-resolution #1781 #1931 #1928]: up_39
#1933 := [unit-resolution #1183 #1932]: #254
#1934 := [unit-resolution #1418 #1931]: #335
#1935 := [unit-resolution #795 #1934]: up_48
#1936 := [unit-resolution #1297 #1935]: #255
#1937 := [unit-resolution #621 #1936 #1933 #1890]: false
#1939 := [lemma #1937]: #1938
#1948 := [unit-resolution #1939 #1947 #1890]: #308
#1949 := [unit-resolution #759 #1948 #1941 #1597]: up_53
#1950 := [unit-resolution #1381 #1949]: #324
#1951 := [unit-resolution #1516 #1950]: up_46
#1952 := [unit-resolution #1401 #1949]: #284
#1953 := [unit-resolution #685 #1952 #1944 #1942]: up_44
#1954 := [unit-resolution #1276 #1953 #1951]: false
#1956 := [lemma #1954]: #1955
#1980 := [unit-resolution #1956 #1611 #1890 #907 #1457 #1597 #1612]: #170
#1981 := [unit-resolution #430 #1980]: up_11
#1982 := [unit-resolution #886 #1981]: #160
#1983 := [unit-resolution #410 #1982 #1612]: up_10
#1984 := [unit-resolution #980 #1983]: #194
#1985 := [unit-resolution #1979 #1611 #907 #1984 #1457 #1612]: up_32
#1970 := (or #235 up_34 up_54 up_26)
#1957 := [hypothesis]: up_32
#1958 := [unit-resolution #1240 #1957]: #276
#1959 := [unit-resolution #1230 #1957]: #275
#1960 := [unit-resolution #1926 #1959 #1605]: #325
#1961 := [unit-resolution #1524 #1960]: up_60
#1962 := [unit-resolution #1448 #1961]: #341
#1963 := [unit-resolution #1939 #1962 #1890]: #308
#1964 := [unit-resolution #759 #1963 #1958 #1597]: up_53
#1965 := [unit-resolution #1381 #1964]: #324
#1966 := [unit-resolution #1516 #1965]: up_46
#1967 := [unit-resolution #1401 #1964]: #284
#1968 := [unit-resolution #685 #1967 #1605 #1959]: up_44
#1969 := [unit-resolution #1276 #1968 #1966]: false
#1971 := [lemma #1969]: #1970
#1986 := [unit-resolution #1971 #1985 #1597 #1890]: up_34
#1987 := [unit-resolution #1113 #1986]: #242
#1988 := [unit-resolution #608 #1987 #1611]: up_24
#1989 := [unit-resolution #970 #1983]: #193
#1990 := [unit-resolution #1136 #1986]: #202
#1991 := [unit-resolution #505 #1990 #1457 #1989]: up_22
#1992 := [unit-resolution #1016 #1991 #1988]: false
#1994 := [lemma #1992]: #1993
#1995 := [unit-resolution #1994 #1457 #1597 #1890 #907 #1612]: up_35
#1996 := [unit-resolution #1281 #1995]: #291
#1997 := [unit-resolution #1516 #1996]: up_55
#1998 := [unit-resolution #1373 #1997]: #325
#1999 := [unit-resolution #1524 #1998]: up_60
#2000 := [unit-resolution #1448 #1999]: #341
#2001 := [unit-resolution #1939 #2000 #1890]: #308
#2002 := [unit-resolution #1610 #2001 #1995 #1597]: up_34
#2003 := [unit-resolution #1131 #2002]: #234
#2004 := [unit-resolution #1381 #1997]: #316
#2005 := [unit-resolution #759 #2001 #2004 #1597]: up_43
#2006 := [unit-resolution #1240 #2005]: #235
#2007 := [unit-resolution #1136 #2002]: #202
#2008 := [unit-resolution #1683 #2007 #1612 #1457]: #194
#2009 := [unit-resolution #579 #2008 #2006 #907 #2003]: false
#2011 := [lemma #2009]: #2010
#2033 := [unit-resolution #2011 #2032 #1612 #1597 #2029]: up_12
#2034 := [unit-resolution #891 #2033]: #160
#2035 := [unit-resolution #410 #2034 #1612]: up_10
#2036 := [unit-resolution #980 #2035]: #194
#2037 := [unit-resolution #878 #2033]: #165
#2038 := [unit-resolution #430 #2037]: up_13
#2039 := [unit-resolution #1021 #2038]: #209
#2024 := (or #234 up_26 up_54 up_24)
#2012 := [hypothesis]: #209
#2013 := [hypothesis]: up_31
#2014 := [unit-resolution #1121 #2013]: #242
#2015 := [unit-resolution #608 #2014 #2012]: up_35
#2016 := [unit-resolution #1131 #2013]: #243
#2017 := [unit-resolution #1610 #2016 #2015 #1597]: up_51
#2018 := [unit-resolution #1939 #2017 #1890]: up_59
#2019 := [unit-resolution #1448 #2018]: #345
#2020 := [unit-resolution #1281 #2015]: #291
#2021 := [unit-resolution #1516 #2020]: up_55
#2022 := [unit-resolution #1373 #2021]: #325
#2023 := [unit-resolution #1524 #2022 #2019]: false
#2025 := [lemma #2023]: #2024
#2040 := [unit-resolution #2025 #2029 #1597 #2039]: #234
#2041 := [unit-resolution #579 #2040 #2032 #2036]: up_32
#2042 := [unit-resolution #1240 #2041]: #276
#2043 := [unit-resolution #1971 #2041 #1597 #2029]: up_34
#2044 := [unit-resolution #1113 #2043]: #242
#2045 := [unit-resolution #608 #2044 #2039]: up_35
#2046 := [unit-resolution #1281 #2045]: #291
#2047 := [unit-resolution #1516 #2046]: up_55
#2048 := [unit-resolution #1381 #2047]: #316
#2049 := [unit-resolution #759 #2048 #2042 #1597]: up_51
#2050 := [unit-resolution #1373 #2047]: #325
#2051 := [unit-resolution #1524 #2050]: up_60
#2052 := [unit-resolution #1448 #2051]: #341
#2053 := [unit-resolution #1939 #2052 #2049 #2029]: false
#2055 := [lemma #2053]: #2054
#2065 := [unit-resolution #2055 #1612 #1626]: up_54
#1447 := (or #317 #345)
#347 := (or #345 #317)
#1449 := (iff #347 #1447)
#1450 := [rewrite]: #1449
#1446 := [asserted]: #347
#1453 := [mp #1446 #1450]: #1447
#2066 := [unit-resolution #1453 #2065]: #345
#2067 := [unit-resolution #1524 #2066]: up_56
#2083 := (or #275 up_7 up_12 up_8)
#2063 := [hypothesis]: up_42
#2064 := [unit-resolution #1230 #2063]: #235
#2068 := [unit-resolution #1373 #2067]: #324
#2069 := [unit-resolution #1516 #2068]: up_46
#2070 := [unit-resolution #1281 #2069]: #250
#2071 := [unit-resolution #1672 #2064 #1626 #2070 #1612]: up_16
#2072 := [unit-resolution #913 #2071]: #172
#2073 := [unit-resolution #1508 #2072]: up_15
#2074 := [unit-resolution #1032 #2073]: #213
#2075 := [unit-resolution #905 #2071]: #178
#1452 := (or #317 #341)
#348 := (or #341 #317)
#1454 := (iff #348 #1452)
#1455 := [rewrite]: #1454
#1451 := [asserted]: #348
#1458 := [mp #1451 #1455]: #1452
#2076 := [unit-resolution #1458 #2065]: #341
#2077 := [unit-resolution #1225 #2063]: #267
#2061 := (or #226 up_59 up_40 up_17 up_25)
#2056 := [unit-resolution #653 #1910 #1782 #1911]: up_41
#2057 := [unit-resolution #1349 #2056]: #300
#1338 := (or #268 #309)
#314 := (or #309 #268)
#1340 := (iff #314 #1338)
#1341 := [rewrite]: #1340
#1337 := [asserted]: #314
#1344 := [mp #1337 #1341]: #1338
#2058 := [unit-resolution #1344 #2056]: #309
#2059 := [unit-resolution #819 #2058 #1929]: up_58
#2060 := [unit-resolution #1781 #2059 #2057 #1901]: false
#2062 := [lemma #2060]: #2061
#2078 := [unit-resolution #2062 #2077 #2076 #2075 #2074]: #226
#2079 := [unit-resolution #1625 #2078 #2070 #1457 #2064 #1612]: up_22
#2080 := [unit-resolution #1979 #2078 #2070 #1457 #2064 #1612]: up_21
#2081 := [unit-resolution #1683 #2080 #1612 #1457]: up_23
#2082 := [unit-resolution #983 #2081 #2079]: false
#2084 := [lemma #2082]: #2083
#2085 := [unit-resolution #2084 #1457 #1612 #1626]: #275
#2086 := [unit-resolution #1926 #2085 #2067]: up_34
#2087 := [unit-resolution #1136 #2086]: #202
#2088 := [unit-resolution #1113 #2086]: #242
#2089 := [unit-resolution #608 #2088 #2070]: up_24
#2090 := [unit-resolution #1016 #2089]: #201
#2091 := [unit-resolution #505 #2090 #1457 #2087]: up_20
#2092 := [unit-resolution #970 #2091]: #161
#2093 := [unit-resolution #1021 #2089]: #170
#2094 := [unit-resolution #430 #2093]: up_11
#2095 := [unit-resolution #886 #2094]: #160
#2096 := [unit-resolution #410 #2095 #2092 #1612]: false
#2098 := [lemma #2096]: #2097
#2102 := [unit-resolution #2098 #2100 #2101]: up_12
#2103 := [unit-resolution #891 #2102]: #160
#2104 := [unit-resolution #410 #2103 #2100]: up_10
#2105 := [unit-resolution #980 #2104]: #194
#2106 := [unit-resolution #2055 #2100 #2101]: up_54
#2107 := [unit-resolution #1453 #2106]: #345
#2108 := [unit-resolution #1524 #2107]: up_56
#2109 := [unit-resolution #1373 #2108]: #324
#2110 := [unit-resolution #1516 #2109]: up_46
#2111 := [unit-resolution #1281 #2110]: #250
#2112 := [unit-resolution #878 #2102]: #165
#2113 := [unit-resolution #430 #2112]: up_13
#2114 := [unit-resolution #1021 #2113]: #209
#2115 := [unit-resolution #608 #2114 #2111]: up_33
#2116 := [unit-resolution #1121 #2115]: #234
#2117 := [unit-resolution #1276 #2110]: #283
#2118 := [unit-resolution #1396 #2108]: #284
#2119 := [unit-resolution #1113 #2115]: #243
#2120 := [unit-resolution #685 #2119 #2118 #2117]: up_42
#2121 := [unit-resolution #1230 #2120]: #235
#2122 := [unit-resolution #579 #2121 #2116 #2105]: up_29
#2123 := [unit-resolution #1225 #2120]: #267
#2124 := [unit-resolution #1458 #2106]: #341
#2125 := [unit-resolution #1672 #2121 #2101 #2111 #2100]: up_16
#2126 := [unit-resolution #905 #2125]: #178
#2127 := [unit-resolution #2062 #2126 #2124 #2123 #2122]: up_25
#2128 := [unit-resolution #913 #2125]: #172
#2129 := [unit-resolution #1508 #2128]: up_15
#2130 := [unit-resolution #1032 #2129 #2127]: false
#2131 := [lemma #2130]: #150
#1494 := (or up_5 up_6)
decl up_1 :: bool
#4 := up_1
#379 := (or up_1 up_5 up_6)
#1497 := (iff #379 #1494)
#1491 := (or false up_5 up_6)
#1495 := (iff #1491 #1494)
#1496 := [rewrite]: #1495
#1492 := (iff #379 #1491)
#1467 := (iff up_1 false)
#5 := (not up_1)
#1470 := (iff #5 #1467)
#1463 := (iff #1467 #5)
#1468 := [rewrite]: #1463
#1471 := [symm #1468]: #1470
#368 := [asserted]: #5
#1472 := [mp #368 #1471]: #1467
#1493 := [monotonicity #1472]: #1492
#1498 := [trans #1493 #1496]: #1497
#14 := (or up_6 up_1)
#15 := (or up_5 #14)
#382 := (iff #15 #379)
#373 := (or up_1 up_6)
#376 := (or up_5 #373)
#380 := (iff #376 #379)
#381 := [rewrite]: #380
#377 := (iff #15 #376)
#374 := (iff #14 #373)
#375 := [rewrite]: #374
#378 := [monotonicity #375]: #377
#383 := [trans #378 #381]: #382
#372 := [asserted]: #15
#384 := [mp #372 #383]: #379
#1499 := [mp #384 #1498]: #1494
#2138 := [unit-resolution #1499 #2131]: up_6
#151 := (not up_6)
#927 := (or #151 #172)
#184 := (or #172 #151)
#929 := (iff #184 #927)
#930 := [rewrite]: #929
#926 := [asserted]: #184
#933 := [mp #926 #930]: #927
#2139 := [unit-resolution #933 #2138]: #172
#2140 := [unit-resolution #1508 #2139]: up_15
#2147 := [unit-resolution #1037 #2140]: #214
#2159 := [unit-resolution #2011 #2147]: #2158
#2160 := [unit-resolution #2159 #907 #1612 #1457]: up_54
#2161 := [unit-resolution #1453 #2160]: #345
#2162 := [unit-resolution #1524 #2161]: up_56
#2163 := [unit-resolution #1926 #2162 #2157 #1605]: false
#2165 := [lemma #2163]: #2164
#2166 := [unit-resolution #2165 #1605 #1612 #1611 #1457]: up_29
#2148 := (or #226 up_54)
#2141 := [unit-resolution #1032 #2140]: #213
#922 := (or #151 #178)
#183 := (or #178 #151)
#924 := (iff #183 #922)
#925 := [rewrite]: #924
#921 := [asserted]: #183
#928 := [mp #921 #925]: #922
#2142 := [unit-resolution #928 #2138]: #178
#2149 := [unit-resolution #1918 #2147 #2142 #2141]: #2148
#2167 := [unit-resolution #2149 #2166]: up_54
#2154 := (or #226 up_34 up_59)
#2143 := (or #226 up_59 up_40)
#2144 := [unit-resolution #2062 #2142 #2141]: #2143
#2145 := [unit-resolution #2144 #1893 #1929]: up_40
#2146 := [unit-resolution #1225 #2145]: #275
#2150 := [unit-resolution #2149 #1893]: up_54
#2151 := [unit-resolution #1453 #2150]: #345
#2152 := [unit-resolution #1524 #2151]: up_56
#2153 := [unit-resolution #1926 #2152 #2146 #1605]: false
#2155 := [lemma #2153]: #2154
#2168 := [unit-resolution #2155 #2166 #1605]: up_59
#2169 := [unit-resolution #1458 #2168 #2167]: false
#2171 := [lemma #2169]: #2170
#2172 := [unit-resolution #2171 #1612 #1611 #1457]: up_34
#2173 := [unit-resolution #1136 #2172]: #202
#2174 := [unit-resolution #1113 #2172]: #242
#2175 := [unit-resolution #608 #2174 #1611]: up_24
#2176 := [unit-resolution #1016 #2175]: #201
#2177 := [unit-resolution #505 #2176 #1457 #2173]: up_20
#2178 := [unit-resolution #970 #2177]: #161
#2179 := [unit-resolution #1021 #2175]: #170
#2180 := [unit-resolution #430 #2179]: up_11
#2181 := [unit-resolution #886 #2180]: #160
#2182 := [unit-resolution #410 #2181 #2178 #1612]: false
#2184 := [lemma #2182]: #2183
#2235 := [unit-resolution #2184 #1457 #1611]: up_7
#157 := (or #155 #156)
#856 := [asserted]: #157
#2236 := [unit-resolution #856 #2235]: #156
#2299 := (or up_34 up_35 up_12)
#2283 := (or #186 up_34)
#2185 := [hypothesis]: up_19
#2191 := [unit-resolution #1084 #2185]: #227
#2186 := [unit-resolution #1089 #2185]: #218
#2187 := (or up_27 up_28)
#2188 := [unit-resolution #547 #2142 #2141]: #2187
#2189 := [unit-resolution #2188 #2186]: up_28
#2192 := [unit-resolution #1178 #2189]: #259
#2265 := [unit-resolution #1193 #2189]: #254
#2266 := (or up_36 up_37)
#2267 := [unit-resolution #621 #2147]: #2266
#2268 := [unit-resolution #2267 #2265]: up_37
#2269 := [unit-resolution #1292 #2268]: #295
#2190 := [unit-resolution #1188 #2189]: #260
#2270 := [unit-resolution #1297 #2268]: #296
#2271 := [unit-resolution #795 #2270]: up_57
#2272 := [unit-resolution #1428 #2271]: #301
#2273 := [unit-resolution #727 #2272 #2190 #2269]: up_49
#2274 := [unit-resolution #1349 #2273]: #268
#2275 := [unit-resolution #653 #2274 #2192 #2191]: up_40
#2276 := [unit-resolution #1225 #2275]: #275
#2277 := [unit-resolution #1418 #2271]: #337
#2278 := [unit-resolution #1339 #2273]: #309
#2279 := [unit-resolution #819 #2278 #2277]: up_59
#2280 := [unit-resolution #1448 #2279]: #345
#2281 := [unit-resolution #1524 #2280]: up_56
#2282 := [unit-resolution #1926 #2281 #2276 #1605]: false
#2284 := [lemma #2282]: #2283
#2292 := [unit-resolution #2284 #1605]: #186
#2223 := (or up_8 up_18 up_19)
#912 := (or #151 #177)
#181 := (or #177 #151)
#914 := (iff #181 #912)
#915 := [rewrite]: #914
#911 := [asserted]: #181
#918 := [mp #911 #915]: #912
#2222 := [unit-resolution #918 #2138]: #177
#2224 := [unit-resolution #473 #2222]: #2223
#2293 := [unit-resolution #2224 #2292 #2236]: up_18
#2257 := (or #235 up_34)
#2252 := (or #235 up_34 up_54)
#2253 := [unit-resolution #1971 #2147]: #2252
#2254 := [unit-resolution #2253 #1957 #1605]: up_54
#2255 := [unit-resolution #1453 #2254]: #345
#2256 := [unit-resolution #1524 #2255 #1960]: false
#2258 := [lemma #2256]: #2257
#2294 := [unit-resolution #2258 #1605]: #235
#2290 := (or up_29 up_35 up_32 up_12 #185)
#2200 := [hypothesis]: up_18
#2206 := (or #185 up_29 up_32 up_12 up_22)
#2201 := [unit-resolution #965 #2200]: #193
#2202 := [unit-resolution #505 #2201 #1457 #1456]: up_23
#2203 := [unit-resolution #975 #2200]: #194
#2204 := [unit-resolution #579 #2203 #907 #895]: up_31
#2205 := [unit-resolution #1141 #2204 #2202]: false
#2207 := [lemma #2205]: #2206
#2285 := [unit-resolution #2207 #907 #895 #1457 #2200]: up_22
#2286 := [unit-resolution #1016 #2285]: #209
#2287 := [unit-resolution #579 #907 #895 #2203]: up_31
#2288 := [unit-resolution #1121 #2287]: #242
#2289 := [unit-resolution #608 #2288 #2286 #1611]: false
#2291 := [lemma #2289]: #2290
#2295 := [unit-resolution #2291 #2294 #1611 #1457 #2293]: up_29
#2296 := [unit-resolution #2149 #2295]: up_54
#2297 := [unit-resolution #2155 #2295 #1605]: up_59
#2298 := [unit-resolution #1458 #2297 #2296]: false
#2300 := [lemma #2298]: #2299
#2301 := [unit-resolution #2300 #1457 #1611]: up_34
#2302 := [unit-resolution #1136 #2301]: #202
#2303 := [unit-resolution #1113 #2301]: #242
#2304 := [unit-resolution #608 #2303 #1611]: up_24
#2305 := [unit-resolution #1016 #2304]: #201
#2306 := [unit-resolution #505 #2305 #1457 #2302]: up_20
#2307 := [unit-resolution #965 #2306]: #185
#2308 := [unit-resolution #2224 #2307 #2236]: up_19
#2309 := [unit-resolution #957 #2306]: #194
#2310 := [unit-resolution #1131 #2301]: #234
#2311 := [unit-resolution #1074 #2308]: #226
#2312 := [unit-resolution #579 #2311 #2310 #2309]: up_32
#2313 := [unit-resolution #1245 #2312]: #267
#2198 := (or #186 up_59 up_40)
#2193 := [unit-resolution #653 #2192 #1782 #2191]: up_41
#2194 := [unit-resolution #1349 #2193]: #300
#2195 := [unit-resolution #1344 #2193]: #309
#2196 := [unit-resolution #819 #2195 #1929]: up_58
#2197 := [unit-resolution #1781 #2196 #2194 #2190]: false
#2199 := [lemma #2197]: #2198
#2314 := [unit-resolution #2199 #2313 #2308]: up_59
#2315 := [unit-resolution #1448 #2314]: #345
#2316 := [unit-resolution #1524 #2315]: up_56
#2317 := [unit-resolution #1084 #2308]: #227
#2318 := [unit-resolution #1089 #2308]: #218
#2319 := [unit-resolution #2188 #2318]: up_28
#2320 := [unit-resolution #1178 #2319]: #259
#2321 := [unit-resolution #653 #2313 #2320 #2317]: up_41
#2322 := [unit-resolution #1334 #2321]: #308
#2323 := [unit-resolution #1240 #2312]: #276
#2324 := [unit-resolution #1458 #2314]: #317
#2325 := [unit-resolution #759 #2324 #2323 #2322]: up_53
#2326 := [unit-resolution #1391 #2325 #2316]: false
#2328 := [lemma #2326]: #2327
#2337 := [unit-resolution #2328 #1611]: up_12
#2338 := [unit-resolution #878 #2337]: #165
#2339 := [unit-resolution #430 #2338]: up_13
#2340 := [unit-resolution #1021 #2339]: #209
#2341 := [unit-resolution #608 #2340 #1611]: up_33
#2342 := [unit-resolution #1113 #2341]: #243
#2343 := [unit-resolution #2258 #2342]: #235
#2344 := [unit-resolution #1121 #2341]: #234
#2345 := [unit-resolution #2284 #2342]: #186
#2346 := [unit-resolution #891 #2337]: #160
#2335 := (or #194 up_9 up_19)
#2329 := [hypothesis]: #186
#2330 := [unit-resolution #975 #1674]: #185
#2331 := [unit-resolution #2224 #2330 #2329]: up_8
#2332 := [hypothesis]: #160
#2333 := [unit-resolution #410 #1678 #2332]: up_7
#2334 := [unit-resolution #856 #2333 #2331]: false
#2336 := [lemma #2334]: #2335
#2347 := [unit-resolution #2336 #2346 #2345]: #194
#2348 := [unit-resolution #579 #2347 #2344 #2343]: up_29
#2349 := [unit-resolution #2149 #2348]: up_54
#2350 := [unit-resolution #2155 #2348 #2342]: up_59
#2351 := [unit-resolution #1458 #2350 #2349]: false
#2352 := [lemma #2351]: up_35
#2353 := [unit-resolution #1281 #2352]: #291
#2354 := [unit-resolution #1516 #2353]: up_55
#2355 := [unit-resolution #1373 #2354]: #325
#2356 := [unit-resolution #1524 #2355]: up_60
#2357 := [unit-resolution #1453 #2356]: #317
#2358 := [unit-resolution #2149 #2357]: #226
#2359 := [unit-resolution #1448 #2356]: #341
#2217 := (or #308 up_59)
#2218 := [unit-resolution #1939 #2147]: #2217
#2360 := [unit-resolution #2218 #2359]: #308
#2361 := [unit-resolution #1381 #2354]: #316
#2362 := [unit-resolution #759 #2357 #2361 #2360]: up_43
#2363 := [unit-resolution #1235 #2362]: #267
#2364 := [unit-resolution #2199 #2363 #2359]: #186
#1145 := (or #209 #250)
#252 := (or #250 #209)
#1147 := (iff #252 #1145)
#1148 := [rewrite]: #1147
#1144 := [asserted]: #252
#1151 := [mp #1144 #1148]: #1145
#2365 := [unit-resolution #1151 #2352]: #209
#2230 := (or #234 up_54 up_24)
#2231 := [unit-resolution #2025 #2147]: #2230
#2366 := [unit-resolution #2231 #2357 #2365]: #234
#2367 := [unit-resolution #1240 #2362]: #235
#2368 := [unit-resolution #579 #2367 #2366 #2358]: up_21
#2369 := [unit-resolution #2336 #2368 #2364]: up_9
#870 := (or #155 #160)
#163 := (or #160 #155)
#871 := (iff #163 #870)
#872 := [rewrite]: #871
#868 := [asserted]: #163
#875 := [mp #868 #872]: #870
#2370 := [unit-resolution #875 #2369]: #155
#2371 := [unit-resolution #891 #2369]: #166
[unit-resolution #2159 #2371 #2370 #2358 #2357]: false
unsat