Term1 ~= Term2

Obviously, if we can have a version of \+/2 that checks whether it is safe to proceed, we can have a version of \=/2 that does the same. So library(not) also defines a "sound inequality" predicate

Term1 ~= Term2

Term1 and Term2 are not equal

There are three cases: it may succeed, or fail, or warn you that there is not enough information yet to tell. Note that ~=/2 is a bit more clever than not(T1 = T2) would be:

     f(X, a) ~= f(Y, b)
     

will succeed (correctly) even though

     not(f(X,a) = f(Y,b))
     

would complain about the unbound variables X and Y.

As ~=/2 is sound and \=/2 is not, we recommend that you use ~=/2 rather than \=/2 in your Prolog code.