ABSTRACT. Automated theorem provers are often used in other tools as black-boxes for discharging proof obligations. One example where this has enjoyed a lot of success is within interactive theorem proving. A key usability factor in such settings is the time taken for the provers to complete. Automated theorem provers run lists of proof strategies sequentially, which can cause proofs to be found more slowly than necessary. We show that it is possible to predict which strategies are likely to succeed while they are running using an artificial neural network. We also implement a run-time strategy scheduler in the Vampire theorem prover which improves average proof search time, and hence increases usability as a black-box solver.