Awards

 

CASC-24 (2013)

  1. 3rd place in FOF (after two versions of Vampire). 2nd place in LTB, winning the ISA subcategory. MaLaReA, based on E, won LTB. The first 5 systems in THF used E as a subsystem.

CASC-J6 and CASC@Turing (2012)

  1. 3rd in FOF and FOF@Turing, each time beaten only by E-MaLeS (a strategy learning system based on E) and Vampire. MaLaReA and PS-E, both based on E, won 1st and 3rd place in MZR@Turing, and E won 3rd place in LTB.

CASC-23 (2011)

   1st in CNF, second in UEQ and LTB. E-MaLeS (a strategy learning system

   based on E) beat E itself by a very small margin for 3rd place in FOF, after

   two versions of Vampire.

CASC-J5 (2010)

    2nd in FOF, 3rd in CNF, special award as “best overall”

CASC-22 (2009)

    2nd in FOF, 3rd in FNT, 3rd in CNF, 3rd in SAT, 2nd in UEQ

CASC-J4 (2008)

    2nd in FOF, 3rd in CNF, 3rd in UEQ

CASC-21 (2007)

    3rd  in CNF, 3rd in UEQ

CASC-J3 (2006)

    2nd in FOF, 3rd in CNF

CASC-20 (2005)

    3rd in MIX, 3rd in FOF

CASC-J2 (2004)

    3rd in MIX

    With E-SETHEO: 2nd in MIX, 3rd in FOF, 2nd in EPR, 3rd in UEQ

CASC-19 (2003)

    3rd in MIX, 3rd in UEQ

    With E-SETHEO: 2nd in MIX, 3rd in FOF, 3rd in EPR

CASC-18 (2002)

    With E-SETHEO: 3rd in UEQ, 2nd in FOF, 1st in EPR

CASC-JC (2001)

    3rd in MIX, 3rd in UEQ

    With E-SETHEO: 1st in MIX, 3rd SAT, 1st in FOF, 1st in EPR

CASC-17 (2000)

    1st in MIX

    With E-SETHEO:  2nd in MIX, 1st in SEM


CASC Performance

E has participated on its own or as part of E-SETHEO in all CASC competitions since 1999. It has entered in nearly all first-order categories, including both proof and disproof categories. E has also been used as a subcomponent by some other competitors. As a stand-alone system, it has done well in the full first-order, clause normal form, and unit equality proof categories, often coming in as one of the top three provers in all these categories.