# HG changeset patch
# User paulson
# Date 1192090989 -7200
# Node ID 4992239a414ecc5ad13f4eb2158bccdd1538c16a
# Parent  3bf6915081d943330c6285cac0f28017461598e5
failure messages

diff -r 3bf6915081d9 -r 4992239a414e src/HOL/Tools/res_reconstruct.ML
--- a/src/HOL/Tools/res_reconstruct.ML	Thu Oct 11 00:33:43 2007 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML	Thu Oct 11 10:23:09 2007 +0200
@@ -622,7 +622,8 @@
      if any_substring [start_V8,start_TSTP] thisLine
      then startTransfer end_V8 arg
      else if (String.isSubstring "Satisfiability detected" thisLine) orelse
-             (String.isSubstring "Refutation not found" thisLine)
+             (String.isSubstring "Refutation not found" thisLine) orelse
+             (String.isSubstring "CANNOT PROVE" thisLine)
      then (signal_parent (toParent, ppid, "Failure\n", probfile);
 	   true)
      else checkVampProofFound arg);
@@ -637,7 +638,8 @@
      else if String.isSubstring "SZS status: Satisfiable" thisLine
      then (signal_parent (toParent, ppid, "Invalid\n", probfile);
 	   true)
-     else if String.isSubstring "SZS status: ResourceOut" thisLine
+     else if String.isSubstring "SZS status: ResourceOut" thisLine orelse
+             String.isSubstring "# Cannot determine problem status" thisLine
      then (signal_parent (toParent, ppid, "Failure\n", probfile);
 	   true)
      else checkEProofFound arg);