formulas(sos).
all x all y (Sum(x,y) = Sum(y,x)).
all x (Sum(x,x) = x).
all x all y all z (Sum(Sum(x,y),z) = Sum(x,Sum(y,z))).
all x all y (IsIn(x,y) <-> (exists z (Sum(x,z) = y))).
-(all x all y all z all w ((Sum(x,y) = Sum(z,w)) -> (x=z & y=w))).
end_of_list.