²Although Sections 13.4 and 14.9 provide a command for computing minimal sets of, respectively, unifiers modulo axioms or modulo a convergent equational theory, at present the complete sets of unifiers used by the narrowing commands are not minimal. Support for narrowing with a minimal set of unifiers is planned for a future release.