The program reads the word, scans it with the verified scanner of $lax-391470$, checks the width of every clause, builds the implication graph in compressed sparse row form by a counting sort, and searches from both literals of every occurring variable; the searches are paid out of a potential that charges a constant to every variable and two searches to every occurring one, which gives the factor $v + 1$. The constant is $8000$.