{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,4]],"date-time":"2026-04-04T01:46:35Z","timestamp":1775267195363,"version":"3.50.1"},"reference-count":22,"publisher":"SAGE Publications","issue":"6","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["AIC"],"published-print":{"date-parts":[[2018,12,21]]},"DOI":"10.3233\/aic-180773","type":"journal-article","created":{"date-parts":[[2018,11,9]],"date-time":"2018-11-09T14:44:30Z","timestamp":1541774670000},"page":"495-507","source":"Crossref","is-referenced-by-count":14,"title":["The 9th IJCAR Automated Theorem Proving System Competition\u00a0\u2013 CASC-J9"],"prefix":"10.1177","volume":"31","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":"1","key":"10.3233\/AIC-180773_ref1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0747-7171(88)80018-X","article-title":"Critical pair criteria for completion","volume":"6","author":"Bachmair","year":"1988","journal-title":"Journal of Symbolic Computation"},{"key":"10.3233\/AIC-180773_ref2","doi-asserted-by":"crossref","unstructured":"J.\u00a0Blanchette, P.\u00a0Fontaine, S.\u00a0Schulz and U.\u00a0Waldmann, Towards strong higher-order automation for fast interactive verification, in: Proceedings of the 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements, G.\u00a0Reger and D.\u00a0Trayfel, eds, EPiC Series in Computing, Vol.\u00a051, EasyChair Publications, 2017, pp.\u00a016\u201323.","DOI":"10.29007\/3ngx"},{"key":"10.3233\/AIC-180773_ref3","doi-asserted-by":"crossref","unstructured":"K.\u00a0Claessen and N.\u00a0Smallbone, Efficient encodings of first-order Horn formulas in equational logic, in: Proceedings of the 9th International Joint Conference on Automated Reasoning, D.\u00a0Galmiche, S.\u00a0Schulz and R.\u00a0Sebastiani, eds, Lecture Notes in Computer Science, Vol.\u00a010900, 2018, pp.\u00a0388\u2013404.","DOI":"10.1007\/978-3-319-94205-6_26"},{"key":"10.3233\/AIC-180773_ref4","doi-asserted-by":"crossref","unstructured":"K.\u00a0Hoder, G.\u00a0Reger, M.\u00a0Suda and A.\u00a0Voronkov, Selecting the selection, in: Proceedings of the 8th International Joint Conference on Automated Reasoning, N.\u00a0Olivetti and A.\u00a0Tiwari, eds, Lecture Notes in Artificial Intelligence, Vol.\u00a09706, 2016, pp.\u00a0313\u2013329.","DOI":"10.1007\/978-3-319-40229-1_22"},{"key":"10.3233\/AIC-180773_ref5","doi-asserted-by":"crossref","unstructured":"B.\u00a0Kiesl, M.\u00a0Suda, M.\u00a0Seidl, H.\u00a0Tompits and A.\u00a0Biere, Blocked clauses in first-order logic, in: Proceedings of the 21st International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, T.\u00a0Eiter and D.\u00a0Sands, eds, EPiC Series in Computing, Vol.\u00a046, EasyChair Publications, 2017, pp.\u00a031\u201348.","DOI":"10.29007\/c3wq"},{"key":"10.3233\/AIC-180773_ref6","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"10.3233\/AIC-180773_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-52885-7_100"},{"key":"10.3233\/AIC-180773_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22119-4_18"},{"key":"10.3233\/AIC-180773_ref9","doi-asserted-by":"crossref","unstructured":"J.\u00a0Otten, nanoCoP: A non-clausal connection prover, 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, 2016, pp.\u00a0302\u2013312.","DOI":"10.1007\/978-3-319-40229-1_21"},{"key":"10.3233\/AIC-180773_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66902-1_13"},{"key":"10.3233\/AIC-180773_ref11","unstructured":"J.\u00a0Otten, Proof search optimizations for non-clausal connection calculi, in: Proceedings of the 6th Workshop on Practical Aspects of Automated Reasoning, B.\u00a0Konev, P.\u00a0R\u00fcmmer and J.\u00a0Urban, eds, CEUR Workshop Proceedings, Vol.\u00a02162, 2018, pp.\u00a049\u201357."},{"key":"10.3233\/AIC-180773_ref12","doi-asserted-by":"crossref","unstructured":"G.\u00a0Reger and M.\u00a0Suda, Set of support for theory reasoning, in: Proceedings of the IWIL Workshop and LPAR Short Presentations, T.\u00a0Eiter, D.\u00a0Sands, G.\u00a0Sutcliffe and A.\u00a0Voronkov, eds, Kalpa Publications in Computing, Vol.\u00a01, 2017, pp.\u00a0124\u2013134.","DOI":"10.29007\/ndjg"},{"key":"10.3233\/AIC-180773_ref13","doi-asserted-by":"crossref","unstructured":"G.\u00a0Reger, M.\u00a0Suda and A.\u00a0Voronkov, Unification with abstraction and theory instantiation in saturation-based reasoning, in: Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, D.\u00a0Beyer and M.\u00a0Huisman, eds, Lecture Notes in Computer Science, Vol.\u00a010805, Springer-Verlag, 2018, pp.\u00a03\u201322.","DOI":"10.1007\/978-3-319-89960-2_1"},{"key":"10.3233\/AIC-180773_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36675-8_3"},{"key":"10.3233\/AIC-180773_ref15","unstructured":"P.\u00a0Smith, An Introduction to Goedel\u2019s Theorems, Cambridge University Press, 2007."},{"key":"10.3233\/AIC-180773_ref16","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-180773_ref17","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-180773_ref18","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-180773_ref19","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-180773_ref20","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":"1\u20132","key":"10.3233\/AIC-180773_ref22","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-180773_ref23","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1016\/j.ins.2018.04.086","article-title":"Contradiction separation based dynamic multi-clause synergized automated deduction","volume":"462","author":"Xu","year":"2018","journal-title":"Information Sciences"}],"container-title":["AI Communications"],"original-title":[],"link":[{"URL":"https:\/\/api.wiley.com\/onlinelibrary\/tdm\/v1\/articles\/10.3233\/AIC-180773","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/content.iospress.com\/download?id=10.3233\/AIC-180773","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,4]],"date-time":"2026-04-04T00:50:32Z","timestamp":1775263832000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/full\/10.3233\/AIC-180773"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,12,21]]},"references-count":22,"journal-issue":{"issue":"6"},"URL":"https:\/\/doi.org\/10.3233\/aic-180773","relation":{},"ISSN":["1875-8452","0921-7126"],"issn-type":[{"value":"1875-8452","type":"electronic"},{"value":"0921-7126","type":"print"}],"subject":[],"published":{"date-parts":[[2018,12,21]]}}}