equal
deleted
inserted
replaced
358 val spass_new_config : atp_config = |
358 val spass_new_config : atp_config = |
359 {exec = ("SPASS_NEW_HOME", "SPASS"), |
359 {exec = ("SPASS_NEW_HOME", "SPASS"), |
360 required_execs = [], |
360 required_execs = [], |
361 arguments = fn _ => fn _ => fn incomplete => fn timeout => fn _ => |
361 arguments = fn _ => fn _ => fn incomplete => fn timeout => fn _ => |
362 (* TODO: add: -FPDFGProof -FPFCR *) |
362 (* TODO: add: -FPDFGProof -FPFCR *) |
363 ("-Auto -Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout)) |
363 ("-Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout)) |
364 (* TODO: not used yet *) |
364 (* TODO: not used yet *) |
365 |> incomplete = spass_incompleteN ? prefix "-Splits=0 -FullRed=0 ", |
365 |> incomplete = spass_incompleteN ? prefix "-Splits=0 -FullRed=0 ", |
366 proof_delims = #proof_delims spass_config, |
366 proof_delims = #proof_delims spass_config, |
367 known_failures = #known_failures spass_config, |
367 known_failures = #known_failures spass_config, |
368 conj_sym_kind = #conj_sym_kind spass_config, |
368 conj_sym_kind = #conj_sym_kind spass_config, |