{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,7]],"date-time":"2025-10-07T14:32:19Z","timestamp":1759847539532,"version":"3.40.3"},"publisher-location":"Cham","reference-count":51,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030294359"},{"type":"electronic","value":"9783030294366"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-29436-6_8","type":"book-chapter","created":{"date-parts":[[2019,8,20]],"date-time":"2019-08-20T16:04:02Z","timestamp":1566317042000},"page":"123-141","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["GRUNGE: A Grand Unified ATP Challenge"],"prefix":"10.1007","author":[{"given":"Chad E.","family":"Brown","sequence":"first","affiliation":[]},{"given":"Thibault","family":"Gauthier","sequence":"additional","affiliation":[]},{"given":"Cezary","family":"Kaliszyk","sequence":"additional","affiliation":[]},{"given":"Geoff","family":"Sutcliffe","sequence":"additional","affiliation":[]},{"given":"Josef","family":"Urban","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,8,20]]},"reference":[{"issue":"2","key":"8_CR1","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s10817-013-9286-5","volume":"52","author":"J Alama","year":"2014","unstructured":"Alama, J., Heskes, T., K\u00fchlwein, D., Tsivtsivadze, E., Urban, J.: Premise selection for mathematics by corpus analysis and kernel methods. J. Autom. Reason. 52(2), 191\u2013213 (2014). https:\/\/doi.org\/10.1007\/s10817-013-9286-5","journal-title":"J. Autom. Reason."},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2011","unstructured":"Barrett, C., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-642-38574-2_3","volume-title":"Automated Deduction \u2013 CADE-24","author":"P Baumgartner","year":"2013","unstructured":"Baumgartner, P., Waldmann, U.: Hierarchic superposition with weak abstraction. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 39\u201357. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_3"},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-540-71070-7_14","volume-title":"Automated Reasoning","author":"C Benzm\u00fcller","year":"2008","unstructured":"Benzm\u00fcller, C., Paulson, L.C., Theiss, F., Fietzke, A.: LEO-II - a cooperative automatic theorem prover for classical higher-order logic (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 162\u2013170. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71070-7_14"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/978-3-540-71070-7_41","volume-title":"Automated Reasoning","author":"C Benzm\u00fcller","year":"2008","unstructured":"Benzm\u00fcller, C., Rabe, F., Sutcliffe, G.: THF0 \u2013 the core of the TPTP language for higher-order logic. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 491\u2013506. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71070-7_41. http:\/\/christoph-benzmueller.de\/papers\/C25.pdf"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1007\/978-3-642-36742-7_34","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"JC Blanchette","year":"2013","unstructured":"Blanchette, J.C., B\u00f6hme, S., Popescu, A., Smallbone, N.: Encoding monomorphic and polymorphic types. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 493\u2013507. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_34"},{"issue":"1","key":"8_CR7","doi-asserted-by":"publisher","first-page":"101","DOI":"10.6092\/issn.1972-5787\/4593","volume":"9","author":"JC Blanchette","year":"2016","unstructured":"Blanchette, J.C., Kaliszyk, C., Paulson, L.C., Urban, J.: Hammering towards QED. J. Formalized Reason. 9(1), 101\u2013148 (2016). https:\/\/doi.org\/10.6092\/issn.1972-5787\/4593","journal-title":"J. Formalized Reason."},{"key":"8_CR8","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":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-642-14052-5_14","volume-title":"Interactive Theorem Proving","author":"S B\u00f6hme","year":"2010","unstructured":"B\u00f6hme, S., Weber, T.: Fast LCF-style proof reconstruction for Z3. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 179\u2013194. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14052-5_14"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-642-31365-3_11","volume-title":"Automated Reasoning","author":"CE Brown","year":"2012","unstructured":"Brown, C.E.: Satallax: an automatic higher-order prover. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 111\u2013117. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31365-3_11"},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-642-22438-6_14","volume-title":"Automated Deduction \u2013 CADE-23","author":"G Burel","year":"2011","unstructured":"Burel, G.: Experimenting with deduction modulo. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 162\u2013176. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22438-6_14"},{"key":"8_CR12","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A Church","year":"1940","unstructured":"Church, A.: A formulation of the simple theory of types. J. Symb. Logic 5, 56\u201368 (1940)","journal-title":"J. Symb. Logic"},{"key":"8_CR13","unstructured":"Cruanes, S.: Extending superposition with integer arithmetic, structural induction, and beyond. (Extensions de la Superposition pour l\u2019Arithm\u00e9tique Lin\u00e9aire Enti\u00e8re, l\u2019Induction Structurelle, et bien plus encore). Ph.D. thesis, \u00c9cole Polytechnique, Palaiseau, France (2015). https:\/\/tel.archives-ouvertes.fr\/tel-01223502"},{"key":"8_CR14","doi-asserted-by":"publisher","unstructured":"Czajka, L.: Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions. In: Avigad, J., Chlipala, A. (eds.) Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, Saint Petersburg, FL, USA, 20\u201322 January 2016, pp. 49\u201357. ACM (2016). https:\/\/doi.org\/10.1145\/2854065.2854069","DOI":"10.1145\/2854065.2854069"},{"key":"8_CR15","doi-asserted-by":"publisher","unstructured":"Delahaye, D., Doligez, D., Gilbert, F., Halmagrand, P., Hermant, O.: Zenon modulo: when achilles outruns the tortoise using deduction modulo. In: McMillan et al. [34], pp. 274\u2013290. https:\/\/doi.org\/10.1007\/978-3-642-45221-5_20","DOI":"10.1007\/978-3-642-45221-5_20"},{"key":"8_CR16","doi-asserted-by":"publisher","unstructured":"Gauthier, T., Kaliszyk, C.: Premise selection and external provers for HOL4. In: Certified Programs and Proofs (CPP 2015). ACM (2015). https:\/\/doi.org\/10.1145\/2676724.2693173","DOI":"10.1145\/2676724.2693173"},{"key":"8_CR17","unstructured":"Gauthier, T., Kaliszyk, C., Urban, J.: TacticToe: learning to reason with HOL4 tactics. In: Eiter, T., Sands, D. (eds.) 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR-21, Maun, Botswana, 7\u201312 May 2017. EPiC Series in Computing, vol. 46, pp. 125\u2013143. EasyChair (2017). http:\/\/www.easychair.org\/publications\/paper\/340355"},{"key":"8_CR18","unstructured":"Gauthier, T., Kaliszyk, C., Urban, J., Kumar, R., Norrish, M.: Learning to prove with tactics. CoRR (2018). http:\/\/arxiv.org\/abs\/1804.00596"},{"key":"8_CR19","unstructured":"Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press (1993). http:\/\/www.cs.ox.ac.uk\/tom.melham\/pub\/Gordon-1993-ITH.html"},{"key":"8_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/BFb0031814","volume-title":"Formal Methods in Computer-Aided Design","author":"J Harrison","year":"1996","unstructured":"Harrison, J.: HOL light: a tutorial introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 265\u2013269. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/BFb0031814"},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/3-540-61511-3_97","volume-title":"Automated Deduction \u2014 Cade-13","author":"J Harrison","year":"1996","unstructured":"Harrison, J.: Optimizing proof search in model elimination. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 313\u2013327. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61511-3_97"},{"key":"8_CR22","doi-asserted-by":"publisher","unstructured":"Harrison, J., Urban, J., Wiedijk, F.: History of interactive theorem proving. In: Siekmann, J.H. (ed.) Computational Logic, Handbook of the History of Logic, vol. 9, pp. 135\u2013214. Elsevier (2014). https:\/\/doi.org\/10.1016\/B978-0-444-51624-4.50004-6","DOI":"10.1016\/B978-0-444-51624-4.50004-6"},{"key":"8_CR23","unstructured":"Hurd, J.: First-order proof tactics in higher-order logic theorem provers. Design and Application of Strategies\/Tactics in Higher Order Logics, number NASA\/CP-2003-212448 in NASA Technical reports, pp. 56\u201368 (2003)"},{"key":"8_CR24","unstructured":"Hurd, J.: System description: the metis proof tactic. In: Benzmueller, C., Harrison, J., Schurmann, C. (ed.) Workshop on Empirically Successful Automated Reasoning in Higher-Order Logic (ESHOL), pp. 103\u2013104 (2005). https:\/\/arxiv.org\/pdf\/cs\/0601042"},{"key":"8_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/978-3-642-20398-5_14","volume-title":"NASA Formal Methods","author":"J Hurd","year":"2011","unstructured":"Hurd, J.: The opentheory standard theory library. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 177\u2013191. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-20398-5_14"},{"key":"8_CR26","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. CEUR Workshop Proceedings, vol. 1635, pp. 41\u201355 (2016)"},{"issue":"2","key":"8_CR27","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/s10817-014-9303-3","volume":"53","author":"C Kaliszyk","year":"2014","unstructured":"Kaliszyk, C., Urban, J.: Learning-assisted automated reasoning with Flyspeck. J. Autom. Reason. 53(2), 173\u2013213 (2014). https:\/\/doi.org\/10.1007\/s10817-014-9303-3","journal-title":"J. Autom. Reason."},{"key":"8_CR28","first-page":"106","volume":"11","author":"D King","year":"1996","unstructured":"King, D., Arthan, R., Winnersh, I.: Development of practical verification tools. ICL Syst. J. 11, 106\u2013122 (1996)","journal-title":"ICL Syst. J."},{"key":"8_CR29","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/978-3-540-71070-7_24","volume-title":"Automated Reasoning","author":"K Korovin","year":"2008","unstructured":"Korovin, K.: iProver \u2013 an instantiation-based theorem prover for first-order logic (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 292\u2013298. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71070-7_24"},{"key":"8_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-39799-8_1","volume-title":"Computer Aided Verification","author":"L Kov\u00e1cs","year":"2013","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1\u201335. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_1"},{"key":"8_CR31","doi-asserted-by":"publisher","unstructured":"Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. In: Jagannathan, S., Sewell, P. (eds.) The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014, San Diego, CA, USA, 20\u201321 January 2014, pp. 179\u2013192. ACM (2014). https:\/\/doi.org\/10.1145\/2535838.2535841","DOI":"10.1145\/2535838.2535841"},{"key":"8_CR32","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-3-319-08587-6_5","volume-title":"Automated Reasoning","author":"F Lindblad","year":"2014","unstructured":"Lindblad, F.: A focused sequent calculus for higher-order logic. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 61\u201375. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_5"},{"key":"8_CR33","unstructured":"McCune, W.: Prover9 and Mace4 (2005\u20132010). http:\/\/www.cs.unm.edu\/~mccune\/prover9\/"},{"key":"8_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-45221-5","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","year":"2013","unstructured":"McMillan, K.L., Middeldorp, A., Voronkov, A. (eds.): LPAR 2013. LNCS, vol. 8312. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-45221-5"},{"issue":"1","key":"8_CR35","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/s10817-007-9085-y","volume":"40","author":"J Meng","year":"2008","unstructured":"Meng, J., Paulson, L.C.: Translating higher-order clauses to first-order clauses. J. Autom. Reason. 40(1), 35\u201360 (2008)","journal-title":"J. Autom. Reason."},{"key":"8_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"key":"8_CR37","doi-asserted-by":"publisher","unstructured":"Pfenning, F., Elliot, C.: Higher-order abstract syntax. In: Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation, PLDI 1988, pp. 199\u2013208. ACM, New York (1988). https:\/\/doi.org\/10.1145\/53990.54010","DOI":"10.1145\/53990.54010"},{"key":"8_CR38","unstructured":"Pitts, A.: The HOL logic. In: Gordon and Melham [19]. http:\/\/www.cs.ox.ac.uk\/tom.melham\/pub\/Gordon-1993-ITH.html"},{"key":"8_CR39","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/978-3-540-89439-1_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P R\u00fcmmer","year":"2008","unstructured":"R\u00fcmmer, P.: A constraint sequent calculus for first-order logic with linear integer arithmetic. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 274\u2013289. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-89439-1_20"},{"key":"8_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/978-3-642-28717-6_28","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P R\u00fcmmer","year":"2012","unstructured":"R\u00fcmmer, P.: E-matching with free variables. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR 2012. LNCS, vol. 7180, pp. 359\u2013374. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28717-6_28"},{"key":"8_CR41","doi-asserted-by":"publisher","unstructured":"Schulz, S.: System description: E 1.8. In: McMillan et al. [34], pp. 735\u2013743. https:\/\/doi.org\/10.1007\/978-3-642-45221-5_49","DOI":"10.1007\/978-3-642-45221-5_49"},{"key":"8_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-540-71067-7_6","volume-title":"Theorem Proving in Higher Order Logics","author":"K Slind","year":"2008","unstructured":"Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 28\u201332. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71067-7_6"},{"key":"8_CR43","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-319-94205-6_8","volume-title":"Automated Reasoning","author":"A Steen","year":"2018","unstructured":"Steen, A., Benzm\u00fcller, C.: The higher-order prover Leo-III. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS (LNAI), vol. 10900, pp. 108\u2013116. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94205-6_8. http:\/\/christoph-benzmueller.de\/papers\/C70.pdf"},{"key":"8_CR44","unstructured":"Steen, A., Wisniewski, M., Benzm\u00fcller, C.: Going polymorphic - TH1 reasoning for Leo-III. In: Eiter, T., Sands, D., Sutcliffe, G., Voronkov, A. (eds.) IWIL@LPAR 2017 Workshop and LPAR-21 Short Presentations, Maun, Botswana, 7\u201312 May 2017, vol. 1. Kalpa Publications in Computing, EasyChair (2017). http:\/\/www.easychair.org\/publications\/paper\/346851"},{"issue":"2","key":"8_CR45","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."},{"issue":"4","key":"8_CR46","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/s10817-017-9407-7","volume":"59","author":"G Sutcliffe","year":"2017","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)","journal-title":"J. Autom. Reason."},{"key":"8_CR47","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"},{"issue":"6","key":"8_CR48","doi-asserted-by":"publisher","first-page":"495","DOI":"10.3233\/AIC-180773","volume":"31","author":"G Sutcliffe","year":"2018","unstructured":"Sutcliffe, G.: The 9th IJCAR automated theorem proving system competition - CASC-J9. AI Commun. 31(6), 495\u2013507 (2018). https:\/\/doi.org\/10.3233\/AIC-180773","journal-title":"AI Commun."},{"issue":"5","key":"8_CR49","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1007\/s10009-011-0188-8","volume":"13","author":"T Weber","year":"2011","unstructured":"Weber, T.: SMT solvers: new oracles for the HOL theorem prover. Int. J. Softw. Tools Technol. Transfer 13(5), 419\u2013429 (2011). https:\/\/doi.org\/10.1007\/s10009-011-0188-8","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"8_CR50","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-642-02959-2_10","volume-title":"Automated Deduction \u2013 CADE-22","author":"C Weidenbach","year":"2009","unstructured":"Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 140\u2013145. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02959-2_10"},{"key":"8_CR51","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1016\/j.ins.2018.04.086","volume":"462","author":"Y Xu","year":"2018","unstructured":"Xu, Y., Liu, J., Chen, S., Zhong, X., He, X.: Contradiction separation based dynamic multi-clause synergized automated deduction. Inf. Sci. 462, 93\u2013113 (2018)","journal-title":"Inf. Sci."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 27"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-29436-6_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,11]],"date-time":"2022-07-11T21:54:39Z","timestamp":1657576479000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-29436-6_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030294359","9783030294366"],"references-count":51,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-29436-6_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"20 August 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Natal","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Brazil","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 August 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 August 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.mat.ufrn.br\/CADE-27\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}