TPTP Performance Summary

The following table summarizes the performance of KRHyper on the problems without equality of the TPTP, partitioned into several subclasses. Numbers in brackets represent the total of problems that could be solved with at least one of some different configurations, including the magic sets preprocessing of the TPTP. Limits were 500MB with 650s for Horn and 300s for non-Horn problems on a 2400MHz Pentium computer. For detailed data see the KRHyper Performance Evaluation Page.

Results for KRHyper on all TPTP Problems without Equality
Problem Class Number of Problems Solved by KRHyper
Horn, satisfiable 50 44% [64%]
Horn, unsatisfiable 676 85% [89%]
non-Horn, satisfiable, range restricted, finite H-universe 43 100%
non-Horn, satisfiable, range restricted, infinite H-universe 20 45%
non-Horn, satisfiable, not range restricted, finite H-universe 136 40%
non-Horn, satisfiable, not range restricted, infinite H-universe 164 0%
non-Horn, unsatisfiable, range restricted 235 70%
non-Horn, unsatisfiable, not range restricted 399 34%
remaining problems (TPTP status field ``unknown'' or ``open'') 167 0%