Tableau formulas have polynomial-size polynomial-time CNF encodings

Put $a=\mathrm{\mid }A\mathrm{\mid }$, a constant of the fixed verifier. There are $a(T+1)(T+2)$ cell variables. Each cell contributes one size-$a$ clause and at most $a(a-1)\mathrm{/}2$ binary clauses. Each update contributes at most $a^4$ clauses of width at most four. The pinning clauses number $O(T^2)$ and the accepting clause has at most $a(T+2)$ literals. Thus the literal count is $O(T^2)$; indices take $O(\log (T+2))$ bits. Enumerate times, cells and the constant symbol tuples with binary counters, and output each clause. Counter arithmetic, the initial input lookup and evaluation of the fixed polynomials cost polynomial time. The binary list headers add only linear overhead in the number of entries.

For completeness, the gate clauses can be written explicitly. For $v=\mathrm{\neg }u$ use $(v\vee u)\wedge (\mathrm{\neg }v\vee \mathrm{\neg }u)$. For $v=u\wedge w$ use $(\mathrm{\neg }v\vee u)\wedge (\mathrm{\neg }v\vee w)\wedge (v\vee \mathrm{\neg }u\vee \mathrm{\neg }w)$. For $v=u\vee w$ use $(v\vee \mathrm{\neg }u)\wedge (v\vee \mathrm{\neg }w)\wedge (\mathrm{\neg }v\vee u\vee w)$. The two possible values of $v$ show that each conjunction holds exactly for the indicated equality: for AND, $v=1$ forces both inputs true and $v=0$ forces at least one false; OR is dual, and NOT forces opposite bits. Constants are pinned by a positive or negative unit clause. Finite list connectives are first expanded as binary trees, using the appropriate constant for an empty list. Finally require the output wire by a unit clause.

Assign gate values in order after a satisfying assignment to the original variables. Each equality clause and the output unit then holds. Conversely any satisfying CNF assignment obeys every gate equality; induction through the acyclic gate order identifies each gate bit with its evaluated value. The output unit makes the original formula true. These arguments also handle an output that is a lone literal or a constant. No assignment to fresh variables is asserted to work unless it obeys the gate equations.

Number the original distinct variables first and new gate variables next, retaining an explicit renaming list; alternatively take new indices above the largest original index. Their bit length is bounded by the input length plus $O(\log (g+2))$ for $g$ gates. There are $O(g)$ clauses after binary expansion, and they can be written by finite scans in polynomial time. Thus the conversion preserves satisfiability in both directions and the tableau's accepting-computation meaning. Zero gates, an empty CNF and an empty clause are handled respectively by the literal output, true constant and false constant rules.