System Rating by SOTA

Approach

• Easy problems are solved by all decent systems, and
  Unsolved problems do not differentiate between systems
  • Use difficult problems

Rating Scheme

• The fraction of difficult problems it can solve

                Number of difficult problems solved by the system
  Rating = -----------------------------------------------------------
           Number of difficult problems solved by any SOTA contributor     

Example Results: THM_RFO_NEQ_CNF_NHN

SPC size                        107
SOTA contributors      solved   104
SOTA contributors all  solved    90 = 0.87 SOTA   14 = 1.00 SSR

E-SETHEO---99csp    SC solved   101 = 0.97 SOTA   11 = 0.79 SSR
SPASS---0.99T       SC solved   100 = 0.96 SOTA   10 = 0.71 SSR
Gandalf---c-1.0d       solved    95 = 0.91 SOTA    8 = 0.57 SSR
E---0.32               solved    95 = 0.91 SOTA    5 = 0.36 SSR
Vampire---0.0       SC solved    95 = 0.91 SOTA    5 = 0.36 SSR
S-SETHEO---0.0         solved    76 = 0.73 SOTA    4 = 0.29 SSR
OtterMACE---437        solved    85 = 0.82 SOTA    2 = 0.14 SSR
Bliksem---1.01         solved    84 = 0.81 SOTA    1 = 0.07 SSR
PROTEIN---V2.20        solved    64 = 0.62 SOTA    0 = 0.00 SSR
  ...