src/HOL/Boogie/Examples/Boogie_Max.certs

updated SMT certificates

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