equal
deleted
inserted
replaced
360 "-p hocore -t " ^ string_of_int (to_secs 1 timeout), |
360 "-p hocore -t " ^ string_of_int (to_secs 1 timeout), |
361 proof_delims = |
361 proof_delims = |
362 [("% Higher-Order Unsat Core BEGIN", "% Higher-Order Unsat Core END")], |
362 [("% Higher-Order Unsat Core BEGIN", "% Higher-Order Unsat Core END")], |
363 known_failures = known_szs_status_failures, |
363 known_failures = known_szs_status_failures, |
364 conj_sym_kind = Axiom, |
364 conj_sym_kind = Axiom, |
365 prem_kind = Hypothesis, |
365 prem_kind = Definition (* motivated by "isabelle tptp_sledgehammer" tool *), |
366 best_slices = |
366 best_slices = |
367 (* FUDGE *) |
367 (* FUDGE *) |
368 K [(1.0, (true, ((100, satallax_thf0, "mono_native_higher", keep_lamsN, false), "")))]} |
368 K [(1.0, (true, ((100, satallax_thf0, "mono_native_higher", keep_lamsN, false), "")))]} |
369 |
369 |
370 val satallax = (satallaxN, fn () => satallax_config) |
370 val satallax = (satallaxN, fn () => satallax_config) |