System on TMTP

This interface is for processing models.
If you want to solve problems, use the SystemOnTPTP interface.
If you want to process solutions more generally, use the SystemOnTSTP interface.

The TPTP Needs Money   See the TPTP web page for details, benefits, and process of making a donation.

Model

 TMTP Model (e.g., KRS176+1.005-FMo)
Browse TMTP
Formulae to interpret
  TMTP Formulae (Model example)
 Local file to upload
  URL to fetch from
Output mode
 Result
 Progress
 System
 Everything
Extras (Nothing else)
 SOnTMTP
Our server does not output results until all tasks are completed. Be patient while the systems do their thing. Results are presented using the SZS problem status ontology.
System CPU s Transform Format Command Application
 BNFParser 0.0  s Checks syntax according to BNF, for TH0 TF1 TF0 FOF CNF
 BNFParserDrill 0.0  s Checks syntax according to BNF, producing user interface, for TH0 TF1 TF0 FOF CNF
 BNFParserTree 0.0  s Checks syntax according to BNF, producing parse tree, for TH0 TF1 TF0 FOF CNF
 TPTP2JSON 0.1  s Converts to JSON, for FOF CNF
 TPTP4X 0.0  s Utility for transforming and formatting