The model SHARP is a result of (somewhat naively) implementing a tableaux-based reasoning algorithm of the description logic ALE into the cognitive architecture ACT-R. Its aim is to predict the inference time of human performance on deciding inconsistency of an ALE ABox, thereby giving rise to a complexity measure on ABoxes that is cognitively adequate. Ten predictions following from SHARP are tested against empirical data and their implications for the model are discussed.