`CNF_UNS`

Highlights

Systems of Choice : E 1.9 and Vampire 4.0
E a SOTA contributor in 6 SPCs
E best in 4 SPCs
- Vampire also strong in these SPCs
Vampire a SOTA contributor in all 7 SPCs
Vampire best in 3 SPCs
- E also strong in 2 of these SPCs
- iProver beaten in CNF_UNS_EPR
Combination of E and Vampire good for CNF_UNS

SPC Analysis

SOTA Contributors and System Ratings

CNF_UNS_EPR
Unbiased SPC size               649
SOTA contributors      solved   592 = 0.91 SPC 0.91 attempted
SOTA contributors all  solved   412 = 0.63 SPC 0.70 SOTA  180 =  1.00 SSR
Vampire---4.0        C solved   588 = 0.91 SPC 0.99 SOTA  176 =  0.98 SSR
iProver---1.4        C solved   556 = 0.86 SPC 0.94 SOTA  144 =  0.80 SSR
CVC4---FOF-1.5pre    C solved   469 = 0.72 SPC 0.79 SOTA   57 =  0.32 SSR
GrAnDe---1.1         C solved   438 = 0.67 SPC 0.74 SOTA   26 =  0.14 SSR

CNF_UNS_RFO_NEQ_HRN
Unbiased SPC size               543
SOTA contributors      solved   530 = 0.98 SPC 0.98 attempted
SOTA contributors all  solved   406 = 0.75 SPC 0.77 SOTA  124 =  1.00 SSR
E---1.9              C solved   525 = 0.97 SPC 0.99 SOTA  119 =  0.96 SSR
Vampire---4.0        C solved   508 = 0.94 SPC 0.96 SOTA  102 =  0.82 SSR
Darwin---1.4.5       C solved   470 = 0.87 SPC 0.89 SOTA   64 =  0.52 SSR
Prover9---1109a      C solved   457 = 0.84 SPC 0.86 SOTA   51 =  0.41 SSR

CNF_UNS_RFO_NEQ_NHN
Unbiased SPC size               481
SOTA contributors      solved   463 = 0.96 SPC 0.96 attempted
SOTA contributors all  solved   191 = 0.40 SPC 0.41 SOTA  272 =  1.00 SSR
Vampire---4.0        C solved   452 = 0.94 SPC 0.98 SOTA  261 =  0.96 SSR
E---1.9              C solved   441 = 0.92 SPC 0.95 SOTA  250 =  0.92 SSR
ET---1.0             C solved   437 = 0.91 SPC 0.94 SOTA  246 =  0.90 SSR
CVC4---FOF-1.5pre    C solved   397 = 0.83 SPC 0.86 SOTA  206 =  0.76 SSR
Geo---2010C          C solved   389 = 0.81 SPC 0.84 SOTA  198 =  0.73 SSR
Prover9---1109a      C solved   379 = 0.79 SPC 0.82 SOTA  188 =  0.69 SSR
Equinox---5.0        C solved   216 = 0.45 SPC 0.47 SOTA   25 =  0.09 SSR

CNF_UNS_RFO_SEQ_HRN
Unbiased SPC size               450
SOTA contributors      solved   429 = 0.95 SPC 0.95 attempted
SOTA contributors all  solved   212 = 0.47 SPC 0.49 SOTA  217 =  1.00 SSR
E---1.9              C solved   421 = 0.94 SPC 0.98 SOTA  209 =  0.96 SSR
Vampire---4.0        C solved   389 = 0.86 SPC 0.91 SOTA  177 =  0.82 SSR
Isabelle---2015      C solved   347 = 0.77 SPC 0.81 SOTA  135 =  0.62 SSR
Prover9---1109a      C solved   333 = 0.74 SPC 0.78 SOTA  121 =  0.56 SSR
SNARK---20120808r022 C solved   294 = 0.65 SPC 0.69 SOTA   82 =  0.38 SSR
Geo---2010C          C solved   227 = 0.50 SPC 0.53 SOTA   15 =  0.07 SSR

CNF_UNS_RFO_SEQ_NHN
Unbiased SPC size              2280
SOTA contributors      solved  1910 = 0.84 SPC 0.84 attempted
SOTA contributors all  solved   424 = 0.19 SPC 0.22 SOTA 1486 =  1.00 SSR
Vampire---4.0        C solved  1785 = 0.78 SPC 0.93 SOTA 1361 =  0.92 SSR
ET---1.0             C solved  1720 = 0.75 SPC 0.90 SOTA 1296 =  0.87 SSR
E---1.9              C solved  1709 = 0.75 SPC 0.89 SOTA 1285 =  0.86 SSR
CVC4---FOF-1.5pre    C solved  1448 = 0.64 SPC 0.76 SOTA 1024 =  0.69 SSR
Isabelle---2015      C solved  1436 = 0.63 SPC 0.75 SOTA 1012 =  0.68 SSR
Isabelle-HOT---2015  C solved  1423 = 0.62 SPC 0.75 SOTA  999 =  0.67 SSR
Prover9---1109a      C solved  1074 = 0.47 SPC 0.56 SOTA  650 =  0.44 SSR
iProver---1.4        C solved  1059 = 0.46 SPC 0.55 SOTA  635 =  0.43 SSR
DCTP---1.31          C solved  1011 = 0.44 SPC 0.53 SOTA  587 =  0.40 SSR
SNARK---20120808r022 C solved  1011 = 0.44 SPC 0.53 SOTA  587 =  0.40 SSR
Equinox---5.0        C solved   762 = 0.33 SPC 0.40 SOTA  338 =  0.23 SSR

CNF_UNS_RFO_PEQ_NUE
Unbiased SPC size               541
SOTA contributors      solved   469 = 0.87 SPC 0.87 attempted
SOTA contributors all  solved    11 = 0.02 SPC 0.02 SOTA  458 =  1.00 SSR
E---1.9              C solved   431 = 0.80 SPC 0.92 SOTA  420 =  0.92 SSR
ET---1.0             C solved   423 = 0.78 SPC 0.90 SOTA  412 =  0.90 SSR
Vampire---4.0        C solved   386 = 0.71 SPC 0.82 SOTA  375 =  0.82 SSR
Isabelle---2015      C solved   384 = 0.71 SPC 0.82 SOTA  373 =  0.81 SSR
SPASS---3.7          C solved   339 = 0.63 SPC 0.72 SOTA  328 =  0.72 SSR
Prover9---1109a      C solved   332 = 0.61 SPC 0.71 SOTA  321 =  0.70 SSR
CVC4---FOF-1.5pre    C solved   314 = 0.58 SPC 0.67 SOTA  303 =  0.66 SSR
E-Darwin---1.5       C solved   264 = 0.49 SPC 0.56 SOTA  253 =  0.55 SSR
SNARK---20120808r022 C solved   162 = 0.30 SPC 0.35 SOTA  151 =  0.33 SSR
Bliksem---1.12       C solved    63 = 0.12 SPC 0.13 SOTA   52 =  0.11 SSR

CNF_UNS_RFO_PEQ_UEQ
Unbiased SPC size               897
SOTA contributors      solved   847 = 0.94 SPC 0.94 attempted
SOTA contributors all  solved    25 = 0.03 SPC 0.03 SOTA  822 =  1.00 SSR
E---1.9              C solved   755 = 0.84 SPC 0.89 SOTA  730 =  0.89 SSR
ET---1.0             C solved   754 = 0.84 SPC 0.89 SOTA  729 =  0.89 SSR
Waldmeister---710    C solved   732 = 0.82 SPC 0.86 SOTA  707 =  0.86 SSR
Vampire---4.0        C solved   718 = 0.80 SPC 0.85 SOTA  693 =  0.84 SSR
Prover9---1109a      C solved   687 = 0.77 SPC 0.81 SOTA  662 =  0.81 SSR
Isabelle---2015      C solved   670 = 0.75 SPC 0.79 SOTA  645 =  0.78 SSR
Fiesta---2           C solved   633 = 0.71 SPC 0.75 SOTA  608 =  0.74 SSR
SPASS---3.7          C solved   600 = 0.67 SPC 0.71 SOTA  575 =  0.70 SSR
LEO-II---1.6.2       C solved   592 = 0.66 SPC 0.70 SOTA  567 =  0.69 SSR
SNARK---20120808r022 C solved   590 = 0.66 SPC 0.70 SOTA  565 =  0.69 SSR
EQP---0.9e           C solved   571 = 0.64 SPC 0.67 SOTA  546 =  0.66 SSR
Metis---2.3          C solved   543 = 0.61 SPC 0.64 SOTA  518 =  0.63 SSR
CiME---2.01          C solved   519 = 0.58 SPC 0.61 SOTA  494 =  0.60 SSR
Bliksem---1.12       C solved   439 = 0.49 SPC 0.52 SOTA  414 =  0.50 SSR
CVC4---FOF-1.5pre    C solved   422 = 0.47 SPC 0.50 SOTA  397 =  0.48 SSR
Geo---2010C          C solved   318 = 0.35 SPC 0.38 SOTA  293 =  0.36 SSR
S-SETHEO---0.0       C solved   118 = 0.13 SPC 0.14 SOTA   93 =  0.11 SSR