---- Top classes for unbiased problems ---- Class Z3---4.4-TPTP Subsumes Princess---140704 Yices---1.0.29 Class H2WO4---11.07 Subsumes SPASS-XDB---0.8 Class CVC4---TFA-1.5pre Subsumes Beagle---0.9 ---- Subsumed classes for unbiased problems ---- Class Princess---140704 Subsumes SPASS-XDB---0.8 Class Beagle---0.9 Subsumes CVC4---TFN-1.5pre Class CVC4---TFN-1.5pre Subsumes Yices---1.0.29 Class Yices---1.0.29 Subsumes SPASS-XDB---0.8 Class SPASS-XDB---0.8 Alt-Ergo---0.95.1 leanCoP-Omega---0.1 MetiTarski---1.9 SNARK---20120808r022 SPASS+T---2.2.22 Vampire---4.0 Vampire---SAT-4.0 Zipperpin---TFF-0.4 Subsumes ---- System scores ---- Unbiased SPC size 64 SOTA contributors attempted 64 = 1.00 SPC SOTA contributors solved 46 = 0.72 SPC 0.72 attempted SOTA contributors all solved 25 = 0.39 SPC 0.54 SOTA 21 = 1.00 SSR Z3---4.4-TPTP C solved 43 = 0.67 SPC 0.93 SOTA 18 = 0.86 SSR H2WO4---11.07 C solved 34 = 0.53 SPC 0.74 SOTA 9 = 0.43 SSR Princess---140704 solved 30 = 0.47 SPC 0.65 SOTA 8 = 0.38 SSR CVC4---TFA-1.5pre C solved 29 = 0.45 SPC 0.63 SOTA 4 = 0.19 SSR Beagle---0.9 solved 28 = 0.44 SPC 0.61 SOTA 4 = 0.19 SSR CVC4---TFN-1.5pre solved 27 = 0.42 SPC 0.59 SOTA 4 = 0.19 SSR Yices---1.0.29 solved 20 = 0.31 SPC 0.43 SOTA 3 = 0.14 SSR Alt-Ergo---0.95.1 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR SPASS-XDB---0.8 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR Vampire---SAT-4.0 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR SPASS+T---2.2.22 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR Zipperpin---TFF-0.4 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR Vampire---4.0 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR MetiTarski---1.9 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR leanCoP-Omega---0.1 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR SNARK---20120808r022 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR ---- Systems not in SPC (missing data for some problems) ---- Metis---2.3 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR FIMO---0.3 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR TPS---3.120601S1b solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR VanHElsing---1.0 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR Infinox---1.0 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR Muscadet---4.4 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR Matita---1.0 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR PROTEIN---V2.20 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR SRASS---0.1 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR LeanTaP---2.3 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR Isabelle---2015 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR Ayane---1.1 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR CLIN-S---1.0+ solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR Refute---2015 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR CLIN-E---0.35FM solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR SCOTT---6.1 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR Mace2---2.2 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR SOS---2.0 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR DISCOUNT---2.0-GL solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR GrAnDe---1.1 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR SETHEO---3.3 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR SInE---0.4 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR DCTP---1.31 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR Geo---2010C solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR Prover9---1109a solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR iProver---SAT-1.4 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR CLIN---1.0 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR S-SETHEO---0.0 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR iProver---1.4 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR CVC4---FNT-1.5pre solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR EQP---0.9e solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR Fiesta---2 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR DISCOUNT---TSM2.1 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR Otter---3.3 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR SPTHEO---m256n1 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR Equinox---5.0 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR Satallax---2.7 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR Gandalf---c-2.6 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR Fampire---1.3 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR CARINE---0.734 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR Zipperpin---FOF-0.4 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR Darwin---1.4.5 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR cocATP---0.2.0 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR Mace4---1109a solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR Waldmeister---710 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR ToFoF---0.1 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR E---1.9 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR LEO-II---1.6.2 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR CLIN-S---1.0- solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR PEPR---0.0ps solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR CVC4---FOF-1.5pre solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR DarwinFM---1.4.5 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR Zenon---0.7.1 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR agsyHOL---1.0 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR iProver-Eq---0.85 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR Paradox---4.0 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR leanCoP---2.2 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR ToFoF-SAT---0.1 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR SuperZenon---0.0.1 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR Bliksem---1.12 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR E-Darwin---1.5 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR omkbTT---1.0 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR iProverMo---0.7-0.2 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR CiME---2.01 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR SPASS---3.7 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR LINUS---1.0.1 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR Isabelle-HOT---2015 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR FDP---0.9.16 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR ET---1.0 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR Nitpick---2015 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR randoCoP---1.1 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR HolyHammer---0.0 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR Faust---1.0 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR