TSTP Solutions

Introduction
- TSTP solutions use the TPTP Format for Derivations and TPTP Format for Finite Interpretations
- Standard format header provides documentation
Example: EP 1.0pre's solution for SET876+1
Header fields
- System an problem identification and description
  - File - system name and version
  - Problem - problem name and releases
  - Transform - problem transformations done for system
  - Format - input format prepared for system
  - Command - system command line
- Resource information
  - Computer - fully qualified computer name
  - Model - computer model
  - CPU - CPU type and speed
  - Memory - memory per CPU
  - OS - operating system information
  - CPULimit - CPU time limit imposed
  - Date - date and time solution was created
- Status and syntax
  - Result - SZS status of the problem
  - Output - SZS output type
  - Verified - not in use
  - Statistics - statistics about the output
- General information
  - Comments - free format comments
Formulae as for TPTP Problems