# HG changeset patch # User blanchet # Date 1306068664 -7200 # Node ID 47f366f1fe32649d93262a9dc4c48ce9eb0728ea # Parent f838586ebec29cc48fc7d367f57d0ad0e72f3420 recognize one more SystemOnTPTP error diff -r f838586ebec2 -r 47f366f1fe32 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Sun May 22 14:51:04 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Sun May 22 14:51:04 2011 +0200 @@ -380,7 +380,8 @@ proof_delims = insert (op =) tstp_proof_delims proof_delims, known_failures = known_failures @ known_perl_failures @ - [(IncompleteUnprovable, "says Unknown"), + [(Unprovable, "says Satisfiable"), + (IncompleteUnprovable, "says Unknown"), (IncompleteUnprovable, "says GaveUp"), (TimedOut, "says Timeout")], conj_sym_kind = conj_sym_kind,