{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,3]],"date-time":"2025-11-03T22:59:29Z","timestamp":1762210769381,"version":"3.41.2"},"reference-count":1,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2014,6,27]],"date-time":"2014-06-27T00:00:00Z","timestamp":1403827200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"funder":[{"name":"National Science Foundation","award":["1213151"],"award-info":[{"award-number":["1213151"]}]},{"name":"National Science Foundation","award":["1101228"],"award-info":[{"award-number":["1101228"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>The Stone tautologies are known to have polynomial size resolution\nrefutations and require exponential size regular refutations. We prove that the\nStone tautologies also have polynomial size proofs in both pool resolution and\nthe proof system of regular tree-like resolution with input lemmas (regRTI).\nTherefore, the Stone tautologies do not separate resolution from DPLL with\nclause learning.<\/jats:p>","DOI":"10.2168\/lmcs-10(2:16)2014","type":"journal-article","created":{"date-parts":[[2014,11,14]],"date-time":"2014-11-14T09:40:42Z","timestamp":1415958042000},"source":"Crossref","is-referenced-by-count":5,"title":["Small Stone in Pool"],"prefix":"10.46298","volume":"Volume 10, Issue 2","author":[{"given":"Samuel R.","family":"Buss","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Leszek Aleksander","family":"Kolodziejczyk","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2014,6,27]]},"reference":[{"key":"804:not-found"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/852\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/852\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T19:57:40Z","timestamp":1681243060000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/852"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,6,27]]},"references-count":1,"URL":"https:\/\/doi.org\/10.2168\/lmcs-10(2:16)2014","relation":{"is-same-as":[{"id-type":"arxiv","id":"1405.5626","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1405.5626","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2014,6,27]]},"article-number":"852"}}