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 ⊼ 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[(# ⊼ #) ⊼ (# ⊼ p_{t}) & , p ⊼ (p ⊼ 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.