7200427fdf70f253d4fd5c12f16bd6805d130a31 2229 0
#2 := false
#35 := 0::Int
decl f10 :: (-> Int Int)
#39 := (f10 0::Int)
#715 := -1::Int
#2156 := (* -1::Int #39)
decl f9 :: Int
#38 := f9
#2152 := (+ f9 #2156)
#2153 := (>= #2152 0::Int)
#40 := (= f9 #39)
decl f8 :: Int
#36 := f8
#1033 := (<= f8 0::Int)
decl f13 :: Int
#63 := f13
#990 := (* -1::Int f13)
#47 := (:var 0 Int)
#51 := (f10 #47)
#991 := (+ #51 #990)
#992 := (<= #991 0::Int)
decl f12 :: Int
#58 := f12
#785 := (* -1::Int f12)
#980 := (+ #47 #785)
#979 := (>= #980 0::Int)
#981 := (not #979)
#704 := (>= #47 0::Int)
#984 := (and #704 #981)
#987 := (not #984)
#995 := (or #987 #992)
#998 := (forall (vars (?v0 Int)) #995)
#1001 := (not #998)
#95 := (f10 f12)
#883 := (* -1::Int #95)
#884 := (+ f13 #883)
#882 := (>= #884 0::Int)
#881 := (not #882)
decl f18 :: Int
#100 := f18
#817 := (>= f18 0::Int)
#42 := 1::Int
#734 := (>= f12 1::Int)
#872 := (and #734 #817)
#875 := (not #872)
decl f20 :: Int
#106 := f20
#829 := (* -1::Int f20)
#866 := (+ f12 #829)
#865 := (= #866 -1::Int)
#869 := (not #865)
decl f19 :: Int
#102 := f19
#840 := (* -1::Int f19)
#841 := (+ #51 #840)
#842 := (<= #841 0::Int)
#830 := (+ #47 #829)
#828 := (>= #830 0::Int)
#831 := (not #828)
#834 := (and #704 #831)
#837 := (not #834)
#845 := (or #837 #842)
#848 := (forall (vars (?v0 Int)) #845)
#851 := (not #848)
#117 := (f10 f18)
#370 := (= f19 #117)
#857 := (or #370 #851)
#862 := (and #848 #857)
#109 := 2::Int
#820 := (>= f20 2::Int)
#822 := (and #817 #820)
#825 := (not #822)
decl f11 :: Int
#56 := f11
#731 := (>= f11 0::Int)
#736 := (and #731 #734)
#739 := (not #736)
#489 := (= f13 f19)
#495 := (not #489)
#486 := (= f11 f18)
#504 := (not #486)
#945 := (or #504 #495 #739 #825 #862 #869 #875 #881)
#878 := (not #734)
decl f17 :: Int
#97 := f17
#351 := (= f17 f19)
#429 := (not #351)
#348 := (= f12 f18)
#438 := (not #348)
#343 := (= #95 f17)
#456 := (not #343)
#921 := (or #456 #438 #429 #878 #739 #825 #862 #869 #875 #882)
#950 := (and #921 #945)
#786 := (+ f8 #785)
#787 := (<= #786 0::Int)
#971 := (or #739 #787 #950)
#790 := (not #787)
decl f15 :: Int
#72 := f15
#768 := (* -1::Int f15)
#769 := (+ #51 #768)
#770 := (<= #769 0::Int)
#742 := (* -1::Int #47)
#743 := (+ f8 #742)
#744 := (<= #743 0::Int)
#745 := (not #744)
#748 := (and #704 #745)
#751 := (not #748)
#773 := (or #751 #770)
#776 := (forall (vars (?v0 Int)) #773)
#78 := (= #51 f15)
#757 := (or #78 #751)
#762 := (exists (vars (?v0 Int)) #757)
#765 := (not #762)
#779 := (or #765 #776)
#782 := (and #762 #779)
decl f16 :: Int
#74 := f16
#248 := (= f12 f16)
#286 := (not #248)
#245 := (= f13 f15)
#295 := (not #245)
decl f14 :: Int
#70 := f14
#242 := (= f11 f14)
#304 := (not #242)
#811 := (or #304 #295 #286 #739 #782 #790)
#976 := (and #811 #971)
#67 := (f10 f11)
#239 := (= f13 #67)
#591 := (not #239)
#624 := (not #40)
#1019 := (or #624 #591 #739 #976 #1001)
#1024 := (and #40 #1019)
#718 := (* -1::Int #51)
#719 := (+ f9 #718)
#717 := (>= #719 0::Int)
#707 := (>= #47 1::Int)
#705 := (not #707)
#709 := (and #704 #705)
#712 := (not #709)
#721 := (or #712 #717)
#724 := (forall (vars (?v0 Int)) #721)
#727 := (not #724)
#1027 := (or #727 #1024)
#1030 := (and #724 #1027)
#1053 := (or #624 #1030 #1033)
#1058 := (not #1053)
#1 := true
#118 := (= #117 f19)
#119 := (and #118 true)
#114 := (<= #51 f19)
#112 := (< #47 f20)
#48 := (<= 0::Int #47)
#113 := (and #48 #112)
#115 := (implies #113 #114)
#116 := (forall (vars (?v0 Int)) #115)
#120 := (implies #116 #119)
#121 := (and #116 #120)
#110 := (<= 2::Int f20)
#104 := (<= 0::Int f18)
#111 := (and #104 #110)
#122 := (implies #111 #121)
#107 := (+ f12 1::Int)
#108 := (= f20 #107)
#123 := (implies #108 #122)
#59 := (<= 1::Int f12)
#105 := (and #104 #59)
#124 := (implies #105 #123)
#125 := (implies true #124)
#135 := (= f19 f13)
#136 := (implies #135 #125)
#134 := (= f18 f11)
#137 := (implies #134 #136)
#57 := (<= 0::Int f11)
#60 := (and #57 #59)
#138 := (implies #60 #137)
#133 := (<= #95 f13)
#139 := (implies #133 #138)
#140 := (implies #60 #139)
#141 := (implies true #140)
#103 := (= f19 f17)
#126 := (implies #103 #125)
#101 := (= f18 f12)
#127 := (implies #101 #126)
#99 := (and #59 #59)
#128 := (implies #99 #127)
#98 := (= f17 #95)
#129 := (implies #98 #128)
#96 := (< f13 #95)
#130 := (implies #96 #129)
#131 := (implies #60 #130)
#132 := (implies true #131)
#142 := (and #132 #141)
#143 := (implies #60 #142)
#94 := (< f12 f8)
#144 := (implies #94 #143)
#145 := (implies #60 #144)
#146 := (implies true #145)
#81 := (<= #51 f15)
#76 := (< #47 f8)
#77 := (and #48 #76)
#82 := (implies #77 #81)
#83 := (forall (vars (?v0 Int)) #82)
#84 := (and #83 true)
#79 := (implies #77 #78)
#80 := (exists (vars (?v0 Int)) #79)
#85 := (implies #80 #84)
#86 := (and #80 #85)
#75 := (= f16 f12)
#87 := (implies #75 #86)
#73 := (= f15 f13)
#88 := (implies #73 #87)
#71 := (= f14 f11)
#89 := (implies #71 #88)
#90 := (implies #60 #89)
#69 := (<= f8 f12)
#91 := (implies #69 #90)
#92 := (implies #60 #91)
#93 := (implies true #92)
#147 := (and #93 #146)
#148 := (implies #60 #147)
#68 := (= #67 f13)
#149 := (implies #68 #148)
#64 := (<= #51 f13)
#61 := (< #47 f12)
#62 := (and #48 #61)
#65 := (implies #62 #64)
#66 := (forall (vars (?v0 Int)) #65)
#150 := (implies #66 #149)
#151 := (implies #60 #150)
#152 := (implies true #151)
#55 := (= #39 f9)
#153 := (implies #55 #152)
#154 := (and #55 #153)
#52 := (<= #51 f9)
#49 := (< #47 1::Int)
#50 := (and #48 #49)
#53 := (implies #50 #52)
#54 := (forall (vars (?v0 Int)) #53)
#155 := (implies #54 #154)
#156 := (and #54 #155)
#43 := (<= 1::Int 1::Int)
#44 := (and #43 #43)
#41 := (<= 0::Int 0::Int)
#45 := (and #41 #44)
#46 := (and #41 #45)
#157 := (implies #46 #156)
#158 := (implies #40 #157)
#37 := (< 0::Int f8)
#159 := (implies #37 #158)
#160 := (implies true #159)
#161 := (not #160)
#1061 := (iff #161 #1058)
#363 := (not #113)
#364 := (or #363 #114)
#367 := (forall (vars (?v0 Int)) #364)
#383 := (not #367)
#384 := (or #383 #370)
#389 := (and #367 #384)
#395 := (not #111)
#396 := (or #395 #389)
#357 := (+ 1::Int f12)
#360 := (= f20 #357)
#404 := (not #360)
#405 := (or #404 #396)
#354 := (and #59 #104)
#413 := (not #354)
#414 := (or #413 #405)
#496 := (or #414 #495)
#505 := (or #504 #496)
#313 := (not #60)
#513 := (or #313 #505)
#521 := (not #133)
#522 := (or #521 #513)
#530 := (or #313 #522)
#430 := (or #429 #414)
#439 := (or #438 #430)
#447 := (not #59)
#448 := (or #447 #439)
#457 := (or #456 #448)
#465 := (not #96)
#466 := (or #465 #457)
#474 := (or #313 #466)
#542 := (and #474 #530)
#548 := (or #313 #542)
#556 := (not #94)
#557 := (or #556 #548)
#565 := (or #313 #557)
#251 := (not #77)
#258 := (or #251 #81)
#261 := (forall (vars (?v0 Int)) #258)
#252 := (or #251 #78)
#255 := (exists (vars (?v0 Int)) #252)
#274 := (not #255)
#275 := (or #274 #261)
#280 := (and #255 #275)
#287 := (or #286 #280)
#296 := (or #295 #287)
#305 := (or #304 #296)
#314 := (or #313 #305)
#322 := (not #69)
#323 := (or #322 #314)
#331 := (or #313 #323)
#577 := (and #331 #565)
#583 := (or #313 #577)
#592 := (or #591 #583)
#232 := (not #62)
#233 := (or #232 #64)
#236 := (forall (vars (?v0 Int)) #233)
#600 := (not #236)
#601 := (or #600 #592)
#609 := (or #313 #601)
#625 := (or #624 #609)
#630 := (and #40 #625)
#223 := (not #50)
#224 := (or #223 #52)
#227 := (forall (vars (?v0 Int)) #224)
#636 := (not #227)
#637 := (or #636 #630)
#642 := (and #227 #637)
#217 := (and #41 #43)
#220 := (and #41 #217)
#648 := (not #220)
#649 := (or #648 #642)
#657 := (or #624 #649)
#665 := (not #37)
#666 := (or #665 #657)
#678 := (not #666)
#1059 := (iff #678 #1058)
#1056 := (iff #666 #1053)
#1044 := (or false #1030)
#1047 := (or #624 #1044)
#1050 := (or #1033 #1047)
#1054 := (iff #1050 #1053)
#1055 := [rewrite]: #1054
#1051 := (iff #666 #1050)
#1048 := (iff #657 #1047)
#1045 := (iff #649 #1044)
#1031 := (iff #642 #1030)
#1028 := (iff #637 #1027)
#1025 := (iff #630 #1024)
#1022 := (iff #625 #1019)
#1004 := (or #739 #976)
#1007 := (or #591 #1004)
#1010 := (or #1001 #1007)
#1013 := (or #739 #1010)
#1016 := (or #624 #1013)
#1020 := (iff #1016 #1019)
#1021 := [rewrite]: #1020
#1017 := (iff #625 #1016)
#1014 := (iff #609 #1013)
#1011 := (iff #601 #1010)
#1008 := (iff #592 #1007)
#1005 := (iff #583 #1004)
#977 := (iff #577 #976)
#974 := (iff #565 #971)
#962 := (or #739 #950)
#965 := (or #787 #962)
#968 := (or #739 #965)
#972 := (iff #968 #971)
#973 := [rewrite]: #972
#969 := (iff #565 #968)
#966 := (iff #557 #965)
#963 := (iff #548 #962)
#951 := (iff #542 #950)
#948 := (iff #530 #945)
#894 := (or #825 #862)
#897 := (or #869 #894)
#900 := (or #875 #897)
#930 := (or #900 #495)
#933 := (or #504 #930)
#936 := (or #739 #933)
#939 := (or #881 #936)
#942 := (or #739 #939)
#946 := (iff #942 #945)
#947 := [rewrite]: #946
#943 := (iff #530 #942)
#940 := (iff #522 #939)
#937 := (iff #513 #936)
#934 := (iff #505 #933)
#931 := (iff #496 #930)
#901 := (iff #414 #900)
#898 := (iff #405 #897)
#895 := (iff #396 #894)
#863 := (iff #389 #862)
#860 := (iff #384 #857)
#854 := (or #851 #370)
#858 := (iff #854 #857)
#859 := [rewrite]: #858
#855 := (iff #384 #854)
#852 := (iff #383 #851)
#849 := (iff #367 #848)
#846 := (iff #364 #845)
#843 := (iff #114 #842)
#844 := [rewrite]: #843
#838 := (iff #363 #837)
#835 := (iff #113 #834)
#832 := (iff #112 #831)
#833 := [rewrite]: #832
#702 := (iff #48 #704)
#703 := [rewrite]: #702
#836 := [monotonicity #703 #833]: #835
#839 := [monotonicity #836]: #838
#847 := [monotonicity #839 #844]: #846
#850 := [quant-intro #847]: #849
#853 := [monotonicity #850]: #852
#856 := [monotonicity #853]: #855
#861 := [trans #856 #859]: #860
#864 := [monotonicity #850 #861]: #863
#826 := (iff #395 #825)
#823 := (iff #111 #822)
#819 := (iff #110 #820)
#821 := [rewrite]: #819
#816 := (iff #104 #817)
#818 := [rewrite]: #816
#824 := [monotonicity #818 #821]: #823
#827 := [monotonicity #824]: #826
#896 := [monotonicity #827 #864]: #895
#870 := (iff #404 #869)
#867 := (iff #360 #865)
#868 := [rewrite]: #867
#871 := [monotonicity #868]: #870
#899 := [monotonicity #871 #896]: #898
#876 := (iff #413 #875)
#873 := (iff #354 #872)
#733 := (iff #59 #734)
#735 := [rewrite]: #733
#874 := [monotonicity #735 #818]: #873
#877 := [monotonicity #874]: #876
#902 := [monotonicity #877 #899]: #901
#932 := [monotonicity #902]: #931
#935 := [monotonicity #932]: #934
#740 := (iff #313 #739)
#737 := (iff #60 #736)
#730 := (iff #57 #731)
#732 := [rewrite]: #730
#738 := [monotonicity #732 #735]: #737
#741 := [monotonicity #738]: #740
#938 := [monotonicity #741 #935]: #937
#928 := (iff #521 #881)
#926 := (iff #133 #882)
#927 := [rewrite]: #926
#929 := [monotonicity #927]: #928
#941 := [monotonicity #929 #938]: #940
#944 := [monotonicity #741 #941]: #943
#949 := [trans #944 #947]: #948
#924 := (iff #474 #921)
#903 := (or #429 #900)
#906 := (or #438 #903)
#909 := (or #878 #906)
#912 := (or #456 #909)
#915 := (or #882 #912)
#918 := (or #739 #915)
#922 := (iff #918 #921)
#923 := [rewrite]: #922
#919 := (iff #474 #918)
#916 := (iff #466 #915)
#913 := (iff #457 #912)
#910 := (iff #448 #909)
#907 := (iff #439 #906)
#904 := (iff #430 #903)
#905 := [monotonicity #902]: #904
#908 := [monotonicity #905]: #907
#879 := (iff #447 #878)
#880 := [monotonicity #735]: #879
#911 := [monotonicity #880 #908]: #910
#914 := [monotonicity #911]: #913
#892 := (iff #465 #882)
#887 := (not #881)
#890 := (iff #887 #882)
#891 := [rewrite]: #890
#888 := (iff #465 #887)
#885 := (iff #96 #881)
#886 := [rewrite]: #885
#889 := [monotonicity #886]: #888
#893 := [trans #889 #891]: #892
#917 := [monotonicity #893 #914]: #916
#920 := [monotonicity #741 #917]: #919
#925 := [trans #920 #923]: #924
#952 := [monotonicity #925 #949]: #951
#964 := [monotonicity #741 #952]: #963
#960 := (iff #556 #787)
#955 := (not #790)
#958 := (iff #955 #787)
#959 := [rewrite]: #958
#956 := (iff #556 #955)
#953 := (iff #94 #790)
#954 := [rewrite]: #953
#957 := [monotonicity #954]: #956
#961 := [trans #957 #959]: #960
#967 := [monotonicity #961 #964]: #966
#970 := [monotonicity #741 #967]: #969
#975 := [trans #970 #973]: #974
#814 := (iff #331 #811)
#793 := (or #286 #782)
#796 := (or #295 #793)
#799 := (or #304 #796)
#802 := (or #739 #799)
#805 := (or #790 #802)
#808 := (or #739 #805)
#812 := (iff #808 #811)
#813 := [rewrite]: #812
#809 := (iff #331 #808)
#806 := (iff #323 #805)
#803 := (iff #314 #802)
#800 := (iff #305 #799)
#797 := (iff #296 #796)
#794 := (iff #287 #793)
#783 := (iff #280 #782)
#780 := (iff #275 #779)
#777 := (iff #261 #776)
#774 := (iff #258 #773)
#771 := (iff #81 #770)
#772 := [rewrite]: #771
#752 := (iff #251 #751)
#749 := (iff #77 #748)
#746 := (iff #76 #745)
#747 := [rewrite]: #746
#750 := [monotonicity #703 #747]: #749
#753 := [monotonicity #750]: #752
#775 := [monotonicity #753 #772]: #774
#778 := [quant-intro #775]: #777
#766 := (iff #274 #765)
#763 := (iff #255 #762)
#760 := (iff #252 #757)
#754 := (or #751 #78)
#758 := (iff #754 #757)
#759 := [rewrite]: #758
#755 := (iff #252 #754)
#756 := [monotonicity #753]: #755
#761 := [trans #756 #759]: #760
#764 := [quant-intro #761]: #763
#767 := [monotonicity #764]: #766
#781 := [monotonicity #767 #778]: #780
#784 := [monotonicity #764 #781]: #783
#795 := [monotonicity #784]: #794
#798 := [monotonicity #795]: #797
#801 := [monotonicity #798]: #800
#804 := [monotonicity #741 #801]: #803
#791 := (iff #322 #790)
#788 := (iff #69 #787)
#789 := [rewrite]: #788
#792 := [monotonicity #789]: #791
#807 := [monotonicity #792 #804]: #806
#810 := [monotonicity #741 #807]: #809
#815 := [trans #810 #813]: #814
#978 := [monotonicity #815 #975]: #977
#1006 := [monotonicity #741 #978]: #1005
#1009 := [monotonicity #1006]: #1008
#1002 := (iff #600 #1001)
#999 := (iff #236 #998)
#996 := (iff #233 #995)
#993 := (iff #64 #992)
#994 := [rewrite]: #993
#988 := (iff #232 #987)
#985 := (iff #62 #984)
#982 := (iff #61 #981)
#983 := [rewrite]: #982
#986 := [monotonicity #703 #983]: #985
#989 := [monotonicity #986]: #988
#997 := [monotonicity #989 #994]: #996
#1000 := [quant-intro #997]: #999
#1003 := [monotonicity #1000]: #1002
#1012 := [monotonicity #1003 #1009]: #1011
#1015 := [monotonicity #741 #1012]: #1014
#1018 := [monotonicity #1015]: #1017
#1023 := [trans #1018 #1021]: #1022
#1026 := [monotonicity #1023]: #1025
#728 := (iff #636 #727)
#725 := (iff #227 #724)
#722 := (iff #224 #721)
#716 := (iff #52 #717)
#720 := [rewrite]: #716
#713 := (iff #223 #712)
#710 := (iff #50 #709)
#706 := (iff #49 #705)
#708 := [rewrite]: #706
#711 := [monotonicity #703 #708]: #710
#714 := [monotonicity #711]: #713
#723 := [monotonicity #714 #720]: #722
#726 := [quant-intro #723]: #725
#729 := [monotonicity #726]: #728
#1029 := [monotonicity #729 #1026]: #1028
#1032 := [monotonicity #726 #1029]: #1031
#700 := (iff #648 false)
#695 := (not true)
#698 := (iff #695 false)
#699 := [rewrite]: #698
#696 := (iff #648 #695)
#693 := (iff #220 true)
#685 := (and true true)
#688 := (and true #685)
#691 := (iff #688 true)
#692 := [rewrite]: #691
#689 := (iff #220 #688)
#686 := (iff #217 #685)
#683 := (iff #43 true)
#684 := [rewrite]: #683
#681 := (iff #41 true)
#682 := [rewrite]: #681
#687 := [monotonicity #682 #684]: #686
#690 := [monotonicity #682 #687]: #689
#694 := [trans #690 #692]: #693
#697 := [monotonicity #694]: #696
#701 := [trans #697 #699]: #700
#1046 := [monotonicity #701 #1032]: #1045
#1049 := [monotonicity #1046]: #1048
#1042 := (iff #665 #1033)
#1034 := (not #1033)
#1037 := (not #1034)
#1040 := (iff #1037 #1033)
#1041 := [rewrite]: #1040
#1038 := (iff #665 #1037)
#1035 := (iff #37 #1034)
#1036 := [rewrite]: #1035
#1039 := [monotonicity #1036]: #1038
#1043 := [trans #1039 #1041]: #1042
#1052 := [monotonicity #1043 #1049]: #1051
#1057 := [trans #1052 #1055]: #1056
#1060 := [monotonicity #1057]: #1059
#679 := (iff #161 #678)
#676 := (iff #160 #666)
#671 := (implies true #666)
#674 := (iff #671 #666)
#675 := [rewrite]: #674
#672 := (iff #160 #671)
#669 := (iff #159 #666)
#662 := (implies #37 #657)
#667 := (iff #662 #666)
#668 := [rewrite]: #667
#663 := (iff #159 #662)
#660 := (iff #158 #657)
#654 := (implies #40 #649)
#658 := (iff #654 #657)
#659 := [rewrite]: #658
#655 := (iff #158 #654)
#652 := (iff #157 #649)
#645 := (implies #220 #642)
#650 := (iff #645 #649)
#651 := [rewrite]: #650
#646 := (iff #157 #645)
#643 := (iff #156 #642)
#640 := (iff #155 #637)
#633 := (implies #227 #630)
#638 := (iff #633 #637)
#639 := [rewrite]: #638
#634 := (iff #155 #633)
#631 := (iff #154 #630)
#628 := (iff #153 #625)
#621 := (implies #40 #609)
#626 := (iff #621 #625)
#627 := [rewrite]: #626
#622 := (iff #153 #621)
#619 := (iff #152 #609)
#614 := (implies true #609)
#617 := (iff #614 #609)
#618 := [rewrite]: #617
#615 := (iff #152 #614)
#612 := (iff #151 #609)
#606 := (implies #60 #601)
#610 := (iff #606 #609)
#611 := [rewrite]: #610
#607 := (iff #151 #606)
#604 := (iff #150 #601)
#597 := (implies #236 #592)
#602 := (iff #597 #601)
#603 := [rewrite]: #602
#598 := (iff #150 #597)
#595 := (iff #149 #592)
#588 := (implies #239 #583)
#593 := (iff #588 #592)
#594 := [rewrite]: #593
#589 := (iff #149 #588)
#586 := (iff #148 #583)
#580 := (implies #60 #577)
#584 := (iff #580 #583)
#585 := [rewrite]: #584
#581 := (iff #148 #580)
#578 := (iff #147 #577)
#575 := (iff #146 #565)
#570 := (implies true #565)
#573 := (iff #570 #565)
#574 := [rewrite]: #573
#571 := (iff #146 #570)
#568 := (iff #145 #565)
#562 := (implies #60 #557)
#566 := (iff #562 #565)
#567 := [rewrite]: #566
#563 := (iff #145 #562)
#560 := (iff #144 #557)
#553 := (implies #94 #548)
#558 := (iff #553 #557)
#559 := [rewrite]: #558
#554 := (iff #144 #553)
#551 := (iff #143 #548)
#545 := (implies #60 #542)
#549 := (iff #545 #548)
#550 := [rewrite]: #549
#546 := (iff #143 #545)
#543 := (iff #142 #542)
#540 := (iff #141 #530)
#535 := (implies true #530)
#538 := (iff #535 #530)
#539 := [rewrite]: #538
#536 := (iff #141 #535)
#533 := (iff #140 #530)
#527 := (implies #60 #522)
#531 := (iff #527 #530)
#532 := [rewrite]: #531
#528 := (iff #140 #527)
#525 := (iff #139 #522)
#518 := (implies #133 #513)
#523 := (iff #518 #522)
#524 := [rewrite]: #523
#519 := (iff #139 #518)
#516 := (iff #138 #513)
#510 := (implies #60 #505)
#514 := (iff #510 #513)
#515 := [rewrite]: #514
#511 := (iff #138 #510)
#508 := (iff #137 #505)
#501 := (implies #486 #496)
#506 := (iff #501 #505)
#507 := [rewrite]: #506
#502 := (iff #137 #501)
#499 := (iff #136 #496)
#492 := (implies #489 #414)
#497 := (iff #492 #496)
#498 := [rewrite]: #497
#493 := (iff #136 #492)
#424 := (iff #125 #414)
#419 := (implies true #414)
#422 := (iff #419 #414)
#423 := [rewrite]: #422
#420 := (iff #125 #419)
#417 := (iff #124 #414)
#410 := (implies #354 #405)
#415 := (iff #410 #414)
#416 := [rewrite]: #415
#411 := (iff #124 #410)
#408 := (iff #123 #405)
#401 := (implies #360 #396)
#406 := (iff #401 #405)
#407 := [rewrite]: #406
#402 := (iff #123 #401)
#399 := (iff #122 #396)
#392 := (implies #111 #389)
#397 := (iff #392 #396)
#398 := [rewrite]: #397
#393 := (iff #122 #392)
#390 := (iff #121 #389)
#387 := (iff #120 #384)
#380 := (implies #367 #370)
#385 := (iff #380 #384)
#386 := [rewrite]: #385
#381 := (iff #120 #380)
#378 := (iff #119 #370)
#373 := (and #370 true)
#376 := (iff #373 #370)
#377 := [rewrite]: #376
#374 := (iff #119 #373)
#371 := (iff #118 #370)
#372 := [rewrite]: #371
#375 := [monotonicity #372]: #374
#379 := [trans #375 #377]: #378
#368 := (iff #116 #367)
#365 := (iff #115 #364)
#366 := [rewrite]: #365
#369 := [quant-intro #366]: #368
#382 := [monotonicity #369 #379]: #381
#388 := [trans #382 #386]: #387
#391 := [monotonicity #369 #388]: #390
#394 := [monotonicity #391]: #393
#400 := [trans #394 #398]: #399
#361 := (iff #108 #360)
#358 := (= #107 #357)
#359 := [rewrite]: #358
#362 := [monotonicity #359]: #361
#403 := [monotonicity #362 #400]: #402
#409 := [trans #403 #407]: #408
#355 := (iff #105 #354)
#356 := [rewrite]: #355
#412 := [monotonicity #356 #409]: #411
#418 := [trans #412 #416]: #417
#421 := [monotonicity #418]: #420
#425 := [trans #421 #423]: #424
#490 := (iff #135 #489)
#491 := [rewrite]: #490
#494 := [monotonicity #491 #425]: #493
#500 := [trans #494 #498]: #499
#487 := (iff #134 #486)
#488 := [rewrite]: #487
#503 := [monotonicity #488 #500]: #502
#509 := [trans #503 #507]: #508
#512 := [monotonicity #509]: #511
#517 := [trans #512 #515]: #516
#520 := [monotonicity #517]: #519
#526 := [trans #520 #524]: #525
#529 := [monotonicity #526]: #528
#534 := [trans #529 #532]: #533
#537 := [monotonicity #534]: #536
#541 := [trans #537 #539]: #540
#484 := (iff #132 #474)
#479 := (implies true #474)
#482 := (iff #479 #474)
#483 := [rewrite]: #482
#480 := (iff #132 #479)
#477 := (iff #131 #474)
#471 := (implies #60 #466)
#475 := (iff #471 #474)
#476 := [rewrite]: #475
#472 := (iff #131 #471)
#469 := (iff #130 #466)
#462 := (implies #96 #457)
#467 := (iff #462 #466)
#468 := [rewrite]: #467
#463 := (iff #130 #462)
#460 := (iff #129 #457)
#453 := (implies #343 #448)
#458 := (iff #453 #457)
#459 := [rewrite]: #458
#454 := (iff #129 #453)
#451 := (iff #128 #448)
#444 := (implies #59 #439)
#449 := (iff #444 #448)
#450 := [rewrite]: #449
#445 := (iff #128 #444)
#442 := (iff #127 #439)
#435 := (implies #348 #430)
#440 := (iff #435 #439)
#441 := [rewrite]: #440
#436 := (iff #127 #435)
#433 := (iff #126 #430)
#426 := (implies #351 #414)
#431 := (iff #426 #430)
#432 := [rewrite]: #431
#427 := (iff #126 #426)
#352 := (iff #103 #351)
#353 := [rewrite]: #352
#428 := [monotonicity #353 #425]: #427
#434 := [trans #428 #432]: #433
#349 := (iff #101 #348)
#350 := [rewrite]: #349
#437 := [monotonicity #350 #434]: #436
#443 := [trans #437 #441]: #442
#346 := (iff #99 #59)
#347 := [rewrite]: #346
#446 := [monotonicity #347 #443]: #445
#452 := [trans #446 #450]: #451
#344 := (iff #98 #343)
#345 := [rewrite]: #344
#455 := [monotonicity #345 #452]: #454
#461 := [trans #455 #459]: #460
#464 := [monotonicity #461]: #463
#470 := [trans #464 #468]: #469
#473 := [monotonicity #470]: #472
#478 := [trans #473 #476]: #477
#481 := [monotonicity #478]: #480
#485 := [trans #481 #483]: #484
#544 := [monotonicity #485 #541]: #543
#547 := [monotonicity #544]: #546
#552 := [trans #547 #550]: #551
#555 := [monotonicity #552]: #554
#561 := [trans #555 #559]: #560
#564 := [monotonicity #561]: #563
#569 := [trans #564 #567]: #568
#572 := [monotonicity #569]: #571
#576 := [trans #572 #574]: #575
#341 := (iff #93 #331)
#336 := (implies true #331)
#339 := (iff #336 #331)
#340 := [rewrite]: #339
#337 := (iff #93 #336)
#334 := (iff #92 #331)
#328 := (implies #60 #323)
#332 := (iff #328 #331)
#333 := [rewrite]: #332
#329 := (iff #92 #328)
#326 := (iff #91 #323)
#319 := (implies #69 #314)
#324 := (iff #319 #323)
#325 := [rewrite]: #324
#320 := (iff #91 #319)
#317 := (iff #90 #314)
#310 := (implies #60 #305)
#315 := (iff #310 #314)
#316 := [rewrite]: #315
#311 := (iff #90 #310)
#308 := (iff #89 #305)
#301 := (implies #242 #296)
#306 := (iff #301 #305)
#307 := [rewrite]: #306
#302 := (iff #89 #301)
#299 := (iff #88 #296)
#292 := (implies #245 #287)
#297 := (iff #292 #296)
#298 := [rewrite]: #297
#293 := (iff #88 #292)
#290 := (iff #87 #287)
#283 := (implies #248 #280)
#288 := (iff #283 #287)
#289 := [rewrite]: #288
#284 := (iff #87 #283)
#281 := (iff #86 #280)
#278 := (iff #85 #275)
#271 := (implies #255 #261)
#276 := (iff #271 #275)
#277 := [rewrite]: #276
#272 := (iff #85 #271)
#269 := (iff #84 #261)
#264 := (and #261 true)
#267 := (iff #264 #261)
#268 := [rewrite]: #267
#265 := (iff #84 #264)
#262 := (iff #83 #261)
#259 := (iff #82 #258)
#260 := [rewrite]: #259
#263 := [quant-intro #260]: #262
#266 := [monotonicity #263]: #265
#270 := [trans #266 #268]: #269
#256 := (iff #80 #255)
#253 := (iff #79 #252)
#254 := [rewrite]: #253
#257 := [quant-intro #254]: #256
#273 := [monotonicity #257 #270]: #272
#279 := [trans #273 #277]: #278
#282 := [monotonicity #257 #279]: #281
#249 := (iff #75 #248)
#250 := [rewrite]: #249
#285 := [monotonicity #250 #282]: #284
#291 := [trans #285 #289]: #290
#246 := (iff #73 #245)
#247 := [rewrite]: #246
#294 := [monotonicity #247 #291]: #293
#300 := [trans #294 #298]: #299
#243 := (iff #71 #242)
#244 := [rewrite]: #243
#303 := [monotonicity #244 #300]: #302
#309 := [trans #303 #307]: #308
#312 := [monotonicity #309]: #311
#318 := [trans #312 #316]: #317
#321 := [monotonicity #318]: #320
#327 := [trans #321 #325]: #326
#330 := [monotonicity #327]: #329
#335 := [trans #330 #333]: #334
#338 := [monotonicity #335]: #337
#342 := [trans #338 #340]: #341
#579 := [monotonicity #342 #576]: #578
#582 := [monotonicity #579]: #581
#587 := [trans #582 #585]: #586
#240 := (iff #68 #239)
#241 := [rewrite]: #240
#590 := [monotonicity #241 #587]: #589
#596 := [trans #590 #594]: #595
#237 := (iff #66 #236)
#234 := (iff #65 #233)
#235 := [rewrite]: #234
#238 := [quant-intro #235]: #237
#599 := [monotonicity #238 #596]: #598
#605 := [trans #599 #603]: #604
#608 := [monotonicity #605]: #607
#613 := [trans #608 #611]: #612
#616 := [monotonicity #613]: #615
#620 := [trans #616 #618]: #619
#230 := (iff #55 #40)
#231 := [rewrite]: #230
#623 := [monotonicity #231 #620]: #622
#629 := [trans #623 #627]: #628
#632 := [monotonicity #231 #629]: #631
#228 := (iff #54 #227)
#225 := (iff #53 #224)
#226 := [rewrite]: #225
#229 := [quant-intro #226]: #228
#635 := [monotonicity #229 #632]: #634
#641 := [trans #635 #639]: #640
#644 := [monotonicity #229 #641]: #643
#221 := (iff #46 #220)
#218 := (iff #45 #217)
#215 := (iff #44 #43)
#216 := [rewrite]: #215
#219 := [monotonicity #216]: #218
#222 := [monotonicity #219]: #221
#647 := [monotonicity #222 #644]: #646
#653 := [trans #647 #651]: #652
#656 := [monotonicity #653]: #655
#661 := [trans #656 #659]: #660
#664 := [monotonicity #661]: #663
#670 := [trans #664 #668]: #669
#673 := [monotonicity #670]: #672
#677 := [trans #673 #675]: #676
#680 := [monotonicity #677]: #679
#1062 := [trans #680 #1060]: #1061
#213 := [asserted]: #161
#1063 := [mp #213 #1062]: #1058
#1064 := [not-or-elim #1063]: #40
#2168 := (or #624 #2153)
#2145 := [th-lemma arith triangle-eq]: #2168
#2038 := [unit-resolution #2145 #1064]: #2153
decl ?v0!0 :: Int
#1130 := ?v0!0
#1131 := (f10 ?v0!0)
#1132 := (* -1::Int #1131)
#1133 := (+ f9 #1132)
#1134 := (>= #1133 0::Int)
#1882 := (not #1134)
#1137 := (>= ?v0!0 0::Int)
#1144 := (not #1137)
#1135 := (>= ?v0!0 1::Int)
#1520 := (or #1134 #1135 #1144)
#1525 := (not #1520)
decl ?v0!1 :: Int
#1174 := ?v0!1
#1182 := (f10 ?v0!1)
#1355 := (= f15 #1182)
#1179 := (>= ?v0!1 0::Int)
#1598 := (not #1179)
#1175 := (* -1::Int ?v0!1)
#1176 := (+ f8 #1175)
#1177 := (<= #1176 0::Int)
#1613 := (or #1177 #1598 #1355)
#1644 := (not #1613)
decl ?v0!2 :: Int
#1192 := ?v0!2
#1193 := (f10 ?v0!2)
#1379 := (* -1::Int #1193)
#1380 := (+ f15 #1379)
#1381 := (>= #1380 0::Int)
#1200 := (>= ?v0!2 0::Int)
#1618 := (not #1200)
#1196 := (* -1::Int ?v0!2)
#1197 := (+ f8 #1196)
#1198 := (<= #1197 0::Int)
#1775 := (or #1198 #1618 #1381 #1644)
#1778 := (not #1775)
#2331 := (pattern #51)
#1528 := (not #704)
#1587 := (or #78 #1528 #744)
#1592 := (not #1587)
#2392 := (forall (vars (?v0 Int)) (:pat #2331) #1592)
#2397 := (or #2392 #1778)
#2400 := (not #2397)
#1657 := (not #731)
#2403 := (or #304 #295 #286 #1657 #878 #790 #2400)
#2406 := (not #2403)
decl ?v0!3 :: Int
#1241 := ?v0!3
#1242 := (f10 ?v0!3)
#1444 := (* -1::Int #1242)
#1445 := (+ f19 #1444)
#1446 := (>= #1445 0::Int)
#1422 := (* -1::Int ?v0!3)
#1423 := (+ f20 #1422)
#1424 := (<= #1423 0::Int)
#1248 := (>= ?v0!3 0::Int)
#1697 := (not #1248)
#1712 := (or #1697 #1424 #1446)
#1717 := (not #1712)
#1679 := (or #1528 #828 #842)
#2348 := (forall (vars (?v0 Int)) (:pat #2331) #1679)
#2353 := (not #2348)
#2356 := (or #370 #2353)
#2359 := (not #2356)
#2362 := (or #2359 #1717)
#2365 := (not #2362)
#1727 := (not #820)
#1726 := (not #817)
#2374 := (or #504 #495 #1657 #878 #1726 #1727 #869 #881 #2365)
#2377 := (not #2374)
#2368 := (or #456 #438 #429 #1657 #878 #1726 #1727 #869 #882 #2365)
#2371 := (not #2368)
#2380 := (or #2371 #2377)
#2383 := (not #2380)
#2386 := (or #1657 #878 #787 #2383)
#2389 := (not #2386)
#2409 := (or #2389 #2406)
#2412 := (not #2409)
#1565 := (or #1528 #979 #992)
#2340 := (forall (vars (?v0 Int)) (:pat #2331) #1565)
#2345 := (not #2340)
#1543 := (or #1528 #707 #717)
#2332 := (forall (vars (?v0 Int)) (:pat #2331) #1543)
#2337 := (not #2332)
#2415 := (or #591 #1657 #878 #2337 #2345 #2412)
#2745 := (+ #95 #1444)
#2747 := (>= #2745 0::Int)
#2744 := (= #95 #1242)
#2623 := (= f12 ?v0!3)
#2548 := (+ f12 #1422)
#2549 := (<= #2548 0::Int)
#2560 := (+ f13 #1444)
#2561 := (>= #2560 0::Int)
#2664 := (not #2561)
#2293 := (not #1446)
#2418 := (not #2415)
#2748 := [hypothesis]: #2418
#2195 := (or #2415 #2409)
#2197 := [def-axiom]: #2195
#2749 := [unit-resolution #2197 #2748]: #2409
#2208 := (or #2415 #2340)
#2194 := [def-axiom]: #2208
#2750 := [unit-resolution #2194 #2748]: #2340
#2217 := (or #2415 #239)
#2201 := [def-axiom]: #2217
#2751 := [unit-resolution #2201 #2748]: #239
#2492 := (or #2403 #591 #2345)
#2432 := (f10 f14)
#2436 := (= f15 #2432)
#2486 := (= #67 #2432)
#2484 := (= #2432 #67)
#2469 := [hypothesis]: #2406
#2134 := (or #2403 #242)
#2135 := [def-axiom]: #2134
#2480 := [unit-resolution #2135 #2469]: #242
#2481 := [symm #2480]: #71
#2485 := [monotonicity #2481]: #2484
#2487 := [symm #2485]: #2486
#2488 := (= f15 #67)
#2482 := [hypothesis]: #239
#2136 := (or #2403 #245)
#2137 := [def-axiom]: #2136
#2472 := [unit-resolution #2137 #2469]: #245
#2483 := [symm #2472]: #73
#2489 := [trans #2483 #2482]: #2488
#2490 := [trans #2489 #2487]: #2436
#2464 := (not #2436)
#2430 := (>= f14 0::Int)
#2431 := (not #2430)
#2427 := (* -1::Int f14)
#2428 := (+ f8 #2427)
#2429 := (<= #2428 0::Int)
#2442 := (or #2429 #2431 #2436)
#2447 := (not #2442)
#2221 := (or #2403 #2397)
#2222 := [def-axiom]: #2221
#2470 := [unit-resolution #2222 #2469]: #2397
#2209 := (or #2403 #787)
#2211 := [def-axiom]: #2209
#2471 := [unit-resolution #2211 #2469]: #787
#1944 := [hypothesis]: #2340
#2055 := (+ f13 #768)
#2056 := (<= #2055 0::Int)
#2473 := (or #295 #2056)
#2474 := [th-lemma arith triangle-eq]: #2473
#2475 := [unit-resolution #2474 #2472]: #2056
#1951 := (not #2056)
#1917 := (or #1775 #1951 #2345 #790)
#1957 := [hypothesis]: #2056
#2024 := (+ f13 #1379)
#2025 := (>= #2024 0::Int)
#2045 := (+ f12 #1196)
#2046 := (<= #2045 0::Int)
#1940 := (not #2046)
#1933 := [hypothesis]: #787
#1199 := (not #1198)
#1938 := [hypothesis]: #1778
#2236 := (or #1775 #1199)
#2234 := [def-axiom]: #2236
#1939 := [unit-resolution #2234 #1938]: #1199
#1941 := (or #1940 #790 #1198)
#1942 := [th-lemma arith assign-bounds 1 -1]: #1941
#1943 := [unit-resolution #1942 #1939 #1933]: #1940
#1925 := (or #2025 #2046)
#2237 := (or #1775 #1200)
#2119 := [def-axiom]: #2237
#1932 := [unit-resolution #2119 #1938]: #1200
#2014 := (or #2345 #1618 #2025 #2046)
#2057 := (+ #1193 #990)
#2047 := (<= #2057 0::Int)
#2037 := (+ ?v0!2 #785)
#2039 := (>= #2037 0::Int)
#2040 := (or #1618 #2039 #2047)
#2015 := (or #2345 #2040)
#2006 := (iff #2015 #2014)
#2008 := (or #1618 #2025 #2046)
#2009 := (or #2345 #2008)
#2003 := (iff #2009 #2014)
#2004 := [rewrite]: #2003
#2017 := (iff #2015 #2009)
#2012 := (iff #2040 #2008)
#2030 := (or #1618 #2046 #2025)
#2010 := (iff #2030 #2008)
#2011 := [rewrite]: #2010
#2019 := (iff #2040 #2030)
#2028 := (iff #2047 #2025)
#2036 := (+ #990 #1193)
#2021 := (<= #2036 0::Int)
#2026 := (iff #2021 #2025)
#2027 := [rewrite]: #2026
#2022 := (iff #2047 #2021)
#2018 := (= #2057 #2036)
#2020 := [rewrite]: #2018
#2023 := [monotonicity #2020]: #2022
#2029 := [trans #2023 #2027]: #2028
#2035 := (iff #2039 #2046)
#2043 := (+ #785 ?v0!2)
#2041 := (>= #2043 0::Int)
#2032 := (iff #2041 #2046)
#2034 := [rewrite]: #2032
#2049 := (iff #2039 #2041)
#2044 := (= #2037 #2043)
#2048 := [rewrite]: #2044
#2042 := [monotonicity #2048]: #2049
#2033 := [trans #2042 #2034]: #2035
#2031 := [monotonicity #2033 #2029]: #2019
#2013 := [trans #2031 #2011]: #2012
#2002 := [monotonicity #2013]: #2017
#2005 := [trans #2002 #2004]: #2006
#2016 := [quant-inst #1192]: #2015
#2007 := [mp #2016 #2005]: #2014
#1927 := [unit-resolution #2007 #1944 #1932]: #1925
#1928 := [unit-resolution #1927 #1943]: #2025
#2120 := (not #1381)
#2121 := (or #1775 #2120)
#2080 := [def-axiom]: #2121
#1926 := [unit-resolution #2080 #1938]: #2120
#1929 := [th-lemma arith farkas 1 -1 1 #1926 #1928 #1957]: false
#1919 := [lemma #1929]: #1917
#2476 := [unit-resolution #1919 #2475 #1944 #2471]: #1775
#2125 := (or #2400 #2392 #1778)
#2133 := [def-axiom]: #2125
#2477 := [unit-resolution #2133 #2476 #2470]: #2392
#2229 := (not #2392)
#2450 := (or #2229 #2447)
#2433 := (= #2432 f15)
#2434 := (or #2433 #2431 #2429)
#2435 := (not #2434)
#2451 := (or #2229 #2435)
#2453 := (iff #2451 #2450)
#2455 := (iff #2450 #2450)
#2456 := [rewrite]: #2455
#2448 := (iff #2435 #2447)
#2445 := (iff #2434 #2442)
#2439 := (or #2436 #2431 #2429)
#2443 := (iff #2439 #2442)
#2444 := [rewrite]: #2443
#2440 := (iff #2434 #2439)
#2437 := (iff #2433 #2436)
#2438 := [rewrite]: #2437
#2441 := [monotonicity #2438]: #2440
#2446 := [trans #2441 #2444]: #2445
#2449 := [monotonicity #2446]: #2448
#2454 := [monotonicity #2449]: #2453
#2457 := [trans #2454 #2456]: #2453
#2452 := [quant-inst #70]: #2451
#2458 := [mp #2452 #2457]: #2450
#2478 := [unit-resolution #2458 #2477]: #2447
#2465 := (or #2442 #2464)
#2466 := [def-axiom]: #2465
#2479 := [unit-resolution #2466 #2478]: #2464
#2491 := [unit-resolution #2479 #2490]: false
#2493 := [lemma #2491]: #2492
#2752 := [unit-resolution #2493 #2751 #2750]: #2403
#2216 := (or #2412 #2389 #2406)
#2210 := [def-axiom]: #2216
#2753 := [unit-resolution #2210 #2752 #2749]: #2389
#2244 := (or #2386 #2380)
#2238 := [def-axiom]: #2244
#2754 := [unit-resolution #2238 #2753]: #2380
#2685 := (or #2368 #2345)
#1429 := (not #1424)
#2601 := [hypothesis]: #2371
#2280 := (or #2368 #2362)
#2283 := [def-axiom]: #2280
#2619 := [unit-resolution #2283 #2601]: #2362
#2643 := (= #95 #117)
#2639 := (= #117 #95)
#1935 := (or #2368 #348)
#1936 := [def-axiom]: #1935
#2622 := [unit-resolution #1936 #2601]: #348
#2624 := [symm #2622]: #101
#2640 := [monotonicity #2624]: #2639
#2644 := [symm #2640]: #2643
#2645 := (= f19 #95)
#2271 := (or #2368 #343)
#1934 := [def-axiom]: #2271
#2621 := [unit-resolution #1934 #2601]: #343
#2642 := [symm #2621]: #98
#1937 := (or #2368 #351)
#2273 := [def-axiom]: #1937
#2620 := [unit-resolution #2273 #2601]: #351
#2641 := [symm #2620]: #103
#2646 := [trans #2641 #2642]: #2645
#2647 := [trans #2646 #2644]: #370
#1257 := (not #370)
#1953 := (or #2356 #1257)
#2288 := [def-axiom]: #1953
#2648 := [unit-resolution #2288 #2647]: #2356
#2287 := (or #2365 #2359 #1717)
#1930 := [def-axiom]: #2287
#2649 := [unit-resolution #1930 #2648 #2619]: #1717
#2291 := (or #1712 #1429)
#2292 := [def-axiom]: #2291
#2650 := [unit-resolution #2292 #2649]: #1429
#2599 := (>= #2548 0::Int)
#2674 := (not #2599)
#2636 := (not #2623)
#2600 := (= #117 #1242)
#2604 := (not #2600)
#2607 := (+ #117 #1444)
#2609 := (>= #2607 0::Int)
#2614 := (not #2609)
#2294 := (or #1712 #2293)
#2289 := [def-axiom]: #2294
#2651 := [unit-resolution #2289 #2649]: #2293
#2495 := (* -1::Int #117)
#2534 := (+ f19 #2495)
#2536 := (>= #2534 0::Int)
#2652 := (or #1257 #2536)
#2653 := [th-lemma arith triangle-eq]: #2652
#2654 := [unit-resolution #2653 #2647]: #2536
#2615 := (not #2536)
#2616 := (or #2614 #2615 #1446)
#2610 := [hypothesis]: #2609
#2611 := [hypothesis]: #2293
#2612 := [hypothesis]: #2536
#2613 := [th-lemma arith farkas 1 -1 1 #2612 #2611 #2610]: false
#2617 := [lemma #2613]: #2616
#2655 := [unit-resolution #2617 #2654 #2651]: #2614
#2605 := (or #2604 #2609)
#2606 := [th-lemma arith triangle-eq]: #2605
#2656 := [unit-resolution #2606 #2655]: #2604
#2637 := (or #2636 #2600 #438)
#2632 := (= #1242 #117)
#2630 := (= ?v0!3 f18)
#2626 := [hypothesis]: #348
#2628 := (= ?v0!3 f12)
#2627 := [hypothesis]: #2623
#2629 := [symm #2627]: #2628
#2631 := [trans #2629 #2626]: #2630
#2633 := [monotonicity #2631]: #2632
#2634 := [symm #2633]: #2600
#2625 := [hypothesis]: #2604
#2635 := [unit-resolution #2625 #2634]: false
#2638 := [lemma #2635]: #2637
#2657 := [unit-resolution #2638 #2656 #2622]: #2636
#2677 := (or #2623 #2674)
#1922 := (or #2368 #881)
#2282 := [def-axiom]: #1922
#2658 := [unit-resolution #2282 #2601]: #881
#1888 := (+ #95 #840)
#2425 := (<= #1888 0::Int)
#1885 := (= #95 f19)
#2659 := [trans #2621 #2620]: #1885
#2660 := (not #1885)
#2661 := (or #2660 #2425)
#2662 := [th-lemma arith triangle-eq]: #2661
#2663 := [unit-resolution #2662 #2659]: #2425
#2665 := (not #2425)
#2666 := (or #2664 #1446 #2665 #882)
#2667 := [th-lemma arith assign-bounds 1 1 1]: #2666
#2668 := [unit-resolution #2667 #2651 #2663 #2658]: #2664
#2670 := (or #2549 #2561)
#1958 := (or #1712 #1248)
#1959 := [def-axiom]: #1958
#2669 := [unit-resolution #1959 #2649]: #1248
#2569 := (or #2345 #1697 #2549 #2561)
#2537 := (+ #1242 #990)
#2538 := (<= #2537 0::Int)
#2539 := (+ ?v0!3 #785)
#2540 := (>= #2539 0::Int)
#2541 := (or #1697 #2540 #2538)
#2570 := (or #2345 #2541)
#2577 := (iff #2570 #2569)
#2566 := (or #1697 #2549 #2561)
#2572 := (or #2345 #2566)
#2575 := (iff #2572 #2569)
#2576 := [rewrite]: #2575
#2573 := (iff #2570 #2572)
#2567 := (iff #2541 #2566)
#2564 := (iff #2538 #2561)
#2554 := (+ #990 #1242)
#2557 := (<= #2554 0::Int)
#2562 := (iff #2557 #2561)
#2563 := [rewrite]: #2562
#2558 := (iff #2538 #2557)
#2555 := (= #2537 #2554)
#2556 := [rewrite]: #2555
#2559 := [monotonicity #2556]: #2558
#2565 := [trans #2559 #2563]: #2564
#2552 := (iff #2540 #2549)
#2542 := (+ #785 ?v0!3)
#2545 := (>= #2542 0::Int)
#2550 := (iff #2545 #2549)
#2551 := [rewrite]: #2550
#2546 := (iff #2540 #2545)
#2543 := (= #2539 #2542)
#2544 := [rewrite]: #2543
#2547 := [monotonicity #2544]: #2546
#2553 := [trans #2547 #2551]: #2552
#2568 := [monotonicity #2553 #2565]: #2567
#2574 := [monotonicity #2568]: #2573
#2578 := [trans #2574 #2576]: #2577
#2571 := [quant-inst #1241]: #2570
#2579 := [mp #2571 #2578]: #2569
#2671 := [unit-resolution #2579 #1944 #2669]: #2670
#2672 := [unit-resolution #2671 #2668]: #2549
#2673 := (not #2549)
#2675 := (or #2623 #2673 #2674)
#2676 := [th-lemma arith triangle-eq]: #2675
#2678 := [unit-resolution #2676 #2672]: #2677
#2679 := [unit-resolution #2678 #2657]: #2674
#1974 := (>= #866 -1::Int)
#2281 := (or #2368 #865)
#1921 := [def-axiom]: #2281
#2680 := [unit-resolution #1921 #2601]: #865
#2681 := (or #869 #1974)
#2682 := [th-lemma arith triangle-eq]: #2681
#2683 := [unit-resolution #2682 #2680]: #1974
#2684 := [th-lemma arith farkas 1 -1 1 #2683 #2679 #2650]: false
#2686 := [lemma #2684]: #2685
#2755 := [unit-resolution #2686 #2750]: #2368
#2250 := (or #2383 #2371 #2377)
#2256 := [def-axiom]: #2250
#2756 := [unit-resolution #2256 #2755 #2754]: #2377
#2262 := (or #2374 #2362)
#2251 := [def-axiom]: #2262
#2757 := [unit-resolution #2251 #2756]: #2362
#2507 := (= #67 #117)
#2762 := (= #117 #67)
#1988 := (or #2374 #486)
#1989 := [def-axiom]: #1988
#2758 := [unit-resolution #1989 #2756]: #486
#2759 := [symm #2758]: #134
#2763 := [monotonicity #2759]: #2762
#2764 := [symm #2763]: #2507
#2765 := (= f19 #67)
#2263 := (or #2374 #489)
#2267 := [def-axiom]: #2263
#2760 := [unit-resolution #2267 #2756]: #489
#2761 := [symm #2760]: #135
#2766 := [trans #2761 #2751]: #2765
#2767 := [trans #2766 #2764]: #370
#2768 := [unit-resolution #2288 #2767]: #2356
#2769 := [unit-resolution #1930 #2768 #2757]: #1717
#2770 := [unit-resolution #2289 #2769]: #2293
#1889 := (+ f13 #840)
#2265 := (<= #1889 0::Int)
#2771 := (or #495 #2265)
#2772 := [th-lemma arith triangle-eq]: #2771
#2773 := [unit-resolution #2772 #2760]: #2265
#2774 := (not #2265)
#2775 := (or #2664 #1446 #2774)
#2776 := [th-lemma arith assign-bounds -1 -1]: #2775
#2777 := [unit-resolution #2776 #2773 #2770]: #2664
#2778 := [unit-resolution #1959 #2769]: #1248
#2779 := [unit-resolution #2579 #2750 #2778 #2777]: #2549
#2780 := [unit-resolution #2292 #2769]: #1429
#1975 := (or #2374 #865)
#2257 := [def-axiom]: #1975
#2781 := [unit-resolution #2257 #2756]: #865
#2782 := [unit-resolution #2682 #2781]: #1974
#2741 := (not #1974)
#2742 := (or #2599 #2741 #1424)
#2737 := [hypothesis]: #1429
#2738 := [hypothesis]: #2674
#2739 := [hypothesis]: #1974
#2740 := [th-lemma arith farkas 1 -1 1 #2739 #2738 #2737]: false
#2743 := [lemma #2740]: #2742
#2783 := [unit-resolution #2743 #2782 #2780]: #2599
#2784 := [unit-resolution #2676 #2783 #2779]: #2623
#2785 := [monotonicity #2784]: #2744
#2786 := (not #2744)
#2787 := (or #2786 #2747)
#2788 := [th-lemma arith triangle-eq]: #2787
#2789 := [unit-resolution #2788 #2785]: #2747
#2261 := (or #2374 #882)
#2258 := [def-axiom]: #2261
#2790 := [unit-resolution #2258 #2756]: #882
#2791 := [th-lemma arith farkas 1 -1 -1 1 #2790 #2770 #2773 #2789]: false
#2792 := [lemma #2791]: #2415
#2421 := (or #1525 #2418)
#1595 := (forall (vars (?v0 Int)) #1592)
#1781 := (or #1595 #1778)
#1784 := (not #1781)
#1787 := (or #304 #295 #286 #1657 #878 #790 #1784)
#1790 := (not #1787)
#1684 := (forall (vars (?v0 Int)) #1679)
#1690 := (not #1684)
#1691 := (or #370 #1690)
#1692 := (not #1691)
#1720 := (or #1692 #1717)
#1728 := (not #1720)
#1738 := (or #504 #495 #1657 #878 #1726 #1727 #869 #881 #1728)
#1739 := (not #1738)
#1729 := (or #456 #438 #429 #1657 #878 #1726 #1727 #869 #882 #1728)
#1730 := (not #1729)
#1744 := (or #1730 #1739)
#1750 := (not #1744)
#1751 := (or #1657 #878 #787 #1750)
#1752 := (not #1751)
#1796 := (or #1752 #1790)
#1801 := (not #1796)
#1570 := (forall (vars (?v0 Int)) #1565)
#1764 := (not #1570)
#1548 := (forall (vars (?v0 Int)) #1543)
#1763 := (not #1548)
#1804 := (or #591 #1657 #878 #1763 #1764 #1801)
#1807 := (not #1804)
#1810 := (or #1525 #1807)
#2422 := (iff #1810 #2421)
#2419 := (iff #1807 #2418)
#2416 := (iff #1804 #2415)
#2413 := (iff #1801 #2412)
#2410 := (iff #1796 #2409)
#2407 := (iff #1790 #2406)
#2404 := (iff #1787 #2403)
#2401 := (iff #1784 #2400)
#2398 := (iff #1781 #2397)
#2395 := (iff #1595 #2392)
#2393 := (iff #1592 #1592)
#2394 := [refl]: #2393
#2396 := [quant-intro #2394]: #2395
#2399 := [monotonicity #2396]: #2398
#2402 := [monotonicity #2399]: #2401
#2405 := [monotonicity #2402]: #2404
#2408 := [monotonicity #2405]: #2407
#2390 := (iff #1752 #2389)
#2387 := (iff #1751 #2386)
#2384 := (iff #1750 #2383)
#2381 := (iff #1744 #2380)
#2378 := (iff #1739 #2377)
#2375 := (iff #1738 #2374)
#2366 := (iff #1728 #2365)
#2363 := (iff #1720 #2362)
#2360 := (iff #1692 #2359)
#2357 := (iff #1691 #2356)
#2354 := (iff #1690 #2353)
#2351 := (iff #1684 #2348)
#2349 := (iff #1679 #1679)
#2350 := [refl]: #2349
#2352 := [quant-intro #2350]: #2351
#2355 := [monotonicity #2352]: #2354
#2358 := [monotonicity #2355]: #2357
#2361 := [monotonicity #2358]: #2360
#2364 := [monotonicity #2361]: #2363
#2367 := [monotonicity #2364]: #2366
#2376 := [monotonicity #2367]: #2375
#2379 := [monotonicity #2376]: #2378
#2372 := (iff #1730 #2371)
#2369 := (iff #1729 #2368)
#2370 := [monotonicity #2367]: #2369
#2373 := [monotonicity #2370]: #2372
#2382 := [monotonicity #2373 #2379]: #2381
#2385 := [monotonicity #2382]: #2384
#2388 := [monotonicity #2385]: #2387
#2391 := [monotonicity #2388]: #2390
#2411 := [monotonicity #2391 #2408]: #2410
#2414 := [monotonicity #2411]: #2413
#2346 := (iff #1764 #2345)
#2343 := (iff #1570 #2340)
#2341 := (iff #1565 #1565)
#2342 := [refl]: #2341
#2344 := [quant-intro #2342]: #2343
#2347 := [monotonicity #2344]: #2346
#2338 := (iff #1763 #2337)
#2335 := (iff #1548 #2332)
#2333 := (iff #1543 #1543)
#2334 := [refl]: #2333
#2336 := [quant-intro #2334]: #2335
#2339 := [monotonicity #2336]: #2338
#2417 := [monotonicity #2339 #2347 #2414]: #2416
#2420 := [monotonicity #2417]: #2419
#2423 := [monotonicity #2420]: #2422
#1432 := (and #1248 #1429)
#1435 := (not #1432)
#1451 := (or #1435 #1446)
#1454 := (not #1451)
#1267 := (and #1257 #848)
#1460 := (or #1267 #1454)
#1484 := (and #486 #489 #731 #734 #817 #820 #865 #882 #1460)
#1472 := (and #343 #348 #351 #731 #734 #817 #820 #865 #881 #1460)
#1489 := (or #1472 #1484)
#1495 := (and #731 #734 #790 #1489)
#1367 := (and #1199 #1200)
#1370 := (not #1367)
#1386 := (or #1370 #1381)
#1389 := (not #1386)
#1178 := (not #1177)
#1358 := (and #1178 #1179)
#1361 := (not #1358)
#1364 := (or #1355 #1361)
#1392 := (and #1364 #1389)
#1168 := (not #757)
#1171 := (forall (vars (?v0 Int)) #1168)
#1395 := (or #1171 #1392)
#1401 := (and #242 #245 #248 #731 #734 #787 #1395)
#1500 := (or #1401 #1495)
#1506 := (and #239 #724 #731 #734 #998 #1500)
#1136 := (not #1135)
#1328 := (and #1136 #1137)
#1331 := (not #1328)
#1337 := (or #1134 #1331)
#1342 := (not #1337)
#1511 := (or #1342 #1506)
#1813 := (iff #1511 #1810)
#1633 := (or #1198 #1618 #1381)
#1645 := (or #1644 #1633)
#1646 := (not #1645)
#1651 := (or #1595 #1646)
#1658 := (not #1651)
#1659 := (or #304 #295 #286 #1657 #878 #790 #1658)
#1660 := (not #1659)
#1757 := (or #1660 #1752)
#1765 := (not #1757)
#1766 := (or #591 #1657 #878 #1763 #1764 #1765)
#1767 := (not #1766)
#1772 := (or #1525 #1767)
#1811 := (iff #1772 #1810)
#1808 := (iff #1767 #1807)
#1805 := (iff #1766 #1804)
#1802 := (iff #1765 #1801)
#1799 := (iff #1757 #1796)
#1793 := (or #1790 #1752)
#1797 := (iff #1793 #1796)
#1798 := [rewrite]: #1797
#1794 := (iff #1757 #1793)
#1791 := (iff #1660 #1790)
#1788 := (iff #1659 #1787)
#1785 := (iff #1658 #1784)
#1782 := (iff #1651 #1781)
#1779 := (iff #1646 #1778)
#1776 := (iff #1645 #1775)
#1777 := [rewrite]: #1776
#1780 := [monotonicity #1777]: #1779
#1783 := [monotonicity #1780]: #1782
#1786 := [monotonicity #1783]: #1785
#1789 := [monotonicity #1786]: #1788
#1792 := [monotonicity #1789]: #1791
#1795 := [monotonicity #1792]: #1794
#1800 := [trans #1795 #1798]: #1799
#1803 := [monotonicity #1800]: #1802
#1806 := [monotonicity #1803]: #1805
#1809 := [monotonicity #1806]: #1808
#1812 := [monotonicity #1809]: #1811
#1773 := (iff #1511 #1772)
#1770 := (iff #1506 #1767)
#1760 := (and #239 #1548 #731 #734 #1570 #1757)
#1768 := (iff #1760 #1767)
#1769 := [rewrite]: #1768
#1761 := (iff #1506 #1760)
#1758 := (iff #1500 #1757)
#1755 := (iff #1495 #1752)
#1747 := (and #731 #734 #790 #1744)
#1753 := (iff #1747 #1752)
#1754 := [rewrite]: #1753
#1748 := (iff #1495 #1747)
#1745 := (iff #1489 #1744)
#1742 := (iff #1484 #1739)
#1735 := (and #486 #489 #731 #734 #817 #820 #865 #882 #1720)
#1740 := (iff #1735 #1739)
#1741 := [rewrite]: #1740
#1736 := (iff #1484 #1735)
#1721 := (iff #1460 #1720)
#1718 := (iff #1454 #1717)
#1715 := (iff #1451 #1712)
#1698 := (or #1697 #1424)
#1709 := (or #1698 #1446)
#1713 := (iff #1709 #1712)
#1714 := [rewrite]: #1713
#1710 := (iff #1451 #1709)
#1707 := (iff #1435 #1698)
#1699 := (not #1698)
#1702 := (not #1699)
#1705 := (iff #1702 #1698)
#1706 := [rewrite]: #1705
#1703 := (iff #1435 #1702)
#1700 := (iff #1432 #1699)
#1701 := [rewrite]: #1700
#1704 := [monotonicity #1701]: #1703
#1708 := [trans #1704 #1706]: #1707
#1711 := [monotonicity #1708]: #1710
#1716 := [trans #1711 #1714]: #1715
#1719 := [monotonicity #1716]: #1718
#1695 := (iff #1267 #1692)
#1687 := (and #1257 #1684)
#1693 := (iff #1687 #1692)
#1694 := [rewrite]: #1693
#1688 := (iff #1267 #1687)
#1685 := (iff #848 #1684)
#1682 := (iff #845 #1679)
#1665 := (or #1528 #828)
#1676 := (or #1665 #842)
#1680 := (iff #1676 #1679)
#1681 := [rewrite]: #1680
#1677 := (iff #845 #1676)
#1674 := (iff #837 #1665)
#1666 := (not #1665)
#1669 := (not #1666)
#1672 := (iff #1669 #1665)
#1673 := [rewrite]: #1672
#1670 := (iff #837 #1669)
#1667 := (iff #834 #1666)
#1668 := [rewrite]: #1667
#1671 := [monotonicity #1668]: #1670
#1675 := [trans #1671 #1673]: #1674
#1678 := [monotonicity #1675]: #1677
#1683 := [trans #1678 #1681]: #1682
#1686 := [quant-intro #1683]: #1685
#1689 := [monotonicity #1686]: #1688
#1696 := [trans #1689 #1694]: #1695
#1722 := [monotonicity #1696 #1719]: #1721
#1737 := [monotonicity #1722]: #1736
#1743 := [trans #1737 #1741]: #1742
#1733 := (iff #1472 #1730)
#1723 := (and #343 #348 #351 #731 #734 #817 #820 #865 #881 #1720)
#1731 := (iff #1723 #1730)
#1732 := [rewrite]: #1731
#1724 := (iff #1472 #1723)
#1725 := [monotonicity #1722]: #1724
#1734 := [trans #1725 #1732]: #1733
#1746 := [monotonicity #1734 #1743]: #1745
#1749 := [monotonicity #1746]: #1748
#1756 := [trans #1749 #1754]: #1755
#1663 := (iff #1401 #1660)
#1654 := (and #242 #245 #248 #731 #734 #787 #1651)
#1661 := (iff #1654 #1660)
#1662 := [rewrite]: #1661
#1655 := (iff #1401 #1654)
#1652 := (iff #1395 #1651)
#1649 := (iff #1392 #1646)
#1638 := (not #1633)
#1641 := (and #1613 #1638)
#1647 := (iff #1641 #1646)
#1648 := [rewrite]: #1647
#1642 := (iff #1392 #1641)
#1639 := (iff #1389 #1638)
#1636 := (iff #1386 #1633)
#1619 := (or #1198 #1618)
#1630 := (or #1619 #1381)
#1634 := (iff #1630 #1633)
#1635 := [rewrite]: #1634
#1631 := (iff #1386 #1630)
#1628 := (iff #1370 #1619)
#1620 := (not #1619)
#1623 := (not #1620)
#1626 := (iff #1623 #1619)
#1627 := [rewrite]: #1626
#1624 := (iff #1370 #1623)
#1621 := (iff #1367 #1620)
#1622 := [rewrite]: #1621
#1625 := [monotonicity #1622]: #1624
#1629 := [trans #1625 #1627]: #1628
#1632 := [monotonicity #1629]: #1631
#1637 := [trans #1632 #1635]: #1636
#1640 := [monotonicity #1637]: #1639
#1616 := (iff #1364 #1613)
#1599 := (or #1177 #1598)
#1610 := (or #1355 #1599)
#1614 := (iff #1610 #1613)
#1615 := [rewrite]: #1614
#1611 := (iff #1364 #1610)
#1608 := (iff #1361 #1599)
#1600 := (not #1599)
#1603 := (not #1600)
#1606 := (iff #1603 #1599)
#1607 := [rewrite]: #1606
#1604 := (iff #1361 #1603)
#1601 := (iff #1358 #1600)
#1602 := [rewrite]: #1601
#1605 := [monotonicity #1602]: #1604
#1609 := [trans #1605 #1607]: #1608
#1612 := [monotonicity #1609]: #1611
#1617 := [trans #1612 #1615]: #1616
#1643 := [monotonicity #1617 #1640]: #1642
#1650 := [trans #1643 #1648]: #1649
#1596 := (iff #1171 #1595)
#1593 := (iff #1168 #1592)
#1590 := (iff #757 #1587)
#1573 := (or #1528 #744)
#1584 := (or #78 #1573)
#1588 := (iff #1584 #1587)
#1589 := [rewrite]: #1588
#1585 := (iff #757 #1584)
#1582 := (iff #751 #1573)
#1574 := (not #1573)
#1577 := (not #1574)
#1580 := (iff #1577 #1573)
#1581 := [rewrite]: #1580
#1578 := (iff #751 #1577)
#1575 := (iff #748 #1574)
#1576 := [rewrite]: #1575
#1579 := [monotonicity #1576]: #1578
#1583 := [trans #1579 #1581]: #1582
#1586 := [monotonicity #1583]: #1585
#1591 := [trans #1586 #1589]: #1590
#1594 := [monotonicity #1591]: #1593
#1597 := [quant-intro #1594]: #1596
#1653 := [monotonicity #1597 #1650]: #1652
#1656 := [monotonicity #1653]: #1655
#1664 := [trans #1656 #1662]: #1663
#1759 := [monotonicity #1664 #1756]: #1758
#1571 := (iff #998 #1570)
#1568 := (iff #995 #1565)
#1551 := (or #1528 #979)
#1562 := (or #1551 #992)
#1566 := (iff #1562 #1565)
#1567 := [rewrite]: #1566
#1563 := (iff #995 #1562)
#1560 := (iff #987 #1551)
#1552 := (not #1551)
#1555 := (not #1552)
#1558 := (iff #1555 #1551)
#1559 := [rewrite]: #1558
#1556 := (iff #987 #1555)
#1553 := (iff #984 #1552)
#1554 := [rewrite]: #1553
#1557 := [monotonicity #1554]: #1556
#1561 := [trans #1557 #1559]: #1560
#1564 := [monotonicity #1561]: #1563
#1569 := [trans #1564 #1567]: #1568
#1572 := [quant-intro #1569]: #1571
#1549 := (iff #724 #1548)
#1546 := (iff #721 #1543)
#1529 := (or #1528 #707)
#1540 := (or #1529 #717)
#1544 := (iff #1540 #1543)
#1545 := [rewrite]: #1544
#1541 := (iff #721 #1540)
#1538 := (iff #712 #1529)
#1530 := (not #1529)
#1533 := (not #1530)
#1536 := (iff #1533 #1529)
#1537 := [rewrite]: #1536
#1534 := (iff #712 #1533)
#1531 := (iff #709 #1530)
#1532 := [rewrite]: #1531
#1535 := [monotonicity #1532]: #1534
#1539 := [trans #1535 #1537]: #1538
#1542 := [monotonicity #1539]: #1541
#1547 := [trans #1542 #1545]: #1546
#1550 := [quant-intro #1547]: #1549
#1762 := [monotonicity #1550 #1572 #1759]: #1761
#1771 := [trans #1762 #1769]: #1770
#1526 := (iff #1342 #1525)
#1523 := (iff #1337 #1520)
#1145 := (or #1135 #1144)
#1517 := (or #1134 #1145)
#1521 := (iff #1517 #1520)
#1522 := [rewrite]: #1521
#1518 := (iff #1337 #1517)
#1515 := (iff #1331 #1145)
#1255 := (not #1145)
#1188 := (not #1255)
#1327 := (iff #1188 #1145)
#1514 := [rewrite]: #1327
#1208 := (iff #1331 #1188)
#1256 := (iff #1328 #1255)
#1187 := [rewrite]: #1256
#1209 := [monotonicity #1187]: #1208
#1516 := [trans #1209 #1514]: #1515
#1519 := [monotonicity #1516]: #1518
#1524 := [trans #1519 #1522]: #1523
#1527 := [monotonicity #1524]: #1526
#1774 := [monotonicity #1527 #1771]: #1773
#1814 := [trans #1774 #1812]: #1813
#1278 := (not #875)
#1275 := (not #869)
#1243 := (+ #1242 #840)
#1244 := (<= #1243 0::Int)
#1245 := (+ ?v0!3 #829)
#1246 := (>= #1245 0::Int)
#1247 := (not #1246)
#1249 := (and #1248 #1247)
#1250 := (not #1249)
#1251 := (or #1250 #1244)
#1252 := (not #1251)
#1271 := (or #1252 #1267)
#1238 := (not #825)
#1156 := (not #739)
#1290 := (not #495)
#1287 := (not #504)
#1295 := (and #1287 #1290 #1156 #1238 #1271 #1275 #1278 #887)
#1235 := (not #878)
#1232 := (not #429)
#1229 := (not #438)
#1226 := (not #456)
#1283 := (and #1226 #1229 #1232 #1235 #1156 #1238 #1271 #1275 #1278 #881)
#1299 := (or #1283 #1295)
#1303 := (and #1156 #790 #1299)
#1194 := (+ #1193 #768)
#1195 := (<= #1194 0::Int)
#1201 := (and #1200 #1199)
#1202 := (not #1201)
#1203 := (or #1202 #1195)
#1204 := (not #1203)
#1180 := (and #1179 #1178)
#1181 := (not #1180)
#1183 := (= #1182 f15)
#1184 := (or #1183 #1181)
#1210 := (and #1184 #1204)
#1214 := (or #1171 #1210)
#1165 := (not #286)
#1162 := (not #295)
#1159 := (not #304)
#1220 := (and #1159 #1162 #1165 #1156 #1214 #955)
#1307 := (or #1220 #1303)
#1146 := (not #591)
#1318 := (and #1146 #724 #1156 #1307 #998)
#1138 := (and #1137 #1136)
#1139 := (not #1138)
#1140 := (or #1139 #1134)
#1141 := (not #1140)
#1322 := (or #1141 #1318)
#1512 := (iff #1322 #1511)
#1509 := (iff #1318 #1506)
#1503 := (and #239 #724 #736 #1500 #998)
#1507 := (iff #1503 #1506)
#1508 := [rewrite]: #1507
#1504 := (iff #1318 #1503)
#1501 := (iff #1307 #1500)
#1498 := (iff #1303 #1495)
#1492 := (and #736 #790 #1489)
#1496 := (iff #1492 #1495)
#1497 := [rewrite]: #1496
#1493 := (iff #1303 #1492)
#1490 := (iff #1299 #1489)
#1487 := (iff #1295 #1484)
#1481 := (and #486 #489 #736 #822 #1460 #865 #872 #882)
#1485 := (iff #1481 #1484)
#1486 := [rewrite]: #1485
#1482 := (iff #1295 #1481)
#1467 := (iff #1278 #872)
#1468 := [rewrite]: #1467
#1465 := (iff #1275 #865)
#1466 := [rewrite]: #1465
#1463 := (iff #1271 #1460)
#1457 := (or #1454 #1267)
#1461 := (iff #1457 #1460)
#1462 := [rewrite]: #1461
#1458 := (iff #1271 #1457)
#1455 := (iff #1252 #1454)
#1452 := (iff #1251 #1451)
#1449 := (iff #1244 #1446)
#1438 := (+ #840 #1242)
#1441 := (<= #1438 0::Int)
#1447 := (iff #1441 #1446)
#1448 := [rewrite]: #1447
#1442 := (iff #1244 #1441)
#1439 := (= #1243 #1438)
#1440 := [rewrite]: #1439
#1443 := [monotonicity #1440]: #1442
#1450 := [trans #1443 #1448]: #1449
#1436 := (iff #1250 #1435)
#1433 := (iff #1249 #1432)
#1430 := (iff #1247 #1429)
#1427 := (iff #1246 #1424)
#1416 := (+ #829 ?v0!3)
#1419 := (>= #1416 0::Int)
#1425 := (iff #1419 #1424)
#1426 := [rewrite]: #1425
#1420 := (iff #1246 #1419)
#1417 := (= #1245 #1416)
#1418 := [rewrite]: #1417
#1421 := [monotonicity #1418]: #1420
#1428 := [trans #1421 #1426]: #1427
#1431 := [monotonicity #1428]: #1430
#1434 := [monotonicity #1431]: #1433
#1437 := [monotonicity #1434]: #1436
#1453 := [monotonicity #1437 #1450]: #1452
#1456 := [monotonicity #1453]: #1455
#1459 := [monotonicity #1456]: #1458
#1464 := [trans #1459 #1462]: #1463
#1414 := (iff #1238 #822)
#1415 := [rewrite]: #1414
#1347 := (iff #1156 #736)
#1348 := [rewrite]: #1347
#1479 := (iff #1290 #489)
#1480 := [rewrite]: #1479
#1477 := (iff #1287 #486)
#1478 := [rewrite]: #1477
#1483 := [monotonicity #1478 #1480 #1348 #1415 #1464 #1466 #1468 #891]: #1482
#1488 := [trans #1483 #1486]: #1487
#1475 := (iff #1283 #1472)
#1469 := (and #343 #348 #351 #734 #736 #822 #1460 #865 #872 #881)
#1473 := (iff #1469 #1472)
#1474 := [rewrite]: #1473
#1470 := (iff #1283 #1469)
#1412 := (iff #1235 #734)
#1413 := [rewrite]: #1412
#1410 := (iff #1232 #351)
#1411 := [rewrite]: #1410
#1408 := (iff #1229 #348)
#1409 := [rewrite]: #1408
#1406 := (iff #1226 #343)
#1407 := [rewrite]: #1406
#1471 := [monotonicity #1407 #1409 #1411 #1413 #1348 #1415 #1464 #1466 #1468]: #1470
#1476 := [trans #1471 #1474]: #1475
#1491 := [monotonicity #1476 #1488]: #1490
#1494 := [monotonicity #1348 #1491]: #1493
#1499 := [trans #1494 #1497]: #1498
#1404 := (iff #1220 #1401)
#1398 := (and #242 #245 #248 #736 #1395 #787)
#1402 := (iff #1398 #1401)
#1403 := [rewrite]: #1402
#1399 := (iff #1220 #1398)
#1396 := (iff #1214 #1395)
#1393 := (iff #1210 #1392)
#1390 := (iff #1204 #1389)
#1387 := (iff #1203 #1386)
#1384 := (iff #1195 #1381)
#1373 := (+ #768 #1193)
#1376 := (<= #1373 0::Int)
#1382 := (iff #1376 #1381)
#1383 := [rewrite]: #1382
#1377 := (iff #1195 #1376)
#1374 := (= #1194 #1373)
#1375 := [rewrite]: #1374
#1378 := [monotonicity #1375]: #1377
#1385 := [trans #1378 #1383]: #1384
#1371 := (iff #1202 #1370)
#1368 := (iff #1201 #1367)
#1369 := [rewrite]: #1368
#1372 := [monotonicity #1369]: #1371
#1388 := [monotonicity #1372 #1385]: #1387
#1391 := [monotonicity #1388]: #1390
#1365 := (iff #1184 #1364)
#1362 := (iff #1181 #1361)
#1359 := (iff #1180 #1358)
#1360 := [rewrite]: #1359
#1363 := [monotonicity #1360]: #1362
#1356 := (iff #1183 #1355)
#1357 := [rewrite]: #1356
#1366 := [monotonicity #1357 #1363]: #1365
#1394 := [monotonicity #1366 #1391]: #1393
#1397 := [monotonicity #1394]: #1396
#1353 := (iff #1165 #248)
#1354 := [rewrite]: #1353
#1351 := (iff #1162 #245)
#1352 := [rewrite]: #1351
#1349 := (iff #1159 #242)
#1350 := [rewrite]: #1349
#1400 := [monotonicity #1350 #1352 #1354 #1348 #1397 #959]: #1399
#1405 := [trans #1400 #1403]: #1404
#1502 := [monotonicity #1405 #1499]: #1501
#1345 := (iff #1146 #239)
#1346 := [rewrite]: #1345
#1505 := [monotonicity #1346 #1348 #1502]: #1504
#1510 := [trans #1505 #1508]: #1509
#1343 := (iff #1141 #1342)
#1340 := (iff #1140 #1337)
#1334 := (or #1331 #1134)
#1338 := (iff #1334 #1337)
#1339 := [rewrite]: #1338
#1335 := (iff #1140 #1334)
#1332 := (iff #1139 #1331)
#1329 := (iff #1138 #1328)
#1330 := [rewrite]: #1329
#1333 := [monotonicity #1330]: #1332
#1336 := [monotonicity #1333]: #1335
#1341 := [trans #1336 #1339]: #1340
#1344 := [monotonicity #1341]: #1343
#1513 := [monotonicity #1344 #1510]: #1512
#1105 := (or #591 #727 #739 #976 #1001)
#1110 := (and #724 #1105)
#1113 := (not #1110)
#1323 := (~ #1113 #1322)
#1319 := (not #1105)
#1320 := (~ #1319 #1318)
#1315 := (not #1001)
#1316 := (~ #1315 #998)
#1313 := (~ #998 #998)
#1311 := (~ #995 #995)
#1312 := [refl]: #1311
#1314 := [nnf-pos #1312]: #1313
#1317 := [nnf-neg #1314]: #1316
#1308 := (not #976)
#1309 := (~ #1308 #1307)
#1304 := (not #971)
#1305 := (~ #1304 #1303)
#1300 := (not #950)
#1301 := (~ #1300 #1299)
#1296 := (not #945)
#1297 := (~ #1296 #1295)
#1293 := (~ #887 #887)
#1294 := [refl]: #1293
#1279 := (~ #1278 #1278)
#1280 := [refl]: #1279
#1276 := (~ #1275 #1275)
#1277 := [refl]: #1276
#1272 := (not #862)
#1273 := (~ #1272 #1271)
#1268 := (not #857)
#1269 := (~ #1268 #1267)
#1264 := (not #851)
#1265 := (~ #1264 #848)
#1262 := (~ #848 #848)
#1260 := (~ #845 #845)
#1261 := [refl]: #1260
#1263 := [nnf-pos #1261]: #1262
#1266 := [nnf-neg #1263]: #1265
#1258 := (~ #1257 #1257)
#1259 := [refl]: #1258
#1270 := [nnf-neg #1259 #1266]: #1269
#1253 := (~ #851 #1252)
#1254 := [sk]: #1253
#1274 := [nnf-neg #1254 #1270]: #1273
#1239 := (~ #1238 #1238)
#1240 := [refl]: #1239
#1157 := (~ #1156 #1156)
#1158 := [refl]: #1157
#1291 := (~ #1290 #1290)
#1292 := [refl]: #1291
#1288 := (~ #1287 #1287)
#1289 := [refl]: #1288
#1298 := [nnf-neg #1289 #1292 #1158 #1240 #1274 #1277 #1280 #1294]: #1297
#1284 := (not #921)
#1285 := (~ #1284 #1283)
#1281 := (~ #881 #881)
#1282 := [refl]: #1281
#1236 := (~ #1235 #1235)
#1237 := [refl]: #1236
#1233 := (~ #1232 #1232)
#1234 := [refl]: #1233
#1230 := (~ #1229 #1229)
#1231 := [refl]: #1230
#1227 := (~ #1226 #1226)
#1228 := [refl]: #1227
#1286 := [nnf-neg #1228 #1231 #1234 #1237 #1158 #1240 #1274 #1277 #1280 #1282]: #1285
#1302 := [nnf-neg #1286 #1298]: #1301
#1224 := (~ #790 #790)
#1225 := [refl]: #1224
#1306 := [nnf-neg #1158 #1225 #1302]: #1305
#1221 := (not #811)
#1222 := (~ #1221 #1220)
#1218 := (~ #955 #955)
#1219 := [refl]: #1218
#1215 := (not #782)
#1216 := (~ #1215 #1214)
#1211 := (not #779)
#1212 := (~ #1211 #1210)
#1205 := (not #776)
#1206 := (~ #1205 #1204)
#1207 := [sk]: #1206
#1189 := (not #765)
#1190 := (~ #1189 #1184)
#1185 := (~ #762 #1184)
#1186 := [sk]: #1185
#1191 := [nnf-neg #1186]: #1190
#1213 := [nnf-neg #1191 #1207]: #1212
#1172 := (~ #765 #1171)
#1169 := (~ #1168 #1168)
#1170 := [refl]: #1169
#1173 := [nnf-neg #1170]: #1172
#1217 := [nnf-neg #1173 #1213]: #1216
#1166 := (~ #1165 #1165)
#1167 := [refl]: #1166
#1163 := (~ #1162 #1162)
#1164 := [refl]: #1163
#1160 := (~ #1159 #1159)
#1161 := [refl]: #1160
#1223 := [nnf-neg #1161 #1164 #1167 #1158 #1217 #1219]: #1222
#1310 := [nnf-neg #1223 #1306]: #1309
#1153 := (not #727)
#1154 := (~ #1153 #724)
#1151 := (~ #724 #724)
#1149 := (~ #721 #721)
#1150 := [refl]: #1149
#1152 := [nnf-pos #1150]: #1151
#1155 := [nnf-neg #1152]: #1154
#1147 := (~ #1146 #1146)
#1148 := [refl]: #1147
#1321 := [nnf-neg #1148 #1155 #1158 #1310 #1317]: #1320
#1142 := (~ #727 #1141)
#1143 := [sk]: #1142
#1324 := [nnf-neg #1143 #1321]: #1323
#1065 := (not #1030)
#1114 := (iff #1065 #1113)
#1111 := (iff #1030 #1110)
#1108 := (iff #1027 #1105)
#1090 := (or #591 #739 #976 #1001)
#1102 := (or #727 #1090)
#1106 := (iff #1102 #1105)
#1107 := [rewrite]: #1106
#1103 := (iff #1027 #1102)
#1100 := (iff #1024 #1090)
#1095 := (and true #1090)
#1098 := (iff #1095 #1090)
#1099 := [rewrite]: #1098
#1096 := (iff #1024 #1095)
#1093 := (iff #1019 #1090)
#1087 := (or false #591 #739 #976 #1001)
#1091 := (iff #1087 #1090)
#1092 := [rewrite]: #1091
#1088 := (iff #1019 #1087)
#1085 := (iff #624 false)
#1083 := (iff #624 #695)
#1081 := (iff #40 true)
#1082 := [iff-true #1064]: #1081
#1084 := [monotonicity #1082]: #1083
#1086 := [trans #1084 #699]: #1085
#1089 := [monotonicity #1086]: #1088
#1094 := [trans #1089 #1092]: #1093
#1097 := [monotonicity #1082 #1094]: #1096
#1101 := [trans #1097 #1099]: #1100
#1104 := [monotonicity #1101]: #1103
#1109 := [trans #1104 #1107]: #1108
#1112 := [monotonicity #1109]: #1111
#1115 := [monotonicity #1112]: #1114
#1066 := [not-or-elim #1063]: #1065
#1116 := [mp #1066 #1115]: #1113
#1325 := [mp~ #1116 #1324]: #1322
#1326 := [mp #1325 #1513]: #1511
#1815 := [mp #1326 #1814]: #1810
#2424 := [mp #1815 #2423]: #2421
#2149 := [unit-resolution #2424 #2792]: #1525
#1967 := (or #1520 #1882)
#1883 := [def-axiom]: #1967
#2150 := [unit-resolution #1883 #2149]: #1882
#2170 := (+ #39 #1132)
#2144 := (>= #2170 0::Int)
#2164 := (= #39 #1131)
#2116 := (= #1131 #39)
#2148 := (= ?v0!0 0::Int)
#1968 := (or #1520 #1136)
#1969 := [def-axiom]: #1968
#2151 := [unit-resolution #1969 #2149]: #1136
#1960 := (or #1520 #1137)
#1971 := [def-axiom]: #1960
#2142 := [unit-resolution #1971 #2149]: #1137
#2147 := [th-lemma arith eq-propagate 0 0 #2142 #2151]: #2148
#2123 := [monotonicity #2147]: #2116
#2082 := [symm #2123]: #2164
#2113 := (not #2164)
#2115 := (or #2113 #2144)
#2117 := [th-lemma arith triangle-eq]: #2115
#2084 := [unit-resolution #2117 #2082]: #2144
[th-lemma arith farkas 1 -1 1 #2084 #2150 #2038]: false
unsat