--- a/src/HOL/Boogie/Examples/cert/Boogie_b_max.proof Thu Nov 05 17:58:58 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,2329 +0,0 @@
-#2 := false
-#4 := 0::int
-decl uf_3 :: (-> int int)
-decl ?x3!1 :: int
-#1188 := ?x3!1
-#1195 := (uf_3 ?x3!1)
-#760 := -1::int
-#1381 := (* -1::int #1195)
-decl uf_4 :: int
-#25 := uf_4
-#39 := (uf_3 uf_4)
-#2763 := (+ #39 #1381)
-#2765 := (>= #2763 0::int)
-#2762 := (= #39 #1195)
-#2631 := (= uf_4 ?x3!1)
-#1394 := (* -1::int ?x3!1)
-#2564 := (+ uf_4 #1394)
-#2628 := (>= #2564 0::int)
-decl uf_9 :: int
-#47 := uf_9
-#806 := (* -1::int uf_9)
-#838 := (+ uf_4 #806)
-#1977 := (>= #838 -1::int)
-#837 := (= #838 -1::int)
-#1395 := (+ uf_9 #1394)
-#1396 := (<= #1395 0::int)
-decl uf_8 :: int
-#43 := uf_8
-#1382 := (+ uf_8 #1381)
-#1383 := (>= #1382 0::int)
-#1192 := (>= ?x3!1 0::int)
-#1625 := (not #1192)
-#1640 := (or #1625 #1383 #1396)
-#1645 := (not #1640)
-#16 := (:var 0 int)
-#20 := (uf_3 #16)
-#2303 := (pattern #20)
-#807 := (+ #16 #806)
-#805 := (>= #807 0::int)
-#799 := (* -1::int uf_8)
-#800 := (+ #20 #799)
-#801 := (<= #800 0::int)
-#753 := (>= #16 0::int)
-#1548 := (not #753)
-#1607 := (or #1548 #801 #805)
-#2320 := (forall (vars (?x3 int)) (:pat #2303) #1607)
-#2325 := (not #2320)
-decl uf_7 :: int
-#41 := uf_7
-#58 := (uf_3 uf_7)
-#221 := (= uf_8 #58)
-#2328 := (or #221 #2325)
-#2331 := (not #2328)
-#2334 := (or #2331 #1645)
-#2337 := (not #2334)
-#851 := (* -1::int #39)
-decl uf_6 :: int
-#32 := uf_6
-#852 := (+ uf_6 #851)
-#850 := (>= #852 0::int)
-#840 := (not #837)
-#50 := 2::int
-#791 := (>= uf_9 2::int)
-#1656 := (not #791)
-#788 := (>= uf_7 0::int)
-#1655 := (not #788)
-decl uf_5 :: int
-#27 := uf_5
-#779 := (>= uf_5 0::int)
-#1654 := (not #779)
-#10 := 1::int
-#776 := (>= uf_4 1::int)
-#886 := (not #776)
-#361 := (= uf_4 uf_7)
-#376 := (not #361)
-decl uf_10 :: int
-#78 := uf_10
-#356 := (= #39 uf_10)
-#401 := (not #356)
-#82 := (= uf_8 uf_10)
-#367 := (not #82)
-#2346 := (or #367 #401 #376 #886 #1654 #1655 #1656 #840 #850 #2337)
-#2349 := (not #2346)
-#854 := (not #850)
-#194 := (= uf_6 uf_8)
-#301 := (not #194)
-#191 := (= uf_5 uf_7)
-#310 := (not #191)
-#2340 := (or #310 #301 #886 #1654 #1655 #1656 #840 #854 #2337)
-#2343 := (not #2340)
-#2352 := (or #2343 #2349)
-#2355 := (not #2352)
-#924 := (* -1::int uf_4)
-decl uf_1 :: int
-#5 := uf_1
-#925 := (+ uf_1 #924)
-#926 := (<= #925 0::int)
-#2358 := (or #886 #1654 #926 #2355)
-#2361 := (not #2358)
-decl ?x7!2 :: int
-#1279 := ?x7!2
-#1287 := (uf_3 ?x7!2)
-decl uf_12 :: int
-#99 := uf_12
-#1469 := (= uf_12 #1287)
-#1284 := (>= ?x7!2 0::int)
-#1711 := (not #1284)
-#1280 := (* -1::int ?x7!2)
-#1281 := (+ uf_1 #1280)
-#1282 := (<= #1281 0::int)
-#1726 := (or #1282 #1711 #1469)
-#1757 := (not #1726)
-decl ?x8!3 :: int
-#1297 := ?x8!3
-#1298 := (uf_3 ?x8!3)
-#1493 := (* -1::int #1298)
-#1494 := (+ uf_12 #1493)
-#1495 := (>= #1494 0::int)
-#1305 := (>= ?x8!3 0::int)
-#1731 := (not #1305)
-#1301 := (* -1::int ?x8!3)
-#1302 := (+ uf_1 #1301)
-#1303 := (<= #1302 0::int)
-#1795 := (or #1303 #1731 #1495 #1757)
-#1798 := (not #1795)
-#951 := (* -1::int #16)
-#952 := (+ uf_1 #951)
-#953 := (<= #952 0::int)
-#105 := (= #20 uf_12)
-#1700 := (or #105 #1548 #953)
-#1705 := (not #1700)
-#2364 := (forall (vars (?x7 int)) (:pat #2303) #1705)
-#2369 := (or #2364 #1798)
-#2372 := (not #2369)
-#927 := (not #926)
-decl uf_13 :: int
-#101 := uf_13
-#472 := (= uf_4 uf_13)
-#542 := (not #472)
-#469 := (= uf_6 uf_12)
-#551 := (not #469)
-decl uf_11 :: int
-#97 := uf_11
-#466 := (= uf_5 uf_11)
-#560 := (not #466)
-#2375 := (or #560 #551 #542 #886 #1654 #927 #2372)
-#2378 := (not #2375)
-#2381 := (or #2361 #2378)
-#2384 := (not #2381)
-#1030 := (+ #16 #924)
-#1029 := (>= #1030 0::int)
-#1024 := (* -1::int uf_6)
-#1025 := (+ #20 #1024)
-#1026 := (<= #1025 0::int)
-#1585 := (or #1548 #1026 #1029)
-#2312 := (forall (vars (?x2 int)) (:pat #2303) #1585)
-#2317 := (not #2312)
-#763 := (* -1::int #20)
-decl uf_2 :: int
-#7 := uf_2
-#764 := (+ uf_2 #763)
-#762 := (>= #764 0::int)
-#749 := (>= #16 1::int)
-#1563 := (or #749 #1548 #762)
-#2304 := (forall (vars (?x1 int)) (:pat #2303) #1563)
-#2309 := (not #2304)
-#36 := (uf_3 uf_5)
-#188 := (= uf_6 #36)
-#619 := (not #188)
-#2387 := (or #619 #886 #1654 #2309 #2317 #2384)
-#2390 := (not #2387)
-decl ?x1!0 :: int
-#1152 := ?x1!0
-#1156 := (>= ?x1!0 1::int)
-#1155 := (>= ?x1!0 0::int)
-#1164 := (not #1155)
-#1153 := (uf_3 ?x1!0)
-#1150 := (* -1::int #1153)
-#1151 := (+ uf_2 #1150)
-#1154 := (>= #1151 0::int)
-#1540 := (or #1154 #1164 #1156)
-#2202 := (= uf_2 #1153)
-#8 := (uf_3 0::int)
-#2191 := (= #8 #1153)
-#2188 := (= #1153 #8)
-#2207 := (= ?x1!0 0::int)
-#1157 := (not #1156)
-#1545 := (not #1540)
-#2205 := [hypothesis]: #1545
-#1976 := (or #1540 #1157)
-#1967 := [def-axiom]: #1976
-#2206 := [unit-resolution #1967 #2205]: #1157
-#1975 := (or #1540 #1155)
-#1890 := [def-axiom]: #1975
-#2203 := [unit-resolution #1890 #2205]: #1155
-#2187 := [th-lemma #2203 #2206]: #2207
-#2190 := [monotonicity #2187]: #2188
-#2192 := [symm #2190]: #2191
-#9 := (= uf_2 #8)
-#1078 := (<= uf_1 0::int)
-#1031 := (not #1029)
-#1034 := (and #753 #1031)
-#1037 := (not #1034)
-#1040 := (or #1026 #1037)
-#1043 := (forall (vars (?x2 int)) #1040)
-#1046 := (not #1043)
-#972 := (* -1::int uf_12)
-#973 := (+ #20 #972)
-#974 := (<= #973 0::int)
-#954 := (not #953)
-#957 := (and #753 #954)
-#960 := (not #957)
-#980 := (or #960 #974)
-#985 := (forall (vars (?x8 int)) #980)
-#963 := (or #105 #960)
-#966 := (exists (vars (?x7 int)) #963)
-#969 := (not #966)
-#988 := (or #969 #985)
-#991 := (and #966 #988)
-#781 := (and #776 #779)
-#784 := (not #781)
-#1016 := (or #560 #551 #542 #784 #927 #991)
-#843 := (and #776 #788)
-#846 := (not #843)
-#804 := (not #805)
-#810 := (and #753 #804)
-#813 := (not #810)
-#816 := (or #801 #813)
-#819 := (forall (vars (?x3 int)) #816)
-#822 := (not #819)
-#828 := (or #221 #822)
-#833 := (and #819 #828)
-#793 := (and #788 #791)
-#796 := (not #793)
-#916 := (or #367 #401 #376 #886 #784 #796 #833 #840 #846 #850)
-#881 := (or #310 #301 #784 #796 #833 #840 #846 #854)
-#921 := (and #881 #916)
-#946 := (or #784 #921 #926)
-#1021 := (and #946 #1016)
-#652 := (not #9)
-#1064 := (or #652 #619 #784 #1021 #1046)
-#1069 := (and #9 #1064)
-#747 := (not #749)
-#754 := (and #747 #753)
-#757 := (not #754)
-#766 := (or #757 #762)
-#769 := (forall (vars (?x1 int)) #766)
-#772 := (not #769)
-#1072 := (or #772 #1069)
-#1075 := (and #769 #1072)
-#1098 := (or #652 #1075 #1078)
-#1103 := (not #1098)
-#21 := (<= #20 uf_2)
-#18 := (<= 0::int #16)
-#17 := (< #16 1::int)
-#19 := (and #17 #18)
-#22 := (implies #19 #21)
-#23 := (forall (vars (?x1 int)) #22)
-#24 := (= #8 uf_2)
-#103 := (< #16 uf_1)
-#104 := (and #103 #18)
-#106 := (implies #104 #105)
-#107 := (exists (vars (?x7 int)) #106)
-#108 := (<= #20 uf_12)
-#109 := (implies #104 #108)
-#110 := (forall (vars (?x8 int)) #109)
-#1 := true
-#111 := (implies #110 true)
-#112 := (and #111 #110)
-#113 := (implies #107 #112)
-#114 := (and #113 #107)
-#115 := (implies true #114)
-#102 := (= uf_13 uf_4)
-#116 := (implies #102 #115)
-#100 := (= uf_12 uf_6)
-#117 := (implies #100 #116)
-#98 := (= uf_11 uf_5)
-#118 := (implies #98 #117)
-#119 := (implies true #118)
-#28 := (<= 0::int uf_5)
-#26 := (<= 1::int uf_4)
-#29 := (and #26 #28)
-#120 := (implies #29 #119)
-#96 := (<= uf_1 uf_4)
-#121 := (implies #96 #120)
-#122 := (implies #29 #121)
-#123 := (implies true #122)
-#55 := (<= #20 uf_8)
-#53 := (< #16 uf_9)
-#54 := (and #53 #18)
-#56 := (implies #54 #55)
-#57 := (forall (vars (?x3 int)) #56)
-#59 := (= #58 uf_8)
-#60 := (implies false true)
-#61 := (implies #59 #60)
-#62 := (and #61 #59)
-#63 := (implies #57 #62)
-#64 := (and #63 #57)
-#65 := (implies true #64)
-#45 := (<= 0::int uf_7)
-#51 := (<= 2::int uf_9)
-#52 := (and #51 #45)
-#66 := (implies #52 #65)
-#48 := (+ uf_4 1::int)
-#49 := (= uf_9 #48)
-#67 := (implies #49 #66)
-#46 := (and #26 #45)
-#68 := (implies #46 #67)
-#69 := (implies true #68)
-#83 := (implies #82 #69)
-#81 := (= uf_7 uf_4)
-#84 := (implies #81 #83)
-#85 := (implies true #84)
-#80 := (and #26 #26)
-#86 := (implies #80 #85)
-#79 := (= uf_10 #39)
-#87 := (implies #79 #86)
-#77 := (< uf_6 #39)
-#88 := (implies #77 #87)
-#89 := (implies #29 #88)
-#90 := (implies true #89)
-#44 := (= uf_8 uf_6)
-#70 := (implies #44 #69)
-#42 := (= uf_7 uf_5)
-#71 := (implies #42 #70)
-#72 := (implies true #71)
-#73 := (implies #29 #72)
-#40 := (<= #39 uf_6)
-#74 := (implies #40 #73)
-#75 := (implies #29 #74)
-#76 := (implies true #75)
-#91 := (and #76 #90)
-#92 := (implies #29 #91)
-#38 := (< uf_4 uf_1)
-#93 := (implies #38 #92)
-#94 := (implies #29 #93)
-#95 := (implies true #94)
-#124 := (and #95 #123)
-#125 := (implies #29 #124)
-#37 := (= #36 uf_6)
-#126 := (implies #37 #125)
-#33 := (<= #20 uf_6)
-#30 := (< #16 uf_4)
-#31 := (and #30 #18)
-#34 := (implies #31 #33)
-#35 := (forall (vars (?x2 int)) #34)
-#127 := (implies #35 #126)
-#128 := (implies #29 #127)
-#129 := (implies true #128)
-#130 := (implies #24 #129)
-#131 := (and #130 #24)
-#132 := (implies #23 #131)
-#133 := (and #132 #23)
-#12 := (<= 0::int 0::int)
-#13 := (and #12 #12)
-#11 := (<= 1::int 1::int)
-#14 := (and #11 #13)
-#15 := (and #11 #14)
-#134 := (implies #15 #133)
-#135 := (implies #9 #134)
-#136 := (implies true #135)
-#6 := (< 0::int uf_1)
-#137 := (implies #6 #136)
-#138 := (implies true #137)
-#139 := (not #138)
-#1106 := (iff #139 #1103)
-#475 := (and #18 #103)
-#481 := (not #475)
-#493 := (or #108 #481)
-#498 := (forall (vars (?x8 int)) #493)
-#482 := (or #105 #481)
-#487 := (exists (vars (?x7 int)) #482)
-#518 := (not #487)
-#519 := (or #518 #498)
-#527 := (and #487 #519)
-#543 := (or #542 #527)
-#552 := (or #551 #543)
-#561 := (or #560 #552)
-#326 := (not #29)
-#576 := (or #326 #561)
-#584 := (not #96)
-#585 := (or #584 #576)
-#593 := (or #326 #585)
-#206 := (and #18 #53)
-#212 := (not #206)
-#213 := (or #55 #212)
-#218 := (forall (vars (?x3 int)) #213)
-#243 := (not #218)
-#244 := (or #243 #221)
-#252 := (and #218 #244)
-#203 := (and #45 #51)
-#267 := (not #203)
-#268 := (or #267 #252)
-#197 := (+ 1::int uf_4)
-#200 := (= uf_9 #197)
-#276 := (not #200)
-#277 := (or #276 #268)
-#285 := (not #46)
-#286 := (or #285 #277)
-#368 := (or #367 #286)
-#377 := (or #376 #368)
-#392 := (not #26)
-#393 := (or #392 #377)
-#402 := (or #401 #393)
-#410 := (not #77)
-#411 := (or #410 #402)
-#419 := (or #326 #411)
-#302 := (or #301 #286)
-#311 := (or #310 #302)
-#327 := (or #326 #311)
-#335 := (not #40)
-#336 := (or #335 #327)
-#344 := (or #326 #336)
-#431 := (and #344 #419)
-#437 := (or #326 #431)
-#445 := (not #38)
-#446 := (or #445 #437)
-#454 := (or #326 #446)
-#605 := (and #454 #593)
-#611 := (or #326 #605)
-#620 := (or #619 #611)
-#173 := (and #18 #30)
-#179 := (not #173)
-#180 := (or #33 #179)
-#185 := (forall (vars (?x2 int)) #180)
-#628 := (not #185)
-#629 := (or #628 #620)
-#637 := (or #326 #629)
-#653 := (or #652 #637)
-#661 := (and #9 #653)
-#164 := (not #19)
-#165 := (or #164 #21)
-#168 := (forall (vars (?x1 int)) #165)
-#669 := (not #168)
-#670 := (or #669 #661)
-#678 := (and #168 #670)
-#158 := (and #11 #12)
-#161 := (and #11 #158)
-#686 := (not #161)
-#687 := (or #686 #678)
-#695 := (or #652 #687)
-#710 := (not #6)
-#711 := (or #710 #695)
-#723 := (not #711)
-#1104 := (iff #723 #1103)
-#1101 := (iff #711 #1098)
-#1089 := (or false #1075)
-#1092 := (or #652 #1089)
-#1095 := (or #1078 #1092)
-#1099 := (iff #1095 #1098)
-#1100 := [rewrite]: #1099
-#1096 := (iff #711 #1095)
-#1093 := (iff #695 #1092)
-#1090 := (iff #687 #1089)
-#1076 := (iff #678 #1075)
-#1073 := (iff #670 #1072)
-#1070 := (iff #661 #1069)
-#1067 := (iff #653 #1064)
-#1049 := (or #784 #1021)
-#1052 := (or #619 #1049)
-#1055 := (or #1046 #1052)
-#1058 := (or #784 #1055)
-#1061 := (or #652 #1058)
-#1065 := (iff #1061 #1064)
-#1066 := [rewrite]: #1065
-#1062 := (iff #653 #1061)
-#1059 := (iff #637 #1058)
-#1056 := (iff #629 #1055)
-#1053 := (iff #620 #1052)
-#1050 := (iff #611 #1049)
-#1022 := (iff #605 #1021)
-#1019 := (iff #593 #1016)
-#998 := (or #542 #991)
-#1001 := (or #551 #998)
-#1004 := (or #560 #1001)
-#1007 := (or #784 #1004)
-#1010 := (or #927 #1007)
-#1013 := (or #784 #1010)
-#1017 := (iff #1013 #1016)
-#1018 := [rewrite]: #1017
-#1014 := (iff #593 #1013)
-#1011 := (iff #585 #1010)
-#1008 := (iff #576 #1007)
-#1005 := (iff #561 #1004)
-#1002 := (iff #552 #1001)
-#999 := (iff #543 #998)
-#992 := (iff #527 #991)
-#989 := (iff #519 #988)
-#986 := (iff #498 #985)
-#983 := (iff #493 #980)
-#977 := (or #974 #960)
-#981 := (iff #977 #980)
-#982 := [rewrite]: #981
-#978 := (iff #493 #977)
-#961 := (iff #481 #960)
-#958 := (iff #475 #957)
-#955 := (iff #103 #954)
-#956 := [rewrite]: #955
-#751 := (iff #18 #753)
-#752 := [rewrite]: #751
-#959 := [monotonicity #752 #956]: #958
-#962 := [monotonicity #959]: #961
-#975 := (iff #108 #974)
-#976 := [rewrite]: #975
-#979 := [monotonicity #976 #962]: #978
-#984 := [trans #979 #982]: #983
-#987 := [quant-intro #984]: #986
-#970 := (iff #518 #969)
-#967 := (iff #487 #966)
-#964 := (iff #482 #963)
-#965 := [monotonicity #962]: #964
-#968 := [quant-intro #965]: #967
-#971 := [monotonicity #968]: #970
-#990 := [monotonicity #971 #987]: #989
-#993 := [monotonicity #968 #990]: #992
-#1000 := [monotonicity #993]: #999
-#1003 := [monotonicity #1000]: #1002
-#1006 := [monotonicity #1003]: #1005
-#785 := (iff #326 #784)
-#782 := (iff #29 #781)
-#778 := (iff #28 #779)
-#780 := [rewrite]: #778
-#775 := (iff #26 #776)
-#777 := [rewrite]: #775
-#783 := [monotonicity #777 #780]: #782
-#786 := [monotonicity #783]: #785
-#1009 := [monotonicity #786 #1006]: #1008
-#996 := (iff #584 #927)
-#994 := (iff #96 #926)
-#995 := [rewrite]: #994
-#997 := [monotonicity #995]: #996
-#1012 := [monotonicity #997 #1009]: #1011
-#1015 := [monotonicity #786 #1012]: #1014
-#1020 := [trans #1015 #1018]: #1019
-#949 := (iff #454 #946)
-#937 := (or #784 #921)
-#940 := (or #926 #937)
-#943 := (or #784 #940)
-#947 := (iff #943 #946)
-#948 := [rewrite]: #947
-#944 := (iff #454 #943)
-#941 := (iff #446 #940)
-#938 := (iff #437 #937)
-#922 := (iff #431 #921)
-#919 := (iff #419 #916)
-#857 := (or #796 #833)
-#860 := (or #840 #857)
-#863 := (or #846 #860)
-#898 := (or #367 #863)
-#901 := (or #376 #898)
-#904 := (or #886 #901)
-#907 := (or #401 #904)
-#910 := (or #850 #907)
-#913 := (or #784 #910)
-#917 := (iff #913 #916)
-#918 := [rewrite]: #917
-#914 := (iff #419 #913)
-#911 := (iff #411 #910)
-#908 := (iff #402 #907)
-#905 := (iff #393 #904)
-#902 := (iff #377 #901)
-#899 := (iff #368 #898)
-#864 := (iff #286 #863)
-#861 := (iff #277 #860)
-#858 := (iff #268 #857)
-#834 := (iff #252 #833)
-#831 := (iff #244 #828)
-#825 := (or #822 #221)
-#829 := (iff #825 #828)
-#830 := [rewrite]: #829
-#826 := (iff #244 #825)
-#823 := (iff #243 #822)
-#820 := (iff #218 #819)
-#817 := (iff #213 #816)
-#814 := (iff #212 #813)
-#811 := (iff #206 #810)
-#808 := (iff #53 #804)
-#809 := [rewrite]: #808
-#812 := [monotonicity #752 #809]: #811
-#815 := [monotonicity #812]: #814
-#802 := (iff #55 #801)
-#803 := [rewrite]: #802
-#818 := [monotonicity #803 #815]: #817
-#821 := [quant-intro #818]: #820
-#824 := [monotonicity #821]: #823
-#827 := [monotonicity #824]: #826
-#832 := [trans #827 #830]: #831
-#835 := [monotonicity #821 #832]: #834
-#797 := (iff #267 #796)
-#794 := (iff #203 #793)
-#790 := (iff #51 #791)
-#792 := [rewrite]: #790
-#787 := (iff #45 #788)
-#789 := [rewrite]: #787
-#795 := [monotonicity #789 #792]: #794
-#798 := [monotonicity #795]: #797
-#859 := [monotonicity #798 #835]: #858
-#841 := (iff #276 #840)
-#836 := (iff #200 #837)
-#839 := [rewrite]: #836
-#842 := [monotonicity #839]: #841
-#862 := [monotonicity #842 #859]: #861
-#847 := (iff #285 #846)
-#844 := (iff #46 #843)
-#845 := [monotonicity #777 #789]: #844
-#848 := [monotonicity #845]: #847
-#865 := [monotonicity #848 #862]: #864
-#900 := [monotonicity #865]: #899
-#903 := [monotonicity #900]: #902
-#887 := (iff #392 #886)
-#888 := [monotonicity #777]: #887
-#906 := [monotonicity #888 #903]: #905
-#909 := [monotonicity #906]: #908
-#896 := (iff #410 #850)
-#891 := (not #854)
-#894 := (iff #891 #850)
-#895 := [rewrite]: #894
-#892 := (iff #410 #891)
-#889 := (iff #77 #854)
-#890 := [rewrite]: #889
-#893 := [monotonicity #890]: #892
-#897 := [trans #893 #895]: #896
-#912 := [monotonicity #897 #909]: #911
-#915 := [monotonicity #786 #912]: #914
-#920 := [trans #915 #918]: #919
-#884 := (iff #344 #881)
-#866 := (or #301 #863)
-#869 := (or #310 #866)
-#872 := (or #784 #869)
-#875 := (or #854 #872)
-#878 := (or #784 #875)
-#882 := (iff #878 #881)
-#883 := [rewrite]: #882
-#879 := (iff #344 #878)
-#876 := (iff #336 #875)
-#873 := (iff #327 #872)
-#870 := (iff #311 #869)
-#867 := (iff #302 #866)
-#868 := [monotonicity #865]: #867
-#871 := [monotonicity #868]: #870
-#874 := [monotonicity #786 #871]: #873
-#855 := (iff #335 #854)
-#849 := (iff #40 #850)
-#853 := [rewrite]: #849
-#856 := [monotonicity #853]: #855
-#877 := [monotonicity #856 #874]: #876
-#880 := [monotonicity #786 #877]: #879
-#885 := [trans #880 #883]: #884
-#923 := [monotonicity #885 #920]: #922
-#939 := [monotonicity #786 #923]: #938
-#935 := (iff #445 #926)
-#930 := (not #927)
-#933 := (iff #930 #926)
-#934 := [rewrite]: #933
-#931 := (iff #445 #930)
-#928 := (iff #38 #927)
-#929 := [rewrite]: #928
-#932 := [monotonicity #929]: #931
-#936 := [trans #932 #934]: #935
-#942 := [monotonicity #936 #939]: #941
-#945 := [monotonicity #786 #942]: #944
-#950 := [trans #945 #948]: #949
-#1023 := [monotonicity #950 #1020]: #1022
-#1051 := [monotonicity #786 #1023]: #1050
-#1054 := [monotonicity #1051]: #1053
-#1047 := (iff #628 #1046)
-#1044 := (iff #185 #1043)
-#1041 := (iff #180 #1040)
-#1038 := (iff #179 #1037)
-#1035 := (iff #173 #1034)
-#1032 := (iff #30 #1031)
-#1033 := [rewrite]: #1032
-#1036 := [monotonicity #752 #1033]: #1035
-#1039 := [monotonicity #1036]: #1038
-#1027 := (iff #33 #1026)
-#1028 := [rewrite]: #1027
-#1042 := [monotonicity #1028 #1039]: #1041
-#1045 := [quant-intro #1042]: #1044
-#1048 := [monotonicity #1045]: #1047
-#1057 := [monotonicity #1048 #1054]: #1056
-#1060 := [monotonicity #786 #1057]: #1059
-#1063 := [monotonicity #1060]: #1062
-#1068 := [trans #1063 #1066]: #1067
-#1071 := [monotonicity #1068]: #1070
-#773 := (iff #669 #772)
-#770 := (iff #168 #769)
-#767 := (iff #165 #766)
-#761 := (iff #21 #762)
-#765 := [rewrite]: #761
-#758 := (iff #164 #757)
-#755 := (iff #19 #754)
-#748 := (iff #17 #747)
-#750 := [rewrite]: #748
-#756 := [monotonicity #750 #752]: #755
-#759 := [monotonicity #756]: #758
-#768 := [monotonicity #759 #765]: #767
-#771 := [quant-intro #768]: #770
-#774 := [monotonicity #771]: #773
-#1074 := [monotonicity #774 #1071]: #1073
-#1077 := [monotonicity #771 #1074]: #1076
-#745 := (iff #686 false)
-#740 := (not true)
-#743 := (iff #740 false)
-#744 := [rewrite]: #743
-#741 := (iff #686 #740)
-#738 := (iff #161 true)
-#730 := (and true true)
-#733 := (and true #730)
-#736 := (iff #733 true)
-#737 := [rewrite]: #736
-#734 := (iff #161 #733)
-#731 := (iff #158 #730)
-#728 := (iff #12 true)
-#729 := [rewrite]: #728
-#726 := (iff #11 true)
-#727 := [rewrite]: #726
-#732 := [monotonicity #727 #729]: #731
-#735 := [monotonicity #727 #732]: #734
-#739 := [trans #735 #737]: #738
-#742 := [monotonicity #739]: #741
-#746 := [trans #742 #744]: #745
-#1091 := [monotonicity #746 #1077]: #1090
-#1094 := [monotonicity #1091]: #1093
-#1087 := (iff #710 #1078)
-#1079 := (not #1078)
-#1082 := (not #1079)
-#1085 := (iff #1082 #1078)
-#1086 := [rewrite]: #1085
-#1083 := (iff #710 #1082)
-#1080 := (iff #6 #1079)
-#1081 := [rewrite]: #1080
-#1084 := [monotonicity #1081]: #1083
-#1088 := [trans #1084 #1086]: #1087
-#1097 := [monotonicity #1088 #1094]: #1096
-#1102 := [trans #1097 #1100]: #1101
-#1105 := [monotonicity #1102]: #1104
-#724 := (iff #139 #723)
-#721 := (iff #138 #711)
-#716 := (implies true #711)
-#719 := (iff #716 #711)
-#720 := [rewrite]: #719
-#717 := (iff #138 #716)
-#714 := (iff #137 #711)
-#707 := (implies #6 #695)
-#712 := (iff #707 #711)
-#713 := [rewrite]: #712
-#708 := (iff #137 #707)
-#705 := (iff #136 #695)
-#700 := (implies true #695)
-#703 := (iff #700 #695)
-#704 := [rewrite]: #703
-#701 := (iff #136 #700)
-#698 := (iff #135 #695)
-#692 := (implies #9 #687)
-#696 := (iff #692 #695)
-#697 := [rewrite]: #696
-#693 := (iff #135 #692)
-#690 := (iff #134 #687)
-#683 := (implies #161 #678)
-#688 := (iff #683 #687)
-#689 := [rewrite]: #688
-#684 := (iff #134 #683)
-#681 := (iff #133 #678)
-#675 := (and #670 #168)
-#679 := (iff #675 #678)
-#680 := [rewrite]: #679
-#676 := (iff #133 #675)
-#169 := (iff #23 #168)
-#166 := (iff #22 #165)
-#167 := [rewrite]: #166
-#170 := [quant-intro #167]: #169
-#673 := (iff #132 #670)
-#666 := (implies #168 #661)
-#671 := (iff #666 #670)
-#672 := [rewrite]: #671
-#667 := (iff #132 #666)
-#664 := (iff #131 #661)
-#658 := (and #653 #9)
-#662 := (iff #658 #661)
-#663 := [rewrite]: #662
-#659 := (iff #131 #658)
-#171 := (iff #24 #9)
-#172 := [rewrite]: #171
-#656 := (iff #130 #653)
-#649 := (implies #9 #637)
-#654 := (iff #649 #653)
-#655 := [rewrite]: #654
-#650 := (iff #130 #649)
-#647 := (iff #129 #637)
-#642 := (implies true #637)
-#645 := (iff #642 #637)
-#646 := [rewrite]: #645
-#643 := (iff #129 #642)
-#640 := (iff #128 #637)
-#634 := (implies #29 #629)
-#638 := (iff #634 #637)
-#639 := [rewrite]: #638
-#635 := (iff #128 #634)
-#632 := (iff #127 #629)
-#625 := (implies #185 #620)
-#630 := (iff #625 #629)
-#631 := [rewrite]: #630
-#626 := (iff #127 #625)
-#623 := (iff #126 #620)
-#616 := (implies #188 #611)
-#621 := (iff #616 #620)
-#622 := [rewrite]: #621
-#617 := (iff #126 #616)
-#614 := (iff #125 #611)
-#608 := (implies #29 #605)
-#612 := (iff #608 #611)
-#613 := [rewrite]: #612
-#609 := (iff #125 #608)
-#606 := (iff #124 #605)
-#603 := (iff #123 #593)
-#598 := (implies true #593)
-#601 := (iff #598 #593)
-#602 := [rewrite]: #601
-#599 := (iff #123 #598)
-#596 := (iff #122 #593)
-#590 := (implies #29 #585)
-#594 := (iff #590 #593)
-#595 := [rewrite]: #594
-#591 := (iff #122 #590)
-#588 := (iff #121 #585)
-#581 := (implies #96 #576)
-#586 := (iff #581 #585)
-#587 := [rewrite]: #586
-#582 := (iff #121 #581)
-#579 := (iff #120 #576)
-#573 := (implies #29 #561)
-#577 := (iff #573 #576)
-#578 := [rewrite]: #577
-#574 := (iff #120 #573)
-#571 := (iff #119 #561)
-#566 := (implies true #561)
-#569 := (iff #566 #561)
-#570 := [rewrite]: #569
-#567 := (iff #119 #566)
-#564 := (iff #118 #561)
-#557 := (implies #466 #552)
-#562 := (iff #557 #561)
-#563 := [rewrite]: #562
-#558 := (iff #118 #557)
-#555 := (iff #117 #552)
-#548 := (implies #469 #543)
-#553 := (iff #548 #552)
-#554 := [rewrite]: #553
-#549 := (iff #117 #548)
-#546 := (iff #116 #543)
-#539 := (implies #472 #527)
-#544 := (iff #539 #543)
-#545 := [rewrite]: #544
-#540 := (iff #116 #539)
-#537 := (iff #115 #527)
-#532 := (implies true #527)
-#535 := (iff #532 #527)
-#536 := [rewrite]: #535
-#533 := (iff #115 #532)
-#530 := (iff #114 #527)
-#524 := (and #519 #487)
-#528 := (iff #524 #527)
-#529 := [rewrite]: #528
-#525 := (iff #114 #524)
-#488 := (iff #107 #487)
-#485 := (iff #106 #482)
-#478 := (implies #475 #105)
-#483 := (iff #478 #482)
-#484 := [rewrite]: #483
-#479 := (iff #106 #478)
-#476 := (iff #104 #475)
-#477 := [rewrite]: #476
-#480 := [monotonicity #477]: #479
-#486 := [trans #480 #484]: #485
-#489 := [quant-intro #486]: #488
-#522 := (iff #113 #519)
-#515 := (implies #487 #498)
-#520 := (iff #515 #519)
-#521 := [rewrite]: #520
-#516 := (iff #113 #515)
-#513 := (iff #112 #498)
-#508 := (and true #498)
-#511 := (iff #508 #498)
-#512 := [rewrite]: #511
-#509 := (iff #112 #508)
-#499 := (iff #110 #498)
-#496 := (iff #109 #493)
-#490 := (implies #475 #108)
-#494 := (iff #490 #493)
-#495 := [rewrite]: #494
-#491 := (iff #109 #490)
-#492 := [monotonicity #477]: #491
-#497 := [trans #492 #495]: #496
-#500 := [quant-intro #497]: #499
-#506 := (iff #111 true)
-#501 := (implies #498 true)
-#504 := (iff #501 true)
-#505 := [rewrite]: #504
-#502 := (iff #111 #501)
-#503 := [monotonicity #500]: #502
-#507 := [trans #503 #505]: #506
-#510 := [monotonicity #507 #500]: #509
-#514 := [trans #510 #512]: #513
-#517 := [monotonicity #489 #514]: #516
-#523 := [trans #517 #521]: #522
-#526 := [monotonicity #523 #489]: #525
-#531 := [trans #526 #529]: #530
-#534 := [monotonicity #531]: #533
-#538 := [trans #534 #536]: #537
-#473 := (iff #102 #472)
-#474 := [rewrite]: #473
-#541 := [monotonicity #474 #538]: #540
-#547 := [trans #541 #545]: #546
-#470 := (iff #100 #469)
-#471 := [rewrite]: #470
-#550 := [monotonicity #471 #547]: #549
-#556 := [trans #550 #554]: #555
-#467 := (iff #98 #466)
-#468 := [rewrite]: #467
-#559 := [monotonicity #468 #556]: #558
-#565 := [trans #559 #563]: #564
-#568 := [monotonicity #565]: #567
-#572 := [trans #568 #570]: #571
-#575 := [monotonicity #572]: #574
-#580 := [trans #575 #578]: #579
-#583 := [monotonicity #580]: #582
-#589 := [trans #583 #587]: #588
-#592 := [monotonicity #589]: #591
-#597 := [trans #592 #595]: #596
-#600 := [monotonicity #597]: #599
-#604 := [trans #600 #602]: #603
-#464 := (iff #95 #454)
-#459 := (implies true #454)
-#462 := (iff #459 #454)
-#463 := [rewrite]: #462
-#460 := (iff #95 #459)
-#457 := (iff #94 #454)
-#451 := (implies #29 #446)
-#455 := (iff #451 #454)
-#456 := [rewrite]: #455
-#452 := (iff #94 #451)
-#449 := (iff #93 #446)
-#442 := (implies #38 #437)
-#447 := (iff #442 #446)
-#448 := [rewrite]: #447
-#443 := (iff #93 #442)
-#440 := (iff #92 #437)
-#434 := (implies #29 #431)
-#438 := (iff #434 #437)
-#439 := [rewrite]: #438
-#435 := (iff #92 #434)
-#432 := (iff #91 #431)
-#429 := (iff #90 #419)
-#424 := (implies true #419)
-#427 := (iff #424 #419)
-#428 := [rewrite]: #427
-#425 := (iff #90 #424)
-#422 := (iff #89 #419)
-#416 := (implies #29 #411)
-#420 := (iff #416 #419)
-#421 := [rewrite]: #420
-#417 := (iff #89 #416)
-#414 := (iff #88 #411)
-#407 := (implies #77 #402)
-#412 := (iff #407 #411)
-#413 := [rewrite]: #412
-#408 := (iff #88 #407)
-#405 := (iff #87 #402)
-#398 := (implies #356 #393)
-#403 := (iff #398 #402)
-#404 := [rewrite]: #403
-#399 := (iff #87 #398)
-#396 := (iff #86 #393)
-#389 := (implies #26 #377)
-#394 := (iff #389 #393)
-#395 := [rewrite]: #394
-#390 := (iff #86 #389)
-#387 := (iff #85 #377)
-#382 := (implies true #377)
-#385 := (iff #382 #377)
-#386 := [rewrite]: #385
-#383 := (iff #85 #382)
-#380 := (iff #84 #377)
-#373 := (implies #361 #368)
-#378 := (iff #373 #377)
-#379 := [rewrite]: #378
-#374 := (iff #84 #373)
-#371 := (iff #83 #368)
-#364 := (implies #82 #286)
-#369 := (iff #364 #368)
-#370 := [rewrite]: #369
-#365 := (iff #83 #364)
-#296 := (iff #69 #286)
-#291 := (implies true #286)
-#294 := (iff #291 #286)
-#295 := [rewrite]: #294
-#292 := (iff #69 #291)
-#289 := (iff #68 #286)
-#282 := (implies #46 #277)
-#287 := (iff #282 #286)
-#288 := [rewrite]: #287
-#283 := (iff #68 #282)
-#280 := (iff #67 #277)
-#273 := (implies #200 #268)
-#278 := (iff #273 #277)
-#279 := [rewrite]: #278
-#274 := (iff #67 #273)
-#271 := (iff #66 #268)
-#264 := (implies #203 #252)
-#269 := (iff #264 #268)
-#270 := [rewrite]: #269
-#265 := (iff #66 #264)
-#262 := (iff #65 #252)
-#257 := (implies true #252)
-#260 := (iff #257 #252)
-#261 := [rewrite]: #260
-#258 := (iff #65 #257)
-#255 := (iff #64 #252)
-#249 := (and #244 #218)
-#253 := (iff #249 #252)
-#254 := [rewrite]: #253
-#250 := (iff #64 #249)
-#219 := (iff #57 #218)
-#216 := (iff #56 #213)
-#209 := (implies #206 #55)
-#214 := (iff #209 #213)
-#215 := [rewrite]: #214
-#210 := (iff #56 #209)
-#207 := (iff #54 #206)
-#208 := [rewrite]: #207
-#211 := [monotonicity #208]: #210
-#217 := [trans #211 #215]: #216
-#220 := [quant-intro #217]: #219
-#247 := (iff #63 #244)
-#240 := (implies #218 #221)
-#245 := (iff #240 #244)
-#246 := [rewrite]: #245
-#241 := (iff #63 #240)
-#238 := (iff #62 #221)
-#233 := (and true #221)
-#236 := (iff #233 #221)
-#237 := [rewrite]: #236
-#234 := (iff #62 #233)
-#222 := (iff #59 #221)
-#223 := [rewrite]: #222
-#231 := (iff #61 true)
-#226 := (implies #221 true)
-#229 := (iff #226 true)
-#230 := [rewrite]: #229
-#227 := (iff #61 #226)
-#224 := (iff #60 true)
-#225 := [rewrite]: #224
-#228 := [monotonicity #223 #225]: #227
-#232 := [trans #228 #230]: #231
-#235 := [monotonicity #232 #223]: #234
-#239 := [trans #235 #237]: #238
-#242 := [monotonicity #220 #239]: #241
-#248 := [trans #242 #246]: #247
-#251 := [monotonicity #248 #220]: #250
-#256 := [trans #251 #254]: #255
-#259 := [monotonicity #256]: #258
-#263 := [trans #259 #261]: #262
-#204 := (iff #52 #203)
-#205 := [rewrite]: #204
-#266 := [monotonicity #205 #263]: #265
-#272 := [trans #266 #270]: #271
-#201 := (iff #49 #200)
-#198 := (= #48 #197)
-#199 := [rewrite]: #198
-#202 := [monotonicity #199]: #201
-#275 := [monotonicity #202 #272]: #274
-#281 := [trans #275 #279]: #280
-#284 := [monotonicity #281]: #283
-#290 := [trans #284 #288]: #289
-#293 := [monotonicity #290]: #292
-#297 := [trans #293 #295]: #296
-#366 := [monotonicity #297]: #365
-#372 := [trans #366 #370]: #371
-#362 := (iff #81 #361)
-#363 := [rewrite]: #362
-#375 := [monotonicity #363 #372]: #374
-#381 := [trans #375 #379]: #380
-#384 := [monotonicity #381]: #383
-#388 := [trans #384 #386]: #387
-#359 := (iff #80 #26)
-#360 := [rewrite]: #359
-#391 := [monotonicity #360 #388]: #390
-#397 := [trans #391 #395]: #396
-#357 := (iff #79 #356)
-#358 := [rewrite]: #357
-#400 := [monotonicity #358 #397]: #399
-#406 := [trans #400 #404]: #405
-#409 := [monotonicity #406]: #408
-#415 := [trans #409 #413]: #414
-#418 := [monotonicity #415]: #417
-#423 := [trans #418 #421]: #422
-#426 := [monotonicity #423]: #425
-#430 := [trans #426 #428]: #429
-#354 := (iff #76 #344)
-#349 := (implies true #344)
-#352 := (iff #349 #344)
-#353 := [rewrite]: #352
-#350 := (iff #76 #349)
-#347 := (iff #75 #344)
-#341 := (implies #29 #336)
-#345 := (iff #341 #344)
-#346 := [rewrite]: #345
-#342 := (iff #75 #341)
-#339 := (iff #74 #336)
-#332 := (implies #40 #327)
-#337 := (iff #332 #336)
-#338 := [rewrite]: #337
-#333 := (iff #74 #332)
-#330 := (iff #73 #327)
-#323 := (implies #29 #311)
-#328 := (iff #323 #327)
-#329 := [rewrite]: #328
-#324 := (iff #73 #323)
-#321 := (iff #72 #311)
-#316 := (implies true #311)
-#319 := (iff #316 #311)
-#320 := [rewrite]: #319
-#317 := (iff #72 #316)
-#314 := (iff #71 #311)
-#307 := (implies #191 #302)
-#312 := (iff #307 #311)
-#313 := [rewrite]: #312
-#308 := (iff #71 #307)
-#305 := (iff #70 #302)
-#298 := (implies #194 #286)
-#303 := (iff #298 #302)
-#304 := [rewrite]: #303
-#299 := (iff #70 #298)
-#195 := (iff #44 #194)
-#196 := [rewrite]: #195
-#300 := [monotonicity #196 #297]: #299
-#306 := [trans #300 #304]: #305
-#192 := (iff #42 #191)
-#193 := [rewrite]: #192
-#309 := [monotonicity #193 #306]: #308
-#315 := [trans #309 #313]: #314
-#318 := [monotonicity #315]: #317
-#322 := [trans #318 #320]: #321
-#325 := [monotonicity #322]: #324
-#331 := [trans #325 #329]: #330
-#334 := [monotonicity #331]: #333
-#340 := [trans #334 #338]: #339
-#343 := [monotonicity #340]: #342
-#348 := [trans #343 #346]: #347
-#351 := [monotonicity #348]: #350
-#355 := [trans #351 #353]: #354
-#433 := [monotonicity #355 #430]: #432
-#436 := [monotonicity #433]: #435
-#441 := [trans #436 #439]: #440
-#444 := [monotonicity #441]: #443
-#450 := [trans #444 #448]: #449
-#453 := [monotonicity #450]: #452
-#458 := [trans #453 #456]: #457
-#461 := [monotonicity #458]: #460
-#465 := [trans #461 #463]: #464
-#607 := [monotonicity #465 #604]: #606
-#610 := [monotonicity #607]: #609
-#615 := [trans #610 #613]: #614
-#189 := (iff #37 #188)
-#190 := [rewrite]: #189
-#618 := [monotonicity #190 #615]: #617
-#624 := [trans #618 #622]: #623
-#186 := (iff #35 #185)
-#183 := (iff #34 #180)
-#176 := (implies #173 #33)
-#181 := (iff #176 #180)
-#182 := [rewrite]: #181
-#177 := (iff #34 #176)
-#174 := (iff #31 #173)
-#175 := [rewrite]: #174
-#178 := [monotonicity #175]: #177
-#184 := [trans #178 #182]: #183
-#187 := [quant-intro #184]: #186
-#627 := [monotonicity #187 #624]: #626
-#633 := [trans #627 #631]: #632
-#636 := [monotonicity #633]: #635
-#641 := [trans #636 #639]: #640
-#644 := [monotonicity #641]: #643
-#648 := [trans #644 #646]: #647
-#651 := [monotonicity #172 #648]: #650
-#657 := [trans #651 #655]: #656
-#660 := [monotonicity #657 #172]: #659
-#665 := [trans #660 #663]: #664
-#668 := [monotonicity #170 #665]: #667
-#674 := [trans #668 #672]: #673
-#677 := [monotonicity #674 #170]: #676
-#682 := [trans #677 #680]: #681
-#162 := (iff #15 #161)
-#159 := (iff #14 #158)
-#156 := (iff #13 #12)
-#157 := [rewrite]: #156
-#160 := [monotonicity #157]: #159
-#163 := [monotonicity #160]: #162
-#685 := [monotonicity #163 #682]: #684
-#691 := [trans #685 #689]: #690
-#694 := [monotonicity #691]: #693
-#699 := [trans #694 #697]: #698
-#702 := [monotonicity #699]: #701
-#706 := [trans #702 #704]: #705
-#709 := [monotonicity #706]: #708
-#715 := [trans #709 #713]: #714
-#718 := [monotonicity #715]: #717
-#722 := [trans #718 #720]: #721
-#725 := [monotonicity #722]: #724
-#1107 := [trans #725 #1105]: #1106
-#155 := [asserted]: #139
-#1108 := [mp #155 #1107]: #1103
-#1109 := [not-or-elim #1108]: #9
-#2193 := [trans #1109 #2192]: #2202
-#1888 := (not #1154)
-#1974 := (or #1540 #1888)
-#1889 := [def-axiom]: #1974
-#2194 := [unit-resolution #1889 #2205]: #1888
-#2195 := (not #2202)
-#2196 := (or #2195 #1154)
-#2197 := [th-lemma]: #2196
-#2198 := [unit-resolution #2197 #2194 #2193]: false
-#2199 := [lemma #2198]: #1540
-#2393 := (or #1545 #2390)
-#1708 := (forall (vars (?x7 int)) #1705)
-#1801 := (or #1708 #1798)
-#1804 := (not #1801)
-#1807 := (or #560 #551 #542 #886 #1654 #927 #1804)
-#1810 := (not #1807)
-#1612 := (forall (vars (?x3 int)) #1607)
-#1618 := (not #1612)
-#1619 := (or #221 #1618)
-#1620 := (not #1619)
-#1648 := (or #1620 #1645)
-#1657 := (not #1648)
-#1667 := (or #367 #401 #376 #886 #1654 #1655 #1656 #840 #850 #1657)
-#1668 := (not #1667)
-#1658 := (or #310 #301 #886 #1654 #1655 #1656 #840 #854 #1657)
-#1659 := (not #1658)
-#1673 := (or #1659 #1668)
-#1679 := (not #1673)
-#1680 := (or #886 #1654 #926 #1679)
-#1681 := (not #1680)
-#1813 := (or #1681 #1810)
-#1816 := (not #1813)
-#1590 := (forall (vars (?x2 int)) #1585)
-#1784 := (not #1590)
-#1568 := (forall (vars (?x1 int)) #1563)
-#1783 := (not #1568)
-#1819 := (or #619 #886 #1654 #1783 #1784 #1816)
-#1822 := (not #1819)
-#1825 := (or #1545 #1822)
-#2394 := (iff #1825 #2393)
-#2391 := (iff #1822 #2390)
-#2388 := (iff #1819 #2387)
-#2385 := (iff #1816 #2384)
-#2382 := (iff #1813 #2381)
-#2379 := (iff #1810 #2378)
-#2376 := (iff #1807 #2375)
-#2373 := (iff #1804 #2372)
-#2370 := (iff #1801 #2369)
-#2367 := (iff #1708 #2364)
-#2365 := (iff #1705 #1705)
-#2366 := [refl]: #2365
-#2368 := [quant-intro #2366]: #2367
-#2371 := [monotonicity #2368]: #2370
-#2374 := [monotonicity #2371]: #2373
-#2377 := [monotonicity #2374]: #2376
-#2380 := [monotonicity #2377]: #2379
-#2362 := (iff #1681 #2361)
-#2359 := (iff #1680 #2358)
-#2356 := (iff #1679 #2355)
-#2353 := (iff #1673 #2352)
-#2350 := (iff #1668 #2349)
-#2347 := (iff #1667 #2346)
-#2338 := (iff #1657 #2337)
-#2335 := (iff #1648 #2334)
-#2332 := (iff #1620 #2331)
-#2329 := (iff #1619 #2328)
-#2326 := (iff #1618 #2325)
-#2323 := (iff #1612 #2320)
-#2321 := (iff #1607 #1607)
-#2322 := [refl]: #2321
-#2324 := [quant-intro #2322]: #2323
-#2327 := [monotonicity #2324]: #2326
-#2330 := [monotonicity #2327]: #2329
-#2333 := [monotonicity #2330]: #2332
-#2336 := [monotonicity #2333]: #2335
-#2339 := [monotonicity #2336]: #2338
-#2348 := [monotonicity #2339]: #2347
-#2351 := [monotonicity #2348]: #2350
-#2344 := (iff #1659 #2343)
-#2341 := (iff #1658 #2340)
-#2342 := [monotonicity #2339]: #2341
-#2345 := [monotonicity #2342]: #2344
-#2354 := [monotonicity #2345 #2351]: #2353
-#2357 := [monotonicity #2354]: #2356
-#2360 := [monotonicity #2357]: #2359
-#2363 := [monotonicity #2360]: #2362
-#2383 := [monotonicity #2363 #2380]: #2382
-#2386 := [monotonicity #2383]: #2385
-#2318 := (iff #1784 #2317)
-#2315 := (iff #1590 #2312)
-#2313 := (iff #1585 #1585)
-#2314 := [refl]: #2313
-#2316 := [quant-intro #2314]: #2315
-#2319 := [monotonicity #2316]: #2318
-#2310 := (iff #1783 #2309)
-#2307 := (iff #1568 #2304)
-#2305 := (iff #1563 #1563)
-#2306 := [refl]: #2305
-#2308 := [quant-intro #2306]: #2307
-#2311 := [monotonicity #2308]: #2310
-#2389 := [monotonicity #2311 #2319 #2386]: #2388
-#2392 := [monotonicity #2389]: #2391
-#2395 := [monotonicity #2392]: #2394
-#1304 := (not #1303)
-#1481 := (and #1304 #1305)
-#1484 := (not #1481)
-#1500 := (or #1484 #1495)
-#1503 := (not #1500)
-#1283 := (not #1282)
-#1472 := (and #1283 #1284)
-#1475 := (not #1472)
-#1478 := (or #1469 #1475)
-#1506 := (and #1478 #1503)
-#1273 := (not #963)
-#1276 := (forall (vars (?x7 int)) #1273)
-#1509 := (or #1276 #1506)
-#1515 := (and #466 #469 #472 #776 #779 #926 #1509)
-#1401 := (not #1396)
-#1404 := (and #1192 #1401)
-#1407 := (not #1404)
-#1410 := (or #1383 #1407)
-#1413 := (not #1410)
-#1204 := (not #221)
-#1214 := (and #1204 #819)
-#1419 := (or #1214 #1413)
-#1447 := (and #82 #356 #361 #776 #779 #788 #791 #837 #854 #1419)
-#1431 := (and #191 #194 #776 #779 #788 #791 #837 #850 #1419)
-#1452 := (or #1431 #1447)
-#1458 := (and #776 #779 #927 #1452)
-#1520 := (or #1458 #1515)
-#1526 := (and #188 #769 #776 #779 #1043 #1520)
-#1348 := (and #1155 #1157)
-#1351 := (not #1348)
-#1357 := (or #1154 #1351)
-#1362 := (not #1357)
-#1531 := (or #1362 #1526)
-#1828 := (iff #1531 #1825)
-#1746 := (or #1303 #1731 #1495)
-#1758 := (or #1757 #1746)
-#1759 := (not #1758)
-#1764 := (or #1708 #1759)
-#1770 := (not #1764)
-#1771 := (or #560 #551 #542 #886 #1654 #927 #1770)
-#1772 := (not #1771)
-#1777 := (or #1681 #1772)
-#1785 := (not #1777)
-#1786 := (or #619 #886 #1654 #1783 #1784 #1785)
-#1787 := (not #1786)
-#1792 := (or #1545 #1787)
-#1826 := (iff #1792 #1825)
-#1823 := (iff #1787 #1822)
-#1820 := (iff #1786 #1819)
-#1817 := (iff #1785 #1816)
-#1814 := (iff #1777 #1813)
-#1811 := (iff #1772 #1810)
-#1808 := (iff #1771 #1807)
-#1805 := (iff #1770 #1804)
-#1802 := (iff #1764 #1801)
-#1799 := (iff #1759 #1798)
-#1796 := (iff #1758 #1795)
-#1797 := [rewrite]: #1796
-#1800 := [monotonicity #1797]: #1799
-#1803 := [monotonicity #1800]: #1802
-#1806 := [monotonicity #1803]: #1805
-#1809 := [monotonicity #1806]: #1808
-#1812 := [monotonicity #1809]: #1811
-#1815 := [monotonicity #1812]: #1814
-#1818 := [monotonicity #1815]: #1817
-#1821 := [monotonicity #1818]: #1820
-#1824 := [monotonicity #1821]: #1823
-#1827 := [monotonicity #1824]: #1826
-#1793 := (iff #1531 #1792)
-#1790 := (iff #1526 #1787)
-#1780 := (and #188 #1568 #776 #779 #1590 #1777)
-#1788 := (iff #1780 #1787)
-#1789 := [rewrite]: #1788
-#1781 := (iff #1526 #1780)
-#1778 := (iff #1520 #1777)
-#1775 := (iff #1515 #1772)
-#1767 := (and #466 #469 #472 #776 #779 #926 #1764)
-#1773 := (iff #1767 #1772)
-#1774 := [rewrite]: #1773
-#1768 := (iff #1515 #1767)
-#1765 := (iff #1509 #1764)
-#1762 := (iff #1506 #1759)
-#1751 := (not #1746)
-#1754 := (and #1726 #1751)
-#1760 := (iff #1754 #1759)
-#1761 := [rewrite]: #1760
-#1755 := (iff #1506 #1754)
-#1752 := (iff #1503 #1751)
-#1749 := (iff #1500 #1746)
-#1732 := (or #1303 #1731)
-#1743 := (or #1732 #1495)
-#1747 := (iff #1743 #1746)
-#1748 := [rewrite]: #1747
-#1744 := (iff #1500 #1743)
-#1741 := (iff #1484 #1732)
-#1733 := (not #1732)
-#1736 := (not #1733)
-#1739 := (iff #1736 #1732)
-#1740 := [rewrite]: #1739
-#1737 := (iff #1484 #1736)
-#1734 := (iff #1481 #1733)
-#1735 := [rewrite]: #1734
-#1738 := [monotonicity #1735]: #1737
-#1742 := [trans #1738 #1740]: #1741
-#1745 := [monotonicity #1742]: #1744
-#1750 := [trans #1745 #1748]: #1749
-#1753 := [monotonicity #1750]: #1752
-#1729 := (iff #1478 #1726)
-#1712 := (or #1282 #1711)
-#1723 := (or #1469 #1712)
-#1727 := (iff #1723 #1726)
-#1728 := [rewrite]: #1727
-#1724 := (iff #1478 #1723)
-#1721 := (iff #1475 #1712)
-#1713 := (not #1712)
-#1716 := (not #1713)
-#1719 := (iff #1716 #1712)
-#1720 := [rewrite]: #1719
-#1717 := (iff #1475 #1716)
-#1714 := (iff #1472 #1713)
-#1715 := [rewrite]: #1714
-#1718 := [monotonicity #1715]: #1717
-#1722 := [trans #1718 #1720]: #1721
-#1725 := [monotonicity #1722]: #1724
-#1730 := [trans #1725 #1728]: #1729
-#1756 := [monotonicity #1730 #1753]: #1755
-#1763 := [trans #1756 #1761]: #1762
-#1709 := (iff #1276 #1708)
-#1706 := (iff #1273 #1705)
-#1703 := (iff #963 #1700)
-#1686 := (or #1548 #953)
-#1697 := (or #105 #1686)
-#1701 := (iff #1697 #1700)
-#1702 := [rewrite]: #1701
-#1698 := (iff #963 #1697)
-#1695 := (iff #960 #1686)
-#1687 := (not #1686)
-#1690 := (not #1687)
-#1693 := (iff #1690 #1686)
-#1694 := [rewrite]: #1693
-#1691 := (iff #960 #1690)
-#1688 := (iff #957 #1687)
-#1689 := [rewrite]: #1688
-#1692 := [monotonicity #1689]: #1691
-#1696 := [trans #1692 #1694]: #1695
-#1699 := [monotonicity #1696]: #1698
-#1704 := [trans #1699 #1702]: #1703
-#1707 := [monotonicity #1704]: #1706
-#1710 := [quant-intro #1707]: #1709
-#1766 := [monotonicity #1710 #1763]: #1765
-#1769 := [monotonicity #1766]: #1768
-#1776 := [trans #1769 #1774]: #1775
-#1684 := (iff #1458 #1681)
-#1676 := (and #776 #779 #927 #1673)
-#1682 := (iff #1676 #1681)
-#1683 := [rewrite]: #1682
-#1677 := (iff #1458 #1676)
-#1674 := (iff #1452 #1673)
-#1671 := (iff #1447 #1668)
-#1664 := (and #82 #356 #361 #776 #779 #788 #791 #837 #854 #1648)
-#1669 := (iff #1664 #1668)
-#1670 := [rewrite]: #1669
-#1665 := (iff #1447 #1664)
-#1649 := (iff #1419 #1648)
-#1646 := (iff #1413 #1645)
-#1643 := (iff #1410 #1640)
-#1626 := (or #1625 #1396)
-#1637 := (or #1383 #1626)
-#1641 := (iff #1637 #1640)
-#1642 := [rewrite]: #1641
-#1638 := (iff #1410 #1637)
-#1635 := (iff #1407 #1626)
-#1627 := (not #1626)
-#1630 := (not #1627)
-#1633 := (iff #1630 #1626)
-#1634 := [rewrite]: #1633
-#1631 := (iff #1407 #1630)
-#1628 := (iff #1404 #1627)
-#1629 := [rewrite]: #1628
-#1632 := [monotonicity #1629]: #1631
-#1636 := [trans #1632 #1634]: #1635
-#1639 := [monotonicity #1636]: #1638
-#1644 := [trans #1639 #1642]: #1643
-#1647 := [monotonicity #1644]: #1646
-#1623 := (iff #1214 #1620)
-#1615 := (and #1204 #1612)
-#1621 := (iff #1615 #1620)
-#1622 := [rewrite]: #1621
-#1616 := (iff #1214 #1615)
-#1613 := (iff #819 #1612)
-#1610 := (iff #816 #1607)
-#1593 := (or #1548 #805)
-#1604 := (or #801 #1593)
-#1608 := (iff #1604 #1607)
-#1609 := [rewrite]: #1608
-#1605 := (iff #816 #1604)
-#1602 := (iff #813 #1593)
-#1594 := (not #1593)
-#1597 := (not #1594)
-#1600 := (iff #1597 #1593)
-#1601 := [rewrite]: #1600
-#1598 := (iff #813 #1597)
-#1595 := (iff #810 #1594)
-#1596 := [rewrite]: #1595
-#1599 := [monotonicity #1596]: #1598
-#1603 := [trans #1599 #1601]: #1602
-#1606 := [monotonicity #1603]: #1605
-#1611 := [trans #1606 #1609]: #1610
-#1614 := [quant-intro #1611]: #1613
-#1617 := [monotonicity #1614]: #1616
-#1624 := [trans #1617 #1622]: #1623
-#1650 := [monotonicity #1624 #1647]: #1649
-#1666 := [monotonicity #1650]: #1665
-#1672 := [trans #1666 #1670]: #1671
-#1662 := (iff #1431 #1659)
-#1651 := (and #191 #194 #776 #779 #788 #791 #837 #850 #1648)
-#1660 := (iff #1651 #1659)
-#1661 := [rewrite]: #1660
-#1652 := (iff #1431 #1651)
-#1653 := [monotonicity #1650]: #1652
-#1663 := [trans #1653 #1661]: #1662
-#1675 := [monotonicity #1663 #1672]: #1674
-#1678 := [monotonicity #1675]: #1677
-#1685 := [trans #1678 #1683]: #1684
-#1779 := [monotonicity #1685 #1776]: #1778
-#1591 := (iff #1043 #1590)
-#1588 := (iff #1040 #1585)
-#1571 := (or #1548 #1029)
-#1582 := (or #1026 #1571)
-#1586 := (iff #1582 #1585)
-#1587 := [rewrite]: #1586
-#1583 := (iff #1040 #1582)
-#1580 := (iff #1037 #1571)
-#1572 := (not #1571)
-#1575 := (not #1572)
-#1578 := (iff #1575 #1571)
-#1579 := [rewrite]: #1578
-#1576 := (iff #1037 #1575)
-#1573 := (iff #1034 #1572)
-#1574 := [rewrite]: #1573
-#1577 := [monotonicity #1574]: #1576
-#1581 := [trans #1577 #1579]: #1580
-#1584 := [monotonicity #1581]: #1583
-#1589 := [trans #1584 #1587]: #1588
-#1592 := [quant-intro #1589]: #1591
-#1569 := (iff #769 #1568)
-#1566 := (iff #766 #1563)
-#1549 := (or #749 #1548)
-#1560 := (or #1549 #762)
-#1564 := (iff #1560 #1563)
-#1565 := [rewrite]: #1564
-#1561 := (iff #766 #1560)
-#1558 := (iff #757 #1549)
-#1550 := (not #1549)
-#1553 := (not #1550)
-#1556 := (iff #1553 #1549)
-#1557 := [rewrite]: #1556
-#1554 := (iff #757 #1553)
-#1551 := (iff #754 #1550)
-#1552 := [rewrite]: #1551
-#1555 := [monotonicity #1552]: #1554
-#1559 := [trans #1555 #1557]: #1558
-#1562 := [monotonicity #1559]: #1561
-#1567 := [trans #1562 #1565]: #1566
-#1570 := [quant-intro #1567]: #1569
-#1782 := [monotonicity #1570 #1592 #1779]: #1781
-#1791 := [trans #1782 #1789]: #1790
-#1546 := (iff #1362 #1545)
-#1543 := (iff #1357 #1540)
-#1165 := (or #1164 #1156)
-#1537 := (or #1154 #1165)
-#1541 := (iff #1537 #1540)
-#1542 := [rewrite]: #1541
-#1538 := (iff #1357 #1537)
-#1535 := (iff #1351 #1165)
-#1292 := (not #1165)
-#1314 := (not #1292)
-#1347 := (iff #1314 #1165)
-#1534 := [rewrite]: #1347
-#1202 := (iff #1351 #1314)
-#1293 := (iff #1348 #1292)
-#1313 := [rewrite]: #1293
-#1203 := [monotonicity #1313]: #1202
-#1536 := [trans #1203 #1534]: #1535
-#1539 := [monotonicity #1536]: #1538
-#1544 := [trans #1539 #1542]: #1543
-#1547 := [monotonicity #1544]: #1546
-#1794 := [monotonicity #1547 #1791]: #1793
-#1829 := [trans #1794 #1827]: #1828
-#1299 := (+ #1298 #972)
-#1300 := (<= #1299 0::int)
-#1306 := (and #1305 #1304)
-#1307 := (not #1306)
-#1308 := (or #1307 #1300)
-#1309 := (not #1308)
-#1285 := (and #1284 #1283)
-#1286 := (not #1285)
-#1288 := (= #1287 uf_12)
-#1289 := (or #1288 #1286)
-#1315 := (and #1289 #1309)
-#1319 := (or #1276 #1315)
-#1176 := (not #784)
-#1268 := (not #542)
-#1265 := (not #551)
-#1262 := (not #560)
-#1323 := (and #1262 #1265 #1268 #1176 #930 #1319)
-#1225 := (not #846)
-#1222 := (not #840)
-#1189 := (+ ?x3!1 #806)
-#1190 := (>= #1189 0::int)
-#1191 := (not #1190)
-#1193 := (and #1192 #1191)
-#1194 := (not #1193)
-#1196 := (+ #1195 #799)
-#1197 := (<= #1196 0::int)
-#1198 := (or #1197 #1194)
-#1199 := (not #1198)
-#1218 := (or #1199 #1214)
-#1185 := (not #796)
-#1243 := (not #886)
-#1240 := (not #376)
-#1237 := (not #401)
-#1234 := (not #367)
-#1248 := (and #1234 #1237 #1240 #1243 #1176 #1185 #1218 #1222 #1225 #854)
-#1182 := (not #301)
-#1179 := (not #310)
-#1230 := (and #1179 #1182 #1176 #1185 #1218 #1222 #1225 #891)
-#1252 := (or #1230 #1248)
-#1258 := (and #1176 #1252 #927)
-#1327 := (or #1258 #1323)
-#1166 := (not #619)
-#1338 := (and #1166 #769 #1176 #1327 #1043)
-#1158 := (and #1157 #1155)
-#1159 := (not #1158)
-#1160 := (or #1159 #1154)
-#1161 := (not #1160)
-#1342 := (or #1161 #1338)
-#1532 := (iff #1342 #1531)
-#1529 := (iff #1338 #1526)
-#1523 := (and #188 #769 #781 #1520 #1043)
-#1527 := (iff #1523 #1526)
-#1528 := [rewrite]: #1527
-#1524 := (iff #1338 #1523)
-#1521 := (iff #1327 #1520)
-#1518 := (iff #1323 #1515)
-#1512 := (and #466 #469 #472 #781 #926 #1509)
-#1516 := (iff #1512 #1515)
-#1517 := [rewrite]: #1516
-#1513 := (iff #1323 #1512)
-#1510 := (iff #1319 #1509)
-#1507 := (iff #1315 #1506)
-#1504 := (iff #1309 #1503)
-#1501 := (iff #1308 #1500)
-#1498 := (iff #1300 #1495)
-#1487 := (+ #972 #1298)
-#1490 := (<= #1487 0::int)
-#1496 := (iff #1490 #1495)
-#1497 := [rewrite]: #1496
-#1491 := (iff #1300 #1490)
-#1488 := (= #1299 #1487)
-#1489 := [rewrite]: #1488
-#1492 := [monotonicity #1489]: #1491
-#1499 := [trans #1492 #1497]: #1498
-#1485 := (iff #1307 #1484)
-#1482 := (iff #1306 #1481)
-#1483 := [rewrite]: #1482
-#1486 := [monotonicity #1483]: #1485
-#1502 := [monotonicity #1486 #1499]: #1501
-#1505 := [monotonicity #1502]: #1504
-#1479 := (iff #1289 #1478)
-#1476 := (iff #1286 #1475)
-#1473 := (iff #1285 #1472)
-#1474 := [rewrite]: #1473
-#1477 := [monotonicity #1474]: #1476
-#1470 := (iff #1288 #1469)
-#1471 := [rewrite]: #1470
-#1480 := [monotonicity #1471 #1477]: #1479
-#1508 := [monotonicity #1480 #1505]: #1507
-#1511 := [monotonicity #1508]: #1510
-#1367 := (iff #1176 #781)
-#1368 := [rewrite]: #1367
-#1467 := (iff #1268 #472)
-#1468 := [rewrite]: #1467
-#1465 := (iff #1265 #469)
-#1466 := [rewrite]: #1465
-#1463 := (iff #1262 #466)
-#1464 := [rewrite]: #1463
-#1514 := [monotonicity #1464 #1466 #1468 #1368 #934 #1511]: #1513
-#1519 := [trans #1514 #1517]: #1518
-#1461 := (iff #1258 #1458)
-#1455 := (and #781 #1452 #927)
-#1459 := (iff #1455 #1458)
-#1460 := [rewrite]: #1459
-#1456 := (iff #1258 #1455)
-#1453 := (iff #1252 #1452)
-#1450 := (iff #1248 #1447)
-#1444 := (and #82 #356 #361 #776 #781 #793 #1419 #837 #843 #854)
-#1448 := (iff #1444 #1447)
-#1449 := [rewrite]: #1448
-#1445 := (iff #1248 #1444)
-#1426 := (iff #1225 #843)
-#1427 := [rewrite]: #1426
-#1424 := (iff #1222 #837)
-#1425 := [rewrite]: #1424
-#1422 := (iff #1218 #1419)
-#1416 := (or #1413 #1214)
-#1420 := (iff #1416 #1419)
-#1421 := [rewrite]: #1420
-#1417 := (iff #1218 #1416)
-#1414 := (iff #1199 #1413)
-#1411 := (iff #1198 #1410)
-#1408 := (iff #1194 #1407)
-#1405 := (iff #1193 #1404)
-#1402 := (iff #1191 #1401)
-#1399 := (iff #1190 #1396)
-#1388 := (+ #806 ?x3!1)
-#1391 := (>= #1388 0::int)
-#1397 := (iff #1391 #1396)
-#1398 := [rewrite]: #1397
-#1392 := (iff #1190 #1391)
-#1389 := (= #1189 #1388)
-#1390 := [rewrite]: #1389
-#1393 := [monotonicity #1390]: #1392
-#1400 := [trans #1393 #1398]: #1399
-#1403 := [monotonicity #1400]: #1402
-#1406 := [monotonicity #1403]: #1405
-#1409 := [monotonicity #1406]: #1408
-#1386 := (iff #1197 #1383)
-#1375 := (+ #799 #1195)
-#1378 := (<= #1375 0::int)
-#1384 := (iff #1378 #1383)
-#1385 := [rewrite]: #1384
-#1379 := (iff #1197 #1378)
-#1376 := (= #1196 #1375)
-#1377 := [rewrite]: #1376
-#1380 := [monotonicity #1377]: #1379
-#1387 := [trans #1380 #1385]: #1386
-#1412 := [monotonicity #1387 #1409]: #1411
-#1415 := [monotonicity #1412]: #1414
-#1418 := [monotonicity #1415]: #1417
-#1423 := [trans #1418 #1421]: #1422
-#1373 := (iff #1185 #793)
-#1374 := [rewrite]: #1373
-#1442 := (iff #1243 #776)
-#1443 := [rewrite]: #1442
-#1440 := (iff #1240 #361)
-#1441 := [rewrite]: #1440
-#1438 := (iff #1237 #356)
-#1439 := [rewrite]: #1438
-#1436 := (iff #1234 #82)
-#1437 := [rewrite]: #1436
-#1446 := [monotonicity #1437 #1439 #1441 #1443 #1368 #1374 #1423 #1425 #1427]: #1445
-#1451 := [trans #1446 #1449]: #1450
-#1434 := (iff #1230 #1431)
-#1428 := (and #191 #194 #781 #793 #1419 #837 #843 #850)
-#1432 := (iff #1428 #1431)
-#1433 := [rewrite]: #1432
-#1429 := (iff #1230 #1428)
-#1371 := (iff #1182 #194)
-#1372 := [rewrite]: #1371
-#1369 := (iff #1179 #191)
-#1370 := [rewrite]: #1369
-#1430 := [monotonicity #1370 #1372 #1368 #1374 #1423 #1425 #1427 #895]: #1429
-#1435 := [trans #1430 #1433]: #1434
-#1454 := [monotonicity #1435 #1451]: #1453
-#1457 := [monotonicity #1368 #1454]: #1456
-#1462 := [trans #1457 #1460]: #1461
-#1522 := [monotonicity #1462 #1519]: #1521
-#1365 := (iff #1166 #188)
-#1366 := [rewrite]: #1365
-#1525 := [monotonicity #1366 #1368 #1522]: #1524
-#1530 := [trans #1525 #1528]: #1529
-#1363 := (iff #1161 #1362)
-#1360 := (iff #1160 #1357)
-#1354 := (or #1351 #1154)
-#1358 := (iff #1354 #1357)
-#1359 := [rewrite]: #1358
-#1355 := (iff #1160 #1354)
-#1352 := (iff #1159 #1351)
-#1349 := (iff #1158 #1348)
-#1350 := [rewrite]: #1349
-#1353 := [monotonicity #1350]: #1352
-#1356 := [monotonicity #1353]: #1355
-#1361 := [trans #1356 #1359]: #1360
-#1364 := [monotonicity #1361]: #1363
-#1533 := [monotonicity #1364 #1530]: #1532
-#1138 := (or #619 #772 #784 #1021 #1046)
-#1143 := (and #769 #1138)
-#1146 := (not #1143)
-#1343 := (~ #1146 #1342)
-#1339 := (not #1138)
-#1340 := (~ #1339 #1338)
-#1335 := (not #1046)
-#1336 := (~ #1335 #1043)
-#1333 := (~ #1043 #1043)
-#1331 := (~ #1040 #1040)
-#1332 := [refl]: #1331
-#1334 := [nnf-pos #1332]: #1333
-#1337 := [nnf-neg #1334]: #1336
-#1328 := (not #1021)
-#1329 := (~ #1328 #1327)
-#1324 := (not #1016)
-#1325 := (~ #1324 #1323)
-#1320 := (not #991)
-#1321 := (~ #1320 #1319)
-#1316 := (not #988)
-#1317 := (~ #1316 #1315)
-#1310 := (not #985)
-#1311 := (~ #1310 #1309)
-#1312 := [sk]: #1311
-#1294 := (not #969)
-#1295 := (~ #1294 #1289)
-#1290 := (~ #966 #1289)
-#1291 := [sk]: #1290
-#1296 := [nnf-neg #1291]: #1295
-#1318 := [nnf-neg #1296 #1312]: #1317
-#1277 := (~ #969 #1276)
-#1274 := (~ #1273 #1273)
-#1275 := [refl]: #1274
-#1278 := [nnf-neg #1275]: #1277
-#1322 := [nnf-neg #1278 #1318]: #1321
-#1271 := (~ #930 #930)
-#1272 := [refl]: #1271
-#1177 := (~ #1176 #1176)
-#1178 := [refl]: #1177
-#1269 := (~ #1268 #1268)
-#1270 := [refl]: #1269
-#1266 := (~ #1265 #1265)
-#1267 := [refl]: #1266
-#1263 := (~ #1262 #1262)
-#1264 := [refl]: #1263
-#1326 := [nnf-neg #1264 #1267 #1270 #1178 #1272 #1322]: #1325
-#1259 := (not #946)
-#1260 := (~ #1259 #1258)
-#1256 := (~ #927 #927)
-#1257 := [refl]: #1256
-#1253 := (not #921)
-#1254 := (~ #1253 #1252)
-#1249 := (not #916)
-#1250 := (~ #1249 #1248)
-#1246 := (~ #854 #854)
-#1247 := [refl]: #1246
-#1226 := (~ #1225 #1225)
-#1227 := [refl]: #1226
-#1223 := (~ #1222 #1222)
-#1224 := [refl]: #1223
-#1219 := (not #833)
-#1220 := (~ #1219 #1218)
-#1215 := (not #828)
-#1216 := (~ #1215 #1214)
-#1211 := (not #822)
-#1212 := (~ #1211 #819)
-#1209 := (~ #819 #819)
-#1207 := (~ #816 #816)
-#1208 := [refl]: #1207
-#1210 := [nnf-pos #1208]: #1209
-#1213 := [nnf-neg #1210]: #1212
-#1205 := (~ #1204 #1204)
-#1206 := [refl]: #1205
-#1217 := [nnf-neg #1206 #1213]: #1216
-#1200 := (~ #822 #1199)
-#1201 := [sk]: #1200
-#1221 := [nnf-neg #1201 #1217]: #1220
-#1186 := (~ #1185 #1185)
-#1187 := [refl]: #1186
-#1244 := (~ #1243 #1243)
-#1245 := [refl]: #1244
-#1241 := (~ #1240 #1240)
-#1242 := [refl]: #1241
-#1238 := (~ #1237 #1237)
-#1239 := [refl]: #1238
-#1235 := (~ #1234 #1234)
-#1236 := [refl]: #1235
-#1251 := [nnf-neg #1236 #1239 #1242 #1245 #1178 #1187 #1221 #1224 #1227 #1247]: #1250
-#1231 := (not #881)
-#1232 := (~ #1231 #1230)
-#1228 := (~ #891 #891)
-#1229 := [refl]: #1228
-#1183 := (~ #1182 #1182)
-#1184 := [refl]: #1183
-#1180 := (~ #1179 #1179)
-#1181 := [refl]: #1180
-#1233 := [nnf-neg #1181 #1184 #1178 #1187 #1221 #1224 #1227 #1229]: #1232
-#1255 := [nnf-neg #1233 #1251]: #1254
-#1261 := [nnf-neg #1178 #1255 #1257]: #1260
-#1330 := [nnf-neg #1261 #1326]: #1329
-#1173 := (not #772)
-#1174 := (~ #1173 #769)
-#1171 := (~ #769 #769)
-#1169 := (~ #766 #766)
-#1170 := [refl]: #1169
-#1172 := [nnf-pos #1170]: #1171
-#1175 := [nnf-neg #1172]: #1174
-#1167 := (~ #1166 #1166)
-#1168 := [refl]: #1167
-#1341 := [nnf-neg #1168 #1175 #1178 #1330 #1337]: #1340
-#1162 := (~ #772 #1161)
-#1163 := [sk]: #1162
-#1344 := [nnf-neg #1163 #1341]: #1343
-#1110 := (not #1075)
-#1147 := (iff #1110 #1146)
-#1144 := (iff #1075 #1143)
-#1141 := (iff #1072 #1138)
-#1123 := (or #619 #784 #1021 #1046)
-#1135 := (or #772 #1123)
-#1139 := (iff #1135 #1138)
-#1140 := [rewrite]: #1139
-#1136 := (iff #1072 #1135)
-#1133 := (iff #1069 #1123)
-#1128 := (and true #1123)
-#1131 := (iff #1128 #1123)
-#1132 := [rewrite]: #1131
-#1129 := (iff #1069 #1128)
-#1126 := (iff #1064 #1123)
-#1120 := (or false #619 #784 #1021 #1046)
-#1124 := (iff #1120 #1123)
-#1125 := [rewrite]: #1124
-#1121 := (iff #1064 #1120)
-#1118 := (iff #652 false)
-#1116 := (iff #652 #740)
-#1115 := (iff #9 true)
-#1113 := [iff-true #1109]: #1115
-#1117 := [monotonicity #1113]: #1116
-#1119 := [trans #1117 #744]: #1118
-#1122 := [monotonicity #1119]: #1121
-#1127 := [trans #1122 #1125]: #1126
-#1130 := [monotonicity #1113 #1127]: #1129
-#1134 := [trans #1130 #1132]: #1133
-#1137 := [monotonicity #1134]: #1136
-#1142 := [trans #1137 #1140]: #1141
-#1145 := [monotonicity #1142]: #1144
-#1148 := [monotonicity #1145]: #1147
-#1111 := [not-or-elim #1108]: #1110
-#1149 := [mp #1111 #1148]: #1146
-#1345 := [mp~ #1149 #1344]: #1342
-#1346 := [mp #1345 #1533]: #1531
-#1830 := [mp #1346 #1829]: #1825
-#2396 := [mp #1830 #2395]: #2393
-#1909 := [unit-resolution #2396 #2199]: #2390
-#2214 := (or #2387 #2381)
-#2210 := [def-axiom]: #2214
-#2414 := [unit-resolution #2210 #1909]: #2381
-#2426 := (uf_3 uf_11)
-#2430 := (= uf_12 #2426)
-#2480 := (= #36 #2426)
-#2478 := (= #2426 #36)
-#2463 := [hypothesis]: #2378
-#2138 := (or #2375 #466)
-#2139 := [def-axiom]: #2138
-#2474 := [unit-resolution #2139 #2463]: #466
-#2475 := [symm #2474]: #98
-#2479 := [monotonicity #2475]: #2478
-#2481 := [symm #2479]: #2480
-#2482 := (= uf_12 #36)
-#2221 := (or #2387 #188)
-#2222 := [def-axiom]: #2221
-#2476 := [unit-resolution #2222 #1909]: #188
-#2132 := (or #2375 #469)
-#2140 := [def-axiom]: #2132
-#2466 := [unit-resolution #2140 #2463]: #469
-#2477 := [symm #2466]: #100
-#2483 := [trans #2477 #2476]: #2482
-#2484 := [trans #2483 #2481]: #2430
-#2458 := (not #2430)
-#2424 := (>= uf_11 0::int)
-#2425 := (not #2424)
-#2421 := (* -1::int uf_11)
-#2422 := (+ uf_1 #2421)
-#2423 := (<= #2422 0::int)
-#2436 := (or #2423 #2425 #2430)
-#2441 := (not #2436)
-#2227 := (or #2375 #2369)
-#2219 := [def-axiom]: #2227
-#2464 := [unit-resolution #2219 #2463]: #2369
-#2238 := (or #2375 #926)
-#2225 := [def-axiom]: #2238
-#2465 := [unit-resolution #2225 #2463]: #926
-#2031 := (+ uf_6 #972)
-#2032 := (<= #2031 0::int)
-#2467 := (or #551 #2032)
-#2468 := [th-lemma]: #2467
-#2469 := [unit-resolution #2468 #2466]: #2032
-#1925 := (not #2032)
-#1915 := (or #1795 #1925 #927)
-#2004 := (+ uf_4 #1301)
-#2005 := (<= #2004 0::int)
-#1918 := (not #2005)
-#1910 := [hypothesis]: #926
-#1911 := [hypothesis]: #1798
-#2086 := (or #1795 #1304)
-#2239 := [def-axiom]: #2086
-#1916 := [unit-resolution #2239 #1911]: #1304
-#1919 := (or #1918 #927 #1303)
-#1921 := [th-lemma]: #1919
-#1917 := [unit-resolution #1921 #1916 #1910]: #1918
-#2021 := (+ uf_6 #1493)
-#2022 := (>= #2021 0::int)
-#1930 := (not #2022)
-#1936 := [hypothesis]: #2032
-#2243 := (not #1495)
-#2241 := (or #1795 #2243)
-#2244 := [def-axiom]: #2241
-#1922 := [unit-resolution #2244 #1911]: #2243
-#1931 := (or #1930 #1495 #1925)
-#1924 := [hypothesis]: #2243
-#1926 := [hypothesis]: #2022
-#1927 := [th-lemma #1926 #1924 #1936]: false
-#1906 := [lemma #1927]: #1931
-#1905 := [unit-resolution #1906 #1922 #1936]: #1930
-#1913 := (or #2005 #2022)
-#2240 := (or #1795 #1305)
-#2242 := [def-axiom]: #2240
-#1908 := [unit-resolution #2242 #1911]: #1305
-#2212 := (or #2387 #2312)
-#2213 := [def-axiom]: #2212
-#1912 := [unit-resolution #2213 #1909]: #2312
-#1994 := (or #2317 #1731 #2005 #2022)
-#2034 := (+ ?x8!3 #924)
-#2035 := (>= #2034 0::int)
-#2036 := (+ #1298 #1024)
-#2037 := (<= #2036 0::int)
-#2026 := (or #1731 #2037 #2035)
-#1961 := (or #2317 #2026)
-#1971 := (iff #1961 #1994)
-#1991 := (or #1731 #2005 #2022)
-#1964 := (or #2317 #1991)
-#1969 := (iff #1964 #1994)
-#1970 := [rewrite]: #1969
-#1955 := (iff #1961 #1964)
-#1993 := (iff #2026 #1991)
-#2008 := (or #1731 #2022 #2005)
-#1983 := (iff #2008 #1991)
-#1992 := [rewrite]: #1983
-#1989 := (iff #2026 #2008)
-#2007 := (iff #2035 #2005)
-#2010 := (+ #924 ?x8!3)
-#2012 := (>= #2010 0::int)
-#1997 := (iff #2012 #2005)
-#2006 := [rewrite]: #1997
-#2014 := (iff #2035 #2012)
-#2011 := (= #2034 #2010)
-#2013 := [rewrite]: #2011
-#2003 := [monotonicity #2013]: #2014
-#1998 := [trans #2003 #2006]: #2007
-#2024 := (iff #2037 #2022)
-#2038 := (+ #1024 #1298)
-#2018 := (<= #2038 0::int)
-#2023 := (iff #2018 #2022)
-#2016 := [rewrite]: #2023
-#2019 := (iff #2037 #2018)
-#2015 := (= #2036 #2038)
-#2017 := [rewrite]: #2015
-#2020 := [monotonicity #2017]: #2019
-#2009 := [trans #2020 #2016]: #2024
-#1990 := [monotonicity #2009 #1998]: #1989
-#1984 := [trans #1990 #1992]: #1993
-#1968 := [monotonicity #1984]: #1955
-#1972 := [trans #1968 #1970]: #1971
-#1963 := [quant-inst]: #1961
-#1962 := [mp #1963 #1972]: #1994
-#1914 := [unit-resolution #1962 #1912 #1908]: #1913
-#1907 := [unit-resolution #1914 #1905 #1917]: false
-#1900 := [lemma #1907]: #1915
-#2470 := [unit-resolution #1900 #2469 #2465]: #1795
-#2121 := (or #2372 #2364 #1798)
-#2136 := [def-axiom]: #2121
-#2471 := [unit-resolution #2136 #2470 #2464]: #2364
-#2235 := (not #2364)
-#2444 := (or #2235 #2441)
-#2427 := (= #2426 uf_12)
-#2428 := (or #2427 #2425 #2423)
-#2429 := (not #2428)
-#2445 := (or #2235 #2429)
-#2447 := (iff #2445 #2444)
-#2449 := (iff #2444 #2444)
-#2450 := [rewrite]: #2449
-#2442 := (iff #2429 #2441)
-#2439 := (iff #2428 #2436)
-#2433 := (or #2430 #2425 #2423)
-#2437 := (iff #2433 #2436)
-#2438 := [rewrite]: #2437
-#2434 := (iff #2428 #2433)
-#2431 := (iff #2427 #2430)
-#2432 := [rewrite]: #2431
-#2435 := [monotonicity #2432]: #2434
-#2440 := [trans #2435 #2438]: #2439
-#2443 := [monotonicity #2440]: #2442
-#2448 := [monotonicity #2443]: #2447
-#2451 := [trans #2448 #2450]: #2447
-#2446 := [quant-inst]: #2445
-#2452 := [mp #2446 #2451]: #2444
-#2472 := [unit-resolution #2452 #2471]: #2441
-#2459 := (or #2436 #2458)
-#2460 := [def-axiom]: #2459
-#2473 := [unit-resolution #2460 #2472]: #2458
-#2485 := [unit-resolution #2473 #2484]: false
-#2486 := [lemma #2485]: #2375
-#2231 := (or #2384 #2361 #2378)
-#2220 := [def-axiom]: #2231
-#2415 := [unit-resolution #2220 #2486 #2414]: #2361
-#2106 := (or #2358 #2352)
-#2248 := [def-axiom]: #2106
-#2416 := [unit-resolution #2248 #2415]: #2352
-#2417 := [hypothesis]: #840
-#2285 := (or #2340 #837)
-#1923 := [def-axiom]: #2285
-#2418 := [unit-resolution #1923 #2417]: #2340
-#1987 := (or #2346 #837)
-#1988 := [def-axiom]: #1987
-#2419 := [unit-resolution #1988 #2417]: #2346
-#2255 := (or #2355 #2343 #2349)
-#2256 := [def-axiom]: #2255
-#2420 := [unit-resolution #2256 #2419 #2418 #2416]: false
-#2403 := [lemma #2420]: #837
-#2690 := (or #840 #1977)
-#2691 := [th-lemma]: #2690
-#2692 := [unit-resolution #2691 #2403]: #1977
-#2661 := [hypothesis]: #2349
-#2272 := (or #2346 #361)
-#2273 := [def-axiom]: #2272
-#2662 := [unit-resolution #2273 #2661]: #361
-#2629 := (= #58 #1195)
-#2642 := (not #2629)
-#2630 := (+ #58 #1381)
-#2632 := (>= #2630 0::int)
-#2636 := (not #2632)
-#2402 := (+ #39 #799)
-#2405 := (<= #2402 0::int)
-#2404 := (= #39 uf_8)
-#2665 := (= uf_10 uf_8)
-#2000 := (or #2346 #82)
-#2001 := [def-axiom]: #2000
-#2663 := [unit-resolution #2001 #2661]: #82
-#2666 := [symm #2663]: #2665
-#2002 := (or #2346 #356)
-#1896 := [def-axiom]: #2002
-#2664 := [unit-resolution #1896 #2661]: #356
-#2667 := [trans #2664 #2666]: #2404
-#2668 := (not #2404)
-#2669 := (or #2668 #2405)
-#2670 := [th-lemma]: #2669
-#2671 := [unit-resolution #2670 #2667]: #2405
-#1966 := (not #1383)
-#1982 := (or #2346 #2334)
-#2264 := [def-axiom]: #1982
-#2672 := [unit-resolution #2264 #2661]: #2334
-#2537 := (= #39 #58)
-#2674 := (= #58 #39)
-#2673 := [symm #2662]: #81
-#2675 := [monotonicity #2673]: #2674
-#2677 := [symm #2675]: #2537
-#2678 := (= uf_8 #39)
-#2676 := [symm #2664]: #79
-#2679 := [trans #2663 #2676]: #2678
-#2680 := [trans #2679 #2677]: #221
-#1981 := (or #2328 #1204)
-#1960 := [def-axiom]: #1981
-#2681 := [unit-resolution #1960 #2680]: #2328
-#1953 := (or #2337 #2331 #1645)
-#2294 := [def-axiom]: #1953
-#2682 := [unit-resolution #2294 #2681 #2672]: #1645
-#2298 := (or #1640 #1966)
-#2299 := [def-axiom]: #2298
-#2683 := [unit-resolution #2299 #2682]: #1966
-#2033 := (* -1::int #58)
-#2538 := (+ #39 #2033)
-#2540 := (>= #2538 0::int)
-#2684 := (not #2537)
-#2685 := (or #2684 #2540)
-#2686 := [th-lemma]: #2685
-#2687 := [unit-resolution #2686 #2677]: #2540
-#2617 := (not #2405)
-#2637 := (not #2540)
-#2638 := (or #2636 #2637 #1383 #2617)
-#2633 := [hypothesis]: #2632
-#2609 := [hypothesis]: #2405
-#2610 := [hypothesis]: #1966
-#2634 := [hypothesis]: #2540
-#2635 := [th-lemma #2634 #2610 #2609 #2633]: false
-#2639 := [lemma #2635]: #2638
-#2688 := [unit-resolution #2639 #2687 #2683 #2671]: #2636
-#2643 := (or #2642 #2632)
-#2644 := [th-lemma]: #2643
-#2689 := [unit-resolution #2644 #2688]: #2642
-#2300 := (or #1640 #1401)
-#2301 := [def-axiom]: #2300
-#2693 := [unit-resolution #2301 #2682]: #1401
-#2694 := (not #1977)
-#2695 := (or #2628 #1396 #2694)
-#2696 := [th-lemma]: #2695
-#2697 := [unit-resolution #2696 #2693 #2692]: #2628
-#2565 := (<= #2564 0::int)
-#2552 := (+ uf_6 #1381)
-#2553 := (>= #2552 0::int)
-#2699 := (not #2553)
-#2266 := (or #2346 #854)
-#2267 := [def-axiom]: #2266
-#2698 := [unit-resolution #2267 #2661]: #854
-#2700 := (or #2699 #1383 #2617 #850)
-#2701 := [th-lemma]: #2700
-#2702 := [unit-resolution #2701 #2683 #2671 #2698]: #2699
-#2704 := (or #2553 #2565)
-#2291 := (or #1640 #1192)
-#1965 := [def-axiom]: #2291
-#2703 := [unit-resolution #1965 #2682]: #1192
-#2573 := (or #2317 #1625 #2553 #2565)
-#2541 := (+ ?x3!1 #924)
-#2542 := (>= #2541 0::int)
-#2543 := (+ #1195 #1024)
-#2544 := (<= #2543 0::int)
-#2545 := (or #1625 #2544 #2542)
-#2574 := (or #2317 #2545)
-#2581 := (iff #2574 #2573)
-#2570 := (or #1625 #2553 #2565)
-#2576 := (or #2317 #2570)
-#2579 := (iff #2576 #2573)
-#2580 := [rewrite]: #2579
-#2577 := (iff #2574 #2576)
-#2571 := (iff #2545 #2570)
-#2568 := (iff #2542 #2565)
-#2558 := (+ #924 ?x3!1)
-#2561 := (>= #2558 0::int)
-#2566 := (iff #2561 #2565)
-#2567 := [rewrite]: #2566
-#2562 := (iff #2542 #2561)
-#2559 := (= #2541 #2558)
-#2560 := [rewrite]: #2559
-#2563 := [monotonicity #2560]: #2562
-#2569 := [trans #2563 #2567]: #2568
-#2556 := (iff #2544 #2553)
-#2546 := (+ #1024 #1195)
-#2549 := (<= #2546 0::int)
-#2554 := (iff #2549 #2553)
-#2555 := [rewrite]: #2554
-#2550 := (iff #2544 #2549)
-#2547 := (= #2543 #2546)
-#2548 := [rewrite]: #2547
-#2551 := [monotonicity #2548]: #2550
-#2557 := [trans #2551 #2555]: #2556
-#2572 := [monotonicity #2557 #2569]: #2571
-#2578 := [monotonicity #2572]: #2577
-#2582 := [trans #2578 #2580]: #2581
-#2575 := [quant-inst]: #2574
-#2583 := [mp #2575 #2582]: #2573
-#2705 := [unit-resolution #2583 #1912 #2703]: #2704
-#2706 := [unit-resolution #2705 #2702]: #2565
-#2708 := (not #2628)
-#2707 := (not #2565)
-#2709 := (or #2631 #2707 #2708)
-#2710 := [th-lemma]: #2709
-#2711 := [unit-resolution #2710 #2706 #2697]: #2631
-#2658 := (not #2631)
-#2659 := (or #2658 #2629 #376)
-#2654 := (= #1195 #58)
-#2652 := (= ?x3!1 uf_7)
-#2648 := [hypothesis]: #361
-#2650 := (= ?x3!1 uf_4)
-#2649 := [hypothesis]: #2631
-#2651 := [symm #2649]: #2650
-#2653 := [trans #2651 #2648]: #2652
-#2655 := [monotonicity #2653]: #2654
-#2656 := [symm #2655]: #2629
-#2647 := [hypothesis]: #2642
-#2657 := [unit-resolution #2647 #2656]: false
-#2660 := [lemma #2657]: #2659
-#2712 := [unit-resolution #2660 #2711 #2689 #2662]: false
-#2713 := [lemma #2712]: #2346
-#2766 := [unit-resolution #2256 #2713 #2416]: #2343
-#1928 := (or #2340 #2334)
-#1929 := [def-axiom]: #1928
-#2767 := [unit-resolution #1929 #2766]: #2334
-#2515 := (= #36 #58)
-#2772 := (= #58 #36)
-#1937 := (or #2340 #191)
-#2278 := [def-axiom]: #1937
-#2768 := [unit-resolution #2278 #2766]: #191
-#2769 := [symm #2768]: #42
-#2773 := [monotonicity #2769]: #2772
-#2774 := [symm #2773]: #2515
-#2775 := (= uf_8 #36)
-#1941 := (or #2340 #194)
-#1942 := [def-axiom]: #1941
-#2770 := [unit-resolution #1942 #2766]: #194
-#2771 := [symm #2770]: #44
-#2776 := [trans #2771 #2476]: #2775
-#2777 := [trans #2776 #2774]: #221
-#2778 := [unit-resolution #1960 #2777]: #2328
-#2779 := [unit-resolution #2294 #2778 #2767]: #1645
-#2780 := [unit-resolution #2301 #2779]: #1401
-#2781 := [unit-resolution #2696 #2780 #2692]: #2628
-#2510 := (+ uf_6 #799)
-#2511 := (<= #2510 0::int)
-#2782 := (or #301 #2511)
-#2783 := [th-lemma]: #2782
-#2784 := [unit-resolution #2783 #2770]: #2511
-#2785 := [unit-resolution #2299 #2779]: #1966
-#2786 := (not #2511)
-#2787 := (or #2699 #1383 #2786)
-#2788 := [th-lemma]: #2787
-#2789 := [unit-resolution #2788 #2785 #2784]: #2699
-#2790 := [unit-resolution #1965 #2779]: #1192
-#2791 := [unit-resolution #2583 #1912 #2790 #2789]: #2565
-#2792 := [unit-resolution #2710 #2791 #2781]: #2631
-#2793 := [monotonicity #2792]: #2762
-#2794 := (not #2762)
-#2795 := (or #2794 #2765)
-#2796 := [th-lemma]: #2795
-#2797 := [unit-resolution #2796 #2793]: #2765
-#2286 := (or #2340 #850)
-#2288 := [def-axiom]: #2286
-#2798 := [unit-resolution #2288 #2766]: #850
-[th-lemma #2798 #2785 #2784 #2797]: false
-unsat