src/HOL/Boogie/Examples/Boogie_Max.certs

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