G. Alagi and C. Weidenbach, NRCL -a model building approach to the Bernays-Schönfinkel fragment, Frocos (Wroclaw), pp.69-84, 2015.

L. Bachmair and H. Ganzinger, Rewrite-based Equational Theorem Proving with Selection and Simplification, Journal of Logic and Computation, vol.4, issue.3, pp.217-247, 1991.
DOI : 10.1093/logcom/4.3.217

H. Comon and P. Lescanne, Equational problems and disunification, Journal of Symbolic Computation, vol.74, issue.3, pp.371-425, 1989.
DOI : 10.1016/s0747-7171(89)80017-3
URL : https://hal.archives-ouvertes.fr/inria-00075652

K. Claessen, New techniques that improve MACE-style finite model finding, Proceedings of the CADE-19 Workshop: Model Computation -Principles, Algorithms, Applications, 2003.

K. Claessen, A. Lillieström, and N. Smallbone, Sort it out with monotonicity -translating between many-sorted and unsorted first-order logic, Automated Deduction -CADE-23 -23rd International Conference on Automated Deduction Proceedings, volume 6803 of Lecture Notes in Computer Science, pp.207-221, 2011.

H. Comon, Disunification: A survey, Computational Logic -Essays in Honor of Alan Robinson, pp.322-359, 1991.

R. Caferra and N. Zabel, A method for simultaneous search for refutations and models by equational constraint solving, Journal of Symbolic Computation, vol.13, issue.6, pp.613-642, 1992.
DOI : 10.1016/S0747-7171(10)80014-8

K. Korovin, Inst-Gen ??? A Modular Approach to Instantiation-Based Automated Reasoning, Programming Logics -Essays in Memory of Harald Ganzinger, pp.239-270, 2013.
DOI : 10.1007/s10817-009-9143-8

J. Lassez and K. Marriott, Explicit representation of terms defined by counter examples, Journal of Automated Reasoning, vol.3, issue.3, pp.301-317, 1987.

R. Nieuwenhuis and A. Rubio, Paramodulation-Based Theorem Proving, Handbook of Automated Reasoning (in 2 volumes), pp.371-443, 2001.
DOI : 10.1016/B978-044450813-3/50009-6

F. Pelletier, Seventy-five problems for testing automatic theorem provers, Journal of Automated Reasoning, vol.26, issue.8, pp.191-216, 1986.
DOI : 10.1007/BF02432151

A. Teucke and C. Weidenbach, First-Order Logic Theorem Proving and Model Building via Approximation and Instantiation, Frontiers of Combining Systems: 10th International Symposium, FroCoS 2015 Proceedings, pp.85-100, 2015.
DOI : 10.1007/978-3-319-24246-0_6