src/HOL/Boogie/Examples/Boogie_Max.certs

updated SMT certificates

dea36391893064c022de7bc923e15ef446cb4303 2224 0
#2 := false
#8 := 0::int
decl f5 :: (-> int int)
decl ?v0!3 :: int
#1153 := ?v0!3
#1154 := (f5 ?v0!3)
#652 := -1::int
#1356 := (* -1::int #1154)
decl f7 :: int
#31 := f7
#68 := (f5 f7)
#2646 := (+ #68 #1356)
#2648 := (>= #2646 0::int)
#2645 := (= #68 #1154)
#2494 := (= f7 ?v0!3)
#1334 := (* -1::int ?v0!3)
#2380 := (+ f7 #1334)
#2496 := (>= #2380 0::int)
decl f15 :: int
#79 := f15
#1335 := (+ f15 #1334)
#1336 := (<= #1335 0::int)
#1341 := (not #1336)
decl f14 :: int
#75 := f14
#1357 := (+ f14 #1356)
#1358 := (>= #1357 0::int)
#1160 := (>= ?v0!3 0::int)
#1609 := (not #1160)
#1624 := (or #1609 #1336 #1358)
#1629 := (not #1624)
#20 := (:var 0 int)
#24 := (f5 #20)
#2199 := (pattern #24)
#777 := (* -1::int f14)
#778 := (+ #24 #777)
#779 := (<= #778 0::int)
#766 := (* -1::int f15)
#767 := (+ #20 #766)
#765 := (>= #767 0::int)
#641 := (>= #20 0::int)
#1440 := (not #641)
#1591 := (or #1440 #765 #779)
#2216 := (forall (vars (?v0 int)) (:pat #2199) #1591)
#2221 := (not #2216)
decl f13 :: int
#73 := f13
#90 := (f5 f13)
#307 := (= f14 #90)
#2224 := (or #307 #2221)
#2227 := (not #2224)
#2230 := (or #2227 #1629)
#2233 := (not #2230)
#820 := (* -1::int #68)
decl f8 :: int
#36 := f8
#821 := (+ f8 #820)
#819 := (>= #821 0::int)
#818 := (not #819)
#803 := (+ f7 #766)
#802 := (= #803 -1::int)
#806 := (not #802)
#82 := 2::int
#757 := (>= f15 2::int)
#1639 := (not #757)
#754 := (>= f13 0::int)
#1638 := (not #754)
#15 := 1::int
#671 := (>= f7 1::int)
#815 := (not #671)
decl f6 :: int
#29 := f6
#668 := (>= f6 0::int)
#1569 := (not #668)
#426 := (= f8 f14)
#432 := (not #426)
#423 := (= f6 f13)
#441 := (not #423)
#2242 := (or #441 #432 #1569 #815 #1638 #1639 #806 #818 #2233)
#2245 := (not #2242)
decl f12 :: int
#70 := f12
#288 := (= f12 f14)
#366 := (not #288)
#285 := (= f7 f13)
#375 := (not #285)
#280 := (= #68 f12)
#393 := (not #280)
#2236 := (or #393 #375 #366 #1569 #815 #1638 #1639 #806 #819 #2233)
#2239 := (not #2236)
#2248 := (or #2239 #2245)
#2251 := (not #2248)
#722 := (* -1::int f7)
decl f3 :: int
#9 := f3
#723 := (+ f3 #722)
#724 := (<= #723 0::int)
#2254 := (or #1569 #815 #724 #2251)
#2257 := (not #2254)
decl ?v0!1 :: int
#1086 := ?v0!1
#1094 := (f5 ?v0!1)
decl f10 :: int
#45 := f10
#1267 := (= f10 #1094)
#1091 := (>= ?v0!1 0::int)
#1510 := (not #1091)
#1087 := (* -1::int ?v0!1)
#1088 := (+ f3 #1087)
#1089 := (<= #1088 0::int)
#1525 := (or #1089 #1510 #1267)
#1556 := (not #1525)
decl ?v0!2 :: int
#1104 := ?v0!2
#1105 := (f5 ?v0!2)
#1291 := (* -1::int #1105)
#1292 := (+ f10 #1291)
#1293 := (>= #1292 0::int)
#1112 := (>= ?v0!2 0::int)
#1530 := (not #1112)
#1108 := (* -1::int ?v0!2)
#1109 := (+ f3 #1108)
#1110 := (<= #1109 0::int)
#1687 := (or #1110 #1530 #1293 #1556)
#1690 := (not #1687)
#679 := (* -1::int #20)
#680 := (+ f3 #679)
#681 := (<= #680 0::int)
#51 := (= #24 f10)
#1499 := (or #51 #1440 #681)
#1504 := (not #1499)
#2260 := (forall (vars (?v0 int)) (:pat #2199) #1504)
#2265 := (or #2260 #1690)
#2268 := (not #2265)
#727 := (not #724)
decl f11 :: int
#47 := f11
#185 := (= f7 f11)
#223 := (not #185)
#182 := (= f8 f10)
#232 := (not #182)
decl f9 :: int
#43 := f9
#179 := (= f6 f9)
#241 := (not #179)
#2271 := (or #241 #232 #223 #1569 #815 #727 #2268)
#927 := (* -1::int f8)
#928 := (+ #24 #927)
#929 := (<= #928 0::int)
#917 := (+ #20 #722)
#916 := (>= #917 0::int)
#1477 := (or #1440 #916 #929)
#2208 := (forall (vars (?v0 int)) (:pat #2199) #1477)
#2274 := (not #2271)
#2277 := (or #2257 #2274)
#2280 := (not #2277)
#2213 := (not #2208)
#655 := (* -1::int #24)
decl f4 :: int
#11 := f4
#656 := (+ f4 #655)
#654 := (>= #656 0::int)
#644 := (>= #20 1::int)
#1455 := (or #1440 #644 #654)
#2200 := (forall (vars (?v0 int)) (:pat #2199) #1455)
#2205 := (not #2200)
#40 := (f5 f6)
#176 := (= f8 #40)
#528 := (not #176)
#2283 := (or #528 #1569 #815 #2205 #2213 #2280)
#2286 := (not #2283)
decl ?v0!0 :: int
#1046 := ?v0!0
#1049 := (>= ?v0!0 0::int)
#1167 := (not #1049)
#1047 := (f5 ?v0!0)
#1044 := (* -1::int #1047)
#1045 := (+ f4 #1044)
#1007 := (>= #1045 0::int)
#1005 := (>= ?v0!0 1::int)
#1432 := (or #1005 #1007 #1167)
#2072 := (= f4 #1047)
#12 := (f5 0::int)
#2053 := (= #12 #1047)
#1941 := (= #1047 #12)
#2071 := (= ?v0!0 0::int)
#1048 := (not #1005)
#1437 := (not #1432)
#2073 := [hypothesis]: #1437
#1785 := (or #1432 #1048)
#1870 := [def-axiom]: #1785
#2046 := [unit-resolution #1870 #2073]: #1048
#1863 := (or #1432 #1049)
#1874 := [def-axiom]: #1863
#2047 := [unit-resolution #1874 #2073]: #1049
#2048 := [th-lemma #2047 #2046]: #2071
#2052 := [monotonicity #2048]: #1941
#2054 := [symm #2052]: #2053
#13 := (= f4 #12)
#970 := (<= f3 0::int)
#918 := (not #916)
#921 := (and #641 #918)
#924 := (not #921)
#932 := (or #924 #929)
#935 := (forall (vars (?v0 int)) #932)
#938 := (not #935)
#809 := (and #671 #754)
#812 := (not #809)
#768 := (not #765)
#771 := (and #641 #768)
#774 := (not #771)
#782 := (or #774 #779)
#785 := (forall (vars (?v0 int)) #782)
#788 := (not #785)
#794 := (or #307 #788)
#799 := (and #785 #794)
#759 := (and #754 #757)
#762 := (not #759)
#673 := (and #668 #671)
#676 := (not #673)
#882 := (or #441 #432 #676 #762 #799 #806 #812 #818)
#858 := (or #393 #375 #366 #815 #676 #762 #799 #806 #812 #819)
#887 := (and #858 #882)
#908 := (or #676 #724 #887)
#705 := (* -1::int f10)
#706 := (+ #24 #705)
#707 := (<= #706 0::int)
#682 := (not #681)
#685 := (and #641 #682)
#688 := (not #685)
#710 := (or #688 #707)
#713 := (forall (vars (?v0 int)) #710)
#694 := (or #51 #688)
#699 := (exists (vars (?v0 int)) #694)
#702 := (not #699)
#716 := (or #702 #713)
#719 := (and #699 #716)
#748 := (or #241 #232 #223 #676 #719 #727)
#913 := (and #748 #908)
#561 := (not #13)
#956 := (or #561 #528 #676 #913 #938)
#961 := (and #13 #956)
#642 := (not #644)
#646 := (and #641 #642)
#649 := (not #646)
#658 := (or #649 #654)
#661 := (forall (vars (?v0 int)) #658)
#664 := (not #661)
#964 := (or #664 #961)
#967 := (and #661 #964)
#990 := (or #561 #967 #970)
#995 := (not #990)
#1 := true
#91 := (= #90 f14)
#92 := (and #91 true)
#87 := (<= #24 f14)
#85 := (< #20 f15)
#21 := (<= 0::int #20)
#86 := (and #21 #85)
#88 := (implies #86 #87)
#89 := (forall (vars (?v0 int)) #88)
#93 := (implies #89 #92)
#94 := (and #89 #93)
#83 := (<= 2::int f15)
#77 := (<= 0::int f13)
#84 := (and #77 #83)
#95 := (implies #84 #94)
#80 := (+ f7 1::int)
#81 := (= f15 #80)
#96 := (implies #81 #95)
#32 := (<= 1::int f7)
#78 := (and #77 #32)
#97 := (implies #78 #96)
#98 := (implies true #97)
#108 := (= f14 f8)
#109 := (implies #108 #98)
#107 := (= f13 f6)
#110 := (implies #107 #109)
#30 := (<= 0::int f6)
#33 := (and #30 #32)
#111 := (implies #33 #110)
#106 := (<= #68 f8)
#112 := (implies #106 #111)
#113 := (implies #33 #112)
#114 := (implies true #113)
#76 := (= f14 f12)
#99 := (implies #76 #98)
#74 := (= f13 f7)
#100 := (implies #74 #99)
#72 := (and #32 #32)
#101 := (implies #72 #100)
#71 := (= f12 #68)
#102 := (implies #71 #101)
#69 := (< f8 #68)
#103 := (implies #69 #102)
#104 := (implies #33 #103)
#105 := (implies true #104)
#115 := (and #105 #114)
#116 := (implies #33 #115)
#67 := (< f7 f3)
#117 := (implies #67 #116)
#118 := (implies #33 #117)
#119 := (implies true #118)
#54 := (<= #24 f10)
#49 := (< #20 f3)
#50 := (and #21 #49)
#55 := (implies #50 #54)
#56 := (forall (vars (?v0 int)) #55)
#57 := (and #56 true)
#52 := (implies #50 #51)
#53 := (exists (vars (?v0 int)) #52)
#58 := (implies #53 #57)
#59 := (and #53 #58)
#48 := (= f11 f7)
#60 := (implies #48 #59)
#46 := (= f10 f8)
#61 := (implies #46 #60)
#44 := (= f9 f6)
#62 := (implies #44 #61)
#63 := (implies #33 #62)
#42 := (<= f3 f7)
#64 := (implies #42 #63)
#65 := (implies #33 #64)
#66 := (implies true #65)
#120 := (and #66 #119)
#121 := (implies #33 #120)
#41 := (= #40 f8)
#122 := (implies #41 #121)
#37 := (<= #24 f8)
#34 := (< #20 f7)
#35 := (and #21 #34)
#38 := (implies #35 #37)
#39 := (forall (vars (?v0 int)) #38)
#123 := (implies #39 #122)
#124 := (implies #33 #123)
#125 := (implies true #124)
#28 := (= #12 f4)
#126 := (implies #28 #125)
#127 := (and #28 #126)
#25 := (<= #24 f4)
#22 := (< #20 1::int)
#23 := (and #21 #22)
#26 := (implies #23 #25)
#27 := (forall (vars (?v0 int)) #26)
#128 := (implies #27 #127)
#129 := (and #27 #128)
#16 := (<= 1::int 1::int)
#17 := (and #16 #16)
#14 := (<= 0::int 0::int)
#18 := (and #14 #17)
#19 := (and #14 #18)
#130 := (implies #19 #129)
#131 := (implies #13 #130)
#10 := (< 0::int f3)
#132 := (implies #10 #131)
#133 := (implies true #132)
#134 := (not #133)
#998 := (iff #134 #995)
#300 := (not #86)
#301 := (or #300 #87)
#304 := (forall (vars (?v0 int)) #301)
#320 := (not #304)
#321 := (or #320 #307)
#326 := (and #304 #321)
#332 := (not #84)
#333 := (or #332 #326)
#294 := (+ 1::int f7)
#297 := (= f15 #294)
#341 := (not #297)
#342 := (or #341 #333)
#291 := (and #32 #77)
#350 := (not #291)
#351 := (or #350 #342)
#433 := (or #351 #432)
#442 := (or #441 #433)
#250 := (not #33)
#450 := (or #250 #442)
#458 := (not #106)
#459 := (or #458 #450)
#467 := (or #250 #459)
#367 := (or #366 #351)
#376 := (or #375 #367)
#384 := (not #32)
#385 := (or #384 #376)
#394 := (or #393 #385)
#402 := (not #69)
#403 := (or #402 #394)
#411 := (or #250 #403)
#479 := (and #411 #467)
#485 := (or #250 #479)
#493 := (not #67)
#494 := (or #493 #485)
#502 := (or #250 #494)
#188 := (not #50)
#195 := (or #188 #54)
#198 := (forall (vars (?v0 int)) #195)
#189 := (or #188 #51)
#192 := (exists (vars (?v0 int)) #189)
#211 := (not #192)
#212 := (or #211 #198)
#217 := (and #192 #212)
#224 := (or #223 #217)
#233 := (or #232 #224)
#242 := (or #241 #233)
#251 := (or #250 #242)
#259 := (not #42)
#260 := (or #259 #251)
#268 := (or #250 #260)
#514 := (and #268 #502)
#520 := (or #250 #514)
#529 := (or #528 #520)
#169 := (not #35)
#170 := (or #169 #37)
#173 := (forall (vars (?v0 int)) #170)
#537 := (not #173)
#538 := (or #537 #529)
#546 := (or #250 #538)
#562 := (or #561 #546)
#567 := (and #13 #562)
#160 := (not #23)
#161 := (or #160 #25)
#164 := (forall (vars (?v0 int)) #161)
#573 := (not #164)
#574 := (or #573 #567)
#579 := (and #164 #574)
#154 := (and #14 #16)
#157 := (and #14 #154)
#585 := (not #157)
#586 := (or #585 #579)
#594 := (or #561 #586)
#602 := (not #10)
#603 := (or #602 #594)
#615 := (not #603)
#996 := (iff #615 #995)
#993 := (iff #603 #990)
#981 := (or false #967)
#984 := (or #561 #981)
#987 := (or #970 #984)
#991 := (iff #987 #990)
#992 := [rewrite]: #991
#988 := (iff #603 #987)
#985 := (iff #594 #984)
#982 := (iff #586 #981)
#968 := (iff #579 #967)
#965 := (iff #574 #964)
#962 := (iff #567 #961)
#959 := (iff #562 #956)
#941 := (or #676 #913)
#944 := (or #528 #941)
#947 := (or #938 #944)
#950 := (or #676 #947)
#953 := (or #561 #950)
#957 := (iff #953 #956)
#958 := [rewrite]: #957
#954 := (iff #562 #953)
#951 := (iff #546 #950)
#948 := (iff #538 #947)
#945 := (iff #529 #944)
#942 := (iff #520 #941)
#914 := (iff #514 #913)
#911 := (iff #502 #908)
#899 := (or #676 #887)
#902 := (or #724 #899)
#905 := (or #676 #902)
#909 := (iff #905 #908)
#910 := [rewrite]: #909
#906 := (iff #502 #905)
#903 := (iff #494 #902)
#900 := (iff #485 #899)
#888 := (iff #479 #887)
#885 := (iff #467 #882)
#831 := (or #762 #799)
#834 := (or #806 #831)
#837 := (or #812 #834)
#867 := (or #837 #432)
#870 := (or #441 #867)
#873 := (or #676 #870)
#876 := (or #818 #873)
#879 := (or #676 #876)
#883 := (iff #879 #882)
#884 := [rewrite]: #883
#880 := (iff #467 #879)
#877 := (iff #459 #876)
#874 := (iff #450 #873)
#871 := (iff #442 #870)
#868 := (iff #433 #867)
#838 := (iff #351 #837)
#835 := (iff #342 #834)
#832 := (iff #333 #831)
#800 := (iff #326 #799)
#797 := (iff #321 #794)
#791 := (or #788 #307)
#795 := (iff #791 #794)
#796 := [rewrite]: #795
#792 := (iff #321 #791)
#789 := (iff #320 #788)
#786 := (iff #304 #785)
#783 := (iff #301 #782)
#780 := (iff #87 #779)
#781 := [rewrite]: #780
#775 := (iff #300 #774)
#772 := (iff #86 #771)
#769 := (iff #85 #768)
#770 := [rewrite]: #769
#639 := (iff #21 #641)
#640 := [rewrite]: #639
#773 := [monotonicity #640 #770]: #772
#776 := [monotonicity #773]: #775
#784 := [monotonicity #776 #781]: #783
#787 := [quant-intro #784]: #786
#790 := [monotonicity #787]: #789
#793 := [monotonicity #790]: #792
#798 := [trans #793 #796]: #797
#801 := [monotonicity #787 #798]: #800
#763 := (iff #332 #762)
#760 := (iff #84 #759)
#756 := (iff #83 #757)
#758 := [rewrite]: #756
#753 := (iff #77 #754)
#755 := [rewrite]: #753
#761 := [monotonicity #755 #758]: #760
#764 := [monotonicity #761]: #763
#833 := [monotonicity #764 #801]: #832
#807 := (iff #341 #806)
#804 := (iff #297 #802)
#805 := [rewrite]: #804
#808 := [monotonicity #805]: #807
#836 := [monotonicity #808 #833]: #835
#813 := (iff #350 #812)
#810 := (iff #291 #809)
#670 := (iff #32 #671)
#672 := [rewrite]: #670
#811 := [monotonicity #672 #755]: #810
#814 := [monotonicity #811]: #813
#839 := [monotonicity #814 #836]: #838
#869 := [monotonicity #839]: #868
#872 := [monotonicity #869]: #871
#677 := (iff #250 #676)
#674 := (iff #33 #673)
#667 := (iff #30 #668)
#669 := [rewrite]: #667
#675 := [monotonicity #669 #672]: #674
#678 := [monotonicity #675]: #677
#875 := [monotonicity #678 #872]: #874
#865 := (iff #458 #818)
#863 := (iff #106 #819)
#864 := [rewrite]: #863
#866 := [monotonicity #864]: #865
#878 := [monotonicity #866 #875]: #877
#881 := [monotonicity #678 #878]: #880
#886 := [trans #881 #884]: #885
#861 := (iff #411 #858)
#840 := (or #366 #837)
#843 := (or #375 #840)
#846 := (or #815 #843)
#849 := (or #393 #846)
#852 := (or #819 #849)
#855 := (or #676 #852)
#859 := (iff #855 #858)
#860 := [rewrite]: #859
#856 := (iff #411 #855)
#853 := (iff #403 #852)
#850 := (iff #394 #849)
#847 := (iff #385 #846)
#844 := (iff #376 #843)
#841 := (iff #367 #840)
#842 := [monotonicity #839]: #841
#845 := [monotonicity #842]: #844
#816 := (iff #384 #815)
#817 := [monotonicity #672]: #816
#848 := [monotonicity #817 #845]: #847
#851 := [monotonicity #848]: #850
#829 := (iff #402 #819)
#824 := (not #818)
#827 := (iff #824 #819)
#828 := [rewrite]: #827
#825 := (iff #402 #824)
#822 := (iff #69 #818)
#823 := [rewrite]: #822
#826 := [monotonicity #823]: #825
#830 := [trans #826 #828]: #829
#854 := [monotonicity #830 #851]: #853
#857 := [monotonicity #678 #854]: #856
#862 := [trans #857 #860]: #861
#889 := [monotonicity #862 #886]: #888
#901 := [monotonicity #678 #889]: #900
#897 := (iff #493 #724)
#892 := (not #727)
#895 := (iff #892 #724)
#896 := [rewrite]: #895
#893 := (iff #493 #892)
#890 := (iff #67 #727)
#891 := [rewrite]: #890
#894 := [monotonicity #891]: #893
#898 := [trans #894 #896]: #897
#904 := [monotonicity #898 #901]: #903
#907 := [monotonicity #678 #904]: #906
#912 := [trans #907 #910]: #911
#751 := (iff #268 #748)
#730 := (or #223 #719)
#733 := (or #232 #730)
#736 := (or #241 #733)
#739 := (or #676 #736)
#742 := (or #727 #739)
#745 := (or #676 #742)
#749 := (iff #745 #748)
#750 := [rewrite]: #749
#746 := (iff #268 #745)
#743 := (iff #260 #742)
#740 := (iff #251 #739)
#737 := (iff #242 #736)
#734 := (iff #233 #733)
#731 := (iff #224 #730)
#720 := (iff #217 #719)
#717 := (iff #212 #716)
#714 := (iff #198 #713)
#711 := (iff #195 #710)
#708 := (iff #54 #707)
#709 := [rewrite]: #708
#689 := (iff #188 #688)
#686 := (iff #50 #685)
#683 := (iff #49 #682)
#684 := [rewrite]: #683
#687 := [monotonicity #640 #684]: #686
#690 := [monotonicity #687]: #689
#712 := [monotonicity #690 #709]: #711
#715 := [quant-intro #712]: #714
#703 := (iff #211 #702)
#700 := (iff #192 #699)
#697 := (iff #189 #694)
#691 := (or #688 #51)
#695 := (iff #691 #694)
#696 := [rewrite]: #695
#692 := (iff #189 #691)
#693 := [monotonicity #690]: #692
#698 := [trans #693 #696]: #697
#701 := [quant-intro #698]: #700
#704 := [monotonicity #701]: #703
#718 := [monotonicity #704 #715]: #717
#721 := [monotonicity #701 #718]: #720
#732 := [monotonicity #721]: #731
#735 := [monotonicity #732]: #734
#738 := [monotonicity #735]: #737
#741 := [monotonicity #678 #738]: #740
#728 := (iff #259 #727)
#725 := (iff #42 #724)
#726 := [rewrite]: #725
#729 := [monotonicity #726]: #728
#744 := [monotonicity #729 #741]: #743
#747 := [monotonicity #678 #744]: #746
#752 := [trans #747 #750]: #751
#915 := [monotonicity #752 #912]: #914
#943 := [monotonicity #678 #915]: #942
#946 := [monotonicity #943]: #945
#939 := (iff #537 #938)
#936 := (iff #173 #935)
#933 := (iff #170 #932)
#930 := (iff #37 #929)
#931 := [rewrite]: #930
#925 := (iff #169 #924)
#922 := (iff #35 #921)
#919 := (iff #34 #918)
#920 := [rewrite]: #919
#923 := [monotonicity #640 #920]: #922
#926 := [monotonicity #923]: #925
#934 := [monotonicity #926 #931]: #933
#937 := [quant-intro #934]: #936
#940 := [monotonicity #937]: #939
#949 := [monotonicity #940 #946]: #948
#952 := [monotonicity #678 #949]: #951
#955 := [monotonicity #952]: #954
#960 := [trans #955 #958]: #959
#963 := [monotonicity #960]: #962
#665 := (iff #573 #664)
#662 := (iff #164 #661)
#659 := (iff #161 #658)
#653 := (iff #25 #654)
#657 := [rewrite]: #653
#650 := (iff #160 #649)
#647 := (iff #23 #646)
#643 := (iff #22 #642)
#645 := [rewrite]: #643
#648 := [monotonicity #640 #645]: #647
#651 := [monotonicity #648]: #650
#660 := [monotonicity #651 #657]: #659
#663 := [quant-intro #660]: #662
#666 := [monotonicity #663]: #665
#966 := [monotonicity #666 #963]: #965
#969 := [monotonicity #663 #966]: #968
#637 := (iff #585 false)
#632 := (not true)
#635 := (iff #632 false)
#636 := [rewrite]: #635
#633 := (iff #585 #632)
#630 := (iff #157 true)
#622 := (and true true)
#625 := (and true #622)
#628 := (iff #625 true)
#629 := [rewrite]: #628
#626 := (iff #157 #625)
#623 := (iff #154 #622)
#620 := (iff #16 true)
#621 := [rewrite]: #620
#618 := (iff #14 true)
#619 := [rewrite]: #618
#624 := [monotonicity #619 #621]: #623
#627 := [monotonicity #619 #624]: #626
#631 := [trans #627 #629]: #630
#634 := [monotonicity #631]: #633
#638 := [trans #634 #636]: #637
#983 := [monotonicity #638 #969]: #982
#986 := [monotonicity #983]: #985
#979 := (iff #602 #970)
#971 := (not #970)
#974 := (not #971)
#977 := (iff #974 #970)
#978 := [rewrite]: #977
#975 := (iff #602 #974)
#972 := (iff #10 #971)
#973 := [rewrite]: #972
#976 := [monotonicity #973]: #975
#980 := [trans #976 #978]: #979
#989 := [monotonicity #980 #986]: #988
#994 := [trans #989 #992]: #993
#997 := [monotonicity #994]: #996
#616 := (iff #134 #615)
#613 := (iff #133 #603)
#608 := (implies true #603)
#611 := (iff #608 #603)
#612 := [rewrite]: #611
#609 := (iff #133 #608)
#606 := (iff #132 #603)
#599 := (implies #10 #594)
#604 := (iff #599 #603)
#605 := [rewrite]: #604
#600 := (iff #132 #599)
#597 := (iff #131 #594)
#591 := (implies #13 #586)
#595 := (iff #591 #594)
#596 := [rewrite]: #595
#592 := (iff #131 #591)
#589 := (iff #130 #586)
#582 := (implies #157 #579)
#587 := (iff #582 #586)
#588 := [rewrite]: #587
#583 := (iff #130 #582)
#580 := (iff #129 #579)
#577 := (iff #128 #574)
#570 := (implies #164 #567)
#575 := (iff #570 #574)
#576 := [rewrite]: #575
#571 := (iff #128 #570)
#568 := (iff #127 #567)
#565 := (iff #126 #562)
#558 := (implies #13 #546)
#563 := (iff #558 #562)
#564 := [rewrite]: #563
#559 := (iff #126 #558)
#556 := (iff #125 #546)
#551 := (implies true #546)
#554 := (iff #551 #546)
#555 := [rewrite]: #554
#552 := (iff #125 #551)
#549 := (iff #124 #546)
#543 := (implies #33 #538)
#547 := (iff #543 #546)
#548 := [rewrite]: #547
#544 := (iff #124 #543)
#541 := (iff #123 #538)
#534 := (implies #173 #529)
#539 := (iff #534 #538)
#540 := [rewrite]: #539
#535 := (iff #123 #534)
#532 := (iff #122 #529)
#525 := (implies #176 #520)
#530 := (iff #525 #529)
#531 := [rewrite]: #530
#526 := (iff #122 #525)
#523 := (iff #121 #520)
#517 := (implies #33 #514)
#521 := (iff #517 #520)
#522 := [rewrite]: #521
#518 := (iff #121 #517)
#515 := (iff #120 #514)
#512 := (iff #119 #502)
#507 := (implies true #502)
#510 := (iff #507 #502)
#511 := [rewrite]: #510
#508 := (iff #119 #507)
#505 := (iff #118 #502)
#499 := (implies #33 #494)
#503 := (iff #499 #502)
#504 := [rewrite]: #503
#500 := (iff #118 #499)
#497 := (iff #117 #494)
#490 := (implies #67 #485)
#495 := (iff #490 #494)
#496 := [rewrite]: #495
#491 := (iff #117 #490)
#488 := (iff #116 #485)
#482 := (implies #33 #479)
#486 := (iff #482 #485)
#487 := [rewrite]: #486
#483 := (iff #116 #482)
#480 := (iff #115 #479)
#477 := (iff #114 #467)
#472 := (implies true #467)
#475 := (iff #472 #467)
#476 := [rewrite]: #475
#473 := (iff #114 #472)
#470 := (iff #113 #467)
#464 := (implies #33 #459)
#468 := (iff #464 #467)
#469 := [rewrite]: #468
#465 := (iff #113 #464)
#462 := (iff #112 #459)
#455 := (implies #106 #450)
#460 := (iff #455 #459)
#461 := [rewrite]: #460
#456 := (iff #112 #455)
#453 := (iff #111 #450)
#447 := (implies #33 #442)
#451 := (iff #447 #450)
#452 := [rewrite]: #451
#448 := (iff #111 #447)
#445 := (iff #110 #442)
#438 := (implies #423 #433)
#443 := (iff #438 #442)
#444 := [rewrite]: #443
#439 := (iff #110 #438)
#436 := (iff #109 #433)
#429 := (implies #426 #351)
#434 := (iff #429 #433)
#435 := [rewrite]: #434
#430 := (iff #109 #429)
#361 := (iff #98 #351)
#356 := (implies true #351)
#359 := (iff #356 #351)
#360 := [rewrite]: #359
#357 := (iff #98 #356)
#354 := (iff #97 #351)
#347 := (implies #291 #342)
#352 := (iff #347 #351)
#353 := [rewrite]: #352
#348 := (iff #97 #347)
#345 := (iff #96 #342)
#338 := (implies #297 #333)
#343 := (iff #338 #342)
#344 := [rewrite]: #343
#339 := (iff #96 #338)
#336 := (iff #95 #333)
#329 := (implies #84 #326)
#334 := (iff #329 #333)
#335 := [rewrite]: #334
#330 := (iff #95 #329)
#327 := (iff #94 #326)
#324 := (iff #93 #321)
#317 := (implies #304 #307)
#322 := (iff #317 #321)
#323 := [rewrite]: #322
#318 := (iff #93 #317)
#315 := (iff #92 #307)
#310 := (and #307 true)
#313 := (iff #310 #307)
#314 := [rewrite]: #313
#311 := (iff #92 #310)
#308 := (iff #91 #307)
#309 := [rewrite]: #308
#312 := [monotonicity #309]: #311
#316 := [trans #312 #314]: #315
#305 := (iff #89 #304)
#302 := (iff #88 #301)
#303 := [rewrite]: #302
#306 := [quant-intro #303]: #305
#319 := [monotonicity #306 #316]: #318
#325 := [trans #319 #323]: #324
#328 := [monotonicity #306 #325]: #327
#331 := [monotonicity #328]: #330
#337 := [trans #331 #335]: #336
#298 := (iff #81 #297)
#295 := (= #80 #294)
#296 := [rewrite]: #295
#299 := [monotonicity #296]: #298
#340 := [monotonicity #299 #337]: #339
#346 := [trans #340 #344]: #345
#292 := (iff #78 #291)
#293 := [rewrite]: #292
#349 := [monotonicity #293 #346]: #348
#355 := [trans #349 #353]: #354
#358 := [monotonicity #355]: #357
#362 := [trans #358 #360]: #361
#427 := (iff #108 #426)
#428 := [rewrite]: #427
#431 := [monotonicity #428 #362]: #430
#437 := [trans #431 #435]: #436
#424 := (iff #107 #423)
#425 := [rewrite]: #424
#440 := [monotonicity #425 #437]: #439
#446 := [trans #440 #444]: #445
#449 := [monotonicity #446]: #448
#454 := [trans #449 #452]: #453
#457 := [monotonicity #454]: #456
#463 := [trans #457 #461]: #462
#466 := [monotonicity #463]: #465
#471 := [trans #466 #469]: #470
#474 := [monotonicity #471]: #473
#478 := [trans #474 #476]: #477
#421 := (iff #105 #411)
#416 := (implies true #411)
#419 := (iff #416 #411)
#420 := [rewrite]: #419
#417 := (iff #105 #416)
#414 := (iff #104 #411)
#408 := (implies #33 #403)
#412 := (iff #408 #411)
#413 := [rewrite]: #412
#409 := (iff #104 #408)
#406 := (iff #103 #403)
#399 := (implies #69 #394)
#404 := (iff #399 #403)
#405 := [rewrite]: #404
#400 := (iff #103 #399)
#397 := (iff #102 #394)
#390 := (implies #280 #385)
#395 := (iff #390 #394)
#396 := [rewrite]: #395
#391 := (iff #102 #390)
#388 := (iff #101 #385)
#381 := (implies #32 #376)
#386 := (iff #381 #385)
#387 := [rewrite]: #386
#382 := (iff #101 #381)
#379 := (iff #100 #376)
#372 := (implies #285 #367)
#377 := (iff #372 #376)
#378 := [rewrite]: #377
#373 := (iff #100 #372)
#370 := (iff #99 #367)
#363 := (implies #288 #351)
#368 := (iff #363 #367)
#369 := [rewrite]: #368
#364 := (iff #99 #363)
#289 := (iff #76 #288)
#290 := [rewrite]: #289
#365 := [monotonicity #290 #362]: #364
#371 := [trans #365 #369]: #370
#286 := (iff #74 #285)
#287 := [rewrite]: #286
#374 := [monotonicity #287 #371]: #373
#380 := [trans #374 #378]: #379
#283 := (iff #72 #32)
#284 := [rewrite]: #283
#383 := [monotonicity #284 #380]: #382
#389 := [trans #383 #387]: #388
#281 := (iff #71 #280)
#282 := [rewrite]: #281
#392 := [monotonicity #282 #389]: #391
#398 := [trans #392 #396]: #397
#401 := [monotonicity #398]: #400
#407 := [trans #401 #405]: #406
#410 := [monotonicity #407]: #409
#415 := [trans #410 #413]: #414
#418 := [monotonicity #415]: #417
#422 := [trans #418 #420]: #421
#481 := [monotonicity #422 #478]: #480
#484 := [monotonicity #481]: #483
#489 := [trans #484 #487]: #488
#492 := [monotonicity #489]: #491
#498 := [trans #492 #496]: #497
#501 := [monotonicity #498]: #500
#506 := [trans #501 #504]: #505
#509 := [monotonicity #506]: #508
#513 := [trans #509 #511]: #512
#278 := (iff #66 #268)
#273 := (implies true #268)
#276 := (iff #273 #268)
#277 := [rewrite]: #276
#274 := (iff #66 #273)
#271 := (iff #65 #268)
#265 := (implies #33 #260)
#269 := (iff #265 #268)
#270 := [rewrite]: #269
#266 := (iff #65 #265)
#263 := (iff #64 #260)
#256 := (implies #42 #251)
#261 := (iff #256 #260)
#262 := [rewrite]: #261
#257 := (iff #64 #256)
#254 := (iff #63 #251)
#247 := (implies #33 #242)
#252 := (iff #247 #251)
#253 := [rewrite]: #252
#248 := (iff #63 #247)
#245 := (iff #62 #242)
#238 := (implies #179 #233)
#243 := (iff #238 #242)
#244 := [rewrite]: #243
#239 := (iff #62 #238)
#236 := (iff #61 #233)
#229 := (implies #182 #224)
#234 := (iff #229 #233)
#235 := [rewrite]: #234
#230 := (iff #61 #229)
#227 := (iff #60 #224)
#220 := (implies #185 #217)
#225 := (iff #220 #224)
#226 := [rewrite]: #225
#221 := (iff #60 #220)
#218 := (iff #59 #217)
#215 := (iff #58 #212)
#208 := (implies #192 #198)
#213 := (iff #208 #212)
#214 := [rewrite]: #213
#209 := (iff #58 #208)
#206 := (iff #57 #198)
#201 := (and #198 true)
#204 := (iff #201 #198)
#205 := [rewrite]: #204
#202 := (iff #57 #201)
#199 := (iff #56 #198)
#196 := (iff #55 #195)
#197 := [rewrite]: #196
#200 := [quant-intro #197]: #199
#203 := [monotonicity #200]: #202
#207 := [trans #203 #205]: #206
#193 := (iff #53 #192)
#190 := (iff #52 #189)
#191 := [rewrite]: #190
#194 := [quant-intro #191]: #193
#210 := [monotonicity #194 #207]: #209
#216 := [trans #210 #214]: #215
#219 := [monotonicity #194 #216]: #218
#186 := (iff #48 #185)
#187 := [rewrite]: #186
#222 := [monotonicity #187 #219]: #221
#228 := [trans #222 #226]: #227
#183 := (iff #46 #182)
#184 := [rewrite]: #183
#231 := [monotonicity #184 #228]: #230
#237 := [trans #231 #235]: #236
#180 := (iff #44 #179)
#181 := [rewrite]: #180
#240 := [monotonicity #181 #237]: #239
#246 := [trans #240 #244]: #245
#249 := [monotonicity #246]: #248
#255 := [trans #249 #253]: #254
#258 := [monotonicity #255]: #257
#264 := [trans #258 #262]: #263
#267 := [monotonicity #264]: #266
#272 := [trans #267 #270]: #271
#275 := [monotonicity #272]: #274
#279 := [trans #275 #277]: #278
#516 := [monotonicity #279 #513]: #515
#519 := [monotonicity #516]: #518
#524 := [trans #519 #522]: #523
#177 := (iff #41 #176)
#178 := [rewrite]: #177
#527 := [monotonicity #178 #524]: #526
#533 := [trans #527 #531]: #532
#174 := (iff #39 #173)
#171 := (iff #38 #170)
#172 := [rewrite]: #171
#175 := [quant-intro #172]: #174
#536 := [monotonicity #175 #533]: #535
#542 := [trans #536 #540]: #541
#545 := [monotonicity #542]: #544
#550 := [trans #545 #548]: #549
#553 := [monotonicity #550]: #552
#557 := [trans #553 #555]: #556
#167 := (iff #28 #13)
#168 := [rewrite]: #167
#560 := [monotonicity #168 #557]: #559
#566 := [trans #560 #564]: #565
#569 := [monotonicity #168 #566]: #568
#165 := (iff #27 #164)
#162 := (iff #26 #161)
#163 := [rewrite]: #162
#166 := [quant-intro #163]: #165
#572 := [monotonicity #166 #569]: #571
#578 := [trans #572 #576]: #577
#581 := [monotonicity #166 #578]: #580
#158 := (iff #19 #157)
#155 := (iff #18 #154)
#152 := (iff #17 #16)
#153 := [rewrite]: #152
#156 := [monotonicity #153]: #155
#159 := [monotonicity #156]: #158
#584 := [monotonicity #159 #581]: #583
#590 := [trans #584 #588]: #589
#593 := [monotonicity #590]: #592
#598 := [trans #593 #596]: #597
#601 := [monotonicity #598]: #600
#607 := [trans #601 #605]: #606
#610 := [monotonicity #607]: #609
#614 := [trans #610 #612]: #613
#617 := [monotonicity #614]: #616
#999 := [trans #617 #997]: #998
#151 := [asserted]: #134
#1000 := [mp #151 #999]: #995
#1001 := [not-or-elim #1000]: #13
#2045 := [trans #1001 #2054]: #2072
#1786 := (not #1007)
#1871 := (or #1432 #1786)
#1872 := [def-axiom]: #1871
#2051 := [unit-resolution #1872 #2073]: #1786
#2050 := (not #2072)
#2019 := (or #2050 #1007)
#2026 := [th-lemma]: #2019
#1985 := [unit-resolution #2026 #2051 #2045]: false
#2016 := [lemma #1985]: #1432
#2289 := (or #1437 #2286)
#1507 := (forall (vars (?v0 int)) #1504)
#1693 := (or #1507 #1690)
#1696 := (not #1693)
#1699 := (or #241 #232 #223 #1569 #815 #727 #1696)
#1702 := (not #1699)
#1596 := (forall (vars (?v0 int)) #1591)
#1602 := (not #1596)
#1603 := (or #307 #1602)
#1604 := (not #1603)
#1632 := (or #1604 #1629)
#1640 := (not #1632)
#1650 := (or #441 #432 #1569 #815 #1638 #1639 #806 #818 #1640)
#1651 := (not #1650)
#1641 := (or #393 #375 #366 #1569 #815 #1638 #1639 #806 #819 #1640)
#1642 := (not #1641)
#1656 := (or #1642 #1651)
#1662 := (not #1656)
#1663 := (or #1569 #815 #724 #1662)
#1664 := (not #1663)
#1708 := (or #1664 #1702)
#1713 := (not #1708)
#1482 := (forall (vars (?v0 int)) #1477)
#1676 := (not #1482)
#1460 := (forall (vars (?v0 int)) #1455)
#1675 := (not #1460)
#1716 := (or #528 #1569 #815 #1675 #1676 #1713)
#1719 := (not #1716)
#1722 := (or #1437 #1719)
#2290 := (iff #1722 #2289)
#2287 := (iff #1719 #2286)
#2284 := (iff #1716 #2283)
#2281 := (iff #1713 #2280)
#2278 := (iff #1708 #2277)
#2275 := (iff #1702 #2274)
#2272 := (iff #1699 #2271)
#2269 := (iff #1696 #2268)
#2266 := (iff #1693 #2265)
#2263 := (iff #1507 #2260)
#2261 := (iff #1504 #1504)
#2262 := [refl]: #2261
#2264 := [quant-intro #2262]: #2263
#2267 := [monotonicity #2264]: #2266
#2270 := [monotonicity #2267]: #2269
#2273 := [monotonicity #2270]: #2272
#2276 := [monotonicity #2273]: #2275
#2258 := (iff #1664 #2257)
#2255 := (iff #1663 #2254)
#2252 := (iff #1662 #2251)
#2249 := (iff #1656 #2248)
#2246 := (iff #1651 #2245)
#2243 := (iff #1650 #2242)
#2234 := (iff #1640 #2233)
#2231 := (iff #1632 #2230)
#2228 := (iff #1604 #2227)
#2225 := (iff #1603 #2224)
#2222 := (iff #1602 #2221)
#2219 := (iff #1596 #2216)
#2217 := (iff #1591 #1591)
#2218 := [refl]: #2217
#2220 := [quant-intro #2218]: #2219
#2223 := [monotonicity #2220]: #2222
#2226 := [monotonicity #2223]: #2225
#2229 := [monotonicity #2226]: #2228
#2232 := [monotonicity #2229]: #2231
#2235 := [monotonicity #2232]: #2234
#2244 := [monotonicity #2235]: #2243
#2247 := [monotonicity #2244]: #2246
#2240 := (iff #1642 #2239)
#2237 := (iff #1641 #2236)
#2238 := [monotonicity #2235]: #2237
#2241 := [monotonicity #2238]: #2240
#2250 := [monotonicity #2241 #2247]: #2249
#2253 := [monotonicity #2250]: #2252
#2256 := [monotonicity #2253]: #2255
#2259 := [monotonicity #2256]: #2258
#2279 := [monotonicity #2259 #2276]: #2278
#2282 := [monotonicity #2279]: #2281
#2214 := (iff #1676 #2213)
#2211 := (iff #1482 #2208)
#2209 := (iff #1477 #1477)
#2210 := [refl]: #2209
#2212 := [quant-intro #2210]: #2211
#2215 := [monotonicity #2212]: #2214
#2206 := (iff #1675 #2205)
#2203 := (iff #1460 #2200)
#2201 := (iff #1455 #1455)
#2202 := [refl]: #2201
#2204 := [quant-intro #2202]: #2203
#2207 := [monotonicity #2204]: #2206
#2285 := [monotonicity #2207 #2215 #2282]: #2284
#2288 := [monotonicity #2285]: #2287
#2291 := [monotonicity #2288]: #2290
#1344 := (and #1160 #1341)
#1347 := (not #1344)
#1363 := (or #1347 #1358)
#1366 := (not #1363)
#1169 := (not #307)
#1179 := (and #1169 #785)
#1372 := (or #1179 #1366)
#1396 := (and #423 #426 #668 #671 #754 #757 #802 #819 #1372)
#1384 := (and #280 #285 #288 #668 #671 #754 #757 #802 #818 #1372)
#1401 := (or #1384 #1396)
#1407 := (and #668 #671 #727 #1401)
#1111 := (not #1110)
#1279 := (and #1111 #1112)
#1282 := (not #1279)
#1298 := (or #1282 #1293)
#1301 := (not #1298)
#1090 := (not #1089)
#1270 := (and #1090 #1091)
#1273 := (not #1270)
#1276 := (or #1267 #1273)
#1304 := (and #1276 #1301)
#1080 := (not #694)
#1083 := (forall (vars (?v0 int)) #1080)
#1307 := (or #1083 #1304)
#1313 := (and #179 #182 #185 #668 #671 #724 #1307)
#1412 := (or #1313 #1407)
#1418 := (and #176 #661 #668 #671 #935 #1412)
#1240 := (and #1048 #1049)
#1243 := (not #1240)
#1249 := (or #1007 #1243)
#1254 := (not #1249)
#1423 := (or #1254 #1418)
#1725 := (iff #1423 #1722)
#1545 := (or #1110 #1530 #1293)
#1557 := (or #1556 #1545)
#1558 := (not #1557)
#1563 := (or #1507 #1558)
#1570 := (not #1563)
#1571 := (or #241 #232 #223 #1569 #815 #727 #1570)
#1572 := (not #1571)
#1669 := (or #1572 #1664)
#1677 := (not #1669)
#1678 := (or #528 #1569 #815 #1675 #1676 #1677)
#1679 := (not #1678)
#1684 := (or #1437 #1679)
#1723 := (iff #1684 #1722)
#1720 := (iff #1679 #1719)
#1717 := (iff #1678 #1716)
#1714 := (iff #1677 #1713)
#1711 := (iff #1669 #1708)
#1705 := (or #1702 #1664)
#1709 := (iff #1705 #1708)
#1710 := [rewrite]: #1709
#1706 := (iff #1669 #1705)
#1703 := (iff #1572 #1702)
#1700 := (iff #1571 #1699)
#1697 := (iff #1570 #1696)
#1694 := (iff #1563 #1693)
#1691 := (iff #1558 #1690)
#1688 := (iff #1557 #1687)
#1689 := [rewrite]: #1688
#1692 := [monotonicity #1689]: #1691
#1695 := [monotonicity #1692]: #1694
#1698 := [monotonicity #1695]: #1697
#1701 := [monotonicity #1698]: #1700
#1704 := [monotonicity #1701]: #1703
#1707 := [monotonicity #1704]: #1706
#1712 := [trans #1707 #1710]: #1711
#1715 := [monotonicity #1712]: #1714
#1718 := [monotonicity #1715]: #1717
#1721 := [monotonicity #1718]: #1720
#1724 := [monotonicity #1721]: #1723
#1685 := (iff #1423 #1684)
#1682 := (iff #1418 #1679)
#1672 := (and #176 #1460 #668 #671 #1482 #1669)
#1680 := (iff #1672 #1679)
#1681 := [rewrite]: #1680
#1673 := (iff #1418 #1672)
#1670 := (iff #1412 #1669)
#1667 := (iff #1407 #1664)
#1659 := (and #668 #671 #727 #1656)
#1665 := (iff #1659 #1664)
#1666 := [rewrite]: #1665
#1660 := (iff #1407 #1659)
#1657 := (iff #1401 #1656)
#1654 := (iff #1396 #1651)
#1647 := (and #423 #426 #668 #671 #754 #757 #802 #819 #1632)
#1652 := (iff #1647 #1651)
#1653 := [rewrite]: #1652
#1648 := (iff #1396 #1647)
#1633 := (iff #1372 #1632)
#1630 := (iff #1366 #1629)
#1627 := (iff #1363 #1624)
#1610 := (or #1609 #1336)
#1621 := (or #1610 #1358)
#1625 := (iff #1621 #1624)
#1626 := [rewrite]: #1625
#1622 := (iff #1363 #1621)
#1619 := (iff #1347 #1610)
#1611 := (not #1610)
#1614 := (not #1611)
#1617 := (iff #1614 #1610)
#1618 := [rewrite]: #1617
#1615 := (iff #1347 #1614)
#1612 := (iff #1344 #1611)
#1613 := [rewrite]: #1612
#1616 := [monotonicity #1613]: #1615
#1620 := [trans #1616 #1618]: #1619
#1623 := [monotonicity #1620]: #1622
#1628 := [trans #1623 #1626]: #1627
#1631 := [monotonicity #1628]: #1630
#1607 := (iff #1179 #1604)
#1599 := (and #1169 #1596)
#1605 := (iff #1599 #1604)
#1606 := [rewrite]: #1605
#1600 := (iff #1179 #1599)
#1597 := (iff #785 #1596)
#1594 := (iff #782 #1591)
#1577 := (or #1440 #765)
#1588 := (or #1577 #779)
#1592 := (iff #1588 #1591)
#1593 := [rewrite]: #1592
#1589 := (iff #782 #1588)
#1586 := (iff #774 #1577)
#1578 := (not #1577)
#1581 := (not #1578)
#1584 := (iff #1581 #1577)
#1585 := [rewrite]: #1584
#1582 := (iff #774 #1581)
#1579 := (iff #771 #1578)
#1580 := [rewrite]: #1579
#1583 := [monotonicity #1580]: #1582
#1587 := [trans #1583 #1585]: #1586
#1590 := [monotonicity #1587]: #1589
#1595 := [trans #1590 #1593]: #1594
#1598 := [quant-intro #1595]: #1597
#1601 := [monotonicity #1598]: #1600
#1608 := [trans #1601 #1606]: #1607
#1634 := [monotonicity #1608 #1631]: #1633
#1649 := [monotonicity #1634]: #1648
#1655 := [trans #1649 #1653]: #1654
#1645 := (iff #1384 #1642)
#1635 := (and #280 #285 #288 #668 #671 #754 #757 #802 #818 #1632)
#1643 := (iff #1635 #1642)
#1644 := [rewrite]: #1643
#1636 := (iff #1384 #1635)
#1637 := [monotonicity #1634]: #1636
#1646 := [trans #1637 #1644]: #1645
#1658 := [monotonicity #1646 #1655]: #1657
#1661 := [monotonicity #1658]: #1660
#1668 := [trans #1661 #1666]: #1667
#1575 := (iff #1313 #1572)
#1566 := (and #179 #182 #185 #668 #671 #724 #1563)
#1573 := (iff #1566 #1572)
#1574 := [rewrite]: #1573
#1567 := (iff #1313 #1566)
#1564 := (iff #1307 #1563)
#1561 := (iff #1304 #1558)
#1550 := (not #1545)
#1553 := (and #1525 #1550)
#1559 := (iff #1553 #1558)
#1560 := [rewrite]: #1559
#1554 := (iff #1304 #1553)
#1551 := (iff #1301 #1550)
#1548 := (iff #1298 #1545)
#1531 := (or #1110 #1530)
#1542 := (or #1531 #1293)
#1546 := (iff #1542 #1545)
#1547 := [rewrite]: #1546
#1543 := (iff #1298 #1542)
#1540 := (iff #1282 #1531)
#1532 := (not #1531)
#1535 := (not #1532)
#1538 := (iff #1535 #1531)
#1539 := [rewrite]: #1538
#1536 := (iff #1282 #1535)
#1533 := (iff #1279 #1532)
#1534 := [rewrite]: #1533
#1537 := [monotonicity #1534]: #1536
#1541 := [trans #1537 #1539]: #1540
#1544 := [monotonicity #1541]: #1543
#1549 := [trans #1544 #1547]: #1548
#1552 := [monotonicity #1549]: #1551
#1528 := (iff #1276 #1525)
#1511 := (or #1089 #1510)
#1522 := (or #1267 #1511)
#1526 := (iff #1522 #1525)
#1527 := [rewrite]: #1526
#1523 := (iff #1276 #1522)
#1520 := (iff #1273 #1511)
#1512 := (not #1511)
#1515 := (not #1512)
#1518 := (iff #1515 #1511)
#1519 := [rewrite]: #1518
#1516 := (iff #1273 #1515)
#1513 := (iff #1270 #1512)
#1514 := [rewrite]: #1513
#1517 := [monotonicity #1514]: #1516
#1521 := [trans #1517 #1519]: #1520
#1524 := [monotonicity #1521]: #1523
#1529 := [trans #1524 #1527]: #1528
#1555 := [monotonicity #1529 #1552]: #1554
#1562 := [trans #1555 #1560]: #1561
#1508 := (iff #1083 #1507)
#1505 := (iff #1080 #1504)
#1502 := (iff #694 #1499)
#1485 := (or #1440 #681)
#1496 := (or #51 #1485)
#1500 := (iff #1496 #1499)
#1501 := [rewrite]: #1500
#1497 := (iff #694 #1496)
#1494 := (iff #688 #1485)
#1486 := (not #1485)
#1489 := (not #1486)
#1492 := (iff #1489 #1485)
#1493 := [rewrite]: #1492
#1490 := (iff #688 #1489)
#1487 := (iff #685 #1486)
#1488 := [rewrite]: #1487
#1491 := [monotonicity #1488]: #1490
#1495 := [trans #1491 #1493]: #1494
#1498 := [monotonicity #1495]: #1497
#1503 := [trans #1498 #1501]: #1502
#1506 := [monotonicity #1503]: #1505
#1509 := [quant-intro #1506]: #1508
#1565 := [monotonicity #1509 #1562]: #1564
#1568 := [monotonicity #1565]: #1567
#1576 := [trans #1568 #1574]: #1575
#1671 := [monotonicity #1576 #1668]: #1670
#1483 := (iff #935 #1482)
#1480 := (iff #932 #1477)
#1463 := (or #1440 #916)
#1474 := (or #1463 #929)
#1478 := (iff #1474 #1477)
#1479 := [rewrite]: #1478
#1475 := (iff #932 #1474)
#1472 := (iff #924 #1463)
#1464 := (not #1463)
#1467 := (not #1464)
#1470 := (iff #1467 #1463)
#1471 := [rewrite]: #1470
#1468 := (iff #924 #1467)
#1465 := (iff #921 #1464)
#1466 := [rewrite]: #1465
#1469 := [monotonicity #1466]: #1468
#1473 := [trans #1469 #1471]: #1472
#1476 := [monotonicity #1473]: #1475
#1481 := [trans #1476 #1479]: #1480
#1484 := [quant-intro #1481]: #1483
#1461 := (iff #661 #1460)
#1458 := (iff #658 #1455)
#1441 := (or #1440 #644)
#1452 := (or #1441 #654)
#1456 := (iff #1452 #1455)
#1457 := [rewrite]: #1456
#1453 := (iff #658 #1452)
#1450 := (iff #649 #1441)
#1442 := (not #1441)
#1445 := (not #1442)
#1448 := (iff #1445 #1441)
#1449 := [rewrite]: #1448
#1446 := (iff #649 #1445)
#1443 := (iff #646 #1442)
#1444 := [rewrite]: #1443
#1447 := [monotonicity #1444]: #1446
#1451 := [trans #1447 #1449]: #1450
#1454 := [monotonicity #1451]: #1453
#1459 := [trans #1454 #1457]: #1458
#1462 := [quant-intro #1459]: #1461
#1674 := [monotonicity #1462 #1484 #1671]: #1673
#1683 := [trans #1674 #1681]: #1682
#1438 := (iff #1254 #1437)
#1435 := (iff #1249 #1432)
#1168 := (or #1005 #1167)
#1429 := (or #1007 #1168)
#1433 := (iff #1429 #1432)
#1434 := [rewrite]: #1433
#1430 := (iff #1249 #1429)
#1427 := (iff #1243 #1168)
#1099 := (not #1168)
#1057 := (not #1099)
#1239 := (iff #1057 #1168)
#1426 := [rewrite]: #1239
#1120 := (iff #1243 #1057)
#1100 := (iff #1240 #1099)
#1056 := [rewrite]: #1100
#1121 := [monotonicity #1056]: #1120
#1428 := [trans #1121 #1426]: #1427
#1431 := [monotonicity #1428]: #1430
#1436 := [trans #1431 #1434]: #1435
#1439 := [monotonicity #1436]: #1438
#1686 := [monotonicity #1439 #1683]: #1685
#1726 := [trans #1686 #1724]: #1725
#1190 := (not #812)
#1187 := (not #806)
#1155 := (+ #1154 #777)
#1156 := (<= #1155 0::int)
#1157 := (+ ?v0!3 #766)
#1158 := (>= #1157 0::int)
#1159 := (not #1158)
#1161 := (and #1160 #1159)
#1162 := (not #1161)
#1163 := (or #1162 #1156)
#1164 := (not #1163)
#1183 := (or #1164 #1179)
#1150 := (not #762)
#1068 := (not #676)
#1202 := (not #432)
#1199 := (not #441)
#1207 := (and #1199 #1202 #1068 #1150 #1183 #1187 #1190 #824)
#1147 := (not #815)
#1144 := (not #366)
#1141 := (not #375)
#1138 := (not #393)
#1195 := (and #1138 #1141 #1144 #1147 #1068 #1150 #1183 #1187 #1190 #818)
#1211 := (or #1195 #1207)
#1215 := (and #1068 #727 #1211)
#1106 := (+ #1105 #705)
#1107 := (<= #1106 0::int)
#1113 := (and #1112 #1111)
#1114 := (not #1113)
#1115 := (or #1114 #1107)
#1116 := (not #1115)
#1092 := (and #1091 #1090)
#1093 := (not #1092)
#1095 := (= #1094 f10)
#1096 := (or #1095 #1093)
#1122 := (and #1096 #1116)
#1126 := (or #1083 #1122)
#1077 := (not #223)
#1074 := (not #232)
#1071 := (not #241)
#1132 := (and #1071 #1074 #1077 #1068 #1126 #892)
#1219 := (or #1132 #1215)
#1058 := (not #528)
#1230 := (and #1058 #661 #1068 #1219 #935)
#1050 := (and #1049 #1048)
#1051 := (not #1050)
#1052 := (or #1051 #1007)
#1053 := (not #1052)
#1234 := (or #1053 #1230)
#1424 := (iff #1234 #1423)
#1421 := (iff #1230 #1418)
#1415 := (and #176 #661 #673 #1412 #935)
#1419 := (iff #1415 #1418)
#1420 := [rewrite]: #1419
#1416 := (iff #1230 #1415)
#1413 := (iff #1219 #1412)
#1410 := (iff #1215 #1407)
#1404 := (and #673 #727 #1401)
#1408 := (iff #1404 #1407)
#1409 := [rewrite]: #1408
#1405 := (iff #1215 #1404)
#1402 := (iff #1211 #1401)
#1399 := (iff #1207 #1396)
#1393 := (and #423 #426 #673 #759 #1372 #802 #809 #819)
#1397 := (iff #1393 #1396)
#1398 := [rewrite]: #1397
#1394 := (iff #1207 #1393)
#1379 := (iff #1190 #809)
#1380 := [rewrite]: #1379
#1377 := (iff #1187 #802)
#1378 := [rewrite]: #1377
#1375 := (iff #1183 #1372)
#1369 := (or #1366 #1179)
#1373 := (iff #1369 #1372)
#1374 := [rewrite]: #1373
#1370 := (iff #1183 #1369)
#1367 := (iff #1164 #1366)
#1364 := (iff #1163 #1363)
#1361 := (iff #1156 #1358)
#1350 := (+ #777 #1154)
#1353 := (<= #1350 0::int)
#1359 := (iff #1353 #1358)
#1360 := [rewrite]: #1359
#1354 := (iff #1156 #1353)
#1351 := (= #1155 #1350)
#1352 := [rewrite]: #1351
#1355 := [monotonicity #1352]: #1354
#1362 := [trans #1355 #1360]: #1361
#1348 := (iff #1162 #1347)
#1345 := (iff #1161 #1344)
#1342 := (iff #1159 #1341)
#1339 := (iff #1158 #1336)
#1328 := (+ #766 ?v0!3)
#1331 := (>= #1328 0::int)
#1337 := (iff #1331 #1336)
#1338 := [rewrite]: #1337
#1332 := (iff #1158 #1331)
#1329 := (= #1157 #1328)
#1330 := [rewrite]: #1329
#1333 := [monotonicity #1330]: #1332
#1340 := [trans #1333 #1338]: #1339
#1343 := [monotonicity #1340]: #1342
#1346 := [monotonicity #1343]: #1345
#1349 := [monotonicity #1346]: #1348
#1365 := [monotonicity #1349 #1362]: #1364
#1368 := [monotonicity #1365]: #1367
#1371 := [monotonicity #1368]: #1370
#1376 := [trans #1371 #1374]: #1375
#1326 := (iff #1150 #759)
#1327 := [rewrite]: #1326
#1259 := (iff #1068 #673)
#1260 := [rewrite]: #1259
#1391 := (iff #1202 #426)
#1392 := [rewrite]: #1391
#1389 := (iff #1199 #423)
#1390 := [rewrite]: #1389
#1395 := [monotonicity #1390 #1392 #1260 #1327 #1376 #1378 #1380 #828]: #1394
#1400 := [trans #1395 #1398]: #1399
#1387 := (iff #1195 #1384)
#1381 := (and #280 #285 #288 #671 #673 #759 #1372 #802 #809 #818)
#1385 := (iff #1381 #1384)
#1386 := [rewrite]: #1385
#1382 := (iff #1195 #1381)
#1324 := (iff #1147 #671)
#1325 := [rewrite]: #1324
#1322 := (iff #1144 #288)
#1323 := [rewrite]: #1322
#1320 := (iff #1141 #285)
#1321 := [rewrite]: #1320
#1318 := (iff #1138 #280)
#1319 := [rewrite]: #1318
#1383 := [monotonicity #1319 #1321 #1323 #1325 #1260 #1327 #1376 #1378 #1380]: #1382
#1388 := [trans #1383 #1386]: #1387
#1403 := [monotonicity #1388 #1400]: #1402
#1406 := [monotonicity #1260 #1403]: #1405
#1411 := [trans #1406 #1409]: #1410
#1316 := (iff #1132 #1313)
#1310 := (and #179 #182 #185 #673 #1307 #724)
#1314 := (iff #1310 #1313)
#1315 := [rewrite]: #1314
#1311 := (iff #1132 #1310)
#1308 := (iff #1126 #1307)
#1305 := (iff #1122 #1304)
#1302 := (iff #1116 #1301)
#1299 := (iff #1115 #1298)
#1296 := (iff #1107 #1293)
#1285 := (+ #705 #1105)
#1288 := (<= #1285 0::int)
#1294 := (iff #1288 #1293)
#1295 := [rewrite]: #1294
#1289 := (iff #1107 #1288)
#1286 := (= #1106 #1285)
#1287 := [rewrite]: #1286
#1290 := [monotonicity #1287]: #1289
#1297 := [trans #1290 #1295]: #1296
#1283 := (iff #1114 #1282)
#1280 := (iff #1113 #1279)
#1281 := [rewrite]: #1280
#1284 := [monotonicity #1281]: #1283
#1300 := [monotonicity #1284 #1297]: #1299
#1303 := [monotonicity #1300]: #1302
#1277 := (iff #1096 #1276)
#1274 := (iff #1093 #1273)
#1271 := (iff #1092 #1270)
#1272 := [rewrite]: #1271
#1275 := [monotonicity #1272]: #1274
#1268 := (iff #1095 #1267)
#1269 := [rewrite]: #1268
#1278 := [monotonicity #1269 #1275]: #1277
#1306 := [monotonicity #1278 #1303]: #1305
#1309 := [monotonicity #1306]: #1308
#1265 := (iff #1077 #185)
#1266 := [rewrite]: #1265
#1263 := (iff #1074 #182)
#1264 := [rewrite]: #1263
#1261 := (iff #1071 #179)
#1262 := [rewrite]: #1261
#1312 := [monotonicity #1262 #1264 #1266 #1260 #1309 #896]: #1311
#1317 := [trans #1312 #1315]: #1316
#1414 := [monotonicity #1317 #1411]: #1413
#1257 := (iff #1058 #176)
#1258 := [rewrite]: #1257
#1417 := [monotonicity #1258 #1260 #1414]: #1416
#1422 := [trans #1417 #1420]: #1421
#1255 := (iff #1053 #1254)
#1252 := (iff #1052 #1249)
#1246 := (or #1243 #1007)
#1250 := (iff #1246 #1249)
#1251 := [rewrite]: #1250
#1247 := (iff #1052 #1246)
#1244 := (iff #1051 #1243)
#1241 := (iff #1050 #1240)
#1242 := [rewrite]: #1241
#1245 := [monotonicity #1242]: #1244
#1248 := [monotonicity #1245]: #1247
#1253 := [trans #1248 #1251]: #1252
#1256 := [monotonicity #1253]: #1255
#1425 := [monotonicity #1256 #1422]: #1424
#1032 := (or #528 #664 #676 #913 #938)
#1037 := (and #661 #1032)
#1040 := (not #1037)
#1235 := (~ #1040 #1234)
#1231 := (not #1032)
#1232 := (~ #1231 #1230)
#1227 := (not #938)
#1228 := (~ #1227 #935)
#1225 := (~ #935 #935)
#1223 := (~ #932 #932)
#1224 := [refl]: #1223
#1226 := [nnf-pos #1224]: #1225
#1229 := [nnf-neg #1226]: #1228
#1220 := (not #913)
#1221 := (~ #1220 #1219)
#1216 := (not #908)
#1217 := (~ #1216 #1215)
#1212 := (not #887)
#1213 := (~ #1212 #1211)
#1208 := (not #882)
#1209 := (~ #1208 #1207)
#1205 := (~ #824 #824)
#1206 := [refl]: #1205
#1191 := (~ #1190 #1190)
#1192 := [refl]: #1191
#1188 := (~ #1187 #1187)
#1189 := [refl]: #1188
#1184 := (not #799)
#1185 := (~ #1184 #1183)
#1180 := (not #794)
#1181 := (~ #1180 #1179)
#1176 := (not #788)
#1177 := (~ #1176 #785)
#1174 := (~ #785 #785)
#1172 := (~ #782 #782)
#1173 := [refl]: #1172
#1175 := [nnf-pos #1173]: #1174
#1178 := [nnf-neg #1175]: #1177
#1170 := (~ #1169 #1169)
#1171 := [refl]: #1170
#1182 := [nnf-neg #1171 #1178]: #1181
#1165 := (~ #788 #1164)
#1166 := [sk]: #1165
#1186 := [nnf-neg #1166 #1182]: #1185
#1151 := (~ #1150 #1150)
#1152 := [refl]: #1151
#1069 := (~ #1068 #1068)
#1070 := [refl]: #1069
#1203 := (~ #1202 #1202)
#1204 := [refl]: #1203
#1200 := (~ #1199 #1199)
#1201 := [refl]: #1200
#1210 := [nnf-neg #1201 #1204 #1070 #1152 #1186 #1189 #1192 #1206]: #1209
#1196 := (not #858)
#1197 := (~ #1196 #1195)
#1193 := (~ #818 #818)
#1194 := [refl]: #1193
#1148 := (~ #1147 #1147)
#1149 := [refl]: #1148
#1145 := (~ #1144 #1144)
#1146 := [refl]: #1145
#1142 := (~ #1141 #1141)
#1143 := [refl]: #1142
#1139 := (~ #1138 #1138)
#1140 := [refl]: #1139
#1198 := [nnf-neg #1140 #1143 #1146 #1149 #1070 #1152 #1186 #1189 #1192 #1194]: #1197
#1214 := [nnf-neg #1198 #1210]: #1213
#1136 := (~ #727 #727)
#1137 := [refl]: #1136
#1218 := [nnf-neg #1070 #1137 #1214]: #1217
#1133 := (not #748)
#1134 := (~ #1133 #1132)
#1130 := (~ #892 #892)
#1131 := [refl]: #1130
#1127 := (not #719)
#1128 := (~ #1127 #1126)
#1123 := (not #716)
#1124 := (~ #1123 #1122)
#1117 := (not #713)
#1118 := (~ #1117 #1116)
#1119 := [sk]: #1118
#1101 := (not #702)
#1102 := (~ #1101 #1096)
#1097 := (~ #699 #1096)
#1098 := [sk]: #1097
#1103 := [nnf-neg #1098]: #1102
#1125 := [nnf-neg #1103 #1119]: #1124
#1084 := (~ #702 #1083)
#1081 := (~ #1080 #1080)
#1082 := [refl]: #1081
#1085 := [nnf-neg #1082]: #1084
#1129 := [nnf-neg #1085 #1125]: #1128
#1078 := (~ #1077 #1077)
#1079 := [refl]: #1078
#1075 := (~ #1074 #1074)
#1076 := [refl]: #1075
#1072 := (~ #1071 #1071)
#1073 := [refl]: #1072
#1135 := [nnf-neg #1073 #1076 #1079 #1070 #1129 #1131]: #1134
#1222 := [nnf-neg #1135 #1218]: #1221
#1065 := (not #664)
#1066 := (~ #1065 #661)
#1063 := (~ #661 #661)
#1061 := (~ #658 #658)
#1062 := [refl]: #1061
#1064 := [nnf-pos #1062]: #1063
#1067 := [nnf-neg #1064]: #1066
#1059 := (~ #1058 #1058)
#1060 := [refl]: #1059
#1233 := [nnf-neg #1060 #1067 #1070 #1222 #1229]: #1232
#1054 := (~ #664 #1053)
#1055 := [sk]: #1054
#1236 := [nnf-neg #1055 #1233]: #1235
#1002 := (not #967)
#1041 := (iff #1002 #1040)
#1038 := (iff #967 #1037)
#1035 := (iff #964 #1032)
#1017 := (or #528 #676 #913 #938)
#1029 := (or #664 #1017)
#1033 := (iff #1029 #1032)
#1034 := [rewrite]: #1033
#1030 := (iff #964 #1029)
#1027 := (iff #961 #1017)
#1022 := (and true #1017)
#1025 := (iff #1022 #1017)
#1026 := [rewrite]: #1025
#1023 := (iff #961 #1022)
#1020 := (iff #956 #1017)
#1014 := (or false #528 #676 #913 #938)
#1018 := (iff #1014 #1017)
#1019 := [rewrite]: #1018
#1015 := (iff #956 #1014)
#1012 := (iff #561 false)
#1010 := (iff #561 #632)
#1008 := (iff #13 true)
#1009 := [iff-true #1001]: #1008
#1011 := [monotonicity #1009]: #1010
#1013 := [trans #1011 #636]: #1012
#1016 := [monotonicity #1013]: #1015
#1021 := [trans #1016 #1019]: #1020
#1024 := [monotonicity #1009 #1021]: #1023
#1028 := [trans #1024 #1026]: #1027
#1031 := [monotonicity #1028]: #1030
#1036 := [trans #1031 #1034]: #1035
#1039 := [monotonicity #1036]: #1038
#1042 := [monotonicity #1039]: #1041
#1003 := [not-or-elim #1000]: #1002
#1043 := [mp #1003 #1042]: #1040
#1237 := [mp~ #1043 #1236]: #1234
#1238 := [mp #1237 #1425]: #1423
#1727 := [mp #1238 #1726]: #1722
#2292 := [mp #1727 #2291]: #2289
#2556 := [unit-resolution #2292 #2016]: #2286
#2111 := (or #2283 #2208)
#2097 := [def-axiom]: #2111
#2557 := [unit-resolution #2097 #2556]: #2208
#2120 := (or #2283 #176)
#2104 := [def-axiom]: #2120
#2620 := [unit-resolution #2104 #2556]: #176
#2352 := (or #2271 #528 #2213)
#1791 := (f5 f9)
#2296 := (= f10 #1791)
#2346 := (= #40 #1791)
#2344 := (= #1791 #40)
#2329 := [hypothesis]: #2274
#2037 := (or #2271 #179)
#2038 := [def-axiom]: #2037
#2340 := [unit-resolution #2038 #2329]: #179
#2341 := [symm #2340]: #44
#2345 := [monotonicity #2341]: #2344
#2347 := [symm #2345]: #2346
#2348 := (= f10 #40)
#2342 := [hypothesis]: #176
#2039 := (or #2271 #182)
#2040 := [def-axiom]: #2039
#2331 := [unit-resolution #2040 #2329]: #182
#2343 := [symm #2331]: #46
#2349 := [trans #2343 #2342]: #2348
#2350 := [trans #2349 #2347]: #2296
#2324 := (not #2296)
#1790 := (>= f9 0::int)
#1788 := (not #1790)
#1800 := (* -1::int f9)
#1787 := (+ f3 #1800)
#1789 := (<= #1787 0::int)
#2302 := (or #1789 #1788 #2296)
#2307 := (not #2302)
#2124 := (or #2271 #2265)
#2125 := [def-axiom]: #2124
#2330 := [unit-resolution #2125 #2329]: #2265
#1958 := (+ f8 #705)
#1959 := (<= #1958 0::int)
#2332 := (or #232 #1959)
#2333 := [th-lemma]: #2332
#2334 := [unit-resolution #2333 #2331]: #1959
#1836 := [hypothesis]: #2208
#2112 := (or #2271 #724)
#2114 := [def-axiom]: #2112
#2335 := [unit-resolution #2114 #2329]: #724
#1867 := (not #1959)
#1846 := (or #1687 #727 #2213 #1867)
#1869 := [hypothesis]: #724
#1948 := (+ f7 #1108)
#1949 := (<= #1948 0::int)
#1927 := (+ f8 #1291)
#1928 := (>= #1927 0::int)
#1866 := (not #1928)
#1860 := [hypothesis]: #1959
#2023 := (not #1293)
#1852 := [hypothesis]: #1690
#2024 := (or #1687 #2023)
#1983 := [def-axiom]: #2024
#1854 := [unit-resolution #1983 #1852]: #2023
#1868 := (or #1866 #1293 #1867)
#1851 := [hypothesis]: #2023
#1864 := [hypothesis]: #1928
#1865 := [th-lemma #1864 #1851 #1860]: false
#1858 := [lemma #1865]: #1868
#1855 := [unit-resolution #1858 #1854 #1860]: #1866
#1841 := (or #1928 #1949)
#2140 := (or #1687 #1112)
#2022 := [def-axiom]: #2140
#1834 := [unit-resolution #2022 #1852]: #1112
#1917 := (or #2213 #1530 #1928 #1949)
#1960 := (+ #1105 #927)
#1950 := (<= #1960 0::int)
#1940 := (+ ?v0!2 #722)
#1942 := (>= #1940 0::int)
#1943 := (or #1530 #1942 #1950)
#1918 := (or #2213 #1943)
#1909 := (iff #1918 #1917)
#1911 := (or #1530 #1928 #1949)
#1912 := (or #2213 #1911)
#1906 := (iff #1912 #1917)
#1907 := [rewrite]: #1906
#1920 := (iff #1918 #1912)
#1915 := (iff #1943 #1911)
#1933 := (or #1530 #1949 #1928)
#1913 := (iff #1933 #1911)
#1914 := [rewrite]: #1913
#1922 := (iff #1943 #1933)
#1931 := (iff #1950 #1928)
#1939 := (+ #927 #1105)
#1924 := (<= #1939 0::int)
#1929 := (iff #1924 #1928)
#1930 := [rewrite]: #1929
#1925 := (iff #1950 #1924)
#1921 := (= #1960 #1939)
#1923 := [rewrite]: #1921
#1926 := [monotonicity #1923]: #1925
#1932 := [trans #1926 #1930]: #1931
#1938 := (iff #1942 #1949)
#1946 := (+ #722 ?v0!2)
#1944 := (>= #1946 0::int)
#1935 := (iff #1944 #1949)
#1937 := [rewrite]: #1935
#1952 := (iff #1942 #1944)
#1947 := (= #1940 #1946)
#1951 := [rewrite]: #1947
#1945 := [monotonicity #1951]: #1952
#1936 := [trans #1945 #1937]: #1938
#1934 := [monotonicity #1936 #1932]: #1922
#1916 := [trans #1934 #1914]: #1915
#1905 := [monotonicity #1916]: #1920
#1908 := [trans #1905 #1907]: #1909
#1919 := [quant-inst]: #1918
#1910 := [mp #1919 #1908]: #1917
#1842 := [unit-resolution #1910 #1836 #1834]: #1841
#1843 := [unit-resolution #1842 #1855]: #1949
#2139 := (or #1687 #1111)
#2137 := [def-axiom]: #2139
#1844 := [unit-resolution #2137 #1852]: #1111
#1845 := [th-lemma #1844 #1843 #1869]: false
#1835 := [lemma #1845]: #1846
#2336 := [unit-resolution #1835 #2335 #1836 #2334]: #1687
#2028 := (or #2268 #2260 #1690)
#2036 := [def-axiom]: #2028
#2337 := [unit-resolution #2036 #2336 #2330]: #2260
#2132 := (not #2260)
#2310 := (or #2132 #2307)
#2293 := (= #1791 f10)
#2294 := (or #2293 #1788 #1789)
#2295 := (not #2294)
#2311 := (or #2132 #2295)
#2313 := (iff #2311 #2310)
#2315 := (iff #2310 #2310)
#2316 := [rewrite]: #2315
#2308 := (iff #2295 #2307)
#2305 := (iff #2294 #2302)
#2299 := (or #2296 #1788 #1789)
#2303 := (iff #2299 #2302)
#2304 := [rewrite]: #2303
#2300 := (iff #2294 #2299)
#2297 := (iff #2293 #2296)
#2298 := [rewrite]: #2297
#2301 := [monotonicity #2298]: #2300
#2306 := [trans #2301 #2304]: #2305
#2309 := [monotonicity #2306]: #2308
#2314 := [monotonicity #2309]: #2313
#2317 := [trans #2314 #2316]: #2313
#2312 := [quant-inst]: #2311
#2318 := [mp #2312 #2317]: #2310
#2338 := [unit-resolution #2318 #2337]: #2307
#2325 := (or #2302 #2324)
#2326 := [def-axiom]: #2325
#2339 := [unit-resolution #2326 #2338]: #2324
#2351 := [unit-resolution #2339 #2350]: false
#2353 := [lemma #2351]: #2352
#2621 := [unit-resolution #2353 #2620 #2557]: #2271
#2098 := (or #2283 #2277)
#2100 := [def-axiom]: #2098
#2622 := [unit-resolution #2100 #2556]: #2277
#2119 := (or #2280 #2257 #2274)
#2113 := [def-axiom]: #2119
#2623 := [unit-resolution #2113 #2622 #2621]: #2257
#2147 := (or #2254 #2248)
#2141 := [def-axiom]: #2147
#2624 := [unit-resolution #2141 #2623]: #2248
#1793 := [hypothesis]: #2239
#2183 := (or #2236 #2230)
#2186 := [def-axiom]: #2183
#2528 := [unit-resolution #2186 #1793]: #2230
#2319 := (or #2236 #307)
#1818 := (= #68 #90)
#1795 := (= #90 #68)
#1838 := (or #2236 #285)
#1839 := [def-axiom]: #1838
#1798 := [unit-resolution #1839 #1793]: #285
#1799 := [symm #1798]: #74
#1817 := [monotonicity #1799]: #1795
#1801 := [symm #1817]: #1818
#1804 := (= f14 #68)
#2174 := (or #2236 #280)
#1837 := [def-axiom]: #2174
#1797 := [unit-resolution #1837 #1793]: #280
#1815 := [symm #1797]: #71
#1840 := (or #2236 #288)
#2176 := [def-axiom]: #1840
#1794 := [unit-resolution #2176 #1793]: #288
#1813 := [symm #1794]: #76
#1805 := [trans #1813 #1815]: #1804
#1808 := [trans #1805 #1801]: #307
#1796 := [hypothesis]: #1169
#1809 := [unit-resolution #1796 #1808]: false
#2320 := [lemma #1809]: #2319
#2529 := [unit-resolution #2320 #1793]: #307
#1856 := (or #2224 #1169)
#2191 := [def-axiom]: #1856
#2530 := [unit-resolution #2191 #2529]: #2224
#2190 := (or #2233 #2227 #1629)
#1833 := [def-axiom]: #2190
#2531 := [unit-resolution #1833 #2530 #2528]: #1629
#2194 := (or #1624 #1341)
#2195 := [def-axiom]: #2194
#2532 := [unit-resolution #2195 #2531]: #1341
#1877 := (>= #803 -1::int)
#2184 := (or #2236 #802)
#1824 := [def-axiom]: #2184
#2533 := [unit-resolution #1824 #1793]: #802
#2534 := (or #806 #1877)
#2535 := [th-lemma]: #2534
#2536 := [unit-resolution #2535 #2533]: #1877
#2562 := (not #2496)
#2525 := (not #2494)
#2495 := (= #90 #1154)
#2499 := (not #2495)
#2502 := (+ #90 #1356)
#2504 := (>= #2502 0::int)
#2509 := (not #2504)
#2196 := (not #1358)
#2197 := (or #1624 #2196)
#2192 := [def-axiom]: #2197
#2537 := [unit-resolution #2192 #2531]: #2196
#2451 := (* -1::int #90)
#2490 := (+ f14 #2451)
#2492 := (>= #2490 0::int)
#2538 := (or #1169 #2492)
#2539 := [th-lemma]: #2538
#2540 := [unit-resolution #2539 #2529]: #2492
#2510 := (not #2492)
#2511 := (or #2509 #2510 #1358)
#2505 := [hypothesis]: #2504
#2506 := [hypothesis]: #2196
#2507 := [hypothesis]: #2492
#2508 := [th-lemma #2507 #2506 #2505]: false
#2512 := [lemma #2508]: #2511
#2541 := [unit-resolution #2512 #2540 #2537]: #2509
#2500 := (or #2499 #2504)
#2501 := [th-lemma]: #2500
#2542 := [unit-resolution #2501 #2541]: #2499
#2526 := (or #2525 #2495 #375)
#2521 := (= #1154 #90)
#2519 := (= ?v0!3 f13)
#2515 := [hypothesis]: #285
#2517 := (= ?v0!3 f7)
#2516 := [hypothesis]: #2494
#2518 := [symm #2516]: #2517
#2520 := [trans #2518 #2515]: #2519
#2522 := [monotonicity #2520]: #2521
#2523 := [symm #2522]: #2495
#2514 := [hypothesis]: #2499
#2524 := [unit-resolution #2514 #2523]: false
#2527 := [lemma #2524]: #2526
#2543 := [unit-resolution #2527 #2542 #1798]: #2525
#2565 := (or #2494 #2562)
#2381 := (<= #2380 0::int)
#2392 := (+ f8 #1356)
#2393 := (>= #2392 0::int)
#2550 := (not #2393)
#1825 := (or #2236 #818)
#2185 := [def-axiom]: #1825
#2544 := [unit-resolution #2185 #1793]: #818
#2366 := (+ #68 #777)
#2367 := (<= #2366 0::int)
#2365 := (= #68 f14)
#2545 := [trans #1797 #1794]: #2365
#2546 := (not #2365)
#2547 := (or #2546 #2367)
#2548 := [th-lemma]: #2547
#2549 := [unit-resolution #2548 #2545]: #2367
#2551 := (not #2367)
#2552 := (or #2550 #1358 #2551 #819)
#2553 := [th-lemma]: #2552
#2554 := [unit-resolution #2553 #2537 #2549 #2544]: #2550
#2558 := (or #2381 #2393)
#1861 := (or #1624 #1160)
#1862 := [def-axiom]: #1861
#2555 := [unit-resolution #1862 #2531]: #1160
#2401 := (or #2213 #1609 #2381 #2393)
#2369 := (+ #1154 #927)
#2370 := (<= #2369 0::int)
#2371 := (+ ?v0!3 #722)
#2372 := (>= #2371 0::int)
#2373 := (or #1609 #2372 #2370)
#2402 := (or #2213 #2373)
#2409 := (iff #2402 #2401)
#2398 := (or #1609 #2381 #2393)
#2404 := (or #2213 #2398)
#2407 := (iff #2404 #2401)
#2408 := [rewrite]: #2407
#2405 := (iff #2402 #2404)
#2399 := (iff #2373 #2398)
#2396 := (iff #2370 #2393)
#2386 := (+ #927 #1154)
#2389 := (<= #2386 0::int)
#2394 := (iff #2389 #2393)
#2395 := [rewrite]: #2394
#2390 := (iff #2370 #2389)
#2387 := (= #2369 #2386)
#2388 := [rewrite]: #2387
#2391 := [monotonicity #2388]: #2390
#2397 := [trans #2391 #2395]: #2396
#2384 := (iff #2372 #2381)
#2374 := (+ #722 ?v0!3)
#2377 := (>= #2374 0::int)
#2382 := (iff #2377 #2381)
#2383 := [rewrite]: #2382
#2378 := (iff #2372 #2377)
#2375 := (= #2371 #2374)
#2376 := [rewrite]: #2375
#2379 := [monotonicity #2376]: #2378
#2385 := [trans #2379 #2383]: #2384
#2400 := [monotonicity #2385 #2397]: #2399
#2406 := [monotonicity #2400]: #2405
#2410 := [trans #2406 #2408]: #2409
#2403 := [quant-inst]: #2402
#2411 := [mp #2403 #2410]: #2401
#2559 := [unit-resolution #2411 #2557 #2555]: #2558
#2560 := [unit-resolution #2559 #2554]: #2381
#2561 := (not #2381)
#2563 := (or #2494 #2561 #2562)
#2564 := [th-lemma]: #2563
#2566 := [unit-resolution #2564 #2560]: #2565
#2567 := [unit-resolution #2566 #2543]: #2562
#2568 := [th-lemma #2567 #2536 #2532]: false
#2569 := [lemma #2568]: #2236
#2153 := (or #2251 #2239 #2245)
#2159 := [def-axiom]: #2153
#2625 := [unit-resolution #2159 #2569 #2624]: #2245
#2165 := (or #2242 #2230)
#2154 := [def-axiom]: #2165
#2626 := [unit-resolution #2154 #2625]: #2230
#2421 := (= #40 #90)
#2631 := (= #90 #40)
#1891 := (or #2242 #423)
#1892 := [def-axiom]: #1891
#2627 := [unit-resolution #1892 #2625]: #423
#2628 := [symm #2627]: #107
#2632 := [monotonicity #2628]: #2631
#2633 := [symm #2632]: #2421
#2634 := (= f14 #40)
#2166 := (or #2242 #426)
#2170 := [def-axiom]: #2166
#2629 := [unit-resolution #2170 #2625]: #426
#2630 := [symm #2629]: #108
#2635 := [trans #2630 #2620]: #2634
#2636 := [trans #2635 #2633]: #307
#2637 := [unit-resolution #2191 #2636]: #2224
#2638 := [unit-resolution #1833 #2637 #2626]: #1629
#2639 := [unit-resolution #2195 #2638]: #1341
#1878 := (or #2242 #802)
#2160 := [def-axiom]: #1878
#2640 := [unit-resolution #2160 #2625]: #802
#2641 := [unit-resolution #2535 #2640]: #1877
#2642 := [hypothesis]: #2562
#2643 := [th-lemma #2642 #2641 #2639]: false
#2644 := [lemma #2643]: #2496
#2649 := [unit-resolution #2192 #2638]: #2196
#1792 := (+ f8 #777)
#2168 := (<= #1792 0::int)
#2650 := (or #432 #2168)
#2651 := [th-lemma]: #2650
#2652 := [unit-resolution #2651 #2629]: #2168
#2653 := (not #2168)
#2654 := (or #2550 #1358 #2653)
#2655 := [th-lemma]: #2654
#2656 := [unit-resolution #2655 #2652 #2649]: #2550
#2657 := [unit-resolution #1862 #2638]: #1160
#2658 := [unit-resolution #2411 #2557 #2657 #2656]: #2381
#2659 := [unit-resolution #2564 #2658]: #2565
#2660 := [unit-resolution #2659 #2644]: #2494
#2661 := [monotonicity #2660]: #2645
#2662 := (not #2645)
#2663 := (or #2662 #2648)
#2664 := [th-lemma]: #2663
#2665 := [unit-resolution #2664 #2661]: #2648
#2164 := (or #2242 #819)
#2161 := [def-axiom]: #2164
#2666 := [unit-resolution #2161 #2625]: #819
[th-lemma #2666 #2649 #2652 #2665]: false
unsat