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 \[Nand] 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[(# \[Nand] #) \[Nand] (# \[Nand] pt) & , p \[Nand] (p \[Nand] p), t - 1]]
whose LeafCount grows like 3^t. 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.