% Theorem 2 (1 -> 2)

formulas(assumptions).

 x <= y | y <= x.

end_of_list.

formulas(goals).

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

end_of_list.