isabelle: changeset 43273:4de998188c1d

--- a/src/HOL/Multivariate_Analysis/Integration.certs	Wed Jun 08 11:59:45 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.certs	Wed Jun 08 13:43:15 2011 +0200
@@ -621,7 +621,7 @@
 #427 := [unit-resolution #411 #426]: #395
 [th-lemma arith farkas 2 1 2 3 1 1 #421 #319 #321 #414 #318 #427]: false
 unsat
-02d40f3e43c6a17458cd5dc30adbe4da03d87a0c 57 0
+abf6187dd71c2713828c15119491112c5b865e88 57 0
 #2 := false
 #41 := 0::Real
 decl f12 :: (-> S5 Real)
@@ -660,10 +660,10 @@
 #243 := (iff #137 #137)
 #244 := [refl]: #243
 #246 := [quant-intro #244]: #245
-#146 := (~ #139 #139)
-#148 := (~ #137 #137)
-#145 := [refl]: #148
-#143 := [nnf-pos #145]: #146
+#155 := (~ #139 #139)
+#143 := (~ #137 #137)
+#144 := [refl]: #143
+#156 := [nnf-pos #144]: #155
 #47 := (<= 0::Real #46)
 #48 := (forall (vars (?v0 S4) (?v1 S4)) #47)
 #140 := (iff #48 #139)
@@ -672,8 +672,8 @@
 #141 := [quant-intro #138]: #140
 #133 := [asserted]: #48
 #142 := [mp #133 #141]: #139
-#144 := [mp~ #142 #143]: #139
-#247 := [mp #144 #246]: #242
+#157 := [mp~ #142 #156]: #139
+#247 := [mp #157 #246]: #242
 #251 := (not #242)
 #252 := (or #251 #248)
 #253 := [quant-inst #37 #38]: #252

--- a/src/HOL/SMT_Examples/SMT_Examples.certs	Wed Jun 08 11:59:45 2011 +0200
+++ b/src/HOL/SMT_Examples/SMT_Examples.certs	Wed Jun 08 13:43:15 2011 +0200
@@ -15565,3 +15565,598 @@
 #252 := [asserted]: #105
 [unit-resolution #252 #617]: false
 unsat
+5a76ac61ccccc3cf413dd2cf808cc3df750b1eab 61 0
+#2 := false
+decl f7 :: S2
+#18 := f7
+decl f5 :: S2
+#14 := f5
+#20 := (= f5 f7)
+decl f3 :: (-> S4 S2)
+decl f4 :: (-> S2 S3 S4)
+decl f6 :: S3
+#15 := f6
+#16 := (f4 f5 f6)
+#17 := (f3 #16)
+#19 := (= #17 f7)
+#50 := (not #19)
+#52 := (or #50 #20)
+#55 := (not #52)
+#21 := (implies #19 #20)
+#22 := (not #21)
+#56 := (iff #22 #55)
+#53 := (iff #21 #52)
+#54 := [rewrite]: #53
+#57 := [monotonicity #54]: #56
+#49 := [asserted]: #22
+#60 := [mp #49 #57]: #55
+#58 := [not-or-elim #60]: #19
+#125 := (= f5 #17)
+#9 := (:var 0 S3)
+#8 := (:var 1 S2)
+#10 := (f4 #8 #9)
+#543 := (pattern #10)
+#11 := (f3 #10)
+#43 := (= #8 #11)
+#544 := (forall (vars (?v0 S2) (?v1 S3)) (:pat #543) #43)
+#46 := (forall (vars (?v0 S2) (?v1 S3)) #43)
+#547 := (iff #46 #544)
+#545 := (iff #43 #43)
+#546 := [refl]: #545
+#548 := [quant-intro #546]: #547
+#73 := (~ #46 #46)
+#71 := (~ #43 #43)
+#72 := [refl]: #71
+#74 := [nnf-pos #72]: #73
+#12 := (= #11 #8)
+#13 := (forall (vars (?v0 S2) (?v1 S3)) #12)
+#47 := (iff #13 #46)
+#44 := (iff #12 #43)
+#45 := [rewrite]: #44
+#48 := [quant-intro #45]: #47
+#42 := [asserted]: #13
+#51 := [mp #42 #48]: #46
+#63 := [mp~ #51 #74]: #46
+#549 := [mp #63 #548]: #544
+#213 := (not #544)
+#127 := (or #213 #125)
+#214 := [quant-inst #14 #15]: #127
+#212 := [unit-resolution #214 #549]: #125
+#126 := [trans #212 #58]: #20
+#59 := (not #20)
+#61 := [not-or-elim #60]: #59
+[unit-resolution #61 #126]: false
+unsat
+e37a715fae94dfacce2b81d39c657fd74713dfe9 116 0
+#2 := false
+decl f8 :: (-> S4 S3)
+decl f12 :: S4
+#31 := f12
+#36 := (f8 f12)
+decl f5 :: (-> S5 S3)
+decl f9 :: S5
+#26 := f9
+#35 := (f5 f9)
+#37 := (= #35 #36)
+decl f4 :: (-> S2 S3 S4)
+decl f10 :: S3
+#27 := f10
+decl f11 :: S2
+#28 := f11
+#32 := (f4 f11 f10)
+#184 := (f8 #32)
+#248 := (= #184 #36)
+#600 := (= #36 #184)
+#33 := (= f12 #32)
+decl f6 :: (-> S3 S2 S5)
+#29 := (f6 f10 f11)
+#30 := (= f9 #29)
+#34 := (and #30 #33)
+#91 := (not #34)
+#93 := (or #91 #37)
+#96 := (not #93)
+#38 := (implies #34 #37)
+#39 := (not #38)
+#97 := (iff #39 #96)
+#94 := (iff #38 #93)
+#95 := [rewrite]: #94
+#98 := [monotonicity #95]: #97
+#90 := [asserted]: #39
+#101 := [mp #90 #98]: #96
+#99 := [not-or-elim #101]: #34
+#102 := [and-elim #99]: #33
+#590 := [monotonicity #102]: #600
+#253 := [symm #590]: #248
+#592 := (= #35 #184)
+#271 := (= f10 #184)
+#9 := (:var 0 S3)
+#8 := (:var 1 S2)
+#10 := (f4 #8 #9)
+#601 := (pattern #10)
+#23 := (f8 #10)
+#83 := (= #9 #23)
+#621 := (forall (vars (?v0 S2) (?v1 S3)) (:pat #601) #83)
+#87 := (forall (vars (?v0 S2) (?v1 S3)) #83)
+#624 := (iff #87 #621)
+#622 := (iff #83 #83)
+#623 := [refl]: #622
+#625 := [quant-intro #623]: #624
+#112 := (~ #87 #87)
+#131 := (~ #83 #83)
+#132 := [refl]: #131
+#113 := [nnf-pos #132]: #112
+#24 := (= #23 #9)
+#25 := (forall (vars (?v0 S2) (?v1 S3)) #24)
+#88 := (iff #25 #87)
+#85 := (iff #24 #83)
+#86 := [rewrite]: #85
+#89 := [quant-intro #86]: #88
+#82 := [asserted]: #25
+#92 := [mp #82 #89]: #87
+#133 := [mp~ #92 #113]: #87
+#626 := [mp #133 #625]: #621
+#203 := (not #621)
+#276 := (or #203 #271)
+#273 := [quant-inst #28 #27]: #276
+#382 := [unit-resolution #273 #626]: #271
+#591 := (= #35 f10)
+#274 := (f5 #29)
+#599 := (= #274 f10)
+#275 := (= f10 #274)
+#15 := (:var 0 S2)
+#14 := (:var 1 S3)
+#16 := (f6 #14 #15)
+#608 := (pattern #16)
+#17 := (f5 #16)
+#67 := (= #14 #17)
+#609 := (forall (vars (?v0 S3) (?v1 S2)) (:pat #608) #67)
+#71 := (forall (vars (?v0 S3) (?v1 S2)) #67)
+#612 := (iff #71 #609)
+#610 := (iff #67 #67)
+#611 := [refl]: #610
+#613 := [quant-intro #611]: #612
+#108 := (~ #71 #71)
+#107 := (~ #67 #67)
+#126 := [refl]: #107
+#109 := [nnf-pos #126]: #108
+#18 := (= #17 #14)
+#19 := (forall (vars (?v0 S3) (?v1 S2)) #18)
+#72 := (iff #19 #71)
+#69 := (iff #18 #67)
+#70 := [rewrite]: #69
+#73 := [quant-intro #70]: #72
+#66 := [asserted]: #19
+#76 := [mp #66 #73]: #71
+#127 := [mp~ #76 #109]: #71
+#614 := [mp #127 #613]: #609
+#593 := (not #609)
+#595 := (or #593 #275)
+#250 := [quant-inst #27 #28]: #595
+#589 := [unit-resolution #250 #614]: #275
+#594 := [symm #589]: #599
+#597 := (= #35 #274)
+#100 := [and-elim #99]: #30
+#598 := [monotonicity #100]: #597
+#249 := [trans #598 #594]: #591
+#233 := [trans #249 #382]: #592
+#576 := [trans #233 #253]: #37
+#103 := (not #37)
+#104 := [not-or-elim #101]: #103
+[unit-resolution #104 #576]: false
+unsat
+0a51c265dbf4d3067e92be219272e95358c500c5 415 0
+#2 := false
+decl f3 :: (-> S2 S3)
+decl f4 :: (-> S1 S2)
+decl f1 :: S1
+#4 := f1
+#102 := (f4 f1)
+#103 := (f3 #102)
+decl f8 :: (-> S5 S3)
+decl f9 :: (-> Int S5)
+#99 := 3::Int
+#100 := (f9 3::Int)
+#101 := (f8 #100)
+#104 := (= #101 #103)
+decl f5 :: (-> S4 S3)
+decl f6 :: (-> S1 S4 S4)
+decl f7 :: S4
+#11 := f7
+#462 := (f6 f1 f7)
+#546 := (f5 #462)
+#638 := (= #546 #103)
+#547 := (= #103 #546)
+#8 := (:var 0 S1)
+#12 := (f6 #8 f7)
+#877 := (pattern #12)
+#9 := (f4 #8)
+#876 := (pattern #9)
+#13 := (f5 #12)
+#10 := (f3 #9)
+#14 := (= #10 #13)
+#878 := (forall (vars (?v0 S1)) (:pat #876 #877) #14)
+#15 := (forall (vars (?v0 S1)) #14)
+#881 := (iff #15 #878)
+#879 := (iff #14 #14)
+#880 := [refl]: #879
+#882 := [quant-intro #880]: #881
+#384 := (~ #15 #15)
+#382 := (~ #14 #14)
+#383 := [refl]: #382
+#385 := [nnf-pos #383]: #384
+#140 := [asserted]: #15
+#340 := [mp~ #140 #385]: #15
+#883 := [mp #340 #882]: #878
+#550 := (not #878)
+#551 := (or #550 #547)
+#552 := [quant-inst #4]: #551
+#719 := [unit-resolution #552 #883]: #547
+#640 := [symm #719]: #638
+#637 := (= #101 #546)
+decl f16 :: (-> S4 S3)
+#569 := (f16 #462)
+#631 := (= #569 #546)
+#843 := (= #546 #569)
+#39 := (:var 0 S4)
+#41 := (f16 #39)
+#901 := (pattern #41)
+#40 := (f5 #39)
+#900 := (pattern #40)
+#42 := (= #40 #41)
+#902 := (forall (vars (?v0 S4)) (:pat #900 #901) #42)
+#43 := (forall (vars (?v0 S4)) #42)
+#905 := (iff #43 #902)
+#903 := (iff #42 #42)
+#904 := [refl]: #903
+#906 := [quant-intro #904]: #905
+#354 := (~ #43 #43)
+#353 := (~ #42 #42)
+#350 := [refl]: #353
+#355 := [nnf-pos #350]: #354
+#154 := [asserted]: #43
+#351 := [mp~ #154 #355]: #43
+#907 := [mp #351 #906]: #902
+#872 := (not #902)
+#848 := (or #872 #843)
+#558 := [quant-inst #462]: #848
+#674 := [unit-resolution #558 #907]: #843
+#634 := [symm #674]: #631
+#636 := (= #101 #569)
+decl f18 :: (-> S7 Int S3)
+decl f21 :: (-> S3 Int)
+#85 := (f16 f7)
+#847 := (f21 #85)
+#64 := 1::Int
+#844 := (+ 1::Int #847)
+decl f19 :: S7
+#46 := f19
+#559 := (f18 f19 #844)
+#561 := (= #559 #569)
+#71 := (:var 1 S1)
+#72 := (f6 #71 #39)
+#943 := (pattern #72)
+#94 := (f21 #41)
+#238 := (+ 1::Int #94)
+#243 := (f18 f19 #238)
+#93 := (f16 #72)
+#246 := (= #93 #243)
+#944 := (forall (vars (?v0 S1) (?v1 S4)) (:pat #943) #246)
+#249 := (forall (vars (?v0 S1) (?v1 S4)) #246)
+#947 := (iff #249 #944)
+#945 := (iff #246 #246)
+#946 := [refl]: #945
+#948 := [quant-intro #946]: #947
+#370 := (~ #249 #249)
+#369 := (~ #246 #246)
+#366 := [refl]: #369
+#371 := [nnf-pos #366]: #370
+#47 := 0::Int
+#65 := (+ 0::Int 1::Int)
+#95 := (+ #94 #65)
+#96 := (f18 f19 #95)
+#97 := (= #93 #96)
+#98 := (forall (vars (?v0 S1) (?v1 S4)) #97)
+#250 := (iff #98 #249)
+#247 := (iff #97 #246)
+#244 := (= #96 #243)
+#241 := (= #95 #238)
+#234 := (+ #94 1::Int)
+#239 := (= #234 #238)
+#240 := [rewrite]: #239
+#236 := (= #95 #234)
+#165 := (= #65 1::Int)
+#167 := [rewrite]: #165
+#237 := [monotonicity #167]: #236
+#242 := [trans #237 #240]: #241
+#245 := [monotonicity #242]: #244
+#248 := [monotonicity #245]: #247
+#251 := [quant-intro #248]: #250
+#233 := [asserted]: #98
+#254 := [mp #233 #251]: #249
+#367 := [mp~ #254 #371]: #249
+#949 := [mp #367 #948]: #944
+#554 := (not #944)
+#837 := (or #554 #561)
+#560 := (= #569 #559)
+#841 := (or #554 #560)
+#842 := (iff #841 #837)
+#832 := (iff #837 #837)
+#833 := [rewrite]: #832
+#839 := (iff #560 #561)
+#840 := [rewrite]: #839
+#831 := [monotonicity #840]: #842
+#828 := [trans #831 #833]: #842
+#838 := [quant-inst #4 #11]: #841
+#829 := [mp #838 #828]: #837
+#681 := [unit-resolution #829 #949]: #561
+#633 := (= #101 #559)
+decl f15 :: (-> S6 S3)
+decl f12 :: S6
+#19 := f12
+#83 := (f15 f12)
+#830 := (f21 #83)
+#836 := (+ 1::Int #830)
+#679 := (f18 f19 #836)
+#647 := (= #679 #559)
+#646 := (= #836 #844)
+#644 := (= 1::Int #844)
+#653 := (= #844 1::Int)
+#815 := (<= #847 0::Int)
+#813 := (= #847 0::Int)
+#48 := (f18 f19 0::Int)
+#869 := (f21 #48)
+#866 := (= #869 0::Int)
+#16 := (:var 0 Int)
+#112 := (f18 f19 #16)
+#957 := (pattern #112)
+#280 := (>= #16 0::Int)
+#281 := (not #280)
+#113 := (f21 #112)
+#262 := (= #16 #113)
+#287 := (or #262 #281)
+#958 := (forall (vars (?v0 Int)) (:pat #957) #287)
+#292 := (forall (vars (?v0 Int)) #287)
+#961 := (iff #292 #958)
+#959 := (iff #287 #287)
+#960 := [refl]: #959
+#962 := [quant-intro #960]: #961
+#376 := (~ #292 #292)
+#375 := (~ #287 #287)
+#402 := [refl]: #375
+#377 := [nnf-pos #402]: #376
+#114 := (= #113 #16)
+#111 := (<= 0::Int #16)
+#115 := (implies #111 #114)
+#116 := (forall (vars (?v0 Int)) #115)
+#295 := (iff #116 #292)
+#269 := (not #111)
+#270 := (or #269 #262)
+#275 := (forall (vars (?v0 Int)) #270)
+#293 := (iff #275 #292)
+#290 := (iff #270 #287)
+#284 := (or #281 #262)
+#288 := (iff #284 #287)
+#289 := [rewrite]: #288
+#285 := (iff #270 #284)
+#282 := (iff #269 #281)
+#278 := (iff #111 #280)
+#279 := [rewrite]: #278
+#283 := [monotonicity #279]: #282
+#286 := [monotonicity #283]: #285
+#291 := [trans #286 #289]: #290
+#294 := [quant-intro #291]: #293
+#276 := (iff #116 #275)
+#273 := (iff #115 #270)
+#266 := (implies #111 #262)
+#271 := (iff #266 #270)
+#272 := [rewrite]: #271
+#267 := (iff #115 #266)
+#264 := (iff #114 #262)
+#265 := [rewrite]: #264
+#268 := [monotonicity #265]: #267
+#274 := [trans #268 #272]: #273
+#277 := [quant-intro #274]: #276
+#296 := [trans #277 #294]: #295
+#261 := [asserted]: #116
+#297 := [mp #261 #296]: #292
+#403 := [mp~ #297 #377]: #292
+#963 := [mp #403 #962]: #958
+#859 := (not #958)
+#861 := (or #859 #866)
+#657 := (>= 0::Int 0::Int)
+#871 := (not #657)
+#875 := (= 0::Int #869)
+#865 := (or #875 #871)
+#500 := (or #859 #865)
+#862 := (iff #500 #861)
+#863 := (iff #861 #861)
+#849 := [rewrite]: #863
+#858 := (iff #865 #866)
+#854 := (or #866 false)
+#857 := (iff #854 #866)
+#852 := [rewrite]: #857
+#855 := (iff #865 #854)
+#516 := (iff #871 false)
+#1 := true
+#509 := (not true)
+#514 := (iff #509 false)
+#515 := [rewrite]: #514
+#851 := (iff #871 #509)
+#525 := (iff #657 true)
+#867 := [rewrite]: #525
+#513 := [monotonicity #867]: #851
+#853 := [trans #513 #515]: #516
+#524 := (iff #875 #866)
+#529 := [rewrite]: #524
+#856 := [monotonicity #529 #853]: #855
+#495 := [trans #856 #852]: #858
+#860 := [monotonicity #495]: #862
+#850 := [trans #860 #849]: #862
+#501 := [quant-inst #47]: #500
+#557 := [mp #501 #850]: #861
+#682 := [unit-resolution #557 #963]: #866
+#684 := (= #847 #869)
+#86 := (= #85 #48)
+#210 := (= #48 #85)
+#212 := (iff #86 #210)
+#213 := [rewrite]: #212
+#209 := [asserted]: #86
+#216 := [mp #209 #213]: #210
+#683 := [symm #216]: #86
+#685 := [monotonicity #683]: #684
+#686 := [trans #685 #682]: #813
+#687 := (not #813)
+#688 := (or #687 #815)
+#689 := [th-lemma arith triangle-eq]: #688
+#690 := [unit-resolution #689 #686]: #815
+#816 := (>= #847 0::Int)
+#691 := (or #687 #816)
+#676 := [th-lemma arith triangle-eq]: #691
+#692 := [unit-resolution #676 #686]: #816
+#654 := [th-lemma arith eq-propagate -1 -1 #692 #690]: #653
+#645 := [symm #654]: #644
+#673 := (= #836 1::Int)
+#817 := (<= #830 0::Int)
+#814 := (= #830 0::Int)
+#663 := (= #830 #869)
+#84 := (= #83 #48)
+#205 := (= #48 #83)
+#207 := (iff #84 #205)
+#208 := [rewrite]: #207
+#204 := [asserted]: #84
+#211 := [mp #204 #208]: #205
+#661 := [symm #211]: #84
+#664 := [monotonicity #661]: #663
+#665 := [trans #664 #682]: #814
+#667 := (not #814)
+#668 := (or #667 #817)
+#669 := [th-lemma arith triangle-eq]: #668
+#670 := [unit-resolution #669 #665]: #817
+#699 := (>= #830 0::Int)
+#671 := (or #667 #699)
+#672 := [th-lemma arith triangle-eq]: #671
+#655 := [unit-resolution #672 #665]: #699
+#643 := [th-lemma arith eq-propagate -1 -1 #655 #670]: #673
+#648 := [trans #643 #645]: #646
+#652 := [monotonicity #648]: #647
+#642 := (= #101 #679)
+decl f11 :: (-> Int S6 S6)
+#548 := (f11 3::Int f12)
+#834 := (f15 #548)
+#821 := (= #834 #679)
+#822 := (= #679 #834)
+#34 := (:var 0 S6)
+#56 := (:var 1 Int)
+#57 := (f11 #56 #34)
+#936 := (pattern #57)
+#36 := (f15 #34)
+#88 := (f21 #36)
+#219 := (+ 1::Int #88)
+#224 := (f18 f19 #219)
+#87 := (f15 #57)
+#227 := (= #87 #224)
+#937 := (forall (vars (?v0 Int) (?v1 S6)) (:pat #936) #227)
+#230 := (forall (vars (?v0 Int) (?v1 S6)) #227)
+#940 := (iff #230 #937)
+#938 := (iff #227 #227)
+#939 := [refl]: #938
+#941 := [quant-intro #939]: #940
+#364 := (~ #230 #230)
+#398 := (~ #227 #227)
+#399 := [refl]: #398
+#365 := [nnf-pos #399]: #364
+#89 := (+ #88 #65)
+#90 := (f18 f19 #89)
+#91 := (= #87 #90)
+#92 := (forall (vars (?v0 Int) (?v1 S6)) #91)
+#231 := (iff #92 #230)
+#228 := (iff #91 #227)
+#225 := (= #90 #224)
+#222 := (= #89 #219)
+#215 := (+ #88 1::Int)
+#220 := (= #215 #219)
+#221 := [rewrite]: #220
+#217 := (= #89 #215)
+#218 := [monotonicity #167]: #217
+#223 := [trans #218 #221]: #222
+#226 := [monotonicity #223]: #225
+#229 := [monotonicity #226]: #228
+#232 := [quant-intro #229]: #231
+#214 := [asserted]: #92
+#235 := [mp #214 #232]: #230
+#368 := [mp~ #235 #365]: #230
+#942 := [mp #368 #941]: #937
+#818 := (not #937)
+#819 := (or #818 #822)
+#825 := (or #818 #821)
+#820 := (iff #825 #819)
+#656 := (iff #819 #819)
+#658 := [rewrite]: #656
+#823 := (iff #821 #822)
+#824 := [rewrite]: #823
+#827 := [monotonicity #824]: #820
+#659 := [trans #827 #658]: #820
+#826 := [quant-inst #99 #19]: #825
+#812 := [mp #826 #659]: #819
+#649 := [unit-resolution #812 #942]: #822
+#651 := [symm #649]: #821
+#641 := (= #101 #834)
+decl f10 :: (-> S6 S3)
+#539 := (f10 #548)
+#835 := (= #539 #834)
+#893 := (pattern #36)
+#35 := (f10 #34)
+#892 := (pattern #35)
+#37 := (= #35 #36)
+#894 := (forall (vars (?v0 S6)) (:pat #892 #893) #37)
+#38 := (forall (vars (?v0 S6)) #37)
+#897 := (iff #38 #894)
+#895 := (iff #37 #37)
+#896 := [refl]: #895
+#898 := [quant-intro #896]: #897
+#344 := (~ #38 #38)
+#388 := (~ #37 #37)
+#389 := [refl]: #388
+#345 := [nnf-pos #389]: #344
+#153 := [asserted]: #38
+#352 := [mp~ #153 #345]: #38
+#899 := [mp #352 #898]: #894
+#864 := (not #894)
+#677 := (or #864 #835)
+#678 := [quant-inst #548]: #677
+#650 := [unit-resolution #678 #899]: #835
+#549 := (= #101 #539)
+#20 := (f11 #16 f12)
+#885 := (pattern #20)
+#17 := (f9 #16)
+#884 := (pattern #17)
+#21 := (f10 #20)
+#18 := (f8 #17)
+#22 := (= #18 #21)
+#886 := (forall (vars (?v0 Int)) (:pat #884 #885) #22)
+#23 := (forall (vars (?v0 Int)) #22)
+#889 := (iff #23 #886)
+#887 := (iff #22 #22)
+#888 := [refl]: #887
+#890 := [quant-intro #888]: #889
+#342 := (~ #23 #23)
+#341 := (~ #22 #22)
+#386 := [refl]: #341
+#343 := [nnf-pos #386]: #342
+#141 := [asserted]: #23
+#387 := [mp~ #141 #343]: #23
+#891 := [mp #387 #890]: #886
+#868 := (not #886)
+#870 := (or #868 #549)
+#526 := [quant-inst #99]: #870
+#492 := [unit-resolution #526 #891]: #549
+#639 := [trans #492 #650]: #641
+#630 := [trans #639 #651]: #642
+#635 := [trans #630 #652]: #633
+#632 := [trans #635 #681]: #636
+#627 := [trans #632 #634]: #637
+#617 := [trans #627 #640]: #104
+#105 := (not #104)
+#252 := [asserted]: #105
+[unit-resolution #252 #617]: false
+unsat

--- a/src/HOL/SMT_Examples/SMT_Tests.certs	Wed Jun 08 11:59:45 2011 +0200
+++ b/src/HOL/SMT_Examples/SMT_Tests.certs	Wed Jun 08 13:43:15 2011 +0200
@@ -50037,7 +50037,7 @@
 #87 := [and-elim #86]: #46
 [th-lemma arith farkas 1 1 1 #87 #88 #89]: false
 unsat
-267c94908fa1cba1e9bb1ecaaa4c65058e972cc1 43 0
+df4ce8c591cd4d3dc5b57ede848dc6285f8d31c0 43 0
 #2 := false
 decl f3 :: (-> S3 S2)
 decl f4 :: (-> S2 S2 S3)
@@ -50062,10 +50062,10 @@
 #566 := (iff #49 #49)
 #567 := [refl]: #566
 #569 := [quant-intro #567]: #568
-#76 := (~ #52 #52)
-#83 := (~ #49 #49)
-#84 := [refl]: #83
-#77 := [nnf-pos #84]: #76
+#86 := (~ #52 #52)
+#84 := (~ #49 #49)
+#85 := [refl]: #84
+#87 := [nnf-pos #85]: #86
 #12 := (= #11 #8)
 #13 := (forall (vars (?v0 S2) (?v1 S2)) #12)
 #53 := (iff #13 #52)
@@ -50074,14 +50074,14 @@
 #54 := [quant-intro #51]: #53
 #48 := [asserted]: #13
 #57 := [mp #48 #54]: #52
-#78 := [mp~ #57 #77]: #52
-#570 := [mp #78 #569]: #565
+#74 := [mp~ #57 #87]: #52
+#570 := [mp #74 #569]: #565
 #147 := (not #565)
 #234 := (or #147 #27)
 #148 := [quant-inst #23 #24]: #234
 [unit-resolution #148 #570 #71]: false
 unsat
-eba38932115d0bb0963b99e993a7e1b0dfff5581 43 0
+7eae83a754ae3930b3797f3d00ee6d160a313dd5 43 0
 #2 := false
 decl f5 :: (-> S3 S2)
 decl f4 :: (-> S2 S2 S3)
@@ -50106,10 +50106,10 @@
 #572 := (iff #56 #56)
 #573 := [refl]: #572
 #575 := [quant-intro #573]: #574
-#85 := (~ #60 #60)
-#81 := (~ #56 #56)
-#82 := [refl]: #81
-#86 := [nnf-pos #82]: #85
+#76 := (~ #60 #60)
+#75 := (~ #56 #56)
+#88 := [refl]: #75
+#77 := [nnf-pos #88]: #76
 #15 := (= #14 #9)
 #16 := (forall (vars (?v0 S2) (?v1 S2)) #15)
 #61 := (iff #16 #60)
@@ -50118,8 +50118,8 @@
 #62 := [quant-intro #59]: #61
 #55 := [asserted]: #16
 #65 := [mp #55 #62]: #60
-#87 := [mp~ #65 #86]: #60
-#576 := [mp #87 #575]: #571
+#89 := [mp~ #65 #77]: #60
+#576 := [mp #89 #575]: #571
 #237 := (not #571)
 #238 := (or #237 #27)
 #166 := [quant-inst #24 #23]: #238
@@ -50367,68 +50367,68 @@
 #266 := [def-axiom]: #179
 [unit-resolution #266 #292 #218 #572]: false
 unsat
-39134e03a4a206aeb5e8ee58e8edb86a602fc708 91 0
+f40f3c3663b225f69de5b154d25c78946af8135f 91 0
 #2 := false
 decl f12 :: S2
 #42 := f12
 decl f9 :: S2
 #36 := f9
 #49 := (= f9 f12)
-decl f3 :: (-> S4 S2)
+decl f5 :: (-> S5 S2)
+decl f6 :: (-> S2 S4 S5)
 decl f4 :: (-> S2 S3 S4)
-decl f6 :: (-> S2 S5 S3)
-decl f14 :: S5
+decl f14 :: S3
 #44 := f14
 decl f13 :: S2
 #43 := f13
-#45 := (f6 f13 f14)
-#46 := (f4 f12 #45)
-#47 := (f3 #46)
-decl f11 :: S5
+#45 := (f4 f13 f14)
+#46 := (f6 f12 #45)
+#47 := (f5 #46)
+decl f11 :: S3
 #38 := f11
 decl f10 :: S2
 #37 := f10
-#39 := (f6 f10 f11)
-#40 := (f4 f9 #39)
-#41 := (f3 #40)
+#39 := (f4 f10 f11)
+#40 := (f6 f9 #39)
+#41 := (f5 #40)
 #48 := (= #41 #47)
 #50 := (iff #48 #49)
 #327 := (iff #49 #48)
-#280 := (= f12 #47)
-#9 := (:var 0 S3)
+#606 := (= f12 #47)
+#14 := (:var 0 S4)
 #8 := (:var 1 S2)
-#10 := (f4 #8 #9)
-#631 := (pattern #10)
-#11 := (f3 #10)
-#72 := (= #8 #11)
-#632 := (forall (vars (?v0 S2) (?v1 S3)) (:pat #631) #72)
-#75 := (forall (vars (?v0 S2) (?v1 S3)) #72)
-#635 := (iff #75 #632)
-#633 := (iff #72 #72)
-#634 := [refl]: #633
-#636 := [quant-intro #634]: #635
-#128 := (~ #75 #75)
-#139 := (~ #72 #72)
-#140 := [refl]: #139
-#129 := [nnf-pos #140]: #128
-#12 := (= #11 #8)
-#13 := (forall (vars (?v0 S2) (?v1 S3)) #12)
-#76 := (iff #13 #75)
-#73 := (iff #12 #72)
-#74 := [rewrite]: #73
-#77 := [quant-intro #74]: #76
-#71 := [asserted]: #13
-#80 := [mp #71 #77]: #75
-#132 := [mp~ #80 #129]: #75
-#637 := [mp #132 #636]: #632
-#286 := (not #632)
-#627 := (or #286 #280)
-#628 := [quant-inst #42 #45]: #627
-#605 := [unit-resolution #628 #637]: #280
-#306 := (= f9 #41)
-#623 := (or #286 #306)
-#625 := [quant-inst #36 #39]: #623
-#311 := [unit-resolution #625 #637]: #306
+#15 := (f6 #8 #14)
+#638 := (pattern #15)
+#16 := (f5 #15)
+#79 := (= #8 #16)
+#639 := (forall (vars (?v0 S2) (?v1 S4)) (:pat #638) #79)
+#83 := (forall (vars (?v0 S2) (?v1 S4)) #79)
+#642 := (iff #83 #639)
+#640 := (iff #79 #79)
+#641 := [refl]: #640
+#643 := [quant-intro #641]: #642
+#128 := (~ #83 #83)
+#127 := (~ #79 #79)
+#146 := [refl]: #127
+#129 := [nnf-pos #146]: #128
+#17 := (= #16 #8)
+#18 := (forall (vars (?v0 S2) (?v1 S4)) #17)
+#84 := (iff #18 #83)
+#81 := (iff #17 #79)
+#82 := [rewrite]: #81
+#85 := [quant-intro #82]: #84
+#78 := [asserted]: #18
+#88 := [mp #78 #85]: #83
+#147 := [mp~ #88 #129]: #83
+#644 := [mp #147 #643]: #639
+#279 := (not #639)
+#609 := (or #279 #606)
+#610 := [quant-inst #42 #45]: #609
+#605 := [unit-resolution #610 #644]: #606
+#630 := (= f9 #41)
+#622 := (or #279 #630)
+#263 := [quant-inst #36 #39]: #622
+#311 := [unit-resolution #263 #644]: #630
 #328 := [monotonicity #311 #605]: #327
 #329 := [symm #328]: #50
 #302 := (not #49)
@@ -50459,74 +50459,74 @@
 #323 := [unit-resolution #233 #601]: #302
 [unit-resolution #323 #324]: false
 unsat
-f188cd132a2dfe3292e7656a282b6a08809558ea 210 0
+21be96a84939ebc40a46fc69c9c8174cc17510e4 210 0
 #2 := false
 decl f14 :: S5
 #44 := f14
 decl f11 :: S5
 #38 := f11
 #50 := (= f11 f14)
-#159 := (not #50)
+#163 := (not #50)
 decl f13 :: S2
 #43 := f13
 decl f10 :: S2
 #37 := f10
 #49 := (= f10 f13)
-#158 := (not #49)
-#160 := (or #158 #159)
-decl f7 :: (-> S4 S3)
+#162 := (not #49)
+#140 := (or #162 #163)
+decl f8 :: (-> S4 S3)
 decl f4 :: (-> S2 S3 S4)
 decl f6 :: (-> S2 S5 S3)
 #45 := (f6 f13 f14)
 decl f12 :: S2
 #42 := f12
 #46 := (f4 f12 #45)
-#47 := (f7 #46)
+#47 := (f8 #46)
 #39 := (f6 f10 f11)
 decl f9 :: S2
 #36 := f9
 #40 := (f4 f9 #39)
-#41 := (f7 #40)
+#41 := (f8 #40)
 #48 := (= #41 #47)
 #652 := (= #45 #47)
 #9 := (:var 0 S3)
 #8 := (:var 1 S2)
 #10 := (f4 #8 #9)
 #653 := (pattern #10)
-#19 := (f7 #10)
-#89 := (= #9 #19)
-#667 := (forall (vars (?v0 S2) (?v1 S3)) (:pat #653) #89)
-#93 := (forall (vars (?v0 S2) (?v1 S3)) #89)
-#670 := (iff #93 #667)
-#668 := (iff #89 #89)
-#669 := [refl]: #668
-#671 := [quant-intro #669]: #670
-#152 := (~ #93 #93)
-#150 := (~ #89 #89)
-#151 := [refl]: #150
-#153 := [nnf-pos #151]: #152
-#20 := (= #19 #9)
-#21 := (forall (vars (?v0 S2) (?v1 S3)) #20)
-#94 := (iff #21 #93)
-#91 := (iff #20 #89)
-#92 := [rewrite]: #91
-#95 := [quant-intro #92]: #94
-#88 := [asserted]: #21
-#98 := [mp #88 #95]: #93
-#154 := [mp~ #98 #153]: #93
-#672 := [mp #154 #671]: #667
-#650 := (not #667)
+#22 := (f8 #10)
+#97 := (= #9 #22)
+#673 := (forall (vars (?v0 S2) (?v1 S3)) (:pat #653) #97)
+#101 := (forall (vars (?v0 S2) (?v1 S3)) #97)
+#676 := (iff #101 #673)
+#674 := (iff #97 #97)
+#675 := [refl]: #674
+#677 := [quant-intro #675]: #676
+#134 := (~ #101 #101)
+#153 := (~ #97 #97)
+#154 := [refl]: #153
+#135 := [nnf-pos #154]: #134
+#23 := (= #22 #9)
+#24 := (forall (vars (?v0 S2) (?v1 S3)) #23)
+#102 := (iff #24 #101)
+#99 := (iff #23 #97)
+#100 := [rewrite]: #99
+#103 := [quant-intro #100]: #102
+#96 := [asserted]: #24
+#106 := [mp #96 #103]: #101
+#155 := [mp~ #106 #135]: #101
+#678 := [mp #155 #677]: #673
+#650 := (not #673)
 #301 := (or #650 #652)
 #644 := [quant-inst #42 #45]: #301
-#337 := [unit-resolution #644 #672]: #652
+#337 := [unit-resolution #644 #678]: #652
 #624 := (= #41 #45)
 #346 := (= #39 #45)
-#161 := (not #160)
-#333 := [hypothesis]: #161
-#236 := (or #160 #50)
+#141 := (not #140)
+#333 := [hypothesis]: #141
+#236 := (or #140 #50)
 #323 := [def-axiom]: #236
 #352 := [unit-resolution #323 #333]: #50
-#235 := (or #160 #49)
+#235 := (or #140 #49)
 #322 := [def-axiom]: #235
 #243 := [unit-resolution #322 #333]: #49
 #620 := [monotonicity #243 #352]: #346
@@ -50534,27 +50534,27 @@
 #434 := (= #39 #41)
 #651 := (or #650 #434)
 #646 := [quant-inst #36 #39]: #651
-#622 := [unit-resolution #646 #672]: #434
+#622 := [unit-resolution #646 #678]: #434
 #345 := [symm #622]: #623
 #621 := [trans #345 #620]: #624
 #625 := [trans #621 #337]: #48
 #121 := (not #48)
-#308 := (or #121 #160)
-#172 := (iff #48 #160)
+#308 := (or #121 #140)
+#172 := (iff #48 #140)
 #51 := (and #49 #50)
 #123 := (iff #51 #121)
 #175 := (iff #123 #172)
-#167 := (iff #160 #48)
+#167 := (iff #140 #48)
 #173 := (iff #167 #172)
 #174 := [rewrite]: #173
 #170 := (iff #123 #167)
-#164 := (iff #161 #121)
+#164 := (iff #141 #121)
 #168 := (iff #164 #167)
 #169 := [rewrite]: #168
 #165 := (iff #123 #164)
-#162 := (iff #51 #161)
-#163 := [rewrite]: #162
-#166 := [monotonicity #163]: #165
+#142 := (iff #51 #141)
+#143 := [rewrite]: #142
+#166 := [monotonicity #143]: #165
 #171 := [trans #166 #169]: #170
 #176 := [trans #171 #174]: #175
 #52 := (iff #48 #51)
@@ -50565,12 +50565,12 @@
 #128 := [mp #120 #125]: #123
 #177 := [mp #128 #176]: #172
 #315 := (not #172)
-#325 := (or #121 #160 #315)
+#325 := (or #121 #140 #315)
 #329 := [def-axiom]: #325
 #645 := [unit-resolution #329 #177]: #308
 #349 := [unit-resolution #645 #333]: #121
 #334 := [unit-resolution #349 #625]: false
-#335 := [lemma #334]: #160
+#335 := [lemma #334]: #140
 decl f5 :: (-> S3 S2)
 #292 := (f5 #45)
 #609 := (= #292 f13)
@@ -50586,10 +50586,10 @@
 #662 := (iff #81 #81)
 #663 := [refl]: #662
 #665 := [quant-intro #663]: #664
-#145 := (~ #85 #85)
-#139 := (~ #81 #81)
-#140 := [refl]: #139
-#146 := [nnf-pos #140]: #145
+#130 := (~ #85 #85)
+#129 := (~ #81 #81)
+#148 := [refl]: #129
+#131 := [nnf-pos #148]: #130
 #17 := (= #16 #8)
 #18 := (forall (vars (?v0 S2) (?v1 S5)) #17)
 #86 := (iff #18 #85)
@@ -50598,8 +50598,8 @@
 #87 := [quant-intro #84]: #86
 #80 := [asserted]: #18
 #90 := [mp #80 #87]: #85
-#147 := [mp~ #90 #146]: #85
-#666 := [mp #147 #665]: #661
+#149 := [mp~ #90 #131]: #85
+#666 := [mp #149 #665]: #661
 #289 := (not #661)
 #635 := (or #289 #630)
 #271 := [quant-inst #43 #44]: #635
@@ -50611,8 +50611,8 @@
 #616 := (= #47 #45)
 #617 := [symm #337]: #616
 #330 := (= #39 #47)
-#255 := (or #48 #161)
-#326 := (or #48 #161 #315)
+#255 := (or #48 #141)
+#326 := (or #48 #141 #315)
 #327 := [def-axiom]: #326
 #328 := [unit-resolution #327 #177]: #255
 #338 := [unit-resolution #328 #335]: #48
@@ -50625,52 +50625,52 @@
 #615 := [unit-resolution #291 #666]: #643
 #606 := [trans #615 #608]: #605
 #611 := [trans #606 #610]: #49
-decl f8 :: (-> S3 S5)
-#634 := (f8 #45)
+decl f7 :: (-> S3 S5)
+#634 := (f7 #45)
 #455 := (= #634 f14)
 #629 := (= f14 #634)
-#22 := (f8 #15)
-#97 := (= #14 #22)
-#673 := (forall (vars (?v0 S2) (?v1 S5)) (:pat #660) #97)
-#101 := (forall (vars (?v0 S2) (?v1 S5)) #97)
-#676 := (iff #101 #673)
-#674 := (iff #97 #97)
-#675 := [refl]: #674
-#677 := [quant-intro #675]: #676
-#143 := (~ #101 #101)
-#148 := (~ #97 #97)
-#149 := [refl]: #148
-#144 := [nnf-pos #149]: #143
-#23 := (= #22 #14)
-#24 := (forall (vars (?v0 S2) (?v1 S5)) #23)
-#102 := (iff #24 #101)
-#99 := (iff #23 #97)
-#100 := [rewrite]: #99
-#103 := [quant-intro #100]: #102
-#96 := [asserted]: #24
-#106 := [mp #96 #103]: #101
-#155 := [mp~ #106 #144]: #101
-#678 := [mp #155 #677]: #673
-#631 := (not #673)
+#19 := (f7 #15)
+#89 := (= #14 #19)
+#667 := (forall (vars (?v0 S2) (?v1 S5)) (:pat #660) #89)
+#93 := (forall (vars (?v0 S2) (?v1 S5)) #89)
+#670 := (iff #93 #667)
+#668 := (iff #89 #89)
+#669 := [refl]: #668
+#671 := [quant-intro #669]: #670
+#132 := (~ #93 #93)
+#150 := (~ #89 #89)
+#151 := [refl]: #150
+#133 := [nnf-pos #151]: #132
+#20 := (= #19 #14)
+#21 := (forall (vars (?v0 S2) (?v1 S5)) #20)
+#94 := (iff #21 #93)
+#91 := (iff #20 #89)
+#92 := [rewrite]: #91
+#95 := [quant-intro #92]: #94
+#88 := [asserted]: #21
+#98 := [mp #88 #95]: #93
+#152 := [mp~ #98 #133]: #93
+#672 := [mp #152 #671]: #667
+#631 := (not #667)
 #276 := (or #631 #629)
 #277 := [quant-inst #43 #44]: #276
-#612 := [unit-resolution #277 #678]: #629
+#612 := [unit-resolution #277 #672]: #629
 #456 := [symm #612]: #455
 #598 := (= f11 #634)
-#285 := (f8 #39)
+#285 := (f7 #39)
 #613 := (= #285 #634)
 #454 := [monotonicity #618]: #613
 #628 := (= f11 #285)
 #632 := (or #631 #628)
 #633 := [quant-inst #37 #38]: #632
-#607 := [unit-resolution #633 #678]: #628
+#607 := [unit-resolution #633 #672]: #628
 #599 := [trans #607 #454]: #598
 #600 := [trans #599 #456]: #50
-#237 := (or #161 #158 #159)
+#237 := (or #141 #162 #163)
 #324 := [def-axiom]: #237
 [unit-resolution #324 #600 #611 #335]: false
 unsat
-bb6d90f8a24326b7dc1b50e80f594ff94486f0cc 144 0
+67dcdd8ec04ec052a954041c9287b8a81ea9bcac 144 0
 #2 := false
 decl f13 :: S2
 #44 := f13
@@ -50678,7 +50678,7 @@
 #37 := f10
 #51 := (= f10 f13)
 decl f5 :: (-> S3 S2)
-decl f7 :: (-> S4 S3)
+decl f8 :: (-> S4 S3)
 decl f4 :: (-> S2 S3 S4)
 decl f6 :: (-> S2 S5 S3)
 decl f14 :: S5
@@ -50687,7 +50687,7 @@
 decl f12 :: S2
 #43 := f12
 #47 := (f4 f12 #46)
-#48 := (f7 #47)
+#48 := (f8 #47)
 #49 := (f5 #48)
 decl f11 :: S5
 #38 := f11
@@ -50695,7 +50695,7 @@
 decl f9 :: S2
 #36 := f9
 #40 := (f4 f9 #39)
-#41 := (f7 #40)
+#41 := (f8 #40)
 #42 := (f5 #41)
 #50 := (= #42 #49)
 #52 := (iff #50 #51)
@@ -50715,10 +50715,10 @@
 #642 := (iff #81 #81)
 #643 := [refl]: #642
 #645 := [quant-intro #643]: #644
-#133 := (~ #85 #85)
-#138 := (~ #81 #81)
-#132 := [refl]: #138
-#134 := [nnf-pos #132]: #133
+#130 := (~ #85 #85)
+#129 := (~ #81 #81)
+#148 := [refl]: #129
+#131 := [nnf-pos #148]: #130
 #17 := (= #16 #8)
 #18 := (forall (vars (?v0 S2) (?v1 S5)) #17)
 #86 := (iff #18 #85)
@@ -50727,8 +50727,8 @@
 #87 := [quant-intro #84]: #86
 #80 := [asserted]: #18
 #90 := [mp #80 #87]: #85
-#135 := [mp~ #90 #134]: #85
-#646 := [mp #135 #645]: #641
+#149 := [mp~ #90 #131]: #85
+#646 := [mp #149 #645]: #641
 #623 := (not #641)
 #611 := (or #623 #608)
 #612 := [quant-inst #44 #45]: #611
@@ -50740,32 +50740,32 @@
 #9 := (:var 0 S3)
 #10 := (f4 #8 #9)
 #633 := (pattern #10)
-#19 := (f7 #10)
-#89 := (= #9 #19)
-#647 := (forall (vars (?v0 S2) (?v1 S3)) (:pat #633) #89)
-#93 := (forall (vars (?v0 S2) (?v1 S3)) #89)
-#650 := (iff #93 #647)
-#648 := (iff #89 #89)
-#649 := [refl]: #648
-#651 := [quant-intro #649]: #650
-#142 := (~ #93 #93)
-#136 := (~ #89 #89)
-#141 := [refl]: #136
-#143 := [nnf-pos #141]: #142
-#20 := (= #19 #9)
-#21 := (forall (vars (?v0 S2) (?v1 S3)) #20)
-#94 := (iff #21 #93)
-#91 := (iff #20 #89)
-#92 := [rewrite]: #91
-#95 := [quant-intro #92]: #94
-#88 := [asserted]: #21
-#98 := [mp #88 #95]: #93
-#148 := [mp~ #98 #143]: #93
-#652 := [mp #148 #651]: #647
-#621 := (not #647)
+#22 := (f8 #10)
+#97 := (= #9 #22)
+#653 := (forall (vars (?v0 S2) (?v1 S3)) (:pat #633) #97)
+#101 := (forall (vars (?v0 S2) (?v1 S3)) #97)
+#656 := (iff #101 #653)
+#654 := (iff #97 #97)
+#655 := [refl]: #654
+#657 := [quant-intro #655]: #656
+#134 := (~ #101 #101)
+#153 := (~ #97 #97)
+#154 := [refl]: #153
+#135 := [nnf-pos #154]: #134
+#23 := (= #22 #9)
+#24 := (forall (vars (?v0 S2) (?v1 S3)) #23)
+#102 := (iff #24 #101)
+#99 := (iff #23 #97)
+#100 := [rewrite]: #99
+#103 := [quant-intro #100]: #102
+#96 := [asserted]: #24
+#106 := [mp #96 #103]: #101
+#155 := [mp~ #106 #135]: #101
+#658 := [mp #155 #657]: #653
+#621 := (not #653)
 #632 := (or #621 #628)
 #622 := [quant-inst #43 #46]: #632
-#600 := [unit-resolution #622 #652]: #628
+#600 := [unit-resolution #622 #658]: #628
 #601 := [symm #600]: #604
 #314 := [monotonicity #601]: #605
 #596 := [trans #314 #316]: #318
@@ -50782,7 +50782,7 @@
 #309 := (= #39 #41)
 #293 := (or #621 #309)
 #294 := [quant-inst #36 #39]: #293
-#310 := [unit-resolution #294 #652]: #309
+#310 := [unit-resolution #294 #658]: #309
 #598 := [symm #310]: #594
 #599 := [monotonicity #598]: #595
 #585 := [trans #599 #589]: #590
@@ -50815,15 +50815,15 @@
 #435 := [unit-resolution #235 #434]: #304
 [unit-resolution #435 #436]: false
 unsat
-ff464dff75d057630c9c6f2ae16d33617edf611b 144 0
+f039385411d77981082c23334b58503acb7a1eee 144 0
 #2 := false
 decl f14 :: S5
 #45 := f14
 decl f11 :: S5
 #38 := f11
 #51 := (= f11 f14)
-decl f8 :: (-> S3 S5)
-decl f7 :: (-> S4 S3)
+decl f7 :: (-> S3 S5)
+decl f8 :: (-> S4 S3)
 decl f4 :: (-> S2 S3 S4)
 decl f6 :: (-> S2 S5 S3)
 decl f13 :: S2
@@ -50832,52 +50832,52 @@
 decl f12 :: S2
 #43 := f12
 #47 := (f4 f12 #46)
-#48 := (f7 #47)
-#49 := (f8 #48)
+#48 := (f8 #47)
+#49 := (f7 #48)
 decl f10 :: S2
 #37 := f10
 #39 := (f6 f10 f11)
 decl f9 :: S2
 #36 := f9
 #40 := (f4 f9 #39)
-#41 := (f7 #40)
-#42 := (f8 #41)
+#41 := (f8 #40)
+#42 := (f7 #41)
 #50 := (= #42 #49)
 #52 := (iff #50 #51)
 #318 := (= #49 f14)
-#272 := (f8 #46)
+#272 := (f7 #46)
 #315 := (= #272 f14)
 #610 := (= f14 #272)
 #14 := (:var 0 S5)
 #8 := (:var 1 S2)
 #15 := (f6 #8 #14)
 #640 := (pattern #15)
-#22 := (f8 #15)
-#97 := (= #14 #22)
-#653 := (forall (vars (?v0 S2) (?v1 S5)) (:pat #640) #97)
-#101 := (forall (vars (?v0 S2) (?v1 S5)) #97)
-#656 := (iff #101 #653)
-#654 := (iff #97 #97)
-#655 := [refl]: #654
-#657 := [quant-intro #655]: #656
-#151 := (~ #101 #101)
-#149 := (~ #97 #97)
-#150 := [refl]: #149
-#152 := [nnf-pos #150]: #151
-#23 := (= #22 #14)
-#24 := (forall (vars (?v0 S2) (?v1 S5)) #23)
-#102 := (iff #24 #101)
-#99 := (iff #23 #97)
-#100 := [rewrite]: #99
-#103 := [quant-intro #100]: #102
-#96 := [asserted]: #24
-#106 := [mp #96 #103]: #101
-#153 := [mp~ #106 #152]: #101
-#658 := [mp #153 #657]: #653
-#269 := (not #653)
+#19 := (f7 #15)
+#89 := (= #14 #19)
+#647 := (forall (vars (?v0 S2) (?v1 S5)) (:pat #640) #89)
+#93 := (forall (vars (?v0 S2) (?v1 S5)) #89)
+#650 := (iff #93 #647)
+#648 := (iff #89 #89)
+#649 := [refl]: #648
+#651 := [quant-intro #649]: #650
+#132 := (~ #93 #93)
+#150 := (~ #89 #89)
+#151 := [refl]: #150
+#133 := [nnf-pos #151]: #132
+#20 := (= #19 #14)
+#21 := (forall (vars (?v0 S2) (?v1 S5)) #20)
+#94 := (iff #21 #93)
+#91 := (iff #20 #89)
+#92 := [rewrite]: #91
+#95 := [quant-intro #92]: #94
+#88 := [asserted]: #21
+#98 := [mp #88 #95]: #93
+#152 := [mp~ #98 #133]: #93
+#652 := [mp #152 #651]: #647
+#269 := (not #647)
 #609 := (or #269 #610)
 #615 := [quant-inst #44 #45]: #609
-#326 := [unit-resolution #615 #658]: #610
+#326 := [unit-resolution #615 #652]: #610
 #316 := [symm #326]: #315
 #605 := (= #49 #272)
 #604 := (= #48 #46)
@@ -50885,49 +50885,49 @@
 #9 := (:var 0 S3)
 #10 := (f4 #8 #9)
 #633 := (pattern #10)
-#19 := (f7 #10)
-#89 := (= #9 #19)
-#647 := (forall (vars (?v0 S2) (?v1 S3)) (:pat #633) #89)
-#93 := (forall (vars (?v0 S2) (?v1 S3)) #89)
-#650 := (iff #93 #647)
-#648 := (iff #89 #89)
-#649 := [refl]: #648
-#651 := [quant-intro #649]: #650
-#142 := (~ #93 #93)
-#140 := (~ #89 #89)
-#141 := [refl]: #140
-#143 := [nnf-pos #141]: #142
-#20 := (= #19 #9)
-#21 := (forall (vars (?v0 S2) (?v1 S3)) #20)
-#94 := (iff #21 #93)
-#91 := (iff #20 #89)
-#92 := [rewrite]: #91
-#95 := [quant-intro #92]: #94
-#88 := [asserted]: #21
-#98 := [mp #88 #95]: #93
-#148 := [mp~ #98 #143]: #93
-#652 := [mp #148 #651]: #647
-#621 := (not #647)
+#22 := (f8 #10)
+#97 := (= #9 #22)
+#653 := (forall (vars (?v0 S2) (?v1 S3)) (:pat #633) #97)
+#101 := (forall (vars (?v0 S2) (?v1 S3)) #97)
+#656 := (iff #101 #653)
+#654 := (iff #97 #97)
+#655 := [refl]: #654
+#657 := [quant-intro #655]: #656
+#134 := (~ #101 #101)
+#153 := (~ #97 #97)
+#154 := [refl]: #153
+#135 := [nnf-pos #154]: #134
+#23 := (= #22 #9)
+#24 := (forall (vars (?v0 S2) (?v1 S3)) #23)
+#102 := (iff #24 #101)
+#99 := (iff #23 #97)
+#100 := [rewrite]: #99
+#103 := [quant-intro #100]: #102
+#96 := [asserted]: #24
+#106 := [mp #96 #103]: #101
+#155 := [mp~ #106 #135]: #101
+#658 := [mp #155 #657]: #653
+#621 := (not #653)
 #632 := (or #621 #628)
 #622 := [quant-inst #43 #46]: #632
-#600 := [unit-resolution #622 #652]: #628
+#600 := [unit-resolution #622 #658]: #628
 #601 := [symm #600]: #604
 #314 := [monotonicity #601]: #605
 #596 := [trans #314 #316]: #318
 #590 := (= #42 f11)
-#280 := (f8 #39)
+#280 := (f7 #39)
 #588 := (= #280 f11)
 #285 := (= f11 #280)
 #270 := (or #269 #285)
 #271 := [quant-inst #37 #38]: #270
-#597 := [unit-resolution #271 #658]: #285
+#597 := [unit-resolution #271 #652]: #285
 #589 := [symm #597]: #588
 #595 := (= #42 #280)
 #594 := (= #41 #39)
 #309 := (= #39 #41)
 #293 := (or #621 #309)
 #294 := [quant-inst #36 #39]: #293
-#310 := [unit-resolution #294 #652]: #309
+#310 := [unit-resolution #294 #658]: #309
 #598 := [symm #310]: #594
 #599 := [monotonicity #598]: #595
 #585 := [trans #599 #589]: #590
@@ -50960,7 +50960,7 @@
 #435 := [unit-resolution #235 #434]: #304
 [unit-resolution #435 #436]: false
 unsat
-c3d12f254b9672d4ea71a3aff4f3729162212903 103 0
+20f57d480df22411665e8be01511bda0544a754c 103 0
 #2 := false
 decl f7 :: S2
 #24 := f7
@@ -50989,10 +50989,10 @@
 #580 := (iff #59 #59)
 #581 := [refl]: #580
 #583 := [quant-intro #581]: #582
-#87 := (~ #63 #63)
-#85 := (~ #59 #59)
-#86 := [refl]: #85
-#88 := [nnf-pos #86]: #87
+#84 := (~ #63 #63)
+#83 := (~ #59 #59)
+#96 := [refl]: #83
+#85 := [nnf-pos #96]: #84
 #15 := (= #14 #9)
 #16 := (forall (vars (?v0 S2) (?v1 S2)) #15)
 #64 := (iff #16 #63)
@@ -51001,8 +51001,8 @@
 #65 := [quant-intro #62]: #64
 #58 := [asserted]: #16
 #68 := [mp #58 #65]: #63
-#91 := [mp~ #68 #88]: #63
-#584 := [mp #91 #583]: #579
+#97 := [mp~ #68 #85]: #63
+#584 := [mp #97 #583]: #579
 #353 := (not #579)
 #560 := (or #353 #244)
 #232 := [quant-inst #23 #24]: #560
@@ -51016,10 +51016,10 @@
 #574 := (iff #52 #52)
 #575 := [refl]: #574
 #577 := [quant-intro #575]: #576
-#89 := (~ #55 #55)
-#94 := (~ #52 #52)
-#95 := [refl]: #94
-#90 := [nnf-pos #95]: #89
+#94 := (~ #55 #55)
+#92 := (~ #52 #52)
+#93 := [refl]: #92
+#95 := [nnf-pos #93]: #94
 #12 := (= #11 #8)
 #13 := (forall (vars (?v0 S2) (?v1 S2)) #12)
 #56 := (iff #13 #55)
@@ -51028,8 +51028,8 @@
 #57 := [quant-intro #54]: #56
 #51 := [asserted]: #13
 #60 := [mp #51 #57]: #55
-#84 := [mp~ #60 #90]: #55
-#578 := [mp #84 #577]: #573
+#81 := [mp~ #60 #95]: #55
+#578 := [mp #81 #577]: #573
 #227 := (not #573)
 #564 := (or #227 #247)
 #566 := [quant-inst #23 #24]: #564
@@ -51064,7 +51064,7 @@
 #208 := [unit-resolution #174 #547]: #243
 [unit-resolution #208 #209]: false
 unsat
-df71e79ae4d3b6ca6b9e37bd4464bcbb19ac1ad4 111 0
+bf86a55d7b42d914595abb0b42ed4b6837aa227f 111 0
 #2 := false
 decl f5 :: (-> S3 S2)
 decl f9 :: S3
@@ -51117,10 +51117,10 @@
 #593 := (iff #64 #64)
 #594 := [refl]: #593
 #596 := [quant-intro #594]: #595
-#100 := (~ #68 #68)
-#98 := (~ #64 #64)
-#99 := [refl]: #98
-#101 := [nnf-pos #99]: #100
+#97 := (~ #68 #68)
+#96 := (~ #64 #64)
+#113 := [refl]: #96
+#98 := [nnf-pos #113]: #97
 #15 := (= #14 #9)
 #16 := (forall (vars (?v0 S2) (?v1 S2)) #15)
 #69 := (iff #16 #68)
@@ -51129,8 +51129,8 @@
 #70 := [quant-intro #67]: #69
 #63 := [asserted]: #16
 #73 := [mp #63 #70]: #68
-#104 := [mp~ #73 #101]: #68
-#597 := [mp #104 #596]: #592
+#114 := [mp~ #73 #98]: #68
+#597 := [mp #114 #596]: #592
 #187 := (not #592)
 #573 := (or #187 #240)
 #245 := [quant-inst #25 #24]: #573
@@ -51147,10 +51147,10 @@
 #587 := (iff #57 #57)
 #588 := [refl]: #587
 #590 := [quant-intro #588]: #589
-#102 := (~ #60 #60)
-#107 := (~ #57 #57)
-#108 := [refl]: #107
-#103 := [nnf-pos #108]: #102
+#111 := (~ #60 #60)
+#109 := (~ #57 #57)
+#110 := [refl]: #109
+#112 := [nnf-pos #110]: #111
 #12 := (= #11 #8)
 #13 := (forall (vars (?v0 S2) (?v1 S2)) #12)
 #61 := (iff #13 #60)
@@ -51159,8 +51159,8 @@
 #62 := [quant-intro #59]: #61
 #56 := [asserted]: #13
 #65 := [mp #56 #62]: #60
-#97 := [mp~ #65 #103]: #60
-#591 := [mp #97 #590]: #586
+#95 := [mp~ #65 #112]: #60
+#591 := [mp #95 #590]: #586
 #169 := (not #586)
 #256 := (or #169 #254)
 #247 := [quant-inst #24 #25]: #256
@@ -51176,7 +51176,7 @@
 #93 := [not-or-elim #90]: #92
 [unit-resolution #93 #566]: false
 unsat
-e078bb600df2bd0f41e49114d3117704e2a9b9b4 117 0
+bc5180d3ea9553f4ce1005fa76475b6a88104f2a 117 0
 #2 := false
 decl f4 :: (-> S2 S2 S3)
 decl f3 :: (-> S3 S2)
@@ -51206,10 +51206,10 @@
 #573 := (iff #51 #51)
 #574 := [refl]: #573
 #576 := [quant-intro #574]: #575
-#88 := (~ #54 #54)
-#93 := (~ #51 #51)
-#94 := [refl]: #93
-#89 := [nnf-pos #94]: #88
+#93 := (~ #54 #54)
+#91 := (~ #51 #51)
+#92 := [refl]: #91
+#94 := [nnf-pos #92]: #93
 #12 := (= #11 #8)
 #13 := (forall (vars (?v0 S2) (?v1 S2)) #12)
 #55 := (iff #13 #54)
@@ -51218,8 +51218,8 @@
 #56 := [quant-intro #53]: #55
 #50 := [asserted]: #13
 #59 := [mp #50 #56]: #54
-#83 := [mp~ #59 #89]: #54
-#577 := [mp #83 #576]: #572
+#80 := [mp~ #59 #94]: #54
+#577 := [mp #80 #576]: #572
 #563 := (not #572)
 #565 := (or #563 #243)
 #220 := [quant-inst #25 #24]: #565
@@ -51267,10 +51267,10 @@
 #587 := (iff #66 #66)
 #588 := [refl]: #587
 #590 := [quant-intro #588]: #589
-#95 := (~ #70 #70)
-#91 := (~ #66 #66)
-#92 := [refl]: #91
-#96 := [nnf-pos #92]: #95
+#85 := (~ #70 #70)
+#97 := (~ #66 #66)
+#98 := [refl]: #97
+#86 := [nnf-pos #98]: #85
 #21 := (= #20 #17)
 #22 := (forall (vars (?v0 S3)) #21)
 #71 := (iff #22 #70)
@@ -51279,8 +51279,8 @@
 #72 := [quant-intro #69]: #71
 #65 := [asserted]: #22
 #75 := [mp #65 #72]: #70
-#97 := [mp~ #75 #96]: #70
-#591 := [mp #97 #590]: #586
+#99 := [mp~ #75 #86]: #70
+#591 := [mp #99 #590]: #586
 #569 := (not #586)
 #564 := (or #569 #559)
 #570 := [quant-inst #23]: #564
@@ -51294,7 +51294,7 @@
 #548 := [unit-resolution #173 #210]: #242
 [unit-resolution #548 #554]: false
 unsat
-e0d0d958c704cd740ed0ffb718fec05abf4295fd 82 0
+4f529fd4091f297cfc050e5da16cb9f0bd732f8b 82 0
 #2 := false
 decl f4 :: (-> S2 S3 S3)
 decl f6 :: S3
@@ -51341,10 +51341,10 @@
 #708 := (iff #31 #31)
 #709 := [refl]: #708
 #711 := [quant-intro #709]: #710
-#194 := (~ #32 #32)
-#192 := (~ #31 #31)
-#193 := [refl]: #192
-#195 := [nnf-pos #193]: #194
+#167 := (~ #32 #32)
+#172 := (~ #31 #31)
+#166 := [refl]: #172
+#164 := [nnf-pos #166]: #167
 #27 := (= f6 #10)
 #28 := (not #27)
 #29 := (forall (vars (?v0 S2) (?v1 S3)) #28)
@@ -51356,8 +51356,8 @@
 #123 := [quant-intro #121]: #122
 #116 := [asserted]: #29
 #126 := [mp #116 #123]: #32
-#196 := [mp~ #126 #195]: #32
-#712 := [mp #196 #711]: #707
+#165 := [mp~ #126 #164]: #32
+#712 := [mp #165 #711]: #707
 #289 := (not #707)
 #362 := (or #289 #349)
 #356 := (= #269 f6)
@@ -51377,7 +51377,7 @@
 #686 := [unit-resolution #675 #712]: #349
 [unit-resolution #686 #323]: false
 unsat
-08e36b4206627321e9ef13c16c3c6ff1083524c9 69 0
+3d691bfff446966153e91c446604c6142068edd9 69 0
 #2 := false
 decl f4 :: (-> S2 S3 S3)
 decl f6 :: S3
@@ -51418,10 +51418,10 @@
 #710 := (iff #31 #31)
 #711 := [refl]: #710
 #713 := [quant-intro #711]: #712
-#196 := (~ #32 #32)
-#194 := (~ #31 #31)
-#195 := [refl]: #194
-#197 := [nnf-pos #195]: #196
+#169 := (~ #32 #32)
+#174 := (~ #31 #31)
+#168 := [refl]: #174
+#166 := [nnf-pos #168]: #169
 #27 := (= f6 #10)
 #28 := (not #27)
 #29 := (forall (vars (?v0 S2) (?v1 S3)) #28)
@@ -51433,8 +51433,8 @@
 #125 := [quant-intro #123]: #124
 #118 := [asserted]: #29
 #128 := [mp #118 #125]: #32
-#198 := [mp~ #128 #197]: #32
-#714 := [mp #198 #713]: #709
+#167 := [mp~ #128 #166]: #32
+#714 := [mp #167 #713]: #709
 #364 := (not #709)
 #649 := (or #364 #150)
 #490 := (or #364 #62)
@@ -51447,7 +51447,7 @@
 #639 := [mp #635 #638]: #649
 [unit-resolution #639 #714 #162]: false
 unsat
-e3c83bfe7d36b6dbe01f810a411eecc94e2d0020 136 0
+4c1447056b8cb4c1d1990c18e936eb64adf50f7a 136 0
 #2 := false
 decl f4 :: (-> S2 S3 S3)
 decl f6 :: S3
@@ -51487,13 +51487,13 @@
 #10 := (f4 #8 #9)
 #700 := (pattern #10 #19)
 #109 := (= #9 #18)
-#163 := (not #109)
+#200 := (not #109)
 #106 := (= #8 #17)
-#162 := (not #106)
-#160 := (or #162 #163)
-#161 := (not #160)
+#199 := (not #106)
+#201 := (or #199 #200)
+#202 := (not #201)
 #102 := (= #10 #19)
-#205 := (iff #102 #161)
+#205 := (iff #102 #202)
 #701 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S2) (?v3 S3)) (:pat #700) #205)
 #208 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S2) (?v3 S3)) #205)
 #704 := (iff #208 #701)
@@ -51505,14 +51505,14 @@
 #118 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S2) (?v3 S3)) #115)
 #209 := (iff #118 #208)
 #206 := (iff #115 #205)
-#203 := (iff #112 #161)
+#203 := (iff #112 #202)
 #204 := [rewrite]: #203
 #207 := [monotonicity #204]: #206
 #210 := [quant-intro #207]: #209
-#191 := (~ #118 #118)
+#175 := (~ #118 #118)
 #177 := (~ #115 #115)
 #178 := [refl]: #177
-#192 := [nnf-pos #178]: #191
+#176 := [nnf-pos #178]: #175
 #22 := (= #18 #9)
 #21 := (= #17 #8)
 #23 := (and #21 #22)
@@ -51533,8 +51533,8 @@
 #120 := [quant-intro #117]: #119
 #101 := [asserted]: #25
 #123 := [mp #101 #120]: #118
-#193 := [mp~ #123 #192]: #118
-#211 := [mp #193 #210]: #208
+#173 := [mp~ #123 #176]: #118
+#211 := [mp #173 #210]: #208
 #706 := [mp #211 #705]: #701
 #660 := (not #701)
 #661 := (or #660 #310)
@@ -51584,7 +51584,7 @@
 #656 := [mp #383 #277]: #661
 [unit-resolution #656 #706 #616]: false
 unsat
-8500def9bd98753ab4a7655e9231b63171fa5f04 50 0
+2c91ac71f41255b8ebcce1fb25dd8a7435a5aefc 50 0
 #2 := false
 decl f3 :: (-> S3 S2)
 decl f4 :: (-> S2 S3 S3)
@@ -51616,10 +51616,10 @@
 #683 := (iff #83 #83)
 #684 := [refl]: #683
 #686 := [quant-intro #684]: #685
-#170 := (~ #86 #86)
-#177 := (~ #83 #83)
-#178 := [refl]: #177
-#171 := [nnf-pos #178]: #170
+#163 := (~ #86 #86)
+#125 := (~ #83 #83)
+#162 := [refl]: #125
+#164 := [nnf-pos #162]: #163
 #12 := (= #11 #8)
 #13 := (forall (vars (?v0 S2) (?v1 S3)) #12)
 #87 := (iff #13 #86)
@@ -51628,14 +51628,14 @@
 #88 := [quant-intro #85]: #87
 #82 := [asserted]: #13
 #91 := [mp #82 #88]: #86
-#125 := [mp~ #91 #171]: #86
-#687 := [mp #125 #686]: #682
+#175 := [mp~ #91 #164]: #86
+#687 := [mp #175 #686]: #682
 #342 := (not #682)
 #676 := (or #342 #146)
 #677 := [quant-inst #57 #58]: #676
 [unit-resolution #677 #687 #154]: false
 unsat
-a4455fa26a2bf5d21921399b4d6f0e721daff1a2 50 0
+3ac68e901beccda437cc98a0bd632fd658e36767 50 0
 #2 := false
 decl f5 :: (-> S3 S3)
 decl f4 :: (-> S2 S3 S3)
@@ -51667,10 +51667,10 @@
 #689 := (iff #90 #90)
 #690 := [refl]: #689
 #692 := [quant-intro #690]: #691
-#158 := (~ #94 #94)
-#165 := (~ #90 #90)
-#166 := [refl]: #165
-#159 := [nnf-pos #166]: #158
+#174 := (~ #94 #94)
+#176 := (~ #90 #90)
+#173 := [refl]: #176
+#171 := [nnf-pos #173]: #174
 #15 := (= #14 #9)
 #16 := (forall (vars (?v0 S2) (?v1 S3)) #15)
 #95 := (iff #16 #94)
@@ -51679,14 +51679,14 @@
 #96 := [quant-intro #93]: #95
 #89 := [asserted]: #16
 #99 := [mp #89 #96]: #94
-#160 := [mp~ #99 #159]: #94
-#693 := [mp #160 #692]: #688
+#172 := [mp~ #99 #171]: #94
+#693 := [mp #172 #692]: #688
 #674 := (not #688)
 #680 := (or #674 #146)
 #670 := [quant-inst #57 #58]: #680
 [unit-resolution #670 #693 #154]: false
 unsat
-65f5926fa55a56a20b93bf43ca8b606d7a725e83 56 0
+8142fde9b86379b43ddc5095b2fea794eefa6812 56 0
 #2 := false
 decl f3 :: (-> S3 S2)
 decl f4 :: (-> S2 S3 S3)
@@ -51724,10 +51724,10 @@
 #686 := (iff #86 #86)
 #687 := [refl]: #686
 #689 := [quant-intro #687]: #688
-#169 := (~ #89 #89)
+#166 := (~ #89 #89)
 #128 := (~ #86 #86)
-#168 := [refl]: #128
-#159 := [nnf-pos #168]: #169
+#165 := [refl]: #128
+#167 := [nnf-pos #165]: #166
 #12 := (= #11 #8)
 #13 := (forall (vars (?v0 S2) (?v1 S3)) #12)
 #90 := (iff #13 #89)
@@ -51736,14 +51736,14 @@
 #91 := [quant-intro #88]: #90
 #85 := [asserted]: #13
 #94 := [mp #85 #91]: #89
-#160 := [mp~ #94 #159]: #89
-#690 := [mp #160 #689]: #685
+#178 := [mp~ #94 #167]: #89
+#690 := [mp #178 #689]: #685
 #618 := (not #685)
 #436 := (or #618 #149)
 #429 := [quant-inst #57 #61]: #436
 [unit-resolution #429 #690 #157]: false
 unsat
-d48bb23843eefa7d190bfd37fdd1c5737b414ba9 56 0
+4c528c48e59636ae8904df7a63f06102514e82cf 56 0
 #2 := false
 decl f5 :: (-> S3 S3)
 decl f4 :: (-> S2 S3 S3)
@@ -51781,10 +51781,10 @@
 #692 := (iff #93 #93)
 #693 := [refl]: #692
 #695 := [quant-intro #693]: #694
-#165 := (~ #97 #97)
-#163 := (~ #93 #93)
-#164 := [refl]: #163
-#170 := [nnf-pos #164]: #165
+#177 := (~ #97 #97)
+#179 := (~ #93 #93)
+#176 := [refl]: #179
+#174 := [nnf-pos #176]: #177
 #15 := (= #14 #9)
 #16 := (forall (vars (?v0 S2) (?v1 S3)) #15)
 #98 := (iff #16 #97)
@@ -51793,14 +51793,14 @@
 #99 := [quant-intro #96]: #98
 #92 := [asserted]: #16
 #102 := [mp #92 #99]: #97
-#171 := [mp~ #102 #170]: #97
-#696 := [mp #171 #695]: #691
+#175 := [mp~ #102 #174]: #97
+#696 := [mp #175 #695]: #691
 #600 := (not #691)
 #433 := (or #600 #149)
 #434 := [quant-inst #57 #61]: #433
 [unit-resolution #434 #696 #157]: false
 unsat
-6b5ffaa8a4665068d38b31a11461bd89d95e477d 95 0
+d57de5e3a80dc81f7c8246af61305a83e94d9d64 95 0
 #2 := false
 decl f3 :: (-> S3 S2)
 decl f5 :: (-> S3 S3)
@@ -51836,10 +51836,10 @@
 #693 := (iff #94 #94)
 #694 := [refl]: #693
 #696 := [quant-intro #694]: #695
-#162 := (~ #98 #98)
-#160 := (~ #94 #94)
-#161 := [refl]: #160
-#163 := [nnf-pos #161]: #162
+#178 := (~ #98 #98)
+#180 := (~ #94 #94)
+#177 := [refl]: #180
+#175 := [nnf-pos #177]: #178
 #15 := (= #14 #9)
 #16 := (forall (vars (?v0 S2) (?v1 S3)) #15)
 #99 := (iff #16 #98)
@@ -51848,8 +51848,8 @@
 #100 := [quant-intro #97]: #99
 #93 := [asserted]: #16
 #103 := [mp #93 #100]: #98
-#164 := [mp~ #103 #163]: #98
-#697 := [mp #164 #696]: #692
+#176 := [mp~ #103 #175]: #98
+#697 := [mp #176 #696]: #692
 #601 := (not #692)
 #435 := (or #601 #437)
 #421 := [quant-inst #57 #61]: #435
@@ -51866,10 +51866,10 @@
 #687 := (iff #87 #87)
 #688 := [refl]: #687
 #690 := [quant-intro #688]: #689
-#173 := (~ #90 #90)
+#167 := (~ #90 #90)
 #129 := (~ #87 #87)
-#172 := [refl]: #129
-#165 := [nnf-pos #172]: #173
+#166 := [refl]: #129
+#168 := [nnf-pos #166]: #167
 #12 := (= #11 #8)
 #13 := (forall (vars (?v0 S2) (?v1 S3)) #12)
 #91 := (iff #13 #90)
@@ -51878,8 +51878,8 @@
 #92 := [quant-intro #89]: #91
 #86 := [asserted]: #13
 #95 := [mp #86 #92]: #90
-#166 := [mp~ #95 #165]: #90
-#691 := [mp #166 #690]: #686
+#179 := [mp~ #95 #168]: #90
+#691 := [mp #179 #690]: #686
 #619 := (not #686)
 #515 := (or #619 #504)
 #516 := [quant-inst #58 #60]: #515
@@ -51896,7 +51896,7 @@
 #158 := [mp #148 #155]: #153
 [unit-resolution #158 #410]: false
 unsat
-3c9960275d5862cae6ae020dd19199bbe60db8f3 71 0
+2396070c784c90f1fb45b2c026662e0b8ae4811a 71 0
 #2 := false
 decl f5 :: (-> S3 S3)
 decl f4 :: (-> S2 S3 S3)
@@ -51931,10 +51931,10 @@
 #693 := (iff #94 #94)
 #694 := [refl]: #693
 #696 := [quant-intro #694]: #695
-#166 := (~ #98 #98)
-#164 := (~ #94 #94)
-#165 := [refl]: #164
-#171 := [nnf-pos #165]: #166
+#178 := (~ #98 #98)
+#180 := (~ #94 #94)
+#177 := [refl]: #180
+#175 := [nnf-pos #177]: #178
 #15 := (= #14 #9)
 #16 := (forall (vars (?v0 S2) (?v1 S3)) #15)
 #99 := (iff #16 #98)
@@ -51943,8 +51943,8 @@
 #100 := [quant-intro #97]: #99
 #93 := [asserted]: #16
 #103 := [mp #93 #100]: #98
-#172 := [mp~ #103 #171]: #98
-#697 := [mp #172 #696]: #692
+#176 := [mp~ #103 #175]: #98
+#697 := [mp #176 #696]: #692
 #601 := (not #692)
 #435 := (or #601 #437)
 #421 := [quant-inst #57 #61]: #435
@@ -51968,7 +51968,7 @@
 #158 := [mp #148 #155]: #153
 [unit-resolution #158 #410]: false
 unsat
-d5569cbebc9c95b668e726d7b9e33fb967151908 97 0
+db423730ba0ca064d1048e6169dad21fed1e792c 97 0
 #2 := false
 decl f3 :: (-> S4 S2)
 decl f6 :: (-> S5 S4)
@@ -52002,10 +52002,10 @@
 #760 := (iff #123 #123)
 #761 := [refl]: #760
 #763 := [quant-intro #761]: #762
-#213 := (~ #127 #127)
-#211 := (~ #123 #123)
-#212 := [refl]: #211
-#220 := [nnf-pos #212]: #213
+#208 := (~ #127 #127)
+#213 := (~ #123 #123)
+#207 := [refl]: #213
+#205 := [nnf-pos #207]: #208
 #27 := (= #26 #23)
 #28 := (forall (vars (?v0 S4) (?v1 S5)) #27)
 #128 := (iff #28 #127)
@@ -52014,8 +52014,8 @@
 #129 := [quant-intro #126]: #128
 #122 := [asserted]: #28
 #132 := [mp #122 #129]: #127
-#221 := [mp~ #132 #220]: #127
-#764 := [mp #221 #763]: #759
+#206 := [mp~ #132 #205]: #127
+#764 := [mp #206 #763]: #759
 #375 := (not #759)
 #376 := (or #375 #712)
 #714 := [quant-inst #74 #41]: #376
@@ -52036,10 +52036,10 @@
 #739 := (iff #100 #100)
 #740 := [refl]: #739
 #742 := [quant-intro #740]: #741
-#219 := (~ #103 #103)
+#210 := (~ #103 #103)
 #166 := (~ #100 #100)
-#218 := [refl]: #166
-#209 := [nnf-pos #218]: #219
+#209 := [refl]: #166
+#211 := [nnf-pos #209]: #210
 #12 := (= #11 #8)
 #13 := (forall (vars (?v0 S2) (?v1 S3)) #12)
 #104 := (iff #13 #103)
@@ -52048,8 +52048,8 @@
 #105 := [quant-intro #102]: #104
 #99 := [asserted]: #13
 #108 := [mp #99 #105]: #103
-#210 := [mp~ #108 #209]: #103
-#743 := [mp #210 #742]: #738
+#222 := [mp~ #108 #211]: #103
+#743 := [mp #222 #742]: #738
 #321 := (not #738)
 #408 := (or #321 #406)
 #399 := [quant-inst #72 #73]: #408
@@ -52066,7 +52066,7 @@
 #195 := [mp #185 #192]: #190
 [unit-resolution #195 #723]: false
 unsat
-4d4a4abaf885c3c42662c956779a33f9969b3641 97 0
+e89d19faaf82ed94357ec4677d8f827dcc26761d 97 0
 #2 := false
 decl f5 :: (-> S4 S3)
 decl f6 :: (-> S5 S4)
@@ -52100,10 +52100,10 @@
 #760 := (iff #123 #123)
 #761 := [refl]: #760
 #763 := [quant-intro #761]: #762
-#213 := (~ #127 #127)
-#211 := (~ #123 #123)
-#212 := [refl]: #211
-#220 := [nnf-pos #212]: #213
+#208 := (~ #127 #127)
+#213 := (~ #123 #123)
+#207 := [refl]: #213
+#205 := [nnf-pos #207]: #208
 #27 := (= #26 #23)
 #28 := (forall (vars (?v0 S4) (?v1 S5)) #27)
 #128 := (iff #28 #127)
@@ -52112,8 +52112,8 @@
 #129 := [quant-intro #126]: #128
 #122 := [asserted]: #28
 #132 := [mp #122 #129]: #127
-#221 := [mp~ #132 #220]: #127
-#764 := [mp #221 #763]: #759
+#206 := [mp~ #132 #205]: #127
+#764 := [mp #206 #763]: #759
 #375 := (not #759)
 #376 := (or #375 #712)
 #714 := [quant-inst #74 #41]: #376
@@ -52134,10 +52134,10 @@
 #745 := (iff #107 #107)
 #746 := [refl]: #745
 #748 := [quant-intro #746]: #747
-#199 := (~ #111 #111)
-#204 := (~ #107 #107)
-#205 := [refl]: #204
-#200 := [nnf-pos #205]: #199
+#221 := (~ #111 #111)
+#223 := (~ #107 #107)
+#220 := [refl]: #223
+#218 := [nnf-pos #220]: #221
 #15 := (= #14 #9)
 #16 := (forall (vars (?v0 S2) (?v1 S3)) #15)
 #112 := (iff #16 #111)
@@ -52146,8 +52146,8 @@
 #113 := [quant-intro #110]: #112
 #106 := [asserted]: #16
 #116 := [mp #106 #113]: #111
-#201 := [mp~ #116 #200]: #111
-#749 := [mp #201 #748]: #744
+#219 := [mp~ #116 #218]: #111
+#749 := [mp #219 #748]: #744
 #339 := (not #744)
 #412 := (or #339 #407)
 #409 := [quant-inst #72 #73]: #412
@@ -52276,7 +52276,7 @@
 #101 := [not-or-elim #103]: #43
 [unit-resolution #101 #277]: false
 unsat
-9701cdd9448439fa34387c2ec3bdc4fe35ec7bdc 54 0
+0c2977c8c8618eef37974bd4a2fc3d59345d9965 54 0
 #2 := false
 #38 := 3::Int
 decl f3 :: (-> S3 Int)
@@ -52331,7 +52331,7 @@
 #247 := [mp #241 #246]: #236
 [unit-resolution #247 #196 #91]: false
 unsat
-3a7987f9f2406e33255cc3f658f066dbd894644a 54 0
+d68134f72bff3c71be36dfe7e7a5d3d9aa42e109 54 0
 #2 := false
 #39 := 4::Int
 decl f5 :: (-> S3 Int)
@@ -52386,7 +52386,7 @@
 #262 := [mp #256 #261]: #254
 [unit-resolution #262 #202 #91]: false
 unsat
-2a9b9fb7f75472ed7447a04c770c82842793429a 109 0
+df4cc6af0d8c7c1f4e2ce7f971d5bcdb24cc7842 109 0
 #2 := false
 #39 := 4::Int
 #38 := 3::Int
@@ -52496,7 +52496,7 @@
 #270 := [trans #268 #261]: #269
 [mp #270 #272]: false
 unsat
-2e54a746615da0b9042b7a1c7abdcba21277b942 73 0
+c3ea340f2ca5088543fc4bdcf4ebe731f9a5f650 73 0
 #2 := false
 decl f6 :: (-> Int Int S3 S4)
 decl f13 :: S3
@@ -52570,7 +52570,7 @@
 #100 := [asserted]: #52
 [unit-resolution #100 #345]: false
 unsat
-a5cf3bd14553e66b05989b95f1712c3548d79c05 73 0
+68cdbe5843e8281a606da777ab86dc4c9c5028ae 73 0
 #2 := false
 decl f6 :: (-> Int Int S3 S4)
 decl f13 :: S3
@@ -52644,7 +52644,7 @@
 #100 := [asserted]: #52
 [unit-resolution #100 #345]: false
 unsat
-b59ea79b3381bb3b8446dda45524f635379fcd3e 211 0
+ff18e62b724360b80c3a974588e17e2bef964664 211 0
 #2 := false
 decl f11 :: (-> S2 S4 S4)
 decl f10 :: (-> S2 S4 S4)
@@ -52856,7 +52856,7 @@
 #127 := [not-or-elim #126]: #125
 [unit-resolution #127 #437]: false
 unsat
-e55f9d76dda3b8c2c60cf7fba6ece493ac2093db 211 0
+d86a80a06ecde74cac9fcb7a0ce1d146b14bdff5 211 0
 #2 := false
 decl f10 :: (-> S2 S4 S4)
 decl f11 :: (-> S2 S4 S4)
@@ -53124,7 +53124,7 @@
 #154 := [not-or-elim #153]: #152
 [unit-resolution #154 #347]: false
 unsat
-1a1dbb36df0b0fe92eb18b671d63ad44f5ac7c76 71 0
+3fc90649d66e9e3133ec6ffaaa72e92cae1906e4 71 0
 #2 := false
 decl f12 :: (-> S3 S1)
 decl f20 :: S3
@@ -53169,30 +53169,30 @@
 #693 := [monotonicity #167]: #691
 #348 := [monotonicity #693]: #152
 #372 := (not #149)
-#205 := (not #146)
-#480 := (iff #205 #372)
+#196 := (not #146)
+#480 := (iff #196 #372)
 #687 := [monotonicity #348]: #480
-#375 := [hypothesis]: #205
+#375 := [hypothesis]: #196
 #359 := [mp #375 #687]: #372
 #370 := (or #149 #146)
-#206 := (iff #149 #205)
+#197 := (iff #149 #196)
 #168 := (not #152)
-#207 := (iff #168 #206)
-#208 := [rewrite]: #207
+#198 := (iff #168 #197)
+#199 := [rewrite]: #198
 #170 := [not-or-elim #169]: #168
-#209 := [mp #170 #208]: #206
-#368 := (not #206)
+#200 := [mp #170 #199]: #197
+#368 := (not #197)
 #369 := (or #149 #146 #368)
 #284 := [def-axiom]: #369
-#361 := [unit-resolution #284 #209]: #370
+#361 := [unit-resolution #284 #200]: #370
 #354 := [unit-resolution #361 #375]: #149
 #360 := [unit-resolution #354 #359]: false
 #694 := [lemma #360]: #146
 #696 := [mp #694 #348]: #149
-#374 := (or #372 #205)
-#373 := (or #372 #205 #368)
+#374 := (or #372 #196)
+#373 := (or #372 #196 #368)
 #301 := [def-axiom]: #373
-#371 := [unit-resolution #301 #209]: #374
+#371 := [unit-resolution #301 #200]: #374
 #695 := [unit-resolution #371 #694]: #372
 [unit-resolution #695 #696]: false
 unsat
@@ -53252,7 +53252,7 @@
 #152 := [not-or-elim #154]: #70
 [unit-resolution #152 #347]: false
 unsat
-3c5eeec3f72704eac255d0f1e9284d0d20ab0722 87 0
+5ac8b5530f88aae423bf81b2aa1ee58c0cb330b8 87 0
 #2 := false
 decl f12 :: (-> S3 S1)
 decl f20 :: S3
@@ -53324,11 +53324,11 @@
 #375 := [mp #391 #703]: #388
 #386 := (or #151 #148)
 #189 := [not-or-elim #190]: #157
-#225 := [mp #189 #163]: #161
+#216 := [mp #189 #163]: #161
 #384 := (not #161)
 #385 := (or #151 #148 #384)
 #300 := [def-axiom]: #385
-#377 := [unit-resolution #300 #225]: #386
+#377 := [unit-resolution #300 #216]: #386
 #370 := [unit-resolution #377 #391]: #151
 #376 := [unit-resolution #370 #375]: false
 #710 := [lemma #376]: #148
@@ -53336,11 +53336,11 @@
 #390 := (or #388 #160)
 #389 := (or #388 #160 #384)
 #317 := [def-axiom]: #389
-#387 := [unit-resolution #317 #225]: #390
+#387 := [unit-resolution #317 #216]: #390
 #711 := [unit-resolution #387 #710]: #388
 [unit-resolution #711 #712]: false
 unsat
-60180a7beca4718d4b909f1bb0ce2c0b84139dea 58 0
+da4bfd4a4625015f645fceb2c4dd17a2e385441a 58 0
 #2 := false
 #65 := 3::Int
 decl f3 :: (-> S3 Int)
@@ -53399,7 +53399,7 @@
 #382 := [mp #376 #381]: #371
 [unit-resolution #382 #269 #144]: false
 unsat
-4e405ea4a814758902eec1be5c3ffd542fdce183 58 0
+74804e4af971e8af0af6d60bbc463cc104ca380a 58 0
 #2 := false
 #66 := 4::Int
 decl f5 :: (-> S3 Int)
@@ -53458,7 +53458,7 @@
 #397 := [mp #391 #396]: #389
 [unit-resolution #397 #275 #144]: false
 unsat
-4ed86aa1fa601dd0a3ec30f70fe5685baa4f141b 105 0
+29db4bfc400e68d7454857ddd1753e5e2b87bacd 105 0
 #2 := false
 decl f12 :: (-> S3 S1)
 decl f4 :: (-> Int Int S2 S3)
@@ -53564,7 +53564,7 @@
 #416 := [unit-resolution #364 #409]: #415
 [unit-resolution #416 #414 #413]: false
 unsat
-1106827b733d83eccb037f282dd3b096b2abf8d0 113 0
+66c763bb178c6b9cd687c2f7614b778b686167f0 113 0
 #2 := false
 #66 := 4::Int
 #65 := 3::Int
@@ -53678,7 +53678,7 @@
 #405 := [trans #403 #396]: #404
 [mp #405 #407]: false
 unsat
-df574a4365f54e674a55945a532b21aa0b2dc1f4 77 0
+ddb9b0a02011f2cff7e6d056c403901bbad7783e 77 0
 #2 := false
 decl f6 :: (-> Int Int S3 S4)
 decl f14 :: (-> S1 S6 S3)
@@ -53756,7 +53756,7 @@
 #153 := [asserted]: #81
 [unit-resolution #153 #540]: false
 unsat
-4e89c6fb18f25038439974fdc91cdb5ab18a8af0 77 0
+ff379bc11c0b6e1c82ab589c8fa86258b5520522 77 0
 #2 := false
 decl f6 :: (-> Int Int S3 S4)
 decl f14 :: (-> S1 S6 S3)
@@ -53834,7 +53834,7 @@
 #153 := [asserted]: #81
 [unit-resolution #153 #540]: false
 unsat
-68e99be1e87e8d0678d49d93a4e91b40c95b96ee 409 0
+0b8858aa262cda85f2c91cda2489bcba0a45e777 409 0
 #2 := false
 decl f19 :: (-> S3 S5 S5)
 decl f13 :: (-> S2 S5 S5)
@@ -54244,7 +54244,7 @@
 #202 := [not-or-elim #201]: #200
 [unit-resolution #202 #799]: false
 unsat
-b772603aaba9792fa294ee48d2ae093633041197 381 0
+c94a232e1e97412d949006cec91fe1baa089456e 381 0
 #2 := false
 decl f12 :: (-> S2 S5 S5)
 decl f19 :: (-> S3 S5 S5)
@@ -54626,7 +54626,7 @@
 #202 := [not-or-elim #201]: #200
 [unit-resolution #202 #800]: false
 unsat
-4bea4bb3dde48b2c759327219b4fbf786808215a 371 0
+1ab1638cab30b8ac06816e79bcba1d425930e19f 371 0
 #2 := false
 decl f13 :: (-> S2 S5 S5)
 decl f12 :: (-> S2 S5 S5)
@@ -56028,27 +56028,27 @@
 #157 := [mp #147 #154]: #152
 [unit-resolution #157 #592]: false
 unsat
-1e7ecf060cee9e61bb4405bc59df8efef823a76d 1 0
-unsat
-ed7be74f50946d158793410899f40df6519543b4 1 0
+ce5c7dc705bde44a6d76052fa847da849e2a25e8 1 0
+unsat
+38f8891a46367464bd66f6857c08f6855d01823e 1 0
 unsat
 4c4662b7eb4bf820d980581a2fc91e7581f1e6de 1 0
 unsat
 604fe1781a4518f475d867cbe05bb790967e29f4 1 0
 unsat
-6f6dde323bd21ef16ff088176bfa80c841d2a67b 1 0
-unsat
-2d706ed8665b791195dfe7d8dde2163fe3e3d050 1 0
-unsat
-5a9342008efdfdb5868bb4ac65d28f9a70022d8e 1 0
-unsat
-1dce42cc11b180208dab2d5cc87ea493ae738340 1 0
-unsat
-24790734475987e966a5f8cdaae6e4d6cf5db0c8 1 0
-unsat
-af484a68410644745b3c7f43e2cb6a1551acf2b9 1 0
-unsat
-ade3c87b7f2ac2ad5c1c06607a5d5f1178485104 1 0
+e130feb491d595cdd26b50ba606e05e82253e662 1 0
+unsat
+c88f40069f119a5ef611e766b88fb27a33376469 1 0
+unsat
+1ccf6da8e3379de961a4726c61dbce60d8a156a6 1 0
+unsat
+08d35d263f3f330d899a684f508f9fb87a1c3c37 1 0
+unsat
+e5d8720cfd335d72e9a747ea51260f137ff368d8 1 0
+unsat
+3b9051c93ad8585444c4095c41043c5faac0a057 1 0
+unsat
+ed62fdab40c4611ac5f753597d277d2ce675438e 1 0
 unsat
 1bb4f3696612274f0ada059e663e5df3e8c1753c 1 0
 unsat
@@ -56056,21 +56056,21 @@
 unsat
 99a4b89024a5ade20a17839e46c3c800a839dc73 1 0
 unsat
-25d7cafeec4877bd332c7a84d48d1e1bba149730 1 0
-unsat
-46cecad9c27ddd660a32c43da02fbc077e4d2653 1 0
-unsat
-9985536f3adcfa82b82611a2e3c65c48234903b7 1 0
-unsat
-650e66124ceb469142418bdf9b727f4eb46000d3 1 0
-unsat
-ad845af29980d8f1b8f9106555beea4a0787e50b 1 0
-unsat
-1226a39ae26fb124fa2784c01feeda2fa8b7f164 1 0
-unsat
-aeed0548e98a49111c97d9c505f2ddcc25a8f0a0 1 0
-unsat
-6937351f88cbcd4ce38d156d36ca3f3b7400b010 1 0
+0cc8b3c4c079835098be13e075f80b6f8f429792 1 0
+unsat
+bae675adb36d3ecf65e47295f7f3002cfca775bc 1 0
+unsat
+fffdec69ce4b32df667e7e36f2aeb449eb96e502 1 0
+unsat
+0f8130ffadb0ea5f83bcb9678a8a0a428f75ba11 1 0
+unsat
+14c521dcb3c0dfca6046dd47445512db024842c8 1 0
+unsat
+70449057ac865f7275970f313c73de2e2e0661aa 1 0
+unsat
+e981571d927b81eda8506ab06352029e66ca215d 1 0
+unsat
+47e9f293cb55e7b278a387a7b63c8dca7bb74490 1 0
 unsat
 660ffa7d21617f3d9be770c0a37b4fe52fc41f63 1 0
 unsat
@@ -56080,57 +56080,57 @@
 unsat
 990af511d3a0b46205abbd2ddd25c459f6e66c5a 1 0
 unsat
-cf85ae43503909529635475e22a3bb7409c56a5c 1 0
-unsat
-fb00d7a0af114cd80f8efb9453ee0baf42d58298 1 0
-unsat
-ea112adb690b675025a205ff95598c0e1bacd1b3 1 0
-unsat
-cde5d9f95f561892bc84c1a943338cf0d427920f 1 0
-unsat
-848677eef79eb7cb4fb3573c0d5c5fca34811251 1 0
-unsat
-0e0faa00af41d5f14b5cb0a291dc7001b6276b81 1 0
-unsat
-3ec23529e810aeac05c8d7c95856e437cc15481a 1 0
-unsat
-991d721d9af19456ad333e832e6e1ff105598a2a 1 0
-unsat
-c6d7a69a2fdeee85db63627aecd087b63d4f1c1c 1 0
-unsat
-f67f5ba5a69d007092f7dd70dc2dbb1215926e11 1 0
+002f1c6e9a3a5a1ad6e0f4bf2560ee22d04cb4cb 1 0
+unsat
+d744812ec0e9257421fb2e0a9820bfee04042dcc 1 0
+unsat
+839f47953dc6c5ce7fe7d2130b5506e3817c2d88 1 0
+unsat
+9524a9683d04ec02a17fa21f4043facff04c80fc 1 0
+unsat
+756c9bc731ec5fb4e483e2dc1116d061c5c2f35f 1 0
+unsat
+a92f055099a204d5b9347ef35e4b654dbde35134 1 0
+unsat
+11baeb6d885300b41ed62e9fc3dbdf6f45620679 1 0
+unsat
+0f60a11f2d707aedad80fb23ffcd23106c420369 1 0
+unsat
+8f1cf6dbbd974f52bf4332e11e8e73c8154082e3 1 0
+unsat
+4aa264ab45139cb17c9c3b017f0459151b0f481a 1 0
 unsat
 1839415a04580c458d9a54c09162d0c394cad86c 1 0
 unsat
 595084d6acf7cb9e727b2d71c11dcd5adfd678ca 1 0
 unsat
-ce8e551a982c6290b1be8781429cefd4f9165293 1 0
+da3f2f9dbdb7632f25c324bc059065293b4304af 1 0
 unsat
 c271fe52291540adaf545c617359ed457de173b1 1 0
 unsat
 d040cce0ec356b71ba4556c265407ab2f545e54c 1 0
 unsat
-674646d69af329d3589eeca7a6f731cbd7aabfb5 1 0
-unsat
-789139e6d5722962adae903c7c6f741a024ed141 1 0
-unsat
-1380018796c654e6dbfb3153a9601c28877a3114 1 0
-unsat
-16408e8543328af45ac16df15c0d63f3fc509499 1 0
-unsat
-0cbacef48453639efbd9117592087fa963979a9a 1 0
-unsat
-4f76e31263dc24919943a2ac6835f5ab5cbb885d 1 0
-unsat
-a76f56105de0da9e78f9f1ecf4de50bfa08478b8 1 0
-unsat
-fb3320cb741f8a5fec9b3b50a2caeab3ab35af68 1 0
-unsat
-4236ba058a6f6c1bacb0db47f2f621769329ff77 1 0
-unsat
-fe15efedfaad3ad3884dcd453f022326a429c99f 1 0
-unsat
-0adc18b99c93cda1aa22c7bd01d4133c76309534 1 0
+e84d0b7d00ab46d7f97ab3271f0a8f18ecad1e24 1 0
+unsat
+ff0c89be3232fff2c8dff18a14f6e1f4a9ac4ae1 1 0
+unsat
+0f8a977f38a5400888bac7277401dedadf78f509 1 0
+unsat
+30ec8a1fe895a83c6ea00219963e48e3d67bd9ff 1 0
+unsat
+d3a9054335fcb92f91170f4fd55fa45552749054 1 0
+unsat
+cbb3b7fa6dd1f35f64da4884777bcb6ae345f930 1 0
+unsat
+34a3d396bad33b535f04edd371ba357068e3fac7 1 0
+unsat
+4ab52d9261a65d65d938eebf39a1245e87bddc05 1 0
+unsat
+6aacde84f68949cd3f125396e017b084e6ee2625 1 0
+unsat
+0747bde3f05b6cd6790fc2f582793f7b8bd560f9 1 0
+unsat
+dc4bda1004c107889de0fd5c23e4a3df7f0c9a2a 1 0
 unsat
 49462927b92e2fe852e19ddabb722de885a6169e 1 0
 unsat
@@ -56781,2147 +56781,6 @@
 #92 := [not-or-elim #91]: #90
 [unit-resolution #92 #499]: false
 unsat
-3ab56ce3ce9ea17007c9ef9659d24c1591a2f1dc 31 0
-#2 := false
-decl f1 :: S1
-#4 := f1
-decl f8 :: (-> S4 S1)
-decl f9 :: S4
-#32 := f9
-#33 := (f8 f9)
-#34 := (= #33 f1)
-#35 := (iff #34 #34)
-#36 := (not #35)
-#125 := (iff #36 false)
-#1 := true
-#120 := (not true)
-#123 := (iff #120 false)
-#124 := [rewrite]: #123
-#121 := (iff #36 #120)
-#118 := (iff #35 true)
-#109 := (= f1 #33)
-#113 := (iff #109 #109)
-#116 := (iff #113 true)
-#117 := [rewrite]: #116
-#114 := (iff #35 #113)
-#111 := (iff #34 #109)
-#112 := [rewrite]: #111
-#115 := [monotonicity #112 #112]: #114
-#119 := [trans #115 #117]: #118
-#122 := [monotonicity #119]: #121
-#126 := [trans #122 #124]: #125
-#108 := [asserted]: #36
-[mp #108 #126]: false
-unsat
-99e99593c1b6e7784dba4d3a0aca41c7272cf4c1 58 0
-#2 := false
-decl f3 :: (-> S2 S1)
-decl f8 :: S2
-#33 := f8
-#34 := (f3 f8)
-decl f1 :: S1
-#4 := f1
-#110 := (= f1 #34)
-#35 := (= #34 f1)
-#36 := (not #35)
-#37 := (not #36)
-#122 := (iff #37 #110)
-#114 := (not #110)
-#117 := (not #114)
-#120 := (iff #117 #110)
-#121 := [rewrite]: #120
-#118 := (iff #37 #117)
-#115 := (iff #36 #114)
-#112 := (iff #35 #110)
-#113 := [rewrite]: #112
-#116 := [monotonicity #113]: #115
-#119 := [monotonicity #116]: #118
-#123 := [trans #119 #121]: #122
-#109 := [asserted]: #37
-#126 := [mp #109 #123]: #110
-#8 := (:var 0 S2)
-#9 := (f3 #8)
-#634 := (pattern #9)
-#58 := (= f1 #9)
-#61 := (not #58)
-#635 := (forall (vars (?v0 S2)) (:pat #634) #61)
-#64 := (forall (vars (?v0 S2)) #61)
-#638 := (iff #64 #635)
-#636 := (iff #61 #61)
-#637 := [refl]: #636
-#639 := [quant-intro #637]: #638
-#140 := (~ #64 #64)
-#138 := (~ #61 #61)
-#139 := [refl]: #138
-#141 := [nnf-pos #139]: #140
-#10 := (= #9 f1)
-#11 := (not #10)
-#12 := (forall (vars (?v0 S2)) #11)
-#65 := (iff #12 #64)
-#62 := (iff #11 #61)
-#59 := (iff #10 #58)
-#60 := [rewrite]: #59
-#63 := [monotonicity #60]: #62
-#66 := [quant-intro #63]: #65
-#57 := [asserted]: #12
-#69 := [mp #57 #66]: #64
-#125 := [mp~ #69 #141]: #64
-#640 := [mp #125 #639]: #635
-#217 := (not #635)
-#304 := (or #217 #114)
-#218 := [quant-inst #33]: #304
-[unit-resolution #218 #640 #126]: false
-unsat
-d9322750c44c3fbc7422a30bcad6e401e2be0930 46 0
-#2 := false
-decl f4 :: (-> S3 S1)
-decl f8 :: S3
-#33 := f8
-#34 := (f4 f8)
-decl f1 :: S1
-#4 := f1
-#109 := (= f1 #34)
-#113 := (not #109)
-#35 := (= #34 f1)
-#36 := (not #35)
-#114 := (iff #36 #113)
-#111 := (iff #35 #109)
-#112 := [rewrite]: #111
-#115 := [monotonicity #112]: #114
-#108 := [asserted]: #36
-#118 := [mp #108 #115]: #113
-#13 := (:var 0 S3)
-#14 := (f4 #13)
-#633 := (pattern #14)
-#67 := (= f1 #14)
-#634 := (forall (vars (?v0 S3)) (:pat #633) #67)
-#71 := (forall (vars (?v0 S3)) #67)
-#637 := (iff #71 #634)
-#635 := (iff #67 #67)
-#636 := [refl]: #635
-#638 := [quant-intro #636]: #637
-#120 := (~ #71 #71)
-#119 := (~ #67 #67)
-#134 := [refl]: #119
-#121 := [nnf-pos #134]: #120
-#15 := (= #14 f1)
-#16 := (forall (vars (?v0 S3)) #15)
-#72 := (iff #16 #71)
-#69 := (iff #15 #67)
-#70 := [rewrite]: #69
-#73 := [quant-intro #70]: #72
-#66 := [asserted]: #16
-#76 := [mp #66 #73]: #71
-#135 := [mp~ #76 #121]: #71
-#639 := [mp #135 #638]: #634
-#209 := (not #634)
-#296 := (or #209 #109)
-#210 := [quant-inst #33]: #296
-[unit-resolution #210 #639 #118]: false
-unsat
-b2f7b9c42d68e0ecab24c1bc7abe7e061806dd00 119 0
-#2 := false
-decl f5 :: (-> S3 S3 S4 S1)
-decl f11 :: S4
-#41 := f11
-decl f10 :: S3
-#40 := f10
-decl f9 :: S3
-#39 := f9
-#42 := (f5 f9 f10 f11)
-decl f1 :: S1
-#4 := f1
-#129 := (= f1 #42)
-#148 := (not #129)
-#652 := [hypothesis]: #148
-decl f6 :: (-> S3 S4 S1)
-#46 := (f6 f10 f11)
-#136 := (= f1 #46)
-#44 := (f6 f9 f11)
-#133 := (= f1 #44)
-#139 := (or #133 #136)
-#340 := (or #139 #129)
-#149 := (iff #139 #148)
-#47 := (= #46 f1)
-#45 := (= #44 f1)
-#48 := (or #45 #47)
-#43 := (= #42 f1)
-#49 := (iff #43 #48)
-#50 := (not #49)
-#152 := (iff #50 #149)
-#142 := (iff #129 #139)
-#145 := (not #142)
-#150 := (iff #145 #149)
-#151 := [rewrite]: #150
-#146 := (iff #50 #145)
-#143 := (iff #49 #142)
-#140 := (iff #48 #139)
-#137 := (iff #47 #136)
-#138 := [rewrite]: #137
-#134 := (iff #45 #133)
-#135 := [rewrite]: #134
-#141 := [monotonicity #135 #138]: #140
-#131 := (iff #43 #129)
-#132 := [rewrite]: #131
-#144 := [monotonicity #132 #141]: #143
-#147 := [monotonicity #144]: #146
-#153 := [trans #147 #151]: #152
-#128 := [asserted]: #50
-#156 := [mp #128 #153]: #149
-#266 := (not #149)
-#339 := (or #139 #129 #266)
-#336 := [def-axiom]: #339
-#319 := [unit-resolution #336 #156]: #340
-#324 := [unit-resolution #319 #652]: #139
-#326 := (not #139)
-#655 := (or #129 #326)
-#18 := (:var 0 S4)
-#17 := (:var 1 S3)
-#16 := (:var 2 S3)
-#19 := (f5 #16 #17 #18)
-#678 := (pattern #19)
-#23 := (f6 #17 #18)
-#96 := (= f1 #23)
-#21 := (f6 #16 #18)
-#93 := (= f1 #21)
-#99 := (or #93 #96)
-#89 := (= f1 #19)
-#102 := (iff #89 #99)
-#679 := (forall (vars (?v0 S3) (?v1 S3) (?v2 S4)) (:pat #678) #102)
-#105 := (forall (vars (?v0 S3) (?v1 S3) (?v2 S4)) #102)
-#682 := (iff #105 #679)
-#680 := (iff #102 #102)
-#681 := [refl]: #680
-#683 := [quant-intro #681]: #682
-#160 := (~ #105 #105)
-#174 := (~ #102 #102)
-#175 := [refl]: #174
-#161 := [nnf-pos #175]: #160
-#24 := (= #23 f1)
-#22 := (= #21 f1)
-#25 := (or #22 #24)
-#20 := (= #19 f1)
-#26 := (iff #20 #25)
-#27 := (forall (vars (?v0 S3) (?v1 S3) (?v2 S4)) #26)
-#106 := (iff #27 #105)
-#103 := (iff #26 #102)
-#100 := (iff #25 #99)
-#97 := (iff #24 #96)
-#98 := [rewrite]: #97
-#94 := (iff #22 #93)
-#95 := [rewrite]: #94
-#101 := [monotonicity #95 #98]: #100
-#91 := (iff #20 #89)
-#92 := [rewrite]: #91
-#104 := [monotonicity #92 #101]: #103
-#107 := [quant-intro #104]: #106
-#88 := [asserted]: #27
-#110 := [mp #88 #107]: #105
-#176 := [mp~ #110 #161]: #105
-#684 := [mp #176 #683]: #679
-#325 := (not #679)
-#659 := (or #325 #142)
-#660 := [quant-inst #39 #40 #41]: #659
-#312 := [unit-resolution #660 #684]: #142
-#661 := (or #145 #129 #326)
-#662 := [def-axiom]: #661
-#296 := [unit-resolution #662 #312]: #655
-#639 := [unit-resolution #296 #324 #652]: false
-#300 := [lemma #639]: #129
-#313 := (or #326 #148)
-#656 := (or #326 #148 #266)
-#658 := [def-axiom]: #656
-#445 := [unit-resolution #658 #156]: #313
-#301 := [unit-resolution #445 #300]: #326
-#302 := (or #148 #139)
-#657 := (or #145 #148 #139)
-#663 := [def-axiom]: #657
-#303 := [unit-resolution #663 #312]: #302
-[unit-resolution #303 #301 #300]: false
-unsat
-b364582b466f46f7d7a33b311dc9888a3ab60e44 154 0
-#2 := false
-decl f3 :: (-> S3 S2 S1)
-decl f10 :: S2
-#41 := f10
-decl f4 :: S3
-#8 := f4
-#330 := (f3 f4 f10)
-decl f1 :: S1
-#4 := f1
-#327 := (= f1 #330)
-decl f9 :: S3
-#40 := f9
-#44 := (f3 f9 f10)
-#130 := (= f1 #44)
-#331 := (or #130 #327)
-decl f6 :: (-> S3 S3 S2 S1)
-#42 := (f6 f9 f4 f10)
-#126 := (= f1 #42)
-#139 := (not #126)
-#647 := [hypothesis]: #139
-#325 := (or #130 #126)
-#140 := (iff #130 #139)
-#45 := (= #44 f1)
-#43 := (= #42 f1)
-#46 := (iff #43 #45)
-#47 := (not #46)
-#143 := (iff #47 #140)
-#133 := (iff #126 #130)
-#136 := (not #133)
-#141 := (iff #136 #140)
-#142 := [rewrite]: #141
-#137 := (iff #47 #136)
-#134 := (iff #46 #133)
-#131 := (iff #45 #130)
-#132 := [rewrite]: #131
-#128 := (iff #43 #126)
-#129 := [rewrite]: #128
-#135 := [monotonicity #129 #132]: #134
-#138 := [monotonicity #135]: #137
-#144 := [trans #138 #142]: #143
-#125 := [asserted]: #47
-#147 := [mp #125 #144]: #140
-#237 := (not #140)
-#324 := (or #130 #126 #237)
-#238 := [def-axiom]: #324
-#239 := [unit-resolution #238 #147]: #325
-#649 := [unit-resolution #239 #647]: #130
-#653 := (not #331)
-#293 := (or #126 #653)
-#310 := (iff #126 #331)
-#9 := (:var 0 S2)
-#19 := (:var 1 S3)
-#18 := (:var 2 S3)
-#20 := (f6 #18 #19 #9)
-#669 := (pattern #20)
-#24 := (f3 #19 #9)
-#93 := (= f1 #24)
-#22 := (f3 #18 #9)
-#90 := (= f1 #22)
-#96 := (or #90 #93)
-#86 := (= f1 #20)
-#99 := (iff #86 #96)
-#670 := (forall (vars (?v0 S3) (?v1 S3) (?v2 S2)) (:pat #669) #99)
-#102 := (forall (vars (?v0 S3) (?v1 S3) (?v2 S2)) #99)
-#673 := (iff #102 #670)
-#671 := (iff #99 #99)
-#672 := [refl]: #671
-#674 := [quant-intro #672]: #673
-#151 := (~ #102 #102)
-#165 := (~ #99 #99)
-#166 := [refl]: #165
-#152 := [nnf-pos #166]: #151
-#25 := (= #24 f1)
-#23 := (= #22 f1)
-#26 := (or #23 #25)
-#21 := (= #20 f1)
-#27 := (iff #21 #26)
-#28 := (forall (vars (?v0 S3) (?v1 S3) (?v2 S2)) #27)
-#103 := (iff #28 #102)
-#100 := (iff #27 #99)
-#97 := (iff #26 #96)
-#94 := (iff #25 #93)
-#95 := [rewrite]: #94
-#91 := (iff #23 #90)
-#92 := [rewrite]: #91
-#98 := [monotonicity #92 #95]: #97
-#88 := (iff #21 #86)
-#89 := [rewrite]: #88
-#101 := [monotonicity #89 #98]: #100
-#104 := [quant-intro #101]: #103
-#85 := [asserted]: #28
-#107 := [mp #85 #104]: #102
-#167 := [mp~ #107 #152]: #102
-#675 := [mp #167 #674]: #670
-#304 := (not #670)
-#436 := (or #304 #310)
-#643 := [quant-inst #40 #8 #41]: #436
-#292 := [unit-resolution #643 #675]: #310
-#644 := (not #310)
-#302 := (or #644 #126 #653)
-#307 := [def-axiom]: #302
-#294 := [unit-resolution #307 #292]: #293
-#632 := [unit-resolution #294 #647]: #653
-#326 := (not #130)
-#315 := (or #331 #326)
-#316 := [def-axiom]: #315
-#633 := [unit-resolution #316 #632 #649]: false
-#634 := [lemma #633]: #126
-#635 := (or #139 #331)
-#645 := (or #644 #139 #331)
-#303 := [def-axiom]: #645
-#636 := [unit-resolution #303 #292]: #635
-#638 := [unit-resolution #636 #634]: #331
-#329 := (or #326 #139)
-#317 := (or #326 #139 #237)
-#328 := [def-axiom]: #317
-#257 := [unit-resolution #328 #147]: #329
-#640 := [unit-resolution #257 #634]: #326
-#648 := (or #653 #130 #327)
-#654 := [def-axiom]: #648
-#278 := [unit-resolution #654 #640 #638]: #327
-#10 := (f3 f4 #9)
-#655 := (pattern #10)
-#68 := (= f1 #10)
-#71 := (not #68)
-#656 := (forall (vars (?v0 S2)) (:pat #655) #71)
-#74 := (forall (vars (?v0 S2)) #71)
-#659 := (iff #74 #656)
-#657 := (iff #71 #71)
-#658 := [refl]: #657
-#660 := [quant-intro #658]: #659
-#161 := (~ #74 #74)
-#159 := (~ #71 #71)
-#160 := [refl]: #159
-#162 := [nnf-pos #160]: #161
-#11 := (= #10 f1)
-#12 := (not #11)
-#13 := (forall (vars (?v0 S2)) #12)
-#75 := (iff #13 #74)
-#72 := (iff #12 #71)
-#69 := (iff #11 #68)
-#70 := [rewrite]: #69
-#73 := [monotonicity #70]: #72
-#76 := [quant-intro #73]: #75
-#67 := [asserted]: #13
-#79 := [mp #67 #76]: #74
-#146 := [mp~ #79 #162]: #74
-#661 := [mp #146 #660]: #656
-#650 := (not #327)
-#631 := (not #656)
-#637 := (or #631 #650)
-#273 := [quant-inst #41]: #637
-[unit-resolution #273 #661 #278]: false
-unsat
-7d907ff63da540f87f38f6be518dd4d79ce5f3db 128 0
-#2 := false
-decl f4 :: (-> S4 S3 S1)
-decl f10 :: S3
-#41 := f10
-decl f5 :: S4
-#13 := f5
-#222 := (f4 f5 f10)
-decl f1 :: S1
-#4 := f1
-#309 := (= f1 #222)
-#636 := (not #309)
-decl f9 :: S4
-#40 := f9
-#223 := (f4 f9 f10)
-#310 := (= f1 #223)
-#302 := (or #309 #310)
-#287 := (not #302)
-decl f6 :: (-> S4 S4 S3 S1)
-#42 := (f6 f9 f5 f10)
-#123 := (= f1 #42)
-#242 := (iff #123 #302)
-#14 := (:var 0 S3)
-#19 := (:var 1 S4)
-#18 := (:var 2 S4)
-#20 := (f6 #18 #19 #14)
-#654 := (pattern #20)
-#24 := (f4 #19 #14)
-#90 := (= f1 #24)
-#22 := (f4 #18 #14)
-#87 := (= f1 #22)
-#93 := (or #87 #90)
-#83 := (= f1 #20)
-#96 := (iff #83 #93)
-#655 := (forall (vars (?v0 S4) (?v1 S4) (?v2 S3)) (:pat #654) #96)
-#99 := (forall (vars (?v0 S4) (?v1 S4) (?v2 S3)) #96)
-#658 := (iff #99 #655)
-#656 := (iff #96 #96)
-#657 := [refl]: #656
-#659 := [quant-intro #657]: #658
-#136 := (~ #99 #99)
-#150 := (~ #96 #96)
-#151 := [refl]: #150
-#137 := [nnf-pos #151]: #136
-#25 := (= #24 f1)
-#23 := (= #22 f1)
-#26 := (or #23 #25)
-#21 := (= #20 f1)
-#27 := (iff #21 #26)
-#28 := (forall (vars (?v0 S4) (?v1 S4) (?v2 S3)) #27)
-#100 := (iff #28 #99)
-#97 := (iff #27 #96)
-#94 := (iff #26 #93)
-#91 := (iff #25 #90)
-#92 := [rewrite]: #91
-#88 := (iff #23 #87)
-#89 := [rewrite]: #88
-#95 := [monotonicity #89 #92]: #94
-#85 := (iff #21 #83)
-#86 := [rewrite]: #85
-#98 := [monotonicity #86 #95]: #97
-#101 := [quant-intro #98]: #100
-#82 := [asserted]: #28
-#104 := [mp #82 #101]: #99
-#152 := [mp~ #104 #137]: #99
-#660 := [mp #152 #659]: #655
-#316 := (not #655)
-#295 := (or #316 #242)
-#224 := (or #310 #309)
-#311 := (iff #123 #224)
-#632 := (or #316 #311)
-#289 := (iff #632 #295)
-#628 := (iff #295 #295)
-#300 := [rewrite]: #628
-#315 := (iff #311 #242)
-#313 := (iff #224 #302)
-#314 := [rewrite]: #313
-#312 := [monotonicity #314]: #315
-#421 := [monotonicity #312]: #289
-#301 := [trans #421 #300]: #289
-#634 := [quant-inst #40 #13 #41]: #632
-#635 := [mp #634 #301]: #295
-#618 := [unit-resolution #635 #660]: #242
-#288 := (not #242)
-#619 := (or #288 #287)
-#127 := (not #123)
-#43 := (= #42 f1)
-#44 := (not #43)
-#128 := (iff #44 #127)
-#125 := (iff #43 #123)
-#126 := [rewrite]: #125
-#129 := [monotonicity #126]: #128
-#122 := [asserted]: #44
-#132 := [mp #122 #129]: #127
-#631 := (or #288 #123 #287)
-#272 := [def-axiom]: #631
-#622 := [unit-resolution #272 #132]: #619
-#258 := [unit-resolution #622 #618]: #287
-#637 := (or #302 #636)
-#638 := [def-axiom]: #637
-#623 := [unit-resolution #638 #258]: #636
-#15 := (f4 f5 #14)
-#647 := (pattern #15)
-#75 := (= f1 #15)
-#648 := (forall (vars (?v0 S3)) (:pat #647) #75)
-#79 := (forall (vars (?v0 S3)) #75)
-#651 := (iff #79 #648)
-#649 := (iff #75 #75)
-#650 := [refl]: #649
-#652 := [quant-intro #650]: #651
-#134 := (~ #79 #79)
-#133 := (~ #75 #75)
-#148 := [refl]: #133
-#135 := [nnf-pos #148]: #134
-#16 := (= #15 f1)
-#17 := (forall (vars (?v0 S3)) #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
-#149 := [mp~ #84 #135]: #79
-#653 := [mp #149 #652]: #648
-#620 := (not #648)
-#621 := (or #620 #309)
-#616 := [quant-inst #41]: #621
-[unit-resolution #616 #653 #623]: false
-unsat
-5cdc991e87f691c3b3a175ff2ede8c62635b20a0 146 0
-#2 := false
-decl f5 :: (-> S3 S3 S4 S1)
-decl f11 :: S4
-#41 := f11
-decl f9 :: S3
-#39 := f9
-decl f10 :: S3
-#40 := f10
-#44 := (f5 f10 f9 f11)
-decl f1 :: S1
-#4 := f1
-#130 := (= f1 #44)
-#326 := (not #130)
-#42 := (f5 f9 f10 f11)
-#126 := (= f1 #42)
-#139 := (not #126)
-#245 := [hypothesis]: #139
-#325 := (or #130 #126)
-#140 := (iff #130 #139)
-#45 := (= #44 f1)
-#43 := (= #42 f1)
-#46 := (iff #43 #45)
-#47 := (not #46)
-#143 := (iff #47 #140)
-#133 := (iff #126 #130)
-#136 := (not #133)
-#141 := (iff #136 #140)
-#142 := [rewrite]: #141
-#137 := (iff #47 #136)
-#134 := (iff #46 #133)
-#131 := (iff #45 #130)
-#132 := [rewrite]: #131
-#128 := (iff #43 #126)
-#129 := [rewrite]: #128
-#135 := [monotonicity #129 #132]: #134
-#138 := [monotonicity #135]: #137
-#144 := [trans #138 #142]: #143
-#125 := [asserted]: #47
-#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
-decl f6 :: (-> S3 S4 S1)
-#330 := (f6 f9 f11)
-#327 := (= f1 #330)
-#331 := (f6 f10 f11)
-#310 := (= f1 #331)
-#647 := (or #310 #327)
-#644 := (not #647)
-#347 := (or #126 #644)
-#634 := (iff #126 #647)
-#18 := (:var 0 S4)
-#17 := (:var 1 S3)
-#16 := (:var 2 S3)
-#19 := (f5 #16 #17 #18)
-#669 := (pattern #19)
-#23 := (f6 #17 #18)
-#93 := (= f1 #23)
-#21 := (f6 #16 #18)
-#90 := (= f1 #21)
-#96 := (or #90 #93)
-#86 := (= f1 #19)
-#99 := (iff #86 #96)
-#670 := (forall (vars (?v0 S3) (?v1 S3) (?v2 S4)) (:pat #669) #99)
-#102 := (forall (vars (?v0 S3) (?v1 S3) (?v2 S4)) #99)
-#673 := (iff #102 #670)
-#671 := (iff #99 #99)
-#672 := [refl]: #671
-#674 := [quant-intro #672]: #673
-#151 := (~ #102 #102)
-#165 := (~ #99 #99)
-#166 := [refl]: #165
-#152 := [nnf-pos #166]: #151
-#24 := (= #23 f1)
-#22 := (= #21 f1)
-#25 := (or #22 #24)
-#20 := (= #19 f1)
-#26 := (iff #20 #25)
-#27 := (forall (vars (?v0 S3) (?v1 S3) (?v2 S4)) #26)
-#103 := (iff #27 #102)
-#100 := (iff #26 #99)
-#97 := (iff #25 #96)
-#94 := (iff #24 #93)
-#95 := [rewrite]: #94
-#91 := (iff #22 #90)
-#92 := [rewrite]: #91
-#98 := [monotonicity #92 #95]: #97
-#88 := (iff #20 #86)
-#89 := [rewrite]: #88
-#101 := [monotonicity #89 #98]: #100
-#104 := [quant-intro #101]: #103
-#85 := [asserted]: #27
-#107 := [mp #85 #104]: #102
-#167 := [mp~ #107 #152]: #102
-#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 #39 #40 #41]: #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 #40 #39 #41]: #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
-fa2f9bd8c428cc56374865b6337a9b9b3979db13 121 0
-#2 := false
-decl f5 :: (-> S3 S3 S4 S1)
-decl f10 :: S4
-#40 := f10
-decl f9 :: S3
-#39 := f9
-#41 := (f5 f9 f9 f10)
-decl f1 :: S1
-#4 := f1
-#125 := (= f1 #41)
-#138 := (not #125)
-#629 := [hypothesis]: #138
-decl f6 :: (-> S3 S4 S1)
-#43 := (f6 f9 f10)
-#129 := (= f1 #43)
-#324 := (or #129 #125)
-#139 := (iff #129 #138)
-#44 := (= #43 f1)
-#42 := (= #41 f1)
-#45 := (iff #42 #44)
-#46 := (not #45)
-#142 := (iff #46 #139)
-#132 := (iff #125 #129)
-#135 := (not #132)
-#140 := (iff #135 #139)
-#141 := [rewrite]: #140
-#136 := (iff #46 #135)
-#133 := (iff #45 #132)
-#130 := (iff #44 #129)
-#131 := [rewrite]: #130
-#127 := (iff #42 #125)
-#128 := [rewrite]: #127
-#134 := [monotonicity #128 #131]: #133
-#137 := [monotonicity #134]: #136
-#143 := [trans #137 #141]: #142
-#124 := [asserted]: #46
-#146 := [mp #124 #143]: #139
-#236 := (not #139)
-#323 := (or #129 #125 #236)
-#237 := [def-axiom]: #323
-#238 := [unit-resolution #237 #146]: #324
-#290 := [unit-resolution #238 #629]: #129
-#325 := (not #129)
-#292 := (or #125 #325)
-#18 := (:var 0 S4)
-#17 := (:var 1 S3)
-#16 := (:var 2 S3)
-#19 := (f5 #16 #17 #18)
-#668 := (pattern #19)
-#23 := (f6 #17 #18)
-#92 := (= f1 #23)
-#21 := (f6 #16 #18)
-#89 := (= f1 #21)
-#95 := (or #89 #92)
-#85 := (= f1 #19)
-#98 := (iff #85 #95)
-#669 := (forall (vars (?v0 S3) (?v1 S3) (?v2 S4)) (:pat #668) #98)
-#101 := (forall (vars (?v0 S3) (?v1 S3) (?v2 S4)) #98)
-#672 := (iff #101 #669)
-#670 := (iff #98 #98)
-#671 := [refl]: #670
-#673 := [quant-intro #671]: #672
-#150 := (~ #101 #101)
-#164 := (~ #98 #98)
-#165 := [refl]: #164
-#151 := [nnf-pos #165]: #150
-#24 := (= #23 f1)
-#22 := (= #21 f1)
-#25 := (or #22 #24)
-#20 := (= #19 f1)
-#26 := (iff #20 #25)
-#27 := (forall (vars (?v0 S3) (?v1 S3) (?v2 S4)) #26)
-#102 := (iff #27 #101)
-#99 := (iff #26 #98)
-#96 := (iff #25 #95)
-#93 := (iff #24 #92)
-#94 := [rewrite]: #93
-#90 := (iff #22 #89)
-#91 := [rewrite]: #90
-#97 := [monotonicity #91 #94]: #96
-#87 := (iff #20 #85)
-#88 := [rewrite]: #87
-#100 := [monotonicity #88 #97]: #99
-#103 := [quant-intro #100]: #102
-#84 := [asserted]: #27
-#106 := [mp #84 #103]: #101
-#166 := [mp~ #106 #151]: #101
-#674 := [mp #166 #673]: #669
-#303 := (not #669)
-#435 := (or #303 #132)
-#329 := (or #129 #129)
-#326 := (iff #125 #329)
-#642 := (or #303 #326)
-#315 := (iff #642 #435)
-#650 := (iff #435 #435)
-#651 := [rewrite]: #650
-#646 := (iff #326 #132)
-#330 := (iff #329 #129)
-#309 := [rewrite]: #330
-#648 := [monotonicity #309]: #646
-#649 := [monotonicity #648]: #315
-#652 := [trans #649 #651]: #315
-#314 := [quant-inst #39 #39 #40]: #642
-#647 := [mp #314 #652]: #435
-#291 := [unit-resolution #647 #674]: #132
-#653 := (or #135 #125 #325)
-#643 := [def-axiom]: #653
-#293 := [unit-resolution #643 #291]: #292
-#631 := [unit-resolution #293 #290 #629]: false
-#632 := [lemma #631]: #125
-#328 := (or #325 #138)
-#316 := (or #325 #138 #236)
-#327 := [def-axiom]: #316
-#256 := [unit-resolution #327 #146]: #328
-#633 := [unit-resolution #256 #632]: #325
-#634 := (or #138 #129)
-#301 := (or #135 #138 #129)
-#306 := [def-axiom]: #301
-#635 := [unit-resolution #306 #291]: #634
-[unit-resolution #635 #633 #632]: false
-unsat
-63dfbec334f0b24e14d14e8841f417fc16248602 259 0
-#2 := false
-decl f5 :: (-> S3 S4 S1)
-decl f12 :: S4
-#45 := f12
-decl f10 :: S3
-#41 := f10
-#625 := (f5 f10 f12)
-decl f1 :: S1
-#4 := f1
-#338 := (= f1 #625)
-decl f11 :: S3
-#42 := f11
-#336 := (f5 f11 f12)
-#333 := (= f1 #336)
-#623 := (or #333 #338)
-decl f6 :: (-> S3 S3 S3)
-#43 := (f6 f10 f11)
-#310 := (f5 #43 f12)
-#442 := (= f1 #310)
-#617 := (iff #442 #623)
-#583 := (not #617)
-#595 := (not #623)
-#607 := (not #338)
-decl f9 :: S3
-#40 := f9
-#638 := (f5 f9 f12)
-#639 := (= f1 #638)
-#485 := (or #338 #639)
-#610 := (not #485)
-#48 := (f6 f9 f10)
-#337 := (f5 #48 f12)
-#316 := (= f1 #337)
-#593 := (iff #316 #485)
-#585 := (not #593)
-#578 := [hypothesis]: #585
-#19 := (:var 0 S4)
-#17 := (:var 1 S3)
-#16 := (:var 2 S3)
-#18 := (f6 #16 #17)
-#20 := (f5 #18 #19)
-#675 := (pattern #20)
-#24 := (f5 #17 #19)
-#99 := (= f1 #24)
-#22 := (f5 #16 #19)
-#96 := (= f1 #22)
-#102 := (or #96 #99)
-#92 := (= f1 #20)
-#105 := (iff #92 #102)
-#676 := (forall (vars (?v0 S3) (?v1 S3) (?v2 S4)) (:pat #675) #105)
-#108 := (forall (vars (?v0 S3) (?v1 S3) (?v2 S4)) #105)
-#679 := (iff #108 #676)
-#677 := (iff #105 #105)
-#678 := [refl]: #677
-#680 := [quant-intro #678]: #679
-#157 := (~ #108 #108)
-#171 := (~ #105 #105)
-#172 := [refl]: #171
-#158 := [nnf-pos #172]: #157
-#25 := (= #24 f1)
-#23 := (= #22 f1)
-#26 := (or #23 #25)
-#21 := (= #20 f1)
-#27 := (iff #21 #26)
-#28 := (forall (vars (?v0 S3) (?v1 S3) (?v2 S4)) #27)
-#109 := (iff #28 #108)
-#106 := (iff #27 #105)
-#103 := (iff #26 #102)
-#100 := (iff #25 #99)
-#101 := [rewrite]: #100
-#97 := (iff #23 #96)
-#98 := [rewrite]: #97
-#104 := [monotonicity #98 #101]: #103
-#94 := (iff #21 #92)
-#95 := [rewrite]: #94
-#107 := [monotonicity #95 #104]: #106
-#110 := [quant-intro #107]: #109
-#91 := [asserted]: #28
-#113 := [mp #91 #110]: #108
-#173 := [mp~ #113 #158]: #108
-#681 := [mp #173 #680]: #676
-#649 := (not #676)
-#591 := (or #649 #593)
-#602 := (or #639 #338)
-#484 := (iff #316 #602)
-#594 := (or #649 #484)
-#494 := (iff #594 #591)
-#497 := (iff #591 #591)
-#490 := [rewrite]: #497
-#495 := (iff #484 #593)
-#486 := (iff #602 #485)
-#445 := [rewrite]: #486
-#590 := [monotonicity #445]: #495
-#496 := [monotonicity #590]: #494
-#498 := [trans #496 #490]: #494
-#479 := [quant-inst #40 #41 #45]: #594
-#499 := [mp #479 #498]: #591
-#579 := [unit-resolution #499 #681 #578]: false
-#580 := [lemma #579]: #593
-#656 := (not #316)
-#653 := (or #316 #333)
-#650 := (not #653)
-#49 := (f6 #48 f11)
-#50 := (f5 #49 f12)
-#136 := (= f1 #50)
-#332 := (not #136)
-#44 := (f6 f9 #43)
-#46 := (f5 #44 f12)
-#132 := (= f1 #46)
-#145 := (not #132)
-#581 := [hypothesis]: #145
-#331 := (or #136 #132)
-#146 := (iff #136 #145)
-#51 := (= #50 f1)
-#47 := (= #46 f1)
-#52 := (iff #47 #51)
-#53 := (not #52)
-#149 := (iff #53 #146)
-#139 := (iff #132 #136)
-#142 := (not #139)
-#147 := (iff #142 #146)
-#148 := [rewrite]: #147
-#143 := (iff #53 #142)
-#140 := (iff #52 #139)
-#137 := (iff #51 #136)
-#138 := [rewrite]: #137
-#134 := (iff #47 #132)
-#135 := [rewrite]: #134
-#141 := [monotonicity #135 #138]: #140
-#144 := [monotonicity #141]: #143
-#150 := [trans #144 #148]: #149
-#131 := [asserted]: #53
-#153 := [mp #131 #150]: #146
-#243 := (not #146)
-#330 := (or #136 #132 #243)
-#244 := [def-axiom]: #330
-#245 := [unit-resolution #244 #153]: #331
-#575 := [unit-resolution #245 #581]: #136
-#566 := (or #332 #653)
-#655 := (iff #136 #653)
-#321 := (or #649 #655)
-#322 := [quant-inst #48 #42 #45]: #321
-#582 := [unit-resolution #322 #681]: #655
-#651 := (not #655)
-#293 := (or #651 #332 #653)
-#636 := [def-axiom]: #293
-#567 := [unit-resolution #636 #582]: #566
-#569 := [unit-resolution #567 #575]: #653
-#659 := (not #333)
-#599 := (or #649 #617)
-#622 := (or #338 #333)
-#626 := (iff #442 #622)
-#619 := (or #649 #626)
-#614 := (iff #619 #599)
-#621 := (iff #599 #599)
-#462 := [rewrite]: #621
-#618 := (iff #626 #617)
-#627 := (iff #622 #623)
-#616 := [rewrite]: #627
-#613 := [monotonicity #616]: #618
-#615 := [monotonicity #613]: #614
-#463 := [trans #615 #462]: #614
-#620 := [quant-inst #41 #42 #45]: #619
-#464 := [mp #620 #463]: #599
-#570 := [unit-resolution #464 #681]: #617
-#560 := (or #583 #595)
-#358 := (not #442)
-#642 := (or #442 #639)
-#631 := (not #642)
-#572 := (or #132 #631)
-#279 := (iff #132 #642)
-#284 := (or #649 #279)
-#640 := (or #639 #442)
-#641 := (iff #132 #640)
-#285 := (or #649 #641)
-#645 := (iff #285 #284)
-#634 := (iff #284 #284)
-#635 := [rewrite]: #634
-#644 := (iff #641 #279)
-#637 := (iff #640 #642)
-#643 := [rewrite]: #637
-#646 := [monotonicity #643]: #644
-#648 := [monotonicity #646]: #645
-#341 := [trans #648 #635]: #645
-#647 := [quant-inst #40 #43 #45]: #285
-#357 := [mp #647 #341]: #284
-#571 := [unit-resolution #357 #681]: #279
-#628 := (not #279)
-#632 := (or #628 #132 #631)
-#629 := [def-axiom]: #632
-#568 := [unit-resolution #629 #571]: #572
-#573 := [unit-resolution #568 #581]: #631
-#359 := (or #642 #358)
-#345 := [def-axiom]: #359
-#559 := [unit-resolution #345 #573]: #358
-#577 := (or #583 #442 #595)
-#574 := [def-axiom]: #577
-#562 := [unit-resolution #574 #559]: #560
-#563 := [unit-resolution #562 #570]: #595
-#606 := (or #623 #659)
-#500 := [def-axiom]: #606
-#564 := [unit-resolution #500 #563]: #659
-#308 := (or #650 #316 #333)
-#313 := [def-axiom]: #308
-#561 := [unit-resolution #313 #564 #569]: #316
-#360 := (not #639)
-#251 := (or #642 #360)
-#630 := [def-axiom]: #251
-#565 := [unit-resolution #630 #573]: #360
-#501 := (or #623 #607)
-#502 := [def-axiom]: #501
-#545 := [unit-resolution #502 #563]: #607
-#611 := (or #610 #338 #639)
-#605 := [def-axiom]: #611
-#546 := [unit-resolution #605 #545 #565]: #610
-#443 := (or #585 #656 #485)
-#444 := [def-axiom]: #443
-#548 := [unit-resolution #444 #546 #561 #580]: false
-#549 := [lemma #548]: #132
-#335 := (or #332 #145)
-#323 := (or #332 #145 #243)
-#334 := [def-axiom]: #323
-#263 := [unit-resolution #334 #153]: #335
-#550 := [unit-resolution #263 #549]: #332
-#551 := (or #136 #650)
-#309 := (or #651 #136 #650)
-#652 := [def-axiom]: #309
-#552 := [unit-resolution #652 #582]: #551
-#553 := [unit-resolution #552 #550]: #650
-#657 := (or #653 #656)
-#658 := [def-axiom]: #657
-#554 := [unit-resolution #658 #553]: #656
-#612 := (or #585 #316 #610)
-#441 := [def-axiom]: #612
-#555 := [unit-resolution #441 #554 #580]: #610
-#608 := (or #485 #607)
-#609 := [def-axiom]: #608
-#556 := [unit-resolution #609 #555]: #607
-#654 := (or #653 #659)
-#660 := [def-axiom]: #654
-#557 := [unit-resolution #660 #553]: #659
-#592 := (or #595 #333 #338)
-#596 := [def-axiom]: #592
-#547 := [unit-resolution #596 #557 #556]: #595
-#558 := (or #145 #642)
-#633 := (or #628 #145 #642)
-#342 := [def-axiom]: #633
-#536 := [unit-resolution #342 #571]: #558
-#537 := [unit-resolution #536 #549]: #642
-#603 := (or #485 #360)
-#604 := [def-axiom]: #603
-#539 := [unit-resolution #604 #555]: #360
-#353 := (or #631 #442 #639)
-#354 := [def-axiom]: #353
-#540 := [unit-resolution #354 #539 #537]: #442
-#576 := (or #583 #358 #623)
-#586 := [def-axiom]: #576
-#541 := [unit-resolution #586 #540 #547]: #583
-[unit-resolution #464 #681 #541]: false
-unsat
-b9a56cfd9dd84219baf29a97bb74d87de1fcb3ba 153 0
-#2 := false
-decl f8 :: (-> S4 S5 S1)
-decl f11 :: S5
-#41 := f11
-decl f10 :: S4
-#40 := f10
-#46 := (f8 f10 f11)
-decl f1 :: S1
-#4 := f1
-#136 := (= f1 #46)
-#190 := (not #136)
-decl f9 :: S4
-#39 := f9
-#44 := (f8 f9 f11)
-#133 := (= f1 #44)
-#189 := (not #133)
-#191 := (or #189 #190)
-#192 := (not #191)
-#333 := [hypothesis]: #192
-decl f7 :: (-> S4 S4 S5 S1)
-#42 := (f7 f9 f10 f11)
-#129 := (= f1 #42)
-#148 := (not #129)
-#339 := (or #148 #191)
-#203 := (iff #129 #191)
-#139 := (and #133 #136)
-#149 := (iff #139 #148)
-#206 := (iff #149 #203)
-#198 := (iff #191 #129)
-#204 := (iff #198 #203)
-#205 := [rewrite]: #204
-#201 := (iff #149 #198)
-#195 := (iff #192 #148)
-#199 := (iff #195 #198)
-#200 := [rewrite]: #199
-#196 := (iff #149 #195)
-#193 := (iff #139 #192)
-#194 := [rewrite]: #193
-#197 := [monotonicity #194]: #196
-#202 := [trans #197 #200]: #201
-#207 := [trans #202 #205]: #206
-#47 := (= #46 f1)
-#45 := (= #44 f1)
-#48 := (and #45 #47)
-#43 := (= #42 f1)
-#49 := (iff #43 #48)
-#50 := (not #49)
-#152 := (iff #50 #149)
-#142 := (iff #129 #139)
-#145 := (not #142)
-#150 := (iff #145 #149)
-#151 := [rewrite]: #150
-#146 := (iff #50 #145)
-#143 := (iff #49 #142)
-#140 := (iff #48 #139)
-#137 := (iff #47 #136)
-#138 := [rewrite]: #137
-#134 := (iff #45 #133)
-#135 := [rewrite]: #134
-#141 := [monotonicity #135 #138]: #140
-#131 := (iff #43 #129)
-#132 := [rewrite]: #131
-#144 := [monotonicity #132 #141]: #143
-#147 := [monotonicity #144]: #146
-#153 := [trans #147 #151]: #152
-#128 := [asserted]: #50
-#156 := [mp #128 #153]: #149
-#208 := [mp #156 #207]: #203
-#346 := (not #203)
-#356 := (or #148 #191 #346)
-#360 := [def-axiom]: #356
-#676 := [unit-resolution #360 #208]: #339
-#465 := [unit-resolution #676 #333]: #148
-#332 := (or #129 #191)
-#678 := (iff #129 #192)
-#29 := (:var 0 S5)
-#28 := (:var 1 S4)
-#27 := (:var 2 S4)
-#30 := (f7 #27 #28 #29)
-#705 := (pattern #30)
-#34 := (f8 #28 #29)
-#116 := (= f1 #34)
-#181 := (not #116)
-#32 := (f8 #27 #29)
-#113 := (= f1 #32)
-#180 := (not #113)
-#164 := (or #180 #181)
-#165 := (not #164)
-#109 := (= f1 #30)
-#182 := (iff #109 #165)
-#706 := (forall (vars (?v0 S4) (?v1 S4) (?v2 S5)) (:pat #705) #182)
-#185 := (forall (vars (?v0 S4) (?v1 S4) (?v2 S5)) #182)
-#709 := (iff #185 #706)
-#707 := (iff #182 #182)
-#708 := [refl]: #707
-#710 := [quant-intro #708]: #709
-#119 := (and #113 #116)
-#122 := (iff #109 #119)
-#125 := (forall (vars (?v0 S4) (?v1 S4) (?v2 S5)) #122)
-#186 := (iff #125 #185)
-#183 := (iff #122 #182)
-#166 := (iff #119 #165)
-#167 := [rewrite]: #166
-#184 := [monotonicity #167]: #183
-#187 := [quant-intro #184]: #186
-#162 := (~ #125 #125)
-#177 := (~ #122 #122)
-#178 := [refl]: #177
-#163 := [nnf-pos #178]: #162
-#35 := (= #34 f1)
-#33 := (= #32 f1)
-#36 := (and #33 #35)
-#31 := (= #30 f1)
-#37 := (iff #31 #36)
-#38 := (forall (vars (?v0 S4) (?v1 S4) (?v2 S5)) #37)
-#126 := (iff #38 #125)
-#123 := (iff #37 #122)
-#120 := (iff #36 #119)
-#117 := (iff #35 #116)
-#118 := [rewrite]: #117
-#114 := (iff #33 #113)
-#115 := [rewrite]: #114
-#121 := [monotonicity #115 #118]: #120
-#111 := (iff #31 #109)
-#112 := [rewrite]: #111
-#124 := [monotonicity #112 #121]: #123
-#127 := [quant-intro #124]: #126
-#108 := [asserted]: #38
-#130 := [mp #108 #127]: #125
-#179 := [mp~ #130 #163]: #125
-#188 := [mp #179 #187]: #185
-#711 := [mp #188 #710]: #706
-#672 := (not #706)
-#344 := (or #672 #678)
-#345 := [quant-inst #39 #40 #41]: #344
-#674 := [unit-resolution #345 #711]: #678
-#679 := (not #678)
-#680 := (or #679 #129 #191)
-#681 := [def-axiom]: #680
-#675 := [unit-resolution #681 #674]: #332
-#316 := [unit-resolution #675 #465 #333]: false
-#659 := [lemma #316]: #191
-#286 := (or #129 #192)
-#357 := (or #129 #192 #346)
-#358 := [def-axiom]: #357
-#359 := [unit-resolution #358 #208]: #286
-#320 := [unit-resolution #359 #659]: #129
-#321 := (or #148 #192)
-#682 := (or #679 #148 #192)
-#677 := [def-axiom]: #682
-#322 := [unit-resolution #677 #674]: #321
-[unit-resolution #322 #320 #659]: false
-unsat
-7f98a59af5916f5d5b5c30234aa00391b0645729 141 0
-#2 := false
-decl f3 :: (-> S3 S2 S1)
-decl f10 :: S2
-#41 := f10
-decl f4 :: S3
-#8 := f4
-#230 := (f3 f4 f10)
-decl f1 :: S1
-#4 := f1
-#317 := (= f1 #230)
-#231 := (not #317)
-decl f9 :: S3
-#40 := f9
-#318 := (f3 f9 f10)
-#232 := (= f1 #318)
-#319 := (not #232)
-#310 := (or #319 #231)
-#321 := (not #310)
-decl f8 :: (-> S3 S3 S2 S1)
-#42 := (f8 f9 f4 f10)
-#124 := (= f1 #42)
-#322 := (iff #124 #321)
-#9 := (:var 0 S2)
-#30 := (:var 1 S3)
-#29 := (:var 2 S3)
-#31 := (f8 #29 #30 #9)
-#669 := (pattern #31)
-#35 := (f3 #30 #9)
-#111 := (= f1 #35)
-#165 := (not #111)
-#33 := (f3 #29 #9)
-#108 := (= f1 #33)
-#164 := (not #108)
-#148 := (or #164 #165)
-#149 := (not #148)
-#104 := (= f1 #31)
-#166 := (iff #104 #149)
-#670 := (forall (vars (?v0 S3) (?v1 S3) (?v2 S2)) (:pat #669) #166)
-#169 := (forall (vars (?v0 S3) (?v1 S3) (?v2 S2)) #166)
-#673 := (iff #169 #670)
-#671 := (iff #166 #166)
-#672 := [refl]: #671
-#674 := [quant-intro #672]: #673
-#114 := (and #108 #111)
-#117 := (iff #104 #114)
-#120 := (forall (vars (?v0 S3) (?v1 S3) (?v2 S2)) #117)
-#170 := (iff #120 #169)
-#167 := (iff #117 #166)
-#150 := (iff #114 #149)
-#151 := [rewrite]: #150
-#168 := [monotonicity #151]: #167
-#171 := [quant-intro #168]: #170
-#146 := (~ #120 #120)
-#161 := (~ #117 #117)
-#162 := [refl]: #161
-#147 := [nnf-pos #162]: #146
-#36 := (= #35 f1)
-#34 := (= #33 f1)
-#37 := (and #34 #36)
-#32 := (= #31 f1)
-#38 := (iff #32 #37)
-#39 := (forall (vars (?v0 S3) (?v1 S3) (?v2 S2)) #38)
-#121 := (iff #39 #120)
-#118 := (iff #38 #117)
-#115 := (iff #37 #114)
-#112 := (iff #36 #111)
-#113 := [rewrite]: #112
-#109 := (iff #34 #108)
-#110 := [rewrite]: #109
-#116 := [monotonicity #110 #113]: #115
-#106 := (iff #32 #104)
-#107 := [rewrite]: #106
-#119 := [monotonicity #107 #116]: #118
-#122 := [quant-intro #119]: #121
-#103 := [asserted]: #39
-#125 := [mp #103 #122]: #120
-#163 := [mp~ #125 #147]: #120
-#172 := [mp #163 #171]: #169
-#675 := [mp #172 #674]: #670
-#320 := (not #670)
-#324 := (or #320 #322)
-#303 := [quant-inst #40 #8 #41]: #324
-#250 := [unit-resolution #303 #675]: #322
-#309 := (not #322)
-#323 := (or #309 #321)
-#43 := (= #42 f1)
-#44 := (not #43)
-#45 := (not #44)
-#136 := (iff #45 #124)
-#128 := (not #124)
-#131 := (not #128)
-#134 := (iff #131 #124)
-#135 := [rewrite]: #134
-#132 := (iff #45 #131)
-#129 := (iff #44 #128)
-#126 := (iff #43 #124)
-#127 := [rewrite]: #126
-#130 := [monotonicity #127]: #129
-#133 := [monotonicity #130]: #132
-#137 := [trans #133 #135]: #136
-#123 := [asserted]: #45
-#140 := [mp #123 #137]: #124
-#645 := (or #309 #128 #321)
-#646 := [def-axiom]: #645
-#639 := [unit-resolution #646 #140]: #323
-#280 := [unit-resolution #639 #250]: #321
-#297 := (or #310 #317)
-#429 := [def-axiom]: #297
-#623 := [unit-resolution #429 #280]: #317
-#10 := (f3 f4 #9)
-#648 := (pattern #10)
-#66 := (= f1 #10)
-#69 := (not #66)
-#649 := (forall (vars (?v0 S2)) (:pat #648) #69)
-#72 := (forall (vars (?v0 S2)) #69)
-#652 := (iff #72 #649)
-#650 := (iff #69 #69)
-#651 := [refl]: #650
-#653 := [quant-intro #651]: #652
-#154 := (~ #72 #72)
-#152 := (~ #69 #69)
-#153 := [refl]: #152
-#155 := [nnf-pos #153]: #154
-#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
-#139 := [mp~ #77 #155]: #72
-#654 := [mp #139 #653]: #649
-#300 := (not #649)
-#638 := (or #300 #231)
-#296 := [quant-inst #41]: #638
-[unit-resolution #296 #654 #623]: false
-unsat
-b75cfd5dcf910762f51953bce5714d91441e0375 165 0
-#2 := false
-decl f4 :: (-> S4 S3 S1)
-decl f10 :: S3
-#41 := f10
-decl f9 :: S4
-#40 := f9
-#44 := (f4 f9 f10)
-decl f1 :: S1
-#4 := f1
-#130 := (= f1 #44)
-#326 := (not #130)
-decl f8 :: (-> S4 S4 S3 S1)
-decl f5 :: S4
-#13 := f5
-#42 := (f8 f9 f5 f10)
-#126 := (= f1 #42)
-#330 := (f4 f5 f10)
-#327 := (= f1 #330)
-#331 := (not #327)
-#304 := [hypothesis]: #331
-#14 := (:var 0 S3)
-#15 := (f4 f5 #14)
-#662 := (pattern #15)
-#78 := (= f1 #15)
-#663 := (forall (vars (?v0 S3)) (:pat #662) #78)
-#82 := (forall (vars (?v0 S3)) #78)
-#666 := (iff #82 #663)
-#664 := (iff #78 #78)
-#665 := [refl]: #664
-#667 := [quant-intro #665]: #666
-#149 := (~ #82 #82)
-#148 := (~ #78 #78)
-#163 := [refl]: #148
-#150 := [nnf-pos #163]: #149
-#16 := (= #15 f1)
-#17 := (forall (vars (?v0 S3)) #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
-#164 := [mp~ #87 #150]: #82
-#668 := [mp #164 #667]: #663
-#292 := (not #663)
-#293 := (or #292 #327)
-#294 := [quant-inst #41]: #293
-#436 := [unit-resolution #294 #668 #304]: false
-#632 := [lemma #436]: #327
-#139 := (not #126)
-#633 := [hypothesis]: #139
-#325 := (or #130 #126)
-#140 := (iff #130 #139)
-#45 := (= #44 f1)
-#43 := (= #42 f1)
-#46 := (iff #43 #45)
-#47 := (not #46)
-#143 := (iff #47 #140)
-#133 := (iff #126 #130)
-#136 := (not #133)
-#141 := (iff #136 #140)
-#142 := [rewrite]: #141
-#137 := (iff #47 #136)
-#134 := (iff #46 #133)
-#131 := (iff #45 #130)
-#132 := [rewrite]: #131
-#128 := (iff #43 #126)
-#129 := [rewrite]: #128
-#135 := [monotonicity #129 #132]: #134
-#138 := [monotonicity #135]: #137
-#144 := [trans #138 #142]: #143
-#125 := [asserted]: #47
-#147 := [mp #125 #144]: #140
-#237 := (not #140)
-#324 := (or #130 #126 #237)
-#238 := [def-axiom]: #324
-#239 := [unit-resolution #238 #147]: #325
-#634 := [unit-resolution #239 #633]: #130
-#310 := (or #326 #331)
-#636 := (or #126 #310)
-#647 := (not #310)
-#649 := (iff #126 #647)
-#30 := (:var 1 S4)
-#29 := (:var 2 S4)
-#31 := (f8 #29 #30 #14)
-#676 := (pattern #31)
-#35 := (f4 #30 #14)
-#113 := (= f1 #35)
-#172 := (not #113)
-#33 := (f4 #29 #14)
-#110 := (= f1 #33)
-#171 := (not #110)
-#155 := (or #171 #172)
-#156 := (not #155)
-#106 := (= f1 #31)
-#173 := (iff #106 #156)
-#677 := (forall (vars (?v0 S4) (?v1 S4) (?v2 S3)) (:pat #676) #173)
-#176 := (forall (vars (?v0 S4) (?v1 S4) (?v2 S3)) #173)
-#680 := (iff #176 #677)
-#678 := (iff #173 #173)
-#679 := [refl]: #678
-#681 := [quant-intro #679]: #680
-#116 := (and #110 #113)
-#119 := (iff #106 #116)
-#122 := (forall (vars (?v0 S4) (?v1 S4) (?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
-#36 := (= #35 f1)
-#34 := (= #33 f1)
-#37 := (and #34 #36)
-#32 := (= #31 f1)
-#38 := (iff #32 #37)
-#39 := (forall (vars (?v0 S4) (?v1 S4) (?v2 S3)) #38)
-#123 := (iff #39 #122)
-#120 := (iff #38 #119)
-#117 := (iff #37 #116)
-#114 := (iff #36 #113)
-#115 := [rewrite]: #114
-#111 := (iff #34 #110)
-#112 := [rewrite]: #111
-#118 := [monotonicity #112 #115]: #117
-#108 := (iff #32 #106)
-#109 := [rewrite]: #108
-#121 := [monotonicity #109 #118]: #120
-#124 := [quant-intro #121]: #123
-#105 := [asserted]: #39
-#127 := [mp #105 #124]: #122
-#170 := [mp~ #127 #154]: #122
-#179 := [mp #170 #178]: #176
-#682 := [mp #179 #681]: #677
-#643 := (not #677)
-#315 := (or #643 #649)
-#316 := [quant-inst #40 #13 #41]: #315
-#635 := [unit-resolution #316 #682]: #649
-#644 := (not #649)
-#302 := (or #644 #126 #310)
-#307 := [def-axiom]: #302
-#631 := [unit-resolution #307 #635]: #636
-#637 := [unit-resolution #631 #633]: #310
-#648 := (or #647 #326 #331)
-#654 := [def-axiom]: #648
-#273 := [unit-resolution #654 #637 #634 #632]: false
-#638 := [lemma #273]: #126
-#329 := (or #326 #139)
-#317 := (or #326 #139 #237)
-#328 := [def-axiom]: #317
-#257 := [unit-resolution #328 #147]: #329
-#640 := [unit-resolution #257 #638]: #326
-#278 := (or #139 #647)
-#645 := (or #644 #139 #647)
-#303 := [def-axiom]: #645
-#279 := [unit-resolution #303 #635]: #278
-#641 := [unit-resolution #279 #638]: #647
-#650 := (or #310 #130)
-#651 := [def-axiom]: #650
-[unit-resolution #651 #641 #640]: false
-unsat
-600bc627f2a337ab9492b3414ff9a405597dcbc3 164 0
-#2 := false
-decl f7 :: (-> S4 S4 S5 S1)
-decl f11 :: S5
-#41 := f11
-decl f9 :: S4
-#39 := f9
-decl f10 :: S4
-#40 := f10
-#44 := (f7 f10 f9 f11)
-decl f1 :: S1
-#4 := f1
-#130 := (= f1 #44)
-#326 := (not #130)
-#42 := (f7 f9 f10 f11)
-#126 := (= f1 #42)
-#139 := (not #126)
-#628 := [hypothesis]: #139
-#325 := (or #130 #126)
-#140 := (iff #130 #139)
-#45 := (= #44 f1)
-#43 := (= #42 f1)
-#46 := (iff #43 #45)
-#47 := (not #46)
-#143 := (iff #47 #140)
-#133 := (iff #126 #130)
-#136 := (not #133)
-#141 := (iff #136 #140)
-#142 := [rewrite]: #141
-#137 := (iff #47 #136)
-#134 := (iff #46 #133)
-#131 := (iff #45 #130)
-#132 := [rewrite]: #131
-#128 := (iff #43 #126)
-#129 := [rewrite]: #128
-#135 := [monotonicity #129 #132]: #134
-#138 := [monotonicity #135]: #137
-#144 := [trans #138 #142]: #143
-#125 := [asserted]: #47
-#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
-decl f8 :: (-> S4 S5 S1)
-#310 := (f8 f10 f11)
-#647 := (= f1 #310)
-#649 := (not #647)
-#330 := (f8 f9 f11)
-#327 := (= f1 #330)
-#331 := (not #327)
-#315 := (or #331 #649)
-#626 := (or #126 #315)
-#651 := (not #315)
-#642 := (iff #126 #651)
-#29 := (:var 0 S5)
-#28 := (:var 1 S4)
-#27 := (:var 2 S4)
-#30 := (f7 #27 #28 #29)
-#676 := (pattern #30)
-#34 := (f8 #28 #29)
-#113 := (= f1 #34)
-#172 := (not #113)
-#32 := (f8 #27 #29)
-#110 := (= f1 #32)
-#171 := (not #110)
-#155 := (or #171 #172)
-#156 := (not #155)
-#106 := (= f1 #30)
-#173 := (iff #106 #156)
-#677 := (forall (vars (?v0 S4) (?v1 S4) (?v2 S5)) (:pat #676) #173)
-#176 := (forall (vars (?v0 S4) (?v1 S4) (?v2 S5)) #173)
-#680 := (iff #176 #677)
-#678 := (iff #173 #173)
-#679 := [refl]: #678
-#681 := [quant-intro #679]: #680
-#116 := (and #110 #113)
-#119 := (iff #106 #116)
-#122 := (forall (vars (?v0 S4) (?v1 S4) (?v2 S5)) #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
-#35 := (= #34 f1)
-#33 := (= #32 f1)
-#36 := (and #33 #35)
-#31 := (= #30 f1)
-#37 := (iff #31 #36)
-#38 := (forall (vars (?v0 S4) (?v1 S4) (?v2 S5)) #37)
-#123 := (iff #38 #122)
-#120 := (iff #37 #119)
-#117 := (iff #36 #116)
-#114 := (iff #35 #113)
-#115 := [rewrite]: #114
-#111 := (iff #33 #110)
-#112 := [rewrite]: #111
-#118 := [monotonicity #112 #115]: #117
-#108 := (iff #31 #106)
-#109 := [rewrite]: #108
-#121 := [monotonicity #109 #118]: #120
-#124 := [quant-intro #121]: #123
-#105 := [asserted]: #38
-#127 := [mp #105 #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 #39 #40 #41]: #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 #40 #39 #41]: #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
-b05e302d276675d4c2c21abbf217592e2a23efc3 142 0
-#2 := false
-decl f7 :: (-> S4 S4 S5 S1)
-decl f10 :: S5
-#40 := f10
-decl f9 :: S4
-#39 := f9
-#41 := (f7 f9 f9 f10)
-decl f1 :: S1
-#4 := f1
-#125 := (= f1 #41)
-#138 := (not #125)
-#634 := [hypothesis]: #138
-decl f8 :: (-> S4 S5 S1)
-#43 := (f8 f9 f10)
-#129 := (= f1 #43)
-#324 := (or #129 #125)
-#139 := (iff #129 #138)
-#44 := (= #43 f1)
-#42 := (= #41 f1)
-#45 := (iff #42 #44)
-#46 := (not #45)
-#142 := (iff #46 #139)
-#132 := (iff #125 #129)
-#135 := (not #132)
-#140 := (iff #135 #139)
-#141 := [rewrite]: #140
-#136 := (iff #46 #135)
-#133 := (iff #45 #132)
-#130 := (iff #44 #129)
-#131 := [rewrite]: #130
-#127 := (iff #42 #125)
-#128 := [rewrite]: #127
-#134 := [monotonicity #128 #131]: #133
-#137 := [monotonicity #134]: #136
-#143 := [trans #137 #141]: #142
-#124 := [asserted]: #46
-#146 := [mp #124 #143]: #139
-#236 := (not #139)
-#323 := (or #129 #125 #236)
-#237 := [def-axiom]: #323
-#238 := [unit-resolution #237 #146]: #324
-#635 := [unit-resolution #238 #634]: #129
-#325 := (not #129)
-#636 := (or #125 #325)
-#29 := (:var 0 S5)
-#28 := (:var 1 S4)
-#27 := (:var 2 S4)
-#30 := (f7 #27 #28 #29)
-#675 := (pattern #30)
-#34 := (f8 #28 #29)
-#112 := (= f1 #34)
-#171 := (not #112)
-#32 := (f8 #27 #29)
-#109 := (= f1 #32)
-#170 := (not #109)
-#154 := (or #170 #171)
-#155 := (not #154)
-#105 := (= f1 #30)
-#172 := (iff #105 #155)
-#676 := (forall (vars (?v0 S4) (?v1 S4) (?v2 S5)) (:pat #675) #172)
-#175 := (forall (vars (?v0 S4) (?v1 S4) (?v2 S5)) #172)
-#679 := (iff #175 #676)
-#677 := (iff #172 #172)
-#678 := [refl]: #677
-#680 := [quant-intro #678]: #679
-#115 := (and #109 #112)
-#118 := (iff #105 #115)
-#121 := (forall (vars (?v0 S4) (?v1 S4) (?v2 S5)) #118)
-#176 := (iff #121 #175)
-#173 := (iff #118 #172)
-#156 := (iff #115 #155)
-#157 := [rewrite]: #156
-#174 := [monotonicity #157]: #173
-#177 := [quant-intro #174]: #176
-#152 := (~ #121 #121)
-#167 := (~ #118 #118)
-#168 := [refl]: #167
-#153 := [nnf-pos #168]: #152
-#35 := (= #34 f1)
-#33 := (= #32 f1)
-#36 := (and #33 #35)
-#31 := (= #30 f1)
-#37 := (iff #31 #36)
-#38 := (forall (vars (?v0 S4) (?v1 S4) (?v2 S5)) #37)
-#122 := (iff #38 #121)
-#119 := (iff #37 #118)
-#116 := (iff #36 #115)
-#113 := (iff #35 #112)
-#114 := [rewrite]: #113
-#110 := (iff #33 #109)
-#111 := [rewrite]: #110
-#117 := [monotonicity #111 #114]: #116
-#107 := (iff #31 #105)
-#108 := [rewrite]: #107
-#120 := [monotonicity #108 #117]: #119
-#123 := [quant-intro #120]: #122
-#104 := [asserted]: #38
-#126 := [mp #104 #123]: #121
-#169 := [mp~ #126 #153]: #121
-#178 := [mp #169 #177]: #175
-#681 := [mp #178 #680]: #676
-#652 := (not #676)
-#647 := (or #652 #132)
-#329 := (or #325 #325)
-#326 := (not #329)
-#330 := (iff #125 #326)
-#653 := (or #652 #330)
-#301 := (iff #653 #647)
-#644 := (iff #647 #647)
-#302 := [rewrite]: #644
-#650 := (iff #330 #132)
-#315 := (iff #326 #129)
-#648 := (not #325)
-#642 := (iff #648 #129)
-#314 := [rewrite]: #642
-#303 := (iff #326 #648)
-#309 := (iff #329 #325)
-#646 := [rewrite]: #309
-#435 := [monotonicity #646]: #303
-#649 := [trans #435 #314]: #315
-#651 := [monotonicity #649]: #650
-#306 := [monotonicity #651]: #301
-#645 := [trans #306 #302]: #301
-#643 := [quant-inst #39 #39 #40]: #653
-#286 := [mp #643 #645]: #647
-#630 := [unit-resolution #286 #681]: #132
-#629 := (or #135 #125 #325)
-#290 := [def-axiom]: #629
-#272 := [unit-resolution #290 #630]: #636
-#637 := [unit-resolution #272 #635 #634]: false
-#639 := [lemma #637]: #125
-#328 := (or #325 #138)
-#316 := (or #325 #138 #236)
-#327 := [def-axiom]: #316
-#256 := [unit-resolution #327 #146]: #328
-#277 := [unit-resolution #256 #639]: #325
-#278 := (or #138 #129)
-#291 := (or #135 #138 #129)
-#292 := [def-axiom]: #291
-#640 := [unit-resolution #292 #630]: #278
-[unit-resolution #640 #277 #639]: false
-unsat
-d8e9744832a91810c03cbef21eb26edf5cd1eec0 280 0
-#2 := false
-decl f7 :: (-> S4 S5 S1)
-decl f12 :: S5
-#45 := f12
-decl f8 :: (-> S4 S4 S4)
-decl f10 :: S4
-#41 := f10
-decl f9 :: S4
-#40 := f9
-#48 := (f8 f9 f10)
-#316 := (f7 #48 f12)
-decl f1 :: S1
-#4 := f1
-#653 := (= f1 #316)
-#251 := (f7 f10 f12)
-#630 := (= f1 #251)
-#627 := (not #630)
-#341 := (f7 f9 f12)
-#357 := (= f1 #341)
-#358 := (not #357)
-#616 := (or #358 #627)
-#617 := (not #616)
-#613 := (iff #617 #653)
-#584 := (not #613)
-decl f11 :: S4
-#42 := f11
-#336 := (f7 f11 f12)
-#333 := (= f1 #336)
-#337 := (not #333)
-#486 := (or #337 #627)
-#495 := (not #486)
-#43 := (f8 f10 f11)
-#648 := (f7 #43 f12)
-#634 := (= f1 #648)
-#496 := (iff #495 #634)
-#589 := (not #496)
-#569 := [hypothesis]: #589
-#30 := (:var 0 S5)
-#28 := (:var 1 S4)
-#27 := (:var 2 S4)
-#29 := (f8 #27 #28)
-#31 := (f7 #29 #30)
-#682 := (pattern #31)
-#35 := (f7 #28 #30)
-#119 := (= f1 #35)
-#178 := (not #119)
-#33 := (f7 #27 #30)
-#116 := (= f1 #33)
-#177 := (not #116)
-#161 := (or #177 #178)
-#162 := (not #161)
-#112 := (= f1 #31)
-#179 := (iff #112 #162)
-#683 := (forall (vars (?v0 S4) (?v1 S4) (?v2 S5)) (:pat #682) #179)
-#182 := (forall (vars (?v0 S4) (?v1 S4) (?v2 S5)) #179)
-#686 := (iff #182 #683)
-#684 := (iff #179 #179)
-#685 := [refl]: #684
-#687 := [quant-intro #685]: #686
-#122 := (and #116 #119)
-#125 := (iff #112 #122)
-#128 := (forall (vars (?v0 S4) (?v1 S4) (?v2 S5)) #125)
-#183 := (iff #128 #182)
-#180 := (iff #125 #179)
-#163 := (iff #122 #162)
-#164 := [rewrite]: #163
-#181 := [monotonicity #164]: #180
-#184 := [quant-intro #181]: #183
-#159 := (~ #128 #128)
-#174 := (~ #125 #125)
-#175 := [refl]: #174
-#160 := [nnf-pos #175]: #159
-#36 := (= #35 f1)
-#34 := (= #33 f1)
-#37 := (and #34 #36)
-#32 := (= #31 f1)
-#38 := (iff #32 #37)
-#39 := (forall (vars (?v0 S4) (?v1 S4) (?v2 S5)) #38)
-#129 := (iff #39 #128)
-#126 := (iff #38 #125)
-#123 := (iff #37 #122)
-#120 := (iff #36 #119)
-#121 := [rewrite]: #120
-#117 := (iff #34 #116)
-#118 := [rewrite]: #117
-#124 := [monotonicity #118 #121]: #123
-#114 := (iff #32 #112)
-#115 := [rewrite]: #114
-#127 := [monotonicity #115 #124]: #126
-#130 := [quant-intro #127]: #129
-#111 := [asserted]: #39
-#133 := [mp #111 #130]: #128
-#176 := [mp~ #133 #160]: #128
-#185 := [mp #176 #184]: #182
-#688 := [mp #185 #687]: #683
-#308 := (not #683)
-#500 := (or #308 #496)
-#602 := (or #627 #337)
-#484 := (not #602)
-#485 := (iff #634 #484)
-#501 := (or #308 #485)
-#595 := (iff #501 #500)
-#596 := (iff #500 #500)
-#583 := [rewrite]: #596
-#498 := (iff #485 #496)
-#594 := (iff #634 #495)
-#497 := (iff #594 #496)
-#490 := [rewrite]: #497
-#479 := (iff #485 #594)
-#590 := (iff #484 #495)
-#445 := (iff #602 #486)
-#593 := [rewrite]: #445
-#591 := [monotonicity #593]: #590
-#494 := [monotonicity #591]: #479
-#499 := [trans #494 #490]: #498
-#592 := [monotonicity #499]: #595
-#585 := [trans #592 #583]: #595
-#502 := [quant-inst #41 #42 #45]: #501
-#577 := [mp #502 #585]: #500
-#570 := [unit-resolution #577 #688 #569]: false
-#571 := [lemma #570]: #496
-#635 := (not #634)
-#359 := (or #358 #635)
-#345 := (not #359)
-#44 := (f8 f9 #43)
-#46 := (f7 #44 f12)
-#132 := (= f1 #46)
-#145 := (not #132)
-#572 := [hypothesis]: #145
-#573 := (or #132 #359)
-#360 := (iff #132 #345)
-#631 := (or #308 #360)
-#353 := [quant-inst #40 #43 #45]: #631
-#568 := [unit-resolution #353 #688]: #360
-#343 := (not #360)
-#344 := (or #343 #132 #359)
-#346 := [def-axiom]: #344
-#559 := [unit-resolution #346 #568]: #573
-#560 := [unit-resolution #559 #572]: #359
-#599 := (or #308 #613)
-#618 := (iff #653 #617)
-#615 := (or #308 #618)
-#620 := (iff #615 #599)
-#463 := (iff #599 #599)
-#464 := [rewrite]: #463
-#614 := (iff #618 #613)
-#619 := [rewrite]: #614
-#462 := [monotonicity #619]: #620
-#606 := [trans #462 #464]: #620
-#621 := [quant-inst #40 #41 #45]: #615
-#607 := [mp #621 #606]: #599
-#562 := [unit-resolution #607 #688]: #613
-#548 := (or #584 #617)
-#655 := (not #653)
-#321 := (or #337 #655)
-#657 := (not #321)
-#49 := (f8 #48 f11)
-#50 := (f7 #49 f12)
-#136 := (= f1 #50)
-#331 := (or #136 #132)
-#146 := (iff #136 #145)
-#51 := (= #50 f1)
-#47 := (= #46 f1)
-#52 := (iff #47 #51)
-#53 := (not #52)
-#149 := (iff #53 #146)
-#139 := (iff #132 #136)
-#142 := (not #139)
-#147 := (iff #142 #146)
-#148 := [rewrite]: #147
-#143 := (iff #53 #142)
-#140 := (iff #52 #139)
-#137 := (iff #51 #136)
-#138 := [rewrite]: #137
-#134 := (iff #47 #132)
-#135 := [rewrite]: #134
-#141 := [monotonicity #135 #138]: #140
-#144 := [monotonicity #141]: #143
-#150 := [trans #144 #148]: #149
-#131 := [asserted]: #53
-#153 := [mp #131 #150]: #146
-#243 := (not #146)
-#330 := (or #136 #132 #243)
-#244 := [def-axiom]: #330
-#245 := [unit-resolution #244 #153]: #331
-#563 := [unit-resolution #245 #572]: #136
-#332 := (not #136)
-#561 := (or #332 #657)
-#654 := (iff #136 #657)
-#313 := (or #308 #654)
-#310 := (or #655 #337)
-#442 := (not #310)
-#649 := (iff #136 #442)
-#651 := (or #308 #649)
-#652 := (iff #651 #313)
-#636 := (iff #313 #313)
-#297 := [rewrite]: #636
-#660 := (iff #649 #654)
-#658 := (iff #442 #657)
-#322 := (iff #310 #321)
-#656 := [rewrite]: #322
-#659 := [monotonicity #656]: #658
-#650 := [monotonicity #659]: #660
-#293 := [monotonicity #650]: #652
-#298 := [trans #293 #297]: #652
-#309 := [quant-inst #48 #42 #45]: #651
-#299 := [mp #309 #298]: #313
-#564 := [unit-resolution #299 #688]: #654
-#637 := (not #654)
-#644 := (or #637 #332 #657)
-#646 := [def-axiom]: #644
-#565 := [unit-resolution #646 #564]: #561
-#545 := [unit-resolution #565 #563]: #657
-#639 := (or #321 #653)
-#640 := [def-axiom]: #639
-#546 := [unit-resolution #640 #545]: #653
-#578 := (or #584 #617 #655)
-#579 := [def-axiom]: #578
-#549 := [unit-resolution #579 #546]: #548
-#550 := [unit-resolution #549 #562]: #617
-#608 := (or #616 #357)
-#574 := [def-axiom]: #608
-#551 := [unit-resolution #574 #550]: #357
-#633 := (or #345 #358 #635)
-#342 := [def-axiom]: #633
-#552 := [unit-resolution #342 #551 #560]: #635
-#300 := (or #321 #333)
-#638 := [def-axiom]: #300
-#553 := [unit-resolution #638 #545]: #333
-#576 := (or #616 #630)
-#586 := [def-axiom]: #576
-#554 := [unit-resolution #586 #550]: #630
-#611 := (or #495 #337 #627)
-#605 := [def-axiom]: #611
-#555 := [unit-resolution #605 #554 #553]: #495
-#443 := (or #589 #486 #634)
-#444 := [def-axiom]: #443
-#556 := [unit-resolution #444 #555 #552 #571]: false
-#557 := [lemma #556]: #132
-#547 := (or #145 #345)
-#624 := (or #343 #145 #345)
-#625 := [def-axiom]: #624
-#558 := [unit-resolution #625 #568]: #547
-#536 := [unit-resolution #558 #557]: #345
-#632 := (or #359 #634)
-#629 := [def-axiom]: #632
-#537 := [unit-resolution #629 #536]: #634
-#612 := (or #589 #495 #635)
-#441 := [def-axiom]: #612
-#539 := [unit-resolution #441 #537 #571]: #495
-#604 := (or #486 #630)
-#610 := [def-axiom]: #604
-#540 := [unit-resolution #610 #539]: #630
-#354 := (or #359 #357)
-#628 := [def-axiom]: #354
-#541 := [unit-resolution #628 #536]: #357
-#587 := (or #617 #358 #627)
-#588 := [def-axiom]: #587
-#542 := [unit-resolution #588 #541 #540]: #617
-#335 := (or #332 #145)
-#323 := (or #332 #145 #243)
-#334 := [def-axiom]: #323
-#263 := [unit-resolution #334 #153]: #335
-#543 := [unit-resolution #263 #557]: #332
-#538 := (or #136 #321)
-#643 := (or #637 #136 #321)
-#279 := [def-axiom]: #643
-#544 := [unit-resolution #279 #564]: #538
-#530 := [unit-resolution #544 #543]: #321
-#609 := (or #486 #333)
-#603 := [def-axiom]: #609
-#526 := [unit-resolution #603 #539]: #333
-#641 := (or #657 #337 #655)
-#642 := [def-axiom]: #641
-#527 := [unit-resolution #642 #526 #530]: #655
-#580 := (or #584 #616 #653)
-#581 := [def-axiom]: #580
-#528 := [unit-resolution #581 #527 #542]: #584
-[unit-resolution #607 #688 #528]: false
-unsat
-cdbf11c9465d749cfd2e9563f8fc0294f62a631c 18 0
-#2 := false
-decl f8 :: S4
-#32 := f8
-#33 := (= f8 f8)
-#34 := (not #33)
-#115 := (iff #34 false)
-#1 := true
-#110 := (not true)
-#113 := (iff #110 false)
-#114 := [rewrite]: #113
-#111 := (iff #34 #110)
-#107 := (iff #33 true)
-#109 := [rewrite]: #107
-#112 := [monotonicity #109]: #111
-#116 := [trans #112 #114]: #115
-#106 := [asserted]: #34
-[mp #106 #116]: false
-unsat
 bd811011020855800543e0a16a4dcb354fda48ef 31 0
 #2 := false
 decl f1 :: S1

author	boehmes
	Wed, 08 Jun 2011 13:43:15 +0200
changeset 43273	4de998188c1d
parent 43272	878c0935a4a4
child 43274	ad4611809a29

src/HOL/Multivariate_Analysis/Integration.certs		file \| annotate \| diff \| comparison \| revisions
src/HOL/SMT_Examples/SMT_Examples.certs		file \| annotate \| diff \| comparison \| revisions
src/HOL/SMT_Examples/SMT_Tests.certs		file \| annotate \| diff \| comparison \| revisions