src/Doc/Sledgehammer/document/root.tex

 \item[\labelitemi] If you prefer to build agsyHOL, Alt-Ergo, E, LEO-II,
 Satallax, or SPASS manually, or found a Vampire executable somewhere (e.g.,
 \url{http://www.vprover.org/}), set the environment variable
 \texttt{AGSYHOL\_HOME}, \texttt{E\_HOME}, \texttt{LEO2\_HOME},
 \texttt{SATALLAX\_HOME}, \texttt{SPASS\_HOME}, or
-\texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{eproof},
+\texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{agsyHOL},
+\texttt{eprover} (and/or \texttt{eproof} or \texttt{eproof\_ram}),
 \texttt{leo}, \texttt{satallax}, \texttt{SPASS}, or \texttt{vampire} executable;
 for Alt-Ergo, set the
 environment variable \texttt{WHY3\_HOME} to the directory that contains the
 \texttt{why3} executable.
-Sledgehammer has been tested with agsyHOL 1.0, Alt-Ergo 0.95.1, E 1.0 to 1.4,
-LEO-II 1.3.4, Satallax 2.2, 2.3, and 2.4, SPASS 3.8ds, and Vampire 0.6 to 2.6.%
+Sledgehammer has been tested with agsyHOL 1.0, Alt-Ergo 0.95.1, E 1.0 to 1.8,
+LEO-II 1.3.4, Satallax 2.2 to 2.7, SPASS 3.8ds, and Vampire 0.6 to 2.6.%
 \footnote{Following the rewrite of Vampire, the counter for version numbers was
 reset to 0; hence the (new) Vampire versions 0.6, 1.0, 1.8, and 2.6 are more
 recent than 9.0 or 11.5.}%
 Since the ATPs' output formats are neither documented nor stable, other
 versions might not work well with Sledgehammer. Ideally,
 you should also set \texttt{E\_VERSION}, \texttt{LEO2\_VERSION},
 \texttt{SATALLAX\_VERSION}, \texttt{SPASS\_VERSION}, or
-\texttt{VAMPIRE\_VERSION} to the prover's version number (e.g., ``1.4'').
+\texttt{VAMPIRE\_VERSION} to the prover's version number (e.g., ``1.8'').
 
 Similarly, if you want to build CVC3, or found a
 Yices or Z3 executable somewhere (e.g.,
 \url{http://yices.csl.sri.com/download.shtml} or
 \url{http://research.microsoft.com/en-us/um/redmond/projects/z3/download.html}),

 \download. Sledgehammer has been tested with version 2.2 and 2.4.1.
 
 \item[\labelitemi] \textbf{\textit{e}:} E is a first-order resolution prover
 developed by Stephan Schulz \cite{schulz-2002}. To use E, set the environment
 variable \texttt{E\_HOME} to the directory that contains the \texttt{eproof}
-executable and \texttt{E\_VERSION} to the version number (e.g., ``1.4''), or
+executable and \texttt{E\_VERSION} to the version number (e.g., ``1.8''), or
 install the prebuilt E package from \download. Sledgehammer has been tested with
-versions 1.0 to 1.6.
+versions 1.0 to 1.8.
 
 \item[\labelitemi] \textbf{\textit{e\_males}:} E-MaLeS is a metaprover developed
 by Daniel K\"uhlwein that implements strategy scheduling on top of E. To use
 E-MaLeS, set the environment variable \texttt{E\_MALES\_HOME} to the directory
 that contains the \texttt{emales.py} script. Sledgehammer has been tested with

 
 \item[\labelitemi] \textbf{\textit{leo2}:} LEO-II is an automatic
 higher-order prover developed by Christoph Benzm\"uller et al.\ \cite{leo2},
 with support for the TPTP typed higher-order syntax (THF0). To use LEO-II, set
 the environment variable \texttt{LEO2\_HOME} to the directory that contains the
-\texttt{leo} executable. Sledgehammer requires version 1.2.9 or above.
+\texttt{leo} executable. Sledgehammer requires version 1.3.4 or above.
 
 \item[\labelitemi] \textbf{\textit{metis}:} Although it is less powerful than
 the external provers, Metis itself can be used for proof search.
 
 \item[\labelitemi] \textbf{\textit{satallax}:} Satallax is an automatic