∃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?