unify_with_occurs_check(X, Y) is true if and only if X and Y are unifiable. This predicate carries out standart unification (unification with the occurs check).