formulas(sos). % unique complementation x v x' = 1. x ^ x' = 0. x v y != 1 | x ^ y != 0 | x' = y. end_of_list.