adjust fudge factors in the light of experiments
authorblanchet
Mon, 23 Aug 2010 21:11:30 +0200
changeset 38685 87a1e97a3ef3
parent 38684 e2c04af9469b
child 38686 45eeee8d6b12
adjust fudge factors in the light of experiments
src/HOL/Tools/ATP/atp_systems.ML
--- 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}