merged
authornoschinl
Wed Sep 14 10:55:07 2011 +0200 (2011-09-14)
changeset 449278bf41f8cf71d
parent 44926 de3ed037c9a5
parent 44925 1db6baa40b0e
child 44928 7ef6505bde7f
merged
     1.1 --- a/src/HOL/SMT_Examples/SMT_Tests.certs	Wed Sep 14 10:24:22 2011 +0200
     1.2 +++ b/src/HOL/SMT_Examples/SMT_Tests.certs	Wed Sep 14 10:55:07 2011 +0200
     1.3 @@ -60554,3 +60554,2186 @@
     1.4  #229 := [mp #227 #156]: #225
     1.5  [unit-resolution #229 #561 #66 #74]: false
     1.6  unsat
     1.7 +7cd7dbb3fbfb0bc76acedbcf070880f3e3e3d434 60 0
     1.8 +#2 := false
     1.9 +decl f3 :: (-> S2 S3 S1)
    1.10 +decl f4 :: S3
    1.11 +#9 := f4
    1.12 +decl f9 :: S2
    1.13 +#39 := f9
    1.14 +#40 := (f3 f9 f4)
    1.15 +decl f1 :: S1
    1.16 +#4 := f1
    1.17 +#116 := (= f1 #40)
    1.18 +#41 := (= #40 f1)
    1.19 +#42 := (not #41)
    1.20 +#43 := (not #42)
    1.21 +#128 := (iff #43 #116)
    1.22 +#120 := (not #116)
    1.23 +#123 := (not #120)
    1.24 +#126 := (iff #123 #116)
    1.25 +#127 := [rewrite]: #126
    1.26 +#124 := (iff #43 #123)
    1.27 +#121 := (iff #42 #120)
    1.28 +#118 := (iff #41 #116)
    1.29 +#119 := [rewrite]: #118
    1.30 +#122 := [monotonicity #119]: #121
    1.31 +#125 := [monotonicity #122]: #124
    1.32 +#129 := [trans #125 #127]: #128
    1.33 +#115 := [asserted]: #43
    1.34 +#132 := [mp #115 #129]: #116
    1.35 +#8 := (:var 0 S2)
    1.36 +#10 := (f3 #8 f4)
    1.37 +#640 := (pattern #10)
    1.38 +#64 := (= f1 #10)
    1.39 +#67 := (not #64)
    1.40 +#641 := (forall (vars (?v0 S2)) (:pat #640) #67)
    1.41 +#70 := (forall (vars (?v0 S2)) #67)
    1.42 +#644 := (iff #70 #641)
    1.43 +#642 := (iff #67 #67)
    1.44 +#643 := [refl]: #642
    1.45 +#645 := [quant-intro #643]: #644
    1.46 +#146 := (~ #70 #70)
    1.47 +#144 := (~ #67 #67)
    1.48 +#145 := [refl]: #144
    1.49 +#147 := [nnf-pos #145]: #146
    1.50 +#11 := (= #10 f1)
    1.51 +#12 := (not #11)
    1.52 +#13 := (forall (vars (?v0 S2)) #12)
    1.53 +#71 := (iff #13 #70)
    1.54 +#68 := (iff #12 #67)
    1.55 +#65 := (iff #11 #64)
    1.56 +#66 := [rewrite]: #65
    1.57 +#69 := [monotonicity #66]: #68
    1.58 +#72 := [quant-intro #69]: #71
    1.59 +#63 := [asserted]: #13
    1.60 +#75 := [mp #63 #72]: #70
    1.61 +#131 := [mp~ #75 #147]: #70
    1.62 +#646 := [mp #131 #645]: #641
    1.63 +#223 := (not #641)
    1.64 +#310 := (or #223 #120)
    1.65 +#224 := [quant-inst #39]: #310
    1.66 +[unit-resolution #224 #646 #132]: false
    1.67 +unsat
    1.68 +71b592381f7787562afdf512ef22356644e574ef 48 0
    1.69 +#2 := false
    1.70 +decl f3 :: (-> S2 S3 S1)
    1.71 +decl f5 :: S3
    1.72 +#14 := f5
    1.73 +decl f9 :: S2
    1.74 +#39 := f9
    1.75 +#40 := (f3 f9 f5)
    1.76 +decl f1 :: S1
    1.77 +#4 := f1
    1.78 +#115 := (= f1 #40)
    1.79 +#119 := (not #115)
    1.80 +#41 := (= #40 f1)
    1.81 +#42 := (not #41)
    1.82 +#120 := (iff #42 #119)
    1.83 +#117 := (iff #41 #115)
    1.84 +#118 := [rewrite]: #117
    1.85 +#121 := [monotonicity #118]: #120
    1.86 +#114 := [asserted]: #42
    1.87 +#124 := [mp #114 #121]: #119
    1.88 +#8 := (:var 0 S2)
    1.89 +#15 := (f3 #8 f5)
    1.90 +#639 := (pattern #15)
    1.91 +#73 := (= f1 #15)
    1.92 +#640 := (forall (vars (?v0 S2)) (:pat #639) #73)
    1.93 +#77 := (forall (vars (?v0 S2)) #73)
    1.94 +#643 := (iff #77 #640)
    1.95 +#641 := (iff #73 #73)
    1.96 +#642 := [refl]: #641
    1.97 +#644 := [quant-intro #642]: #643
    1.98 +#126 := (~ #77 #77)
    1.99 +#125 := (~ #73 #73)
   1.100 +#140 := [refl]: #125
   1.101 +#127 := [nnf-pos #140]: #126
   1.102 +#16 := (= #15 f1)
   1.103 +#17 := (forall (vars (?v0 S2)) #16)
   1.104 +#78 := (iff #17 #77)
   1.105 +#75 := (iff #16 #73)
   1.106 +#76 := [rewrite]: #75
   1.107 +#79 := [quant-intro #76]: #78
   1.108 +#72 := [asserted]: #17
   1.109 +#82 := [mp #72 #79]: #77
   1.110 +#141 := [mp~ #82 #127]: #77
   1.111 +#645 := [mp #141 #644]: #640
   1.112 +#215 := (not #640)
   1.113 +#302 := (or #215 #115)
   1.114 +#216 := [quant-inst #39]: #302
   1.115 +[unit-resolution #216 #645 #124]: false
   1.116 +unsat
   1.117 +164d5a6bdaf120b4948f5b45d9c26eb765a67512 124 0
   1.118 +#2 := false
   1.119 +decl f3 :: (-> S2 S3 S1)
   1.120 +decl f6 :: (-> S4 S3 S3)
   1.121 +decl f11 :: S3
   1.122 +#42 := f11
   1.123 +decl f7 :: (-> S3 S4)
   1.124 +decl f10 :: S3
   1.125 +#40 := f10
   1.126 +#41 := (f7 f10)
   1.127 +#43 := (f6 #41 f11)
   1.128 +decl f9 :: S2
   1.129 +#39 := f9
   1.130 +#44 := (f3 f9 #43)
   1.131 +decl f1 :: S1
   1.132 +#4 := f1
   1.133 +#125 := (= f1 #44)
   1.134 +#144 := (not #125)
   1.135 +#648 := [hypothesis]: #144
   1.136 +#48 := (f3 f9 f11)
   1.137 +#132 := (= f1 #48)
   1.138 +#46 := (f3 f9 f10)
   1.139 +#129 := (= f1 #46)
   1.140 +#135 := (or #129 #132)
   1.141 +#336 := (or #135 #125)
   1.142 +#145 := (iff #135 #144)
   1.143 +#49 := (= #48 f1)
   1.144 +#47 := (= #46 f1)
   1.145 +#50 := (or #47 #49)
   1.146 +#45 := (= #44 f1)
   1.147 +#51 := (iff #45 #50)
   1.148 +#52 := (not #51)
   1.149 +#148 := (iff #52 #145)
   1.150 +#138 := (iff #125 #135)
   1.151 +#141 := (not #138)
   1.152 +#146 := (iff #141 #145)
   1.153 +#147 := [rewrite]: #146
   1.154 +#142 := (iff #52 #141)
   1.155 +#139 := (iff #51 #138)
   1.156 +#136 := (iff #50 #135)
   1.157 +#133 := (iff #49 #132)
   1.158 +#134 := [rewrite]: #133
   1.159 +#130 := (iff #47 #129)
   1.160 +#131 := [rewrite]: #130
   1.161 +#137 := [monotonicity #131 #134]: #136
   1.162 +#127 := (iff #45 #125)
   1.163 +#128 := [rewrite]: #127
   1.164 +#140 := [monotonicity #128 #137]: #139
   1.165 +#143 := [monotonicity #140]: #142
   1.166 +#149 := [trans #143 #147]: #148
   1.167 +#124 := [asserted]: #52
   1.168 +#152 := [mp #124 #149]: #145
   1.169 +#262 := (not #145)
   1.170 +#335 := (or #135 #125 #262)
   1.171 +#332 := [def-axiom]: #335
   1.172 +#315 := [unit-resolution #332 #152]: #336
   1.173 +#320 := [unit-resolution #315 #648]: #135
   1.174 +#322 := (not #135)
   1.175 +#651 := (or #125 #322)
   1.176 +#21 := (:var 0 S3)
   1.177 +#19 := (:var 1 S3)
   1.178 +#20 := (f7 #19)
   1.179 +#22 := (f6 #20 #21)
   1.180 +#18 := (:var 2 S2)
   1.181 +#23 := (f3 #18 #22)
   1.182 +#674 := (pattern #23)
   1.183 +#27 := (f3 #18 #21)
   1.184 +#98 := (= f1 #27)
   1.185 +#25 := (f3 #18 #19)
   1.186 +#95 := (= f1 #25)
   1.187 +#101 := (or #95 #98)
   1.188 +#91 := (= f1 #23)
   1.189 +#104 := (iff #91 #101)
   1.190 +#675 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #674) #104)
   1.191 +#107 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #104)
   1.192 +#678 := (iff #107 #675)
   1.193 +#676 := (iff #104 #104)
   1.194 +#677 := [refl]: #676
   1.195 +#679 := [quant-intro #677]: #678
   1.196 +#156 := (~ #107 #107)
   1.197 +#170 := (~ #104 #104)
   1.198 +#171 := [refl]: #170
   1.199 +#157 := [nnf-pos #171]: #156
   1.200 +#28 := (= #27 f1)
   1.201 +#26 := (= #25 f1)
   1.202 +#29 := (or #26 #28)
   1.203 +#24 := (= #23 f1)
   1.204 +#30 := (iff #24 #29)
   1.205 +#31 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #30)
   1.206 +#108 := (iff #31 #107)
   1.207 +#105 := (iff #30 #104)
   1.208 +#102 := (iff #29 #101)
   1.209 +#99 := (iff #28 #98)
   1.210 +#100 := [rewrite]: #99
   1.211 +#96 := (iff #26 #95)
   1.212 +#97 := [rewrite]: #96
   1.213 +#103 := [monotonicity #97 #100]: #102
   1.214 +#93 := (iff #24 #91)
   1.215 +#94 := [rewrite]: #93
   1.216 +#106 := [monotonicity #94 #103]: #105
   1.217 +#109 := [quant-intro #106]: #108
   1.218 +#90 := [asserted]: #31
   1.219 +#112 := [mp #90 #109]: #107
   1.220 +#172 := [mp~ #112 #157]: #107
   1.221 +#680 := [mp #172 #679]: #675
   1.222 +#321 := (not #675)
   1.223 +#655 := (or #321 #138)
   1.224 +#656 := [quant-inst #39 #40 #42]: #655
   1.225 +#308 := [unit-resolution #656 #680]: #138
   1.226 +#657 := (or #141 #125 #322)
   1.227 +#658 := [def-axiom]: #657
   1.228 +#292 := [unit-resolution #658 #308]: #651
   1.229 +#635 := [unit-resolution #292 #320 #648]: false
   1.230 +#296 := [lemma #635]: #125
   1.231 +#309 := (or #322 #144)
   1.232 +#652 := (or #322 #144 #262)
   1.233 +#654 := [def-axiom]: #652
   1.234 +#441 := [unit-resolution #654 #152]: #309
   1.235 +#297 := [unit-resolution #441 #296]: #322
   1.236 +#298 := (or #144 #135)
   1.237 +#653 := (or #141 #144 #135)
   1.238 +#659 := [def-axiom]: #653
   1.239 +#299 := [unit-resolution #659 #308]: #298
   1.240 +[unit-resolution #299 #297 #296]: false
   1.241 +unsat
   1.242 +d1bc5c257411f66b4000ce061c39762e6b5b7a04 160 0
   1.243 +#2 := false
   1.244 +decl f3 :: (-> S2 S3 S1)
   1.245 +decl f4 :: S3
   1.246 +#9 := f4
   1.247 +decl f9 :: S2
   1.248 +#39 := f9
   1.249 +#325 := (f3 f9 f4)
   1.250 +decl f1 :: S1
   1.251 +#4 := f1
   1.252 +#322 := (= f1 #325)
   1.253 +decl f10 :: S3
   1.254 +#40 := f10
   1.255 +#45 := (f3 f9 f10)
   1.256 +#125 := (= f1 #45)
   1.257 +#326 := (or #125 #322)
   1.258 +decl f6 :: (-> S4 S3 S3)
   1.259 +decl f7 :: (-> S3 S4)
   1.260 +#41 := (f7 f10)
   1.261 +#42 := (f6 #41 f4)
   1.262 +#43 := (f3 f9 #42)
   1.263 +#121 := (= f1 #43)
   1.264 +#134 := (not #121)
   1.265 +#642 := [hypothesis]: #134
   1.266 +#320 := (or #125 #121)
   1.267 +#135 := (iff #125 #134)
   1.268 +#46 := (= #45 f1)
   1.269 +#44 := (= #43 f1)
   1.270 +#47 := (iff #44 #46)
   1.271 +#48 := (not #47)
   1.272 +#138 := (iff #48 #135)
   1.273 +#128 := (iff #121 #125)
   1.274 +#131 := (not #128)
   1.275 +#136 := (iff #131 #135)
   1.276 +#137 := [rewrite]: #136
   1.277 +#132 := (iff #48 #131)
   1.278 +#129 := (iff #47 #128)
   1.279 +#126 := (iff #46 #125)
   1.280 +#127 := [rewrite]: #126
   1.281 +#123 := (iff #44 #121)
   1.282 +#124 := [rewrite]: #123
   1.283 +#130 := [monotonicity #124 #127]: #129
   1.284 +#133 := [monotonicity #130]: #132
   1.285 +#139 := [trans #133 #137]: #138
   1.286 +#120 := [asserted]: #48
   1.287 +#142 := [mp #120 #139]: #135
   1.288 +#232 := (not #135)
   1.289 +#319 := (or #125 #121 #232)
   1.290 +#233 := [def-axiom]: #319
   1.291 +#234 := [unit-resolution #233 #142]: #320
   1.292 +#644 := [unit-resolution #234 #642]: #125
   1.293 +#648 := (not #326)
   1.294 +#288 := (or #121 #648)
   1.295 +#305 := (iff #121 #326)
   1.296 +#21 := (:var 0 S3)
   1.297 +#19 := (:var 1 S3)
   1.298 +#20 := (f7 #19)
   1.299 +#22 := (f6 #20 #21)
   1.300 +#18 := (:var 2 S2)
   1.301 +#23 := (f3 #18 #22)
   1.302 +#664 := (pattern #23)
   1.303 +#27 := (f3 #18 #21)
   1.304 +#94 := (= f1 #27)
   1.305 +#25 := (f3 #18 #19)
   1.306 +#91 := (= f1 #25)
   1.307 +#97 := (or #91 #94)
   1.308 +#87 := (= f1 #23)
   1.309 +#100 := (iff #87 #97)
   1.310 +#665 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #664) #100)
   1.311 +#103 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #100)
   1.312 +#668 := (iff #103 #665)
   1.313 +#666 := (iff #100 #100)
   1.314 +#667 := [refl]: #666
   1.315 +#669 := [quant-intro #667]: #668
   1.316 +#146 := (~ #103 #103)
   1.317 +#160 := (~ #100 #100)
   1.318 +#161 := [refl]: #160
   1.319 +#147 := [nnf-pos #161]: #146
   1.320 +#28 := (= #27 f1)
   1.321 +#26 := (= #25 f1)
   1.322 +#29 := (or #26 #28)
   1.323 +#24 := (= #23 f1)
   1.324 +#30 := (iff #24 #29)
   1.325 +#31 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #30)
   1.326 +#104 := (iff #31 #103)
   1.327 +#101 := (iff #30 #100)
   1.328 +#98 := (iff #29 #97)
   1.329 +#95 := (iff #28 #94)
   1.330 +#96 := [rewrite]: #95
   1.331 +#92 := (iff #26 #91)
   1.332 +#93 := [rewrite]: #92
   1.333 +#99 := [monotonicity #93 #96]: #98
   1.334 +#89 := (iff #24 #87)
   1.335 +#90 := [rewrite]: #89
   1.336 +#102 := [monotonicity #90 #99]: #101
   1.337 +#105 := [quant-intro #102]: #104
   1.338 +#86 := [asserted]: #31
   1.339 +#108 := [mp #86 #105]: #103
   1.340 +#162 := [mp~ #108 #147]: #103
   1.341 +#670 := [mp #162 #669]: #665
   1.342 +#299 := (not #665)
   1.343 +#431 := (or #299 #305)
   1.344 +#638 := [quant-inst #39 #40 #9]: #431
   1.345 +#287 := [unit-resolution #638 #670]: #305
   1.346 +#639 := (not #305)
   1.347 +#297 := (or #639 #121 #648)
   1.348 +#302 := [def-axiom]: #297
   1.349 +#289 := [unit-resolution #302 #287]: #288
   1.350 +#627 := [unit-resolution #289 #642]: #648
   1.351 +#321 := (not #125)
   1.352 +#310 := (or #326 #321)
   1.353 +#311 := [def-axiom]: #310
   1.354 +#628 := [unit-resolution #311 #627 #644]: false
   1.355 +#629 := [lemma #628]: #121
   1.356 +#630 := (or #134 #326)
   1.357 +#640 := (or #639 #134 #326)
   1.358 +#298 := [def-axiom]: #640
   1.359 +#631 := [unit-resolution #298 #287]: #630
   1.360 +#633 := [unit-resolution #631 #629]: #326
   1.361 +#324 := (or #321 #134)
   1.362 +#312 := (or #321 #134 #232)
   1.363 +#323 := [def-axiom]: #312
   1.364 +#252 := [unit-resolution #323 #142]: #324
   1.365 +#635 := [unit-resolution #252 #629]: #321
   1.366 +#643 := (or #648 #125 #322)
   1.367 +#649 := [def-axiom]: #643
   1.368 +#273 := [unit-resolution #649 #635 #633]: #322
   1.369 +#8 := (:var 0 S2)
   1.370 +#10 := (f3 #8 f4)
   1.371 +#650 := (pattern #10)
   1.372 +#69 := (= f1 #10)
   1.373 +#72 := (not #69)
   1.374 +#651 := (forall (vars (?v0 S2)) (:pat #650) #72)
   1.375 +#75 := (forall (vars (?v0 S2)) #72)
   1.376 +#654 := (iff #75 #651)
   1.377 +#652 := (iff #72 #72)
   1.378 +#653 := [refl]: #652
   1.379 +#655 := [quant-intro #653]: #654
   1.380 +#156 := (~ #75 #75)
   1.381 +#154 := (~ #72 #72)
   1.382 +#155 := [refl]: #154
   1.383 +#157 := [nnf-pos #155]: #156
   1.384 +#11 := (= #10 f1)
   1.385 +#12 := (not #11)
   1.386 +#13 := (forall (vars (?v0 S2)) #12)
   1.387 +#76 := (iff #13 #75)
   1.388 +#73 := (iff #12 #72)
   1.389 +#70 := (iff #11 #69)
   1.390 +#71 := [rewrite]: #70
   1.391 +#74 := [monotonicity #71]: #73
   1.392 +#77 := [quant-intro #74]: #76
   1.393 +#68 := [asserted]: #13
   1.394 +#80 := [mp #68 #77]: #75
   1.395 +#141 := [mp~ #80 #157]: #75
   1.396 +#656 := [mp #141 #655]: #651
   1.397 +#645 := (not #322)
   1.398 +#626 := (not #651)
   1.399 +#632 := (or #626 #645)
   1.400 +#268 := [quant-inst #39]: #632
   1.401 +[unit-resolution #268 #656 #273]: false
   1.402 +unsat
   1.403 +37e8c2c682de93175c2e3b6573d2a98ccec54dc2 134 0
   1.404 +#2 := false
   1.405 +decl f3 :: (-> S2 S3 S1)
   1.406 +decl f5 :: S3
   1.407 +#14 := f5
   1.408 +decl f9 :: S2
   1.409 +#39 := f9
   1.410 +#217 := (f3 f9 f5)
   1.411 +decl f1 :: S1
   1.412 +#4 := f1
   1.413 +#304 := (= f1 #217)
   1.414 +#631 := (not #304)
   1.415 +decl f10 :: S3
   1.416 +#40 := f10
   1.417 +#218 := (f3 f9 f10)
   1.418 +#305 := (= f1 #218)
   1.419 +#297 := (or #304 #305)
   1.420 +#282 := (not #297)
   1.421 +decl f6 :: (-> S4 S3 S3)
   1.422 +decl f7 :: (-> S3 S4)
   1.423 +#41 := (f7 f10)
   1.424 +#42 := (f6 #41 f5)
   1.425 +#43 := (f3 f9 #42)
   1.426 +#118 := (= f1 #43)
   1.427 +#237 := (iff #118 #297)
   1.428 +#21 := (:var 0 S3)
   1.429 +#19 := (:var 1 S3)
   1.430 +#20 := (f7 #19)
   1.431 +#22 := (f6 #20 #21)
   1.432 +#18 := (:var 2 S2)
   1.433 +#23 := (f3 #18 #22)
   1.434 +#649 := (pattern #23)
   1.435 +#27 := (f3 #18 #21)
   1.436 +#91 := (= f1 #27)
   1.437 +#25 := (f3 #18 #19)
   1.438 +#88 := (= f1 #25)
   1.439 +#94 := (or #88 #91)
   1.440 +#84 := (= f1 #23)
   1.441 +#97 := (iff #84 #94)
   1.442 +#650 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #649) #97)
   1.443 +#100 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #97)
   1.444 +#653 := (iff #100 #650)
   1.445 +#651 := (iff #97 #97)
   1.446 +#652 := [refl]: #651
   1.447 +#654 := [quant-intro #652]: #653
   1.448 +#131 := (~ #100 #100)
   1.449 +#145 := (~ #97 #97)
   1.450 +#146 := [refl]: #145
   1.451 +#132 := [nnf-pos #146]: #131
   1.452 +#28 := (= #27 f1)
   1.453 +#26 := (= #25 f1)
   1.454 +#29 := (or #26 #28)
   1.455 +#24 := (= #23 f1)
   1.456 +#30 := (iff #24 #29)
   1.457 +#31 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #30)
   1.458 +#101 := (iff #31 #100)
   1.459 +#98 := (iff #30 #97)
   1.460 +#95 := (iff #29 #94)
   1.461 +#92 := (iff #28 #91)
   1.462 +#93 := [rewrite]: #92
   1.463 +#89 := (iff #26 #88)
   1.464 +#90 := [rewrite]: #89
   1.465 +#96 := [monotonicity #90 #93]: #95
   1.466 +#86 := (iff #24 #84)
   1.467 +#87 := [rewrite]: #86
   1.468 +#99 := [monotonicity #87 #96]: #98
   1.469 +#102 := [quant-intro #99]: #101
   1.470 +#83 := [asserted]: #31
   1.471 +#105 := [mp #83 #102]: #100
   1.472 +#147 := [mp~ #105 #132]: #100
   1.473 +#655 := [mp #147 #654]: #650
   1.474 +#311 := (not #650)
   1.475 +#290 := (or #311 #237)
   1.476 +#219 := (or #305 #304)
   1.477 +#306 := (iff #118 #219)
   1.478 +#627 := (or #311 #306)
   1.479 +#284 := (iff #627 #290)
   1.480 +#623 := (iff #290 #290)
   1.481 +#295 := [rewrite]: #623
   1.482 +#310 := (iff #306 #237)
   1.483 +#308 := (iff #219 #297)
   1.484 +#309 := [rewrite]: #308
   1.485 +#307 := [monotonicity #309]: #310
   1.486 +#416 := [monotonicity #307]: #284
   1.487 +#296 := [trans #416 #295]: #284
   1.488 +#629 := [quant-inst #39 #40 #14]: #627
   1.489 +#630 := [mp #629 #296]: #290
   1.490 +#613 := [unit-resolution #630 #655]: #237
   1.491 +#283 := (not #237)
   1.492 +#614 := (or #283 #282)
   1.493 +#122 := (not #118)
   1.494 +#44 := (= #43 f1)
   1.495 +#45 := (not #44)
   1.496 +#123 := (iff #45 #122)
   1.497 +#120 := (iff #44 #118)
   1.498 +#121 := [rewrite]: #120
   1.499 +#124 := [monotonicity #121]: #123
   1.500 +#117 := [asserted]: #45
   1.501 +#127 := [mp #117 #124]: #122
   1.502 +#626 := (or #283 #118 #282)
   1.503 +#267 := [def-axiom]: #626
   1.504 +#617 := [unit-resolution #267 #127]: #614
   1.505 +#253 := [unit-resolution #617 #613]: #282
   1.506 +#632 := (or #297 #631)
   1.507 +#633 := [def-axiom]: #632
   1.508 +#618 := [unit-resolution #633 #253]: #631
   1.509 +#8 := (:var 0 S2)
   1.510 +#15 := (f3 #8 f5)
   1.511 +#642 := (pattern #15)
   1.512 +#76 := (= f1 #15)
   1.513 +#643 := (forall (vars (?v0 S2)) (:pat #642) #76)
   1.514 +#80 := (forall (vars (?v0 S2)) #76)
   1.515 +#646 := (iff #80 #643)
   1.516 +#644 := (iff #76 #76)
   1.517 +#645 := [refl]: #644
   1.518 +#647 := [quant-intro #645]: #646
   1.519 +#129 := (~ #80 #80)
   1.520 +#128 := (~ #76 #76)
   1.521 +#143 := [refl]: #128
   1.522 +#130 := [nnf-pos #143]: #129
   1.523 +#16 := (= #15 f1)
   1.524 +#17 := (forall (vars (?v0 S2)) #16)
   1.525 +#81 := (iff #17 #80)
   1.526 +#78 := (iff #16 #76)
   1.527 +#79 := [rewrite]: #78
   1.528 +#82 := [quant-intro #79]: #81
   1.529 +#75 := [asserted]: #17
   1.530 +#85 := [mp #75 #82]: #80
   1.531 +#144 := [mp~ #85 #130]: #80
   1.532 +#648 := [mp #144 #647]: #643
   1.533 +#615 := (not #643)
   1.534 +#616 := (or #615 #304)
   1.535 +#611 := [quant-inst #39]: #616
   1.536 +[unit-resolution #611 #648 #618]: false
   1.537 +unsat
   1.538 +8b3671158912b5be83077a5d2f71eae8a40f4427 153 0
   1.539 +#2 := false
   1.540 +decl f3 :: (-> S2 S3 S1)
   1.541 +decl f6 :: (-> S4 S3 S3)
   1.542 +decl f10 :: S3
   1.543 +#40 := f10
   1.544 +decl f7 :: (-> S3 S4)
   1.545 +decl f11 :: S3
   1.546 +#42 := f11
   1.547 +#46 := (f7 f11)
   1.548 +#47 := (f6 #46 f10)
   1.549 +decl f9 :: S2
   1.550 +#39 := f9
   1.551 +#48 := (f3 f9 #47)
   1.552 +decl f1 :: S1
   1.553 +#4 := f1
   1.554 +#128 := (= f1 #48)
   1.555 +#324 := (not #128)
   1.556 +#41 := (f7 f10)
   1.557 +#43 := (f6 #41 f11)
   1.558 +#44 := (f3 f9 #43)
   1.559 +#124 := (= f1 #44)
   1.560 +#137 := (not #124)
   1.561 +#243 := [hypothesis]: #137
   1.562 +#323 := (or #128 #124)
   1.563 +#138 := (iff #128 #137)
   1.564 +#49 := (= #48 f1)
   1.565 +#45 := (= #44 f1)
   1.566 +#50 := (iff #45 #49)
   1.567 +#51 := (not #50)
   1.568 +#141 := (iff #51 #138)
   1.569 +#131 := (iff #124 #128)
   1.570 +#134 := (not #131)
   1.571 +#139 := (iff #134 #138)
   1.572 +#140 := [rewrite]: #139
   1.573 +#135 := (iff #51 #134)
   1.574 +#132 := (iff #50 #131)
   1.575 +#129 := (iff #49 #128)
   1.576 +#130 := [rewrite]: #129
   1.577 +#126 := (iff #45 #124)
   1.578 +#127 := [rewrite]: #126
   1.579 +#133 := [monotonicity #127 #130]: #132
   1.580 +#136 := [monotonicity #133]: #135
   1.581 +#142 := [trans #136 #140]: #141
   1.582 +#123 := [asserted]: #51
   1.583 +#145 := [mp #123 #142]: #138
   1.584 +#235 := (not #138)
   1.585 +#322 := (or #128 #124 #235)
   1.586 +#236 := [def-axiom]: #322
   1.587 +#237 := [unit-resolution #236 #145]: #323
   1.588 +#622 := [unit-resolution #237 #243]: #128
   1.589 +#328 := (f3 f9 f10)
   1.590 +#325 := (= f1 #328)
   1.591 +#329 := (f3 f9 f11)
   1.592 +#308 := (= f1 #329)
   1.593 +#645 := (or #308 #325)
   1.594 +#642 := (not #645)
   1.595 +#345 := (or #124 #642)
   1.596 +#632 := (iff #124 #645)
   1.597 +#21 := (:var 0 S3)
   1.598 +#19 := (:var 1 S3)
   1.599 +#20 := (f7 #19)
   1.600 +#22 := (f6 #20 #21)
   1.601 +#18 := (:var 2 S2)
   1.602 +#23 := (f3 #18 #22)
   1.603 +#667 := (pattern #23)
   1.604 +#27 := (f3 #18 #21)
   1.605 +#97 := (= f1 #27)
   1.606 +#25 := (f3 #18 #19)
   1.607 +#94 := (= f1 #25)
   1.608 +#100 := (or #94 #97)
   1.609 +#90 := (= f1 #23)
   1.610 +#103 := (iff #90 #100)
   1.611 +#668 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #667) #103)
   1.612 +#106 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #103)
   1.613 +#671 := (iff #106 #668)
   1.614 +#669 := (iff #103 #103)
   1.615 +#670 := [refl]: #669
   1.616 +#672 := [quant-intro #670]: #671
   1.617 +#149 := (~ #106 #106)
   1.618 +#163 := (~ #103 #103)
   1.619 +#164 := [refl]: #163
   1.620 +#150 := [nnf-pos #164]: #149
   1.621 +#28 := (= #27 f1)
   1.622 +#26 := (= #25 f1)
   1.623 +#29 := (or #26 #28)
   1.624 +#24 := (= #23 f1)
   1.625 +#30 := (iff #24 #29)
   1.626 +#31 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #30)
   1.627 +#107 := (iff #31 #106)
   1.628 +#104 := (iff #30 #103)
   1.629 +#101 := (iff #29 #100)
   1.630 +#98 := (iff #28 #97)
   1.631 +#99 := [rewrite]: #98
   1.632 +#95 := (iff #26 #94)
   1.633 +#96 := [rewrite]: #95
   1.634 +#102 := [monotonicity #96 #99]: #101
   1.635 +#92 := (iff #24 #90)
   1.636 +#93 := [rewrite]: #92
   1.637 +#105 := [monotonicity #93 #102]: #104
   1.638 +#108 := [quant-intro #105]: #107
   1.639 +#89 := [asserted]: #31
   1.640 +#111 := [mp #89 #108]: #106
   1.641 +#165 := [mp~ #111 #150]: #106
   1.642 +#673 := [mp #165 #672]: #668
   1.643 +#641 := (not #668)
   1.644 +#629 := (or #641 #632)
   1.645 +#302 := (or #325 #308)
   1.646 +#434 := (iff #124 #302)
   1.647 +#635 := (or #641 #434)
   1.648 +#636 := (iff #635 #629)
   1.649 +#276 := (iff #629 #629)
   1.650 +#277 := [rewrite]: #276
   1.651 +#633 := (iff #434 #632)
   1.652 +#630 := (iff #302 #645)
   1.653 +#631 := [rewrite]: #630
   1.654 +#634 := [monotonicity #631]: #633
   1.655 +#638 := [monotonicity #634]: #636
   1.656 +#639 := [trans #638 #277]: #636
   1.657 +#271 := [quant-inst #39 #40 #42]: #635
   1.658 +#637 := [mp #271 #639]: #629
   1.659 +#623 := [unit-resolution #637 #673]: #632
   1.660 +#640 := (not #632)
   1.661 +#626 := (or #640 #124 #642)
   1.662 +#627 := [def-axiom]: #626
   1.663 +#346 := [unit-resolution #627 #623]: #345
   1.664 +#620 := [unit-resolution #346 #243]: #642
   1.665 +#621 := (or #324 #645)
   1.666 +#647 := (iff #128 #645)
   1.667 +#313 := (or #641 #647)
   1.668 +#314 := [quant-inst #39 #42 #40]: #313
   1.669 +#624 := [unit-resolution #314 #673]: #647
   1.670 +#643 := (not #647)
   1.671 +#285 := (or #643 #324 #645)
   1.672 +#628 := [def-axiom]: #285
   1.673 +#625 := [unit-resolution #628 #624]: #621
   1.674 +#334 := [unit-resolution #625 #620 #622]: false
   1.675 +#335 := [lemma #334]: #124
   1.676 +#327 := (or #324 #137)
   1.677 +#315 := (or #324 #137 #235)
   1.678 +#326 := [def-axiom]: #315
   1.679 +#255 := [unit-resolution #326 #145]: #327
   1.680 +#336 := [unit-resolution #255 #335]: #324
   1.681 +#338 := (or #137 #645)
   1.682 +#333 := (or #640 #137 #645)
   1.683 +#349 := [def-axiom]: #333
   1.684 +#616 := [unit-resolution #349 #623]: #338
   1.685 +#617 := [unit-resolution #616 #335]: #645
   1.686 +#330 := (or #128 #642)
   1.687 +#301 := (or #643 #128 #642)
   1.688 +#644 := [def-axiom]: #301
   1.689 +#614 := [unit-resolution #644 #624]: #330
   1.690 +[unit-resolution #614 #617 #336]: false
   1.691 +unsat
   1.692 +76f35b24758dff3b162e8fc64fc760da00fb55d8 126 0
   1.693 +#2 := false
   1.694 +decl f3 :: (-> S2 S3 S1)
   1.695 +decl f6 :: (-> S4 S3 S3)
   1.696 +decl f10 :: S3
   1.697 +#40 := f10
   1.698 +decl f7 :: (-> S3 S4)
   1.699 +#41 := (f7 f10)
   1.700 +#42 := (f6 #41 f10)
   1.701 +decl f9 :: S2
   1.702 +#39 := f9
   1.703 +#43 := (f3 f9 #42)
   1.704 +decl f1 :: S1
   1.705 +#4 := f1
   1.706 +#121 := (= f1 #43)
   1.707 +#134 := (not #121)
   1.708 +#625 := [hypothesis]: #134
   1.709 +#45 := (f3 f9 f10)
   1.710 +#125 := (= f1 #45)
   1.711 +#320 := (or #125 #121)
   1.712 +#135 := (iff #125 #134)
   1.713 +#46 := (= #45 f1)
   1.714 +#44 := (= #43 f1)
   1.715 +#47 := (iff #44 #46)
   1.716 +#48 := (not #47)
   1.717 +#138 := (iff #48 #135)
   1.718 +#128 := (iff #121 #125)
   1.719 +#131 := (not #128)
   1.720 +#136 := (iff #131 #135)
   1.721 +#137 := [rewrite]: #136
   1.722 +#132 := (iff #48 #131)
   1.723 +#129 := (iff #47 #128)
   1.724 +#126 := (iff #46 #125)
   1.725 +#127 := [rewrite]: #126
   1.726 +#123 := (iff #44 #121)
   1.727 +#124 := [rewrite]: #123
   1.728 +#130 := [monotonicity #124 #127]: #129
   1.729 +#133 := [monotonicity #130]: #132
   1.730 +#139 := [trans #133 #137]: #138
   1.731 +#120 := [asserted]: #48
   1.732 +#142 := [mp #120 #139]: #135
   1.733 +#232 := (not #135)
   1.734 +#319 := (or #125 #121 #232)
   1.735 +#233 := [def-axiom]: #319
   1.736 +#234 := [unit-resolution #233 #142]: #320
   1.737 +#286 := [unit-resolution #234 #625]: #125
   1.738 +#321 := (not #125)
   1.739 +#288 := (or #121 #321)
   1.740 +#21 := (:var 0 S3)
   1.741 +#19 := (:var 1 S3)
   1.742 +#20 := (f7 #19)
   1.743 +#22 := (f6 #20 #21)
   1.744 +#18 := (:var 2 S2)
   1.745 +#23 := (f3 #18 #22)
   1.746 +#664 := (pattern #23)
   1.747 +#27 := (f3 #18 #21)
   1.748 +#94 := (= f1 #27)
   1.749 +#25 := (f3 #18 #19)
   1.750 +#91 := (= f1 #25)
   1.751 +#97 := (or #91 #94)
   1.752 +#87 := (= f1 #23)
   1.753 +#100 := (iff #87 #97)
   1.754 +#665 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #664) #100)
   1.755 +#103 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #100)
   1.756 +#668 := (iff #103 #665)
   1.757 +#666 := (iff #100 #100)
   1.758 +#667 := [refl]: #666
   1.759 +#669 := [quant-intro #667]: #668
   1.760 +#146 := (~ #103 #103)
   1.761 +#160 := (~ #100 #100)
   1.762 +#161 := [refl]: #160
   1.763 +#147 := [nnf-pos #161]: #146
   1.764 +#28 := (= #27 f1)
   1.765 +#26 := (= #25 f1)
   1.766 +#29 := (or #26 #28)
   1.767 +#24 := (= #23 f1)
   1.768 +#30 := (iff #24 #29)
   1.769 +#31 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #30)
   1.770 +#104 := (iff #31 #103)
   1.771 +#101 := (iff #30 #100)
   1.772 +#98 := (iff #29 #97)
   1.773 +#95 := (iff #28 #94)
   1.774 +#96 := [rewrite]: #95
   1.775 +#92 := (iff #26 #91)
   1.776 +#93 := [rewrite]: #92
   1.777 +#99 := [monotonicity #93 #96]: #98
   1.778 +#89 := (iff #24 #87)
   1.779 +#90 := [rewrite]: #89
   1.780 +#102 := [monotonicity #90 #99]: #101
   1.781 +#105 := [quant-intro #102]: #104
   1.782 +#86 := [asserted]: #31
   1.783 +#108 := [mp #86 #105]: #103
   1.784 +#162 := [mp~ #108 #147]: #103
   1.785 +#670 := [mp #162 #669]: #665
   1.786 +#299 := (not #665)
   1.787 +#431 := (or #299 #128)
   1.788 +#325 := (or #125 #125)
   1.789 +#322 := (iff #121 #325)
   1.790 +#638 := (or #299 #322)
   1.791 +#311 := (iff #638 #431)
   1.792 +#646 := (iff #431 #431)
   1.793 +#647 := [rewrite]: #646
   1.794 +#642 := (iff #322 #128)
   1.795 +#326 := (iff #325 #125)
   1.796 +#305 := [rewrite]: #326
   1.797 +#644 := [monotonicity #305]: #642
   1.798 +#645 := [monotonicity #644]: #311
   1.799 +#648 := [trans #645 #647]: #311
   1.800 +#310 := [quant-inst #39 #40 #40]: #638
   1.801 +#643 := [mp #310 #648]: #431
   1.802 +#287 := [unit-resolution #643 #670]: #128
   1.803 +#649 := (or #131 #121 #321)
   1.804 +#639 := [def-axiom]: #649
   1.805 +#289 := [unit-resolution #639 #287]: #288
   1.806 +#627 := [unit-resolution #289 #286 #625]: false
   1.807 +#628 := [lemma #627]: #121
   1.808 +#324 := (or #321 #134)
   1.809 +#312 := (or #321 #134 #232)
   1.810 +#323 := [def-axiom]: #312
   1.811 +#252 := [unit-resolution #323 #142]: #324
   1.812 +#629 := [unit-resolution #252 #628]: #321
   1.813 +#630 := (or #134 #125)
   1.814 +#297 := (or #131 #134 #125)
   1.815 +#302 := [def-axiom]: #297
   1.816 +#631 := [unit-resolution #302 #287]: #630
   1.817 +[unit-resolution #631 #629 #628]: false
   1.818 +unsat
   1.819 +2ac06f7d84c36d7f3c61e2f783f6f8bf82530665 264 0
   1.820 +#2 := false
   1.821 +decl f3 :: (-> S2 S3 S1)
   1.822 +decl f11 :: S3
   1.823 +#42 := f11
   1.824 +decl f9 :: S2
   1.825 +#39 := f9
   1.826 +#621 := (f3 f9 f11)
   1.827 +decl f1 :: S1
   1.828 +#4 := f1
   1.829 +#334 := (= f1 #621)
   1.830 +decl f12 :: S3
   1.831 +#44 := f12
   1.832 +#332 := (f3 f9 f12)
   1.833 +#329 := (= f1 #332)
   1.834 +#619 := (or #329 #334)
   1.835 +decl f6 :: (-> S4 S3 S3)
   1.836 +decl f7 :: (-> S3 S4)
   1.837 +#43 := (f7 f11)
   1.838 +#45 := (f6 #43 f12)
   1.839 +#306 := (f3 f9 #45)
   1.840 +#438 := (= f1 #306)
   1.841 +#613 := (iff #438 #619)
   1.842 +#579 := (not #613)
   1.843 +#591 := (not #619)
   1.844 +#603 := (not #334)
   1.845 +decl f10 :: S3
   1.846 +#40 := f10
   1.847 +#634 := (f3 f9 f10)
   1.848 +#635 := (= f1 #634)
   1.849 +#481 := (or #334 #635)
   1.850 +#606 := (not #481)
   1.851 +#41 := (f7 f10)
   1.852 +#49 := (f6 #41 f11)
   1.853 +#333 := (f3 f9 #49)
   1.854 +#312 := (= f1 #333)
   1.855 +#589 := (iff #312 #481)
   1.856 +#581 := (not #589)
   1.857 +#574 := [hypothesis]: #581
   1.858 +#21 := (:var 0 S3)
   1.859 +#19 := (:var 1 S3)
   1.860 +#20 := (f7 #19)
   1.861 +#22 := (f6 #20 #21)
   1.862 +#18 := (:var 2 S2)
   1.863 +#23 := (f3 #18 #22)
   1.864 +#671 := (pattern #23)
   1.865 +#27 := (f3 #18 #21)
   1.866 +#101 := (= f1 #27)
   1.867 +#25 := (f3 #18 #19)
   1.868 +#98 := (= f1 #25)
   1.869 +#104 := (or #98 #101)
   1.870 +#94 := (= f1 #23)
   1.871 +#107 := (iff #94 #104)
   1.872 +#672 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #671) #107)
   1.873 +#110 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #107)
   1.874 +#675 := (iff #110 #672)
   1.875 +#673 := (iff #107 #107)
   1.876 +#674 := [refl]: #673
   1.877 +#676 := [quant-intro #674]: #675
   1.878 +#153 := (~ #110 #110)
   1.879 +#167 := (~ #107 #107)
   1.880 +#168 := [refl]: #167
   1.881 +#154 := [nnf-pos #168]: #153
   1.882 +#28 := (= #27 f1)
   1.883 +#26 := (= #25 f1)
   1.884 +#29 := (or #26 #28)
   1.885 +#24 := (= #23 f1)
   1.886 +#30 := (iff #24 #29)
   1.887 +#31 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #30)
   1.888 +#111 := (iff #31 #110)
   1.889 +#108 := (iff #30 #107)
   1.890 +#105 := (iff #29 #104)
   1.891 +#102 := (iff #28 #101)
   1.892 +#103 := [rewrite]: #102
   1.893 +#99 := (iff #26 #98)
   1.894 +#100 := [rewrite]: #99
   1.895 +#106 := [monotonicity #100 #103]: #105
   1.896 +#96 := (iff #24 #94)
   1.897 +#97 := [rewrite]: #96
   1.898 +#109 := [monotonicity #97 #106]: #108
   1.899 +#112 := [quant-intro #109]: #111
   1.900 +#93 := [asserted]: #31
   1.901 +#115 := [mp #93 #112]: #110
   1.902 +#169 := [mp~ #115 #154]: #110
   1.903 +#677 := [mp #169 #676]: #672
   1.904 +#645 := (not #672)
   1.905 +#587 := (or #645 #589)
   1.906 +#598 := (or #635 #334)
   1.907 +#480 := (iff #312 #598)
   1.908 +#590 := (or #645 #480)
   1.909 +#490 := (iff #590 #587)
   1.910 +#493 := (iff #587 #587)
   1.911 +#486 := [rewrite]: #493
   1.912 +#491 := (iff #480 #589)
   1.913 +#482 := (iff #598 #481)
   1.914 +#441 := [rewrite]: #482
   1.915 +#586 := [monotonicity #441]: #491
   1.916 +#492 := [monotonicity #586]: #490
   1.917 +#494 := [trans #492 #486]: #490
   1.918 +#475 := [quant-inst #39 #40 #42]: #590
   1.919 +#495 := [mp #475 #494]: #587
   1.920 +#575 := [unit-resolution #495 #677 #574]: false
   1.921 +#576 := [lemma #575]: #589
   1.922 +#652 := (not #312)
   1.923 +#649 := (or #312 #329)
   1.924 +#646 := (not #649)
   1.925 +#50 := (f7 #49)
   1.926 +#51 := (f6 #50 f12)
   1.927 +#52 := (f3 f9 #51)
   1.928 +#132 := (= f1 #52)
   1.929 +#328 := (not #132)
   1.930 +#46 := (f6 #41 #45)
   1.931 +#47 := (f3 f9 #46)
   1.932 +#128 := (= f1 #47)
   1.933 +#141 := (not #128)
   1.934 +#577 := [hypothesis]: #141
   1.935 +#327 := (or #132 #128)
   1.936 +#142 := (iff #132 #141)
   1.937 +#53 := (= #52 f1)
   1.938 +#48 := (= #47 f1)
   1.939 +#54 := (iff #48 #53)
   1.940 +#55 := (not #54)
   1.941 +#145 := (iff #55 #142)
   1.942 +#135 := (iff #128 #132)
   1.943 +#138 := (not #135)
   1.944 +#143 := (iff #138 #142)
   1.945 +#144 := [rewrite]: #143
   1.946 +#139 := (iff #55 #138)
   1.947 +#136 := (iff #54 #135)
   1.948 +#133 := (iff #53 #132)
   1.949 +#134 := [rewrite]: #133
   1.950 +#130 := (iff #48 #128)
   1.951 +#131 := [rewrite]: #130
   1.952 +#137 := [monotonicity #131 #134]: #136
   1.953 +#140 := [monotonicity #137]: #139
   1.954 +#146 := [trans #140 #144]: #145
   1.955 +#127 := [asserted]: #55
   1.956 +#149 := [mp #127 #146]: #142
   1.957 +#239 := (not #142)
   1.958 +#326 := (or #132 #128 #239)
   1.959 +#240 := [def-axiom]: #326
   1.960 +#241 := [unit-resolution #240 #149]: #327
   1.961 +#571 := [unit-resolution #241 #577]: #132
   1.962 +#562 := (or #328 #649)
   1.963 +#651 := (iff #132 #649)
   1.964 +#317 := (or #645 #651)
   1.965 +#318 := [quant-inst #39 #49 #44]: #317
   1.966 +#578 := [unit-resolution #318 #677]: #651
   1.967 +#647 := (not #651)
   1.968 +#289 := (or #647 #328 #649)
   1.969 +#632 := [def-axiom]: #289
   1.970 +#563 := [unit-resolution #632 #578]: #562
   1.971 +#565 := [unit-resolution #563 #571]: #649
   1.972 +#655 := (not #329)
   1.973 +#595 := (or #645 #613)
   1.974 +#618 := (or #334 #329)
   1.975 +#622 := (iff #438 #618)
   1.976 +#615 := (or #645 #622)
   1.977 +#610 := (iff #615 #595)
   1.978 +#617 := (iff #595 #595)
   1.979 +#458 := [rewrite]: #617
   1.980 +#614 := (iff #622 #613)
   1.981 +#623 := (iff #618 #619)
   1.982 +#612 := [rewrite]: #623
   1.983 +#609 := [monotonicity #612]: #614
   1.984 +#611 := [monotonicity #609]: #610
   1.985 +#459 := [trans #611 #458]: #610
   1.986 +#616 := [quant-inst #39 #42 #44]: #615
   1.987 +#460 := [mp #616 #459]: #595
   1.988 +#566 := [unit-resolution #460 #677]: #613
   1.989 +#556 := (or #579 #591)
   1.990 +#354 := (not #438)
   1.991 +#638 := (or #438 #635)
   1.992 +#627 := (not #638)
   1.993 +#568 := (or #128 #627)
   1.994 +#275 := (iff #128 #638)
   1.995 +#280 := (or #645 #275)
   1.996 +#636 := (or #635 #438)
   1.997 +#637 := (iff #128 #636)
   1.998 +#281 := (or #645 #637)
   1.999 +#641 := (iff #281 #280)
  1.1000 +#630 := (iff #280 #280)
  1.1001 +#631 := [rewrite]: #630
  1.1002 +#640 := (iff #637 #275)
  1.1003 +#633 := (iff #636 #638)
  1.1004 +#639 := [rewrite]: #633
  1.1005 +#642 := [monotonicity #639]: #640
  1.1006 +#644 := [monotonicity #642]: #641
  1.1007 +#337 := [trans #644 #631]: #641
  1.1008 +#643 := [quant-inst #39 #40 #45]: #281
  1.1009 +#353 := [mp #643 #337]: #280
  1.1010 +#567 := [unit-resolution #353 #677]: #275
  1.1011 +#624 := (not #275)
  1.1012 +#628 := (or #624 #128 #627)
  1.1013 +#625 := [def-axiom]: #628
  1.1014 +#564 := [unit-resolution #625 #567]: #568
  1.1015 +#569 := [unit-resolution #564 #577]: #627
  1.1016 +#355 := (or #638 #354)
  1.1017 +#341 := [def-axiom]: #355
  1.1018 +#555 := [unit-resolution #341 #569]: #354
  1.1019 +#573 := (or #579 #438 #591)
  1.1020 +#570 := [def-axiom]: #573
  1.1021 +#558 := [unit-resolution #570 #555]: #556
  1.1022 +#559 := [unit-resolution #558 #566]: #591
  1.1023 +#602 := (or #619 #655)
  1.1024 +#496 := [def-axiom]: #602
  1.1025 +#560 := [unit-resolution #496 #559]: #655
  1.1026 +#304 := (or #646 #312 #329)
  1.1027 +#309 := [def-axiom]: #304
  1.1028 +#557 := [unit-resolution #309 #560 #565]: #312
  1.1029 +#356 := (not #635)
  1.1030 +#247 := (or #638 #356)
  1.1031 +#626 := [def-axiom]: #247
  1.1032 +#561 := [unit-resolution #626 #569]: #356
  1.1033 +#497 := (or #619 #603)
  1.1034 +#498 := [def-axiom]: #497
  1.1035 +#541 := [unit-resolution #498 #559]: #603
  1.1036 +#607 := (or #606 #334 #635)
  1.1037 +#601 := [def-axiom]: #607
  1.1038 +#542 := [unit-resolution #601 #541 #561]: #606
  1.1039 +#439 := (or #581 #652 #481)
  1.1040 +#440 := [def-axiom]: #439
  1.1041 +#544 := [unit-resolution #440 #542 #557 #576]: false
  1.1042 +#545 := [lemma #544]: #128
  1.1043 +#331 := (or #328 #141)
  1.1044 +#319 := (or #328 #141 #239)
  1.1045 +#330 := [def-axiom]: #319
  1.1046 +#259 := [unit-resolution #330 #149]: #331
  1.1047 +#546 := [unit-resolution #259 #545]: #328
  1.1048 +#547 := (or #132 #646)
  1.1049 +#305 := (or #647 #132 #646)
  1.1050 +#648 := [def-axiom]: #305
  1.1051 +#548 := [unit-resolution #648 #578]: #547
  1.1052 +#549 := [unit-resolution #548 #546]: #646
  1.1053 +#653 := (or #649 #652)
  1.1054 +#654 := [def-axiom]: #653
  1.1055 +#550 := [unit-resolution #654 #549]: #652
  1.1056 +#608 := (or #581 #312 #606)
  1.1057 +#437 := [def-axiom]: #608
  1.1058 +#551 := [unit-resolution #437 #550 #576]: #606
  1.1059 +#604 := (or #481 #603)
  1.1060 +#605 := [def-axiom]: #604
  1.1061 +#552 := [unit-resolution #605 #551]: #603
  1.1062 +#650 := (or #649 #655)
  1.1063 +#656 := [def-axiom]: #650
  1.1064 +#553 := [unit-resolution #656 #549]: #655
  1.1065 +#588 := (or #591 #329 #334)
  1.1066 +#592 := [def-axiom]: #588
  1.1067 +#543 := [unit-resolution #592 #553 #552]: #591
  1.1068 +#554 := (or #141 #638)
  1.1069 +#629 := (or #624 #141 #638)
  1.1070 +#338 := [def-axiom]: #629
  1.1071 +#532 := [unit-resolution #338 #567]: #554
  1.1072 +#533 := [unit-resolution #532 #545]: #638
  1.1073 +#599 := (or #481 #356)
  1.1074 +#600 := [def-axiom]: #599
  1.1075 +#535 := [unit-resolution #600 #551]: #356
  1.1076 +#349 := (or #627 #438 #635)
  1.1077 +#350 := [def-axiom]: #349
  1.1078 +#536 := [unit-resolution #350 #535 #533]: #438
  1.1079 +#572 := (or #579 #354 #619)
  1.1080 +#582 := [def-axiom]: #572
  1.1081 +#537 := [unit-resolution #582 #536 #543]: #579
  1.1082 +[unit-resolution #460 #677 #537]: false
  1.1083 +unsat
  1.1084 +95f37b9506ab4a9ecf6e4bca8da6ce25960cec6d 158 0
  1.1085 +#2 := false
  1.1086 +decl f3 :: (-> S2 S3 S1)
  1.1087 +decl f11 :: S3
  1.1088 +#42 := f11
  1.1089 +decl f9 :: S2
  1.1090 +#39 := f9
  1.1091 +#48 := (f3 f9 f11)
  1.1092 +decl f1 :: S1
  1.1093 +#4 := f1
  1.1094 +#132 := (= f1 #48)
  1.1095 +#186 := (not #132)
  1.1096 +decl f10 :: S3
  1.1097 +#40 := f10
  1.1098 +#46 := (f3 f9 f10)
  1.1099 +#129 := (= f1 #46)
  1.1100 +#185 := (not #129)
  1.1101 +#187 := (or #185 #186)
  1.1102 +#188 := (not #187)
  1.1103 +#329 := [hypothesis]: #188
  1.1104 +decl f6 :: (-> S4 S3 S3)
  1.1105 +decl f8 :: (-> S3 S4)
  1.1106 +#41 := (f8 f10)
  1.1107 +#43 := (f6 #41 f11)
  1.1108 +#44 := (f3 f9 #43)
  1.1109 +#125 := (= f1 #44)
  1.1110 +#144 := (not #125)
  1.1111 +#335 := (or #144 #187)
  1.1112 +#199 := (iff #125 #187)
  1.1113 +#135 := (and #129 #132)
  1.1114 +#145 := (iff #135 #144)
  1.1115 +#202 := (iff #145 #199)
  1.1116 +#194 := (iff #187 #125)
  1.1117 +#200 := (iff #194 #199)
  1.1118 +#201 := [rewrite]: #200
  1.1119 +#197 := (iff #145 #194)
  1.1120 +#191 := (iff #188 #144)
  1.1121 +#195 := (iff #191 #194)
  1.1122 +#196 := [rewrite]: #195
  1.1123 +#192 := (iff #145 #191)
  1.1124 +#189 := (iff #135 #188)
  1.1125 +#190 := [rewrite]: #189
  1.1126 +#193 := [monotonicity #190]: #192
  1.1127 +#198 := [trans #193 #196]: #197
  1.1128 +#203 := [trans #198 #201]: #202
  1.1129 +#49 := (= #48 f1)
  1.1130 +#47 := (= #46 f1)
  1.1131 +#50 := (and #47 #49)
  1.1132 +#45 := (= #44 f1)
  1.1133 +#51 := (iff #45 #50)
  1.1134 +#52 := (not #51)
  1.1135 +#148 := (iff #52 #145)
  1.1136 +#138 := (iff #125 #135)
  1.1137 +#141 := (not #138)
  1.1138 +#146 := (iff #141 #145)
  1.1139 +#147 := [rewrite]: #146
  1.1140 +#142 := (iff #52 #141)
  1.1141 +#139 := (iff #51 #138)
  1.1142 +#136 := (iff #50 #135)
  1.1143 +#133 := (iff #49 #132)
  1.1144 +#134 := [rewrite]: #133
  1.1145 +#130 := (iff #47 #129)
  1.1146 +#131 := [rewrite]: #130
  1.1147 +#137 := [monotonicity #131 #134]: #136
  1.1148 +#127 := (iff #45 #125)
  1.1149 +#128 := [rewrite]: #127
  1.1150 +#140 := [monotonicity #128 #137]: #139
  1.1151 +#143 := [monotonicity #140]: #142
  1.1152 +#149 := [trans #143 #147]: #148
  1.1153 +#124 := [asserted]: #52
  1.1154 +#152 := [mp #124 #149]: #145
  1.1155 +#204 := [mp #152 #203]: #199
  1.1156 +#342 := (not #199)
  1.1157 +#352 := (or #144 #187 #342)
  1.1158 +#356 := [def-axiom]: #352
  1.1159 +#672 := [unit-resolution #356 #204]: #335
  1.1160 +#461 := [unit-resolution #672 #329]: #144
  1.1161 +#328 := (or #125 #187)
  1.1162 +#674 := (iff #125 #188)
  1.1163 +#21 := (:var 0 S3)
  1.1164 +#19 := (:var 1 S3)
  1.1165 +#32 := (f8 #19)
  1.1166 +#33 := (f6 #32 #21)
  1.1167 +#18 := (:var 2 S2)
  1.1168 +#34 := (f3 #18 #33)
  1.1169 +#701 := (pattern #34)
  1.1170 +#27 := (f3 #18 #21)
  1.1171 +#98 := (= f1 #27)
  1.1172 +#177 := (not #98)
  1.1173 +#25 := (f3 #18 #19)
  1.1174 +#95 := (= f1 #25)
  1.1175 +#176 := (not #95)
  1.1176 +#160 := (or #176 #177)
  1.1177 +#161 := (not #160)
  1.1178 +#111 := (= f1 #34)
  1.1179 +#178 := (iff #111 #161)
  1.1180 +#702 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #701) #178)
  1.1181 +#181 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #178)
  1.1182 +#705 := (iff #181 #702)
  1.1183 +#703 := (iff #178 #178)
  1.1184 +#704 := [refl]: #703
  1.1185 +#706 := [quant-intro #704]: #705
  1.1186 +#115 := (and #95 #98)
  1.1187 +#118 := (iff #111 #115)
  1.1188 +#121 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #118)
  1.1189 +#182 := (iff #121 #181)
  1.1190 +#179 := (iff #118 #178)
  1.1191 +#162 := (iff #115 #161)
  1.1192 +#163 := [rewrite]: #162
  1.1193 +#180 := [monotonicity #163]: #179
  1.1194 +#183 := [quant-intro #180]: #182
  1.1195 +#158 := (~ #121 #121)
  1.1196 +#173 := (~ #118 #118)
  1.1197 +#174 := [refl]: #173
  1.1198 +#159 := [nnf-pos #174]: #158
  1.1199 +#28 := (= #27 f1)
  1.1200 +#26 := (= #25 f1)
  1.1201 +#36 := (and #26 #28)
  1.1202 +#35 := (= #34 f1)
  1.1203 +#37 := (iff #35 #36)
  1.1204 +#38 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #37)
  1.1205 +#122 := (iff #38 #121)
  1.1206 +#119 := (iff #37 #118)
  1.1207 +#116 := (iff #36 #115)
  1.1208 +#99 := (iff #28 #98)
  1.1209 +#100 := [rewrite]: #99
  1.1210 +#96 := (iff #26 #95)
  1.1211 +#97 := [rewrite]: #96
  1.1212 +#117 := [monotonicity #97 #100]: #116
  1.1213 +#113 := (iff #35 #111)
  1.1214 +#114 := [rewrite]: #113
  1.1215 +#120 := [monotonicity #114 #117]: #119
  1.1216 +#123 := [quant-intro #120]: #122
  1.1217 +#110 := [asserted]: #38
  1.1218 +#126 := [mp #110 #123]: #121
  1.1219 +#175 := [mp~ #126 #159]: #121
  1.1220 +#184 := [mp #175 #183]: #181
  1.1221 +#707 := [mp #184 #706]: #702
  1.1222 +#668 := (not #702)
  1.1223 +#340 := (or #668 #674)
  1.1224 +#341 := [quant-inst #39 #40 #42]: #340
  1.1225 +#670 := [unit-resolution #341 #707]: #674
  1.1226 +#675 := (not #674)
  1.1227 +#676 := (or #675 #125 #187)
  1.1228 +#677 := [def-axiom]: #676
  1.1229 +#671 := [unit-resolution #677 #670]: #328
  1.1230 +#312 := [unit-resolution #671 #461 #329]: false
  1.1231 +#655 := [lemma #312]: #187
  1.1232 +#282 := (or #125 #188)
  1.1233 +#353 := (or #125 #188 #342)
  1.1234 +#354 := [def-axiom]: #353
  1.1235 +#355 := [unit-resolution #354 #204]: #282
  1.1236 +#316 := [unit-resolution #355 #655]: #125
  1.1237 +#317 := (or #144 #188)
  1.1238 +#678 := (or #675 #144 #188)
  1.1239 +#673 := [def-axiom]: #678
  1.1240 +#318 := [unit-resolution #673 #670]: #317
  1.1241 +[unit-resolution #318 #316 #655]: false
  1.1242 +unsat
  1.1243 +453491eb61ee5da70153220378ac3f020b43cd23 147 0
  1.1244 +#2 := false
  1.1245 +decl f3 :: (-> S2 S3 S1)
  1.1246 +decl f4 :: S3
  1.1247 +#9 := f4
  1.1248 +decl f9 :: S2
  1.1249 +#39 := f9
  1.1250 +#225 := (f3 f9 f4)
  1.1251 +decl f1 :: S1
  1.1252 +#4 := f1
  1.1253 +#312 := (= f1 #225)
  1.1254 +#226 := (not #312)
  1.1255 +decl f10 :: S3
  1.1256 +#40 := f10
  1.1257 +#313 := (f3 f9 f10)
  1.1258 +#227 := (= f1 #313)
  1.1259 +#314 := (not #227)
  1.1260 +#305 := (or #314 #226)
  1.1261 +#316 := (not #305)
  1.1262 +decl f6 :: (-> S4 S3 S3)
  1.1263 +decl f8 :: (-> S3 S4)
  1.1264 +#41 := (f8 f10)
  1.1265 +#42 := (f6 #41 f4)
  1.1266 +#43 := (f3 f9 #42)
  1.1267 +#119 := (= f1 #43)
  1.1268 +#317 := (iff #119 #316)
  1.1269 +#21 := (:var 0 S3)
  1.1270 +#19 := (:var 1 S3)
  1.1271 +#32 := (f8 #19)
  1.1272 +#33 := (f6 #32 #21)
  1.1273 +#18 := (:var 2 S2)
  1.1274 +#34 := (f3 #18 #33)
  1.1275 +#664 := (pattern #34)
  1.1276 +#27 := (f3 #18 #21)
  1.1277 +#92 := (= f1 #27)
  1.1278 +#160 := (not #92)
  1.1279 +#25 := (f3 #18 #19)
  1.1280 +#89 := (= f1 #25)
  1.1281 +#159 := (not #89)
  1.1282 +#143 := (or #159 #160)
  1.1283 +#144 := (not #143)
  1.1284 +#105 := (= f1 #34)
  1.1285 +#161 := (iff #105 #144)
  1.1286 +#665 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #664) #161)
  1.1287 +#164 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #161)
  1.1288 +#668 := (iff #164 #665)
  1.1289 +#666 := (iff #161 #161)
  1.1290 +#667 := [refl]: #666
  1.1291 +#669 := [quant-intro #667]: #668
  1.1292 +#109 := (and #89 #92)
  1.1293 +#112 := (iff #105 #109)
  1.1294 +#115 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #112)
  1.1295 +#165 := (iff #115 #164)
  1.1296 +#162 := (iff #112 #161)
  1.1297 +#145 := (iff #109 #144)
  1.1298 +#146 := [rewrite]: #145
  1.1299 +#163 := [monotonicity #146]: #162
  1.1300 +#166 := [quant-intro #163]: #165
  1.1301 +#141 := (~ #115 #115)
  1.1302 +#156 := (~ #112 #112)
  1.1303 +#157 := [refl]: #156
  1.1304 +#142 := [nnf-pos #157]: #141
  1.1305 +#28 := (= #27 f1)
  1.1306 +#26 := (= #25 f1)
  1.1307 +#36 := (and #26 #28)
  1.1308 +#35 := (= #34 f1)
  1.1309 +#37 := (iff #35 #36)
  1.1310 +#38 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #37)
  1.1311 +#116 := (iff #38 #115)
  1.1312 +#113 := (iff #37 #112)
  1.1313 +#110 := (iff #36 #109)
  1.1314 +#93 := (iff #28 #92)
  1.1315 +#94 := [rewrite]: #93
  1.1316 +#90 := (iff #26 #89)
  1.1317 +#91 := [rewrite]: #90
  1.1318 +#111 := [monotonicity #91 #94]: #110
  1.1319 +#107 := (iff #35 #105)
  1.1320 +#108 := [rewrite]: #107
  1.1321 +#114 := [monotonicity #108 #111]: #113
  1.1322 +#117 := [quant-intro #114]: #116
  1.1323 +#104 := [asserted]: #38
  1.1324 +#120 := [mp #104 #117]: #115
  1.1325 +#158 := [mp~ #120 #142]: #115
  1.1326 +#167 := [mp #158 #166]: #164
  1.1327 +#670 := [mp #167 #669]: #665
  1.1328 +#315 := (not #665)
  1.1329 +#319 := (or #315 #317)
  1.1330 +#298 := [quant-inst #39 #40 #9]: #319
  1.1331 +#245 := [unit-resolution #298 #670]: #317
  1.1332 +#304 := (not #317)
  1.1333 +#318 := (or #304 #316)
  1.1334 +#44 := (= #43 f1)
  1.1335 +#45 := (not #44)
  1.1336 +#46 := (not #45)
  1.1337 +#131 := (iff #46 #119)
  1.1338 +#123 := (not #119)
  1.1339 +#126 := (not #123)
  1.1340 +#129 := (iff #126 #119)
  1.1341 +#130 := [rewrite]: #129
  1.1342 +#127 := (iff #46 #126)
  1.1343 +#124 := (iff #45 #123)
  1.1344 +#121 := (iff #44 #119)
  1.1345 +#122 := [rewrite]: #121
  1.1346 +#125 := [monotonicity #122]: #124
  1.1347 +#128 := [monotonicity #125]: #127
  1.1348 +#132 := [trans #128 #130]: #131
  1.1349 +#118 := [asserted]: #46
  1.1350 +#135 := [mp #118 #132]: #119
  1.1351 +#640 := (or #304 #123 #316)
  1.1352 +#641 := [def-axiom]: #640
  1.1353 +#634 := [unit-resolution #641 #135]: #318
  1.1354 +#275 := [unit-resolution #634 #245]: #316
  1.1355 +#292 := (or #305 #312)
  1.1356 +#424 := [def-axiom]: #292
  1.1357 +#618 := [unit-resolution #424 #275]: #312
  1.1358 +#8 := (:var 0 S2)
  1.1359 +#10 := (f3 #8 f4)
  1.1360 +#643 := (pattern #10)
  1.1361 +#67 := (= f1 #10)
  1.1362 +#70 := (not #67)
  1.1363 +#644 := (forall (vars (?v0 S2)) (:pat #643) #70)
  1.1364 +#73 := (forall (vars (?v0 S2)) #70)
  1.1365 +#647 := (iff #73 #644)
  1.1366 +#645 := (iff #70 #70)
  1.1367 +#646 := [refl]: #645
  1.1368 +#648 := [quant-intro #646]: #647
  1.1369 +#149 := (~ #73 #73)
  1.1370 +#147 := (~ #70 #70)
  1.1371 +#148 := [refl]: #147
  1.1372 +#150 := [nnf-pos #148]: #149
  1.1373 +#11 := (= #10 f1)
  1.1374 +#12 := (not #11)
  1.1375 +#13 := (forall (vars (?v0 S2)) #12)
  1.1376 +#74 := (iff #13 #73)
  1.1377 +#71 := (iff #12 #70)
  1.1378 +#68 := (iff #11 #67)
  1.1379 +#69 := [rewrite]: #68
  1.1380 +#72 := [monotonicity #69]: #71
  1.1381 +#75 := [quant-intro #72]: #74
  1.1382 +#66 := [asserted]: #13
  1.1383 +#78 := [mp #66 #75]: #73
  1.1384 +#134 := [mp~ #78 #150]: #73
  1.1385 +#649 := [mp #134 #648]: #644
  1.1386 +#295 := (not #644)
  1.1387 +#633 := (or #295 #226)
  1.1388 +#291 := [quant-inst #39]: #633
  1.1389 +[unit-resolution #291 #649 #618]: false
  1.1390 +unsat
  1.1391 +6f8829ccc8ddcc6f60b1e61de2ed840042d23d2c 171 0
  1.1392 +#2 := false
  1.1393 +decl f3 :: (-> S2 S3 S1)
  1.1394 +decl f10 :: S3
  1.1395 +#40 := f10
  1.1396 +decl f9 :: S2
  1.1397 +#39 := f9
  1.1398 +#45 := (f3 f9 f10)
  1.1399 +decl f1 :: S1
  1.1400 +#4 := f1
  1.1401 +#125 := (= f1 #45)
  1.1402 +#321 := (not #125)
  1.1403 +decl f6 :: (-> S4 S3 S3)
  1.1404 +decl f5 :: S3
  1.1405 +#14 := f5
  1.1406 +decl f8 :: (-> S3 S4)
  1.1407 +#41 := (f8 f10)
  1.1408 +#42 := (f6 #41 f5)
  1.1409 +#43 := (f3 f9 #42)
  1.1410 +#121 := (= f1 #43)
  1.1411 +#325 := (f3 f9 f5)
  1.1412 +#322 := (= f1 #325)
  1.1413 +#326 := (not #322)
  1.1414 +#299 := [hypothesis]: #326
  1.1415 +#8 := (:var 0 S2)
  1.1416 +#15 := (f3 #8 f5)
  1.1417 +#657 := (pattern #15)
  1.1418 +#79 := (= f1 #15)
  1.1419 +#658 := (forall (vars (?v0 S2)) (:pat #657) #79)
  1.1420 +#83 := (forall (vars (?v0 S2)) #79)
  1.1421 +#661 := (iff #83 #658)
  1.1422 +#659 := (iff #79 #79)
  1.1423 +#660 := [refl]: #659
  1.1424 +#662 := [quant-intro #660]: #661
  1.1425 +#144 := (~ #83 #83)
  1.1426 +#143 := (~ #79 #79)
  1.1427 +#158 := [refl]: #143
  1.1428 +#145 := [nnf-pos #158]: #144
  1.1429 +#16 := (= #15 f1)
  1.1430 +#17 := (forall (vars (?v0 S2)) #16)
  1.1431 +#84 := (iff #17 #83)
  1.1432 +#81 := (iff #16 #79)
  1.1433 +#82 := [rewrite]: #81
  1.1434 +#85 := [quant-intro #82]: #84
  1.1435 +#78 := [asserted]: #17
  1.1436 +#88 := [mp #78 #85]: #83
  1.1437 +#159 := [mp~ #88 #145]: #83
  1.1438 +#663 := [mp #159 #662]: #658
  1.1439 +#287 := (not #658)
  1.1440 +#288 := (or #287 #322)
  1.1441 +#289 := [quant-inst #39]: #288
  1.1442 +#431 := [unit-resolution #289 #663 #299]: false
  1.1443 +#627 := [lemma #431]: #322
  1.1444 +#134 := (not #121)
  1.1445 +#628 := [hypothesis]: #134
  1.1446 +#320 := (or #125 #121)
  1.1447 +#135 := (iff #125 #134)
  1.1448 +#46 := (= #45 f1)
  1.1449 +#44 := (= #43 f1)
  1.1450 +#47 := (iff #44 #46)
  1.1451 +#48 := (not #47)
  1.1452 +#138 := (iff #48 #135)
  1.1453 +#128 := (iff #121 #125)
  1.1454 +#131 := (not #128)
  1.1455 +#136 := (iff #131 #135)
  1.1456 +#137 := [rewrite]: #136
  1.1457 +#132 := (iff #48 #131)
  1.1458 +#129 := (iff #47 #128)
  1.1459 +#126 := (iff #46 #125)
  1.1460 +#127 := [rewrite]: #126
  1.1461 +#123 := (iff #44 #121)
  1.1462 +#124 := [rewrite]: #123
  1.1463 +#130 := [monotonicity #124 #127]: #129
  1.1464 +#133 := [monotonicity #130]: #132
  1.1465 +#139 := [trans #133 #137]: #138
  1.1466 +#120 := [asserted]: #48
  1.1467 +#142 := [mp #120 #139]: #135
  1.1468 +#232 := (not #135)
  1.1469 +#319 := (or #125 #121 #232)
  1.1470 +#233 := [def-axiom]: #319
  1.1471 +#234 := [unit-resolution #233 #142]: #320
  1.1472 +#629 := [unit-resolution #234 #628]: #125
  1.1473 +#305 := (or #321 #326)
  1.1474 +#631 := (or #121 #305)
  1.1475 +#642 := (not #305)
  1.1476 +#644 := (iff #121 #642)
  1.1477 +#21 := (:var 0 S3)
  1.1478 +#19 := (:var 1 S3)
  1.1479 +#32 := (f8 #19)
  1.1480 +#33 := (f6 #32 #21)
  1.1481 +#18 := (:var 2 S2)
  1.1482 +#34 := (f3 #18 #33)
  1.1483 +#671 := (pattern #34)
  1.1484 +#27 := (f3 #18 #21)
  1.1485 +#94 := (= f1 #27)
  1.1486 +#167 := (not #94)
  1.1487 +#25 := (f3 #18 #19)
  1.1488 +#91 := (= f1 #25)
  1.1489 +#166 := (not #91)
  1.1490 +#150 := (or #166 #167)
  1.1491 +#151 := (not #150)
  1.1492 +#107 := (= f1 #34)
  1.1493 +#168 := (iff #107 #151)
  1.1494 +#672 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #671) #168)
  1.1495 +#171 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #168)
  1.1496 +#675 := (iff #171 #672)
  1.1497 +#673 := (iff #168 #168)
  1.1498 +#674 := [refl]: #673
  1.1499 +#676 := [quant-intro #674]: #675
  1.1500 +#111 := (and #91 #94)
  1.1501 +#114 := (iff #107 #111)
  1.1502 +#117 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #114)
  1.1503 +#172 := (iff #117 #171)
  1.1504 +#169 := (iff #114 #168)
  1.1505 +#152 := (iff #111 #151)
  1.1506 +#153 := [rewrite]: #152
  1.1507 +#170 := [monotonicity #153]: #169
  1.1508 +#173 := [quant-intro #170]: #172
  1.1509 +#148 := (~ #117 #117)
  1.1510 +#163 := (~ #114 #114)
  1.1511 +#164 := [refl]: #163
  1.1512 +#149 := [nnf-pos #164]: #148
  1.1513 +#28 := (= #27 f1)
  1.1514 +#26 := (= #25 f1)
  1.1515 +#36 := (and #26 #28)
  1.1516 +#35 := (= #34 f1)
  1.1517 +#37 := (iff #35 #36)
  1.1518 +#38 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #37)
  1.1519 +#118 := (iff #38 #117)
  1.1520 +#115 := (iff #37 #114)
  1.1521 +#112 := (iff #36 #111)
  1.1522 +#95 := (iff #28 #94)
  1.1523 +#96 := [rewrite]: #95
  1.1524 +#92 := (iff #26 #91)
  1.1525 +#93 := [rewrite]: #92
  1.1526 +#113 := [monotonicity #93 #96]: #112
  1.1527 +#109 := (iff #35 #107)
  1.1528 +#110 := [rewrite]: #109
  1.1529 +#116 := [monotonicity #110 #113]: #115
  1.1530 +#119 := [quant-intro #116]: #118
  1.1531 +#106 := [asserted]: #38
  1.1532 +#122 := [mp #106 #119]: #117
  1.1533 +#165 := [mp~ #122 #149]: #117
  1.1534 +#174 := [mp #165 #173]: #171
  1.1535 +#677 := [mp #174 #676]: #672
  1.1536 +#638 := (not #672)
  1.1537 +#310 := (or #638 #644)
  1.1538 +#311 := [quant-inst #39 #40 #14]: #310
  1.1539 +#630 := [unit-resolution #311 #677]: #644
  1.1540 +#639 := (not #644)
  1.1541 +#297 := (or #639 #121 #305)
  1.1542 +#302 := [def-axiom]: #297
  1.1543 +#626 := [unit-resolution #302 #630]: #631
  1.1544 +#632 := [unit-resolution #626 #628]: #305
  1.1545 +#643 := (or #642 #321 #326)
  1.1546 +#649 := [def-axiom]: #643
  1.1547 +#268 := [unit-resolution #649 #632 #629 #627]: false
  1.1548 +#633 := [lemma #268]: #121
  1.1549 +#324 := (or #321 #134)
  1.1550 +#312 := (or #321 #134 #232)
  1.1551 +#323 := [def-axiom]: #312
  1.1552 +#252 := [unit-resolution #323 #142]: #324
  1.1553 +#635 := [unit-resolution #252 #633]: #321
  1.1554 +#273 := (or #134 #642)
  1.1555 +#640 := (or #639 #134 #642)
  1.1556 +#298 := [def-axiom]: #640
  1.1557 +#274 := [unit-resolution #298 #630]: #273
  1.1558 +#636 := [unit-resolution #274 #633]: #642
  1.1559 +#645 := (or #305 #125)
  1.1560 +#646 := [def-axiom]: #645
  1.1561 +[unit-resolution #646 #636 #635]: false
  1.1562 +unsat
  1.1563 +7fb5c9e3c94a5bd9f761d4854f2678f455553edf 171 0
  1.1564 +#2 := false
  1.1565 +decl f3 :: (-> S2 S3 S1)
  1.1566 +decl f6 :: (-> S4 S3 S3)
  1.1567 +decl f10 :: S3
  1.1568 +#40 := f10
  1.1569 +decl f8 :: (-> S3 S4)
  1.1570 +decl f11 :: S3
  1.1571 +#42 := f11
  1.1572 +#46 := (f8 f11)
  1.1573 +#47 := (f6 #46 f10)
  1.1574 +decl f9 :: S2
  1.1575 +#39 := f9
  1.1576 +#48 := (f3 f9 #47)
  1.1577 +decl f1 :: S1
  1.1578 +#4 := f1
  1.1579 +#128 := (= f1 #48)
  1.1580 +#324 := (not #128)
  1.1581 +#41 := (f8 f10)
  1.1582 +#43 := (f6 #41 f11)
  1.1583 +#44 := (f3 f9 #43)
  1.1584 +#124 := (= f1 #44)
  1.1585 +#137 := (not #124)
  1.1586 +#626 := [hypothesis]: #137
  1.1587 +#323 := (or #128 #124)
  1.1588 +#138 := (iff #128 #137)
  1.1589 +#49 := (= #48 f1)
  1.1590 +#45 := (= #44 f1)
  1.1591 +#50 := (iff #45 #49)
  1.1592 +#51 := (not #50)
  1.1593 +#141 := (iff #51 #138)
  1.1594 +#131 := (iff #124 #128)
  1.1595 +#134 := (not #131)
  1.1596 +#139 := (iff #134 #138)
  1.1597 +#140 := [rewrite]: #139
  1.1598 +#135 := (iff #51 #134)
  1.1599 +#132 := (iff #50 #131)
  1.1600 +#129 := (iff #49 #128)
  1.1601 +#130 := [rewrite]: #129
  1.1602 +#126 := (iff #45 #124)
  1.1603 +#127 := [rewrite]: #126
  1.1604 +#133 := [monotonicity #127 #130]: #132
  1.1605 +#136 := [monotonicity #133]: #135
  1.1606 +#142 := [trans #136 #140]: #141
  1.1607 +#123 := [asserted]: #51
  1.1608 +#145 := [mp #123 #142]: #138
  1.1609 +#235 := (not #138)
  1.1610 +#322 := (or #128 #124 #235)
  1.1611 +#236 := [def-axiom]: #322
  1.1612 +#237 := [unit-resolution #236 #145]: #323
  1.1613 +#627 := [unit-resolution #237 #626]: #128
  1.1614 +#308 := (f3 f9 f11)
  1.1615 +#645 := (= f1 #308)
  1.1616 +#647 := (not #645)
  1.1617 +#328 := (f3 f9 f10)
  1.1618 +#325 := (= f1 #328)
  1.1619 +#329 := (not #325)
  1.1620 +#313 := (or #329 #647)
  1.1621 +#624 := (or #124 #313)
  1.1622 +#649 := (not #313)
  1.1623 +#640 := (iff #124 #649)
  1.1624 +#21 := (:var 0 S3)
  1.1625 +#19 := (:var 1 S3)
  1.1626 +#32 := (f8 #19)
  1.1627 +#33 := (f6 #32 #21)
  1.1628 +#18 := (:var 2 S2)
  1.1629 +#34 := (f3 #18 #33)
  1.1630 +#674 := (pattern #34)
  1.1631 +#27 := (f3 #18 #21)
  1.1632 +#97 := (= f1 #27)
  1.1633 +#170 := (not #97)
  1.1634 +#25 := (f3 #18 #19)
  1.1635 +#94 := (= f1 #25)
  1.1636 +#169 := (not #94)
  1.1637 +#153 := (or #169 #170)
  1.1638 +#154 := (not #153)
  1.1639 +#110 := (= f1 #34)
  1.1640 +#171 := (iff #110 #154)
  1.1641 +#675 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #674) #171)
  1.1642 +#174 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #171)
  1.1643 +#678 := (iff #174 #675)
  1.1644 +#676 := (iff #171 #171)
  1.1645 +#677 := [refl]: #676
  1.1646 +#679 := [quant-intro #677]: #678
  1.1647 +#114 := (and #94 #97)
  1.1648 +#117 := (iff #110 #114)
  1.1649 +#120 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #117)
  1.1650 +#175 := (iff #120 #174)
  1.1651 +#172 := (iff #117 #171)
  1.1652 +#155 := (iff #114 #154)
  1.1653 +#156 := [rewrite]: #155
  1.1654 +#173 := [monotonicity #156]: #172
  1.1655 +#176 := [quant-intro #173]: #175
  1.1656 +#151 := (~ #120 #120)
  1.1657 +#166 := (~ #117 #117)
  1.1658 +#167 := [refl]: #166
  1.1659 +#152 := [nnf-pos #167]: #151
  1.1660 +#28 := (= #27 f1)
  1.1661 +#26 := (= #25 f1)
  1.1662 +#36 := (and #26 #28)
  1.1663 +#35 := (= #34 f1)
  1.1664 +#37 := (iff #35 #36)
  1.1665 +#38 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #37)
  1.1666 +#121 := (iff #38 #120)
  1.1667 +#118 := (iff #37 #117)
  1.1668 +#115 := (iff #36 #114)
  1.1669 +#98 := (iff #28 #97)
  1.1670 +#99 := [rewrite]: #98
  1.1671 +#95 := (iff #26 #94)
  1.1672 +#96 := [rewrite]: #95
  1.1673 +#116 := [monotonicity #96 #99]: #115
  1.1674 +#112 := (iff #35 #110)
  1.1675 +#113 := [rewrite]: #112
  1.1676 +#119 := [monotonicity #113 #116]: #118
  1.1677 +#122 := [quant-intro #119]: #121
  1.1678 +#109 := [asserted]: #38
  1.1679 +#125 := [mp #109 #122]: #120
  1.1680 +#168 := [mp~ #125 #152]: #120
  1.1681 +#177 := [mp #168 #176]: #174
  1.1682 +#680 := [mp #177 #679]: #675
  1.1683 +#300 := (not #675)
  1.1684 +#333 := (or #300 #640)
  1.1685 +#349 := [quant-inst #39 #40 #42]: #333
  1.1686 +#620 := [unit-resolution #349 #680]: #640
  1.1687 +#350 := (not #640)
  1.1688 +#351 := (or #350 #124 #313)
  1.1689 +#337 := [def-axiom]: #351
  1.1690 +#621 := [unit-resolution #337 #620]: #624
  1.1691 +#625 := [unit-resolution #621 #626]: #313
  1.1692 +#335 := (or #324 #649)
  1.1693 +#646 := (iff #128 #649)
  1.1694 +#305 := (or #300 #646)
  1.1695 +#302 := (or #647 #329)
  1.1696 +#434 := (not #302)
  1.1697 +#641 := (iff #128 #434)
  1.1698 +#643 := (or #300 #641)
  1.1699 +#644 := (iff #643 #305)
  1.1700 +#628 := (iff #305 #305)
  1.1701 +#289 := [rewrite]: #628
  1.1702 +#652 := (iff #641 #646)
  1.1703 +#650 := (iff #434 #649)
  1.1704 +#314 := (iff #302 #313)
  1.1705 +#648 := [rewrite]: #314
  1.1706 +#651 := [monotonicity #648]: #650
  1.1707 +#642 := [monotonicity #651]: #652
  1.1708 +#285 := [monotonicity #642]: #644
  1.1709 +#290 := [trans #285 #289]: #644
  1.1710 +#301 := [quant-inst #39 #42 #40]: #643
  1.1711 +#291 := [mp #301 #290]: #305
  1.1712 +#334 := [unit-resolution #291 #680]: #646
  1.1713 +#629 := (not #646)
  1.1714 +#636 := (or #629 #324 #649)
  1.1715 +#638 := [def-axiom]: #636
  1.1716 +#336 := [unit-resolution #638 #334]: #335
  1.1717 +#338 := [unit-resolution #336 #625 #627]: false
  1.1718 +#616 := [lemma #338]: #124
  1.1719 +#327 := (or #324 #137)
  1.1720 +#315 := (or #324 #137 #235)
  1.1721 +#326 := [def-axiom]: #315
  1.1722 +#255 := [unit-resolution #326 #145]: #327
  1.1723 +#617 := [unit-resolution #255 #616]: #324
  1.1724 +#330 := (or #137 #649)
  1.1725 +#352 := (or #350 #137 #649)
  1.1726 +#243 := [def-axiom]: #352
  1.1727 +#614 := [unit-resolution #243 #620]: #330
  1.1728 +#618 := [unit-resolution #614 #616]: #649
  1.1729 +#615 := (or #128 #313)
  1.1730 +#635 := (or #629 #128 #313)
  1.1731 +#271 := [def-axiom]: #635
  1.1732 +#619 := [unit-resolution #271 #334]: #615
  1.1733 +[unit-resolution #619 #618 #617]: false
  1.1734 +unsat
  1.1735 +894705c4ef9337c77fce76fc097ee92668a964e4 147 0
  1.1736 +#2 := false
  1.1737 +decl f3 :: (-> S2 S3 S1)
  1.1738 +decl f6 :: (-> S4 S3 S3)
  1.1739 +decl f10 :: S3
  1.1740 +#40 := f10
  1.1741 +decl f8 :: (-> S3 S4)
  1.1742 +#41 := (f8 f10)
  1.1743 +#42 := (f6 #41 f10)
  1.1744 +decl f9 :: S2
  1.1745 +#39 := f9
  1.1746 +#43 := (f3 f9 #42)
  1.1747 +decl f1 :: S1
  1.1748 +#4 := f1
  1.1749 +#121 := (= f1 #43)
  1.1750 +#134 := (not #121)
  1.1751 +#630 := [hypothesis]: #134
  1.1752 +#45 := (f3 f9 f10)
  1.1753 +#125 := (= f1 #45)
  1.1754 +#320 := (or #125 #121)
  1.1755 +#135 := (iff #125 #134)
  1.1756 +#46 := (= #45 f1)
  1.1757 +#44 := (= #43 f1)
  1.1758 +#47 := (iff #44 #46)
  1.1759 +#48 := (not #47)
  1.1760 +#138 := (iff #48 #135)
  1.1761 +#128 := (iff #121 #125)
  1.1762 +#131 := (not #128)
  1.1763 +#136 := (iff #131 #135)
  1.1764 +#137 := [rewrite]: #136
  1.1765 +#132 := (iff #48 #131)
  1.1766 +#129 := (iff #47 #128)
  1.1767 +#126 := (iff #46 #125)
  1.1768 +#127 := [rewrite]: #126
  1.1769 +#123 := (iff #44 #121)
  1.1770 +#124 := [rewrite]: #123
  1.1771 +#130 := [monotonicity #124 #127]: #129
  1.1772 +#133 := [monotonicity #130]: #132
  1.1773 +#139 := [trans #133 #137]: #138
  1.1774 +#120 := [asserted]: #48
  1.1775 +#142 := [mp #120 #139]: #135
  1.1776 +#232 := (not #135)
  1.1777 +#319 := (or #125 #121 #232)
  1.1778 +#233 := [def-axiom]: #319
  1.1779 +#234 := [unit-resolution #233 #142]: #320
  1.1780 +#631 := [unit-resolution #234 #630]: #125
  1.1781 +#321 := (not #125)
  1.1782 +#632 := (or #121 #321)
  1.1783 +#21 := (:var 0 S3)
  1.1784 +#19 := (:var 1 S3)
  1.1785 +#32 := (f8 #19)
  1.1786 +#33 := (f6 #32 #21)
  1.1787 +#18 := (:var 2 S2)
  1.1788 +#34 := (f3 #18 #33)
  1.1789 +#671 := (pattern #34)
  1.1790 +#27 := (f3 #18 #21)
  1.1791 +#94 := (= f1 #27)
  1.1792 +#167 := (not #94)
  1.1793 +#25 := (f3 #18 #19)
  1.1794 +#91 := (= f1 #25)
  1.1795 +#166 := (not #91)
  1.1796 +#150 := (or #166 #167)
  1.1797 +#151 := (not #150)
  1.1798 +#107 := (= f1 #34)
  1.1799 +#168 := (iff #107 #151)
  1.1800 +#672 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #671) #168)
  1.1801 +#171 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #168)
  1.1802 +#675 := (iff #171 #672)
  1.1803 +#673 := (iff #168 #168)
  1.1804 +#674 := [refl]: #673
  1.1805 +#676 := [quant-intro #674]: #675
  1.1806 +#111 := (and #91 #94)
  1.1807 +#114 := (iff #107 #111)
  1.1808 +#117 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #114)
  1.1809 +#172 := (iff #117 #171)
  1.1810 +#169 := (iff #114 #168)
  1.1811 +#152 := (iff #111 #151)
  1.1812 +#153 := [rewrite]: #152
  1.1813 +#170 := [monotonicity #153]: #169
  1.1814 +#173 := [quant-intro #170]: #172
  1.1815 +#148 := (~ #117 #117)
  1.1816 +#163 := (~ #114 #114)
  1.1817 +#164 := [refl]: #163
  1.1818 +#149 := [nnf-pos #164]: #148
  1.1819 +#28 := (= #27 f1)
  1.1820 +#26 := (= #25 f1)
  1.1821 +#36 := (and #26 #28)
  1.1822 +#35 := (= #34 f1)
  1.1823 +#37 := (iff #35 #36)
  1.1824 +#38 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #37)
  1.1825 +#118 := (iff #38 #117)
  1.1826 +#115 := (iff #37 #114)
  1.1827 +#112 := (iff #36 #111)
  1.1828 +#95 := (iff #28 #94)
  1.1829 +#96 := [rewrite]: #95
  1.1830 +#92 := (iff #26 #91)
  1.1831 +#93 := [rewrite]: #92
  1.1832 +#113 := [monotonicity #93 #96]: #112
  1.1833 +#109 := (iff #35 #107)
  1.1834 +#110 := [rewrite]: #109
  1.1835 +#116 := [monotonicity #110 #113]: #115
  1.1836 +#119 := [quant-intro #116]: #118
  1.1837 +#106 := [asserted]: #38
  1.1838 +#122 := [mp #106 #119]: #117
  1.1839 +#165 := [mp~ #122 #149]: #117
  1.1840 +#174 := [mp #165 #173]: #171
  1.1841 +#677 := [mp #174 #676]: #672
  1.1842 +#648 := (not #672)
  1.1843 +#643 := (or #648 #128)
  1.1844 +#325 := (or #321 #321)
  1.1845 +#322 := (not #325)
  1.1846 +#326 := (iff #121 #322)
  1.1847 +#649 := (or #648 #326)
  1.1848 +#297 := (iff #649 #643)
  1.1849 +#640 := (iff #643 #643)
  1.1850 +#298 := [rewrite]: #640
  1.1851 +#646 := (iff #326 #128)
  1.1852 +#311 := (iff #322 #125)
  1.1853 +#644 := (not #321)
  1.1854 +#638 := (iff #644 #125)
  1.1855 +#310 := [rewrite]: #638
  1.1856 +#299 := (iff #322 #644)
  1.1857 +#305 := (iff #325 #321)
  1.1858 +#642 := [rewrite]: #305
  1.1859 +#431 := [monotonicity #642]: #299
  1.1860 +#645 := [trans #431 #310]: #311
  1.1861 +#647 := [monotonicity #645]: #646
  1.1862 +#302 := [monotonicity #647]: #297
  1.1863 +#641 := [trans #302 #298]: #297
  1.1864 +#639 := [quant-inst #39 #40 #40]: #649
  1.1865 +#282 := [mp #639 #641]: #643
  1.1866 +#626 := [unit-resolution #282 #677]: #128
  1.1867 +#625 := (or #131 #121 #321)
  1.1868 +#286 := [def-axiom]: #625
  1.1869 +#268 := [unit-resolution #286 #626]: #632
  1.1870 +#633 := [unit-resolution #268 #631 #630]: false
  1.1871 +#635 := [lemma #633]: #121
  1.1872 +#324 := (or #321 #134)
  1.1873 +#312 := (or #321 #134 #232)
  1.1874 +#323 := [def-axiom]: #312
  1.1875 +#252 := [unit-resolution #323 #142]: #324
  1.1876 +#273 := [unit-resolution #252 #635]: #321
  1.1877 +#274 := (or #134 #125)
  1.1878 +#287 := (or #131 #134 #125)
  1.1879 +#288 := [def-axiom]: #287
  1.1880 +#636 := [unit-resolution #288 #626]: #274
  1.1881 +[unit-resolution #636 #273 #635]: false
  1.1882 +unsat
  1.1883 +6bc0dc7cf7d78f36cf0c61d5f399a6c019b36218 285 0
  1.1884 +#2 := false
  1.1885 +decl f3 :: (-> S2 S3 S1)
  1.1886 +decl f6 :: (-> S4 S3 S3)
  1.1887 +decl f11 :: S3
  1.1888 +#42 := f11
  1.1889 +decl f8 :: (-> S3 S4)
  1.1890 +decl f10 :: S3
  1.1891 +#40 := f10
  1.1892 +#41 := (f8 f10)
  1.1893 +#49 := (f6 #41 f11)
  1.1894 +decl f9 :: S2
  1.1895 +#39 := f9
  1.1896 +#312 := (f3 f9 #49)
  1.1897 +decl f1 :: S1
  1.1898 +#4 := f1
  1.1899 +#649 := (= f1 #312)
  1.1900 +#247 := (f3 f9 f11)
  1.1901 +#626 := (= f1 #247)
  1.1902 +#623 := (not #626)
  1.1903 +#337 := (f3 f9 f10)
  1.1904 +#353 := (= f1 #337)
  1.1905 +#354 := (not #353)
  1.1906 +#612 := (or #354 #623)
  1.1907 +#613 := (not #612)
  1.1908 +#609 := (iff #613 #649)
  1.1909 +#580 := (not #609)
  1.1910 +decl f12 :: S3
  1.1911 +#44 := f12
  1.1912 +#332 := (f3 f9 f12)
  1.1913 +#329 := (= f1 #332)
  1.1914 +#333 := (not #329)
  1.1915 +#482 := (or #333 #623)
  1.1916 +#491 := (not #482)
  1.1917 +#43 := (f8 f11)
  1.1918 +#45 := (f6 #43 f12)
  1.1919 +#644 := (f3 f9 #45)
  1.1920 +#630 := (= f1 #644)
  1.1921 +#492 := (iff #491 #630)
  1.1922 +#585 := (not #492)
  1.1923 +#565 := [hypothesis]: #585
  1.1924 +#21 := (:var 0 S3)
  1.1925 +#19 := (:var 1 S3)
  1.1926 +#32 := (f8 #19)
  1.1927 +#33 := (f6 #32 #21)
  1.1928 +#18 := (:var 2 S2)
  1.1929 +#34 := (f3 #18 #33)
  1.1930 +#678 := (pattern #34)
  1.1931 +#27 := (f3 #18 #21)
  1.1932 +#101 := (= f1 #27)
  1.1933 +#174 := (not #101)
  1.1934 +#25 := (f3 #18 #19)
  1.1935 +#98 := (= f1 #25)
  1.1936 +#173 := (not #98)
  1.1937 +#157 := (or #173 #174)
  1.1938 +#158 := (not #157)
  1.1939 +#114 := (= f1 #34)
  1.1940 +#175 := (iff #114 #158)
  1.1941 +#679 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #678) #175)
  1.1942 +#178 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #175)
  1.1943 +#682 := (iff #178 #679)
  1.1944 +#680 := (iff #175 #175)
  1.1945 +#681 := [refl]: #680
  1.1946 +#683 := [quant-intro #681]: #682
  1.1947 +#118 := (and #98 #101)
  1.1948 +#121 := (iff #114 #118)
  1.1949 +#124 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #121)
  1.1950 +#179 := (iff #124 #178)
  1.1951 +#176 := (iff #121 #175)
  1.1952 +#159 := (iff #118 #158)
  1.1953 +#160 := [rewrite]: #159
  1.1954 +#177 := [monotonicity #160]: #176
  1.1955 +#180 := [quant-intro #177]: #179
  1.1956 +#155 := (~ #124 #124)
  1.1957 +#170 := (~ #121 #121)
  1.1958 +#171 := [refl]: #170
  1.1959 +#156 := [nnf-pos #171]: #155
  1.1960 +#28 := (= #27 f1)
  1.1961 +#26 := (= #25 f1)
  1.1962 +#36 := (and #26 #28)
  1.1963 +#35 := (= #34 f1)
  1.1964 +#37 := (iff #35 #36)
  1.1965 +#38 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #37)
  1.1966 +#125 := (iff #38 #124)
  1.1967 +#122 := (iff #37 #121)
  1.1968 +#119 := (iff #36 #118)
  1.1969 +#102 := (iff #28 #101)
  1.1970 +#103 := [rewrite]: #102
  1.1971 +#99 := (iff #26 #98)
  1.1972 +#100 := [rewrite]: #99
  1.1973 +#120 := [monotonicity #100 #103]: #119
  1.1974 +#116 := (iff #35 #114)
  1.1975 +#117 := [rewrite]: #116
  1.1976 +#123 := [monotonicity #117 #120]: #122
  1.1977 +#126 := [quant-intro #123]: #125
  1.1978 +#113 := [asserted]: #38
  1.1979 +#129 := [mp #113 #126]: #124
  1.1980 +#172 := [mp~ #129 #156]: #124
  1.1981 +#181 := [mp #172 #180]: #178
  1.1982 +#684 := [mp #181 #683]: #679
  1.1983 +#304 := (not #679)
  1.1984 +#496 := (or #304 #492)
  1.1985 +#598 := (or #623 #333)
  1.1986 +#480 := (not #598)
  1.1987 +#481 := (iff #630 #480)
  1.1988 +#497 := (or #304 #481)
  1.1989 +#591 := (iff #497 #496)
  1.1990 +#592 := (iff #496 #496)
  1.1991 +#579 := [rewrite]: #592
  1.1992 +#494 := (iff #481 #492)
  1.1993 +#590 := (iff #630 #491)
  1.1994 +#493 := (iff #590 #492)
  1.1995 +#486 := [rewrite]: #493
  1.1996 +#475 := (iff #481 #590)
  1.1997 +#586 := (iff #480 #491)
  1.1998 +#441 := (iff #598 #482)
  1.1999 +#589 := [rewrite]: #441
  1.2000 +#587 := [monotonicity #589]: #586
  1.2001 +#490 := [monotonicity #587]: #475
  1.2002 +#495 := [trans #490 #486]: #494
  1.2003 +#588 := [monotonicity #495]: #591
  1.2004 +#581 := [trans #588 #579]: #591
  1.2005 +#498 := [quant-inst #39 #42 #44]: #497
  1.2006 +#573 := [mp #498 #581]: #496
  1.2007 +#566 := [unit-resolution #573 #684 #565]: false
  1.2008 +#567 := [lemma #566]: #492
  1.2009 +#631 := (not #630)
  1.2010 +#355 := (or #354 #631)
  1.2011 +#341 := (not #355)
  1.2012 +#46 := (f6 #41 #45)
  1.2013 +#47 := (f3 f9 #46)
  1.2014 +#128 := (= f1 #47)
  1.2015 +#141 := (not #128)
  1.2016 +#568 := [hypothesis]: #141
  1.2017 +#569 := (or #128 #355)
  1.2018 +#356 := (iff #128 #341)
  1.2019 +#627 := (or #304 #356)
  1.2020 +#349 := [quant-inst #39 #40 #45]: #627
  1.2021 +#564 := [unit-resolution #349 #684]: #356
  1.2022 +#339 := (not #356)
  1.2023 +#340 := (or #339 #128 #355)
  1.2024 +#342 := [def-axiom]: #340
  1.2025 +#555 := [unit-resolution #342 #564]: #569
  1.2026 +#556 := [unit-resolution #555 #568]: #355
  1.2027 +#595 := (or #304 #609)
  1.2028 +#614 := (iff #649 #613)
  1.2029 +#611 := (or #304 #614)
  1.2030 +#616 := (iff #611 #595)
  1.2031 +#459 := (iff #595 #595)
  1.2032 +#460 := [rewrite]: #459
  1.2033 +#610 := (iff #614 #609)
  1.2034 +#615 := [rewrite]: #610
  1.2035 +#458 := [monotonicity #615]: #616
  1.2036 +#602 := [trans #458 #460]: #616
  1.2037 +#617 := [quant-inst #39 #40 #42]: #611
  1.2038 +#603 := [mp #617 #602]: #595
  1.2039 +#558 := [unit-resolution #603 #684]: #609
  1.2040 +#544 := (or #580 #613)
  1.2041 +#651 := (not #649)
  1.2042 +#317 := (or #333 #651)
  1.2043 +#653 := (not #317)
  1.2044 +#50 := (f8 #49)
  1.2045 +#51 := (f6 #50 f12)
  1.2046 +#52 := (f3 f9 #51)
  1.2047 +#132 := (= f1 #52)
  1.2048 +#327 := (or #132 #128)
  1.2049 +#142 := (iff #132 #141)
  1.2050 +#53 := (= #52 f1)
  1.2051 +#48 := (= #47 f1)
  1.2052 +#54 := (iff #48 #53)
  1.2053 +#55 := (not #54)
  1.2054 +#145 := (iff #55 #142)
  1.2055 +#135 := (iff #128 #132)
  1.2056 +#138 := (not #135)
  1.2057 +#143 := (iff #138 #142)
  1.2058 +#144 := [rewrite]: #143
  1.2059 +#139 := (iff #55 #138)
  1.2060 +#136 := (iff #54 #135)
  1.2061 +#133 := (iff #53 #132)
  1.2062 +#134 := [rewrite]: #133
  1.2063 +#130 := (iff #48 #128)
  1.2064 +#131 := [rewrite]: #130
  1.2065 +#137 := [monotonicity #131 #134]: #136
  1.2066 +#140 := [monotonicity #137]: #139
  1.2067 +#146 := [trans #140 #144]: #145
  1.2068 +#127 := [asserted]: #55
  1.2069 +#149 := [mp #127 #146]: #142
  1.2070 +#239 := (not #142)
  1.2071 +#326 := (or #132 #128 #239)
  1.2072 +#240 := [def-axiom]: #326
  1.2073 +#241 := [unit-resolution #240 #149]: #327
  1.2074 +#559 := [unit-resolution #241 #568]: #132
  1.2075 +#328 := (not #132)
  1.2076 +#557 := (or #328 #653)
  1.2077 +#650 := (iff #132 #653)
  1.2078 +#309 := (or #304 #650)
  1.2079 +#306 := (or #651 #333)
  1.2080 +#438 := (not #306)
  1.2081 +#645 := (iff #132 #438)
  1.2082 +#647 := (or #304 #645)
  1.2083 +#648 := (iff #647 #309)
  1.2084 +#632 := (iff #309 #309)
  1.2085 +#293 := [rewrite]: #632
  1.2086 +#656 := (iff #645 #650)
  1.2087 +#654 := (iff #438 #653)
  1.2088 +#318 := (iff #306 #317)
  1.2089 +#652 := [rewrite]: #318
  1.2090 +#655 := [monotonicity #652]: #654
  1.2091 +#646 := [monotonicity #655]: #656
  1.2092 +#289 := [monotonicity #646]: #648
  1.2093 +#294 := [trans #289 #293]: #648
  1.2094 +#305 := [quant-inst #39 #49 #44]: #647
  1.2095 +#295 := [mp #305 #294]: #309
  1.2096 +#560 := [unit-resolution #295 #684]: #650
  1.2097 +#633 := (not #650)
  1.2098 +#640 := (or #633 #328 #653)
  1.2099 +#642 := [def-axiom]: #640
  1.2100 +#561 := [unit-resolution #642 #560]: #557
  1.2101 +#541 := [unit-resolution #561 #559]: #653
  1.2102 +#635 := (or #317 #649)
  1.2103 +#636 := [def-axiom]: #635
  1.2104 +#542 := [unit-resolution #636 #541]: #649
  1.2105 +#574 := (or #580 #613 #651)
  1.2106 +#575 := [def-axiom]: #574
  1.2107 +#545 := [unit-resolution #575 #542]: #544
  1.2108 +#546 := [unit-resolution #545 #558]: #613
  1.2109 +#604 := (or #612 #353)
  1.2110 +#570 := [def-axiom]: #604
  1.2111 +#547 := [unit-resolution #570 #546]: #353
  1.2112 +#629 := (or #341 #354 #631)
  1.2113 +#338 := [def-axiom]: #629
  1.2114 +#548 := [unit-resolution #338 #547 #556]: #631
  1.2115 +#296 := (or #317 #329)
  1.2116 +#634 := [def-axiom]: #296
  1.2117 +#549 := [unit-resolution #634 #541]: #329
  1.2118 +#572 := (or #612 #626)
  1.2119 +#582 := [def-axiom]: #572
  1.2120 +#550 := [unit-resolution #582 #546]: #626
  1.2121 +#607 := (or #491 #333 #623)
  1.2122 +#601 := [def-axiom]: #607
  1.2123 +#551 := [unit-resolution #601 #550 #549]: #491
  1.2124 +#439 := (or #585 #482 #630)
  1.2125 +#440 := [def-axiom]: #439
  1.2126 +#552 := [unit-resolution #440 #551 #548 #567]: false
  1.2127 +#553 := [lemma #552]: #128
  1.2128 +#543 := (or #141 #341)
  1.2129 +#620 := (or #339 #141 #341)
  1.2130 +#621 := [def-axiom]: #620
  1.2131 +#554 := [unit-resolution #621 #564]: #543
  1.2132 +#532 := [unit-resolution #554 #553]: #341
  1.2133 +#628 := (or #355 #630)
  1.2134 +#625 := [def-axiom]: #628
  1.2135 +#533 := [unit-resolution #625 #532]: #630
  1.2136 +#608 := (or #585 #491 #631)
  1.2137 +#437 := [def-axiom]: #608
  1.2138 +#535 := [unit-resolution #437 #533 #567]: #491
  1.2139 +#600 := (or #482 #626)
  1.2140 +#606 := [def-axiom]: #600
  1.2141 +#536 := [unit-resolution #606 #535]: #626
  1.2142 +#350 := (or #355 #353)
  1.2143 +#624 := [def-axiom]: #350
  1.2144 +#537 := [unit-resolution #624 #532]: #353
  1.2145 +#583 := (or #613 #354 #623)
  1.2146 +#584 := [def-axiom]: #583
  1.2147 +#538 := [unit-resolution #584 #537 #536]: #613
  1.2148 +#331 := (or #328 #141)
  1.2149 +#319 := (or #328 #141 #239)
  1.2150 +#330 := [def-axiom]: #319
  1.2151 +#259 := [unit-resolution #330 #149]: #331
  1.2152 +#539 := [unit-resolution #259 #553]: #328
  1.2153 +#534 := (or #132 #317)
  1.2154 +#639 := (or #633 #132 #317)
  1.2155 +#275 := [def-axiom]: #639
  1.2156 +#540 := [unit-resolution #275 #560]: #534
  1.2157 +#526 := [unit-resolution #540 #539]: #317
  1.2158 +#605 := (or #482 #329)
  1.2159 +#599 := [def-axiom]: #605
  1.2160 +#522 := [unit-resolution #599 #535]: #329
  1.2161 +#637 := (or #653 #333 #651)
  1.2162 +#638 := [def-axiom]: #637
  1.2163 +#523 := [unit-resolution #638 #522 #526]: #651
  1.2164 +#576 := (or #580 #612 #649)
  1.2165 +#577 := [def-axiom]: #576
  1.2166 +#524 := [unit-resolution #577 #523 #538]: #580
  1.2167 +[unit-resolution #603 #684 #524]: false
  1.2168 +unsat
  1.2169 +a7bc4cb1c082efb5c0f6c878be007f36211e0adf 20 0
  1.2170 +#2 := false
  1.2171 +decl f12 :: (-> S3 S3)
  1.2172 +decl f4 :: S3
  1.2173 +#8 := f4
  1.2174 +#48 := (f12 f4)
  1.2175 +#49 := (= #48 #48)
  1.2176 +#50 := (not #49)
  1.2177 +#145 := (iff #50 false)
  1.2178 +#1 := true
  1.2179 +#140 := (not true)
  1.2180 +#143 := (iff #140 false)
  1.2181 +#144 := [rewrite]: #143
  1.2182 +#141 := (iff #50 #140)
  1.2183 +#137 := (iff #49 true)
  1.2184 +#139 := [rewrite]: #137
  1.2185 +#142 := [monotonicity #139]: #141
  1.2186 +#146 := [trans #142 #144]: #145
  1.2187 +#136 := [asserted]: #50
  1.2188 +[mp #136 #146]: false
  1.2189 +unsat
     2.1 --- a/src/HOL/SMT_Examples/SMT_Tests.thy	Wed Sep 14 10:24:22 2011 +0200
     2.2 +++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Wed Sep 14 10:55:07 2011 +0200
     2.3 @@ -937,32 +937,26 @@
     2.4  
     2.5  section {* Sets *}
     2.6  
     2.7 -lemma smt_sets:
     2.8 -  "\<not>({} x)"
     2.9 -  "UNIV x"
    2.10 -  "(A \<union> B) x = (A x \<or> B x)"
    2.11 -  "(A \<inter> B) x = (A x \<and> B x)"
    2.12 -  by auto
    2.13 +lemma Empty: "x \<notin> {}" by simp
    2.14 +
    2.15 +lemmas smt_sets = Empty UNIV_I Un_iff Int_iff
    2.16  
    2.17  lemma
    2.18 -  "x \<in> P = P x"
    2.19 -  "x \<in> {x. P x} = P x"
    2.20    "x \<notin> {}"
    2.21    "x \<in> UNIV"
    2.22 -  "x \<in> P \<union> Q = (P x \<or> Q x)"
    2.23 -  "x \<in> P \<union> {} = P x"
    2.24 +  "x \<in> A \<union> B \<longleftrightarrow> x \<in> A \<or> x \<in> B"
    2.25 +  "x \<in> P \<union> {} \<longleftrightarrow> x \<in> P"
    2.26    "x \<in> P \<union> UNIV"
    2.27 -  "(x \<in> P \<union> Q) = (x \<in> Q \<union> P)"
    2.28 -  "(x \<in> P \<union> P) = (x \<in> P)"
    2.29 -  "(x \<in> P \<union> (Q \<union> R)) = (x \<in> (P \<union> Q) \<union> R)"
    2.30 -  "(x \<in> P \<inter> Q) = (P x \<and> Q x)"
    2.31 +  "x \<in> P \<union> Q \<longleftrightarrow> x \<in> Q \<union> P"
    2.32 +  "x \<in> P \<union> P \<longleftrightarrow> x \<in> P"
    2.33 +  "x \<in> P \<union> (Q \<union> R) \<longleftrightarrow> x \<in> (P \<union> Q) \<union> R"
    2.34 +  "x \<in> A \<inter> B \<longleftrightarrow> x \<in> A \<and> x \<in> B"
    2.35    "x \<notin> P \<inter> {}"
    2.36 -  "(x \<in> P \<inter> UNIV) = (x \<in> P)"
    2.37 -  "(x \<in> P \<inter> Q) = (x \<in> Q \<inter> P)"
    2.38 -  "(x \<in> P \<inter> P) = (x \<in> P)"
    2.39 -  "(x \<in> P \<inter> (Q \<inter> R)) = (x \<in> (P \<inter> Q) \<inter> R)"
    2.40 -  "{x. P x} = {y. P y}"
    2.41 -  unfolding mem_def Collect_def
    2.42 +  "x \<in> P \<inter> UNIV \<longleftrightarrow> x \<in> P"
    2.43 +  "x \<in> P \<inter> Q \<longleftrightarrow> x \<in> Q \<inter> P"
    2.44 +  "x \<in> P \<inter> P \<longleftrightarrow> x \<in> P"
    2.45 +  "x \<in> P \<inter> (Q \<inter> R) \<longleftrightarrow> x \<in> (P \<inter> Q) \<inter> R"
    2.46 +  "{x. x \<in> P} = {y. y \<in> P}"
    2.47    by (smt smt_sets)+
    2.48  
    2.49  end