# HG changeset patch
# User boehmes
# Date 1315986419 -7200
# Node ID 1db6baa40b0e72ffde4c1603111a1abb454bcec1
# Parent  1a5811bfe837ea4eb2184499ee24695b3897b4be
observe distinction between sets and predicates

diff -r 1a5811bfe837 -r 1db6baa40b0e src/HOL/SMT_Examples/SMT_Tests.certs
--- a/src/HOL/SMT_Examples/SMT_Tests.certs	Wed Sep 14 06:49:24 2011 +0200
+++ b/src/HOL/SMT_Examples/SMT_Tests.certs	Wed Sep 14 09:46:59 2011 +0200
@@ -60554,3 +60554,2186 @@
 #229 := [mp #227 #156]: #225
 [unit-resolution #229 #561 #66 #74]: false
 unsat
+7cd7dbb3fbfb0bc76acedbcf070880f3e3e3d434 60 0
+#2 := false
+decl f3 :: (-> S2 S3 S1)
+decl f4 :: S3
+#9 := f4
+decl f9 :: S2
+#39 := f9
+#40 := (f3 f9 f4)
+decl f1 :: S1
+#4 := f1
+#116 := (= f1 #40)
+#41 := (= #40 f1)
+#42 := (not #41)
+#43 := (not #42)
+#128 := (iff #43 #116)
+#120 := (not #116)
+#123 := (not #120)
+#126 := (iff #123 #116)
+#127 := [rewrite]: #126
+#124 := (iff #43 #123)
+#121 := (iff #42 #120)
+#118 := (iff #41 #116)
+#119 := [rewrite]: #118
+#122 := [monotonicity #119]: #121
+#125 := [monotonicity #122]: #124
+#129 := [trans #125 #127]: #128
+#115 := [asserted]: #43
+#132 := [mp #115 #129]: #116
+#8 := (:var 0 S2)
+#10 := (f3 #8 f4)
+#640 := (pattern #10)
+#64 := (= f1 #10)
+#67 := (not #64)
+#641 := (forall (vars (?v0 S2)) (:pat #640) #67)
+#70 := (forall (vars (?v0 S2)) #67)
+#644 := (iff #70 #641)
+#642 := (iff #67 #67)
+#643 := [refl]: #642
+#645 := [quant-intro #643]: #644
+#146 := (~ #70 #70)
+#144 := (~ #67 #67)
+#145 := [refl]: #144
+#147 := [nnf-pos #145]: #146
+#11 := (= #10 f1)
+#12 := (not #11)
+#13 := (forall (vars (?v0 S2)) #12)
+#71 := (iff #13 #70)
+#68 := (iff #12 #67)
+#65 := (iff #11 #64)
+#66 := [rewrite]: #65
+#69 := [monotonicity #66]: #68
+#72 := [quant-intro #69]: #71
+#63 := [asserted]: #13
+#75 := [mp #63 #72]: #70
+#131 := [mp~ #75 #147]: #70
+#646 := [mp #131 #645]: #641
+#223 := (not #641)
+#310 := (or #223 #120)
+#224 := [quant-inst #39]: #310
+[unit-resolution #224 #646 #132]: false
+unsat
+71b592381f7787562afdf512ef22356644e574ef 48 0
+#2 := false
+decl f3 :: (-> S2 S3 S1)
+decl f5 :: S3
+#14 := f5
+decl f9 :: S2
+#39 := f9
+#40 := (f3 f9 f5)
+decl f1 :: S1
+#4 := f1
+#115 := (= f1 #40)
+#119 := (not #115)
+#41 := (= #40 f1)
+#42 := (not #41)
+#120 := (iff #42 #119)
+#117 := (iff #41 #115)
+#118 := [rewrite]: #117
+#121 := [monotonicity #118]: #120
+#114 := [asserted]: #42
+#124 := [mp #114 #121]: #119
+#8 := (:var 0 S2)
+#15 := (f3 #8 f5)
+#639 := (pattern #15)
+#73 := (= f1 #15)
+#640 := (forall (vars (?v0 S2)) (:pat #639) #73)
+#77 := (forall (vars (?v0 S2)) #73)
+#643 := (iff #77 #640)
+#641 := (iff #73 #73)
+#642 := [refl]: #641
+#644 := [quant-intro #642]: #643
+#126 := (~ #77 #77)
+#125 := (~ #73 #73)
+#140 := [refl]: #125
+#127 := [nnf-pos #140]: #126
+#16 := (= #15 f1)
+#17 := (forall (vars (?v0 S2)) #16)
+#78 := (iff #17 #77)
+#75 := (iff #16 #73)
+#76 := [rewrite]: #75
+#79 := [quant-intro #76]: #78
+#72 := [asserted]: #17
+#82 := [mp #72 #79]: #77
+#141 := [mp~ #82 #127]: #77
+#645 := [mp #141 #644]: #640
+#215 := (not #640)
+#302 := (or #215 #115)
+#216 := [quant-inst #39]: #302
+[unit-resolution #216 #645 #124]: false
+unsat
+164d5a6bdaf120b4948f5b45d9c26eb765a67512 124 0
+#2 := false
+decl f3 :: (-> S2 S3 S1)
+decl f6 :: (-> S4 S3 S3)
+decl f11 :: S3
+#42 := f11
+decl f7 :: (-> S3 S4)
+decl f10 :: S3
+#40 := f10
+#41 := (f7 f10)
+#43 := (f6 #41 f11)
+decl f9 :: S2
+#39 := f9
+#44 := (f3 f9 #43)
+decl f1 :: S1
+#4 := f1
+#125 := (= f1 #44)
+#144 := (not #125)
+#648 := [hypothesis]: #144
+#48 := (f3 f9 f11)
+#132 := (= f1 #48)
+#46 := (f3 f9 f10)
+#129 := (= f1 #46)
+#135 := (or #129 #132)
+#336 := (or #135 #125)
+#145 := (iff #135 #144)
+#49 := (= #48 f1)
+#47 := (= #46 f1)
+#50 := (or #47 #49)
+#45 := (= #44 f1)
+#51 := (iff #45 #50)
+#52 := (not #51)
+#148 := (iff #52 #145)
+#138 := (iff #125 #135)
+#141 := (not #138)
+#146 := (iff #141 #145)
+#147 := [rewrite]: #146
+#142 := (iff #52 #141)
+#139 := (iff #51 #138)
+#136 := (iff #50 #135)
+#133 := (iff #49 #132)
+#134 := [rewrite]: #133
+#130 := (iff #47 #129)
+#131 := [rewrite]: #130
+#137 := [monotonicity #131 #134]: #136
+#127 := (iff #45 #125)
+#128 := [rewrite]: #127
+#140 := [monotonicity #128 #137]: #139
+#143 := [monotonicity #140]: #142
+#149 := [trans #143 #147]: #148
+#124 := [asserted]: #52
+#152 := [mp #124 #149]: #145
+#262 := (not #145)
+#335 := (or #135 #125 #262)
+#332 := [def-axiom]: #335
+#315 := [unit-resolution #332 #152]: #336
+#320 := [unit-resolution #315 #648]: #135
+#322 := (not #135)
+#651 := (or #125 #322)
+#21 := (:var 0 S3)
+#19 := (:var 1 S3)
+#20 := (f7 #19)
+#22 := (f6 #20 #21)
+#18 := (:var 2 S2)
+#23 := (f3 #18 #22)
+#674 := (pattern #23)
+#27 := (f3 #18 #21)
+#98 := (= f1 #27)
+#25 := (f3 #18 #19)
+#95 := (= f1 #25)
+#101 := (or #95 #98)
+#91 := (= f1 #23)
+#104 := (iff #91 #101)
+#675 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #674) #104)
+#107 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #104)
+#678 := (iff #107 #675)
+#676 := (iff #104 #104)
+#677 := [refl]: #676
+#679 := [quant-intro #677]: #678
+#156 := (~ #107 #107)
+#170 := (~ #104 #104)
+#171 := [refl]: #170
+#157 := [nnf-pos #171]: #156
+#28 := (= #27 f1)
+#26 := (= #25 f1)
+#29 := (or #26 #28)
+#24 := (= #23 f1)
+#30 := (iff #24 #29)
+#31 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #30)
+#108 := (iff #31 #107)
+#105 := (iff #30 #104)
+#102 := (iff #29 #101)
+#99 := (iff #28 #98)
+#100 := [rewrite]: #99
+#96 := (iff #26 #95)
+#97 := [rewrite]: #96
+#103 := [monotonicity #97 #100]: #102
+#93 := (iff #24 #91)
+#94 := [rewrite]: #93
+#106 := [monotonicity #94 #103]: #105
+#109 := [quant-intro #106]: #108
+#90 := [asserted]: #31
+#112 := [mp #90 #109]: #107
+#172 := [mp~ #112 #157]: #107
+#680 := [mp #172 #679]: #675
+#321 := (not #675)
+#655 := (or #321 #138)
+#656 := [quant-inst #39 #40 #42]: #655
+#308 := [unit-resolution #656 #680]: #138
+#657 := (or #141 #125 #322)
+#658 := [def-axiom]: #657
+#292 := [unit-resolution #658 #308]: #651
+#635 := [unit-resolution #292 #320 #648]: false
+#296 := [lemma #635]: #125
+#309 := (or #322 #144)
+#652 := (or #322 #144 #262)
+#654 := [def-axiom]: #652
+#441 := [unit-resolution #654 #152]: #309
+#297 := [unit-resolution #441 #296]: #322
+#298 := (or #144 #135)
+#653 := (or #141 #144 #135)
+#659 := [def-axiom]: #653
+#299 := [unit-resolution #659 #308]: #298
+[unit-resolution #299 #297 #296]: false
+unsat
+d1bc5c257411f66b4000ce061c39762e6b5b7a04 160 0
+#2 := false
+decl f3 :: (-> S2 S3 S1)
+decl f4 :: S3
+#9 := f4
+decl f9 :: S2
+#39 := f9
+#325 := (f3 f9 f4)
+decl f1 :: S1
+#4 := f1
+#322 := (= f1 #325)
+decl f10 :: S3
+#40 := f10
+#45 := (f3 f9 f10)
+#125 := (= f1 #45)
+#326 := (or #125 #322)
+decl f6 :: (-> S4 S3 S3)
+decl f7 :: (-> S3 S4)
+#41 := (f7 f10)
+#42 := (f6 #41 f4)
+#43 := (f3 f9 #42)
+#121 := (= f1 #43)
+#134 := (not #121)
+#642 := [hypothesis]: #134
+#320 := (or #125 #121)
+#135 := (iff #125 #134)
+#46 := (= #45 f1)
+#44 := (= #43 f1)
+#47 := (iff #44 #46)
+#48 := (not #47)
+#138 := (iff #48 #135)
+#128 := (iff #121 #125)
+#131 := (not #128)
+#136 := (iff #131 #135)
+#137 := [rewrite]: #136
+#132 := (iff #48 #131)
+#129 := (iff #47 #128)
+#126 := (iff #46 #125)
+#127 := [rewrite]: #126
+#123 := (iff #44 #121)
+#124 := [rewrite]: #123
+#130 := [monotonicity #124 #127]: #129
+#133 := [monotonicity #130]: #132
+#139 := [trans #133 #137]: #138
+#120 := [asserted]: #48
+#142 := [mp #120 #139]: #135
+#232 := (not #135)
+#319 := (or #125 #121 #232)
+#233 := [def-axiom]: #319
+#234 := [unit-resolution #233 #142]: #320
+#644 := [unit-resolution #234 #642]: #125
+#648 := (not #326)
+#288 := (or #121 #648)
+#305 := (iff #121 #326)
+#21 := (:var 0 S3)
+#19 := (:var 1 S3)
+#20 := (f7 #19)
+#22 := (f6 #20 #21)
+#18 := (:var 2 S2)
+#23 := (f3 #18 #22)
+#664 := (pattern #23)
+#27 := (f3 #18 #21)
+#94 := (= f1 #27)
+#25 := (f3 #18 #19)
+#91 := (= f1 #25)
+#97 := (or #91 #94)
+#87 := (= f1 #23)
+#100 := (iff #87 #97)
+#665 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #664) #100)
+#103 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #100)
+#668 := (iff #103 #665)
+#666 := (iff #100 #100)
+#667 := [refl]: #666
+#669 := [quant-intro #667]: #668
+#146 := (~ #103 #103)
+#160 := (~ #100 #100)
+#161 := [refl]: #160
+#147 := [nnf-pos #161]: #146
+#28 := (= #27 f1)
+#26 := (= #25 f1)
+#29 := (or #26 #28)
+#24 := (= #23 f1)
+#30 := (iff #24 #29)
+#31 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #30)
+#104 := (iff #31 #103)
+#101 := (iff #30 #100)
+#98 := (iff #29 #97)
+#95 := (iff #28 #94)
+#96 := [rewrite]: #95
+#92 := (iff #26 #91)
+#93 := [rewrite]: #92
+#99 := [monotonicity #93 #96]: #98
+#89 := (iff #24 #87)
+#90 := [rewrite]: #89
+#102 := [monotonicity #90 #99]: #101
+#105 := [quant-intro #102]: #104
+#86 := [asserted]: #31
+#108 := [mp #86 #105]: #103
+#162 := [mp~ #108 #147]: #103
+#670 := [mp #162 #669]: #665
+#299 := (not #665)
+#431 := (or #299 #305)
+#638 := [quant-inst #39 #40 #9]: #431
+#287 := [unit-resolution #638 #670]: #305
+#639 := (not #305)
+#297 := (or #639 #121 #648)
+#302 := [def-axiom]: #297
+#289 := [unit-resolution #302 #287]: #288
+#627 := [unit-resolution #289 #642]: #648
+#321 := (not #125)
+#310 := (or #326 #321)
+#311 := [def-axiom]: #310
+#628 := [unit-resolution #311 #627 #644]: false
+#629 := [lemma #628]: #121
+#630 := (or #134 #326)
+#640 := (or #639 #134 #326)
+#298 := [def-axiom]: #640
+#631 := [unit-resolution #298 #287]: #630
+#633 := [unit-resolution #631 #629]: #326
+#324 := (or #321 #134)
+#312 := (or #321 #134 #232)
+#323 := [def-axiom]: #312
+#252 := [unit-resolution #323 #142]: #324
+#635 := [unit-resolution #252 #629]: #321
+#643 := (or #648 #125 #322)
+#649 := [def-axiom]: #643
+#273 := [unit-resolution #649 #635 #633]: #322
+#8 := (:var 0 S2)
+#10 := (f3 #8 f4)
+#650 := (pattern #10)
+#69 := (= f1 #10)
+#72 := (not #69)
+#651 := (forall (vars (?v0 S2)) (:pat #650) #72)
+#75 := (forall (vars (?v0 S2)) #72)
+#654 := (iff #75 #651)
+#652 := (iff #72 #72)
+#653 := [refl]: #652
+#655 := [quant-intro #653]: #654
+#156 := (~ #75 #75)
+#154 := (~ #72 #72)
+#155 := [refl]: #154
+#157 := [nnf-pos #155]: #156
+#11 := (= #10 f1)
+#12 := (not #11)
+#13 := (forall (vars (?v0 S2)) #12)
+#76 := (iff #13 #75)
+#73 := (iff #12 #72)
+#70 := (iff #11 #69)
+#71 := [rewrite]: #70
+#74 := [monotonicity #71]: #73
+#77 := [quant-intro #74]: #76
+#68 := [asserted]: #13
+#80 := [mp #68 #77]: #75
+#141 := [mp~ #80 #157]: #75
+#656 := [mp #141 #655]: #651
+#645 := (not #322)
+#626 := (not #651)
+#632 := (or #626 #645)
+#268 := [quant-inst #39]: #632
+[unit-resolution #268 #656 #273]: false
+unsat
+37e8c2c682de93175c2e3b6573d2a98ccec54dc2 134 0
+#2 := false
+decl f3 :: (-> S2 S3 S1)
+decl f5 :: S3
+#14 := f5
+decl f9 :: S2
+#39 := f9
+#217 := (f3 f9 f5)
+decl f1 :: S1
+#4 := f1
+#304 := (= f1 #217)
+#631 := (not #304)
+decl f10 :: S3
+#40 := f10
+#218 := (f3 f9 f10)
+#305 := (= f1 #218)
+#297 := (or #304 #305)
+#282 := (not #297)
+decl f6 :: (-> S4 S3 S3)
+decl f7 :: (-> S3 S4)
+#41 := (f7 f10)
+#42 := (f6 #41 f5)
+#43 := (f3 f9 #42)
+#118 := (= f1 #43)
+#237 := (iff #118 #297)
+#21 := (:var 0 S3)
+#19 := (:var 1 S3)
+#20 := (f7 #19)
+#22 := (f6 #20 #21)
+#18 := (:var 2 S2)
+#23 := (f3 #18 #22)
+#649 := (pattern #23)
+#27 := (f3 #18 #21)
+#91 := (= f1 #27)
+#25 := (f3 #18 #19)
+#88 := (= f1 #25)
+#94 := (or #88 #91)
+#84 := (= f1 #23)
+#97 := (iff #84 #94)
+#650 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #649) #97)
+#100 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #97)
+#653 := (iff #100 #650)
+#651 := (iff #97 #97)
+#652 := [refl]: #651
+#654 := [quant-intro #652]: #653
+#131 := (~ #100 #100)
+#145 := (~ #97 #97)
+#146 := [refl]: #145
+#132 := [nnf-pos #146]: #131
+#28 := (= #27 f1)
+#26 := (= #25 f1)
+#29 := (or #26 #28)
+#24 := (= #23 f1)
+#30 := (iff #24 #29)
+#31 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #30)
+#101 := (iff #31 #100)
+#98 := (iff #30 #97)
+#95 := (iff #29 #94)
+#92 := (iff #28 #91)
+#93 := [rewrite]: #92
+#89 := (iff #26 #88)
+#90 := [rewrite]: #89
+#96 := [monotonicity #90 #93]: #95
+#86 := (iff #24 #84)
+#87 := [rewrite]: #86
+#99 := [monotonicity #87 #96]: #98
+#102 := [quant-intro #99]: #101
+#83 := [asserted]: #31
+#105 := [mp #83 #102]: #100
+#147 := [mp~ #105 #132]: #100
+#655 := [mp #147 #654]: #650
+#311 := (not #650)
+#290 := (or #311 #237)
+#219 := (or #305 #304)
+#306 := (iff #118 #219)
+#627 := (or #311 #306)
+#284 := (iff #627 #290)
+#623 := (iff #290 #290)
+#295 := [rewrite]: #623
+#310 := (iff #306 #237)
+#308 := (iff #219 #297)
+#309 := [rewrite]: #308
+#307 := [monotonicity #309]: #310
+#416 := [monotonicity #307]: #284
+#296 := [trans #416 #295]: #284
+#629 := [quant-inst #39 #40 #14]: #627
+#630 := [mp #629 #296]: #290
+#613 := [unit-resolution #630 #655]: #237
+#283 := (not #237)
+#614 := (or #283 #282)
+#122 := (not #118)
+#44 := (= #43 f1)
+#45 := (not #44)
+#123 := (iff #45 #122)
+#120 := (iff #44 #118)
+#121 := [rewrite]: #120
+#124 := [monotonicity #121]: #123
+#117 := [asserted]: #45
+#127 := [mp #117 #124]: #122
+#626 := (or #283 #118 #282)
+#267 := [def-axiom]: #626
+#617 := [unit-resolution #267 #127]: #614
+#253 := [unit-resolution #617 #613]: #282
+#632 := (or #297 #631)
+#633 := [def-axiom]: #632
+#618 := [unit-resolution #633 #253]: #631
+#8 := (:var 0 S2)
+#15 := (f3 #8 f5)
+#642 := (pattern #15)
+#76 := (= f1 #15)
+#643 := (forall (vars (?v0 S2)) (:pat #642) #76)
+#80 := (forall (vars (?v0 S2)) #76)
+#646 := (iff #80 #643)
+#644 := (iff #76 #76)
+#645 := [refl]: #644
+#647 := [quant-intro #645]: #646
+#129 := (~ #80 #80)
+#128 := (~ #76 #76)
+#143 := [refl]: #128
+#130 := [nnf-pos #143]: #129
+#16 := (= #15 f1)
+#17 := (forall (vars (?v0 S2)) #16)
+#81 := (iff #17 #80)
+#78 := (iff #16 #76)
+#79 := [rewrite]: #78
+#82 := [quant-intro #79]: #81
+#75 := [asserted]: #17
+#85 := [mp #75 #82]: #80
+#144 := [mp~ #85 #130]: #80
+#648 := [mp #144 #647]: #643
+#615 := (not #643)
+#616 := (or #615 #304)
+#611 := [quant-inst #39]: #616
+[unit-resolution #611 #648 #618]: false
+unsat
+8b3671158912b5be83077a5d2f71eae8a40f4427 153 0
+#2 := false
+decl f3 :: (-> S2 S3 S1)
+decl f6 :: (-> S4 S3 S3)
+decl f10 :: S3
+#40 := f10
+decl f7 :: (-> S3 S4)
+decl f11 :: S3
+#42 := f11
+#46 := (f7 f11)
+#47 := (f6 #46 f10)
+decl f9 :: S2
+#39 := f9
+#48 := (f3 f9 #47)
+decl f1 :: S1
+#4 := f1
+#128 := (= f1 #48)
+#324 := (not #128)
+#41 := (f7 f10)
+#43 := (f6 #41 f11)
+#44 := (f3 f9 #43)
+#124 := (= f1 #44)
+#137 := (not #124)
+#243 := [hypothesis]: #137
+#323 := (or #128 #124)
+#138 := (iff #128 #137)
+#49 := (= #48 f1)
+#45 := (= #44 f1)
+#50 := (iff #45 #49)
+#51 := (not #50)
+#141 := (iff #51 #138)
+#131 := (iff #124 #128)
+#134 := (not #131)
+#139 := (iff #134 #138)
+#140 := [rewrite]: #139
+#135 := (iff #51 #134)
+#132 := (iff #50 #131)
+#129 := (iff #49 #128)
+#130 := [rewrite]: #129
+#126 := (iff #45 #124)
+#127 := [rewrite]: #126
+#133 := [monotonicity #127 #130]: #132
+#136 := [monotonicity #133]: #135
+#142 := [trans #136 #140]: #141
+#123 := [asserted]: #51
+#145 := [mp #123 #142]: #138
+#235 := (not #138)
+#322 := (or #128 #124 #235)
+#236 := [def-axiom]: #322
+#237 := [unit-resolution #236 #145]: #323
+#622 := [unit-resolution #237 #243]: #128
+#328 := (f3 f9 f10)
+#325 := (= f1 #328)
+#329 := (f3 f9 f11)
+#308 := (= f1 #329)
+#645 := (or #308 #325)
+#642 := (not #645)
+#345 := (or #124 #642)
+#632 := (iff #124 #645)
+#21 := (:var 0 S3)
+#19 := (:var 1 S3)
+#20 := (f7 #19)
+#22 := (f6 #20 #21)
+#18 := (:var 2 S2)
+#23 := (f3 #18 #22)
+#667 := (pattern #23)
+#27 := (f3 #18 #21)
+#97 := (= f1 #27)
+#25 := (f3 #18 #19)
+#94 := (= f1 #25)
+#100 := (or #94 #97)
+#90 := (= f1 #23)
+#103 := (iff #90 #100)
+#668 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #667) #103)
+#106 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #103)
+#671 := (iff #106 #668)
+#669 := (iff #103 #103)
+#670 := [refl]: #669
+#672 := [quant-intro #670]: #671
+#149 := (~ #106 #106)
+#163 := (~ #103 #103)
+#164 := [refl]: #163
+#150 := [nnf-pos #164]: #149
+#28 := (= #27 f1)
+#26 := (= #25 f1)
+#29 := (or #26 #28)
+#24 := (= #23 f1)
+#30 := (iff #24 #29)
+#31 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #30)
+#107 := (iff #31 #106)
+#104 := (iff #30 #103)
+#101 := (iff #29 #100)
+#98 := (iff #28 #97)
+#99 := [rewrite]: #98
+#95 := (iff #26 #94)
+#96 := [rewrite]: #95
+#102 := [monotonicity #96 #99]: #101
+#92 := (iff #24 #90)
+#93 := [rewrite]: #92
+#105 := [monotonicity #93 #102]: #104
+#108 := [quant-intro #105]: #107
+#89 := [asserted]: #31
+#111 := [mp #89 #108]: #106
+#165 := [mp~ #111 #150]: #106
+#673 := [mp #165 #672]: #668
+#641 := (not #668)
+#629 := (or #641 #632)
+#302 := (or #325 #308)
+#434 := (iff #124 #302)
+#635 := (or #641 #434)
+#636 := (iff #635 #629)
+#276 := (iff #629 #629)
+#277 := [rewrite]: #276
+#633 := (iff #434 #632)
+#630 := (iff #302 #645)
+#631 := [rewrite]: #630
+#634 := [monotonicity #631]: #633
+#638 := [monotonicity #634]: #636
+#639 := [trans #638 #277]: #636
+#271 := [quant-inst #39 #40 #42]: #635
+#637 := [mp #271 #639]: #629
+#623 := [unit-resolution #637 #673]: #632
+#640 := (not #632)
+#626 := (or #640 #124 #642)
+#627 := [def-axiom]: #626
+#346 := [unit-resolution #627 #623]: #345
+#620 := [unit-resolution #346 #243]: #642
+#621 := (or #324 #645)
+#647 := (iff #128 #645)
+#313 := (or #641 #647)
+#314 := [quant-inst #39 #42 #40]: #313
+#624 := [unit-resolution #314 #673]: #647
+#643 := (not #647)
+#285 := (or #643 #324 #645)
+#628 := [def-axiom]: #285
+#625 := [unit-resolution #628 #624]: #621
+#334 := [unit-resolution #625 #620 #622]: false
+#335 := [lemma #334]: #124
+#327 := (or #324 #137)
+#315 := (or #324 #137 #235)
+#326 := [def-axiom]: #315
+#255 := [unit-resolution #326 #145]: #327
+#336 := [unit-resolution #255 #335]: #324
+#338 := (or #137 #645)
+#333 := (or #640 #137 #645)
+#349 := [def-axiom]: #333
+#616 := [unit-resolution #349 #623]: #338
+#617 := [unit-resolution #616 #335]: #645
+#330 := (or #128 #642)
+#301 := (or #643 #128 #642)
+#644 := [def-axiom]: #301
+#614 := [unit-resolution #644 #624]: #330
+[unit-resolution #614 #617 #336]: false
+unsat
+76f35b24758dff3b162e8fc64fc760da00fb55d8 126 0
+#2 := false
+decl f3 :: (-> S2 S3 S1)
+decl f6 :: (-> S4 S3 S3)
+decl f10 :: S3
+#40 := f10
+decl f7 :: (-> S3 S4)
+#41 := (f7 f10)
+#42 := (f6 #41 f10)
+decl f9 :: S2
+#39 := f9
+#43 := (f3 f9 #42)
+decl f1 :: S1
+#4 := f1
+#121 := (= f1 #43)
+#134 := (not #121)
+#625 := [hypothesis]: #134
+#45 := (f3 f9 f10)
+#125 := (= f1 #45)
+#320 := (or #125 #121)
+#135 := (iff #125 #134)
+#46 := (= #45 f1)
+#44 := (= #43 f1)
+#47 := (iff #44 #46)
+#48 := (not #47)
+#138 := (iff #48 #135)
+#128 := (iff #121 #125)
+#131 := (not #128)
+#136 := (iff #131 #135)
+#137 := [rewrite]: #136
+#132 := (iff #48 #131)
+#129 := (iff #47 #128)
+#126 := (iff #46 #125)
+#127 := [rewrite]: #126
+#123 := (iff #44 #121)
+#124 := [rewrite]: #123
+#130 := [monotonicity #124 #127]: #129
+#133 := [monotonicity #130]: #132
+#139 := [trans #133 #137]: #138
+#120 := [asserted]: #48
+#142 := [mp #120 #139]: #135
+#232 := (not #135)
+#319 := (or #125 #121 #232)
+#233 := [def-axiom]: #319
+#234 := [unit-resolution #233 #142]: #320
+#286 := [unit-resolution #234 #625]: #125
+#321 := (not #125)
+#288 := (or #121 #321)
+#21 := (:var 0 S3)
+#19 := (:var 1 S3)
+#20 := (f7 #19)
+#22 := (f6 #20 #21)
+#18 := (:var 2 S2)
+#23 := (f3 #18 #22)
+#664 := (pattern #23)
+#27 := (f3 #18 #21)
+#94 := (= f1 #27)
+#25 := (f3 #18 #19)
+#91 := (= f1 #25)
+#97 := (or #91 #94)
+#87 := (= f1 #23)
+#100 := (iff #87 #97)
+#665 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #664) #100)
+#103 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #100)
+#668 := (iff #103 #665)
+#666 := (iff #100 #100)
+#667 := [refl]: #666
+#669 := [quant-intro #667]: #668
+#146 := (~ #103 #103)
+#160 := (~ #100 #100)
+#161 := [refl]: #160
+#147 := [nnf-pos #161]: #146
+#28 := (= #27 f1)
+#26 := (= #25 f1)
+#29 := (or #26 #28)
+#24 := (= #23 f1)
+#30 := (iff #24 #29)
+#31 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #30)
+#104 := (iff #31 #103)
+#101 := (iff #30 #100)
+#98 := (iff #29 #97)
+#95 := (iff #28 #94)
+#96 := [rewrite]: #95
+#92 := (iff #26 #91)
+#93 := [rewrite]: #92
+#99 := [monotonicity #93 #96]: #98
+#89 := (iff #24 #87)
+#90 := [rewrite]: #89
+#102 := [monotonicity #90 #99]: #101
+#105 := [quant-intro #102]: #104
+#86 := [asserted]: #31
+#108 := [mp #86 #105]: #103
+#162 := [mp~ #108 #147]: #103
+#670 := [mp #162 #669]: #665
+#299 := (not #665)
+#431 := (or #299 #128)
+#325 := (or #125 #125)
+#322 := (iff #121 #325)
+#638 := (or #299 #322)
+#311 := (iff #638 #431)
+#646 := (iff #431 #431)
+#647 := [rewrite]: #646
+#642 := (iff #322 #128)
+#326 := (iff #325 #125)
+#305 := [rewrite]: #326
+#644 := [monotonicity #305]: #642
+#645 := [monotonicity #644]: #311
+#648 := [trans #645 #647]: #311
+#310 := [quant-inst #39 #40 #40]: #638
+#643 := [mp #310 #648]: #431
+#287 := [unit-resolution #643 #670]: #128
+#649 := (or #131 #121 #321)
+#639 := [def-axiom]: #649
+#289 := [unit-resolution #639 #287]: #288
+#627 := [unit-resolution #289 #286 #625]: false
+#628 := [lemma #627]: #121
+#324 := (or #321 #134)
+#312 := (or #321 #134 #232)
+#323 := [def-axiom]: #312
+#252 := [unit-resolution #323 #142]: #324
+#629 := [unit-resolution #252 #628]: #321
+#630 := (or #134 #125)
+#297 := (or #131 #134 #125)
+#302 := [def-axiom]: #297
+#631 := [unit-resolution #302 #287]: #630
+[unit-resolution #631 #629 #628]: false
+unsat
+2ac06f7d84c36d7f3c61e2f783f6f8bf82530665 264 0
+#2 := false
+decl f3 :: (-> S2 S3 S1)
+decl f11 :: S3
+#42 := f11
+decl f9 :: S2
+#39 := f9
+#621 := (f3 f9 f11)
+decl f1 :: S1
+#4 := f1
+#334 := (= f1 #621)
+decl f12 :: S3
+#44 := f12
+#332 := (f3 f9 f12)
+#329 := (= f1 #332)
+#619 := (or #329 #334)
+decl f6 :: (-> S4 S3 S3)
+decl f7 :: (-> S3 S4)
+#43 := (f7 f11)
+#45 := (f6 #43 f12)
+#306 := (f3 f9 #45)
+#438 := (= f1 #306)
+#613 := (iff #438 #619)
+#579 := (not #613)
+#591 := (not #619)
+#603 := (not #334)
+decl f10 :: S3
+#40 := f10
+#634 := (f3 f9 f10)
+#635 := (= f1 #634)
+#481 := (or #334 #635)
+#606 := (not #481)
+#41 := (f7 f10)
+#49 := (f6 #41 f11)
+#333 := (f3 f9 #49)
+#312 := (= f1 #333)
+#589 := (iff #312 #481)
+#581 := (not #589)
+#574 := [hypothesis]: #581
+#21 := (:var 0 S3)
+#19 := (:var 1 S3)
+#20 := (f7 #19)
+#22 := (f6 #20 #21)
+#18 := (:var 2 S2)
+#23 := (f3 #18 #22)
+#671 := (pattern #23)
+#27 := (f3 #18 #21)
+#101 := (= f1 #27)
+#25 := (f3 #18 #19)
+#98 := (= f1 #25)
+#104 := (or #98 #101)
+#94 := (= f1 #23)
+#107 := (iff #94 #104)
+#672 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #671) #107)
+#110 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #107)
+#675 := (iff #110 #672)
+#673 := (iff #107 #107)
+#674 := [refl]: #673
+#676 := [quant-intro #674]: #675
+#153 := (~ #110 #110)
+#167 := (~ #107 #107)
+#168 := [refl]: #167
+#154 := [nnf-pos #168]: #153
+#28 := (= #27 f1)
+#26 := (= #25 f1)
+#29 := (or #26 #28)
+#24 := (= #23 f1)
+#30 := (iff #24 #29)
+#31 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #30)
+#111 := (iff #31 #110)
+#108 := (iff #30 #107)
+#105 := (iff #29 #104)
+#102 := (iff #28 #101)
+#103 := [rewrite]: #102
+#99 := (iff #26 #98)
+#100 := [rewrite]: #99
+#106 := [monotonicity #100 #103]: #105
+#96 := (iff #24 #94)
+#97 := [rewrite]: #96
+#109 := [monotonicity #97 #106]: #108
+#112 := [quant-intro #109]: #111
+#93 := [asserted]: #31
+#115 := [mp #93 #112]: #110
+#169 := [mp~ #115 #154]: #110
+#677 := [mp #169 #676]: #672
+#645 := (not #672)
+#587 := (or #645 #589)
+#598 := (or #635 #334)
+#480 := (iff #312 #598)
+#590 := (or #645 #480)
+#490 := (iff #590 #587)
+#493 := (iff #587 #587)
+#486 := [rewrite]: #493
+#491 := (iff #480 #589)
+#482 := (iff #598 #481)
+#441 := [rewrite]: #482
+#586 := [monotonicity #441]: #491
+#492 := [monotonicity #586]: #490
+#494 := [trans #492 #486]: #490
+#475 := [quant-inst #39 #40 #42]: #590
+#495 := [mp #475 #494]: #587
+#575 := [unit-resolution #495 #677 #574]: false
+#576 := [lemma #575]: #589
+#652 := (not #312)
+#649 := (or #312 #329)
+#646 := (not #649)
+#50 := (f7 #49)
+#51 := (f6 #50 f12)
+#52 := (f3 f9 #51)
+#132 := (= f1 #52)
+#328 := (not #132)
+#46 := (f6 #41 #45)
+#47 := (f3 f9 #46)
+#128 := (= f1 #47)
+#141 := (not #128)
+#577 := [hypothesis]: #141
+#327 := (or #132 #128)
+#142 := (iff #132 #141)
+#53 := (= #52 f1)
+#48 := (= #47 f1)
+#54 := (iff #48 #53)
+#55 := (not #54)
+#145 := (iff #55 #142)
+#135 := (iff #128 #132)
+#138 := (not #135)
+#143 := (iff #138 #142)
+#144 := [rewrite]: #143
+#139 := (iff #55 #138)
+#136 := (iff #54 #135)
+#133 := (iff #53 #132)
+#134 := [rewrite]: #133
+#130 := (iff #48 #128)
+#131 := [rewrite]: #130
+#137 := [monotonicity #131 #134]: #136
+#140 := [monotonicity #137]: #139
+#146 := [trans #140 #144]: #145
+#127 := [asserted]: #55
+#149 := [mp #127 #146]: #142
+#239 := (not #142)
+#326 := (or #132 #128 #239)
+#240 := [def-axiom]: #326
+#241 := [unit-resolution #240 #149]: #327
+#571 := [unit-resolution #241 #577]: #132
+#562 := (or #328 #649)
+#651 := (iff #132 #649)
+#317 := (or #645 #651)
+#318 := [quant-inst #39 #49 #44]: #317
+#578 := [unit-resolution #318 #677]: #651
+#647 := (not #651)
+#289 := (or #647 #328 #649)
+#632 := [def-axiom]: #289
+#563 := [unit-resolution #632 #578]: #562
+#565 := [unit-resolution #563 #571]: #649
+#655 := (not #329)
+#595 := (or #645 #613)
+#618 := (or #334 #329)
+#622 := (iff #438 #618)
+#615 := (or #645 #622)
+#610 := (iff #615 #595)
+#617 := (iff #595 #595)
+#458 := [rewrite]: #617
+#614 := (iff #622 #613)
+#623 := (iff #618 #619)
+#612 := [rewrite]: #623
+#609 := [monotonicity #612]: #614
+#611 := [monotonicity #609]: #610
+#459 := [trans #611 #458]: #610
+#616 := [quant-inst #39 #42 #44]: #615
+#460 := [mp #616 #459]: #595
+#566 := [unit-resolution #460 #677]: #613
+#556 := (or #579 #591)
+#354 := (not #438)
+#638 := (or #438 #635)
+#627 := (not #638)
+#568 := (or #128 #627)
+#275 := (iff #128 #638)
+#280 := (or #645 #275)
+#636 := (or #635 #438)
+#637 := (iff #128 #636)
+#281 := (or #645 #637)
+#641 := (iff #281 #280)
+#630 := (iff #280 #280)
+#631 := [rewrite]: #630
+#640 := (iff #637 #275)
+#633 := (iff #636 #638)
+#639 := [rewrite]: #633
+#642 := [monotonicity #639]: #640
+#644 := [monotonicity #642]: #641
+#337 := [trans #644 #631]: #641
+#643 := [quant-inst #39 #40 #45]: #281
+#353 := [mp #643 #337]: #280
+#567 := [unit-resolution #353 #677]: #275
+#624 := (not #275)
+#628 := (or #624 #128 #627)
+#625 := [def-axiom]: #628
+#564 := [unit-resolution #625 #567]: #568
+#569 := [unit-resolution #564 #577]: #627
+#355 := (or #638 #354)
+#341 := [def-axiom]: #355
+#555 := [unit-resolution #341 #569]: #354
+#573 := (or #579 #438 #591)
+#570 := [def-axiom]: #573
+#558 := [unit-resolution #570 #555]: #556
+#559 := [unit-resolution #558 #566]: #591
+#602 := (or #619 #655)
+#496 := [def-axiom]: #602
+#560 := [unit-resolution #496 #559]: #655
+#304 := (or #646 #312 #329)
+#309 := [def-axiom]: #304
+#557 := [unit-resolution #309 #560 #565]: #312
+#356 := (not #635)
+#247 := (or #638 #356)
+#626 := [def-axiom]: #247
+#561 := [unit-resolution #626 #569]: #356
+#497 := (or #619 #603)
+#498 := [def-axiom]: #497
+#541 := [unit-resolution #498 #559]: #603
+#607 := (or #606 #334 #635)
+#601 := [def-axiom]: #607
+#542 := [unit-resolution #601 #541 #561]: #606
+#439 := (or #581 #652 #481)
+#440 := [def-axiom]: #439
+#544 := [unit-resolution #440 #542 #557 #576]: false
+#545 := [lemma #544]: #128
+#331 := (or #328 #141)
+#319 := (or #328 #141 #239)
+#330 := [def-axiom]: #319
+#259 := [unit-resolution #330 #149]: #331
+#546 := [unit-resolution #259 #545]: #328
+#547 := (or #132 #646)
+#305 := (or #647 #132 #646)
+#648 := [def-axiom]: #305
+#548 := [unit-resolution #648 #578]: #547
+#549 := [unit-resolution #548 #546]: #646
+#653 := (or #649 #652)
+#654 := [def-axiom]: #653
+#550 := [unit-resolution #654 #549]: #652
+#608 := (or #581 #312 #606)
+#437 := [def-axiom]: #608
+#551 := [unit-resolution #437 #550 #576]: #606
+#604 := (or #481 #603)
+#605 := [def-axiom]: #604
+#552 := [unit-resolution #605 #551]: #603
+#650 := (or #649 #655)
+#656 := [def-axiom]: #650
+#553 := [unit-resolution #656 #549]: #655
+#588 := (or #591 #329 #334)
+#592 := [def-axiom]: #588
+#543 := [unit-resolution #592 #553 #552]: #591
+#554 := (or #141 #638)
+#629 := (or #624 #141 #638)
+#338 := [def-axiom]: #629
+#532 := [unit-resolution #338 #567]: #554
+#533 := [unit-resolution #532 #545]: #638
+#599 := (or #481 #356)
+#600 := [def-axiom]: #599
+#535 := [unit-resolution #600 #551]: #356
+#349 := (or #627 #438 #635)
+#350 := [def-axiom]: #349
+#536 := [unit-resolution #350 #535 #533]: #438
+#572 := (or #579 #354 #619)
+#582 := [def-axiom]: #572
+#537 := [unit-resolution #582 #536 #543]: #579
+[unit-resolution #460 #677 #537]: false
+unsat
+95f37b9506ab4a9ecf6e4bca8da6ce25960cec6d 158 0
+#2 := false
+decl f3 :: (-> S2 S3 S1)
+decl f11 :: S3
+#42 := f11
+decl f9 :: S2
+#39 := f9
+#48 := (f3 f9 f11)
+decl f1 :: S1
+#4 := f1
+#132 := (= f1 #48)
+#186 := (not #132)
+decl f10 :: S3
+#40 := f10
+#46 := (f3 f9 f10)
+#129 := (= f1 #46)
+#185 := (not #129)
+#187 := (or #185 #186)
+#188 := (not #187)
+#329 := [hypothesis]: #188
+decl f6 :: (-> S4 S3 S3)
+decl f8 :: (-> S3 S4)
+#41 := (f8 f10)
+#43 := (f6 #41 f11)
+#44 := (f3 f9 #43)
+#125 := (= f1 #44)
+#144 := (not #125)
+#335 := (or #144 #187)
+#199 := (iff #125 #187)
+#135 := (and #129 #132)
+#145 := (iff #135 #144)
+#202 := (iff #145 #199)
+#194 := (iff #187 #125)
+#200 := (iff #194 #199)
+#201 := [rewrite]: #200
+#197 := (iff #145 #194)
+#191 := (iff #188 #144)
+#195 := (iff #191 #194)
+#196 := [rewrite]: #195
+#192 := (iff #145 #191)
+#189 := (iff #135 #188)
+#190 := [rewrite]: #189
+#193 := [monotonicity #190]: #192
+#198 := [trans #193 #196]: #197
+#203 := [trans #198 #201]: #202
+#49 := (= #48 f1)
+#47 := (= #46 f1)
+#50 := (and #47 #49)
+#45 := (= #44 f1)
+#51 := (iff #45 #50)
+#52 := (not #51)
+#148 := (iff #52 #145)
+#138 := (iff #125 #135)
+#141 := (not #138)
+#146 := (iff #141 #145)
+#147 := [rewrite]: #146
+#142 := (iff #52 #141)
+#139 := (iff #51 #138)
+#136 := (iff #50 #135)
+#133 := (iff #49 #132)
+#134 := [rewrite]: #133
+#130 := (iff #47 #129)
+#131 := [rewrite]: #130
+#137 := [monotonicity #131 #134]: #136
+#127 := (iff #45 #125)
+#128 := [rewrite]: #127
+#140 := [monotonicity #128 #137]: #139
+#143 := [monotonicity #140]: #142
+#149 := [trans #143 #147]: #148
+#124 := [asserted]: #52
+#152 := [mp #124 #149]: #145
+#204 := [mp #152 #203]: #199
+#342 := (not #199)
+#352 := (or #144 #187 #342)
+#356 := [def-axiom]: #352
+#672 := [unit-resolution #356 #204]: #335
+#461 := [unit-resolution #672 #329]: #144
+#328 := (or #125 #187)
+#674 := (iff #125 #188)
+#21 := (:var 0 S3)
+#19 := (:var 1 S3)
+#32 := (f8 #19)
+#33 := (f6 #32 #21)
+#18 := (:var 2 S2)
+#34 := (f3 #18 #33)
+#701 := (pattern #34)
+#27 := (f3 #18 #21)
+#98 := (= f1 #27)
+#177 := (not #98)
+#25 := (f3 #18 #19)
+#95 := (= f1 #25)
+#176 := (not #95)
+#160 := (or #176 #177)
+#161 := (not #160)
+#111 := (= f1 #34)
+#178 := (iff #111 #161)
+#702 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #701) #178)
+#181 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #178)
+#705 := (iff #181 #702)
+#703 := (iff #178 #178)
+#704 := [refl]: #703
+#706 := [quant-intro #704]: #705
+#115 := (and #95 #98)
+#118 := (iff #111 #115)
+#121 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #118)
+#182 := (iff #121 #181)
+#179 := (iff #118 #178)
+#162 := (iff #115 #161)
+#163 := [rewrite]: #162
+#180 := [monotonicity #163]: #179
+#183 := [quant-intro #180]: #182
+#158 := (~ #121 #121)
+#173 := (~ #118 #118)
+#174 := [refl]: #173
+#159 := [nnf-pos #174]: #158
+#28 := (= #27 f1)
+#26 := (= #25 f1)
+#36 := (and #26 #28)
+#35 := (= #34 f1)
+#37 := (iff #35 #36)
+#38 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #37)
+#122 := (iff #38 #121)
+#119 := (iff #37 #118)
+#116 := (iff #36 #115)
+#99 := (iff #28 #98)
+#100 := [rewrite]: #99
+#96 := (iff #26 #95)
+#97 := [rewrite]: #96
+#117 := [monotonicity #97 #100]: #116
+#113 := (iff #35 #111)
+#114 := [rewrite]: #113
+#120 := [monotonicity #114 #117]: #119
+#123 := [quant-intro #120]: #122
+#110 := [asserted]: #38
+#126 := [mp #110 #123]: #121
+#175 := [mp~ #126 #159]: #121
+#184 := [mp #175 #183]: #181
+#707 := [mp #184 #706]: #702
+#668 := (not #702)
+#340 := (or #668 #674)
+#341 := [quant-inst #39 #40 #42]: #340
+#670 := [unit-resolution #341 #707]: #674
+#675 := (not #674)
+#676 := (or #675 #125 #187)
+#677 := [def-axiom]: #676
+#671 := [unit-resolution #677 #670]: #328
+#312 := [unit-resolution #671 #461 #329]: false
+#655 := [lemma #312]: #187
+#282 := (or #125 #188)
+#353 := (or #125 #188 #342)
+#354 := [def-axiom]: #353
+#355 := [unit-resolution #354 #204]: #282
+#316 := [unit-resolution #355 #655]: #125
+#317 := (or #144 #188)
+#678 := (or #675 #144 #188)
+#673 := [def-axiom]: #678
+#318 := [unit-resolution #673 #670]: #317
+[unit-resolution #318 #316 #655]: false
+unsat
+453491eb61ee5da70153220378ac3f020b43cd23 147 0
+#2 := false
+decl f3 :: (-> S2 S3 S1)
+decl f4 :: S3
+#9 := f4
+decl f9 :: S2
+#39 := f9
+#225 := (f3 f9 f4)
+decl f1 :: S1
+#4 := f1
+#312 := (= f1 #225)
+#226 := (not #312)
+decl f10 :: S3
+#40 := f10
+#313 := (f3 f9 f10)
+#227 := (= f1 #313)
+#314 := (not #227)
+#305 := (or #314 #226)
+#316 := (not #305)
+decl f6 :: (-> S4 S3 S3)
+decl f8 :: (-> S3 S4)
+#41 := (f8 f10)
+#42 := (f6 #41 f4)
+#43 := (f3 f9 #42)
+#119 := (= f1 #43)
+#317 := (iff #119 #316)
+#21 := (:var 0 S3)
+#19 := (:var 1 S3)
+#32 := (f8 #19)
+#33 := (f6 #32 #21)
+#18 := (:var 2 S2)
+#34 := (f3 #18 #33)
+#664 := (pattern #34)
+#27 := (f3 #18 #21)
+#92 := (= f1 #27)
+#160 := (not #92)
+#25 := (f3 #18 #19)
+#89 := (= f1 #25)
+#159 := (not #89)
+#143 := (or #159 #160)
+#144 := (not #143)
+#105 := (= f1 #34)
+#161 := (iff #105 #144)
+#665 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #664) #161)
+#164 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #161)
+#668 := (iff #164 #665)
+#666 := (iff #161 #161)
+#667 := [refl]: #666
+#669 := [quant-intro #667]: #668
+#109 := (and #89 #92)
+#112 := (iff #105 #109)
+#115 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #112)
+#165 := (iff #115 #164)
+#162 := (iff #112 #161)
+#145 := (iff #109 #144)
+#146 := [rewrite]: #145
+#163 := [monotonicity #146]: #162
+#166 := [quant-intro #163]: #165
+#141 := (~ #115 #115)
+#156 := (~ #112 #112)
+#157 := [refl]: #156
+#142 := [nnf-pos #157]: #141
+#28 := (= #27 f1)
+#26 := (= #25 f1)
+#36 := (and #26 #28)
+#35 := (= #34 f1)
+#37 := (iff #35 #36)
+#38 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #37)
+#116 := (iff #38 #115)
+#113 := (iff #37 #112)
+#110 := (iff #36 #109)
+#93 := (iff #28 #92)
+#94 := [rewrite]: #93
+#90 := (iff #26 #89)
+#91 := [rewrite]: #90
+#111 := [monotonicity #91 #94]: #110
+#107 := (iff #35 #105)
+#108 := [rewrite]: #107
+#114 := [monotonicity #108 #111]: #113
+#117 := [quant-intro #114]: #116
+#104 := [asserted]: #38
+#120 := [mp #104 #117]: #115
+#158 := [mp~ #120 #142]: #115
+#167 := [mp #158 #166]: #164
+#670 := [mp #167 #669]: #665
+#315 := (not #665)
+#319 := (or #315 #317)
+#298 := [quant-inst #39 #40 #9]: #319
+#245 := [unit-resolution #298 #670]: #317
+#304 := (not #317)
+#318 := (or #304 #316)
+#44 := (= #43 f1)
+#45 := (not #44)
+#46 := (not #45)
+#131 := (iff #46 #119)
+#123 := (not #119)
+#126 := (not #123)
+#129 := (iff #126 #119)
+#130 := [rewrite]: #129
+#127 := (iff #46 #126)
+#124 := (iff #45 #123)
+#121 := (iff #44 #119)
+#122 := [rewrite]: #121
+#125 := [monotonicity #122]: #124
+#128 := [monotonicity #125]: #127
+#132 := [trans #128 #130]: #131
+#118 := [asserted]: #46
+#135 := [mp #118 #132]: #119
+#640 := (or #304 #123 #316)
+#641 := [def-axiom]: #640
+#634 := [unit-resolution #641 #135]: #318
+#275 := [unit-resolution #634 #245]: #316
+#292 := (or #305 #312)
+#424 := [def-axiom]: #292
+#618 := [unit-resolution #424 #275]: #312
+#8 := (:var 0 S2)
+#10 := (f3 #8 f4)
+#643 := (pattern #10)
+#67 := (= f1 #10)
+#70 := (not #67)
+#644 := (forall (vars (?v0 S2)) (:pat #643) #70)
+#73 := (forall (vars (?v0 S2)) #70)
+#647 := (iff #73 #644)
+#645 := (iff #70 #70)
+#646 := [refl]: #645
+#648 := [quant-intro #646]: #647
+#149 := (~ #73 #73)
+#147 := (~ #70 #70)
+#148 := [refl]: #147
+#150 := [nnf-pos #148]: #149
+#11 := (= #10 f1)
+#12 := (not #11)
+#13 := (forall (vars (?v0 S2)) #12)
+#74 := (iff #13 #73)
+#71 := (iff #12 #70)
+#68 := (iff #11 #67)
+#69 := [rewrite]: #68
+#72 := [monotonicity #69]: #71
+#75 := [quant-intro #72]: #74
+#66 := [asserted]: #13
+#78 := [mp #66 #75]: #73
+#134 := [mp~ #78 #150]: #73
+#649 := [mp #134 #648]: #644
+#295 := (not #644)
+#633 := (or #295 #226)
+#291 := [quant-inst #39]: #633
+[unit-resolution #291 #649 #618]: false
+unsat
+6f8829ccc8ddcc6f60b1e61de2ed840042d23d2c 171 0
+#2 := false
+decl f3 :: (-> S2 S3 S1)
+decl f10 :: S3
+#40 := f10
+decl f9 :: S2
+#39 := f9
+#45 := (f3 f9 f10)
+decl f1 :: S1
+#4 := f1
+#125 := (= f1 #45)
+#321 := (not #125)
+decl f6 :: (-> S4 S3 S3)
+decl f5 :: S3
+#14 := f5
+decl f8 :: (-> S3 S4)
+#41 := (f8 f10)
+#42 := (f6 #41 f5)
+#43 := (f3 f9 #42)
+#121 := (= f1 #43)
+#325 := (f3 f9 f5)
+#322 := (= f1 #325)
+#326 := (not #322)
+#299 := [hypothesis]: #326
+#8 := (:var 0 S2)
+#15 := (f3 #8 f5)
+#657 := (pattern #15)
+#79 := (= f1 #15)
+#658 := (forall (vars (?v0 S2)) (:pat #657) #79)
+#83 := (forall (vars (?v0 S2)) #79)
+#661 := (iff #83 #658)
+#659 := (iff #79 #79)
+#660 := [refl]: #659
+#662 := [quant-intro #660]: #661
+#144 := (~ #83 #83)
+#143 := (~ #79 #79)
+#158 := [refl]: #143
+#145 := [nnf-pos #158]: #144
+#16 := (= #15 f1)
+#17 := (forall (vars (?v0 S2)) #16)
+#84 := (iff #17 #83)
+#81 := (iff #16 #79)
+#82 := [rewrite]: #81
+#85 := [quant-intro #82]: #84
+#78 := [asserted]: #17
+#88 := [mp #78 #85]: #83
+#159 := [mp~ #88 #145]: #83
+#663 := [mp #159 #662]: #658
+#287 := (not #658)
+#288 := (or #287 #322)
+#289 := [quant-inst #39]: #288
+#431 := [unit-resolution #289 #663 #299]: false
+#627 := [lemma #431]: #322
+#134 := (not #121)
+#628 := [hypothesis]: #134
+#320 := (or #125 #121)
+#135 := (iff #125 #134)
+#46 := (= #45 f1)
+#44 := (= #43 f1)
+#47 := (iff #44 #46)
+#48 := (not #47)
+#138 := (iff #48 #135)
+#128 := (iff #121 #125)
+#131 := (not #128)
+#136 := (iff #131 #135)
+#137 := [rewrite]: #136
+#132 := (iff #48 #131)
+#129 := (iff #47 #128)
+#126 := (iff #46 #125)
+#127 := [rewrite]: #126
+#123 := (iff #44 #121)
+#124 := [rewrite]: #123
+#130 := [monotonicity #124 #127]: #129
+#133 := [monotonicity #130]: #132
+#139 := [trans #133 #137]: #138
+#120 := [asserted]: #48
+#142 := [mp #120 #139]: #135
+#232 := (not #135)
+#319 := (or #125 #121 #232)
+#233 := [def-axiom]: #319
+#234 := [unit-resolution #233 #142]: #320
+#629 := [unit-resolution #234 #628]: #125
+#305 := (or #321 #326)
+#631 := (or #121 #305)
+#642 := (not #305)
+#644 := (iff #121 #642)
+#21 := (:var 0 S3)
+#19 := (:var 1 S3)
+#32 := (f8 #19)
+#33 := (f6 #32 #21)
+#18 := (:var 2 S2)
+#34 := (f3 #18 #33)
+#671 := (pattern #34)
+#27 := (f3 #18 #21)
+#94 := (= f1 #27)
+#167 := (not #94)
+#25 := (f3 #18 #19)
+#91 := (= f1 #25)
+#166 := (not #91)
+#150 := (or #166 #167)
+#151 := (not #150)
+#107 := (= f1 #34)
+#168 := (iff #107 #151)
+#672 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #671) #168)
+#171 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #168)
+#675 := (iff #171 #672)
+#673 := (iff #168 #168)
+#674 := [refl]: #673
+#676 := [quant-intro #674]: #675
+#111 := (and #91 #94)
+#114 := (iff #107 #111)
+#117 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #114)
+#172 := (iff #117 #171)
+#169 := (iff #114 #168)
+#152 := (iff #111 #151)
+#153 := [rewrite]: #152
+#170 := [monotonicity #153]: #169
+#173 := [quant-intro #170]: #172
+#148 := (~ #117 #117)
+#163 := (~ #114 #114)
+#164 := [refl]: #163
+#149 := [nnf-pos #164]: #148
+#28 := (= #27 f1)
+#26 := (= #25 f1)
+#36 := (and #26 #28)
+#35 := (= #34 f1)
+#37 := (iff #35 #36)
+#38 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #37)
+#118 := (iff #38 #117)
+#115 := (iff #37 #114)
+#112 := (iff #36 #111)
+#95 := (iff #28 #94)
+#96 := [rewrite]: #95
+#92 := (iff #26 #91)
+#93 := [rewrite]: #92
+#113 := [monotonicity #93 #96]: #112
+#109 := (iff #35 #107)
+#110 := [rewrite]: #109
+#116 := [monotonicity #110 #113]: #115
+#119 := [quant-intro #116]: #118
+#106 := [asserted]: #38
+#122 := [mp #106 #119]: #117
+#165 := [mp~ #122 #149]: #117
+#174 := [mp #165 #173]: #171
+#677 := [mp #174 #676]: #672
+#638 := (not #672)
+#310 := (or #638 #644)
+#311 := [quant-inst #39 #40 #14]: #310
+#630 := [unit-resolution #311 #677]: #644
+#639 := (not #644)
+#297 := (or #639 #121 #305)
+#302 := [def-axiom]: #297
+#626 := [unit-resolution #302 #630]: #631
+#632 := [unit-resolution #626 #628]: #305
+#643 := (or #642 #321 #326)
+#649 := [def-axiom]: #643
+#268 := [unit-resolution #649 #632 #629 #627]: false
+#633 := [lemma #268]: #121
+#324 := (or #321 #134)
+#312 := (or #321 #134 #232)
+#323 := [def-axiom]: #312
+#252 := [unit-resolution #323 #142]: #324
+#635 := [unit-resolution #252 #633]: #321
+#273 := (or #134 #642)
+#640 := (or #639 #134 #642)
+#298 := [def-axiom]: #640
+#274 := [unit-resolution #298 #630]: #273
+#636 := [unit-resolution #274 #633]: #642
+#645 := (or #305 #125)
+#646 := [def-axiom]: #645
+[unit-resolution #646 #636 #635]: false
+unsat
+7fb5c9e3c94a5bd9f761d4854f2678f455553edf 171 0
+#2 := false
+decl f3 :: (-> S2 S3 S1)
+decl f6 :: (-> S4 S3 S3)
+decl f10 :: S3
+#40 := f10
+decl f8 :: (-> S3 S4)
+decl f11 :: S3
+#42 := f11
+#46 := (f8 f11)
+#47 := (f6 #46 f10)
+decl f9 :: S2
+#39 := f9
+#48 := (f3 f9 #47)
+decl f1 :: S1
+#4 := f1
+#128 := (= f1 #48)
+#324 := (not #128)
+#41 := (f8 f10)
+#43 := (f6 #41 f11)
+#44 := (f3 f9 #43)
+#124 := (= f1 #44)
+#137 := (not #124)
+#626 := [hypothesis]: #137
+#323 := (or #128 #124)
+#138 := (iff #128 #137)
+#49 := (= #48 f1)
+#45 := (= #44 f1)
+#50 := (iff #45 #49)
+#51 := (not #50)
+#141 := (iff #51 #138)
+#131 := (iff #124 #128)
+#134 := (not #131)
+#139 := (iff #134 #138)
+#140 := [rewrite]: #139
+#135 := (iff #51 #134)
+#132 := (iff #50 #131)
+#129 := (iff #49 #128)
+#130 := [rewrite]: #129
+#126 := (iff #45 #124)
+#127 := [rewrite]: #126
+#133 := [monotonicity #127 #130]: #132
+#136 := [monotonicity #133]: #135
+#142 := [trans #136 #140]: #141
+#123 := [asserted]: #51
+#145 := [mp #123 #142]: #138
+#235 := (not #138)
+#322 := (or #128 #124 #235)
+#236 := [def-axiom]: #322
+#237 := [unit-resolution #236 #145]: #323
+#627 := [unit-resolution #237 #626]: #128
+#308 := (f3 f9 f11)
+#645 := (= f1 #308)
+#647 := (not #645)
+#328 := (f3 f9 f10)
+#325 := (= f1 #328)
+#329 := (not #325)
+#313 := (or #329 #647)
+#624 := (or #124 #313)
+#649 := (not #313)
+#640 := (iff #124 #649)
+#21 := (:var 0 S3)
+#19 := (:var 1 S3)
+#32 := (f8 #19)
+#33 := (f6 #32 #21)
+#18 := (:var 2 S2)
+#34 := (f3 #18 #33)
+#674 := (pattern #34)
+#27 := (f3 #18 #21)
+#97 := (= f1 #27)
+#170 := (not #97)
+#25 := (f3 #18 #19)
+#94 := (= f1 #25)
+#169 := (not #94)
+#153 := (or #169 #170)
+#154 := (not #153)
+#110 := (= f1 #34)
+#171 := (iff #110 #154)
+#675 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #674) #171)
+#174 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #171)
+#678 := (iff #174 #675)
+#676 := (iff #171 #171)
+#677 := [refl]: #676
+#679 := [quant-intro #677]: #678
+#114 := (and #94 #97)
+#117 := (iff #110 #114)
+#120 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #117)
+#175 := (iff #120 #174)
+#172 := (iff #117 #171)
+#155 := (iff #114 #154)
+#156 := [rewrite]: #155
+#173 := [monotonicity #156]: #172
+#176 := [quant-intro #173]: #175
+#151 := (~ #120 #120)
+#166 := (~ #117 #117)
+#167 := [refl]: #166
+#152 := [nnf-pos #167]: #151
+#28 := (= #27 f1)
+#26 := (= #25 f1)
+#36 := (and #26 #28)
+#35 := (= #34 f1)
+#37 := (iff #35 #36)
+#38 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #37)
+#121 := (iff #38 #120)
+#118 := (iff #37 #117)
+#115 := (iff #36 #114)
+#98 := (iff #28 #97)
+#99 := [rewrite]: #98
+#95 := (iff #26 #94)
+#96 := [rewrite]: #95
+#116 := [monotonicity #96 #99]: #115
+#112 := (iff #35 #110)
+#113 := [rewrite]: #112
+#119 := [monotonicity #113 #116]: #118
+#122 := [quant-intro #119]: #121
+#109 := [asserted]: #38
+#125 := [mp #109 #122]: #120
+#168 := [mp~ #125 #152]: #120
+#177 := [mp #168 #176]: #174
+#680 := [mp #177 #679]: #675
+#300 := (not #675)
+#333 := (or #300 #640)
+#349 := [quant-inst #39 #40 #42]: #333
+#620 := [unit-resolution #349 #680]: #640
+#350 := (not #640)
+#351 := (or #350 #124 #313)
+#337 := [def-axiom]: #351
+#621 := [unit-resolution #337 #620]: #624
+#625 := [unit-resolution #621 #626]: #313
+#335 := (or #324 #649)
+#646 := (iff #128 #649)
+#305 := (or #300 #646)
+#302 := (or #647 #329)
+#434 := (not #302)
+#641 := (iff #128 #434)
+#643 := (or #300 #641)
+#644 := (iff #643 #305)
+#628 := (iff #305 #305)
+#289 := [rewrite]: #628
+#652 := (iff #641 #646)
+#650 := (iff #434 #649)
+#314 := (iff #302 #313)
+#648 := [rewrite]: #314
+#651 := [monotonicity #648]: #650
+#642 := [monotonicity #651]: #652
+#285 := [monotonicity #642]: #644
+#290 := [trans #285 #289]: #644
+#301 := [quant-inst #39 #42 #40]: #643
+#291 := [mp #301 #290]: #305
+#334 := [unit-resolution #291 #680]: #646
+#629 := (not #646)
+#636 := (or #629 #324 #649)
+#638 := [def-axiom]: #636
+#336 := [unit-resolution #638 #334]: #335
+#338 := [unit-resolution #336 #625 #627]: false
+#616 := [lemma #338]: #124
+#327 := (or #324 #137)
+#315 := (or #324 #137 #235)
+#326 := [def-axiom]: #315
+#255 := [unit-resolution #326 #145]: #327
+#617 := [unit-resolution #255 #616]: #324
+#330 := (or #137 #649)
+#352 := (or #350 #137 #649)
+#243 := [def-axiom]: #352
+#614 := [unit-resolution #243 #620]: #330
+#618 := [unit-resolution #614 #616]: #649
+#615 := (or #128 #313)
+#635 := (or #629 #128 #313)
+#271 := [def-axiom]: #635
+#619 := [unit-resolution #271 #334]: #615
+[unit-resolution #619 #618 #617]: false
+unsat
+894705c4ef9337c77fce76fc097ee92668a964e4 147 0
+#2 := false
+decl f3 :: (-> S2 S3 S1)
+decl f6 :: (-> S4 S3 S3)
+decl f10 :: S3
+#40 := f10
+decl f8 :: (-> S3 S4)
+#41 := (f8 f10)
+#42 := (f6 #41 f10)
+decl f9 :: S2
+#39 := f9
+#43 := (f3 f9 #42)
+decl f1 :: S1
+#4 := f1
+#121 := (= f1 #43)
+#134 := (not #121)
+#630 := [hypothesis]: #134
+#45 := (f3 f9 f10)
+#125 := (= f1 #45)
+#320 := (or #125 #121)
+#135 := (iff #125 #134)
+#46 := (= #45 f1)
+#44 := (= #43 f1)
+#47 := (iff #44 #46)
+#48 := (not #47)
+#138 := (iff #48 #135)
+#128 := (iff #121 #125)
+#131 := (not #128)
+#136 := (iff #131 #135)
+#137 := [rewrite]: #136
+#132 := (iff #48 #131)
+#129 := (iff #47 #128)
+#126 := (iff #46 #125)
+#127 := [rewrite]: #126
+#123 := (iff #44 #121)
+#124 := [rewrite]: #123
+#130 := [monotonicity #124 #127]: #129
+#133 := [monotonicity #130]: #132
+#139 := [trans #133 #137]: #138
+#120 := [asserted]: #48
+#142 := [mp #120 #139]: #135
+#232 := (not #135)
+#319 := (or #125 #121 #232)
+#233 := [def-axiom]: #319
+#234 := [unit-resolution #233 #142]: #320
+#631 := [unit-resolution #234 #630]: #125
+#321 := (not #125)
+#632 := (or #121 #321)
+#21 := (:var 0 S3)
+#19 := (:var 1 S3)
+#32 := (f8 #19)
+#33 := (f6 #32 #21)
+#18 := (:var 2 S2)
+#34 := (f3 #18 #33)
+#671 := (pattern #34)
+#27 := (f3 #18 #21)
+#94 := (= f1 #27)
+#167 := (not #94)
+#25 := (f3 #18 #19)
+#91 := (= f1 #25)
+#166 := (not #91)
+#150 := (or #166 #167)
+#151 := (not #150)
+#107 := (= f1 #34)
+#168 := (iff #107 #151)
+#672 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #671) #168)
+#171 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #168)
+#675 := (iff #171 #672)
+#673 := (iff #168 #168)
+#674 := [refl]: #673
+#676 := [quant-intro #674]: #675
+#111 := (and #91 #94)
+#114 := (iff #107 #111)
+#117 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #114)
+#172 := (iff #117 #171)
+#169 := (iff #114 #168)
+#152 := (iff #111 #151)
+#153 := [rewrite]: #152
+#170 := [monotonicity #153]: #169
+#173 := [quant-intro #170]: #172
+#148 := (~ #117 #117)
+#163 := (~ #114 #114)
+#164 := [refl]: #163
+#149 := [nnf-pos #164]: #148
+#28 := (= #27 f1)
+#26 := (= #25 f1)
+#36 := (and #26 #28)
+#35 := (= #34 f1)
+#37 := (iff #35 #36)
+#38 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #37)
+#118 := (iff #38 #117)
+#115 := (iff #37 #114)
+#112 := (iff #36 #111)
+#95 := (iff #28 #94)
+#96 := [rewrite]: #95
+#92 := (iff #26 #91)
+#93 := [rewrite]: #92
+#113 := [monotonicity #93 #96]: #112
+#109 := (iff #35 #107)
+#110 := [rewrite]: #109
+#116 := [monotonicity #110 #113]: #115
+#119 := [quant-intro #116]: #118
+#106 := [asserted]: #38
+#122 := [mp #106 #119]: #117
+#165 := [mp~ #122 #149]: #117
+#174 := [mp #165 #173]: #171
+#677 := [mp #174 #676]: #672
+#648 := (not #672)
+#643 := (or #648 #128)
+#325 := (or #321 #321)
+#322 := (not #325)
+#326 := (iff #121 #322)
+#649 := (or #648 #326)
+#297 := (iff #649 #643)
+#640 := (iff #643 #643)
+#298 := [rewrite]: #640
+#646 := (iff #326 #128)
+#311 := (iff #322 #125)
+#644 := (not #321)
+#638 := (iff #644 #125)
+#310 := [rewrite]: #638
+#299 := (iff #322 #644)
+#305 := (iff #325 #321)
+#642 := [rewrite]: #305
+#431 := [monotonicity #642]: #299
+#645 := [trans #431 #310]: #311
+#647 := [monotonicity #645]: #646
+#302 := [monotonicity #647]: #297
+#641 := [trans #302 #298]: #297
+#639 := [quant-inst #39 #40 #40]: #649
+#282 := [mp #639 #641]: #643
+#626 := [unit-resolution #282 #677]: #128
+#625 := (or #131 #121 #321)
+#286 := [def-axiom]: #625
+#268 := [unit-resolution #286 #626]: #632
+#633 := [unit-resolution #268 #631 #630]: false
+#635 := [lemma #633]: #121
+#324 := (or #321 #134)
+#312 := (or #321 #134 #232)
+#323 := [def-axiom]: #312
+#252 := [unit-resolution #323 #142]: #324
+#273 := [unit-resolution #252 #635]: #321
+#274 := (or #134 #125)
+#287 := (or #131 #134 #125)
+#288 := [def-axiom]: #287
+#636 := [unit-resolution #288 #626]: #274
+[unit-resolution #636 #273 #635]: false
+unsat
+6bc0dc7cf7d78f36cf0c61d5f399a6c019b36218 285 0
+#2 := false
+decl f3 :: (-> S2 S3 S1)
+decl f6 :: (-> S4 S3 S3)
+decl f11 :: S3
+#42 := f11
+decl f8 :: (-> S3 S4)
+decl f10 :: S3
+#40 := f10
+#41 := (f8 f10)
+#49 := (f6 #41 f11)
+decl f9 :: S2
+#39 := f9
+#312 := (f3 f9 #49)
+decl f1 :: S1
+#4 := f1
+#649 := (= f1 #312)
+#247 := (f3 f9 f11)
+#626 := (= f1 #247)
+#623 := (not #626)
+#337 := (f3 f9 f10)
+#353 := (= f1 #337)
+#354 := (not #353)
+#612 := (or #354 #623)
+#613 := (not #612)
+#609 := (iff #613 #649)
+#580 := (not #609)
+decl f12 :: S3
+#44 := f12
+#332 := (f3 f9 f12)
+#329 := (= f1 #332)
+#333 := (not #329)
+#482 := (or #333 #623)
+#491 := (not #482)
+#43 := (f8 f11)
+#45 := (f6 #43 f12)
+#644 := (f3 f9 #45)
+#630 := (= f1 #644)
+#492 := (iff #491 #630)
+#585 := (not #492)
+#565 := [hypothesis]: #585
+#21 := (:var 0 S3)
+#19 := (:var 1 S3)
+#32 := (f8 #19)
+#33 := (f6 #32 #21)
+#18 := (:var 2 S2)
+#34 := (f3 #18 #33)
+#678 := (pattern #34)
+#27 := (f3 #18 #21)
+#101 := (= f1 #27)
+#174 := (not #101)
+#25 := (f3 #18 #19)
+#98 := (= f1 #25)
+#173 := (not #98)
+#157 := (or #173 #174)
+#158 := (not #157)
+#114 := (= f1 #34)
+#175 := (iff #114 #158)
+#679 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #678) #175)
+#178 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #175)
+#682 := (iff #178 #679)
+#680 := (iff #175 #175)
+#681 := [refl]: #680
+#683 := [quant-intro #681]: #682
+#118 := (and #98 #101)
+#121 := (iff #114 #118)
+#124 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #121)
+#179 := (iff #124 #178)
+#176 := (iff #121 #175)
+#159 := (iff #118 #158)
+#160 := [rewrite]: #159
+#177 := [monotonicity #160]: #176
+#180 := [quant-intro #177]: #179
+#155 := (~ #124 #124)
+#170 := (~ #121 #121)
+#171 := [refl]: #170
+#156 := [nnf-pos #171]: #155
+#28 := (= #27 f1)
+#26 := (= #25 f1)
+#36 := (and #26 #28)
+#35 := (= #34 f1)
+#37 := (iff #35 #36)
+#38 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #37)
+#125 := (iff #38 #124)
+#122 := (iff #37 #121)
+#119 := (iff #36 #118)
+#102 := (iff #28 #101)
+#103 := [rewrite]: #102
+#99 := (iff #26 #98)
+#100 := [rewrite]: #99
+#120 := [monotonicity #100 #103]: #119
+#116 := (iff #35 #114)
+#117 := [rewrite]: #116
+#123 := [monotonicity #117 #120]: #122
+#126 := [quant-intro #123]: #125
+#113 := [asserted]: #38
+#129 := [mp #113 #126]: #124
+#172 := [mp~ #129 #156]: #124
+#181 := [mp #172 #180]: #178
+#684 := [mp #181 #683]: #679
+#304 := (not #679)
+#496 := (or #304 #492)
+#598 := (or #623 #333)
+#480 := (not #598)
+#481 := (iff #630 #480)
+#497 := (or #304 #481)
+#591 := (iff #497 #496)
+#592 := (iff #496 #496)
+#579 := [rewrite]: #592
+#494 := (iff #481 #492)
+#590 := (iff #630 #491)
+#493 := (iff #590 #492)
+#486 := [rewrite]: #493
+#475 := (iff #481 #590)
+#586 := (iff #480 #491)
+#441 := (iff #598 #482)
+#589 := [rewrite]: #441
+#587 := [monotonicity #589]: #586
+#490 := [monotonicity #587]: #475
+#495 := [trans #490 #486]: #494
+#588 := [monotonicity #495]: #591
+#581 := [trans #588 #579]: #591
+#498 := [quant-inst #39 #42 #44]: #497
+#573 := [mp #498 #581]: #496
+#566 := [unit-resolution #573 #684 #565]: false
+#567 := [lemma #566]: #492
+#631 := (not #630)
+#355 := (or #354 #631)
+#341 := (not #355)
+#46 := (f6 #41 #45)
+#47 := (f3 f9 #46)
+#128 := (= f1 #47)
+#141 := (not #128)
+#568 := [hypothesis]: #141
+#569 := (or #128 #355)
+#356 := (iff #128 #341)
+#627 := (or #304 #356)
+#349 := [quant-inst #39 #40 #45]: #627
+#564 := [unit-resolution #349 #684]: #356
+#339 := (not #356)
+#340 := (or #339 #128 #355)
+#342 := [def-axiom]: #340
+#555 := [unit-resolution #342 #564]: #569
+#556 := [unit-resolution #555 #568]: #355
+#595 := (or #304 #609)
+#614 := (iff #649 #613)
+#611 := (or #304 #614)
+#616 := (iff #611 #595)
+#459 := (iff #595 #595)
+#460 := [rewrite]: #459
+#610 := (iff #614 #609)
+#615 := [rewrite]: #610
+#458 := [monotonicity #615]: #616
+#602 := [trans #458 #460]: #616
+#617 := [quant-inst #39 #40 #42]: #611
+#603 := [mp #617 #602]: #595
+#558 := [unit-resolution #603 #684]: #609
+#544 := (or #580 #613)
+#651 := (not #649)
+#317 := (or #333 #651)
+#653 := (not #317)
+#50 := (f8 #49)
+#51 := (f6 #50 f12)
+#52 := (f3 f9 #51)
+#132 := (= f1 #52)
+#327 := (or #132 #128)
+#142 := (iff #132 #141)
+#53 := (= #52 f1)
+#48 := (= #47 f1)
+#54 := (iff #48 #53)
+#55 := (not #54)
+#145 := (iff #55 #142)
+#135 := (iff #128 #132)
+#138 := (not #135)
+#143 := (iff #138 #142)
+#144 := [rewrite]: #143
+#139 := (iff #55 #138)
+#136 := (iff #54 #135)
+#133 := (iff #53 #132)
+#134 := [rewrite]: #133
+#130 := (iff #48 #128)
+#131 := [rewrite]: #130
+#137 := [monotonicity #131 #134]: #136
+#140 := [monotonicity #137]: #139
+#146 := [trans #140 #144]: #145
+#127 := [asserted]: #55
+#149 := [mp #127 #146]: #142
+#239 := (not #142)
+#326 := (or #132 #128 #239)
+#240 := [def-axiom]: #326
+#241 := [unit-resolution #240 #149]: #327
+#559 := [unit-resolution #241 #568]: #132
+#328 := (not #132)
+#557 := (or #328 #653)
+#650 := (iff #132 #653)
+#309 := (or #304 #650)
+#306 := (or #651 #333)
+#438 := (not #306)
+#645 := (iff #132 #438)
+#647 := (or #304 #645)
+#648 := (iff #647 #309)
+#632 := (iff #309 #309)
+#293 := [rewrite]: #632
+#656 := (iff #645 #650)
+#654 := (iff #438 #653)
+#318 := (iff #306 #317)
+#652 := [rewrite]: #318
+#655 := [monotonicity #652]: #654
+#646 := [monotonicity #655]: #656
+#289 := [monotonicity #646]: #648
+#294 := [trans #289 #293]: #648
+#305 := [quant-inst #39 #49 #44]: #647
+#295 := [mp #305 #294]: #309
+#560 := [unit-resolution #295 #684]: #650
+#633 := (not #650)
+#640 := (or #633 #328 #653)
+#642 := [def-axiom]: #640
+#561 := [unit-resolution #642 #560]: #557
+#541 := [unit-resolution #561 #559]: #653
+#635 := (or #317 #649)
+#636 := [def-axiom]: #635
+#542 := [unit-resolution #636 #541]: #649
+#574 := (or #580 #613 #651)
+#575 := [def-axiom]: #574
+#545 := [unit-resolution #575 #542]: #544
+#546 := [unit-resolution #545 #558]: #613
+#604 := (or #612 #353)
+#570 := [def-axiom]: #604
+#547 := [unit-resolution #570 #546]: #353
+#629 := (or #341 #354 #631)
+#338 := [def-axiom]: #629
+#548 := [unit-resolution #338 #547 #556]: #631
+#296 := (or #317 #329)
+#634 := [def-axiom]: #296
+#549 := [unit-resolution #634 #541]: #329
+#572 := (or #612 #626)
+#582 := [def-axiom]: #572
+#550 := [unit-resolution #582 #546]: #626
+#607 := (or #491 #333 #623)
+#601 := [def-axiom]: #607
+#551 := [unit-resolution #601 #550 #549]: #491
+#439 := (or #585 #482 #630)
+#440 := [def-axiom]: #439
+#552 := [unit-resolution #440 #551 #548 #567]: false
+#553 := [lemma #552]: #128
+#543 := (or #141 #341)
+#620 := (or #339 #141 #341)
+#621 := [def-axiom]: #620
+#554 := [unit-resolution #621 #564]: #543
+#532 := [unit-resolution #554 #553]: #341
+#628 := (or #355 #630)
+#625 := [def-axiom]: #628
+#533 := [unit-resolution #625 #532]: #630
+#608 := (or #585 #491 #631)
+#437 := [def-axiom]: #608
+#535 := [unit-resolution #437 #533 #567]: #491
+#600 := (or #482 #626)
+#606 := [def-axiom]: #600
+#536 := [unit-resolution #606 #535]: #626
+#350 := (or #355 #353)
+#624 := [def-axiom]: #350
+#537 := [unit-resolution #624 #532]: #353
+#583 := (or #613 #354 #623)
+#584 := [def-axiom]: #583
+#538 := [unit-resolution #584 #537 #536]: #613
+#331 := (or #328 #141)
+#319 := (or #328 #141 #239)
+#330 := [def-axiom]: #319
+#259 := [unit-resolution #330 #149]: #331
+#539 := [unit-resolution #259 #553]: #328
+#534 := (or #132 #317)
+#639 := (or #633 #132 #317)
+#275 := [def-axiom]: #639
+#540 := [unit-resolution #275 #560]: #534
+#526 := [unit-resolution #540 #539]: #317
+#605 := (or #482 #329)
+#599 := [def-axiom]: #605
+#522 := [unit-resolution #599 #535]: #329
+#637 := (or #653 #333 #651)
+#638 := [def-axiom]: #637
+#523 := [unit-resolution #638 #522 #526]: #651
+#576 := (or #580 #612 #649)
+#577 := [def-axiom]: #576
+#524 := [unit-resolution #577 #523 #538]: #580
+[unit-resolution #603 #684 #524]: false
+unsat
+a7bc4cb1c082efb5c0f6c878be007f36211e0adf 20 0
+#2 := false
+decl f12 :: (-> S3 S3)
+decl f4 :: S3
+#8 := f4
+#48 := (f12 f4)
+#49 := (= #48 #48)
+#50 := (not #49)
+#145 := (iff #50 false)
+#1 := true
+#140 := (not true)
+#143 := (iff #140 false)
+#144 := [rewrite]: #143
+#141 := (iff #50 #140)
+#137 := (iff #49 true)
+#139 := [rewrite]: #137
+#142 := [monotonicity #139]: #141
+#146 := [trans #142 #144]: #145
+#136 := [asserted]: #50
+[mp #136 #146]: false
+unsat
diff -r 1a5811bfe837 -r 1db6baa40b0e src/HOL/SMT_Examples/SMT_Tests.thy
--- a/src/HOL/SMT_Examples/SMT_Tests.thy	Wed Sep 14 06:49:24 2011 +0200
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Wed Sep 14 09:46:59 2011 +0200
@@ -937,32 +937,26 @@
 
 section {* Sets *}
 
-lemma smt_sets:
-  "\<not>({} x)"
-  "UNIV x"
-  "(A \<union> B) x = (A x \<or> B x)"
-  "(A \<inter> B) x = (A x \<and> B x)"
-  by auto
+lemma Empty: "x \<notin> {}" by simp
+
+lemmas smt_sets = Empty UNIV_I Un_iff Int_iff
 
 lemma
-  "x \<in> P = P x"
-  "x \<in> {x. P x} = P x"
   "x \<notin> {}"
   "x \<in> UNIV"
-  "x \<in> P \<union> Q = (P x \<or> Q x)"
-  "x \<in> P \<union> {} = P x"
+  "x \<in> A \<union> B \<longleftrightarrow> x \<in> A \<or> x \<in> B"
+  "x \<in> P \<union> {} \<longleftrightarrow> x \<in> P"
   "x \<in> P \<union> UNIV"
-  "(x \<in> P \<union> Q) = (x \<in> Q \<union> P)"
-  "(x \<in> P \<union> P) = (x \<in> P)"
-  "(x \<in> P \<union> (Q \<union> R)) = (x \<in> (P \<union> Q) \<union> R)"
-  "(x \<in> P \<inter> Q) = (P x \<and> Q x)"
+  "x \<in> P \<union> Q \<longleftrightarrow> x \<in> Q \<union> P"
+  "x \<in> P \<union> P \<longleftrightarrow> x \<in> P"
+  "x \<in> P \<union> (Q \<union> R) \<longleftrightarrow> x \<in> (P \<union> Q) \<union> R"
+  "x \<in> A \<inter> B \<longleftrightarrow> x \<in> A \<and> x \<in> B"
   "x \<notin> P \<inter> {}"
-  "(x \<in> P \<inter> UNIV) = (x \<in> P)"
-  "(x \<in> P \<inter> Q) = (x \<in> Q \<inter> P)"
-  "(x \<in> P \<inter> P) = (x \<in> P)"
-  "(x \<in> P \<inter> (Q \<inter> R)) = (x \<in> (P \<inter> Q) \<inter> R)"
-  "{x. P x} = {y. P y}"
-  unfolding mem_def Collect_def
+  "x \<in> P \<inter> UNIV \<longleftrightarrow> x \<in> P"
+  "x \<in> P \<inter> Q \<longleftrightarrow> x \<in> Q \<inter> P"
+  "x \<in> P \<inter> P \<longleftrightarrow> x \<in> P"
+  "x \<in> P \<inter> (Q \<inter> R) \<longleftrightarrow> x \<in> (P \<inter> Q) \<inter> R"
+  "{x. x \<in> P} = {y. y \<in> P}"
   by (smt smt_sets)+
 
 end