{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T21:29:47Z","timestamp":1773869387632,"version":"3.50.1"},"publisher-location":"Cham","reference-count":56,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031634970","type":"print"},{"value":"9783031634987","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,1]],"date-time":"2024-07-01T00:00:00Z","timestamp":1719792000000},"content-version":"vor","delay-in-days":182,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>The TPTP World is a well established infrastructure that supports research, development, and deployment of Automated Theorem Proving (ATP) systems. There are key components that help make the TPTP World a success: the TPTP problem library was first released in 1993, the CADE ATP System Competition (CASC) was conceived after CADE-12 in 1994, problem difficulty ratings were added in 1997, the current TPTP language was adopted in 2003, the SZS ontologies were specified in 2004, the TSTP solution library was built starting around 2005, the Specialist Problem Classes (SPCs) have been used to classify problems since 2010, the SystemOnTPTP service has been offered from 2011, the StarExec service was started in 2013, and a world of TPTP users have helped all along. This paper reviews these stepping stones in the development of the TPTP World.<\/jats:p>","DOI":"10.1007\/978-3-031-63498-7_3","type":"book-chapter","created":{"date-parts":[[2024,6,30]],"date-time":"2024-06-30T19:01:44Z","timestamp":1719774104000},"page":"30-50","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Stepping Stones in\u00a0the\u00a0TPTP World"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9120-3927","authenticated-orcid":false,"given":"Geoff","family":"Sutcliffe","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,1]]},"reference":[{"key":"3_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-17502-3_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Bartocci","year":"2019","unstructured":"Bartocci, E., et al.: TOOLympics 2019: an overview of competitions in formal methods. In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) TACAS 2019. LNCS, vol. 11429, pp. 3\u201324. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_1"},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"414","DOI":"10.1007\/978-3-642-38574-2_29","volume-title":"Automated Deduction \u2013 CADE-24","author":"JC Blanchette","year":"2013","unstructured":"Blanchette, J.C., Paskevich, A.: TFF1: the TPTP typed first-order form with rank-1 polymorphism. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 414\u2013420. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_29"},{"key":"3_CR3","unstructured":"Blanchette, J., Urban, J. (eds.): Proceedings of the 3rd International International Workshop on Proof Exchange for Theorem Proving. No.\u00a014 in EPiC Series in Computing, EasyChair Publications (2013)"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"Boyer, R., Lusk, E., McCune, W., Overbeek, R., Stickel, M., Wos, L.: Set theory in first-order logic: clauses for Godel\u2019s axioms. J. Autom. Reason. 2(3), 287\u2013327 (1986)","DOI":"10.1007\/BF02328452"},{"issue":"1","key":"3_CR5","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/s10817-015-9328-2","volume":"55","author":"D Cok","year":"2015","unstructured":"Cok, D., Stump, A., Weber, T.: The 2013 evaluation of SMT-COMP and SMT-LIB. J. Autom. Reason. 55(1), 61\u201390 (2015)","journal-title":"J. Autom. Reason."},{"key":"3_CR6","unstructured":"Fuchs, M., Sutcliffe, G.: Homogeneous sets of ATP Problems. In: Haller, S., Simmons, G. (eds.) Proceedings of the 15th International FLAIRS Conference, pp. 57\u201361. AAAI Press (2002)"},{"key":"3_CR7","unstructured":"Fuenmayor, D., McKeown, J., Sutcliffe, G.: Towards StarExec in the cloud. In: Rawson, M., Schulz, S., Korovin, K. (eds.) Proceedings of the 15th International Workshop on the Implementation of Logics. p. To appear (2024)"},{"issue":"4","key":"3_CR8","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1007\/BF00248251","volume":"2","author":"B Glickfield","year":"1986","unstructured":"Glickfield, B., Overbeek, R.: A foray into combinatory logic. J. Autom. Reason. 2(4), 419\u2013431 (1986)","journal-title":"J. Autom. Reason."},{"key":"3_CR9","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-642-22438-6_23","volume-title":"Automated Deduction \u2013 CADE-23","author":"K Hoder","year":"2011","unstructured":"Hoder, K., Voronkov, A.: Sine Qua non for large theory reasoning. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 299\u2013314. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22438-6_23"},{"key":"3_CR10","unstructured":"Hoos, H., St\u00fctzle, T.: SATLIB: an online resource for research on SAT. In: Gent, I., van Maaren, H., Walsh, T. (eds.) Proceedings of the 3rd Workshop on the Satisfiability Problem, pp. 283\u2013292. IOS Press (2000)"},{"issue":"3","key":"3_CR11","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/BF00881715","volume":"14","author":"T Jech","year":"1995","unstructured":"Jech, T.: Otter experiments in a system of combinatory logic. J. Autom. Reason. 14(3), 413\u2013426 (1995)","journal-title":"J. Autom. Reason."},{"key":"3_CR12","unstructured":"Kaliszyk, C., Sutcliffe, G., Rabe, F.: TH1: the TPTP typed higher-order form with Rank-1 polymorphism. In: Fontaine, P., Schulz, S., Urban, J. (eds.) Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning, pp. 41\u201355. No.\u00a01635 in CEUR Workshop Proceedings (2016)"},{"key":"3_CR13","unstructured":"Laboratory, A.N.: The Argonne National Laboratory Problem Collection. http:\/\/info.mcs.anl.gov\/"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"McCharen, J., Overbeek, R., Wos, L.: Problems and experiments for and with automated theorem-proving programs. IEEE Trans. Comput. C-25(8), 773\u2013782 (1976)","DOI":"10.1109\/TC.1976.1674696"},{"key":"3_CR15","unstructured":"McCune, W.: Otter 3.3 Reference Manual. Technical report. ANL\/MSC-TM-263, Argonne National Laboratory, Argonne, USA (2003)"},{"key":"3_CR16","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61398-6","volume-title":"Automated Deduction in Equational Logic and Cubic Curves","author":"W McCune","year":"1996","unstructured":"McCune, W., Padmanabhan, R.: Automated Deduction in Equational Logic and Cubic Curves. LNAI, vol. 1095. Springer-Verlag, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61398-6"},{"key":"3_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/3-540-55602-8_167","volume-title":"Automated Deduction\u2014CADE-11","author":"W McCune","year":"1992","unstructured":"McCune, W., Wos, L.: Experiments in automated deduction with condensed detachment. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 209\u2013223. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-55602-8_167"},{"issue":"2\u20133","key":"3_CR18","first-page":"77","volume":"15","author":"R Nieuwenhuis","year":"2002","unstructured":"Nieuwenhuis, R.: The impact of CASC in the development of automated deduction systems. AI Commun. 15(2\u20133), 77\u201378 (2002)","journal-title":"AI Commun."},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"Paulson, L., Blanchette, J.: Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers. In: Sutcliffe, G., Ternovska, E., Schulz, S. (eds.) Proceedings of the 8th International Workshop on the Implementation of Logics, pp. 1\u201311. No.\u00a02 in EPiC Series in Computing, EasyChair Publications (2010)","DOI":"10.29007\/36dt"},{"key":"3_CR20","unstructured":"Peli, G., Bruggeman, J., Masuch, M., O\u00a0Nuallain, B.: A Logical Approach to Formalizing Organizational Ecology: Formalizing the Inertia-Fragment in First-Order Logic. Technical report. CCSOM Preprint 92-74, Department of Statistics and Methodology, University of Amsterdam (1992)"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"Peli, G., Masuch, M.: The logic of propogation strategies: axiomatizing a fragment of organization ecology in first-order logic. In: Moore, D. (ed.) Academy Of Management: Best Papers Proceedings 1994, pp. 218\u2013222 (1994)","DOI":"10.5465\/ambpp.1994.10343802"},{"issue":"2","key":"3_CR22","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/BF02432151","volume":"2","author":"F Pelletier","year":"1986","unstructured":"Pelletier, F.: Seventy-five problems for testing automatic theorem provers. J. Autom. Reason. 2(2), 191\u2013216 (1986)","journal-title":"J. Autom. Reason."},{"key":"3_CR23","unstructured":"Peter, L., Hull, R.: The Peter Principle. Souvenir Press, Chicago (1969)"},{"key":"3_CR24","unstructured":"Puzis, Y., Gao, Y., Sutcliffe, G.: Automated generation of interesting theorems. In: Sutcliffe, G., Goebel, R. (eds.) Proceedings of the 19th International FLAIRS Conference, pp. 49\u201354. AAAI Press (2006)"},{"issue":"1","key":"3_CR25","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/BF00263451","volume":"8","author":"A Quaife","year":"1992","unstructured":"Quaife, A.: Automated deduction in von Neumann-Bernays-Godel set theory. J. Autom. Reason. 8(1), 91\u2013147 (1992)","journal-title":"J. Autom. Reason."},{"key":"3_CR26","unstructured":"Quaife, A.: Automated Development of Fundamental Mathematical Theories. Kluwer Academic Publishers (1992)"},{"key":"3_CR27","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/978-3-030-29436-6_29","volume-title":"Automated Deduction \u2013 CADE 27","author":"S Schulz","year":"2019","unstructured":"Schulz, S., Cruanes, S., Vukmirovi\u0107, P.: Faster, higher, stronger: E 2.3. In: Fontaine, P. (ed.) CADE 2019. LNCS (LNAI), vol. 11716, pp. 495\u2013507. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_29"},{"issue":"1\u20132","key":"3_CR28","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0004-3702(94)90077-9","volume":"69","author":"A Segre","year":"1994","unstructured":"Segre, A., Elkan, C.: A high-performance explanation-based learning algorithm. Artif. Intell. 69(1\u20132), 1\u201350 (1994)","journal-title":"Artif. Intell."},{"key":"3_CR29","unstructured":"SPRFN: The Problem Collection Distributed with the SPRFN ATP System. https:\/\/www.cs.unc.edu\/Research\/mi\/mi-provers.html"},{"key":"3_CR30","unstructured":"Steen, A., Fuenmayor, D., Glei\u00dfner, T., Sutcliffe, G., Benzm\u00fcller, C.: Automated reasoning in non-classical logics in the TPTP world. In: Konev, B., Schon, C., Steen, A. (eds.) Proceedings of the 8th Workshop on Practical Aspects of Automated Reasoning. p. Online. No.\u00a03201 in CEUR Workshop Proceedings (2022)"},{"key":"3_CR31","unstructured":"Steen, A., Sutcliffe, G.: TPTP world infrastructure for non-classical logics. In: Nalon, C., Steen, A., Suda, M. (eds.) Proceedings of the 9th Workshop on Practical Aspects of Automated Reasoning, p. Online. CEUR Workshop Proceedings (2024)"},{"key":"3_CR32","doi-asserted-by":"crossref","unstructured":"Stump, A., Sutcliffe, G., Tinelli, C.: StarExec: a cross-community infrastructure for logic solving. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) Proceedings of the 7th International Joint Conference on Automated Reasoning. pp. 367\u2013373. No.\u00a08562 in Lecture Notes in Artificial Intelligence (2014)","DOI":"10.1007\/978-3-319-08587-6_28"},{"key":"3_CR33","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G.: SystemOnTPTP. In: McAllester, D. (ed.) Proceedings of the 17th International Conference on Automated Deduction, pp. 406\u2013410. No.\u00a01831 in Lecture Notes in Artificial Intelligence, Springer-Verlag (2000)","DOI":"10.1007\/10721959_31"},{"issue":"6","key":"3_CR34","doi-asserted-by":"publisher","first-page":"1053","DOI":"10.1142\/S0218213006003119","volume":"15","author":"G Sutcliffe","year":"2006","unstructured":"Sutcliffe, G.: Semantic Derivation Verification: techniques and Implementation. Int. J. Artif. Intell. Tools 15(6), 1053\u20131070 (2006)","journal-title":"Int. J. Artif. Intell. Tools"},{"key":"3_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1007\/978-3-540-74510-5_4","volume-title":"Computer Science \u2013 Theory and Applications","author":"G Sutcliffe","year":"2007","unstructured":"Sutcliffe, G.: TPTP, TSTP, CASC, etc. In: Diekert, V., Volkov, M.V., Voronkov, A. (eds.) CSR 2007. LNCS, vol. 4649, pp. 6\u201322. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74510-5_4"},{"key":"3_CR36","unstructured":"Sutcliffe, G.: The SZS ontologies for automated reasoning software. In: Sutcliffe, G., Rudnicki, P., Schmidt, R., Konev, B., Schulz, S. (eds.) Proceedings of the LPAR Workshops: Knowledge Exchange: Automated Provers and Proof Assistants, and the 7th International Workshop on the Implementation of Logics, pp. 38\u201349. No.\u00a0418 in CEUR Workshop Proceedings (2008)"},{"key":"3_CR37","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure. The FOF and CNF parts, v3.5.0. J. Autom. Reason. 43(4), 337\u2013362 (2009)","DOI":"10.1007\/s10817-009-9143-8"},{"key":"3_CR38","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-17511-4_1","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"G Sutcliffe","year":"2010","unstructured":"Sutcliffe, G.: The TPTP world \u2013 infrastructure for automated reasoning. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 1\u201312. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_1"},{"key":"3_CR39","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G.: The TPTP process instruction language, with applications. In: Benzm\u00fcller, C., , Woltzenlogel\u00a0Paleo, B. (eds.) Proceedings of the 11th Workshop on User Interfaces for Theorem Provers, pp.\u00a01. No.\u00a0167 in Electronic Proceedings in Theoretical Computer Science (2014)","DOI":"10.4204\/EPTCS.167.0"},{"issue":"2","key":"3_CR40","first-page":"99","volume":"37","author":"G Sutcliffe","year":"2016","unstructured":"Sutcliffe, G.: The CADE ATP system competition - CASC. AI Mag. 37(2), 99\u2013101 (2016)","journal-title":"AI Mag."},{"key":"3_CR41","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0. J. Autom. Reason. 59(4), 483\u2013502 (2017)","DOI":"10.1007\/s10817-017-9407-7"},{"issue":"6","key":"3_CR42","doi-asserted-by":"publisher","first-page":"1153","DOI":"10.1093\/jigpal\/jzac068","volume":"31","author":"G Sutcliffe","year":"2023","unstructured":"Sutcliffe, G.: The logic languages of the TPTP world. Logic J. IGPL 31(6), 1153\u20131169 (2023)","journal-title":"Logic J. IGPL"},{"issue":"1","key":"3_CR43","first-page":"1","volume":"3","author":"G Sutcliffe","year":"2010","unstructured":"Sutcliffe, G., Benzm\u00fcller, C.: Automated reasoning in higher-order logic using the TPTP THF infrastructure. J. Formaliz. Reason. 3(1), 1\u201327 (2010)","journal-title":"J. Formaliz. Reason."},{"key":"3_CR44","unstructured":"Sutcliffe, G., Kotelnikov, E.: TFX: the TPTP extended typed first-order form. In: Konev, B., Urban, J., Schulz, S. (eds.) Proceedings of the 6th Workshop on Practical Aspects of Automated Reasoning, pp. 72\u201387. No.\u00a02162 in CEUR Workshop Proceedings (2018)"},{"key":"3_CR45","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G., Kotthoff, L., Perrault, C., Khalid, Z.: An empirical assessment of progress in automated theorem proving. In: Benzm\u00fcller, C., Heule, M., Schmidt, R. (eds.) Proceedings of the 12th International Joint Conference on Automated Reasoning. Lecture Notes in Artificial Intelligence, p. To appear (2024)","DOI":"10.1007\/978-3-031-63498-7_4"},{"key":"3_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"406","DOI":"10.1007\/978-3-642-28717-6_32","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"G Sutcliffe","year":"2012","unstructured":"Sutcliffe, G., Schulz, S., Claessen, K., Baumgartner, P.: The TPTP typed first-order form with arithmetic. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR 2012. LNCS, vol. 7180, pp. 406\u2013419. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28717-6_32"},{"key":"3_CR47","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/11814771_7","volume-title":"Automated Reasoning","author":"G Sutcliffe","year":"2006","unstructured":"Sutcliffe, G., Schulz, S., Claessen, K., Van Gelder, A.: Using the TPTP language for writing derivations and finite interpretations. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 67\u201381. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11814771_7"},{"key":"3_CR48","unstructured":"Sutcliffe, G., Seyfang, D.: Smart selective competition parallelism ATP. In: Kumar, A., Russell, I. (eds.) Proceedings of the 12th International FLAIRS Conference, pp. 341\u2013345. AAAI Press (1999)"},{"key":"3_CR49","unstructured":"Sutcliffe, G., Steen, A., Fontaine, P.: The new TPTP format for interpretations. In: Korovin, K., Rawson, M., Schulz, S. (eds.) Proceedings of the 15th International Workshop on the Implementation of Logics, p. Submitted confidently (2024)"},{"key":"3_CR50","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G., Suttner, C.: The TPTP problem library: CNF release v1.2.1. J. Autom. Reason. 21(2), 177\u2013203 (1998)","DOI":"10.1023\/A:1005806324129"},{"issue":"1\u20132","key":"3_CR51","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1016\/S0004-3702(01)00113-8","volume":"131","author":"G Sutcliffe","year":"2001","unstructured":"Sutcliffe, G., Suttner, C.: Evaluating general purpose automated theorem proving systems. Artif. Intell. 131(1\u20132), 39\u201354 (2001)","journal-title":"Artif. Intell."},{"key":"3_CR52","unstructured":"Sutcliffe, G., Zimmer, J., Schulz, S.: Communication formalisms for automated theorem proving tools. In: Sorge, V., Colton, S., Fisher, M., Gow, J. (eds.) Proceedings of the Workshop on Agents and Automated Reasoning, pp. 52\u201357 (2003)"},{"key":"3_CR53","doi-asserted-by":"crossref","unstructured":"Trac, S., Puzis, Y., Sutcliffe, G.: An interactive derivation viewer. In: Autexier, S., Benzm\u00fcller, C. (eds.) Proceedings of the 7th Workshop on User Interfaces for Theorem Provers. Electronic Notes in Theoretical Computer Science, vol.\u00a0174, pp. 109\u2013123 (2007)","DOI":"10.1016\/j.entcs.2006.09.025"},{"key":"3_CR54","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/11814771_15","volume-title":"Automated Reasoning","author":"A Van Gelder","year":"2006","unstructured":"Van Gelder, A., Sutcliffe, G.: Extending the TPTP language to higher-order logic with automated parser generation. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 156\u2013161. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11814771_15"},{"key":"3_CR55","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/3-540-48660-7_34","volume-title":"Automated Deduction \u2014 CADE-16","author":"C Weidenbach","year":"1999","unstructured":"Weidenbach, C., et al.: System description: Spass version 1.0.0. In: CADE 1999. LNCS (LNAI), vol. 1632, pp. 378\u2013382. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48660-7_34"},{"key":"3_CR56","doi-asserted-by":"crossref","unstructured":"Wilson, G., Minker, J.: Resolution, refinements, and search strategies: a comparative study. IEEE Trans. Comput. C-25(8), 782\u2013801 (1976)","DOI":"10.1109\/TC.1976.1674697"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-63498-7_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:17:15Z","timestamp":1747592235000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-63498-7_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031634970","9783031634987"],"references-count":56,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-63498-7_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"1 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IJCAR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Joint Conference on Automated Reasoning","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Nancy","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ijcar2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/merz.gitlabpages.inria.fr\/2024-ijcar\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}