resolution - satisfiability of formula (edit: renaming clause variables) 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?
 A: 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.
