% Theorem 2  (2 -> 3)

formulas(assumptions).

  -D(x,y,z) | A(x,y,z).

end_of_list.

formulas(goals).

  B(x,y,z) & B(y,z,u) & y != z -> B(x,z,u).

end_of_list.