{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,12]],"date-time":"2026-11-12T12:52:44Z","timestamp":1794487964729,"version":"4.9.1"},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319136462","type":"print"},{"value":"9783319136479","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-13647-9_39","type":"book-chapter","created":{"date-parts":[[2014,11,5]],"date-time":"2014-11-05T03:02:35Z","timestamp":1415156555000},"page":"431-442","source":"Crossref","is-referenced-by-count":3,"title":["Experimenting\u00a0with\u00a0SAT\u00a0Solvers\u00a0in\u00a0Vampire"],"prefix":"10.1007","author":[{"given":"Armin","family":"Biere","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ioan","family":"Dragan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Laura","family":"Kov\u00e1cs","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"39_CR1","unstructured":"HPC Center - West University of Timisoara, \n                    \n                      http:\/\/hpc.uvt.ro\/infrastructure\/infragrid\/"},{"issue":"2-4","key":"39_CR2","first-page":"75","volume":"4","author":"A. Biere","year":"2008","unstructured":"Biere, A.: Picosat essentials. JSAT\u00a04(2-4), 75\u201397 (2008)","journal-title":"JSAT"},{"key":"39_CR3","unstructured":"Biere, A.: Lingeling, plingeling and treengeling entering sat competition 2013. In: SAT Competition 2013, pp. 51\u201352 (2013)"},{"key":"39_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/11499107_5","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2005","unstructured":"E\u00e9n, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569, pp. 61\u201375. Springer, Heidelberg (2005)"},{"key":"39_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"39_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/978-3-642-38574-2_33","volume-title":"Automated Deduction \u2013 CADE-24","author":"K. Hoder","year":"2013","unstructured":"Hoder, K., Voronkov, A.: The 481 ways to split a clause and deal with propositional variables. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol.\u00a07898, pp. 450\u2013464. Springer, Heidelberg (2013)"},{"key":"39_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-642-37651-1_10","volume-title":"Programming Logics","author":"K. Korovin","year":"2013","unstructured":"Korovin, K.: Inst-gen \u2013 A modular approach to instantiation-based automated reasoning. In: Voronkov, A., Weidenbach, C. (eds.) Programming Logics. LNCS, vol.\u00a07797, pp. 239\u2013270. Springer, Heidelberg (2013)"},{"key":"39_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-39799-8_1","volume-title":"Computer Aided Verification","author":"L. Kov\u00e1cs","year":"2013","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-Order Theorem Proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 1\u201335. Springer, Heidelberg (2013)"},{"key":"39_CR9","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Hillenbrand, T., Riazanov, A., Voronkov, A.: On the evaluation of indexing techniques for theorem proving. In: IJCAR, pp. 257\u2013271 (2001)","DOI":"10.1007\/3-540-45744-5_19"},{"key":"39_CR10","unstructured":"Riazanov, A., Voronkov, A.: Splitting without backtracking. In: IJCAI, pp. 611\u2013617 (2001)"},{"issue":"1-2","key":"39_CR11","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/S0747-7171(03)00040-3","volume":"36","author":"A. Riazanov","year":"2003","unstructured":"Riazanov, A., Voronkov, A.: Limited resource strategy in resolution theorem proving. J. Symb. Comput.\u00a036(1-2), 101\u2013115 (2003)","journal-title":"J. Symb. Comput."},{"key":"39_CR12","unstructured":"Silva, J.P.M., Lynce, I., Malik, S.: Conflict-driven clause learning sat solvers. In: Handbook of Satisfiability, pp. 131\u2013153 (2009)"},{"issue":"4","key":"39_CR13","doi-asserted-by":"publisher","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. J. Autom. Reasoning\u00a043(4), 337\u2013362 (2009)","journal-title":"J. Autom. Reasoning"},{"key":"39_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1007\/978-3-540-74510-5_4","volume-title":"Computer Science \u2013 Theory and Applications","author":"G. Sutcliffe","year":"2007","unstructured":"Sutcliffe, G.: TPTP, TSTP, CASC, etc. In: Diekert, V., Volkov, M.V., Voronkov, A. (eds.) CSR 2007. LNCS, vol.\u00a04649, pp. 6\u201322. Springer, Heidelberg (2007)"},{"key":"39_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1007\/978-3-319-08867-9_46","volume-title":"Computer Aided Verification","author":"A. Voronkov","year":"2014","unstructured":"Voronkov, A.: AVATAR: The architecture for first-order theorem provers. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol.\u00a08559, pp. 696\u2013710. Springer, Heidelberg (2014)"},{"key":"39_CR16","doi-asserted-by":"crossref","unstructured":"Weidenbach, C.: Combining superposition, sorts and splitting. In: Handbook of Automated Reasoning, pp. 1965\u20132013 (2001)","DOI":"10.1016\/B978-044450813-3\/50029-1"}],"container-title":["Lecture Notes in Computer Science","Human-Inspired Computing and Its Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-13647-9_39","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,28]],"date-time":"2019-05-28T10:28:30Z","timestamp":1559039310000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-13647-9_39"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319136462","9783319136479"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-13647-9_39","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/978-3-319-13647-9","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}