Awards

[CASC Trophies]
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.
[CASC-29 Trophy]
[CASC J11 Medal]
[CASC J10 Trophies]
[CASC 27 Trophy]
[CASC 23 Trophy]
[CASC J5 Trophy]

CASC Performance

CASC-29 (2023)
First place in SLH, second place in FOF, third places in UEQ, THF and FNT.
CASC-J11 (2022)
First place in SLH, second place in THF, FOF, UEQ, third place in LTB.
CASC-28 (2021)
First place in SLH (as Ehoh), second place in UEQ, third in LTB.
CASC-J10 (2020)
First place in UEQ and LTB, third in FOF (after Vampire and Enigma, which is based on E).
CASC-27 (2019)
First place in UEQ, second place in FOF and LTB. The winners of LTB (LEO-III) and THF (Satallax) both used E as a component.
CASC-J9 (2018)
3rd place in FOF (after Vampire and CSE_E, based on E). MaLaReA, based on E, won first place in LTB. As in several previous years, all systems in the "Higher-order Theorems" category use E.
CASC-26 (2017)
3rd place in FOF (after two versions of Vampire). MaLaReA, based on E, achieved 3rd place in LTB.
CASC-J8 (2016)
3rd place in FOF (after two versions of Vampire), and again beating ET. 3rd place in LTB. 3rd place in EPR, after iProver and Vampire.
CASC-25 (2015)
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)
Standalone E achieved 3rd place in FOF, being beaten by Vampire and ET, a meta-system based on E.
CASC-24 (2013)
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)
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.
Stephan Schulz, schulz@eprover.org