System on TSTP
This interface is for processing solutions. If you want to solve problems, use the SystemOnTPTP interface. If you want to process models specifically, use the SystemOnTMTP interface.
The TPTP Needs Money   See the TPTP web page for details, benefits, and process of making a donation.

Solution

 TPTP Problem (e.g., SYN054-1)
Browse TPTP
& TSTP System (e.g., Otter---3.3)
Browse TSTP

TPTP2T problem and solution finder

 TSTP Formulae (Refutation example, Model example)
 Local file to upload
  URL to fetch from
Solution is in format
Output mode
 Nothing (except extras)
 Result
 Progress
 System
 Everything
Extras (Nothing else)
 SoTSTP
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
 AGInTRater 0.0  s Rates proof formulae for interestingness, for
 AGMV 1.0  s Model verifier
 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
 GDV 0.0  s Derivation verifier, for TH0 TF0 FOF CNF
 IDV 0.0  s Interactive derivation viewer
 IIV 0.0  s Interactive interpretation viewer
 InterpretByATP 0.0  s Evaluates formulae against a model, between SZS lines (ask Geoff)
 OAESys 0.0  s Extracts answers from derivation
 OAFSys 0.0  s Extracts answers from derivation, with reproving
 PProofSummary 0.0  s Summarizes proof in Prolog format
 ProofSummary 0.0  s Summarizes proof
 TPTP2JSON 0.1  s Converts to JSON, for FOF CNF
 TPTP4X 0.0  s Utility for transforming and formatting