unify

open fun unify(term1: Term, term2: Term, occurCheckEnabled: Boolean): Term?

Unifies term1 and term2 if possible, optionally enabling occurs-check.

the result of applying the computed mgu to term1 (retaining term1's orientation), or null if term1 and term2 do not unify.

open fun unify(term1: Term, term2: Term): Term?

Unifies term1 and term2 if possible, with occurs-check enabled.