
formulas(sos).

% unique complementation

x v x' = 1.
x ^ x' = 0.

x v y != 1 | x ^ y != 0 | x' = y.

end_of_list.
