assign(max_seconds, 30).

formulas(sos).

% wang1:
(m != b).
(b != k).
(k != m).

% wang2:
%  (m != b).
%  (b = k) | (k = m).
%  (y = j) | -p(y,j) | (y = k).
%  (y = j) | p(y,j) | (y != k).

% wang3:
% (m != b).
% (y = j) | -p(y,j) | (y = k).
% (y = j) | p(y,j) | (y != k).

end_of_list.
