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