{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T11:00:24Z","timestamp":1775818824820,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540581567","type":"print"},{"value":"9783540484677","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58156-1_18","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T15:22:05Z","timestamp":1330269725000},"page":"252-266","source":"Crossref","is-referenced-by-count":73,"title":["The TPTP problem library"],"prefix":"10.1007","author":[{"given":"Geoff","family":"Sutcliffe","sequence":"first","affiliation":[]},{"given":"Christian","family":"Suttner","sequence":"additional","affiliation":[]},{"given":"Theodor","family":"Yemenis","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,30]]},"reference":[{"key":"18_CR1","unstructured":"ANL Problem Library. Available by anonymous ftp from info.msc.anl.gov, Maths and Computer Science Division, Argonne National Laboratory, Argonne, IL."},{"key":"18_CR2","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1007\/BF00244493","volume":"6","author":"W. W. Bledsoe","year":"1990","unstructured":"W.W. Bledsoe. Challenge Problems in Elementary Calculus. Journal of Automated Reasoning, 6:341\u2013359, 1990.","journal-title":"Journal of Automated Reasoning"},{"key":"18_CR3","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/BF02328452","volume":"2","author":"R. Boyer","year":"1986","unstructured":"[BLM+86] R. Boyer, E. Lusk, W. McCune, R. Overbeek, M. Stickel, and L. Wos. Set Theory in First-Order Logic: Clauses for G\u00f6del's Axioms. Journal of Automated Reasoning, 2:287\u2013327, 1986.","journal-title":"Journal of Automated Reasoning"},{"key":"18_CR4","unstructured":"M. Dewey. Dewey Decimal Classification and Relative Index. Forest Press, 20 edition, 1989."},{"key":"18_CR5","unstructured":"M. Fujita, R. Hasegawa, M. Koshimura, and H. Fujita. Model Generation Theorem Provers on a Parallel Inference Machine. In Proceedings of the International Conference on Fifth Generation Computer Systems, pages 357\u2013375, 1992."},{"key":"18_CR6","unstructured":"W.W. McCune. Otter 2.0 Users Guide. Technical Report ANL-90\/9, Argonne National Laboratory, 1990."},{"issue":"1","key":"18_CR7","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF00881862","volume":"10","author":"W. W. McCune","year":"1993","unstructured":"W.W. McCune. Single Axioms for Groups and Abelian Groups with Various Operations. Journal of Automated Reasoning, 10(1):1\u201313, 1993.","journal-title":"Journal of Automated Reasoning"},{"issue":"8","key":"18_CR8","doi-asserted-by":"crossref","first-page":"773","DOI":"10.1109\/TC.1976.1674696","volume":"C-25","author":"J. McCharen","year":"1976","unstructured":"J. McCharen, A. Overbeek, and L. Wos. Problems and Experiments for and with Automated Theorem-Proving Programs. IEEE Transactions on Computers, C-25(8):773\u2013782, August 1976.","journal-title":"IEEE Transactions on Computers"},{"key":"18_CR9","unstructured":"Mathematical Subject Classification. American Mathematical Society, Provedence, RI, 1992. Mathematical Reviews, Subject Index."},{"key":"18_CR10","doi-asserted-by":"crossref","unstructured":"W. McCune and L. Wos. Experiments in Automated Deduction with Condensed Detachment. In Proceedings of CADE-11, pages 209\u2013223, Saratoga Springs, USA, 1992. Springer LNAI 607.","DOI":"10.1007\/3-540-55602-8_167"},{"key":"18_CR11","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/BF02432151","volume":"2","author":"F. J. Pelletier","year":"1986","unstructured":"F.J. Pelletier. Seventy-five Problems for Testing Automated Theorem Provers. Journal of Automated Reasoning, 2:191\u2013216, 1986.","journal-title":"Journal of Automated Reasoning"},{"issue":"3","key":"18_CR12","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/BF00244944","volume":"4","author":"D. A. Plaisted","year":"1988","unstructured":"D.A. Plaisted. Non-Horn Clause Logic Programming without Contrapositives. Journal of Automated Reasoning, 4(3):287\u2013325, 1988.","journal-title":"Journal of Automated Reasoning"},{"issue":"1","key":"18_CR13","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1007\/BF00263451","volume":"8","author":"A. Quaife","year":"1992","unstructured":"A. Quaife. Automated Deduction in von Neumann-Bernays-Godel Set Theory. Journal of Automated Reasoning, 8(1):91\u2013147, 1992.","journal-title":"Journal of Automated Reasoning"},{"key":"18_CR14","unstructured":"A. Quaife. Problems based on NBG Set Theory. Emailed from A. Quaife to G. Sutcliffe, 1992."},{"issue":"3","key":"18_CR15","first-page":"287","volume":"4","author":"SPRFN","year":"1988","unstructured":"SPRFN. The problem collection distributed with the SPRFN ATP system [Pla88].","journal-title":"Journal of Automated Reasoning"},{"key":"18_CR16","series-title":"Technical Report 93\/11","volume-title":"Technical Report FKI-184-93","author":"C. B. Suttner","year":"1993","unstructured":"C.B. Suttner, G. Sutcliffe, and T. Yemenis. The TPTP Problem Library (TPTP vl.0.0). Technical Report FKI-184-93, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, Munich, Germany; Technical Report 93\/11, Department of Computer Science, James Cook University, Townsville, Australia, 1993."},{"issue":"4","key":"18_CR17","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1007\/BF03037328","volume":"2","author":"M. E. Stickel","year":"1984","unstructured":"M.E. Stickel. A Prolog Technology Theorem Prover. New Generation Computing, 2(4):371\u2013383, 1984.","journal-title":"New Generation Computing"},{"key":"18_CR18","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1007\/BF00246025","volume":"2","author":"M. E. Stickel","year":"1986","unstructured":"M.E. Stickel. Schubert's Steamroller Problem: Formulations and Solutions. Journal of Automated Reasoning, 2:89\u2013101, 1986.","journal-title":"Journal of Automated Reasoning"},{"key":"18_CR19","doi-asserted-by":"crossref","unstructured":"M.E. Stickel. Upside-Down Meta-Interpretation of the Model Elimination Theorem-Proving Procedure for Deduction and Abduction. Journal of Automated Reasoning, to appear, 1994.","DOI":"10.1007\/BF00881955"},{"key":"18_CR20","unstructured":"J. Schumann, N. Trapp, and M. van der Koelen. SETHEO\/PARTHEO Users Manual. Technical Report SFB Bericht 342\/7\/90 A, Institut f\u00fcr Informatik, TU M\u00fcnchen, 1990."},{"issue":"8","key":"18_CR21","doi-asserted-by":"crossref","first-page":"782","DOI":"10.1109\/TC.1976.1674697","volume":"C-25","author":"G. A. Wilson","year":"1976","unstructured":"G.A. Wilson and J. Minker. Resolution, Refinements, and Search Strategies: A Comparative Study. IEEE Transactions on Computers, C-25(8):782\u2013801, 1976.","journal-title":"IEEE Transactions on Computers"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-12"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58156-1_18.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:11:50Z","timestamp":1619572310000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58156-1_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540581567","9783540484677"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-58156-1_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994]]}}}