First$-$Order Logic

Use resolution to check whether the goal $$G$$ below can be proved or not. To do so$,$ show:

$($a$)$ how to construct all necessary clauses,

$($b$)$ the application $($all the steps$)$ of the proof method,

$($c$)$ which most general unifiers are used $($in case a proof can be found$).$

G : $$x$.$ P$($x$)$

$1$ : $($z$.$ R$($z$))->($w$.$ T$($w$))$

$2$ : $$x $$y$.(($z$.($P$($x$)$R$($z$)))($w$.($T$($w$)->$ Q$($y$))))$

$3$ : $$w $$y$.(($x$.($P$($x$)->$T$($w$)))($x$.($Q$($y$)->$P$($x$))))$