This paper aims to do two things. Firstly, it discusses how the VAMPIRE automatic theorem prover both succeeds and fails at pretending to be an SMT solver. We discuss how Vampire reasons with problems containing both quantification and theories, the limitations this places on what it can do, and the advantages this provides over the standard SMT approach. Secondly, it focuses on the problem of instantiation of quantified formulas and asks whether VAMPIRE needs it (it does) and whether it can directly borrow techniques from SMT solving (maybe).
VAMPIRE [22] is an automatic theorem prover (ATP) for first-order logic. It is successful at
establishing both theorems and non-theorems, winning related tracks in the well-known CASC competition1
[37]. For the last few years, we have been extending VAMPIRE’s theory reasoning abilities and in 2016
VAMPIRE entered SMT-COMP2 [
Whilst there is a long history of extending ATPs with theory reasoning capabilities, this has only achieved limited success and in recent years theory reasoning has been dominated by SMT solvers. To extend satisfiability checking procedures for ground theories to handle quantifiers, the focus has been on instantiation techniques that aim to find useful instances of quantified formulas to pass to the ground procedures. Arguably, this may become a bottleneck when the reasoning requires many non-trivial instances. Conversely, ATPs reason directly with universally quantified clauses and make inferences at this level, e.g., p(x) _ q(x) resolves with :p(f (y)) to establish that all instances of q(f (y)) must hold. This approach performs generally well for pure first-order problems, but is not traditionally suited to reasoning with theories. We conjecture (currently without evidence) that instance-based techniques are more suited to problems with large ground parts and small quantified parts, whilst saturation-based techniques are more suited to problems making heavy use of quantifiers. We are currently exploring this conjecture. The goal of recent developments in VAMPIRE has been to preserve efficient techniques for reasoning with quantifiers whilst adding effective techniques for reasoning with theories.
This paper assumes general knowledge of SMT solving and first-order logic as this paper is written with the SMT community in mind. An introduction to these topics can be found in many of the papers cited in this paper. We begin (Section 2) by describing how VAMPIRE is both similar and different to an SMT solver. We then describe briefly how VAMPIRE currently reasons with quantifiers and theories (Section 3). Finally, we consider the issue of instantiation, the primary approach for dealing with quantified formulas in SMT solvers, and consider its relevance to reasoning in VAMPIRE (Section 4).
Here we describe the main differences between SMT solvers and an ATP such as VAMPIRE. The
following discussion is applicable to provers similar to VAMPIRE, but to save space we will take VAMPIRE
as a canonical example of provers similar to VAMPIRE and make a direct comparison between SMT
solvers and VAMPIRE. To be more precise, when we refer to SMT solvers we are generally thinking of
lazy CDCL(T ) solvers [
The main similarity between an SMT solver and VAMPIRE is that both accept problems in first-order
logic extended with theories. VAMPIRE accepts problems in SMT-LIB syntax [
The main difference between an SMT solver and VAMPIRE is that SMT solvers have
satisfiabilitychecking at their core, whilst VAMPIRE has unsatisfiability-checking at its core, as it is a refutational
prover. By this we mean that SMT solvers attempt to build a model satisfying the input problem,
whilst VAMPIRE attempts to find a proof that the input problem is inconsistent. If an SMT solver
succeeds it returns sat and if VAMPIRE succeeds it returns unsat. Under certain circumstances, a
failure to build a model or find a proof means that no model or proof exists. In that case, an SMT
solver would return unsat and VAMPIRE, respectively, would return sat. A third option is that the
process runs out of resources before establishing either or the process is incomplete, in which case
both would return unknown. For SMT solvers, incompleteness comes from ground theories lacking
decision procedures and from incomplete instantiation techniques. For VAMPIRE, incompleteness can
come from certain proof search heuristics (e.g. selection functions [
A key feature of SMT solvers is the ability to produce models. As explained further below, VAMPIRE finds unsatisfiability by deriving a contradiction from the input problem through the iterative generation of consequences of that problem. This approach is well-suited to producing proofs of unsatisfiability, but does not in general produce models. Whilst VAMPIRE does support finite model building [30], this is (currently) restricted to the theory of uninterpreted functions only.
Another frequently used feature of SMT solvers is their ability to be used incrementally, due to their basis in the backtracking search of CDCL. VAMPIRE does not share this quality as proof search is inherently non-incremental and cumbersome to backtrack. We give further explanation for why below.
Similar to many SMT solvers, VAMPIRE is a portfolio solver. It implements many different techniques and when solving a problem it may use tens to hundreds of different strategies in a time-sliced fashion. Along with the below saturation-based proof search method, VAMPIRE also implements the InstGen calculus [19] and a finite-model building through reduction to SAT [30]. In addition, VAMPIRE can be run in a parallel mode where strategies are distributed over a given number of cores. 2.2
To illustrate the differences outlined above we will briefly describe saturation-based proof search. Usually, VAMPIRE deals with the separate notions of axioms and conjecture,3 but SMT-LIB does not have 3 Intuitively, axioms formalise the domain of interest and the conjecture is the claim that should logically follow from the axioms. Conjecture is, therefore, negated before we start the search for a contradiction. these notions and we assume an input (conjunctive) set of formulas. This set of formulas is clausified to produce a set of clauses S. This set is then saturated with respect to some inference system I meaning that for every inference from I with premises in S the conclusion of the inference is also added to S. If the saturated set S contains a contradiction then the initial formulas are unsatisfiable. Otherwise, if I is a complete inference system and, importantly, the requirements for this completeness have been preserved, then the initial formulas are satisfiable. Finite saturation may not be possible and many heuristics are employed to make finding a contradiction more likely.
The standard approach to saturation is the given-clause algorithm illustrated in Figure 1. The idea is to have a set of active clauses with the invariant that all inferences between active clauses have been performed and a set of passive clauses waiting to be activated. The algorithm then iteratively selects a given clause from passive and performs all necessary inferences to add it to active. This process of clause selection is important for good performance (and fairness) but not discussed here.
VAMPIRE uses resolution and superposition as its inference system I [
It is important to note that the process of going from input formulas to clauses is (i) important for
efficiency, but also (ii) typically not equivalence preserving. Whilst the generation of clauses from
formulas typically preserves models on the initial signature [31], many useful preprocessing steps remove
part of the input. For example, the removal of unused definitions [
Let us consider what incrementality would look like in this setting. After saturating the set of
clauses, a new set of clauses would be added, and proof search would continue. However, this new set
of clauses may break the conditions under which optimising preprocessing steps are applied, making
proof search incomplete. An easy solution would be to disable such preprocessing steps, as is done
in incremental SMT. Additionally, care should be taken if the signature is extended, as parameters to
proof search, such as term orderings, are dependent on the signature. Another important element of
incremental proof search is the ability to backtrack previously asserted formulas. This would require
the removal of clauses that may have caused the reduction of other clauses, requiring heavy machinery
for tracking and undoing such steps (as done in splitting with backtracking [
Quantifier-Free Problems. Our first set of results is for problems that VAMPIRE is unlikely to perform well on: quantifier-free problems. Table 1 uses the results from SMT-COMP 2016 and compares these to results from a VAMPIRE run on the same problems and platform (e.g. StarExec). We only considered problems known to be unsatisfiable, as VAMPIRE cannot show satisfiability for problems with theories. In general, VAMPIRE did not perform as well as most other SMT solvers, although it solved 24 problems uniquely, mostly in non-linear real arithmetic. The conclusion is that VAMPIRE should not be selected as the system of choice for solving quantifier-free problems. The results for QF UF show that this conclusion is not restricted to problems involving arithmetic, although the difference here is small. Quantifier Problems. Our previous study [27] compared VAMPIRE and three well-known SMT solvers (CVC4, veriT, and Z3) and we refer the reader to this publication for those results. In this evaluation, which considered problems that were unsatisfiable or whose results were unknown, VAMPIRE solved the most problems overall (by 0.2%) and the most for the logics AUFLIRA, AUFNIRA, UFIDL, and UFNIA. The improvement over other SMT solvers is not very large, but there were unique solutions suggesting a complementary approach.
x + (y + z) = (x + y) + z (x + y) = ( x + y)
x 0 = 0 x y = y x x < y _ y < x _ x = y :(x < x) x + 0 = x
x = x x (y z) = (x y) z (x y) + (x z) = x (y + z)
:(x < y) _ :(y < x + 1) x < y _ y < x + 1 (for ints) x + y = y + x x + ( x) = 0
x 1 = x :(x < y) _ :(y < z) _ :(x < z)
:(x < y) _ x + z < y + z x = 0 _ (y x)=x = y (for reals ) SMT solvers and VAMPIRE are different mainly due to their underlying proof search approach, and thus the features available (i.e. limited model-building for VAMPIRE). They are similar as they apply to the same problems and, for a large number of problems, perform similarly. However, results show that, mostly likely due to this fundamental difference in approach, they are likely to complement each other. 3
The previous section explained how VAMPIRE is different from an SMT solver. So how does it perform theory reasoning? This section aims at addressing this question. 3.1
One of the earliest practical saturation-based approaches for reasoning with theories was SPASS+T [26]. They utilised two ideas that we adopted in VAMPIRE: simplification of theory terms, and introduction of theory axioms. This approach for theory reasoning has been implemented in VAMPIRE since 2010. Evaluation. In VAMPIRE, this is implemented as an immediate simplification, i.e., whenever we generate a new term we eagerly evaluate it. Currently, evaluation is restricted to arithmetic terms only (we do not perform evaluation on arrays) and consists of three kinds of simplification:
Normalisation: Literals containing inequalities are rewritten in terms of < only, e.g., t1 t2 :(t1 < t2). Subtraction is rewritten in terms of addition of negative numbers and some specialised arithmetic operations, such as rounding functions coming from the TPTP language4, are rewritten in terms of standard operators.
Evaluation: Purely interpreted subterms are evaluated with respect to the standard model of arithmetic, e.g., f (1 + 2) f (3) and f (x + 0) f (x). Purely interpreted literals are treated similarly, e.g., 1 + 2 < 4 true.
Balancing: Literals containing a single uninterpreted term or a variable may be ‘balanced’ by bringing interpreted constants to one side to allow further evaluations, e.g. 4 = 2 (x + 1) (4 div 2) 1 = x x = 1 and 2 a > 2 a < 1. Care is taken to avoid division by zero and integer division is only applied when there is no non-trivial remainder.
4A standard input language for first-order theorem provers [36].
Theory Axioms. In VAMPIRE, the signature of the input problem is analysed to select which theory axioms to add. A theory axiom is a statement true in some relevant theory. The theory axioms VAMPIRE might add for the theory of arithmetic are given in Figure 2.5 It is important to note that we only need to consider < because, as described above, VAMPIRE normalises input formulas by rewriting all inequalities in terms of <. VAMPIRE also adds a finite axiomatisation of arrays [20] if they appear in the signature, and relevant axioms for term algebras (datatypes) [21].
One issue with reasoning with theory axioms is that they can be explosive, i.e., they combine with each other, making the search space grow quickly. Recent work in VAMPIRE has explored heuristic techniques for restricting this effect [28]. So far, VAMPIRE has not made any separate efforts to handle particularly harmful associativity and commutativity axioms, as has been done in other solvers [35].
Lastly, the term ordering gives high precedence to uninterpreted operations and totally orders interpreted constants. The result is that the uninterpreted parts of clauses tend to be targeted by the superposition calculus before the interpreted part. 3.2
A recently implemented feature [32] in VAMPIRE is a specialised unification that handles interpreted terms separately from uninterpreted terms.6 The general idea is to avoid having to perform abstraction eagerly. Take, for example, the clauses which cannot unify without first being abstracted to r(14y)
:r(x2 + 49) _ p(x); r(u) _ u 6' 14y
:r(v) _ v 6' x2 + 49 _ p(x) allowing resolution to produce
u 6' 14y _ u 6' x2 + 49 _ p(x): The unification with abstraction approach will allow the first two clauses to unify directly under the constraint 14y 6= x2 + 49. This directly captures the condition under which the terms can unify and is something to which theory reasoning can be directly applied. We note that this rule directly resolves the issue of losing proofs via eager evaluation, i.e. where p(1 + 3) is eagerly evaluated to p(4), missing the chance to resolve with :p(x + 3).
This feature is implemented by extending the substitution tree indexing structures used in VAMPIRE to perform unification. 3.3
A key technique in VAMPIRE is the use of AVATAR to control clause splitting. A full description of how AVATAR works is beyond the scope of this paper, but it is also not essential for this discussion and has been given elsewhere [38, 29]. Instead, we imagine VAMPIRE with AVATAR as an SMT solver with a saturation-based theory solver for the theory of quantified formulas, as illustrated in Figure 3.
5We have ignored some less standard operators such as floor and ceiling operators. We also ignore integer division for simplicity of exposition.
6Note that the experimental results described previously do not contain this new feature.
VAMPIRE with AVATAR
Theory Solver for Quantified Formulas
Theory Solver for Arithmetic
Theory Solver for BitVectors
Core CDCL SAT Solver
Theory Solver for Uninterpreted Functions
Quantifier Instantiation
AVATAR inside VAMPIRE. The previously described given-clause algorithm is extended by using a
SAT solver to iteratively select sub-problems of the input problem to find inconsistencies within. To do
this, the initial clause set, and all subsequent clauses, are propositionally abstracted and the propositional
abstraction is given to a SAT solver. This is similar to how the SAT solver is utilised in SMT solvers but
is applied to the full problem, not just to the ground part. However, to preserve soundness it is necessary
to only break clauses down into variable-disjoint sub-clauses. For example, the following clause
s(x) _ :r(x; z) _ :q(w)
| share {xzand z }
is|di{szjoi}nt
is split into two sub-clauses, each propositionally abstracted. If a set of sub-clauses with propositional
names a1; : : : ; an are shown to be inconsistent then the propositional clause :a1 _ : : : _ :an is learned
(passed to the SAT solver) and a new sub-problem is selected by rerunning the SAT solver.
Replacing SAT by SMT. The relevance to theory reasoning is when the SAT solver is replaced by an
SMT solver [27]. The only difference is that where previously sub-clauses were translated as
propositional symbols, now only non-ground subclauses are so translated whilst ground (necessarily unit)
sub-clauses are mapped directly as themselves. In this case, the subproblem being explored by the
first-order saturation-based proof search is guaranteed to be theory-consistent in the ground part.
VAMPIRE as a Theory Solver. Conversely, the above can be viewed as adding VAMPIRE as a theory
solver for quantified formulas which is invoked when a theory-consistent model for the abstraction is
constructed. It is still necessary to propositionally abstract the quantified clauses in the SAT solver,
otherwise the clause-splitting advantage of AVATAR would be lost. Indeed, this is one of the main
differences between this approach and the work of DPLL( ) [
Another prominent approach is to extend the calculus with specialised inference rules. This is what
we do for reasoning with terms of boolean sort [20], datatypes [21], and the extensionality rule for
arrays [
C _ s = t _ s t
C _ s 1
t
C _ s = t _ s + 1
t
aimed at encoding the above integer ordering axioms, thus avoiding their explosive combination.
Another practical work that extends the superposition calculus with additional rules is the Zipperposition
tool [
This section focuses on the issue of instantiation (missing from the previous section). We separate this issue as it is the key method by which SMT solvers handle quantified formulas and we want to understand if these ideas can help saturation-based solvers. 4.1
To see why VAMPIRE can benefit from instantiation, consider the first-order clause 14x 6' x2 + 49 _ p(x) for which there is a single integer value for x that makes the first literal false with respect to the underlying theory of arithmetic, namely x = 7. However, if we apply standard superposition rules to the original clause and a sufficiently rich axiomatisation of arithmetic (e.g. the one we gave previously), we will most likely end up with a very large number of logical consequences and never generate p(7), or run out of space before generating it. Indeed, VAMPIRE cannot find a refutation of 14x 6' x2 + 49 in reasonable time using the techniques described in the previous section. 4.2
Here we briefly overview the main instantiation techniques used in SMT solving. This is largely taken from a recent review of the topic [33] and this text should be referenced for full details. The Quantifier Instantiation Module. Modern SMT solvers based on the CDCL(T ) architecture (Figure 3) separate the input into ground and non-ground parts. To handle non-ground parts they first establish a satisfiable ground model and then ask the quantifier instantiation module to suggest instances of the non-ground formulas. Below we outline the three main approaches to quantifier instantiation. They all follow a similar pattern: to take 8xP (x) and find some terms t to produce an instance P (t). E-Matching. The general idea is to use patterns to match against existing terms to produce possible instances. Pattern selection is a complex topic [23], but a simple choice is to use sub-terms of the formula being instantiated. For example, given the non-ground formula P (x) _ R(x) the sub-term P (x) could be used as a pattern to match against an existing ground term P (a) to produce instance P (a) _ R(a). This typically makes use of the congruence closure data structures (E-graph) available for the theory of uninterpreted functions, so if this implied that a = f (b) then the instance P (f (b)) _ R(f (b)) could also be created in the above example. A key point is that patterns are usually restricted to applications of uninterpreted functions and instantiation is with existing terms only.
Conflict-Based Instantiation. An issue with E-matching is that it is unguided, it is not clear whether
the created instances are helpful. In conflict-based instantiation the idea is to produce instances that are
in conflict with the current model, forcing it to change. Such instances are a special case of those found
by E-matching and the difficulty is not in checking if an instance is conflicting, but in finding
conflicting instances efficiently [34]. Finding conflicting instances in the presence of interpreted symbols is
additionally challenging due to the need to check entailment modulo the relevant theory.
Model-Based Instantiation. The above two approaches are incomplete, i.e., the failure to find a
(conflicting) instance does not imply that formula in question is satisfiable. In model-based instantiation [
We briefly examine each of the above instantiation approaches and consider whether we could borrow
the idea and use it within VAMPIRE, or a similar ATP. Firstly, we note that the focus of instantiation will,
in general, be different. In ATP systems, there is a good approach for dealing with quantified formulas
containing uninterpreted symbols and it is those containing interpreted symbols that are the challenge.
Whilst for SMT solvers instantiation seems to be focussed on the uninterpreted parts, as they typically
have reasonable methods for dealing with interpreted symbols, e.g., quantifier elimination [
C[s] ground(s)
ground(s) L[t] _ D ground(u1) : : : ground(un) export((L[t] _ D) ) with similar restrictions to the above, but in addition s is uninterpreted and u1; : : : ; un are the uninterpreted ground terms in (L[t] _ D) different from s. The general idea is to use the special predicate ground to store the set of ground terms that are removed by subsumption.
We would like to reiterate the above point about subsumption. Instantiating the clause x > c _ x < c to produce 0 > c _ 0 < c is unhelpful as the new clause is immediately subsumed and deleted. However, if one of the literals in (L[t] _ D) becomes false the subsumption no longer holds. For example, instantiating x > y _ p(x; y) with fx 7! 0; y 7! 1g produces p(0; 1), which is not subsumed.
This leads us to the observation that the instances useful to saturation-based proof search are those that remove literals, which in the limit will lead to the empty clause. In [32] we introduce a theory instantiation rule that explicitly produces instances that remove literals. The general idea is as follows. Given a clause C[x] _ D[x] where D[x] consists purely of interpreted symbols, a solution such that (:D[x]) is T-valid (true in every model of the relevant theory) can be used to produce the instance C[x] . The problem of finding such a solution is something that an SMT solver handles well. Conflict-Based Instantiation. In typical saturation-based proof search there is no concept of a model to be in conflict with. But, when AVATAR is being used for clause splitting, there is now a model of the current splitting branch. If we were to take the view that VAMPIRE becomes an extra theory module via AVATAR, then we could directly apply conflict-based instantiation to produce instances inconsistent with the current splitting branch. Conversely, attempting to do this whilst using an SMT solver as a black-box does not seem workable.
If this approach were in place, then the new question would become whether it is better to spend effort finding conflicting instances to refute a splitting branch, or using saturation-based reasoning. The above combination and this question remain further research. Our conjecture is that the two approaches would be complementary and a heuristic combination would be beneficial.
Model-Based Instantiation. Currently, if VAMPIRE saturates a particular splitting branch it is not clear if this is due to the incompleteness of its proof search or the consistency of that branch. The model-based instantiation approach could provide a technique for (i) returning satisfiable in such a circumstance, or (ii) otherwise refuting the current splitting branch and continuing with proof search. Again, the question would then be whether the combination with saturation-based proof search contributes to this general approach. 5
We have briefly compared how VAMPIRE performs theory reasoning to the standard architecture of
modern SMT solvers and discussed the topic of instantiation. It is clear that the integration of saturation
provers with SMT solvers can be further explored, especially with respect to instantiation. If we view
AVATAR as a method for adding VAMPIRE as a theory solver to an SMT solver then an important open
question remains: when should VAMPIRE be called, and when should existing quantifier instantiation
techniques be used instead. Recent work [
Deduction CADE-24, vol. 7898 of Lecture Notes in Computer Science, pp. 450–464. Springer, 2013. [19] K. Korovin. Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning. In Programming
Logics: Essays in Memory of Harald Ganzinger, pp. 239–270. Springer Berlin Heidelberg, 2013. [20] E. Kotelnikov, L. Kova´cs, G. Reger, and A. Voronkov. The vampire and the FOOL. In Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016, pp. 37–48, 2016. [21] L. Kova´cs, S. Robillard, and A. Voronkov. Coming to terms with quantified reasoning. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pp. 260–270. ACM, 2017. [22] L. Kova´cs and A. Voronkov. First-order theorem proving and Vampire. In CAV 2013, vol. 8044 of Lecture
Notes in Computer Science, pp. 1–35, 2013. [23] K. R. M. Leino and C. Pit-Claudel. Trigger selection strategies to stabilize program verifiers. In Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I, pp. 361–381, 2016. [24] D. Monniaux. Quantifier elimination by lazy model enumeration. In Computer Aided Verification: 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings, pp. 585–599. Springer Berlin Heidelberg, 2010. [25] R. Nieuwenhuis and A. Rubio. Paramodulation-based theorem proving. In Handbook of Automated Reasoning, vol. I, chapter 7, pp. 371–443. Elsevier Science, 2001. [26] V. Prevosto and U. Waldmann. SPASS+T. In Proceedings of the FLoC’06 Workshop on Empirically Successful Computerized Reasoning, 3rd International Joint Conference on Automated Reasoning, number 192 in CEUR Workshop Proceedings, pp. 19–33, 2006. [27] G. Reger, N. Bjørner, M. Suda, and A. Voronkov. AVATAR modulo theories. In GCAI 2016. 2nd Global
Conference on Artificial Intelligence, vol. 41 of EPiC Series in Computing, pp. 39–52. EasyChair, 2016. [28] G. Reger and M. Suda. Set of support for theory reasoning. In IWIL-2017, 2017. To appear. [29] G. Reger, M. Suda, and A. Voronkov. Playing with AVATAR. In Automated Deduction - CADE-25: 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, pp. 399–415. Springer International Publishing, 2015. [30] G. Reger, M. Suda, and A. Voronkov. Finding finite models in multi-sorted first-order logic. In Theory and Applications of Satisfiability Testing – SAT 2016: 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings, pp. 323–341. Springer International Publishing, 2016. [31] G. Reger, M. Suda, and A. Voronkov. New techniques in clausal form generation. In GCAI 2016. 2nd Global
Conference on Artificial Intelligence, vol. 41 of EPiC Series in Computing, pp. 11–23. EasyChair, 2016. [32] G. Reger, M. Suda, and A. Voronkov. Unification with abstraction and theory instantiation in saturation-based reasoning. In IWIL-2017, 2017. To appear. [33] A. Reynolds. Conflicts, models and heuristics for quantifier instantiation in SMT. In Vampire 2016. Proceedings of the 3rd Vampire Workshop, vol. 44 of EPiC Series in Computing, pp. 1–15. EasyChair, 2017. [34] A. Reynolds, C. Tinelli, and L. de Moura. Finding conflicting instances of quantified formulas in SMT.
In Proceedings of the 14th Conference on Formal Methods in Computer-Aided Design, FMCAD ’14, pp. 31:195–31:202. FMCAD Inc, 2014. [35] S. Schulz. System Description: E 1.8. In Proc. of the 19th LPAR, Stellenbosch, vol. 8312 of LNCS. Springer, 2013. [36] G. Sutcliffe. The TPTP problem library and associated infrastructure. J. Autom. Reasoning, 43(4):337–362, 2009. [37] G. Sutcliffe. The 8th IJCAR automated theorem proving system competition - CASC-J8. AI Commun., 29(5):607–619, 2016. [38] A. Voronkov. AVATAR: The architecture for first-order theorem provers. In Computer Aided Verification, vol. 8559 of Lecture Notes in Computer Science, pp. 696–710. Springer International Publishing, 2014.