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

+#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