# HG changeset patch
# User blanchet
# Date 1336637261 -7200
# Node ID 6440a74b2f62773d0f3a6cef1d4e1e7e6e8e8bb7
# Parent  493d70c63fd66ef98d7db35c1786eef65e1f8bc9
pass fewer facts to LEO-II and Satallax

diff -r 493d70c63fd6 -r 6440a74b2f62 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Thu May 10 10:07:40 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu May 10 10:07:41 2012 +0200
@@ -340,7 +340,7 @@
    prem_kind = Hypothesis,
    best_slices = fn ctxt =>
      (* FUDGE *)
-     [(0.667, (false, ((150, leo2_thf0, "mono_native_higher", keep_lamsN, false), sosN))),
+     [(0.667, (false, ((100, leo2_thf0, "mono_native_higher", keep_lamsN, false), sosN))),
       (0.333, (true, ((50, leo2_thf0, "mono_native_higher", keep_lamsN, false), no_sosN)))]
      |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
          else I)}
@@ -365,7 +365,7 @@
    prem_kind = Definition (* motivated by "isabelle tptp_sledgehammer" tool *),
    best_slices =
      (* FUDGE *)
-     K [(1.0, (true, ((100, satallax_thf0, "mono_native_higher", keep_lamsN, false), "")))]}
+     K [(1.0, (true, ((75, satallax_thf0, "mono_native_higher", keep_lamsN, false), "")))]}
 
 val satallax = (satallaxN, fn () => satallax_config)