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

removed legacy asm_lr

#2 := false
#6 := 0::int
decl z3name!0 :: int
#647 := z3name!0
#81 := -1::int
#656 := (* -1::int z3name!0)
decl uf_2 :: int
#5 := uf_2
#882 := (+ uf_2 #656)
#883 := (<= #882 0::int)
#885 := (not #883)
#881 := (>= #882 0::int)
#884 := (not #881)
#886 := (or #884 #885)
decl uf_11 :: int
#55 := uf_11
#513 := (* -1::int uf_11)
#514 := (+ uf_2 #513)
#515 := (<= #514 0::int)
decl z3name!5 :: int
#777 := z3name!5
decl uf_7 :: int
#31 := uf_7
#1083 := (+ uf_7 z3name!5)
#1084 := (<= #1083 0::int)
#335 := (>= uf_7 0::int)
#1085 := (>= #1083 0::int)
#1087 := (not #1085)
#1086 := (not #1084)
#1088 := (or #1086 #1087)
#2302 := [hypothesis]: #1086
#1289 := (or #1088 #1084)
#1290 := [def-axiom]: #1289
#2303 := [unit-resolution #1290 #2302]: #1088
#1089 := (not #1088)
#1092 := (or #335 #1089)
#1099 := (not #1092)
#786 := (* -1::int z3name!5)
#1072 := (+ uf_7 #786)
#1073 := (<= #1072 0::int)
#1075 := (not #1073)
#1071 := (>= #1072 0::int)
#1074 := (not #1071)
#1076 := (or #1074 #1075)
#1077 := (not #1076)
#336 := (not #335)
#1080 := (or #336 #1077)
#1098 := (not #1080)
#1100 := (or #1098 #1099)
#1101 := (not #1100)
#318 := (* -1::int uf_7)
#780 := (= z3name!5 #318)
#781 := (or #335 #780)
#778 := (= z3name!5 uf_7)
#779 := (or #336 #778)
#782 := (and #779 #781)
#1104 := (iff #782 #1101)
#1095 := (and #1080 #1092)
#1102 := (iff #1095 #1101)
#1103 := [rewrite]: #1102
#1096 := (iff #782 #1095)
#1093 := (iff #781 #1092)
#1090 := (iff #780 #1089)
#1091 := [rewrite]: #1090
#1094 := [monotonicity #1091]: #1093
#1081 := (iff #779 #1080)
#1078 := (iff #778 #1077)
#1079 := [rewrite]: #1078
#1082 := [monotonicity #1079]: #1081
#1097 := [monotonicity #1082 #1094]: #1096
#1105 := [trans #1097 #1103]: #1104
#783 := [intro-def]: #782
#1106 := [mp #783 #1105]: #1101
#1108 := [not-or-elim #1106]: #1092
#2304 := [unit-resolution #1108 #2303]: #335
decl uf_4 :: int
#13 := uf_4
#194 := (>= uf_4 0::int)
decl uf_10 :: int
#49 := uf_10
#459 := (* -1::int uf_10)
decl uf_3 :: int
#10 := uf_3
#508 := (+ uf_3 #459)
#509 := (>= #508 0::int)
decl z3name!1 :: int
#673 := z3name!1
#682 := (* -1::int z3name!1)
decl uf_1 :: int
#4 := uf_1
#920 := (+ uf_1 #682)
#921 := (<= #920 0::int)
#931 := (+ uf_1 z3name!1)
#933 := (>= #931 0::int)
#935 := (not #933)
#932 := (<= #931 0::int)
#934 := (not #932)
#936 := (or #934 #935)
#937 := (not #936)
#147 := (>= uf_1 0::int)
#148 := (not #147)
#923 := (not #921)
#919 := (>= #920 0::int)
#922 := (not #919)
#924 := (or #922 #923)
#2022 := [hypothesis]: #923
#1237 := (or #924 #921)
#1238 := [def-axiom]: #1237
#2023 := [unit-resolution #1238 #2022]: #924
#925 := (not #924)
#928 := (or #148 #925)
#940 := (or #147 #937)
#947 := (not #940)
#946 := (not #928)
#948 := (or #946 #947)
#949 := (not #948)
#130 := (* -1::int uf_1)
#676 := (= z3name!1 #130)
#677 := (or #147 #676)
#674 := (= z3name!1 uf_1)
#675 := (or #148 #674)
#678 := (and #675 #677)
#952 := (iff #678 #949)
#943 := (and #928 #940)
#950 := (iff #943 #949)
#951 := [rewrite]: #950
#944 := (iff #678 #943)
#941 := (iff #677 #940)
#938 := (iff #676 #937)
#939 := [rewrite]: #938
#942 := [monotonicity #939]: #941
#929 := (iff #675 #928)
#926 := (iff #674 #925)
#927 := [rewrite]: #926
#930 := [monotonicity #927]: #929
#945 := [monotonicity #930 #942]: #944
#953 := [trans #945 #951]: #952
#679 := [intro-def]: #678
#954 := [mp #679 #953]: #949
#955 := [not-or-elim #954]: #928
#2024 := [unit-resolution #955 #2023]: #148
#956 := [not-or-elim #954]: #940
#2025 := [unit-resolution #956 #2024]: #937
#2026 := (or #921 #919)
#2027 := [th-lemma]: #2026
#2028 := [unit-resolution #2027 #2022]: #919
#2029 := (or #922 #147 #935)
#2030 := [th-lemma]: #2029
#2031 := [unit-resolution #2030 #2024 #2028]: #935
#1243 := (or #936 #933)
#1244 := [def-axiom]: #1243
#2032 := [unit-resolution #1244 #2031 #2025]: false
#2033 := [lemma #2032]: #921
decl z3name!7 :: int
#829 := z3name!7
decl uf_9 :: int
#43 := uf_9
#1159 := (+ uf_9 z3name!7)
#1160 := (<= #1159 0::int)
#838 := (* -1::int z3name!7)
#1148 := (+ uf_9 #838)
#1147 := (>= #1148 0::int)
decl z3name!4 :: int
#751 := z3name!4
#760 := (* -1::int z3name!4)
decl uf_6 :: int
#25 := uf_6
#1034 := (+ uf_6 #760)
#1033 := (>= #1034 0::int)
#1035 := (<= #1034 0::int)
#1037 := (not #1035)
#1036 := (not #1033)
#1038 := (or #1036 #1037)
#1039 := (not #1038)
#288 := (>= uf_6 0::int)
#893 := (+ uf_2 z3name!0)
#895 := (>= #893 0::int)
#897 := (not #895)
#894 := (<= #893 0::int)
#896 := (not #894)
#898 := (or #896 #897)
#899 := (not #898)
#100 := (>= uf_2 0::int)
#101 := (not #100)
#1736 := [hypothesis]: #885
#1225 := (or #886 #883)
#1226 := [def-axiom]: #1225
#1737 := [unit-resolution #1226 #1736]: #886
#887 := (not #886)
#890 := (or #101 #887)
#902 := (or #100 #899)
#909 := (not #902)
#908 := (not #890)
#910 := (or #908 #909)
#911 := (not #910)
#82 := (* -1::int uf_2)
#650 := (= z3name!0 #82)
#651 := (or #100 #650)
#648 := (= z3name!0 uf_2)
#649 := (or #101 #648)
#652 := (and #649 #651)
#914 := (iff #652 #911)
#905 := (and #890 #902)
#912 := (iff #905 #911)
#913 := [rewrite]: #912
#906 := (iff #652 #905)
#903 := (iff #651 #902)
#900 := (iff #650 #899)
#901 := [rewrite]: #900
#904 := [monotonicity #901]: #903
#891 := (iff #649 #890)
#888 := (iff #648 #887)
#889 := [rewrite]: #888
#892 := [monotonicity #889]: #891
#907 := [monotonicity #892 #904]: #906
#915 := [trans #907 #913]: #914
#653 := [intro-def]: #652
#916 := [mp #653 #915]: #911
#917 := [not-or-elim #916]: #890
#1738 := [unit-resolution #917 #1737]: #101
#918 := [not-or-elim #916]: #902
#1739 := [unit-resolution #918 #1738]: #899
#1231 := (or #898 #895)
#1232 := [def-axiom]: #1231
#1740 := [unit-resolution #1232 #1739]: #895
#1741 := [th-lemma #1736 #1738 #1740]: false
#1742 := [lemma #1741]: #883
#1149 := (<= #1148 0::int)
#1151 := (not #1149)
#1150 := (not #1147)
#1152 := (or #1150 #1151)
#1153 := (not #1152)
#429 := (>= uf_9 0::int)
decl z3name!6 :: int
#803 := z3name!6
#812 := (* -1::int z3name!6)
decl uf_8 :: int
#37 := uf_8
#1110 := (+ uf_8 #812)
#1111 := (<= #1110 0::int)
#1113 := (not #1111)
#1109 := (>= #1110 0::int)
#1112 := (not #1109)
#1114 := (or #1112 #1113)
#1865 := [hypothesis]: #1113
#1297 := (or #1114 #1111)
#1298 := [def-axiom]: #1297
#1866 := [unit-resolution #1298 #1865]: #1114
#382 := (>= uf_8 0::int)
#1685 := (or #1111 #1109)
#1686 := [th-lemma]: #1685
#1867 := [unit-resolution #1686 #1865]: #1109
#1734 := (or #382 #1112)
#1121 := (+ uf_8 z3name!6)
#1123 := (>= #1121 0::int)
#1125 := (not #1123)
#1122 := (<= #1121 0::int)
#1124 := (not #1122)
#1126 := (or #1124 #1125)
#1127 := (not #1126)
#383 := (not #382)
#1428 := [hypothesis]: #383
#1130 := (or #382 #1127)
#1137 := (not #1130)
#1115 := (not #1114)
#1118 := (or #383 #1115)
#1136 := (not #1118)
#1138 := (or #1136 #1137)
#1139 := (not #1138)
#365 := (* -1::int uf_8)
#806 := (= z3name!6 #365)
#807 := (or #382 #806)
#804 := (= z3name!6 uf_8)
#805 := (or #383 #804)
#808 := (and #805 #807)
#1142 := (iff #808 #1139)
#1133 := (and #1118 #1130)
#1140 := (iff #1133 #1139)
#1141 := [rewrite]: #1140
#1134 := (iff #808 #1133)
#1131 := (iff #807 #1130)
#1128 := (iff #806 #1127)
#1129 := [rewrite]: #1128
#1132 := [monotonicity #1129]: #1131
#1119 := (iff #805 #1118)
#1116 := (iff #804 #1115)
#1117 := [rewrite]: #1116
#1120 := [monotonicity #1117]: #1119
#1135 := [monotonicity #1120 #1132]: #1134
#1143 := [trans #1135 #1141]: #1142
#809 := [intro-def]: #808
#1144 := [mp #809 #1143]: #1139
#1146 := [not-or-elim #1144]: #1130
#1729 := [unit-resolution #1146 #1428]: #1127
#1637 := [hypothesis]: #1109
#1730 := (or #1112 #1125 #382)
#1731 := [th-lemma]: #1730
#1732 := [unit-resolution #1731 #1428 #1637]: #1125
#1303 := (or #1126 #1123)
#1304 := [def-axiom]: #1303
#1733 := [unit-resolution #1304 #1732 #1729]: false
#1735 := [lemma #1733]: #1734
#1868 := [unit-resolution #1735 #1867]: #382
#1145 := [not-or-elim #1144]: #1118
#1869 := [unit-resolution #1145 #1868 #1866]: false
#1870 := [lemma #1869]: #1111
#289 := (not #288)
#1405 := [hypothesis]: #289
#1688 := (or #288 #429 #1113)
#815 := (+ uf_9 #812)
#818 := (+ uf_7 #815)
#825 := (>= #818 0::int)
#389 := (ite #382 uf_8 #365)
#400 := (* -1::int #389)
#401 := (+ uf_9 #400)
#402 := (+ uf_7 #401)
#599 := (>= #402 0::int)
#826 := (= #599 #825)
#819 := (~ #402 #818)
#816 := (~ #401 #815)
#813 := (~ #400 #812)
#810 := (~ #389 z3name!6)
#811 := [apply-def #809]: #810
#814 := [monotonicity #811]: #813
#817 := [monotonicity #814]: #816
#820 := [monotonicity #817]: #819
#827 := [monotonicity #820]: #826
#601 := (not #599)
#598 := (<= #402 0::int)
#600 := (not #598)
#602 := (or #600 #601)
#603 := (not #602)
#403 := (= #402 0::int)
#604 := (iff #403 #603)
#605 := [rewrite]: #604
#45 := (- uf_8)
#44 := (< uf_8 0::int)
#46 := (ite #44 #45 uf_8)
#47 := (- #46 uf_7)
#48 := (= uf_9 #47)
#408 := (iff #48 #403)
#368 := (ite #44 #365 uf_8)
#374 := (+ #318 #368)
#379 := (= uf_9 #374)
#406 := (iff #379 #403)
#394 := (+ #318 #389)
#397 := (= uf_9 #394)
#404 := (iff #397 #403)
#405 := [rewrite]: #404
#398 := (iff #379 #397)
#395 := (= #374 #394)
#392 := (= #368 #389)
#386 := (ite #383 #365 uf_8)
#390 := (= #386 #389)
#391 := [rewrite]: #390
#387 := (= #368 #386)
#384 := (iff #44 #383)
#385 := [rewrite]: #384
#388 := [monotonicity #385]: #387
#393 := [trans #388 #391]: #392
#396 := [monotonicity #393]: #395
#399 := [monotonicity #396]: #398
#407 := [trans #399 #405]: #406
#380 := (iff #48 #379)
#377 := (= #47 #374)
#371 := (- #368 uf_7)
#375 := (= #371 #374)
#376 := [rewrite]: #375
#372 := (= #47 #371)
#369 := (= #46 #368)
#366 := (= #45 #365)
#367 := [rewrite]: #366
#370 := [monotonicity #367]: #369
#373 := [monotonicity #370]: #372
#378 := [trans #373 #376]: #377
#381 := [monotonicity #378]: #380
#409 := [trans #381 #407]: #408
#364 := [asserted]: #48
#410 := [mp #364 #409]: #403
#606 := [mp #410 #605]: #603
#608 := [not-or-elim #606]: #599
#828 := [mp~ #608 #827]: #825
#1441 := [hypothesis]: #1075
#1285 := (or #1076 #1073)
#1286 := [def-axiom]: #1285
#1442 := [unit-resolution #1286 #1441]: #1076
#1107 := [not-or-elim #1106]: #1080
#1443 := [unit-resolution #1107 #1442]: #336
#1444 := [unit-resolution #1108 #1443]: #1089
#1291 := (or #1088 #1085)
#1292 := [def-axiom]: #1291
#1445 := [unit-resolution #1292 #1444]: #1085
#1446 := [th-lemma #1441 #1445 #1443]: false
#1447 := [lemma #1446]: #1073
#789 := (+ uf_8 #786)
#792 := (+ uf_6 #789)
#799 := (>= #792 0::int)
#342 := (ite #335 uf_7 #318)
#353 := (* -1::int #342)
#354 := (+ uf_8 #353)
#355 := (+ uf_6 #354)
#588 := (>= #355 0::int)
#800 := (= #588 #799)
#793 := (~ #355 #792)
#790 := (~ #354 #789)
#787 := (~ #353 #786)
#784 := (~ #342 z3name!5)
#785 := [apply-def #783]: #784
#788 := [monotonicity #785]: #787
#791 := [monotonicity #788]: #790
#794 := [monotonicity #791]: #793
#801 := [monotonicity #794]: #800
#590 := (not #588)
#587 := (<= #355 0::int)
#589 := (not #587)
#591 := (or #589 #590)
#592 := (not #591)
#356 := (= #355 0::int)
#593 := (iff #356 #592)
#594 := [rewrite]: #593
#39 := (- uf_7)
#38 := (< uf_7 0::int)
#40 := (ite #38 #39 uf_7)
#41 := (- #40 uf_6)
#42 := (= uf_8 #41)
#361 := (iff #42 #356)
#321 := (ite #38 #318 uf_7)
#271 := (* -1::int uf_6)
#327 := (+ #271 #321)
#332 := (= uf_8 #327)
#359 := (iff #332 #356)
#347 := (+ #271 #342)
#350 := (= uf_8 #347)
#357 := (iff #350 #356)
#358 := [rewrite]: #357
#351 := (iff #332 #350)
#348 := (= #327 #347)
#345 := (= #321 #342)
#339 := (ite #336 #318 uf_7)
#343 := (= #339 #342)
#344 := [rewrite]: #343
#340 := (= #321 #339)
#337 := (iff #38 #336)
#338 := [rewrite]: #337
#341 := [monotonicity #338]: #340
#346 := [trans #341 #344]: #345
#349 := [monotonicity #346]: #348
#352 := [monotonicity #349]: #351
#360 := [trans #352 #358]: #359
#333 := (iff #42 #332)
#330 := (= #41 #327)
#324 := (- #321 uf_6)
#328 := (= #324 #327)
#329 := [rewrite]: #328
#325 := (= #41 #324)
#322 := (= #40 #321)
#319 := (= #39 #318)
#320 := [rewrite]: #319
#323 := [monotonicity #320]: #322
#326 := [monotonicity #323]: #325
#331 := [trans #326 #329]: #330
#334 := [monotonicity #331]: #333
#362 := [trans #334 #360]: #361
#317 := [asserted]: #42
#363 := [mp #317 #362]: #356
#595 := [mp #363 #594]: #592
#597 := [not-or-elim #595]: #588
#802 := [mp~ #597 #801]: #799
#1343 := (not #825)
#1350 := (not #799)
#1351 := (or #288 #1075 #1350 #429 #1113 #1343)
#1352 := [th-lemma]: #1351
#1689 := [unit-resolution #1352 #802 #1447 #828]: #1688
#2046 := [unit-resolution #1689 #1405 #1870]: #429
#430 := (not #429)
#1156 := (or #430 #1153)
#1161 := (>= #1159 0::int)
#1163 := (not #1161)
#1162 := (not #1160)
#1164 := (or #1162 #1163)
#1165 := (not #1164)
#1168 := (or #429 #1165)
#1175 := (not #1168)
#1174 := (not #1156)
#1176 := (or #1174 #1175)
#1177 := (not #1176)
#412 := (* -1::int uf_9)
#832 := (= z3name!7 #412)
#833 := (or #429 #832)
#830 := (= z3name!7 uf_9)
#831 := (or #430 #830)
#834 := (and #831 #833)
#1180 := (iff #834 #1177)
#1171 := (and #1156 #1168)
#1178 := (iff #1171 #1177)
#1179 := [rewrite]: #1178
#1172 := (iff #834 #1171)
#1169 := (iff #833 #1168)
#1166 := (iff #832 #1165)
#1167 := [rewrite]: #1166
#1170 := [monotonicity #1167]: #1169
#1157 := (iff #831 #1156)
#1154 := (iff #830 #1153)
#1155 := [rewrite]: #1154
#1158 := [monotonicity #1155]: #1157
#1173 := [monotonicity #1158 #1170]: #1172
#1181 := [trans #1173 #1179]: #1180
#835 := [intro-def]: #834
#1182 := [mp #835 #1181]: #1177
#1183 := [not-or-elim #1182]: #1156
#2047 := [unit-resolution #1183 #2046]: #1153
#1307 := (or #1152 #1147)
#1308 := [def-axiom]: #1307
#2112 := [unit-resolution #1308 #2047]: #1147
#2009 := (or #288 #382)
#1998 := (or #1036 #288)
#1045 := (+ uf_6 z3name!4)
#1047 := (>= #1045 0::int)
#1049 := (not #1047)
#1046 := (<= #1045 0::int)
#1048 := (not #1046)
#1050 := (or #1048 #1049)
#1460 := [hypothesis]: #1049
#1279 := (or #1050 #1047)
#1280 := [def-axiom]: #1279
#1461 := [unit-resolution #1280 #1460]: #1050
#1464 := (or #1047 #289)
#1051 := (not #1050)
#1448 := [hypothesis]: #1037
#1273 := (or #1038 #1035)
#1274 := [def-axiom]: #1273
#1449 := [unit-resolution #1274 #1448]: #1038
#1042 := (or #289 #1039)
#1054 := (or #288 #1051)
#1061 := (not #1054)
#1060 := (not #1042)
#1062 := (or #1060 #1061)
#1063 := (not #1062)
#754 := (= z3name!4 #271)
#755 := (or #288 #754)
#752 := (= z3name!4 uf_6)
#753 := (or #289 #752)
#756 := (and #753 #755)
#1066 := (iff #756 #1063)
#1057 := (and #1042 #1054)
#1064 := (iff #1057 #1063)
#1065 := [rewrite]: #1064
#1058 := (iff #756 #1057)
#1055 := (iff #755 #1054)
#1052 := (iff #754 #1051)
#1053 := [rewrite]: #1052
#1056 := [monotonicity #1053]: #1055
#1043 := (iff #753 #1042)
#1040 := (iff #752 #1039)
#1041 := [rewrite]: #1040
#1044 := [monotonicity #1041]: #1043
#1059 := [monotonicity #1044 #1056]: #1058
#1067 := [trans #1059 #1065]: #1066
#757 := [intro-def]: #756
#1068 := [mp #757 #1067]: #1063
#1069 := [not-or-elim #1068]: #1042
#1450 := [unit-resolution #1069 #1449]: #289
#1070 := [not-or-elim #1068]: #1054
#1451 := [unit-resolution #1070 #1450]: #1051
#1452 := (or #1035 #1033)
#1453 := [th-lemma]: #1452
#1454 := [unit-resolution #1453 #1448]: #1033
#1455 := (or #1036 #288 #1049)
#1456 := [th-lemma]: #1455
#1457 := [unit-resolution #1456 #1450 #1454]: #1049
#1458 := [unit-resolution #1280 #1457 #1451]: false
#1459 := [lemma #1458]: #1035
#1462 := (or #1047 #1037 #289)
#1463 := [th-lemma]: #1462
#1465 := [unit-resolution #1463 #1459]: #1464
#1466 := [unit-resolution #1465 #1460]: #289
#1467 := [unit-resolution #1070 #1466 #1461]: false
#1468 := [lemma #1467]: #1047
#1999 := [unit-resolution #1456 #1468]: #1998
#2000 := [unit-resolution #1999 #1405]: #1036
#1407 := [unit-resolution #1070 #1405]: #1051
#1277 := (or #1050 #1046)
#1278 := [def-axiom]: #1277
#1497 := [unit-resolution #1278 #1407]: #1046
#2001 := (or #336 #1048 #1033 #382 #1350 #1075)
#2002 := [th-lemma]: #2001
#2003 := [unit-resolution #2002 #1497 #2000 #1447 #802 #1428]: #336
#2004 := (or #1087 #1075 #1048 #1033 #382 #1350)
#2005 := [th-lemma]: #2004
#2006 := [unit-resolution #2005 #1497 #1447 #2000 #802 #1428]: #1087
#2007 := [unit-resolution #1292 #2006]: #1088
#2008 := [unit-resolution #1108 #2007 #2003]: false
#2010 := [lemma #2008]: #2009
#2113 := [unit-resolution #2010 #1405]: #382
#2114 := [unit-resolution #1145 #2113]: #1115
#1295 := (or #1114 #1109)
#1296 := [def-axiom]: #1295
#2115 := [unit-resolution #1296 #2114]: #1109
decl z3name!2 :: int
#699 := z3name!2
#708 := (* -1::int z3name!2)
#958 := (+ uf_4 #708)
#957 := (>= #958 0::int)
#959 := (<= #958 0::int)
#961 := (not #959)
#960 := (not #957)
#962 := (or #960 #961)
#963 := (not #962)
decl uf_5 :: int
#19 := uf_5
#241 := (>= uf_5 0::int)
#242 := (not #241)
#1406 := [hypothesis]: #242
#1579 := (or #1048 #241)
#516 := (>= #514 0::int)
#476 := (>= uf_10 0::int)
#477 := (not #476)
#1484 := (or #382 #241)
#1430 := (or #382 #241 #1075 #1037)
#1421 := [hypothesis]: #1035
#1427 := [hypothesis]: #1073
#763 := (+ uf_7 #760)
#766 := (+ uf_5 #763)
#773 := (>= #766 0::int)
#295 := (ite #288 uf_6 #271)
#306 := (* -1::int #295)
#307 := (+ uf_7 #306)
#308 := (+ uf_5 #307)
#577 := (>= #308 0::int)
#774 := (= #577 #773)
#767 := (~ #308 #766)
#764 := (~ #307 #763)
#761 := (~ #306 #760)
#758 := (~ #295 z3name!4)
#759 := [apply-def #757]: #758
#762 := [monotonicity #759]: #761
#765 := [monotonicity #762]: #764
#768 := [monotonicity #765]: #767
#775 := [monotonicity #768]: #774
#579 := (not #577)
#576 := (<= #308 0::int)
#578 := (not #576)
#580 := (or #578 #579)
#581 := (not #580)
#309 := (= #308 0::int)
#582 := (iff #309 #581)
#583 := [rewrite]: #582
#33 := (- uf_6)
#32 := (< uf_6 0::int)
#34 := (ite #32 #33 uf_6)
#35 := (- #34 uf_5)
#36 := (= uf_7 #35)
#314 := (iff #36 #309)
#274 := (ite #32 #271 uf_6)
#224 := (* -1::int uf_5)
#280 := (+ #224 #274)
#285 := (= uf_7 #280)
#312 := (iff #285 #309)
#300 := (+ #224 #295)
#303 := (= uf_7 #300)
#310 := (iff #303 #309)
#311 := [rewrite]: #310
#304 := (iff #285 #303)
#301 := (= #280 #300)
#298 := (= #274 #295)
#292 := (ite #289 #271 uf_6)
#296 := (= #292 #295)
#297 := [rewrite]: #296
#293 := (= #274 #292)
#290 := (iff #32 #289)
#291 := [rewrite]: #290
#294 := [monotonicity #291]: #293
#299 := [trans #294 #297]: #298
#302 := [monotonicity #299]: #301
#305 := [monotonicity #302]: #304
#313 := [trans #305 #311]: #312
#286 := (iff #36 #285)
#283 := (= #35 #280)
#277 := (- #274 uf_5)
#281 := (= #277 #280)
#282 := [rewrite]: #281
#278 := (= #35 #277)
#275 := (= #34 #274)
#272 := (= #33 #271)
#273 := [rewrite]: #272
#276 := [monotonicity #273]: #275
#279 := [monotonicity #276]: #278
#284 := [trans #279 #282]: #283
#287 := [monotonicity #284]: #286
#315 := [trans #287 #313]: #314
#270 := [asserted]: #36
#316 := [mp #270 #315]: #309
#584 := [mp #316 #583]: #581
#586 := [not-or-elim #584]: #577
#776 := [mp~ #586 #775]: #773
#1429 := [th-lemma #776 #1406 #1428 #1427 #802 #1421]: false
#1431 := [lemma #1429]: #1430
#1485 := [unit-resolution #1431 #1447 #1459]: #1484
#1486 := [unit-resolution #1485 #1406]: #382
#1487 := [unit-resolution #1145 #1486]: #1115
#1496 := [unit-resolution #1298 #1487]: #1111
#1545 := [hypothesis]: #1046
#1548 := (or #1048 #1113 #429)
#1546 := (or #1048 #1113 #429 #1343 #1075 #1350 #1037)
#1547 := [th-lemma]: #1546
#1549 := [unit-resolution #1547 #1447 #802 #1459 #828]: #1548
#1550 := [unit-resolution #1549 #1545 #1496]: #429
#1551 := [unit-resolution #1183 #1550]: #1153
#1552 := [unit-resolution #1308 #1551]: #1147
#1543 := (or #477 #241 #1150)
#1488 := [unit-resolution #1296 #1487]: #1109
#821 := (<= #818 0::int)
#822 := (= #598 #821)
#823 := [monotonicity #820]: #822
#607 := [not-or-elim #606]: #598
#824 := [mp~ #607 #823]: #821
#841 := (+ uf_10 #838)
#844 := (+ uf_8 #841)
#847 := (<= #844 0::int)
#436 := (ite #429 uf_9 #412)
#447 := (* -1::int #436)
#448 := (+ uf_10 #447)
#449 := (+ uf_8 #448)
#609 := (<= #449 0::int)
#848 := (= #609 #847)
#845 := (~ #449 #844)
#842 := (~ #448 #841)
#839 := (~ #447 #838)
#836 := (~ #436 z3name!7)
#837 := [apply-def #835]: #836
#840 := [monotonicity #837]: #839
#843 := [monotonicity #840]: #842
#846 := [monotonicity #843]: #845
#849 := [monotonicity #846]: #848
#610 := (>= #449 0::int)
#612 := (not #610)
#611 := (not #609)
#613 := (or #611 #612)
#614 := (not #613)
#450 := (= #449 0::int)
#615 := (iff #450 #614)
#616 := [rewrite]: #615
#51 := (- uf_9)
#50 := (< uf_9 0::int)
#52 := (ite #50 #51 uf_9)
#53 := (- #52 uf_8)
#54 := (= uf_10 #53)
#455 := (iff #54 #450)
#415 := (ite #50 #412 uf_9)
#421 := (+ #365 #415)
#426 := (= uf_10 #421)
#453 := (iff #426 #450)
#441 := (+ #365 #436)
#444 := (= uf_10 #441)
#451 := (iff #444 #450)
#452 := [rewrite]: #451
#445 := (iff #426 #444)
#442 := (= #421 #441)
#439 := (= #415 #436)
#433 := (ite #430 #412 uf_9)
#437 := (= #433 #436)
#438 := [rewrite]: #437
#434 := (= #415 #433)
#431 := (iff #50 #430)
#432 := [rewrite]: #431
#435 := [monotonicity #432]: #434
#440 := [trans #435 #438]: #439
#443 := [monotonicity #440]: #442
#446 := [monotonicity #443]: #445
#454 := [trans #446 #452]: #453
#427 := (iff #54 #426)
#424 := (= #53 #421)
#418 := (- #415 uf_8)
#422 := (= #418 #421)
#423 := [rewrite]: #422
#419 := (= #53 #418)
#416 := (= #52 #415)
#413 := (= #51 #412)
#414 := [rewrite]: #413
#417 := [monotonicity #414]: #416
#420 := [monotonicity #417]: #419
#425 := [trans #420 #423]: #424
#428 := [monotonicity #425]: #427
#456 := [trans #428 #454]: #455
#411 := [asserted]: #54
#457 := [mp #411 #456]: #450
#617 := [mp #457 #616]: #614
#618 := [not-or-elim #617]: #609
#850 := [mp~ #618 #849]: #847
#1540 := [hypothesis]: #1147
#1541 := [hypothesis]: #476
#1542 := [th-lemma #1468 #1406 #1541 #1540 #850 #824 #1488 #776 #1459]: false
#1544 := [lemma #1542]: #1543
#1553 := [unit-resolution #1544 #1552 #1406]: #477
#851 := (>= #844 0::int)
#852 := (= #610 #851)
#853 := [monotonicity #846]: #852
#619 := [not-or-elim #617]: #610
#854 := [mp~ #619 #853]: #851
#1309 := (or #1152 #1149)
#1310 := [def-axiom]: #1309
#1554 := [unit-resolution #1310 #1551]: #1149
#769 := (<= #766 0::int)
#770 := (= #576 #769)
#771 := [monotonicity #768]: #770
#585 := [not-or-elim #584]: #576
#772 := [mp~ #585 #771]: #769
decl z3name!3 :: int
#725 := z3name!3
#1007 := (+ uf_5 z3name!3)
#1009 := (>= #1007 0::int)
#1011 := (not #1009)
#1398 := [hypothesis]: #1011
#734 := (* -1::int z3name!3)
#996 := (+ uf_5 #734)
#997 := (<= #996 0::int)
#999 := (not #997)
#995 := (>= #996 0::int)
#998 := (not #995)
#1000 := (or #998 #999)
#1001 := (not #1000)
#1008 := (<= #1007 0::int)
#1010 := (not #1008)
#1012 := (or #1010 #1011)
#1267 := (or #1012 #1009)
#1268 := [def-axiom]: #1267
#1399 := [unit-resolution #1268 #1398]: #1012
#1013 := (not #1012)
#1016 := (or #241 #1013)
#1023 := (not #1016)
#1004 := (or #242 #1001)
#1022 := (not #1004)
#1024 := (or #1022 #1023)
#1025 := (not #1024)
#728 := (= z3name!3 #224)
#729 := (or #241 #728)
#726 := (= z3name!3 uf_5)
#727 := (or #242 #726)
#730 := (and #727 #729)
#1028 := (iff #730 #1025)
#1019 := (and #1004 #1016)
#1026 := (iff #1019 #1025)
#1027 := [rewrite]: #1026
#1020 := (iff #730 #1019)
#1017 := (iff #729 #1016)
#1014 := (iff #728 #1013)
#1015 := [rewrite]: #1014
#1018 := [monotonicity #1015]: #1017
#1005 := (iff #727 #1004)
#1002 := (iff #726 #1001)
#1003 := [rewrite]: #1002
#1006 := [monotonicity #1003]: #1005
#1021 := [monotonicity #1006 #1018]: #1020
#1029 := [trans #1021 #1027]: #1028
#731 := [intro-def]: #730
#1030 := [mp #731 #1029]: #1025
#1032 := [not-or-elim #1030]: #1016
#1400 := [unit-resolution #1032 #1399]: #241
#1031 := [not-or-elim #1030]: #1004
#1401 := [unit-resolution #1031 #1400]: #1001
#1261 := (or #1000 #997)
#1262 := [def-axiom]: #1261
#1402 := [unit-resolution #1262 #1401]: #997
#1403 := [th-lemma #1400 #1402 #1398]: false
#1404 := [lemma #1403]: #1009
#737 := (+ uf_6 #734)
#740 := (+ uf_4 #737)
#747 := (>= #740 0::int)
#248 := (ite #241 uf_5 #224)
#259 := (* -1::int #248)
#260 := (+ uf_6 #259)
#261 := (+ uf_4 #260)
#566 := (>= #261 0::int)
#748 := (= #566 #747)
#741 := (~ #261 #740)
#738 := (~ #260 #737)
#735 := (~ #259 #734)
#732 := (~ #248 z3name!3)
#733 := [apply-def #731]: #732
#736 := [monotonicity #733]: #735
#739 := [monotonicity #736]: #738
#742 := [monotonicity #739]: #741
#749 := [monotonicity #742]: #748
#568 := (not #566)
#565 := (<= #261 0::int)
#567 := (not #565)
#569 := (or #567 #568)
#570 := (not #569)
#262 := (= #261 0::int)
#571 := (iff #262 #570)
#572 := [rewrite]: #571
#27 := (- uf_5)
#26 := (< uf_5 0::int)
#28 := (ite #26 #27 uf_5)
#29 := (- #28 uf_4)
#30 := (= uf_6 #29)
#267 := (iff #30 #262)
#227 := (ite #26 #224 uf_5)
#177 := (* -1::int uf_4)
#233 := (+ #177 #227)
#238 := (= uf_6 #233)
#265 := (iff #238 #262)
#253 := (+ #177 #248)
#256 := (= uf_6 #253)
#263 := (iff #256 #262)
#264 := [rewrite]: #263
#257 := (iff #238 #256)
#254 := (= #233 #253)
#251 := (= #227 #248)
#245 := (ite #242 #224 uf_5)
#249 := (= #245 #248)
#250 := [rewrite]: #249
#246 := (= #227 #245)
#243 := (iff #26 #242)
#244 := [rewrite]: #243
#247 := [monotonicity #244]: #246
#252 := [trans #247 #250]: #251
#255 := [monotonicity #252]: #254
#258 := [monotonicity #255]: #257
#266 := [trans #258 #264]: #265
#239 := (iff #30 #238)
#236 := (= #29 #233)
#230 := (- #227 uf_4)
#234 := (= #230 #233)
#235 := [rewrite]: #234
#231 := (= #29 #230)
#228 := (= #28 #227)
#225 := (= #27 #224)
#226 := [rewrite]: #225
#229 := [monotonicity #226]: #228
#232 := [monotonicity #229]: #231
#237 := [trans #232 #235]: #236
#240 := [monotonicity #237]: #239
#268 := [trans #240 #266]: #267
#223 := [asserted]: #30
#269 := [mp #223 #268]: #262
#573 := [mp #269 #572]: #570
#575 := [not-or-elim #573]: #566
#750 := [mp~ #575 #749]: #747
#1364 := (not #747)
#1357 := (not #769)
#1337 := (not #851)
#1555 := (or #194 #476 #1151 #1337 #1343 #1113 #1048 #1357 #1364 #1011)
#1556 := [th-lemma]: #1555
#1557 := [unit-resolution #1556 #1545 #750 #1404 #772 #1496 #828 #1554 #854 #1553]: #194
#195 := (not #194)
#966 := (or #195 #963)
#969 := (+ uf_4 z3name!2)
#971 := (>= #969 0::int)
#973 := (not #971)
#970 := (<= #969 0::int)
#972 := (not #970)
#974 := (or #972 #973)
#975 := (not #974)
#978 := (or #194 #975)
#985 := (not #978)
#984 := (not #966)
#986 := (or #984 #985)
#987 := (not #986)
#702 := (= z3name!2 #177)
#703 := (or #194 #702)
#700 := (= z3name!2 uf_4)
#701 := (or #195 #700)
#704 := (and #701 #703)
#990 := (iff #704 #987)
#981 := (and #966 #978)
#988 := (iff #981 #987)
#989 := [rewrite]: #988
#982 := (iff #704 #981)
#979 := (iff #703 #978)
#976 := (iff #702 #975)
#977 := [rewrite]: #976
#980 := [monotonicity #977]: #979
#967 := (iff #701 #966)
#964 := (iff #700 #963)
#965 := [rewrite]: #964
#968 := [monotonicity #965]: #967
#983 := [monotonicity #968 #980]: #982
#991 := [trans #983 #989]: #990
#705 := [intro-def]: #704
#992 := [mp #705 #991]: #987
#993 := [not-or-elim #992]: #966
#1558 := [unit-resolution #993 #1557]: #963
#1249 := (or #962 #959)
#1250 := [def-axiom]: #1249
#1559 := [unit-resolution #1250 #1558]: #959
decl z3name!8 :: int
#855 := z3name!8
#864 := (* -1::int z3name!8)
#867 := (+ uf_11 #864)
#870 := (+ uf_9 #867)
#873 := (<= #870 0::int)
#483 := (ite #476 uf_10 #459)
#494 := (* -1::int #483)
#495 := (+ uf_11 #494)
#496 := (+ uf_9 #495)
#620 := (<= #496 0::int)
#874 := (= #620 #873)
#871 := (~ #496 #870)
#868 := (~ #495 #867)
#865 := (~ #494 #864)
#862 := (~ #483 z3name!8)
#858 := (= z3name!8 #459)
#859 := (or #476 #858)
#856 := (= z3name!8 uf_10)
#857 := (or #477 #856)
#860 := (and #857 #859)
#861 := [intro-def]: #860
#863 := [apply-def #861]: #862
#866 := [monotonicity #863]: #865
#869 := [monotonicity #866]: #868
#872 := [monotonicity #869]: #871
#875 := [monotonicity #872]: #874
#621 := (>= #496 0::int)
#623 := (not #621)
#622 := (not #620)
#624 := (or #622 #623)
#625 := (not #624)
#497 := (= #496 0::int)
#626 := (iff #497 #625)
#627 := [rewrite]: #626
#57 := (- uf_10)
#56 := (< uf_10 0::int)
#58 := (ite #56 #57 uf_10)
#59 := (- #58 uf_9)
#60 := (= uf_11 #59)
#502 := (iff #60 #497)
#462 := (ite #56 #459 uf_10)
#468 := (+ #412 #462)
#473 := (= uf_11 #468)
#500 := (iff #473 #497)
#488 := (+ #412 #483)
#491 := (= uf_11 #488)
#498 := (iff #491 #497)
#499 := [rewrite]: #498
#492 := (iff #473 #491)
#489 := (= #468 #488)
#486 := (= #462 #483)
#480 := (ite #477 #459 uf_10)
#484 := (= #480 #483)
#485 := [rewrite]: #484
#481 := (= #462 #480)
#478 := (iff #56 #477)
#479 := [rewrite]: #478
#482 := [monotonicity #479]: #481
#487 := [trans #482 #485]: #486
#490 := [monotonicity #487]: #489
#493 := [monotonicity #490]: #492
#501 := [trans #493 #499]: #500
#474 := (iff #60 #473)
#471 := (= #59 #468)
#465 := (- #462 uf_9)
#469 := (= #465 #468)
#470 := [rewrite]: #469
#466 := (= #59 #465)
#463 := (= #58 #462)
#460 := (= #57 #459)
#461 := [rewrite]: #460
#464 := [monotonicity #461]: #463
#467 := [monotonicity #464]: #466
#472 := [trans #467 #470]: #471
#475 := [monotonicity #472]: #474
#503 := [trans #475 #501]: #502
#458 := [asserted]: #60
#504 := [mp #458 #503]: #497
#628 := [mp #504 #627]: #625
#629 := [not-or-elim #628]: #620
#876 := [mp~ #629 #875]: #873
#1197 := (+ uf_10 z3name!8)
#1198 := (<= #1197 0::int)
#1199 := (>= #1197 0::int)
#1201 := (not #1199)
#1200 := (not #1198)
#1202 := (or #1200 #1201)
#1203 := (not #1202)
#1206 := (or #476 #1203)
#1213 := (not #1206)
#1186 := (+ uf_10 #864)
#1187 := (<= #1186 0::int)
#1189 := (not #1187)
#1185 := (>= #1186 0::int)
#1188 := (not #1185)
#1190 := (or #1188 #1189)
#1191 := (not #1190)
#1194 := (or #477 #1191)
#1212 := (not #1194)
#1214 := (or #1212 #1213)
#1215 := (not #1214)
#1218 := (iff #860 #1215)
#1209 := (and #1194 #1206)
#1216 := (iff #1209 #1215)
#1217 := [rewrite]: #1216
#1210 := (iff #860 #1209)
#1207 := (iff #859 #1206)
#1204 := (iff #858 #1203)
#1205 := [rewrite]: #1204
#1208 := [monotonicity #1205]: #1207
#1195 := (iff #857 #1194)
#1192 := (iff #856 #1191)
#1193 := [rewrite]: #1192
#1196 := [monotonicity #1193]: #1195
#1211 := [monotonicity #1196 #1208]: #1210
#1219 := [trans #1211 #1217]: #1218
#1220 := [mp #861 #1219]: #1215
#1222 := [not-or-elim #1220]: #1206
#1560 := [unit-resolution #1222 #1553]: #1203
#1325 := (or #1202 #1198)
#1326 := [def-axiom]: #1325
#1561 := [unit-resolution #1326 #1560]: #1198
#711 := (+ uf_5 #708)
#714 := (+ uf_1 #711)
#721 := (>= #714 0::int)
#201 := (ite #194 uf_4 #177)
#212 := (* -1::int #201)
#213 := (+ uf_5 #212)
#214 := (+ uf_1 #213)
#555 := (>= #214 0::int)
#722 := (= #555 #721)
#715 := (~ #214 #714)
#712 := (~ #213 #711)
#709 := (~ #212 #708)
#706 := (~ #201 z3name!2)
#707 := [apply-def #705]: #706
#710 := [monotonicity #707]: #709
#713 := [monotonicity #710]: #712
#716 := [monotonicity #713]: #715
#723 := [monotonicity #716]: #722
#557 := (not #555)
#554 := (<= #214 0::int)
#556 := (not #554)
#558 := (or #556 #557)
#559 := (not #558)
#215 := (= #214 0::int)
#560 := (iff #215 #559)
#561 := [rewrite]: #560
#21 := (- uf_4)
#20 := (< uf_4 0::int)
#22 := (ite #20 #21 uf_4)
#23 := (- #22 uf_1)
#24 := (= uf_5 #23)
#220 := (iff #24 #215)
#180 := (ite #20 #177 uf_4)
#186 := (+ #130 #180)
#191 := (= uf_5 #186)
#218 := (iff #191 #215)
#206 := (+ #130 #201)
#209 := (= uf_5 #206)
#216 := (iff #209 #215)
#217 := [rewrite]: #216
#210 := (iff #191 #209)
#207 := (= #186 #206)
#204 := (= #180 #201)
#198 := (ite #195 #177 uf_4)
#202 := (= #198 #201)
#203 := [rewrite]: #202
#199 := (= #180 #198)
#196 := (iff #20 #195)
#197 := [rewrite]: #196
#200 := [monotonicity #197]: #199
#205 := [trans #200 #203]: #204
#208 := [monotonicity #205]: #207
#211 := [monotonicity #208]: #210
#219 := [trans #211 #217]: #218
#192 := (iff #24 #191)
#189 := (= #23 #186)
#183 := (- #180 uf_1)
#187 := (= #183 #186)
#188 := [rewrite]: #187
#184 := (= #23 #183)
#181 := (= #22 #180)
#178 := (= #21 #177)
#179 := [rewrite]: #178
#182 := [monotonicity #179]: #181
#185 := [monotonicity #182]: #184
#190 := [trans #185 #188]: #189
#193 := [monotonicity #190]: #192
#221 := [trans #193 #219]: #220
#176 := [asserted]: #24
#222 := [mp #176 #221]: #215
#562 := [mp #222 #561]: #559
#564 := [not-or-elim #562]: #555
#724 := [mp~ #564 #723]: #721
#685 := (+ uf_4 #682)
#688 := (+ uf_2 #685)
#695 := (>= #688 0::int)
#154 := (ite #147 uf_1 #130)
#165 := (* -1::int #154)
#166 := (+ uf_4 #165)
#167 := (+ uf_2 #166)
#544 := (>= #167 0::int)
#696 := (= #544 #695)
#689 := (~ #167 #688)
#686 := (~ #166 #685)
#683 := (~ #165 #682)
#680 := (~ #154 z3name!1)
#681 := [apply-def #679]: #680
#684 := [monotonicity #681]: #683
#687 := [monotonicity #684]: #686
#690 := [monotonicity #687]: #689
#697 := [monotonicity #690]: #696
#546 := (not #544)
#543 := (<= #167 0::int)
#545 := (not #543)
#547 := (or #545 #546)
#548 := (not #547)
#168 := (= #167 0::int)
#549 := (iff #168 #548)
#550 := [rewrite]: #549
#15 := (- uf_1)
#14 := (< uf_1 0::int)
#16 := (ite #14 #15 uf_1)
#17 := (- #16 uf_2)
#18 := (= uf_4 #17)
#173 := (iff #18 #168)
#133 := (ite #14 #130 uf_1)
#139 := (+ #82 #133)
#144 := (= uf_4 #139)
#171 := (iff #144 #168)
#159 := (+ #82 #154)
#162 := (= uf_4 #159)
#169 := (iff #162 #168)
#170 := [rewrite]: #169
#163 := (iff #144 #162)
#160 := (= #139 #159)
#157 := (= #133 #154)
#151 := (ite #148 #130 uf_1)
#155 := (= #151 #154)
#156 := [rewrite]: #155
#152 := (= #133 #151)
#149 := (iff #14 #148)
#150 := [rewrite]: #149
#153 := [monotonicity #150]: #152
#158 := [trans #153 #156]: #157
#161 := [monotonicity #158]: #160
#164 := [monotonicity #161]: #163
#172 := [trans #164 #170]: #171
#145 := (iff #18 #144)
#142 := (= #17 #139)
#136 := (- #133 uf_2)
#140 := (= #136 #139)
#141 := [rewrite]: #140
#137 := (= #17 #136)
#134 := (= #16 #133)
#131 := (= #15 #130)
#132 := [rewrite]: #131
#135 := [monotonicity #132]: #134
#138 := [monotonicity #135]: #137
#143 := [trans #138 #141]: #142
#146 := [monotonicity #143]: #145
#174 := [trans #146 #172]: #173
#129 := [asserted]: #18
#175 := [mp #129 #174]: #168
#551 := [mp #175 #550]: #548
#553 := [not-or-elim #551]: #544
#698 := [mp~ #553 #697]: #695
#1373 := (not #721)
#1562 := (or #147 #1373 #961 #241 #195)
#1563 := [th-lemma]: #1562
#1564 := [unit-resolution #1563 #1559 #1557 #724 #1406]: #147
#1565 := [unit-resolution #955 #1564]: #925
#1566 := [unit-resolution #1238 #1565]: #921
#1372 := (not #873)
#1371 := (not #695)
#1498 := (or #516 #923 #1373 #1371 #1372 #1343 #1200 #1075 #1350 #1113 #961 #1151 #1337 #1048 #1357)
#1499 := [th-lemma]: #1498
#1567 := [unit-resolution #1499 #1566 #698 #724 #1545 #772 #1447 #802 #1496 #828 #1554 #854 #1561 #876 #1559]: #516
#1247 := (or #962 #957)
#1248 := [def-axiom]: #1247
#1568 := [unit-resolution #1248 #1558]: #957
#877 := (>= #870 0::int)
#878 := (= #621 #877)
#879 := [monotonicity #872]: #878
#630 := [not-or-elim #628]: #621
#880 := [mp~ #630 #879]: #877
#1327 := (or #1202 #1199)
#1328 := [def-axiom]: #1327
#1569 := [unit-resolution #1328 #1560]: #1199
#795 := (<= #792 0::int)
#796 := (= #587 #795)
#797 := [monotonicity #794]: #796
#596 := [not-or-elim #595]: #587
#798 := [mp~ #596 #797]: #795
#1503 := (or #335 #1049 #241)
#1425 := (or #335 #1049 #241 #1037)
#1422 := [hypothesis]: #336
#1423 := [hypothesis]: #1047
#1424 := [th-lemma #1423 #1422 #776 #1406 #1421]: false
#1426 := [lemma #1424]: #1425
#1504 := [unit-resolution #1426 #1459]: #1503
#1505 := [unit-resolution #1504 #1406 #1468]: #335
#1506 := [unit-resolution #1107 #1505]: #1077
#1283 := (or #1076 #1071)
#1284 := [def-axiom]: #1283
#1507 := [unit-resolution #1284 #1506]: #1071
#717 := (<= #714 0::int)
#718 := (= #554 #717)
#719 := [monotonicity #716]: #718
#563 := [not-or-elim #562]: #554
#720 := [mp~ #563 #719]: #717
#691 := (<= #688 0::int)
#692 := (= #543 #691)
#693 := [monotonicity #690]: #692
#552 := [not-or-elim #551]: #543
#694 := [mp~ #552 #693]: #691
#1235 := (or #924 #919)
#1236 := [def-axiom]: #1235
#1570 := [unit-resolution #1236 #1565]: #919
#1409 := (not #773)
#1489 := (not #847)
#1358 := (not #795)
#1365 := (not #821)
#1511 := (not #877)
#1510 := (not #691)
#1509 := (not #717)
#1512 := (or #515 #922 #1509 #1510 #1511 #1365 #1201 #1074 #1358 #1112 #960 #1150 #1489 #1049 #1409)
#1513 := [th-lemma]: #1512
#1571 := [unit-resolution #1513 #1570 #694 #720 #1468 #776 #1507 #798 #1488 #824 #1552 #850 #1569 #880 #1568]: #515
#506 := (<= #508 0::int)
#659 := (+ uf_3 #656)
#662 := (+ uf_1 #659)
#665 := (<= #662 0::int)
#107 := (ite #100 uf_2 #82)
#118 := (* -1::int #107)
#119 := (+ uf_3 #118)
#120 := (+ uf_1 #119)
#532 := (<= #120 0::int)
#666 := (= #532 #665)
#663 := (~ #120 #662)
#660 := (~ #119 #659)
#657 := (~ #118 #656)
#654 := (~ #107 z3name!0)
#655 := [apply-def #653]: #654
#658 := [monotonicity #655]: #657
#661 := [monotonicity #658]: #660
#664 := [monotonicity #661]: #663
#667 := [monotonicity #664]: #666
#533 := (>= #120 0::int)
#535 := (not #533)
#534 := (not #532)
#536 := (or #534 #535)
#537 := (not #536)
#121 := (= #120 0::int)
#538 := (iff #121 #537)
#539 := [rewrite]: #538
#8 := (- uf_2)
#7 := (< uf_2 0::int)
#9 := (ite #7 #8 uf_2)
#11 := (- #9 uf_3)
#12 := (= uf_1 #11)
#126 := (iff #12 #121)
#85 := (ite #7 #82 uf_2)
#91 := (* -1::int uf_3)
#92 := (+ #91 #85)
#97 := (= uf_1 #92)
#124 := (iff #97 #121)
#112 := (+ #91 #107)
#115 := (= uf_1 #112)
#122 := (iff #115 #121)
#123 := [rewrite]: #122
#116 := (iff #97 #115)
#113 := (= #92 #112)
#110 := (= #85 #107)
#104 := (ite #101 #82 uf_2)
#108 := (= #104 #107)
#109 := [rewrite]: #108
#105 := (= #85 #104)
#102 := (iff #7 #101)
#103 := [rewrite]: #102
#106 := [monotonicity #103]: #105
#111 := [trans #106 #109]: #110
#114 := [monotonicity #111]: #113
#117 := [monotonicity #114]: #116
#125 := [trans #117 #123]: #124
#98 := (iff #12 #97)
#95 := (= #11 #92)
#88 := (- #85 uf_3)
#93 := (= #88 #92)
#94 := [rewrite]: #93
#89 := (= #11 #88)
#86 := (= #9 #85)
#83 := (= #8 #82)
#84 := [rewrite]: #83
#87 := [monotonicity #84]: #86
#90 := [monotonicity #87]: #89
#96 := [trans #90 #94]: #95
#99 := [monotonicity #96]: #98
#127 := [trans #99 #125]: #126
#80 := [asserted]: #12
#128 := [mp #80 #127]: #121
#540 := [mp #128 #539]: #537
#541 := [not-or-elim #540]: #532
#668 := [mp~ #541 #667]: #665
#1515 := (or #100 #241 #923 #1373 #1371 #961)
#1516 := [th-lemma]: #1515
#1572 := [unit-resolution #1516 #1566 #698 #1559 #724 #1406]: #100
#1573 := [unit-resolution #917 #1572]: #887
#1223 := (or #886 #881)
#1224 := [def-axiom]: #1223
#1574 := [unit-resolution #1224 #1573]: #881
#1528 := (not #665)
#1529 := (or #506 #884 #1528 #1364 #1011 #1343 #1113 #1151 #1337 #1048 #1357 #922 #1510)
#1530 := [th-lemma]: #1529
#1575 := [unit-resolution #1530 #1574 #668 #694 #1404 #750 #1545 #772 #1496 #828 #1554 #854 #1570]: #506
#743 := (<= #740 0::int)
#744 := (= #565 #743)
#745 := [monotonicity #742]: #744
#574 := [not-or-elim #573]: #565
#746 := [mp~ #574 #745]: #743
#1520 := [unit-resolution #1032 #1406]: #1013
#1265 := (or #1012 #1008)
#1266 := [def-axiom]: #1265
#1521 := [unit-resolution #1266 #1520]: #1008
#669 := (>= #662 0::int)
#670 := (= #533 #669)
#671 := [monotonicity #664]: #670
#542 := [not-or-elim #540]: #533
#672 := [mp~ #542 #671]: #669
#1576 := [unit-resolution #1226 #1573]: #883
#1523 := (not #743)
#1522 := (not #669)
#1524 := (or #509 #885 #1522 #1523 #1010 #1365 #1112 #1150 #1489 #1049 #1409 #923 #1371)
#1525 := [th-lemma]: #1524
#1577 := [unit-resolution #1525 #1576 #672 #698 #1521 #746 #1468 #776 #1488 #824 #1552 #850 #1566]: #509
#634 := (not #516)
#633 := (not #515)
#632 := (not #509)
#631 := (not #506)
#635 := (or #631 #632 #633 #634)
#523 := (and #506 #509 #515 #516)
#528 := (not #523)
#644 := (iff #528 #635)
#636 := (not #635)
#639 := (not #636)
#642 := (iff #639 #635)
#643 := [rewrite]: #642
#640 := (iff #528 #639)
#637 := (iff #523 #636)
#638 := [rewrite]: #637
#641 := [monotonicity #638]: #640
#645 := [trans #641 #643]: #644
#62 := (= uf_2 uf_11)
#61 := (= uf_3 uf_10)
#63 := (and #61 #62)
#64 := (not #63)
#529 := (iff #64 #528)
#526 := (iff #63 #523)
#517 := (and #515 #516)
#510 := (and #506 #509)
#520 := (and #510 #517)
#524 := (iff #520 #523)
#525 := [rewrite]: #524
#521 := (iff #63 #520)
#518 := (iff #62 #517)
#519 := [rewrite]: #518
#511 := (iff #61 #510)
#512 := [rewrite]: #511
#522 := [monotonicity #512 #519]: #521
#527 := [trans #522 #525]: #526
#530 := [monotonicity #527]: #529
#505 := [asserted]: #64
#531 := [mp #505 #530]: #528
#646 := [mp #531 #645]: #635
#1578 := [unit-resolution #646 #1577 #1575 #1571 #1567]: false
#1580 := [lemma #1578]: #1579
#1657 := [unit-resolution #1580 #1406]: #1048
#1625 := (or #194 #241)
#1535 := [hypothesis]: #195
#1538 := (or #194 #960)
#1432 := [hypothesis]: #973
#1255 := (or #974 #971)
#1256 := [def-axiom]: #1255
#1433 := [unit-resolution #1256 #1432]: #974
#994 := [not-or-elim #992]: #978
#1434 := [unit-resolution #994 #1433]: #194
#1435 := [unit-resolution #993 #1434]: #963
#1436 := (or #971 #195 #961)
#1437 := [th-lemma]: #1436
#1438 := [unit-resolution #1437 #1434 #1432]: #961
#1439 := [unit-resolution #1250 #1438 #1435]: false
#1440 := [lemma #1439]: #971
#1536 := [hypothesis]: #957
#1537 := [th-lemma #1536 #1535 #1440]: false
#1539 := [lemma #1537]: #1538
#1581 := [unit-resolution #1539 #1535]: #960
#1582 := (or #959 #957)
#1583 := [th-lemma]: #1582
#1584 := [unit-resolution #1583 #1581]: #959
#1585 := (or #147 #1373 #241 #194 #973)
#1586 := [th-lemma]: #1585
#1587 := [unit-resolution #1586 #1535 #1440 #724 #1406]: #147
#1588 := [unit-resolution #955 #1587]: #925
#1589 := [unit-resolution #1238 #1588]: #921
#1590 := [unit-resolution #1516 #1589 #698 #1584 #724 #1406]: #100
#1591 := [unit-resolution #917 #1590]: #887
#1592 := [unit-resolution #1224 #1591]: #881
#1593 := (or #430 #1365 #1074 #1358 #1112 #194 #1364 #1011 #241)
#1594 := [th-lemma]: #1593
#1595 := [unit-resolution #1594 #1535 #1404 #750 #1507 #798 #1488 #824 #1406]: #430
#1184 := [not-or-elim #1182]: #1168
#1596 := [unit-resolution #1184 #1595]: #1165
#1315 := (or #1164 #1161)
#1316 := [def-axiom]: #1315
#1597 := [unit-resolution #1316 #1596]: #1161
#1533 := (or #288 #241)
#1471 := (or #194 #288 #241)
#1469 := (or #194 #288 #241 #1364 #1011)
#1470 := [th-lemma]: #1469
#1472 := [unit-resolution #1470 #1404 #750]: #1471
#1473 := [unit-resolution #1472 #1405 #1406]: #194
#1474 := [unit-resolution #993 #1473]: #963
#1475 := [unit-resolution #1250 #1474]: #959
#1476 := (or #147 #1373 #1364 #1011 #961 #241 #288)
#1477 := [th-lemma]: #1476
#1478 := [unit-resolution #1477 #1475 #724 #1406 #1404 #750 #1405]: #147
#1479 := [unit-resolution #955 #1478]: #925
#1480 := [unit-resolution #1238 #1479]: #921
#1419 := (or #288 #241 #429)
#1333 := [hypothesis]: #430
#1408 := [unit-resolution #1280 #1407]: #1047
#1410 := (or #335 #1049 #1409 #288 #241)
#1411 := [th-lemma]: #1410
#1412 := [unit-resolution #1411 #1405 #1408 #776 #1406]: #335
#1413 := [unit-resolution #1107 #1412]: #1077
#1414 := [unit-resolution #1286 #1413]: #1073
#1415 := [unit-resolution #1352 #1414 #802 #1405 #828 #1333]: #1113
#1416 := [unit-resolution #1298 #1415]: #1114
#1417 := [unit-resolution #1145 #1416]: #383
#1418 := [th-lemma #1414 #802 #1405 #1408 #776 #1406 #1417]: false
#1420 := [lemma #1418]: #1419
#1481 := [unit-resolution #1420 #1405 #1406]: #429
#1482 := [unit-resolution #1183 #1481]: #1153
#1483 := [unit-resolution #1308 #1482]: #1147
#1490 := (or #477 #1150 #1489 #1365 #1112 #1049 #241 #1409 #288)
#1491 := [th-lemma]: #1490
#1492 := [unit-resolution #1491 #1405 #1468 #776 #1488 #824 #1483 #850 #1406]: #477
#1493 := [unit-resolution #1222 #1492]: #1203
#1494 := [unit-resolution #1326 #1493]: #1198
#1495 := [unit-resolution #1310 #1482]: #1149
#1500 := [unit-resolution #1499 #1475 #698 #724 #1497 #772 #1447 #802 #1496 #828 #1495 #854 #1494 #876 #1480]: #516
#1501 := [unit-resolution #1236 #1479]: #919
#1502 := [unit-resolution #1328 #1493]: #1199
#1508 := [unit-resolution #1248 #1474]: #957
#1514 := [unit-resolution #1513 #1508 #694 #720 #1468 #776 #1507 #798 #1488 #824 #1483 #850 #1502 #880 #1501]: #515
#1517 := [unit-resolution #1516 #1480 #698 #1475 #724 #1406]: #100
#1518 := [unit-resolution #917 #1517]: #887
#1519 := [unit-resolution #1226 #1518]: #883
#1526 := [unit-resolution #1525 #1480 #672 #698 #1521 #746 #1468 #776 #1488 #824 #1483 #850 #1519]: #509
#1527 := [unit-resolution #1224 #1518]: #881
#1531 := [unit-resolution #1530 #1501 #668 #694 #1404 #750 #1497 #772 #1496 #828 #1495 #854 #1527]: #506
#1532 := [unit-resolution #646 #1531 #1526 #1514 #1500]: false
#1534 := [lemma #1532]: #1533
#1598 := [unit-resolution #1534 #1406]: #288
#1599 := [unit-resolution #1069 #1598]: #1039
#1271 := (or #1038 #1033)
#1272 := [def-axiom]: #1271
#1600 := [unit-resolution #1272 #1599]: #1033
#1601 := [unit-resolution #1236 #1588]: #919
#1602 := (or #506 #884 #1528 #1364 #1011 #1365 #1112 #1337 #1357 #922 #1510 #1036 #1163 #1074 #1358)
#1603 := [th-lemma]: #1602
#1604 := [unit-resolution #1603 #1601 #668 #694 #1404 #750 #1600 #772 #1507 #798 #1488 #824 #1597 #854 #1592]: #506
#1605 := [unit-resolution #1226 #1591]: #883
#1313 := (or #1164 #1160)
#1314 := [def-axiom]: #1313
#1606 := [unit-resolution #1314 #1596]: #1160
#1607 := (or #509 #885 #1522 #1523 #1010 #1343 #1113 #1489 #1409 #923 #1371 #1037 #1162 #1075 #1350)
#1608 := [th-lemma]: #1607
#1609 := [unit-resolution #1608 #1589 #672 #698 #1521 #746 #1459 #776 #1447 #802 #1496 #828 #1606 #850 #1605]: #509
#1610 := (or #476 #1036 #1337 #1365 #1112 #1357 #194 #1364 #1011 #1163 #1074 #1358)
#1611 := [th-lemma]: #1610
#1612 := [unit-resolution #1611 #1597 #750 #1600 #772 #1507 #798 #1488 #824 #1404 #854 #1535]: #476
#1221 := [not-or-elim #1220]: #1194
#1613 := [unit-resolution #1221 #1612]: #1191
#1319 := (or #1190 #1185)
#1320 := [def-axiom]: #1319
#1614 := [unit-resolution #1320 #1613]: #1185
#1615 := (or #516 #923 #1373 #1371 #1372 #1075 #1350 #1489 #1409 #1037 #973 #1162 #1188 #1343 #1113 #1523 #1010)
#1616 := [th-lemma]: #1615
#1617 := [unit-resolution #1616 #1606 #1440 #724 #1521 #746 #1459 #776 #1447 #802 #1496 #828 #698 #850 #1614 #876 #1589]: #516
#1321 := (or #1190 #1187)
#1322 := [def-axiom]: #1321
#1618 := [unit-resolution #1322 #1613]: #1187
#1619 := [unit-resolution #994 #1535]: #975
#1253 := (or #974 #970)
#1254 := [def-axiom]: #1253
#1620 := [unit-resolution #1254 #1619]: #970
#1621 := (or #515 #922 #1509 #1510 #1511 #1074 #1358 #1337 #1357 #1036 #972 #1163 #1189 #1365 #1112 #1364 #1011)
#1622 := [th-lemma]: #1621
#1623 := [unit-resolution #1622 #1620 #694 #720 #1404 #750 #1600 #772 #1507 #798 #1488 #824 #1597 #854 #1618 #880 #1601]: #515
#1624 := [unit-resolution #646 #1623 #1617 #1609 #1604]: false
#1626 := [lemma #1624]: #1625
#1658 := [unit-resolution #1626 #1406]: #194
#1659 := [unit-resolution #993 #1658]: #963
#1660 := [unit-resolution #1250 #1659]: #959
#1661 := [unit-resolution #1563 #1660 #1658 #724 #1406]: #147
#1662 := [unit-resolution #955 #1661]: #925
#1663 := [unit-resolution #1238 #1662]: #921
#1664 := [unit-resolution #1516 #1663 #698 #1660 #724 #1406]: #100
#1665 := [unit-resolution #917 #1664]: #887
#1666 := [unit-resolution #1226 #1665]: #883
#1667 := [unit-resolution #1224 #1665]: #881
#1668 := [unit-resolution #1236 #1662]: #919
#1669 := [unit-resolution #1248 #1659]: #957
#1655 := (or #429 #1113 #1010 #960 #1036 #1074 #1112 #922 #923 #884 #885)
#1632 := [hypothesis]: #919
#1636 := [hypothesis]: #881
#1638 := [hypothesis]: #1071
#1639 := [hypothesis]: #1033
#1334 := [unit-resolution #1184 #1333]: #1165
#1335 := [unit-resolution #1316 #1334]: #1161
#1640 := [unit-resolution #1603 #1335 #668 #694 #1404 #750 #1639 #772 #1638 #798 #1637 #824 #1632 #854 #1636]: #506
#1641 := [hypothesis]: #883
#1642 := [hypothesis]: #921
#1643 := [hypothesis]: #1111
#1644 := [hypothesis]: #1008
#1631 := [unit-resolution #1314 #1334]: #1160
#1645 := [unit-resolution #1608 #1631 #672 #698 #1644 #746 #1459 #776 #1447 #802 #1643 #828 #1642 #850 #1641]: #509
#1634 := (or #1202 #922 #960 #632 #631 #429)
#1627 := [hypothesis]: #506
#1628 := [hypothesis]: #509
#1384 := [hypothesis]: #1203
#1396 := (or #1202 #516 #429)
#1331 := [hypothesis]: #634
#1385 := [unit-resolution #1326 #1384]: #1198
#1382 := (or #1189 #1200 #516 #429)
#1332 := [hypothesis]: #1198
#1336 := [hypothesis]: #1187
#1338 := (or #382 #1189 #1337 #429 #1163 #1200)
#1339 := [th-lemma]: #1338
#1340 := [unit-resolution #1339 #1336 #1335 #854 #1333 #1332]: #382
#1341 := [unit-resolution #1145 #1340]: #1115
#1342 := [unit-resolution #1298 #1341]: #1111
#1344 := (or #335 #1113 #429 #1343 #1189 #1337 #1163 #1200)
#1345 := [th-lemma]: #1344
#1346 := [unit-resolution #1345 #1342 #828 #1333 #1335 #854 #1336 #1332]: #335
#1347 := [unit-resolution #1107 #1346]: #1077
#1348 := [unit-resolution #1284 #1347]: #1071
#1349 := [unit-resolution #1286 #1347]: #1073
#1353 := [unit-resolution #1352 #1349 #802 #1342 #828 #1333]: #288
#1354 := [unit-resolution #1069 #1353]: #1039
#1355 := [unit-resolution #1272 #1354]: #1033
#1356 := [unit-resolution #1296 #1341]: #1109
#1359 := (or #242 #1036 #1357 #429 #1189 #1337 #1163 #1200 #1074 #1358)
#1360 := [th-lemma]: #1359
#1361 := [unit-resolution #1360 #1355 #772 #1348 #798 #1333 #1335 #854 #1336 #1332]: #242
#1362 := [unit-resolution #1032 #1361]: #1013
#1363 := [unit-resolution #1268 #1362]: #1009
#1366 := (or #194 #1011 #1364 #1074 #1358 #1112 #1365 #1036 #1357 #1189 #1337 #1163 #1200)
#1367 := [th-lemma]: #1366
#1368 := [unit-resolution #1367 #1363 #750 #1355 #772 #1348 #798 #1356 #824 #1335 #854 #1336 #1332]: #194
#1369 := [unit-resolution #993 #1368]: #963
#1370 := [unit-resolution #1250 #1369]: #959
#1374 := (or #923 #1371 #516 #1372 #1200 #961 #1373 #1036 #1357 #1337 #1163 #1074 #1358)
#1375 := [th-lemma]: #1374
#1376 := [unit-resolution #1375 #1370 #698 #724 #1355 #772 #1348 #798 #1335 #854 #1332 #876 #1331]: #923
#1377 := (or #147 #195 #961 #1373 #1036 #1357 #429 #1189 #1337 #1163 #1200 #1074 #1358)
#1378 := [th-lemma]: #1377
#1379 := [unit-resolution #1378 #1368 #1370 #724 #1355 #772 #1348 #798 #1333 #1335 #854 #1336 #1332]: #147
#1380 := [unit-resolution #955 #1379]: #925
#1381 := [unit-resolution #1238 #1380 #1376]: false
#1383 := [lemma #1381]: #1382
#1386 := [unit-resolution #1383 #1385 #1331 #1333]: #1189
#1387 := [unit-resolution #1322 #1386]: #1190
#1388 := [unit-resolution #1328 #1384]: #1199
#1389 := (or #1187 #1185)
#1390 := [th-lemma]: #1389
#1391 := [unit-resolution #1390 #1386]: #1185
#1392 := (or #476 #1188 #1201)
#1393 := [th-lemma]: #1392
#1394 := [unit-resolution #1393 #1391 #1388]: #476
#1395 := [unit-resolution #1221 #1394 #1387]: false
#1397 := [lemma #1395]: #1396
#1629 := [unit-resolution #1397 #1384 #1333]: #516
#1630 := [unit-resolution #646 #1629 #1628 #1627]: #633
#1633 := [th-lemma #1632 #720 #694 #880 #1447 #802 #850 #776 #1459 #1631 #1536 #1388 #1630]: false
#1635 := [lemma #1633]: #1634
#1646 := [unit-resolution #1635 #1645 #1536 #1632 #1640 #1333]: #1202
#1647 := [unit-resolution #1222 #1646]: #476
#1648 := [unit-resolution #1221 #1647]: #1191
#1649 := [unit-resolution #1322 #1648]: #1187
#1650 := [unit-resolution #1320 #1648]: #1185
#1651 := [unit-resolution #1616 #1650 #1440 #724 #1644 #746 #1459 #776 #1447 #802 #1643 #828 #698 #850 #1631 #876 #1642]: #516
#1652 := [unit-resolution #646 #1651 #1645 #1640]: #633
#1653 := [unit-resolution #1622 #1652 #694 #720 #1404 #750 #1639 #772 #1638 #798 #1637 #824 #1335 #854 #1649 #880 #1632]: #972
#1654 := [th-lemma #1459 #1647 #850 #828 #1643 #776 #746 #1644 #1631 #1447 #802 #1536 #1653]: false
#1656 := [lemma #1654]: #1655
#1670 := [unit-resolution #1656 #1496 #1521 #1669 #1600 #1507 #1488 #1668 #1663 #1667 #1666]: #429
#1671 := [th-lemma #1600 #1670 #824 #1507 #798 #1488 #1657]: false
#1672 := [lemma #1671]: #241
#1683 := [unit-resolution #1031 #1672]: #1001
#1703 := [unit-resolution #1262 #1683]: #997
#1920 := (or #194 #242 #1364 #999 #288)
#1921 := [th-lemma]: #1920
#1922 := [unit-resolution #1921 #1405 #1703 #750 #1672]: #194
#1923 := [unit-resolution #993 #1922]: #963
#1924 := [unit-resolution #1248 #1923]: #957
#1925 := [unit-resolution #1250 #1923]: #959
#1843 := (or #288 #961 #147)
#1763 := [hypothesis]: #148
#1828 := [hypothesis]: #959
#1842 := [th-lemma #724 #750 #1703 #1828 #1405 #1763]: false
#1844 := [lemma #1842]: #1843
#1926 := [unit-resolution #1844 #1925 #1405]: #147
#1927 := [unit-resolution #955 #1926]: #925
#1928 := [unit-resolution #1236 #1927]: #919
#2116 := [unit-resolution #1310 #2047]: #1149
#2084 := (or #288 #516)
#2050 := (or #288 #961 #516)
#2037 := [hypothesis]: #1087
#2038 := [unit-resolution #1292 #2037]: #1088
#2041 := (or #1085 #336)
#2039 := (or #1085 #1075 #336)
#2040 := [th-lemma]: #2039
#2042 := [unit-resolution #2040 #1447]: #2041
#2043 := [unit-resolution #2042 #2037]: #336
#2044 := [unit-resolution #1108 #2043 #2038]: false
#2045 := [lemma #2044]: #1085
#2035 := (or #1087 #1150 #961 #1048 #516)
#1845 := [hypothesis]: #1085
#1874 := [hypothesis]: #477
#1901 := (or #335 #476)
#1895 := [unit-resolution #1222 #1874]: #1203
#1896 := [unit-resolution #1326 #1895]: #1198
#1893 := (or #429 #1200)
#1880 := (or #335 #1113 #429 #1163 #1200)
#1857 := [hypothesis]: #1189
#1858 := [unit-resolution #1322 #1857]: #1190
#1859 := [unit-resolution #1221 #1858]: #477
#1860 := [unit-resolution #1222 #1859]: #1203
#1861 := [unit-resolution #1390 #1857]: #1185
#1862 := [unit-resolution #1393 #1859 #1861]: #1201
#1863 := [unit-resolution #1328 #1862 #1860]: false
#1864 := [lemma #1863]: #1187
#1878 := (or #335 #1113 #429 #1189 #1163 #1200)
#1879 := [unit-resolution #1345 #828 #854]: #1878
#1881 := [unit-resolution #1879 #1864]: #1880
#1882 := [unit-resolution #1881 #1335 #1870 #1333 #1332]: #335
#1883 := [unit-resolution #1107 #1882]: #1077
#1884 := [unit-resolution #1689 #1333 #1870]: #288
#1885 := [unit-resolution #1069 #1884]: #1039
#1886 := [unit-resolution #1272 #1885]: #1033
#1889 := (or #1036 #429 #1163 #1200 #1074)
#1887 := (or #242 #1036 #429 #1189 #1163 #1200 #1074)
#1888 := [unit-resolution #1360 #772 #798 #854]: #1887
#1890 := [unit-resolution #1888 #1672 #1864]: #1889
#1891 := [unit-resolution #1890 #1886 #1332 #1333 #1335]: #1074
#1892 := [unit-resolution #1284 #1891 #1883]: false
#1894 := [lemma #1892]: #1893
#1897 := [unit-resolution #1894 #1896]: #429
#1898 := [unit-resolution #1183 #1897]: #1153
#1899 := [unit-resolution #1310 #1898]: #1149
#1900 := [th-lemma #854 #1899 #1870 #828 #1422 #1874]: false
#1902 := [lemma #1900]: #1901
#1950 := [unit-resolution #1902 #1874]: #335
#1951 := [unit-resolution #1107 #1950]: #1077
#1952 := [unit-resolution #1284 #1951]: #1071
#1953 := [unit-resolution #1328 #1895]: #1199
#1876 := (or #1109 #476)
#1673 := [hypothesis]: #1112
#1760 := (or #429 #1109)
#1674 := [unit-resolution #1296 #1673]: #1114
#1675 := [unit-resolution #1145 #1674]: #383
#1676 := [unit-resolution #1146 #1675]: #1127
#1677 := [unit-resolution #1304 #1676]: #1123
#1687 := [unit-resolution #1686 #1673]: #1111
#1743 := [unit-resolution #1689 #1333 #1687]: #288
#1744 := [unit-resolution #1069 #1743]: #1039
#1745 := [unit-resolution #1272 #1744]: #1033
#1678 := (or #335 #1343 #429 #382 #1125)
#1679 := [th-lemma]: #1678
#1746 := [unit-resolution #1679 #1333 #1675 #828 #1677]: #335
#1747 := [unit-resolution #1107 #1746]: #1077
#1748 := [unit-resolution #1284 #1747]: #1071
#1259 := (or #1000 #995)
#1260 := [def-axiom]: #1259
#1684 := [unit-resolution #1260 #1683]: #995
#1693 := (or #147 #1373 #1343 #1074 #1358 #1523 #429 #973 #998 #1036 #1357 #1125)
#1694 := [th-lemma]: #1693
#1749 := [unit-resolution #1694 #1745 #724 #1684 #746 #1440 #772 #1748 #798 #1677 #828 #1333]: #147
#1750 := [unit-resolution #955 #1749]: #925
#1751 := [unit-resolution #1238 #1750]: #921
#1714 := (or #100 #923 #1373 #1371 #1343 #1523 #1074 #1358 #973 #429 #382 #1036 #1357 #998 #1125)
#1715 := [th-lemma]: #1714
#1752 := [unit-resolution #1715 #1751 #698 #1440 #724 #1684 #746 #1675 #772 #1748 #798 #1745 #1677 #828 #1333]: #100
#1753 := [unit-resolution #1236 #1750]: #919
#1727 := (or #1109 #429 #972)
#1680 := [unit-resolution #1679 #1675 #1677 #828 #1333]: #335
#1681 := [unit-resolution #1107 #1680]: #1077
#1682 := [unit-resolution #1284 #1681]: #1071
#1690 := [unit-resolution #1689 #1687 #1333]: #288
#1691 := [unit-resolution #1069 #1690]: #1039
#1692 := [unit-resolution #1272 #1691]: #1033
#1695 := [unit-resolution #1694 #1692 #724 #1684 #746 #1440 #772 #1682 #798 #1677 #828 #1333]: #147
#1696 := [unit-resolution #955 #1695]: #925
#1697 := [unit-resolution #1236 #1696]: #919
#1698 := (or #476 #429 #1337 #1163 #382)
#1699 := [th-lemma]: #1698
#1700 := [unit-resolution #1699 #1675 #1335 #854 #1333]: #476
#1701 := [unit-resolution #1221 #1700]: #1191
#1702 := [unit-resolution #1322 #1701]: #1187
#1704 := [hypothesis]: #970
#1301 := (or #1126 #1122)
#1302 := [def-axiom]: #1301
#1705 := [unit-resolution #1302 #1676]: #1122
#1706 := (or #515 #922 #1509 #1510 #1511 #1075 #1350 #1337 #1409 #1037 #1163 #1365 #1364 #972 #999 #1124 #1189)
#1707 := [th-lemma]: #1706
#1708 := [unit-resolution #1707 #1705 #1704 #720 #1703 #750 #1459 #776 #1447 #802 #694 #824 #1335 #854 #1702 #880 #1697]: #515
#1709 := [unit-resolution #1238 #1696]: #921
#1710 := [unit-resolution #1320 #1701]: #1185
#1711 := (or #516 #923 #1373 #1371 #1372 #1074 #1358 #1489 #1357 #1036 #1162 #1343 #1523 #973 #998 #1125 #1188)
#1712 := [th-lemma]: #1711
#1713 := [unit-resolution #1712 #1692 #1440 #724 #1684 #746 #698 #772 #1682 #798 #1677 #828 #1631 #850 #1710 #876 #1709]: #516
#1716 := [unit-resolution #1715 #1709 #698 #1440 #724 #1684 #746 #1692 #772 #1682 #798 #1675 #1677 #828 #1333]: #100
#1717 := [unit-resolution #917 #1716]: #887
#1718 := [unit-resolution #1226 #1717]: #883
#1719 := (or #509 #885 #1522 #1523 #1343 #1489 #1357 #923 #1371 #1036 #1162 #998 #1125)
#1720 := [th-lemma]: #1719
#1721 := [unit-resolution #1720 #1709 #672 #698 #1684 #746 #1692 #772 #1677 #828 #1631 #850 #1718]: #509
#1722 := [unit-resolution #1224 #1717]: #881
#1723 := (or #506 #884 #1528 #1364 #1365 #1337 #1409 #922 #1510 #1037 #1163 #999 #1124)
#1724 := [th-lemma]: #1723
#1725 := [unit-resolution #1724 #1697 #668 #694 #1703 #750 #1459 #776 #1705 #824 #1335 #854 #1722]: #506
#1726 := [unit-resolution #646 #1725 #1721 #1713 #1708]: false
#1728 := [lemma #1726]: #1727
#1754 := [unit-resolution #1728 #1333 #1673]: #972
#1755 := [unit-resolution #1254 #1754]: #974
#1756 := [unit-resolution #994 #1755]: #194
#1757 := [unit-resolution #993 #1756]: #963
#1758 := [unit-resolution #1248 #1757]: #957
#1759 := [th-lemma #1758 #1753 #720 #694 #1675 #1459 #776 #1447 #802 #1752]: false
#1761 := [lemma #1759]: #1760
#1871 := [unit-resolution #1761 #1673]: #429
#1872 := [unit-resolution #1183 #1871]: #1153
#1873 := [unit-resolution #1310 #1872]: #1149
#1875 := [th-lemma #1675 #1874 #854 #1873 #1871]: false
#1877 := [lemma #1875]: #1876
#1954 := [unit-resolution #1877 #1874]: #1109
#1948 := (or #288 #1112 #1200 #1201 #1074)
#1917 := [unit-resolution #1894 #1332]: #429
#1918 := [unit-resolution #1183 #1917]: #1153
#1919 := [unit-resolution #1308 #1918]: #1147
#1929 := [unit-resolution #1310 #1918]: #1149
#1930 := [unit-resolution #1238 #1927]: #921
#1931 := [hypothesis]: #1199
#1932 := (or #515 #922 #1201 #1074 #1112 #960 #1150)
#1933 := [unit-resolution #1513 #694 #720 #1468 #776 #798 #824 #850 #880]: #1932
#1934 := [unit-resolution #1933 #1928 #1931 #1637 #1638 #1919 #1924]: #515
#1935 := (or #516 #923 #1200 #1113 #961 #1151 #1048)
#1936 := [unit-resolution #1499 #698 #724 #772 #1447 #802 #828 #854 #876]: #1935
#1937 := [unit-resolution #1936 #1930 #1870 #1332 #1929 #1497 #1925]: #516
#1915 := (or #898 #634 #633 #923 #961 #1048 #1151 #922 #960 #1112 #1150)
#1903 := [hypothesis]: #515
#1904 := [hypothesis]: #516
#1905 := [hypothesis]: #899
#1906 := [unit-resolution #1232 #1905]: #895
#1907 := (or #509 #1522 #1523 #897 #998 #1489 #1150 #960 #1509 #1112 #1365 #1049 #922 #1510 #1409)
#1908 := [th-lemma]: #1907
#1909 := [unit-resolution #1908 #1906 #1632 #694 #1536 #720 #1684 #746 #1468 #776 #1637 #824 #1540 #850 #672]: #509
#1774 := [hypothesis]: #1149
#1229 := (or #898 #894)
#1230 := [def-axiom]: #1229
#1910 := [unit-resolution #1230 #1905]: #894
#1911 := (or #506 #1528 #1364 #896 #999 #1337 #1151 #961 #1373 #1113 #1343 #1048 #923 #1371 #1357)
#1912 := [th-lemma]: #1911
#1913 := [unit-resolution #1912 #1910 #1642 #698 #1828 #724 #1703 #750 #1545 #772 #1870 #828 #1774 #854 #668]: #506
#1914 := [unit-resolution #646 #1913 #1909 #1904 #1903]: false
#1916 := [lemma #1914]: #1915
#1938 := [unit-resolution #1916 #1937 #1934 #1930 #1925 #1497 #1929 #1928 #1924 #1637 #1919]: #898
#1939 := [unit-resolution #918 #1938]: #100
#1940 := [unit-resolution #917 #1939]: #887
#1941 := [unit-resolution #1224 #1940]: #881
#1942 := (or #506 #884 #1113 #1151 #1048 #922)
#1943 := [unit-resolution #1530 #668 #694 #1404 #750 #772 #828 #854]: #1942
#1944 := [unit-resolution #1943 #1941 #1497 #1870 #1929 #1928]: #506
#1945 := [unit-resolution #646 #1944 #1937 #1934]: #632
#1946 := [unit-resolution #1908 #1945 #1928 #694 #1924 #720 #1684 #746 #1468 #776 #1637 #824 #1919 #850 #672]: #897
#1947 := [th-lemma #1946 #1939 #1742]: false
#1949 := [lemma #1947]: #1948
#1955 := [unit-resolution #1949 #1954 #1896 #1953 #1952]: #288
#1956 := [unit-resolution #1069 #1955]: #1039
#1957 := [unit-resolution #1272 #1956]: #1033
#1958 := [unit-resolution #1735 #1954]: #382
#1959 := (or #1123 #383 #1113)
#1960 := [th-lemma]: #1959
#1961 := [unit-resolution #1960 #1958 #1870]: #1123
#1962 := [unit-resolution #1308 #1898]: #1147
#1965 := (or #1160 #1112 #1074 #289 #1150)
#1963 := (or #1160 #1365 #1112 #1074 #1358 #289 #1150)
#1964 := [th-lemma]: #1963
#1966 := [unit-resolution #1964 #798 #824]: #1965
#1967 := [unit-resolution #1966 #1955 #1954 #1962 #1952]: #1160
#1970 := (or #1162 #1151 #1036 #1125 #147 #1074)
#1968 := (or #1162 #1151 #1343 #1523 #998 #1036 #1357 #1125 #973 #147 #1373 #1074 #1358)
#1969 := [th-lemma]: #1968
#1971 := [unit-resolution #1969 #724 #1684 #746 #1440 #772 #798 #828]: #1970
#1972 := [unit-resolution #1971 #1967 #1952 #1961 #1899 #1957]: #147
#1973 := [unit-resolution #955 #1972]: #925
#1974 := [unit-resolution #1236 #1973]: #919
#1975 := (or #1161 #1151 #430)
#1976 := [th-lemma]: #1975
#1977 := [unit-resolution #1976 #1899 #1897]: #1161
#1978 := (or #476 #1036 #1112 #194 #1163 #1074)
#1979 := [unit-resolution #1611 #750 #772 #798 #824 #1404 #854]: #1978
#1980 := [unit-resolution #1979 #1957 #1874 #1954 #1952 #1977]: #194
#1981 := [unit-resolution #993 #1980]: #963
#1982 := [unit-resolution #1248 #1981]: #957
#1983 := [unit-resolution #1933 #1974 #1953 #1954 #1952 #1962 #1982]: #515
#1984 := [unit-resolution #1238 #1973]: #921
#1985 := [unit-resolution #1250 #1981]: #959
#1849 := (or #923 #516 #1200 #961 #1036 #1163 #1074)
#1850 := [unit-resolution #1375 #698 #724 #772 #798 #854 #876]: #1849
#1986 := [unit-resolution #1850 #1985 #1896 #1952 #1977 #1957 #1984]: #516
#1987 := (or #509 #923 #1036 #1162 #1125)
#1988 := [unit-resolution #1720 #672 #698 #1684 #746 #1742 #772 #828 #850]: #1987
#1989 := [unit-resolution #1988 #1984 #1961 #1967 #1957]: #509
#1990 := [unit-resolution #646 #1989 #1986 #1983]: #631
#1991 := (or #506 #884 #1112 #922 #1036 #1163 #1074)
#1992 := [unit-resolution #1603 #668 #694 #1404 #750 #772 #798 #824 #854]: #1991
#1993 := [unit-resolution #1992 #1990 #1977 #1954 #1952 #1957 #1974]: #884
#1994 := [unit-resolution #1224 #1993]: #886
#1995 := [unit-resolution #917 #1994]: #101
#1996 := [th-lemma #746 #1684 #1957 #1874 #854 #1899 #1870 #828 #1984 #1995 #698 #772 #1972]: false
#1997 := [lemma #1996]: #476
#2014 := [unit-resolution #1221 #1997]: #1191
#2015 := [unit-resolution #1320 #2014]: #1185
#2034 := [th-lemma #876 #850 #1540 #2015 #802 #2033 #698 #772 #1828 #724 #1545 #1845 #1331]: false
#2036 := [lemma #2034]: #2035
#2048 := [unit-resolution #2036 #1497 #2045 #1828 #1331]: #1150
#2049 := [unit-resolution #1308 #2048 #2047]: false
#2051 := [lemma #2049]: #2050
#2082 := [unit-resolution #2051 #1405 #1331]: #961
#2083 := [unit-resolution #1250 #1923 #2082]: false
#2085 := [lemma #2083]: #2084
#2089 := [unit-resolution #2085 #1331]: #288
#2090 := [unit-resolution #1069 #2089]: #1039
#2091 := [unit-resolution #1272 #2090]: #1033
#2065 := [hypothesis]: #935
#2066 := [unit-resolution #1244 #2065]: #936
#2067 := [unit-resolution #956 #2066]: #147
#2068 := [th-lemma #2065 #2033 #2067]: false
#2069 := [lemma #2068]: #933
#2100 := (or #429 #516)
#2063 := (or #429 #1086 #516)
#2052 := [unit-resolution #1761 #1333]: #1109
#2053 := [unit-resolution #1735 #2052]: #382
#2054 := [hypothesis]: #1084
#2055 := (or #1200 #516 #429)
#2056 := [unit-resolution #1383 #1864]: #2055
#2057 := [unit-resolution #2056 #1333 #1331]: #1200
#2060 := (or #1086 #383 #1113 #1188 #1162 #1198)
#2058 := (or #1086 #383 #1113 #1343 #1188 #1489 #1162 #1198 #1075)
#2059 := [th-lemma]: #2058
#2061 := [unit-resolution #2059 #1447 #828 #850]: #2060
#2062 := [unit-resolution #2061 #1631 #2057 #2015 #1870 #2054 #2053]: false
#2064 := [lemma #2062]: #2063
#2086 := [unit-resolution #2064 #1333 #1331]: #1086
#2087 := [unit-resolution #1290 #2086]: #1088
#2088 := [unit-resolution #1108 #2087]: #335
#2080 := (or #1109 #516)
#2070 := [unit-resolution #1308 #1872]: #1147
#2020 := (or #194 #1150 #516 #1125 #1151 #1124)
#1762 := [hypothesis]: #1122
#1775 := [hypothesis]: #1123
#1803 := (or #194 #1151 #1150 #1125 #147 #1124)
#1764 := [unit-resolution #956 #1763]: #937
#1765 := [unit-resolution #1244 #1764]: #933
#1766 := (or #509 #885 #1522 #1364 #1365 #1489 #999 #1124 #1371 #1037 #1409 #935 #1150 #972 #1509 #1075 #1350)
#1767 := [th-lemma]: #1766
#1768 := [unit-resolution #1767 #1620 #1765 #698 #672 #720 #1703 #750 #1459 #776 #1447 #802 #1762 #824 #1540 #850 #1742]: #509
#1769 := (or #100 #1371 #935 #194 #147)
#1770 := [th-lemma]: #1769
#1771 := [unit-resolution #1770 #1535 #1765 #698 #1763]: #100
#1772 := [unit-resolution #917 #1771]: #887
#1773 := [unit-resolution #1224 #1772]: #881
#1776 := (or #335 #194 #1364 #1037 #1409 #999)
#1777 := [th-lemma]: #1776
#1778 := [unit-resolution #1777 #1535 #750 #1459 #776 #1703]: #335
#1779 := [unit-resolution #1107 #1778]: #1077
#1780 := [unit-resolution #1284 #1779]: #1071
#1241 := (or #936 #932)
#1242 := [def-axiom]: #1241
#1781 := [unit-resolution #1242 #1764]: #932
#1782 := (or #288 #1364 #999 #973 #147 #1373 #194)
#1783 := [th-lemma]: #1782
#1784 := [unit-resolution #1783 #1535 #1440 #724 #1703 #750 #1763]: #288
#1785 := [unit-resolution #1069 #1784]: #1039
#1786 := [unit-resolution #1272 #1785]: #1033
#1787 := (or #506 #884 #1528 #1523 #1343 #1337 #998 #1125 #1510 #1036 #1357 #934 #1151 #973 #1373 #1074 #1358)
#1788 := [th-lemma]: #1787
#1789 := [unit-resolution #1788 #1786 #1781 #694 #1440 #724 #1684 #746 #668 #772 #1780 #798 #1775 #828 #1774 #854 #1773]: #506
#1790 := (or #476 #1337 #1343 #1523 #1036 #1357 #998 #1125 #973 #147 #1373 #1074 #1358 #1151 #194)
#1791 := [th-lemma]: #1790
#1792 := [unit-resolution #1791 #1535 #1440 #724 #1684 #746 #1786 #772 #1780 #798 #1775 #828 #1774 #854 #1763]: #476
#1793 := [unit-resolution #1221 #1792]: #1191
#1794 := [unit-resolution #1320 #1793]: #1185
#1795 := (or #516 #1372 #1489 #1409 #1037 #1188 #1371 #935 #972 #1509 #1075 #1350 #1150)
#1796 := [th-lemma]: #1795
#1797 := [unit-resolution #1796 #1620 #698 #720 #1459 #776 #1447 #802 #1540 #850 #1794 #876 #1765]: #516
#1798 := [unit-resolution #1322 #1793]: #1187
#1799 := (or #515 #1511 #1337 #1357 #1036 #1189 #1510 #934 #973 #1373 #1074 #1358 #1151)
#1800 := [th-lemma]: #1799
#1801 := [unit-resolution #1800 #1786 #1440 #724 #694 #772 #1780 #798 #1774 #854 #1798 #880 #1781]: #515
#1802 := [unit-resolution #646 #1801 #1797 #1789 #1768]: false
#1804 := [lemma #1802]: #1803
#2011 := [unit-resolution #1804 #1535 #1540 #1775 #1774 #1762]: #147
#2012 := [unit-resolution #955 #2011]: #925
#2013 := [unit-resolution #1238 #2012]: #921
#2016 := (or #516 #1188 #935 #972 #1150)
#2017 := [unit-resolution #1796 #698 #720 #1459 #776 #1447 #802 #850 #876]: #2016
#2018 := [unit-resolution #2017 #1620 #2015 #1540 #1331]: #935
#2019 := [th-lemma #2018 #2013 #2011]: false
#2021 := [lemma #2019]: #2020
#2071 := [unit-resolution #2021 #2070 #1331 #1677 #1873 #1705]: #194
#2072 := [unit-resolution #993 #2071]: #963
#2073 := [unit-resolution #2010 #1675]: #288
#2074 := [unit-resolution #1069 #2073]: #1039
#2075 := [unit-resolution #1272 #2074]: #1033
#2076 := (or #516 #1036 #1188 #935 #1150 #960 #1087)
#1823 := (or #516 #1372 #1489 #1357 #1036 #1188 #1371 #935 #1509 #1350 #1150 #960 #1523 #998 #1087)
#1824 := [th-lemma]: #1823
#2077 := [unit-resolution #1824 #720 #1684 #746 #698 #772 #802 #850 #876]: #2076
#2078 := [unit-resolution #2077 #2075 #2015 #2045 #2069 #1331 #2070]: #960
#2079 := [unit-resolution #1248 #2078 #2072]: false
#2081 := [lemma #2079]: #2080
#2092 := [unit-resolution #2081 #1331]: #1109
#2093 := [unit-resolution #1735 #2092]: #382
#2094 := [unit-resolution #1960 #2093 #1870]: #1123
#2095 := (or #516 #923 #1074 #1036 #1162 #1125 #1188)
#2096 := [unit-resolution #1712 #1440 #724 #1684 #746 #698 #772 #798 #828 #850 #876]: #2095
#2097 := [unit-resolution #2096 #1631 #2015 #2094 #1331 #2091 #2033]: #1074
#2098 := [unit-resolution #1284 #2097]: #1076
#2099 := [unit-resolution #1107 #2098 #2088]: false
#2101 := [lemma #2099]: #2100
#2102 := [unit-resolution #2101 #1331]: #429
#2103 := [unit-resolution #1183 #2102]: #1153
#2104 := [unit-resolution #1308 #2103]: #1147
#2105 := [unit-resolution #2077 #2104 #2015 #2045 #2069 #1331 #2091]: #960
#2106 := [unit-resolution #1248 #2105]: #962
#2107 := [unit-resolution #2017 #2104 #2015 #2069 #1331]: #972
#2108 := [unit-resolution #1254 #2107]: #974
#2109 := [unit-resolution #994 #2108]: #194
#2110 := [unit-resolution #993 #2109 #2106]: false
#2111 := [lemma #2110]: #516
#2127 := (or #1199 #1189 #477)
#2128 := [th-lemma]: #2127
#2129 := [unit-resolution #2128 #1864 #1997]: #1199
#2125 := (or #335 #288)
#1806 := [unit-resolution #1108 #1422]: #1089
#1829 := [unit-resolution #1290 #1806]: #1084
#2117 := (or #515 #1511 #1337 #1151 #1189 #1358 #922 #1510 #1409 #960 #1509 #1049 #1086)
#2118 := [th-lemma]: #2117
#2119 := [unit-resolution #2118 #1829 #1924 #720 #1468 #776 #694 #798 #2116 #854 #1864 #880 #1928]: #515
#2120 := (or #101 #922 #1510 #1409 #960 #1509 #1049 #335 #288)
#2121 := [th-lemma]: #2120
#2122 := [unit-resolution #2121 #1422 #694 #1924 #720 #1405 #1468 #776 #1928]: #101
#2123 := [unit-resolution #918 #2122]: #899
#2124 := [unit-resolution #1916 #2123 #2119 #2111 #1497 #1925 #2033 #2116 #1928 #1924 #2115 #2112]: false
#2126 := [lemma #2124]: #2125
#2130 := [unit-resolution #2126 #1405]: #335
#2131 := [unit-resolution #1107 #2130]: #1077
#2132 := [unit-resolution #1284 #2131]: #1071
#2133 := [unit-resolution #1933 #2132 #2129 #2115 #1928 #2112 #1924]: #515
#2134 := [unit-resolution #1916 #2133 #2111 #1497 #1925 #2033 #2116 #1928 #1924 #2115 #2112]: #898
#2135 := [unit-resolution #918 #2134]: #100
#2136 := [unit-resolution #917 #2135]: #887
#2137 := [unit-resolution #1224 #2136]: #881
#2138 := [unit-resolution #1943 #2137 #1497 #1870 #2116 #1928]: #506
#2139 := [unit-resolution #646 #2138 #2111 #2133]: #632
#2140 := [unit-resolution #1908 #2139 #1928 #694 #1924 #720 #1684 #746 #1468 #776 #2115 #824 #2112 #850 #672]: #897
#2141 := [th-lemma #2140 #2135 #1742]: false
#2142 := [lemma #2141]: #288
#2143 := [unit-resolution #1069 #2142]: #1039
#2144 := [unit-resolution #1272 #2143]: #1033
#2145 := [hypothesis]: #1150
#2146 := [unit-resolution #1308 #2145]: #1152
#2147 := [unit-resolution #1183 #2146]: #430
#2148 := [unit-resolution #1184 #2147]: #1165
#2149 := [unit-resolution #1314 #2148]: #1160
#2150 := [unit-resolution #1761 #2147]: #1109
#2151 := [unit-resolution #1735 #2150]: #382
#2152 := [unit-resolution #1960 #2151 #1870]: #1123
#2153 := [unit-resolution #1988 #2152 #2149 #2033 #2144]: #509
#2154 := (or #1149 #1147)
#2155 := [th-lemma]: #2154
#2156 := [unit-resolution #2155 #2145]: #1149
#2157 := [unit-resolution #1894 #2147]: #1200
#2158 := [unit-resolution #2061 #2149 #2015 #1870 #2157 #2151]: #1086
#2159 := [unit-resolution #1290 #2158]: #1088
#2160 := [unit-resolution #1108 #2159]: #335
#2161 := [unit-resolution #1107 #2160]: #1077
#2162 := [unit-resolution #1284 #2161]: #1071
#2163 := [unit-resolution #1971 #2162 #2149 #2152 #2156 #2144]: #147
#2164 := [unit-resolution #955 #2163]: #925
#2165 := [unit-resolution #1236 #2164]: #919
#2166 := [unit-resolution #1316 #2148]: #1161
#2167 := (or #100 #923 #1371 #1357 #1523 #998 #1036 #383 #429 #1343 #1113 #973 #1373 #1074 #1358)
#2168 := [th-lemma]: #2167
#2169 := [unit-resolution #2168 #2162 #698 #1440 #724 #1684 #746 #2144 #772 #2033 #798 #2151 #1870 #828 #2147]: #100
#2170 := [unit-resolution #917 #2169]: #887
#2171 := [unit-resolution #1224 #2170]: #881
#2172 := [unit-resolution #1992 #2171 #2166 #2150 #2162 #2144 #2165]: #506
#2173 := (or #195 #1357 #1523 #998 #1036 #383 #429 #1343 #1113)
#2174 := [th-lemma]: #2173
#2175 := [unit-resolution #2174 #2151 #746 #2144 #772 #1684 #1870 #828 #2147]: #195
#2176 := [unit-resolution #994 #2175]: #975
#2177 := [unit-resolution #1254 #2176]: #970
#2178 := (or #515 #922 #1074 #1036 #972 #1163 #1112)
#2179 := [unit-resolution #1622 #694 #720 #1404 #750 #772 #1864 #798 #824 #854 #880]: #2178
#2180 := [unit-resolution #2179 #2177 #2150 #2162 #2166 #2144 #2165]: #515
#2181 := [unit-resolution #646 #2180 #2172 #2111 #2153]: false
#2182 := [lemma #2181]: #1147
#1805 := [unit-resolution #1302 #1729]: #1122
#2231 := (or #194 #382)
#2183 := (or #1150 #429 #1163)
#2184 := [th-lemma]: #2183
#2185 := [unit-resolution #2184 #1333 #2182]: #1163
#2186 := [unit-resolution #1316 #2185 #1334]: false
#2187 := [lemma #2186]: #429
#2196 := [unit-resolution #1183 #2187]: #1153
#2197 := [unit-resolution #1310 #2196]: #1149
#1817 := [unit-resolution #1304 #1729]: #1123
#2217 := [unit-resolution #1804 #1535 #2182 #1817 #2197 #1805]: #147
#2218 := [unit-resolution #955 #2217]: #925
#2219 := [unit-resolution #1236 #2218]: #919
#2210 := [unit-resolution #1976 #2197 #2187]: #1161
#2220 := (or #509 #1124 #935 #1150 #972)
#2221 := [unit-resolution #1767 #698 #672 #720 #1703 #750 #1459 #776 #1447 #802 #824 #850 #1742]: #2220
#2222 := [unit-resolution #2221 #1620 #2069 #1805 #2182]: #509
#2223 := (or #515 #922 #1163 #972 #1124)
#2224 := [unit-resolution #1707 #720 #1703 #750 #1459 #776 #1447 #802 #694 #824 #854 #880 #1864]: #2223
#2225 := [unit-resolution #2224 #2219 #1805 #1620 #2210]: #515
#2226 := [unit-resolution #646 #2225 #2111 #2222]: #631
#2211 := (or #506 #884 #922 #1163 #1124)
#2212 := [unit-resolution #1724 #668 #694 #1703 #750 #1459 #776 #824 #854]: #2211
#2227 := [unit-resolution #2212 #2226 #1805 #2210 #2219]: #884
#2228 := [unit-resolution #1224 #2227]: #886
#2229 := [unit-resolution #917 #2228]: #101
#2230 := [th-lemma #1620 #720 #1459 #776 #1447 #802 #2033 #2229 #698 #1428 #2217]: false
#2232 := [lemma #2230]: #2231
#2242 := [unit-resolution #2232 #1428]: #194
#2243 := [unit-resolution #993 #2242]: #963
#2244 := [unit-resolution #1248 #2243]: #957
#2193 := (or #509 #1124 #1036 #935 #1150 #960 #1087)
#1814 := (or #509 #885 #1522 #1523 #1365 #1489 #998 #1124 #1371 #1036 #1357 #935 #1150 #1509 #1350 #960 #1087)
#1815 := [th-lemma]: #1814
#2194 := [unit-resolution #1815 #698 #720 #1684 #746 #672 #772 #802 #824 #850 #1742]: #2193
#2245 := [unit-resolution #2194 #2244 #2069 #2144 #2045 #1805 #2182]: #509
#2205 := (or #100 #935 #1036 #382 #960 #1087)
#1834 := (or #100 #1371 #935 #1523 #1036 #1357 #998 #1509 #382 #1350 #960 #1087)
#1835 := [th-lemma]: #1834
#2206 := [unit-resolution #1835 #698 #720 #1684 #746 #772 #802]: #2205
#2246 := [unit-resolution #2206 #2244 #2045 #2069 #2144 #1428]: #100
#2247 := [unit-resolution #917 #2246]: #887
#2248 := [unit-resolution #1224 #2247]: #881
#2215 := (or #335 #382)
#2188 := (or #335 #194)
#2189 := [unit-resolution #1777 #750 #1459 #776 #1703]: #2188
#2190 := [unit-resolution #2189 #1422]: #194
#2191 := [unit-resolution #993 #2190]: #963
#2192 := [unit-resolution #1248 #2191]: #957
#2195 := [unit-resolution #2194 #2192 #2069 #2144 #2045 #1805 #2182]: #509
#2198 := [unit-resolution #1250 #2191]: #959
#1840 := (or #335 #934 #1151 #961 #935 #960 #1150 #382)
#1807 := [unit-resolution #1292 #1806]: #1085
#1808 := [hypothesis]: #933
#1809 := (or #288 #382 #1350 #335 #1087)
#1810 := [th-lemma]: #1809
#1811 := [unit-resolution #1810 #1422 #1807 #802 #1428]: #288
#1812 := [unit-resolution #1069 #1811]: #1039
#1813 := [unit-resolution #1272 #1812]: #1033
#1816 := [unit-resolution #1815 #1813 #1808 #698 #1536 #720 #1684 #746 #672 #772 #1807 #802 #1805 #824 #1540 #850 #1742]: #509
#1818 := (or #476 #1337 #1343 #1125 #1151 #335 #382)
#1819 := [th-lemma]: #1818
#1820 := [unit-resolution #1819 #1422 #1817 #828 #1774 #854 #1428]: #476
#1821 := [unit-resolution #1221 #1820]: #1191
#1822 := [unit-resolution #1320 #1821]: #1185
#1825 := [unit-resolution #1824 #1813 #1536 #720 #1684 #746 #698 #772 #1807 #802 #1540 #850 #1822 #876 #1808]: #516
#1826 := [hypothesis]: #932
#1827 := [unit-resolution #1322 #1821]: #1187
#1830 := (or #515 #1511 #1337 #1409 #1037 #1189 #1510 #934 #1373 #1358 #1151 #961 #1364 #999 #1086)
#1831 := [th-lemma]: #1830
#1832 := [unit-resolution #1831 #1829 #1828 #724 #1703 #750 #1459 #776 #694 #798 #1774 #854 #1827 #880 #1826]: #515
#1833 := [unit-resolution #646 #1832 #1825 #1816]: #631
#1836 := [unit-resolution #1835 #1813 #698 #1536 #720 #1684 #746 #1808 #772 #1807 #802 #1428]: #100
#1837 := [unit-resolution #917 #1836]: #887
#1838 := [unit-resolution #1224 #1837]: #881
#1839 := [th-lemma #1838 #668 #750 #828 #854 #1703 #1817 #694 #1459 #776 #1826 #1774 #724 #798 #1828 #1829 #1833]: false
#1841 := [lemma #1839]: #1840
#2199 := [unit-resolution #1841 #2198 #2069 #1422 #2197 #2192 #2182 #1428]: #934
#2200 := [unit-resolution #1242 #2199]: #936
#2201 := [unit-resolution #956 #2200]: #147
#2202 := [unit-resolution #955 #2201]: #925
#2203 := [unit-resolution #1236 #2202]: #919
#2204 := [unit-resolution #2118 #2203 #1829 #720 #1468 #776 #694 #798 #2197 #854 #1864 #880 #2192]: #515
#2207 := [unit-resolution #2206 #2192 #2045 #2069 #2144 #1428]: #100
#2208 := [unit-resolution #917 #2207]: #887
#2209 := [unit-resolution #1224 #2208]: #881
#2213 := [unit-resolution #2212 #2203 #1805 #2210 #2209]: #506
#2214 := [unit-resolution #646 #2213 #2204 #2111 #2195]: false
#2216 := [lemma #2214]: #2215
#2249 := [unit-resolution #2216 #1428]: #335
#2250 := [unit-resolution #1107 #2249]: #1077
#2251 := [unit-resolution #1284 #2250]: #1071
#2252 := (or #1084 #1074 #1357 #1523 #998 #1036 #195)
#2253 := [th-lemma]: #2252
#2254 := [unit-resolution #2253 #2251 #746 #2144 #772 #1684 #2242]: #1084
#2255 := [unit-resolution #1250 #2243]: #959
#2240 := (or #934 #632 #884 #1074 #1125 #961 #1086)
#2233 := (or #515 #934 #1151 #961 #1086)
#2234 := [unit-resolution #1831 #1864 #724 #1703 #750 #1459 #776 #694 #798 #854 #880]: #2233
#2235 := [unit-resolution #2234 #1826 #2197 #1828 #2054]: #515
#2236 := (or #506 #884 #1125 #1036 #934 #1151 #1074)
#2237 := [unit-resolution #1788 #694 #1440 #724 #1684 #746 #668 #772 #798 #828 #854]: #2236
#2238 := [unit-resolution #2237 #1826 #1636 #1638 #1775 #2197 #2144]: #506
#2239 := [unit-resolution #646 #2238 #2235 #2111 #1628]: false
#2241 := [lemma #2239]: #2240
#2256 := [unit-resolution #2241 #2245 #2248 #2251 #1817 #2255 #2254]: #934
#2257 := [unit-resolution #1242 #2256]: #936
#2258 := [unit-resolution #956 #2257]: #147
#2259 := [unit-resolution #955 #2258]: #925
#2260 := [unit-resolution #1236 #2259]: #919
#2261 := [unit-resolution #2212 #2260 #1805 #2210 #2248]: #506
#2262 := [unit-resolution #2118 #2260 #2254 #720 #1468 #776 #694 #798 #2197 #854 #1864 #880 #2244]: #515
#2263 := [unit-resolution #646 #2262 #2261 #2111 #2245]: false
#2264 := [lemma #2263]: #382
#2265 := [unit-resolution #1145 #2264]: #1115
#2266 := [unit-resolution #1296 #2265]: #1109
#2267 := [unit-resolution #2189 #1535]: #335
#2268 := [unit-resolution #1107 #2267]: #1077
#2269 := [unit-resolution #1284 #2268]: #1071
#2270 := [unit-resolution #1966 #2269 #2142 #2266 #2182]: #1160
#2271 := (or #1008 #998 #1036 #1357 #1074 #1358 #383)
#2272 := [th-lemma]: #2271
#2273 := [unit-resolution #2272 #2269 #2144 #772 #1684 #798 #2264]: #1008
#2274 := (or #509 #1010 #1113 #923 #1162)
#2275 := [unit-resolution #1608 #672 #698 #1742 #746 #1459 #776 #1447 #802 #828 #850]: #2274
#2276 := [unit-resolution #2275 #2273 #1870 #2270 #2033]: #509
#2277 := [unit-resolution #1960 #2264 #1870]: #1123
#2278 := [unit-resolution #1971 #2270 #2269 #2277 #2197 #2144]: #147
#2279 := [unit-resolution #955 #2278]: #925
#2280 := [unit-resolution #1236 #2279]: #919
#2281 := (or #1010 #999 #923 #100 #1371 #961 #1373)
#2282 := [th-lemma]: #2281
#2283 := [unit-resolution #2282 #2273 #698 #1584 #724 #1703 #2033]: #100
#2284 := [unit-resolution #917 #2283]: #887
#2285 := [unit-resolution #1224 #2284]: #881
#2286 := [unit-resolution #1992 #2285 #2210 #2266 #2269 #2144 #2280]: #506
#2287 := [unit-resolution #2179 #2280 #2266 #1620 #2210 #2144 #2269]: #515
#2288 := [unit-resolution #646 #2287 #2286 #2111 #2276]: false
#2289 := [lemma #2288]: #194
#2305 := [unit-resolution #2253 #2302 #746 #2144 #772 #1684 #2289]: #1074
#2306 := [unit-resolution #1284 #2305]: #1076
#2307 := [unit-resolution #1107 #2306 #2304]: false
#2308 := [lemma #2307]: #1084
#2300 := (or #1086 #515)
#2290 := [hypothesis]: #633
#2291 := [unit-resolution #993 #2289]: #963
#2292 := [unit-resolution #1250 #2291]: #959
#2293 := [unit-resolution #2234 #2054 #2197 #2292 #2290]: #934
#2294 := [unit-resolution #1242 #2293]: #936
#2295 := [unit-resolution #1248 #2291]: #957
#2296 := [unit-resolution #2118 #2054 #2290 #720 #1468 #776 #694 #798 #2197 #854 #1864 #880 #2295]: #922
#2297 := [unit-resolution #1236 #2296]: #924
#2298 := [unit-resolution #955 #2297]: #148
#2299 := [unit-resolution #956 #2298 #2294]: false
#2301 := [lemma #2299]: #2300
#1848 := [unit-resolution #2301 #2308]: #515
#1851 := [hypothesis]: #632
#1852 := (or #897 #1522 #509 #1523 #998 #1365 #1489 #1150 #1509 #1350 #633 #1372 #1188 #960 #1087 #1112)
#1853 := [th-lemma]: #1852
#1846 := [unit-resolution #1853 #1851 #2295 #720 #1684 #746 #2045 #802 #2266 #824 #2182 #850 #2015 #876 #672 #1848]: #897
#1847 := [unit-resolution #1232 #1846]: #898
#1854 := [unit-resolution #918 #1847]: #100
#1855 := (or #509 #1124)
#1856 := [unit-resolution #2194 #2069 #2144 #2045 #2295 #2182]: #1855
#2309 := [unit-resolution #1856 #1851]: #1124
#2310 := [th-lemma #1848 #876 #850 #2182 #2015 #2309 #2266 #1854]: false
#2311 := [lemma #2310]: #509
#2312 := (or #631 #632)
#2313 := [unit-resolution #646 #2111 #1848]: #2312
#2314 := [unit-resolution #2313 #2311]: #631
#2315 := (or #884 #633 #1372 #1188 #1125 #1528 #506 #1364 #999 #1343 #1373 #1358 #961 #1086)
#2316 := [th-lemma]: #2315
#2317 := [unit-resolution #2316 #668 #2292 #724 #1703 #750 #2308 #798 #2277 #828 #2015 #876 #2314 #1848]: #884
#2318 := [unit-resolution #1224 #2317]: #886
#2319 := (or #896 #1528 #506 #1364 #999 #1343 #1337 #1151 #1373 #1358 #634 #1511 #1189 #961 #1086 #1113)
#2320 := [th-lemma]: #2319
#2321 := [unit-resolution #2320 #668 #2292 #724 #1703 #750 #2308 #798 #1870 #828 #2197 #854 #1864 #880 #2314 #2111]: #896
#2322 := [unit-resolution #1230 #2321]: #898
#2323 := [unit-resolution #918 #2322]: #100
[unit-resolution #917 #2323 #2318]: false
unsat