# HG changeset patch
# User blanchet
# Date 1306485007 -7200
# Node ID 0db96016bdbfd3bba047e6b416e2e8e16aa802f0
# Parent  1c80902d04567fb617a17906898ba2d7f2b0b44b
recognize more ATP failures

diff -r 1c80902d0456 -r 0db96016bdbf src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Fri May 27 10:30:07 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Fri May 27 10:30:07 2011 +0200
@@ -387,7 +387,9 @@
    proof_delims = union (op =) tstp_proof_delims proof_delims,
    known_failures = known_failures @ known_perl_failures @
      [(Unprovable, "says Satisfiable"),
+      (Unprovable, "says CounterSatisfiable"),
       (ProofMissing, "says Theorem"),
+      (ProofMissing, "says Unsatisfiable"),
       (IncompleteUnprovable, "says Unknown"),
       (IncompleteUnprovable, "says GaveUp"),
       (TimedOut, "says Timeout"),