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