"Anyone who has cats as pets will not have mice": $$\forall x[\exists zHave(x,cat(z))]\rightarrow \forall y[\neg Have(x,mouse(y))]$$
I need to translate this into conjunctive normal form. So the first thing I do is eliminate the $\rightarrow$:
$$\forall x [\neg \exists z Have(x,cat(z))] \vee \forall y[\neg Have(x,mouse(y))]$$
Then we apply the negation:
$$\forall x[\forall z \neg Have(x,cat(z))] \vee \forall y[\neg Have(x,mouse(y))]$$
Then apply the Skolem function & drop universal quantifiers (?):
$$\neg Have(x,F(x)) \vee \neg Have(x, G(y))$$
So this last sentence is in conjunctive normal form, but I'm not sure if it means the same thing as the original sentence. The last sentence may read as "$x$ has a cat or $x$ has a mouse." Is this the same thing as "Anyone who has cats as pets will not have mice?" Are my steps correct?