ATP Systems with Arithmetic
ATP Systems
- Main players ... Alt-Ergo, Beagle, CVC3, CVC4, Isabelle/Nitrox,
MetiTarski, Princess, SNARK, SPASS+T, Z3, Zipperposition
- Available in SystemOnTPTP
|
| System
| THM/UNS
| Unique
| CSA/SAT
| Unique
|
|
| Problems
| 1323
|
| 89
|
|
| Beagle 0.8.2
| 793
| 6
| 31
| 0
|
| Princess 140602
| 759
| 3
| 29
| 0
|
| Z3 4.4
| 694
| 14
| 48
| 2
|
| SPASS+T 2.2.19
| 653
| 2
| 0
| 0
|
| CVC3 2.4
| 565
| 3
| 24
| 0
|
| SNARK 20120808r022
| 531
| 0
| 0
| 0
|
| MetiTarski 1.9
| 426
| 0
| 0
| 0
|
| Alt-Ergo 0.95.1
| 282
| 5
| 0
| 0
|
| Isabelle/Nitrox 2013
| 152
| 3
| 67
| 17
|
| CVC4 1.3
| ???
|
| ??
|
|
| Zipperposition 0.4
| ???
|
| ??
|
|
|
| Union
| 876
| 36
| 70
| 19
|
|