Proving satisfiability using resolution and variable elimination
If $x_7$ is a pure literal, then this means that you can satisfy all clauses containing $x_7$ by setting it to true. Accordingly, we set $x_7,x_5,x_6,x_8$ to true, satisfying all clauses apart from $\lnot x_2 \lor \lnot x_3 \lor x_4$, which we can satisfy by setting $x_4$ to true (for example).
If you set $x_4,x_5,x_6,x_7,x_8$ to true, then the left-hand side of your original formula is satisfied (once you correct $x_1 \lor x_2$ to $x_1 \lor x_2 \lor x_6$ and $\lnot x_5 \lor \lnot x_6$ to $x_5 \lor \lnot x_6$), while the right-hand side is falsified, and so the entailment is false. (In contrast to your post, there is no &quot;formula&quot; there which can be satisfied or not.)