Old or Heavy? Decaying Gracefully with Age/Weight Shapes.

Modern saturation theorem provers are based on the given clause algorithm, which iteratively selects new clauses to process. This clause selection has a large impact on the performance of proof search and has been the subject of much folklore. The standard approach is to alternate between selecting the oldest clause and the lightest clause with a fixed, but congfiurable age/weight ratio (AWR). An optimal fixed value of this ratio is shown to produce proofs significantly more quickly on a given problem, and further that varying AWR during proof search can improve upon a fixed ratio. Several new modes for the Vampire prover which vary AWR according to a \shape" during proof search are developed based on these observations. The modes solve a number of new problems in the TPTP benchmark set.