1.1 --- a/src/HOL/SMT_Examples/SMT_Tests.certs Sat Dec 24 16:14:59 2011 +0100
1.2 +++ b/src/HOL/SMT_Examples/SMT_Tests.certs Sun Dec 25 08:42:33 2011 +0100
1.3 @@ -62737,3 +62737,4421 @@
1.4 #136 := [asserted]: #50
1.5 [mp #136 #146]: false
1.6 unsat
1.7 +eac8197a82f6b3a5c2024430d69641bb761b0abc 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 f10 :: S2
1.13 +#41 := f10
1.14 +#42 := (f3 f10 f4)
1.15 +decl f1 :: S1
1.16 +#4 := f1
1.17 +#118 := (= f1 #42)
1.18 +#43 := (= #42 f1)
1.19 +#44 := (not #43)
1.20 +#45 := (not #44)
1.21 +#130 := (iff #45 #118)
1.22 +#122 := (not #118)
1.23 +#125 := (not #122)
1.24 +#128 := (iff #125 #118)
1.25 +#129 := [rewrite]: #128
1.26 +#126 := (iff #45 #125)
1.27 +#123 := (iff #44 #122)
1.28 +#120 := (iff #43 #118)
1.29 +#121 := [rewrite]: #120
1.30 +#124 := [monotonicity #121]: #123
1.31 +#127 := [monotonicity #124]: #126
1.32 +#131 := [trans #127 #129]: #130
1.33 +#117 := [asserted]: #45
1.34 +#134 := [mp #117 #131]: #118
1.35 +#8 := (:var 0 S2)
1.36 +#10 := (f3 #8 f4)
1.37 +#642 := (pattern #10)
1.38 +#66 := (= f1 #10)
1.39 +#69 := (not #66)
1.40 +#643 := (forall (vars (?v0 S2)) (:pat #642) #69)
1.41 +#72 := (forall (vars (?v0 S2)) #69)
1.42 +#646 := (iff #72 #643)
1.43 +#644 := (iff #69 #69)
1.44 +#645 := [refl]: #644
1.45 +#647 := [quant-intro #645]: #646
1.46 +#148 := (~ #72 #72)
1.47 +#146 := (~ #69 #69)
1.48 +#147 := [refl]: #146
1.49 +#149 := [nnf-pos #147]: #148
1.50 +#11 := (= #10 f1)
1.51 +#12 := (not #11)
1.52 +#13 := (forall (vars (?v0 S2)) #12)
1.53 +#73 := (iff #13 #72)
1.54 +#70 := (iff #12 #69)
1.55 +#67 := (iff #11 #66)
1.56 +#68 := [rewrite]: #67
1.57 +#71 := [monotonicity #68]: #70
1.58 +#74 := [quant-intro #71]: #73
1.59 +#65 := [asserted]: #13
1.60 +#77 := [mp #65 #74]: #72
1.61 +#133 := [mp~ #77 #149]: #72
1.62 +#648 := [mp #133 #647]: #643
1.63 +#225 := (not #643)
1.64 +#312 := (or #225 #122)
1.65 +#226 := [quant-inst #41]: #312
1.66 +[unit-resolution #226 #648 #134]: false
1.67 +unsat
1.68 +32295808d649b2df10d022ec20bfa2f501001522 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 f10 :: S2
1.74 +#41 := f10
1.75 +#42 := (f3 f10 f5)
1.76 +decl f1 :: S1
1.77 +#4 := f1
1.78 +#117 := (= f1 #42)
1.79 +#121 := (not #117)
1.80 +#43 := (= #42 f1)
1.81 +#44 := (not #43)
1.82 +#122 := (iff #44 #121)
1.83 +#119 := (iff #43 #117)
1.84 +#120 := [rewrite]: #119
1.85 +#123 := [monotonicity #120]: #122
1.86 +#116 := [asserted]: #44
1.87 +#126 := [mp #116 #123]: #121
1.88 +#8 := (:var 0 S2)
1.89 +#15 := (f3 #8 f5)
1.90 +#641 := (pattern #15)
1.91 +#75 := (= f1 #15)
1.92 +#642 := (forall (vars (?v0 S2)) (:pat #641) #75)
1.93 +#79 := (forall (vars (?v0 S2)) #75)
1.94 +#645 := (iff #79 #642)
1.95 +#643 := (iff #75 #75)
1.96 +#644 := [refl]: #643
1.97 +#646 := [quant-intro #644]: #645
1.98 +#128 := (~ #79 #79)
1.99 +#127 := (~ #75 #75)
1.100 +#142 := [refl]: #127
1.101 +#129 := [nnf-pos #142]: #128
1.102 +#16 := (= #15 f1)
1.103 +#17 := (forall (vars (?v0 S2)) #16)
1.104 +#80 := (iff #17 #79)
1.105 +#77 := (iff #16 #75)
1.106 +#78 := [rewrite]: #77
1.107 +#81 := [quant-intro #78]: #80
1.108 +#74 := [asserted]: #17
1.109 +#84 := [mp #74 #81]: #79
1.110 +#143 := [mp~ #84 #129]: #79
1.111 +#647 := [mp #143 #646]: #642
1.112 +#217 := (not #642)
1.113 +#304 := (or #217 #117)
1.114 +#218 := [quant-inst #41]: #304
1.115 +[unit-resolution #218 #647 #126]: false
1.116 +unsat
1.117 +dfe83e391823f1cbfcca9d6fb06c0ae74a22248a 126 0
1.118 +#2 := false
1.119 +decl f3 :: (-> S2 S3 S1)
1.120 +decl f6 :: (-> S4 S3 S3)
1.121 +decl f12 :: S3
1.122 +#44 := f12
1.123 +decl f7 :: (-> S5 S3 S4)
1.124 +decl f11 :: S3
1.125 +#42 := f11
1.126 +decl f8 :: S5
1.127 +#19 := f8
1.128 +#43 := (f7 f8 f11)
1.129 +#45 := (f6 #43 f12)
1.130 +decl f10 :: S2
1.131 +#41 := f10
1.132 +#46 := (f3 f10 #45)
1.133 +decl f1 :: S1
1.134 +#4 := f1
1.135 +#127 := (= f1 #46)
1.136 +#146 := (not #127)
1.137 +#650 := [hypothesis]: #146
1.138 +#50 := (f3 f10 f12)
1.139 +#134 := (= f1 #50)
1.140 +#48 := (f3 f10 f11)
1.141 +#131 := (= f1 #48)
1.142 +#137 := (or #131 #134)
1.143 +#338 := (or #137 #127)
1.144 +#147 := (iff #137 #146)
1.145 +#51 := (= #50 f1)
1.146 +#49 := (= #48 f1)
1.147 +#52 := (or #49 #51)
1.148 +#47 := (= #46 f1)
1.149 +#53 := (iff #47 #52)
1.150 +#54 := (not #53)
1.151 +#150 := (iff #54 #147)
1.152 +#140 := (iff #127 #137)
1.153 +#143 := (not #140)
1.154 +#148 := (iff #143 #147)
1.155 +#149 := [rewrite]: #148
1.156 +#144 := (iff #54 #143)
1.157 +#141 := (iff #53 #140)
1.158 +#138 := (iff #52 #137)
1.159 +#135 := (iff #51 #134)
1.160 +#136 := [rewrite]: #135
1.161 +#132 := (iff #49 #131)
1.162 +#133 := [rewrite]: #132
1.163 +#139 := [monotonicity #133 #136]: #138
1.164 +#129 := (iff #47 #127)
1.165 +#130 := [rewrite]: #129
1.166 +#142 := [monotonicity #130 #139]: #141
1.167 +#145 := [monotonicity #142]: #144
1.168 +#151 := [trans #145 #149]: #150
1.169 +#126 := [asserted]: #54
1.170 +#154 := [mp #126 #151]: #147
1.171 +#264 := (not #147)
1.172 +#337 := (or #137 #127 #264)
1.173 +#334 := [def-axiom]: #337
1.174 +#317 := [unit-resolution #334 #154]: #338
1.175 +#322 := [unit-resolution #317 #650]: #137
1.176 +#324 := (not #137)
1.177 +#653 := (or #127 #324)
1.178 +#22 := (:var 0 S3)
1.179 +#20 := (:var 1 S3)
1.180 +#21 := (f7 f8 #20)
1.181 +#23 := (f6 #21 #22)
1.182 +#18 := (:var 2 S2)
1.183 +#24 := (f3 #18 #23)
1.184 +#676 := (pattern #24)
1.185 +#28 := (f3 #18 #22)
1.186 +#100 := (= f1 #28)
1.187 +#26 := (f3 #18 #20)
1.188 +#97 := (= f1 #26)
1.189 +#103 := (or #97 #100)
1.190 +#93 := (= f1 #24)
1.191 +#106 := (iff #93 #103)
1.192 +#677 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #676) #106)
1.193 +#109 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #106)
1.194 +#680 := (iff #109 #677)
1.195 +#678 := (iff #106 #106)
1.196 +#679 := [refl]: #678
1.197 +#681 := [quant-intro #679]: #680
1.198 +#158 := (~ #109 #109)
1.199 +#172 := (~ #106 #106)
1.200 +#173 := [refl]: #172
1.201 +#159 := [nnf-pos #173]: #158
1.202 +#29 := (= #28 f1)
1.203 +#27 := (= #26 f1)
1.204 +#30 := (or #27 #29)
1.205 +#25 := (= #24 f1)
1.206 +#31 := (iff #25 #30)
1.207 +#32 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #31)
1.208 +#110 := (iff #32 #109)
1.209 +#107 := (iff #31 #106)
1.210 +#104 := (iff #30 #103)
1.211 +#101 := (iff #29 #100)
1.212 +#102 := [rewrite]: #101
1.213 +#98 := (iff #27 #97)
1.214 +#99 := [rewrite]: #98
1.215 +#105 := [monotonicity #99 #102]: #104
1.216 +#95 := (iff #25 #93)
1.217 +#96 := [rewrite]: #95
1.218 +#108 := [monotonicity #96 #105]: #107
1.219 +#111 := [quant-intro #108]: #110
1.220 +#92 := [asserted]: #32
1.221 +#114 := [mp #92 #111]: #109
1.222 +#174 := [mp~ #114 #159]: #109
1.223 +#682 := [mp #174 #681]: #677
1.224 +#323 := (not #677)
1.225 +#657 := (or #323 #140)
1.226 +#658 := [quant-inst #41 #42 #44]: #657
1.227 +#310 := [unit-resolution #658 #682]: #140
1.228 +#659 := (or #143 #127 #324)
1.229 +#660 := [def-axiom]: #659
1.230 +#294 := [unit-resolution #660 #310]: #653
1.231 +#637 := [unit-resolution #294 #322 #650]: false
1.232 +#298 := [lemma #637]: #127
1.233 +#311 := (or #324 #146)
1.234 +#654 := (or #324 #146 #264)
1.235 +#656 := [def-axiom]: #654
1.236 +#443 := [unit-resolution #656 #154]: #311
1.237 +#299 := [unit-resolution #443 #298]: #324
1.238 +#300 := (or #146 #137)
1.239 +#655 := (or #143 #146 #137)
1.240 +#661 := [def-axiom]: #655
1.241 +#301 := [unit-resolution #661 #310]: #300
1.242 +[unit-resolution #301 #299 #298]: false
1.243 +unsat
1.244 +54d5adcc9aa92b5c35a0e590a6651cbf7d0b828e 162 0
1.245 +#2 := false
1.246 +decl f3 :: (-> S2 S3 S1)
1.247 +decl f4 :: S3
1.248 +#9 := f4
1.249 +decl f10 :: S2
1.250 +#41 := f10
1.251 +#327 := (f3 f10 f4)
1.252 +decl f1 :: S1
1.253 +#4 := f1
1.254 +#324 := (= f1 #327)
1.255 +decl f11 :: S3
1.256 +#42 := f11
1.257 +#47 := (f3 f10 f11)
1.258 +#127 := (= f1 #47)
1.259 +#328 := (or #127 #324)
1.260 +decl f6 :: (-> S4 S3 S3)
1.261 +decl f7 :: (-> S5 S3 S4)
1.262 +decl f8 :: S5
1.263 +#19 := f8
1.264 +#43 := (f7 f8 f11)
1.265 +#44 := (f6 #43 f4)
1.266 +#45 := (f3 f10 #44)
1.267 +#123 := (= f1 #45)
1.268 +#136 := (not #123)
1.269 +#644 := [hypothesis]: #136
1.270 +#322 := (or #127 #123)
1.271 +#137 := (iff #127 #136)
1.272 +#48 := (= #47 f1)
1.273 +#46 := (= #45 f1)
1.274 +#49 := (iff #46 #48)
1.275 +#50 := (not #49)
1.276 +#140 := (iff #50 #137)
1.277 +#130 := (iff #123 #127)
1.278 +#133 := (not #130)
1.279 +#138 := (iff #133 #137)
1.280 +#139 := [rewrite]: #138
1.281 +#134 := (iff #50 #133)
1.282 +#131 := (iff #49 #130)
1.283 +#128 := (iff #48 #127)
1.284 +#129 := [rewrite]: #128
1.285 +#125 := (iff #46 #123)
1.286 +#126 := [rewrite]: #125
1.287 +#132 := [monotonicity #126 #129]: #131
1.288 +#135 := [monotonicity #132]: #134
1.289 +#141 := [trans #135 #139]: #140
1.290 +#122 := [asserted]: #50
1.291 +#144 := [mp #122 #141]: #137
1.292 +#234 := (not #137)
1.293 +#321 := (or #127 #123 #234)
1.294 +#235 := [def-axiom]: #321
1.295 +#236 := [unit-resolution #235 #144]: #322
1.296 +#646 := [unit-resolution #236 #644]: #127
1.297 +#650 := (not #328)
1.298 +#290 := (or #123 #650)
1.299 +#307 := (iff #123 #328)
1.300 +#22 := (:var 0 S3)
1.301 +#20 := (:var 1 S3)
1.302 +#21 := (f7 f8 #20)
1.303 +#23 := (f6 #21 #22)
1.304 +#18 := (:var 2 S2)
1.305 +#24 := (f3 #18 #23)
1.306 +#666 := (pattern #24)
1.307 +#28 := (f3 #18 #22)
1.308 +#96 := (= f1 #28)
1.309 +#26 := (f3 #18 #20)
1.310 +#93 := (= f1 #26)
1.311 +#99 := (or #93 #96)
1.312 +#89 := (= f1 #24)
1.313 +#102 := (iff #89 #99)
1.314 +#667 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #666) #102)
1.315 +#105 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #102)
1.316 +#670 := (iff #105 #667)
1.317 +#668 := (iff #102 #102)
1.318 +#669 := [refl]: #668
1.319 +#671 := [quant-intro #669]: #670
1.320 +#148 := (~ #105 #105)
1.321 +#162 := (~ #102 #102)
1.322 +#163 := [refl]: #162
1.323 +#149 := [nnf-pos #163]: #148
1.324 +#29 := (= #28 f1)
1.325 +#27 := (= #26 f1)
1.326 +#30 := (or #27 #29)
1.327 +#25 := (= #24 f1)
1.328 +#31 := (iff #25 #30)
1.329 +#32 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #31)
1.330 +#106 := (iff #32 #105)
1.331 +#103 := (iff #31 #102)
1.332 +#100 := (iff #30 #99)
1.333 +#97 := (iff #29 #96)
1.334 +#98 := [rewrite]: #97
1.335 +#94 := (iff #27 #93)
1.336 +#95 := [rewrite]: #94
1.337 +#101 := [monotonicity #95 #98]: #100
1.338 +#91 := (iff #25 #89)
1.339 +#92 := [rewrite]: #91
1.340 +#104 := [monotonicity #92 #101]: #103
1.341 +#107 := [quant-intro #104]: #106
1.342 +#88 := [asserted]: #32
1.343 +#110 := [mp #88 #107]: #105
1.344 +#164 := [mp~ #110 #149]: #105
1.345 +#672 := [mp #164 #671]: #667
1.346 +#301 := (not #667)
1.347 +#433 := (or #301 #307)
1.348 +#640 := [quant-inst #41 #42 #9]: #433
1.349 +#289 := [unit-resolution #640 #672]: #307
1.350 +#641 := (not #307)
1.351 +#299 := (or #641 #123 #650)
1.352 +#304 := [def-axiom]: #299
1.353 +#291 := [unit-resolution #304 #289]: #290
1.354 +#629 := [unit-resolution #291 #644]: #650
1.355 +#323 := (not #127)
1.356 +#312 := (or #328 #323)
1.357 +#313 := [def-axiom]: #312
1.358 +#630 := [unit-resolution #313 #629 #646]: false
1.359 +#631 := [lemma #630]: #123
1.360 +#632 := (or #136 #328)
1.361 +#642 := (or #641 #136 #328)
1.362 +#300 := [def-axiom]: #642
1.363 +#633 := [unit-resolution #300 #289]: #632
1.364 +#635 := [unit-resolution #633 #631]: #328
1.365 +#326 := (or #323 #136)
1.366 +#314 := (or #323 #136 #234)
1.367 +#325 := [def-axiom]: #314
1.368 +#254 := [unit-resolution #325 #144]: #326
1.369 +#637 := [unit-resolution #254 #631]: #323
1.370 +#645 := (or #650 #127 #324)
1.371 +#651 := [def-axiom]: #645
1.372 +#275 := [unit-resolution #651 #637 #635]: #324
1.373 +#8 := (:var 0 S2)
1.374 +#10 := (f3 #8 f4)
1.375 +#652 := (pattern #10)
1.376 +#71 := (= f1 #10)
1.377 +#74 := (not #71)
1.378 +#653 := (forall (vars (?v0 S2)) (:pat #652) #74)
1.379 +#77 := (forall (vars (?v0 S2)) #74)
1.380 +#656 := (iff #77 #653)
1.381 +#654 := (iff #74 #74)
1.382 +#655 := [refl]: #654
1.383 +#657 := [quant-intro #655]: #656
1.384 +#158 := (~ #77 #77)
1.385 +#156 := (~ #74 #74)
1.386 +#157 := [refl]: #156
1.387 +#159 := [nnf-pos #157]: #158
1.388 +#11 := (= #10 f1)
1.389 +#12 := (not #11)
1.390 +#13 := (forall (vars (?v0 S2)) #12)
1.391 +#78 := (iff #13 #77)
1.392 +#75 := (iff #12 #74)
1.393 +#72 := (iff #11 #71)
1.394 +#73 := [rewrite]: #72
1.395 +#76 := [monotonicity #73]: #75
1.396 +#79 := [quant-intro #76]: #78
1.397 +#70 := [asserted]: #13
1.398 +#82 := [mp #70 #79]: #77
1.399 +#143 := [mp~ #82 #159]: #77
1.400 +#658 := [mp #143 #657]: #653
1.401 +#647 := (not #324)
1.402 +#628 := (not #653)
1.403 +#634 := (or #628 #647)
1.404 +#270 := [quant-inst #41]: #634
1.405 +[unit-resolution #270 #658 #275]: false
1.406 +unsat
1.407 +6579b339206079120a92afc0dda92279c34507ae 136 0
1.408 +#2 := false
1.409 +decl f3 :: (-> S2 S3 S1)
1.410 +decl f5 :: S3
1.411 +#14 := f5
1.412 +decl f10 :: S2
1.413 +#41 := f10
1.414 +#219 := (f3 f10 f5)
1.415 +decl f1 :: S1
1.416 +#4 := f1
1.417 +#306 := (= f1 #219)
1.418 +#633 := (not #306)
1.419 +decl f11 :: S3
1.420 +#42 := f11
1.421 +#220 := (f3 f10 f11)
1.422 +#307 := (= f1 #220)
1.423 +#299 := (or #306 #307)
1.424 +#284 := (not #299)
1.425 +decl f6 :: (-> S4 S3 S3)
1.426 +decl f7 :: (-> S5 S3 S4)
1.427 +decl f8 :: S5
1.428 +#19 := f8
1.429 +#43 := (f7 f8 f11)
1.430 +#44 := (f6 #43 f5)
1.431 +#45 := (f3 f10 #44)
1.432 +#120 := (= f1 #45)
1.433 +#239 := (iff #120 #299)
1.434 +#22 := (:var 0 S3)
1.435 +#20 := (:var 1 S3)
1.436 +#21 := (f7 f8 #20)
1.437 +#23 := (f6 #21 #22)
1.438 +#18 := (:var 2 S2)
1.439 +#24 := (f3 #18 #23)
1.440 +#651 := (pattern #24)
1.441 +#28 := (f3 #18 #22)
1.442 +#93 := (= f1 #28)
1.443 +#26 := (f3 #18 #20)
1.444 +#90 := (= f1 #26)
1.445 +#96 := (or #90 #93)
1.446 +#86 := (= f1 #24)
1.447 +#99 := (iff #86 #96)
1.448 +#652 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #651) #99)
1.449 +#102 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #99)
1.450 +#655 := (iff #102 #652)
1.451 +#653 := (iff #99 #99)
1.452 +#654 := [refl]: #653
1.453 +#656 := [quant-intro #654]: #655
1.454 +#133 := (~ #102 #102)
1.455 +#147 := (~ #99 #99)
1.456 +#148 := [refl]: #147
1.457 +#134 := [nnf-pos #148]: #133
1.458 +#29 := (= #28 f1)
1.459 +#27 := (= #26 f1)
1.460 +#30 := (or #27 #29)
1.461 +#25 := (= #24 f1)
1.462 +#31 := (iff #25 #30)
1.463 +#32 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #31)
1.464 +#103 := (iff #32 #102)
1.465 +#100 := (iff #31 #99)
1.466 +#97 := (iff #30 #96)
1.467 +#94 := (iff #29 #93)
1.468 +#95 := [rewrite]: #94
1.469 +#91 := (iff #27 #90)
1.470 +#92 := [rewrite]: #91
1.471 +#98 := [monotonicity #92 #95]: #97
1.472 +#88 := (iff #25 #86)
1.473 +#89 := [rewrite]: #88
1.474 +#101 := [monotonicity #89 #98]: #100
1.475 +#104 := [quant-intro #101]: #103
1.476 +#85 := [asserted]: #32
1.477 +#107 := [mp #85 #104]: #102
1.478 +#149 := [mp~ #107 #134]: #102
1.479 +#657 := [mp #149 #656]: #652
1.480 +#313 := (not #652)
1.481 +#292 := (or #313 #239)
1.482 +#221 := (or #307 #306)
1.483 +#308 := (iff #120 #221)
1.484 +#629 := (or #313 #308)
1.485 +#286 := (iff #629 #292)
1.486 +#625 := (iff #292 #292)
1.487 +#297 := [rewrite]: #625
1.488 +#312 := (iff #308 #239)
1.489 +#310 := (iff #221 #299)
1.490 +#311 := [rewrite]: #310
1.491 +#309 := [monotonicity #311]: #312
1.492 +#418 := [monotonicity #309]: #286
1.493 +#298 := [trans #418 #297]: #286
1.494 +#631 := [quant-inst #41 #42 #14]: #629
1.495 +#632 := [mp #631 #298]: #292
1.496 +#615 := [unit-resolution #632 #657]: #239
1.497 +#285 := (not #239)
1.498 +#616 := (or #285 #284)
1.499 +#124 := (not #120)
1.500 +#46 := (= #45 f1)
1.501 +#47 := (not #46)
1.502 +#125 := (iff #47 #124)
1.503 +#122 := (iff #46 #120)
1.504 +#123 := [rewrite]: #122
1.505 +#126 := [monotonicity #123]: #125
1.506 +#119 := [asserted]: #47
1.507 +#129 := [mp #119 #126]: #124
1.508 +#628 := (or #285 #120 #284)
1.509 +#269 := [def-axiom]: #628
1.510 +#619 := [unit-resolution #269 #129]: #616
1.511 +#255 := [unit-resolution #619 #615]: #284
1.512 +#634 := (or #299 #633)
1.513 +#635 := [def-axiom]: #634
1.514 +#620 := [unit-resolution #635 #255]: #633
1.515 +#8 := (:var 0 S2)
1.516 +#15 := (f3 #8 f5)
1.517 +#644 := (pattern #15)
1.518 +#78 := (= f1 #15)
1.519 +#645 := (forall (vars (?v0 S2)) (:pat #644) #78)
1.520 +#82 := (forall (vars (?v0 S2)) #78)
1.521 +#648 := (iff #82 #645)
1.522 +#646 := (iff #78 #78)
1.523 +#647 := [refl]: #646
1.524 +#649 := [quant-intro #647]: #648
1.525 +#131 := (~ #82 #82)
1.526 +#130 := (~ #78 #78)
1.527 +#145 := [refl]: #130
1.528 +#132 := [nnf-pos #145]: #131
1.529 +#16 := (= #15 f1)
1.530 +#17 := (forall (vars (?v0 S2)) #16)
1.531 +#83 := (iff #17 #82)
1.532 +#80 := (iff #16 #78)
1.533 +#81 := [rewrite]: #80
1.534 +#84 := [quant-intro #81]: #83
1.535 +#77 := [asserted]: #17
1.536 +#87 := [mp #77 #84]: #82
1.537 +#146 := [mp~ #87 #132]: #82
1.538 +#650 := [mp #146 #649]: #645
1.539 +#617 := (not #645)
1.540 +#618 := (or #617 #306)
1.541 +#613 := [quant-inst #41]: #618
1.542 +[unit-resolution #613 #650 #620]: false
1.543 +unsat
1.544 +21f3225a60811428730067e610d6913c3bcb0df3 155 0
1.545 +#2 := false
1.546 +decl f3 :: (-> S2 S3 S1)
1.547 +decl f6 :: (-> S4 S3 S3)
1.548 +decl f11 :: S3
1.549 +#42 := f11
1.550 +decl f7 :: (-> S5 S3 S4)
1.551 +decl f12 :: S3
1.552 +#44 := f12
1.553 +decl f8 :: S5
1.554 +#19 := f8
1.555 +#48 := (f7 f8 f12)
1.556 +#49 := (f6 #48 f11)
1.557 +decl f10 :: S2
1.558 +#41 := f10
1.559 +#50 := (f3 f10 #49)
1.560 +decl f1 :: S1
1.561 +#4 := f1
1.562 +#130 := (= f1 #50)
1.563 +#326 := (not #130)
1.564 +#43 := (f7 f8 f11)
1.565 +#45 := (f6 #43 f12)
1.566 +#46 := (f3 f10 #45)
1.567 +#126 := (= f1 #46)
1.568 +#139 := (not #126)
1.569 +#245 := [hypothesis]: #139
1.570 +#325 := (or #130 #126)
1.571 +#140 := (iff #130 #139)
1.572 +#51 := (= #50 f1)
1.573 +#47 := (= #46 f1)
1.574 +#52 := (iff #47 #51)
1.575 +#53 := (not #52)
1.576 +#143 := (iff #53 #140)
1.577 +#133 := (iff #126 #130)
1.578 +#136 := (not #133)
1.579 +#141 := (iff #136 #140)
1.580 +#142 := [rewrite]: #141
1.581 +#137 := (iff #53 #136)
1.582 +#134 := (iff #52 #133)
1.583 +#131 := (iff #51 #130)
1.584 +#132 := [rewrite]: #131
1.585 +#128 := (iff #47 #126)
1.586 +#129 := [rewrite]: #128
1.587 +#135 := [monotonicity #129 #132]: #134
1.588 +#138 := [monotonicity #135]: #137
1.589 +#144 := [trans #138 #142]: #143
1.590 +#125 := [asserted]: #53
1.591 +#147 := [mp #125 #144]: #140
1.592 +#237 := (not #140)
1.593 +#324 := (or #130 #126 #237)
1.594 +#238 := [def-axiom]: #324
1.595 +#239 := [unit-resolution #238 #147]: #325
1.596 +#624 := [unit-resolution #239 #245]: #130
1.597 +#330 := (f3 f10 f11)
1.598 +#327 := (= f1 #330)
1.599 +#331 := (f3 f10 f12)
1.600 +#310 := (= f1 #331)
1.601 +#647 := (or #310 #327)
1.602 +#644 := (not #647)
1.603 +#347 := (or #126 #644)
1.604 +#634 := (iff #126 #647)
1.605 +#22 := (:var 0 S3)
1.606 +#20 := (:var 1 S3)
1.607 +#21 := (f7 f8 #20)
1.608 +#23 := (f6 #21 #22)
1.609 +#18 := (:var 2 S2)
1.610 +#24 := (f3 #18 #23)
1.611 +#669 := (pattern #24)
1.612 +#28 := (f3 #18 #22)
1.613 +#99 := (= f1 #28)
1.614 +#26 := (f3 #18 #20)
1.615 +#96 := (= f1 #26)
1.616 +#102 := (or #96 #99)
1.617 +#92 := (= f1 #24)
1.618 +#105 := (iff #92 #102)
1.619 +#670 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #669) #105)
1.620 +#108 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #105)
1.621 +#673 := (iff #108 #670)
1.622 +#671 := (iff #105 #105)
1.623 +#672 := [refl]: #671
1.624 +#674 := [quant-intro #672]: #673
1.625 +#151 := (~ #108 #108)
1.626 +#165 := (~ #105 #105)
1.627 +#166 := [refl]: #165
1.628 +#152 := [nnf-pos #166]: #151
1.629 +#29 := (= #28 f1)
1.630 +#27 := (= #26 f1)
1.631 +#30 := (or #27 #29)
1.632 +#25 := (= #24 f1)
1.633 +#31 := (iff #25 #30)
1.634 +#32 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #31)
1.635 +#109 := (iff #32 #108)
1.636 +#106 := (iff #31 #105)
1.637 +#103 := (iff #30 #102)
1.638 +#100 := (iff #29 #99)
1.639 +#101 := [rewrite]: #100
1.640 +#97 := (iff #27 #96)
1.641 +#98 := [rewrite]: #97
1.642 +#104 := [monotonicity #98 #101]: #103
1.643 +#94 := (iff #25 #92)
1.644 +#95 := [rewrite]: #94
1.645 +#107 := [monotonicity #95 #104]: #106
1.646 +#110 := [quant-intro #107]: #109
1.647 +#91 := [asserted]: #32
1.648 +#113 := [mp #91 #110]: #108
1.649 +#167 := [mp~ #113 #152]: #108
1.650 +#675 := [mp #167 #674]: #670
1.651 +#643 := (not #670)
1.652 +#631 := (or #643 #634)
1.653 +#304 := (or #327 #310)
1.654 +#436 := (iff #126 #304)
1.655 +#637 := (or #643 #436)
1.656 +#638 := (iff #637 #631)
1.657 +#278 := (iff #631 #631)
1.658 +#279 := [rewrite]: #278
1.659 +#635 := (iff #436 #634)
1.660 +#632 := (iff #304 #647)
1.661 +#633 := [rewrite]: #632
1.662 +#636 := [monotonicity #633]: #635
1.663 +#640 := [monotonicity #636]: #638
1.664 +#641 := [trans #640 #279]: #638
1.665 +#273 := [quant-inst #41 #42 #44]: #637
1.666 +#639 := [mp #273 #641]: #631
1.667 +#625 := [unit-resolution #639 #675]: #634
1.668 +#642 := (not #634)
1.669 +#628 := (or #642 #126 #644)
1.670 +#629 := [def-axiom]: #628
1.671 +#348 := [unit-resolution #629 #625]: #347
1.672 +#622 := [unit-resolution #348 #245]: #644
1.673 +#623 := (or #326 #647)
1.674 +#649 := (iff #130 #647)
1.675 +#315 := (or #643 #649)
1.676 +#316 := [quant-inst #41 #44 #42]: #315
1.677 +#626 := [unit-resolution #316 #675]: #649
1.678 +#645 := (not #649)
1.679 +#287 := (or #645 #326 #647)
1.680 +#630 := [def-axiom]: #287
1.681 +#627 := [unit-resolution #630 #626]: #623
1.682 +#336 := [unit-resolution #627 #622 #624]: false
1.683 +#337 := [lemma #336]: #126
1.684 +#329 := (or #326 #139)
1.685 +#317 := (or #326 #139 #237)
1.686 +#328 := [def-axiom]: #317
1.687 +#257 := [unit-resolution #328 #147]: #329
1.688 +#338 := [unit-resolution #257 #337]: #326
1.689 +#340 := (or #139 #647)
1.690 +#335 := (or #642 #139 #647)
1.691 +#351 := [def-axiom]: #335
1.692 +#618 := [unit-resolution #351 #625]: #340
1.693 +#619 := [unit-resolution #618 #337]: #647
1.694 +#332 := (or #130 #644)
1.695 +#303 := (or #645 #130 #644)
1.696 +#646 := [def-axiom]: #303
1.697 +#616 := [unit-resolution #646 #626]: #332
1.698 +[unit-resolution #616 #619 #338]: false
1.699 +unsat
1.700 +0a38803d5203ebb9de80029b1e5de8bcd8e8f404 128 0
1.701 +#2 := false
1.702 +decl f3 :: (-> S2 S3 S1)
1.703 +decl f6 :: (-> S4 S3 S3)
1.704 +decl f11 :: S3
1.705 +#42 := f11
1.706 +decl f7 :: (-> S5 S3 S4)
1.707 +decl f8 :: S5
1.708 +#19 := f8
1.709 +#43 := (f7 f8 f11)
1.710 +#44 := (f6 #43 f11)
1.711 +decl f10 :: S2
1.712 +#41 := f10
1.713 +#45 := (f3 f10 #44)
1.714 +decl f1 :: S1
1.715 +#4 := f1
1.716 +#123 := (= f1 #45)
1.717 +#136 := (not #123)
1.718 +#627 := [hypothesis]: #136
1.719 +#47 := (f3 f10 f11)
1.720 +#127 := (= f1 #47)
1.721 +#322 := (or #127 #123)
1.722 +#137 := (iff #127 #136)
1.723 +#48 := (= #47 f1)
1.724 +#46 := (= #45 f1)
1.725 +#49 := (iff #46 #48)
1.726 +#50 := (not #49)
1.727 +#140 := (iff #50 #137)
1.728 +#130 := (iff #123 #127)
1.729 +#133 := (not #130)
1.730 +#138 := (iff #133 #137)
1.731 +#139 := [rewrite]: #138
1.732 +#134 := (iff #50 #133)
1.733 +#131 := (iff #49 #130)
1.734 +#128 := (iff #48 #127)
1.735 +#129 := [rewrite]: #128
1.736 +#125 := (iff #46 #123)
1.737 +#126 := [rewrite]: #125
1.738 +#132 := [monotonicity #126 #129]: #131
1.739 +#135 := [monotonicity #132]: #134
1.740 +#141 := [trans #135 #139]: #140
1.741 +#122 := [asserted]: #50
1.742 +#144 := [mp #122 #141]: #137
1.743 +#234 := (not #137)
1.744 +#321 := (or #127 #123 #234)
1.745 +#235 := [def-axiom]: #321
1.746 +#236 := [unit-resolution #235 #144]: #322
1.747 +#288 := [unit-resolution #236 #627]: #127
1.748 +#323 := (not #127)
1.749 +#290 := (or #123 #323)
1.750 +#22 := (:var 0 S3)
1.751 +#20 := (:var 1 S3)
1.752 +#21 := (f7 f8 #20)
1.753 +#23 := (f6 #21 #22)
1.754 +#18 := (:var 2 S2)
1.755 +#24 := (f3 #18 #23)
1.756 +#666 := (pattern #24)
1.757 +#28 := (f3 #18 #22)
1.758 +#96 := (= f1 #28)
1.759 +#26 := (f3 #18 #20)
1.760 +#93 := (= f1 #26)
1.761 +#99 := (or #93 #96)
1.762 +#89 := (= f1 #24)
1.763 +#102 := (iff #89 #99)
1.764 +#667 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #666) #102)
1.765 +#105 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #102)
1.766 +#670 := (iff #105 #667)
1.767 +#668 := (iff #102 #102)
1.768 +#669 := [refl]: #668
1.769 +#671 := [quant-intro #669]: #670
1.770 +#148 := (~ #105 #105)
1.771 +#162 := (~ #102 #102)
1.772 +#163 := [refl]: #162
1.773 +#149 := [nnf-pos #163]: #148
1.774 +#29 := (= #28 f1)
1.775 +#27 := (= #26 f1)
1.776 +#30 := (or #27 #29)
1.777 +#25 := (= #24 f1)
1.778 +#31 := (iff #25 #30)
1.779 +#32 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #31)
1.780 +#106 := (iff #32 #105)
1.781 +#103 := (iff #31 #102)
1.782 +#100 := (iff #30 #99)
1.783 +#97 := (iff #29 #96)
1.784 +#98 := [rewrite]: #97
1.785 +#94 := (iff #27 #93)
1.786 +#95 := [rewrite]: #94
1.787 +#101 := [monotonicity #95 #98]: #100
1.788 +#91 := (iff #25 #89)
1.789 +#92 := [rewrite]: #91
1.790 +#104 := [monotonicity #92 #101]: #103
1.791 +#107 := [quant-intro #104]: #106
1.792 +#88 := [asserted]: #32
1.793 +#110 := [mp #88 #107]: #105
1.794 +#164 := [mp~ #110 #149]: #105
1.795 +#672 := [mp #164 #671]: #667
1.796 +#301 := (not #667)
1.797 +#433 := (or #301 #130)
1.798 +#327 := (or #127 #127)
1.799 +#324 := (iff #123 #327)
1.800 +#640 := (or #301 #324)
1.801 +#313 := (iff #640 #433)
1.802 +#648 := (iff #433 #433)
1.803 +#649 := [rewrite]: #648
1.804 +#644 := (iff #324 #130)
1.805 +#328 := (iff #327 #127)
1.806 +#307 := [rewrite]: #328
1.807 +#646 := [monotonicity #307]: #644
1.808 +#647 := [monotonicity #646]: #313
1.809 +#650 := [trans #647 #649]: #313
1.810 +#312 := [quant-inst #41 #42 #42]: #640
1.811 +#645 := [mp #312 #650]: #433
1.812 +#289 := [unit-resolution #645 #672]: #130
1.813 +#651 := (or #133 #123 #323)
1.814 +#641 := [def-axiom]: #651
1.815 +#291 := [unit-resolution #641 #289]: #290
1.816 +#629 := [unit-resolution #291 #288 #627]: false
1.817 +#630 := [lemma #629]: #123
1.818 +#326 := (or #323 #136)
1.819 +#314 := (or #323 #136 #234)
1.820 +#325 := [def-axiom]: #314
1.821 +#254 := [unit-resolution #325 #144]: #326
1.822 +#631 := [unit-resolution #254 #630]: #323
1.823 +#632 := (or #136 #127)
1.824 +#299 := (or #133 #136 #127)
1.825 +#304 := [def-axiom]: #299
1.826 +#633 := [unit-resolution #304 #289]: #632
1.827 +[unit-resolution #633 #631 #630]: false
1.828 +unsat
1.829 +a9b4d2c6d5d71402741164958baf8befeec2192a 266 0
1.830 +#2 := false
1.831 +decl f3 :: (-> S2 S3 S1)
1.832 +decl f12 :: S3
1.833 +#44 := f12
1.834 +decl f10 :: S2
1.835 +#41 := f10
1.836 +#623 := (f3 f10 f12)
1.837 +decl f1 :: S1
1.838 +#4 := f1
1.839 +#336 := (= f1 #623)
1.840 +decl f13 :: S3
1.841 +#46 := f13
1.842 +#334 := (f3 f10 f13)
1.843 +#331 := (= f1 #334)
1.844 +#621 := (or #331 #336)
1.845 +decl f6 :: (-> S4 S3 S3)
1.846 +decl f7 :: (-> S5 S3 S4)
1.847 +decl f8 :: S5
1.848 +#19 := f8
1.849 +#45 := (f7 f8 f12)
1.850 +#47 := (f6 #45 f13)
1.851 +#308 := (f3 f10 #47)
1.852 +#440 := (= f1 #308)
1.853 +#615 := (iff #440 #621)
1.854 +#581 := (not #615)
1.855 +#593 := (not #621)
1.856 +#605 := (not #336)
1.857 +decl f11 :: S3
1.858 +#42 := f11
1.859 +#636 := (f3 f10 f11)
1.860 +#637 := (= f1 #636)
1.861 +#483 := (or #336 #637)
1.862 +#608 := (not #483)
1.863 +#43 := (f7 f8 f11)
1.864 +#51 := (f6 #43 f12)
1.865 +#335 := (f3 f10 #51)
1.866 +#314 := (= f1 #335)
1.867 +#591 := (iff #314 #483)
1.868 +#583 := (not #591)
1.869 +#576 := [hypothesis]: #583
1.870 +#22 := (:var 0 S3)
1.871 +#20 := (:var 1 S3)
1.872 +#21 := (f7 f8 #20)
1.873 +#23 := (f6 #21 #22)
1.874 +#18 := (:var 2 S2)
1.875 +#24 := (f3 #18 #23)
1.876 +#673 := (pattern #24)
1.877 +#28 := (f3 #18 #22)
1.878 +#103 := (= f1 #28)
1.879 +#26 := (f3 #18 #20)
1.880 +#100 := (= f1 #26)
1.881 +#106 := (or #100 #103)
1.882 +#96 := (= f1 #24)
1.883 +#109 := (iff #96 #106)
1.884 +#674 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #673) #109)
1.885 +#112 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #109)
1.886 +#677 := (iff #112 #674)
1.887 +#675 := (iff #109 #109)
1.888 +#676 := [refl]: #675
1.889 +#678 := [quant-intro #676]: #677
1.890 +#155 := (~ #112 #112)
1.891 +#169 := (~ #109 #109)
1.892 +#170 := [refl]: #169
1.893 +#156 := [nnf-pos #170]: #155
1.894 +#29 := (= #28 f1)
1.895 +#27 := (= #26 f1)
1.896 +#30 := (or #27 #29)
1.897 +#25 := (= #24 f1)
1.898 +#31 := (iff #25 #30)
1.899 +#32 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #31)
1.900 +#113 := (iff #32 #112)
1.901 +#110 := (iff #31 #109)
1.902 +#107 := (iff #30 #106)
1.903 +#104 := (iff #29 #103)
1.904 +#105 := [rewrite]: #104
1.905 +#101 := (iff #27 #100)
1.906 +#102 := [rewrite]: #101
1.907 +#108 := [monotonicity #102 #105]: #107
1.908 +#98 := (iff #25 #96)
1.909 +#99 := [rewrite]: #98
1.910 +#111 := [monotonicity #99 #108]: #110
1.911 +#114 := [quant-intro #111]: #113
1.912 +#95 := [asserted]: #32
1.913 +#117 := [mp #95 #114]: #112
1.914 +#171 := [mp~ #117 #156]: #112
1.915 +#679 := [mp #171 #678]: #674
1.916 +#647 := (not #674)
1.917 +#589 := (or #647 #591)
1.918 +#600 := (or #637 #336)
1.919 +#482 := (iff #314 #600)
1.920 +#592 := (or #647 #482)
1.921 +#492 := (iff #592 #589)
1.922 +#495 := (iff #589 #589)
1.923 +#488 := [rewrite]: #495
1.924 +#493 := (iff #482 #591)
1.925 +#484 := (iff #600 #483)
1.926 +#443 := [rewrite]: #484
1.927 +#588 := [monotonicity #443]: #493
1.928 +#494 := [monotonicity #588]: #492
1.929 +#496 := [trans #494 #488]: #492
1.930 +#477 := [quant-inst #41 #42 #44]: #592
1.931 +#497 := [mp #477 #496]: #589
1.932 +#577 := [unit-resolution #497 #679 #576]: false
1.933 +#578 := [lemma #577]: #591
1.934 +#654 := (not #314)
1.935 +#651 := (or #314 #331)
1.936 +#648 := (not #651)
1.937 +#52 := (f7 f8 #51)
1.938 +#53 := (f6 #52 f13)
1.939 +#54 := (f3 f10 #53)
1.940 +#134 := (= f1 #54)
1.941 +#330 := (not #134)
1.942 +#48 := (f6 #43 #47)
1.943 +#49 := (f3 f10 #48)
1.944 +#130 := (= f1 #49)
1.945 +#143 := (not #130)
1.946 +#579 := [hypothesis]: #143
1.947 +#329 := (or #134 #130)
1.948 +#144 := (iff #134 #143)
1.949 +#55 := (= #54 f1)
1.950 +#50 := (= #49 f1)
1.951 +#56 := (iff #50 #55)
1.952 +#57 := (not #56)
1.953 +#147 := (iff #57 #144)
1.954 +#137 := (iff #130 #134)
1.955 +#140 := (not #137)
1.956 +#145 := (iff #140 #144)
1.957 +#146 := [rewrite]: #145
1.958 +#141 := (iff #57 #140)
1.959 +#138 := (iff #56 #137)
1.960 +#135 := (iff #55 #134)
1.961 +#136 := [rewrite]: #135
1.962 +#132 := (iff #50 #130)
1.963 +#133 := [rewrite]: #132
1.964 +#139 := [monotonicity #133 #136]: #138
1.965 +#142 := [monotonicity #139]: #141
1.966 +#148 := [trans #142 #146]: #147
1.967 +#129 := [asserted]: #57
1.968 +#151 := [mp #129 #148]: #144
1.969 +#241 := (not #144)
1.970 +#328 := (or #134 #130 #241)
1.971 +#242 := [def-axiom]: #328
1.972 +#243 := [unit-resolution #242 #151]: #329
1.973 +#573 := [unit-resolution #243 #579]: #134
1.974 +#564 := (or #330 #651)
1.975 +#653 := (iff #134 #651)
1.976 +#319 := (or #647 #653)
1.977 +#320 := [quant-inst #41 #51 #46]: #319
1.978 +#580 := [unit-resolution #320 #679]: #653
1.979 +#649 := (not #653)
1.980 +#291 := (or #649 #330 #651)
1.981 +#634 := [def-axiom]: #291
1.982 +#565 := [unit-resolution #634 #580]: #564
1.983 +#567 := [unit-resolution #565 #573]: #651
1.984 +#657 := (not #331)
1.985 +#597 := (or #647 #615)
1.986 +#620 := (or #336 #331)
1.987 +#624 := (iff #440 #620)
1.988 +#617 := (or #647 #624)
1.989 +#612 := (iff #617 #597)
1.990 +#619 := (iff #597 #597)
1.991 +#460 := [rewrite]: #619
1.992 +#616 := (iff #624 #615)
1.993 +#625 := (iff #620 #621)
1.994 +#614 := [rewrite]: #625
1.995 +#611 := [monotonicity #614]: #616
1.996 +#613 := [monotonicity #611]: #612
1.997 +#461 := [trans #613 #460]: #612
1.998 +#618 := [quant-inst #41 #44 #46]: #617
1.999 +#462 := [mp #618 #461]: #597
1.1000 +#568 := [unit-resolution #462 #679]: #615
1.1001 +#558 := (or #581 #593)
1.1002 +#356 := (not #440)
1.1003 +#640 := (or #440 #637)
1.1004 +#629 := (not #640)
1.1005 +#570 := (or #130 #629)
1.1006 +#277 := (iff #130 #640)
1.1007 +#282 := (or #647 #277)
1.1008 +#638 := (or #637 #440)
1.1009 +#639 := (iff #130 #638)
1.1010 +#283 := (or #647 #639)
1.1011 +#643 := (iff #283 #282)
1.1012 +#632 := (iff #282 #282)
1.1013 +#633 := [rewrite]: #632
1.1014 +#642 := (iff #639 #277)
1.1015 +#635 := (iff #638 #640)
1.1016 +#641 := [rewrite]: #635
1.1017 +#644 := [monotonicity #641]: #642
1.1018 +#646 := [monotonicity #644]: #643
1.1019 +#339 := [trans #646 #633]: #643
1.1020 +#645 := [quant-inst #41 #42 #47]: #283
1.1021 +#355 := [mp #645 #339]: #282
1.1022 +#569 := [unit-resolution #355 #679]: #277
1.1023 +#626 := (not #277)
1.1024 +#630 := (or #626 #130 #629)
1.1025 +#627 := [def-axiom]: #630
1.1026 +#566 := [unit-resolution #627 #569]: #570
1.1027 +#571 := [unit-resolution #566 #579]: #629
1.1028 +#357 := (or #640 #356)
1.1029 +#343 := [def-axiom]: #357
1.1030 +#557 := [unit-resolution #343 #571]: #356
1.1031 +#575 := (or #581 #440 #593)
1.1032 +#572 := [def-axiom]: #575
1.1033 +#560 := [unit-resolution #572 #557]: #558
1.1034 +#561 := [unit-resolution #560 #568]: #593
1.1035 +#604 := (or #621 #657)
1.1036 +#498 := [def-axiom]: #604
1.1037 +#562 := [unit-resolution #498 #561]: #657
1.1038 +#306 := (or #648 #314 #331)
1.1039 +#311 := [def-axiom]: #306
1.1040 +#559 := [unit-resolution #311 #562 #567]: #314
1.1041 +#358 := (not #637)
1.1042 +#249 := (or #640 #358)
1.1043 +#628 := [def-axiom]: #249
1.1044 +#563 := [unit-resolution #628 #571]: #358
1.1045 +#499 := (or #621 #605)
1.1046 +#500 := [def-axiom]: #499
1.1047 +#543 := [unit-resolution #500 #561]: #605
1.1048 +#609 := (or #608 #336 #637)
1.1049 +#603 := [def-axiom]: #609
1.1050 +#544 := [unit-resolution #603 #543 #563]: #608
1.1051 +#441 := (or #583 #654 #483)
1.1052 +#442 := [def-axiom]: #441
1.1053 +#546 := [unit-resolution #442 #544 #559 #578]: false
1.1054 +#547 := [lemma #546]: #130
1.1055 +#333 := (or #330 #143)
1.1056 +#321 := (or #330 #143 #241)
1.1057 +#332 := [def-axiom]: #321
1.1058 +#261 := [unit-resolution #332 #151]: #333
1.1059 +#548 := [unit-resolution #261 #547]: #330
1.1060 +#549 := (or #134 #648)
1.1061 +#307 := (or #649 #134 #648)
1.1062 +#650 := [def-axiom]: #307
1.1063 +#550 := [unit-resolution #650 #580]: #549
1.1064 +#551 := [unit-resolution #550 #548]: #648
1.1065 +#655 := (or #651 #654)
1.1066 +#656 := [def-axiom]: #655
1.1067 +#552 := [unit-resolution #656 #551]: #654
1.1068 +#610 := (or #583 #314 #608)
1.1069 +#439 := [def-axiom]: #610
1.1070 +#553 := [unit-resolution #439 #552 #578]: #608
1.1071 +#606 := (or #483 #605)
1.1072 +#607 := [def-axiom]: #606
1.1073 +#554 := [unit-resolution #607 #553]: #605
1.1074 +#652 := (or #651 #657)
1.1075 +#658 := [def-axiom]: #652
1.1076 +#555 := [unit-resolution #658 #551]: #657
1.1077 +#590 := (or #593 #331 #336)
1.1078 +#594 := [def-axiom]: #590
1.1079 +#545 := [unit-resolution #594 #555 #554]: #593
1.1080 +#556 := (or #143 #640)
1.1081 +#631 := (or #626 #143 #640)
1.1082 +#340 := [def-axiom]: #631
1.1083 +#534 := [unit-resolution #340 #569]: #556
1.1084 +#535 := [unit-resolution #534 #547]: #640
1.1085 +#601 := (or #483 #358)
1.1086 +#602 := [def-axiom]: #601
1.1087 +#537 := [unit-resolution #602 #553]: #358
1.1088 +#351 := (or #629 #440 #637)
1.1089 +#352 := [def-axiom]: #351
1.1090 +#538 := [unit-resolution #352 #537 #535]: #440
1.1091 +#574 := (or #581 #356 #621)
1.1092 +#584 := [def-axiom]: #574
1.1093 +#539 := [unit-resolution #584 #538 #545]: #581
1.1094 +[unit-resolution #462 #679 #539]: false
1.1095 +unsat
1.1096 +c3c3648cfba9d6c85cac6f8d51a3b06b08975178 160 0
1.1097 +#2 := false
1.1098 +decl f3 :: (-> S2 S3 S1)
1.1099 +decl f12 :: S3
1.1100 +#44 := f12
1.1101 +decl f10 :: S2
1.1102 +#41 := f10
1.1103 +#50 := (f3 f10 f12)
1.1104 +decl f1 :: S1
1.1105 +#4 := f1
1.1106 +#134 := (= f1 #50)
1.1107 +#188 := (not #134)
1.1108 +decl f11 :: S3
1.1109 +#42 := f11
1.1110 +#48 := (f3 f10 f11)
1.1111 +#131 := (= f1 #48)
1.1112 +#187 := (not #131)
1.1113 +#189 := (or #187 #188)
1.1114 +#190 := (not #189)
1.1115 +#331 := [hypothesis]: #190
1.1116 +decl f6 :: (-> S4 S3 S3)
1.1117 +decl f7 :: (-> S5 S3 S4)
1.1118 +decl f9 :: S5
1.1119 +#33 := f9
1.1120 +#43 := (f7 f9 f11)
1.1121 +#45 := (f6 #43 f12)
1.1122 +#46 := (f3 f10 #45)
1.1123 +#127 := (= f1 #46)
1.1124 +#146 := (not #127)
1.1125 +#337 := (or #146 #189)
1.1126 +#201 := (iff #127 #189)
1.1127 +#137 := (and #131 #134)
1.1128 +#147 := (iff #137 #146)
1.1129 +#204 := (iff #147 #201)
1.1130 +#196 := (iff #189 #127)
1.1131 +#202 := (iff #196 #201)
1.1132 +#203 := [rewrite]: #202
1.1133 +#199 := (iff #147 #196)
1.1134 +#193 := (iff #190 #146)
1.1135 +#197 := (iff #193 #196)
1.1136 +#198 := [rewrite]: #197
1.1137 +#194 := (iff #147 #193)
1.1138 +#191 := (iff #137 #190)
1.1139 +#192 := [rewrite]: #191
1.1140 +#195 := [monotonicity #192]: #194
1.1141 +#200 := [trans #195 #198]: #199
1.1142 +#205 := [trans #200 #203]: #204
1.1143 +#51 := (= #50 f1)
1.1144 +#49 := (= #48 f1)
1.1145 +#52 := (and #49 #51)
1.1146 +#47 := (= #46 f1)
1.1147 +#53 := (iff #47 #52)
1.1148 +#54 := (not #53)
1.1149 +#150 := (iff #54 #147)
1.1150 +#140 := (iff #127 #137)
1.1151 +#143 := (not #140)
1.1152 +#148 := (iff #143 #147)
1.1153 +#149 := [rewrite]: #148
1.1154 +#144 := (iff #54 #143)
1.1155 +#141 := (iff #53 #140)
1.1156 +#138 := (iff #52 #137)
1.1157 +#135 := (iff #51 #134)
1.1158 +#136 := [rewrite]: #135
1.1159 +#132 := (iff #49 #131)
1.1160 +#133 := [rewrite]: #132
1.1161 +#139 := [monotonicity #133 #136]: #138
1.1162 +#129 := (iff #47 #127)
1.1163 +#130 := [rewrite]: #129
1.1164 +#142 := [monotonicity #130 #139]: #141
1.1165 +#145 := [monotonicity #142]: #144
1.1166 +#151 := [trans #145 #149]: #150
1.1167 +#126 := [asserted]: #54
1.1168 +#154 := [mp #126 #151]: #147
1.1169 +#206 := [mp #154 #205]: #201
1.1170 +#344 := (not #201)
1.1171 +#354 := (or #146 #189 #344)
1.1172 +#358 := [def-axiom]: #354
1.1173 +#674 := [unit-resolution #358 #206]: #337
1.1174 +#463 := [unit-resolution #674 #331]: #146
1.1175 +#330 := (or #127 #189)
1.1176 +#676 := (iff #127 #190)
1.1177 +#22 := (:var 0 S3)
1.1178 +#20 := (:var 1 S3)
1.1179 +#34 := (f7 f9 #20)
1.1180 +#35 := (f6 #34 #22)
1.1181 +#18 := (:var 2 S2)
1.1182 +#36 := (f3 #18 #35)
1.1183 +#703 := (pattern #36)
1.1184 +#28 := (f3 #18 #22)
1.1185 +#100 := (= f1 #28)
1.1186 +#179 := (not #100)
1.1187 +#26 := (f3 #18 #20)
1.1188 +#97 := (= f1 #26)
1.1189 +#178 := (not #97)
1.1190 +#162 := (or #178 #179)
1.1191 +#163 := (not #162)
1.1192 +#113 := (= f1 #36)
1.1193 +#180 := (iff #113 #163)
1.1194 +#704 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #703) #180)
1.1195 +#183 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #180)
1.1196 +#707 := (iff #183 #704)
1.1197 +#705 := (iff #180 #180)
1.1198 +#706 := [refl]: #705
1.1199 +#708 := [quant-intro #706]: #707
1.1200 +#117 := (and #97 #100)
1.1201 +#120 := (iff #113 #117)
1.1202 +#123 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #120)
1.1203 +#184 := (iff #123 #183)
1.1204 +#181 := (iff #120 #180)
1.1205 +#164 := (iff #117 #163)
1.1206 +#165 := [rewrite]: #164
1.1207 +#182 := [monotonicity #165]: #181
1.1208 +#185 := [quant-intro #182]: #184
1.1209 +#160 := (~ #123 #123)
1.1210 +#175 := (~ #120 #120)
1.1211 +#176 := [refl]: #175
1.1212 +#161 := [nnf-pos #176]: #160
1.1213 +#29 := (= #28 f1)
1.1214 +#27 := (= #26 f1)
1.1215 +#38 := (and #27 #29)
1.1216 +#37 := (= #36 f1)
1.1217 +#39 := (iff #37 #38)
1.1218 +#40 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #39)
1.1219 +#124 := (iff #40 #123)
1.1220 +#121 := (iff #39 #120)
1.1221 +#118 := (iff #38 #117)
1.1222 +#101 := (iff #29 #100)
1.1223 +#102 := [rewrite]: #101
1.1224 +#98 := (iff #27 #97)
1.1225 +#99 := [rewrite]: #98
1.1226 +#119 := [monotonicity #99 #102]: #118
1.1227 +#115 := (iff #37 #113)
1.1228 +#116 := [rewrite]: #115
1.1229 +#122 := [monotonicity #116 #119]: #121
1.1230 +#125 := [quant-intro #122]: #124
1.1231 +#112 := [asserted]: #40
1.1232 +#128 := [mp #112 #125]: #123
1.1233 +#177 := [mp~ #128 #161]: #123
1.1234 +#186 := [mp #177 #185]: #183
1.1235 +#709 := [mp #186 #708]: #704
1.1236 +#670 := (not #704)
1.1237 +#342 := (or #670 #676)
1.1238 +#343 := [quant-inst #41 #42 #44]: #342
1.1239 +#672 := [unit-resolution #343 #709]: #676
1.1240 +#677 := (not #676)
1.1241 +#678 := (or #677 #127 #189)
1.1242 +#679 := [def-axiom]: #678
1.1243 +#673 := [unit-resolution #679 #672]: #330
1.1244 +#314 := [unit-resolution #673 #463 #331]: false
1.1245 +#657 := [lemma #314]: #189
1.1246 +#284 := (or #127 #190)
1.1247 +#355 := (or #127 #190 #344)
1.1248 +#356 := [def-axiom]: #355
1.1249 +#357 := [unit-resolution #356 #206]: #284
1.1250 +#318 := [unit-resolution #357 #657]: #127
1.1251 +#319 := (or #146 #190)
1.1252 +#680 := (or #677 #146 #190)
1.1253 +#675 := [def-axiom]: #680
1.1254 +#320 := [unit-resolution #675 #672]: #319
1.1255 +[unit-resolution #320 #318 #657]: false
1.1256 +unsat
1.1257 +1adc4d295cebee376081ce9f5a9d0e96c2943423 149 0
1.1258 +#2 := false
1.1259 +decl f3 :: (-> S2 S3 S1)
1.1260 +decl f4 :: S3
1.1261 +#9 := f4
1.1262 +decl f10 :: S2
1.1263 +#41 := f10
1.1264 +#227 := (f3 f10 f4)
1.1265 +decl f1 :: S1
1.1266 +#4 := f1
1.1267 +#314 := (= f1 #227)
1.1268 +#228 := (not #314)
1.1269 +decl f11 :: S3
1.1270 +#42 := f11
1.1271 +#315 := (f3 f10 f11)
1.1272 +#229 := (= f1 #315)
1.1273 +#316 := (not #229)
1.1274 +#307 := (or #316 #228)
1.1275 +#318 := (not #307)
1.1276 +decl f6 :: (-> S4 S3 S3)
1.1277 +decl f7 :: (-> S5 S3 S4)
1.1278 +decl f9 :: S5
1.1279 +#33 := f9
1.1280 +#43 := (f7 f9 f11)
1.1281 +#44 := (f6 #43 f4)
1.1282 +#45 := (f3 f10 #44)
1.1283 +#121 := (= f1 #45)
1.1284 +#319 := (iff #121 #318)
1.1285 +#22 := (:var 0 S3)
1.1286 +#20 := (:var 1 S3)
1.1287 +#34 := (f7 f9 #20)
1.1288 +#35 := (f6 #34 #22)
1.1289 +#18 := (:var 2 S2)
1.1290 +#36 := (f3 #18 #35)
1.1291 +#666 := (pattern #36)
1.1292 +#28 := (f3 #18 #22)
1.1293 +#94 := (= f1 #28)
1.1294 +#162 := (not #94)
1.1295 +#26 := (f3 #18 #20)
1.1296 +#91 := (= f1 #26)
1.1297 +#161 := (not #91)
1.1298 +#145 := (or #161 #162)
1.1299 +#146 := (not #145)
1.1300 +#107 := (= f1 #36)
1.1301 +#163 := (iff #107 #146)
1.1302 +#667 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #666) #163)
1.1303 +#166 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #163)
1.1304 +#670 := (iff #166 #667)
1.1305 +#668 := (iff #163 #163)
1.1306 +#669 := [refl]: #668
1.1307 +#671 := [quant-intro #669]: #670
1.1308 +#111 := (and #91 #94)
1.1309 +#114 := (iff #107 #111)
1.1310 +#117 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #114)
1.1311 +#167 := (iff #117 #166)
1.1312 +#164 := (iff #114 #163)
1.1313 +#147 := (iff #111 #146)
1.1314 +#148 := [rewrite]: #147
1.1315 +#165 := [monotonicity #148]: #164
1.1316 +#168 := [quant-intro #165]: #167
1.1317 +#143 := (~ #117 #117)
1.1318 +#158 := (~ #114 #114)
1.1319 +#159 := [refl]: #158
1.1320 +#144 := [nnf-pos #159]: #143
1.1321 +#29 := (= #28 f1)
1.1322 +#27 := (= #26 f1)
1.1323 +#38 := (and #27 #29)
1.1324 +#37 := (= #36 f1)
1.1325 +#39 := (iff #37 #38)
1.1326 +#40 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #39)
1.1327 +#118 := (iff #40 #117)
1.1328 +#115 := (iff #39 #114)
1.1329 +#112 := (iff #38 #111)
1.1330 +#95 := (iff #29 #94)
1.1331 +#96 := [rewrite]: #95
1.1332 +#92 := (iff #27 #91)
1.1333 +#93 := [rewrite]: #92
1.1334 +#113 := [monotonicity #93 #96]: #112
1.1335 +#109 := (iff #37 #107)
1.1336 +#110 := [rewrite]: #109
1.1337 +#116 := [monotonicity #110 #113]: #115
1.1338 +#119 := [quant-intro #116]: #118
1.1339 +#106 := [asserted]: #40
1.1340 +#122 := [mp #106 #119]: #117
1.1341 +#160 := [mp~ #122 #144]: #117
1.1342 +#169 := [mp #160 #168]: #166
1.1343 +#672 := [mp #169 #671]: #667
1.1344 +#317 := (not #667)
1.1345 +#321 := (or #317 #319)
1.1346 +#300 := [quant-inst #41 #42 #9]: #321
1.1347 +#247 := [unit-resolution #300 #672]: #319
1.1348 +#306 := (not #319)
1.1349 +#320 := (or #306 #318)
1.1350 +#46 := (= #45 f1)
1.1351 +#47 := (not #46)
1.1352 +#48 := (not #47)
1.1353 +#133 := (iff #48 #121)
1.1354 +#125 := (not #121)
1.1355 +#128 := (not #125)
1.1356 +#131 := (iff #128 #121)
1.1357 +#132 := [rewrite]: #131
1.1358 +#129 := (iff #48 #128)
1.1359 +#126 := (iff #47 #125)
1.1360 +#123 := (iff #46 #121)
1.1361 +#124 := [rewrite]: #123
1.1362 +#127 := [monotonicity #124]: #126
1.1363 +#130 := [monotonicity #127]: #129
1.1364 +#134 := [trans #130 #132]: #133
1.1365 +#120 := [asserted]: #48
1.1366 +#137 := [mp #120 #134]: #121
1.1367 +#642 := (or #306 #125 #318)
1.1368 +#643 := [def-axiom]: #642
1.1369 +#636 := [unit-resolution #643 #137]: #320
1.1370 +#277 := [unit-resolution #636 #247]: #318
1.1371 +#294 := (or #307 #314)
1.1372 +#426 := [def-axiom]: #294
1.1373 +#620 := [unit-resolution #426 #277]: #314
1.1374 +#8 := (:var 0 S2)
1.1375 +#10 := (f3 #8 f4)
1.1376 +#645 := (pattern #10)
1.1377 +#69 := (= f1 #10)
1.1378 +#72 := (not #69)
1.1379 +#646 := (forall (vars (?v0 S2)) (:pat #645) #72)
1.1380 +#75 := (forall (vars (?v0 S2)) #72)
1.1381 +#649 := (iff #75 #646)
1.1382 +#647 := (iff #72 #72)
1.1383 +#648 := [refl]: #647
1.1384 +#650 := [quant-intro #648]: #649
1.1385 +#151 := (~ #75 #75)
1.1386 +#149 := (~ #72 #72)
1.1387 +#150 := [refl]: #149
1.1388 +#152 := [nnf-pos #150]: #151
1.1389 +#11 := (= #10 f1)
1.1390 +#12 := (not #11)
1.1391 +#13 := (forall (vars (?v0 S2)) #12)
1.1392 +#76 := (iff #13 #75)
1.1393 +#73 := (iff #12 #72)
1.1394 +#70 := (iff #11 #69)
1.1395 +#71 := [rewrite]: #70
1.1396 +#74 := [monotonicity #71]: #73
1.1397 +#77 := [quant-intro #74]: #76
1.1398 +#68 := [asserted]: #13
1.1399 +#80 := [mp #68 #77]: #75
1.1400 +#136 := [mp~ #80 #152]: #75
1.1401 +#651 := [mp #136 #650]: #646
1.1402 +#297 := (not #646)
1.1403 +#635 := (or #297 #228)
1.1404 +#293 := [quant-inst #41]: #635
1.1405 +[unit-resolution #293 #651 #620]: false
1.1406 +unsat
1.1407 +27fbc35929f013c0b43884a593f3f377821cad64 173 0
1.1408 +#2 := false
1.1409 +decl f3 :: (-> S2 S3 S1)
1.1410 +decl f11 :: S3
1.1411 +#42 := f11
1.1412 +decl f10 :: S2
1.1413 +#41 := f10
1.1414 +#47 := (f3 f10 f11)
1.1415 +decl f1 :: S1
1.1416 +#4 := f1
1.1417 +#127 := (= f1 #47)
1.1418 +#323 := (not #127)
1.1419 +decl f6 :: (-> S4 S3 S3)
1.1420 +decl f5 :: S3
1.1421 +#14 := f5
1.1422 +decl f7 :: (-> S5 S3 S4)
1.1423 +decl f9 :: S5
1.1424 +#33 := f9
1.1425 +#43 := (f7 f9 f11)
1.1426 +#44 := (f6 #43 f5)
1.1427 +#45 := (f3 f10 #44)
1.1428 +#123 := (= f1 #45)
1.1429 +#327 := (f3 f10 f5)
1.1430 +#324 := (= f1 #327)
1.1431 +#328 := (not #324)
1.1432 +#301 := [hypothesis]: #328
1.1433 +#8 := (:var 0 S2)
1.1434 +#15 := (f3 #8 f5)
1.1435 +#659 := (pattern #15)
1.1436 +#81 := (= f1 #15)
1.1437 +#660 := (forall (vars (?v0 S2)) (:pat #659) #81)
1.1438 +#85 := (forall (vars (?v0 S2)) #81)
1.1439 +#663 := (iff #85 #660)
1.1440 +#661 := (iff #81 #81)
1.1441 +#662 := [refl]: #661
1.1442 +#664 := [quant-intro #662]: #663
1.1443 +#146 := (~ #85 #85)
1.1444 +#145 := (~ #81 #81)
1.1445 +#160 := [refl]: #145
1.1446 +#147 := [nnf-pos #160]: #146
1.1447 +#16 := (= #15 f1)
1.1448 +#17 := (forall (vars (?v0 S2)) #16)
1.1449 +#86 := (iff #17 #85)
1.1450 +#83 := (iff #16 #81)
1.1451 +#84 := [rewrite]: #83
1.1452 +#87 := [quant-intro #84]: #86
1.1453 +#80 := [asserted]: #17
1.1454 +#90 := [mp #80 #87]: #85
1.1455 +#161 := [mp~ #90 #147]: #85
1.1456 +#665 := [mp #161 #664]: #660
1.1457 +#289 := (not #660)
1.1458 +#290 := (or #289 #324)
1.1459 +#291 := [quant-inst #41]: #290
1.1460 +#433 := [unit-resolution #291 #665 #301]: false
1.1461 +#629 := [lemma #433]: #324
1.1462 +#136 := (not #123)
1.1463 +#630 := [hypothesis]: #136
1.1464 +#322 := (or #127 #123)
1.1465 +#137 := (iff #127 #136)
1.1466 +#48 := (= #47 f1)
1.1467 +#46 := (= #45 f1)
1.1468 +#49 := (iff #46 #48)
1.1469 +#50 := (not #49)
1.1470 +#140 := (iff #50 #137)
1.1471 +#130 := (iff #123 #127)
1.1472 +#133 := (not #130)
1.1473 +#138 := (iff #133 #137)
1.1474 +#139 := [rewrite]: #138
1.1475 +#134 := (iff #50 #133)
1.1476 +#131 := (iff #49 #130)
1.1477 +#128 := (iff #48 #127)
1.1478 +#129 := [rewrite]: #128
1.1479 +#125 := (iff #46 #123)
1.1480 +#126 := [rewrite]: #125
1.1481 +#132 := [monotonicity #126 #129]: #131
1.1482 +#135 := [monotonicity #132]: #134
1.1483 +#141 := [trans #135 #139]: #140
1.1484 +#122 := [asserted]: #50
1.1485 +#144 := [mp #122 #141]: #137
1.1486 +#234 := (not #137)
1.1487 +#321 := (or #127 #123 #234)
1.1488 +#235 := [def-axiom]: #321
1.1489 +#236 := [unit-resolution #235 #144]: #322
1.1490 +#631 := [unit-resolution #236 #630]: #127
1.1491 +#307 := (or #323 #328)
1.1492 +#633 := (or #123 #307)
1.1493 +#644 := (not #307)
1.1494 +#646 := (iff #123 #644)
1.1495 +#22 := (:var 0 S3)
1.1496 +#20 := (:var 1 S3)
1.1497 +#34 := (f7 f9 #20)
1.1498 +#35 := (f6 #34 #22)
1.1499 +#18 := (:var 2 S2)
1.1500 +#36 := (f3 #18 #35)
1.1501 +#673 := (pattern #36)
1.1502 +#28 := (f3 #18 #22)
1.1503 +#96 := (= f1 #28)
1.1504 +#169 := (not #96)
1.1505 +#26 := (f3 #18 #20)
1.1506 +#93 := (= f1 #26)
1.1507 +#168 := (not #93)
1.1508 +#152 := (or #168 #169)
1.1509 +#153 := (not #152)
1.1510 +#109 := (= f1 #36)
1.1511 +#170 := (iff #109 #153)
1.1512 +#674 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #673) #170)
1.1513 +#173 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #170)
1.1514 +#677 := (iff #173 #674)
1.1515 +#675 := (iff #170 #170)
1.1516 +#676 := [refl]: #675
1.1517 +#678 := [quant-intro #676]: #677
1.1518 +#113 := (and #93 #96)
1.1519 +#116 := (iff #109 #113)
1.1520 +#119 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #116)
1.1521 +#174 := (iff #119 #173)
1.1522 +#171 := (iff #116 #170)
1.1523 +#154 := (iff #113 #153)
1.1524 +#155 := [rewrite]: #154
1.1525 +#172 := [monotonicity #155]: #171
1.1526 +#175 := [quant-intro #172]: #174
1.1527 +#150 := (~ #119 #119)
1.1528 +#165 := (~ #116 #116)
1.1529 +#166 := [refl]: #165
1.1530 +#151 := [nnf-pos #166]: #150
1.1531 +#29 := (= #28 f1)
1.1532 +#27 := (= #26 f1)
1.1533 +#38 := (and #27 #29)
1.1534 +#37 := (= #36 f1)
1.1535 +#39 := (iff #37 #38)
1.1536 +#40 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #39)
1.1537 +#120 := (iff #40 #119)
1.1538 +#117 := (iff #39 #116)
1.1539 +#114 := (iff #38 #113)
1.1540 +#97 := (iff #29 #96)
1.1541 +#98 := [rewrite]: #97
1.1542 +#94 := (iff #27 #93)
1.1543 +#95 := [rewrite]: #94
1.1544 +#115 := [monotonicity #95 #98]: #114
1.1545 +#111 := (iff #37 #109)
1.1546 +#112 := [rewrite]: #111
1.1547 +#118 := [monotonicity #112 #115]: #117
1.1548 +#121 := [quant-intro #118]: #120
1.1549 +#108 := [asserted]: #40
1.1550 +#124 := [mp #108 #121]: #119
1.1551 +#167 := [mp~ #124 #151]: #119
1.1552 +#176 := [mp #167 #175]: #173
1.1553 +#679 := [mp #176 #678]: #674
1.1554 +#640 := (not #674)
1.1555 +#312 := (or #640 #646)
1.1556 +#313 := [quant-inst #41 #42 #14]: #312
1.1557 +#632 := [unit-resolution #313 #679]: #646
1.1558 +#641 := (not #646)
1.1559 +#299 := (or #641 #123 #307)
1.1560 +#304 := [def-axiom]: #299
1.1561 +#628 := [unit-resolution #304 #632]: #633
1.1562 +#634 := [unit-resolution #628 #630]: #307
1.1563 +#645 := (or #644 #323 #328)
1.1564 +#651 := [def-axiom]: #645
1.1565 +#270 := [unit-resolution #651 #634 #631 #629]: false
1.1566 +#635 := [lemma #270]: #123
1.1567 +#326 := (or #323 #136)
1.1568 +#314 := (or #323 #136 #234)
1.1569 +#325 := [def-axiom]: #314
1.1570 +#254 := [unit-resolution #325 #144]: #326
1.1571 +#637 := [unit-resolution #254 #635]: #323
1.1572 +#275 := (or #136 #644)
1.1573 +#642 := (or #641 #136 #644)
1.1574 +#300 := [def-axiom]: #642
1.1575 +#276 := [unit-resolution #300 #632]: #275
1.1576 +#638 := [unit-resolution #276 #635]: #644
1.1577 +#647 := (or #307 #127)
1.1578 +#648 := [def-axiom]: #647
1.1579 +[unit-resolution #648 #638 #637]: false
1.1580 +unsat
1.1581 +fa1e213c15b8e9288bf16d2dc4bd96e3c7fb5c7e 173 0
1.1582 +#2 := false
1.1583 +decl f3 :: (-> S2 S3 S1)
1.1584 +decl f6 :: (-> S4 S3 S3)
1.1585 +decl f11 :: S3
1.1586 +#42 := f11
1.1587 +decl f7 :: (-> S5 S3 S4)
1.1588 +decl f12 :: S3
1.1589 +#44 := f12
1.1590 +decl f9 :: S5
1.1591 +#33 := f9
1.1592 +#48 := (f7 f9 f12)
1.1593 +#49 := (f6 #48 f11)
1.1594 +decl f10 :: S2
1.1595 +#41 := f10
1.1596 +#50 := (f3 f10 #49)
1.1597 +decl f1 :: S1
1.1598 +#4 := f1
1.1599 +#130 := (= f1 #50)
1.1600 +#326 := (not #130)
1.1601 +#43 := (f7 f9 f11)
1.1602 +#45 := (f6 #43 f12)
1.1603 +#46 := (f3 f10 #45)
1.1604 +#126 := (= f1 #46)
1.1605 +#139 := (not #126)
1.1606 +#628 := [hypothesis]: #139
1.1607 +#325 := (or #130 #126)
1.1608 +#140 := (iff #130 #139)
1.1609 +#51 := (= #50 f1)
1.1610 +#47 := (= #46 f1)
1.1611 +#52 := (iff #47 #51)
1.1612 +#53 := (not #52)
1.1613 +#143 := (iff #53 #140)
1.1614 +#133 := (iff #126 #130)
1.1615 +#136 := (not #133)
1.1616 +#141 := (iff #136 #140)
1.1617 +#142 := [rewrite]: #141
1.1618 +#137 := (iff #53 #136)
1.1619 +#134 := (iff #52 #133)
1.1620 +#131 := (iff #51 #130)
1.1621 +#132 := [rewrite]: #131
1.1622 +#128 := (iff #47 #126)
1.1623 +#129 := [rewrite]: #128
1.1624 +#135 := [monotonicity #129 #132]: #134
1.1625 +#138 := [monotonicity #135]: #137
1.1626 +#144 := [trans #138 #142]: #143
1.1627 +#125 := [asserted]: #53
1.1628 +#147 := [mp #125 #144]: #140
1.1629 +#237 := (not #140)
1.1630 +#324 := (or #130 #126 #237)
1.1631 +#238 := [def-axiom]: #324
1.1632 +#239 := [unit-resolution #238 #147]: #325
1.1633 +#629 := [unit-resolution #239 #628]: #130
1.1634 +#310 := (f3 f10 f12)
1.1635 +#647 := (= f1 #310)
1.1636 +#649 := (not #647)
1.1637 +#330 := (f3 f10 f11)
1.1638 +#327 := (= f1 #330)
1.1639 +#331 := (not #327)
1.1640 +#315 := (or #331 #649)
1.1641 +#626 := (or #126 #315)
1.1642 +#651 := (not #315)
1.1643 +#642 := (iff #126 #651)
1.1644 +#22 := (:var 0 S3)
1.1645 +#20 := (:var 1 S3)
1.1646 +#34 := (f7 f9 #20)
1.1647 +#35 := (f6 #34 #22)
1.1648 +#18 := (:var 2 S2)
1.1649 +#36 := (f3 #18 #35)
1.1650 +#676 := (pattern #36)
1.1651 +#28 := (f3 #18 #22)
1.1652 +#99 := (= f1 #28)
1.1653 +#172 := (not #99)
1.1654 +#26 := (f3 #18 #20)
1.1655 +#96 := (= f1 #26)
1.1656 +#171 := (not #96)
1.1657 +#155 := (or #171 #172)
1.1658 +#156 := (not #155)
1.1659 +#112 := (= f1 #36)
1.1660 +#173 := (iff #112 #156)
1.1661 +#677 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #676) #173)
1.1662 +#176 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #173)
1.1663 +#680 := (iff #176 #677)
1.1664 +#678 := (iff #173 #173)
1.1665 +#679 := [refl]: #678
1.1666 +#681 := [quant-intro #679]: #680
1.1667 +#116 := (and #96 #99)
1.1668 +#119 := (iff #112 #116)
1.1669 +#122 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #119)
1.1670 +#177 := (iff #122 #176)
1.1671 +#174 := (iff #119 #173)
1.1672 +#157 := (iff #116 #156)
1.1673 +#158 := [rewrite]: #157
1.1674 +#175 := [monotonicity #158]: #174
1.1675 +#178 := [quant-intro #175]: #177
1.1676 +#153 := (~ #122 #122)
1.1677 +#168 := (~ #119 #119)
1.1678 +#169 := [refl]: #168
1.1679 +#154 := [nnf-pos #169]: #153
1.1680 +#29 := (= #28 f1)
1.1681 +#27 := (= #26 f1)
1.1682 +#38 := (and #27 #29)
1.1683 +#37 := (= #36 f1)
1.1684 +#39 := (iff #37 #38)
1.1685 +#40 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #39)
1.1686 +#123 := (iff #40 #122)
1.1687 +#120 := (iff #39 #119)
1.1688 +#117 := (iff #38 #116)
1.1689 +#100 := (iff #29 #99)
1.1690 +#101 := [rewrite]: #100
1.1691 +#97 := (iff #27 #96)
1.1692 +#98 := [rewrite]: #97
1.1693 +#118 := [monotonicity #98 #101]: #117
1.1694 +#114 := (iff #37 #112)
1.1695 +#115 := [rewrite]: #114
1.1696 +#121 := [monotonicity #115 #118]: #120
1.1697 +#124 := [quant-intro #121]: #123
1.1698 +#111 := [asserted]: #40
1.1699 +#127 := [mp #111 #124]: #122
1.1700 +#170 := [mp~ #127 #154]: #122
1.1701 +#179 := [mp #170 #178]: #176
1.1702 +#682 := [mp #179 #681]: #677
1.1703 +#302 := (not #677)
1.1704 +#335 := (or #302 #642)
1.1705 +#351 := [quant-inst #41 #42 #44]: #335
1.1706 +#622 := [unit-resolution #351 #682]: #642
1.1707 +#352 := (not #642)
1.1708 +#353 := (or #352 #126 #315)
1.1709 +#339 := [def-axiom]: #353
1.1710 +#623 := [unit-resolution #339 #622]: #626
1.1711 +#627 := [unit-resolution #623 #628]: #315
1.1712 +#337 := (or #326 #651)
1.1713 +#648 := (iff #130 #651)
1.1714 +#307 := (or #302 #648)
1.1715 +#304 := (or #649 #331)
1.1716 +#436 := (not #304)
1.1717 +#643 := (iff #130 #436)
1.1718 +#645 := (or #302 #643)
1.1719 +#646 := (iff #645 #307)
1.1720 +#630 := (iff #307 #307)
1.1721 +#291 := [rewrite]: #630
1.1722 +#654 := (iff #643 #648)
1.1723 +#652 := (iff #436 #651)
1.1724 +#316 := (iff #304 #315)
1.1725 +#650 := [rewrite]: #316
1.1726 +#653 := [monotonicity #650]: #652
1.1727 +#644 := [monotonicity #653]: #654
1.1728 +#287 := [monotonicity #644]: #646
1.1729 +#292 := [trans #287 #291]: #646
1.1730 +#303 := [quant-inst #41 #44 #42]: #645
1.1731 +#293 := [mp #303 #292]: #307
1.1732 +#336 := [unit-resolution #293 #682]: #648
1.1733 +#631 := (not #648)
1.1734 +#638 := (or #631 #326 #651)
1.1735 +#640 := [def-axiom]: #638
1.1736 +#338 := [unit-resolution #640 #336]: #337
1.1737 +#340 := [unit-resolution #338 #627 #629]: false
1.1738 +#618 := [lemma #340]: #126
1.1739 +#329 := (or #326 #139)
1.1740 +#317 := (or #326 #139 #237)
1.1741 +#328 := [def-axiom]: #317
1.1742 +#257 := [unit-resolution #328 #147]: #329
1.1743 +#619 := [unit-resolution #257 #618]: #326
1.1744 +#332 := (or #139 #651)
1.1745 +#354 := (or #352 #139 #651)
1.1746 +#245 := [def-axiom]: #354
1.1747 +#616 := [unit-resolution #245 #622]: #332
1.1748 +#620 := [unit-resolution #616 #618]: #651
1.1749 +#617 := (or #130 #315)
1.1750 +#637 := (or #631 #130 #315)
1.1751 +#273 := [def-axiom]: #637
1.1752 +#621 := [unit-resolution #273 #336]: #617
1.1753 +[unit-resolution #621 #620 #619]: false
1.1754 +unsat
1.1755 +8424513290e59440c92fec106021e2354c2f6a1c 149 0
1.1756 +#2 := false
1.1757 +decl f3 :: (-> S2 S3 S1)
1.1758 +decl f6 :: (-> S4 S3 S3)
1.1759 +decl f11 :: S3
1.1760 +#42 := f11
1.1761 +decl f7 :: (-> S5 S3 S4)
1.1762 +decl f9 :: S5
1.1763 +#33 := f9
1.1764 +#43 := (f7 f9 f11)
1.1765 +#44 := (f6 #43 f11)
1.1766 +decl f10 :: S2
1.1767 +#41 := f10
1.1768 +#45 := (f3 f10 #44)
1.1769 +decl f1 :: S1
1.1770 +#4 := f1
1.1771 +#123 := (= f1 #45)
1.1772 +#136 := (not #123)
1.1773 +#632 := [hypothesis]: #136
1.1774 +#47 := (f3 f10 f11)
1.1775 +#127 := (= f1 #47)
1.1776 +#322 := (or #127 #123)
1.1777 +#137 := (iff #127 #136)
1.1778 +#48 := (= #47 f1)
1.1779 +#46 := (= #45 f1)
1.1780 +#49 := (iff #46 #48)
1.1781 +#50 := (not #49)
1.1782 +#140 := (iff #50 #137)
1.1783 +#130 := (iff #123 #127)
1.1784 +#133 := (not #130)
1.1785 +#138 := (iff #133 #137)
1.1786 +#139 := [rewrite]: #138
1.1787 +#134 := (iff #50 #133)
1.1788 +#131 := (iff #49 #130)
1.1789 +#128 := (iff #48 #127)
1.1790 +#129 := [rewrite]: #128
1.1791 +#125 := (iff #46 #123)
1.1792 +#126 := [rewrite]: #125
1.1793 +#132 := [monotonicity #126 #129]: #131
1.1794 +#135 := [monotonicity #132]: #134
1.1795 +#141 := [trans #135 #139]: #140
1.1796 +#122 := [asserted]: #50
1.1797 +#144 := [mp #122 #141]: #137
1.1798 +#234 := (not #137)
1.1799 +#321 := (or #127 #123 #234)
1.1800 +#235 := [def-axiom]: #321
1.1801 +#236 := [unit-resolution #235 #144]: #322
1.1802 +#633 := [unit-resolution #236 #632]: #127
1.1803 +#323 := (not #127)
1.1804 +#634 := (or #123 #323)
1.1805 +#22 := (:var 0 S3)
1.1806 +#20 := (:var 1 S3)
1.1807 +#34 := (f7 f9 #20)
1.1808 +#35 := (f6 #34 #22)
1.1809 +#18 := (:var 2 S2)
1.1810 +#36 := (f3 #18 #35)
1.1811 +#673 := (pattern #36)
1.1812 +#28 := (f3 #18 #22)
1.1813 +#96 := (= f1 #28)
1.1814 +#169 := (not #96)
1.1815 +#26 := (f3 #18 #20)
1.1816 +#93 := (= f1 #26)
1.1817 +#168 := (not #93)
1.1818 +#152 := (or #168 #169)
1.1819 +#153 := (not #152)
1.1820 +#109 := (= f1 #36)
1.1821 +#170 := (iff #109 #153)
1.1822 +#674 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #673) #170)
1.1823 +#173 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #170)
1.1824 +#677 := (iff #173 #674)
1.1825 +#675 := (iff #170 #170)
1.1826 +#676 := [refl]: #675
1.1827 +#678 := [quant-intro #676]: #677
1.1828 +#113 := (and #93 #96)
1.1829 +#116 := (iff #109 #113)
1.1830 +#119 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #116)
1.1831 +#174 := (iff #119 #173)
1.1832 +#171 := (iff #116 #170)
1.1833 +#154 := (iff #113 #153)
1.1834 +#155 := [rewrite]: #154
1.1835 +#172 := [monotonicity #155]: #171
1.1836 +#175 := [quant-intro #172]: #174
1.1837 +#150 := (~ #119 #119)
1.1838 +#165 := (~ #116 #116)
1.1839 +#166 := [refl]: #165
1.1840 +#151 := [nnf-pos #166]: #150
1.1841 +#29 := (= #28 f1)
1.1842 +#27 := (= #26 f1)
1.1843 +#38 := (and #27 #29)
1.1844 +#37 := (= #36 f1)
1.1845 +#39 := (iff #37 #38)
1.1846 +#40 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #39)
1.1847 +#120 := (iff #40 #119)
1.1848 +#117 := (iff #39 #116)
1.1849 +#114 := (iff #38 #113)
1.1850 +#97 := (iff #29 #96)
1.1851 +#98 := [rewrite]: #97
1.1852 +#94 := (iff #27 #93)
1.1853 +#95 := [rewrite]: #94
1.1854 +#115 := [monotonicity #95 #98]: #114
1.1855 +#111 := (iff #37 #109)
1.1856 +#112 := [rewrite]: #111
1.1857 +#118 := [monotonicity #112 #115]: #117
1.1858 +#121 := [quant-intro #118]: #120
1.1859 +#108 := [asserted]: #40
1.1860 +#124 := [mp #108 #121]: #119
1.1861 +#167 := [mp~ #124 #151]: #119
1.1862 +#176 := [mp #167 #175]: #173
1.1863 +#679 := [mp #176 #678]: #674
1.1864 +#650 := (not #674)
1.1865 +#645 := (or #650 #130)
1.1866 +#327 := (or #323 #323)
1.1867 +#324 := (not #327)
1.1868 +#328 := (iff #123 #324)
1.1869 +#651 := (or #650 #328)
1.1870 +#299 := (iff #651 #645)
1.1871 +#642 := (iff #645 #645)
1.1872 +#300 := [rewrite]: #642
1.1873 +#648 := (iff #328 #130)
1.1874 +#313 := (iff #324 #127)
1.1875 +#646 := (not #323)
1.1876 +#640 := (iff #646 #127)
1.1877 +#312 := [rewrite]: #640
1.1878 +#301 := (iff #324 #646)
1.1879 +#307 := (iff #327 #323)
1.1880 +#644 := [rewrite]: #307
1.1881 +#433 := [monotonicity #644]: #301
1.1882 +#647 := [trans #433 #312]: #313
1.1883 +#649 := [monotonicity #647]: #648
1.1884 +#304 := [monotonicity #649]: #299
1.1885 +#643 := [trans #304 #300]: #299
1.1886 +#641 := [quant-inst #41 #42 #42]: #651
1.1887 +#284 := [mp #641 #643]: #645
1.1888 +#628 := [unit-resolution #284 #679]: #130
1.1889 +#627 := (or #133 #123 #323)
1.1890 +#288 := [def-axiom]: #627
1.1891 +#270 := [unit-resolution #288 #628]: #634
1.1892 +#635 := [unit-resolution #270 #633 #632]: false
1.1893 +#637 := [lemma #635]: #123
1.1894 +#326 := (or #323 #136)
1.1895 +#314 := (or #323 #136 #234)
1.1896 +#325 := [def-axiom]: #314
1.1897 +#254 := [unit-resolution #325 #144]: #326
1.1898 +#275 := [unit-resolution #254 #637]: #323
1.1899 +#276 := (or #136 #127)
1.1900 +#289 := (or #133 #136 #127)
1.1901 +#290 := [def-axiom]: #289
1.1902 +#638 := [unit-resolution #290 #628]: #276
1.1903 +[unit-resolution #638 #275 #637]: false
1.1904 +unsat
1.1905 +5973328496eea1e33493c38f9af9d86965f67ad9 287 0
1.1906 +#2 := false
1.1907 +decl f3 :: (-> S2 S3 S1)
1.1908 +decl f6 :: (-> S4 S3 S3)
1.1909 +decl f12 :: S3
1.1910 +#44 := f12
1.1911 +decl f7 :: (-> S5 S3 S4)
1.1912 +decl f11 :: S3
1.1913 +#42 := f11
1.1914 +decl f9 :: S5
1.1915 +#33 := f9
1.1916 +#43 := (f7 f9 f11)
1.1917 +#51 := (f6 #43 f12)
1.1918 +decl f10 :: S2
1.1919 +#41 := f10
1.1920 +#314 := (f3 f10 #51)
1.1921 +decl f1 :: S1
1.1922 +#4 := f1
1.1923 +#651 := (= f1 #314)
1.1924 +#249 := (f3 f10 f12)
1.1925 +#628 := (= f1 #249)
1.1926 +#625 := (not #628)
1.1927 +#339 := (f3 f10 f11)
1.1928 +#355 := (= f1 #339)
1.1929 +#356 := (not #355)
1.1930 +#614 := (or #356 #625)
1.1931 +#615 := (not #614)
1.1932 +#611 := (iff #615 #651)
1.1933 +#582 := (not #611)
1.1934 +decl f13 :: S3
1.1935 +#46 := f13
1.1936 +#334 := (f3 f10 f13)
1.1937 +#331 := (= f1 #334)
1.1938 +#335 := (not #331)
1.1939 +#484 := (or #335 #625)
1.1940 +#493 := (not #484)
1.1941 +#45 := (f7 f9 f12)
1.1942 +#47 := (f6 #45 f13)
1.1943 +#646 := (f3 f10 #47)
1.1944 +#632 := (= f1 #646)
1.1945 +#494 := (iff #493 #632)
1.1946 +#587 := (not #494)
1.1947 +#567 := [hypothesis]: #587
1.1948 +#22 := (:var 0 S3)
1.1949 +#20 := (:var 1 S3)
1.1950 +#34 := (f7 f9 #20)
1.1951 +#35 := (f6 #34 #22)
1.1952 +#18 := (:var 2 S2)
1.1953 +#36 := (f3 #18 #35)
1.1954 +#680 := (pattern #36)
1.1955 +#28 := (f3 #18 #22)
1.1956 +#103 := (= f1 #28)
1.1957 +#176 := (not #103)
1.1958 +#26 := (f3 #18 #20)
1.1959 +#100 := (= f1 #26)
1.1960 +#175 := (not #100)
1.1961 +#159 := (or #175 #176)
1.1962 +#160 := (not #159)
1.1963 +#116 := (= f1 #36)
1.1964 +#177 := (iff #116 #160)
1.1965 +#681 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #680) #177)
1.1966 +#180 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #177)
1.1967 +#684 := (iff #180 #681)
1.1968 +#682 := (iff #177 #177)
1.1969 +#683 := [refl]: #682
1.1970 +#685 := [quant-intro #683]: #684
1.1971 +#120 := (and #100 #103)
1.1972 +#123 := (iff #116 #120)
1.1973 +#126 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #123)
1.1974 +#181 := (iff #126 #180)
1.1975 +#178 := (iff #123 #177)
1.1976 +#161 := (iff #120 #160)
1.1977 +#162 := [rewrite]: #161
1.1978 +#179 := [monotonicity #162]: #178
1.1979 +#182 := [quant-intro #179]: #181
1.1980 +#157 := (~ #126 #126)
1.1981 +#172 := (~ #123 #123)
1.1982 +#173 := [refl]: #172
1.1983 +#158 := [nnf-pos #173]: #157
1.1984 +#29 := (= #28 f1)
1.1985 +#27 := (= #26 f1)
1.1986 +#38 := (and #27 #29)
1.1987 +#37 := (= #36 f1)
1.1988 +#39 := (iff #37 #38)
1.1989 +#40 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #39)
1.1990 +#127 := (iff #40 #126)
1.1991 +#124 := (iff #39 #123)
1.1992 +#121 := (iff #38 #120)
1.1993 +#104 := (iff #29 #103)
1.1994 +#105 := [rewrite]: #104
1.1995 +#101 := (iff #27 #100)
1.1996 +#102 := [rewrite]: #101
1.1997 +#122 := [monotonicity #102 #105]: #121
1.1998 +#118 := (iff #37 #116)
1.1999 +#119 := [rewrite]: #118
1.2000 +#125 := [monotonicity #119 #122]: #124
1.2001 +#128 := [quant-intro #125]: #127
1.2002 +#115 := [asserted]: #40
1.2003 +#131 := [mp #115 #128]: #126
1.2004 +#174 := [mp~ #131 #158]: #126
1.2005 +#183 := [mp #174 #182]: #180
1.2006 +#686 := [mp #183 #685]: #681
1.2007 +#306 := (not #681)
1.2008 +#498 := (or #306 #494)
1.2009 +#600 := (or #625 #335)
1.2010 +#482 := (not #600)
1.2011 +#483 := (iff #632 #482)
1.2012 +#499 := (or #306 #483)
1.2013 +#593 := (iff #499 #498)
1.2014 +#594 := (iff #498 #498)
1.2015 +#581 := [rewrite]: #594
1.2016 +#496 := (iff #483 #494)
1.2017 +#592 := (iff #632 #493)
1.2018 +#495 := (iff #592 #494)
1.2019 +#488 := [rewrite]: #495
1.2020 +#477 := (iff #483 #592)
1.2021 +#588 := (iff #482 #493)
1.2022 +#443 := (iff #600 #484)
1.2023 +#591 := [rewrite]: #443
1.2024 +#589 := [monotonicity #591]: #588
1.2025 +#492 := [monotonicity #589]: #477
1.2026 +#497 := [trans #492 #488]: #496
1.2027 +#590 := [monotonicity #497]: #593
1.2028 +#583 := [trans #590 #581]: #593
1.2029 +#500 := [quant-inst #41 #44 #46]: #499
1.2030 +#575 := [mp #500 #583]: #498
1.2031 +#568 := [unit-resolution #575 #686 #567]: false
1.2032 +#569 := [lemma #568]: #494
1.2033 +#633 := (not #632)
1.2034 +#357 := (or #356 #633)
1.2035 +#343 := (not #357)
1.2036 +#48 := (f6 #43 #47)
1.2037 +#49 := (f3 f10 #48)
1.2038 +#130 := (= f1 #49)
1.2039 +#143 := (not #130)
1.2040 +#570 := [hypothesis]: #143
1.2041 +#571 := (or #130 #357)
1.2042 +#358 := (iff #130 #343)
1.2043 +#629 := (or #306 #358)
1.2044 +#351 := [quant-inst #41 #42 #47]: #629
1.2045 +#566 := [unit-resolution #351 #686]: #358
1.2046 +#341 := (not #358)
1.2047 +#342 := (or #341 #130 #357)
1.2048 +#344 := [def-axiom]: #342
1.2049 +#557 := [unit-resolution #344 #566]: #571
1.2050 +#558 := [unit-resolution #557 #570]: #357
1.2051 +#597 := (or #306 #611)
1.2052 +#616 := (iff #651 #615)
1.2053 +#613 := (or #306 #616)
1.2054 +#618 := (iff #613 #597)
1.2055 +#461 := (iff #597 #597)
1.2056 +#462 := [rewrite]: #461
1.2057 +#612 := (iff #616 #611)
1.2058 +#617 := [rewrite]: #612
1.2059 +#460 := [monotonicity #617]: #618
1.2060 +#604 := [trans #460 #462]: #618
1.2061 +#619 := [quant-inst #41 #42 #44]: #613
1.2062 +#605 := [mp #619 #604]: #597
1.2063 +#560 := [unit-resolution #605 #686]: #611
1.2064 +#546 := (or #582 #615)
1.2065 +#653 := (not #651)
1.2066 +#319 := (or #335 #653)
1.2067 +#655 := (not #319)
1.2068 +#52 := (f7 f9 #51)
1.2069 +#53 := (f6 #52 f13)
1.2070 +#54 := (f3 f10 #53)
1.2071 +#134 := (= f1 #54)
1.2072 +#329 := (or #134 #130)
1.2073 +#144 := (iff #134 #143)
1.2074 +#55 := (= #54 f1)
1.2075 +#50 := (= #49 f1)
1.2076 +#56 := (iff #50 #55)
1.2077 +#57 := (not #56)
1.2078 +#147 := (iff #57 #144)
1.2079 +#137 := (iff #130 #134)
1.2080 +#140 := (not #137)
1.2081 +#145 := (iff #140 #144)
1.2082 +#146 := [rewrite]: #145
1.2083 +#141 := (iff #57 #140)
1.2084 +#138 := (iff #56 #137)
1.2085 +#135 := (iff #55 #134)
1.2086 +#136 := [rewrite]: #135
1.2087 +#132 := (iff #50 #130)
1.2088 +#133 := [rewrite]: #132
1.2089 +#139 := [monotonicity #133 #136]: #138
1.2090 +#142 := [monotonicity #139]: #141
1.2091 +#148 := [trans #142 #146]: #147
1.2092 +#129 := [asserted]: #57
1.2093 +#151 := [mp #129 #148]: #144
1.2094 +#241 := (not #144)
1.2095 +#328 := (or #134 #130 #241)
1.2096 +#242 := [def-axiom]: #328
1.2097 +#243 := [unit-resolution #242 #151]: #329
1.2098 +#561 := [unit-resolution #243 #570]: #134
1.2099 +#330 := (not #134)
1.2100 +#559 := (or #330 #655)
1.2101 +#652 := (iff #134 #655)
1.2102 +#311 := (or #306 #652)
1.2103 +#308 := (or #653 #335)
1.2104 +#440 := (not #308)
1.2105 +#647 := (iff #134 #440)
1.2106 +#649 := (or #306 #647)
1.2107 +#650 := (iff #649 #311)
1.2108 +#634 := (iff #311 #311)
1.2109 +#295 := [rewrite]: #634
1.2110 +#658 := (iff #647 #652)
1.2111 +#656 := (iff #440 #655)
1.2112 +#320 := (iff #308 #319)
1.2113 +#654 := [rewrite]: #320
1.2114 +#657 := [monotonicity #654]: #656
1.2115 +#648 := [monotonicity #657]: #658
1.2116 +#291 := [monotonicity #648]: #650
1.2117 +#296 := [trans #291 #295]: #650
1.2118 +#307 := [quant-inst #41 #51 #46]: #649
1.2119 +#297 := [mp #307 #296]: #311
1.2120 +#562 := [unit-resolution #297 #686]: #652
1.2121 +#635 := (not #652)
1.2122 +#642 := (or #635 #330 #655)
1.2123 +#644 := [def-axiom]: #642
1.2124 +#563 := [unit-resolution #644 #562]: #559
1.2125 +#543 := [unit-resolution #563 #561]: #655
1.2126 +#637 := (or #319 #651)
1.2127 +#638 := [def-axiom]: #637
1.2128 +#544 := [unit-resolution #638 #543]: #651
1.2129 +#576 := (or #582 #615 #653)
1.2130 +#577 := [def-axiom]: #576
1.2131 +#547 := [unit-resolution #577 #544]: #546
1.2132 +#548 := [unit-resolution #547 #560]: #615
1.2133 +#606 := (or #614 #355)
1.2134 +#572 := [def-axiom]: #606
1.2135 +#549 := [unit-resolution #572 #548]: #355
1.2136 +#631 := (or #343 #356 #633)
1.2137 +#340 := [def-axiom]: #631
1.2138 +#550 := [unit-resolution #340 #549 #558]: #633
1.2139 +#298 := (or #319 #331)
1.2140 +#636 := [def-axiom]: #298
1.2141 +#551 := [unit-resolution #636 #543]: #331
1.2142 +#574 := (or #614 #628)
1.2143 +#584 := [def-axiom]: #574
1.2144 +#552 := [unit-resolution #584 #548]: #628
1.2145 +#609 := (or #493 #335 #625)
1.2146 +#603 := [def-axiom]: #609
1.2147 +#553 := [unit-resolution #603 #552 #551]: #493
1.2148 +#441 := (or #587 #484 #632)
1.2149 +#442 := [def-axiom]: #441
1.2150 +#554 := [unit-resolution #442 #553 #550 #569]: false
1.2151 +#555 := [lemma #554]: #130
1.2152 +#545 := (or #143 #343)
1.2153 +#622 := (or #341 #143 #343)
1.2154 +#623 := [def-axiom]: #622
1.2155 +#556 := [unit-resolution #623 #566]: #545
1.2156 +#534 := [unit-resolution #556 #555]: #343
1.2157 +#630 := (or #357 #632)
1.2158 +#627 := [def-axiom]: #630
1.2159 +#535 := [unit-resolution #627 #534]: #632
1.2160 +#610 := (or #587 #493 #633)
1.2161 +#439 := [def-axiom]: #610
1.2162 +#537 := [unit-resolution #439 #535 #569]: #493
1.2163 +#602 := (or #484 #628)
1.2164 +#608 := [def-axiom]: #602
1.2165 +#538 := [unit-resolution #608 #537]: #628
1.2166 +#352 := (or #357 #355)
1.2167 +#626 := [def-axiom]: #352
1.2168 +#539 := [unit-resolution #626 #534]: #355
1.2169 +#585 := (or #615 #356 #625)
1.2170 +#586 := [def-axiom]: #585
1.2171 +#540 := [unit-resolution #586 #539 #538]: #615
1.2172 +#333 := (or #330 #143)
1.2173 +#321 := (or #330 #143 #241)
1.2174 +#332 := [def-axiom]: #321
1.2175 +#261 := [unit-resolution #332 #151]: #333
1.2176 +#541 := [unit-resolution #261 #555]: #330
1.2177 +#536 := (or #134 #319)
1.2178 +#641 := (or #635 #134 #319)
1.2179 +#277 := [def-axiom]: #641
1.2180 +#542 := [unit-resolution #277 #562]: #536
1.2181 +#528 := [unit-resolution #542 #541]: #319
1.2182 +#607 := (or #484 #331)
1.2183 +#601 := [def-axiom]: #607
1.2184 +#524 := [unit-resolution #601 #537]: #331
1.2185 +#639 := (or #655 #335 #653)
1.2186 +#640 := [def-axiom]: #639
1.2187 +#525 := [unit-resolution #640 #524 #528]: #653
1.2188 +#578 := (or #582 #614 #651)
1.2189 +#579 := [def-axiom]: #578
1.2190 +#526 := [unit-resolution #579 #525 #540]: #582
1.2191 +[unit-resolution #605 #686 #526]: false
1.2192 +unsat
1.2193 +6c759b8f06a9510b6e4f2c41f45fd7a908ea138f 22 0
1.2194 +#2 := false
1.2195 +decl f13 :: (-> S7 S3 S4)
1.2196 +decl f4 :: S3
1.2197 +#8 := f4
1.2198 +decl f14 :: S7
1.2199 +#50 := f14
1.2200 +#51 := (f13 f14 f4)
1.2201 +#52 := (= #51 #51)
1.2202 +#53 := (not #52)
1.2203 +#148 := (iff #53 false)
1.2204 +#1 := true
1.2205 +#143 := (not true)
1.2206 +#146 := (iff #143 false)
1.2207 +#147 := [rewrite]: #146
1.2208 +#144 := (iff #53 #143)
1.2209 +#140 := (iff #52 true)
1.2210 +#142 := [rewrite]: #140
1.2211 +#145 := [monotonicity #142]: #144
1.2212 +#149 := [trans #145 #147]: #148
1.2213 +#139 := [asserted]: #53
1.2214 +[mp #139 #149]: false
1.2215 +unsat
1.2216 +eac8197a82f6b3a5c2024430d69641bb761b0abc 60 0
1.2217 +#2 := false
1.2218 +decl f3 :: (-> S2 S3 S1)
1.2219 +decl f4 :: S3
1.2220 +#9 := f4
1.2221 +decl f10 :: S2
1.2222 +#41 := f10
1.2223 +#42 := (f3 f10 f4)
1.2224 +decl f1 :: S1
1.2225 +#4 := f1
1.2226 +#118 := (= f1 #42)
1.2227 +#43 := (= #42 f1)
1.2228 +#44 := (not #43)
1.2229 +#45 := (not #44)
1.2230 +#130 := (iff #45 #118)
1.2231 +#122 := (not #118)
1.2232 +#125 := (not #122)
1.2233 +#128 := (iff #125 #118)
1.2234 +#129 := [rewrite]: #128
1.2235 +#126 := (iff #45 #125)
1.2236 +#123 := (iff #44 #122)
1.2237 +#120 := (iff #43 #118)
1.2238 +#121 := [rewrite]: #120
1.2239 +#124 := [monotonicity #121]: #123
1.2240 +#127 := [monotonicity #124]: #126
1.2241 +#131 := [trans #127 #129]: #130
1.2242 +#117 := [asserted]: #45
1.2243 +#134 := [mp #117 #131]: #118
1.2244 +#8 := (:var 0 S2)
1.2245 +#10 := (f3 #8 f4)
1.2246 +#642 := (pattern #10)
1.2247 +#66 := (= f1 #10)
1.2248 +#69 := (not #66)
1.2249 +#643 := (forall (vars (?v0 S2)) (:pat #642) #69)
1.2250 +#72 := (forall (vars (?v0 S2)) #69)
1.2251 +#646 := (iff #72 #643)
1.2252 +#644 := (iff #69 #69)
1.2253 +#645 := [refl]: #644
1.2254 +#647 := [quant-intro #645]: #646
1.2255 +#148 := (~ #72 #72)
1.2256 +#146 := (~ #69 #69)
1.2257 +#147 := [refl]: #146
1.2258 +#149 := [nnf-pos #147]: #148
1.2259 +#11 := (= #10 f1)
1.2260 +#12 := (not #11)
1.2261 +#13 := (forall (vars (?v0 S2)) #12)
1.2262 +#73 := (iff #13 #72)
1.2263 +#70 := (iff #12 #69)
1.2264 +#67 := (iff #11 #66)
1.2265 +#68 := [rewrite]: #67
1.2266 +#71 := [monotonicity #68]: #70
1.2267 +#74 := [quant-intro #71]: #73
1.2268 +#65 := [asserted]: #13
1.2269 +#77 := [mp #65 #74]: #72
1.2270 +#133 := [mp~ #77 #149]: #72
1.2271 +#648 := [mp #133 #647]: #643
1.2272 +#225 := (not #643)
1.2273 +#312 := (or #225 #122)
1.2274 +#226 := [quant-inst #41]: #312
1.2275 +[unit-resolution #226 #648 #134]: false
1.2276 +unsat
1.2277 +32295808d649b2df10d022ec20bfa2f501001522 48 0
1.2278 +#2 := false
1.2279 +decl f3 :: (-> S2 S3 S1)
1.2280 +decl f5 :: S3
1.2281 +#14 := f5
1.2282 +decl f10 :: S2
1.2283 +#41 := f10
1.2284 +#42 := (f3 f10 f5)
1.2285 +decl f1 :: S1
1.2286 +#4 := f1
1.2287 +#117 := (= f1 #42)
1.2288 +#121 := (not #117)
1.2289 +#43 := (= #42 f1)
1.2290 +#44 := (not #43)
1.2291 +#122 := (iff #44 #121)
1.2292 +#119 := (iff #43 #117)
1.2293 +#120 := [rewrite]: #119
1.2294 +#123 := [monotonicity #120]: #122
1.2295 +#116 := [asserted]: #44
1.2296 +#126 := [mp #116 #123]: #121
1.2297 +#8 := (:var 0 S2)
1.2298 +#15 := (f3 #8 f5)
1.2299 +#641 := (pattern #15)
1.2300 +#75 := (= f1 #15)
1.2301 +#642 := (forall (vars (?v0 S2)) (:pat #641) #75)
1.2302 +#79 := (forall (vars (?v0 S2)) #75)
1.2303 +#645 := (iff #79 #642)
1.2304 +#643 := (iff #75 #75)
1.2305 +#644 := [refl]: #643
1.2306 +#646 := [quant-intro #644]: #645
1.2307 +#128 := (~ #79 #79)
1.2308 +#127 := (~ #75 #75)
1.2309 +#142 := [refl]: #127
1.2310 +#129 := [nnf-pos #142]: #128
1.2311 +#16 := (= #15 f1)
1.2312 +#17 := (forall (vars (?v0 S2)) #16)
1.2313 +#80 := (iff #17 #79)
1.2314 +#77 := (iff #16 #75)
1.2315 +#78 := [rewrite]: #77
1.2316 +#81 := [quant-intro #78]: #80
1.2317 +#74 := [asserted]: #17
1.2318 +#84 := [mp #74 #81]: #79
1.2319 +#143 := [mp~ #84 #129]: #79
1.2320 +#647 := [mp #143 #646]: #642
1.2321 +#217 := (not #642)
1.2322 +#304 := (or #217 #117)
1.2323 +#218 := [quant-inst #41]: #304
1.2324 +[unit-resolution #218 #647 #126]: false
1.2325 +unsat
1.2326 +dfe83e391823f1cbfcca9d6fb06c0ae74a22248a 126 0
1.2327 +#2 := false
1.2328 +decl f3 :: (-> S2 S3 S1)
1.2329 +decl f6 :: (-> S4 S3 S3)
1.2330 +decl f12 :: S3
1.2331 +#44 := f12
1.2332 +decl f7 :: (-> S5 S3 S4)
1.2333 +decl f11 :: S3
1.2334 +#42 := f11
1.2335 +decl f8 :: S5
1.2336 +#19 := f8
1.2337 +#43 := (f7 f8 f11)
1.2338 +#45 := (f6 #43 f12)
1.2339 +decl f10 :: S2
1.2340 +#41 := f10
1.2341 +#46 := (f3 f10 #45)
1.2342 +decl f1 :: S1
1.2343 +#4 := f1
1.2344 +#127 := (= f1 #46)
1.2345 +#146 := (not #127)
1.2346 +#650 := [hypothesis]: #146
1.2347 +#50 := (f3 f10 f12)
1.2348 +#134 := (= f1 #50)
1.2349 +#48 := (f3 f10 f11)
1.2350 +#131 := (= f1 #48)
1.2351 +#137 := (or #131 #134)
1.2352 +#338 := (or #137 #127)
1.2353 +#147 := (iff #137 #146)
1.2354 +#51 := (= #50 f1)
1.2355 +#49 := (= #48 f1)
1.2356 +#52 := (or #49 #51)
1.2357 +#47 := (= #46 f1)
1.2358 +#53 := (iff #47 #52)
1.2359 +#54 := (not #53)
1.2360 +#150 := (iff #54 #147)
1.2361 +#140 := (iff #127 #137)
1.2362 +#143 := (not #140)
1.2363 +#148 := (iff #143 #147)
1.2364 +#149 := [rewrite]: #148
1.2365 +#144 := (iff #54 #143)
1.2366 +#141 := (iff #53 #140)
1.2367 +#138 := (iff #52 #137)
1.2368 +#135 := (iff #51 #134)
1.2369 +#136 := [rewrite]: #135
1.2370 +#132 := (iff #49 #131)
1.2371 +#133 := [rewrite]: #132
1.2372 +#139 := [monotonicity #133 #136]: #138
1.2373 +#129 := (iff #47 #127)
1.2374 +#130 := [rewrite]: #129
1.2375 +#142 := [monotonicity #130 #139]: #141
1.2376 +#145 := [monotonicity #142]: #144
1.2377 +#151 := [trans #145 #149]: #150
1.2378 +#126 := [asserted]: #54
1.2379 +#154 := [mp #126 #151]: #147
1.2380 +#264 := (not #147)
1.2381 +#337 := (or #137 #127 #264)
1.2382 +#334 := [def-axiom]: #337
1.2383 +#317 := [unit-resolution #334 #154]: #338
1.2384 +#322 := [unit-resolution #317 #650]: #137
1.2385 +#324 := (not #137)
1.2386 +#653 := (or #127 #324)
1.2387 +#22 := (:var 0 S3)
1.2388 +#20 := (:var 1 S3)
1.2389 +#21 := (f7 f8 #20)
1.2390 +#23 := (f6 #21 #22)
1.2391 +#18 := (:var 2 S2)
1.2392 +#24 := (f3 #18 #23)
1.2393 +#676 := (pattern #24)
1.2394 +#28 := (f3 #18 #22)
1.2395 +#100 := (= f1 #28)
1.2396 +#26 := (f3 #18 #20)
1.2397 +#97 := (= f1 #26)
1.2398 +#103 := (or #97 #100)
1.2399 +#93 := (= f1 #24)
1.2400 +#106 := (iff #93 #103)
1.2401 +#677 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #676) #106)
1.2402 +#109 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #106)
1.2403 +#680 := (iff #109 #677)
1.2404 +#678 := (iff #106 #106)
1.2405 +#679 := [refl]: #678
1.2406 +#681 := [quant-intro #679]: #680
1.2407 +#158 := (~ #109 #109)
1.2408 +#172 := (~ #106 #106)
1.2409 +#173 := [refl]: #172
1.2410 +#159 := [nnf-pos #173]: #158
1.2411 +#29 := (= #28 f1)
1.2412 +#27 := (= #26 f1)
1.2413 +#30 := (or #27 #29)
1.2414 +#25 := (= #24 f1)
1.2415 +#31 := (iff #25 #30)
1.2416 +#32 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #31)
1.2417 +#110 := (iff #32 #109)
1.2418 +#107 := (iff #31 #106)
1.2419 +#104 := (iff #30 #103)
1.2420 +#101 := (iff #29 #100)
1.2421 +#102 := [rewrite]: #101
1.2422 +#98 := (iff #27 #97)
1.2423 +#99 := [rewrite]: #98
1.2424 +#105 := [monotonicity #99 #102]: #104
1.2425 +#95 := (iff #25 #93)
1.2426 +#96 := [rewrite]: #95
1.2427 +#108 := [monotonicity #96 #105]: #107
1.2428 +#111 := [quant-intro #108]: #110
1.2429 +#92 := [asserted]: #32
1.2430 +#114 := [mp #92 #111]: #109
1.2431 +#174 := [mp~ #114 #159]: #109
1.2432 +#682 := [mp #174 #681]: #677
1.2433 +#323 := (not #677)
1.2434 +#657 := (or #323 #140)
1.2435 +#658 := [quant-inst #41 #42 #44]: #657
1.2436 +#310 := [unit-resolution #658 #682]: #140
1.2437 +#659 := (or #143 #127 #324)
1.2438 +#660 := [def-axiom]: #659
1.2439 +#294 := [unit-resolution #660 #310]: #653
1.2440 +#637 := [unit-resolution #294 #322 #650]: false
1.2441 +#298 := [lemma #637]: #127
1.2442 +#311 := (or #324 #146)
1.2443 +#654 := (or #324 #146 #264)
1.2444 +#656 := [def-axiom]: #654
1.2445 +#443 := [unit-resolution #656 #154]: #311
1.2446 +#299 := [unit-resolution #443 #298]: #324
1.2447 +#300 := (or #146 #137)
1.2448 +#655 := (or #143 #146 #137)
1.2449 +#661 := [def-axiom]: #655
1.2450 +#301 := [unit-resolution #661 #310]: #300
1.2451 +[unit-resolution #301 #299 #298]: false
1.2452 +unsat
1.2453 +54d5adcc9aa92b5c35a0e590a6651cbf7d0b828e 162 0
1.2454 +#2 := false
1.2455 +decl f3 :: (-> S2 S3 S1)
1.2456 +decl f4 :: S3
1.2457 +#9 := f4
1.2458 +decl f10 :: S2
1.2459 +#41 := f10
1.2460 +#327 := (f3 f10 f4)
1.2461 +decl f1 :: S1
1.2462 +#4 := f1
1.2463 +#324 := (= f1 #327)
1.2464 +decl f11 :: S3
1.2465 +#42 := f11
1.2466 +#47 := (f3 f10 f11)
1.2467 +#127 := (= f1 #47)
1.2468 +#328 := (or #127 #324)
1.2469 +decl f6 :: (-> S4 S3 S3)
1.2470 +decl f7 :: (-> S5 S3 S4)
1.2471 +decl f8 :: S5
1.2472 +#19 := f8
1.2473 +#43 := (f7 f8 f11)
1.2474 +#44 := (f6 #43 f4)
1.2475 +#45 := (f3 f10 #44)
1.2476 +#123 := (= f1 #45)
1.2477 +#136 := (not #123)
1.2478 +#644 := [hypothesis]: #136
1.2479 +#322 := (or #127 #123)
1.2480 +#137 := (iff #127 #136)
1.2481 +#48 := (= #47 f1)
1.2482 +#46 := (= #45 f1)
1.2483 +#49 := (iff #46 #48)
1.2484 +#50 := (not #49)
1.2485 +#140 := (iff #50 #137)
1.2486 +#130 := (iff #123 #127)
1.2487 +#133 := (not #130)
1.2488 +#138 := (iff #133 #137)
1.2489 +#139 := [rewrite]: #138
1.2490 +#134 := (iff #50 #133)
1.2491 +#131 := (iff #49 #130)
1.2492 +#128 := (iff #48 #127)
1.2493 +#129 := [rewrite]: #128
1.2494 +#125 := (iff #46 #123)
1.2495 +#126 := [rewrite]: #125
1.2496 +#132 := [monotonicity #126 #129]: #131
1.2497 +#135 := [monotonicity #132]: #134
1.2498 +#141 := [trans #135 #139]: #140
1.2499 +#122 := [asserted]: #50
1.2500 +#144 := [mp #122 #141]: #137
1.2501 +#234 := (not #137)
1.2502 +#321 := (or #127 #123 #234)
1.2503 +#235 := [def-axiom]: #321
1.2504 +#236 := [unit-resolution #235 #144]: #322
1.2505 +#646 := [unit-resolution #236 #644]: #127
1.2506 +#650 := (not #328)
1.2507 +#290 := (or #123 #650)
1.2508 +#307 := (iff #123 #328)
1.2509 +#22 := (:var 0 S3)
1.2510 +#20 := (:var 1 S3)
1.2511 +#21 := (f7 f8 #20)
1.2512 +#23 := (f6 #21 #22)
1.2513 +#18 := (:var 2 S2)
1.2514 +#24 := (f3 #18 #23)
1.2515 +#666 := (pattern #24)
1.2516 +#28 := (f3 #18 #22)
1.2517 +#96 := (= f1 #28)
1.2518 +#26 := (f3 #18 #20)
1.2519 +#93 := (= f1 #26)
1.2520 +#99 := (or #93 #96)
1.2521 +#89 := (= f1 #24)
1.2522 +#102 := (iff #89 #99)
1.2523 +#667 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #666) #102)
1.2524 +#105 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #102)
1.2525 +#670 := (iff #105 #667)
1.2526 +#668 := (iff #102 #102)
1.2527 +#669 := [refl]: #668
1.2528 +#671 := [quant-intro #669]: #670
1.2529 +#148 := (~ #105 #105)
1.2530 +#162 := (~ #102 #102)
1.2531 +#163 := [refl]: #162
1.2532 +#149 := [nnf-pos #163]: #148
1.2533 +#29 := (= #28 f1)
1.2534 +#27 := (= #26 f1)
1.2535 +#30 := (or #27 #29)
1.2536 +#25 := (= #24 f1)
1.2537 +#31 := (iff #25 #30)
1.2538 +#32 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #31)
1.2539 +#106 := (iff #32 #105)
1.2540 +#103 := (iff #31 #102)
1.2541 +#100 := (iff #30 #99)
1.2542 +#97 := (iff #29 #96)
1.2543 +#98 := [rewrite]: #97
1.2544 +#94 := (iff #27 #93)
1.2545 +#95 := [rewrite]: #94
1.2546 +#101 := [monotonicity #95 #98]: #100
1.2547 +#91 := (iff #25 #89)
1.2548 +#92 := [rewrite]: #91
1.2549 +#104 := [monotonicity #92 #101]: #103
1.2550 +#107 := [quant-intro #104]: #106
1.2551 +#88 := [asserted]: #32
1.2552 +#110 := [mp #88 #107]: #105
1.2553 +#164 := [mp~ #110 #149]: #105
1.2554 +#672 := [mp #164 #671]: #667
1.2555 +#301 := (not #667)
1.2556 +#433 := (or #301 #307)
1.2557 +#640 := [quant-inst #41 #42 #9]: #433
1.2558 +#289 := [unit-resolution #640 #672]: #307
1.2559 +#641 := (not #307)
1.2560 +#299 := (or #641 #123 #650)
1.2561 +#304 := [def-axiom]: #299
1.2562 +#291 := [unit-resolution #304 #289]: #290
1.2563 +#629 := [unit-resolution #291 #644]: #650
1.2564 +#323 := (not #127)
1.2565 +#312 := (or #328 #323)
1.2566 +#313 := [def-axiom]: #312
1.2567 +#630 := [unit-resolution #313 #629 #646]: false
1.2568 +#631 := [lemma #630]: #123
1.2569 +#632 := (or #136 #328)
1.2570 +#642 := (or #641 #136 #328)
1.2571 +#300 := [def-axiom]: #642
1.2572 +#633 := [unit-resolution #300 #289]: #632
1.2573 +#635 := [unit-resolution #633 #631]: #328
1.2574 +#326 := (or #323 #136)
1.2575 +#314 := (or #323 #136 #234)
1.2576 +#325 := [def-axiom]: #314
1.2577 +#254 := [unit-resolution #325 #144]: #326
1.2578 +#637 := [unit-resolution #254 #631]: #323
1.2579 +#645 := (or #650 #127 #324)
1.2580 +#651 := [def-axiom]: #645
1.2581 +#275 := [unit-resolution #651 #637 #635]: #324
1.2582 +#8 := (:var 0 S2)
1.2583 +#10 := (f3 #8 f4)
1.2584 +#652 := (pattern #10)
1.2585 +#71 := (= f1 #10)
1.2586 +#74 := (not #71)
1.2587 +#653 := (forall (vars (?v0 S2)) (:pat #652) #74)
1.2588 +#77 := (forall (vars (?v0 S2)) #74)
1.2589 +#656 := (iff #77 #653)
1.2590 +#654 := (iff #74 #74)
1.2591 +#655 := [refl]: #654
1.2592 +#657 := [quant-intro #655]: #656
1.2593 +#158 := (~ #77 #77)
1.2594 +#156 := (~ #74 #74)
1.2595 +#157 := [refl]: #156
1.2596 +#159 := [nnf-pos #157]: #158
1.2597 +#11 := (= #10 f1)
1.2598 +#12 := (not #11)
1.2599 +#13 := (forall (vars (?v0 S2)) #12)
1.2600 +#78 := (iff #13 #77)
1.2601 +#75 := (iff #12 #74)
1.2602 +#72 := (iff #11 #71)
1.2603 +#73 := [rewrite]: #72
1.2604 +#76 := [monotonicity #73]: #75
1.2605 +#79 := [quant-intro #76]: #78
1.2606 +#70 := [asserted]: #13
1.2607 +#82 := [mp #70 #79]: #77
1.2608 +#143 := [mp~ #82 #159]: #77
1.2609 +#658 := [mp #143 #657]: #653
1.2610 +#647 := (not #324)
1.2611 +#628 := (not #653)
1.2612 +#634 := (or #628 #647)
1.2613 +#270 := [quant-inst #41]: #634
1.2614 +[unit-resolution #270 #658 #275]: false
1.2615 +unsat
1.2616 +6579b339206079120a92afc0dda92279c34507ae 136 0
1.2617 +#2 := false
1.2618 +decl f3 :: (-> S2 S3 S1)
1.2619 +decl f5 :: S3
1.2620 +#14 := f5
1.2621 +decl f10 :: S2
1.2622 +#41 := f10
1.2623 +#219 := (f3 f10 f5)
1.2624 +decl f1 :: S1
1.2625 +#4 := f1
1.2626 +#306 := (= f1 #219)
1.2627 +#633 := (not #306)
1.2628 +decl f11 :: S3
1.2629 +#42 := f11
1.2630 +#220 := (f3 f10 f11)
1.2631 +#307 := (= f1 #220)
1.2632 +#299 := (or #306 #307)
1.2633 +#284 := (not #299)
1.2634 +decl f6 :: (-> S4 S3 S3)
1.2635 +decl f7 :: (-> S5 S3 S4)
1.2636 +decl f8 :: S5
1.2637 +#19 := f8
1.2638 +#43 := (f7 f8 f11)
1.2639 +#44 := (f6 #43 f5)
1.2640 +#45 := (f3 f10 #44)
1.2641 +#120 := (= f1 #45)
1.2642 +#239 := (iff #120 #299)
1.2643 +#22 := (:var 0 S3)
1.2644 +#20 := (:var 1 S3)
1.2645 +#21 := (f7 f8 #20)
1.2646 +#23 := (f6 #21 #22)
1.2647 +#18 := (:var 2 S2)
1.2648 +#24 := (f3 #18 #23)
1.2649 +#651 := (pattern #24)
1.2650 +#28 := (f3 #18 #22)
1.2651 +#93 := (= f1 #28)
1.2652 +#26 := (f3 #18 #20)
1.2653 +#90 := (= f1 #26)
1.2654 +#96 := (or #90 #93)
1.2655 +#86 := (= f1 #24)
1.2656 +#99 := (iff #86 #96)
1.2657 +#652 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #651) #99)
1.2658 +#102 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #99)
1.2659 +#655 := (iff #102 #652)
1.2660 +#653 := (iff #99 #99)
1.2661 +#654 := [refl]: #653
1.2662 +#656 := [quant-intro #654]: #655
1.2663 +#133 := (~ #102 #102)
1.2664 +#147 := (~ #99 #99)
1.2665 +#148 := [refl]: #147
1.2666 +#134 := [nnf-pos #148]: #133
1.2667 +#29 := (= #28 f1)
1.2668 +#27 := (= #26 f1)
1.2669 +#30 := (or #27 #29)
1.2670 +#25 := (= #24 f1)
1.2671 +#31 := (iff #25 #30)
1.2672 +#32 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #31)
1.2673 +#103 := (iff #32 #102)
1.2674 +#100 := (iff #31 #99)
1.2675 +#97 := (iff #30 #96)
1.2676 +#94 := (iff #29 #93)
1.2677 +#95 := [rewrite]: #94
1.2678 +#91 := (iff #27 #90)
1.2679 +#92 := [rewrite]: #91
1.2680 +#98 := [monotonicity #92 #95]: #97
1.2681 +#88 := (iff #25 #86)
1.2682 +#89 := [rewrite]: #88
1.2683 +#101 := [monotonicity #89 #98]: #100
1.2684 +#104 := [quant-intro #101]: #103
1.2685 +#85 := [asserted]: #32
1.2686 +#107 := [mp #85 #104]: #102
1.2687 +#149 := [mp~ #107 #134]: #102
1.2688 +#657 := [mp #149 #656]: #652
1.2689 +#313 := (not #652)
1.2690 +#292 := (or #313 #239)
1.2691 +#221 := (or #307 #306)
1.2692 +#308 := (iff #120 #221)
1.2693 +#629 := (or #313 #308)
1.2694 +#286 := (iff #629 #292)
1.2695 +#625 := (iff #292 #292)
1.2696 +#297 := [rewrite]: #625
1.2697 +#312 := (iff #308 #239)
1.2698 +#310 := (iff #221 #299)
1.2699 +#311 := [rewrite]: #310
1.2700 +#309 := [monotonicity #311]: #312
1.2701 +#418 := [monotonicity #309]: #286
1.2702 +#298 := [trans #418 #297]: #286
1.2703 +#631 := [quant-inst #41 #42 #14]: #629
1.2704 +#632 := [mp #631 #298]: #292
1.2705 +#615 := [unit-resolution #632 #657]: #239
1.2706 +#285 := (not #239)
1.2707 +#616 := (or #285 #284)
1.2708 +#124 := (not #120)
1.2709 +#46 := (= #45 f1)
1.2710 +#47 := (not #46)
1.2711 +#125 := (iff #47 #124)
1.2712 +#122 := (iff #46 #120)
1.2713 +#123 := [rewrite]: #122
1.2714 +#126 := [monotonicity #123]: #125
1.2715 +#119 := [asserted]: #47
1.2716 +#129 := [mp #119 #126]: #124
1.2717 +#628 := (or #285 #120 #284)
1.2718 +#269 := [def-axiom]: #628
1.2719 +#619 := [unit-resolution #269 #129]: #616
1.2720 +#255 := [unit-resolution #619 #615]: #284
1.2721 +#634 := (or #299 #633)
1.2722 +#635 := [def-axiom]: #634
1.2723 +#620 := [unit-resolution #635 #255]: #633
1.2724 +#8 := (:var 0 S2)
1.2725 +#15 := (f3 #8 f5)
1.2726 +#644 := (pattern #15)
1.2727 +#78 := (= f1 #15)
1.2728 +#645 := (forall (vars (?v0 S2)) (:pat #644) #78)
1.2729 +#82 := (forall (vars (?v0 S2)) #78)
1.2730 +#648 := (iff #82 #645)
1.2731 +#646 := (iff #78 #78)
1.2732 +#647 := [refl]: #646
1.2733 +#649 := [quant-intro #647]: #648
1.2734 +#131 := (~ #82 #82)
1.2735 +#130 := (~ #78 #78)
1.2736 +#145 := [refl]: #130
1.2737 +#132 := [nnf-pos #145]: #131
1.2738 +#16 := (= #15 f1)
1.2739 +#17 := (forall (vars (?v0 S2)) #16)
1.2740 +#83 := (iff #17 #82)
1.2741 +#80 := (iff #16 #78)
1.2742 +#81 := [rewrite]: #80
1.2743 +#84 := [quant-intro #81]: #83
1.2744 +#77 := [asserted]: #17
1.2745 +#87 := [mp #77 #84]: #82
1.2746 +#146 := [mp~ #87 #132]: #82
1.2747 +#650 := [mp #146 #649]: #645
1.2748 +#617 := (not #645)
1.2749 +#618 := (or #617 #306)
1.2750 +#613 := [quant-inst #41]: #618
1.2751 +[unit-resolution #613 #650 #620]: false
1.2752 +unsat
1.2753 +21f3225a60811428730067e610d6913c3bcb0df3 155 0
1.2754 +#2 := false
1.2755 +decl f3 :: (-> S2 S3 S1)
1.2756 +decl f6 :: (-> S4 S3 S3)
1.2757 +decl f11 :: S3
1.2758 +#42 := f11
1.2759 +decl f7 :: (-> S5 S3 S4)
1.2760 +decl f12 :: S3
1.2761 +#44 := f12
1.2762 +decl f8 :: S5
1.2763 +#19 := f8
1.2764 +#48 := (f7 f8 f12)
1.2765 +#49 := (f6 #48 f11)
1.2766 +decl f10 :: S2
1.2767 +#41 := f10
1.2768 +#50 := (f3 f10 #49)
1.2769 +decl f1 :: S1
1.2770 +#4 := f1
1.2771 +#130 := (= f1 #50)
1.2772 +#326 := (not #130)
1.2773 +#43 := (f7 f8 f11)
1.2774 +#45 := (f6 #43 f12)
1.2775 +#46 := (f3 f10 #45)
1.2776 +#126 := (= f1 #46)
1.2777 +#139 := (not #126)
1.2778 +#245 := [hypothesis]: #139
1.2779 +#325 := (or #130 #126)
1.2780 +#140 := (iff #130 #139)
1.2781 +#51 := (= #50 f1)
1.2782 +#47 := (= #46 f1)
1.2783 +#52 := (iff #47 #51)
1.2784 +#53 := (not #52)
1.2785 +#143 := (iff #53 #140)
1.2786 +#133 := (iff #126 #130)
1.2787 +#136 := (not #133)
1.2788 +#141 := (iff #136 #140)
1.2789 +#142 := [rewrite]: #141
1.2790 +#137 := (iff #53 #136)
1.2791 +#134 := (iff #52 #133)
1.2792 +#131 := (iff #51 #130)
1.2793 +#132 := [rewrite]: #131
1.2794 +#128 := (iff #47 #126)
1.2795 +#129 := [rewrite]: #128
1.2796 +#135 := [monotonicity #129 #132]: #134
1.2797 +#138 := [monotonicity #135]: #137
1.2798 +#144 := [trans #138 #142]: #143
1.2799 +#125 := [asserted]: #53
1.2800 +#147 := [mp #125 #144]: #140
1.2801 +#237 := (not #140)
1.2802 +#324 := (or #130 #126 #237)
1.2803 +#238 := [def-axiom]: #324
1.2804 +#239 := [unit-resolution #238 #147]: #325
1.2805 +#624 := [unit-resolution #239 #245]: #130
1.2806 +#330 := (f3 f10 f11)
1.2807 +#327 := (= f1 #330)
1.2808 +#331 := (f3 f10 f12)
1.2809 +#310 := (= f1 #331)
1.2810 +#647 := (or #310 #327)
1.2811 +#644 := (not #647)
1.2812 +#347 := (or #126 #644)
1.2813 +#634 := (iff #126 #647)
1.2814 +#22 := (:var 0 S3)
1.2815 +#20 := (:var 1 S3)
1.2816 +#21 := (f7 f8 #20)
1.2817 +#23 := (f6 #21 #22)
1.2818 +#18 := (:var 2 S2)
1.2819 +#24 := (f3 #18 #23)
1.2820 +#669 := (pattern #24)
1.2821 +#28 := (f3 #18 #22)
1.2822 +#99 := (= f1 #28)
1.2823 +#26 := (f3 #18 #20)
1.2824 +#96 := (= f1 #26)
1.2825 +#102 := (or #96 #99)
1.2826 +#92 := (= f1 #24)
1.2827 +#105 := (iff #92 #102)
1.2828 +#670 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #669) #105)
1.2829 +#108 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #105)
1.2830 +#673 := (iff #108 #670)
1.2831 +#671 := (iff #105 #105)
1.2832 +#672 := [refl]: #671
1.2833 +#674 := [quant-intro #672]: #673
1.2834 +#151 := (~ #108 #108)
1.2835 +#165 := (~ #105 #105)
1.2836 +#166 := [refl]: #165
1.2837 +#152 := [nnf-pos #166]: #151
1.2838 +#29 := (= #28 f1)
1.2839 +#27 := (= #26 f1)
1.2840 +#30 := (or #27 #29)
1.2841 +#25 := (= #24 f1)
1.2842 +#31 := (iff #25 #30)
1.2843 +#32 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #31)
1.2844 +#109 := (iff #32 #108)
1.2845 +#106 := (iff #31 #105)
1.2846 +#103 := (iff #30 #102)
1.2847 +#100 := (iff #29 #99)
1.2848 +#101 := [rewrite]: #100
1.2849 +#97 := (iff #27 #96)
1.2850 +#98 := [rewrite]: #97
1.2851 +#104 := [monotonicity #98 #101]: #103
1.2852 +#94 := (iff #25 #92)
1.2853 +#95 := [rewrite]: #94
1.2854 +#107 := [monotonicity #95 #104]: #106
1.2855 +#110 := [quant-intro #107]: #109
1.2856 +#91 := [asserted]: #32
1.2857 +#113 := [mp #91 #110]: #108
1.2858 +#167 := [mp~ #113 #152]: #108
1.2859 +#675 := [mp #167 #674]: #670
1.2860 +#643 := (not #670)
1.2861 +#631 := (or #643 #634)
1.2862 +#304 := (or #327 #310)
1.2863 +#436 := (iff #126 #304)
1.2864 +#637 := (or #643 #436)
1.2865 +#638 := (iff #637 #631)
1.2866 +#278 := (iff #631 #631)
1.2867 +#279 := [rewrite]: #278
1.2868 +#635 := (iff #436 #634)
1.2869 +#632 := (iff #304 #647)
1.2870 +#633 := [rewrite]: #632
1.2871 +#636 := [monotonicity #633]: #635
1.2872 +#640 := [monotonicity #636]: #638
1.2873 +#641 := [trans #640 #279]: #638
1.2874 +#273 := [quant-inst #41 #42 #44]: #637
1.2875 +#639 := [mp #273 #641]: #631
1.2876 +#625 := [unit-resolution #639 #675]: #634
1.2877 +#642 := (not #634)
1.2878 +#628 := (or #642 #126 #644)
1.2879 +#629 := [def-axiom]: #628
1.2880 +#348 := [unit-resolution #629 #625]: #347
1.2881 +#622 := [unit-resolution #348 #245]: #644
1.2882 +#623 := (or #326 #647)
1.2883 +#649 := (iff #130 #647)
1.2884 +#315 := (or #643 #649)
1.2885 +#316 := [quant-inst #41 #44 #42]: #315
1.2886 +#626 := [unit-resolution #316 #675]: #649
1.2887 +#645 := (not #649)
1.2888 +#287 := (or #645 #326 #647)
1.2889 +#630 := [def-axiom]: #287
1.2890 +#627 := [unit-resolution #630 #626]: #623
1.2891 +#336 := [unit-resolution #627 #622 #624]: false
1.2892 +#337 := [lemma #336]: #126
1.2893 +#329 := (or #326 #139)
1.2894 +#317 := (or #326 #139 #237)
1.2895 +#328 := [def-axiom]: #317
1.2896 +#257 := [unit-resolution #328 #147]: #329
1.2897 +#338 := [unit-resolution #257 #337]: #326
1.2898 +#340 := (or #139 #647)
1.2899 +#335 := (or #642 #139 #647)
1.2900 +#351 := [def-axiom]: #335
1.2901 +#618 := [unit-resolution #351 #625]: #340
1.2902 +#619 := [unit-resolution #618 #337]: #647
1.2903 +#332 := (or #130 #644)
1.2904 +#303 := (or #645 #130 #644)
1.2905 +#646 := [def-axiom]: #303
1.2906 +#616 := [unit-resolution #646 #626]: #332
1.2907 +[unit-resolution #616 #619 #338]: false
1.2908 +unsat
1.2909 +0a38803d5203ebb9de80029b1e5de8bcd8e8f404 128 0
1.2910 +#2 := false
1.2911 +decl f3 :: (-> S2 S3 S1)
1.2912 +decl f6 :: (-> S4 S3 S3)
1.2913 +decl f11 :: S3
1.2914 +#42 := f11
1.2915 +decl f7 :: (-> S5 S3 S4)
1.2916 +decl f8 :: S5
1.2917 +#19 := f8
1.2918 +#43 := (f7 f8 f11)
1.2919 +#44 := (f6 #43 f11)
1.2920 +decl f10 :: S2
1.2921 +#41 := f10
1.2922 +#45 := (f3 f10 #44)
1.2923 +decl f1 :: S1
1.2924 +#4 := f1
1.2925 +#123 := (= f1 #45)
1.2926 +#136 := (not #123)
1.2927 +#627 := [hypothesis]: #136
1.2928 +#47 := (f3 f10 f11)
1.2929 +#127 := (= f1 #47)
1.2930 +#322 := (or #127 #123)
1.2931 +#137 := (iff #127 #136)
1.2932 +#48 := (= #47 f1)
1.2933 +#46 := (= #45 f1)
1.2934 +#49 := (iff #46 #48)
1.2935 +#50 := (not #49)
1.2936 +#140 := (iff #50 #137)
1.2937 +#130 := (iff #123 #127)
1.2938 +#133 := (not #130)
1.2939 +#138 := (iff #133 #137)
1.2940 +#139 := [rewrite]: #138
1.2941 +#134 := (iff #50 #133)
1.2942 +#131 := (iff #49 #130)
1.2943 +#128 := (iff #48 #127)
1.2944 +#129 := [rewrite]: #128
1.2945 +#125 := (iff #46 #123)
1.2946 +#126 := [rewrite]: #125
1.2947 +#132 := [monotonicity #126 #129]: #131
1.2948 +#135 := [monotonicity #132]: #134
1.2949 +#141 := [trans #135 #139]: #140
1.2950 +#122 := [asserted]: #50
1.2951 +#144 := [mp #122 #141]: #137
1.2952 +#234 := (not #137)
1.2953 +#321 := (or #127 #123 #234)
1.2954 +#235 := [def-axiom]: #321
1.2955 +#236 := [unit-resolution #235 #144]: #322
1.2956 +#288 := [unit-resolution #236 #627]: #127
1.2957 +#323 := (not #127)
1.2958 +#290 := (or #123 #323)
1.2959 +#22 := (:var 0 S3)
1.2960 +#20 := (:var 1 S3)
1.2961 +#21 := (f7 f8 #20)
1.2962 +#23 := (f6 #21 #22)
1.2963 +#18 := (:var 2 S2)
1.2964 +#24 := (f3 #18 #23)
1.2965 +#666 := (pattern #24)
1.2966 +#28 := (f3 #18 #22)
1.2967 +#96 := (= f1 #28)
1.2968 +#26 := (f3 #18 #20)
1.2969 +#93 := (= f1 #26)
1.2970 +#99 := (or #93 #96)
1.2971 +#89 := (= f1 #24)
1.2972 +#102 := (iff #89 #99)
1.2973 +#667 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #666) #102)
1.2974 +#105 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #102)
1.2975 +#670 := (iff #105 #667)
1.2976 +#668 := (iff #102 #102)
1.2977 +#669 := [refl]: #668
1.2978 +#671 := [quant-intro #669]: #670
1.2979 +#148 := (~ #105 #105)
1.2980 +#162 := (~ #102 #102)
1.2981 +#163 := [refl]: #162
1.2982 +#149 := [nnf-pos #163]: #148
1.2983 +#29 := (= #28 f1)
1.2984 +#27 := (= #26 f1)
1.2985 +#30 := (or #27 #29)
1.2986 +#25 := (= #24 f1)
1.2987 +#31 := (iff #25 #30)
1.2988 +#32 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #31)
1.2989 +#106 := (iff #32 #105)
1.2990 +#103 := (iff #31 #102)
1.2991 +#100 := (iff #30 #99)
1.2992 +#97 := (iff #29 #96)
1.2993 +#98 := [rewrite]: #97
1.2994 +#94 := (iff #27 #93)
1.2995 +#95 := [rewrite]: #94
1.2996 +#101 := [monotonicity #95 #98]: #100
1.2997 +#91 := (iff #25 #89)
1.2998 +#92 := [rewrite]: #91
1.2999 +#104 := [monotonicity #92 #101]: #103
1.3000 +#107 := [quant-intro #104]: #106
1.3001 +#88 := [asserted]: #32
1.3002 +#110 := [mp #88 #107]: #105
1.3003 +#164 := [mp~ #110 #149]: #105
1.3004 +#672 := [mp #164 #671]: #667
1.3005 +#301 := (not #667)
1.3006 +#433 := (or #301 #130)
1.3007 +#327 := (or #127 #127)
1.3008 +#324 := (iff #123 #327)
1.3009 +#640 := (or #301 #324)
1.3010 +#313 := (iff #640 #433)
1.3011 +#648 := (iff #433 #433)
1.3012 +#649 := [rewrite]: #648
1.3013 +#644 := (iff #324 #130)
1.3014 +#328 := (iff #327 #127)
1.3015 +#307 := [rewrite]: #328
1.3016 +#646 := [monotonicity #307]: #644
1.3017 +#647 := [monotonicity #646]: #313
1.3018 +#650 := [trans #647 #649]: #313
1.3019 +#312 := [quant-inst #41 #42 #42]: #640
1.3020 +#645 := [mp #312 #650]: #433
1.3021 +#289 := [unit-resolution #645 #672]: #130
1.3022 +#651 := (or #133 #123 #323)
1.3023 +#641 := [def-axiom]: #651
1.3024 +#291 := [unit-resolution #641 #289]: #290
1.3025 +#629 := [unit-resolution #291 #288 #627]: false
1.3026 +#630 := [lemma #629]: #123
1.3027 +#326 := (or #323 #136)
1.3028 +#314 := (or #323 #136 #234)
1.3029 +#325 := [def-axiom]: #314
1.3030 +#254 := [unit-resolution #325 #144]: #326
1.3031 +#631 := [unit-resolution #254 #630]: #323
1.3032 +#632 := (or #136 #127)
1.3033 +#299 := (or #133 #136 #127)
1.3034 +#304 := [def-axiom]: #299
1.3035 +#633 := [unit-resolution #304 #289]: #632
1.3036 +[unit-resolution #633 #631 #630]: false
1.3037 +unsat
1.3038 +a9b4d2c6d5d71402741164958baf8befeec2192a 266 0
1.3039 +#2 := false
1.3040 +decl f3 :: (-> S2 S3 S1)
1.3041 +decl f12 :: S3
1.3042 +#44 := f12
1.3043 +decl f10 :: S2
1.3044 +#41 := f10
1.3045 +#623 := (f3 f10 f12)
1.3046 +decl f1 :: S1
1.3047 +#4 := f1
1.3048 +#336 := (= f1 #623)
1.3049 +decl f13 :: S3
1.3050 +#46 := f13
1.3051 +#334 := (f3 f10 f13)
1.3052 +#331 := (= f1 #334)
1.3053 +#621 := (or #331 #336)
1.3054 +decl f6 :: (-> S4 S3 S3)
1.3055 +decl f7 :: (-> S5 S3 S4)
1.3056 +decl f8 :: S5
1.3057 +#19 := f8
1.3058 +#45 := (f7 f8 f12)
1.3059 +#47 := (f6 #45 f13)
1.3060 +#308 := (f3 f10 #47)
1.3061 +#440 := (= f1 #308)
1.3062 +#615 := (iff #440 #621)
1.3063 +#581 := (not #615)
1.3064 +#593 := (not #621)
1.3065 +#605 := (not #336)
1.3066 +decl f11 :: S3
1.3067 +#42 := f11
1.3068 +#636 := (f3 f10 f11)
1.3069 +#637 := (= f1 #636)
1.3070 +#483 := (or #336 #637)
1.3071 +#608 := (not #483)
1.3072 +#43 := (f7 f8 f11)
1.3073 +#51 := (f6 #43 f12)
1.3074 +#335 := (f3 f10 #51)
1.3075 +#314 := (= f1 #335)
1.3076 +#591 := (iff #314 #483)
1.3077 +#583 := (not #591)
1.3078 +#576 := [hypothesis]: #583
1.3079 +#22 := (:var 0 S3)
1.3080 +#20 := (:var 1 S3)
1.3081 +#21 := (f7 f8 #20)
1.3082 +#23 := (f6 #21 #22)
1.3083 +#18 := (:var 2 S2)
1.3084 +#24 := (f3 #18 #23)
1.3085 +#673 := (pattern #24)
1.3086 +#28 := (f3 #18 #22)
1.3087 +#103 := (= f1 #28)
1.3088 +#26 := (f3 #18 #20)
1.3089 +#100 := (= f1 #26)
1.3090 +#106 := (or #100 #103)
1.3091 +#96 := (= f1 #24)
1.3092 +#109 := (iff #96 #106)
1.3093 +#674 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #673) #109)
1.3094 +#112 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #109)
1.3095 +#677 := (iff #112 #674)
1.3096 +#675 := (iff #109 #109)
1.3097 +#676 := [refl]: #675
1.3098 +#678 := [quant-intro #676]: #677
1.3099 +#155 := (~ #112 #112)
1.3100 +#169 := (~ #109 #109)
1.3101 +#170 := [refl]: #169
1.3102 +#156 := [nnf-pos #170]: #155
1.3103 +#29 := (= #28 f1)
1.3104 +#27 := (= #26 f1)
1.3105 +#30 := (or #27 #29)
1.3106 +#25 := (= #24 f1)
1.3107 +#31 := (iff #25 #30)
1.3108 +#32 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #31)
1.3109 +#113 := (iff #32 #112)
1.3110 +#110 := (iff #31 #109)
1.3111 +#107 := (iff #30 #106)
1.3112 +#104 := (iff #29 #103)
1.3113 +#105 := [rewrite]: #104
1.3114 +#101 := (iff #27 #100)
1.3115 +#102 := [rewrite]: #101
1.3116 +#108 := [monotonicity #102 #105]: #107
1.3117 +#98 := (iff #25 #96)
1.3118 +#99 := [rewrite]: #98
1.3119 +#111 := [monotonicity #99 #108]: #110
1.3120 +#114 := [quant-intro #111]: #113
1.3121 +#95 := [asserted]: #32
1.3122 +#117 := [mp #95 #114]: #112
1.3123 +#171 := [mp~ #117 #156]: #112
1.3124 +#679 := [mp #171 #678]: #674
1.3125 +#647 := (not #674)
1.3126 +#589 := (or #647 #591)
1.3127 +#600 := (or #637 #336)
1.3128 +#482 := (iff #314 #600)
1.3129 +#592 := (or #647 #482)
1.3130 +#492 := (iff #592 #589)
1.3131 +#495 := (iff #589 #589)
1.3132 +#488 := [rewrite]: #495
1.3133 +#493 := (iff #482 #591)
1.3134 +#484 := (iff #600 #483)
1.3135 +#443 := [rewrite]: #484
1.3136 +#588 := [monotonicity #443]: #493
1.3137 +#494 := [monotonicity #588]: #492
1.3138 +#496 := [trans #494 #488]: #492
1.3139 +#477 := [quant-inst #41 #42 #44]: #592
1.3140 +#497 := [mp #477 #496]: #589
1.3141 +#577 := [unit-resolution #497 #679 #576]: false
1.3142 +#578 := [lemma #577]: #591
1.3143 +#654 := (not #314)
1.3144 +#651 := (or #314 #331)
1.3145 +#648 := (not #651)
1.3146 +#52 := (f7 f8 #51)
1.3147 +#53 := (f6 #52 f13)
1.3148 +#54 := (f3 f10 #53)
1.3149 +#134 := (= f1 #54)
1.3150 +#330 := (not #134)
1.3151 +#48 := (f6 #43 #47)
1.3152 +#49 := (f3 f10 #48)
1.3153 +#130 := (= f1 #49)
1.3154 +#143 := (not #130)
1.3155 +#579 := [hypothesis]: #143
1.3156 +#329 := (or #134 #130)
1.3157 +#144 := (iff #134 #143)
1.3158 +#55 := (= #54 f1)
1.3159 +#50 := (= #49 f1)
1.3160 +#56 := (iff #50 #55)
1.3161 +#57 := (not #56)
1.3162 +#147 := (iff #57 #144)
1.3163 +#137 := (iff #130 #134)
1.3164 +#140 := (not #137)
1.3165 +#145 := (iff #140 #144)
1.3166 +#146 := [rewrite]: #145
1.3167 +#141 := (iff #57 #140)
1.3168 +#138 := (iff #56 #137)
1.3169 +#135 := (iff #55 #134)
1.3170 +#136 := [rewrite]: #135
1.3171 +#132 := (iff #50 #130)
1.3172 +#133 := [rewrite]: #132
1.3173 +#139 := [monotonicity #133 #136]: #138
1.3174 +#142 := [monotonicity #139]: #141
1.3175 +#148 := [trans #142 #146]: #147
1.3176 +#129 := [asserted]: #57
1.3177 +#151 := [mp #129 #148]: #144
1.3178 +#241 := (not #144)
1.3179 +#328 := (or #134 #130 #241)
1.3180 +#242 := [def-axiom]: #328
1.3181 +#243 := [unit-resolution #242 #151]: #329
1.3182 +#573 := [unit-resolution #243 #579]: #134
1.3183 +#564 := (or #330 #651)
1.3184 +#653 := (iff #134 #651)
1.3185 +#319 := (or #647 #653)
1.3186 +#320 := [quant-inst #41 #51 #46]: #319
1.3187 +#580 := [unit-resolution #320 #679]: #653
1.3188 +#649 := (not #653)
1.3189 +#291 := (or #649 #330 #651)
1.3190 +#634 := [def-axiom]: #291
1.3191 +#565 := [unit-resolution #634 #580]: #564
1.3192 +#567 := [unit-resolution #565 #573]: #651
1.3193 +#657 := (not #331)
1.3194 +#597 := (or #647 #615)
1.3195 +#620 := (or #336 #331)
1.3196 +#624 := (iff #440 #620)
1.3197 +#617 := (or #647 #624)
1.3198 +#612 := (iff #617 #597)
1.3199 +#619 := (iff #597 #597)
1.3200 +#460 := [rewrite]: #619
1.3201 +#616 := (iff #624 #615)
1.3202 +#625 := (iff #620 #621)
1.3203 +#614 := [rewrite]: #625
1.3204 +#611 := [monotonicity #614]: #616
1.3205 +#613 := [monotonicity #611]: #612
1.3206 +#461 := [trans #613 #460]: #612
1.3207 +#618 := [quant-inst #41 #44 #46]: #617
1.3208 +#462 := [mp #618 #461]: #597
1.3209 +#568 := [unit-resolution #462 #679]: #615
1.3210 +#558 := (or #581 #593)
1.3211 +#356 := (not #440)
1.3212 +#640 := (or #440 #637)
1.3213 +#629 := (not #640)
1.3214 +#570 := (or #130 #629)
1.3215 +#277 := (iff #130 #640)
1.3216 +#282 := (or #647 #277)
1.3217 +#638 := (or #637 #440)
1.3218 +#639 := (iff #130 #638)
1.3219 +#283 := (or #647 #639)
1.3220 +#643 := (iff #283 #282)
1.3221 +#632 := (iff #282 #282)
1.3222 +#633 := [rewrite]: #632
1.3223 +#642 := (iff #639 #277)
1.3224 +#635 := (iff #638 #640)
1.3225 +#641 := [rewrite]: #635
1.3226 +#644 := [monotonicity #641]: #642
1.3227 +#646 := [monotonicity #644]: #643
1.3228 +#339 := [trans #646 #633]: #643
1.3229 +#645 := [quant-inst #41 #42 #47]: #283
1.3230 +#355 := [mp #645 #339]: #282
1.3231 +#569 := [unit-resolution #355 #679]: #277
1.3232 +#626 := (not #277)
1.3233 +#630 := (or #626 #130 #629)
1.3234 +#627 := [def-axiom]: #630
1.3235 +#566 := [unit-resolution #627 #569]: #570
1.3236 +#571 := [unit-resolution #566 #579]: #629
1.3237 +#357 := (or #640 #356)
1.3238 +#343 := [def-axiom]: #357
1.3239 +#557 := [unit-resolution #343 #571]: #356
1.3240 +#575 := (or #581 #440 #593)
1.3241 +#572 := [def-axiom]: #575
1.3242 +#560 := [unit-resolution #572 #557]: #558
1.3243 +#561 := [unit-resolution #560 #568]: #593
1.3244 +#604 := (or #621 #657)
1.3245 +#498 := [def-axiom]: #604
1.3246 +#562 := [unit-resolution #498 #561]: #657
1.3247 +#306 := (or #648 #314 #331)
1.3248 +#311 := [def-axiom]: #306
1.3249 +#559 := [unit-resolution #311 #562 #567]: #314
1.3250 +#358 := (not #637)
1.3251 +#249 := (or #640 #358)
1.3252 +#628 := [def-axiom]: #249
1.3253 +#563 := [unit-resolution #628 #571]: #358
1.3254 +#499 := (or #621 #605)
1.3255 +#500 := [def-axiom]: #499
1.3256 +#543 := [unit-resolution #500 #561]: #605
1.3257 +#609 := (or #608 #336 #637)
1.3258 +#603 := [def-axiom]: #609
1.3259 +#544 := [unit-resolution #603 #543 #563]: #608
1.3260 +#441 := (or #583 #654 #483)
1.3261 +#442 := [def-axiom]: #441
1.3262 +#546 := [unit-resolution #442 #544 #559 #578]: false
1.3263 +#547 := [lemma #546]: #130
1.3264 +#333 := (or #330 #143)
1.3265 +#321 := (or #330 #143 #241)
1.3266 +#332 := [def-axiom]: #321
1.3267 +#261 := [unit-resolution #332 #151]: #333
1.3268 +#548 := [unit-resolution #261 #547]: #330
1.3269 +#549 := (or #134 #648)
1.3270 +#307 := (or #649 #134 #648)
1.3271 +#650 := [def-axiom]: #307
1.3272 +#550 := [unit-resolution #650 #580]: #549
1.3273 +#551 := [unit-resolution #550 #548]: #648
1.3274 +#655 := (or #651 #654)
1.3275 +#656 := [def-axiom]: #655
1.3276 +#552 := [unit-resolution #656 #551]: #654
1.3277 +#610 := (or #583 #314 #608)
1.3278 +#439 := [def-axiom]: #610
1.3279 +#553 := [unit-resolution #439 #552 #578]: #608
1.3280 +#606 := (or #483 #605)
1.3281 +#607 := [def-axiom]: #606
1.3282 +#554 := [unit-resolution #607 #553]: #605
1.3283 +#652 := (or #651 #657)
1.3284 +#658 := [def-axiom]: #652
1.3285 +#555 := [unit-resolution #658 #551]: #657
1.3286 +#590 := (or #593 #331 #336)
1.3287 +#594 := [def-axiom]: #590
1.3288 +#545 := [unit-resolution #594 #555 #554]: #593
1.3289 +#556 := (or #143 #640)
1.3290 +#631 := (or #626 #143 #640)
1.3291 +#340 := [def-axiom]: #631
1.3292 +#534 := [unit-resolution #340 #569]: #556
1.3293 +#535 := [unit-resolution #534 #547]: #640
1.3294 +#601 := (or #483 #358)
1.3295 +#602 := [def-axiom]: #601
1.3296 +#537 := [unit-resolution #602 #553]: #358
1.3297 +#351 := (or #629 #440 #637)
1.3298 +#352 := [def-axiom]: #351
1.3299 +#538 := [unit-resolution #352 #537 #535]: #440
1.3300 +#574 := (or #581 #356 #621)
1.3301 +#584 := [def-axiom]: #574
1.3302 +#539 := [unit-resolution #584 #538 #545]: #581
1.3303 +[unit-resolution #462 #679 #539]: false
1.3304 +unsat
1.3305 +c3c3648cfba9d6c85cac6f8d51a3b06b08975178 160 0
1.3306 +#2 := false
1.3307 +decl f3 :: (-> S2 S3 S1)
1.3308 +decl f12 :: S3
1.3309 +#44 := f12
1.3310 +decl f10 :: S2
1.3311 +#41 := f10
1.3312 +#50 := (f3 f10 f12)
1.3313 +decl f1 :: S1
1.3314 +#4 := f1
1.3315 +#134 := (= f1 #50)
1.3316 +#188 := (not #134)
1.3317 +decl f11 :: S3
1.3318 +#42 := f11
1.3319 +#48 := (f3 f10 f11)
1.3320 +#131 := (= f1 #48)
1.3321 +#187 := (not #131)
1.3322 +#189 := (or #187 #188)
1.3323 +#190 := (not #189)
1.3324 +#331 := [hypothesis]: #190
1.3325 +decl f6 :: (-> S4 S3 S3)
1.3326 +decl f7 :: (-> S5 S3 S4)
1.3327 +decl f9 :: S5
1.3328 +#33 := f9
1.3329 +#43 := (f7 f9 f11)
1.3330 +#45 := (f6 #43 f12)
1.3331 +#46 := (f3 f10 #45)
1.3332 +#127 := (= f1 #46)
1.3333 +#146 := (not #127)
1.3334 +#337 := (or #146 #189)
1.3335 +#201 := (iff #127 #189)
1.3336 +#137 := (and #131 #134)
1.3337 +#147 := (iff #137 #146)
1.3338 +#204 := (iff #147 #201)
1.3339 +#196 := (iff #189 #127)
1.3340 +#202 := (iff #196 #201)
1.3341 +#203 := [rewrite]: #202
1.3342 +#199 := (iff #147 #196)
1.3343 +#193 := (iff #190 #146)
1.3344 +#197 := (iff #193 #196)
1.3345 +#198 := [rewrite]: #197
1.3346 +#194 := (iff #147 #193)
1.3347 +#191 := (iff #137 #190)
1.3348 +#192 := [rewrite]: #191
1.3349 +#195 := [monotonicity #192]: #194
1.3350 +#200 := [trans #195 #198]: #199
1.3351 +#205 := [trans #200 #203]: #204
1.3352 +#51 := (= #50 f1)
1.3353 +#49 := (= #48 f1)
1.3354 +#52 := (and #49 #51)
1.3355 +#47 := (= #46 f1)
1.3356 +#53 := (iff #47 #52)
1.3357 +#54 := (not #53)
1.3358 +#150 := (iff #54 #147)
1.3359 +#140 := (iff #127 #137)
1.3360 +#143 := (not #140)
1.3361 +#148 := (iff #143 #147)
1.3362 +#149 := [rewrite]: #148
1.3363 +#144 := (iff #54 #143)
1.3364 +#141 := (iff #53 #140)
1.3365 +#138 := (iff #52 #137)
1.3366 +#135 := (iff #51 #134)
1.3367 +#136 := [rewrite]: #135
1.3368 +#132 := (iff #49 #131)
1.3369 +#133 := [rewrite]: #132
1.3370 +#139 := [monotonicity #133 #136]: #138
1.3371 +#129 := (iff #47 #127)
1.3372 +#130 := [rewrite]: #129
1.3373 +#142 := [monotonicity #130 #139]: #141
1.3374 +#145 := [monotonicity #142]: #144
1.3375 +#151 := [trans #145 #149]: #150
1.3376 +#126 := [asserted]: #54
1.3377 +#154 := [mp #126 #151]: #147
1.3378 +#206 := [mp #154 #205]: #201
1.3379 +#344 := (not #201)
1.3380 +#354 := (or #146 #189 #344)
1.3381 +#358 := [def-axiom]: #354
1.3382 +#674 := [unit-resolution #358 #206]: #337
1.3383 +#463 := [unit-resolution #674 #331]: #146
1.3384 +#330 := (or #127 #189)
1.3385 +#676 := (iff #127 #190)
1.3386 +#22 := (:var 0 S3)
1.3387 +#20 := (:var 1 S3)
1.3388 +#34 := (f7 f9 #20)
1.3389 +#35 := (f6 #34 #22)
1.3390 +#18 := (:var 2 S2)
1.3391 +#36 := (f3 #18 #35)
1.3392 +#703 := (pattern #36)
1.3393 +#28 := (f3 #18 #22)
1.3394 +#100 := (= f1 #28)
1.3395 +#179 := (not #100)
1.3396 +#26 := (f3 #18 #20)
1.3397 +#97 := (= f1 #26)
1.3398 +#178 := (not #97)
1.3399 +#162 := (or #178 #179)
1.3400 +#163 := (not #162)
1.3401 +#113 := (= f1 #36)
1.3402 +#180 := (iff #113 #163)
1.3403 +#704 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #703) #180)
1.3404 +#183 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #180)
1.3405 +#707 := (iff #183 #704)
1.3406 +#705 := (iff #180 #180)
1.3407 +#706 := [refl]: #705
1.3408 +#708 := [quant-intro #706]: #707
1.3409 +#117 := (and #97 #100)
1.3410 +#120 := (iff #113 #117)
1.3411 +#123 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #120)
1.3412 +#184 := (iff #123 #183)
1.3413 +#181 := (iff #120 #180)
1.3414 +#164 := (iff #117 #163)
1.3415 +#165 := [rewrite]: #164
1.3416 +#182 := [monotonicity #165]: #181
1.3417 +#185 := [quant-intro #182]: #184
1.3418 +#160 := (~ #123 #123)
1.3419 +#175 := (~ #120 #120)
1.3420 +#176 := [refl]: #175
1.3421 +#161 := [nnf-pos #176]: #160
1.3422 +#29 := (= #28 f1)
1.3423 +#27 := (= #26 f1)
1.3424 +#38 := (and #27 #29)
1.3425 +#37 := (= #36 f1)
1.3426 +#39 := (iff #37 #38)
1.3427 +#40 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #39)
1.3428 +#124 := (iff #40 #123)
1.3429 +#121 := (iff #39 #120)
1.3430 +#118 := (iff #38 #117)
1.3431 +#101 := (iff #29 #100)
1.3432 +#102 := [rewrite]: #101
1.3433 +#98 := (iff #27 #97)
1.3434 +#99 := [rewrite]: #98
1.3435 +#119 := [monotonicity #99 #102]: #118
1.3436 +#115 := (iff #37 #113)
1.3437 +#116 := [rewrite]: #115
1.3438 +#122 := [monotonicity #116 #119]: #121
1.3439 +#125 := [quant-intro #122]: #124
1.3440 +#112 := [asserted]: #40
1.3441 +#128 := [mp #112 #125]: #123
1.3442 +#177 := [mp~ #128 #161]: #123
1.3443 +#186 := [mp #177 #185]: #183
1.3444 +#709 := [mp #186 #708]: #704
1.3445 +#670 := (not #704)
1.3446 +#342 := (or #670 #676)
1.3447 +#343 := [quant-inst #41 #42 #44]: #342
1.3448 +#672 := [unit-resolution #343 #709]: #676
1.3449 +#677 := (not #676)
1.3450 +#678 := (or #677 #127 #189)
1.3451 +#679 := [def-axiom]: #678
1.3452 +#673 := [unit-resolution #679 #672]: #330
1.3453 +#314 := [unit-resolution #673 #463 #331]: false
1.3454 +#657 := [lemma #314]: #189
1.3455 +#284 := (or #127 #190)
1.3456 +#355 := (or #127 #190 #344)
1.3457 +#356 := [def-axiom]: #355
1.3458 +#357 := [unit-resolution #356 #206]: #284
1.3459 +#318 := [unit-resolution #357 #657]: #127
1.3460 +#319 := (or #146 #190)
1.3461 +#680 := (or #677 #146 #190)
1.3462 +#675 := [def-axiom]: #680
1.3463 +#320 := [unit-resolution #675 #672]: #319
1.3464 +[unit-resolution #320 #318 #657]: false
1.3465 +unsat
1.3466 +1adc4d295cebee376081ce9f5a9d0e96c2943423 149 0
1.3467 +#2 := false
1.3468 +decl f3 :: (-> S2 S3 S1)
1.3469 +decl f4 :: S3
1.3470 +#9 := f4
1.3471 +decl f10 :: S2
1.3472 +#41 := f10
1.3473 +#227 := (f3 f10 f4)
1.3474 +decl f1 :: S1
1.3475 +#4 := f1
1.3476 +#314 := (= f1 #227)
1.3477 +#228 := (not #314)
1.3478 +decl f11 :: S3
1.3479 +#42 := f11
1.3480 +#315 := (f3 f10 f11)
1.3481 +#229 := (= f1 #315)
1.3482 +#316 := (not #229)
1.3483 +#307 := (or #316 #228)
1.3484 +#318 := (not #307)
1.3485 +decl f6 :: (-> S4 S3 S3)
1.3486 +decl f7 :: (-> S5 S3 S4)
1.3487 +decl f9 :: S5
1.3488 +#33 := f9
1.3489 +#43 := (f7 f9 f11)
1.3490 +#44 := (f6 #43 f4)
1.3491 +#45 := (f3 f10 #44)
1.3492 +#121 := (= f1 #45)
1.3493 +#319 := (iff #121 #318)
1.3494 +#22 := (:var 0 S3)
1.3495 +#20 := (:var 1 S3)
1.3496 +#34 := (f7 f9 #20)
1.3497 +#35 := (f6 #34 #22)
1.3498 +#18 := (:var 2 S2)
1.3499 +#36 := (f3 #18 #35)
1.3500 +#666 := (pattern #36)
1.3501 +#28 := (f3 #18 #22)
1.3502 +#94 := (= f1 #28)
1.3503 +#162 := (not #94)
1.3504 +#26 := (f3 #18 #20)
1.3505 +#91 := (= f1 #26)
1.3506 +#161 := (not #91)
1.3507 +#145 := (or #161 #162)
1.3508 +#146 := (not #145)
1.3509 +#107 := (= f1 #36)
1.3510 +#163 := (iff #107 #146)
1.3511 +#667 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #666) #163)
1.3512 +#166 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #163)
1.3513 +#670 := (iff #166 #667)
1.3514 +#668 := (iff #163 #163)
1.3515 +#669 := [refl]: #668
1.3516 +#671 := [quant-intro #669]: #670
1.3517 +#111 := (and #91 #94)
1.3518 +#114 := (iff #107 #111)
1.3519 +#117 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #114)
1.3520 +#167 := (iff #117 #166)
1.3521 +#164 := (iff #114 #163)
1.3522 +#147 := (iff #111 #146)
1.3523 +#148 := [rewrite]: #147
1.3524 +#165 := [monotonicity #148]: #164
1.3525 +#168 := [quant-intro #165]: #167
1.3526 +#143 := (~ #117 #117)
1.3527 +#158 := (~ #114 #114)
1.3528 +#159 := [refl]: #158
1.3529 +#144 := [nnf-pos #159]: #143
1.3530 +#29 := (= #28 f1)
1.3531 +#27 := (= #26 f1)
1.3532 +#38 := (and #27 #29)
1.3533 +#37 := (= #36 f1)
1.3534 +#39 := (iff #37 #38)
1.3535 +#40 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #39)
1.3536 +#118 := (iff #40 #117)
1.3537 +#115 := (iff #39 #114)
1.3538 +#112 := (iff #38 #111)
1.3539 +#95 := (iff #29 #94)
1.3540 +#96 := [rewrite]: #95
1.3541 +#92 := (iff #27 #91)
1.3542 +#93 := [rewrite]: #92
1.3543 +#113 := [monotonicity #93 #96]: #112
1.3544 +#109 := (iff #37 #107)
1.3545 +#110 := [rewrite]: #109
1.3546 +#116 := [monotonicity #110 #113]: #115
1.3547 +#119 := [quant-intro #116]: #118
1.3548 +#106 := [asserted]: #40
1.3549 +#122 := [mp #106 #119]: #117
1.3550 +#160 := [mp~ #122 #144]: #117
1.3551 +#169 := [mp #160 #168]: #166
1.3552 +#672 := [mp #169 #671]: #667
1.3553 +#317 := (not #667)
1.3554 +#321 := (or #317 #319)
1.3555 +#300 := [quant-inst #41 #42 #9]: #321
1.3556 +#247 := [unit-resolution #300 #672]: #319
1.3557 +#306 := (not #319)
1.3558 +#320 := (or #306 #318)
1.3559 +#46 := (= #45 f1)
1.3560 +#47 := (not #46)
1.3561 +#48 := (not #47)
1.3562 +#133 := (iff #48 #121)
1.3563 +#125 := (not #121)
1.3564 +#128 := (not #125)
1.3565 +#131 := (iff #128 #121)
1.3566 +#132 := [rewrite]: #131
1.3567 +#129 := (iff #48 #128)
1.3568 +#126 := (iff #47 #125)
1.3569 +#123 := (iff #46 #121)
1.3570 +#124 := [rewrite]: #123
1.3571 +#127 := [monotonicity #124]: #126
1.3572 +#130 := [monotonicity #127]: #129
1.3573 +#134 := [trans #130 #132]: #133
1.3574 +#120 := [asserted]: #48
1.3575 +#137 := [mp #120 #134]: #121
1.3576 +#642 := (or #306 #125 #318)
1.3577 +#643 := [def-axiom]: #642
1.3578 +#636 := [unit-resolution #643 #137]: #320
1.3579 +#277 := [unit-resolution #636 #247]: #318
1.3580 +#294 := (or #307 #314)
1.3581 +#426 := [def-axiom]: #294
1.3582 +#620 := [unit-resolution #426 #277]: #314
1.3583 +#8 := (:var 0 S2)
1.3584 +#10 := (f3 #8 f4)
1.3585 +#645 := (pattern #10)
1.3586 +#69 := (= f1 #10)
1.3587 +#72 := (not #69)
1.3588 +#646 := (forall (vars (?v0 S2)) (:pat #645) #72)
1.3589 +#75 := (forall (vars (?v0 S2)) #72)
1.3590 +#649 := (iff #75 #646)
1.3591 +#647 := (iff #72 #72)
1.3592 +#648 := [refl]: #647
1.3593 +#650 := [quant-intro #648]: #649
1.3594 +#151 := (~ #75 #75)
1.3595 +#149 := (~ #72 #72)
1.3596 +#150 := [refl]: #149
1.3597 +#152 := [nnf-pos #150]: #151
1.3598 +#11 := (= #10 f1)
1.3599 +#12 := (not #11)
1.3600 +#13 := (forall (vars (?v0 S2)) #12)
1.3601 +#76 := (iff #13 #75)
1.3602 +#73 := (iff #12 #72)
1.3603 +#70 := (iff #11 #69)
1.3604 +#71 := [rewrite]: #70
1.3605 +#74 := [monotonicity #71]: #73
1.3606 +#77 := [quant-intro #74]: #76
1.3607 +#68 := [asserted]: #13
1.3608 +#80 := [mp #68 #77]: #75
1.3609 +#136 := [mp~ #80 #152]: #75
1.3610 +#651 := [mp #136 #650]: #646
1.3611 +#297 := (not #646)
1.3612 +#635 := (or #297 #228)
1.3613 +#293 := [quant-inst #41]: #635
1.3614 +[unit-resolution #293 #651 #620]: false
1.3615 +unsat
1.3616 +27fbc35929f013c0b43884a593f3f377821cad64 173 0
1.3617 +#2 := false
1.3618 +decl f3 :: (-> S2 S3 S1)
1.3619 +decl f11 :: S3
1.3620 +#42 := f11
1.3621 +decl f10 :: S2
1.3622 +#41 := f10
1.3623 +#47 := (f3 f10 f11)
1.3624 +decl f1 :: S1
1.3625 +#4 := f1
1.3626 +#127 := (= f1 #47)
1.3627 +#323 := (not #127)
1.3628 +decl f6 :: (-> S4 S3 S3)
1.3629 +decl f5 :: S3
1.3630 +#14 := f5
1.3631 +decl f7 :: (-> S5 S3 S4)
1.3632 +decl f9 :: S5
1.3633 +#33 := f9
1.3634 +#43 := (f7 f9 f11)
1.3635 +#44 := (f6 #43 f5)
1.3636 +#45 := (f3 f10 #44)
1.3637 +#123 := (= f1 #45)
1.3638 +#327 := (f3 f10 f5)
1.3639 +#324 := (= f1 #327)
1.3640 +#328 := (not #324)
1.3641 +#301 := [hypothesis]: #328
1.3642 +#8 := (:var 0 S2)
1.3643 +#15 := (f3 #8 f5)
1.3644 +#659 := (pattern #15)
1.3645 +#81 := (= f1 #15)
1.3646 +#660 := (forall (vars (?v0 S2)) (:pat #659) #81)
1.3647 +#85 := (forall (vars (?v0 S2)) #81)
1.3648 +#663 := (iff #85 #660)
1.3649 +#661 := (iff #81 #81)
1.3650 +#662 := [refl]: #661
1.3651 +#664 := [quant-intro #662]: #663
1.3652 +#146 := (~ #85 #85)
1.3653 +#145 := (~ #81 #81)
1.3654 +#160 := [refl]: #145
1.3655 +#147 := [nnf-pos #160]: #146
1.3656 +#16 := (= #15 f1)
1.3657 +#17 := (forall (vars (?v0 S2)) #16)
1.3658 +#86 := (iff #17 #85)
1.3659 +#83 := (iff #16 #81)
1.3660 +#84 := [rewrite]: #83
1.3661 +#87 := [quant-intro #84]: #86
1.3662 +#80 := [asserted]: #17
1.3663 +#90 := [mp #80 #87]: #85
1.3664 +#161 := [mp~ #90 #147]: #85
1.3665 +#665 := [mp #161 #664]: #660
1.3666 +#289 := (not #660)
1.3667 +#290 := (or #289 #324)
1.3668 +#291 := [quant-inst #41]: #290
1.3669 +#433 := [unit-resolution #291 #665 #301]: false
1.3670 +#629 := [lemma #433]: #324
1.3671 +#136 := (not #123)
1.3672 +#630 := [hypothesis]: #136
1.3673 +#322 := (or #127 #123)
1.3674 +#137 := (iff #127 #136)
1.3675 +#48 := (= #47 f1)
1.3676 +#46 := (= #45 f1)
1.3677 +#49 := (iff #46 #48)
1.3678 +#50 := (not #49)
1.3679 +#140 := (iff #50 #137)
1.3680 +#130 := (iff #123 #127)
1.3681 +#133 := (not #130)
1.3682 +#138 := (iff #133 #137)
1.3683 +#139 := [rewrite]: #138
1.3684 +#134 := (iff #50 #133)
1.3685 +#131 := (iff #49 #130)
1.3686 +#128 := (iff #48 #127)
1.3687 +#129 := [rewrite]: #128
1.3688 +#125 := (iff #46 #123)
1.3689 +#126 := [rewrite]: #125
1.3690 +#132 := [monotonicity #126 #129]: #131
1.3691 +#135 := [monotonicity #132]: #134
1.3692 +#141 := [trans #135 #139]: #140
1.3693 +#122 := [asserted]: #50
1.3694 +#144 := [mp #122 #141]: #137
1.3695 +#234 := (not #137)
1.3696 +#321 := (or #127 #123 #234)
1.3697 +#235 := [def-axiom]: #321
1.3698 +#236 := [unit-resolution #235 #144]: #322
1.3699 +#631 := [unit-resolution #236 #630]: #127
1.3700 +#307 := (or #323 #328)
1.3701 +#633 := (or #123 #307)
1.3702 +#644 := (not #307)
1.3703 +#646 := (iff #123 #644)
1.3704 +#22 := (:var 0 S3)
1.3705 +#20 := (:var 1 S3)
1.3706 +#34 := (f7 f9 #20)
1.3707 +#35 := (f6 #34 #22)
1.3708 +#18 := (:var 2 S2)
1.3709 +#36 := (f3 #18 #35)
1.3710 +#673 := (pattern #36)
1.3711 +#28 := (f3 #18 #22)
1.3712 +#96 := (= f1 #28)
1.3713 +#169 := (not #96)
1.3714 +#26 := (f3 #18 #20)
1.3715 +#93 := (= f1 #26)
1.3716 +#168 := (not #93)
1.3717 +#152 := (or #168 #169)
1.3718 +#153 := (not #152)
1.3719 +#109 := (= f1 #36)
1.3720 +#170 := (iff #109 #153)
1.3721 +#674 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #673) #170)
1.3722 +#173 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #170)
1.3723 +#677 := (iff #173 #674)
1.3724 +#675 := (iff #170 #170)
1.3725 +#676 := [refl]: #675
1.3726 +#678 := [quant-intro #676]: #677
1.3727 +#113 := (and #93 #96)
1.3728 +#116 := (iff #109 #113)
1.3729 +#119 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #116)
1.3730 +#174 := (iff #119 #173)
1.3731 +#171 := (iff #116 #170)
1.3732 +#154 := (iff #113 #153)
1.3733 +#155 := [rewrite]: #154
1.3734 +#172 := [monotonicity #155]: #171
1.3735 +#175 := [quant-intro #172]: #174
1.3736 +#150 := (~ #119 #119)
1.3737 +#165 := (~ #116 #116)
1.3738 +#166 := [refl]: #165
1.3739 +#151 := [nnf-pos #166]: #150
1.3740 +#29 := (= #28 f1)
1.3741 +#27 := (= #26 f1)
1.3742 +#38 := (and #27 #29)
1.3743 +#37 := (= #36 f1)
1.3744 +#39 := (iff #37 #38)
1.3745 +#40 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #39)
1.3746 +#120 := (iff #40 #119)
1.3747 +#117 := (iff #39 #116)
1.3748 +#114 := (iff #38 #113)
1.3749 +#97 := (iff #29 #96)
1.3750 +#98 := [rewrite]: #97
1.3751 +#94 := (iff #27 #93)
1.3752 +#95 := [rewrite]: #94
1.3753 +#115 := [monotonicity #95 #98]: #114
1.3754 +#111 := (iff #37 #109)
1.3755 +#112 := [rewrite]: #111
1.3756 +#118 := [monotonicity #112 #115]: #117
1.3757 +#121 := [quant-intro #118]: #120
1.3758 +#108 := [asserted]: #40
1.3759 +#124 := [mp #108 #121]: #119
1.3760 +#167 := [mp~ #124 #151]: #119
1.3761 +#176 := [mp #167 #175]: #173
1.3762 +#679 := [mp #176 #678]: #674
1.3763 +#640 := (not #674)
1.3764 +#312 := (or #640 #646)
1.3765 +#313 := [quant-inst #41 #42 #14]: #312
1.3766 +#632 := [unit-resolution #313 #679]: #646
1.3767 +#641 := (not #646)
1.3768 +#299 := (or #641 #123 #307)
1.3769 +#304 := [def-axiom]: #299
1.3770 +#628 := [unit-resolution #304 #632]: #633
1.3771 +#634 := [unit-resolution #628 #630]: #307
1.3772 +#645 := (or #644 #323 #328)
1.3773 +#651 := [def-axiom]: #645
1.3774 +#270 := [unit-resolution #651 #634 #631 #629]: false
1.3775 +#635 := [lemma #270]: #123
1.3776 +#326 := (or #323 #136)
1.3777 +#314 := (or #323 #136 #234)
1.3778 +#325 := [def-axiom]: #314
1.3779 +#254 := [unit-resolution #325 #144]: #326
1.3780 +#637 := [unit-resolution #254 #635]: #323
1.3781 +#275 := (or #136 #644)
1.3782 +#642 := (or #641 #136 #644)
1.3783 +#300 := [def-axiom]: #642
1.3784 +#276 := [unit-resolution #300 #632]: #275
1.3785 +#638 := [unit-resolution #276 #635]: #644
1.3786 +#647 := (or #307 #127)
1.3787 +#648 := [def-axiom]: #647
1.3788 +[unit-resolution #648 #638 #637]: false
1.3789 +unsat
1.3790 +fa1e213c15b8e9288bf16d2dc4bd96e3c7fb5c7e 173 0
1.3791 +#2 := false
1.3792 +decl f3 :: (-> S2 S3 S1)
1.3793 +decl f6 :: (-> S4 S3 S3)
1.3794 +decl f11 :: S3
1.3795 +#42 := f11
1.3796 +decl f7 :: (-> S5 S3 S4)
1.3797 +decl f12 :: S3
1.3798 +#44 := f12
1.3799 +decl f9 :: S5
1.3800 +#33 := f9
1.3801 +#48 := (f7 f9 f12)
1.3802 +#49 := (f6 #48 f11)
1.3803 +decl f10 :: S2
1.3804 +#41 := f10
1.3805 +#50 := (f3 f10 #49)
1.3806 +decl f1 :: S1
1.3807 +#4 := f1
1.3808 +#130 := (= f1 #50)
1.3809 +#326 := (not #130)
1.3810 +#43 := (f7 f9 f11)
1.3811 +#45 := (f6 #43 f12)
1.3812 +#46 := (f3 f10 #45)
1.3813 +#126 := (= f1 #46)
1.3814 +#139 := (not #126)
1.3815 +#628 := [hypothesis]: #139
1.3816 +#325 := (or #130 #126)
1.3817 +#140 := (iff #130 #139)
1.3818 +#51 := (= #50 f1)
1.3819 +#47 := (= #46 f1)
1.3820 +#52 := (iff #47 #51)
1.3821 +#53 := (not #52)
1.3822 +#143 := (iff #53 #140)
1.3823 +#133 := (iff #126 #130)
1.3824 +#136 := (not #133)
1.3825 +#141 := (iff #136 #140)
1.3826 +#142 := [rewrite]: #141
1.3827 +#137 := (iff #53 #136)
1.3828 +#134 := (iff #52 #133)
1.3829 +#131 := (iff #51 #130)
1.3830 +#132 := [rewrite]: #131
1.3831 +#128 := (iff #47 #126)
1.3832 +#129 := [rewrite]: #128
1.3833 +#135 := [monotonicity #129 #132]: #134
1.3834 +#138 := [monotonicity #135]: #137
1.3835 +#144 := [trans #138 #142]: #143
1.3836 +#125 := [asserted]: #53
1.3837 +#147 := [mp #125 #144]: #140
1.3838 +#237 := (not #140)
1.3839 +#324 := (or #130 #126 #237)
1.3840 +#238 := [def-axiom]: #324
1.3841 +#239 := [unit-resolution #238 #147]: #325
1.3842 +#629 := [unit-resolution #239 #628]: #130
1.3843 +#310 := (f3 f10 f12)
1.3844 +#647 := (= f1 #310)
1.3845 +#649 := (not #647)
1.3846 +#330 := (f3 f10 f11)
1.3847 +#327 := (= f1 #330)
1.3848 +#331 := (not #327)
1.3849 +#315 := (or #331 #649)
1.3850 +#626 := (or #126 #315)
1.3851 +#651 := (not #315)
1.3852 +#642 := (iff #126 #651)
1.3853 +#22 := (:var 0 S3)
1.3854 +#20 := (:var 1 S3)
1.3855 +#34 := (f7 f9 #20)
1.3856 +#35 := (f6 #34 #22)
1.3857 +#18 := (:var 2 S2)
1.3858 +#36 := (f3 #18 #35)
1.3859 +#676 := (pattern #36)
1.3860 +#28 := (f3 #18 #22)
1.3861 +#99 := (= f1 #28)
1.3862 +#172 := (not #99)
1.3863 +#26 := (f3 #18 #20)
1.3864 +#96 := (= f1 #26)
1.3865 +#171 := (not #96)
1.3866 +#155 := (or #171 #172)
1.3867 +#156 := (not #155)
1.3868 +#112 := (= f1 #36)
1.3869 +#173 := (iff #112 #156)
1.3870 +#677 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #676) #173)
1.3871 +#176 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #173)
1.3872 +#680 := (iff #176 #677)
1.3873 +#678 := (iff #173 #173)
1.3874 +#679 := [refl]: #678
1.3875 +#681 := [quant-intro #679]: #680
1.3876 +#116 := (and #96 #99)
1.3877 +#119 := (iff #112 #116)
1.3878 +#122 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #119)
1.3879 +#177 := (iff #122 #176)
1.3880 +#174 := (iff #119 #173)
1.3881 +#157 := (iff #116 #156)
1.3882 +#158 := [rewrite]: #157
1.3883 +#175 := [monotonicity #158]: #174
1.3884 +#178 := [quant-intro #175]: #177
1.3885 +#153 := (~ #122 #122)
1.3886 +#168 := (~ #119 #119)
1.3887 +#169 := [refl]: #168
1.3888 +#154 := [nnf-pos #169]: #153
1.3889 +#29 := (= #28 f1)
1.3890 +#27 := (= #26 f1)
1.3891 +#38 := (and #27 #29)
1.3892 +#37 := (= #36 f1)
1.3893 +#39 := (iff #37 #38)
1.3894 +#40 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #39)
1.3895 +#123 := (iff #40 #122)
1.3896 +#120 := (iff #39 #119)
1.3897 +#117 := (iff #38 #116)
1.3898 +#100 := (iff #29 #99)
1.3899 +#101 := [rewrite]: #100
1.3900 +#97 := (iff #27 #96)
1.3901 +#98 := [rewrite]: #97
1.3902 +#118 := [monotonicity #98 #101]: #117
1.3903 +#114 := (iff #37 #112)
1.3904 +#115 := [rewrite]: #114
1.3905 +#121 := [monotonicity #115 #118]: #120
1.3906 +#124 := [quant-intro #121]: #123
1.3907 +#111 := [asserted]: #40
1.3908 +#127 := [mp #111 #124]: #122
1.3909 +#170 := [mp~ #127 #154]: #122
1.3910 +#179 := [mp #170 #178]: #176
1.3911 +#682 := [mp #179 #681]: #677
1.3912 +#302 := (not #677)
1.3913 +#335 := (or #302 #642)
1.3914 +#351 := [quant-inst #41 #42 #44]: #335
1.3915 +#622 := [unit-resolution #351 #682]: #642
1.3916 +#352 := (not #642)
1.3917 +#353 := (or #352 #126 #315)
1.3918 +#339 := [def-axiom]: #353
1.3919 +#623 := [unit-resolution #339 #622]: #626
1.3920 +#627 := [unit-resolution #623 #628]: #315
1.3921 +#337 := (or #326 #651)
1.3922 +#648 := (iff #130 #651)
1.3923 +#307 := (or #302 #648)
1.3924 +#304 := (or #649 #331)
1.3925 +#436 := (not #304)
1.3926 +#643 := (iff #130 #436)
1.3927 +#645 := (or #302 #643)
1.3928 +#646 := (iff #645 #307)
1.3929 +#630 := (iff #307 #307)
1.3930 +#291 := [rewrite]: #630
1.3931 +#654 := (iff #643 #648)
1.3932 +#652 := (iff #436 #651)
1.3933 +#316 := (iff #304 #315)
1.3934 +#650 := [rewrite]: #316
1.3935 +#653 := [monotonicity #650]: #652
1.3936 +#644 := [monotonicity #653]: #654
1.3937 +#287 := [monotonicity #644]: #646
1.3938 +#292 := [trans #287 #291]: #646
1.3939 +#303 := [quant-inst #41 #44 #42]: #645
1.3940 +#293 := [mp #303 #292]: #307
1.3941 +#336 := [unit-resolution #293 #682]: #648
1.3942 +#631 := (not #648)
1.3943 +#638 := (or #631 #326 #651)
1.3944 +#640 := [def-axiom]: #638
1.3945 +#338 := [unit-resolution #640 #336]: #337
1.3946 +#340 := [unit-resolution #338 #627 #629]: false
1.3947 +#618 := [lemma #340]: #126
1.3948 +#329 := (or #326 #139)
1.3949 +#317 := (or #326 #139 #237)
1.3950 +#328 := [def-axiom]: #317
1.3951 +#257 := [unit-resolution #328 #147]: #329
1.3952 +#619 := [unit-resolution #257 #618]: #326
1.3953 +#332 := (or #139 #651)
1.3954 +#354 := (or #352 #139 #651)
1.3955 +#245 := [def-axiom]: #354
1.3956 +#616 := [unit-resolution #245 #622]: #332
1.3957 +#620 := [unit-resolution #616 #618]: #651
1.3958 +#617 := (or #130 #315)
1.3959 +#637 := (or #631 #130 #315)
1.3960 +#273 := [def-axiom]: #637
1.3961 +#621 := [unit-resolution #273 #336]: #617
1.3962 +[unit-resolution #621 #620 #619]: false
1.3963 +unsat
1.3964 +8424513290e59440c92fec106021e2354c2f6a1c 149 0
1.3965 +#2 := false
1.3966 +decl f3 :: (-> S2 S3 S1)
1.3967 +decl f6 :: (-> S4 S3 S3)
1.3968 +decl f11 :: S3
1.3969 +#42 := f11
1.3970 +decl f7 :: (-> S5 S3 S4)
1.3971 +decl f9 :: S5
1.3972 +#33 := f9
1.3973 +#43 := (f7 f9 f11)
1.3974 +#44 := (f6 #43 f11)
1.3975 +decl f10 :: S2
1.3976 +#41 := f10
1.3977 +#45 := (f3 f10 #44)
1.3978 +decl f1 :: S1
1.3979 +#4 := f1
1.3980 +#123 := (= f1 #45)
1.3981 +#136 := (not #123)
1.3982 +#632 := [hypothesis]: #136
1.3983 +#47 := (f3 f10 f11)
1.3984 +#127 := (= f1 #47)
1.3985 +#322 := (or #127 #123)
1.3986 +#137 := (iff #127 #136)
1.3987 +#48 := (= #47 f1)
1.3988 +#46 := (= #45 f1)
1.3989 +#49 := (iff #46 #48)
1.3990 +#50 := (not #49)
1.3991 +#140 := (iff #50 #137)
1.3992 +#130 := (iff #123 #127)
1.3993 +#133 := (not #130)
1.3994 +#138 := (iff #133 #137)
1.3995 +#139 := [rewrite]: #138
1.3996 +#134 := (iff #50 #133)
1.3997 +#131 := (iff #49 #130)
1.3998 +#128 := (iff #48 #127)
1.3999 +#129 := [rewrite]: #128
1.4000 +#125 := (iff #46 #123)
1.4001 +#126 := [rewrite]: #125
1.4002 +#132 := [monotonicity #126 #129]: #131
1.4003 +#135 := [monotonicity #132]: #134
1.4004 +#141 := [trans #135 #139]: #140
1.4005 +#122 := [asserted]: #50
1.4006 +#144 := [mp #122 #141]: #137
1.4007 +#234 := (not #137)
1.4008 +#321 := (or #127 #123 #234)
1.4009 +#235 := [def-axiom]: #321
1.4010 +#236 := [unit-resolution #235 #144]: #322
1.4011 +#633 := [unit-resolution #236 #632]: #127
1.4012 +#323 := (not #127)
1.4013 +#634 := (or #123 #323)
1.4014 +#22 := (:var 0 S3)
1.4015 +#20 := (:var 1 S3)
1.4016 +#34 := (f7 f9 #20)
1.4017 +#35 := (f6 #34 #22)
1.4018 +#18 := (:var 2 S2)
1.4019 +#36 := (f3 #18 #35)
1.4020 +#673 := (pattern #36)
1.4021 +#28 := (f3 #18 #22)
1.4022 +#96 := (= f1 #28)
1.4023 +#169 := (not #96)
1.4024 +#26 := (f3 #18 #20)
1.4025 +#93 := (= f1 #26)
1.4026 +#168 := (not #93)
1.4027 +#152 := (or #168 #169)
1.4028 +#153 := (not #152)
1.4029 +#109 := (= f1 #36)
1.4030 +#170 := (iff #109 #153)
1.4031 +#674 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #673) #170)
1.4032 +#173 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #170)
1.4033 +#677 := (iff #173 #674)
1.4034 +#675 := (iff #170 #170)
1.4035 +#676 := [refl]: #675
1.4036 +#678 := [quant-intro #676]: #677
1.4037 +#113 := (and #93 #96)
1.4038 +#116 := (iff #109 #113)
1.4039 +#119 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #116)
1.4040 +#174 := (iff #119 #173)
1.4041 +#171 := (iff #116 #170)
1.4042 +#154 := (iff #113 #153)
1.4043 +#155 := [rewrite]: #154
1.4044 +#172 := [monotonicity #155]: #171
1.4045 +#175 := [quant-intro #172]: #174
1.4046 +#150 := (~ #119 #119)
1.4047 +#165 := (~ #116 #116)
1.4048 +#166 := [refl]: #165
1.4049 +#151 := [nnf-pos #166]: #150
1.4050 +#29 := (= #28 f1)
1.4051 +#27 := (= #26 f1)
1.4052 +#38 := (and #27 #29)
1.4053 +#37 := (= #36 f1)
1.4054 +#39 := (iff #37 #38)
1.4055 +#40 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #39)
1.4056 +#120 := (iff #40 #119)
1.4057 +#117 := (iff #39 #116)
1.4058 +#114 := (iff #38 #113)
1.4059 +#97 := (iff #29 #96)
1.4060 +#98 := [rewrite]: #97
1.4061 +#94 := (iff #27 #93)
1.4062 +#95 := [rewrite]: #94
1.4063 +#115 := [monotonicity #95 #98]: #114
1.4064 +#111 := (iff #37 #109)
1.4065 +#112 := [rewrite]: #111
1.4066 +#118 := [monotonicity #112 #115]: #117
1.4067 +#121 := [quant-intro #118]: #120
1.4068 +#108 := [asserted]: #40
1.4069 +#124 := [mp #108 #121]: #119
1.4070 +#167 := [mp~ #124 #151]: #119
1.4071 +#176 := [mp #167 #175]: #173
1.4072 +#679 := [mp #176 #678]: #674
1.4073 +#650 := (not #674)
1.4074 +#645 := (or #650 #130)
1.4075 +#327 := (or #323 #323)
1.4076 +#324 := (not #327)
1.4077 +#328 := (iff #123 #324)
1.4078 +#651 := (or #650 #328)
1.4079 +#299 := (iff #651 #645)
1.4080 +#642 := (iff #645 #645)
1.4081 +#300 := [rewrite]: #642
1.4082 +#648 := (iff #328 #130)
1.4083 +#313 := (iff #324 #127)
1.4084 +#646 := (not #323)
1.4085 +#640 := (iff #646 #127)
1.4086 +#312 := [rewrite]: #640
1.4087 +#301 := (iff #324 #646)
1.4088 +#307 := (iff #327 #323)
1.4089 +#644 := [rewrite]: #307
1.4090 +#433 := [monotonicity #644]: #301
1.4091 +#647 := [trans #433 #312]: #313
1.4092 +#649 := [monotonicity #647]: #648
1.4093 +#304 := [monotonicity #649]: #299
1.4094 +#643 := [trans #304 #300]: #299
1.4095 +#641 := [quant-inst #41 #42 #42]: #651
1.4096 +#284 := [mp #641 #643]: #645
1.4097 +#628 := [unit-resolution #284 #679]: #130
1.4098 +#627 := (or #133 #123 #323)
1.4099 +#288 := [def-axiom]: #627
1.4100 +#270 := [unit-resolution #288 #628]: #634
1.4101 +#635 := [unit-resolution #270 #633 #632]: false
1.4102 +#637 := [lemma #635]: #123
1.4103 +#326 := (or #323 #136)
1.4104 +#314 := (or #323 #136 #234)
1.4105 +#325 := [def-axiom]: #314
1.4106 +#254 := [unit-resolution #325 #144]: #326
1.4107 +#275 := [unit-resolution #254 #637]: #323
1.4108 +#276 := (or #136 #127)
1.4109 +#289 := (or #133 #136 #127)
1.4110 +#290 := [def-axiom]: #289
1.4111 +#638 := [unit-resolution #290 #628]: #276
1.4112 +[unit-resolution #638 #275 #637]: false
1.4113 +unsat
1.4114 +5973328496eea1e33493c38f9af9d86965f67ad9 287 0
1.4115 +#2 := false
1.4116 +decl f3 :: (-> S2 S3 S1)
1.4117 +decl f6 :: (-> S4 S3 S3)
1.4118 +decl f12 :: S3
1.4119 +#44 := f12
1.4120 +decl f7 :: (-> S5 S3 S4)
1.4121 +decl f11 :: S3
1.4122 +#42 := f11
1.4123 +decl f9 :: S5
1.4124 +#33 := f9
1.4125 +#43 := (f7 f9 f11)
1.4126 +#51 := (f6 #43 f12)
1.4127 +decl f10 :: S2
1.4128 +#41 := f10
1.4129 +#314 := (f3 f10 #51)
1.4130 +decl f1 :: S1
1.4131 +#4 := f1
1.4132 +#651 := (= f1 #314)
1.4133 +#249 := (f3 f10 f12)
1.4134 +#628 := (= f1 #249)
1.4135 +#625 := (not #628)
1.4136 +#339 := (f3 f10 f11)
1.4137 +#355 := (= f1 #339)
1.4138 +#356 := (not #355)
1.4139 +#614 := (or #356 #625)
1.4140 +#615 := (not #614)
1.4141 +#611 := (iff #615 #651)
1.4142 +#582 := (not #611)
1.4143 +decl f13 :: S3
1.4144 +#46 := f13
1.4145 +#334 := (f3 f10 f13)
1.4146 +#331 := (= f1 #334)
1.4147 +#335 := (not #331)
1.4148 +#484 := (or #335 #625)
1.4149 +#493 := (not #484)
1.4150 +#45 := (f7 f9 f12)
1.4151 +#47 := (f6 #45 f13)
1.4152 +#646 := (f3 f10 #47)
1.4153 +#632 := (= f1 #646)
1.4154 +#494 := (iff #493 #632)
1.4155 +#587 := (not #494)
1.4156 +#567 := [hypothesis]: #587
1.4157 +#22 := (:var 0 S3)
1.4158 +#20 := (:var 1 S3)
1.4159 +#34 := (f7 f9 #20)
1.4160 +#35 := (f6 #34 #22)
1.4161 +#18 := (:var 2 S2)
1.4162 +#36 := (f3 #18 #35)
1.4163 +#680 := (pattern #36)
1.4164 +#28 := (f3 #18 #22)
1.4165 +#103 := (= f1 #28)
1.4166 +#176 := (not #103)
1.4167 +#26 := (f3 #18 #20)
1.4168 +#100 := (= f1 #26)
1.4169 +#175 := (not #100)
1.4170 +#159 := (or #175 #176)
1.4171 +#160 := (not #159)
1.4172 +#116 := (= f1 #36)
1.4173 +#177 := (iff #116 #160)
1.4174 +#681 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #680) #177)
1.4175 +#180 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #177)
1.4176 +#684 := (iff #180 #681)
1.4177 +#682 := (iff #177 #177)
1.4178 +#683 := [refl]: #682
1.4179 +#685 := [quant-intro #683]: #684
1.4180 +#120 := (and #100 #103)
1.4181 +#123 := (iff #116 #120)
1.4182 +#126 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #123)
1.4183 +#181 := (iff #126 #180)
1.4184 +#178 := (iff #123 #177)
1.4185 +#161 := (iff #120 #160)
1.4186 +#162 := [rewrite]: #161
1.4187 +#179 := [monotonicity #162]: #178
1.4188 +#182 := [quant-intro #179]: #181
1.4189 +#157 := (~ #126 #126)
1.4190 +#172 := (~ #123 #123)
1.4191 +#173 := [refl]: #172
1.4192 +#158 := [nnf-pos #173]: #157
1.4193 +#29 := (= #28 f1)
1.4194 +#27 := (= #26 f1)
1.4195 +#38 := (and #27 #29)
1.4196 +#37 := (= #36 f1)
1.4197 +#39 := (iff #37 #38)
1.4198 +#40 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #39)
1.4199 +#127 := (iff #40 #126)
1.4200 +#124 := (iff #39 #123)
1.4201 +#121 := (iff #38 #120)
1.4202 +#104 := (iff #29 #103)
1.4203 +#105 := [rewrite]: #104
1.4204 +#101 := (iff #27 #100)
1.4205 +#102 := [rewrite]: #101
1.4206 +#122 := [monotonicity #102 #105]: #121
1.4207 +#118 := (iff #37 #116)
1.4208 +#119 := [rewrite]: #118
1.4209 +#125 := [monotonicity #119 #122]: #124
1.4210 +#128 := [quant-intro #125]: #127
1.4211 +#115 := [asserted]: #40
1.4212 +#131 := [mp #115 #128]: #126
1.4213 +#174 := [mp~ #131 #158]: #126
1.4214 +#183 := [mp #174 #182]: #180
1.4215 +#686 := [mp #183 #685]: #681
1.4216 +#306 := (not #681)
1.4217 +#498 := (or #306 #494)
1.4218 +#600 := (or #625 #335)
1.4219 +#482 := (not #600)
1.4220 +#483 := (iff #632 #482)
1.4221 +#499 := (or #306 #483)
1.4222 +#593 := (iff #499 #498)
1.4223 +#594 := (iff #498 #498)
1.4224 +#581 := [rewrite]: #594
1.4225 +#496 := (iff #483 #494)
1.4226 +#592 := (iff #632 #493)
1.4227 +#495 := (iff #592 #494)
1.4228 +#488 := [rewrite]: #495
1.4229 +#477 := (iff #483 #592)
1.4230 +#588 := (iff #482 #493)
1.4231 +#443 := (iff #600 #484)
1.4232 +#591 := [rewrite]: #443
1.4233 +#589 := [monotonicity #591]: #588
1.4234 +#492 := [monotonicity #589]: #477
1.4235 +#497 := [trans #492 #488]: #496
1.4236 +#590 := [monotonicity #497]: #593
1.4237 +#583 := [trans #590 #581]: #593
1.4238 +#500 := [quant-inst #41 #44 #46]: #499
1.4239 +#575 := [mp #500 #583]: #498
1.4240 +#568 := [unit-resolution #575 #686 #567]: false
1.4241 +#569 := [lemma #568]: #494
1.4242 +#633 := (not #632)
1.4243 +#357 := (or #356 #633)
1.4244 +#343 := (not #357)
1.4245 +#48 := (f6 #43 #47)
1.4246 +#49 := (f3 f10 #48)
1.4247 +#130 := (= f1 #49)
1.4248 +#143 := (not #130)
1.4249 +#570 := [hypothesis]: #143
1.4250 +#571 := (or #130 #357)
1.4251 +#358 := (iff #130 #343)
1.4252 +#629 := (or #306 #358)
1.4253 +#351 := [quant-inst #41 #42 #47]: #629
1.4254 +#566 := [unit-resolution #351 #686]: #358
1.4255 +#341 := (not #358)
1.4256 +#342 := (or #341 #130 #357)
1.4257 +#344 := [def-axiom]: #342
1.4258 +#557 := [unit-resolution #344 #566]: #571
1.4259 +#558 := [unit-resolution #557 #570]: #357
1.4260 +#597 := (or #306 #611)
1.4261 +#616 := (iff #651 #615)
1.4262 +#613 := (or #306 #616)
1.4263 +#618 := (iff #613 #597)
1.4264 +#461 := (iff #597 #597)
1.4265 +#462 := [rewrite]: #461
1.4266 +#612 := (iff #616 #611)
1.4267 +#617 := [rewrite]: #612
1.4268 +#460 := [monotonicity #617]: #618
1.4269 +#604 := [trans #460 #462]: #618
1.4270 +#619 := [quant-inst #41 #42 #44]: #613
1.4271 +#605 := [mp #619 #604]: #597
1.4272 +#560 := [unit-resolution #605 #686]: #611
1.4273 +#546 := (or #582 #615)
1.4274 +#653 := (not #651)
1.4275 +#319 := (or #335 #653)
1.4276 +#655 := (not #319)
1.4277 +#52 := (f7 f9 #51)
1.4278 +#53 := (f6 #52 f13)
1.4279 +#54 := (f3 f10 #53)
1.4280 +#134 := (= f1 #54)
1.4281 +#329 := (or #134 #130)
1.4282 +#144 := (iff #134 #143)
1.4283 +#55 := (= #54 f1)
1.4284 +#50 := (= #49 f1)
1.4285 +#56 := (iff #50 #55)
1.4286 +#57 := (not #56)
1.4287 +#147 := (iff #57 #144)
1.4288 +#137 := (iff #130 #134)
1.4289 +#140 := (not #137)
1.4290 +#145 := (iff #140 #144)
1.4291 +#146 := [rewrite]: #145
1.4292 +#141 := (iff #57 #140)
1.4293 +#138 := (iff #56 #137)
1.4294 +#135 := (iff #55 #134)
1.4295 +#136 := [rewrite]: #135
1.4296 +#132 := (iff #50 #130)
1.4297 +#133 := [rewrite]: #132
1.4298 +#139 := [monotonicity #133 #136]: #138
1.4299 +#142 := [monotonicity #139]: #141
1.4300 +#148 := [trans #142 #146]: #147
1.4301 +#129 := [asserted]: #57
1.4302 +#151 := [mp #129 #148]: #144
1.4303 +#241 := (not #144)
1.4304 +#328 := (or #134 #130 #241)
1.4305 +#242 := [def-axiom]: #328
1.4306 +#243 := [unit-resolution #242 #151]: #329
1.4307 +#561 := [unit-resolution #243 #570]: #134
1.4308 +#330 := (not #134)
1.4309 +#559 := (or #330 #655)
1.4310 +#652 := (iff #134 #655)
1.4311 +#311 := (or #306 #652)
1.4312 +#308 := (or #653 #335)
1.4313 +#440 := (not #308)
1.4314 +#647 := (iff #134 #440)
1.4315 +#649 := (or #306 #647)
1.4316 +#650 := (iff #649 #311)
1.4317 +#634 := (iff #311 #311)
1.4318 +#295 := [rewrite]: #634
1.4319 +#658 := (iff #647 #652)
1.4320 +#656 := (iff #440 #655)
1.4321 +#320 := (iff #308 #319)
1.4322 +#654 := [rewrite]: #320
1.4323 +#657 := [monotonicity #654]: #656
1.4324 +#648 := [monotonicity #657]: #658
1.4325 +#291 := [monotonicity #648]: #650
1.4326 +#296 := [trans #291 #295]: #650
1.4327 +#307 := [quant-inst #41 #51 #46]: #649
1.4328 +#297 := [mp #307 #296]: #311
1.4329 +#562 := [unit-resolution #297 #686]: #652
1.4330 +#635 := (not #652)
1.4331 +#642 := (or #635 #330 #655)
1.4332 +#644 := [def-axiom]: #642
1.4333 +#563 := [unit-resolution #644 #562]: #559
1.4334 +#543 := [unit-resolution #563 #561]: #655
1.4335 +#637 := (or #319 #651)
1.4336 +#638 := [def-axiom]: #637
1.4337 +#544 := [unit-resolution #638 #543]: #651
1.4338 +#576 := (or #582 #615 #653)
1.4339 +#577 := [def-axiom]: #576
1.4340 +#547 := [unit-resolution #577 #544]: #546
1.4341 +#548 := [unit-resolution #547 #560]: #615
1.4342 +#606 := (or #614 #355)
1.4343 +#572 := [def-axiom]: #606
1.4344 +#549 := [unit-resolution #572 #548]: #355
1.4345 +#631 := (or #343 #356 #633)
1.4346 +#340 := [def-axiom]: #631
1.4347 +#550 := [unit-resolution #340 #549 #558]: #633
1.4348 +#298 := (or #319 #331)
1.4349 +#636 := [def-axiom]: #298
1.4350 +#551 := [unit-resolution #636 #543]: #331
1.4351 +#574 := (or #614 #628)
1.4352 +#584 := [def-axiom]: #574
1.4353 +#552 := [unit-resolution #584 #548]: #628
1.4354 +#609 := (or #493 #335 #625)
1.4355 +#603 := [def-axiom]: #609
1.4356 +#553 := [unit-resolution #603 #552 #551]: #493
1.4357 +#441 := (or #587 #484 #632)
1.4358 +#442 := [def-axiom]: #441
1.4359 +#554 := [unit-resolution #442 #553 #550 #569]: false
1.4360 +#555 := [lemma #554]: #130
1.4361 +#545 := (or #143 #343)
1.4362 +#622 := (or #341 #143 #343)
1.4363 +#623 := [def-axiom]: #622
1.4364 +#556 := [unit-resolution #623 #566]: #545
1.4365 +#534 := [unit-resolution #556 #555]: #343
1.4366 +#630 := (or #357 #632)
1.4367 +#627 := [def-axiom]: #630
1.4368 +#535 := [unit-resolution #627 #534]: #632
1.4369 +#610 := (or #587 #493 #633)
1.4370 +#439 := [def-axiom]: #610
1.4371 +#537 := [unit-resolution #439 #535 #569]: #493
1.4372 +#602 := (or #484 #628)
1.4373 +#608 := [def-axiom]: #602
1.4374 +#538 := [unit-resolution #608 #537]: #628
1.4375 +#352 := (or #357 #355)
1.4376 +#626 := [def-axiom]: #352
1.4377 +#539 := [unit-resolution #626 #534]: #355
1.4378 +#585 := (or #615 #356 #625)
1.4379 +#586 := [def-axiom]: #585
1.4380 +#540 := [unit-resolution #586 #539 #538]: #615
1.4381 +#333 := (or #330 #143)
1.4382 +#321 := (or #330 #143 #241)
1.4383 +#332 := [def-axiom]: #321
1.4384 +#261 := [unit-resolution #332 #151]: #333
1.4385 +#541 := [unit-resolution #261 #555]: #330
1.4386 +#536 := (or #134 #319)
1.4387 +#641 := (or #635 #134 #319)
1.4388 +#277 := [def-axiom]: #641
1.4389 +#542 := [unit-resolution #277 #562]: #536
1.4390 +#528 := [unit-resolution #542 #541]: #319
1.4391 +#607 := (or #484 #331)
1.4392 +#601 := [def-axiom]: #607
1.4393 +#524 := [unit-resolution #601 #537]: #331
1.4394 +#639 := (or #655 #335 #653)
1.4395 +#640 := [def-axiom]: #639
1.4396 +#525 := [unit-resolution #640 #524 #528]: #653
1.4397 +#578 := (or #582 #614 #651)
1.4398 +#579 := [def-axiom]: #578
1.4399 +#526 := [unit-resolution #579 #525 #540]: #582
1.4400 +[unit-resolution #605 #686 #526]: false
1.4401 +unsat
1.4402 +6c759b8f06a9510b6e4f2c41f45fd7a908ea138f 22 0
1.4403 +#2 := false
1.4404 +decl f13 :: (-> S7 S3 S4)
1.4405 +decl f4 :: S3
1.4406 +#8 := f4
1.4407 +decl f14 :: S7
1.4408 +#50 := f14
1.4409 +#51 := (f13 f14 f4)
1.4410 +#52 := (= #51 #51)
1.4411 +#53 := (not #52)
1.4412 +#148 := (iff #53 false)
1.4413 +#1 := true
1.4414 +#143 := (not true)
1.4415 +#146 := (iff #143 false)
1.4416 +#147 := [rewrite]: #146
1.4417 +#144 := (iff #53 #143)
1.4418 +#140 := (iff #52 true)
1.4419 +#142 := [rewrite]: #140
1.4420 +#145 := [monotonicity #142]: #144
1.4421 +#149 := [trans #145 #147]: #148
1.4422 +#139 := [asserted]: #53
1.4423 +[mp #139 #149]: false
1.4424 +unsat