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.

翻译：为实现最佳性能，自动定理证明器通常依赖于多样化的证明策略调度，这些策略会在给定问题上依次或并行尝试。本文报告了一项大规模实验，旨在基于安德烈·沃龙科夫Spider系统的思想，为Vampire证明器发现针对TPTP库FOF片段的策略并构建相应调度。我们从多角度审视该过程，讨论为CASC竞赛获取强大Vampire调度器的难易程度，并确定调度器在未见问题上的泛化能力预期及其影响因素。