--- a/src/Doc/Sledgehammer/document/root.tex Wed Apr 08 18:55:52 2015 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Wed Apr 08 18:58:28 2015 +0200
@@ -259,27 +259,22 @@
\prew
\slshape
-Sledgehammer: ``\textit{e\/}'' \\
+Sledgehammer: ``\textit{cvc4\/}'' \\
Try this: \textbf{by} (\textit{metis last\_ConsL}) (64 ms). \\[3\smallskipamount]
%
Sledgehammer: ``\textit{z3\/}'' \\
Try this: \textbf{by} (\textit{metis list.inject}) (20 ms). \\[3\smallskipamount]
%
-Sledgehammer: ``\textit{vampire\/}'' \\
+Sledgehammer: ``\textit{remote\_vampire\/}'' \\
Try this: \textbf{by} (\textit{metis hd.simps}) (14 ms). \\[3\smallskipamount]
%
Sledgehammer: ``\textit{spass\/}'' \\
Try this: \textbf{by} (\textit{metis list.inject}) (17 ms). \\[3\smallskipamount]
-%
-Sledgehammer: ``\textit{remote\_e\_sine\/}'' \\
-Try this: \textbf{by} (\textit{metis hd.simps}) (18 ms).
\postw
-Sledgehammer ran E, E-SInE, SPASS, Vampire, 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.
-Waldmeister is run only for unit equational problems, where the goal's
-conclusion is a (universally quantified) equation.
+Sledgehammer ran CVC4, SPASS, Vampire, 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.
For each successful prover, Sledgehammer gives a one-line \textit{metis} or
\textit{smt2} method call. Rough timings are shown in parentheses, indicating how