--- a/src/Doc/Sledgehammer/document/root.tex Thu Jul 15 22:51:49 2021 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Fri Jul 16 15:27:55 2021 +0200
@@ -803,9 +803,6 @@
\item[\labelitemi] \textbf{\textit{remote\_leo3}:} The remote version of Leo-III
runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
-\item[\labelitemi] \textbf{\textit{remote\_vampire}:} The remote version of
-Vampire runs on Geoff Sutcliffe's Miami servers.
-
\item[\labelitemi] \textbf{\textit{remote\_waldmeister}:} Waldmeister is a unit
equality prover developed by Hillenbrand et al.\ \cite{waldmeister}. It can be
used to prove universally quantified equations using unconditional equations,