--- 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);