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