{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T14:40:26Z","timestamp":1777560026034,"version":"3.51.4"},"reference-count":49,"publisher":"SAGE Publications","issue":"2","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["AIC"],"published-print":{"date-parts":[[2023,5,11]]},"abstract":"<jats:p>The CADE ATP System Competition (CASC) is the annual evaluation of fully automatic, classical logic, Automated Theorem Proving (ATP) systems. CASC-J11 was the twenty-seventh competition in the CASC series. Twenty-four ATP systems 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-220244","type":"journal-article","created":{"date-parts":[[2023,3,31]],"date-time":"2023-03-31T11:36:50Z","timestamp":1680262610000},"page":"73-91","source":"Crossref","is-referenced-by-count":8,"title":["The 11th IJCAR automated theorem proving system competition\u00a0\u2013 CASC-J11"],"prefix":"10.1177","volume":"36","author":[{"given":"Geoff","family":"Sutcliffe","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Miami, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Desharnais","sequence":"additional","affiliation":[{"name":"Automation of Logic, Max Planck Institute for Informatics, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"179","reference":[{"key":"10.3233\/AIC-220244_ref2","doi-asserted-by":"crossref","unstructured":"P.\u00a0Baumgartner, J.\u00a0Bax and U.\u00a0Waldmann, Beagle\u00a0\u2013 A hierarchic superposition theorem prover, in: Proceedings of the 25th International Conference on Automated Deduction, A.\u00a0Felty and A.\u00a0Middeldorp, eds, Lecture Notes in Computer Science, Springer-Verlag, 2015, pp.\u00a0285\u2013294.","DOI":"10.1007\/978-3-319-21401-6_25"},{"key":"10.3233\/AIC-220244_ref3","doi-asserted-by":"crossref","unstructured":"A.\u00a0Bentkamp, J.\u00a0Blanchette, S.\u00a0Tourret and P.\u00a0Vukmirovi\u0107, Superposition for full higher-order logic, in: Proceedings of the 28th International Conference on Automated Deduction, A.\u00a0Platzer and G.\u00a0Sutcliffe, eds, Lecture Notes in Computer Science, Springer-Verlag, 2021, pp.\u00a0396\u2013412.","DOI":"10.1007\/978-3-030-79876-5_23"},{"issue":"7","key":"10.3233\/AIC-220244_ref4","doi-asserted-by":"publisher","first-page":"893","DOI":"10.1007\/s10817-021-09595-y","article-title":"Superposition with lambdas","volume":"65","author":"Bentkamp","year":"2021","journal-title":"Journal of Automated Reasoning"},{"key":"10.3233\/AIC-220244_ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_11"},{"key":"10.3233\/AIC-220244_ref6","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, Springer-Verlag, 2019, pp.\u00a0123\u2013141.","DOI":"10.1007\/978-3-030-29436-6_8"},{"key":"10.3233\/AIC-220244_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-10769-6_21"},{"key":"10.3233\/AIC-220244_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31365-3_11"},{"key":"10.3233\/AIC-220244_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-10769-6_22"},{"key":"10.3233\/AIC-220244_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94205-6_26"},{"key":"10.3233\/AIC-220244_ref11","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-220244_ref13","doi-asserted-by":"crossref","unstructured":"L.\u00a0de\u00a0Moura and N.\u00a0Bj\u00f8rner, Z3: An efficient SMT solver, in: Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, C.\u00a0Ramakrishnan and J.\u00a0Rehof, eds, Lecture Notes in Artificial Intelligence, Springer-Verlag, 2008, pp.\u00a0337\u2013340.","DOI":"10.1007\/978-3-540-78800-3_24"},{"issue":"7","key":"10.3233\/AIC-220244_ref14","doi-asserted-by":"publisher","first-page":"1165","DOI":"10.1109\/TCAD.2008.923410","article-title":"A survey of automated techniques for formal software verification","volume":"27","author":"D\u2019Silva","year":"2008","journal-title":"IEEE Transactions on Computer-aided Design of Integrated Circuits and Systems"},{"key":"10.3233\/AIC-220244_ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51054-1_24"},{"key":"10.3233\/AIC-220244_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-86059-2_12"},{"key":"10.3233\/AIC-220244_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-10769-6_11"},{"key":"10.3233\/AIC-220244_ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"10.3233\/AIC-220244_ref19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08434-3_7"},{"key":"10.3233\/AIC-220244_ref20","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1016\/j.jalgebra.2004.07.002","article-title":"Generalized MV-algebras","volume":"283","author":"Galatos","year":"2005","journal-title":"Journal of Algebra"},{"key":"10.3233\/AIC-220244_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51074-9_23"},{"key":"10.3233\/AIC-220244_ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94205-6_43"},{"key":"10.3233\/AIC-220244_ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81097-9_8"},{"key":"10.3233\/AIC-220244_ref24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39320-4_8"},{"key":"10.3233\/AIC-220244_ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71070-7_24"},{"key":"10.3233\/AIC-220244_ref26","doi-asserted-by":"crossref","unstructured":"K.\u00a0Korovin, Inst-Gen\u00a0\u2013 A modular approach to instantiation-based automated reasoning, in: Programming Logics, Essays in Memory of Harald Ganzinger, A.\u00a0Voronkov and C.\u00a0Weidenbach, eds, Lecture Notes in Computer Science, Springer-Verlag, 2013, pp.\u00a0239\u2013270.","DOI":"10.1007\/978-3-642-37651-1_10"},{"key":"10.3233\/AIC-220244_ref27","doi-asserted-by":"crossref","unstructured":"L.\u00a0Kovacs and A.\u00a0Voronkov, First-order theorem proving and vampire, in: Proceedings of the 25th International Conference on Computer Aided Verification, N.\u00a0Sharygina and H.\u00a0Veith, eds, Lecture Notes in Artificial Intelligence, Springer-Verlag, 2013, pp.\u00a01\u201335.","DOI":"10.1007\/978-3-642-39799-8_1"},{"issue":"4","key":"10.3233\/AIC-220244_ref28","doi-asserted-by":"publisher","first-page":"540","DOI":"10.1016\/j.jlamp.2015.11.008","article-title":"Relational lattices: From databases to universal algebra","volume":"85","author":"Litak","year":"2016","journal-title":"Journal of Logical and Algebraic Methods in Programming"},{"key":"10.3233\/AIC-220244_ref29","doi-asserted-by":"crossref","unstructured":"L.\u00a0Paulson and J.\u00a0Blanchette, Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers, in: Proceedings of the 8th International Workshop on the Implementation of Logics, G.\u00a0Sutcliffe, E.\u00a0Ternovska and S.\u00a0Schulz, eds, EPiC Series in Computing, EasyChair Publications, 2010, pp.\u00a01\u201311.","DOI":"10.29007\/36dt"},{"key":"10.3233\/AIC-220244_ref30","unstructured":"V.\u00a0Prevosto and U.\u00a0Waldmann, SPASS+T, in: Proceedings of the FLoC\u201906 Workshop on Empirically Successful Computerized Reasoning, 3rd International Joint Conference on Automated Reasoning, G.\u00a0Sutcliffe, R.\u00a0Schmidt and S.\u00a0Schulz, eds, CEUR Workshop Proceedings, 2006, pp.\u00a019\u201333."},{"key":"10.3233\/AIC-220244_ref31","doi-asserted-by":"crossref","unstructured":"G.\u00a0Reger, J.\u00a0Schoisswohl and A.\u00a0Voronkov, Making theory reasoning simpler, in: Proceedings of the 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, J.\u00a0Groote and K.\u00a0Larsen, eds, Lecture Notes in Computer Science, Springer-Verlag, 2021, pp.\u00a0164\u2013180.","DOI":"10.1007\/978-3-030-72013-1_9"},{"key":"10.3233\/AIC-220244_ref32","doi-asserted-by":"crossref","unstructured":"G.\u00a0Reger, M.\u00a0Suda and A.\u00a0Voronkov, Playing with AVATAR, in: Proceedings of the 25th International Conference on Automated Deduction, A.\u00a0Felty and A.\u00a0Middeldorp, eds, Lecture Notes in Computer Science, Springer-Verlag, 2015, pp.\u00a0399\u2013415.","DOI":"10.1007\/978-3-319-21401-6_28"},{"key":"10.3233\/AIC-220244_ref33","unstructured":"A.\u00a0Robinson and A.\u00a0Voronkov, Handbook of Automated Reasoning, Elsevier Science, 2001."},{"issue":"4","key":"10.3233\/AIC-220244_ref34","doi-asserted-by":"publisher","first-page":"139","DOI":"10.3233\/SAT190083","article-title":"Controlling a solver execution with the runsolver tool","volume":"7","author":"Roussel","year":"2011","journal-title":"Journal of Satisfiability, Boolean Modeling and Computation"},{"key":"10.3233\/AIC-220244_ref35","doi-asserted-by":"crossref","unstructured":"P.\u00a0R\u00fcmmer, A constraint sequent calculus for first-order logic with linear integer arithmetic, in: Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, I.\u00a0Cervesato, H.\u00a0Veith and A.\u00a0Voronkov, eds, Lecture Notes in Artificial Intelligence, Springer-Verlag, 2008, pp.\u00a0274\u2013289.","DOI":"10.1007\/978-3-540-89439-1_20"},{"key":"10.3233\/AIC-220244_ref36","unstructured":"S.\u00a0Schulz, Empirical properties of term orderings for superposition, in: Proceedings of the 8th Workshop on Practical Aspects of Automated Reasoning, B.\u00a0Konev, C.\u00a0Schon and A.\u00a0Steen, eds, CEUR Workshop Proceedings, 2022, Online."},{"key":"10.3233\/AIC-220244_ref37","doi-asserted-by":"crossref","unstructured":"S.\u00a0Schulz, S.\u00a0Cruanes and P.\u00a0Vukmirovi\u0107, Faster, higher, stronger: E 2.3, in: Proceedings of the 27th International Conference on Automated Deduction, P.\u00a0Fontaine, ed., Lecture Notes in Computer Science, Springer-Verlag, 2019, pp.\u00a0495\u2013507.","DOI":"10.1007\/978-3-030-29436-6_29"},{"key":"10.3233\/AIC-220244_ref38","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, Springer-Verlag, 2017, pp.\u00a0310\u2013325.","DOI":"10.1007\/978-3-319-63046-5_19"},{"key":"10.3233\/AIC-220244_ref39","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08587-6_28"},{"issue":"3","key":"10.3233\/AIC-220244_ref41","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":"2","key":"10.3233\/AIC-220244_ref42","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":"4","key":"10.3233\/AIC-220244_ref43","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/s10817-017-9407-7","article-title":"The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0","volume":"59","author":"Sutcliffe","year":"2017","journal-title":"Journal of Automated Reasoning"},{"key":"10.3233\/AIC-220244_ref46","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/jzac068"},{"issue":"4","key":"10.3233\/AIC-220244_ref47","doi-asserted-by":"publisher","first-page":"259","DOI":"10.3233\/AIC-210235","article-title":"The CADE-28 automated theorem proving system competition\u00a0\u2013 CASC-28","volume":"34","author":"Sutcliffe","year":"2022","journal-title":"AI Communications"},{"issue":"1\u20132","key":"10.3233\/AIC-220244_ref48","doi-asserted-by":"crossref","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"},{"issue":"2","key":"10.3233\/AIC-220244_ref49","first-page":"231","article-title":"ATP-based cross verification of Mizar proofs: Method, systems, and first experiments","volume":"2","author":"Urban","year":"2009","journal-title":"Journal of Mathematics in Computer Science"},{"key":"10.3233\/AIC-220244_ref50","doi-asserted-by":"crossref","unstructured":"P.\u00a0Vukmirovi\u0107, A.\u00a0Bentkamp, J.\u00a0Blanchette, S.\u00a0Cruanes, V.\u00a0Nummelin and S.\u00a0Tourret, Making higher-order superposition work, in: Proceedings of the 28th International Conference on Automated Deduction, A.\u00a0Platzer and G.\u00a0Sutcliffe, eds, Lecture Notes in Computer Science, Springer-Verlag, 2021, pp.\u00a0415\u2013432.","DOI":"10.1007\/978-3-030-79876-5_24"},{"key":"10.3233\/AIC-220244_ref51","unstructured":"P.\u00a0Vukmirovi\u0107, 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, Dagstuhl Publishing, 2020, pp.\u00a05:1\u20135:20."},{"key":"10.3233\/AIC-220244_ref52","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/s10009-021-00639-7","article-title":"Extending a brainiac prover to lambda-free higher-order logic","volume":"24","author":"Vukmirovi\u0107","year":"2021","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"10.3233\/AIC-220244_ref53","unstructured":"P.\u00a0Vukmirovi\u0107 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, 2020, pp.\u00a0148\u2013166."},{"issue":"2","key":"10.3233\/AIC-220244_ref54","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1145\/322307.322308","article-title":"Generation and verification of finite models and counterexamples using an automated theorem prover answering two open questions","volume":"29","author":"Winker","year":"1982","journal-title":"Journal of the ACM"}],"container-title":["AI Communications"],"original-title":[],"link":[{"URL":"https:\/\/content.iospress.com\/download?id=10.3233\/AIC-220244","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T18:28:08Z","timestamp":1777400888000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/full\/10.3233\/AIC-220244"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,5,11]]},"references-count":49,"journal-issue":{"issue":"2"},"URL":"https:\/\/doi.org\/10.3233\/aic-220244","relation":{},"ISSN":["1875-8452","0921-7126"],"issn-type":[{"value":"1875-8452","type":"electronic"},{"value":"0921-7126","type":"print"}],"subject":[],"published":{"date-parts":[[2023,5,11]]}}}