System before TPTP
(This interface is for preparing problems. If you want to solve problems, use the
System on TPTP
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 (
TPTP FOF Example
,
TPTP CNF Example
)
Insert problem here
Local file to upload
URL to fetch from
Input is in
TPTP
DFG
LADR
Mizar
Otter
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
Time Limit
Transform
Format
Command
BNFParser 0.0
s
BNFParserDrill 0.0
s
BNFParserTree 0.0
s
ECNF
1.0
s
FlotterOnTPTP 1.3
s
Prophet 0.0
s
tptp2X 0.0
s
tptp4X 0.0
s
TwHelFTC 0.0
s
