first order logic to normal form order of operations
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()).