The reduction is a word RAM program on the zeros and ones of its input: a finite-state scan decodes the formula into arrays of literal indices, signs and clause numbers; one pass tabulates where each clause ends; the chain clauses are then written clause by clause and the cycle clauses position by position, each with its padding and its three gadgets, in the encoding's unary code. Polynomial time on the word RAM transfers to a Turing machine.