--- 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}