%	in(f(S1,S2),S1),S1=S2,in(f(S1,S2),S2).

l1(S1,S2),l2(S1,S2),l3(S1,S2) -> [].
in(f(S1,S2),S1),l1(S1,S2).
eq(S1,S2),l2(S1,S2).
in(f(S1,S2),S2),l3(S1,S2).


%	in(f(S1,S2),S1),in(f(S1,S2),S2) -> S1=S2.

l4(S1,S2),l5(S1,S2),l2(S1,S2).
in(f(S1,S2),S1) -> l4(S1,S2).
in(f(S1,S2),S2) -> l5(S1,S2).


%	in(X,empty) -> [].
l6(X) -> [].
in(X,empty) -> l6(X).



%	in(X1,add(S,X2)) = if X1=X2 then true else in(X1,S)
%  i.e.,
%       -in(X1,add(S,X2)), X1=X2, (-X1=X2 & in(X1,S))
%       in(X1,add(S,X2)), (-X1=X2 & -in(X1,S))


l7(X1,X2,S),l2(X1,X2),l8(X1,X2,S) -> [].
in(X1,add(S,X2)) -> l7(X1,X2,S).
eq(X1,X2) -> l7(X1,X2,S).
in(X1,S),l7(X1,X2,S).

l9(X1,X2,S),l10(X1,X2,S) -> [].
eq(X1,X2) -> l9(X1,X2,S).
in(X1,S) -> l9(X1,X2,S).
in(X1,add(S,X2)),l10(X1,X2,S).


% equality Axioms:

% eq(X,X).
l11(X) -> [].
eq(X,X), l11(X).

% eq(X,Y) -> eq(Y,X).
l12(X,Y),l2(Y,X) -> [].
eq(X,Y) -> l12(X,Y).

% eq(X,Y),eq(Y,Z) -> eq(X,Z).
l12(X,Y),l12(Y,Z),l2(X,Z) -> [].


% eq(X,Y),eq(U,V), in(X,U) -> in(Y,V).

l12(X,Y),l12(U,V),l19(X,U),l20(Y,V).
in(X,U) -> l19(X,U).
in(Y,V), l20(Y,V).

% eq(X,Y),eq(U,V) -> eq(add(X,U),add(Y,V))
l12(X,Y),l12(U,V),l2(add(X,U),add(Y,V)).


% goal add(s,x)=s -> [].
goal l24 -> [].
goal eq(add(s,x),s) -> l24.


first_predicate_precedence([in,eq,l1,l2,l3,l4,l5,l6,l7,l8,l9,l10,l11,l12,
	l13,l14,l15,l16,l17,l18,l19,l20,l21,l22,l23,l24]).




:-sama([2]).