src/HOL/Boogie/Examples/Boogie_Max.certs

more exception handling -- make print functions total;

43f8affa0232e904defc8acf7ee4c00d186b27a1 2078 0
#2 := false
#7 := 0::Int
decl ?v0!3 :: Int
#1093 := ?v0!3
#616 := -1::Int
#1238 := (* -1::Int ?v0!3)
decl f8 :: Int
#31 := f8
#2314 := (+ f8 #1238)
#2315 := (<= #2314 0::Int)
#2420 := (not #2315)
#2347 := (>= #2314 0::Int)
decl f16 :: Int
#79 := f16
#725 := (* -1::Int f16)
#757 := (+ f8 #725)
#1758 := (>= #757 -1::Int)
#756 := (= #757 -1::Int)
decl f15 :: Int
#75 := f15
decl f5 :: (-> S2 Int Int)
decl f14 :: Int
#73 := f14
decl f6 :: S2
#11 := f6
#90 := (f5 f6 f14)
#91 := (= #90 f15)
#20 := (:var 0 Int)
#24 := (f5 f6 #20)
#2076 := (pattern #24)
#736 := (* -1::Int f15)
#737 := (+ #24 #736)
#738 := (<= #737 0::Int)
#726 := (+ #20 #725)
#724 := (>= #726 0::Int)
#605 := (>= #20 0::Int)
#1341 := (not #605)
#1515 := (or #1341 #724 #738)
#2110 := (forall (vars (?v0 Int)) (:pat #2076) #1515)
#2115 := (not #2110)
#2118 := (or #2115 #91)
#2121 := (not #2118)
#1100 := (f5 f6 ?v0!3)
#1260 := (* -1::Int #1100)
#1261 := (+ f15 #1260)
#1262 := (>= #1261 0::Int)
#1239 := (+ f16 #1238)
#1240 := (<= #1239 0::Int)
#1094 := (>= ?v0!3 0::Int)
#1478 := (not #1094)
#1493 := (or #1478 #1240 #1262)
#1498 := (not #1493)
#2124 := (or #1498 #2121)
#2127 := (not #2124)
#82 := 2::Int
#716 := (>= f16 2::Int)
#1540 := (not #716)
#713 := (>= f14 0::Int)
#1539 := (not #713)
#760 := (not #756)
#15 := 1::Int
#635 := (>= f8 1::Int)
#769 := (not #635)
decl f9 :: Int
#36 := f9
#108 := (= f15 f9)
#395 := (not #108)
decl f7 :: Int
#29 := f7
#107 := (= f14 f7)
#404 := (not #107)
#68 := (f5 f6 f8)
#774 := (* -1::Int #68)
#775 := (+ f9 #774)
#773 := (>= #775 0::Int)
#772 := (not #773)
#632 := (>= f7 0::Int)
#1470 := (not #632)
#2136 := (or #1470 #772 #404 #395 #769 #760 #1539 #1540 #2127)
#2139 := (not #2136)
decl f13 :: Int
#70 := f13
#76 := (= f15 f13)
#335 := (not #76)
#74 := (= f14 f8)
#344 := (not #74)
#71 := (= f13 #68)
#362 := (not #71)
#2130 := (or #1470 #773 #362 #344 #335 #769 #760 #1539 #1540 #2127)
#2133 := (not #2130)
#2142 := (or #2133 #2139)
#2145 := (not #2142)
#681 := (* -1::Int f8)
decl f3 :: Int
#8 := f3
#682 := (+ f3 #681)
#683 := (<= #682 0::Int)
#2148 := (or #1470 #769 #683 #2145)
#2151 := (not #2148)
decl ?v0!2 :: Int
#1038 := ?v0!2
#1046 := (f5 f6 ?v0!2)
#1191 := (* -1::Int #1046)
decl f11 :: Int
#45 := f11
#1192 := (+ f11 #1191)
#1193 := (>= #1192 0::Int)
#1040 := (* -1::Int ?v0!2)
#1041 := (+ f3 #1040)
#1042 := (<= #1041 0::Int)
#1039 := (>= ?v0!2 0::Int)
#1431 := (not #1039)
decl ?v0!1 :: Int
#1020 := ?v0!1
#1028 := (f5 f6 ?v0!1)
#1029 := (= #1028 f11)
#1022 := (* -1::Int ?v0!1)
#1023 := (+ f3 #1022)
#1024 := (<= #1023 0::Int)
#1021 := (>= ?v0!1 0::Int)
#1411 := (not #1021)
#1426 := (or #1411 #1024 #1029)
#1457 := (not #1426)
#1458 := (or #1457 #1431 #1042 #1193)
#1459 := (not #1458)
#51 := (= #24 f11)
#643 := (* -1::Int #20)
#644 := (+ f3 #643)
#645 := (<= #644 0::Int)
#1400 := (or #1341 #645 #51)
#1405 := (not #1400)
#2093 := (forall (vars (?v0 Int)) (:pat #2076) #1405)
#2098 := (or #2093 #1459)
#2101 := (not #2098)
decl f12 :: Int
#47 := f12
#48 := (= f12 f8)
#212 := (not #48)
#46 := (= f11 f9)
#221 := (not #46)
decl f10 :: Int
#43 := f10
#44 := (= f10 f7)
#230 := (not #44)
#686 := (not #683)
#2104 := (or #1470 #769 #686 #230 #221 #212 #2101)
#2107 := (not #2104)
#2154 := (or #2107 #2151)
#2157 := (not #2154)
#40 := (f5 f6 f7)
#41 := (= #40 f9)
#491 := (not #41)
#881 := (* -1::Int f9)
#882 := (+ #24 #881)
#883 := (<= #882 0::Int)
#871 := (+ #20 #681)
#870 := (>= #871 0::Int)
#1378 := (or #1341 #870 #883)
#2085 := (forall (vars (?v0 Int)) (:pat #2076) #1378)
#2090 := (not #2085)
decl f4 :: Int
#10 := f4
#12 := (f5 f6 0::Int)
#28 := (= #12 f4)
#524 := (not #28)
#2160 := (or #524 #1470 #769 #2090 #491 #2157)
#2163 := (not #2160)
#2166 := (or #524 #2163)
#2169 := (not #2166)
#619 := (* -1::Int #24)
#620 := (+ f4 #619)
#618 := (>= #620 0::Int)
#608 := (>= #20 1::Int)
#1356 := (or #1341 #608 #618)
#2077 := (forall (vars (?v0 Int)) (:pat #2076) #1356)
#2082 := (not #2077)
#2172 := (or #2082 #2169)
#2175 := (not #2172)
decl ?v0!0 :: Int
#968 := ?v0!0
#962 := (f5 f6 ?v0!0)
#963 := (* -1::Int #962)
#960 := (+ f4 #963)
#961 := (>= #960 0::Int)
#970 := (>= ?v0!0 1::Int)
#969 := (>= ?v0!0 0::Int)
#1033 := (not #969)
#1333 := (or #1033 #970 #961)
#1927 := (= f4 #962)
#1853 := (= #12 #962)
#1893 := (= #962 #12)
#1903 := (= ?v0!0 0::Int)
#971 := (not #970)
#1338 := (not #1333)
#1926 := [hypothesis]: #1338
#1663 := (or #1333 #971)
#1748 := [def-axiom]: #1663
#1928 := [unit-resolution #1748 #1926]: #971
#1662 := (or #1333 #969)
#1747 := [def-axiom]: #1662
#1896 := [unit-resolution #1747 #1926]: #969
#1862 := [th-lemma arith eq-propagate 0 0 #1896 #1928]: #1903
#1895 := [monotonicity #1862]: #1893
#1854 := [symm #1895]: #1853
#13 := (= f4 #12)
#727 := (not #724)
#730 := (and #605 #727)
#733 := (not #730)
#741 := (or #733 #738)
#744 := (forall (vars (?v0 Int)) #741)
#747 := (not #744)
#750 := (or #747 #91)
#753 := (and #744 #750)
#718 := (and #713 #716)
#721 := (not #718)
#763 := (and #713 #635)
#766 := (not #763)
#637 := (and #632 #635)
#640 := (not #637)
#836 := (or #640 #772 #404 #395 #766 #760 #721 #753)
#812 := (or #640 #773 #362 #769 #344 #335 #766 #760 #721 #753)
#841 := (and #812 #836)
#862 := (or #640 #683 #841)
#664 := (* -1::Int f11)
#665 := (+ #24 #664)
#666 := (<= #665 0::Int)
#646 := (not #645)
#649 := (and #605 #646)
#652 := (not #649)
#669 := (or #652 #666)
#672 := (forall (vars (?v0 Int)) #669)
#655 := (or #652 #51)
#658 := (exists (vars (?v0 Int)) #655)
#661 := (not #658)
#675 := (or #661 #672)
#678 := (and #658 #675)
#707 := (or #640 #686 #230 #221 #212 #678)
#867 := (and #707 #862)
#872 := (not #870)
#875 := (and #605 #872)
#878 := (not #875)
#886 := (or #878 #883)
#889 := (forall (vars (?v0 Int)) #886)
#892 := (not #889)
#910 := (or #524 #640 #892 #491 #867)
#915 := (and #28 #910)
#606 := (not #608)
#610 := (and #605 #606)
#613 := (not #610)
#622 := (or #613 #618)
#625 := (forall (vars (?v0 Int)) #622)
#628 := (not #625)
#918 := (or #628 #915)
#921 := (and #625 #918)
#557 := (not #13)
#924 := (<= f3 0::Int)
#944 := (or #924 #557 #921)
#949 := (not #944)
#1 := true
#92 := (and #91 true)
#87 := (<= #24 f15)
#85 := (< #20 f16)
#21 := (<= 0::Int #20)
#86 := (and #21 #85)
#88 := (implies #86 #87)
#89 := (forall (vars (?v0 Int)) #88)
#93 := (implies #89 #92)
#94 := (and #89 #93)
#83 := (<= 2::Int f16)
#77 := (<= 0::Int f14)
#84 := (and #77 #83)
#95 := (implies #84 #94)
#80 := (+ f8 1::Int)
#81 := (= f16 #80)
#96 := (implies #81 #95)
#32 := (<= 1::Int f8)
#78 := (and #77 #32)
#97 := (implies #78 #96)
#98 := (implies true #97)
#109 := (implies #108 #98)
#110 := (implies #107 #109)
#30 := (<= 0::Int f7)
#33 := (and #30 #32)
#111 := (implies #33 #110)
#106 := (<= #68 f9)
#112 := (implies #106 #111)
#113 := (implies #33 #112)
#114 := (implies true #113)
#99 := (implies #76 #98)
#100 := (implies #74 #99)
#72 := (and #32 #32)
#101 := (implies #72 #100)
#102 := (implies #71 #101)
#69 := (< f9 #68)
#103 := (implies #69 #102)
#104 := (implies #33 #103)
#105 := (implies true #104)
#115 := (and #105 #114)
#116 := (implies #33 #115)
#67 := (< f8 f3)
#117 := (implies #67 #116)
#118 := (implies #33 #117)
#119 := (implies true #118)
#54 := (<= #24 f11)
#49 := (< #20 f3)
#50 := (and #21 #49)
#55 := (implies #50 #54)
#56 := (forall (vars (?v0 Int)) #55)
#57 := (and #56 true)
#52 := (implies #50 #51)
#53 := (exists (vars (?v0 Int)) #52)
#58 := (implies #53 #57)
#59 := (and #53 #58)
#60 := (implies #48 #59)
#61 := (implies #46 #60)
#62 := (implies #44 #61)
#63 := (implies #33 #62)
#42 := (<= f3 f8)
#64 := (implies #42 #63)
#65 := (implies #33 #64)
#66 := (implies true #65)
#120 := (and #66 #119)
#121 := (implies #33 #120)
#122 := (implies #41 #121)
#37 := (<= #24 f9)
#34 := (< #20 f8)
#35 := (and #21 #34)
#38 := (implies #35 #37)
#39 := (forall (vars (?v0 Int)) #38)
#123 := (implies #39 #122)
#124 := (implies #33 #123)
#125 := (implies true #124)
#126 := (implies #28 #125)
#127 := (and #28 #126)
#25 := (<= #24 f4)
#22 := (< #20 1::Int)
#23 := (and #21 #22)
#26 := (implies #23 #25)
#27 := (forall (vars (?v0 Int)) #26)
#128 := (implies #27 #127)
#129 := (and #27 #128)
#16 := (<= 1::Int 1::Int)
#17 := (and #16 #16)
#14 := (<= 0::Int 0::Int)
#18 := (and #14 #17)
#19 := (and #14 #18)
#130 := (implies #19 #129)
#131 := (implies #13 #130)
#9 := (< 0::Int f3)
#132 := (implies #9 #131)
#133 := (implies true #132)
#134 := (not #133)
#952 := (iff #134 #949)
#277 := (not #86)
#278 := (or #277 #87)
#281 := (forall (vars (?v0 Int)) #278)
#289 := (not #281)
#290 := (or #289 #91)
#295 := (and #281 #290)
#301 := (not #84)
#302 := (or #301 #295)
#271 := (+ 1::Int f8)
#274 := (= f16 #271)
#310 := (not #274)
#311 := (or #310 #302)
#319 := (not #78)
#320 := (or #319 #311)
#396 := (or #395 #320)
#405 := (or #404 #396)
#239 := (not #33)
#413 := (or #239 #405)
#421 := (not #106)
#422 := (or #421 #413)
#430 := (or #239 #422)
#336 := (or #335 #320)
#345 := (or #344 #336)
#353 := (not #32)
#354 := (or #353 #345)
#363 := (or #362 #354)
#371 := (not #69)
#372 := (or #371 #363)
#380 := (or #239 #372)
#442 := (and #380 #430)
#448 := (or #239 #442)
#456 := (not #67)
#457 := (or #456 #448)
#465 := (or #239 #457)
#177 := (not #50)
#184 := (or #177 #54)
#187 := (forall (vars (?v0 Int)) #184)
#178 := (or #177 #51)
#181 := (exists (vars (?v0 Int)) #178)
#200 := (not #181)
#201 := (or #200 #187)
#206 := (and #181 #201)
#213 := (or #212 #206)
#222 := (or #221 #213)
#231 := (or #230 #222)
#240 := (or #239 #231)
#248 := (not #42)
#249 := (or #248 #240)
#257 := (or #239 #249)
#477 := (and #257 #465)
#483 := (or #239 #477)
#492 := (or #491 #483)
#170 := (not #35)
#171 := (or #170 #37)
#174 := (forall (vars (?v0 Int)) #171)
#500 := (not #174)
#501 := (or #500 #492)
#509 := (or #239 #501)
#525 := (or #524 #509)
#530 := (and #28 #525)
#163 := (not #23)
#164 := (or #163 #25)
#167 := (forall (vars (?v0 Int)) #164)
#536 := (not #167)
#537 := (or #536 #530)
#542 := (and #167 #537)
#157 := (and #14 #16)
#160 := (and #14 #157)
#548 := (not #160)
#549 := (or #548 #542)
#558 := (or #557 #549)
#566 := (not #9)
#567 := (or #566 #558)
#579 := (not #567)
#950 := (iff #579 #949)
#947 := (iff #567 #944)
#935 := (or false #921)
#938 := (or #557 #935)
#941 := (or #924 #938)
#945 := (iff #941 #944)
#946 := [rewrite]: #945
#942 := (iff #567 #941)
#939 := (iff #558 #938)
#936 := (iff #549 #935)
#922 := (iff #542 #921)
#919 := (iff #537 #918)
#916 := (iff #530 #915)
#913 := (iff #525 #910)
#895 := (or #640 #867)
#898 := (or #491 #895)
#901 := (or #892 #898)
#904 := (or #640 #901)
#907 := (or #524 #904)
#911 := (iff #907 #910)
#912 := [rewrite]: #911
#908 := (iff #525 #907)
#905 := (iff #509 #904)
#902 := (iff #501 #901)
#899 := (iff #492 #898)
#896 := (iff #483 #895)
#868 := (iff #477 #867)
#865 := (iff #465 #862)
#853 := (or #640 #841)
#856 := (or #683 #853)
#859 := (or #640 #856)
#863 := (iff #859 #862)
#864 := [rewrite]: #863
#860 := (iff #465 #859)
#857 := (iff #457 #856)
#854 := (iff #448 #853)
#842 := (iff #442 #841)
#839 := (iff #430 #836)
#785 := (or #721 #753)
#788 := (or #760 #785)
#791 := (or #766 #788)
#821 := (or #395 #791)
#824 := (or #404 #821)
#827 := (or #640 #824)
#830 := (or #772 #827)
#833 := (or #640 #830)
#837 := (iff #833 #836)
#838 := [rewrite]: #837
#834 := (iff #430 #833)
#831 := (iff #422 #830)
#828 := (iff #413 #827)
#825 := (iff #405 #824)
#822 := (iff #396 #821)
#792 := (iff #320 #791)
#789 := (iff #311 #788)
#786 := (iff #302 #785)
#754 := (iff #295 #753)
#751 := (iff #290 #750)
#748 := (iff #289 #747)
#745 := (iff #281 #744)
#742 := (iff #278 #741)
#739 := (iff #87 #738)
#740 := [rewrite]: #739
#734 := (iff #277 #733)
#731 := (iff #86 #730)
#728 := (iff #85 #727)
#729 := [rewrite]: #728
#603 := (iff #21 #605)
#604 := [rewrite]: #603
#732 := [monotonicity #604 #729]: #731
#735 := [monotonicity #732]: #734
#743 := [monotonicity #735 #740]: #742
#746 := [quant-intro #743]: #745
#749 := [monotonicity #746]: #748
#752 := [monotonicity #749]: #751
#755 := [monotonicity #746 #752]: #754
#722 := (iff #301 #721)
#719 := (iff #84 #718)
#715 := (iff #83 #716)
#717 := [rewrite]: #715
#712 := (iff #77 #713)
#714 := [rewrite]: #712
#720 := [monotonicity #714 #717]: #719
#723 := [monotonicity #720]: #722
#787 := [monotonicity #723 #755]: #786
#761 := (iff #310 #760)
#758 := (iff #274 #756)
#759 := [rewrite]: #758
#762 := [monotonicity #759]: #761
#790 := [monotonicity #762 #787]: #789
#767 := (iff #319 #766)
#764 := (iff #78 #763)
#634 := (iff #32 #635)
#636 := [rewrite]: #634
#765 := [monotonicity #714 #636]: #764
#768 := [monotonicity #765]: #767
#793 := [monotonicity #768 #790]: #792
#823 := [monotonicity #793]: #822
#826 := [monotonicity #823]: #825
#641 := (iff #239 #640)
#638 := (iff #33 #637)
#631 := (iff #30 #632)
#633 := [rewrite]: #631
#639 := [monotonicity #633 #636]: #638
#642 := [monotonicity #639]: #641
#829 := [monotonicity #642 #826]: #828
#819 := (iff #421 #772)
#817 := (iff #106 #773)
#818 := [rewrite]: #817
#820 := [monotonicity #818]: #819
#832 := [monotonicity #820 #829]: #831
#835 := [monotonicity #642 #832]: #834
#840 := [trans #835 #838]: #839
#815 := (iff #380 #812)
#794 := (or #335 #791)
#797 := (or #344 #794)
#800 := (or #769 #797)
#803 := (or #362 #800)
#806 := (or #773 #803)
#809 := (or #640 #806)
#813 := (iff #809 #812)
#814 := [rewrite]: #813
#810 := (iff #380 #809)
#807 := (iff #372 #806)
#804 := (iff #363 #803)
#801 := (iff #354 #800)
#798 := (iff #345 #797)
#795 := (iff #336 #794)
#796 := [monotonicity #793]: #795
#799 := [monotonicity #796]: #798
#770 := (iff #353 #769)
#771 := [monotonicity #636]: #770
#802 := [monotonicity #771 #799]: #801
#805 := [monotonicity #802]: #804
#783 := (iff #371 #773)
#778 := (not #772)
#781 := (iff #778 #773)
#782 := [rewrite]: #781
#779 := (iff #371 #778)
#776 := (iff #69 #772)
#777 := [rewrite]: #776
#780 := [monotonicity #777]: #779
#784 := [trans #780 #782]: #783
#808 := [monotonicity #784 #805]: #807
#811 := [monotonicity #642 #808]: #810
#816 := [trans #811 #814]: #815
#843 := [monotonicity #816 #840]: #842
#855 := [monotonicity #642 #843]: #854
#851 := (iff #456 #683)
#846 := (not #686)
#849 := (iff #846 #683)
#850 := [rewrite]: #849
#847 := (iff #456 #846)
#844 := (iff #67 #686)
#845 := [rewrite]: #844
#848 := [monotonicity #845]: #847
#852 := [trans #848 #850]: #851
#858 := [monotonicity #852 #855]: #857
#861 := [monotonicity #642 #858]: #860
#866 := [trans #861 #864]: #865
#710 := (iff #257 #707)
#689 := (or #212 #678)
#692 := (or #221 #689)
#695 := (or #230 #692)
#698 := (or #640 #695)
#701 := (or #686 #698)
#704 := (or #640 #701)
#708 := (iff #704 #707)
#709 := [rewrite]: #708
#705 := (iff #257 #704)
#702 := (iff #249 #701)
#699 := (iff #240 #698)
#696 := (iff #231 #695)
#693 := (iff #222 #692)
#690 := (iff #213 #689)
#679 := (iff #206 #678)
#676 := (iff #201 #675)
#673 := (iff #187 #672)
#670 := (iff #184 #669)
#667 := (iff #54 #666)
#668 := [rewrite]: #667
#653 := (iff #177 #652)
#650 := (iff #50 #649)
#647 := (iff #49 #646)
#648 := [rewrite]: #647
#651 := [monotonicity #604 #648]: #650
#654 := [monotonicity #651]: #653
#671 := [monotonicity #654 #668]: #670
#674 := [quant-intro #671]: #673
#662 := (iff #200 #661)
#659 := (iff #181 #658)
#656 := (iff #178 #655)
#657 := [monotonicity #654]: #656
#660 := [quant-intro #657]: #659
#663 := [monotonicity #660]: #662
#677 := [monotonicity #663 #674]: #676
#680 := [monotonicity #660 #677]: #679
#691 := [monotonicity #680]: #690
#694 := [monotonicity #691]: #693
#697 := [monotonicity #694]: #696
#700 := [monotonicity #642 #697]: #699
#687 := (iff #248 #686)
#684 := (iff #42 #683)
#685 := [rewrite]: #684
#688 := [monotonicity #685]: #687
#703 := [monotonicity #688 #700]: #702
#706 := [monotonicity #642 #703]: #705
#711 := [trans #706 #709]: #710
#869 := [monotonicity #711 #866]: #868
#897 := [monotonicity #642 #869]: #896
#900 := [monotonicity #897]: #899
#893 := (iff #500 #892)
#890 := (iff #174 #889)
#887 := (iff #171 #886)
#884 := (iff #37 #883)
#885 := [rewrite]: #884
#879 := (iff #170 #878)
#876 := (iff #35 #875)
#873 := (iff #34 #872)
#874 := [rewrite]: #873
#877 := [monotonicity #604 #874]: #876
#880 := [monotonicity #877]: #879
#888 := [monotonicity #880 #885]: #887
#891 := [quant-intro #888]: #890
#894 := [monotonicity #891]: #893
#903 := [monotonicity #894 #900]: #902
#906 := [monotonicity #642 #903]: #905
#909 := [monotonicity #906]: #908
#914 := [trans #909 #912]: #913
#917 := [monotonicity #914]: #916
#629 := (iff #536 #628)
#626 := (iff #167 #625)
#623 := (iff #164 #622)
#617 := (iff #25 #618)
#621 := [rewrite]: #617
#614 := (iff #163 #613)
#611 := (iff #23 #610)
#607 := (iff #22 #606)
#609 := [rewrite]: #607
#612 := [monotonicity #604 #609]: #611
#615 := [monotonicity #612]: #614
#624 := [monotonicity #615 #621]: #623
#627 := [quant-intro #624]: #626
#630 := [monotonicity #627]: #629
#920 := [monotonicity #630 #917]: #919
#923 := [monotonicity #627 #920]: #922
#601 := (iff #548 false)
#596 := (not true)
#599 := (iff #596 false)
#600 := [rewrite]: #599
#597 := (iff #548 #596)
#594 := (iff #160 true)
#586 := (and true true)
#589 := (and true #586)
#592 := (iff #589 true)
#593 := [rewrite]: #592
#590 := (iff #160 #589)
#587 := (iff #157 #586)
#584 := (iff #16 true)
#585 := [rewrite]: #584
#582 := (iff #14 true)
#583 := [rewrite]: #582
#588 := [monotonicity #583 #585]: #587
#591 := [monotonicity #583 #588]: #590
#595 := [trans #591 #593]: #594
#598 := [monotonicity #595]: #597
#602 := [trans #598 #600]: #601
#937 := [monotonicity #602 #923]: #936
#940 := [monotonicity #937]: #939
#933 := (iff #566 #924)
#925 := (not #924)
#928 := (not #925)
#931 := (iff #928 #924)
#932 := [rewrite]: #931
#929 := (iff #566 #928)
#926 := (iff #9 #925)
#927 := [rewrite]: #926
#930 := [monotonicity #927]: #929
#934 := [trans #930 #932]: #933
#943 := [monotonicity #934 #940]: #942
#948 := [trans #943 #946]: #947
#951 := [monotonicity #948]: #950
#580 := (iff #134 #579)
#577 := (iff #133 #567)
#572 := (implies true #567)
#575 := (iff #572 #567)
#576 := [rewrite]: #575
#573 := (iff #133 #572)
#570 := (iff #132 #567)
#563 := (implies #9 #558)
#568 := (iff #563 #567)
#569 := [rewrite]: #568
#564 := (iff #132 #563)
#561 := (iff #131 #558)
#554 := (implies #13 #549)
#559 := (iff #554 #558)
#560 := [rewrite]: #559
#555 := (iff #131 #554)
#552 := (iff #130 #549)
#545 := (implies #160 #542)
#550 := (iff #545 #549)
#551 := [rewrite]: #550
#546 := (iff #130 #545)
#543 := (iff #129 #542)
#540 := (iff #128 #537)
#533 := (implies #167 #530)
#538 := (iff #533 #537)
#539 := [rewrite]: #538
#534 := (iff #128 #533)
#531 := (iff #127 #530)
#528 := (iff #126 #525)
#521 := (implies #28 #509)
#526 := (iff #521 #525)
#527 := [rewrite]: #526
#522 := (iff #126 #521)
#519 := (iff #125 #509)
#514 := (implies true #509)
#517 := (iff #514 #509)
#518 := [rewrite]: #517
#515 := (iff #125 #514)
#512 := (iff #124 #509)
#506 := (implies #33 #501)
#510 := (iff #506 #509)
#511 := [rewrite]: #510
#507 := (iff #124 #506)
#504 := (iff #123 #501)
#497 := (implies #174 #492)
#502 := (iff #497 #501)
#503 := [rewrite]: #502
#498 := (iff #123 #497)
#495 := (iff #122 #492)
#488 := (implies #41 #483)
#493 := (iff #488 #492)
#494 := [rewrite]: #493
#489 := (iff #122 #488)
#486 := (iff #121 #483)
#480 := (implies #33 #477)
#484 := (iff #480 #483)
#485 := [rewrite]: #484
#481 := (iff #121 #480)
#478 := (iff #120 #477)
#475 := (iff #119 #465)
#470 := (implies true #465)
#473 := (iff #470 #465)
#474 := [rewrite]: #473
#471 := (iff #119 #470)
#468 := (iff #118 #465)
#462 := (implies #33 #457)
#466 := (iff #462 #465)
#467 := [rewrite]: #466
#463 := (iff #118 #462)
#460 := (iff #117 #457)
#453 := (implies #67 #448)
#458 := (iff #453 #457)
#459 := [rewrite]: #458
#454 := (iff #117 #453)
#451 := (iff #116 #448)
#445 := (implies #33 #442)
#449 := (iff #445 #448)
#450 := [rewrite]: #449
#446 := (iff #116 #445)
#443 := (iff #115 #442)
#440 := (iff #114 #430)
#435 := (implies true #430)
#438 := (iff #435 #430)
#439 := [rewrite]: #438
#436 := (iff #114 #435)
#433 := (iff #113 #430)
#427 := (implies #33 #422)
#431 := (iff #427 #430)
#432 := [rewrite]: #431
#428 := (iff #113 #427)
#425 := (iff #112 #422)
#418 := (implies #106 #413)
#423 := (iff #418 #422)
#424 := [rewrite]: #423
#419 := (iff #112 #418)
#416 := (iff #111 #413)
#410 := (implies #33 #405)
#414 := (iff #410 #413)
#415 := [rewrite]: #414
#411 := (iff #111 #410)
#408 := (iff #110 #405)
#401 := (implies #107 #396)
#406 := (iff #401 #405)
#407 := [rewrite]: #406
#402 := (iff #110 #401)
#399 := (iff #109 #396)
#392 := (implies #108 #320)
#397 := (iff #392 #396)
#398 := [rewrite]: #397
#393 := (iff #109 #392)
#330 := (iff #98 #320)
#325 := (implies true #320)
#328 := (iff #325 #320)
#329 := [rewrite]: #328
#326 := (iff #98 #325)
#323 := (iff #97 #320)
#316 := (implies #78 #311)
#321 := (iff #316 #320)
#322 := [rewrite]: #321
#317 := (iff #97 #316)
#314 := (iff #96 #311)
#307 := (implies #274 #302)
#312 := (iff #307 #311)
#313 := [rewrite]: #312
#308 := (iff #96 #307)
#305 := (iff #95 #302)
#298 := (implies #84 #295)
#303 := (iff #298 #302)
#304 := [rewrite]: #303
#299 := (iff #95 #298)
#296 := (iff #94 #295)
#293 := (iff #93 #290)
#286 := (implies #281 #91)
#291 := (iff #286 #290)
#292 := [rewrite]: #291
#287 := (iff #93 #286)
#284 := (iff #92 #91)
#285 := [rewrite]: #284
#282 := (iff #89 #281)
#279 := (iff #88 #278)
#280 := [rewrite]: #279
#283 := [quant-intro #280]: #282
#288 := [monotonicity #283 #285]: #287
#294 := [trans #288 #292]: #293
#297 := [monotonicity #283 #294]: #296
#300 := [monotonicity #297]: #299
#306 := [trans #300 #304]: #305
#275 := (iff #81 #274)
#272 := (= #80 #271)
#273 := [rewrite]: #272
#276 := [monotonicity #273]: #275
#309 := [monotonicity #276 #306]: #308
#315 := [trans #309 #313]: #314
#318 := [monotonicity #315]: #317
#324 := [trans #318 #322]: #323
#327 := [monotonicity #324]: #326
#331 := [trans #327 #329]: #330
#394 := [monotonicity #331]: #393
#400 := [trans #394 #398]: #399
#403 := [monotonicity #400]: #402
#409 := [trans #403 #407]: #408
#412 := [monotonicity #409]: #411
#417 := [trans #412 #415]: #416
#420 := [monotonicity #417]: #419
#426 := [trans #420 #424]: #425
#429 := [monotonicity #426]: #428
#434 := [trans #429 #432]: #433
#437 := [monotonicity #434]: #436
#441 := [trans #437 #439]: #440
#390 := (iff #105 #380)
#385 := (implies true #380)
#388 := (iff #385 #380)
#389 := [rewrite]: #388
#386 := (iff #105 #385)
#383 := (iff #104 #380)
#377 := (implies #33 #372)
#381 := (iff #377 #380)
#382 := [rewrite]: #381
#378 := (iff #104 #377)
#375 := (iff #103 #372)
#368 := (implies #69 #363)
#373 := (iff #368 #372)
#374 := [rewrite]: #373
#369 := (iff #103 #368)
#366 := (iff #102 #363)
#359 := (implies #71 #354)
#364 := (iff #359 #363)
#365 := [rewrite]: #364
#360 := (iff #102 #359)
#357 := (iff #101 #354)
#350 := (implies #32 #345)
#355 := (iff #350 #354)
#356 := [rewrite]: #355
#351 := (iff #101 #350)
#348 := (iff #100 #345)
#341 := (implies #74 #336)
#346 := (iff #341 #345)
#347 := [rewrite]: #346
#342 := (iff #100 #341)
#339 := (iff #99 #336)
#332 := (implies #76 #320)
#337 := (iff #332 #336)
#338 := [rewrite]: #337
#333 := (iff #99 #332)
#334 := [monotonicity #331]: #333
#340 := [trans #334 #338]: #339
#343 := [monotonicity #340]: #342
#349 := [trans #343 #347]: #348
#269 := (iff #72 #32)
#270 := [rewrite]: #269
#352 := [monotonicity #270 #349]: #351
#358 := [trans #352 #356]: #357
#361 := [monotonicity #358]: #360
#367 := [trans #361 #365]: #366
#370 := [monotonicity #367]: #369
#376 := [trans #370 #374]: #375
#379 := [monotonicity #376]: #378
#384 := [trans #379 #382]: #383
#387 := [monotonicity #384]: #386
#391 := [trans #387 #389]: #390
#444 := [monotonicity #391 #441]: #443
#447 := [monotonicity #444]: #446
#452 := [trans #447 #450]: #451
#455 := [monotonicity #452]: #454
#461 := [trans #455 #459]: #460
#464 := [monotonicity #461]: #463
#469 := [trans #464 #467]: #468
#472 := [monotonicity #469]: #471
#476 := [trans #472 #474]: #475
#267 := (iff #66 #257)
#262 := (implies true #257)
#265 := (iff #262 #257)
#266 := [rewrite]: #265
#263 := (iff #66 #262)
#260 := (iff #65 #257)
#254 := (implies #33 #249)
#258 := (iff #254 #257)
#259 := [rewrite]: #258
#255 := (iff #65 #254)
#252 := (iff #64 #249)
#245 := (implies #42 #240)
#250 := (iff #245 #249)
#251 := [rewrite]: #250
#246 := (iff #64 #245)
#243 := (iff #63 #240)
#236 := (implies #33 #231)
#241 := (iff #236 #240)
#242 := [rewrite]: #241
#237 := (iff #63 #236)
#234 := (iff #62 #231)
#227 := (implies #44 #222)
#232 := (iff #227 #231)
#233 := [rewrite]: #232
#228 := (iff #62 #227)
#225 := (iff #61 #222)
#218 := (implies #46 #213)
#223 := (iff #218 #222)
#224 := [rewrite]: #223
#219 := (iff #61 #218)
#216 := (iff #60 #213)
#209 := (implies #48 #206)
#214 := (iff #209 #213)
#215 := [rewrite]: #214
#210 := (iff #60 #209)
#207 := (iff #59 #206)
#204 := (iff #58 #201)
#197 := (implies #181 #187)
#202 := (iff #197 #201)
#203 := [rewrite]: #202
#198 := (iff #58 #197)
#195 := (iff #57 #187)
#190 := (and #187 true)
#193 := (iff #190 #187)
#194 := [rewrite]: #193
#191 := (iff #57 #190)
#188 := (iff #56 #187)
#185 := (iff #55 #184)
#186 := [rewrite]: #185
#189 := [quant-intro #186]: #188
#192 := [monotonicity #189]: #191
#196 := [trans #192 #194]: #195
#182 := (iff #53 #181)
#179 := (iff #52 #178)
#180 := [rewrite]: #179
#183 := [quant-intro #180]: #182
#199 := [monotonicity #183 #196]: #198
#205 := [trans #199 #203]: #204
#208 := [monotonicity #183 #205]: #207
#211 := [monotonicity #208]: #210
#217 := [trans #211 #215]: #216
#220 := [monotonicity #217]: #219
#226 := [trans #220 #224]: #225
#229 := [monotonicity #226]: #228
#235 := [trans #229 #233]: #234
#238 := [monotonicity #235]: #237
#244 := [trans #238 #242]: #243
#247 := [monotonicity #244]: #246
#253 := [trans #247 #251]: #252
#256 := [monotonicity #253]: #255
#261 := [trans #256 #259]: #260
#264 := [monotonicity #261]: #263
#268 := [trans #264 #266]: #267
#479 := [monotonicity #268 #476]: #478
#482 := [monotonicity #479]: #481
#487 := [trans #482 #485]: #486
#490 := [monotonicity #487]: #489
#496 := [trans #490 #494]: #495
#175 := (iff #39 #174)
#172 := (iff #38 #171)
#173 := [rewrite]: #172
#176 := [quant-intro #173]: #175
#499 := [monotonicity #176 #496]: #498
#505 := [trans #499 #503]: #504
#508 := [monotonicity #505]: #507
#513 := [trans #508 #511]: #512
#516 := [monotonicity #513]: #515
#520 := [trans #516 #518]: #519
#523 := [monotonicity #520]: #522
#529 := [trans #523 #527]: #528
#532 := [monotonicity #529]: #531
#168 := (iff #27 #167)
#165 := (iff #26 #164)
#166 := [rewrite]: #165
#169 := [quant-intro #166]: #168
#535 := [monotonicity #169 #532]: #534
#541 := [trans #535 #539]: #540
#544 := [monotonicity #169 #541]: #543
#161 := (iff #19 #160)
#158 := (iff #18 #157)
#155 := (iff #17 #16)
#156 := [rewrite]: #155
#159 := [monotonicity #156]: #158
#162 := [monotonicity #159]: #161
#547 := [monotonicity #162 #544]: #546
#553 := [trans #547 #551]: #552
#556 := [monotonicity #553]: #555
#562 := [trans #556 #560]: #561
#565 := [monotonicity #562]: #564
#571 := [trans #565 #569]: #570
#574 := [monotonicity #571]: #573
#578 := [trans #574 #576]: #577
#581 := [monotonicity #578]: #580
#953 := [trans #581 #951]: #952
#154 := [asserted]: #134
#954 := [mp #154 #953]: #949
#956 := [not-or-elim #954]: #13
#1861 := [trans #956 #1854]: #1927
#1749 := (not #961)
#1740 := (or #1333 #1749)
#1751 := [def-axiom]: #1740
#1863 := [unit-resolution #1751 #1926]: #1749
#1864 := (not #1927)
#1892 := (or #1864 #961)
#1865 := [th-lemma arith triangle-eq]: #1892
#1867 := [unit-resolution #1865 #1863 #1861]: false
#1868 := [lemma #1867]: #1333
#2178 := (or #1338 #2175)
#1520 := (forall (vars (?v0 Int)) #1515)
#1526 := (not #1520)
#1527 := (or #1526 #91)
#1528 := (not #1527)
#1533 := (or #1498 #1528)
#1541 := (not #1533)
#1551 := (or #1470 #772 #404 #395 #769 #760 #1539 #1540 #1541)
#1552 := (not #1551)
#1542 := (or #1470 #773 #362 #344 #335 #769 #760 #1539 #1540 #1541)
#1543 := (not #1542)
#1557 := (or #1543 #1552)
#1563 := (not #1557)
#1564 := (or #1470 #769 #683 #1563)
#1565 := (not #1564)
#1408 := (forall (vars (?v0 Int)) #1405)
#1464 := (or #1408 #1459)
#1471 := (not #1464)
#1472 := (or #1470 #769 #686 #230 #221 #212 #1471)
#1473 := (not #1472)
#1570 := (or #1473 #1565)
#1577 := (not #1570)
#1383 := (forall (vars (?v0 Int)) #1378)
#1576 := (not #1383)
#1578 := (or #524 #1470 #769 #1576 #491 #1577)
#1579 := (not #1578)
#1584 := (or #524 #1579)
#1591 := (not #1584)
#1361 := (forall (vars (?v0 Int)) #1356)
#1590 := (not #1361)
#1592 := (or #1590 #1591)
#1593 := (not #1592)
#1598 := (or #1338 #1593)
#2179 := (iff #1598 #2178)
#2176 := (iff #1593 #2175)
#2173 := (iff #1592 #2172)
#2170 := (iff #1591 #2169)
#2167 := (iff #1584 #2166)
#2164 := (iff #1579 #2163)
#2161 := (iff #1578 #2160)
#2158 := (iff #1577 #2157)
#2155 := (iff #1570 #2154)
#2152 := (iff #1565 #2151)
#2149 := (iff #1564 #2148)
#2146 := (iff #1563 #2145)
#2143 := (iff #1557 #2142)
#2140 := (iff #1552 #2139)
#2137 := (iff #1551 #2136)
#2128 := (iff #1541 #2127)
#2125 := (iff #1533 #2124)
#2122 := (iff #1528 #2121)
#2119 := (iff #1527 #2118)
#2116 := (iff #1526 #2115)
#2113 := (iff #1520 #2110)
#2111 := (iff #1515 #1515)
#2112 := [refl]: #2111
#2114 := [quant-intro #2112]: #2113
#2117 := [monotonicity #2114]: #2116
#2120 := [monotonicity #2117]: #2119
#2123 := [monotonicity #2120]: #2122
#2126 := [monotonicity #2123]: #2125
#2129 := [monotonicity #2126]: #2128
#2138 := [monotonicity #2129]: #2137
#2141 := [monotonicity #2138]: #2140
#2134 := (iff #1543 #2133)
#2131 := (iff #1542 #2130)
#2132 := [monotonicity #2129]: #2131
#2135 := [monotonicity #2132]: #2134
#2144 := [monotonicity #2135 #2141]: #2143
#2147 := [monotonicity #2144]: #2146
#2150 := [monotonicity #2147]: #2149
#2153 := [monotonicity #2150]: #2152
#2108 := (iff #1473 #2107)
#2105 := (iff #1472 #2104)
#2102 := (iff #1471 #2101)
#2099 := (iff #1464 #2098)
#2096 := (iff #1408 #2093)
#2094 := (iff #1405 #1405)
#2095 := [refl]: #2094
#2097 := [quant-intro #2095]: #2096
#2100 := [monotonicity #2097]: #2099
#2103 := [monotonicity #2100]: #2102
#2106 := [monotonicity #2103]: #2105
#2109 := [monotonicity #2106]: #2108
#2156 := [monotonicity #2109 #2153]: #2155
#2159 := [monotonicity #2156]: #2158
#2091 := (iff #1576 #2090)
#2088 := (iff #1383 #2085)
#2086 := (iff #1378 #1378)
#2087 := [refl]: #2086
#2089 := [quant-intro #2087]: #2088
#2092 := [monotonicity #2089]: #2091
#2162 := [monotonicity #2092 #2159]: #2161
#2165 := [monotonicity #2162]: #2164
#2168 := [monotonicity #2165]: #2167
#2171 := [monotonicity #2168]: #2170
#2083 := (iff #1590 #2082)
#2080 := (iff #1361 #2077)
#2078 := (iff #1356 #1356)
#2079 := [refl]: #2078
#2081 := [quant-intro #2079]: #2080
#2084 := [monotonicity #2081]: #2083
#2174 := [monotonicity #2084 #2171]: #2173
#2177 := [monotonicity #2174]: #2176
#2180 := [monotonicity #2177]: #2179
#1116 := (not #91)
#1119 := (and #744 #1116)
#1245 := (not #1240)
#1248 := (and #1094 #1245)
#1251 := (not #1248)
#1267 := (or #1251 #1262)
#1270 := (not #1267)
#1273 := (or #1270 #1119)
#1291 := (and #632 #773 #107 #108 #635 #756 #713 #716 #1273)
#1279 := (and #632 #772 #71 #74 #76 #635 #756 #713 #716 #1273)
#1296 := (or #1279 #1291)
#1302 := (and #632 #635 #686 #1296)
#1043 := (not #1042)
#1044 := (and #1039 #1043)
#1045 := (not #1044)
#1198 := (or #1045 #1193)
#1201 := (not #1198)
#1025 := (not #1024)
#1026 := (and #1021 #1025)
#1027 := (not #1026)
#1030 := (or #1027 #1029)
#1204 := (and #1030 #1201)
#1014 := (not #655)
#1017 := (forall (vars (?v0 Int)) #1014)
#1207 := (or #1017 #1204)
#1213 := (and #632 #635 #683 #44 #46 #48 #1207)
#1307 := (or #1213 #1302)
#1313 := (and #28 #632 #635 #889 #41 #1307)
#1318 := (or #524 #1313)
#1321 := (and #625 #1318)
#964 := (and #969 #971)
#965 := (not #964)
#972 := (or #965 #961)
#973 := (not #972)
#1324 := (or #973 #1321)
#1599 := (iff #1324 #1598)
#1596 := (iff #1321 #1593)
#1587 := (and #1361 #1584)
#1594 := (iff #1587 #1593)
#1595 := [rewrite]: #1594
#1588 := (iff #1321 #1587)
#1585 := (iff #1318 #1584)
#1582 := (iff #1313 #1579)
#1573 := (and #28 #632 #635 #1383 #41 #1570)
#1580 := (iff #1573 #1579)
#1581 := [rewrite]: #1580
#1574 := (iff #1313 #1573)
#1571 := (iff #1307 #1570)
#1568 := (iff #1302 #1565)
#1560 := (and #632 #635 #686 #1557)
#1566 := (iff #1560 #1565)
#1567 := [rewrite]: #1566
#1561 := (iff #1302 #1560)
#1558 := (iff #1296 #1557)
#1555 := (iff #1291 #1552)
#1548 := (and #632 #773 #107 #108 #635 #756 #713 #716 #1533)
#1553 := (iff #1548 #1552)
#1554 := [rewrite]: #1553
#1549 := (iff #1291 #1548)
#1534 := (iff #1273 #1533)
#1531 := (iff #1119 #1528)
#1523 := (and #1520 #1116)
#1529 := (iff #1523 #1528)
#1530 := [rewrite]: #1529
#1524 := (iff #1119 #1523)
#1521 := (iff #744 #1520)
#1518 := (iff #741 #1515)
#1501 := (or #1341 #724)
#1512 := (or #1501 #738)
#1516 := (iff #1512 #1515)
#1517 := [rewrite]: #1516
#1513 := (iff #741 #1512)
#1510 := (iff #733 #1501)
#1502 := (not #1501)
#1505 := (not #1502)
#1508 := (iff #1505 #1501)
#1509 := [rewrite]: #1508
#1506 := (iff #733 #1505)
#1503 := (iff #730 #1502)
#1504 := [rewrite]: #1503
#1507 := [monotonicity #1504]: #1506
#1511 := [trans #1507 #1509]: #1510
#1514 := [monotonicity #1511]: #1513
#1519 := [trans #1514 #1517]: #1518
#1522 := [quant-intro #1519]: #1521
#1525 := [monotonicity #1522]: #1524
#1532 := [trans #1525 #1530]: #1531
#1499 := (iff #1270 #1498)
#1496 := (iff #1267 #1493)
#1479 := (or #1478 #1240)
#1490 := (or #1479 #1262)
#1494 := (iff #1490 #1493)
#1495 := [rewrite]: #1494
#1491 := (iff #1267 #1490)
#1488 := (iff #1251 #1479)
#1480 := (not #1479)
#1483 := (not #1480)
#1486 := (iff #1483 #1479)
#1487 := [rewrite]: #1486
#1484 := (iff #1251 #1483)
#1481 := (iff #1248 #1480)
#1482 := [rewrite]: #1481
#1485 := [monotonicity #1482]: #1484
#1489 := [trans #1485 #1487]: #1488
#1492 := [monotonicity #1489]: #1491
#1497 := [trans #1492 #1495]: #1496
#1500 := [monotonicity #1497]: #1499
#1535 := [monotonicity #1500 #1532]: #1534
#1550 := [monotonicity #1535]: #1549
#1556 := [trans #1550 #1554]: #1555
#1546 := (iff #1279 #1543)
#1536 := (and #632 #772 #71 #74 #76 #635 #756 #713 #716 #1533)
#1544 := (iff #1536 #1543)
#1545 := [rewrite]: #1544
#1537 := (iff #1279 #1536)
#1538 := [monotonicity #1535]: #1537
#1547 := [trans #1538 #1545]: #1546
#1559 := [monotonicity #1547 #1556]: #1558
#1562 := [monotonicity #1559]: #1561
#1569 := [trans #1562 #1567]: #1568
#1476 := (iff #1213 #1473)
#1467 := (and #632 #635 #683 #44 #46 #48 #1464)
#1474 := (iff #1467 #1473)
#1475 := [rewrite]: #1474
#1468 := (iff #1213 #1467)
#1465 := (iff #1207 #1464)
#1462 := (iff #1204 #1459)
#1446 := (or #1431 #1042 #1193)
#1451 := (not #1446)
#1454 := (and #1426 #1451)
#1460 := (iff #1454 #1459)
#1461 := [rewrite]: #1460
#1455 := (iff #1204 #1454)
#1452 := (iff #1201 #1451)
#1449 := (iff #1198 #1446)
#1432 := (or #1431 #1042)
#1443 := (or #1432 #1193)
#1447 := (iff #1443 #1446)
#1448 := [rewrite]: #1447
#1444 := (iff #1198 #1443)
#1441 := (iff #1045 #1432)
#1433 := (not #1432)
#1436 := (not #1433)
#1439 := (iff #1436 #1432)
#1440 := [rewrite]: #1439
#1437 := (iff #1045 #1436)
#1434 := (iff #1044 #1433)
#1435 := [rewrite]: #1434
#1438 := [monotonicity #1435]: #1437
#1442 := [trans #1438 #1440]: #1441
#1445 := [monotonicity #1442]: #1444
#1450 := [trans #1445 #1448]: #1449
#1453 := [monotonicity #1450]: #1452
#1429 := (iff #1030 #1426)
#1412 := (or #1411 #1024)
#1423 := (or #1412 #1029)
#1427 := (iff #1423 #1426)
#1428 := [rewrite]: #1427
#1424 := (iff #1030 #1423)
#1421 := (iff #1027 #1412)
#1413 := (not #1412)
#1416 := (not #1413)
#1419 := (iff #1416 #1412)
#1420 := [rewrite]: #1419
#1417 := (iff #1027 #1416)
#1414 := (iff #1026 #1413)
#1415 := [rewrite]: #1414
#1418 := [monotonicity #1415]: #1417
#1422 := [trans #1418 #1420]: #1421
#1425 := [monotonicity #1422]: #1424
#1430 := [trans #1425 #1428]: #1429
#1456 := [monotonicity #1430 #1453]: #1455
#1463 := [trans #1456 #1461]: #1462
#1409 := (iff #1017 #1408)
#1406 := (iff #1014 #1405)
#1403 := (iff #655 #1400)
#1386 := (or #1341 #645)
#1397 := (or #1386 #51)
#1401 := (iff #1397 #1400)
#1402 := [rewrite]: #1401
#1398 := (iff #655 #1397)
#1395 := (iff #652 #1386)
#1387 := (not #1386)
#1390 := (not #1387)
#1393 := (iff #1390 #1386)
#1394 := [rewrite]: #1393
#1391 := (iff #652 #1390)
#1388 := (iff #649 #1387)
#1389 := [rewrite]: #1388
#1392 := [monotonicity #1389]: #1391
#1396 := [trans #1392 #1394]: #1395
#1399 := [monotonicity #1396]: #1398
#1404 := [trans #1399 #1402]: #1403
#1407 := [monotonicity #1404]: #1406
#1410 := [quant-intro #1407]: #1409
#1466 := [monotonicity #1410 #1463]: #1465
#1469 := [monotonicity #1466]: #1468
#1477 := [trans #1469 #1475]: #1476
#1572 := [monotonicity #1477 #1569]: #1571
#1384 := (iff #889 #1383)
#1381 := (iff #886 #1378)
#1364 := (or #1341 #870)
#1375 := (or #1364 #883)
#1379 := (iff #1375 #1378)
#1380 := [rewrite]: #1379
#1376 := (iff #886 #1375)
#1373 := (iff #878 #1364)
#1365 := (not #1364)
#1368 := (not #1365)
#1371 := (iff #1368 #1364)
#1372 := [rewrite]: #1371
#1369 := (iff #878 #1368)
#1366 := (iff #875 #1365)
#1367 := [rewrite]: #1366
#1370 := [monotonicity #1367]: #1369
#1374 := [trans #1370 #1372]: #1373
#1377 := [monotonicity #1374]: #1376
#1382 := [trans #1377 #1380]: #1381
#1385 := [quant-intro #1382]: #1384
#1575 := [monotonicity #1385 #1572]: #1574
#1583 := [trans #1575 #1581]: #1582
#1586 := [monotonicity #1583]: #1585
#1362 := (iff #625 #1361)
#1359 := (iff #622 #1356)
#1342 := (or #1341 #608)
#1353 := (or #1342 #618)
#1357 := (iff #1353 #1356)
#1358 := [rewrite]: #1357
#1354 := (iff #622 #1353)
#1351 := (iff #613 #1342)
#1343 := (not #1342)
#1346 := (not #1343)
#1349 := (iff #1346 #1342)
#1350 := [rewrite]: #1349
#1347 := (iff #613 #1346)
#1344 := (iff #610 #1343)
#1345 := [rewrite]: #1344
#1348 := [monotonicity #1345]: #1347
#1352 := [trans #1348 #1350]: #1351
#1355 := [monotonicity #1352]: #1354
#1360 := [trans #1355 #1358]: #1359
#1363 := [quant-intro #1360]: #1362
#1589 := [monotonicity #1363 #1586]: #1588
#1597 := [trans #1589 #1595]: #1596
#1339 := (iff #973 #1338)
#1336 := (iff #972 #1333)
#1034 := (or #1033 #970)
#1330 := (or #1034 #961)
#1334 := (iff #1330 #1333)
#1335 := [rewrite]: #1334
#1331 := (iff #972 #1330)
#1328 := (iff #965 #1034)
#1054 := (not #1034)
#1108 := (not #1054)
#1172 := (iff #1108 #1034)
#1327 := [rewrite]: #1172
#976 := (iff #965 #1108)
#1055 := (iff #964 #1054)
#1107 := [rewrite]: #1055
#977 := [monotonicity #1107]: #976
#1329 := [trans #977 #1327]: #1328
#1332 := [monotonicity #1329]: #1331
#1337 := [trans #1332 #1335]: #1336
#1340 := [monotonicity #1337]: #1339
#1600 := [monotonicity #1340 #1597]: #1599
#1101 := (+ #1100 #736)
#1102 := (<= #1101 0::Int)
#1095 := (+ ?v0!3 #725)
#1096 := (>= #1095 0::Int)
#1097 := (not #1096)
#1098 := (and #1094 #1097)
#1099 := (not #1098)
#1103 := (or #1099 #1102)
#1104 := (not #1103)
#1123 := (or #1104 #1119)
#1090 := (not #721)
#1087 := (not #760)
#1084 := (not #766)
#1136 := (not #395)
#1133 := (not #404)
#990 := (not #640)
#1139 := (and #990 #778 #1133 #1136 #1084 #1087 #1090 #1123)
#1081 := (not #335)
#1078 := (not #344)
#1075 := (not #769)
#1072 := (not #362)
#1127 := (and #990 #772 #1072 #1075 #1078 #1081 #1084 #1087 #1090 #1123)
#1143 := (or #1127 #1139)
#1147 := (and #990 #686 #1143)
#1047 := (+ #1046 #664)
#1048 := (<= #1047 0::Int)
#1049 := (or #1045 #1048)
#1050 := (not #1049)
#1056 := (and #1030 #1050)
#1060 := (or #1017 #1056)
#1011 := (not #212)
#1008 := (not #221)
#1005 := (not #230)
#1064 := (and #990 #846 #1005 #1008 #1011 #1060)
#1151 := (or #1064 #1147)
#1000 := (not #491)
#987 := (not #524)
#1155 := (and #987 #990 #889 #1000 #1151)
#1159 := (or #524 #1155)
#1163 := (and #625 #1159)
#1167 := (or #973 #1163)
#1325 := (iff #1167 #1324)
#1322 := (iff #1163 #1321)
#1319 := (iff #1159 #1318)
#1316 := (iff #1155 #1313)
#1310 := (and #28 #637 #889 #41 #1307)
#1314 := (iff #1310 #1313)
#1315 := [rewrite]: #1314
#1311 := (iff #1155 #1310)
#1308 := (iff #1151 #1307)
#1305 := (iff #1147 #1302)
#1299 := (and #637 #686 #1296)
#1303 := (iff #1299 #1302)
#1304 := [rewrite]: #1303
#1300 := (iff #1147 #1299)
#1297 := (iff #1143 #1296)
#1294 := (iff #1139 #1291)
#1288 := (and #637 #773 #107 #108 #763 #756 #718 #1273)
#1292 := (iff #1288 #1291)
#1293 := [rewrite]: #1292
#1289 := (iff #1139 #1288)
#1274 := (iff #1123 #1273)
#1271 := (iff #1104 #1270)
#1268 := (iff #1103 #1267)
#1265 := (iff #1102 #1262)
#1254 := (+ #736 #1100)
#1257 := (<= #1254 0::Int)
#1263 := (iff #1257 #1262)
#1264 := [rewrite]: #1263
#1258 := (iff #1102 #1257)
#1255 := (= #1101 #1254)
#1256 := [rewrite]: #1255
#1259 := [monotonicity #1256]: #1258
#1266 := [trans #1259 #1264]: #1265
#1252 := (iff #1099 #1251)
#1249 := (iff #1098 #1248)
#1246 := (iff #1097 #1245)
#1243 := (iff #1096 #1240)
#1232 := (+ #725 ?v0!3)
#1235 := (>= #1232 0::Int)
#1241 := (iff #1235 #1240)
#1242 := [rewrite]: #1241
#1236 := (iff #1096 #1235)
#1233 := (= #1095 #1232)
#1234 := [rewrite]: #1233
#1237 := [monotonicity #1234]: #1236
#1244 := [trans #1237 #1242]: #1243
#1247 := [monotonicity #1244]: #1246
#1250 := [monotonicity #1247]: #1249
#1253 := [monotonicity #1250]: #1252
#1269 := [monotonicity #1253 #1266]: #1268
#1272 := [monotonicity #1269]: #1271
#1275 := [monotonicity #1272]: #1274
#1230 := (iff #1090 #718)
#1231 := [rewrite]: #1230
#1228 := (iff #1087 #756)
#1229 := [rewrite]: #1228
#1226 := (iff #1084 #763)
#1227 := [rewrite]: #1226
#1286 := (iff #1136 #108)
#1287 := [rewrite]: #1286
#1284 := (iff #1133 #107)
#1285 := [rewrite]: #1284
#1175 := (iff #990 #637)
#1176 := [rewrite]: #1175
#1290 := [monotonicity #1176 #782 #1285 #1287 #1227 #1229 #1231 #1275]: #1289
#1295 := [trans #1290 #1293]: #1294
#1282 := (iff #1127 #1279)
#1276 := (and #637 #772 #71 #635 #74 #76 #763 #756 #718 #1273)
#1280 := (iff #1276 #1279)
#1281 := [rewrite]: #1280
#1277 := (iff #1127 #1276)
#1224 := (iff #1081 #76)
#1225 := [rewrite]: #1224
#1222 := (iff #1078 #74)
#1223 := [rewrite]: #1222
#1220 := (iff #1075 #635)
#1221 := [rewrite]: #1220
#1218 := (iff #1072 #71)
#1219 := [rewrite]: #1218
#1278 := [monotonicity #1176 #1219 #1221 #1223 #1225 #1227 #1229 #1231 #1275]: #1277
#1283 := [trans #1278 #1281]: #1282
#1298 := [monotonicity #1283 #1295]: #1297
#1301 := [monotonicity #1176 #1298]: #1300
#1306 := [trans #1301 #1304]: #1305
#1216 := (iff #1064 #1213)
#1210 := (and #637 #683 #44 #46 #48 #1207)
#1214 := (iff #1210 #1213)
#1215 := [rewrite]: #1214
#1211 := (iff #1064 #1210)
#1208 := (iff #1060 #1207)
#1205 := (iff #1056 #1204)
#1202 := (iff #1050 #1201)
#1199 := (iff #1049 #1198)
#1196 := (iff #1048 #1193)
#1185 := (+ #664 #1046)
#1188 := (<= #1185 0::Int)
#1194 := (iff #1188 #1193)
#1195 := [rewrite]: #1194
#1189 := (iff #1048 #1188)
#1186 := (= #1047 #1185)
#1187 := [rewrite]: #1186
#1190 := [monotonicity #1187]: #1189
#1197 := [trans #1190 #1195]: #1196
#1200 := [monotonicity #1197]: #1199
#1203 := [monotonicity #1200]: #1202
#1206 := [monotonicity #1203]: #1205
#1209 := [monotonicity #1206]: #1208
#1183 := (iff #1011 #48)
#1184 := [rewrite]: #1183
#1181 := (iff #1008 #46)
#1182 := [rewrite]: #1181
#1179 := (iff #1005 #44)
#1180 := [rewrite]: #1179
#1212 := [monotonicity #1176 #850 #1180 #1182 #1184 #1209]: #1211
#1217 := [trans #1212 #1215]: #1216
#1309 := [monotonicity #1217 #1306]: #1308
#1177 := (iff #1000 #41)
#1178 := [rewrite]: #1177
#1173 := (iff #987 #28)
#1174 := [rewrite]: #1173
#1312 := [monotonicity #1174 #1176 #1178 #1309]: #1311
#1317 := [trans #1312 #1315]: #1316
#1320 := [monotonicity #1317]: #1319
#1323 := [monotonicity #1320]: #1322
#1326 := [monotonicity #1323]: #1325
#957 := (not #921)
#1168 := (~ #957 #1167)
#1164 := (not #918)
#1165 := (~ #1164 #1163)
#1160 := (not #915)
#1161 := (~ #1160 #1159)
#1156 := (not #910)
#1157 := (~ #1156 #1155)
#1152 := (not #867)
#1153 := (~ #1152 #1151)
#1148 := (not #862)
#1149 := (~ #1148 #1147)
#1144 := (not #841)
#1145 := (~ #1144 #1143)
#1140 := (not #836)
#1141 := (~ #1140 #1139)
#1124 := (not #753)
#1125 := (~ #1124 #1123)
#1120 := (not #750)
#1121 := (~ #1120 #1119)
#1117 := (~ #1116 #1116)
#1118 := [refl]: #1117
#1113 := (not #747)
#1114 := (~ #1113 #744)
#1111 := (~ #744 #744)
#1109 := (~ #741 #741)
#1110 := [refl]: #1109
#1112 := [nnf-pos #1110]: #1111
#1115 := [nnf-neg #1112]: #1114
#1122 := [nnf-neg #1115 #1118]: #1121
#1105 := (~ #747 #1104)
#1106 := [sk]: #1105
#1126 := [nnf-neg #1106 #1122]: #1125
#1091 := (~ #1090 #1090)
#1092 := [refl]: #1091
#1088 := (~ #1087 #1087)
#1089 := [refl]: #1088
#1085 := (~ #1084 #1084)
#1086 := [refl]: #1085
#1137 := (~ #1136 #1136)
#1138 := [refl]: #1137
#1134 := (~ #1133 #1133)
#1135 := [refl]: #1134
#1131 := (~ #778 #778)
#1132 := [refl]: #1131
#991 := (~ #990 #990)
#992 := [refl]: #991
#1142 := [nnf-neg #992 #1132 #1135 #1138 #1086 #1089 #1092 #1126]: #1141
#1128 := (not #812)
#1129 := (~ #1128 #1127)
#1082 := (~ #1081 #1081)
#1083 := [refl]: #1082
#1079 := (~ #1078 #1078)
#1080 := [refl]: #1079
#1076 := (~ #1075 #1075)
#1077 := [refl]: #1076
#1073 := (~ #1072 #1072)
#1074 := [refl]: #1073
#1070 := (~ #772 #772)
#1071 := [refl]: #1070
#1130 := [nnf-neg #992 #1071 #1074 #1077 #1080 #1083 #1086 #1089 #1092 #1126]: #1129
#1146 := [nnf-neg #1130 #1142]: #1145
#1068 := (~ #686 #686)
#1069 := [refl]: #1068
#1150 := [nnf-neg #992 #1069 #1146]: #1149
#1065 := (not #707)
#1066 := (~ #1065 #1064)
#1061 := (not #678)
#1062 := (~ #1061 #1060)
#1057 := (not #675)
#1058 := (~ #1057 #1056)
#1051 := (not #672)
#1052 := (~ #1051 #1050)
#1053 := [sk]: #1052
#1035 := (not #661)
#1036 := (~ #1035 #1030)
#1031 := (~ #658 #1030)
#1032 := [sk]: #1031
#1037 := [nnf-neg #1032]: #1036
#1059 := [nnf-neg #1037 #1053]: #1058
#1018 := (~ #661 #1017)
#1015 := (~ #1014 #1014)
#1016 := [refl]: #1015
#1019 := [nnf-neg #1016]: #1018
#1063 := [nnf-neg #1019 #1059]: #1062
#1012 := (~ #1011 #1011)
#1013 := [refl]: #1012
#1009 := (~ #1008 #1008)
#1010 := [refl]: #1009
#1006 := (~ #1005 #1005)
#1007 := [refl]: #1006
#1003 := (~ #846 #846)
#1004 := [refl]: #1003
#1067 := [nnf-neg #992 #1004 #1007 #1010 #1013 #1063]: #1066
#1154 := [nnf-neg #1067 #1150]: #1153
#1001 := (~ #1000 #1000)
#1002 := [refl]: #1001
#997 := (not #892)
#998 := (~ #997 #889)
#995 := (~ #889 #889)
#993 := (~ #886 #886)
#994 := [refl]: #993
#996 := [nnf-pos #994]: #995
#999 := [nnf-neg #996]: #998
#988 := (~ #987 #987)
#989 := [refl]: #988
#1158 := [nnf-neg #989 #992 #999 #1002 #1154]: #1157
#985 := (~ #524 #524)
#986 := [refl]: #985
#1162 := [nnf-neg #986 #1158]: #1161
#982 := (not #628)
#983 := (~ #982 #625)
#980 := (~ #625 #625)
#978 := (~ #622 #622)
#979 := [refl]: #978
#981 := [nnf-pos #979]: #980
#984 := [nnf-neg #981]: #983
#1166 := [nnf-neg #984 #1162]: #1165
#974 := (~ #628 #973)
#975 := [sk]: #974
#1169 := [nnf-neg #975 #1166]: #1168
#958 := [not-or-elim #954]: #957
#1170 := [mp~ #958 #1169]: #1167
#1171 := [mp #1170 #1326]: #1324
#1601 := [mp #1171 #1600]: #1598
#2181 := [mp #1601 #2180]: #2178
#1676 := [unit-resolution #2181 #1868]: #2175
#1946 := (or #2172 #2166)
#1947 := [def-axiom]: #1946
#1672 := [unit-resolution #1947 #1676]: #2166
#1668 := (or #2169 #2163)
#1666 := (iff #13 #28)
#1677 := (iff #28 #13)
#1664 := [commutativity]: #1677
#1667 := [symm #1664]: #1666
#1665 := [mp #956 #1667]: #28
#1945 := (or #2169 #524 #2163)
#1941 := [def-axiom]: #1945
#2182 := [unit-resolution #1941 #1665]: #1668
#2183 := [unit-resolution #2182 #1672]: #2163
#1952 := (or #2160 #2154)
#1954 := [def-axiom]: #1952
#2263 := [unit-resolution #1954 #2183]: #2154
#2221 := [hypothesis]: #2107
#1769 := (or #2104 #2098)
#2043 := [def-axiom]: #1769
#2222 := [unit-resolution #2043 #2221]: #2098
#2058 := (not #2093)
#1669 := (or #2104 #46)
#2045 := [def-axiom]: #1669
#2223 := [unit-resolution #2045 #2221]: #46
#2256 := (or #2058 #221)
#2231 := (= #40 f11)
#2228 := (* -1::Int f7)
#2229 := (+ f3 #2228)
#2230 := (<= #2229 0::Int)
#2232 := (or #1470 #2230 #2231)
#1785 := (= f9 f11)
#2234 := [hypothesis]: #46
#2251 := [symm #2234]: #1785
#1973 := (or #2160 #41)
#1951 := [def-axiom]: #1973
#2235 := [unit-resolution #1951 #2183]: #41
#2252 := [trans #2235 #2251]: #2231
#2246 := (not #2231)
#2247 := (or #2232 #2246)
#2248 := [def-axiom]: #2247
#2253 := [unit-resolution #2248 #2252]: #2232
#2254 := [hypothesis]: #2093
#2233 := (not #2232)
#2236 := (or #2058 #2233)
#2237 := [quant-inst #29]: #2236
#2255 := [unit-resolution #2237 #2254 #2253]: false
#2257 := [lemma #2255]: #2256
#2224 := [unit-resolution #2257 #2223]: #2058
#1702 := (or #2101 #2093 #1459)
#2062 := [def-axiom]: #1702
#2225 := [unit-resolution #2062 #2224 #2222]: #1459
#1715 := (or #1458 #1039)
#1716 := [def-axiom]: #1715
#2226 := [unit-resolution #1716 #2225]: #1039
#1744 := (+ f8 #1040)
#1745 := (<= #1744 0::Int)
#1695 := (not #1745)
#1772 := (or #2104 #683)
#1773 := [def-axiom]: #1772
#2227 := [unit-resolution #1773 #2221]: #683
#1717 := (or #1458 #1043)
#2053 := [def-axiom]: #1717
#2210 := [unit-resolution #2053 #2225]: #1043
#1678 := (or #1695 #686 #1042)
#1691 := [hypothesis]: #1043
#1692 := [hypothesis]: #1745
#1694 := [hypothesis]: #683
#1690 := [th-lemma arith farkas -1 -1 1 #1694 #1692 #1691]: false
#1681 := [lemma #1690]: #1678
#2211 := [unit-resolution #1681 #2210 #2227]: #1695
#1721 := (+ f9 #1191)
#1722 := (>= #1721 0::Int)
#1680 := (not #1722)
#1787 := (+ f9 #664)
#1776 := (<= #1787 0::Int)
#2209 := [symm #2223]: #1785
#2212 := (not #1785)
#2213 := (or #2212 #1776)
#2214 := [th-lemma arith triangle-eq]: #2213
#2215 := [unit-resolution #2214 #2209]: #1776
#2054 := (not #1193)
#2055 := (or #1458 #2054)
#2056 := [def-axiom]: #2055
#2216 := [unit-resolution #2056 #2225]: #2054
#1688 := (not #1776)
#1673 := (or #1680 #1193 #1688)
#1682 := [hypothesis]: #1776
#1685 := [hypothesis]: #2054
#1686 := [hypothesis]: #1722
#1687 := [th-lemma arith farkas -1 1 1 #1686 #1685 #1682]: false
#1670 := [lemma #1687]: #1673
#2217 := [unit-resolution #1670 #2216 #2215]: #1680
#1707 := (or #1431 #1745 #1722)
#1671 := [hypothesis]: #1680
#1674 := [hypothesis]: #1695
#1675 := [hypothesis]: #1039
#1972 := (or #2160 #2085)
#1962 := [def-axiom]: #1972
#2184 := [unit-resolution #1962 #2183]: #2085
#1763 := (or #2090 #1431 #1745 #1722)
#1757 := (+ #1046 #881)
#1767 := (<= #1757 0::Int)
#1771 := (+ ?v0!2 #681)
#1781 := (>= #1771 0::Int)
#1734 := (or #1431 #1781 #1767)
#1764 := (or #2090 #1734)
#1683 := (iff #1764 #1763)
#1703 := (or #2090 #1707)
#1704 := (iff #1703 #1763)
#1679 := [rewrite]: #1704
#1698 := (iff #1764 #1703)
#1708 := (iff #1734 #1707)
#1724 := (iff #1767 #1722)
#1732 := (+ #881 #1046)
#1718 := (<= #1732 0::Int)
#1723 := (iff #1718 #1722)
#1712 := [rewrite]: #1723
#1719 := (iff #1767 #1718)
#1711 := (= #1757 #1732)
#1713 := [rewrite]: #1711
#1720 := [monotonicity #1713]: #1719
#1705 := [trans #1720 #1712]: #1724
#1729 := (iff #1781 #1745)
#1736 := (+ #681 ?v0!2)
#1741 := (>= #1736 0::Int)
#1735 := (iff #1741 #1745)
#1746 := [rewrite]: #1735
#1742 := (iff #1781 #1741)
#1737 := (= #1771 #1736)
#1728 := [rewrite]: #1737
#1743 := [monotonicity #1728]: #1742
#1731 := [trans #1743 #1746]: #1729
#1706 := [monotonicity #1731 #1705]: #1708
#1709 := [monotonicity #1706]: #1698
#1684 := [trans #1709 #1679]: #1683
#1700 := [quant-inst #1038]: #1764
#1689 := [mp #1700 #1684]: #1763
#2185 := [unit-resolution #1689 #2184 #1675 #1674 #1671]: false
#2186 := [lemma #2185]: #1707
#2241 := [unit-resolution #2186 #2217 #2211 #2226]: false
#2242 := [lemma #2241]: #2104
#1964 := (or #2157 #2107 #2151)
#1965 := [def-axiom]: #1964
#2261 := [unit-resolution #1965 #2242 #2263]: #2151
#1977 := (or #2148 #2142)
#1978 := [def-axiom]: #1977
#2427 := [unit-resolution #1978 #2261]: #2142
#2348 := (= #68 #1100)
#2362 := (not #2348)
#2349 := (+ #68 #1260)
#2351 := (>= #2349 0::Int)
#2356 := (not #2351)
#2250 := (+ #68 #736)
#2218 := (<= #2250 0::Int)
#2249 := (= #68 f15)
#2383 := (= f13 f15)
#2378 := [hypothesis]: #2133
#1859 := (or #2130 #76)
#2012 := [def-axiom]: #1859
#2379 := [unit-resolution #2012 #2378]: #76
#2384 := [symm #2379]: #2383
#2381 := (= #68 f13)
#2020 := (or #2130 #71)
#2027 := [def-axiom]: #2020
#2380 := [unit-resolution #2027 #2378]: #71
#2382 := [symm #2380]: #2381
#2385 := [trans #2382 #2384]: #2249
#2386 := (not #2249)
#2387 := (or #2386 #2218)
#2388 := [th-lemma arith triangle-eq]: #2387
#2389 := [unit-resolution #2388 #2385]: #2218
#2040 := (not #1262)
#1860 := (or #2130 #2124)
#2008 := [def-axiom]: #1860
#2390 := [unit-resolution #2008 #2378]: #2124
#2394 := (= #90 f13)
#2392 := (= #90 #68)
#1856 := (or #2130 #74)
#1858 := [def-axiom]: #1856
#2391 := [unit-resolution #1858 #2378]: #74
#2393 := [monotonicity #2391]: #2392
#2395 := [trans #2393 #2382]: #2394
#2396 := [trans #2395 #2384]: #91
#2032 := (or #2118 #1116)
#2028 := [def-axiom]: #2032
#2397 := [unit-resolution #2028 #2396]: #2118
#2023 := (or #2127 #1498 #2121)
#2024 := [def-axiom]: #2023
#2398 := [unit-resolution #2024 #2397 #2390]: #1498
#1755 := (or #1493 #2040)
#2037 := [def-axiom]: #1755
#2399 := [unit-resolution #2037 #2398]: #2040
#2357 := (not #2218)
#2358 := (or #2356 #1262 #2357)
#2352 := [hypothesis]: #2351
#2353 := [hypothesis]: #2218
#2354 := [hypothesis]: #2040
#2355 := [th-lemma arith farkas -1 -1 1 #2354 #2353 #2352]: false
#2359 := [lemma #2355]: #2358
#2400 := [unit-resolution #2359 #2399 #2389]: #2356
#2363 := (or #2362 #2351)
#2364 := [th-lemma arith triangle-eq]: #2363
#2401 := [unit-resolution #2364 #2400]: #2362
#2350 := (= f8 ?v0!3)
#2016 := (or #2130 #756)
#2014 := [def-axiom]: #2016
#2402 := [unit-resolution #2014 #2378]: #756
#2403 := (or #760 #1758)
#2404 := [th-lemma arith triangle-eq]: #2403
#2405 := [unit-resolution #2404 #2402]: #1758
#1761 := (or #1493 #1245)
#2039 := [def-axiom]: #1761
#2406 := [unit-resolution #2039 #2398]: #1245
#2407 := (not #1758)
#2408 := (or #2347 #1240 #2407)
#2409 := [th-lemma arith assign-bounds 1 1]: #2408
#2410 := [unit-resolution #2409 #2406 #2405]: #2347
#2326 := (+ f9 #1260)
#2327 := (>= #2326 0::Int)
#2412 := (not #2327)
#2025 := (or #2130 #772)
#2026 := [def-axiom]: #2025
#2411 := [unit-resolution #2026 #2378]: #772
#2413 := (or #2412 #1262 #2357 #773)
#2414 := [th-lemma arith assign-bounds 1 1 1]: #2413
#2415 := [unit-resolution #2414 #2399 #2389 #2411]: #2412
#2417 := (or #2315 #2327)
#1759 := (or #1493 #1094)
#1760 := [def-axiom]: #1759
#2416 := [unit-resolution #1760 #2398]: #1094
#2335 := (or #2090 #1478 #2315 #2327)
#2305 := (+ #1100 #881)
#2306 := (<= #2305 0::Int)
#2297 := (+ ?v0!3 #681)
#2298 := (>= #2297 0::Int)
#2307 := (or #1478 #2298 #2306)
#2336 := (or #2090 #2307)
#2343 := (iff #2336 #2335)
#2332 := (or #1478 #2315 #2327)
#2338 := (or #2090 #2332)
#2341 := (iff #2338 #2335)
#2342 := [rewrite]: #2341
#2339 := (iff #2336 #2338)
#2333 := (iff #2307 #2332)
#2330 := (iff #2306 #2327)
#2320 := (+ #881 #1100)
#2323 := (<= #2320 0::Int)
#2328 := (iff #2323 #2327)
#2329 := [rewrite]: #2328
#2324 := (iff #2306 #2323)
#2321 := (= #2305 #2320)
#2322 := [rewrite]: #2321
#2325 := [monotonicity #2322]: #2324
#2331 := [trans #2325 #2329]: #2330
#2318 := (iff #2298 #2315)
#2308 := (+ #681 ?v0!3)
#2311 := (>= #2308 0::Int)
#2316 := (iff #2311 #2315)
#2317 := [rewrite]: #2316
#2312 := (iff #2298 #2311)
#2309 := (= #2297 #2308)
#2310 := [rewrite]: #2309
#2313 := [monotonicity #2310]: #2312
#2319 := [trans #2313 #2317]: #2318
#2334 := [monotonicity #2319 #2331]: #2333
#2340 := [monotonicity #2334]: #2339
#2344 := [trans #2340 #2342]: #2343
#2337 := [quant-inst #1093]: #2336
#2345 := [mp #2337 #2344]: #2335
#2418 := [unit-resolution #2345 #2184 #2416]: #2417
#2419 := [unit-resolution #2418 #2415]: #2315
#2421 := (not #2347)
#2422 := (or #2350 #2420 #2421)
#2423 := [th-lemma arith triangle-eq]: #2422
#2424 := [unit-resolution #2423 #2419 #2410]: #2350
#2375 := (not #2350)
#2376 := (or #2375 #2348)
#2371 := (= #1100 #68)
#2369 := (= ?v0!3 f8)
#2368 := [hypothesis]: #2350
#2370 := [symm #2368]: #2369
#2372 := [monotonicity #2370]: #2371
#2373 := [symm #2372]: #2348
#2367 := [hypothesis]: #2362
#2374 := [unit-resolution #2367 #2373]: false
#2377 := [lemma #2374]: #2376
#2425 := [unit-resolution #2377 #2424 #2401]: false
#2426 := [lemma #2425]: #2130
#1984 := (or #2145 #2133 #2139)
#1985 := [def-axiom]: #1984
#2428 := [unit-resolution #1985 #2426 #2427]: #2139
#1991 := (or #2136 #756)
#2001 := [def-axiom]: #1991
#2429 := [unit-resolution #2001 #2428]: #756
#2430 := [unit-resolution #2404 #2429]: #1758
#1993 := (or #2136 #2124)
#1994 := [def-axiom]: #1993
#2431 := [unit-resolution #1994 #2428]: #2124
#1912 := (= f9 f15)
#1998 := (or #2136 #108)
#2000 := [def-axiom]: #1998
#2432 := [unit-resolution #2000 #2428]: #108
#2436 := [symm #2432]: #1912
#2437 := (= #90 f9)
#2434 := (= #90 #40)
#2007 := (or #2136 #107)
#2011 := [def-axiom]: #2007
#2433 := [unit-resolution #2011 #2428]: #107
#2435 := [monotonicity #2433]: #2434
#2438 := [trans #2435 #2235]: #2437
#2439 := [trans #2438 #2436]: #91
#2440 := [unit-resolution #2028 #2439]: #2118
#2441 := [unit-resolution #2024 #2440 #2431]: #1498
#2442 := [unit-resolution #2039 #2441]: #1245
#2443 := [unit-resolution #2409 #2442 #2430]: #2347
#1917 := (or #2136 #773)
#2010 := [def-axiom]: #1917
#2444 := [unit-resolution #2010 #2428]: #773
#1905 := (+ f9 #736)
#1913 := (<= #1905 0::Int)
#1808 := (or #395 #1912)
#1804 := (iff #108 #1912)
#1802 := (iff #1912 #108)
#1803 := [commutativity]: #1802
#1805 := [symm #1803]: #1804
#1801 := [hypothesis]: #108
#1806 := [mp #1801 #1805]: #1912
#1798 := (not #1912)
#1800 := [hypothesis]: #1798
#1807 := [unit-resolution #1800 #1806]: false
#1809 := [lemma #1807]: #1808
#2445 := [unit-resolution #1809 #2432]: #1912
#2446 := (or #1798 #1913)
#2447 := [th-lemma arith triangle-eq]: #2446
#2448 := [unit-resolution #2447 #2445]: #1913
#2449 := (not #1913)
#2450 := (or #2218 #772 #2449)
#2451 := [th-lemma arith assign-bounds 1 -1]: #2450
#2452 := [unit-resolution #2451 #2448 #2444]: #2218
#2453 := [unit-resolution #2037 #2441]: #2040
#2454 := [unit-resolution #2359 #2453 #2452]: #2356
#2455 := [unit-resolution #2364 #2454]: #2362
#2456 := [unit-resolution #2377 #2455]: #2375
#2457 := [unit-resolution #2423 #2456 #2443]: #2420
#2458 := (or #2412 #1262 #2449)
#2459 := [th-lemma arith assign-bounds -1 -1]: #2458
#2460 := [unit-resolution #2459 #2448 #2453]: #2412
#2461 := [unit-resolution #1760 #2441]: #1094
[unit-resolution #2345 #2184 #2461 #2460 #2457]: false
unsat