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