% benchmark parameters -n4

% The formulas below are theorems of the equivalential calculus.
% We can show that neither is a single axiom, because e(x,x) does not
% follow.

list(usable).

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

% P(e(e(x,y),e(e(y,z),e(x,z)))).     % easier
P(e(e(x,y),e(e(y,z),e(z,x)))).     % a bit harder

-P(e(a,a)).

% The following can speed up finding models for CD problems.
% It says that the all values for which P is false come before
% any of the values for which P is true.
% But it can be incomplete if you use -c or if you DON'T use
% -z 0.  In this case it works, because a gets assigned 0,
% and there is a model in which P(a) is false.

-P(x) | -(x < y) | P(y).

end_of_list.

