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