src/Doc/Sledgehammer/document/root.tex

 \footnote{The distinction between ATPs and SMT solvers is convenient but mostly
 historical.}
 %
 The supported ATPs are AgsyHOL \cite{agsyHOL}, Alt-Ergo \cite{alt-ergo}, E
 \cite{schulz-2002}, E-SInE \cite{sine}, E-ToFoF \cite{tofof}, iProver
-\cite{korovin-2009}, iProver-Eq \cite{korovin-sticksel-2010}, LEO-II
-\cite{leo2}, Leo-III \cite{leo3}, Satallax \cite{satallax}, SNARK \cite{snark}, SPASS
-\cite{weidenbach-et-al-2009}, Vampire \cite{riazanov-voronkov-2002},
-Waldmeister \cite{waldmeister}, and Zipperposition \cite{cruanes-2014}.
-The ATPs are run either locally or remotely via the System\-On\-TPTP web service
-\cite{sutcliffe-2000}. The supported SMT solvers are CVC3 \cite{cvc3}, CVC4
-\cite{cvc4}, veriT \cite{bouton-et-al-2009}, and Z3 \cite{z3}. These are always
-run locally.
+\cite{korovin-2009}, LEO-II \cite{leo2}, Leo-III \cite{leo3}, Satallax
+\cite{satallax}, SNARK \cite{snark}, SPASS \cite{weidenbach-et-al-2009},
+Vampire \cite{riazanov-voronkov-2002}, Waldmeister \cite{waldmeister}, and
+Zipperposition \cite{cruanes-2014}. The ATPs are run either locally or
+remotely via the System\-On\-TPTP web service \cite{sutcliffe-2000}. The
+supported SMT solvers are CVC3 \cite{cvc3}, CVC4 \cite{cvc4}, veriT
+\cite{bouton-et-al-2009}, and Z3 \cite{z3}. These are always run locally.
 
 The problem passed to the external provers (or solvers) consists of your current
 goal together with a heuristic selection of hundreds of facts (theorems) from the
 current theory context, filtered by relevance.
 

 Sledgehammer is part of Isabelle, so you do not need to install it. However, it
 relies on third-party automatic provers (ATPs and SMT solvers).
 
 Among the ATPs, AgsyHOL, Alt-Ergo, E, LEO-II, Leo-III, Satallax, SPASS, Vampire, and
 Zipperposition can be run locally; in addition, AgsyHOL, E, E-SInE, E-ToFoF,
-iProver, iProver-Eq, LEO-II, Leo-III, Satallax, SNARK, Vampire, and Waldmeister are
+iProver, LEO-II, Leo-III, Satallax, SNARK, Vampire, and Waldmeister are
 available remotely via System\-On\-TPTP \cite{sutcliffe-2000}. The SMT solvers
 CVC3, CVC4, veriT, and Z3 can be run locally.
 
 There are three main ways to install automatic provers on your machine:
 

 \cite{korovin-2009}. To use iProver, set the environment variable
 \texttt{IPROVER\_HOME} to the directory that contains the \texttt{iproveropt}
 executable. Sledgehammer has been tested with version 2.8. iProver depends on
 E to clausify problems, so make sure that E is installed as well.
 
-\item[\labelitemi] \textbf{\textit{iprover\_eq}:} iProver-Eq is an
-instantiation-based prover with native support for equality developed by
-Konstantin Korovin and Christoph Sticksel \cite{korovin-sticksel-2010}. To use
-iProver-Eq, set the environment variable \texttt{IPROVER\_EQ\_HOME} to the
-directory that contains the \texttt{iprover-eq} and \texttt{vclausify\_rel}
-executables. Sledgehammer has been tested with version 0.8.
-
 \item[\labelitemi] \textbf{\textit{leo2}:} LEO-II is an automatic
 higher-order prover developed by Christoph Benzm\"uller et al.\ \cite{leo2},
 with support for the TPTP typed higher-order syntax (THF0). To use LEO-II, set
 the environment variable \texttt{LEO2\_HOME} to the directory that contains the
 \texttt{leo} executable. Sledgehammer requires version 1.3.4 or above.

 servers. This ATP supports the TPTP typed first-order format (TFF0). The
 remote version of E-ToFoF runs on Geoff Sutcliffe's Miami servers.
 
 \item[\labelitemi] \textbf{\textit{remote\_iprover}:} The
 remote version of iProver runs on Geoff Sutcliffe's Miami servers
-\cite{sutcliffe-2000}.
-
-\item[\labelitemi] \textbf{\textit{remote\_iprover\_eq}:} The
-remote version of iProver-Eq runs on Geoff Sutcliffe's Miami servers
 \cite{sutcliffe-2000}.
 
 \item[\labelitemi] \textbf{\textit{remote\_leo2}:} The remote version of LEO-II
 runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.