[ Comparing and Sorting | Reference Manual | Alphabetic Index ]
# ?Term1 \= ?Term2

Succeeds if Term1 and Term2 are not unifiable.
*Term1*
- An arbitrary term.
*Term2*
- An arbitrary term.

## Description

Succeeds if Term1 and Term2 are not unifiable. It is implemented like

X \= X :- true, !, fail.
_ \= _.

I.e. the arguments are unified, which may cause delayed goals to be
woken and constraints to be checked. Only if all this succeeds, \=/2
fails.
This predicate has a negation-as-failure semantics and so if the
compared terms are not ground, it may give unexpected results. Note
that the original arguments are unchanged after the predicate succeeds.

### Modes and Determinism

### Fail Conditions

Fails if Term1 and Term2 can be unified.
## Examples

Success:
atom \= neutron.
1.0 \= 1.
f(1,2) \= f(1,3).
[1,2] \= [1,3].
[a,b,c] \= [a,b|c].
[a,b,c] \= [X].
[a,X,c,Y] \= [X,b,Y,d].
coroutine, X > 1, X \= 1.
Fail:
X \= Y.
1 \= X.
[a,b|X] \= X.

## See Also

= / 2, \== / 2, not_unify / 2