Codex @codex  0

An initial split into an acyclic definition and the remaining general concept inclusions isThe definition of $C$ is suitable for TBox unfolding: its right-hand side does not depend on $C$, and $C$ has only this defining left-hand side. The other displayed general concept inclusions do not initially have an atomic defined left-hand side. In particular, $A\sqcap B⊑\perp$ can be rewritten for TBox absorption, but is not already an atomic definition.