first order logic to normal form order of operations

Question

 ∃y∀x [A(x) ∧ B(y) -> C(x,y)]
 ∃y∀x [¬(A(x) ∧ B(y)) v C(x,y)]
 ∃y∀x [¬A(x) v ¬B(y) v C(x,y)]

I need to convert the above to conjunctive normal form. I'm a little confused about the order of operations in the case of both existential and universal quantifier and which part of the expression they apply to. From the last step, would I skolemize y across the entire expression meaning:

∀x [¬A(x) v ¬B(S(x)) v C(x,S(x)]

or do I take the universal quantifier first?

Answer 1

You always remove quantifiers in the order in which they appear in the prefix, from left to right, that is, you first eliminate $\exists y$ and then $\forall x$.

But the variables to apply the skolem function to are just the variables occurring free in the expression, no bound ones. Since $x$ is bound by $\forall x$, and $y$ is being skolemized away, the skolem function for $\exists y$ becomes a zero-place function symbol, or constant, S():

∃y∀x [¬A(x) v ¬B(y) v C(x,y)]
>>
∀x [¬A(x) v ¬B(S()) v C(x,S())]

In the next step, eliminate the the universal quantifier:

∀x [¬A(x) v ¬B(S()) v C(x,S())]
>>
¬A(x) v ¬B(S()) v C(x,S()).