How do we translate first order logic's universal quantifier (the $\forall$) and the existential quantifier (the $\exists$) to Prolog?

I'm trying to convert some English statements to first order logic statements and I'm trying to use Prolog to verify the translations. My question is: how do I convert a first order logic statement (having $$\forall$$ and $$\exists$$ quantifiers) into Prolog rules?

For example, there's this English statement:

Every voter votes for a candidate which some voter doesn't vote for.

and here's my translation of the English statement into first order logic:

$$\forall x, y[Voter(x) \land Candidate(y) \land Votes(x, y) \rightarrow \exists z[ Voter(z) \land \lnot Votes(z, y) ] ]$$

Now I'm not sure if this translation is correct. That's what I want to find out. My question is: how do I convert this first order logic statement to a Prolog rule?

So first I'm trying to fill a Prolog database with some facts.

human(p1).
human(p2).
human(p3).
human(p4).
human(p5).
human(p6).
human(p7).
human(p8).
human(p9).
%humans who are neither voters nor candidates
human(p10).
human(p11).

%humans who are only voters
voter(p1).
voter(p2).
voter(p3).

%humans who are candidates and voters
voter(p4).
voter(p5).
voter(p6).
candidate(p4).
candidate(p5).
candidate(p6).

%humans who are only candidates
candidate(p7).
candidate(p8).
candidate(p9).

I'm using human, voter, candidate, and votes. Here are some attempts to model the statement into a Prolog rule:

rule1 :-

rule2 :-
foreach((human(X), voter(X), candidate(Y), votes(X, Y)),(human(Z), voter(Z), \+votes(Z, Y))).

Prolog does not support arbitrary first-order logic but only a fragment of it known as Horn clauses. These are statements of the form $$\forall x_1, \ldots, x_n \,.\, P(x_1, \ldots, x_n) \Rightarrow q(x_1, \ldots, x_n)$$ where $$P$$ is built from atomic predicates and conjunctions, and $$q$$ is an atomic predicate. Not every statement in logic can be converted to this form.