Awards
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.