{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:06:24Z","timestamp":1749125184193},"publisher-location":"Berlin, Heidelberg","reference-count":7,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540556022"},{"type":"electronic","value":"9783540472520"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1992]]},"DOI":"10.1007\/3-540-55602-8_224","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T10:22:31Z","timestamp":1330251751000},"page":"781-785","source":"Crossref","is-referenced-by-count":4,"title":["Benchmark problems in which equality plays the major role"],"prefix":"10.1007","author":[{"given":"E.","family":"Lusk","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"L.","family":"Wos","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"74_CR1","volume-title":"The Lambda Calculus: Its Syntax and Semantics","author":"H. P. Barendregt","year":"1981","unstructured":"Barendregt, H. P. The Lambda Calculus: Its Syntax and Semantics, North-Holland, Amsterdam (1981)."},{"key":"74_CR2","first-page":"274","volume":"35","author":"E. Huntington","year":"1933","unstructured":"Huntington, E., \u201cNew sets of independent postulates for the algebra of logic, with special reference to Whitehead and Russell's Principia Mathematica\u201d, Trans. of AMS, 35, pp. 274\u2013304 (1933).","journal-title":"Trans. of AMS"},{"key":"74_CR3","volume-title":"Technical Report ANL-90\/9","author":"W. McCune","year":"1990","unstructured":"McCune, W., OTTER 2.0 Users Guide, Technical Report ANL-90\/9, Argonne National Laboratory, Argonne, Illinois, 1990."},{"key":"74_CR4","unstructured":"McCune, W., What's New in OTTER 2.2, Mathematics and Computer Science Division Technical Report ANL\/MCS-TM-153, Argonne National Laboratory, 1991."},{"key":"74_CR5","volume-title":"Mathematics and Computer Science Division Preprint MCS-P270-1091","author":"W. McCune","year":"1991","unstructured":"McCune, W., Single Axioms for Groups and Abelian Groups with Various Operations, Mathematics and Computer Science Division Preprint MCS-P270-1091, Argonne National Laboratory, Argonne, Illinois, 1991."},{"key":"74_CR6","doi-asserted-by":"crossref","first-page":"212","DOI":"10.1305\/ndjfl\/1093893457","volume":"9","author":"C. A. Meredith","year":"1968","unstructured":"Meredith, C. A., and Prior, A. N., \u201cEquational logic\u201d, Notre Dame J. Formal Logic, 9, pp. 212\u2013226 (1968).","journal-title":"Notre Dame J. Formal Logic"},{"key":"74_CR7","volume-title":"Automated Reasoning: 33 Basic Research Problems","author":"L. Wos","year":"1987","unstructured":"Wos, L., Automated Reasoning: 33 Basic Research Problems, Prentice-Hall, Englewood Cliffs, N.J., 1987."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-11"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-55602-8_224.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:33:06Z","timestamp":1619573586000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-55602-8_224"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992]]},"ISBN":["9783540556022","9783540472520"],"references-count":7,"URL":"https:\/\/doi.org\/10.1007\/3-540-55602-8_224","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1992]]}}}