Formulate the problem of checking whether a clause set is

Question

Formulate the problem of checking whether a clause set is renamable Horn as a 2SAT problem.

For each of the n variables x_j, let y_j be true when x_j is renamed. Since the number of clauses is quadratic in n, show how to add variables to make it linear in n.