| 137 | -- | 138 | Geoff Sutcliffe, Christian B. Suttner. The CADE-13 ATP System Competition |
| 139 | -- | 162 | Geoff Sutcliffe, Christian B. Suttner. The Design of the CADE-13 ATP System Competition |
| 163 | -- | 169 | Geoff Sutcliffe, Christian B. Suttner. The Procedures of the CADE-13 ATP System Competition |
| 171 | -- | 176 | Robert Nieuwenhuis, José Miguel Rivero, Miguel Ángel Vallejo. Barcelona |
| 177 | -- | 182 | Geoffrey D. Alexander. CLIN-E - Smallest Instance First Hyper-Linking |
| 183 | -- | 188 | Heng Chu, David A. Plaisted. CLIN-S - A Semantically Guided First-Order Theorem Prover |
| 189 | -- | 198 | Jörg Denzinger, Martin Kronenburg, Stephan Schulz. DISCOUNT - A Distributed and Learning Equational Prover |
| 199 | -- | 204 | Tanel Tammet. Gandalf |
| 205 | -- | 210 | Reinhold Letz. LINUS - A Link Instantion Prover with Unit Support |
| 211 | -- | 220 | William McCune, Larry Wos. Otter - The CADE-13 Competition Incarnations |
| 221 | -- | 226 | M. Paramasivam, David A. Plaisted. RRTP - A Replacement Rule Theorem Prover |
| 227 | -- | 236 | Tim Geisler, Sven Panne, Heribert Schütz. Satchmo - The Compiling and Functional Variants |
| 237 | -- | 246 | Max Moser, Ortrun Ibens, Reinhold Letz, Joachim Steinbach, Christoph Goller, Johann Schumann, Klaus Mayr. SETHEO and E-SETHEO - The CADE-13 Systems |
| 247 | -- | 252 | Christoph Weidenbach. SPASS - Version 0.49 |
| 253 | -- | 258 | Christian B. Suttner. SPTHEO - A Parallel Theorem Prover |
| 259 | -- | 264 | Steve Greenbaum. Violet |
| 265 | -- | 270 | Thomas Hillenbrand, Arnim Buch, Roland Vogt, Bernd Löchner. WALDMEISTER - High-Performance Equational Deduction |
| 271 | -- | 286 | Geoff Sutcliffe, Christian B. Suttner. The Results - of the CADE-13 ATP System Competition |
| 287 | -- | 296 | Francis Jeffry Pelletier, Geoff Sutcliffe, Christian B. Suttner. Conclusions about the CADE-13 ATP System Competition |