formulas(sos).

   % Theorem 2 (denials)

% 1 -> 2

% x <= y | y <= x.
% D(ca,cx,cb).
% -A(ca,cx,cb).

% 2 -> 3
-D(x,y,z) | A(x,y,z).

B(ca,cx,cb).
B(cx,cb,cy).
cx != cb.
-B(ca,cb,cy).

end_of_list.