The presented approach aims at identifying false conjectures about
free data types. Given a specification and a conjecture, the method
performs a search for a model of an according counter
specification.  The model search is tailor-made for the semantical
setting of free data types, where the fixed domain allows to describe
models just in terms of interpretations.  For sake of
interpretation construction, a theory specific calculus is provided.
The concrete rules are `executed' by a procedure known as model
generation.  As most free data types have infinite domains, the
ability of automatically solving the non-consequence problem is
necessarily limited.  That problem is addressed by limiting the
instantiation of the axioms.  This approximation leads to a
restricted notion of model correctness, which is discussed.  At the
same time, it enables model completeness for free data types, unlike
approaches based on limiting the domain size.