{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:10:04Z","timestamp":1749125404080,"version":"3.41.0"},"reference-count":19,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2002,4,1]],"date-time":"2002-04-01T00:00:00Z","timestamp":1017619200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2002,4,1]],"date-time":"2002-04-01T00:00:00Z","timestamp":1017619200000},"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":[[2002,4]]},"DOI":"10.1023\/a:1015736313131","type":"journal-article","created":{"date-parts":[[2002,12,29]],"date-time":"2002-12-29T00:56:06Z","timestamp":1041123366000},"page":"307-320","source":"Crossref","is-referenced-by-count":5,"title":["The IJCAR ATP System Competition"],"prefix":"10.1007","volume":"28","author":[{"given":"G.","family":"Sutcliffe","sequence":"first","affiliation":[]},{"given":"C. B.","family":"Suttner","sequence":"additional","affiliation":[]},{"given":"F. J.","family":"Pelletier","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"394819_CR1","unstructured":"Avenhaus, J., Hillenbrand, T. and L\u00f6chner, B.: On using ground joinable equations in equational theorem proving, in P. Baumgartner and H. Zhang (eds.), Proceedings of the 3rd International Workshop on First Order Theorem Proving, 2000, pp. 33\u201343."},{"key":"394819_CR2","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Dershowitz, N. and Plaisted, D.: Completion without failure, in H. Ait-Kaci and M. Nivat (eds.), Resolution of Equations in Algebraic Structures, Academic Press, 1989, pp. 1\u201330.","DOI":"10.1016\/B978-0-12-046371-8.50007-9"},{"key":"394819_CR3","doi-asserted-by":"crossref","unstructured":"Baumgartner, P.: FDPLL \u2014 A first order Davis\u2014Putnam\u2014Logeman\u2014Loveland procedure, in: D. McAllester (ed.), Proceedings of the 17th International Conference on Automated Deduction, Springer-Verlag, 2000, pp. 200\u2013219.","DOI":"10.1007\/10721959_16"},{"key":"394819_CR4","doi-asserted-by":"crossref","unstructured":"Hillenbrand, T., Jaeger, A. and L\u00f6chner, B.: Waldmeister \u2014 Improvements in performance and ease of use, in H. Ganzinger (ed.), Proceedings of the 16th International Conference on Automated Deduction, Springer-Verlag, 1999, pp. 232\u2013236.","DOI":"10.1007\/3-540-48660-7_20"},{"key":"394819_CR5","doi-asserted-by":"crossref","unstructured":"Letz, R. and Stenz, G.: System description: DCTP \u2014 A Disconnection Calculus Theorem Prover, in R. Gore, A. Leitsch and T. Nipkow (eds.), Proceedings of the International Joint Conference on Automated Reasoning. Springer-Verlag, 2001, pp. 381\u2013385.","DOI":"10.1007\/3-540-45744-5_30"},{"issue":"2","key":"394819_CR6","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.: SETHEO and E-SETHEO: The CADE-13 systems, J. Automated Reasoning\n18(2) (1997), 237\u2013246.","journal-title":"J. Automated Reasoning"},{"key":"394819_CR7","doi-asserted-by":"crossref","unstructured":"Riazanov, A. and Voronkov, A.: Partiallly adaptive code trees, in M. Ojeda-Aciego, I. de Guzman, G. Brewka and L. Pereira (eds.), Proceedings of the 7th European Workshop on Logics in Artificial Inteligence, Springer-Verlag, 2000, pp. 209\u2013223.","DOI":"10.1007\/3-540-40006-0_15"},{"key":"394819_CR8","unstructured":"Schulz, S.: System abstract: E 0.61, in R. Gore, A. Leitsch and T. Nipkow (eds.), Proceedings of the International Joint Conference on Automated Reasoning, Springer-Verlag, 2001, pp. 370\u2013375."},{"key":"394819_CR9","doi-asserted-by":"crossref","unstructured":"Slaney, J.: FINDER: Finite Domain Enumerator, system description, in A. Bundy (ed.), Proceedings of the 12th International Conference on Automated Deduction, Springer-Verlag, 1994, pp. 798\u2013801.","DOI":"10.1007\/3-540-58156-1_63"},{"key":"394819_CR10","volume-title":"Technical Note 464","author":"M. Stickel","year":"1989","unstructured":"Stickel, M.: A Prolog technology theorem prover: A new exposition and implementation in Prolog, Technical Note 464, SRI International, Menlo Park, California, USA, 1989."},{"issue":"3","key":"394819_CR11","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1023\/A:1006393501098","volume":"24","author":"G. Sutcliffe","year":"2000","unstructured":"Sutcliffe, G.: The CADE-16 ATP system competition, J. Automated Reasoning\n24(3) (2000), 371\u2013396.","journal-title":"J. Automated Reasoning"},{"key":"394819_CR12","unstructured":"Sutcliffe, G.: Proceedings of the IJCAR ATP System Competition, Siena, Italy, 2001a."},{"issue":"3","key":"394819_CR13","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1023\/A:1017517027537","volume":"27","author":"G. Sutcliffe","year":"2001","unstructured":"Sutcliffe, G.: The CADE-17 ATP system competition, J. Automated Reasoning\n27(3) (2001b), 227\u2013250.","journal-title":"J. Automated Reasoning"},{"key":"394819_CR14","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G. and Suttner, C.: Special issue: The CADE-13 ATP system competition, J. Automated Reasoning\n18(2) (1997).","DOI":"10.1023\/A:1005858625038"},{"issue":"2","key":"394819_CR15","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.: The TPTP problem library: CNF release v1.2.1, J. Automated Reasoning\n21(2) (1998), 177\u2013203.","journal-title":"J. Automated Reasoning"},{"issue":"1","key":"394819_CR16","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.: The CADE-15 ATP system competition, J. Automated Reasoning\n23(1) (1999), 1\u201323.","journal-title":"J. Automated Reasoning"},{"key":"394819_CR17","volume-title":"Technical Report UM-CSC-2001-001","author":"G. Sutcliffe","year":"2001","unstructured":"Sutcliffe, G., Suttner, C. and Pelletier, J.: The IJCAR ATP system competition: All the details, Technical Report UM-CSC-2001-001, Department of Computer Science, University of Miami, Miami, Florida, USA, 2001."},{"issue":"1","key":"394819_CR18","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.: The CADE-14 ATP system competition, J. Automated Reasoning\n21(1) (1998), 99\u2013134.","journal-title":"J. Automated Reasoning"},{"key":"394819_CR19","doi-asserted-by":"crossref","unstructured":"Weidenbach, C., Gaede, B. and Rock, G.: SPASS and FLOTTER, in M. McRobbie and J. Slaney (eds.), Proceedings of the 13th International Conference on Automated Deduction, Springer-Verlag, 1996, pp. 141\u2013145.","DOI":"10.1007\/3-540-61511-3_75"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1015736313131.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1015736313131\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1015736313131.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:40:07Z","timestamp":1749123607000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1015736313131"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,4]]},"references-count":19,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2002,4]]}},"alternative-id":["394819"],"URL":"https:\/\/doi.org\/10.1023\/a:1015736313131","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2002,4]]}}}