# HG changeset patch
# User blanchet
# Date 1282547077 -7200
# Node ID 5500241da479f08685697ca4796c3a4a3f0e79a3
# Parent  8fe717f5048e586cb4918748f81692e1ad17c284
play with fudge factor + parse one more Vampire error

diff -r 8fe717f5048e -r 5500241da479 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Mon Aug 23 00:09:25 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon Aug 23 09:04:37 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 = 50 (* FUDGE *),
+   default_max_relevant_per_iter = 60 (* FUDGE *),
    default_theory_relevant = false,
    explicit_forall = false,
    use_conjecture_for_hypotheses = true}
@@ -203,6 +203,7 @@
       (IncompleteUnprovable, "CANNOT PROVE"),
       (TimedOut, "SZS status Timeout"),
       (Unprovable, "Satisfiability detected"),
+      (Unprovable, "Termination reason: Satisfiable"),
       (VampireTooOld, "not a valid option")],
    default_max_relevant_per_iter = 45 (* FUDGE *),
    default_theory_relevant = false,