# HG changeset patch
# User blanchet
# Date 1306224195 -7200
# Node ID 10baeee358a50cffd83d6c023371e3b42c9988ec
# Parent  74415622d2933549c5bf9bc78d03d4f4b4d1e3d4
pass fewer relevant facts to less used remote systems

diff -r 74415622d293 -r 10baeee358a5 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue May 24 10:01:03 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue May 24 10:03:15 2011 +0200
@@ -417,10 +417,10 @@
 val remote_z3_atp = remotify_atp z3_atp "Z3" ["2.18"]
 val remote_leo2 =
   remote_atp leo2N "LEO-II" ["1.2.6"] [] [] Axiom Hypothesis [THF]
-             (K (200, ["simple"]) (* FUDGE *))
+             (K (150, ["simple"]) (* FUDGE *))
 val remote_satallax =
   remote_atp satallaxN "Satallax" ["2.0"] [] [] Axiom Hypothesis [THF]
-             (K (200, ["simple"]) (* FUDGE *))
+             (K (150, ["simple"]) (* FUDGE *))
 val remote_sine_e =
   remote_atp sine_eN "SInE" ["0.4"] [] (#known_failures e_config)
              Axiom Conjecture [FOF]
@@ -431,7 +431,7 @@
              [TFF, FOF] (K (250, ["simple"]) (* FUDGE *))
 val remote_tofof_e =
   remote_atp tofof_eN "ToFoF" ["0.1"] [] (#known_failures e_config)
-             Axiom Hypothesis [TFF] (K (200, ["simple"]) (* FUDGE *))
+             Axiom Hypothesis [TFF] (K (150, ["simple"]) (* FUDGE *))
 val remote_waldmeister =
   remote_atp waldmeisterN "Waldmeister" ["710"]
              [("#START OF PROOF", "Proved Goals:")]