NAND tautologies

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] p_{t}) & , 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.