Sufficient, but not necessary

Stratification guarantees a least fixed point, yet some unstratified programs have one anyway.

Take a subtraction game: a pile of stones, players alternate removing 1, 2, or 3, and taking the last stone wins.

A position wins if some move reaches a losing position, so win depends on not win: Datamog rejects!

But every move shrinks the pile, so in fact the program has a least fixed point. The losing positions turn out to be the multiples of 4.

Stratification is sufficient but not necessary. If it cannot be sure, Datamog rejects the program.