--- a/src/Sequents/LK/Hard_Quantifiers.thy	Tue Oct 02 19:02:47 2018 +0200
+++ b/src/Sequents/LK/Hard_Quantifiers.thy	Tue Oct 02 19:10:04 2018 +0200
@@ -248,8 +248,8 @@
 text "Problem 59"
 (*Unification works poorly here -- the abstraction %sobj prevents efficient
   operation of the occurs check*)
-
 lemma "\<turnstile> (\<forall>x. P(x) \<longleftrightarrow> \<not> P(f(x))) \<longrightarrow> (\<exists>x. P(x) \<and> \<not> P(f(x)))"
+  using [[unify_trace_bound = 50]]
   by best_dup
 
 text "Problem 60"