# HG changeset patch
# User haftmann
# Date 1324798953 -3600
# Node ID 5de99514fd07a75ced0d8c0ed8f8962e9dc0c368
# Parent  f6f582a5c5fd01bc1b478bcc020e6ec5afd77428
updated certificate

diff -r f6f582a5c5fd -r 5de99514fd07 src/HOL/SMT_Examples/SMT_Tests.certs
--- a/src/HOL/SMT_Examples/SMT_Tests.certs	Sat Dec 24 16:14:59 2011 +0100
+++ b/src/HOL/SMT_Examples/SMT_Tests.certs	Sun Dec 25 08:42:33 2011 +0100
@@ -62737,3 +62737,4421 @@
 #136 := [asserted]: #50
 [mp #136 #146]: false
 unsat
+eac8197a82f6b3a5c2024430d69641bb761b0abc 60 0
+#2 := false
+decl f3 :: (-> S2 S3 S1)
+decl f4 :: S3
+#9 := f4
+decl f10 :: S2
+#41 := f10
+#42 := (f3 f10 f4)
+decl f1 :: S1
+#4 := f1
+#118 := (= f1 #42)
+#43 := (= #42 f1)
+#44 := (not #43)
+#45 := (not #44)
+#130 := (iff #45 #118)
+#122 := (not #118)
+#125 := (not #122)
+#128 := (iff #125 #118)
+#129 := [rewrite]: #128
+#126 := (iff #45 #125)
+#123 := (iff #44 #122)
+#120 := (iff #43 #118)
+#121 := [rewrite]: #120
+#124 := [monotonicity #121]: #123
+#127 := [monotonicity #124]: #126
+#131 := [trans #127 #129]: #130
+#117 := [asserted]: #45
+#134 := [mp #117 #131]: #118
+#8 := (:var 0 S2)
+#10 := (f3 #8 f4)
+#642 := (pattern #10)
+#66 := (= f1 #10)
+#69 := (not #66)
+#643 := (forall (vars (?v0 S2)) (:pat #642) #69)
+#72 := (forall (vars (?v0 S2)) #69)
+#646 := (iff #72 #643)
+#644 := (iff #69 #69)
+#645 := [refl]: #644
+#647 := [quant-intro #645]: #646
+#148 := (~ #72 #72)
+#146 := (~ #69 #69)
+#147 := [refl]: #146
+#149 := [nnf-pos #147]: #148
+#11 := (= #10 f1)
+#12 := (not #11)
+#13 := (forall (vars (?v0 S2)) #12)
+#73 := (iff #13 #72)
+#70 := (iff #12 #69)
+#67 := (iff #11 #66)
+#68 := [rewrite]: #67
+#71 := [monotonicity #68]: #70
+#74 := [quant-intro #71]: #73
+#65 := [asserted]: #13
+#77 := [mp #65 #74]: #72
+#133 := [mp~ #77 #149]: #72
+#648 := [mp #133 #647]: #643
+#225 := (not #643)
+#312 := (or #225 #122)
+#226 := [quant-inst #41]: #312
+[unit-resolution #226 #648 #134]: false
+unsat
+32295808d649b2df10d022ec20bfa2f501001522 48 0
+#2 := false
+decl f3 :: (-> S2 S3 S1)
+decl f5 :: S3
+#14 := f5
+decl f10 :: S2
+#41 := f10
+#42 := (f3 f10 f5)
+decl f1 :: S1
+#4 := f1
+#117 := (= f1 #42)
+#121 := (not #117)
+#43 := (= #42 f1)
+#44 := (not #43)
+#122 := (iff #44 #121)
+#119 := (iff #43 #117)
+#120 := [rewrite]: #119
+#123 := [monotonicity #120]: #122
+#116 := [asserted]: #44
+#126 := [mp #116 #123]: #121
+#8 := (:var 0 S2)
+#15 := (f3 #8 f5)
+#641 := (pattern #15)
+#75 := (= f1 #15)
+#642 := (forall (vars (?v0 S2)) (:pat #641) #75)
+#79 := (forall (vars (?v0 S2)) #75)
+#645 := (iff #79 #642)
+#643 := (iff #75 #75)
+#644 := [refl]: #643
+#646 := [quant-intro #644]: #645
+#128 := (~ #79 #79)
+#127 := (~ #75 #75)
+#142 := [refl]: #127
+#129 := [nnf-pos #142]: #128
+#16 := (= #15 f1)
+#17 := (forall (vars (?v0 S2)) #16)
+#80 := (iff #17 #79)
+#77 := (iff #16 #75)
+#78 := [rewrite]: #77
+#81 := [quant-intro #78]: #80
+#74 := [asserted]: #17
+#84 := [mp #74 #81]: #79
+#143 := [mp~ #84 #129]: #79
+#647 := [mp #143 #646]: #642
+#217 := (not #642)
+#304 := (or #217 #117)
+#218 := [quant-inst #41]: #304
+[unit-resolution #218 #647 #126]: false
+unsat
+dfe83e391823f1cbfcca9d6fb06c0ae74a22248a 126 0
+#2 := false
+decl f3 :: (-> S2 S3 S1)
+decl f6 :: (-> S4 S3 S3)
+decl f12 :: S3
+#44 := f12
+decl f7 :: (-> S5 S3 S4)
+decl f11 :: S3
+#42 := f11
+decl f8 :: S5
+#19 := f8
+#43 := (f7 f8 f11)
+#45 := (f6 #43 f12)
+decl f10 :: S2
+#41 := f10
+#46 := (f3 f10 #45)
+decl f1 :: S1
+#4 := f1
+#127 := (= f1 #46)
+#146 := (not #127)
+#650 := [hypothesis]: #146
+#50 := (f3 f10 f12)
+#134 := (= f1 #50)
+#48 := (f3 f10 f11)
+#131 := (= f1 #48)
+#137 := (or #131 #134)
+#338 := (or #137 #127)
+#147 := (iff #137 #146)
+#51 := (= #50 f1)
+#49 := (= #48 f1)
+#52 := (or #49 #51)
+#47 := (= #46 f1)
+#53 := (iff #47 #52)
+#54 := (not #53)
+#150 := (iff #54 #147)
+#140 := (iff #127 #137)
+#143 := (not #140)
+#148 := (iff #143 #147)
+#149 := [rewrite]: #148
+#144 := (iff #54 #143)
+#141 := (iff #53 #140)
+#138 := (iff #52 #137)
+#135 := (iff #51 #134)
+#136 := [rewrite]: #135
+#132 := (iff #49 #131)
+#133 := [rewrite]: #132
+#139 := [monotonicity #133 #136]: #138
+#129 := (iff #47 #127)
+#130 := [rewrite]: #129
+#142 := [monotonicity #130 #139]: #141
+#145 := [monotonicity #142]: #144
+#151 := [trans #145 #149]: #150
+#126 := [asserted]: #54
+#154 := [mp #126 #151]: #147
+#264 := (not #147)
+#337 := (or #137 #127 #264)
+#334 := [def-axiom]: #337
+#317 := [unit-resolution #334 #154]: #338
+#322 := [unit-resolution #317 #650]: #137
+#324 := (not #137)
+#653 := (or #127 #324)
+#22 := (:var 0 S3)
+#20 := (:var 1 S3)
+#21 := (f7 f8 #20)
+#23 := (f6 #21 #22)
+#18 := (:var 2 S2)
+#24 := (f3 #18 #23)
+#676 := (pattern #24)
+#28 := (f3 #18 #22)
+#100 := (= f1 #28)
+#26 := (f3 #18 #20)
+#97 := (= f1 #26)
+#103 := (or #97 #100)
+#93 := (= f1 #24)
+#106 := (iff #93 #103)
+#677 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #676) #106)
+#109 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #106)
+#680 := (iff #109 #677)
+#678 := (iff #106 #106)
+#679 := [refl]: #678
+#681 := [quant-intro #679]: #680
+#158 := (~ #109 #109)
+#172 := (~ #106 #106)
+#173 := [refl]: #172
+#159 := [nnf-pos #173]: #158
+#29 := (= #28 f1)
+#27 := (= #26 f1)
+#30 := (or #27 #29)
+#25 := (= #24 f1)
+#31 := (iff #25 #30)
+#32 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #31)
+#110 := (iff #32 #109)
+#107 := (iff #31 #106)
+#104 := (iff #30 #103)
+#101 := (iff #29 #100)
+#102 := [rewrite]: #101
+#98 := (iff #27 #97)
+#99 := [rewrite]: #98
+#105 := [monotonicity #99 #102]: #104
+#95 := (iff #25 #93)
+#96 := [rewrite]: #95
+#108 := [monotonicity #96 #105]: #107
+#111 := [quant-intro #108]: #110
+#92 := [asserted]: #32
+#114 := [mp #92 #111]: #109
+#174 := [mp~ #114 #159]: #109
+#682 := [mp #174 #681]: #677
+#323 := (not #677)
+#657 := (or #323 #140)
+#658 := [quant-inst #41 #42 #44]: #657
+#310 := [unit-resolution #658 #682]: #140
+#659 := (or #143 #127 #324)
+#660 := [def-axiom]: #659
+#294 := [unit-resolution #660 #310]: #653
+#637 := [unit-resolution #294 #322 #650]: false
+#298 := [lemma #637]: #127
+#311 := (or #324 #146)
+#654 := (or #324 #146 #264)
+#656 := [def-axiom]: #654
+#443 := [unit-resolution #656 #154]: #311
+#299 := [unit-resolution #443 #298]: #324
+#300 := (or #146 #137)
+#655 := (or #143 #146 #137)
+#661 := [def-axiom]: #655
+#301 := [unit-resolution #661 #310]: #300
+[unit-resolution #301 #299 #298]: false
+unsat
+54d5adcc9aa92b5c35a0e590a6651cbf7d0b828e 162 0
+#2 := false
+decl f3 :: (-> S2 S3 S1)
+decl f4 :: S3
+#9 := f4
+decl f10 :: S2
+#41 := f10
+#327 := (f3 f10 f4)
+decl f1 :: S1
+#4 := f1
+#324 := (= f1 #327)
+decl f11 :: S3
+#42 := f11
+#47 := (f3 f10 f11)
+#127 := (= f1 #47)
+#328 := (or #127 #324)
+decl f6 :: (-> S4 S3 S3)
+decl f7 :: (-> S5 S3 S4)
+decl f8 :: S5
+#19 := f8
+#43 := (f7 f8 f11)
+#44 := (f6 #43 f4)
+#45 := (f3 f10 #44)
+#123 := (= f1 #45)
+#136 := (not #123)
+#644 := [hypothesis]: #136
+#322 := (or #127 #123)
+#137 := (iff #127 #136)
+#48 := (= #47 f1)
+#46 := (= #45 f1)
+#49 := (iff #46 #48)
+#50 := (not #49)
+#140 := (iff #50 #137)
+#130 := (iff #123 #127)
+#133 := (not #130)
+#138 := (iff #133 #137)
+#139 := [rewrite]: #138
+#134 := (iff #50 #133)
+#131 := (iff #49 #130)
+#128 := (iff #48 #127)
+#129 := [rewrite]: #128
+#125 := (iff #46 #123)
+#126 := [rewrite]: #125
+#132 := [monotonicity #126 #129]: #131
+#135 := [monotonicity #132]: #134
+#141 := [trans #135 #139]: #140
+#122 := [asserted]: #50
+#144 := [mp #122 #141]: #137
+#234 := (not #137)
+#321 := (or #127 #123 #234)
+#235 := [def-axiom]: #321
+#236 := [unit-resolution #235 #144]: #322
+#646 := [unit-resolution #236 #644]: #127
+#650 := (not #328)
+#290 := (or #123 #650)
+#307 := (iff #123 #328)
+#22 := (:var 0 S3)
+#20 := (:var 1 S3)
+#21 := (f7 f8 #20)
+#23 := (f6 #21 #22)
+#18 := (:var 2 S2)
+#24 := (f3 #18 #23)
+#666 := (pattern #24)
+#28 := (f3 #18 #22)
+#96 := (= f1 #28)
+#26 := (f3 #18 #20)
+#93 := (= f1 #26)
+#99 := (or #93 #96)
+#89 := (= f1 #24)
+#102 := (iff #89 #99)
+#667 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #666) #102)
+#105 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #102)
+#670 := (iff #105 #667)
+#668 := (iff #102 #102)
+#669 := [refl]: #668
+#671 := [quant-intro #669]: #670
+#148 := (~ #105 #105)
+#162 := (~ #102 #102)
+#163 := [refl]: #162
+#149 := [nnf-pos #163]: #148
+#29 := (= #28 f1)
+#27 := (= #26 f1)
+#30 := (or #27 #29)
+#25 := (= #24 f1)
+#31 := (iff #25 #30)
+#32 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #31)
+#106 := (iff #32 #105)
+#103 := (iff #31 #102)
+#100 := (iff #30 #99)
+#97 := (iff #29 #96)
+#98 := [rewrite]: #97
+#94 := (iff #27 #93)
+#95 := [rewrite]: #94
+#101 := [monotonicity #95 #98]: #100
+#91 := (iff #25 #89)
+#92 := [rewrite]: #91
+#104 := [monotonicity #92 #101]: #103
+#107 := [quant-intro #104]: #106
+#88 := [asserted]: #32
+#110 := [mp #88 #107]: #105
+#164 := [mp~ #110 #149]: #105
+#672 := [mp #164 #671]: #667
+#301 := (not #667)
+#433 := (or #301 #307)
+#640 := [quant-inst #41 #42 #9]: #433
+#289 := [unit-resolution #640 #672]: #307
+#641 := (not #307)
+#299 := (or #641 #123 #650)
+#304 := [def-axiom]: #299
+#291 := [unit-resolution #304 #289]: #290
+#629 := [unit-resolution #291 #644]: #650
+#323 := (not #127)
+#312 := (or #328 #323)
+#313 := [def-axiom]: #312
+#630 := [unit-resolution #313 #629 #646]: false
+#631 := [lemma #630]: #123
+#632 := (or #136 #328)
+#642 := (or #641 #136 #328)
+#300 := [def-axiom]: #642
+#633 := [unit-resolution #300 #289]: #632
+#635 := [unit-resolution #633 #631]: #328
+#326 := (or #323 #136)
+#314 := (or #323 #136 #234)
+#325 := [def-axiom]: #314
+#254 := [unit-resolution #325 #144]: #326
+#637 := [unit-resolution #254 #631]: #323
+#645 := (or #650 #127 #324)
+#651 := [def-axiom]: #645
+#275 := [unit-resolution #651 #637 #635]: #324
+#8 := (:var 0 S2)
+#10 := (f3 #8 f4)
+#652 := (pattern #10)
+#71 := (= f1 #10)
+#74 := (not #71)
+#653 := (forall (vars (?v0 S2)) (:pat #652) #74)
+#77 := (forall (vars (?v0 S2)) #74)
+#656 := (iff #77 #653)
+#654 := (iff #74 #74)
+#655 := [refl]: #654
+#657 := [quant-intro #655]: #656
+#158 := (~ #77 #77)
+#156 := (~ #74 #74)
+#157 := [refl]: #156
+#159 := [nnf-pos #157]: #158
+#11 := (= #10 f1)
+#12 := (not #11)
+#13 := (forall (vars (?v0 S2)) #12)
+#78 := (iff #13 #77)
+#75 := (iff #12 #74)
+#72 := (iff #11 #71)
+#73 := [rewrite]: #72
+#76 := [monotonicity #73]: #75
+#79 := [quant-intro #76]: #78
+#70 := [asserted]: #13
+#82 := [mp #70 #79]: #77
+#143 := [mp~ #82 #159]: #77
+#658 := [mp #143 #657]: #653
+#647 := (not #324)
+#628 := (not #653)
+#634 := (or #628 #647)
+#270 := [quant-inst #41]: #634
+[unit-resolution #270 #658 #275]: false
+unsat
+6579b339206079120a92afc0dda92279c34507ae 136 0
+#2 := false
+decl f3 :: (-> S2 S3 S1)
+decl f5 :: S3
+#14 := f5
+decl f10 :: S2
+#41 := f10
+#219 := (f3 f10 f5)
+decl f1 :: S1
+#4 := f1
+#306 := (= f1 #219)
+#633 := (not #306)
+decl f11 :: S3
+#42 := f11
+#220 := (f3 f10 f11)
+#307 := (= f1 #220)
+#299 := (or #306 #307)
+#284 := (not #299)
+decl f6 :: (-> S4 S3 S3)
+decl f7 :: (-> S5 S3 S4)
+decl f8 :: S5
+#19 := f8
+#43 := (f7 f8 f11)
+#44 := (f6 #43 f5)
+#45 := (f3 f10 #44)
+#120 := (= f1 #45)
+#239 := (iff #120 #299)
+#22 := (:var 0 S3)
+#20 := (:var 1 S3)
+#21 := (f7 f8 #20)
+#23 := (f6 #21 #22)
+#18 := (:var 2 S2)
+#24 := (f3 #18 #23)
+#651 := (pattern #24)
+#28 := (f3 #18 #22)
+#93 := (= f1 #28)
+#26 := (f3 #18 #20)
+#90 := (= f1 #26)
+#96 := (or #90 #93)
+#86 := (= f1 #24)
+#99 := (iff #86 #96)
+#652 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #651) #99)
+#102 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #99)
+#655 := (iff #102 #652)
+#653 := (iff #99 #99)
+#654 := [refl]: #653
+#656 := [quant-intro #654]: #655
+#133 := (~ #102 #102)
+#147 := (~ #99 #99)
+#148 := [refl]: #147
+#134 := [nnf-pos #148]: #133
+#29 := (= #28 f1)
+#27 := (= #26 f1)
+#30 := (or #27 #29)
+#25 := (= #24 f1)
+#31 := (iff #25 #30)
+#32 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #31)
+#103 := (iff #32 #102)
+#100 := (iff #31 #99)
+#97 := (iff #30 #96)
+#94 := (iff #29 #93)
+#95 := [rewrite]: #94
+#91 := (iff #27 #90)
+#92 := [rewrite]: #91
+#98 := [monotonicity #92 #95]: #97
+#88 := (iff #25 #86)
+#89 := [rewrite]: #88
+#101 := [monotonicity #89 #98]: #100
+#104 := [quant-intro #101]: #103
+#85 := [asserted]: #32
+#107 := [mp #85 #104]: #102
+#149 := [mp~ #107 #134]: #102
+#657 := [mp #149 #656]: #652
+#313 := (not #652)
+#292 := (or #313 #239)
+#221 := (or #307 #306)
+#308 := (iff #120 #221)
+#629 := (or #313 #308)
+#286 := (iff #629 #292)
+#625 := (iff #292 #292)
+#297 := [rewrite]: #625
+#312 := (iff #308 #239)
+#310 := (iff #221 #299)
+#311 := [rewrite]: #310
+#309 := [monotonicity #311]: #312
+#418 := [monotonicity #309]: #286
+#298 := [trans #418 #297]: #286
+#631 := [quant-inst #41 #42 #14]: #629
+#632 := [mp #631 #298]: #292
+#615 := [unit-resolution #632 #657]: #239
+#285 := (not #239)
+#616 := (or #285 #284)
+#124 := (not #120)
+#46 := (= #45 f1)
+#47 := (not #46)
+#125 := (iff #47 #124)
+#122 := (iff #46 #120)
+#123 := [rewrite]: #122
+#126 := [monotonicity #123]: #125
+#119 := [asserted]: #47
+#129 := [mp #119 #126]: #124
+#628 := (or #285 #120 #284)
+#269 := [def-axiom]: #628
+#619 := [unit-resolution #269 #129]: #616
+#255 := [unit-resolution #619 #615]: #284
+#634 := (or #299 #633)
+#635 := [def-axiom]: #634
+#620 := [unit-resolution #635 #255]: #633
+#8 := (:var 0 S2)
+#15 := (f3 #8 f5)
+#644 := (pattern #15)
+#78 := (= f1 #15)
+#645 := (forall (vars (?v0 S2)) (:pat #644) #78)
+#82 := (forall (vars (?v0 S2)) #78)
+#648 := (iff #82 #645)
+#646 := (iff #78 #78)
+#647 := [refl]: #646
+#649 := [quant-intro #647]: #648
+#131 := (~ #82 #82)
+#130 := (~ #78 #78)
+#145 := [refl]: #130
+#132 := [nnf-pos #145]: #131
+#16 := (= #15 f1)
+#17 := (forall (vars (?v0 S2)) #16)
+#83 := (iff #17 #82)
+#80 := (iff #16 #78)
+#81 := [rewrite]: #80
+#84 := [quant-intro #81]: #83
+#77 := [asserted]: #17
+#87 := [mp #77 #84]: #82
+#146 := [mp~ #87 #132]: #82
+#650 := [mp #146 #649]: #645
+#617 := (not #645)
+#618 := (or #617 #306)
+#613 := [quant-inst #41]: #618
+[unit-resolution #613 #650 #620]: false
+unsat
+21f3225a60811428730067e610d6913c3bcb0df3 155 0
+#2 := false
+decl f3 :: (-> S2 S3 S1)
+decl f6 :: (-> S4 S3 S3)
+decl f11 :: S3
+#42 := f11
+decl f7 :: (-> S5 S3 S4)
+decl f12 :: S3
+#44 := f12
+decl f8 :: S5
+#19 := f8
+#48 := (f7 f8 f12)
+#49 := (f6 #48 f11)
+decl f10 :: S2
+#41 := f10
+#50 := (f3 f10 #49)
+decl f1 :: S1
+#4 := f1
+#130 := (= f1 #50)
+#326 := (not #130)
+#43 := (f7 f8 f11)
+#45 := (f6 #43 f12)
+#46 := (f3 f10 #45)
+#126 := (= f1 #46)
+#139 := (not #126)
+#245 := [hypothesis]: #139
+#325 := (or #130 #126)
+#140 := (iff #130 #139)
+#51 := (= #50 f1)
+#47 := (= #46 f1)
+#52 := (iff #47 #51)
+#53 := (not #52)
+#143 := (iff #53 #140)
+#133 := (iff #126 #130)
+#136 := (not #133)
+#141 := (iff #136 #140)
+#142 := [rewrite]: #141
+#137 := (iff #53 #136)
+#134 := (iff #52 #133)
+#131 := (iff #51 #130)
+#132 := [rewrite]: #131
+#128 := (iff #47 #126)
+#129 := [rewrite]: #128
+#135 := [monotonicity #129 #132]: #134
+#138 := [monotonicity #135]: #137
+#144 := [trans #138 #142]: #143
+#125 := [asserted]: #53
+#147 := [mp #125 #144]: #140
+#237 := (not #140)
+#324 := (or #130 #126 #237)
+#238 := [def-axiom]: #324
+#239 := [unit-resolution #238 #147]: #325
+#624 := [unit-resolution #239 #245]: #130
+#330 := (f3 f10 f11)
+#327 := (= f1 #330)
+#331 := (f3 f10 f12)
+#310 := (= f1 #331)
+#647 := (or #310 #327)
+#644 := (not #647)
+#347 := (or #126 #644)
+#634 := (iff #126 #647)
+#22 := (:var 0 S3)
+#20 := (:var 1 S3)
+#21 := (f7 f8 #20)
+#23 := (f6 #21 #22)
+#18 := (:var 2 S2)
+#24 := (f3 #18 #23)
+#669 := (pattern #24)
+#28 := (f3 #18 #22)
+#99 := (= f1 #28)
+#26 := (f3 #18 #20)
+#96 := (= f1 #26)
+#102 := (or #96 #99)
+#92 := (= f1 #24)
+#105 := (iff #92 #102)
+#670 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #669) #105)
+#108 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #105)
+#673 := (iff #108 #670)
+#671 := (iff #105 #105)
+#672 := [refl]: #671
+#674 := [quant-intro #672]: #673
+#151 := (~ #108 #108)
+#165 := (~ #105 #105)
+#166 := [refl]: #165
+#152 := [nnf-pos #166]: #151
+#29 := (= #28 f1)
+#27 := (= #26 f1)
+#30 := (or #27 #29)
+#25 := (= #24 f1)
+#31 := (iff #25 #30)
+#32 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #31)
+#109 := (iff #32 #108)
+#106 := (iff #31 #105)
+#103 := (iff #30 #102)
+#100 := (iff #29 #99)
+#101 := [rewrite]: #100
+#97 := (iff #27 #96)
+#98 := [rewrite]: #97
+#104 := [monotonicity #98 #101]: #103
+#94 := (iff #25 #92)
+#95 := [rewrite]: #94
+#107 := [monotonicity #95 #104]: #106
+#110 := [quant-intro #107]: #109
+#91 := [asserted]: #32
+#113 := [mp #91 #110]: #108
+#167 := [mp~ #113 #152]: #108
+#675 := [mp #167 #674]: #670
+#643 := (not #670)
+#631 := (or #643 #634)
+#304 := (or #327 #310)
+#436 := (iff #126 #304)
+#637 := (or #643 #436)
+#638 := (iff #637 #631)
+#278 := (iff #631 #631)
+#279 := [rewrite]: #278
+#635 := (iff #436 #634)
+#632 := (iff #304 #647)
+#633 := [rewrite]: #632
+#636 := [monotonicity #633]: #635
+#640 := [monotonicity #636]: #638
+#641 := [trans #640 #279]: #638
+#273 := [quant-inst #41 #42 #44]: #637
+#639 := [mp #273 #641]: #631
+#625 := [unit-resolution #639 #675]: #634
+#642 := (not #634)
+#628 := (or #642 #126 #644)
+#629 := [def-axiom]: #628
+#348 := [unit-resolution #629 #625]: #347
+#622 := [unit-resolution #348 #245]: #644
+#623 := (or #326 #647)
+#649 := (iff #130 #647)
+#315 := (or #643 #649)
+#316 := [quant-inst #41 #44 #42]: #315
+#626 := [unit-resolution #316 #675]: #649
+#645 := (not #649)
+#287 := (or #645 #326 #647)
+#630 := [def-axiom]: #287
+#627 := [unit-resolution #630 #626]: #623
+#336 := [unit-resolution #627 #622 #624]: false
+#337 := [lemma #336]: #126
+#329 := (or #326 #139)
+#317 := (or #326 #139 #237)
+#328 := [def-axiom]: #317
+#257 := [unit-resolution #328 #147]: #329
+#338 := [unit-resolution #257 #337]: #326
+#340 := (or #139 #647)
+#335 := (or #642 #139 #647)
+#351 := [def-axiom]: #335
+#618 := [unit-resolution #351 #625]: #340
+#619 := [unit-resolution #618 #337]: #647
+#332 := (or #130 #644)
+#303 := (or #645 #130 #644)
+#646 := [def-axiom]: #303
+#616 := [unit-resolution #646 #626]: #332
+[unit-resolution #616 #619 #338]: false
+unsat
+0a38803d5203ebb9de80029b1e5de8bcd8e8f404 128 0
+#2 := false
+decl f3 :: (-> S2 S3 S1)
+decl f6 :: (-> S4 S3 S3)
+decl f11 :: S3
+#42 := f11
+decl f7 :: (-> S5 S3 S4)
+decl f8 :: S5
+#19 := f8
+#43 := (f7 f8 f11)
+#44 := (f6 #43 f11)
+decl f10 :: S2
+#41 := f10
+#45 := (f3 f10 #44)
+decl f1 :: S1
+#4 := f1
+#123 := (= f1 #45)
+#136 := (not #123)
+#627 := [hypothesis]: #136
+#47 := (f3 f10 f11)
+#127 := (= f1 #47)
+#322 := (or #127 #123)
+#137 := (iff #127 #136)
+#48 := (= #47 f1)
+#46 := (= #45 f1)
+#49 := (iff #46 #48)
+#50 := (not #49)
+#140 := (iff #50 #137)
+#130 := (iff #123 #127)
+#133 := (not #130)
+#138 := (iff #133 #137)
+#139 := [rewrite]: #138
+#134 := (iff #50 #133)
+#131 := (iff #49 #130)
+#128 := (iff #48 #127)
+#129 := [rewrite]: #128
+#125 := (iff #46 #123)
+#126 := [rewrite]: #125
+#132 := [monotonicity #126 #129]: #131
+#135 := [monotonicity #132]: #134
+#141 := [trans #135 #139]: #140
+#122 := [asserted]: #50
+#144 := [mp #122 #141]: #137
+#234 := (not #137)
+#321 := (or #127 #123 #234)
+#235 := [def-axiom]: #321
+#236 := [unit-resolution #235 #144]: #322
+#288 := [unit-resolution #236 #627]: #127
+#323 := (not #127)
+#290 := (or #123 #323)
+#22 := (:var 0 S3)
+#20 := (:var 1 S3)
+#21 := (f7 f8 #20)
+#23 := (f6 #21 #22)
+#18 := (:var 2 S2)
+#24 := (f3 #18 #23)
+#666 := (pattern #24)
+#28 := (f3 #18 #22)
+#96 := (= f1 #28)
+#26 := (f3 #18 #20)
+#93 := (= f1 #26)
+#99 := (or #93 #96)
+#89 := (= f1 #24)
+#102 := (iff #89 #99)
+#667 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #666) #102)
+#105 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #102)
+#670 := (iff #105 #667)
+#668 := (iff #102 #102)
+#669 := [refl]: #668
+#671 := [quant-intro #669]: #670
+#148 := (~ #105 #105)
+#162 := (~ #102 #102)
+#163 := [refl]: #162
+#149 := [nnf-pos #163]: #148
+#29 := (= #28 f1)
+#27 := (= #26 f1)
+#30 := (or #27 #29)
+#25 := (= #24 f1)
+#31 := (iff #25 #30)
+#32 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #31)
+#106 := (iff #32 #105)
+#103 := (iff #31 #102)
+#100 := (iff #30 #99)
+#97 := (iff #29 #96)
+#98 := [rewrite]: #97
+#94 := (iff #27 #93)
+#95 := [rewrite]: #94
+#101 := [monotonicity #95 #98]: #100
+#91 := (iff #25 #89)
+#92 := [rewrite]: #91
+#104 := [monotonicity #92 #101]: #103
+#107 := [quant-intro #104]: #106
+#88 := [asserted]: #32
+#110 := [mp #88 #107]: #105
+#164 := [mp~ #110 #149]: #105
+#672 := [mp #164 #671]: #667
+#301 := (not #667)
+#433 := (or #301 #130)
+#327 := (or #127 #127)
+#324 := (iff #123 #327)
+#640 := (or #301 #324)
+#313 := (iff #640 #433)
+#648 := (iff #433 #433)
+#649 := [rewrite]: #648
+#644 := (iff #324 #130)
+#328 := (iff #327 #127)
+#307 := [rewrite]: #328
+#646 := [monotonicity #307]: #644
+#647 := [monotonicity #646]: #313
+#650 := [trans #647 #649]: #313
+#312 := [quant-inst #41 #42 #42]: #640
+#645 := [mp #312 #650]: #433
+#289 := [unit-resolution #645 #672]: #130
+#651 := (or #133 #123 #323)
+#641 := [def-axiom]: #651
+#291 := [unit-resolution #641 #289]: #290
+#629 := [unit-resolution #291 #288 #627]: false
+#630 := [lemma #629]: #123
+#326 := (or #323 #136)
+#314 := (or #323 #136 #234)
+#325 := [def-axiom]: #314
+#254 := [unit-resolution #325 #144]: #326
+#631 := [unit-resolution #254 #630]: #323
+#632 := (or #136 #127)
+#299 := (or #133 #136 #127)
+#304 := [def-axiom]: #299
+#633 := [unit-resolution #304 #289]: #632
+[unit-resolution #633 #631 #630]: false
+unsat
+a9b4d2c6d5d71402741164958baf8befeec2192a 266 0
+#2 := false
+decl f3 :: (-> S2 S3 S1)
+decl f12 :: S3
+#44 := f12
+decl f10 :: S2
+#41 := f10
+#623 := (f3 f10 f12)
+decl f1 :: S1
+#4 := f1
+#336 := (= f1 #623)
+decl f13 :: S3
+#46 := f13
+#334 := (f3 f10 f13)
+#331 := (= f1 #334)
+#621 := (or #331 #336)
+decl f6 :: (-> S4 S3 S3)
+decl f7 :: (-> S5 S3 S4)
+decl f8 :: S5
+#19 := f8
+#45 := (f7 f8 f12)
+#47 := (f6 #45 f13)
+#308 := (f3 f10 #47)
+#440 := (= f1 #308)
+#615 := (iff #440 #621)
+#581 := (not #615)
+#593 := (not #621)
+#605 := (not #336)
+decl f11 :: S3
+#42 := f11
+#636 := (f3 f10 f11)
+#637 := (= f1 #636)
+#483 := (or #336 #637)
+#608 := (not #483)
+#43 := (f7 f8 f11)
+#51 := (f6 #43 f12)
+#335 := (f3 f10 #51)
+#314 := (= f1 #335)
+#591 := (iff #314 #483)
+#583 := (not #591)
+#576 := [hypothesis]: #583
+#22 := (:var 0 S3)
+#20 := (:var 1 S3)
+#21 := (f7 f8 #20)
+#23 := (f6 #21 #22)
+#18 := (:var 2 S2)
+#24 := (f3 #18 #23)
+#673 := (pattern #24)
+#28 := (f3 #18 #22)
+#103 := (= f1 #28)
+#26 := (f3 #18 #20)
+#100 := (= f1 #26)
+#106 := (or #100 #103)
+#96 := (= f1 #24)
+#109 := (iff #96 #106)
+#674 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #673) #109)
+#112 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #109)
+#677 := (iff #112 #674)
+#675 := (iff #109 #109)
+#676 := [refl]: #675
+#678 := [quant-intro #676]: #677
+#155 := (~ #112 #112)
+#169 := (~ #109 #109)
+#170 := [refl]: #169
+#156 := [nnf-pos #170]: #155
+#29 := (= #28 f1)
+#27 := (= #26 f1)
+#30 := (or #27 #29)
+#25 := (= #24 f1)
+#31 := (iff #25 #30)
+#32 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #31)
+#113 := (iff #32 #112)
+#110 := (iff #31 #109)
+#107 := (iff #30 #106)
+#104 := (iff #29 #103)
+#105 := [rewrite]: #104
+#101 := (iff #27 #100)
+#102 := [rewrite]: #101
+#108 := [monotonicity #102 #105]: #107
+#98 := (iff #25 #96)
+#99 := [rewrite]: #98
+#111 := [monotonicity #99 #108]: #110
+#114 := [quant-intro #111]: #113
+#95 := [asserted]: #32
+#117 := [mp #95 #114]: #112
+#171 := [mp~ #117 #156]: #112
+#679 := [mp #171 #678]: #674
+#647 := (not #674)
+#589 := (or #647 #591)
+#600 := (or #637 #336)
+#482 := (iff #314 #600)
+#592 := (or #647 #482)
+#492 := (iff #592 #589)
+#495 := (iff #589 #589)
+#488 := [rewrite]: #495
+#493 := (iff #482 #591)
+#484 := (iff #600 #483)
+#443 := [rewrite]: #484
+#588 := [monotonicity #443]: #493
+#494 := [monotonicity #588]: #492
+#496 := [trans #494 #488]: #492
+#477 := [quant-inst #41 #42 #44]: #592
+#497 := [mp #477 #496]: #589
+#577 := [unit-resolution #497 #679 #576]: false
+#578 := [lemma #577]: #591
+#654 := (not #314)
+#651 := (or #314 #331)
+#648 := (not #651)
+#52 := (f7 f8 #51)
+#53 := (f6 #52 f13)
+#54 := (f3 f10 #53)
+#134 := (= f1 #54)
+#330 := (not #134)
+#48 := (f6 #43 #47)
+#49 := (f3 f10 #48)
+#130 := (= f1 #49)
+#143 := (not #130)
+#579 := [hypothesis]: #143
+#329 := (or #134 #130)
+#144 := (iff #134 #143)
+#55 := (= #54 f1)
+#50 := (= #49 f1)
+#56 := (iff #50 #55)
+#57 := (not #56)
+#147 := (iff #57 #144)
+#137 := (iff #130 #134)
+#140 := (not #137)
+#145 := (iff #140 #144)
+#146 := [rewrite]: #145
+#141 := (iff #57 #140)
+#138 := (iff #56 #137)
+#135 := (iff #55 #134)
+#136 := [rewrite]: #135
+#132 := (iff #50 #130)
+#133 := [rewrite]: #132
+#139 := [monotonicity #133 #136]: #138
+#142 := [monotonicity #139]: #141
+#148 := [trans #142 #146]: #147
+#129 := [asserted]: #57
+#151 := [mp #129 #148]: #144
+#241 := (not #144)
+#328 := (or #134 #130 #241)
+#242 := [def-axiom]: #328
+#243 := [unit-resolution #242 #151]: #329
+#573 := [unit-resolution #243 #579]: #134
+#564 := (or #330 #651)
+#653 := (iff #134 #651)
+#319 := (or #647 #653)
+#320 := [quant-inst #41 #51 #46]: #319
+#580 := [unit-resolution #320 #679]: #653
+#649 := (not #653)
+#291 := (or #649 #330 #651)
+#634 := [def-axiom]: #291
+#565 := [unit-resolution #634 #580]: #564
+#567 := [unit-resolution #565 #573]: #651
+#657 := (not #331)
+#597 := (or #647 #615)
+#620 := (or #336 #331)
+#624 := (iff #440 #620)
+#617 := (or #647 #624)
+#612 := (iff #617 #597)
+#619 := (iff #597 #597)
+#460 := [rewrite]: #619
+#616 := (iff #624 #615)
+#625 := (iff #620 #621)
+#614 := [rewrite]: #625
+#611 := [monotonicity #614]: #616
+#613 := [monotonicity #611]: #612
+#461 := [trans #613 #460]: #612
+#618 := [quant-inst #41 #44 #46]: #617
+#462 := [mp #618 #461]: #597
+#568 := [unit-resolution #462 #679]: #615
+#558 := (or #581 #593)
+#356 := (not #440)
+#640 := (or #440 #637)
+#629 := (not #640)
+#570 := (or #130 #629)
+#277 := (iff #130 #640)
+#282 := (or #647 #277)
+#638 := (or #637 #440)
+#639 := (iff #130 #638)
+#283 := (or #647 #639)
+#643 := (iff #283 #282)
+#632 := (iff #282 #282)
+#633 := [rewrite]: #632
+#642 := (iff #639 #277)
+#635 := (iff #638 #640)
+#641 := [rewrite]: #635
+#644 := [monotonicity #641]: #642
+#646 := [monotonicity #644]: #643
+#339 := [trans #646 #633]: #643
+#645 := [quant-inst #41 #42 #47]: #283
+#355 := [mp #645 #339]: #282
+#569 := [unit-resolution #355 #679]: #277
+#626 := (not #277)
+#630 := (or #626 #130 #629)
+#627 := [def-axiom]: #630
+#566 := [unit-resolution #627 #569]: #570
+#571 := [unit-resolution #566 #579]: #629
+#357 := (or #640 #356)
+#343 := [def-axiom]: #357
+#557 := [unit-resolution #343 #571]: #356
+#575 := (or #581 #440 #593)
+#572 := [def-axiom]: #575
+#560 := [unit-resolution #572 #557]: #558
+#561 := [unit-resolution #560 #568]: #593
+#604 := (or #621 #657)
+#498 := [def-axiom]: #604
+#562 := [unit-resolution #498 #561]: #657
+#306 := (or #648 #314 #331)
+#311 := [def-axiom]: #306
+#559 := [unit-resolution #311 #562 #567]: #314
+#358 := (not #637)
+#249 := (or #640 #358)
+#628 := [def-axiom]: #249
+#563 := [unit-resolution #628 #571]: #358
+#499 := (or #621 #605)
+#500 := [def-axiom]: #499
+#543 := [unit-resolution #500 #561]: #605
+#609 := (or #608 #336 #637)
+#603 := [def-axiom]: #609
+#544 := [unit-resolution #603 #543 #563]: #608
+#441 := (or #583 #654 #483)
+#442 := [def-axiom]: #441
+#546 := [unit-resolution #442 #544 #559 #578]: false
+#547 := [lemma #546]: #130
+#333 := (or #330 #143)
+#321 := (or #330 #143 #241)
+#332 := [def-axiom]: #321
+#261 := [unit-resolution #332 #151]: #333
+#548 := [unit-resolution #261 #547]: #330
+#549 := (or #134 #648)
+#307 := (or #649 #134 #648)
+#650 := [def-axiom]: #307
+#550 := [unit-resolution #650 #580]: #549
+#551 := [unit-resolution #550 #548]: #648
+#655 := (or #651 #654)
+#656 := [def-axiom]: #655
+#552 := [unit-resolution #656 #551]: #654
+#610 := (or #583 #314 #608)
+#439 := [def-axiom]: #610
+#553 := [unit-resolution #439 #552 #578]: #608
+#606 := (or #483 #605)
+#607 := [def-axiom]: #606
+#554 := [unit-resolution #607 #553]: #605
+#652 := (or #651 #657)
+#658 := [def-axiom]: #652
+#555 := [unit-resolution #658 #551]: #657
+#590 := (or #593 #331 #336)
+#594 := [def-axiom]: #590
+#545 := [unit-resolution #594 #555 #554]: #593
+#556 := (or #143 #640)
+#631 := (or #626 #143 #640)
+#340 := [def-axiom]: #631
+#534 := [unit-resolution #340 #569]: #556
+#535 := [unit-resolution #534 #547]: #640
+#601 := (or #483 #358)
+#602 := [def-axiom]: #601
+#537 := [unit-resolution #602 #553]: #358
+#351 := (or #629 #440 #637)
+#352 := [def-axiom]: #351
+#538 := [unit-resolution #352 #537 #535]: #440
+#574 := (or #581 #356 #621)
+#584 := [def-axiom]: #574
+#539 := [unit-resolution #584 #538 #545]: #581
+[unit-resolution #462 #679 #539]: false
+unsat
+c3c3648cfba9d6c85cac6f8d51a3b06b08975178 160 0
+#2 := false
+decl f3 :: (-> S2 S3 S1)
+decl f12 :: S3
+#44 := f12
+decl f10 :: S2
+#41 := f10
+#50 := (f3 f10 f12)
+decl f1 :: S1
+#4 := f1
+#134 := (= f1 #50)
+#188 := (not #134)
+decl f11 :: S3
+#42 := f11
+#48 := (f3 f10 f11)
+#131 := (= f1 #48)
+#187 := (not #131)
+#189 := (or #187 #188)
+#190 := (not #189)
+#331 := [hypothesis]: #190
+decl f6 :: (-> S4 S3 S3)
+decl f7 :: (-> S5 S3 S4)
+decl f9 :: S5
+#33 := f9
+#43 := (f7 f9 f11)
+#45 := (f6 #43 f12)
+#46 := (f3 f10 #45)
+#127 := (= f1 #46)
+#146 := (not #127)
+#337 := (or #146 #189)
+#201 := (iff #127 #189)
+#137 := (and #131 #134)
+#147 := (iff #137 #146)
+#204 := (iff #147 #201)
+#196 := (iff #189 #127)
+#202 := (iff #196 #201)
+#203 := [rewrite]: #202
+#199 := (iff #147 #196)
+#193 := (iff #190 #146)
+#197 := (iff #193 #196)
+#198 := [rewrite]: #197
+#194 := (iff #147 #193)
+#191 := (iff #137 #190)
+#192 := [rewrite]: #191
+#195 := [monotonicity #192]: #194
+#200 := [trans #195 #198]: #199
+#205 := [trans #200 #203]: #204
+#51 := (= #50 f1)
+#49 := (= #48 f1)
+#52 := (and #49 #51)
+#47 := (= #46 f1)
+#53 := (iff #47 #52)
+#54 := (not #53)
+#150 := (iff #54 #147)
+#140 := (iff #127 #137)
+#143 := (not #140)
+#148 := (iff #143 #147)
+#149 := [rewrite]: #148
+#144 := (iff #54 #143)
+#141 := (iff #53 #140)
+#138 := (iff #52 #137)
+#135 := (iff #51 #134)
+#136 := [rewrite]: #135
+#132 := (iff #49 #131)
+#133 := [rewrite]: #132
+#139 := [monotonicity #133 #136]: #138
+#129 := (iff #47 #127)
+#130 := [rewrite]: #129
+#142 := [monotonicity #130 #139]: #141
+#145 := [monotonicity #142]: #144
+#151 := [trans #145 #149]: #150
+#126 := [asserted]: #54
+#154 := [mp #126 #151]: #147
+#206 := [mp #154 #205]: #201
+#344 := (not #201)
+#354 := (or #146 #189 #344)
+#358 := [def-axiom]: #354
+#674 := [unit-resolution #358 #206]: #337
+#463 := [unit-resolution #674 #331]: #146
+#330 := (or #127 #189)
+#676 := (iff #127 #190)
+#22 := (:var 0 S3)
+#20 := (:var 1 S3)
+#34 := (f7 f9 #20)
+#35 := (f6 #34 #22)
+#18 := (:var 2 S2)
+#36 := (f3 #18 #35)
+#703 := (pattern #36)
+#28 := (f3 #18 #22)
+#100 := (= f1 #28)
+#179 := (not #100)
+#26 := (f3 #18 #20)
+#97 := (= f1 #26)
+#178 := (not #97)
+#162 := (or #178 #179)
+#163 := (not #162)
+#113 := (= f1 #36)
+#180 := (iff #113 #163)
+#704 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #703) #180)
+#183 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #180)
+#707 := (iff #183 #704)
+#705 := (iff #180 #180)
+#706 := [refl]: #705
+#708 := [quant-intro #706]: #707
+#117 := (and #97 #100)
+#120 := (iff #113 #117)
+#123 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #120)
+#184 := (iff #123 #183)
+#181 := (iff #120 #180)
+#164 := (iff #117 #163)
+#165 := [rewrite]: #164
+#182 := [monotonicity #165]: #181
+#185 := [quant-intro #182]: #184
+#160 := (~ #123 #123)
+#175 := (~ #120 #120)
+#176 := [refl]: #175
+#161 := [nnf-pos #176]: #160
+#29 := (= #28 f1)
+#27 := (= #26 f1)
+#38 := (and #27 #29)
+#37 := (= #36 f1)
+#39 := (iff #37 #38)
+#40 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #39)
+#124 := (iff #40 #123)
+#121 := (iff #39 #120)
+#118 := (iff #38 #117)
+#101 := (iff #29 #100)
+#102 := [rewrite]: #101
+#98 := (iff #27 #97)
+#99 := [rewrite]: #98
+#119 := [monotonicity #99 #102]: #118
+#115 := (iff #37 #113)
+#116 := [rewrite]: #115
+#122 := [monotonicity #116 #119]: #121
+#125 := [quant-intro #122]: #124
+#112 := [asserted]: #40
+#128 := [mp #112 #125]: #123
+#177 := [mp~ #128 #161]: #123
+#186 := [mp #177 #185]: #183
+#709 := [mp #186 #708]: #704
+#670 := (not #704)
+#342 := (or #670 #676)
+#343 := [quant-inst #41 #42 #44]: #342
+#672 := [unit-resolution #343 #709]: #676
+#677 := (not #676)
+#678 := (or #677 #127 #189)
+#679 := [def-axiom]: #678
+#673 := [unit-resolution #679 #672]: #330
+#314 := [unit-resolution #673 #463 #331]: false
+#657 := [lemma #314]: #189
+#284 := (or #127 #190)
+#355 := (or #127 #190 #344)
+#356 := [def-axiom]: #355
+#357 := [unit-resolution #356 #206]: #284
+#318 := [unit-resolution #357 #657]: #127
+#319 := (or #146 #190)
+#680 := (or #677 #146 #190)
+#675 := [def-axiom]: #680
+#320 := [unit-resolution #675 #672]: #319
+[unit-resolution #320 #318 #657]: false
+unsat
+1adc4d295cebee376081ce9f5a9d0e96c2943423 149 0
+#2 := false
+decl f3 :: (-> S2 S3 S1)
+decl f4 :: S3
+#9 := f4
+decl f10 :: S2
+#41 := f10
+#227 := (f3 f10 f4)
+decl f1 :: S1
+#4 := f1
+#314 := (= f1 #227)
+#228 := (not #314)
+decl f11 :: S3
+#42 := f11
+#315 := (f3 f10 f11)
+#229 := (= f1 #315)
+#316 := (not #229)
+#307 := (or #316 #228)
+#318 := (not #307)
+decl f6 :: (-> S4 S3 S3)
+decl f7 :: (-> S5 S3 S4)
+decl f9 :: S5
+#33 := f9
+#43 := (f7 f9 f11)
+#44 := (f6 #43 f4)
+#45 := (f3 f10 #44)
+#121 := (= f1 #45)
+#319 := (iff #121 #318)
+#22 := (:var 0 S3)
+#20 := (:var 1 S3)
+#34 := (f7 f9 #20)
+#35 := (f6 #34 #22)
+#18 := (:var 2 S2)
+#36 := (f3 #18 #35)
+#666 := (pattern #36)
+#28 := (f3 #18 #22)
+#94 := (= f1 #28)
+#162 := (not #94)
+#26 := (f3 #18 #20)
+#91 := (= f1 #26)
+#161 := (not #91)
+#145 := (or #161 #162)
+#146 := (not #145)
+#107 := (= f1 #36)
+#163 := (iff #107 #146)
+#667 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #666) #163)
+#166 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #163)
+#670 := (iff #166 #667)
+#668 := (iff #163 #163)
+#669 := [refl]: #668
+#671 := [quant-intro #669]: #670
+#111 := (and #91 #94)
+#114 := (iff #107 #111)
+#117 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #114)
+#167 := (iff #117 #166)
+#164 := (iff #114 #163)
+#147 := (iff #111 #146)
+#148 := [rewrite]: #147
+#165 := [monotonicity #148]: #164
+#168 := [quant-intro #165]: #167
+#143 := (~ #117 #117)
+#158 := (~ #114 #114)
+#159 := [refl]: #158
+#144 := [nnf-pos #159]: #143
+#29 := (= #28 f1)
+#27 := (= #26 f1)
+#38 := (and #27 #29)
+#37 := (= #36 f1)
+#39 := (iff #37 #38)
+#40 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #39)
+#118 := (iff #40 #117)
+#115 := (iff #39 #114)
+#112 := (iff #38 #111)
+#95 := (iff #29 #94)
+#96 := [rewrite]: #95
+#92 := (iff #27 #91)
+#93 := [rewrite]: #92
+#113 := [monotonicity #93 #96]: #112
+#109 := (iff #37 #107)
+#110 := [rewrite]: #109
+#116 := [monotonicity #110 #113]: #115
+#119 := [quant-intro #116]: #118
+#106 := [asserted]: #40
+#122 := [mp #106 #119]: #117
+#160 := [mp~ #122 #144]: #117
+#169 := [mp #160 #168]: #166
+#672 := [mp #169 #671]: #667
+#317 := (not #667)
+#321 := (or #317 #319)
+#300 := [quant-inst #41 #42 #9]: #321
+#247 := [unit-resolution #300 #672]: #319
+#306 := (not #319)
+#320 := (or #306 #318)
+#46 := (= #45 f1)
+#47 := (not #46)
+#48 := (not #47)
+#133 := (iff #48 #121)
+#125 := (not #121)
+#128 := (not #125)
+#131 := (iff #128 #121)
+#132 := [rewrite]: #131
+#129 := (iff #48 #128)
+#126 := (iff #47 #125)
+#123 := (iff #46 #121)
+#124 := [rewrite]: #123
+#127 := [monotonicity #124]: #126
+#130 := [monotonicity #127]: #129
+#134 := [trans #130 #132]: #133
+#120 := [asserted]: #48
+#137 := [mp #120 #134]: #121
+#642 := (or #306 #125 #318)
+#643 := [def-axiom]: #642
+#636 := [unit-resolution #643 #137]: #320
+#277 := [unit-resolution #636 #247]: #318
+#294 := (or #307 #314)
+#426 := [def-axiom]: #294
+#620 := [unit-resolution #426 #277]: #314
+#8 := (:var 0 S2)
+#10 := (f3 #8 f4)
+#645 := (pattern #10)
+#69 := (= f1 #10)
+#72 := (not #69)
+#646 := (forall (vars (?v0 S2)) (:pat #645) #72)
+#75 := (forall (vars (?v0 S2)) #72)
+#649 := (iff #75 #646)
+#647 := (iff #72 #72)
+#648 := [refl]: #647
+#650 := [quant-intro #648]: #649
+#151 := (~ #75 #75)
+#149 := (~ #72 #72)
+#150 := [refl]: #149
+#152 := [nnf-pos #150]: #151
+#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
+#136 := [mp~ #80 #152]: #75
+#651 := [mp #136 #650]: #646
+#297 := (not #646)
+#635 := (or #297 #228)
+#293 := [quant-inst #41]: #635
+[unit-resolution #293 #651 #620]: false
+unsat
+27fbc35929f013c0b43884a593f3f377821cad64 173 0
+#2 := false
+decl f3 :: (-> S2 S3 S1)
+decl f11 :: S3
+#42 := f11
+decl f10 :: S2
+#41 := f10
+#47 := (f3 f10 f11)
+decl f1 :: S1
+#4 := f1
+#127 := (= f1 #47)
+#323 := (not #127)
+decl f6 :: (-> S4 S3 S3)
+decl f5 :: S3
+#14 := f5
+decl f7 :: (-> S5 S3 S4)
+decl f9 :: S5
+#33 := f9
+#43 := (f7 f9 f11)
+#44 := (f6 #43 f5)
+#45 := (f3 f10 #44)
+#123 := (= f1 #45)
+#327 := (f3 f10 f5)
+#324 := (= f1 #327)
+#328 := (not #324)
+#301 := [hypothesis]: #328
+#8 := (:var 0 S2)
+#15 := (f3 #8 f5)
+#659 := (pattern #15)
+#81 := (= f1 #15)
+#660 := (forall (vars (?v0 S2)) (:pat #659) #81)
+#85 := (forall (vars (?v0 S2)) #81)
+#663 := (iff #85 #660)
+#661 := (iff #81 #81)
+#662 := [refl]: #661
+#664 := [quant-intro #662]: #663
+#146 := (~ #85 #85)
+#145 := (~ #81 #81)
+#160 := [refl]: #145
+#147 := [nnf-pos #160]: #146
+#16 := (= #15 f1)
+#17 := (forall (vars (?v0 S2)) #16)
+#86 := (iff #17 #85)
+#83 := (iff #16 #81)
+#84 := [rewrite]: #83
+#87 := [quant-intro #84]: #86
+#80 := [asserted]: #17
+#90 := [mp #80 #87]: #85
+#161 := [mp~ #90 #147]: #85
+#665 := [mp #161 #664]: #660
+#289 := (not #660)
+#290 := (or #289 #324)
+#291 := [quant-inst #41]: #290
+#433 := [unit-resolution #291 #665 #301]: false
+#629 := [lemma #433]: #324
+#136 := (not #123)
+#630 := [hypothesis]: #136
+#322 := (or #127 #123)
+#137 := (iff #127 #136)
+#48 := (= #47 f1)
+#46 := (= #45 f1)
+#49 := (iff #46 #48)
+#50 := (not #49)
+#140 := (iff #50 #137)
+#130 := (iff #123 #127)
+#133 := (not #130)
+#138 := (iff #133 #137)
+#139 := [rewrite]: #138
+#134 := (iff #50 #133)
+#131 := (iff #49 #130)
+#128 := (iff #48 #127)
+#129 := [rewrite]: #128
+#125 := (iff #46 #123)
+#126 := [rewrite]: #125
+#132 := [monotonicity #126 #129]: #131
+#135 := [monotonicity #132]: #134
+#141 := [trans #135 #139]: #140
+#122 := [asserted]: #50
+#144 := [mp #122 #141]: #137
+#234 := (not #137)
+#321 := (or #127 #123 #234)
+#235 := [def-axiom]: #321
+#236 := [unit-resolution #235 #144]: #322
+#631 := [unit-resolution #236 #630]: #127
+#307 := (or #323 #328)
+#633 := (or #123 #307)
+#644 := (not #307)
+#646 := (iff #123 #644)
+#22 := (:var 0 S3)
+#20 := (:var 1 S3)
+#34 := (f7 f9 #20)
+#35 := (f6 #34 #22)
+#18 := (:var 2 S2)
+#36 := (f3 #18 #35)
+#673 := (pattern #36)
+#28 := (f3 #18 #22)
+#96 := (= f1 #28)
+#169 := (not #96)
+#26 := (f3 #18 #20)
+#93 := (= f1 #26)
+#168 := (not #93)
+#152 := (or #168 #169)
+#153 := (not #152)
+#109 := (= f1 #36)
+#170 := (iff #109 #153)
+#674 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #673) #170)
+#173 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #170)
+#677 := (iff #173 #674)
+#675 := (iff #170 #170)
+#676 := [refl]: #675
+#678 := [quant-intro #676]: #677
+#113 := (and #93 #96)
+#116 := (iff #109 #113)
+#119 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #116)
+#174 := (iff #119 #173)
+#171 := (iff #116 #170)
+#154 := (iff #113 #153)
+#155 := [rewrite]: #154
+#172 := [monotonicity #155]: #171
+#175 := [quant-intro #172]: #174
+#150 := (~ #119 #119)
+#165 := (~ #116 #116)
+#166 := [refl]: #165
+#151 := [nnf-pos #166]: #150
+#29 := (= #28 f1)
+#27 := (= #26 f1)
+#38 := (and #27 #29)
+#37 := (= #36 f1)
+#39 := (iff #37 #38)
+#40 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #39)
+#120 := (iff #40 #119)
+#117 := (iff #39 #116)
+#114 := (iff #38 #113)
+#97 := (iff #29 #96)
+#98 := [rewrite]: #97
+#94 := (iff #27 #93)
+#95 := [rewrite]: #94
+#115 := [monotonicity #95 #98]: #114
+#111 := (iff #37 #109)
+#112 := [rewrite]: #111
+#118 := [monotonicity #112 #115]: #117
+#121 := [quant-intro #118]: #120
+#108 := [asserted]: #40
+#124 := [mp #108 #121]: #119
+#167 := [mp~ #124 #151]: #119
+#176 := [mp #167 #175]: #173
+#679 := [mp #176 #678]: #674
+#640 := (not #674)
+#312 := (or #640 #646)
+#313 := [quant-inst #41 #42 #14]: #312
+#632 := [unit-resolution #313 #679]: #646
+#641 := (not #646)
+#299 := (or #641 #123 #307)
+#304 := [def-axiom]: #299
+#628 := [unit-resolution #304 #632]: #633
+#634 := [unit-resolution #628 #630]: #307
+#645 := (or #644 #323 #328)
+#651 := [def-axiom]: #645
+#270 := [unit-resolution #651 #634 #631 #629]: false
+#635 := [lemma #270]: #123
+#326 := (or #323 #136)
+#314 := (or #323 #136 #234)
+#325 := [def-axiom]: #314
+#254 := [unit-resolution #325 #144]: #326
+#637 := [unit-resolution #254 #635]: #323
+#275 := (or #136 #644)
+#642 := (or #641 #136 #644)
+#300 := [def-axiom]: #642
+#276 := [unit-resolution #300 #632]: #275
+#638 := [unit-resolution #276 #635]: #644
+#647 := (or #307 #127)
+#648 := [def-axiom]: #647
+[unit-resolution #648 #638 #637]: false
+unsat
+fa1e213c15b8e9288bf16d2dc4bd96e3c7fb5c7e 173 0
+#2 := false
+decl f3 :: (-> S2 S3 S1)
+decl f6 :: (-> S4 S3 S3)
+decl f11 :: S3
+#42 := f11
+decl f7 :: (-> S5 S3 S4)
+decl f12 :: S3
+#44 := f12
+decl f9 :: S5
+#33 := f9
+#48 := (f7 f9 f12)
+#49 := (f6 #48 f11)
+decl f10 :: S2
+#41 := f10
+#50 := (f3 f10 #49)
+decl f1 :: S1
+#4 := f1
+#130 := (= f1 #50)
+#326 := (not #130)
+#43 := (f7 f9 f11)
+#45 := (f6 #43 f12)
+#46 := (f3 f10 #45)
+#126 := (= f1 #46)
+#139 := (not #126)
+#628 := [hypothesis]: #139
+#325 := (or #130 #126)
+#140 := (iff #130 #139)
+#51 := (= #50 f1)
+#47 := (= #46 f1)
+#52 := (iff #47 #51)
+#53 := (not #52)
+#143 := (iff #53 #140)
+#133 := (iff #126 #130)
+#136 := (not #133)
+#141 := (iff #136 #140)
+#142 := [rewrite]: #141
+#137 := (iff #53 #136)
+#134 := (iff #52 #133)
+#131 := (iff #51 #130)
+#132 := [rewrite]: #131
+#128 := (iff #47 #126)
+#129 := [rewrite]: #128
+#135 := [monotonicity #129 #132]: #134
+#138 := [monotonicity #135]: #137
+#144 := [trans #138 #142]: #143
+#125 := [asserted]: #53
+#147 := [mp #125 #144]: #140
+#237 := (not #140)
+#324 := (or #130 #126 #237)
+#238 := [def-axiom]: #324
+#239 := [unit-resolution #238 #147]: #325
+#629 := [unit-resolution #239 #628]: #130
+#310 := (f3 f10 f12)
+#647 := (= f1 #310)
+#649 := (not #647)
+#330 := (f3 f10 f11)
+#327 := (= f1 #330)
+#331 := (not #327)
+#315 := (or #331 #649)
+#626 := (or #126 #315)
+#651 := (not #315)
+#642 := (iff #126 #651)
+#22 := (:var 0 S3)
+#20 := (:var 1 S3)
+#34 := (f7 f9 #20)
+#35 := (f6 #34 #22)
+#18 := (:var 2 S2)
+#36 := (f3 #18 #35)
+#676 := (pattern #36)
+#28 := (f3 #18 #22)
+#99 := (= f1 #28)
+#172 := (not #99)
+#26 := (f3 #18 #20)
+#96 := (= f1 #26)
+#171 := (not #96)
+#155 := (or #171 #172)
+#156 := (not #155)
+#112 := (= f1 #36)
+#173 := (iff #112 #156)
+#677 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #676) #173)
+#176 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #173)
+#680 := (iff #176 #677)
+#678 := (iff #173 #173)
+#679 := [refl]: #678
+#681 := [quant-intro #679]: #680
+#116 := (and #96 #99)
+#119 := (iff #112 #116)
+#122 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #119)
+#177 := (iff #122 #176)
+#174 := (iff #119 #173)
+#157 := (iff #116 #156)
+#158 := [rewrite]: #157
+#175 := [monotonicity #158]: #174
+#178 := [quant-intro #175]: #177
+#153 := (~ #122 #122)
+#168 := (~ #119 #119)
+#169 := [refl]: #168
+#154 := [nnf-pos #169]: #153
+#29 := (= #28 f1)
+#27 := (= #26 f1)
+#38 := (and #27 #29)
+#37 := (= #36 f1)
+#39 := (iff #37 #38)
+#40 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #39)
+#123 := (iff #40 #122)
+#120 := (iff #39 #119)
+#117 := (iff #38 #116)
+#100 := (iff #29 #99)
+#101 := [rewrite]: #100
+#97 := (iff #27 #96)
+#98 := [rewrite]: #97
+#118 := [monotonicity #98 #101]: #117
+#114 := (iff #37 #112)
+#115 := [rewrite]: #114
+#121 := [monotonicity #115 #118]: #120
+#124 := [quant-intro #121]: #123
+#111 := [asserted]: #40
+#127 := [mp #111 #124]: #122
+#170 := [mp~ #127 #154]: #122
+#179 := [mp #170 #178]: #176
+#682 := [mp #179 #681]: #677
+#302 := (not #677)
+#335 := (or #302 #642)
+#351 := [quant-inst #41 #42 #44]: #335
+#622 := [unit-resolution #351 #682]: #642
+#352 := (not #642)
+#353 := (or #352 #126 #315)
+#339 := [def-axiom]: #353
+#623 := [unit-resolution #339 #622]: #626
+#627 := [unit-resolution #623 #628]: #315
+#337 := (or #326 #651)
+#648 := (iff #130 #651)
+#307 := (or #302 #648)
+#304 := (or #649 #331)
+#436 := (not #304)
+#643 := (iff #130 #436)
+#645 := (or #302 #643)
+#646 := (iff #645 #307)
+#630 := (iff #307 #307)
+#291 := [rewrite]: #630
+#654 := (iff #643 #648)
+#652 := (iff #436 #651)
+#316 := (iff #304 #315)
+#650 := [rewrite]: #316
+#653 := [monotonicity #650]: #652
+#644 := [monotonicity #653]: #654
+#287 := [monotonicity #644]: #646
+#292 := [trans #287 #291]: #646
+#303 := [quant-inst #41 #44 #42]: #645
+#293 := [mp #303 #292]: #307
+#336 := [unit-resolution #293 #682]: #648
+#631 := (not #648)
+#638 := (or #631 #326 #651)
+#640 := [def-axiom]: #638
+#338 := [unit-resolution #640 #336]: #337
+#340 := [unit-resolution #338 #627 #629]: false
+#618 := [lemma #340]: #126
+#329 := (or #326 #139)
+#317 := (or #326 #139 #237)
+#328 := [def-axiom]: #317
+#257 := [unit-resolution #328 #147]: #329
+#619 := [unit-resolution #257 #618]: #326
+#332 := (or #139 #651)
+#354 := (or #352 #139 #651)
+#245 := [def-axiom]: #354
+#616 := [unit-resolution #245 #622]: #332
+#620 := [unit-resolution #616 #618]: #651
+#617 := (or #130 #315)
+#637 := (or #631 #130 #315)
+#273 := [def-axiom]: #637
+#621 := [unit-resolution #273 #336]: #617
+[unit-resolution #621 #620 #619]: false
+unsat
+8424513290e59440c92fec106021e2354c2f6a1c 149 0
+#2 := false
+decl f3 :: (-> S2 S3 S1)
+decl f6 :: (-> S4 S3 S3)
+decl f11 :: S3
+#42 := f11
+decl f7 :: (-> S5 S3 S4)
+decl f9 :: S5
+#33 := f9
+#43 := (f7 f9 f11)
+#44 := (f6 #43 f11)
+decl f10 :: S2
+#41 := f10
+#45 := (f3 f10 #44)
+decl f1 :: S1
+#4 := f1
+#123 := (= f1 #45)
+#136 := (not #123)
+#632 := [hypothesis]: #136
+#47 := (f3 f10 f11)
+#127 := (= f1 #47)
+#322 := (or #127 #123)
+#137 := (iff #127 #136)
+#48 := (= #47 f1)
+#46 := (= #45 f1)
+#49 := (iff #46 #48)
+#50 := (not #49)
+#140 := (iff #50 #137)
+#130 := (iff #123 #127)
+#133 := (not #130)
+#138 := (iff #133 #137)
+#139 := [rewrite]: #138
+#134 := (iff #50 #133)
+#131 := (iff #49 #130)
+#128 := (iff #48 #127)
+#129 := [rewrite]: #128
+#125 := (iff #46 #123)
+#126 := [rewrite]: #125
+#132 := [monotonicity #126 #129]: #131
+#135 := [monotonicity #132]: #134
+#141 := [trans #135 #139]: #140
+#122 := [asserted]: #50
+#144 := [mp #122 #141]: #137
+#234 := (not #137)
+#321 := (or #127 #123 #234)
+#235 := [def-axiom]: #321
+#236 := [unit-resolution #235 #144]: #322
+#633 := [unit-resolution #236 #632]: #127
+#323 := (not #127)
+#634 := (or #123 #323)
+#22 := (:var 0 S3)
+#20 := (:var 1 S3)
+#34 := (f7 f9 #20)
+#35 := (f6 #34 #22)
+#18 := (:var 2 S2)
+#36 := (f3 #18 #35)
+#673 := (pattern #36)
+#28 := (f3 #18 #22)
+#96 := (= f1 #28)
+#169 := (not #96)
+#26 := (f3 #18 #20)
+#93 := (= f1 #26)
+#168 := (not #93)
+#152 := (or #168 #169)
+#153 := (not #152)
+#109 := (= f1 #36)
+#170 := (iff #109 #153)
+#674 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #673) #170)
+#173 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #170)
+#677 := (iff #173 #674)
+#675 := (iff #170 #170)
+#676 := [refl]: #675
+#678 := [quant-intro #676]: #677
+#113 := (and #93 #96)
+#116 := (iff #109 #113)
+#119 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #116)
+#174 := (iff #119 #173)
+#171 := (iff #116 #170)
+#154 := (iff #113 #153)
+#155 := [rewrite]: #154
+#172 := [monotonicity #155]: #171
+#175 := [quant-intro #172]: #174
+#150 := (~ #119 #119)
+#165 := (~ #116 #116)
+#166 := [refl]: #165
+#151 := [nnf-pos #166]: #150
+#29 := (= #28 f1)
+#27 := (= #26 f1)
+#38 := (and #27 #29)
+#37 := (= #36 f1)
+#39 := (iff #37 #38)
+#40 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #39)
+#120 := (iff #40 #119)
+#117 := (iff #39 #116)
+#114 := (iff #38 #113)
+#97 := (iff #29 #96)
+#98 := [rewrite]: #97
+#94 := (iff #27 #93)
+#95 := [rewrite]: #94
+#115 := [monotonicity #95 #98]: #114
+#111 := (iff #37 #109)
+#112 := [rewrite]: #111
+#118 := [monotonicity #112 #115]: #117
+#121 := [quant-intro #118]: #120
+#108 := [asserted]: #40
+#124 := [mp #108 #121]: #119
+#167 := [mp~ #124 #151]: #119
+#176 := [mp #167 #175]: #173
+#679 := [mp #176 #678]: #674
+#650 := (not #674)
+#645 := (or #650 #130)
+#327 := (or #323 #323)
+#324 := (not #327)
+#328 := (iff #123 #324)
+#651 := (or #650 #328)
+#299 := (iff #651 #645)
+#642 := (iff #645 #645)
+#300 := [rewrite]: #642
+#648 := (iff #328 #130)
+#313 := (iff #324 #127)
+#646 := (not #323)
+#640 := (iff #646 #127)
+#312 := [rewrite]: #640
+#301 := (iff #324 #646)
+#307 := (iff #327 #323)
+#644 := [rewrite]: #307
+#433 := [monotonicity #644]: #301
+#647 := [trans #433 #312]: #313
+#649 := [monotonicity #647]: #648
+#304 := [monotonicity #649]: #299
+#643 := [trans #304 #300]: #299
+#641 := [quant-inst #41 #42 #42]: #651
+#284 := [mp #641 #643]: #645
+#628 := [unit-resolution #284 #679]: #130
+#627 := (or #133 #123 #323)
+#288 := [def-axiom]: #627
+#270 := [unit-resolution #288 #628]: #634
+#635 := [unit-resolution #270 #633 #632]: false
+#637 := [lemma #635]: #123
+#326 := (or #323 #136)
+#314 := (or #323 #136 #234)
+#325 := [def-axiom]: #314
+#254 := [unit-resolution #325 #144]: #326
+#275 := [unit-resolution #254 #637]: #323
+#276 := (or #136 #127)
+#289 := (or #133 #136 #127)
+#290 := [def-axiom]: #289
+#638 := [unit-resolution #290 #628]: #276
+[unit-resolution #638 #275 #637]: false
+unsat
+5973328496eea1e33493c38f9af9d86965f67ad9 287 0
+#2 := false
+decl f3 :: (-> S2 S3 S1)
+decl f6 :: (-> S4 S3 S3)
+decl f12 :: S3
+#44 := f12
+decl f7 :: (-> S5 S3 S4)
+decl f11 :: S3
+#42 := f11
+decl f9 :: S5
+#33 := f9
+#43 := (f7 f9 f11)
+#51 := (f6 #43 f12)
+decl f10 :: S2
+#41 := f10
+#314 := (f3 f10 #51)
+decl f1 :: S1
+#4 := f1
+#651 := (= f1 #314)
+#249 := (f3 f10 f12)
+#628 := (= f1 #249)
+#625 := (not #628)
+#339 := (f3 f10 f11)
+#355 := (= f1 #339)
+#356 := (not #355)
+#614 := (or #356 #625)
+#615 := (not #614)
+#611 := (iff #615 #651)
+#582 := (not #611)
+decl f13 :: S3
+#46 := f13
+#334 := (f3 f10 f13)
+#331 := (= f1 #334)
+#335 := (not #331)
+#484 := (or #335 #625)
+#493 := (not #484)
+#45 := (f7 f9 f12)
+#47 := (f6 #45 f13)
+#646 := (f3 f10 #47)
+#632 := (= f1 #646)
+#494 := (iff #493 #632)
+#587 := (not #494)
+#567 := [hypothesis]: #587
+#22 := (:var 0 S3)
+#20 := (:var 1 S3)
+#34 := (f7 f9 #20)
+#35 := (f6 #34 #22)
+#18 := (:var 2 S2)
+#36 := (f3 #18 #35)
+#680 := (pattern #36)
+#28 := (f3 #18 #22)
+#103 := (= f1 #28)
+#176 := (not #103)
+#26 := (f3 #18 #20)
+#100 := (= f1 #26)
+#175 := (not #100)
+#159 := (or #175 #176)
+#160 := (not #159)
+#116 := (= f1 #36)
+#177 := (iff #116 #160)
+#681 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #680) #177)
+#180 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #177)
+#684 := (iff #180 #681)
+#682 := (iff #177 #177)
+#683 := [refl]: #682
+#685 := [quant-intro #683]: #684
+#120 := (and #100 #103)
+#123 := (iff #116 #120)
+#126 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #123)
+#181 := (iff #126 #180)
+#178 := (iff #123 #177)
+#161 := (iff #120 #160)
+#162 := [rewrite]: #161
+#179 := [monotonicity #162]: #178
+#182 := [quant-intro #179]: #181
+#157 := (~ #126 #126)
+#172 := (~ #123 #123)
+#173 := [refl]: #172
+#158 := [nnf-pos #173]: #157
+#29 := (= #28 f1)
+#27 := (= #26 f1)
+#38 := (and #27 #29)
+#37 := (= #36 f1)
+#39 := (iff #37 #38)
+#40 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #39)
+#127 := (iff #40 #126)
+#124 := (iff #39 #123)
+#121 := (iff #38 #120)
+#104 := (iff #29 #103)
+#105 := [rewrite]: #104
+#101 := (iff #27 #100)
+#102 := [rewrite]: #101
+#122 := [monotonicity #102 #105]: #121
+#118 := (iff #37 #116)
+#119 := [rewrite]: #118
+#125 := [monotonicity #119 #122]: #124
+#128 := [quant-intro #125]: #127
+#115 := [asserted]: #40
+#131 := [mp #115 #128]: #126
+#174 := [mp~ #131 #158]: #126
+#183 := [mp #174 #182]: #180
+#686 := [mp #183 #685]: #681
+#306 := (not #681)
+#498 := (or #306 #494)
+#600 := (or #625 #335)
+#482 := (not #600)
+#483 := (iff #632 #482)
+#499 := (or #306 #483)
+#593 := (iff #499 #498)
+#594 := (iff #498 #498)
+#581 := [rewrite]: #594
+#496 := (iff #483 #494)
+#592 := (iff #632 #493)
+#495 := (iff #592 #494)
+#488 := [rewrite]: #495
+#477 := (iff #483 #592)
+#588 := (iff #482 #493)
+#443 := (iff #600 #484)
+#591 := [rewrite]: #443
+#589 := [monotonicity #591]: #588
+#492 := [monotonicity #589]: #477
+#497 := [trans #492 #488]: #496
+#590 := [monotonicity #497]: #593
+#583 := [trans #590 #581]: #593
+#500 := [quant-inst #41 #44 #46]: #499
+#575 := [mp #500 #583]: #498
+#568 := [unit-resolution #575 #686 #567]: false
+#569 := [lemma #568]: #494
+#633 := (not #632)
+#357 := (or #356 #633)
+#343 := (not #357)
+#48 := (f6 #43 #47)
+#49 := (f3 f10 #48)
+#130 := (= f1 #49)
+#143 := (not #130)
+#570 := [hypothesis]: #143
+#571 := (or #130 #357)
+#358 := (iff #130 #343)
+#629 := (or #306 #358)
+#351 := [quant-inst #41 #42 #47]: #629
+#566 := [unit-resolution #351 #686]: #358
+#341 := (not #358)
+#342 := (or #341 #130 #357)
+#344 := [def-axiom]: #342
+#557 := [unit-resolution #344 #566]: #571
+#558 := [unit-resolution #557 #570]: #357
+#597 := (or #306 #611)
+#616 := (iff #651 #615)
+#613 := (or #306 #616)
+#618 := (iff #613 #597)
+#461 := (iff #597 #597)
+#462 := [rewrite]: #461
+#612 := (iff #616 #611)
+#617 := [rewrite]: #612
+#460 := [monotonicity #617]: #618
+#604 := [trans #460 #462]: #618
+#619 := [quant-inst #41 #42 #44]: #613
+#605 := [mp #619 #604]: #597
+#560 := [unit-resolution #605 #686]: #611
+#546 := (or #582 #615)
+#653 := (not #651)
+#319 := (or #335 #653)
+#655 := (not #319)
+#52 := (f7 f9 #51)
+#53 := (f6 #52 f13)
+#54 := (f3 f10 #53)
+#134 := (= f1 #54)
+#329 := (or #134 #130)
+#144 := (iff #134 #143)
+#55 := (= #54 f1)
+#50 := (= #49 f1)
+#56 := (iff #50 #55)
+#57 := (not #56)
+#147 := (iff #57 #144)
+#137 := (iff #130 #134)
+#140 := (not #137)
+#145 := (iff #140 #144)
+#146 := [rewrite]: #145
+#141 := (iff #57 #140)
+#138 := (iff #56 #137)
+#135 := (iff #55 #134)
+#136 := [rewrite]: #135
+#132 := (iff #50 #130)
+#133 := [rewrite]: #132
+#139 := [monotonicity #133 #136]: #138
+#142 := [monotonicity #139]: #141
+#148 := [trans #142 #146]: #147
+#129 := [asserted]: #57
+#151 := [mp #129 #148]: #144
+#241 := (not #144)
+#328 := (or #134 #130 #241)
+#242 := [def-axiom]: #328
+#243 := [unit-resolution #242 #151]: #329
+#561 := [unit-resolution #243 #570]: #134
+#330 := (not #134)
+#559 := (or #330 #655)
+#652 := (iff #134 #655)
+#311 := (or #306 #652)
+#308 := (or #653 #335)
+#440 := (not #308)
+#647 := (iff #134 #440)
+#649 := (or #306 #647)
+#650 := (iff #649 #311)
+#634 := (iff #311 #311)
+#295 := [rewrite]: #634
+#658 := (iff #647 #652)
+#656 := (iff #440 #655)
+#320 := (iff #308 #319)
+#654 := [rewrite]: #320
+#657 := [monotonicity #654]: #656
+#648 := [monotonicity #657]: #658
+#291 := [monotonicity #648]: #650
+#296 := [trans #291 #295]: #650
+#307 := [quant-inst #41 #51 #46]: #649
+#297 := [mp #307 #296]: #311
+#562 := [unit-resolution #297 #686]: #652
+#635 := (not #652)
+#642 := (or #635 #330 #655)
+#644 := [def-axiom]: #642
+#563 := [unit-resolution #644 #562]: #559
+#543 := [unit-resolution #563 #561]: #655
+#637 := (or #319 #651)
+#638 := [def-axiom]: #637
+#544 := [unit-resolution #638 #543]: #651
+#576 := (or #582 #615 #653)
+#577 := [def-axiom]: #576
+#547 := [unit-resolution #577 #544]: #546
+#548 := [unit-resolution #547 #560]: #615
+#606 := (or #614 #355)
+#572 := [def-axiom]: #606
+#549 := [unit-resolution #572 #548]: #355
+#631 := (or #343 #356 #633)
+#340 := [def-axiom]: #631
+#550 := [unit-resolution #340 #549 #558]: #633
+#298 := (or #319 #331)
+#636 := [def-axiom]: #298
+#551 := [unit-resolution #636 #543]: #331
+#574 := (or #614 #628)
+#584 := [def-axiom]: #574
+#552 := [unit-resolution #584 #548]: #628
+#609 := (or #493 #335 #625)
+#603 := [def-axiom]: #609
+#553 := [unit-resolution #603 #552 #551]: #493
+#441 := (or #587 #484 #632)
+#442 := [def-axiom]: #441
+#554 := [unit-resolution #442 #553 #550 #569]: false
+#555 := [lemma #554]: #130
+#545 := (or #143 #343)
+#622 := (or #341 #143 #343)
+#623 := [def-axiom]: #622
+#556 := [unit-resolution #623 #566]: #545
+#534 := [unit-resolution #556 #555]: #343
+#630 := (or #357 #632)
+#627 := [def-axiom]: #630
+#535 := [unit-resolution #627 #534]: #632
+#610 := (or #587 #493 #633)
+#439 := [def-axiom]: #610
+#537 := [unit-resolution #439 #535 #569]: #493
+#602 := (or #484 #628)
+#608 := [def-axiom]: #602
+#538 := [unit-resolution #608 #537]: #628
+#352 := (or #357 #355)
+#626 := [def-axiom]: #352
+#539 := [unit-resolution #626 #534]: #355
+#585 := (or #615 #356 #625)
+#586 := [def-axiom]: #585
+#540 := [unit-resolution #586 #539 #538]: #615
+#333 := (or #330 #143)
+#321 := (or #330 #143 #241)
+#332 := [def-axiom]: #321
+#261 := [unit-resolution #332 #151]: #333
+#541 := [unit-resolution #261 #555]: #330
+#536 := (or #134 #319)
+#641 := (or #635 #134 #319)
+#277 := [def-axiom]: #641
+#542 := [unit-resolution #277 #562]: #536
+#528 := [unit-resolution #542 #541]: #319
+#607 := (or #484 #331)
+#601 := [def-axiom]: #607
+#524 := [unit-resolution #601 #537]: #331
+#639 := (or #655 #335 #653)
+#640 := [def-axiom]: #639
+#525 := [unit-resolution #640 #524 #528]: #653
+#578 := (or #582 #614 #651)
+#579 := [def-axiom]: #578
+#526 := [unit-resolution #579 #525 #540]: #582
+[unit-resolution #605 #686 #526]: false
+unsat
+6c759b8f06a9510b6e4f2c41f45fd7a908ea138f 22 0
+#2 := false
+decl f13 :: (-> S7 S3 S4)
+decl f4 :: S3
+#8 := f4
+decl f14 :: S7
+#50 := f14
+#51 := (f13 f14 f4)
+#52 := (= #51 #51)
+#53 := (not #52)
+#148 := (iff #53 false)
+#1 := true
+#143 := (not true)
+#146 := (iff #143 false)
+#147 := [rewrite]: #146
+#144 := (iff #53 #143)
+#140 := (iff #52 true)
+#142 := [rewrite]: #140
+#145 := [monotonicity #142]: #144
+#149 := [trans #145 #147]: #148
+#139 := [asserted]: #53
+[mp #139 #149]: false
+unsat
+eac8197a82f6b3a5c2024430d69641bb761b0abc 60 0
+#2 := false
+decl f3 :: (-> S2 S3 S1)
+decl f4 :: S3
+#9 := f4
+decl f10 :: S2
+#41 := f10
+#42 := (f3 f10 f4)
+decl f1 :: S1
+#4 := f1
+#118 := (= f1 #42)
+#43 := (= #42 f1)
+#44 := (not #43)
+#45 := (not #44)
+#130 := (iff #45 #118)
+#122 := (not #118)
+#125 := (not #122)
+#128 := (iff #125 #118)
+#129 := [rewrite]: #128
+#126 := (iff #45 #125)
+#123 := (iff #44 #122)
+#120 := (iff #43 #118)
+#121 := [rewrite]: #120
+#124 := [monotonicity #121]: #123
+#127 := [monotonicity #124]: #126
+#131 := [trans #127 #129]: #130
+#117 := [asserted]: #45
+#134 := [mp #117 #131]: #118
+#8 := (:var 0 S2)
+#10 := (f3 #8 f4)
+#642 := (pattern #10)
+#66 := (= f1 #10)
+#69 := (not #66)
+#643 := (forall (vars (?v0 S2)) (:pat #642) #69)
+#72 := (forall (vars (?v0 S2)) #69)
+#646 := (iff #72 #643)
+#644 := (iff #69 #69)
+#645 := [refl]: #644
+#647 := [quant-intro #645]: #646
+#148 := (~ #72 #72)
+#146 := (~ #69 #69)
+#147 := [refl]: #146
+#149 := [nnf-pos #147]: #148
+#11 := (= #10 f1)
+#12 := (not #11)
+#13 := (forall (vars (?v0 S2)) #12)
+#73 := (iff #13 #72)
+#70 := (iff #12 #69)
+#67 := (iff #11 #66)
+#68 := [rewrite]: #67
+#71 := [monotonicity #68]: #70
+#74 := [quant-intro #71]: #73
+#65 := [asserted]: #13
+#77 := [mp #65 #74]: #72
+#133 := [mp~ #77 #149]: #72
+#648 := [mp #133 #647]: #643
+#225 := (not #643)
+#312 := (or #225 #122)
+#226 := [quant-inst #41]: #312
+[unit-resolution #226 #648 #134]: false
+unsat
+32295808d649b2df10d022ec20bfa2f501001522 48 0
+#2 := false
+decl f3 :: (-> S2 S3 S1)
+decl f5 :: S3
+#14 := f5
+decl f10 :: S2
+#41 := f10
+#42 := (f3 f10 f5)
+decl f1 :: S1
+#4 := f1
+#117 := (= f1 #42)
+#121 := (not #117)
+#43 := (= #42 f1)
+#44 := (not #43)
+#122 := (iff #44 #121)
+#119 := (iff #43 #117)
+#120 := [rewrite]: #119
+#123 := [monotonicity #120]: #122
+#116 := [asserted]: #44
+#126 := [mp #116 #123]: #121
+#8 := (:var 0 S2)
+#15 := (f3 #8 f5)
+#641 := (pattern #15)
+#75 := (= f1 #15)
+#642 := (forall (vars (?v0 S2)) (:pat #641) #75)
+#79 := (forall (vars (?v0 S2)) #75)
+#645 := (iff #79 #642)
+#643 := (iff #75 #75)
+#644 := [refl]: #643
+#646 := [quant-intro #644]: #645
+#128 := (~ #79 #79)
+#127 := (~ #75 #75)
+#142 := [refl]: #127
+#129 := [nnf-pos #142]: #128
+#16 := (= #15 f1)
+#17 := (forall (vars (?v0 S2)) #16)
+#80 := (iff #17 #79)
+#77 := (iff #16 #75)
+#78 := [rewrite]: #77
+#81 := [quant-intro #78]: #80
+#74 := [asserted]: #17
+#84 := [mp #74 #81]: #79
+#143 := [mp~ #84 #129]: #79
+#647 := [mp #143 #646]: #642
+#217 := (not #642)
+#304 := (or #217 #117)
+#218 := [quant-inst #41]: #304
+[unit-resolution #218 #647 #126]: false
+unsat
+dfe83e391823f1cbfcca9d6fb06c0ae74a22248a 126 0
+#2 := false
+decl f3 :: (-> S2 S3 S1)
+decl f6 :: (-> S4 S3 S3)
+decl f12 :: S3
+#44 := f12
+decl f7 :: (-> S5 S3 S4)
+decl f11 :: S3
+#42 := f11
+decl f8 :: S5
+#19 := f8
+#43 := (f7 f8 f11)
+#45 := (f6 #43 f12)
+decl f10 :: S2
+#41 := f10
+#46 := (f3 f10 #45)
+decl f1 :: S1
+#4 := f1
+#127 := (= f1 #46)
+#146 := (not #127)
+#650 := [hypothesis]: #146
+#50 := (f3 f10 f12)
+#134 := (= f1 #50)
+#48 := (f3 f10 f11)
+#131 := (= f1 #48)
+#137 := (or #131 #134)
+#338 := (or #137 #127)
+#147 := (iff #137 #146)
+#51 := (= #50 f1)
+#49 := (= #48 f1)
+#52 := (or #49 #51)
+#47 := (= #46 f1)
+#53 := (iff #47 #52)
+#54 := (not #53)
+#150 := (iff #54 #147)
+#140 := (iff #127 #137)
+#143 := (not #140)
+#148 := (iff #143 #147)
+#149 := [rewrite]: #148
+#144 := (iff #54 #143)
+#141 := (iff #53 #140)
+#138 := (iff #52 #137)
+#135 := (iff #51 #134)
+#136 := [rewrite]: #135
+#132 := (iff #49 #131)
+#133 := [rewrite]: #132
+#139 := [monotonicity #133 #136]: #138
+#129 := (iff #47 #127)
+#130 := [rewrite]: #129
+#142 := [monotonicity #130 #139]: #141
+#145 := [monotonicity #142]: #144
+#151 := [trans #145 #149]: #150
+#126 := [asserted]: #54
+#154 := [mp #126 #151]: #147
+#264 := (not #147)
+#337 := (or #137 #127 #264)
+#334 := [def-axiom]: #337
+#317 := [unit-resolution #334 #154]: #338
+#322 := [unit-resolution #317 #650]: #137
+#324 := (not #137)
+#653 := (or #127 #324)
+#22 := (:var 0 S3)
+#20 := (:var 1 S3)
+#21 := (f7 f8 #20)
+#23 := (f6 #21 #22)
+#18 := (:var 2 S2)
+#24 := (f3 #18 #23)
+#676 := (pattern #24)
+#28 := (f3 #18 #22)
+#100 := (= f1 #28)
+#26 := (f3 #18 #20)
+#97 := (= f1 #26)
+#103 := (or #97 #100)
+#93 := (= f1 #24)
+#106 := (iff #93 #103)
+#677 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #676) #106)
+#109 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #106)
+#680 := (iff #109 #677)
+#678 := (iff #106 #106)
+#679 := [refl]: #678
+#681 := [quant-intro #679]: #680
+#158 := (~ #109 #109)
+#172 := (~ #106 #106)
+#173 := [refl]: #172
+#159 := [nnf-pos #173]: #158
+#29 := (= #28 f1)
+#27 := (= #26 f1)
+#30 := (or #27 #29)
+#25 := (= #24 f1)
+#31 := (iff #25 #30)
+#32 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #31)
+#110 := (iff #32 #109)
+#107 := (iff #31 #106)
+#104 := (iff #30 #103)
+#101 := (iff #29 #100)
+#102 := [rewrite]: #101
+#98 := (iff #27 #97)
+#99 := [rewrite]: #98
+#105 := [monotonicity #99 #102]: #104
+#95 := (iff #25 #93)
+#96 := [rewrite]: #95
+#108 := [monotonicity #96 #105]: #107
+#111 := [quant-intro #108]: #110
+#92 := [asserted]: #32
+#114 := [mp #92 #111]: #109
+#174 := [mp~ #114 #159]: #109
+#682 := [mp #174 #681]: #677
+#323 := (not #677)
+#657 := (or #323 #140)
+#658 := [quant-inst #41 #42 #44]: #657
+#310 := [unit-resolution #658 #682]: #140
+#659 := (or #143 #127 #324)
+#660 := [def-axiom]: #659
+#294 := [unit-resolution #660 #310]: #653
+#637 := [unit-resolution #294 #322 #650]: false
+#298 := [lemma #637]: #127
+#311 := (or #324 #146)
+#654 := (or #324 #146 #264)
+#656 := [def-axiom]: #654
+#443 := [unit-resolution #656 #154]: #311
+#299 := [unit-resolution #443 #298]: #324
+#300 := (or #146 #137)
+#655 := (or #143 #146 #137)
+#661 := [def-axiom]: #655
+#301 := [unit-resolution #661 #310]: #300
+[unit-resolution #301 #299 #298]: false
+unsat
+54d5adcc9aa92b5c35a0e590a6651cbf7d0b828e 162 0
+#2 := false
+decl f3 :: (-> S2 S3 S1)
+decl f4 :: S3
+#9 := f4
+decl f10 :: S2
+#41 := f10
+#327 := (f3 f10 f4)
+decl f1 :: S1
+#4 := f1
+#324 := (= f1 #327)
+decl f11 :: S3
+#42 := f11
+#47 := (f3 f10 f11)
+#127 := (= f1 #47)
+#328 := (or #127 #324)
+decl f6 :: (-> S4 S3 S3)
+decl f7 :: (-> S5 S3 S4)
+decl f8 :: S5
+#19 := f8
+#43 := (f7 f8 f11)
+#44 := (f6 #43 f4)
+#45 := (f3 f10 #44)
+#123 := (= f1 #45)
+#136 := (not #123)
+#644 := [hypothesis]: #136
+#322 := (or #127 #123)
+#137 := (iff #127 #136)
+#48 := (= #47 f1)
+#46 := (= #45 f1)
+#49 := (iff #46 #48)
+#50 := (not #49)
+#140 := (iff #50 #137)
+#130 := (iff #123 #127)
+#133 := (not #130)
+#138 := (iff #133 #137)
+#139 := [rewrite]: #138
+#134 := (iff #50 #133)
+#131 := (iff #49 #130)
+#128 := (iff #48 #127)
+#129 := [rewrite]: #128
+#125 := (iff #46 #123)
+#126 := [rewrite]: #125
+#132 := [monotonicity #126 #129]: #131
+#135 := [monotonicity #132]: #134
+#141 := [trans #135 #139]: #140
+#122 := [asserted]: #50
+#144 := [mp #122 #141]: #137
+#234 := (not #137)
+#321 := (or #127 #123 #234)
+#235 := [def-axiom]: #321
+#236 := [unit-resolution #235 #144]: #322
+#646 := [unit-resolution #236 #644]: #127
+#650 := (not #328)
+#290 := (or #123 #650)
+#307 := (iff #123 #328)
+#22 := (:var 0 S3)
+#20 := (:var 1 S3)
+#21 := (f7 f8 #20)
+#23 := (f6 #21 #22)
+#18 := (:var 2 S2)
+#24 := (f3 #18 #23)
+#666 := (pattern #24)
+#28 := (f3 #18 #22)
+#96 := (= f1 #28)
+#26 := (f3 #18 #20)
+#93 := (= f1 #26)
+#99 := (or #93 #96)
+#89 := (= f1 #24)
+#102 := (iff #89 #99)
+#667 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #666) #102)
+#105 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #102)
+#670 := (iff #105 #667)
+#668 := (iff #102 #102)
+#669 := [refl]: #668
+#671 := [quant-intro #669]: #670
+#148 := (~ #105 #105)
+#162 := (~ #102 #102)
+#163 := [refl]: #162
+#149 := [nnf-pos #163]: #148
+#29 := (= #28 f1)
+#27 := (= #26 f1)
+#30 := (or #27 #29)
+#25 := (= #24 f1)
+#31 := (iff #25 #30)
+#32 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #31)
+#106 := (iff #32 #105)
+#103 := (iff #31 #102)
+#100 := (iff #30 #99)
+#97 := (iff #29 #96)
+#98 := [rewrite]: #97
+#94 := (iff #27 #93)
+#95 := [rewrite]: #94
+#101 := [monotonicity #95 #98]: #100
+#91 := (iff #25 #89)
+#92 := [rewrite]: #91
+#104 := [monotonicity #92 #101]: #103
+#107 := [quant-intro #104]: #106
+#88 := [asserted]: #32
+#110 := [mp #88 #107]: #105
+#164 := [mp~ #110 #149]: #105
+#672 := [mp #164 #671]: #667
+#301 := (not #667)
+#433 := (or #301 #307)
+#640 := [quant-inst #41 #42 #9]: #433
+#289 := [unit-resolution #640 #672]: #307
+#641 := (not #307)
+#299 := (or #641 #123 #650)
+#304 := [def-axiom]: #299
+#291 := [unit-resolution #304 #289]: #290
+#629 := [unit-resolution #291 #644]: #650
+#323 := (not #127)
+#312 := (or #328 #323)
+#313 := [def-axiom]: #312
+#630 := [unit-resolution #313 #629 #646]: false
+#631 := [lemma #630]: #123
+#632 := (or #136 #328)
+#642 := (or #641 #136 #328)
+#300 := [def-axiom]: #642
+#633 := [unit-resolution #300 #289]: #632
+#635 := [unit-resolution #633 #631]: #328
+#326 := (or #323 #136)
+#314 := (or #323 #136 #234)
+#325 := [def-axiom]: #314
+#254 := [unit-resolution #325 #144]: #326
+#637 := [unit-resolution #254 #631]: #323
+#645 := (or #650 #127 #324)
+#651 := [def-axiom]: #645
+#275 := [unit-resolution #651 #637 #635]: #324
+#8 := (:var 0 S2)
+#10 := (f3 #8 f4)
+#652 := (pattern #10)
+#71 := (= f1 #10)
+#74 := (not #71)
+#653 := (forall (vars (?v0 S2)) (:pat #652) #74)
+#77 := (forall (vars (?v0 S2)) #74)
+#656 := (iff #77 #653)
+#654 := (iff #74 #74)
+#655 := [refl]: #654
+#657 := [quant-intro #655]: #656
+#158 := (~ #77 #77)
+#156 := (~ #74 #74)
+#157 := [refl]: #156
+#159 := [nnf-pos #157]: #158
+#11 := (= #10 f1)
+#12 := (not #11)
+#13 := (forall (vars (?v0 S2)) #12)
+#78 := (iff #13 #77)
+#75 := (iff #12 #74)
+#72 := (iff #11 #71)
+#73 := [rewrite]: #72
+#76 := [monotonicity #73]: #75
+#79 := [quant-intro #76]: #78
+#70 := [asserted]: #13
+#82 := [mp #70 #79]: #77
+#143 := [mp~ #82 #159]: #77
+#658 := [mp #143 #657]: #653
+#647 := (not #324)
+#628 := (not #653)
+#634 := (or #628 #647)
+#270 := [quant-inst #41]: #634
+[unit-resolution #270 #658 #275]: false
+unsat
+6579b339206079120a92afc0dda92279c34507ae 136 0
+#2 := false
+decl f3 :: (-> S2 S3 S1)
+decl f5 :: S3
+#14 := f5
+decl f10 :: S2
+#41 := f10
+#219 := (f3 f10 f5)
+decl f1 :: S1
+#4 := f1
+#306 := (= f1 #219)
+#633 := (not #306)
+decl f11 :: S3
+#42 := f11
+#220 := (f3 f10 f11)
+#307 := (= f1 #220)
+#299 := (or #306 #307)
+#284 := (not #299)
+decl f6 :: (-> S4 S3 S3)
+decl f7 :: (-> S5 S3 S4)
+decl f8 :: S5
+#19 := f8
+#43 := (f7 f8 f11)
+#44 := (f6 #43 f5)
+#45 := (f3 f10 #44)
+#120 := (= f1 #45)
+#239 := (iff #120 #299)
+#22 := (:var 0 S3)
+#20 := (:var 1 S3)
+#21 := (f7 f8 #20)
+#23 := (f6 #21 #22)
+#18 := (:var 2 S2)
+#24 := (f3 #18 #23)
+#651 := (pattern #24)
+#28 := (f3 #18 #22)
+#93 := (= f1 #28)
+#26 := (f3 #18 #20)
+#90 := (= f1 #26)
+#96 := (or #90 #93)
+#86 := (= f1 #24)
+#99 := (iff #86 #96)
+#652 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #651) #99)
+#102 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #99)
+#655 := (iff #102 #652)
+#653 := (iff #99 #99)
+#654 := [refl]: #653
+#656 := [quant-intro #654]: #655
+#133 := (~ #102 #102)
+#147 := (~ #99 #99)
+#148 := [refl]: #147
+#134 := [nnf-pos #148]: #133
+#29 := (= #28 f1)
+#27 := (= #26 f1)
+#30 := (or #27 #29)
+#25 := (= #24 f1)
+#31 := (iff #25 #30)
+#32 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #31)
+#103 := (iff #32 #102)
+#100 := (iff #31 #99)
+#97 := (iff #30 #96)
+#94 := (iff #29 #93)
+#95 := [rewrite]: #94
+#91 := (iff #27 #90)
+#92 := [rewrite]: #91
+#98 := [monotonicity #92 #95]: #97
+#88 := (iff #25 #86)
+#89 := [rewrite]: #88
+#101 := [monotonicity #89 #98]: #100
+#104 := [quant-intro #101]: #103
+#85 := [asserted]: #32
+#107 := [mp #85 #104]: #102
+#149 := [mp~ #107 #134]: #102
+#657 := [mp #149 #656]: #652
+#313 := (not #652)
+#292 := (or #313 #239)
+#221 := (or #307 #306)
+#308 := (iff #120 #221)
+#629 := (or #313 #308)
+#286 := (iff #629 #292)
+#625 := (iff #292 #292)
+#297 := [rewrite]: #625
+#312 := (iff #308 #239)
+#310 := (iff #221 #299)
+#311 := [rewrite]: #310
+#309 := [monotonicity #311]: #312
+#418 := [monotonicity #309]: #286
+#298 := [trans #418 #297]: #286
+#631 := [quant-inst #41 #42 #14]: #629
+#632 := [mp #631 #298]: #292
+#615 := [unit-resolution #632 #657]: #239
+#285 := (not #239)
+#616 := (or #285 #284)
+#124 := (not #120)
+#46 := (= #45 f1)
+#47 := (not #46)
+#125 := (iff #47 #124)
+#122 := (iff #46 #120)
+#123 := [rewrite]: #122
+#126 := [monotonicity #123]: #125
+#119 := [asserted]: #47
+#129 := [mp #119 #126]: #124
+#628 := (or #285 #120 #284)
+#269 := [def-axiom]: #628
+#619 := [unit-resolution #269 #129]: #616
+#255 := [unit-resolution #619 #615]: #284
+#634 := (or #299 #633)
+#635 := [def-axiom]: #634
+#620 := [unit-resolution #635 #255]: #633
+#8 := (:var 0 S2)
+#15 := (f3 #8 f5)
+#644 := (pattern #15)
+#78 := (= f1 #15)
+#645 := (forall (vars (?v0 S2)) (:pat #644) #78)
+#82 := (forall (vars (?v0 S2)) #78)
+#648 := (iff #82 #645)
+#646 := (iff #78 #78)
+#647 := [refl]: #646
+#649 := [quant-intro #647]: #648
+#131 := (~ #82 #82)
+#130 := (~ #78 #78)
+#145 := [refl]: #130
+#132 := [nnf-pos #145]: #131
+#16 := (= #15 f1)
+#17 := (forall (vars (?v0 S2)) #16)
+#83 := (iff #17 #82)
+#80 := (iff #16 #78)
+#81 := [rewrite]: #80
+#84 := [quant-intro #81]: #83
+#77 := [asserted]: #17
+#87 := [mp #77 #84]: #82
+#146 := [mp~ #87 #132]: #82
+#650 := [mp #146 #649]: #645
+#617 := (not #645)
+#618 := (or #617 #306)
+#613 := [quant-inst #41]: #618
+[unit-resolution #613 #650 #620]: false
+unsat
+21f3225a60811428730067e610d6913c3bcb0df3 155 0
+#2 := false
+decl f3 :: (-> S2 S3 S1)
+decl f6 :: (-> S4 S3 S3)
+decl f11 :: S3
+#42 := f11
+decl f7 :: (-> S5 S3 S4)
+decl f12 :: S3
+#44 := f12
+decl f8 :: S5
+#19 := f8
+#48 := (f7 f8 f12)
+#49 := (f6 #48 f11)
+decl f10 :: S2
+#41 := f10
+#50 := (f3 f10 #49)
+decl f1 :: S1
+#4 := f1
+#130 := (= f1 #50)
+#326 := (not #130)
+#43 := (f7 f8 f11)
+#45 := (f6 #43 f12)
+#46 := (f3 f10 #45)
+#126 := (= f1 #46)
+#139 := (not #126)
+#245 := [hypothesis]: #139
+#325 := (or #130 #126)
+#140 := (iff #130 #139)
+#51 := (= #50 f1)
+#47 := (= #46 f1)
+#52 := (iff #47 #51)
+#53 := (not #52)
+#143 := (iff #53 #140)
+#133 := (iff #126 #130)
+#136 := (not #133)
+#141 := (iff #136 #140)
+#142 := [rewrite]: #141
+#137 := (iff #53 #136)
+#134 := (iff #52 #133)
+#131 := (iff #51 #130)
+#132 := [rewrite]: #131
+#128 := (iff #47 #126)
+#129 := [rewrite]: #128
+#135 := [monotonicity #129 #132]: #134
+#138 := [monotonicity #135]: #137
+#144 := [trans #138 #142]: #143
+#125 := [asserted]: #53
+#147 := [mp #125 #144]: #140
+#237 := (not #140)
+#324 := (or #130 #126 #237)
+#238 := [def-axiom]: #324
+#239 := [unit-resolution #238 #147]: #325
+#624 := [unit-resolution #239 #245]: #130
+#330 := (f3 f10 f11)
+#327 := (= f1 #330)
+#331 := (f3 f10 f12)
+#310 := (= f1 #331)
+#647 := (or #310 #327)
+#644 := (not #647)
+#347 := (or #126 #644)
+#634 := (iff #126 #647)
+#22 := (:var 0 S3)
+#20 := (:var 1 S3)
+#21 := (f7 f8 #20)
+#23 := (f6 #21 #22)
+#18 := (:var 2 S2)
+#24 := (f3 #18 #23)
+#669 := (pattern #24)
+#28 := (f3 #18 #22)
+#99 := (= f1 #28)
+#26 := (f3 #18 #20)
+#96 := (= f1 #26)
+#102 := (or #96 #99)
+#92 := (= f1 #24)
+#105 := (iff #92 #102)
+#670 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #669) #105)
+#108 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #105)
+#673 := (iff #108 #670)
+#671 := (iff #105 #105)
+#672 := [refl]: #671
+#674 := [quant-intro #672]: #673
+#151 := (~ #108 #108)
+#165 := (~ #105 #105)
+#166 := [refl]: #165
+#152 := [nnf-pos #166]: #151
+#29 := (= #28 f1)
+#27 := (= #26 f1)
+#30 := (or #27 #29)
+#25 := (= #24 f1)
+#31 := (iff #25 #30)
+#32 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #31)
+#109 := (iff #32 #108)
+#106 := (iff #31 #105)
+#103 := (iff #30 #102)
+#100 := (iff #29 #99)
+#101 := [rewrite]: #100
+#97 := (iff #27 #96)
+#98 := [rewrite]: #97
+#104 := [monotonicity #98 #101]: #103
+#94 := (iff #25 #92)
+#95 := [rewrite]: #94
+#107 := [monotonicity #95 #104]: #106
+#110 := [quant-intro #107]: #109
+#91 := [asserted]: #32
+#113 := [mp #91 #110]: #108
+#167 := [mp~ #113 #152]: #108
+#675 := [mp #167 #674]: #670
+#643 := (not #670)
+#631 := (or #643 #634)
+#304 := (or #327 #310)
+#436 := (iff #126 #304)
+#637 := (or #643 #436)
+#638 := (iff #637 #631)
+#278 := (iff #631 #631)
+#279 := [rewrite]: #278
+#635 := (iff #436 #634)
+#632 := (iff #304 #647)
+#633 := [rewrite]: #632
+#636 := [monotonicity #633]: #635
+#640 := [monotonicity #636]: #638
+#641 := [trans #640 #279]: #638
+#273 := [quant-inst #41 #42 #44]: #637
+#639 := [mp #273 #641]: #631
+#625 := [unit-resolution #639 #675]: #634
+#642 := (not #634)
+#628 := (or #642 #126 #644)
+#629 := [def-axiom]: #628
+#348 := [unit-resolution #629 #625]: #347
+#622 := [unit-resolution #348 #245]: #644
+#623 := (or #326 #647)
+#649 := (iff #130 #647)
+#315 := (or #643 #649)
+#316 := [quant-inst #41 #44 #42]: #315
+#626 := [unit-resolution #316 #675]: #649
+#645 := (not #649)
+#287 := (or #645 #326 #647)
+#630 := [def-axiom]: #287
+#627 := [unit-resolution #630 #626]: #623
+#336 := [unit-resolution #627 #622 #624]: false
+#337 := [lemma #336]: #126
+#329 := (or #326 #139)
+#317 := (or #326 #139 #237)
+#328 := [def-axiom]: #317
+#257 := [unit-resolution #328 #147]: #329
+#338 := [unit-resolution #257 #337]: #326
+#340 := (or #139 #647)
+#335 := (or #642 #139 #647)
+#351 := [def-axiom]: #335
+#618 := [unit-resolution #351 #625]: #340
+#619 := [unit-resolution #618 #337]: #647
+#332 := (or #130 #644)
+#303 := (or #645 #130 #644)
+#646 := [def-axiom]: #303
+#616 := [unit-resolution #646 #626]: #332
+[unit-resolution #616 #619 #338]: false
+unsat
+0a38803d5203ebb9de80029b1e5de8bcd8e8f404 128 0
+#2 := false
+decl f3 :: (-> S2 S3 S1)
+decl f6 :: (-> S4 S3 S3)
+decl f11 :: S3
+#42 := f11
+decl f7 :: (-> S5 S3 S4)
+decl f8 :: S5
+#19 := f8
+#43 := (f7 f8 f11)
+#44 := (f6 #43 f11)
+decl f10 :: S2
+#41 := f10
+#45 := (f3 f10 #44)
+decl f1 :: S1
+#4 := f1
+#123 := (= f1 #45)
+#136 := (not #123)
+#627 := [hypothesis]: #136
+#47 := (f3 f10 f11)
+#127 := (= f1 #47)
+#322 := (or #127 #123)
+#137 := (iff #127 #136)
+#48 := (= #47 f1)
+#46 := (= #45 f1)
+#49 := (iff #46 #48)
+#50 := (not #49)
+#140 := (iff #50 #137)
+#130 := (iff #123 #127)
+#133 := (not #130)
+#138 := (iff #133 #137)
+#139 := [rewrite]: #138
+#134 := (iff #50 #133)
+#131 := (iff #49 #130)
+#128 := (iff #48 #127)
+#129 := [rewrite]: #128
+#125 := (iff #46 #123)
+#126 := [rewrite]: #125
+#132 := [monotonicity #126 #129]: #131
+#135 := [monotonicity #132]: #134
+#141 := [trans #135 #139]: #140
+#122 := [asserted]: #50
+#144 := [mp #122 #141]: #137
+#234 := (not #137)
+#321 := (or #127 #123 #234)
+#235 := [def-axiom]: #321
+#236 := [unit-resolution #235 #144]: #322
+#288 := [unit-resolution #236 #627]: #127
+#323 := (not #127)
+#290 := (or #123 #323)
+#22 := (:var 0 S3)
+#20 := (:var 1 S3)
+#21 := (f7 f8 #20)
+#23 := (f6 #21 #22)
+#18 := (:var 2 S2)
+#24 := (f3 #18 #23)
+#666 := (pattern #24)
+#28 := (f3 #18 #22)
+#96 := (= f1 #28)
+#26 := (f3 #18 #20)
+#93 := (= f1 #26)
+#99 := (or #93 #96)
+#89 := (= f1 #24)
+#102 := (iff #89 #99)
+#667 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #666) #102)
+#105 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #102)
+#670 := (iff #105 #667)
+#668 := (iff #102 #102)
+#669 := [refl]: #668
+#671 := [quant-intro #669]: #670
+#148 := (~ #105 #105)
+#162 := (~ #102 #102)
+#163 := [refl]: #162
+#149 := [nnf-pos #163]: #148
+#29 := (= #28 f1)
+#27 := (= #26 f1)
+#30 := (or #27 #29)
+#25 := (= #24 f1)
+#31 := (iff #25 #30)
+#32 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #31)
+#106 := (iff #32 #105)
+#103 := (iff #31 #102)
+#100 := (iff #30 #99)
+#97 := (iff #29 #96)
+#98 := [rewrite]: #97
+#94 := (iff #27 #93)
+#95 := [rewrite]: #94
+#101 := [monotonicity #95 #98]: #100
+#91 := (iff #25 #89)
+#92 := [rewrite]: #91
+#104 := [monotonicity #92 #101]: #103
+#107 := [quant-intro #104]: #106
+#88 := [asserted]: #32
+#110 := [mp #88 #107]: #105
+#164 := [mp~ #110 #149]: #105
+#672 := [mp #164 #671]: #667
+#301 := (not #667)
+#433 := (or #301 #130)
+#327 := (or #127 #127)
+#324 := (iff #123 #327)
+#640 := (or #301 #324)
+#313 := (iff #640 #433)
+#648 := (iff #433 #433)
+#649 := [rewrite]: #648
+#644 := (iff #324 #130)
+#328 := (iff #327 #127)
+#307 := [rewrite]: #328
+#646 := [monotonicity #307]: #644
+#647 := [monotonicity #646]: #313
+#650 := [trans #647 #649]: #313
+#312 := [quant-inst #41 #42 #42]: #640
+#645 := [mp #312 #650]: #433
+#289 := [unit-resolution #645 #672]: #130
+#651 := (or #133 #123 #323)
+#641 := [def-axiom]: #651
+#291 := [unit-resolution #641 #289]: #290
+#629 := [unit-resolution #291 #288 #627]: false
+#630 := [lemma #629]: #123
+#326 := (or #323 #136)
+#314 := (or #323 #136 #234)
+#325 := [def-axiom]: #314
+#254 := [unit-resolution #325 #144]: #326
+#631 := [unit-resolution #254 #630]: #323
+#632 := (or #136 #127)
+#299 := (or #133 #136 #127)
+#304 := [def-axiom]: #299
+#633 := [unit-resolution #304 #289]: #632
+[unit-resolution #633 #631 #630]: false
+unsat
+a9b4d2c6d5d71402741164958baf8befeec2192a 266 0
+#2 := false
+decl f3 :: (-> S2 S3 S1)
+decl f12 :: S3
+#44 := f12
+decl f10 :: S2
+#41 := f10
+#623 := (f3 f10 f12)
+decl f1 :: S1
+#4 := f1
+#336 := (= f1 #623)
+decl f13 :: S3
+#46 := f13
+#334 := (f3 f10 f13)
+#331 := (= f1 #334)
+#621 := (or #331 #336)
+decl f6 :: (-> S4 S3 S3)
+decl f7 :: (-> S5 S3 S4)
+decl f8 :: S5
+#19 := f8
+#45 := (f7 f8 f12)
+#47 := (f6 #45 f13)
+#308 := (f3 f10 #47)
+#440 := (= f1 #308)
+#615 := (iff #440 #621)
+#581 := (not #615)
+#593 := (not #621)
+#605 := (not #336)
+decl f11 :: S3
+#42 := f11
+#636 := (f3 f10 f11)
+#637 := (= f1 #636)
+#483 := (or #336 #637)
+#608 := (not #483)
+#43 := (f7 f8 f11)
+#51 := (f6 #43 f12)
+#335 := (f3 f10 #51)
+#314 := (= f1 #335)
+#591 := (iff #314 #483)
+#583 := (not #591)
+#576 := [hypothesis]: #583
+#22 := (:var 0 S3)
+#20 := (:var 1 S3)
+#21 := (f7 f8 #20)
+#23 := (f6 #21 #22)
+#18 := (:var 2 S2)
+#24 := (f3 #18 #23)
+#673 := (pattern #24)
+#28 := (f3 #18 #22)
+#103 := (= f1 #28)
+#26 := (f3 #18 #20)
+#100 := (= f1 #26)
+#106 := (or #100 #103)
+#96 := (= f1 #24)
+#109 := (iff #96 #106)
+#674 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #673) #109)
+#112 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #109)
+#677 := (iff #112 #674)
+#675 := (iff #109 #109)
+#676 := [refl]: #675
+#678 := [quant-intro #676]: #677
+#155 := (~ #112 #112)
+#169 := (~ #109 #109)
+#170 := [refl]: #169
+#156 := [nnf-pos #170]: #155
+#29 := (= #28 f1)
+#27 := (= #26 f1)
+#30 := (or #27 #29)
+#25 := (= #24 f1)
+#31 := (iff #25 #30)
+#32 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #31)
+#113 := (iff #32 #112)
+#110 := (iff #31 #109)
+#107 := (iff #30 #106)
+#104 := (iff #29 #103)
+#105 := [rewrite]: #104
+#101 := (iff #27 #100)
+#102 := [rewrite]: #101
+#108 := [monotonicity #102 #105]: #107
+#98 := (iff #25 #96)
+#99 := [rewrite]: #98
+#111 := [monotonicity #99 #108]: #110
+#114 := [quant-intro #111]: #113
+#95 := [asserted]: #32
+#117 := [mp #95 #114]: #112
+#171 := [mp~ #117 #156]: #112
+#679 := [mp #171 #678]: #674
+#647 := (not #674)
+#589 := (or #647 #591)
+#600 := (or #637 #336)
+#482 := (iff #314 #600)
+#592 := (or #647 #482)
+#492 := (iff #592 #589)
+#495 := (iff #589 #589)
+#488 := [rewrite]: #495
+#493 := (iff #482 #591)
+#484 := (iff #600 #483)
+#443 := [rewrite]: #484
+#588 := [monotonicity #443]: #493
+#494 := [monotonicity #588]: #492
+#496 := [trans #494 #488]: #492
+#477 := [quant-inst #41 #42 #44]: #592
+#497 := [mp #477 #496]: #589
+#577 := [unit-resolution #497 #679 #576]: false
+#578 := [lemma #577]: #591
+#654 := (not #314)
+#651 := (or #314 #331)
+#648 := (not #651)
+#52 := (f7 f8 #51)
+#53 := (f6 #52 f13)
+#54 := (f3 f10 #53)
+#134 := (= f1 #54)
+#330 := (not #134)
+#48 := (f6 #43 #47)
+#49 := (f3 f10 #48)
+#130 := (= f1 #49)
+#143 := (not #130)
+#579 := [hypothesis]: #143
+#329 := (or #134 #130)
+#144 := (iff #134 #143)
+#55 := (= #54 f1)
+#50 := (= #49 f1)
+#56 := (iff #50 #55)
+#57 := (not #56)
+#147 := (iff #57 #144)
+#137 := (iff #130 #134)
+#140 := (not #137)
+#145 := (iff #140 #144)
+#146 := [rewrite]: #145
+#141 := (iff #57 #140)
+#138 := (iff #56 #137)
+#135 := (iff #55 #134)
+#136 := [rewrite]: #135
+#132 := (iff #50 #130)
+#133 := [rewrite]: #132
+#139 := [monotonicity #133 #136]: #138
+#142 := [monotonicity #139]: #141
+#148 := [trans #142 #146]: #147
+#129 := [asserted]: #57
+#151 := [mp #129 #148]: #144
+#241 := (not #144)
+#328 := (or #134 #130 #241)
+#242 := [def-axiom]: #328
+#243 := [unit-resolution #242 #151]: #329
+#573 := [unit-resolution #243 #579]: #134
+#564 := (or #330 #651)
+#653 := (iff #134 #651)
+#319 := (or #647 #653)
+#320 := [quant-inst #41 #51 #46]: #319
+#580 := [unit-resolution #320 #679]: #653
+#649 := (not #653)
+#291 := (or #649 #330 #651)
+#634 := [def-axiom]: #291
+#565 := [unit-resolution #634 #580]: #564
+#567 := [unit-resolution #565 #573]: #651
+#657 := (not #331)
+#597 := (or #647 #615)
+#620 := (or #336 #331)
+#624 := (iff #440 #620)
+#617 := (or #647 #624)
+#612 := (iff #617 #597)
+#619 := (iff #597 #597)
+#460 := [rewrite]: #619
+#616 := (iff #624 #615)
+#625 := (iff #620 #621)
+#614 := [rewrite]: #625
+#611 := [monotonicity #614]: #616
+#613 := [monotonicity #611]: #612
+#461 := [trans #613 #460]: #612
+#618 := [quant-inst #41 #44 #46]: #617
+#462 := [mp #618 #461]: #597
+#568 := [unit-resolution #462 #679]: #615
+#558 := (or #581 #593)
+#356 := (not #440)
+#640 := (or #440 #637)
+#629 := (not #640)
+#570 := (or #130 #629)
+#277 := (iff #130 #640)
+#282 := (or #647 #277)
+#638 := (or #637 #440)
+#639 := (iff #130 #638)
+#283 := (or #647 #639)
+#643 := (iff #283 #282)
+#632 := (iff #282 #282)
+#633 := [rewrite]: #632
+#642 := (iff #639 #277)
+#635 := (iff #638 #640)
+#641 := [rewrite]: #635
+#644 := [monotonicity #641]: #642
+#646 := [monotonicity #644]: #643
+#339 := [trans #646 #633]: #643
+#645 := [quant-inst #41 #42 #47]: #283
+#355 := [mp #645 #339]: #282
+#569 := [unit-resolution #355 #679]: #277
+#626 := (not #277)
+#630 := (or #626 #130 #629)
+#627 := [def-axiom]: #630
+#566 := [unit-resolution #627 #569]: #570
+#571 := [unit-resolution #566 #579]: #629
+#357 := (or #640 #356)
+#343 := [def-axiom]: #357
+#557 := [unit-resolution #343 #571]: #356
+#575 := (or #581 #440 #593)
+#572 := [def-axiom]: #575
+#560 := [unit-resolution #572 #557]: #558
+#561 := [unit-resolution #560 #568]: #593
+#604 := (or #621 #657)
+#498 := [def-axiom]: #604
+#562 := [unit-resolution #498 #561]: #657
+#306 := (or #648 #314 #331)
+#311 := [def-axiom]: #306
+#559 := [unit-resolution #311 #562 #567]: #314
+#358 := (not #637)
+#249 := (or #640 #358)
+#628 := [def-axiom]: #249
+#563 := [unit-resolution #628 #571]: #358
+#499 := (or #621 #605)
+#500 := [def-axiom]: #499
+#543 := [unit-resolution #500 #561]: #605
+#609 := (or #608 #336 #637)
+#603 := [def-axiom]: #609
+#544 := [unit-resolution #603 #543 #563]: #608
+#441 := (or #583 #654 #483)
+#442 := [def-axiom]: #441
+#546 := [unit-resolution #442 #544 #559 #578]: false
+#547 := [lemma #546]: #130
+#333 := (or #330 #143)
+#321 := (or #330 #143 #241)
+#332 := [def-axiom]: #321
+#261 := [unit-resolution #332 #151]: #333
+#548 := [unit-resolution #261 #547]: #330
+#549 := (or #134 #648)
+#307 := (or #649 #134 #648)
+#650 := [def-axiom]: #307
+#550 := [unit-resolution #650 #580]: #549
+#551 := [unit-resolution #550 #548]: #648
+#655 := (or #651 #654)
+#656 := [def-axiom]: #655
+#552 := [unit-resolution #656 #551]: #654
+#610 := (or #583 #314 #608)
+#439 := [def-axiom]: #610
+#553 := [unit-resolution #439 #552 #578]: #608
+#606 := (or #483 #605)
+#607 := [def-axiom]: #606
+#554 := [unit-resolution #607 #553]: #605
+#652 := (or #651 #657)
+#658 := [def-axiom]: #652
+#555 := [unit-resolution #658 #551]: #657
+#590 := (or #593 #331 #336)
+#594 := [def-axiom]: #590
+#545 := [unit-resolution #594 #555 #554]: #593
+#556 := (or #143 #640)
+#631 := (or #626 #143 #640)
+#340 := [def-axiom]: #631
+#534 := [unit-resolution #340 #569]: #556
+#535 := [unit-resolution #534 #547]: #640
+#601 := (or #483 #358)
+#602 := [def-axiom]: #601
+#537 := [unit-resolution #602 #553]: #358
+#351 := (or #629 #440 #637)
+#352 := [def-axiom]: #351
+#538 := [unit-resolution #352 #537 #535]: #440
+#574 := (or #581 #356 #621)
+#584 := [def-axiom]: #574
+#539 := [unit-resolution #584 #538 #545]: #581
+[unit-resolution #462 #679 #539]: false
+unsat
+c3c3648cfba9d6c85cac6f8d51a3b06b08975178 160 0
+#2 := false
+decl f3 :: (-> S2 S3 S1)
+decl f12 :: S3
+#44 := f12
+decl f10 :: S2
+#41 := f10
+#50 := (f3 f10 f12)
+decl f1 :: S1
+#4 := f1
+#134 := (= f1 #50)
+#188 := (not #134)
+decl f11 :: S3
+#42 := f11
+#48 := (f3 f10 f11)
+#131 := (= f1 #48)
+#187 := (not #131)
+#189 := (or #187 #188)
+#190 := (not #189)
+#331 := [hypothesis]: #190
+decl f6 :: (-> S4 S3 S3)
+decl f7 :: (-> S5 S3 S4)
+decl f9 :: S5
+#33 := f9
+#43 := (f7 f9 f11)
+#45 := (f6 #43 f12)
+#46 := (f3 f10 #45)
+#127 := (= f1 #46)
+#146 := (not #127)
+#337 := (or #146 #189)
+#201 := (iff #127 #189)
+#137 := (and #131 #134)
+#147 := (iff #137 #146)
+#204 := (iff #147 #201)
+#196 := (iff #189 #127)
+#202 := (iff #196 #201)
+#203 := [rewrite]: #202
+#199 := (iff #147 #196)
+#193 := (iff #190 #146)
+#197 := (iff #193 #196)
+#198 := [rewrite]: #197
+#194 := (iff #147 #193)
+#191 := (iff #137 #190)
+#192 := [rewrite]: #191
+#195 := [monotonicity #192]: #194
+#200 := [trans #195 #198]: #199
+#205 := [trans #200 #203]: #204
+#51 := (= #50 f1)
+#49 := (= #48 f1)
+#52 := (and #49 #51)
+#47 := (= #46 f1)
+#53 := (iff #47 #52)
+#54 := (not #53)
+#150 := (iff #54 #147)
+#140 := (iff #127 #137)
+#143 := (not #140)
+#148 := (iff #143 #147)
+#149 := [rewrite]: #148
+#144 := (iff #54 #143)
+#141 := (iff #53 #140)
+#138 := (iff #52 #137)
+#135 := (iff #51 #134)
+#136 := [rewrite]: #135
+#132 := (iff #49 #131)
+#133 := [rewrite]: #132
+#139 := [monotonicity #133 #136]: #138
+#129 := (iff #47 #127)
+#130 := [rewrite]: #129
+#142 := [monotonicity #130 #139]: #141
+#145 := [monotonicity #142]: #144
+#151 := [trans #145 #149]: #150
+#126 := [asserted]: #54
+#154 := [mp #126 #151]: #147
+#206 := [mp #154 #205]: #201
+#344 := (not #201)
+#354 := (or #146 #189 #344)
+#358 := [def-axiom]: #354
+#674 := [unit-resolution #358 #206]: #337
+#463 := [unit-resolution #674 #331]: #146
+#330 := (or #127 #189)
+#676 := (iff #127 #190)
+#22 := (:var 0 S3)
+#20 := (:var 1 S3)
+#34 := (f7 f9 #20)
+#35 := (f6 #34 #22)
+#18 := (:var 2 S2)
+#36 := (f3 #18 #35)
+#703 := (pattern #36)
+#28 := (f3 #18 #22)
+#100 := (= f1 #28)
+#179 := (not #100)
+#26 := (f3 #18 #20)
+#97 := (= f1 #26)
+#178 := (not #97)
+#162 := (or #178 #179)
+#163 := (not #162)
+#113 := (= f1 #36)
+#180 := (iff #113 #163)
+#704 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #703) #180)
+#183 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #180)
+#707 := (iff #183 #704)
+#705 := (iff #180 #180)
+#706 := [refl]: #705
+#708 := [quant-intro #706]: #707
+#117 := (and #97 #100)
+#120 := (iff #113 #117)
+#123 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #120)
+#184 := (iff #123 #183)
+#181 := (iff #120 #180)
+#164 := (iff #117 #163)
+#165 := [rewrite]: #164
+#182 := [monotonicity #165]: #181
+#185 := [quant-intro #182]: #184
+#160 := (~ #123 #123)
+#175 := (~ #120 #120)
+#176 := [refl]: #175
+#161 := [nnf-pos #176]: #160
+#29 := (= #28 f1)
+#27 := (= #26 f1)
+#38 := (and #27 #29)
+#37 := (= #36 f1)
+#39 := (iff #37 #38)
+#40 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #39)
+#124 := (iff #40 #123)
+#121 := (iff #39 #120)
+#118 := (iff #38 #117)
+#101 := (iff #29 #100)
+#102 := [rewrite]: #101
+#98 := (iff #27 #97)
+#99 := [rewrite]: #98
+#119 := [monotonicity #99 #102]: #118
+#115 := (iff #37 #113)
+#116 := [rewrite]: #115
+#122 := [monotonicity #116 #119]: #121
+#125 := [quant-intro #122]: #124
+#112 := [asserted]: #40
+#128 := [mp #112 #125]: #123
+#177 := [mp~ #128 #161]: #123
+#186 := [mp #177 #185]: #183
+#709 := [mp #186 #708]: #704
+#670 := (not #704)
+#342 := (or #670 #676)
+#343 := [quant-inst #41 #42 #44]: #342
+#672 := [unit-resolution #343 #709]: #676
+#677 := (not #676)
+#678 := (or #677 #127 #189)
+#679 := [def-axiom]: #678
+#673 := [unit-resolution #679 #672]: #330
+#314 := [unit-resolution #673 #463 #331]: false
+#657 := [lemma #314]: #189
+#284 := (or #127 #190)
+#355 := (or #127 #190 #344)
+#356 := [def-axiom]: #355
+#357 := [unit-resolution #356 #206]: #284
+#318 := [unit-resolution #357 #657]: #127
+#319 := (or #146 #190)
+#680 := (or #677 #146 #190)
+#675 := [def-axiom]: #680
+#320 := [unit-resolution #675 #672]: #319
+[unit-resolution #320 #318 #657]: false
+unsat
+1adc4d295cebee376081ce9f5a9d0e96c2943423 149 0
+#2 := false
+decl f3 :: (-> S2 S3 S1)
+decl f4 :: S3
+#9 := f4
+decl f10 :: S2
+#41 := f10
+#227 := (f3 f10 f4)
+decl f1 :: S1
+#4 := f1
+#314 := (= f1 #227)
+#228 := (not #314)
+decl f11 :: S3
+#42 := f11
+#315 := (f3 f10 f11)
+#229 := (= f1 #315)
+#316 := (not #229)
+#307 := (or #316 #228)
+#318 := (not #307)
+decl f6 :: (-> S4 S3 S3)
+decl f7 :: (-> S5 S3 S4)
+decl f9 :: S5
+#33 := f9
+#43 := (f7 f9 f11)
+#44 := (f6 #43 f4)
+#45 := (f3 f10 #44)
+#121 := (= f1 #45)
+#319 := (iff #121 #318)
+#22 := (:var 0 S3)
+#20 := (:var 1 S3)
+#34 := (f7 f9 #20)
+#35 := (f6 #34 #22)
+#18 := (:var 2 S2)
+#36 := (f3 #18 #35)
+#666 := (pattern #36)
+#28 := (f3 #18 #22)
+#94 := (= f1 #28)
+#162 := (not #94)
+#26 := (f3 #18 #20)
+#91 := (= f1 #26)
+#161 := (not #91)
+#145 := (or #161 #162)
+#146 := (not #145)
+#107 := (= f1 #36)
+#163 := (iff #107 #146)
+#667 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #666) #163)
+#166 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #163)
+#670 := (iff #166 #667)
+#668 := (iff #163 #163)
+#669 := [refl]: #668
+#671 := [quant-intro #669]: #670
+#111 := (and #91 #94)
+#114 := (iff #107 #111)
+#117 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #114)
+#167 := (iff #117 #166)
+#164 := (iff #114 #163)
+#147 := (iff #111 #146)
+#148 := [rewrite]: #147
+#165 := [monotonicity #148]: #164
+#168 := [quant-intro #165]: #167
+#143 := (~ #117 #117)
+#158 := (~ #114 #114)
+#159 := [refl]: #158
+#144 := [nnf-pos #159]: #143
+#29 := (= #28 f1)
+#27 := (= #26 f1)
+#38 := (and #27 #29)
+#37 := (= #36 f1)
+#39 := (iff #37 #38)
+#40 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #39)
+#118 := (iff #40 #117)
+#115 := (iff #39 #114)
+#112 := (iff #38 #111)
+#95 := (iff #29 #94)
+#96 := [rewrite]: #95
+#92 := (iff #27 #91)
+#93 := [rewrite]: #92
+#113 := [monotonicity #93 #96]: #112
+#109 := (iff #37 #107)
+#110 := [rewrite]: #109
+#116 := [monotonicity #110 #113]: #115
+#119 := [quant-intro #116]: #118
+#106 := [asserted]: #40
+#122 := [mp #106 #119]: #117
+#160 := [mp~ #122 #144]: #117
+#169 := [mp #160 #168]: #166
+#672 := [mp #169 #671]: #667
+#317 := (not #667)
+#321 := (or #317 #319)
+#300 := [quant-inst #41 #42 #9]: #321
+#247 := [unit-resolution #300 #672]: #319
+#306 := (not #319)
+#320 := (or #306 #318)
+#46 := (= #45 f1)
+#47 := (not #46)
+#48 := (not #47)
+#133 := (iff #48 #121)
+#125 := (not #121)
+#128 := (not #125)
+#131 := (iff #128 #121)
+#132 := [rewrite]: #131
+#129 := (iff #48 #128)
+#126 := (iff #47 #125)
+#123 := (iff #46 #121)
+#124 := [rewrite]: #123
+#127 := [monotonicity #124]: #126
+#130 := [monotonicity #127]: #129
+#134 := [trans #130 #132]: #133
+#120 := [asserted]: #48
+#137 := [mp #120 #134]: #121
+#642 := (or #306 #125 #318)
+#643 := [def-axiom]: #642
+#636 := [unit-resolution #643 #137]: #320
+#277 := [unit-resolution #636 #247]: #318
+#294 := (or #307 #314)
+#426 := [def-axiom]: #294
+#620 := [unit-resolution #426 #277]: #314
+#8 := (:var 0 S2)
+#10 := (f3 #8 f4)
+#645 := (pattern #10)
+#69 := (= f1 #10)
+#72 := (not #69)
+#646 := (forall (vars (?v0 S2)) (:pat #645) #72)
+#75 := (forall (vars (?v0 S2)) #72)
+#649 := (iff #75 #646)
+#647 := (iff #72 #72)
+#648 := [refl]: #647
+#650 := [quant-intro #648]: #649
+#151 := (~ #75 #75)
+#149 := (~ #72 #72)
+#150 := [refl]: #149
+#152 := [nnf-pos #150]: #151
+#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
+#136 := [mp~ #80 #152]: #75
+#651 := [mp #136 #650]: #646
+#297 := (not #646)
+#635 := (or #297 #228)
+#293 := [quant-inst #41]: #635
+[unit-resolution #293 #651 #620]: false
+unsat
+27fbc35929f013c0b43884a593f3f377821cad64 173 0
+#2 := false
+decl f3 :: (-> S2 S3 S1)
+decl f11 :: S3
+#42 := f11
+decl f10 :: S2
+#41 := f10
+#47 := (f3 f10 f11)
+decl f1 :: S1
+#4 := f1
+#127 := (= f1 #47)
+#323 := (not #127)
+decl f6 :: (-> S4 S3 S3)
+decl f5 :: S3
+#14 := f5
+decl f7 :: (-> S5 S3 S4)
+decl f9 :: S5
+#33 := f9
+#43 := (f7 f9 f11)
+#44 := (f6 #43 f5)
+#45 := (f3 f10 #44)
+#123 := (= f1 #45)
+#327 := (f3 f10 f5)
+#324 := (= f1 #327)
+#328 := (not #324)
+#301 := [hypothesis]: #328
+#8 := (:var 0 S2)
+#15 := (f3 #8 f5)
+#659 := (pattern #15)
+#81 := (= f1 #15)
+#660 := (forall (vars (?v0 S2)) (:pat #659) #81)
+#85 := (forall (vars (?v0 S2)) #81)
+#663 := (iff #85 #660)
+#661 := (iff #81 #81)
+#662 := [refl]: #661
+#664 := [quant-intro #662]: #663
+#146 := (~ #85 #85)
+#145 := (~ #81 #81)
+#160 := [refl]: #145
+#147 := [nnf-pos #160]: #146
+#16 := (= #15 f1)
+#17 := (forall (vars (?v0 S2)) #16)
+#86 := (iff #17 #85)
+#83 := (iff #16 #81)
+#84 := [rewrite]: #83
+#87 := [quant-intro #84]: #86
+#80 := [asserted]: #17
+#90 := [mp #80 #87]: #85
+#161 := [mp~ #90 #147]: #85
+#665 := [mp #161 #664]: #660
+#289 := (not #660)
+#290 := (or #289 #324)
+#291 := [quant-inst #41]: #290
+#433 := [unit-resolution #291 #665 #301]: false
+#629 := [lemma #433]: #324
+#136 := (not #123)
+#630 := [hypothesis]: #136
+#322 := (or #127 #123)
+#137 := (iff #127 #136)
+#48 := (= #47 f1)
+#46 := (= #45 f1)
+#49 := (iff #46 #48)
+#50 := (not #49)
+#140 := (iff #50 #137)
+#130 := (iff #123 #127)
+#133 := (not #130)
+#138 := (iff #133 #137)
+#139 := [rewrite]: #138
+#134 := (iff #50 #133)
+#131 := (iff #49 #130)
+#128 := (iff #48 #127)
+#129 := [rewrite]: #128
+#125 := (iff #46 #123)
+#126 := [rewrite]: #125
+#132 := [monotonicity #126 #129]: #131
+#135 := [monotonicity #132]: #134
+#141 := [trans #135 #139]: #140
+#122 := [asserted]: #50
+#144 := [mp #122 #141]: #137
+#234 := (not #137)
+#321 := (or #127 #123 #234)
+#235 := [def-axiom]: #321
+#236 := [unit-resolution #235 #144]: #322
+#631 := [unit-resolution #236 #630]: #127
+#307 := (or #323 #328)
+#633 := (or #123 #307)
+#644 := (not #307)
+#646 := (iff #123 #644)
+#22 := (:var 0 S3)
+#20 := (:var 1 S3)
+#34 := (f7 f9 #20)
+#35 := (f6 #34 #22)
+#18 := (:var 2 S2)
+#36 := (f3 #18 #35)
+#673 := (pattern #36)
+#28 := (f3 #18 #22)
+#96 := (= f1 #28)
+#169 := (not #96)
+#26 := (f3 #18 #20)
+#93 := (= f1 #26)
+#168 := (not #93)
+#152 := (or #168 #169)
+#153 := (not #152)
+#109 := (= f1 #36)
+#170 := (iff #109 #153)
+#674 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #673) #170)
+#173 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #170)
+#677 := (iff #173 #674)
+#675 := (iff #170 #170)
+#676 := [refl]: #675
+#678 := [quant-intro #676]: #677
+#113 := (and #93 #96)
+#116 := (iff #109 #113)
+#119 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #116)
+#174 := (iff #119 #173)
+#171 := (iff #116 #170)
+#154 := (iff #113 #153)
+#155 := [rewrite]: #154
+#172 := [monotonicity #155]: #171
+#175 := [quant-intro #172]: #174
+#150 := (~ #119 #119)
+#165 := (~ #116 #116)
+#166 := [refl]: #165
+#151 := [nnf-pos #166]: #150
+#29 := (= #28 f1)
+#27 := (= #26 f1)
+#38 := (and #27 #29)
+#37 := (= #36 f1)
+#39 := (iff #37 #38)
+#40 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #39)
+#120 := (iff #40 #119)
+#117 := (iff #39 #116)
+#114 := (iff #38 #113)
+#97 := (iff #29 #96)
+#98 := [rewrite]: #97
+#94 := (iff #27 #93)
+#95 := [rewrite]: #94
+#115 := [monotonicity #95 #98]: #114
+#111 := (iff #37 #109)
+#112 := [rewrite]: #111
+#118 := [monotonicity #112 #115]: #117
+#121 := [quant-intro #118]: #120
+#108 := [asserted]: #40
+#124 := [mp #108 #121]: #119
+#167 := [mp~ #124 #151]: #119
+#176 := [mp #167 #175]: #173
+#679 := [mp #176 #678]: #674
+#640 := (not #674)
+#312 := (or #640 #646)
+#313 := [quant-inst #41 #42 #14]: #312
+#632 := [unit-resolution #313 #679]: #646
+#641 := (not #646)
+#299 := (or #641 #123 #307)
+#304 := [def-axiom]: #299
+#628 := [unit-resolution #304 #632]: #633
+#634 := [unit-resolution #628 #630]: #307
+#645 := (or #644 #323 #328)
+#651 := [def-axiom]: #645
+#270 := [unit-resolution #651 #634 #631 #629]: false
+#635 := [lemma #270]: #123
+#326 := (or #323 #136)
+#314 := (or #323 #136 #234)
+#325 := [def-axiom]: #314
+#254 := [unit-resolution #325 #144]: #326
+#637 := [unit-resolution #254 #635]: #323
+#275 := (or #136 #644)
+#642 := (or #641 #136 #644)
+#300 := [def-axiom]: #642
+#276 := [unit-resolution #300 #632]: #275
+#638 := [unit-resolution #276 #635]: #644
+#647 := (or #307 #127)
+#648 := [def-axiom]: #647
+[unit-resolution #648 #638 #637]: false
+unsat
+fa1e213c15b8e9288bf16d2dc4bd96e3c7fb5c7e 173 0
+#2 := false
+decl f3 :: (-> S2 S3 S1)
+decl f6 :: (-> S4 S3 S3)
+decl f11 :: S3
+#42 := f11
+decl f7 :: (-> S5 S3 S4)
+decl f12 :: S3
+#44 := f12
+decl f9 :: S5
+#33 := f9
+#48 := (f7 f9 f12)
+#49 := (f6 #48 f11)
+decl f10 :: S2
+#41 := f10
+#50 := (f3 f10 #49)
+decl f1 :: S1
+#4 := f1
+#130 := (= f1 #50)
+#326 := (not #130)
+#43 := (f7 f9 f11)
+#45 := (f6 #43 f12)
+#46 := (f3 f10 #45)
+#126 := (= f1 #46)
+#139 := (not #126)
+#628 := [hypothesis]: #139
+#325 := (or #130 #126)
+#140 := (iff #130 #139)
+#51 := (= #50 f1)
+#47 := (= #46 f1)
+#52 := (iff #47 #51)
+#53 := (not #52)
+#143 := (iff #53 #140)
+#133 := (iff #126 #130)
+#136 := (not #133)
+#141 := (iff #136 #140)
+#142 := [rewrite]: #141
+#137 := (iff #53 #136)
+#134 := (iff #52 #133)
+#131 := (iff #51 #130)
+#132 := [rewrite]: #131
+#128 := (iff #47 #126)
+#129 := [rewrite]: #128
+#135 := [monotonicity #129 #132]: #134
+#138 := [monotonicity #135]: #137
+#144 := [trans #138 #142]: #143
+#125 := [asserted]: #53
+#147 := [mp #125 #144]: #140
+#237 := (not #140)
+#324 := (or #130 #126 #237)
+#238 := [def-axiom]: #324
+#239 := [unit-resolution #238 #147]: #325
+#629 := [unit-resolution #239 #628]: #130
+#310 := (f3 f10 f12)
+#647 := (= f1 #310)
+#649 := (not #647)
+#330 := (f3 f10 f11)
+#327 := (= f1 #330)
+#331 := (not #327)
+#315 := (or #331 #649)
+#626 := (or #126 #315)
+#651 := (not #315)
+#642 := (iff #126 #651)
+#22 := (:var 0 S3)
+#20 := (:var 1 S3)
+#34 := (f7 f9 #20)
+#35 := (f6 #34 #22)
+#18 := (:var 2 S2)
+#36 := (f3 #18 #35)
+#676 := (pattern #36)
+#28 := (f3 #18 #22)
+#99 := (= f1 #28)
+#172 := (not #99)
+#26 := (f3 #18 #20)
+#96 := (= f1 #26)
+#171 := (not #96)
+#155 := (or #171 #172)
+#156 := (not #155)
+#112 := (= f1 #36)
+#173 := (iff #112 #156)
+#677 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #676) #173)
+#176 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #173)
+#680 := (iff #176 #677)
+#678 := (iff #173 #173)
+#679 := [refl]: #678
+#681 := [quant-intro #679]: #680
+#116 := (and #96 #99)
+#119 := (iff #112 #116)
+#122 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #119)
+#177 := (iff #122 #176)
+#174 := (iff #119 #173)
+#157 := (iff #116 #156)
+#158 := [rewrite]: #157
+#175 := [monotonicity #158]: #174
+#178 := [quant-intro #175]: #177
+#153 := (~ #122 #122)
+#168 := (~ #119 #119)
+#169 := [refl]: #168
+#154 := [nnf-pos #169]: #153
+#29 := (= #28 f1)
+#27 := (= #26 f1)
+#38 := (and #27 #29)
+#37 := (= #36 f1)
+#39 := (iff #37 #38)
+#40 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #39)
+#123 := (iff #40 #122)
+#120 := (iff #39 #119)
+#117 := (iff #38 #116)
+#100 := (iff #29 #99)
+#101 := [rewrite]: #100
+#97 := (iff #27 #96)
+#98 := [rewrite]: #97
+#118 := [monotonicity #98 #101]: #117
+#114 := (iff #37 #112)
+#115 := [rewrite]: #114
+#121 := [monotonicity #115 #118]: #120
+#124 := [quant-intro #121]: #123
+#111 := [asserted]: #40
+#127 := [mp #111 #124]: #122
+#170 := [mp~ #127 #154]: #122
+#179 := [mp #170 #178]: #176
+#682 := [mp #179 #681]: #677
+#302 := (not #677)
+#335 := (or #302 #642)
+#351 := [quant-inst #41 #42 #44]: #335
+#622 := [unit-resolution #351 #682]: #642
+#352 := (not #642)
+#353 := (or #352 #126 #315)
+#339 := [def-axiom]: #353
+#623 := [unit-resolution #339 #622]: #626
+#627 := [unit-resolution #623 #628]: #315
+#337 := (or #326 #651)
+#648 := (iff #130 #651)
+#307 := (or #302 #648)
+#304 := (or #649 #331)
+#436 := (not #304)
+#643 := (iff #130 #436)
+#645 := (or #302 #643)
+#646 := (iff #645 #307)
+#630 := (iff #307 #307)
+#291 := [rewrite]: #630
+#654 := (iff #643 #648)
+#652 := (iff #436 #651)
+#316 := (iff #304 #315)
+#650 := [rewrite]: #316
+#653 := [monotonicity #650]: #652
+#644 := [monotonicity #653]: #654
+#287 := [monotonicity #644]: #646
+#292 := [trans #287 #291]: #646
+#303 := [quant-inst #41 #44 #42]: #645
+#293 := [mp #303 #292]: #307
+#336 := [unit-resolution #293 #682]: #648
+#631 := (not #648)
+#638 := (or #631 #326 #651)
+#640 := [def-axiom]: #638
+#338 := [unit-resolution #640 #336]: #337
+#340 := [unit-resolution #338 #627 #629]: false
+#618 := [lemma #340]: #126
+#329 := (or #326 #139)
+#317 := (or #326 #139 #237)
+#328 := [def-axiom]: #317
+#257 := [unit-resolution #328 #147]: #329
+#619 := [unit-resolution #257 #618]: #326
+#332 := (or #139 #651)
+#354 := (or #352 #139 #651)
+#245 := [def-axiom]: #354
+#616 := [unit-resolution #245 #622]: #332
+#620 := [unit-resolution #616 #618]: #651
+#617 := (or #130 #315)
+#637 := (or #631 #130 #315)
+#273 := [def-axiom]: #637
+#621 := [unit-resolution #273 #336]: #617
+[unit-resolution #621 #620 #619]: false
+unsat
+8424513290e59440c92fec106021e2354c2f6a1c 149 0
+#2 := false
+decl f3 :: (-> S2 S3 S1)
+decl f6 :: (-> S4 S3 S3)
+decl f11 :: S3
+#42 := f11
+decl f7 :: (-> S5 S3 S4)
+decl f9 :: S5
+#33 := f9
+#43 := (f7 f9 f11)
+#44 := (f6 #43 f11)
+decl f10 :: S2
+#41 := f10
+#45 := (f3 f10 #44)
+decl f1 :: S1
+#4 := f1
+#123 := (= f1 #45)
+#136 := (not #123)
+#632 := [hypothesis]: #136
+#47 := (f3 f10 f11)
+#127 := (= f1 #47)
+#322 := (or #127 #123)
+#137 := (iff #127 #136)
+#48 := (= #47 f1)
+#46 := (= #45 f1)
+#49 := (iff #46 #48)
+#50 := (not #49)
+#140 := (iff #50 #137)
+#130 := (iff #123 #127)
+#133 := (not #130)
+#138 := (iff #133 #137)
+#139 := [rewrite]: #138
+#134 := (iff #50 #133)
+#131 := (iff #49 #130)
+#128 := (iff #48 #127)
+#129 := [rewrite]: #128
+#125 := (iff #46 #123)
+#126 := [rewrite]: #125
+#132 := [monotonicity #126 #129]: #131
+#135 := [monotonicity #132]: #134
+#141 := [trans #135 #139]: #140
+#122 := [asserted]: #50
+#144 := [mp #122 #141]: #137
+#234 := (not #137)
+#321 := (or #127 #123 #234)
+#235 := [def-axiom]: #321
+#236 := [unit-resolution #235 #144]: #322
+#633 := [unit-resolution #236 #632]: #127
+#323 := (not #127)
+#634 := (or #123 #323)
+#22 := (:var 0 S3)
+#20 := (:var 1 S3)
+#34 := (f7 f9 #20)
+#35 := (f6 #34 #22)
+#18 := (:var 2 S2)
+#36 := (f3 #18 #35)
+#673 := (pattern #36)
+#28 := (f3 #18 #22)
+#96 := (= f1 #28)
+#169 := (not #96)
+#26 := (f3 #18 #20)
+#93 := (= f1 #26)
+#168 := (not #93)
+#152 := (or #168 #169)
+#153 := (not #152)
+#109 := (= f1 #36)
+#170 := (iff #109 #153)
+#674 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #673) #170)
+#173 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #170)
+#677 := (iff #173 #674)
+#675 := (iff #170 #170)
+#676 := [refl]: #675
+#678 := [quant-intro #676]: #677
+#113 := (and #93 #96)
+#116 := (iff #109 #113)
+#119 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #116)
+#174 := (iff #119 #173)
+#171 := (iff #116 #170)
+#154 := (iff #113 #153)
+#155 := [rewrite]: #154
+#172 := [monotonicity #155]: #171
+#175 := [quant-intro #172]: #174
+#150 := (~ #119 #119)
+#165 := (~ #116 #116)
+#166 := [refl]: #165
+#151 := [nnf-pos #166]: #150
+#29 := (= #28 f1)
+#27 := (= #26 f1)
+#38 := (and #27 #29)
+#37 := (= #36 f1)
+#39 := (iff #37 #38)
+#40 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #39)
+#120 := (iff #40 #119)
+#117 := (iff #39 #116)
+#114 := (iff #38 #113)
+#97 := (iff #29 #96)
+#98 := [rewrite]: #97
+#94 := (iff #27 #93)
+#95 := [rewrite]: #94
+#115 := [monotonicity #95 #98]: #114
+#111 := (iff #37 #109)
+#112 := [rewrite]: #111
+#118 := [monotonicity #112 #115]: #117
+#121 := [quant-intro #118]: #120
+#108 := [asserted]: #40
+#124 := [mp #108 #121]: #119
+#167 := [mp~ #124 #151]: #119
+#176 := [mp #167 #175]: #173
+#679 := [mp #176 #678]: #674
+#650 := (not #674)
+#645 := (or #650 #130)
+#327 := (or #323 #323)
+#324 := (not #327)
+#328 := (iff #123 #324)
+#651 := (or #650 #328)
+#299 := (iff #651 #645)
+#642 := (iff #645 #645)
+#300 := [rewrite]: #642
+#648 := (iff #328 #130)
+#313 := (iff #324 #127)
+#646 := (not #323)
+#640 := (iff #646 #127)
+#312 := [rewrite]: #640
+#301 := (iff #324 #646)
+#307 := (iff #327 #323)
+#644 := [rewrite]: #307
+#433 := [monotonicity #644]: #301
+#647 := [trans #433 #312]: #313
+#649 := [monotonicity #647]: #648
+#304 := [monotonicity #649]: #299
+#643 := [trans #304 #300]: #299
+#641 := [quant-inst #41 #42 #42]: #651
+#284 := [mp #641 #643]: #645
+#628 := [unit-resolution #284 #679]: #130
+#627 := (or #133 #123 #323)
+#288 := [def-axiom]: #627
+#270 := [unit-resolution #288 #628]: #634
+#635 := [unit-resolution #270 #633 #632]: false
+#637 := [lemma #635]: #123
+#326 := (or #323 #136)
+#314 := (or #323 #136 #234)
+#325 := [def-axiom]: #314
+#254 := [unit-resolution #325 #144]: #326
+#275 := [unit-resolution #254 #637]: #323
+#276 := (or #136 #127)
+#289 := (or #133 #136 #127)
+#290 := [def-axiom]: #289
+#638 := [unit-resolution #290 #628]: #276
+[unit-resolution #638 #275 #637]: false
+unsat
+5973328496eea1e33493c38f9af9d86965f67ad9 287 0
+#2 := false
+decl f3 :: (-> S2 S3 S1)
+decl f6 :: (-> S4 S3 S3)
+decl f12 :: S3
+#44 := f12
+decl f7 :: (-> S5 S3 S4)
+decl f11 :: S3
+#42 := f11
+decl f9 :: S5
+#33 := f9
+#43 := (f7 f9 f11)
+#51 := (f6 #43 f12)
+decl f10 :: S2
+#41 := f10
+#314 := (f3 f10 #51)
+decl f1 :: S1
+#4 := f1
+#651 := (= f1 #314)
+#249 := (f3 f10 f12)
+#628 := (= f1 #249)
+#625 := (not #628)
+#339 := (f3 f10 f11)
+#355 := (= f1 #339)
+#356 := (not #355)
+#614 := (or #356 #625)
+#615 := (not #614)
+#611 := (iff #615 #651)
+#582 := (not #611)
+decl f13 :: S3
+#46 := f13
+#334 := (f3 f10 f13)
+#331 := (= f1 #334)
+#335 := (not #331)
+#484 := (or #335 #625)
+#493 := (not #484)
+#45 := (f7 f9 f12)
+#47 := (f6 #45 f13)
+#646 := (f3 f10 #47)
+#632 := (= f1 #646)
+#494 := (iff #493 #632)
+#587 := (not #494)
+#567 := [hypothesis]: #587
+#22 := (:var 0 S3)
+#20 := (:var 1 S3)
+#34 := (f7 f9 #20)
+#35 := (f6 #34 #22)
+#18 := (:var 2 S2)
+#36 := (f3 #18 #35)
+#680 := (pattern #36)
+#28 := (f3 #18 #22)
+#103 := (= f1 #28)
+#176 := (not #103)
+#26 := (f3 #18 #20)
+#100 := (= f1 #26)
+#175 := (not #100)
+#159 := (or #175 #176)
+#160 := (not #159)
+#116 := (= f1 #36)
+#177 := (iff #116 #160)
+#681 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) (:pat #680) #177)
+#180 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #177)
+#684 := (iff #180 #681)
+#682 := (iff #177 #177)
+#683 := [refl]: #682
+#685 := [quant-intro #683]: #684
+#120 := (and #100 #103)
+#123 := (iff #116 #120)
+#126 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #123)
+#181 := (iff #126 #180)
+#178 := (iff #123 #177)
+#161 := (iff #120 #160)
+#162 := [rewrite]: #161
+#179 := [monotonicity #162]: #178
+#182 := [quant-intro #179]: #181
+#157 := (~ #126 #126)
+#172 := (~ #123 #123)
+#173 := [refl]: #172
+#158 := [nnf-pos #173]: #157
+#29 := (= #28 f1)
+#27 := (= #26 f1)
+#38 := (and #27 #29)
+#37 := (= #36 f1)
+#39 := (iff #37 #38)
+#40 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #39)
+#127 := (iff #40 #126)
+#124 := (iff #39 #123)
+#121 := (iff #38 #120)
+#104 := (iff #29 #103)
+#105 := [rewrite]: #104
+#101 := (iff #27 #100)
+#102 := [rewrite]: #101
+#122 := [monotonicity #102 #105]: #121
+#118 := (iff #37 #116)
+#119 := [rewrite]: #118
+#125 := [monotonicity #119 #122]: #124
+#128 := [quant-intro #125]: #127
+#115 := [asserted]: #40
+#131 := [mp #115 #128]: #126
+#174 := [mp~ #131 #158]: #126
+#183 := [mp #174 #182]: #180
+#686 := [mp #183 #685]: #681
+#306 := (not #681)
+#498 := (or #306 #494)
+#600 := (or #625 #335)
+#482 := (not #600)
+#483 := (iff #632 #482)
+#499 := (or #306 #483)
+#593 := (iff #499 #498)
+#594 := (iff #498 #498)
+#581 := [rewrite]: #594
+#496 := (iff #483 #494)
+#592 := (iff #632 #493)
+#495 := (iff #592 #494)
+#488 := [rewrite]: #495
+#477 := (iff #483 #592)
+#588 := (iff #482 #493)
+#443 := (iff #600 #484)
+#591 := [rewrite]: #443
+#589 := [monotonicity #591]: #588
+#492 := [monotonicity #589]: #477
+#497 := [trans #492 #488]: #496
+#590 := [monotonicity #497]: #593
+#583 := [trans #590 #581]: #593
+#500 := [quant-inst #41 #44 #46]: #499
+#575 := [mp #500 #583]: #498
+#568 := [unit-resolution #575 #686 #567]: false
+#569 := [lemma #568]: #494
+#633 := (not #632)
+#357 := (or #356 #633)
+#343 := (not #357)
+#48 := (f6 #43 #47)
+#49 := (f3 f10 #48)
+#130 := (= f1 #49)
+#143 := (not #130)
+#570 := [hypothesis]: #143
+#571 := (or #130 #357)
+#358 := (iff #130 #343)
+#629 := (or #306 #358)
+#351 := [quant-inst #41 #42 #47]: #629
+#566 := [unit-resolution #351 #686]: #358
+#341 := (not #358)
+#342 := (or #341 #130 #357)
+#344 := [def-axiom]: #342
+#557 := [unit-resolution #344 #566]: #571
+#558 := [unit-resolution #557 #570]: #357
+#597 := (or #306 #611)
+#616 := (iff #651 #615)
+#613 := (or #306 #616)
+#618 := (iff #613 #597)
+#461 := (iff #597 #597)
+#462 := [rewrite]: #461
+#612 := (iff #616 #611)
+#617 := [rewrite]: #612
+#460 := [monotonicity #617]: #618
+#604 := [trans #460 #462]: #618
+#619 := [quant-inst #41 #42 #44]: #613
+#605 := [mp #619 #604]: #597
+#560 := [unit-resolution #605 #686]: #611
+#546 := (or #582 #615)
+#653 := (not #651)
+#319 := (or #335 #653)
+#655 := (not #319)
+#52 := (f7 f9 #51)
+#53 := (f6 #52 f13)
+#54 := (f3 f10 #53)
+#134 := (= f1 #54)
+#329 := (or #134 #130)
+#144 := (iff #134 #143)
+#55 := (= #54 f1)
+#50 := (= #49 f1)
+#56 := (iff #50 #55)
+#57 := (not #56)
+#147 := (iff #57 #144)
+#137 := (iff #130 #134)
+#140 := (not #137)
+#145 := (iff #140 #144)
+#146 := [rewrite]: #145
+#141 := (iff #57 #140)
+#138 := (iff #56 #137)
+#135 := (iff #55 #134)
+#136 := [rewrite]: #135
+#132 := (iff #50 #130)
+#133 := [rewrite]: #132
+#139 := [monotonicity #133 #136]: #138
+#142 := [monotonicity #139]: #141
+#148 := [trans #142 #146]: #147
+#129 := [asserted]: #57
+#151 := [mp #129 #148]: #144
+#241 := (not #144)
+#328 := (or #134 #130 #241)
+#242 := [def-axiom]: #328
+#243 := [unit-resolution #242 #151]: #329
+#561 := [unit-resolution #243 #570]: #134
+#330 := (not #134)
+#559 := (or #330 #655)
+#652 := (iff #134 #655)
+#311 := (or #306 #652)
+#308 := (or #653 #335)
+#440 := (not #308)
+#647 := (iff #134 #440)
+#649 := (or #306 #647)
+#650 := (iff #649 #311)
+#634 := (iff #311 #311)
+#295 := [rewrite]: #634
+#658 := (iff #647 #652)
+#656 := (iff #440 #655)
+#320 := (iff #308 #319)
+#654 := [rewrite]: #320
+#657 := [monotonicity #654]: #656
+#648 := [monotonicity #657]: #658
+#291 := [monotonicity #648]: #650
+#296 := [trans #291 #295]: #650
+#307 := [quant-inst #41 #51 #46]: #649
+#297 := [mp #307 #296]: #311
+#562 := [unit-resolution #297 #686]: #652
+#635 := (not #652)
+#642 := (or #635 #330 #655)
+#644 := [def-axiom]: #642
+#563 := [unit-resolution #644 #562]: #559
+#543 := [unit-resolution #563 #561]: #655
+#637 := (or #319 #651)
+#638 := [def-axiom]: #637
+#544 := [unit-resolution #638 #543]: #651
+#576 := (or #582 #615 #653)
+#577 := [def-axiom]: #576
+#547 := [unit-resolution #577 #544]: #546
+#548 := [unit-resolution #547 #560]: #615
+#606 := (or #614 #355)
+#572 := [def-axiom]: #606
+#549 := [unit-resolution #572 #548]: #355
+#631 := (or #343 #356 #633)
+#340 := [def-axiom]: #631
+#550 := [unit-resolution #340 #549 #558]: #633
+#298 := (or #319 #331)
+#636 := [def-axiom]: #298
+#551 := [unit-resolution #636 #543]: #331
+#574 := (or #614 #628)
+#584 := [def-axiom]: #574
+#552 := [unit-resolution #584 #548]: #628
+#609 := (or #493 #335 #625)
+#603 := [def-axiom]: #609
+#553 := [unit-resolution #603 #552 #551]: #493
+#441 := (or #587 #484 #632)
+#442 := [def-axiom]: #441
+#554 := [unit-resolution #442 #553 #550 #569]: false
+#555 := [lemma #554]: #130
+#545 := (or #143 #343)
+#622 := (or #341 #143 #343)
+#623 := [def-axiom]: #622
+#556 := [unit-resolution #623 #566]: #545
+#534 := [unit-resolution #556 #555]: #343
+#630 := (or #357 #632)
+#627 := [def-axiom]: #630
+#535 := [unit-resolution #627 #534]: #632
+#610 := (or #587 #493 #633)
+#439 := [def-axiom]: #610
+#537 := [unit-resolution #439 #535 #569]: #493
+#602 := (or #484 #628)
+#608 := [def-axiom]: #602
+#538 := [unit-resolution #608 #537]: #628
+#352 := (or #357 #355)
+#626 := [def-axiom]: #352
+#539 := [unit-resolution #626 #534]: #355
+#585 := (or #615 #356 #625)
+#586 := [def-axiom]: #585
+#540 := [unit-resolution #586 #539 #538]: #615
+#333 := (or #330 #143)
+#321 := (or #330 #143 #241)
+#332 := [def-axiom]: #321
+#261 := [unit-resolution #332 #151]: #333
+#541 := [unit-resolution #261 #555]: #330
+#536 := (or #134 #319)
+#641 := (or #635 #134 #319)
+#277 := [def-axiom]: #641
+#542 := [unit-resolution #277 #562]: #536
+#528 := [unit-resolution #542 #541]: #319
+#607 := (or #484 #331)
+#601 := [def-axiom]: #607
+#524 := [unit-resolution #601 #537]: #331
+#639 := (or #655 #335 #653)
+#640 := [def-axiom]: #639
+#525 := [unit-resolution #640 #524 #528]: #653
+#578 := (or #582 #614 #651)
+#579 := [def-axiom]: #578
+#526 := [unit-resolution #579 #525 #540]: #582
+[unit-resolution #605 #686 #526]: false
+unsat
+6c759b8f06a9510b6e4f2c41f45fd7a908ea138f 22 0
+#2 := false
+decl f13 :: (-> S7 S3 S4)
+decl f4 :: S3
+#8 := f4
+decl f14 :: S7
+#50 := f14
+#51 := (f13 f14 f4)
+#52 := (= #51 #51)
+#53 := (not #52)
+#148 := (iff #53 false)
+#1 := true
+#143 := (not true)
+#146 := (iff #143 false)
+#147 := [rewrite]: #146
+#144 := (iff #53 #143)
+#140 := (iff #52 true)
+#142 := [rewrite]: #140
+#145 := [monotonicity #142]: #144
+#149 := [trans #145 #147]: #148
+#139 := [asserted]: #53
+[mp #139 #149]: false
+unsat