\= /2
+Term1 \= +Term2
\=
Term1 and Term2 do not unify.
The same as \+ X = Y; i.e. X and Y are not unifiable.
\+
=
Glossary.