| 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 : 1339 problems (2652 in TPTP v1.1.3, 1313 since Bugfixed)
14 IAP-Non
567 TMO-Non
758 UNS-Ass
1325 tested (99%)
758 solutions
57% success, over those tested
57% 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 : 1339 problems (2652 in TPTP v1.1.3, 1313 since Bugfixed)
4 ERR-Non
666 TMO-Non
660 UNS-Ass
9 SAT-Ass
1339 tested (100%)
669 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 : 1339 problems (2652 in TPTP v1.1.3, 1313 since Bugfixed)
787 TMO-Non
543 UNS-Ass
9 SAT-Ass
1339 tested (100%)
552 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 : 1339 problems (2652 in TPTP v1.1.3, 1313 since Bugfixed)
78 NTT-Non
25 ERR-Non
604 TMO-Non
632 UNS-Ass
1261 tested (94%)
632 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 : 1339 problems (2652 in TPTP v1.1.3, 1313 since Bugfixed)
19 NTT-Non
28 ERR-Non
682 TMO-Non
610 UNS-Ass
1320 tested (99%)
610 solutions
46% success, over those tested
46% 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 : 1339 problems (2652 in TPTP v1.1.3, 1313 since Bugfixed)
594 TMO-Non
736 UNS-Ass
9 SAT-Ass
1339 tested (100%)
745 solutions
56% success, over those tested
56% 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 : 1692 problems (2752 in TPTP v1.2.1, 1060 since Bugfixed)
1330 IAP-Non
106 TMO-Non
255 UNS-Ass
1 SAT-Ass
362 tested (21%)
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 : 1935 problems (3277 in TPTP v2.0.0, 1342 since Bugfixed)
212 IAP-Non
32 GUP-Non
854 TMO-Non
837 UNS-Ass
1723 tested (89%)
837 solutions
49% 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 : 3479 problems (3622 in TPTP v2.1.0, 143 since Bugfixed)
3097 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 : 9894 problems (9894 in TPTP v3.3.0, 0 since Bugfixed)
684 UNK-Non
694 GUP-Non
4320 TMO-Non
1174 THM-Ref
2513 UNS-Ref
136 CSA-Mod
373 SAT-Mod
9894 tested (100%)
4196 solutions
42% success, over those tested
42% success, overall
Comments :
-------------------------------------------------------------------------------
ATP system name : Bliksem 1.12
People : Hans de Nivelle
URL : http://www.ii.uni.wroc.pl/~nivelle/software/bliksem
TPTP release : v3.5.0
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 : 600
Command/settings : bliksem %s
Results format : Solns Time Generated Kept
Results summary : 11395 problems (11395 in TPTP v3.5.0, 0 since Bugfixed)
2298 UNK-Non
5162 TMO-Non
1259 THM-Ref
2 UNS-Ass
2674 UNS-Ref
11395 tested (100%)
3935 solutions
35% success, over those tested
35% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Jul 22 06:06:34 EDT 2008
Comments :
-------------------------------------------------------------------------------
ATP system name : CARINE 0.734
People : Paul Haroun
URL : http://www.atpcarine.com/
TPTP release : v3.5.0
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 : 11395 problems (11395 in TPTP v3.5.0, 0 since Bugfixed)
5049 IAP-Non
739 UNK-Non
85 GUP-Non
4571 TMO-Non
951 UNS-Ref
6346 tested (56%)
951 solutions
15% success, over those tested
8% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Jul 22 06:06:34 EDT 2008
Comments :
-------------------------------------------------------------------------------
ATP system name : CiME 2.01
People : Benjamin Monate, Evelyn Contejean
URL : http://cime.lri.fr/
TPTP release : v3.5.0
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 : 11395 problems (11395 in TPTP v3.5.0, 0 since Bugfixed)
10532 IAP-Non
4 UNK-Non
357 TMO-Non
493 UNS-Ass
9 SAT-Sat
863 tested (8%)
502 solutions
58% success, over those tested
4% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Jul 22 06:06:34 EDT 2008
Comments :
-------------------------------------------------------------------------------
ATP system name : Darwin 1.4.3
People : Alexander Fuchs, Peter Baumgartner, Cesare Tinelli
URL : http://goedel.cs.uiowa.edu/Darwin/
TPTP release : v3.5.0
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 : darwin -pl 0 -pmc true -to %d %s
Results format : Solns Time
Results summary : 11395 problems (11395 in TPTP v3.5.0, 0 since Bugfixed)
57 UNK-Non
6632 TMO-Non
1593 THM-Ass
2349 UNS-Ass
256 CSA-Mod
508 SAT-Mod
11395 tested (100%)
4706 solutions
41% success, over those tested
41% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Sat Jul 26 03:48:48 EDT 2008
Comments :
-------------------------------------------------------------------------------
ATP system name : DarwinFM 1.4.3
People : Alexander Fuchs, Peter Baumgartner, Cesare Tinelli
URL : http://goedel.cs.uiowa.edu/Darwin/
TPTP release : v3.5.0
Tested on SPCs : FOF_NKT FOF_NKU CNF_NKU
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 : darwin -fd true -ppp true -pl 0 -to %d -pmtptp true %s
Results format : Solns Time
Results summary : 11395 problems (11395 in TPTP v3.5.0, 0 since Bugfixed)
8960 IAP-Non
1 UNK-Non
1332 TMO-Non
333 CSA-FMo
769 SAT-FMo
2435 tested (21%)
1102 solutions
45% success, over those tested
10% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Sat Jul 26 11:35:55 EDT 2008
Comments :
-------------------------------------------------------------------------------
ATP system name : DCTP 1.31
People : Gernot Stenz, Reinhold Letz
URL :
TPTP release : v3.5.0
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 : 11395 problems (11395 in TPTP v3.5.0, 0 since Bugfixed)
5049 IAP-Non
746 UNK-Non
587 GUP-Non
1787 TMO-Non
2723 UNS-Ass
503 SAT-Ass
6346 tested (56%)
3226 solutions
51% success, over those tested
28% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Jul 22 06:06:34 EDT 2008
Comments :
-------------------------------------------------------------------------------
ATP system name : E 1.0pre
People : Stephan Schulz
URL : http://www.eprover.org/
TPTP release : v3.5.0
Tested on SPCs : FOF CNF
tptp2X flags : -f tptp:raw -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 : eprover -s --print-statistics -xAuto -tAuto --cpu-limit=%d --memory-limit=Auto --tstp-in %s
Results format : Solns Time Generated NonTrivial Processed
Results summary : 11395 problems (11395 in TPTP v3.5.0, 0 since Bugfixed)
1 UNK-Non
4082 TMO-Non
2437 THM-Ass
4082 UNS-Ass
309 CSA-Ass
484 SAT-Ass
11395 tested (100%)
7312 solutions
64% success, over those tested
64% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Jul 22 06:06:34 EDT 2008
Comments :
-------------------------------------------------------------------------------
ATP system name : E-KRHyper 1.1
People : Bjorn Pelzer
URL : http://www.uni-koblenz.de/~bpelzer/ekrhyper/
TPTP release : v3.5.0
Tested on SPCs : CNF
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 : casc/ekrhyper %s
Results format : Solns Time Disjuntcions Depth Closed Evaluations
Results summary : 11395 problems (11395 in TPTP v3.5.0, 0 since Bugfixed)
5049 IAP-Non
4120 UNK-Non
77 TMO-Non
1939 UNS-CRf
210 SAT-Ass
6346 tested (56%)
2149 solutions
34% success, over those tested
19% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Jul 22 06:06:34 EDT 2008
Comments :
-------------------------------------------------------------------------------
ATP system name : EQP 0.9d
People : William McCune
URL : http://www.cs.unm.edu/~mccune/eqp/
TPTP release : v3.5.0
Tested on SPCs : CNF_UEQ
tptp2X flags : -f eqp -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 : eqp_wrapper %s
Results format : Solns Time Clauses Given
Results summary : 11395 problems (11395 in TPTP v3.5.0, 0 since Bugfixed)
10532 IAP-Non
321 UNK-Non
1 TMO-Non
541 UNS-Ref
863 tested (8%)
541 solutions
63% success, over those tested
5% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Jul 22 06:06:34 EDT 2008
Comments :
-------------------------------------------------------------------------------
ATP system name : Equinox 1.3
People : Koen Claessen
URL : http://www.cs.chalmers.se/~koen/folkung/
TPTP release : v3.5.0
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 : equinox --tstp --split %s
Results format : Solns Time
Results summary : 11395 problems (11395 in TPTP v3.5.0, 0 since Bugfixed)
108 UNK-Non
788 GUP-Non
6476 TMO-Non
1878 THM-Ass
2145 UNS-Ass
11395 tested (100%)
4023 solutions
35% success, over those tested
35% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Jul 22 06:06:34 EDT 2008
Comments :
-------------------------------------------------------------------------------
ATP system name : Fampire 1.3
People : Josef Urban
URL : http://dreamers.com/lichlair/imagenes/bloodredmoon3.jpg
TPTP release : v3.5.0
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 : 11395 problems (11395 in TPTP v3.5.0, 0 since Bugfixed)
6346 IAP-Non
2239 UNK-Non
304 TMO-Non
2338 THM-Ass
78 UNS-Ass
72 CSA-Ass
18 SAT-Ass
5049 tested (44%)
2506 solutions
50% success, over those tested
22% 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 : 11395 problems (11395 in TPTP v3.5.0, 0 since Bugfixed)
4640 UNK-Non
4868 TMO-Non
595 THM-Ref
5 THM-Ass
1287 UNS-Ref
11395 tested (100%)
1887 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 : FDP 0.9.16
People : Peter Baumgartner
URL :
TPTP release : v3.5.0
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 : 11395 problems (11395 in TPTP v3.5.0, 0 since Bugfixed)
5049 IAP-Non
1169 UNK-Non
168 GUP-Non
2700 TMO-Non
1904 UNS-Ass
405 SAT-Ass
6346 tested (56%)
2309 solutions
36% success, over those tested
20% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Jul 22 06:06:34 EDT 2008
Comments : Flags: -q -a
-------------------------------------------------------------------------------
ATP system name : Fiesta 2
People : Robert Nieuwenhuis
URL :
TPTP release : v3.5.0
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 : 11395 problems (11395 in TPTP v3.5.0, 0 since Bugfixed)
10532 IAP-Non
40 UNK-Non
230 TMO-Non
593 UNS-Ref
863 tested (8%)
593 solutions
69% success, over those tested
5% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Jul 22 06:06:34 EDT 2008
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 : 11395 problems (11395 in TPTP v3.5.0, 0 since Bugfixed)
5049 IAP-Non
2460 UNK-Non
311 TMO-Non
3575 UNS-Ass
6346 tested (56%)
3575 solutions
56% success, over those tested
31% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Jul 22 06:06:34 EDT 2008
Comments :
-------------------------------------------------------------------------------
ATP system name : Geo 2007f
People : Hans de Nivelle
URL : http://www.ii.uni.wroc.pl/~nivelle/software/geo/
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 @ 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 : 11395 problems (11395 in TPTP v3.5.0, 0 since Bugfixed)
749 UNK-Non
93 GUP-Non
6090 TMO-Non
1264 THM-Ref
2261 UNS-Ref
318 CSA-Mod
620 SAT-Mod
11395 tested (100%)
4463 solutions
39% success, over those tested
39% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Jul 22 06:06:34 EDT 2008
Comments :
-------------------------------------------------------------------------------
ATP system name : GrAnDe 1.1
People : Stephan Schulz, Geoff Sutcliffe
URL : http://www.cs.miami.edu/~tptp/ATPSystems/GrAnDe/
TPTP release : v3.5.0
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 : 11395 problems (11395 in TPTP v3.5.0, 0 since Bugfixed)
10612 IAP-Non
181 UNK-Non
5 TMO-Non
453 UNS-Ass
144 SAT-Ass
783 tested (7%)
597 solutions
76% success, over those tested
5% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Jul 22 06:06:34 EDT 2008
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 : iProver 0.5crv
People : Konstantin Korovin
URL : http://www.cs.man.ac.uk/~korovink/iprover/
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 @ 2793MHz
RAM size : 1003MB
Operating system : Linux 2.6.17-1.2142_FC4
Resource limits : 600s
Command/settings : iproveropt --eprover_path /home/graph/tptp/Systems/iProver---0.5crv/ %s
Results format : Solns Time ILoops RLoops PropCalls
Results summary : 11395 problems (11395 in TPTP v3.5.0, 0 since Bugfixed)
844 UNK-Non
51 GUP-Non
4532 TMO-Non
2216 THM-Ass
2827 UNS-Ass
312 CSA-Ass
613 SAT-Ass
11395 tested (100%)
5968 solutions
52% success, over those tested
52% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Jul 22 08:41:22 EDT 2008
Comments :
-------------------------------------------------------------------------------
ATP system name : leanCoP 2.0
People : Jens Otten, Thomas Raths
URL : http://www.leancop.de/
TPTP release : v3.5.0
Tested on SPCs : FOF CNF
tptp2X flags : -f leancop -t stdfof+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 : leancop.sh %s %d
Results format : Solns Time
Results summary : 11395 problems (11395 in TPTP v3.5.0, 0 since Bugfixed)
1451 UNK-Non
6231 TMO-Non
1789 THM-Ass
1716 UNS-Ass
69 CSA-Ass
139 SAT-Ass
11395 tested (100%)
3713 solutions
33% success, over those tested
33% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Jul 22 06:06:34 EDT 2008
Comments :
-------------------------------------------------------------------------------
ATP system name : LeanTAP 2.3
People : Bernhard Beckert
URL : http://www.uni-koblenz.de/~beckert/leantap/
TPTP release : v3.5.0
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 : 11395 problems (11395 in TPTP v3.5.0, 0 since Bugfixed)
3851 UNK-Non
6901 TMO-Non
328 THM-Ass
315 UNS-Ass
11395 tested (100%)
643 solutions
6% success, over those tested
6% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Jul 22 06:06:34 EDT 2008
Comments :
-------------------------------------------------------------------------------
ATP system name : Mace2 2.2
People : William McCune
URL : http://www.cs.unm.edu/~mccune/otter/
TPTP release : v3.5.0
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 : 11395 problems (11395 in TPTP v3.5.0, 0 since Bugfixed)
8963 IAP-Non
995 GUP-Non
861 TMO-Non
102 CSA-Mod
3 CSA-FMo
470 SAT-Mod
1 SAT-FMo
2432 tested (21%)
576 solutions
24% success, over those tested
5% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Jul 22 06:06:34 EDT 2008
Comments : Flags: -N 12 -p -k 100000
-------------------------------------------------------------------------------
ATP system name : Mace4 1207
People : William McCune
URL : http://www.cs.unm.edu/~mccune/prover9/
TPTP release : v3.5.0
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 : 1003MB
Operating system : Linux 2.6.17-1.2142_FC4
Resource limits : 600s
Command/settings : mace4 -c -N -1 -t %d -f %s
Results format : Solns Time Size
Results summary : 11395 problems (11395 in TPTP v3.5.0, 0 since Bugfixed)
8963 IAP-Non
405 UNK-Non
1203 TMO-Non
204 CSA-FMo
620 SAT-FMo
2432 tested (21%)
824 solutions
34% success, over those tested
7% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Jul 22 06:06:34 EDT 2008
Comments :
-------------------------------------------------------------------------------
ATP system name : Matita 0.1.0
People : Andrea Asperti
URL : http://matita.cs.unibo.it/
TPTP release : v3.5.0
Tested on SPCs : CNF_UEQ
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 : DoMatita %d %s
Results format : Solns Time
Results summary : 11395 problems (11395 in TPTP v3.5.0, 0 since Bugfixed)
10532 IAP-Non
67 UNK-Non
274 TMO-Non
522 UNS-Ref
863 tested (8%)
522 solutions
60% success, over those tested
5% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Jul 22 06:06:34 EDT 2008
Comments :
-------------------------------------------------------------------------------
ATP system name : Metis 2.1
People : Joe Hurd
URL : http://www.gilith.com/software/metis
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 @ 2793MHz
RAM size : 1003MB
Operating system : Linux 2.6.17-1.2142_FC4
Resource limits : 600s
Command/settings : metis --show proof --show saturation %s
Results format : Solns Time
Results summary : 11395 problems (11395 in TPTP v3.5.0, 0 since Bugfixed)
1667 UNK-Non
5311 TMO-Non
1557 THM-CRf
2183 UNS-CRf
276 CSA-Ass
379 SAT-Ass
22 SAT-Sat
11395 tested (100%)
4417 solutions
39% success, over those tested
39% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Jul 22 06:06:34 EDT 2008
Comments :
-------------------------------------------------------------------------------
ATP system name : Muscadet 2.7a
People : Dominique Pastre
URL : http://www.math-info.univ-paris5.fr/~pastre/muscadet/muscadet.html
TPTP release : v3.5.0
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 : muscadet %s
Results format : Solns Time
Results summary : 11395 problems (11395 in TPTP v3.5.0, 0 since Bugfixed)
6346 IAP-Non
118 UNK-Non
575 GUP-Non
3184 TMO-Non
1164 THM-Ass
8 UNS-Ass
5049 tested (44%)
1172 solutions
23% success, over those tested
10% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Jul 22 06:06:34 EDT 2008
Comments :
-------------------------------------------------------------------------------
ATP system name : Otter 3.3
People : William McCune
URL : http://www.cs.unm.edu/~mccune/otter/
TPTP release : v3.5.0
Tested on SPCs : FOF CNF
tptp2X flags : -f otter -t add_equality:r
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 : otter-script %s
Results format : Solns Time Given Generated Kept
Results summary : 11395 problems (11395 in TPTP v3.5.0, 0 since Bugfixed)
3 UNK-Non
5989 GUP-Non
1694 TMO-Non
1279 THM-Ref
2430 UNS-Ref
11395 tested (100%)
3709 solutions
33% success, over those tested
33% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Jul 22 06:06:34 EDT 2008
Comments : Flags: set(prolog_style_variables) set(auto) set(tptp_eq)
-------------------------------------------------------------------------------
ATP system name : Paradox 2.3
People : Koen Claessen
URL : http://www.cs.chalmers.se/~koen/folkung/
TPTP release : v3.5.0
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 : 1003MB
Operating system : Linux 2.6.17-1.2142_FC4
Resource limits : 600s
Command/settings : paradox --tstp --model %s
Results format : Solns Time Size
Results summary : 11395 problems (11395 in TPTP v3.5.0, 0 since Bugfixed)
8954 IAP-Non
198 UNK-Non
1131 TMO-Non
329 CSA-FMo
783 SAT-FMo
2441 tested (21%)
1112 solutions
46% success, over those tested
10% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Jul 22 06:06:34 EDT 2008
Comments :
-------------------------------------------------------------------------------
ATP system name : Prover9 1207
People : William McCune
URL : http://www.cs.unm.edu/~mccune/prover9/
TPTP release : v3.5.0
Tested on SPCs : FOF CNF
tptp2X flags : -f prover9 -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 : prover9 -t %d -f %s
Results format : Solns Time Given Generated Kept
Results summary : 11395 problems (11395 in TPTP v3.5.0, 0 since Bugfixed)
1288 UNK-Non
864 GUP-Non
4231 TMO-Non
1678 THM-Ref
3334 UNS-Ref
11395 tested (100%)
5012 solutions
44% success, over those tested
44% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Jul 22 06:06:34 EDT 2008
Comments :
-------------------------------------------------------------------------------
ATP system name : randoCoP 2.0
People : Jens Otten, Thomas Raths
URL :
TPTP release : v3.5.0
Tested on SPCs : FOF CNF
tptp2X flags : -f leancop -t stdfof+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 : randocop.sh %s %d
Results format : Solns Time
Results summary : 11395 problems (11395 in TPTP v3.5.0, 0 since Bugfixed)
974 UNK-Non
6697 TMO-Non
2079 THM-Ass
1495 UNS-Ass
14 CSA-Ass
136 SAT-Ass
11395 tested (100%)
3724 solutions
33% success, over those tested
33% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Jul 22 06:06:34 EDT 2008
Comments :
-------------------------------------------------------------------------------
ATP system name : SETHEO 3.3
People : Reinhold Letz
URL : http://www4.informatik.tu-muenchen.de/~letz/setheo/
TPTP release : v3.5.0
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 : 11395 problems (11395 in TPTP v3.5.0, 0 since Bugfixed)
5049 IAP-Non
348 UNK-Non
2334 GUP-Non
1867 TMO-Non
1797 UNS-Ass
6346 tested (56%)
1797 solutions
28% success, over those tested
16% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Jul 22 06:06:34 EDT 2008
Comments : Flags: inwasm -cons -foldup, sam -dr -cons
-------------------------------------------------------------------------------
ATP system name : S-SETHEO 0.0
People : Reinhold Letz
URL : http://www4.informatik.tu-muenchen.de/~letz/setheo/
TPTP release : v3.5.0
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 : 11395 problems (11395 in TPTP v3.5.0, 0 since Bugfixed)
5049 IAP-Non
4211 UNK-Non
216 TMO-Non
1919 UNS-Ass
6346 tested (56%)
1919 solutions
30% success, over those tested
17% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Jul 22 06:06:34 EDT 2008
Comments :
-------------------------------------------------------------------------------
ATP system name : SNARK 20070805
People : Mark Stickel
URL : http://www.ai.sri.com/~stickel/snark.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 @ 2793MHz
RAM size : 1003MB
Operating system : Linux 2.6.17-1.2142_FC4
Resource limits : 600s
Command/settings : run-snark %s %d
Results format : Solns Time Derived Kept Answers
Results summary : 11395 problems (11395 in TPTP v3.5.0, 0 since Bugfixed)
3039 UNK-Non
432 GUP-Non
3421 TMO-Non
1719 THM-Ref
2784 UNS-Ref
11395 tested (100%)
4503 solutions
40% success, over those tested
40% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Jul 22 06:06:34 EDT 2008
Comments : This is SNARK release 20070805r043
: 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 : v3.5.0
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 : 11395 problems (11395 in TPTP v3.5.0, 0 since Bugfixed)
2229 UNK-Non
460 GUP-Non
4610 TMO-Non
1347 THM-Ref
2749 UNS-Ref
11395 tested (100%)
4096 solutions
36% success, over those tested
36% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Jul 22 06:06:34 EDT 2008
Comments :
-------------------------------------------------------------------------------
ATP system name : SPASS 3.01
People : Christoph Weidenbach
URL : http://spass.mpi-sb.mpg.de/
TPTP release : v3.5.0
Tested on SPCs : FOF CNF
tptp2X flags : -f dfg -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 : SPASS -PGiven=0 -PProblem=0 -DocProof -TimeLimit=%d %s
Results format : Solns Time Memory Derived Kept Used
Results summary : 11395 problems (11395 in TPTP v3.5.0, 0 since Bugfixed)
1955 UNK-Non
9 GUP-Non
3391 TMO-Non
2126 THM-Ref
3147 UNS-Ref
302 CSA-Ass
465 SAT-Ass
11395 tested (100%)
6040 solutions
53% success, over those tested
53% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Jul 22 06:06:34 EDT 2008
Comments :
-------------------------------------------------------------------------------
ATP system name : SRASS 0.1
People : Geoff Sutcliffe
URL : http://www.cs.miami.edu/~tptp/ATPSystems/SRASS/
TPTP release : v3.5.0
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 : 11395 problems (11395 in TPTP v3.5.0, 0 since Bugfixed)
6346 IAP-Non
824 UNK-Non
1870 TMO-Non
2307 THM-Sol
48 THM-Ass
5049 tested (44%)
2355 solutions
47% success, over those tested
21% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Jul 22 06:06:34 EDT 2008
Comments :
-------------------------------------------------------------------------------
ATP system name : Theo 2006
People : Monty Newborn
URL :
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 @ 2793MHz
RAM size : 1003MB
Operating system : Linux 2.6.17-1.2142_FC4
Resource limits : 600s
Command/settings : theo %s -l L1 w0 t%d
Results format : Solns Time
Results summary : 11395 problems (11395 in TPTP v3.5.0, 0 since Bugfixed)
2879 UNK-Non
597 GUP-Non
4313 TMO-Non
1277 THM-Ref
7 UNS-Ass
2322 UNS-Ref
11395 tested (100%)
3606 solutions
32% success, over those tested
32% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Jul 22 06:06:34 EDT 2008
Comments :
-------------------------------------------------------------------------------
ATP system name : Vampire 9.0
People : Andrei Voronkov
URL : http://www.vampire.fm
TPTP release : v3.5.0
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 : jumpirefix --output_syntax tptp -t %d %s
Results format : Solns Time
Results summary : 11395 problems (11395 in TPTP v3.5.0, 0 since Bugfixed)
650 UNK-Non
841 GUP-Non
2965 TMO-Non
2559 THM-Ref
2 THM-Ass
1 UNS-Ass
4271 UNS-Ref
106 SAT-Ass
11395 tested (100%)
6939 solutions
61% success, over those tested
61% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Jul 22 06:06:34 EDT 2008
Comments :
-------------------------------------------------------------------------------
ATP system name : Waldmeister 806
People : Thomas Hillenbrand, Bernd Loechner (WEC)
URL : http://www.waldmeister.org/
TPTP release : v3.5.0
Tested on SPCs : CNF_UEQ
tptp2X flags : -f waldmeister -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 : WaldmeisterII.comp %s
Results format : Solns Time
Results summary : 11395 problems (11395 in TPTP v3.5.0, 0 since Bugfixed)
10532 IAP-Non
2 UNK-Non
2 GUP-Non
168 TMO-Non
686 UNS-Ref
3 SAT-Ass
2 SAT-Sat
863 tested (8%)
691 solutions
80% success, over those tested
6% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Jul 22 06:06:34 EDT 2008
Comments :
-------------------------------------------------------------------------------
ATP system name : zChaff 04.11.15
People : Sharad Malik
URL : http://www.princeton.edu/~chaff
TPTP release : v3.5.0
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 : 11395 problems (11395 in TPTP v3.5.0, 0 since Bugfixed)
11350 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 Jul 22 06:06:34 EDT 2008
Comments :
-------------------------------------------------------------------------------
ATP system name : Zenon 0.5.0
People : Richard Bonichon, David Delahaye, Damien Doligez
URL : http://focal.inria.fr/zenon/
TPTP release : v3.5.0
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 : 11395 problems (11395 in TPTP v3.5.0, 0 since Bugfixed)
6346 IAP-Non
107 UNK-Non
2763 GUP-Non
1083 TMO-Non
1011 THM-Prf
85 UNS-Prf
5049 tested (44%)
1011 solutions
20% success, over those tested
9% success, overall
Submitted by : Geoff Sutcliffe
Inserted : Tue Jul 22 06:06:34 EDT 2008
Comments :
-------------------------------------------------------------------------------