?. ,

, P(z, y) and ? Q(x, x) with P(x, y) ? P(x, z), P(z , y) and ? Q(x, x ), respectively. Consequently, ordered resolution derives ? P(a, z 1 ), P(z 2 , a) which subsumes any further inference clauses ? P(a, FO-AR replaces P(x, y) ? P(x, z)

, Both examples belong to the Bernays-Schönfinkel fragment, so model evolution (Darwin) and Inst-Gen (iProver) can decide them as well, Hence, saturation of the approximation terminates immediately

, With a shallow approximation of P(x, y) ? P(g(x), z) into S(v) ? P(v, z) and P(x, y) ? S(g(x)), FO-AR (SPASS-AR) terminates after deriving ? S(g(a)) and S(x) ? S(g(x)). Again, model evolution (Darwin) and Inst-Gen (iProver) can also solve this example, superposition derives all clauses of the form ? P(g

, P( f ( f (x))) ? P(x)

, is already saturated under superposition. For FO-AR, the clause P(x) ? P( f ( f (x))) is replaced by S(x) ? P( f (x)) and P(x) ? S( f (x)). Then ordered resolution terminates after inferring S(a) ? and S( f (x)) ? P(x)

, The Inst-Gen and model evolution calculi, however, fail. In either, a satisfying model is represented by a finite set of literals, i.e, a model of the propositional approximation for Inst-Gen and the trail of literals in case of model evolution. Therefore, there necessarily exists a literal P( f n (x)) or ¬P( f n (x)) with a maximal n in these models

, Lastly consider an example of the form f (x) ? x ?; f ( f (x)) ? x ?; . . . ; f n (x) ? x ? which is trivially satisfiable, e.g., saturated by superposition, but any model has at least n + 1 domain elements. Therefore, adding these clauses to any satisfiable clause set containing f forces calculi that explicitly consider finite models to consider at least n + 1 elements. The performance of final model finders [16] typically degrades in the number of different domain elements to be considered. Combining each of these examples into one problem is then solvable by neither superposition, Inst-Gen, or model evolution and not practically solvable with increasing n via testing finite models. For example

. P(-f,

, P( f ( f (x)), y) ? P

, P(x, y) ? P( f ( f (x)), y)

). ?-x-?; and .. .. ,

, Vampire, iProver, and Darwin for more than one hour each without success. Only SPASS-AR solved it in less than one second. For iProver we added an artificial positive equation b ? c. For otherwise, iProver throws away all inequations while preprocessing. This is a satisfiability preserving operation, however, the afterwards found (finite) models are not models of the above clause set due to the collapsing of ground terms

). and P. (x-,-y,-z)-?-p,

, P(x, y , z) ? P(x, f 3 (y), z)

). and P. (x,-y,-z-)-?-p,

L. Bachmair and H. Ganzinger, Rewrite-based equational theorem proving with selection and simplification, Revised version of Max-Planck-Institut für Informatik technical report, vol.4, pp.217-247, 1991.

L. Bachmair and H. Ganzinger, Ordered chaining calculi for first-order theories of transitive relations, Journal of the ACM, vol.45, issue.6, pp.1007-1049, 1998.

J. C. Baeten, J. A. Bergstra, J. W. Klop, and W. P. Weijland, Term-rewriting systems with rule priorities, Theor. Comput. Sci, vol.67, issue.2&3, pp.283-301, 1989.

P. Baumgartner, A. Fuchs, and C. Tinelli, Implementing the model evolution calculus, International Journal on Artificial Intelligence Tools, vol.15, issue.1, pp.21-52, 2006.

P. Baumgartner and C. Tinelli, The model evolution calculus, 19th International Conference on Automated Deduction Miami Beach, vol.2741, pp.350-364, 2003.

R. Caferra, A. Leitsch, and N. Peltier, Automated Model Building, Applied Logic, vol.31, p.55, 2004.

H. Comon, M. Dauchet, R. Gilleron, C. Löding, F. Jacquemard et al., Tree automata techniques and applications. Available on, 2007.

J. Goubault-larrecq, Deciding H 1 by resolution, Information Processing Letters, vol.95, issue.3, pp.401-408, 2005.

F. Jacquemard, C. Meyer, and C. Weidenbach, Unification in extensions of shallow equational theories, Rewriting Techniques and Applications, 9th International Conference, RTA-98, vol.1379, pp.76-90, 1998.
URL : https://hal.archives-ouvertes.fr/inria-00098740

K. Korovin, iprover -an instantiation-based theorem prover for first-order logic (system description), Automated Reasoning, 4th International Joint Conference, vol.5195, pp.292-298, 2008.

K. Korovin, Inst-Gen -A modular approach to instantiation-based automated reasoning, Programming Logics -Essays in Memory of Harald Ganzinger, pp.239-270, 2013.

L. Kovács and A. Voronkov, First-order theorem proving and vampire, Computer Aided Verification -25th International Conference, CAV 2013, vol.8044, pp.1-35, 2013.

H. Seidl and A. Reuß, Extending H1-Clauses with Disequalities, Information Processing Letters, vol.111, issue.20, pp.1007-1013, 2011.

H. Seidl and A. Reuß, Extending ${\cal H} 1$ -clauses with path disequalities, Foundations of Software Science and Computational Structures -15th International Conference, FOSSACS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, vol.7213, pp.165-179, 2012.

H. Seidl and K. N. Verma, Cryptographic protocol verification using tractable classes of horn clauses, Program Analysis and Compilation, Theory and Practice, pp.97-119, 2007.

J. K. Slaney and T. Surendonk, Combining finite model generation with theorem proving: Problems and prospects, Frontiers of Combining Systems, First International Workshop FroCoS, vol.3, pp.141-155, 1996.

M. Suda, C. Weidenbach, and P. Wischnewski, On the saturation of yago, Automated Reasoning, 5th International Joint Conference, IJCAR 2010, LNAI, vol.6173, pp.441-456, 2010.

G. Sutcliffe, The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, vol.43, pp.337-362, 2009.

A. Teucke, M. Voigt, and C. Weidenbach, On the expressivity and applicability of model representation formalisms, Frontiers of Combining Systems -12th International Symposium, vol.11715, pp.22-39, 2019.
URL : https://hal.archives-ouvertes.fr/hal-02406605

A. Teucke and C. Weidenbach, First-order logic theorem proving and model building via approximation and instantiation, Frontiers of Combining Systems: 10th International Symposium, pp.85-100, 2015.

A. Teucke and C. Weidenbach, Ordered resolution with straight dismatching constraints, Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning co-located with International Joint Conference on Automated Reasoning (IJCAR 2016), vol.1635, pp.95-109, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01403206

A. Teucke and C. Weidenbach, Decidability of the monadic shallow linear first-order fragment with straight dismatching constraints, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01657026

A. Voronkov, AVATAR: the architecture for first-order theorem provers, Computer Aided Verification -26th International Conference, vol.8559, pp.696-710, 2014.

C. Weidenbach, Towards an automatic analysis of security protocols in first-order logic, 16th International Conference on Automated Deduction, CADE-16, LNAI, vol.1632, pp.314-328, 1999.

C. Weidenbach, D. Dimova, A. Fietzke, R. Kumar, M. Suda et al., Automated Deduction -CADE-22, 22nd International Conference on Automated Deduction, vol.5663, pp.140-145, 2009.