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; the three numbers and the pairs are written directly; for each clause the elements of its literals are marked and counted in one pass over the positions, and a sweep of the marks writes them in increasing order. Polynomial time on the word RAM transfers to a Turing machine, and the machine writing the word of the instance is one writing the instance.