Vampire is an automatic theorem prover for first-order logic. During proof search in given-clause algorithms, Vampire repeatedly selects clauses from either an age or a weight queue in a fixed, but configurable age/weight ratio (AWR). We show that an optimal fixed value of this ratio can produce proofs significantly more quickly on a given problem, and further that varying AWR during proof search can improve upon a fixed ratio. Based on these observations we develop several new modes for Vampire which vary AWR according to a “shape” during proof search. The modes solve a number of new problems in the TPTP benchmark.
Old or Heavy? Decaying Gracefully with Age/Weight Shapes.