Use unification and resolution to justify proof

Question

Prove:

If $\neg A(x)\lor B(y),\neg C(x)\lor G(w),\neg G(x)$, and $A(x)$, then $B(x)\land \neg C(w)$

Use resolution and unification to do your proof. Justify each step.

I'm not sure how to correctly use Unification to get the correct variables where I want them. Here's what I tried:

Premises:

$\neg A(x)\lor B(y)$

$\neg C(x)\lor G(w)$

$\neg G(x)$

$A(x)$

Conclusion:

$B(x)\land C(w)$

---

Proof:

1. $\neg B(x)\lor C(w)$ - Proof By Contradiction
2. $\neg A(x)\lor B(y)$ - Premise
3. $\neg A(x)\lor B(x)$ - Unification (Sub x in place of y) <--Can I do this?
4. $C(w)\lor \neg A(x)$ - Resolution; Lines 1,3
5. $\neg C(x)\lor G(w)$ - Premise
6. $\neg C(w)\lor G(w)$ - Unification (sub w in place of x) <--OK?
7. $\neg A(x)\lor G(w)$ - Resolution; Lines 4,6
8. $\neg G(x)$ - Premise
9. $\neg G(w)$ - Unification (sub w in place of x)
10. $\neg A(x)$ - Resolution; Lines 7,9
11. $A(x)$ - Premise
12. FALSE - Resolution; Lines 10,11

---

So essentially, I substituted variables wherever I wanted whenever I need them. Is that how Unification(/Instantiation) works?

Answer 1

You can use disjunctive syllogism to combine $\neg A(x)\lor B(y)$ with $A(x)$ to get $B(y)$.

Then combine $\neg C(x)\lor G(w)$ with $\neg G(x)$ to get $\neg C(x)$ the same way.

If you can then use unification to get the substitutions, you can finish up with an application of conjunction.