added function update examples and set examples

--- a/src/HOL/SMT.thy	Thu May 27 17:09:37 2010 +0200
+++ b/src/HOL/SMT.thy	Thu May 27 18:16:54 2010 +0200
@@ -68,7 +68,7 @@
 *}
 
 lemmas array_rules = ext fun_upd_apply fun_upd_same fun_upd_other
-  fun_upd_upd
+  fun_upd_upd fun_app_def
 
 
 

--- a/src/HOL/SMT_Examples/SMT_Tests.certs	Thu May 27 17:09:37 2010 +0200
+++ b/src/HOL/SMT_Examples/SMT_Tests.certs	Thu May 27 18:16:54 2010 +0200
@@ -51174,3 +51174,2781 @@
 #545 := [unit-resolution #170 #207]: #239
 [unit-resolution #545 #551]: false
 unsat
+13c013ce9b60f948f65ac05c9f64640c23a178bb 50 0
+#2 := false
+decl f3 :: (-> S2 S3 S4 S3 S4)
+#15 := (:var 1 S3)
+#16 := (:var 0 S4)
+#14 := (:var 2 S2)
+#17 := (f3 #14 #15 #16 #15)
+#571 := (pattern #17)
+#54 := (= #16 #17)
+#572 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S4)) (:pat #571) #54)
+#58 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S4)) #54)
+#575 := (iff #58 #572)
+#573 := (iff #54 #54)
+#574 := [refl]: #573
+#576 := [quant-intro #574]: #575
+#87 := (~ #58 #58)
+#85 := (~ #54 #54)
+#86 := [refl]: #85
+#88 := [nnf-pos #86]: #87
+#18 := (= #17 #16)
+#19 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S4)) #18)
+#59 := (iff #19 #58)
+#56 := (iff #18 #54)
+#57 := [rewrite]: #56
+#60 := [quant-intro #57]: #59
+#53 := [asserted]: #19
+#63 := [mp #53 #60]: #58
+#79 := [mp~ #63 #88]: #58
+#577 := [mp #79 #576]: #572
+decl f5 :: S3
+#9 := f5
+decl f6 :: S4
+#10 := f6
+decl f4 :: S2
+#8 := f4
+#11 := (f3 f4 f5 f6 f5)
+#47 := (= f6 #11)
+#50 := (not #47)
+#12 := (= #11 f6)
+#13 := (not #12)
+#51 := (iff #13 #50)
+#48 := (iff #12 #47)
+#49 := [rewrite]: #48
+#52 := [monotonicity #49]: #51
+#46 := [asserted]: #13
+#55 := [mp #46 #52]: #50
+#154 := (not #572)
+#241 := (or #154 #47)
+#155 := [quant-inst]: #241
+[unit-resolution #155 #55 #577]: false
+unsat
+1359b66e79f681fc73d3d69747fa44ddaf8fc00b 85 0
+#2 := false
+decl f8 :: (-> S3 S2 S4)
+decl f4 :: S2
+#9 := f4
+decl f6 :: S3
+#12 := f6
+#15 := (f8 f6 f4)
+decl f5 :: (-> S3 S2 S4 S2 S4)
+decl f7 :: S4
+#13 := f7
+decl f3 :: S2
+#8 := f3
+#14 := (f5 f6 f3 f7 f4)
+#16 := (= #14 #15)
+#161 := (= f7 #14)
+#10 := (= f3 f4)
+#248 := (ite #10 #161 #16)
+#252 := (not #248)
+#59 := (not #16)
+#52 := (or #10 #16)
+#55 := (not #52)
+#11 := (not #10)
+#17 := (implies #11 #16)
+#18 := (not #17)
+#56 := (iff #18 #55)
+#53 := (iff #17 #52)
+#54 := [rewrite]: #53
+#57 := [monotonicity #54]: #56
+#51 := [asserted]: #18
+#60 := [mp #51 #57]: #55
+#61 := [not-or-elim #60]: #59
+#58 := [not-or-elim #60]: #11
+#254 := (or #252 #10 #16)
+#251 := [def-axiom]: #254
+#162 := [unit-resolution #251 #58 #61]: #252
+#28 := (:var 0 S2)
+#27 := (:var 1 S4)
+#26 := (:var 2 S2)
+#25 := (:var 3 S3)
+#29 := (f5 #25 #26 #27 #28)
+#586 := (pattern #29)
+#31 := (f8 #25 #28)
+#83 := (= #29 #31)
+#86 := (= #27 #29)
+#70 := (= #26 #28)
+#93 := (ite #70 #86 #83)
+#587 := (forall (vars (?v0 S3) (?v1 S2) (?v2 S4) (?v3 S2)) (:pat #586) #93)
+#100 := (forall (vars (?v0 S3) (?v1 S2) (?v2 S4) (?v3 S2)) #93)
+#590 := (iff #100 #587)
+#588 := (iff #93 #93)
+#589 := [refl]: #588
+#591 := [quant-intro #589]: #590
+#74 := (ite #70 #27 #31)
+#77 := (= #29 #74)
+#80 := (forall (vars (?v0 S3) (?v1 S2) (?v2 S4) (?v3 S2)) #77)
+#101 := (iff #80 #100)
+#94 := (iff #77 #93)
+#99 := [rewrite]: #94
+#102 := [quant-intro #99]: #101
+#91 := (~ #80 #80)
+#90 := (~ #77 #77)
+#87 := [refl]: #90
+#92 := [nnf-pos #87]: #91
+#30 := (= #28 #26)
+#32 := (ite #30 #27 #31)
+#33 := (= #29 #32)
+#34 := (forall (vars (?v0 S3) (?v1 S2) (?v2 S4) (?v3 S2)) #33)
+#81 := (iff #34 #80)
+#78 := (iff #33 #77)
+#75 := (= #32 #74)
+#72 := (iff #30 #70)
+#73 := [rewrite]: #72
+#76 := [monotonicity #73]: #75
+#79 := [monotonicity #76]: #78
+#82 := [quant-intro #79]: #81
+#69 := [asserted]: #34
+#85 := [mp #69 #82]: #80
+#88 := [mp~ #85 #92]: #80
+#103 := [mp #88 #102]: #100
+#592 := [mp #103 #591]: #587
+#163 := (not #587)
+#250 := (or #163 #248)
+#241 := [quant-inst]: #250
+[unit-resolution #241 #592 #162]: false
+unsat
+85295dd87d7cebdd794ace783556d1b1d280619a 158 0
+#2 := false
+decl f5 :: (-> S3 S2 S4)
+decl f3 :: S2
+#8 := f3
+decl f6 :: (-> S3 S2 S4 S3)
+decl f9 :: S4
+#15 := f9
+decl f4 :: S2
+#9 := f4
+decl f8 :: S4
+#13 := f8
+decl f7 :: S3
+#12 := f7
+#14 := (f6 f7 f3 f8)
+#16 := (f6 #14 f4 f9)
+#17 := (f5 #16 f3)
+#56 := (= f8 #17)
+#173 := (f5 #14 f3)
+#264 := (= #17 #173)
+#577 := (iff #264 #56)
+#214 := (iff #56 #264)
+#567 := (= #173 #17)
+#574 := (iff #567 #264)
+#576 := [commutativity]: #574
+#573 := (iff #56 #567)
+#260 := (= f8 #173)
+#23 := (:var 0 S4)
+#22 := (:var 1 S2)
+#21 := (:var 2 S3)
+#24 := (f6 #21 #22 #23)
+#591 := (pattern #24)
+#25 := (f5 #24 #22)
+#75 := (= #23 #25)
+#593 := (forall (vars (?v0 S3) (?v1 S2) (?v2 S4)) (:pat #591) #75)
+#78 := (forall (vars (?v0 S3) (?v1 S2) (?v2 S4)) #75)
+#592 := (iff #78 #593)
+#595 := (iff #593 #593)
+#596 := [rewrite]: #595
+#594 := [rewrite]: #592
+#597 := [trans #594 #596]: #592
+#109 := (~ #78 #78)
+#107 := (~ #75 #75)
+#108 := [refl]: #107
+#110 := [nnf-pos #108]: #109
+#26 := (= #25 #23)
+#27 := (forall (vars (?v0 S3) (?v1 S2) (?v2 S4)) #26)
+#79 := (iff #27 #78)
+#76 := (iff #26 #75)
+#77 := [rewrite]: #76
+#80 := [quant-intro #77]: #79
+#74 := [asserted]: #27
+#83 := [mp #74 #80]: #78
+#101 := [mp~ #83 #110]: #78
+#598 := [mp #101 #597]: #593
+#175 := (not #593)
+#262 := (or #175 #260)
+#253 := [quant-inst]: #262
+#572 := [unit-resolution #253 #598]: #260
+#209 := [monotonicity #572]: #573
+#215 := [trans #209 #576]: #214
+#575 := [symm #215]: #577
+#265 := (= f9 #17)
+#10 := (= f3 f4)
+#585 := (ite #10 #265 #264)
+#32 := (:var 0 S2)
+#30 := (:var 1 S4)
+#29 := (:var 2 S2)
+#28 := (:var 3 S3)
+#31 := (f6 #28 #29 #30)
+#33 := (f5 #31 #32)
+#599 := (pattern #33)
+#35 := (f5 #28 #32)
+#95 := (= #33 #35)
+#98 := (= #30 #33)
+#82 := (= #29 #32)
+#105 := (ite #82 #98 #95)
+#600 := (forall (vars (?v0 S3) (?v1 S2) (?v2 S4) (?v3 S2)) (:pat #599) #105)
+#112 := (forall (vars (?v0 S3) (?v1 S2) (?v2 S4) (?v3 S2)) #105)
+#603 := (iff #112 #600)
+#601 := (iff #105 #105)
+#602 := [refl]: #601
+#604 := [quant-intro #602]: #603
+#86 := (ite #82 #30 #35)
+#89 := (= #33 #86)
+#92 := (forall (vars (?v0 S3) (?v1 S2) (?v2 S4) (?v3 S2)) #89)
+#113 := (iff #92 #112)
+#106 := (iff #89 #105)
+#111 := [rewrite]: #106
+#114 := [quant-intro #111]: #113
+#103 := (~ #92 #92)
+#102 := (~ #89 #89)
+#99 := [refl]: #102
+#104 := [nnf-pos #99]: #103
+#34 := (= #32 #29)
+#36 := (ite #34 #30 #35)
+#37 := (= #33 #36)
+#38 := (forall (vars (?v0 S3) (?v1 S2) (?v2 S4) (?v3 S2)) #37)
+#93 := (iff #38 #92)
+#90 := (iff #37 #89)
+#87 := (= #36 #86)
+#84 := (iff #34 #82)
+#85 := [rewrite]: #84
+#88 := [monotonicity #85]: #87
+#91 := [monotonicity #88]: #90
+#94 := [quant-intro #91]: #93
+#81 := [asserted]: #38
+#97 := [mp #81 #94]: #92
+#100 := [mp~ #97 #104]: #92
+#115 := [mp #100 #114]: #112
+#605 := [mp #115 #604]: #600
+#579 := (not #600)
+#251 := (or #579 #585)
+#263 := (= f4 f3)
+#267 := (ite #263 #265 #264)
+#252 := (or #579 #267)
+#587 := (iff #252 #251)
+#589 := (iff #251 #251)
+#584 := [rewrite]: #589
+#240 := (iff #267 #585)
+#246 := (iff #263 #10)
+#583 := [rewrite]: #246
+#372 := [monotonicity #583]: #240
+#588 := [monotonicity #372]: #587
+#590 := [trans #588 #584]: #587
+#586 := [quant-inst]: #252
+#580 := [mp #586 #590]: #251
+#568 := [unit-resolution #580 #605]: #585
+#238 := (not #585)
+#569 := (or #238 #264)
+#11 := (not #10)
+#62 := (or #10 #56)
+#67 := (not #62)
+#18 := (= #17 f8)
+#19 := (implies #11 #18)
+#20 := (not #19)
+#68 := (iff #20 #67)
+#65 := (iff #19 #62)
+#59 := (implies #11 #56)
+#63 := (iff #59 #62)
+#64 := [rewrite]: #63
+#60 := (iff #19 #59)
+#57 := (iff #18 #56)
+#58 := [rewrite]: #57
+#61 := [monotonicity #58]: #60
+#66 := [trans #61 #64]: #65
+#69 := [monotonicity #66]: #68
+#55 := [asserted]: #20
+#72 := [mp #55 #69]: #67
+#70 := [not-or-elim #72]: #11
+#239 := (or #238 #10 #264)
+#582 := [def-axiom]: #239
+#570 := [unit-resolution #582 #70]: #569
+#571 := [unit-resolution #570 #568]: #264
+#578 := [mp #571 #575]: #56
+#71 := (not #56)
+#73 := [not-or-elim #72]: #71
+[unit-resolution #73 #578]: false
+unsat
+c0ecafa6d8b41ce5e1c9ab26d4838fdbd8c57d3d 72 0
+#2 := false
+decl f6 :: (-> S3 S2 S4 S3)
+#23 := (:var 0 S4)
+#22 := (:var 1 S2)
+#21 := (:var 2 S3)
+#24 := (f6 #21 #22 #23)
+#591 := (pattern #24)
+decl f5 :: (-> S3 S2 S4)
+#25 := (f5 #24 #22)
+#75 := (= #23 #25)
+#593 := (forall (vars (?v0 S3) (?v1 S2) (?v2 S4)) (:pat #591) #75)
+#78 := (forall (vars (?v0 S3) (?v1 S2) (?v2 S4)) #75)
+#592 := (iff #78 #593)
+#595 := (iff #593 #593)
+#596 := [rewrite]: #595
+#594 := [rewrite]: #592
+#597 := [trans #594 #596]: #592
+#109 := (~ #78 #78)
+#107 := (~ #75 #75)
+#108 := [refl]: #107
+#110 := [nnf-pos #108]: #109
+#26 := (= #25 #23)
+#27 := (forall (vars (?v0 S3) (?v1 S2) (?v2 S4)) #26)
+#79 := (iff #27 #78)
+#76 := (iff #26 #75)
+#77 := [rewrite]: #76
+#80 := [quant-intro #77]: #79
+#74 := [asserted]: #27
+#83 := [mp #74 #80]: #78
+#101 := [mp~ #83 #110]: #78
+#598 := [mp #101 #597]: #593
+decl f4 :: S2
+#9 := f4
+decl f9 :: S4
+#15 := f9
+decl f8 :: S4
+#13 := f8
+decl f3 :: S2
+#8 := f3
+decl f7 :: S3
+#12 := f7
+#14 := (f6 f7 f3 f8)
+#16 := (f6 #14 f4 f9)
+#17 := (f5 #16 f4)
+#56 := (= f9 #17)
+#71 := (not #56)
+#10 := (= f3 f4)
+#62 := (or #10 #56)
+#67 := (not #62)
+#18 := (= #17 f9)
+#11 := (not #10)
+#19 := (implies #11 #18)
+#20 := (not #19)
+#68 := (iff #20 #67)
+#65 := (iff #19 #62)
+#59 := (implies #11 #56)
+#63 := (iff #59 #62)
+#64 := [rewrite]: #63
+#60 := (iff #19 #59)
+#57 := (iff #18 #56)
+#58 := [rewrite]: #57
+#61 := [monotonicity #58]: #60
+#66 := [trans #61 #64]: #65
+#69 := [monotonicity #66]: #68
+#55 := [asserted]: #20
+#72 := [mp #55 #69]: #67
+#73 := [not-or-elim #72]: #71
+#175 := (not #593)
+#264 := (or #175 #56)
+#265 := [quant-inst]: #264
+[unit-resolution #265 #73 #598]: false
+unsat
+dc41ee203ffc081fb445ff0000ddb4be9134fe60 81 0
+#2 := false
+decl f5 :: (-> S3 S2 S4)
+decl f3 :: S2
+#8 := f3
+decl f6 :: (-> S3 S2 S4 S3)
+decl f9 :: S4
+#14 := f9
+decl f4 :: S2
+#9 := f4
+decl f8 :: S4
+#12 := f8
+decl f7 :: S3
+#11 := f7
+#13 := (f6 f7 f3 f8)
+#15 := (f6 #13 f4 f9)
+#16 := (f5 #15 f3)
+#55 := (= f9 #16)
+#261 := (f5 #15 f4)
+#228 := (= #261 #16)
+#566 := (= #16 #261)
+#10 := (= f3 f4)
+#61 := (not #10)
+#62 := (or #61 #55)
+#67 := (not #62)
+#17 := (= #16 f9)
+#18 := (implies #10 #17)
+#19 := (not #18)
+#68 := (iff #19 #67)
+#65 := (iff #18 #62)
+#58 := (implies #10 #55)
+#63 := (iff #58 #62)
+#64 := [rewrite]: #63
+#59 := (iff #18 #58)
+#56 := (iff #17 #55)
+#57 := [rewrite]: #56
+#60 := [monotonicity #57]: #59
+#66 := [trans #60 #64]: #65
+#69 := [monotonicity #66]: #68
+#54 := [asserted]: #19
+#72 := [mp #54 #69]: #67
+#70 := [not-or-elim #72]: #10
+#227 := [monotonicity #70]: #566
+#229 := [symm #227]: #228
+#175 := (= f9 #261)
+#22 := (:var 0 S4)
+#21 := (:var 1 S2)
+#20 := (:var 2 S3)
+#23 := (f6 #20 #21 #22)
+#591 := (pattern #23)
+#24 := (f5 #23 #21)
+#75 := (= #22 #24)
+#593 := (forall (vars (?v0 S3) (?v1 S2) (?v2 S4)) (:pat #591) #75)
+#78 := (forall (vars (?v0 S3) (?v1 S2) (?v2 S4)) #75)
+#592 := (iff #78 #593)
+#595 := (iff #593 #593)
+#596 := [rewrite]: #595
+#594 := [rewrite]: #592
+#597 := [trans #594 #596]: #592
+#109 := (~ #78 #78)
+#107 := (~ #75 #75)
+#108 := [refl]: #107
+#110 := [nnf-pos #108]: #109
+#25 := (= #24 #22)
+#26 := (forall (vars (?v0 S3) (?v1 S2) (?v2 S4)) #25)
+#79 := (iff #26 #78)
+#76 := (iff #25 #75)
+#77 := [rewrite]: #76
+#80 := [quant-intro #77]: #79
+#74 := [asserted]: #26
+#83 := [mp #74 #80]: #78
+#101 := [mp~ #83 #110]: #78
+#598 := [mp #101 #597]: #593
+#262 := (not #593)
+#266 := (or #262 #175)
+#263 := [quant-inst]: #266
+#223 := [unit-resolution #263 #598]: #175
+#230 := [trans #223 #229]: #55
+#71 := (not #55)
+#73 := [not-or-elim #72]: #71
+[unit-resolution #73 #230]: false
+unsat
+ae5be72196cf39e4c9692c5e427b5fb33965ed8f 187 0
+#2 := false
+decl f6 :: (-> S3 S2 S4)
+decl f5 :: S2
+#10 := f5
+decl f8 :: S3
+#12 := f8
+#18 := (f6 f8 f5)
+decl f7 :: (-> S3 S2 S4 S3)
+decl f10 :: S4
+#15 := f10
+decl f4 :: S2
+#9 := f4
+decl f9 :: S4
+#13 := f9
+decl f3 :: S2
+#8 := f3
+#14 := (f7 f8 f3 f9)
+#16 := (f7 #14 f4 f10)
+#17 := (f6 #16 f5)
+#19 := (= #17 #18)
+#246 := (f6 #14 f3)
+#560 := (f7 f8 f3 #246)
+#536 := (f6 #560 f5)
+#365 := (= #536 #18)
+#521 := (= #18 #536)
+#367 := (= #246 #536)
+#168 := (= f3 f5)
+#525 := (ite #168 #367 #521)
+#33 := (:var 0 S2)
+#31 := (:var 1 S4)
+#30 := (:var 2 S2)
+#29 := (:var 3 S3)
+#32 := (f7 #29 #30 #31)
+#34 := (f6 #32 #33)
+#593 := (pattern #34)
+#36 := (f6 #29 #33)
+#89 := (= #34 #36)
+#92 := (= #31 #34)
+#76 := (= #30 #33)
+#99 := (ite #76 #92 #89)
+#594 := (forall (vars (?v0 S3) (?v1 S2) (?v2 S4) (?v3 S2)) (:pat #593) #99)
+#106 := (forall (vars (?v0 S3) (?v1 S2) (?v2 S4) (?v3 S2)) #99)
+#597 := (iff #106 #594)
+#595 := (iff #99 #99)
+#596 := [refl]: #595
+#598 := [quant-intro #596]: #597
+#80 := (ite #76 #31 #36)
+#83 := (= #34 #80)
+#86 := (forall (vars (?v0 S3) (?v1 S2) (?v2 S4) (?v3 S2)) #83)
+#107 := (iff #86 #106)
+#100 := (iff #83 #99)
+#105 := [rewrite]: #100
+#108 := [quant-intro #105]: #107
+#97 := (~ #86 #86)
+#96 := (~ #83 #83)
+#93 := [refl]: #96
+#98 := [nnf-pos #93]: #97
+#35 := (= #33 #30)
+#37 := (ite #35 #31 #36)
+#38 := (= #34 #37)
+#39 := (forall (vars (?v0 S3) (?v1 S2) (?v2 S4) (?v3 S2)) #38)
+#87 := (iff #39 #86)
+#84 := (iff #38 #83)
+#81 := (= #37 #80)
+#78 := (iff #35 #76)
+#79 := [rewrite]: #78
+#82 := [monotonicity #79]: #81
+#85 := [monotonicity #82]: #84
+#88 := [quant-intro #85]: #87
+#75 := [asserted]: #39
+#91 := [mp #75 #88]: #86
+#94 := [mp~ #91 #98]: #86
+#109 := [mp #94 #108]: #106
+#599 := [mp #109 #598]: #594
+#221 := (not #594)
+#408 := (or #221 #525)
+#368 := (ite #168 #367 #365)
+#409 := (or #221 #368)
+#369 := (iff #409 #408)
+#419 := (iff #408 #408)
+#514 := [rewrite]: #419
+#523 := (iff #368 #525)
+#522 := (iff #365 #521)
+#524 := [rewrite]: #522
+#526 := [monotonicity #524]: #523
+#517 := [monotonicity #526]: #369
+#515 := [trans #517 #514]: #369
+#410 := [quant-inst]: #409
+#518 := [mp #410 #515]: #408
+#498 := [unit-resolution #518 #599]: #525
+#403 := (not #525)
+#511 := (or #403 #521)
+#255 := (not #168)
+#169 := (= f4 f5)
+#256 := (not #169)
+#167 := (= f3 f4)
+#254 := (not #167)
+#247 := (and #254 #255 #256)
+#11 := (distinct f3 f4 f5)
+#57 := (not #11)
+#58 := (or #57 #19)
+#61 := (not #58)
+#20 := (implies #11 #19)
+#21 := (not #20)
+#62 := (iff #21 #61)
+#59 := (iff #20 #58)
+#60 := [rewrite]: #59
+#63 := [monotonicity #60]: #62
+#56 := [asserted]: #21
+#66 := [mp #56 #63]: #61
+#64 := [not-or-elim #66]: #11
+#234 := (or #57 #247)
+#366 := [def-axiom]: #234
+#500 := [unit-resolution #366 #64]: #247
+#258 := (not #247)
+#260 := (or #258 #255)
+#257 := [def-axiom]: #260
+#510 := [unit-resolution #257 #500]: #255
+#421 := (or #403 #168 #521)
+#414 := [def-axiom]: #421
+#512 := [unit-resolution #414 #510]: #511
+#508 := [unit-resolution #512 #498]: #521
+#493 := [symm #508]: #365
+#494 := (= #17 #536)
+#574 := (f6 #14 f5)
+#490 := (= #574 #536)
+#499 := (= #536 #574)
+#509 := (= #560 #14)
+#520 := (= #246 f9)
+#580 := (= f9 #246)
+#24 := (:var 0 S4)
+#23 := (:var 1 S2)
+#22 := (:var 2 S3)
+#25 := (f7 #22 #23 #24)
+#585 := (pattern #25)
+#26 := (f6 #25 #23)
+#69 := (= #24 #26)
+#587 := (forall (vars (?v0 S3) (?v1 S2) (?v2 S4)) (:pat #585) #69)
+#72 := (forall (vars (?v0 S3) (?v1 S2) (?v2 S4)) #69)
+#586 := (iff #72 #587)
+#589 := (iff #587 #587)
+#590 := [rewrite]: #589
+#588 := [rewrite]: #586
+#591 := [trans #588 #590]: #586
+#103 := (~ #72 #72)
+#101 := (~ #69 #69)
+#102 := [refl]: #101
+#104 := [nnf-pos #102]: #103
+#27 := (= #26 #24)
+#28 := (forall (vars (?v0 S3) (?v1 S2) (?v2 S4)) #27)
+#73 := (iff #28 #72)
+#70 := (iff #27 #69)
+#71 := [rewrite]: #70
+#74 := [quant-intro #71]: #73
+#68 := [asserted]: #28
+#77 := [mp #68 #74]: #72
+#95 := [mp~ #77 #104]: #72
+#592 := [mp #95 #591]: #587
+#583 := (not #587)
+#578 := (or #583 #580)
+#584 := [quant-inst]: #578
+#516 := [unit-resolution #584 #592]: #580
+#507 := [symm #516]: #520
+#501 := [monotonicity #507]: #509
+#506 := [monotonicity #501]: #499
+#491 := [symm #506]: #490
+#232 := (= #17 #574)
+#233 := (= f10 #17)
+#576 := (ite #169 #233 #232)
+#222 := (or #221 #576)
+#223 := [quant-inst]: #222
+#513 := [unit-resolution #223 #599]: #576
+#224 := (not #576)
+#503 := (or #224 #232)
+#261 := (or #258 #256)
+#240 := [def-axiom]: #261
+#502 := [unit-resolution #240 #500]: #256
+#564 := (or #224 #169 #232)
+#565 := [def-axiom]: #564
+#504 := [unit-resolution #565 #502]: #503
+#505 := [unit-resolution #504 #513]: #232
+#495 := [trans #505 #491]: #494
+#496 := [trans #495 #493]: #19
+#65 := (not #19)
+#67 := [not-or-elim #66]: #65
+[unit-resolution #67 #496]: false
+unsat
+2f659b6a47ef547b90b00946538367bd9efdeee0 31 0
+#2 := false
+decl f1 :: S1
+#4 := f1
+decl f3 :: (-> S2 S1)
+decl f4 :: S2
+#8 := f4
+#9 := (f3 f4)
+#10 := (= #9 f1)
+#11 := (iff #10 #10)
+#12 := (not #11)
+#78 := (iff #12 false)
+#1 := true
+#73 := (not true)
+#76 := (iff #73 false)
+#77 := [rewrite]: #76
+#74 := (iff #12 #73)
+#71 := (iff #11 true)
+#63 := (= f1 #9)
+#66 := (iff #63 #63)
+#69 := (iff #66 true)
+#70 := [rewrite]: #69
+#67 := (iff #11 #66)
+#64 := (iff #10 #63)
+#65 := [rewrite]: #64
+#68 := [monotonicity #65 #65]: #67
+#72 := [trans #68 #70]: #71
+#75 := [monotonicity #72]: #74
+#79 := [trans #75 #77]: #78
+#62 := [asserted]: #12
+[mp #62 #79]: false
+unsat
+3329505aa680c82f608d61377279461a25778b94 58 0
+#2 := false
+decl f3 :: (-> S2 S1)
+#13 := (:var 0 S2)
+#14 := (f3 #13)
+#661 := (pattern #14)
+decl f1 :: S1
+#4 := f1
+#77 := (= f1 #14)
+#81 := (not #77)
+#662 := (forall (vars (?v0 S2)) (:pat #661) #81)
+#84 := (forall (vars (?v0 S2)) #81)
+#665 := (iff #84 #662)
+#663 := (iff #81 #81)
+#664 := [refl]: #663
+#666 := [quant-intro #664]: #665
+#151 := (~ #84 #84)
+#149 := (~ #81 #81)
+#150 := [refl]: #149
+#152 := [nnf-pos #150]: #151
+#15 := (= #14 f1)
+#16 := (not #15)
+#17 := (forall (vars (?v0 S2)) #16)
+#85 := (iff #17 #84)
+#82 := (iff #16 #81)
+#79 := (iff #15 #77)
+#80 := [rewrite]: #79
+#83 := [monotonicity #80]: #82
+#86 := [quant-intro #83]: #85
+#76 := [asserted]: #17
+#89 := [mp #76 #86]: #84
+#139 := [mp~ #89 #152]: #84
+#667 := [mp #139 #666]: #662
+decl f4 :: S2
+#8 := f4
+#9 := (f3 f4)
+#63 := (= f1 #9)
+#10 := (= #9 f1)
+#11 := (not #10)
+#12 := (not #11)
+#74 := (iff #12 #63)
+#66 := (not #63)
+#69 := (not #66)
+#72 := (iff #69 #63)
+#73 := [rewrite]: #72
+#70 := (iff #12 #69)
+#67 := (iff #11 #66)
+#64 := (iff #10 #63)
+#65 := [rewrite]: #64
+#68 := [monotonicity #65]: #67
+#71 := [monotonicity #68]: #70
+#75 := [trans #71 #73]: #74
+#62 := [asserted]: #12
+#78 := [mp #62 #75]: #63
+#246 := (not #662)
+#333 := (or #246 #66)
+#247 := [quant-inst]: #333
+[unit-resolution #247 #78 #667]: false
+unsat
+f68aac6d5243061ae9a95773075ebafc014b27eb 46 0
+#2 := false
+decl f3 :: (-> S2 S1)
+#17 := (:var 0 S2)
+#18 := (f3 #17)
+#660 := (pattern #18)
+decl f1 :: S1
+#4 := f1
+#80 := (= f1 #18)
+#661 := (forall (vars (?v0 S2)) (:pat #660) #80)
+#84 := (forall (vars (?v0 S2)) #80)
+#664 := (iff #84 #661)
+#662 := (iff #80 #80)
+#663 := [refl]: #662
+#665 := [quant-intro #663]: #664
+#133 := (~ #84 #84)
+#132 := (~ #80 #80)
+#130 := [refl]: #132
+#134 := [nnf-pos #130]: #133
+#19 := (= #18 f1)
+#20 := (forall (vars (?v0 S2)) #19)
+#85 := (iff #20 #84)
+#82 := (iff #19 #80)
+#83 := [rewrite]: #82
+#86 := [quant-intro #83]: #85
+#79 := [asserted]: #20
+#89 := [mp #79 #86]: #84
+#127 := [mp~ #89 #134]: #84
+#666 := [mp #127 #665]: #661
+decl f4 :: S2
+#8 := f4
+#9 := (f3 f4)
+#62 := (= f1 #9)
+#65 := (not #62)
+#10 := (= #9 f1)
+#11 := (not #10)
+#66 := (iff #11 #65)
+#63 := (iff #10 #62)
+#64 := [rewrite]: #63
+#67 := [monotonicity #64]: #66
+#61 := [asserted]: #11
+#70 := [mp #61 #67]: #65
+#238 := (not #661)
+#325 := (or #238 #62)
+#239 := [quant-inst]: #325
+[unit-resolution #239 #70 #666]: false
+unsat
+fca05a20824fb9ae1ae5b948aca1cdacb4ec3a3d 119 0
+#2 := false
+decl f3 :: (-> S2 S2 S3 S1)
+decl f6 :: S3
+#10 := f6
+decl f5 :: S2
+#9 := f5
+decl f4 :: S2
+#8 := f4
+#11 := (f3 f4 f5 f6)
+decl f1 :: S1
+#4 := f1
+#70 := (= f1 #11)
+#88 := (not #70)
+#667 := [hypothesis]: #88
+decl f7 :: (-> S2 S3 S1)
+#15 := (f7 f5 f6)
+#76 := (= f1 #15)
+#13 := (f7 f4 f6)
+#73 := (= f1 #13)
+#79 := (or #73 #76)
+#357 := (or #79 #70)
+#89 := (iff #79 #88)
+#16 := (= #15 f1)
+#14 := (= #13 f1)
+#17 := (or #14 #16)
+#12 := (= #11 f1)
+#18 := (iff #12 #17)
+#19 := (not #18)
+#92 := (iff #19 #89)
+#82 := (iff #70 #79)
+#85 := (not #82)
+#90 := (iff #85 #89)
+#91 := [rewrite]: #90
+#86 := (iff #19 #85)
+#83 := (iff #18 #82)
+#80 := (iff #17 #79)
+#77 := (iff #16 #76)
+#78 := [rewrite]: #77
+#74 := (iff #14 #73)
+#75 := [rewrite]: #74
+#81 := [monotonicity #75 #78]: #80
+#71 := (iff #12 #70)
+#72 := [rewrite]: #71
+#84 := [monotonicity #72 #81]: #83
+#87 := [monotonicity #84]: #86
+#93 := [trans #87 #91]: #92
+#69 := [asserted]: #19
+#96 := [mp #69 #93]: #89
+#283 := (not #89)
+#356 := (or #79 #70 #283)
+#353 := [def-axiom]: #356
+#336 := [unit-resolution #353 #96]: #357
+#341 := [unit-resolution #336 #667]: #79
+#343 := (not #79)
+#670 := (or #70 #343)
+#31 := (:var 0 S3)
+#30 := (:var 1 S2)
+#29 := (:var 2 S2)
+#32 := (f3 #29 #30 #31)
+#693 := (pattern #32)
+#36 := (f7 #30 #31)
+#121 := (= f1 #36)
+#34 := (f7 #29 #31)
+#118 := (= f1 #34)
+#124 := (or #118 #121)
+#114 := (= f1 #32)
+#127 := (iff #114 #124)
+#694 := (forall (vars (?v0 S2) (?v1 S2) (?v2 S3)) (:pat #693) #127)
+#130 := (forall (vars (?v0 S2) (?v1 S2) (?v2 S3)) #127)
+#697 := (iff #130 #694)
+#695 := (iff #127 #127)
+#696 := [refl]: #695
+#698 := [quant-intro #696]: #697
+#161 := (~ #130 #130)
+#171 := (~ #127 #127)
+#172 := [refl]: #171
+#162 := [nnf-pos #172]: #161
+#37 := (= #36 f1)
+#35 := (= #34 f1)
+#38 := (or #35 #37)
+#33 := (= #32 f1)
+#39 := (iff #33 #38)
+#40 := (forall (vars (?v0 S2) (?v1 S2) (?v2 S3)) #39)
+#131 := (iff #40 #130)
+#128 := (iff #39 #127)
+#125 := (iff #38 #124)
+#122 := (iff #37 #121)
+#123 := [rewrite]: #122
+#119 := (iff #35 #118)
+#120 := [rewrite]: #119
+#126 := [monotonicity #120 #123]: #125
+#116 := (iff #33 #114)
+#117 := [rewrite]: #116
+#129 := [monotonicity #117 #126]: #128
+#132 := [quant-intro #129]: #131
+#113 := [asserted]: #40
+#135 := [mp #113 #132]: #130
+#173 := [mp~ #135 #162]: #130
+#699 := [mp #173 #698]: #694
+#342 := (not #694)
+#674 := (or #342 #82)
+#675 := [quant-inst]: #674
+#329 := [unit-resolution #675 #699]: #82
+#676 := (or #85 #70 #343)
+#677 := [def-axiom]: #676
+#313 := [unit-resolution #677 #329]: #670
+#654 := [unit-resolution #313 #341 #667]: false
+#317 := [lemma #654]: #70
+#330 := (or #343 #88)
+#671 := (or #343 #88 #283)
+#673 := [def-axiom]: #671
+#460 := [unit-resolution #673 #96]: #330
+#318 := [unit-resolution #460 #317]: #343
+#319 := (or #88 #79)
+#672 := (or #85 #88 #79)
+#678 := [def-axiom]: #672
+#320 := [unit-resolution #678 #329]: #319
+[unit-resolution #320 #318 #317]: false
+unsat
+3c528fd543bec1b0abe827803d678f1293dd7fb0 154 0
+#2 := false
+decl f7 :: (-> S2 S3 S1)
+decl f6 :: S3
+#10 := f6
+decl f5 :: S2
+#9 := f5
+#346 := (f7 f5 f6)
+decl f1 :: S1
+#4 := f1
+#343 := (= f1 #346)
+decl f4 :: S2
+#8 := f4
+#13 := (f7 f4 f6)
+#69 := (= f1 #13)
+#347 := (or #69 #343)
+decl f3 :: (-> S2 S2 S3 S1)
+#11 := (f3 f4 f5 f6)
+#66 := (= f1 #11)
+#78 := (not #66)
+#661 := [hypothesis]: #78
+#341 := (or #69 #66)
+#79 := (iff #69 #78)
+#14 := (= #13 f1)
+#12 := (= #11 f1)
+#15 := (iff #12 #14)
+#16 := (not #15)
+#82 := (iff #16 #79)
+#72 := (iff #66 #69)
+#75 := (not #72)
+#80 := (iff #75 #79)
+#81 := [rewrite]: #80
+#76 := (iff #16 #75)
+#73 := (iff #15 #72)
+#70 := (iff #14 #69)
+#71 := [rewrite]: #70
+#67 := (iff #12 #66)
+#68 := [rewrite]: #67
+#74 := [monotonicity #68 #71]: #73
+#77 := [monotonicity #74]: #76
+#83 := [trans #77 #81]: #82
+#65 := [asserted]: #16
+#86 := [mp #65 #83]: #79
+#253 := (not #79)
+#340 := (or #69 #66 #253)
+#254 := [def-axiom]: #340
+#255 := [unit-resolution #254 #86]: #341
+#663 := [unit-resolution #255 #661]: #69
+#667 := (not #347)
+#309 := (or #66 #667)
+#326 := (iff #66 #347)
+#17 := (:var 0 S3)
+#27 := (:var 1 S2)
+#26 := (:var 2 S2)
+#28 := (f3 #26 #27 #17)
+#683 := (pattern #28)
+#32 := (f7 #27 #17)
+#111 := (= f1 #32)
+#30 := (f7 #26 #17)
+#108 := (= f1 #30)
+#114 := (or #108 #111)
+#104 := (= f1 #28)
+#117 := (iff #104 #114)
+#684 := (forall (vars (?v0 S2) (?v1 S2) (?v2 S3)) (:pat #683) #117)
+#120 := (forall (vars (?v0 S2) (?v1 S2) (?v2 S3)) #117)
+#687 := (iff #120 #684)
+#685 := (iff #117 #117)
+#686 := [refl]: #685
+#688 := [quant-intro #686]: #687
+#151 := (~ #120 #120)
+#161 := (~ #117 #117)
+#162 := [refl]: #161
+#152 := [nnf-pos #162]: #151
+#33 := (= #32 f1)
+#31 := (= #30 f1)
+#34 := (or #31 #33)
+#29 := (= #28 f1)
+#35 := (iff #29 #34)
+#36 := (forall (vars (?v0 S2) (?v1 S2) (?v2 S3)) #35)
+#121 := (iff #36 #120)
+#118 := (iff #35 #117)
+#115 := (iff #34 #114)
+#112 := (iff #33 #111)
+#113 := [rewrite]: #112
+#109 := (iff #31 #108)
+#110 := [rewrite]: #109
+#116 := [monotonicity #110 #113]: #115
+#106 := (iff #29 #104)
+#107 := [rewrite]: #106
+#119 := [monotonicity #107 #116]: #118
+#122 := [quant-intro #119]: #121
+#103 := [asserted]: #36
+#125 := [mp #103 #122]: #120
+#163 := [mp~ #125 #152]: #120
+#689 := [mp #163 #688]: #684
+#320 := (not #684)
+#450 := (or #320 #326)
+#657 := [quant-inst]: #450
+#308 := [unit-resolution #657 #689]: #326
+#658 := (not #326)
+#318 := (or #658 #66 #667)
+#323 := [def-axiom]: #318
+#310 := [unit-resolution #323 #308]: #309
+#646 := [unit-resolution #310 #661]: #667
+#342 := (not #69)
+#331 := (or #347 #342)
+#332 := [def-axiom]: #331
+#647 := [unit-resolution #332 #646 #663]: false
+#648 := [lemma #647]: #66
+#649 := (or #78 #347)
+#659 := (or #658 #78 #347)
+#319 := [def-axiom]: #659
+#650 := [unit-resolution #319 #308]: #649
+#652 := [unit-resolution #650 #648]: #347
+#345 := (or #342 #78)
+#333 := (or #342 #78 #253)
+#344 := [def-axiom]: #333
+#273 := [unit-resolution #344 #86]: #345
+#654 := [unit-resolution #273 #648]: #342
+#662 := (or #667 #69 #343)
+#668 := [def-axiom]: #662
+#294 := [unit-resolution #668 #654 #652]: #343
+#18 := (f7 f5 #17)
+#669 := (pattern #18)
+#85 := (= f1 #18)
+#89 := (not #85)
+#670 := (forall (vars (?v0 S3)) (:pat #669) #89)
+#92 := (forall (vars (?v0 S3)) #89)
+#673 := (iff #92 #670)
+#671 := (iff #89 #89)
+#672 := [refl]: #671
+#674 := [quant-intro #672]: #673
+#159 := (~ #92 #92)
+#157 := (~ #89 #89)
+#158 := [refl]: #157
+#160 := [nnf-pos #158]: #159
+#19 := (= #18 f1)
+#20 := (not #19)
+#21 := (forall (vars (?v0 S3)) #20)
+#93 := (iff #21 #92)
+#90 := (iff #20 #89)
+#87 := (iff #19 #85)
+#88 := [rewrite]: #87
+#91 := [monotonicity #88]: #90
+#94 := [quant-intro #91]: #93
+#84 := [asserted]: #21
+#97 := [mp #84 #94]: #92
+#147 := [mp~ #97 #160]: #92
+#675 := [mp #147 #674]: #670
+#664 := (not #343)
+#645 := (not #670)
+#651 := (or #645 #664)
+#289 := [quant-inst]: #651
+[unit-resolution #289 #675 #294]: false
+unsat
+156b5bbccd88bf00c5d19d456c8d5c95867a3e79 128 0
+#2 := false
+decl f8 :: (-> S2 S3 S1)
+decl f6 :: S3
+#10 := f6
+decl f5 :: S2
+#9 := f5
+#238 := (f8 f5 f6)
+decl f1 :: S1
+#4 := f1
+#325 := (= f1 #238)
+#650 := (not #325)
+decl f4 :: S2
+#8 := f4
+#239 := (f8 f4 f6)
+#326 := (= f1 #239)
+#318 := (or #325 #326)
+#303 := (not #318)
+decl f3 :: (-> S2 S2 S3 S1)
+#11 := (f3 f4 f5 f6)
+#63 := (= f1 #11)
+#258 := (iff #63 #318)
+#19 := (:var 0 S3)
+#24 := (:var 1 S2)
+#23 := (:var 2 S2)
+#25 := (f3 #23 #24 #19)
+#668 := (pattern #25)
+#29 := (f8 #24 #19)
+#96 := (= f1 #29)
+#27 := (f8 #23 #19)
+#93 := (= f1 #27)
+#99 := (or #93 #96)
+#89 := (= f1 #25)
+#102 := (iff #89 #99)
+#669 := (forall (vars (?v0 S2) (?v1 S2) (?v2 S3)) (:pat #668) #102)
+#105 := (forall (vars (?v0 S2) (?v1 S2) (?v2 S3)) #102)
+#672 := (iff #105 #669)
+#670 := (iff #102 #102)
+#671 := [refl]: #670
+#673 := [quant-intro #671]: #672
+#136 := (~ #105 #105)
+#146 := (~ #102 #102)
+#147 := [refl]: #146
+#137 := [nnf-pos #147]: #136
+#30 := (= #29 f1)
+#28 := (= #27 f1)
+#31 := (or #28 #30)
+#26 := (= #25 f1)
+#32 := (iff #26 #31)
+#33 := (forall (vars (?v0 S2) (?v1 S2) (?v2 S3)) #32)
+#106 := (iff #33 #105)
+#103 := (iff #32 #102)
+#100 := (iff #31 #99)
+#97 := (iff #30 #96)
+#98 := [rewrite]: #97
+#94 := (iff #28 #93)
+#95 := [rewrite]: #94
+#101 := [monotonicity #95 #98]: #100
+#91 := (iff #26 #89)
+#92 := [rewrite]: #91
+#104 := [monotonicity #92 #101]: #103
+#107 := [quant-intro #104]: #106
+#88 := [asserted]: #33
+#110 := [mp #88 #107]: #105
+#148 := [mp~ #110 #137]: #105
+#674 := [mp #148 #673]: #669
+#332 := (not #669)
+#311 := (or #332 #258)
+#240 := (or #326 #325)
+#327 := (iff #63 #240)
+#646 := (or #332 #327)
+#305 := (iff #646 #311)
+#642 := (iff #311 #311)
+#316 := [rewrite]: #642
+#331 := (iff #327 #258)
+#329 := (iff #240 #318)
+#330 := [rewrite]: #329
+#328 := [monotonicity #330]: #331
+#435 := [monotonicity #328]: #305
+#317 := [trans #435 #316]: #305
+#648 := [quant-inst]: #646
+#649 := [mp #648 #317]: #311
+#632 := [unit-resolution #649 #674]: #258
+#304 := (not #258)
+#633 := (or #304 #303)
+#66 := (not #63)
+#12 := (= #11 f1)
+#13 := (not #12)
+#67 := (iff #13 #66)
+#64 := (iff #12 #63)
+#65 := [rewrite]: #64
+#68 := [monotonicity #65]: #67
+#62 := [asserted]: #13
+#71 := [mp #62 #68]: #66
+#645 := (or #304 #63 #303)
+#288 := [def-axiom]: #645
+#636 := [unit-resolution #288 #71]: #633
+#274 := [unit-resolution #636 #632]: #303
+#651 := (or #318 #650)
+#652 := [def-axiom]: #651
+#637 := [unit-resolution #652 #274]: #650
+#20 := (f8 f5 #19)
+#661 := (pattern #20)
+#81 := (= f1 #20)
+#662 := (forall (vars (?v0 S3)) (:pat #661) #81)
+#85 := (forall (vars (?v0 S3)) #81)
+#665 := (iff #85 #662)
+#663 := (iff #81 #81)
+#664 := [refl]: #663
+#666 := [quant-intro #664]: #665
+#134 := (~ #85 #85)
+#133 := (~ #81 #81)
+#131 := [refl]: #133
+#135 := [nnf-pos #131]: #134
+#21 := (= #20 f1)
+#22 := (forall (vars (?v0 S3)) #21)
+#86 := (iff #22 #85)
+#83 := (iff #21 #81)
+#84 := [rewrite]: #83
+#87 := [quant-intro #84]: #86
+#80 := [asserted]: #22
+#90 := [mp #80 #87]: #85
+#128 := [mp~ #90 #135]: #85
+#667 := [mp #128 #666]: #662
+#634 := (not #662)
+#635 := (or #634 #325)
+#630 := [quant-inst]: #635
+[unit-resolution #630 #667 #637]: false
+unsat
+e9501ad699b29b1a0c65a378dbd0d68cdbadce66 146 0
+#2 := false
+decl f3 :: (-> S2 S2 S3 S1)
+decl f6 :: S3
+#10 := f6
+decl f4 :: S2
+#8 := f4
+decl f5 :: S2
+#9 := f5
+#13 := (f3 f5 f4 f6)
+decl f1 :: S1
+#4 := f1
+#70 := (= f1 #13)
+#343 := (not #70)
+#11 := (f3 f4 f5 f6)
+#67 := (= f1 #11)
+#79 := (not #67)
+#640 := [hypothesis]: #79
+#342 := (or #70 #67)
+#80 := (iff #70 #79)
+#14 := (= #13 f1)
+#12 := (= #11 f1)
+#15 := (iff #12 #14)
+#16 := (not #15)
+#83 := (iff #16 #80)
+#73 := (iff #67 #70)
+#76 := (not #73)
+#81 := (iff #76 #80)
+#82 := [rewrite]: #81
+#77 := (iff #16 #76)
+#74 := (iff #15 #73)
+#71 := (iff #14 #70)
+#72 := [rewrite]: #71
+#68 := (iff #12 #67)
+#69 := [rewrite]: #68
+#75 := [monotonicity #69 #72]: #74
+#78 := [monotonicity #75]: #77
+#84 := [trans #78 #82]: #83
+#66 := [asserted]: #16
+#87 := [mp #66 #84]: #80
+#254 := (not #80)
+#341 := (or #70 #67 #254)
+#255 := [def-axiom]: #341
+#256 := [unit-resolution #255 #87]: #342
+#362 := [unit-resolution #256 #640]: #70
+decl f9 :: (-> S2 S3 S1)
+#347 := (f9 f4 f6)
+#344 := (= f1 #347)
+#348 := (f9 f5 f6)
+#327 := (= f1 #348)
+#662 := (or #327 #344)
+#659 := (not #662)
+#637 := (or #67 #659)
+#649 := (iff #67 #662)
+#28 := (:var 0 S3)
+#27 := (:var 1 S2)
+#26 := (:var 2 S2)
+#29 := (f3 #26 #27 #28)
+#684 := (pattern #29)
+#33 := (f9 #27 #28)
+#112 := (= f1 #33)
+#31 := (f9 #26 #28)
+#109 := (= f1 #31)
+#115 := (or #109 #112)
+#105 := (= f1 #29)
+#118 := (iff #105 #115)
+#685 := (forall (vars (?v0 S2) (?v1 S2) (?v2 S3)) (:pat #684) #118)
+#121 := (forall (vars (?v0 S2) (?v1 S2) (?v2 S3)) #118)
+#688 := (iff #121 #685)
+#686 := (iff #118 #118)
+#687 := [refl]: #686
+#689 := [quant-intro #687]: #688
+#152 := (~ #121 #121)
+#162 := (~ #118 #118)
+#163 := [refl]: #162
+#153 := [nnf-pos #163]: #152
+#34 := (= #33 f1)
+#32 := (= #31 f1)
+#35 := (or #32 #34)
+#30 := (= #29 f1)
+#36 := (iff #30 #35)
+#37 := (forall (vars (?v0 S2) (?v1 S2) (?v2 S3)) #36)
+#122 := (iff #37 #121)
+#119 := (iff #36 #118)
+#116 := (iff #35 #115)
+#113 := (iff #34 #112)
+#114 := [rewrite]: #113
+#110 := (iff #32 #109)
+#111 := [rewrite]: #110
+#117 := [monotonicity #111 #114]: #116
+#107 := (iff #30 #105)
+#108 := [rewrite]: #107
+#120 := [monotonicity #108 #117]: #119
+#123 := [quant-intro #120]: #122
+#104 := [asserted]: #37
+#126 := [mp #104 #123]: #121
+#164 := [mp~ #126 #153]: #121
+#690 := [mp #164 #689]: #685
+#658 := (not #685)
+#646 := (or #658 #649)
+#321 := (or #344 #327)
+#451 := (iff #67 #321)
+#652 := (or #658 #451)
+#653 := (iff #652 #646)
+#295 := (iff #646 #646)
+#296 := [rewrite]: #295
+#650 := (iff #451 #649)
+#647 := (iff #321 #662)
+#648 := [rewrite]: #647
+#651 := [monotonicity #648]: #650
+#655 := [monotonicity #651]: #653
+#656 := [trans #655 #296]: #653
+#290 := [quant-inst]: #652
+#654 := [mp #290 #656]: #646
+#363 := [unit-resolution #654 #690]: #649
+#657 := (not #649)
+#643 := (or #657 #67 #659)
+#644 := [def-axiom]: #643
+#641 := [unit-resolution #644 #363]: #637
+#638 := [unit-resolution #641 #640]: #659
+#352 := (or #343 #662)
+#664 := (iff #70 #662)
+#332 := (or #658 #664)
+#333 := [quant-inst]: #332
+#642 := [unit-resolution #333 #690]: #664
+#660 := (not #664)
+#304 := (or #660 #343 #662)
+#645 := [def-axiom]: #304
+#353 := [unit-resolution #645 #642]: #352
+#354 := [unit-resolution #353 #638 #362]: false
+#355 := [lemma #354]: #67
+#346 := (or #343 #79)
+#334 := (or #343 #79 #254)
+#345 := [def-axiom]: #334
+#274 := [unit-resolution #345 #87]: #346
+#633 := [unit-resolution #274 #355]: #343
+#634 := (or #79 #662)
+#366 := (or #657 #79 #662)
+#367 := [def-axiom]: #366
+#349 := [unit-resolution #367 #363]: #634
+#631 := [unit-resolution #349 #355]: #662
+#635 := (or #70 #659)
+#320 := (or #660 #70 #659)
+#661 := [def-axiom]: #320
+#632 := [unit-resolution #661 #642]: #635
+[unit-resolution #632 #631 #633]: false
+unsat
+60cdff9edbb9caaee078a8376311922be886cc87 121 0
+#2 := false
+decl f3 :: (-> S2 S2 S3 S1)
+decl f5 :: S3
+#9 := f5
+decl f4 :: S2
+#8 := f4
+#10 := (f3 f4 f4 f5)
+decl f1 :: S1
+#4 := f1
+#66 := (= f1 #10)
+#78 := (not #66)
+#644 := [hypothesis]: #78
+decl f6 :: (-> S2 S3 S1)
+#12 := (f6 f4 f5)
+#69 := (= f1 #12)
+#341 := (or #69 #66)
+#79 := (iff #69 #78)
+#13 := (= #12 f1)
+#11 := (= #10 f1)
+#14 := (iff #11 #13)
+#15 := (not #14)
+#82 := (iff #15 #79)
+#72 := (iff #66 #69)
+#75 := (not #72)
+#80 := (iff #75 #79)
+#81 := [rewrite]: #80
+#76 := (iff #15 #75)
+#73 := (iff #14 #72)
+#70 := (iff #13 #69)
+#71 := [rewrite]: #70
+#67 := (iff #11 #66)
+#68 := [rewrite]: #67
+#74 := [monotonicity #68 #71]: #73
+#77 := [monotonicity #74]: #76
+#83 := [trans #77 #81]: #82
+#65 := [asserted]: #15
+#86 := [mp #65 #83]: #79
+#253 := (not #79)
+#340 := (or #69 #66 #253)
+#254 := [def-axiom]: #340
+#255 := [unit-resolution #254 #86]: #341
+#307 := [unit-resolution #255 #644]: #69
+#342 := (not #69)
+#309 := (or #66 #342)
+#27 := (:var 0 S3)
+#26 := (:var 1 S2)
+#25 := (:var 2 S2)
+#28 := (f3 #25 #26 #27)
+#683 := (pattern #28)
+#32 := (f6 #26 #27)
+#111 := (= f1 #32)
+#30 := (f6 #25 #27)
+#108 := (= f1 #30)
+#114 := (or #108 #111)
+#104 := (= f1 #28)
+#117 := (iff #104 #114)
+#684 := (forall (vars (?v0 S2) (?v1 S2) (?v2 S3)) (:pat #683) #117)
+#120 := (forall (vars (?v0 S2) (?v1 S2) (?v2 S3)) #117)
+#687 := (iff #120 #684)
+#685 := (iff #117 #117)
+#686 := [refl]: #685
+#688 := [quant-intro #686]: #687
+#151 := (~ #120 #120)
+#161 := (~ #117 #117)
+#162 := [refl]: #161
+#152 := [nnf-pos #162]: #151
+#33 := (= #32 f1)
+#31 := (= #30 f1)
+#34 := (or #31 #33)
+#29 := (= #28 f1)
+#35 := (iff #29 #34)
+#36 := (forall (vars (?v0 S2) (?v1 S2) (?v2 S3)) #35)
+#121 := (iff #36 #120)
+#118 := (iff #35 #117)
+#115 := (iff #34 #114)
+#112 := (iff #33 #111)
+#113 := [rewrite]: #112
+#109 := (iff #31 #108)
+#110 := [rewrite]: #109
+#116 := [monotonicity #110 #113]: #115
+#106 := (iff #29 #104)
+#107 := [rewrite]: #106
+#119 := [monotonicity #107 #116]: #118
+#122 := [quant-intro #119]: #121
+#103 := [asserted]: #36
+#125 := [mp #103 #122]: #120
+#163 := [mp~ #125 #152]: #120
+#689 := [mp #163 #688]: #684
+#320 := (not #684)
+#450 := (or #320 #72)
+#346 := (or #69 #69)
+#343 := (iff #66 #346)
+#657 := (or #320 #343)
+#332 := (iff #657 #450)
+#665 := (iff #450 #450)
+#666 := [rewrite]: #665
+#661 := (iff #343 #72)
+#347 := (iff #346 #69)
+#326 := [rewrite]: #347
+#663 := [monotonicity #326]: #661
+#664 := [monotonicity #663]: #332
+#667 := [trans #664 #666]: #332
+#331 := [quant-inst]: #657
+#662 := [mp #331 #667]: #450
+#308 := [unit-resolution #662 #689]: #72
+#668 := (or #75 #66 #342)
+#658 := [def-axiom]: #668
+#310 := [unit-resolution #658 #308]: #309
+#646 := [unit-resolution #310 #307 #644]: false
+#647 := [lemma #646]: #66
+#345 := (or #342 #78)
+#333 := (or #342 #78 #253)
+#344 := [def-axiom]: #333
+#273 := [unit-resolution #344 #86]: #345
+#648 := [unit-resolution #273 #647]: #342
+#649 := (or #78 #69)
+#318 := (or #75 #78 #69)
+#323 := [def-axiom]: #318
+#650 := [unit-resolution #323 #308]: #649
+[unit-resolution #650 #648 #647]: false
+unsat
+e7ec03d0541acce6c328f68f87047aa506800ef8 258 0
+#2 := false
+decl f3 :: (-> S2 S3 S1)
+decl f8 :: S3
+#13 := f8
+decl f6 :: S2
+#9 := f6
+#624 := (f3 f6 f8)
+decl f1 :: S1
+#4 := f1
+#337 := (= f1 #624)
+decl f7 :: S2
+#10 := f7
+#335 := (f3 f7 f8)
+#332 := (= f1 #335)
+#622 := (or #332 #337)
+decl f4 :: (-> S2 S2 S2)
+#11 := (f4 f6 f7)
+#309 := (f3 #11 f8)
+#441 := (= f1 #309)
+#616 := (iff #441 #622)
+#582 := (not #616)
+#580 := [hypothesis]: #582
+#34 := (:var 0 S3)
+#32 := (:var 1 S2)
+#31 := (:var 2 S2)
+#33 := (f4 #31 #32)
+#35 := (f3 #33 #34)
+#674 := (pattern #35)
+#39 := (f3 #32 #34)
+#118 := (= f1 #39)
+#37 := (f3 #31 #34)
+#115 := (= f1 #37)
+#121 := (or #115 #118)
+#111 := (= f1 #35)
+#124 := (iff #111 #121)
+#675 := (forall (vars (?v0 S2) (?v1 S2) (?v2 S3)) (:pat #674) #124)
+#127 := (forall (vars (?v0 S2) (?v1 S2) (?v2 S3)) #124)
+#678 := (iff #127 #675)
+#676 := (iff #124 #124)
+#677 := [refl]: #676
+#679 := [quant-intro #677]: #678
+#158 := (~ #127 #127)
+#168 := (~ #124 #124)
+#169 := [refl]: #168
+#159 := [nnf-pos #169]: #158
+#40 := (= #39 f1)
+#38 := (= #37 f1)
+#41 := (or #38 #40)
+#36 := (= #35 f1)
+#42 := (iff #36 #41)
+#43 := (forall (vars (?v0 S2) (?v1 S2) (?v2 S3)) #42)
+#128 := (iff #43 #127)
+#125 := (iff #42 #124)
+#122 := (iff #41 #121)
+#119 := (iff #40 #118)
+#120 := [rewrite]: #119
+#116 := (iff #38 #115)
+#117 := [rewrite]: #116
+#123 := [monotonicity #117 #120]: #122
+#113 := (iff #36 #111)
+#114 := [rewrite]: #113
+#126 := [monotonicity #114 #123]: #125
+#129 := [quant-intro #126]: #128
+#110 := [asserted]: #43
+#132 := [mp #110 #129]: #127
+#170 := [mp~ #132 #159]: #127
+#680 := [mp #170 #679]: #675
+#648 := (not #675)
+#598 := (or #648 #616)
+#621 := (or #337 #332)
+#625 := (iff #441 #621)
+#618 := (or #648 #625)
+#613 := (iff #618 #598)
+#620 := (iff #598 #598)
+#461 := [rewrite]: #620
+#617 := (iff #625 #616)
+#626 := (iff #621 #622)
+#615 := [rewrite]: #626
+#612 := [monotonicity #615]: #617
+#614 := [monotonicity #612]: #613
+#462 := [trans #614 #461]: #613
+#619 := [quant-inst]: #618
+#463 := [mp #619 #462]: #598
+#574 := [unit-resolution #463 #680 #580]: false
+#581 := [lemma #574]: #616
+#594 := (not #622)
+#658 := (not #332)
+decl f5 :: S2
+#8 := f5
+#16 := (f4 f5 f6)
+#336 := (f3 #16 f8)
+#315 := (= f1 #336)
+#652 := (or #315 #332)
+#649 := (not #652)
+#17 := (f4 #16 f7)
+#18 := (f3 #17 f8)
+#76 := (= f1 #18)
+#331 := (not #76)
+#12 := (f4 f5 #11)
+#14 := (f3 #12 f8)
+#73 := (= f1 #14)
+#637 := (f3 f5 f8)
+#638 := (= f1 #637)
+#484 := (or #337 #638)
+#592 := (iff #315 #484)
+#584 := (not #592)
+#577 := [hypothesis]: #584
+#590 := (or #648 #592)
+#601 := (or #638 #337)
+#483 := (iff #315 #601)
+#593 := (or #648 #483)
+#493 := (iff #593 #590)
+#496 := (iff #590 #590)
+#489 := [rewrite]: #496
+#494 := (iff #483 #592)
+#485 := (iff #601 #484)
+#444 := [rewrite]: #485
+#589 := [monotonicity #444]: #494
+#495 := [monotonicity #589]: #493
+#497 := [trans #495 #489]: #493
+#478 := [quant-inst]: #593
+#498 := [mp #478 #497]: #590
+#578 := [unit-resolution #498 #680 #577]: false
+#579 := [lemma #578]: #592
+#85 := (not #73)
+#565 := [hypothesis]: #85
+#330 := (or #76 #73)
+#86 := (iff #76 #85)
+#19 := (= #18 f1)
+#15 := (= #14 f1)
+#20 := (iff #15 #19)
+#21 := (not #20)
+#89 := (iff #21 #86)
+#79 := (iff #73 #76)
+#82 := (not #79)
+#87 := (iff #82 #86)
+#88 := [rewrite]: #87
+#83 := (iff #21 #82)
+#80 := (iff #20 #79)
+#77 := (iff #19 #76)
+#78 := [rewrite]: #77
+#74 := (iff #15 #73)
+#75 := [rewrite]: #74
+#81 := [monotonicity #75 #78]: #80
+#84 := [monotonicity #81]: #83
+#90 := [trans #84 #88]: #89
+#72 := [asserted]: #21
+#93 := [mp #72 #90]: #86
+#242 := (not #86)
+#329 := (or #76 #73 #242)
+#243 := [def-axiom]: #329
+#244 := [unit-resolution #243 #93]: #330
+#566 := [unit-resolution #244 #565]: #76
+#569 := (or #331 #652)
+#654 := (iff #76 #652)
+#320 := (or #648 #654)
+#321 := [quant-inst]: #320
+#568 := [unit-resolution #321 #680]: #654
+#650 := (not #654)
+#292 := (or #650 #331 #652)
+#635 := [def-axiom]: #292
+#570 := [unit-resolution #635 #568]: #569
+#571 := [unit-resolution #570 #566]: #652
+#357 := (not #441)
+#641 := (or #441 #638)
+#630 := (not #641)
+#572 := (or #73 #630)
+#278 := (iff #73 #641)
+#283 := (or #648 #278)
+#639 := (or #638 #441)
+#640 := (iff #73 #639)
+#284 := (or #648 #640)
+#644 := (iff #284 #283)
+#633 := (iff #283 #283)
+#634 := [rewrite]: #633
+#643 := (iff #640 #278)
+#636 := (iff #639 #641)
+#642 := [rewrite]: #636
+#645 := [monotonicity #642]: #643
+#647 := [monotonicity #645]: #644
+#340 := [trans #647 #634]: #644
+#646 := [quant-inst]: #284
+#356 := [mp #646 #340]: #283
+#567 := [unit-resolution #356 #680]: #278
+#627 := (not #278)
+#631 := (or #627 #73 #630)
+#628 := [def-axiom]: #631
+#558 := [unit-resolution #628 #567]: #572
+#559 := [unit-resolution #558 #565]: #630
+#358 := (or #641 #357)
+#344 := [def-axiom]: #358
+#561 := [unit-resolution #344 #559]: #357
+#576 := (or #582 #441 #594)
+#573 := [def-axiom]: #576
+#562 := [unit-resolution #573 #561 #581]: #594
+#605 := (or #622 #658)
+#499 := [def-axiom]: #605
+#563 := [unit-resolution #499 #562]: #658
+#307 := (or #649 #315 #332)
+#312 := [def-axiom]: #307
+#560 := [unit-resolution #312 #563 #571]: #315
+#609 := (not #484)
+#359 := (not #638)
+#250 := (or #641 #359)
+#629 := [def-axiom]: #250
+#564 := [unit-resolution #629 #559]: #359
+#606 := (not #337)
+#500 := (or #622 #606)
+#501 := [def-axiom]: #500
+#544 := [unit-resolution #501 #562]: #606
+#610 := (or #609 #337 #638)
+#604 := [def-axiom]: #610
+#545 := [unit-resolution #604 #544 #564]: #609
+#655 := (not #315)
+#442 := (or #584 #655 #484)
+#443 := [def-axiom]: #442
+#547 := [unit-resolution #443 #545 #560 #579]: false
+#548 := [lemma #547]: #73
+#334 := (or #331 #85)
+#322 := (or #331 #85 #242)
+#333 := [def-axiom]: #322
+#262 := [unit-resolution #333 #93]: #334
+#549 := [unit-resolution #262 #548]: #331
+#550 := (or #76 #649)
+#308 := (or #650 #76 #649)
+#651 := [def-axiom]: #308
+#551 := [unit-resolution #651 #568]: #550
+#552 := [unit-resolution #551 #549]: #649
+#653 := (or #652 #658)
+#659 := [def-axiom]: #653
+#553 := [unit-resolution #659 #552]: #658
+#656 := (or #652 #655)
+#657 := [def-axiom]: #656
+#554 := [unit-resolution #657 #552]: #655
+#611 := (or #584 #315 #609)
+#440 := [def-axiom]: #611
+#555 := [unit-resolution #440 #554 #579]: #609
+#607 := (or #484 #606)
+#608 := [def-axiom]: #607
+#556 := [unit-resolution #608 #555]: #606
+#591 := (or #594 #332 #337)
+#595 := [def-axiom]: #591
+#546 := [unit-resolution #595 #556 #553]: #594
+#557 := (or #85 #641)
+#632 := (or #627 #85 #641)
+#341 := [def-axiom]: #632
+#535 := [unit-resolution #341 #567]: #557
+#536 := [unit-resolution #535 #548]: #641
+#602 := (or #484 #359)
+#603 := [def-axiom]: #602
+#538 := [unit-resolution #603 #555]: #359
+#352 := (or #630 #441 #638)
+#353 := [def-axiom]: #352
+#539 := [unit-resolution #353 #538 #536]: #441
+#575 := (or #582 #357 #622)
+#585 := [def-axiom]: #575
+[unit-resolution #585 #539 #546 #581]: false
+unsat
+0ff3bde207876a1e2bbf9f523fbb88a3af58b75b 153 0
+#2 := false
+decl f7 :: (-> S2 S3 S1)
+decl f6 :: S3
+#10 := f6
+decl f5 :: S2
+#9 := f5
+#15 := (f7 f5 f6)
+decl f1 :: S1
+#4 := f1
+#76 := (= f1 #15)
+#178 := (not #76)
+decl f4 :: S2
+#8 := f4
+#13 := (f7 f4 f6)
+#73 := (= f1 #13)
+#177 := (not #73)
+#165 := (or #177 #178)
+#166 := (not #165)
+#350 := [hypothesis]: #166
+decl f3 :: (-> S2 S2 S3 S1)
+#11 := (f3 f4 f5 f6)
+#70 := (= f1 #11)
+#88 := (not #70)
+#356 := (or #88 #165)
+#189 := (iff #70 #165)
+#79 := (and #73 #76)
+#89 := (iff #79 #88)
+#192 := (iff #89 #189)
+#184 := (iff #165 #70)
+#190 := (iff #184 #189)
+#191 := [rewrite]: #190
+#187 := (iff #89 #184)
+#181 := (iff #166 #88)
+#185 := (iff #181 #184)
+#186 := [rewrite]: #185
+#182 := (iff #89 #181)
+#179 := (iff #79 #166)
+#180 := [rewrite]: #179
+#183 := [monotonicity #180]: #182
+#188 := [trans #183 #186]: #187
+#193 := [trans #188 #191]: #192
+#16 := (= #15 f1)
+#14 := (= #13 f1)
+#17 := (and #14 #16)
+#12 := (= #11 f1)
+#18 := (iff #12 #17)
+#19 := (not #18)
+#92 := (iff #19 #89)
+#82 := (iff #70 #79)
+#85 := (not #82)
+#90 := (iff #85 #89)
+#91 := [rewrite]: #90
+#86 := (iff #19 #85)
+#83 := (iff #18 #82)
+#80 := (iff #17 #79)
+#77 := (iff #16 #76)
+#78 := [rewrite]: #77
+#74 := (iff #14 #73)
+#75 := [rewrite]: #74
+#81 := [monotonicity #75 #78]: #80
+#71 := (iff #12 #70)
+#72 := [rewrite]: #71
+#84 := [monotonicity #72 #81]: #83
+#87 := [monotonicity #84]: #86
+#93 := [trans #87 #91]: #92
+#69 := [asserted]: #19
+#96 := [mp #69 #93]: #89
+#194 := [mp #96 #193]: #189
+#363 := (not #189)
+#373 := (or #88 #165 #363)
+#377 := [def-axiom]: #373
+#691 := [unit-resolution #377 #194]: #356
+#480 := [unit-resolution #691 #350]: #88
+#349 := (or #70 #165)
+#693 := (iff #70 #166)
+#43 := (:var 0 S3)
+#42 := (:var 1 S2)
+#41 := (:var 2 S2)
+#44 := (f3 #41 #42 #43)
+#720 := (pattern #44)
+#48 := (f7 #42 #43)
+#141 := (= f1 #48)
+#196 := (not #141)
+#46 := (f7 #41 #43)
+#138 := (= f1 #46)
+#195 := (not #138)
+#197 := (or #195 #196)
+#198 := (not #197)
+#134 := (= f1 #44)
+#201 := (iff #134 #198)
+#721 := (forall (vars (?v0 S2) (?v1 S2) (?v2 S3)) (:pat #720) #201)
+#204 := (forall (vars (?v0 S2) (?v1 S2) (?v2 S3)) #201)
+#724 := (iff #204 #721)
+#722 := (iff #201 #201)
+#723 := [refl]: #722
+#725 := [quant-intro #723]: #724
+#144 := (and #138 #141)
+#147 := (iff #134 #144)
+#150 := (forall (vars (?v0 S2) (?v1 S2) (?v2 S3)) #147)
+#205 := (iff #150 #204)
+#202 := (iff #147 #201)
+#199 := (iff #144 #198)
+#200 := [rewrite]: #199
+#203 := [monotonicity #200]: #202
+#206 := [quant-intro #203]: #205
+#163 := (~ #150 #150)
+#174 := (~ #147 #147)
+#175 := [refl]: #174
+#164 := [nnf-pos #175]: #163
+#49 := (= #48 f1)
+#47 := (= #46 f1)
+#50 := (and #47 #49)
+#45 := (= #44 f1)
+#51 := (iff #45 #50)
+#52 := (forall (vars (?v0 S2) (?v1 S2) (?v2 S3)) #51)
+#151 := (iff #52 #150)
+#148 := (iff #51 #147)
+#145 := (iff #50 #144)
+#142 := (iff #49 #141)
+#143 := [rewrite]: #142
+#139 := (iff #47 #138)
+#140 := [rewrite]: #139
+#146 := [monotonicity #140 #143]: #145
+#136 := (iff #45 #134)
+#137 := [rewrite]: #136
+#149 := [monotonicity #137 #146]: #148
+#152 := [quant-intro #149]: #151
+#133 := [asserted]: #52
+#155 := [mp #133 #152]: #150
+#176 := [mp~ #155 #164]: #150
+#207 := [mp #176 #206]: #204
+#726 := [mp #207 #725]: #721
+#687 := (not #721)
+#361 := (or #687 #693)
+#362 := [quant-inst]: #361
+#689 := [unit-resolution #362 #726]: #693
+#694 := (not #693)
+#695 := (or #694 #70 #165)
+#696 := [def-axiom]: #695
+#690 := [unit-resolution #696 #689]: #349
+#333 := [unit-resolution #690 #480 #350]: false
+#674 := [lemma #333]: #165
+#303 := (or #70 #166)
+#374 := (or #70 #166 #363)
+#375 := [def-axiom]: #374
+#376 := [unit-resolution #375 #194]: #303
+#337 := [unit-resolution #376 #674]: #70
+#338 := (or #88 #166)
+#697 := (or #694 #88 #166)
+#692 := [def-axiom]: #697
+#339 := [unit-resolution #692 #689]: #338
+[unit-resolution #339 #337 #674]: false
+unsat
+af9d88d34e35638de5cad45a5fcb0943b421dc7f 141 0
+#2 := false
+decl f7 :: (-> S2 S3 S1)
+decl f6 :: S3
+#10 := f6
+decl f5 :: S2
+#9 := f5
+#246 := (f7 f5 f6)
+decl f1 :: S1
+#4 := f1
+#333 := (= f1 #246)
+#247 := (not #333)
+decl f4 :: S2
+#8 := f4
+#334 := (f7 f4 f6)
+#248 := (= f1 #334)
+#335 := (not #248)
+#326 := (or #335 #247)
+#337 := (not #326)
+decl f3 :: (-> S2 S2 S3 S1)
+#11 := (f3 f4 f5 f6)
+#64 := (= f1 #11)
+#338 := (iff #64 #337)
+#15 := (:var 0 S3)
+#37 := (:var 1 S2)
+#36 := (:var 2 S2)
+#38 := (f3 #36 #37 #15)
+#683 := (pattern #38)
+#42 := (f7 #37 #15)
+#124 := (= f1 #42)
+#161 := (not #124)
+#40 := (f7 #36 #15)
+#121 := (= f1 #40)
+#160 := (not #121)
+#148 := (or #160 #161)
+#149 := (not #148)
+#117 := (= f1 #38)
+#164 := (iff #117 #149)
+#684 := (forall (vars (?v0 S2) (?v1 S2) (?v2 S3)) (:pat #683) #164)
+#167 := (forall (vars (?v0 S2) (?v1 S2) (?v2 S3)) #164)
+#687 := (iff #167 #684)
+#685 := (iff #164 #164)
+#686 := [refl]: #685
+#688 := [quant-intro #686]: #687
+#127 := (and #121 #124)
+#130 := (iff #117 #127)
+#133 := (forall (vars (?v0 S2) (?v1 S2) (?v2 S3)) #130)
+#168 := (iff #133 #167)
+#165 := (iff #130 #164)
+#162 := (iff #127 #149)
+#163 := [rewrite]: #162
+#166 := [monotonicity #163]: #165
+#169 := [quant-intro #166]: #168
+#146 := (~ #133 #133)
+#157 := (~ #130 #130)
+#158 := [refl]: #157
+#147 := [nnf-pos #158]: #146
+#43 := (= #42 f1)
+#41 := (= #40 f1)
+#44 := (and #41 #43)
+#39 := (= #38 f1)
+#45 := (iff #39 #44)
+#46 := (forall (vars (?v0 S2) (?v1 S2) (?v2 S3)) #45)
+#134 := (iff #46 #133)
+#131 := (iff #45 #130)
+#128 := (iff #44 #127)
+#125 := (iff #43 #124)
+#126 := [rewrite]: #125
+#122 := (iff #41 #121)
+#123 := [rewrite]: #122
+#129 := [monotonicity #123 #126]: #128
+#119 := (iff #39 #117)
+#120 := [rewrite]: #119
+#132 := [monotonicity #120 #129]: #131
+#135 := [quant-intro #132]: #134
+#116 := [asserted]: #46
+#138 := [mp #116 #135]: #133
+#159 := [mp~ #138 #147]: #133
+#170 := [mp #159 #169]: #167
+#689 := [mp #170 #688]: #684
+#336 := (not #684)
+#340 := (or #336 #338)
+#319 := [quant-inst]: #340
+#266 := [unit-resolution #319 #689]: #338
+#325 := (not #338)
+#339 := (or #325 #337)
+#12 := (= #11 f1)
+#13 := (not #12)
+#14 := (not #13)
+#75 := (iff #14 #64)
+#67 := (not #64)
+#70 := (not #67)
+#73 := (iff #70 #64)
+#74 := [rewrite]: #73
+#71 := (iff #14 #70)
+#68 := (iff #13 #67)
+#65 := (iff #12 #64)
+#66 := [rewrite]: #65
+#69 := [monotonicity #66]: #68
+#72 := [monotonicity #69]: #71
+#76 := [trans #72 #74]: #75
+#63 := [asserted]: #14
+#79 := [mp #63 #76]: #64
+#659 := (or #325 #67 #337)
+#660 := [def-axiom]: #659
+#653 := [unit-resolution #660 #79]: #339
+#296 := [unit-resolution #653 #266]: #337
+#313 := (or #326 #333)
+#443 := [def-axiom]: #313
+#637 := [unit-resolution #443 #296]: #333
+#16 := (f7 f5 #15)
+#662 := (pattern #16)
+#78 := (= f1 #16)
+#82 := (not #78)
+#663 := (forall (vars (?v0 S3)) (:pat #662) #82)
+#85 := (forall (vars (?v0 S3)) #82)
+#666 := (iff #85 #663)
+#664 := (iff #82 #82)
+#665 := [refl]: #664
+#667 := [quant-intro #665]: #666
+#152 := (~ #85 #85)
+#150 := (~ #82 #82)
+#151 := [refl]: #150
+#153 := [nnf-pos #151]: #152
+#17 := (= #16 f1)
+#18 := (not #17)
+#19 := (forall (vars (?v0 S3)) #18)
+#86 := (iff #19 #85)
+#83 := (iff #18 #82)
+#80 := (iff #17 #78)
+#81 := [rewrite]: #80
+#84 := [monotonicity #81]: #83
+#87 := [quant-intro #84]: #86
+#77 := [asserted]: #19
+#90 := [mp #77 #87]: #85
+#140 := [mp~ #90 #153]: #85
+#668 := [mp #140 #667]: #663
+#316 := (not #663)
+#652 := (or #316 #247)
+#312 := [quant-inst]: #652
+[unit-resolution #312 #668 #637]: false
+unsat
+1fe992aa332936da32d8835a880128a83f76f965 165 0
+#2 := false
+decl f7 :: (-> S2 S3 S1)
+decl f6 :: S3
+#10 := f6
+decl f4 :: S2
+#8 := f4
+#13 := (f7 f4 f6)
+decl f1 :: S1
+#4 := f1
+#69 := (= f1 #13)
+#342 := (not #69)
+decl f3 :: (-> S2 S2 S3 S1)
+decl f5 :: S2
+#9 := f5
+#11 := (f3 f4 f5 f6)
+#66 := (= f1 #11)
+#346 := (f7 f5 f6)
+#343 := (= f1 #346)
+#347 := (not #343)
+#320 := [hypothesis]: #347
+#22 := (:var 0 S3)
+#23 := (f7 f5 #22)
+#676 := (pattern #23)
+#96 := (= f1 #23)
+#677 := (forall (vars (?v0 S3)) (:pat #676) #96)
+#100 := (forall (vars (?v0 S3)) #96)
+#680 := (iff #100 #677)
+#678 := (iff #96 #96)
+#679 := [refl]: #678
+#681 := [quant-intro #679]: #680
+#149 := (~ #100 #100)
+#148 := (~ #96 #96)
+#146 := [refl]: #148
+#150 := [nnf-pos #146]: #149
+#24 := (= #23 f1)
+#25 := (forall (vars (?v0 S3)) #24)
+#101 := (iff #25 #100)
+#98 := (iff #24 #96)
+#99 := [rewrite]: #98
+#102 := [quant-intro #99]: #101
+#95 := [asserted]: #25
+#105 := [mp #95 #102]: #100
+#143 := [mp~ #105 #150]: #100
+#682 := [mp #143 #681]: #677
+#308 := (not #677)
+#309 := (or #308 #343)
+#310 := [quant-inst]: #309
+#450 := [unit-resolution #310 #682 #320]: false
+#646 := [lemma #450]: #343
+#78 := (not #66)
+#647 := [hypothesis]: #78
+#341 := (or #69 #66)
+#79 := (iff #69 #78)
+#14 := (= #13 f1)
+#12 := (= #11 f1)
+#15 := (iff #12 #14)
+#16 := (not #15)
+#82 := (iff #16 #79)
+#72 := (iff #66 #69)
+#75 := (not #72)
+#80 := (iff #75 #79)
+#81 := [rewrite]: #80
+#76 := (iff #16 #75)
+#73 := (iff #15 #72)
+#70 := (iff #14 #69)
+#71 := [rewrite]: #70
+#67 := (iff #12 #66)
+#68 := [rewrite]: #67
+#74 := [monotonicity #68 #71]: #73
+#77 := [monotonicity #74]: #76
+#83 := [trans #77 #81]: #82
+#65 := [asserted]: #16
+#86 := [mp #65 #83]: #79
+#253 := (not #79)
+#340 := (or #69 #66 #253)
+#254 := [def-axiom]: #340
+#255 := [unit-resolution #254 #86]: #341
+#648 := [unit-resolution #255 #647]: #69
+#326 := (or #342 #347)
+#650 := (or #66 #326)
+#661 := (not #326)
+#663 := (iff #66 #661)
+#39 := (:var 1 S2)
+#38 := (:var 2 S2)
+#40 := (f3 #38 #39 #22)
+#690 := (pattern #40)
+#44 := (f7 #39 #22)
+#131 := (= f1 #44)
+#168 := (not #131)
+#42 := (f7 #38 #22)
+#128 := (= f1 #42)
+#167 := (not #128)
+#155 := (or #167 #168)
+#156 := (not #155)
+#124 := (= f1 #40)
+#171 := (iff #124 #156)
+#691 := (forall (vars (?v0 S2) (?v1 S2) (?v2 S3)) (:pat #690) #171)
+#174 := (forall (vars (?v0 S2) (?v1 S2) (?v2 S3)) #171)
+#694 := (iff #174 #691)
+#692 := (iff #171 #171)
+#693 := [refl]: #692
+#695 := [quant-intro #693]: #694
+#134 := (and #128 #131)
+#137 := (iff #124 #134)
+#140 := (forall (vars (?v0 S2) (?v1 S2) (?v2 S3)) #137)
+#175 := (iff #140 #174)
+#172 := (iff #137 #171)
+#169 := (iff #134 #156)
+#170 := [rewrite]: #169
+#173 := [monotonicity #170]: #172
+#176 := [quant-intro #173]: #175
+#153 := (~ #140 #140)
+#164 := (~ #137 #137)
+#165 := [refl]: #164
+#154 := [nnf-pos #165]: #153
+#45 := (= #44 f1)
+#43 := (= #42 f1)
+#46 := (and #43 #45)
+#41 := (= #40 f1)
+#47 := (iff #41 #46)
+#48 := (forall (vars (?v0 S2) (?v1 S2) (?v2 S3)) #47)
+#141 := (iff #48 #140)
+#138 := (iff #47 #137)
+#135 := (iff #46 #134)
+#132 := (iff #45 #131)
+#133 := [rewrite]: #132
+#129 := (iff #43 #128)
+#130 := [rewrite]: #129
+#136 := [monotonicity #130 #133]: #135
+#126 := (iff #41 #124)
+#127 := [rewrite]: #126
+#139 := [monotonicity #127 #136]: #138
+#142 := [quant-intro #139]: #141
+#123 := [asserted]: #48
+#145 := [mp #123 #142]: #140
+#166 := [mp~ #145 #154]: #140
+#177 := [mp #166 #176]: #174
+#696 := [mp #177 #695]: #691
+#657 := (not #691)
+#331 := (or #657 #663)
+#332 := [quant-inst]: #331
+#649 := [unit-resolution #332 #696]: #663
+#658 := (not #663)
+#318 := (or #658 #66 #326)
+#323 := [def-axiom]: #318
+#645 := [unit-resolution #323 #649]: #650
+#651 := [unit-resolution #645 #647]: #326
+#662 := (or #661 #342 #347)
+#668 := [def-axiom]: #662
+#289 := [unit-resolution #668 #651 #648 #646]: false
+#652 := [lemma #289]: #66
+#345 := (or #342 #78)
+#333 := (or #342 #78 #253)
+#344 := [def-axiom]: #333
+#273 := [unit-resolution #344 #86]: #345
+#654 := [unit-resolution #273 #652]: #342
+#294 := (or #78 #661)
+#659 := (or #658 #78 #661)
+#319 := [def-axiom]: #659
+#295 := [unit-resolution #319 #649]: #294
+#655 := [unit-resolution #295 #652]: #661
+#664 := (or #326 #69)
+#665 := [def-axiom]: #664
+[unit-resolution #665 #655 #654]: false
+unsat
+71f085d2a9c00dbd0a999021926a678b17395642 164 0
+#2 := false
+decl f3 :: (-> S2 S2 S3 S1)
+decl f6 :: S3
+#10 := f6
+decl f4 :: S2
+#8 := f4
+decl f5 :: S2
+#9 := f5
+#13 := (f3 f5 f4 f6)
+decl f1 :: S1
+#4 := f1
+#70 := (= f1 #13)
+#343 := (not #70)
+#11 := (f3 f4 f5 f6)
+#67 := (= f1 #11)
+#79 := (not #67)
+#643 := [hypothesis]: #79
+#342 := (or #70 #67)
+#80 := (iff #70 #79)
+#14 := (= #13 f1)
+#12 := (= #11 f1)
+#15 := (iff #12 #14)
+#16 := (not #15)
+#83 := (iff #16 #80)
+#73 := (iff #67 #70)
+#76 := (not #73)
+#81 := (iff #76 #80)
+#82 := [rewrite]: #81
+#77 := (iff #16 #76)
+#74 := (iff #15 #73)
+#71 := (iff #14 #70)
+#72 := [rewrite]: #71
+#68 := (iff #12 #67)
+#69 := [rewrite]: #68
+#75 := [monotonicity #69 #72]: #74
+#78 := [monotonicity #75]: #77
+#84 := [trans #78 #82]: #83
+#66 := [asserted]: #16
+#87 := [mp #66 #84]: #80
+#254 := (not #80)
+#341 := (or #70 #67 #254)
+#255 := [def-axiom]: #341
+#256 := [unit-resolution #255 #87]: #342
+#644 := [unit-resolution #256 #643]: #70
+decl f11 :: (-> S2 S3 S1)
+#327 := (f11 f5 f6)
+#662 := (= f1 #327)
+#664 := (not #662)
+#347 := (f11 f4 f6)
+#344 := (= f1 #347)
+#348 := (not #344)
+#332 := (or #348 #664)
+#642 := (or #67 #332)
+#666 := (not #332)
+#657 := (iff #67 #666)
+#40 := (:var 0 S3)
+#39 := (:var 1 S2)
+#38 := (:var 2 S2)
+#41 := (f3 #38 #39 #40)
+#691 := (pattern #41)
+#45 := (f11 #39 #40)
+#132 := (= f1 #45)
+#169 := (not #132)
+#43 := (f11 #38 #40)
+#129 := (= f1 #43)
+#168 := (not #129)
+#156 := (or #168 #169)
+#157 := (not #156)
+#125 := (= f1 #41)
+#172 := (iff #125 #157)
+#692 := (forall (vars (?v0 S2) (?v1 S2) (?v2 S3)) (:pat #691) #172)
+#175 := (forall (vars (?v0 S2) (?v1 S2) (?v2 S3)) #172)
+#695 := (iff #175 #692)
+#693 := (iff #172 #172)
+#694 := [refl]: #693
+#696 := [quant-intro #694]: #695
+#135 := (and #129 #132)
+#138 := (iff #125 #135)
+#141 := (forall (vars (?v0 S2) (?v1 S2) (?v2 S3)) #138)
+#176 := (iff #141 #175)
+#173 := (iff #138 #172)
+#170 := (iff #135 #157)
+#171 := [rewrite]: #170
+#174 := [monotonicity #171]: #173
+#177 := [quant-intro #174]: #176
+#154 := (~ #141 #141)
+#165 := (~ #138 #138)
+#166 := [refl]: #165
+#155 := [nnf-pos #166]: #154
+#46 := (= #45 f1)
+#44 := (= #43 f1)
+#47 := (and #44 #46)
+#42 := (= #41 f1)
+#48 := (iff #42 #47)
+#49 := (forall (vars (?v0 S2) (?v1 S2) (?v2 S3)) #48)
+#142 := (iff #49 #141)
+#139 := (iff #48 #138)
+#136 := (iff #47 #135)
+#133 := (iff #46 #132)
+#134 := [rewrite]: #133
+#130 := (iff #44 #129)
+#131 := [rewrite]: #130
+#137 := [monotonicity #131 #134]: #136
+#127 := (iff #42 #125)
+#128 := [rewrite]: #127
+#140 := [monotonicity #128 #137]: #139
+#143 := [quant-intro #140]: #142
+#124 := [asserted]: #49
+#146 := [mp #124 #143]: #141
+#167 := [mp~ #146 #155]: #141
+#178 := [mp #167 #177]: #175
+#697 := [mp #178 #696]: #692
+#319 := (not #692)
+#366 := (or #319 #657)
+#367 := [quant-inst]: #366
+#638 := [unit-resolution #367 #697]: #657
+#368 := (not #657)
+#369 := (or #368 #67 #332)
+#262 := [def-axiom]: #369
+#352 := [unit-resolution #262 #638]: #642
+#353 := [unit-resolution #352 #643]: #332
+#355 := (or #343 #666)
+#663 := (iff #70 #666)
+#324 := (or #319 #663)
+#321 := (or #664 #348)
+#451 := (not #321)
+#658 := (iff #70 #451)
+#660 := (or #319 #658)
+#661 := (iff #660 #324)
+#645 := (iff #324 #324)
+#308 := [rewrite]: #645
+#669 := (iff #658 #663)
+#667 := (iff #451 #666)
+#333 := (iff #321 #332)
+#665 := [rewrite]: #333
+#668 := [monotonicity #665]: #667
+#659 := [monotonicity #668]: #669
+#304 := [monotonicity #659]: #661
+#309 := [trans #304 #308]: #661
+#320 := [quant-inst]: #660
+#310 := [mp #320 #309]: #324
+#354 := [unit-resolution #310 #697]: #663
+#646 := (not #663)
+#653 := (or #646 #343 #666)
+#655 := [def-axiom]: #653
+#633 := [unit-resolution #655 #354]: #355
+#634 := [unit-resolution #633 #353 #644]: false
+#349 := [lemma #634]: #67
+#346 := (or #343 #79)
+#334 := (or #343 #79 #254)
+#345 := [def-axiom]: #334
+#274 := [unit-resolution #345 #87]: #346
+#631 := [unit-resolution #274 #349]: #343
+#635 := (or #79 #666)
+#639 := (or #368 #79 #666)
+#640 := [def-axiom]: #639
+#632 := [unit-resolution #640 #638]: #635
+#636 := [unit-resolution #632 #349]: #666
+#625 := (or #70 #332)
+#652 := (or #646 #70 #332)
+#290 := [def-axiom]: #652
+#626 := [unit-resolution #290 #354]: #625
+[unit-resolution #626 #636 #631]: false
+unsat
+4a2ec1009e57974d1e4c4125b313542f141f334f 142 0
+#2 := false
+decl f3 :: (-> S2 S2 S3 S1)
+decl f5 :: S3
+#9 := f5
+decl f4 :: S2
+#8 := f4
+#10 := (f3 f4 f4 f5)
+decl f1 :: S1
+#4 := f1
+#66 := (= f1 #10)
+#78 := (not #66)
+#649 := [hypothesis]: #78
+decl f6 :: (-> S2 S3 S1)
+#12 := (f6 f4 f5)
+#69 := (= f1 #12)
+#341 := (or #69 #66)
+#79 := (iff #69 #78)
+#13 := (= #12 f1)
+#11 := (= #10 f1)
+#14 := (iff #11 #13)
+#15 := (not #14)
+#82 := (iff #15 #79)
+#72 := (iff #66 #69)
+#75 := (not #72)
+#80 := (iff #75 #79)
+#81 := [rewrite]: #80
+#76 := (iff #15 #75)
+#73 := (iff #14 #72)
+#70 := (iff #13 #69)
+#71 := [rewrite]: #70
+#67 := (iff #11 #66)
+#68 := [rewrite]: #67
+#74 := [monotonicity #68 #71]: #73
+#77 := [monotonicity #74]: #76
+#83 := [trans #77 #81]: #82
+#65 := [asserted]: #15
+#86 := [mp #65 #83]: #79
+#253 := (not #79)
+#340 := (or #69 #66 #253)
+#254 := [def-axiom]: #340
+#255 := [unit-resolution #254 #86]: #341
+#650 := [unit-resolution #255 #649]: #69
+#342 := (not #69)
+#651 := (or #66 #342)
+#39 := (:var 0 S3)
+#38 := (:var 1 S2)
+#37 := (:var 2 S2)
+#40 := (f3 #37 #38 #39)
+#690 := (pattern #40)
+#44 := (f6 #38 #39)
+#131 := (= f1 #44)
+#168 := (not #131)
+#42 := (f6 #37 #39)
+#128 := (= f1 #42)
+#167 := (not #128)
+#155 := (or #167 #168)
+#156 := (not #155)
+#124 := (= f1 #40)
+#171 := (iff #124 #156)
+#691 := (forall (vars (?v0 S2) (?v1 S2) (?v2 S3)) (:pat #690) #171)
+#174 := (forall (vars (?v0 S2) (?v1 S2) (?v2 S3)) #171)
+#694 := (iff #174 #691)
+#692 := (iff #171 #171)
+#693 := [refl]: #692
+#695 := [quant-intro #693]: #694
+#134 := (and #128 #131)
+#137 := (iff #124 #134)
+#140 := (forall (vars (?v0 S2) (?v1 S2) (?v2 S3)) #137)
+#175 := (iff #140 #174)
+#172 := (iff #137 #171)
+#169 := (iff #134 #156)
+#170 := [rewrite]: #169
+#173 := [monotonicity #170]: #172
+#176 := [quant-intro #173]: #175
+#153 := (~ #140 #140)
+#164 := (~ #137 #137)
+#165 := [refl]: #164
+#154 := [nnf-pos #165]: #153
+#45 := (= #44 f1)
+#43 := (= #42 f1)
+#46 := (and #43 #45)
+#41 := (= #40 f1)
+#47 := (iff #41 #46)
+#48 := (forall (vars (?v0 S2) (?v1 S2) (?v2 S3)) #47)
+#141 := (iff #48 #140)
+#138 := (iff #47 #137)
+#135 := (iff #46 #134)
+#132 := (iff #45 #131)
+#133 := [rewrite]: #132
+#129 := (iff #43 #128)
+#130 := [rewrite]: #129
+#136 := [monotonicity #130 #133]: #135
+#126 := (iff #41 #124)
+#127 := [rewrite]: #126
+#139 := [monotonicity #127 #136]: #138
+#142 := [quant-intro #139]: #141
+#123 := [asserted]: #48
+#145 := [mp #123 #142]: #140
+#166 := [mp~ #145 #154]: #140
+#177 := [mp #166 #176]: #174
+#696 := [mp #177 #695]: #691
+#667 := (not #691)
+#662 := (or #667 #72)
+#346 := (or #342 #342)
+#343 := (not #346)
+#347 := (iff #66 #343)
+#668 := (or #667 #347)
+#318 := (iff #668 #662)
+#659 := (iff #662 #662)
+#319 := [rewrite]: #659
+#665 := (iff #347 #72)
+#332 := (iff #343 #69)
+#663 := (not #342)
+#657 := (iff #663 #69)
+#331 := [rewrite]: #657
+#320 := (iff #343 #663)
+#326 := (iff #346 #342)
+#661 := [rewrite]: #326
+#450 := [monotonicity #661]: #320
+#664 := [trans #450 #331]: #332
+#666 := [monotonicity #664]: #665
+#323 := [monotonicity #666]: #318
+#660 := [trans #323 #319]: #318
+#658 := [quant-inst]: #668
+#303 := [mp #658 #660]: #662
+#645 := [unit-resolution #303 #696]: #72
+#644 := (or #75 #66 #342)
+#307 := [def-axiom]: #644
+#289 := [unit-resolution #307 #645]: #651
+#652 := [unit-resolution #289 #650 #649]: false
+#654 := [lemma #652]: #66
+#345 := (or #342 #78)
+#333 := (or #342 #78 #253)
+#344 := [def-axiom]: #333
+#273 := [unit-resolution #344 #86]: #345
+#294 := [unit-resolution #273 #654]: #342
+#295 := (or #78 #69)
+#308 := (or #75 #78 #69)
+#309 := [def-axiom]: #308
+#655 := [unit-resolution #309 #645]: #295
+[unit-resolution #655 #294 #654]: false
+unsat
+9a719bb56314c3b4bab4bac5b0adde4b491a8497 279 0
+#2 := false
+decl f3 :: (-> S2 S3 S1)
+decl f8 :: S3
+#13 := f8
+decl f4 :: (-> S2 S2 S2)
+decl f6 :: S2
+#9 := f6
+decl f5 :: S2
+#8 := f5
+#16 := (f4 f5 f6)
+#315 := (f3 #16 f8)
+decl f1 :: S1
+#4 := f1
+#652 := (= f1 #315)
+#250 := (f3 f6 f8)
+#629 := (= f1 #250)
+#626 := (not #629)
+#340 := (f3 f5 f8)
+#356 := (= f1 #340)
+#357 := (not #356)
+#615 := (or #357 #626)
+#616 := (not #615)
+#612 := (iff #616 #652)
+#583 := (not #612)
+#571 := [hypothesis]: #583
+#46 := (:var 0 S3)
+#44 := (:var 1 S2)
+#43 := (:var 2 S2)
+#45 := (f4 #43 #44)
+#47 := (f3 #45 #46)
+#681 := (pattern #47)
+#51 := (f3 #44 #46)
+#138 := (= f1 #51)
+#175 := (not #138)
+#49 := (f3 #43 #46)
+#135 := (= f1 #49)
+#174 := (not #135)
+#162 := (or #174 #175)
+#163 := (not #162)
+#131 := (= f1 #47)
+#178 := (iff #131 #163)
+#682 := (forall (vars (?v0 S2) (?v1 S2) (?v2 S3)) (:pat #681) #178)
+#181 := (forall (vars (?v0 S2) (?v1 S2) (?v2 S3)) #178)
+#685 := (iff #181 #682)
+#683 := (iff #178 #178)
+#684 := [refl]: #683
+#686 := [quant-intro #684]: #685
+#141 := (and #135 #138)
+#144 := (iff #131 #141)
+#147 := (forall (vars (?v0 S2) (?v1 S2) (?v2 S3)) #144)
+#182 := (iff #147 #181)
+#179 := (iff #144 #178)
+#176 := (iff #141 #163)
+#177 := [rewrite]: #176
+#180 := [monotonicity #177]: #179
+#183 := [quant-intro #180]: #182
+#160 := (~ #147 #147)
+#171 := (~ #144 #144)
+#172 := [refl]: #171
+#161 := [nnf-pos #172]: #160
+#52 := (= #51 f1)
+#50 := (= #49 f1)
+#53 := (and #50 #52)
+#48 := (= #47 f1)
+#54 := (iff #48 #53)
+#55 := (forall (vars (?v0 S2) (?v1 S2) (?v2 S3)) #54)
+#148 := (iff #55 #147)
+#145 := (iff #54 #144)
+#142 := (iff #53 #141)
+#139 := (iff #52 #138)
+#140 := [rewrite]: #139
+#136 := (iff #50 #135)
+#137 := [rewrite]: #136
+#143 := [monotonicity #137 #140]: #142
+#133 := (iff #48 #131)
+#134 := [rewrite]: #133
+#146 := [monotonicity #134 #143]: #145
+#149 := [quant-intro #146]: #148
+#130 := [asserted]: #55
+#152 := [mp #130 #149]: #147
+#173 := [mp~ #152 #161]: #147
+#184 := [mp #173 #183]: #181
+#687 := [mp #184 #686]: #682
+#307 := (not #682)
+#598 := (or #307 #612)
+#617 := (iff #652 #616)
+#614 := (or #307 #617)
+#619 := (iff #614 #598)
+#462 := (iff #598 #598)
+#463 := [rewrite]: #462
+#613 := (iff #617 #612)
+#618 := [rewrite]: #613
+#461 := [monotonicity #618]: #619
+#605 := [trans #461 #463]: #619
+#620 := [quant-inst]: #614
+#606 := [mp #620 #605]: #598
+#567 := [unit-resolution #606 #687 #571]: false
+#572 := [lemma #567]: #612
+#654 := (not #652)
+decl f7 :: S2
+#10 := f7
+#335 := (f3 f7 f8)
+#332 := (= f1 #335)
+#336 := (not #332)
+#320 := (or #336 #654)
+#17 := (f4 #16 f7)
+#18 := (f3 #17 f8)
+#76 := (= f1 #18)
+#331 := (not #76)
+#11 := (f4 f6 f7)
+#12 := (f4 f5 #11)
+#14 := (f3 #12 f8)
+#73 := (= f1 #14)
+#647 := (f3 #11 f8)
+#633 := (= f1 #647)
+#485 := (or #336 #626)
+#494 := (not #485)
+#495 := (iff #494 #633)
+#588 := (not #495)
+#568 := [hypothesis]: #588
+#499 := (or #307 #495)
+#601 := (or #626 #336)
+#483 := (not #601)
+#484 := (iff #633 #483)
+#500 := (or #307 #484)
+#594 := (iff #500 #499)
+#595 := (iff #499 #499)
+#582 := [rewrite]: #595
+#497 := (iff #484 #495)
+#593 := (iff #633 #494)
+#496 := (iff #593 #495)
+#489 := [rewrite]: #496
+#478 := (iff #484 #593)
+#589 := (iff #483 #494)
+#444 := (iff #601 #485)
+#592 := [rewrite]: #444
+#590 := [monotonicity #592]: #589
+#493 := [monotonicity #590]: #478
+#498 := [trans #493 #489]: #497
+#591 := [monotonicity #498]: #594
+#584 := [trans #591 #582]: #594
+#501 := [quant-inst]: #500
+#576 := [mp #501 #584]: #499
+#569 := [unit-resolution #576 #687 #568]: false
+#570 := [lemma #569]: #495
+#634 := (not #633)
+#358 := (or #357 #634)
+#85 := (not #73)
+#558 := [hypothesis]: #85
+#561 := (or #73 #358)
+#344 := (not #358)
+#359 := (iff #73 #344)
+#630 := (or #307 #359)
+#352 := [quant-inst]: #630
+#559 := [unit-resolution #352 #687]: #359
+#342 := (not #359)
+#343 := (or #342 #73 #358)
+#345 := [def-axiom]: #343
+#562 := [unit-resolution #345 #559]: #561
+#563 := [unit-resolution #562 #558]: #358
+#656 := (not #320)
+#330 := (or #76 #73)
+#86 := (iff #76 #85)
+#19 := (= #18 f1)
+#15 := (= #14 f1)
+#20 := (iff #15 #19)
+#21 := (not #20)
+#89 := (iff #21 #86)
+#79 := (iff #73 #76)
+#82 := (not #79)
+#87 := (iff #82 #86)
+#88 := [rewrite]: #87
+#83 := (iff #21 #82)
+#80 := (iff #20 #79)
+#77 := (iff #19 #76)
+#78 := [rewrite]: #77
+#74 := (iff #15 #73)
+#75 := [rewrite]: #74
+#81 := [monotonicity #75 #78]: #80
+#84 := [monotonicity #81]: #83
+#90 := [trans #84 #88]: #89
+#72 := [asserted]: #21
+#93 := [mp #72 #90]: #86
+#242 := (not #86)
+#329 := (or #76 #73 #242)
+#243 := [def-axiom]: #329
+#244 := [unit-resolution #243 #93]: #330
+#560 := [unit-resolution #244 #558]: #76
+#544 := (or #331 #656)
+#653 := (iff #76 #656)
+#312 := (or #307 #653)
+#309 := (or #654 #336)
+#441 := (not #309)
+#648 := (iff #76 #441)
+#650 := (or #307 #648)
+#651 := (iff #650 #312)
+#635 := (iff #312 #312)
+#296 := [rewrite]: #635
+#659 := (iff #648 #653)
+#657 := (iff #441 #656)
+#321 := (iff #309 #320)
+#655 := [rewrite]: #321
+#658 := [monotonicity #655]: #657
+#649 := [monotonicity #658]: #659
+#292 := [monotonicity #649]: #651
+#297 := [trans #292 #296]: #651
+#308 := [quant-inst]: #650
+#298 := [mp #308 #297]: #312
+#564 := [unit-resolution #298 #687]: #653
+#636 := (not #653)
+#643 := (or #636 #331 #656)
+#645 := [def-axiom]: #643
+#545 := [unit-resolution #645 #564]: #544
+#547 := [unit-resolution #545 #560]: #656
+#638 := (or #320 #652)
+#639 := [def-axiom]: #638
+#548 := [unit-resolution #639 #547]: #652
+#577 := (or #583 #616 #654)
+#578 := [def-axiom]: #577
+#549 := [unit-resolution #578 #548 #572]: #616
+#607 := (or #615 #356)
+#573 := [def-axiom]: #607
+#550 := [unit-resolution #573 #549]: #356
+#632 := (or #344 #357 #634)
+#341 := [def-axiom]: #632
+#551 := [unit-resolution #341 #550 #563]: #634
+#299 := (or #320 #332)
+#637 := [def-axiom]: #299
+#552 := [unit-resolution #637 #547]: #332
+#575 := (or #615 #629)
+#585 := [def-axiom]: #575
+#553 := [unit-resolution #585 #549]: #629
+#610 := (or #494 #336 #626)
+#604 := [def-axiom]: #610
+#554 := [unit-resolution #604 #553 #552]: #494
+#442 := (or #588 #485 #633)
+#443 := [def-axiom]: #442
+#555 := [unit-resolution #443 #554 #551 #570]: false
+#556 := [lemma #555]: #73
+#334 := (or #331 #85)
+#322 := (or #331 #85 #242)
+#333 := [def-axiom]: #322
+#262 := [unit-resolution #333 #93]: #334
+#546 := [unit-resolution #262 #556]: #331
+#557 := (or #76 #320)
+#642 := (or #636 #76 #320)
+#278 := [def-axiom]: #642
+#535 := [unit-resolution #278 #564]: #557
+#536 := [unit-resolution #535 #546]: #320
+#538 := (or #85 #344)
+#623 := (or #342 #85 #344)
+#624 := [def-axiom]: #623
+#539 := [unit-resolution #624 #559]: #538
+#540 := [unit-resolution #539 #556]: #344
+#631 := (or #358 #633)
+#628 := [def-axiom]: #631
+#541 := [unit-resolution #628 #540]: #633
+#611 := (or #588 #494 #634)
+#440 := [def-axiom]: #611
+#542 := [unit-resolution #440 #541 #570]: #494
+#608 := (or #485 #332)
+#602 := [def-axiom]: #608
+#537 := [unit-resolution #602 #542]: #332
+#640 := (or #656 #336 #654)
+#641 := [def-axiom]: #640
+#543 := [unit-resolution #641 #537 #536]: #654
+#353 := (or #358 #356)
+#627 := [def-axiom]: #353
+#529 := [unit-resolution #627 #540]: #356
+#603 := (or #485 #629)
+#609 := [def-axiom]: #603
+#525 := [unit-resolution #609 #542]: #629
+#586 := (or #616 #357 #626)
+#587 := [def-axiom]: #586
+#526 := [unit-resolution #587 #525 #529]: #616
+#579 := (or #583 #615 #652)
+#580 := [def-axiom]: #579
+[unit-resolution #580 #526 #543 #572]: false
+unsat
+d1f4c7d9bd1f639df15a28175017a4537fb9637f 18 0
+#2 := false
+decl f3 :: S2
+#8 := f3
+#9 := (= f3 f3)
+#10 := (not #9)
+#68 := (iff #10 false)
+#1 := true
+#63 := (not true)
+#66 := (iff #63 false)
+#67 := [rewrite]: #66
+#64 := (iff #10 #63)
+#61 := (iff #9 true)
+#62 := [rewrite]: #61
+#65 := [monotonicity #62]: #64
+#69 := [trans #65 #67]: #68
+#60 := [asserted]: #10
+[mp #60 #69]: false
+unsat

--- a/src/HOL/SMT_Examples/SMT_Tests.thy	Thu May 27 17:09:37 2010 +0200
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Thu May 27 18:16:54 2010 +0200
@@ -618,4 +618,50 @@
   "(fst p = snd p) = (p = (snd p, fst p))"
   by smt+
 
+
+
+section {* Function updates *}
+
+lemma
+  "(f (i := v)) i = v"
+  "i1 \<noteq> i2 \<longrightarrow> (f (i1 := v)) i2 = f i2"
+  "i1 \<noteq> i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i1 = v1"
+  "i1 \<noteq> i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i2 = v2"
+  "i1 = i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i1 = v2"
+  "i1 = i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i1 = v2"
+  "distinct [i1, i2, i3] \<longrightarrow> (f (i1 := v1, i2 := v2)) i3 = f i3"
+  by smt+
+
+
+
+section {* Sets *}
+
+lemma smt_sets:
+  "\<not>({} x)"
+  "UNIV x"
+  "(A \<union> B) x = (A x \<or> B x)"
+  "(A \<inter> B) x = (A x \<and> B x)"
+  by auto
+
+lemma
+  "x \<in> P = P x"
+  "x \<in> {x. P x} = P x"
+  "x \<notin> {}"
+  "x \<in> UNIV"
+  "x \<in> P \<union> Q = (P x \<or> Q x)"
+  "x \<in> P \<union> {} = P x"
+  "x \<in> P \<union> UNIV"
+  "(x \<in> P \<union> Q) = (x \<in> Q \<union> P)"
+  "(x \<in> P \<union> P) = (x \<in> P)"
+  "(x \<in> P \<union> (Q \<union> R)) = (x \<in> (P \<union> Q) \<union> R)"
+  "(x \<in> P \<inter> Q) = (P x \<and> Q x)"
+  "x \<notin> P \<inter> {}"
+  "(x \<in> P \<inter> UNIV) = (x \<in> P)"
+  "(x \<in> P \<inter> Q) = (x \<in> Q \<inter> P)"
+  "(x \<in> P \<inter> P) = (x \<in> P)"
+  "(x \<in> P \<inter> (Q \<inter> R)) = (x \<in> (P \<inter> Q) \<inter> R)"
+  "{x. P x} = {y. P y}"
+  unfolding mem_def Collect_def
+  by (smt smt_sets)+
+
 end