% This exercises redundancy proofs by clausal rewriting.
% Saturation terminates even without any special treatment
% of transitivity.
%
predicates( [p] ).


:-option([special_relations(off),crw_depth(3)]).

axiom( [ [], [p(X,X)] ] ).
axiom( [ [], [p(X,Y), p(Y,X)] ] ).
axiom( [ [p(X,Y), p(Y,Z)], [p(X,Z)] ] ).
axiom( [ [p(X,Y), p(Y,X)], [X=Y] ] ).

precedence( [] ).
first_predicate_precedence( [p] ).

:-sarp(all).
:-sama([]).