  We prove that the occur-check is not needed for a certain definite clause
logic program, independently from the selection rule. First we prove that the
program is occur-check free. Then we consider a more general class of queries,
under which the program is not occur-check free; however we show that it will
be correctly executed under Prolog without occur-check.
  The main result of this report states that the occur-check may be skipped for
the cases in which a single run of a standard nondeterministic unification
algorithm does not fail due to the occur-check. The usual approaches are based
on the notion of NSTO (not subject to occur-check), which considers all the
runs. To formulate the result, it was necessary to introduce an abstraction of
a "unification" algorithm without the occur-check.
