some facts on logics...

fact 1

Simple DLs (like ALC) can be translated into the FOL class L2 (the FOL fragment with no function symbols and only 2 variables).

fact 2

L2 is decidable.

fact 3

FOL with three variables is known to be undecidable.

hm...