Evaluation
Methodology
- Evaluation on 22 problems hard for SPASS 2.1 (no solution
in 600s), randomly choosen.
- SPASS 2.1, 3600s overall time limit
- YuCS
- Using SPASS 2.1 for proofs
- Implements the combinatorial groups algorithm
- Using GeRe - non-contextual transitive relevance combined
by Euclidean distance
- 3600s overall time limit, 60s per attempt
- In YuCS the problems were mostly divided into 6 groups, leading to 64
combinations and 57s per combination
- Hardware: P3 with 256MB, Linux 2.4
Results
- For problems solved by either system:
| Problem
| TPTP
Rating
| SPASS
CPU time
| YuCS
CPU time
| Axioms
| Axioms
Used
| Groups
Used
|
|
| GEO084+1
| 0.50
| 1250
| 434
| 34
| 25
| 4
|
| GEO088+1
| 0.83
| Timeout
| 763
| 34
| 7
| 3
|
| GEO093+1
| 0.67
| 1130
| 435
| 34
| 25
| 4
|
| MGT042+1
| 0.67
| 1879
| Timeout
| 35
|
|
|
| SET199+4
| 0.67
| Timeout
| 1923
| 32
| 14
| 3
|
| SET351+4
| 0.83
| Timeout
| 345
| 32
| 29
| 5
|
| SET595+3
| 0.67
| 1053
| Timeout
| 8
|
|
|
| SET606+3
| 0.67
| Timeout
| 215
| 8
| 6
| 4
|