--- a/src/Doc/Sledgehammer/document/root.tex Tue Dec 17 11:12:10 2013 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex Tue Dec 17 14:03:29 2013 +0100
@@ -960,6 +960,11 @@
TPTP typed first-order format (TFF0). The remote version of SNARK runs on
Geoff Sutcliffe's Miami servers.
+\item[\labelitemi] \textbf{\textit{remote\_spass\_pirate}:} SPASS-Pirate is a
+highly experimental first-order resolution prover developed by Daniel Wand.
+The remote version of SPASS-Pirate run on a private server set up by Daniel
+Wand.
+
\item[\labelitemi] \textbf{\textit{remote\_vampire}:} The remote version of
Vampire runs on Geoff Sutcliffe's Miami servers.