src/HOL/SMT_Examples/Boogie_Max.certs

added exercise

2fe4278cefdf713c58d9bb38d221cd0a858eee31 2150 0
#2 := false
#7 := 0::Int
decl ?v0!3 :: Int
#1165 := ?v0!3
#688 := -1::Int
#1310 := (* -1::Int ?v0!3)
decl f8 :: Int
#31 := f8
#2386 := (+ f8 #1310)
#2387 := (<= #2386 0::Int)
#2492 := (not #2387)
#2419 := (>= #2386 0::Int)
decl f16 :: Int
#82 := f16
#797 := (* -1::Int f16)
#829 := (+ f8 #797)
#1830 := (>= #829 -1::Int)
#828 := (= #829 -1::Int)
decl f15 :: Int
#78 := f15
decl f5 :: (-> S2 Int Int)
decl f14 :: Int
#76 := f14
decl f6 :: S2
#11 := f6
#93 := (f5 f6 f14)
#94 := (= #93 f15)
#20 := (:var 0 Int)
#24 := (f5 f6 #20)
#2148 := (pattern #24)
#808 := (* -1::Int f15)
#809 := (+ #24 #808)
#810 := (<= #809 0::Int)
#798 := (+ #20 #797)
#796 := (>= #798 0::Int)
#677 := (>= #20 0::Int)
#1413 := (not #677)
#1587 := (or #1413 #796 #810)
#2182 := (forall (vars (?v0 Int)) (:pat #2148) #1587)
#2187 := (not #2182)
#2190 := (or #2187 #94)
#2193 := (not #2190)
#1172 := (f5 f6 ?v0!3)
#1332 := (* -1::Int #1172)
#1333 := (+ f15 #1332)
#1334 := (>= #1333 0::Int)
#1311 := (+ f16 #1310)
#1312 := (<= #1311 0::Int)
#1166 := (>= ?v0!3 0::Int)
#1550 := (not #1166)
#1565 := (or #1550 #1312 #1334)
#1570 := (not #1565)
#2196 := (or #1570 #2193)
#2199 := (not #2196)
#85 := 2::Int
#788 := (>= f16 2::Int)
#1612 := (not #788)
#785 := (>= f14 0::Int)
#1611 := (not #785)
#832 := (not #828)
#15 := 1::Int
#707 := (>= f8 1::Int)
#841 := (not #707)
decl f9 :: Int
#36 := f9
#115 := (= f15 f9)
#453 := (not #115)
decl f7 :: Int
#29 := f7
#114 := (= f14 f7)
#462 := (not #114)
#71 := (f5 f6 f8)
#846 := (* -1::Int #71)
#847 := (+ f9 #846)
#845 := (>= #847 0::Int)
#844 := (not #845)
#704 := (>= f7 0::Int)
#1542 := (not #704)
#2208 := (or #1542 #844 #462 #453 #841 #832 #1611 #1612 #2199)
#2211 := (not #2208)
decl f13 :: Int
#73 := f13
#79 := (= f15 f13)
#386 := (not #79)
#77 := (= f14 f8)
#395 := (not #77)
#74 := (= f13 #71)
#420 := (not #74)
#2202 := (or #1542 #845 #420 #395 #386 #841 #832 #1611 #1612 #2199)
#2205 := (not #2202)
#2214 := (or #2205 #2211)
#2217 := (not #2214)
#753 := (* -1::Int f8)
decl f3 :: Int
#8 := f3
#754 := (+ f3 #753)
#755 := (<= #754 0::Int)
#2220 := (or #1542 #841 #755 #2217)
#2223 := (not #2220)
decl ?v0!2 :: Int
#1110 := ?v0!2
#1118 := (f5 f6 ?v0!2)
#1263 := (* -1::Int #1118)
decl f11 :: Int
#45 := f11
#1264 := (+ f11 #1263)
#1265 := (>= #1264 0::Int)
#1112 := (* -1::Int ?v0!2)
#1113 := (+ f3 #1112)
#1114 := (<= #1113 0::Int)
#1111 := (>= ?v0!2 0::Int)
#1503 := (not #1111)
decl ?v0!1 :: Int
#1092 := ?v0!1
#1100 := (f5 f6 ?v0!1)
#1101 := (= #1100 f11)
#1094 := (* -1::Int ?v0!1)
#1095 := (+ f3 #1094)
#1096 := (<= #1095 0::Int)
#1093 := (>= ?v0!1 0::Int)
#1483 := (not #1093)
#1498 := (or #1483 #1096 #1101)
#1529 := (not #1498)
#1530 := (or #1529 #1503 #1114 #1265)
#1531 := (not #1530)
#51 := (= #24 f11)
#715 := (* -1::Int #20)
#716 := (+ f3 #715)
#717 := (<= #716 0::Int)
#1472 := (or #1413 #717 #51)
#1477 := (not #1472)
#2165 := (forall (vars (?v0 Int)) (:pat #2148) #1477)
#2170 := (or #2165 #1531)
#2173 := (not #2170)
decl f12 :: Int
#47 := f12
#48 := (= f12 f8)
#235 := (not #48)
#46 := (= f11 f9)
#244 := (not #46)
decl f10 :: Int
#43 := f10
#44 := (= f10 f7)
#253 := (not #44)
#758 := (not #755)
#2176 := (or #1542 #841 #758 #253 #244 #235 #2173)
#2179 := (not #2176)
#2226 := (or #2179 #2223)
#2229 := (not #2226)
#40 := (f5 f6 f7)
#41 := (= #40 f9)
#556 := (not #41)
#953 := (* -1::Int f9)
#954 := (+ #24 #953)
#955 := (<= #954 0::Int)
#943 := (+ #20 #753)
#942 := (>= #943 0::Int)
#1450 := (or #1413 #942 #955)
#2157 := (forall (vars (?v0 Int)) (:pat #2148) #1450)
#2162 := (not #2157)
decl f4 :: Int
#10 := f4
#12 := (f5 f6 0::Int)
#28 := (= #12 f4)
#589 := (not #28)
#2232 := (or #589 #1542 #841 #2162 #556 #2229)
#2235 := (not #2232)
#2238 := (or #589 #2235)
#2241 := (not #2238)
#691 := (* -1::Int #24)
#692 := (+ f4 #691)
#690 := (>= #692 0::Int)
#680 := (>= #20 1::Int)
#1428 := (or #1413 #680 #690)
#2149 := (forall (vars (?v0 Int)) (:pat #2148) #1428)
#2154 := (not #2149)
#2244 := (or #2154 #2241)
#2247 := (not #2244)
decl ?v0!0 :: Int
#1040 := ?v0!0
#1034 := (f5 f6 ?v0!0)
#1035 := (* -1::Int #1034)
#1032 := (+ f4 #1035)
#1033 := (>= #1032 0::Int)
#1042 := (>= ?v0!0 1::Int)
#1041 := (>= ?v0!0 0::Int)
#1179 := (not #1041)
#1405 := (or #1179 #1042 #1033)
#1999 := (= f4 #1034)
#1925 := (= #12 #1034)
#1965 := (= #1034 #12)
#1975 := (= ?v0!0 0::Int)
#1043 := (not #1042)
#1410 := (not #1405)
#1998 := [hypothesis]: #1410
#1735 := (or #1405 #1043)
#1820 := [def-axiom]: #1735
#2000 := [unit-resolution #1820 #1998]: #1043
#1734 := (or #1405 #1041)
#1819 := [def-axiom]: #1734
#1968 := [unit-resolution #1819 #1998]: #1041
#1934 := [th-lemma arith eq-propagate 0 0 #1968 #2000]: #1975
#1967 := [monotonicity #1934]: #1965
#1926 := [symm #1967]: #1925
#13 := (= f4 #12)
#799 := (not #796)
#802 := (and #677 #799)
#805 := (not #802)
#813 := (or #805 #810)
#816 := (forall (vars (?v0 Int)) #813)
#819 := (not #816)
#822 := (or #819 #94)
#825 := (and #816 #822)
#790 := (and #785 #788)
#793 := (not #790)
#835 := (and #785 #707)
#838 := (not #835)
#709 := (and #704 #707)
#712 := (not #709)
#908 := (or #712 #844 #462 #453 #838 #832 #793 #825)
#884 := (or #712 #845 #420 #841 #395 #386 #838 #832 #793 #825)
#913 := (and #884 #908)
#934 := (or #712 #755 #913)
#736 := (* -1::Int f11)
#737 := (+ #24 #736)
#738 := (<= #737 0::Int)
#718 := (not #717)
#721 := (and #677 #718)
#724 := (not #721)
#741 := (or #724 #738)
#744 := (forall (vars (?v0 Int)) #741)
#727 := (or #724 #51)
#730 := (exists (vars (?v0 Int)) #727)
#733 := (not #730)
#747 := (or #733 #744)
#750 := (and #730 #747)
#779 := (or #712 #758 #253 #244 #235 #750)
#939 := (and #779 #934)
#944 := (not #942)
#947 := (and #677 #944)
#950 := (not #947)
#958 := (or #950 #955)
#961 := (forall (vars (?v0 Int)) #958)
#964 := (not #961)
#982 := (or #589 #712 #964 #556 #939)
#987 := (and #28 #982)
#678 := (not #680)
#682 := (and #677 #678)
#685 := (not #682)
#694 := (or #685 #690)
#697 := (forall (vars (?v0 Int)) #694)
#700 := (not #697)
#990 := (or #700 #987)
#993 := (and #697 #990)
#622 := (not #13)
#996 := (<= f3 0::Int)
#1016 := (or #996 #622 #993)
#1021 := (not #1016)
#1 := true
#95 := (implies false true)
#96 := (implies #94 #95)
#97 := (and #94 #96)
#90 := (<= #24 f15)
#88 := (< #20 f16)
#21 := (<= 0::Int #20)
#89 := (and #21 #88)
#91 := (implies #89 #90)
#92 := (forall (vars (?v0 Int)) #91)
#98 := (implies #92 #97)
#99 := (and #92 #98)
#100 := (implies true #99)
#86 := (<= 2::Int f16)
#80 := (<= 0::Int f14)
#87 := (and #80 #86)
#101 := (implies #87 #100)
#83 := (+ f8 1::Int)
#84 := (= f16 #83)
#102 := (implies #84 #101)
#32 := (<= 1::Int f8)
#81 := (and #80 #32)
#103 := (implies #81 #102)
#104 := (implies true #103)
#116 := (implies #115 #104)
#117 := (implies #114 #116)
#118 := (implies true #117)
#30 := (<= 0::Int f7)
#33 := (and #30 #32)
#119 := (implies #33 #118)
#113 := (<= #71 f9)
#120 := (implies #113 #119)
#121 := (implies #33 #120)
#122 := (implies true #121)
#105 := (implies #79 #104)
#106 := (implies #77 #105)
#107 := (implies true #106)
#75 := (and #32 #32)
#108 := (implies #75 #107)
#109 := (implies #74 #108)
#72 := (< f9 #71)
#110 := (implies #72 #109)
#111 := (implies #33 #110)
#112 := (implies true #111)
#123 := (and #112 #122)
#124 := (implies #33 #123)
#70 := (< f8 f3)
#125 := (implies #70 #124)
#126 := (implies #33 #125)
#127 := (implies true #126)
#54 := (<= #24 f11)
#49 := (< #20 f3)
#50 := (and #21 #49)
#55 := (implies #50 #54)
#56 := (forall (vars (?v0 Int)) #55)
#57 := (implies #56 true)
#58 := (and #56 #57)
#52 := (implies #50 #51)
#53 := (exists (vars (?v0 Int)) #52)
#59 := (implies #53 #58)
#60 := (and #53 #59)
#61 := (implies true #60)
#62 := (implies #48 #61)
#63 := (implies #46 #62)
#64 := (implies #44 #63)
#65 := (implies true #64)
#66 := (implies #33 #65)
#42 := (<= f3 f8)
#67 := (implies #42 #66)
#68 := (implies #33 #67)
#69 := (implies true #68)
#128 := (and #69 #127)
#129 := (implies #33 #128)
#130 := (implies #41 #129)
#37 := (<= #24 f9)
#34 := (< #20 f8)
#35 := (and #21 #34)
#38 := (implies #35 #37)
#39 := (forall (vars (?v0 Int)) #38)
#131 := (implies #39 #130)
#132 := (implies #33 #131)
#133 := (implies true #132)
#134 := (implies #28 #133)
#135 := (and #28 #134)
#25 := (<= #24 f4)
#22 := (< #20 1::Int)
#23 := (and #21 #22)
#26 := (implies #23 #25)
#27 := (forall (vars (?v0 Int)) #26)
#136 := (implies #27 #135)
#137 := (and #27 #136)
#16 := (<= 1::Int 1::Int)
#17 := (and #16 #16)
#14 := (<= 0::Int 0::Int)
#18 := (and #14 #17)
#19 := (and #14 #18)
#138 := (implies #19 #137)
#139 := (implies #13 #138)
#140 := (implies true #139)
#9 := (< 0::Int f3)
#141 := (implies #9 #140)
#142 := (implies true #141)
#143 := (not #142)
#1024 := (iff #143 #1021)
#307 := (not #89)
#308 := (or #307 #90)
#311 := (forall (vars (?v0 Int)) #308)
#333 := (not #311)
#334 := (or #333 #94)
#339 := (and #311 #334)
#352 := (not #87)
#353 := (or #352 #339)
#301 := (+ 1::Int f8)
#304 := (= f16 #301)
#361 := (not #304)
#362 := (or #361 #353)
#370 := (not #81)
#371 := (or #370 #362)
#454 := (or #453 #371)
#463 := (or #462 #454)
#269 := (not #33)
#478 := (or #269 #463)
#486 := (not #113)
#487 := (or #486 #478)
#495 := (or #269 #487)
#387 := (or #386 #371)
#396 := (or #395 #387)
#411 := (not #32)
#412 := (or #411 #396)
#421 := (or #420 #412)
#429 := (not #72)
#430 := (or #429 #421)
#438 := (or #269 #430)
#507 := (and #438 #495)
#513 := (or #269 #507)
#521 := (not #70)
#522 := (or #521 #513)
#530 := (or #269 #522)
#186 := (not #50)
#193 := (or #186 #54)
#196 := (forall (vars (?v0 Int)) #193)
#187 := (or #186 #51)
#190 := (exists (vars (?v0 Int)) #187)
#216 := (not #190)
#217 := (or #216 #196)
#222 := (and #190 #217)
#236 := (or #235 #222)
#245 := (or #244 #236)
#254 := (or #253 #245)
#270 := (or #269 #254)
#278 := (not #42)
#279 := (or #278 #270)
#287 := (or #269 #279)
#542 := (and #287 #530)
#548 := (or #269 #542)
#557 := (or #556 #548)
#179 := (not #35)
#180 := (or #179 #37)
#183 := (forall (vars (?v0 Int)) #180)
#565 := (not #183)
#566 := (or #565 #557)
#574 := (or #269 #566)
#590 := (or #589 #574)
#595 := (and #28 #590)
#172 := (not #23)
#173 := (or #172 #25)
#176 := (forall (vars (?v0 Int)) #173)
#601 := (not #176)
#602 := (or #601 #595)
#607 := (and #176 #602)
#166 := (and #14 #16)
#169 := (and #14 #166)
#613 := (not #169)
#614 := (or #613 #607)
#623 := (or #622 #614)
#638 := (not #9)
#639 := (or #638 #623)
#651 := (not #639)
#1022 := (iff #651 #1021)
#1019 := (iff #639 #1016)
#1007 := (or false #993)
#1010 := (or #622 #1007)
#1013 := (or #996 #1010)
#1017 := (iff #1013 #1016)
#1018 := [rewrite]: #1017
#1014 := (iff #639 #1013)
#1011 := (iff #623 #1010)
#1008 := (iff #614 #1007)
#994 := (iff #607 #993)
#991 := (iff #602 #990)
#988 := (iff #595 #987)
#985 := (iff #590 #982)
#967 := (or #712 #939)
#970 := (or #556 #967)
#973 := (or #964 #970)
#976 := (or #712 #973)
#979 := (or #589 #976)
#983 := (iff #979 #982)
#984 := [rewrite]: #983
#980 := (iff #590 #979)
#977 := (iff #574 #976)
#974 := (iff #566 #973)
#971 := (iff #557 #970)
#968 := (iff #548 #967)
#940 := (iff #542 #939)
#937 := (iff #530 #934)
#925 := (or #712 #913)
#928 := (or #755 #925)
#931 := (or #712 #928)
#935 := (iff #931 #934)
#936 := [rewrite]: #935
#932 := (iff #530 #931)
#929 := (iff #522 #928)
#926 := (iff #513 #925)
#914 := (iff #507 #913)
#911 := (iff #495 #908)
#857 := (or #793 #825)
#860 := (or #832 #857)
#863 := (or #838 #860)
#893 := (or #453 #863)
#896 := (or #462 #893)
#899 := (or #712 #896)
#902 := (or #844 #899)
#905 := (or #712 #902)
#909 := (iff #905 #908)
#910 := [rewrite]: #909
#906 := (iff #495 #905)
#903 := (iff #487 #902)
#900 := (iff #478 #899)
#897 := (iff #463 #896)
#894 := (iff #454 #893)
#864 := (iff #371 #863)
#861 := (iff #362 #860)
#858 := (iff #353 #857)
#826 := (iff #339 #825)
#823 := (iff #334 #822)
#820 := (iff #333 #819)
#817 := (iff #311 #816)
#814 := (iff #308 #813)
#811 := (iff #90 #810)
#812 := [rewrite]: #811
#806 := (iff #307 #805)
#803 := (iff #89 #802)
#800 := (iff #88 #799)
#801 := [rewrite]: #800
#675 := (iff #21 #677)
#676 := [rewrite]: #675
#804 := [monotonicity #676 #801]: #803
#807 := [monotonicity #804]: #806
#815 := [monotonicity #807 #812]: #814
#818 := [quant-intro #815]: #817
#821 := [monotonicity #818]: #820
#824 := [monotonicity #821]: #823
#827 := [monotonicity #818 #824]: #826
#794 := (iff #352 #793)
#791 := (iff #87 #790)
#787 := (iff #86 #788)
#789 := [rewrite]: #787
#784 := (iff #80 #785)
#786 := [rewrite]: #784
#792 := [monotonicity #786 #789]: #791
#795 := [monotonicity #792]: #794
#859 := [monotonicity #795 #827]: #858
#833 := (iff #361 #832)
#830 := (iff #304 #828)
#831 := [rewrite]: #830
#834 := [monotonicity #831]: #833
#862 := [monotonicity #834 #859]: #861
#839 := (iff #370 #838)
#836 := (iff #81 #835)
#706 := (iff #32 #707)
#708 := [rewrite]: #706
#837 := [monotonicity #786 #708]: #836
#840 := [monotonicity #837]: #839
#865 := [monotonicity #840 #862]: #864
#895 := [monotonicity #865]: #894
#898 := [monotonicity #895]: #897
#713 := (iff #269 #712)
#710 := (iff #33 #709)
#703 := (iff #30 #704)
#705 := [rewrite]: #703
#711 := [monotonicity #705 #708]: #710
#714 := [monotonicity #711]: #713
#901 := [monotonicity #714 #898]: #900
#891 := (iff #486 #844)
#889 := (iff #113 #845)
#890 := [rewrite]: #889
#892 := [monotonicity #890]: #891
#904 := [monotonicity #892 #901]: #903
#907 := [monotonicity #714 #904]: #906
#912 := [trans #907 #910]: #911
#887 := (iff #438 #884)
#866 := (or #386 #863)
#869 := (or #395 #866)
#872 := (or #841 #869)
#875 := (or #420 #872)
#878 := (or #845 #875)
#881 := (or #712 #878)
#885 := (iff #881 #884)
#886 := [rewrite]: #885
#882 := (iff #438 #881)
#879 := (iff #430 #878)
#876 := (iff #421 #875)
#873 := (iff #412 #872)
#870 := (iff #396 #869)
#867 := (iff #387 #866)
#868 := [monotonicity #865]: #867
#871 := [monotonicity #868]: #870
#842 := (iff #411 #841)
#843 := [monotonicity #708]: #842
#874 := [monotonicity #843 #871]: #873
#877 := [monotonicity #874]: #876
#855 := (iff #429 #845)
#850 := (not #844)
#853 := (iff #850 #845)
#854 := [rewrite]: #853
#851 := (iff #429 #850)
#848 := (iff #72 #844)
#849 := [rewrite]: #848
#852 := [monotonicity #849]: #851
#856 := [trans #852 #854]: #855
#880 := [monotonicity #856 #877]: #879
#883 := [monotonicity #714 #880]: #882
#888 := [trans #883 #886]: #887
#915 := [monotonicity #888 #912]: #914
#927 := [monotonicity #714 #915]: #926
#923 := (iff #521 #755)
#918 := (not #758)
#921 := (iff #918 #755)
#922 := [rewrite]: #921
#919 := (iff #521 #918)
#916 := (iff #70 #758)
#917 := [rewrite]: #916
#920 := [monotonicity #917]: #919
#924 := [trans #920 #922]: #923
#930 := [monotonicity #924 #927]: #929
#933 := [monotonicity #714 #930]: #932
#938 := [trans #933 #936]: #937
#782 := (iff #287 #779)
#761 := (or #235 #750)
#764 := (or #244 #761)
#767 := (or #253 #764)
#770 := (or #712 #767)
#773 := (or #758 #770)
#776 := (or #712 #773)
#780 := (iff #776 #779)
#781 := [rewrite]: #780
#777 := (iff #287 #776)
#774 := (iff #279 #773)
#771 := (iff #270 #770)
#768 := (iff #254 #767)
#765 := (iff #245 #764)
#762 := (iff #236 #761)
#751 := (iff #222 #750)
#748 := (iff #217 #747)
#745 := (iff #196 #744)
#742 := (iff #193 #741)
#739 := (iff #54 #738)
#740 := [rewrite]: #739
#725 := (iff #186 #724)
#722 := (iff #50 #721)
#719 := (iff #49 #718)
#720 := [rewrite]: #719
#723 := [monotonicity #676 #720]: #722
#726 := [monotonicity #723]: #725
#743 := [monotonicity #726 #740]: #742
#746 := [quant-intro #743]: #745
#734 := (iff #216 #733)
#731 := (iff #190 #730)
#728 := (iff #187 #727)
#729 := [monotonicity #726]: #728
#732 := [quant-intro #729]: #731
#735 := [monotonicity #732]: #734
#749 := [monotonicity #735 #746]: #748
#752 := [monotonicity #732 #749]: #751
#763 := [monotonicity #752]: #762
#766 := [monotonicity #763]: #765
#769 := [monotonicity #766]: #768
#772 := [monotonicity #714 #769]: #771
#759 := (iff #278 #758)
#756 := (iff #42 #755)
#757 := [rewrite]: #756
#760 := [monotonicity #757]: #759
#775 := [monotonicity #760 #772]: #774
#778 := [monotonicity #714 #775]: #777
#783 := [trans #778 #781]: #782
#941 := [monotonicity #783 #938]: #940
#969 := [monotonicity #714 #941]: #968
#972 := [monotonicity #969]: #971
#965 := (iff #565 #964)
#962 := (iff #183 #961)
#959 := (iff #180 #958)
#956 := (iff #37 #955)
#957 := [rewrite]: #956
#951 := (iff #179 #950)
#948 := (iff #35 #947)
#945 := (iff #34 #944)
#946 := [rewrite]: #945
#949 := [monotonicity #676 #946]: #948
#952 := [monotonicity #949]: #951
#960 := [monotonicity #952 #957]: #959
#963 := [quant-intro #960]: #962
#966 := [monotonicity #963]: #965
#975 := [monotonicity #966 #972]: #974
#978 := [monotonicity #714 #975]: #977
#981 := [monotonicity #978]: #980
#986 := [trans #981 #984]: #985
#989 := [monotonicity #986]: #988
#701 := (iff #601 #700)
#698 := (iff #176 #697)
#695 := (iff #173 #694)
#689 := (iff #25 #690)
#693 := [rewrite]: #689
#686 := (iff #172 #685)
#683 := (iff #23 #682)
#679 := (iff #22 #678)
#681 := [rewrite]: #679
#684 := [monotonicity #676 #681]: #683
#687 := [monotonicity #684]: #686
#696 := [monotonicity #687 #693]: #695
#699 := [quant-intro #696]: #698
#702 := [monotonicity #699]: #701
#992 := [monotonicity #702 #989]: #991
#995 := [monotonicity #699 #992]: #994
#673 := (iff #613 false)
#668 := (not true)
#671 := (iff #668 false)
#672 := [rewrite]: #671
#669 := (iff #613 #668)
#666 := (iff #169 true)
#658 := (and true true)
#661 := (and true #658)
#664 := (iff #661 true)
#665 := [rewrite]: #664
#662 := (iff #169 #661)
#659 := (iff #166 #658)
#656 := (iff #16 true)
#657 := [rewrite]: #656
#654 := (iff #14 true)
#655 := [rewrite]: #654
#660 := [monotonicity #655 #657]: #659
#663 := [monotonicity #655 #660]: #662
#667 := [trans #663 #665]: #666
#670 := [monotonicity #667]: #669
#674 := [trans #670 #672]: #673
#1009 := [monotonicity #674 #995]: #1008
#1012 := [monotonicity #1009]: #1011
#1005 := (iff #638 #996)
#997 := (not #996)
#1000 := (not #997)
#1003 := (iff #1000 #996)
#1004 := [rewrite]: #1003
#1001 := (iff #638 #1000)
#998 := (iff #9 #997)
#999 := [rewrite]: #998
#1002 := [monotonicity #999]: #1001
#1006 := [trans #1002 #1004]: #1005
#1015 := [monotonicity #1006 #1012]: #1014
#1020 := [trans #1015 #1018]: #1019
#1023 := [monotonicity #1020]: #1022
#652 := (iff #143 #651)
#649 := (iff #142 #639)
#644 := (implies true #639)
#647 := (iff #644 #639)
#648 := [rewrite]: #647
#645 := (iff #142 #644)
#642 := (iff #141 #639)
#635 := (implies #9 #623)
#640 := (iff #635 #639)
#641 := [rewrite]: #640
#636 := (iff #141 #635)
#633 := (iff #140 #623)
#628 := (implies true #623)
#631 := (iff #628 #623)
#632 := [rewrite]: #631
#629 := (iff #140 #628)
#626 := (iff #139 #623)
#619 := (implies #13 #614)
#624 := (iff #619 #623)
#625 := [rewrite]: #624
#620 := (iff #139 #619)
#617 := (iff #138 #614)
#610 := (implies #169 #607)
#615 := (iff #610 #614)
#616 := [rewrite]: #615
#611 := (iff #138 #610)
#608 := (iff #137 #607)
#605 := (iff #136 #602)
#598 := (implies #176 #595)
#603 := (iff #598 #602)
#604 := [rewrite]: #603
#599 := (iff #136 #598)
#596 := (iff #135 #595)
#593 := (iff #134 #590)
#586 := (implies #28 #574)
#591 := (iff #586 #590)
#592 := [rewrite]: #591
#587 := (iff #134 #586)
#584 := (iff #133 #574)
#579 := (implies true #574)
#582 := (iff #579 #574)
#583 := [rewrite]: #582
#580 := (iff #133 #579)
#577 := (iff #132 #574)
#571 := (implies #33 #566)
#575 := (iff #571 #574)
#576 := [rewrite]: #575
#572 := (iff #132 #571)
#569 := (iff #131 #566)
#562 := (implies #183 #557)
#567 := (iff #562 #566)
#568 := [rewrite]: #567
#563 := (iff #131 #562)
#560 := (iff #130 #557)
#553 := (implies #41 #548)
#558 := (iff #553 #557)
#559 := [rewrite]: #558
#554 := (iff #130 #553)
#551 := (iff #129 #548)
#545 := (implies #33 #542)
#549 := (iff #545 #548)
#550 := [rewrite]: #549
#546 := (iff #129 #545)
#543 := (iff #128 #542)
#540 := (iff #127 #530)
#535 := (implies true #530)
#538 := (iff #535 #530)
#539 := [rewrite]: #538
#536 := (iff #127 #535)
#533 := (iff #126 #530)
#527 := (implies #33 #522)
#531 := (iff #527 #530)
#532 := [rewrite]: #531
#528 := (iff #126 #527)
#525 := (iff #125 #522)
#518 := (implies #70 #513)
#523 := (iff #518 #522)
#524 := [rewrite]: #523
#519 := (iff #125 #518)
#516 := (iff #124 #513)
#510 := (implies #33 #507)
#514 := (iff #510 #513)
#515 := [rewrite]: #514
#511 := (iff #124 #510)
#508 := (iff #123 #507)
#505 := (iff #122 #495)
#500 := (implies true #495)
#503 := (iff #500 #495)
#504 := [rewrite]: #503
#501 := (iff #122 #500)
#498 := (iff #121 #495)
#492 := (implies #33 #487)
#496 := (iff #492 #495)
#497 := [rewrite]: #496
#493 := (iff #121 #492)
#490 := (iff #120 #487)
#483 := (implies #113 #478)
#488 := (iff #483 #487)
#489 := [rewrite]: #488
#484 := (iff #120 #483)
#481 := (iff #119 #478)
#475 := (implies #33 #463)
#479 := (iff #475 #478)
#480 := [rewrite]: #479
#476 := (iff #119 #475)
#473 := (iff #118 #463)
#468 := (implies true #463)
#471 := (iff #468 #463)
#472 := [rewrite]: #471
#469 := (iff #118 #468)
#466 := (iff #117 #463)
#459 := (implies #114 #454)
#464 := (iff #459 #463)
#465 := [rewrite]: #464
#460 := (iff #117 #459)
#457 := (iff #116 #454)
#450 := (implies #115 #371)
#455 := (iff #450 #454)
#456 := [rewrite]: #455
#451 := (iff #116 #450)
#381 := (iff #104 #371)
#376 := (implies true #371)
#379 := (iff #376 #371)
#380 := [rewrite]: #379
#377 := (iff #104 #376)
#374 := (iff #103 #371)
#367 := (implies #81 #362)
#372 := (iff #367 #371)
#373 := [rewrite]: #372
#368 := (iff #103 #367)
#365 := (iff #102 #362)
#358 := (implies #304 #353)
#363 := (iff #358 #362)
#364 := [rewrite]: #363
#359 := (iff #102 #358)
#356 := (iff #101 #353)
#349 := (implies #87 #339)
#354 := (iff #349 #353)
#355 := [rewrite]: #354
#350 := (iff #101 #349)
#347 := (iff #100 #339)
#342 := (implies true #339)
#345 := (iff #342 #339)
#346 := [rewrite]: #345
#343 := (iff #100 #342)
#340 := (iff #99 #339)
#337 := (iff #98 #334)
#330 := (implies #311 #94)
#335 := (iff #330 #334)
#336 := [rewrite]: #335
#331 := (iff #98 #330)
#328 := (iff #97 #94)
#323 := (and #94 true)
#326 := (iff #323 #94)
#327 := [rewrite]: #326
#324 := (iff #97 #323)
#321 := (iff #96 true)
#316 := (implies #94 true)
#319 := (iff #316 true)
#320 := [rewrite]: #319
#317 := (iff #96 #316)
#314 := (iff #95 true)
#315 := [rewrite]: #314
#318 := [monotonicity #315]: #317
#322 := [trans #318 #320]: #321
#325 := [monotonicity #322]: #324
#329 := [trans #325 #327]: #328
#312 := (iff #92 #311)
#309 := (iff #91 #308)
#310 := [rewrite]: #309
#313 := [quant-intro #310]: #312
#332 := [monotonicity #313 #329]: #331
#338 := [trans #332 #336]: #337
#341 := [monotonicity #313 #338]: #340
#344 := [monotonicity #341]: #343
#348 := [trans #344 #346]: #347
#351 := [monotonicity #348]: #350
#357 := [trans #351 #355]: #356
#305 := (iff #84 #304)
#302 := (= #83 #301)
#303 := [rewrite]: #302
#306 := [monotonicity #303]: #305
#360 := [monotonicity #306 #357]: #359
#366 := [trans #360 #364]: #365
#369 := [monotonicity #366]: #368
#375 := [trans #369 #373]: #374
#378 := [monotonicity #375]: #377
#382 := [trans #378 #380]: #381
#452 := [monotonicity #382]: #451
#458 := [trans #452 #456]: #457
#461 := [monotonicity #458]: #460
#467 := [trans #461 #465]: #466
#470 := [monotonicity #467]: #469
#474 := [trans #470 #472]: #473
#477 := [monotonicity #474]: #476
#482 := [trans #477 #480]: #481
#485 := [monotonicity #482]: #484
#491 := [trans #485 #489]: #490
#494 := [monotonicity #491]: #493
#499 := [trans #494 #497]: #498
#502 := [monotonicity #499]: #501
#506 := [trans #502 #504]: #505
#448 := (iff #112 #438)
#443 := (implies true #438)
#446 := (iff #443 #438)
#447 := [rewrite]: #446
#444 := (iff #112 #443)
#441 := (iff #111 #438)
#435 := (implies #33 #430)
#439 := (iff #435 #438)
#440 := [rewrite]: #439
#436 := (iff #111 #435)
#433 := (iff #110 #430)
#426 := (implies #72 #421)
#431 := (iff #426 #430)
#432 := [rewrite]: #431
#427 := (iff #110 #426)
#424 := (iff #109 #421)
#417 := (implies #74 #412)
#422 := (iff #417 #421)
#423 := [rewrite]: #422
#418 := (iff #109 #417)
#415 := (iff #108 #412)
#408 := (implies #32 #396)
#413 := (iff #408 #412)
#414 := [rewrite]: #413
#409 := (iff #108 #408)
#406 := (iff #107 #396)
#401 := (implies true #396)
#404 := (iff #401 #396)
#405 := [rewrite]: #404
#402 := (iff #107 #401)
#399 := (iff #106 #396)
#392 := (implies #77 #387)
#397 := (iff #392 #396)
#398 := [rewrite]: #397
#393 := (iff #106 #392)
#390 := (iff #105 #387)
#383 := (implies #79 #371)
#388 := (iff #383 #387)
#389 := [rewrite]: #388
#384 := (iff #105 #383)
#385 := [monotonicity #382]: #384
#391 := [trans #385 #389]: #390
#394 := [monotonicity #391]: #393
#400 := [trans #394 #398]: #399
#403 := [monotonicity #400]: #402
#407 := [trans #403 #405]: #406
#299 := (iff #75 #32)
#300 := [rewrite]: #299
#410 := [monotonicity #300 #407]: #409
#416 := [trans #410 #414]: #415
#419 := [monotonicity #416]: #418
#425 := [trans #419 #423]: #424
#428 := [monotonicity #425]: #427
#434 := [trans #428 #432]: #433
#437 := [monotonicity #434]: #436
#442 := [trans #437 #440]: #441
#445 := [monotonicity #442]: #444
#449 := [trans #445 #447]: #448
#509 := [monotonicity #449 #506]: #508
#512 := [monotonicity #509]: #511
#517 := [trans #512 #515]: #516
#520 := [monotonicity #517]: #519
#526 := [trans #520 #524]: #525
#529 := [monotonicity #526]: #528
#534 := [trans #529 #532]: #533
#537 := [monotonicity #534]: #536
#541 := [trans #537 #539]: #540
#297 := (iff #69 #287)
#292 := (implies true #287)
#295 := (iff #292 #287)
#296 := [rewrite]: #295
#293 := (iff #69 #292)
#290 := (iff #68 #287)
#284 := (implies #33 #279)
#288 := (iff #284 #287)
#289 := [rewrite]: #288
#285 := (iff #68 #284)
#282 := (iff #67 #279)
#275 := (implies #42 #270)
#280 := (iff #275 #279)
#281 := [rewrite]: #280
#276 := (iff #67 #275)
#273 := (iff #66 #270)
#266 := (implies #33 #254)
#271 := (iff #266 #270)
#272 := [rewrite]: #271
#267 := (iff #66 #266)
#264 := (iff #65 #254)
#259 := (implies true #254)
#262 := (iff #259 #254)
#263 := [rewrite]: #262
#260 := (iff #65 #259)
#257 := (iff #64 #254)
#250 := (implies #44 #245)
#255 := (iff #250 #254)
#256 := [rewrite]: #255
#251 := (iff #64 #250)
#248 := (iff #63 #245)
#241 := (implies #46 #236)
#246 := (iff #241 #245)
#247 := [rewrite]: #246
#242 := (iff #63 #241)
#239 := (iff #62 #236)
#232 := (implies #48 #222)
#237 := (iff #232 #236)
#238 := [rewrite]: #237
#233 := (iff #62 #232)
#230 := (iff #61 #222)
#225 := (implies true #222)
#228 := (iff #225 #222)
#229 := [rewrite]: #228
#226 := (iff #61 #225)
#223 := (iff #60 #222)
#220 := (iff #59 #217)
#213 := (implies #190 #196)
#218 := (iff #213 #217)
#219 := [rewrite]: #218
#214 := (iff #59 #213)
#211 := (iff #58 #196)
#206 := (and #196 true)
#209 := (iff #206 #196)
#210 := [rewrite]: #209
#207 := (iff #58 #206)
#204 := (iff #57 true)
#199 := (implies #196 true)
#202 := (iff #199 true)
#203 := [rewrite]: #202
#200 := (iff #57 #199)
#197 := (iff #56 #196)
#194 := (iff #55 #193)
#195 := [rewrite]: #194
#198 := [quant-intro #195]: #197
#201 := [monotonicity #198]: #200
#205 := [trans #201 #203]: #204
#208 := [monotonicity #198 #205]: #207
#212 := [trans #208 #210]: #211
#191 := (iff #53 #190)
#188 := (iff #52 #187)
#189 := [rewrite]: #188
#192 := [quant-intro #189]: #191
#215 := [monotonicity #192 #212]: #214
#221 := [trans #215 #219]: #220
#224 := [monotonicity #192 #221]: #223
#227 := [monotonicity #224]: #226
#231 := [trans #227 #229]: #230
#234 := [monotonicity #231]: #233
#240 := [trans #234 #238]: #239
#243 := [monotonicity #240]: #242
#249 := [trans #243 #247]: #248
#252 := [monotonicity #249]: #251
#258 := [trans #252 #256]: #257
#261 := [monotonicity #258]: #260
#265 := [trans #261 #263]: #264
#268 := [monotonicity #265]: #267
#274 := [trans #268 #272]: #273
#277 := [monotonicity #274]: #276
#283 := [trans #277 #281]: #282
#286 := [monotonicity #283]: #285
#291 := [trans #286 #289]: #290
#294 := [monotonicity #291]: #293
#298 := [trans #294 #296]: #297
#544 := [monotonicity #298 #541]: #543
#547 := [monotonicity #544]: #546
#552 := [trans #547 #550]: #551
#555 := [monotonicity #552]: #554
#561 := [trans #555 #559]: #560
#184 := (iff #39 #183)
#181 := (iff #38 #180)
#182 := [rewrite]: #181
#185 := [quant-intro #182]: #184
#564 := [monotonicity #185 #561]: #563
#570 := [trans #564 #568]: #569
#573 := [monotonicity #570]: #572
#578 := [trans #573 #576]: #577
#581 := [monotonicity #578]: #580
#585 := [trans #581 #583]: #584
#588 := [monotonicity #585]: #587
#594 := [trans #588 #592]: #593
#597 := [monotonicity #594]: #596
#177 := (iff #27 #176)
#174 := (iff #26 #173)
#175 := [rewrite]: #174
#178 := [quant-intro #175]: #177
#600 := [monotonicity #178 #597]: #599
#606 := [trans #600 #604]: #605
#609 := [monotonicity #178 #606]: #608
#170 := (iff #19 #169)
#167 := (iff #18 #166)
#164 := (iff #17 #16)
#165 := [rewrite]: #164
#168 := [monotonicity #165]: #167
#171 := [monotonicity #168]: #170
#612 := [monotonicity #171 #609]: #611
#618 := [trans #612 #616]: #617
#621 := [monotonicity #618]: #620
#627 := [trans #621 #625]: #626
#630 := [monotonicity #627]: #629
#634 := [trans #630 #632]: #633
#637 := [monotonicity #634]: #636
#643 := [trans #637 #641]: #642
#646 := [monotonicity #643]: #645
#650 := [trans #646 #648]: #649
#653 := [monotonicity #650]: #652
#1025 := [trans #653 #1023]: #1024
#163 := [asserted]: #143
#1026 := [mp #163 #1025]: #1021
#1028 := [not-or-elim #1026]: #13
#1933 := [trans #1028 #1926]: #1999
#1821 := (not #1033)
#1812 := (or #1405 #1821)
#1823 := [def-axiom]: #1812
#1935 := [unit-resolution #1823 #1998]: #1821
#1936 := (not #1999)
#1964 := (or #1936 #1033)
#1937 := [th-lemma arith triangle-eq]: #1964
#1939 := [unit-resolution #1937 #1935 #1933]: false
#1940 := [lemma #1939]: #1405
#2250 := (or #1410 #2247)
#1592 := (forall (vars (?v0 Int)) #1587)
#1598 := (not #1592)
#1599 := (or #1598 #94)
#1600 := (not #1599)
#1605 := (or #1570 #1600)
#1613 := (not #1605)
#1623 := (or #1542 #844 #462 #453 #841 #832 #1611 #1612 #1613)
#1624 := (not #1623)
#1614 := (or #1542 #845 #420 #395 #386 #841 #832 #1611 #1612 #1613)
#1615 := (not #1614)
#1629 := (or #1615 #1624)
#1635 := (not #1629)
#1636 := (or #1542 #841 #755 #1635)
#1637 := (not #1636)
#1480 := (forall (vars (?v0 Int)) #1477)
#1536 := (or #1480 #1531)
#1543 := (not #1536)
#1544 := (or #1542 #841 #758 #253 #244 #235 #1543)
#1545 := (not #1544)
#1642 := (or #1545 #1637)
#1649 := (not #1642)
#1455 := (forall (vars (?v0 Int)) #1450)
#1648 := (not #1455)
#1650 := (or #589 #1542 #841 #1648 #556 #1649)
#1651 := (not #1650)
#1656 := (or #589 #1651)
#1663 := (not #1656)
#1433 := (forall (vars (?v0 Int)) #1428)
#1662 := (not #1433)
#1664 := (or #1662 #1663)
#1665 := (not #1664)
#1670 := (or #1410 #1665)
#2251 := (iff #1670 #2250)
#2248 := (iff #1665 #2247)
#2245 := (iff #1664 #2244)
#2242 := (iff #1663 #2241)
#2239 := (iff #1656 #2238)
#2236 := (iff #1651 #2235)
#2233 := (iff #1650 #2232)
#2230 := (iff #1649 #2229)
#2227 := (iff #1642 #2226)
#2224 := (iff #1637 #2223)
#2221 := (iff #1636 #2220)
#2218 := (iff #1635 #2217)
#2215 := (iff #1629 #2214)
#2212 := (iff #1624 #2211)
#2209 := (iff #1623 #2208)
#2200 := (iff #1613 #2199)
#2197 := (iff #1605 #2196)
#2194 := (iff #1600 #2193)
#2191 := (iff #1599 #2190)
#2188 := (iff #1598 #2187)
#2185 := (iff #1592 #2182)
#2183 := (iff #1587 #1587)
#2184 := [refl]: #2183
#2186 := [quant-intro #2184]: #2185
#2189 := [monotonicity #2186]: #2188
#2192 := [monotonicity #2189]: #2191
#2195 := [monotonicity #2192]: #2194
#2198 := [monotonicity #2195]: #2197
#2201 := [monotonicity #2198]: #2200
#2210 := [monotonicity #2201]: #2209
#2213 := [monotonicity #2210]: #2212
#2206 := (iff #1615 #2205)
#2203 := (iff #1614 #2202)
#2204 := [monotonicity #2201]: #2203
#2207 := [monotonicity #2204]: #2206
#2216 := [monotonicity #2207 #2213]: #2215
#2219 := [monotonicity #2216]: #2218
#2222 := [monotonicity #2219]: #2221
#2225 := [monotonicity #2222]: #2224
#2180 := (iff #1545 #2179)
#2177 := (iff #1544 #2176)
#2174 := (iff #1543 #2173)
#2171 := (iff #1536 #2170)
#2168 := (iff #1480 #2165)
#2166 := (iff #1477 #1477)
#2167 := [refl]: #2166
#2169 := [quant-intro #2167]: #2168
#2172 := [monotonicity #2169]: #2171
#2175 := [monotonicity #2172]: #2174
#2178 := [monotonicity #2175]: #2177
#2181 := [monotonicity #2178]: #2180
#2228 := [monotonicity #2181 #2225]: #2227
#2231 := [monotonicity #2228]: #2230
#2163 := (iff #1648 #2162)
#2160 := (iff #1455 #2157)
#2158 := (iff #1450 #1450)
#2159 := [refl]: #2158
#2161 := [quant-intro #2159]: #2160
#2164 := [monotonicity #2161]: #2163
#2234 := [monotonicity #2164 #2231]: #2233
#2237 := [monotonicity #2234]: #2236
#2240 := [monotonicity #2237]: #2239
#2243 := [monotonicity #2240]: #2242
#2155 := (iff #1662 #2154)
#2152 := (iff #1433 #2149)
#2150 := (iff #1428 #1428)
#2151 := [refl]: #2150
#2153 := [quant-intro #2151]: #2152
#2156 := [monotonicity #2153]: #2155
#2246 := [monotonicity #2156 #2243]: #2245
#2249 := [monotonicity #2246]: #2248
#2252 := [monotonicity #2249]: #2251
#1188 := (not #94)
#1191 := (and #816 #1188)
#1317 := (not #1312)
#1320 := (and #1166 #1317)
#1323 := (not #1320)
#1339 := (or #1323 #1334)
#1342 := (not #1339)
#1345 := (or #1342 #1191)
#1363 := (and #704 #845 #114 #115 #707 #828 #785 #788 #1345)
#1351 := (and #704 #844 #74 #77 #79 #707 #828 #785 #788 #1345)
#1368 := (or #1351 #1363)
#1374 := (and #704 #707 #758 #1368)
#1115 := (not #1114)
#1116 := (and #1111 #1115)
#1117 := (not #1116)
#1270 := (or #1117 #1265)
#1273 := (not #1270)
#1097 := (not #1096)
#1098 := (and #1093 #1097)
#1099 := (not #1098)
#1102 := (or #1099 #1101)
#1276 := (and #1102 #1273)
#1086 := (not #727)
#1089 := (forall (vars (?v0 Int)) #1086)
#1279 := (or #1089 #1276)
#1285 := (and #704 #707 #755 #44 #46 #48 #1279)
#1379 := (or #1285 #1374)
#1385 := (and #28 #704 #707 #961 #41 #1379)
#1390 := (or #589 #1385)
#1393 := (and #697 #1390)
#1036 := (and #1041 #1043)
#1037 := (not #1036)
#1044 := (or #1037 #1033)
#1045 := (not #1044)
#1396 := (or #1045 #1393)
#1671 := (iff #1396 #1670)
#1668 := (iff #1393 #1665)
#1659 := (and #1433 #1656)
#1666 := (iff #1659 #1665)
#1667 := [rewrite]: #1666
#1660 := (iff #1393 #1659)
#1657 := (iff #1390 #1656)
#1654 := (iff #1385 #1651)
#1645 := (and #28 #704 #707 #1455 #41 #1642)
#1652 := (iff #1645 #1651)
#1653 := [rewrite]: #1652
#1646 := (iff #1385 #1645)
#1643 := (iff #1379 #1642)
#1640 := (iff #1374 #1637)
#1632 := (and #704 #707 #758 #1629)
#1638 := (iff #1632 #1637)
#1639 := [rewrite]: #1638
#1633 := (iff #1374 #1632)
#1630 := (iff #1368 #1629)
#1627 := (iff #1363 #1624)
#1620 := (and #704 #845 #114 #115 #707 #828 #785 #788 #1605)
#1625 := (iff #1620 #1624)
#1626 := [rewrite]: #1625
#1621 := (iff #1363 #1620)
#1606 := (iff #1345 #1605)
#1603 := (iff #1191 #1600)
#1595 := (and #1592 #1188)
#1601 := (iff #1595 #1600)
#1602 := [rewrite]: #1601
#1596 := (iff #1191 #1595)
#1593 := (iff #816 #1592)
#1590 := (iff #813 #1587)
#1573 := (or #1413 #796)
#1584 := (or #1573 #810)
#1588 := (iff #1584 #1587)
#1589 := [rewrite]: #1588
#1585 := (iff #813 #1584)
#1582 := (iff #805 #1573)
#1574 := (not #1573)
#1577 := (not #1574)
#1580 := (iff #1577 #1573)
#1581 := [rewrite]: #1580
#1578 := (iff #805 #1577)
#1575 := (iff #802 #1574)
#1576 := [rewrite]: #1575
#1579 := [monotonicity #1576]: #1578
#1583 := [trans #1579 #1581]: #1582
#1586 := [monotonicity #1583]: #1585
#1591 := [trans #1586 #1589]: #1590
#1594 := [quant-intro #1591]: #1593
#1597 := [monotonicity #1594]: #1596
#1604 := [trans #1597 #1602]: #1603
#1571 := (iff #1342 #1570)
#1568 := (iff #1339 #1565)
#1551 := (or #1550 #1312)
#1562 := (or #1551 #1334)
#1566 := (iff #1562 #1565)
#1567 := [rewrite]: #1566
#1563 := (iff #1339 #1562)
#1560 := (iff #1323 #1551)
#1552 := (not #1551)
#1555 := (not #1552)
#1558 := (iff #1555 #1551)
#1559 := [rewrite]: #1558
#1556 := (iff #1323 #1555)
#1553 := (iff #1320 #1552)
#1554 := [rewrite]: #1553
#1557 := [monotonicity #1554]: #1556
#1561 := [trans #1557 #1559]: #1560
#1564 := [monotonicity #1561]: #1563
#1569 := [trans #1564 #1567]: #1568
#1572 := [monotonicity #1569]: #1571
#1607 := [monotonicity #1572 #1604]: #1606
#1622 := [monotonicity #1607]: #1621
#1628 := [trans #1622 #1626]: #1627
#1618 := (iff #1351 #1615)
#1608 := (and #704 #844 #74 #77 #79 #707 #828 #785 #788 #1605)
#1616 := (iff #1608 #1615)
#1617 := [rewrite]: #1616
#1609 := (iff #1351 #1608)
#1610 := [monotonicity #1607]: #1609
#1619 := [trans #1610 #1617]: #1618
#1631 := [monotonicity #1619 #1628]: #1630
#1634 := [monotonicity #1631]: #1633
#1641 := [trans #1634 #1639]: #1640
#1548 := (iff #1285 #1545)
#1539 := (and #704 #707 #755 #44 #46 #48 #1536)
#1546 := (iff #1539 #1545)
#1547 := [rewrite]: #1546
#1540 := (iff #1285 #1539)
#1537 := (iff #1279 #1536)
#1534 := (iff #1276 #1531)
#1518 := (or #1503 #1114 #1265)
#1523 := (not #1518)
#1526 := (and #1498 #1523)
#1532 := (iff #1526 #1531)
#1533 := [rewrite]: #1532
#1527 := (iff #1276 #1526)
#1524 := (iff #1273 #1523)
#1521 := (iff #1270 #1518)
#1504 := (or #1503 #1114)
#1515 := (or #1504 #1265)
#1519 := (iff #1515 #1518)
#1520 := [rewrite]: #1519
#1516 := (iff #1270 #1515)
#1513 := (iff #1117 #1504)
#1505 := (not #1504)
#1508 := (not #1505)
#1511 := (iff #1508 #1504)
#1512 := [rewrite]: #1511
#1509 := (iff #1117 #1508)
#1506 := (iff #1116 #1505)
#1507 := [rewrite]: #1506
#1510 := [monotonicity #1507]: #1509
#1514 := [trans #1510 #1512]: #1513
#1517 := [monotonicity #1514]: #1516
#1522 := [trans #1517 #1520]: #1521
#1525 := [monotonicity #1522]: #1524
#1501 := (iff #1102 #1498)
#1484 := (or #1483 #1096)
#1495 := (or #1484 #1101)
#1499 := (iff #1495 #1498)
#1500 := [rewrite]: #1499
#1496 := (iff #1102 #1495)
#1493 := (iff #1099 #1484)
#1485 := (not #1484)
#1488 := (not #1485)
#1491 := (iff #1488 #1484)
#1492 := [rewrite]: #1491
#1489 := (iff #1099 #1488)
#1486 := (iff #1098 #1485)
#1487 := [rewrite]: #1486
#1490 := [monotonicity #1487]: #1489
#1494 := [trans #1490 #1492]: #1493
#1497 := [monotonicity #1494]: #1496
#1502 := [trans #1497 #1500]: #1501
#1528 := [monotonicity #1502 #1525]: #1527
#1535 := [trans #1528 #1533]: #1534
#1481 := (iff #1089 #1480)
#1478 := (iff #1086 #1477)
#1475 := (iff #727 #1472)
#1458 := (or #1413 #717)
#1469 := (or #1458 #51)
#1473 := (iff #1469 #1472)
#1474 := [rewrite]: #1473
#1470 := (iff #727 #1469)
#1467 := (iff #724 #1458)
#1459 := (not #1458)
#1462 := (not #1459)
#1465 := (iff #1462 #1458)
#1466 := [rewrite]: #1465
#1463 := (iff #724 #1462)
#1460 := (iff #721 #1459)
#1461 := [rewrite]: #1460
#1464 := [monotonicity #1461]: #1463
#1468 := [trans #1464 #1466]: #1467
#1471 := [monotonicity #1468]: #1470
#1476 := [trans #1471 #1474]: #1475
#1479 := [monotonicity #1476]: #1478
#1482 := [quant-intro #1479]: #1481
#1538 := [monotonicity #1482 #1535]: #1537
#1541 := [monotonicity #1538]: #1540
#1549 := [trans #1541 #1547]: #1548
#1644 := [monotonicity #1549 #1641]: #1643
#1456 := (iff #961 #1455)
#1453 := (iff #958 #1450)
#1436 := (or #1413 #942)
#1447 := (or #1436 #955)
#1451 := (iff #1447 #1450)
#1452 := [rewrite]: #1451
#1448 := (iff #958 #1447)
#1445 := (iff #950 #1436)
#1437 := (not #1436)
#1440 := (not #1437)
#1443 := (iff #1440 #1436)
#1444 := [rewrite]: #1443
#1441 := (iff #950 #1440)
#1438 := (iff #947 #1437)
#1439 := [rewrite]: #1438
#1442 := [monotonicity #1439]: #1441
#1446 := [trans #1442 #1444]: #1445
#1449 := [monotonicity #1446]: #1448
#1454 := [trans #1449 #1452]: #1453
#1457 := [quant-intro #1454]: #1456
#1647 := [monotonicity #1457 #1644]: #1646
#1655 := [trans #1647 #1653]: #1654
#1658 := [monotonicity #1655]: #1657
#1434 := (iff #697 #1433)
#1431 := (iff #694 #1428)
#1414 := (or #1413 #680)
#1425 := (or #1414 #690)
#1429 := (iff #1425 #1428)
#1430 := [rewrite]: #1429
#1426 := (iff #694 #1425)
#1423 := (iff #685 #1414)
#1415 := (not #1414)
#1418 := (not #1415)
#1421 := (iff #1418 #1414)
#1422 := [rewrite]: #1421
#1419 := (iff #685 #1418)
#1416 := (iff #682 #1415)
#1417 := [rewrite]: #1416
#1420 := [monotonicity #1417]: #1419
#1424 := [trans #1420 #1422]: #1423
#1427 := [monotonicity #1424]: #1426
#1432 := [trans #1427 #1430]: #1431
#1435 := [quant-intro #1432]: #1434
#1661 := [monotonicity #1435 #1658]: #1660
#1669 := [trans #1661 #1667]: #1668
#1411 := (iff #1045 #1410)
#1408 := (iff #1044 #1405)
#1180 := (or #1179 #1042)
#1402 := (or #1180 #1033)
#1406 := (iff #1402 #1405)
#1407 := [rewrite]: #1406
#1403 := (iff #1044 #1402)
#1400 := (iff #1037 #1180)
#1126 := (not #1180)
#1049 := (not #1126)
#1244 := (iff #1049 #1180)
#1399 := [rewrite]: #1244
#1105 := (iff #1037 #1049)
#1127 := (iff #1036 #1126)
#1048 := [rewrite]: #1127
#1106 := [monotonicity #1048]: #1105
#1401 := [trans #1106 #1399]: #1400
#1404 := [monotonicity #1401]: #1403
#1409 := [trans #1404 #1407]: #1408
#1412 := [monotonicity #1409]: #1411
#1672 := [monotonicity #1412 #1669]: #1671
#1173 := (+ #1172 #808)
#1174 := (<= #1173 0::Int)
#1167 := (+ ?v0!3 #797)
#1168 := (>= #1167 0::Int)
#1169 := (not #1168)
#1170 := (and #1166 #1169)
#1171 := (not #1170)
#1175 := (or #1171 #1174)
#1176 := (not #1175)
#1195 := (or #1176 #1191)
#1162 := (not #793)
#1159 := (not #832)
#1156 := (not #838)
#1208 := (not #453)
#1205 := (not #462)
#1062 := (not #712)
#1211 := (and #1062 #850 #1205 #1208 #1156 #1159 #1162 #1195)
#1153 := (not #386)
#1150 := (not #395)
#1147 := (not #841)
#1144 := (not #420)
#1199 := (and #1062 #844 #1144 #1147 #1150 #1153 #1156 #1159 #1162 #1195)
#1215 := (or #1199 #1211)
#1219 := (and #1062 #758 #1215)
#1119 := (+ #1118 #736)
#1120 := (<= #1119 0::Int)
#1121 := (or #1117 #1120)
#1122 := (not #1121)
#1128 := (and #1102 #1122)
#1132 := (or #1089 #1128)
#1083 := (not #235)
#1080 := (not #244)
#1077 := (not #253)
#1136 := (and #1062 #918 #1077 #1080 #1083 #1132)
#1223 := (or #1136 #1219)
#1072 := (not #556)
#1059 := (not #589)
#1227 := (and #1059 #1062 #961 #1072 #1223)
#1231 := (or #589 #1227)
#1235 := (and #697 #1231)
#1239 := (or #1045 #1235)
#1397 := (iff #1239 #1396)
#1394 := (iff #1235 #1393)
#1391 := (iff #1231 #1390)
#1388 := (iff #1227 #1385)
#1382 := (and #28 #709 #961 #41 #1379)
#1386 := (iff #1382 #1385)
#1387 := [rewrite]: #1386
#1383 := (iff #1227 #1382)
#1380 := (iff #1223 #1379)
#1377 := (iff #1219 #1374)
#1371 := (and #709 #758 #1368)
#1375 := (iff #1371 #1374)
#1376 := [rewrite]: #1375
#1372 := (iff #1219 #1371)
#1369 := (iff #1215 #1368)
#1366 := (iff #1211 #1363)
#1360 := (and #709 #845 #114 #115 #835 #828 #790 #1345)
#1364 := (iff #1360 #1363)
#1365 := [rewrite]: #1364
#1361 := (iff #1211 #1360)
#1346 := (iff #1195 #1345)
#1343 := (iff #1176 #1342)
#1340 := (iff #1175 #1339)
#1337 := (iff #1174 #1334)
#1326 := (+ #808 #1172)
#1329 := (<= #1326 0::Int)
#1335 := (iff #1329 #1334)
#1336 := [rewrite]: #1335
#1330 := (iff #1174 #1329)
#1327 := (= #1173 #1326)
#1328 := [rewrite]: #1327
#1331 := [monotonicity #1328]: #1330
#1338 := [trans #1331 #1336]: #1337
#1324 := (iff #1171 #1323)
#1321 := (iff #1170 #1320)
#1318 := (iff #1169 #1317)
#1315 := (iff #1168 #1312)
#1304 := (+ #797 ?v0!3)
#1307 := (>= #1304 0::Int)
#1313 := (iff #1307 #1312)
#1314 := [rewrite]: #1313
#1308 := (iff #1168 #1307)
#1305 := (= #1167 #1304)
#1306 := [rewrite]: #1305
#1309 := [monotonicity #1306]: #1308
#1316 := [trans #1309 #1314]: #1315
#1319 := [monotonicity #1316]: #1318
#1322 := [monotonicity #1319]: #1321
#1325 := [monotonicity #1322]: #1324
#1341 := [monotonicity #1325 #1338]: #1340
#1344 := [monotonicity #1341]: #1343
#1347 := [monotonicity #1344]: #1346
#1302 := (iff #1162 #790)
#1303 := [rewrite]: #1302
#1300 := (iff #1159 #828)
#1301 := [rewrite]: #1300
#1298 := (iff #1156 #835)
#1299 := [rewrite]: #1298
#1358 := (iff #1208 #115)
#1359 := [rewrite]: #1358
#1356 := (iff #1205 #114)
#1357 := [rewrite]: #1356
#1247 := (iff #1062 #709)
#1248 := [rewrite]: #1247
#1362 := [monotonicity #1248 #854 #1357 #1359 #1299 #1301 #1303 #1347]: #1361
#1367 := [trans #1362 #1365]: #1366
#1354 := (iff #1199 #1351)
#1348 := (and #709 #844 #74 #707 #77 #79 #835 #828 #790 #1345)
#1352 := (iff #1348 #1351)
#1353 := [rewrite]: #1352
#1349 := (iff #1199 #1348)
#1296 := (iff #1153 #79)
#1297 := [rewrite]: #1296
#1294 := (iff #1150 #77)
#1295 := [rewrite]: #1294
#1292 := (iff #1147 #707)
#1293 := [rewrite]: #1292
#1290 := (iff #1144 #74)
#1291 := [rewrite]: #1290
#1350 := [monotonicity #1248 #1291 #1293 #1295 #1297 #1299 #1301 #1303 #1347]: #1349
#1355 := [trans #1350 #1353]: #1354
#1370 := [monotonicity #1355 #1367]: #1369
#1373 := [monotonicity #1248 #1370]: #1372
#1378 := [trans #1373 #1376]: #1377
#1288 := (iff #1136 #1285)
#1282 := (and #709 #755 #44 #46 #48 #1279)
#1286 := (iff #1282 #1285)
#1287 := [rewrite]: #1286
#1283 := (iff #1136 #1282)
#1280 := (iff #1132 #1279)
#1277 := (iff #1128 #1276)
#1274 := (iff #1122 #1273)
#1271 := (iff #1121 #1270)
#1268 := (iff #1120 #1265)
#1257 := (+ #736 #1118)
#1260 := (<= #1257 0::Int)
#1266 := (iff #1260 #1265)
#1267 := [rewrite]: #1266
#1261 := (iff #1120 #1260)
#1258 := (= #1119 #1257)
#1259 := [rewrite]: #1258
#1262 := [monotonicity #1259]: #1261
#1269 := [trans #1262 #1267]: #1268
#1272 := [monotonicity #1269]: #1271
#1275 := [monotonicity #1272]: #1274
#1278 := [monotonicity #1275]: #1277
#1281 := [monotonicity #1278]: #1280
#1255 := (iff #1083 #48)
#1256 := [rewrite]: #1255
#1253 := (iff #1080 #46)
#1254 := [rewrite]: #1253
#1251 := (iff #1077 #44)
#1252 := [rewrite]: #1251
#1284 := [monotonicity #1248 #922 #1252 #1254 #1256 #1281]: #1283
#1289 := [trans #1284 #1287]: #1288
#1381 := [monotonicity #1289 #1378]: #1380
#1249 := (iff #1072 #41)
#1250 := [rewrite]: #1249
#1245 := (iff #1059 #28)
#1246 := [rewrite]: #1245
#1384 := [monotonicity #1246 #1248 #1250 #1381]: #1383
#1389 := [trans #1384 #1387]: #1388
#1392 := [monotonicity #1389]: #1391
#1395 := [monotonicity #1392]: #1394
#1398 := [monotonicity #1395]: #1397
#1029 := (not #993)
#1240 := (~ #1029 #1239)
#1236 := (not #990)
#1237 := (~ #1236 #1235)
#1232 := (not #987)
#1233 := (~ #1232 #1231)
#1228 := (not #982)
#1229 := (~ #1228 #1227)
#1224 := (not #939)
#1225 := (~ #1224 #1223)
#1220 := (not #934)
#1221 := (~ #1220 #1219)
#1216 := (not #913)
#1217 := (~ #1216 #1215)
#1212 := (not #908)
#1213 := (~ #1212 #1211)
#1196 := (not #825)
#1197 := (~ #1196 #1195)
#1192 := (not #822)
#1193 := (~ #1192 #1191)
#1189 := (~ #1188 #1188)
#1190 := [refl]: #1189
#1185 := (not #819)
#1186 := (~ #1185 #816)
#1183 := (~ #816 #816)
#1181 := (~ #813 #813)
#1182 := [refl]: #1181
#1184 := [nnf-pos #1182]: #1183
#1187 := [nnf-neg #1184]: #1186
#1194 := [nnf-neg #1187 #1190]: #1193
#1177 := (~ #819 #1176)
#1178 := [sk]: #1177
#1198 := [nnf-neg #1178 #1194]: #1197
#1163 := (~ #1162 #1162)
#1164 := [refl]: #1163
#1160 := (~ #1159 #1159)
#1161 := [refl]: #1160
#1157 := (~ #1156 #1156)
#1158 := [refl]: #1157
#1209 := (~ #1208 #1208)
#1210 := [refl]: #1209
#1206 := (~ #1205 #1205)
#1207 := [refl]: #1206
#1203 := (~ #850 #850)
#1204 := [refl]: #1203
#1063 := (~ #1062 #1062)
#1064 := [refl]: #1063
#1214 := [nnf-neg #1064 #1204 #1207 #1210 #1158 #1161 #1164 #1198]: #1213
#1200 := (not #884)
#1201 := (~ #1200 #1199)
#1154 := (~ #1153 #1153)
#1155 := [refl]: #1154
#1151 := (~ #1150 #1150)
#1152 := [refl]: #1151
#1148 := (~ #1147 #1147)
#1149 := [refl]: #1148
#1145 := (~ #1144 #1144)
#1146 := [refl]: #1145
#1142 := (~ #844 #844)
#1143 := [refl]: #1142
#1202 := [nnf-neg #1064 #1143 #1146 #1149 #1152 #1155 #1158 #1161 #1164 #1198]: #1201
#1218 := [nnf-neg #1202 #1214]: #1217
#1140 := (~ #758 #758)
#1141 := [refl]: #1140
#1222 := [nnf-neg #1064 #1141 #1218]: #1221
#1137 := (not #779)
#1138 := (~ #1137 #1136)
#1133 := (not #750)
#1134 := (~ #1133 #1132)
#1129 := (not #747)
#1130 := (~ #1129 #1128)
#1123 := (not #744)
#1124 := (~ #1123 #1122)
#1125 := [sk]: #1124
#1107 := (not #733)
#1108 := (~ #1107 #1102)
#1103 := (~ #730 #1102)
#1104 := [sk]: #1103
#1109 := [nnf-neg #1104]: #1108
#1131 := [nnf-neg #1109 #1125]: #1130
#1090 := (~ #733 #1089)
#1087 := (~ #1086 #1086)
#1088 := [refl]: #1087
#1091 := [nnf-neg #1088]: #1090
#1135 := [nnf-neg #1091 #1131]: #1134
#1084 := (~ #1083 #1083)
#1085 := [refl]: #1084
#1081 := (~ #1080 #1080)
#1082 := [refl]: #1081
#1078 := (~ #1077 #1077)
#1079 := [refl]: #1078
#1075 := (~ #918 #918)
#1076 := [refl]: #1075
#1139 := [nnf-neg #1064 #1076 #1079 #1082 #1085 #1135]: #1138
#1226 := [nnf-neg #1139 #1222]: #1225
#1073 := (~ #1072 #1072)
#1074 := [refl]: #1073
#1069 := (not #964)
#1070 := (~ #1069 #961)
#1067 := (~ #961 #961)
#1065 := (~ #958 #958)
#1066 := [refl]: #1065
#1068 := [nnf-pos #1066]: #1067
#1071 := [nnf-neg #1068]: #1070
#1060 := (~ #1059 #1059)
#1061 := [refl]: #1060
#1230 := [nnf-neg #1061 #1064 #1071 #1074 #1226]: #1229
#1057 := (~ #589 #589)
#1058 := [refl]: #1057
#1234 := [nnf-neg #1058 #1230]: #1233
#1054 := (not #700)
#1055 := (~ #1054 #697)
#1052 := (~ #697 #697)
#1050 := (~ #694 #694)
#1051 := [refl]: #1050
#1053 := [nnf-pos #1051]: #1052
#1056 := [nnf-neg #1053]: #1055
#1238 := [nnf-neg #1056 #1234]: #1237
#1046 := (~ #700 #1045)
#1047 := [sk]: #1046
#1241 := [nnf-neg #1047 #1238]: #1240
#1030 := [not-or-elim #1026]: #1029
#1242 := [mp~ #1030 #1241]: #1239
#1243 := [mp #1242 #1398]: #1396
#1673 := [mp #1243 #1672]: #1670
#2253 := [mp #1673 #2252]: #2250
#1748 := [unit-resolution #2253 #1940]: #2247
#2018 := (or #2244 #2238)
#2019 := [def-axiom]: #2018
#1744 := [unit-resolution #2019 #1748]: #2238
#1740 := (or #2241 #2235)
#1738 := (iff #13 #28)
#1749 := (iff #28 #13)
#1736 := [commutativity]: #1749
#1739 := [symm #1736]: #1738
#1737 := [mp #1028 #1739]: #28
#2017 := (or #2241 #589 #2235)
#2013 := [def-axiom]: #2017
#2254 := [unit-resolution #2013 #1737]: #1740
#2255 := [unit-resolution #2254 #1744]: #2235
#2024 := (or #2232 #2226)
#2026 := [def-axiom]: #2024
#2335 := [unit-resolution #2026 #2255]: #2226
#2293 := [hypothesis]: #2179
#1841 := (or #2176 #2170)
#2115 := [def-axiom]: #1841
#2294 := [unit-resolution #2115 #2293]: #2170
#2130 := (not #2165)
#1741 := (or #2176 #46)
#2117 := [def-axiom]: #1741
#2295 := [unit-resolution #2117 #2293]: #46
#2328 := (or #2130 #244)
#2303 := (= #40 f11)
#2300 := (* -1::Int f7)
#2301 := (+ f3 #2300)
#2302 := (<= #2301 0::Int)
#2304 := (or #1542 #2302 #2303)
#1857 := (= f9 f11)
#2306 := [hypothesis]: #46
#2323 := [symm #2306]: #1857
#2045 := (or #2232 #41)
#2023 := [def-axiom]: #2045
#2307 := [unit-resolution #2023 #2255]: #41
#2324 := [trans #2307 #2323]: #2303
#2318 := (not #2303)
#2319 := (or #2304 #2318)
#2320 := [def-axiom]: #2319
#2325 := [unit-resolution #2320 #2324]: #2304
#2326 := [hypothesis]: #2165
#2305 := (not #2304)
#2308 := (or #2130 #2305)
#2309 := [quant-inst #29]: #2308
#2327 := [unit-resolution #2309 #2326 #2325]: false
#2329 := [lemma #2327]: #2328
#2296 := [unit-resolution #2329 #2295]: #2130
#1774 := (or #2173 #2165 #1531)
#2134 := [def-axiom]: #1774
#2297 := [unit-resolution #2134 #2296 #2294]: #1531
#1787 := (or #1530 #1111)
#1788 := [def-axiom]: #1787
#2298 := [unit-resolution #1788 #2297]: #1111
#1816 := (+ f8 #1112)
#1817 := (<= #1816 0::Int)
#1767 := (not #1817)
#1844 := (or #2176 #755)
#1845 := [def-axiom]: #1844
#2299 := [unit-resolution #1845 #2293]: #755
#1789 := (or #1530 #1115)
#2125 := [def-axiom]: #1789
#2282 := [unit-resolution #2125 #2297]: #1115
#1750 := (or #1767 #758 #1114)
#1763 := [hypothesis]: #1115
#1764 := [hypothesis]: #1817
#1766 := [hypothesis]: #755
#1762 := [th-lemma arith farkas -1 -1 1 #1766 #1764 #1763]: false
#1753 := [lemma #1762]: #1750
#2283 := [unit-resolution #1753 #2282 #2299]: #1767
#1793 := (+ f9 #1263)
#1794 := (>= #1793 0::Int)
#1752 := (not #1794)
#1859 := (+ f9 #736)
#1848 := (<= #1859 0::Int)
#2281 := [symm #2295]: #1857
#2284 := (not #1857)
#2285 := (or #2284 #1848)
#2286 := [th-lemma arith triangle-eq]: #2285
#2287 := [unit-resolution #2286 #2281]: #1848
#2126 := (not #1265)
#2127 := (or #1530 #2126)
#2128 := [def-axiom]: #2127
#2288 := [unit-resolution #2128 #2297]: #2126
#1760 := (not #1848)
#1745 := (or #1752 #1265 #1760)
#1754 := [hypothesis]: #1848
#1757 := [hypothesis]: #2126
#1758 := [hypothesis]: #1794
#1759 := [th-lemma arith farkas -1 1 1 #1758 #1757 #1754]: false
#1742 := [lemma #1759]: #1745
#2289 := [unit-resolution #1742 #2288 #2287]: #1752
#1779 := (or #1503 #1817 #1794)
#1743 := [hypothesis]: #1752
#1746 := [hypothesis]: #1767
#1747 := [hypothesis]: #1111
#2044 := (or #2232 #2157)
#2034 := [def-axiom]: #2044
#2256 := [unit-resolution #2034 #2255]: #2157
#1835 := (or #2162 #1503 #1817 #1794)
#1829 := (+ #1118 #953)
#1839 := (<= #1829 0::Int)
#1843 := (+ ?v0!2 #753)
#1853 := (>= #1843 0::Int)
#1806 := (or #1503 #1853 #1839)
#1836 := (or #2162 #1806)
#1755 := (iff #1836 #1835)
#1775 := (or #2162 #1779)
#1776 := (iff #1775 #1835)
#1751 := [rewrite]: #1776
#1770 := (iff #1836 #1775)
#1780 := (iff #1806 #1779)
#1796 := (iff #1839 #1794)
#1804 := (+ #953 #1118)
#1790 := (<= #1804 0::Int)
#1795 := (iff #1790 #1794)
#1784 := [rewrite]: #1795
#1791 := (iff #1839 #1790)
#1783 := (= #1829 #1804)
#1785 := [rewrite]: #1783
#1792 := [monotonicity #1785]: #1791
#1777 := [trans #1792 #1784]: #1796
#1801 := (iff #1853 #1817)
#1808 := (+ #753 ?v0!2)
#1813 := (>= #1808 0::Int)
#1807 := (iff #1813 #1817)
#1818 := [rewrite]: #1807
#1814 := (iff #1853 #1813)
#1809 := (= #1843 #1808)
#1800 := [rewrite]: #1809
#1815 := [monotonicity #1800]: #1814
#1803 := [trans #1815 #1818]: #1801
#1778 := [monotonicity #1803 #1777]: #1780
#1781 := [monotonicity #1778]: #1770
#1756 := [trans #1781 #1751]: #1755
#1772 := [quant-inst #1110]: #1836
#1761 := [mp #1772 #1756]: #1835
#2257 := [unit-resolution #1761 #2256 #1747 #1746 #1743]: false
#2258 := [lemma #2257]: #1779
#2313 := [unit-resolution #2258 #2289 #2283 #2298]: false
#2314 := [lemma #2313]: #2176
#2036 := (or #2229 #2179 #2223)
#2037 := [def-axiom]: #2036
#2333 := [unit-resolution #2037 #2314 #2335]: #2223
#2049 := (or #2220 #2214)
#2050 := [def-axiom]: #2049
#2499 := [unit-resolution #2050 #2333]: #2214
#2420 := (= #71 #1172)
#2434 := (not #2420)
#2421 := (+ #71 #1332)
#2423 := (>= #2421 0::Int)
#2428 := (not #2423)
#2322 := (+ #71 #808)
#2290 := (<= #2322 0::Int)
#2321 := (= #71 f15)
#2455 := (= f13 f15)
#2450 := [hypothesis]: #2205
#1931 := (or #2202 #79)
#2084 := [def-axiom]: #1931
#2451 := [unit-resolution #2084 #2450]: #79
#2456 := [symm #2451]: #2455
#2453 := (= #71 f13)
#2092 := (or #2202 #74)
#2099 := [def-axiom]: #2092
#2452 := [unit-resolution #2099 #2450]: #74
#2454 := [symm #2452]: #2453
#2457 := [trans #2454 #2456]: #2321
#2458 := (not #2321)
#2459 := (or #2458 #2290)
#2460 := [th-lemma arith triangle-eq]: #2459
#2461 := [unit-resolution #2460 #2457]: #2290
#2112 := (not #1334)
#1932 := (or #2202 #2196)
#2080 := [def-axiom]: #1932
#2462 := [unit-resolution #2080 #2450]: #2196
#2466 := (= #93 f13)
#2464 := (= #93 #71)
#1928 := (or #2202 #77)
#1930 := [def-axiom]: #1928
#2463 := [unit-resolution #1930 #2450]: #77
#2465 := [monotonicity #2463]: #2464
#2467 := [trans #2465 #2454]: #2466
#2468 := [trans #2467 #2456]: #94
#2104 := (or #2190 #1188)
#2100 := [def-axiom]: #2104
#2469 := [unit-resolution #2100 #2468]: #2190
#2095 := (or #2199 #1570 #2193)
#2096 := [def-axiom]: #2095
#2470 := [unit-resolution #2096 #2469 #2462]: #1570
#1827 := (or #1565 #2112)
#2109 := [def-axiom]: #1827
#2471 := [unit-resolution #2109 #2470]: #2112
#2429 := (not #2290)
#2430 := (or #2428 #1334 #2429)
#2424 := [hypothesis]: #2423
#2425 := [hypothesis]: #2290
#2426 := [hypothesis]: #2112
#2427 := [th-lemma arith farkas -1 -1 1 #2426 #2425 #2424]: false
#2431 := [lemma #2427]: #2430
#2472 := [unit-resolution #2431 #2471 #2461]: #2428
#2435 := (or #2434 #2423)
#2436 := [th-lemma arith triangle-eq]: #2435
#2473 := [unit-resolution #2436 #2472]: #2434
#2422 := (= f8 ?v0!3)
#2088 := (or #2202 #828)
#2086 := [def-axiom]: #2088
#2474 := [unit-resolution #2086 #2450]: #828
#2475 := (or #832 #1830)
#2476 := [th-lemma arith triangle-eq]: #2475
#2477 := [unit-resolution #2476 #2474]: #1830
#1833 := (or #1565 #1317)
#2111 := [def-axiom]: #1833
#2478 := [unit-resolution #2111 #2470]: #1317
#2479 := (not #1830)
#2480 := (or #2419 #1312 #2479)
#2481 := [th-lemma arith assign-bounds 1 1]: #2480
#2482 := [unit-resolution #2481 #2478 #2477]: #2419
#2398 := (+ f9 #1332)
#2399 := (>= #2398 0::Int)
#2484 := (not #2399)
#2097 := (or #2202 #844)
#2098 := [def-axiom]: #2097
#2483 := [unit-resolution #2098 #2450]: #844
#2485 := (or #2484 #1334 #2429 #845)
#2486 := [th-lemma arith assign-bounds 1 1 1]: #2485
#2487 := [unit-resolution #2486 #2471 #2461 #2483]: #2484
#2489 := (or #2387 #2399)
#1831 := (or #1565 #1166)
#1832 := [def-axiom]: #1831
#2488 := [unit-resolution #1832 #2470]: #1166
#2407 := (or #2162 #1550 #2387 #2399)
#2377 := (+ #1172 #953)
#2378 := (<= #2377 0::Int)
#2369 := (+ ?v0!3 #753)
#2370 := (>= #2369 0::Int)
#2379 := (or #1550 #2370 #2378)
#2408 := (or #2162 #2379)
#2415 := (iff #2408 #2407)
#2404 := (or #1550 #2387 #2399)
#2410 := (or #2162 #2404)
#2413 := (iff #2410 #2407)
#2414 := [rewrite]: #2413
#2411 := (iff #2408 #2410)
#2405 := (iff #2379 #2404)
#2402 := (iff #2378 #2399)
#2392 := (+ #953 #1172)
#2395 := (<= #2392 0::Int)
#2400 := (iff #2395 #2399)
#2401 := [rewrite]: #2400
#2396 := (iff #2378 #2395)
#2393 := (= #2377 #2392)
#2394 := [rewrite]: #2393
#2397 := [monotonicity #2394]: #2396
#2403 := [trans #2397 #2401]: #2402
#2390 := (iff #2370 #2387)
#2380 := (+ #753 ?v0!3)
#2383 := (>= #2380 0::Int)
#2388 := (iff #2383 #2387)
#2389 := [rewrite]: #2388
#2384 := (iff #2370 #2383)
#2381 := (= #2369 #2380)
#2382 := [rewrite]: #2381
#2385 := [monotonicity #2382]: #2384
#2391 := [trans #2385 #2389]: #2390
#2406 := [monotonicity #2391 #2403]: #2405
#2412 := [monotonicity #2406]: #2411
#2416 := [trans #2412 #2414]: #2415
#2409 := [quant-inst #1165]: #2408
#2417 := [mp #2409 #2416]: #2407
#2490 := [unit-resolution #2417 #2256 #2488]: #2489
#2491 := [unit-resolution #2490 #2487]: #2387
#2493 := (not #2419)
#2494 := (or #2422 #2492 #2493)
#2495 := [th-lemma arith triangle-eq]: #2494
#2496 := [unit-resolution #2495 #2491 #2482]: #2422
#2447 := (not #2422)
#2448 := (or #2447 #2420)
#2443 := (= #1172 #71)
#2441 := (= ?v0!3 f8)
#2440 := [hypothesis]: #2422
#2442 := [symm #2440]: #2441
#2444 := [monotonicity #2442]: #2443
#2445 := [symm #2444]: #2420
#2439 := [hypothesis]: #2434
#2446 := [unit-resolution #2439 #2445]: false
#2449 := [lemma #2446]: #2448
#2497 := [unit-resolution #2449 #2496 #2473]: false
#2498 := [lemma #2497]: #2202
#2056 := (or #2217 #2205 #2211)
#2057 := [def-axiom]: #2056
#2500 := [unit-resolution #2057 #2498 #2499]: #2211
#2063 := (or #2208 #828)
#2073 := [def-axiom]: #2063
#2501 := [unit-resolution #2073 #2500]: #828
#2502 := [unit-resolution #2476 #2501]: #1830
#2065 := (or #2208 #2196)
#2066 := [def-axiom]: #2065
#2503 := [unit-resolution #2066 #2500]: #2196
#1984 := (= f9 f15)
#2070 := (or #2208 #115)
#2072 := [def-axiom]: #2070
#2504 := [unit-resolution #2072 #2500]: #115
#2508 := [symm #2504]: #1984
#2509 := (= #93 f9)
#2506 := (= #93 #40)
#2079 := (or #2208 #114)
#2083 := [def-axiom]: #2079
#2505 := [unit-resolution #2083 #2500]: #114
#2507 := [monotonicity #2505]: #2506
#2510 := [trans #2507 #2307]: #2509
#2511 := [trans #2510 #2508]: #94
#2512 := [unit-resolution #2100 #2511]: #2190
#2513 := [unit-resolution #2096 #2512 #2503]: #1570
#2514 := [unit-resolution #2111 #2513]: #1317
#2515 := [unit-resolution #2481 #2514 #2502]: #2419
#1989 := (or #2208 #845)
#2082 := [def-axiom]: #1989
#2516 := [unit-resolution #2082 #2500]: #845
#1977 := (+ f9 #808)
#1985 := (<= #1977 0::Int)
#1880 := (or #453 #1984)
#1876 := (iff #115 #1984)
#1874 := (iff #1984 #115)
#1875 := [commutativity]: #1874
#1877 := [symm #1875]: #1876
#1873 := [hypothesis]: #115
#1878 := [mp #1873 #1877]: #1984
#1870 := (not #1984)
#1872 := [hypothesis]: #1870
#1879 := [unit-resolution #1872 #1878]: false
#1881 := [lemma #1879]: #1880
#2517 := [unit-resolution #1881 #2504]: #1984
#2518 := (or #1870 #1985)
#2519 := [th-lemma arith triangle-eq]: #2518
#2520 := [unit-resolution #2519 #2517]: #1985
#2521 := (not #1985)
#2522 := (or #2290 #844 #2521)
#2523 := [th-lemma arith assign-bounds 1 -1]: #2522
#2524 := [unit-resolution #2523 #2520 #2516]: #2290
#2525 := [unit-resolution #2109 #2513]: #2112
#2526 := [unit-resolution #2431 #2525 #2524]: #2428
#2527 := [unit-resolution #2436 #2526]: #2434
#2528 := [unit-resolution #2449 #2527]: #2447
#2529 := [unit-resolution #2495 #2528 #2515]: #2492
#2530 := (or #2484 #1334 #2521)
#2531 := [th-lemma arith assign-bounds -1 -1]: #2530
#2532 := [unit-resolution #2531 #2520 #2525]: #2484
#2533 := [unit-resolution #1832 #2513]: #1166
[unit-resolution #2417 #2256 #2533 #2532 #2529]: false
unsat