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.