  Thom Fr\"uhwirth presented a short, elegant and efficient Prolog program for
the n queens problem. However the program may be seen as rather tricky and one
may not be convinced about its correctness. This paper explains the program in
a declarative way, and provides proofs of its correctness and completeness. The
specification and the proofs are declarative, i.e. they abstract from any
operational semantics. The specification is approximate, it is unnecessary to
describe the program's semantics exactly. Despite the program works on
non-ground terms, this work employs the standard semantics, based on logical
consequence and Herbrand interpretations.
  Another purpose of the paper is to present an example of precise declarative
reasoning about the semantics of a logic program.
  Under consideration in Theory and Practice of Logic Programming (TPLP).
