- Darwin 1.3 (CASC-J3 EPR division winner)
- Darwin 1.4.1
- FM-Darwin 1.4.1
- E and EP 0.999
- E-KRHyper 1.0
- Equinox 1.2
- Fampire 1.3
- Geo 2007f
- leanCoP 2.0
- ileanCoP 1.2
- iProver 0.2
- Metis 2.0
- Muscadet 2.7
- Otter 3.3
- Paradox 1.3 (CASC-J3 SAT division winner)
- Paradox 2.2
- Vampire 8.1 (CASC-J3 FOF and CNF divisions winner)
- Vampire 9.0
- Waldmeister 806 (CASC-J3 UEQ division winner)

The current version of Darwin implements first-order versions of unit propagation inference rules analogously to a restricted form of unit resolution and subsumption by unit clauses. To retain completeness, it includes a first-order version of the (binary) propositional splitting inference rule.

Proof search in Darwin starts with a default interpretation for a given clause set, which is evolved towards a model or until a refutation is found.

Improvements to the previous version include additional preprocessing steps, less memory requirements, and lemma learning [BFT06b].

Darwin is implemented in OCaml and has been tested under various Linux distributions. It is available from:

http://goedel.cs.uiowa.edu/Darwin/

The current version of Darwin implements first-order versions of unit propagation inference rules analogously to a restricted form of unit resolution and subsumption by unit clauses. To retain completeness, it includes a first-order version of the (binary) propositional splitting inference rule.

Proof search in Darwin starts with a default interpretation for a given clause set, which is evolved towards a model or until a refutation is found.

Darwin is implemented in OCaml and has been tested under various Linux distributions. It is available from:

http://goedel.cs.uiowa.edu/Darwin/

For each domain size the problem is transformed into an equisatisfiable function-free clause set, which is decided by the Darwin prover [BFT06a].

Like Paradox, the system uses clause splitting, term definitions, static symmetry reduction, sort inference, and lemmas. In contrast, clause splitting and term definitions are only applied in a restricted way, that is for variable disjunct clause and ground terms, as ground instantiation is not performed and thus the exponential increase in the size of the clause set does not happen.

FM-Darwin is available from:

http://goedel.cs.uiowa.edu/Darwin/

The first-order clausal problem is transformed into a decidable logic, here function-free clause logic. Then, the system tries to find a finite domain model for sizes 1 .. n. A given domain is encoded by adding the axioms of totality and functionality for the symbols which have been converted from function to predicate symbols, such that any finite model of the original problem can be translated into a model of the transformed problem, and vice versa.

Like Paradox, FM-Darwin is a complete method for function-free clause sets, and can also detect unsatisfiability if the totality axioms are not used in a refutation.

Institut für Informatik, Technische Universität, Germany

E is based on the DISCOUNT-loop variant of the *given-clause*
algorithm, i.e. a strict separation of active and passive facts.
Proof search in E is primarily controlled by a literal selection
strategy, a clause evaluation heuristic, and a simplification
ordering. The prover supports a large number of preprogrammed literal
selection strategies, many of which are only experimental. Clause
evaluation heuristics can be constructed on the fly by combining
various parameterized primitive evaluation functions, or can be
selected from a set of predefined heuristics. Supported term orderings
are several parameterized instances of Knuth-Bendix-Ordering (KBO) and
Lexicographic Path Ordering (LPO).

The prover uses a preprocessing step to convert formulas in full first order format to clause normal form. This step may introduce (first-order) definitions to avoid an exponential growth of the formula. Preprocessing also unfolds equational definitions and performs some simplifications on the clause level.

The automatic mode determines literal selection strategy, term ordering, and search heuristic based on simple problem characteristics of the preprocessed clausal problem.

EP 0.999 is just a combination of E 0.999 in verbose mode and a proof analysis tool extracting the used inference steps.

The program has been successfully installed under SunOS 4.3.x, Solaris 2.x, HP-UX B 10.20, MacOS-X, and various versions of Linux. Sources of the latest released version are available freely from:

EP 0.999 is a simple Bourne shell script calling E and the postprocessor in a pipeline.http://www.eprover.org

E distinguishes problem classes based on a number of features, all of which have between 2 and 4 possible values. The most important ones are:

- Is the most general non-negative clause unit, Horn, or Non-Horn?
- Is the most general negative clause unit or non-unit?
- Are all negative clauses unit clauses?
- Are all literals equality literals, are some literals equality literals, or is the problem non-equational?
- Are there a few, some, or many clauses in the problem?
- Is the maximum arity of any function symbol 0, 1, 2, or greater?
- Is the sum of function symbol arities in the signature small, medium, or large?

For classes above a threshold size, we assign the absolute best heuristic to the class. For smaller, non-empty classes, we assign the globally best heuristic that solves the same number of problems on this class as the best heuristic on this class does. Empty classes are assigned the globally best heuristic. Typically, most selected heuristics are assigned to more than one class.

EP 0.999 will be hampered by the fact that it has to analyse the
inference step listing, an operation that typically is about as
expensive as the proof search itself. Nevertheless, it should be
competitive among the FOF^{*} and CNF^{*} systems.

Universität Koblenz-Landau, Germany

An E-hyper tableau is a tree whose nodes are labeled with clauses and which is built up by the application of the inference rules of the E-hyper tableau calculus. The calculus rules are designed such that most of the reasoning is performed using positive unit clauses. A branch can be extended with new clauses that have been derived from the clauses of that branch.

A positive disjunction can be used to split a branch, creating a new branch for each disjunct. No variables may be shared between branches, and if a case-split creates branches with shared variables, then these are immediately substituted by ground terms. The grounding substitution is arbitrary as long as the terms in its range are irreducible: the branch being split may not contain a positive equational unit which can simplify a substituting term, i.e. rewrite it with one that is smaller according to a reduction ordering. When multiple irreducible substitutions are possible, each of them must be applied in consecutive splittings in order to preserve completeness.

Redundancy rules allow the detection and removal of clauses that are redundant with respect to a branch.

The hyper extension inference from the original hyper tableau calculus is equivalent to a series of E-hyper tableau calculus inference applications. Therefore the implementation of the hyper extension in KRHyper by a variant of semi-naive evaluation [Ull89] is retained in E-KRHyper, where it serves as a shortcut inference for the resolution of non-equational literals.

The system accepts clause input in the TPTP-supported Protein-format. E-KRHyper operates on an E-hyper tableau that is represented by linked node records. A layered discrimination-tree based index provides access to the clauses in the tableau and supports backtracking.http://www.uni-koblenz.de/~bpelzer/ekrhyper

Chalmers University of Technology, Sweden

- Give all ground clauses in the problem to a SAT solver.
- Run the SAT-solver.
- If a contradiction is found, we have a proof and we terminate.
- If a model is found, we use the model to indicate which new ground instantiations should be added to the SAT-solver.
- Goto 2.

Charles University of Prague, Czech Republic

University of Wroclaw, Poland

FORALL x1, ..., xn [ A1 /\ ... /\ Ap /\ v1 != w1 /\ ... /\ vq != wq -> Z(x1,...,xn) ].The

`Z(x1,...,xn)` must have one of the following three forms:

- The constant
`FALSE`. - A disjunction
`B1 \/ ... \/ Br`. The atoms`Bk`must be non-equality atoms. The arguments of the atoms`Bk`are among the variables`x1, ..., xn`. There are no function symbols, and no constants in the atoms`Bk`. - An existential quantification
`EXISTS y B`.`y`is a variable distinct from`x1,...,xn`.`B`is an atom which has all arguments among`x1,...,xn,y`. There are no function symbols and constants in`B`.

Geo accepts formulas either in its own syntax or in TPTP-syntax. Because CNF has no special status for Geo, TPTP-formulas in CNF form are treated as ordinary first-order formulas.

During search, Geo searches for a model of the geometric formulas by a combination of backtracking and learning. Whenever it cannot extend an interpretation into a model, Geo learns a new rule of Type 1, which ensures that Geo will not explore similar models in the future.

In case Geo finds a finite model, it simply prints the model. In case no model exists, it will eventually learn the rule -> FALSE, so that it is able to output a proof.

The final aim of geometric resolution, and of Geo, is to obtain a prover that is both good at finding proofs, and at finding finite models.

** Differences with last year (2006) **

- Geo2007f has lemma simplification. Learnt lemmas are used to simplify each other. In addition, inductive consequences of the initial rules are used as simplification rules.
- The heuristics for rule selection have been improved.

University of Potsdam, Germany

http://www.leancop.de

*Acknowledgments:
Thomas Raths contributed to the development of
leanCoP 2.0 by performing comprehensive
benchmark tests on several problem libraries.*

University of Potsdam, Germany

http://www.leancop.de/ileancop

*Acknowledgments:
Thomas Raths contributed to the development of
ileanCoP by performing comprehensive
benchmark tests on several problem libraries.*

The University of Manchester, England

iProver successively instantiates a given set of clauses, and uses a ground SAT solver for checking whether the current ground abstraction of clauses is satisfiable. If the ground solver finds unsatisfiability then the prover terminates, proving unsatisfiability of the initial set of clauses; otherwise the model for ground clauses is used to guide further instantiations. The saturation process is implemented as a modification of a given clause algorithm. We use non-perfect discrimination trees for the unification index. The following redundancy eliminations are implemented: blocking non-proper instantiations; dismatching constraints [GK04]; resolution-based simplifications; propositional-based simplifications, and removing duplicates. Equality is dealt with (internally) by adding the necessary axioms of equality.

Oxford University, UK

Experiments with various first order calculi
[Hur03] have shown a *given clause
algorithm* and ordered resolution to best suit this application,
and that is what Metis 2.0 implements.
Since equality often appears in higher order
logic goals, Metis 2.0 also implements the ordered paramodulation
calculus.

In addition to standard size and distance measures, Metis 2.0 uses
finite models to weight clauses in the *Waiting* set. When
integrated with higher order logic, a finite model is manually
constructed to interpret standard functions and relations in such a
way as to make many axioms true and negated goals false. Non-standard
functions and relations are interpreted randomly. Since it is part of
the CASC competition rules that standard functions and relations are
obfuscated, Metis 2.0 will back-off to interpreting all functions and
relations randomly (except equality).

Metis 2.0 is free software, released under the GPL. It can be downloaded from:

http://www.gilith.com/software/metis

Testing on previous UEQ problem sets has shown Metis to be weak on equality problems, so I expect Metis 2.0 to perform relatively worse on the equality divisions, particularly UEQ.

Université René Descartes (Paris 5), France

http://www.math-info.univ-paris5.fr/~pastre/muscadet/muscadet.html

The system is also able to work with second order statements. It may also receive knowledge and know-how for a specific domain from a human user; see [Pas89, Pas93]. These two possibilities are not used while working with the TPTP Library.

Argonne National Laboratory, USA

Otter 3.3 [McC03a] is an ATP system for statements in first-order (unsorted) logic with equality. Otter is based on resolution and paramodulation applied to clauses. An Otter search uses the "given clause algorithm", and typically involves a large database of clauses; subsumption and demodulation play an important role.

Otter is written in C. Otter uses shared data structures for clauses and terms, and it uses indexing for resolution, paramodulation, forward and backward subsumption, forward and backward demodulation, and unit conflict. Otter is available from:

http://www-unix.mcs.anl.gov/AR/otter/

Otter's original automatic mode, which reflects no tuning to the TPTP problems, will be used.

Otter has been entered into CASC as a stable benchmark against which progress can be judged (there have been only minor changes to Otter since 1996 [MW97], nothing that really affects its performace in CASC). This is not an ordinary entry, and we do not hope for Otter to do well in the competition.

*Acknowledgments: Ross Overbeek, Larry Wos, Bob Veroff, and
Rusty Lusk contributed to the development of Otter.*

Chalmers University of Technology and Gothenburg University, Sweden

Paradox incorporates the following features: Polynomial-time
*clause splitting heuristics*, the use of *incremental SAT*,
*static symmetry reduction* techniques, and the use of *sort
inference*.

The main differences with Paradox 1.0 are: a better SAT-solver, better memory behaviour, and a faster clause instantiation algorithm.

- Analyze the problem, finding an upper bound N on the domain size of models, where N is possibly infinite. A finite such upper bound can be found, for example, for EPR problems.
- Flatten the problem, and split clauses and simplify as much as possible.
- Instantiate the problem for domain sizes 1 up to N, applying the SAT solver incrementally for each size. Report "SATISFIABLE" when a model is found.
- When no model of sizes smaller or equal to N is found, report "CONTRADICTION".

Chalmers University of Technology, Sweden

University of Manchester, England

No system description supplied. However, see the description of Vampire 8.0 for general information. Minor changes have been made, including a bugfix in the FOF to CNF conversion.

University of Manchester, England

None supplied.

No system description supplied. However, see the description of Waldmeister 704 for general information.

- BG98
- Bachmair L., Ganzinger H. (1998),
**Equational Reasoning in Saturation-Based Theorem Proving**, Bibel W., Schmitt P.H.,*Automated Deduction, A Basis for Applications*, pp.352-397, Applied Logic Series 10, Kluwer Academic Publishers. - BFN96
- Baumgartner P., Furbach U., Niemelä I. (1996),
**Hyper Tableaux**, Alferes J., Pereira L., Orlowska E.,*Proceedings of JELIA'96: European Workshop on Logic in Artificial Intelligence*(Evora, Portugal), pp.1-17, Lecture Notes in Artificial Intelligence 1126, Springer-Verlag. - BT03
- Baumgartner P., Tinelli C. (2003),
**The Model Evolution Calculus**, Baader F.,*Proceedings of the 19th International Conference on Automated Deduction*(Miami, USA), pp.350-364, Lecture Notes in Artificial Intelligence 2741, Springer-Verlag. - BFT04
- Baumgartner P., Fuchs A., Tinelli C. (2004),
**Darwin - A Theorem Prover for the Model Evolution Calculus**, Sutcliffe G., Schulz S., Tammet T.,*Proceedings of the Workshop on Empirically Successful First Order Reasoning, 2nd International Joint Conference on Automated Reasoning*(Cork, Ireland). - BFT06a
- Baumgartner P., Fuchs A., Tinelli C. (2006),
**Implementing the Model Evolution Calculus**,*International Journal on Artificial Intelligence Tools*15(1), pp.21-52. - BFT06b
- Baumgartner P., Fuchs A., Tinelli C. (2006),
**Lemma Learning in the Model Evolution Calculus**, Hermann M., Voronkov A.,*Proceedings of the 13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning*(Phnom Penh, Cambodia), Lecture Notes in Artificial Intelligence. - BFP07
- Baumgartner P., Furbach U., Pelzer B. (2007),
**Hyper Tableaux with Equality**, Pfenning F.,*Proceedings of the 21st International Conference on Automated Deduction*(Bremen, Germany), Lecture Notes in Artificial Intelligence 4603, Springer-Verlag. - CS03
- Claessen K., Sorensson N. (2003),
**New Techniques that Improve MACE-style Finite Model Finding**, Baumgartner P., Fermueller C.,*Proceedings of the CADE-19 Workshop: Model Computation - Principles, Algorithms, Applications*(Miami, USA). - dNM06
- de Nivelle H., Meng J. (2006),
**Geometric Resolution: A Proof Procedure Based on Finite Model Search**, Furbach U., Shankar N.,*Proceedings of the 3rd International Joint Conference on Automated Reasoning*(Seattle, USA), pp.303-317, Lecture Notes in Artificial Intelligence 4130, Springer-Verlag. - deN07
- de Nivelle H. (2007),
**Redundancy for Geometric Resolution**, Ahrendt W., Baumgartner P., de Nivelle H.,*Proceedings of CADE-21 Workshop on DISPROVING - Non-Theorems, Non-Validity, Non-Provability*(Bremen, Germany). - GK03
- Ganzinger H., Korovin K. (2003),
**New Directions in Instantiation-Based Theorem Proving**, Kolaitis P.,*Proceedings of the 18th IEEE Symposium on Logic in Computer Science*(Ottawa, Canada), pp.55-64. - GK04
- Ganzinger H., Korovin K. (2004),
**Integrating Equational Reasoning into Instantiation-Based Theorem Proving**, Marcinkowski J., Tarlecki A.,*Proceedings of the 18th International Workshop on Computer Science Logic, 13th Annual Conference of the EACSL*(Karpacz, Poland), pp.71-84, Lecture Notes in Computer Science 3210. - Hur03
- Hurd J. (2003),
**First-Order Proof Tactics in Higher-Order Logic Theorem Provers**, Archer M., Di Vito B., Munoz C.,*Proceedings of the 1st International Workshop on Design and Application of Strategies/Tactics in Higher Order Logics*(Rome, Italy), pp.56-68, NASA Technical Reports NASA/CP-2003-212448. - LS01
- Letz R., Stenz G. (2001),
**Model Elimination and Connection Tableau Procedures**, Robinson A., Voronkov A.,*Handbook of Automated Reasoning*, pp.2015-2114, Elsevier Science. - Loe04
- Loechner B. (2004),
**What to Know When Implementing LPO**, Sutcliffe G., Schulz S., Tammet T.,*Proceedings of the Workshop on Empirically Successful First Order Reasoning, 2nd International Joint Conference on Automated Reasoning*(Cork, Ireland). - MW97
- McCune W.W., Wos L. (1997),
**Otter: The CADE-13 Competition Incarnations**,*Journal of Automated Reasoning*18(2), pp.211-220. - McC94
- McCune W.W. (1994),
**A Davis-Putnam Program and its Application to Finite First-Order Model Search: Quasigroup Existence Problems**, ANL/MCS-TM-194, Argonne National Laboratory, Argonne, USA. - McC03a
- McCune W.W. (2003),
**Otter 3.3 Reference Manual**, ANL/MSC-TM-263, Argonne National Laboratory, Argonne, USA. - OB03
- Otten J., Bibel W. (2003),
**leanCoP: Lean Connection-Based Theorem Proving**,*Journal of Symbolic Computation*36(1-2), pp.139-161. - OK96
- Otten J., Kreitz C. (1996),
**T-String-Unification: Unifying Prefixes in Non-Classical Proof Methods**, Miglioli P., Moscato U., Mundici D., Ornaghi M.,*Proceedings of the 5th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods*(Palermo, Italy), pp.244-20, Lecture Notes in Computer Science 1071, Springer-Verlag. - Ott05
- Otten J. (2005),
**Clausal Connection-Based Theorem Proving in Intuitionistic First-Order Logic**, Beckert B.,*Proceedings of the 14th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods*(Koblenz, Germany), pp.245-261, Lecture Notes in Artificial Intelligence 3702, Springer-Verlag. - Pas78
- Pastre D. (1978),
**Automatic Theorem Proving in Set Theory**,*Artificial Intelligence*10, pp.1-27. - Pas89
- Pastre D. (1989),
**Muscadet : An Automatic Theorem Proving System using Knowledge and Metaknowledge in Mathematics**,*Artificial Intelligence*38, pp.257-318. - Pas93
- Pastre D. (1993),
**Automated Theorem Proving in Mathematics**,*Annals of Mathematics and Artificial Intelligence*8, pp.425-447. - Pas01
- Pastre D. (2001),
**Muscadet 2.3 : A Knowledge-based Theorem Prover based on Natural Deduction**, Gore R., Leitsch A., Nipkow T.,*Proceedings of the International Joint Conference on Automated Reasoning*(Siena, Italy), pp.685-689, Lecture Notes in Artificial Intelligence 2083, Springer-Verlag. - Pas02
- Pastre D. (2002),
**Strong and Weak Points of the Muscadet Theorem Prover**,*AI Communications*15(2-3), pp.147-160. - Pas07
- Pastre D. (2007),
**Complementarity of a Natural Deduction Knowledge-based Prover and Resolution-based Provers in Automated Theorem Proving**, http://www.math-info.univ-paris5.fr/~pastre/compl-NDKB-RB.pdf. - PW07
- Pelzer B., Wernhard C. (2007),
**System Description: E-KRHyper**, Pfenning F.,*Proceedings of the 21st International Conference on Automated Deduction*(Bremen, Germany), Lecture Notes in Artificial Intelligence 4603, Springer-Verlag. - ROK07
- Raths T., Otten J., Kreitz C. (2007),
**The ILTP Problem Library for Intuitionistic Logic - Release v1.1**,*Journal of Automated Reasoning*38(1-2), pp.261-271. - Sch02
- Schulz S. (2002),
**E: A Brainiac Theorem Prover**,*AI Communications*15(2-3), pp.111-126. - Sch04a
- Schulz S. (2004),
**System Abstract: E 0.81**, Rusinowitch M., Basin D.,*Proceedings of the 2nd International Joint Conference on Automated Reasoning*(Cork, Ireland), pp.223-228, Lecture Notes in Artificial Intelligence 3097. - Sch04b
- Schulz S. (2004),
**Simple and Efficient Clause Subsumption with Feature Vector Indexing**, Sutcliffe G., Schulz S., Tammet T.,*Proceedings of the Workshop on Empirically Successful First Order Reasoning, 2nd International Joint Conference on Automated Reasoning*(Cork, Ireland). - Ull89
- Ullman J. (1989),
**Principles of Database and Knowledge-Base Bystems**, Computer Science Press, Inc.. - Wer03
- Wernhard C. (2003),
**System Description: KRHyper**, Fachberichte Informatik 14--2003, Universität Koblenz-Landau, Koblenz, Germany.