At each step every possible transformation rule in the axioms is applied wherever it can. New expressions are also created by replacing each possible variable with x ⊼ y, where x and y are new variables, and by setting every possible pair of variables equal in turn. The longest tautology at step t is
Nest[(# ⊼ #) ⊼ (# ⊼ pt) & , p ⊼ (p ⊼ p), t - 1]
whose LeafCount grows like 3t. The distribution of sizes of statements generated at each step is shown below.
Even with the same underlying axioms the tautologies are generated in a somewhat different order if one uses a different strategy—say one based on paramodulation (see page 1156). Pages 818 and 1175 discuss the sequence of all Nand theorems listed in order of increasing complexity.