The CADE-13 ATP System Competition
The Design of the CADE-13 ATP System Competition
The Procedures of the CADE-13 ATP System Competition
Barcelona
CLIN-E : Smallest Instance First Hyper-Linking
CLIN-S : A Semantically Guided First-Order Theorem Prover
DISCOUNT : A Distributed and Learning Equational Prover
Gandalf
LINUS : A Link Instantion Prover with Unit Support
Otter : The CADE-13 Competition Incarnations
RRTP : A Replacement Rule Theorem Prover
Satchmo : The Compiling and Functional Variants
SETHEO and E-SETHEO : The CADE-13 Systems
SPASS : Version 0.49
SPTHEO : A Parallel Theorem Prover
Violet
WALDMEISTER : High-Performance Equational Deduction
The Results : of the CADE-13 ATP System Competition
Conclusions about the CADE-13 ATP System Competition