A competition on automated theorem proving (ATP), held during conferences on automated deduction (CADE), is described in this paper.

The CADE ATP system competition (CASC) has been held annually since 1996. CASC evaluates only ATP systems that solve problems in classical first order logic. The problem library, known as thousands of problems for theorem provers (TPTP), along with the evaluation schemes, are the foundation of CASC.

CASC is run in divisions, according to problem characteristics. The characteristics used to define the divisions and categories include:

• whether or not the problem is a theorem
• whether the problems are presented in first-order form, or in conjunctive normal form (CNF-problems)
• whether or not equality is presented in the problem
• whether or not the clauses of a CNF-problem are all Horn
• whether a problem is “really first-order” or “effectively propositional.”

Some ATP systems that include meaningful information about performance characteristics are noted in the paper. The evolution of CASC, starting from 1996, is described, paying particular attention to its design, design changes, and organization.