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.
| 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% |