src/HOL/Boogie/Examples/cert/Boogie_b_max.proof

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