X<Y, Y<Z -> X<Z.
X<X -> [].
X<Y, Y<X, X=Y.
X<Y -> X=<Y.
X=<Y -> X<Y,X=Y.
X=<X.

p(s(X))=X.
s(p(X))=X.

% consequences, but apparently not redundant for certain incomplete
% strategies
s(X)=s(Y) -> X=Y.
p(X)=p(Y) -> X=Y.

X<s(X).

% discreteness
X<Y -> s(X)=<Y.



precedence([=<,<,s,p,0]).

option(var_overlaps(off)).  % they are redundant in this case