Let n count all declared variables and u count those absent from every retained non-tautological clause. Variables appearing only in discarded tautologies also count toward u. Compute the clause-network contraction modulo 2^(n+1), then multiply it by 2^u modulo the same modulus. Each unused variable independently permits two values. The least nonnegative residue is the exact formula count, between zero and 2^n. For (x OR y) with declared variables x,y,z, contraction is three; multiplication by two gives six. An empty formula has empty-network contraction one and gives 2^n. No modular division is required.