  The s-semantics makes it possible to explicitly deal with variables in
program answers. So it seems suitable for programs using nonground data
structures, like open lists. However it is difficult to find published examples
of using the s-semantics to reason about particular programs.
  Here we apply s-semantics to prove correctness and completeness of
Fr\"uhwirth's $n$ queens program. This is compared with a proof, published
elsewhere, based on the standard semantics and Herbrand interpretations.
