{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:47:30Z","timestamp":1749124050159},"reference-count":11,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1993,1,1]],"date-time":"1993-01-01T00:00:00Z","timestamp":725846400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/bf00881871","type":"journal-article","created":{"date-parts":[[2004,12,27]],"date-time":"2004-12-27T18:44:45Z","timestamp":1104173085000},"page":"317-331","source":"Crossref","is-referenced-by-count":2,"title":["Uniform strategies: The CADE-11 theorem proving contest"],"prefix":"10.1007","volume":"11","author":[{"given":"Ewing L.","family":"Lusk","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"William W.","family":"McCune","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","first-page":"139","volume-title":"Parallelization in Inference Systems, Lecture Notes in Artificial Intelligence, Vol. 590","author":"E. Lusk","year":"1992","unstructured":"Lusk, E., and McCune, W., ?Experiments withRoo, a parallel automated deduction system?, in B. Fronh\u00f6fer and G. Wrightson (Eds.),Parallelization in Inference Systems, Lecture Notes in Artificial Intelligence, Vol. 590, pp. 139?162, New York, Springer-Verlag (1992)."},{"key":"CR2","series-title":"Tech. Memo","volume-title":"Roo ? a parallel theorem prover","author":"E. Lusk","year":"1991","unstructured":"Lusk, E., McCune, W. and Slaney, J., ?Roo ? a parallel theorem prover?,Tech. Memo ANL\/MCS-TM-149, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, Ill. (1991)."},{"key":"CR3","series-title":"Tech. Report","volume-title":"The automated reasoning system ITP","author":"E. Lusk","year":"1984","unstructured":"Lusk, E. and Overbeek, R., ?The automated reasoning system ITP?,Tech. Report ANL-84\/27, Argonne National Laboratory, Argonne, Ill. (April 1984)."},{"key":"CR4","first-page":"1","volume":"2","author":"J. McCharen","year":"1976","unstructured":"McCharen, J., Overbeek, R. and Wos, L., ?Complexity and related enhancements for automated theorem-proving programs?,Computers and Mathematics with Applications,2 1?16 (1976).","journal-title":"Computers and Mathematics with Applications"},{"issue":"8","key":"CR5","doi-asserted-by":"crossref","first-page":"773","DOI":"10.1109\/TC.1976.1674696","volume":"C-25","author":"J. McCharen","year":"1976","unstructured":"McCharen, J., Overbeek, R. and Wos, L., ?Problems and experiments for and with automated theorem-proving programs?,IEEE Transactions on Computers,C-25(8), 773?782 (August 1976).","journal-title":"IEEE Transactions on Computers"},{"key":"CR6","series-title":"Tech. Report","volume-title":"Otter 2.0 Users' Guide","author":"W. McCune","year":"1990","unstructured":"McCune, W.,Otter 2.0 Users' Guide. Tech. Report ANL-90\/9, Argonne National Laboratory, Argonne, Ill. (March 1990)."},{"key":"CR7","series-title":"Tech. Memo","volume-title":"What's New inOtter 2.2","author":"W. McCune","year":"1991","unstructured":"McCune, W., ?What's New inOtter 2.2?,Tech. Memo ANL\/MCS-TM-153, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, Ill. (July 1991)."},{"key":"CR8","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1016\/0304-3975(91)90034-Y","volume":"87","author":"W. McCune","year":"1991","unstructured":"McCune, W. and Wos, L., ?The absence and the presence of fixed point combinators?,Theoretical Computer Science,87 221?228 (1991).","journal-title":"Theoretical Computer Science"},{"key":"CR9","first-page":"209","volume-title":"Proceedings 11th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, Vol. 607","author":"W. McCune","year":"1992","unstructured":"McCune, W. and Wos, L., ?Experiments in automated deduction with condensed detachment?, D. Kapur (Ed.),Proceedings 11th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, Vol. 607, pp. 209?223. New York, Springer Verlag (June 1992)."},{"key":"CR10","series-title":"Tech. Report","volume-title":"Reference manual for the environmental theorem prover: An incarnation ofAura","author":"B. Smith","year":"1988","unstructured":"Smith, B., ?Reference manual for the environmental theorem prover: An incarnation ofAura?,Tech. Report ANL-88-2, Argonne National Laboratory, Argonne, Ill. (March 1988)."},{"key":"CR11","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/BF00881872","volume":"11","author":"Hantao Zhang","year":"1993","unstructured":"Hantao Zhang, ?Automatic proofs of equality problems in Overbeek's competition?,Journal of Automated Reasoning,11 333?351 (1993).","journal-title":"Journal of Automated Reasoning"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881871.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00881871\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881871","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,29]],"date-time":"2019-04-29T08:58:11Z","timestamp":1556528291000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00881871"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"references-count":11,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1993]]}},"alternative-id":["BF00881871"],"URL":"https:\/\/doi.org\/10.1007\/bf00881871","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993]]}}}