1.1 --- a/src/HOL/SMT/Examples/SMT_Examples.certs Tue Feb 16 16:20:34 2010 +0100
1.2 +++ b/src/HOL/SMT/Examples/SMT_Examples.certs Tue Feb 16 16:20:46 2010 +0100
1.3 @@ -1,4 +1,4 @@
1.4 -yknPpoG47N1CXnUaEL9RvQ 8 0
1.5 +Fg1W6egjwo9zhhAmUXOW+w 8 0
1.6 #2 := false
1.7 #1 := true
1.8 #4 := (not true)
1.9 @@ -7,7 +7,7 @@
1.10 #20 := [asserted]: #4
1.11 [mp #20 #22]: false
1.12 unsat
1.13 -ymB2ZiCSl9aUjMXP3tIpZA 19 0
1.14 +2+cndY9nzS72l7VvBCGRAw 19 0
1.15 #2 := false
1.16 decl up_1 :: bool
1.17 #4 := up_1
1.18 @@ -27,7 +27,7 @@
1.19 #23 := [asserted]: #7
1.20 [mp #23 #32]: false
1.21 unsat
1.22 -XC3j0tGm4Y5klDm8sMkzVg 25 0
1.23 +0vJQrobUDcQ9PkGJO8aM8g 25 0
1.24 #2 := false
1.25 decl up_1 :: bool
1.26 #4 := up_1
1.27 @@ -53,7 +53,7 @@
1.28 #23 := [asserted]: #7
1.29 [mp #23 #38]: false
1.30 unsat
1.31 -y5d/Jtt47lXm/wUEvH5fHw 38 0
1.32 +AGGnpwEv208Vqxly7wTWHA 38 0
1.33 #2 := false
1.34 decl up_2 :: bool
1.35 #5 := up_2
1.36 @@ -92,9 +92,9 @@
1.37 #30 := [and-elim #31]: #6
1.38 [mp #30 #52]: false
1.39 unsat
1.40 -mDaukNkyA4glYbkfEOtcAw 1 0
1.41 -unsat
1.42 -TmB9YjKjdtDMIh0j9rMVPw 71 0
1.43 +wakXeIy1uoPgglzOQGFhJQ 1 0
1.44 +unsat
1.45 +cpSlDe0l7plVktRNxGU5dA 71 0
1.46 #2 := false
1.47 decl up_1 :: bool
1.48 #4 := up_1
1.49 @@ -166,7 +166,7 @@
1.50 #31 := [asserted]: #15
1.51 [mp #31 #82]: false
1.52 unsat
1.53 -olufSxMlwMAAqyArYWPVOA 57 0
1.54 +pg19mjJfV75T2QDrgWd4JA 57 0
1.55 #2 := false
1.56 decl up_1 :: bool
1.57 #4 := up_1
1.58 @@ -224,7 +224,7 @@
1.59 #30 := [asserted]: #14
1.60 [mp #30 #70]: false
1.61 unsat
1.62 -agKJ550QwZ1mvlK8gw+tjQ 194 0
1.63 +Mj1B8X1MaN7xU/W4Kz3FoQ 194 0
1.64 #2 := false
1.65 decl up_1 :: bool
1.66 #4 := up_1
1.67 @@ -419,7 +419,7 @@
1.68 #237 := [mp #83 #236]: #75
1.69 [mp #237 #247]: false
1.70 unsat
1.71 -+R/oj2I+uFZAw/Eu+3ULdw 52 0
1.72 +JkhYJB8FDavTZkizO1/9IA 52 0
1.73 #2 := false
1.74 decl uf_1 :: (-> T1 T1 T1)
1.75 decl uf_2 :: T1
1.76 @@ -472,7 +472,7 @@
1.77 #113 := [quant-inst]: #199
1.78 [unit-resolution #113 #536 #49]: false
1.79 unsat
1.80 -c67Ar5f1aFkzAZ2wYy62Wg 1667 0
1.81 +0ZdSZH2DbtjHNTyrDkZmXg 1667 0
1.82 #2 := false
1.83 decl up_54 :: bool
1.84 #126 := up_54
1.85 @@ -2140,7 +2140,7 @@
1.86 #2371 := [unit-resolution #891 #2369]: #166
1.87 [unit-resolution #2159 #2371 #2370 #2358 #2357]: false
1.88 unsat
1.89 -NdJwa8pysYWhn57eCXiqFA 78 0
1.90 +R3pmBDBlU9XdUrxJXhj7nA 78 0
1.91 #2 := false
1.92 decl up_1 :: (-> int bool)
1.93 decl ?x1!0 :: int
1.94 @@ -2219,7 +2219,7 @@
1.95 #82 := [and-elim #81]: #55
1.96 [unit-resolution #82 #95]: false
1.97 unsat
1.98 -dWWXDEA5bUZjEafLPXbSkA 135 0
1.99 +IBRj/loev6P6r0J+HOit6A 135 0
1.100 #2 := false
1.101 decl up_1 :: (-> T1 T2 bool)
1.102 #5 := (:var 0 T2)
1.103 @@ -2355,7 +2355,7 @@
1.104 #176 := [quant-inst]: #538
1.105 [unit-resolution #176 #252 #535]: false
1.106 unsat
1.107 -iGZ7b2jaCnn82lPL6oIDZA 135 2
1.108 +72504KVBixGB/87pOYiU/A 135 2
1.109 #2 := false
1.110 decl up_1 :: (-> T1 T2 bool)
1.111 #5 := (:var 0 T2)
1.112 @@ -2491,9 +2491,9 @@
1.113 #235 := [quant-inst]: #597
1.114 [unit-resolution #235 #311 #594]: false
1.115 unsat
1.116 -WARNING: failed to find a pattern for quantifier (quantifier id: k!11)
1.117 +WARNING: failed to find a pattern for quantifier (quantifier id: k!12)
1.118
1.119 -eTjcfu6S5eyz+xNJ7SVluw 56 0
1.120 +RaQLz4GxtUICnOD5WoYnzQ 56 0
1.121 #2 := false
1.122 decl up_1 :: (-> T1 bool)
1.123 decl uf_2 :: T1
1.124 @@ -2550,7 +2550,7 @@
1.125 #120 := [quant-inst]: #206
1.126 [unit-resolution #120 #542 #41]: false
1.127 unsat
1.128 -anG1bKU/YVTHEmc1Eh/ZXw 17 0
1.129 +NPQIgVPhSpgSLeS+u/EatQ 17 0
1.130 #2 := false
1.131 #4 := 3::int
1.132 #5 := (= 3::int 3::int)
1.133 @@ -2568,7 +2568,7 @@
1.134 #22 := [asserted]: #6
1.135 [mp #22 #31]: false
1.136 unsat
1.137 -lHpRCTa744ODgmii2zARAw 17 0
1.138 +Lc9NwVtwY2Wo0G7UbFD1oA 17 0
1.139 #2 := false
1.140 #4 := 3::real
1.141 #5 := (= 3::real 3::real)
1.142 @@ -2586,7 +2586,7 @@
1.143 #22 := [asserted]: #6
1.144 [mp #22 #31]: false
1.145 unsat
1.146 -AinXomcY4W1L/t0ZtkDhBg 26 0
1.147 +pYVrUflpYrrZEWALJDnvPw 26 0
1.148 #2 := false
1.149 #7 := 4::int
1.150 #5 := 1::int
1.151 @@ -2613,7 +2613,7 @@
1.152 #25 := [asserted]: #9
1.153 [mp #25 #40]: false
1.154 unsat
1.155 -WxMdOusjxqQwBPorpXBkFQ 41 0
1.156 +FIqzVlbN8RT0iWarmBEpjw 41 0
1.157 #2 := false
1.158 decl uf_1 :: int
1.159 #4 := uf_1
1.160 @@ -2655,7 +2655,7 @@
1.161 #28 := [asserted]: #12
1.162 [mp #28 #52]: false
1.163 unsat
1.164 -K7g37p4yZoVyQcabYS4I2w 35 0
1.165 +HWVNtxMa8xktQsg8pHG+1w 35 0
1.166 #2 := false
1.167 #5 := 3::int
1.168 #6 := 8::int
1.169 @@ -2691,7 +2691,7 @@
1.170 #26 := [asserted]: #10
1.171 [mp #26 #51]: false
1.172 unsat
1.173 -eCmVy21SUmWImXZDJNOfzA 250 0
1.174 +M71YYpEc8u/aEIH3MOQrcg 250 0
1.175 #2 := false
1.176 #7 := 0::real
1.177 decl uf_2 :: real
1.178 @@ -2942,7 +2942,7 @@
1.179 #294 := [unit-resolution #190 #293]: #188
1.180 [th-lemma #280 #294]: false
1.181 unsat
1.182 -eBRZKSXriNPK3BNu3AWMmQ 124 0
1.183 +G00bTqBjtW66EmwIZbXbOg 124 0
1.184 #2 := false
1.185 decl uf_1 :: (-> T1 T2)
1.186 decl uf_3 :: T1
1.187 @@ -3067,7 +3067,7 @@
1.188 #34 := [asserted]: #11
1.189 [unit-resolution #34 #536]: false
1.190 unsat
1.191 -CjDkjvq1e9i+SJ3L9ESARg 54 0
1.192 +6QdzkSy/RtEjUu+wUKIKqA 54 0
1.193 #2 := false
1.194 #9 := 1::int
1.195 decl uf_1 :: int
1.196 @@ -3122,7 +3122,7 @@
1.197 #28 := [asserted]: #12
1.198 [mp #28 #67]: false
1.199 unsat
1.200 -nonk4MmmwlBqL8YtiJY/Qw 63 0
1.201 +xoSwaSeELbR0PHe0zb/BSg 63 0
1.202 #2 := false
1.203 #11 := 0::int
1.204 decl uf_2 :: int
1.205 @@ -3186,7 +3186,7 @@
1.206 #76 := [mp #52 #75]: #63
1.207 [mp #76 #84]: false
1.208 unsat
1.209 -dCX9jxibjKl6gmr8okzk0w 35 0
1.210 +ciHqmDSmPpA15rO932dhvA 35 0
1.211 #2 := false
1.212 #6 := 5::int
1.213 #4 := 2::int
1.214 @@ -3222,7 +3222,7 @@
1.215 #25 := [asserted]: #9
1.216 [mp #25 #49]: false
1.217 unsat
1.218 -/kLzs8f/jQjEM38PdppYPA 45 0
1.219 +HzwFy7SRHqpspkYnzyeF4w 45 0
1.220 #2 := false
1.221 #11 := 4::real
1.222 decl uf_2 :: real
1.223 @@ -3268,7 +3268,7 @@
1.224 #60 := [mp #36 #59]: #51
1.225 [th-lemma #60 #47 #38]: false
1.226 unsat
1.227 -iT8vKYi503k30rQLczD7yw 59 0
1.228 +XW7QIWmzYjfQXaHHPc98eA 59 0
1.229 #2 := false
1.230 #16 := (not false)
1.231 decl uf_2 :: int
1.232 @@ -3328,7 +3328,94 @@
1.233 #34 := [asserted]: #18
1.234 [mp #34 #71]: false
1.235 unsat
1.236 -6R4JcV7tL9QRH7WWPAKM5g 212 0
1.237 +ZGL00TLLioiLlWFiXUnbxg 86 0
1.238 +#2 := false
1.239 +decl uf_1 :: int
1.240 +#5 := uf_1
1.241 +#7 := 2::int
1.242 +#29 := (* 2::int uf_1)
1.243 +#4 := 0::int
1.244 +#54 := (= 0::int #29)
1.245 +#55 := (not #54)
1.246 +#61 := (= #29 0::int)
1.247 +#104 := (not #61)
1.248 +#110 := (iff #104 #55)
1.249 +#108 := (iff #61 #54)
1.250 +#109 := [commutativity]: #108
1.251 +#111 := [monotonicity #109]: #110
1.252 +#62 := (<= #29 0::int)
1.253 +#100 := (not #62)
1.254 +#30 := (<= uf_1 0::int)
1.255 +#31 := (not #30)
1.256 +#6 := (< 0::int uf_1)
1.257 +#32 := (iff #6 #31)
1.258 +#33 := [rewrite]: #32
1.259 +#27 := [asserted]: #6
1.260 +#34 := [mp #27 #33]: #31
1.261 +#101 := (or #100 #30)
1.262 +#102 := [th-lemma]: #101
1.263 +#103 := [unit-resolution #102 #34]: #100
1.264 +#105 := (or #104 #62)
1.265 +#106 := [th-lemma]: #105
1.266 +#107 := [unit-resolution #106 #103]: #104
1.267 +#112 := [mp #107 #111]: #55
1.268 +#56 := (= uf_1 #29)
1.269 +#57 := (not #56)
1.270 +#53 := (= 0::int uf_1)
1.271 +#50 := (not #53)
1.272 +#58 := (and #50 #55 #57)
1.273 +#69 := (not #58)
1.274 +#42 := (distinct 0::int uf_1 #29)
1.275 +#47 := (not #42)
1.276 +#9 := (- uf_1 uf_1)
1.277 +#8 := (* uf_1 2::int)
1.278 +#10 := (distinct uf_1 #8 #9)
1.279 +#11 := (not #10)
1.280 +#48 := (iff #11 #47)
1.281 +#45 := (iff #10 #42)
1.282 +#39 := (distinct uf_1 #29 0::int)
1.283 +#43 := (iff #39 #42)
1.284 +#44 := [rewrite]: #43
1.285 +#40 := (iff #10 #39)
1.286 +#37 := (= #9 0::int)
1.287 +#38 := [rewrite]: #37
1.288 +#35 := (= #8 #29)
1.289 +#36 := [rewrite]: #35
1.290 +#41 := [monotonicity #36 #38]: #40
1.291 +#46 := [trans #41 #44]: #45
1.292 +#49 := [monotonicity #46]: #48
1.293 +#28 := [asserted]: #11
1.294 +#52 := [mp #28 #49]: #47
1.295 +#80 := (or #42 #69)
1.296 +#81 := [def-axiom]: #80
1.297 +#82 := [unit-resolution #81 #52]: #69
1.298 +#59 := (= uf_1 0::int)
1.299 +#83 := (not #59)
1.300 +#89 := (iff #83 #50)
1.301 +#87 := (iff #59 #53)
1.302 +#88 := [commutativity]: #87
1.303 +#90 := [monotonicity #88]: #89
1.304 +#84 := (or #83 #30)
1.305 +#85 := [th-lemma]: #84
1.306 +#86 := [unit-resolution #85 #34]: #83
1.307 +#91 := [mp #86 #90]: #50
1.308 +#64 := -1::int
1.309 +#65 := (* -1::int #29)
1.310 +#66 := (+ uf_1 #65)
1.311 +#68 := (>= #66 0::int)
1.312 +#92 := (not #68)
1.313 +#93 := (or #92 #30)
1.314 +#94 := [th-lemma]: #93
1.315 +#95 := [unit-resolution #94 #34]: #92
1.316 +#96 := (or #57 #68)
1.317 +#97 := [th-lemma]: #96
1.318 +#98 := [unit-resolution #97 #95]: #57
1.319 +#76 := (or #58 #53 #54 #56)
1.320 +#77 := [def-axiom]: #76
1.321 +#99 := [unit-resolution #77 #98 #91 #82]: #54
1.322 +[unit-resolution #99 #112]: false
1.323 +unsat
1.324 +DWt5rIK6NWlI4vrw+691Zg 212 0
1.325 #2 := false
1.326 decl uf_4 :: T1
1.327 #13 := uf_4
1.328 @@ -3541,94 +3628,7 @@
1.329 #519 := [unit-resolution #521 #518]: #547
1.330 [unit-resolution #519 #522]: false
1.331 unsat
1.332 -eOXl5Nf4A2Sq4Q+Wh5XNfA 86 0
1.333 -#2 := false
1.334 -decl uf_1 :: int
1.335 -#5 := uf_1
1.336 -#7 := 2::int
1.337 -#29 := (* 2::int uf_1)
1.338 -#4 := 0::int
1.339 -#54 := (= 0::int #29)
1.340 -#55 := (not #54)
1.341 -#61 := (= #29 0::int)
1.342 -#104 := (not #61)
1.343 -#110 := (iff #104 #55)
1.344 -#108 := (iff #61 #54)
1.345 -#109 := [commutativity]: #108
1.346 -#111 := [monotonicity #109]: #110
1.347 -#62 := (<= #29 0::int)
1.348 -#100 := (not #62)
1.349 -#30 := (<= uf_1 0::int)
1.350 -#31 := (not #30)
1.351 -#6 := (< 0::int uf_1)
1.352 -#32 := (iff #6 #31)
1.353 -#33 := [rewrite]: #32
1.354 -#27 := [asserted]: #6
1.355 -#34 := [mp #27 #33]: #31
1.356 -#101 := (or #100 #30)
1.357 -#102 := [th-lemma]: #101
1.358 -#103 := [unit-resolution #102 #34]: #100
1.359 -#105 := (or #104 #62)
1.360 -#106 := [th-lemma]: #105
1.361 -#107 := [unit-resolution #106 #103]: #104
1.362 -#112 := [mp #107 #111]: #55
1.363 -#56 := (= uf_1 #29)
1.364 -#57 := (not #56)
1.365 -#53 := (= 0::int uf_1)
1.366 -#50 := (not #53)
1.367 -#58 := (and #50 #55 #57)
1.368 -#69 := (not #58)
1.369 -#42 := (distinct 0::int uf_1 #29)
1.370 -#47 := (not #42)
1.371 -#9 := (- uf_1 uf_1)
1.372 -#8 := (* uf_1 2::int)
1.373 -#10 := (distinct uf_1 #8 #9)
1.374 -#11 := (not #10)
1.375 -#48 := (iff #11 #47)
1.376 -#45 := (iff #10 #42)
1.377 -#39 := (distinct uf_1 #29 0::int)
1.378 -#43 := (iff #39 #42)
1.379 -#44 := [rewrite]: #43
1.380 -#40 := (iff #10 #39)
1.381 -#37 := (= #9 0::int)
1.382 -#38 := [rewrite]: #37
1.383 -#35 := (= #8 #29)
1.384 -#36 := [rewrite]: #35
1.385 -#41 := [monotonicity #36 #38]: #40
1.386 -#46 := [trans #41 #44]: #45
1.387 -#49 := [monotonicity #46]: #48
1.388 -#28 := [asserted]: #11
1.389 -#52 := [mp #28 #49]: #47
1.390 -#80 := (or #42 #69)
1.391 -#81 := [def-axiom]: #80
1.392 -#82 := [unit-resolution #81 #52]: #69
1.393 -#59 := (= uf_1 0::int)
1.394 -#83 := (not #59)
1.395 -#89 := (iff #83 #50)
1.396 -#87 := (iff #59 #53)
1.397 -#88 := [commutativity]: #87
1.398 -#90 := [monotonicity #88]: #89
1.399 -#84 := (or #83 #30)
1.400 -#85 := [th-lemma]: #84
1.401 -#86 := [unit-resolution #85 #34]: #83
1.402 -#91 := [mp #86 #90]: #50
1.403 -#64 := -1::int
1.404 -#65 := (* -1::int #29)
1.405 -#66 := (+ uf_1 #65)
1.406 -#68 := (>= #66 0::int)
1.407 -#92 := (not #68)
1.408 -#93 := (or #92 #30)
1.409 -#94 := [th-lemma]: #93
1.410 -#95 := [unit-resolution #94 #34]: #92
1.411 -#96 := (or #57 #68)
1.412 -#97 := [th-lemma]: #96
1.413 -#98 := [unit-resolution #97 #95]: #57
1.414 -#76 := (or #58 #53 #54 #56)
1.415 -#77 := [def-axiom]: #76
1.416 -#99 := [unit-resolution #77 #98 #91 #82]: #54
1.417 -[unit-resolution #99 #112]: false
1.418 -unsat
1.419 -TwJgkTydtls9Q94iw4a3jw 673 0
1.420 +PaSeDRf7Set5ywlblDOoTg 673 0
1.421 #2 := false
1.422 #169 := 0::int
1.423 decl uf_2 :: int
1.424 @@ -4302,7 +4302,7 @@
1.425 #410 := [mp #349 #409]: #405
1.426 [unit-resolution #410 #710 #709 #697 #706]: false
1.427 unsat
1.428 -ib5n9nvBAC5jXuKIpV/54g 2291 0
1.429 +U7jSPEM53XYq3qs03aUczw 2291 0
1.430 #2 := false
1.431 #6 := 0::int
1.432 decl z3name!0 :: int
1.433 @@ -6594,7 +6594,7 @@
1.434 #2323 := [unit-resolution #918 #2322]: #100
1.435 [unit-resolution #917 #2323 #2318]: false
1.436 unsat
1.437 -SqgPFdiZeq8SOFuTISQN5g 52 0
1.438 +eqE7IAqFr0UIBuUsVDgHvw 52 0
1.439 #2 := false
1.440 #8 := 1::real
1.441 decl uf_1 :: real
1.442 @@ -6647,7 +6647,7 @@
1.443 #29 := [asserted]: #13
1.444 [mp #29 #65]: false
1.445 unsat
1.446 -rOkYPs+Q++z/M3OPR/88JQ 59 0
1.447 +ADs4ZPiuUr7Xu7tk71NnEw 59 0
1.448 #2 := false
1.449 #55 := 0::int
1.450 #7 := 2::int
1.451 @@ -6707,7 +6707,7 @@
1.452 #144 := [unit-resolution #143 #28]: #58
1.453 [unit-resolution #144 #68]: false
1.454 unsat
1.455 -oSBTeiF6GKDeHPsMxXHXtQ 54 0
1.456 +x2NmsblNl28xPXP2EG22rA 54 0
1.457 #2 := false
1.458 #5 := 2::int
1.459 decl uf_1 :: int
1.460 @@ -6762,7 +6762,7 @@
1.461 #139 := [unit-resolution #138 #27]: #127
1.462 [unit-resolution #139 #62]: false
1.463 unsat
1.464 -hqH9yBHvmZgES3pBkvsqVQ 118 0
1.465 +kfLiOGBz3RZx9wt+FS+hfg 118 0
1.466 #2 := false
1.467 #5 := 0::real
1.468 decl uf_1 :: real
1.469 @@ -6881,7 +6881,7 @@
1.470 #126 := [mp #101 #125]: #115
1.471 [unit-resolution #126 #132 #129]: false
1.472 unsat
1.473 -ar4IlNF9IylWgGSPOf9paw 208 0
1.474 +FPTJq9aN3ES4iIrHgaTv+A 208 0
1.475 #2 := false
1.476 #9 := 0::int
1.477 #11 := 4::int
1.478 @@ -7090,7 +7090,7 @@
1.479 #418 := [unit-resolution #417 #36]: #298
1.480 [th-lemma #418 #415 #412 #411 #99 #400 #397 #396]: false
1.481 unsat
1.482 -o9WM91Nq0O5f08PEA0qA6w 24 0
1.483 +yN0aj3KferzvOSp2KlyNwg 24 0
1.484 #2 := false
1.485 #4 := (exists (vars (?x1 int)) false)
1.486 #5 := (not #4)
1.487 @@ -7115,7 +7115,7 @@
1.488 #22 := [asserted]: #6
1.489 [mp #22 #38]: false
1.490 unsat
1.491 -SJxvvXYE4z1G4iLRBCPerg 24 0
1.492 +7iMPasu6AIeHm45slLCByA 24 0
1.493 #2 := false
1.494 #4 := (exists (vars (?x1 real)) false)
1.495 #5 := (not #4)
1.496 @@ -7140,13 +7140,13 @@
1.497 #22 := [asserted]: #6
1.498 [mp #22 #38]: false
1.499 unsat
1.500 -Fr3hfDrqfMuGDpDYbXAHwg 1 0
1.501 -unsat
1.502 -bFuFCRUoQSRWyp0iCwo+PA 1 0
1.503 -unsat
1.504 -NJEgv3p5NO4/yEATNBBDNw 1 0
1.505 -unsat
1.506 -RC1LWjyqEEsh1xhocCgPmQ 73 0
1.507 +cv2pC2I0gIUYtVwtXngvXg 1 0
1.508 +unsat
1.509 +4r8/IxBBDH1ZqF0YfzLLTg 1 0
1.510 +unsat
1.511 +uj7n+C4nG462DNJy9Divrg 1 0
1.512 +unsat
1.513 +dn/LVwy1BXEOmtqdUBNhLw 73 0
1.514 #2 := false
1.515 #5 := 0::int
1.516 #8 := 1::int
1.517 @@ -7220,7 +7220,7 @@
1.518 #144 := [trans #142 #82]: #143
1.519 [mp #144 #146]: false
1.520 unsat
1.521 -6pnpFuE9SN6Jr5Upml9T0A 82 0
1.522 +VzZ1W5SEEis1AJp1qZz86g 82 0
1.523 #2 := false
1.524 #5 := (:var 0 int)
1.525 #7 := 0::int
1.526 @@ -7303,7 +7303,7 @@
1.527 #30 := [asserted]: #14
1.528 [mp #30 #96]: false
1.529 unsat
1.530 -sHpY0IFBgZUNhP56aRB+/w 78 0
1.531 +UoXgZh5LkmyNCmQEfEtnig 78 0
1.532 #2 := false
1.533 #5 := (:var 0 int)
1.534 #7 := 2::int
1.535 @@ -7382,7 +7382,7 @@
1.536 #31 := [asserted]: #15
1.537 [mp #31 #92]: false
1.538 unsat
1.539 -7GSX+dyn9XwHWNcjJ4X1ww 61 0
1.540 +Qv4gVhCmOzC39uufV9ZpDA 61 0
1.541 #2 := false
1.542 #9 := (:var 0 int)
1.543 #4 := 2::int
1.544 @@ -7444,7 +7444,7 @@
1.545 #30 := [asserted]: #14
1.546 [mp #30 #75]: false
1.547 unsat
1.548 -oieid3+1h5s04LTQ9d796Q 111 0
1.549 ++j+tSj7aUImWej2XcTL9dw 111 0
1.550 #2 := false
1.551 #4 := 2::int
1.552 decl ?x1!1 :: int
1.553 @@ -7556,7 +7556,7 @@
1.554 #184 := [th-lemma]: #183
1.555 [unit-resolution #184 #127 #125 #126]: false
1.556 unsat
1.557 -+RiWXCcHPvuSeYUjZ4Ky/g 89 0
1.558 +kQRsBd9oowc7exsvsEgTUg 89 0
1.559 #2 := false
1.560 #4 := 0::int
1.561 decl ?x1!0 :: int
1.562 @@ -7646,7 +7646,7 @@
1.563 #167 := [unit-resolution #154 #90]: #166
1.564 [unit-resolution #167 #165 #162]: false
1.565 unsat
1.566 -hlG1vHDJCcXbyvxKYDWifg 83 2
1.567 +VPjD8BtzPcTZKIRT4SA3Nw 83 2
1.568 #2 := false
1.569 #5 := 0::int
1.570 #4 := (:var 0 int)
1.571 @@ -7730,9 +7730,9 @@
1.572 #62 := [mp~ #54 #61]: #49
1.573 [unit-resolution #62 #174]: false
1.574 unsat
1.575 -WARNING: failed to find a pattern for quantifier (quantifier id: k!1)
1.576 +WARNING: failed to find a pattern for quantifier (quantifier id: k!2)
1.577
1.578 -oOC8ghGUYboMezGio2exAg 180 2
1.579 +DCV5zpDW3cC2A61VghqFkA 180 2
1.580 #2 := false
1.581 #4 := 0::int
1.582 #5 := (:var 0 int)
1.583 @@ -7913,9 +7913,9 @@
1.584 #585 := [unit-resolution #128 #581]: #55
1.585 [unit-resolution #585 #307]: false
1.586 unsat
1.587 -WARNING: failed to find a pattern for quantifier (quantifier id: k!1)
1.588 +WARNING: failed to find a pattern for quantifier (quantifier id: k!2)
1.589
1.590 -4Dtb5Y1TTRPWZcHG9Griog 68 0
1.591 +lYXJpXHB9nLXJbOsr9VH1w 68 0
1.592 #2 := false
1.593 #12 := 1::int
1.594 #9 := (:var 1 int)
1.595 @@ -7984,7 +7984,7 @@
1.596 #32 := [asserted]: #16
1.597 [mp #32 #83]: false
1.598 unsat
1.599 -dbOre63OdVavsqL3lG2ttw 107 0
1.600 +jNvpOd8qnh73F8B6mQDrRw 107 0
1.601 #2 := false
1.602 #4 := 0::int
1.603 decl ?x2!1 :: int
1.604 @@ -8092,7 +8092,7 @@
1.605 #123 := [and-elim #101]: #88
1.606 [th-lemma #123 #124 #125]: false
1.607 unsat
1.608 -LtM5szEGH9QAF1TwsVtH4w 117 0
1.609 +QWWPBUGjgvTCpxqJ9oPGdQ 117 0
1.610 #2 := false
1.611 #4 := 0::int
1.612 decl ?x2!1 :: int
1.613 @@ -8210,7 +8210,7 @@
1.614 #188 := [unit-resolution #187 #110]: #98
1.615 [unit-resolution #188 #130]: false
1.616 unsat
1.617 -ibIqbnIUB+oyERADdbFW6w 148 0
1.618 +3r4MsKEvDJc1RWnNRxu/3Q 148 0
1.619 #2 := false
1.620 #144 := (not false)
1.621 #7 := 0::int
1.622 @@ -8359,7 +8359,7 @@
1.623 #158 := [mp #126 #157]: #153
1.624 [mp #158 #181]: false
1.625 unsat
1.626 -1HbJvLWS/aG8IZEVLDIWyA 67 0
1.627 +Q+cnHyqIFLGWsSlQkp3fEg 67 0
1.628 #2 := false
1.629 #4 := (:var 0 int)
1.630 #5 := (pattern #4)
1.631 @@ -8427,9 +8427,9 @@
1.632 #30 := [asserted]: #14
1.633 [mp #30 #80]: false
1.634 unsat
1.635 -K7kWge9RT44bPFRy+hxaqg 1 0
1.636 -unsat
1.637 -+rwKUm5bOzD9paEkmogLyw 75 0
1.638 +Q7HDzu4ER2dw+lHHM6YgFg 1 0
1.639 +unsat
1.640 +saejIG5KeeVxOolEIo3gtw 75 0
1.641 #2 := false
1.642 #6 := 1::int
1.643 decl uf_3 :: int
1.644 @@ -8505,7 +8505,7 @@
1.645 #32 := [asserted]: #16
1.646 [mp #32 #86]: false
1.647 unsat
1.648 -iRJ30NP1Enylq9tZfpCPTA 62 0
1.649 +PPaoU5CzQFYr3LRpOsGPhQ 62 0
1.650 #2 := false
1.651 decl uf_2 :: real
1.652 #6 := uf_2
1.653 @@ -8568,7 +8568,7 @@
1.654 #32 := [asserted]: #16
1.655 [mp #32 #74]: false
1.656 unsat
1.657 -Ff1vqDiuUnet19j/x+mXkA 141 0
1.658 +hXKzem5+KYZMOj+GKxjszQ 141 0
1.659 #2 := false
1.660 decl uf_4 :: int
1.661 #9 := uf_4
1.662 @@ -8710,7 +8710,7 @@
1.663 #45 := [asserted]: #29
1.664 [mp #45 #150]: false
1.665 unsat
1.666 -iPZ87GNdi7uQw4ehEpbTPQ 252 0
1.667 +3D8WhjZTO7T824d7mwXcCA 252 0
1.668 #2 := false
1.669 #9 := 0::int
1.670 decl uf_2 :: (-> T1 int)
1.671 @@ -8963,7 +8963,7 @@
1.672 #539 := [unit-resolution #532 #451]: #557
1.673 [th-lemma #455 #539 #537 #546]: false
1.674 unsat
1.675 -kDuOn7kAggfP4Um8ghhv5A 223 0
1.676 +kyphS4o71h68g2YhvYbQQQ 223 0
1.677 #2 := false
1.678 #23 := 3::int
1.679 decl uf_2 :: (-> T1 int)
1.680 @@ -9187,7 +9187,7 @@
1.681 #598 := [unit-resolution #593 #596]: #623
1.682 [th-lemma #152 #598 #139]: false
1.683 unsat
1.684 -aiB004AWADNjynNrqCDsxw 367 0
1.685 +M8P5WxpiY5AWxaJDBtXoLQ 367 0
1.686 #2 := false
1.687 #9 := 0::int
1.688 decl uf_2 :: (-> T1 int)
1.689 @@ -9555,7 +9555,7 @@
1.690 #456 := [th-lemma]: #455
1.691 [unit-resolution #456 #464 #452]: false
1.692 unsat
1.693 -twoPNF2RBLeff4yYfubpfg 302 0
1.694 +Xs4JZCKb5egkcPabsrodXg 302 0
1.695 #2 := false
1.696 #9 := 0::int
1.697 decl uf_2 :: (-> T1 int)
1.698 @@ -9858,7 +9858,7 @@
1.699 #601 := [unit-resolution #615 #613]: #683
1.700 [th-lemma #623 #188 #601 #628]: false
1.701 unsat
1.702 -ZcLxnpFewGGQ0H47MfRXGw 458 0
1.703 +clMAi2WqMi360EjFURRGLg 458 0
1.704 #2 := false
1.705 #9 := 0::int
1.706 decl uf_2 :: (-> T1 int)
1.707 @@ -10317,7 +10317,7 @@
1.708 #350 := [unit-resolution #369 #367]: #368
1.709 [unit-resolution #350 #323]: false
1.710 unsat
1.711 -ipe8HUL/t33OoeNl/z0smQ 161 0
1.712 +mu7O1os0t3tPqWZhwizjxw 161 0
1.713 #2 := false
1.714 #9 := 0::int
1.715 decl uf_3 :: int
1.716 @@ -10479,7 +10479,7 @@
1.717 #361 := [unit-resolution #639 #655]: #647
1.718 [th-lemma #656 #361 #261]: false
1.719 unsat
1.720 -9FrZeHP8ZKJM+JmhfAjimQ 557 0
1.721 +08cmOtIT4NYs2PG/F3zeZw 557 0
1.722 #2 := false
1.723 #9 := 0::int
1.724 decl uf_2 :: (-> T1 int)
1.725 @@ -11037,57 +11037,57 @@
1.726 #990 := [unit-resolution #501 #807]: #511
1.727 [unit-resolution #990 #989 #979]: false
1.728 unsat
1.729 -uq2MbDTgTG1nxWdwzZtWew 1 0
1.730 -unsat
1.731 -E5BydeDaPocMMvChMGY+og 1 0
1.732 -unsat
1.733 -p81EQzqwJrGunGO7GuNt3g 1 0
1.734 -unsat
1.735 -KpYfvnTcz2WncWNg3dJDCA 1 0
1.736 -unsat
1.737 -ybGRm230DLO0wH6aROKBBw 1 0
1.738 -unsat
1.739 -goFtZfJ6kkxA8sqBVpZutw 1 0
1.740 -unsat
1.741 -0+nmgsMqioeTuwam1ScP7g 1 0
1.742 -unsat
1.743 -nI63LP/VCL//bjsS1gNB2A 1 0
1.744 -unsat
1.745 -9+2QHvrRgbKz97Zg0kfybw 1 0
1.746 -unsat
1.747 -6kquszLXeBUhTwzaw6gd2Q 1 0
1.748 -unsat
1.749 -j5Z04lpza+N5I1cpno5mtw 1 0
1.750 -unsat
1.751 -mapbfUM6Ils30x5nEBJmaw 1 0
1.752 -unsat
1.753 -e8P++0FczY3zhNhEVclACw 1 0
1.754 -unsat
1.755 -yXMQNOyCylhI+EH8hNYxHA 1 0
1.756 -unsat
1.757 -GkYN9j7cjrR2KR/lb04/qw 1 0
1.758 -unsat
1.759 -PajzgNjLWHwVHpjoje+gnA 1 0
1.760 -unsat
1.761 -URpJYU7D8PO0VRnciRgE5A 1 0
1.762 -unsat
1.763 -D9ZGhymoV3L6zbWsJlwG2A 1 0
1.764 -unsat
1.765 -0QLuovrnnANWnCkUY3l10g 1 0
1.766 -unsat
1.767 -CYprps2G0Au5F3Z7n3KTRg 1 0
1.768 -unsat
1.769 -iyIMuJd6zijfEao8zKnx2w 1 0
1.770 -unsat
1.771 -49jzsAwAEfR6NSFBhBEisQ 1 0
1.772 -unsat
1.773 -T0j6xFgrghxif91jL+2yAw 1 0
1.774 -unsat
1.775 -md/M3rVve0+8sQ6oqIoL2w 1 0
1.776 -unsat
1.777 -pY7C8PCf5lVVaim6q7PJcQ 1 0
1.778 -unsat
1.779 -4zCFLQf4Jrov/gmEvsBm4Q 43 0
1.780 +8HdmSMHHP2B8XMFzjNuw5Q 1 0
1.781 +unsat
1.782 +O4aM0+/isn2q5CrIefZjzg 1 0
1.783 +unsat
1.784 +t/ni9djl2DqxH0iKupZSwg 1 0
1.785 +unsat
1.786 +RumBGekdxZQaBF1HNa3x9w 1 0
1.787 +unsat
1.788 +Q9d+IbQ8chjKld71X6/zqw 1 0
1.789 +unsat
1.790 +PhC8zQV8hnJ6E2YYjZPGjQ 1 0
1.791 +unsat
1.792 +mieI2RhSp3bYaojlWH1A4A 1 0
1.793 +unsat
1.794 +pRSV6nBLconzrQz2zUrJ6g 1 0
1.795 +unsat
1.796 +Js0JfdwDoKq3YuilPPgeZw 1 0
1.797 +unsat
1.798 +GRIqjLUJiqXbo+pXhAeKIw 1 0
1.799 +unsat
1.800 +Bg5scsmPFp82+7Y2ScL6Wg 1 0
1.801 +unsat
1.802 +XD6zX6850dLxyfZSfNv30A 1 0
1.803 +unsat
1.804 +BG/HwJYnumvDICXxtBu/tA 1 0
1.805 +unsat
1.806 +YMc4t19sUMWbUkx3woxCmQ 1 0
1.807 +unsat
1.808 +YyD9IF72pKXGGKZTO7FY5Q 1 0
1.809 +unsat
1.810 +zRPsIUi+TEoz5fPWP0H9bQ 1 0
1.811 +unsat
1.812 +8ipTE8BOXpvSo/U6D4p3lA 1 0
1.813 +unsat
1.814 +MSzQywedZPsOE0CDxrrO0g 1 0
1.815 +unsat
1.816 +SryZuXv48ItET8NPIv07pA 1 0
1.817 +unsat
1.818 +qOMUQN18hYFl/wWt54lvbA 1 0
1.819 +unsat
1.820 ++njWXdn6fETK3/AjtiHjcA 1 0
1.821 +unsat
1.822 +5cQ7gJ33gzYTIIPA3hbBmQ 1 0
1.823 +unsat
1.824 +ZznT34cvumrP00mXZ3gcjw 1 0
1.825 +unsat
1.826 +//LQca1Et5RfhQJZA+CGCA 1 0
1.827 +unsat
1.828 +3ntxKz+kaQNfTrLzY9sVXw 1 0
1.829 +unsat
1.830 +4lL2Qo8ngE1EH1UdeN1Qng 43 0
1.831 #2 := false
1.832 #6 := 0::int
1.833 decl uf_1 :: (-> bv[2] int)
1.834 @@ -11131,9 +11131,9 @@
1.835 #287 := [th-lemma]: #627
1.836 [unit-resolution #287 #47 #635]: false
1.837 unsat
1.838 -czvSLyjMowmFNi82us4N2Q 1 0
1.839 -unsat
1.840 -aU+7kcyE8oAPbs5RjfuwIw 50 0
1.841 ++xe3O927LrflFUE6NDqRlA 1 0
1.842 +unsat
1.843 +JPoL7fPYhqhAkjUiVF+THQ 50 0
1.844 #2 := false
1.845 decl uf_6 :: T2
1.846 #23 := uf_6
1.847 @@ -11184,7 +11184,7 @@
1.848 #66 := [asserted]: #26
1.849 [unit-resolution #66 #235]: false
1.850 unsat
1.851 -dXfueqZAXkudfE6G0VKkwg 105 0
1.852 +l23ZDmd0VbO/Q+uO5EtabA 105 0
1.853 #2 := false
1.854 decl uf_6 :: (-> T4 T2)
1.855 decl uf_10 :: T4
1.856 @@ -11290,7 +11290,7 @@
1.857 #110 := [asserted]: #46
1.858 [unit-resolution #110 #238]: false
1.859 unsat
1.860 -Dc/6bNJffjYYplvoitScJQ 181 0
1.861 +GZjffeZPQnL3OyLCvxdCpg 181 0
1.862 #2 := false
1.863 decl uf_1 :: (-> T1 T2 T3)
1.864 decl uf_3 :: T2
1.865 @@ -11472,7 +11472,7 @@
1.866 #76 := [asserted]: #38
1.867 [unit-resolution #76 #489]: false
1.868 unsat
1.869 -jdmsd1j41Osn+WzTtqTUSQ 62 0
1.870 +i6jCzzRosHYE0w7sF1Nraw 62 0
1.871 #2 := false
1.872 decl up_4 :: (-> T1 T2 bool)
1.873 decl uf_3 :: T2
1.874 @@ -11535,7 +11535,7 @@
1.875 #73 := [unit-resolution #71 #68]: #72
1.876 [unit-resolution #73 #59 #61]: false
1.877 unsat
1.878 -EA8ecQ7czWL46/C3k7D7tg 115 0
1.879 +YZHSyhN2TGlpe+vpkzWrgQ 115 0
1.880 #2 := false
1.881 decl up_2 :: (-> T2 bool)
1.882 decl uf_3 :: T2
1.883 @@ -11651,7 +11651,7 @@
1.884 #560 := [mp #344 #559]: #557
1.885 [unit-resolution #560 #576 #561]: false
1.886 unsat
1.887 -mNfbN3NQCB4ik2xJmLE1UQ 464 0
1.888 +TibRlXkU+X+1+zGPYTiT0g 464 0
1.889 #2 := false
1.890 decl uf_2 :: (-> T2 T3 T3)
1.891 decl uf_4 :: T3
1.892 @@ -12116,7 +12116,7 @@
1.893 #177 := [asserted]: #53
1.894 [unit-resolution #177 #793]: false
1.895 unsat
1.896 -Jtmz+P173L9nRQkQk52h+Q 21 0
1.897 +DJPKxi9AO25zGBcs5kxUrw 21 0
1.898 #2 := false
1.899 decl up_1 :: (-> T1 bool)
1.900 #4 := (:var 0 T1)
1.901 @@ -12138,7 +12138,7 @@
1.902 #25 := [asserted]: #9
1.903 [mp #25 #34]: false
1.904 unsat
1.905 -YG20f6Uf93koN6rVg/alpA 366 0
1.906 +i5PnMbuM9mWv5LnVszz9+g 366 0
1.907 #2 := false
1.908 decl uf_1 :: (-> int T1)
1.909 #37 := 6::int
1.910 @@ -12505,7 +12505,7 @@
1.911 #182 := [asserted]: #40
1.912 [unit-resolution #182 #399]: false
1.913 unsat
1.914 -/fwo5o8vhLVHyS4oYEs4QA 408 0
1.915 +K2SXMHU6QCZJ8TRs6zjKRg 408 0
1.916 #2 := false
1.917 #22 := 0::int
1.918 #8 := 2::int
1.919 @@ -12914,7 +12914,7 @@
1.920 #375 := [unit-resolution #374 #407]: #708
1.921 [th-lemma #375 #370 #465]: false
1.922 unsat
1.923 -s8LL71+1HTN+eIuEYeKhUw 50 0
1.924 +1DhSL9G2fGRGmuI8IaMNOA 50 0
1.925 #2 := false
1.926 decl up_35 :: (-> int bool)
1.927 #112 := 1::int
1.928 @@ -12965,7 +12965,7 @@
1.929 #504 := [quant-inst]: #503
1.930 [unit-resolution #504 #916 #297]: false
1.931 unsat
1.932 -MZYsU5krlrOK4MkB71Ikeg 506 0
1.933 +dyXROdcPFSd36N3K7dpmDw 506 0
1.934 #2 := false
1.935 decl uf_17 :: (-> T8 T3)
1.936 decl uf_18 :: (-> T1 T8)