---- Top classes for unbiased problems ---- Class DarwinFM---1.4.3 Subsumes Paradox---3.0 Metis---2.1 Class iProver---0.5c Subsumes SPASS---3.01 Darwin---1.4.3 Class Geo---2007f Subsumes Mace2---2.2 leanCoP---2.0 ---- Subsumed classes for unbiased problems ---- Class Paradox---3.0 Subsumes Mace4---0908 Mace2---2.2 Class SPASS---3.01 Subsumes E---1.0 Mace2---2.2 Class Darwin---1.4.3 Subsumes Mace2---2.2 leanCoP---2.0 Metis---2.1 Class Mace4---0908 Subsumes leanCoP---2.0 Fampire---1.3 Class E---1.0 Subsumes leanCoP---2.0 Fampire---1.3 Class Mace2---2.2 Subsumes Fampire---1.3 Class Metis---2.1 Subsumes Bliksem---1.12 Class leanCoP---2.0 randoCoP---1.1 Subsumes Bliksem---1.12 Class Fampire---1.3 Subsumes Bliksem---1.12 Class Bliksem---1.12 Equinox---3.0 LeanTAP---2.3 Muscadet---3.0 OSHL-S---0.1 Otter---3.3 Prover9---0908 SInE---0.3 SNARK---20080805 SOS---2.0 SRASS---0.1 Theo---2006 Vampire---10.0 VampireLT---10.0 Zenon---0.5.0 Subsumes ---- System scores ---- Unbiased SPC size 38 SOTA contributors attempted 38 = 1.00 SPC SOTA contributors solved 36 = 0.95 SPC 0.95 attempted SOTA contributors all solved 29 = 0.76 SPC 0.81 SOTA 7 = 1.00 SSR DarwinFM---1.4.3 C solved 35 = 0.92 SPC 0.97 SOTA 6 = 0.86 SSR iProver---0.5c C solved 35 = 0.92 SPC 0.97 SOTA 6 = 0.86 SSR Darwin---1.4.3 solved 31 = 0.82 SPC 0.86 SOTA 6 = 0.86 SSR Paradox---3.0 solved 34 = 0.89 SPC 0.94 SOTA 5 = 0.71 SSR SPASS---3.01 solved 33 = 0.87 SPC 0.92 SOTA 5 = 0.71 SSR Mace4---0908 solved 33 = 0.87 SPC 0.92 SOTA 5 = 0.71 SSR E---1.0 solved 32 = 0.84 SPC 0.89 SOTA 5 = 0.71 SSR Metis---2.1 solved 3 = 0.08 SPC 0.08 SOTA 3 = 0.43 SSR Geo---2007f C solved 31 = 0.82 SPC 0.86 SOTA 2 = 0.29 SSR Mace2---2.2 solved 24 = 0.63 SPC 0.67 SOTA 0 = 0.00 SSR leanCoP---2.0 solved 18 = 0.47 SPC 0.50 SOTA 0 = 0.00 SSR randoCoP---1.1 solved 18 = 0.47 SPC 0.50 SOTA 0 = 0.00 SSR Fampire---1.3 solved 16 = 0.42 SPC 0.44 SOTA 0 = 0.00 SSR SNARK---20080805 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 Vampire---10.0 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR Muscadet---3.0 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 Equinox---3.0 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR Theo---2006 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR OSHL-S---0.1 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR Zenon---0.5.0 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 SInE---0.3 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR Prover9---0908 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 VampireLT---10.0 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 ---- Systems not in SPC (missing data for some problems) ---- SCOTT---6.1 solved 17 = 0.45 SPC 0.47 SOTA 0 = 0.00 SSR Matita---0.1.0 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 Gandalf---c-2.6 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 EQP---0.9d 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 CLIN-S---1.0+ 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 CLIN-E---0.35FM solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR TPS---3.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 LEO-II---0.99 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR zChaff---04.11.15 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 E-KRHyper---1.1 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 Vampire---9.0 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 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 E-Darwin---1.0 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 FDP---0.9.16 solved 0 = 0.00 SPC 0.00 SOTA 0 = 0.00 SSR Waldmeister---806 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 Faust---1.0 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