395 val iprover_eq = (iprover_eqN, fn () => iprover_eq_config) |
395 val iprover_eq = (iprover_eqN, fn () => iprover_eq_config) |
396 |
396 |
397 |
397 |
398 (* LEO-II *) |
398 (* LEO-II *) |
399 |
399 |
400 (* LEO-II supports definitions, but it performs significantly better on our |
|
401 benchmarks when they are not used. *) |
|
402 val leo2_thf0 = THF (Monomorphic, THF_Without_Choice) |
400 val leo2_thf0 = THF (Monomorphic, THF_Without_Choice) |
403 |
401 |
404 val leo2_config : atp_config = |
402 val leo2_config : atp_config = |
405 {exec = K (["LEO2_HOME"], ["leo.opt", "leo"]), |
403 {exec = K (["LEO2_HOME"], ["leo.opt", "leo"]), |
406 arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => |
404 arguments = fn _ => fn full_proofs => fn _ => fn timeout => fn file_name => fn _ => |
407 "--foatp e --atp e=\"$E_HOME\"/eprover \ |
405 "--foatp e --atp e=\"$E_HOME\"/eprover \ |
408 \--atp epclextract=\"$E_HOME\"/epclextract \ |
406 \--atp epclextract=\"$E_HOME\"/epclextract \ |
409 \--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout) ^ " " ^ |
407 \--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout) ^ " " ^ |
410 file_name, |
408 (if full_proofs then "--notReplLeibnizEQ --notReplAndrewsEQ --notUseExtCnfCmbd " else "") ^ |
|
409 file_name, |
411 proof_delims = tstp_proof_delims, |
410 proof_delims = tstp_proof_delims, |
412 known_failures = |
411 known_failures = |
413 [(TimedOut, "CPU time limit exceeded, terminating"), |
412 [(TimedOut, "CPU time limit exceeded, terminating"), |
414 (GaveUp, "No.of.Axioms")] @ |
413 (GaveUp, "No.of.Axioms")] @ |
415 known_szs_status_failures, |
414 known_szs_status_failures, |