{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T06:40:04Z","timestamp":1748414404532,"version":"3.41.0"},"publisher-location":"Cham","reference-count":54,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031669965"},{"type":"electronic","value":"9783031669972"}],"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:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-66997-2_18","type":"book-chapter","created":{"date-parts":[[2024,8,3]],"date-time":"2024-08-03T20:03:12Z","timestamp":1722715392000},"page":"315-333","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Solving Hard Mizar Problems with\u00a0Instantiation and\u00a0Strategy Invention"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8848-5537","authenticated-orcid":false,"given":"Jan","family":"Jakub\u016fv","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3487-784X","authenticated-orcid":false,"given":"Mikol\u00e1\u0161","family":"Janota","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1384-1613","authenticated-orcid":false,"given":"Josef","family":"Urban","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,29]]},"reference":[{"issue":"1\u20134","key":"18_CR1","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/s10817-017-9440-6","volume":"61","author":"G Bancerek","year":"2018","unstructured":"Bancerek, G., et al.: The role of the Mizar mathematical library for interactive proof development in Mizar. J. Autom. Reason. 61(1\u20134), 9\u201332 (2018)","journal-title":"J. Autom. Reason."},{"key":"18_CR2","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/978-3-319-20615-8_17","volume-title":"Intelligent Computer Mathematics","author":"G Bancerek","year":"2015","unstructured":"Bancerek, G., et al.: Mizar: state-of-the-art and beyond. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS (LNAI), vol. 9150, pp. 261\u2013279. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-20615-8_17"},{"key":"18_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/978-3-030-99524-9_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Barbosa","year":"2022","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: Fisman, D., Rosu, G. (eds.) TACAS 2022. LNCS, vol. 13243, pp. 415\u2013442. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24"},{"key":"18_CR4","unstructured":"Barrett, C., Stump, A., Tinelli, C., et\u00a0al.: The SMT-LIB standard: version 2.0. In: Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh, UK), vol. 13, p. 14 (2010)"},{"key":"18_CR5","unstructured":"Bj\u00f8rner, N., Janota, M.: Playing with quantified satisfaction. In: 20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning \u2013 Short Presentations, LPAR, vol. 35, pp. 15\u201327. EasyChair (2015)"},{"issue":"1","key":"18_CR6","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/s10817-013-9278-5","volume":"51","author":"JC Blanchette","year":"2013","unstructured":"Blanchette, J.C., B\u00f6hme, S., Paulson, L.C.: Extending sledgehammer with SMT solvers. J. Autom. Reason. 51(1), 109\u2013128 (2013)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"18_CR7","first-page":"101","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)","journal-title":"J. Formalized Reason."},{"key":"18_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1007\/978-3-031-10769-6_21","volume-title":"Automated Reasoning","author":"CE Brown","year":"2022","unstructured":"Brown, C.E., Kaliszyk, C.: Lash 1.0 (system description). In: Blanchette, J., Kov\u00e1cs, L., Pattinson, D. (eds.) IJCAR 2022. LNCS, vol. 13385, pp. 350\u2013358. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-10769-6_21"},{"key":"18_CR9","doi-asserted-by":"crossref","unstructured":"Chvalovsk\u00fd, K., Korovin, K., Piepenbrock, J., Urban, J.: Guiding an instantiation prover with graph neural networks. In: LPAR. EPiC Series in Computing, vol. 94, pp. 112\u2013123. EasyChair (2023)","DOI":"10.29007\/tp23"},{"key":"18_CR10","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/3-540-46508-1_9","volume-title":"Automated Deduction in Classical and Non-Classical Logics","author":"I Dahn","year":"2000","unstructured":"Dahn, I.: Interpretation of a Mizar-like logic in first order logic. In: Caferra, R., Salzer, G. (eds.) FTP 1998. LNCS (LNAI), vol. 1761, pp. 137\u2013151. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-46508-1_9"},{"key":"18_CR11","unstructured":"Dahn, I., Wernhard, C.: First order proof problems extracted from an article in the MIZAR mathematical library. In: Bonacina, M.P., Furbach, U. (eds.) International Workshop on First-Order Theorem Proving (FTP 1997), RISC-Linz Report Series No. 97-50, pp. 58\u201362. Johannes Kepler Universit\u00e4t, Linz (1997)"},{"key":"18_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"18_CR13","unstructured":"Desharnais, M., Vukmirovic, P., Blanchette, J., Wenzel, M.: Seventeen provers under the hammer. In: ITP. LIPIcs, vol. 237, pp. 8:1\u20138:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022)"},{"issue":"3","key":"18_CR14","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"D Detlefs","year":"2005","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365\u2013473 (2005)","journal-title":"J. ACM"},{"key":"18_CR15","doi-asserted-by":"crossref","unstructured":"Farzan, A., Kincaid, Z.: Strategy synthesis for linear arithmetic games. Proc. ACM Program. Lang. 2(POPL), 61:1\u201361:30 (2018)","DOI":"10.1145\/3158149"},{"key":"18_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-642-02658-4_25","volume-title":"Computer Aided Verification","author":"Y Ge","year":"2009","unstructured":"Ge, Y., de Moura, L.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 306\u2013320. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_25"},{"key":"18_CR17","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-030-86205-3_10","volume-title":"Frontiers of Combining Systems","author":"ZA Goertzel","year":"2021","unstructured":"Goertzel, Z.A., Chvalovsk\u00fd, K., Jakub\u016fv, J., Ol\u0161\u00e1k, M., Urban, J.: Fast and slow enigmas and parental guidance. In: Konev, B., Reger, G. (eds.) FroCoS 2021. LNCS (LNAI), vol. 12941, pp. 173\u2013191. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-86205-3_10"},{"key":"18_CR18","unstructured":"Goertzel, Z.A., Jakub\u016fv, J., Kaliszyk, C., Ols\u00e1k, M., Piepenbrock, J., Urban, J.: The Isabelle ENIGMA. In: ITP. LIPIcs, vol. 237, pp. 16:1\u201316:21. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022)"},{"issue":"2","key":"18_CR19","first-page":"153","volume":"3","author":"A Grabowski","year":"2010","unstructured":"Grabowski, A., Korni\u0142owicz, A., Naumowicz, A.: Mizar in a nutshell. J. Formalized Reasoning 3(2), 153\u2013245 (2010)","journal-title":"J. Formalized Reasoning"},{"key":"18_CR20","unstructured":"H\u00e4hnle, R., Kerber, M., Weidenbach, C.: Common syntax of the DFGSchwerpunktprogramm deduction. Technical report TR 10\/96, Fakult\u00e4t f\u00fcr Informatik, Universit\u00e4t Karlsruhe, Karlsruhe (1996)"},{"key":"18_CR21","unstructured":"Holden, E.K., Korovin, K.: Graph sequence learning for premise selection. CoRR, abs\/2303.15642 (2023)"},{"key":"18_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/978-3-031-16681-5_18","volume-title":"Intelligent Computer Mathematics","author":"J H\u016fla","year":"2022","unstructured":"H\u016fla, J., Jakub\u016fv, J., Janota, M., Kubej, L.: Targeted configuration of an SMT solver. In: Buzzard, K., Kutsia, T. (eds.) CICM 2022. LNCS, vol. 13467, pp. 256\u2013271. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-16681-5_18"},{"key":"18_CR23","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1613\/jair.2861","volume":"36","author":"F Hutter","year":"2009","unstructured":"Hutter, F., Hoos, H.H., Leyton-Brown, K., St\u00fctzle, T.: ParamILS: an automatic algorithm configuration framework. J. Artif. Intell. Res. 36, 267\u2013306 (2009)","journal-title":"J. Artif. Intell. Res."},{"key":"18_CR24","unstructured":"Jakub\u016fv, J., et al.: MizAR 60 for Mizar 50. In: ITP. LIPIcs, vol. 268, pp. 19:1\u201319:22. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2023)"},{"key":"18_CR25","doi-asserted-by":"crossref","unstructured":"Jakub\u016fv, J., Suda, M., Urban, J.: Automated invention of strategies and term orderings for vampire. In: GCAI. EPiC Series in Computing, vol. 50, pp. 121\u2013133. EasyChair (2017)","DOI":"10.29007\/xghj"},{"key":"18_CR26","doi-asserted-by":"crossref","unstructured":"Jakub\u016fv, J., Urban, J.: BliStrTune: hierarchical invention of theorem proving strategies. In: Bertot, Y., Vafeiadis, V. (eds.) Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, 16\u201317 January 2017, pp. 43\u201352. ACM (2017)","DOI":"10.1145\/3018610.3018619"},{"key":"18_CR27","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/978-3-319-62075-6_20","volume-title":"Intelligent Computer Mathematics","author":"J Jakub\u016fv","year":"2017","unstructured":"Jakub\u016fv, J., Urban, J.: ENIGMA: efficient learning-based inference guiding machine. In: Geuvers, H., England, M., Hasan, O., Rabe, F., Teschke, O. (eds.) CICM 2017. LNCS (LNAI), vol. 10383, pp. 292\u2013302. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-62075-6_20"},{"key":"18_CR28","unstructured":"Jakub\u016fv, J., Urban, J.: Hammering Mizar by learning clause guidance. In: Harrison, J., O\u2019Leary, J., Tolmach, A. (eds.) 10th International Conference on Interactive Theorem Proving, ITP 2019, 9\u201312 September 2019, Portland, OR, USA. LIPIcs, vol. 141, pp. 34:1\u201334:8. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2019)"},{"key":"18_CR29","unstructured":"Janota, M., Barbosa, H., Fontaine, P., Reynolds, A.: Fair and adventurous enumeration of quantifier instantiations. In: Formal Methods in Computer-Aided Design (2021)"},{"issue":"3","key":"18_CR30","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/s10817-015-9330-8","volume":"55","author":"C Kaliszyk","year":"2015","unstructured":"Kaliszyk, C., Urban, J.: MizAR 40 for Mizar 40. J. Autom. Reasoning 55(3), 245\u2013256 (2015)","journal-title":"J. Autom. Reasoning"},{"key":"18_CR31","unstructured":"Ke, G., et al.: LightGBM: a highly efficient gradient boosting decision tree. In: NIPS, pp. 3146\u20133154 (2017)"},{"key":"18_CR32","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":"18_CR33","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":"18_CR34","unstructured":"Lindauer, M., et al.: SMAC3: a versatile bayesian optimization package for hyperparameter optimization (2021)"},{"key":"18_CR35","first-page":"3","volume":"4","author":"R Matuszewski","year":"2005","unstructured":"Matuszewski, R., Rudnicki, P.: Mizar: the first 30 years. Mech. Math. Appl. 4, 3\u201324 (2005)","journal-title":"Mech. Math. Appl."},{"key":"18_CR36","doi-asserted-by":"crossref","unstructured":"Moskal, M., Lopuszanski, J., Kiniry, J.R.: E-matching for fun and profit. In: Krstic, S., Oliveras, A. (eds.) Proceedings of the 5th International Workshop on Satisfiability Modulo Theories, SMT@CAV 2007. Electronic Notes in Theoretical Computer Science, Berlin, Germany, 1\u20132 July 2007, vol. 198, pp. 19\u201335. Elsevier (2007)","DOI":"10.1016\/j.entcs.2008.04.078"},{"key":"18_CR37","unstructured":"Niemetz, A., Preiner, M.: Bitwuzla at the SMT-COMP 2020. CoRR, abs\/2006.01621 (2020)"},{"key":"18_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/978-3-319-96142-2_16","volume-title":"Computer Aided Verification","author":"A Niemetz","year":"2018","unstructured":"Niemetz, A., Preiner, M., Reynolds, A., Barrett, C., Tinelli, C.: Solving quantified bit-vectors using invertibility conditions. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 236\u2013255. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96142-2_16"},{"key":"18_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/978-3-030-72013-1_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Niemetz","year":"2021","unstructured":"Niemetz, A., Preiner, M., Reynolds, A., Barrett, C., Tinelli, C.: Syntax-guided quantifier instantiation. In: TACAS 2021. LNCS, vol. 12652, pp. 145\u2013163. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_8"},{"key":"18_CR40","unstructured":"Ols\u00e1k, M., Kaliszyk, C., Urban, J.: Property invariant embedding for automated reasoning. In: De Giacomo, G., et al. (eds.) ECAI 2020 - 24th European Conference on Artificial Intelligence. Frontiers in Artificial Intelligence and Applications, vol. 325, pp. 1395\u20131402. IOS Press (2020)"},{"key":"18_CR41","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/978-3-030-29007-8_3","volume-title":"Frontiers of Combining Systems","author":"M Rawson","year":"2019","unstructured":"Rawson, M., Reger, G.: A neurally-guided, parallel theorem prover. In: Herzig, A., Popescu, A. (eds.) FroCoS 2019. LNCS (LNAI), vol. 11715, pp. 40\u201356. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29007-8_3"},{"key":"18_CR42","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-030-86059-2_11","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"M Rawson","year":"2021","unstructured":"Rawson, M., Reger, G.: lazyCoP: lazy paramodulation meets neurally guided search. In: Das, A., Negri, S. (eds.) TABLEAUX 2021. LNCS (LNAI), vol. 12842, pp. 187\u2013199. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-86059-2_11"},{"key":"18_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-319-89963-3_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Reynolds","year":"2018","unstructured":"Reynolds, A., Barbosa, H., Fontaine, P.: Revisiting enumerative instantiation. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 112\u2013131. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_7"},{"issue":"3","key":"18_CR44","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/s10703-017-0290-y","volume":"51","author":"A Reynolds","year":"2017","unstructured":"Reynolds, A., King, T., Kuncak, V.: Solving quantified linear arithmetic by counterexample-guided instantiation. Formal Methods Syst. Des. 51(3), 500\u2013532 (2017)","journal-title":"Formal Methods Syst. Des."},{"key":"18_CR45","doi-asserted-by":"crossref","unstructured":"Reynolds, A., Tinelli, C., de\u00a0Moura, L.M.: Finding conflicting instances of quantified formulas in SMT. In: Formal Methods in Computer-Aided Design, FMCAD, pp. 195\u2013202. IEEE (2014)","DOI":"10.1109\/FMCAD.2014.6987613"},{"key":"18_CR46","unstructured":"Robinson, J.A., Voronkov, (eds.): Handbook of Automated Reasoning (in 2 Volumes). Elsevier and MIT Press (2001)"},{"key":"18_CR47","unstructured":"Janota, M., Piepenbrock, J., Piotrowski, B.: Towards learning quantifier instantiation in SMT. In: Meel, K.S., Strichman, O. (eds.) 25th International Conference on Theory and Applications of Satisfiability Testing, SAT 2022, 2\u20135 August 2022, Haifa, Israel. LIPIcs, vol. 236, pp. 7:1\u20137:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022)"},{"key":"18_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"735","DOI":"10.1007\/978-3-642-45221-5_49","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"S Schulz","year":"2013","unstructured":"Schulz, S.: System description: E\u00a01.8. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 735\u2013743. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-45221-5_49"},{"key":"18_CR49","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1007\/978-3-030-79876-5_31","volume-title":"Automated Deduction \u2013 CADE 28","author":"M Suda","year":"2021","unstructured":"Suda, M.: Improving ENIGMA-style clause selection while learning from history. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 543\u2013561. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_31"},{"key":"18_CR50","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1007\/978-3-030-86205-3_11","volume-title":"Frontiers of Combining Systems","author":"M Suda","year":"2021","unstructured":"Suda, M.: Vampire with a brain is a good ITP hammer. In: Konev, B., Reger, G. (eds.) FroCoS 2021. LNCS (LNAI), vol. 12941, pp. 192\u2013209. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-86205-3_11"},{"key":"18_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/3-540-58156-1_18","volume-title":"Automated Deduction \u2014 CADE-12","author":"G Sutcliffe","year":"1994","unstructured":"Sutcliffe, G., Suttner, C., Yemenis, T.: The TPTP problem library. In: Bundy, A. (ed.) CADE 1994. LNCS, vol. 814, pp. 252\u2013266. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-58156-1_18"},{"issue":"3\u20134","key":"18_CR52","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/s10817-004-6245-1","volume":"33","author":"J Urban","year":"2004","unstructured":"Urban, J.: MPTP - motivation, implementation, first experiments. J. Autom. Reasoning 33(3\u20134), 319\u2013339 (2004)","journal-title":"J. Autom. Reasoning"},{"issue":"1\u20132","key":"18_CR53","first-page":"21","volume":"37","author":"J Urban","year":"2006","unstructured":"Urban, J.: MPTP 0.2: design, implementation, and initial experiments. J. Autom. Reasoning 37(1\u20132), 21\u201343 (2006)","journal-title":"J. Autom. Reasoning"},{"key":"18_CR54","doi-asserted-by":"crossref","unstructured":"Urban, J.: BliStr: the blind strategymaker. In: Gottlob, G., Sutcliffe, G., Voronkov, A. (eds.) Global Conference on Artificial Intelligence, GCAI 2015. EPiC Series in Computing, Tbilisi, Georgia, 16\u201319 October 2015, vol. 36, pp. 312\u2013319. EasyChair (2015)","DOI":"10.29007\/8n7m"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-66997-2_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T06:05:48Z","timestamp":1748412348000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-66997-2_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031669965","9783031669972"],"references-count":54,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-66997-2_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"29 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CICM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Intelligent Computer Mathematics","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Montreal, QC","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","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":"5 August 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 August 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"mkm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/cicm-conference.org\/2024\/cicm.php","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}