{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T22:54:36Z","timestamp":1673477676769},"reference-count":14,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2011,1,5]],"date-time":"2011-01-05T00:00:00Z","timestamp":1294185600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2011,8]]},"DOI":"10.1007\/s10817-010-9216-8","type":"journal-article","created":{"date-parts":[[2011,1,3]],"date-time":"2011-01-03T23:49:54Z","timestamp":1294098594000},"page":"111-132","source":"Crossref","is-referenced-by-count":7,"title":["Automated Inference of Finite Unsatisfiability"],"prefix":"10.1007","volume":"47","author":[{"given":"Koen","family":"Claessen","sequence":"first","affiliation":[]},{"given":"Ann","family":"Lilliestr\u00f6m","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2011,1,5]]},"reference":[{"key":"9216_CR1","doi-asserted-by":"crossref","unstructured":"Benzm\u00fcller, C., Theiss, F., Paulson, L., Fietzke, A.: LEO-II\u2014a cooperative automatic theorem prover for higher-order logic. In: Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, 12\u201315 August, 2008, Proceedings. LNCS, vol. 5195, pp. 162\u2013170. Springer (2008)","DOI":"10.1007\/978-3-540-71070-7_14"},{"key":"9216_CR2","unstructured":"B\u00f6rger, E., Gr\u00e4del, E., Gurevich, Y.: The Classical Decision Problem. Universitext. Springer (2001)"},{"key":"9216_CR3","doi-asserted-by":"crossref","first-page":"388","DOI":"10.1007\/978-3-642-02959-2_29","volume-title":"CADE-22: Proceedings of the 22nd International Conference on Automated Deduction","author":"K Claessen","year":"2009","unstructured":"Claessen, K., Lilliestr\u00f6m, A.: Automated inference of finite unsatisfiability. In: CADE-22: Proceedings of the 22nd International Conference on Automated Deduction, pp. 388\u2013403. Springer, Berlin, Heidelberg (2009)"},{"key":"9216_CR4","unstructured":"Claessen, K., S\u00f6rensson, N.: New techniques that improve MACE-style model finding. In: Proc. of Workshop on Model Computation (MODEL) (2003)"},{"key":"9216_CR5","unstructured":"Curry, H.B.: Foundations of Mathematical Logic. Courier Dover Publications (1977)"},{"issue":"3","key":"9216_CR6","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1023\/A:1005843212881","volume":"19","author":"W McCune","year":"1997","unstructured":"McCune, W.: Solution of the Robbins problem. J. Autom. Reas. 19(3), 263\u2013276 (1997)","journal-title":"J. Autom. Reas."},{"key":"9216_CR7","doi-asserted-by":"crossref","unstructured":"McCune, W.: Mace4 reference manual and guide. CoRR, cs.SC\/0310055 (2003)","DOI":"10.2172\/822574"},{"key":"9216_CR8","doi-asserted-by":"crossref","unstructured":"Roederer, A., Puzis, Y., Sutcliffe, G.: Divvy: an ATP meta-system based on axiom relevance ordering. In: CADE, pp. 157\u2013162 (2009)","DOI":"10.1007\/978-3-642-02959-2_13"},{"issue":"2, 3","key":"9216_CR9","first-page":"111","volume":"15","author":"S Schulz","year":"2002","unstructured":"Schulz, S.: E\u2014a brainiac theorem prover. AI Commun. 15(2, 3), 111\u2013126 (2002)","journal-title":"AI Commun."},{"key":"9216_CR10","unstructured":"Sutcliffe, G.: The SZS ontologies for automated reasoning software. In: Rudnicki, P., Sutcliffe, G., Konev, B., Schmidt, R.A., Schulz, S. (eds.) LPAR Workshops. CEUR Workshop Proceedings, vol. 418. CEUR-WS.org (2008)"},{"issue":"4","key":"9216_CR11","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","volume":"43","author":"G Sutcliffe","year":"2009","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure: the FOF and CNF parts, v3.5.0. J. Autom. Reas. 43(4), 337\u2013362 (2009)","journal-title":"J. Autom. Reas."},{"issue":"1","key":"9216_CR12","first-page":"35","volume":"19","author":"G Sutcliffe","year":"2006","unstructured":"Sutcliffe, G., Suttner, C.: The state of CASC. AI Commun. 19(1), 35\u201348 (2006)","journal-title":"AI Commun."},{"key":"9216_CR13","unstructured":"V\u00e4nn\u00e4nnen, J.: A Short Course on Finite Model Theory. Department of Mathematics, University of Helsinki (2006)"},{"key":"9216_CR14","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1007\/3-540-45620-1_22","volume-title":"Automated Deduction, CADE-18: 18th International Conference on Automated Deduction. Lecture Notes in Artificial Intelligence, vol. 2392","author":"C Weidenbach","year":"2002","unstructured":"Weidenbach, C., Brahm, U., Hillenbrand, T., Keen, E., Theobalt, C., Topi\u0107, D.: SPASS version 2.0. In: Voronkov, A. (ed.) Automated Deduction, CADE-18: 18th International Conference on Automated Deduction. Lecture Notes in Artificial Intelligence, vol. 2392, pp. 275\u2013279. Springer, Copenhagen, Denmark (2002)","edition":"2392"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-010-9216-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-010-9216-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-010-9216-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T10:39:27Z","timestamp":1559903967000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-010-9216-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,1,5]]},"references-count":14,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2011,8]]}},"alternative-id":["9216"],"URL":"https:\/\/doi.org\/10.1007\/s10817-010-9216-8","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,1,5]]}}}