{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,11]],"date-time":"2025-03-11T01:10:11Z","timestamp":1741655411144,"version":"3.38.0"},"reference-count":15,"publisher":"SAGE Publications","issue":"4","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["AIC"],"published-print":{"date-parts":[[2015,9,18]]},"DOI":"10.3233\/aic-150668","type":"journal-article","created":{"date-parts":[[2015,9,22]],"date-time":"2015-09-22T15:57:25Z","timestamp":1442937445000},"page":"683-692","source":"Crossref","is-referenced-by-count":6,"title":["The 7th IJCAR automated theorem proving system competition\u00a0\u2013 CASC-J7"],"prefix":"10.1177","volume":"28","author":[{"given":"Geoff","family":"Sutcliffe","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Miami, Coral Gables, FL, USA. Tel.:\u00a0 ;\u00a0Fax:\u00a0 ;\u00a0E-mail:\u00a0geoff@cs.miami.edu"}]}],"member":"179","reference":[{"key":"10.3233\/AIC-150668_ref1","doi-asserted-by":"crossref","unstructured":"[1]C.\u00a0Barrett, C.\u00a0Conway, M.\u00a0Deters, L.\u00a0Hadarean, D.\u00a0Jovanovic, T.\u00a0King, A.\u00a0Reynolds and C.\u00a0Tinelli, CVC4, in: Proceedings of the 23rd International Conference on Computer Aided Verification, G.\u00a0Gopalakrishnan and S.\u00a0Qadeer, eds, Lecture Notes in Computer Science, Vol.\u00a06806, Springer-Verlag, 2011, pp.\u00a0171\u2013177.","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"10.3233\/AIC-150668_ref2","doi-asserted-by":"crossref","unstructured":"[2]P.\u00a0Baumgartner and U.\u00a0Waldmann, Hierarchic superposition with weak abstraction, in: Proceedings of the 24th International Conference on Automated Deduction, M.P.\u00a0Bonacina, ed., Lecture Notes in Artificial Intelligence, Vol.\u00a07898, Springer-Verlag, 2013, pp.\u00a039\u201357.","DOI":"10.1007\/978-3-642-38574-2_3"},{"key":"10.3233\/AIC-150668_ref3","doi-asserted-by":"crossref","unstructured":"[3]A.\u00a0Reynolds, C.\u00a0Tinelli and L.\u00a0de\u00a0Moura, Finding conflicting instances of quantified formulas in SMT, in: Proceedings of the 14th Conference on Formal Methods in Computer-Aided Design, K.\u00a0Claessen and V.\u00a0Kuncak, eds, 2014, pp.\u00a0195\u2013202.","DOI":"10.1109\/FMCAD.2014.6987613"},{"key":"10.3233\/AIC-150668_ref4","doi-asserted-by":"crossref","unstructured":"[4]A.\u00a0Reynolds, C.\u00a0Tinelli, A.\u00a0Goel and S.\u00a0Krstic, Finite model finding in SMT, in: Proceedings of the 25th International Conference on Computer Aided Verification, N.\u00a0Sharygina and H.\u00a0Veith, eds, Lecture Notes in Computer Science, Vol.\u00a08044, Springer-Verlag, 2013, pp.\u00a0640\u2013655.","DOI":"10.1007\/978-3-642-39799-8_42"},{"key":"10.3233\/AIC-150668_ref5","doi-asserted-by":"crossref","unstructured":"[5]A.\u00a0Reynolds, C.\u00a0Tinelli, A.\u00a0Goel, S.\u00a0Krstic, M.\u00a0Deters and C.\u00a0Barrett, Quantifier instantiation techniques for finite model finding in SMT, in: Proceedings of the 24th International Conference on Automated Deduction, M.P.\u00a0Bonacina, ed., Lecture Notes in Artificial Intelligence, Vol.\u00a07898, Springer-Verlag, 2013, pp.\u00a0377\u2013391.","DOI":"10.1007\/978-3-642-38574-2_26"},{"key":"10.3233\/AIC-150668_ref6","doi-asserted-by":"crossref","unstructured":"[6]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-150668_ref7","doi-asserted-by":"crossref","unstructured":"[7]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-150668_ref8","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"},{"key":"10.3233\/AIC-150668_ref9","unstructured":"[9]G.\u00a0Sutcliffe, The SZS ontologies for automated reasoning software, in: Proceedings of the LPAR Workshops, Knowledge Exchange: Automated Provers and Proof Assistants, and the 7th International Workshop on the Implementation of Logics, G.\u00a0Sutcliffe, P.\u00a0Rudnicki, R.\u00a0Schmidt, B.\u00a0Konev and S.\u00a0Schulz, eds, CEUR Workshop Proceedings, Vol.\u00a0418, 2008, pp.\u00a038\u201349."},{"issue":"4","key":"10.3233\/AIC-150668_ref10","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-150668_ref11","doi-asserted-by":"crossref","unstructured":"[11]G.\u00a0Sutcliffe, The TPTP world\u00a0\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-150668_ref12","unstructured":"[12]G.\u00a0Sutcliffe, in: Proceedings of the 7th IJCAR ATP System Competition, Vienna, Austria, 2014."},{"issue":"4","key":"10.3233\/AIC-150668_ref13","doi-asserted-by":"crossref","first-page":"405","DOI":"10.3233\/AIC-140606","article-title":"The CADE-24 automated theorem proving system competition\u00a0\u2013 CASC-24","volume":"27","author":"Sutcliffe","year":"2014","journal-title":"AI Communications"},{"issue":"1,2","key":"10.3233\/AIC-150668_ref14","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-150668_ref15","doi-asserted-by":"crossref","unstructured":"[15]A.\u00a0Voronkov, AVATAR: The new architecture for first-order theorem provers, in: Proceedings of Automated Reasoning, 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"}],"container-title":["AI Communications"],"original-title":[],"link":[{"URL":"https:\/\/content.iospress.com\/download?id=10.3233\/AIC-150668","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,11]],"date-time":"2025-03-11T00:19:02Z","timestamp":1741652342000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.medra.org\/servlet\/aliasResolver?alias=iospress&doi=10.3233\/AIC-150668"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,9,18]]},"references-count":15,"journal-issue":{"issue":"4"},"URL":"https:\/\/doi.org\/10.3233\/aic-150668","relation":{},"ISSN":["1875-8452","0921-7126"],"issn-type":[{"type":"electronic","value":"1875-8452"},{"type":"print","value":"0921-7126"}],"subject":[],"published":{"date-parts":[[2015,9,18]]}}}