src/HOL/Tools/ATP/atp_systems.ML

--- a/src/HOL/Tools/ATP/atp_systems.ML	Mon Feb 14 18:28:36 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Feb 15 10:03:10 2011 +0100
@@ -164,7 +164,7 @@
        "# Cannot determine problem status within resource limit"),
       (OutOfResources, "SZS status: ResourceOut"),
       (OutOfResources, "SZS status ResourceOut")],
-   default_max_relevant = 500 (* FUDGE *),
+   default_max_relevant = 250 (* FUDGE *),
    explicit_forall = false,
    use_conjecture_for_hypotheses = true}
 
@@ -193,7 +193,7 @@
       (MalformedInput, "Free Variable"),
       (SpassTooOld, "tptp2dfg"),
       (InternalError, "Please report this error")],
-   default_max_relevant = 350 (* FUDGE *),
+   default_max_relevant = 150 (* FUDGE *),
    explicit_forall = true,
    use_conjecture_for_hypotheses = true}
 
@@ -224,7 +224,7 @@
       (Unprovable, "Termination reason: Satisfiable"),
       (VampireTooOld, "not a valid option"),
       (Interrupted, "Aborted by signal SIGINT")],
-   default_max_relevant = 400 (* FUDGE *),
+   default_max_relevant = 450 (* FUDGE *),
    explicit_forall = false,
    use_conjecture_for_hypotheses = true}
 
@@ -244,7 +244,7 @@
      [(Unprovable, "\nsat"),
       (IncompleteUnprovable, "\nunknown"),
       (ProofMissing, "\nunsat")],
-   default_max_relevant = 250 (* FUDGE *),
+   default_max_relevant = 225 (* FUDGE *),
    explicit_forall = true,
    use_conjecture_for_hypotheses = false}
 
@@ -319,10 +319,10 @@
   remote_atp z3_atpN "Z3---" ["2.18"] []
              [(IncompleteUnprovable, "SZS status Satisfiable"),
               (ProofMissing, "SZS status Unsatisfiable")]
-             250 (* FUDGE *) false
+             225 (* FUDGE *) false
 val remote_sine_e =
   remote_atp sine_eN "SInE" [] [] [(IncompleteUnprovable, "says Unknown")]
-             600 (* FUDGE *) true
+             500 (* FUDGE *) true
 val remote_snark =
   remote_atp snarkN "SNARK---" [] [("refutation.", "end_refutation.")] []
              250 (* FUDGE *) true