Problem Lists

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

The problems for the CADE-15 ATP System Competition were chosen from TPTP v2.1.0, as described in the Competition Design.

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

- HNE category (Horn with No Equality) in the MIX division
- HEQ category (Horn with some Equality) in the MIX division
- NNE category (Non-Horn with No Equality) in the MIX division
- NEQ category (Non-Horn with some Equality) in the MIX division
- PEQ category (Pure Equality) in the MIX division
- UEQ division (Unit Equality)
- SAT division (Satisfiable)
- FEQ category (FOF with Equality) in the FOF Division
- FNE category (FOF with No Equality) in the FOF Division

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

- HNE category (Horn with No Equality) in the MIX division
- HEQ category (Horn with some Equality) in the MIX division
- NNE category (Non-Horn with No Equality) in the MIX division
- NEQ category (Non-Horn with some Equality) in the MIX division
- PEQ category (Pure Equality) in the MIX division
- UEQ division (Unit Equality)
- SAT division (Satisfiable)
- FEQ category (FOF with Equality) in the FOF Division
- FNE category (FOF with No Equality) in the FOF Division