# Theory Classical

theory Classical
imports Main
```(*  Title:      HOL/ex/Classical.thy
Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
*)

section‹Classical Predicate Calculus Problems›

theory Classical imports Main begin

text‹The machine "griffon" mentioned below is a 2.5GHz Power Mac G5.›

text‹Taken from ‹FOL/Classical.thy›. When porting examples from
first-order logic, beware of the precedence of ‹=› versus ‹↔›.›

lemma "(P --> Q | R) --> (P-->Q) | (P-->R)"
by blast

text‹If and only if›

lemma "(P=Q) = (Q = (P::bool))"
by blast

lemma "~ (P = (~P))"
by blast

text‹Sample problems from
F. J. Pelletier,
Seventy-Five Problems for Testing Automatic Theorem Provers,
J. Automated Reasoning 2 (1986), 191-216.
Errata, JAR 4 (1988), 236-236.

The hardest problems -- judging by experience with several theorem provers,
including matrix ones -- are 34 and 43.
›

subsubsection‹Pelletier's examples›

text‹1›
lemma "(P-->Q)  =  (~Q --> ~P)"
by blast

text‹2›
lemma "(~ ~ P) =  P"
by blast

text‹3›
lemma "~(P-->Q) --> (Q-->P)"
by blast

text‹4›
lemma "(~P-->Q)  =  (~Q --> P)"
by blast

text‹5›
lemma "((P|Q)-->(P|R)) --> (P|(Q-->R))"
by blast

text‹6›
lemma "P | ~ P"
by blast

text‹7›
lemma "P | ~ ~ ~ P"
by blast

text‹8.  Peirce's law›
lemma "((P-->Q) --> P)  -->  P"
by blast

text‹9›
lemma "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
by blast

text‹10›
lemma "(Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P=Q)"
by blast

text‹11.  Proved in each direction (incorrectly, says Pelletier!!)›
lemma "P=(P::bool)"
by blast

text‹12.  "Dijkstra's law"›
lemma "((P = Q) = R) = (P = (Q = R))"
by blast

text‹13.  Distributive law›
lemma "(P | (Q & R)) = ((P | Q) & (P | R))"
by blast

text‹14›
lemma "(P = Q) = ((Q | ~P) & (~Q|P))"
by blast

text‹15›
lemma "(P --> Q) = (~P | Q)"
by blast

text‹16›
lemma "(P-->Q) | (Q-->P)"
by blast

text‹17›
lemma "((P & (Q-->R))-->S)  =  ((~P | Q | S) & (~P | ~R | S))"
by blast

subsubsection‹Classical Logic: examples with quantifiers›

lemma "(∀x. P(x) & Q(x)) = ((∀x. P(x)) & (∀x. Q(x)))"
by blast

lemma "(∃x. P-->Q(x))  =  (P --> (∃x. Q(x)))"
by blast

lemma "(∃x. P(x)-->Q) = ((∀x. P(x)) --> Q)"
by blast

lemma "((∀x. P(x)) | Q)  =  (∀x. P(x) | Q)"
by blast

text‹From Wishnu Prasetya›
lemma "(∀s. q(s) --> r(s)) & ~r(s) & (∀s. ~r(s) & ~q(s) --> p(t) | q(t))
--> p(t) | r(t)"
by blast

subsubsection‹Problems requiring quantifier duplication›

text‹Theorem B of Peter Andrews, Theorem Proving via General Matings,
JACM 28 (1981).›
lemma "(∃x. ∀y. P(x) = P(y)) --> ((∃x. P(x)) = (∀y. P(y)))"
by blast

text‹Needs multiple instantiation of the quantifier.›
lemma "(∀x. P(x)-->P(f(x)))  &  P(d)-->P(f(f(f(d))))"
by blast

text‹Needs double instantiation of the quantifier›
lemma "∃x. P(x) --> P(a) & P(b)"
by blast

lemma "∃z. P(z) --> (∀x. P(x))"
by blast

lemma "∃x. (∃y. P(y)) --> P(x)"
by blast

subsubsection‹Hard examples with quantifiers›

text‹Problem 18›
lemma "∃y. ∀x. P(y)-->P(x)"
by blast

text‹Problem 19›
lemma "∃x. ∀y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))"
by blast

text‹Problem 20›
lemma "(∀x y. ∃z. ∀w. (P(x)&Q(y)-->R(z)&S(w)))
--> (∃x y. P(x) & Q(y)) --> (∃z. R(z))"
by blast

text‹Problem 21›
lemma "(∃x. P-->Q(x)) & (∃x. Q(x)-->P) --> (∃x. P=Q(x))"
by blast

text‹Problem 22›
lemma "(∀x. P = Q(x))  -->  (P = (∀x. Q(x)))"
by blast

text‹Problem 23›
lemma "(∀x. P | Q(x))  =  (P | (∀x. Q(x)))"
by blast

text‹Problem 24›
lemma "~(∃x. S(x)&Q(x)) & (∀x. P(x) --> Q(x)|R(x)) &
(~(∃x. P(x)) --> (∃x. Q(x))) & (∀x. Q(x)|R(x) --> S(x))
--> (∃x. P(x)&R(x))"
by blast

text‹Problem 25›
lemma "(∃x. P(x)) &
(∀x. L(x) --> ~ (M(x) & R(x))) &
(∀x. P(x) --> (M(x) & L(x))) &
((∀x. P(x)-->Q(x)) | (∃x. P(x)&R(x)))
--> (∃x. Q(x)&P(x))"
by blast

text‹Problem 26›
lemma "((∃x. p(x)) = (∃x. q(x))) &
(∀x. ∀y. p(x) & q(y) --> (r(x) = s(y)))
--> ((∀x. p(x)-->r(x)) = (∀x. q(x)-->s(x)))"
by blast

text‹Problem 27›
lemma "(∃x. P(x) & ~Q(x)) &
(∀x. P(x) --> R(x)) &
(∀x. M(x) & L(x) --> P(x)) &
((∃x. R(x) & ~ Q(x)) --> (∀x. L(x) --> ~ R(x)))
--> (∀x. M(x) --> ~L(x))"
by blast

text‹Problem 28.  AMENDED›
lemma "(∀x. P(x) --> (∀x. Q(x))) &
((∀x. Q(x)|R(x)) --> (∃x. Q(x)&S(x))) &
((∃x. S(x)) --> (∀x. L(x) --> M(x)))
--> (∀x. P(x) & L(x) --> M(x))"
by blast

text‹Problem 29.  Essentially the same as Principia Mathematica *11.71›
lemma "(∃x. F(x)) & (∃y. G(y))
--> ( ((∀x. F(x)-->H(x)) & (∀y. G(y)-->J(y)))  =
(∀x y. F(x) & G(y) --> H(x) & J(y)))"
by blast

text‹Problem 30›
lemma "(∀x. P(x) | Q(x) --> ~ R(x)) &
(∀x. (Q(x) --> ~ S(x)) --> P(x) & R(x))
--> (∀x. S(x))"
by blast

text‹Problem 31›
lemma "~(∃x. P(x) & (Q(x) | R(x))) &
(∃x. L(x) & P(x)) &
(∀x. ~ R(x) --> M(x))
--> (∃x. L(x) & M(x))"
by blast

text‹Problem 32›
lemma "(∀x. P(x) & (Q(x)|R(x))-->S(x)) &
(∀x. S(x) & R(x) --> L(x)) &
(∀x. M(x) --> R(x))
--> (∀x. P(x) & M(x) --> L(x))"
by blast

text‹Problem 33›
lemma "(∀x. P(a) & (P(x)-->P(b))-->P(c))  =
(∀x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))"
by blast

text‹Problem 34  AMENDED (TWICE!!)›
text‹Andrews's challenge›
lemma "((∃x. ∀y. p(x) = p(y))  =
((∃x. q(x)) = (∀y. p(y))))   =
((∃x. ∀y. q(x) = q(y))  =
((∃x. p(x)) = (∀y. q(y))))"
by blast

text‹Problem 35›
lemma "∃x y. P x y -->  (∀u v. P u v)"
by blast

text‹Problem 36›
lemma "(∀x. ∃y. J x y) &
(∀x. ∃y. G x y) &
(∀x y. J x y | G x y -->
(∀z. J y z | G y z --> H x z))
--> (∀x. ∃y. H x y)"
by blast

text‹Problem 37›
lemma "(∀z. ∃w. ∀x. ∃y.
(P x z -->P y w) & P y z & (P y w --> (∃u. Q u w))) &
(∀x z. ~(P x z) --> (∃y. Q y z)) &
((∃x y. Q x y) --> (∀x. R x x))
--> (∀x. ∃y. R x y)"
by blast

text‹Problem 38›
lemma "(∀x. p(a) & (p(x) --> (∃y. p(y) & r x y)) -->
(∃z. ∃w. p(z) & r x w & r w z))  =
(∀x. (~p(a) | p(x) | (∃z. ∃w. p(z) & r x w & r w z)) &
(~p(a) | ~(∃y. p(y) & r x y) |
(∃z. ∃w. p(z) & r x w & r w z)))"
by blast (*beats fast!*)

text‹Problem 39›
lemma "~ (∃x. ∀y. F y x = (~ F y y))"
by blast

text‹Problem 40.  AMENDED›
lemma "(∃y. ∀x. F x y = F x x)
-->  ~ (∀x. ∃y. ∀z. F z y = (~ F z x))"
by blast

text‹Problem 41›
lemma "(∀z. ∃y. ∀x. f x y = (f x z & ~ f x x))
--> ~ (∃z. ∀x. f x z)"
by blast

text‹Problem 42›
lemma "~ (∃y. ∀x. p x y = (~ (∃z. p x z & p z x)))"
by blast

text‹Problem 43!!›
lemma "(∀x::'a. ∀y::'a. q x y = (∀z. p z x = (p z y::bool)))
--> (∀x. (∀y. q x y = (q y x::bool)))"
by blast

text‹Problem 44›
lemma "(∀x. f(x) -->
(∃y. g(y) & h x y & (∃y. g(y) & ~ h x y)))  &
(∃x. j(x) & (∀y. g(y) --> h x y))
--> (∃x. j(x) & ~f(x))"
by blast

text‹Problem 45›
lemma "(∀x. f(x) & (∀y. g(y) & h x y --> j x y)
--> (∀y. g(y) & h x y --> k(y))) &
~ (∃y. l(y) & k(y)) &
(∃x. f(x) & (∀y. h x y --> l(y))
& (∀y. g(y) & h x y --> j x y))
--> (∃x. f(x) & ~ (∃y. g(y) & h x y))"
by blast

subsubsection‹Problems (mainly) involving equality or functions›

text‹Problem 48›
lemma "(a=b | c=d) & (a=c | b=d) --> a=d | b=c"
by blast

text‹Problem 49  NOT PROVED AUTOMATICALLY.
Hard because it involves substitution for Vars
the type constraint ensures that x,y,z have the same type as a,b,u.›
lemma "(∃x y::'a. ∀z. z=x | z=y) & P(a) & P(b) & (~a=b)
--> (∀u::'a. P(u))"
by metis

text‹Problem 50.  (What has this to do with equality?)›
lemma "(∀x. P a x | (∀y. P x y)) --> (∃x. ∀y. P x y)"
by blast

text‹Problem 51›
lemma "(∃z w. ∀x y. P x y = (x=z & y=w)) -->
(∃z. ∀x. ∃w. (∀y. P x y = (y=w)) = (x=z))"
by blast

text‹Problem 52. Almost the same as 51.›
lemma "(∃z w. ∀x y. P x y = (x=z & y=w)) -->
(∃w. ∀y. ∃z. (∀x. P x y = (x=z)) = (y=w))"
by blast

text‹Problem 55›

text‹Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988).
fast DISCOVERS who killed Agatha.›
schematic_goal "lives(agatha) & lives(butler) & lives(charles) &
(killed agatha agatha | killed butler agatha | killed charles agatha) &
(∀x y. killed x y --> hates x y & ~richer x y) &
(∀x. hates agatha x --> ~hates charles x) &
(hates agatha agatha & hates agatha charles) &
(∀x. lives(x) & ~richer x agatha --> hates butler x) &
(∀x. hates agatha x --> hates butler x) &
(∀x. ~hates x agatha | ~hates x butler | ~hates x charles) -->
killed ?who agatha"
by fast

text‹Problem 56›
lemma "(∀x. (∃y. P(y) & x=f(y)) --> P(x)) = (∀x. P(x) --> P(f(x)))"
by blast

text‹Problem 57›
lemma "P (f a b) (f b c) & P (f b c) (f a c) &
(∀x y z. P x y & P y z --> P x z)    -->   P (f a b) (f a c)"
by blast

text‹Problem 58  NOT PROVED AUTOMATICALLY›
lemma "(∀x y. f(x)=g(y)) --> (∀x y. f(f(x))=f(g(y)))"
by (fast intro: arg_cong [of concl: f])

text‹Problem 59›
lemma "(∀x. P(x) = (~P(f(x)))) --> (∃x. P(x) & ~P(f(x)))"
by blast

text‹Problem 60›
lemma "∀x. P x (f x) = (∃y. (∀z. P z y --> P z (f x)) & P x y)"
by blast

text‹Problem 62 as corrected in JAR 18 (1997), page 135›
lemma "(∀x. p a & (p x --> p(f x)) --> p(f(f x)))  =
(∀x. (~ p a | p x | p(f(f x))) &
(~ p a | ~ p(f x) | p(f(f x))))"
by blast

text‹From Davis, Obvious Logical Inferences, IJCAI-81, 530-531
fast indeed copes!›
lemma "(∀x. F(x) & ~G(x) --> (∃y. H(x,y) & J(y))) &
(∃x. K(x) & F(x) & (∀y. H(x,y) --> K(y))) &
(∀x. K(x) --> ~G(x))  -->  (∃x. K(x) & J(x))"
by fast

text‹From Rudnicki, Obvious Inferences, JAR 3 (1987), 383-393.
It does seem obvious!›
lemma "(∀x. F(x) & ~G(x) --> (∃y. H(x,y) & J(y))) &
(∃x. K(x) & F(x) & (∀y. H(x,y) --> K(y)))  &
(∀x. K(x) --> ~G(x))   -->   (∃x. K(x) --> ~G(x))"
by fast

text‹Attributed to Lewis Carroll by S. G. Pulman.  The first or last
assumption can be deleted.›
lemma "(∀x. honest(x) & industrious(x) --> healthy(x)) &
~ (∃x. grocer(x) & healthy(x)) &
(∀x. industrious(x) & grocer(x) --> honest(x)) &
(∀x. cyclist(x) --> industrious(x)) &
(∀x. ~healthy(x) & cyclist(x) --> ~honest(x))
--> (∀x. grocer(x) --> ~cyclist(x))"
by blast

lemma "(∀x y. R(x,y) | R(y,x)) &
(∀x y. S(x,y) & S(y,x) --> x=y) &
(∀x y. R(x,y) --> S(x,y))    -->   (∀x y. S(x,y) --> R(x,y))"
by blast

subsection‹Model Elimination Prover›

text‹Trying out meson with arguments›
lemma "x < y & y < z --> ~ (z < (x::nat))"
by (meson order_less_irrefl order_less_trans)

text‹The "small example" from Bezem, Hendriks and de Nivelle,
Automatic Proof Construction in Type Theory Using Resolution,
JAR 29: 3-4 (2002), pages 253-275›
lemma "(∀x y z. R(x,y) & R(y,z) --> R(x,z)) &
(∀x. ∃y. R(x,y)) -->
~ (∀x. P x = (∀y. R(x,y) --> ~ P y))"
by (tactic‹Meson.safe_best_meson_tac @{context} 1›)
―‹In contrast, ‹meson› is SLOW: 7.6s on griffon›

subsubsection‹Pelletier's examples›
text‹1›
lemma "(P --> Q)  =  (~Q --> ~P)"
by blast

text‹2›
lemma "(~ ~ P) =  P"
by blast

text‹3›
lemma "~(P-->Q) --> (Q-->P)"
by blast

text‹4›
lemma "(~P-->Q)  =  (~Q --> P)"
by blast

text‹5›
lemma "((P|Q)-->(P|R)) --> (P|(Q-->R))"
by blast

text‹6›
lemma "P | ~ P"
by blast

text‹7›
lemma "P | ~ ~ ~ P"
by blast

text‹8.  Peirce's law›
lemma "((P-->Q) --> P)  -->  P"
by blast

text‹9›
lemma "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
by blast

text‹10›
lemma "(Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P=Q)"
by blast

text‹11.  Proved in each direction (incorrectly, says Pelletier!!)›
lemma "P=(P::bool)"
by blast

text‹12.  "Dijkstra's law"›
lemma "((P = Q) = R) = (P = (Q = R))"
by blast

text‹13.  Distributive law›
lemma "(P | (Q & R)) = ((P | Q) & (P | R))"
by blast

text‹14›
lemma "(P = Q) = ((Q | ~P) & (~Q|P))"
by blast

text‹15›
lemma "(P --> Q) = (~P | Q)"
by blast

text‹16›
lemma "(P-->Q) | (Q-->P)"
by blast

text‹17›
lemma "((P & (Q-->R))-->S)  =  ((~P | Q | S) & (~P | ~R | S))"
by blast

subsubsection‹Classical Logic: examples with quantifiers›

lemma "(∀x. P x & Q x) = ((∀x. P x) & (∀x. Q x))"
by blast

lemma "(∃x. P --> Q x)  =  (P --> (∃x. Q x))"
by blast

lemma "(∃x. P x --> Q) = ((∀x. P x) --> Q)"
by blast

lemma "((∀x. P x) | Q)  =  (∀x. P x | Q)"
by blast

lemma "(∀x. P x --> P(f x))  &  P d --> P(f(f(f d)))"
by blast

text‹Needs double instantiation of EXISTS›
lemma "∃x. P x --> P a & P b"
by blast

lemma "∃z. P z --> (∀x. P x)"
by blast

text‹From a paper by Claire Quigley›
lemma "∃y. ((P c & Q y) | (∃z. ~ Q z)) | (∃x. ~ P x & Q d)"
by fast

subsubsection‹Hard examples with quantifiers›

text‹Problem 18›
lemma "∃y. ∀x. P y --> P x"
by blast

text‹Problem 19›
lemma "∃x. ∀y z. (P y --> Q z) --> (P x --> Q x)"
by blast

text‹Problem 20›
lemma "(∀x y. ∃z. ∀w. (P x & Q y --> R z & S w))
--> (∃x y. P x & Q y) --> (∃z. R z)"
by blast

text‹Problem 21›
lemma "(∃x. P --> Q x) & (∃x. Q x --> P) --> (∃x. P=Q x)"
by blast

text‹Problem 22›
lemma "(∀x. P = Q x)  -->  (P = (∀x. Q x))"
by blast

text‹Problem 23›
lemma "(∀x. P | Q x)  =  (P | (∀x. Q x))"
by blast

text‹Problem 24›  (*The first goal clause is useless*)
lemma "~(∃x. S x & Q x) & (∀x. P x --> Q x | R x) &
(~(∃x. P x) --> (∃x. Q x)) & (∀x. Q x | R x --> S x)
--> (∃x. P x & R x)"
by blast

text‹Problem 25›
lemma "(∃x. P x) &
(∀x. L x --> ~ (M x & R x)) &
(∀x. P x --> (M x & L x)) &
((∀x. P x --> Q x) | (∃x. P x & R x))
--> (∃x. Q x & P x)"
by blast

text‹Problem 26; has 24 Horn clauses›
lemma "((∃x. p x) = (∃x. q x)) &
(∀x. ∀y. p x & q y --> (r x = s y))
--> ((∀x. p x --> r x) = (∀x. q x --> s x))"
by blast

text‹Problem 27; has 13 Horn clauses›
lemma "(∃x. P x & ~Q x) &
(∀x. P x --> R x) &
(∀x. M x & L x --> P x) &
((∃x. R x & ~ Q x) --> (∀x. L x --> ~ R x))
--> (∀x. M x --> ~L x)"
by blast

text‹Problem 28.  AMENDED; has 14 Horn clauses›
lemma "(∀x. P x --> (∀x. Q x)) &
((∀x. Q x | R x) --> (∃x. Q x & S x)) &
((∃x. S x) --> (∀x. L x --> M x))
--> (∀x. P x & L x --> M x)"
by blast

text‹Problem 29.  Essentially the same as Principia Mathematica *11.71.
62 Horn clauses›
lemma "(∃x. F x) & (∃y. G y)
--> ( ((∀x. F x --> H x) & (∀y. G y --> J y))  =
(∀x y. F x & G y --> H x & J y))"
by blast

text‹Problem 30›
lemma "(∀x. P x | Q x --> ~ R x) & (∀x. (Q x --> ~ S x) --> P x & R x)
--> (∀x. S x)"
by blast

text‹Problem 31; has 10 Horn clauses; first negative clauses is useless›
lemma "~(∃x. P x & (Q x | R x)) &
(∃x. L x & P x) &
(∀x. ~ R x --> M x)
--> (∃x. L x & M x)"
by blast

text‹Problem 32›
lemma "(∀x. P x & (Q x | R x)-->S x) &
(∀x. S x & R x --> L x) &
(∀x. M x --> R x)
--> (∀x. P x & M x --> L x)"
by blast

text‹Problem 33; has 55 Horn clauses›
lemma "(∀x. P a & (P x --> P b)-->P c)  =
(∀x. (~P a | P x | P c) & (~P a | ~P b | P c))"
by blast

text‹Problem 34: Andrews's challenge has 924 Horn clauses›
lemma "((∃x. ∀y. p x = p y)  = ((∃x. q x) = (∀y. p y)))     =
((∃x. ∀y. q x = q y)  = ((∃x. p x) = (∀y. q y)))"
by blast

text‹Problem 35›
lemma "∃x y. P x y -->  (∀u v. P u v)"
by blast

text‹Problem 36; has 15 Horn clauses›
lemma "(∀x. ∃y. J x y) & (∀x. ∃y. G x y) &
(∀x y. J x y | G x y --> (∀z. J y z | G y z --> H x z))
--> (∀x. ∃y. H x y)"
by blast

text‹Problem 37; has 10 Horn clauses›
lemma "(∀z. ∃w. ∀x. ∃y.
(P x z --> P y w) & P y z & (P y w --> (∃u. Q u w))) &
(∀x z. ~P x z --> (∃y. Q y z)) &
((∃x y. Q x y) --> (∀x. R x x))
--> (∀x. ∃y. R x y)"
by blast ―‹causes unification tracing messages›

text‹Problem 38›  text‹Quite hard: 422 Horn clauses!!›
lemma "(∀x. p a & (p x --> (∃y. p y & r x y)) -->
(∃z. ∃w. p z & r x w & r w z))  =
(∀x. (~p a | p x | (∃z. ∃w. p z & r x w & r w z)) &
(~p a | ~(∃y. p y & r x y) |
(∃z. ∃w. p z & r x w & r w z)))"
by blast

text‹Problem 39›
lemma "~ (∃x. ∀y. F y x = (~F y y))"
by blast

text‹Problem 40.  AMENDED›
lemma "(∃y. ∀x. F x y = F x x)
-->  ~ (∀x. ∃y. ∀z. F z y = (~F z x))"
by blast

text‹Problem 41›
lemma "(∀z. (∃y. (∀x. f x y = (f x z & ~ f x x))))
--> ~ (∃z. ∀x. f x z)"
by blast

text‹Problem 42›
lemma "~ (∃y. ∀x. p x y = (~ (∃z. p x z & p z x)))"
by blast

text‹Problem 43  NOW PROVED AUTOMATICALLY!!›
lemma "(∀x. ∀y. q x y = (∀z. p z x = (p z y::bool)))
--> (∀x. (∀y. q x y = (q y x::bool)))"
by blast

text‹Problem 44: 13 Horn clauses; 7-step proof›
lemma "(∀x. f x --> (∃y. g y & h x y & (∃y. g y & ~ h x y)))  &
(∃x. j x & (∀y. g y --> h x y))
--> (∃x. j x & ~f x)"
by blast

text‹Problem 45; has 27 Horn clauses; 54-step proof›
lemma "(∀x. f x & (∀y. g y & h x y --> j x y)
--> (∀y. g y & h x y --> k y)) &
~ (∃y. l y & k y) &
(∃x. f x & (∀y. h x y --> l y)
& (∀y. g y & h x y --> j x y))
--> (∃x. f x & ~ (∃y. g y & h x y))"
by blast

text‹Problem 46; has 26 Horn clauses; 21-step proof›
lemma "(∀x. f x & (∀y. f y & h y x --> g y) --> g x) &
((∃x. f x & ~g x) -->
(∃x. f x & ~g x & (∀y. f y & ~g y --> j x y))) &
(∀x y. f x & f y & h x y --> ~j y x)
--> (∀x. f x --> g x)"
by blast

text‹Problem 47.  Schubert's Steamroller.
26 clauses; 63 Horn clauses.
87094 inferences so far.  Searching to depth 36›
lemma "(∀x. wolf x ⟶ animal x) & (∃x. wolf x) &
(∀x. fox x ⟶ animal x) & (∃x. fox x) &
(∀x. bird x ⟶ animal x) & (∃x. bird x) &
(∀x. caterpillar x ⟶ animal x) & (∃x. caterpillar x) &
(∀x. snail x ⟶ animal x) & (∃x. snail x) &
(∀x. grain x ⟶ plant x) & (∃x. grain x) &
(∀x. animal x ⟶
((∀y. plant y ⟶ eats x y)  ∨
(∀y. animal y & smaller_than y x &
(∃z. plant z & eats y z) ⟶ eats x y))) &
(∀x y. bird y & (snail x ∨ caterpillar x) ⟶ smaller_than x y) &
(∀x y. bird x & fox y ⟶ smaller_than x y) &
(∀x y. fox x & wolf y ⟶ smaller_than x y) &
(∀x y. wolf x & (fox y ∨ grain y) ⟶ ~eats x y) &
(∀x y. bird x & caterpillar y ⟶ eats x y) &
(∀x y. bird x & snail y ⟶ ~eats x y) &
(∀x. (caterpillar x ∨ snail x) ⟶ (∃y. plant y & eats x y))
⟶ (∃x y. animal x & animal y & (∃z. grain z & eats y z & eats x y))"
by (tactic‹Meson.safe_best_meson_tac @{context} 1›)
―‹Nearly twice as fast as ‹meson›,
which performs iterative deepening rather than best-first search›

text‹The Los problem. Circulated by John Harrison›
lemma "(∀x y z. P x y & P y z --> P x z) &
(∀x y z. Q x y & Q y z --> Q x z) &
(∀x y. P x y --> P y x) &
(∀x y. P x y | Q x y)
--> (∀x y. P x y) | (∀x y. Q x y)"
by meson

text‹A similar example, suggested by Johannes Schumann and
credited to Pelletier›
lemma "(∀x y z. P x y --> P y z --> P x z) -->
(∀x y z. Q x y --> Q y z --> Q x z) -->
(∀x y. Q x y --> Q y x) -->  (∀x y. P x y | Q x y) -->
(∀x y. P x y) | (∀x y. Q x y)"
by meson

text‹Problem 50.  What has this to do with equality?›
lemma "(∀x. P a x | (∀y. P x y)) --> (∃x. ∀y. P x y)"
by blast

text‹Problem 54: NOT PROVED›
lemma "(∀y::'a. ∃z. ∀x. F x z = (x=y)) -->
~ (∃w. ∀x. F x w = (∀u. F x u --> (∃y. F y u & ~ (∃z. F z u & F z y))))"
oops

text‹Problem 55›

text‹Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988).
‹meson› cannot report who killed Agatha.›
lemma "lives agatha & lives butler & lives charles &
(killed agatha agatha | killed butler agatha | killed charles agatha) &
(∀x y. killed x y --> hates x y & ~richer x y) &
(∀x. hates agatha x --> ~hates charles x) &
(hates agatha agatha & hates agatha charles) &
(∀x. lives x & ~richer x agatha --> hates butler x) &
(∀x. hates agatha x --> hates butler x) &
(∀x. ~hates x agatha | ~hates x butler | ~hates x charles) -->
(∃x. killed x agatha)"
by meson

text‹Problem 57›
lemma "P (f a b) (f b c) & P (f b c) (f a c) &
(∀x y z. P x y & P y z --> P x z)    -->   P (f a b) (f a c)"
by blast

text‹Problem 58: Challenge found on info-hol›
lemma "∀P Q R x. ∃v w. ∀y z. P x & Q y --> (P v | R w) & (R z --> Q v)"
by blast

text‹Problem 59›
lemma "(∀x. P x = (~P(f x))) --> (∃x. P x & ~P(f x))"
by blast

text‹Problem 60›
lemma "∀x. P x (f x) = (∃y. (∀z. P z y --> P z (f x)) & P x y)"
by blast

text‹Problem 62 as corrected in JAR 18 (1997), page 135›
lemma "(∀x. p a & (p x --> p(f x)) --> p(f(f x)))  =
(∀x. (~ p a | p x | p(f(f x))) &
(~ p a | ~ p(f x) | p(f(f x))))"
by blast

text‹Charles Morgan's problems›
context
fixes T i n
assumes a: "∀x y. T(i x(i y x))"
and b: "∀x y z. T(i (i x (i y z)) (i (i x y) (i x z)))"
and c: "∀x y. T(i (i (n x) (n y)) (i y x))"
and c': "∀x y. T(i (i y x) (i (n x) (n y)))"
and d: "∀x y. T(i x y) & T x --> T y"
begin

lemma "∀x. T(i x x)"
using a b d by blast

lemma "∀x. T(i x (n(n x)))" ―‹Problem 66›
using a b c d by metis

lemma "∀x. T(i (n(n x)) x)" ―‹Problem 67›
using a b c d by meson ―‹4.9s on griffon. 51061 inferences, depth 21›

lemma "∀x. T(i x (n(n x)))" ―‹Problem 68: not proved.  Listed as satisfiable in TPTP (LCL078-1)›
using a b c' d oops

end

text‹Problem 71, as found in TPTP (SYN007+1.005)›
lemma "p1 = (p2 = (p3 = (p4 = (p5 = (p1 = (p2 = (p3 = (p4 = p5))))))))"
by blast

end
```