N-Bishops Puzzle

This puzzle is a variation of the N-Queens puzzle: we try to place as many bishops as possible on a n by n chess board. In contrast to the N-Queens puzzle, one can place more than one bishop per row. As such, we can now longer represent the positions of the bishops as an total function 1..n >-> 1..n. There are two encodings we show below. The first represents the bishops as a subset of the Cartesian product (1..n)*(1..n), i.e., a set of positions (aka a binary relation on 1..n).

MACHINE NBishopsSets
CONSTANTS n, nbishops, hasbishop
PROPERTIES
 n=8 &
 hasbishop <: (1..n)*(1..n) & 
 !(i,j).(i:1..n & j:1..n
    =>
    ( (i,j): hasbishop
       =>
        (!k.(k:(i+1)..n => 
           (k,j+k-i) /: hasbishop &
           (k,j-k+i) /: hasbishop
        ))
    ))
 & nbishops = card(hasbishop) 
 & nbishops >13
END

The maximum number of bishops tath can be placed is 2*n - 2; see http://mathworld.wolfram.com/BishopsProblem.html