1.1 --- a/src/HOL/SMT/Examples/SMT_Examples.certs Mon Feb 08 17:12:38 2010 +0100
1.2 +++ b/src/HOL/SMT/Examples/SMT_Examples.certs Mon Feb 08 17:12:40 2010 +0100
1.3 @@ -6677,15 +6677,25 @@
1.4 [mp #29 #65]: false
1.5 unsat
1.6
1.7 -rOkYPs+Q++z/M3OPR/88JQ 1272
1.8 +rOkYPs+Q++z/M3OPR/88JQ 1654
1.9 #2 := false
1.10 #55 := 0::int
1.11 #7 := 2::int
1.12 decl uf_1 :: int
1.13 #4 := uf_1
1.14 #8 := (mod uf_1 2::int)
1.15 -#58 := (>= #8 0::int)
1.16 -#61 := (not #58)
1.17 +#67 := (>= #8 0::int)
1.18 +#1 := true
1.19 +#156 := (iff #67 true)
1.20 +#158 := (iff #156 #67)
1.21 +#159 := [rewrite]: #158
1.22 +#28 := [true-axiom]: true
1.23 +#153 := (or false #67)
1.24 +#154 := [th-lemma]: #153
1.25 +#155 := [unit-resolution #154 #28]: #67
1.26 +#157 := [iff-true #155]: #156
1.27 +#160 := [mp #157 #159]: #67
1.28 +#70 := (not #67)
1.29 #5 := 1::int
1.30 #9 := (* 2::int #8)
1.31 #10 := (+ #9 1::int)
1.32 @@ -6693,24 +6703,35 @@
1.33 #6 := (+ uf_1 1::int)
1.34 #12 := (<= #6 #11)
1.35 #13 := (not #12)
1.36 -#66 := (iff #13 #61)
1.37 +#77 := (iff #13 #70)
1.38 #39 := (+ uf_1 #9)
1.39 #40 := (+ 1::int #39)
1.40 #30 := (+ 1::int uf_1)
1.41 #45 := (<= #30 #40)
1.42 #48 := (not #45)
1.43 -#64 := (iff #48 #61)
1.44 +#75 := (iff #48 #70)
1.45 +#58 := (* 1::int #8)
1.46 +#59 := (>= #58 0::int)
1.47 +#62 := (not #59)
1.48 +#71 := (iff #62 #70)
1.49 +#68 := (iff #59 #67)
1.50 +#65 := (= #58 #8)
1.51 +#66 := [rewrite]: #65
1.52 +#69 := [monotonicity #66]: #68
1.53 +#72 := [monotonicity #69]: #71
1.54 +#73 := (iff #48 #62)
1.55 #56 := (>= #9 0::int)
1.56 #51 := (not #56)
1.57 -#62 := (iff #51 #61)
1.58 -#59 := (iff #56 #58)
1.59 -#60 := [rewrite]: #59
1.60 -#63 := [monotonicity #60]: #62
1.61 +#63 := (iff #51 #62)
1.62 +#60 := (iff #56 #59)
1.63 +#61 := [rewrite]: #60
1.64 +#64 := [monotonicity #61]: #63
1.65 #52 := (iff #48 #51)
1.66 #53 := (iff #45 #56)
1.67 #54 := [rewrite]: #53
1.68 #57 := [monotonicity #54]: #52
1.69 -#65 := [trans #57 #63]: #64
1.70 +#74 := [trans #57 #64]: #73
1.71 +#76 := [trans #74 #72]: #75
1.72 #49 := (iff #13 #48)
1.73 #46 := (iff #12 #45)
1.74 #43 := (= #11 #40)
1.75 @@ -6727,40 +6748,38 @@
1.76 #32 := [rewrite]: #31
1.77 #47 := [monotonicity #32 #44]: #46
1.78 #50 := [monotonicity #47]: #49
1.79 -#67 := [trans #50 #65]: #66
1.80 +#78 := [trans #50 #76]: #77
1.81 #29 := [asserted]: #13
1.82 -#68 := [mp #29 #67]: #61
1.83 -#1 := true
1.84 -#28 := [true-axiom]: true
1.85 -#142 := (or false #58)
1.86 -#143 := [th-lemma]: #142
1.87 -#144 := [unit-resolution #143 #28]: #58
1.88 -[unit-resolution #144 #68]: false
1.89 -unsat
1.90 -
1.91 -oSBTeiF6GKDeHPsMxXHXtQ 1161
1.92 +#79 := [mp #29 #78]: #70
1.93 +[unit-resolution #79 #160]: false
1.94 +unsat
1.95 +
1.96 +oSBTeiF6GKDeHPsMxXHXtQ 1064
1.97 #2 := false
1.98 #5 := 2::int
1.99 decl uf_1 :: int
1.100 #4 := uf_1
1.101 #6 := (mod uf_1 2::int)
1.102 -#55 := (>= #6 2::int)
1.103 +#122 := (>= #6 2::int)
1.104 +#123 := (not #122)
1.105 +#1 := true
1.106 +#27 := [true-axiom]: true
1.107 +#133 := (or false #123)
1.108 +#134 := [th-lemma]: #133
1.109 +#135 := [unit-resolution #134 #27]: #123
1.110 #9 := 3::int
1.111 +#29 := (* 2::int #6)
1.112 +#48 := (>= #29 3::int)
1.113 #10 := (+ uf_1 3::int)
1.114 #7 := (+ #6 #6)
1.115 #8 := (+ uf_1 #7)
1.116 #11 := (< #8 #10)
1.117 #12 := (not #11)
1.118 -#60 := (iff #12 #55)
1.119 +#55 := (iff #12 #48)
1.120 #35 := (+ 3::int uf_1)
1.121 -#29 := (* 2::int #6)
1.122 #32 := (+ uf_1 #29)
1.123 #38 := (< #32 #35)
1.124 #41 := (not #38)
1.125 -#58 := (iff #41 #55)
1.126 -#48 := (>= #29 3::int)
1.127 -#56 := (iff #48 #55)
1.128 -#57 := [rewrite]: #56
1.129 #53 := (iff #41 #48)
1.130 #46 := (not #48)
1.131 #45 := (not #46)
1.132 @@ -6771,7 +6790,6 @@
1.133 #44 := [rewrite]: #47
1.134 #50 := [monotonicity #44]: #49
1.135 #54 := [trans #50 #52]: #53
1.136 -#59 := [trans #54 #57]: #58
1.137 #42 := (iff #12 #41)
1.138 #39 := (iff #11 #38)
1.139 #36 := (= #10 #35)
1.140 @@ -6782,16 +6800,10 @@
1.141 #34 := [monotonicity #31]: #33
1.142 #40 := [monotonicity #34 #37]: #39
1.143 #43 := [monotonicity #40]: #42
1.144 -#61 := [trans #43 #59]: #60
1.145 +#56 := [trans #43 #54]: #55
1.146 #28 := [asserted]: #12
1.147 -#62 := [mp #28 #61]: #55
1.148 -#127 := (not #55)
1.149 -#1 := true
1.150 -#27 := [true-axiom]: true
1.151 -#137 := (or false #127)
1.152 -#138 := [th-lemma]: #137
1.153 -#139 := [unit-resolution #138 #27]: #127
1.154 -[unit-resolution #139 #62]: false
1.155 +#57 := [mp #28 #56]: #48
1.156 +[th-lemma #57 #135]: false
1.157 unsat
1.158
1.159 hqH9yBHvmZgES3pBkvsqVQ 2715
1.160 @@ -7344,52 +7356,99 @@
1.161 [mp #30 #96]: false
1.162 unsat
1.163
1.164 -sHpY0IFBgZUNhP56aRB+/w 1765
1.165 +sHpY0IFBgZUNhP56aRB+/w 2968
1.166 #2 := false
1.167 +#9 := 1::int
1.168 +decl ?x1!1 :: int
1.169 +#91 := ?x1!1
1.170 +#68 := -2::int
1.171 +#129 := (* -2::int ?x1!1)
1.172 +decl ?x2!0 :: int
1.173 +#90 := ?x2!0
1.174 +#7 := 2::int
1.175 +#128 := (* 2::int ?x2!0)
1.176 +#130 := (+ #128 #129)
1.177 +#131 := (<= #130 1::int)
1.178 +#136 := (not #131)
1.179 +#55 := 0::int
1.180 +#53 := -1::int
1.181 +#115 := (* -1::int ?x1!1)
1.182 +#116 := (+ ?x2!0 #115)
1.183 +#117 := (<= #116 0::int)
1.184 +#139 := (or #117 #136)
1.185 +#142 := (not #139)
1.186 +#92 := (* -2::int ?x2!0)
1.187 +#93 := (* 2::int ?x1!1)
1.188 +#94 := (+ #93 #92)
1.189 +#95 := (>= #94 -1::int)
1.190 +#96 := (not #95)
1.191 +#97 := (* -1::int ?x2!0)
1.192 +#98 := (+ ?x1!1 #97)
1.193 +#99 := (>= #98 0::int)
1.194 +#100 := (or #99 #96)
1.195 +#101 := (not #100)
1.196 +#143 := (iff #101 #142)
1.197 +#140 := (iff #100 #139)
1.198 +#137 := (iff #96 #136)
1.199 +#134 := (iff #95 #131)
1.200 +#122 := (+ #92 #93)
1.201 +#125 := (>= #122 -1::int)
1.202 +#132 := (iff #125 #131)
1.203 +#133 := [rewrite]: #132
1.204 +#126 := (iff #95 #125)
1.205 +#123 := (= #94 #122)
1.206 +#124 := [rewrite]: #123
1.207 +#127 := [monotonicity #124]: #126
1.208 +#135 := [trans #127 #133]: #134
1.209 +#138 := [monotonicity #135]: #137
1.210 +#120 := (iff #99 #117)
1.211 +#109 := (+ #97 ?x1!1)
1.212 +#112 := (>= #109 0::int)
1.213 +#118 := (iff #112 #117)
1.214 +#119 := [rewrite]: #118
1.215 +#113 := (iff #99 #112)
1.216 +#110 := (= #98 #109)
1.217 +#111 := [rewrite]: #110
1.218 +#114 := [monotonicity #111]: #113
1.219 +#121 := [trans #114 #119]: #120
1.220 +#141 := [monotonicity #121 #138]: #140
1.221 +#144 := [monotonicity #141]: #143
1.222 #5 := (:var 0 int)
1.223 -#7 := 2::int
1.224 -#11 := (* 2::int #5)
1.225 -#9 := 1::int
1.226 +#71 := (* -2::int #5)
1.227 #4 := (:var 1 int)
1.228 #8 := (* 2::int #4)
1.229 +#72 := (+ #8 #71)
1.230 +#70 := (>= #72 -1::int)
1.231 +#69 := (not #70)
1.232 +#57 := (* -1::int #5)
1.233 +#58 := (+ #4 #57)
1.234 +#56 := (>= #58 0::int)
1.235 +#75 := (or #56 #69)
1.236 +#78 := (forall (vars (?x1 int) (?x2 int)) #75)
1.237 +#81 := (not #78)
1.238 +#102 := (~ #81 #101)
1.239 +#103 := [sk]: #102
1.240 +#11 := (* 2::int #5)
1.241 #10 := (+ #8 1::int)
1.242 #12 := (< #10 #11)
1.243 #6 := (< #4 #5)
1.244 #13 := (implies #6 #12)
1.245 #14 := (forall (vars (?x1 int) (?x2 int)) #13)
1.246 #15 := (not #14)
1.247 -#91 := (iff #15 false)
1.248 +#84 := (iff #15 #81)
1.249 #32 := (+ 1::int #8)
1.250 #35 := (< #32 #11)
1.251 #41 := (not #6)
1.252 #42 := (or #41 #35)
1.253 #47 := (forall (vars (?x1 int) (?x2 int)) #42)
1.254 #50 := (not #47)
1.255 -#89 := (iff #50 false)
1.256 -#1 := true
1.257 -#84 := (not true)
1.258 -#87 := (iff #84 false)
1.259 -#88 := [rewrite]: #87
1.260 -#85 := (iff #50 #84)
1.261 -#82 := (iff #47 true)
1.262 -#77 := (forall (vars (?x1 int) (?x2 int)) true)
1.263 -#80 := (iff #77 true)
1.264 -#81 := [elim-unused]: #80
1.265 -#78 := (iff #47 #77)
1.266 -#75 := (iff #42 true)
1.267 -#55 := 0::int
1.268 -#53 := -1::int
1.269 -#57 := (* -1::int #5)
1.270 -#58 := (+ #4 #57)
1.271 -#56 := (>= #58 0::int)
1.272 +#82 := (iff #50 #81)
1.273 +#79 := (iff #47 #78)
1.274 +#76 := (iff #42 #75)
1.275 +#73 := (iff #35 #69)
1.276 +#74 := [rewrite]: #73
1.277 +#66 := (iff #41 #56)
1.278 #54 := (not #56)
1.279 -#69 := (or #56 #54)
1.280 -#73 := (iff #69 true)
1.281 -#74 := [rewrite]: #73
1.282 -#71 := (iff #42 #69)
1.283 -#70 := (iff #35 #54)
1.284 -#68 := [rewrite]: #70
1.285 -#66 := (iff #41 #56)
1.286 #61 := (not #54)
1.287 #64 := (iff #61 #56)
1.288 #65 := [rewrite]: #64
1.289 @@ -7398,12 +7457,9 @@
1.290 #60 := [rewrite]: #59
1.291 #63 := [monotonicity #60]: #62
1.292 #67 := [trans #63 #65]: #66
1.293 -#72 := [monotonicity #67 #68]: #71
1.294 -#76 := [trans #72 #74]: #75
1.295 -#79 := [quant-intro #76]: #78
1.296 -#83 := [trans #79 #81]: #82
1.297 -#86 := [monotonicity #83]: #85
1.298 -#90 := [trans #86 #88]: #89
1.299 +#77 := [monotonicity #67 #74]: #76
1.300 +#80 := [quant-intro #77]: #79
1.301 +#83 := [monotonicity #80]: #82
1.302 #51 := (iff #15 #50)
1.303 #48 := (iff #14 #47)
1.304 #45 := (iff #13 #42)
1.305 @@ -7419,54 +7475,89 @@
1.306 #46 := [trans #40 #44]: #45
1.307 #49 := [quant-intro #46]: #48
1.308 #52 := [monotonicity #49]: #51
1.309 -#92 := [trans #52 #90]: #91
1.310 +#85 := [trans #52 #83]: #84
1.311 #31 := [asserted]: #15
1.312 -[mp #31 #92]: false
1.313 -unsat
1.314 -
1.315 -7GSX+dyn9XwHWNcjJ4X1ww 1400
1.316 +#86 := [mp #31 #85]: #81
1.317 +#106 := [mp~ #86 #103]: #101
1.318 +#107 := [mp #106 #144]: #142
1.319 +#146 := [not-or-elim #107]: #131
1.320 +#108 := (not #117)
1.321 +#145 := [not-or-elim #107]: #108
1.322 +[th-lemma #145 #146]: false
1.323 +unsat
1.324 +
1.325 +7GSX+dyn9XwHWNcjJ4X1ww 2292
1.326 #2 := false
1.327 +#7 := 1::int
1.328 +decl ?x1!1 :: int
1.329 +#74 := ?x1!1
1.330 +#51 := -2::int
1.331 +#96 := (* -2::int ?x1!1)
1.332 +decl ?x2!0 :: int
1.333 +#73 := ?x2!0
1.334 +#4 := 2::int
1.335 +#95 := (* 2::int ?x2!0)
1.336 +#97 := (+ #95 #96)
1.337 +#166 := (<= #97 1::int)
1.338 +#94 := (= #97 1::int)
1.339 +#53 := -1::int
1.340 +#75 := (* -2::int ?x2!0)
1.341 +#76 := (* 2::int ?x1!1)
1.342 +#77 := (+ #76 #75)
1.343 +#78 := (= #77 -1::int)
1.344 +#79 := (not #78)
1.345 +#80 := (not #79)
1.346 +#110 := (iff #80 #94)
1.347 +#102 := (not #94)
1.348 +#105 := (not #102)
1.349 +#108 := (iff #105 #94)
1.350 +#109 := [rewrite]: #108
1.351 +#106 := (iff #80 #105)
1.352 +#103 := (iff #79 #102)
1.353 +#100 := (iff #78 #94)
1.354 +#88 := (+ #75 #76)
1.355 +#91 := (= #88 -1::int)
1.356 +#98 := (iff #91 #94)
1.357 +#99 := [rewrite]: #98
1.358 +#92 := (iff #78 #91)
1.359 +#89 := (= #77 #88)
1.360 +#90 := [rewrite]: #89
1.361 +#93 := [monotonicity #90]: #92
1.362 +#101 := [trans #93 #99]: #100
1.363 +#104 := [monotonicity #101]: #103
1.364 +#107 := [monotonicity #104]: #106
1.365 +#111 := [trans #107 #109]: #110
1.366 #9 := (:var 0 int)
1.367 -#4 := 2::int
1.368 -#10 := (* 2::int #9)
1.369 -#7 := 1::int
1.370 +#55 := (* -2::int #9)
1.371 #5 := (:var 1 int)
1.372 #6 := (* 2::int #5)
1.373 +#56 := (+ #6 #55)
1.374 +#54 := (= #56 -1::int)
1.375 +#58 := (not #54)
1.376 +#61 := (forall (vars (?x1 int) (?x2 int)) #58)
1.377 +#64 := (not #61)
1.378 +#81 := (~ #64 #80)
1.379 +#82 := [sk]: #81
1.380 +#10 := (* 2::int #9)
1.381 #8 := (+ #6 1::int)
1.382 #11 := (= #8 #10)
1.383 #12 := (not #11)
1.384 #13 := (forall (vars (?x1 int) (?x2 int)) #12)
1.385 #14 := (not #13)
1.386 -#74 := (iff #14 false)
1.387 +#67 := (iff #14 #64)
1.388 #31 := (+ 1::int #6)
1.389 #37 := (= #10 #31)
1.390 #42 := (not #37)
1.391 #45 := (forall (vars (?x1 int) (?x2 int)) #42)
1.392 #48 := (not #45)
1.393 -#72 := (iff #48 false)
1.394 -#1 := true
1.395 -#67 := (not true)
1.396 -#70 := (iff #67 false)
1.397 -#71 := [rewrite]: #70
1.398 -#68 := (iff #48 #67)
1.399 -#65 := (iff #45 true)
1.400 -#60 := (forall (vars (?x1 int) (?x2 int)) true)
1.401 -#63 := (iff #60 true)
1.402 -#64 := [elim-unused]: #63
1.403 -#61 := (iff #45 #60)
1.404 -#58 := (iff #42 true)
1.405 -#51 := (not false)
1.406 -#56 := (iff #51 true)
1.407 -#57 := [rewrite]: #56
1.408 -#52 := (iff #42 #51)
1.409 -#53 := (iff #37 false)
1.410 -#54 := [rewrite]: #53
1.411 -#55 := [monotonicity #54]: #52
1.412 -#59 := [trans #55 #57]: #58
1.413 -#62 := [quant-intro #59]: #61
1.414 -#66 := [trans #62 #64]: #65
1.415 -#69 := [monotonicity #66]: #68
1.416 -#73 := [trans #69 #71]: #72
1.417 +#65 := (iff #48 #64)
1.418 +#62 := (iff #45 #61)
1.419 +#59 := (iff #42 #58)
1.420 +#52 := (iff #37 #54)
1.421 +#57 := [rewrite]: #52
1.422 +#60 := [monotonicity #57]: #59
1.423 +#63 := [quant-intro #60]: #62
1.424 +#66 := [monotonicity #63]: #65
1.425 #49 := (iff #14 #48)
1.426 #46 := (iff #13 #45)
1.427 #43 := (iff #12 #42)
1.428 @@ -7482,9 +7573,19 @@
1.429 #44 := [monotonicity #41]: #43
1.430 #47 := [quant-intro #44]: #46
1.431 #50 := [monotonicity #47]: #49
1.432 -#75 := [trans #50 #73]: #74
1.433 +#68 := [trans #50 #66]: #67
1.434 #30 := [asserted]: #14
1.435 -[mp #30 #75]: false
1.436 +#69 := [mp #30 #68]: #64
1.437 +#85 := [mp~ #69 #82]: #80
1.438 +#86 := [mp #85 #111]: #94
1.439 +#168 := (or #102 #166)
1.440 +#169 := [th-lemma]: #168
1.441 +#170 := [unit-resolution #169 #86]: #166
1.442 +#167 := (>= #97 1::int)
1.443 +#171 := (or #102 #167)
1.444 +#172 := [th-lemma]: #171
1.445 +#173 := [unit-resolution #172 #86]: #167
1.446 +[th-lemma #173 #170]: false
1.447 unsat
1.448
1.449 oieid3+1h5s04LTQ9d796Q 2636
1.450 @@ -7960,38 +8061,62 @@
1.451 [unit-resolution #585 #307]: false
1.452 unsat
1.453
1.454 -4Dtb5Y1TTRPWZcHG9Griog 1594
1.455 +4Dtb5Y1TTRPWZcHG9Griog 2407
1.456 #2 := false
1.457 +#104 := -1::int
1.458 +decl ?x1!1 :: int
1.459 +#86 := ?x1!1
1.460 +#106 := -4::int
1.461 +#107 := (* -4::int ?x1!1)
1.462 +decl ?x2!0 :: int
1.463 +#85 := ?x2!0
1.464 +#7 := 6::int
1.465 +#105 := (* 6::int ?x2!0)
1.466 +#108 := (+ #105 #107)
1.467 +#168 := (<= #108 -1::int)
1.468 +#109 := (= #108 -1::int)
1.469 #12 := 1::int
1.470 +#33 := -6::int
1.471 +#87 := (* -6::int ?x2!0)
1.472 +#4 := 4::int
1.473 +#88 := (* 4::int ?x1!1)
1.474 +#89 := (+ #88 #87)
1.475 +#90 := (= #89 1::int)
1.476 +#112 := (iff #90 #109)
1.477 +#98 := (+ #87 #88)
1.478 +#101 := (= #98 1::int)
1.479 +#110 := (iff #101 #109)
1.480 +#111 := [rewrite]: #110
1.481 +#102 := (iff #90 #101)
1.482 +#99 := (= #89 #98)
1.483 +#100 := [rewrite]: #99
1.484 +#103 := [monotonicity #100]: #102
1.485 +#113 := [trans #103 #111]: #112
1.486 +#53 := (:var 0 int)
1.487 +#54 := (* -6::int #53)
1.488 #9 := (:var 1 int)
1.489 -#7 := 6::int
1.490 +#55 := (* 4::int #9)
1.491 +#56 := (+ #55 #54)
1.492 +#76 := (= #56 1::int)
1.493 +#74 := (exists (vars (?x1 int) (?x2 int)) #76)
1.494 +#91 := (~ #74 #90)
1.495 +#92 := [sk]: #91
1.496 #8 := (- 6::int)
1.497 #10 := (* #8 #9)
1.498 #5 := (:var 2 int)
1.499 -#4 := 4::int
1.500 #6 := (* 4::int #5)
1.501 #11 := (+ #6 #10)
1.502 #13 := (= #11 1::int)
1.503 #14 := (exists (vars (?x1 int) (?x2 int) (?x3 int)) #13)
1.504 #15 := (not #14)
1.505 #16 := (not #15)
1.506 -#82 := (iff #16 false)
1.507 -#53 := (:var 0 int)
1.508 -#33 := -6::int
1.509 -#54 := (* -6::int #53)
1.510 -#55 := (* 4::int #9)
1.511 -#56 := (+ #55 #54)
1.512 +#79 := (iff #16 #74)
1.513 #57 := (= 1::int #56)
1.514 #58 := (exists (vars (?x1 int) (?x2 int)) #57)
1.515 -#80 := (iff #58 false)
1.516 -#76 := (exists (vars (?x1 int) (?x2 int)) false)
1.517 -#78 := (iff #76 false)
1.518 -#79 := [elim-unused]: #78
1.519 -#77 := (iff #58 #76)
1.520 -#73 := (iff #57 false)
1.521 -#74 := [rewrite]: #73
1.522 -#75 := [quant-intro #74]: #77
1.523 -#81 := [trans #75 #79]: #80
1.524 +#77 := (iff #58 #74)
1.525 +#75 := (iff #57 #76)
1.526 +#73 := [rewrite]: #75
1.527 +#78 := [quant-intro #73]: #77
1.528 #71 := (iff #16 #58)
1.529 #63 := (not #58)
1.530 #66 := (not #63)
1.531 @@ -8025,9 +8150,20 @@
1.532 #65 := [monotonicity #62]: #64
1.533 #68 := [monotonicity #65]: #67
1.534 #72 := [trans #68 #70]: #71
1.535 -#83 := [trans #72 #81]: #82
1.536 +#80 := [trans #72 #78]: #79
1.537 #32 := [asserted]: #16
1.538 -[mp #32 #83]: false
1.539 +#81 := [mp #32 #80]: #74
1.540 +#95 := [mp~ #81 #92]: #90
1.541 +#96 := [mp #95 #113]: #109
1.542 +#170 := (not #109)
1.543 +#171 := (or #170 #168)
1.544 +#172 := [th-lemma]: #171
1.545 +#173 := [unit-resolution #172 #96]: #168
1.546 +#169 := (>= #108 -1::int)
1.547 +#174 := (or #170 #169)
1.548 +#175 := [th-lemma]: #174
1.549 +#176 := [unit-resolution #175 #96]: #169
1.550 +[th-lemma #176 #173]: false
1.551 unsat
1.552
1.553 dbOre63OdVavsqL3lG2ttw 2516
1.554 @@ -8445,12 +8581,12 @@
1.555 #46 := (+ #4 #45)
1.556 #44 := (>= #46 0::int)
1.557 #42 := (not #44)
1.558 -#57 := (or #44 #42)
1.559 -#61 := (iff #57 true)
1.560 +#60 := (or #44 #42)
1.561 +#61 := (iff #60 true)
1.562 #62 := [rewrite]: #61
1.563 -#59 := (iff #32 #57)
1.564 +#56 := (iff #32 #60)
1.565 #58 := (iff #11 #42)
1.566 -#56 := [rewrite]: #58
1.567 +#59 := [rewrite]: #58
1.568 #54 := (iff #31 #44)
1.569 #49 := (not #42)
1.570 #52 := (iff #49 #44)
1.571 @@ -8460,8 +8596,8 @@
1.572 #48 := [rewrite]: #47
1.573 #51 := [monotonicity #48]: #50
1.574 #55 := [trans #51 #53]: #54
1.575 -#60 := [monotonicity #55 #56]: #59
1.576 -#64 := [trans #60 #62]: #63
1.577 +#57 := [monotonicity #55 #59]: #56
1.578 +#64 := [trans #57 #62]: #63
1.579 #67 := [quant-intro #64]: #66
1.580 #71 := [trans #67 #69]: #70
1.581 #74 := [monotonicity #71]: #73
1.582 @@ -8764,7 +8900,7 @@
1.583 [mp #45 #150]: false
1.584 unsat
1.585
1.586 -iPZ87GNdi7uQw4ehEpbTPQ 6383
1.587 +iPZ87GNdi7uQw4ehEpbTPQ 7012
1.588 #2 := false
1.589 #9 := 0::int
1.590 decl uf_2 :: (-> T1 int)
1.591 @@ -8779,19 +8915,19 @@
1.592 #295 := -1::int
1.593 #274 := (* -1::int #293)
1.594 #610 := (+ #24 #274)
1.595 -#594 := (<= #610 0::int)
1.596 +#315 := (<= #610 0::int)
1.597 #612 := (= #610 0::int)
1.598 -#606 := (>= #23 0::int)
1.599 -#237 := (= #293 0::int)
1.600 -#549 := (not #237)
1.601 -#588 := (<= #293 0::int)
1.602 -#457 := (not #588)
1.603 +#255 := (>= #23 0::int)
1.604 +#317 := (= #293 0::int)
1.605 +#522 := (not #317)
1.606 +#577 := (<= #293 0::int)
1.607 +#519 := (not #577)
1.608 #26 := 1::int
1.609 -#558 := (>= #293 1::int)
1.610 -#555 := (= #293 1::int)
1.611 +#553 := (>= #293 1::int)
1.612 +#552 := (= #293 1::int)
1.613 #27 := (uf_1 1::int)
1.614 -#589 := (uf_2 #27)
1.615 -#301 := (= #589 1::int)
1.616 +#420 := (uf_2 #27)
1.617 +#565 := (= #420 1::int)
1.618 #10 := (:var 0 int)
1.619 #12 := (uf_1 #10)
1.620 #626 := (pattern #12)
1.621 @@ -8847,57 +8983,57 @@
1.622 #87 := [mp #51 #86]: #82
1.623 #146 := [mp~ #87 #130]: #82
1.624 #632 := [mp #146 #631]: #627
1.625 -#609 := (not #627)
1.626 -#578 := (or #609 #301)
1.627 -#311 := (>= 1::int 0::int)
1.628 -#585 := (not #311)
1.629 -#586 := (= 1::int #589)
1.630 -#590 := (or #586 #585)
1.631 -#419 := (or #609 #590)
1.632 -#421 := (iff #419 #578)
1.633 -#564 := (iff #578 #578)
1.634 -#565 := [rewrite]: #564
1.635 -#577 := (iff #590 #301)
1.636 -#574 := (or #301 false)
1.637 -#571 := (iff #574 #301)
1.638 -#576 := [rewrite]: #571
1.639 -#575 := (iff #590 #574)
1.640 -#584 := (iff #585 false)
1.641 +#237 := (not #627)
1.642 +#442 := (or #237 #565)
1.643 +#578 := (>= 1::int 0::int)
1.644 +#419 := (not #578)
1.645 +#421 := (= 1::int #420)
1.646 +#563 := (or #421 #419)
1.647 +#443 := (or #237 #563)
1.648 +#550 := (iff #443 #442)
1.649 +#547 := (iff #442 #442)
1.650 +#548 := [rewrite]: #547
1.651 +#559 := (iff #563 #565)
1.652 +#554 := (or #565 false)
1.653 +#558 := (iff #554 #565)
1.654 +#556 := [rewrite]: #558
1.655 +#555 := (iff #563 #554)
1.656 +#400 := (iff #419 false)
1.657 #1 := true
1.658 -#582 := (not true)
1.659 -#583 := (iff #582 false)
1.660 -#580 := [rewrite]: #583
1.661 -#296 := (iff #585 #582)
1.662 -#303 := (iff #311 true)
1.663 -#581 := [rewrite]: #303
1.664 -#579 := [monotonicity #581]: #296
1.665 -#573 := [trans #579 #580]: #584
1.666 -#300 := (iff #586 #301)
1.667 -#302 := [rewrite]: #300
1.668 -#570 := [monotonicity #302 #573]: #575
1.669 -#572 := [trans #570 #576]: #577
1.670 -#563 := [monotonicity #572]: #421
1.671 -#566 := [trans #563 #565]: #421
1.672 -#420 := [quant-inst]: #419
1.673 -#560 := [mp #420 #566]: #578
1.674 -#442 := [unit-resolution #560 #632]: #301
1.675 -#443 := (= #293 #589)
1.676 +#567 := (not true)
1.677 +#569 := (iff #567 false)
1.678 +#398 := [rewrite]: #569
1.679 +#568 := (iff #419 #567)
1.680 +#560 := (iff #578 true)
1.681 +#561 := [rewrite]: #560
1.682 +#562 := [monotonicity #561]: #568
1.683 +#401 := [trans #562 #398]: #400
1.684 +#564 := (iff #421 #565)
1.685 +#566 := [rewrite]: #564
1.686 +#557 := [monotonicity #566 #401]: #555
1.687 +#441 := [trans #557 #556]: #559
1.688 +#452 := [monotonicity #441]: #550
1.689 +#551 := [trans #452 #548]: #550
1.690 +#402 := [quant-inst]: #443
1.691 +#436 := [mp #402 #551]: #442
1.692 +#524 := [unit-resolution #436 #632]: #565
1.693 +#526 := (= #293 #420)
1.694 #28 := (= #25 #27)
1.695 #129 := [asserted]: #28
1.696 -#436 := [monotonicity #129]: #443
1.697 -#451 := [trans #436 #442]: #555
1.698 -#453 := (not #555)
1.699 -#454 := (or #453 #558)
1.700 -#447 := [th-lemma]: #454
1.701 -#455 := [unit-resolution #447 #451]: #558
1.702 -#456 := (not #558)
1.703 -#458 := (or #456 #457)
1.704 -#459 := [th-lemma]: #458
1.705 -#552 := [unit-resolution #459 #455]: #457
1.706 -#553 := (or #549 #588)
1.707 -#540 := [th-lemma]: #553
1.708 -#542 := [unit-resolution #540 #552]: #549
1.709 -#603 := (or #237 #606)
1.710 +#527 := [monotonicity #129]: #526
1.711 +#528 := [trans #527 #524]: #552
1.712 +#529 := (not #552)
1.713 +#525 := (or #529 #553)
1.714 +#530 := [th-lemma]: #525
1.715 +#516 := [unit-resolution #530 #528]: #553
1.716 +#517 := (not #553)
1.717 +#520 := (or #517 #519)
1.718 +#521 := [th-lemma]: #520
1.719 +#518 := [unit-resolution #521 #516]: #519
1.720 +#502 := (or #522 #577)
1.721 +#503 := [th-lemma]: #502
1.722 +#505 := [unit-resolution #503 #518]: #522
1.723 +#300 := (or #255 #317)
1.724 #18 := (= #13 0::int)
1.725 #118 := (or #18 #70)
1.726 #633 := (forall (vars (?x3 int)) (:pat #626) #118)
1.727 @@ -8954,71 +9090,95 @@
1.728 #128 := [mp #88 #127]: #123
1.729 #149 := [mp~ #128 #134]: #123
1.730 #638 := [mp #149 #637]: #633
1.731 -#604 := (not #633)
1.732 -#602 := (or #604 #237 #606)
1.733 +#582 := (not #633)
1.734 +#296 := (or #582 #255 #317)
1.735 #204 := (>= #24 0::int)
1.736 -#601 := (or #237 #204)
1.737 -#605 := (or #604 #601)
1.738 -#317 := (iff #605 #602)
1.739 -#592 := (or #604 #603)
1.740 -#315 := (iff #592 #602)
1.741 -#316 := [rewrite]: #315
1.742 -#299 := (iff #605 #592)
1.743 -#242 := (iff #601 #603)
1.744 -#279 := (iff #204 #606)
1.745 -#280 := [rewrite]: #279
1.746 -#243 := [monotonicity #280]: #242
1.747 -#314 := [monotonicity #243]: #299
1.748 -#210 := [trans #314 #316]: #317
1.749 -#591 := [quant-inst]: #605
1.750 -#587 := [mp #591 #210]: #602
1.751 -#534 := [unit-resolution #587 #638]: #603
1.752 -#531 := [unit-resolution #534 #542]: #606
1.753 -#613 := (not #606)
1.754 -#607 := (or #613 #612)
1.755 -#251 := (or #609 #613 #612)
1.756 +#210 := (or #317 #204)
1.757 +#579 := (or #582 #210)
1.758 +#570 := (iff #579 #296)
1.759 +#580 := (or #582 #300)
1.760 +#574 := (iff #580 #296)
1.761 +#575 := [rewrite]: #574
1.762 +#584 := (iff #579 #580)
1.763 +#303 := (iff #210 #300)
1.764 +#606 := (* 1::int #23)
1.765 +#279 := (>= #606 0::int)
1.766 +#311 := (or #279 #317)
1.767 +#301 := (iff #311 #300)
1.768 +#256 := (iff #279 #255)
1.769 +#251 := (= #606 #23)
1.770 +#593 := [rewrite]: #251
1.771 +#257 := [monotonicity #593]: #256
1.772 +#302 := [monotonicity #257]: #301
1.773 +#586 := (iff #210 #311)
1.774 +#587 := (or #317 #279)
1.775 +#585 := (iff #587 #311)
1.776 +#589 := [rewrite]: #585
1.777 +#588 := (iff #210 #587)
1.778 +#280 := (iff #204 #279)
1.779 +#613 := [rewrite]: #280
1.780 +#310 := [monotonicity #613]: #588
1.781 +#590 := [trans #310 #589]: #586
1.782 +#581 := [trans #590 #302]: #303
1.783 +#573 := [monotonicity #581]: #584
1.784 +#571 := [trans #573 #575]: #570
1.785 +#583 := [quant-inst]: #579
1.786 +#576 := [mp #583 #571]: #296
1.787 +#506 := [unit-resolution #576 #638]: #300
1.788 +#507 := [unit-resolution #506 #505]: #255
1.789 +#258 := (not #255)
1.790 +#597 := (or #258 #612)
1.791 +#601 := (or #237 #258 #612)
1.792 #289 := (not #204)
1.793 #294 := (= #24 #293)
1.794 #291 := (or #294 #289)
1.795 -#593 := (or #609 #291)
1.796 -#597 := (iff #593 #251)
1.797 -#256 := (or #609 #607)
1.798 -#595 := (iff #256 #251)
1.799 -#596 := [rewrite]: #595
1.800 -#257 := (iff #593 #256)
1.801 -#608 := (iff #291 #607)
1.802 -#616 := (or #612 #613)
1.803 -#266 := (iff #616 #607)
1.804 -#271 := [rewrite]: #266
1.805 -#611 := (iff #291 #616)
1.806 -#614 := (iff #289 #613)
1.807 -#615 := [monotonicity #280]: #614
1.808 +#603 := (or #237 #291)
1.809 +#592 := (iff #603 #601)
1.810 +#243 := (or #237 #597)
1.811 +#605 := (iff #243 #601)
1.812 +#591 := [rewrite]: #605
1.813 +#604 := (iff #603 #243)
1.814 +#594 := (iff #291 #597)
1.815 +#614 := (not #279)
1.816 +#266 := (or #614 #612)
1.817 +#598 := (iff #266 #597)
1.818 +#595 := (iff #614 #258)
1.819 +#596 := [monotonicity #257]: #595
1.820 +#599 := [monotonicity #596]: #598
1.821 +#267 := (iff #291 #266)
1.822 +#611 := (or #612 #614)
1.823 +#271 := (iff #611 #266)
1.824 +#608 := [rewrite]: #271
1.825 +#617 := (iff #291 #611)
1.826 +#615 := (iff #289 #614)
1.827 +#616 := [monotonicity #613]: #615
1.828 #268 := (iff #294 #612)
1.829 #399 := [rewrite]: #268
1.830 -#617 := [monotonicity #399 #615]: #611
1.831 -#267 := [trans #617 #271]: #608
1.832 -#258 := [monotonicity #267]: #257
1.833 -#598 := [trans #258 #596]: #597
1.834 -#255 := [quant-inst]: #593
1.835 -#599 := [mp #255 #598]: #251
1.836 -#533 := [unit-resolution #599 #632]: #607
1.837 -#543 := [unit-resolution #533 #531]: #612
1.838 -#544 := (not #612)
1.839 -#545 := (or #544 #594)
1.840 -#541 := [th-lemma]: #545
1.841 -#546 := [unit-resolution #541 #543]: #594
1.842 -#600 := (>= #610 0::int)
1.843 -#535 := (or #544 #600)
1.844 -#536 := [th-lemma]: #535
1.845 -#537 := [unit-resolution #536 #543]: #600
1.846 -#557 := (<= #293 1::int)
1.847 -#538 := (or #453 #557)
1.848 -#532 := [th-lemma]: #538
1.849 -#539 := [unit-resolution #532 #451]: #557
1.850 -[th-lemma #455 #539 #537 #546]: false
1.851 -unsat
1.852 -
1.853 -kDuOn7kAggfP4Um8ghhv5A 5551
1.854 +#607 := [monotonicity #399 #616]: #617
1.855 +#609 := [trans #607 #608]: #267
1.856 +#600 := [trans #609 #599]: #594
1.857 +#602 := [monotonicity #600]: #604
1.858 +#299 := [trans #602 #591]: #592
1.859 +#242 := [quant-inst]: #603
1.860 +#314 := [mp #242 #299]: #601
1.861 +#508 := [unit-resolution #314 #632]: #597
1.862 +#509 := [unit-resolution #508 #507]: #612
1.863 +#510 := (not #612)
1.864 +#511 := (or #510 #315)
1.865 +#512 := [th-lemma]: #511
1.866 +#513 := [unit-resolution #512 #509]: #315
1.867 +#316 := (>= #610 0::int)
1.868 +#514 := (or #510 #316)
1.869 +#504 := [th-lemma]: #514
1.870 +#515 := [unit-resolution #504 #509]: #316
1.871 +#549 := (<= #293 1::int)
1.872 +#493 := (or #529 #549)
1.873 +#494 := [th-lemma]: #493
1.874 +#496 := [unit-resolution #494 #528]: #549
1.875 +[th-lemma #516 #496 #515 #513]: false
1.876 +unsat
1.877 +
1.878 +kDuOn7kAggfP4Um8ghhv5A 6068
1.879 #2 := false
1.880 #23 := 3::int
1.881 decl uf_2 :: (-> T1 int)
1.882 @@ -9041,13 +9201,13 @@
1.883 #632 := -1::int
1.884 #634 := (* -1::int #28)
1.885 #290 := (+ #26 #634)
1.886 -#623 := (>= #290 0::int)
1.887 +#609 := (>= #290 0::int)
1.888 #421 := (= #290 0::int)
1.889 -#302 := (>= #22 0::int)
1.890 -#625 := (= #28 0::int)
1.891 -#318 := (not #625)
1.892 -#322 := (<= #28 0::int)
1.893 -#324 := (not #322)
1.894 +#273 := (>= #22 0::int)
1.895 +#610 := (= #28 0::int)
1.896 +#588 := (not #610)
1.897 +#441 := (<= #28 0::int)
1.898 +#443 := (not #441)
1.899 #29 := 7::int
1.900 #143 := (>= #28 7::int)
1.901 #30 := (< #28 7::int)
1.902 @@ -9064,12 +9224,12 @@
1.903 #151 := [trans #147 #149]: #150
1.904 #133 := [asserted]: #31
1.905 #152 := [mp #133 #151]: #143
1.906 -#325 := (or #324 #141)
1.907 -#603 := [th-lemma]: #325
1.908 -#604 := [unit-resolution #603 #152]: #324
1.909 -#601 := (or #318 #322)
1.910 -#605 := [th-lemma]: #601
1.911 -#602 := [unit-resolution #605 #604]: #318
1.912 +#585 := (or #443 #141)
1.913 +#586 := [th-lemma]: #585
1.914 +#587 := [unit-resolution #586 #152]: #443
1.915 +#582 := (or #588 #441)
1.916 +#583 := [th-lemma]: #582
1.917 +#589 := [unit-resolution #583 #587]: #588
1.918 #10 := (:var 0 int)
1.919 #12 := (uf_1 #10)
1.920 #648 := (pattern #12)
1.921 @@ -9132,33 +9292,45 @@
1.922 #131 := [mp #91 #130]: #126
1.923 #172 := [mp~ #131 #155]: #126
1.924 #660 := [mp #172 #659]: #655
1.925 -#337 := (not #655)
1.926 -#338 := (or #337 #302 #625)
1.927 +#605 := (not #655)
1.928 +#602 := (or #605 #273 #610)
1.929 #315 := (>= #26 0::int)
1.930 -#264 := (or #625 #315)
1.931 -#339 := (or #337 #264)
1.932 -#611 := (iff #339 #338)
1.933 -#627 := (or #302 #625)
1.934 -#609 := (or #337 #627)
1.935 -#333 := (iff #609 #338)
1.936 -#607 := [rewrite]: #333
1.937 -#610 := (iff #339 #609)
1.938 -#321 := (iff #264 #627)
1.939 -#265 := (or #625 #302)
1.940 -#613 := (iff #265 #627)
1.941 -#614 := [rewrite]: #613
1.942 -#626 := (iff #264 #265)
1.943 -#635 := (iff #315 #302)
1.944 -#636 := [rewrite]: #635
1.945 -#624 := [monotonicity #636]: #626
1.946 -#336 := [trans #624 #614]: #321
1.947 -#332 := [monotonicity #336]: #610
1.948 -#608 := [trans #332 #607]: #611
1.949 -#231 := [quant-inst]: #339
1.950 -#612 := [mp #231 #608]: #338
1.951 -#606 := [unit-resolution #612 #660 #602]: #302
1.952 -#637 := (not #302)
1.953 -#293 := (or #637 #421)
1.954 +#332 := (or #610 #315)
1.955 +#606 := (or #605 #332)
1.956 +#599 := (iff #606 #602)
1.957 +#323 := (or #273 #610)
1.958 +#596 := (or #605 #323)
1.959 +#593 := (iff #596 #602)
1.960 +#598 := [rewrite]: #593
1.961 +#597 := (iff #606 #596)
1.962 +#318 := (iff #332 #323)
1.963 +#302 := 1::int
1.964 +#635 := (* 1::int #22)
1.965 +#636 := (>= #635 0::int)
1.966 +#333 := (or #610 #636)
1.967 +#603 := (iff #333 #323)
1.968 +#608 := (or #610 #273)
1.969 +#324 := (iff #608 #323)
1.970 +#325 := [rewrite]: #324
1.971 +#612 := (iff #333 #608)
1.972 +#615 := (iff #636 #273)
1.973 +#289 := (= #635 #22)
1.974 +#631 := [rewrite]: #289
1.975 +#277 := [monotonicity #631]: #615
1.976 +#322 := [monotonicity #277]: #612
1.977 +#604 := [trans #322 #325]: #603
1.978 +#607 := (iff #332 #333)
1.979 +#637 := (iff #315 #636)
1.980 +#638 := [rewrite]: #637
1.981 +#611 := [monotonicity #638]: #607
1.982 +#601 := [trans #611 #604]: #318
1.983 +#592 := [monotonicity #601]: #597
1.984 +#594 := [trans #592 #598]: #599
1.985 +#595 := [quant-inst]: #606
1.986 +#600 := [mp #595 #594]: #602
1.987 +#590 := [unit-resolution #600 #660 #589]: #273
1.988 +#278 := (not #273)
1.989 +#620 := (or #278 #421)
1.990 #55 := (= #10 #13)
1.991 #80 := (or #55 #74)
1.992 #649 := (forall (vars (?x2 int)) (:pat #648) #80)
1.993 @@ -9208,39 +9380,47 @@
1.994 #90 := [mp #54 #89]: #85
1.995 #169 := [mp~ #90 #134]: #85
1.996 #654 := [mp #169 #653]: #649
1.997 -#615 := (not #649)
1.998 -#277 := (or #615 #637 #421)
1.999 +#264 := (not #649)
1.1000 +#265 := (or #264 #278 #421)
1.1001 #243 := (not #315)
1.1002 #317 := (= #26 #28)
1.1003 #296 := (or #317 #243)
1.1004 -#278 := (or #615 #296)
1.1005 -#621 := (iff #278 #277)
1.1006 -#280 := (or #615 #293)
1.1007 -#619 := (iff #280 #277)
1.1008 -#620 := [rewrite]: #619
1.1009 -#617 := (iff #278 #280)
1.1010 -#631 := (iff #296 #293)
1.1011 -#639 := (or #421 #637)
1.1012 -#630 := (iff #639 #293)
1.1013 -#289 := [rewrite]: #630
1.1014 -#629 := (iff #296 #639)
1.1015 -#638 := (iff #243 #637)
1.1016 -#633 := [monotonicity #636]: #638
1.1017 +#626 := (or #264 #296)
1.1018 +#337 := (iff #626 #265)
1.1019 +#627 := (or #264 #620)
1.1020 +#321 := (iff #627 #265)
1.1021 +#336 := [rewrite]: #321
1.1022 +#613 := (iff #626 #627)
1.1023 +#623 := (iff #296 #620)
1.1024 +#633 := (not #636)
1.1025 +#288 := (or #421 #633)
1.1026 +#622 := (iff #288 #620)
1.1027 +#617 := (or #421 #278)
1.1028 +#621 := (iff #617 #620)
1.1029 +#616 := [rewrite]: #621
1.1030 +#618 := (iff #288 #617)
1.1031 +#279 := (iff #633 #278)
1.1032 +#280 := [monotonicity #277]: #279
1.1033 +#619 := [monotonicity #280]: #618
1.1034 +#259 := [trans #619 #616]: #622
1.1035 +#293 := (iff #296 #288)
1.1036 +#639 := (iff #243 #633)
1.1037 +#629 := [monotonicity #638]: #639
1.1038 #628 := (iff #317 #421)
1.1039 #301 := [rewrite]: #628
1.1040 -#288 := [monotonicity #301 #633]: #629
1.1041 -#273 := [trans #288 #289]: #631
1.1042 -#618 := [monotonicity #273]: #617
1.1043 -#616 := [trans #618 #620]: #621
1.1044 -#279 := [quant-inst]: #278
1.1045 -#622 := [mp #279 #616]: #277
1.1046 -#595 := [unit-resolution #622 #654]: #293
1.1047 -#596 := [unit-resolution #595 #606]: #421
1.1048 -#597 := (not #421)
1.1049 -#592 := (or #597 #623)
1.1050 -#593 := [th-lemma]: #592
1.1051 -#598 := [unit-resolution #593 #596]: #623
1.1052 -[th-lemma #152 #598 #139]: false
1.1053 +#630 := [monotonicity #301 #629]: #293
1.1054 +#625 := [trans #630 #259]: #623
1.1055 +#614 := [monotonicity #625]: #613
1.1056 +#338 := [trans #614 #336]: #337
1.1057 +#624 := [quant-inst]: #626
1.1058 +#339 := [mp #624 #338]: #265
1.1059 +#584 := [unit-resolution #339 #654]: #620
1.1060 +#591 := [unit-resolution #584 #590]: #421
1.1061 +#420 := (not #421)
1.1062 +#422 := (or #420 #609)
1.1063 +#423 := [th-lemma]: #422
1.1064 +#576 := [unit-resolution #423 #591]: #609
1.1065 +[th-lemma #152 #576 #139]: false
1.1066 unsat
1.1067
1.1068 aiB004AWADNjynNrqCDsxw 9284
1.1069 @@ -9916,7 +10096,7 @@
1.1070 [th-lemma #623 #188 #601 #628]: false
1.1071 unsat
1.1072
1.1073 -ZcLxnpFewGGQ0H47MfRXGw 11816
1.1074 +ZcLxnpFewGGQ0H47MfRXGw 12389
1.1075 #2 := false
1.1076 #9 := 0::int
1.1077 decl uf_2 :: (-> T1 int)
1.1078 @@ -9930,8 +10110,8 @@
1.1079 #297 := (uf_2 #141)
1.1080 #357 := (= #297 0::int)
1.1081 #166 := (uf_1 0::int)
1.1082 -#531 := (uf_2 #166)
1.1083 -#537 := (= #531 0::int)
1.1084 +#454 := (uf_2 #166)
1.1085 +#515 := (= #454 0::int)
1.1086 #10 := (:var 0 int)
1.1087 #12 := (uf_1 #10)
1.1088 #672 := (pattern #12)
1.1089 @@ -9988,40 +10168,40 @@
1.1090 #192 := [mp~ #95 #175]: #90
1.1091 #678 := [mp #192 #677]: #673
1.1092 #650 := (not #673)
1.1093 -#528 := (or #650 #537)
1.1094 -#529 := (>= 0::int 0::int)
1.1095 -#530 := (not #529)
1.1096 -#534 := (= 0::int #531)
1.1097 -#535 := (or #534 #530)
1.1098 -#508 := (or #650 #535)
1.1099 -#509 := (iff #508 #528)
1.1100 -#514 := (iff #528 #528)
1.1101 -#515 := [rewrite]: #514
1.1102 -#527 := (iff #535 #537)
1.1103 -#520 := (or #537 false)
1.1104 -#525 := (iff #520 #537)
1.1105 -#526 := [rewrite]: #525
1.1106 -#521 := (iff #535 #520)
1.1107 -#519 := (iff #530 false)
1.1108 +#468 := (or #650 #515)
1.1109 +#528 := (>= 0::int 0::int)
1.1110 +#508 := (not #528)
1.1111 +#509 := (= 0::int #454)
1.1112 +#490 := (or #509 #508)
1.1113 +#469 := (or #650 #490)
1.1114 +#471 := (iff #469 #468)
1.1115 +#473 := (iff #468 #468)
1.1116 +#474 := [rewrite]: #473
1.1117 +#462 := (iff #490 #515)
1.1118 +#495 := (or #515 false)
1.1119 +#486 := (iff #495 #515)
1.1120 +#507 := [rewrite]: #486
1.1121 +#496 := (iff #490 #495)
1.1122 +#492 := (iff #508 false)
1.1123 #1 := true
1.1124 -#512 := (not true)
1.1125 -#517 := (iff #512 false)
1.1126 -#518 := [rewrite]: #517
1.1127 -#513 := (iff #530 #512)
1.1128 -#538 := (iff #529 true)
1.1129 -#511 := [rewrite]: #538
1.1130 -#406 := [monotonicity #511]: #513
1.1131 -#524 := [trans #406 #518]: #519
1.1132 -#536 := (iff #534 #537)
1.1133 -#532 := [rewrite]: #536
1.1134 -#522 := [monotonicity #532 #524]: #521
1.1135 -#523 := [trans #522 #526]: #527
1.1136 -#490 := [monotonicity #523]: #509
1.1137 -#510 := [trans #490 #515]: #509
1.1138 -#454 := [quant-inst]: #508
1.1139 -#516 := [mp #454 #510]: #528
1.1140 -#394 := [unit-resolution #516 #678]: #537
1.1141 -#355 := (= #297 #531)
1.1142 +#491 := (not true)
1.1143 +#483 := (iff #491 false)
1.1144 +#485 := [rewrite]: #483
1.1145 +#450 := (iff #508 #491)
1.1146 +#516 := (iff #528 true)
1.1147 +#484 := [rewrite]: #516
1.1148 +#481 := [monotonicity #484]: #450
1.1149 +#494 := [trans #481 #485]: #492
1.1150 +#514 := (iff #509 #515)
1.1151 +#510 := [rewrite]: #514
1.1152 +#506 := [monotonicity #510 #494]: #496
1.1153 +#463 := [trans #506 #507]: #462
1.1154 +#472 := [monotonicity #463]: #471
1.1155 +#475 := [trans #472 #474]: #471
1.1156 +#470 := [quant-inst]: #469
1.1157 +#476 := [mp #470 #475]: #468
1.1158 +#351 := [unit-resolution #476 #678]: #515
1.1159 +#287 := (= #297 #454)
1.1160 #250 := (= #141 #166)
1.1161 #26 := 2::int
1.1162 #144 := (* 2::int #22)
1.1163 @@ -10032,29 +10212,24 @@
1.1164 #161 := (uf_1 #156)
1.1165 #336 := (= #161 #166)
1.1166 #327 := (not #336)
1.1167 -#588 := (uf_2 #161)
1.1168 -#555 := (= #588 0::int)
1.1169 -#398 := (= #588 #531)
1.1170 -#395 := [hypothesis]: #336
1.1171 -#387 := [monotonicity #395]: #398
1.1172 -#399 := [trans #387 #394]: #555
1.1173 -#390 := (not #555)
1.1174 -#547 := (<= #588 0::int)
1.1175 -#403 := (not #547)
1.1176 -#595 := (>= #150 0::int)
1.1177 -#302 := -1::int
1.1178 -#618 := (* -1::int #150)
1.1179 -#624 := (+ #144 #618)
1.1180 -#488 := (<= #624 0::int)
1.1181 -#465 := (= #624 0::int)
1.1182 -#609 := (>= #22 0::int)
1.1183 -#442 := (= #22 0::int)
1.1184 +#568 := (uf_2 #161)
1.1185 +#537 := (= #568 0::int)
1.1186 +#354 := (= #568 #454)
1.1187 +#352 := [hypothesis]: #336
1.1188 +#344 := [monotonicity #352]: #354
1.1189 +#355 := [trans #344 #351]: #537
1.1190 +#368 := (not #537)
1.1191 +#527 := (<= #568 0::int)
1.1192 +#375 := (not #527)
1.1193 +#566 := (>= #150 0::int)
1.1194 +#447 := (>= #22 0::int)
1.1195 +#421 := (= #22 0::int)
1.1196 #660 := (uf_1 #22)
1.1197 -#495 := (uf_2 #660)
1.1198 -#496 := (= #495 0::int)
1.1199 -#612 := (not #609)
1.1200 -#451 := [hypothesis]: #612
1.1201 -#506 := (or #496 #609)
1.1202 +#451 := (uf_2 #660)
1.1203 +#452 := (= #451 0::int)
1.1204 +#603 := (not #447)
1.1205 +#424 := [hypothesis]: #603
1.1206 +#455 := (or #447 #452)
1.1207 #18 := (= #13 0::int)
1.1208 #126 := (or #18 #78)
1.1209 #679 := (forall (vars (?x3 int)) (:pat #672) #126)
1.1210 @@ -10112,15 +10287,23 @@
1.1211 #195 := [mp~ #136 #180]: #131
1.1212 #684 := [mp #195 #683]: #679
1.1213 #346 := (not #679)
1.1214 -#462 := (or #346 #496 #609)
1.1215 -#463 := (or #346 #506)
1.1216 -#469 := (iff #463 #462)
1.1217 -#470 := [rewrite]: #469
1.1218 -#468 := [quant-inst]: #463
1.1219 -#471 := [mp #468 #470]: #462
1.1220 -#452 := [unit-resolution #471 #684]: #506
1.1221 -#453 := [unit-resolution #452 #451]: #496
1.1222 -#456 := (= #22 #495)
1.1223 +#458 := (or #346 #447 #452)
1.1224 +#453 := (or #452 #447)
1.1225 +#459 := (or #346 #453)
1.1226 +#434 := (iff #459 #458)
1.1227 +#443 := (or #346 #455)
1.1228 +#432 := (iff #443 #458)
1.1229 +#433 := [rewrite]: #432
1.1230 +#461 := (iff #459 #443)
1.1231 +#456 := (iff #453 #455)
1.1232 +#457 := [rewrite]: #456
1.1233 +#431 := [monotonicity #457]: #461
1.1234 +#436 := [trans #431 #433]: #434
1.1235 +#460 := [quant-inst]: #459
1.1236 +#437 := [mp #460 #436]: #458
1.1237 +#420 := [unit-resolution #437 #684]: #455
1.1238 +#425 := [unit-resolution #420 #424]: #452
1.1239 +#405 := (= #22 #451)
1.1240 #661 := (= uf_3 #660)
1.1241 #4 := (:var 0 T1)
1.1242 #5 := (uf_2 #4)
1.1243 @@ -10151,117 +10334,136 @@
1.1244 #663 := (not #665)
1.1245 #653 := (or #663 #661)
1.1246 #312 := [quant-inst]: #653
1.1247 -#455 := [unit-resolution #312 #671]: #661
1.1248 -#457 := [monotonicity #455]: #456
1.1249 -#458 := [trans #457 #453]: #442
1.1250 -#459 := (not #442)
1.1251 -#460 := (or #459 #609)
1.1252 -#443 := [th-lemma]: #460
1.1253 -#461 := [unit-resolution #443 #451 #458]: false
1.1254 -#431 := [lemma #461]: #609
1.1255 -#613 := (or #465 #612)
1.1256 -#615 := (or #650 #465 #612)
1.1257 +#415 := [unit-resolution #312 #671]: #661
1.1258 +#407 := [monotonicity #415]: #405
1.1259 +#408 := [trans #407 #425]: #421
1.1260 +#411 := (not #421)
1.1261 +#412 := (or #411 #447)
1.1262 +#416 := [th-lemma]: #412
1.1263 +#409 := [unit-resolution #416 #424 #408]: false
1.1264 +#417 := [lemma #409]: #447
1.1265 +#302 := -1::int
1.1266 +#618 := (* -1::int #150)
1.1267 +#624 := (+ #144 #618)
1.1268 +#595 := (<= #624 0::int)
1.1269 +#465 := (= #624 0::int)
1.1270 +#489 := (or #603 #465)
1.1271 +#482 := (or #650 #603 #465)
1.1272 #616 := (>= #144 0::int)
1.1273 #617 := (not #616)
1.1274 #622 := (= #144 #150)
1.1275 #623 := (or #622 #617)
1.1276 -#444 := (or #650 #623)
1.1277 -#602 := (iff #444 #615)
1.1278 -#447 := (or #650 #613)
1.1279 -#603 := (iff #447 #615)
1.1280 -#604 := [rewrite]: #603
1.1281 -#600 := (iff #444 #447)
1.1282 -#614 := (iff #623 #613)
1.1283 -#606 := (iff #617 #612)
1.1284 -#610 := (iff #616 #609)
1.1285 -#611 := [rewrite]: #610
1.1286 -#607 := [monotonicity #611]: #606
1.1287 +#497 := (or #650 #623)
1.1288 +#504 := (iff #497 #482)
1.1289 +#500 := (or #650 #489)
1.1290 +#502 := (iff #500 #482)
1.1291 +#503 := [rewrite]: #502
1.1292 +#493 := (iff #497 #500)
1.1293 +#594 := (iff #623 #489)
1.1294 +#609 := (* 1::int #22)
1.1295 +#610 := (>= #609 0::int)
1.1296 +#606 := (not #610)
1.1297 +#614 := (or #465 #606)
1.1298 +#498 := (iff #614 #489)
1.1299 +#605 := (or #465 #603)
1.1300 +#448 := (iff #605 #489)
1.1301 +#596 := [rewrite]: #448
1.1302 +#487 := (iff #614 #605)
1.1303 +#604 := (iff #606 #603)
1.1304 +#600 := (iff #610 #447)
1.1305 +#444 := (= #609 #22)
1.1306 +#446 := [rewrite]: #444
1.1307 +#601 := [monotonicity #446]: #600
1.1308 +#602 := [monotonicity #601]: #604
1.1309 +#488 := [monotonicity #602]: #487
1.1310 +#593 := [trans #488 #596]: #498
1.1311 +#608 := (iff #623 #614)
1.1312 +#607 := (iff #617 #606)
1.1313 +#611 := (iff #616 #610)
1.1314 +#612 := [rewrite]: #611
1.1315 +#613 := [monotonicity #612]: #607
1.1316 #466 := (iff #622 #465)
1.1317 #467 := [rewrite]: #466
1.1318 -#608 := [monotonicity #467 #607]: #614
1.1319 -#601 := [monotonicity #608]: #600
1.1320 -#605 := [trans #601 #604]: #602
1.1321 -#446 := [quant-inst]: #444
1.1322 -#487 := [mp #446 #605]: #615
1.1323 -#439 := [unit-resolution #487 #678]: #613
1.1324 -#435 := [unit-resolution #439 #431]: #465
1.1325 -#440 := (not #465)
1.1326 -#419 := (or #440 #488)
1.1327 -#422 := [th-lemma]: #419
1.1328 -#426 := [unit-resolution #422 #435]: #488
1.1329 -#430 := (not #488)
1.1330 -#433 := (or #595 #612 #430)
1.1331 -#438 := [th-lemma]: #433
1.1332 -#402 := [unit-resolution #438 #431 #426]: #595
1.1333 -#590 := -3::int
1.1334 -#579 := (* -1::int #588)
1.1335 -#589 := (+ #150 #579)
1.1336 -#553 := (<= #589 -3::int)
1.1337 -#591 := (= #589 -3::int)
1.1338 -#581 := (>= #150 -3::int)
1.1339 +#615 := [monotonicity #467 #613]: #608
1.1340 +#597 := [trans #615 #593]: #594
1.1341 +#501 := [monotonicity #597]: #493
1.1342 +#505 := [trans #501 #503]: #504
1.1343 +#499 := [quant-inst]: #497
1.1344 +#598 := [mp #499 #505]: #482
1.1345 +#404 := [unit-resolution #598 #678]: #489
1.1346 +#386 := [unit-resolution #404 #417]: #465
1.1347 +#388 := (not #465)
1.1348 +#389 := (or #388 #595)
1.1349 +#390 := [th-lemma]: #389
1.1350 +#391 := [unit-resolution #390 #386]: #595
1.1351 +#395 := (not #595)
1.1352 +#413 := (or #566 #603 #395)
1.1353 +#403 := [th-lemma]: #413
1.1354 +#373 := [unit-resolution #403 #391 #417]: #566
1.1355 +#553 := -3::int
1.1356 +#551 := (* -1::int #568)
1.1357 +#552 := (+ #150 #551)
1.1358 +#535 := (<= #552 -3::int)
1.1359 +#554 := (= #552 -3::int)
1.1360 +#557 := (>= #150 -3::int)
1.1361 #644 := (>= #22 -1::int)
1.1362 -#428 := (or #612 #644)
1.1363 -#429 := [th-lemma]: #428
1.1364 -#427 := [unit-resolution #429 #431]: #644
1.1365 +#392 := (or #603 #644)
1.1366 +#393 := [th-lemma]: #392
1.1367 +#394 := [unit-resolution #393 #417]: #644
1.1368 #646 := (not #644)
1.1369 -#418 := (or #581 #646 #430)
1.1370 -#421 := [th-lemma]: #418
1.1371 -#423 := [unit-resolution #421 #426 #427]: #581
1.1372 -#584 := (not #581)
1.1373 -#573 := (or #584 #591)
1.1374 -#562 := (or #650 #584 #591)
1.1375 -#599 := (>= #156 0::int)
1.1376 -#586 := (not #599)
1.1377 -#580 := (= #156 #588)
1.1378 -#577 := (or #580 #586)
1.1379 -#563 := (or #650 #577)
1.1380 -#549 := (iff #563 #562)
1.1381 -#566 := (or #650 #573)
1.1382 -#568 := (iff #566 #562)
1.1383 -#548 := [rewrite]: #568
1.1384 -#567 := (iff #563 #566)
1.1385 -#571 := (iff #577 #573)
1.1386 -#569 := (or #591 #584)
1.1387 -#574 := (iff #569 #573)
1.1388 -#575 := [rewrite]: #574
1.1389 -#570 := (iff #577 #569)
1.1390 -#578 := (iff #586 #584)
1.1391 -#582 := (iff #599 #581)
1.1392 -#583 := [rewrite]: #582
1.1393 -#585 := [monotonicity #583]: #578
1.1394 -#587 := (iff #580 #591)
1.1395 -#592 := [rewrite]: #587
1.1396 -#572 := [monotonicity #592 #585]: #570
1.1397 -#576 := [trans #572 #575]: #571
1.1398 -#564 := [monotonicity #576]: #567
1.1399 -#551 := [trans #564 #548]: #549
1.1400 -#565 := [quant-inst]: #563
1.1401 -#552 := [mp #565 #551]: #562
1.1402 -#424 := [unit-resolution #552 #678]: #573
1.1403 -#420 := [unit-resolution #424 #423]: #591
1.1404 -#425 := (not #591)
1.1405 -#415 := (or #425 #553)
1.1406 -#405 := [th-lemma]: #415
1.1407 -#407 := [unit-resolution #405 #420]: #553
1.1408 -#404 := (not #553)
1.1409 -#401 := (not #595)
1.1410 -#386 := (or #403 #401 #404)
1.1411 -#388 := [th-lemma]: #386
1.1412 -#389 := [unit-resolution #388 #407 #402]: #403
1.1413 -#391 := (or #390 #547)
1.1414 -#392 := [th-lemma]: #391
1.1415 -#393 := [unit-resolution #392 #389]: #390
1.1416 -#376 := [unit-resolution #393 #399]: false
1.1417 -#378 := [lemma #376]: #327
1.1418 +#396 := (or #557 #646 #395)
1.1419 +#397 := [th-lemma]: #396
1.1420 +#398 := [unit-resolution #397 #391 #394]: #557
1.1421 +#560 := (not #557)
1.1422 +#539 := (or #554 #560)
1.1423 +#543 := (or #650 #554 #560)
1.1424 +#567 := (>= #156 0::int)
1.1425 +#564 := (not #567)
1.1426 +#548 := (= #156 #568)
1.1427 +#549 := (or #548 #564)
1.1428 +#544 := (or #650 #549)
1.1429 +#530 := (iff #544 #543)
1.1430 +#546 := (or #650 #539)
1.1431 +#533 := (iff #546 #543)
1.1432 +#529 := [rewrite]: #533
1.1433 +#541 := (iff #544 #546)
1.1434 +#540 := (iff #549 #539)
1.1435 +#550 := (iff #564 #560)
1.1436 +#558 := (iff #567 #557)
1.1437 +#559 := [rewrite]: #558
1.1438 +#561 := [monotonicity #559]: #550
1.1439 +#555 := (iff #548 #554)
1.1440 +#556 := [rewrite]: #555
1.1441 +#542 := [monotonicity #556 #561]: #540
1.1442 +#547 := [monotonicity #542]: #541
1.1443 +#531 := [trans #547 #529]: #530
1.1444 +#545 := [quant-inst]: #544
1.1445 +#534 := [mp #545 #531]: #543
1.1446 +#387 := [unit-resolution #534 #678]: #539
1.1447 +#399 := [unit-resolution #387 #398]: #554
1.1448 +#376 := (not #554)
1.1449 +#378 := (or #376 #535)
1.1450 +#379 := [th-lemma]: #378
1.1451 +#380 := [unit-resolution #379 #399]: #535
1.1452 +#365 := (not #535)
1.1453 +#364 := (not #566)
1.1454 +#366 := (or #375 #364 #365)
1.1455 +#358 := [th-lemma]: #366
1.1456 +#367 := [unit-resolution #358 #380 #373]: #375
1.1457 +#359 := (or #368 #527)
1.1458 +#369 := [th-lemma]: #359
1.1459 +#350 := [unit-resolution #369 #367]: #368
1.1460 +#321 := [unit-resolution #350 #355]: false
1.1461 +#323 := [lemma #321]: #327
1.1462 #249 := (= #141 #161)
1.1463 #334 := (not #249)
1.1464 -#396 := (= #297 #588)
1.1465 -#385 := [hypothesis]: #249
1.1466 -#370 := [monotonicity #385]: #396
1.1467 -#380 := (not #396)
1.1468 -#434 := (+ #297 #579)
1.1469 -#280 := (>= #434 0::int)
1.1470 -#414 := (not #280)
1.1471 +#343 := (= #297 #568)
1.1472 +#322 := [hypothesis]: #249
1.1473 +#333 := [monotonicity #322]: #343
1.1474 +#315 := (not #343)
1.1475 +#414 := (+ #297 #551)
1.1476 +#401 := (>= #414 0::int)
1.1477 +#372 := (not #401)
1.1478 #303 := (* -1::int #297)
1.1479 #304 := (+ #22 #303)
1.1480 #356 := (>= #304 -1::int)
1.1481 @@ -10290,21 +10492,21 @@
1.1482 #256 := [trans #360 #362]: #363
1.1483 #637 := [quant-inst]: #651
1.1484 #633 := [mp #637 #256]: #648
1.1485 -#408 := [unit-resolution #633 #678]: #649
1.1486 -#411 := [unit-resolution #408 #427]: #641
1.1487 -#412 := (not #641)
1.1488 -#416 := (or #412 #356)
1.1489 -#409 := [th-lemma]: #416
1.1490 -#417 := [unit-resolution #409 #411]: #356
1.1491 -#410 := [hypothesis]: #280
1.1492 -#413 := [th-lemma #423 #410 #417 #407 #426]: false
1.1493 -#400 := [lemma #413]: #414
1.1494 -#381 := (or #380 #280)
1.1495 -#382 := [th-lemma]: #381
1.1496 -#377 := [unit-resolution #382 #400]: #380
1.1497 -#371 := [unit-resolution #377 #370]: false
1.1498 -#372 := [lemma #371]: #334
1.1499 -#352 := (or #249 #250 #336)
1.1500 +#381 := [unit-resolution #633 #678]: #649
1.1501 +#382 := [unit-resolution #381 #394]: #641
1.1502 +#383 := (not #641)
1.1503 +#384 := (or #383 #356)
1.1504 +#377 := [th-lemma]: #384
1.1505 +#385 := [unit-resolution #377 #382]: #356
1.1506 +#370 := [hypothesis]: #401
1.1507 +#371 := [th-lemma #398 #370 #385 #380 #391]: false
1.1508 +#374 := [lemma #371]: #372
1.1509 +#328 := (or #315 #401)
1.1510 +#329 := [th-lemma]: #328
1.1511 +#332 := [unit-resolution #329 #374]: #315
1.1512 +#316 := [unit-resolution #332 #333]: false
1.1513 +#318 := [lemma #316]: #334
1.1514 +#295 := (or #249 #250 #336)
1.1515 #335 := (not #250)
1.1516 #338 := (and #334 #335 #327)
1.1517 #339 := (not #338)
1.1518 @@ -10352,28 +10554,28 @@
1.1519 #177 := [mp #137 #174]: #172
1.1520 #326 := (or #169 #339)
1.1521 #659 := [def-axiom]: #326
1.1522 -#351 := [unit-resolution #659 #177]: #339
1.1523 +#294 := [unit-resolution #659 #177]: #339
1.1524 #314 := (or #338 #249 #250 #336)
1.1525 #445 := [def-axiom]: #314
1.1526 -#343 := [unit-resolution #445 #351]: #352
1.1527 -#353 := [unit-resolution #343 #372 #378]: #250
1.1528 -#321 := [monotonicity #353]: #355
1.1529 -#323 := [trans #321 #394]: #357
1.1530 -#368 := (not #357)
1.1531 +#293 := [unit-resolution #445 #294]: #295
1.1532 +#296 := [unit-resolution #293 #318 #323]: #250
1.1533 +#290 := [monotonicity #296]: #287
1.1534 +#285 := [trans #290 #351]: #357
1.1535 +#310 := (not #357)
1.1536 #620 := (<= #297 0::int)
1.1537 -#364 := (not #620)
1.1538 +#305 := (not #620)
1.1539 #634 := (<= #304 -1::int)
1.1540 -#374 := (or #412 #634)
1.1541 -#373 := [th-lemma]: #374
1.1542 -#375 := [unit-resolution #373 #411]: #634
1.1543 -#365 := (not #634)
1.1544 -#366 := (or #364 #612 #365)
1.1545 -#358 := [th-lemma]: #366
1.1546 -#367 := [unit-resolution #358 #375 #431]: #364
1.1547 -#359 := (or #368 #620)
1.1548 -#369 := [th-lemma]: #359
1.1549 -#350 := [unit-resolution #369 #367]: #368
1.1550 -[unit-resolution #350 #323]: false
1.1551 +#319 := (or #383 #634)
1.1552 +#298 := [th-lemma]: #319
1.1553 +#300 := [unit-resolution #298 #382]: #634
1.1554 +#306 := (not #634)
1.1555 +#307 := (or #305 #603 #306)
1.1556 +#308 := [th-lemma]: #307
1.1557 +#309 := [unit-resolution #308 #300 #417]: #305
1.1558 +#299 := (or #310 #620)
1.1559 +#311 := [th-lemma]: #299
1.1560 +#292 := [unit-resolution #311 #309]: #310
1.1561 +[unit-resolution #292 #285]: false
1.1562 unsat
1.1563
1.1564 ipe8HUL/t33OoeNl/z0smQ 4011
1.1565 @@ -10539,7 +10741,7 @@
1.1566 [th-lemma #656 #361 #261]: false
1.1567 unsat
1.1568
1.1569 -eRjXXrQSzpzyc8Ro409d3Q 14366
1.1570 +9FrZeHP8ZKJM+JmhfAjimQ 14889
1.1571 #2 := false
1.1572 #9 := 0::int
1.1573 decl uf_2 :: (-> T1 int)
1.1574 @@ -10551,46 +10753,46 @@
1.1575 #38 := (* 4::int #37)
1.1576 #39 := (uf_1 #38)
1.1577 #40 := (uf_2 #39)
1.1578 -#527 := (= #40 0::int)
1.1579 -#976 := (not #527)
1.1580 -#502 := (<= #40 0::int)
1.1581 -#971 := (not #502)
1.1582 +#504 := (= #40 0::int)
1.1583 +#995 := (not #504)
1.1584 +#475 := (<= #40 0::int)
1.1585 +#990 := (not #475)
1.1586 #22 := 1::int
1.1587 #186 := (+ 1::int #40)
1.1588 #189 := (uf_1 #186)
1.1589 -#506 := (uf_2 #189)
1.1590 -#407 := (<= #506 1::int)
1.1591 -#876 := (not #407)
1.1592 +#467 := (uf_2 #189)
1.1593 +#380 := (<= #467 1::int)
1.1594 +#893 := (not #380)
1.1595 decl up_4 :: (-> T1 T1 bool)
1.1596 #4 := (:var 0 T1)
1.1597 -#408 := (up_4 #4 #189)
1.1598 -#393 := (pattern #408)
1.1599 -#413 := (= #4 #189)
1.1600 -#414 := (not #408)
1.1601 +#386 := (up_4 #4 #189)
1.1602 +#374 := (pattern #386)
1.1603 +#382 := (not #386)
1.1604 +#385 := (= #4 #189)
1.1605 #26 := (uf_1 1::int)
1.1606 #27 := (= #4 #26)
1.1607 -#392 := (or #27 #414 #413)
1.1608 -#397 := (forall (vars (?x5 T1)) (:pat #393) #392)
1.1609 -#383 := (not #397)
1.1610 -#382 := (or #383 #407)
1.1611 -#375 := (not #382)
1.1612 +#845 := (or #27 #385 #382)
1.1613 +#848 := (forall (vars (?x5 T1)) (:pat #374) #845)
1.1614 +#851 := (not #848)
1.1615 +#854 := (or #380 #851)
1.1616 +#857 := (not #854)
1.1617 decl up_3 :: (-> T1 bool)
1.1618 #192 := (up_3 #189)
1.1619 -#404 := (not #192)
1.1620 -#841 := (or #404 #375)
1.1621 +#840 := (not #192)
1.1622 +#860 := (or #840 #857)
1.1623 decl ?x5!0 :: (-> T1 T1)
1.1624 -#422 := (?x5!0 #189)
1.1625 -#434 := (= #189 #422)
1.1626 -#417 := (up_4 #422 #189)
1.1627 -#418 := (not #417)
1.1628 -#415 := (= #26 #422)
1.1629 -#847 := (or #415 #418 #434)
1.1630 -#850 := (not #847)
1.1631 -#853 := (or #192 #407 #850)
1.1632 -#856 := (not #853)
1.1633 -#844 := (not #841)
1.1634 -#859 := (or #844 #856)
1.1635 -#862 := (not #859)
1.1636 +#392 := (?x5!0 #189)
1.1637 +#397 := (up_4 #392 #189)
1.1638 +#390 := (not #397)
1.1639 +#396 := (= #26 #392)
1.1640 +#395 := (= #189 #392)
1.1641 +#866 := (or #395 #396 #390)
1.1642 +#869 := (not #866)
1.1643 +#872 := (or #192 #380 #869)
1.1644 +#875 := (not #872)
1.1645 +#863 := (not #860)
1.1646 +#878 := (or #863 #875)
1.1647 +#881 := (not #878)
1.1648 #5 := (uf_2 #4)
1.1649 #787 := (pattern #5)
1.1650 #21 := (up_3 #4)
1.1651 @@ -10769,64 +10971,59 @@
1.1652 #314 := [mp #267 #313]: #311
1.1653 #839 := [mp #314 #838]: #836
1.1654 #589 := (not #836)
1.1655 -#865 := (or #589 #862)
1.1656 -#416 := (or #418 #415 #434)
1.1657 -#419 := (not #416)
1.1658 -#409 := (or #192 #407 #419)
1.1659 -#410 := (not #409)
1.1660 -#389 := (or #414 #27 #413)
1.1661 -#394 := (forall (vars (?x5 T1)) (:pat #393) #389)
1.1662 -#399 := (not #394)
1.1663 -#401 := (or #407 #399)
1.1664 -#402 := (not #401)
1.1665 -#400 := (or #404 #402)
1.1666 -#405 := (not #400)
1.1667 -#388 := (or #405 #410)
1.1668 -#391 := (not #388)
1.1669 -#866 := (or #589 #391)
1.1670 -#868 := (iff #866 #865)
1.1671 -#870 := (iff #865 #865)
1.1672 -#871 := [rewrite]: #870
1.1673 -#863 := (iff #391 #862)
1.1674 -#860 := (iff #388 #859)
1.1675 -#857 := (iff #410 #856)
1.1676 -#854 := (iff #409 #853)
1.1677 -#851 := (iff #419 #850)
1.1678 -#848 := (iff #416 #847)
1.1679 -#849 := [rewrite]: #848
1.1680 -#852 := [monotonicity #849]: #851
1.1681 -#855 := [monotonicity #852]: #854
1.1682 -#858 := [monotonicity #855]: #857
1.1683 -#845 := (iff #405 #844)
1.1684 -#842 := (iff #400 #841)
1.1685 -#378 := (iff #402 #375)
1.1686 -#376 := (iff #401 #382)
1.1687 -#384 := (or #407 #383)
1.1688 -#387 := (iff #384 #382)
1.1689 -#374 := [rewrite]: #387
1.1690 -#385 := (iff #401 #384)
1.1691 -#380 := (iff #399 #383)
1.1692 -#390 := (iff #394 #397)
1.1693 -#395 := (iff #389 #392)
1.1694 -#396 := [rewrite]: #395
1.1695 -#398 := [quant-intro #396]: #390
1.1696 -#381 := [monotonicity #398]: #380
1.1697 -#386 := [monotonicity #381]: #385
1.1698 -#377 := [trans #386 #374]: #376
1.1699 -#840 := [monotonicity #377]: #378
1.1700 -#843 := [monotonicity #840]: #842
1.1701 -#846 := [monotonicity #843]: #845
1.1702 -#861 := [monotonicity #846 #858]: #860
1.1703 -#864 := [monotonicity #861]: #863
1.1704 -#869 := [monotonicity #864]: #868
1.1705 -#872 := [trans #869 #871]: #868
1.1706 -#867 := [quant-inst]: #866
1.1707 -#873 := [mp #867 #872]: #865
1.1708 -#947 := [unit-resolution #873 #839]: #862
1.1709 -#905 := (or #859 #841)
1.1710 -#906 := [def-axiom]: #905
1.1711 -#948 := [unit-resolution #906 #947]: #841
1.1712 -#951 := (or #844 #375)
1.1713 +#884 := (or #589 #881)
1.1714 +#398 := (or #390 #396 #395)
1.1715 +#383 := (not #398)
1.1716 +#381 := (or #192 #380 #383)
1.1717 +#384 := (not #381)
1.1718 +#387 := (or #382 #27 #385)
1.1719 +#376 := (forall (vars (?x5 T1)) (:pat #374) #387)
1.1720 +#377 := (not #376)
1.1721 +#375 := (or #380 #377)
1.1722 +#378 := (not #375)
1.1723 +#841 := (or #840 #378)
1.1724 +#842 := (not #841)
1.1725 +#843 := (or #842 #384)
1.1726 +#844 := (not #843)
1.1727 +#885 := (or #589 #844)
1.1728 +#887 := (iff #885 #884)
1.1729 +#889 := (iff #884 #884)
1.1730 +#890 := [rewrite]: #889
1.1731 +#882 := (iff #844 #881)
1.1732 +#879 := (iff #843 #878)
1.1733 +#876 := (iff #384 #875)
1.1734 +#873 := (iff #381 #872)
1.1735 +#870 := (iff #383 #869)
1.1736 +#867 := (iff #398 #866)
1.1737 +#868 := [rewrite]: #867
1.1738 +#871 := [monotonicity #868]: #870
1.1739 +#874 := [monotonicity #871]: #873
1.1740 +#877 := [monotonicity #874]: #876
1.1741 +#864 := (iff #842 #863)
1.1742 +#861 := (iff #841 #860)
1.1743 +#858 := (iff #378 #857)
1.1744 +#855 := (iff #375 #854)
1.1745 +#852 := (iff #377 #851)
1.1746 +#849 := (iff #376 #848)
1.1747 +#846 := (iff #387 #845)
1.1748 +#847 := [rewrite]: #846
1.1749 +#850 := [quant-intro #847]: #849
1.1750 +#853 := [monotonicity #850]: #852
1.1751 +#856 := [monotonicity #853]: #855
1.1752 +#859 := [monotonicity #856]: #858
1.1753 +#862 := [monotonicity #859]: #861
1.1754 +#865 := [monotonicity #862]: #864
1.1755 +#880 := [monotonicity #865 #877]: #879
1.1756 +#883 := [monotonicity #880]: #882
1.1757 +#888 := [monotonicity #883]: #887
1.1758 +#891 := [trans #888 #890]: #887
1.1759 +#886 := [quant-inst]: #885
1.1760 +#892 := [mp #886 #891]: #884
1.1761 +#966 := [unit-resolution #892 #839]: #881
1.1762 +#924 := (or #878 #860)
1.1763 +#925 := [def-axiom]: #924
1.1764 +#967 := [unit-resolution #925 #966]: #860
1.1765 +#970 := (or #863 #857)
1.1766 #41 := (+ #40 1::int)
1.1767 #42 := (uf_1 #41)
1.1768 #43 := (up_3 #42)
1.1769 @@ -10838,30 +11035,30 @@
1.1770 #194 := [monotonicity #191]: #193
1.1771 #185 := [asserted]: #43
1.1772 #197 := [mp #185 #194]: #192
1.1773 -#885 := (or #844 #404 #375)
1.1774 -#886 := [def-axiom]: #885
1.1775 -#952 := [unit-resolution #886 #197]: #951
1.1776 -#953 := [unit-resolution #952 #948]: #375
1.1777 -#877 := (or #382 #876)
1.1778 -#878 := [def-axiom]: #877
1.1779 -#954 := [unit-resolution #878 #953]: #876
1.1780 +#904 := (or #863 #840 #857)
1.1781 +#905 := [def-axiom]: #904
1.1782 +#971 := [unit-resolution #905 #197]: #970
1.1783 +#972 := [unit-resolution #971 #967]: #857
1.1784 +#894 := (or #854 #893)
1.1785 +#895 := [def-axiom]: #894
1.1786 +#973 := [unit-resolution #895 #972]: #893
1.1787 #542 := -1::int
1.1788 -#508 := (* -1::int #506)
1.1789 -#493 := (+ #40 #508)
1.1790 -#438 := (>= #493 -1::int)
1.1791 -#494 := (= #493 -1::int)
1.1792 -#496 := (>= #40 -1::int)
1.1793 -#451 := (= #506 0::int)
1.1794 -#959 := (not #451)
1.1795 -#432 := (<= #506 0::int)
1.1796 -#955 := (not #432)
1.1797 -#956 := (or #955 #407)
1.1798 -#957 := [th-lemma]: #956
1.1799 -#958 := [unit-resolution #957 #954]: #955
1.1800 -#960 := (or #959 #432)
1.1801 -#961 := [th-lemma]: #960
1.1802 -#962 := [unit-resolution #961 #958]: #959
1.1803 -#453 := (or #451 #496)
1.1804 +#446 := (* -1::int #467)
1.1805 +#447 := (+ #40 #446)
1.1806 +#416 := (>= #447 -1::int)
1.1807 +#438 := (= #447 -1::int)
1.1808 +#453 := (>= #40 -1::int)
1.1809 +#419 := (= #467 0::int)
1.1810 +#978 := (not #419)
1.1811 +#388 := (<= #467 0::int)
1.1812 +#974 := (not #388)
1.1813 +#975 := (or #974 #380)
1.1814 +#976 := [th-lemma]: #975
1.1815 +#977 := [unit-resolution #976 #973]: #974
1.1816 +#979 := (or #978 #388)
1.1817 +#980 := [th-lemma]: #979
1.1818 +#981 := [unit-resolution #980 #977]: #978
1.1819 +#409 := (or #419 #453)
1.1820 #10 := (:var 0 int)
1.1821 #12 := (uf_1 #10)
1.1822 #795 := (pattern #12)
1.1823 @@ -10924,28 +11121,28 @@
1.1824 #145 := [mp #105 #144]: #140
1.1825 #227 := [mp~ #145 #208]: #140
1.1826 #807 := [mp #227 #806]: #802
1.1827 -#514 := (not #802)
1.1828 -#445 := (or #514 #451 #496)
1.1829 -#504 := (>= #186 0::int)
1.1830 -#452 := (or #451 #504)
1.1831 -#456 := (or #514 #452)
1.1832 -#429 := (iff #456 #445)
1.1833 -#441 := (or #514 #453)
1.1834 -#423 := (iff #441 #445)
1.1835 -#428 := [rewrite]: #423
1.1836 -#442 := (iff #456 #441)
1.1837 -#454 := (iff #452 #453)
1.1838 -#498 := (iff #504 #496)
1.1839 -#487 := [rewrite]: #498
1.1840 -#455 := [monotonicity #487]: #454
1.1841 -#421 := [monotonicity #455]: #442
1.1842 -#430 := [trans #421 #428]: #429
1.1843 -#439 := [quant-inst]: #456
1.1844 -#431 := [mp #439 #430]: #445
1.1845 -#963 := [unit-resolution #431 #807]: #453
1.1846 -#964 := [unit-resolution #963 #962]: #496
1.1847 -#488 := (not #496)
1.1848 -#490 := (or #494 #488)
1.1849 +#496 := (not #802)
1.1850 +#408 := (or #496 #419 #453)
1.1851 +#476 := (>= #186 0::int)
1.1852 +#407 := (or #419 #476)
1.1853 +#414 := (or #496 #407)
1.1854 +#404 := (iff #414 #408)
1.1855 +#393 := (or #496 #409)
1.1856 +#401 := (iff #393 #408)
1.1857 +#402 := [rewrite]: #401
1.1858 +#394 := (iff #414 #393)
1.1859 +#410 := (iff #407 #409)
1.1860 +#454 := (iff #476 #453)
1.1861 +#455 := [rewrite]: #454
1.1862 +#413 := [monotonicity #455]: #410
1.1863 +#399 := [monotonicity #413]: #394
1.1864 +#400 := [trans #399 #402]: #404
1.1865 +#389 := [quant-inst]: #414
1.1866 +#405 := [mp #389 #400]: #408
1.1867 +#982 := [unit-resolution #405 #807]: #409
1.1868 +#983 := [unit-resolution #982 #981]: #453
1.1869 +#445 := (not #453)
1.1870 +#441 := (or #438 #445)
1.1871 #69 := (= #10 #13)
1.1872 #94 := (or #69 #88)
1.1873 #796 := (forall (vars (?x2 int)) (:pat #795) #94)
1.1874 @@ -10995,48 +11192,48 @@
1.1875 #104 := [mp #68 #103]: #99
1.1876 #224 := [mp~ #104 #196]: #99
1.1877 #801 := [mp #224 #800]: #796
1.1878 -#530 := (not #796)
1.1879 -#492 := (or #530 #494 #488)
1.1880 -#505 := (not #504)
1.1881 -#507 := (= #186 #506)
1.1882 -#500 := (or #507 #505)
1.1883 -#473 := (or #530 #500)
1.1884 -#478 := (iff #473 #492)
1.1885 -#475 := (or #530 #490)
1.1886 -#477 := (iff #475 #492)
1.1887 -#467 := [rewrite]: #477
1.1888 -#466 := (iff #473 #475)
1.1889 -#491 := (iff #500 #490)
1.1890 -#489 := (iff #505 #488)
1.1891 -#481 := [monotonicity #487]: #489
1.1892 -#495 := (iff #507 #494)
1.1893 -#497 := [rewrite]: #495
1.1894 -#482 := [monotonicity #497 #481]: #491
1.1895 -#476 := [monotonicity #482]: #466
1.1896 -#444 := [trans #476 #467]: #478
1.1897 -#474 := [quant-inst]: #473
1.1898 -#446 := [mp #474 #444]: #492
1.1899 -#965 := [unit-resolution #446 #801]: #490
1.1900 -#966 := [unit-resolution #965 #964]: #494
1.1901 -#967 := (not #494)
1.1902 -#968 := (or #967 #438)
1.1903 -#969 := [th-lemma]: #968
1.1904 -#970 := [unit-resolution #969 #966]: #438
1.1905 -#972 := (not #438)
1.1906 -#973 := (or #971 #407 #972)
1.1907 -#974 := [th-lemma]: #973
1.1908 -#975 := [unit-resolution #974 #970 #954]: #971
1.1909 -#977 := (or #976 #502)
1.1910 -#978 := [th-lemma]: #977
1.1911 -#979 := [unit-resolution #978 #975]: #976
1.1912 -#553 := (>= #37 0::int)
1.1913 -#546 := (not #553)
1.1914 +#514 := (not #796)
1.1915 +#423 := (or #514 #438 #445)
1.1916 +#477 := (not #476)
1.1917 +#478 := (= #186 #467)
1.1918 +#444 := (or #478 #477)
1.1919 +#428 := (or #514 #444)
1.1920 +#434 := (iff #428 #423)
1.1921 +#430 := (or #514 #441)
1.1922 +#433 := (iff #430 #423)
1.1923 +#422 := [rewrite]: #433
1.1924 +#431 := (iff #428 #430)
1.1925 +#442 := (iff #444 #441)
1.1926 +#456 := (iff #477 #445)
1.1927 +#439 := [monotonicity #455]: #456
1.1928 +#451 := (iff #478 #438)
1.1929 +#452 := [rewrite]: #451
1.1930 +#421 := [monotonicity #452 #439]: #442
1.1931 +#432 := [monotonicity #421]: #431
1.1932 +#415 := [trans #432 #422]: #434
1.1933 +#429 := [quant-inst]: #428
1.1934 +#417 := [mp #429 #415]: #423
1.1935 +#984 := [unit-resolution #417 #801]: #441
1.1936 +#985 := [unit-resolution #984 #983]: #438
1.1937 +#986 := (not #438)
1.1938 +#987 := (or #986 #416)
1.1939 +#988 := [th-lemma]: #987
1.1940 +#989 := [unit-resolution #988 #985]: #416
1.1941 +#991 := (not #416)
1.1942 +#992 := (or #990 #380 #991)
1.1943 +#993 := [th-lemma]: #992
1.1944 +#994 := [unit-resolution #993 #989 #973]: #990
1.1945 +#996 := (or #995 #475)
1.1946 +#997 := [th-lemma]: #996
1.1947 +#998 := [unit-resolution #997 #994]: #995
1.1948 +#536 := (>= #37 0::int)
1.1949 +#525 := (not #536)
1.1950 #545 := (* -1::int #40)
1.1951 #549 := (+ #38 #545)
1.1952 #551 := (= #549 0::int)
1.1953 -#984 := (not #551)
1.1954 -#524 := (>= #549 0::int)
1.1955 -#980 := (not #524)
1.1956 +#1003 := (not #551)
1.1957 +#503 := (>= #549 0::int)
1.1958 +#999 := (not #503)
1.1959 #201 := (>= #37 1::int)
1.1960 #202 := (not #201)
1.1961 #44 := (<= 1::int #37)
1.1962 @@ -11047,55 +11244,79 @@
1.1963 #204 := [monotonicity #200]: #203
1.1964 #195 := [asserted]: #45
1.1965 #205 := [mp #195 #204]: #202
1.1966 -#981 := (or #980 #201 #407 #972)
1.1967 -#982 := [th-lemma]: #981
1.1968 -#983 := [unit-resolution #982 #205 #970 #954]: #980
1.1969 -#985 := (or #984 #524)
1.1970 -#986 := [th-lemma]: #985
1.1971 -#987 := [unit-resolution #986 #983]: #984
1.1972 -#548 := (or #551 #546)
1.1973 -#531 := (or #530 #551 #546)
1.1974 +#1000 := (or #999 #201 #380 #991)
1.1975 +#1001 := [th-lemma]: #1000
1.1976 +#1002 := [unit-resolution #1001 #205 #989 #973]: #999
1.1977 +#1004 := (or #1003 #503)
1.1978 +#1005 := [th-lemma]: #1004
1.1979 +#1006 := [unit-resolution #1005 #1002]: #1003
1.1980 +#527 := (or #525 #551)
1.1981 +#515 := (or #514 #525 #551)
1.1982 #403 := (>= #38 0::int)
1.1983 #562 := (not #403)
1.1984 #558 := (= #38 #40)
1.1985 #563 := (or #558 #562)
1.1986 -#534 := (or #530 #563)
1.1987 -#537 := (iff #534 #531)
1.1988 -#539 := (or #530 #548)
1.1989 -#533 := (iff #539 #531)
1.1990 -#536 := [rewrite]: #533
1.1991 -#532 := (iff #534 #539)
1.1992 -#538 := (iff #563 #548)
1.1993 -#547 := (iff #562 #546)
1.1994 -#541 := (iff #403 #553)
1.1995 -#544 := [rewrite]: #541
1.1996 -#543 := [monotonicity #544]: #547
1.1997 -#552 := (iff #558 #551)
1.1998 -#550 := [rewrite]: #552
1.1999 -#528 := [monotonicity #550 #543]: #538
1.2000 -#540 := [monotonicity #528]: #532
1.2001 -#523 := [trans #540 #536]: #537
1.2002 -#535 := [quant-inst]: #534
1.2003 -#525 := [mp #535 #523]: #531
1.2004 -#988 := [unit-resolution #525 #801]: #548
1.2005 -#989 := [unit-resolution #988 #987]: #546
1.2006 -#511 := (or #527 #553)
1.2007 -#515 := (or #514 #527 #553)
1.2008 -#509 := (or #527 #403)
1.2009 -#516 := (or #514 #509)
1.2010 +#516 := (or #514 #563)
1.2011 #522 := (iff #516 #515)
1.2012 -#518 := (or #514 #511)
1.2013 +#518 := (or #514 #527)
1.2014 #521 := (iff #518 #515)
1.2015 #510 := [rewrite]: #521
1.2016 #519 := (iff #516 #518)
1.2017 -#512 := (iff #509 #511)
1.2018 -#513 := [monotonicity #544]: #512
1.2019 +#512 := (iff #563 #527)
1.2020 +#553 := (* 1::int #37)
1.2021 +#541 := (>= #553 0::int)
1.2022 +#547 := (not #541)
1.2023 +#531 := (or #547 #551)
1.2024 +#509 := (iff #531 #527)
1.2025 +#526 := (iff #547 #525)
1.2026 +#537 := (iff #541 #536)
1.2027 +#540 := (= #553 #37)
1.2028 +#533 := [rewrite]: #540
1.2029 +#523 := [monotonicity #533]: #537
1.2030 +#524 := [monotonicity #523]: #526
1.2031 +#511 := [monotonicity #524]: #509
1.2032 +#539 := (iff #563 #531)
1.2033 +#538 := (or #551 #547)
1.2034 +#534 := (iff #538 #531)
1.2035 +#535 := [rewrite]: #534
1.2036 +#528 := (iff #563 #538)
1.2037 +#543 := (iff #562 #547)
1.2038 +#544 := (iff #403 #541)
1.2039 +#546 := [rewrite]: #544
1.2040 +#548 := [monotonicity #546]: #543
1.2041 +#552 := (iff #558 #551)
1.2042 +#550 := [rewrite]: #552
1.2043 +#530 := [monotonicity #550 #548]: #528
1.2044 +#532 := [trans #530 #535]: #539
1.2045 +#513 := [trans #532 #511]: #512
1.2046 #520 := [monotonicity #513]: #519
1.2047 #499 := [trans #520 #510]: #522
1.2048 #517 := [quant-inst]: #516
1.2049 #501 := [mp #517 #499]: #515
1.2050 -#990 := [unit-resolution #501 #807]: #511
1.2051 -[unit-resolution #990 #989 #979]: false
1.2052 +#1007 := [unit-resolution #501 #801]: #527
1.2053 +#1008 := [unit-resolution #1007 #1006]: #525
1.2054 +#508 := (or #504 #536)
1.2055 +#498 := (or #496 #504 #536)
1.2056 +#505 := (or #504 #403)
1.2057 +#487 := (or #496 #505)
1.2058 +#492 := (iff #487 #498)
1.2059 +#489 := (or #496 #508)
1.2060 +#491 := (iff #489 #498)
1.2061 +#482 := [rewrite]: #491
1.2062 +#481 := (iff #487 #489)
1.2063 +#495 := (iff #505 #508)
1.2064 +#506 := (or #504 #541)
1.2065 +#493 := (iff #506 #508)
1.2066 +#494 := [monotonicity #523]: #493
1.2067 +#507 := (iff #505 #506)
1.2068 +#500 := [monotonicity #546]: #507
1.2069 +#497 := [trans #500 #494]: #495
1.2070 +#490 := [monotonicity #497]: #481
1.2071 +#473 := [trans #490 #482]: #492
1.2072 +#488 := [quant-inst]: #487
1.2073 +#474 := [mp #488 #473]: #498
1.2074 +#1009 := [unit-resolution #474 #807]: #508
1.2075 +[unit-resolution #1009 #1008 #998]: false
1.2076 unsat
1.2077
1.2078 uq2MbDTgTG1nxWdwzZtWew 7
1.2079 @@ -12233,7 +12454,7 @@
1.2080 [mp #25 #34]: false
1.2081 unsat
1.2082
1.2083 -YG20f6Uf93koN6rVg/alpA 9362
1.2084 +YG20f6Uf93koN6rVg/alpA 9742
1.2085 #2 := false
1.2086 decl uf_1 :: (-> int T1)
1.2087 #37 := 6::int
1.2088 @@ -12248,18 +12469,18 @@
1.2089 #35 := (uf_1 #34)
1.2090 #36 := (uf_3 #35)
1.2091 #39 := (= #36 #38)
1.2092 -#476 := (uf_3 #38)
1.2093 -#403 := (= #476 #38)
1.2094 -#531 := (= #38 #476)
1.2095 -#620 := (uf_2 #38)
1.2096 +#484 := (uf_3 #38)
1.2097 +#372 := (= #484 #38)
1.2098 +#485 := (= #38 #484)
1.2099 +#592 := (uf_2 #38)
1.2100 #142 := -10::int
1.2101 -#513 := (+ -10::int #620)
1.2102 -#472 := (uf_1 #513)
1.2103 -#503 := (uf_3 #472)
1.2104 -#505 := (= #476 #503)
1.2105 +#496 := (+ -10::int #592)
1.2106 +#497 := (uf_1 #496)
1.2107 +#498 := (uf_3 #497)
1.2108 +#499 := (= #484 #498)
1.2109 #22 := 10::int
1.2110 -#507 := (>= #620 10::int)
1.2111 -#514 := (ite #507 #505 #531)
1.2112 +#500 := (>= #592 10::int)
1.2113 +#501 := (ite #500 #499 #485)
1.2114 #4 := (:var 0 T1)
1.2115 #21 := (uf_3 #4)
1.2116 #707 := (pattern #21)
1.2117 @@ -12333,12 +12554,12 @@
1.2118 #212 := [mp #207 #211]: #193
1.2119 #713 := [mp #212 #712]: #708
1.2120 #336 := (not #708)
1.2121 -#518 := (or #336 #514)
1.2122 -#528 := [quant-inst]: #518
1.2123 -#477 := [unit-resolution #528 #713]: #514
1.2124 -#529 := (not #507)
1.2125 -#498 := (<= #620 6::int)
1.2126 -#610 := (= #620 6::int)
1.2127 +#463 := (or #336 #501)
1.2128 +#464 := [quant-inst]: #463
1.2129 +#444 := [unit-resolution #464 #713]: #501
1.2130 +#473 := (not #500)
1.2131 +#453 := (<= #592 6::int)
1.2132 +#597 := (= #592 6::int)
1.2133 #10 := (:var 0 int)
1.2134 #12 := (uf_1 #10)
1.2135 #694 := (pattern #12)
1.2136 @@ -12396,79 +12617,79 @@
1.2137 #201 := [mp~ #99 #183]: #94
1.2138 #700 := [mp #201 #699]: #695
1.2139 #673 := (not #695)
1.2140 -#591 := (or #673 #610)
1.2141 -#526 := (>= 6::int 0::int)
1.2142 -#527 := (not #526)
1.2143 -#617 := (= 6::int #620)
1.2144 -#621 := (or #617 #527)
1.2145 -#592 := (or #673 #621)
1.2146 -#595 := (iff #592 #591)
1.2147 -#597 := (iff #591 #591)
1.2148 -#593 := [rewrite]: #597
1.2149 -#600 := (iff #621 #610)
1.2150 -#614 := (or #610 false)
1.2151 -#605 := (iff #614 #610)
1.2152 -#606 := [rewrite]: #605
1.2153 -#603 := (iff #621 #614)
1.2154 -#613 := (iff #527 false)
1.2155 +#576 := (or #673 #597)
1.2156 +#607 := (>= 6::int 0::int)
1.2157 +#591 := (not #607)
1.2158 +#594 := (= 6::int #592)
1.2159 +#595 := (or #594 #591)
1.2160 +#577 := (or #673 #595)
1.2161 +#579 := (iff #577 #576)
1.2162 +#581 := (iff #576 #576)
1.2163 +#582 := [rewrite]: #581
1.2164 +#574 := (iff #595 #597)
1.2165 +#586 := (or #597 false)
1.2166 +#571 := (iff #586 #597)
1.2167 +#573 := [rewrite]: #571
1.2168 +#590 := (iff #595 #586)
1.2169 +#588 := (iff #591 false)
1.2170 #1 := true
1.2171 #663 := (not true)
1.2172 #666 := (iff #663 false)
1.2173 #667 := [rewrite]: #666
1.2174 -#611 := (iff #527 #663)
1.2175 -#599 := (iff #526 true)
1.2176 -#601 := [rewrite]: #599
1.2177 -#612 := [monotonicity #601]: #611
1.2178 -#609 := [trans #612 #667]: #613
1.2179 -#608 := (iff #617 #610)
1.2180 -#602 := [rewrite]: #608
1.2181 -#604 := [monotonicity #602 #609]: #603
1.2182 -#607 := [trans #604 #606]: #600
1.2183 -#596 := [monotonicity #607]: #595
1.2184 -#598 := [trans #596 #593]: #595
1.2185 -#594 := [quant-inst]: #592
1.2186 -#584 := [mp #594 #598]: #591
1.2187 -#478 := [unit-resolution #584 #700]: #610
1.2188 -#453 := (not #610)
1.2189 -#454 := (or #453 #498)
1.2190 -#455 := [th-lemma]: #454
1.2191 -#456 := [unit-resolution #455 #478]: #498
1.2192 -#458 := (not #498)
1.2193 -#459 := (or #458 #529)
1.2194 -#460 := [th-lemma]: #459
1.2195 -#302 := [unit-resolution #460 #456]: #529
1.2196 -#508 := (not #514)
1.2197 -#490 := (or #508 #507 #531)
1.2198 -#491 := [def-axiom]: #490
1.2199 -#461 := [unit-resolution #491 #302 #477]: #531
1.2200 -#404 := [symm #461]: #403
1.2201 -#405 := (= #36 #476)
1.2202 +#585 := (iff #591 #663)
1.2203 +#598 := (iff #607 true)
1.2204 +#584 := [rewrite]: #598
1.2205 +#587 := [monotonicity #584]: #585
1.2206 +#589 := [trans #587 #667]: #588
1.2207 +#596 := (iff #594 #597)
1.2208 +#593 := [rewrite]: #596
1.2209 +#570 := [monotonicity #593 #589]: #590
1.2210 +#575 := [trans #570 #573]: #574
1.2211 +#580 := [monotonicity #575]: #579
1.2212 +#572 := [trans #580 #582]: #579
1.2213 +#578 := [quant-inst]: #577
1.2214 +#583 := [mp #578 #572]: #576
1.2215 +#448 := [unit-resolution #583 #700]: #597
1.2216 +#445 := (not #597)
1.2217 +#446 := (or #445 #453)
1.2218 +#442 := [th-lemma]: #446
1.2219 +#447 := [unit-resolution #442 #448]: #453
1.2220 +#437 := (not #453)
1.2221 +#427 := (or #437 #473)
1.2222 +#429 := [th-lemma]: #427
1.2223 +#430 := [unit-resolution #429 #447]: #473
1.2224 +#471 := (not #501)
1.2225 +#477 := (or #471 #500 #485)
1.2226 +#478 := [def-axiom]: #477
1.2227 +#433 := [unit-resolution #478 #430 #444]: #485
1.2228 +#373 := [symm #433]: #372
1.2229 +#374 := (= #36 #484)
1.2230 #649 := (uf_2 #35)
1.2231 -#582 := (+ -10::int #649)
1.2232 -#553 := (uf_1 #582)
1.2233 -#556 := (uf_3 #553)
1.2234 -#401 := (= #556 #476)
1.2235 -#417 := (= #553 #38)
1.2236 -#415 := (= #582 6::int)
1.2237 +#554 := (+ -10::int #649)
1.2238 +#549 := (uf_1 #554)
1.2239 +#545 := (uf_3 #549)
1.2240 +#381 := (= #545 #484)
1.2241 +#395 := (= #549 #38)
1.2242 +#394 := (= #554 6::int)
1.2243 #335 := (uf_2 #31)
1.2244 #647 := -1::int
1.2245 -#502 := (* -1::int #335)
1.2246 -#463 := (+ #33 #502)
1.2247 -#464 := (<= #463 0::int)
1.2248 -#486 := (= #33 #335)
1.2249 -#445 := (= #32 #31)
1.2250 -#574 := (= #31 #32)
1.2251 -#575 := (+ -10::int #335)
1.2252 -#576 := (uf_1 #575)
1.2253 -#577 := (uf_3 #576)
1.2254 -#578 := (= #32 #577)
1.2255 -#579 := (>= #335 10::int)
1.2256 -#580 := (ite #579 #578 #574)
1.2257 -#572 := (or #336 #580)
1.2258 -#583 := [quant-inst]: #572
1.2259 -#457 := [unit-resolution #583 #713]: #580
1.2260 -#562 := (not #579)
1.2261 -#554 := (<= #335 4::int)
1.2262 +#459 := (* -1::int #335)
1.2263 +#460 := (+ #33 #459)
1.2264 +#302 := (<= #460 0::int)
1.2265 +#458 := (= #33 #335)
1.2266 +#426 := (= #32 #31)
1.2267 +#555 := (= #31 #32)
1.2268 +#551 := (+ -10::int #335)
1.2269 +#552 := (uf_1 #551)
1.2270 +#553 := (uf_3 #552)
1.2271 +#556 := (= #32 #553)
1.2272 +#557 := (>= #335 10::int)
1.2273 +#558 := (ite #557 #556 #555)
1.2274 +#560 := (or #336 #558)
1.2275 +#533 := [quant-inst]: #560
1.2276 +#434 := [unit-resolution #533 #713]: #558
1.2277 +#535 := (not #557)
1.2278 +#531 := (<= #335 4::int)
1.2279 #324 := (= #335 4::int)
1.2280 #659 := (or #673 #324)
1.2281 #678 := (>= 4::int 0::int)
1.2282 @@ -12498,110 +12719,125 @@
1.2283 #277 := [trans #383 #385]: #382
1.2284 #367 := [quant-inst]: #660
1.2285 #655 := [mp #367 #277]: #659
1.2286 -#462 := [unit-resolution #655 #700]: #324
1.2287 -#441 := (not #324)
1.2288 -#444 := (or #441 #554)
1.2289 -#448 := [th-lemma]: #444
1.2290 -#450 := [unit-resolution #448 #462]: #554
1.2291 -#451 := (not #554)
1.2292 -#449 := (or #451 #562)
1.2293 -#452 := [th-lemma]: #449
1.2294 -#440 := [unit-resolution #452 #450]: #562
1.2295 -#561 := (not #580)
1.2296 -#566 := (or #561 #579 #574)
1.2297 -#567 := [def-axiom]: #566
1.2298 -#443 := [unit-resolution #567 #440 #457]: #574
1.2299 -#446 := [symm #443]: #445
1.2300 -#442 := [monotonicity #446]: #486
1.2301 -#447 := (not #486)
1.2302 -#437 := (or #447 #464)
1.2303 -#427 := [th-lemma]: #437
1.2304 -#429 := [unit-resolution #427 #442]: #464
1.2305 -#471 := (>= #463 0::int)
1.2306 -#430 := (or #447 #471)
1.2307 -#433 := [th-lemma]: #430
1.2308 -#434 := [unit-resolution #433 #442]: #471
1.2309 -#560 := (>= #335 4::int)
1.2310 -#438 := (or #441 #560)
1.2311 -#431 := [th-lemma]: #438
1.2312 -#439 := [unit-resolution #431 #462]: #560
1.2313 +#438 := [unit-resolution #655 #700]: #324
1.2314 +#431 := (not #324)
1.2315 +#439 := (or #431 #531)
1.2316 +#432 := [th-lemma]: #439
1.2317 +#435 := [unit-resolution #432 #438]: #531
1.2318 +#436 := (not #531)
1.2319 +#422 := (or #436 #535)
1.2320 +#424 := [th-lemma]: #422
1.2321 +#425 := [unit-resolution #424 #435]: #535
1.2322 +#534 := (not #558)
1.2323 +#540 := (or #534 #557 #555)
1.2324 +#541 := [def-axiom]: #540
1.2325 +#423 := [unit-resolution #541 #425 #434]: #555
1.2326 +#408 := [symm #423]: #426
1.2327 +#410 := [monotonicity #408]: #458
1.2328 +#411 := (not #458)
1.2329 +#412 := (or #411 #302)
1.2330 +#413 := [th-lemma]: #412
1.2331 +#414 := [unit-resolution #413 #410]: #302
1.2332 +#461 := (>= #460 0::int)
1.2333 +#415 := (or #411 #461)
1.2334 +#416 := [th-lemma]: #415
1.2335 +#417 := [unit-resolution #416 #410]: #461
1.2336 +#512 := (>= #335 4::int)
1.2337 +#418 := (or #431 #512)
1.2338 +#419 := [th-lemma]: #418
1.2339 +#420 := [unit-resolution #419 #438]: #512
1.2340 #651 := (* -1::int #649)
1.2341 #648 := (+ #34 #651)
1.2342 -#625 := (<= #648 0::int)
1.2343 +#521 := (<= #648 0::int)
1.2344 #652 := (= #648 0::int)
1.2345 -#643 := (>= #33 0::int)
1.2346 -#435 := (not #471)
1.2347 -#432 := (not #560)
1.2348 -#436 := (or #643 #432 #435)
1.2349 -#422 := [th-lemma]: #436
1.2350 -#424 := [unit-resolution #422 #439 #434]: #643
1.2351 -#644 := (not #643)
1.2352 -#489 := (or #644 #652)
1.2353 -#628 := (or #673 #644 #652)
1.2354 +#630 := (>= #33 0::int)
1.2355 +#421 := (not #461)
1.2356 +#409 := (not #512)
1.2357 +#398 := (or #630 #409 #421)
1.2358 +#400 := [th-lemma]: #398
1.2359 +#401 := [unit-resolution #400 #420 #417]: #630
1.2360 +#468 := (not #630)
1.2361 +#623 := (or #468 #652)
1.2362 +#509 := (or #673 #468 #652)
1.2363 #370 := (>= #34 0::int)
1.2364 #371 := (not #370)
1.2365 #650 := (= #34 #649)
1.2366 #364 := (or #650 #371)
1.2367 -#629 := (or #673 #364)
1.2368 -#469 := (iff #629 #628)
1.2369 -#636 := (or #673 #489)
1.2370 -#466 := (iff #636 #628)
1.2371 -#468 := [rewrite]: #466
1.2372 -#630 := (iff #629 #636)
1.2373 -#633 := (iff #364 #489)
1.2374 -#646 := (or #652 #644)
1.2375 -#631 := (iff #646 #489)
1.2376 -#632 := [rewrite]: #631
1.2377 -#487 := (iff #364 #646)
1.2378 -#645 := (iff #371 #644)
1.2379 -#638 := (iff #370 #643)
1.2380 -#639 := [rewrite]: #638
1.2381 -#640 := [monotonicity #639]: #645
1.2382 +#510 := (or #673 #364)
1.2383 +#619 := (iff #510 #509)
1.2384 +#470 := (or #673 #623)
1.2385 +#615 := (iff #470 #509)
1.2386 +#616 := [rewrite]: #615
1.2387 +#618 := (iff #510 #470)
1.2388 +#624 := (iff #364 #623)
1.2389 +#643 := 1::int
1.2390 +#638 := (* 1::int #33)
1.2391 +#639 := (>= #638 0::int)
1.2392 +#640 := (not #639)
1.2393 +#632 := (or #640 #652)
1.2394 +#625 := (iff #632 #623)
1.2395 +#469 := (iff #640 #468)
1.2396 +#637 := (iff #639 #630)
1.2397 +#635 := (= #638 #33)
1.2398 +#636 := [rewrite]: #635
1.2399 +#466 := [monotonicity #636]: #637
1.2400 +#622 := [monotonicity #466]: #469
1.2401 +#626 := [monotonicity #622]: #625
1.2402 +#628 := (iff #364 #632)
1.2403 +#488 := (or #652 #640)
1.2404 +#633 := (iff #488 #632)
1.2405 +#634 := [rewrite]: #633
1.2406 +#489 := (iff #364 #488)
1.2407 +#646 := (iff #371 #640)
1.2408 +#644 := (iff #370 #639)
1.2409 +#645 := [rewrite]: #644
1.2410 +#487 := [monotonicity #645]: #646
1.2411 #641 := (iff #650 #652)
1.2412 #642 := [rewrite]: #641
1.2413 -#488 := [monotonicity #642 #640]: #487
1.2414 -#634 := [trans #488 #632]: #633
1.2415 -#637 := [monotonicity #634]: #630
1.2416 -#622 := [trans #637 #468]: #469
1.2417 -#635 := [quant-inst]: #629
1.2418 -#623 := [mp #635 #622]: #628
1.2419 -#425 := [unit-resolution #623 #700]: #489
1.2420 -#423 := [unit-resolution #425 #424]: #652
1.2421 -#426 := (not #652)
1.2422 -#408 := (or #426 #625)
1.2423 -#410 := [th-lemma]: #408
1.2424 -#411 := [unit-resolution #410 #423]: #625
1.2425 -#626 := (>= #648 0::int)
1.2426 -#412 := (or #426 #626)
1.2427 -#413 := [th-lemma]: #412
1.2428 -#414 := [unit-resolution #413 #423]: #626
1.2429 -#416 := [th-lemma #414 #411 #439 #450 #434 #429]: #415
1.2430 -#418 := [monotonicity #416]: #417
1.2431 -#402 := [monotonicity #418]: #401
1.2432 -#557 := (= #36 #556)
1.2433 -#581 := (= #35 #36)
1.2434 -#558 := (>= #649 10::int)
1.2435 -#559 := (ite #558 #557 #581)
1.2436 -#533 := (or #336 #559)
1.2437 -#534 := [quant-inst]: #533
1.2438 -#419 := [unit-resolution #534 #713]: #559
1.2439 -#420 := (not #625)
1.2440 -#409 := (or #558 #420 #432 #435)
1.2441 -#421 := [th-lemma]: #409
1.2442 -#398 := [unit-resolution #421 #411 #439 #434]: #558
1.2443 -#428 := (not #558)
1.2444 -#535 := (not #559)
1.2445 -#539 := (or #535 #428 #557)
1.2446 -#540 := [def-axiom]: #539
1.2447 -#400 := [unit-resolution #540 #398 #419]: #557
1.2448 -#406 := [trans #400 #402]: #405
1.2449 -#399 := [trans #406 #404]: #39
1.2450 +#631 := [monotonicity #642 #487]: #489
1.2451 +#629 := [trans #631 #634]: #628
1.2452 +#627 := [trans #629 #626]: #624
1.2453 +#520 := [monotonicity #627]: #618
1.2454 +#504 := [trans #520 #616]: #619
1.2455 +#511 := [quant-inst]: #510
1.2456 +#519 := [mp #511 #504]: #509
1.2457 +#402 := [unit-resolution #519 #700]: #623
1.2458 +#403 := [unit-resolution #402 #401]: #652
1.2459 +#404 := (not #652)
1.2460 +#405 := (or #404 #521)
1.2461 +#406 := [th-lemma]: #405
1.2462 +#399 := [unit-resolution #406 #403]: #521
1.2463 +#522 := (>= #648 0::int)
1.2464 +#407 := (or #404 #522)
1.2465 +#392 := [th-lemma]: #407
1.2466 +#393 := [unit-resolution #392 #403]: #522
1.2467 +#396 := [th-lemma #393 #399 #420 #435 #417 #414]: #394
1.2468 +#397 := [monotonicity #396]: #395
1.2469 +#391 := [monotonicity #397]: #381
1.2470 +#550 := (= #36 #545)
1.2471 +#559 := (= #35 #36)
1.2472 +#530 := (>= #649 10::int)
1.2473 +#476 := (ite #530 #550 #559)
1.2474 +#536 := (or #336 #476)
1.2475 +#537 := [quant-inst]: #536
1.2476 +#386 := [unit-resolution #537 #713]: #476
1.2477 +#387 := (not #521)
1.2478 +#388 := (or #530 #387 #409 #421)
1.2479 +#380 := [th-lemma]: #388
1.2480 +#389 := [unit-resolution #380 #399 #420 #417]: #530
1.2481 +#538 := (not #530)
1.2482 +#532 := (not #476)
1.2483 +#506 := (or #532 #538 #550)
1.2484 +#513 := [def-axiom]: #506
1.2485 +#390 := [unit-resolution #513 #389 #386]: #550
1.2486 +#365 := [trans #390 #391]: #374
1.2487 +#375 := [trans #365 #373]: #39
1.2488 #40 := (not #39)
1.2489 #182 := [asserted]: #40
1.2490 -[unit-resolution #182 #399]: false
1.2491 -unsat
1.2492 -
1.2493 -/fwo5o8vhLVHyS4oYEs4QA 10833
1.2494 +[unit-resolution #182 #375]: false
1.2495 +unsat
1.2496 +
1.2497 +/fwo5o8vhLVHyS4oYEs4QA 10902
1.2498 #2 := false
1.2499 #22 := 0::int
1.2500 #8 := 2::int
1.2501 @@ -12677,18 +12913,18 @@
1.2502 #604 := [trans #593 #597]: #562
1.2503 #603 := [quant-inst]: #596
1.2504 #606 := [mp #603 #604]: #628
1.2505 -#528 := [unit-resolution #606 #817]: #566
1.2506 -#521 := (not #566)
1.2507 -#464 := (or #521 #608)
1.2508 -#456 := [th-lemma]: #464
1.2509 -#465 := [unit-resolution #456 #528]: #608
1.2510 +#516 := [unit-resolution #606 #817]: #566
1.2511 +#498 := (not #566)
1.2512 +#432 := (or #498 #608)
1.2513 +#411 := [th-lemma]: #432
1.2514 +#413 := [unit-resolution #411 #516]: #608
1.2515 decl uf_10 :: int
1.2516 #52 := uf_10
1.2517 #57 := (mod uf_10 2::int)
1.2518 #243 := (* -1::int #57)
1.2519 #244 := (+ #56 #243)
1.2520 #447 := (>= #244 0::int)
1.2521 -#387 := (not #447)
1.2522 +#372 := (not #447)
1.2523 #245 := (= #244 0::int)
1.2524 #248 := (not #245)
1.2525 #218 := (* -1::int #55)
1.2526 @@ -12708,9 +12944,9 @@
1.2527 #662 := (not #672)
1.2528 #1 := true
1.2529 #81 := [true-axiom]: true
1.2530 -#520 := (or false #662)
1.2531 -#523 := [th-lemma]: #520
1.2532 -#524 := [unit-resolution #523 #81]: #662
1.2533 +#514 := (or false #662)
1.2534 +#515 := [th-lemma]: #514
1.2535 +#513 := [unit-resolution #515 #81]: #662
1.2536 #701 := (* -1::int #613)
1.2537 #204 := -2::int
1.2538 #691 := (* -2::int #222)
1.2539 @@ -12723,82 +12959,58 @@
1.2540 #546 := [th-lemma]: #545
1.2541 #548 := [unit-resolution #546 #81]: #692
1.2542 #549 := (not #692)
1.2543 -#497 := (or #549 #694)
1.2544 -#482 := [th-lemma]: #497
1.2545 -#483 := [unit-resolution #482 #548]: #694
1.2546 +#482 := (or #549 #694)
1.2547 +#483 := [th-lemma]: #482
1.2548 +#484 := [unit-resolution #483 #548]: #694
1.2549 #536 := (not #448)
1.2550 -#395 := [hypothesis]: #536
1.2551 +#382 := [hypothesis]: #536
1.2552 #555 := (* -1::int uf_10)
1.2553 #573 := (+ #51 #555)
1.2554 #543 := (<= #573 0::int)
1.2555 #53 := (= #51 uf_10)
1.2556 #256 := (not #253)
1.2557 #259 := (or #248 #256)
1.2558 -#502 := 1::int
1.2559 #731 := (div uf_10 2::int)
1.2560 -#515 := (* -1::int #731)
1.2561 -#513 := (+ #640 #515)
1.2562 +#723 := (* -2::int #731)
1.2563 +#521 := (* -2::int #624)
1.2564 +#529 := (+ #521 #723)
1.2565 #618 := (div #51 2::int)
1.2566 -#514 := (* -1::int #618)
1.2567 -#516 := (+ #514 #513)
1.2568 -#498 := (+ #243 #516)
1.2569 -#500 := (+ #56 #498)
1.2570 -#501 := (+ uf_10 #500)
1.2571 -#503 := (>= #501 1::int)
1.2572 -#486 := (not #503)
1.2573 -#361 := (<= #244 0::int)
1.2574 +#583 := (* -2::int #618)
1.2575 +#522 := (+ #583 #529)
1.2576 +#528 := (* -2::int #57)
1.2577 +#525 := (+ #528 #522)
1.2578 +#524 := (* 2::int #56)
1.2579 +#526 := (+ #524 #525)
1.2580 +#523 := (* 2::int uf_10)
1.2581 +#512 := (+ #523 #526)
1.2582 +#520 := (>= #512 2::int)
1.2583 #453 := (not #259)
1.2584 -#517 := [hypothesis]: #453
1.2585 +#519 := [hypothesis]: #453
1.2586 #440 := (or #259 #245)
1.2587 #451 := [def-axiom]: #440
1.2588 -#519 := [unit-resolution #451 #517]: #245
1.2589 -#478 := (or #248 #361)
1.2590 -#470 := [th-lemma]: #478
1.2591 -#479 := [unit-resolution #470 #519]: #361
1.2592 -#449 := (>= #252 0::int)
1.2593 +#470 := [unit-resolution #451 #519]: #245
1.2594 +#465 := (or #248 #447)
1.2595 +#466 := [th-lemma]: #465
1.2596 +#457 := [unit-resolution #466 #470]: #447
1.2597 +#544 := (>= #573 0::int)
1.2598 +#441 := (not #544)
1.2599 #452 := (or #259 #253)
1.2600 #380 := [def-axiom]: #452
1.2601 -#480 := [unit-resolution #380 #517]: #253
1.2602 -#471 := (or #256 #449)
1.2603 -#481 := [th-lemma]: #471
1.2604 -#462 := [unit-resolution #481 #480]: #449
1.2605 -#487 := (not #361)
1.2606 -#485 := (not #449)
1.2607 -#476 := (or #486 #485 #487)
1.2608 -#607 := (<= #620 0::int)
1.2609 -#529 := (or #521 #607)
1.2610 -#522 := [th-lemma]: #529
1.2611 -#525 := [unit-resolution #522 #528]: #607
1.2612 -#723 := (* -2::int #731)
1.2613 -#724 := (+ #243 #723)
1.2614 -#718 := (+ uf_10 #724)
1.2615 -#720 := (<= #718 0::int)
1.2616 -#722 := (= #718 0::int)
1.2617 -#526 := (or false #722)
1.2618 -#512 := [th-lemma]: #526
1.2619 -#504 := [unit-resolution #512 #81]: #722
1.2620 -#505 := (not #722)
1.2621 -#506 := (or #505 #720)
1.2622 -#507 := [th-lemma]: #506
1.2623 -#508 := [unit-resolution #507 #504]: #720
1.2624 -#509 := [hypothesis]: #361
1.2625 -#583 := (* -2::int #618)
1.2626 -#584 := (+ #583 #640)
1.2627 -#585 := (+ #51 #584)
1.2628 -#587 := (<= #585 0::int)
1.2629 -#582 := (= #585 0::int)
1.2630 -#510 := (or false #582)
1.2631 -#499 := [th-lemma]: #510
1.2632 -#511 := [unit-resolution #499 #81]: #582
1.2633 -#488 := (not #582)
1.2634 -#490 := (or #488 #587)
1.2635 -#491 := [th-lemma]: #490
1.2636 -#492 := [unit-resolution #491 #511]: #587
1.2637 -#493 := [hypothesis]: #503
1.2638 +#481 := [unit-resolution #380 #519]: #253
1.2639 +#467 := (or #256 #448)
1.2640 +#434 := [th-lemma]: #467
1.2641 +#436 := [unit-resolution #434 #481]: #448
1.2642 +#532 := (or #543 #536)
1.2643 +#695 := (>= #699 0::int)
1.2644 +#550 := (or #549 #695)
1.2645 +#393 := [th-lemma]: #550
1.2646 +#551 := [unit-resolution #393 #548]: #695
1.2647 +#547 := (not #543)
1.2648 +#552 := [hypothesis]: #547
1.2649 #649 := (* -2::int #60)
1.2650 #644 := (+ #218 #649)
1.2651 #650 := (+ #51 #644)
1.2652 -#636 := (>= #650 0::int)
1.2653 +#631 := (<= #650 0::int)
1.2654 #623 := (= #650 0::int)
1.2655 #43 := (uf_7 uf_2 #35)
1.2656 #44 := (uf_6 #34 #43)
1.2657 @@ -12859,33 +13071,6 @@
1.2658 #630 := [quant-inst]: #629
1.2659 #531 := [unit-resolution #630 #824]: #623
1.2660 #534 := (not #623)
1.2661 -#494 := (or #534 #636)
1.2662 -#495 := [th-lemma]: #494
1.2663 -#496 := [unit-resolution #495 #531]: #636
1.2664 -#489 := [hypothesis]: #449
1.2665 -#484 := [th-lemma #483 #489 #496 #493 #492 #509 #508 #525 #524]: false
1.2666 -#477 := [lemma #484]: #476
1.2667 -#463 := [unit-resolution #477 #462 #479]: #486
1.2668 -#727 := (>= #718 0::int)
1.2669 -#466 := (or #505 #727)
1.2670 -#457 := [th-lemma]: #466
1.2671 -#467 := [unit-resolution #457 #504]: #727
1.2672 -#434 := (or #248 #447)
1.2673 -#436 := [th-lemma]: #434
1.2674 -#437 := [unit-resolution #436 #519]: #447
1.2675 -#544 := (>= #573 0::int)
1.2676 -#445 := (not #544)
1.2677 -#428 := (or #256 #448)
1.2678 -#441 := [th-lemma]: #428
1.2679 -#442 := [unit-resolution #441 #480]: #448
1.2680 -#532 := (or #543 #536)
1.2681 -#695 := (>= #699 0::int)
1.2682 -#550 := (or #549 #695)
1.2683 -#393 := [th-lemma]: #550
1.2684 -#551 := [unit-resolution #393 #548]: #695
1.2685 -#547 := (not #543)
1.2686 -#552 := [hypothesis]: #547
1.2687 -#631 := (<= #650 0::int)
1.2688 #538 := (or #534 #631)
1.2689 #540 := [th-lemma]: #538
1.2690 #541 := [unit-resolution #540 #531]: #631
1.2691 @@ -12896,8 +13081,8 @@
1.2692 #533 := [unit-resolution #530 #81]: #666
1.2693 #535 := [th-lemma #533 #539 #541 #552 #551]: false
1.2694 #537 := [lemma #535]: #532
1.2695 -#443 := [unit-resolution #537 #442]: #543
1.2696 -#429 := (or #547 #445)
1.2697 +#437 := [unit-resolution #537 #436]: #543
1.2698 +#444 := (or #547 #441)
1.2699 #764 := (not #53)
1.2700 #771 := (or #764 #259)
1.2701 #262 := (iff #53 #259)
1.2702 @@ -12950,65 +13135,118 @@
1.2703 #438 := (or #764 #259 #433)
1.2704 #439 := [def-axiom]: #438
1.2705 #772 := [unit-resolution #439 #267]: #771
1.2706 -#444 := [unit-resolution #772 #517]: #764
1.2707 -#435 := (or #53 #547 #445)
1.2708 -#446 := [th-lemma]: #435
1.2709 -#431 := [unit-resolution #446 #444]: #429
1.2710 -#432 := [unit-resolution #431 #443]: #445
1.2711 +#428 := [unit-resolution #772 #519]: #764
1.2712 +#442 := (or #53 #547 #441)
1.2713 +#443 := [th-lemma]: #442
1.2714 +#445 := [unit-resolution #443 #428]: #444
1.2715 +#435 := [unit-resolution #445 #437]: #441
1.2716 +#584 := (+ #583 #640)
1.2717 +#585 := (+ #51 #584)
1.2718 #588 := (>= #585 0::int)
1.2719 -#411 := (or #488 #588)
1.2720 -#413 := [th-lemma]: #411
1.2721 -#418 := [unit-resolution #413 #511]: #588
1.2722 -#419 := [th-lemma #418 #432 #437 #467 #465 #463]: false
1.2723 -#420 := [lemma #419]: #259
1.2724 +#582 := (= #585 0::int)
1.2725 +#499 := (or false #582)
1.2726 +#511 := [th-lemma]: #499
1.2727 +#488 := [unit-resolution #511 #81]: #582
1.2728 +#490 := (not #582)
1.2729 +#446 := (or #490 #588)
1.2730 +#429 := [th-lemma]: #446
1.2731 +#431 := [unit-resolution #429 #488]: #588
1.2732 +#724 := (+ #243 #723)
1.2733 +#718 := (+ uf_10 #724)
1.2734 +#727 := (>= #718 0::int)
1.2735 +#722 := (= #718 0::int)
1.2736 +#503 := (or false #722)
1.2737 +#504 := [th-lemma]: #503
1.2738 +#505 := [unit-resolution #504 #81]: #722
1.2739 +#506 := (not #722)
1.2740 +#418 := (or #506 #727)
1.2741 +#419 := [th-lemma]: #418
1.2742 +#420 := [unit-resolution #419 #505]: #727
1.2743 +#421 := [th-lemma #420 #413 #431 #435 #457]: #520
1.2744 +#485 := (not #520)
1.2745 +#361 := (<= #244 0::int)
1.2746 +#479 := (or #248 #361)
1.2747 +#480 := [th-lemma]: #479
1.2748 +#471 := [unit-resolution #480 #470]: #361
1.2749 +#449 := (>= #252 0::int)
1.2750 +#462 := (or #256 #449)
1.2751 +#463 := [th-lemma]: #462
1.2752 +#464 := [unit-resolution #463 #481]: #449
1.2753 +#476 := (not #361)
1.2754 +#487 := (not #449)
1.2755 +#477 := (or #485 #487 #476)
1.2756 +#607 := (<= #620 0::int)
1.2757 +#500 := (or #498 #607)
1.2758 +#501 := [th-lemma]: #500
1.2759 +#502 := [unit-resolution #501 #516]: #607
1.2760 +#720 := (<= #718 0::int)
1.2761 +#507 := (or #506 #720)
1.2762 +#508 := [th-lemma]: #507
1.2763 +#509 := [unit-resolution #508 #505]: #720
1.2764 +#510 := [hypothesis]: #361
1.2765 +#587 := (<= #585 0::int)
1.2766 +#491 := (or #490 #587)
1.2767 +#492 := [th-lemma]: #491
1.2768 +#493 := [unit-resolution #492 #488]: #587
1.2769 +#494 := [hypothesis]: #520
1.2770 +#636 := (>= #650 0::int)
1.2771 +#495 := (or #534 #636)
1.2772 +#496 := [th-lemma]: #495
1.2773 +#489 := [unit-resolution #496 #531]: #636
1.2774 +#497 := [hypothesis]: #449
1.2775 +#486 := [th-lemma #484 #497 #489 #494 #493 #510 #509 #502 #513]: false
1.2776 +#478 := [lemma #486]: #477
1.2777 +#456 := [unit-resolution #478 #464 #471]: #485
1.2778 +#422 := [unit-resolution #456 #421]: false
1.2779 +#423 := [lemma #422]: #259
1.2780 #427 := (or #53 #453)
1.2781 #768 := (or #53 #453 #433)
1.2782 #770 := [def-axiom]: #768
1.2783 #557 := [unit-resolution #770 #267]: #427
1.2784 -#406 := [unit-resolution #557 #420]: #53
1.2785 -#377 := (or #764 #543)
1.2786 -#381 := [th-lemma]: #377
1.2787 -#382 := [unit-resolution #381 #406]: #543
1.2788 -#385 := [th-lemma #496 #382 #395 #483 #524]: false
1.2789 -#386 := [lemma #385]: #448
1.2790 -#390 := (or #253 #536)
1.2791 -#408 := [hypothesis]: #485
1.2792 -#409 := (or #764 #544)
1.2793 -#397 := [th-lemma]: #409
1.2794 -#399 := [unit-resolution #397 #406]: #544
1.2795 -#400 := [th-lemma #399 #408 #533 #551 #541]: false
1.2796 -#403 := [lemma #400]: #449
1.2797 -#392 := (or #253 #536 #485)
1.2798 -#394 := [th-lemma]: #392
1.2799 -#657 := [unit-resolution #394 #403]: #390
1.2800 -#658 := [unit-resolution #657 #386]: #253
1.2801 +#399 := [unit-resolution #557 #423]: #53
1.2802 +#385 := (or #764 #543)
1.2803 +#386 := [th-lemma]: #385
1.2804 +#387 := [unit-resolution #386 #399]: #543
1.2805 +#379 := [th-lemma #489 #387 #382 #484 #513]: false
1.2806 +#388 := [lemma #379]: #448
1.2807 +#381 := (or #253 #536)
1.2808 +#397 := [hypothesis]: #487
1.2809 +#400 := (or #764 #544)
1.2810 +#403 := [th-lemma]: #400
1.2811 +#398 := [unit-resolution #403 #399]: #544
1.2812 +#404 := [th-lemma #398 #397 #533 #551 #541]: false
1.2813 +#378 := [lemma #404]: #449
1.2814 +#395 := (or #253 #536 #487)
1.2815 +#377 := [th-lemma]: #395
1.2816 +#658 := [unit-resolution #377 #378]: #381
1.2817 +#653 := [unit-resolution #658 #388]: #253
1.2818 #450 := (or #453 #248 #256)
1.2819 #454 := [def-axiom]: #450
1.2820 -#762 := [unit-resolution #454 #420]: #259
1.2821 -#664 := [unit-resolution #762 #658]: #248
1.2822 -#372 := (or #245 #387)
1.2823 -#560 := (+ #57 #640)
1.2824 -#610 := (>= #560 0::int)
1.2825 -#742 := (= #57 #624)
1.2826 -#424 := (= #624 #57)
1.2827 -#405 := [monotonicity #406]: #424
1.2828 -#407 := [symm #405]: #742
1.2829 -#705 := (not #742)
1.2830 -#706 := (or #705 #610)
1.2831 -#568 := [th-lemma]: #706
1.2832 -#569 := [unit-resolution #568 #407]: #610
1.2833 -#398 := [hypothesis]: #487
1.2834 -#404 := [th-lemma #525 #398 #569]: false
1.2835 -#378 := [lemma #404]: #361
1.2836 -#379 := (or #245 #487 #387)
1.2837 -#388 := [th-lemma]: #379
1.2838 -#369 := [unit-resolution #388 #378]: #372
1.2839 -#370 := [unit-resolution #369 #664]: #387
1.2840 -#708 := (<= #560 0::int)
1.2841 -#373 := (or #705 #708)
1.2842 -#374 := [th-lemma]: #373
1.2843 -#375 := [unit-resolution #374 #407]: #708
1.2844 -[th-lemma #375 #370 #465]: false
1.2845 +#664 := [unit-resolution #454 #423]: #259
1.2846 +#665 := [unit-resolution #664 #653]: #248
1.2847 +#373 := (or #245 #372)
1.2848 +#708 := (+ #57 #640)
1.2849 +#705 := (>= #708 0::int)
1.2850 +#560 := (= #57 #624)
1.2851 +#408 := (= #624 #57)
1.2852 +#406 := [monotonicity #399]: #408
1.2853 +#409 := [symm #406]: #560
1.2854 +#706 := (not #560)
1.2855 +#655 := (or #706 #705)
1.2856 +#569 := [th-lemma]: #655
1.2857 +#570 := [unit-resolution #569 #409]: #705
1.2858 +#383 := [hypothesis]: #476
1.2859 +#384 := [th-lemma #502 #383 #570]: false
1.2860 +#389 := [lemma #384]: #361
1.2861 +#369 := (or #245 #476 #372)
1.2862 +#370 := [th-lemma]: #369
1.2863 +#374 := [unit-resolution #370 #389]: #373
1.2864 +#375 := [unit-resolution #374 #665]: #372
1.2865 +#610 := (<= #708 0::int)
1.2866 +#371 := (or #706 #610)
1.2867 +#376 := [th-lemma]: #371
1.2868 +#363 := [unit-resolution #376 #409]: #610
1.2869 +[th-lemma #363 #375 #413]: false
1.2870 unsat
1.2871
1.2872 s8LL71+1HTN+eIuEYeKhUw 1251
2.1 --- a/src/HOL/SMT/Examples/SMT_Examples.thy Mon Feb 08 17:12:38 2010 +0100
2.2 +++ b/src/HOL/SMT/Examples/SMT_Examples.thy Mon Feb 08 17:12:40 2010 +0100
2.3 @@ -17,7 +17,7 @@
2.4 the following option is set to "false":
2.5 *}
2.6
2.7 -declare [[smt_record=false]]
2.8 +declare [[smt_record=false]]
2.9
2.10
2.11