I need to determine whether the following formula is satisfiable, using binary resolution:
$$\exists x \forall y \forall z ((P(y) \to Q(z)) \to (P(x) \to Q(x)))$$
I re-framed the problem to showing that the [above] formula's negation is unsatisfiable:
$\lnot\exists x \forall y \forall z ((P(y) \to Q(z)) \to (P(x) \to Q(x)))$ negation of the [original] formula
$\forall x \lnot ((P(g(x)) \to Q(h(x))) \to (P(x) \to Q(x)))$ skolemized: y = g(x) & z = h(x)
$\forall x ((\lnot P(g(x)) \lor Q(h(x))) \land P(x) \land (\lnot Q(x)))$ converted to CNF
Now, it is clear that I cannot derive an empty clause from the set of clauses $$\{[\lnot P(g(x)), Q(h(x))], \, [P(x)], \, [\lnot Q(x)] \}$$ Does this mean that the negation of the [original] formula is satisfiable?
But I'm unable to derive an empty clause even using the original formula:
$\exists x \forall y \forall z ((P(y) \to Q(z)) \to (P(x) \to Q(x)))$ original formula
$\forall y \forall z ((P(y) \to Q(z)) \to (P(a) \to Q(a)))$ skolemized: x = a
$\forall y \forall z ((P(y) \lor \lnot P(a) \lor Q(a)) \land (\lnot Q(z) \lor \lnot P(a) \lor Q(a))$ converted to CNF
Now, again clearly I cannot derive an empty clause from the set of clauses $$\{[P(y), \lnot P(a), Q(a)], \, [\lnot Q(z), \lnot P(a), Q(a)] \}$$ Does this mean that the satisfiability of the [original] formula cannot be determined?
In fact, the formula
$$\tag{1} \exists x \forall y \forall z \big( (P(y) \to Q(z)) \to (P(x) \to Q(x)) \big)$$
is valid, which means that every structure satisfies it. In particular, it is satisfiable.
This is because, by applying the resolution method to the negation of the formula $(1)$, it is possible to get the empty clause. Hence, the negation of $(1)$ is unsatisfiable, which amounts to say that $(1)$ is valid.
Your syntactical handling starting from the negation of $(1)$ is correct, eventually you get the clauses:
\begin{align} \{¬P(g(x)), Q(h(x))\} && \{P(x)\} && \{¬ Q(x)\} \end{align} and after renaming the free variables so that distinct clauses have no variables in common (all variables in a clause are implicitly universally quantified, hence renaming does not change satisfiability), you get
\begin{align} \tag{2} \{¬P(g(x)), Q(h(x))\} && \{P(y)\} && \{¬ Q(z)\} \end{align}
You can resolve the first two clauses on $(2)$ thanks to the MGU $\{y \leftarrow g(x)\}$, thus the resolvent is the clause
\begin{align} \tag{3} \{Q(h(x))\} \end{align}
You can resolve the clause $(3)$ with the third clause in $(2)$ thanks to the MGU $\{z \leftarrow h(x)\}$, and the resolvent is the empty clause $\square$. Since there is a way to derive the empty clause by repeating the resolution method, the negation of $(1)$ is unsatisfiable and hence $(1)$ is valid, in particular $(1)$ is satisfiable.
EDIT. Note that the formula $$\forall x \big((\lnot P(g(x))\lor Q(h(x)))\land P(x) \land \lnot Q(x) \big) $$ (the CNF you correctly wrote in the OP) is logically equivalent to $$\forall x (\lnot P(g(x))\lor Q(h(x))) \land \forall x P(x) \land \forall x\lnot Q(x)$$ which is the same as $$\forall x (\lnot P(g(x))\lor Q(h(x))) \land \forall y P(y) \land \forall z\lnot Q(z).$$
This the logical reason that explains why the clauses \begin{align} \{¬P(g(x)), Q(h(x))\} && \{P(x)\} && \{¬ Q(x)\} \end{align} can be rewritten as in $(2)$ above, after renaming the free variables so that distinct clauses have no variables in common.