--- a/src/Doc/Sledgehammer/document/root.tex Sun Jan 19 23:02:00 2014 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex Mon Jan 20 10:07:07 2014 +0100
@@ -923,10 +923,6 @@
\item[\labelitemi] \textbf{\textit{remote\_agsyhol}:} The remote version of
agsyHOL runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
-\item[\labelitemi] \textbf{\textit{remote\_cvc3}:} The remote version of CVC3 runs
-on servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to
-point).
-
\item[\labelitemi] \textbf{\textit{remote\_e}:} The remote version of E runs
on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
@@ -971,10 +967,6 @@
used to prove universally quantified equations using unconditional equations,
corresponding to the TPTP CNF UEQ division. The remote version of Waldmeister
runs on Geoff Sutcliffe's Miami servers.
-
-\item[\labelitemi] \textbf{\textit{remote\_z3}:} The remote version of Z3 runs on
-servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to
-point).
\end{enum}
By default, Sledgehammer runs a selection of CVC3, E, E-SInE, SPASS, Vampire,