{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T13:21:53Z","timestamp":1773840113158,"version":"3.50.1"},"reference-count":8,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T00:00:00Z","timestamp":1773792000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0"},{"start":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T00:00:00Z","timestamp":1773792000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0"}],"funder":[{"name":"Northeastern University USA"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2026,6]]},"DOI":"10.1007\/s10817-026-09752-1","type":"journal-article","created":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T09:39:58Z","timestamp":1773826798000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Applying Saturation-Based Theorem Proving to Open Problems in Positive Implicational Logic"],"prefix":"10.1007","volume":"70","author":[{"given":"Branden","family":"Fitelson","sequence":"first","affiliation":[]},{"given":"Nicolas","family":"Peltier","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2026,3,18]]},"reference":[{"key":"9752_CR1","doi-asserted-by":"publisher","unstructured":"B\u00e1rtek, F., Bhayat, A., Coutelier, R., Hajdu, M., Hetzenberger, M., Hozzov\u00e1, P., Kov\u00e1cs, L., Rath, J., Rawson, M., Reger, G., Suda, M., Schoisswohl, J., Voronkov, A.: The Vampire Diary. In 37th International Conference on Computer Aided Verification. LNCS 15933, pp 57-71. Springer (2025). https:\/\/doi.org\/10.48550\/arxiv.2506.03030","DOI":"10.48550\/arxiv.2506.03030"},{"key":"9752_CR2","doi-asserted-by":"crossref","unstructured":"Korovin, K.: iProver \u2014 An Instantiation-Based Theorem Prover for First-Order Logic (System Description). In IJCAR 2008, LNCS 5195, pp. 292\u2013298. Springer, (2008)","DOI":"10.1007\/978-3-540-71070-7_24"},{"key":"9752_CR3","first-page":"171","volume":"4","author":"AN Prior","year":"1963","unstructured":"Prior, A.N., Meredith, C.: Notes on the axiomatics of the propositional calculus. Notre Dame J. Formal Logic 4, 171\u2013187 (1963)","journal-title":"Notre Dame J. Formal Logic"},{"issue":"3","key":"9752_CR4","first-page":"169","volume":"1","author":"C Meredith","year":"1953","unstructured":"Meredith, C.: A single axiom of positive logic. The journal of computing systems 1(3), 169\u2013170 (1953)","journal-title":"The journal of computing systems"},{"key":"9752_CR5","doi-asserted-by":"crossref","unstructured":"Schulz, S., Cruanes, S., Vukmirovi\u0107, P.: Faster, higher, stronger: E 2.3. In International Conference on Automated Deduction (pp. 495-507). Cham: Springer International Publishing","DOI":"10.1007\/978-3-030-29436-6_29"},{"key":"9752_CR6","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G.: Stepping Stones in the TPTP World. In IJCAR, LNCS 14739, pp 30-50. Springer (2024)","DOI":"10.1007\/978-3-031-63498-7_3"},{"key":"9752_CR7","first-page":"39","volume":"28","author":"D Ulrich","year":"1999","unstructured":"Ulrich, D.: New single axioms for positive implication. Bull. Sect. Logic 28, 39\u201342 (1999)","journal-title":"Bull. Sect. Logic"},{"issue":"2","key":"9752_CR8","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1023\/A:1010683508225","volume":"27","author":"D Ulrich","year":"2001","unstructured":"Ulrich, D.: A legacy recalled and a tradition continued. J. Autom. Reason. 27(2), 97\u2013122 (2001)","journal-title":"J. Autom. Reason."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-026-09752-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-026-09752-1","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-026-09752-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T09:40:02Z","timestamp":1773826802000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-026-09752-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,3,18]]},"references-count":8,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2026,6]]}},"alternative-id":["9752"],"URL":"https:\/\/doi.org\/10.1007\/s10817-026-09752-1","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,3,18]]},"assertion":[{"value":"27 October 2025","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"2 March 2026","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 March 2026","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}],"article-number":"5"}}