A two-step computation tableau and its local clauses

Let $a_0=(q_0,0)$, $a_1=(q_1,\bigsqcup )$, $a_2=(q_{\mathrm{a}\mathrm{c}\mathrm{c}},0)$ and $B=\bigsqcup$. Set $X_{0,0,a_0}=X_{1,1,a_1}=X_{2,0,a_2}=1$, $X_{1,0,0}=1$, and select $B$ in all other cells. In every cell the positive symbol disjunction has one true term, and every pairwise exclusion has at least one true negated term. All initial units and the three right-guard units $X_{t,3,B}$ are 1. The final accepting disjunction has its $(j,a)=(0,0)$ term true.

The outputs required by the local rule at cells 0 through 3 for the first transition are $0,a_1,B,B$, and for the second are $a_2,B,B,B$. At cell zero the first tuple is $(\mathrm{\#},a_0,B,0)$; at cell one it is $(a_0,B,B,a_1)$. In the second transition the corresponding tuples are $(\mathrm{\#},0,a_1,a_2)$ and $(0,a_1,B,B)$. Here $\mathrm{\#}$ denotes the fixed exterior marker and contributes no Boolean literal. These four tuples follow the two table entries; cells two and three remain unmarked blanks because no head moves into them. Every forbidden-tuple clause therefore has at least one selected-symbol premise false, or its forbidden output false, and evaluates to 1.

Change just the first successor cell zero from unmarked 0 to unmarked 1, retaining one-hot encoding. The tuple $(\mathrm{\#},a_0,B,1)$ is forbidden, and its explicit clause $\mathrm{\neg }{X}_{0,0,a_0}\vee \mathrm{\neg }{X}_{0,1,B}\vee \mathrm{\neg }{X}_{1,0,1}$ now has values $0\vee 0\vee 0=0$. Thus the correct assignment satisfies every clause whereas this altered assignment fails an actual local clause. F2 identifies the satisfying tableau with the stated two-step accepting run; for any larger allowed bound simply repeat its last row and add blank columns.