src/HOL/Tools/ATP_Manager/atp_systems.ML
changeset 37390 521bc1d10445
parent 37389 d0cea0796295
child 37455 d5a85d35ef62
     1.1 --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Mon Jun 14 16:43:44 2010 +0200
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Mon Jun 14 17:12:41 2010 +0200
     1.3 @@ -276,9 +276,9 @@
     1.4         "======= End of refutation ======="),
     1.5        ("% SZS output start Refutation", "% SZS output end Refutation")],
     1.6     known_failures =
     1.7 -     [(Unprovable, "Satisfiability detected"),
     1.8 -      (Unprovable, "UNPROVABLE"),
     1.9 -      (Unprovable, "CANNOT PROVE"),
    1.10 +     [(Unprovable, "UNPROVABLE"),
    1.11 +      (IncompleteUnprovable, "CANNOT PROVE"),
    1.12 +      (Unprovable, "Satisfiability detected"),
    1.13        (OutOfResources, "Refutation not found")],
    1.14     max_axiom_clauses = 60,
    1.15     prefers_theory_relevant = false}