133 |
133 |
134 val vampire_config : prover_config = |
134 val vampire_config : prover_config = |
135 {executable = ("VAMPIRE_HOME", "vampire"), |
135 {executable = ("VAMPIRE_HOME", "vampire"), |
136 required_executables = [], |
136 required_executables = [], |
137 arguments = fn _ => fn timeout => |
137 arguments = fn _ => fn timeout => |
138 "--output_syntax tptp --mode casc -t " ^ |
138 "--mode casc -t " ^ string_of_int (to_generous_secs timeout) ^ |
139 string_of_int (to_generous_secs timeout), |
139 " --input_file ", |
140 proof_delims = |
140 proof_delims = |
141 [("=========== Refutation ==========", |
141 [("=========== Refutation ==========", |
142 "======= End of refutation ======="), |
142 "======= End of refutation ======="), |
143 ("% SZS output start Refutation", "% SZS output end Refutation")], |
143 ("% SZS output start Refutation", "% SZS output end Refutation"), |
|
144 ("% SZS output start Proof", "% SZS output end Proof")], |
144 known_failures = |
145 known_failures = |
145 [(Unprovable, "UNPROVABLE"), |
146 [(Unprovable, "UNPROVABLE"), |
146 (IncompleteUnprovable, "CANNOT PROVE"), |
147 (IncompleteUnprovable, "CANNOT PROVE"), |
147 (Unprovable, "Satisfiability detected"), |
148 (Unprovable, "Satisfiability detected"), |
148 (OutOfResources, "Refutation not found")], |
149 (OutOfResources, "Refutation not found")], |