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.

翻译：为了达到最佳性能，自动定理证明器通常依赖于多种证明策略的调度（按顺序或并行）来处理给定问题。本文基于Andrei Voronkov开发的Spider系统思想，报告了一项大规模实验：针对Vampire证明器发现策略，以TPTP库中的FOF片段为目标，并为其构建调度。我们从多个角度审视了这一过程，讨论了在CASC比赛中获得强大Vampire调度的难度（或容易程度），并确定了调度在多大程度上可推广至未见问题，以及影响该性质的关键因素。