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