% The formula below is a theorem of the equivalential calculus.
% We can show that it is not a single axiom, because e(x,x) does not
% follow.

assign(domain_size, 4).

% set(verbose).

clauses(theory).

-P(e(x,y)) | -P(x) | P(y).           % condensed detachment

P(e(e(x,y),e(e(y,z),e(z,x)))).

-P(e(a,a)).

end_of_list.