A description classifier organizes concepts and relations into a taxonomy based on the results of subsumption computations applied to pairs of relation definitions. Until now, description classifiers have only been designed to operate over definitions phrased in highly restricted subsets of the predicate calculus. This paper describes a classifier able to reason with definitions phrased in the full first order predicate calculus, extended with sets, cardinality, equality, scalar inequalities, and predicate variables. The performance of the new classifier is comparable to that of existing description classifiers. Our classifier introduces two new techniques, dual representations and auto-Socratic elaboration, that may be expected to improve the performance of existing description classifiers.