# HG changeset patch
# User blanchet
# Date 1572005162 -7200
# Node ID 1019b860955274b8fbb5ba24123230af549c9f05
# Parent  9b69bb9c1c8d140bc416667b9be733f10f3838bb
removed support for remote Satallax because its output does not clearly identify the lemmas used

diff -r 9b69bb9c1c8d -r 1019b8609552 src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Fri Oct 25 13:25:30 2019 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Fri Oct 25 14:06:02 2019 +0200
@@ -893,9 +893,6 @@
 highly experimental first-order resolution prover developed by Daniel Wand.
 The remote version of Pirate run on a private server he generously set up.
 
-\item[\labelitemi] \textbf{\textit{remote\_satallax}:} The remote version of
-Satallax runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
-
 \item[\labelitemi] \textbf{\textit{remote\_snark}:} SNARK is a first-order
 resolution prover developed by Stickel et al.\ \cite{snark}. It supports the
 TPTP typed first-order format (TFF0). The remote version of SNARK runs on
diff -r 9b69bb9c1c8d -r 1019b8609552 src/HOL/Tools/ATP/atp_satallax.ML
--- a/src/HOL/Tools/ATP/atp_satallax.ML	Fri Oct 25 13:25:30 2019 +0200
+++ b/src/HOL/Tools/ATP/atp_satallax.ML	Fri Oct 25 14:06:02 2019 +0200
@@ -124,6 +124,7 @@
     else
       raise Fail ("the rule " ^ rule ^" is not supported in the reconstruction")
   end
+
 fun to_satallax_step (((id, role), formula), (SOME (_,((rule, l), used_rules)))) =
     let
       val (used_assumptions, new_goals, generated_assumptions) = seperate_dependices used_rules
@@ -220,7 +221,7 @@
           Linear_Part {node = node, succs = []}
         else
           let
-            (*one singel goal is created, two hypothesis can be created, for the "and" rule:
+            (*one single goal is created, two hypothesis can be created, for the "and" rule:
               (A /\ B) create two hypotheses A, and B.*)
             fun set_hypotheses_as_goal [hypothesis] succs =
                 Linear_Part {node = add_detailled_eigen detailed_eigen
@@ -361,7 +362,7 @@
       let
         val role' = role_of_tptp_string role
         val new_transformed = filter
-          (fn s => size s >=4 andalso not (is_special_satallax_rule s) andalso not
+          (fn s => size s >= 4 andalso not (is_special_satallax_rule s) andalso not
           (member (op =) already_transformed s)) used_assumptions
       in
         (map create_fact_step new_transformed
diff -r 9b69bb9c1c8d -r 1019b8609552 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Fri Oct 25 13:25:30 2019 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Fri Oct 25 14:06:02 2019 +0200
@@ -783,9 +783,6 @@
 val remote_leo3 =
   remotify_atp leo3 "Leo-III" ["1.1"]
     (K (((150, ""), leo3_thf1, "poly_native_higher", keep_lamsN, false), "") (* FUDGE *))
-val remote_satallax =
-  remotify_atp satallax "Satallax" ["2.7", "2.3", "2"]
-    (K (((150, ""), satallax_thf0, "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
 val remote_vampire =
   remotify_atp vampire "Vampire" ["4.2", "4.1", "4.0"]
     (K (((400, ""), vampire_tff0, "mono_native", combs_or_liftingN, false), remote_vampire_full_proof_command) (* FUDGE *))
@@ -839,8 +836,7 @@
   [agsyhol, alt_ergo, e, e_males, e_par, ehoh, iprover, iprover_eq, leo2, leo3, satallax, spass,
    vampire, z3_tptp, zipperposition, dummy_thf, dummy_thf_ml, remote_agsyhol, remote_e,
    remote_e_sine, remote_e_tofof, remote_iprover, remote_iprover_eq, remote_leo2, remote_leo3,
-   remote_satallax, remote_vampire, remote_snark, remote_pirate, remote_waldmeister,
-   remote_waldmeister_new]
+   remote_vampire, remote_snark, remote_pirate, remote_waldmeister, remote_waldmeister_new]
 
 val _ = Theory.setup (fold add_atp atps)