{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:35:23Z","timestamp":1740123323600,"version":"3.37.3"},"reference-count":47,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2022,2,1]],"date-time":"2022-02-01T00:00:00Z","timestamp":1643673600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,2,1]],"date-time":"2022-02-01T00:00:00Z","timestamp":1643673600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"Max Planck Institute for Informatics"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2022,11]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Shortly before Larry Wos passed away, he sent a manuscript for discussion to Sophie Tourret, the editor of the AAR newsletter. We present excerpts from this final manuscript, put it in its historic context and explain its relevance for today\u2019s research in automated reasoning.<\/jats:p>","DOI":"10.1007\/s10817-022-09617-3","type":"journal-article","created":{"date-parts":[[2022,2,1]],"date-time":"2022-02-01T11:03:14Z","timestamp":1643713394000},"page":"575-584","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Posthumous Contribution by Larry Wos: Excerpts from an Unpublished Column"],"prefix":"10.1007","volume":"66","author":[{"given":"Sophie","family":"Tourret","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6002-0458","authenticated-orcid":false,"given":"Christoph","family":"Weidenbach","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,2,1]]},"reference":[{"issue":"3","key":"9617_CR1","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","volume":"4","author":"L Bachmair","year":"1994","unstructured":"Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Log. Comput. 4(3), 217\u2013247 (1994)","journal-title":"J. Log. Comput."},{"key":"9617_CR2","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/BF01190829","volume":"5","author":"L Bachmair","year":"1994","unstructured":"Bachmair, L., Ganzinger, H., Waldmann, U.: Refutational theorem proving for hierarchic first-order theories. Appl. Algebra Eng. Commun. Comput. 5, 193\u2013212 (1994)","journal-title":"Appl. Algebra Eng. Commun. Comput."},{"key":"9617_CR3","unstructured":"Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 825\u2013885. IOS Press (2009)"},{"key":"9617_CR4","doi-asserted-by":"crossref","unstructured":"Barrett, C.W., Conway, C.L., Deters, M., Hadarean, L., Jovanovic, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14\u201320, 2011. Proceedings, Springer, Lecture Notes in Computer Science, vol. 6806, pp. 171\u2013177 (2011)","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"9617_CR5","unstructured":"Bentkamp, A., Blanchette, J., Cruanes, S., Waldmann, U.: Superposition for lambda-free higher-order logic. Log. Methods Comput. Sci. 17(2), 1\u201338 (2021)"},{"key":"9617_CR6","doi-asserted-by":"crossref","unstructured":"Bonacina, M.P., Furbach, U., Sofronie-Stokkermans, V.: On first-order model-based reasoning. In: Mart\u00ed-Oliet, N., \u00d6lveczky, P.C., Talcott, C.L. (eds.) Logic, Rewriting, and Concurrency\u2014Essays dedicated to Jos\u00e9 Meseguer on the Occasion of His 65th Birthday, Springer, Lecture Notes in Computer Science, vol. 9200, pp. 181\u2013204 (2015)","DOI":"10.1007\/978-3-319-23165-5_8"},{"key":"9617_CR7","doi-asserted-by":"crossref","unstructured":"Bonacina, M.P., Fontaine, P., Ringeissen, C., Tinelli, C.: Theory combination: beyond equality sharing. In: Lutz, C., Sattler, U., Tinelli, C., Turhan, A., Wolter, F. (eds.) Description Logic, Theory Combination, and All That\u2014Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday, Springer, Lecture Notes in Computer Science, vol. 11560, pp. 57\u201389 (2019)","DOI":"10.1007\/978-3-030-22102-7_3"},{"key":"9617_CR8","doi-asserted-by":"crossref","unstructured":"Bromberger, M., Fiori, A., Weidenbach, C.: Deciding the Bernays\u2013Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories. In: Henglein, F., Shoham, S., Vizel, Y. (eds.) Verification, Model Checking, and Abstract Interpretation - 22nd International Conference, VMCAI 2021, Copenhagen, Denmark, January 17\u201319, 2021, Proceedings, Springer, Lecture Notes in Computer Science, vol. 12597, pp. 511\u2013533 (2021)","DOI":"10.1007\/978-3-030-67067-2_23"},{"issue":"1\u20132","key":"9617_CR9","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/s10472-009-9152-7","volume":"55","author":"R Bruttomesso","year":"2009","unstructured":"Bruttomesso, R., Cimatti, A., Franz\u00e9n, A., Griggio, A., Sebastiani, R.: Delayed theory combination vs. Nelson\u2013Oppen for satisfiability modulo theories: a comparative analysis. Ann. Math. Artif. Intell. 55(1\u20132), 63\u201399 (2009)","journal-title":"Ann. Math. Artif. Intell."},{"issue":"1","key":"9617_CR10","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/s10817-019-09512-4","volume":"64","author":"PD Chocron","year":"2020","unstructured":"Chocron, P.D., Fontaine, P., Ringeissen, C.: Politeness and combination methods for theories with bridging functions. J. Autom. Reason. 64(1), 97\u2013134 (2020)","journal-title":"J. Autom. Reason."},{"key":"9617_CR11","doi-asserted-by":"crossref","unstructured":"Comon, H., Godoy, G., Nieuwenhuis, R.: The confluence of ground term rewrite systems is decidable in polynomial time. In: 42nd Annual Symposium on Foundations of Computer Science, FOCS 2001, 14\u201317 October 2001, pp. 298\u2013307. Nevada, USA, IEEE Computer Society, Las Vegas (2001)","DOI":"10.1109\/SFCS.2001.959904"},{"issue":"3","key":"9617_CR12","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201\u2013215 (1960)","journal-title":"J. ACM"},{"key":"9617_CR13","doi-asserted-by":"crossref","unstructured":"Dershowitz, N., Plaisted, D.A.: Rewriting. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 2, pp. 535\u2013610. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50011-4"},{"issue":"3","key":"9617_CR14","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"D Detlefs","year":"2005","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365\u2013473 (2005)","journal-title":"J. ACM"},{"key":"9617_CR15","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.: Efficient e-matching for SMT solvers. In: Pfenning, F. (ed.) Automated Deduction\u2014CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17\u201320, 2007, Proceedings, Springer, Lecture Notes in Computer Science, vol. 4603, pp. 183\u2013198 (2007)","DOI":"10.1007\/978-3-540-73595-3_13"},{"issue":"2","key":"9617_CR16","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/j.entcs.2008.04.079","volume":"198","author":"LM de Moura","year":"2008","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Model-based theory combination. Electron. Notes Theor. Comput. Sci. 198(2), 37\u201349 (2008)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"9617_CR17","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29\u2013April 6, 2008. Proceedings, Springer, Lecture Notes in Computer Science, vol. 4963, pp. 337\u2013340 (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9617_CR18","doi-asserted-by":"crossref","unstructured":"Duarte, A., Korovin, K.: Implementing superposition in iProver (system description). In: Peltier, N., Sofronie-Stokkermans, V. (eds.) Automated Reasoning\u201410th International Joint Conference, IJCAR 2020, Paris, France, July 1\u20134, 2020, Proceedings, Part II, Springer, Lecture Notes in Computer Science, vol. 12167, pp. 388\u2013397 (2020)","DOI":"10.1007\/978-3-030-51054-1_24"},{"key":"9617_CR19","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003. Santa Margherita Ligure, Italy, May 5\u20138, 2003 Selected Revised Papers, Springer, Lecture Notes in Computer Science, vol. 2919, pp. 502\u2013518 (2003)"},{"key":"9617_CR20","doi-asserted-by":"crossref","unstructured":"Fiori, A., Weidenbach, C.: SCL clause learning from simple models. In: Fontaine, P. (ed.) Automated Deduction\u2014CADE 27\u201427th International Conference on Automated Deduction, Natal, Brazil, August 27\u201330, 2019, Proceedings, Springer, Lecture Notes in Computer Science, vol. 11716, pp. 233\u2013249 (2019)","DOI":"10.1007\/978-3-030-29436-6_14"},{"key":"9617_CR21","unstructured":"Fiori, A., Weidenbach, C.: SCL with Theory Constraints. CoRR arXiv:2003.04627 (2020)"},{"key":"9617_CR22","doi-asserted-by":"crossref","unstructured":"Ganzinger, H., Korovin, K.: New directions in instantiation-based theorem proving. In: 18th IEEE Symposium on Logic in Computer Science (LICS 2003), 22\u201325 June 2003, Ottawa, Canada, Proceedings, IEEE Computer Society, pp. 55\u201364 (2003)","DOI":"10.1109\/LICS.2003.1210045"},{"key":"9617_CR23","doi-asserted-by":"crossref","unstructured":"Ge, Y., de\u00a0Moura, L.M.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26\u2013July 2, 2009. Proceedings, Springer, Lecture Notes in Computer Science, vol. 5643, pp. 306\u2013320 (2009)","DOI":"10.1007\/978-3-642-02658-4_25"},{"issue":"1","key":"9617_CR24","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1147\/rd.41.0028","volume":"4","author":"PC Gilmore","year":"1960","unstructured":"Gilmore, P.C.: A proof method for quantification theory: its justification and realization. IBM J. Res. Dev. 4(1), 28\u201335 (1960)","journal-title":"IBM J. Res. Dev."},{"key":"9617_CR25","doi-asserted-by":"crossref","unstructured":"Haifani, F., Tourret, S., Weidenbach, C.: Generalized completeness for SOS resolution and its application to a new notion of relevance. In: Platzer, A., Sutcliffe, G. (eds.) Automated Deduction\u2014CADE 28\u201428th International Conference on Automated Deduction, Virtual Event, July 12\u201315, 2021, Proceedings, Springer, Lecture Notes in Computer Science, vol. 12699, pp. 327\u2013343 (2021)","DOI":"10.1007\/978-3-030-79876-5_19"},{"key":"9617_CR26","doi-asserted-by":"crossref","unstructured":"Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebras. In: Leech, I. (ed.) Computational Problems in Abstract Algebra, pp. 263\u2013297. Pergamon Press (1970)","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"9617_CR27","unstructured":"Lankford\u00a0Dallas, S.: Canonical inference. Technical Report ATP-32, Southwestern University, Georgetown, Texas (1975)"},{"key":"9617_CR28","doi-asserted-by":"crossref","unstructured":"McCune, W.: OTTER 2.0. In: Stickel, M.E. (ed.) 10th International Conference on Automated Deduction, Kaiserslautern, FRG, July 24\u201327, 1990, Proceedings, Springer, Lecture Notes in Computer Science, vol. 449, pp. 663\u2013664 (1990)","DOI":"10.1007\/3-540-52885-7_131"},{"key":"9617_CR29","unstructured":"Monniaux, D.: A survey of satisfiability modulo theory. In: Gerdt, V.P., Koepf, W., Seiler, W.M., Vorozhtsov, E.V. (eds.) Computer Algebra in Scientific Computing\u201418th International Workshop, CASC 2016, Bucharest, Romania, September 19\u201323, 2016, Proceedings, Springer, Lecture Notes in Computer Science, vol. 9890, pp. 401\u2013425 (2016)"},{"issue":"2","key":"9617_CR30","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245\u2013257 (1979)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"2","key":"9617_CR31","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G Nelson","year":"1980","unstructured":"Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J. ACM 27(2), 356\u2013364 (1980)","journal-title":"J. ACM"},{"issue":"6","key":"9617_CR32","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis\u2013Putnam\u2013Logemann\u2013Loveland procedure to dpll(T). J. ACM 53(6), 937\u2013977 (2006)","journal-title":"J. ACM"},{"key":"9617_CR33","unstructured":"P\u00e9rez, J.A.N., Voronkov, A.: Proof systems for effectively propositional logic. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12\u201315, 2008, Proceedings, Springer, Lecture Notes in Computer Science, vol. 5195, pp. 426\u2013440 (2008)"},{"key":"9617_CR34","unstructured":"Prawitz, D.: Commentary by the author: an improved proof procedure. In: Siekmann, J., Wrightson, G. (eds.) Automation of Reasoning: Classical Papers on Computational Logic, vol. 1, pp. 159\u2013161. Springer (1983)"},{"key":"9617_CR35","doi-asserted-by":"crossref","unstructured":"Reynolds, A., Barbosa, H., Fontaine, P.: Revisiting enumerative instantiation. In: Beyer, D., Huisman, M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems\u201424th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14\u201320, 2018, Proceedings, Part II, Springer, Lecture Notes in Computer Science, vol. 10806, pp. 112\u2013131 (2018)","DOI":"10.1007\/978-3-319-89963-3_7"},{"issue":"2\u20133","key":"9617_CR36","first-page":"91","volume":"15","author":"A Riazanov","year":"2002","unstructured":"Riazanov, A., Voronkov, A.: The design and implementation of VAMPIRE. AI Commun. 15(2\u20133), 91\u2013110 (2002)","journal-title":"AI Commun."},{"key":"9617_CR37","unstructured":"Robinson, J.A., Voronkov, A. (eds.): Handbook of Automated Reasoning, vol. 2. Elsevier and MIT Press (2001)"},{"key":"9617_CR38","doi-asserted-by":"crossref","unstructured":"Schulz, S., Cruanes, S., Vukmirovic, P.: Faster, higher, stronger: E 2.3. In: Fontaine, P. (ed.) Automated Deduction\u2014CADE 27\u201427th International Conference on Automated Deduction, Natal, Brazil, August 27\u201330, 2019, Proceedings, Springer, Lecture Notes in Computer Science, vol. 11716, pp. 495\u2013507 (2019)","DOI":"10.1007\/978-3-030-29436-6_29"},{"issue":"1","key":"9617_CR39","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/BF00246025","volume":"2","author":"ME Stickel","year":"1986","unstructured":"Stickel, M.E.: Schubert\u2019s steamroller problem: formulation and solutions. J. Autom. Reason. 2(1), 89\u2013101 (1986)","journal-title":"J. Autom. Reason."},{"issue":"4","key":"9617_CR40","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/s10817-017-9407-7","volume":"59","author":"G Sutcliffe","year":"2017","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure\u2014from CNF to TH0, TPTP v.6.4.0. J. Autom. Reason. 59(4), 483\u2013502 (2017)","journal-title":"J. Autom. Reason."},{"key":"9617_CR41","doi-asserted-by":"crossref","unstructured":"Tammet, T.: GKC: a reasoning system for large knowledge bases. In: Fontaine, P. (ed.) Automated Deduction\u2014CADE 27\u201427th International Conference on Automated Deduction, Natal, Brazil, August 27\u201330, 2019, Proceedings, Springer, Lecture Notes in Computer Science, vol. 11716, pp. 538\u2013549 (2019)","DOI":"10.1007\/978-3-030-29436-6_32"},{"issue":"3","key":"9617_CR42","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/BF00252178","volume":"16","author":"R Veroff","year":"1996","unstructured":"Veroff, R.: Using hints to increase the effectiveness of an automated reasoning program: case studies. J. Autom. Reason. 16(3), 223\u2013239 (1996)","journal-title":"J. Autom. Reason."},{"issue":"2","key":"9617_CR43","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1023\/A:1010639725972","volume":"27","author":"R Veroff","year":"2001","unstructured":"Veroff, R.: Solving open questions and other challenge problems using proof sketches. J. Autom. Reason. 27(2), 157\u2013174 (2001)","journal-title":"J. Autom. Reason."},{"key":"9617_CR44","doi-asserted-by":"crossref","unstructured":"Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 2, pp. 1965\u20132013. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50029-1"},{"key":"9617_CR45","doi-asserted-by":"crossref","unstructured":"Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R.A. (ed.) Automated Deduction\u2014CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, August 2\u20137, 2009. Proceedings, Springer, Lecture Notes in Computer Science, vol. 5663, pp. 140\u2013145 (2009)","DOI":"10.1007\/978-3-642-02959-2_10"},{"key":"9617_CR46","doi-asserted-by":"crossref","unstructured":"Wos, L., Carson, D.F., Robinson, G.A.: The unit preference strategy in theorem proving. In: Proceedings of the 1964 fall Joint Computer Conference, part I, AFIPS 1964 (Fall, part I), San Francisco, California, USA, October 27\u201329, 1964, ACM, pp. 615\u2013621 (1964)","DOI":"10.1145\/1464052.1464109"},{"issue":"4","key":"9617_CR47","doi-asserted-by":"publisher","first-page":"536","DOI":"10.1145\/321296.321302","volume":"12","author":"L Wos","year":"1965","unstructured":"Wos, L., Robinson, G.A., Carson, D.F.: Efficiency and completeness of the set of support strategy in theorem proving. J. ACM 12(4), 536\u2013541 (1965)","journal-title":"J. ACM"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-022-09617-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-022-09617-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-022-09617-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,17]],"date-time":"2024-09-17T18:23:23Z","timestamp":1726597403000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-022-09617-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,2,1]]},"references-count":47,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2022,11]]}},"alternative-id":["9617"],"URL":"https:\/\/doi.org\/10.1007\/s10817-022-09617-3","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2022,2,1]]},"assertion":[{"value":"5 July 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"10 January 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"1 February 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}