Solution (source code)

= Solution

\b[Depth $N$; at most $2^N N!$ complete plays; $3^N$ partial-assignment states; and $\sum_{k=0}^N2^kN!/(N-k)!$ <tree> nodes.] Here “different games” means complete move histories for the fixed <propositional formula>, rather than different syntactic formulas or merely different terminal <Boolean valuations>.

At depth $k$, the players have chosen an ordered list of $k$ distinct <variables> and a truth value for each, giving
$$
L_k=\frac{N!}{(N-k)!}\,2^k.
$$
Thus complete histories number $L_N=2^N N!$: $N!$ <variable> orders and $2^N$ assignments. Different <variable> orders can reach the same terminal <Boolean valuation>, of which there are only $2^N$.

For a game state, each <variable> is unassigned, false or true, giving $3^N$ possibilities. Ownership and variable-assignment order are irrelevant in this version, and the next player is determined by the parity of the number already assigned. The full <game tree>, which keeps histories separate, has
$$
\boxed{\sum_{k=0}^N L_k=2^N N!\sum_{j=0}^N\frac1{2^j j!}<2^{N+1}N!.}
$$
The depth counts <edges>; there are $N+1$ levels. These bounds explore the full <tree> even when a formula's truth might be inferable from a partial assignment, since the stated stopping rule waits for all <variables>.