I'm trying to convert $\forall x \exists y(P(x, y) \rightarrow (\neg\exists z \exists yR(z, y) \wedge \neg\forall xS(x)))$ into PCNF, but am getting stuck at the end.
$\equiv \forall x \exists y(\neg P(x, y) \vee (\forall z \neg\exists yR(z, y) \wedge \forall x \neg S(x)))$
$\equiv \forall x \exists y(\neg P(x, y) \vee (\forall z \forall y \neg R(z, y) \wedge \forall x \neg S(x)))$
$\equiv \forall x \exists y(\neg P(x, y) \vee \forall z \forall y (\neg R(z, y) \wedge \neg S(x)))$
$\equiv \forall x \exists y(\forall z \forall y (\neg P(x, y) \vee \neg R(z, y) \wedge \neg S(x)))$
I applied the following rules:
$x \rightarrow y \equiv \neg x \vee y$
$\neg\exists xF \equiv \forall x \neg F$
$(\forall xF) \vee G \equiv \forall x(F \vee G)$
Namely I don't know how to resolve the outer $\exists Y$ with the inner $\forall Y$. Guessing I did something wrong in the intermediate steps. What am I missing?