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 ESFOR paper.
The following tests were run on the 753 Horn problems without equality. The time limit is 300 s, the memory limit 500 MB. The version of Darwin used is the same as the one mentioned in the ESFOR workshop paper listed above.
| Configuration | Solved | Time | Memory | Theorem | Non Theorem | Out of Memory | Details |
|---|---|---|---|---|---|---|---|
| Default | 591 | 6.5 | 4.0 | 570 | 21 | 0 | name/rating |
| with Discrimination trees | 592 | 6.0 | 3.9 | 571 | 21 | 0 | name/rating |
| without Subsume | 591 | 6.4 | 4.0 | 570 | 21 | 0 | name/rating |
| without Term Database | 589 | 5.8 | 3.9 | 568 | 21 | 1 | name/rating |
| best inactive candidate | 600 | 7.6 | 4.6 | 579 | 21 | 1 | 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 | 803 | 4.1 | 3.2 | 520 | 283 | 0 | name/rating |
| with Discrimination trees | 801 | 3.7 | 4.0 | 519 | 282 | 0 | name/rating |
| without Subsume | 802 | 4.1 | 3.3 | 520 | 282 | 0 | name/rating |
| without Term Database | 803 | 4.0 | 4.1 | 520 | 283 | 0 | name/rating |
| best inactive candidate | 802 | 4.0 | 3.2 | 519 | 283 | 0 | name/rating |
| Dynamic Backtracking | 804 | 3.9 | 3.4 | 517 | 287 | 0 | name/rating |
| with +v | 730 | 9.0 | 6.4 | 482 | 248 | 32 | name/rating |
The following tests were run on some of the problem sets used at CASC18. The time limit is 500 s, the memory limit 500 MB. See also the results of the CASC18 competition. Note: the reason for unsound derivations are buggy TPTP problems.
| Problems | Configuration | Solved | Time | Memory | Details |
|---|---|---|---|---|---|
| hne / 35 | Default | 18 | 24.0 | 17.3 | name/rating |
| hne / 35 | best inactive candidate | 19 | 23.0 | 20.6 | name/rating |
| heq / 35 | Default | 9 | 23.6 | 12.8 | name/rating |
| heq / 35 | best inactive candidate | 9 | 24.2 | 17.9 | name/rating |
| eps / 35 | Default | 28 | 11.1 | 4.8 | name/rating |
| eps / 35 | best inactive candidate | 28 | 10.0 | 4.8 | name/rating |
| eps / 35 | Dynamic Backtracking | 30 | 3.8 | 6.7 | name/rating |
| eps / 35 | with +v | 29 | 26.9 | 12.6 | name/rating |
| ept / 35 | Default | 33 | 16.8 | 4.5 | name/rating |
| ept / 35 | best inactive candidate | 33 | 18.1 | 4.6 | name/rating |
| ept / 35 | Dynamic Backtracking | 32 | 9.9 | 4.4 | name/rating |
| ept / 35 | with +v | 28 | 7.1 | 4.7 | name/rating |
| nne / 35 | Default | 16 | 7.4 | 3.1 | name/rating |
| nne / 35 | best inactive candidate | 17 | 19.7 | 4.0 | name/rating |
| nne / 35 | Dynamic Backtracking | 16 | 7.7 | 3.6 | name/rating |
| nne / 35 | with +v | 11 | 6.8 | 4.8 | name/rating |
| sne / 35 | Default | 9 | 14.5 | 2.1 | name/rating |
| sne / 35 | best inactive candidate | 9 | 14.1 | 2.1 | name/rating |
| sne / 35 | Dynamic Backtracking | 9 | 15.5 | 4.0 | name/rating |
| sne / 35 | with +v | 6 | 0.0 | 2.5 | name/rating |
The following tests were run on some of the problem sets used at CASC19. The time limit is 500 s, the memory limit 500 MB. See also the results of the CASC19 competition. Note: the reason for unsound derivations are buggy TPTP problems.
| Problems | Configuration | Solved | Time | Memory | Details |
|---|---|---|---|---|---|
| hne / 20 | Default | 10 | 64.9 | 37.4 | name/rating |
| hne / 20 | best inactive candidate | 10 | 33.8 | 32.4 | name/rating |
| heq / 20 | Default | 0 | 0.0 | 0.0 | name/rating |
| heq / 20 | best inactive candidate | 0 | 0.0 | 0.0 | name/rating |
| eps / 35 | Default | 31 | 6.2 | 8.1 | name/rating |
| eps / 35 | best inactive candidate | 31 | 5.4 | 8.2 | name/rating |
| eps / 35 | Dynamic Backtracking | 31 | 5.0 | 7.6 | name/rating |
| eps / 35 | with +v | 31 | 28.5 | 16.6 | name/rating |
| ept / 35 | Default | 31 | 5.6 | 4.5 | name/rating |
| ept / 35 | best inactive candidate | 32 | 19.1 | 5.8 | name/rating |
| ept / 35 | Dynamic Backtracking | 31 | 7.6 | 3.5 | name/rating |
| ept / 35 | with +v | 30 | 29.3 | 5.9 | name/rating |
| nne / 20 | Default | 12 | 16.5 | 6.4 | name/rating |
| nne / 20 | best inactive candidate | 13 | 31.0 | 6.0 | name/rating |
| nne / 20 | Dynamic Backtracking | 10 | 16.8 | 5.4 | name/rating |
| nne / 20 | with +v | 8 | 53.9 | 16.5 | name/rating |
| sne / 35 | Default | 3 | 0.0 | 4.0 | name/rating |
| sne / 35 | best inactive candidate | 3 | 0.0 | 4.0 | name/rating |
| sne / 35 | Dynamic Backtracking | 3 | 0.0 | 2.0 | name/rating |
| sne / 35 | with +v | 2 | 0.0 | 2.0 | name/rating |