{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,28]],"date-time":"2026-01-28T04:44:48Z","timestamp":1769575488099,"version":"3.49.0"},"reference-count":54,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2017,2,17]],"date-time":"2017-02-17T00:00:00Z","timestamp":1487289600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2017,12]]},"DOI":"10.1007\/s10817-017-9407-7","type":"journal-article","created":{"date-parts":[[2017,2,17]],"date-time":"2017-02-17T09:00:47Z","timestamp":1487322047000},"page":"483-502","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":152,"title":["The TPTP Problem Library and Associated Infrastructure"],"prefix":"10.1007","volume":"59","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9120-3927","authenticated-orcid":false,"given":"Geoff","family":"Sutcliffe","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,2,17]]},"reference":[{"key":"9407_CR1","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard: Version 2.0. In: Gupta, A., Kroening, D. (eds.) Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (2010)"},{"key":"9407_CR2","doi-asserted-by":"crossref","unstructured":"Baumgartner, P.: SMTtoTPTP-A converter for theorem proving formats. In: Felty, A., Middeldorp, A. (eds.) Proceedings of the 25th International Conference on Automated Deduction, number 9195 in Lecture Notes in Computer Science, pp. 285\u2013294. Springer (2015)","DOI":"10.1007\/978-3-319-21401-6_19"},{"issue":"1","key":"9407_CR3","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1007\/s11787-012-0052-y","volume":"7","author":"C Benzm\u00fcller","year":"2013","unstructured":"Benzm\u00fcller, C., Paulson, L.: Quantified multimodal logics in simple type theory. Log. Univ. 7(1), 7\u201320 (2013)","journal-title":"Log. Univ."},{"issue":"3","key":"9407_CR4","doi-asserted-by":"crossref","first-page":"318","DOI":"10.1016\/j.jal.2007.06.003","volume":"6","author":"C Benzm\u00fcller","year":"2008","unstructured":"Benzm\u00fcller, C., Sorge, V., Jamnik, M., Kerber, M.: Combined reasoning by automated cooperation. J. Appl. Log. 6(3), 318\u2013342 (2008)","journal-title":"J. Appl. Log."},{"key":"9407_CR5","unstructured":"Benzm\u00fcller, C., Paleo, B.W.: Automating G\u00f6del\u2019s ontological proof of God\u2019s existence with higher-order automated theorem provers. In: Schaub, T. (ed.) Proceedings of the 21st European Conference on Artificial Intelligence, pp. 93\u201398 (2014)"},{"issue":"3","key":"9407_CR6","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1007\/s10817-016-9362-8","volume":"57","author":"J Blanchette","year":"2016","unstructured":"Blanchette, J., Greenaway, D., Kaliszyk, C., K\u00fchlwein, D., Urban, J.: A learning-based fact selector for Isabelle\/HOL. J. Autom. Reason. 57(3), 219\u2013244 (2016)","journal-title":"J. Autom. Reason."},{"key":"9407_CR7","doi-asserted-by":"crossref","unstructured":"Blanchette, J., Paskevich, A.: TFF1: The TPTP typed first-order form with rank-1 polymorphism. In: Bonacina, M.P. (ed.) Proceedings of the 24th International Conference on Automated Deduction, number 7898 in Lecture Notes in Artificial Intelligence, pp. 414\u2013420. Springer (2013)","DOI":"10.1007\/978-3-642-38574-2_29"},{"key":"9407_CR8","doi-asserted-by":"crossref","unstructured":"B\u00f6hme, S., Nipkow, T.: Sledgehammer: judgement day. In: Giesl, J., Haehnle, R. (ed) Proceedings of the 5th International Joint Conference on Automated Reasoning, number 6173 in Lecture Notes in Artificial Intelligence, pp. 107\u2013121 (2010)","DOI":"10.1007\/978-3-642-14203-1_9"},{"key":"9407_CR9","volume-title":"Dewey Decimal Classification and Relative Index","author":"JP Comaromi","year":"1989","unstructured":"Comaromi, J.P., Beall, J., Matthews, W.E., New, G.R.: Dewey Decimal Classification and Relative Index, 20th edn. Forest Press, Cinderford (1989)","edition":"20"},{"key":"9407_CR10","doi-asserted-by":"crossref","unstructured":"Denney, E., Fischer, B., Schumann, J.: Using automated theorem provers to certify auto-generated aerospace software. In: Rusinowitch, M., Basin, D. (eds.) Proceedings of the 2nd International Joint Conference on Automated Reasoning, number 3097 in Lecture Notes in Artificial Intelligence, pp. 198\u2013212 (2004)","DOI":"10.1007\/978-3-540-25984-8_12"},{"key":"9407_CR11","unstructured":"Emmer, M., Khasidashvili, Z., Korovin, K., Voronkov, A.: Encoding industrial hardware verification problems into effectively propositional logic. In: Bloem, R., Sharygina, N. (eds.) Proceedings of the 10th International Conference on Formal Methods in Computer-Aided Design, pp. 137\u2013144. IEEE Press (2010)"},{"key":"9407_CR12","doi-asserted-by":"crossref","unstructured":"Gent, I., Walsh, T.: CSPLib: a benchmark library for constraints. In: Jaffar, J. (ed.), Proceedings of the 5th International Conference on the Principles and Practice of Constraint Programming, number 1713 in Lecture Notes in Computer Science, pp. 480\u2013481. Springer (1999)","DOI":"10.1007\/978-3-540-48085-3_36"},{"key":"9407_CR13","doi-asserted-by":"crossref","unstructured":"H\u00f6fner, P., Struth, G.: Automated reasoning in Kleene Algebra. In: Pfenning, F. (ed.) Proceedings of the 21st International Conference on Automated Deduction, number 4603 in Lecture Notes in Artificial Intelligence, pp. 279\u2013294. Springer (2007)","DOI":"10.1007\/978-3-540-73595-3_19"},{"key":"9407_CR14","unstructured":"Hoos, H., St\u00fctzle, T.: SATLIB: an online resource for research on SAT. In: Gent, I., van Maaren, H., Walsh, T. (eds.) Proceedings of the 3rd Workshop on the Satisfiability Problem, pp. 283\u2013292. IOS Press (2000)"},{"key":"9407_CR15","unstructured":"Kaliszyk, C., Sutcliffe, G., Rabe, F.: TH1: The TPTP typed higher-order form with rank-1 polymorphism. In: Fontaine, P., Schulz, S., Urban, J. (eds.) Proceedings of the 5th Workshop on the Practical Aspects of Automated Reasoning, number 1635 in CEUR Workshop Proceedings, pp. 41\u201355 (2016)"},{"issue":"2","key":"9407_CR16","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/s10817-014-9303-3","volume":"53","author":"C Kaliszyk","year":"2014","unstructured":"Kaliszyk, C., Urban, J.: Learning-assisted automated reasoning with Flyspeck. J. Autom. Reason. 53(2), 173\u2013213 (2014)","journal-title":"J. Autom. Reason."},{"key":"9407_CR17","doi-asserted-by":"crossref","unstructured":"Kotelnikov, E., Kovacs, L., Voronkov, A.: A first class boolean sort in first-order theorem proving and TPTP. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) Proceedings of the International Conference on Intelligent Computer Mathematics, number 9150 in Lecture Notes in Computer Science, pp. 71\u201386. Springer (2015)","DOI":"10.1007\/978-3-319-20615-8_5"},{"key":"9407_CR18","unstructured":"Matuszek, C., Cabral, J., Witbrock, M., DeOliveira, J.: An introduction to the syntax and content of Cyc. In: Baral, C. (ed.) Proceedings of the 2006 AAAI Spring Symposium on Formalizing and Compiling Background Knowledge and Its Applications to Knowledge Representation and Question Answering, pp. 44\u201349 (2006)"},{"key":"9407_CR19","unstructured":"McCune, W.W.: Otter 3.3 Reference Manual. Technical Report ANL\/MSC-TM-263, Argonne National Laboratory, Argonne, USA (2003)"},{"key":"9407_CR20","doi-asserted-by":"crossref","unstructured":"Narizzano, M., Pulina, L., Tacchella, A.: The QBFEVAL Web Portal. In: Fischer, M., van\u00a0der Hoek, W., Konev, B., Lisitsa, A. (eds.) Proceedings of the 10th European Conference on Logics in Artificial Intelligence, pp. 494\u2013497 (2006)","DOI":"10.1007\/11853886_45"},{"key":"9407_CR21","doi-asserted-by":"crossref","unstructured":"Otten, J.: leanCoP 2.0 and ileancop 1.2: high performance lean theorem proving in classical and intuitionistic logic. In: Baumgartner, P., Armando, A., Dowek, G. (eds.) Proceedings of the 4th International Joint Conference on Automated Reasoning, number 5195 in Lecture Notes in Artificial Intelligence, pp. 283\u2013291 (2008)","DOI":"10.1007\/978-3-540-71070-7_23"},{"key":"9407_CR22","doi-asserted-by":"crossref","unstructured":"Paulson, L., Blanchette, J.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: Sutcliffe, G., Ternovska, E., Schulz, S. (eds.) Proceedings of the 8th International Workshop on the Implementation of Logics, number\u00a02 in EPiC, pp. 1\u201311 (2010)","DOI":"10.29007\/36dt"},{"key":"9407_CR23","unstructured":"Pease, A., Sutcliffe, G.: First order reasoning on a large ontology. In: Urban, J., Sutcliffe, G., Schulz, S. (eds.) Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories, number 257 in CEUR Workshop Proceedings, pp. 61\u201370 (2007)"},{"issue":"2","key":"9407_CR24","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/BF02432151","volume":"2","author":"FJ Pelletier","year":"1986","unstructured":"Pelletier, F.J.: Seventy-five problems for testing automatic theorem provers. J. Autom. Reason. 2(2), 191\u2013216 (1986)","journal-title":"J. Autom. Reason."},{"key":"9407_CR25","unstructured":"Phillips, J.D., Stanovsky, D.: Automated theorem proving in loop theory. In: Sutcliffe, G., Colton, S., Schulz, S. (eds.) Proceedings of the CICM Workshop on Empirically Successful Automated Reasoning in Mathematics, number 378 in CEUR Workshop Proceedings, pp. 42\u201353 (2008)"},{"issue":"3","key":"9407_CR26","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/BF00244944","volume":"4","author":"DA Plaisted","year":"1988","unstructured":"Plaisted, D.A.: Non-Horn clause logic programming without contrapositives. J. Autom. Reason. 4(3), 287\u2013325 (1988)","journal-title":"J. Autom. Reason."},{"key":"9407_CR27","unstructured":"Puzis, Y., Gao, Y., Sutcliffe, G.: Automated generation of interesting theorems. In: Sutcliffe, G., Goebel, R. (eds.) Proceedings of the 19th International FLAIRS Conference, pp. 49\u201354. AAAI Press (2006)"},{"issue":"1","key":"9407_CR28","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1007\/BF00263451","volume":"8","author":"A Quaife","year":"1992","unstructured":"Quaife, A.: Automated deduction in von Neumann-Bernays-Godel set theory. J. Autom. Reason. 8(1), 91\u2013147 (1992)","journal-title":"J. Autom. Reason."},{"issue":"1\u20132","key":"9407_CR29","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1007\/s10817-006-9060-z","volume":"38","author":"T Raths","year":"2007","unstructured":"Raths, T., Otten, J., Kreitz, C.: The ILTP problem library for intuitionistic logic\u2014release v1.1. J. Autom. Reason. 38(1\u20132), 261\u2013271 (2007)","journal-title":"J. Autom. Reason."},{"key":"9407_CR30","unstructured":"American\u00a0Mathematical Society. Mathematical Subject Classification. American Mathematical Society (1992)"},{"issue":"6","key":"9407_CR31","doi-asserted-by":"crossref","first-page":"1053","DOI":"10.1142\/S0218213006003119","volume":"15","author":"G Sutcliffe","year":"2006","unstructured":"Sutcliffe, G.: Semantic derivation verification: techniques and implementation. Int. J. Artif. Intell. Tools 15(6), 1053\u20131070 (2006)","journal-title":"Int. J. Artif. Intell. Tools"},{"key":"9407_CR32","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G.: TPTP, TSTP, CASC, etc. In: Diekert, V., Volkov, M., Voronkov, A. (eds.) Proceedings of the 2nd International Symposium on Computer Science in Russia, number 4649 in Lecture Notes in Computer Science, pp. 6\u201322. Springer (2007)","DOI":"10.1007\/978-3-540-74510-5_4"},{"key":"9407_CR33","unstructured":"Sutcliffe, G.: The SZS ontologies for automated reasoning software. In: Sutcliffe, G., Rudnicki, P., Schmidt, R., Konev, B., Schulz, S. (eds.) Proceedings of the LPAR Workshops: Knowledge Exchange: Automated Provers and Proof Assistants, and The 7th International Workshop on the Implementation of Logics, number 418 in CEUR Workshop Proceedings, pp. 38\u201349 (2008)"},{"issue":"4","key":"9407_CR34","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. Reason. 43(4), 337\u2013362 (2009)","journal-title":"J. Autom. Reason."},{"key":"9407_CR35","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G.: The TPTP world - infrastructure for automated reasoning. In: Clarke, E., Voronkov, A. (eds.) Proceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, number 6355 in Lecture Notes in Artificial Intelligence, pp. 1\u201312. Springer (2010)","DOI":"10.1007\/978-3-642-17511-4_1"},{"issue":"1","key":"9407_CR36","first-page":"1","volume":"3","author":"G Sutcliffe","year":"2010","unstructured":"Sutcliffe, G., Benzm\u00fcller, C.: Automated reasoning in higher-order logic using the TPTP THF infrastructure. J. Formaliz. Reason. 3(1), 1\u201327 (2010)","journal-title":"J. Formaliz. Reason."},{"key":"9407_CR37","unstructured":"Sutcliffe, G., Fuchs, M., Suttner, C.: Progress in automated theorem proving, 1997\u20132001. In: Hoos, H., St\u00fctzle, T. (eds.) Proceedings of the IJCAI\u201901 Workshop on Empirical Methods in Artificial Intelligence, pp. 53\u201360 (2001)"},{"key":"9407_CR38","unstructured":"Sutcliffe, G., Pelletier, F.J.: Hoping for the truth\u2014a survey of the TPTP logics. In: Markov, Z., Russell, I. (eds.) Proceedings of the 29th International FLAIRS Conference, pp. 110\u2013115 (2016)"},{"key":"9407_CR39","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G., Schulz, S.: The thousands of models for theorem provers (TMTP) model library - first steps. In: Konev, B., Schulz, S., Simon, L. (eds.) Proceedings of the 11th International Workshop on the Implementation of Logics, number\u00a040 in EPiC Series in Computing, pp. 106\u2013121. EasyChair Publications (2016)","DOI":"10.29007\/7dg5"},{"key":"9407_CR40","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G., Schulz, S., Claessen, K., Baumgartner, P.: The TPTP typed first-order form with arithmetic. In: Bj\u00f8rner, N., Voronkov, A. (eds.) Proceedings of the 18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, number 7180 in Lecture Notes in Artificial Intelligence, pp. 406\u2013419. Springer (2012)","DOI":"10.1007\/978-3-642-28717-6_32"},{"key":"9407_CR41","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G., Schulz, S., Claessen, K., Van\u00a0Gelder, A.: Using the TPTP language for writing derivations and finite interpretations. In: Furbach, U., Shankar, N. (eds.) Proceedings of the 3rd International Joint Conference on Automated Reasoning, number 4130 in Lecture Notes in Artificial Intelligence, pp. 67\u201381 (2006)","DOI":"10.1007\/11814771_7"},{"issue":"1","key":"9407_CR42","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."},{"issue":"3","key":"9407_CR43","doi-asserted-by":"crossref","first-page":"307","DOI":"10.1023\/A:1015736313131","volume":"28","author":"G Sutcliffe","year":"2002","unstructured":"Sutcliffe, G., Suttner, C., Pelletier, F.J.: The IJCAR ATP system competition. J. Autom. Reason. 28(3), 307\u2013320 (2002)","journal-title":"J. Autom. Reason."},{"issue":"2","key":"9407_CR44","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1023\/A:1005806324129","volume":"21","author":"G Sutcliffe","year":"1998","unstructured":"Sutcliffe, G., Suttner, C.B.: The TPTP problem library: CNF release v1.2.1. J. Autom. Reason. 21(2), 177\u2013203 (1998)","journal-title":"J. Autom. Reason."},{"issue":"1\u20132","key":"9407_CR45","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1016\/S0004-3702(01)00113-8","volume":"131","author":"G Sutcliffe","year":"2001","unstructured":"Sutcliffe, G., Suttner, C.B.: Evaluating general purpose automated theorem proving systems. Artif. Intell. 131(1\u20132), 39\u201354 (2001)","journal-title":"Artif. Intell."},{"key":"9407_CR46","unstructured":"Sutcliffe, G., Zimmer, J., Schulz, S.: Communication formalisms for automated theorem proving tools. In: Sorge, V., Colton, S., Fisher, M., Gow, J. (eds.) Proceedings of the Workshop on Agents and Automated Reasoning, 18th International Joint Conference on Artificial Intelligence, pp. 52\u201357 (2003)"},{"key":"9407_CR47","doi-asserted-by":"crossref","unstructured":"Trac, S., Puzis, Y., Sutcliffe, G.: An interactive derivation viewer. In: Autexier, S., Benzm\u00fcller, C. (eds.) Proceedings of the 7th Workshop on User Interfaces for Theorem Provers, 3rd International Joint Conference on Automated Reasoning, volume 174 of Electronic Notes in Theoretical Computer Science, pp. 109\u2013123 (2007)","DOI":"10.1016\/j.entcs.2006.09.025"},{"issue":"1\u20132","key":"9407_CR48","first-page":"21","volume":"37","author":"J Urban","year":"2006","unstructured":"Urban, J.: MPTP 0.2: design, implementation, and initial experiments. J. Autom. Reason. 37(1\u20132), 21\u201343 (2006)","journal-title":"J. Autom. Reason."},{"issue":"2","key":"9407_CR49","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1007\/s10817-012-9269-y","volume":"50","author":"J Urban","year":"2013","unstructured":"Urban, J., Rudnicki, P., Sutcliffe, G.: ATP and presentation service for Mizar formalizations. J. Autom. Reason. 50(2), 229\u2013241 (2013)","journal-title":"J. Autom. Reason."},{"key":"9407_CR50","doi-asserted-by":"crossref","unstructured":"Urban, J., Sutcliffe, G., Pudlak, P., Vyskocil, J.: MaLARea SG1: machine learner for automated reasoning with semantic guidance. In: Baumgartner, P., Armando, A., Dowek, G. (eds.) Proceedings of the 4th International Joint Conference on Automated Reasoning, number 5195 in Lecture Notes in Artificial Intelligence, pp. 441\u2013456. Springer (2008)","DOI":"10.1007\/978-3-540-71070-7_37"},{"key":"9407_CR51","doi-asserted-by":"crossref","unstructured":"Van\u00a0Gelder, A., Sutcliffe, G.: Extending the tptp language to higher-order logic with automated parser generation. In: Furbach, U., Shankar, N. (eds.) Proceedings of the 3rd International Joint Conference on Automated Reasoning, number 4130 in Lecture Notes in Artificial Intelligence, pp. 156\u2013161. Springer (2006)","DOI":"10.1007\/11814771_15"},{"key":"9407_CR52","doi-asserted-by":"crossref","unstructured":"Verchinine, K., Lyaletski, A., Paskevich, A.: System for automated deduction (SAD): a tool for proof verification. In: Pfenning, F. (ed.) Proceedings of the 21st International Conference on Automated Deduction, number 4603 in Lecture Notes in Artificial Intelligence, pp. 398\u2013403. Springer (2007)","DOI":"10.1007\/978-3-540-73595-3_29"},{"key":"9407_CR53","unstructured":"Wisniewski, M., Steen, A., Benzm\u00fcller, C.: TPTP and beyond: representation of quantified non-classical logics. In: Benzm\u00fcller, C., Otten, J. (eds.) Proceedings of the 2nd International Workshop on Automated Reasoning in Quantified Non-Classical Logics, number 1770 in CEUR Workshop Proceedings, pp. 51\u201365 (2016)"},{"issue":"8","key":"9407_CR54","first-page":"773","volume":"C\u201325","author":"LA Wos","year":"1976","unstructured":"Wos, L.A., Overbeek, R.A., McCharen, J.D.: Problems and experiments for and with automated theorem-proving programs. IEEE Trans. Comput. C\u201325(8), 773\u2013782 (1976)","journal-title":"IEEE Trans. Comput."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-017-9407-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-017-9407-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-017-9407-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,15]],"date-time":"2025-06-15T13:00:29Z","timestamp":1749992429000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-017-9407-7"}},"subtitle":["From CNF to TH0, TPTP v6.4.0"],"short-title":[],"issued":{"date-parts":[[2017,2,17]]},"references-count":54,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2017,12]]}},"alternative-id":["9407"],"URL":"https:\/\/doi.org\/10.1007\/s10817-017-9407-7","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,2,17]]}}}