Classically, in saturation-based proof systems, unification has been considered atomic. However, it is also possible to move unification t