Technische Universität München, Fakultät für Informatik
Lehrstuhl Informatik IV, Research Group Automated Reasoning

E and E-SETHEO -- Trophies

The CASC theorem proving competition has been held annually since 1996. It compares the performance of sound, fully automatic, classical 1st order ATP systems. Various versions of our provers have successfully participated since the very first CASC, held at CADE-13 in 1996).


2010 Best prover overall trophy

After several years of good showing accros the board, E was recognized as the "overall best" prover in the 2010 CASC-J5. It came in second in FOF and third (after two version of Vampire) in CNF, 4th in UEQ, 5th in FNT, and participated successfully in LTB and EPR.


2001 Trophies for FOF, MIX and EPR

From left to right: FOF, MIX assurance, EPR

The FOF division

The FOF division compared the performance of theorem provers on theorems spcified in full first-order format. In 2001, it was won by E-SETHEO, which beat last year's winner Vampire.

The MIX division

E-SETHEO and Vampire shared the win in the MIX division assurance class. In this division, theorems are specified as (unsatisfiable) problems in clause normal form. Provers only have to find a proof, they do not need to present a proof object. This year, the first 6 places in a field of 11 were taken by different versions of E-SETHEO, E, and Vampire. In the proof classs, where provers have to generate an explicit proof object, E won 3rd place after two versions of Vampire.

The EPR division

In EPR, provers have to determine the status (satisfiable or unsatisfiable) of near-propositional problems specifies in clause normal form. This category was won by E-SETHEO. The runner-up, PizEAndSato, is also based on E's library (and SATO).

Other successes

In the UEQ division (unit-equational problems), E won a very good third place after two versions of Waldmeister. Similarly, in the SAT division, E-SETHO achieved a third place after two versions of Gandalf optimized for model finding.


2000 Trophies for MIX and SEM

From left to right: MIX and SEM

The MIX division

In 2000, E managed to beat E-SETHEO by a hair's breadth (well, by an average of 80 seconds per problem...) to snatch the trophy for the MIX division. E was particularly strong on Horn problems, winning both the HEQ and the HNE subdivisions, as well as PEQ (purely equational non-unit problems).

The SEM division

The SEM division, first-order probems from a single semantic domain (SET theory) was won by E-SETHEO.

Other successes

E-SETHEO achieved a third place in the FOF division in 2000. It did not enter the SAT division.
Stephan Schulz,, 20.8.2001