{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,10]],"date-time":"2026-03-10T14:57:20Z","timestamp":1773154640011,"version":"3.50.1"},"reference-count":64,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2009,7,22]],"date-time":"2009-07-22T00:00:00Z","timestamp":1248220800000},"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":[[2009,12]]},"DOI":"10.1007\/s10817-009-9143-8","type":"journal-article","created":{"date-parts":[[2009,7,21]],"date-time":"2009-07-21T07:10:15Z","timestamp":1248160215000},"page":"337-362","source":"Crossref","is-referenced-by-count":237,"title":["The TPTP Problem Library and Associated Infrastructure"],"prefix":"10.1007","volume":"43","author":[{"given":"Geoff","family":"Sutcliffe","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2009,7,22]]},"reference":[{"issue":"3","key":"9143_CR1","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1007\/BF00252180","volume":"16","author":"PB Andrews","year":"1996","unstructured":"Andrews, P.B., Bishop, M., Issar, S., Nesmith, D., Pfenning, F., Xi, H.: TPS: a theorem-proving system for classical type theory. J. Autom. Reason. 16(3), 321\u2013353 (1996)","journal-title":"J. Autom. Reason."},{"key":"9143_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1007\/11513988_4","volume-title":"Proceedings of the 17th International Conference on Computer Aided Verification","author":"C Barrett","year":"2005","unstructured":"Barrett, C., de\u00a0Moura, L., Stump, A.: SMT-COMP: satisfiability modulo theories competition. In: Etessami, K., Rajamani, S. (eds.) Proceedings of the 17th International Conference on Computer Aided Verification. Lecture Notes in Computer Science, no. 3576, pp.\u00a020\u201323. Springer, New York (2005)"},{"key":"9143_CR3","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"162","DOI":"10.1007\/978-3-540-71070-7_14","volume-title":"Proceedings of the 4th International Joint Conference on Automated Reasoning","author":"C Benzm\u00fcller","year":"2008","unstructured":"Benzm\u00fcller, C., Paulson, L., Theiss, F., Fietzke, A.: LEO-II\u2014a cooperative automatic theorem prover for higher-order logic. In: Baumgartner, P., Armando, A., Gilles, D. (eds.) Proceedings of the 4th International Joint Conference on Automated Reasoning. Lecture Notes in Artificial Intelligence, no. 5195, pp.\u00a0162\u2013170. Springer, New York (2008)"},{"key":"9143_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"491","DOI":"10.1007\/978-3-540-71070-7_41","volume-title":"Proceedings of the 4th International Joint Conference on Automated Reasoning","author":"C Benzm\u00fcller","year":"2008","unstructured":"Benzm\u00fcller, C., Rabe, F., Sutcliffe, G.: THF0\u2014the core TPTP language for classical higher-order logic. In: Baumgartner, P., Armando, A., Gilles, D. (eds.) Proceedings of the 4th International Joint Conference on Automated Reasoning. Lecture Notes in Artificial Intelligence, no. 5195, pp.\u00a0491\u2013506. Springer, New York (2008)"},{"key":"9143_CR5","doi-asserted-by":"crossref","unstructured":"Bonichon, R., Delahaye, D., Doligez, D.: Zenon: an extensible automated theorem prover producing checkable proofs. In: Dershowitz, N., Voronkov, A. (eds.) Proceedings of the 14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning. Lecture Notes in Artificial Intelligence, no. 4790, pp.\u00a0151\u2013165 (2007)","DOI":"10.1007\/978-3-540-75560-9_13"},{"issue":"3","key":"9143_CR6","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/BF02328452","volume":"2","author":"R Boyer","year":"1986","unstructured":"Boyer, R., Lusk, E.L., McCune, W.W., Overbeek, R., Stickel, M.E., Wos, L.: Set theory in first-order logic: clauses for Godel\u2019s axioms. J. Autom. Reason. 2(3), 287\u2013327 (1986)","journal-title":"J. Autom. Reason."},{"key":"9143_CR7","volume-title":"Dewey Decimal Classification and Relative Index","author":"JP Comaromi","year":"1989","unstructured":"Comaromi, J.P., Beall, J., Matthews, W.E., New, G.R.: Dewey Decimal Classification and Relative Index, 20th edn. Forest, Albany (1989)","edition":"20"},{"key":"9143_CR8","unstructured":"de\u00a0Nivelle, H., Witkowski, P.: A small framework for proof checking. In: Schmidt, R., Konev, B., Schulz, S. (eds.) Proceedings of the Workshop on Practical Aspects of Automated Reasoning, 4th International Joint Conference on Automated Reasoning. CEUR Workshop Proceedings, no. 373, pp.\u00a081\u201393 (2008)"},{"key":"9143_CR9","doi-asserted-by":"crossref","unstructured":"Denney, E., Fischer, B., Schumann, J.: Using automated theorem provers to certify auto-generated aerospace software. In: Rusinowitch, M., Basin, D. (eds.) Proceedings of the 2nd International Joint Conference on Automated Reasoning. Lecture Notes in Artificial Intelligence, no. 3097, pp.\u00a0198\u2013212 (2004)","DOI":"10.1007\/978-3-540-25984-8_12"},{"key":"9143_CR10","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/978-3-540-72200-7_3","volume-title":"Proceedings of the 9th International Conference on Logic Programming and Nonmonotonic Reasoning","author":"M Gebser","year":"2007","unstructured":"Gebser, M., Liu, L., Namasivayam, G., Neumann, A., Schaub, T., Truszczynski, M.: The first answer set programming system competition. In: Baral, C., Bewka, G., Schlipf, J. (eds.) Proceedings of the 9th International Conference on Logic Programming and Nonmonotonic Reasoning. Lecture Notes in Artificial Intelligence, no. 4483, pp.\u00a03\u201317. Springer, New York (2007)"},{"key":"9143_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"480","DOI":"10.1007\/978-3-540-48085-3_36","volume-title":"Proceedings of the 5th International Conference on the Principles and Practice of Constraint Programming","author":"I Gent","year":"1999","unstructured":"Gent, I., Walsh, T.: CSPLib: a benchmark library for constraints. In: Jaffar, J. (ed.) Proceedings of the 5th International Conference on the Principles and Practice of Constraint Programming. Lecture Notes in Computer Science, no.\u00a01713, pp.\u00a0480\u2013481. Springer, New York (1999)"},{"key":"9143_CR12","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 (2001). http:\/\/www.satlib.org\/"},{"key":"9143_CR13","volume-title":"Lecture Notes in Artificial Intelligence, no. 4180","author":"M Kohlhase","year":"2006","unstructured":"Kohlhase, M.: OMDoc\u2014an open markup format for mathematical documents [version 1.2]. In: Lecture Notes in Artificial Intelligence, no. 4180. Springer, New York (2006)"},{"issue":"2\/3","key":"9143_CR14","first-page":"127","volume":"15","author":"B Loechner","year":"2002","unstructured":"Loechner, B., Hillenbrand, T.: A phytography of Waldmeister. J. AI Commun. 15(2\/3), 127\u2013133 (2002)","journal-title":"J. AI Commun."},{"key":"9143_CR15","unstructured":"Matuszek, C., Cabral, J., Witbrock, M., DeOliveira, J.: An introduction to the syntax and content of Cyc. In: Baralm C. (ed.) Proceedings of the 2006 AAAI Spring Symposium on Formalizing and Compiling Background Knowledge and Its Applications to Knowledge Representation and Question Answering, pp.\u00a044\u201349 (2006)"},{"issue":"8","key":"9143_CR16","doi-asserted-by":"crossref","first-page":"773","DOI":"10.1109\/TC.1976.1674696","volume":"C-25","author":"JD McCharen","year":"1976","unstructured":"McCharen, J.D., Overbeek, R.A., Wos, L.A.: Problems and experiments for and with automated theorem-proving programs. IEEE Trans. Comput. C-25(8), 773\u2013782 (1976)","journal-title":"IEEE Trans. Comput."},{"key":"9143_CR17","series-title":"Advances in Formal Methods","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/978-1-4757-3188-0_16","volume-title":"Computer-Aided Reasoning: ACL2 Case Studies","author":"W McCune","year":"2000","unstructured":"McCune, W., Shumsky-Matlin, O.: Ivy: a preprocessor and proof checker for first-order logic. In: Kaufmann, M., Manolios, P., Strother\u00a0Moore, J. (eds.) Computer-Aided Reasoning: ACL2 Case Studies. Advances in Formal Methods, no. 4, pp.\u00a0265\u2013282. Kluwer Academic, Dordrecht (2000)"},{"issue":"1","key":"9143_CR18","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF00881862","volume":"10","author":"WW McCune","year":"1993","unstructured":"McCune, W.W.: Single axioms for groups and Abelian groups with various operations. J. Autom. Reason. 10(1), 1\u201313 (1993)","journal-title":"J. Autom. Reason."},{"key":"9143_CR19","doi-asserted-by":"crossref","unstructured":"McCune, W.W.: Otter 3.3 reference manual. Technical report ANL\/MSC-TM-263, Argonne National Laboratory, Argonne (2003)","DOI":"10.2172\/822573"},{"key":"9143_CR20","series-title":"Lecture Notes in Artificial Intelligence","first-page":"209","volume-title":"Proceedings of the 11th International Conference on Automated Deduction","author":"WW McCune","year":"1992","unstructured":"McCune, W.W., Wos, L.: Experiments in automated deduction with condensed detachment. In: Kapur, D. (ed.) Proceedings of the 11th International Conference on Automated Deduction. Lecture Notes in Artificial Intelligence, no. 607, pp.\u00a0209\u2013223. Springer, New York (1992)"},{"issue":"10","key":"9143_CR21","doi-asserted-by":"crossref","first-page":"1575","DOI":"10.1016\/j.ic.2005.05.010","volume":"204","author":"J Meng","year":"2006","unstructured":"Meng, J., Quigley, C., Paulson, L.: Automation for interactive proof: first prototype. Inf. Comput. 204(10), 1575\u20131596 (2006)","journal-title":"Inf. Comput."},{"issue":"2","key":"9143_CR22","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/s10817-004-3243-2","volume":"33","author":"M Newborn","year":"2004","unstructured":"Newborn, M., Wang, Z.: Octopus: combining Learning and parallel search. J. Autom. Reason. 33(2), 171\u2013218 (2004)","journal-title":"J. Autom. Reason."},{"issue":"2\u20133","key":"9143_CR23","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":"9143_CR24","unstructured":"Pease, A., Sutcliffe, G.: First order reasoning on a large ontology. In: Urban, J., Sutcliffe, G., Schulz, S. (eds.) Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories. CEUR Workshop Proceedings, no. 257, pp.\u00a059\u201369 (2007)"},{"issue":"2","key":"9143_CR25","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/BF02432151","volume":"2","author":"FJ Pelletier","year":"1986","unstructured":"Pelletier, F.J.: Seventy-five problems for testing automatic theorem provers. J. Autom. Reason. 2(2), 191\u2013216 (1986)","journal-title":"J. Autom. Reason."},{"key":"9143_CR26","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"202","DOI":"10.1007\/3-540-48660-7_14","volume-title":"Proceedings of the 16th International Conference on Automated Deduction","author":"F Pfenning","year":"1999","unstructured":"Pfenning, F., Sch\u00fcrmann, C.: System description: Twelf\u2014a meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) Proceedings of the 16th International Conference on Automated Deduction. Lecture Notes in Artificial Intelligence, no. 1632, pp.\u00a0202\u2013206. Springer, New York (1999)"},{"issue":"3","key":"9143_CR27","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/BF00244944","volume":"4","author":"DA Plaisted","year":"1988","unstructured":"Plaisted, D.A.: Non-Horn clause logic programming without contrapositives. J. Autom. Reason. 4(3), 287\u2013325 (1988)","journal-title":"J. Autom. Reason."},{"key":"9143_CR28","first-page":"49","volume-title":"Proceedings of the 19th International FLAIRS Conference","author":"Y Puzis","year":"2006","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.\u00a049\u201354. AAAI, Menlo Park (2006)"},{"issue":"1","key":"9143_CR29","doi-asserted-by":"crossref","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":"9143_CR30","unstructured":"Ramachandran, D., Reagan, P., Goolsbey, K.: First-orderized researchCyc: expressiveness and efficiency in a common sense knowledge base. In: Shvaiko, P. (ed.) Proceedings of the Workshop on Contexts and Ontologies: Theory, Practice and Applications (2005)"},{"key":"9143_CR31","unstructured":"Ranise, S., Tinelli, C.: The SMT-LIB standard: version 1.2. Technical report, Department of Computer Science, The University of Iowa, Iowa City (2006)"},{"issue":"1\u20132","key":"9143_CR32","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1007\/s10817-006-9060-z","volume":"38","author":"T Raths","year":"2007","unstructured":"Raths, T., Otten, J., Kreitz, C.: The ILTP problem library for intuitionistic logic\u2014release v1.1. J. Autom. Reason. 38(1\u20132), 261\u2013271 (2007)","journal-title":"J. Autom. Reason."},{"key":"9143_CR33","series-title":"Lecture Notes in Artificial Intelligence","first-page":"320","volume-title":"Proceedings of the Joint German\/Austrian Conference on Artificial Intelligence","author":"S Schulz","year":"2001","unstructured":"Schulz, S.: Learning search control knowledge for equational theorem proving. In: Baader, F., Brewka, G., Eiter, T. (eds.) Proceedings of the Joint German\/Austrian Conference on Artificial Intelligence. Lecture Notes in Artificial Intelligence, no. 2174, pp.\u00a0320\u2013334. Springer, New York (2001)"},{"issue":"2\u20133","key":"9143_CR34","first-page":"111","volume":"15","author":"S Schulz","year":"2002","unstructured":"Schulz, S.: E: a brainiac theorem prover. AI Commun. 15(2\u20133), 111\u2013126 (2002)","journal-title":"AI Commun."},{"key":"9143_CR35","unstructured":"Schulz, S., Bonacina, M.-P.: On handling distinct objects in the superposition calculus. In: Konev, B., Schulz, S. (eds.) Proceedings of the 5th International Workshop on the Implementation of Logics, pp.\u00a066\u201377 (2005)"},{"key":"9143_CR36","series-title":"Lecture Notes in Artificial Intelligence","first-page":"143","volume-title":"Proceedings of the 18th International Conference on Automated Deduction","author":"JH Siekmann","year":"2002","unstructured":"Siekmann, J.H., Benzm\u00fcller, C., Brezhnev, V., Cheikhrouhou, L., Fiedler, A., Franke, A., Horacek, H., Kohlhase, M., Meier, A., Melis, E., Moschner, M., Normann, I., Pollet, M., Sorge, V., Ullrich, C., Wirth, C.P., Zimmer, J.: Proof development with OMEGA. In: Voronkov, A. (ed.) Proceedings of the 18th International Conference on Automated Deduction. Lecture Notes in Artificial Intelligence, no. 2392, pp.\u00a0143\u2013148. Springer, New York (2002)"},{"key":"9143_CR37","volume-title":"Mathematical Subject Classification","author":"American Mathematical Society","year":"1992","unstructured":"American\u00a0Mathematical Society: Mathematical Subject Classification. American Mathematical Society, Providence (1992)"},{"key":"9143_CR38","unstructured":"Stickel, M.E.: SNARK\u2014SRI\u2019s New Automated Reasoning Kit. http:\/\/www.ai.sri.com\/~stickel\/snark.html"},{"key":"9143_CR39","first-page":"1197","volume-title":"Proceedings of the 22nd Conference on Artificial Intelligence","author":"M Streeter","year":"2007","unstructured":"Streeter, M., Golovin, D., Smith, S.F.: Combining multiple heuristics online. In: Holte, R.C., Howe, A. (eds.) Proceedings of the 22nd Conference on Artificial Intelligence, pp.\u00a01197\u20131203. AAAI, Menlo Park (2007)"},{"key":"9143_CR40","doi-asserted-by":"crossref","unstructured":"Suchanek, F., Kasneci, G., Weikum, G.: YAGO: a core of semantic knowledge. In: Patel-Schneider, P., Shenoy, P. (eds.) Proceedings of the 16th International World Wide Web Conference, pp.\u00a0697\u2013706 (2007)","DOI":"10.1145\/1242572.1242667"},{"key":"9143_CR41","doi-asserted-by":"crossref","unstructured":"Suda, M., Sutcliffe, G., Wischnewsk, P., Lamotte-Schubert, M.: External sources of axioms in automated theorem proving. In: Mertsching, B. (ed.) Proceedings of the 32nd Annual Conference on Artificial Intelligence (2009)","DOI":"10.1007\/978-3-642-04617-9_36"},{"key":"9143_CR42","unstructured":"Sutcliffe, G.: The TSTP Solution Library. http:\/\/www.TPTP.org\/TSTP"},{"key":"9143_CR43","series-title":"Lecture Notes in Artificial Intelligence","first-page":"406","volume-title":"Proceedings of the 17th International Conference on Automated Deduction","author":"G Sutcliffe","year":"2000","unstructured":"Sutcliffe, G.: SystemOnTPTP. In: McAllester, D. (ed.) Proceedings of the 17th International Conference on Automated Deduction. Lecture Notes in Artificial Intelligence, no. 1831, pp.\u00a0406\u2013410. Springer, New York (2000)"},{"issue":"6","key":"9143_CR44","doi-asserted-by":"crossref","first-page":"1053","DOI":"10.1142\/S0218213006003119","volume":"15","author":"G Sutcliffe","year":"2006","unstructured":"Sutcliffe, G.: Semantic derivation verification. Int. J. Artif. Intell. Tools 15(6), 1053\u20131070 (2006)","journal-title":"Int. J. Artif. Intell. Tools"},{"key":"9143_CR45","series-title":"Lecture Notes in Computer Science","first-page":"7","volume-title":"Proceedings of the 2nd International Computer Science Symposium in Russia","author":"G Sutcliffe","year":"2007","unstructured":"Sutcliffe, G.: TPTP, TSTP, CASC, etc. In: Diekert, V., Volkov, M., Voronkov, A. (eds.) Proceedings of the 2nd International Computer Science Symposium in Russia. Lecture Notes in Computer Science, no. 4649, pp.\u00a07\u201323. Springer, New York (2007)"},{"issue":"1","key":"9143_CR46","first-page":"71","volume":"21","author":"G Sutcliffe","year":"2008","unstructured":"Sutcliffe, G.: The CADE-21 automated theorem proving system competition. AI Commun. 21(1), 71\u201382 (2008)","journal-title":"AI Commun."},{"key":"9143_CR47","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. CEUR Workshop Proceedings, no. 418, pp.\u00a038\u201349 (2008)"},{"key":"9143_CR48","author":"G Sutcliffe","year":"2009","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure. The FOF and CNF Parts, v3.5.0. J. Autom. Reason. (2009). doi: 10.1007\/s10817-009-9143-8","journal-title":"J. Autom. Reason."},{"key":"9143_CR49","unstructured":"Sutcliffe, G., Fuchs, M., Suttner, C.: Progress in automated theorem proving, 1997\u20131999. In: Hoos, H., St\u00fctzle, T. (eds.) Proceedings of the IJCAI\u201901 Workshop on Empirical Methods in Artificial Intelligence, pp.\u00a053\u201360 (2001)"},{"key":"9143_CR50","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1007\/978-3-540-73595-3_20","volume-title":"Proceedings of the 21st International Conference on Automated Deduction","author":"G Sutcliffe","year":"2007","unstructured":"Sutcliffe, G., Puzis, Y.: SRASS\u2014a semantic relevance axiom selection system. In: Pfenning, F. (ed.) Proceedings of the 21st International Conference on Automated Deduction. Lecture Notes in Artificial Intelligence, no. 4603, pp.\u00a0295\u2013310. Springer, New York (2007)"},{"key":"9143_CR51","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G., Schulz, S., Claessen, K., Van\u00a0Gelder, A.: Using the TPTP language for writing derivations and finite interpretations. In: Furbach, U., Shankar, N. (eds.) Proceedings of the 3rd International Joint Conference on Automated Reasoning. Lecture Notes in Artificial Intelligence, no. 4130, pp.\u00a067\u201381 (2006)","DOI":"10.1007\/11814771_7"},{"key":"9143_CR52","first-page":"341","volume-title":"Proceedings of the 12th International FLAIRS Conference","author":"G Sutcliffe","year":"1999","unstructured":"Sutcliffe, G., Seyfang, D.: Smart selective competition parallelism ATP. In: Kumar, A., Russell, I. (eds.) Proceedings of the 12th International FLAIRS Conference, pp.\u00a0341\u2013345. AAAI, Menlo Park (1999)"},{"issue":"1","key":"9143_CR53","first-page":"35","volume":"19","author":"G Sutcliffe","year":"2006","unstructured":"Sutcliffe, G., Suttner, C.: The state of CASC. AI Commun. 19(1), 35\u201348 (2006)","journal-title":"AI Commun."},{"issue":"3","key":"9143_CR54","doi-asserted-by":"crossref","first-page":"307","DOI":"10.1023\/A:1015736313131","volume":"28","author":"G Sutcliffe","year":"2002","unstructured":"Sutcliffe, G., Suttner, C., Pelletier, F.J.: The IJCAR ATP system competition. J. Autom. Reason. 28(3), 307\u2013320 (2002)","journal-title":"J. Autom. Reason."},{"issue":"2","key":"9143_CR55","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1023\/A:1005806324129","volume":"21","author":"G Sutcliffe","year":"1998","unstructured":"Sutcliffe, G., Suttner, C.B.: The TPTP problem library: CNF release v1.2.1. J. Autom. Reason. 21(2), 177\u2013203 (1998)","journal-title":"J. Autom. Reason."},{"issue":"1\u20132","key":"9143_CR56","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1016\/S0004-3702(01)00113-8","volume":"131","author":"G Sutcliffe","year":"2001","unstructured":"Sutcliffe, G., Suttner, C.B.: Evaluating general purpose automated theorem proving systems. Artif. Intell. 131(1\u20132), 39\u201354 (2001)","journal-title":"Artif. Intell."},{"key":"9143_CR57","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, 18th International Joint Conference on Artificial Intelligence, pp.\u00a052\u201357 (2003)"},{"issue":"2","key":"9143_CR58","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1023\/A:1005887414560","volume":"18","author":"T Tammet","year":"1997","unstructured":"Tammet, T.: Gandalf. J. Autom. Reason. 18(2), 199\u2013204 (1997)","journal-title":"J. Autom. Reason."},{"key":"9143_CR59","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, 3rd International Joint Conference on Automated Reasoning. Electronic Notes in Theoretical Computer Science, vol. 174, pp.\u00a0109\u2013123 (2006)","DOI":"10.1016\/j.entcs.2006.09.025"},{"key":"9143_CR60","unstructured":"Trac, S., Sutcliffe, G., Pease, A.: Integration of the TPTPWorld into SigmaKEE. In: Schmidt, R., Konev, B., Schulz, S. (eds.) Proceedings of the Workshop on Practical Aspects of Automated Reasoning, 4th International Joint Conference on Automated Reasoning. CEUR Workshop Proceedings, no. 373, pp.\u00a0103\u2013114 (2008)"},{"issue":"1\u20132","key":"9143_CR61","first-page":"21","volume":"37","author":"J Urban","year":"2006","unstructured":"Urban, J.: MPTP 0.2: design, implementation, and initial experiments. J. Autom. Reason. 37(1\u20132), 21\u201343 (2006)","journal-title":"J. Autom. Reason."},{"key":"9143_CR62","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"441","DOI":"10.1007\/978-3-540-71070-7_37","volume-title":"Proceedings of the 4th International Joint Conference on Automated Reasoning","author":"J Urban","year":"2008","unstructured":"Urban, J., Sutcliffe, G., Pudlak, P., Vyskocil, J.: MaLARea SG1: machine learner for automated reasoning with semantic guidance. In: Baumgartner, P., Armando, A., Gilles, D. (eds.) Proceedings of the 4th International Joint Conference on Automated Reasoning. Lecture Notes in Artificial Intelligence, no. 5195, pp.\u00a0441\u2013456. Springer, New York (2008)"},{"key":"9143_CR63","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"156","DOI":"10.1007\/11814771_15","volume-title":"Proceedings of the 3rd International Joint Conference on Automated Reasoning","author":"A Gelder Van","year":"2006","unstructured":"Van\u00a0Gelder, A., Sutcliffe, G.: Extending the TPTP language to higher-order logic with automated parser generation. In: Furbach, U., Shankar, N. (eds.) Proceedings of the 3rd International Joint Conference on Automated Reasoning. Lecture Notes in Artificial Intelligence, no. 4130, pp.\u00a0156\u2013161. Springer, New York (2006)"},{"issue":"2","key":"9143_CR64","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1142\/S0218001499000136","volume":"13","author":"A Wolf","year":"1999","unstructured":"Wolf, A., Letz, R.: Strategy parallelism in automated theorem proving. Int. J. Pattern Recogn. Artif. Intell. 13(2), 219\u2013245 (1999)","journal-title":"Int. J. Pattern Recogn. Artif. Intell."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-009-9143-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-009-9143-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-009-9143-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,26]],"date-time":"2023-05-26T02:16:58Z","timestamp":1685067418000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-009-9143-8"}},"subtitle":["The FOF and CNF Parts, v3.5.0"],"short-title":[],"issued":{"date-parts":[[2009,7,22]]},"references-count":64,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2009,12]]}},"alternative-id":["9143"],"URL":"https:\/\/doi.org\/10.1007\/s10817-009-9143-8","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,7,22]]}}}