Time Limit and Problem Selection

Selection of Problems

• Minimal number of problems determined by confidence requirements

•                      Number of workstations * Time allocated
  Number of problems = ---------------------------------------
                          Number of ATP systems * Time limit
  

• Random from eligible, based on panel seed

Presentation of Problems

• Underlying ideas
• Rename symbols except equal/2
• Randomly reorder formulae, literals, equality arguments
• Remove built in established theories
• Add dependant established theories
• Output in format required by systems using tptp2X
• Allow use of formula type information
• Use dummy file names to prevent identification

Time Limit

• Minimal time limit of 180 seconds per problem
• Minimal number of problems to ensure confidence in the results

•                   Number of workstations * Time allocated
  Time limit = --------------------------------------------------
               Number of ATP systems * Minimal number of problems