doc-src/Sledgehammer/sledgehammer.tex

 \texttt{Z3\_SOLVER} to the complete path of the executable, including the file
 name. Sledgehammer has been tested with versions 2.7 to 2.18.
 
 \item[$\bullet$] \textbf{\textit{z3\_atp}:} This version of Z3 pretends to be an
 ATP, exploiting Z3's undocumented support for the TPTP format. It is included
-for experimental purposes. It requires versions 2.18 or above.
+for experimental purposes. It requires version 2.18 or above.
 
 \item[$\bullet$] \textbf{\textit{remote\_e}:} The remote version of E runs
 on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
 
 \item[$\bullet$] \textbf{\textit{remote\_vampire}:} The remote version of