equal
deleted
inserted
replaced
351 (* iProver *) |
351 (* iProver *) |
352 |
352 |
353 val iprover_config : atp_config = |
353 val iprover_config : atp_config = |
354 {exec = (["IPROVER_HOME"], ["iprover"]), |
354 {exec = (["IPROVER_HOME"], ["iprover"]), |
355 arguments = fn _ => fn _ => fn _ => fn timeout => fn _ => |
355 arguments = fn _ => fn _ => fn _ => fn timeout => fn _ => |
356 "--clausifier $IPROVER_HOME/vclausify_rel --time_out_real " ^ |
356 "--clausifier \"$IPROVER_HOME\"/vclausify_rel --time_out_real " ^ |
357 string_of_real (Time.toReal timeout), |
357 string_of_real (Time.toReal timeout), |
358 proof_delims = tstp_proof_delims, |
358 proof_delims = tstp_proof_delims, |
359 known_failures = |
359 known_failures = |
360 [(ProofIncomplete, "% SZS output start CNFRefutation")] @ |
360 [(ProofIncomplete, "% SZS output start CNFRefutation")] @ |
361 known_szs_status_failures, |
361 known_szs_status_failures, |