src/HOL/Tools/ATP_Manager/atp_systems.ML
changeset 37331 942435c34341
parent 37171 fc1e20373e6a
child 37346 cdba266f0383
equal deleted inserted replaced
37330:a7a150650d40 37331:942435c34341
   273      [("=========== Refutation ==========",
   273      [("=========== Refutation ==========",
   274        "======= End of refutation ======="),
   274        "======= End of refutation ======="),
   275       ("% SZS output start Refutation", "% SZS output end Refutation")],
   275       ("% SZS output start Refutation", "% SZS output end Refutation")],
   276    known_failures =
   276    known_failures =
   277      [(Unprovable, "Satisfiability detected"),
   277      [(Unprovable, "Satisfiability detected"),
       
   278       (Unprovable, "UNPROVABLE"),
   278       (OutOfResources, "CANNOT PROVE"),
   279       (OutOfResources, "CANNOT PROVE"),
   279       (OutOfResources, "Refutation not found")],
   280       (OutOfResources, "Refutation not found")],
   280    max_axiom_clauses = 60,
   281    max_axiom_clauses = 60,
   281    prefers_theory_relevant = false}
   282    prefers_theory_relevant = false}
   282 val vampire = tptp_prover "vampire" vampire_config
   283 val vampire = tptp_prover "vampire" vampire_config