equal
deleted
inserted
replaced
317 (* iProver *) |
317 (* iProver *) |
318 |
318 |
319 val iprover_config : atp_config = |
319 val iprover_config : atp_config = |
320 {exec = (["IPROVER_HOME"], ["iproveropt", "iprover"]), |
320 {exec = (["IPROVER_HOME"], ["iproveropt", "iprover"]), |
321 arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => fn _ => |
321 arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => fn _ => |
322 ["--clausifier \"$E_HOME\"/eprover " ^ |
322 ["--clausifier \"$VAMPIRE_HOME\"/vampire " ^ |
323 "--clausifier_options \"--tstp-format --silent --cnf\" " ^ |
323 "--clausifier_options \"--mode clausify\" " ^ |
324 "--time_out_real " ^ string_of_real (Time.toReal timeout) ^ " " ^ File.bash_path problem], |
324 "--time_out_real " ^ string_of_real (Time.toReal timeout) ^ " " ^ File.bash_path problem], |
325 proof_delims = tstp_proof_delims, |
325 proof_delims = tstp_proof_delims, |
326 known_failures = |
326 known_failures = |
327 [(ProofIncomplete, "% SZS output start CNFRefutation")] @ |
327 [(ProofIncomplete, "% SZS output start CNFRefutation")] @ |
328 known_szs_status_failures, |
328 known_szs_status_failures, |