first order logic to normal form order of operations ∃y∀x [A(x) ∧ B(y) -&gt; 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?
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)]
&gt;&gt;
∀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())]
&gt;&gt;
¬A(x) v ¬B(S()) v C(x,S()).