diff -r 5c8a0580d513 -r 14de47e29fe4 src/Doc/Sledgehammer/document/root.tex
--- 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,