src/HOL/Boogie/Examples/Boogie_Dijkstra.certs

make SML/NJ happy;

a549accb56a0340bea4e867d66fdfbbac187f40c 6047 0
#2 := false
#7 := 0::Int
decl f30 :: (-> S2 Int)
decl ?v1!7 :: (-> S2 S2)
decl ?v0!20 :: S2
#2034 := ?v0!20
#5342 := (?v1!7 ?v0!20)
#13325 := (f30 #5342)
#923 := -1::Int
#13327 := (* -1::Int #13325)
decl f4 :: (-> S3 Int)
decl f5 :: (-> S4 S2 S3)
decl f6 :: (-> S5 S2 S4)
decl f7 :: S5
#13 := f7
#5350 := (f6 f7 #5342)
#5351 := (f5 #5350 ?v0!20)
#5352 := (f4 #5351)
#5353 := (* -1::Int #5352)
#14209 := (+ #5353 #13327)
#2037 := (f30 ?v0!20)
#14210 := (+ #2037 #14209)
#18243 := (>= #14210 0::Int)
decl f19 :: (-> S11 S2 Int)
decl f20 :: S11
#109 := f20
#5343 := (f19 f20 #5342)
#5344 := (* -1::Int #5343)
#5354 := (+ #5344 #5353)
#5080 := (f19 f20 ?v0!20)
#5355 := (+ #5080 #5354)
#15530 := (>= #5355 0::Int)
#5356 := (= #5355 0::Int)
#5357 := (not #5356)
decl f1 :: S1
#3 := f1
decl f11 :: (-> S7 S2 S1)
decl f21 :: S7
#115 := f21
#5347 := (f11 f21 #5342)
#5348 := (= #5347 f1)
#5349 := (not #5348)
#5345 := (+ #5080 #5344)
#5346 := (<= #5345 0::Int)
#5358 := (or #5346 #5349 #5357)
#5359 := (not #5358)
#5105 := (* -1::Int #5080)
decl f3 :: Int
#8 := f3
#5340 := (+ f3 #5105)
#5341 := (<= #5340 0::Int)
#15968 := (not #5341)
#5106 := (+ #2037 #5105)
#12022 := (>= #5106 0::Int)
#5087 := (= #2037 #5080)
decl f28 :: S2
#181 := f28
#195 := (f6 f7 f28)
#5121 := (f5 #195 ?v0!20)
#5122 := (f4 #5121)
#5139 := (+ #5105 #5122)
#185 := (f19 f20 f28)
#5140 := (+ #185 #5139)
#5141 := (>= #5140 0::Int)
#5123 := (* -1::Int #5122)
#5124 := (+ f3 #5123)
#5125 := (<= #5124 0::Int)
#5146 := (or #5125 #5141)
#2038 := (* -1::Int #2037)
#5178 := (+ #2038 #5122)
#5179 := (+ #185 #5178)
#5182 := (= #5179 0::Int)
#15374 := (not #5182)
#12121 := (<= #5179 0::Int)
#15379 := (not #12121)
#4078 := (f30 f28)
#4079 := (* -1::Int #4078)
#5068 := (+ #2037 #4079)
#5229 := (<= #5068 0::Int)
#15402 := (not #5229)
#15340 := (<= #5122 0::Int)
#15358 := (not #15340)
#15327 := (= f28 ?v0!20)
#15368 := (not #15327)
#9945 := (= ?v0!20 f28)
#16393 := [hypothesis]: #15327
#16394 := [symm #16393]: #9945
#9687 := (not #9945)
#5309 := (f11 f21 ?v0!20)
#5310 := (= #5309 f1)
#9951 := (or #9945 #5310)
#9685 := (not #9951)
decl f12 :: (-> S8 S1 S7)
decl f13 :: (-> S9 S2 S8)
decl f14 :: (-> S10 S7 S9)
decl f15 :: S10
#39 := f15
#191 := (f14 f15 f21)
#192 := (f13 #191 f28)
#193 := (f12 #192 f1)
#9943 := (f11 #193 ?v0!20)
#9944 := (= #9943 f1)
#9956 := (iff #9944 #9951)
#11 := (:var 0 S2)
#54 := (:var 1 S1)
#52 := (:var 2 S2)
#50 := (:var 3 S7)
#51 := (f14 f15 #50)
#53 := (f13 #51 #52)
#55 := (f12 #53 #54)
#56 := (f11 #55 #11)
#3640 := (pattern #56)
#60 := (f11 #50 #11)
#61 := (= #60 f1)
#59 := (= #54 f1)
#58 := (= #11 #52)
#62 := (if #58 #59 #61)
#57 := (= #56 f1)
#63 := (iff #57 #62)
#3641 := (forall (vars (?v0 S7) (?v1 S2) (?v2 S1) (?v3 S2)) (:pat #3640) #63)
#64 := (forall (vars (?v0 S7) (?v1 S2) (?v2 S1) (?v3 S2)) #63)
#3644 := (iff #64 #3641)
#3642 := (iff #63 #63)
#3643 := [refl]: #3642
#3645 := [quant-intro #3643]: #3644
#1496 := (~ #64 #64)
#1524 := (~ #63 #63)
#1525 := [refl]: #1524
#1497 := [nnf-pos #1525]: #1496
#342 := [asserted]: #64
#1526 := [mp~ #342 #1497]: #64
#3646 := [mp #1526 #3645]: #3641
#7518 := (not #3641)
#9763 := (or #7518 #9956)
#4057 := (= f1 f1)
#9946 := (if #9945 #4057 #5310)
#9947 := (iff #9944 #9946)
#9775 := (or #7518 #9947)
#9715 := (iff #9775 #9763)
#9722 := (iff #9763 #9763)
#9724 := [rewrite]: #9722
#9957 := (iff #9947 #9956)
#9954 := (iff #9946 #9951)
#1 := true
#9948 := (if #9945 true #5310)
#9952 := (iff #9948 #9951)
#9953 := [rewrite]: #9952
#9949 := (iff #9946 #9948)
#4059 := (iff #4057 true)
#4060 := [rewrite]: #4059
#9950 := [monotonicity #4060]: #9949
#9955 := [trans #9950 #9953]: #9954
#9958 := [monotonicity #9955]: #9957
#9706 := [monotonicity #9958]: #9715
#9734 := [trans #9706 #9724]: #9715
#9776 := [quant-inst #115 #181 #3 #2034]: #9775
#9519 := [mp #9776 #9734]: #9763
#16374 := [unit-resolution #9519 #3646]: #9956
#9410 := (not #9944)
decl f29 :: S7
#190 := f29
#4533 := (f11 f29 ?v0!20)
#4534 := (= #4533 f1)
#4541 := (not #4534)
#16390 := (iff #4541 #9410)
#16382 := (iff #4534 #9944)
#16359 := (iff #9944 #4534)
#16289 := (= #9943 #4533)
#8145 := (= #193 f29)
#194 := (= f29 #193)
#91 := (f6 f7 #11)
#3693 := (pattern #91)
#212 := (f11 f29 #11)
#3854 := (pattern #212)
#202 := (f30 #11)
#3829 := (pattern #202)
#2047 := (f5 #91 ?v0!20)
#2048 := (f4 #2047)
#2383 := (+ #2038 #2048)
#2384 := (+ #202 #2383)
#2387 := (= #2384 0::Int)
#2941 := (not #2387)
#213 := (= #212 f1)
#220 := (not #213)
#2044 := (+ #202 #2038)
#2045 := (>= #2044 0::Int)
#2942 := (or #2045 #220 #2941)
#3888 := (forall (vars (?v1 S2)) (:pat #3829 #3854 #3693) #2942)
#3893 := (not #3888)
#2039 := (+ f3 #2038)
#2040 := (<= #2039 0::Int)
decl f16 :: S2
#65 := f16
#2035 := (= ?v0!20 f16)
#10 := (:var 1 S2)
#92 := (f5 #91 #10)
#3684 := (pattern #92)
#224 := (f30 #10)
#1186 := (* -1::Int #224)
#1187 := (+ #202 #1186)
#93 := (f4 #92)
#1207 := (+ #93 #1187)
#1205 := (>= #1207 0::Int)
#938 := (* -1::Int #93)
#939 := (+ f3 #938)
#940 := (<= #939 0::Int)
#2933 := (or #220 #940 #1205)
#3880 := (forall (vars (?v0 S2) (?v1 S2)) (:pat #3684) #2933)
#3885 := (not #3880)
#3896 := (or #3885 #2035 #2040 #3893)
#3899 := (not #3896)
decl ?v0!19 :: S2
#2003 := ?v0!19
#2016 := (f30 ?v0!19)
#2017 := (* -1::Int #2016)
decl ?v1!18 :: S2
#2002 := ?v1!18
#2015 := (f30 ?v1!18)
#2018 := (+ #2015 #2017)
#2006 := (f6 f7 ?v1!18)
#2007 := (f5 #2006 ?v0!19)
#2008 := (f4 #2007)
#2019 := (+ #2008 #2018)
#2020 := (>= #2019 0::Int)
#2009 := (* -1::Int #2008)
#2010 := (+ f3 #2009)
#2011 := (<= #2010 0::Int)
#2004 := (f11 f29 ?v1!18)
#2005 := (= #2004 f1)
#2896 := (not #2005)
#2911 := (or #2896 #2011 #2020)
#2916 := (not #2911)
#3902 := (or #2916 #3899)
#3905 := (not #3902)
#3871 := (pattern #202 #224)
#1185 := (>= #1187 0::Int)
#221 := (f11 f29 #10)
#222 := (= #221 f1)
#2873 := (not #222)
#2888 := (or #213 #2873 #1185)
#3872 := (forall (vars (?v0 S2) (?v1 S2)) (:pat #3871) #2888)
#3877 := (not #3872)
#3908 := (or #3877 #3905)
#3911 := (not #3908)
decl ?v0!17 :: S2
#1976 := ?v0!17
#1985 := (f30 ?v0!17)
#1986 := (* -1::Int #1985)
decl ?v1!16 :: S2
#1975 := ?v1!16
#1984 := (f30 ?v1!16)
#1987 := (+ #1984 #1986)
#1988 := (>= #1987 0::Int)
#1980 := (f11 f29 ?v0!17)
#1981 := (= #1980 f1)
#2850 := (not #1981)
#1977 := (f11 f29 ?v1!16)
#1978 := (= #1977 f1)
#2865 := (or #1978 #2850 #1988)
#2870 := (not #2865)
#3914 := (or #2870 #3911)
#3917 := (not #3914)
#1176 := (>= #202 0::Int)
#3863 := (forall (vars (?v0 S2)) (:pat #3829) #1176)
#3868 := (not #3863)
#3920 := (or #3868 #3917)
#3923 := (not #3920)
decl ?v0!15 :: S2
#1960 := ?v0!15
#1961 := (f30 ?v0!15)
#1962 := (>= #1961 0::Int)
#1963 := (not #1962)
#3926 := (or #1963 #3923)
#3929 := (not #3926)
#216 := (f30 f16)
#217 := (= #216 0::Int)
#661 := (not #217)
#3932 := (or #661 #3929)
#3935 := (not #3932)
#3938 := (or #661 #3935)
#3941 := (not #3938)
#112 := (f19 f20 #11)
#3716 := (pattern #112)
#207 := (= #202 #112)
#560 := (or #220 #207)
#3855 := (forall (vars (?v0 S2)) (:pat #3854 #3829 #3716) #560)
#3860 := (not #3855)
#3944 := (or #3860 #3941)
#3947 := (not #3944)
decl ?v0!14 :: S2
#1935 := ?v0!14
#1940 := (f19 f20 ?v0!14)
#1939 := (f30 ?v0!14)
#1941 := (= #1939 #1940)
#1936 := (f11 f29 ?v0!14)
#1937 := (= #1936 f1)
#1938 := (not #1937)
#1942 := (or #1938 #1941)
#1943 := (not #1942)
#3950 := (or #1943 #3947)
#3953 := (not #3950)
#1166 := (* -1::Int #202)
#1167 := (+ #112 #1166)
#1165 := (>= #1167 0::Int)
#3846 := (forall (vars (?v0 S2)) (:pat #3716 #3829) #1165)
#3851 := (not #3846)
#3956 := (or #3851 #3953)
#3959 := (not #3956)
decl ?v0!13 :: S2
#1917 := ?v0!13
#1919 := (f30 ?v0!13)
#1920 := (* -1::Int #1919)
#1918 := (f19 f20 ?v0!13)
#1921 := (+ #1918 #1920)
#1922 := (>= #1921 0::Int)
#1923 := (not #1922)
#3962 := (or #1923 #3959)
#3965 := (not #3962)
#196 := (f5 #195 #11)
#3828 := (pattern #196)
#197 := (f4 #196)
#1140 := (* -1::Int #197)
#1146 := (* -1::Int #185)
#1147 := (+ #1146 #1140)
#1148 := (+ #112 #1147)
#1149 := (<= #1148 0::Int)
#1141 := (+ f3 #1140)
#1142 := (<= #1141 0::Int)
#2822 := (or #1142 #1149)
#2823 := (not #2822)
#2844 := (or #2823 #207)
#3838 := (forall (vars (?v0 S2)) (:pat #3828 #3716 #3829) #2844)
#3843 := (not #3838)
#1296 := (+ #197 #1166)
#1297 := (+ #185 #1296)
#1294 := (= #1297 0::Int)
#2836 := (or #1142 #1149 #1294)
#3830 := (forall (vars (?v0 S2)) (:pat #3828 #3716 #3829) #2836)
#3835 := (not #3830)
#715 := (not #194)
#116 := (f11 f21 #11)
#3750 := (pattern #116)
#1309 := (+ #112 #1146)
#1308 := (>= #1309 0::Int)
#117 := (= #116 f1)
#1312 := (or #117 #1308)
#3820 := (forall (vars (?v0 S2)) (:pat #3750 #3716) #1312)
#3825 := (not #3820)
#1321 := (+ f3 #1146)
#1322 := (<= #1321 0::Int)
#182 := (f11 f21 f28)
#183 := (= #182 f1)
decl ?v0!12 :: S2
#1872 := ?v0!12
#1876 := (f19 f20 ?v0!12)
#1877 := (* -1::Int #1876)
#1878 := (+ f3 #1877)
#1879 := (<= #1878 0::Int)
#1873 := (f11 f21 ?v0!12)
#1874 := (= #1873 f1)
#3968 := (or #1874 #1879 #183 #1322 #3825 #715 #3835 #3843 #3965)
#3971 := (not #3968)
decl f25 :: S11
#148 := f25
#168 := (f19 f25 f16)
#169 := (= #168 0::Int)
#156 := (f19 f25 #10)
#1060 := (* -1::Int #156)
#153 := (f19 f25 #11)
#1061 := (+ #153 #1060)
#1067 := (+ #93 #1061)
#1090 := (>= #1067 0::Int)
#1047 := (* -1::Int #153)
#1048 := (+ f3 #1047)
#1049 := (<= #1048 0::Int)
#2776 := (or #1049 #940 #1090)
#3782 := (forall (vars (?v0 S2) (?v1 S2)) (:pat #3684) #2776)
#3787 := (not #3782)
#3790 := (or #3787 #169)
#3793 := (not #3790)
decl ?v0!11 :: S2
#1816 := ?v0!11
#1831 := (f19 f25 ?v0!11)
#1832 := (* -1::Int #1831)
decl ?v1!10 :: S2
#1815 := ?v1!10
#1822 := (f6 f7 ?v1!10)
#1823 := (f5 #1822 ?v0!11)
#1824 := (f4 #1823)
#2352 := (+ #1824 #1832)
#1817 := (f19 f25 ?v1!10)
#2353 := (+ #1817 #2352)
#2356 := (>= #2353 0::Int)
#1825 := (* -1::Int #1824)
#1826 := (+ f3 #1825)
#1827 := (<= #1826 0::Int)
#1818 := (* -1::Int #1817)
#1819 := (+ f3 #1818)
#1820 := (<= #1819 0::Int)
#2754 := (or #1820 #1827 #2356)
#2759 := (not #2754)
#3796 := (or #2759 #3793)
#3799 := (not #3796)
#3759 := (pattern #153)
decl ?v1!9 :: (-> S2 S2)
#1791 := (?v1!9 #11)
#1796 := (f6 f7 #1791)
#1797 := (f5 #1796 #11)
#1798 := (f4 #1797)
#2335 := (* -1::Int #1798)
#1792 := (f19 f25 #1791)
#2318 := (* -1::Int #1792)
#2336 := (+ #2318 #2335)
#2337 := (+ #153 #2336)
#2338 := (= #2337 0::Int)
#2724 := (not #2338)
#2319 := (+ #153 #2318)
#2320 := (<= #2319 0::Int)
#2725 := (or #2320 #2724)
#2726 := (not #2725)
#66 := (= #11 f16)
#2732 := (or #66 #1049 #2726)
#3774 := (forall (vars (?v0 S2)) (:pat #3759) #2732)
#3779 := (not #3774)
#3802 := (or #3779 #3799)
#3805 := (not #3802)
decl ?v0!8 :: S2
#1751 := ?v0!8
#1764 := (f5 #91 ?v0!8)
#1765 := (f4 #1764)
#1754 := (f19 f25 ?v0!8)
#1755 := (* -1::Int #1754)
#2288 := (+ #1755 #1765)
#2289 := (+ #153 #2288)
#2292 := (= #2289 0::Int)
#2688 := (not #2292)
#1761 := (+ #153 #1755)
#1762 := (>= #1761 0::Int)
#2689 := (or #1762 #2688)
#3760 := (forall (vars (?v1 S2)) (:pat #3759 #3693) #2689)
#3765 := (not #3760)
#1756 := (+ f3 #1755)
#1757 := (<= #1756 0::Int)
#1752 := (= ?v0!8 f16)
#3768 := (or #1752 #1757 #3765)
#3771 := (not #3768)
#3808 := (or #3771 #3805)
#3811 := (not #3808)
decl f27 :: S11
#151 := f27
decl f26 :: S11
#150 := f26
#152 := (= f26 f27)
#494 := (not #152)
#149 := (= f25 f20)
#503 := (not #149)
decl f24 :: S2
#146 := f24
decl f23 :: S2
#145 := f23
#147 := (= f23 f24)
#512 := (not #147)
decl f22 :: S7
#143 := f22
#144 := (= f22 f21)
#521 := (not #144)
#1002 := (* -1::Int #112)
#1003 := (+ f3 #1002)
#1004 := (<= #1003 0::Int)
#2674 := (or #117 #1004)
#3751 := (forall (vars (?v0 S2)) (:pat #3750 #3716) #2674)
#3756 := (not #3751)
#3814 := (or #3756 #521 #512 #503 #494 #3811)
#3817 := (not #3814)
#3974 := (or #3817 #3971)
#3977 := (not #3974)
#1707 := (?v1!7 #11)
#1714 := (f6 f7 #1707)
#1715 := (f5 #1714 #11)
#1716 := (f4 #1715)
#2261 := (* -1::Int #1716)
#1708 := (f19 f20 #1707)
#2244 := (* -1::Int #1708)
#2262 := (+ #2244 #2261)
#2263 := (+ #112 #2262)
#2264 := (= #2263 0::Int)
#2658 := (not #2264)
#1712 := (f11 f21 #1707)
#1713 := (= #1712 f1)
#2657 := (not #1713)
#2245 := (+ #112 #2244)
#2246 := (<= #2245 0::Int)
#2659 := (or #2246 #2657 #2658)
#2660 := (not #2659)
#2666 := (or #66 #1004 #2660)
#3742 := (forall (vars (?v0 S2)) (:pat #3716) #2666)
#3747 := (not #3742)
#122 := (f19 f20 #10)
#1016 := (* -1::Int #122)
#1017 := (+ #112 #1016)
#1018 := (+ #93 #1017)
#1371 := (>= #1018 0::Int)
#118 := (not #117)
#2638 := (or #118 #940 #1371)
#3734 := (forall (vars (?v0 S2) (?v1 S2)) (:pat #3684) #2638)
#3739 := (not #3734)
#119 := (f11 f21 #10)
#3725 := (pattern #116 #119)
#1020 := (>= #1017 0::Int)
#120 := (= #119 f1)
#2601 := (not #120)
#2616 := (or #117 #2601 #1020)
#3726 := (forall (vars (?v0 S2) (?v1 S2)) (:pat #3725) #2616)
#3731 := (not #3726)
#1394 := (>= #112 0::Int)
#3717 := (forall (vars (?v0 S2)) (:pat #3716) #1394)
#3722 := (not #3717)
#110 := (f19 f20 f16)
#111 := (= #110 0::Int)
#804 := (not #111)
decl f17 :: (-> S2 Int)
#67 := (f17 #11)
#3647 := (pattern #67)
decl ?v1!6 :: (-> S2 S2)
#1654 := (?v1!6 #11)
#1661 := (f6 f7 #1654)
#1662 := (f5 #1661 #11)
#1663 := (f4 #1662)
#2219 := (* -1::Int #1663)
#1655 := (f17 #1654)
#2202 := (* -1::Int #1655)
#2220 := (+ #2202 #2219)
#2221 := (+ #67 #2220)
#2222 := (= #2221 0::Int)
#2585 := (not #2222)
decl f18 :: S7
#75 := f18
#1659 := (f11 f18 #1654)
#1660 := (= #1659 f1)
#2584 := (not #1660)
#2203 := (+ #67 #2202)
#2204 := (<= #2203 0::Int)
#2586 := (or #2204 #2584 #2585)
#2587 := (not #2586)
#964 := (* -1::Int #67)
#965 := (+ f3 #964)
#966 := (<= #965 0::Int)
#2593 := (or #66 #966 #2587)
#3708 := (forall (vars (?v0 S2)) (:pat #3647) #2593)
#3713 := (not #3708)
#3980 := (or #3713 #804 #3722 #3731 #3739 #3747 #3977)
#3983 := (not #3980)
#76 := (f11 f18 #11)
#3660 := (pattern #76)
decl ?v0!5 :: S2
#1613 := ?v0!5
#1626 := (f5 #91 ?v0!5)
#1627 := (f4 #1626)
#1616 := (f17 ?v0!5)
#1617 := (* -1::Int #1616)
#1628 := (+ #1617 #1627)
#1629 := (+ #67 #1628)
#1630 := (= #1629 0::Int)
#2548 := (not #1630)
#77 := (= #76 f1)
#78 := (not #77)
#1623 := (+ #67 #1617)
#1624 := (>= #1623 0::Int)
#2549 := (or #1624 #78 #2548)
#3694 := (forall (vars (?v1 S2)) (:pat #3647 #3660 #3693) #2549)
#3699 := (not #3694)
#1618 := (+ f3 #1617)
#1619 := (<= #1618 0::Int)
#1614 := (= ?v0!5 f16)
#3702 := (or #1614 #1619 #3699)
#6176 := (= f3 #1616)
#6574 := (= #1616 f3)
#6629 := (iff #6574 #6176)
#6627 := (iff #6176 #6574)
#6628 := [commutativity]: #6627
#6630 := [symm #6628]: #6629
#1615 := (not #1614)
#3705 := (not #3702)
#5790 := [hypothesis]: #3705
#3262 := (or #3702 #1615)
#3263 := [def-axiom]: #3262
#6625 := [unit-resolution #3263 #5790]: #1615
#72 := (= #67 f3)
#350 := (or #66 #72)
#3654 := (forall (vars (?v0 S2)) (:pat #3647) #350)
#353 := (forall (vars (?v0 S2)) #350)
#3657 := (iff #353 #3654)
#3655 := (iff #350 #350)
#3656 := [refl]: #3655
#3658 := [quant-intro #3656]: #3657
#1500 := (~ #353 #353)
#1530 := (~ #350 #350)
#1531 := [refl]: #1530
#1501 := [nnf-pos #1531]: #1500
#1229 := (= #1207 0::Int)
#1232 := (not #1185)
#1241 := (and #1232 #213 #1229)
#1246 := (exists (vars (?v1 S2)) #1241)
#1218 := (+ f3 #1166)
#1219 := (<= #1218 0::Int)
#1220 := (not #1219)
#71 := (not #66)
#1223 := (and #71 #1220)
#1226 := (not #1223)
#1249 := (or #1226 #1246)
#1252 := (forall (vars (?v0 S2)) #1249)
#941 := (not #940)
#1199 := (and #213 #941)
#1202 := (not #1199)
#1209 := (or #1202 #1205)
#1212 := (forall (vars (?v0 S2) (?v1 S2)) #1209)
#1215 := (not #1212)
#1255 := (or #1215 #1252)
#1258 := (and #1212 #1255)
#223 := (and #220 #222)
#566 := (not #223)
#1190 := (or #566 #1185)
#1193 := (forall (vars (?v0 S2) (?v1 S2)) #1190)
#1196 := (not #1193)
#1261 := (or #1196 #1258)
#1264 := (and #1193 #1261)
#1179 := (forall (vars (?v0 S2)) #1176)
#1182 := (not #1179)
#1267 := (or #1182 #1264)
#1270 := (and #1179 #1267)
#1273 := (or #661 #1270)
#1276 := (and #217 #1273)
#563 := (forall (vars (?v0 S2)) #560)
#673 := (not #563)
#1279 := (or #673 #1276)
#1282 := (and #563 #1279)
#1170 := (forall (vars (?v0 S2)) #1165)
#1173 := (not #1170)
#1285 := (or #1173 #1282)
#1288 := (and #1170 #1285)
#1150 := (not #1149)
#1143 := (not #1142)
#1153 := (and #1143 #1150)
#1156 := (or #1153 #207)
#1159 := (forall (vars (?v0 S2)) #1156)
#1162 := (not #1159)
#1291 := (not #1153)
#1299 := (or #1291 #1294)
#1302 := (forall (vars (?v0 S2)) #1299)
#1305 := (not #1302)
#1315 := (forall (vars (?v0 S2)) #1312)
#1318 := (not #1315)
#1005 := (not #1004)
#1114 := (and #118 #1005)
#1117 := (exists (vars (?v0 S2)) #1114)
#1333 := (not #1117)
#1357 := (or #1333 #183 #1322 #1318 #715 #1305 #1162 #1288)
#1050 := (not #1049)
#1084 := (and #1050 #941)
#1087 := (not #1084)
#1093 := (or #1087 #1090)
#1096 := (forall (vars (?v0 S2) (?v1 S2)) #1093)
#1099 := (not #1096)
#1102 := (or #1099 #169)
#1105 := (and #1096 #1102)
#1065 := (= #1067 0::Int)
#1059 := (>= #1061 0::Int)
#1062 := (not #1059)
#1069 := (and #1062 #1065)
#1072 := (exists (vars (?v1 S2)) #1069)
#1053 := (and #71 #1050)
#1056 := (not #1053)
#1075 := (or #1056 #1072)
#1078 := (forall (vars (?v0 S2)) #1075)
#1081 := (not #1078)
#1108 := (or #1081 #1105)
#1111 := (and #1078 #1108)
#1135 := (or #1117 #521 #512 #503 #494 #1111)
#1362 := (and #1135 #1357)
#1014 := (= #1018 0::Int)
#1021 := (not #1020)
#1030 := (and #1021 #117 #1014)
#1035 := (exists (vars (?v1 S2)) #1030)
#1008 := (and #71 #1005)
#1011 := (not #1008)
#1038 := (or #1011 #1035)
#1041 := (forall (vars (?v0 S2)) #1038)
#1044 := (not #1041)
#1365 := (and #117 #941)
#1368 := (not #1365)
#1374 := (or #1368 #1371)
#1377 := (forall (vars (?v0 S2) (?v1 S2)) #1374)
#1380 := (not #1377)
#121 := (and #118 #120)
#377 := (not #121)
#1385 := (or #377 #1020)
#1388 := (forall (vars (?v0 S2) (?v1 S2)) #1385)
#1391 := (not #1388)
#1397 := (forall (vars (?v0 S2)) #1394)
#1400 := (not #1397)
#87 := (f17 #10)
#926 := (* -1::Int #87)
#953 := (+ #926 #93)
#954 := (+ #67 #953)
#976 := (= #954 0::Int)
#927 := (+ #67 #926)
#925 := (>= #927 0::Int)
#979 := (not #925)
#988 := (and #979 #77 #976)
#993 := (exists (vars (?v1 S2)) #988)
#967 := (not #966)
#970 := (and #71 #967)
#973 := (not #970)
#996 := (or #973 #993)
#999 := (forall (vars (?v0 S2)) #996)
#1403 := (not #999)
#1424 := (or #1403 #804 #1400 #1391 #1380 #1044 #1362)
#1429 := (and #999 #1424)
#951 := (>= #954 0::Int)
#944 := (and #77 #941)
#947 := (not #944)
#955 := (or #947 #951)
#958 := (forall (vars (?v0 S2) (?v1 S2)) #955)
#961 := (not #958)
#1432 := (or #961 #1429)
#1435 := (and #958 #1432)
#84 := (f11 f18 #10)
#85 := (= #84 f1)
#86 := (and #78 #85)
#356 := (not #86)
#929 := (or #356 #925)
#932 := (forall (vars (?v0 S2) (?v1 S2)) #929)
#935 := (not #932)
#1438 := (or #935 #1435)
#1441 := (and #932 #1438)
#916 := (>= #67 0::Int)
#917 := (forall (vars (?v0 S2)) #916)
#920 := (not #917)
#1444 := (or #920 #1441)
#1447 := (and #917 #1444)
#80 := (f17 f16)
#81 := (= #80 0::Int)
#868 := (not #81)
#1450 := (or #868 #1447)
#1453 := (and #81 #1450)
#79 := (forall (vars (?v0 S2)) #78)
#880 := (not #79)
#889 := (not #353)
#68 := (= #67 0::Int)
#344 := (or #71 #68)
#347 := (forall (vars (?v0 S2)) #344)
#898 := (not #347)
#1465 := (or #898 #889 #880 #1453)
#1470 := (not #1465)
#229 := (+ #202 #93)
#236 := (= #224 #229)
#237 := (and #213 #236)
#235 := (< #202 #224)
#238 := (and #235 #237)
#239 := (exists (vars (?v1 S2)) #238)
#233 := (< #202 f3)
#234 := (and #71 #233)
#240 := (implies #234 #239)
#241 := (forall (vars (?v0 S2)) #240)
#242 := (and #241 true)
#230 := (<= #224 #229)
#94 := (< #93 f3)
#228 := (and #213 #94)
#231 := (implies #228 #230)
#232 := (forall (vars (?v0 S2) (?v1 S2)) #231)
#243 := (implies #232 #242)
#244 := (and #232 #243)
#225 := (<= #224 #202)
#226 := (implies #223 #225)
#227 := (forall (vars (?v0 S2) (?v1 S2)) #226)
#245 := (implies #227 #244)
#246 := (and #227 #245)
#218 := (<= 0::Int #202)
#219 := (forall (vars (?v0 S2)) #218)
#247 := (implies #219 #246)
#248 := (and #219 #247)
#249 := (implies #217 #248)
#250 := (and #217 #249)
#214 := (implies #213 #207)
#215 := (forall (vars (?v0 S2)) #214)
#251 := (implies #215 #250)
#252 := (and #215 #251)
#210 := (<= #202 #112)
#211 := (forall (vars (?v0 S2)) #210)
#253 := (implies #211 #252)
#254 := (and #211 #253)
#199 := (+ #185 #197)
#200 := (< #199 #112)
#198 := (< #197 f3)
#201 := (and #198 #200)
#206 := (not #201)
#208 := (implies #206 #207)
#209 := (forall (vars (?v0 S2)) #208)
#255 := (implies #209 #254)
#203 := (= #202 #199)
#204 := (implies #201 #203)
#205 := (forall (vars (?v0 S2)) #204)
#256 := (implies #205 #255)
#257 := (implies #194 #256)
#187 := (<= #185 #112)
#188 := (implies #118 #187)
#189 := (forall (vars (?v0 S2)) #188)
#258 := (implies #189 #257)
#186 := (< #185 f3)
#259 := (implies #186 #258)
#184 := (not #183)
#260 := (implies #184 #259)
#131 := (< #112 f3)
#140 := (and #118 #131)
#141 := (exists (vars (?v0 S2)) #140)
#261 := (implies #141 #260)
#262 := (implies true #261)
#170 := (and #169 true)
#158 := (+ #153 #93)
#165 := (<= #156 #158)
#154 := (< #153 f3)
#164 := (and #154 #94)
#166 := (implies #164 #165)
#167 := (forall (vars (?v0 S2) (?v1 S2)) #166)
#171 := (implies #167 #170)
#172 := (and #167 #171)
#159 := (= #156 #158)
#157 := (< #153 #156)
#160 := (and #157 #159)
#161 := (exists (vars (?v1 S2)) #160)
#155 := (and #71 #154)
#162 := (implies #155 #161)
#163 := (forall (vars (?v0 S2)) #162)
#173 := (implies #163 #172)
#174 := (and #163 #173)
#175 := (implies #152 #174)
#176 := (implies #149 #175)
#177 := (implies #147 #176)
#178 := (implies #144 #177)
#142 := (not #141)
#179 := (implies #142 #178)
#180 := (implies true #179)
#263 := (and #180 #262)
#127 := (+ #112 #93)
#134 := (= #122 #127)
#135 := (and #117 #134)
#133 := (< #112 #122)
#136 := (and #133 #135)
#137 := (exists (vars (?v1 S2)) #136)
#132 := (and #71 #131)
#138 := (implies #132 #137)
#139 := (forall (vars (?v0 S2)) #138)
#264 := (implies #139 #263)
#128 := (<= #122 #127)
#126 := (and #117 #94)
#129 := (implies #126 #128)
#130 := (forall (vars (?v0 S2) (?v1 S2)) #129)
#265 := (implies #130 #264)
#123 := (<= #122 #112)
#124 := (implies #121 #123)
#125 := (forall (vars (?v0 S2) (?v1 S2)) #124)
#266 := (implies #125 #265)
#113 := (<= 0::Int #112)
#114 := (forall (vars (?v0 S2)) #113)
#267 := (implies #114 #266)
#268 := (implies #111 #267)
#269 := (implies true #268)
#96 := (+ #67 #93)
#103 := (= #87 #96)
#104 := (and #77 #103)
#102 := (< #67 #87)
#105 := (and #102 #104)
#106 := (exists (vars (?v1 S2)) #105)
#100 := (< #67 f3)
#101 := (and #71 #100)
#107 := (implies #101 #106)
#108 := (forall (vars (?v0 S2)) #107)
#270 := (implies #108 #269)
#271 := (and #108 #270)
#97 := (<= #87 #96)
#95 := (and #77 #94)
#98 := (implies #95 #97)
#99 := (forall (vars (?v0 S2) (?v1 S2)) #98)
#272 := (implies #99 #271)
#273 := (and #99 #272)
#88 := (<= #87 #67)
#89 := (implies #86 #88)
#90 := (forall (vars (?v0 S2) (?v1 S2)) #89)
#274 := (implies #90 #273)
#275 := (and #90 #274)
#82 := (<= 0::Int #67)
#83 := (forall (vars (?v0 S2)) #82)
#276 := (implies #83 #275)
#277 := (and #83 #276)
#278 := (implies #81 #277)
#279 := (and #81 #278)
#280 := (implies #79 #279)
#73 := (implies #71 #72)
#74 := (forall (vars (?v0 S2)) #73)
#281 := (implies #74 #280)
#69 := (implies #66 #68)
#70 := (forall (vars (?v0 S2)) #69)
#282 := (implies #70 #281)
#283 := (implies true #282)
#284 := (not #283)
#1473 := (iff #284 #1470)
#573 := (+ #93 #202)
#591 := (= #224 #573)
#594 := (and #213 #591)
#597 := (and #235 #594)
#600 := (exists (vars (?v1 S2)) #597)
#606 := (not #234)
#607 := (or #606 #600)
#612 := (forall (vars (?v0 S2)) #607)
#576 := (<= #224 #573)
#582 := (not #228)
#583 := (or #582 #576)
#588 := (forall (vars (?v0 S2) (?v1 S2)) #583)
#625 := (not #588)
#626 := (or #625 #612)
#631 := (and #588 #626)
#567 := (or #566 #225)
#570 := (forall (vars (?v0 S2) (?v1 S2)) #567)
#637 := (not #570)
#638 := (or #637 #631)
#643 := (and #570 #638)
#649 := (not #219)
#650 := (or #649 #643)
#655 := (and #219 #650)
#662 := (or #661 #655)
#667 := (and #217 #662)
#674 := (or #673 #667)
#679 := (and #563 #674)
#685 := (not #211)
#686 := (or #685 #679)
#691 := (and #211 #686)
#554 := (or #201 #207)
#557 := (forall (vars (?v0 S2)) #554)
#697 := (not #557)
#698 := (or #697 #691)
#548 := (or #206 #203)
#551 := (forall (vars (?v0 S2)) #548)
#706 := (not #551)
#707 := (or #706 #698)
#716 := (or #715 #707)
#542 := (or #117 #187)
#545 := (forall (vars (?v0 S2)) #542)
#724 := (not #545)
#725 := (or #724 #716)
#733 := (not #186)
#734 := (or #733 #725)
#742 := (or #183 #734)
#750 := (or #142 #742)
#426 := (+ #93 #153)
#450 := (<= #156 #426)
#456 := (not #164)
#457 := (or #456 #450)
#462 := (forall (vars (?v0 S2) (?v1 S2)) #457)
#470 := (not #462)
#471 := (or #470 #169)
#476 := (and #462 #471)
#429 := (= #156 #426)
#432 := (and #157 #429)
#435 := (exists (vars (?v1 S2)) #432)
#441 := (not #155)
#442 := (or #441 #435)
#447 := (forall (vars (?v0 S2)) #442)
#482 := (not #447)
#483 := (or #482 #476)
#488 := (and #447 #483)
#495 := (or #494 #488)
#504 := (or #503 #495)
#513 := (or #512 #504)
#522 := (or #521 #513)
#530 := (or #141 #522)
#762 := (and #530 #750)
#384 := (+ #93 #112)
#402 := (= #122 #384)
#405 := (and #117 #402)
#408 := (and #133 #405)
#411 := (exists (vars (?v1 S2)) #408)
#417 := (not #132)
#418 := (or #417 #411)
#423 := (forall (vars (?v0 S2)) #418)
#768 := (not #423)
#769 := (or #768 #762)
#387 := (<= #122 #384)
#393 := (not #126)
#394 := (or #393 #387)
#399 := (forall (vars (?v0 S2) (?v1 S2)) #394)
#777 := (not #399)
#778 := (or #777 #769)
#378 := (or #377 #123)
#381 := (forall (vars (?v0 S2) (?v1 S2)) #378)
#786 := (not #381)
#787 := (or #786 #778)
#795 := (not #114)
#796 := (or #795 #787)
#805 := (or #804 #796)
#370 := (not #101)
#371 := (or #370 #106)
#374 := (forall (vars (?v0 S2)) #371)
#820 := (not #374)
#821 := (or #820 #805)
#826 := (and #374 #821)
#363 := (not #95)
#364 := (or #363 #97)
#367 := (forall (vars (?v0 S2) (?v1 S2)) #364)
#832 := (not #367)
#833 := (or #832 #826)
#838 := (and #367 #833)
#357 := (or #356 #88)
#360 := (forall (vars (?v0 S2) (?v1 S2)) #357)
#844 := (not #360)
#845 := (or #844 #838)
#850 := (and #360 #845)
#856 := (not #83)
#857 := (or #856 #850)
#862 := (and #83 #857)
#869 := (or #868 #862)
#874 := (and #81 #869)
#881 := (or #880 #874)
#890 := (or #889 #881)
#899 := (or #898 #890)
#911 := (not #899)
#1471 := (iff #911 #1470)
#1468 := (iff #899 #1465)
#1456 := (or #880 #1453)
#1459 := (or #889 #1456)
#1462 := (or #898 #1459)
#1466 := (iff #1462 #1465)
#1467 := [rewrite]: #1466
#1463 := (iff #899 #1462)
#1460 := (iff #890 #1459)
#1457 := (iff #881 #1456)
#1454 := (iff #874 #1453)
#1451 := (iff #869 #1450)
#1448 := (iff #862 #1447)
#1445 := (iff #857 #1444)
#1442 := (iff #850 #1441)
#1439 := (iff #845 #1438)
#1436 := (iff #838 #1435)
#1433 := (iff #833 #1432)
#1430 := (iff #826 #1429)
#1427 := (iff #821 #1424)
#1406 := (or #1044 #1362)
#1409 := (or #1380 #1406)
#1412 := (or #1391 #1409)
#1415 := (or #1400 #1412)
#1418 := (or #804 #1415)
#1421 := (or #1403 #1418)
#1425 := (iff #1421 #1424)
#1426 := [rewrite]: #1425
#1422 := (iff #821 #1421)
#1419 := (iff #805 #1418)
#1416 := (iff #796 #1415)
#1413 := (iff #787 #1412)
#1410 := (iff #778 #1409)
#1407 := (iff #769 #1406)
#1363 := (iff #762 #1362)
#1360 := (iff #750 #1357)
#1336 := (or #1162 #1288)
#1339 := (or #1305 #1336)
#1342 := (or #715 #1339)
#1345 := (or #1318 #1342)
#1348 := (or #1322 #1345)
#1351 := (or #183 #1348)
#1354 := (or #1333 #1351)
#1358 := (iff #1354 #1357)
#1359 := [rewrite]: #1358
#1355 := (iff #750 #1354)
#1352 := (iff #742 #1351)
#1349 := (iff #734 #1348)
#1346 := (iff #725 #1345)
#1343 := (iff #716 #1342)
#1340 := (iff #707 #1339)
#1337 := (iff #698 #1336)
#1289 := (iff #691 #1288)
#1286 := (iff #686 #1285)
#1283 := (iff #679 #1282)
#1280 := (iff #674 #1279)
#1277 := (iff #667 #1276)
#1274 := (iff #662 #1273)
#1271 := (iff #655 #1270)
#1268 := (iff #650 #1267)
#1265 := (iff #643 #1264)
#1262 := (iff #638 #1261)
#1259 := (iff #631 #1258)
#1256 := (iff #626 #1255)
#1253 := (iff #612 #1252)
#1250 := (iff #607 #1249)
#1247 := (iff #600 #1246)
#1244 := (iff #597 #1241)
#1235 := (and #213 #1229)
#1238 := (and #1232 #1235)
#1242 := (iff #1238 #1241)
#1243 := [rewrite]: #1242
#1239 := (iff #597 #1238)
#1236 := (iff #594 #1235)
#1230 := (iff #591 #1229)
#1231 := [rewrite]: #1230
#1237 := [monotonicity #1231]: #1236
#1233 := (iff #235 #1232)
#1234 := [rewrite]: #1233
#1240 := [monotonicity #1234 #1237]: #1239
#1245 := [trans #1240 #1243]: #1244
#1248 := [quant-intro #1245]: #1247
#1227 := (iff #606 #1226)
#1224 := (iff #234 #1223)
#1221 := (iff #233 #1220)
#1222 := [rewrite]: #1221
#1225 := [monotonicity #1222]: #1224
#1228 := [monotonicity #1225]: #1227
#1251 := [monotonicity #1228 #1248]: #1250
#1254 := [quant-intro #1251]: #1253
#1216 := (iff #625 #1215)
#1213 := (iff #588 #1212)
#1210 := (iff #583 #1209)
#1206 := (iff #576 #1205)
#1208 := [rewrite]: #1206
#1203 := (iff #582 #1202)
#1200 := (iff #228 #1199)
#942 := (iff #94 #941)
#943 := [rewrite]: #942
#1201 := [monotonicity #943]: #1200
#1204 := [monotonicity #1201]: #1203
#1211 := [monotonicity #1204 #1208]: #1210
#1214 := [quant-intro #1211]: #1213
#1217 := [monotonicity #1214]: #1216
#1257 := [monotonicity #1217 #1254]: #1256
#1260 := [monotonicity #1214 #1257]: #1259
#1197 := (iff #637 #1196)
#1194 := (iff #570 #1193)
#1191 := (iff #567 #1190)
#1188 := (iff #225 #1185)
#1189 := [rewrite]: #1188
#1192 := [monotonicity #1189]: #1191
#1195 := [quant-intro #1192]: #1194
#1198 := [monotonicity #1195]: #1197
#1263 := [monotonicity #1198 #1260]: #1262
#1266 := [monotonicity #1195 #1263]: #1265
#1183 := (iff #649 #1182)
#1180 := (iff #219 #1179)
#1177 := (iff #218 #1176)
#1178 := [rewrite]: #1177
#1181 := [quant-intro #1178]: #1180
#1184 := [monotonicity #1181]: #1183
#1269 := [monotonicity #1184 #1266]: #1268
#1272 := [monotonicity #1181 #1269]: #1271
#1275 := [monotonicity #1272]: #1274
#1278 := [monotonicity #1275]: #1277
#1281 := [monotonicity #1278]: #1280
#1284 := [monotonicity #1281]: #1283
#1174 := (iff #685 #1173)
#1171 := (iff #211 #1170)
#1168 := (iff #210 #1165)
#1169 := [rewrite]: #1168
#1172 := [quant-intro #1169]: #1171
#1175 := [monotonicity #1172]: #1174
#1287 := [monotonicity #1175 #1284]: #1286
#1290 := [monotonicity #1172 #1287]: #1289
#1163 := (iff #697 #1162)
#1160 := (iff #557 #1159)
#1157 := (iff #554 #1156)
#1154 := (iff #201 #1153)
#1151 := (iff #200 #1150)
#1152 := [rewrite]: #1151
#1144 := (iff #198 #1143)
#1145 := [rewrite]: #1144
#1155 := [monotonicity #1145 #1152]: #1154
#1158 := [monotonicity #1155]: #1157
#1161 := [quant-intro #1158]: #1160
#1164 := [monotonicity #1161]: #1163
#1338 := [monotonicity #1164 #1290]: #1337
#1306 := (iff #706 #1305)
#1303 := (iff #551 #1302)
#1300 := (iff #548 #1299)
#1295 := (iff #203 #1294)
#1298 := [rewrite]: #1295
#1292 := (iff #206 #1291)
#1293 := [monotonicity #1155]: #1292
#1301 := [monotonicity #1293 #1298]: #1300
#1304 := [quant-intro #1301]: #1303
#1307 := [monotonicity #1304]: #1306
#1341 := [monotonicity #1307 #1338]: #1340
#1344 := [monotonicity #1341]: #1343
#1319 := (iff #724 #1318)
#1316 := (iff #545 #1315)
#1313 := (iff #542 #1312)
#1310 := (iff #187 #1308)
#1311 := [rewrite]: #1310
#1314 := [monotonicity #1311]: #1313
#1317 := [quant-intro #1314]: #1316
#1320 := [monotonicity #1317]: #1319
#1347 := [monotonicity #1320 #1344]: #1346
#1331 := (iff #733 #1322)
#1323 := (not #1322)
#1326 := (not #1323)
#1329 := (iff #1326 #1322)
#1330 := [rewrite]: #1329
#1327 := (iff #733 #1326)
#1324 := (iff #186 #1323)
#1325 := [rewrite]: #1324
#1328 := [monotonicity #1325]: #1327
#1332 := [trans #1328 #1330]: #1331
#1350 := [monotonicity #1332 #1347]: #1349
#1353 := [monotonicity #1350]: #1352
#1334 := (iff #142 #1333)
#1118 := (iff #141 #1117)
#1115 := (iff #140 #1114)
#1006 := (iff #131 #1005)
#1007 := [rewrite]: #1006
#1116 := [monotonicity #1007]: #1115
#1119 := [quant-intro #1116]: #1118
#1335 := [monotonicity #1119]: #1334
#1356 := [monotonicity #1335 #1353]: #1355
#1361 := [trans #1356 #1359]: #1360
#1138 := (iff #530 #1135)
#1120 := (or #494 #1111)
#1123 := (or #503 #1120)
#1126 := (or #512 #1123)
#1129 := (or #521 #1126)
#1132 := (or #1117 #1129)
#1136 := (iff #1132 #1135)
#1137 := [rewrite]: #1136
#1133 := (iff #530 #1132)
#1130 := (iff #522 #1129)
#1127 := (iff #513 #1126)
#1124 := (iff #504 #1123)
#1121 := (iff #495 #1120)
#1112 := (iff #488 #1111)
#1109 := (iff #483 #1108)
#1106 := (iff #476 #1105)
#1103 := (iff #471 #1102)
#1100 := (iff #470 #1099)
#1097 := (iff #462 #1096)
#1094 := (iff #457 #1093)
#1091 := (iff #450 #1090)
#1092 := [rewrite]: #1091
#1088 := (iff #456 #1087)
#1085 := (iff #164 #1084)
#1051 := (iff #154 #1050)
#1052 := [rewrite]: #1051
#1086 := [monotonicity #1052 #943]: #1085
#1089 := [monotonicity #1086]: #1088
#1095 := [monotonicity #1089 #1092]: #1094
#1098 := [quant-intro #1095]: #1097
#1101 := [monotonicity #1098]: #1100
#1104 := [monotonicity #1101]: #1103
#1107 := [monotonicity #1098 #1104]: #1106
#1082 := (iff #482 #1081)
#1079 := (iff #447 #1078)
#1076 := (iff #442 #1075)
#1073 := (iff #435 #1072)
#1070 := (iff #432 #1069)
#1066 := (iff #429 #1065)
#1068 := [rewrite]: #1066
#1063 := (iff #157 #1062)
#1064 := [rewrite]: #1063
#1071 := [monotonicity #1064 #1068]: #1070
#1074 := [quant-intro #1071]: #1073
#1057 := (iff #441 #1056)
#1054 := (iff #155 #1053)
#1055 := [monotonicity #1052]: #1054
#1058 := [monotonicity #1055]: #1057
#1077 := [monotonicity #1058 #1074]: #1076
#1080 := [quant-intro #1077]: #1079
#1083 := [monotonicity #1080]: #1082
#1110 := [monotonicity #1083 #1107]: #1109
#1113 := [monotonicity #1080 #1110]: #1112
#1122 := [monotonicity #1113]: #1121
#1125 := [monotonicity #1122]: #1124
#1128 := [monotonicity #1125]: #1127
#1131 := [monotonicity #1128]: #1130
#1134 := [monotonicity #1119 #1131]: #1133
#1139 := [trans #1134 #1137]: #1138
#1364 := [monotonicity #1139 #1361]: #1363
#1045 := (iff #768 #1044)
#1042 := (iff #423 #1041)
#1039 := (iff #418 #1038)
#1036 := (iff #411 #1035)
#1033 := (iff #408 #1030)
#1024 := (and #117 #1014)
#1027 := (and #1021 #1024)
#1031 := (iff #1027 #1030)
#1032 := [rewrite]: #1031
#1028 := (iff #408 #1027)
#1025 := (iff #405 #1024)
#1015 := (iff #402 #1014)
#1019 := [rewrite]: #1015
#1026 := [monotonicity #1019]: #1025
#1022 := (iff #133 #1021)
#1023 := [rewrite]: #1022
#1029 := [monotonicity #1023 #1026]: #1028
#1034 := [trans #1029 #1032]: #1033
#1037 := [quant-intro #1034]: #1036
#1012 := (iff #417 #1011)
#1009 := (iff #132 #1008)
#1010 := [monotonicity #1007]: #1009
#1013 := [monotonicity #1010]: #1012
#1040 := [monotonicity #1013 #1037]: #1039
#1043 := [quant-intro #1040]: #1042
#1046 := [monotonicity #1043]: #1045
#1408 := [monotonicity #1046 #1364]: #1407
#1381 := (iff #777 #1380)
#1378 := (iff #399 #1377)
#1375 := (iff #394 #1374)
#1372 := (iff #387 #1371)
#1373 := [rewrite]: #1372
#1369 := (iff #393 #1368)
#1366 := (iff #126 #1365)
#1367 := [monotonicity #943]: #1366
#1370 := [monotonicity #1367]: #1369
#1376 := [monotonicity #1370 #1373]: #1375
#1379 := [quant-intro #1376]: #1378
#1382 := [monotonicity #1379]: #1381
#1411 := [monotonicity #1382 #1408]: #1410
#1392 := (iff #786 #1391)
#1389 := (iff #381 #1388)
#1386 := (iff #378 #1385)
#1383 := (iff #123 #1020)
#1384 := [rewrite]: #1383
#1387 := [monotonicity #1384]: #1386
#1390 := [quant-intro #1387]: #1389
#1393 := [monotonicity #1390]: #1392
#1414 := [monotonicity #1393 #1411]: #1413
#1401 := (iff #795 #1400)
#1398 := (iff #114 #1397)
#1395 := (iff #113 #1394)
#1396 := [rewrite]: #1395
#1399 := [quant-intro #1396]: #1398
#1402 := [monotonicity #1399]: #1401
#1417 := [monotonicity #1402 #1414]: #1416
#1420 := [monotonicity #1417]: #1419
#1404 := (iff #820 #1403)
#1000 := (iff #374 #999)
#997 := (iff #371 #996)
#994 := (iff #106 #993)
#991 := (iff #105 #988)
#982 := (and #77 #976)
#985 := (and #979 #982)
#989 := (iff #985 #988)
#990 := [rewrite]: #989
#986 := (iff #105 #985)
#983 := (iff #104 #982)
#977 := (iff #103 #976)
#978 := [rewrite]: #977
#984 := [monotonicity #978]: #983
#980 := (iff #102 #979)
#981 := [rewrite]: #980
#987 := [monotonicity #981 #984]: #986
#992 := [trans #987 #990]: #991
#995 := [quant-intro #992]: #994
#974 := (iff #370 #973)
#971 := (iff #101 #970)
#968 := (iff #100 #967)
#969 := [rewrite]: #968
#972 := [monotonicity #969]: #971
#975 := [monotonicity #972]: #974
#998 := [monotonicity #975 #995]: #997
#1001 := [quant-intro #998]: #1000
#1405 := [monotonicity #1001]: #1404
#1423 := [monotonicity #1405 #1420]: #1422
#1428 := [trans #1423 #1426]: #1427
#1431 := [monotonicity #1001 #1428]: #1430
#962 := (iff #832 #961)
#959 := (iff #367 #958)
#956 := (iff #364 #955)
#950 := (iff #97 #951)
#952 := [rewrite]: #950
#948 := (iff #363 #947)
#945 := (iff #95 #944)
#946 := [monotonicity #943]: #945
#949 := [monotonicity #946]: #948
#957 := [monotonicity #949 #952]: #956
#960 := [quant-intro #957]: #959
#963 := [monotonicity #960]: #962
#1434 := [monotonicity #963 #1431]: #1433
#1437 := [monotonicity #960 #1434]: #1436
#936 := (iff #844 #935)
#933 := (iff #360 #932)
#930 := (iff #357 #929)
#924 := (iff #88 #925)
#928 := [rewrite]: #924
#931 := [monotonicity #928]: #930
#934 := [quant-intro #931]: #933
#937 := [monotonicity #934]: #936
#1440 := [monotonicity #937 #1437]: #1439
#1443 := [monotonicity #934 #1440]: #1442
#921 := (iff #856 #920)
#918 := (iff #83 #917)
#914 := (iff #82 #916)
#915 := [rewrite]: #914
#919 := [quant-intro #915]: #918
#922 := [monotonicity #919]: #921
#1446 := [monotonicity #922 #1443]: #1445
#1449 := [monotonicity #919 #1446]: #1448
#1452 := [monotonicity #1449]: #1451
#1455 := [monotonicity #1452]: #1454
#1458 := [monotonicity #1455]: #1457
#1461 := [monotonicity #1458]: #1460
#1464 := [monotonicity #1461]: #1463
#1469 := [trans #1464 #1467]: #1468
#1472 := [monotonicity #1469]: #1471
#912 := (iff #284 #911)
#909 := (iff #283 #899)
#904 := (implies true #899)
#907 := (iff #904 #899)
#908 := [rewrite]: #907
#905 := (iff #283 #904)
#902 := (iff #282 #899)
#895 := (implies #347 #890)
#900 := (iff #895 #899)
#901 := [rewrite]: #900
#896 := (iff #282 #895)
#893 := (iff #281 #890)
#886 := (implies #353 #881)
#891 := (iff #886 #890)
#892 := [rewrite]: #891
#887 := (iff #281 #886)
#884 := (iff #280 #881)
#877 := (implies #79 #874)
#882 := (iff #877 #881)
#883 := [rewrite]: #882
#878 := (iff #280 #877)
#875 := (iff #279 #874)
#872 := (iff #278 #869)
#865 := (implies #81 #862)
#870 := (iff #865 #869)
#871 := [rewrite]: #870
#866 := (iff #278 #865)
#863 := (iff #277 #862)
#860 := (iff #276 #857)
#853 := (implies #83 #850)
#858 := (iff #853 #857)
#859 := [rewrite]: #858
#854 := (iff #276 #853)
#851 := (iff #275 #850)
#848 := (iff #274 #845)
#841 := (implies #360 #838)
#846 := (iff #841 #845)
#847 := [rewrite]: #846
#842 := (iff #274 #841)
#839 := (iff #273 #838)
#836 := (iff #272 #833)
#829 := (implies #367 #826)
#834 := (iff #829 #833)
#835 := [rewrite]: #834
#830 := (iff #272 #829)
#827 := (iff #271 #826)
#824 := (iff #270 #821)
#817 := (implies #374 #805)
#822 := (iff #817 #821)
#823 := [rewrite]: #822
#818 := (iff #270 #817)
#815 := (iff #269 #805)
#810 := (implies true #805)
#813 := (iff #810 #805)
#814 := [rewrite]: #813
#811 := (iff #269 #810)
#808 := (iff #268 #805)
#801 := (implies #111 #796)
#806 := (iff #801 #805)
#807 := [rewrite]: #806
#802 := (iff #268 #801)
#799 := (iff #267 #796)
#792 := (implies #114 #787)
#797 := (iff #792 #796)
#798 := [rewrite]: #797
#793 := (iff #267 #792)
#790 := (iff #266 #787)
#783 := (implies #381 #778)
#788 := (iff #783 #787)
#789 := [rewrite]: #788
#784 := (iff #266 #783)
#781 := (iff #265 #778)
#774 := (implies #399 #769)
#779 := (iff #774 #778)
#780 := [rewrite]: #779
#775 := (iff #265 #774)
#772 := (iff #264 #769)
#765 := (implies #423 #762)
#770 := (iff #765 #769)
#771 := [rewrite]: #770
#766 := (iff #264 #765)
#763 := (iff #263 #762)
#760 := (iff #262 #750)
#755 := (implies true #750)
#758 := (iff #755 #750)
#759 := [rewrite]: #758
#756 := (iff #262 #755)
#753 := (iff #261 #750)
#747 := (implies #141 #742)
#751 := (iff #747 #750)
#752 := [rewrite]: #751
#748 := (iff #261 #747)
#745 := (iff #260 #742)
#739 := (implies #184 #734)
#743 := (iff #739 #742)
#744 := [rewrite]: #743
#740 := (iff #260 #739)
#737 := (iff #259 #734)
#730 := (implies #186 #725)
#735 := (iff #730 #734)
#736 := [rewrite]: #735
#731 := (iff #259 #730)
#728 := (iff #258 #725)
#721 := (implies #545 #716)
#726 := (iff #721 #725)
#727 := [rewrite]: #726
#722 := (iff #258 #721)
#719 := (iff #257 #716)
#712 := (implies #194 #707)
#717 := (iff #712 #716)
#718 := [rewrite]: #717
#713 := (iff #257 #712)
#710 := (iff #256 #707)
#703 := (implies #551 #698)
#708 := (iff #703 #707)
#709 := [rewrite]: #708
#704 := (iff #256 #703)
#701 := (iff #255 #698)
#694 := (implies #557 #691)
#699 := (iff #694 #698)
#700 := [rewrite]: #699
#695 := (iff #255 #694)
#692 := (iff #254 #691)
#689 := (iff #253 #686)
#682 := (implies #211 #679)
#687 := (iff #682 #686)
#688 := [rewrite]: #687
#683 := (iff #253 #682)
#680 := (iff #252 #679)
#677 := (iff #251 #674)
#670 := (implies #563 #667)
#675 := (iff #670 #674)
#676 := [rewrite]: #675
#671 := (iff #251 #670)
#668 := (iff #250 #667)
#665 := (iff #249 #662)
#658 := (implies #217 #655)
#663 := (iff #658 #662)
#664 := [rewrite]: #663
#659 := (iff #249 #658)
#656 := (iff #248 #655)
#653 := (iff #247 #650)
#646 := (implies #219 #643)
#651 := (iff #646 #650)
#652 := [rewrite]: #651
#647 := (iff #247 #646)
#644 := (iff #246 #643)
#641 := (iff #245 #638)
#634 := (implies #570 #631)
#639 := (iff #634 #638)
#640 := [rewrite]: #639
#635 := (iff #245 #634)
#632 := (iff #244 #631)
#629 := (iff #243 #626)
#622 := (implies #588 #612)
#627 := (iff #622 #626)
#628 := [rewrite]: #627
#623 := (iff #243 #622)
#620 := (iff #242 #612)
#615 := (and #612 true)
#618 := (iff #615 #612)
#619 := [rewrite]: #618
#616 := (iff #242 #615)
#613 := (iff #241 #612)
#610 := (iff #240 #607)
#603 := (implies #234 #600)
#608 := (iff #603 #607)
#609 := [rewrite]: #608
#604 := (iff #240 #603)
#601 := (iff #239 #600)
#598 := (iff #238 #597)
#595 := (iff #237 #594)
#592 := (iff #236 #591)
#574 := (= #229 #573)
#575 := [rewrite]: #574
#593 := [monotonicity #575]: #592
#596 := [monotonicity #593]: #595
#599 := [monotonicity #596]: #598
#602 := [quant-intro #599]: #601
#605 := [monotonicity #602]: #604
#611 := [trans #605 #609]: #610
#614 := [quant-intro #611]: #613
#617 := [monotonicity #614]: #616
#621 := [trans #617 #619]: #620
#589 := (iff #232 #588)
#586 := (iff #231 #583)
#579 := (implies #228 #576)
#584 := (iff #579 #583)
#585 := [rewrite]: #584
#580 := (iff #231 #579)
#577 := (iff #230 #576)
#578 := [monotonicity #575]: #577
#581 := [monotonicity #578]: #580
#587 := [trans #581 #585]: #586
#590 := [quant-intro #587]: #589
#624 := [monotonicity #590 #621]: #623
#630 := [trans #624 #628]: #629
#633 := [monotonicity #590 #630]: #632
#571 := (iff #227 #570)
#568 := (iff #226 #567)
#569 := [rewrite]: #568
#572 := [quant-intro #569]: #571
#636 := [monotonicity #572 #633]: #635
#642 := [trans #636 #640]: #641
#645 := [monotonicity #572 #642]: #644
#648 := [monotonicity #645]: #647
#654 := [trans #648 #652]: #653
#657 := [monotonicity #654]: #656
#660 := [monotonicity #657]: #659
#666 := [trans #660 #664]: #665
#669 := [monotonicity #666]: #668
#564 := (iff #215 #563)
#561 := (iff #214 #560)
#562 := [rewrite]: #561
#565 := [quant-intro #562]: #564
#672 := [monotonicity #565 #669]: #671
#678 := [trans #672 #676]: #677
#681 := [monotonicity #565 #678]: #680
#684 := [monotonicity #681]: #683
#690 := [trans #684 #688]: #689
#693 := [monotonicity #690]: #692
#558 := (iff #209 #557)
#555 := (iff #208 #554)
#556 := [rewrite]: #555
#559 := [quant-intro #556]: #558
#696 := [monotonicity #559 #693]: #695
#702 := [trans #696 #700]: #701
#552 := (iff #205 #551)
#549 := (iff #204 #548)
#550 := [rewrite]: #549
#553 := [quant-intro #550]: #552
#705 := [monotonicity #553 #702]: #704
#711 := [trans #705 #709]: #710
#714 := [monotonicity #711]: #713
#720 := [trans #714 #718]: #719
#546 := (iff #189 #545)
#543 := (iff #188 #542)
#544 := [rewrite]: #543
#547 := [quant-intro #544]: #546
#723 := [monotonicity #547 #720]: #722
#729 := [trans #723 #727]: #728
#732 := [monotonicity #729]: #731
#738 := [trans #732 #736]: #737
#741 := [monotonicity #738]: #740
#746 := [trans #741 #744]: #745
#749 := [monotonicity #746]: #748
#754 := [trans #749 #752]: #753
#757 := [monotonicity #754]: #756
#761 := [trans #757 #759]: #760
#540 := (iff #180 #530)
#535 := (implies true #530)
#538 := (iff #535 #530)
#539 := [rewrite]: #538
#536 := (iff #180 #535)
#533 := (iff #179 #530)
#527 := (implies #142 #522)
#531 := (iff #527 #530)
#532 := [rewrite]: #531
#528 := (iff #179 #527)
#525 := (iff #178 #522)
#518 := (implies #144 #513)
#523 := (iff #518 #522)
#524 := [rewrite]: #523
#519 := (iff #178 #518)
#516 := (iff #177 #513)
#509 := (implies #147 #504)
#514 := (iff #509 #513)
#515 := [rewrite]: #514
#510 := (iff #177 #509)
#507 := (iff #176 #504)
#500 := (implies #149 #495)
#505 := (iff #500 #504)
#506 := [rewrite]: #505
#501 := (iff #176 #500)
#498 := (iff #175 #495)
#491 := (implies #152 #488)
#496 := (iff #491 #495)
#497 := [rewrite]: #496
#492 := (iff #175 #491)
#489 := (iff #174 #488)
#486 := (iff #173 #483)
#479 := (implies #447 #476)
#484 := (iff #479 #483)
#485 := [rewrite]: #484
#480 := (iff #173 #479)
#477 := (iff #172 #476)
#474 := (iff #171 #471)
#467 := (implies #462 #169)
#472 := (iff #467 #471)
#473 := [rewrite]: #472
#468 := (iff #171 #467)
#465 := (iff #170 #169)
#466 := [rewrite]: #465
#463 := (iff #167 #462)
#460 := (iff #166 #457)
#453 := (implies #164 #450)
#458 := (iff #453 #457)
#459 := [rewrite]: #458
#454 := (iff #166 #453)
#451 := (iff #165 #450)
#427 := (= #158 #426)
#428 := [rewrite]: #427
#452 := [monotonicity #428]: #451
#455 := [monotonicity #452]: #454
#461 := [trans #455 #459]: #460
#464 := [quant-intro #461]: #463
#469 := [monotonicity #464 #466]: #468
#475 := [trans #469 #473]: #474
#478 := [monotonicity #464 #475]: #477
#448 := (iff #163 #447)
#445 := (iff #162 #442)
#438 := (implies #155 #435)
#443 := (iff #438 #442)
#444 := [rewrite]: #443
#439 := (iff #162 #438)
#436 := (iff #161 #435)
#433 := (iff #160 #432)
#430 := (iff #159 #429)
#431 := [monotonicity #428]: #430
#434 := [monotonicity #431]: #433
#437 := [quant-intro #434]: #436
#440 := [monotonicity #437]: #439
#446 := [trans #440 #444]: #445
#449 := [quant-intro #446]: #448
#481 := [monotonicity #449 #478]: #480
#487 := [trans #481 #485]: #486
#490 := [monotonicity #449 #487]: #489
#493 := [monotonicity #490]: #492
#499 := [trans #493 #497]: #498
#502 := [monotonicity #499]: #501
#508 := [trans #502 #506]: #507
#511 := [monotonicity #508]: #510
#517 := [trans #511 #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
#764 := [monotonicity #541 #761]: #763
#424 := (iff #139 #423)
#421 := (iff #138 #418)
#414 := (implies #132 #411)
#419 := (iff #414 #418)
#420 := [rewrite]: #419
#415 := (iff #138 #414)
#412 := (iff #137 #411)
#409 := (iff #136 #408)
#406 := (iff #135 #405)
#403 := (iff #134 #402)
#385 := (= #127 #384)
#386 := [rewrite]: #385
#404 := [monotonicity #386]: #403
#407 := [monotonicity #404]: #406
#410 := [monotonicity #407]: #409
#413 := [quant-intro #410]: #412
#416 := [monotonicity #413]: #415
#422 := [trans #416 #420]: #421
#425 := [quant-intro #422]: #424
#767 := [monotonicity #425 #764]: #766
#773 := [trans #767 #771]: #772
#400 := (iff #130 #399)
#397 := (iff #129 #394)
#390 := (implies #126 #387)
#395 := (iff #390 #394)
#396 := [rewrite]: #395
#391 := (iff #129 #390)
#388 := (iff #128 #387)
#389 := [monotonicity #386]: #388
#392 := [monotonicity #389]: #391
#398 := [trans #392 #396]: #397
#401 := [quant-intro #398]: #400
#776 := [monotonicity #401 #773]: #775
#782 := [trans #776 #780]: #781
#382 := (iff #125 #381)
#379 := (iff #124 #378)
#380 := [rewrite]: #379
#383 := [quant-intro #380]: #382
#785 := [monotonicity #383 #782]: #784
#791 := [trans #785 #789]: #790
#794 := [monotonicity #791]: #793
#800 := [trans #794 #798]: #799
#803 := [monotonicity #800]: #802
#809 := [trans #803 #807]: #808
#812 := [monotonicity #809]: #811
#816 := [trans #812 #814]: #815
#375 := (iff #108 #374)
#372 := (iff #107 #371)
#373 := [rewrite]: #372
#376 := [quant-intro #373]: #375
#819 := [monotonicity #376 #816]: #818
#825 := [trans #819 #823]: #824
#828 := [monotonicity #376 #825]: #827
#368 := (iff #99 #367)
#365 := (iff #98 #364)
#366 := [rewrite]: #365
#369 := [quant-intro #366]: #368
#831 := [monotonicity #369 #828]: #830
#837 := [trans #831 #835]: #836
#840 := [monotonicity #369 #837]: #839
#361 := (iff #90 #360)
#358 := (iff #89 #357)
#359 := [rewrite]: #358
#362 := [quant-intro #359]: #361
#843 := [monotonicity #362 #840]: #842
#849 := [trans #843 #847]: #848
#852 := [monotonicity #362 #849]: #851
#855 := [monotonicity #852]: #854
#861 := [trans #855 #859]: #860
#864 := [monotonicity #861]: #863
#867 := [monotonicity #864]: #866
#873 := [trans #867 #871]: #872
#876 := [monotonicity #873]: #875
#879 := [monotonicity #876]: #878
#885 := [trans #879 #883]: #884
#354 := (iff #74 #353)
#351 := (iff #73 #350)
#352 := [rewrite]: #351
#355 := [quant-intro #352]: #354
#888 := [monotonicity #355 #885]: #887
#894 := [trans #888 #892]: #893
#348 := (iff #70 #347)
#345 := (iff #69 #344)
#346 := [rewrite]: #345
#349 := [quant-intro #346]: #348
#897 := [monotonicity #349 #894]: #896
#903 := [trans #897 #901]: #902
#906 := [monotonicity #903]: #905
#910 := [trans #906 #908]: #909
#913 := [monotonicity #910]: #912
#1474 := [trans #913 #1472]: #1473
#343 := [asserted]: #284
#1475 := [mp #343 #1474]: #1470
#1477 := [not-or-elim #1475]: #353
#1532 := [mp~ #1477 #1501]: #353
#3659 := [mp #1532 #3658]: #3654
#3289 := (not #3654)
#5853 := (or #3289 #1614 #6574)
#6575 := (or #1614 #6574)
#6155 := (or #3289 #6575)
#6156 := (iff #6155 #5853)
#6165 := [rewrite]: #6156
#5702 := [quant-inst #1613]: #6155
#6166 := [mp #5702 #6165]: #5853
#6626 := [unit-resolution #6166 #3659 #6625]: #6574
#6631 := [mp #6626 #6630]: #6176
#6615 := (not #6176)
#1620 := (not #1619)
#3595 := (or #3702 #1620)
#3596 := [def-axiom]: #3595
#5852 := [unit-resolution #3596 #5790]: #1620
#6616 := (or #6615 #1619)
#6622 := [th-lemma arith triangle-eq]: #6616
#6624 := [unit-resolution #6622 #5852]: #6615
#6632 := [unit-resolution #6624 #6631]: false
#6633 := [lemma #6632]: #3702
#3986 := (or #3705 #3983)
#3989 := (not #3986)
#2540 := (or #78 #940 #951)
#3685 := (forall (vars (?v0 S2) (?v1 S2)) (:pat #3684) #2540)
#3690 := (not #3685)
#3992 := (or #3690 #3989)
#3995 := (not #3992)
decl ?v0!4 :: S2
#1582 := ?v0!4
#1595 := (f17 ?v0!4)
#1596 := (* -1::Int #1595)
decl ?v1!3 :: S2
#1581 := ?v1!3
#1594 := (f17 ?v1!3)
#2173 := (+ #1594 #1596)
#1585 := (f6 f7 ?v1!3)
#1586 := (f5 #1585 ?v0!4)
#1587 := (f4 #1586)
#2174 := (+ #1587 #2173)
#2177 := (>= #2174 0::Int)
#1588 := (* -1::Int #1587)
#1589 := (+ f3 #1588)
#1590 := (<= #1589 0::Int)
#1583 := (f11 f18 ?v1!3)
#1584 := (= #1583 f1)
#2503 := (not #1584)
#2518 := (or #2503 #1590 #2177)
#2523 := (not #2518)
#3998 := (or #2523 #3995)
#4001 := (not #3998)
#3675 := (pattern #67 #87)
#1605 := (not #85)
#2495 := (or #77 #1605 #925)
#3676 := (forall (vars (?v0 S2) (?v1 S2)) (:pat #3675) #2495)
#3681 := (not #3676)
#4004 := (or #3681 #4001)
#4007 := (not #4004)
decl ?v0!2 :: S2
#1555 := ?v0!2
#1564 := (f17 ?v0!2)
#1565 := (* -1::Int #1564)
decl ?v1!1 :: S2
#1554 := ?v1!1
#1563 := (f17 ?v1!1)
#1566 := (+ #1563 #1565)
#1567 := (>= #1566 0::Int)
#1559 := (f11 f18 ?v0!2)
#1560 := (= #1559 f1)
#1884 := (not #1560)
#1556 := (f11 f18 ?v1!1)
#1557 := (= #1556 f1)
#1841 := (or #1557 #1884 #1567)
#1946 := (not #1841)
#4010 := (or #1946 #4007)
#4013 := (not #4010)
#3667 := (forall (vars (?v0 S2)) (:pat #3647) #916)
#3672 := (not #3667)
#4016 := (or #3672 #4013)
#4019 := (not #4016)
decl ?v0!0 :: S2
#1539 := ?v0!0
#1540 := (f17 ?v0!0)
#1541 := (>= #1540 0::Int)
#3259 := (= f3 #1540)
#3321 := (= #1540 f3)
#3223 := (iff #3321 #3259)
#3224 := (iff #3259 #3321)
#3227 := [commutativity]: #3224
#3222 := [symm #3227]: #3223
#3345 := (= ?v0!0 f16)
#3353 := (not #3345)
#3306 := (= #1540 0::Int)
#3281 := (not #3306)
#1542 := (not #1541)
#3290 := [hypothesis]: #1542
#3246 := (or #3281 #1541)
#3244 := [th-lemma arith triangle-eq]: #3246
#3247 := [unit-resolution #3244 #3290]: #3281
#3648 := (forall (vars (?v0 S2)) (:pat #3647) #344)
#3651 := (iff #347 #3648)
#3649 := (iff #344 #344)
#3650 := [refl]: #3649
#3652 := [quant-intro #3650]: #3651
#1498 := (~ #347 #347)
#1527 := (~ #344 #344)
#1528 := [refl]: #1527
#1499 := [nnf-pos #1528]: #1498
#1476 := [not-or-elim #1475]: #347
#1529 := [mp~ #1476 #1499]: #347
#3653 := [mp #1529 #3652]: #3648
#3310 := (not #3648)
#3309 := (or #3310 #3353 #3306)
#3307 := (or #3353 #3306)
#3303 := (or #3310 #3307)
#3294 := (iff #3303 #3309)
#3295 := [rewrite]: #3294
#3304 := [quant-inst #1539]: #3303
#3305 := [mp #3304 #3295]: #3309
#3236 := [unit-resolution #3305 #3653 #3247]: #3353
#3291 := (or #3289 #3345 #3321)
#3308 := (or #3345 #3321)
#3258 := (or #3289 #3308)
#3268 := (iff #3258 #3291)
#3269 := [rewrite]: #3268
#3260 := [quant-inst #1539]: #3258
#3267 := [mp #3260 #3269]: #3291
#3248 := [unit-resolution #3267 #3659 #3236]: #3321
#3228 := [mp #3248 #3222]: #3259
#3316 := (* -1::Int #1540)
#3270 := (+ f3 #3316)
#3253 := (<= #3270 0::Int)
#4045 := (not #3253)
#307 := (<= f3 0::Int)
#308 := (not #307)
#9 := (< 0::Int f3)
#309 := (iff #9 #308)
#310 := [rewrite]: #309
#304 := [asserted]: #9
#311 := [mp #304 #310]: #308
#3286 := (<= #1540 0::Int)
#3203 := (or #3286 #1541)
#3208 := [th-lemma arith farkas 1 1]: #3203
#3213 := [unit-resolution #3208 #3290]: #3286
#4046 := (not #3286)
#4047 := (or #4045 #307 #4046)
#4048 := [th-lemma arith assign-bounds 1 1]: #4047
#4049 := [unit-resolution #4048 #3213 #311]: #4045
#4044 := (not #3259)
#4050 := (or #4044 #3253)
#4051 := [th-lemma arith triangle-eq]: #4050
#4052 := [unit-resolution #4051 #4049 #3228]: false
#4053 := [lemma #4052]: #1541
#4022 := (or #1542 #4019)
#4025 := (not #4022)
#4028 := (or #868 #4025)
#4031 := (not #4028)
#4121 := [hypothesis]: #868
#4075 := (or #3310 #81)
#6826 := (= f16 f16)
#6905 := (not #6826)
#4054 := (or #6905 #81)
#4076 := (or #3310 #4054)
#4084 := (iff #4076 #4075)
#4117 := (iff #4075 #4075)
#4118 := [rewrite]: #4117
#4073 := (iff #4054 #81)
#4068 := (or false #81)
#4069 := (iff #4068 #81)
#4072 := [rewrite]: #4069
#4070 := (iff #4054 #4068)
#6915 := (iff #6905 false)
#6910 := (not true)
#6913 := (iff #6910 false)
#6914 := [rewrite]: #6913
#6911 := (iff #6905 #6910)
#6829 := (iff #6826 true)
#6830 := [rewrite]: #6829
#6912 := [monotonicity #6830]: #6911
#6916 := [trans #6912 #6914]: #6915
#4071 := [monotonicity #6916]: #4070
#4074 := [trans #4071 #4072]: #4073
#4085 := [monotonicity #4074]: #4084
#4119 := [trans #4085 #4118]: #4084
#4077 := [quant-inst #65]: #4076
#4120 := [mp #4077 #4119]: #4075
#4116 := [unit-resolution #4120 #3653 #4121]: false
#4122 := [lemma #4116]: #81
#4034 := (or #868 #4031)
#2953 := (forall (vars (?v1 S2)) #2942)
#2960 := (not #2953)
#2938 := (forall (vars (?v0 S2) (?v1 S2)) #2933)
#2959 := (not #2938)
#2961 := (or #2959 #2035 #2040 #2960)
#2962 := (not #2961)
#2967 := (or #2916 #2962)
#2974 := (not #2967)
#2893 := (forall (vars (?v0 S2) (?v1 S2)) #2888)
#2973 := (not #2893)
#2975 := (or #2973 #2974)
#2976 := (not #2975)
#2981 := (or #2870 #2976)
#2987 := (not #2981)
#2988 := (or #1182 #2987)
#2989 := (not #2988)
#2994 := (or #1963 #2989)
#3000 := (not #2994)
#3001 := (or #661 #3000)
#3002 := (not #3001)
#3007 := (or #661 #3002)
#3013 := (not #3007)
#3014 := (or #673 #3013)
#3015 := (not #3014)
#3020 := (or #1943 #3015)
#3026 := (not #3020)
#3027 := (or #1173 #3026)
#3028 := (not #3027)
#3033 := (or #1923 #3028)
#3041 := (not #3033)
#2847 := (forall (vars (?v0 S2)) #2844)
#3040 := (not #2847)
#2841 := (forall (vars (?v0 S2)) #2836)
#3039 := (not #2841)
#3042 := (or #1874 #1879 #183 #1322 #1318 #715 #3039 #3040 #3041)
#3043 := (not #3042)
#2781 := (forall (vars (?v0 S2) (?v1 S2)) #2776)
#2787 := (not #2781)
#2788 := (or #2787 #169)
#2789 := (not #2788)
#2794 := (or #2759 #2789)
#2801 := (not #2794)
#2737 := (forall (vars (?v0 S2)) #2732)
#2800 := (not #2737)
#2802 := (or #2800 #2801)
#2803 := (not #2802)
#2700 := (forall (vars (?v1 S2)) #2689)
#2706 := (not #2700)
#2707 := (or #1752 #1757 #2706)
#2708 := (not #2707)
#2808 := (or #2708 #2803)
#2815 := (not #2808)
#2685 := (forall (vars (?v0 S2)) #2674)
#2814 := (not #2685)
#2816 := (or #2814 #521 #512 #503 #494 #2815)
#2817 := (not #2816)
#3048 := (or #2817 #3043)
#3058 := (not #3048)
#2671 := (forall (vars (?v0 S2)) #2666)
#3057 := (not #2671)
#2643 := (forall (vars (?v0 S2) (?v1 S2)) #2638)
#3056 := (not #2643)
#2621 := (forall (vars (?v0 S2) (?v1 S2)) #2616)
#3055 := (not #2621)
#2598 := (forall (vars (?v0 S2)) #2593)
#3054 := (not #2598)
#3059 := (or #3054 #804 #1400 #3055 #3056 #3057 #3058)
#3060 := (not #3059)
#2560 := (forall (vars (?v1 S2)) #2549)
#2566 := (not #2560)
#2567 := (or #1614 #1619 #2566)
#2568 := (not #2567)
#3065 := (or #2568 #3060)
#3072 := (not #3065)
#2545 := (forall (vars (?v0 S2) (?v1 S2)) #2540)
#3071 := (not #2545)
#3073 := (or #3071 #3072)
#3074 := (not #3073)
#3079 := (or #2523 #3074)
#3086 := (not #3079)
#2500 := (forall (vars (?v0 S2) (?v1 S2)) #2495)
#3085 := (not #2500)
#3087 := (or #3085 #3086)
#3088 := (not #3087)
#3093 := (or #1946 #3088)
#3099 := (not #3093)
#3100 := (or #920 #3099)
#3101 := (not #3100)
#3106 := (or #1542 #3101)
#3112 := (not #3106)
#3113 := (or #868 #3112)
#3114 := (not #3113)
#3119 := (or #868 #3114)
#4035 := (iff #3119 #4034)
#4032 := (iff #3114 #4031)
#4029 := (iff #3113 #4028)
#4026 := (iff #3112 #4025)
#4023 := (iff #3106 #4022)
#4020 := (iff #3101 #4019)
#4017 := (iff #3100 #4016)
#4014 := (iff #3099 #4013)
#4011 := (iff #3093 #4010)
#4008 := (iff #3088 #4007)
#4005 := (iff #3087 #4004)
#4002 := (iff #3086 #4001)
#3999 := (iff #3079 #3998)
#3996 := (iff #3074 #3995)
#3993 := (iff #3073 #3992)
#3990 := (iff #3072 #3989)
#3987 := (iff #3065 #3986)
#3984 := (iff #3060 #3983)
#3981 := (iff #3059 #3980)
#3978 := (iff #3058 #3977)
#3975 := (iff #3048 #3974)
#3972 := (iff #3043 #3971)
#3969 := (iff #3042 #3968)
#3966 := (iff #3041 #3965)
#3963 := (iff #3033 #3962)
#3960 := (iff #3028 #3959)
#3957 := (iff #3027 #3956)
#3954 := (iff #3026 #3953)
#3951 := (iff #3020 #3950)
#3948 := (iff #3015 #3947)
#3945 := (iff #3014 #3944)
#3942 := (iff #3013 #3941)
#3939 := (iff #3007 #3938)
#3936 := (iff #3002 #3935)
#3933 := (iff #3001 #3932)
#3930 := (iff #3000 #3929)
#3927 := (iff #2994 #3926)
#3924 := (iff #2989 #3923)
#3921 := (iff #2988 #3920)
#3918 := (iff #2987 #3917)
#3915 := (iff #2981 #3914)
#3912 := (iff #2976 #3911)
#3909 := (iff #2975 #3908)
#3906 := (iff #2974 #3905)
#3903 := (iff #2967 #3902)
#3900 := (iff #2962 #3899)
#3897 := (iff #2961 #3896)
#3894 := (iff #2960 #3893)
#3891 := (iff #2953 #3888)
#3889 := (iff #2942 #2942)
#3890 := [refl]: #3889
#3892 := [quant-intro #3890]: #3891
#3895 := [monotonicity #3892]: #3894
#3886 := (iff #2959 #3885)
#3883 := (iff #2938 #3880)
#3881 := (iff #2933 #2933)
#3882 := [refl]: #3881
#3884 := [quant-intro #3882]: #3883
#3887 := [monotonicity #3884]: #3886
#3898 := [monotonicity #3887 #3895]: #3897
#3901 := [monotonicity #3898]: #3900
#3904 := [monotonicity #3901]: #3903
#3907 := [monotonicity #3904]: #3906
#3878 := (iff #2973 #3877)
#3875 := (iff #2893 #3872)
#3873 := (iff #2888 #2888)
#3874 := [refl]: #3873
#3876 := [quant-intro #3874]: #3875
#3879 := [monotonicity #3876]: #3878
#3910 := [monotonicity #3879 #3907]: #3909
#3913 := [monotonicity #3910]: #3912
#3916 := [monotonicity #3913]: #3915
#3919 := [monotonicity #3916]: #3918
#3869 := (iff #1182 #3868)
#3866 := (iff #1179 #3863)
#3864 := (iff #1176 #1176)
#3865 := [refl]: #3864
#3867 := [quant-intro #3865]: #3866
#3870 := [monotonicity #3867]: #3869
#3922 := [monotonicity #3870 #3919]: #3921
#3925 := [monotonicity #3922]: #3924
#3928 := [monotonicity #3925]: #3927
#3931 := [monotonicity #3928]: #3930
#3934 := [monotonicity #3931]: #3933
#3937 := [monotonicity #3934]: #3936
#3940 := [monotonicity #3937]: #3939
#3943 := [monotonicity #3940]: #3942
#3861 := (iff #673 #3860)
#3858 := (iff #563 #3855)
#3856 := (iff #560 #560)
#3857 := [refl]: #3856
#3859 := [quant-intro #3857]: #3858
#3862 := [monotonicity #3859]: #3861
#3946 := [monotonicity #3862 #3943]: #3945
#3949 := [monotonicity #3946]: #3948
#3952 := [monotonicity #3949]: #3951
#3955 := [monotonicity #3952]: #3954
#3852 := (iff #1173 #3851)
#3849 := (iff #1170 #3846)
#3847 := (iff #1165 #1165)
#3848 := [refl]: #3847
#3850 := [quant-intro #3848]: #3849
#3853 := [monotonicity #3850]: #3852
#3958 := [monotonicity #3853 #3955]: #3957
#3961 := [monotonicity #3958]: #3960
#3964 := [monotonicity #3961]: #3963
#3967 := [monotonicity #3964]: #3966
#3844 := (iff #3040 #3843)
#3841 := (iff #2847 #3838)
#3839 := (iff #2844 #2844)
#3840 := [refl]: #3839
#3842 := [quant-intro #3840]: #3841
#3845 := [monotonicity #3842]: #3844
#3836 := (iff #3039 #3835)
#3833 := (iff #2841 #3830)
#3831 := (iff #2836 #2836)
#3832 := [refl]: #3831
#3834 := [quant-intro #3832]: #3833
#3837 := [monotonicity #3834]: #3836
#3826 := (iff #1318 #3825)
#3823 := (iff #1315 #3820)
#3821 := (iff #1312 #1312)
#3822 := [refl]: #3821
#3824 := [quant-intro #3822]: #3823
#3827 := [monotonicity #3824]: #3826
#3970 := [monotonicity #3827 #3837 #3845 #3967]: #3969
#3973 := [monotonicity #3970]: #3972
#3818 := (iff #2817 #3817)
#3815 := (iff #2816 #3814)
#3812 := (iff #2815 #3811)
#3809 := (iff #2808 #3808)
#3806 := (iff #2803 #3805)
#3803 := (iff #2802 #3802)
#3800 := (iff #2801 #3799)
#3797 := (iff #2794 #3796)
#3794 := (iff #2789 #3793)
#3791 := (iff #2788 #3790)
#3788 := (iff #2787 #3787)
#3785 := (iff #2781 #3782)
#3783 := (iff #2776 #2776)
#3784 := [refl]: #3783
#3786 := [quant-intro #3784]: #3785
#3789 := [monotonicity #3786]: #3788
#3792 := [monotonicity #3789]: #3791
#3795 := [monotonicity #3792]: #3794
#3798 := [monotonicity #3795]: #3797
#3801 := [monotonicity #3798]: #3800
#3780 := (iff #2800 #3779)
#3777 := (iff #2737 #3774)
#3775 := (iff #2732 #2732)
#3776 := [refl]: #3775
#3778 := [quant-intro #3776]: #3777
#3781 := [monotonicity #3778]: #3780
#3804 := [monotonicity #3781 #3801]: #3803
#3807 := [monotonicity #3804]: #3806
#3772 := (iff #2708 #3771)
#3769 := (iff #2707 #3768)
#3766 := (iff #2706 #3765)
#3763 := (iff #2700 #3760)
#3761 := (iff #2689 #2689)
#3762 := [refl]: #3761
#3764 := [quant-intro #3762]: #3763
#3767 := [monotonicity #3764]: #3766
#3770 := [monotonicity #3767]: #3769
#3773 := [monotonicity #3770]: #3772
#3810 := [monotonicity #3773 #3807]: #3809
#3813 := [monotonicity #3810]: #3812
#3757 := (iff #2814 #3756)
#3754 := (iff #2685 #3751)
#3752 := (iff #2674 #2674)
#3753 := [refl]: #3752
#3755 := [quant-intro #3753]: #3754
#3758 := [monotonicity #3755]: #3757
#3816 := [monotonicity #3758 #3813]: #3815
#3819 := [monotonicity #3816]: #3818
#3976 := [monotonicity #3819 #3973]: #3975
#3979 := [monotonicity #3976]: #3978
#3748 := (iff #3057 #3747)
#3745 := (iff #2671 #3742)
#3743 := (iff #2666 #2666)
#3744 := [refl]: #3743
#3746 := [quant-intro #3744]: #3745
#3749 := [monotonicity #3746]: #3748
#3740 := (iff #3056 #3739)
#3737 := (iff #2643 #3734)
#3735 := (iff #2638 #2638)
#3736 := [refl]: #3735
#3738 := [quant-intro #3736]: #3737
#3741 := [monotonicity #3738]: #3740
#3732 := (iff #3055 #3731)
#3729 := (iff #2621 #3726)
#3727 := (iff #2616 #2616)
#3728 := [refl]: #3727
#3730 := [quant-intro #3728]: #3729
#3733 := [monotonicity #3730]: #3732
#3723 := (iff #1400 #3722)
#3720 := (iff #1397 #3717)
#3718 := (iff #1394 #1394)
#3719 := [refl]: #3718
#3721 := [quant-intro #3719]: #3720
#3724 := [monotonicity #3721]: #3723
#3714 := (iff #3054 #3713)
#3711 := (iff #2598 #3708)
#3709 := (iff #2593 #2593)
#3710 := [refl]: #3709
#3712 := [quant-intro #3710]: #3711
#3715 := [monotonicity #3712]: #3714
#3982 := [monotonicity #3715 #3724 #3733 #3741 #3749 #3979]: #3981
#3985 := [monotonicity #3982]: #3984
#3706 := (iff #2568 #3705)
#3703 := (iff #2567 #3702)
#3700 := (iff #2566 #3699)
#3697 := (iff #2560 #3694)
#3695 := (iff #2549 #2549)
#3696 := [refl]: #3695
#3698 := [quant-intro #3696]: #3697
#3701 := [monotonicity #3698]: #3700
#3704 := [monotonicity #3701]: #3703
#3707 := [monotonicity #3704]: #3706
#3988 := [monotonicity #3707 #3985]: #3987
#3991 := [monotonicity #3988]: #3990
#3691 := (iff #3071 #3690)
#3688 := (iff #2545 #3685)
#3686 := (iff #2540 #2540)
#3687 := [refl]: #3686
#3689 := [quant-intro #3687]: #3688
#3692 := [monotonicity #3689]: #3691
#3994 := [monotonicity #3692 #3991]: #3993
#3997 := [monotonicity #3994]: #3996
#4000 := [monotonicity #3997]: #3999
#4003 := [monotonicity #4000]: #4002
#3682 := (iff #3085 #3681)
#3679 := (iff #2500 #3676)
#3677 := (iff #2495 #2495)
#3678 := [refl]: #3677
#3680 := [quant-intro #3678]: #3679
#3683 := [monotonicity #3680]: #3682
#4006 := [monotonicity #3683 #4003]: #4005
#4009 := [monotonicity #4006]: #4008
#4012 := [monotonicity #4009]: #4011
#4015 := [monotonicity #4012]: #4014
#3673 := (iff #920 #3672)
#3670 := (iff #917 #3667)
#3668 := (iff #916 #916)
#3669 := [refl]: #3668
#3671 := [quant-intro #3669]: #3670
#3674 := [monotonicity #3671]: #3673
#4018 := [monotonicity #3674 #4015]: #4017
#4021 := [monotonicity #4018]: #4020
#4024 := [monotonicity #4021]: #4023
#4027 := [monotonicity #4024]: #4026
#4030 := [monotonicity #4027]: #4029
#4033 := [monotonicity #4030]: #4032
#4036 := [monotonicity #4033]: #4035
#2046 := (not #2045)
#2390 := (and #2046 #213 #2387)
#2393 := (not #2390)
#2396 := (forall (vars (?v1 S2)) #2393)
#2041 := (not #2040)
#2036 := (not #2035)
#2405 := (and #1212 #2036 #2041 #2396)
#2012 := (not #2011)
#2013 := (and #2005 #2012)
#2014 := (not #2013)
#2021 := (or #2014 #2020)
#2022 := (not #2021)
#2410 := (or #2022 #2405)
#2413 := (and #1193 #2410)
#1979 := (not #1978)
#1982 := (and #1979 #1981)
#1983 := (not #1982)
#1989 := (or #1983 #1988)
#1990 := (not #1989)
#2416 := (or #1990 #2413)
#2419 := (and #1179 #2416)
#2422 := (or #1963 #2419)
#2425 := (and #217 #2422)
#2428 := (or #661 #2425)
#2431 := (and #563 #2428)
#2434 := (or #1943 #2431)
#2437 := (and #1170 #2434)
#2440 := (or #1923 #2437)
#1880 := (not #1879)
#1875 := (not #1874)
#2446 := (and #1875 #1880 #184 #1323 #1315 #194 #1302 #1159 #2440)
#1849 := (not #169)
#1852 := (and #1096 #1849)
#1828 := (not #1827)
#1821 := (not #1820)
#1829 := (and #1821 #1828)
#1830 := (not #1829)
#2359 := (or #1830 #2356)
#2362 := (not #2359)
#2365 := (or #2362 #1852)
#2325 := (not #2320)
#2343 := (and #2325 #2338)
#2346 := (or #1056 #2343)
#2349 := (forall (vars (?v0 S2)) #2346)
#2368 := (and #2349 #2365)
#1763 := (not #1762)
#2295 := (and #1763 #2292)
#2298 := (not #2295)
#2301 := (forall (vars (?v1 S2)) #2298)
#1758 := (not #1757)
#1753 := (not #1752)
#2307 := (and #1753 #1758 #2301)
#2371 := (or #2307 #2368)
#1733 := (not #1114)
#1736 := (forall (vars (?v0 S2)) #1733)
#2374 := (and #1736 #144 #147 #149 #152 #2371)
#2451 := (or #2374 #2446)
#2251 := (not #2246)
#2269 := (and #2251 #1713 #2264)
#2272 := (or #1011 #2269)
#2275 := (forall (vars (?v0 S2)) #2272)
#2209 := (not #2204)
#2227 := (and #2209 #1660 #2222)
#2230 := (or #973 #2227)
#2233 := (forall (vars (?v0 S2)) #2230)
#2454 := (and #2233 #111 #1397 #1388 #1377 #2275 #2451)
#1625 := (not #1624)
#1631 := (and #1625 #77 #1630)
#1640 := (not #1631)
#1643 := (forall (vars (?v1 S2)) #1640)
#2191 := (and #1615 #1620 #1643)
#2457 := (or #2191 #2454)
#2460 := (and #958 #2457)
#1591 := (not #1590)
#1592 := (and #1584 #1591)
#1593 := (not #1592)
#2180 := (or #1593 #2177)
#2183 := (not #2180)
#2463 := (or #2183 #2460)
#2466 := (and #932 #2463)
#1558 := (not #1557)
#1561 := (and #1558 #1560)
#1562 := (not #1561)
#1568 := (or #1562 #1567)
#1569 := (not #1568)
#2469 := (or #1569 #2466)
#2472 := (and #917 #2469)
#2475 := (or #1542 #2472)
#2478 := (and #81 #2475)
#2481 := (or #868 #2478)
#3120 := (iff #2481 #3119)
#3117 := (iff #2478 #3114)
#3109 := (and #81 #3106)
#3115 := (iff #3109 #3114)
#3116 := [rewrite]: #3115
#3110 := (iff #2478 #3109)
#3107 := (iff #2475 #3106)
#3104 := (iff #2472 #3101)
#3096 := (and #917 #3093)
#3102 := (iff #3096 #3101)
#3103 := [rewrite]: #3102
#3097 := (iff #2472 #3096)
#3094 := (iff #2469 #3093)
#3091 := (iff #2466 #3088)
#3082 := (and #2500 #3079)
#3089 := (iff #3082 #3088)
#3090 := [rewrite]: #3089
#3083 := (iff #2466 #3082)
#3080 := (iff #2463 #3079)
#3077 := (iff #2460 #3074)
#3068 := (and #2545 #3065)
#3075 := (iff #3068 #3074)
#3076 := [rewrite]: #3075
#3069 := (iff #2460 #3068)
#3066 := (iff #2457 #3065)
#3063 := (iff #2454 #3060)
#3051 := (and #2598 #111 #1397 #2621 #2643 #2671 #3048)
#3061 := (iff #3051 #3060)
#3062 := [rewrite]: #3061
#3052 := (iff #2454 #3051)
#3049 := (iff #2451 #3048)
#3046 := (iff #2446 #3043)
#3036 := (and #1875 #1880 #184 #1323 #1315 #194 #2841 #2847 #3033)
#3044 := (iff #3036 #3043)
#3045 := [rewrite]: #3044
#3037 := (iff #2446 #3036)
#3034 := (iff #2440 #3033)
#3031 := (iff #2437 #3028)
#3023 := (and #1170 #3020)
#3029 := (iff #3023 #3028)
#3030 := [rewrite]: #3029
#3024 := (iff #2437 #3023)
#3021 := (iff #2434 #3020)
#3018 := (iff #2431 #3015)
#3010 := (and #563 #3007)
#3016 := (iff #3010 #3015)
#3017 := [rewrite]: #3016
#3011 := (iff #2431 #3010)
#3008 := (iff #2428 #3007)
#3005 := (iff #2425 #3002)
#2997 := (and #217 #2994)
#3003 := (iff #2997 #3002)
#3004 := [rewrite]: #3003
#2998 := (iff #2425 #2997)
#2995 := (iff #2422 #2994)
#2992 := (iff #2419 #2989)
#2984 := (and #1179 #2981)
#2990 := (iff #2984 #2989)
#2991 := [rewrite]: #2990
#2985 := (iff #2419 #2984)
#2982 := (iff #2416 #2981)
#2979 := (iff #2413 #2976)
#2970 := (and #2893 #2967)
#2977 := (iff #2970 #2976)
#2978 := [rewrite]: #2977
#2971 := (iff #2413 #2970)
#2968 := (iff #2410 #2967)
#2965 := (iff #2405 #2962)
#2956 := (and #2938 #2036 #2041 #2953)
#2963 := (iff #2956 #2962)
#2964 := [rewrite]: #2963
#2957 := (iff #2405 #2956)
#2954 := (iff #2396 #2953)
#2951 := (iff #2393 #2942)
#2943 := (not #2942)
#2946 := (not #2943)
#2949 := (iff #2946 #2942)
#2950 := [rewrite]: #2949
#2947 := (iff #2393 #2946)
#2944 := (iff #2390 #2943)
#2945 := [rewrite]: #2944
#2948 := [monotonicity #2945]: #2947
#2952 := [trans #2948 #2950]: #2951
#2955 := [quant-intro #2952]: #2954
#2939 := (iff #1212 #2938)
#2936 := (iff #1209 #2933)
#2919 := (or #220 #940)
#2930 := (or #2919 #1205)
#2934 := (iff #2930 #2933)
#2935 := [rewrite]: #2934
#2931 := (iff #1209 #2930)
#2928 := (iff #1202 #2919)
#2920 := (not #2919)
#2923 := (not #2920)
#2926 := (iff #2923 #2919)
#2927 := [rewrite]: #2926
#2924 := (iff #1202 #2923)
#2921 := (iff #1199 #2920)
#2922 := [rewrite]: #2921
#2925 := [monotonicity #2922]: #2924
#2929 := [trans #2925 #2927]: #2928
#2932 := [monotonicity #2929]: #2931
#2937 := [trans #2932 #2935]: #2936
#2940 := [quant-intro #2937]: #2939
#2958 := [monotonicity #2940 #2955]: #2957
#2966 := [trans #2958 #2964]: #2965
#2917 := (iff #2022 #2916)
#2914 := (iff #2021 #2911)
#2897 := (or #2896 #2011)
#2908 := (or #2897 #2020)
#2912 := (iff #2908 #2911)
#2913 := [rewrite]: #2912
#2909 := (iff #2021 #2908)
#2906 := (iff #2014 #2897)
#2898 := (not #2897)
#2901 := (not #2898)
#2904 := (iff #2901 #2897)
#2905 := [rewrite]: #2904
#2902 := (iff #2014 #2901)
#2899 := (iff #2013 #2898)
#2900 := [rewrite]: #2899
#2903 := [monotonicity #2900]: #2902
#2907 := [trans #2903 #2905]: #2906
#2910 := [monotonicity #2907]: #2909
#2915 := [trans #2910 #2913]: #2914
#2918 := [monotonicity #2915]: #2917
#2969 := [monotonicity #2918 #2966]: #2968
#2894 := (iff #1193 #2893)
#2891 := (iff #1190 #2888)
#2874 := (or #213 #2873)
#2885 := (or #2874 #1185)
#2889 := (iff #2885 #2888)
#2890 := [rewrite]: #2889
#2886 := (iff #1190 #2885)
#2883 := (iff #566 #2874)
#2875 := (not #2874)
#2878 := (not #2875)
#2881 := (iff #2878 #2874)
#2882 := [rewrite]: #2881
#2879 := (iff #566 #2878)
#2876 := (iff #223 #2875)
#2877 := [rewrite]: #2876
#2880 := [monotonicity #2877]: #2879
#2884 := [trans #2880 #2882]: #2883
#2887 := [monotonicity #2884]: #2886
#2892 := [trans #2887 #2890]: #2891
#2895 := [quant-intro #2892]: #2894
#2972 := [monotonicity #2895 #2969]: #2971
#2980 := [trans #2972 #2978]: #2979
#2871 := (iff #1990 #2870)
#2868 := (iff #1989 #2865)
#2851 := (or #1978 #2850)
#2862 := (or #2851 #1988)
#2866 := (iff #2862 #2865)
#2867 := [rewrite]: #2866
#2863 := (iff #1989 #2862)
#2860 := (iff #1983 #2851)
#2852 := (not #2851)
#2855 := (not #2852)
#2858 := (iff #2855 #2851)
#2859 := [rewrite]: #2858
#2856 := (iff #1983 #2855)
#2853 := (iff #1982 #2852)
#2854 := [rewrite]: #2853
#2857 := [monotonicity #2854]: #2856
#2861 := [trans #2857 #2859]: #2860
#2864 := [monotonicity #2861]: #2863
#2869 := [trans #2864 #2867]: #2868
#2872 := [monotonicity #2869]: #2871
#2983 := [monotonicity #2872 #2980]: #2982
#2986 := [monotonicity #2983]: #2985
#2993 := [trans #2986 #2991]: #2992
#2996 := [monotonicity #2993]: #2995
#2999 := [monotonicity #2996]: #2998
#3006 := [trans #2999 #3004]: #3005
#3009 := [monotonicity #3006]: #3008
#3012 := [monotonicity #3009]: #3011
#3019 := [trans #3012 #3017]: #3018
#3022 := [monotonicity #3019]: #3021
#3025 := [monotonicity #3022]: #3024
#3032 := [trans #3025 #3030]: #3031
#3035 := [monotonicity #3032]: #3034
#2848 := (iff #1159 #2847)
#2845 := (iff #1156 #2844)
#2824 := (iff #1153 #2823)
#2825 := [rewrite]: #2824
#2846 := [monotonicity #2825]: #2845
#2849 := [quant-intro #2846]: #2848
#2842 := (iff #1302 #2841)
#2839 := (iff #1299 #2836)
#2833 := (or #2822 #1294)
#2837 := (iff #2833 #2836)
#2838 := [rewrite]: #2837
#2834 := (iff #1299 #2833)
#2831 := (iff #1291 #2822)
#2826 := (not #2823)
#2829 := (iff #2826 #2822)
#2830 := [rewrite]: #2829
#2827 := (iff #1291 #2826)
#2828 := [monotonicity #2825]: #2827
#2832 := [trans #2828 #2830]: #2831
#2835 := [monotonicity #2832]: #2834
#2840 := [trans #2835 #2838]: #2839
#2843 := [quant-intro #2840]: #2842
#3038 := [monotonicity #2843 #2849 #3035]: #3037
#3047 := [trans #3038 #3045]: #3046
#2820 := (iff #2374 #2817)
#2811 := (and #2685 #144 #147 #149 #152 #2808)
#2818 := (iff #2811 #2817)
#2819 := [rewrite]: #2818
#2812 := (iff #2374 #2811)
#2809 := (iff #2371 #2808)
#2806 := (iff #2368 #2803)
#2797 := (and #2737 #2794)
#2804 := (iff #2797 #2803)
#2805 := [rewrite]: #2804
#2798 := (iff #2368 #2797)
#2795 := (iff #2365 #2794)
#2792 := (iff #1852 #2789)
#2784 := (and #2781 #1849)
#2790 := (iff #2784 #2789)
#2791 := [rewrite]: #2790
#2785 := (iff #1852 #2784)
#2782 := (iff #1096 #2781)
#2779 := (iff #1093 #2776)
#2762 := (or #1049 #940)
#2773 := (or #2762 #1090)
#2777 := (iff #2773 #2776)
#2778 := [rewrite]: #2777
#2774 := (iff #1093 #2773)
#2771 := (iff #1087 #2762)
#2763 := (not #2762)
#2766 := (not #2763)
#2769 := (iff #2766 #2762)
#2770 := [rewrite]: #2769
#2767 := (iff #1087 #2766)
#2764 := (iff #1084 #2763)
#2765 := [rewrite]: #2764
#2768 := [monotonicity #2765]: #2767
#2772 := [trans #2768 #2770]: #2771
#2775 := [monotonicity #2772]: #2774
#2780 := [trans #2775 #2778]: #2779
#2783 := [quant-intro #2780]: #2782
#2786 := [monotonicity #2783]: #2785
#2793 := [trans #2786 #2791]: #2792
#2760 := (iff #2362 #2759)
#2757 := (iff #2359 #2754)
#2740 := (or #1820 #1827)
#2751 := (or #2740 #2356)
#2755 := (iff #2751 #2754)
#2756 := [rewrite]: #2755
#2752 := (iff #2359 #2751)
#2749 := (iff #1830 #2740)
#2741 := (not #2740)
#2744 := (not #2741)
#2747 := (iff #2744 #2740)
#2748 := [rewrite]: #2747
#2745 := (iff #1830 #2744)
#2742 := (iff #1829 #2741)
#2743 := [rewrite]: #2742
#2746 := [monotonicity #2743]: #2745
#2750 := [trans #2746 #2748]: #2749
#2753 := [monotonicity #2750]: #2752
#2758 := [trans #2753 #2756]: #2757
#2761 := [monotonicity #2758]: #2760
#2796 := [monotonicity #2761 #2793]: #2795
#2738 := (iff #2349 #2737)
#2735 := (iff #2346 #2732)
#2713 := (or #66 #1049)
#2729 := (or #2713 #2726)
#2733 := (iff #2729 #2732)
#2734 := [rewrite]: #2733
#2730 := (iff #2346 #2729)
#2727 := (iff #2343 #2726)
#2728 := [rewrite]: #2727
#2722 := (iff #1056 #2713)
#2714 := (not #2713)
#2717 := (not #2714)
#2720 := (iff #2717 #2713)
#2721 := [rewrite]: #2720
#2718 := (iff #1056 #2717)
#2715 := (iff #1053 #2714)
#2716 := [rewrite]: #2715
#2719 := [monotonicity #2716]: #2718
#2723 := [trans #2719 #2721]: #2722
#2731 := [monotonicity #2723 #2728]: #2730
#2736 := [trans #2731 #2734]: #2735
#2739 := [quant-intro #2736]: #2738
#2799 := [monotonicity #2739 #2796]: #2798
#2807 := [trans #2799 #2805]: #2806
#2711 := (iff #2307 #2708)
#2703 := (and #1753 #1758 #2700)
#2709 := (iff #2703 #2708)
#2710 := [rewrite]: #2709
#2704 := (iff #2307 #2703)
#2701 := (iff #2301 #2700)
#2698 := (iff #2298 #2689)
#2690 := (not #2689)
#2693 := (not #2690)
#2696 := (iff #2693 #2689)
#2697 := [rewrite]: #2696
#2694 := (iff #2298 #2693)
#2691 := (iff #2295 #2690)
#2692 := [rewrite]: #2691
#2695 := [monotonicity #2692]: #2694
#2699 := [trans #2695 #2697]: #2698
#2702 := [quant-intro #2699]: #2701
#2705 := [monotonicity #2702]: #2704
#2712 := [trans #2705 #2710]: #2711
#2810 := [monotonicity #2712 #2807]: #2809
#2686 := (iff #1736 #2685)
#2683 := (iff #1733 #2674)
#2675 := (not #2674)
#2678 := (not #2675)
#2681 := (iff #2678 #2674)
#2682 := [rewrite]: #2681
#2679 := (iff #1733 #2678)
#2676 := (iff #1114 #2675)
#2677 := [rewrite]: #2676
#2680 := [monotonicity #2677]: #2679
#2684 := [trans #2680 #2682]: #2683
#2687 := [quant-intro #2684]: #2686
#2813 := [monotonicity #2687 #2810]: #2812
#2821 := [trans #2813 #2819]: #2820
#3050 := [monotonicity #2821 #3047]: #3049
#2672 := (iff #2275 #2671)
#2669 := (iff #2272 #2666)
#2646 := (or #66 #1004)
#2663 := (or #2646 #2660)
#2667 := (iff #2663 #2666)
#2668 := [rewrite]: #2667
#2664 := (iff #2272 #2663)
#2661 := (iff #2269 #2660)
#2662 := [rewrite]: #2661
#2655 := (iff #1011 #2646)
#2647 := (not #2646)
#2650 := (not #2647)
#2653 := (iff #2650 #2646)
#2654 := [rewrite]: #2653
#2651 := (iff #1011 #2650)
#2648 := (iff #1008 #2647)
#2649 := [rewrite]: #2648
#2652 := [monotonicity #2649]: #2651
#2656 := [trans #2652 #2654]: #2655
#2665 := [monotonicity #2656 #2662]: #2664
#2670 := [trans #2665 #2668]: #2669
#2673 := [quant-intro #2670]: #2672
#2644 := (iff #1377 #2643)
#2641 := (iff #1374 #2638)
#2624 := (or #118 #940)
#2635 := (or #2624 #1371)
#2639 := (iff #2635 #2638)
#2640 := [rewrite]: #2639
#2636 := (iff #1374 #2635)
#2633 := (iff #1368 #2624)
#2625 := (not #2624)
#2628 := (not #2625)
#2631 := (iff #2628 #2624)
#2632 := [rewrite]: #2631
#2629 := (iff #1368 #2628)
#2626 := (iff #1365 #2625)
#2627 := [rewrite]: #2626
#2630 := [monotonicity #2627]: #2629
#2634 := [trans #2630 #2632]: #2633
#2637 := [monotonicity #2634]: #2636
#2642 := [trans #2637 #2640]: #2641
#2645 := [quant-intro #2642]: #2644
#2622 := (iff #1388 #2621)
#2619 := (iff #1385 #2616)
#2602 := (or #117 #2601)
#2613 := (or #2602 #1020)
#2617 := (iff #2613 #2616)
#2618 := [rewrite]: #2617
#2614 := (iff #1385 #2613)
#2611 := (iff #377 #2602)
#2603 := (not #2602)
#2606 := (not #2603)
#2609 := (iff #2606 #2602)
#2610 := [rewrite]: #2609
#2607 := (iff #377 #2606)
#2604 := (iff #121 #2603)
#2605 := [rewrite]: #2604
#2608 := [monotonicity #2605]: #2607
#2612 := [trans #2608 #2610]: #2611
#2615 := [monotonicity #2612]: #2614
#2620 := [trans #2615 #2618]: #2619
#2623 := [quant-intro #2620]: #2622
#2599 := (iff #2233 #2598)
#2596 := (iff #2230 #2593)
#2573 := (or #66 #966)
#2590 := (or #2573 #2587)
#2594 := (iff #2590 #2593)
#2595 := [rewrite]: #2594
#2591 := (iff #2230 #2590)
#2588 := (iff #2227 #2587)
#2589 := [rewrite]: #2588
#2582 := (iff #973 #2573)
#2574 := (not #2573)
#2577 := (not #2574)
#2580 := (iff #2577 #2573)
#2581 := [rewrite]: #2580
#2578 := (iff #973 #2577)
#2575 := (iff #970 #2574)
#2576 := [rewrite]: #2575
#2579 := [monotonicity #2576]: #2578
#2583 := [trans #2579 #2581]: #2582
#2592 := [monotonicity #2583 #2589]: #2591
#2597 := [trans #2592 #2595]: #2596
#2600 := [quant-intro #2597]: #2599
#3053 := [monotonicity #2600 #2623 #2645 #2673 #3050]: #3052
#3064 := [trans #3053 #3062]: #3063
#2571 := (iff #2191 #2568)
#2563 := (and #1615 #1620 #2560)
#2569 := (iff #2563 #2568)
#2570 := [rewrite]: #2569
#2564 := (iff #2191 #2563)
#2561 := (iff #1643 #2560)
#2558 := (iff #1640 #2549)
#2550 := (not #2549)
#2553 := (not #2550)
#2556 := (iff #2553 #2549)
#2557 := [rewrite]: #2556
#2554 := (iff #1640 #2553)
#2551 := (iff #1631 #2550)
#2552 := [rewrite]: #2551
#2555 := [monotonicity #2552]: #2554
#2559 := [trans #2555 #2557]: #2558
#2562 := [quant-intro #2559]: #2561
#2565 := [monotonicity #2562]: #2564
#2572 := [trans #2565 #2570]: #2571
#3067 := [monotonicity #2572 #3064]: #3066
#2546 := (iff #958 #2545)
#2543 := (iff #955 #2540)
#2526 := (or #78 #940)
#2537 := (or #2526 #951)
#2541 := (iff #2537 #2540)
#2542 := [rewrite]: #2541
#2538 := (iff #955 #2537)
#2535 := (iff #947 #2526)
#2527 := (not #2526)
#2530 := (not #2527)
#2533 := (iff #2530 #2526)
#2534 := [rewrite]: #2533
#2531 := (iff #947 #2530)
#2528 := (iff #944 #2527)
#2529 := [rewrite]: #2528
#2532 := [monotonicity #2529]: #2531
#2536 := [trans #2532 #2534]: #2535
#2539 := [monotonicity #2536]: #2538
#2544 := [trans #2539 #2542]: #2543
#2547 := [quant-intro #2544]: #2546
#3070 := [monotonicity #2547 #3067]: #3069
#3078 := [trans #3070 #3076]: #3077
#2524 := (iff #2183 #2523)
#2521 := (iff #2180 #2518)
#2504 := (or #2503 #1590)
#2515 := (or #2504 #2177)
#2519 := (iff #2515 #2518)
#2520 := [rewrite]: #2519
#2516 := (iff #2180 #2515)
#2513 := (iff #1593 #2504)
#2505 := (not #2504)
#2508 := (not #2505)
#2511 := (iff #2508 #2504)
#2512 := [rewrite]: #2511
#2509 := (iff #1593 #2508)
#2506 := (iff #1592 #2505)
#2507 := [rewrite]: #2506
#2510 := [monotonicity #2507]: #2509
#2514 := [trans #2510 #2512]: #2513
#2517 := [monotonicity #2514]: #2516
#2522 := [trans #2517 #2520]: #2521
#2525 := [monotonicity #2522]: #2524
#3081 := [monotonicity #2525 #3078]: #3080
#2501 := (iff #932 #2500)
#2498 := (iff #929 #2495)
#1670 := (or #77 #1605)
#2492 := (or #1670 #925)
#2496 := (iff #2492 #2495)
#2497 := [rewrite]: #2496
#2493 := (iff #929 #2492)
#2490 := (iff #356 #1670)
#1671 := (not #1670)
#2485 := (not #1671)
#2488 := (iff #2485 #1670)
#2489 := [rewrite]: #2488
#2486 := (iff #356 #2485)
#2170 := (iff #86 #1671)
#2484 := [rewrite]: #2170
#2487 := [monotonicity #2484]: #2486
#2491 := [trans #2487 #2489]: #2490
#2494 := [monotonicity #2491]: #2493
#2499 := [trans #2494 #2497]: #2498
#2502 := [quant-intro #2499]: #2501
#3084 := [monotonicity #2502 #3081]: #3083
#3092 := [trans #3084 #3090]: #3091
#1947 := (iff #1569 #1946)
#1966 := (iff #1568 #1841)
#1885 := (or #1557 #1884)
#1545 := (or #1885 #1567)
#1926 := (iff #1545 #1841)
#1927 := [rewrite]: #1926
#1546 := (iff #1568 #1545)
#1572 := (iff #1562 #1885)
#1804 := (not #1885)
#2026 := (not #1804)
#1993 := (iff #2026 #1885)
#1994 := [rewrite]: #1993
#1722 := (iff #1562 #2026)
#1805 := (iff #1561 #1804)
#2025 := [rewrite]: #1805
#1723 := [monotonicity #2025]: #1722
#1573 := [trans #1723 #1994]: #1572
#1840 := [monotonicity #1573]: #1546
#1967 := [trans #1840 #1927]: #1966
#1604 := [monotonicity #1967]: #1947
#3095 := [monotonicity #1604 #3092]: #3094
#3098 := [monotonicity #3095]: #3097
#3105 := [trans #3098 #3103]: #3104
#3108 := [monotonicity #3105]: #3107
#3111 := [monotonicity #3108]: #3110
#3118 := [trans #3111 #3116]: #3117
#3121 := [monotonicity #3118]: #3120
#2049 := (+ #2048 #2044)
#2050 := (= #2049 0::Int)
#2051 := (and #2046 #213 #2050)
#2061 := (not #2051)
#2064 := (forall (vars (?v1 S2)) #2061)
#2042 := (and #2036 #2041)
#2043 := (not #2042)
#2058 := (not #2043)
#2068 := (and #2058 #2064)
#2073 := (and #1212 #2068)
#2077 := (or #2022 #2073)
#2081 := (and #1193 #2077)
#2085 := (or #1990 #2081)
#2089 := (and #1179 #2085)
#2093 := (or #1963 #2089)
#1957 := (not #661)
#2097 := (and #1957 #2093)
#2101 := (or #661 #2097)
#2105 := (and #563 #2101)
#2109 := (or #1943 #2105)
#2113 := (and #1170 #2109)
#2117 := (or #1923 #2113)
#1900 := (not #715)
#1881 := (and #1875 #1880)
#2121 := (and #1881 #184 #1323 #1315 #1900 #1302 #1159 #2117)
#1833 := (+ #1817 #1832)
#1834 := (+ #1824 #1833)
#1835 := (>= #1834 0::Int)
#1836 := (or #1830 #1835)
#1837 := (not #1836)
#1856 := (or #1837 #1852)
#1793 := (+ #1792 #1047)
#1799 := (+ #1798 #1793)
#1800 := (= #1799 0::Int)
#1794 := (>= #1793 0::Int)
#1795 := (not #1794)
#1801 := (and #1795 #1800)
#1806 := (or #1056 #1801)
#1809 := (forall (vars (?v0 S2)) #1806)
#1860 := (and #1809 #1856)
#1766 := (+ #1765 #1761)
#1767 := (= #1766 0::Int)
#1768 := (and #1763 #1767)
#1777 := (not #1768)
#1780 := (forall (vars (?v1 S2)) #1777)
#1759 := (and #1753 #1758)
#1760 := (not #1759)
#1774 := (not #1760)
#1784 := (and #1774 #1780)
#1864 := (or #1784 #1860)
#1748 := (not #494)
#1745 := (not #503)
#1742 := (not #512)
#1739 := (not #521)
#1868 := (and #1736 #1739 #1742 #1745 #1748 #1864)
#2125 := (or #1868 #2121)
#1709 := (+ #1708 #1002)
#1717 := (+ #1716 #1709)
#1718 := (= #1717 0::Int)
#1710 := (>= #1709 0::Int)
#1711 := (not #1710)
#1719 := (and #1711 #1713 #1718)
#1724 := (or #1011 #1719)
#1727 := (forall (vars (?v0 S2)) #1724)
#1681 := (not #804)
#1664 := (+ #964 #1663)
#1665 := (+ #1655 #1664)
#1666 := (= #1665 0::Int)
#1656 := (+ #1655 #964)
#1657 := (>= #1656 0::Int)
#1658 := (not #1657)
#1667 := (and #1658 #1660 #1666)
#1672 := (or #973 #1667)
#1675 := (forall (vars (?v0 S2)) #1672)
#2129 := (and #1675 #1681 #1397 #1388 #1377 #1727 #2125)
#1621 := (and #1615 #1620)
#1622 := (not #1621)
#1637 := (not #1622)
#1647 := (and #1637 #1643)
#2133 := (or #1647 #2129)
#2137 := (and #958 #2133)
#1597 := (+ #1596 #1587)
#1598 := (+ #1594 #1597)
#1599 := (>= #1598 0::Int)
#1600 := (or #1593 #1599)
#1601 := (not #1600)
#2141 := (or #1601 #2137)
#2145 := (and #932 #2141)
#2149 := (or #1569 #2145)
#2153 := (and #917 #2149)
#2157 := (or #1542 #2153)
#1504 := (not #868)
#2161 := (and #1504 #2157)
#2165 := (or #868 #2161)
#2482 := (iff #2165 #2481)
#2479 := (iff #2161 #2478)
#2476 := (iff #2157 #2475)
#2473 := (iff #2153 #2472)
#2470 := (iff #2149 #2469)
#2467 := (iff #2145 #2466)
#2464 := (iff #2141 #2463)
#2461 := (iff #2137 #2460)
#2458 := (iff #2133 #2457)
#2455 := (iff #2129 #2454)
#2452 := (iff #2125 #2451)
#2449 := (iff #2121 #2446)
#2443 := (and #1881 #184 #1323 #1315 #194 #1302 #1159 #2440)
#2447 := (iff #2443 #2446)
#2448 := [rewrite]: #2447
#2444 := (iff #2121 #2443)
#2441 := (iff #2117 #2440)
#2438 := (iff #2113 #2437)
#2435 := (iff #2109 #2434)
#2432 := (iff #2105 #2431)
#2429 := (iff #2101 #2428)
#2426 := (iff #2097 #2425)
#2423 := (iff #2093 #2422)
#2420 := (iff #2089 #2419)
#2417 := (iff #2085 #2416)
#2414 := (iff #2081 #2413)
#2411 := (iff #2077 #2410)
#2408 := (iff #2073 #2405)
#2399 := (and #2042 #2396)
#2402 := (and #1212 #2399)
#2406 := (iff #2402 #2405)
#2407 := [rewrite]: #2406
#2403 := (iff #2073 #2402)
#2400 := (iff #2068 #2399)
#2397 := (iff #2064 #2396)
#2394 := (iff #2061 #2393)
#2391 := (iff #2051 #2390)
#2388 := (iff #2050 #2387)
#2385 := (= #2049 #2384)
#2386 := [rewrite]: #2385
#2389 := [monotonicity #2386]: #2388
#2392 := [monotonicity #2389]: #2391
#2395 := [monotonicity #2392]: #2394
#2398 := [quant-intro #2395]: #2397
#2381 := (iff #2058 #2042)
#2382 := [rewrite]: #2381
#2401 := [monotonicity #2382 #2398]: #2400
#2404 := [monotonicity #2401]: #2403
#2409 := [trans #2404 #2407]: #2408
#2412 := [monotonicity #2409]: #2411
#2415 := [monotonicity #2412]: #2414
#2418 := [monotonicity #2415]: #2417
#2421 := [monotonicity #2418]: #2420
#2424 := [monotonicity #2421]: #2423
#2379 := (iff #1957 #217)
#2380 := [rewrite]: #2379
#2427 := [monotonicity #2380 #2424]: #2426
#2430 := [monotonicity #2427]: #2429
#2433 := [monotonicity #2430]: #2432
#2436 := [monotonicity #2433]: #2435
#2439 := [monotonicity #2436]: #2438
#2442 := [monotonicity #2439]: #2441
#2377 := (iff #1900 #194)
#2378 := [rewrite]: #2377
#2445 := [monotonicity #2378 #2442]: #2444
#2450 := [trans #2445 #2448]: #2449
#2375 := (iff #1868 #2374)
#2372 := (iff #1864 #2371)
#2369 := (iff #1860 #2368)
#2366 := (iff #1856 #2365)
#2363 := (iff #1837 #2362)
#2360 := (iff #1836 #2359)
#2357 := (iff #1835 #2356)
#2354 := (= #1834 #2353)
#2355 := [rewrite]: #2354
#2358 := [monotonicity #2355]: #2357
#2361 := [monotonicity #2358]: #2360
#2364 := [monotonicity #2361]: #2363
#2367 := [monotonicity #2364]: #2366
#2350 := (iff #1809 #2349)
#2347 := (iff #1806 #2346)
#2344 := (iff #1801 #2343)
#2341 := (iff #1800 #2338)
#2328 := (+ #1792 #1798)
#2329 := (+ #1047 #2328)
#2332 := (= #2329 0::Int)
#2339 := (iff #2332 #2338)
#2340 := [rewrite]: #2339
#2333 := (iff #1800 #2332)
#2330 := (= #1799 #2329)
#2331 := [rewrite]: #2330
#2334 := [monotonicity #2331]: #2333
#2342 := [trans #2334 #2340]: #2341
#2326 := (iff #1795 #2325)
#2323 := (iff #1794 #2320)
#2312 := (+ #1047 #1792)
#2315 := (>= #2312 0::Int)
#2321 := (iff #2315 #2320)
#2322 := [rewrite]: #2321
#2316 := (iff #1794 #2315)
#2313 := (= #1793 #2312)
#2314 := [rewrite]: #2313
#2317 := [monotonicity #2314]: #2316
#2324 := [trans #2317 #2322]: #2323
#2327 := [monotonicity #2324]: #2326
#2345 := [monotonicity #2327 #2342]: #2344
#2348 := [monotonicity #2345]: #2347
#2351 := [quant-intro #2348]: #2350
#2370 := [monotonicity #2351 #2367]: #2369
#2310 := (iff #1784 #2307)
#2304 := (and #1759 #2301)
#2308 := (iff #2304 #2307)
#2309 := [rewrite]: #2308
#2305 := (iff #1784 #2304)
#2302 := (iff #1780 #2301)
#2299 := (iff #1777 #2298)
#2296 := (iff #1768 #2295)
#2293 := (iff #1767 #2292)
#2290 := (= #1766 #2289)
#2291 := [rewrite]: #2290
#2294 := [monotonicity #2291]: #2293
#2297 := [monotonicity #2294]: #2296
#2300 := [monotonicity #2297]: #2299
#2303 := [quant-intro #2300]: #2302
#2286 := (iff #1774 #1759)
#2287 := [rewrite]: #2286
#2306 := [monotonicity #2287 #2303]: #2305
#2311 := [trans #2306 #2309]: #2310
#2373 := [monotonicity #2311 #2370]: #2372
#2284 := (iff #1748 #152)
#2285 := [rewrite]: #2284
#2282 := (iff #1745 #149)
#2283 := [rewrite]: #2282
#2280 := (iff #1742 #147)
#2281 := [rewrite]: #2280
#2278 := (iff #1739 #144)
#2279 := [rewrite]: #2278
#2376 := [monotonicity #2279 #2281 #2283 #2285 #2373]: #2375
#2453 := [monotonicity #2376 #2450]: #2452
#2276 := (iff #1727 #2275)
#2273 := (iff #1724 #2272)
#2270 := (iff #1719 #2269)
#2267 := (iff #1718 #2264)
#2254 := (+ #1708 #1716)
#2255 := (+ #1002 #2254)
#2258 := (= #2255 0::Int)
#2265 := (iff #2258 #2264)
#2266 := [rewrite]: #2265
#2259 := (iff #1718 #2258)
#2256 := (= #1717 #2255)
#2257 := [rewrite]: #2256
#2260 := [monotonicity #2257]: #2259
#2268 := [trans #2260 #2266]: #2267
#2252 := (iff #1711 #2251)
#2249 := (iff #1710 #2246)
#2238 := (+ #1002 #1708)
#2241 := (>= #2238 0::Int)
#2247 := (iff #2241 #2246)
#2248 := [rewrite]: #2247
#2242 := (iff #1710 #2241)
#2239 := (= #1709 #2238)
#2240 := [rewrite]: #2239
#2243 := [monotonicity #2240]: #2242
#2250 := [trans #2243 #2248]: #2249
#2253 := [monotonicity #2250]: #2252
#2271 := [monotonicity #2253 #2268]: #2270
#2274 := [monotonicity #2271]: #2273
#2277 := [quant-intro #2274]: #2276
#2236 := (iff #1681 #111)
#2237 := [rewrite]: #2236
#2234 := (iff #1675 #2233)
#2231 := (iff #1672 #2230)
#2228 := (iff #1667 #2227)
#2225 := (iff #1666 #2222)
#2212 := (+ #1655 #1663)
#2213 := (+ #964 #2212)
#2216 := (= #2213 0::Int)
#2223 := (iff #2216 #2222)
#2224 := [rewrite]: #2223
#2217 := (iff #1666 #2216)
#2214 := (= #1665 #2213)
#2215 := [rewrite]: #2214
#2218 := [monotonicity #2215]: #2217
#2226 := [trans #2218 #2224]: #2225
#2210 := (iff #1658 #2209)
#2207 := (iff #1657 #2204)
#2196 := (+ #964 #1655)
#2199 := (>= #2196 0::Int)
#2205 := (iff #2199 #2204)
#2206 := [rewrite]: #2205
#2200 := (iff #1657 #2199)
#2197 := (= #1656 #2196)
#2198 := [rewrite]: #2197
#2201 := [monotonicity #2198]: #2200
#2208 := [trans #2201 #2206]: #2207
#2211 := [monotonicity #2208]: #2210
#2229 := [monotonicity #2211 #2226]: #2228
#2232 := [monotonicity #2229]: #2231
#2235 := [quant-intro #2232]: #2234
#2456 := [monotonicity #2235 #2237 #2277 #2453]: #2455
#2194 := (iff #1647 #2191)
#2188 := (and #1621 #1643)
#2192 := (iff #2188 #2191)
#2193 := [rewrite]: #2192
#2189 := (iff #1647 #2188)
#2186 := (iff #1637 #1621)
#2187 := [rewrite]: #2186
#2190 := [monotonicity #2187]: #2189
#2195 := [trans #2190 #2193]: #2194
#2459 := [monotonicity #2195 #2456]: #2458
#2462 := [monotonicity #2459]: #2461
#2184 := (iff #1601 #2183)
#2181 := (iff #1600 #2180)
#2178 := (iff #1599 #2177)
#2175 := (= #1598 #2174)
#2176 := [rewrite]: #2175
#2179 := [monotonicity #2176]: #2178
#2182 := [monotonicity #2179]: #2181
#2185 := [monotonicity #2182]: #2184
#2465 := [monotonicity #2185 #2462]: #2464
#2468 := [monotonicity #2465]: #2467
#2471 := [monotonicity #2468]: #2470
#2474 := [monotonicity #2471]: #2473
#2477 := [monotonicity #2474]: #2476
#2171 := (iff #1504 #81)
#2172 := [rewrite]: #2171
#2480 := [monotonicity #2172 #2477]: #2479
#2483 := [monotonicity #2480]: #2482
#1479 := (not #1453)
#2166 := (~ #1479 #2165)
#2162 := (not #1450)
#2163 := (~ #2162 #2161)
#2158 := (not #1447)
#2159 := (~ #2158 #2157)
#2154 := (not #1444)
#2155 := (~ #2154 #2153)
#2150 := (not #1441)
#2151 := (~ #2150 #2149)
#2146 := (not #1438)
#2147 := (~ #2146 #2145)
#2142 := (not #1435)
#2143 := (~ #2142 #2141)
#2138 := (not #1432)
#2139 := (~ #2138 #2137)
#2134 := (not #1429)
#2135 := (~ #2134 #2133)
#2130 := (not #1424)
#2131 := (~ #2130 #2129)
#2126 := (not #1362)
#2127 := (~ #2126 #2125)
#2122 := (not #1357)
#2123 := (~ #2122 #2121)
#2118 := (not #1288)
#2119 := (~ #2118 #2117)
#2114 := (not #1285)
#2115 := (~ #2114 #2113)
#2110 := (not #1282)
#2111 := (~ #2110 #2109)
#2106 := (not #1279)
#2107 := (~ #2106 #2105)
#2102 := (not #1276)
#2103 := (~ #2102 #2101)
#2098 := (not #1273)
#2099 := (~ #2098 #2097)
#2094 := (not #1270)
#2095 := (~ #2094 #2093)
#2090 := (not #1267)
#2091 := (~ #2090 #2089)
#2086 := (not #1264)
#2087 := (~ #2086 #2085)
#2082 := (not #1261)
#2083 := (~ #2082 #2081)
#2078 := (not #1258)
#2079 := (~ #2078 #2077)
#2074 := (not #1255)
#2075 := (~ #2074 #2073)
#2055 := (not #1252)
#2071 := (~ #2055 #2068)
#2052 := (exists (vars (?v1 S2)) #2051)
#2053 := (or #2043 #2052)
#2054 := (not #2053)
#2069 := (~ #2054 #2068)
#2065 := (not #2052)
#2066 := (~ #2065 #2064)
#2062 := (~ #2061 #2061)
#2063 := [refl]: #2062
#2067 := [nnf-neg #2063]: #2066
#2059 := (~ #2058 #2058)
#2060 := [refl]: #2059
#2070 := [nnf-neg #2060 #2067]: #2069
#2056 := (~ #2055 #2054)
#2057 := [sk]: #2056
#2072 := [trans #2057 #2070]: #2071
#2031 := (not #1215)
#2032 := (~ #2031 #1212)
#2029 := (~ #1212 #1212)
#2027 := (~ #1209 #1209)
#2028 := [refl]: #2027
#2030 := [nnf-pos #2028]: #2029
#2033 := [nnf-neg #2030]: #2032
#2076 := [nnf-neg #2033 #2072]: #2075
#2023 := (~ #1215 #2022)
#2024 := [sk]: #2023
#2080 := [nnf-neg #2024 #2076]: #2079
#1999 := (not #1196)
#2000 := (~ #1999 #1193)
#1997 := (~ #1193 #1193)
#1995 := (~ #1190 #1190)
#1996 := [refl]: #1995
#1998 := [nnf-pos #1996]: #1997
#2001 := [nnf-neg #1998]: #2000
#2084 := [nnf-neg #2001 #2080]: #2083
#1991 := (~ #1196 #1990)
#1992 := [sk]: #1991
#2088 := [nnf-neg #1992 #2084]: #2087
#1972 := (not #1182)
#1973 := (~ #1972 #1179)
#1970 := (~ #1179 #1179)
#1968 := (~ #1176 #1176)
#1969 := [refl]: #1968
#1971 := [nnf-pos #1969]: #1970
#1974 := [nnf-neg #1971]: #1973
#2092 := [nnf-neg #1974 #2088]: #2091
#1964 := (~ #1182 #1963)
#1965 := [sk]: #1964
#2096 := [nnf-neg #1965 #2092]: #2095
#1958 := (~ #1957 #1957)
#1959 := [refl]: #1958
#2100 := [nnf-neg #1959 #2096]: #2099
#1955 := (~ #661 #661)
#1956 := [refl]: #1955
#2104 := [nnf-neg #1956 #2100]: #2103
#1952 := (not #673)
#1953 := (~ #1952 #563)
#1950 := (~ #563 #563)
#1948 := (~ #560 #560)
#1949 := [refl]: #1948
#1951 := [nnf-pos #1949]: #1950
#1954 := [nnf-neg #1951]: #1953
#2108 := [nnf-neg #1954 #2104]: #2107
#1944 := (~ #673 #1943)
#1945 := [sk]: #1944
#2112 := [nnf-neg #1945 #2108]: #2111
#1932 := (not #1173)
#1933 := (~ #1932 #1170)
#1930 := (~ #1170 #1170)
#1928 := (~ #1165 #1165)
#1929 := [refl]: #1928
#1931 := [nnf-pos #1929]: #1930
#1934 := [nnf-neg #1931]: #1933
#2116 := [nnf-neg #1934 #2112]: #2115
#1924 := (~ #1173 #1923)
#1925 := [sk]: #1924
#2120 := [nnf-neg #1925 #2116]: #2119
#1914 := (not #1162)
#1915 := (~ #1914 #1159)
#1912 := (~ #1159 #1159)
#1910 := (~ #1156 #1156)
#1911 := [refl]: #1910
#1913 := [nnf-pos #1911]: #1912
#1916 := [nnf-neg #1913]: #1915
#1907 := (not #1305)
#1908 := (~ #1907 #1302)
#1905 := (~ #1302 #1302)
#1903 := (~ #1299 #1299)
#1904 := [refl]: #1903
#1906 := [nnf-pos #1904]: #1905
#1909 := [nnf-neg #1906]: #1908
#1901 := (~ #1900 #1900)
#1902 := [refl]: #1901
#1897 := (not #1318)
#1898 := (~ #1897 #1315)
#1895 := (~ #1315 #1315)
#1893 := (~ #1312 #1312)
#1894 := [refl]: #1893
#1896 := [nnf-pos #1894]: #1895
#1899 := [nnf-neg #1896]: #1898
#1891 := (~ #1323 #1323)
#1892 := [refl]: #1891
#1889 := (~ #184 #184)
#1890 := [refl]: #1889
#1886 := (not #1333)
#1887 := (~ #1886 #1881)
#1882 := (~ #1117 #1881)
#1883 := [sk]: #1882
#1888 := [nnf-neg #1883]: #1887
#2124 := [nnf-neg #1888 #1890 #1892 #1899 #1902 #1909 #1916 #2120]: #2123
#1869 := (not #1135)
#1870 := (~ #1869 #1868)
#1865 := (not #1111)
#1866 := (~ #1865 #1864)
#1861 := (not #1108)
#1862 := (~ #1861 #1860)
#1857 := (not #1105)
#1858 := (~ #1857 #1856)
#1853 := (not #1102)
#1854 := (~ #1853 #1852)
#1850 := (~ #1849 #1849)
#1851 := [refl]: #1850
#1846 := (not #1099)
#1847 := (~ #1846 #1096)
#1844 := (~ #1096 #1096)
#1842 := (~ #1093 #1093)
#1843 := [refl]: #1842
#1845 := [nnf-pos #1843]: #1844
#1848 := [nnf-neg #1845]: #1847
#1855 := [nnf-neg #1848 #1851]: #1854
#1838 := (~ #1099 #1837)
#1839 := [sk]: #1838
#1859 := [nnf-neg #1839 #1855]: #1858
#1812 := (not #1081)
#1813 := (~ #1812 #1809)
#1810 := (~ #1078 #1809)
#1807 := (~ #1075 #1806)
#1802 := (~ #1072 #1801)
#1803 := [sk]: #1802
#1789 := (~ #1056 #1056)
#1790 := [refl]: #1789
#1808 := [monotonicity #1790 #1803]: #1807
#1811 := [nnf-pos #1808]: #1810
#1814 := [nnf-neg #1811]: #1813
#1863 := [nnf-neg #1814 #1859]: #1862
#1787 := (~ #1081 #1784)
#1769 := (exists (vars (?v1 S2)) #1768)
#1770 := (or #1760 #1769)
#1771 := (not #1770)
#1785 := (~ #1771 #1784)
#1781 := (not #1769)
#1782 := (~ #1781 #1780)
#1778 := (~ #1777 #1777)
#1779 := [refl]: #1778
#1783 := [nnf-neg #1779]: #1782
#1775 := (~ #1774 #1774)
#1776 := [refl]: #1775
#1786 := [nnf-neg #1776 #1783]: #1785
#1772 := (~ #1081 #1771)
#1773 := [sk]: #1772
#1788 := [trans #1773 #1786]: #1787
#1867 := [nnf-neg #1788 #1863]: #1866
#1749 := (~ #1748 #1748)
#1750 := [refl]: #1749
#1746 := (~ #1745 #1745)
#1747 := [refl]: #1746
#1743 := (~ #1742 #1742)
#1744 := [refl]: #1743
#1740 := (~ #1739 #1739)
#1741 := [refl]: #1740
#1737 := (~ #1333 #1736)
#1734 := (~ #1733 #1733)
#1735 := [refl]: #1734
#1738 := [nnf-neg #1735]: #1737
#1871 := [nnf-neg #1738 #1741 #1744 #1747 #1750 #1867]: #1870
#2128 := [nnf-neg #1871 #2124]: #2127
#1730 := (not #1044)
#1731 := (~ #1730 #1727)
#1728 := (~ #1041 #1727)
#1725 := (~ #1038 #1724)
#1720 := (~ #1035 #1719)
#1721 := [sk]: #1720
#1705 := (~ #1011 #1011)
#1706 := [refl]: #1705
#1726 := [monotonicity #1706 #1721]: #1725
#1729 := [nnf-pos #1726]: #1728
#1732 := [nnf-neg #1729]: #1731
#1702 := (not #1380)
#1703 := (~ #1702 #1377)
#1700 := (~ #1377 #1377)
#1698 := (~ #1374 #1374)
#1699 := [refl]: #1698
#1701 := [nnf-pos #1699]: #1700
#1704 := [nnf-neg #1701]: #1703
#1695 := (not #1391)
#1696 := (~ #1695 #1388)
#1693 := (~ #1388 #1388)
#1691 := (~ #1385 #1385)
#1692 := [refl]: #1691
#1694 := [nnf-pos #1692]: #1693
#1697 := [nnf-neg #1694]: #1696
#1688 := (not #1400)
#1689 := (~ #1688 #1397)
#1686 := (~ #1397 #1397)
#1684 := (~ #1394 #1394)
#1685 := [refl]: #1684
#1687 := [nnf-pos #1685]: #1686
#1690 := [nnf-neg #1687]: #1689
#1682 := (~ #1681 #1681)
#1683 := [refl]: #1682
#1678 := (not #1403)
#1679 := (~ #1678 #1675)
#1676 := (~ #999 #1675)
#1673 := (~ #996 #1672)
#1668 := (~ #993 #1667)
#1669 := [sk]: #1668
#1652 := (~ #973 #973)
#1653 := [refl]: #1652
#1674 := [monotonicity #1653 #1669]: #1673
#1677 := [nnf-pos #1674]: #1676
#1680 := [nnf-neg #1677]: #1679
#2132 := [nnf-neg #1680 #1683 #1690 #1697 #1704 #1732 #2128]: #2131
#1650 := (~ #1403 #1647)
#1632 := (exists (vars (?v1 S2)) #1631)
#1633 := (or #1622 #1632)
#1634 := (not #1633)
#1648 := (~ #1634 #1647)
#1644 := (not #1632)
#1645 := (~ #1644 #1643)
#1641 := (~ #1640 #1640)
#1642 := [refl]: #1641
#1646 := [nnf-neg #1642]: #1645
#1638 := (~ #1637 #1637)
#1639 := [refl]: #1638
#1649 := [nnf-neg #1639 #1646]: #1648
#1635 := (~ #1403 #1634)
#1636 := [sk]: #1635
#1651 := [trans #1636 #1649]: #1650
#2136 := [nnf-neg #1651 #2132]: #2135
#1610 := (not #961)
#1611 := (~ #1610 #958)
#1608 := (~ #958 #958)
#1606 := (~ #955 #955)
#1607 := [refl]: #1606
#1609 := [nnf-pos #1607]: #1608
#1612 := [nnf-neg #1609]: #1611
#2140 := [nnf-neg #1612 #2136]: #2139
#1602 := (~ #961 #1601)
#1603 := [sk]: #1602
#2144 := [nnf-neg #1603 #2140]: #2143
#1578 := (not #935)
#1579 := (~ #1578 #932)
#1576 := (~ #932 #932)
#1574 := (~ #929 #929)
#1575 := [refl]: #1574
#1577 := [nnf-pos #1575]: #1576
#1580 := [nnf-neg #1577]: #1579
#2148 := [nnf-neg #1580 #2144]: #2147
#1570 := (~ #935 #1569)
#1571 := [sk]: #1570
#2152 := [nnf-neg #1571 #2148]: #2151
#1551 := (not #920)
#1552 := (~ #1551 #917)
#1549 := (~ #917 #917)
#1547 := (~ #916 #916)
#1548 := [refl]: #1547
#1550 := [nnf-pos #1548]: #1549
#1553 := [nnf-neg #1550]: #1552
#2156 := [nnf-neg #1553 #2152]: #2155
#1543 := (~ #920 #1542)
#1544 := [sk]: #1543
#2160 := [nnf-neg #1544 #2156]: #2159
#1505 := (~ #1504 #1504)
#1538 := [refl]: #1505
#2164 := [nnf-neg #1538 #2160]: #2163
#1536 := (~ #868 #868)
#1537 := [refl]: #1536
#2167 := [nnf-neg #1537 #2164]: #2166
#1480 := [not-or-elim #1475]: #1479
#2168 := [mp~ #1480 #2167]: #2165
#2169 := [mp #2168 #2483]: #2481
#3122 := [mp #2169 #3121]: #3119
#4037 := [mp #3122 #4036]: #4034
#7144 := [unit-resolution #4037 #4122]: #4031
#3361 := (or #4028 #4022)
#3351 := [def-axiom]: #3361
#7145 := [unit-resolution #3351 #7144]: #4022
#3357 := (or #4025 #1542 #4019)
#3359 := [def-axiom]: #3357
#7146 := [unit-resolution #3359 #7145 #4053]: #4019
#3355 := (or #4016 #4010)
#3358 := [def-axiom]: #3355
#7147 := [unit-resolution #3358 #7146]: #4010
#4245 := [hypothesis]: #1560
#3661 := (forall (vars (?v0 S2)) (:pat #3660) #78)
#3664 := (iff #79 #3661)
#3662 := (iff #78 #78)
#3663 := [refl]: #3662
#3665 := [quant-intro #3663]: #3664
#1502 := (~ #79 #79)
#1533 := (~ #78 #78)
#1534 := [refl]: #1533
#1503 := [nnf-pos #1534]: #1502
#1478 := [not-or-elim #1475]: #79
#1535 := [mp~ #1478 #1503]: #79
#3666 := [mp #1535 #3665]: #3661
#6940 := (not #3661)
#4154 := (or #6940 #1884)
#4155 := [quant-inst #1555]: #4154
#4251 := [unit-resolution #4155 #3666 #4245]: false
#4288 := [lemma #4251]: #1884
#3186 := (or #1841 #1560)
#3272 := [def-axiom]: #3186
#7148 := [unit-resolution #3272 #4288]: #1841
#3217 := (or #4013 #1946 #4007)
#3375 := [def-axiom]: #3217
#7149 := [unit-resolution #3375 #7148 #7147]: #4007
#3397 := (or #4004 #3998)
#3367 := [def-axiom]: #3397
#7150 := [unit-resolution #3367 #7149]: #3998
#6160 := [hypothesis]: #1584
#6331 := (or #6940 #2503)
#6332 := [quant-inst #1581]: #6331
#6161 := [unit-resolution #6332 #3666 #6160]: false
#6581 := [lemma #6161]: #2503
#3277 := (or #2518 #1584)
#3274 := [def-axiom]: #3277
#7151 := [unit-resolution #3274 #6581]: #2518
#3394 := (or #4001 #2523 #3995)
#3395 := [def-axiom]: #3394
#7152 := [unit-resolution #3395 #7151 #7150]: #3995
#3378 := (or #3992 #3986)
#3385 := [def-axiom]: #3378
#7153 := [unit-resolution #3385 #7152]: #3986
#3415 := (or #3989 #3705 #3983)
#3400 := [def-axiom]: #3415
#7154 := [unit-resolution #3400 #7153]: #3986
#7155 := [unit-resolution #7154 #6633]: #3983
#3407 := (or #3980 #3974)
#3408 := [def-axiom]: #3407
#7801 := [unit-resolution #3408 #7155]: #3974
#6893 := [hypothesis]: #3817
#3559 := (or #3814 #149)
#3554 := [def-axiom]: #3559
#6888 := [unit-resolution #3554 #6893]: #149
#3555 := (or #3814 #3751)
#3556 := [def-axiom]: #3555
#6808 := [unit-resolution #3556 #6893]: #3751
#3431 := (or #3980 #111)
#3432 := [def-axiom]: #3431
#6894 := [unit-resolution #3432 #7155]: #111
#4278 := (or #503 #169 #804)
#4273 := [hypothesis]: #111
#4275 := (= #168 #110)
#4274 := [hypothesis]: #149
#4276 := [monotonicity #4274]: #4275
#4271 := [trans #4276 #4273]: #169
#4158 := [hypothesis]: #1849
#4277 := [unit-resolution #4158 #4271]: false
#4279 := [lemma #4277]: #4278
#6895 := [unit-resolution #4279 #6888 #6894]: #169
#3298 := (or #3790 #1849)
#3299 := [def-axiom]: #3298
#6896 := [unit-resolution #3299 #6895]: #3790
#3402 := (or #3814 #3808)
#3403 := [def-axiom]: #3402
#6861 := [unit-resolution #3403 #6893]: #3808
#7454 := (or #3768 #503)
#6806 := (?v1!7 ?v0!8)
#7010 := (f19 f25 #6806)
#7056 := (* -1::Int #7010)
#6807 := (f19 f20 #6806)
#7278 := (+ #6807 #7056)
#7328 := (>= #7278 0::Int)
#7277 := (= #6807 #7010)
#7409 := (= #7010 #6807)
#7410 := [monotonicity #4274]: #7409
#7411 := [symm #7410]: #7277
#7412 := (not #7277)
#7413 := (or #7412 #7328)
#7414 := [th-lemma arith triangle-eq]: #7413
#7415 := [unit-resolution #7414 #7411]: #7328
#6897 := (* -1::Int #6807)
#6741 := (f19 f20 ?v0!8)
#6898 := (+ #6741 #6897)
#6903 := (<= #6898 0::Int)
#6821 := (not #6903)
#6850 := (f6 f7 #6806)
#6853 := (f5 #6850 ?v0!8)
#6889 := (f4 #6853)
#6890 := (* -1::Int #6889)
#6908 := (+ #6897 #6890)
#6925 := (+ #6741 #6908)
#5298 := (= #6925 0::Int)
#6077 := (not #5298)
#6904 := (f11 f21 #6806)
#6851 := (= #6904 f1)
#6852 := (not #6851)
#6078 := (or #6903 #6852 #6077)
#6102 := (not #6078)
#6742 := (* -1::Int #6741)
#6772 := (+ f3 #6742)
#6773 := (<= #6772 0::Int)
#7378 := (not #6773)
#7416 := [hypothesis]: #3771
#3249 := (or #3768 #1758)
#3591 := [def-axiom]: #3249
#7417 := [unit-resolution #3591 #7416]: #1758
#7026 := (+ #1754 #6742)
#7012 := (>= #7026 0::Int)
#7025 := (= #1754 #6741)
#7418 := (= #6741 #1754)
#6982 := (= f20 f25)
#6983 := [symm #4274]: #6982
#7419 := [monotonicity #6983]: #7418
#7420 := [symm #7419]: #7025
#7421 := (not #7025)
#7422 := (or #7421 #7012)
#7423 := [th-lemma arith triangle-eq]: #7422
#7424 := [unit-resolution #7423 #7420]: #7012
#7379 := (not #7012)
#7380 := (or #7378 #7379 #1757)
#7368 := [hypothesis]: #1758
#7369 := [hypothesis]: #6773
#7376 := [hypothesis]: #7012
#7377 := [th-lemma arith farkas 1 -1 1 #7376 #7369 #7368]: false
#7381 := [lemma #7377]: #7380
#7425 := [unit-resolution #7381 #7424 #7417]: #7378
#7428 := (or #6773 #6102)
#3589 := (or #3768 #1753)
#3254 := [def-axiom]: #3589
#7426 := [unit-resolution #3254 #7416]: #1753
#3405 := (or #3980 #3742)
#3406 := [def-axiom]: #3405
#7427 := [unit-resolution #3406 #7155]: #3742
#6227 := (or #3747 #1752 #6773 #6102)
#6103 := (or #1752 #6773 #6102)
#6189 := (or #3747 #6103)
#6704 := (iff #6189 #6227)
#6805 := [rewrite]: #6704
#6190 := [quant-inst #1751]: #6189
#6797 := [mp #6190 #6805]: #6227
#7429 := [unit-resolution #6797 #7427 #7426]: #7428
#7430 := [unit-resolution #7429 #7425]: #6102
#6854 := (or #6078 #6821)
#6860 := [def-axiom]: #6854
#7431 := [unit-resolution #6860 #7430]: #6821
#7057 := (+ #1754 #7056)
#7058 := (<= #7057 0::Int)
#7101 := (+ #6890 #7056)
#7102 := (+ #1754 #7101)
#7105 := (= #7102 0::Int)
#7195 := (<= #7102 0::Int)
#7327 := (<= #7278 0::Int)
#7432 := (or #7412 #7327)
#7433 := [th-lemma arith triangle-eq]: #7432
#7434 := [unit-resolution #7433 #7411]: #7327
#6815 := (<= #6925 0::Int)
#6862 := (or #6078 #5298)
#6863 := [def-axiom]: #6862
#7435 := [unit-resolution #6863 #7430]: #5298
#7436 := (or #6077 #6815)
#7437 := [th-lemma arith triangle-eq]: #7436
#7438 := [unit-resolution #7437 #7435]: #6815
#7011 := (<= #7026 0::Int)
#7439 := (or #7421 #7011)
#7440 := [th-lemma arith triangle-eq]: #7439
#7441 := [unit-resolution #7440 #7420]: #7011
#7390 := (not #7327)
#7389 := (not #6815)
#7388 := (not #7011)
#7391 := (or #7195 #7388 #7389 #7390)
#7375 := [hypothesis]: #7327
#7128 := [hypothesis]: #6815
#7384 := [hypothesis]: #7011
#7385 := (not #7195)
#7386 := [hypothesis]: #7385
#7387 := [th-lemma arith farkas -1 1 1 1 #7386 #7384 #7128 #7375]: false
#7392 := [lemma #7387]: #7391
#7442 := [unit-resolution #7392 #7441 #7438 #7434]: #7195
#7196 := (>= #7102 0::Int)
#6820 := (>= #6925 0::Int)
#7443 := (or #6077 #6820)
#7444 := [th-lemma arith triangle-eq]: #7443
#7445 := [unit-resolution #7444 #7435]: #6820
#7406 := (not #7328)
#7405 := (not #6820)
#7407 := (or #7196 #7379 #7405 #7406)
#7400 := [hypothesis]: #7328
#7401 := [hypothesis]: #6820
#7402 := (not #7196)
#7403 := [hypothesis]: #7402
#7404 := [th-lemma arith farkas -1 1 1 1 #7403 #7376 #7401 #7400]: false
#7408 := [lemma #7404]: #7407
#7446 := [unit-resolution #7408 #7424 #7445 #7415]: #7196
#7447 := (or #7105 #7385 #7402)
#7448 := [th-lemma arith triangle-eq]: #7447
#7449 := [unit-resolution #7448 #7446 #7442]: #7105
#7114 := (not #7105)
#7122 := (or #7058 #7114)
#3234 := (or #3768 #3760)
#3575 := [def-axiom]: #3234
#7450 := [unit-resolution #3575 #7416]: #3760
#7125 := (or #3765 #7058 #7114)
#7015 := (+ #1755 #6889)
#7028 := (+ #7010 #7015)
#7029 := (= #7028 0::Int)
#7049 := (not #7029)
#7013 := (+ #7010 #1755)
#7014 := (>= #7013 0::Int)
#7050 := (or #7014 #7049)
#7126 := (or #3765 #7050)
#7119 := (iff #7126 #7125)
#6981 := (or #3765 #7122)
#7017 := (iff #6981 #7125)
#7118 := [rewrite]: #7017
#7016 := (iff #7126 #6981)
#7123 := (iff #7050 #7122)
#7115 := (iff #7049 #7114)
#7113 := (iff #7029 #7105)
#7091 := (+ #6889 #7010)
#7086 := (+ #1755 #7091)
#7094 := (= #7086 0::Int)
#7106 := (iff #7094 #7105)
#7112 := [rewrite]: #7106
#7095 := (iff #7029 #7094)
#7092 := (= #7028 #7086)
#7093 := [rewrite]: #7092
#7096 := [monotonicity #7093]: #7095
#7111 := [trans #7096 #7112]: #7113
#7116 := [monotonicity #7111]: #7115
#7089 := (iff #7014 #7058)
#7051 := (+ #1755 #7010)
#7048 := (>= #7051 0::Int)
#7087 := (iff #7048 #7058)
#7088 := [rewrite]: #7087
#7054 := (iff #7014 #7048)
#7052 := (= #7013 #7051)
#7053 := [rewrite]: #7052
#7055 := [monotonicity #7053]: #7054
#7090 := [trans #7055 #7088]: #7089
#7121 := [monotonicity #7090 #7116]: #7123
#7124 := [monotonicity #7121]: #7016
#7120 := [trans #7124 #7118]: #7119
#6980 := [quant-inst #6806]: #7126
#7127 := [mp #6980 #7120]: #7125
#7451 := [unit-resolution #7127 #7450]: #7122
#7452 := [unit-resolution #7451 #7449]: #7058
#7453 := [th-lemma arith farkas 1 -1 1 1 #7424 #7452 #7431 #7415]: false
#7455 := [lemma #7453]: #7454
#6859 := [unit-resolution #7455 #6888]: #3768
#3562 := (or #3811 #3771 #3805)
#3566 := [def-axiom]: #3562
#6864 := [unit-resolution #3566 #6859 #6861]: #3805
#3283 := (or #3802 #3796)
#3284 := [def-axiom]: #3283
#6869 := [unit-resolution #3284 #6864]: #3796
#3571 := (or #3799 #2759 #3793)
#3568 := [def-axiom]: #3571
#6935 := [unit-resolution #3568 #6869 #6896]: #2759
#3225 := (or #2754 #1828)
#3226 := [def-axiom]: #3225
#6870 := [unit-resolution #3226 #6935]: #1828
#6589 := (f19 f20 ?v1!10)
#6584 := (* -1::Int #6589)
#6868 := (+ #1817 #6584)
#6946 := (>= #6868 0::Int)
#4646 := (or #6946 #503)
#6329 := (= #1817 #6589)
#6605 := (= #6589 #1817)
#6606 := [monotonicity #6983]: #6605
#6585 := [symm #6606]: #6329
#7134 := (not #6946)
#6586 := [hypothesis]: #7134
#6330 := (not #6329)
#6322 := (or #6330 #6946)
#6328 := [th-lemma arith triangle-eq]: #6322
#6580 := [unit-resolution #6328 #6586 #6585]: false
#4567 := [lemma #6580]: #4646
#6867 := [unit-resolution #4567 #6888]: #6946
#3583 := (or #2754 #1821)
#3585 := [def-axiom]: #3583
#6945 := [unit-resolution #3585 #6935]: #1821
#3586 := (not #2356)
#3584 := (or #2754 #3586)
#3587 := [def-axiom]: #3584
#6866 := [unit-resolution #3587 #6935]: #3586
#7019 := (or #7134 #3756 #1827 #2356 #1820 #503)
#6765 := (f19 f20 ?v0!11)
#6766 := (* -1::Int #6765)
#6948 := (+ #1831 #6766)
#6949 := (<= #6948 0::Int)
#6947 := (= #1831 #6765)
#6984 := (= #6765 #1831)
#6985 := [monotonicity #6983]: #6984
#6986 := [symm #6985]: #6947
#6987 := (not #6947)
#6988 := (or #6987 #6949)
#6975 := [th-lemma arith triangle-eq]: #6988
#6976 := [unit-resolution #6975 #6986]: #6949
#7130 := [hypothesis]: #3586
#7143 := [hypothesis]: #1828
#7140 := [hypothesis]: #3751
#7131 := [hypothesis]: #6946
#6572 := (+ f3 #6584)
#6576 := (<= #6572 0::Int)
#7138 := (not #6576)
#6974 := [hypothesis]: #1821
#6977 := (or #7138 #1820 #7134)
#6978 := [th-lemma arith assign-bounds -1 -1]: #6977
#6979 := [unit-resolution #6978 #7131 #6974]: #7138
#7133 := (not #6949)
#7160 := (or #6576 #1827 #3756 #7134 #2356 #7133)
#6907 := (+ #6589 #6766)
#6926 := (+ #1824 #6907)
#6924 := (>= #6926 0::Int)
#7132 := (not #6924)
#7129 := [hypothesis]: #6949
#7135 := (or #7132 #7133 #2356 #7134)
#7136 := [th-lemma arith assign-bounds -1 -1 1]: #7135
#7137 := [unit-resolution #7136 #7131 #7130 #7129]: #7132
#6587 := (f11 f21 ?v1!10)
#6588 := (= #6587 f1)
#7139 := [hypothesis]: #7138
#5703 := (or #6588 #6576)
#6635 := (or #3756 #6588 #6576)
#6636 := (or #3756 #5703)
#6638 := (iff #6636 #6635)
#6211 := [rewrite]: #6638
#6637 := [quant-inst #1815]: #6636
#6252 := [mp #6637 #6211]: #6635
#7141 := [unit-resolution #6252 #7140]: #5703
#7142 := [unit-resolution #7141 #7139]: #6588
#6849 := (not #6588)
#7157 := (or #6849 #6924)
#3399 := (or #3980 #3734)
#3404 := [def-axiom]: #3399
#7156 := [unit-resolution #3404 #7155]: #3734
#6930 := (or #3739 #6849 #1827 #6924)
#6927 := (or #6849 #1827 #6924)
#6931 := (or #3739 #6927)
#3348 := (iff #6931 #6930)
#3221 := [rewrite]: #3348
#6932 := [quant-inst #1816 #1815]: #6931
#4127 := [mp #6932 #3221]: #6930
#7158 := [unit-resolution #4127 #7156 #7143]: #7157
#7159 := [unit-resolution #7158 #7142 #7137]: false
#7161 := [lemma #7159]: #7160
#7018 := [unit-resolution #7161 #6979 #7131 #7140 #7143 #7130 #6976]: false
#7020 := [lemma #7018]: #7019
#6950 := [unit-resolution #7020 #6866 #6945 #6867 #6870 #6808 #6888]: false
#7021 := [lemma #6950]: #3814
#3419 := (or #3977 #3817 #3971)
#3421 := [def-axiom]: #3419
#7802 := [unit-resolution #3421 #7021 #7801]: #3971
#3459 := (or #3968 #194)
#3464 := [def-axiom]: #3459
#8144 := [unit-resolution #3464 #7802]: #194
#8146 := [symm #8144]: #8145
#16380 := [monotonicity #8146]: #16289
#16388 := [monotonicity #16380]: #16359
#16389 := [symm #16388]: #16382
#16391 := [monotonicity #16389]: #16390
#19086 := [hypothesis]: #4534
#5090 := (or #4541 #5087)
#8395 := [hypothesis]: #1943
#3547 := (or #1942 #1937)
#3543 := [def-axiom]: #3547
#8389 := [unit-resolution #3543 #8395]: #1937
#3548 := (not #1941)
#3542 := (or #1942 #3548)
#3549 := [def-axiom]: #3542
#8396 := [unit-resolution #3549 #8395]: #3548
#5879 := (* -1::Int #1940)
#5980 := (+ #185 #5879)
#7760 := (>= #5980 0::Int)
#4329 := (f11 f21 ?v0!14)
#4316 := (= #4329 f1)
#4315 := (= ?v0!14 f28)
#4345 := (or #4315 #4316)
#4328 := (f11 #193 ?v0!14)
#4330 := (= #4328 f1)
#4348 := (iff #4330 #4345)
#8073 := (or #7518 #4348)
#4314 := (if #4315 #4057 #4316)
#4317 := (iff #4330 #4314)
#8074 := (or #7518 #4317)
#8078 := (iff #8074 #8073)
#8080 := (iff #8073 #8073)
#8081 := [rewrite]: #8080
#4337 := (iff #4317 #4348)
#4344 := (iff #4314 #4345)
#4318 := (if #4315 true #4316)
#4346 := (iff #4318 #4345)
#4338 := [rewrite]: #4346
#4319 := (iff #4314 #4318)
#4332 := [monotonicity #4060]: #4319
#4347 := [trans #4332 #4338]: #4344
#4349 := [monotonicity #4347]: #4337
#8079 := [monotonicity #4349]: #8078
#8082 := [trans #8079 #8081]: #8078
#8077 := [quant-inst #115 #181 #3 #1935]: #8074
#8083 := [mp #8077 #8082]: #8073
#8113 := [unit-resolution #8083 #3646]: #4348
#8114 := [hypothesis]: #1937
#8147 := (= #4328 #1936)
#8148 := [monotonicity #8146]: #8147
#8149 := [trans #8148 #8114]: #4330
#8094 := (not #4330)
#8091 := (not #4348)
#8095 := (or #8091 #8094 #4345)
#8096 := [def-axiom]: #8095
#8150 := [unit-resolution #8096 #8149 #8113]: #4345
#8088 := (not #4345)
#8152 := (or #8088 #4316)
#7690 := (not #4315)
#7795 := [hypothesis]: #3548
#7815 := (or #7690 #1941)
#7809 := (= #185 #1940)
#7807 := (= #1940 #185)
#7796 := [hypothesis]: #4315
#7808 := [monotonicity #7796]: #7807
#7810 := [symm #7808]: #7809
#7811 := (= #1939 #185)
#4131 := (= #4078 #185)
#4082 := (f5 #195 f28)
#4083 := (f4 #4082)
#4101 := (>= #4083 0::Int)
#4086 := (* -1::Int #4083)
#4087 := (+ f3 #4086)
#4088 := (<= #4087 0::Int)
#4133 := (or #4088 #4101)
#6365 := (= #4083 0::Int)
#6474 := (not #6365)
#6475 := [hypothesis]: #6474
#14 := (f6 f7 #10)
#15 := (f5 #14 #11)
#3600 := (pattern #15)
#16 := (f4 #15)
#17 := (= #16 0::Int)
#12 := (= #10 #11)
#20 := (not #12)
#306 := (or #20 #17)
#3601 := (forall (vars (?v0 S2) (?v1 S2)) (:pat #3600) #306)
#314 := (forall (vars (?v0 S2) (?v1 S2)) #306)
#3604 := (iff #314 #3601)
#3602 := (iff #306 #306)
#3603 := [refl]: #3602
#3605 := [quant-intro #3603]: #3604
#1510 := (~ #314 #314)
#1508 := (~ #306 #306)
#1509 := [refl]: #1508
#1511 := [nnf-pos #1509]: #1510
#18 := (implies #12 #17)
#19 := (forall (vars (?v0 S2) (?v1 S2)) #18)
#315 := (iff #19 #314)
#312 := (iff #18 #306)
#313 := [rewrite]: #312
#316 := [quant-intro #313]: #315
#305 := [asserted]: #19
#319 := [mp #305 #316]: #314
#1484 := [mp~ #319 #1511]: #314
#3606 := [mp #1484 #3605]: #3601
#6226 := (not #3601)
#6401 := (or #6226 #6365)
#4403 := (= f28 f28)
#6358 := (not #4403)
#6369 := (or #6358 #6365)
#6400 := (or #6226 #6369)
#6403 := (iff #6400 #6401)
#6471 := (iff #6401 #6401)
#6466 := [rewrite]: #6471
#6387 := (iff #6369 #6365)
#6377 := (or false #6365)
#6382 := (iff #6377 #6365)
#6386 := [rewrite]: #6382
#6383 := (iff #6369 #6377)
#6378 := (iff #6358 false)
#6370 := (iff #6358 #6910)
#4406 := (iff #4403 true)
#4407 := [rewrite]: #4406
#6375 := [monotonicity #4407]: #6370
#6379 := [trans #6375 #6914]: #6378
#6384 := [monotonicity #6379]: #6383
#6398 := [trans #6384 #6386]: #6387
#6439 := [monotonicity #6398]: #6403
#6470 := [trans #6439 #6466]: #6403
#6402 := [quant-inst #181 #181]: #6400
#6472 := [mp #6402 #6470]: #6401
#6476 := [unit-resolution #6472 #3606 #6475]: false
#6482 := [lemma #6476]: #6365
#7797 := (or #6474 #4101)
#7798 := [th-lemma arith triangle-eq]: #7797
#7799 := [unit-resolution #7798 #6482]: #4101
#7285 := (not #4101)
#7283 := (or #4133 #7285)
#7286 := [def-axiom]: #7283
#7800 := [unit-resolution #7286 #7799]: #4133
#3445 := (or #3968 #3838)
#3426 := [def-axiom]: #3445
#7803 := [unit-resolution #3426 #7802]: #3838
#4136 := (not #4133)
#7259 := (or #3843 #4136 #4131)
#4089 := (+ #1146 #4086)
#4090 := (+ #185 #4089)
#4091 := (<= #4090 0::Int)
#4129 := (or #4088 #4091)
#4130 := (not #4129)
#4132 := (or #4130 #4131)
#7260 := (or #3843 #4132)
#7266 := (iff #7260 #7259)
#4139 := (or #4136 #4131)
#7262 := (or #3843 #4139)
#7265 := (iff #7262 #7259)
#7261 := [rewrite]: #7265
#7263 := (iff #7260 #7262)
#4140 := (iff #4132 #4139)
#4137 := (iff #4130 #4136)
#4134 := (iff #4129 #4133)
#4104 := (iff #4091 #4101)
#4098 := (<= #4086 0::Int)
#4102 := (iff #4098 #4101)
#4103 := [rewrite]: #4102
#4099 := (iff #4091 #4098)
#4096 := (= #4090 #4086)
#4097 := [rewrite]: #4096
#4100 := [monotonicity #4097]: #4099
#4105 := [trans #4100 #4103]: #4104
#4135 := [monotonicity #4105]: #4134
#4138 := [monotonicity #4135]: #4137
#4141 := [monotonicity #4138]: #4140
#7264 := [monotonicity #4141]: #7263
#7271 := [trans #7264 #7261]: #7266
#7256 := [quant-inst #181]: #7260
#7272 := [mp #7256 #7271]: #7259
#7804 := [unit-resolution #7272 #7803 #7800]: #4131
#7805 := (= #1939 #4078)
#7806 := [monotonicity #7796]: #7805
#7812 := [trans #7806 #7804]: #7811
#7813 := [trans #7812 #7810]: #1941
#7814 := [unit-resolution #7795 #7813]: false
#7816 := [lemma #7814]: #7815
#8151 := [unit-resolution #7816 #7795]: #7690
#8089 := (or #8088 #4315 #4316)
#8090 := [def-axiom]: #8089
#8153 := [unit-resolution #8090 #8151]: #8152
#8154 := [unit-resolution #8153 #8150]: #4316
#3456 := (or #3968 #184)
#3457 := [def-axiom]: #3456
#8155 := [unit-resolution #3457 #7802]: #184
#3443 := (or #3980 #3726)
#3398 := [def-axiom]: #3443
#8156 := [unit-resolution #3398 #7155]: #3726
#7693 := (not #4316)
#8138 := (or #3731 #183 #7693 #7760)
#7761 := (or #183 #7693 #7760)
#8139 := (or #3731 #7761)
#8141 := (iff #8139 #8138)
#8142 := [rewrite]: #8141
#8140 := [quant-inst #1935 #181]: #8139
#8143 := [mp #8140 #8142]: #8138
#8157 := [unit-resolution #8143 #8156 #8155 #8154]: #7760
#6005 := (f5 #195 ?v0!14)
#6011 := (f4 #6005)
#6036 := (+ #5879 #6011)
#6037 := (+ #185 #6036)
#6038 := (>= #6037 0::Int)
#8046 := (not #6038)
#6012 := (* -1::Int #6011)
#6010 := (+ f3 #6012)
#6014 := (<= #6010 0::Int)
#6049 := (or #6014 #6038)
#6056 := (not #6049)
#8032 := (or #3843 #6056 #1941)
#6015 := (+ #1146 #6012)
#6013 := (+ #1940 #6015)
#6017 := (<= #6013 0::Int)
#6051 := (or #6014 #6017)
#6052 := (not #6051)
#6054 := (or #6052 #1941)
#8033 := (or #3843 #6054)
#8040 := (iff #8033 #8032)
#6067 := (or #6056 #1941)
#8035 := (or #3843 #6067)
#8038 := (iff #8035 #8032)
#8039 := [rewrite]: #8038
#8036 := (iff #8033 #8035)
#6068 := (iff #6054 #6067)
#6057 := (iff #6052 #6056)
#6055 := (iff #6051 #6049)
#6043 := (iff #6017 #6038)
#6027 := (+ #1940 #6012)
#6030 := (+ #1146 #6027)
#6034 := (<= #6030 0::Int)
#6039 := (iff #6034 #6038)
#6040 := [rewrite]: #6039
#6035 := (iff #6017 #6034)
#6031 := (= #6013 #6030)
#6032 := [rewrite]: #6031
#6033 := [monotonicity #6032]: #6035
#6044 := [trans #6033 #6040]: #6043
#6053 := [monotonicity #6044]: #6055
#6058 := [monotonicity #6053]: #6057
#6045 := [monotonicity #6058]: #6068
#8037 := [monotonicity #6045]: #8036
#8041 := [trans #8037 #8039]: #8040
#8034 := [quant-inst #1935]: #8033
#8042 := [mp #8034 #8041]: #8032
#8158 := [unit-resolution #8042 #7803 #7795]: #6056
#8047 := (or #6049 #8046)
#8048 := [def-axiom]: #8047
#8159 := [unit-resolution #8048 #8158]: #8046
#8125 := (>= #6011 0::Int)
#6251 := (<= #6011 0::Int)
#6224 := (not #6251)
#6208 := (= f28 ?v0!14)
#6209 := (not #6208)
#8164 := (iff #7690 #6209)
#8162 := (iff #4315 #6208)
#8160 := (iff #6208 #4315)
#8161 := [commutativity]: #8160
#8163 := [symm #8161]: #8162
#8165 := [monotonicity #8163]: #8164
#8166 := [mp #8151 #8165]: #6209
#6225 := (or #6208 #6224)
#325 := (<= #16 0::Int)
#326 := (not #325)
#329 := (or #12 #326)
#3607 := (forall (vars (?v0 S2) (?v1 S2)) (:pat #3600) #329)
#332 := (forall (vars (?v0 S2) (?v1 S2)) #329)
#3610 := (iff #332 #3607)
#3608 := (iff #329 #329)
#3609 := [refl]: #3608
#3611 := [quant-intro #3609]: #3610
#1486 := (~ #332 #332)
#1485 := (~ #329 #329)
#1482 := [refl]: #1485
#1487 := [nnf-pos #1482]: #1486
#21 := (< 0::Int #16)
#22 := (implies #20 #21)
#23 := (forall (vars (?v0 S2) (?v1 S2)) #22)
#335 := (iff #23 #332)
#318 := (or #12 #21)
#322 := (forall (vars (?v0 S2) (?v1 S2)) #318)
#333 := (iff #322 #332)
#330 := (iff #318 #329)
#327 := (iff #21 #326)
#328 := [rewrite]: #327
#331 := [monotonicity #328]: #330
#334 := [quant-intro #331]: #333
#323 := (iff #23 #322)
#320 := (iff #22 #318)
#321 := [rewrite]: #320
#324 := [quant-intro #321]: #323
#336 := [trans #324 #334]: #335
#317 := [asserted]: #23
#337 := [mp #317 #336]: #332
#1483 := [mp~ #337 #1487]: #332
#3612 := [mp #1483 #3611]: #3607
#7600 := (not #3607)
#8126 := (or #7600 #6208 #6224)
#8127 := (or #7600 #6225)
#8129 := (iff #8127 #8126)
#8130 := [rewrite]: #8129
#8128 := [quant-inst #181 #1935]: #8127
#8131 := [mp #8128 #8130]: #8126
#8167 := [unit-resolution #8131 #3612]: #6225
#8168 := [unit-resolution #8167 #8166]: #6224
#8169 := (or #8125 #6251)
#8170 := [th-lemma arith farkas 1 1]: #8169
#8171 := [unit-resolution #8170 #8168]: #8125
#8172 := [th-lemma arith farkas 1 -1 1 #8171 #8159 #8157]: false
#8173 := [lemma #8172]: #1942
#8376 := [unit-resolution #8173 #8396 #8389]: false
#8397 := [lemma #8376]: #1942
#3450 := (or #3968 #3962)
#3451 := [def-axiom]: #3450
#7966 := [unit-resolution #3451 #7802]: #3962
#3444 := (or #3968 #3830)
#3390 := [def-axiom]: #3444
#7967 := [unit-resolution #3390 #7802]: #3830
#5748 := (or #1922 #3835 #3843)
#4760 := (f5 #195 ?v0!13)
#4761 := (f4 #4760)
#4791 := (+ #1920 #4761)
#4792 := (+ #185 #4791)
#4951 := (>= #4792 0::Int)
#4794 := (= #4792 0::Int)
#4766 := (* -1::Int #4761)
#4767 := (+ f3 #4766)
#4768 := (<= #4767 0::Int)
#5036 := (not #4768)
#4703 := (* -1::Int #1918)
#4881 := (+ #4703 #4761)
#4879 := (+ #185 #4881)
#4882 := (>= #4879 0::Int)
#4975 := (or #4768 #4882)
#4979 := (not #4975)
#4945 := (= #1919 #1918)
#5470 := (not #4945)
#5031 := (= #1918 #1919)
#5429 := (not #5031)
#5471 := (iff #5429 #5470)
#5469 := (iff #5031 #4945)
#5468 := [commutativity]: #5469
#5472 := [monotonicity #5468]: #5471
#5428 := [hypothesis]: #1923
#5431 := (or #5429 #1922)
#5467 := [th-lemma arith triangle-eq]: #5431
#5466 := [unit-resolution #5467 #5428]: #5429
#5474 := [mp #5466 #5472]: #5470
#4981 := (or #4979 #4945)
#5494 := [hypothesis]: #3838
#4983 := (or #3843 #4979 #4945)
#4769 := (+ #1146 #4766)
#4770 := (+ #1918 #4769)
#4798 := (<= #4770 0::Int)
#4954 := (or #4768 #4798)
#4955 := (not #4954)
#4974 := (or #4955 #4945)
#5002 := (or #3843 #4974)
#5074 := (iff #5002 #4983)
#5004 := (or #3843 #4981)
#5066 := (iff #5004 #4983)
#5067 := [rewrite]: #5066
#5064 := (iff #5002 #5004)
#4977 := (iff #4974 #4981)
#4980 := (iff #4955 #4979)
#4976 := (iff #4954 #4975)
#4889 := (iff #4798 #4882)
#4871 := (+ #1918 #4766)
#4872 := (+ #1146 #4871)
#4874 := (<= #4872 0::Int)
#4883 := (iff #4874 #4882)
#4884 := [rewrite]: #4883
#4875 := (iff #4798 #4874)
#4870 := (= #4770 #4872)
#4873 := [rewrite]: #4870
#4880 := [monotonicity #4873]: #4875
#4890 := [trans #4880 #4884]: #4889
#4978 := [monotonicity #4890]: #4976
#4973 := [monotonicity #4978]: #4980
#4982 := [monotonicity #4973]: #4977
#5065 := [monotonicity #4982]: #5064
#5075 := [trans #5065 #5067]: #5074
#5003 := [quant-inst #1917]: #5002
#5035 := [mp #5003 #5075]: #4983
#5473 := [unit-resolution #5035 #5494]: #4981
#5495 := [unit-resolution #5473 #5474]: #4979
#5008 := (or #4975 #5036)
#5009 := [def-axiom]: #5008
#5496 := [unit-resolution #5009 #5495]: #5036
#5005 := (not #4882)
#5010 := (or #4975 #5005)
#5011 := [def-axiom]: #5010
#5497 := [unit-resolution #5011 #5495]: #5005
#4796 := (or #4768 #4882 #4794)
#5498 := [hypothesis]: #3830
#4854 := (or #3835 #4768 #4882 #4794)
#4799 := (+ #4761 #1920)
#4864 := (+ #185 #4799)
#4865 := (= #4864 0::Int)
#4866 := (or #4768 #4798 #4865)
#4852 := (or #3835 #4866)
#4863 := (iff #4852 #4854)
#4855 := (or #3835 #4796)
#4857 := (iff #4855 #4854)
#4862 := [rewrite]: #4857
#4888 := (iff #4852 #4855)
#4797 := (iff #4866 #4796)
#4789 := (iff #4865 #4794)
#4790 := (= #4864 #4792)
#4793 := [rewrite]: #4790
#4795 := [monotonicity #4793]: #4789
#4891 := [monotonicity #4890 #4795]: #4797
#4856 := [monotonicity #4891]: #4888
#4861 := [trans #4856 #4862]: #4863
#4853 := [quant-inst #1917]: #4852
#4952 := [mp #4853 #4861]: #4854
#5493 := [unit-resolution #4952 #5498]: #4796
#5450 := [unit-resolution #5493 #5497 #5496]: #4794
#5424 := (not #4794)
#5366 := (or #5424 #4951)
#5425 := [th-lemma arith triangle-eq]: #5366
#5423 := [unit-resolution #5425 #5450]: #4951
#5032 := (<= #1921 0::Int)
#5426 := (or #5032 #1922)
#5743 := [th-lemma arith farkas 1 1]: #5426
#5746 := [unit-resolution #5743 #5428]: #5032
#5747 := [th-lemma arith farkas 1 -1 1 #5746 #5497 #5423]: false
#5749 := [lemma #5747]: #5748
#7968 := [unit-resolution #5749 #7803 #7967]: #1922
#3449 := (or #3965 #1923 #3959)
#3342 := [def-axiom]: #3449
#7969 := [unit-resolution #3342 #7968 #7966]: #3959
#3470 := (or #3956 #3950)
#3471 := [def-axiom]: #3470
#10050 := [unit-resolution #3471 #7969]: #3950
#3469 := (or #3953 #1943 #3947)
#3465 := [def-axiom]: #3469
#10051 := [unit-resolution #3465 #10050]: #3950
#10052 := [unit-resolution #10051 #8397]: #3947
#3497 := (or #3944 #3855)
#3475 := [def-axiom]: #3497
#10053 := [unit-resolution #3475 #10052]: #3855
#10974 := (or #3860 #4541 #5087)
#11004 := (or #3860 #5090)
#10996 := (iff #11004 #10974)
#11018 := [rewrite]: #10996
#10999 := [quant-inst #2034]: #11004
#11019 := [mp #10999 #11018]: #10974
#19095 := [unit-resolution #11019 #10053]: #5090
#19096 := [unit-resolution #19095 #19086]: #5087
#11867 := (not #5087)
#11974 := (or #11867 #12022)
#12636 := [th-lemma arith triangle-eq]: #11974
#19097 := [unit-resolution #12636 #19096]: #12022
#13344 := (+ #5343 #13327)
#13366 := (>= #13344 0::Int)
#3466 := (or #3956 #3846)
#3467 := [def-axiom]: #3466
#7970 := [unit-resolution #3467 #7969]: #3846
#18080 := (or #3851 #13366)
#18086 := [quant-inst #5342]: #18080
#19087 := [unit-resolution #18086 #7970]: #13366
#15969 := (not #12022)
#19098 := (or #15968 #15969)
#3538 := (not #1988)
#5971 := [hypothesis]: #2870
#3541 := (or #2865 #3538)
#3425 := [def-axiom]: #3541
#5972 := [unit-resolution #3425 #5971]: #3538
#3536 := (or #2865 #1979)
#3539 := [def-axiom]: #3536
#5974 := [unit-resolution #3539 #5971]: #1979
#3537 := (or #2865 #1981)
#3540 := [def-axiom]: #3537
#5973 := [unit-resolution #3540 #5971]: #1981
#10629 := (or #2850 #1988 #1978)
#5727 := (= ?v1!16 f28)
#9301 := (= f28 ?v1!16)
#5888 := (f5 #195 ?v1!16)
#5889 := (f4 #5888)
#9302 := (<= #5889 0::Int)
#9711 := [hypothesis]: #3538
#5985 := (+ #1985 #4079)
#9236 := (<= #5985 0::Int)
#5682 := (f11 f21 ?v0!17)
#5683 := (= #5682 f1)
#5681 := (= ?v0!17 f28)
#5689 := (or #5681 #5683)
#5671 := (f11 #193 ?v0!17)
#5672 := (= #5671 f1)
#5694 := (iff #5672 #5689)
#9981 := (or #7518 #5694)
#5684 := (if #5681 #4057 #5683)
#5685 := (iff #5672 #5684)
#9982 := (or #7518 #5685)
#9550 := (iff #9982 #9981)
#9683 := (iff #9981 #9981)
#9737 := [rewrite]: #9683
#5695 := (iff #5685 #5694)
#5692 := (iff #5684 #5689)
#5686 := (if #5681 true #5683)
#5690 := (iff #5686 #5689)
#5691 := [rewrite]: #5690
#5687 := (iff #5684 #5686)
#5688 := [monotonicity #4060]: #5687
#5693 := [trans #5688 #5691]: #5692
#5696 := [monotonicity #5693]: #5695
#9267 := [monotonicity #5696]: #9550
#9960 := [trans #9267 #9737]: #9550
#9682 := [quant-inst #115 #181 #3 #1976]: #9982
#9972 := [mp #9682 #9960]: #9981
#10602 := [unit-resolution #9972 #3646]: #5694
#10603 := [hypothesis]: #1981
#10604 := (= #5671 #1980)
#10599 := [monotonicity #8146]: #10604
#10571 := [trans #10599 #10603]: #5672
#9787 := (not #5672)
#9971 := (not #5694)
#9963 := (or #9971 #9787 #5689)
#9964 := [def-axiom]: #9963
#10605 := [unit-resolution #9964 #10571 #10602]: #5689
#8065 := (not #5689)
#10754 := (or #9236 #8065)
#9774 := (not #9236)
#10735 := [hypothesis]: #9774
#5652 := (f19 f20 ?v0!17)
#5545 := (* -1::Int #5652)
#5605 := (+ #1985 #5545)
#5610 := (<= #5605 0::Int)
#8385 := (or #3851 #5610)
#5582 := (+ #5652 #1986)
#5595 := (>= #5582 0::Int)
#8384 := (or #3851 #5595)
#7710 := (iff #8384 #8385)
#7667 := (iff #8385 #8385)
#8392 := [rewrite]: #7667
#5612 := (iff #5595 #5610)
#5596 := (+ #1986 #5652)
#5600 := (>= #5596 0::Int)
#5611 := (iff #5600 #5610)
#5609 := [rewrite]: #5611
#5603 := (iff #5595 #5600)
#5601 := (= #5582 #5596)
#5602 := [rewrite]: #5601
#5604 := [monotonicity #5602]: #5603
#5613 := [trans #5604 #5609]: #5612
#7791 := [monotonicity #5613]: #7710
#7912 := [trans #7791 #8392]: #7710
#8393 := [quant-inst #1976]: #8384
#8060 := [mp #8393 #7912]: #8385
#9712 := [unit-resolution #8060 #7970]: #5610
#5540 := (+ #185 #5545)
#9420 := (>= #5540 0::Int)
#9400 := [hypothesis]: #5689
#8193 := (not #5681)
#9234 := (= #1985 #4078)
#9689 := (not #9234)
#9518 := (or #9689 #9236)
#9690 := [th-lemma arith triangle-eq]: #9518
#10715 := [unit-resolution #9690 #10735]: #9689
#10725 := (or #8193 #9234)
#9309 := [hypothesis]: #5681
#10737 := [monotonicity #9309]: #9234
#10736 := [hypothesis]: #9689
#10724 := [unit-resolution #10736 #10737]: false
#10726 := [lemma #10724]: #10725
#10727 := [unit-resolution #10726 #10715]: #8193
#8066 := (or #8065 #5681 #5683)
#8067 := [def-axiom]: #8066
#10723 := [unit-resolution #8067 #10727 #9400]: #5683
#8196 := (not #5683)
#9377 := (or #8196 #9420)
#9723 := (not #9420)
#9387 := [hypothesis]: #9723
#9362 := [hypothesis]: #5683
#9219 := (or #3731 #183 #8196 #9420)
#9438 := (or #183 #8196 #9420)
#9235 := (or #3731 #9438)
#9246 := (iff #9235 #9219)
#9220 := [rewrite]: #9246
#9237 := [quant-inst #1976 #181]: #9235
#8778 := [mp #9237 #9220]: #9219
#9376 := [unit-resolution #8778 #8156 #8155 #9362 #9387]: false
#9457 := [lemma #9376]: #9377
#10721 := [unit-resolution #9457 #10723]: #9420
#4080 := (+ #185 #4079)
#4439 := (<= #4080 0::Int)
#7295 := (= #185 #4078)
#10741 := (iff #4131 #7295)
#10728 := (iff #7295 #4131)
#10729 := [commutativity]: #10728
#10742 := [symm #10729]: #10741
#10743 := [mp #7804 #10742]: #7295
#10747 := (not #7295)
#10748 := (or #10747 #4439)
#10750 := [th-lemma arith triangle-eq]: #10748
#10752 := [unit-resolution #10750 #10743]: #4439
#10753 := [th-lemma arith farkas -1 1 -1 1 #10752 #10721 #9712 #10735]: false
#10749 := [lemma #10753]: #10754
#10606 := [unit-resolution #10749 #10605]: #9236
#4081 := (>= #4080 0::Int)
#7188 := (or #3851 #4081)
#7230 := [quant-inst #181]: #7188
#9459 := [unit-resolution #7230 #7970]: #4081
#4492 := (* -1::Int #1984)
#5947 := (+ #4492 #5889)
#5948 := (+ #185 #5947)
#7908 := (<= #5948 0::Int)
#5951 := (= #5948 0::Int)
#5855 := (f19 f20 ?v1!16)
#5872 := (* -1::Int #5855)
#5907 := (+ #5872 #5889)
#5908 := (+ #185 #5907)
#5909 := (>= #5908 0::Int)
#5890 := (* -1::Int #5889)
#5891 := (+ f3 #5890)
#5892 := (<= #5891 0::Int)
#5914 := (or #5892 #5909)
#5917 := (not #5914)
#5898 := (= #1984 #5855)
#10613 := (not #5898)
#5873 := (+ #1984 #5872)
#8314 := (>= #5873 0::Int)
#9718 := (not #8314)
#4924 := (+ #185 #5872)
#4925 := (<= #4924 0::Int)
#5728 := (f11 f21 ?v1!16)
#5729 := (= #5728 f1)
#9937 := (not #5729)
#5735 := (or #5727 #5729)
#9563 := (not #5735)
#5725 := (f11 #193 ?v1!16)
#5726 := (= #5725 f1)
#5740 := (iff #5726 #5735)
#9884 := (or #7518 #5740)
#5730 := (if #5727 #4057 #5729)
#5731 := (iff #5726 #5730)
#9851 := (or #7518 #5731)
#9678 := (iff #9851 #9884)
#9677 := (iff #9884 #9884)
#9566 := [rewrite]: #9677
#5741 := (iff #5731 #5740)
#5738 := (iff #5730 #5735)
#5732 := (if #5727 true #5729)
#5736 := (iff #5732 #5735)
#5737 := [rewrite]: #5736
#5733 := (iff #5730 #5732)
#5734 := [monotonicity #4060]: #5733
#5739 := [trans #5734 #5737]: #5738
#5742 := [monotonicity #5739]: #5741
#9679 := [monotonicity #5742]: #9678
#8478 := [trans #9679 #9566]: #9678
#9932 := [quant-inst #115 #181 #3 #1975]: #9851
#7394 := [mp #9932 #8478]: #9884
#10476 := [unit-resolution #7394 #3646]: #5740
#8333 := (not #5726)
#10578 := (iff #1979 #8333)
#10579 := (iff #1978 #5726)
#10551 := (iff #5726 #1978)
#10541 := (= #5725 #1977)
#10544 := [monotonicity #8146]: #10541
#10552 := [monotonicity #10544]: #10551
#10580 := [symm #10552]: #10579
#10581 := [monotonicity #10580]: #10578
#10477 := [hypothesis]: #1979
#10600 := [mp #10477 #10581]: #8333
#8954 := (not #5740)
#9175 := (or #8954 #5726 #9563)
#7890 := [def-axiom]: #9175
#10601 := [unit-resolution #7890 #10600 #10476]: #9563
#8489 := (or #5735 #9937)
#9914 := [def-axiom]: #8489
#10607 := [unit-resolution #9914 #10601]: #9937
#4948 := (or #5729 #4925)
#3462 := (or #3968 #3820)
#3463 := [def-axiom]: #3462
#9789 := [unit-resolution #3463 #7802]: #3820
#9716 := (or #3825 #5729 #4925)
#4892 := (+ #5855 #1146)
#4893 := (>= #4892 0::Int)
#4918 := (or #5729 #4893)
#9628 := (or #3825 #4918)
#10139 := (iff #9628 #9716)
#10115 := (or #3825 #4948)
#10118 := (iff #10115 #9716)
#10138 := [rewrite]: #10118
#10117 := (iff #9628 #10115)
#4949 := (iff #4918 #4948)
#4946 := (iff #4893 #4925)
#4919 := (+ #1146 #5855)
#4922 := (>= #4919 0::Int)
#4926 := (iff #4922 #4925)
#4927 := [rewrite]: #4926
#4917 := (iff #4893 #4922)
#4920 := (= #4892 #4919)
#4921 := [rewrite]: #4920
#4923 := [monotonicity #4921]: #4917
#4947 := [trans #4923 #4927]: #4946
#4950 := [monotonicity #4947]: #4949
#10112 := [monotonicity #4950]: #10117
#10140 := [trans #10112 #10138]: #10139
#10116 := [quant-inst #1975]: #9628
#10141 := [mp #10116 #10140]: #9716
#10608 := [unit-resolution #10141 #9789]: #4948
#10609 := [unit-resolution #10608 #10607]: #4925
#11010 := (not #4925)
#11011 := (or #9774 #9718 #1988 #11010)
#11006 := [hypothesis]: #4925
#9759 := [hypothesis]: #9236
#9707 := [hypothesis]: #8314
#11009 := [th-lemma arith farkas -1 1 1 -1 1 #9707 #9759 #9711 #9459 #11006]: false
#11012 := [lemma #11009]: #11011
#10612 := [unit-resolution #11012 #10606 #9711 #10609]: #9718
#10614 := (or #10613 #8314)
#10615 := [th-lemma arith triangle-eq]: #10614
#10610 := [unit-resolution #10615 #10612]: #10613
#5920 := (or #5917 #5898)
#10033 := (or #3843 #5917 #5898)
#5893 := (+ #1146 #5890)
#5894 := (+ #5855 #5893)
#5895 := (<= #5894 0::Int)
#5896 := (or #5892 #5895)
#5897 := (not #5896)
#5899 := (or #5897 #5898)
#10016 := (or #3843 #5899)
#9991 := (iff #10016 #10033)
#10017 := (or #3843 #5920)
#10008 := (iff #10017 #10033)
#10004 := [rewrite]: #10008
#9989 := (iff #10016 #10017)
#5921 := (iff #5899 #5920)
#5918 := (iff #5897 #5917)
#5915 := (iff #5896 #5914)
#5912 := (iff #5895 #5909)
#5900 := (+ #5855 #5890)
#5901 := (+ #1146 #5900)
#5904 := (<= #5901 0::Int)
#5910 := (iff #5904 #5909)
#5911 := [rewrite]: #5910
#5905 := (iff #5895 #5904)
#5902 := (= #5894 #5901)
#5903 := [rewrite]: #5902
#5906 := [monotonicity #5903]: #5905
#5913 := [trans #5906 #5911]: #5912
#5916 := [monotonicity #5913]: #5915
#5919 := [monotonicity #5916]: #5918
#5922 := [monotonicity #5919]: #5921
#10005 := [monotonicity #5922]: #9989
#10002 := [trans #10005 #10004]: #9991
#9962 := [quant-inst #1975]: #10016
#10010 := [mp #9962 #10002]: #10033
#10611 := [unit-resolution #10010 #7803]: #5920
#10616 := [unit-resolution #10611 #10610]: #5917
#9749 := (or #5914 #5951)
#9732 := (not #5951)
#9742 := [hypothesis]: #9732
#8264 := (not #5892)
#9745 := [hypothesis]: #5917
#8000 := (or #5914 #8264)
#8092 := [def-axiom]: #8000
#9727 := [unit-resolution #8092 #9745]: #8264
#8284 := (not #5909)
#8311 := (or #5914 #8284)
#8280 := [def-axiom]: #8311
#9746 := [unit-resolution #8280 #9745]: #8284
#5954 := (or #5892 #5909 #5951)
#8310 := (or #3835 #5892 #5909 #5951)
#5943 := (+ #5889 #4492)
#5944 := (+ #185 #5943)
#5945 := (= #5944 0::Int)
#5946 := (or #5892 #5895 #5945)
#8334 := (or #3835 #5946)
#8377 := (iff #8334 #8310)
#8335 := (or #3835 #5954)
#8378 := (iff #8335 #8310)
#8379 := [rewrite]: #8378
#8336 := (iff #8334 #8335)
#5955 := (iff #5946 #5954)
#5952 := (iff #5945 #5951)
#5949 := (= #5944 #5948)
#5950 := [rewrite]: #5949
#5953 := [monotonicity #5950]: #5952
#5956 := [monotonicity #5913 #5953]: #5955
#8337 := [monotonicity #5956]: #8336
#8371 := [trans #8337 #8379]: #8377
#8279 := [quant-inst #1975]: #8334
#8381 := [mp #8279 #8371]: #8310
#9747 := [unit-resolution #8381 #7967]: #5954
#9748 := [unit-resolution #9747 #9746 #9727 #9742]: false
#9750 := [lemma #9748]: #9749
#10617 := [unit-resolution #9750 #10616]: #5951
#10618 := (or #9732 #7908)
#10619 := [th-lemma arith triangle-eq]: #10618
#10620 := [unit-resolution #10619 #10617]: #7908
#10624 := (not #4081)
#10623 := (not #7908)
#10625 := (or #9302 #10623 #1988 #9774 #10624)
#10626 := [th-lemma arith assign-bounds 1 1 1 1]: #10625
#10621 := [unit-resolution #10626 #10620 #9459 #10606 #9711]: #9302
#9349 := (not #9302)
#10411 := (or #7600 #9301 #9349)
#9385 := (or #9301 #9349)
#10539 := (or #7600 #9385)
#10540 := (iff #10539 #10411)
#10542 := [rewrite]: #10540
#10381 := [quant-inst #181 #1975]: #10539
#10543 := [mp #10381 #10542]: #10411
#10622 := [unit-resolution #10543 #3612 #10621]: #9301
#10627 := [symm #10622]: #5727
#7819 := (not #5727)
#9916 := (or #5735 #7819)
#9935 := [def-axiom]: #9916
#10577 := [unit-resolution #9935 #10601]: #7819
#10628 := [unit-resolution #10577 #10627]: false
#10630 := [lemma #10628]: #10629
#9889 := [unit-resolution #10630 #5973 #5974 #5972]: false
#9891 := [lemma #9889]: #2865
#8784 := (or #1962 #3860)
#4183 := (>= #185 0::Int)
#3442 := (or #3980 #3717)
#3422 := [def-axiom]: #3442
#7614 := [unit-resolution #3422 #7155]: #3717
#7345 := (or #3722 #4183)
#7351 := [quant-inst #181]: #7345
#7620 := [unit-resolution #7351 #7614]: #4183
#6537 := (f5 #195 ?v0!15)
#6538 := (f4 #6537)
#4488 := (* -1::Int #1961)
#6594 := (+ #4488 #6538)
#6595 := (+ #185 #6594)
#8465 := (<= #6595 0::Int)
#6598 := (= #6595 0::Int)
#6496 := (f19 f20 ?v0!15)
#6521 := (* -1::Int #6496)
#6555 := (+ #6521 #6538)
#6556 := (+ #185 #6555)
#6557 := (>= #6556 0::Int)
#6539 := (* -1::Int #6538)
#6540 := (+ f3 #6539)
#6541 := (<= #6540 0::Int)
#6562 := (or #6541 #6557)
#6565 := (not #6562)
#6497 := (= #1961 #6496)
#9674 := (not #6497)
#6522 := (+ #1961 #6521)
#9653 := (>= #6522 0::Int)
#9661 := (not #9653)
#6618 := [hypothesis]: #1963
#9453 := (or #9661 #1962)
#8190 := (>= #6496 0::Int)
#8498 := (or #3722 #8190)
#8474 := [quant-inst #1960]: #8498
#9421 := [unit-resolution #8474 #7614]: #8190
#9654 := [hypothesis]: #9653
#9452 := [th-lemma arith farkas -1 1 1 #6618 #9654 #9421]: false
#9454 := [lemma #9452]: #9453
#8733 := [unit-resolution #9454 #6618]: #9661
#9675 := (or #9674 #9653)
#8499 := [hypothesis]: #9661
#8502 := [hypothesis]: #6497
#9676 := [th-lemma arith triangle-eq]: #9675
#8503 := [unit-resolution #9676 #8502 #8499]: false
#8506 := [lemma #8503]: #9675
#8735 := [unit-resolution #8506 #8733]: #9674
#6568 := (or #6565 #6497)
#8443 := (or #3843 #6565 #6497)
#6542 := (+ #1146 #6539)
#6543 := (+ #6496 #6542)
#6544 := (<= #6543 0::Int)
#6545 := (or #6541 #6544)
#6546 := (not #6545)
#6547 := (or #6546 #6497)
#8444 := (or #3843 #6547)
#8433 := (iff #8444 #8443)
#8446 := (or #3843 #6568)
#8449 := (iff #8446 #8443)
#8432 := [rewrite]: #8449
#8447 := (iff #8444 #8446)
#6569 := (iff #6547 #6568)
#6566 := (iff #6546 #6565)
#6563 := (iff #6545 #6562)
#6560 := (iff #6544 #6557)
#6548 := (+ #6496 #6539)
#6549 := (+ #1146 #6548)
#6552 := (<= #6549 0::Int)
#6558 := (iff #6552 #6557)
#6559 := [rewrite]: #6558
#6553 := (iff #6544 #6552)
#6550 := (= #6543 #6549)
#6551 := [rewrite]: #6550
#6554 := [monotonicity #6551]: #6553
#6561 := [trans #6554 #6559]: #6560
#6564 := [monotonicity #6561]: #6563
#6567 := [monotonicity #6564]: #6566
#6570 := [monotonicity #6567]: #6569
#8448 := [monotonicity #6570]: #8447
#8434 := [trans #8448 #8432]: #8433
#8445 := [quant-inst #1960]: #8444
#8435 := [mp #8445 #8434]: #8443
#9672 := [unit-resolution #8435 #7803]: #6568
#8736 := [unit-resolution #9672 #8735]: #6565
#9651 := (or #6562 #6598)
#9644 := (not #6598)
#9645 := [hypothesis]: #9644
#8436 := (not #6541)
#9646 := [hypothesis]: #6565
#8431 := (or #6562 #8436)
#8437 := [def-axiom]: #8431
#9647 := [unit-resolution #8437 #9646]: #8436
#8438 := (not #6557)
#8439 := (or #6562 #8438)
#8440 := [def-axiom]: #8439
#9648 := [unit-resolution #8440 #9646]: #8438
#6601 := (or #6541 #6557 #6598)
#8452 := (or #3835 #6541 #6557 #6598)
#6590 := (+ #6538 #4488)
#6591 := (+ #185 #6590)
#6592 := (= #6591 0::Int)
#6593 := (or #6541 #6544 #6592)
#8453 := (or #3835 #6593)
#8459 := (iff #8453 #8452)
#8455 := (or #3835 #6601)
#8457 := (iff #8455 #8452)
#8458 := [rewrite]: #8457
#8450 := (iff #8453 #8455)
#6602 := (iff #6593 #6601)
#6599 := (iff #6592 #6598)
#6596 := (= #6591 #6595)
#6597 := [rewrite]: #6596
#6600 := [monotonicity #6597]: #6599
#6603 := [monotonicity #6561 #6600]: #6602
#8456 := [monotonicity #6603]: #8450
#8460 := [trans #8456 #8458]: #8459
#8454 := [quant-inst #1960]: #8453
#8464 := [mp #8454 #8460]: #8452
#9649 := [unit-resolution #8464 #7967]: #6601
#9650 := [unit-resolution #9649 #9648 #9647 #9645]: false
#9652 := [lemma #9650]: #9651
#8729 := [unit-resolution #9652 #8736]: #6598
#9668 := (or #9644 #8465)
#9669 := [th-lemma arith triangle-eq]: #9668
#8737 := [unit-resolution #9669 #8729]: #8465
#8633 := (>= #6538 0::Int)
#9565 := (<= #6538 0::Int)
#9568 := (not #9565)
#9564 := (= f28 ?v0!15)
#9601 := (not #9564)
#9422 := (= ?v0!15 f28)
#9445 := (not #9422)
#9602 := (iff #9445 #9601)
#9625 := (iff #9422 #9564)
#9571 := (iff #9564 #9422)
#9624 := [commutativity]: #9571
#9626 := [symm #9624]: #9625
#9603 := [monotonicity #9626]: #9602
#8093 := (f11 f21 ?v0!15)
#8097 := (= #8093 f1)
#9428 := (or #9422 #8097)
#9451 := (not #9428)
#9414 := (f11 #193 ?v0!15)
#9415 := (= #9414 f1)
#9433 := (iff #9415 #9428)
#8508 := (or #7518 #9433)
#9423 := (if #9422 #4057 #8097)
#9424 := (iff #9415 #9423)
#8509 := (or #7518 #9424)
#8511 := (iff #8509 #8508)
#8510 := (iff #8508 #8508)
#8514 := [rewrite]: #8510
#9434 := (iff #9424 #9433)
#9431 := (iff #9423 #9428)
#9425 := (if #9422 true #8097)
#9429 := (iff #9425 #9428)
#9430 := [rewrite]: #9429
#9426 := (iff #9423 #9425)
#9427 := [monotonicity #4060]: #9426
#9432 := [trans #9427 #9430]: #9431
#9435 := [monotonicity #9432]: #9434
#8512 := [monotonicity #9435]: #8511
#8515 := [trans #8512 #8514]: #8511
#8507 := [quant-inst #115 #181 #3 #1960]: #8509
#8513 := [mp #8507 #8515]: #8508
#8738 := [unit-resolution #8513 #3646]: #9433
#8520 := (not #9415)
#4485 := (f11 f29 ?v0!15)
#4486 := (= #4485 f1)
#4487 := (not #4486)
#8754 := (iff #4487 #8520)
#8755 := (iff #4486 #9415)
#8702 := (iff #9415 #4486)
#8748 := (= #9414 #4485)
#8749 := [monotonicity #8146]: #8748
#8703 := [monotonicity #8749]: #8702
#8756 := [symm #8703]: #8755
#8757 := [monotonicity #8756]: #8754
#6506 := (or #4487 #6497)
#8739 := [hypothesis]: #3855
#8421 := (or #3860 #4487 #6497)
#8422 := (or #3860 #6506)
#8406 := (iff #8422 #8421)
#8424 := [rewrite]: #8406
#8423 := [quant-inst #1960]: #8422
#8405 := [mp #8423 #8424]: #8421
#8744 := [unit-resolution #8405 #8739]: #6506
#8745 := [unit-resolution #8744 #8735]: #4487
#8758 := [mp #8745 #8757]: #8520
#8518 := (not #9433)
#8519 := (or #8518 #9415 #9451)
#8517 := [def-axiom]: #8519
#8767 := [unit-resolution #8517 #8758 #8738]: #9451
#9446 := (or #9428 #9445)
#9447 := [def-axiom]: #9446
#8768 := [unit-resolution #9447 #8767]: #9445
#8774 := [mp #8768 #9603]: #9601
#9572 := (or #9564 #9568)
#9574 := (or #7600 #9564 #9568)
#9575 := (or #7600 #9572)
#9579 := (iff #9575 #9574)
#9580 := [rewrite]: #9579
#9576 := [quant-inst #181 #1960]: #9575
#9578 := [mp #9576 #9580]: #9574
#9605 := [unit-resolution #9578 #3612]: #9572
#8775 := [unit-resolution #9605 #8774]: #9568
#8773 := (or #8633 #9565)
#8776 := [th-lemma arith farkas 1 1]: #8773
#8769 := [unit-resolution #8776 #8775]: #8633
#8777 := [th-lemma arith farkas 1 1 -1 1 #6618 #8769 #8737 #7620]: false
#8782 := [lemma #8777]: #8784
#10054 := [unit-resolution #8782 #10053]: #1962
#4342 := (f5 #195 f16)
#4343 := (f4 #4342)
#7596 := (<= #4343 0::Int)
#7588 := (not #7596)
#4163 := (= f28 f16)
#7583 := (not #4163)
#7834 := [hypothesis]: #661
#7847 := (or #7583 #217)
#4358 := (= #216 #110)
#7840 := (= #185 #110)
#7835 := [hypothesis]: #4163
#7841 := [monotonicity #7835]: #7840
#7842 := (= #216 #185)
#7838 := (= #216 #4078)
#7836 := (= f16 f28)
#7837 := [symm #7835]: #7836
#7839 := [monotonicity #7837]: #7838
#7843 := [trans #7839 #7804]: #7842
#7844 := [trans #7843 #7841]: #4358
#7845 := [trans #7844 #6894]: #217
#7846 := [unit-resolution #7834 #7845]: false
#7848 := [lemma #7846]: #7847
#7599 := [unit-resolution #7848 #7834]: #7583
#7589 := (or #4163 #7588)
#7601 := (or #7600 #4163 #7588)
#7602 := (or #7600 #7589)
#7604 := (iff #7602 #7601)
#7605 := [rewrite]: #7604
#7603 := [quant-inst #181 #65]: #7602
#7606 := [mp #7603 #7605]: #7601
#7607 := [unit-resolution #7606 #3612]: #7589
#7598 := [unit-resolution #7607 #7599]: #7588
#4350 := (* -1::Int #4343)
#4353 := (+ #1146 #4350)
#4354 := (+ #110 #4353)
#4355 := (<= #4354 0::Int)
#7500 := (not #4355)
#4351 := (+ f3 #4350)
#4352 := (<= #4351 0::Int)
#4356 := (or #4352 #4355)
#4357 := (not #4356)
#7612 := (not #4358)
#7613 := (iff #661 #7612)
#7610 := (iff #217 #4358)
#7608 := (iff #4358 #217)
#7609 := [monotonicity #6894]: #7608
#7611 := [symm #7609]: #7610
#7615 := [monotonicity #7611]: #7613
#7616 := [mp #7834 #7615]: #7612
#4359 := (or #4357 #4358)
#7491 := (or #3843 #4357 #4358)
#7492 := (or #3843 #4359)
#7494 := (iff #7492 #7491)
#7495 := [rewrite]: #7494
#7493 := [quant-inst #65]: #7492
#7496 := [mp #7493 #7495]: #7491
#7617 := [unit-resolution #7496 #7803]: #4359
#7618 := [unit-resolution #7617 #7616]: #4357
#7501 := (or #4356 #7500)
#7502 := [def-axiom]: #7501
#7619 := [unit-resolution #7502 #7618]: #7500
#4504 := (<= #110 0::Int)
#7621 := (or #804 #4504)
#7622 := [th-lemma arith triangle-eq]: #7621
#7623 := [unit-resolution #7622 #6894]: #4504
#7624 := [th-lemma arith farkas 1 1 1 1 #7623 #7620 #7619 #7598]: false
#7626 := [lemma #7624]: #217
#3476 := (or #3944 #3938)
#3478 := [def-axiom]: #3476
#10055 := [unit-resolution #3478 #10052]: #3938
#3496 := (or #3941 #661 #3935)
#3486 := [def-axiom]: #3496
#10056 := [unit-resolution #3486 #10055 #7626]: #3935
#3488 := (or #3932 #3926)
#3489 := [def-axiom]: #3488
#10057 := [unit-resolution #3489 #10056]: #3926
#3504 := (or #3929 #1963 #3923)
#3484 := [def-axiom]: #3504
#10058 := [unit-resolution #3484 #10057 #10054]: #3923
#3507 := (or #3920 #3914)
#3512 := [def-axiom]: #3507
#18172 := [unit-resolution #3512 #10058]: #3914
#3508 := (or #3917 #2870 #3911)
#3509 := [def-axiom]: #3508
#18183 := [unit-resolution #3509 #18172]: #3914
#18184 := [unit-resolution #18183 #9891]: #3911
#3517 := (or #3908 #3902)
#3518 := [def-axiom]: #3517
#18185 := [unit-resolution #3518 #18184]: #3902
#18186 := (or #3905 #3899)
#15845 := [hypothesis]: #2916
#3530 := (or #2911 #2012)
#3533 := [def-axiom]: #3530
#15846 := [unit-resolution #3533 #15845]: #2012
#6483 := (f5 #195 ?v0!19)
#6481 := (f4 #6483)
#6484 := (* -1::Int #6481)
#15446 := (+ #2008 #6484)
#15535 := (>= #15446 0::Int)
#15445 := (= #2008 #6481)
#15962 := (= #2007 #6483)
#15956 := (= #2006 #195)
#5407 := (= ?v1!18 f28)
#5408 := (f11 f21 ?v1!18)
#5409 := (= #5408 f1)
#5415 := (or #5407 #5409)
#5397 := (f11 #193 ?v1!18)
#5398 := (= #5397 f1)
#5420 := (iff #5398 #5415)
#14616 := (or #7518 #5420)
#5410 := (if #5407 #4057 #5409)
#5411 := (iff #5398 #5410)
#14606 := (or #7518 #5411)
#14610 := (iff #14606 #14616)
#14613 := (iff #14616 #14616)
#14619 := [rewrite]: #14613
#5421 := (iff #5411 #5420)
#5418 := (iff #5410 #5415)
#5412 := (if #5407 true #5409)
#5416 := (iff #5412 #5415)
#5417 := [rewrite]: #5416
#5413 := (iff #5410 #5412)
#5414 := [monotonicity #4060]: #5413
#5419 := [trans #5414 #5417]: #5418
#5422 := [monotonicity #5419]: #5421
#14620 := [monotonicity #5422]: #14610
#14630 := [trans #14620 #14619]: #14610
#14618 := [quant-inst #115 #181 #3 #2002]: #14606
#14662 := [mp #14618 #14630]: #14616
#15893 := [unit-resolution #14662 #3646]: #5420
#3434 := (or #2911 #2005)
#3529 := [def-axiom]: #3434
#15907 := [unit-resolution #3529 #15845]: #2005
#15926 := (= #5397 #2004)
#15928 := [monotonicity #8146]: #15926
#15908 := [trans #15928 #15907]: #5398
#11373 := (not #5398)
#15102 := (not #5420)
#15199 := (or #15102 #11373 #5415)
#15197 := [def-axiom]: #15199
#15929 := [unit-resolution #15197 #15908 #15893]: #5415
#6623 := (not #5409)
#6374 := (f19 f20 ?v0!19)
#6445 := (* -1::Int #6374)
#5362 := (f19 f20 ?v1!18)
#6639 := (+ #5362 #6445)
#6640 := (+ #2008 #6639)
#6641 := (>= #6640 0::Int)
#15933 := (not #6641)
#3418 := (not #2020)
#3433 := (or #2911 #3418)
#3435 := [def-axiom]: #3433
#15930 := [unit-resolution #3435 #15845]: #3418
#6446 := (+ #2016 #6445)
#6447 := (<= #6446 0::Int)
#12992 := (not #6447)
#12993 := [hypothesis]: #12992
#12524 := (or #3851 #6447)
#6389 := (+ #6374 #2017)
#6399 := (>= #6389 0::Int)
#12525 := (or #3851 #6399)
#12527 := (iff #12525 #12524)
#12530 := (iff #12524 #12524)
#12531 := [rewrite]: #12530
#6468 := (iff #6399 #6447)
#6440 := (+ #2017 #6374)
#6443 := (>= #6440 0::Int)
#6448 := (iff #6443 #6447)
#6467 := [rewrite]: #6448
#6438 := (iff #6399 #6443)
#6441 := (= #6389 #6440)
#6442 := [rewrite]: #6441
#6444 := [monotonicity #6442]: #6438
#6469 := [trans #6444 #6467]: #6468
#12529 := [monotonicity #6469]: #12527
#12532 := [trans #12529 #12531]: #12527
#12526 := [quant-inst #2003]: #12525
#12533 := [mp #12526 #12532]: #12524
#12610 := [unit-resolution #12533 #7970 #12993]: false
#12611 := [lemma #12610]: #6447
#5459 := (* -1::Int #5362)
#5460 := (+ #2015 #5459)
#12226 := (>= #5460 0::Int)
#5380 := (= #2015 #5362)
#12307 := (or #3860 #2896 #5380)
#5383 := (or #2896 #5380)
#12303 := (or #3860 #5383)
#12279 := (iff #12303 #12307)
#12410 := [rewrite]: #12279
#12304 := [quant-inst #2002]: #12303
#12398 := [mp #12304 #12410]: #12307
#15925 := [unit-resolution #12398 #10053 #15907]: #5380
#15889 := (not #5380)
#15931 := (or #15889 #12226)
#15927 := [th-lemma arith triangle-eq]: #15931
#15932 := [unit-resolution #15927 #15925]: #12226
#15883 := (not #12226)
#15934 := (or #15933 #15883 #12992 #2020)
#15935 := [th-lemma arith assign-bounds 1 -1 -1]: #15934
#15955 := [unit-resolution #15935 #15932 #12611 #15930]: #15933
#15957 := (or #6623 #6641)
#15290 := (or #3739 #6623 #2011 #6641)
#6642 := (or #6623 #2011 #6641)
#15291 := (or #3739 #6642)
#15288 := (iff #15291 #15290)
#15308 := [rewrite]: #15288
#15270 := [quant-inst #2003 #2002]: #15291
#15282 := [mp #15270 #15308]: #15290
#15958 := [unit-resolution #15282 #7156 #15846]: #15957
#15954 := [unit-resolution #15958 #15955]: #6623
#15090 := (not #5415)
#15098 := (or #15090 #5407 #5409)
#15091 := [def-axiom]: #15098
#15960 := [unit-resolution #15091 #15954 #15929]: #5407
#15961 := [monotonicity #15960]: #15956
#15959 := [monotonicity #15961]: #15962
#15963 := [monotonicity #15959]: #15445
#15964 := (not #15445)
#13461 := (or #15964 #15535)
#11575 := [th-lemma arith triangle-eq]: #13461
#14042 := [unit-resolution #11575 #15963]: #15535
#6485 := (+ f3 #6484)
#6486 := (<= #6485 0::Int)
#6610 := (+ #2017 #6481)
#6611 := (+ #185 #6610)
#6614 := (= #6611 0::Int)
#15542 := (not #6614)
#14614 := (>= #6611 0::Int)
#13597 := (not #14614)
#6363 := (+ #2015 #4079)
#6364 := (>= #6363 0::Int)
#7961 := (= #2015 #4078)
#14062 := [monotonicity #15960]: #7961
#15213 := (not #7961)
#15268 := (or #15213 #6364)
#15479 := [th-lemma arith triangle-eq]: #15268
#15484 := [unit-resolution #15479 #14062]: #6364
#12694 := (not #15535)
#14493 := (not #4439)
#15269 := (not #6364)
#12544 := (or #13597 #2020 #15269 #14493 #12694)
#14974 := [th-lemma arith assign-bounds -1 1 -1 1]: #12544
#15581 := [unit-resolution #14974 #15930 #10752 #15484 #14042]: #13597
#15702 := (or #15542 #14614)
#15714 := [th-lemma arith triangle-eq]: #15702
#15715 := [unit-resolution #15714 #15581]: #15542
#6511 := (+ #6445 #6481)
#6509 := (+ #185 #6511)
#6512 := (>= #6509 0::Int)
#13034 := (not #6512)
#15736 := (or #13034 #12992 #2020 #15269 #14493 #12694)
#15582 := [th-lemma arith assign-bounds -1 -1 1 -1 1]: #15736
#15841 := [unit-resolution #15582 #15930 #12611 #10752 #15484 #14042]: #13034
#5073 := (or #6486 #6512 #6614)
#14397 := (or #3835 #6486 #6512 #6614)
#6607 := (+ #6481 #2017)
#6608 := (+ #185 #6607)
#6609 := (= #6608 0::Int)
#6491 := (+ #1146 #6484)
#6492 := (+ #6374 #6491)
#6490 := (<= #6492 0::Int)
#6604 := (or #6486 #6490 #6609)
#12671 := (or #3835 #6604)
#14485 := (iff #12671 #14397)
#14423 := (or #3835 #5073)
#14478 := (iff #14423 #14397)
#14483 := [rewrite]: #14478
#14389 := (iff #12671 #14423)
#5263 := (iff #6604 #5073)
#5033 := (iff #6609 #6614)
#6612 := (= #6608 #6611)
#6613 := [rewrite]: #6612
#5034 := [monotonicity #6613]: #5033
#6529 := (iff #6490 #6512)
#6499 := (+ #6374 #6484)
#6500 := (+ #1146 #6499)
#6502 := (<= #6500 0::Int)
#6513 := (iff #6502 #6512)
#6514 := [rewrite]: #6513
#6503 := (iff #6490 #6502)
#6498 := (= #6492 #6500)
#6501 := [rewrite]: #6498
#6510 := [monotonicity #6501]: #6503
#6530 := [trans #6510 #6514]: #6529
#5264 := [monotonicity #6530 #5034]: #5263
#14396 := [monotonicity #5264]: #14389
#14472 := [trans #14396 #14483]: #14485
#14422 := [quant-inst #2003]: #12671
#14486 := [mp #14422 #14472]: #14397
#15735 := [unit-resolution #14486 #7967]: #5073
#15853 := [unit-resolution #15735 #15841 #15715]: #6486
#15854 := [th-lemma arith farkas -1 1 1 #15853 #14042 #15846]: false
#15894 := [lemma #15854]: #2911
#3526 := (or #3905 #2916 #3899)
#3527 := [def-axiom]: #3526
#18187 := [unit-resolution #3527 #15894]: #18186
#18188 := [unit-resolution #18187 #18185]: #3899
#3441 := (or #3896 #2041)
#3534 := [def-axiom]: #3441
#18189 := [unit-resolution #3534 #18188]: #2041
#15970 := (or #15968 #15969 #2040)
#13634 := [hypothesis]: #2041
#15965 := [hypothesis]: #12022
#15966 := [hypothesis]: #5341
#15967 := [th-lemma arith farkas -1 1 1 #15966 #15965 #13634]: false
#15971 := [lemma #15967]: #15970
#19099 := [unit-resolution #15971 #18189]: #19098
#19100 := [unit-resolution #19099 #19097]: #15968
#15703 := (or #5341 #5359)
#3439 := (or #3896 #2036)
#3440 := [def-axiom]: #3439
#19101 := [unit-resolution #3440 #18188]: #2036
#12207 := (or #3747 #2035 #5341 #5359)
#5360 := (or #2035 #5341 #5359)
#12245 := (or #3747 #5360)
#12251 := (iff #12245 #12207)
#12352 := [rewrite]: #12251
#12240 := [quant-inst #2034]: #12245
#12292 := [mp #12240 #12352]: #12207
#19102 := [unit-resolution #12292 #7427 #19101]: #15703
#19103 := [unit-resolution #19102 #19100]: #5359
#15553 := (or #5358 #5356)
#15554 := [def-axiom]: #15553
#18351 := [unit-resolution #15554 #19103]: #5356
#18355 := (or #5357 #15530)
#18361 := [th-lemma arith triangle-eq]: #18355
#18362 := [unit-resolution #18361 #18351]: #15530
#19106 := (not #13366)
#18364 := (not #15530)
#18350 := (or #18243 #18364 #15969 #19106)
#18365 := [th-lemma arith assign-bounds 1 1 1]: #18350
#18367 := [unit-resolution #18365 #18362 #19087 #19097]: #18243
#14134 := (<= #14210 0::Int)
#14035 := (+ f3 #5353)
#14131 := (<= #14035 0::Int)
#18369 := (not #14131)
#13911 := (>= #5343 0::Int)
#18177 := (or #3722 #13911)
#18180 := [quant-inst #5342]: #18177
#18368 := [unit-resolution #18180 #7614]: #13911
#18363 := (not #13911)
#18372 := (or #18369 #18363 #18364 #15969)
#18371 := (or #18369 #18363 #18364 #2040 #15969)
#18366 := [th-lemma arith assign-bounds -1 -1 -1 -1]: #18371
#18373 := [unit-resolution #18366 #18189]: #18372
#18378 := [unit-resolution #18373 #18368 #18362 #19097]: #18369
#13322 := (f11 f29 #5342)
#13321 := (= #13322 f1)
#15207 := (+ #2037 #13327)
#15217 := (<= #15207 0::Int)
#19105 := (not #15217)
#12311 := (not #5346)
#12351 := (or #5358 #12311)
#12297 := [def-axiom]: #12351
#19104 := [unit-resolution #12297 #19103]: #12311
#19107 := (or #19105 #5346 #15969 #19106)
#19108 := [th-lemma arith assign-bounds 1 1 1]: #19107
#19109 := [unit-resolution #19108 #19104 #19097 #19087]: #19105
#15548 := (or #13321 #4541 #15217)
#3523 := (or #3908 #3872)
#3528 := [def-axiom]: #3523
#18201 := [unit-resolution #3528 #18184]: #3872
#10669 := (or #3877 #13321 #4541 #15217)
#14133 := (+ #13325 #2038)
#15115 := (>= #14133 0::Int)
#15556 := (or #13321 #4541 #15115)
#10675 := (or #3877 #15556)
#10689 := (iff #10675 #10669)
#10671 := (or #3877 #15548)
#10662 := (iff #10671 #10669)
#10672 := [rewrite]: #10662
#10679 := (iff #10675 #10671)
#15557 := (iff #15556 #15548)
#15222 := (iff #15115 #15217)
#15259 := (+ #2038 #13325)
#15255 := (>= #15259 0::Int)
#15218 := (iff #15255 #15217)
#15261 := [rewrite]: #15218
#15208 := (iff #15115 #15255)
#15253 := (= #14133 #15259)
#15258 := [rewrite]: #15253
#15216 := [monotonicity #15258]: #15208
#15202 := [trans #15216 #15261]: #15222
#15555 := [monotonicity #15202]: #15557
#10681 := [monotonicity #15555]: #10679
#10677 := [trans #10681 #10672]: #10689
#10676 := [quant-inst #2034 #5342]: #10675
#10678 := [mp #10676 #10677]: #10669
#19114 := [unit-resolution #10678 #18201]: #15548
#18370 := [unit-resolution #19114 #19109 #19086]: #13321
#13323 := (not #13321)
#11985 := (or #13323 #14131 #14134)
#3437 := (or #3896 #3880)
#3438 := [def-axiom]: #3437
#18542 := [unit-resolution #3438 #18188]: #3880
#18156 := (or #3885 #13323 #14131 #14134)
#14205 := (+ #5352 #14133)
#12308 := (>= #14205 0::Int)
#11983 := (or #13323 #14131 #12308)
#18152 := (or #3885 #11983)
#18167 := (iff #18152 #18156)
#18181 := (or #3885 #11985)
#17096 := (iff #18181 #18156)
#18166 := [rewrite]: #17096
#18182 := (iff #18152 #18181)
#12007 := (iff #11983 #11985)
#14226 := (iff #12308 #14134)
#11853 := (+ #5352 #13325)
#14129 := (+ #2038 #11853)
#14155 := (>= #14129 0::Int)
#8205 := (iff #14155 #14134)
#14211 := [rewrite]: #8205
#14206 := (iff #12308 #14155)
#12309 := (= #14205 #14129)
#12299 := [rewrite]: #12309
#14118 := [monotonicity #12299]: #14206
#14132 := [trans #14118 #14211]: #14226
#11847 := [monotonicity #14132]: #12007
#17095 := [monotonicity #11847]: #18182
#18163 := [trans #17095 #18166]: #18167
#18175 := [quant-inst #2034 #5342]: #18152
#18168 := [mp #18175 #18163]: #18156
#18379 := [unit-resolution #18168 #18542]: #11985
#18376 := [unit-resolution #18379 #18370 #18378]: #14134
#15298 := (= #14210 0::Int)
#15302 := (not #15298)
#15303 := (or #15217 #13323 #15302)
#3531 := (or #3896 #3888)
#3535 := [def-axiom]: #3531
#18380 := [unit-resolution #3535 #18188]: #3888
#18219 := (or #3893 #15217 #13323 #15302)
#15198 := (+ #2038 #5352)
#15203 := (+ #13325 #15198)
#15204 := (= #15203 0::Int)
#15256 := (not #15204)
#15257 := (or #15115 #13323 #15256)
#18220 := (or #3893 #15257)
#18239 := (iff #18220 #18219)
#18247 := (or #3893 #15303)
#18237 := (iff #18247 #18219)
#18238 := [rewrite]: #18237
#18253 := (iff #18220 #18247)
#15292 := (iff #15257 #15303)
#15304 := (iff #15256 #15302)
#15275 := (iff #15204 #15298)
#15285 := (= #14129 0::Int)
#15299 := (iff #15285 #15298)
#15297 := [rewrite]: #15299
#15279 := (iff #15204 #15285)
#15264 := (= #15203 #14129)
#15254 := [rewrite]: #15264
#15284 := [monotonicity #15254]: #15279
#15300 := [trans #15284 #15297]: #15275
#15289 := [monotonicity #15300]: #15304
#15301 := [monotonicity #15202 #15289]: #15292
#18254 := [monotonicity #15301]: #18253
#18236 := [trans #18254 #18238]: #18239
#18252 := [quant-inst #5342]: #18220
#18242 := [mp #18252 #18236]: #18219
#18381 := [unit-resolution #18242 #18380]: #15303
#18382 := [unit-resolution #18381 #18370 #19109]: #15302
#18393 := (not #18243)
#18392 := (not #14134)
#18388 := (or #15298 #18392 #18393)
#18394 := [th-lemma arith triangle-eq]: #18388
#18396 := [unit-resolution #18394 #18382 #18376 #18367]: false
#18397 := [lemma #18396]: #4541
#16386 := [mp #18397 #16391]: #9410
#9307 := (not #9956)
#9346 := (or #9307 #9944 #9685)
#9347 := [def-axiom]: #9346
#16392 := [unit-resolution #9347 #16386 #16374]: #9685
#9688 := (or #9951 #9687)
#9684 := [def-axiom]: #9688
#16383 := [unit-resolution #9684 #16392]: #9687
#16395 := [unit-resolution #16383 #16394]: false
#16405 := [lemma #16395]: #15368
#16379 := [hypothesis]: #15340
#15365 := (or #7600 #15327 #15358)
#15362 := (or #15327 #15358)
#15360 := (or #7600 #15362)
#15351 := (iff #15360 #15365)
#15352 := [rewrite]: #15351
#15364 := [quant-inst #181 #2034]: #15360
#15353 := [mp #15364 #15352]: #15365
#16275 := [unit-resolution #15353 #3612 #16379 #16405]: false
#16404 := [lemma #16275]: #15358
#16322 := [hypothesis]: #12121
#16307 := (or #15340 #15379 #15402)
#15400 := (or #15340 #15379 #15402 #10624)
#15403 := [th-lemma arith assign-bounds -1 -1 1]: #15400
#16283 := [unit-resolution #15403 #9459]: #16307
#16319 := [unit-resolution #16283 #16322 #16404]: #15402
#5241 := (+ #4079 #5123)
#5242 := (+ #2037 #5241)
#5243 := (= #5242 0::Int)
#12167 := (>= #5242 0::Int)
#16360 := (or #12167 #15379)
#15382 := (or #12167 #10624 #15379)
#14315 := [th-lemma arith assign-bounds -1 1]: #15382
#16376 := [unit-resolution #14315 #9459]: #16360
#16377 := [unit-resolution #16376 #16322]: #12167
#15390 := (not #12167)
#16258 := (or #5243 #15390)
#12074 := (<= #5242 0::Int)
#4339 := (+ #110 #1146)
#7776 := (<= #4339 0::Int)
#4340 := (>= #4339 0::Int)
#9693 := (not #4340)
#4164 := (?v1!7 f28)
#4165 := (f19 f20 #4164)
#4166 := (* -1::Int #4165)
#4167 := (+ #185 #4166)
#4168 := (<= #4167 0::Int)
#7320 := (not #4168)
#4172 := (f6 f7 #4164)
#4173 := (f5 #4172 f28)
#4174 := (f4 #4173)
#4175 := (* -1::Int #4174)
#4176 := (+ #4166 #4175)
#4177 := (+ #185 #4176)
#4178 := (= #4177 0::Int)
#4179 := (not #4178)
#4169 := (f11 f21 #4164)
#4170 := (= #4169 f1)
#4171 := (not #4170)
#4180 := (or #4168 #4171 #4179)
#4181 := (not #4180)
#4335 := (f11 f21 f16)
#4336 := (= #4335 f1)
#13038 := (or #3896 #2040 #4336)
#12906 := [hypothesis]: #3899
#12800 := [unit-resolution #3535 #12906]: #3888
#7302 := (not #4336)
#15705 := [hypothesis]: #7302
#4341 := (or #4336 #4340)
#7485 := (or #3825 #4336 #4340)
#7486 := (or #3825 #4341)
#7488 := (iff #7486 #7485)
#7489 := [rewrite]: #7488
#7487 := [quant-inst #65]: #7486
#7490 := [mp #7487 #7489]: #7485
#15712 := [unit-resolution #7490 #9789]: #4341
#15713 := [unit-resolution #15712 #15705]: #4340
#15716 := (or #9693 #4168)
#7756 := (>= #4165 0::Int)
#7707 := (not #7756)
#7708 := [hypothesis]: #7707
#7822 := (or #3722 #7756)
#7824 := [quant-inst #4164]: #7822
#7859 := [unit-resolution #7824 #7614 #7708]: false
#7860 := [lemma #7859]: #7756
#15719 := (or #9693 #7707 #4168)
#7972 := (not #4504)
#15717 := (or #9693 #7972 #7707 #4168)
#15718 := [th-lemma arith assign-bounds -1 1 1]: #15717
#15721 := [unit-resolution #15718 #7623]: #15719
#15722 := [unit-resolution #15721 #7860]: #15716
#15723 := [unit-resolution #15722 #15713]: #4168
#7326 := (or #4180 #7320)
#7330 := [def-axiom]: #7326
#15728 := [unit-resolution #7330 #15723]: #4180
#7978 := (or #4163 #4181)
#3458 := (or #3968 #1323)
#3461 := [def-axiom]: #3458
#7977 := [unit-resolution #3461 #7802]: #1323
#7294 := (or #3747 #4163 #1322 #4181)
#4182 := (or #4163 #1322 #4181)
#7297 := (or #3747 #4182)
#7321 := (iff #7297 #7294)
#7323 := [rewrite]: #7321
#7298 := [quant-inst #181]: #7297
#7324 := [mp #7298 #7323]: #7294
#7979 := [unit-resolution #7324 #7427 #7977]: #7978
#15748 := [unit-resolution #7979 #15728]: #4163
#11585 := [unit-resolution #3440 #12906]: #2036
#15405 := (or #15374 #2035 #7583 #3893)
#15369 := (iff #2036 #15368)
#15350 := (iff #2035 #15327)
#15367 := (iff #15327 #2035)
#12076 := (= f16 ?v0!20)
#15366 := (iff #12076 #2035)
#15354 := [commutativity]: #15366
#15357 := (iff #15327 #12076)
#15317 := [monotonicity #7835]: #15357
#15318 := [trans #15317 #15354]: #15367
#15336 := [symm #15318]: #15350
#15370 := [monotonicity #15336]: #15369
#15363 := [hypothesis]: #2036
#15373 := [mp #15363 #15370]: #15368
#15335 := [hypothesis]: #5182
#15375 := (or #15374 #12121)
#15376 := [th-lemma arith triangle-eq]: #15375
#15378 := [unit-resolution #15376 #15335]: #12121
#15381 := [unit-resolution #14315 #15378 #9459]: #12167
#12123 := (>= #5179 0::Int)
#14322 := (or #15374 #12123)
#11027 := [th-lemma arith triangle-eq]: #14322
#15349 := [unit-resolution #11027 #15335]: #12123
#15265 := (not #12123)
#14563 := (or #12074 #14493 #15265)
#15266 := [th-lemma arith assign-bounds -1 1]: #14563
#15286 := [unit-resolution #15266 #15349 #10752]: #12074
#14562 := (not #12074)
#15295 := (or #5243 #14562 #15390)
#15391 := [th-lemma arith triangle-eq]: #15295
#15392 := [unit-resolution #15391 #15286 #15381]: #5243
#5248 := (not #5243)
#15394 := (or #5229 #5248)
#4429 := (f11 f29 f28)
#4430 := (= #4429 f1)
#4055 := (f11 #193 f28)
#4056 := (= #4055 f1)
#43 := (:var 0 S1)
#40 := (:var 2 S7)
#41 := (f14 f15 #40)
#42 := (f13 #41 #10)
#44 := (f12 #42 #43)
#3633 := (pattern #44)
#47 := (= #43 f1)
#45 := (f11 #44 #10)
#46 := (= #45 f1)
#48 := (iff #46 #47)
#3634 := (forall (vars (?v0 S7) (?v1 S2) (?v2 S1)) (:pat #3633) #48)
#49 := (forall (vars (?v0 S7) (?v1 S2) (?v2 S1)) #48)
#3637 := (iff #49 #3634)
#3635 := (iff #48 #48)
#3636 := [refl]: #3635
#3638 := [quant-intro #3636]: #3637
#1494 := (~ #49 #49)
#1521 := (~ #48 #48)
#1522 := [refl]: #1521
#1495 := [nnf-pos #1522]: #1494
#341 := [asserted]: #49
#1523 := [mp~ #341 #1495]: #49
#3639 := [mp #1523 #3638]: #3634
#7192 := (not #3634)
#7205 := (or #7192 #4056)
#4058 := (iff #4056 #4057)
#7206 := (or #7192 #4058)
#7227 := (iff #7206 #7205)
#7229 := (iff #7205 #7205)
#7200 := [rewrite]: #7229
#4066 := (iff #4058 #4056)
#4061 := (iff #4056 true)
#4064 := (iff #4061 #4056)
#4065 := [rewrite]: #4064
#4062 := (iff #4058 #4061)
#4063 := [monotonicity #4060]: #4062
#4067 := [trans #4063 #4065]: #4066
#7228 := [monotonicity #4067]: #7227
#7201 := [trans #7228 #7200]: #7227
#7226 := [quant-inst #115 #181 #3]: #7206
#7199 := [mp #7226 #7201]: #7205
#15296 := [unit-resolution #7199 #3639]: #4056
#14014 := (= #4429 #4055)
#15393 := [monotonicity #8144]: #14014
#15395 := [trans #15393 #15296]: #4430
#15396 := [hypothesis]: #3888
#4431 := (not #4430)
#12122 := (or #3893 #5229 #4431 #5248)
#5219 := (+ #4078 #5178)
#5220 := (= #5219 0::Int)
#5221 := (not #5220)
#5209 := (+ #4078 #2038)
#5210 := (>= #5209 0::Int)
#5222 := (or #5210 #4431 #5221)
#12125 := (or #3893 #5222)
#12149 := (iff #12125 #12122)
#5251 := (or #5229 #4431 #5248)
#12146 := (or #3893 #5251)
#12083 := (iff #12146 #12122)
#12143 := [rewrite]: #12083
#12131 := (iff #12125 #12146)
#5252 := (iff #5222 #5251)
#5249 := (iff #5221 #5248)
#5246 := (iff #5220 #5243)
#5234 := (+ #4078 #5122)
#5235 := (+ #2038 #5234)
#5238 := (= #5235 0::Int)
#5244 := (iff #5238 #5243)
#5245 := [rewrite]: #5244
#5239 := (iff #5220 #5238)
#5236 := (= #5219 #5235)
#5237 := [rewrite]: #5236
#5240 := [monotonicity #5237]: #5239
#5247 := [trans #5240 #5245]: #5246
#5250 := [monotonicity #5247]: #5249
#5232 := (iff #5210 #5229)
#5223 := (+ #2038 #4078)
#5226 := (>= #5223 0::Int)
#5230 := (iff #5226 #5229)
#5231 := [rewrite]: #5230
#5227 := (iff #5210 #5226)
#5224 := (= #5209 #5223)
#5225 := [rewrite]: #5224
#5228 := [monotonicity #5225]: #5227
#5233 := [trans #5228 #5231]: #5232
#5253 := [monotonicity #5233 #5250]: #5252
#12082 := [monotonicity #5253]: #12131
#12147 := [trans #12082 #12143]: #12149
#12075 := [quant-inst #181]: #12125
#12124 := [mp #12075 #12147]: #12122
#15399 := [unit-resolution #12124 #15396 #15395]: #15394
#15401 := [unit-resolution #15399 #15392]: #5229
#15397 := [unit-resolution #15403 #15378 #15401 #9459]: #15340
#15398 := [unit-resolution #15353 #3612]: #15362
#15404 := [unit-resolution #15398 #15397 #15373]: false
#15406 := [lemma #15404]: #15405
#11721 := [unit-resolution #15406 #11585 #15748 #12800]: #15374
#12105 := (not #5125)
#5149 := (not #5146)
#15784 := (or #15969 #4336 #2040 #2035)
#15708 := [unit-resolution #15971 #15965 #13634]: #15968
#15709 := [unit-resolution #12292 #7427 #15363]: #15703
#15710 := [unit-resolution #15709 #15708]: #5359
#12264 := (or #5358 #5348)
#12306 := [def-axiom]: #12264
#15453 := [unit-resolution #12306 #15710]: #5348
#15775 := (= #4335 #5347)
#15780 := (= #182 #5347)
#15777 := (= f28 #5342)
#15752 := (= f16 #5342)
#13856 := (= #5342 f16)
#13857 := (?v1!7 #5342)
#13952 := (f6 f7 #13857)
#13906 := (f5 #13952 #5342)
#13881 := (f4 #13906)
#13913 := (* -1::Int #13881)
#13835 := (f19 f20 #13857)
#13871 := (* -1::Int #13835)
#13806 := (+ #13871 #13913)
#11518 := (+ #5343 #13806)
#11879 := (= #11518 0::Int)
#13861 := (not #11879)
#13937 := (f11 f21 #13857)
#13943 := (= #13937 f1)
#13938 := (not #13943)
#13870 := (+ #5343 #13871)
#13936 := (<= #13870 0::Int)
#11576 := (or #13936 #13938 #13861)
#12649 := (+ #185 #5344)
#12802 := (>= #12649 0::Int)
#11633 := (or #3731 #183 #5349 #12802)
#11028 := (or #183 #5349 #12802)
#12259 := (or #3731 #11028)
#11754 := (iff #12259 #11633)
#12879 := [rewrite]: #11754
#12287 := [quant-inst #5342 #181]: #12259
#12883 := [mp #12287 #12879]: #11633
#15747 := [unit-resolution #12883 #8156 #8155 #15453]: #12802
#17243 := (not #12802)
#17244 := (or #13936 #9693 #17243)
#17239 := [hypothesis]: #12802
#14038 := (not #13936)
#17240 := [hypothesis]: #14038
#17043 := (>= #13835 0::Int)
#17063 := (or #3722 #17043)
#17064 := [quant-inst #13857]: #17063
#17241 := [unit-resolution #17064 #7614]: #17043
#9714 := [hypothesis]: #4340
#17242 := [th-lemma arith farkas -1 1 1 1 1 #7623 #9714 #17241 #17240 #17239]: false
#17245 := [lemma #17242]: #17244
#15749 := [unit-resolution #17245 #15747 #15713]: #13936
#14010 := (or #11576 #14038)
#14095 := [def-axiom]: #14010
#15750 := [unit-resolution #14095 #15749]: #11576
#13847 := (+ f3 #5344)
#13841 := (<= #13847 0::Int)
#16579 := (not #13841)
#15746 := [unit-resolution #12297 #15710]: #12311
#16524 := (or #16579 #2040 #15969 #5346)
#16576 := [hypothesis]: #13841
#16577 := [hypothesis]: #12311
#16578 := [th-lemma arith farkas 1 1 1 1 #13634 #15965 #16577 #16576]: false
#16580 := [lemma #16578]: #16524
#15711 := [unit-resolution #16580 #15965 #13634 #15746]: #16579
#13912 := (not #11576)
#13915 := (or #13856 #13841 #13912)
#14033 := (or #3747 #13856 #13841 #13912)
#14036 := (or #3747 #13915)
#14009 := (iff #14036 #14033)
#14008 := [rewrite]: #14009
#14011 := [quant-inst #5342]: #14036
#14037 := [mp #14011 #14008]: #14033
#15720 := [unit-resolution #14037 #7427]: #13915
#15751 := [unit-resolution #15720 #15711 #15750]: #13856
#15753 := [symm #15751]: #15752
#15778 := [trans #15748 #15753]: #15777
#15754 := [monotonicity #15778]: #15780
#15776 := (= #4335 #182)
#15727 := [symm #15748]: #7836
#15779 := [monotonicity #15727]: #15776
#15782 := [trans #15779 #15754]: #15775
#15783 := [trans #15782 #15453]: #4336
#15781 := [unit-resolution #15705 #15783]: false
#15786 := [lemma #15781]: #15784
#12801 := [unit-resolution #15786 #11585 #13634 #15705]: #15969
#12564 := [unit-resolution #12636 #12801]: #11867
#5152 := (or #5149 #5087)
#11970 := (or #3843 #5149 #5087)
#5126 := (+ #1146 #5123)
#5127 := (+ #5080 #5126)
#5128 := (<= #5127 0::Int)
#5129 := (or #5125 #5128)
#5130 := (not #5129)
#5131 := (or #5130 #5087)
#12023 := (or #3843 #5131)
#12067 := (iff #12023 #11970)
#12068 := (or #3843 #5152)
#12042 := (iff #12068 #11970)
#12107 := [rewrite]: #12042
#12058 := (iff #12023 #12068)
#5153 := (iff #5131 #5152)
#5150 := (iff #5130 #5149)
#5147 := (iff #5129 #5146)
#5144 := (iff #5128 #5141)
#5132 := (+ #5080 #5123)
#5133 := (+ #1146 #5132)
#5136 := (<= #5133 0::Int)
#5142 := (iff #5136 #5141)
#5143 := [rewrite]: #5142
#5137 := (iff #5128 #5136)
#5134 := (= #5127 #5133)
#5135 := [rewrite]: #5134
#5138 := [monotonicity #5135]: #5137
#5145 := [trans #5138 #5143]: #5144
#5148 := [monotonicity #5145]: #5147
#5151 := [monotonicity #5148]: #5150
#5154 := [monotonicity #5151]: #5153
#12062 := [monotonicity #5154]: #12058
#12070 := [trans #12062 #12107]: #12067
#12017 := [quant-inst #2034]: #12023
#12084 := [mp #12017 #12070]: #11970
#9728 := [unit-resolution #12084 #7803]: #5152
#12860 := [unit-resolution #9728 #12564]: #5149
#12072 := (or #5146 #12105)
#12071 := [def-axiom]: #12072
#13044 := [unit-resolution #12071 #12860]: #12105
#12081 := (not #5141)
#12073 := (or #5146 #12081)
#12118 := [def-axiom]: #12073
#13025 := [unit-resolution #12118 #12860]: #12081
#5185 := (or #5125 #5141 #5182)
#12077 := (or #3835 #5125 #5141 #5182)
#5174 := (+ #5122 #2038)
#5175 := (+ #185 #5174)
#5176 := (= #5175 0::Int)
#5177 := (or #5125 #5128 #5176)
#12079 := (or #3835 #5177)
#12130 := (iff #12079 #12077)
#12113 := (or #3835 #5185)
#12114 := (iff #12113 #12077)
#12129 := [rewrite]: #12114
#12117 := (iff #12079 #12113)
#5186 := (iff #5177 #5185)
#5183 := (iff #5176 #5182)
#5180 := (= #5175 #5179)
#5181 := [rewrite]: #5180
#5184 := [monotonicity #5181]: #5183
#5187 := [monotonicity #5145 #5184]: #5186
#12115 := [monotonicity #5187]: #12117
#12109 := [trans #12115 #12129]: #12130
#12120 := [quant-inst #2034]: #12079
#12128 := [mp #12120 #12109]: #12077
#11095 := [unit-resolution #12128 #7967]: #5185
#13026 := [unit-resolution #11095 #13025 #13044 #11721]: false
#11841 := [lemma #13026]: #13038
#18190 := [unit-resolution #11841 #18188 #18189]: #4336
#9665 := (or #7583 #7302)
#8260 := [hypothesis]: #4336
#9629 := (= #182 #4335)
#9567 := [monotonicity #7835]: #9629
#7820 := [trans #9567 #8260]: #183
#7888 := [unit-resolution #8155 #7820]: false
#7765 := [lemma #7888]: #9665
#18191 := [unit-resolution #7765 #18190]: #7583
#18192 := [unit-resolution #7979 #18191]: #4181
#18193 := [unit-resolution #7330 #18192]: #7320
#16378 := [unit-resolution #15722 #18193]: #9693
#16277 := (or #7776 #4340)
#16270 := [th-lemma arith farkas 1 1]: #16277
#16406 := [unit-resolution #16270 #16378]: #7776
#9345 := (not #7776)
#12779 := (or #12074 #9345 #2040 #3885)
#12732 := [hypothesis]: #14562
#12904 := (or #5125 #12074)
#12870 := [hypothesis]: #3880
#12757 := (or #3885 #4431 #5125 #12074)
#15309 := (+ #5122 #5209)
#15305 := (>= #15309 0::Int)
#15310 := (or #4431 #5125 #15305)
#12733 := (or #3885 #15310)
#12657 := (iff #12733 #12757)
#15344 := (or #4431 #5125 #12074)
#12731 := (or #3885 #15344)
#12778 := (iff #12731 #12757)
#12664 := [rewrite]: #12778
#12760 := (iff #12733 #12731)
#15345 := (iff #15310 #15344)
#15319 := (iff #15305 #12074)
#15287 := (>= #5235 0::Int)
#15315 := (iff #15287 #12074)
#15321 := [rewrite]: #15315
#15312 := (iff #15305 #15287)
#15307 := (= #15309 #5235)
#15311 := [rewrite]: #15307
#15313 := [monotonicity #15311]: #15312
#15342 := [trans #15313 #15321]: #15319
#15343 := [monotonicity #15342]: #15345
#12770 := [monotonicity #15343]: #12760
#12730 := [trans #12770 #12664]: #12657
#12432 := [quant-inst #2034 #181]: #12733
#12772 := [mp #12432 #12730]: #12757
#12909 := [unit-resolution #12772 #12870 #15395]: #12904
#12907 := [unit-resolution #12909 #12732]: #5125
#12775 := (or #12167 #12074)
#12881 := [th-lemma arith farkas 1 1]: #12775
#12865 := [unit-resolution #12881 #12732]: #12167
#9736 := [hypothesis]: #7776
#3233 := (>= #110 0::Int)
#4506 := (or #3722 #3233)
#4549 := [quant-inst #65]: #4506
#9790 := [unit-resolution #4549 #7614]: #3233
#12861 := [th-lemma arith farkas 1 1 1 1 -1 1 #10752 #9790 #9736 #12865 #12907 #13634]: false
#12858 := [lemma #12861]: #12779
#16384 := [unit-resolution #12858 #16406 #18189 #18542]: #12074
#16235 := [unit-resolution #15391 #16384]: #16258
#16285 := [unit-resolution #16235 #16377]: #5243
#16416 := [unit-resolution #12124 #18380]: #5251
#16417 := [unit-resolution #16416 #15395]: #15394
#16408 := [unit-resolution #16417 #16285 #16319]: false
#16407 := [lemma #16408]: #15379
#16321 := [unit-resolution #15376 #16407]: #15374
#16309 := [hypothesis]: #5149
#16410 := [unit-resolution #12071 #16309]: #12105
#16431 := [unit-resolution #12118 #16309]: #12081
#16434 := [unit-resolution #11095 #16431 #16410 #16321]: false
#16432 := [lemma #16434]: #5146
#16614 := [unit-resolution #9728 #16432]: #5087
#16615 := [unit-resolution #12636 #16614]: #12022
#16603 := [unit-resolution #19099 #16615]: #15968
#16597 := [unit-resolution #19102 #16603]: #5359
#16549 := [unit-resolution #15554 #16597]: #5356
#16573 := [unit-resolution #18361 #16549]: #15530
#16590 := [unit-resolution #18365 #19087 #16615 #16573]: #18243
#16554 := [unit-resolution #18373 #18368 #16573 #16615]: #18369
#16552 := (f11 #193 #5342)
#16553 := (= #16552 f1)
#16559 := (= #5342 f28)
#16561 := (or #16559 #5348)
#16545 := (iff #16553 #16561)
#16568 := (or #7518 #16545)
#16522 := (if #16559 #4057 #5348)
#16560 := (iff #16553 #16522)
#16569 := (or #7518 #16560)
#16571 := (iff #16569 #16568)
#16563 := (iff #16568 #16568)
#16588 := [rewrite]: #16563
#16567 := (iff #16560 #16545)
#16564 := (iff #16522 #16561)
#16557 := (if #16559 true #5348)
#16565 := (iff #16557 #16561)
#16547 := [rewrite]: #16565
#16562 := (iff #16522 #16557)
#16548 := [monotonicity #4060]: #16562
#16566 := [trans #16548 #16547]: #16564
#16546 := [monotonicity #16566]: #16567
#16574 := [monotonicity #16546]: #16571
#16586 := [trans #16574 #16588]: #16571
#16572 := [quant-inst #115 #181 #3 #5342]: #16569
#16589 := [mp #16572 #16586]: #16568
#16611 := [unit-resolution #16589 #3646]: #16545
#16373 := (not #16545)
#16635 := (or #16373 #16553)
#16598 := [unit-resolution #12306 #16597]: #5348
#15874 := (or #16561 #5349)
#16585 := [def-axiom]: #15874
#16596 := [unit-resolution #16585 #16598]: #16561
#15886 := (not #16561)
#16515 := (or #16373 #16553 #15886)
#16581 := [def-axiom]: #16515
#16599 := [unit-resolution #16581 #16596]: #16635
#16620 := [unit-resolution #16599 #16611]: #16553
#16621 := (= #13322 #16552)
#16619 := [monotonicity #8144]: #16621
#16595 := [trans #16619 #16620]: #13321
#16610 := [hypothesis]: #13323
#16622 := [unit-resolution #16610 #16595]: false
#16600 := [lemma #16622]: #13321
#16372 := [unit-resolution #18379 #16600 #16554]: #14134
#16550 := [unit-resolution #12297 #16597]: #12311
#16043 := [unit-resolution #19108 #19087 #16615 #16550]: #19105
#16044 := [unit-resolution #18381 #16600 #16043]: #15302
[unit-resolution #18394 #16044 #16372 #16590]: false
unsat