This paper is the successor to two previous papers published at the ICFCA conference. In the first paper we have shown that in the Description Logics (mathcal{EL}) and (mathcal{EL}_{ m gfp}), the set of general concept inclusions holding in a finite model always has a finite basis. An exploration formalism that can be used to obtain this basis was presented in the second paper. In this paper we show how this formalism can be modified such that counterexamples to GCIs can be provided in the form of ABox-individuals. In a second part of the paper we examine which description logics can be used for this ABox.