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))). end_of_list. formulas(goals). all x all y ((-IsIn(x,y) & -IsIn(y,x)) -> (exists z (-(z=x) & -(z=y) & (IsIn(Sum(x,z),Sum(y,z)) | IsIn(Sum(y,z),Sum(x,z)))))). end_of_list.