% Theorem 3

formulas(assumptions).

  x ^ (y v z) = (x ^ y) v (x ^ z)  # label(dist_1).
  x v (y ^ z) = (x v y) ^ (x v z)  # label(dist_2).

end_of_list.

formulas(goals).

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

end_of_list.