# HG changeset patch
# User nipkow
# Date 1238681899 -7200
# Node ID 3fb9345721e4ac49536173cdacb7a92f0e79a148
# Parent  8b8d86cc2437197f3410681b5b2f04af4afe64f0
Updated to corrected E output messages

diff -r 8b8d86cc2437 -r 3fb9345721e4 src/HOL/Tools/res_reconstruct.ML
--- a/src/HOL/Tools/res_reconstruct.ML	Thu Apr 02 15:08:38 2009 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML	Thu Apr 02 16:18:19 2009 +0200
@@ -459,7 +459,7 @@
     
   (* ==== CHECK IF PROOF OF E OR VAMPIRE WAS SUCCESSFUL === *)
   
-  val failure_strings_E = ["SZS status: Satisfiable","SZS status: ResourceOut","# Cannot determine problem status"];
+  val failure_strings_E = ["SZS status: Satisfiable","SZS status Satisfiable","SZS status: ResourceOut","SZS status ResourceOut","# Cannot determine problem status"];
   val failure_strings_vampire = ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"];
   val failure_strings_SPASS = ["SPASS beiseite: Completion found.","SPASS beiseite: Ran out of time.",
   "SPASS beiseite: Maximal number of loops exceeded."];