- ... Berre1
- This work has been supported in part by the IUT de Lens, the Université d'Artois and by the ``Région Nord/Pas-de-Calais'' under the TACT-TIC project.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
- ... Hirsch2
- Supported in part by RFBR grant No. 02-01-00089 and by grant No. 1 of
the 6th RAS contest-expertise of young scientists projects (1999).
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
- ... 19963
- Benchmarks available at
http://www.cirl.uoregon.edu/crawford/beijing/
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
- ... web4
- At:
http://www.satlive.org/SATCompetition/cfs.html
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
- ... format5
- This was more precisely a restriction of this format,
as described in our call for benchmarks
(http://www.satlive.org/SATCompetition/cfb.html)
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
- ... solvers6
- http://www.satlive.org/SATCompetition/cfs.html
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
- ... system7
- Linux-SMP 2.4.3, solvers binaries compiled by gcc 2.96
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
- ... SATLIB8
- http://www.satlib.org/
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
- ... CASC9
-
CASC=``CADE ATP System Competition'',
CADE=``Conference on Automated Deduction'',
ATP=``Automated Theorem Proving'',
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
- ... difficult10
- A degree of difficulty can be computed using the
ratio number of failing SOTA contributors over the total number of
SOTA contributors.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
- ... chosen11
- Based only on the number of benchmarks/solvers and
machines
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.