323 val leo2_config : atp_config = |
323 val leo2_config : atp_config = |
324 {exec = (["LEO2_HOME"], "leo"), |
324 {exec = (["LEO2_HOME"], "leo"), |
325 required_vars = [], |
325 required_vars = [], |
326 arguments = |
326 arguments = |
327 fn _ => fn _ => fn sos => fn timeout => fn _ => |
327 fn _ => fn _ => fn sos => fn timeout => fn _ => |
328 "--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout) |
328 "--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout), |
329 |> sos = sosN ? prefix "--sos ", |
|
330 proof_delims = tstp_proof_delims, |
329 proof_delims = tstp_proof_delims, |
331 known_failures = |
330 known_failures = |
332 known_szs_status_failures @ |
331 known_szs_status_failures @ |
333 [(TimedOut, "CPU time limit exceeded, terminating"), |
332 [(TimedOut, "CPU time limit exceeded, terminating"), |
334 (GaveUp, "No.of.Axioms")], |
333 (GaveUp, "No.of.Axioms")], |
335 prem_kind = Hypothesis, |
334 prem_kind = Hypothesis, |
336 best_slices = fn ctxt => |
335 best_slices = |
337 (* FUDGE *) |
336 (* FUDGE *) |
338 [(0.667, (false, ((100, leo2_thf0, "mono_native_higher", keep_lamsN, false), sosN))), |
337 K [(1.0, (true, ((20, leo2_thf0, "mono_native_higher", keep_lamsN, false), "")))]} |
339 (0.333, (true, ((50, leo2_thf0, "mono_native_higher", keep_lamsN, false), no_sosN)))] |
|
340 |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single |
|
341 else I)} |
|
342 |
338 |
343 val leo2 = (leo2N, fn () => leo2_config) |
339 val leo2 = (leo2N, fn () => leo2_config) |
344 |
340 |
345 |
341 |
346 (* Satallax *) |
342 (* Satallax *) |
357 [("% Higher-Order Unsat Core BEGIN", "% Higher-Order Unsat Core END")], |
353 [("% Higher-Order Unsat Core BEGIN", "% Higher-Order Unsat Core END")], |
358 known_failures = known_szs_status_failures, |
354 known_failures = known_szs_status_failures, |
359 prem_kind = Definition (* motivated by "isabelle tptp_sledgehammer" tool *), |
355 prem_kind = Definition (* motivated by "isabelle tptp_sledgehammer" tool *), |
360 best_slices = |
356 best_slices = |
361 (* FUDGE *) |
357 (* FUDGE *) |
362 K [(1.0, (true, ((75, satallax_thf0, "mono_native_higher", keep_lamsN, false), "")))]} |
358 K [(1.0, (true, ((120, satallax_thf0, "mono_native_higher", keep_lamsN, false), "")))]} |
363 |
359 |
364 val satallax = (satallaxN, fn () => satallax_config) |
360 val satallax = (satallaxN, fn () => satallax_config) |
365 |
361 |
366 |
362 |
367 (* SPASS *) |
363 (* SPASS *) |