{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,24]],"date-time":"2025-06-24T06:27:49Z","timestamp":1750746469435,"version":"3.38.0"},"reference-count":17,"publisher":"SAGE Publications","issue":"3","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["AIC"],"published-print":{"date-parts":[[2016,4,26]]},"DOI":"10.3233\/aic-150691","type":"journal-article","created":{"date-parts":[[2016,4,26]],"date-time":"2016-04-26T20:05:58Z","timestamp":1461701158000},"page":"423-433","source":"Crossref","is-referenced-by-count":5,"title":["The CADE-25 Automated Theorem Proving system competition\u00a0\u2013 CASC-25"],"prefix":"10.1177","volume":"29","author":[{"given":"Geoff","family":"Sutcliffe","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Miami, Miami, USA. E-mail:\u00a0geoff@cs.miami.edu"}]},{"given":"Josef","family":"Urban","sequence":"additional","affiliation":[{"name":"Intelligent Systems ICIS, Radboud Universiteit, Nijmegen, The Netherlands"}]}],"member":"179","reference":[{"key":"10.3233\/AIC-150691_ref1","doi-asserted-by":"crossref","unstructured":"P.\u00a0Backeman and P.\u00a0R\u00fcmmer, Efficient algorithms for bounded rigid E-unification, in: Proceedings of the 24th Conference on Automated Reasoning with Analytic Tableaux and Related Methods, H.\u00a0de\u00a0Nivelle, ed., Lecture Notes in Computer Science, Vol.\u00a09323, Springer-Verlag, 2015, pp.\u00a070\u201385.","DOI":"10.1007\/978-3-319-24312-2_6"},{"key":"10.3233\/AIC-150691_ref2","doi-asserted-by":"crossref","unstructured":"P.\u00a0Backeman and P.\u00a0R\u00fcmmer, Theorem proving with bounded rigid E-unification, in: Proceedings of the 25th International Conference on Automated Deduction, A.\u00a0Felty and A.\u00a0Middeldorp, eds, Lecture Notes in Computer Science, Vol.\u00a09195, Springer-Verlag, 2015, pp.\u00a0572\u2013587.","DOI":"10.1007\/978-3-319-21401-6_39"},{"key":"10.3233\/AIC-150691_ref3","doi-asserted-by":"crossref","unstructured":"R.\u00a0Bonichon, D.\u00a0Delahaye and D.\u00a0Doligez, Zenon: An extensible automated theorem prover producing checkable proofs, in: Proceedings of the 14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, N.\u00a0Dershowitz and A.\u00a0Voronkov, eds, Lecture Notes in Artificial Intelligence, Vol.\u00a04790, 2007, pp.\u00a0151\u2013165.","DOI":"10.1007\/978-3-540-75560-9_13"},{"key":"10.3233\/AIC-150691_ref4","doi-asserted-by":"crossref","unstructured":"G.\u00a0Bury and D.\u00a0Delahaye, Integrating simplex with tableaux, in: Proceedings of the 24th Conference on Automated Reasoning with Analytic Tableaux and Related Methods, H.\u00a0de\u00a0Nivelle, ed., Lecture Notes in Computer Science, Vol.\u00a09323, Springer-Verlag, 2015, pp.\u00a086\u2013101.","DOI":"10.1007\/978-3-319-24312-2_7"},{"key":"10.3233\/AIC-150691_ref5","doi-asserted-by":"crossref","unstructured":"L.\u00a0de\u00a0Moura and N.\u00a0Bjorner, 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, Vol.\u00a04963, Springer-Verlag, 2008, pp.\u00a0337\u2013340.","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"10.3233\/AIC-150691_ref6","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, Vol.\u00a08044, Springer-Verlag, 2013, pp.\u00a01\u201335.","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"10.3233\/AIC-150691_ref7","doi-asserted-by":"crossref","unstructured":"A.\u00a0Reynolds, M.\u00a0Deters, V.\u00a0Kuncak, C.\u00a0Barrett and C.\u00a0Tinelli, Counterexample guided quantifier instantiation for synthesis in CVC4, in: Proceedings of the 27th International Conference on Computer Aided Verification, D.\u00a0Kroening and C.\u00a0Pasareanu, eds, Lecture Notes in Computer Science, Vol.\u00a09207, Springer-Verlag, 2015, pp.\u00a0198\u2013216.","DOI":"10.1007\/978-3-319-21668-3_12"},{"key":"10.3233\/AIC-150691_ref8","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, Vol.\u00a05330, Springer-Verlag, 2008, pp.\u00a0274\u2013289.","DOI":"10.1007\/978-3-540-89439-1_20"},{"key":"10.3233\/AIC-150691_ref9","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-150691_ref10","doi-asserted-by":"crossref","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-150691_ref11","doi-asserted-by":"crossref","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"},{"key":"10.3233\/AIC-150691_ref12","doi-asserted-by":"crossref","unstructured":"G.\u00a0Sutcliffe, The TPTP World \u2013 Infrastructure for automated reasoning, in: Proceedings of the 16th International Conference on Logic for Programming Artificial Intelligence and Reasoning, E.\u00a0Clarke and A.\u00a0Voronkov, eds, Lecture Notes in Artificial Intelligence, Vol.\u00a06355, Springer-Verlag, 2010, pp.\u00a01\u201312.","DOI":"10.1007\/978-3-642-17511-4_1"},{"key":"10.3233\/AIC-150691_ref13","unstructured":"G.\u00a0Sutcliffe, in: Proceedings of the CADE-25 ATP System Competition, Berlin, Germany, 2015, http:\/\/www.tptp.org\/CASC\/25\/Proceedings.pdf."},{"issue":"4","key":"10.3233\/AIC-150691_ref14","doi-asserted-by":"crossref","first-page":"683","DOI":"10.3233\/AIC-150668","article-title":"The 7th IJCAR Automated Theorem Proving system competition \u2013 CASC-J7","volume":"28","author":"Sutcliffe","year":"2015","journal-title":"AI Communications"},{"issue":"1,2","key":"10.3233\/AIC-150691_ref15","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"},{"key":"10.3233\/AIC-150691_ref16","doi-asserted-by":"crossref","unstructured":"A.\u00a0Voronkov, AVATAR: The new architecture for first-order theorem provers, in: Proceedings of the 26th International Conference on Computer Aided Verification, A.\u00a0Biere and R.\u00a0Bloem, eds, Lecture Notes in Computer Science, Vol.\u00a08559, 2014, pp.\u00a0696\u2013710.","DOI":"10.1007\/978-3-319-08867-9_46"},{"key":"10.3233\/AIC-150691_ref17","unstructured":"M.\u00a0Wisniewski, A.\u00a0Steen and C.\u00a0Benzm\u00fcller, The Leo-III project, in: Proceedings of the Joint Automated Reasoning Workshop and Deduktionstreffen, A.\u00a0Bolotov and M.\u00a0Kerber, eds, 2014, p.\u00a038."}],"container-title":["AI Communications"],"original-title":[],"link":[{"URL":"https:\/\/content.iospress.com\/download?id=10.3233\/AIC-150691","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,11]],"date-time":"2025-03-11T07:40:46Z","timestamp":1741678846000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.medra.org\/servlet\/aliasResolver?alias=iospress&doi=10.3233\/AIC-150691"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,4,26]]},"references-count":17,"journal-issue":{"issue":"3"},"URL":"https:\/\/doi.org\/10.3233\/aic-150691","relation":{},"ISSN":["1875-8452","0921-7126"],"issn-type":[{"type":"electronic","value":"1875-8452"},{"type":"print","value":"0921-7126"}],"subject":[],"published":{"date-parts":[[2016,4,26]]}}}