System before TPTP

This interface is for preparing problems.
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.

Problem

 TPTP Problem (e.g., SYN054-1)
Browse TPTP

TPTP2T problem and solution finder

 Input Formulae (FOF example, CNF example)
 Local file to upload
  URL to fetch from
Input is in format
Output mode
 Result
 Progress
 System
 Everything
Extras (Nothing else)
 SB4TPTP
 SoTPTP
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
 CheckTyping 0.0  s Checks all symbols are typed, for TH0 TF0
 ECNF 3.0.04  s Converts FOF to CNF, for FOF
 EGround 3.0.04  s Grounds a set of EPR clauses, for CNF_EPR
 ESelect 3.0.04  s Axiom selection, for FOF CNF
 FlotterOnTPTP 1.3  s Converts to CNF, for FOF
 GetSymbols 0.0  s Extracts the symbols in formulae
 Horn2UEQ 0.4.1  s Converts Horn to UEQ, for FOF CNF
 Isabelle 2FOF  s Converts to FOF, for TH0 TF0 FOF CNF
 Isabelle 2TF0  s Converts to TF0, for TH0 TF0 FOF CNF
 Isabelle 2TH0  s Converts to TH0, for TH0 TF0 FOF CNF
 Monotonox 0.4.1  s Tests for monotonicity, for TF0_NAR FOF CNF
 Monotonox‑2CNF 0.4.1  s Converts to CNF, for TF0 FOF
 Monotonox‑2FOF 0.4.1  s Converts to FOF, for TF0_NAR
 NTFLET 1.8.2  s Embeds NTF in TFF or THF, for NTF
 Prophet 0.0  s Axiom selection
 Saffron 4.5  s Converts to DLF, for CNF
 SPCForProblem 1.0  s Computes the SPC, for NTF THF TXF TFF FOF CNF
 TPII 0.0  s Interpreter for TPI language
 TPTP2JSON 0.1  s Converts to JSON, for FOF CNF
 TPTP2SMT2 1.0.5  s Converts to SMT2, for TH0 TF0 FOF CNF
 TPTP2X 0.0  s Utility for transforming and formatting
 TPTP4X 0.0  s Utility for transforming and formatting
 TwHelFTC 0.0  s Type check based on LF, for TH0 TF0 TF1
 VCNF 4.8  s Converts to CNF, for FOF
 VSelect 4.4  s Axiom selection
 Why3‑FOF 0.85  s Converts to FOF, for TF1
 Why3‑TF0 0.85  s Converts to TF0, for TF1