# HG changeset patch
# User blanchet
# Date 1276528361 -7200
# Node ID 521bc1d1044503ed27eb2c88ea969af273833623
# Parent  d0cea0796295a3844106c56e58168e9bda3cea02
better error reporting for Vampire

diff -r d0cea0796295 -r 521bc1d10445 src/HOL/Tools/ATP_Manager/atp_systems.ML
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Mon Jun 14 16:43:44 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Mon Jun 14 17:12:41 2010 +0200
@@ -276,9 +276,9 @@
        "======= End of refutation ======="),
       ("% SZS output start Refutation", "% SZS output end Refutation")],
    known_failures =
-     [(Unprovable, "Satisfiability detected"),
-      (Unprovable, "UNPROVABLE"),
-      (Unprovable, "CANNOT PROVE"),
+     [(Unprovable, "UNPROVABLE"),
+      (IncompleteUnprovable, "CANNOT PROVE"),
+      (Unprovable, "Satisfiability detected"),
       (OutOfResources, "Refutation not found")],
    max_axiom_clauses = 60,
    prefers_theory_relevant = false}