The CADE ATP System Competition

Systems, Division lists, and Entrants


System Version Divisions Entrant (Associates) Entrant's Affiliation Entry date Description Solutions Source
CSE 1.0 FOF Feng Cao (Yang Xu, Jun Liu,
Shuwei Chen, Xiaomei Zhong,
Peng Xu, Qinghua Liu, Huimin Fu,
Xiaodong Guan, Zhenming Song)
Southwest Jiaotong University
(Jun Liu - Ulster University)
06/06/18 Description Samples
CSE 1.1 FOF Feng Cao (Yang Xu, Jun Liu,
Shuwei Chen, Xingxing He,
Xiaomei Zhong, Peng Xu,
Qinghua Liu, Huimin Fu, Jian
Zhong, Guanfeng Wu, Xiaodong
Guan, Zhenming Song)
Southwest Jiaotong University
(Jun Liu - Ulster University)
06/06/18 Description Samples
CSE_E 1.0 FOF Feng Cao (Yang Xu, Stephan
Schulz, Jun Liu, Shuwei Chen,
Xingxing He, Xiaomei Zhong,
Peng Xu, Qinghua Liu, Huimin Fu,
Jian Zhong, Guanfeng Wu,
Xiaodong Guan, Zhenming Song)
Southwest Jiaotong University
(Stephan Schulz - DHBW Stuttgart,
Jun Liu - Ulster University)
06/06/18 Description Samples
CVC4 1.6pre TFA FOF FNT Andrew Reynolds (Clark Barrett,
Cesare Tinelli)
University of Iowa 12/06/18 Description Samples Source
E 2.2pre FOF FNT EPR LTB Stephan Schulz DHBW Stuttgart 19/04/18 Description Samples
Geo-III 2018C FOF FNT EPR Hans de Nivelle Nazarbayev University 26/05/18 Description Samples
Grackle 0.1 LTB Jan Jakubuv (Cezary Kaliszyk,
Stephan Schulz, Josef Urban)
Czech Technical University
in Prague
11/06/18 Description Samples
iProver 2.6 EPR (demo) CASC CASC-26 winner 17/08/17 Description Samples Source
iProver 2.8 FOF FNT EPR LTB Konstantin Korovin (Julio Cesar
Lopez Hernandez)
The University of Manchester 11/06/18
leanCoP 2.2 FOF Jens Otten University of Oslo 15/06/18 Description Samples Source
LEO-II 1.7.0 THF Alexander Steen
(Christoph Benzmüller)
Freie Universität Berlin 27/05/18 Description Samples Source
Leo-III 1.3 THF
FOF, EPR (demo)
Alexander Steen, Christoph
Benzmüller, Max Wisniewski
Freie Universität Berlin 24/05/18 Description Samples
MaLARea 0.7 LTB Josef Urban (Jan Jakubuv,
Cezary Kaliszyk, Stephan Schulz)
Czech Technical University
in Prague
11/06/18 Description Samples
nanoCoP 1.1 FOF Jens Otten University of Oslo 15/06/18
Princess 170717 TFA Philipp Rümmer (Peter Backeman,
Aleksandar Zeljic)
Uppsala University 15/06/18 Description Samples Source
Prover9 2009‑11A FOF (demo) CASC
(William McCune, Bob Veroff)
CASC
(University of New Mexico)
17/08/17 Description Samples Source
Satallax 3.2 THF (demo) CASC CASC-26 winner 17/08/17 Description Samples Source
Satallax 3.3 THF Michael Färber (Chad Brown) University of Innsbruck 19/06/18 Description Samples
Twee 2.2 FOF Nick Smallbone (Koen Claessen) Chalmers University of Technology 06/06/18 Description Samples
Vampire 4.0 LTB (demo) CASC CASC-26 winner 17/08/17 Description Samples Source
Vampire 4.1 TFA FNT (demo) CASC CADE-26 winner 17/08/17 Description Samples Source
Vampire 4.2 FOF (demo) CASC CASC-26 winner 17/08/17 Description Samples Source
Vampire 4.3 TFA FOF FNT EPR
LTB
Giles Reger (Martin Suda, Andrei
Voronkov, Evgeny Kotelnikov,
Martin Riener, Laura Kovacs)
University of Manchester 11/06/18


Systems in the Competition Divisions

THF TFA FOF FNT EPR LTB
LEO-II 1.7.0
Leo-III 1.3
Satallax 3.3
CVC4 1.6pre
Princess 170717
Vampire 4.3
CSE 1.0
CSE 1.1
CSE_E 1.0
CVC4 1.6pre
Geo-III 2018C
E 2.2pre
iProver 2.8
leanCoP 2.2
nanoCoP 1.1
Twee 2.2
Vampire 4.3
CVC4 1.6pre
Geo-III 2018C
E 2.2pre
iProver 2.8
Vampire 4.3
Geo-III 2018C
E 2.2pre
iProver 2.8
Vampire 4.3
E 2.2pre
Grackle 0.1
iProver 2.8
MaLARea 0.7
Vampire 4.3

Systems in the Demonstration Division

THF TFA FOF FNT EPR LTB
Satallax 3.2
Vampire 4.1
Leo-III 1.3
Prover9 2009‑11A
Vampire 4.2
Vampire 4.1
iProver 2.6
Leo-III 1.3
Vampire 4.0


Personal Details

Who System T-Shirt Rego Here? Dinner? Notes
Feng Cao CSE 1.0 XLarge + XXL Paid
Hans de Nivelle Geo-III 2018C Small Paid
Michael Färber Satallax 3.3 Medium $120
Martin Giese Panelist Large Free
Jan Jakubuv Grackle 0.1 Medium $25 No No Josef to pay
Konstantin Korovin iProver 2.8 Medium Paid
Laura Kovacs Vampire 4.3 Medium Paid
Julio Cesar Lopez Hernandez iProver 2.8 Medium Paid
Aart Middeldorp Panelist XLarge Free
Jens Otten lenaCoP 2.2, nanoCoP 1.1 Small $120
Leo Lebedev Woltzenlogel Paleo Future entrant Baby $25
Florian Rabe Panelist Medium Free
Giles Reger Vampire 4.3 Large Paid
Andrew Reynolds CVC4 1.6pre Large $120
Philipp Rümmer Princess 170717 Medium Paid
Stephan Schulz E 2.2pre XXLarge Paid
Nick Smallbone Twee 2.2 XLarge Paid
Alexander Steen LEO-II 1.7.0, Leo-III 1.3 Medium Paid
Geoff Sutcliffe Organizer XLarge Free Yes Yes
Josef Urban MaLARea 0.7 XLarge $145
Andrei Voronkov Vampire 4.3 Large Paid
Charlotte Weidenbach Future entrant Baby (35") Paid No No