# HG changeset patch # User blanchet # Date 1275663250 -7200 # Node ID 942435c3434124fc608d83b6a70d91fabc5204a0 # Parent a7a150650d40bd844f556c86b00cb057db9d8017 recongize one more outcome string for "remote_vampire" diff -r a7a150650d40 -r 942435c34341 src/HOL/Tools/ATP_Manager/atp_systems.ML --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Fri Jun 04 16:53:08 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Fri Jun 04 16:54:10 2010 +0200 @@ -275,6 +275,7 @@ ("% SZS output start Refutation", "% SZS output end Refutation")], known_failures = [(Unprovable, "Satisfiability detected"), + (Unprovable, "UNPROVABLE"), (OutOfResources, "CANNOT PROVE"), (OutOfResources, "Refutation not found")], max_axiom_clauses = 60,