X \= Y is true if and only if X and Y are not unifiable. For unification with occurs check see unify_with_occurs_check/2