src/HOL/Boogie/Examples/Boogie_Max.certs

regenerated SMT certificates

1a4173e577cb1c2445a5c7913a23b8824b6da092 2068 0
#2 := false
decl f16 :: (-> S11 Int Int)
decl ?v0!3 :: Int
#1162 := ?v0!3
decl f17 :: S11
#50 := f17
#1169 := (f16 f17 ?v0!3)
decl f19 :: Int
#70 := f19
#107 := (f16 f17 f19)
#2469 := (= #107 #1169)
#2481 := (not #2469)
#46 := 0::Int
#660 := -1::Int
#1329 := (* -1::Int #1169)
#2470 := (+ #107 #1329)
#2472 := (>= #2470 0::Int)
#2476 := (not #2472)
decl f26 :: Int
#114 := f26
#780 := (* -1::Int f26)
#2398 := (+ #107 #780)
#2399 := (<= #2398 0::Int)
#2364 := (= #107 f26)
decl f24 :: Int
#109 := f24
#2553 := (= f24 f26)
#115 := (= f26 f24)
decl f25 :: Int
#112 := f25
#129 := (f16 f17 f25)
#130 := (= #129 f26)
#59 := (:var 0 Int)
#63 := (f16 f17 #59)
#2189 := (pattern #63)
#781 := (+ #63 #780)
#782 := (<= #781 0::Int)
decl f27 :: Int
#118 := f27
#769 := (* -1::Int f27)
#770 := (+ #59 #769)
#768 := (>= #770 0::Int)
#649 := (>= #59 0::Int)
#1410 := (not #649)
#1584 := (or #1410 #768 #782)
#2223 := (forall (vars (?v0 Int)) (:pat #2189) #1584)
#2228 := (not #2223)
#2231 := (or #2228 #130)
#2234 := (not #2231)
#1330 := (+ f26 #1329)
#1331 := (>= #1330 0::Int)
#1307 := (* -1::Int ?v0!3)
#1308 := (+ f27 #1307)
#1309 := (<= #1308 0::Int)
#1163 := (>= ?v0!3 0::Int)
#1547 := (not #1163)
#1562 := (or #1547 #1309 #1331)
#1567 := (not #1562)
#2237 := (or #1567 #2234)
#2240 := (not #2237)
#121 := 2::Int
#760 := (>= f27 2::Int)
#1609 := (not #760)
#757 := (>= f25 0::Int)
#1608 := (not #757)
#801 := (+ f19 #769)
#800 := (= #801 -1::Int)
#804 := (not #800)
#54 := 1::Int
#679 := (>= f19 1::Int)
#813 := (not #679)
#379 := (not #115)
#113 := (= f25 f19)
#388 := (not #113)
#110 := (= f24 #107)
#406 := (not #110)
#818 := (* -1::Int #107)
decl f20 :: Int
#75 := f20
#819 := (+ f20 #818)
#817 := (>= #819 0::Int)
decl f18 :: Int
#68 := f18
#676 := (>= f18 0::Int)
#1539 := (not #676)
#2243 := (or #1539 #817 #406 #388 #379 #813 #804 #1608 #1609 #2240)
#2246 := (not #2243)
#147 := (= f26 f20)
#439 := (not #147)
#146 := (= f25 f18)
#448 := (not #146)
#816 := (not #817)
#2249 := (or #1539 #816 #448 #439 #813 #804 #1608 #1609 #2240)
#2252 := (not #2249)
#2255 := (or #2246 #2252)
#2258 := (not #2255)
#725 := (* -1::Int f19)
decl f14 :: Int
#47 := f14
#726 := (+ f14 #725)
#727 := (<= #726 0::Int)
#2261 := (or #1539 #813 #727 #2258)
#2264 := (not #2261)
decl ?v0!2 :: Int
#1107 := ?v0!2
#1115 := (f16 f17 ?v0!2)
#1260 := (* -1::Int #1115)
decl f22 :: Int
#84 := f22
#1261 := (+ f22 #1260)
#1262 := (>= #1261 0::Int)
#1109 := (* -1::Int ?v0!2)
#1110 := (+ f14 #1109)
#1111 := (<= #1110 0::Int)
#1108 := (>= ?v0!2 0::Int)
#1500 := (not #1108)
decl ?v0!1 :: Int
#1089 := ?v0!1
#1097 := (f16 f17 ?v0!1)
#1098 := (= #1097 f22)
#1091 := (* -1::Int ?v0!1)
#1092 := (+ f14 #1091)
#1093 := (<= #1092 0::Int)
#1090 := (>= ?v0!1 0::Int)
#1480 := (not #1090)
#1495 := (or #1480 #1093 #1098)
#1526 := (not #1495)
#1527 := (or #1526 #1500 #1111 #1262)
#1528 := (not #1527)
#90 := (= #63 f22)
#687 := (* -1::Int #59)
#688 := (+ f14 #687)
#689 := (<= #688 0::Int)
#1469 := (or #1410 #689 #90)
#1474 := (not #1469)
#2206 := (forall (vars (?v0 Int)) (:pat #2189) #1474)
#2211 := (or #2206 #1528)
#2214 := (not #2211)
decl f23 :: Int
#86 := f23
#87 := (= f23 f19)
#256 := (not #87)
#85 := (= f22 f20)
#265 := (not #85)
decl f21 :: Int
#82 := f21
#83 := (= f21 f18)
#274 := (not #83)
#730 := (not #727)
#2217 := (or #1539 #813 #730 #274 #265 #256 #2214)
#2220 := (not #2217)
#2267 := (or #2220 #2264)
#2270 := (not #2267)
#79 := (f16 f17 f18)
#80 := (= #79 f20)
#535 := (not #80)
#925 := (* -1::Int f20)
#926 := (+ #63 #925)
#927 := (<= #926 0::Int)
#915 := (+ #59 #725)
#914 := (>= #915 0::Int)
#1447 := (or #1410 #914 #927)
#2198 := (forall (vars (?v0 Int)) (:pat #2189) #1447)
#2203 := (not #2198)
decl f15 :: Int
#49 := f15
#51 := (f16 f17 0::Int)
#67 := (= #51 f15)
#568 := (not #67)
#2273 := (or #568 #1539 #813 #2203 #535 #2270)
#2276 := (not #2273)
#2279 := (or #568 #2276)
#2282 := (not #2279)
#663 := (* -1::Int #63)
#664 := (+ f15 #663)
#662 := (>= #664 0::Int)
#652 := (>= #59 1::Int)
#1425 := (or #1410 #652 #662)
#2190 := (forall (vars (?v0 Int)) (:pat #2189) #1425)
#2195 := (not #2190)
#2285 := (or #2195 #2282)
#2288 := (not #2285)
decl ?v0!0 :: Int
#1037 := ?v0!0
#1016 := (f16 f17 ?v0!0)
#1017 := (* -1::Int #1016)
#1039 := (+ f15 #1017)
#1040 := (>= #1039 0::Int)
#1014 := (>= ?v0!0 1::Int)
#1038 := (>= ?v0!0 0::Int)
#1123 := (not #1038)
#1402 := (or #1123 #1014 #1040)
#1981 := (= f15 #1016)
#1942 := (= #51 #1016)
#1984 := (= #1016 #51)
#1975 := (= ?v0!0 0::Int)
#1015 := (not #1014)
#1407 := (not #1402)
#1974 := [hypothesis]: #1407
#1741 := (or #1402 #1015)
#1826 := [def-axiom]: #1741
#1971 := [unit-resolution #1826 #1974]: #1015
#1740 := (or #1402 #1038)
#1825 := [def-axiom]: #1740
#1973 := [unit-resolution #1825 #1974]: #1038
#1982 := [th-lemma arith eq-propagate 0 0 #1973 #1971]: #1975
#1985 := [monotonicity #1982]: #1984
#1943 := [symm #1985]: #1942
#52 := (= f15 #51)
#771 := (not #768)
#774 := (and #649 #771)
#777 := (not #774)
#785 := (or #777 #782)
#788 := (forall (vars (?v0 Int)) #785)
#791 := (not #788)
#794 := (or #791 #130)
#797 := (and #788 #794)
#762 := (and #757 #760)
#765 := (not #762)
#807 := (and #757 #679)
#810 := (not #807)
#681 := (and #676 #679)
#684 := (not #681)
#880 := (or #684 #816 #448 #439 #810 #804 #765 #797)
#856 := (or #684 #817 #406 #813 #388 #379 #810 #804 #765 #797)
#885 := (and #856 #880)
#906 := (or #684 #727 #885)
#708 := (* -1::Int f22)
#709 := (+ #63 #708)
#710 := (<= #709 0::Int)
#690 := (not #689)
#693 := (and #649 #690)
#696 := (not #693)
#713 := (or #696 #710)
#716 := (forall (vars (?v0 Int)) #713)
#699 := (or #696 #90)
#702 := (exists (vars (?v0 Int)) #699)
#705 := (not #702)
#719 := (or #705 #716)
#722 := (and #702 #719)
#751 := (or #684 #730 #274 #265 #256 #722)
#911 := (and #751 #906)
#916 := (not #914)
#919 := (and #649 #916)
#922 := (not #919)
#930 := (or #922 #927)
#933 := (forall (vars (?v0 Int)) #930)
#936 := (not #933)
#954 := (or #568 #684 #936 #535 #911)
#959 := (and #67 #954)
#650 := (not #652)
#654 := (and #649 #650)
#657 := (not #654)
#666 := (or #657 #662)
#669 := (forall (vars (?v0 Int)) #666)
#672 := (not #669)
#962 := (or #672 #959)
#965 := (and #669 #962)
#601 := (not #52)
#968 := (<= f14 0::Int)
#988 := (or #968 #601 #965)
#993 := (not #988)
#1 := true
#131 := (and #130 true)
#126 := (<= #63 f26)
#124 := (< #59 f27)
#60 := (<= 0::Int #59)
#125 := (and #60 #124)
#127 := (implies #125 #126)
#128 := (forall (vars (?v0 Int)) #127)
#132 := (implies #128 #131)
#133 := (and #128 #132)
#122 := (<= 2::Int f27)
#116 := (<= 0::Int f25)
#123 := (and #116 #122)
#134 := (implies #123 #133)
#119 := (+ f19 1::Int)
#120 := (= f27 #119)
#135 := (implies #120 #134)
#71 := (<= 1::Int f19)
#117 := (and #116 #71)
#136 := (implies #117 #135)
#137 := (implies true #136)
#148 := (implies #147 #137)
#149 := (implies #146 #148)
#69 := (<= 0::Int f18)
#72 := (and #69 #71)
#150 := (implies #72 #149)
#145 := (<= #107 f20)
#151 := (implies #145 #150)
#152 := (implies #72 #151)
#153 := (implies true #152)
#138 := (implies #115 #137)
#139 := (implies #113 #138)
#111 := (and #71 #71)
#140 := (implies #111 #139)
#141 := (implies #110 #140)
#108 := (< f20 #107)
#142 := (implies #108 #141)
#143 := (implies #72 #142)
#144 := (implies true #143)
#154 := (and #144 #153)
#155 := (implies #72 #154)
#106 := (< f19 f14)
#156 := (implies #106 #155)
#157 := (implies #72 #156)
#158 := (implies true #157)
#93 := (<= #63 f22)
#88 := (< #59 f14)
#89 := (and #60 #88)
#94 := (implies #89 #93)
#95 := (forall (vars (?v0 Int)) #94)
#96 := (and #95 true)
#91 := (implies #89 #90)
#92 := (exists (vars (?v0 Int)) #91)
#97 := (implies #92 #96)
#98 := (and #92 #97)
#99 := (implies #87 #98)
#100 := (implies #85 #99)
#101 := (implies #83 #100)
#102 := (implies #72 #101)
#81 := (<= f14 f19)
#103 := (implies #81 #102)
#104 := (implies #72 #103)
#105 := (implies true #104)
#159 := (and #105 #158)
#160 := (implies #72 #159)
#161 := (implies #80 #160)
#76 := (<= #63 f20)
#73 := (< #59 f19)
#74 := (and #60 #73)
#77 := (implies #74 #76)
#78 := (forall (vars (?v0 Int)) #77)
#162 := (implies #78 #161)
#163 := (implies #72 #162)
#164 := (implies true #163)
#165 := (implies #67 #164)
#166 := (and #67 #165)
#64 := (<= #63 f15)
#61 := (< #59 1::Int)
#62 := (and #60 #61)
#65 := (implies #62 #64)
#66 := (forall (vars (?v0 Int)) #65)
#167 := (implies #66 #166)
#168 := (and #66 #167)
#55 := (<= 1::Int 1::Int)
#56 := (and #55 #55)
#53 := (<= 0::Int 0::Int)
#57 := (and #53 #56)
#58 := (and #53 #57)
#169 := (implies #58 #168)
#170 := (implies #52 #169)
#48 := (< 0::Int f14)
#171 := (implies #48 #170)
#172 := (implies true #171)
#173 := (not #172)
#996 := (iff #173 #993)
#321 := (not #125)
#322 := (or #321 #126)
#325 := (forall (vars (?v0 Int)) #322)
#333 := (not #325)
#334 := (or #333 #130)
#339 := (and #325 #334)
#345 := (not #123)
#346 := (or #345 #339)
#315 := (+ 1::Int f19)
#318 := (= f27 #315)
#354 := (not #318)
#355 := (or #354 #346)
#363 := (not #117)
#364 := (or #363 #355)
#440 := (or #439 #364)
#449 := (or #448 #440)
#283 := (not #72)
#457 := (or #283 #449)
#465 := (not #145)
#466 := (or #465 #457)
#474 := (or #283 #466)
#380 := (or #379 #364)
#389 := (or #388 #380)
#397 := (not #71)
#398 := (or #397 #389)
#407 := (or #406 #398)
#415 := (not #108)
#416 := (or #415 #407)
#424 := (or #283 #416)
#486 := (and #424 #474)
#492 := (or #283 #486)
#500 := (not #106)
#501 := (or #500 #492)
#509 := (or #283 #501)
#221 := (not #89)
#228 := (or #221 #93)
#231 := (forall (vars (?v0 Int)) #228)
#222 := (or #221 #90)
#225 := (exists (vars (?v0 Int)) #222)
#244 := (not #225)
#245 := (or #244 #231)
#250 := (and #225 #245)
#257 := (or #256 #250)
#266 := (or #265 #257)
#275 := (or #274 #266)
#284 := (or #283 #275)
#292 := (not #81)
#293 := (or #292 #284)
#301 := (or #283 #293)
#521 := (and #301 #509)
#527 := (or #283 #521)
#536 := (or #535 #527)
#214 := (not #74)
#215 := (or #214 #76)
#218 := (forall (vars (?v0 Int)) #215)
#544 := (not #218)
#545 := (or #544 #536)
#553 := (or #283 #545)
#569 := (or #568 #553)
#574 := (and #67 #569)
#207 := (not #62)
#208 := (or #207 #64)
#211 := (forall (vars (?v0 Int)) #208)
#580 := (not #211)
#581 := (or #580 #574)
#586 := (and #211 #581)
#201 := (and #53 #55)
#204 := (and #53 #201)
#592 := (not #204)
#593 := (or #592 #586)
#602 := (or #601 #593)
#610 := (not #48)
#611 := (or #610 #602)
#623 := (not #611)
#994 := (iff #623 #993)
#991 := (iff #611 #988)
#979 := (or false #965)
#982 := (or #601 #979)
#985 := (or #968 #982)
#989 := (iff #985 #988)
#990 := [rewrite]: #989
#986 := (iff #611 #985)
#983 := (iff #602 #982)
#980 := (iff #593 #979)
#966 := (iff #586 #965)
#963 := (iff #581 #962)
#960 := (iff #574 #959)
#957 := (iff #569 #954)
#939 := (or #684 #911)
#942 := (or #535 #939)
#945 := (or #936 #942)
#948 := (or #684 #945)
#951 := (or #568 #948)
#955 := (iff #951 #954)
#956 := [rewrite]: #955
#952 := (iff #569 #951)
#949 := (iff #553 #948)
#946 := (iff #545 #945)
#943 := (iff #536 #942)
#940 := (iff #527 #939)
#912 := (iff #521 #911)
#909 := (iff #509 #906)
#897 := (or #684 #885)
#900 := (or #727 #897)
#903 := (or #684 #900)
#907 := (iff #903 #906)
#908 := [rewrite]: #907
#904 := (iff #509 #903)
#901 := (iff #501 #900)
#898 := (iff #492 #897)
#886 := (iff #486 #885)
#883 := (iff #474 #880)
#829 := (or #765 #797)
#832 := (or #804 #829)
#835 := (or #810 #832)
#865 := (or #439 #835)
#868 := (or #448 #865)
#871 := (or #684 #868)
#874 := (or #816 #871)
#877 := (or #684 #874)
#881 := (iff #877 #880)
#882 := [rewrite]: #881
#878 := (iff #474 #877)
#875 := (iff #466 #874)
#872 := (iff #457 #871)
#869 := (iff #449 #868)
#866 := (iff #440 #865)
#836 := (iff #364 #835)
#833 := (iff #355 #832)
#830 := (iff #346 #829)
#798 := (iff #339 #797)
#795 := (iff #334 #794)
#792 := (iff #333 #791)
#789 := (iff #325 #788)
#786 := (iff #322 #785)
#783 := (iff #126 #782)
#784 := [rewrite]: #783
#778 := (iff #321 #777)
#775 := (iff #125 #774)
#772 := (iff #124 #771)
#773 := [rewrite]: #772
#647 := (iff #60 #649)
#648 := [rewrite]: #647
#776 := [monotonicity #648 #773]: #775
#779 := [monotonicity #776]: #778
#787 := [monotonicity #779 #784]: #786
#790 := [quant-intro #787]: #789
#793 := [monotonicity #790]: #792
#796 := [monotonicity #793]: #795
#799 := [monotonicity #790 #796]: #798
#766 := (iff #345 #765)
#763 := (iff #123 #762)
#759 := (iff #122 #760)
#761 := [rewrite]: #759
#756 := (iff #116 #757)
#758 := [rewrite]: #756
#764 := [monotonicity #758 #761]: #763
#767 := [monotonicity #764]: #766
#831 := [monotonicity #767 #799]: #830
#805 := (iff #354 #804)
#802 := (iff #318 #800)
#803 := [rewrite]: #802
#806 := [monotonicity #803]: #805
#834 := [monotonicity #806 #831]: #833
#811 := (iff #363 #810)
#808 := (iff #117 #807)
#678 := (iff #71 #679)
#680 := [rewrite]: #678
#809 := [monotonicity #758 #680]: #808
#812 := [monotonicity #809]: #811
#837 := [monotonicity #812 #834]: #836
#867 := [monotonicity #837]: #866
#870 := [monotonicity #867]: #869
#685 := (iff #283 #684)
#682 := (iff #72 #681)
#675 := (iff #69 #676)
#677 := [rewrite]: #675
#683 := [monotonicity #677 #680]: #682
#686 := [monotonicity #683]: #685
#873 := [monotonicity #686 #870]: #872
#863 := (iff #465 #816)
#861 := (iff #145 #817)
#862 := [rewrite]: #861
#864 := [monotonicity #862]: #863
#876 := [monotonicity #864 #873]: #875
#879 := [monotonicity #686 #876]: #878
#884 := [trans #879 #882]: #883
#859 := (iff #424 #856)
#838 := (or #379 #835)
#841 := (or #388 #838)
#844 := (or #813 #841)
#847 := (or #406 #844)
#850 := (or #817 #847)
#853 := (or #684 #850)
#857 := (iff #853 #856)
#858 := [rewrite]: #857
#854 := (iff #424 #853)
#851 := (iff #416 #850)
#848 := (iff #407 #847)
#845 := (iff #398 #844)
#842 := (iff #389 #841)
#839 := (iff #380 #838)
#840 := [monotonicity #837]: #839
#843 := [monotonicity #840]: #842
#814 := (iff #397 #813)
#815 := [monotonicity #680]: #814
#846 := [monotonicity #815 #843]: #845
#849 := [monotonicity #846]: #848
#827 := (iff #415 #817)
#822 := (not #816)
#825 := (iff #822 #817)
#826 := [rewrite]: #825
#823 := (iff #415 #822)
#820 := (iff #108 #816)
#821 := [rewrite]: #820
#824 := [monotonicity #821]: #823
#828 := [trans #824 #826]: #827
#852 := [monotonicity #828 #849]: #851
#855 := [monotonicity #686 #852]: #854
#860 := [trans #855 #858]: #859
#887 := [monotonicity #860 #884]: #886
#899 := [monotonicity #686 #887]: #898
#895 := (iff #500 #727)
#890 := (not #730)
#893 := (iff #890 #727)
#894 := [rewrite]: #893
#891 := (iff #500 #890)
#888 := (iff #106 #730)
#889 := [rewrite]: #888
#892 := [monotonicity #889]: #891
#896 := [trans #892 #894]: #895
#902 := [monotonicity #896 #899]: #901
#905 := [monotonicity #686 #902]: #904
#910 := [trans #905 #908]: #909
#754 := (iff #301 #751)
#733 := (or #256 #722)
#736 := (or #265 #733)
#739 := (or #274 #736)
#742 := (or #684 #739)
#745 := (or #730 #742)
#748 := (or #684 #745)
#752 := (iff #748 #751)
#753 := [rewrite]: #752
#749 := (iff #301 #748)
#746 := (iff #293 #745)
#743 := (iff #284 #742)
#740 := (iff #275 #739)
#737 := (iff #266 #736)
#734 := (iff #257 #733)
#723 := (iff #250 #722)
#720 := (iff #245 #719)
#717 := (iff #231 #716)
#714 := (iff #228 #713)
#711 := (iff #93 #710)
#712 := [rewrite]: #711
#697 := (iff #221 #696)
#694 := (iff #89 #693)
#691 := (iff #88 #690)
#692 := [rewrite]: #691
#695 := [monotonicity #648 #692]: #694
#698 := [monotonicity #695]: #697
#715 := [monotonicity #698 #712]: #714
#718 := [quant-intro #715]: #717
#706 := (iff #244 #705)
#703 := (iff #225 #702)
#700 := (iff #222 #699)
#701 := [monotonicity #698]: #700
#704 := [quant-intro #701]: #703
#707 := [monotonicity #704]: #706
#721 := [monotonicity #707 #718]: #720
#724 := [monotonicity #704 #721]: #723
#735 := [monotonicity #724]: #734
#738 := [monotonicity #735]: #737
#741 := [monotonicity #738]: #740
#744 := [monotonicity #686 #741]: #743
#731 := (iff #292 #730)
#728 := (iff #81 #727)
#729 := [rewrite]: #728
#732 := [monotonicity #729]: #731
#747 := [monotonicity #732 #744]: #746
#750 := [monotonicity #686 #747]: #749
#755 := [trans #750 #753]: #754
#913 := [monotonicity #755 #910]: #912
#941 := [monotonicity #686 #913]: #940
#944 := [monotonicity #941]: #943
#937 := (iff #544 #936)
#934 := (iff #218 #933)
#931 := (iff #215 #930)
#928 := (iff #76 #927)
#929 := [rewrite]: #928
#923 := (iff #214 #922)
#920 := (iff #74 #919)
#917 := (iff #73 #916)
#918 := [rewrite]: #917
#921 := [monotonicity #648 #918]: #920
#924 := [monotonicity #921]: #923
#932 := [monotonicity #924 #929]: #931
#935 := [quant-intro #932]: #934
#938 := [monotonicity #935]: #937
#947 := [monotonicity #938 #944]: #946
#950 := [monotonicity #686 #947]: #949
#953 := [monotonicity #950]: #952
#958 := [trans #953 #956]: #957
#961 := [monotonicity #958]: #960
#673 := (iff #580 #672)
#670 := (iff #211 #669)
#667 := (iff #208 #666)
#661 := (iff #64 #662)
#665 := [rewrite]: #661
#658 := (iff #207 #657)
#655 := (iff #62 #654)
#651 := (iff #61 #650)
#653 := [rewrite]: #651
#656 := [monotonicity #648 #653]: #655
#659 := [monotonicity #656]: #658
#668 := [monotonicity #659 #665]: #667
#671 := [quant-intro #668]: #670
#674 := [monotonicity #671]: #673
#964 := [monotonicity #674 #961]: #963
#967 := [monotonicity #671 #964]: #966
#645 := (iff #592 false)
#640 := (not true)
#643 := (iff #640 false)
#644 := [rewrite]: #643
#641 := (iff #592 #640)
#638 := (iff #204 true)
#630 := (and true true)
#633 := (and true #630)
#636 := (iff #633 true)
#637 := [rewrite]: #636
#634 := (iff #204 #633)
#631 := (iff #201 #630)
#628 := (iff #55 true)
#629 := [rewrite]: #628
#626 := (iff #53 true)
#627 := [rewrite]: #626
#632 := [monotonicity #627 #629]: #631
#635 := [monotonicity #627 #632]: #634
#639 := [trans #635 #637]: #638
#642 := [monotonicity #639]: #641
#646 := [trans #642 #644]: #645
#981 := [monotonicity #646 #967]: #980
#984 := [monotonicity #981]: #983
#977 := (iff #610 #968)
#969 := (not #968)
#972 := (not #969)
#975 := (iff #972 #968)
#976 := [rewrite]: #975
#973 := (iff #610 #972)
#970 := (iff #48 #969)
#971 := [rewrite]: #970
#974 := [monotonicity #971]: #973
#978 := [trans #974 #976]: #977
#987 := [monotonicity #978 #984]: #986
#992 := [trans #987 #990]: #991
#995 := [monotonicity #992]: #994
#624 := (iff #173 #623)
#621 := (iff #172 #611)
#616 := (implies true #611)
#619 := (iff #616 #611)
#620 := [rewrite]: #619
#617 := (iff #172 #616)
#614 := (iff #171 #611)
#607 := (implies #48 #602)
#612 := (iff #607 #611)
#613 := [rewrite]: #612
#608 := (iff #171 #607)
#605 := (iff #170 #602)
#598 := (implies #52 #593)
#603 := (iff #598 #602)
#604 := [rewrite]: #603
#599 := (iff #170 #598)
#596 := (iff #169 #593)
#589 := (implies #204 #586)
#594 := (iff #589 #593)
#595 := [rewrite]: #594
#590 := (iff #169 #589)
#587 := (iff #168 #586)
#584 := (iff #167 #581)
#577 := (implies #211 #574)
#582 := (iff #577 #581)
#583 := [rewrite]: #582
#578 := (iff #167 #577)
#575 := (iff #166 #574)
#572 := (iff #165 #569)
#565 := (implies #67 #553)
#570 := (iff #565 #569)
#571 := [rewrite]: #570
#566 := (iff #165 #565)
#563 := (iff #164 #553)
#558 := (implies true #553)
#561 := (iff #558 #553)
#562 := [rewrite]: #561
#559 := (iff #164 #558)
#556 := (iff #163 #553)
#550 := (implies #72 #545)
#554 := (iff #550 #553)
#555 := [rewrite]: #554
#551 := (iff #163 #550)
#548 := (iff #162 #545)
#541 := (implies #218 #536)
#546 := (iff #541 #545)
#547 := [rewrite]: #546
#542 := (iff #162 #541)
#539 := (iff #161 #536)
#532 := (implies #80 #527)
#537 := (iff #532 #536)
#538 := [rewrite]: #537
#533 := (iff #161 #532)
#530 := (iff #160 #527)
#524 := (implies #72 #521)
#528 := (iff #524 #527)
#529 := [rewrite]: #528
#525 := (iff #160 #524)
#522 := (iff #159 #521)
#519 := (iff #158 #509)
#514 := (implies true #509)
#517 := (iff #514 #509)
#518 := [rewrite]: #517
#515 := (iff #158 #514)
#512 := (iff #157 #509)
#506 := (implies #72 #501)
#510 := (iff #506 #509)
#511 := [rewrite]: #510
#507 := (iff #157 #506)
#504 := (iff #156 #501)
#497 := (implies #106 #492)
#502 := (iff #497 #501)
#503 := [rewrite]: #502
#498 := (iff #156 #497)
#495 := (iff #155 #492)
#489 := (implies #72 #486)
#493 := (iff #489 #492)
#494 := [rewrite]: #493
#490 := (iff #155 #489)
#487 := (iff #154 #486)
#484 := (iff #153 #474)
#479 := (implies true #474)
#482 := (iff #479 #474)
#483 := [rewrite]: #482
#480 := (iff #153 #479)
#477 := (iff #152 #474)
#471 := (implies #72 #466)
#475 := (iff #471 #474)
#476 := [rewrite]: #475
#472 := (iff #152 #471)
#469 := (iff #151 #466)
#462 := (implies #145 #457)
#467 := (iff #462 #466)
#468 := [rewrite]: #467
#463 := (iff #151 #462)
#460 := (iff #150 #457)
#454 := (implies #72 #449)
#458 := (iff #454 #457)
#459 := [rewrite]: #458
#455 := (iff #150 #454)
#452 := (iff #149 #449)
#445 := (implies #146 #440)
#450 := (iff #445 #449)
#451 := [rewrite]: #450
#446 := (iff #149 #445)
#443 := (iff #148 #440)
#436 := (implies #147 #364)
#441 := (iff #436 #440)
#442 := [rewrite]: #441
#437 := (iff #148 #436)
#374 := (iff #137 #364)
#369 := (implies true #364)
#372 := (iff #369 #364)
#373 := [rewrite]: #372
#370 := (iff #137 #369)
#367 := (iff #136 #364)
#360 := (implies #117 #355)
#365 := (iff #360 #364)
#366 := [rewrite]: #365
#361 := (iff #136 #360)
#358 := (iff #135 #355)
#351 := (implies #318 #346)
#356 := (iff #351 #355)
#357 := [rewrite]: #356
#352 := (iff #135 #351)
#349 := (iff #134 #346)
#342 := (implies #123 #339)
#347 := (iff #342 #346)
#348 := [rewrite]: #347
#343 := (iff #134 #342)
#340 := (iff #133 #339)
#337 := (iff #132 #334)
#330 := (implies #325 #130)
#335 := (iff #330 #334)
#336 := [rewrite]: #335
#331 := (iff #132 #330)
#328 := (iff #131 #130)
#329 := [rewrite]: #328
#326 := (iff #128 #325)
#323 := (iff #127 #322)
#324 := [rewrite]: #323
#327 := [quant-intro #324]: #326
#332 := [monotonicity #327 #329]: #331
#338 := [trans #332 #336]: #337
#341 := [monotonicity #327 #338]: #340
#344 := [monotonicity #341]: #343
#350 := [trans #344 #348]: #349
#319 := (iff #120 #318)
#316 := (= #119 #315)
#317 := [rewrite]: #316
#320 := [monotonicity #317]: #319
#353 := [monotonicity #320 #350]: #352
#359 := [trans #353 #357]: #358
#362 := [monotonicity #359]: #361
#368 := [trans #362 #366]: #367
#371 := [monotonicity #368]: #370
#375 := [trans #371 #373]: #374
#438 := [monotonicity #375]: #437
#444 := [trans #438 #442]: #443
#447 := [monotonicity #444]: #446
#453 := [trans #447 #451]: #452
#456 := [monotonicity #453]: #455
#461 := [trans #456 #459]: #460
#464 := [monotonicity #461]: #463
#470 := [trans #464 #468]: #469
#473 := [monotonicity #470]: #472
#478 := [trans #473 #476]: #477
#481 := [monotonicity #478]: #480
#485 := [trans #481 #483]: #484
#434 := (iff #144 #424)
#429 := (implies true #424)
#432 := (iff #429 #424)
#433 := [rewrite]: #432
#430 := (iff #144 #429)
#427 := (iff #143 #424)
#421 := (implies #72 #416)
#425 := (iff #421 #424)
#426 := [rewrite]: #425
#422 := (iff #143 #421)
#419 := (iff #142 #416)
#412 := (implies #108 #407)
#417 := (iff #412 #416)
#418 := [rewrite]: #417
#413 := (iff #142 #412)
#410 := (iff #141 #407)
#403 := (implies #110 #398)
#408 := (iff #403 #407)
#409 := [rewrite]: #408
#404 := (iff #141 #403)
#401 := (iff #140 #398)
#394 := (implies #71 #389)
#399 := (iff #394 #398)
#400 := [rewrite]: #399
#395 := (iff #140 #394)
#392 := (iff #139 #389)
#385 := (implies #113 #380)
#390 := (iff #385 #389)
#391 := [rewrite]: #390
#386 := (iff #139 #385)
#383 := (iff #138 #380)
#376 := (implies #115 #364)
#381 := (iff #376 #380)
#382 := [rewrite]: #381
#377 := (iff #138 #376)
#378 := [monotonicity #375]: #377
#384 := [trans #378 #382]: #383
#387 := [monotonicity #384]: #386
#393 := [trans #387 #391]: #392
#313 := (iff #111 #71)
#314 := [rewrite]: #313
#396 := [monotonicity #314 #393]: #395
#402 := [trans #396 #400]: #401
#405 := [monotonicity #402]: #404
#411 := [trans #405 #409]: #410
#414 := [monotonicity #411]: #413
#420 := [trans #414 #418]: #419
#423 := [monotonicity #420]: #422
#428 := [trans #423 #426]: #427
#431 := [monotonicity #428]: #430
#435 := [trans #431 #433]: #434
#488 := [monotonicity #435 #485]: #487
#491 := [monotonicity #488]: #490
#496 := [trans #491 #494]: #495
#499 := [monotonicity #496]: #498
#505 := [trans #499 #503]: #504
#508 := [monotonicity #505]: #507
#513 := [trans #508 #511]: #512
#516 := [monotonicity #513]: #515
#520 := [trans #516 #518]: #519
#311 := (iff #105 #301)
#306 := (implies true #301)
#309 := (iff #306 #301)
#310 := [rewrite]: #309
#307 := (iff #105 #306)
#304 := (iff #104 #301)
#298 := (implies #72 #293)
#302 := (iff #298 #301)
#303 := [rewrite]: #302
#299 := (iff #104 #298)
#296 := (iff #103 #293)
#289 := (implies #81 #284)
#294 := (iff #289 #293)
#295 := [rewrite]: #294
#290 := (iff #103 #289)
#287 := (iff #102 #284)
#280 := (implies #72 #275)
#285 := (iff #280 #284)
#286 := [rewrite]: #285
#281 := (iff #102 #280)
#278 := (iff #101 #275)
#271 := (implies #83 #266)
#276 := (iff #271 #275)
#277 := [rewrite]: #276
#272 := (iff #101 #271)
#269 := (iff #100 #266)
#262 := (implies #85 #257)
#267 := (iff #262 #266)
#268 := [rewrite]: #267
#263 := (iff #100 #262)
#260 := (iff #99 #257)
#253 := (implies #87 #250)
#258 := (iff #253 #257)
#259 := [rewrite]: #258
#254 := (iff #99 #253)
#251 := (iff #98 #250)
#248 := (iff #97 #245)
#241 := (implies #225 #231)
#246 := (iff #241 #245)
#247 := [rewrite]: #246
#242 := (iff #97 #241)
#239 := (iff #96 #231)
#234 := (and #231 true)
#237 := (iff #234 #231)
#238 := [rewrite]: #237
#235 := (iff #96 #234)
#232 := (iff #95 #231)
#229 := (iff #94 #228)
#230 := [rewrite]: #229
#233 := [quant-intro #230]: #232
#236 := [monotonicity #233]: #235
#240 := [trans #236 #238]: #239
#226 := (iff #92 #225)
#223 := (iff #91 #222)
#224 := [rewrite]: #223
#227 := [quant-intro #224]: #226
#243 := [monotonicity #227 #240]: #242
#249 := [trans #243 #247]: #248
#252 := [monotonicity #227 #249]: #251
#255 := [monotonicity #252]: #254
#261 := [trans #255 #259]: #260
#264 := [monotonicity #261]: #263
#270 := [trans #264 #268]: #269
#273 := [monotonicity #270]: #272
#279 := [trans #273 #277]: #278
#282 := [monotonicity #279]: #281
#288 := [trans #282 #286]: #287
#291 := [monotonicity #288]: #290
#297 := [trans #291 #295]: #296
#300 := [monotonicity #297]: #299
#305 := [trans #300 #303]: #304
#308 := [monotonicity #305]: #307
#312 := [trans #308 #310]: #311
#523 := [monotonicity #312 #520]: #522
#526 := [monotonicity #523]: #525
#531 := [trans #526 #529]: #530
#534 := [monotonicity #531]: #533
#540 := [trans #534 #538]: #539
#219 := (iff #78 #218)
#216 := (iff #77 #215)
#217 := [rewrite]: #216
#220 := [quant-intro #217]: #219
#543 := [monotonicity #220 #540]: #542
#549 := [trans #543 #547]: #548
#552 := [monotonicity #549]: #551
#557 := [trans #552 #555]: #556
#560 := [monotonicity #557]: #559
#564 := [trans #560 #562]: #563
#567 := [monotonicity #564]: #566
#573 := [trans #567 #571]: #572
#576 := [monotonicity #573]: #575
#212 := (iff #66 #211)
#209 := (iff #65 #208)
#210 := [rewrite]: #209
#213 := [quant-intro #210]: #212
#579 := [monotonicity #213 #576]: #578
#585 := [trans #579 #583]: #584
#588 := [monotonicity #213 #585]: #587
#205 := (iff #58 #204)
#202 := (iff #57 #201)
#199 := (iff #56 #55)
#200 := [rewrite]: #199
#203 := [monotonicity #200]: #202
#206 := [monotonicity #203]: #205
#591 := [monotonicity #206 #588]: #590
#597 := [trans #591 #595]: #596
#600 := [monotonicity #597]: #599
#606 := [trans #600 #604]: #605
#609 := [monotonicity #606]: #608
#615 := [trans #609 #613]: #614
#618 := [monotonicity #615]: #617
#622 := [trans #618 #620]: #621
#625 := [monotonicity #622]: #624
#997 := [trans #625 #995]: #996
#198 := [asserted]: #173
#998 := [mp #198 #997]: #993
#1000 := [not-or-elim #998]: #52
#1945 := [trans #1000 #1943]: #1981
#1827 := (not #1040)
#1818 := (or #1402 #1827)
#1829 := [def-axiom]: #1818
#1946 := [unit-resolution #1829 #1974]: #1827
#1947 := (not #1981)
#1941 := (or #1947 #1040)
#1948 := [th-lemma arith triangle-eq]: #1941
#1949 := [unit-resolution #1948 #1946 #1945]: false
#1950 := [lemma #1949]: #1402
#2291 := (or #1407 #2288)
#1589 := (forall (vars (?v0 Int)) #1584)
#1595 := (not #1589)
#1596 := (or #1595 #130)
#1597 := (not #1596)
#1602 := (or #1567 #1597)
#1610 := (not #1602)
#1620 := (or #1539 #816 #448 #439 #813 #804 #1608 #1609 #1610)
#1621 := (not #1620)
#1611 := (or #1539 #817 #406 #388 #379 #813 #804 #1608 #1609 #1610)
#1612 := (not #1611)
#1626 := (or #1612 #1621)
#1632 := (not #1626)
#1633 := (or #1539 #813 #727 #1632)
#1634 := (not #1633)
#1477 := (forall (vars (?v0 Int)) #1474)
#1533 := (or #1477 #1528)
#1540 := (not #1533)
#1541 := (or #1539 #813 #730 #274 #265 #256 #1540)
#1542 := (not #1541)
#1639 := (or #1542 #1634)
#1646 := (not #1639)
#1452 := (forall (vars (?v0 Int)) #1447)
#1645 := (not #1452)
#1647 := (or #568 #1539 #813 #1645 #535 #1646)
#1648 := (not #1647)
#1653 := (or #568 #1648)
#1660 := (not #1653)
#1430 := (forall (vars (?v0 Int)) #1425)
#1659 := (not #1430)
#1661 := (or #1659 #1660)
#1662 := (not #1661)
#1667 := (or #1407 #1662)
#2292 := (iff #1667 #2291)
#2289 := (iff #1662 #2288)
#2286 := (iff #1661 #2285)
#2283 := (iff #1660 #2282)
#2280 := (iff #1653 #2279)
#2277 := (iff #1648 #2276)
#2274 := (iff #1647 #2273)
#2271 := (iff #1646 #2270)
#2268 := (iff #1639 #2267)
#2265 := (iff #1634 #2264)
#2262 := (iff #1633 #2261)
#2259 := (iff #1632 #2258)
#2256 := (iff #1626 #2255)
#2253 := (iff #1621 #2252)
#2250 := (iff #1620 #2249)
#2241 := (iff #1610 #2240)
#2238 := (iff #1602 #2237)
#2235 := (iff #1597 #2234)
#2232 := (iff #1596 #2231)
#2229 := (iff #1595 #2228)
#2226 := (iff #1589 #2223)
#2224 := (iff #1584 #1584)
#2225 := [refl]: #2224
#2227 := [quant-intro #2225]: #2226
#2230 := [monotonicity #2227]: #2229
#2233 := [monotonicity #2230]: #2232
#2236 := [monotonicity #2233]: #2235
#2239 := [monotonicity #2236]: #2238
#2242 := [monotonicity #2239]: #2241
#2251 := [monotonicity #2242]: #2250
#2254 := [monotonicity #2251]: #2253
#2247 := (iff #1612 #2246)
#2244 := (iff #1611 #2243)
#2245 := [monotonicity #2242]: #2244
#2248 := [monotonicity #2245]: #2247
#2257 := [monotonicity #2248 #2254]: #2256
#2260 := [monotonicity #2257]: #2259
#2263 := [monotonicity #2260]: #2262
#2266 := [monotonicity #2263]: #2265
#2221 := (iff #1542 #2220)
#2218 := (iff #1541 #2217)
#2215 := (iff #1540 #2214)
#2212 := (iff #1533 #2211)
#2209 := (iff #1477 #2206)
#2207 := (iff #1474 #1474)
#2208 := [refl]: #2207
#2210 := [quant-intro #2208]: #2209
#2213 := [monotonicity #2210]: #2212
#2216 := [monotonicity #2213]: #2215
#2219 := [monotonicity #2216]: #2218
#2222 := [monotonicity #2219]: #2221
#2269 := [monotonicity #2222 #2266]: #2268
#2272 := [monotonicity #2269]: #2271
#2204 := (iff #1645 #2203)
#2201 := (iff #1452 #2198)
#2199 := (iff #1447 #1447)
#2200 := [refl]: #2199
#2202 := [quant-intro #2200]: #2201
#2205 := [monotonicity #2202]: #2204
#2275 := [monotonicity #2205 #2272]: #2274
#2278 := [monotonicity #2275]: #2277
#2281 := [monotonicity #2278]: #2280
#2284 := [monotonicity #2281]: #2283
#2196 := (iff #1659 #2195)
#2193 := (iff #1430 #2190)
#2191 := (iff #1425 #1425)
#2192 := [refl]: #2191
#2194 := [quant-intro #2192]: #2193
#2197 := [monotonicity #2194]: #2196
#2287 := [monotonicity #2197 #2284]: #2286
#2290 := [monotonicity #2287]: #2289
#2293 := [monotonicity #2290]: #2292
#1185 := (not #130)
#1188 := (and #788 #1185)
#1314 := (not #1309)
#1317 := (and #1163 #1314)
#1320 := (not #1317)
#1336 := (or #1320 #1331)
#1339 := (not #1336)
#1342 := (or #1339 #1188)
#1360 := (and #676 #817 #146 #147 #679 #800 #757 #760 #1342)
#1348 := (and #676 #816 #110 #113 #115 #679 #800 #757 #760 #1342)
#1365 := (or #1348 #1360)
#1371 := (and #676 #679 #730 #1365)
#1112 := (not #1111)
#1113 := (and #1108 #1112)
#1114 := (not #1113)
#1267 := (or #1114 #1262)
#1270 := (not #1267)
#1094 := (not #1093)
#1095 := (and #1090 #1094)
#1096 := (not #1095)
#1099 := (or #1096 #1098)
#1273 := (and #1099 #1270)
#1083 := (not #699)
#1086 := (forall (vars (?v0 Int)) #1083)
#1276 := (or #1086 #1273)
#1282 := (and #676 #679 #727 #83 #85 #87 #1276)
#1376 := (or #1282 #1371)
#1382 := (and #67 #676 #679 #933 #80 #1376)
#1387 := (or #568 #1382)
#1390 := (and #669 #1387)
#1018 := (and #1038 #1015)
#1019 := (not #1018)
#1041 := (or #1019 #1040)
#1042 := (not #1041)
#1393 := (or #1042 #1390)
#1668 := (iff #1393 #1667)
#1665 := (iff #1390 #1662)
#1656 := (and #1430 #1653)
#1663 := (iff #1656 #1662)
#1664 := [rewrite]: #1663
#1657 := (iff #1390 #1656)
#1654 := (iff #1387 #1653)
#1651 := (iff #1382 #1648)
#1642 := (and #67 #676 #679 #1452 #80 #1639)
#1649 := (iff #1642 #1648)
#1650 := [rewrite]: #1649
#1643 := (iff #1382 #1642)
#1640 := (iff #1376 #1639)
#1637 := (iff #1371 #1634)
#1629 := (and #676 #679 #730 #1626)
#1635 := (iff #1629 #1634)
#1636 := [rewrite]: #1635
#1630 := (iff #1371 #1629)
#1627 := (iff #1365 #1626)
#1624 := (iff #1360 #1621)
#1617 := (and #676 #817 #146 #147 #679 #800 #757 #760 #1602)
#1622 := (iff #1617 #1621)
#1623 := [rewrite]: #1622
#1618 := (iff #1360 #1617)
#1603 := (iff #1342 #1602)
#1600 := (iff #1188 #1597)
#1592 := (and #1589 #1185)
#1598 := (iff #1592 #1597)
#1599 := [rewrite]: #1598
#1593 := (iff #1188 #1592)
#1590 := (iff #788 #1589)
#1587 := (iff #785 #1584)
#1570 := (or #1410 #768)
#1581 := (or #1570 #782)
#1585 := (iff #1581 #1584)
#1586 := [rewrite]: #1585
#1582 := (iff #785 #1581)
#1579 := (iff #777 #1570)
#1571 := (not #1570)
#1574 := (not #1571)
#1577 := (iff #1574 #1570)
#1578 := [rewrite]: #1577
#1575 := (iff #777 #1574)
#1572 := (iff #774 #1571)
#1573 := [rewrite]: #1572
#1576 := [monotonicity #1573]: #1575
#1580 := [trans #1576 #1578]: #1579
#1583 := [monotonicity #1580]: #1582
#1588 := [trans #1583 #1586]: #1587
#1591 := [quant-intro #1588]: #1590
#1594 := [monotonicity #1591]: #1593
#1601 := [trans #1594 #1599]: #1600
#1568 := (iff #1339 #1567)
#1565 := (iff #1336 #1562)
#1548 := (or #1547 #1309)
#1559 := (or #1548 #1331)
#1563 := (iff #1559 #1562)
#1564 := [rewrite]: #1563
#1560 := (iff #1336 #1559)
#1557 := (iff #1320 #1548)
#1549 := (not #1548)
#1552 := (not #1549)
#1555 := (iff #1552 #1548)
#1556 := [rewrite]: #1555
#1553 := (iff #1320 #1552)
#1550 := (iff #1317 #1549)
#1551 := [rewrite]: #1550
#1554 := [monotonicity #1551]: #1553
#1558 := [trans #1554 #1556]: #1557
#1561 := [monotonicity #1558]: #1560
#1566 := [trans #1561 #1564]: #1565
#1569 := [monotonicity #1566]: #1568
#1604 := [monotonicity #1569 #1601]: #1603
#1619 := [monotonicity #1604]: #1618
#1625 := [trans #1619 #1623]: #1624
#1615 := (iff #1348 #1612)
#1605 := (and #676 #816 #110 #113 #115 #679 #800 #757 #760 #1602)
#1613 := (iff #1605 #1612)
#1614 := [rewrite]: #1613
#1606 := (iff #1348 #1605)
#1607 := [monotonicity #1604]: #1606
#1616 := [trans #1607 #1614]: #1615
#1628 := [monotonicity #1616 #1625]: #1627
#1631 := [monotonicity #1628]: #1630
#1638 := [trans #1631 #1636]: #1637
#1545 := (iff #1282 #1542)
#1536 := (and #676 #679 #727 #83 #85 #87 #1533)
#1543 := (iff #1536 #1542)
#1544 := [rewrite]: #1543
#1537 := (iff #1282 #1536)
#1534 := (iff #1276 #1533)
#1531 := (iff #1273 #1528)
#1515 := (or #1500 #1111 #1262)
#1520 := (not #1515)
#1523 := (and #1495 #1520)
#1529 := (iff #1523 #1528)
#1530 := [rewrite]: #1529
#1524 := (iff #1273 #1523)
#1521 := (iff #1270 #1520)
#1518 := (iff #1267 #1515)
#1501 := (or #1500 #1111)
#1512 := (or #1501 #1262)
#1516 := (iff #1512 #1515)
#1517 := [rewrite]: #1516
#1513 := (iff #1267 #1512)
#1510 := (iff #1114 #1501)
#1502 := (not #1501)
#1505 := (not #1502)
#1508 := (iff #1505 #1501)
#1509 := [rewrite]: #1508
#1506 := (iff #1114 #1505)
#1503 := (iff #1113 #1502)
#1504 := [rewrite]: #1503
#1507 := [monotonicity #1504]: #1506
#1511 := [trans #1507 #1509]: #1510
#1514 := [monotonicity #1511]: #1513
#1519 := [trans #1514 #1517]: #1518
#1522 := [monotonicity #1519]: #1521
#1498 := (iff #1099 #1495)
#1481 := (or #1480 #1093)
#1492 := (or #1481 #1098)
#1496 := (iff #1492 #1495)
#1497 := [rewrite]: #1496
#1493 := (iff #1099 #1492)
#1490 := (iff #1096 #1481)
#1482 := (not #1481)
#1485 := (not #1482)
#1488 := (iff #1485 #1481)
#1489 := [rewrite]: #1488
#1486 := (iff #1096 #1485)
#1483 := (iff #1095 #1482)
#1484 := [rewrite]: #1483
#1487 := [monotonicity #1484]: #1486
#1491 := [trans #1487 #1489]: #1490
#1494 := [monotonicity #1491]: #1493
#1499 := [trans #1494 #1497]: #1498
#1525 := [monotonicity #1499 #1522]: #1524
#1532 := [trans #1525 #1530]: #1531
#1478 := (iff #1086 #1477)
#1475 := (iff #1083 #1474)
#1472 := (iff #699 #1469)
#1455 := (or #1410 #689)
#1466 := (or #1455 #90)
#1470 := (iff #1466 #1469)
#1471 := [rewrite]: #1470
#1467 := (iff #699 #1466)
#1464 := (iff #696 #1455)
#1456 := (not #1455)
#1459 := (not #1456)
#1462 := (iff #1459 #1455)
#1463 := [rewrite]: #1462
#1460 := (iff #696 #1459)
#1457 := (iff #693 #1456)
#1458 := [rewrite]: #1457
#1461 := [monotonicity #1458]: #1460
#1465 := [trans #1461 #1463]: #1464
#1468 := [monotonicity #1465]: #1467
#1473 := [trans #1468 #1471]: #1472
#1476 := [monotonicity #1473]: #1475
#1479 := [quant-intro #1476]: #1478
#1535 := [monotonicity #1479 #1532]: #1534
#1538 := [monotonicity #1535]: #1537
#1546 := [trans #1538 #1544]: #1545
#1641 := [monotonicity #1546 #1638]: #1640
#1453 := (iff #933 #1452)
#1450 := (iff #930 #1447)
#1433 := (or #1410 #914)
#1444 := (or #1433 #927)
#1448 := (iff #1444 #1447)
#1449 := [rewrite]: #1448
#1445 := (iff #930 #1444)
#1442 := (iff #922 #1433)
#1434 := (not #1433)
#1437 := (not #1434)
#1440 := (iff #1437 #1433)
#1441 := [rewrite]: #1440
#1438 := (iff #922 #1437)
#1435 := (iff #919 #1434)
#1436 := [rewrite]: #1435
#1439 := [monotonicity #1436]: #1438
#1443 := [trans #1439 #1441]: #1442
#1446 := [monotonicity #1443]: #1445
#1451 := [trans #1446 #1449]: #1450
#1454 := [quant-intro #1451]: #1453
#1644 := [monotonicity #1454 #1641]: #1643
#1652 := [trans #1644 #1650]: #1651
#1655 := [monotonicity #1652]: #1654
#1431 := (iff #669 #1430)
#1428 := (iff #666 #1425)
#1411 := (or #1410 #652)
#1422 := (or #1411 #662)
#1426 := (iff #1422 #1425)
#1427 := [rewrite]: #1426
#1423 := (iff #666 #1422)
#1420 := (iff #657 #1411)
#1412 := (not #1411)
#1415 := (not #1412)
#1418 := (iff #1415 #1411)
#1419 := [rewrite]: #1418
#1416 := (iff #657 #1415)
#1413 := (iff #654 #1412)
#1414 := [rewrite]: #1413
#1417 := [monotonicity #1414]: #1416
#1421 := [trans #1417 #1419]: #1420
#1424 := [monotonicity #1421]: #1423
#1429 := [trans #1424 #1427]: #1428
#1432 := [quant-intro #1429]: #1431
#1658 := [monotonicity #1432 #1655]: #1657
#1666 := [trans #1658 #1664]: #1665
#1408 := (iff #1042 #1407)
#1405 := (iff #1041 #1402)
#1124 := (or #1123 #1014)
#1399 := (or #1124 #1040)
#1403 := (iff #1399 #1402)
#1404 := [rewrite]: #1403
#1400 := (iff #1041 #1399)
#1397 := (iff #1019 #1124)
#1176 := (not #1124)
#1103 := (not #1176)
#1241 := (iff #1103 #1124)
#1396 := [rewrite]: #1241
#1045 := (iff #1019 #1103)
#1177 := (iff #1018 #1176)
#1102 := [rewrite]: #1177
#1046 := [monotonicity #1102]: #1045
#1398 := [trans #1046 #1396]: #1397
#1401 := [monotonicity #1398]: #1400
#1406 := [trans #1401 #1404]: #1405
#1409 := [monotonicity #1406]: #1408
#1669 := [monotonicity #1409 #1666]: #1668
#1170 := (+ #1169 #780)
#1171 := (<= #1170 0::Int)
#1164 := (+ ?v0!3 #769)
#1165 := (>= #1164 0::Int)
#1166 := (not #1165)
#1167 := (and #1163 #1166)
#1168 := (not #1167)
#1172 := (or #1168 #1171)
#1173 := (not #1172)
#1192 := (or #1173 #1188)
#1159 := (not #765)
#1156 := (not #804)
#1153 := (not #810)
#1205 := (not #439)
#1202 := (not #448)
#1059 := (not #684)
#1208 := (and #1059 #822 #1202 #1205 #1153 #1156 #1159 #1192)
#1150 := (not #379)
#1147 := (not #388)
#1144 := (not #813)
#1141 := (not #406)
#1196 := (and #1059 #816 #1141 #1144 #1147 #1150 #1153 #1156 #1159 #1192)
#1212 := (or #1196 #1208)
#1216 := (and #1059 #730 #1212)
#1116 := (+ #1115 #708)
#1117 := (<= #1116 0::Int)
#1118 := (or #1114 #1117)
#1119 := (not #1118)
#1125 := (and #1099 #1119)
#1129 := (or #1086 #1125)
#1080 := (not #256)
#1077 := (not #265)
#1074 := (not #274)
#1133 := (and #1059 #890 #1074 #1077 #1080 #1129)
#1220 := (or #1133 #1216)
#1069 := (not #535)
#1056 := (not #568)
#1224 := (and #1056 #1059 #933 #1069 #1220)
#1228 := (or #568 #1224)
#1232 := (and #669 #1228)
#1236 := (or #1042 #1232)
#1394 := (iff #1236 #1393)
#1391 := (iff #1232 #1390)
#1388 := (iff #1228 #1387)
#1385 := (iff #1224 #1382)
#1379 := (and #67 #681 #933 #80 #1376)
#1383 := (iff #1379 #1382)
#1384 := [rewrite]: #1383
#1380 := (iff #1224 #1379)
#1377 := (iff #1220 #1376)
#1374 := (iff #1216 #1371)
#1368 := (and #681 #730 #1365)
#1372 := (iff #1368 #1371)
#1373 := [rewrite]: #1372
#1369 := (iff #1216 #1368)
#1366 := (iff #1212 #1365)
#1363 := (iff #1208 #1360)
#1357 := (and #681 #817 #146 #147 #807 #800 #762 #1342)
#1361 := (iff #1357 #1360)
#1362 := [rewrite]: #1361
#1358 := (iff #1208 #1357)
#1343 := (iff #1192 #1342)
#1340 := (iff #1173 #1339)
#1337 := (iff #1172 #1336)
#1334 := (iff #1171 #1331)
#1323 := (+ #780 #1169)
#1326 := (<= #1323 0::Int)
#1332 := (iff #1326 #1331)
#1333 := [rewrite]: #1332
#1327 := (iff #1171 #1326)
#1324 := (= #1170 #1323)
#1325 := [rewrite]: #1324
#1328 := [monotonicity #1325]: #1327
#1335 := [trans #1328 #1333]: #1334
#1321 := (iff #1168 #1320)
#1318 := (iff #1167 #1317)
#1315 := (iff #1166 #1314)
#1312 := (iff #1165 #1309)
#1301 := (+ #769 ?v0!3)
#1304 := (>= #1301 0::Int)
#1310 := (iff #1304 #1309)
#1311 := [rewrite]: #1310
#1305 := (iff #1165 #1304)
#1302 := (= #1164 #1301)
#1303 := [rewrite]: #1302
#1306 := [monotonicity #1303]: #1305
#1313 := [trans #1306 #1311]: #1312
#1316 := [monotonicity #1313]: #1315
#1319 := [monotonicity #1316]: #1318
#1322 := [monotonicity #1319]: #1321
#1338 := [monotonicity #1322 #1335]: #1337
#1341 := [monotonicity #1338]: #1340
#1344 := [monotonicity #1341]: #1343
#1299 := (iff #1159 #762)
#1300 := [rewrite]: #1299
#1297 := (iff #1156 #800)
#1298 := [rewrite]: #1297
#1295 := (iff #1153 #807)
#1296 := [rewrite]: #1295
#1355 := (iff #1205 #147)
#1356 := [rewrite]: #1355
#1353 := (iff #1202 #146)
#1354 := [rewrite]: #1353
#1244 := (iff #1059 #681)
#1245 := [rewrite]: #1244
#1359 := [monotonicity #1245 #826 #1354 #1356 #1296 #1298 #1300 #1344]: #1358
#1364 := [trans #1359 #1362]: #1363
#1351 := (iff #1196 #1348)
#1345 := (and #681 #816 #110 #679 #113 #115 #807 #800 #762 #1342)
#1349 := (iff #1345 #1348)
#1350 := [rewrite]: #1349
#1346 := (iff #1196 #1345)
#1293 := (iff #1150 #115)
#1294 := [rewrite]: #1293
#1291 := (iff #1147 #113)
#1292 := [rewrite]: #1291
#1289 := (iff #1144 #679)
#1290 := [rewrite]: #1289
#1287 := (iff #1141 #110)
#1288 := [rewrite]: #1287
#1347 := [monotonicity #1245 #1288 #1290 #1292 #1294 #1296 #1298 #1300 #1344]: #1346
#1352 := [trans #1347 #1350]: #1351
#1367 := [monotonicity #1352 #1364]: #1366
#1370 := [monotonicity #1245 #1367]: #1369
#1375 := [trans #1370 #1373]: #1374
#1285 := (iff #1133 #1282)
#1279 := (and #681 #727 #83 #85 #87 #1276)
#1283 := (iff #1279 #1282)
#1284 := [rewrite]: #1283
#1280 := (iff #1133 #1279)
#1277 := (iff #1129 #1276)
#1274 := (iff #1125 #1273)
#1271 := (iff #1119 #1270)
#1268 := (iff #1118 #1267)
#1265 := (iff #1117 #1262)
#1254 := (+ #708 #1115)
#1257 := (<= #1254 0::Int)
#1263 := (iff #1257 #1262)
#1264 := [rewrite]: #1263
#1258 := (iff #1117 #1257)
#1255 := (= #1116 #1254)
#1256 := [rewrite]: #1255
#1259 := [monotonicity #1256]: #1258
#1266 := [trans #1259 #1264]: #1265
#1269 := [monotonicity #1266]: #1268
#1272 := [monotonicity #1269]: #1271
#1275 := [monotonicity #1272]: #1274
#1278 := [monotonicity #1275]: #1277
#1252 := (iff #1080 #87)
#1253 := [rewrite]: #1252
#1250 := (iff #1077 #85)
#1251 := [rewrite]: #1250
#1248 := (iff #1074 #83)
#1249 := [rewrite]: #1248
#1281 := [monotonicity #1245 #894 #1249 #1251 #1253 #1278]: #1280
#1286 := [trans #1281 #1284]: #1285
#1378 := [monotonicity #1286 #1375]: #1377
#1246 := (iff #1069 #80)
#1247 := [rewrite]: #1246
#1242 := (iff #1056 #67)
#1243 := [rewrite]: #1242
#1381 := [monotonicity #1243 #1245 #1247 #1378]: #1380
#1386 := [trans #1381 #1384]: #1385
#1389 := [monotonicity #1386]: #1388
#1392 := [monotonicity #1389]: #1391
#1395 := [monotonicity #1392]: #1394
#1001 := (not #965)
#1237 := (~ #1001 #1236)
#1233 := (not #962)
#1234 := (~ #1233 #1232)
#1229 := (not #959)
#1230 := (~ #1229 #1228)
#1225 := (not #954)
#1226 := (~ #1225 #1224)
#1221 := (not #911)
#1222 := (~ #1221 #1220)
#1217 := (not #906)
#1218 := (~ #1217 #1216)
#1213 := (not #885)
#1214 := (~ #1213 #1212)
#1209 := (not #880)
#1210 := (~ #1209 #1208)
#1193 := (not #797)
#1194 := (~ #1193 #1192)
#1189 := (not #794)
#1190 := (~ #1189 #1188)
#1186 := (~ #1185 #1185)
#1187 := [refl]: #1186
#1182 := (not #791)
#1183 := (~ #1182 #788)
#1180 := (~ #788 #788)
#1178 := (~ #785 #785)
#1179 := [refl]: #1178
#1181 := [nnf-pos #1179]: #1180
#1184 := [nnf-neg #1181]: #1183
#1191 := [nnf-neg #1184 #1187]: #1190
#1174 := (~ #791 #1173)
#1175 := [sk]: #1174
#1195 := [nnf-neg #1175 #1191]: #1194
#1160 := (~ #1159 #1159)
#1161 := [refl]: #1160
#1157 := (~ #1156 #1156)
#1158 := [refl]: #1157
#1154 := (~ #1153 #1153)
#1155 := [refl]: #1154
#1206 := (~ #1205 #1205)
#1207 := [refl]: #1206
#1203 := (~ #1202 #1202)
#1204 := [refl]: #1203
#1200 := (~ #822 #822)
#1201 := [refl]: #1200
#1060 := (~ #1059 #1059)
#1061 := [refl]: #1060
#1211 := [nnf-neg #1061 #1201 #1204 #1207 #1155 #1158 #1161 #1195]: #1210
#1197 := (not #856)
#1198 := (~ #1197 #1196)
#1151 := (~ #1150 #1150)
#1152 := [refl]: #1151
#1148 := (~ #1147 #1147)
#1149 := [refl]: #1148
#1145 := (~ #1144 #1144)
#1146 := [refl]: #1145
#1142 := (~ #1141 #1141)
#1143 := [refl]: #1142
#1139 := (~ #816 #816)
#1140 := [refl]: #1139
#1199 := [nnf-neg #1061 #1140 #1143 #1146 #1149 #1152 #1155 #1158 #1161 #1195]: #1198
#1215 := [nnf-neg #1199 #1211]: #1214
#1137 := (~ #730 #730)
#1138 := [refl]: #1137
#1219 := [nnf-neg #1061 #1138 #1215]: #1218
#1134 := (not #751)
#1135 := (~ #1134 #1133)
#1130 := (not #722)
#1131 := (~ #1130 #1129)
#1126 := (not #719)
#1127 := (~ #1126 #1125)
#1120 := (not #716)
#1121 := (~ #1120 #1119)
#1122 := [sk]: #1121
#1104 := (not #705)
#1105 := (~ #1104 #1099)
#1100 := (~ #702 #1099)
#1101 := [sk]: #1100
#1106 := [nnf-neg #1101]: #1105
#1128 := [nnf-neg #1106 #1122]: #1127
#1087 := (~ #705 #1086)
#1084 := (~ #1083 #1083)
#1085 := [refl]: #1084
#1088 := [nnf-neg #1085]: #1087
#1132 := [nnf-neg #1088 #1128]: #1131
#1081 := (~ #1080 #1080)
#1082 := [refl]: #1081
#1078 := (~ #1077 #1077)
#1079 := [refl]: #1078
#1075 := (~ #1074 #1074)
#1076 := [refl]: #1075
#1072 := (~ #890 #890)
#1073 := [refl]: #1072
#1136 := [nnf-neg #1061 #1073 #1076 #1079 #1082 #1132]: #1135
#1223 := [nnf-neg #1136 #1219]: #1222
#1070 := (~ #1069 #1069)
#1071 := [refl]: #1070
#1066 := (not #936)
#1067 := (~ #1066 #933)
#1064 := (~ #933 #933)
#1062 := (~ #930 #930)
#1063 := [refl]: #1062
#1065 := [nnf-pos #1063]: #1064
#1068 := [nnf-neg #1065]: #1067
#1057 := (~ #1056 #1056)
#1058 := [refl]: #1057
#1227 := [nnf-neg #1058 #1061 #1068 #1071 #1223]: #1226
#1054 := (~ #568 #568)
#1055 := [refl]: #1054
#1231 := [nnf-neg #1055 #1227]: #1230
#1051 := (not #672)
#1052 := (~ #1051 #669)
#1049 := (~ #669 #669)
#1047 := (~ #666 #666)
#1048 := [refl]: #1047
#1050 := [nnf-pos #1048]: #1049
#1053 := [nnf-neg #1050]: #1052
#1235 := [nnf-neg #1053 #1231]: #1234
#1043 := (~ #672 #1042)
#1044 := [sk]: #1043
#1238 := [nnf-neg #1044 #1235]: #1237
#1002 := [not-or-elim #998]: #1001
#1239 := [mp~ #1002 #1238]: #1236
#1240 := [mp #1239 #1395]: #1393
#1670 := [mp #1240 #1669]: #1667
#2294 := [mp #1670 #2293]: #2291
#2323 := [unit-resolution #2294 #1950]: #2288
#2024 := (or #2285 #2279)
#2025 := [def-axiom]: #2024
#2327 := [unit-resolution #2025 #2323]: #2279
#2296 := (or #2282 #2276)
#1878 := (iff #52 #67)
#2328 := (iff #67 #52)
#2002 := [commutativity]: #2328
#1879 := [symm #2002]: #1878
#1880 := [mp #1000 #1879]: #67
#2023 := (or #2282 #568 #2276)
#2019 := [def-axiom]: #2023
#2297 := [unit-resolution #2019 #1880]: #2296
#2298 := [unit-resolution #2297 #2327]: #2276
#2346 := (or #2273 #2264)
#2309 := (= #79 f22)
#2306 := (* -1::Int f18)
#2307 := (+ f14 #2306)
#2308 := (<= #2307 0::Int)
#2310 := (or #1539 #2308 #2309)
#2022 := (= f20 f22)
#2312 := [hypothesis]: #2261
#2313 := [hypothesis]: #2276
#2030 := (or #2273 #2267)
#2032 := [def-axiom]: #2030
#2329 := [unit-resolution #2032 #2313]: #2267
#2042 := (or #2270 #2220 #2264)
#2043 := [def-axiom]: #2042
#2330 := [unit-resolution #2043 #2329 #2312]: #2220
#1747 := (or #2217 #85)
#2123 := [def-axiom]: #1747
#2331 := [unit-resolution #2123 #2330]: #85
#2333 := [symm #2331]: #2022
#2051 := (or #2273 #80)
#2029 := [def-axiom]: #2051
#2332 := [unit-resolution #2029 #2313]: #80
#2334 := [trans #2332 #2333]: #2309
#2324 := (not #2309)
#2325 := (or #2310 #2324)
#2326 := [def-axiom]: #2325
#2335 := [unit-resolution #2326 #2334]: #2310
#1847 := (or #2217 #2211)
#2121 := [def-axiom]: #1847
#2336 := [unit-resolution #2121 #2330]: #2211
#1850 := (or #2217 #727)
#1851 := [def-axiom]: #1850
#2337 := [unit-resolution #1851 #2330]: #727
#2028 := (+ f20 #708)
#2001 := (<= #2028 0::Int)
#2338 := (not #2022)
#2339 := (or #2338 #2001)
#2340 := [th-lemma arith triangle-eq]: #2339
#2341 := [unit-resolution #2340 #2333]: #2001
#2050 := (or #2273 #2198)
#2040 := [def-axiom]: #2050
#2342 := [unit-resolution #2040 #2313]: #2198
#1796 := (not #2001)
#1776 := (or #1527 #2203 #1796 #730)
#1861 := (+ f19 #1109)
#1862 := (<= #1861 0::Int)
#1790 := (not #1862)
#1799 := [hypothesis]: #727
#1800 := [hypothesis]: #1528
#1795 := (or #1527 #1112)
#2131 := [def-axiom]: #1795
#1801 := [unit-resolution #2131 #1800]: #1112
#1802 := (or #1790 #730 #1111)
#1783 := [th-lemma arith assign-bounds 1 -1]: #1802
#1785 := [unit-resolution #1783 #1801 #1799]: #1790
#1859 := (+ f20 #1260)
#1840 := (>= #1859 0::Int)
#1791 := (not #1840)
#1807 := [hypothesis]: #2001
#2132 := (not #1262)
#2133 := (or #1527 #2132)
#2134 := [def-axiom]: #2133
#1786 := [unit-resolution #2134 #1800]: #2132
#1797 := (or #1791 #1262 #1796)
#1809 := [hypothesis]: #2132
#1810 := [hypothesis]: #1840
#1789 := [th-lemma arith farkas -1 1 1 #1810 #1809 #1807]: false
#1798 := [lemma #1789]: #1797
#1784 := [unit-resolution #1798 #1786 #1807]: #1791
#1777 := (or #1862 #1840)
#1793 := (or #1527 #1108)
#1794 := [def-axiom]: #1793
#1787 := [unit-resolution #1794 #1800]: #1108
#1775 := [hypothesis]: #2198
#1812 := (or #2203 #1500 #1862 #1840)
#1869 := (+ #1115 #925)
#1870 := (<= #1869 0::Int)
#1885 := (+ ?v0!2 #725)
#1886 := (>= #1885 0::Int)
#1871 := (or #1500 #1886 #1870)
#1814 := (or #2203 #1871)
#1823 := (iff #1814 #1812)
#1844 := (or #1500 #1862 #1840)
#1806 := (or #2203 #1844)
#1821 := (iff #1806 #1812)
#1822 := [rewrite]: #1821
#1819 := (iff #1814 #1806)
#1835 := (iff #1871 #1844)
#1834 := (iff #1870 #1840)
#1855 := (+ #925 #1115)
#1857 := (<= #1855 0::Int)
#1841 := (iff #1857 #1840)
#1842 := [rewrite]: #1841
#1858 := (iff #1870 #1857)
#1856 := (= #1869 #1855)
#1848 := [rewrite]: #1856
#1849 := [monotonicity #1848]: #1858
#1843 := [trans #1849 #1842]: #1834
#1865 := (iff #1886 #1862)
#1872 := (+ #725 ?v0!2)
#1867 := (>= #1872 0::Int)
#1864 := (iff #1867 #1862)
#1863 := [rewrite]: #1864
#1875 := (iff #1886 #1867)
#1873 := (= #1885 #1872)
#1874 := [rewrite]: #1873
#1860 := [monotonicity #1874]: #1875
#1854 := [trans #1860 #1863]: #1865
#1845 := [monotonicity #1854 #1843]: #1835
#1820 := [monotonicity #1845]: #1819
#1813 := [trans #1820 #1822]: #1823
#1815 := [quant-inst #1107]: #1814
#1824 := [mp #1815 #1813]: #1812
#1778 := [unit-resolution #1824 #1775 #1787]: #1777
#1781 := [unit-resolution #1778 #1784 #1785]: false
#1782 := [lemma #1781]: #1776
#2343 := [unit-resolution #1782 #2342 #2341 #2337]: #1527
#1780 := (or #2214 #2206 #1528)
#2140 := [def-axiom]: #1780
#2344 := [unit-resolution #2140 #2343 #2336]: #2206
#2311 := (not #2310)
#2136 := (not #2206)
#2314 := (or #2136 #2311)
#2315 := [quant-inst #68]: #2314
#2345 := [unit-resolution #2315 #2344 #2335]: false
#2347 := [lemma #2345]: #2346
#2316 := [unit-resolution #2347 #2298]: #2264
#2055 := (or #2261 #2255)
#2056 := [def-axiom]: #2055
#2317 := [unit-resolution #2056 #2316]: #2255
#2493 := [hypothesis]: #2252
#1995 := (or #2249 #817)
#2088 := [def-axiom]: #1995
#2494 := [unit-resolution #2088 #2493]: #817
#2118 := (not #1331)
#2071 := (or #2249 #2237)
#2072 := [def-axiom]: #2071
#2495 := [unit-resolution #2072 #2493]: #2237
#1990 := (= f20 f26)
#2076 := (or #2249 #147)
#2078 := [def-axiom]: #2076
#2496 := [unit-resolution #2078 #2493]: #147
#2501 := [symm #2496]: #1990
#2502 := (= #129 f20)
#2497 := [unit-resolution #2029 #2298]: #80
#2499 := (= #129 #79)
#2085 := (or #2249 #146)
#2089 := [def-axiom]: #2085
#2498 := [unit-resolution #2089 #2493]: #146
#2500 := [monotonicity #2498]: #2499
#2503 := [trans #2500 #2497]: #2502
#2504 := [trans #2503 #2501]: #130
#2110 := (or #2231 #1185)
#2106 := [def-axiom]: #2110
#2505 := [unit-resolution #2106 #2504]: #2231
#2101 := (or #2240 #1567 #2234)
#2102 := [def-axiom]: #2101
#2506 := [unit-resolution #2102 #2505 #2495]: #1567
#1833 := (or #1562 #2118)
#2115 := [def-axiom]: #1833
#2507 := [unit-resolution #2115 #2506]: #2118
#1983 := (+ f20 #780)
#1991 := (<= #1983 0::Int)
#2510 := (iff #147 #1990)
#2508 := (iff #1990 #147)
#2509 := [commutativity]: #2508
#2511 := [symm #2509]: #2510
#2512 := [mp #2496 #2511]: #1990
#2513 := (not #1990)
#2514 := (or #2513 #1991)
#2515 := [th-lemma arith triangle-eq]: #2514
#2516 := [unit-resolution #2515 #2512]: #1991
#2449 := (not #1991)
#2477 := (or #2476 #2449 #1331 #816)
#2473 := [hypothesis]: #817
#2445 := [hypothesis]: #2118
#2444 := [hypothesis]: #1991
#2474 := [hypothesis]: #2472
#2475 := [th-lemma arith farkas 1 -1 -1 1 #2474 #2444 #2445 #2473]: false
#2478 := [lemma #2475]: #2477
#2517 := [unit-resolution #2478 #2516 #2507 #2494]: #2476
#2482 := (or #2481 #2472)
#2483 := [th-lemma arith triangle-eq]: #2482
#2518 := [unit-resolution #2483 #2517]: #2481
#2471 := (= f19 ?v0!3)
#2412 := (+ f19 #1307)
#2468 := (>= #2412 0::Int)
#2126 := (>= #801 -1::Int)
#2069 := (or #2249 #800)
#2079 := [def-axiom]: #2069
#2519 := [unit-resolution #2079 #2493]: #800
#2520 := (or #804 #2126)
#2521 := [th-lemma arith triangle-eq]: #2520
#2522 := [unit-resolution #2521 #2519]: #2126
#1839 := (or #1562 #1314)
#2117 := [def-axiom]: #1839
#2523 := [unit-resolution #2117 #2506]: #1314
#2524 := (not #2126)
#2525 := (or #2468 #1309 #2524)
#2526 := [th-lemma arith assign-bounds 1 1]: #2525
#2527 := [unit-resolution #2526 #2523 #2522]: #2468
#2413 := (<= #2412 0::Int)
#2424 := (+ f20 #1329)
#2425 := (>= #2424 0::Int)
#2448 := (not #2425)
#2450 := (or #2448 #1331 #2449)
#2446 := [hypothesis]: #2425
#2447 := [th-lemma arith farkas -1 1 1 #2446 #2445 #2444]: false
#2451 := [lemma #2447]: #2450
#2528 := [unit-resolution #2451 #2507 #2516]: #2448
#2530 := (or #2413 #2425)
#1837 := (or #1562 #1163)
#1838 := [def-axiom]: #1837
#2529 := [unit-resolution #1838 #2506]: #1163
#2457 := [unit-resolution #2040 #2298]: #2198
#2433 := (or #2203 #1547 #2413 #2425)
#2403 := (+ #1169 #925)
#2404 := (<= #2403 0::Int)
#2395 := (+ ?v0!3 #725)
#2396 := (>= #2395 0::Int)
#2405 := (or #1547 #2396 #2404)
#2434 := (or #2203 #2405)
#2441 := (iff #2434 #2433)
#2430 := (or #1547 #2413 #2425)
#2436 := (or #2203 #2430)
#2439 := (iff #2436 #2433)
#2440 := [rewrite]: #2439
#2437 := (iff #2434 #2436)
#2431 := (iff #2405 #2430)
#2428 := (iff #2404 #2425)
#2418 := (+ #925 #1169)
#2421 := (<= #2418 0::Int)
#2426 := (iff #2421 #2425)
#2427 := [rewrite]: #2426
#2422 := (iff #2404 #2421)
#2419 := (= #2403 #2418)
#2420 := [rewrite]: #2419
#2423 := [monotonicity #2420]: #2422
#2429 := [trans #2423 #2427]: #2428
#2416 := (iff #2396 #2413)
#2406 := (+ #725 ?v0!3)
#2409 := (>= #2406 0::Int)
#2414 := (iff #2409 #2413)
#2415 := [rewrite]: #2414
#2410 := (iff #2396 #2409)
#2407 := (= #2395 #2406)
#2408 := [rewrite]: #2407
#2411 := [monotonicity #2408]: #2410
#2417 := [trans #2411 #2415]: #2416
#2432 := [monotonicity #2417 #2429]: #2431
#2438 := [monotonicity #2432]: #2437
#2442 := [trans #2438 #2440]: #2441
#2435 := [quant-inst #1162]: #2434
#2443 := [mp #2435 #2442]: #2433
#2531 := [unit-resolution #2443 #2457 #2529]: #2530
#2532 := [unit-resolution #2531 #2528]: #2413
#2534 := (not #2468)
#2533 := (not #2413)
#2535 := (or #2471 #2533 #2534)
#2536 := [th-lemma arith triangle-eq]: #2535
#2537 := [unit-resolution #2536 #2532 #2527]: #2471
#2490 := (not #2471)
#2491 := (or #2490 #2469)
#2487 := [hypothesis]: #2471
#2488 := [monotonicity #2487]: #2469
#2486 := [hypothesis]: #2481
#2489 := [unit-resolution #2486 #2488]: false
#2492 := [lemma #2489]: #2491
#2538 := [unit-resolution #2492 #2537 #2518]: false
#2539 := [lemma #2538]: #2249
#2062 := (or #2258 #2246 #2252)
#2063 := [def-axiom]: #2062
#2400 := [unit-resolution #2063 #2539 #2317]: #2246
#1937 := (or #2243 #115)
#2090 := [def-axiom]: #1937
#2401 := [unit-resolution #2090 #2400]: #115
#2554 := [symm #2401]: #2553
#2551 := (= #107 f24)
#2098 := (or #2243 #110)
#2105 := [def-axiom]: #2098
#2550 := [unit-resolution #2105 #2400]: #110
#2552 := [symm #2550]: #2551
#2555 := [trans #2552 #2554]: #2364
#2556 := (not #2364)
#2557 := (or #2556 #2399)
#2558 := [th-lemma arith triangle-eq]: #2557
#2559 := [unit-resolution #2558 #2555]: #2399
#1938 := (or #2243 #2237)
#2086 := [def-axiom]: #1938
#2560 := [unit-resolution #2086 #2400]: #2237
#2564 := (= #129 f24)
#2562 := (= #129 #107)
#1934 := (or #2243 #113)
#1936 := [def-axiom]: #1934
#2561 := [unit-resolution #1936 #2400]: #113
#2563 := [monotonicity #2561]: #2562
#2565 := [trans #2563 #2552]: #2564
#2566 := [trans #2565 #2554]: #130
#2567 := [unit-resolution #2106 #2566]: #2231
#2568 := [unit-resolution #2102 #2567 #2560]: #1567
#2569 := [unit-resolution #2115 #2568]: #2118
#2570 := (not #2399)
#2571 := (or #2476 #1331 #2570)
#2572 := [th-lemma arith assign-bounds -1 -1]: #2571
#2573 := [unit-resolution #2572 #2569 #2559]: #2476
#2574 := [unit-resolution #2483 #2573]: #2481
#2094 := (or #2243 #800)
#2092 := [def-axiom]: #2094
#2575 := [unit-resolution #2092 #2400]: #800
#2576 := [unit-resolution #2521 #2575]: #2126
#2577 := [unit-resolution #2117 #2568]: #1314
#2578 := [unit-resolution #2526 #2577 #2576]: #2468
#2103 := (or #2243 #816)
#2104 := [def-axiom]: #2103
#2579 := [unit-resolution #2104 #2400]: #816
#2580 := (or #2448 #1331 #2570 #817)
#2581 := [th-lemma arith assign-bounds 1 1 1]: #2580
#2582 := [unit-resolution #2581 #2569 #2579 #2559]: #2448
#2583 := [unit-resolution #1838 #2568]: #1163
#2584 := [unit-resolution #2443 #2457 #2583 #2582]: #2413
#2585 := [unit-resolution #2536 #2584 #2578]: #2471
[unit-resolution #2492 #2585 #2574]: false
unsat