src/HOL/Boogie/Examples/Boogie_Max.certs

merged

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