Problem Selection

Presentation of Problems

• TPTP format (Underlying ideas)
• Rename non-defined symbols
• Randomly reorder formulae, connective arguments, equality terms
• Allow use of formula type information

Number of Problems

• Minimal number of problems determined by confidence requirements

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

Selection of Problems

• Random from eligible, based on panel seed
• Biased towards 50% unseen problems
• Constrained to avoid too many very similar problems