... Berre¹

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.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... Hirsch²

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).

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... 1996³

Benchmarks available at http://www.cirl.uoregon.edu/crawford/beijing/

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... web⁴

At: http://www.satlive.org/SATCompetition/cfs.html

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... format⁵

This was more precisely a restriction of this format, as described in our call for benchmarks (http://www.satlive.org/SATCompetition/cfb.html)

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... solvers⁶

http://www.satlive.org/SATCompetition/cfs.html

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... system⁷

Linux-SMP 2.4.3, solvers binaries compiled by gcc 2.96

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... SATLIB⁸

http://www.satlib.org/

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... CASC⁹

CASC=``CADE ATP System Competition'', CADE=``Conference on Automated Deduction'', ATP=``Automated Theorem Proving'',

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... difficult¹⁰

A degree of difficulty can be computed using the ratio number of failing SOTA contributors over the total number of SOTA contributors.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... chosen¹¹

Based only on the number of benchmarks/solvers and machines

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.