{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T13:24:07Z","timestamp":1770297847637,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":9,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540662228","type":"print"},{"value":"9783540486602","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48660-7_26","type":"book-chapter","created":{"date-parts":[[2007,11,9]],"date-time":"2007-11-09T15:53:07Z","timestamp":1194623587000},"page":"292-296","source":"Crossref","is-referenced-by-count":29,"title":["Vampire"],"prefix":"10.1007","author":[{"given":"Alexandre","family":"Riazanov","sequence":"first","affiliation":[]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,5,17]]},"reference":[{"issue":"1\/2","key":"26_CR1","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1023\/A:1005992522805","volume":"20","author":"H. Nivelle de","year":"1998","unstructured":"H. de Nivelle. An algorithm for the retrieval of unifiers from discrimination trees. Journal of Automated Reasoning, 20(1\/2):5\u201325, January 1998.","journal-title":"Journal of Automated Reasoning"},{"key":"26_CR2","series-title":"Lect Notes Comput Sci","volume-title":"Term Indexing","author":"P. Graf","year":"1996","unstructured":"P. Graf. Term Indexing, volume 1053of Lecture Notes in Computer Science. Springer Verlag, 1996."},{"key":"26_CR3","doi-asserted-by":"crossref","unstructured":"E.L. Lusk. Controlling redundancy in large search spaces: Argonne-style theorem proving through the years. In A. Voronkov, editor, Logic Programming and Automated Reasoning. International Conference LPAR\u201992., volume 624 of Lecture Notes in Artificial Intelligence, pages 96\u2013106, St.Petersburg, Russia, July 1992.","DOI":"10.1007\/BFb0013052"},{"issue":"2","key":"26_CR4","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BF00245458","volume":"9","author":"W. W. McCune","year":"1992","unstructured":"William W. McCune. Experiments with discrimination-tree indexing and path indexing for term retrieval. Journal of Automated Reasoning, 9(2):147\u2013167, 1992.","journal-title":"Journal of Automated Reasoning"},{"key":"26_CR5","doi-asserted-by":"crossref","unstructured":"W.W. McCune. OTTER 3.0 reference manual and guide. Technical Report ANL-94\/6, Argonne National Laboratory, January 1994.","DOI":"10.2172\/10129052"},{"key":"26_CR6","unstructured":"I.V. Ramakrishnan, R. Sekar, and A. Voronkov. Term indexing. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning. Elsevier Science and MIT Press, 1999. To appear."},{"key":"26_CR7","series-title":"Technical Report","doi-asserted-by":"crossref","DOI":"10.21236\/ADA460990","volume-title":"The path indexing method for indexing terms","author":"M. Stickel","year":"1989","unstructured":"M. Stickel. The path indexing method for indexing terms. Technical Report 473, Artificial Intelligence Center, SRI International, Menlo Park, CA, October 1989."},{"issue":"2","key":"26_CR8","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/BF00881918","volume":"15","author":"A. Voronkov","year":"1995","unstructured":"A. Voronkov. The anatomy of Vampire: Implementing bottom-up procedures with code trees. Journal of Automated Reasoning, 15(2):237\u2013265, 1995.","journal-title":"Journal of Automated Reasoning"},{"key":"26_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1007\/3-540-61511-3_75","volume-title":"Automated Deduction CADE-13","author":"C. Weidenbach","year":"1996","unstructured":"C. Weidenbach, B. Gaede, and G. Rock. Spass & flotter. version 0.42. In M.A. McRobbie and J.K. Slaney, editors, Automated Deduction CADE-13, volume 1104 of Lecture Notes in Computer Science, pages 141\u2013145, New Brunswick, NJ, USA, 1996."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-16"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48660-7_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,4]],"date-time":"2019-05-04T04:56:41Z","timestamp":1556945801000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48660-7_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540662228","9783540486602"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/3-540-48660-7_26","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[1999]]}}}