1.1 --- a/src/HOL/SMT/Examples/SMT_Examples.certs Fri Mar 26 23:57:35 2010 +0100
1.2 +++ b/src/HOL/SMT/Examples/SMT_Examples.certs Fri Mar 26 23:58:27 2010 +0100
1.3 @@ -224,7 +224,7 @@
1.4 #30 := [asserted]: #14
1.5 [mp #30 #70]: false
1.6 unsat
1.7 -c6eb111aa830c9669a030c2e58b4e827706981da 194 0
1.8 +212c7825456dae820eef6b1fa0cb8c5ceeff8780 194 0
1.9 #2 := false
1.10 decl up_1 :: bool
1.11 #4 := up_1
1.12 @@ -472,7 +472,7 @@
1.13 #113 := [quant-inst]: #199
1.14 [unit-resolution #113 #536 #49]: false
1.15 unsat
1.16 -94169ba151f7a720e818287ce490015dde764bad 1667 0
1.17 +62bff2883948b13c19c4cd52ed250bf0afc3ec90 1667 0
1.18 #2 := false
1.19 decl up_54 :: bool
1.20 #126 := up_54
1.21 @@ -2219,7 +2219,7 @@
1.22 #82 := [and-elim #81]: #55
1.23 [unit-resolution #82 #95]: false
1.24 unsat
1.25 -18bde40beb0dd1fc2613a67805e24d767dd9a3bf 135 0
1.26 +bc722e6a73140d95a8643a8d8a522de8bf529dea 135 0
1.27 #2 := false
1.28 decl up_1 :: (-> T1 T2 bool)
1.29 #5 := (:var 0 T2)
1.30 @@ -2355,7 +2355,8 @@
1.31 #176 := [quant-inst]: #538
1.32 [unit-resolution #176 #252 #535]: false
1.33 unsat
1.34 -013861f683c286a3ef38681266913846a3a39b9a 135 2
1.35 +3ad10572aa4268ecfd73368c6cc15680136648a3 136 0
1.36 +WARNING: failed to find a pattern for quantifier (quantifier id: k!12)
1.37 #2 := false
1.38 decl up_1 :: (-> T1 T2 bool)
1.39 #5 := (:var 0 T2)
1.40 @@ -2491,8 +2492,6 @@
1.41 #235 := [quant-inst]: #597
1.42 [unit-resolution #235 #311 #594]: false
1.43 unsat
1.44 -WARNING: failed to find a pattern for quantifier (quantifier id: k!12)
1.45 -
1.46 0e958e27514643bb596851e6dbb61a23f6b348b0 56 0
1.47 #2 := false
1.48 decl up_1 :: (-> T1 bool)
1.49 @@ -2942,7 +2941,7 @@
1.50 #294 := [unit-resolution #190 #293]: #188
1.51 [th-lemma #280 #294]: false
1.52 unsat
1.53 -8e6af261ea9f94b967813d4e2f2abcb94463d612 124 0
1.54 +a67db8da0b1a1104d4370e2e261e8521096f24e1 124 0
1.55 #2 := false
1.56 decl uf_1 :: (-> T1 T2)
1.57 decl uf_3 :: T1
1.58 @@ -3222,7 +3221,7 @@
1.59 #25 := [asserted]: #9
1.60 [mp #25 #49]: false
1.61 unsat
1.62 -5f3503ae4a43341932052006638f286bea551e87 45 0
1.63 +7a45124c81166760c08802d05bb1a73c01b0f138 45 0
1.64 #2 := false
1.65 #11 := 4::real
1.66 decl uf_2 :: real
1.67 @@ -3268,7 +3267,7 @@
1.68 #60 := [mp #36 #59]: #51
1.69 [th-lemma #60 #47 #38]: false
1.70 unsat
1.71 -347776ce17d7d3f6d1252ead05795e4eee6f4b20 59 0
1.72 +f946ff901958cea1a0225dfba1e556060c889a10 59 0
1.73 #2 := false
1.74 #16 := (not false)
1.75 decl uf_2 :: int
1.76 @@ -3328,7 +3327,7 @@
1.77 #34 := [asserted]: #18
1.78 [mp #34 #71]: false
1.79 unsat
1.80 -f7b1b99e3470f713e48aaae1336ace10223be6f0 212 0
1.81 +88d529b1517abb78e220ec8f58e3b3405bb2453b 212 0
1.82 #2 := false
1.83 decl uf_4 :: T1
1.84 #13 := uf_4
1.85 @@ -3628,7 +3627,7 @@
1.86 #99 := [unit-resolution #77 #98 #91 #82]: #54
1.87 [unit-resolution #99 #112]: false
1.88 unsat
1.89 -9791139ea2cfda88ae799477fc61e411aab42b18 673 0
1.90 +d4ecdf21a3d5d758670676ddb9e6e093ea9fcc15 673 0
1.91 #2 := false
1.92 #169 := 0::int
1.93 decl uf_2 :: int
1.94 @@ -4302,7 +4301,7 @@
1.95 #410 := [mp #349 #409]: #405
1.96 [unit-resolution #410 #710 #709 #697 #706]: false
1.97 unsat
1.98 -0d07e457c5602ba4a5dc70af32b6dc53a80a858c 2291 0
1.99 +efea5b71ce31ca68241e4ee8755a8335445d88e6 2291 0
1.100 #2 := false
1.101 #6 := 0::int
1.102 decl z3name!0 :: int
1.103 @@ -6881,7 +6880,7 @@
1.104 #126 := [mp #101 #125]: #115
1.105 [unit-resolution #126 #132 #129]: false
1.106 unsat
1.107 -c8ed8eae868ac61c8f3a616f1b0b1df4032f4eac 208 0
1.108 +8bded5c2f0cd48cce9a86100cc4c6ce26ec88a2e 208 0
1.109 #2 := false
1.110 #9 := 0::int
1.111 #11 := 4::int
1.112 @@ -7646,7 +7645,8 @@
1.113 #167 := [unit-resolution #154 #90]: #166
1.114 [unit-resolution #167 #165 #162]: false
1.115 unsat
1.116 -b7c4f9440c4594c46eee14ce57f17610bb7e2536 83 2
1.117 +b7c4f9440c4594c46eee14ce57f17610bb7e2536 84 0
1.118 +WARNING: failed to find a pattern for quantifier (quantifier id: k!2)
1.119 #2 := false
1.120 #5 := 0::int
1.121 #4 := (:var 0 int)
1.122 @@ -7730,9 +7730,8 @@
1.123 #62 := [mp~ #54 #61]: #49
1.124 [unit-resolution #62 #174]: false
1.125 unsat
1.126 +7a9cc3ee85422788d981af84d181bd61d65f774c 181 0
1.127 WARNING: failed to find a pattern for quantifier (quantifier id: k!2)
1.128 -
1.129 -7a9cc3ee85422788d981af84d181bd61d65f774c 180 2
1.130 #2 := false
1.131 #4 := 0::int
1.132 #5 := (:var 0 int)
1.133 @@ -7913,8 +7912,6 @@
1.134 #585 := [unit-resolution #128 #581]: #55
1.135 [unit-resolution #585 #307]: false
1.136 unsat
1.137 -WARNING: failed to find a pattern for quantifier (quantifier id: k!2)
1.138 -
1.139 5201b12abd6b3d0f247a34c1fd9f443fc951c55f 68 0
1.140 #2 := false
1.141 #12 := 1::int
1.142 @@ -8568,7 +8565,7 @@
1.143 #32 := [asserted]: #16
1.144 [mp #32 #74]: false
1.145 unsat
1.146 -99d65e323e3d85dbdc2d8c52c169db4d46ead198 141 0
1.147 +a89308e99854a72f032798efa6ed32cee1f069ad 141 0
1.148 #2 := false
1.149 decl uf_4 :: int
1.150 #9 := uf_4
1.151 @@ -10479,7 +10476,7 @@
1.152 #361 := [unit-resolution #639 #655]: #647
1.153 [th-lemma #656 #361 #261]: false
1.154 unsat
1.155 -980ba021fe0853c3aa46377383e3f0f6fa9e2888 557 0
1.156 +201224fffb303874a019c931bc3ddb7a48e74843 557 0
1.157 #2 := false
1.158 #9 := 0::int
1.159 decl uf_2 :: (-> T1 int)
1.160 @@ -11131,9 +11128,9 @@
1.161 #287 := [th-lemma]: #627
1.162 [unit-resolution #287 #47 #635]: false
1.163 unsat
1.164 -2e4bd6e1ab7bfedbefd3ada8caf5332ba5651065 1 0
1.165 -unsat
1.166 -96d2e1aad559535e781a07ee5e55bb19caef769c 50 0
1.167 +585c02dc1784e4298147af8e1f7a14d1e20f4938 1 0
1.168 +unsat
1.169 +af0e29f90d51c2b97a1ecaa16facf1cd8b6c5ba3 50 0
1.170 #2 := false
1.171 decl uf_6 :: T2
1.172 #23 := uf_6
1.173 @@ -11184,7 +11181,7 @@
1.174 #66 := [asserted]: #26
1.175 [unit-resolution #66 #235]: false
1.176 unsat
1.177 -008ad82b0a62ff600e66e8f2cc72b5795c7c5032 105 0
1.178 +dda7f93ea68b6650d60fb96e3a60e68637d12660 105 0
1.179 #2 := false
1.180 decl uf_6 :: (-> T4 T2)
1.181 decl uf_10 :: T4
1.182 @@ -11290,7 +11287,7 @@
1.183 #110 := [asserted]: #46
1.184 [unit-resolution #110 #238]: false
1.185 unsat
1.186 -0a15a60660bc0c3f06688ad5de50ed50a24d0df0 181 0
1.187 +bab035487a4c595c2090c8097591bd8874c90db9 181 0
1.188 #2 := false
1.189 decl uf_1 :: (-> T1 T2 T3)
1.190 decl uf_3 :: T2
1.191 @@ -11472,7 +11469,7 @@
1.192 #76 := [asserted]: #38
1.193 [unit-resolution #76 #489]: false
1.194 unsat
1.195 -dde2364f13fc9ce8af00c7a02bfea9a6c979a805 62 0
1.196 +4e1c8dc2fbb6a09931090ee5acf8d0e6f34352b4 62 0
1.197 #2 := false
1.198 decl up_4 :: (-> T1 T2 bool)
1.199 decl uf_3 :: T2
1.200 @@ -11535,7 +11532,7 @@
1.201 #73 := [unit-resolution #71 #68]: #72
1.202 [unit-resolution #73 #59 #61]: false
1.203 unsat
1.204 -3cb6787c7063b0a04bff9e2bfa4203b73903dabe 115 0
1.205 +87c5323638926f09820cf502a43fcd61cba03c0c 115 0
1.206 #2 := false
1.207 decl up_2 :: (-> T2 bool)
1.208 decl uf_3 :: T2
1.209 @@ -11651,7 +11648,7 @@
1.210 #560 := [mp #344 #559]: #557
1.211 [unit-resolution #560 #576 #561]: false
1.212 unsat
1.213 -dcb635ada6f2482ea11de30713fe962bcb57c9ad 464 0
1.214 +352491b756faec7ffa24a6d9cce95d2879223e60 464 0
1.215 #2 := false
1.216 decl uf_2 :: (-> T2 T3 T3)
1.217 decl uf_4 :: T3
1.218 @@ -12138,7 +12135,7 @@
1.219 #25 := [asserted]: #9
1.220 [mp #25 #34]: false
1.221 unsat
1.222 -f6e9645ebbb8739d12b8e96bc83ddef33c7d53bc 366 0
1.223 +c5b3c6b4f593e27f97db06f2c64fc61d8f9bebaa 366 0
1.224 #2 := false
1.225 decl uf_1 :: (-> int T1)
1.226 #37 := 6::int
1.227 @@ -12505,7 +12502,7 @@
1.228 #182 := [asserted]: #40
1.229 [unit-resolution #182 #399]: false
1.230 unsat
1.231 -b15b527236338a437e355afcde07dd3c6dfc451f 408 0
1.232 +9d577a545efebaa46a634487a3e922a7cddbb866 408 0
1.233 #2 := false
1.234 #22 := 0::int
1.235 #8 := 2::int
1.236 @@ -12914,7 +12911,7 @@
1.237 #375 := [unit-resolution #374 #407]: #708
1.238 [th-lemma #375 #370 #465]: false
1.239 unsat
1.240 -71b79533f46a8514b2fc189fc382867d50f52a9a 50 0
1.241 +af6e260cca3c1cafcab25bb9a90bb548b2b7ec6b 50 0
1.242 #2 := false
1.243 decl up_35 :: (-> int bool)
1.244 #112 := 1::int
1.245 @@ -12965,7 +12962,7 @@
1.246 #504 := [quant-inst]: #503
1.247 [unit-resolution #504 #916 #297]: false
1.248 unsat
1.249 -e40ba7aed8ae5409337a331038da0587c03354d6 506 0
1.250 +679f514494fa97481f8fb2124de829ed6e4d2b68 506 0
1.251 #2 := false
1.252 decl uf_17 :: (-> T8 T3)
1.253 decl uf_18 :: (-> T1 T8)