--- a/src/HOL/SMT_Examples/SMT_Examples.certs Wed Feb 12 08:37:28 2014 +0100
+++ b/src/HOL/SMT_Examples/SMT_Examples.certs Wed Feb 12 08:37:28 2014 +0100
@@ -101,40 +101,6 @@
#45 := [and-elim #44]: #11
[mp #45 #65]: false
unsat
-050883983ebe99dc3b7f24a011b1724b1b2c4dd9 33 0
-#2 := false
-decl f1 :: S1
-#3 := f1
-decl f6 :: S1
-#14 := f6
-#15 := (= f6 f1)
-decl f5 :: S1
-#12 := f5
-#13 := (= f5 f1)
-#16 := (and #13 #15)
-decl f4 :: S1
-#9 := f4
-#10 := (= f4 f1)
-decl f3 :: S1
-#7 := f3
-#8 := (= f3 f1)
-#11 := (and #8 #10)
-#17 := (or #11 #16)
-#18 := (implies #17 #17)
-#19 := (not #18)
-#48 := (iff #19 false)
-#1 := true
-#43 := (not true)
-#46 := (iff #43 false)
-#47 := [rewrite]: #46
-#44 := (iff #19 #43)
-#41 := (iff #18 true)
-#42 := [rewrite]: #41
-#45 := [monotonicity #42]: #44
-#49 := [trans #45 #47]: #48
-#40 := [asserted]: #19
-[mp #40 #49]: false
-unsat
79d9d246dd9d27e03e8f1ea895e790f3a4420bfd 55 0
#2 := false
decl f1 :: S1
@@ -191,6 +157,40 @@
#42 := [asserted]: #21
[mp #42 #72]: false
unsat
+050883983ebe99dc3b7f24a011b1724b1b2c4dd9 33 0
+#2 := false
+decl f1 :: S1
+#3 := f1
+decl f6 :: S1
+#14 := f6
+#15 := (= f6 f1)
+decl f5 :: S1
+#12 := f5
+#13 := (= f5 f1)
+#16 := (and #13 #15)
+decl f4 :: S1
+#9 := f4
+#10 := (= f4 f1)
+decl f3 :: S1
+#7 := f3
+#8 := (= f3 f1)
+#11 := (and #8 #10)
+#17 := (or #11 #16)
+#18 := (implies #17 #17)
+#19 := (not #18)
+#48 := (iff #19 false)
+#1 := true
+#43 := (not true)
+#46 := (iff #43 false)
+#47 := [rewrite]: #46
+#44 := (iff #19 #43)
+#41 := (iff #18 true)
+#42 := [rewrite]: #41
+#45 := [monotonicity #42]: #44
+#49 := [trans #45 #47]: #48
+#40 := [asserted]: #19
+[mp #40 #49]: false
+unsat
8575241c64c02491d277f6598ca57e576f5a6b45 60 0
#2 := false
decl f1 :: S1
@@ -546,6 +546,124 @@
#83 := [and-elim #82]: #57
[unit-resolution #83 #90]: false
unsat
+a69a9e8c5e31ec6b9da4cf96f47b52cf6b9404d9 117 0
+#2 := false
+decl f3 :: (-> S3 S2 S1)
+#10 := (:var 0 S2)
+decl f4 :: (-> S4 S1 S3)
+decl f6 :: S1
+#16 := f6
+decl f5 :: S4
+#7 := f5
+#17 := (f4 f5 f6)
+#18 := (f3 #17 #10)
+#573 := (pattern #18)
+decl f1 :: S1
+#3 := f1
+#19 := (= #18 f1)
+#76 := (not #19)
+#574 := (forall (vars (?v0 S2)) (:pat #573) #76)
+decl f7 :: S2
+#21 := f7
+#22 := (f3 #17 f7)
+#23 := (= #22 f1)
+#150 := (= f6 f1)
+#151 := (iff #23 #150)
+#8 := (:var 1 S1)
+#9 := (f4 f5 #8)
+#11 := (f3 #9 #10)
+#566 := (pattern #11)
+#13 := (= #8 f1)
+#12 := (= #11 f1)
+#14 := (iff #12 #13)
+#567 := (forall (vars (?v0 S1) (?v1 S2)) (:pat #566) #14)
+#15 := (forall (vars (?v0 S1) (?v1 S2)) #14)
+#570 := (iff #15 #567)
+#568 := (iff #14 #14)
+#569 := [refl]: #568
+#571 := [quant-intro #569]: #570
+#62 := (~ #15 #15)
+#60 := (~ #14 #14)
+#61 := [refl]: #60
+#63 := [nnf-pos #61]: #62
+#46 := [asserted]: #15
+#53 := [mp~ #46 #63]: #15
+#572 := [mp #53 #571]: #567
+#152 := (not #567)
+#228 := (or #152 #151)
+#561 := [quant-inst #16 #21]: #228
+#237 := [unit-resolution #561 #572]: #151
+decl ?v0!0 :: S2
+#66 := ?v0!0
+#67 := (f3 #17 ?v0!0)
+#68 := (= #67 f1)
+#236 := (iff #68 #150)
+#238 := (or #152 #236)
+#229 := [quant-inst #16 #66]: #238
+#227 := [unit-resolution #229 #572]: #236
+#240 := (not #236)
+#199 := (or #240 #150)
+#55 := (not #23)
+#215 := [hypothesis]: #55
+#83 := (or #68 #23)
+#79 := (forall (vars (?v0 S2)) #76)
+#82 := (or #79 #55)
+#84 := (and #83 #82)
+#20 := (exists (vars (?v0 S2)) #19)
+#48 := (not #20)
+#49 := (iff #48 #23)
+#85 := (~ #49 #84)
+#57 := (~ #23 #23)
+#65 := [refl]: #57
+#64 := (~ #55 #55)
+#56 := [refl]: #64
+#80 := (~ #48 #79)
+#77 := (~ #76 #76)
+#78 := [refl]: #77
+#81 := [nnf-neg #78]: #80
+#73 := (not #48)
+#74 := (~ #73 #68)
+#69 := (~ #20 #68)
+#70 := [sk]: #69
+#75 := [nnf-neg #70]: #74
+#86 := [nnf-pos #75 #81 #56 #65]: #85
+#24 := (iff #20 #23)
+#25 := (not #24)
+#50 := (iff #25 #49)
+#51 := [rewrite]: #50
+#47 := [asserted]: #25
+#54 := [mp #47 #51]: #49
+#87 := [mp~ #54 #86]: #84
+#90 := [and-elim #87]: #83
+#557 := [unit-resolution #90 #215]: #68
+#243 := (not #68)
+#222 := (or #240 #243 #150)
+#558 := [def-axiom]: #222
+#541 := [unit-resolution #558 #557]: #199
+#203 := [unit-resolution #541 #227]: #150
+#241 := (not #150)
+#562 := (not #151)
+#204 := (or #562 #241)
+#563 := (or #562 #23 #241)
+#564 := [def-axiom]: #563
+#205 := [unit-resolution #564 #215]: #204
+#206 := [unit-resolution #205 #203 #237]: false
+#543 := [lemma #206]: #23
+#579 := (or #574 #55)
+#580 := (iff #82 #579)
+#577 := (iff #79 #574)
+#575 := (iff #76 #76)
+#576 := [refl]: #575
+#578 := [quant-intro #576]: #577
+#581 := [monotonicity #578]: #580
+#91 := [and-elim #87]: #82
+#582 := [mp #91 #581]: #579
+#242 := [unit-resolution #582 #543]: #574
+#555 := (not #574)
+#214 := (or #555 #55)
+#219 := [quant-inst #21]: #214
+[unit-resolution #219 #543 #242]: false
+unsat
d97439af6f5bc7794ab403d0f6cc318d103016a1 1288 0
#2 := false
decl f1 :: S1
@@ -1835,124 +1953,6 @@
#1532 := [unit-resolution #769 #1531]: #20
[unit-resolution #606 #1532 #1528]: false
unsat
-a69a9e8c5e31ec6b9da4cf96f47b52cf6b9404d9 117 0
-#2 := false
-decl f3 :: (-> S3 S2 S1)
-#10 := (:var 0 S2)
-decl f4 :: (-> S4 S1 S3)
-decl f6 :: S1
-#16 := f6
-decl f5 :: S4
-#7 := f5
-#17 := (f4 f5 f6)
-#18 := (f3 #17 #10)
-#573 := (pattern #18)
-decl f1 :: S1
-#3 := f1
-#19 := (= #18 f1)
-#76 := (not #19)
-#574 := (forall (vars (?v0 S2)) (:pat #573) #76)
-decl f7 :: S2
-#21 := f7
-#22 := (f3 #17 f7)
-#23 := (= #22 f1)
-#150 := (= f6 f1)
-#151 := (iff #23 #150)
-#8 := (:var 1 S1)
-#9 := (f4 f5 #8)
-#11 := (f3 #9 #10)
-#566 := (pattern #11)
-#13 := (= #8 f1)
-#12 := (= #11 f1)
-#14 := (iff #12 #13)
-#567 := (forall (vars (?v0 S1) (?v1 S2)) (:pat #566) #14)
-#15 := (forall (vars (?v0 S1) (?v1 S2)) #14)
-#570 := (iff #15 #567)
-#568 := (iff #14 #14)
-#569 := [refl]: #568
-#571 := [quant-intro #569]: #570
-#62 := (~ #15 #15)
-#60 := (~ #14 #14)
-#61 := [refl]: #60
-#63 := [nnf-pos #61]: #62
-#46 := [asserted]: #15
-#53 := [mp~ #46 #63]: #15
-#572 := [mp #53 #571]: #567
-#152 := (not #567)
-#228 := (or #152 #151)
-#561 := [quant-inst #16 #21]: #228
-#237 := [unit-resolution #561 #572]: #151
-decl ?v0!0 :: S2
-#66 := ?v0!0
-#67 := (f3 #17 ?v0!0)
-#68 := (= #67 f1)
-#236 := (iff #68 #150)
-#238 := (or #152 #236)
-#229 := [quant-inst #16 #66]: #238
-#227 := [unit-resolution #229 #572]: #236
-#240 := (not #236)
-#199 := (or #240 #150)
-#55 := (not #23)
-#215 := [hypothesis]: #55
-#83 := (or #68 #23)
-#79 := (forall (vars (?v0 S2)) #76)
-#82 := (or #79 #55)
-#84 := (and #83 #82)
-#20 := (exists (vars (?v0 S2)) #19)
-#48 := (not #20)
-#49 := (iff #48 #23)
-#85 := (~ #49 #84)
-#57 := (~ #23 #23)
-#65 := [refl]: #57
-#64 := (~ #55 #55)
-#56 := [refl]: #64
-#80 := (~ #48 #79)
-#77 := (~ #76 #76)
-#78 := [refl]: #77
-#81 := [nnf-neg #78]: #80
-#73 := (not #48)
-#74 := (~ #73 #68)
-#69 := (~ #20 #68)
-#70 := [sk]: #69
-#75 := [nnf-neg #70]: #74
-#86 := [nnf-pos #75 #81 #56 #65]: #85
-#24 := (iff #20 #23)
-#25 := (not #24)
-#50 := (iff #25 #49)
-#51 := [rewrite]: #50
-#47 := [asserted]: #25
-#54 := [mp #47 #51]: #49
-#87 := [mp~ #54 #86]: #84
-#90 := [and-elim #87]: #83
-#557 := [unit-resolution #90 #215]: #68
-#243 := (not #68)
-#222 := (or #240 #243 #150)
-#558 := [def-axiom]: #222
-#541 := [unit-resolution #558 #557]: #199
-#203 := [unit-resolution #541 #227]: #150
-#241 := (not #150)
-#562 := (not #151)
-#204 := (or #562 #241)
-#563 := (or #562 #23 #241)
-#564 := [def-axiom]: #563
-#205 := [unit-resolution #564 #215]: #204
-#206 := [unit-resolution #205 #203 #237]: false
-#543 := [lemma #206]: #23
-#579 := (or #574 #55)
-#580 := (iff #82 #579)
-#577 := (iff #79 #574)
-#575 := (iff #76 #76)
-#576 := [refl]: #575
-#578 := [quant-intro #576]: #577
-#581 := [monotonicity #578]: #580
-#91 := [and-elim #87]: #82
-#582 := [mp #91 #581]: #579
-#242 := [unit-resolution #582 #543]: #574
-#555 := (not #574)
-#214 := (or #555 #55)
-#219 := [quant-inst #21]: #214
-[unit-resolution #219 #543 #242]: false
-unsat
fdf61e060f49731790f4d6c8f9b26c21349c60b3 117 0
#2 := false
decl f1 :: S1
@@ -2071,24 +2071,6 @@
#603 := [unit-resolution #271 #618]: #602
[unit-resolution #603 #601 #297]: false
unsat
-0ce3a745d60cdbf0fe26b07c5e76de09d459dd25 17 0
-#2 := false
-#7 := 3::Int
-#8 := (= 3::Int 3::Int)
-#9 := (not #8)
-#38 := (iff #9 false)
-#1 := true
-#33 := (not true)
-#36 := (iff #33 false)
-#37 := [rewrite]: #36
-#34 := (iff #9 #33)
-#31 := (iff #8 true)
-#32 := [rewrite]: #31
-#35 := [monotonicity #32]: #34
-#39 := [trans #35 #37]: #38
-#30 := [asserted]: #9
-[mp #30 #39]: false
-unsat
5c792581e65682628e5c59ca9f3f8801e6aeba72 61 0
#2 := false
decl f1 :: S1
@@ -2151,6 +2133,24 @@
#136 := [quant-inst #7]: #221
[unit-resolution #136 #556 #52]: false
unsat
+0ce3a745d60cdbf0fe26b07c5e76de09d459dd25 17 0
+#2 := false
+#7 := 3::Int
+#8 := (= 3::Int 3::Int)
+#9 := (not #8)
+#38 := (iff #9 false)
+#1 := true
+#33 := (not true)
+#36 := (iff #33 false)
+#37 := [rewrite]: #36
+#34 := (iff #9 #33)
+#31 := (iff #8 true)
+#32 := [rewrite]: #31
+#35 := [monotonicity #32]: #34
+#39 := [trans #35 #37]: #38
+#30 := [asserted]: #9
+[mp #30 #39]: false
+unsat
1532b1dde71eb42ca0a012bb62d9bbadf37fa326 17 0
#2 := false
#7 := 3::Real
@@ -7256,9 +7256,9 @@
unsat
c4f4c8220660d1979009b33a643f0927bee816b1 1 0
unsat
-db6426d59fdd57da8ca5d11de399761d1f1443de 1 0
+e7ef76d73ccb9bc09d2b5368495a7a59d1bae3dc 1 0
unsat
-e7ef76d73ccb9bc09d2b5368495a7a59d1bae3dc 1 0
+db6426d59fdd57da8ca5d11de399761d1f1443de 1 0
unsat
a2da5fa16f268876e3dcbc1874e34212d0a36218 54 0
#2 := false
@@ -7799,6 +7799,70 @@
#63 := [mp~ #61 #70]: #56
[unit-resolution #63 #529]: false
unsat
+f6f0c702e5caae5d1fc0a3e7862c44d261de6d47 63 0
+#2 := false
+#15 := 1::Int
+#12 := (:var 1 Int)
+#10 := 6::Int
+#11 := (- 6::Int)
+#13 := (* #11 #12)
+#8 := (:var 2 Int)
+#7 := 4::Int
+#9 := (* 4::Int #8)
+#14 := (+ #9 #13)
+#16 := (= #14 1::Int)
+#17 := (exists (vars (?v0 Int) (?v1 Int) (?v2 Int)) #16)
+#18 := (not #17)
+#19 := (not #18)
+#86 := (iff #19 false)
+#56 := (:var 0 Int)
+#41 := -6::Int
+#58 := (* -6::Int #56)
+#57 := (* 4::Int #12)
+#59 := (+ #57 #58)
+#60 := (= #59 1::Int)
+#61 := (exists (vars (?v0 Int) (?v1 Int)) #60)
+#84 := (iff #61 false)
+#77 := (exists (vars (?v0 Int) (?v1 Int)) false)
+#82 := (iff #77 false)
+#83 := [elim-unused]: #82
+#80 := (iff #61 #77)
+#78 := (iff #60 false)
+#79 := [rewrite]: #78
+#81 := [quant-intro #79]: #80
+#85 := [trans #81 #83]: #84
+#74 := (iff #19 #61)
+#66 := (not #61)
+#69 := (not #66)
+#72 := (iff #69 #61)
+#73 := [rewrite]: #72
+#70 := (iff #19 #69)
+#67 := (iff #18 #66)
+#64 := (iff #17 #61)
+#44 := (* -6::Int #12)
+#47 := (+ #9 #44)
+#50 := (= #47 1::Int)
+#53 := (exists (vars (?v0 Int) (?v1 Int) (?v2 Int)) #50)
+#62 := (iff #53 #61)
+#63 := [elim-unused]: #62
+#54 := (iff #17 #53)
+#51 := (iff #16 #50)
+#48 := (= #14 #47)
+#45 := (= #13 #44)
+#42 := (= #11 -6::Int)
+#43 := [rewrite]: #42
+#46 := [monotonicity #43]: #45
+#49 := [monotonicity #46]: #48
+#52 := [monotonicity #49]: #51
+#55 := [quant-intro #52]: #54
+#65 := [trans #55 #63]: #64
+#68 := [monotonicity #65]: #67
+#71 := [monotonicity #68]: #70
+#75 := [trans #71 #73]: #74
+#87 := [trans #75 #85]: #86
+#40 := [asserted]: #19
+[mp #40 #87]: false
+unsat
252d255c564463d916bc68156eea8dbe7fb0be0a 165 0
WARNING: failed to find a pattern for quantifier (quantifier id: k!10)
#2 := false
@@ -7965,70 +8029,6 @@
#563 := [unit-resolution #136 #574]: #62
[unit-resolution #563 #570]: false
unsat
-f6f0c702e5caae5d1fc0a3e7862c44d261de6d47 63 0
-#2 := false
-#15 := 1::Int
-#12 := (:var 1 Int)
-#10 := 6::Int
-#11 := (- 6::Int)
-#13 := (* #11 #12)
-#8 := (:var 2 Int)
-#7 := 4::Int
-#9 := (* 4::Int #8)
-#14 := (+ #9 #13)
-#16 := (= #14 1::Int)
-#17 := (exists (vars (?v0 Int) (?v1 Int) (?v2 Int)) #16)
-#18 := (not #17)
-#19 := (not #18)
-#86 := (iff #19 false)
-#56 := (:var 0 Int)
-#41 := -6::Int
-#58 := (* -6::Int #56)
-#57 := (* 4::Int #12)
-#59 := (+ #57 #58)
-#60 := (= #59 1::Int)
-#61 := (exists (vars (?v0 Int) (?v1 Int)) #60)
-#84 := (iff #61 false)
-#77 := (exists (vars (?v0 Int) (?v1 Int)) false)
-#82 := (iff #77 false)
-#83 := [elim-unused]: #82
-#80 := (iff #61 #77)
-#78 := (iff #60 false)
-#79 := [rewrite]: #78
-#81 := [quant-intro #79]: #80
-#85 := [trans #81 #83]: #84
-#74 := (iff #19 #61)
-#66 := (not #61)
-#69 := (not #66)
-#72 := (iff #69 #61)
-#73 := [rewrite]: #72
-#70 := (iff #19 #69)
-#67 := (iff #18 #66)
-#64 := (iff #17 #61)
-#44 := (* -6::Int #12)
-#47 := (+ #9 #44)
-#50 := (= #47 1::Int)
-#53 := (exists (vars (?v0 Int) (?v1 Int) (?v2 Int)) #50)
-#62 := (iff #53 #61)
-#63 := [elim-unused]: #62
-#54 := (iff #17 #53)
-#51 := (iff #16 #50)
-#48 := (= #14 #47)
-#45 := (= #13 #44)
-#42 := (= #11 -6::Int)
-#43 := [rewrite]: #42
-#46 := [monotonicity #43]: #45
-#49 := [monotonicity #46]: #48
-#52 := [monotonicity #49]: #51
-#55 := [quant-intro #52]: #54
-#65 := [trans #55 #63]: #64
-#68 := [monotonicity #65]: #67
-#71 := [monotonicity #68]: #70
-#75 := [trans #71 #73]: #74
-#87 := [trans #75 #85]: #86
-#40 := [asserted]: #19
-[mp #40 #87]: false
-unsat
302156fb98e1f9b5657a3c89c418d5e1813f274a 101 0
#2 := false
#7 := 0::Int
@@ -10281,33 +10281,33 @@
#55 := [not-or-elim #54]: #53
[unit-resolution #55 #214]: false
unsat
-22f5a208d6aa87f9794b1ab4d7ebb0a58f9ec89d 106 0
+86345bce2206ce27e174d4b1d6d3e0182564f8a1 106 0
#2 := false
-decl f11 :: (-> S9 S7 S2)
-decl f16 :: S7
+decl f11 :: (-> S9 S5 S3)
+decl f16 :: S5
#34 := f16
decl f12 :: S9
#25 := f12
#39 := (f11 f12 f16)
-decl f3 :: (-> S4 S5 S2)
-decl f13 :: S5
+decl f6 :: (-> S6 S7 S3)
+decl f13 :: S7
#29 := f13
-decl f4 :: S4
-#7 := f4
-#38 := (f3 f4 f13)
+decl f7 :: S6
+#14 := f7
+#38 := (f6 f7 f13)
#40 := (= #38 #39)
-decl f8 :: (-> S3 S2 S7)
-decl f14 :: S2
+decl f5 :: (-> S2 S3 S5)
+decl f14 :: S3
#30 := f14
-decl f15 :: S3
+decl f15 :: S2
#31 := f15
-#35 := (f8 f15 f14)
-#236 := (f11 f12 #35)
-#233 := (= #236 #39)
-#573 := (= #39 #236)
+#35 := (f5 f15 f14)
+#165 := (f11 f12 #35)
+#233 := (= #165 #39)
+#573 := (= #39 #165)
#36 := (= f16 #35)
-decl f5 :: (-> S2 S3 S5)
-#32 := (f5 f14 f15)
+decl f8 :: (-> S3 S2 S7)
+#32 := (f8 f14 f15)
#33 := (= f13 #32)
#37 := (and #33 #36)
#68 := (not #37)
@@ -10325,17 +10325,17 @@
#78 := [and-elim #75]: #36
#579 := [monotonicity #78]: #573
#570 := [symm #579]: #233
-#213 := (= #38 #236)
-#569 := (= f14 #236)
-#572 := (= #236 f14)
-#16 := (:var 0 S2)
-#15 := (:var 1 S3)
-#17 := (f8 #15 #16)
-#587 := (pattern #17)
-#26 := (f11 f12 #17)
-#27 := (= #26 #16)
-#600 := (forall (vars (?v0 S3) (?v1 S2)) (:pat #587) #27)
-#28 := (forall (vars (?v0 S3) (?v1 S2)) #27)
+#213 := (= #38 #165)
+#569 := (= f14 #165)
+#251 := (= #165 f14)
+#9 := (:var 0 S3)
+#8 := (:var 1 S2)
+#10 := (f5 #8 #9)
+#580 := (pattern #10)
+#26 := (f11 f12 #10)
+#27 := (= #26 #9)
+#600 := (forall (vars (?v0 S2) (?v1 S3)) (:pat #580) #27)
+#28 := (forall (vars (?v0 S2) (?v1 S3)) #27)
#603 := (iff #28 #600)
#601 := (iff #27 #27)
#602 := [refl]: #601
@@ -10347,38 +10347,38 @@
#66 := [asserted]: #28
#109 := [mp~ #66 #89]: #28
#605 := [mp #109 #604]: #600
-#242 := (not #600)
-#575 := (or #242 #572)
-#576 := [quant-inst #31 #30]: #575
-#568 := [unit-resolution #576 #605]: #572
+#256 := (not #600)
+#253 := (or #256 #251)
+#257 := [quant-inst #31 #30]: #253
+#568 := [unit-resolution #257 #605]: #251
#228 := [symm #568]: #569
#229 := (= #38 f14)
-#164 := (f3 f4 #32)
-#250 := (= #164 f14)
-#9 := (:var 0 S3)
-#8 := (:var 1 S2)
-#10 := (f5 #8 #9)
-#580 := (pattern #10)
-#11 := (f3 f4 #10)
-#12 := (= #11 #8)
-#581 := (forall (vars (?v0 S2) (?v1 S3)) (:pat #580) #12)
-#13 := (forall (vars (?v0 S2) (?v1 S3)) #12)
-#584 := (iff #13 #581)
-#582 := (iff #12 #12)
-#583 := [refl]: #582
-#585 := [quant-intro #583]: #584
-#100 := (~ #13 #13)
-#98 := (~ #12 #12)
-#99 := [refl]: #98
-#101 := [nnf-pos #99]: #100
-#63 := [asserted]: #13
-#82 := [mp~ #63 #101]: #13
-#586 := [mp #82 #585]: #581
-#166 := (not #581)
-#252 := (or #166 #250)
-#243 := [quant-inst #30 #31]: #252
-#241 := [unit-resolution #243 #586]: #250
-#577 := (= #38 #164)
+#254 := (f6 f7 #32)
+#255 := (= #254 f14)
+#16 := (:var 0 S2)
+#15 := (:var 1 S3)
+#17 := (f8 #15 #16)
+#587 := (pattern #17)
+#18 := (f6 f7 #17)
+#19 := (= #18 #15)
+#588 := (forall (vars (?v0 S3) (?v1 S2)) (:pat #587) #19)
+#20 := (forall (vars (?v0 S3) (?v1 S2)) #19)
+#591 := (iff #20 #588)
+#589 := (iff #19 #19)
+#590 := [refl]: #589
+#592 := [quant-intro #590]: #591
+#84 := (~ #20 #20)
+#83 := (~ #19 #19)
+#102 := [refl]: #83
+#85 := [nnf-pos #102]: #84
+#64 := [asserted]: #20
+#103 := [mp~ #64 #85]: #20
+#593 := [mp #103 #592]: #588
+#574 := (not #588)
+#230 := (or #574 #255)
+#361 := [quant-inst #30 #31]: #230
+#241 := [unit-resolution #361 #593]: #255
+#577 := (= #38 #254)
#76 := [and-elim #75]: #33
#578 := [monotonicity #76]: #577
#571 := [trans #578 #241]: #229