`TH0_THM`

Highlights

Systems of Choice : Isabelle 2015 and Satallax 2.7
Isabelle and Satallax SOTA contributors in both SPCs
Isabelle and Satallax best two in both SPCs
LEO-II also quite strong in both SPCs

SPC Analysis

TH0_THM_NEQ : Satallax 2.7
TH0_THM_EQU : Isabelle 2015

SOTA Contributors and System Ratings

TH0_THM_NEQ
Unbiased SPC size               548
SOTA contributors      solved   515 = 0.94 SPC 0.94 attempted
SOTA contributors all  solved   209 = 0.38 SPC 0.41 SOTA  306 =  1.00 SSR
Satallax---2.7       C solved   479 = 0.87 SPC 0.93 SOTA  270 =  0.88 SSR
Isabelle---2015      C solved   474 = 0.86 SPC 0.92 SOTA  265 =  0.87 SSR
LEO-II---1.6.2       C solved   445 = 0.81 SPC 0.86 SOTA  236 =  0.77 SSR
TPS---3.120601S1b    C solved   440 = 0.80 SPC 0.85 SOTA  231 =  0.75 SSR
agsyHOL---1.0        C solved   414 = 0.76 SPC 0.80 SOTA  205 =  0.67 SSR
cocATP---0.2.0       C solved   237 = 0.43 SPC 0.46 SOTA   28 =  0.09 SSR

TH0_THM_EQU
Unbiased SPC size              1921
SOTA contributors      solved  1707 = 0.89 SPC 0.89 attempted
SOTA contributors all  solved   399 = 0.21 SPC 0.23 SOTA 1308 =  1.00 SSR
Isabelle---2015      C solved  1537 = 0.80 SPC 0.90 SOTA 1138 =  0.87 SSR
Satallax---2.7       C solved  1509 = 0.79 SPC 0.88 SOTA 1110 =  0.85 SSR
LEO-II---1.6.2       C solved  1339 = 0.70 SPC 0.78 SOTA  940 =  0.72 SSR
agsyHOL---1.0        C solved  1317 = 0.69 SPC 0.77 SOTA  918 =  0.70 SSR
cocATP---0.2.0       C solved   487 = 0.25 SPC 0.29 SOTA   88 =  0.07 SSR