Awards

 

CASC-25 (2015)

  1. 3rd place in FOF (after two versions of Vampire), and this time beating ET. 3nd place in LTB. MaLaReA, based on E, achieved 2nd place in LTB. As previously, to our knowledge all higher-order provers in the competition used E as a subsystem.

CASC-J7 (2014)

  1. Standalone E achieved 3rd place in FOF, being beaten by Vampire and ET, a meta-system based on E.

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, routinely coming in as one of the top three provers in all these categories.