Solution (source code)

= Solution

\b[Take $\varphi_1=p$ for an $A$ win and $\varphi_2=p\land\neg p$ for a $B$ win.] In the first case $A$ assigns $p$ true and play terminates immediately. In the second, either value of $p$ completes an assignment making the <contradiction> false, so $B$ wins regardless of $A$'s move. These examples force termination and do not rely on a stalling convention.

For the subsequent parts, adopt the explicit convention that an infinite play is a draw, with <payoff> $0$, between an $A$ win at $+1$ and a $B$ win at $-1$. The source does not assign a value to nontermination. Different conventions can change values of cyclic positions; the forced finite wins above remain valid.