Automated generation of models and counterexamples and its application to open questions in Ternary Boolean algebra.