set(arithmetic).

formulas(assumptions).

% n-Queens Puzzle
%
% Relation Q(x,y) means there is a queen at row x, column y.

all x exists y Q(x,y).           % Each row has at *least* one queen.

Q(x,y1) & Q(x,y2) -> y1 = y2.    % Each row has at most one queen.

Q(x1,y) & Q(x2,y) -> x1 = x2.    % Each column has at most one queen.

Q(x1,y1) & Q(x2,y2) & (x2 + -x1 = y2 + -y1) ->
           x1 = x2 & y1 = y2.     % Each \ diagonal has at most one queen.

Q(x1,y1) & Q(x2,y2) & (x1 + -x2 = y2 + -y1) ->
           x1 = x2 & y1 = y2.     % Each / diagonal has at most one queen.

end_of_list.
