The paper discusses the unification problem in the description logic $\mathcal{FL}_\bot$, which extends $\mathcal{FL}_0$ by adding the bottom concept constructor. The unification problem involves finding a substitution that makes two concepts equivalent. The paper presents an algorithm for solving this problem, which runs in exponential time relative to the size of the input. The algorithm is divided into two stages: flattening and solving a normalized problem. Flattening involves guessing how variables should be substituted, while solving the normalized problem involves using techniques from $\mathcal{FL}_0$ and a decreasing rule to find a unifier. The paper also introduces the concept of shortcuts, which are pairs of sets of variables used to distribute $\bot$-particles over flat subsumptions. The main procedure of the algorithm is described, along with sub-procedures for computing shortcuts and checking their validity. The paper concludes with a proof of the algorithm's correctness and termination, showing that it terminates in at most exponential time.The paper discusses the unification problem in the description logic $\mathcal{FL}_\bot$, which extends $\mathcal{FL}_0$ by adding the bottom concept constructor. The unification problem involves finding a substitution that makes two concepts equivalent. The paper presents an algorithm for solving this problem, which runs in exponential time relative to the size of the input. The algorithm is divided into two stages: flattening and solving a normalized problem. Flattening involves guessing how variables should be substituted, while solving the normalized problem involves using techniques from $\mathcal{FL}_0$ and a decreasing rule to find a unifier. The paper also introduces the concept of shortcuts, which are pairs of sets of variables used to distribute $\bot$-particles over flat subsumptions. The main procedure of the algorithm is described, along with sub-procedures for computing shortcuts and checking their validity. The paper concludes with a proof of the algorithm's correctness and termination, showing that it terminates in at most exponential time.