The performance of automated theorem provers can be improved by the
introduction of strategy parallelism in combination with automated resource
allocation. This is of particular importance if the theorem prover is to be
integrated into a larger proof environment or if the prover is to be applied
to a new problem domain, where the configuration of the theorem prover must be
done automatically.  Therefore we have developed a method for strategy
evaluation and selection based on test data generated from the problem domain.
We present the theorem prover e-SETHEO which automatically handles training
data management, strategy evaluation and selection, and actual proof tasks.
We also give some experimental data produced with this system.  We address the
problem of test set extraction and give an assessment of our work.