| collected by | Geoff Sutcliffe geoff@cs.miami.edu | and | Christian Suttner suttner@informatik.tu-muenchen.de |
Since the first release of the TPTP Problem Library in 1993, many researchers have used the TPTP as an appropriate and convenient basis for ATP system evaluation. Some researchers, who have tested their ATP systems over the entire TPTP, have made their result data available. The data has been collected, and is used for determining system ratings, system recommendations, and the TPTP problem ratings. Currently we have data for the systems listed below.
-------------------------------------------------------------------------------
ATP system name : SPTHEO m256n1
People : Christian Suttner
URL : http://wwwjessen.informatik.tu-muenchen.de/~suttner/sptheo.html
References : [Sut95] Suttner (1995), Parallelization of Search-based Sy
TPTP release : v1.1.3
tptp2X flags : -f setheo (No use of clause type information)
CPU : HP 720
RAM size : 32 MByte
Operating system : HP-UX 9.X
Implementation : C and PVM. Compiler: HP-UX cc. Flags: -c -g -o
Resource limits : 20 seconds for task generation. 20 seconds per task
Settings/flags : -cons -ir -m 256 for task generation (i.e., 256 tasks
requested)
-cons -dr for task processing. 1 processor used (time
sharing)
Results format : Solns TotTime APnTime PEnWork APnWork PL m
Results values : Solns - P and number of proofs found
or TMO-Non
or ERR-Non (X), where X indicates the type of error
TotTime - Wall clock time for parallel system, with 0
communication time, in seconds
APnWork - Task generation time plus accumulated search
times (summed over all processors), in seconds
PEnTime - Number of inferences (generation + 1st proof
task)
APnWork - Accumulated number of inferences (summed over
all processors)
PL - Proof length of first proof found (not shortest)
m - Number of tasks generated
Results summary : 1329 problems (2652 in TPTP v1.1.3, 1323 since Bugfixed)
14 IAP-Non
566 TMO-Non
749 UNS-Ass
1315 tested (99%)
749 solutions
57% success, over those tested
56% success, overall
Comments : Not tested on problems known to be satisfiable
: If a proof is found in the sequential task generation
phase, CPUapn and APnWork are meaningless and marked with
"-". CPUtot and PEnWork then refer to task generation
: Some satisfiable problems were not_tested. They are
labelled "satisfiable"
: The problems with "Error" results exceeded the capacity
of some component of SETHEO
-------------------------------------------------------------------------------
ATP system name : CLIN 1.0
People : Shie-Jue Lee
URL : ftp.cs.unc.edu:pub/projects/mi/clin/prover.tar.Z
http://www.cs.unc.edu/mi/mi-provers.html
References : [Lee90] Lee (1990), CLIN: An Automated Reasoning System Us
: [LP92] Lee & Plaisted (1992), Eliminating Duplication wit
TPTP release : v1.1.3
tptp2X flags : -f sprfn (No use of clause type information)
CPU : RS/6000 550
RAM size : 512MB / 1024MB
Operating system : AIX 3.2.5
Implementation : Prolog. Compiler: ECLiPSe 3.4.5. Flags: nodbgcomp
Resource limits : 1800 seconds
Settings/flags : assign(support_list,[f]). set(slidepriority)
Maximum clause size method
Results format : Solns TotTime ModTime Clauses
Results values : Solns - P and number of proofs found
or M and number of models found
or TMO-Non
or var_lim (limit of 20 distinct variables
exceeded)
or cls_lim (limit of 1600 input clauses exceeded)
TotTime - CPU time, in seconds
Clauses - Number of clauses retained
Results summary : 1329 problems (2652 in TPTP v1.1.3, 1323 since Bugfixed)
4 ERR-Non
665 TMO-Non
651 UNS-Ass
9 SAT-Ass
1329 tested (100%)
660 solutions
50% success, over those tested
50% success, overall
Comments : CLIN automatically switches to All support and the Maximum
clause size method for propositional problems
-------------------------------------------------------------------------------
ATP system name : CLIN-E 0.35FM
People : Geoff Alexander
URL :
References : [Ale95] Alexander (1995), Proving First-Order Equality The
TPTP release : v1.1.3
tptp2X flags : -f sprfn (No use of clause type information)
CPU : RS/6000 550
RAM size : 512MB / 1024MB
Operating system : AIX 3.2.5
Implementation : C++. Compiler: IBM C Set++. Flags: -03 -qinlglue
Resource limits : 1800 seconds
Settings/flags : Forward support. Maximum clause size method
Unit literal deletion on. Unit literal subsumption on
Results format : Solns TotTime ModTime Memory Clauses
Results values : Solns - P and number of proofs found
or M and number of models found
or TMO-Non
TotTime - CPU time, in seconds
Memory - Memory used, in K
Clauses - Number of clauses retained
Results summary : 1329 problems (2652 in TPTP v1.1.3, 1323 since Bugfixed)
784 TMO-Non
536 UNS-Ass
9 SAT-Ass
1329 tested (100%)
545 solutions
41% success, over those tested
41% success, overall
Comments : CLIN-E automatically switches to All support and the Sum
clause size method for propositional problems
-------------------------------------------------------------------------------
ATP system name : CLIN-S 1.0+
People : Heng Chu
URL : ftp.cs.unc.edu:pub/projects/mi/clin-s/*
http://www.cs.unc.edu/Research/mi/mi-provers.html
References : [CP94] Chu & Plaisted (1994), Semantically Guided First-o
TPTP release : v1.1.3
tptp2X flags : -f sprfn ??
(No use of clause type information)
CPU : DEC station 5000/120
RAM size : ??
Operating system : ??
Implementation : Prolog. Compiler: Quintus. Flags: ??
Resource limits : 1000 seconds ?MEMORY?
Settings/flags : FL (Model literal filtering) on,
NP (Natural replacement on model literals) on,
TR (Simple term rewriting on model literals) off,
MP (Minimal replacement on model literals) on,
RR (Rough resolution) on,
UR (UR resolution) on
Backward support = Using the all positive model
Results format : Solns Time Rounds Clauses Backtracks
Results values : Solns - P(XX) and number of proofs found, where XX
indicates how the proof was found, one of:
HM=Hyper linking, MF=Model Finding,
RR=Rough Resolution, US=Unit Simplification,
UR=UR resolution
or M and number of models found
or TMO-Non
or ERR-Non (UNK-Non error)
or unsound_model
Time - CPU time, in seconds
Rounds - Number of hyper-linking rounds
Clauses - Number of clauses retained
Backtrack - Number of backtrackings caused by FL,NP,TR,MP,
and UR (see Settings/flags above)
Results summary : 1329 problems (2652 in TPTP v1.1.3, 1323 since Bugfixed)
78 NTT-Non
25 ERR-Non
603 TMO-Non
623 UNS-Ass
1251 tested (94%)
623 solutions
50% success, over those tested
47% success, overall
Comments : Hardware used was not constant; other similar machines
were also used
-------------------------------------------------------------------------------
ATP system name : CLIN-S 1.0-
TPTP release : v1.1.3
Settings/flags : FL (Model literal filtering) on,
NP (Natural replacement on model literals) on,
TR (Simple term rewriting on model literals) off,
MP (Minimal replacement on model literals) on,
RR (Rough resolution) on,
UR (UR resolution) on
Forward support = Using the all negative model
Results summary : 1329 problems (2652 in TPTP v1.1.3, 1323 since Bugfixed)
19 NTT-Non
28 ERR-Non
681 TMO-Non
601 UNS-Ass
1310 tested (99%)
601 solutions
46% success, over those tested
45% success, overall
Comments : See CLIN-S 1.0+
-------------------------------------------------------------------------------
ATP system name : LINUS 1.0.1
People : Reinhold Letz
URL :
References : [Let97] Letz (1997), LINUS: A Link Instantiation Prover wi
TPTP release : v1.1.3
tptp2X flags : -f setheo (No use of clause type information)
CPU : Sparc 10
RAM size : 128 Mb
Operating system : Solaris 2.4
Implementation : LISP. Compiler: Allegro Common Lisp 4.2. Flags: ??
Resource limits : 300 seconds
Settings/flags : increase_rate = 1.5 (general weighting factor)
unit_div = 2 (weighting factor for units)
non_unit_mult = 1 (weighting factor for non-units)
no dynamic clause splitting
Results format : Solns Time GroundCls UnitCls Inferences
Results values : Solns - P(X) and number of proofs found, where X = S
for proofs found at the propositional level,
X = U for proofs found by the unit module
or M and number of models found
or TMO-Non
Time - CPU time, in seconds
GroundCls - Number of ground clauses in P(S) proofs
UnitCls - Number of unit clauses in P(S) proofs
Inferences - Number of inference steps in proofs
Results summary : 1329 problems (2652 in TPTP v1.1.3, 1323 since Bugfixed)
593 TMO-Non
727 UNS-Ass
9 SAT-Ass
1329 tested (100%)
736 solutions
55% success, over those tested
55% success, overall
Comments : For unit proofs (P(U)) the number of inferences is
currently missing. In a future version of LINUS it will be
given
-------------------------------------------------------------------------------
ATP system name : DISCOUNT 2.0-GL
People : Stephan Schulz (Proof protocols, Learning)
Joerg Denzinger (Distribution concept, theory for
existentially qualified goals)
Werner Pitz (Implementation of inference engine and
distribution scheme)
Martin Kronenburg (Planning component, his domain
recognition engine is reused by the learning system)
URL :
References : [DS96] Denzinger & Schulz (1996), Learning Domain Knowled
TPTP release : v1.2.1
Tested on SPCs : UEQ
tptp2X flags : -f otter (No use of clause type information)
CPU : SparcStation 10, 50MHz sun4m (SuperSparc Processor)
RAM size : 128MB
Operating system : Solaris 2.5.1
Implementation : C. Compiler: gcc 2.4.5 Flags: -O2 -D SPARC
Resource limits : 150 seconds
Settings/flags : -I 5 -D 1 -G 15 -R 2 -T 1 -A -3 -B 1500 -x c_global_learn
Results format : Solns Time SrhTime
Results values : Solns - P(X) and number of proofs found
or M(X) and the number of models found, where X is
"C" when the goal is universally quantified,
and "P" when the goal is existentially
quantified and thus overlapping into the goal
is performed
or TMO-Non
Time - CPU time, in seconds
SrhTime - Time in proof search, in seconds
Results summary : 1682 problems (2752 in TPTP v1.2.1, 1070 since Bugfixed)
1320 IAP-Non
106 TMO-Non
255 UNS-Ass
1 SAT-Ass
362 tested (22%)
256 solutions
71% success, over those tested
15% success, overall
Comments : Used a knowledge base (implicitly named "KNOWLEDGE")
generated from 664 proofs/226 problems
: PCL, the "Proof Communication Language" is currently
supported only for universally quantified goals
: Various other people work on DISCOUNT. In particular, the
learning system profits from proofs found with the
distributed system and Matthias Fuchs' analogical learning
-------------------------------------------------------------------------------
ATP system name : PROTEIN V2.20
People : Artificial Intelligence Research Group, University Koblenz
URL : http://www.uni-koblenz.de/ag-ki/Systems/Protein/
References : [BF94] Baumgartner & Furbach (1994), PROTEIN: A PROver wi
[BF94] Baumgartner & Furbach (1994), Model Elimination wi
[Bau94] Baumgartner (1994), Refinements of Theory Model El
[Bau96] Baumgartner (1996), Linear and Unit-Resulting Refu
[BFS97] Baumgartner et al. (1997), Computing Answers with
TPTP release : v2.0.0
Tested on SPCs : CNF
tptp2X flags : -f protein
(No use of clause type information)
CPU : 143MHz Sun Ultra 1 and 75MHz SPARCstation 20 MP
RAM size : 64MB and 300MB
Operating system : SunOS 5.5.1
Implementation : Prolog. Compiler: Eclipse Prolog
Resource limits : 300 seconds
Settings/flags : Default expect trace switched off ???
Results format : Solns Time WCTime
Results values : Solns - P and number of proofs found
or TMO-Non
or GUP-Non (No solution due to incompleteness)
Time - CPU time, in seconds
WCTime - Wall clock time, in seconds
Results summary : 1925 problems (3277 in TPTP v2.0.0, 1352 since Bugfixed)
212 IAP-Non
32 GUP-Non
851 TMO-Non
830 UNS-Ass
1713 tested (89%)
830 solutions
48% success, over those tested
43% success, overall
Comments : PROTEIN with automated theory handling, as used to
establish these results, is incomplete. (Without theory
handling PROTEIN is complete, but it would loop e.g. on
BOO008-3.)
-------------------------------------------------------------------------------
ATP system name : DISCOUNT TSM2.1
People : Stephan Schulz (Term Space Maps, Proof Analysis and
Learning, Hacks)
Joerg Denzinger (Initial supervision, Calculus)
Werner Pitz (Main inference engine)
Martin Kronenburg
URL :
References : [DS96a] Denzinger & Schulz (1996), Learning Domain Knowled
[DS96b] Denzinger & Schulz (1996), Recording and Analysing
[DKS97] Denzinger et al. (1997), DISCOUNT: A Distributed a
[Sch98] Schultz (1998), Term Space Mapping for DISCOUNT
TPTP release : v2.1.0
Tested on SPCs : UEQ
tptp2X flags : -t rm_equality:rm_eq_rstfp -f otter
CPU : SparcStation Ultra2/200
RAM size : 512MB
Operating system : Solaris 2.5.1
Implementation : C. Compiler: gcc-2.7.2. Flags: -O6
Resource limits : 300 seconds
Settings/flags : -x otsmstandard -proofs_limit 0.4 -neg_limit 0.8
Results format : Solns Time PE
Results values : Solns - P and number of proofs found
or M and the number of models found
or TMO-Non
Time - CPU time, in seconds
PE - Problem Encoding: Universally (A) or Existentially
(E) quantified
Results summary : 3469 problems (3622 in TPTP v2.1.0, 153 since Bugfixed)
3087 IAP-Non
113 TMO-Non
268 UNS-Ass
1 SAT-Ass
382 tested (11%)
269 solutions
70% success, over those tested
8% success, overall
Comments : Used a knowledge base containing 203 problems for learning
-------------------------------------------------------------------------------
ATP system name : SCOTT 6.1
People : Kahlil Hodgson, John Slaney, Ewing Lusk, William McCune
URL :
References : [SH97] Slaney & Hodgson (1997), Extending SCOTT to use Mu
[SLM94] Slaney et al. (1994), SCOTT: Semantically Constrai
[Sla93] Slaney (1993), SCOTT: A Model-Guided Theorem Prove
TPTP release : v3.3.0
tptp2X flags : -t add_equality:r -f scott:hypothesis:conjecture:none
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1000MB
Operating system : Linux 2.6.17-1.2142_FC4
Implementation : C
Resource limits : 600 seconds
Settings/flags : assign(max_num_maxisets, 5)
assign(min_num_maxisets, 3)
assign(true_weight, 0)
assign(sem_queue_limit, 2)
assign(min_search_time, 500)
assign(max_search_time, 2000)
assign(tolerance, \"1.5\")
assign(min_prob_extn, \"0.3\")
assign(cost_margin, \"10.0\")
assign(guidance_factor, \"5.0\")
assign(min_refinement, 0)
clear(demod_in_conjecture)
clear(demod_in_sem_base)
assign(max_int_fails, 2)
assign(max_ext_fails, 2)
assign(revs_to_skip_on_fail, 2)
assign(limit_weight_to, 10)
assign(cull_weights_over, 90)
assign(memory_control_point, 10000)
set(semantic_guidance)
Results format : Solns Time Given Clauses ClsKept
Results values : Solns - SZS standard
Time - CPU time, in seconds
Given - Number of given clauses in loop
Clauses - Number of clauses generated
ClsKept - Number of clauses kept
Results summary : 9854 problems (9894 in TPTP v3.3.0, 40 since Bugfixed)
674 UNK-Non
693 GUP-Non
4303 TMO-Non
1174 THM-Ref
2504 UNS-Ref
136 CSA-Mod
370 SAT-Mod
9854 tested (100%)
4184 solutions
42% success, over those tested
42% success, overall
Comments :
-------------------------------------------------------------------------------
ATP system name : Gandalf c-2.6
People : Tanel Tammet
URL : http://www.ttu.ee/it/gandalf/
TPTP release : v3.5.0
Tested on SPCs : CNF
tptp2X flags : -f otter:hypothesis:set(auto),clear(print_given) -t add_equality:r
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1000MB
Operating system : Linux 2.4.22-21mdk-i686-up-4GB
Resource limits : 600s
Command/settings : gandalf-wrapper -time %d %s
Results format : Solns Time Given Derived Kept
Results summary : 11247 problems (11395 in TPTP v3.5.0, 148 since Bugfixed)
4914 IAP-Non
2457 UNK-Non
310 TMO-Non
3566 UNS-Ass
6333 tested (56%)
3566 solutions
56% success, over those tested
32% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Jul 22 06:06:34 EDT 2008
Comments :
-------------------------------------------------------------------------------
ATP system name : Faust 1.0
People : Yury Puzis
URL : http://umsis.miami.edu/~ypuzis/FAUST-AutomatedTheoremProver.html
TPTP release : v3.5.0
Tested on SPCs : FOF CNF
tptp2X flags : -f tptp -t none
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2794MHz
RAM size : 1003MB
Operating system : Linux 2.6.11-1.1369_FC4
Resource limits : 600s
Command/settings : faust %s
Results format : Solns Time
Results summary : 11247 problems (11395 in TPTP v3.5.0, 148 since Bugfixed)
4567 UNK-Non
4803 TMO-Non
593 THM-Ref
5 THM-Ass
1279 UNS-Ref
11247 tested (100%)
1877 solutions
17% success, over those tested
17% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Jul 22 06:06:34 EDT 2008
Comments :
-------------------------------------------------------------------------------
ATP system name : Ayane 1.1
People : Russell Wallace
URL : http://code.google.com/p/ayane/
TPTP release : v4.0.1
Tested on SPCs : FOF CNF
tptp2X flags : -f tptp:raw -t none
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1002MB
Operating system : Linux 2.6.18-1.2798.fc6
Resource limits : 600s
Command/settings : ayane -t %d %s
Results format : Solns Time
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
2729 IAP-Non
10067 UNK-Non
72 GUP-Non
1331 TMO-Non
1102 THM-CRf
1211 UNS-CRf
13783 tested (83%)
2313 solutions
17% success, over those tested
14% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Mon Nov 2 10:47:38 EST 2009
Comments :
-------------------------------------------------------------------------------
ATP system name : Bliksem 1.12
People : Hans de Nivelle
URL : http://www.ii.uni.wroc.pl/~nivelle/software/bliksem
TPTP release : v4.0.1
Tested on SPCs : FOF CNF
tptp2X flags : -f bliksem -t none
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1000MB
Operating system : Linux 2.4.22-21mdk-i686-up-4GB
Resource limits : 600s
Command/settings : bliksem %s
Results format : Solns Time Generated Kept
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
2729 IAP-Non
3172 UNK-Non
6105 TMO-Non
1685 THM-Ref
2 UNS-Ass
2819 UNS-Ref
13783 tested (83%)
4506 solutions
33% success, over those tested
27% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Mon Nov 2 10:52:58 EST 2009
Comments :
-------------------------------------------------------------------------------
ATP system name : CARINE 0.734
People : Paul Haroun
URL : http://www.atpcarine.com/
TPTP release : v4.0.1
Tested on SPCs : CNF
tptp2X flags : -f carine -t add_equality
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1000MB
Operating system : Linux 2.4.22-21mdk-i686-up-4GB
Resource limits : 600s
Command/settings : carine %s t=%d xo=off uct=32000
Results format : Solns Time Generated Units
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
9712 IAP-Non
1193 UNK-Non
85 GUP-Non
4571 TMO-Non
951 UNS-Ref
6800 tested (41%)
951 solutions
14% success, over those tested
6% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Mon Nov 2 11:18:48 EST 2009
Comments :
-------------------------------------------------------------------------------
ATP system name : CiME 2.01
People : Benjamin Monate, Evelyn Contejean
URL : http://cime.lri.fr/
TPTP release : v4.0.1
Tested on SPCs : CNF_UEQ
tptp2X flags : -f oldtptp -t none
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1000MB
Operating system : Linux 2.4.22-21mdk-i686-up-4GB
Resource limits : 600s
Command/settings : tptp2cime %s
Results format : Solns Time
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
15474 IAP-Non
4 UNK-Non
515 TMO-Non
510 UNS-Ass
9 SAT-Sat
1038 tested (6%)
519 solutions
50% success, over those tested
3% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Mon Nov 2 11:22:03 EST 2009
Comments :
-------------------------------------------------------------------------------
ATP system name : Darwin 1.4.5
People : Alexander Fuchs, Peter Baumgartner, Cesare Tinelli
URL : http://goedel.cs.uiowa.edu/Darwin/
TPTP release : v4.0.1
Tested on SPCs : FOF CNF
tptp2X flags : -f tptp:raw -t none
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1002MB
Operating system : Linux 2.6.26.8-57.fc8
Resource limits : 300s
Command/settings : darwin -pl 0 -pmc true -to %d %s
Results format : Solns Time
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
2729 IAP-Non
112 UNK-Non
8356 TMO-Non
2180 THM-Ass
2327 UNS-Ass
301 CSA-Mod
507 SAT-Mod
13783 tested (83%)
5315 solutions
39% success, over those tested
32% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Mon Nov 2 11:23:10 EST 2009
Comments :
-------------------------------------------------------------------------------
ATP system name : DarwinFM 1.4.5
People : Alexander Fuchs, Peter Baumgartner, Cesare Tinelli
URL : http://goedel.cs.uiowa.edu/Darwin/
TPTP release : v4.0.1
Tested on SPCs : FOF_NKT FOF_NKU CNF_NKU
tptp2X flags : -f tptp:raw -t none
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1002MB
Operating system : Linux 2.6.26.8-57.fc8
Resource limits : 300s
Command/settings : darwin -fd true -ppp true -pl 0 -to %d -pmtptp true %s
Results format : Solns Time
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
13719 IAP-Non
7 UNK-Non
1557 TMO-Non
476 CSA-FMo
753 SAT-FMo
2793 tested (17%)
1229 solutions
44% success, over those tested
7% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Mon Nov 2 11:28:03 EST 2009
Comments :
-------------------------------------------------------------------------------
ATP system name : DCTP 1.31
People : Gernot Stenz, Reinhold Letz
URL :
TPTP release : v4.0.1
Tested on SPCs : CNF
tptp2X flags : -f oldtptp -t none
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1000MB
Operating system : Linux 2.4.22-21mdk-i686-up-4GB
Resource limits : 600s
Command/settings : dctp-wrapper -negpref -complexity -fullrewrite -alternate -resisol %s
Results format : Solns Time Linkings ClausesInTableau
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
9712 IAP-Non
759 UNK-Non
589 GUP-Non
2181 TMO-Non
2767 UNS-Ass
504 SAT-Ass
6800 tested (41%)
3271 solutions
48% success, over those tested
20% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Mon Nov 2 11:29:25 EST 2009
Comments :
-------------------------------------------------------------------------------
ATP system name : E 1.1
People : Stephan Schulz
URL : http://www.eprover.org/
TPTP release : v4.0.1
Tested on SPCs : FOF CNF
tptp2X flags : -f tptp:raw -t none
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1002MB
Operating system : Linux 2.6.26.8-57.fc8
Resource limits : 300s
Command/settings : eprover -s --print-statistics -xAuto -tAuto --cpu-limit=%d --memory-limit=Auto --tstp-in %s
Results format : Solns Time Generated NonTrivial Processed
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
2729 IAP-Non
51 UNK-Non
1 GUP-Non
5041 TMO-Non
3610 THM-Ass
4211 UNS-Ass
333 CSA-Ass
536 SAT-Ass
13783 tested (83%)
8690 solutions
63% success, over those tested
53% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Mon Nov 2 11:32:30 EST 2009
Comments :
-------------------------------------------------------------------------------
ATP system name : E-Darwin 1.2
People : Bjorn Pelzer
URL : http://www.uni-koblenz.de/~bpelzer/edarwin/
TPTP release : v4.0.1
Tested on SPCs : CNF
tptp2X flags : -f tptp:raw -t none
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1002MB
Operating system : Linux 2.6.26.8-57.fc8
Resource limits : 300s
Command/settings : e-darwin -if tptp -pl 0 %s
Results format : Solns Time
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
9712 IAP-Non
130 UNK-Non
4062 TMO-Non
2145 UNS-Ass
463 SAT-Ass
6800 tested (41%)
2608 solutions
38% success, over those tested
16% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Mon Nov 2 11:37:46 EST 2009
Comments :
-------------------------------------------------------------------------------
ATP system name : E-KRHyper 1.1.3
People : Bjorn Pelzer
URL : http://www.uni-koblenz.de/~bpelzer/ekrhyper/
TPTP release : v4.0.1
Tested on SPCs : FOF CNF
tptp2X flags : -f tptp:raw -t none
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1002MB
Operating system : Linux 2.6.26.8-57.fc8
Resource limits : 300s
Command/settings : casc/ekrhyper %s
Results format : Solns Time Disjunctions Depth Closed Evaluations
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
2729 IAP-Non
457 UNK-Non
18 GUP-Non
8920 TMO-Non
1828 THM-Ass
2022 UNS-Ass
303 CSA-Ass
235 SAT-Ass
13783 tested (83%)
4388 solutions
32% success, over those tested
27% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Mon Nov 2 11:40:37 EST 2009
Comments :
-------------------------------------------------------------------------------
ATP system name : EQP 0.9e
People : William McCune
URL : http://www.cs.unm.edu/~mccune/eqp/
TPTP release : v4.0.1
Tested on SPCs : CNF_UEQ
tptp2X flags : -f eqp -t none
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1002MB
Operating system : Linux 2.6.18-1.2798.fc6
Resource limits : 600s
Command/settings : eqp_wrapper %s
Results format : Solns Time Clauses Given
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
15474 IAP-Non
461 UNK-Non
2 TMO-Non
575 UNS-Ref
1038 tested (6%)
575 solutions
55% success, over those tested
3% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Mon Nov 2 11:45:41 EST 2009
Comments :
-------------------------------------------------------------------------------
ATP system name : Equinox 4.1
People : Koen Claessen
URL : http://www.cs.chalmers.se/~koen/folkung/
TPTP release : v4.0.1
Tested on SPCs : FOF CNF
tptp2X flags : -f tptp:raw -t none
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1002MB
Operating system : Linux 2.6.26.8-57.fc8
Resource limits : 300s
Command/settings : equinox --tstp %s
Results format : Solns Time
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
2729 IAP-Non
39 UNK-Non
675 GUP-Non
8503 TMO-Non
2487 THM-Ass
2079 UNS-Ass
13783 tested (83%)
4566 solutions
33% success, over those tested
28% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Mon Nov 2 11:46:37 EST 2009
Comments :
-------------------------------------------------------------------------------
ATP system name : Fampire 1.3
People : Josef Urban
URL : http://dreamers.com/lichlair/imagenes/bloodredmoon3.jpg
TPTP release : v4.0.1
Tested on SPCs : FOF
tptp2X flags : -f tptp -t none
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1003MB
Operating system : Linux 2.6.11-1.1369_FC4
Resource limits : 600s
Command/settings : FlotterOnTPTP.pl -f oldtptp -s vampire -t %d %s
Results format : Solns Time
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
9529 IAP-Non
2670 UNK-Non
935 TMO-Non
3203 THM-Ass
78 UNS-Ass
79 CSA-Ass
18 SAT-Ass
6983 tested (42%)
3378 solutions
48% success, over those tested
20% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Mon Nov 2 11:51:23 EST 2009
Comments :
-------------------------------------------------------------------------------
ATP system name : FDP 0.9.16
People : Peter Baumgartner
URL :
TPTP release : v4.0.1
Tested on SPCs : CNF
tptp2X flags : -f protein -t add_equality
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1000MB
Operating system : Linux 2.4.22-21mdk-i686-up-4GB
Resource limits : 600s
Command/settings : fdp-casc %s %d
Results format : Solns Time
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
9712 IAP-Non
1635 UNK-Non
168 GUP-Non
2698 TMO-Non
1895 UNS-Ass
404 SAT-Ass
6800 tested (41%)
2299 solutions
34% success, over those tested
14% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Mon Nov 2 11:54:14 EST 2009
Comments : Flags: -q -a
-------------------------------------------------------------------------------
ATP system name : Fiesta 2
People : Robert Nieuwenhuis
URL :
TPTP release : v4.0.1
Tested on SPCs : CNF_UEQ
tptp2X flags : -f dedam -t none
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1000MB
Operating system : Linux 2.4.22-21mdk-i686-up-4GB
Resource limits : 600s
Command/settings : fiesta-wrapper %s
Results format : Solns Time Memory
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
15474 IAP-Non
76 UNK-Non
328 TMO-Non
634 UNS-Ref
1038 tested (6%)
634 solutions
61% success, over those tested
4% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Mon Nov 2 11:56:52 EST 2009
Comments :
-------------------------------------------------------------------------------
ATP system name : Geo 2007f
People : Hans de Nivelle
URL : http://www.ii.uni.wroc.pl/~nivelle/software/geo/
TPTP release : v4.0.1
Tested on SPCs : FOF CNF
tptp2X flags : -f tptp:short -t none
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1003MB
Operating system : Linux 2.6.17-1.2142_FC4
Resource limits : 600s
Command/settings : geo -nonempty -tptp_input -inputfile %s
Results format : Solns Time
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
2729 IAP-Non
968 UNK-Non
139 GUP-Non
7620 TMO-Non
1703 THM-Ref
2270 UNS-Ref
460 CSA-Mod
623 SAT-Mod
13783 tested (83%)
5056 solutions
37% success, over those tested
31% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Mon Nov 2 11:57:35 EST 2009
Comments :
-------------------------------------------------------------------------------
ATP system name : GrAnDe 1.1
People : Stephan Schulz, Geoff Sutcliffe
URL : http://www.cs.miami.edu/~tptp/ATPSystems/GrAnDe/
TPTP release : v4.0.1
Tested on SPCs : CNF_EPR
tptp2X flags : -f tptp -t add_equality+cnf:otter
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1003MB
Operating system : Linux 2.6.17-1.2142_FC4
Resource limits : 600s
Command/settings : And %s %d
Results format : Solns Time EStatus
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
15729 IAP-Non
181 UNK-Non
5 TMO-Non
453 UNS-Ass
144 SAT-Ass
783 tested (5%)
597 solutions
76% success, over those tested
4% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Mon Nov 2 12:06:12 EST 2009
Comments : eground: --tptp-in --dimacs --silent --resources-info
--split-tries=100 --memory-limit=400
--soft-cpu-limit=%d --add-one-instance
--constraints
-------------------------------------------------------------------------------
ATP system name : Infinox 1.0
People : Koen Claessen
URL :
TPTP release : v4.0.1
Tested on SPCs : FOF CNF
tptp2X flags : -f tptp:raw -t none
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1002MB
Operating system : Linux 2.6.26.8-57.fc8
Resource limits : 300s
Command/settings : run_infinox %s
Results format : Solns Time
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
2729 IAP-Non
28 UNK-Non
5101 GUP-Non
4606 TMO-Non
1970 FUN-Ass
2078 FTH-Ass
13783 tested (83%)
4048 solutions
29% success, over those tested
25% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Nov 3 09:35:35 EST 2009
Comments :
-------------------------------------------------------------------------------
ATP system name : iProver 0.7
People : Konstantin Korovin
URL : http://www.cs.man.ac.uk/~korovink/iprover/
TPTP release : v4.0.1
Tested on SPCs : FOF CNF
tptp2X flags : -f tptp:raw -t none
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1002MB
Operating system : Linux 2.6.26.8-57.fc8
Resource limits : 300s
Command/settings : iproveropt --eprover_path /home/graph/tptp/Systems/iProver---0.7/ --time_out_real %d %s
Results format : Solns Time ILoops RLoops PropCalls
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
2729 IAP-Non
51 UNK-Non
46 GUP-Non
6995 TMO-Non
3031 THM-Ass
2687 UNS-Ass
369 CSA-Ass
604 SAT-Ass
13783 tested (83%)
6691 solutions
49% success, over those tested
41% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Mon Nov 2 12:06:54 EST 2009
Comments :
-------------------------------------------------------------------------------
ATP system name : IsabelleM 2009
People : Larry Paulson, Tobias Nipkow, Stefan Berghofer, Makarius Wenzel, Jasmin Blanchette
URL : http://isabelle.in.tum.de/
TPTP release : v4.0.1
Tested on SPCs : THF
tptp2X flags : -f tptp:raw -t none
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1002MB
Operating system : Linux 2.6.26.8-57.fc8
Resource limits : 300s
Command/settings : run-isabelle %s %d refute
Results format : Solns Time
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
13783 IAP-Non
1724 UNK-Non
793 TMO-Non
210 CSA-Mod
2 SAT-Ass
2729 tested (17%)
212 solutions
8% success, over those tested
1% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Wed Nov 11 07:35:10 EST 2009
Comments :
-------------------------------------------------------------------------------
ATP system name : IsabelleN 2009
People : Larry Paulson, Tobias Nipkow, Jasmin Blanchette
URL : http://isabelle.in.tum.de/
TPTP release : v4.0.1
Tested on SPCs : THF
tptp2X flags : -f tptp:raw -t none
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1002MB
Operating system : Linux 2.6.26.8-57.fc8
Resource limits : 300s
Command/settings : run-isabelle %s %d nitpick
Results format : Solns Time
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
13783 IAP-Non
1736 UNK-Non
703 TMO-Non
288 CSA-Ass
2 SAT-Ass
2729 tested (17%)
290 solutions
11% success, over those tested
2% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Fri Nov 13 07:03:53 EST 2009
Comments :
-------------------------------------------------------------------------------
ATP system name : IsabelleP 2009
People : Larry Paulson, Tobias Nipkow, Stefan Berghofer, Makarius Wenzel
URL : http://isabelle.in.tum.de/
TPTP release : v4.0.1
Tested on SPCs : THF
tptp2X flags : -f tptp:raw -t none
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1002MB
Operating system : Linux 2.6.26.8-57.fc8
Resource limits : 300s
Command/settings : run-isabelle %s %d 'simp,blast,auto,metis,fast,fastsimp,best,force,meson'
Results format : Solns Time SolvedBy
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
13783 IAP-Non
805 UNK-Non
641 TMO-Non
1280 THM-Prf
3 UNS-Prf
2729 tested (17%)
1283 solutions
47% success, over those tested
8% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Wed Nov 11 07:28:34 EST 2009
Comments :
-------------------------------------------------------------------------------
ATP system name : leanCoP 2.1
People : Jens Otten, Thomas Raths
URL : http://www.leancop.de/
TPTP release : v4.0.1
Tested on SPCs : FOF
tptp2X flags : -f tptp:raw -t none
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1002MB
Operating system : Linux 2.6.26.8-57.fc8
Resource limits : 300s
Command/settings : leancop.sh %s %d
Results format : Solns Time
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
9529 IAP-Non
23 UNK-Non
4556 TMO-Non
2302 THM-Prf
57 UNS-Prf
25 CSA-Ass
20 SAT-Ass
6983 tested (42%)
2404 solutions
34% success, over those tested
15% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Mon Nov 2 12:17:08 EST 2009
Comments :
-------------------------------------------------------------------------------
ATP system name : LeanTAP 2.3
People : Bernhard Beckert
URL : http://www.uni-koblenz.de/~beckert/leantap/
TPTP release : v4.0.1
Tested on SPCs : FOF CNF
tptp2X flags : -f leantap -t add_equality
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2794MHz
RAM size : 1003MB
Operating system : Linux 2.6.11-1.1369_FC4
Resource limits : 600s
Command/settings : leantap %s
Results format : Solns Time
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
2729 IAP-Non
6281 UNK-Non
6860 TMO-Non
328 THM-Ass
314 UNS-Ass
13783 tested (83%)
642 solutions
5% success, over those tested
4% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Mon Nov 2 12:20:00 EST 2009
Comments :
-------------------------------------------------------------------------------
ATP system name : LEO-II 1.1
People : Christoph Benzmueller, Frank Theiss
URL : http://www.ags.uni-sb.de/~leo/
TPTP release : v4.0.1
Tested on SPCs : THF
tptp2X flags : -f tptp:raw -t none
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1002MB
Operating system : Linux 2.6.26.8-57.fc8
Resource limits : 300s
Command/settings : leo.opt --proofoutput --foatp e --atp e=/home/graph/tptp/Systems/LEO-II---1.1/eprover %s
Results format : Solns Time
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
13783 IAP-Non
171 UNK-Non
1082 TMO-Non
1469 THM-CRf
7 UNS-CRf
2729 tested (17%)
1476 solutions
54% success, over those tested
9% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Wed Nov 4 06:14:27 EST 2009
Comments :
-------------------------------------------------------------------------------
ATP system name : Mace2 2.2
People : William McCune
URL : http://www.cs.unm.edu/~mccune/otter/
TPTP release : v4.0.1
Tested on SPCs : CNF_NKU FOF_NKT FOF_NKu
tptp2X flags : -f otter:hypothesis:set(auto),clear(print_given) -t add_equality:r
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1000MB
Operating system : Linux 2.4.22-21mdk-i686-up-4GB
Resource limits : 600s
Command/settings : mace-script %s
Results format : Solns Time Size
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
13821 IAP-Non
4 UNK-Non
1205 GUP-Non
924 TMO-Non
133 CSA-FMo
425 SAT-FMo
2691 tested (16%)
558 solutions
21% success, over those tested
3% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Mon Nov 2 12:26:37 EST 2009
Comments : Flags: -N 12 -p -k 100000
-------------------------------------------------------------------------------
ATP system name : Mace4 0908
People : William McCune
URL : http://www.cs.unm.edu/~mccune/prover9/
TPTP release : v4.0.1
Tested on SPCs : CNF_NKU FOF_NKT FOF_NKU
tptp2X flags : -f prover9:[set(print_models_portable)] -t stdfof
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1002MB
Operating system : Linux 2.6.18-1.2798.fc6
Resource limits : 600s
Command/settings : mace4 -c -N -1 -t %d -f %s
Results format : Solns Time Size
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
13719 IAP-Non
468 UNK-Non
1411 TMO-Non
286 CSA-FMo
628 SAT-FMo
2793 tested (17%)
914 solutions
33% success, over those tested
6% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Mon Nov 2 12:27:58 EST 2009
Comments :
-------------------------------------------------------------------------------
ATP system name : Matita 1.0
People : Andrea Asperti
URL : http://matita.cs.unibo.it/
TPTP release : v4.0.1
Tested on SPCs : CNF_UEQ
tptp2X flags : -f tptp:raw -t none
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1002MB
Operating system : Linux 2.6.26.8-57.fc8
Resource limits : 300s
Command/settings : matitaprover --timeout %d --tptppath /home/graph/tptp/TPTP %s
Results format : Solns Time
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
15474 IAP-Non
23 UNK-Non
21 GUP-Non
467 TMO-Non
527 UNS-CRf
1038 tested (6%)
527 solutions
51% success, over those tested
3% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Mon Nov 2 12:29:38 EST 2009
Comments :
-------------------------------------------------------------------------------
ATP system name : Metis 2.2
People : Joe Hurd
URL : http://www.gilith.com/software/metis
TPTP release : v4.0.1
Tested on SPCs : FOF CNF
tptp2X flags : -f tptp:raw -t none
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1002MB
Operating system : Linux 2.6.18-1.2798.fc6
Resource limits : 600s
Command/settings : metis --show proof --show saturation %s
Results format : Solns Time
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
2729 IAP-Non
1294 UNK-Non
8278 TMO-Non
1926 THM-CRf
4 UNS-Ass
2253 UNS-CRf
28 CSA-Sat
13783 tested (83%)
4211 solutions
31% success, over those tested
26% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Mon Nov 2 12:30:14 EST 2009
Comments :
-------------------------------------------------------------------------------
ATP system name : Muscadet 3.0
People : Dominique Pastre
URL : http://www.math-info.univ-paris5.fr/~pastre/muscadet/muscadet.html
TPTP release : v4.0.1
Tested on SPCs : FOF
tptp2X flags : -f tptp -t none
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1002MB
Operating system : Linux 2.6.18-1.2798.fc6
Resource limits : 600s
Command/settings : muscadet-FOF %s
Results format : Solns Time
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
9529 IAP-Non
386 UNK-Non
1047 GUP-Non
4063 TMO-Non
1343 THM-Prf
112 THM-Ass
1 UNS-Ass
31 UNS-Prf
6983 tested (42%)
1487 solutions
21% success, over those tested
9% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Mon Nov 2 12:37:36 EST 2009
Comments :
-------------------------------------------------------------------------------
ATP system name : Otter 3.3
People : William McCune
URL : http://www.cs.unm.edu/~mccune/otter/
TPTP release : v4.0.1
Tested on SPCs : FOF CNF
tptp2X flags : -f tptp:raw -t none
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1002MB
Operating system : Linux 2.6.18-1.2798.fc6
Resource limits : 600s
Command/settings : otter-tptp-script %s
Results format : Solns Time Given Generated Kept
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
2729 IAP-Non
25 UNK-Non
8184 GUP-Non
2365 TMO-Non
1518 THM-Ref
1691 UNS-Ref
13783 tested (83%)
3209 solutions
23% success, over those tested
19% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Mon Nov 2 12:45:23 EST 2009
Comments : Flags: set(prolog_style_variables) set(auto) set(tptp_eq)
-------------------------------------------------------------------------------
ATP system name : Paradox 3.0
People : Koen Claessen
URL : http://www.cs.chalmers.se/~koen/folkung/
TPTP release : v4.0.1
Tested on SPCs : FOF_NKT FOF_NKU_NUN CNF_NKU
tptp2X flags : -f tptp:short -t none
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1002MB
Operating system : Linux 2.6.18-1.2798.fc6
Resource limits : 600s
Command/settings : paradox --tstp --model %s
Results format : Solns Time Size
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
13719 IAP-Non
274 UNK-Non
32 GUP-Non
1208 TMO-Non
487 CSA-FMo
792 SAT-FMo
2793 tested (17%)
1279 solutions
46% success, over those tested
8% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Mon Nov 2 13:01:32 EST 2009
Comments :
-------------------------------------------------------------------------------
ATP system name : Prover9 0908
People : William McCune
URL : http://www.cs.unm.edu/~mccune/prover9/
TPTP release : v4.0.1
Tested on SPCs : FOF CNF
tptp2X flags : -f prover9 -t stdfof
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1002MB
Operating system : Linux 2.6.18-1.2798.fc6
Resource limits : 600s
Command/settings : prover9 -t %d -f %s
Results format : Solns Time Given Generated Kept
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
2729 IAP-Non
4331 UNK-Non
845 GUP-Non
3584 TMO-Non
2189 THM-Ref
2834 UNS-Ref
13783 tested (83%)
5023 solutions
36% success, over those tested
30% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Mon Nov 2 13:05:13 EST 2009
Comments :
-------------------------------------------------------------------------------
ATP system name : randoCoP 1.1
People : Jens Otten, Thomas Raths
URL :
TPTP release : v4.0.1
Tested on SPCs : FOF
tptp2X flags : -f tptp:raw -t none
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1002MB
Operating system : Linux 2.6.18-1.2798.fc6
Resource limits : 600s
Command/settings : randocop.sh %s %d
Results format : Solns Time
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
9529 IAP-Non
9 UNK-Non
4509 TMO-Non
2366 THM-Prf
55 UNS-Prf
24 CSA-Ass
20 SAT-Ass
6983 tested (42%)
2465 solutions
35% success, over those tested
15% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Mon Nov 2 13:36:22 EST 2009
Comments :
-------------------------------------------------------------------------------
ATP system name : S-SETHEO 0.0
People : Reinhold Letz
URL : http://www4.informatik.tu-muenchen.de/~letz/setheo/
TPTP release : v4.0.1
Tested on SPCs : CNF
tptp2X flags : -f oldtptp -t add_equality
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1003MB
Operating system : Linux 2.6.17-1.2142_FC4
Resource limits : 600s
Command/settings : scheme-setheo -norel -foldup -sgindex -indexfoldup -reg -mate -dynsgreord 0 %s
Results format : Solns Time ProofLength Inferences
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
9712 IAP-Non
4557 UNK-Non
323 TMO-Non
1920 UNS-Ass
6800 tested (41%)
1920 solutions
28% success, over those tested
12% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Mon Nov 2 13:39:30 EST 2009
Comments :
-------------------------------------------------------------------------------
ATP system name : SETHEO 3.3
People : Reinhold Letz
URL : http://www4.informatik.tu-muenchen.de/~letz/setheo/
TPTP release : v4.0.1
Tested on SPCs : CNF
tptp2X flags : -f setheo -t add_equality
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1000MB
Operating system : Linux 2.4.22-21mdk-i686-up-4GB
Resource limits : 600s
Command/settings : setheo-wrapper %s
Results format : Solns Time Inferences
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
9712 IAP-Non
802 UNK-Non
2333 GUP-Non
1868 TMO-Non
1797 UNS-Ass
6800 tested (41%)
1797 solutions
26% success, over those tested
11% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Mon Nov 2 13:42:31 EST 2009
Comments : Flags: inwasm -cons -foldup, sam -dr -cons
-------------------------------------------------------------------------------
ATP system name : SInE 0.4
People : Krystof Hoder
URL : http://www.cs.man.ac.uk/~hoderk/sine/
TPTP release : v4.0.1
Tested on SPCs : FOF
tptp2X flags : -f tptp:raw -t none
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1002MB
Operating system : Linux 2.6.26.8-57.fc8
Resource limits : 300s
Command/settings : Source/sine.py -e eprover -t %d %s
Results format : Solns Time
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
9529 IAP-Non
851 UNK-Non
2788 TMO-Non
83 THM-Ass
3261 THM-CRf
6983 tested (42%)
3344 solutions
48% success, over those tested
20% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Wed Nov 11 13:10:48 EST 2009
Comments :
-------------------------------------------------------------------------------
ATP system name : SNARK 20080805
People : Mark Stickel
URL : http://www.ai.sri.com/~stickel/snark.html
TPTP release : v4.0.1
Tested on SPCs : FOF CNF
tptp2X flags : -f tptp -t none
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1002MB
Operating system : Linux 2.6.18-1.2798.fc6
Resource limits : 600s
Command/settings : run-snark %s %d
Results format : Solns Time Derived Kept Answers
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
2729 IAP-Non
3521 UNK-Non
492 GUP-Non
4481 TMO-Non
2446 THM-Ref
2843 UNS-Ref
13783 tested (83%)
5289 solutions
38% success, over those tested
32% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Nov 3 07:57:39 EST 2009
Comments : This is SNARK release 20080805r005
: Settings/flags:
Agenda length 3000
(default-use-hyperresolution t)
(default-use-paramodulation t)
(default-use-factoring :pos)
(default-use-literal-ordering-with-hyperresolution
'literal-ordering-p)
(default-use-literal-ordering-with-paramodulation
'literal-ordering-p)
(default-print-rows-when-given nil)
(default-print-rows-when-derived nil)
(default-run-time-limit 600)
(default-listen-for-commands nil)
(default-use-kif-rewrites nil)
(default-use-closure-when-satisfiable nil)
: The strategy is incomplete, so no solution does not
indicate satisfiability. If the propositional abstraction
of a problem is satisfiable, existence of a model is
reported
: Commutative unification is used for commutative function
and predicate symbols. Associative-commutative unification
is used for associative-commutative function symbols
Commutativity and associativity axioms in the problems are
detected automatically
-------------------------------------------------------------------------------
ATP system name : SOS 2.0
People : John Slaney
URL : http://users.rsise.anu.edu.au/~jks/software/sos2.tar.gz
TPTP release : v4.0.1
Tested on SPCs : FOF CNF
tptp2X flags : -f otter:hypothesis:set(auto),clear(print_given) -t add_equality:r
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1003MB
Operating system : Linux 2.6.17-1.2142_FC4
Resource limits : 600s
Command/settings : sos-script %s
Results format : Solns Time
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
2729 IAP-Non
4147 UNK-Non
486 GUP-Non
4885 TMO-Non
1515 THM-Ref
2750 UNS-Ref
13783 tested (83%)
4265 solutions
31% success, over those tested
26% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Nov 3 09:41:46 EST 2009
Comments :
-------------------------------------------------------------------------------
ATP system name : SPASS 3.01
People : Christoph Weidenbach
URL : http://spass.mpi-sb.mpg.de/
TPTP release : v4.0.1
Tested on SPCs : FOF CNF
tptp2X flags : -f dfg -t stdfof
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1003MB
Operating system : Linux 2.6.17-1.2142_FC4
Resource limits : 600s
Command/settings : SPASS -PGiven=0 -PProblem=0 -DocProof -TimeLimit=%d %s
Results format : Solns Time Memory Derived Kept Used
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
2729 IAP-Non
1492 UNK-Non
345 GUP-Non
4791 TMO-Non
2893 THM-Ref
3406 UNS-Ref
321 CSA-Ass
535 SAT-Ass
13783 tested (83%)
7155 solutions
52% success, over those tested
43% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Nov 3 08:18:20 EST 2009
Comments :
-------------------------------------------------------------------------------
ATP system name : SRASS 0.1
People : Geoff Sutcliffe
URL : http://www.cs.miami.edu/~tptp/ATPSystems/SRASS/
TPTP release : v4.0.1
Tested on SPCs : FOF
tptp2X flags : -f tptp -t none
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1003MB
Operating system : Linux 2.6.17-1.2142_FC4
Resource limits : 600s
Command/settings : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
Results format : Solns Time Selected Unselected
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
9529 IAP-Non
1751 UNK-Non
2370 TMO-Non
2813 THM-Sol
49 THM-Ass
6983 tested (42%)
2862 solutions
41% success, over those tested
17% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Nov 3 08:30:59 EST 2009
Comments :
-------------------------------------------------------------------------------
ATP system name : TPS 3.080227G1d
People : Peter Andrews, Chad Brown
URL : http://gtps.math.cmu.edu/tps.html
TPTP release : v4.0.1
Tested on SPCs : THF
tptp2X flags : -f tptp:raw -t none
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1002MB
Operating system : Linux 2.6.18-1.2798.fc6
Resource limits : 600s
Command/settings : run-tps-GOOD1 %s %d
Results format : Solns Time Mode
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
13783 IAP-Non
91 UNK-Non
4 GUP-Non
1185 TMO-Non
1446 THM-Ass
3 UNS-Ass
2729 tested (17%)
1449 solutions
53% success, over those tested
9% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Nov 3 08:45:19 EST 2009
Comments :
-------------------------------------------------------------------------------
ATP system name : Vampire 9.0
People : Andrei Voronkov
URL : http://www.voronkov.com/vampire.cgi
TPTP release : v4.0.1
Tested on SPCs : CNF_EPR
tptp2X flags : -f tptp:short -t none
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1002MB
Operating system : Linux 2.6.18-1.2798.fc6
Resource limits : 600s
Command/settings : jumpirefix --output_syntax tptp -t %d %s
Results format : Solns Time
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
15729 IAP-Non
15 UNK-Non
32 GUP-Non
146 TMO-Non
484 UNS-Ref
106 SAT-Ass
783 tested (5%)
590 solutions
75% success, over those tested
4% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Nov 3 08:50:44 EST 2009
Comments :
-------------------------------------------------------------------------------
ATP system name : VampireLT 10.0
People : Andrei Voronkov
URL : http://www.voronkov.com/vampire.cgi
TPTP release : v4.0.1
Tested on SPCs : FOF
tptp2X flags : -f tptp:raw -t none
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1002MB
Operating system : Linux 2.6.18-1.2798.fc6
Resource limits : 600s
Command/settings : lto.pl %d %s
Results format : Solns Time
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
9529 IAP-Non
1638 UNK-Non
2093 TMO-Non
3165 THM-Ref
87 UNS-Ref
6983 tested (42%)
3252 solutions
47% success, over those tested
20% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Nov 3 09:27:30 EST 2009
Comments :
-------------------------------------------------------------------------------
ATP system name : Vampire 11.0
People : Andrei Voronkov
URL : http://www.voronkov.com/vampire.cgi
TPTP release : v4.0.1
Tested on SPCs : FOF CNF
tptp2X flags : -f tptp:raw -t none
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1002MB
Operating system : Linux 2.6.26.8-57.fc8
Resource limits : 300s
Command/settings : drakosha.pl %d %s /home/graph/tptp/TPTP
Results format : Solns Time
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
2729 IAP-Non
619 UNK-Non
2339 GUP-Non
3331 TMO-Non
3229 THM-Ref
4265 UNS-Ref
13783 tested (83%)
7494 solutions
54% success, over those tested
45% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Nov 3 09:14:02 EST 2009
Comments :
-------------------------------------------------------------------------------
ATP system name : Waldmeister C09
People : Thomas Hillenbrand, Bernd Loechner (WEC)
URL : http://www.waldmeister.org/
TPTP release : v4.0.1
Tested on SPCs : CNF_UEQ
tptp2X flags : -f tptp -t none
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1002MB
Operating system : Linux 2.6.18-1.2798.fc6
Resource limits : 600s
Command/settings : woody %s
Results format : Solns Time
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
15474 IAP-Non
2 UNK-Non
2 GUP-Non
223 TMO-Non
806 UNS-Prf
5 SAT-Ass
1038 tested (6%)
811 solutions
78% success, over those tested
5% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Nov 3 10:06:45 EST 2009
Comments :
-------------------------------------------------------------------------------
ATP system name : zChaff 04.11.15
People : Sharad Malik
URL : http://www.princeton.edu/~chaff
TPTP release : v4.0.1
Tested on SPCs : CNF_PRP
tptp2X flags : -f dimacs -t none
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1003MB
Operating system : Linux 2.6.17-1.2142_FC4
Resource limits : 600s
Command/settings : zchaff %s %d
Results format : Solns Time MaxDecisionLevel NumDecisions
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
16467 IAP-Non
37 UNS-Ass
8 SAT-Ass
45 tested (0%)
45 solutions
100% success, over those tested
0% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Nov 3 10:08:59 EST 2009
Comments :
-------------------------------------------------------------------------------
ATP system name : Zenon 0.5.0
People : Richard Bonichon, David Delahaye, Damien Doligez
URL : http://focal.inria.fr/zenon/
TPTP release : v4.0.1
Tested on SPCs : FOF
tptp2X flags : -f tptp -t none
CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
RAM size : 1003MB
Operating system : Linux 2.6.17-1.2142_FC4
Resource limits : 600s
Command/settings : zenon -itptp -p0 -stats -ocoq -max-time %ds %s
Results format : Solns Time NodesSearch MaxBranchF ProofNodes Formulas
Results summary : 16512 problems (16512 in TPTP v4.0.1, 0 since Bugfixed)
9529 IAP-Non
712 UNK-Non
3562 GUP-Non
1440 TMO-Non
1184 THM-Prf
85 UNS-Prf
6983 tested (42%)
1269 solutions
18% success, over those tested
8% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Nov 3 10:09:14 EST 2009
Comments :
-------------------------------------------------------------------------------