In the same way, the stratification rule rejects this program: withUs/1 needs to be above (evaluated later than) withTheTerrorists/1, but also vice versa. I'm not sure how to state this so SWIPL's CLP(FD) can tell that it's unsolvable, but that's probably because I'm a total noob at logic in general:

    ?- X #> Y, Y #> X.
    X#=<Y+ -1,
    Y#=<X+ -1.

    ?- X #> Y, Y #> X, label([X, Y]).
    ERROR: Arguments are not sufficiently instantiated

I'm not very sure about this either, I haven't used CLP(FD) much. triska, the OP in this thread, is the author of the CLP(FD) library and he could help but I guess he's probably moved on from this thread by now.