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

% Denial of the Robbins basis.

B v A != A v B |
	(A v B) v C != A v (B v C) |
	((A v B)' v (A' v B)')' != B # answer(robbins_basis).

end_of_list.