# HG changeset patch # User blanchet # Date 1281344745 -7200 # Node ID 601b7972eef296f6b73f9f9300a6c6ef1d107d33 # Parent 577f138af235bb418027699cf85b61c6a07bf2df fiddle some more with "max_new_relevant_facts_per_iter" diff -r 577f138af235 -r 601b7972eef2 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Mon Aug 09 11:03:54 2010 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Mon Aug 09 11:05:45 2010 +0200 @@ -140,7 +140,7 @@ "# Cannot determine problem status within resource limit"), (OutOfResources, "SZS status: ResourceOut"), (OutOfResources, "SZS status ResourceOut")], - max_new_relevant_facts_per_iter = 90 (* FIXME *), + max_new_relevant_facts_per_iter = 60 (* FIXME *), prefers_theory_relevant = false, explicit_forall = false} val e = ("e", e_config)