NAND theorems

The total number of expressions with n NANDs and s variables is: Binomial[2n, n]s^(n+1)/(n+1) (see page 897). With s=2 and n from 0 to 7 the number of these True for all values of variables is {0, 0, 4, 0, 80, 108, 2592, 7296}, with the first few distinct ones being (see page 781)

{(p \[Nand] p) \[Nand] p, (((p \[Nand] p) \[Nand] p) \[Nand] p) \[Nand] p, (((p \[Nand] p) \[Nand] p) \[Nand] q) \[Nand] q}

The number of unequal expressions obtained is {2, 3, 3, 7, 10, 15, 12, 16} (compare page 1096), with the first few distinct ones being

{p, p \[Nand] p, p \[Nand] q, (p \[Nand] p) \[Nand] p, (p \[Nand] q) \[Nand] p, (p \[Nand] p) \[Nand] q}

Most of the axioms from page 808 are too long to appear early in the list of theorems. But those of system (d) appear at positions {3, 15, 568} and those of (e) at {855, 4}.

(See also page 1096.)