# Converting first-order formula to CNF

I need to convert this statement to CNF (Conjunctive normal form):

$\qquad \left((\forall x.\, P(x)) \implies Q(a)\right)\implies \left((\exists y.\, P(y)) \implies Q(a)\right)$

\qquad \begin{align} &\left((\forall x.\, P(x)) \lor (\forall y.\, \neg P(y))\right) \\ \land &\left((\forall x.\, P(x)) \lor Q(a) \right)\\ \land &\left(\neg Q(a) \lor (\forall y.\, \neg P(y))\right) \end{align}
It is not clear whether $\forall x$ resp $\forall y$ binds only $P(\_)$ or the respective implications $P(\_) \implies Q(a)$. Please check whether we got it right. – Raphael Feb 2 at 21:15