set(auto).
set(print_initial_clauses).
set(print_given).

formulas(sos).
% Commutativity
all x all y (Sum(x,y) = Sum(y,x)).

% Idempotence
all x (Sum(x,x) = x).

% Associativity
all x all y all z (Sum(Sum(x,y),z) = Sum(x,Sum(y,z))).

% Inclusion
all x all y (IsIn(x,y) <-> (exists z (Sum(x,z) = y))).

% Postulate 1:
% all x exists y (-IsIn(x,y) & -IsIn(y,x)).

% Postulate 2
% all x all y exists z (Sum(x,y) = z).

end_of_list.