\begin{verbatim}

%This program is to test if
% sat iff \exists X \forall Y p(X,Y)
% is properly encoded below or not.

 univ(a).
 univ(b).
 univ(c).

 p(a,b).
 p(a,c).
 p(a,a).
 p(b,a).

 t(X)   :-
    univ(X),
    univ(Y),
    not p(X,Y).

 r(X)   :-
    univ(X),
    not t(X).

 sat    :-
    univ(X),
    r(X).

\end{verbatim}