System on TSTP

This interface is for processing solutions.
If you want to solve problems, use the SystemOnTPTP 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
Continue to
 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, for NX0 TX0 TF0 FOF
 BNFParser 0.0  s Checks syntax according to BNF, for TH1 TH0 TF1 TF0 FOF CNF
 BNFParserDrill 0.0  s Checks syntax according to BNF, producing user interface, for TH1 TH0 TF1 TF0 FOF CNF
 BNFParserTree 0.0  s Checks syntax according to BNF, producing parse tree, for TH1 TH0 TF1 TF0 FOF CNF
 GAPT 2.16.0  s Derivation verifier, for FOF CNF
 GDV 1.0  s Derivation verifier, for NH0 NX0 TH0 TX0 TF0 FOF CNF
 GDV‑LP 1.0  s Derivation verifier for LambdaPi format, for TH0 TF0 FOF CNF
 IDV 1.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)
 PProofSummary 0.0  s Summarizes proof in Prolog format
 ProofSummary 0.0  s Summarizes proof
 SolutionStats 1.0  s Print solution statistics
 TPTP2JSON 0.1  s Converts to JSON, for FOF CNF
 TPTP4X 0.0  s Utility for transforming and formatting