diff -r cc4eb23d37b3 -r 0b1364481214 src/FOL/ex/cla.ML
--- a/src/FOL/ex/cla.ML	Fri Feb 14 10:35:42 1997 +0100
+++ b/src/FOL/ex/cla.ML	Fri Feb 14 10:36:33 1997 +0100
@@ -518,6 +518,12 @@
 \  ~ (EX X. a(X) & (ALL Y. c(Y) --> (ALL Z. d(X, Y, Z))))";
 
 
+(* Challenge found on info-hol *)
+goal FOL.thy
+    "ALL x. EX v w. ALL y z. P(x) & Q(y) --> (P(v) | R(w)) & (R(z) --> Q(v))";
+by (Deepen_tac 0 1);
+result();
+
 writeln"Reached end of file.";
 
 (*Thu Jul 23 1992: loaded in 467s using iffE [on SPARC2] *)