{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,2]],"date-time":"2025-08-02T19:10:46Z","timestamp":1754161846500,"version":"3.41.2"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031999833","type":"print"},{"value":"9783031999840","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T00:00:00Z","timestamp":1753833600000},"content-version":"vor","delay-in-days":210,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We use SMT technology to address a class of problems involving uninterpreted functions and nonlinear real arithmetic. In particular, we focus on problems commonly found in mathematical competitions, such as the International Mathematical Olympiad (IMO), where the task is to determine all solutions\u00a0to constraints on an uninterpreted function. Although these problems require\u00a0only high-school-level mathematics, state-of-the-art SMT solvers often struggle\u00a0with them. We propose several techniques to improve SMT performance in this setting.<\/jats:p>","DOI":"10.1007\/978-3-031-99984-0_9","type":"book-chapter","created":{"date-parts":[[2025,7,29]],"date-time":"2025-07-29T11:47:50Z","timestamp":1753789670000},"page":"150-163","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["SMT and\u00a0Functional Equation Solving over\u00a0the\u00a0Reals: Challenges from\u00a0the\u00a0IMO"],"prefix":"10.1007","author":[{"given":"Chad E.","family":"Brown","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0541-3889","authenticated-orcid":false,"given":"Karel","family":"Chvalovsk\u00fd","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3487-784X","authenticated-orcid":false,"given":"Mikol\u00e1\u0161","family":"Janota","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9361-1921","authenticated-orcid":false,"given":"Mirek","family":"Ol\u0161\u00e1k","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1710-1513","authenticated-orcid":false,"given":"Stefan","family":"Ratschan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,7,30]]},"reference":[{"key":"9_CR1","unstructured":"Art of problem solving. https:\/\/artofproblemsolving.com\/community\/c13_contest_collections"},{"key":"9_CR2","doi-asserted-by":"publisher","unstructured":"Alur, R., et al.: Syntax-guided synthesis. In: 2013 Formal Methods in Computer-Aided Design, pp.\u00a01\u20138 (2013). https:\/\/doi.org\/10.1109\/FMCAD.2013.6679385","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"9_CR3","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-24246-0_1","volume-title":"Frontiers of Combining Systems","author":"P Backeman","year":"2015","unstructured":"Backeman, P., R\u00fcmmer, P.: Free variables and theories: revisiting rigid E-unification. In: Lutz, C., Ranise, S. (eds.) FroCoS 2015. LNCS (LNAI), vol. 9322, pp. 3\u201313. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24246-0_1"},{"key":"9_CR4","doi-asserted-by":"publisher","unstructured":"Barbosa, H., et al.: cvc5: A versatile and industrial-strength SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems, TACAS. LNCS, vol. 13243, pp. 415\u2013442. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"9_CR5","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/978-3-319-10575-8_11","volume-title":"Handbook of Model Checking","author":"C Barrett","year":"2018","unstructured":"Barrett, C., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Model Checking, pp. 305\u2013343. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_11"},{"key":"9_CR6","doi-asserted-by":"publisher","unstructured":"Bhayat, A., Korovin, K., Kov\u00e1cs, L., Schoisswohl, J.: Refining unification with abstraction. In: Piskac, R., Voronkov, A. (eds.) LPAR 2023: Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Manizales, Colombia, 4\u20139 June 2023. EPiC Series in Computing, vol.\u00a094, pp. 36\u201347. EasyChair (2023). https:\/\/doi.org\/10.29007\/H65J","DOI":"10.29007\/H65J"},{"key":"9_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/11609773_28","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AR Bradley","year":"2005","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: What\u2019s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 427\u2013442. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11609773_28"},{"key":"9_CR8","unstructured":"Brown, C.E., Janota, M., Ol\u0161\u00e1k, M.: Symbolic computation for all the fun. In: Brown, C.W., Kaufmann, D., Nalon, C., Steen, A., Suda, M. (eds.) Joint Proceedings of the 9th Workshop on Practical Aspects of Automated Reasoning (PAAR) and the 9th Satisfiability Checking and Symbolic Computation Workshop (SC-Square), 2024 co-located with the 12th International Joint Conference on Automated Reasoning (IJCAR 2024). CEUR Workshop Proceedings, vol.\u00a03717, pp. 111\u2013121. CEUR-WS.org (2024). https:\/\/ceur-ws.org\/Vol-3717\/paper6.pdf"},{"issue":"1","key":"9_CR9","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/980175.980185","volume":"38","author":"CW Brown","year":"2004","unstructured":"Brown, C.W.: QEPCAD B: a system for computing with semi-algebraic sets via cylindrical algebraic decomposition. SIGSAM Bull. 38(1), 23\u201324 (2004). https:\/\/doi.org\/10.1145\/980175.980185","journal-title":"SIGSAM Bull."},{"key":"9_CR10","volume-title":"Numerical Analysis","author":"RL Burden","year":"2015","unstructured":"Burden, R.L., Faires, J., Douglas, A.: Numerical Analysis, 10th edn. Cengage Learning, Boston (2015)","edition":"10"},{"key":"9_CR11","doi-asserted-by":"publisher","unstructured":"Caviness, B.F., Johnson, J.R. (eds.): Quantifier Elimination and Cylindrical Algebraic Decomposition. Springer, Wien (1998). https:\/\/doi.org\/10.1007\/978-3-7091-9459-1","DOI":"10.1007\/978-3-7091-9459-1"},{"issue":"3","key":"9_CR12","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1016\/S0747-7171(08)80152-6","volume":"12","author":"GE Collins","year":"1991","unstructured":"Collins, G.E., Hong, H.: Partial cylindrical algebraic decomposition for quantifier elimination. J. Symb. Comput. 12(3), 299\u2013328 (1991). https:\/\/doi.org\/10.1016\/S0747-7171(08)80152-6","journal-title":"J. Symb. Comput."},{"key":"9_CR13","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/S0747-7171(88)80004-X","volume":"5","author":"JH Davenport","year":"1988","unstructured":"Davenport, J.H., Heintz, J.: Real quantifier elimination is doubly exponential. J. Symb. Comput. 5, 29\u201335 (1988). https:\/\/doi.org\/10.1016\/S0747-7171(88)80004-X","journal-title":"J. Symb. Comput."},{"key":"9_CR14","unstructured":"Dekoninck, J., Balunovi\u0107, M., Jovanovi\u0107, N., Petrov, I., Vechev, M.: MathConstruct: challenging LLM reasoning with constructive proofs. In: ICLR 2025 Workshop: VerifAI: AI Verification in the Wild (2025). https:\/\/openreview.net\/forum?id=nHW2tiGMrb"},{"issue":"3","key":"9_CR15","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). https:\/\/doi.org\/10.1145\/1066100.1066102","journal-title":"J. ACM"},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-642-02658-4_25","volume-title":"Computer Aided Verification","author":"Y Ge","year":"2009","unstructured":"Ge, Y., de Moura, L.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 306\u2013320. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_25"},{"key":"9_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"534","DOI":"10.1007\/978-3-030-67067-2_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"J Hoenicke","year":"2021","unstructured":"Hoenicke, J., Schindler, T.: Incremental search for conflict and unit instances of quantified formulas with e-matching. In: Henglein, F., Shoham, S., Vizel, Y. (eds.) VMCAI 2021. LNCS, vol. 12597, pp. 534\u2013555. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-67067-2_24"},{"key":"9_CR18","doi-asserted-by":"publisher","unstructured":"Hozzov\u00e1, P., Kov\u00e1cs, L., Norman, C., Voronkov, A.: Program synthesis in saturation. In: Pientka, B., Tinelli, C. (eds.) Automated Deduction - CADE 29 - 29th International Conference on Automated Deduction. LNCS, vol. 14132, pp. 307\u2013324. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-38499-8_18","DOI":"10.1007\/978-3-031-38499-8_18"},{"key":"9_CR19","doi-asserted-by":"publisher","unstructured":"Hozzov\u00e1, P., Amrollahi, D., Hajdu, M., Kov\u00e1cs, L., Voronkov, A., Wagner, E.M.: Synthesis of recursive programs in saturation. In: International Joint Conference on Automated Reasoning IJCAR (2024). https:\/\/doi.org\/10.1007\/978-3-031-63498-7_10","DOI":"10.1007\/978-3-031-63498-7_10"},{"key":"9_CR20","doi-asserted-by":"publisher","unstructured":"Janota, M.: Allfun (2025). https:\/\/doi.org\/10.5281\/zenodo.15554870","DOI":"10.5281\/zenodo.15554870"},{"key":"9_CR21","doi-asserted-by":"publisher","unstructured":"Janota, M., Barbosa, H., Fontaine, P., Reynolds, A.: Fair and adventurous enumeration of quantifier instantiations. In: Formal Methods in Computer-Aided Design, pp. 256\u2013260. IEEE (2021). https:\/\/doi.org\/10.34727\/2021\/ISBN.978-3-85448-046-4_35","DOI":"10.34727\/2021\/ISBN.978-3-85448-046-4_35"},{"key":"9_CR22","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. 8044, pp. 1\u201335. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_1"},{"key":"9_CR23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-7643-8749-5","author":"M Kuczma","year":"2009","unstructured":"Kuczma, M.: An introduction to the theory of functional equations and inequalities. Birkh\u00e4user Basel (2009). https:\/\/doi.org\/10.1007\/978-3-7643-8749-5","journal-title":"Birkh\u00e4user Basel"},{"key":"9_CR24","doi-asserted-by":"publisher","unstructured":"Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Complete functional synthesis. In: PLDI, pp. 316\u2013329. ACM (2010). https:\/\/doi.org\/10.1145\/1806596.1806632","DOI":"10.1145\/1806596.1806632"},{"key":"9_CR25","doi-asserted-by":"crossref","unstructured":"Meurer, A., et\u00a0al.: SymPy: symbolic computing in Python. PeerJ Comput. Sci. 3, e103 (2017). https:\/\/www.sympy.org","DOI":"10.7717\/peerj-cs.103"},{"key":"9_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"9_CR27","unstructured":"Musil, V.: Funkcion\u00e1ln\u00ed rovnice (2024). https:\/\/prase.cz\/library\/FunkcionalniRovniceVM\/FunkcionalniRovniceVM.pdf, online library of the Matematick\u00fd koresponden\u010dn\u00ed semin\u00e1\u0159 PraSe (PRA\u017esk\u00fd SEmin\u00e1\u0159), Downloaded 8 March 2024"},{"key":"9_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/978-3-030-72013-1_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Niemetz","year":"2021","unstructured":"Niemetz, A., Preiner, M., Reynolds, A., Barrett, C., Tinelli, C.: Syntax-guided quantifier instantiation. In: TACAS 2021. LNCS, vol. 12652, pp. 145\u2013163. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_8"},{"key":"9_CR29","unstructured":"Petrov, I., et al.: Proof or bluff? Evaluating LLMs on 2025 USA math Olympiad (2025). https:\/\/arxiv.org\/abs\/2503.21934"},{"key":"9_CR30","doi-asserted-by":"publisher","unstructured":"Ratschan, S.: Deciding predicate logical theories of real-valued functions. In: Leroux, J., Lombardy, S., Peleg, D. (eds.) 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023), LIPIcs, vol.\u00a0272, pp. 76:1\u201376:15. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2023). https:\/\/doi.org\/10.4230\/LIPIcs.MFCS.2023.76","DOI":"10.4230\/LIPIcs.MFCS.2023.76"},{"key":"9_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-89960-2_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Reger","year":"2018","unstructured":"Reger, G., Suda, M., Voronkov, A.: Unification with abstraction and theory instantiation in saturation-based reasoning. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 3\u201322. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89960-2_1"},{"key":"9_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-319-89963-3_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Reynolds","year":"2018","unstructured":"Reynolds, A., Barbosa, H., Fontaine, P.: Revisiting enumerative instantiation. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 112\u2013131. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_7"},{"key":"9_CR33","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/978-3-642-38574-2_26","volume-title":"Automated Deduction \u2013 CADE-24","author":"A Reynolds","year":"2013","unstructured":"Reynolds, A., Tinelli, C., Goel, A., Krsti\u0107, S., Deters, M., Barrett, C.: Quantifier instantiation techniques for finite model finding in SMT. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 377\u2013391. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_26"},{"key":"9_CR34","doi-asserted-by":"publisher","unstructured":"Reynolds, A., Tinelli, C., de\u00a0Moura, L.M.: Finding conflicting instances of quantified formulas in SMT. In: Formal Methods in Computer-Aided Design, FMCAD, pp. 195\u2013202. IEEE (2014). https:\/\/doi.org\/10.1109\/FMCAD.2014.6987613","DOI":"10.1109\/FMCAD.2014.6987613"},{"key":"9_CR35","unstructured":"Robinson, J.A., Voronkov, A. (eds.): Handbook of Automated Reasoning (in 2 volumes). Elsevier and MIT Press (2001). https:\/\/www.sciencedirect.com\/book\/9780444508133\/handbook-of-automated-reasoning"},{"issue":"5\u20136","key":"9_CR36","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1007\/S10009-012-0223-4","volume":"15","author":"S Srivastava","year":"2013","unstructured":"Srivastava, S., Gulwani, S., Foster, J.S.: Template-based program verification and program synthesis. Int. J. Softw. Tools Technol. Transf. 15(5\u20136), 497\u2013518 (2013). https:\/\/doi.org\/10.1007\/S10009-012-0223-4","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"9_CR37","doi-asserted-by":"publisher","unstructured":"Tarski, A.: A Decision Method for Elementary Algebra and Geometry. University of California Press, Berkeley (1951). https:\/\/doi.org\/10.2307\/jj.8501420, also in\u00a0[11]","DOI":"10.2307\/jj.8501420"},{"key":"9_CR38","doi-asserted-by":"publisher","unstructured":"Vale-Enriquez, F., Brown, C.W.: Polynomial constraints and unsat cores in Tarski. In: Davenport, J.H., Kauers, M., Labahn, G., Urban, J. (eds.) ICMS 2018. LNCS, vol. 10931, pp. 466\u2013474. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96418-8_55, https:\/\/www.usna.edu\/Users\/cs\/wcbrown\/tarski\/index.html, code obtained from https:\/\/github.com\/chriswestbrown\/tarski","DOI":"10.1007\/978-3-319-96418-8_55"},{"issue":"1\u20132","key":"9_CR39","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0747-7171(88)80003-8","volume":"5","author":"V Weispfenning","year":"1988","unstructured":"Weispfenning, V.: The complexity of linear problems in fields. J. Symb. Comput. 5(1\u20132), 3\u201327 (1988). https:\/\/doi.org\/10.1016\/S0747-7171(88)80003-8","journal-title":"J. Symb. Comput."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 30"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-99984-0_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,29]],"date-time":"2025-07-29T11:47:52Z","timestamp":1753789672000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-99984-0_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031999833","9783031999840"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-99984-0_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"30 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Stuttgart","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.dhbw-stuttgart.de\/cade-30\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}