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

formulas(goals).
all x all y (Sum(x,y)=x -> IsIn(y,x)).
end_of_list.