src/Doc/Sledgehammer/document/root.tex

 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
 version 1.1.
 
-\item[\labelitemi] \textbf{\textit{e\_par}:} E-Par is a metaprover developed
-by Josef Urban that implements strategy scheduling on top of E. To use
-E-Par, set the environment variable \texttt{E\_HOME} to the directory
-that contains the \texttt{runepar.pl} script and the \texttt{eprover} and
+\item[\labelitemi] \textbf{\textit{e\_par}:} E-Par is an experimental metaprover
+developed by Josef Urban that implements strategy scheduling on top of E. To use
+E-Par, set the environment variable \texttt{E\_HOME} to the directory that
+contains the \texttt{runepar.pl} script and the \texttt{eprover} and
 \texttt{epclextract} executables, or use the prebuilt E package from \download.
+Be aware that E-Par is experimental software. It has been known to generate
+zombie processes. Use at your own risks.
 
 \item[\labelitemi] \textbf{\textit{iprover}:} iProver is a pure
 instantiation-based prover developed by Konstantin Korovin \cite{korovin-2009}.
 To use iProver, set the environment variable \texttt{IPROVER\_HOME} to the
 directory that contains the \texttt{iprover} and \texttt{vclausify\_rel}