of the variable blocks of each clause graph. Otherwise let $B$ contain the false vertices. In each case, let $A$ contain the mates of these vertices. Consider the constraint graph that is an induced subgraph of each clause graph. The vertices $X_1$, $X_2$ and $X_3$ have been assigned to either $A$ or $B$ with at most two, representing false literals, belonging to $A$. By Lemma \[lem:constraint-graph\], we can assign the remaining vertices of the subgraph (which are all true vertices of clause blocks) to $A$ and $B$ such that on the subgraph they form a near-bipartite decomposition. When we assign a true vertex of a clause block to $A$ or $B$, we assign all other true vertices in the same row of $H_\phi$ to the same set and assign their mates to the other set. As each row of the clause blocks contains only one vertex in a constraint graph, this process assigns every vertex in $H_\phi$ to exactly one of $A$ and $B$, and we have assigned every vertex of $H_\phi$ to $A$ or $B$.

It is immediately clear that $A$ is an independent set. We must show that $B$ contains no cycles. We know that $B$ contains all 