14236

1 
(* Title: FOL/ex/Classical


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1994 University of Cambridge


5 
*)


6 


7 
header{*Classical Predicate Calculus Problems*}


8 

16417

9 
theory Classical imports FOL begin

14236

10 


11 
lemma "(P > Q  R) > (P>Q)  (P>R)"


12 
by blast


13 


14 
text{*If and only if*}


15 


16 
lemma "(P<>Q) <> (Q<>P)"


17 
by blast


18 


19 
lemma "~ (P <> ~P)"


20 
by blast


21 


22 


23 
text{*Sample problems from


24 
F. J. Pelletier,


25 
SeventyFive Problems for Testing Automatic Theorem Provers,


26 
J. Automated Reasoning 2 (1986), 191216.


27 
Errata, JAR 4 (1988), 236236.


28 


29 
The hardest problems  judging by experience with several theorem provers,


30 
including matrix ones  are 34 and 43.


31 
*}


32 


33 
subsection{*Pelletier's examples*}


34 


35 
text{*1*}


36 
lemma "(P>Q) <> (~Q > ~P)"


37 
by blast


38 


39 
text{*2*}


40 
lemma "~ ~ P <> P"


41 
by blast


42 


43 
text{*3*}


44 
lemma "~(P>Q) > (Q>P)"


45 
by blast


46 


47 
text{*4*}


48 
lemma "(~P>Q) <> (~Q > P)"


49 
by blast


50 


51 
text{*5*}


52 
lemma "((PQ)>(PR)) > (P(Q>R))"


53 
by blast


54 


55 
text{*6*}


56 
lemma "P  ~ P"


57 
by blast


58 


59 
text{*7*}


60 
lemma "P  ~ ~ ~ P"


61 
by blast


62 


63 
text{*8. Peirce's law*}


64 
lemma "((P>Q) > P) > P"


65 
by blast


66 


67 
text{*9*}


68 
lemma "((PQ) & (~PQ) & (P ~Q)) > ~ (~P  ~Q)"


69 
by blast


70 


71 
text{*10*}


72 
lemma "(Q>R) & (R>P&Q) & (P>QR) > (P<>Q)"


73 
by blast


74 


75 
text{*11. Proved in each direction (incorrectly, says Pelletier!!) *}


76 
lemma "P<>P"


77 
by blast


78 


79 
text{*12. "Dijkstra's law"*}


80 
lemma "((P <> Q) <> R) <> (P <> (Q <> R))"


81 
by blast


82 


83 
text{*13. Distributive law*}


84 
lemma "P  (Q & R) <> (P  Q) & (P  R)"


85 
by blast


86 


87 
text{*14*}


88 
lemma "(P <> Q) <> ((Q  ~P) & (~QP))"


89 
by blast


90 


91 
text{*15*}


92 
lemma "(P > Q) <> (~P  Q)"


93 
by blast


94 


95 
text{*16*}


96 
lemma "(P>Q)  (Q>P)"


97 
by blast


98 


99 
text{*17*}


100 
lemma "((P & (Q>R))>S) <> ((~P  Q  S) & (~P  ~R  S))"


101 
by blast


102 


103 
subsection{*Classical Logic: examples with quantifiers*}


104 


105 
lemma "(\<forall>x. P(x) & Q(x)) <> (\<forall>x. P(x)) & (\<forall>x. Q(x))"


106 
by blast


107 


108 
lemma "(\<exists>x. P>Q(x)) <> (P > (\<exists>x. Q(x)))"


109 
by blast


110 


111 
lemma "(\<exists>x. P(x)>Q) <> (\<forall>x. P(x)) > Q"


112 
by blast


113 


114 
lemma "(\<forall>x. P(x))  Q <> (\<forall>x. P(x)  Q)"


115 
by blast


116 


117 
text{*Discussed in Avron, GentzenType Systems, Resolution and Tableaux,


118 
JAR 10 (265281), 1993. Proof is trivial!*}


119 
lemma "~((\<exists>x.~P(x)) & ((\<exists>x. P(x))  (\<exists>x. P(x) & Q(x))) & ~ (\<exists>x. P(x)))"


120 
by blast


121 


122 
subsection{*Problems requiring quantifier duplication*}


123 


124 
text{*Theorem B of Peter Andrews, Theorem Proving via General Matings,


125 
JACM 28 (1981).*}


126 
lemma "(\<exists>x. \<forall>y. P(x) <> P(y)) > ((\<exists>x. P(x)) <> (\<forall>y. P(y)))"


127 
by blast


128 


129 
text{*Needs multiple instantiation of ALL.*}


130 
lemma "(\<forall>x. P(x)>P(f(x))) & P(d)>P(f(f(f(d))))"


131 
by blast


132 


133 
text{*Needs double instantiation of the quantifier*}


134 
lemma "\<exists>x. P(x) > P(a) & P(b)"


135 
by blast


136 


137 
lemma "\<exists>z. P(z) > (\<forall>x. P(x))"


138 
by blast


139 


140 
lemma "\<exists>x. (\<exists>y. P(y)) > P(x)"


141 
by blast


142 


143 
text{*V. Lifschitz, What Is the Inverse Method?, JAR 5 (1989), 123. NOT PROVED*}


144 
lemma "\<exists>x x'. \<forall>y. \<exists>z z'.


145 
(~P(y,y)  P(x,x)  ~S(z,x)) &


146 
(S(x,y)  ~S(y,z)  Q(z',z')) &


147 
(Q(x',y)  ~Q(y,z')  S(x',x'))"


148 
oops


149 


150 


151 


152 
subsection{*Hard examples with quantifiers*}


153 


154 
text{*18*}


155 
lemma "\<exists>y. \<forall>x. P(y)>P(x)"


156 
by blast


157 


158 
text{*19*}


159 
lemma "\<exists>x. \<forall>y z. (P(y)>Q(z)) > (P(x)>Q(x))"


160 
by blast


161 


162 
text{*20*}


163 
lemma "(\<forall>x y. \<exists>z. \<forall>w. (P(x)&Q(y)>R(z)&S(w)))


164 
> (\<exists>x y. P(x) & Q(y)) > (\<exists>z. R(z))"


165 
by blast


166 


167 
text{*21*}


168 
lemma "(\<exists>x. P>Q(x)) & (\<exists>x. Q(x)>P) > (\<exists>x. P<>Q(x))"


169 
by blast


170 


171 
text{*22*}


172 
lemma "(\<forall>x. P <> Q(x)) > (P <> (\<forall>x. Q(x)))"


173 
by blast


174 


175 
text{*23*}


176 
lemma "(\<forall>x. P  Q(x)) <> (P  (\<forall>x. Q(x)))"


177 
by blast


178 


179 
text{*24*}


180 
lemma "~(\<exists>x. S(x)&Q(x)) & (\<forall>x. P(x) > Q(x)R(x)) &


181 
(~(\<exists>x. P(x)) > (\<exists>x. Q(x))) & (\<forall>x. Q(x)R(x) > S(x))


182 
> (\<exists>x. P(x)&R(x))"


183 
by blast


184 


185 
text{*25*}


186 
lemma "(\<exists>x. P(x)) &


187 
(\<forall>x. L(x) > ~ (M(x) & R(x))) &


188 
(\<forall>x. P(x) > (M(x) & L(x))) &


189 
((\<forall>x. P(x)>Q(x))  (\<exists>x. P(x)&R(x)))


190 
> (\<exists>x. Q(x)&P(x))"


191 
by blast


192 


193 
text{*26*}


194 
lemma "((\<exists>x. p(x)) <> (\<exists>x. q(x))) &


195 
(\<forall>x. \<forall>y. p(x) & q(y) > (r(x) <> s(y)))


196 
> ((\<forall>x. p(x)>r(x)) <> (\<forall>x. q(x)>s(x)))"


197 
by blast


198 


199 
text{*27*}


200 
lemma "(\<exists>x. P(x) & ~Q(x)) &


201 
(\<forall>x. P(x) > R(x)) &


202 
(\<forall>x. M(x) & L(x) > P(x)) &


203 
((\<exists>x. R(x) & ~ Q(x)) > (\<forall>x. L(x) > ~ R(x)))


204 
> (\<forall>x. M(x) > ~L(x))"


205 
by blast


206 


207 
text{*28. AMENDED*}


208 
lemma "(\<forall>x. P(x) > (\<forall>x. Q(x))) &


209 
((\<forall>x. Q(x)R(x)) > (\<exists>x. Q(x)&S(x))) &


210 
((\<exists>x. S(x)) > (\<forall>x. L(x) > M(x)))


211 
> (\<forall>x. P(x) & L(x) > M(x))"


212 
by blast


213 


214 
text{*29. Essentially the same as Principia Mathematica *11.71*}


215 
lemma "(\<exists>x. P(x)) & (\<exists>y. Q(y))


216 
> ((\<forall>x. P(x)>R(x)) & (\<forall>y. Q(y)>S(y)) <>


217 
(\<forall>x y. P(x) & Q(y) > R(x) & S(y)))"


218 
by blast


219 


220 
text{*30*}


221 
lemma "(\<forall>x. P(x)  Q(x) > ~ R(x)) &


222 
(\<forall>x. (Q(x) > ~ S(x)) > P(x) & R(x))


223 
> (\<forall>x. S(x))"


224 
by blast


225 


226 
text{*31*}


227 
lemma "~(\<exists>x. P(x) & (Q(x)  R(x))) &


228 
(\<exists>x. L(x) & P(x)) &


229 
(\<forall>x. ~ R(x) > M(x))


230 
> (\<exists>x. L(x) & M(x))"


231 
by blast


232 


233 
text{*32*}


234 
lemma "(\<forall>x. P(x) & (Q(x)R(x))>S(x)) &


235 
(\<forall>x. S(x) & R(x) > L(x)) &


236 
(\<forall>x. M(x) > R(x))


237 
> (\<forall>x. P(x) & M(x) > L(x))"


238 
by blast


239 


240 
text{*33*}


241 
lemma "(\<forall>x. P(a) & (P(x)>P(b))>P(c)) <>


242 
(\<forall>x. (~P(a)  P(x)  P(c)) & (~P(a)  ~P(b)  P(c)))"


243 
by blast


244 


245 
text{*34 AMENDED (TWICE!!). Andrews's challenge*}


246 
lemma "((\<exists>x. \<forall>y. p(x) <> p(y)) <>


247 
((\<exists>x. q(x)) <> (\<forall>y. p(y)))) <>


248 
((\<exists>x. \<forall>y. q(x) <> q(y)) <>


249 
((\<exists>x. p(x)) <> (\<forall>y. q(y))))"


250 
by blast


251 


252 
text{*35*}


253 
lemma "\<exists>x y. P(x,y) > (\<forall>u v. P(u,v))"


254 
by blast


255 


256 
text{*36*}


257 
lemma "(\<forall>x. \<exists>y. J(x,y)) &


258 
(\<forall>x. \<exists>y. G(x,y)) &


259 
(\<forall>x y. J(x,y)  G(x,y) > (\<forall>z. J(y,z)  G(y,z) > H(x,z)))


260 
> (\<forall>x. \<exists>y. H(x,y))"


261 
by blast


262 


263 
text{*37*}


264 
lemma "(\<forall>z. \<exists>w. \<forall>x. \<exists>y.


265 
(P(x,z)>P(y,w)) & P(y,z) & (P(y,w) > (\<exists>u. Q(u,w)))) &


266 
(\<forall>x z. ~P(x,z) > (\<exists>y. Q(y,z))) &


267 
((\<exists>x y. Q(x,y)) > (\<forall>x. R(x,x)))


268 
> (\<forall>x. \<exists>y. R(x,y))"


269 
by blast


270 


271 
text{*38*}


272 
lemma "(\<forall>x. p(a) & (p(x) > (\<exists>y. p(y) & r(x,y))) >


273 
(\<exists>z. \<exists>w. p(z) & r(x,w) & r(w,z))) <>


274 
(\<forall>x. (~p(a)  p(x)  (\<exists>z. \<exists>w. p(z) & r(x,w) & r(w,z))) &


275 
(~p(a)  ~(\<exists>y. p(y) & r(x,y)) 


276 
(\<exists>z. \<exists>w. p(z) & r(x,w) & r(w,z))))"


277 
by blast


278 


279 
text{*39*}


280 
lemma "~ (\<exists>x. \<forall>y. F(y,x) <> ~F(y,y))"


281 
by blast


282 


283 
text{*40. AMENDED*}


284 
lemma "(\<exists>y. \<forall>x. F(x,y) <> F(x,x)) >


285 
~(\<forall>x. \<exists>y. \<forall>z. F(z,y) <> ~ F(z,x))"


286 
by blast


287 


288 
text{*41*}


289 
lemma "(\<forall>z. \<exists>y. \<forall>x. f(x,y) <> f(x,z) & ~ f(x,x))


290 
> ~ (\<exists>z. \<forall>x. f(x,z))"


291 
by blast


292 


293 
text{*42*}


294 
lemma "~ (\<exists>y. \<forall>x. p(x,y) <> ~ (\<exists>z. p(x,z) & p(z,x)))"


295 
by blast


296 


297 
text{*43*}


298 
lemma "(\<forall>x. \<forall>y. q(x,y) <> (\<forall>z. p(z,x) <> p(z,y)))


299 
> (\<forall>x. \<forall>y. q(x,y) <> q(y,x))"


300 
by blast


301 


302 
(*Other proofs: Can use auto, which cheats by using rewriting!


303 
Deepen_tac alone requires 253 secs. Or


304 
by (mini_tac 1 THEN Deepen_tac 5 1) *)


305 


306 
text{*44*}


307 
lemma "(\<forall>x. f(x) > (\<exists>y. g(y) & h(x,y) & (\<exists>y. g(y) & ~ h(x,y)))) &


308 
(\<exists>x. j(x) & (\<forall>y. g(y) > h(x,y)))


309 
> (\<exists>x. j(x) & ~f(x))"


310 
by blast


311 


312 
text{*45*}


313 
lemma "(\<forall>x. f(x) & (\<forall>y. g(y) & h(x,y) > j(x,y))


314 
> (\<forall>y. g(y) & h(x,y) > k(y))) &


315 
~ (\<exists>y. l(y) & k(y)) &


316 
(\<exists>x. f(x) & (\<forall>y. h(x,y) > l(y))


317 
& (\<forall>y. g(y) & h(x,y) > j(x,y)))


318 
> (\<exists>x. f(x) & ~ (\<exists>y. g(y) & h(x,y)))"


319 
by blast


320 


321 


322 
text{*46*}


323 
lemma "(\<forall>x. f(x) & (\<forall>y. f(y) & h(y,x) > g(y)) > g(x)) &


324 
((\<exists>x. f(x) & ~g(x)) >


325 
(\<exists>x. f(x) & ~g(x) & (\<forall>y. f(y) & ~g(y) > j(x,y)))) &


326 
(\<forall>x y. f(x) & f(y) & h(x,y) > ~j(y,x))


327 
> (\<forall>x. f(x) > g(x))"


328 
by blast


329 


330 


331 
subsection{*Problems (mainly) involving equality or functions*}


332 


333 
text{*48*}


334 
lemma "(a=b  c=d) & (a=c  b=d) > a=d  b=c"


335 
by blast


336 


337 
text{*49 NOT PROVED AUTOMATICALLY. Hard because it involves substitution


338 
for Vars


339 
the type constraint ensures that x,y,z have the same type as a,b,u. *}


340 
lemma "(\<exists>x y::'a. \<forall>z. z=x  z=y) & P(a) & P(b) & a~=b


341 
> (\<forall>u::'a. P(u))"


342 
apply safe


343 
apply (rule_tac x = a in allE, assumption)


344 
apply (rule_tac x = b in allE, assumption, fast)


345 
{*blast's treatment of equality can't do it*}


346 
done


347 


348 
text{*50. (What has this to do with equality?) *}


349 
lemma "(\<forall>x. P(a,x)  (\<forall>y. P(x,y))) > (\<exists>x. \<forall>y. P(x,y))"


350 
by blast


351 


352 
text{*51*}


353 
lemma "(\<exists>z w. \<forall>x y. P(x,y) <> (x=z & y=w)) >


354 
(\<exists>z. \<forall>x. \<exists>w. (\<forall>y. P(x,y) <> y=w) <> x=z)"


355 
by blast


356 


357 
text{*52*}


358 
text{*Almost the same as 51. *}


359 
lemma "(\<exists>z w. \<forall>x y. P(x,y) <> (x=z & y=w)) >


360 
(\<exists>w. \<forall>y. \<exists>z. (\<forall>x. P(x,y) <> x=z) <> y=w)"


361 
by blast


362 


363 
text{*55*}


364 


365 
(*Original, equational version by Len Schubert, via Pelletier *** NOT PROVED


366 
Goal "(\<exists>x. lives(x) & killed(x,agatha)) &


367 
lives(agatha) & lives(butler) & lives(charles) &


368 
(\<forall>x. lives(x) > x=agatha  x=butler  x=charles) &


369 
(\<forall>x y. killed(x,y) > hates(x,y)) &


370 
(\<forall>x y. killed(x,y) > ~richer(x,y)) &


371 
(\<forall>x. hates(agatha,x) > ~hates(charles,x)) &


372 
(\<forall>x. ~ x=butler > hates(agatha,x)) &


373 
(\<forall>x. ~richer(x,agatha) > hates(butler,x)) &


374 
(\<forall>x. hates(agatha,x) > hates(butler,x)) &


375 
(\<forall>x. \<exists>y. ~hates(x,y)) &


376 
~ agatha=butler >


377 
killed(?who,agatha)"


378 
by Safe_tac;


379 
by (dres_inst_tac [("x1","x")] (spec RS mp) 1);


380 
by (assume_tac 1);


381 
by (etac (spec RS exE) 1);


382 
by (REPEAT (etac allE 1));


383 
by (Blast_tac 1);


384 
result();


385 
****)


386 


387 
text{*Nonequational version, from Manthey and Bry, CADE9 (Springer, 1988).


388 
fast DISCOVERS who killed Agatha. *}


389 
lemma "lives(agatha) & lives(butler) & lives(charles) &


390 
(killed(agatha,agatha)  killed(butler,agatha)  killed(charles,agatha)) &


391 
(\<forall>x y. killed(x,y) > hates(x,y) & ~richer(x,y)) &


392 
(\<forall>x. hates(agatha,x) > ~hates(charles,x)) &


393 
(hates(agatha,agatha) & hates(agatha,charles)) &


394 
(\<forall>x. lives(x) & ~richer(x,agatha) > hates(butler,x)) &


395 
(\<forall>x. hates(agatha,x) > hates(butler,x)) &


396 
(\<forall>x. ~hates(x,agatha)  ~hates(x,butler)  ~hates(x,charles)) >


397 
killed(?who,agatha)"


398 
by fast {*MUCH faster than blast*}


399 


400 


401 
text{*56*}


402 
lemma "(\<forall>x. (\<exists>y. P(y) & x=f(y)) > P(x)) <> (\<forall>x. P(x) > P(f(x)))"


403 
by blast


404 


405 
text{*57*}


406 
lemma "P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) &


407 
(\<forall>x y z. P(x,y) & P(y,z) > P(x,z)) > P(f(a,b), f(a,c))"


408 
by blast


409 


410 
text{*58 NOT PROVED AUTOMATICALLY*}


411 
lemma "(\<forall>x y. f(x)=g(y)) > (\<forall>x y. f(f(x))=f(g(y)))"


412 
by (slow elim: subst_context)


413 


414 


415 
text{*59*}


416 
lemma "(\<forall>x. P(x) <> ~P(f(x))) > (\<exists>x. P(x) & ~P(f(x)))"


417 
by blast


418 


419 
text{*60*}


420 
lemma "\<forall>x. P(x,f(x)) <> (\<exists>y. (\<forall>z. P(z,y) > P(z,f(x))) & P(x,y))"


421 
by blast


422 


423 
text{*62 as corrected in JAR 18 (1997), page 135*}


424 
lemma "(\<forall>x. p(a) & (p(x) > p(f(x))) > p(f(f(x)))) <>


425 
(\<forall>x. (~p(a)  p(x)  p(f(f(x)))) &


426 
(~p(a)  ~p(f(x))  p(f(f(x)))))"


427 
by blast


428 


429 
text{*From Davis, Obvious Logical Inferences, IJCAI81, 530531


430 
fast indeed copes!*}


431 
lemma "(\<forall>x. F(x) & ~G(x) > (\<exists>y. H(x,y) & J(y))) &


432 
(\<exists>x. K(x) & F(x) & (\<forall>y. H(x,y) > K(y))) &


433 
(\<forall>x. K(x) > ~G(x)) > (\<exists>x. K(x) & J(x))"


434 
by fast


435 


436 
text{*From Rudnicki, Obvious Inferences, JAR 3 (1987), 383393.


437 
It does seem obvious!*}


438 
lemma "(\<forall>x. F(x) & ~G(x) > (\<exists>y. H(x,y) & J(y))) &


439 
(\<exists>x. K(x) & F(x) & (\<forall>y. H(x,y) > K(y))) &


440 
(\<forall>x. K(x) > ~G(x)) > (\<exists>x. K(x) > ~G(x))"


441 
by fast


442 


443 
text{*Halting problem: Formulation of Li Dafa (AAR Newsletter 27, Oct 1994.)


444 
author U. Egly*}


445 
lemma "((\<exists>x. A(x) & (\<forall>y. C(y) > (\<forall>z. D(x,y,z)))) >


446 
(\<exists>w. C(w) & (\<forall>y. C(y) > (\<forall>z. D(w,y,z)))))


447 
&


448 
(\<forall>w. C(w) & (\<forall>u. C(u) > (\<forall>v. D(w,u,v))) >


449 
(\<forall>y z.


450 
(C(y) & P(y,z) > Q(w,y,z) & OO(w,g)) &


451 
(C(y) & ~P(y,z) > Q(w,y,z) & OO(w,b))))


452 
&


453 
(\<forall>w. C(w) &


454 
(\<forall>y z.


455 
(C(y) & P(y,z) > Q(w,y,z) & OO(w,g)) &


456 
(C(y) & ~P(y,z) > Q(w,y,z) & OO(w,b))) >


457 
(\<exists>v. C(v) &


458 
(\<forall>y. ((C(y) & Q(w,y,y)) & OO(w,g) > ~P(v,y)) &


459 
((C(y) & Q(w,y,y)) & OO(w,b) > P(v,y) & OO(v,b)))))


460 
>


461 
~ (\<exists>x. A(x) & (\<forall>y. C(y) > (\<forall>z. D(x,y,z))))"


462 
by (tactic{*Blast.depth_tac (claset ()) 12 1*})


463 
{*Needed because the search for depths below 12 is very slow*}


464 


465 


466 
text{*Halting problem II: credited to M. Bruschi by Li Dafa in JAR 18(1), p.105*}


467 
lemma "((\<exists>x. A(x) & (\<forall>y. C(y) > (\<forall>z. D(x,y,z)))) >


468 
(\<exists>w. C(w) & (\<forall>y. C(y) > (\<forall>z. D(w,y,z)))))


469 
&


470 
(\<forall>w. C(w) & (\<forall>u. C(u) > (\<forall>v. D(w,u,v))) >


471 
(\<forall>y z.


472 
(C(y) & P(y,z) > Q(w,y,z) & OO(w,g)) &


473 
(C(y) & ~P(y,z) > Q(w,y,z) & OO(w,b))))


474 
&


475 
((\<exists>w. C(w) & (\<forall>y. (C(y) & P(y,y) > Q(w,y,y) & OO(w,g)) &


476 
(C(y) & ~P(y,y) > Q(w,y,y) & OO(w,b))))


477 
>


478 
(\<exists>v. C(v) & (\<forall>y. (C(y) & P(y,y) > P(v,y) & OO(v,g)) &


479 
(C(y) & ~P(y,y) > P(v,y) & OO(v,b)))))


480 
>


481 
((\<exists>v. C(v) & (\<forall>y. (C(y) & P(y,y) > P(v,y) & OO(v,g)) &


482 
(C(y) & ~P(y,y) > P(v,y) & OO(v,b))))


483 
>


484 
(\<exists>u. C(u) & (\<forall>y. (C(y) & P(y,y) > ~P(u,y)) &


485 
(C(y) & ~P(y,y) > P(u,y) & OO(u,b)))))


486 
>


487 
~ (\<exists>x. A(x) & (\<forall>y. C(y) > (\<forall>z. D(x,y,z))))"


488 
by blast


489 


490 
text{* Challenge found on infohol *}


491 
lemma "\<forall>x. \<exists>v w. \<forall>y z. P(x) & Q(y) > (P(v)  R(w)) & (R(z) > Q(v))"


492 
by blast


493 


494 
text{*Attributed to Lewis Carroll by S. G. Pulman. The first or last assumption


495 
can be deleted.*}


496 
lemma "(\<forall>x. honest(x) & industrious(x) > healthy(x)) &


497 
~ (\<exists>x. grocer(x) & healthy(x)) &


498 
(\<forall>x. industrious(x) & grocer(x) > honest(x)) &


499 
(\<forall>x. cyclist(x) > industrious(x)) &


500 
(\<forall>x. ~healthy(x) & cyclist(x) > ~honest(x))


501 
> (\<forall>x. grocer(x) > ~cyclist(x))"


502 
by blast


503 


504 


505 
(*Runtimes for old versions of this file:


506 
Thu Jul 23 1992: loaded in 467s using iffE [on SPARC2]


507 
Mon Nov 14 1994: loaded in 144s [on SPARC10, with deepen_tac]


508 
Wed Nov 16 1994: loaded in 138s [after addition of norm_term_skip]


509 
Mon Nov 21 1994: loaded in 131s [DEPTH_FIRST suppressing repetitions]


510 


511 
Further runtimes on a Sun4


512 
Tue Mar 4 1997: loaded in 93s (version 947)


513 
Tue Mar 4 1997: loaded in 89s


514 
Thu Apr 3 1997: loaded in 44susing mostly Blast_tac


515 
Thu Apr 3 1997: loaded in 96saddition of two Halting Probs


516 
Thu Apr 3 1997: loaded in 98susing lim1 for all haz rules


517 
Tue Dec 2 1997: loaded in 107sadded 46; new equalSubst


518 
Fri Dec 12 1997: loaded in 91sfaster proof reconstruction


519 
Thu Dec 18 1997: loaded in 94stwo new "obvious theorems" (??)


520 
*)


521 


522 
end


523 
