assign(max_seconds, 30).

assign(new_constants, 1).

assign(max_weight,25).

% This proves distributivity from a Boolean algebra basis.

formulas(sos).

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

end_of_list.

set(restrict_denials).

formulas(goals).

  x ^ (y v z) = (x ^ y) v (x ^ z) # label(distributivity_1).

end_of_list.