Unification is a form of pattern matching. Which of the following is not a characteristic of unification?

1. Unification never changes the binding of a bound variable.
2. Unification is symmetric; unifying A with B has exactly the same effect as unifying B with A.
3. Unification is very slow, and is only used rarely during computations of logic programs.
4. Unification can bind unbound variables.

In fact, every step in a logic program involves performing a unification, and the speed of the unification implementation is primarily what limits the speed of implementations of logic programming languages.