```// **************************************************************************
//
//    eses                   eses
//   eses                     eses
//  eses    eseses  esesese    eses   Embedded Systems Group
//  ese    ese  ese ese         ese
//  ese    eseseses eseseses    ese   Department of Computer Science
//  eses   eses          ese   eses
//   eses   eseses  eseseses  eses    University of Kaiserslautern
//    eses                   eses
//
// **************************************************************************
//
// N queens are to be placed on a NxN chessboard so that no queen can
// attack another queen. It is known that there are no solutions for
// chessboards with N<=6.
//
// **************************************************************************

macro N = 6;

module Queens( [N][N]bool q ) {
nothing;
} satisfies {
s [ProveA]: assert
!(
// -- each row contains a queen -------------
( forall(i=0..N-1) exists(j=0..N-1) q[i][j] )
&
// -- forbid row attacks --------------------
( forall(i=0..N-1) forall(j=0..N-1)
(q[i][j] -> forall(k=1..N-1) !q[i][(j+k)%N])
)
&
// -- forbid column attacks --------------------
( forall(i=0..N-1) forall(j=0..N-1)
(q[i][j] -> forall(k=1..N-1) !q[(i+k)%N][j])
)
&
// -- forbid diagonal attacks --------------------
( forall(i=0..N-1) forall(j=0..N-1)
(q[i][j] -> forall(k=1..N-1) !q[(i+k)%N][(j+k)%N])
)
&
// -- forbid diagonal attacks --------------------
(forall(i=0..N-1) forall(j=0..N-1)
(q[i][j] -> forall(k=1..N-1) !q[(i+k)%N][(N+j-k)%N])
)
);
}
```