"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?
Ok, I decided to convert the comments into an answer. The sentence in English is "Anyone who has cats as pets will not have mice". This naturally translates as $$\forall x (\exists y(Cat(y) \land Have(x,y))\rightarrow \neg \exists z (Mouse(z) \land Have(x,z)))$$ remove $\rightarrow$
$$\forall x (\neg\exists y(Cat(y) \land Have(x,y))\lor \neg \exists z (Mouse(z) \land Have(x,z)))$$
move negations in
$$\forall x (\forall y(\neg Cat(y) \lor \neg Have(x,y))\lor \forall z (\neg Mouse(z) \lor \neg Have(x,z)))$$
Pull out quantifiers
$$\forall x,y,z (\neg Cat(y) \lor \neg Have(x,y) \lor \neg Mouse(z) \lor \neg Have(x,z))$$
Skolem function things (trivial step as there are no existentials). Drop universals
$$\neg Cat(y) \lor \neg Have(x,y) \lor \neg Mouse(z) \lor \neg Have(x,z)$$