---- Top classes for unbiased problems ---- Class Alt-Ergo---0.95.1 Subsumes ---- Subsumed classes for unbiased problems ---- ---- System scores ---- Unbiased SPC size 537 SOTA contributors attempted 537 = 1.00 SPC SOTA contributors solved 193 = 0.36 SPC 0.36 attempted SOTA contributors all solved 193 = 0.36 SPC 1.00 SOTA 0 = 1.00 SSR Alt-Ergo---0.95.1 C solved 193 = 0.36 SPC 1.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 Princess---140704 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 SPASS-XDB---0.8 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 Z3---4.4-TPTP 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 CVC4---TFA-1.5pre 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 r 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 Vampire---SAT-4.0 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 SPASS+T---2.2.22 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 r 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 Zipperpin---TFF-0.4 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 Vampire---4.0 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR H2WO4---11.07 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 Beagle---0.9 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 MetiTarski---1.9 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 leanCoP-Omega---0.1 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 CVC4---TFN-1.5pre 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 SNARK---20120808r022 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 Yices---1.0.29 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR