Constraint that expresses that Term1 and Term2 never become
identical (==/2). Fails if Term1 == Term2. Succeeds if Term1
can never become identical to Term2. In other cases the
predicate succeeds after attaching constraints to the relevant
parts of Term1 and Term2 that prevent the two terms to become
identical.