Tells whether term1 and term2 match each other, that is, whether mgu would succeed for them, optionally enabling occurs-check.
Tells whether term1 and term2 match each other, that is, whether mgu would succeed for them. Performs unification with occurs-check enabled.