Term1 \= Term2

library(not) defines another inequality predicate, as do the C-Prolog and DEC-10 Prolog libraries:

Term1 \= Term2

Term1 and Term2 do not unify

This means exactly the same thing as

     \+ Term1 = Term2
     

and is subject to the same problems as the use of unprovability to simulate negation. However, when the terms are ground, it is more efficient than \==/2.