{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T14:52:00Z","timestamp":1761922320319,"version":"build-2065373602"},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2000,4,1]],"date-time":"2000-04-01T00:00:00Z","timestamp":954547200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2000,4,1]],"date-time":"2000-04-01T00:00:00Z","timestamp":954547200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Automated Reasoning"],"published-print":{"date-parts":[[2000,4]]},"DOI":"10.1023\/a:1006393501098","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T01:36:27Z","timestamp":1040520987000},"page":"371-396","source":"Crossref","is-referenced-by-count":26,"title":["The CADE-16 ATP System Competition"],"prefix":"10.1007","volume":"24","author":[{"given":"Geoff","family":"Sutcliffe","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"254252_CR1","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1016\/0004-3702(71)90004-X","volume":"2","author":"W. Bledsoe","year":"1971","unstructured":"Bledsoe, W.: 1971, Splitting and reduction heuristics in automatic theorem proving, Artif. Intell.\n2, 55-77.","journal-title":"Artif. Intell."},{"key":"254252_CR2","series-title":"Technical Report I9638","volume-title":"A probablistic stopping criterion for the evaluation of benchmarks","author":"M. Greiner","year":"1996","unstructured":"Greiner, M. and M. Schramm: 1996, A probablistic stopping criterion for the evaluation of benchmarks, Technical Report I9638, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, M\u00fcnchen, Germany."},{"key":"254252_CR3","doi-asserted-by":"crossref","unstructured":"Hillenbrand, T., Jaeger, A. and L\u00f6chner, B.: 1999, Waldmeister-improvements in performance and ease of use, in H. Ganzinger (ed.), Proceedings of the 16th International Conference on Automated Deduction, pp. 232-236.","DOI":"10.1007\/3-540-48660-7_20"},{"issue":"2","key":"254252_CR4","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1023\/A:1005808119103","volume":"18","author":"M. Moser","year":"1997","unstructured":"Moser, M., Ibens, O., Letz, R., Steinbach, J., Goller, C., Schumann, J. and Mayr, K.: 1997, SETHEO and E-SETHEO: The CADE-13 systems, J. Automated Reasoning\n18(2), 237-246.","journal-title":"J. Automated Reasoning"},{"key":"254252_CR5","doi-asserted-by":"crossref","unstructured":"Nonnengart, A. Rock, G. and Weidenbach, C.: 1998, On generating small clause normal forms, in C. Kirchner and H. Kirchner (eds.), Proceedings of the 15th International Conference on Automated Deduction, pp. 397-411.","DOI":"10.1007\/BFb0054274"},{"key":"254252_CR6","unstructured":"Nonnengart, A. and Weidenbach, C.: 1999, On generating small clause normal forms, in A. Robinson and A. Voronkov (eds.), Handbook of Automated Reasoning, Elsevier Science."},{"key":"254252_CR7","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0004-3702(78)90028-0","volume":"10","author":"D. Pastre","year":"1978","unstructured":"Pastre, D.: 1978, Automatic theorem proving in set theory, Artif. Intell.\n10, 1-27.","journal-title":"Artif. Intell."},{"issue":"1","key":"254252_CR8","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1007\/BF00263451","volume":"8","author":"A. Quaife","year":"1992","unstructured":"Quaife, A.: 1992a, Automated deduction in von Neumann-Bernays-Godel set theory, J. Automated Reasoning\n8(1), 91-147.","journal-title":"J. Automated Reasoning"},{"key":"254252_CR9","unstructured":"Quaife, A.: 1992b, Automated Development of Fundamental Mathematical Theories, Kluwer Academic Publishers."},{"key":"254252_CR10","doi-asserted-by":"crossref","unstructured":"Schulz, S.: 1999, System abstract: E 0.3, in H. Ganzinger (ed.), Proceedings of the 16th International Conference on Automated Deduction, pp. 297-301.","DOI":"10.1007\/3-540-48660-7_27"},{"key":"254252_CR11","unstructured":"Sutcliffe, G.: 1999, Proceedings of the CADE-16 ATP System Competition, Trento, Italy."},{"issue":"2","key":"254252_CR12","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1023\/A:1005839515219","volume":"18","author":"G. Sutcliffe","year":"1997","unstructured":"Sutcliffe, G. and Suttner, C.: 1997a, Special issue: The CADE-13 ATP system competition, J. Automated Reasoning\n18(2), 137-138.","journal-title":"J. Automated Reasoning"},{"issue":"2","key":"254252_CR13","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1023\/A:1005858625038","volume":"18","author":"G. Sutcliffe","year":"1997","unstructured":"Sutcliffe, G. and Suttner, C.: 1997b, The procedures of the CADE-13 ATP system competition, J. Automated Reasoning\n18(2), 163-169.","journal-title":"J. Automated Reasoning"},{"key":"254252_CR14","unstructured":"Sutcliffe, G. and Suttner, C.: 1998a, Proceedings of the CADE-15 ATP System Competition, Lindau, Germany."},{"key":"254252_CR15","series-title":"Technical Report 98\/01","volume-title":"The CADE-14 ATP System Competition","author":"G. Sutcliffe","year":"1998","unstructured":"Sutcliffe, G. and Suttner, C.: 1998b, The CADE-14 ATP System Competition, Technical Report 98\/01, Department of Computer Science, James Cook University, Townsville, Australia."},{"issue":"2","key":"254252_CR16","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1023\/A:1005806324129","volume":"21","author":"G. Sutcliffe","year":"1998","unstructured":"Sutcliffe, G. and Suttner, C.: 1998c, The TPTP problem library: CNF release v1.2.1, J. Automated Reasoning\n21(2), 177-203.","journal-title":"J. Automated Reasoning"},{"issue":"1","key":"254252_CR17","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1023\/A:1006285423991","volume":"23","author":"G. Sutcliffe","year":"1999","unstructured":"Sutcliffe, G. and Suttner, C.: 1999, The CADE-15 ATP system competition, J. Automated Reasoning\n23(1), 1-23.","journal-title":"J. Automated Reasoning"},{"key":"254252_CR18","doi-asserted-by":"crossref","unstructured":"Suttner, C. and Schumann, J.: 1994, Parallel automated theorem proving, in L. Kanal, V. Kumar, H. Kitano, and C. Suttner (eds.), Parallel Processing for Artificial Intelligence 1, Elsevier Science, pp. 209-257.","DOI":"10.1016\/B978-0-444-81704-4.50015-6"},{"issue":"2","key":"254252_CR19","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1023\/A:1005802523220","volume":"18","author":"C. Suttner","year":"1997","unstructured":"Suttner, C. and Sutcliffe, G.: 1997, The design of the CADE-13 ATP system competition, J. Automated Reasoning\n18(2), 139-162.","journal-title":"J. Automated Reasoning"},{"issue":"1","key":"254252_CR20","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1023\/A:1006006930186","volume":"21","author":"C. Suttner","year":"1998","unstructured":"Suttner, C. and Sutcliffe, G.: 1998, The CADE-14 ATP system competition, J. Automated Reasoning\n21(1), 99-134.","journal-title":"J. Automated Reasoning"},{"issue":"2","key":"254252_CR21","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1007\/BF00881918","volume":"15","author":"A. Voronkov","year":"1995","unstructured":"Voronkov, A.: 1995, The anatomy of vampire, J. Automated Reasoning\n15(2), 237-265.","journal-title":"J. Automated Reasoning"},{"key":"254252_CR22","unstructured":"Weidenbach, C.: 1999, SPASS: Combining superposition, sorts and splitting, in A. Robinson and A. Voronkov (eds.), Handbook of Automated Reasoning, Elsevier Science."},{"key":"254252_CR23","doi-asserted-by":"crossref","unstructured":"Weidenbach, C., Afshordel, B., Brahm, U., Cohrs, C., Engel, T., Keen, E., Theobalt, C. and Tpoic, D.: 1999, System description: SPASS version 1.0.0, in H. Ganzinger (ed.), Proceedings of the 16th International Conference on Automated Deduction, pp. 378-382.","DOI":"10.1007\/3-540-48660-7_34"},{"key":"254252_CR24","doi-asserted-by":"crossref","unstructured":"Weidenbach, C., Gaede, B. and Rock, G.: 1996, SPASS and FLOTTER, in M. McRobbie and J. Slaney (eds.), Proceedings of the 13th International Conference on Automated Deduction, pp. 141-145.","DOI":"10.1007\/3-540-61511-3_75"},{"key":"254252_CR25","doi-asserted-by":"crossref","unstructured":"Wolf, A.: 1998a, p-SETHEO: Strategy parallelism in automated theorem proving, in H. de Swart (ed.), Proceedings of International Conference TABLEAUX'98: Analytic Tableaux and Related Methods, pp. 320-324.","DOI":"10.1007\/3-540-69778-0_32"},{"key":"254252_CR26","doi-asserted-by":"crossref","unstructured":"Wolf, A.: 1998b, Strategy selection for automated theorem proving, in F. Giunchiglia (ed.), Proceedings of the 8th International Conference on Artificial Intelligence: Methodology, Systems, Applications (AIMSA), pp. 452-465.","DOI":"10.1007\/BFb0057466"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1006393501098.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1006393501098\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1006393501098.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:34:48Z","timestamp":1749123288000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1006393501098"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,4]]},"references-count":26,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2000,4]]}},"alternative-id":["254252"],"URL":"https:\/\/doi.org\/10.1023\/a:1006393501098","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2000,4]]}}}