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