equal
deleted
inserted
replaced
470 val satallax_thf0 = THF (Monomorphic, THF_Without_Choice) |
470 val satallax_thf0 = THF (Monomorphic, THF_Without_Choice) |
471 |
471 |
472 val satallax_config : atp_config = |
472 val satallax_config : atp_config = |
473 {exec = K (["SATALLAX_HOME"], ["satallax.opt", "satallax"]), |
473 {exec = K (["SATALLAX_HOME"], ["satallax.opt", "satallax"]), |
474 arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => |
474 arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => |
|
475 (case getenv "E_HOME" of |
|
476 "" => "" |
|
477 | home => "-E " ^ home ^ "/eprover ") ^ |
475 "-p tstp -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name, |
478 "-p tstp -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name, |
476 proof_delims = |
479 proof_delims = |
477 [("% SZS output start Proof", "% SZS output end Proof")], |
480 [("% SZS output start Proof", "% SZS output end Proof")], |
478 known_failures = known_szs_status_failures, |
481 known_failures = known_szs_status_failures, |
479 prem_role = Hypothesis, |
482 prem_role = Hypothesis, |