--- a/src/HOL/Tools/ATP_Manager/SystemOnTPTP Wed Jul 28 15:53:52 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/SystemOnTPTP Wed Jul 28 16:13:34 2010 +0200
@@ -106,7 +106,7 @@
exit(-1);
} elsif (exists($Options{'x'}) &&
$Response->content =~
- /%\s*Result\s*:\s*Unsatisfiable.*\n%\s*Output\s*:\s*(CNF)?Refutation.*\n%/ &&
+ /%\s*Result\s*:\s*(Unsatisfiable|Theorem).*\n%\s*Output\s*:\s*(CNF)?Refutation.*\n%/ &&
$Response->content !~ /ERROR: Could not form TPTP format derivation/ )
{
# converted output: extract proof