Problem Lists

The shortened, randomized, and formatted problems, precisely as used in the competition, are all available.

The problems for the CADE-14 ATP System Competition were chosen from TPTP v2.0.0, as described in the Call for Participation.

The **eligible** problems in each division were as follows:

- Horn with No Equality category in the MIX division
- Horn with Equality category in the MIX division
- non-Horn with No Equality category in the MIX division
- non-Horn with Equality category in the MIX division
- Unit Equality (UEQ) Division
- Satisfiable (SAT) Division
- First Order Form (FOF) Division

The **selected** problems in each division were as follows:

- Horn with No Equality category in the MIX division
- Horn with Equality category in the MIX division
- non-Horn with No Equality category in the MIX division
- non-Horn with Equality category in the MIX division
- Unit Equality (UEQ) Division
- Satisfiable (SAT) Division
- First Order Form (FOF) Division