assign(max_seconds, 30).

assign(new_constants, 1).

formulas(sos).

% Single axiom for Boolean algebra in terms of join and complement.

  (((x v y)' v z)' v (x v (z' v (z v u)')')')' = z # label(DN1).

end_of_list.

formulas(goals).

% The Robbins basis.

  y v x = x v y &
  (x v y) v z = x v (y v z) &
  ((x v y)' v (x' v y)')' = y # answer(robbins_basis).

end_of_list.