{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T07:00:38Z","timestamp":1760598038291,"version":"3.38.0"},"reference-count":32,"publisher":"SAGE Publications","issue":"2","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["AIC"],"published-print":{"date-parts":[[2021,9,10]]},"abstract":"<jats:p>The CADE ATP System Competition (CASC) is the annual evaluation of fully automatic, classical logic Automated Theorem Proving (ATP) systems. CASC-J10 was the twenty-fifth competition in the CASC series. Twenty-four ATP systems and system variants competed in the various competition divisions. This paper presents an outline of the competition design, and a commentated summary of the results.<\/jats:p>","DOI":"10.3233\/aic-201566","type":"journal-article","created":{"date-parts":[[2021,3,19]],"date-time":"2021-03-19T17:12:54Z","timestamp":1616173974000},"page":"163-177","source":"Crossref","is-referenced-by-count":8,"title":["The 10th IJCAR automated theorem proving system competition\u00a0\u2013 CASC-J10"],"prefix":"10.1177","volume":"34","author":[{"given":"Geoff","family":"Sutcliffe","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Miami, USA. E-mail:\u00a0geoff@cs.miami.edu"}]}],"member":"179","reference":[{"issue":"2","key":"10.3233\/AIC-201566_ref1","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s10817-013-9286-5","article-title":"Premise selection for mathematics by corpus analysis and kernel methods","volume":"52","author":"Alama","year":"2014","journal-title":"Journal of Automated Reasoning"},{"key":"10.3233\/AIC-201566_ref2","doi-asserted-by":"crossref","unstructured":"A.\u00a0Bentkamp, J.\u00a0Blanchette, P.\u00a0Vukmirovic and U.\u00a0Waldmann, Superposition with lambdas, in: Proceedings of the 27th International Conference on Automated Deduction, P.\u00a0Fontaine, ed., Lecture Notes in Computer Science, Vol.\u00a011716, Springer-Verlag, 2019, pp.\u00a055\u201373.","DOI":"10.1007\/978-3-030-29436-6_4"},{"key":"10.3233\/AIC-201566_ref3","doi-asserted-by":"crossref","unstructured":"A.\u00a0Bhayat and G.\u00a0Reger, A combinator-based superposition calculus for higher-order logic, in: Proceedings of the 10th International Joint Conference on Automated Reasoning, N.\u00a0Peltier and V.\u00a0Sofronie-Stokkermans, eds, Lecture Notes in Artificial Intelligence, Vol.\u00a012166, 2020, pp.\u00a0278\u2013296.","DOI":"10.1007\/978-3-030-51074-9_16"},{"key":"10.3233\/AIC-201566_ref4","doi-asserted-by":"crossref","unstructured":"A.\u00a0Bhayat and G.\u00a0Reger, A Knuth-bendix-like ordering for orienting combinator equations, in: Proceedings of the 10th International Joint Conference on Automated Reasoning, N.\u00a0Peltier and V.\u00a0Sofronie-Stokkermans, eds, Lecture Notes in Artificial Intelligence, Vol.\u00a012166, 2020, pp.\u00a0259\u2013277.","DOI":"10.1007\/978-3-030-51074-9_15"},{"issue":"1","key":"10.3233\/AIC-201566_ref5","first-page":"101","article-title":"Hammering towards QED","volume":"9","author":"Blanchette","year":"2016","journal-title":"Journal of Formalized Reasoning"},{"key":"10.3233\/AIC-201566_ref6","unstructured":"J.U.\u00a0BliStr, The blind strategymaker, in: Proceedings of the 1st Global Conference on Artificial Intelligence, S.\u00a0Autexier, ed., EPiC Series in Computing, Vol.\u00a036, EasyChair Publications, 2015, pp.\u00a0312\u2013319."},{"key":"10.3233\/AIC-201566_ref7","doi-asserted-by":"crossref","unstructured":"C.\u00a0Brown, T.\u00a0Gauthier, C.\u00a0Kaliszyk, G.\u00a0Sutcliffe and J.\u00a0Urban, GRUNGE: A grand unified ATP challenge, in: Proceedings of the 27th International Conference on Automated Deduction, P.\u00a0Fontaine, ed., Lecture Notes in Computer Science, Vol.\u00a011716, Springer-Verlag, 2019, pp.\u00a0123\u2013141.","DOI":"10.1007\/978-3-030-29436-6_8"},{"key":"10.3233\/AIC-201566_ref8","doi-asserted-by":"crossref","unstructured":"K.\u00a0Chvalovsky, J.\u00a0Jakubuv, M.\u00a0Suda and J.\u00a0Urban, ENIGMA-NG: Efficient neural and gradient-boosted inference guidance for E, in: Proceedings of the 27th International Conference on Automated Deduction, P.\u00a0Fontaine, ed., Lecture Notes in Computer Science, Vol.\u00a011716, Springer-Verlag, 2019, pp.\u00a0197\u2013215.","DOI":"10.1007\/978-3-030-29436-6_12"},{"key":"10.3233\/AIC-201566_ref9","unstructured":"K.\u00a0Claessen and N.\u00a0S\u00f6rensson, New techniques that improve MACE-style finite model finding, in: Proceedings of the CADE-19 Workshop: Model Computation\u00a0\u2013 Principles, Algorithms, Applications, P.\u00a0Baumgartner and C.\u00a0Fermueller, eds, 2003."},{"key":"10.3233\/AIC-201566_ref10","unstructured":"B.\u00a0Gleiss and M.\u00a0Suda, Layered clause selection for saturation-based theorem proving, in: Proceedings of the 7th Workshop on Practical Aspects of Automated Reasoning, P.\u00a0Fontaine, P.\u00a0R\u00fcmmer and S.\u00a0Tourret, eds, CEUR Workshop Proceedings, Vol.\u00a02752, 2020, pp.\u00a034\u201352."},{"key":"10.3233\/AIC-201566_ref11","doi-asserted-by":"crossref","unstructured":"L.\u00a0Gleiss, B.\u00a0Kovacs and J.\u00a0Rath, Subsumption demodulation in first-order theorem proving, in: Proceedings of the 10th International Joint Conference on Automated Reasoning, N.\u00a0Peltier and V.\u00a0Sofronie-Stokkermans, eds, Lecture Notes in Computer Science, Vol.\u00a012166, 2020, pp.\u00a0297\u2013315.","DOI":"10.1007\/978-3-030-51074-9_17"},{"key":"10.3233\/AIC-201566_ref12","doi-asserted-by":"crossref","unstructured":"J.\u00a0Jakubuv, K.\u00a0Chvalovsk\u00fd, M.\u00a0Ols\u00e1k, B.\u00a0Piotrowski, M.\u00a0Suda and J.\u00a0Urban, ENIGMA anonymous: Symbol-independent inference guiding machine (system description), in: Proceedings of the 10th International Joint Conference on Automated Reasoning, N.\u00a0Peltier and V.\u00a0Sofronie-Stokkermans, eds, Lecture Notes in Artificial Intelligence, Vol.\u00a012167, 2020, pp.\u00a0448\u2013463.","DOI":"10.1007\/978-3-030-51054-1_29"},{"issue":"3","key":"10.3233\/AIC-201566_ref13","doi-asserted-by":"publisher","first-page":"237","DOI":"10.3233\/AIC-180761","article-title":"Hierarchical invention of theorem proving strategies","volume":"31","author":"Jakubuv","year":"2018","journal-title":"AI Communications"},{"key":"10.3233\/AIC-201566_ref14","unstructured":"J.\u00a0Jakubuv and J.\u00a0Urban, Hammering mizar by learning clause guidance, in: Proceedings of the 10th International Conference on Interactive Theorem Proving, Leibniz International Proceedings in Informatics, Dagstuhl Publishing, 2019."},{"key":"10.3233\/AIC-201566_ref15","unstructured":"C.\u00a0Kaliszyk, J.\u00a0Urban and J.\u00a0Vyskocil, Machine learner for automated reasoning 0.4 and 0.5, in: Proceedings of the 4th Workshop on Practical Aspects of Automated Reasoning, S.\u00a0Schulz, L.\u00a0de\u00a0Moura and B.\u00a0Konev, eds, EPiC Series in Computing, Vol.\u00a031, EasyChair Publications, 2015, pp.\u00a060\u201366."},{"key":"10.3233\/AIC-201566_ref16","doi-asserted-by":"crossref","unstructured":"T.\u00a0Lampert and A.\u00a0Nakano, Deciding simple infinity axiom sets with one binary relation by superpostulates, in: Proceedings of the 10th International Joint Conference on Automated Reasoning, N.\u00a0Peltier and V.\u00a0Sofronie-Stokkermans, eds, Lecture Notes in Artificial Intelligence, Vol.\u00a012166, 2020, pp.\u00a0201\u2013217.","DOI":"10.1007\/978-3-030-51074-9_12"},{"key":"10.3233\/AIC-201566_ref17","doi-asserted-by":"crossref","unstructured":"D.L.\u00a0Li and A.\u00a0Tiu, Combining ProVerif and automated theorem provers for security protocol verification, in: Proceedings of the 27th International Conference on Automated Deduction, P.\u00a0Fontaine, ed., Lecture Notes in Computer Science, Vol.\u00a011716, Springer-Verlag, 2019, pp.\u00a0354\u2013365.","DOI":"10.1007\/978-3-030-29436-6_21"},{"issue":"2\u20133","key":"10.3233\/AIC-201566_ref18","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/s10817-007-9089-7","article-title":"Connection tableaux with lazy paramodulation","volume":"40","author":"Paskevich","year":"2008","journal-title":"Journal of Automated Reasoning"},{"issue":"1\u20132","key":"10.3233\/AIC-201566_ref20","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/S0747-7171(03)00040-3","article-title":"Limited resource strategy in resolution theorem proving","volume":"36","author":"Riazanov","year":"2003","journal-title":"Journal of Symbolic Computation"},{"issue":"2\u20133","key":"10.3233\/AIC-201566_ref21","first-page":"111","article-title":"E: A brainiac theorem prover","volume":"15","author":"Schulz","year":"2002","journal-title":"AI Communications"},{"key":"10.3233\/AIC-201566_ref22","doi-asserted-by":"crossref","unstructured":"S.\u00a0Schulz, G.\u00a0Sutcliffe, J.\u00a0Urban and A.\u00a0Pease, Detecting inconsistencies in large first-order knowledge bases, in: Proceedings of the 26th International Conference on Automated Deduction, L.\u00a0de\u00a0Moura, ed., Lecture Notes in Computer Science, Vol.\u00a010395, Springer-Verlag, 2017, pp.\u00a0310\u2013325.","DOI":"10.1007\/978-3-319-63046-5_19"},{"key":"10.3233\/AIC-201566_ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_6"},{"key":"10.3233\/AIC-201566_ref24","doi-asserted-by":"crossref","unstructured":"A.\u00a0Stump, G.\u00a0Sutcliffe and C.\u00a0Tinelli, StarExec: A cross-community infrastructure for logic solving, in: Proceedings of the 7th International Joint Conference on Automated Reasoning, S.\u00a0Demri, D.\u00a0Kapur and C.\u00a0Weidenbach, eds, Lecture Notes in Artificial Intelligence, Vol.\u00a08562, 2014, pp.\u00a0367\u2013373.","DOI":"10.1007\/978-3-319-08587-6_28"},{"issue":"3","key":"10.3233\/AIC-201566_ref25","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1023\/A:1006393501098","article-title":"The CADE-16 ATP system competition","volume":"24","author":"Sutcliffe","year":"2000","journal-title":"Journal of Automated Reasoning"},{"issue":"4","key":"10.3233\/AIC-201566_ref26","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","article-title":"The TPTP problem library and associated infrastructure. The FOF and CNF parts, v3.5.0","volume":"43","author":"Sutcliffe","year":"2009","journal-title":"Journal of Automated Reasoning"},{"issue":"2","key":"10.3233\/AIC-201566_ref27","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1609\/aimag.v37i2.2620","article-title":"The CADE ATP system competition\u00a0\u2013 CASC","volume":"37","author":"Sutcliffe","year":"2016","journal-title":"AI Magazine"},{"issue":"6","key":"10.3233\/AIC-201566_ref28","doi-asserted-by":"publisher","first-page":"419","DOI":"10.3233\/AIC-170744","article-title":"The CADE-26 automated theorem proving system competition\u00a0\u2013 CASC-26","volume":"30","author":"Sutcliffe","year":"2017","journal-title":"AI Communications"},{"issue":"5\u20136","key":"10.3233\/AIC-201566_ref30","doi-asserted-by":"publisher","first-page":"373","DOI":"10.3233\/AIC-190627","article-title":"The CADE-27 automated theorem proving system competition\u00a0\u2013 CASC-27","volume":"32","author":"Sutcliffe","year":"2020","journal-title":"AI Communications"},{"key":"10.3233\/AIC-201566_ref31","unstructured":"G.\u00a0Sutcliffe and F.J.\u00a0Pelletier, Hoping for the truth\u00a0\u2013 a survey of the TPTP logics, in: Proceedings of the 29th International FLAIRS Conference, Z.\u00a0Markov and I.\u00a0Russell, eds, 2016, pp.\u00a0110\u2013115."},{"issue":"1\u20132","key":"10.3233\/AIC-201566_ref32","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1016\/S0004-3702(01)00113-8","article-title":"Evaluating general purpose automated theorem proving systems","volume":"131","author":"Sutcliffe","year":"2001","journal-title":"Artificial Intelligence"},{"key":"10.3233\/AIC-201566_ref33","unstructured":"P.\u00a0Vukmirovic, A.\u00a0Bentkamp and V.\u00a0Nummelin, Efficient full higher-order unification, in: Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction, Z.M.\u00a0Ariola, ed., Leibniz International Proceedings in Informatics, Vol.\u00a0167, Dagstuhl Publishing, 2020, pp.\u00a05:1\u20135:20."},{"key":"10.3233\/AIC-201566_ref34","unstructured":"P.\u00a0Vukmirovic and V.\u00a0Nummelin, Boolean reasoning in a higher-order superposition prover, in: Proceedings of the 7th Workshop on Practical Aspects of Automated Reasoning, P.\u00a0Fontaine, P.\u00a0R\u00fcmmer and S.\u00a0Tourret, eds, CEUR Workshop Proceedings, Vol.\u00a02752, 2020, pp.\u00a0148\u2013166."}],"container-title":["AI Communications"],"original-title":[],"link":[{"URL":"https:\/\/content.iospress.com\/download?id=10.3233\/AIC-201566","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,11]],"date-time":"2025-03-11T05:51:59Z","timestamp":1741672319000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/full\/10.3233\/AIC-201566"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,9,10]]},"references-count":32,"journal-issue":{"issue":"2"},"URL":"https:\/\/doi.org\/10.3233\/aic-201566","relation":{},"ISSN":["1875-8452","0921-7126"],"issn-type":[{"type":"electronic","value":"1875-8452"},{"type":"print","value":"0921-7126"}],"subject":[],"published":{"date-parts":[[2021,9,10]]}}}