split Unifier into a configuration and the real unifier, the
configuration can be cached but the unifier has to be re-created for
each unification process