src/HOL/Tools/ATP/atp_systems.ML
changeset 47899 493d70c63fd6
parent 47898 6213900d6d5f
child 47900 6440a74b2f62
equal deleted inserted replaced
47898:6213900d6d5f 47899:493d70c63fd6
   335    known_failures =
   335    known_failures =
   336      known_szs_status_failures @
   336      known_szs_status_failures @
   337      [(TimedOut, "CPU time limit exceeded, terminating"),
   337      [(TimedOut, "CPU time limit exceeded, terminating"),
   338       (GaveUp, "No.of.Axioms")],
   338       (GaveUp, "No.of.Axioms")],
   339    conj_sym_kind = Axiom,
   339    conj_sym_kind = Axiom,
   340    prem_kind = Definition (* motivated by "isabelle tptp_sledgehammer" tool *),
   340    prem_kind = Hypothesis,
   341    best_slices = fn ctxt =>
   341    best_slices = fn ctxt =>
   342      (* FUDGE *)
   342      (* FUDGE *)
   343      [(0.667, (false, ((150, leo2_thf0, "mono_native_higher", keep_lamsN, false), sosN))),
   343      [(0.667, (false, ((150, leo2_thf0, "mono_native_higher", keep_lamsN, false), sosN))),
   344       (0.333, (true, ((50, leo2_thf0, "mono_native_higher", keep_lamsN, false), no_sosN)))]
   344       (0.333, (true, ((50, leo2_thf0, "mono_native_higher", keep_lamsN, false), no_sosN)))]
   345      |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
   345      |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single