Building the TMTP

Collecting Models

• Models created automatically as part of TSTP updates
• Copy "new" models from TSTP to TMTP

Model Files

• 
• Divided into domains, like the TPTP and TSTP
• Files named DDDNNNFV.MMM-SZS.m
  • DDDNNNFV is the TPTP problem name
  • MMM is the model number
  • SZS is the SZS dataform, e.g., FMo, Sat
• Header section
  • Model finder information
  • Resources given and used
  • Model properties and statistics
  • Comments
• Formula section