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 the Vampire prover, schedules were for a long time constructed by Andrei Voronkov using a tool called Spider, about which little was officially known until recently. After Andrei Voronkov's talk at the Vampire Workshop 2023, we decided to analyse this powerful technology on our own.

In this paper, we report on a large-scale experiment with discovering Vampire strategies targeting the FOF fragment of the TPTP library and constructing a schedule for it, based on the ideas of Spider. We examine the process from various angles, discuss the difficulty (or ease) of obtaining a strong Vampire schedule for the CASC competition, but also estimate how well can a schedule be expected to generalize to unseen problems and what factors influence this property.