The Method Vaughan Pratt The method represents a theory as the set of its satisfying valuations, those that make every formula in the theory true. Sets are represented as in Pascal, namely as bit vectors. There being 16 valuations of four variables (the default case n = 4), the bit vectors are of length 16, which in the program are typed as uint (unsigned int). Theories range from 1 to 65534, with 0 (the inconsistent theory) and 65535 (the tautology) being omitted. The theories being finitely generated and therefore finite, they can be represented as single propositions, namely their conjunction, equivalently their strongest member. Every theory (including 0 and the tautology) can be obtained as a Boolean combination of the variables p_0 through p_3, which themselves constitute theories, respectively 0xaaaa, 0xcccc, 0xf0f0, and 0xff00, denoted p[0] through p[3] in the implementation; as such these realize the generators of a free Boolean algebra under the usual bitwise Boolean operations. Boolean combinations of theories can therefore be expressed directly in the implementation using C's bitwise Boolean operators: x&y for conjunction, x|y for disjunction, ~x for complement, and x^y for exclusive-or. For n < 4 (i.e. when running the implementation for fewer than 4 variables), the unused p_i's are still there in this particular implementation but are simply not touched. The method linearly orders the theories via the standard ordering on uints interpreted as natural numbers. To each theory t is associated its reduct r[t], namely the (numerically) least theory currently known to be equivalent to t under interchange of variables and complementation of literals. Initially r[t] = t for all theories t. Whenever s and t are determined to be equivalent, they are "joined" by setting both r[s] and r[t] to min(r[s],r[t]) (by no means the asymptotically fastest implementation of JOIN, but more than adequate for the present purpose). The method is repeated until r stabilizes, at which point the answer is given by the number of t's that still satisfy r[t] = t, these being the normal-form theories, defined as the numerically least representatives of their respective equivalence classes. The method enumerates all consistent nontautological theories t. For each it considers variables p_i and p_j for 0 <= i < j <= 3 (6 pairs). It joins t with the theory obtained by complementing p_i, and with the theory obtained by interchanging p_i and p_j. These two theories are determined as per the following two paragraphs respectively. Complementing p_i has the effect of interchanging the set p[i] of valuations for which p_i = 1, i.e. the theory consisting of (the consequences of) the proposition p_i, with the complementary theory ~p[i] (strictly speaking, T&~p[i] where T is the tautological theory, but the extra bits from omitting T do no harm). This exchange effectively moves the former valuations down, and the latter up, by a distance of 2^i positions in the list of all 16 valuations. It follows that the resulting theory is given by the OR of ((t & p[i]) >> (1<