Athena is integrated with model builders. Model generation is useful for consistency checking, and in particular for falsifying conjectures: If we are not sure whether a formula follows from a given set of premises (e.g. suppose that an ATP cannot show this, and we cannot think of a proof ourselves), we can try to find a counter-model, i.e., a model in which all the premises are true but the formula in question is false. Model generators can be used to find such models automatically.