TAOCP 7.2.2.2 Exercise 150
At depth $d=1$, the current assignment is the one obtained after the first branch $x_5=0$.
Section 7.2.2.2: Satisfiability
Exercise 150. [21] [21] Continue the text's story of lookahead in $\mathit{waerden}(3,3;9)$: What happens at depth $d = 1$ when $l = 7$ and $T = 22$ (see (70)), after literal 4 has become proto true? (Assume that no double-lookahead is done.)
Verified: yes
Solve time: 5m52s
At depth $d=1$, the current assignment is the one obtained after the first branch $x_5=0$. The resulting binary clauses are
$$ (1\vee3),\ (1\vee9),\ (2\vee8),\ (3\vee4),\ (3\vee7),\ (4\vee6),\ (6\vee7),\ (7\vee9). $$
The lookahead branch chooses $l=7$. During this lookahead, literal $4$ eventually becomes proto true. Since double-lookahead is not being performed, we only continue the ordinary lookahead propagation from this new proto-true literal.
The assumption $7$ makes every clause containing $\bar 7$ active. In particular,
$$ (\bar1\vee\bar4\vee\bar7) $$
becomes the binary clause
$$ (\bar1\vee\bar4). $$
Once $4$ is proto true, this binary clause forces
$$ \bar1 $$
to become proto true. Now the ternary clauses of $\mathit{waerden}(3,3;9)$ continue the propagation.
The clause
$$ (1\vee5\vee9) $$
together with $x_5=0$ and $\bar1$ forces
$$ 9. $$
Similarly,
$$ (1\vee3\vee5) $$
forces
$$ 3. $$
With $3$ and $4$ true, the negative arithmetic-progression clause
$$ (\bar2\vee\bar3\vee\bar4) $$
forces
$$ \bar2. $$
Then the clause
$$ (2\vee5\vee8) $$
forces
$$ 8. $$
Finally, the clause
$$ (\bar3\vee\bar6\vee\bar9) $$
forces
$$ \bar6. $$
At this point the clause
$$ (\bar7\vee\bar8\vee\bar9) $$
has all three literals false, because the lookahead already has
$$ 7,\qquad 8,\qquad 9 $$
true. Hence it produces a contradiction.
Therefore the ordinary lookahead at $d=1$, after $l=7$ and after literal $4$ has become proto true, detects a conflict:
$$ 7\Longrightarrow4\Longrightarrow\bar1\Longrightarrow9,3 \Longrightarrow\bar2\Longrightarrow8\Longrightarrow\bar6 $$
and this contradicts the clause $(\bar7\vee\bar8\vee\bar9)$. Since no double-lookahead is done, the contradiction is found only through this single propagation chain.