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

Question

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).


%some random votes
votes(p1, p6).
votes(p2, p6).
votes(p3, p6).
votes(p4, p7).
votes(p5, p8).
votes(p6, p5).

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

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

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