258 {home = getenv "VAMPIRE_HOME", |
258 {home = getenv "VAMPIRE_HOME", |
259 executable = "vampire", |
259 executable = "vampire", |
260 arguments = fn timeout => |
260 arguments = fn timeout => |
261 "--output_syntax tptp --mode casc -t " ^ |
261 "--output_syntax tptp --mode casc -t " ^ |
262 string_of_int (to_generous_secs timeout), |
262 string_of_int (to_generous_secs timeout), |
263 proof_delims = [("=========== Refutation ==========", |
263 proof_delims = |
264 "======= End of refutation =======")], |
264 [("=========== Refutation ==========", |
|
265 "======= End of refutation ======="), |
|
266 ("% SZS output start Refutation", "% SZS output end Refutation")], |
265 known_failures = |
267 known_failures = |
266 [(Unprovable, "Satisfiability detected"), |
268 [(Unprovable, "Satisfiability detected"), |
267 (OutOfResources, "CANNOT PROVE"), |
269 (OutOfResources, "CANNOT PROVE"), |
268 (OutOfResources, "Refutation not found")], |
270 (OutOfResources, "Refutation not found")], |
269 max_axiom_clauses = 60, |
271 max_axiom_clauses = 60, |
390 max_axiom_clauses = max_axiom_clauses, |
392 max_axiom_clauses = max_axiom_clauses, |
391 prefers_theory_relevant = prefers_theory_relevant} |
393 prefers_theory_relevant = prefers_theory_relevant} |
392 |
394 |
393 val remote_vampire = |
395 val remote_vampire = |
394 tptp_prover (remotify (fst vampire)) |
396 tptp_prover (remotify (fst vampire)) |
395 (remote_prover_config "Vampire---9" "" vampire_config) |
397 (remote_prover_config "Vampire---11" "" vampire_config) |
396 |
398 |
397 val remote_e = |
399 val remote_e = |
398 tptp_prover (remotify (fst e)) |
400 tptp_prover (remotify (fst e)) |
399 (remote_prover_config "EP---" "" e_config) |
401 (remote_prover_config "EP---" "" e_config) |
400 |
402 |