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

added HOL-Boogie

#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