The following tests were run on a Pentium IV 2.4 Ghz with 512 MB RAM under SUSe Linux 9.0 on the TPTP version 2.6. The Time/Memory columns give the average time spent on the solved problems - but due to sharing the test computer with other processes these results are not highly reliable. The detailed results are given sorted by name and rating in the Details column. Detailed explanations for the configurations and results are given in the handbook.
The following tests were run on the 753 Horn problems without equality. The time limit is 300 s, the memory limit 500 MB.
| Configuration | Solved | Time | Memory | Theorem | Non Theorem | Out of Memory | Details |
|---|---|---|---|---|---|---|---|
| Default | 599 | 5.4 | 4.7 | 578 | 21 | 0 | name/rating |
| without Subsume | 599 | 5.5 | 3.0 | 578 | 21 | 0 | name/rating |
| without Resolve | 599 | 5.4 | 2.9 | 578 | 21 | 0 | name/rating |
| without Compact | 599 | 5.4 | 3.0 | 578 | 21 | 0 | name/rating |
| without Indexing | 592 | 6.9 | 2.8 | 571 | 21 | 0 | name/rating |
| without Splitt-less Horn | 594 | 4.5 | 4.4 | 573 | 21 | 0 | name/rating |
The following tests were run on the 1172 non-Horn problems without equality. The time limit is 300 s, the memory limit 500 MB. Note: the reason for unsound derivations are buggy TPTP problems.
| Configuration | Solved | Time | Memory | Theorem | Non Theorem | Out of Memory | Details |
|---|---|---|---|---|---|---|---|
| Default | 875 | 4.2 | 3.3 | 544 | 331 | 1 | name/rating |
| without Subsume | 875 | 4.3 | 3.3 | 544 | 331 | 1 | name/rating |
| without Resolve | 857 | 7.8 | 4.6 | 543 | 314 | 1 | name/rating |
| without Compact | 875 | 4.2 | 3.3 | 544 | 331 | 1 | name/rating | without Productivity | 819 | 5.0 | 3.7 | 530 | 289 | 0 | name/rating |
| Naive Backtracking | 844 | 4.0 | 3.1 | 515 | 329 | 1 | name/rating |
| Dynamic Backtracking | 866 | 4.4 | 3.3 | 535 | 331 | 1 | name/rating |
| without Mixed Literals | 875 | 4.3 | 3.3 | 544 | 331 | 1 | name/rating |
| with +v | 816 | 6.6 | 4.5 | 521 | 295 | 32 | name/rating |
| without Indexing | 859 | 4.3 | 3.2 | 532 | 327 | 0 | name/rating |
The following tests were run on all 5473 problems of the TPTP version 2.6. The time limit is 500 s, the memory limit 500 MB. Note: the reason for unsound derivations are buggy TPTP problems.
| Division | Problems | Solved | Time | Memory | Theorem | Non Theorem | Out of Memory | Details |
|---|---|---|---|---|---|---|---|---|
| all | 5473 | 2287 | 13.0 | 5.5 | 1843 | 444 | 55 | name/rating |
| hne | 753 | 604 | 8.9 | 3.4 | 583 | 21 | 1 | name/rating |
| heq | 1403 | 412 | 29.4 | 11.6 | 367 | 45 | 0 | name/rating |
| nne | 1172 | 881 | 6.9 | 4.3 | 549 | 332 | 1 | name/rating |
| neq | 2145 | 390 | 15.9 | 5.0 | 344 | 46 | 53 | name/rating |
The following tests were run with the default configuration on some of the problem sets used at CASC-J2. The time limit is 500 s, the memory limit 500 MB. See also the results of the CASC-J2 competition.
| Division | Problems | Solved | Time | Memory | Details |
|---|---|---|---|---|---|
| hne | 35 | 15 | 16.3 | 7.9 | name/rating | heq | 35 | -- | -- | -- | name/rating | eps | 40 | 40 | 13.0 | 9.2 | name/rating | ept | 40 | 39 | 20.6 | 5.9 | name/rating | nne | 35 | 17 | 19.2 | 5.2 | name/rating | sne | 50 | 17 | 0.1 | 2.0 | name/rating |