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