{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:10:03Z","timestamp":1749125403199,"version":"3.41.0"},"reference-count":11,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2003,9,1]],"date-time":"2003-09-01T00:00:00Z","timestamp":1062374400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2003,9,1]],"date-time":"2003-09-01T00:00:00Z","timestamp":1062374400000},"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":[[2003,9]]},"DOI":"10.1023\/a:1027302123309","type":"journal-article","created":{"date-parts":[[2003,11,9]],"date-time":"2003-11-09T22:46:39Z","timestamp":1068417999000},"page":"23-32","source":"Crossref","is-referenced-by-count":2,"title":["The CADE-18 ATP System Competition"],"prefix":"10.1007","volume":"31","author":[{"given":"G.","family":"Sutcliffe","sequence":"first","affiliation":[]},{"given":"C. B.","family":"Suttner","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"5150102_CR1","doi-asserted-by":"crossref","unstructured":"Colton, S.: Automated Theory Formation in Pure Mathematics, Springer-Verlag, 2002.","DOI":"10.1007\/978-1-4471-0147-5"},{"key":"5150102_CR2","doi-asserted-by":"crossref","unstructured":"Hillenbrand, T., Jaeger, A. and L\u00f6chner, B.: Waldmeister - 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-236.","DOI":"10.1007\/3-540-48660-7_20"},{"issue":"2","key":"5150102_CR3","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1023\/A:1015067300005","volume":"28","author":"U. Hustadt","year":"2002","unstructured":"Hustadt, U. and Schmidt, R.: Using resolution for testing modal satisfiability and building models, J. Automated Reasoning\n                  28(2) (2002), 205-232.","journal-title":"J. Automated Reasoning"},{"key":"5150102_CR4","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L. and Malik, S.: Chaff: Engineering an efficient SAT solver, in B. D. and L. Lavagno (eds.), Proceedings of the 39th Design Automation Conference, 2001, pp. 530-535.","DOI":"10.1145\/378239.379017"},{"key":"5150102_CR5","unstructured":"Riazanov, A. and Voronkov, A.: The design and implementation of vampire, AI Communications (2002), to appear."},{"key":"5150102_CR6","doi-asserted-by":"crossref","unstructured":"Schumann, J.: Automated Theorem Proving in Software Engineering, Springer-Verlag, 2002.","DOI":"10.1007\/978-3-662-22646-9"},{"key":"5150102_CR7","unstructured":"Stenz, G. and Wolf, A.: Strategy selection by genetic programming, in A. Kumar and I. Russell (eds.), Proceedings of the 12th Florida Artificial Intelligence Research Symposium, AAAI Press, 1999, pp. 346-350."},{"key":"5150102_CR8","unstructured":"Sutcliffe, G.: Proceedings of the CADE-18 ATP System Competition, Copenhagen, Denmark, 2002."},{"issue":"2","key":"5150102_CR9","doi-asserted-by":"publisher","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\n                  21(2) (1998), 177-203.","journal-title":"J. Automated Reasoning"},{"issue":"3","key":"5150102_CR10","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1023\/A:1015736313131","volume":"28","author":"G. Sutcliffe","year":"2002","unstructured":"Sutcliffe, G., Suttner, C. and Pelletier, F.: The IJCAR ATP system competition, J. Automated Reasoning\n                  28(3) (2002), 307-320.","journal-title":"J. Automated Reasoning"},{"key":"5150102_CR11","doi-asserted-by":"crossref","unstructured":"Tammet, T.: Towards efficient ATP progress, in C. Kirchner and H. Kirchner (eds.), Proceedings of the 15th International Conference on Automated Deduction, Springer-Verlag, 1998, pp. 427-440.","DOI":"10.1007\/BFb0054276"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1027302123309.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1027302123309\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1027302123309.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:39:01Z","timestamp":1749123541000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1027302123309"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,9]]},"references-count":11,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2003,9]]}},"alternative-id":["5150102"],"URL":"https:\/\/doi.org\/10.1023\/a:1027302123309","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2003,9]]}}}