op(400, infix, ^).
op(400, infix, v).

clauses(theory).

x ^ (y v z) = (x ^ y) v (x ^ z).

end_of_list.