--- a/src/HOL/Tools/ATP/atp_systems.ML Mon Aug 23 18:53:11 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Mon Aug 23 21:11:30 2010 +0200
@@ -149,7 +149,7 @@
"# Cannot determine problem status within resource limit"),
(OutOfResources, "SZS status: ResourceOut"),
(OutOfResources, "SZS status ResourceOut")],
- default_max_relevant_per_iter = 60 (* FUDGE *),
+ default_max_relevant_per_iter = 80 (* FUDGE *),
default_theory_relevant = false,
explicit_forall = false,
use_conjecture_for_hypotheses = true}
@@ -176,7 +176,7 @@
(MalformedInput, "Undefined symbol"),
(MalformedInput, "Free Variable"),
(SpassTooOld, "tptp2dfg")],
- default_max_relevant_per_iter = 32 (* FUDGE *),
+ default_max_relevant_per_iter = 40 (* FUDGE *),
default_theory_relevant = true,
explicit_forall = true,
use_conjecture_for_hypotheses = true}