An Optimized KE-Tableau-Based System for Reasoning in the Description Logic $${\mathcal {DL}}_{{\mathbf {D}}}^{4, \!\times }$$