src/HOL/Boogie/Examples/Boogie_Max.certs

clarified example settings for Proof General;

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