% Theorem 4

formulas(assumptions).

  x v (y ^ (x v z)) = (x v y) ^ (x v z) # label("modularity_1").
  x ^ (y v (x ^ z)) = (x ^ y) v (x ^ z) # label("modularity_2").

end_of_list.

formulas(goals).

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

end_of_list.