src/Doc/Sledgehammer/document/root.tex

 %
 ``\textit{cvc4\/}'': Try this: \textbf{by} \textit{simp} (0.4 ms) \\
 %
 ``\textit{z3\/}'': Try this: \textbf{by} \textit{simp} (0.5 ms) \\
 %
-``\textit{spass\/}'': Try this: \textbf{by} \textit{simp} (0.3 ms)
+``\textit{vampire\/}'': Try this: \textbf{by} \textit{simp} (0.3 ms)
 %
 \postw
 
-Sledgehammer ran CVC4, E, SPASS, and Z3 in parallel. Depending on which
-provers are installed and how many processor cores are available, some of the
-provers might be missing or present with a \textit{remote\_} prefix.
+Sledgehammer ran CVC4, E, Vampire, and Z3 in parallel. This list may vary
+depending on which provers are installed and how many processor cores are
+available.
 
 For each successful prover, Sledgehammer gives a one-line Isabelle proof. Rough
 timings are shown in parentheses, indicating how fast the call is. You can
 click the proof to insert it into the theory text.