  To achieve the best performance, automatic theorem provers often rely on
schedules of diverse proving strategies to be tried out (either sequentially or
in parallel) on a given problem. In this paper, we report on a large-scale
experiment with discovering strategies for the Vampire prover, targeting the
FOF fragment of the TPTP library and constructing a schedule for it, based on
the ideas of Andrei Voronkov's system Spider. We examine the process from
various angles, discuss the difficulty (or ease) of obtaining a strong Vampire
schedule for the CASC competition, and establish how well a schedule can be
expected to generalize to unseen problems and what factors influence this
property.
