# HG changeset patch
# User blanchet
# Date 1282590690 -7200
# Node ID 87a1e97a3ef307f896087667c4da401a0df67d0f
# Parent  e2c04af9469bda4a363f115a4c0f79ea3710c99e
adjust fudge factors in the light of experiments

diff -r e2c04af9469b -r 87a1e97a3ef3 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}