I will discuss the latest developments in Equinox, an instance-based theorem prover that not only produces proofs, but can also produce approximative counter models in case of a failed proof search. I will argue for the usefulness of such models and present a number of practical examples.