Performance
Evaluation Environment
- TPTP v2.4.1
THM_RFO_SEQ_CNF_NHN
- Three systems always
- Resources
- SUN Ultra-80, 1GB RAM
- 300 second CPU time limit (total)
- Soundness
- 484 non-theorems
- Some proved at first, thanks to splitting
- Completeness
- 1745 theorems
- 918 rating 1.00
Results
|
|
| CSSCPA
| E
| Otter
| SPASS
| SSCPA
| SSCPA*
|
|
| Solved by
| 686
| 616
| 364
| 630
| 673
| 723
|
| CCSCPA, not by other
| 131
| 329
| 91
| 75
| 52
|
| other, not by CSSCPA
| 65
| 11
| 39
| 62
| 89
|
|
Solved 25 with rating 1.00