The formulas of this submission reduce to the 2-SAT of $lax-429075$ by renaming: the variable of every literal is replaced by the position of the first occurrence of that variable, so that the unary code of $lax-429075$ stays polynomial in the binary code of this submission, and renaming along an injection preserves satisfiability in both directions. A word that is not the code of a formula is sent to the code of a formula with one empty clause, which is unsatisfiable. The reduction is a word RAM program on the zeros and ones of its input, in the same way as the reductions of the theorems, and transfers to a Turing machine; 2-SAT of $lax-429075$ is in polynomial time by the algorithm of this submission, and polynomial time is closed under polynomial-time reductions.