equal
deleted
inserted
replaced
335 arguments = |
335 arguments = |
336 fn _ => fn _ => fn _ => fn timeout => fn _ => |
336 fn _ => fn _ => fn _ => fn timeout => fn _ => |
337 "--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout), |
337 "--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout), |
338 proof_delims = tstp_proof_delims, |
338 proof_delims = tstp_proof_delims, |
339 known_failures = |
339 known_failures = |
340 [(* LEO 1.3.3 does not record definitions properly, leading to missing |
340 [(TimedOut, "CPU time limit exceeded, terminating"), |
341 dependencies in the TSTP proof. Remove the next line once this is |
|
342 fixed. *) |
|
343 (ProofIncomplete, "_def,definition,"), |
|
344 (TimedOut, "CPU time limit exceeded, terminating"), |
|
345 (GaveUp, "No.of.Axioms")] @ |
341 (GaveUp, "No.of.Axioms")] @ |
346 known_szs_status_failures, |
342 known_szs_status_failures, |
347 prem_kind = Hypothesis, |
343 prem_kind = Hypothesis, |
348 best_slices = |
344 best_slices = |
349 (* FUDGE *) |
345 (* FUDGE *) |