# HG changeset patch
# User haftmann
# Date 1265645560 -3600
# Node ID 648e492abc43b6e71abaafb14ef212a9e6a26f21
# Parent  9f841f20dca6798de52437e34dff846beda2f7cf
re-generated certificates

diff -r 9f841f20dca6 -r 648e492abc43 src/HOL/SMT/Examples/SMT_Examples.certs
--- a/src/HOL/SMT/Examples/SMT_Examples.certs	Mon Feb 08 17:12:38 2010 +0100
+++ b/src/HOL/SMT/Examples/SMT_Examples.certs	Mon Feb 08 17:12:40 2010 +0100
@@ -6677,15 +6677,25 @@
 [mp #29 #65]: false
 unsat
 
-rOkYPs+Q++z/M3OPR/88JQ 1272
+rOkYPs+Q++z/M3OPR/88JQ 1654
 #2 := false
 #55 := 0::int
 #7 := 2::int
 decl uf_1 :: int
 #4 := uf_1
 #8 := (mod uf_1 2::int)
-#58 := (>= #8 0::int)
-#61 := (not #58)
+#67 := (>= #8 0::int)
+#1 := true
+#156 := (iff #67 true)
+#158 := (iff #156 #67)
+#159 := [rewrite]: #158
+#28 := [true-axiom]: true
+#153 := (or false #67)
+#154 := [th-lemma]: #153
+#155 := [unit-resolution #154 #28]: #67
+#157 := [iff-true #155]: #156
+#160 := [mp #157 #159]: #67
+#70 := (not #67)
 #5 := 1::int
 #9 := (* 2::int #8)
 #10 := (+ #9 1::int)
@@ -6693,24 +6703,35 @@
 #6 := (+ uf_1 1::int)
 #12 := (<= #6 #11)
 #13 := (not #12)
-#66 := (iff #13 #61)
+#77 := (iff #13 #70)
 #39 := (+ uf_1 #9)
 #40 := (+ 1::int #39)
 #30 := (+ 1::int uf_1)
 #45 := (<= #30 #40)
 #48 := (not #45)
-#64 := (iff #48 #61)
+#75 := (iff #48 #70)
+#58 := (* 1::int #8)
+#59 := (>= #58 0::int)
+#62 := (not #59)
+#71 := (iff #62 #70)
+#68 := (iff #59 #67)
+#65 := (= #58 #8)
+#66 := [rewrite]: #65
+#69 := [monotonicity #66]: #68
+#72 := [monotonicity #69]: #71
+#73 := (iff #48 #62)
 #56 := (>= #9 0::int)
 #51 := (not #56)
-#62 := (iff #51 #61)
-#59 := (iff #56 #58)
-#60 := [rewrite]: #59
-#63 := [monotonicity #60]: #62
+#63 := (iff #51 #62)
+#60 := (iff #56 #59)
+#61 := [rewrite]: #60
+#64 := [monotonicity #61]: #63
 #52 := (iff #48 #51)
 #53 := (iff #45 #56)
 #54 := [rewrite]: #53
 #57 := [monotonicity #54]: #52
-#65 := [trans #57 #63]: #64
+#74 := [trans #57 #64]: #73
+#76 := [trans #74 #72]: #75
 #49 := (iff #13 #48)
 #46 := (iff #12 #45)
 #43 := (= #11 #40)
@@ -6727,40 +6748,38 @@
 #32 := [rewrite]: #31
 #47 := [monotonicity #32 #44]: #46
 #50 := [monotonicity #47]: #49
-#67 := [trans #50 #65]: #66
+#78 := [trans #50 #76]: #77
 #29 := [asserted]: #13
-#68 := [mp #29 #67]: #61
-#1 := true
-#28 := [true-axiom]: true
-#142 := (or false #58)
-#143 := [th-lemma]: #142
-#144 := [unit-resolution #143 #28]: #58
-[unit-resolution #144 #68]: false
-unsat
-
-oSBTeiF6GKDeHPsMxXHXtQ 1161
+#79 := [mp #29 #78]: #70
+[unit-resolution #79 #160]: false
+unsat
+
+oSBTeiF6GKDeHPsMxXHXtQ 1064
 #2 := false
 #5 := 2::int
 decl uf_1 :: int
 #4 := uf_1
 #6 := (mod uf_1 2::int)
-#55 := (>= #6 2::int)
+#122 := (>= #6 2::int)
+#123 := (not #122)
+#1 := true
+#27 := [true-axiom]: true
+#133 := (or false #123)
+#134 := [th-lemma]: #133
+#135 := [unit-resolution #134 #27]: #123
 #9 := 3::int
+#29 := (* 2::int #6)
+#48 := (>= #29 3::int)
 #10 := (+ uf_1 3::int)
 #7 := (+ #6 #6)
 #8 := (+ uf_1 #7)
 #11 := (< #8 #10)
 #12 := (not #11)
-#60 := (iff #12 #55)
+#55 := (iff #12 #48)
 #35 := (+ 3::int uf_1)
-#29 := (* 2::int #6)
 #32 := (+ uf_1 #29)
 #38 := (< #32 #35)
 #41 := (not #38)
-#58 := (iff #41 #55)
-#48 := (>= #29 3::int)
-#56 := (iff #48 #55)
-#57 := [rewrite]: #56
 #53 := (iff #41 #48)
 #46 := (not #48)
 #45 := (not #46)
@@ -6771,7 +6790,6 @@
 #44 := [rewrite]: #47
 #50 := [monotonicity #44]: #49
 #54 := [trans #50 #52]: #53
-#59 := [trans #54 #57]: #58
 #42 := (iff #12 #41)
 #39 := (iff #11 #38)
 #36 := (= #10 #35)
@@ -6782,16 +6800,10 @@
 #34 := [monotonicity #31]: #33
 #40 := [monotonicity #34 #37]: #39
 #43 := [monotonicity #40]: #42
-#61 := [trans #43 #59]: #60
+#56 := [trans #43 #54]: #55
 #28 := [asserted]: #12
-#62 := [mp #28 #61]: #55
-#127 := (not #55)
-#1 := true
-#27 := [true-axiom]: true
-#137 := (or false #127)
-#138 := [th-lemma]: #137
-#139 := [unit-resolution #138 #27]: #127
-[unit-resolution #139 #62]: false
+#57 := [mp #28 #56]: #48
+[th-lemma #57 #135]: false
 unsat
 
 hqH9yBHvmZgES3pBkvsqVQ 2715
@@ -7344,52 +7356,99 @@
 [mp #30 #96]: false
 unsat
 
-sHpY0IFBgZUNhP56aRB+/w 1765
+sHpY0IFBgZUNhP56aRB+/w 2968
 #2 := false
+#9 := 1::int
+decl ?x1!1 :: int
+#91 := ?x1!1
+#68 := -2::int
+#129 := (* -2::int ?x1!1)
+decl ?x2!0 :: int
+#90 := ?x2!0
+#7 := 2::int
+#128 := (* 2::int ?x2!0)
+#130 := (+ #128 #129)
+#131 := (<= #130 1::int)
+#136 := (not #131)
+#55 := 0::int
+#53 := -1::int
+#115 := (* -1::int ?x1!1)
+#116 := (+ ?x2!0 #115)
+#117 := (<= #116 0::int)
+#139 := (or #117 #136)
+#142 := (not #139)
+#92 := (* -2::int ?x2!0)
+#93 := (* 2::int ?x1!1)
+#94 := (+ #93 #92)
+#95 := (>= #94 -1::int)
+#96 := (not #95)
+#97 := (* -1::int ?x2!0)
+#98 := (+ ?x1!1 #97)
+#99 := (>= #98 0::int)
+#100 := (or #99 #96)
+#101 := (not #100)
+#143 := (iff #101 #142)
+#140 := (iff #100 #139)
+#137 := (iff #96 #136)
+#134 := (iff #95 #131)
+#122 := (+ #92 #93)
+#125 := (>= #122 -1::int)
+#132 := (iff #125 #131)
+#133 := [rewrite]: #132
+#126 := (iff #95 #125)
+#123 := (= #94 #122)
+#124 := [rewrite]: #123
+#127 := [monotonicity #124]: #126
+#135 := [trans #127 #133]: #134
+#138 := [monotonicity #135]: #137
+#120 := (iff #99 #117)
+#109 := (+ #97 ?x1!1)
+#112 := (>= #109 0::int)
+#118 := (iff #112 #117)
+#119 := [rewrite]: #118
+#113 := (iff #99 #112)
+#110 := (= #98 #109)
+#111 := [rewrite]: #110
+#114 := [monotonicity #111]: #113
+#121 := [trans #114 #119]: #120
+#141 := [monotonicity #121 #138]: #140
+#144 := [monotonicity #141]: #143
 #5 := (:var 0 int)
-#7 := 2::int
-#11 := (* 2::int #5)
-#9 := 1::int
+#71 := (* -2::int #5)
 #4 := (:var 1 int)
 #8 := (* 2::int #4)
+#72 := (+ #8 #71)
+#70 := (>= #72 -1::int)
+#69 := (not #70)
+#57 := (* -1::int #5)
+#58 := (+ #4 #57)
+#56 := (>= #58 0::int)
+#75 := (or #56 #69)
+#78 := (forall (vars (?x1 int) (?x2 int)) #75)
+#81 := (not #78)
+#102 := (~ #81 #101)
+#103 := [sk]: #102
+#11 := (* 2::int #5)
 #10 := (+ #8 1::int)
 #12 := (< #10 #11)
 #6 := (< #4 #5)
 #13 := (implies #6 #12)
 #14 := (forall (vars (?x1 int) (?x2 int)) #13)
 #15 := (not #14)
-#91 := (iff #15 false)
+#84 := (iff #15 #81)
 #32 := (+ 1::int #8)
 #35 := (< #32 #11)
 #41 := (not #6)
 #42 := (or #41 #35)
 #47 := (forall (vars (?x1 int) (?x2 int)) #42)
 #50 := (not #47)
-#89 := (iff #50 false)
-#1 := true
-#84 := (not true)
-#87 := (iff #84 false)
-#88 := [rewrite]: #87
-#85 := (iff #50 #84)
-#82 := (iff #47 true)
-#77 := (forall (vars (?x1 int) (?x2 int)) true)
-#80 := (iff #77 true)
-#81 := [elim-unused]: #80
-#78 := (iff #47 #77)
-#75 := (iff #42 true)
-#55 := 0::int
-#53 := -1::int
-#57 := (* -1::int #5)
-#58 := (+ #4 #57)
-#56 := (>= #58 0::int)
+#82 := (iff #50 #81)
+#79 := (iff #47 #78)
+#76 := (iff #42 #75)
+#73 := (iff #35 #69)
+#74 := [rewrite]: #73
+#66 := (iff #41 #56)
 #54 := (not #56)
-#69 := (or #56 #54)
-#73 := (iff #69 true)
-#74 := [rewrite]: #73
-#71 := (iff #42 #69)
-#70 := (iff #35 #54)
-#68 := [rewrite]: #70
-#66 := (iff #41 #56)
 #61 := (not #54)
 #64 := (iff #61 #56)
 #65 := [rewrite]: #64
@@ -7398,12 +7457,9 @@
 #60 := [rewrite]: #59
 #63 := [monotonicity #60]: #62
 #67 := [trans #63 #65]: #66
-#72 := [monotonicity #67 #68]: #71
-#76 := [trans #72 #74]: #75
-#79 := [quant-intro #76]: #78
-#83 := [trans #79 #81]: #82
-#86 := [monotonicity #83]: #85
-#90 := [trans #86 #88]: #89
+#77 := [monotonicity #67 #74]: #76
+#80 := [quant-intro #77]: #79
+#83 := [monotonicity #80]: #82
 #51 := (iff #15 #50)
 #48 := (iff #14 #47)
 #45 := (iff #13 #42)
@@ -7419,54 +7475,89 @@
 #46 := [trans #40 #44]: #45
 #49 := [quant-intro #46]: #48
 #52 := [monotonicity #49]: #51
-#92 := [trans #52 #90]: #91
+#85 := [trans #52 #83]: #84
 #31 := [asserted]: #15
-[mp #31 #92]: false
-unsat
-
-7GSX+dyn9XwHWNcjJ4X1ww 1400
+#86 := [mp #31 #85]: #81
+#106 := [mp~ #86 #103]: #101
+#107 := [mp #106 #144]: #142
+#146 := [not-or-elim #107]: #131
+#108 := (not #117)
+#145 := [not-or-elim #107]: #108
+[th-lemma #145 #146]: false
+unsat
+
+7GSX+dyn9XwHWNcjJ4X1ww 2292
 #2 := false
-#9 := (:var 0 int)
+#7 := 1::int
+decl ?x1!1 :: int
+#74 := ?x1!1
+#51 := -2::int
+#96 := (* -2::int ?x1!1)
+decl ?x2!0 :: int
+#73 := ?x2!0
 #4 := 2::int
-#10 := (* 2::int #9)
-#7 := 1::int
+#95 := (* 2::int ?x2!0)
+#97 := (+ #95 #96)
+#166 := (<= #97 1::int)
+#94 := (= #97 1::int)
+#53 := -1::int
+#75 := (* -2::int ?x2!0)
+#76 := (* 2::int ?x1!1)
+#77 := (+ #76 #75)
+#78 := (= #77 -1::int)
+#79 := (not #78)
+#80 := (not #79)
+#110 := (iff #80 #94)
+#102 := (not #94)
+#105 := (not #102)
+#108 := (iff #105 #94)
+#109 := [rewrite]: #108
+#106 := (iff #80 #105)
+#103 := (iff #79 #102)
+#100 := (iff #78 #94)
+#88 := (+ #75 #76)
+#91 := (= #88 -1::int)
+#98 := (iff #91 #94)
+#99 := [rewrite]: #98
+#92 := (iff #78 #91)
+#89 := (= #77 #88)
+#90 := [rewrite]: #89
+#93 := [monotonicity #90]: #92
+#101 := [trans #93 #99]: #100
+#104 := [monotonicity #101]: #103
+#107 := [monotonicity #104]: #106
+#111 := [trans #107 #109]: #110
+#9 := (:var 0 int)
+#55 := (* -2::int #9)
 #5 := (:var 1 int)
 #6 := (* 2::int #5)
+#56 := (+ #6 #55)
+#54 := (= #56 -1::int)
+#58 := (not #54)
+#61 := (forall (vars (?x1 int) (?x2 int)) #58)
+#64 := (not #61)
+#81 := (~ #64 #80)
+#82 := [sk]: #81
+#10 := (* 2::int #9)
 #8 := (+ #6 1::int)
 #11 := (= #8 #10)
 #12 := (not #11)
 #13 := (forall (vars (?x1 int) (?x2 int)) #12)
 #14 := (not #13)
-#74 := (iff #14 false)
+#67 := (iff #14 #64)
 #31 := (+ 1::int #6)
 #37 := (= #10 #31)
 #42 := (not #37)
 #45 := (forall (vars (?x1 int) (?x2 int)) #42)
 #48 := (not #45)
-#72 := (iff #48 false)
-#1 := true
-#67 := (not true)
-#70 := (iff #67 false)
-#71 := [rewrite]: #70
-#68 := (iff #48 #67)
-#65 := (iff #45 true)
-#60 := (forall (vars (?x1 int) (?x2 int)) true)
-#63 := (iff #60 true)
-#64 := [elim-unused]: #63
-#61 := (iff #45 #60)
-#58 := (iff #42 true)
-#51 := (not false)
-#56 := (iff #51 true)
-#57 := [rewrite]: #56
-#52 := (iff #42 #51)
-#53 := (iff #37 false)
-#54 := [rewrite]: #53
-#55 := [monotonicity #54]: #52
-#59 := [trans #55 #57]: #58
-#62 := [quant-intro #59]: #61
-#66 := [trans #62 #64]: #65
-#69 := [monotonicity #66]: #68
-#73 := [trans #69 #71]: #72
+#65 := (iff #48 #64)
+#62 := (iff #45 #61)
+#59 := (iff #42 #58)
+#52 := (iff #37 #54)
+#57 := [rewrite]: #52
+#60 := [monotonicity #57]: #59
+#63 := [quant-intro #60]: #62
+#66 := [monotonicity #63]: #65
 #49 := (iff #14 #48)
 #46 := (iff #13 #45)
 #43 := (iff #12 #42)
@@ -7482,9 +7573,19 @@
 #44 := [monotonicity #41]: #43
 #47 := [quant-intro #44]: #46
 #50 := [monotonicity #47]: #49
-#75 := [trans #50 #73]: #74
+#68 := [trans #50 #66]: #67
 #30 := [asserted]: #14
-[mp #30 #75]: false
+#69 := [mp #30 #68]: #64
+#85 := [mp~ #69 #82]: #80
+#86 := [mp #85 #111]: #94
+#168 := (or #102 #166)
+#169 := [th-lemma]: #168
+#170 := [unit-resolution #169 #86]: #166
+#167 := (>= #97 1::int)
+#171 := (or #102 #167)
+#172 := [th-lemma]: #171
+#173 := [unit-resolution #172 #86]: #167
+[th-lemma #173 #170]: false
 unsat
 
 oieid3+1h5s04LTQ9d796Q 2636
@@ -7960,38 +8061,62 @@
 [unit-resolution #585 #307]: false
 unsat
 
-4Dtb5Y1TTRPWZcHG9Griog 1594
+4Dtb5Y1TTRPWZcHG9Griog 2407
 #2 := false
+#104 := -1::int
+decl ?x1!1 :: int
+#86 := ?x1!1
+#106 := -4::int
+#107 := (* -4::int ?x1!1)
+decl ?x2!0 :: int
+#85 := ?x2!0
+#7 := 6::int
+#105 := (* 6::int ?x2!0)
+#108 := (+ #105 #107)
+#168 := (<= #108 -1::int)
+#109 := (= #108 -1::int)
 #12 := 1::int
+#33 := -6::int
+#87 := (* -6::int ?x2!0)
+#4 := 4::int
+#88 := (* 4::int ?x1!1)
+#89 := (+ #88 #87)
+#90 := (= #89 1::int)
+#112 := (iff #90 #109)
+#98 := (+ #87 #88)
+#101 := (= #98 1::int)
+#110 := (iff #101 #109)
+#111 := [rewrite]: #110
+#102 := (iff #90 #101)
+#99 := (= #89 #98)
+#100 := [rewrite]: #99
+#103 := [monotonicity #100]: #102
+#113 := [trans #103 #111]: #112
+#53 := (:var 0 int)
+#54 := (* -6::int #53)
 #9 := (:var 1 int)
-#7 := 6::int
+#55 := (* 4::int #9)
+#56 := (+ #55 #54)
+#76 := (= #56 1::int)
+#74 := (exists (vars (?x1 int) (?x2 int)) #76)
+#91 := (~ #74 #90)
+#92 := [sk]: #91
 #8 := (- 6::int)
 #10 := (* #8 #9)
 #5 := (:var 2 int)
-#4 := 4::int
 #6 := (* 4::int #5)
 #11 := (+ #6 #10)
 #13 := (= #11 1::int)
 #14 := (exists (vars (?x1 int) (?x2 int) (?x3 int)) #13)
 #15 := (not #14)
 #16 := (not #15)
-#82 := (iff #16 false)
-#53 := (:var 0 int)
-#33 := -6::int
-#54 := (* -6::int #53)
-#55 := (* 4::int #9)
-#56 := (+ #55 #54)
+#79 := (iff #16 #74)
 #57 := (= 1::int #56)
 #58 := (exists (vars (?x1 int) (?x2 int)) #57)
-#80 := (iff #58 false)
-#76 := (exists (vars (?x1 int) (?x2 int)) false)
-#78 := (iff #76 false)
-#79 := [elim-unused]: #78
-#77 := (iff #58 #76)
-#73 := (iff #57 false)
-#74 := [rewrite]: #73
-#75 := [quant-intro #74]: #77
-#81 := [trans #75 #79]: #80
+#77 := (iff #58 #74)
+#75 := (iff #57 #76)
+#73 := [rewrite]: #75
+#78 := [quant-intro #73]: #77
 #71 := (iff #16 #58)
 #63 := (not #58)
 #66 := (not #63)
@@ -8025,9 +8150,20 @@
 #65 := [monotonicity #62]: #64
 #68 := [monotonicity #65]: #67
 #72 := [trans #68 #70]: #71
-#83 := [trans #72 #81]: #82
+#80 := [trans #72 #78]: #79
 #32 := [asserted]: #16
-[mp #32 #83]: false
+#81 := [mp #32 #80]: #74
+#95 := [mp~ #81 #92]: #90
+#96 := [mp #95 #113]: #109
+#170 := (not #109)
+#171 := (or #170 #168)
+#172 := [th-lemma]: #171
+#173 := [unit-resolution #172 #96]: #168
+#169 := (>= #108 -1::int)
+#174 := (or #170 #169)
+#175 := [th-lemma]: #174
+#176 := [unit-resolution #175 #96]: #169
+[th-lemma #176 #173]: false
 unsat
 
 dbOre63OdVavsqL3lG2ttw 2516
@@ -8445,12 +8581,12 @@
 #46 := (+ #4 #45)
 #44 := (>= #46 0::int)
 #42 := (not #44)
-#57 := (or #44 #42)
-#61 := (iff #57 true)
+#60 := (or #44 #42)
+#61 := (iff #60 true)
 #62 := [rewrite]: #61
-#59 := (iff #32 #57)
+#56 := (iff #32 #60)
 #58 := (iff #11 #42)
-#56 := [rewrite]: #58
+#59 := [rewrite]: #58
 #54 := (iff #31 #44)
 #49 := (not #42)
 #52 := (iff #49 #44)
@@ -8460,8 +8596,8 @@
 #48 := [rewrite]: #47
 #51 := [monotonicity #48]: #50
 #55 := [trans #51 #53]: #54
-#60 := [monotonicity #55 #56]: #59
-#64 := [trans #60 #62]: #63
+#57 := [monotonicity #55 #59]: #56
+#64 := [trans #57 #62]: #63
 #67 := [quant-intro #64]: #66
 #71 := [trans #67 #69]: #70
 #74 := [monotonicity #71]: #73
@@ -8764,7 +8900,7 @@
 [mp #45 #150]: false
 unsat
 
-iPZ87GNdi7uQw4ehEpbTPQ 6383
+iPZ87GNdi7uQw4ehEpbTPQ 7012
 #2 := false
 #9 := 0::int
 decl uf_2 :: (-> T1 int)
@@ -8779,19 +8915,19 @@
 #295 := -1::int
 #274 := (* -1::int #293)
 #610 := (+ #24 #274)
-#594 := (<= #610 0::int)
+#315 := (<= #610 0::int)
 #612 := (= #610 0::int)
-#606 := (>= #23 0::int)
-#237 := (= #293 0::int)
-#549 := (not #237)
-#588 := (<= #293 0::int)
-#457 := (not #588)
+#255 := (>= #23 0::int)
+#317 := (= #293 0::int)
+#522 := (not #317)
+#577 := (<= #293 0::int)
+#519 := (not #577)
 #26 := 1::int
-#558 := (>= #293 1::int)
-#555 := (= #293 1::int)
+#553 := (>= #293 1::int)
+#552 := (= #293 1::int)
 #27 := (uf_1 1::int)
-#589 := (uf_2 #27)
-#301 := (= #589 1::int)
+#420 := (uf_2 #27)
+#565 := (= #420 1::int)
 #10 := (:var 0 int)
 #12 := (uf_1 #10)
 #626 := (pattern #12)
@@ -8847,57 +8983,57 @@
 #87 := [mp #51 #86]: #82
 #146 := [mp~ #87 #130]: #82
 #632 := [mp #146 #631]: #627
-#609 := (not #627)
-#578 := (or #609 #301)
-#311 := (>= 1::int 0::int)
-#585 := (not #311)
-#586 := (= 1::int #589)
-#590 := (or #586 #585)
-#419 := (or #609 #590)
-#421 := (iff #419 #578)
-#564 := (iff #578 #578)
-#565 := [rewrite]: #564
-#577 := (iff #590 #301)
-#574 := (or #301 false)
-#571 := (iff #574 #301)
-#576 := [rewrite]: #571
-#575 := (iff #590 #574)
-#584 := (iff #585 false)
+#237 := (not #627)
+#442 := (or #237 #565)
+#578 := (>= 1::int 0::int)
+#419 := (not #578)
+#421 := (= 1::int #420)
+#563 := (or #421 #419)
+#443 := (or #237 #563)
+#550 := (iff #443 #442)
+#547 := (iff #442 #442)
+#548 := [rewrite]: #547
+#559 := (iff #563 #565)
+#554 := (or #565 false)
+#558 := (iff #554 #565)
+#556 := [rewrite]: #558
+#555 := (iff #563 #554)
+#400 := (iff #419 false)
 #1 := true
-#582 := (not true)
-#583 := (iff #582 false)
-#580 := [rewrite]: #583
-#296 := (iff #585 #582)
-#303 := (iff #311 true)
-#581 := [rewrite]: #303
-#579 := [monotonicity #581]: #296
-#573 := [trans #579 #580]: #584
-#300 := (iff #586 #301)
-#302 := [rewrite]: #300
-#570 := [monotonicity #302 #573]: #575
-#572 := [trans #570 #576]: #577
-#563 := [monotonicity #572]: #421
-#566 := [trans #563 #565]: #421
-#420 := [quant-inst]: #419
-#560 := [mp #420 #566]: #578
-#442 := [unit-resolution #560 #632]: #301
-#443 := (= #293 #589)
+#567 := (not true)
+#569 := (iff #567 false)
+#398 := [rewrite]: #569
+#568 := (iff #419 #567)
+#560 := (iff #578 true)
+#561 := [rewrite]: #560
+#562 := [monotonicity #561]: #568
+#401 := [trans #562 #398]: #400
+#564 := (iff #421 #565)
+#566 := [rewrite]: #564
+#557 := [monotonicity #566 #401]: #555
+#441 := [trans #557 #556]: #559
+#452 := [monotonicity #441]: #550
+#551 := [trans #452 #548]: #550
+#402 := [quant-inst]: #443
+#436 := [mp #402 #551]: #442
+#524 := [unit-resolution #436 #632]: #565
+#526 := (= #293 #420)
 #28 := (= #25 #27)
 #129 := [asserted]: #28
-#436 := [monotonicity #129]: #443
-#451 := [trans #436 #442]: #555
-#453 := (not #555)
-#454 := (or #453 #558)
-#447 := [th-lemma]: #454
-#455 := [unit-resolution #447 #451]: #558
-#456 := (not #558)
-#458 := (or #456 #457)
-#459 := [th-lemma]: #458
-#552 := [unit-resolution #459 #455]: #457
-#553 := (or #549 #588)
-#540 := [th-lemma]: #553
-#542 := [unit-resolution #540 #552]: #549
-#603 := (or #237 #606)
+#527 := [monotonicity #129]: #526
+#528 := [trans #527 #524]: #552
+#529 := (not #552)
+#525 := (or #529 #553)
+#530 := [th-lemma]: #525
+#516 := [unit-resolution #530 #528]: #553
+#517 := (not #553)
+#520 := (or #517 #519)
+#521 := [th-lemma]: #520
+#518 := [unit-resolution #521 #516]: #519
+#502 := (or #522 #577)
+#503 := [th-lemma]: #502
+#505 := [unit-resolution #503 #518]: #522
+#300 := (or #255 #317)
 #18 := (= #13 0::int)
 #118 := (or #18 #70)
 #633 := (forall (vars (?x3 int)) (:pat #626) #118)
@@ -8954,71 +9090,95 @@
 #128 := [mp #88 #127]: #123
 #149 := [mp~ #128 #134]: #123
 #638 := [mp #149 #637]: #633
-#604 := (not #633)
-#602 := (or #604 #237 #606)
+#582 := (not #633)
+#296 := (or #582 #255 #317)
 #204 := (>= #24 0::int)
-#601 := (or #237 #204)
-#605 := (or #604 #601)
-#317 := (iff #605 #602)
-#592 := (or #604 #603)
-#315 := (iff #592 #602)
-#316 := [rewrite]: #315
-#299 := (iff #605 #592)
-#242 := (iff #601 #603)
-#279 := (iff #204 #606)
-#280 := [rewrite]: #279
-#243 := [monotonicity #280]: #242
-#314 := [monotonicity #243]: #299
-#210 := [trans #314 #316]: #317
-#591 := [quant-inst]: #605
-#587 := [mp #591 #210]: #602
-#534 := [unit-resolution #587 #638]: #603
-#531 := [unit-resolution #534 #542]: #606
-#613 := (not #606)
-#607 := (or #613 #612)
-#251 := (or #609 #613 #612)
+#210 := (or #317 #204)
+#579 := (or #582 #210)
+#570 := (iff #579 #296)
+#580 := (or #582 #300)
+#574 := (iff #580 #296)
+#575 := [rewrite]: #574
+#584 := (iff #579 #580)
+#303 := (iff #210 #300)
+#606 := (* 1::int #23)
+#279 := (>= #606 0::int)
+#311 := (or #279 #317)
+#301 := (iff #311 #300)
+#256 := (iff #279 #255)
+#251 := (= #606 #23)
+#593 := [rewrite]: #251
+#257 := [monotonicity #593]: #256
+#302 := [monotonicity #257]: #301
+#586 := (iff #210 #311)
+#587 := (or #317 #279)
+#585 := (iff #587 #311)
+#589 := [rewrite]: #585
+#588 := (iff #210 #587)
+#280 := (iff #204 #279)
+#613 := [rewrite]: #280
+#310 := [monotonicity #613]: #588
+#590 := [trans #310 #589]: #586
+#581 := [trans #590 #302]: #303
+#573 := [monotonicity #581]: #584
+#571 := [trans #573 #575]: #570
+#583 := [quant-inst]: #579
+#576 := [mp #583 #571]: #296
+#506 := [unit-resolution #576 #638]: #300
+#507 := [unit-resolution #506 #505]: #255
+#258 := (not #255)
+#597 := (or #258 #612)
+#601 := (or #237 #258 #612)
 #289 := (not #204)
 #294 := (= #24 #293)
 #291 := (or #294 #289)
-#593 := (or #609 #291)
-#597 := (iff #593 #251)
-#256 := (or #609 #607)
-#595 := (iff #256 #251)
-#596 := [rewrite]: #595
-#257 := (iff #593 #256)
-#608 := (iff #291 #607)
-#616 := (or #612 #613)
-#266 := (iff #616 #607)
-#271 := [rewrite]: #266
-#611 := (iff #291 #616)
-#614 := (iff #289 #613)
-#615 := [monotonicity #280]: #614
+#603 := (or #237 #291)
+#592 := (iff #603 #601)
+#243 := (or #237 #597)
+#605 := (iff #243 #601)
+#591 := [rewrite]: #605
+#604 := (iff #603 #243)
+#594 := (iff #291 #597)
+#614 := (not #279)
+#266 := (or #614 #612)
+#598 := (iff #266 #597)
+#595 := (iff #614 #258)
+#596 := [monotonicity #257]: #595
+#599 := [monotonicity #596]: #598
+#267 := (iff #291 #266)
+#611 := (or #612 #614)
+#271 := (iff #611 #266)
+#608 := [rewrite]: #271
+#617 := (iff #291 #611)
+#615 := (iff #289 #614)
+#616 := [monotonicity #613]: #615
 #268 := (iff #294 #612)
 #399 := [rewrite]: #268
-#617 := [monotonicity #399 #615]: #611
-#267 := [trans #617 #271]: #608
-#258 := [monotonicity #267]: #257
-#598 := [trans #258 #596]: #597
-#255 := [quant-inst]: #593
-#599 := [mp #255 #598]: #251
-#533 := [unit-resolution #599 #632]: #607
-#543 := [unit-resolution #533 #531]: #612
-#544 := (not #612)
-#545 := (or #544 #594)
-#541 := [th-lemma]: #545
-#546 := [unit-resolution #541 #543]: #594
-#600 := (>= #610 0::int)
-#535 := (or #544 #600)
-#536 := [th-lemma]: #535
-#537 := [unit-resolution #536 #543]: #600
-#557 := (<= #293 1::int)
-#538 := (or #453 #557)
-#532 := [th-lemma]: #538
-#539 := [unit-resolution #532 #451]: #557
-[th-lemma #455 #539 #537 #546]: false
-unsat
-
-kDuOn7kAggfP4Um8ghhv5A 5551
+#607 := [monotonicity #399 #616]: #617
+#609 := [trans #607 #608]: #267
+#600 := [trans #609 #599]: #594
+#602 := [monotonicity #600]: #604
+#299 := [trans #602 #591]: #592
+#242 := [quant-inst]: #603
+#314 := [mp #242 #299]: #601
+#508 := [unit-resolution #314 #632]: #597
+#509 := [unit-resolution #508 #507]: #612
+#510 := (not #612)
+#511 := (or #510 #315)
+#512 := [th-lemma]: #511
+#513 := [unit-resolution #512 #509]: #315
+#316 := (>= #610 0::int)
+#514 := (or #510 #316)
+#504 := [th-lemma]: #514
+#515 := [unit-resolution #504 #509]: #316
+#549 := (<= #293 1::int)
+#493 := (or #529 #549)
+#494 := [th-lemma]: #493
+#496 := [unit-resolution #494 #528]: #549
+[th-lemma #516 #496 #515 #513]: false
+unsat
+
+kDuOn7kAggfP4Um8ghhv5A 6068
 #2 := false
 #23 := 3::int
 decl uf_2 :: (-> T1 int)
@@ -9041,13 +9201,13 @@
 #632 := -1::int
 #634 := (* -1::int #28)
 #290 := (+ #26 #634)
-#623 := (>= #290 0::int)
+#609 := (>= #290 0::int)
 #421 := (= #290 0::int)
-#302 := (>= #22 0::int)
-#625 := (= #28 0::int)
-#318 := (not #625)
-#322 := (<= #28 0::int)
-#324 := (not #322)
+#273 := (>= #22 0::int)
+#610 := (= #28 0::int)
+#588 := (not #610)
+#441 := (<= #28 0::int)
+#443 := (not #441)
 #29 := 7::int
 #143 := (>= #28 7::int)
 #30 := (< #28 7::int)
@@ -9064,12 +9224,12 @@
 #151 := [trans #147 #149]: #150
 #133 := [asserted]: #31
 #152 := [mp #133 #151]: #143
-#325 := (or #324 #141)
-#603 := [th-lemma]: #325
-#604 := [unit-resolution #603 #152]: #324
-#601 := (or #318 #322)
-#605 := [th-lemma]: #601
-#602 := [unit-resolution #605 #604]: #318
+#585 := (or #443 #141)
+#586 := [th-lemma]: #585
+#587 := [unit-resolution #586 #152]: #443
+#582 := (or #588 #441)
+#583 := [th-lemma]: #582
+#589 := [unit-resolution #583 #587]: #588
 #10 := (:var 0 int)
 #12 := (uf_1 #10)
 #648 := (pattern #12)
@@ -9132,33 +9292,45 @@
 #131 := [mp #91 #130]: #126
 #172 := [mp~ #131 #155]: #126
 #660 := [mp #172 #659]: #655
-#337 := (not #655)
-#338 := (or #337 #302 #625)
+#605 := (not #655)
+#602 := (or #605 #273 #610)
 #315 := (>= #26 0::int)
-#264 := (or #625 #315)
-#339 := (or #337 #264)
-#611 := (iff #339 #338)
-#627 := (or #302 #625)
-#609 := (or #337 #627)
-#333 := (iff #609 #338)
-#607 := [rewrite]: #333
-#610 := (iff #339 #609)
-#321 := (iff #264 #627)
-#265 := (or #625 #302)
-#613 := (iff #265 #627)
-#614 := [rewrite]: #613
-#626 := (iff #264 #265)
-#635 := (iff #315 #302)
-#636 := [rewrite]: #635
-#624 := [monotonicity #636]: #626
-#336 := [trans #624 #614]: #321
-#332 := [monotonicity #336]: #610
-#608 := [trans #332 #607]: #611
-#231 := [quant-inst]: #339
-#612 := [mp #231 #608]: #338
-#606 := [unit-resolution #612 #660 #602]: #302
-#637 := (not #302)
-#293 := (or #637 #421)
+#332 := (or #610 #315)
+#606 := (or #605 #332)
+#599 := (iff #606 #602)
+#323 := (or #273 #610)
+#596 := (or #605 #323)
+#593 := (iff #596 #602)
+#598 := [rewrite]: #593
+#597 := (iff #606 #596)
+#318 := (iff #332 #323)
+#302 := 1::int
+#635 := (* 1::int #22)
+#636 := (>= #635 0::int)
+#333 := (or #610 #636)
+#603 := (iff #333 #323)
+#608 := (or #610 #273)
+#324 := (iff #608 #323)
+#325 := [rewrite]: #324
+#612 := (iff #333 #608)
+#615 := (iff #636 #273)
+#289 := (= #635 #22)
+#631 := [rewrite]: #289
+#277 := [monotonicity #631]: #615
+#322 := [monotonicity #277]: #612
+#604 := [trans #322 #325]: #603
+#607 := (iff #332 #333)
+#637 := (iff #315 #636)
+#638 := [rewrite]: #637
+#611 := [monotonicity #638]: #607
+#601 := [trans #611 #604]: #318
+#592 := [monotonicity #601]: #597
+#594 := [trans #592 #598]: #599
+#595 := [quant-inst]: #606
+#600 := [mp #595 #594]: #602
+#590 := [unit-resolution #600 #660 #589]: #273
+#278 := (not #273)
+#620 := (or #278 #421)
 #55 := (= #10 #13)
 #80 := (or #55 #74)
 #649 := (forall (vars (?x2 int)) (:pat #648) #80)
@@ -9208,39 +9380,47 @@
 #90 := [mp #54 #89]: #85
 #169 := [mp~ #90 #134]: #85
 #654 := [mp #169 #653]: #649
-#615 := (not #649)
-#277 := (or #615 #637 #421)
+#264 := (not #649)
+#265 := (or #264 #278 #421)
 #243 := (not #315)
 #317 := (= #26 #28)
 #296 := (or #317 #243)
-#278 := (or #615 #296)
-#621 := (iff #278 #277)
-#280 := (or #615 #293)
-#619 := (iff #280 #277)
-#620 := [rewrite]: #619
-#617 := (iff #278 #280)
-#631 := (iff #296 #293)
-#639 := (or #421 #637)
-#630 := (iff #639 #293)
-#289 := [rewrite]: #630
-#629 := (iff #296 #639)
-#638 := (iff #243 #637)
-#633 := [monotonicity #636]: #638
+#626 := (or #264 #296)
+#337 := (iff #626 #265)
+#627 := (or #264 #620)
+#321 := (iff #627 #265)
+#336 := [rewrite]: #321
+#613 := (iff #626 #627)
+#623 := (iff #296 #620)
+#633 := (not #636)
+#288 := (or #421 #633)
+#622 := (iff #288 #620)
+#617 := (or #421 #278)
+#621 := (iff #617 #620)
+#616 := [rewrite]: #621
+#618 := (iff #288 #617)
+#279 := (iff #633 #278)
+#280 := [monotonicity #277]: #279
+#619 := [monotonicity #280]: #618
+#259 := [trans #619 #616]: #622
+#293 := (iff #296 #288)
+#639 := (iff #243 #633)
+#629 := [monotonicity #638]: #639
 #628 := (iff #317 #421)
 #301 := [rewrite]: #628
-#288 := [monotonicity #301 #633]: #629
-#273 := [trans #288 #289]: #631
-#618 := [monotonicity #273]: #617
-#616 := [trans #618 #620]: #621
-#279 := [quant-inst]: #278
-#622 := [mp #279 #616]: #277
-#595 := [unit-resolution #622 #654]: #293
-#596 := [unit-resolution #595 #606]: #421
-#597 := (not #421)
-#592 := (or #597 #623)
-#593 := [th-lemma]: #592
-#598 := [unit-resolution #593 #596]: #623
-[th-lemma #152 #598 #139]: false
+#630 := [monotonicity #301 #629]: #293
+#625 := [trans #630 #259]: #623
+#614 := [monotonicity #625]: #613
+#338 := [trans #614 #336]: #337
+#624 := [quant-inst]: #626
+#339 := [mp #624 #338]: #265
+#584 := [unit-resolution #339 #654]: #620
+#591 := [unit-resolution #584 #590]: #421
+#420 := (not #421)
+#422 := (or #420 #609)
+#423 := [th-lemma]: #422
+#576 := [unit-resolution #423 #591]: #609
+[th-lemma #152 #576 #139]: false
 unsat
 
 aiB004AWADNjynNrqCDsxw 9284
@@ -9916,7 +10096,7 @@
 [th-lemma #623 #188 #601 #628]: false
 unsat
 
-ZcLxnpFewGGQ0H47MfRXGw 11816
+ZcLxnpFewGGQ0H47MfRXGw 12389
 #2 := false
 #9 := 0::int
 decl uf_2 :: (-> T1 int)
@@ -9930,8 +10110,8 @@
 #297 := (uf_2 #141)
 #357 := (= #297 0::int)
 #166 := (uf_1 0::int)
-#531 := (uf_2 #166)
-#537 := (= #531 0::int)
+#454 := (uf_2 #166)
+#515 := (= #454 0::int)
 #10 := (:var 0 int)
 #12 := (uf_1 #10)
 #672 := (pattern #12)
@@ -9988,40 +10168,40 @@
 #192 := [mp~ #95 #175]: #90
 #678 := [mp #192 #677]: #673
 #650 := (not #673)
-#528 := (or #650 #537)
-#529 := (>= 0::int 0::int)
-#530 := (not #529)
-#534 := (= 0::int #531)
-#535 := (or #534 #530)
-#508 := (or #650 #535)
-#509 := (iff #508 #528)
-#514 := (iff #528 #528)
-#515 := [rewrite]: #514
-#527 := (iff #535 #537)
-#520 := (or #537 false)
-#525 := (iff #520 #537)
-#526 := [rewrite]: #525
-#521 := (iff #535 #520)
-#519 := (iff #530 false)
+#468 := (or #650 #515)
+#528 := (>= 0::int 0::int)
+#508 := (not #528)
+#509 := (= 0::int #454)
+#490 := (or #509 #508)
+#469 := (or #650 #490)
+#471 := (iff #469 #468)
+#473 := (iff #468 #468)
+#474 := [rewrite]: #473
+#462 := (iff #490 #515)
+#495 := (or #515 false)
+#486 := (iff #495 #515)
+#507 := [rewrite]: #486
+#496 := (iff #490 #495)
+#492 := (iff #508 false)
 #1 := true
-#512 := (not true)
-#517 := (iff #512 false)
-#518 := [rewrite]: #517
-#513 := (iff #530 #512)
-#538 := (iff #529 true)
-#511 := [rewrite]: #538
-#406 := [monotonicity #511]: #513
-#524 := [trans #406 #518]: #519
-#536 := (iff #534 #537)
-#532 := [rewrite]: #536
-#522 := [monotonicity #532 #524]: #521
-#523 := [trans #522 #526]: #527
-#490 := [monotonicity #523]: #509
-#510 := [trans #490 #515]: #509
-#454 := [quant-inst]: #508
-#516 := [mp #454 #510]: #528
-#394 := [unit-resolution #516 #678]: #537
-#355 := (= #297 #531)
+#491 := (not true)
+#483 := (iff #491 false)
+#485 := [rewrite]: #483
+#450 := (iff #508 #491)
+#516 := (iff #528 true)
+#484 := [rewrite]: #516
+#481 := [monotonicity #484]: #450
+#494 := [trans #481 #485]: #492
+#514 := (iff #509 #515)
+#510 := [rewrite]: #514
+#506 := [monotonicity #510 #494]: #496
+#463 := [trans #506 #507]: #462
+#472 := [monotonicity #463]: #471
+#475 := [trans #472 #474]: #471
+#470 := [quant-inst]: #469
+#476 := [mp #470 #475]: #468
+#351 := [unit-resolution #476 #678]: #515
+#287 := (= #297 #454)
 #250 := (= #141 #166)
 #26 := 2::int
 #144 := (* 2::int #22)
@@ -10032,29 +10212,24 @@
 #161 := (uf_1 #156)
 #336 := (= #161 #166)
 #327 := (not #336)
-#588 := (uf_2 #161)
-#555 := (= #588 0::int)
-#398 := (= #588 #531)
-#395 := [hypothesis]: #336
-#387 := [monotonicity #395]: #398
-#399 := [trans #387 #394]: #555
-#390 := (not #555)
-#547 := (<= #588 0::int)
-#403 := (not #547)
-#595 := (>= #150 0::int)
-#302 := -1::int
-#618 := (* -1::int #150)
-#624 := (+ #144 #618)
-#488 := (<= #624 0::int)
-#465 := (= #624 0::int)
-#609 := (>= #22 0::int)
-#442 := (= #22 0::int)
+#568 := (uf_2 #161)
+#537 := (= #568 0::int)
+#354 := (= #568 #454)
+#352 := [hypothesis]: #336
+#344 := [monotonicity #352]: #354
+#355 := [trans #344 #351]: #537
+#368 := (not #537)
+#527 := (<= #568 0::int)
+#375 := (not #527)
+#566 := (>= #150 0::int)
+#447 := (>= #22 0::int)
+#421 := (= #22 0::int)
 #660 := (uf_1 #22)
-#495 := (uf_2 #660)
-#496 := (= #495 0::int)
-#612 := (not #609)
-#451 := [hypothesis]: #612
-#506 := (or #496 #609)
+#451 := (uf_2 #660)
+#452 := (= #451 0::int)
+#603 := (not #447)
+#424 := [hypothesis]: #603
+#455 := (or #447 #452)
 #18 := (= #13 0::int)
 #126 := (or #18 #78)
 #679 := (forall (vars (?x3 int)) (:pat #672) #126)
@@ -10112,15 +10287,23 @@
 #195 := [mp~ #136 #180]: #131
 #684 := [mp #195 #683]: #679
 #346 := (not #679)
-#462 := (or #346 #496 #609)
-#463 := (or #346 #506)
-#469 := (iff #463 #462)
-#470 := [rewrite]: #469
-#468 := [quant-inst]: #463
-#471 := [mp #468 #470]: #462
-#452 := [unit-resolution #471 #684]: #506
-#453 := [unit-resolution #452 #451]: #496
-#456 := (= #22 #495)
+#458 := (or #346 #447 #452)
+#453 := (or #452 #447)
+#459 := (or #346 #453)
+#434 := (iff #459 #458)
+#443 := (or #346 #455)
+#432 := (iff #443 #458)
+#433 := [rewrite]: #432
+#461 := (iff #459 #443)
+#456 := (iff #453 #455)
+#457 := [rewrite]: #456
+#431 := [monotonicity #457]: #461
+#436 := [trans #431 #433]: #434
+#460 := [quant-inst]: #459
+#437 := [mp #460 #436]: #458
+#420 := [unit-resolution #437 #684]: #455
+#425 := [unit-resolution #420 #424]: #452
+#405 := (= #22 #451)
 #661 := (= uf_3 #660)
 #4 := (:var 0 T1)
 #5 := (uf_2 #4)
@@ -10151,117 +10334,136 @@
 #663 := (not #665)
 #653 := (or #663 #661)
 #312 := [quant-inst]: #653
-#455 := [unit-resolution #312 #671]: #661
-#457 := [monotonicity #455]: #456
-#458 := [trans #457 #453]: #442
-#459 := (not #442)
-#460 := (or #459 #609)
-#443 := [th-lemma]: #460
-#461 := [unit-resolution #443 #451 #458]: false
-#431 := [lemma #461]: #609
-#613 := (or #465 #612)
-#615 := (or #650 #465 #612)
+#415 := [unit-resolution #312 #671]: #661
+#407 := [monotonicity #415]: #405
+#408 := [trans #407 #425]: #421
+#411 := (not #421)
+#412 := (or #411 #447)
+#416 := [th-lemma]: #412
+#409 := [unit-resolution #416 #424 #408]: false
+#417 := [lemma #409]: #447
+#302 := -1::int
+#618 := (* -1::int #150)
+#624 := (+ #144 #618)
+#595 := (<= #624 0::int)
+#465 := (= #624 0::int)
+#489 := (or #603 #465)
+#482 := (or #650 #603 #465)
 #616 := (>= #144 0::int)
 #617 := (not #616)
 #622 := (= #144 #150)
 #623 := (or #622 #617)
-#444 := (or #650 #623)
-#602 := (iff #444 #615)
-#447 := (or #650 #613)
-#603 := (iff #447 #615)
-#604 := [rewrite]: #603
-#600 := (iff #444 #447)
-#614 := (iff #623 #613)
-#606 := (iff #617 #612)
-#610 := (iff #616 #609)
-#611 := [rewrite]: #610
-#607 := [monotonicity #611]: #606
+#497 := (or #650 #623)
+#504 := (iff #497 #482)
+#500 := (or #650 #489)
+#502 := (iff #500 #482)
+#503 := [rewrite]: #502
+#493 := (iff #497 #500)
+#594 := (iff #623 #489)
+#609 := (* 1::int #22)
+#610 := (>= #609 0::int)
+#606 := (not #610)
+#614 := (or #465 #606)
+#498 := (iff #614 #489)
+#605 := (or #465 #603)
+#448 := (iff #605 #489)
+#596 := [rewrite]: #448
+#487 := (iff #614 #605)
+#604 := (iff #606 #603)
+#600 := (iff #610 #447)
+#444 := (= #609 #22)
+#446 := [rewrite]: #444
+#601 := [monotonicity #446]: #600
+#602 := [monotonicity #601]: #604
+#488 := [monotonicity #602]: #487
+#593 := [trans #488 #596]: #498
+#608 := (iff #623 #614)
+#607 := (iff #617 #606)
+#611 := (iff #616 #610)
+#612 := [rewrite]: #611
+#613 := [monotonicity #612]: #607
 #466 := (iff #622 #465)
 #467 := [rewrite]: #466
-#608 := [monotonicity #467 #607]: #614
-#601 := [monotonicity #608]: #600
-#605 := [trans #601 #604]: #602
-#446 := [quant-inst]: #444
-#487 := [mp #446 #605]: #615
-#439 := [unit-resolution #487 #678]: #613
-#435 := [unit-resolution #439 #431]: #465
-#440 := (not #465)
-#419 := (or #440 #488)
-#422 := [th-lemma]: #419
-#426 := [unit-resolution #422 #435]: #488
-#430 := (not #488)
-#433 := (or #595 #612 #430)
-#438 := [th-lemma]: #433
-#402 := [unit-resolution #438 #431 #426]: #595
-#590 := -3::int
-#579 := (* -1::int #588)
-#589 := (+ #150 #579)
-#553 := (<= #589 -3::int)
-#591 := (= #589 -3::int)
-#581 := (>= #150 -3::int)
+#615 := [monotonicity #467 #613]: #608
+#597 := [trans #615 #593]: #594
+#501 := [monotonicity #597]: #493
+#505 := [trans #501 #503]: #504
+#499 := [quant-inst]: #497
+#598 := [mp #499 #505]: #482
+#404 := [unit-resolution #598 #678]: #489
+#386 := [unit-resolution #404 #417]: #465
+#388 := (not #465)
+#389 := (or #388 #595)
+#390 := [th-lemma]: #389
+#391 := [unit-resolution #390 #386]: #595
+#395 := (not #595)
+#413 := (or #566 #603 #395)
+#403 := [th-lemma]: #413
+#373 := [unit-resolution #403 #391 #417]: #566
+#553 := -3::int
+#551 := (* -1::int #568)
+#552 := (+ #150 #551)
+#535 := (<= #552 -3::int)
+#554 := (= #552 -3::int)
+#557 := (>= #150 -3::int)
 #644 := (>= #22 -1::int)
-#428 := (or #612 #644)
-#429 := [th-lemma]: #428
-#427 := [unit-resolution #429 #431]: #644
+#392 := (or #603 #644)
+#393 := [th-lemma]: #392
+#394 := [unit-resolution #393 #417]: #644
 #646 := (not #644)
-#418 := (or #581 #646 #430)
-#421 := [th-lemma]: #418
-#423 := [unit-resolution #421 #426 #427]: #581
-#584 := (not #581)
-#573 := (or #584 #591)
-#562 := (or #650 #584 #591)
-#599 := (>= #156 0::int)
-#586 := (not #599)
-#580 := (= #156 #588)
-#577 := (or #580 #586)
-#563 := (or #650 #577)
-#549 := (iff #563 #562)
-#566 := (or #650 #573)
-#568 := (iff #566 #562)
-#548 := [rewrite]: #568
-#567 := (iff #563 #566)
-#571 := (iff #577 #573)
-#569 := (or #591 #584)
-#574 := (iff #569 #573)
-#575 := [rewrite]: #574
-#570 := (iff #577 #569)
-#578 := (iff #586 #584)
-#582 := (iff #599 #581)
-#583 := [rewrite]: #582
-#585 := [monotonicity #583]: #578
-#587 := (iff #580 #591)
-#592 := [rewrite]: #587
-#572 := [monotonicity #592 #585]: #570
-#576 := [trans #572 #575]: #571
-#564 := [monotonicity #576]: #567
-#551 := [trans #564 #548]: #549
-#565 := [quant-inst]: #563
-#552 := [mp #565 #551]: #562
-#424 := [unit-resolution #552 #678]: #573
-#420 := [unit-resolution #424 #423]: #591
-#425 := (not #591)
-#415 := (or #425 #553)
-#405 := [th-lemma]: #415
-#407 := [unit-resolution #405 #420]: #553
-#404 := (not #553)
-#401 := (not #595)
-#386 := (or #403 #401 #404)
-#388 := [th-lemma]: #386
-#389 := [unit-resolution #388 #407 #402]: #403
-#391 := (or #390 #547)
-#392 := [th-lemma]: #391
-#393 := [unit-resolution #392 #389]: #390
-#376 := [unit-resolution #393 #399]: false
-#378 := [lemma #376]: #327
+#396 := (or #557 #646 #395)
+#397 := [th-lemma]: #396
+#398 := [unit-resolution #397 #391 #394]: #557
+#560 := (not #557)
+#539 := (or #554 #560)
+#543 := (or #650 #554 #560)
+#567 := (>= #156 0::int)
+#564 := (not #567)
+#548 := (= #156 #568)
+#549 := (or #548 #564)
+#544 := (or #650 #549)
+#530 := (iff #544 #543)
+#546 := (or #650 #539)
+#533 := (iff #546 #543)
+#529 := [rewrite]: #533
+#541 := (iff #544 #546)
+#540 := (iff #549 #539)
+#550 := (iff #564 #560)
+#558 := (iff #567 #557)
+#559 := [rewrite]: #558
+#561 := [monotonicity #559]: #550
+#555 := (iff #548 #554)
+#556 := [rewrite]: #555
+#542 := [monotonicity #556 #561]: #540
+#547 := [monotonicity #542]: #541
+#531 := [trans #547 #529]: #530
+#545 := [quant-inst]: #544
+#534 := [mp #545 #531]: #543
+#387 := [unit-resolution #534 #678]: #539
+#399 := [unit-resolution #387 #398]: #554
+#376 := (not #554)
+#378 := (or #376 #535)
+#379 := [th-lemma]: #378
+#380 := [unit-resolution #379 #399]: #535
+#365 := (not #535)
+#364 := (not #566)
+#366 := (or #375 #364 #365)
+#358 := [th-lemma]: #366
+#367 := [unit-resolution #358 #380 #373]: #375
+#359 := (or #368 #527)
+#369 := [th-lemma]: #359
+#350 := [unit-resolution #369 #367]: #368
+#321 := [unit-resolution #350 #355]: false
+#323 := [lemma #321]: #327
 #249 := (= #141 #161)
 #334 := (not #249)
-#396 := (= #297 #588)
-#385 := [hypothesis]: #249
-#370 := [monotonicity #385]: #396
-#380 := (not #396)
-#434 := (+ #297 #579)
-#280 := (>= #434 0::int)
-#414 := (not #280)
+#343 := (= #297 #568)
+#322 := [hypothesis]: #249
+#333 := [monotonicity #322]: #343
+#315 := (not #343)
+#414 := (+ #297 #551)
+#401 := (>= #414 0::int)
+#372 := (not #401)
 #303 := (* -1::int #297)
 #304 := (+ #22 #303)
 #356 := (>= #304 -1::int)
@@ -10290,21 +10492,21 @@
 #256 := [trans #360 #362]: #363
 #637 := [quant-inst]: #651
 #633 := [mp #637 #256]: #648
-#408 := [unit-resolution #633 #678]: #649
-#411 := [unit-resolution #408 #427]: #641
-#412 := (not #641)
-#416 := (or #412 #356)
-#409 := [th-lemma]: #416
-#417 := [unit-resolution #409 #411]: #356
-#410 := [hypothesis]: #280
-#413 := [th-lemma #423 #410 #417 #407 #426]: false
-#400 := [lemma #413]: #414
-#381 := (or #380 #280)
-#382 := [th-lemma]: #381
-#377 := [unit-resolution #382 #400]: #380
-#371 := [unit-resolution #377 #370]: false
-#372 := [lemma #371]: #334
-#352 := (or #249 #250 #336)
+#381 := [unit-resolution #633 #678]: #649
+#382 := [unit-resolution #381 #394]: #641
+#383 := (not #641)
+#384 := (or #383 #356)
+#377 := [th-lemma]: #384
+#385 := [unit-resolution #377 #382]: #356
+#370 := [hypothesis]: #401
+#371 := [th-lemma #398 #370 #385 #380 #391]: false
+#374 := [lemma #371]: #372
+#328 := (or #315 #401)
+#329 := [th-lemma]: #328
+#332 := [unit-resolution #329 #374]: #315
+#316 := [unit-resolution #332 #333]: false
+#318 := [lemma #316]: #334
+#295 := (or #249 #250 #336)
 #335 := (not #250)
 #338 := (and #334 #335 #327)
 #339 := (not #338)
@@ -10352,28 +10554,28 @@
 #177 := [mp #137 #174]: #172
 #326 := (or #169 #339)
 #659 := [def-axiom]: #326
-#351 := [unit-resolution #659 #177]: #339
+#294 := [unit-resolution #659 #177]: #339
 #314 := (or #338 #249 #250 #336)
 #445 := [def-axiom]: #314
-#343 := [unit-resolution #445 #351]: #352
-#353 := [unit-resolution #343 #372 #378]: #250
-#321 := [monotonicity #353]: #355
-#323 := [trans #321 #394]: #357
-#368 := (not #357)
+#293 := [unit-resolution #445 #294]: #295
+#296 := [unit-resolution #293 #318 #323]: #250
+#290 := [monotonicity #296]: #287
+#285 := [trans #290 #351]: #357
+#310 := (not #357)
 #620 := (<= #297 0::int)
-#364 := (not #620)
+#305 := (not #620)
 #634 := (<= #304 -1::int)
-#374 := (or #412 #634)
-#373 := [th-lemma]: #374
-#375 := [unit-resolution #373 #411]: #634
-#365 := (not #634)
-#366 := (or #364 #612 #365)
-#358 := [th-lemma]: #366
-#367 := [unit-resolution #358 #375 #431]: #364
-#359 := (or #368 #620)
-#369 := [th-lemma]: #359
-#350 := [unit-resolution #369 #367]: #368
-[unit-resolution #350 #323]: false
+#319 := (or #383 #634)
+#298 := [th-lemma]: #319
+#300 := [unit-resolution #298 #382]: #634
+#306 := (not #634)
+#307 := (or #305 #603 #306)
+#308 := [th-lemma]: #307
+#309 := [unit-resolution #308 #300 #417]: #305
+#299 := (or #310 #620)
+#311 := [th-lemma]: #299
+#292 := [unit-resolution #311 #309]: #310
+[unit-resolution #292 #285]: false
 unsat
 
 ipe8HUL/t33OoeNl/z0smQ 4011
@@ -10539,7 +10741,7 @@
 [th-lemma #656 #361 #261]: false
 unsat
 
-eRjXXrQSzpzyc8Ro409d3Q 14366
+9FrZeHP8ZKJM+JmhfAjimQ 14889
 #2 := false
 #9 := 0::int
 decl uf_2 :: (-> T1 int)
@@ -10551,46 +10753,46 @@
 #38 := (* 4::int #37)
 #39 := (uf_1 #38)
 #40 := (uf_2 #39)
-#527 := (= #40 0::int)
-#976 := (not #527)
-#502 := (<= #40 0::int)
-#971 := (not #502)
+#504 := (= #40 0::int)
+#995 := (not #504)
+#475 := (<= #40 0::int)
+#990 := (not #475)
 #22 := 1::int
 #186 := (+ 1::int #40)
 #189 := (uf_1 #186)
-#506 := (uf_2 #189)
-#407 := (<= #506 1::int)
-#876 := (not #407)
+#467 := (uf_2 #189)
+#380 := (<= #467 1::int)
+#893 := (not #380)
 decl up_4 :: (-> T1 T1 bool)
 #4 := (:var 0 T1)
-#408 := (up_4 #4 #189)
-#393 := (pattern #408)
-#413 := (= #4 #189)
-#414 := (not #408)
+#386 := (up_4 #4 #189)
+#374 := (pattern #386)
+#382 := (not #386)
+#385 := (= #4 #189)
 #26 := (uf_1 1::int)
 #27 := (= #4 #26)
-#392 := (or #27 #414 #413)
-#397 := (forall (vars (?x5 T1)) (:pat #393) #392)
-#383 := (not #397)
-#382 := (or #383 #407)
-#375 := (not #382)
+#845 := (or #27 #385 #382)
+#848 := (forall (vars (?x5 T1)) (:pat #374) #845)
+#851 := (not #848)
+#854 := (or #380 #851)
+#857 := (not #854)
 decl up_3 :: (-> T1 bool)
 #192 := (up_3 #189)
-#404 := (not #192)
-#841 := (or #404 #375)
+#840 := (not #192)
+#860 := (or #840 #857)
 decl ?x5!0 :: (-> T1 T1)
-#422 := (?x5!0 #189)
-#434 := (= #189 #422)
-#417 := (up_4 #422 #189)
-#418 := (not #417)
-#415 := (= #26 #422)
-#847 := (or #415 #418 #434)
-#850 := (not #847)
-#853 := (or #192 #407 #850)
-#856 := (not #853)
-#844 := (not #841)
-#859 := (or #844 #856)
-#862 := (not #859)
+#392 := (?x5!0 #189)
+#397 := (up_4 #392 #189)
+#390 := (not #397)
+#396 := (= #26 #392)
+#395 := (= #189 #392)
+#866 := (or #395 #396 #390)
+#869 := (not #866)
+#872 := (or #192 #380 #869)
+#875 := (not #872)
+#863 := (not #860)
+#878 := (or #863 #875)
+#881 := (not #878)
 #5 := (uf_2 #4)
 #787 := (pattern #5)
 #21 := (up_3 #4)
@@ -10769,64 +10971,59 @@
 #314 := [mp #267 #313]: #311
 #839 := [mp #314 #838]: #836
 #589 := (not #836)
-#865 := (or #589 #862)
-#416 := (or #418 #415 #434)
-#419 := (not #416)
-#409 := (or #192 #407 #419)
-#410 := (not #409)
-#389 := (or #414 #27 #413)
-#394 := (forall (vars (?x5 T1)) (:pat #393) #389)
-#399 := (not #394)
-#401 := (or #407 #399)
-#402 := (not #401)
-#400 := (or #404 #402)
-#405 := (not #400)
-#388 := (or #405 #410)
-#391 := (not #388)
-#866 := (or #589 #391)
-#868 := (iff #866 #865)
-#870 := (iff #865 #865)
-#871 := [rewrite]: #870
-#863 := (iff #391 #862)
-#860 := (iff #388 #859)
-#857 := (iff #410 #856)
-#854 := (iff #409 #853)
-#851 := (iff #419 #850)
-#848 := (iff #416 #847)
-#849 := [rewrite]: #848
-#852 := [monotonicity #849]: #851
-#855 := [monotonicity #852]: #854
-#858 := [monotonicity #855]: #857
-#845 := (iff #405 #844)
-#842 := (iff #400 #841)
-#378 := (iff #402 #375)
-#376 := (iff #401 #382)
-#384 := (or #407 #383)
-#387 := (iff #384 #382)
-#374 := [rewrite]: #387
-#385 := (iff #401 #384)
-#380 := (iff #399 #383)
-#390 := (iff #394 #397)
-#395 := (iff #389 #392)
-#396 := [rewrite]: #395
-#398 := [quant-intro #396]: #390
-#381 := [monotonicity #398]: #380
-#386 := [monotonicity #381]: #385
-#377 := [trans #386 #374]: #376
-#840 := [monotonicity #377]: #378
-#843 := [monotonicity #840]: #842
-#846 := [monotonicity #843]: #845
-#861 := [monotonicity #846 #858]: #860
-#864 := [monotonicity #861]: #863
-#869 := [monotonicity #864]: #868
-#872 := [trans #869 #871]: #868
-#867 := [quant-inst]: #866
-#873 := [mp #867 #872]: #865
-#947 := [unit-resolution #873 #839]: #862
-#905 := (or #859 #841)
-#906 := [def-axiom]: #905
-#948 := [unit-resolution #906 #947]: #841
-#951 := (or #844 #375)
+#884 := (or #589 #881)
+#398 := (or #390 #396 #395)
+#383 := (not #398)
+#381 := (or #192 #380 #383)
+#384 := (not #381)
+#387 := (or #382 #27 #385)
+#376 := (forall (vars (?x5 T1)) (:pat #374) #387)
+#377 := (not #376)
+#375 := (or #380 #377)
+#378 := (not #375)
+#841 := (or #840 #378)
+#842 := (not #841)
+#843 := (or #842 #384)
+#844 := (not #843)
+#885 := (or #589 #844)
+#887 := (iff #885 #884)
+#889 := (iff #884 #884)
+#890 := [rewrite]: #889
+#882 := (iff #844 #881)
+#879 := (iff #843 #878)
+#876 := (iff #384 #875)
+#873 := (iff #381 #872)
+#870 := (iff #383 #869)
+#867 := (iff #398 #866)
+#868 := [rewrite]: #867
+#871 := [monotonicity #868]: #870
+#874 := [monotonicity #871]: #873
+#877 := [monotonicity #874]: #876
+#864 := (iff #842 #863)
+#861 := (iff #841 #860)
+#858 := (iff #378 #857)
+#855 := (iff #375 #854)
+#852 := (iff #377 #851)
+#849 := (iff #376 #848)
+#846 := (iff #387 #845)
+#847 := [rewrite]: #846
+#850 := [quant-intro #847]: #849
+#853 := [monotonicity #850]: #852
+#856 := [monotonicity #853]: #855
+#859 := [monotonicity #856]: #858
+#862 := [monotonicity #859]: #861
+#865 := [monotonicity #862]: #864
+#880 := [monotonicity #865 #877]: #879
+#883 := [monotonicity #880]: #882
+#888 := [monotonicity #883]: #887
+#891 := [trans #888 #890]: #887
+#886 := [quant-inst]: #885
+#892 := [mp #886 #891]: #884
+#966 := [unit-resolution #892 #839]: #881
+#924 := (or #878 #860)
+#925 := [def-axiom]: #924
+#967 := [unit-resolution #925 #966]: #860
+#970 := (or #863 #857)
 #41 := (+ #40 1::int)
 #42 := (uf_1 #41)
 #43 := (up_3 #42)
@@ -10838,30 +11035,30 @@
 #194 := [monotonicity #191]: #193
 #185 := [asserted]: #43
 #197 := [mp #185 #194]: #192
-#885 := (or #844 #404 #375)
-#886 := [def-axiom]: #885
-#952 := [unit-resolution #886 #197]: #951
-#953 := [unit-resolution #952 #948]: #375
-#877 := (or #382 #876)
-#878 := [def-axiom]: #877
-#954 := [unit-resolution #878 #953]: #876
+#904 := (or #863 #840 #857)
+#905 := [def-axiom]: #904
+#971 := [unit-resolution #905 #197]: #970
+#972 := [unit-resolution #971 #967]: #857
+#894 := (or #854 #893)
+#895 := [def-axiom]: #894
+#973 := [unit-resolution #895 #972]: #893
 #542 := -1::int
-#508 := (* -1::int #506)
-#493 := (+ #40 #508)
-#438 := (>= #493 -1::int)
-#494 := (= #493 -1::int)
-#496 := (>= #40 -1::int)
-#451 := (= #506 0::int)
-#959 := (not #451)
-#432 := (<= #506 0::int)
-#955 := (not #432)
-#956 := (or #955 #407)
-#957 := [th-lemma]: #956
-#958 := [unit-resolution #957 #954]: #955
-#960 := (or #959 #432)
-#961 := [th-lemma]: #960
-#962 := [unit-resolution #961 #958]: #959
-#453 := (or #451 #496)
+#446 := (* -1::int #467)
+#447 := (+ #40 #446)
+#416 := (>= #447 -1::int)
+#438 := (= #447 -1::int)
+#453 := (>= #40 -1::int)
+#419 := (= #467 0::int)
+#978 := (not #419)
+#388 := (<= #467 0::int)
+#974 := (not #388)
+#975 := (or #974 #380)
+#976 := [th-lemma]: #975
+#977 := [unit-resolution #976 #973]: #974
+#979 := (or #978 #388)
+#980 := [th-lemma]: #979
+#981 := [unit-resolution #980 #977]: #978
+#409 := (or #419 #453)
 #10 := (:var 0 int)
 #12 := (uf_1 #10)
 #795 := (pattern #12)
@@ -10924,28 +11121,28 @@
 #145 := [mp #105 #144]: #140
 #227 := [mp~ #145 #208]: #140
 #807 := [mp #227 #806]: #802
-#514 := (not #802)
-#445 := (or #514 #451 #496)
-#504 := (>= #186 0::int)
-#452 := (or #451 #504)
-#456 := (or #514 #452)
-#429 := (iff #456 #445)
-#441 := (or #514 #453)
-#423 := (iff #441 #445)
-#428 := [rewrite]: #423
-#442 := (iff #456 #441)
-#454 := (iff #452 #453)
-#498 := (iff #504 #496)
-#487 := [rewrite]: #498
-#455 := [monotonicity #487]: #454
-#421 := [monotonicity #455]: #442
-#430 := [trans #421 #428]: #429
-#439 := [quant-inst]: #456
-#431 := [mp #439 #430]: #445
-#963 := [unit-resolution #431 #807]: #453
-#964 := [unit-resolution #963 #962]: #496
-#488 := (not #496)
-#490 := (or #494 #488)
+#496 := (not #802)
+#408 := (or #496 #419 #453)
+#476 := (>= #186 0::int)
+#407 := (or #419 #476)
+#414 := (or #496 #407)
+#404 := (iff #414 #408)
+#393 := (or #496 #409)
+#401 := (iff #393 #408)
+#402 := [rewrite]: #401
+#394 := (iff #414 #393)
+#410 := (iff #407 #409)
+#454 := (iff #476 #453)
+#455 := [rewrite]: #454
+#413 := [monotonicity #455]: #410
+#399 := [monotonicity #413]: #394
+#400 := [trans #399 #402]: #404
+#389 := [quant-inst]: #414
+#405 := [mp #389 #400]: #408
+#982 := [unit-resolution #405 #807]: #409
+#983 := [unit-resolution #982 #981]: #453
+#445 := (not #453)
+#441 := (or #438 #445)
 #69 := (= #10 #13)
 #94 := (or #69 #88)
 #796 := (forall (vars (?x2 int)) (:pat #795) #94)
@@ -10995,48 +11192,48 @@
 #104 := [mp #68 #103]: #99
 #224 := [mp~ #104 #196]: #99
 #801 := [mp #224 #800]: #796
-#530 := (not #796)
-#492 := (or #530 #494 #488)
-#505 := (not #504)
-#507 := (= #186 #506)
-#500 := (or #507 #505)
-#473 := (or #530 #500)
-#478 := (iff #473 #492)
-#475 := (or #530 #490)
-#477 := (iff #475 #492)
-#467 := [rewrite]: #477
-#466 := (iff #473 #475)
-#491 := (iff #500 #490)
-#489 := (iff #505 #488)
-#481 := [monotonicity #487]: #489
-#495 := (iff #507 #494)
-#497 := [rewrite]: #495
-#482 := [monotonicity #497 #481]: #491
-#476 := [monotonicity #482]: #466
-#444 := [trans #476 #467]: #478
-#474 := [quant-inst]: #473
-#446 := [mp #474 #444]: #492
-#965 := [unit-resolution #446 #801]: #490
-#966 := [unit-resolution #965 #964]: #494
-#967 := (not #494)
-#968 := (or #967 #438)
-#969 := [th-lemma]: #968
-#970 := [unit-resolution #969 #966]: #438
-#972 := (not #438)
-#973 := (or #971 #407 #972)
-#974 := [th-lemma]: #973
-#975 := [unit-resolution #974 #970 #954]: #971
-#977 := (or #976 #502)
-#978 := [th-lemma]: #977
-#979 := [unit-resolution #978 #975]: #976
-#553 := (>= #37 0::int)
-#546 := (not #553)
+#514 := (not #796)
+#423 := (or #514 #438 #445)
+#477 := (not #476)
+#478 := (= #186 #467)
+#444 := (or #478 #477)
+#428 := (or #514 #444)
+#434 := (iff #428 #423)
+#430 := (or #514 #441)
+#433 := (iff #430 #423)
+#422 := [rewrite]: #433
+#431 := (iff #428 #430)
+#442 := (iff #444 #441)
+#456 := (iff #477 #445)
+#439 := [monotonicity #455]: #456
+#451 := (iff #478 #438)
+#452 := [rewrite]: #451
+#421 := [monotonicity #452 #439]: #442
+#432 := [monotonicity #421]: #431
+#415 := [trans #432 #422]: #434
+#429 := [quant-inst]: #428
+#417 := [mp #429 #415]: #423
+#984 := [unit-resolution #417 #801]: #441
+#985 := [unit-resolution #984 #983]: #438
+#986 := (not #438)
+#987 := (or #986 #416)
+#988 := [th-lemma]: #987
+#989 := [unit-resolution #988 #985]: #416
+#991 := (not #416)
+#992 := (or #990 #380 #991)
+#993 := [th-lemma]: #992
+#994 := [unit-resolution #993 #989 #973]: #990
+#996 := (or #995 #475)
+#997 := [th-lemma]: #996
+#998 := [unit-resolution #997 #994]: #995
+#536 := (>= #37 0::int)
+#525 := (not #536)
 #545 := (* -1::int #40)
 #549 := (+ #38 #545)
 #551 := (= #549 0::int)
-#984 := (not #551)
-#524 := (>= #549 0::int)
-#980 := (not #524)
+#1003 := (not #551)
+#503 := (>= #549 0::int)
+#999 := (not #503)
 #201 := (>= #37 1::int)
 #202 := (not #201)
 #44 := (<= 1::int #37)
@@ -11047,55 +11244,79 @@
 #204 := [monotonicity #200]: #203
 #195 := [asserted]: #45
 #205 := [mp #195 #204]: #202
-#981 := (or #980 #201 #407 #972)
-#982 := [th-lemma]: #981
-#983 := [unit-resolution #982 #205 #970 #954]: #980
-#985 := (or #984 #524)
-#986 := [th-lemma]: #985
-#987 := [unit-resolution #986 #983]: #984
-#548 := (or #551 #546)
-#531 := (or #530 #551 #546)
+#1000 := (or #999 #201 #380 #991)
+#1001 := [th-lemma]: #1000
+#1002 := [unit-resolution #1001 #205 #989 #973]: #999
+#1004 := (or #1003 #503)
+#1005 := [th-lemma]: #1004
+#1006 := [unit-resolution #1005 #1002]: #1003
+#527 := (or #525 #551)
+#515 := (or #514 #525 #551)
 #403 := (>= #38 0::int)
 #562 := (not #403)
 #558 := (= #38 #40)
 #563 := (or #558 #562)
-#534 := (or #530 #563)
-#537 := (iff #534 #531)
-#539 := (or #530 #548)
-#533 := (iff #539 #531)
-#536 := [rewrite]: #533
-#532 := (iff #534 #539)
-#538 := (iff #563 #548)
-#547 := (iff #562 #546)
-#541 := (iff #403 #553)
-#544 := [rewrite]: #541
-#543 := [monotonicity #544]: #547
-#552 := (iff #558 #551)
-#550 := [rewrite]: #552
-#528 := [monotonicity #550 #543]: #538
-#540 := [monotonicity #528]: #532
-#523 := [trans #540 #536]: #537
-#535 := [quant-inst]: #534
-#525 := [mp #535 #523]: #531
-#988 := [unit-resolution #525 #801]: #548
-#989 := [unit-resolution #988 #987]: #546
-#511 := (or #527 #553)
-#515 := (or #514 #527 #553)
-#509 := (or #527 #403)
-#516 := (or #514 #509)
+#516 := (or #514 #563)
 #522 := (iff #516 #515)
-#518 := (or #514 #511)
+#518 := (or #514 #527)
 #521 := (iff #518 #515)
 #510 := [rewrite]: #521
 #519 := (iff #516 #518)
-#512 := (iff #509 #511)
-#513 := [monotonicity #544]: #512
+#512 := (iff #563 #527)
+#553 := (* 1::int #37)
+#541 := (>= #553 0::int)
+#547 := (not #541)
+#531 := (or #547 #551)
+#509 := (iff #531 #527)
+#526 := (iff #547 #525)
+#537 := (iff #541 #536)
+#540 := (= #553 #37)
+#533 := [rewrite]: #540
+#523 := [monotonicity #533]: #537
+#524 := [monotonicity #523]: #526
+#511 := [monotonicity #524]: #509
+#539 := (iff #563 #531)
+#538 := (or #551 #547)
+#534 := (iff #538 #531)
+#535 := [rewrite]: #534
+#528 := (iff #563 #538)
+#543 := (iff #562 #547)
+#544 := (iff #403 #541)
+#546 := [rewrite]: #544
+#548 := [monotonicity #546]: #543
+#552 := (iff #558 #551)
+#550 := [rewrite]: #552
+#530 := [monotonicity #550 #548]: #528
+#532 := [trans #530 #535]: #539
+#513 := [trans #532 #511]: #512
 #520 := [monotonicity #513]: #519
 #499 := [trans #520 #510]: #522
 #517 := [quant-inst]: #516
 #501 := [mp #517 #499]: #515
-#990 := [unit-resolution #501 #807]: #511
-[unit-resolution #990 #989 #979]: false
+#1007 := [unit-resolution #501 #801]: #527
+#1008 := [unit-resolution #1007 #1006]: #525
+#508 := (or #504 #536)
+#498 := (or #496 #504 #536)
+#505 := (or #504 #403)
+#487 := (or #496 #505)
+#492 := (iff #487 #498)
+#489 := (or #496 #508)
+#491 := (iff #489 #498)
+#482 := [rewrite]: #491
+#481 := (iff #487 #489)
+#495 := (iff #505 #508)
+#506 := (or #504 #541)
+#493 := (iff #506 #508)
+#494 := [monotonicity #523]: #493
+#507 := (iff #505 #506)
+#500 := [monotonicity #546]: #507
+#497 := [trans #500 #494]: #495
+#490 := [monotonicity #497]: #481
+#473 := [trans #490 #482]: #492
+#488 := [quant-inst]: #487
+#474 := [mp #488 #473]: #498
+#1009 := [unit-resolution #474 #807]: #508
+[unit-resolution #1009 #1008 #998]: false
 unsat
 
 uq2MbDTgTG1nxWdwzZtWew 7
@@ -12233,7 +12454,7 @@
 [mp #25 #34]: false
 unsat
 
-YG20f6Uf93koN6rVg/alpA 9362
+YG20f6Uf93koN6rVg/alpA 9742
 #2 := false
 decl uf_1 :: (-> int T1)
 #37 := 6::int
@@ -12248,18 +12469,18 @@
 #35 := (uf_1 #34)
 #36 := (uf_3 #35)
 #39 := (= #36 #38)
-#476 := (uf_3 #38)
-#403 := (= #476 #38)
-#531 := (= #38 #476)
-#620 := (uf_2 #38)
+#484 := (uf_3 #38)
+#372 := (= #484 #38)
+#485 := (= #38 #484)
+#592 := (uf_2 #38)
 #142 := -10::int
-#513 := (+ -10::int #620)
-#472 := (uf_1 #513)
-#503 := (uf_3 #472)
-#505 := (= #476 #503)
+#496 := (+ -10::int #592)
+#497 := (uf_1 #496)
+#498 := (uf_3 #497)
+#499 := (= #484 #498)
 #22 := 10::int
-#507 := (>= #620 10::int)
-#514 := (ite #507 #505 #531)
+#500 := (>= #592 10::int)
+#501 := (ite #500 #499 #485)
 #4 := (:var 0 T1)
 #21 := (uf_3 #4)
 #707 := (pattern #21)
@@ -12333,12 +12554,12 @@
 #212 := [mp #207 #211]: #193
 #713 := [mp #212 #712]: #708
 #336 := (not #708)
-#518 := (or #336 #514)
-#528 := [quant-inst]: #518
-#477 := [unit-resolution #528 #713]: #514
-#529 := (not #507)
-#498 := (<= #620 6::int)
-#610 := (= #620 6::int)
+#463 := (or #336 #501)
+#464 := [quant-inst]: #463
+#444 := [unit-resolution #464 #713]: #501
+#473 := (not #500)
+#453 := (<= #592 6::int)
+#597 := (= #592 6::int)
 #10 := (:var 0 int)
 #12 := (uf_1 #10)
 #694 := (pattern #12)
@@ -12396,79 +12617,79 @@
 #201 := [mp~ #99 #183]: #94
 #700 := [mp #201 #699]: #695
 #673 := (not #695)
-#591 := (or #673 #610)
-#526 := (>= 6::int 0::int)
-#527 := (not #526)
-#617 := (= 6::int #620)
-#621 := (or #617 #527)
-#592 := (or #673 #621)
-#595 := (iff #592 #591)
-#597 := (iff #591 #591)
-#593 := [rewrite]: #597
-#600 := (iff #621 #610)
-#614 := (or #610 false)
-#605 := (iff #614 #610)
-#606 := [rewrite]: #605
-#603 := (iff #621 #614)
-#613 := (iff #527 false)
+#576 := (or #673 #597)
+#607 := (>= 6::int 0::int)
+#591 := (not #607)
+#594 := (= 6::int #592)
+#595 := (or #594 #591)
+#577 := (or #673 #595)
+#579 := (iff #577 #576)
+#581 := (iff #576 #576)
+#582 := [rewrite]: #581
+#574 := (iff #595 #597)
+#586 := (or #597 false)
+#571 := (iff #586 #597)
+#573 := [rewrite]: #571
+#590 := (iff #595 #586)
+#588 := (iff #591 false)
 #1 := true
 #663 := (not true)
 #666 := (iff #663 false)
 #667 := [rewrite]: #666
-#611 := (iff #527 #663)
-#599 := (iff #526 true)
-#601 := [rewrite]: #599
-#612 := [monotonicity #601]: #611
-#609 := [trans #612 #667]: #613
-#608 := (iff #617 #610)
-#602 := [rewrite]: #608
-#604 := [monotonicity #602 #609]: #603
-#607 := [trans #604 #606]: #600
-#596 := [monotonicity #607]: #595
-#598 := [trans #596 #593]: #595
-#594 := [quant-inst]: #592
-#584 := [mp #594 #598]: #591
-#478 := [unit-resolution #584 #700]: #610
-#453 := (not #610)
-#454 := (or #453 #498)
-#455 := [th-lemma]: #454
-#456 := [unit-resolution #455 #478]: #498
-#458 := (not #498)
-#459 := (or #458 #529)
-#460 := [th-lemma]: #459
-#302 := [unit-resolution #460 #456]: #529
-#508 := (not #514)
-#490 := (or #508 #507 #531)
-#491 := [def-axiom]: #490
-#461 := [unit-resolution #491 #302 #477]: #531
-#404 := [symm #461]: #403
-#405 := (= #36 #476)
+#585 := (iff #591 #663)
+#598 := (iff #607 true)
+#584 := [rewrite]: #598
+#587 := [monotonicity #584]: #585
+#589 := [trans #587 #667]: #588
+#596 := (iff #594 #597)
+#593 := [rewrite]: #596
+#570 := [monotonicity #593 #589]: #590
+#575 := [trans #570 #573]: #574
+#580 := [monotonicity #575]: #579
+#572 := [trans #580 #582]: #579
+#578 := [quant-inst]: #577
+#583 := [mp #578 #572]: #576
+#448 := [unit-resolution #583 #700]: #597
+#445 := (not #597)
+#446 := (or #445 #453)
+#442 := [th-lemma]: #446
+#447 := [unit-resolution #442 #448]: #453
+#437 := (not #453)
+#427 := (or #437 #473)
+#429 := [th-lemma]: #427
+#430 := [unit-resolution #429 #447]: #473
+#471 := (not #501)
+#477 := (or #471 #500 #485)
+#478 := [def-axiom]: #477
+#433 := [unit-resolution #478 #430 #444]: #485
+#373 := [symm #433]: #372
+#374 := (= #36 #484)
 #649 := (uf_2 #35)
-#582 := (+ -10::int #649)
-#553 := (uf_1 #582)
-#556 := (uf_3 #553)
-#401 := (= #556 #476)
-#417 := (= #553 #38)
-#415 := (= #582 6::int)
+#554 := (+ -10::int #649)
+#549 := (uf_1 #554)
+#545 := (uf_3 #549)
+#381 := (= #545 #484)
+#395 := (= #549 #38)
+#394 := (= #554 6::int)
 #335 := (uf_2 #31)
 #647 := -1::int
-#502 := (* -1::int #335)
-#463 := (+ #33 #502)
-#464 := (<= #463 0::int)
-#486 := (= #33 #335)
-#445 := (= #32 #31)
-#574 := (= #31 #32)
-#575 := (+ -10::int #335)
-#576 := (uf_1 #575)
-#577 := (uf_3 #576)
-#578 := (= #32 #577)
-#579 := (>= #335 10::int)
-#580 := (ite #579 #578 #574)
-#572 := (or #336 #580)
-#583 := [quant-inst]: #572
-#457 := [unit-resolution #583 #713]: #580
-#562 := (not #579)
-#554 := (<= #335 4::int)
+#459 := (* -1::int #335)
+#460 := (+ #33 #459)
+#302 := (<= #460 0::int)
+#458 := (= #33 #335)
+#426 := (= #32 #31)
+#555 := (= #31 #32)
+#551 := (+ -10::int #335)
+#552 := (uf_1 #551)
+#553 := (uf_3 #552)
+#556 := (= #32 #553)
+#557 := (>= #335 10::int)
+#558 := (ite #557 #556 #555)
+#560 := (or #336 #558)
+#533 := [quant-inst]: #560
+#434 := [unit-resolution #533 #713]: #558
+#535 := (not #557)
+#531 := (<= #335 4::int)
 #324 := (= #335 4::int)
 #659 := (or #673 #324)
 #678 := (>= 4::int 0::int)
@@ -12498,110 +12719,125 @@
 #277 := [trans #383 #385]: #382
 #367 := [quant-inst]: #660
 #655 := [mp #367 #277]: #659
-#462 := [unit-resolution #655 #700]: #324
-#441 := (not #324)
-#444 := (or #441 #554)
-#448 := [th-lemma]: #444
-#450 := [unit-resolution #448 #462]: #554
-#451 := (not #554)
-#449 := (or #451 #562)
-#452 := [th-lemma]: #449
-#440 := [unit-resolution #452 #450]: #562
-#561 := (not #580)
-#566 := (or #561 #579 #574)
-#567 := [def-axiom]: #566
-#443 := [unit-resolution #567 #440 #457]: #574
-#446 := [symm #443]: #445
-#442 := [monotonicity #446]: #486
-#447 := (not #486)
-#437 := (or #447 #464)
-#427 := [th-lemma]: #437
-#429 := [unit-resolution #427 #442]: #464
-#471 := (>= #463 0::int)
-#430 := (or #447 #471)
-#433 := [th-lemma]: #430
-#434 := [unit-resolution #433 #442]: #471
-#560 := (>= #335 4::int)
-#438 := (or #441 #560)
-#431 := [th-lemma]: #438
-#439 := [unit-resolution #431 #462]: #560
+#438 := [unit-resolution #655 #700]: #324
+#431 := (not #324)
+#439 := (or #431 #531)
+#432 := [th-lemma]: #439
+#435 := [unit-resolution #432 #438]: #531
+#436 := (not #531)
+#422 := (or #436 #535)
+#424 := [th-lemma]: #422
+#425 := [unit-resolution #424 #435]: #535
+#534 := (not #558)
+#540 := (or #534 #557 #555)
+#541 := [def-axiom]: #540
+#423 := [unit-resolution #541 #425 #434]: #555
+#408 := [symm #423]: #426
+#410 := [monotonicity #408]: #458
+#411 := (not #458)
+#412 := (or #411 #302)
+#413 := [th-lemma]: #412
+#414 := [unit-resolution #413 #410]: #302
+#461 := (>= #460 0::int)
+#415 := (or #411 #461)
+#416 := [th-lemma]: #415
+#417 := [unit-resolution #416 #410]: #461
+#512 := (>= #335 4::int)
+#418 := (or #431 #512)
+#419 := [th-lemma]: #418
+#420 := [unit-resolution #419 #438]: #512
 #651 := (* -1::int #649)
 #648 := (+ #34 #651)
-#625 := (<= #648 0::int)
+#521 := (<= #648 0::int)
 #652 := (= #648 0::int)
-#643 := (>= #33 0::int)
-#435 := (not #471)
-#432 := (not #560)
-#436 := (or #643 #432 #435)
-#422 := [th-lemma]: #436
-#424 := [unit-resolution #422 #439 #434]: #643
-#644 := (not #643)
-#489 := (or #644 #652)
-#628 := (or #673 #644 #652)
+#630 := (>= #33 0::int)
+#421 := (not #461)
+#409 := (not #512)
+#398 := (or #630 #409 #421)
+#400 := [th-lemma]: #398
+#401 := [unit-resolution #400 #420 #417]: #630
+#468 := (not #630)
+#623 := (or #468 #652)
+#509 := (or #673 #468 #652)
 #370 := (>= #34 0::int)
 #371 := (not #370)
 #650 := (= #34 #649)
 #364 := (or #650 #371)
-#629 := (or #673 #364)
-#469 := (iff #629 #628)
-#636 := (or #673 #489)
-#466 := (iff #636 #628)
-#468 := [rewrite]: #466
-#630 := (iff #629 #636)
-#633 := (iff #364 #489)
-#646 := (or #652 #644)
-#631 := (iff #646 #489)
-#632 := [rewrite]: #631
-#487 := (iff #364 #646)
-#645 := (iff #371 #644)
-#638 := (iff #370 #643)
-#639 := [rewrite]: #638
-#640 := [monotonicity #639]: #645
+#510 := (or #673 #364)
+#619 := (iff #510 #509)
+#470 := (or #673 #623)
+#615 := (iff #470 #509)
+#616 := [rewrite]: #615
+#618 := (iff #510 #470)
+#624 := (iff #364 #623)
+#643 := 1::int
+#638 := (* 1::int #33)
+#639 := (>= #638 0::int)
+#640 := (not #639)
+#632 := (or #640 #652)
+#625 := (iff #632 #623)
+#469 := (iff #640 #468)
+#637 := (iff #639 #630)
+#635 := (= #638 #33)
+#636 := [rewrite]: #635
+#466 := [monotonicity #636]: #637
+#622 := [monotonicity #466]: #469
+#626 := [monotonicity #622]: #625
+#628 := (iff #364 #632)
+#488 := (or #652 #640)
+#633 := (iff #488 #632)
+#634 := [rewrite]: #633
+#489 := (iff #364 #488)
+#646 := (iff #371 #640)
+#644 := (iff #370 #639)
+#645 := [rewrite]: #644
+#487 := [monotonicity #645]: #646
 #641 := (iff #650 #652)
 #642 := [rewrite]: #641
-#488 := [monotonicity #642 #640]: #487
-#634 := [trans #488 #632]: #633
-#637 := [monotonicity #634]: #630
-#622 := [trans #637 #468]: #469
-#635 := [quant-inst]: #629
-#623 := [mp #635 #622]: #628
-#425 := [unit-resolution #623 #700]: #489
-#423 := [unit-resolution #425 #424]: #652
-#426 := (not #652)
-#408 := (or #426 #625)
-#410 := [th-lemma]: #408
-#411 := [unit-resolution #410 #423]: #625
-#626 := (>= #648 0::int)
-#412 := (or #426 #626)
-#413 := [th-lemma]: #412
-#414 := [unit-resolution #413 #423]: #626
-#416 := [th-lemma #414 #411 #439 #450 #434 #429]: #415
-#418 := [monotonicity #416]: #417
-#402 := [monotonicity #418]: #401
-#557 := (= #36 #556)
-#581 := (= #35 #36)
-#558 := (>= #649 10::int)
-#559 := (ite #558 #557 #581)
-#533 := (or #336 #559)
-#534 := [quant-inst]: #533
-#419 := [unit-resolution #534 #713]: #559
-#420 := (not #625)
-#409 := (or #558 #420 #432 #435)
-#421 := [th-lemma]: #409
-#398 := [unit-resolution #421 #411 #439 #434]: #558
-#428 := (not #558)
-#535 := (not #559)
-#539 := (or #535 #428 #557)
-#540 := [def-axiom]: #539
-#400 := [unit-resolution #540 #398 #419]: #557
-#406 := [trans #400 #402]: #405
-#399 := [trans #406 #404]: #39
+#631 := [monotonicity #642 #487]: #489
+#629 := [trans #631 #634]: #628
+#627 := [trans #629 #626]: #624
+#520 := [monotonicity #627]: #618
+#504 := [trans #520 #616]: #619
+#511 := [quant-inst]: #510
+#519 := [mp #511 #504]: #509
+#402 := [unit-resolution #519 #700]: #623
+#403 := [unit-resolution #402 #401]: #652
+#404 := (not #652)
+#405 := (or #404 #521)
+#406 := [th-lemma]: #405
+#399 := [unit-resolution #406 #403]: #521
+#522 := (>= #648 0::int)
+#407 := (or #404 #522)
+#392 := [th-lemma]: #407
+#393 := [unit-resolution #392 #403]: #522
+#396 := [th-lemma #393 #399 #420 #435 #417 #414]: #394
+#397 := [monotonicity #396]: #395
+#391 := [monotonicity #397]: #381
+#550 := (= #36 #545)
+#559 := (= #35 #36)
+#530 := (>= #649 10::int)
+#476 := (ite #530 #550 #559)
+#536 := (or #336 #476)
+#537 := [quant-inst]: #536
+#386 := [unit-resolution #537 #713]: #476
+#387 := (not #521)
+#388 := (or #530 #387 #409 #421)
+#380 := [th-lemma]: #388
+#389 := [unit-resolution #380 #399 #420 #417]: #530
+#538 := (not #530)
+#532 := (not #476)
+#506 := (or #532 #538 #550)
+#513 := [def-axiom]: #506
+#390 := [unit-resolution #513 #389 #386]: #550
+#365 := [trans #390 #391]: #374
+#375 := [trans #365 #373]: #39
 #40 := (not #39)
 #182 := [asserted]: #40
-[unit-resolution #182 #399]: false
-unsat
-
-/fwo5o8vhLVHyS4oYEs4QA 10833
+[unit-resolution #182 #375]: false
+unsat
+
+/fwo5o8vhLVHyS4oYEs4QA 10902
 #2 := false
 #22 := 0::int
 #8 := 2::int
@@ -12677,18 +12913,18 @@
 #604 := [trans #593 #597]: #562
 #603 := [quant-inst]: #596
 #606 := [mp #603 #604]: #628
-#528 := [unit-resolution #606 #817]: #566
-#521 := (not #566)
-#464 := (or #521 #608)
-#456 := [th-lemma]: #464
-#465 := [unit-resolution #456 #528]: #608
+#516 := [unit-resolution #606 #817]: #566
+#498 := (not #566)
+#432 := (or #498 #608)
+#411 := [th-lemma]: #432
+#413 := [unit-resolution #411 #516]: #608
 decl uf_10 :: int
 #52 := uf_10
 #57 := (mod uf_10 2::int)
 #243 := (* -1::int #57)
 #244 := (+ #56 #243)
 #447 := (>= #244 0::int)
-#387 := (not #447)
+#372 := (not #447)
 #245 := (= #244 0::int)
 #248 := (not #245)
 #218 := (* -1::int #55)
@@ -12708,9 +12944,9 @@
 #662 := (not #672)
 #1 := true
 #81 := [true-axiom]: true
-#520 := (or false #662)
-#523 := [th-lemma]: #520
-#524 := [unit-resolution #523 #81]: #662
+#514 := (or false #662)
+#515 := [th-lemma]: #514
+#513 := [unit-resolution #515 #81]: #662
 #701 := (* -1::int #613)
 #204 := -2::int
 #691 := (* -2::int #222)
@@ -12723,82 +12959,58 @@
 #546 := [th-lemma]: #545
 #548 := [unit-resolution #546 #81]: #692
 #549 := (not #692)
-#497 := (or #549 #694)
-#482 := [th-lemma]: #497
-#483 := [unit-resolution #482 #548]: #694
+#482 := (or #549 #694)
+#483 := [th-lemma]: #482
+#484 := [unit-resolution #483 #548]: #694
 #536 := (not #448)
-#395 := [hypothesis]: #536
+#382 := [hypothesis]: #536
 #555 := (* -1::int uf_10)
 #573 := (+ #51 #555)
 #543 := (<= #573 0::int)
 #53 := (= #51 uf_10)
 #256 := (not #253)
 #259 := (or #248 #256)
-#502 := 1::int
 #731 := (div uf_10 2::int)
-#515 := (* -1::int #731)
-#513 := (+ #640 #515)
+#723 := (* -2::int #731)
+#521 := (* -2::int #624)
+#529 := (+ #521 #723)
 #618 := (div #51 2::int)
-#514 := (* -1::int #618)
-#516 := (+ #514 #513)
-#498 := (+ #243 #516)
-#500 := (+ #56 #498)
-#501 := (+ uf_10 #500)
-#503 := (>= #501 1::int)
-#486 := (not #503)
-#361 := (<= #244 0::int)
+#583 := (* -2::int #618)
+#522 := (+ #583 #529)
+#528 := (* -2::int #57)
+#525 := (+ #528 #522)
+#524 := (* 2::int #56)
+#526 := (+ #524 #525)
+#523 := (* 2::int uf_10)
+#512 := (+ #523 #526)
+#520 := (>= #512 2::int)
 #453 := (not #259)
-#517 := [hypothesis]: #453
+#519 := [hypothesis]: #453
 #440 := (or #259 #245)
 #451 := [def-axiom]: #440
-#519 := [unit-resolution #451 #517]: #245
-#478 := (or #248 #361)
-#470 := [th-lemma]: #478
-#479 := [unit-resolution #470 #519]: #361
-#449 := (>= #252 0::int)
+#470 := [unit-resolution #451 #519]: #245
+#465 := (or #248 #447)
+#466 := [th-lemma]: #465
+#457 := [unit-resolution #466 #470]: #447
+#544 := (>= #573 0::int)
+#441 := (not #544)
 #452 := (or #259 #253)
 #380 := [def-axiom]: #452
-#480 := [unit-resolution #380 #517]: #253
-#471 := (or #256 #449)
-#481 := [th-lemma]: #471
-#462 := [unit-resolution #481 #480]: #449
-#487 := (not #361)
-#485 := (not #449)
-#476 := (or #486 #485 #487)
-#607 := (<= #620 0::int)
-#529 := (or #521 #607)
-#522 := [th-lemma]: #529
-#525 := [unit-resolution #522 #528]: #607
-#723 := (* -2::int #731)
-#724 := (+ #243 #723)
-#718 := (+ uf_10 #724)
-#720 := (<= #718 0::int)
-#722 := (= #718 0::int)
-#526 := (or false #722)
-#512 := [th-lemma]: #526
-#504 := [unit-resolution #512 #81]: #722
-#505 := (not #722)
-#506 := (or #505 #720)
-#507 := [th-lemma]: #506
-#508 := [unit-resolution #507 #504]: #720
-#509 := [hypothesis]: #361
-#583 := (* -2::int #618)
-#584 := (+ #583 #640)
-#585 := (+ #51 #584)
-#587 := (<= #585 0::int)
-#582 := (= #585 0::int)
-#510 := (or false #582)
-#499 := [th-lemma]: #510
-#511 := [unit-resolution #499 #81]: #582
-#488 := (not #582)
-#490 := (or #488 #587)
-#491 := [th-lemma]: #490
-#492 := [unit-resolution #491 #511]: #587
-#493 := [hypothesis]: #503
+#481 := [unit-resolution #380 #519]: #253
+#467 := (or #256 #448)
+#434 := [th-lemma]: #467
+#436 := [unit-resolution #434 #481]: #448
+#532 := (or #543 #536)
+#695 := (>= #699 0::int)
+#550 := (or #549 #695)
+#393 := [th-lemma]: #550
+#551 := [unit-resolution #393 #548]: #695
+#547 := (not #543)
+#552 := [hypothesis]: #547
 #649 := (* -2::int #60)
 #644 := (+ #218 #649)
 #650 := (+ #51 #644)
-#636 := (>= #650 0::int)
+#631 := (<= #650 0::int)
 #623 := (= #650 0::int)
 #43 := (uf_7 uf_2 #35)
 #44 := (uf_6 #34 #43)
@@ -12859,33 +13071,6 @@
 #630 := [quant-inst]: #629
 #531 := [unit-resolution #630 #824]: #623
 #534 := (not #623)
-#494 := (or #534 #636)
-#495 := [th-lemma]: #494
-#496 := [unit-resolution #495 #531]: #636
-#489 := [hypothesis]: #449
-#484 := [th-lemma #483 #489 #496 #493 #492 #509 #508 #525 #524]: false
-#477 := [lemma #484]: #476
-#463 := [unit-resolution #477 #462 #479]: #486
-#727 := (>= #718 0::int)
-#466 := (or #505 #727)
-#457 := [th-lemma]: #466
-#467 := [unit-resolution #457 #504]: #727
-#434 := (or #248 #447)
-#436 := [th-lemma]: #434
-#437 := [unit-resolution #436 #519]: #447
-#544 := (>= #573 0::int)
-#445 := (not #544)
-#428 := (or #256 #448)
-#441 := [th-lemma]: #428
-#442 := [unit-resolution #441 #480]: #448
-#532 := (or #543 #536)
-#695 := (>= #699 0::int)
-#550 := (or #549 #695)
-#393 := [th-lemma]: #550
-#551 := [unit-resolution #393 #548]: #695
-#547 := (not #543)
-#552 := [hypothesis]: #547
-#631 := (<= #650 0::int)
 #538 := (or #534 #631)
 #540 := [th-lemma]: #538
 #541 := [unit-resolution #540 #531]: #631
@@ -12896,8 +13081,8 @@
 #533 := [unit-resolution #530 #81]: #666
 #535 := [th-lemma #533 #539 #541 #552 #551]: false
 #537 := [lemma #535]: #532
-#443 := [unit-resolution #537 #442]: #543
-#429 := (or #547 #445)
+#437 := [unit-resolution #537 #436]: #543
+#444 := (or #547 #441)
 #764 := (not #53)
 #771 := (or #764 #259)
 #262 := (iff #53 #259)
@@ -12950,65 +13135,118 @@
 #438 := (or #764 #259 #433)
 #439 := [def-axiom]: #438
 #772 := [unit-resolution #439 #267]: #771
-#444 := [unit-resolution #772 #517]: #764
-#435 := (or #53 #547 #445)
-#446 := [th-lemma]: #435
-#431 := [unit-resolution #446 #444]: #429
-#432 := [unit-resolution #431 #443]: #445
+#428 := [unit-resolution #772 #519]: #764
+#442 := (or #53 #547 #441)
+#443 := [th-lemma]: #442
+#445 := [unit-resolution #443 #428]: #444
+#435 := [unit-resolution #445 #437]: #441
+#584 := (+ #583 #640)
+#585 := (+ #51 #584)
 #588 := (>= #585 0::int)
-#411 := (or #488 #588)
-#413 := [th-lemma]: #411
-#418 := [unit-resolution #413 #511]: #588
-#419 := [th-lemma #418 #432 #437 #467 #465 #463]: false
-#420 := [lemma #419]: #259
+#582 := (= #585 0::int)
+#499 := (or false #582)
+#511 := [th-lemma]: #499
+#488 := [unit-resolution #511 #81]: #582
+#490 := (not #582)
+#446 := (or #490 #588)
+#429 := [th-lemma]: #446
+#431 := [unit-resolution #429 #488]: #588
+#724 := (+ #243 #723)
+#718 := (+ uf_10 #724)
+#727 := (>= #718 0::int)
+#722 := (= #718 0::int)
+#503 := (or false #722)
+#504 := [th-lemma]: #503
+#505 := [unit-resolution #504 #81]: #722
+#506 := (not #722)
+#418 := (or #506 #727)
+#419 := [th-lemma]: #418
+#420 := [unit-resolution #419 #505]: #727
+#421 := [th-lemma #420 #413 #431 #435 #457]: #520
+#485 := (not #520)
+#361 := (<= #244 0::int)
+#479 := (or #248 #361)
+#480 := [th-lemma]: #479
+#471 := [unit-resolution #480 #470]: #361
+#449 := (>= #252 0::int)
+#462 := (or #256 #449)
+#463 := [th-lemma]: #462
+#464 := [unit-resolution #463 #481]: #449
+#476 := (not #361)
+#487 := (not #449)
+#477 := (or #485 #487 #476)
+#607 := (<= #620 0::int)
+#500 := (or #498 #607)
+#501 := [th-lemma]: #500
+#502 := [unit-resolution #501 #516]: #607
+#720 := (<= #718 0::int)
+#507 := (or #506 #720)
+#508 := [th-lemma]: #507
+#509 := [unit-resolution #508 #505]: #720
+#510 := [hypothesis]: #361
+#587 := (<= #585 0::int)
+#491 := (or #490 #587)
+#492 := [th-lemma]: #491
+#493 := [unit-resolution #492 #488]: #587
+#494 := [hypothesis]: #520
+#636 := (>= #650 0::int)
+#495 := (or #534 #636)
+#496 := [th-lemma]: #495
+#489 := [unit-resolution #496 #531]: #636
+#497 := [hypothesis]: #449
+#486 := [th-lemma #484 #497 #489 #494 #493 #510 #509 #502 #513]: false
+#478 := [lemma #486]: #477
+#456 := [unit-resolution #478 #464 #471]: #485
+#422 := [unit-resolution #456 #421]: false
+#423 := [lemma #422]: #259
 #427 := (or #53 #453)
 #768 := (or #53 #453 #433)
 #770 := [def-axiom]: #768
 #557 := [unit-resolution #770 #267]: #427
-#406 := [unit-resolution #557 #420]: #53
-#377 := (or #764 #543)
-#381 := [th-lemma]: #377
-#382 := [unit-resolution #381 #406]: #543
-#385 := [th-lemma #496 #382 #395 #483 #524]: false
-#386 := [lemma #385]: #448
-#390 := (or #253 #536)
-#408 := [hypothesis]: #485
-#409 := (or #764 #544)
-#397 := [th-lemma]: #409
-#399 := [unit-resolution #397 #406]: #544
-#400 := [th-lemma #399 #408 #533 #551 #541]: false
-#403 := [lemma #400]: #449
-#392 := (or #253 #536 #485)
-#394 := [th-lemma]: #392
-#657 := [unit-resolution #394 #403]: #390
-#658 := [unit-resolution #657 #386]: #253
+#399 := [unit-resolution #557 #423]: #53
+#385 := (or #764 #543)
+#386 := [th-lemma]: #385
+#387 := [unit-resolution #386 #399]: #543
+#379 := [th-lemma #489 #387 #382 #484 #513]: false
+#388 := [lemma #379]: #448
+#381 := (or #253 #536)
+#397 := [hypothesis]: #487
+#400 := (or #764 #544)
+#403 := [th-lemma]: #400
+#398 := [unit-resolution #403 #399]: #544
+#404 := [th-lemma #398 #397 #533 #551 #541]: false
+#378 := [lemma #404]: #449
+#395 := (or #253 #536 #487)
+#377 := [th-lemma]: #395
+#658 := [unit-resolution #377 #378]: #381
+#653 := [unit-resolution #658 #388]: #253
 #450 := (or #453 #248 #256)
 #454 := [def-axiom]: #450
-#762 := [unit-resolution #454 #420]: #259
-#664 := [unit-resolution #762 #658]: #248
-#372 := (or #245 #387)
-#560 := (+ #57 #640)
-#610 := (>= #560 0::int)
-#742 := (= #57 #624)
-#424 := (= #624 #57)
-#405 := [monotonicity #406]: #424
-#407 := [symm #405]: #742
-#705 := (not #742)
-#706 := (or #705 #610)
-#568 := [th-lemma]: #706
-#569 := [unit-resolution #568 #407]: #610
-#398 := [hypothesis]: #487
-#404 := [th-lemma #525 #398 #569]: false
-#378 := [lemma #404]: #361
-#379 := (or #245 #487 #387)
-#388 := [th-lemma]: #379
-#369 := [unit-resolution #388 #378]: #372
-#370 := [unit-resolution #369 #664]: #387
-#708 := (<= #560 0::int)
-#373 := (or #705 #708)
-#374 := [th-lemma]: #373
-#375 := [unit-resolution #374 #407]: #708
-[th-lemma #375 #370 #465]: false
+#664 := [unit-resolution #454 #423]: #259
+#665 := [unit-resolution #664 #653]: #248
+#373 := (or #245 #372)
+#708 := (+ #57 #640)
+#705 := (>= #708 0::int)
+#560 := (= #57 #624)
+#408 := (= #624 #57)
+#406 := [monotonicity #399]: #408
+#409 := [symm #406]: #560
+#706 := (not #560)
+#655 := (or #706 #705)
+#569 := [th-lemma]: #655
+#570 := [unit-resolution #569 #409]: #705
+#383 := [hypothesis]: #476
+#384 := [th-lemma #502 #383 #570]: false
+#389 := [lemma #384]: #361
+#369 := (or #245 #476 #372)
+#370 := [th-lemma]: #369
+#374 := [unit-resolution #370 #389]: #373
+#375 := [unit-resolution #374 #665]: #372
+#610 := (<= #708 0::int)
+#371 := (or #706 #610)
+#376 := [th-lemma]: #371
+#363 := [unit-resolution #376 #409]: #610
+[th-lemma #363 #375 #413]: false
 unsat
 
 s8LL71+1HTN+eIuEYeKhUw 1251
diff -r 9f841f20dca6 -r 648e492abc43 src/HOL/SMT/Examples/SMT_Examples.thy
--- a/src/HOL/SMT/Examples/SMT_Examples.thy	Mon Feb 08 17:12:38 2010 +0100
+++ b/src/HOL/SMT/Examples/SMT_Examples.thy	Mon Feb 08 17:12:40 2010 +0100
@@ -17,7 +17,7 @@
 the following option is set to "false":
 *}
 
-declare [[smt_record=false]] 
+declare [[smt_record=false]]