TF0_THM and TF0_UNS
Highlights
- Systems of Choice : Vampire 4.0 and
CVC4 1.5 and Princess 140704
- Vampire a SOTA contributor in all 5 SPCs
- Vampire best in 2 SPCs
- CVC4 a SOTA contributor in 4 SPCs
- CVC4 best in 2 SPCs, Vampire also a strong SOTA contributor in both,
Princess in 1
- Princess a SOTA contributor in 2 SPCs, best in 1 SPC
- Portfolio approach seems appropriate
SPC Analysis
SOTA Contributors and System Ratings
TF0_THM_NEQ_ARI
Unbiased SPC size 282
SOTA contributors solved 279 = 0.99 SPC 0.99 attempted
SOTA contributors all solved 224 = 0.79 SPC 0.80 SOTA 55 = 1.00 SSR
Princess---140704 C solved 277 = 0.98 SPC 0.99 SOTA 53 = 0.96 SSR
Beagle---0.9 C solved 276 = 0.98 SPC 0.99 SOTA 52 = 0.95 SSR
CVC4---TFA-1.5pre C solved 272 = 0.96 SPC 0.97 SOTA 48 = 0.87 SSR
Vampire---4.0 solved 270 = 0.96 SPC 0.97 SOTA 47 = 0.85 SSR
Z3---4.4-TPTP C solved 229 = 0.81 SPC 0.82 SOTA 5 = 0.09 SSR
TF0_THM_EQU_NAR
Unbiased SPC size 127
SOTA contributors solved 73 = 0.57 SPC 0.57 attempted
SOTA contributors all solved 57 = 0.45 SPC 0.78 SOTA 16 = 1.00 SSR
Vampire---4.0 C solved 70 = 0.55 SPC 0.96 SOTA 13 = 0.81 SSR
CVC4---TFA-1.5pre C solved 60 = 0.47 SPC 0.82 SOTA 3 = 0.19 SSR
TF0_THM_EQU_ARI
Unbiased SPC size 667
SOTA contributors solved 616 = 0.92 SPC 0.92 attempted
SOTA contributors all solved 135 = 0.20 SPC 0.22 SOTA 481 = 1.00 SSR
CVC4---TFA-1.5pre C solved 557 = 0.84 SPC 0.90 SOTA 422 = 0.88 SSR
Vampire---4.0 C solved 556 = 0.83 SPC 0.90 SOTA 421 = 0.88 SSR
Princess---140704 C solved 533 = 0.80 SPC 0.87 SOTA 398 = 0.83 SSR
Beagle---0.9 C solved 487 = 0.73 SPC 0.79 SOTA 352 = 0.73 SSR
SPASS+T---2.2.22 C solved 469 = 0.70 SPC 0.76 SOTA 334 = 0.69 SSR
SNARK---20120808r022 C solved 348 = 0.52 SPC 0.56 SOTA 213 = 0.44 SSR
Zipperpin---TFF-0.4 C solved 274 = 0.41 SPC 0.44 SOTA 139 = 0.29 SSR
TF0_UNS_EQU_NAR
Unbiased SPC size 20
SOTA contributors solved 20 = 1.00 SPC 1.00 attempted
SOTA contributors all solved 10 = 0.50 SPC 0.50 SOTA 10 = 1.00 SSR
CVC4---TFA-1.5pre C solved 20 = 1.00 SPC 1.00 SOTA 10 = 1.00 SSR
Vampire---4.0 R solved 20 = 1.00 SPC 1.00 SOTA 10 = 1.00 SSR
TF0_UNS_EQU_ARI
Unbiased SPC size 20
SOTA contributors solved 12 = 0.60 SPC 0.60 attempted
SOTA contributors all solved 10 = 0.50 SPC 0.83 SOTA 2 = 1.00 SSR
Vampire---4.0 C solved 12 = 0.60 SPC 1.00 SOTA 2 = 1.00 SSR