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