# HG changeset patch # User blanchet # Date 1392190648 -3600 # Node ID 0aaca907aeab4aae1aeeaf898bf853866872ebfb # Parent 4d2123c583fa7bcbf9c7fdadd7fc444419ef7aa4 updated certificates diff -r 4d2123c583fa -r 0aaca907aeab src/HOL/SMT_Examples/SMT_Examples.certs --- 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