{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,6]],"date-time":"2025-06-06T04:06:55Z","timestamp":1749182815293,"version":"3.41.0"},"reference-count":23,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[1999,7,1]],"date-time":"1999-07-01T00:00:00Z","timestamp":930787200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1999,7,1]],"date-time":"1999-07-01T00:00:00Z","timestamp":930787200000},"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":[[1999,7]]},"DOI":"10.1023\/a:1006285423991","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T01:20:41Z","timestamp":1040520041000},"page":"1-23","source":"Crossref","is-referenced-by-count":11,"title":["The CADE-15 ATP System Competition"],"prefix":"10.1007","volume":"23","author":[{"given":"G.","family":"Sutcliffe","sequence":"first","affiliation":[]},{"given":"C. B.","family":"Suttner","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"207708_CR1","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Dershowitz, N. and Plaisted, D. A.: 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":"207708_CR2","series-title":"Technical Report SEKI-Report","volume-title":"Waldmeister: Development of a high performance completion based theorem prover","author":"A. Buch","year":"1996","unstructured":"Buch, A. and Hillenbrand, T.: Waldmeister: Development of a high performance completion based theorem prover, Technical Report SEKI-Report SR-96-01, AG Effiziente Algorithmen, Universit\u00e4t Kaiserslautern, Kaiserslautern, Germany, 1996."},{"key":"207708_CR3","doi-asserted-by":"crossref","unstructured":"Ferm\u00fcller, C., Leitsch, A., Tammet, T. and Zamov, N.: Resolution Methods for the Decision Problem, Lecture Notes in Comput. Sci. 679, Springer-Verlag, 1993.","DOI":"10.1007\/3-540-56732-1"},{"key":"207708_CR4","doi-asserted-by":"crossref","unstructured":"Ganzinger, H., Meyer, C. and Weidenbach, C.: Soft typing for ordered resolution, in W. W. McCune (ed.), Proceedings of the 14th International Conference on Automated Deduction, Lecture Notes in Artif. Intell. 1249, Springer-Verlag, 1997, pp. 321\u2013335.","DOI":"10.1007\/3-540-63104-6_32"},{"key":"207708_CR5","series-title":"Technical Report","volume-title":"A probablistic stopping criterion for the evaluation of benchmarks","author":"M. Greiner","year":"1996","unstructured":"Greiner, M. and Schramm, M.: A probablistic stopping criterion for the evaluation of benchmarks, Technical Report I9638, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, M\u00fcnchen, Germany, 1996."},{"issue":"2","key":"207708_CR6","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1023\/A:1005872405899","volume":"18","author":"T. Hillenbrand","year":"1997","unstructured":"Hillenbrand, T., Buch, A., Vogt, R. and L\u00f6chner, B.: Waldmeister: High performance equational deduction, J. Automated Reasoning\n18(2) (1997), 265\u2013270.","journal-title":"J. Automated Reasoning"},{"key":"207708_CR7","doi-asserted-by":"crossref","unstructured":"Kaufmann, M.: ACL2 Support for Verification Projects, in C. Kirchner and H. Kirchner (eds.), Proceedings of the 15th International Conference on Automated Deduction, Lecture Notes in Artif. Intell. 142, Springer-Verlag, 1998, pp. 220\u2013238.","DOI":"10.1007\/BFb0054262"},{"key":"207708_CR8","doi-asserted-by":"crossref","unstructured":"Nonnengart, A., Rock, G. and Weidenbach, C.: On generating small clause normal forms, in C. Kirchner and H. Kirchner (eds.), Proceedings of the 15th International Conference on Automated Deduction, Lecture Notes in Artif. Intell. 1421, Springer-Verlag, 1998, pp. 397\u2013411.","DOI":"10.1007\/BFb0054274"},{"key":"207708_CR9","doi-asserted-by":"crossref","unstructured":"Slaney, J. K., Lusk, E. and McCune, W. W.: SCOTT: Semantically constrained Otter, system description, in A. Bundy (ed.), Proceedings of the 12th International Conference on Automated Deduction, Lecture Notes in Artif. Intell. 814, Springer-Verlag, 1994, pp. 764\u2013768.","DOI":"10.1007\/3-540-58156-1_56"},{"key":"207708_CR10","doi-asserted-by":"crossref","unstructured":"Suttner, C. B. and Schumann, J.: Parallel automated theorem proving, in L. Kanal, V. Kumar, H. Kitano, and C. Suttner (eds.), Parallel Processing for Artificial Intelligence 1, Elsevier Science, 1994, pp. 209\u2013257.","DOI":"10.1016\/B978-0-444-81704-4.50015-6"},{"key":"207708_CR11","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G. and Suttner, C. B.: Special issue: The CADE-13 ATP system competition, J. Automated Reasoning\n18(2) (1997).","DOI":"10.1023\/A:1005839515219"},{"issue":"2","key":"207708_CR12","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. B.: The procedures of the CADE-13 ATP system competition, J. Automated Reasoning\n18(2) (1997), 163\u2013169.","journal-title":"J. Automated Reasoning"},{"issue":"2","key":"207708_CR13","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1023\/A:1005802523220","volume":"18","author":"C. B. Suttner","year":"1997","unstructured":"Suttner, C. B. and Sutcliffe, G.: The design of the CADE-13 ATP system competition, J. Automated Reasoning\n18(2) (1997), 139\u2013162.","journal-title":"J. Automated Reasoning"},{"key":"207708_CR14","series-title":"Technical Report","volume-title":"The CADE-14 ATP system competition","author":"G. Sutcliffe","year":"1998","unstructured":"Sutcliffe, G. and Suttner, C.: The CADE-14 ATP system competition, Technical Report 98\/01, Department of Computer Science, James Cook University, Townsville, Australia, 1998."},{"key":"207708_CR15","unstructured":"Sutcliffe, G. and Suttner, C. B.: Proceedings of the CADE-15 ATP System Competition, Lindau, Germany, 1998."},{"issue":"2","key":"207708_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. B.: 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":"207708_CR17","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1023\/A:1006006930186","volume":"21","author":"C. B. Suttner","year":"1998","unstructured":"Suttner, C. B. and Sutcliffe, G.: The CADE-14 ATP system competition, J. Automated Reasoning\n21(1) (1998), 99\u2013134.","journal-title":"J. Automated Reasoning"},{"key":"207708_CR18","doi-asserted-by":"crossref","unstructured":"Tammet, T.: A resolution theorem prover for intuitionistic logic, in M. McRobbie and J. K. Slaney (eds.), Proceedings of the 13th International Conference on Automated Deduction, Lecture Notes in Artif. Intell. 1104, Springer-Verlag, 1996, pp. 2\u201316.","DOI":"10.1007\/3-540-61511-3_65"},{"issue":"2","key":"207708_CR19","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1023\/A:1005887414560","volume":"18","author":"T. Tammet","year":"1997","unstructured":"Tammet, T.: Gandalf, J. Automated Reasoning\n18(2) (1997), 199\u2013204.","journal-title":"J. Automated Reasoning"},{"key":"207708_CR20","doi-asserted-by":"crossref","unstructured":"Tammet, T.: Towards efficient subsumption, in C. Kirchner and H. Kirchner (eds.), Proceedings of the 15th International Conference on Automated Deduction, Lecture Notes in Artif. Intell. 1421, Springer-Verlag, 1998, pp. 427\u2013440.","DOI":"10.1007\/BFb0054276"},{"key":"207708_CR21","doi-asserted-by":"crossref","unstructured":"Tammet, T. and Smith, J.: Optimised encodings of fragments of type theory in first order logic, in S. Berardi and M. Coppo (eds.), Types for Proofs and Programs: Proceedings of the International Workshop TYPES'95, Lecture Notes in Artif. Intell. 1158, Springer-Verlag, 1996, pp. 265\u2013287.","DOI":"10.1007\/3-540-61780-9_75"},{"key":"207708_CR22","unstructured":"Weidenbach, C.: Email to G. Sutcliffe, 1997."},{"issue":"2","key":"207708_CR23","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1023\/A:1005812220011","volume":"18","author":"C. Weidenbach","year":"1997","unstructured":"Weidenbach, C.: SPASS: Version 0.49, J. Automated Reasoning\n18(2) (1997), 247\u2013252.","journal-title":"J. Automated Reasoning"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1006285423991.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1006285423991\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1006285423991.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:43:47Z","timestamp":1749123827000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1006285423991"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999,7]]},"references-count":23,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1999,7]]}},"alternative-id":["207708"],"URL":"https:\/\/doi.org\/10.1023\/a:1006285423991","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[1999,7]]}}}