--- 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,