System on TSTP
(This interface is for processing solutions. 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.
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
)
Insert problem here
Local file to upload
URL to fetch from
Solution is in
TPTP
EQP
Otter
SPASS
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
Time Limit
Transform
Format
Command
AGInTRater 0.0
s
BNFParser 0.0
s
BNFParserDrill 0.0
s
BNFParserTree 0.0
s
GDV 0.0
s
IDV 0.0
s
Otterfier 0.0
s
ProofSummary 0.0
s
tptp4X 0.0
s
YuTV 0.0
s