formulas(sos).

   % Theorem 3 (denials)

% 1 -> 2

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).

B(a,b,c).
B(a,d,c).
B(b,e,d).
-B(a,e,c).

end_of_list.