{ "cells": [ { "attachments": {}, "cell_type": "markdown", "id": "1c1da340-c836-4acc-8b7d-978cc917ebb2", "metadata": {}, "source": [ "# IJCAR 2026 Short Paper Examples\n", "\n", "Below are code cells corresponding to the figures of the IJCAR 2026 short paper submission, plus additional details." ] }, { "attachments": {}, "cell_type": "markdown", "id": "810d31fe-bc75-499d-ad76-97e5b23d4889", "metadata": {}, "source": [ "## Figure 1\n", "\n", "Parsing a fuzzy sort taxonomy" ] }, { "cell_type": "code", "execution_count": 1, "id": "76d7d0e0-d953-40f3-b5bf-fe7fedf6c2b6", "metadata": { "tags": [] }, "outputs": [], "source": [ "from fosf.parsers import parse_taxonomy\n", "ftax_str = \"\"\"\n", "# Fuzzy subsumption declarations\n", "director < person.\n", "slasher < thriller (0.5), horror.\n", "thriller, horror < movie.\n", "# Fuzzy instance declarations\n", "{h, 0.7/p} < slasher.\n", "{p} < horror, thriller.\n", "\"\"\"\n", "ftax = parse_taxonomy(ftax_str)" ] }, { "cell_type": "code", "execution_count": 2, "id": "dec3c5c7-d0a2-4be5-9e85-fa3c0f35fc45", "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "\n" ] } ], "source": [ "print(type(ftax))" ] }, { "cell_type": "markdown", "id": "a80840d7-043b-42bd-98e4-808fb14129ce", "metadata": {}, "source": [ "Drawing the fuzzy taxonomy" ] }, { "cell_type": "code", "execution_count": 3, "id": "b2290ccc-1f0d-4f14-9e5b-1dbc651adaf3", "metadata": {}, "outputs": [ { "data": { "image/png": "iVBORw0KGgoAAAANSUhEUgAAAOgAAAEqCAYAAAAf/hxzAAAABmJLR0QA/wD/AP+gvaeTAAAgAElEQVR4nOydd1QUVxvGn91laYtUKQICooIUFRUVK/YSE3vvvUVjisYvJpZYoqIGjQULFoy9xhZ7TQy2YEFEEZCiFEH6sixb3u+PFZRQpOzuLMv8zuFwmHLfZ4Z55s7Mvfe9HCIisLCwaCLLuEwrYGFhKR3WoCwsGgxrUBYWDUaHaQGailwux8uXLxEXF4eMjIxy72dqagoHBwc0bNgQXC57/2OpGqxB/0NCQgJ+/fVXHDp0CG/evKl0OXZ2dhg2bBi+++472NraKlUjS82BvcW/h4iwbt06uLq64ujRo5g8eTIePHiAtLQ0EFG5f9LT0/HgwQNMnjwZx48fh6urK9atWwf2YzlLpSAWEolENHz4cOLz+bRs2TISiURKK3f58uWkq6tLw4YNo9zcXKWUy1JjWMqhGn5rl8vlGDZsGK5evYpjx46hS5cuSo9x/fp1DBo0CJ06dcKxY8fYd1OW8sK2gy5btgxnzpzBqVOnVGJOAOjcuTPOnDmDP//8E0uXLlVJDBYthek6nEkiIiJIV1eXfvvtN7XE27RpE+nq6tKLFy/UEo+l2lOzH3FHjRqF0NBQPHz4EDweT+XxZDIZmjdvDnd3dxw8eFDl8ViqPTX3EVcoFOLUqVOYPXu2WswJADweD7Nnz8Yff/yBzMxMtcRkqd7UWIPevHkTQqEQAwcOVGvcQYMGQSwW46+//lJrXJbqSY01aExMDCwtLWFhYaHWuGZmZrC0tERMTIxa47JUT2qsQVNSUlC7dm1GYltbWyM5OZmR2CzVixprUCICh8MptjxPLEOv6WdVGrukuCwsJVFjDVoae8+8QHKqiGkZLCwA21m+KFsOPcX6358gMzsf3Safhp21EYJWdAGRYt3B8y+hr8tDepYYrvXMsGSmN1wcTXHlzmssWH8XaZl56OPriOv33uDtOxEau1jglzmt0dLTiulDY6mmsDXoR8wc7gmfptawtRLgSmBfBK1Q9CxaFRiCNbsfYefSzrgS2Bd3Dw6CHp+L3tPP4W2aCN187NGumQ1yxVJ8N84Lj48Pwz/7B0IuJwz8+gLSs8RMHxpLNYU16CfIE8uw6eBTDOhaD65OpgAAHR4XS2a2xLuMPOz543nhtjo8LhzqGIHDAZztjbH62zbIFkqw6+TzMiKwsJQOa9BPEB6dDqFIUmjOAhxta8HIkI9/n6WUum9zt9rgcTkIj0pXg1IWbYQ16CfIzMkHAOjrFe9tJDDQKVxfElwuB7UEukjNYD86sVQO1qCfwMRIFwAgEsuKrcvJlcLUSK/UfWVyQpYwH7ZWApVqZNFeWIP+h/+2UbrVN4PAgI+ImKJ5ieIScyAUSdDCw7LUskIj3kEuJzR3K30bFpayqLEGNTIyQk5OTrHlZsZ6SEwVIjElF3liGXR4HMwe6YmTV18hIlZhUqlMjp8D7qO2qT7G93ctsXypTI5VgQ9hZy3A6C9ciqzLycmBkZGRio6MRZuose2gDg4OSEhIgEQiAZ/PL1w+eaAbrt19jVYjjsGjgTn2/tIV8yc1h8CAj/E/XkMtQ11k5ojRwMEE57d9Dkszg8J9xWIZhs+9jHypDLEJ2XCtZ4Yzmz6Dvu6H91epVIr4+Hg4Ojqq/ZhZqh811qCtWrWCTCbDtWvX0LNnz8Llng3N8eTEsGLbzx7VGLNHNS6zTIGhDg6t7V7mNteuXYNUKkXLli2roJ6lplBjH3GdnJzg4+ODnTt3Kq1MqezTY9937dqFVq1aoX79+kqLy6K91FiDAsC8efNw7NgxtY3NDA4OxpEjR/D999+rJR5L9adGpzwBgJ49e+LVq1cIDg6u9NjQY5ej4LfzEV69ycKE/o0wpGf9Yv1v09LS0KZNGzg4OODy5ctKUs+i5Syr8QZNTk5G69atUbduXZw5cwampqbl2KtiZGZmom/fvoiJicHdu3dhY2Oj9BgsWknNzUlUgLW1Nc6dO4eYmBi0bdsWYWFhSi3/6dOnaNOmDaKionDu3DnWnCwVosYbFAA8PDxw9+5dmJqawsvLC7Nnz66yUcPCwjB79mw0a9YMJiYmuHfvHjw9PZWmmaVmUOMfcT9GLpdj9+7dWLp0KeLi4lC/fn3Ur18fJiYm5S4jKysLkZGRiIqKgoODAxYtWoQJEyaw2eRZKgP7DloSRISbN2/izJkzyMzMRFZWVrn3NTY2hqOjI+rXr4/hw4ezxmSpCqxBS+Ldu3cYNmwYxo0bhzFjxlSqjFmzZkEoFGLTpk0QCNjO8iyVgv1I9F+ePHkCLy8vXL16tUr9Za2srLBnzx54eXnh6dOnStXIUnNgDfoRR48eRevWrZGUlAQAVar5rKyswOVyERMTgxYtWmDHjh1KVMpSU2AN+v7j0IIFCzBs2DCIxWJIpVLg/YiXymJlZQW5XA6pVIr8/HxMmzYNw4YNq9D7LAtLjTdoZmYmPv/8c/j5+RXOkl1AVQ36MUSEkydPokmTJggJCamSZpaaQ4026PPnz9G8eXNcuXIFMpmsyLAzKNmgOjo6kEgkiI+Ph4+PDzZu3Aj2+xzLp6ixBj1z5gy8vb0RHR0NmUyRzkQikRTZpqrvoB8jlUqhq6tbGOerr75Cv379kJ7OJhRjKZ0aZ1AiwvLly9GvXz8IhUIAQI8ePTB79mzw+Xzo6X3IMVSVGtTU1LSwRubxeLC2tsb48ePx22+/wd7eHnh/k/D09ERwcHCVj4tFS2F0/mA1k52dTQMGDCAABIA6depEwcHBlJ+fT87OzjR58mRq2rQpASAOh0NyubxK8aytrQkA2djY0NatW0lXV5ciIiJIIpHQgQMHyNPTkwAQj8ej1atXVzkei9axtMYYNDIyktzd3QkAtW7dmm7cuFG4bseOHaSrq0uvXr2isWPHEgAyMDCocswCA7Zq1YokEgl5eHjQwIEDi2xz4cIF6tixIwGg3r1709u3b6scl0VrWFojHnEvX76MVq1aQSAQ4MKFC7hz5w58fX0BAPn5+VixYgUmTJgAJycnNGrUCABgYGDwiVI/ja2tLQCgQYMG0NHRgZ+fH06cOFFkgHjPnj1x8+ZN3Lt3DwKBAC1atMDNmzerHJtFS2D6FqFqtm3bRl5eXnTkyJESHyEDAgIKa08iohMnThAAqlu3bpVjjxs3jgDQDz/8ULisR48e1KxZM5LJZCXuExUVRd9++y2tXr2apFJplTWwVGu0twYViURYsWIFTExM8O+//2LIkCHFct6KxWKsXbsWw4cPh5OTEwDAzc0NqOIHogIKvuTWrVu3cNmaNWugo6ODgwcPlriPs7Mz1q1bh7Fjx+LatWvIzc2tsg6W6otWZvUjIkRHR+N///sfeLziUzYUEBgYiDdv3mDRokWFy+rXrw8ej6dUgzo4OBQua9KkCZo0aYL//e9/GDBgAAwNDUvc18bGhh3czaKdzSwcDgceHh5lmjMvLw+rVq3CtGnTimTY4/P5cHBwqNAY0NIoyaAAsGLFCmRmZmLDhg1VjsGi3WilQcvD9u3bkZqainnz5hVb17RpUxgbG1c5hrW1NVCCQa2trTF37lysXLmysGM+C0tJ1EiD5uXlwc/PDzNnzoSdnV2x9e7u7qhVq1aV41hZWcHU1LTE2njevHkwNTXFzz//XOU4LNpLjTToli1bkJGRUWp+2kaNGintHfS/tWcBBgYGWLp0KXbs2MGOF2UplRpnUJFIhHXr1mHmzJmFj6D/xc3NTWkGLWsOlrFjx8LLywvz58+vciwW7aTGGXTTpk3IzMzE3LlzS92mUaNGSnnE5fP5aNKkSanruVwu1q5diz///BOXLl2qcjwW7aNGGVQoFGLt2rX46quvio02+RgjIyO4uLiUur4ieHt7l7m+U6dO+OKLLzBv3rzCUTUsLAXUKINu3LgRubm5+Oabbz65rbJmH/uUQfG+80J4eDiCgoKUEpNFe6gxWf1ycnLg7OyMadOmYdmyZUzLKcasWbNw7NgxvHz5UimP1yxaQc3J6rd+/Xrk5+eXq/ZkgiVLliAvLw9r165lWgqLBlEjDJqVlQV/f398/fXXMDc3Z1pOidSuXRsLFizAmjVrEB8fz7QcFg2hRhjU398fMpkMc+bMYVpKmXz99dewtbUt0jeYpWaj9QYt6PP63XffwczMjGk5ZaKrq4vly5dj7969+Pfff5mWw6IBaP1HokWLFmHjxo149eqVSub+VDZEhA4dOoDP5+P69etMy2FhFu3+SJSRkYGNGzcW9nutDnA4HKxduxY3b97E2bNnmZbDwjBabdA1a9aAx+Nh9uzZTEupED4+Phg0aBDmzp1bLBUoS81Caw367t07bNy4Ed9//321bFf08/NDTEwMO6dLDUdrDbpmzRro6elhxowZTEupFPXq1cOXX36JJUuWIDMzk2k5LAyhlQZNTU3Fli1b8L///a9a1p4FLFy4EHK5HCtXrmRaCgtDaKVBV61aBYFAUG1rzwJMTU2xcOFC+Pv7Iyoqimk5LAygdQZNSkpCQEAA5s+fX2pCrurEzJkz4eTkhIULFzIthYUBtM6gq1evhomJCaZNm8a0FKXA5/OxevVqHDp0CP/88w/TcljUjFZ1VEhMTET9+vXh5+eHWbNmMS1HqXTr1g25ubm4fft2sfy+LFqLdnVUWLlyJczMzDBp0iSmpSidNWvW4O7duzh+/DjTUljUiNYYNCEhAYGBgfjpp5+UMq+KptGsWTOMHDkS33//PcRiMdNyWNSE1hh0+fLlsLS0xMSJE5mWojJWrVqF5ORkbN68mWkpLGpCKwwaFxeHXbt24ccffywyAa+2YWdnh6+//hrLli3Du3fvmJbDoga0wqArVqyAjY0Nxo8fz7QUlfPDDz9AX19fI9O2sCifam/Q2NhY7NmzB4sWLYKuri7TclSOkZERlixZgi1btiAiIoJpOSwqpto3s0yePBk3btxAeHg4+Hw+03LUgkwmg5eXFxo2bIgTJ04wLYdFdVTvZpaoqCjs3bsXCxcurDHmBAAejwc/Pz+cPHkS165dY1oOiwqp1jXo+PHjcfv2bYSHh0NHRyunOi2Tnj17IiUlBQ8ePACXW63vtSwlU31r0MjISOzfvx+LFy+ukebE+2RooaGhpc7WzVL9UeqVLZVKERkZibi4OJWPYTx58iSsra3B5/Nx9OjRMrflcDiwsbGBk5MT7O3tVapLWbx58wavXr1CUlISynrI8fX1xapVq1T+gczExAQODg5o0KBBjb0hMgIpgefPn9P06dPJwsKCAGj0j4eHB61atYqys7OVcehKJScnh1atWkWenp6Mn6fSfiwsLGjatGkUHh7O9OmqCSytkkHz8vJo7ty5xOfzyc3Njfz8/OjRo0eUnp6uPIlKQC6X05s3b+jatWs0a9YsMjU1JTs7Ozp+/DjT0go5duwY2dnZkampKc2aNYuuXbtGb968IblczrQ0IiLKyMigR48ekZ+fH7m7uxOfz6e5c+dSXl4e09K0mcobNDU1lTp27EgmJia0detWkkqlypWmQlJSUmjy5MnE4XBo0aJFjJpALpfT4sWLicPh0OTJkyklJYUxLeVFKpXStm3byMTEhDp06FAtNFdTKmdQoVBI3t7e5OTkRE+fPlW+LDWxY8cO4vP5tHDhQsY0LF68mPh8Pu3YsYMxDZUlLCyM6tWrRy1atCChUMi0HG2kcgYdPnw41a5dmyIjI5UvSc0EBgYSh8Oho0ePqj32sWPHiMPhUGBgoNpjK4uoqCiytLSkYcOGMS1FG6m4QS9cuEAA6NKlS6qRxABTp04lW1tbysrKUlvM7OxssrW1palTp6otpqq4fPkyAaDz588zLUXbqLhBmzVrRoMGDVKNHIZITU0lc3NzWr58udpirlixgszMzCg1NVVtMVXJoEGDyMvLi2kZ2sbSCnVUePbsGR4+fKixc2xWFgsLC4wZMwb79u1TW8z9+/dj7NixsLCwUFtMVfLNN9/g0aNHCA0NZVqKVlEhg/7555+oU6cO2rZtqzpFDDF48GA8f/4cr169Unms2NhYPHv2DIMGDVJ5LHXRtm1b2Nra4sKFC0xL0SoqZNCYmBi4uLhoZdKqRo0aAe+PUdUU3ARcXV1VHquiJKbkon7v/Vi46V6F9uNwOHBxcVHLDa4mUSGDvn37FpaWlqpTwyC1a9cGl8tFcnKyymOlpKQAgEaeSw4H0OFxwONW/CZsbW2tlvNXk6hwp0ptrD0L4HA4ZfZ7VRYFMTTxXNrUNsSLsyMrta8mHk91p9qOZmFhqQlUeVjC1iNhWLH9X3jUN4exkS4ehqciN0+Krj528Pu2DWxqK6ZfSM3Iw48b7uJheCpMaunCQF8Hq772gXt9M2w6EIoN+0LRwt0SC6Y2x69Bj/Ek4h1Cjg7B7j+eI+jUCxjq6+BdRh4aN7RA4NJOAIBsoQRLtz7AXyGJMDLQQXqWGJ1b2WHxjJaoJeAj8Hg4Vu98CLf6Zhjc3Rl7/niBZ1FpaOhoiu1LfOHmbFb1M6gkImIzsDTgAc7ejIX//Hb4NywFF/6OAwD07eyE6cM8sPvkc5z/Ow7J70To2KIOdi7tDCPDDwPVLwe/xro9j5CXL0NevgzGhnzMneCFHm3rYu/pF1iy5T7Ss8SYNNANM4d7wtneGPeevkXgsWe4cDseP05tgYS3QgQeD0dXHzvs/aVrYdnHL0fD//fH0NXhQSqTo4+vI74b1xQ6PPYer1Iq0igzZMgQGjJkSLHl3kOPUq/pZ+ldRh5JZXL6698Ecu61j3pOPUNERHI5UecJp6jThD8oVyQhIqKvV/1NDXrvL/y759Qz5Nb3IH2/7h/afTKc2o85ScGPkqh2+12U8FbRjUwkltKw7z50kPhsxlnqPOEUZeXkExFR8rtcajnsGPWafrZwm55Tz1CzwUfobmgyJbwV0q0HCWTXJYgGfX2h2HHweDw6cOBARU5JpTh8+DCVdOr/+jeBTHwCadGme/Qg7C09ffmOpv18g0x8Aulbv9t060EChUelkd+uh2TiE0gBhz50s7xx/w2Ztd1Jxy5FFS4LOPyUTNsE0rW7r4mIaGVgCJn4BNLVO6+LxA04/JQWbLhT+LfXoCM05ocrhX+f/zuWTHwC6eTVaCIiik3IJuuOu2nj/idFyhk+fDgNHDhQKeeIhajC7aBlYWasB3MTPfC4HLRvXgezRzbGnSfJuBuajDuPkxASnoKpg91hoK+otIf1boCUdBHOv68lAMDW0hCrv22D8f0bYfsSXzyNTAOXw4GhgWIffV0eNv7YHgAQ/CgJtx8m4csRnqglUNQiVuYGmDO6MYIfJSH4UVJhueYmemjlaYU6lobo0KIOOreyQ/irdGUdutJp42WNFu6W8Ghgjv9Nag4AcK9vhg4t6qCRsxnmjveCHp+Hl3EfxtyuC3qM+vbGGNTduXDZ9KEesLc2gv/vTwAAEwc0gi6fix3HnxWJ9/uZCEwa6Faqni2HwuBQxwj9u9QDADjUMYJPU2vsPc0mLVM1Kns+aelpBQAIj0rH4xeKHK717I0L19d5/+gbk5Bd4v5uzmZo3cQKMjmh66TT2P3Hc2Rki2Fppsga/yBM8SXU1cm0yH4eDcyLrC8JAz0eJBJ5FY9QPRTc0PI/0svhAHp6PORLZIXLHoS9hct/zgUAeNQ3x4Owt8D7G9iArs64eDse8Uk5AID7T9+iTm1DOH/0v/kvj5+nFltvU9sQsaX871iUh8qGxpvWUozwT83IQ8GH0QXr78JAn1e4TbtmNjA3Lj3RdOOGFti3qitWBobgm9W38YP/HXw7rim+n9gMmTn5AAB9PV6RfQTv38myhPmqOCyNRCqTI1ckhYFe8X+nwFAHuSIpZHICj8vB9KEeOHwhErtOPsfiGd4IOvUCkweXXnsCQE6uBE9fpqHPzHNFlnt7al4zkbahMoOmZSrmD7GzEhSayX9+OzR1rVjXtl7tHdCrvQMi4zKxaPN9/LIjBO2a1YGJkeIGIBJLi2wvzJUAQOH6moAOjwtDAx3k/udcAIAwVwqBAb+wXbOZW2208rTC3tMv8OUIT/z7LAW//dC+zPJrCXTh7WmFQ2u6q+wYWEpGZY+4j1+kgsMBvBrVRuOGFoXLKsKtBwnIFSkuugYOJghc0gkcjuKLZ8vGikfoiJiiuY+eRSneLb09rJR0JNWDVp5WeBmTUWx5WFQavD2K1nTThnrgXUYexi24iuG9G4D7iU4Jng3N8fRlGuTyapsAstpSIYMKBALk5OR8cruk1FxsP/YM/TrXg5uzGdo0tYZHA3P8siMEf4ckQiYnyOSE+KQciPKK3/ULePziHXaeCC/8OzI+ExwOB83dLOHTxBrtmtlg88GnyHlfa6Zm5OG3/U/QrpkNfJpaV+TQIBKJIJfLYWRkVKH9KkNBDKFQqLQyvxnbFFGvs3DiSnThsh3HnuHNWyG+Hde0yLb9ujihjqUh/g1LwejPXT5Z9tTB7nidnIP5/nfwLiMPeP/YW/AeW0BOTg4EAoHSjomlgo+4jo6OuH//fonrQp6lYOh3l5CbJ0XCWyF6tXPAkpktAQBcLgfH/Xti8eb7GP/jNeSIJLC1FKB98zpYPrsVdh4IRVR8FuREWLTpHqYOcYe9tREaOZvh54D7OH4lGiZGusgWSrBtsW/hY/JBv+74OeABuk0+DdNaekjPEsPX2xYLp3sDAAKPhxeW67frIb6f2Ax7/niO+09TkJWTj192hGDBFMVX0piYGBARHB0dq3pOP4mDgwPwvtO8u7s78L4ddOuRMADAzuPh0OFxYWspwJZDTwEAJ65Ew8xYD51a2mLjgVCI8qQIfpyMQ+cjMbx3A/h62+KgX3es3fMImw48hVQmh6G+Do6s6wFfb9si8XV4XEwa6IbIuExYmOoXLn8Zl4k9fzzH2zQRHoanYmnAA8wa2Rh9Ozth22JfbDrwFO59D6GWgI8GDiaYNbIx6tp8uKHFxMSgWbNmKj9/NYqKNMqcPXuWuFwuxcXFFVnuPfRokXaz6oi/vz+ZmJioJQlWXl4emZqakr+/v8pjqYu4uDjicrl0+vRppqVoExVrB+3evTvMzMywe/fuYuuksur7fiKXy7Fnzx4MHDhQLdMX6unpYeDAgdizZw/k8urR3PMp9uzZA1NTU/Ts2ZNpKVpFhQyqq6uLOXPmYO3atUhMTFSdKjUTFBSEsLAwtQ5E/+abbxAWFoagoCC1xVQViYmJWLNmDebMmVMjZphTKxWtc3Nzc8nZ2Zm6detG+fn5tDIwhOy7BpF7v4O0aNM9SkypXtndXrx4Qebm5vTVV1+pPfZXX31FZmZm9OLFC7XHVhYSiYS6d+9Ozs7OlJuby7QcbaNyWf1CQkJIIBDQuHHjSCKRKF+WmoiLiyMXFxdq3bo1iUQitccXiUTk4+NDDRo0oNjYWLXHryoSiYQmTJhAAoGAQkJCmJajjVQ+cfWff/5JAoGAunfvTomJicqVpQauX79ONjY21KRJE0b1JyUlUZMmTcjGxoZu3LjBmI6KkpSURD169CCBQEDnzp1jWo62UrWpH/79919ycnIiY2NjWrFiBb1580Z50lTE3bt3acSIEcThcKh///5qTbVZGllZWdS/f3/icDg0YsQIunv3LtOSSuXNmze0YsUKMjY2JicnJ7bmVC1Lqzw/qEgkgp+fHzZs2IDMzEw0btwYjo6OavkaWhEyMjLw4sULxMXFwd3dHStXrkTfvn2ZllWE06dP44cffsCzZ8/g4OAAV1dXmJoW7wDPBGKxGHFxcXjy5AmMjY0xZ84czJ8/HwYGBkxL02aWKW0CX7FYjPPnz+PevXuIj4+HWCyucpkikUhpF4CJiQnq1auHXr16oXnz5kopU1WEhITgwoULePXqlVKmcazseczNzYVMJkOtWrWgq6sLBwcHtGrVCr1799a4G7CWojyDKpuoqChMnz4dly9fZlpKtebSpUs4cuQIAgMDK7xvVlYW6tSpg0aNGmHChAkYPnw4ateurRKdLCWyTCnzg6qCcePGEYfDoWfPnjEtpVrTrVs34vP5lf4QNmHCBAJAPB6PeDwe9e7dmw4fPszIV+8aSNU+EqmK6Oho4vF4xOFwaM6cOUzLqbaEhoYSh8MhDodDP/30U6XKCA4OLjKBb8H/xdDQkCZMmEA3btwgmUymdO0sRBpr0EmTJhGfzycAZGRkRDk5OUxLqpaMGzeu8DwaGxtX+jw2atSIOBxOsdm2dXR0CABZW1vTDz/8QGFhYUo/hhqO5hk0Jiam8B8PgLhcLu3cuZNpWdWOhISEQnMW1HybN2+uVFm//fYb8Xi8YgYt6adJkybk7+9PSUlJSj+mGojmGXTatGmkq6tbxKDsrFkVZ8GCBUUMyuFwyMnJqVKPo2lpaUX+JwDIy8uLTpw4Qf7+/jRz5kzq3Lkz2draEpfLLaxde/fuTfv372cn9608VW8HVSavX7+Gs7MzJBIJ+Hw+ZDJZ4WiP+/fvw9vbm2mJ1QKhUAhbW1tkZWWBz+dDKpUWZrM/efIk+vfvX+Eyx4wZg8OHD4PD4aBnz564desW2rZtixMnTkBf/8OYUrFYjOjoaERERODly5eIjIxEUlISGjdujE6dOqFz587gctlcuuVEs77izpo1i/h8fpHHKT6fT3w+nyZOnMi0vGrDpk2bCj/mfHweuVwu+fj4VKrMW7duFdbEI0aMoPv375O5uTl169at3DVkbm6u1syHqiY05xH3zZs3hY9kfD6fvLy8qFGjRoWPVvr6+pSens60TI1HKpWSo6NjoTG9vb3J1taWrKysCg17586dcpRUnIYNGxIAcnFxISKihw8fkqWlJbVv354yMzOVfCQsSk1cXVX8/PwgkShyC23duhUNGjSAp6cnli1bBgDIy8vD77//zrBKzeePP/5AbGwsAGDq1Kn4/PPPYWJigiNHjhRObrRmzZpKlT19+nQAQHR0NPLz8+Hl5YXr168jMjISw4YNU0qvJ5b/wPQtgt6PjJrY8s4AACAASURBVNDT0yMANGnSJCIi6tOnD40ZM4ZkMhn5+PgQAGrQoAHJ5XKm5Wo0LVu2JADUsGFDEgqFtGTJEnJzcyMiovnz5xd+eIuMjKxw2SkpKYVPOU+efJj2ISQkhGxtbcnb25vevXun1OOp4WhGDbpmzRqIxWJ4eHhg48aNwEf9R7lcLvbs2QNdXV1ERkbir7/+YlquxnL//n3cv38ffD4fR44cgaGhYZH1y5cvh7e3N+RyeeF5rgi1a9fGgAEDAABPnz4tXN6sWTPcvn0baWlp6NChg1Zl22Aaxg2ampqKLVu2wNjYGGfOnCns1P1xB29XV1esXLkSALBlyxZG9WoyBefo119/hZeXV7H1Ojo6OHz4MAwNDbFt2zakpaVVOMa0adMAAKGhoUWWOzk54fr168jPz0eXLl2QkJBQ6eNg+QDjBl27di3EYjEOHz6MevXqFS7Py8srMgLj66+/ho+PD06cOIG3b98ypFZzefXqFU6dOoUePXrgyy+/LHU7Z2dn7N69G3l5edixY0eF43Tu3BlOTk548uRJsXUODg7466+/wOPx0LlzZ7x+/brC5bMUhVGDvnv3Dps3b8bixYvRq1evIusyMzOLJHbmcrn4/fffwefzsXPnTgbUajb+/v6wtrbG/v37i8x0nZycjLy8vCLbDh06FKNGjcLGjRuRn1+xOWw4HA5mzJiBsLCwEtfb2Njg2rVr0NPTQ/v27REdHV3idizlg1GD/vrrr/D19cVPP/1UbJ1MJoO9vX2RZQ0aNMDKlSuxdetWyGSyYvvUVNLT0xEUFIS9e/cWGw5mbW1dpCNBAVu3boVAIMDhw4crHG/cuHFISEhAVlZWieutrKxw8+ZNWFlZoXPnzoiMjKxwDBYFjBk0IyMD586dQ1BQUIk9S0obZDxr1iw4Ozvj0qVLalKq+WzduhUzZ85Et27dyr2PkZERDhw4gA0bNqCincmsra3Rt2/fUmtRADAzM8OlS5dQp04ddOjQocxtWUqHMYNu2bIFO3fuhIVFybOdlWZQLpeL3bt3Y9++fWpQqflIJBLcu3cPP//8c4X3bdGiBYYMGYKrV69WeN8pU6YU+1D0X0xNTXHx4kU4OzujS5cun9yepTiMGDQzMxNubm5o0aJFqduUlabDyckJvr6+hQ3yNZlTp05h9erVlU4YPW/evBI/+HyK7t27Izc395PbmZiY4NKlS2jcuDF8fX1LnduHpWQYMWhubm5he1pJSKVSSKXSMvPoTJkyBa9evVKRwupDo0aN4OLy6RnKSoPL5WL06NFITk6u0H4cDqfcgxcEAgFOnz6Nli1bokePHrhz504l1dY8GDFonTp1ylwvEokAoEyDcjgc+Pj4KF1bdYKI4OnpWeVyrKysYGVV8flUy3oC+i+GhoY4c+YMfH190b17d9y4caPC8WoijLeDlkR5DAqgxK+TNYmPm1OYKKuimQJ1dXVx5MgR9OjRA59//nml3n1rGhpp0IJ2OzbnqvZRYNIBAwagb9++7Nf4T6CRBi1vDcpSPeHxeNizZw+GDh2KL774AqdOnWJaksZSoRm21QVrUO2Hx+Nh165dEAgEGDp0KA4ePIiBAwcyLUvjYA3KwhgcDgcbN24Ej8fD0KFDsXv3bowZM4ZpWRoFa1AWRuFwOFi/fj10dHQwYcIEyGQyjB8/nmlZGgNrUBbG4XA4WLduHYyMjDBx4kQIhcIyR+TUJDTaoDW9GaWm8fPPP8PQ0BCzZ8+GVCrFnDlzmJbEOBprUD09PTY9Yw1k/vz54HK5+Prrr5GTk4Mff/yRaUmMorEGZR9vay7z5s2DkZERvvzyS0ilUixevJhpSYzBGpRFI5kxYwZ4PB5mzJgBkUiEVatWMS2JEViDsmgsU6dOhUAgwPjx4yGXy+Hn58e0JLWjsQZlPxCxAMCoUaPA4/EwZswY5OTkYPPmzUrtg6zpaKxB2RqUpYDhw4dDR0cHI0eOhFQqxdatW2vMB0TWoCzVgsGDB8PAwACDBw+GUChEUFAQdHQ08vJVKhp5G2INylISffr0wcmTJ3Hy5EmMHj0aUqmUaUkqhzUoS7WiV69eOH/+PM6dO4cRI0YUzuejrbAGZal2+Pr64vz587h06RIGDBhQLO+vNsEalKVa0r59e1y9ehXBwcEYMGBAYfdQbUMjDfrfaR9YWErC29sbly9fxoMHD9CrVy9kZ2czLUnpaKRB2RqUpbw0b94cN2/exMuXL/HZZ5+Vmu2+usIalKXa4+7ujmvXriE6Ohpdu3at1KxtmgprUBatoFGjRrh+/TqSkpLQrVs3pKamMi1JKbAGZdEaXFxc8PfffyMzMxO+vr5aMZEwa1AWrcLR0VGrJhJmDcqidWjTRMKV6syYlJSEV69eITExUSXzdPJ4PDx+/BhHjx5Varnm5uZwcHBAvXr1NLYfp1gsRlRUFOLi4pTSbPDy5UtIpVKlnEs+nw97e3vUq1ev1FnpNIG0tDS8fv0ac+fOxaJFi/DFF19gwYIFjGgxMjKCo6Mj6tevDz09vYoXQOVEKBTSmjVrqGnTpgSgWv9YWlrSzJkz6cWLF+U9fJUTHBxMo0ePJiMjI8bPz6d+OBwOdejQgXbu3ElSqZTpU0dERFKplHbt2kUdO3YkLpfL+Dn674+RkRGNGjWKgoODK3JYS8tl0JMnT1LdunXJ2NiYZsyYQVeuXKH4+HiN+eeUl9TUVAoJCaGVK1dSo0aNSFdXl+bPn09isZgxTWlpaTR69GjicDjk4+NDmzdvpqdPn1JWVhZjmkpDLBZTdHQ0nTp1ikaOHEm6urrUpEkTunPnDqO67ty5Q02aNCFdXV0aOXIknTp1iqKiohj9vxaQlZVFT58+pc2bN5OPjw9xOBwaM2YMpaWllWf3sg0ql8tp6dKlxOFwaMKECZScnKw04UwjlUppy5YtZGxsTL6+vpSamqp2DS9fviRXV1eyt7enEydOqD1+VYmIiKCePXuSvr4+7d+/nxENBw4cIH19ferRo4dGPRGVxokTJ6hu3brk6upKERERn9q8bIMuXbqUdHR0aOvWrUoVqUmEhoaSo6MjtWzZknJzc9UW982bN2Rvb08tW7akxMREtcVVNjKZjObOnUscDocOHz6s1thHjx4lLpdL3333HclkMrXGrgqJiYnUqlUrsrOzo9evX5e1aekGPXHiBHE4HNq+fbtKRGoSL1++pNq1a9PIkSPVEi8/P5+8vb3J3d2d0tPT1RJT1cyZM4cMDAzo0aNHaon36NEjMjAwoDlz5qglnrLJyMggd3d38vb2pvz8/NI2K9mg2dnZZGdnR5MnT1apSE3i4sWLBIAuXryo8lj+/v6kr69PL1++VHksdSGVSql9+/bUrl07ksvlKo0ll8upXbt21L59+2r3HeRjXr58SQYGBvTrr7+WtknJBl25ciWZmppSSkqKSgVqGgMGDKBmzZqpNEZubi6ZmZnRjz/+qNI4TBASEkJcLpdOnTql0jinT58mLpdLISEhKo2jDn766ScyNTUloVBY0uqSDerh4UFfffWVysVpGrdu3SIAFBoaqrIYhw4dIh0dHUpKSlJZDCbp2rUrDR48WKUxBg8eTF27dlVpDHXx9u1b0tHRoUOHDpW0emmxnkSxsbEICwvDoEGDlNRUW31o37496tSpg/Pnz6ssxoULF9CxY0dYW1urLAaTDBkyBOfPnwcRqSzGhQsXtOb6tLS0LMwQURLFDBoTEwO8Hx1QFrceJGDWir9g2mYnAg6HAQASU3JRv/d+LNx0Tznq1QyHw4Grq2vhOVAFMTExnzy3+RI5lm/7Fw0/O4Buk09XKs7PAQ/g3Gsf3iQLAQDbjj7DZzPOwbTNTkTEZpS6rKq4urpCKBQiJSVFKeX9l9TUVOTk5BQ5hzcfJGDE95dh2mYnrtypft36GjVqVOo1V6y/29u3b4H3zi6Ljt62cK1nhn1nIwqXcTiADo8DHrf6Jha2trZGcnKyyspPSUlB7dq1y9xGl8/FT9Na4O+QREhl8krF4XIAHR4XBTmepw1xh4EeD/88SircpqRlVaXgySA5ORlWVlZKK7eAkq5PX29bEAHn/4pTejx1YGVlVeo1V6wGLXg0qUz2bpvahnhxdiSWzGxZGZ0VZsT3l5GYkqvUMjkcjkofz4ioxHP76Hkqvl59W2lxFk73RsS5kbC1EiitzPJQcGyqOodVuT41lbKuuSqNZuHxmDtJ4dHpuPB3nErNpE5+3fsYshJqS226ENWBtp2uCg3puPRPPPx2PURGdj5srQT4+FyI8qRYtfMhAo+Ho6uPHfb+0hXh0elYuvUBzv8Vh4vbP8e/YSkIOvUCM4Z5YHz/Rjh+ORr+vz+Grg4PUpkcfXwd8d24ptDhKe4b956+xarAECSk5MJEoIukd7lwczbDpIFuWLLlPoiA4fMuQ5fPxaG1PVDbVB+Xg19j3Z5HyMuXIS9fBmNDPuZO8EKPtnU/qYcpvll9G3/eioNpLV10m3wan3V0xLdjmxau3/3Hc+w7E4GwyDTUszfGtsW+aOJigU0HQrFhXyhauFtiwdTm+DXoMZ5EvIPfd23w2/5Q3HqQgOD9A+HmbFYhPakZefhxw108DE+FSS1dGOjrYNXXPnCvb1ZqzJCjQ1RwZipOZFwW/rj6Fy79E488sQwjPmuIVd/4FK6vzPXRqaUt4pJySr1uVHnNlbsGvXE/AcPnXUafjo54cHgwTm/sje1LOhWuN9DXwc9ftoSV+YdxnG7OZpg2xAMA8GvQY+RL5GjXzAZyAi7cjsOkRdcxd7wXru3qi32rusE/6DG2vv/g9CAsBX1mnEOrxta4s38gLm7/HP/sG4D4pBx0b2OPcf1cAQCH1nTHlcC+qG2qj5sPEjBs7iVMGeyOG7v74c7+gRjY3RnD5l7C9XtvytTDJP7z28HYiI/eHRxwJbBvEXO+y8iDe30z7FvVDac3f4bU9Dws2HAXADBrZGPUr2uMJy/fYf/ZCHRqaQuBAR/dfOwxqk/DSmkhAoZ+ewkRsRm4uacfLu/4AvXtjdFv9nmI8qSlxtQUMrPF+Gp0E1zb2Q8jPmuIrUfCcPuh4h27steHa73SrxtVX3PlrkHX7nkESzN9fDW6SSVOGzBlsDu6+dhDLJHhdZIQ3/jdhkMdI/TvUg8A4FDHCD5NrbH3dARmjWyMVYEhMK2lh+/GfbhYBQZ8jPncpdQY64Ieo769MQZ1dy5cNn2oBzYffAr/35+gcyu7UvVoKuYmemjdWPHhpY6lIbq1scflf+KLbGNraYjV37YBALRuUrXmmzuPkxASnoKAhR1hoK+4PIb1boDdfzzH+b/jMLCbs9JjKpPm7pZo6GACAJg53BNbj4QhPDod7ZrZVOn6iE/KKXH5N363VXrNlasGJQLuh76FV6PaVf5Cq8fnoX5dYzx+ngpne+Mi62xqGyI2IRtEQPDjZHg2NAdfp6jE6cM8Si37QdhbuDiZFlvuUd8cD8LelqmnuqCvy0O+tPQvuxV9nP0vj1+8AwDU++h/U6e2IQAgJqHkAeRVjakq9HR5AADJ+/OlzOujYLmqr7ly1aC5eRKIJTKYGVdiRHgp5ORK8PRlGvrMPFdkubenJfLEUghFkgrFk8rkyBVJYaBX/JAEhjrIFUkhY/pZthqQnauY62TB+rsw0OcVLm/XzAbmSvz/qxtVXB/quObKZVA9XR64XA4ysvOrFOxjagl04e1phUNrupe4XmDAR2YF4unwuDA00EGuuPiMV8JcKQQG/GrdPqsuagkU75P+89uhqavmpjWpKKq4PtRxzZXrEVeHx4WrkykePU+tdMP5f/FsaI6nL9MgL+UO07qJFe6HvUWuqOQp5ko67FaeVngZU7xHTFhUGrw9yu54wTSa0pzSuKHClI9faEde2Y9RxfWh6muumEGNjIwAAEJh0ZfYyYPckJSaiwXr7yI9SwypTI7w6PRKB5462B2vk3Mw3/8O3mUoZqfKyZUUvozPG+8FYa4EI+dfRlhkGqQyOWRyQvTrLORL5DAzUTxu/fssBVKZHHliGb4Z2xRRr7Nw4kp0YZwdx57hzVshvv3oY1NZ5OTkQCBQXeO+QCAodm4BwMxYD2GR6RBLZMjJZW5KvTZNreHRwBy/7AjB3yGJkMkJMjkhPikHorxPz8dZcGwF15GyKfjflHQOP4Uyrg9VlCkUCku95nhLlixZ8vECsViMgIAAjBo1qkh3quZuljA04OPwhUj47XqIk1dfwcm2Fq7eeY2sHAnkcsLRS1G4/TAJmdn5SE3Pg44OF1uPhOFlbCYysvMhkxM8G5oDAFzrmaKevTFOXHmFpQEPsO1IGK7ceQ1H21pwcTJFXRsjtGtmg78fJmHN7kfw3/sEh89HIjUjD11a26G+vTH+eZiEHcef4eTVV2jc0AIdWtSBV6Pa+G1/KPb88QI7T4QjMi4T/vPboUsrO4RHp8P/9ycl6ilg5cqV8PHxQZcuXSr2nyonFy9eRHZ2NoYMKdpuaGykiyMXI7HtyDO8jM1EbEI2zv8dj/QsMcT5MrRrVgcH/3yJIxejkJIugkgsw9OX7wq3eZeRh4aOJjA20sXOE+E4fCEKcYk5SMvMgw6Pi+v3E3DscjReJ+UgLVMMPo+La/eKL3NxMkWfjo549SYb/nsfY9XOEBz6MxKvk4Xo1NIWO449KzFmAcHBwTh27Bj8/PzA4/FKOANVQyAQ4JdffkH37t3h7u4OvO+0UvB/zcqRKD5wEbBqZwgev3iHHKEEDeoao33zyl0fZV03Tra1qnzNBQYGolatWhg2bNh/D/dWseFmeXl5ZGJiQuvXr1fLcBtN4vXr1yofz7hy5UqytLQkiUSishhMMm3aNJWPqW3evDlNnTpVpTHUhUQiISsrK/rll19KWl18uJmenh4GDhyIoKAgrelGV16CgoJgYmKCXr16qSzG8OHDkZqairNnz6osBlNkZ2fj6NGjGDFihErjjBgxAseOHdOK6QbPnj2LlJQUDB8+vOQNSrLt48ePicfjUVBQkMrvIJpCUlISGRsb0+LFi1Uea8iQIeTq6qoRaSGVyfz588nc3FzlGRLfvXtHFhYW9P3336s0jqoRi8Xk6upa1gD30pOGffnll2RhYVGe1IDVHolEQj179iRHR8fSUk8olZiYGDI0NNSqrBXXrl0jPp9PmzdvVku8LVu2EJ/Pp6tXr6olnir46quvyNDQkGJiYkrbpHSD5ubmUqtWrcjFxYXi4uJUJpJppFIpTZ48mQwNDenBgwdqi3vkyBHicDi0evVqtcVUFSEhIWRubk7Dhw9XecKwAuRyOQ0fPpzMzMzU+n9TFmvWrCEOh0NHjhwpa7Oy8+ImJCSQp6cn1alTh/766y+li2Sa5ORk6t27NxkaGtKZM2fUHn/Dhg3E5XJp2rRpaqm5VcHBgwdJIBBQjx491JpXmIhIJBJRz549SSAQ0IEDB9Qau7Lk5OTQtGnTiMvlludD7KenfsjMzKQvvviCOBwOjR49ulrerf5LYmIirVq1ikxNTcnBwYHRYzp58iSZmJhQ3bp1aceOHZSZmcmYlvIik8no2rVr1K1bN+JwODR79mzGvkpLJBKaPXs2cTgc6tq1K129elUjk1hnZmZSYGAg2dvbk6mpKZ08ebI8uy3lUDk/1Z48eRILFizA8+fPUa9ePbi6usLOzk4lbV2q4t27d4iJicGjR49gZGSE2bNn44cffoChoSGjut6+fYuffvoJe/fuBYfDQbNmzeDo6AhjY83qxJ+fn4/4+Hg8e/YMiYmJaNu2LdauXYs2bdowLQ3BwcGYN28ebt++DRsbG3h4eKBu3brQ1dUtx96qIysrC7GxsXj48CGICGPGjMGKFSvKmw5mWbkNWsD9+/dx8eJFREdHIyEhQSXTD6oKCwsLODo6olWrVujTpw/09fWZllSEjIwMnDp1Co8fP0ZMTIxKmxFsRCJk6OoirwI3WD6fj7p166JBgwbo27cvXF1dVaavskRERODUqVOIiopCfHw88vM/3Z87Ly8POjo6KpmSslatWnB0dISXlxf69esHU9PiI1/KoOIGZdESjh4FfvsNOHcO0LCaWp28fPkS3bt3x+XLl9GwYeUGuauQZRo5wzaLGhAKgb//Bjp3BtIr36e6OhMaGoo2bdogNjYWeXl5TMspEdagNRWhEODxgNBQoGNHIFX7Rq+Uxb1799C+fXtkZChGorAGZdEshEJARweQSIBnz4B27YAk5eXH1WRu3LiBzp07Iycnp/AbCmtQFs1CKATk78f2yuVAdLTCpK+rX2b2inDu3Dn07NkTYrEYcvmHsc2sQVk0C6HwQxJZHg+QSoH4eKBtW0CFU18wyeHDh9GvXz9IJJJirQ+sQVk0i5wcRTY4HR2g4GKVy4E3bxQmjYxkWqFS2blzJ0aOHAmZTFZicwprUBbNQihUGLPApC4ugIODwqSJiQqThoczrVIprF+/HlOmTCl8pP3ss8+gq6sLPp8PHo8HLpfLGpRFw8jJUZhRJgO+/VbxWPv338CqVQCfD6SkKN5JHz9mWmmVWL16Nb755hsQERwcHHD+/HkMGTIEcrkc3377LTgcDjgcjsYa9JN9cVm0lC5diAAiKyui7GyiWrWI1q1TrAsNJWrZUrHexISoGva/lsvl9N133xEA0tHRoUWLFpFIJCIiovbt29PAgQPp0aNHBIAA0IYNG5iWXBKf7izPoqUUGHDUKMXf06YRubkRFQwXk8mINm0iEgiIjI2J/vmHUbkVQSaT0ZQpUwgAdezYkZ4/f1647smTJwSALl++TDKZjGrVqkUANHXYX/GUJyw1hBxF9kR07qz4PXWq4p3zr78Uf3O5wJdfAi9eAF26AD17AjdvMqe3nEgkEowePRqnT5/G77//jps3bxbpMxwQEAAXFxd07doVXC4X7du3B9iPRCwax38N2rw50KIFEBhYdDs7O+DkSWD/fmDaNODSJfVrLSdisRgjRoyAjo4OwsLCMHr06CLrs7OzsX//fsyYMaMwD7Gvr2/hvpoIa9CaSm4uYGMDOH+Y9AczZgC3bwNpacW3/+IL4O5d4MIF4Px5tUotDzk5OViwYAHmzp2LvXv3wsKieFb833//He7u7hg7dmzhso4dOwIARCKRWvWWF9agNRWRCOjRo+iyYcMUfXL37i15HxMT4NdfAUtL4PlztcgsDxKJBE+ePMHq1avh4+NT6nZbt26Fh4cHzM0/5KVt0aIF9PX12UdcFg1DLP7weFuAkREwfDiwbZuifbQ0vL0V7aYaAp/PR9u2bcscz3nr1i2EhoZi+vTpRZbr6uqidevWrEFZNIi8PEX7Z6dOxddNmaKoHW/fLrsMbvW6dAICAtCqVSt4e3sXW+fr68u+g7JoEEIhUK8e4ORUfJ23t+KD0Y4dTChTCSkpKTh58iRmzJhR4voOHTqw76AsGoRQWHLtWcCUKYqMCyV9LKqGbN++HQYGBhg6dGiJ69u0aQOp9NMTQzEBa9CaSE5O8ffPjxk9WtE/d98+dapSCXK5HIGBgZg0aVKpyeEEAkHhREyaBmvQmohQCLxv/ysRIyNg5kx1KlIZZ8+eRWxsLKZOnVrmdi1btlSbporAJg2ricTHA3XrMq1CLfTu3RtyuRwXL14sc7v4+HjU1bxzskz5eQZZNB/NuxBVQnR0NC5duoTjx49/clsNNCfAPuKyaDNbt26FjY0N+vTpw7SUSsMalEUrEYvFCAoKwvTp08Hn85mWU2lYg7JoJUeOHEFaWhomTpzItJQqwRqURSsJCAjAgAEDYGdnx7SUKsF+JGIpH2IxoKdX9jZZWYpugiYmQHnmbYmNBV69Kr5cIACq0Ozx+PFjBAcH49q1a5UuQ1NgDcryaS5dAkaOBKKiFOYriXXrFJ3s+/VT5DHKzASOHwfs7Usv9/ffgYULiy/38ACePq203M2bN8PNzQ2dyuotVU1gDcryaVq3VgxP27+/5A4M584BP/ygyMhQv75i2eefA0OGAMHBZZe9cqVi24+pwqxz2dnZOHToEFasWFE4KLs6w76DsnwaExNg6FBFDVkSa9YoMgAWmBNQZF+4cwe4davssu3tAU/Poj8NGlRa6p49eyCTyYplU6iusAZlKR9TpgBPngD37hVdnpurGJrm6Vl0eYsWit+f6MGjbLZv345Ro0bBzMxMrXFVBWtQlvLRti3QtCmwfXvR5ZGRimkjrK2LLrexUYwZ/VTmhbw8xbvtP/8AYWGKsirJjRs38PTpU0ybNq3SZWgarEFZys+kScChQ4qvtQUUDEkzMCi6LZereJcsa8iagwNw8CDwyy/A4cOKnEjW1sCWLZWSFxAQAB8fH7QoqL21ANagLOVn7FhFKpT9+z8sK6jxSsqwwOMppjcsq7yrV4GdO4ENGxTvq3PnKtJ9/vlnhaQlJSWVOSi7usIalKX8mJgomkU+7lguECh+5+cX3z4vTzF0rSIU5Az6+CZQDnbs2AFjY+NSB2VXV9hmFpaK8b//Ff3bwUHxOz296PLsbEXtWbC+vJiZKTpEJCaWexeZTIadO3di4sSJ0K9CE40mwtagLFXDzg6wtS3eIygiQvG7hCRdhZT0AUkiUfx8lBrzU5w5cwZxcXGYMmVKufepLrAGZak6w4crZkb7eFLcCxcUH47691f8LRIBISFF9yspy0FwsGLWtV69yh0+ICAAPXv2RMOGDSt9CBoL07PDsGgBqalETk5E//sfUV4eUXAwkbk5kb//h21GjlRM1rR9+4dlTZoQbd5M9Po1UXo60aVLRA0aEPXsSSSRlCt0ZGQkcblcOnXqlAoOjHGWsu+gLFXHwkLRgWHtWkWNaW6uSDjWu/eHbQYOVLyXvp+sCICie+DVq4qpJPLyFE0sS5YoamQer1yhAwICYGdnV60HZZcFm5OIpdoiEolQt25dfPPNN/jxxx+ZlqMKlrHvoCxVIz6esdCHDx9GVlYWJkyYwJgGXTEwtQAACrtJREFUVcMalKXyBAUphoYVTGWoZgICAjBo0CDY2toyEl8dsAZlqTyff65oEjl4UO2hHz16hHv37mldz6H/whqUpfJYWACDBjEyj8umTZvg5uaGDh06qD22OmENylI1pkwB7t8v3sapQjIyMnDo0CF8+eWXWjEouyxYg7JUDV9fwN0dCAxUW8g9e/aAw+FgzJgxaovJFKxBWarOxImKds/sbLWE27FjB0aPHg1jY2O1xGMS1qAsVWf8eMXHoiNHVB7q6tWrePbs2ScnQ9IWWIOyVB0LC+C334BWrVQeKiAgAO3atUOzZs1UHksTYLv6sSgHNYwkSUxMxOnTp7F7926Vx9IU2BqUpdqwbds2mJiYYNCgQUxLURusQVmqBVKptHCmbG0blF0WrEFZqgWnTp1CYmKiVmXsKw/saBaWakG3bt2gr6+Ps2fPMi1FnbAzbLNoPpGRkbh27RrOnDnDtBS1wz7isigfkQi4e1dpxW3evBl169ZFrwqkQdEWWIOyKJ/NmxU5hUSiKhclEomwd+9ezJgxA7xyZlnQJliDsiif8eMV5lRCz6KDBw8iJydHqwdllwX7kYhFNQwdCiQkKLL9VYGWLVvCxcUF+yuYyFpLYFOesKiIKVMUs55VYSLee/fu4cGDB1o/KLssWIOyqIZu3RTzfFZhGFpAQADc3d3R/uNMgDUM1qAsqoHDUQxDCwpSzCFaQTIyMnDkyBHMmjVLJfKqC6xBWVTHxImAUAgcP17hXXft2gUej4dRo0apRFp1ge2owKI6rK0V5mzbtkK7ERG2bduGMWPG1IhB2WXBGpRFtXzxRYV3uXLlCiIiInDs2DGVSKpOsM0sLBrHwIEDkZqailu3bjEthWmWsQZl+SRyuRy3bt3CvXv3EB8fj/ySJutVIjdu3ICDgwOcnZ0rtJ+xsTGcnJzQs2dPNGjQQGX61AhrUJbSkUgk2LRpE9atW4c3b97AyckJdevWhZ6eHtPSSiQzMxNRUVFIS0tDmzZt8Msvv6BTp05My6oKy9jpB1lKJDw8nNzd3UlfX5++//57ev78OdOSyoVUKqVLly5Rnz59CACNGzeORCIR07Iqy1K2BmUpxq1bt9C/f3+4ublh//79cHJyYlpSpTh79izGjRsHFxcXnDt3DuYVmLVbQ2AfcVmKEh4ejrZt26Jr167Yt29ftU8vEhERge7du8PZ2RmXLl0Cn89nWlJFYA3K8oH8/Hw0bdoUtWvXxpUrVzT2XbOihIaGon379pg+fTpWr17NtJyKwHaWZ/nA+vXrERsbi3379mmNOQGgcePGWL16NdavX48XL14wLadCsDUoC/A+a56dnR2mTJmC5cuXMy1H6chkMjRp0gTt27fHtm3bmJZTXtgalEXB1atXkZKSgkmTJjEtRSXweDxMmDABx48fV3k7rjJhDcoCALhz5w5cXV1Rr149pqWojN69e+Pdu3eIiIhgWkq5YQ3KAgCIi4urUHOKXE7YdCAUpm12IiI2o8rxxRIZOk88hW6TT1e5rNIoOL7Y2FiVxVA2rEFZAADZ2dmoVatWubfncjkwNtJVWnw9Pg96fNUmBRMIBODxeMjKylJpHGXCGpSFRYNhh5uxlIkoT4rTN2Lw5q0QxgJdeDYwh09T61K3f52cg+DHyUhMyQWPy0ELD0v4NLEud3k8LhdSmRzX7yUgLDINzvbG+KKTEz6e6T4yLhNX776BXE7wcrVAGy8bAMD2Y8+QlpEHFydTDOzmjOfR6Qh+kowJ/Rup6vSoHLYGZSmVjGwx2ow+gaeRaWjiYgFRnhTz1gWXuc+GfaG4cT8BTV0tYG6ihz4zzmHr4bByl5eclouvV93GmRsxuPVvAsYuuIrl2x4Urt/zx3O0H3sS+fky2NQ2xNSfb+Jbv9sAgHH9XHHxn3j8tj8U4368hv5zLmBVYIhKzo26YGtQllI5ezMWKWl5WDZLMTFvNx97mNQq+73T3lqAKYPcYWiguLSCTr3A8SvRmD7Mo1zl1TbVx6YfOxT+3Xf2eZy48goLp3sjJV2E+b/ewbSh7pg9qjEAIF8iw7Sfb2J8/0Zo4mIBPT4P6VlirPmuDazMDbB4832lnxd1wtagLKWir8eDUCRB4PFwyOWK/ixj+7qWuc+c0U0KzQkAJrV0kZElrnR59e2NkZaZBwC4dvcNxBIZfFvaFq5v6mIBALj/9G3hsloCPqzMDQAAP3/ZssLHrUmwNShLqfTp4IhWnlaYu/YfrAt69P/27i2mrToO4Pi3UDY2GK5KuQzWRHCbBEVhBIIDfSJ0ji2YGEHrCJIoD94ql5fFhMTwQgAfGhJjhBckhIYRgjHI2ANRxMCUESMSDB3IfbKNQKEto5fjQ7eGe1ZgtE3+n5fmtOf88mvTX07/1/JO1gt8/O5Lri//dlbMVn75Y5bJuyusmK3cmTIi20c8gMdT3WbmTQD80P0vv//lLEijyQrA3D33dw70BaJAhR0dC5Tz07fZ3PxtitabY3yjH0LfaaD3+7d47uTWVS7jM0ayPvqR18+f4uqVsygVx+i+NcP8A8ue4u0k9eVwVJHBruM3M1REhwfveo2vEgUq7Gh1zU7gEX/U6SrU6Sryr5zj8icd3Oid4r1LZ7ac39xh4P7iKrVfZhB4xDmmGXw8wFWg7sbbLCosCB61c9OTIg/8/Xoj0QYVXDavm6i7PszfhgXXcUpCGDKZsy25HZvd4Xy0ObZ93d14m72RfAq5vx9NHaNPdP5OZOvHbLycuIMKAISGhjIyMrLhOUmCoq9+5jNNAkpFIPpOAy8+ryDrwmkcDomlZeek84UlZydQ5mun+brhT97+4gbn45VMzC4zM2/CanewumbfNd6a1cFDqx2bTeKh1c7RAH/sDgnzqg2HQ8JssRERepyKT1O4putn+j8T6YkROCS4e9/MtQ+TePaZQFcMs8W2obMKYGFhAbvdjlKpPMRPdn/EcjMBgMrKSmpra5mcnHTdYYwra/TcnmNidhmrzUFMdAjqdBUBcj++uz7Mg8VV1/WvnAvlYoaKgeF7/Hp7jpMnjnIxQ8U/44v0Ds5xIugIVy+f3THe40kGPGqrfv5+AvpOA+PTzml5/v5+lH3wKgB3pox035rBaFojKiyIC4kRRIcHb4gh85OhuXRmQ9u0r6+PtLQ0DAYDsbGxh/r57pHYUUFwGhwcJCkpif7+flJSUjydzlNRVlZGW1sbo6OjvvIzV6wHFZwSExOJj49Hp9N5OpWnYmlpiYaGBjQaja8UJ4hOImG9iooKmpqa6Onp8XQqB668vBxJktBqtZ5OxS2iQAWXnJwcsrOzycvLY3p62tPpHBi9Xo9Op6O6uhqFQuHpdNwiClTYoLGxEYVCQWZmJmNjY55OZ99aWlooKChAq9WSn5/v6XTcJgpU2CAkJISuri6CgoJITU2lubl5y/ioLzAajZSUlJCbm0tRURFVVVWeTmlPRC+usC2TyURxcTF1dXUkJydTWFiIWq0mKioKudw7h88tFgsjIyO0trZSX1+P1WqlurqagoICT6e2V2KYRdjdwMAANTU1tLe3Yzabkcvlbm2NclgkSWJx0bk3kkqlQqPRUFpa6ot/97CeKFDhyZhMJoaGhpiYmHAVgjeRyWRERkYSExNDXFycTw2l7EIUqCB4MTFRQRC8mShQQfBiokAFwYv9D2HYvw0awgxsAAAAAElFTkSuQmCC", "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "from fosf.utils.draw import notebook_display as display\n", "display(ftax, drop=\"bot\", instances=False)" ] }, { "cell_type": "markdown", "id": "7f5d0125-1846-4fa3-a434-3d1315a67219", "metadata": {}, "source": [ "Accessing instances" ] }, { "cell_type": "code", "execution_count": 4, "id": "739a5d75-f9bc-4a01-83aa-8302b239814d", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "0.7" ] }, "execution_count": 4, "metadata": {}, "output_type": "execute_result" } ], "source": [ "from fosf.syntax import Sort\n", "ftax.instances[\"p\"][Sort(\"slasher\")]" ] }, { "cell_type": "markdown", "id": "79258c5c-ff8e-440e-a04a-11d6e1e5148d", "metadata": {}, "source": [ "Computing GLBs" ] }, { "cell_type": "code", "execution_count": 5, "id": "fc5cd212-204c-4754-84d9-7deb672343a4", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "Sort('slasher')" ] }, "execution_count": 5, "metadata": {}, "output_type": "execute_result" } ], "source": [ "thriller, horror = Sort(\"thriller\"), Sort(\"horror\")\n", "ftax.glb(thriller, horror)" ] }, { "cell_type": "markdown", "id": "54ce9e3d-b29b-48a3-b62a-ac8046a1ad23", "metadata": {}, "source": [ "Checking sort subsumption" ] }, { "cell_type": "code", "execution_count": 6, "id": "78073933-2061-491d-84ce-b9b53d80b5b5", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "True" ] }, "execution_count": 6, "metadata": {}, "output_type": "execute_result" } ], "source": [ "slasher = Sort(\"slasher\")\n", "ftax.is_subsort(slasher, thriller)" ] }, { "cell_type": "markdown", "id": "6fde9024-b5c9-48c1-a382-bd0cdff8faa3", "metadata": {}, "source": [ "Computing subsumption degrees" ] }, { "cell_type": "code", "execution_count": 7, "id": "7acd78da-3f0d-4a9e-9956-b37128e7549f", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "0.5" ] }, "execution_count": 7, "metadata": {}, "output_type": "execute_result" } ], "source": [ "ftax.degree(slasher, thriller)" ] }, { "cell_type": "code", "execution_count": 8, "id": "572a39b2-a6bf-48e7-ac4a-9b85decd3c35", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "1.0" ] }, "execution_count": 8, "metadata": {}, "output_type": "execute_result" } ], "source": [ "movie = Sort(\"movie\")\n", "ftax.degree(slasher, movie)" ] }, { "cell_type": "markdown", "id": "b56111f6-ceef-49c0-878f-4acc0d812120", "metadata": {}, "source": [ "Computing membership degrees of each instance with respect to a few sorts:" ] }, { "cell_type": "code", "execution_count": 9, "id": "165550c7-3c87-4aa1-ae0e-c440a09c26e4", "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "h\n", "slasher(h) = 1.0\n", "horror(h) = 1.0\n", "thriller(h) = 0.5\n", "movie(h) = 1.0\n", "p\n", "slasher(p) = 0.7\n", "horror(p) = 1.0\n", "thriller(p) = 1.0\n", "movie(p) = 1.0\n" ] } ], "source": [ "for mov in [\"h\", \"p\"]:\n", " print(mov)\n", " for genre in [slasher, horror, thriller, movie]:\n", " degree = ftax.membership_degree(mov, genre)\n", " print(f\"{genre}({mov}) = {degree}\")" ] }, { "attachments": {}, "cell_type": "markdown", "id": "167ed259-02ad-4f34-a569-68e525f25405", "metadata": {}, "source": [ "## Figure 2\n", "\n", "Parsing an OSF term and converting it to an OSF clause" ] }, { "cell_type": "code", "execution_count": 10, "id": "59054c53-03e3-4a94-95dd-2a09a36dcbb3", "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "X0 : movie & X0.directed_by = X1 & X0.written_by = X1 & X1 : person.\n" ] } ], "source": [ "from fosf.parsers import parse_term\n", "term_str = \"X0:movie(directed_by -> X1:person, written_by -> X1)\"\n", "term = parse_term(term_str)\n", "print(term.to_clause())" ] }, { "cell_type": "markdown", "id": "882fe8e0-bc9a-42f0-b76a-eb7f5b62c9c8", "metadata": {}, "source": [ "We can pretty-print the OSF term" ] }, { "cell_type": "code", "execution_count": 11, "id": "858075aa-bd0c-4514-9bed-e1df62a3f7df", "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "X0 : movie(\n", " directed_by -> X1 : person\n", " written_by -> X1\n", ")\n", "\n" ] } ], "source": [ "term.pretty_print()" ] }, { "cell_type": "markdown", "id": "b7f7726e-7e76-4f9f-9d5a-78bd0ea74230", "metadata": {}, "source": [ "And also draw it" ] }, { "cell_type": "code", "execution_count": 12, "id": "f86691e2-e458-41a6-b309-4bb16f2478ea", "metadata": {}, "outputs": [ { "data": { "image/png": "iVBORw0KGgoAAAANSUhEUgAAAMQAAAC7CAIAAAC1sKYoAAAABmJLR0QA/wD/AP+gvaeTAAAgAElEQVR4nO2deVwTV9fHZxKSAAlhJ2ENILIEZBER2URERNyr4o7YWtGiUpcq2ta6tLX6tIp9XFCrVnEBBWtVKhYQlUVAWUS2IKBEIIQ9gRAI2d4/7tN5UzZRsgDy/SOfzM3MnTOT39y5c+fcc2CxWAyNMYY0QCnagDFGD2NiGkNqjIlpDKmhpGgDZAKXy2Wz2Ww2u6OjAyzyeDwIgsRiMYvFAusoKSmpqamB7wQCAYPBQBCkoaGhrq5OJBKxWKxCj2BEMvLExGKx6urqmExmbW1tfX09+GQymWw2u7W1FWhIIBAMcS8qKirq/6Ctra2np2doaEgmk/UlUFFRkdIxjRLg4fw0V1dXVyFBZWVlRUUFm80Gv2KxWBKJZGhoSCKRyGSyhoaGpqYmkUgETQv4BG0PDodTVVUFW6mrq6NQKAiCeDwel8sFhWw2WyQSgXYLyLGtrQ35bGpqamhoAKqtr69Hzpi+vr7FP4wbNw58UVdXV9DZUjzDSExdXV1FRUUFBQUvX74sKCgoKCgAtyRVVVXJf8vU1NTAwIBEIunq6srfSIFA0NDQwGAwgNCBvisqKuh0OmgOjY2NHRwc7O3tHR0dHRwcLCwsgHY/BhQsplevXmVkZKSlpWVnZ7969UogEODxeDs7OwcHB0dHRyqVamFhYWhoqEALBwmfz6fT6eXl5ciVgByOvb29m5ubl5eXu7u7np6eoi2VIfIWk1gsfvHixaNHj9LT0zMyMhoaGlRUVCZPnuzu7u7k5DSaLuWurq7i4uIXL17k5eWlp6cXFRWJRCIrKysPDw9PT88ZM2YYGxsr2kYpIycxdXR0pKSkxMfH379/v6amhkgkTp48GZxWLy8vHA73vhWKRKLGxsbGxsaGhgYmk9nU1NTY2NjW1tbe3s7hcFpbWzkcDofD4XK53d3d4JkO3KTa29vBdxiGNTQ0kApBX0pdXZ3wD5qamgQCQV1dXVdXl0wm6+rq6urqkkgkya0GD4fDycrKApdQRkZGZ2enubn53Llz582b92FnYBgiWzHV1tbeuHHjzz//zMzMFIvFbm5uAQEBAQEBjo6OMAwPpgYej1dZWVlVVVVVVUWn08EnnU5vaGgQiURgHSUlJfBPE4lEAoGgpqamoaFBIBDweDyBQECj0UQi8X9HKyEgSWGJRCLQr2exWJx/YLFY7e3tbW1tDQ0Nzc3NiElYLNbAwIBCoVAoFDMzM1NTUwqFAj4H2aZ2dXWlpqYmJCQkJCSUlZWpqan5+fktWbJk/vz5eDz+Pc/xMEImYmppabl169b169dTU1OJROKCBQtmz57t5+enqak58Ibt7e2lpaUlJSWlpaXgS1VVlVAohCBIS0sL+c9MTU3JZDLSWsihJ87n80FDWFdX19jYWFtbiyi7qqqqs7MTgiBlZWVra2tra2sqlWpjY2NjY2NlZaWk9I7Bl9evXyckJNy7d+/hw4c4HG7BggUrVqyYOXPmSBzokqaYxGJxUlLS6dOnExIS0Gj0vHnzVqxYERAQMEAb3tXVVVBQ8Pz585ycnOfPn9NoNJFI1ONfsbS0NDU1RVqXYUh9fX1VVVXpPyDXgIqKiqOjo4uLy6RJk1xcXCwtLQdouhobG2NjY6OjozMyMjQ1NVeuXBkaGmpjYyPfQxkaYmnAYrGOHz9uaWkJQZCPj09UVFRbW1t/K7e3tyckJISHh7u6uiLjzjNmzNizZ8+tW7cqKiqEQqFUrFIgnZ2d+fn5Fy9eDA0NnTx5MriciERiQEDAkSNHsrOz+Xx+f9vS6fQjR45YWFjAMOzr6/vHH38IBAL5mv+BDFVM1dXVoaGhoHfyxRdfFBUV9bmaUCjMyMjYs2ePm5sbaPmpVGpoaOj169dfvXoFBgxHMd3d3Tk5OadPn16+fDmZTIYgSE1Nbc6cOUePHi0vL+9zE6FQeP/+/Tlz5qBQKGNj46NHj3K5XLkb/n58uJjq6urCwsJwOByFQvn111/ZbHbvdbhc7p07d9atWwfGVywsLDZu3BgTE8NkModm9simpKTk9OnTS5cu1dLSAtfV7t27MzMz+2ySKyoqtm3bhsfj9fX1T5w40dXVpQiTB8WHiKm1tXXnzp2qqqqGhoanTp3i8Xg9VhAKhYmJiatXr8bj8SgUytXV9dChQ/01Wh8zfD4/JSVl69at5ubmEAQZGhru2rWrzxPFZDK3bt2qrKxsYmJy/vz54dkTeG8x3bx5U19fX09PLyIiorOzs8evZWVlu3fvNjIygiBoypQpp06dYjAY0rN2NPPy5ctvv/3WxMQEgqBJkyb997//bWlp6bFOTU1NaGgoBoNxd3cvLCxUkKX98h5iqq2tXbRoEQzDQUFBTU1NPX5NS0sLDAxEo9GGhoZhYWEFBQXSNvWjQCgUpqWlhYSEqKmpEQiEkJAQGo3WY53CwkLQ9QwLC+NwOAqytA8GK6bY2Fg1NTUbG5vU1FTJcpFIFBcX5+LiAkGQh4fH7du3h2cLPOJoa2s7duwYhUJBo9GBgYH5+fmSvwqFwpMnTxKJRCqV2lttiuLdYhIIBLt374ZheMuWLT16f+np6VOmTEGhUIsXLwZj3GNIFz6fHx0dPXHiRBQKFRwcXF1dLflrdXX1lClTiETinTt3FGfj//MOMbFYrFmzZikrK1+6dEmyvKqqavHixRAETZ8+PTc3V8ZGfuyIRKKYmBgzMzNVVdVvv/1Wsqva1dW1fv16GIb37dunUBvF7xBTe3u7u7u7gYHB8+fPJcuvXr2qrq5ubW0dHx8vewvH+B9dXV2//PKLurq6ra1tj7ve2bNnlZSUdu3apTjrxAOJicvl+vj46OrqlpSUIIUsFmv58uUwDH/55Ze9H+XGkANVVVXe3t5YLPbIkSOSg72xsbFoNPrgwYMKtK1vMQmFwrlz52pra798+RIpZDAY9vb2+vr6iYmJcrRwjJ4IhcIjR45gMJi1a9dKvpY5d+4cDMMnT55UlGF9i+nHH3/E4XBZWVlIyevXr8ePH29tbU2n0+Vo3hj9kpycrKamNm/ePMnXLD/88AMWi3327JlCTOpDTMXFxRgMJiIiAilpbm6mUCguLi6NjY3yNW+MgXj69KmWltaSJUuQEqFQOHPmTCqV2t3dLX97+nBBmTVrVlNT07Nnz4C/hFgs/uSTT/Ly8vLy8nR0dKTosBAVFfX69Wtkcf78+RMnTnz9+nVUVBQoIZPJGzduBN8LCwuTk5MhCPLz87Ozs5OiGVJEJBJFRkZ6eHg4OjrKZ49PnjyZMWPG0aNHw8LCQMmbN29sbW0PHTq0detW+djw//QQ1/PnzyEIkuwVRUREYLFYyVuetOBwOAkJCRgMBofD5eTkgNFOkUhUVFSkqakZExODvDwGLhk3bty4dOkSmUw+evSo1I2RCrm5uRAEzZ49W547/emnn7BYrOTz3fbt2w0NDXu/M5U1PcW0ceNGe3t7ZLG1tVVTU3Pv3r2ys+Cbb76BIOizzz5DSoKDg3fv3o0s5ufnwzCMjLzfunULhUJJPhkMH0Qi0ZkzZ+Rsm0gkcnV1DQgIQErevn2LQqHkP5LZU0xkMvnHH39EFk+dOoXH4/t0L5EWXV1d1tbWEAQ9fPhQLBbfuHFj0qRJkrf80NBQdXV15DG4u7tbWVl58+bNsjNpxBEfHw/DcEVFBVLi5eW1du1aOZvxLw9lOp3OZDK9vb2Rknv37s2bN0+mLrM4HO63336bOnXqhg0b/vrrrx07dqSkpAAPTEBaWhpwOwSLGAxm/Pjxqampfd6yL1y4YGZm5uvr2+MnGo1248YNsVj8+eefCwSC+/fvg96hubl5Y2PjgwcPwIFPnjwZ2UQkEiUnJ4M31g4ODn5+figU6sqVK5WVlWBuwqpVqywsLDIzM//++28IggwMDOrr64VCIZVKXbp0Kaiku7v73r175eXlRkZG/v7+MnJXnzVrlra29r1795B+0tSpU//44w9Z7GsgJJX18OFD4IyMlJBIJMnHOtkRGhoK/A8vXLjQ4ydVVdWZM2dKlvj6+uLx+N6V5OfnQxCkra3d5y7u3LkDQdDChQvnzZv3ySefEIlEPB4fGhoKZoYYGRmhUKi0tDSwcltbm7u7+5QpU2JiYi5fvkylUt3c3Nra2rq6umbOnAnDsKTX0Z07d9zd3Xk8HofDMTExWbx4MShvbm62t7cH/+vmzZv19PRkdwcMCAgICgpCFq9evYrBYGS0r/74l5iAliVvMRgM5urVq3Kwo62tjUwmwzCcl5cnWQ7mXM+bN0+ycO7cuWCuUo9KRCLRb7/9lpSU1OcuHj16BNpasJiYmAhBEHJ0tbW1EAQhbyR27txJIBBYLBZYZDAYWCx2x44dYrE4ISEBgqAffvgBqTk4ODg6Ohp8HzduHCKmrVu34nC45uZmsGhhYbFgwYIPPUPvIDg4WLLjHx8fDybryWh3ffKvyRIgukNXV5dkCRLdQaaAeSlisXjdunWSMUz6nF4HhjN6/wTD8Oeffz5jxozB7BGMLzQ1NYFFAwMDIpHY0tICFmNjY11cXJAoFPr6+i4uLrdu3YIgyN/f38rK6syZM2AOFpvNTktLA6+9e3Dv3j0nJyfgmwtBkKOjY2Zm5uDOx3vT0dEhOeeOy+WiUCg5x2n5l5j09fVBzwkpsbS0LCwslLURHA4nKCgoNjYWOO788ssv/28fCoXH4yX1DUFQZ2cngUAY4ixyoEXJYTYY/t+om0gkotPpPeICGBoa0ul0kUgEw/DmzZtramru3r0L2rZVq1ZJdvIQqqurm5ub9/9DZWVlQ0PDUGwegJcvX1pZWSGLdDqdTCbLeaL9v3ZmY2OjoqLy7NkzpGTGjBl3795F5s7KiM2bNy9ZsmTq1KknTpzQ0tI6cODAq1evkF/HjRuHtB+A+vp64DQtZ2AYBhJcu3aturr6qVOnIAi6dOnShg0b+tvEwMBg2j8cO3YM3GqlTnFx8atXrySb5Ozs7IkTJ8piXwPwLzFhMBhfX9/bt28jJWvWrKmurgbNu4y4ceNGaWnp/v37IQgikUhHjx4FPjpIm+Hl5VVeXo4ImsfjlZeXT506VXYmoVAoU1PT+vp6ycLa2loKhQLERCAQPv3004cPH0ZFRVEolP7itBgbG4tEomn/RhYGHzt2zMLCAjknXC73wYMHAQEBstjXQPToQ0VHRyspKVVWViIlq1evNjExQXqR0oVOpxsZGfWYO+bn5wdBUGRkJFgEg5ZgFAoMRMEw/OLFi961iUSi8+fPD7IDXldXB0GQ5LOqurr6unXrwPddu3bh8XikA85kMnE43M6dO5GVKyoqUCiUsrJySkqK5F4kO+CbNm3CYrGSPjyyIDU1VUlJKSoqCik5c+aMsrIyiEsmT3qKic/nm5mZSY53tbS0mJqazp49W7rO3UKhsKyszNPTc8eOHZIPHd3d3QkJCTAME4nE9PR04DX1008/mZubx8XFXblyhUwm//zzz33WOZihgStXroDFkpISCIL2798PjovNZqupqS1fvhw8JLa1tbm5ubm5ucXFxV2/ft3W1tbDw6O9vV2ywrlz59rY2EiWsNlsExOTgIAAYHZ9fb2NjY2WltamTZu+//777du3S90/pL6+3tDQcP78+cigLpfLNTMzCwkJke6OBkMfXgPg0kdGXMRicWZmJhaLVbgj3xg9YLPZHh4eFhYWSAsqFou//fZbIpFYW1srf3v69meaM2cOhUKRnLd15coVJSWlDRs2jJR576OehoYGZ2dnAwOD4uJipPDJkydoNPr06dMKMalvMTU2NhoZGXl5eXV0dCCFd+/eVVFRWbx4seR1MIZCKC4utrKyGjdu3OvXr5HCoqIiHR2dRYsWKcqqfn3Ay8rKSCTSjBkzJH29U1NTyWQyhUJ5/PixvCwc41+IRKLjx48rKytPmTKlrq4OKa+oqDAwMHB3d1fgtMyBZqfk5eVpaGjMmzdPsn1qbGxcuHAhCoXasWOHTL0JxugNGEzCYDAHDhyQ9P4uLy+nUCiTJ09W7D/yjnlzmZmZ2trajo6Oks0peDmvpaWlp6d36tSpAUINjSEtmpqatmzZgsFg7Ozserh4x8fHa2houLi4yGj4ZvC8e0bv27dvXVxctLS0/v77b8ny5ubm7du3Y7FYa2vr6OjoMUnJiJaWlh9//FFDQ4NMJp87d07yAUgkEh0+fBiFQq1evVry7qEoBhVroKOjY9WqVWg0etu2bT3GWiorK1esWIFGoykUyrFjxwYIGDfG+/L69euwsDAQ8fe7777rcebLy8t9fX2xWOypU6cUZ+O/eI8oKODWRqFQek/klTzsL7/8socbyRjvBZ/Pv3fv3qJFi/q7RLu7uw8dOqSiouLg4KCoWU198n7xmZhM5sqVKyEICgwMlHQSBbS0tBw+fHj8+PEQBE2YMOGXX36RfNwY450UFBRs27aNRCLBMOzt7d1n5yEpKcne3l5VVfXw4cPDrWvxIZHjEhISQFDidevWVVVV9V4hJycnLCxMR0cHhUI5Ozvv27dPcmBtDEmEQmFOTs6+ffucnZ3Bu+Hw8PDeFyoYkASvcufMmSP58nT48IExLQUCwaVLl8zNzbFYbGho6Js3b3qv09nZGRcXFxQUpK2tDfxbwsPDk5KShkNXUeEwmcwbN258+umnwCt8/PjxO3bsSEtL6zNWbGpqKnAvmT59ekZGhiLsHRRDirbb3d199uxZExMTNBq9cOHCpKSkPs+FQCB4/Pjxjh07gPcWFov19PTcu3fvw4cPPyph1dfXx8bGbtq0iUqlgsQKHh4ehw8f7s+tgMvlnj9/3snJCYIgT0/PR48eyd3k90MKccC7u7tv3LgBWmAbG5uTJ0+2trb2tzKTybx582ZISAg4oWg0mkqlBgUFHT9+PC0tbfhHJ34vgEfv8ePHg4KCqFQqDMNoNNrZ2TksLOzmzZsDnKXy8vKdO3dqaWnhcLjVq1fLYgasLJBmhgIajRYZGXnhwgWBQODn5xcYGLho0SICgdDf+jU1NU+fPgW5CfLy8tra2rBYLJVKtba2trW1tbGxASnC+vSIHYa0t7fTaLSSkhKQrqOkpASM9BoaGk6aNAkkKXBzcxtg3hiDwYiNjY2NjX369CmJRAoODt68eTOINjsikH7uFDab/eeff8bExCQnJ4NkIIGBgTNmzBhAVcDt+tWrVzk5OYWFheCfePPmjUgkwmAw5ubmIGUKwNTU1NTUVE9PT1Ei6+zsrKmpof9D1T9UV1eDaYA2NjbgenBwcJg0aRLwrB+A2tra+Pj4mJiY1NRUNTW1hQsXrlixwtfX9515V4YbMszq1NjYePPmzZiYmKdPn2IwGC8vr4CAgNmzZ4P5u++kq6urtLSURqO9evUKSeZUXV3N5/PBCjo6Onp6eiBtF0iMCabCgYSqIM0XSKuqoaEB3G0lszoJhcK2tjbwHaQRA9HMQJIxDofT9g9MJrOhoaGxsRGkVeVwOGArPB4PlA0kbmVlRaVSzczM0Gj0O49OIBA8ffoUJHYqKChQVVWdO3fu8uXLAwIClJWVP/SUKxh55JtraGh48OBBQkJCYmJiS0uLmZmZn58fSDb3vvMCRCIRg8GoqqpqaGgACZaamprAF5BvDohg6DaD3HNEIpFIJOrp6QGx6unpgVRSIEXY+8aEEQgEBQUFGRkZqampDx8+ZLFYFhYW4ALz9vYeBemj5ZoJUygUZmdnJyQkPHr0KCcnh8fj6evre3p6enh4uLu7T5gwQVoXJZvNRtLGIbnkBkheiOSkAwkLCQQCkiB6iLS0tOTm5oKEhVlZWRwOR0tLy93d3c/PLyAgAAzwjhoUlqMXXKYgM+SjR4+amprA2wMqlers7Ozs7DyY3sYwhMFg5Obm5ubmlpSUFBcXl5aWisVi5Jrx9PR0cnIaHXljezMssodnZWX5+/svWLDAyMgIJEyuqakBvSILCUACcekGHPtgRCJRdXU1yB6O5BCvrKzs6OhAo9GWlpYODg4gbbWjoyPI5DTqUbyYMjIyZs+e7enpeevWLeQ219zc/OLFCxqNVvEPb9684fF4oNtraGhIIpEMDQ3JZLKBgQGZTCaRSFpaWqCXo66uPvTbJUioymaz2Wx2S0sLk8msra2tr6+vra1taGiorq5uaGjo7u4GyX2ByoHcJ0yYYGdnNwo6QB+AgsX05MmTOXPm+Pv7R0dHD5xIFLQEFRUV1dXVNTU14H8Fn0wmE+gMAYfDAVWBYAGS3SM1NTXwyN3Z2QlmnSMdKaFQyGazWSwWm83uMYmZQCAYGRnp6emh0eiKioqwsDB9fX1zc3MLCws5JHUdKShSTNnZ2X5+frNmzbp+/foQx1TYbHZzczPSlgDAg32PfjciFBwOB3rZiNTAE5yGhob6PwBFamlpITEhXr16ZWtre/HixaCgIGmcg1GFwsT08uVLHx8fFxeXO3fujKxE7OvWrUtJSaHRaCPLbHmgkJc4NBpNT0/P19d3JKY5qKmpUVFRUWDs9mGLAlqm+vp6Nzc3EomUnJwsGVJoBLFt27br169XVFSAEfYxAPIe8OByuWCm1J07d0aokiAI2rNnT2dn55kzZxRtyPBCrmISCARLly6trKz8+++/e4TSGlno6elt2LDh+PHjYHRgjP8hz3vqjh07VFRURop3zsDU1NRgsdjff/9d0YYMI+QnpmvXrkEQdPHiRbntUdYEBQVZW1uPpZFFkJOYXrx4oaqqCqLVjhpevnwJw/Bff/2laEOGC/J4mmOz2U5OTubm5g8ePBhxDl8DM2vWLB6PJ6NIlSMOeXTAQ0NDuVzu1atXR5mSwBjB48ePS0tLFW3IsEDmYjp//nxMTAwIHyjrfckfPz8/ExMTJKfZx45Mb6I0Gg2Px4eHh8t0L4rlm2++MTAwGAuoJ9s+k0gk8vb25nK5WVlZI2WGyQdQXl5uZWV1//79WbNmKdoWBSPD29zZs2ezsrJ+++23UawkMBnX3d398uXLijZkGCCjFq+2tlZDQ2PPnj0yqn9Ycf78eWVl5QEmVX4kyOo2FxgYWFBQUFBQ8DH4HLJYLD09vaioqOXLlyvaFkUik9tcZmbmrVu3jh8//jEoCczLc3NzA6nDPmak3zKJxWJXV1c1NTWQCvEj4fDhw8eOHWMymaN15slgkP6RX7t2LS8v7/jx41KveTgze/bsxsbGvLw8RRuiSKQsJqFQeODAgbVr106YMEG6NQ9z7O3tTUxMQOrfjxYpi+nGjRtv3rwJDw+XbrUjAn9//4+82yRNMYnF4sOHDy9btmyUzXoeJNOmTcvNze3s7FS0IQpDmmL666+/ioqKPs5mCYIgV1dXPp//4sULRRuiMKQpphMnTvj7+9vb20uxzhGEubm5tra2ZFLajw2p+YRUVlYmJyf/+eef0qpwxAHDsIODgxzyYw9bpNYynTlzxsjIaPbs2dKqcCRiY2PzMfs2SUdMIpHo2rVrn3322WCCpo1iqFQqjUZTtBUKQzq3ubS0tLq6uqVLl/Yor6ioAMFxLCwsQKDPoqIiExOTAYKEypreJvXJixcvWCwWiJk8eAdRMzOzlpaW9vb2D56c2d7eXlVVJedROhaLBZ4bjIyMLCwsPrge6bRMt27dsrOzs7Gx6VGOxWIrKyt9fHzi4uIgCCotLZ0wYcJnn30mlZ1+GD1M6g80Gh0ZGenj44NEsBwMBgYGIODpB5u3fv16e3t7OXe8lJSU2trafH19T548OZR6pCOmlJSUOXPm9C43MTGRLDc2Nl6+fPnixYulslMAnU5/r5mQPUzqjwkTJnxA8wDExGAw3ndDhEWLFi1btszU1BQsghSXyK89FqUFgUCYP38+iCE7FKQgJhaLVVpa6u7u3uevkiYSCITo6OgVK1YMfacICxYsaGhoeK9N3uusvdfKWlpa4IS8lz2SLF26NCYmBrlL/vnnn4cPH0Z+7bEodYaoJyn0mfLy8kQi0eTJkyUL29raSktLlZWVES+U7u7up0+fQhCkq6tra2vLZDJBX9XFxQWPx9fV1cEwDCYdNDY2VlZWGhkZ9ejT8Hi8kpKSzs5OTU1NMzMzHA535cqVgoKCzMxMXV1dNzc3EOOmv817mzQYMBjMmzdvmEymmZkZMO/Nmzd0Oh38amJiYm5uXl5eDm5turq6ysrKOTk5QFUYDMbDw6NHhenp6QKBAIKg1tZWTU1NcDaEQmFJSQkOhwOtGjgnzc3Nhw4d0tPTe/z4sb6+vo6OjuQiyB0iEomKi4uFQqGVlRU4rpycHA6HA6pls9k0Gs3MzGyQk/ExGEx7e/urV6+UlJRsbW2VlJRAAiBkhalTpwqFwoyMDLAI7ER+lULLxGAwsFgsiUQCi2KxeM+ePRQK5dSpU5cvX/7mm2/+tycUqrOzc+nSpfv27QP36ZSUFB8fnz/++ANEs/zzzz+FQuEXX3zh6OgYHR29aNGi6dOnNzU1gc2PHj1qbGwcERFx+/btjRs3jh8/PjEx8erVqxAEPX78+MGDBzwer7/N+zNpMCxfvnzNmjXr1683MDAICgri8XgoFOr48eM+Pj7Jycmgb47BYBISEr755hsYhgkEwtu3b318fA4dOoS49zAYDBByHnDw4MGEhAQYhkNCQrZv337ixAljY2M/Pz8lJaW4uDgfH583b950d3dHREQUFxfX1NQ8ePAgPz9fcrG4uBjEAjU3N9+zZ8+5c+eMjY3BJBmRSBQSErJixYqQkBA3Nzc/Pz9jY+Pbt28P5mATExNnzZq1bdu2adOmmZiYJCcnwzDc3Nw8Y8aMkJAQHo8HwzAKheru7g4ODi4rK+v58D50Z81jx44ZGhoii6dOnYIgCMnBWldXB0FQREQEWBw3btzixYvB96SkJAiCNmzYkJWVdfny5cjIyIiICAiCCgsLQVIobW3tzZs3i8XiK1euQBAkmTTR09NTLBafOHECgqDq6mpQ2N/mA5vUH99//z1oP8DipUuXIAjatysd0sQAABmpSURBVG+fWCzOzc2FIEhygvKGDRtu3rwpFot1dXVPnjzp6OhIpVKRX1etWjVv3jxk0dbWlsViicViDw8PQ0PDmzdvlpWVBQQEIEcKDkEsFmtra69btw7ZUHKRy+WSyeQlS5aAxf/85z84HK6mpgZUO3HiRDBhhsVimZiYTJ48+Z3/IxqN/vLLL8H3lpYWJycndXV1cPjz5s3DYrFIDuDa2lo7O7veNUihZRIKhZIKPXPmjLW19cyZMwe5+cKFC11dXdesWRMUFBQVFWVvb29nZwdBkLKysqen5507dyAI+vXXX8ePHy/Zcf7uu+96V9Xf5u9rUp8EBwdbWlqCtnDixIlOTk7Xrl0TCoXgDp6SkjJ//nwIgvh8PhaLXb16dUlJycuXL8HT/u3btx88eNDY2AhBUH5+vpWVFQi2CZ7GAwMDLS0tY2Nj38uepKQkJJckmMHH4/H+/vtvsIjBYMCfoq6u7ubmJtkuDgZNTc2vvvqKzWbHx8dDEPT55593d3dHR0eDX69fvx4cHNx7KymISUtLq7W1FXwXCoXFxcWDTGjRAzweX1ZWhsPhHv8Dj8djMBhCobCgoMDS0lJyZT8/v9419Ll5d3f3B5vUAysrK5BZDzzDM5lM8OclJCTMmjUL9NiAmFauXIlGo2NiYiAIunnz5sKFC/l8/vXr1yEIiouL6/MR5H2jVZWVlUEQVFdXBw4WLL59+7b3mkpKSj3ivQ4GcMYqKytBukQDAwNkBs7Nmzf7DOkphQ64jo4Oh8Pp6OjA4/GdnZ0ikeiDh+y6u7u5XO7jx4/Boqurq6urq0Ag4PP5A+fxGWBzLpc7FJMkAR1SsVgMw/DKlSu/+uqry5cvz549+9q1a19//TVigLq6ur6+vq+vb0xMzKFDh65duxYdHV1YWBgVFfXll18mJiZ+++23QzcGDIiUlJQgD7P79u3z9PQces0A0B0EVw4ajV67du2hQ4dAjHwQOruPTYa+V0dHR7FYnJeX5+XlhcfjcThcfX39h1Wlq6trZGS0f//+3uWDGQnsc3OxWDwUkyRhMplGRkbAy1tdXT0wMDAmJoZOp9fW1jo6OoIsMWKxGJzo1atXr1mz5vr163g8nkQirV27dseOHTExMVQqVSrzLEDI6NWrV0+ZMmXotfWGyWSCx1WwuG7dup9++uny5csoFOrTTz/tcxMp3OZMTEz09fWzs7PBQMWUKVPS09M/bKzF3d09OzsbSXWCMGvWrOzs7Kqqqh7l4H8FHZf+Nh+iSQjNzc05OTmS/bbPP/+cx+OtXLkSmeEEJAuewxctWoTH40NDQ9esWQP+dSUlpdDQ0PcaZkOhUMjR9VgEA3tIJ0nqgJA1/v7+YNHc3Hz69OlXr15NSUnp73W+dEbAvb29Effn7777rru7OyAg4Pbt2ykpKRcuXBh8Pd988013d7e/v39cXFx6evq9e/f++usvCIK+//57HR0dd3f3//73vykpKSkpKefPn+dwOGZmZhAERUZGpqSkVFRU9Lf5UEyi0+lsNruoqGjlypUGBgaSzZ6np6eNjU1ubu6qVatAyevXr9FotKGhIegDLVy4EIZh0DHX09ObPXu2kpISyLY7SMzMzFJSUpKSkh48eNBj0c7ObsWKFYcOHdq/f//jx49TUlIuX778vuO3PWhtbQX5saKiok6fPn3w4EFwLID169fX1tZ6eXn197IS3fue8gGgUKiff/55/fr1ampqIANYVVXVkydPmEzm6tWrX7161dzczGKxrl+/zuPxxGJxcXGxkpLSlStX1NXV6XQ6h8NxcHCAIEhfX3/JkiX19fWJiYm5ubk8Hs/X11dbW1tDQyMoKAiG4fT09PT09OrqapAacNy4cUKh8MWLF3V1dW5ubra2tn1u3p9JJBKJQqH0d1BWVlZWVla3b9++fPlyUlLSlClTLly40CMfAZfLJRKJoO2BICg2Nra2tnbbtm1gUUdHx9jY2MfHB1k0NTUF+WfByFlNTQ0OhyssLATPd5GRkUlJSTo6OjQaTSQS2djYODk5VVRU5Ofna2lpTZo0qcfiwoULDQ0Ns7KykpOT3759O27cuMmTJ585c+bNmzc4HK6qqsrb2/vcuXMvX77U1NQEbyQH+BO9vLyampquXbt27dq1xsbGH3/8scftzNLS8tSpUydPnuw3KcM7hx8GA5fLVVNT+/XXX6VS2whi8+bNSUlJyOLSpUsXLlyoUItkSF1d3bRp0wZYQTouKCoqKsuWLTtz5syWLVuG/r5Qbjx9+rS/l8RYLLa/t41MJhPkpKuvr8/LywMDp4Bnz5711zlVOAwG49WrV/39amlpCd5S96aiogL4pRw9enTLli0D7EJqbrtbt269cOFCYmIi0mUb/kRGRiIjZD3Q1NTsT0zp6ekgp9m+ffsOHTqElFdXV4M7i8zsHRIFBQXgTUCfbNq0qT8xbdmyZdu2bQUFBYWFhT///PNA+5BiM+jj4wPeCYxucnNzP/nkkwULFiQmJkqWR0VF4XA4LperONNkwtdff+3v779jx4729vaB15RmrIH79+/PnTs3MzPT1dVVWnWOIJYsWdLW1paYmKhoQxSGlANXTJs2DYPBgDe4HxXt7e0kEunEiRPr1q1TtC0KQ8rTw3/44Yfk5OSUlBTpVjv8uXv3rkAgWLhwoaINUSTSD6nj7+/f3t6ekZExgh7rhs78+fOFQiEYI/1okX5InUOHDmVnZwO/nI8EFouVmJi4bNkyRRuiYKQvJmdn59DQ0O3btw9xaH8EERsbC8PwggULFG2IgpFJTMv29nZbW9tp06Z9JNHWHRwcnJ2dL168qGhDFI2MBifu3r0r6Sk7msjMzEQcWMViMXjaeP78uUKNGhbIMEPB0qVLjYyMGhsbZbcLhbBs2TIikQgyF4rF4k8++cTLy0vRRg0LZCim1tZWMzOzgICAUZaRDbyoQqFQZmZmv/32GxqNBlMJxpBt7pTs7GwsFnvkyBGZ7kWedHV1IbMngGseDod79uyZou0aFsg8eeEvv/yipKSUnp4uWVhUVBQXFyfrXcuC3vF0lZSUYBhevHgxnU5XtHUKRuZiEolE8+fPJ5FIYF6HWCyurKzU1dU1NDQEjnIjC+AE3fs5BoPB4HC4AwcOdHR0KNpGhSHzCOgwDF+7do1MJs+ZM4fFYjEYjGnTprW2tjKZzHPnzsl671KnsLCwz7xCfD4fzF7/qCNUyUeztbW1RkZGPj4+lpaWyJ+ho6Mz4q7j/jxfYRjesmXLKHvUeF/klz08NTUVhUJJXrhKSkojrm+ura3dW0YoFOrkyZOKNk3xyElMXC63zxBsampqLS0t8rFh6PR+QYRGo7FY7NjQAEAeWWP4fP7ixYuzsrJAKBlJOjs7R1CWFRA7AEFJSYlAIKSkpAQGBirOqOGErNUqFAqXLVs2QK4jFRWVkTJKfuzYMaTDh8FgjI2Ny8rKFG3UMELmLVN5efmbN29EIlF/yVUFAoFMo6FJERDpBihpwoQJOTk5PcJpfOzIR7M5OTmrVq1Co9F9SgqDwSAxloYzIPkCGo2eP3/+6Js4MHTk9zQnFosZDMa+ffuIRCIajZb0w8RisRs3bpSnJR+AQCAAQXM2b948lni+T+QqJkB7e/vZs2fHjRsHwzAyUoBGoysqKuRvzOCh0WgoFOqXX35RtCHDF1klfH4nIpHozp07P//8c2ZmJgaD4fP5q1atAnHZ3hcul9vY2NjU1NTW1sbhcDgcTnt7O5vN5nA4PB6Py+XyeDywZnd3d0dHB7KhhoYG0kASCAQMBgOm6uLxeA0NDTU1NQKBQCQSdXR0dHV179+/z+VypRsqeJShMDEh5OTkHD16NDY2ViwWFxYWUqnU3uvweLzq6mr6P7x9+7apqamxsbG+vr6xsVFSH6CRIxKJRCKRQCAoKytjsVgkKBv4CXwXiUSSwXdAkMn29nYQuKx3WB9NTU0SiQSEpa+vb2RkRKFQKBQKiML7MafmRVC8mAA1NTUnT55sbm4GQTxoNFppaWlZWRmNRnvz5k1dXR2wU1VV1dTU1NjYWE9PT1dXV09PD/mDdXV1iUQiHo+XVspyIKy2tjYQZaa+vr6hoaGpqamhoaGuru7t27e1tbV8Ph/0+YyNjc3Nza2trW1sbMAniPP8UaF4MXV0dOTn5+fm5ubk5OTn51dUVIC7kpGRkbW1tZWV1bhx40xMTEAz0G8wF0UgFAoZDAadTq+qqqLT6a9fvy4pKaHRaCCqmIaGho2NzcSJE52dnSdNmmRjYzP4HCwjFMWIiUajpaamZmRk5Obm0mg0oVCoo6Pj7Ozs5OREpVKtra2tra2lEoVSITCZzNLSUhqNVlxcnJubW1BQ0NnZqaqq6uDg4OLi4uXlNXXq1EFGeR9ZyE9MNBotJSUlNTUVRNzC4/FTpkxxcXEBFy6SLWT0IRAIgKpycnKePXv24sULEMjL29vb29vbx8dn1AhLtmISCoWZmZnx8fF3794tLS3F4/Fubm4eHh6enp5eXl5g2OZjg8PhZGVlpaenZ2RkpKamCgQCJyenuXPnzps3b+LEiSN7GrQsxhu6u7vv3r27YsUKDQ0NkNIvPDw8PT2dz+fLYncjl7a2tj/++OOzzz4DjZOZmdm2bdtycnIUbdcHImUxZWVlbd68WUdHB4bhqVOnRkREDPOhyGECaMK//vrr8ePHg8vv0KFDI86pXGoxLc+ePQuGiKytrX/44Yeqqiqp1PwRkpmZuWnTJh0dHRQKFRAQkJiYKBKJFG3UoBiqmOrq6vbu3aurq4vD4T777LOxST/Sgsfj3b59e/r06SCT4oULF7q6uhRt1Dv4cDG1t7fv27dPRUVFV1c3PDwc5BMaQ+q8ePEiJCRERUXF0NDw7Nmzw/kd84eIqaur6+jRo1paWjo6OhEREZ2dnTIwbIx/wWAwNm7cqKSkZGdnJ5kqbVjx3mIqKCiwt7dXVVUNDw9HcrGNIR/KysoCAwNhGJ49ezaDwVC0OT15DzHx+fwDBw5gMBhfX98R96Axmnj48KGJiQmJRLpz546ibfkXgxVTa2urt7e3iorKr7/+OlIeLkYxLBZr7dq1EATt2rVr+PwdgxJTTU3NhAkTjI2NkXSfYwwHoqKisFjsmjVrQHAfhfPu99h1dXUeHh4EAiEjI8PY2Fguw/JjDIqgoCASibR48WI2m/3HH38o3qdqYK11d3d7eXlZWVmNoKmSHxtPnz7F4XAgE7VieYeYtm/fTiAQioqKpL7jjIyM8PBwEN/o3LlzYJiqubn50qVL6urqX3zxxcOHD5GVu7q6du/ejUajx54f++Ts2bMoFCohIUGxZgwkphcvXqBQqEuXLslu94sWLYIg6D//+Q9ScvTo0dmzZ0uu8+zZMyqVqqysLJkYfowerFixwszMTLFRigYS06pVqyZOnCjThwUGg6GhoaGqqlpZWQnka2JiUl9fj6zQ1dW1c+fO3Nxc0IyNiak/3r59i8Vio6KiFGhDv2Lq6upSVVU9c+aMrC04f/48SC3P5XKpVGp/bfVgxFRWVgZSLvegoaHh0aNHjx496uzsZDKZWVlZvV/+NDQ0ZGZmInNB6+rqwCYcDgeIHvihd3Z25ufnZ2dn9xgzbG9vf/bsWXZ2dltbGyhpbGxEahCJRCUlJQUFBTJ9GfLJJ58oNqtWv2J6+vQpSGsvByNA0CNHR8etW7f2t847xUSj0WAYplAovX9qaWnZunUrBEEzZ8708vKys7ODYTg4OBj4VwkEgo0bNxoYGISFhbm4uPj4+IAZBHv37oUgKCoqav78+SgUCmQCNjc337RpU1hYGJlMBpEURSLR7t27DQwMNm7c+Omnn2ppaYWHh4tEotbW1n379kEQ9MUXX3h5eYF0wu7u7rJz6jp9+jSRSFTgsFO/Yrp58yYKhZLPa8WKigoVFRUYhgcYWH+nmDgczqpVqw4cONDnr9HR0RAE5efng0XQHJ47d04sFkdERCBxBDo7O7W1tTdv3iwWi0Fuqg0bNmRlZV2+fDkyMtLOzu7gwYOghr///hsMQJ8+fRqNRhcXF4Py9PR0GIZPnTqF1HD79m3wE9jR/fv3h3CqBgIkhQZzthRCv2KKjY2Vm5jq6up0dHQgCFq6dGl/6wyxz9RDTCKRiEKhTJo0SSwWOzk52dvbI2suWLDA2NgYkQJy2+VwOAYGBkuWLOkRHs7R0dHFxUWyxN7e3sHBoXcNpaWlEASdPXv2ww7hnSQkJEAQxGazZVT/O+l3mMvIyEgkElVVVclhoGvt2rXfffedo6PjzZs379y5I+s9gnBvVlZWlZWVEASVlZXhcLjH/8Dj8RgMhlAo7LEJHo9fu3ZtXFwclUo9fPgwg8EA5UVFRT1mQ1hYWJSUlPTeKZjqJBKJZHRQr1+/VldXV+Csnn7F5OTkpKqqKoc0hBEREVgsdsuWLRcuXECj0aGhob1n08oCFRWVzs5OMGecy+UiYnJ1df3222/7nGfxww8/REdHUyiUvXv3jh8//q+//hIKhQKBoMeEOCwWy+fze8tR1iQlJbm7uytySsIArdbq1asdHR1l2qHLz8+nUChIsK9du3ZBELR+/frea0r3NicWi93c3KytrcVisb6+vr+/f+9NetykJHn9+vX48ePt7OzEYrGurm6PZyg/Pz9dXd3eNZSXl4Ms0x92CANDp9MxGMyVK1dkUfkgGehtzq5duwoLCy9fviwjHXO53FWrVp09exZ0mCAI2r9/v4WFxfnz5x8/fvwBFZaXlw8yL1lra2teXt6sWbPAE1Z2dvZgmsOffvoJfDEzM1u2bBnYxM/PLy8vD2mHeDxeTk7OjBkzPsD+oRAeHm5iYrJ06VI57/dfDKy1r776Co/Hy8hZYMOGDb3HAh49egTDsIWFRY9oWoMZGkChUKDv3BvQMiUmJnZ1dTEYjMWLF5PJZCaTCZIOqKqqurq6xsbGpqWl3b17F7gy9m6ZDA0N79+/39XVRafTnZyctm3bBh5FtbW1t2zZ0tTUxGAwVq1apaOjA+bkyK1lioyMRKFQDx48kHrN7wV6//79A0ht+vTpSUlJFy9eXLlypaqqqrQUXFRUtHXr1qqqqo6ODhaL5eLiAsqTkpJ+++03HR0dNTW1+Ph4GIbNzc3Dw8MvXbpUXl5uYmISHx//6NEjgUBgY2PTo04VFZWqqip/f/+pU6f2ucdbt27x+fyYmJhbt25RqdTff/8dxJbQ19dfsmRJfX19YmJibm4uj8fz9fWtq6s7e/asuro6nU7ncDgODg6gB/3gwYMLFy6kpaUtW7Zs165dKBRKS0tr5cqVeXl5kZGR9+7ds7GxuXjxIoVCqaioOH36tLq6enV1NUjH8PPPPxMIhObmZiMjIyMjI2mdzIyMjJUrV+7du1fxuabfKbe6ujozMzMbG5sR7V0JWqaCggJFGyJlEhIS8Hj8okWLhkM8+3d7wJDJ5IyMDCwW6+HhUVhYKBeFywrZPZYrBDA6HxgYeOPGDcU7Mw0yR6++vv6TJ08sLCxcXV2B267sDRtjIFgsVnBwcHBw8I4dOy5evDhcgvUMvhHj8/kHDx7EYDA+Pj5IiqYRwbNnz1auXOnt7R0cHHz9+nVFmzNUEhMTjY2NyWTy3bt3FW3Lv3jvqU4vX750cHDAYrFhYWFjDiFyhkajgalOS5YsGYaR+D9kEiaPx4uIiNDR0dHW1j569OhYRGw5UFNTExISoqSkZG9vr3CPyv4Y0vTww4cPq6mpgenhIyIq/EgkPz8/JCREWVnZyMhoFE4Pl6S+vn7fvn16eno4HC44ODgrK0tKhn3s8Hi8uLg4b29vCIIcHBx+//330Ry4QpLOzs7z589PmDABgiBLS8uDBw+OrB76sCIjI+OLL77Q0tJCoVBz585NTk5WtEWDRcrBvp4/fx4WFqanpwfDsJeX17Fjx8rLy6W7i1GJUCjMyMjYs2cPyHNvZ2d35MiRERdYRiZhCPl8fnx8/MqVKzU1NUH4r507dz558mQsDGEPWCxWbGxscHAwCEltbm6+ffv2vLw8Rdv1gcgpQOq9e/dKSkpUVVWdnJw8PT1nzJjxkQdITU5OTk9Pf/bsmVAoRAKkOjs7K9q6ISG/0M3l5eUgdPPjx48ZDAZ4UT9p0qRJkyY5OzuPGzdOPmbIHz6fX1hYmJubm5ubm52d/fLlS7FYbGtrO23aNG9v72nTpiEeOCMdxQSVLy8vf/LkCQgqX1paKhAINDQ0nJ2dJ06caG1tbWtra2VlBSL1jkRqa2tBUPmioqK8vLyXL1/yeDw8Hu/k5DRp0iQQVH7UCEgSxae74HK5BQUF4MItKCig0WjAm1ZfX59KpVpZWZmbm1MoFJDxgkQiKdZaSQQCQW1tLZIeqLKysqSkpKysDDjNaWtrU6lUkO7C2dnZyspKMnP6qETxYuqBSCSi0+k0Gg3kIUES8YC3y8rKyhQKxcjIiEwmIwmWdHV1wXeQ1AvJ4TREWCxWR0dHW1sbSL7DZDJBIjImk1lfX0+n05F5BzgczsTEBDjqgEQ8VCp1WKV5kQ/DTkx90t3dXVNTA5KDVVVV1dTUNDQ0gKmSTCaTw+H0WF9TUxOPxyPCAg+VYFIKcvcUCATt7e3gO5/PB5UAAYGkdT3qBImjdHR0SCQSiUQyNjYG7aWpqSmZTB7ZmQWkxMgQ08B0dXUBYbW3twMpsFgs8J3L5QqFwra2NrCm5HdJYaFQKHV1dQiCQJY6AoGgpqamoaGBx+PB+yJdXd1Rf5MaOqNBTGMMExTvnjfGqGFMTGNIjTExjSE1/g9YFLsJcblzXAAAAABJRU5ErkJggg==", "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "display(term)" ] }, { "attachments": {}, "cell_type": "markdown", "id": "d85397d2-7563-4f5b-99ce-402ce306a9fc", "metadata": {}, "source": [ "## Figure 4\n", "\n", "Unifying two OSF terms" ] }, { "cell_type": "code", "execution_count": 13, "id": "c534af51-ce0d-49d8-b5ac-a67133098f41", "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "X0 : slasher(directed_by -> X1 : director, written_by -> X1) 0.5\n" ] } ], "source": [ "from fosf.reasoning import unify_terms\n", "t1 = parse_term(\"horror(directed_by -> director)\")\n", "t2 = parse_term(\"thriller(directed_by -> X:person , written_by -> X)\")\n", "unif, deg = unify_terms([t1, t2], ftax, return_degree=True)\n", "print(unif, deg)" ] }, { "cell_type": "markdown", "id": "b7b0bce9-0d47-4bcf-8d6f-b60930dbe12f", "metadata": {}, "source": [ "We can draw the unification, including the tag mappings from `t1` and `t2` to the unifier." ] }, { "cell_type": "code", "execution_count": 14, "id": "28d4a1f3-4d5c-4338-b64c-dcc70a295624", "metadata": {}, "outputs": [], "source": [ "from fosf.utils.draw import unification_to_agraph" ] }, { "cell_type": "code", "execution_count": 15, "id": "790a67a9-f910-4a60-aa38-9945ac85e6e2", "metadata": {}, "outputs": [ { "data": { "image/png": "iVBORw0KGgoAAAANSUhEUgAAAfwAAAE8CAYAAAAlugOnAAAABmJLR0QA/wD/AP+gvaeTAAAgAElEQVR4nOydd3gUVffHv6mQQkJLoSUQehMwgJRIR0QBFREFQbEhdn0t2Ov7vvaf+vqKCiiCL9JUEOkCCoQmhA6BUBMCISGBdEjZPb8/vgyzm2wq2Z3N5n6eZ57dnZmdPTtz7z33nnvuOW4iIlAoFAqFQuHKzHc3WgKFQqFQKBT2Ryl8hUKhUChqAErhKxQKhUJRA/A0WgCFA7h4EcjI4FZYqO/TuHQJuHxZ/1ynDuB5pWh4eQH+/nzv4wMEBnLT9ikUTo4IkJ5evApkZABmM98XFADZ2fp3vL0BPz/9s2WVCAwEAgL4WquWI/+JQnFtKIVf3TCbgZQU4Nw54MwZ/TU5ma+pqXrLlpEBZGbaRw4PD7Z4devqnYDQUG6NG/O1SRP9c9269pFDUePIyQGSklj0z53j+5QUFv+UFCAtjcVeK/5ZWfaTpVYtKv+AABbxunVZ5IODWexDQvi5USO+DwqynywKRVm4KS99J6SwEEhIAI4d07ejR/l64gSQn6+f6+8PNG3K1qRpU6BBA10Ba5ulUvby4vcCAwH3KzM6tWoBvr76NS2HPpcv0wIAALm5xTsT6en68ElrgbUOSF6efs3AQKBVq+Jb69aUXaGwICkJOH68+HbiBHD+vH6emxuVq6WCbdhQV8LaVq+e/t7bm9/199erg7s7i6hGUaNXejotBbhiHMvMLL5lZPDYuXPWHRDLalC7NtCype0tPFyXTaGwA/OVwjeajAxg715927MHOHhQb20aNLBWjq1aAWFhbNmaNLG2Ozobqals/c6eBU6dsu7AHDumdyTq1we6dgW6dNG3jh311ljhsmRnAwcOAPv26dv+/VSwuNIXbdHCWjFGROij5uBg5y8maWl6XzghoXgn5sIFnuflBbRrB3TuDFx3nb41aWL0P1C4CErhOxSTia3bpk1AdDTw99/AyZM8Zqn0unYF2rencq9Xz2ip7YMIh0BHj7KDs2ePdWfHy4tKv08foG9f4MYbgWbNjJZacQ0UFrJPu2ULsHUri/+JEywKdeoAnTrpSq59eyr3pk11Q5SrcvEiFX9cnN7pOXAAOH2ax+vXB66/Hujdm1ufPtbWCIWinCiFb1dMJmD7duDPP4HNm7llZrK29u3L2qspeaXMSGEhcOQINUNMDLVDTAy9qsLCqPijooAhQ9ghUjgtubnAxo0s9tHRwI4dnH+vV49F/4YbdAXfogXN8wqdixd1i8fOnawKR4+yA9ShAxV/nz7A4MHsGCkUZaAUfpWTmkoFv3YtsHQp7XiNGgGRkbqi6tataoYtly9zQjM5mdv585w0vHCBNtHsbHosZWfrc+4mk/6qkZ1Nharh62vtfly7Nj30a9fmxKfmoeTvzy0wkN5IQUGcatAmUoOC6Nx3reTmArt26Zpj82a2hhERvJ8jRgBDh1I+haGcOMGi//vvfL18mY+pb1+9ClRV8ceVufXkZFY7rfinpOhz6lrxz8mxrgJFi7ylqwqu+KQGBFj/lub2EhDAmTStKgQE6O8bNuQWEsLpBq0aeFaRe3RGBjtOWjXYvJlya1VhyBBg+HC1iEZhE6Xwq4T4eGDePGDxYnbFPT2Bfv1Y8265hRNzlSEjg7a+U6est5Mnae/LyLA+39eXrUyDBtYK2d+fn7W1RX5+1t5BmjLXyMrS1y7hilt0fj5bFq0ToXUotM7E+fPcLFtRNze2fOHhQPPm+qu2tWxZOS+lwkK2dCtXAitWcAjk5wcMGgTcdRdw++38rwq7U1gIrF8P/PwzH0diIpXckCHAsGHcGjWq3LXz8tiBiI/nlpCgv4+PZ1/asrgBLOYhIfqyuTp1WDT8/PQq4eVVvMhbrj4FWNxzcvTPZrNe3TIyeEyrCtrnzEy942FZfQAq/aZNaaTSqoH2vkULVtnKcPkyZwhXrQJWr+aMmK8vm5/Ro7lV9toKl0Mp/EqTmgosXAj89BNtbfXrs3YNH87RZkW62GlpnLSLjQUOHeJrbCznuHFFcTZqxJbBsrVo1IgtSXAwvZicwYEvNZVDLM3ykJRk3VmJj9djAHh6cmjSsSM7RR07cvK2fXu2yOXl9Gkq/mXLgDVrODwbNQoYPx64+Wbl+lzFmM001S9YAPzyCx91jx7AyJFU8N27V2wEf+ECi/3hw5zNiY3l+1OndENUYGBxZakV/9BQvjZs6DyPWlP82uvZsyymCQncTp1i1dBa34YNWezbtQPattXfV3SqIzGRin/FCnbACgtp8r/7bvaD1erYGo1S+BXCbGZtmjaNr97ewG23AePGsaUrj7twdjbN0zt2cLN03AsMtFZ8HTpwnjo83LUifGRk8D/HxXFIonVw4uI4tPLyogdXjx5Az5587dChfHbRCxeARYtocdm0iS3cuHHAE0/wnioqzbFjwLffAnPnUll16UJFcvfd7LeVh7Q0umTExLAaxMToxd/fn8rOUuG1bs3i74qKKj+fnYATJ9jBiY3VOzxJSTwnMJAOe5GR+taqVfk6AdnZnFpZsIAWAIDjkcmT2Vy5ujOkohhK4ZeLjAxg1iwq+mPHaDp+8EEq+7JG1Rcvcjj055/AX39xJG8ycVjSoweHQz16qPU3uGIfPnYM2L2bnaGdO6kVcnJop+zVCxg4kFvPnmV3sBITqfinT+fUyODBwJNPcs6/KnwLagCFhVQa33zDOfkmTVj077mnfDNVx4+z3/XXX3w9cYL7mzal8urena8dO3LUriAZGVT8WqcoJoZ948JCdgL69KHZvl8/Nh9lVYWMDOC334AffuCzaNGCiv/BB1UwoBqEUvilcuYM8MEHrCUAMHEiFUaHDiV/x2SiR82yZVTye/bQbtelCzBgAL2WevRQXvnlxWSivXfHDmDDBt7T06fZ0erbl0r8tts4LCwJzTLzn//Q5B8WBvzjH2zxXMlyUoVkZQFffQX8978cbd50E/DYY8Ctt5beV0pJAZYvB9ato2I5c4Zz5TfcAPTvz9fISBVrqTJcvszFKzt2sPO0cSP9GHx9ueph4EA+n65dS7/O4cPswM2eTbecu+4CXnml9GZN4RIohW+T8+ep6L/+mpNrzz8PTJpU8uLX3FwqlN9+o6JPS6NNcuhQKvn+/TnHr6gajh2jNvnzT+CPP/i82rblJOVtt1GrlGSvPHoU+PJLYMYM+j68/jqfrbNHb3EQWVlU8p9+SpPzlCncSjPZ79vHYv/775yh8vbm6sl+/Vj8e/RQ/Sp7ceQIFf/GjexkJSVxLHHrrfSpGDiwZHeY3FwawD77jNaEsWOBN95Qit+FmQ9R6GRlibz+uoi/v0hoqMgXX4hcvmz7XJNJZPVqkfHjRXx8RNzdRfr2FfnoI5G4OEdLXnMpLBTZuFHk+edFWrYUAUQaNxZ56SWRgwdL/l5ioshjj4l4e4u0aiXy00+OlNrpyM0Vef99kQYNRAICRF57TSQtreTzDx8WeeMNkYgI3vLQUJGHHhJZvFgkO9uRkis0zGaRHTtE3npLJDJSxM1NxM9P5N57RVasECkosP09k0lkwQKRTp3YjN19t2rCXJR5SuFrLF8uEh4uUr++yAcflNxqxcWJvPKKSNOmbOl69xb5+muRc+ccLbHCFvv3s9MWFsbn07OnyFdfiWRk2D7/xAmRSZPY0g0ZInL8uKMlNpyVK9lXqlOHt64kRX/+vMjnn4t0785b26SJyAsviPz9N5WNwrk4c4ZFv08fKv+QEJFnnhGJibF9vskksnAhFX+tWiJvvily6ZKjpVbYEaXwJTlZZOJEtmAjRnDkZ4udO3mehwdbuqefFtm719HSKsqLySSyaZPI5Mm02NSpw2eWkGD7/JgYkeuvp7XmrbdE8vIcLbHDOXvWuujHx9s+Ly6Ot87Xl7fnrrtEli4tecSocD4SEjiOaduWzzsyUmT2bNvPsKCAHbuAAFpwVqwwQmKFHajhCn/tWpGGDTmyX77c9jnLltFUD4jccIPIokVUJorqQ3q6yIcf0tTv7S1y3320SRclP1/kn/8UqV1bpFcvDpFclJ9/ZoPesiVH+LZYu1bkpps4OmzbVmTaNGWudwXWrxcZNYpGrebNRf7v/zilU5TERJE772TT9/DDarTvAtRghf9//yfi6Skybhzn7osSEyMycCBbu1GjOE+sqN7k5YnMmiXSsaOIl5fIk0/STl2UQ4dE2rUTadRIZPNmIyS1GwUFNMO7udGFwVZDv3OnyNChbOiHDGFfWJnsXY+jR0Weeorz/E2bisycSZeYovz6q0hgIK0CJ08aIamiiqiBCj8vTzfNf/RR8ePJySL338/ub+/eIlu2GCGlwp4UFrJ1a9RIpG5dkY8/Lt7SZWSwo+ftzXNdgJQUkf79aZqfM6f48YQEkXvuYWegd2+RDRuMkFLhaJKSRB5/nH3gDh1sm/CPHhXp0oUuTqtXGyGlogqoYQq/oEBk9Gh2V1etKn58+XJ6toSHi8yfr4Y1rk5WFl3Na9fmtM2JE9bHTSYed3MTmT7dKCmrhPPnRTp35pysLdeTH35gtWjThiM6Rc0jLo7+GYDIAw9wJsySnByRCRPYB162zCgpFddADVL4ZjPXDfn6Fh+6XL5M866bG0t0SR7dCtdk3z5qw4AAkR9/LH78nXdo8Zk71wjprpmLF2mODQsrbpJNSRG57Tb+veees23iV9QslizhuCcsjPP9lpjN+mpWpfSrHTVI4T/zDNearFljvT8zU2TQIA5v5s0zSjqF0Vy6RI3n5kYFX5QXXqDN05ZlyInJyeEyuubNRU6dsj529Cid9po3F/nrL6MkVDgj58+LjBlDN6fvvrM+ZjJxJauPj3JtqmbUEIW/aBEb8gULrPdfuMDJypAQkd27jZJO4UzMns1W7oknrFdjmM20/jRsWPLSTSfk/vsZTKdoeIG//xYJDhbp0YNuKwqFLT74gCb+qVOt95tMInfcQTcYFYKk2jDP9UPrXrzIsKujRzOAtEZ+PmN/pqQwPGvLlkZKqXAmFi0CJkwAXn4ZeOcdfX92NlOXdewILF5spITl4rffgDvuYNjbW27R98fFMdxt377M8FyRTM6Kmsf06cDjjzPa+Asv6PszMlgdunUDfv7ZSAkV5aQGxNJ/7jkGjD5yxDoW/nPPATNnMhNFedJ+VQVz5ujpwjRGjWKtOXGCxzVCQxnEXGP/fqYrAxijv1Ona5dn3Tpm4QCo4Fq1uvZrugrTpzNbzMqVzByjsXYt7//atUzc46Tk5wNt2jCm/Y8/6vtzcphqwN+fuYgcFeM+IQH4/nvrfQEBzGEE8FhCgn7MMhtfbi6wdClzyDdvznQJJcWHvxby84GPPmJGuqZNgYcfrvg19u1jXPvHH2c6h2nTOKYAmHerYUPb+5ydzz4DXnwRWLHCujqsWcNUu2vWsFoonBoXj6V//jyd9L74wnr/ihU08Tt6zj47m1FOvLzoT7Bzp242NptFDhwQqVePKwQsHQc//JDx3hcsoDt1aKjIp59WjUw//0ybXUnRV2oy995Lu3fRWLNDh4oMHmyUVOVixgw6Vp0+bb1/0iSRoKCSAw7aC7OZDoOjR7O4TZpk7QWenc1ofoMG0bdAqxZnzrDoP/MMq+3EiQwCZC8z8uXL9Hm44YbKfX/kSP6/v//mZ5NJ5JNPuC82tuR91YG772Z1KBq6YvhwkRtvNEoqRQVw8Tn8//yHnteW4cHMZgaLHjPGOLlee421/cEHrffff7/Iyy9b79u9m50TS++YX36hW/W+fdcuyx9/KIVfEpmZ1I5FJzCXL+czKbqMz4no3p3FyZKdOyn2L78YJRX9BerX50pIywQthw4x+EtR94g77mAnQMNs5nrwqqq+OTnFvc379q28wt+/n6k1LN0/Zswortxt7XN2MjM51njuOev969bxv5SWq0rhFMwrIYeoi7B0KfNE+vnp+zZuBA4cAN580zi53niD9srvvwfWr+e+hQuBgweBd9+1PnfGDNo+o6L0fSNHMgfp9OmOlbumUacO8OyznPrJz9f3Dx0K1KvHSXInJCEB2LkTuPde6/1ffcVc6aNHGyUZMxL/3/8xt/vkyYAIb+348cB//gM0aaKfm5ICLFkCjBih73NzA+68E/j1V2ZFvlZmzKhad4xOnTgTV1J25upMnTrASy8B333HqSGNAQP43H75xUjpFOXB02gB7IYI5+c//NB6/++/s1Z27myUZJw4nTGDToOPPgosXw48/zyVf9G87Js2cW7dzU3f5+UFtG7NzktJiLBmtmhRvrlmDw8gPh5YtQq4dIkTpS1a6MfNZs5b793La3fpQsXn7s4OlOa189hj7KD8/jtbdc1nwXJ/q1b0W6jMNbXvOop77wVeew3YsoUtG67c/969mfzdCdmyBfD0tO4jirD/++qrRkpG7r8f+Oknzvt+9x1zsffsSQdDS6KjKXfr1tb7O3Zk0YmOLv4djdhYFuWHHmLRKYrZzPvx8cfshLz9NovVqFE87uHBufw//uC8fKtW7Ci5uQH//S+Qmgq0bw/cfTf76dHR9C/YupXff/xxXreixMUBq1cDJhMQGUkfDKDk33z00Yr/xrUwYYLeVI0cyX3u7kD//sC2bY6VRVFxXFfhnz9PN9K2ba3379kD9OpllFQ6UVFUZNOmAd27A59/XrxlA4Djx61bbo3g4NJr2N69wCOPAA0asKUoix9+YGtWqxY9c955h46OwcFAVhZw881sJZ99FsjLo7dVYCBbp06deO6YMUB6OhXzxYvAv//NjpWt/a1bV/6ajlT44eF0oNy9W1f4AFveDRscJ0cFOH6cfTVLx7b4eCAtjf0UZ+Dbb/mIn3sOaNaMFomiHD/O1wYNrPdrilQ7botXXqEBxsuLjnFFMZuB2rVZtDt1YpPQrJl+/Nw5KlN3d1pMXn6ZnaV//YvVKiqKqx9+/pkdLLMZSEoCjh3j740ZU3GFP306q8K77wJhYcDEicDw4cDXX5f8m45W+EFBdAbdvVtX+ADQoQMwe7ZjZVFUHNdV+JmZfLX0zAeACxc4nHAGPviAtsnkZK5tKYrJRBdlW67UPj60q5lMHI4UpUsXWhGaNy+fLBMnUgHjilWhXz8OwSZMAN57j8OcxET9fg4dymu/8w7wySf6/jZtgKNHuarg0KGS91/LNR1NcDC1pSV167JD6YRkZBQv9pr4ISGGiFSM5s05qn7xRT5eX9/i52hVuGjx1zoy2nFbvP8+i/DEibaPe3qyuHt50SNfK/oaQUG0PmgMHgwsWECFX6sWtwsXOPIOCQGmTuV5Re97eUlJAZ5+mpu29C0/n/JPnszmoaTfdDQhIcWnU+rWZb9c4dy44EzTFbRW4dIl6/2+vtYTUEZy+DC76SK0PRYWWh+3NOMXRVtNWdI5bm5cVzRkSMXl0iwNmpZYtIgLty1bs0aNuK/oxF1EBIdFXboA48aVvL8qrukocnKs/UC0fba0lBPg62u72ONKKAFnITpad4WwNf9bUtEuq+jjigFGMxhVBa1bF+/zBQToHaiiM4cVZc0aGrksZ9+0MYClIa8qf7OyZGXZrg5F9ymcD9dV+A0bsvtuubgXV0aLBw4YJZVOdja774sWAXfdRRvZJ59Yn+Puzlp0+XLx71+6xMXU9vQOEmGHJD7etn2ySRMeM5srdl17XNNeZGVxAXibNtb7T58GGjc2SqpSadyY4lnewhYtOELct89IyXS++YbGq/XrOdp+8knO2Fiizb0XLf5aZ8bW3Lw9sWfEktOn+frLL7R8vP22bmE4c8Z+v1tR8vM5TikauiQhwWmrg8IC11X4tWrRu6eoY9WgQRxalGde255oE339+gFffgnUr09Tdlyc9XktW9qWNTmZI1+jcXMrfajlLNesLMuW6V5JlmzfbnsaxgmIjKS5++BBfV/t2pwDdoYAgbGxNLnPns1VAy+9xDnz55+3Pk8Lflm0+Ccn89UZin9V06cPXUUGDKAD4Z9/Ag8+aLRUOitW0BIxaJD1/q1b6YqkcG5cV+EDnJhbssS6a37HHbRvfvWVcXItWMBW7+23+TkkBPj0Uw5lHnnEWt4bb+T8teVwLS+P+/r1s7+s7u6ccNVaWUvOnKFTW0WVsz2uaQ9EGGJs5EjrcGgHDvD+Dx9upHQl0q0bR1tFzeQPP0zP9MOHjZJMX4L35ZecwQG4QrZtW2DWLAZ/1Ojbl8XgyBHra+zfz/22fFmrK5rDYFiYrvC1zZk6Nh9/zGY1LEzfd/w4DZS33mqkZIry4NoKf9w4mmNXr9b3+fnRU+iTT4qPph1BQgK9cubOpS1TY9IkOq1t3EgXZo2HH+YE2V9/6ft++w0oKCg99qe2LE8Lx3st3HUXlzhaOqklJ9O1eswY57lmVTNjBhATw7gJlnzzDW3kzuLyXgR3d/paTp9ubQ4fO5ZGr0cfLe4u4iimTqVHvLb8DVeMcTNnUok/8ghN/bjiK3n77eykaIiwI3P77XSsK4kjR7jevyy/Si+v4v4ORjB4MJuDH34wWpKS+fZb+hNYppfAlSWDTZoUH/UrnBCjQ//YnWHDmBHPbNb35eeL9OnDiHs5OY6Rw2QSOXJEJCpK5PnnraP/aTKtXMlQaAEBItHRTNkqIvL++yIREQyD++OPDHf18cel/97u3Qx/1aBB6ef98gvPmz9f33f4MPe9+y4/Z2byHvbuTRl++kmkY0eGJMvKsr7OTz9Z3+uS9l/LNR3Bvn3M//nmm9b74+O5/8svHStPBTl7ltHsikZgjo1l8SoaLc3epKeLzJnDKHuxscUf5/nzrKqAyOTJekjgxESm8H3mGQaFvO8+htY9e7b037vtNl6rrMd0660ifn4ir74q8vrrInl5jFLYtSvD7IqIFBYyUWKdOqy2ludYVmOTicE9AT3dsMnEqgqwSpe0T0Tk888ZQHPAAJG33hJ54w2Rhx9meOGSftNRbNvGaOBFM0fHxzN6+WefOV4mRYWpAdnydu+m5/f06daTYfHxXM89ZAjwv/8VD3ijqLmcPg0MHMiphTVrrJc93nEHlwbu2+e4zDOV5K23OCOxfz//isb8+TSr//e/DBCjUJTGkSO0QHTrRuOi5icsQkvN0aMM++Hk1UEBzHdtkz6uTGg+8wwjWhw7pu8PD2cEixUrGELLGex6CuM5coSTw35+zLJoqexnzKB9+euvq0Xr9sornGu95x7ryMD33MP4RU8+yflzF+/yK66BbdtYHcLDmXXRclHQF18wmuGMGdWiOihQE0z6YpECq02b4mm2tm2jnfHGG0WSkoySUOEMbNzIdGC9e4tcuGB9bM0a2jRfe80o6SqFZsIfM0akoMD62HffiXh6MsmONouiUGjMm0dz/ahRIrm51scWLmTZef99o6RTVAIXz5ZnSUqKSLt2Ip07F093euAAc3AGBYksWWKUhAqjyM/nJK6HByd/i06Sbt0q4u/PiVzLNGjVhM2bKb4tpb98Od08IiKsEzIqai6pqUyF6+Ym8tRTxcvM4sXM8P3MM0ZJqKgkNUjhyxUPk7Aw5r5MTbU+lpXFdLWAyEMPFU/6rHBNdu0SiYyk59Y33xQ/vm2bSN26zNNatOWrRqxfz9Ha+PG6M5pGUhLzuLu705nv4kWjpFQYidlM393QUJFmzWjUKsrPP4t4e4s88YTj/WgV10wNU/giTMIdHi7SooXInj3Fj//yC0t83bp0pS3aOipcg8REkUmTqOX69OEKiqJ8/z1d3UeOdIly8McfNO/36CFy6lTx499/L9KwIWe4Pv5YXySicH3WreOsp7s7xzvp6dbHCwpEXnqJo/4nn1TKvppSAxW+XLFZDRnCxnz27OLHs7K4RsfXl7bO2bNp9lVUf1JS+Gz9/ESaN+dEZdHWq6BAZOpUtm5Tp3JdlosQFydy3XU0469cWfx4ejrdFPz8aAz75hvHrVxVOJ4NG/TlkMOHi+zdW/yclBS9uZwxwwgpFVVEDVX4cqVRf+YZNuoPPVTcSUuEi4EnTeKEVdOmIh99JJKRYYS0imslLk7k0Ue5hr5hQ5EPP7Q9hN2zh0Mdf3/aL12QnBy6I7i7izz+uG0T/tmzIlOmsJFv0EDklVdoFFFUf/LyOIa5/noq+r59OeVTFLOZYT+Cg+niZMsgqqhW1GCFr/HzzyKNGtGMv2CB7XMSEkT+8Q9G3ggIoCdLTIyjJVVUlPx8OmGOGkXt1qqVyFdf2R6y5uaKvPwyXY+jouje7uLMmcPGPDRUZO5c2+ekpDD+Umgo+71jx4r8/rsyeFVHDh5kx017luPGiWzfbvvcw4dFBg1itZkypbiJX1EtUQpfRDjEeeQRjvZHjBA5dMj2eenpHOW3acOucefODGVWdKmfwlj27BF59llqM3d3tlw//1yyh/1vv7EzEBgoMm1atfTErywXLtDw4e4uMniwyM6dts/TRoU33shqEhTEfu+2bY6WWFERkpIYBU8bzTdrximbkqw1aWnsFNSqJdKtm3q+LoZS+FZs2EAl7uEhMnGiyPHjJZ+7c6fI00/T3unhQbvYBx+wa6xwLCYTn8dbb9HjXmvZpk4t/RmuWSPSsyc12F131Wib9dat+q0YOVJkx46Sz01IYBjYrl15q8PDGQ534UK1nt8ZOH6cz2fIEI7kAwPZnC1dWrI7SloaXVsCAtikff65S7muKIhS+MUwmWjfbNOGtWXyZJETJ0o+PzeXUwHjx9OzH6BX1OuvM6C2C3h3OyWpqVxR8cgjtFECDLr+3HMimzaV7ka8fr1Iv378zi23qOkZC5Yv1xX/iBEiW7aUfv7OnSzq3brxdvr5idx+O539SjKUKaqW1FSujX/iCfqhAjRuPfAAq0hpqy3OneOIv04durb8+99Mc6FwSWpALP3KUlgIzJkDvPsuY6uPHMlYpIMHl5y6taAA2LCB4VeXLQNOngR8fJjkeuBAbj16qLj9lSE9Hdi0CVi/nknCtRyp3bszoPeoUUCnTiV//9IlZij88kvGwR80CHjvPT4bRZPiF4UAACAASURBVDFWrGBWtL//ZnTqxx5j/H0/v5K/k5gILF8O/P47q0F2NjM/9+vHrX9/Zutzd/2A3nbl3DlWhY0bmUTz4EFWhS5dmKJ2xAg2M6Xd540bGSH611+BgADg+efZvPn7O/KfKBzMfKXwy6KwEFi8mJlGNm4EOnRgzRg/HggMLP27SUlAdDRT1K5Zw1S9Xl5A69ZAZKS+9ewJeHs76h85PwUFVMrR0UxPGxPDJO5mM5ODDxnCbfBgoH790q914gTzes6cyTTD99wDPPUU77uiTLZupWJYtIjx0u+7D5g8ufS+FQCYTMCePXyEmzczz/2FC1QoXbpYF/927axTFih0Ll6kQteqQUwMczd5eABt2zLO/ZAh7L82aFD2tebN4/M8cAC44QZ25O6+G6hd21H/SGEgSuFXiMOHWVtmzmSLNnQo87rfeWfpQx+No0eZjWLHDuZ9372bCcv9/dmR6NSJrV+nTkD79sxYUZI1wRXIz2eymthYtmqHDnGLi2NHq2FDDlW6d+drnz5lt2oAkJbGpOlz5gBbtnCYef/9VPRNmjjin7kc6enAwoXA55/zcXXowKJ/990sqmVhMrEPt2MHldauXfycn8+q06EDi3779lRkHToALVvWHGPY2bNsXg4fZhU4coRVIimJx1u00DtI118P9O4N1KlT9nVzc2l1mTOHYw53dxorn31WGbdqIErhV4r0dNrCfvqJNjU/P6ZNHTuWZnsfn/Jdp6CAXe2dO/mqKbyzZ3ncz4+tXvPm1lt4ONCsGRAUZNe/ec0UFgLJyZzaOHWKKYnj4/n+1CnuLywEPD05ctc6PF27Usm3aFH+30pO5jTKggU0+/v5AbffDowbxyGQp6c9/2mNwWzmiH3hQiabPHeOI/axY8ueVSmKVvxjYtiJOHSICi8+nhn8vLxYBMLDmfUvLIzFX3vfuHH1GJmazUBKCpCQoG9aVUhIoBEqI4Pn1qvHTk/79npViIzk/vKSmsosdj//zFcR4Kab2DkbNYomfEWNRCn8ayYpiUpm3jxOePr4UOnfeiswfHjFlJZGero+6j1xQleWJ0+yhdUemZcXlX5QENCoERAcrH8OCKDlwN+fQ4G6dfne25u2WV9f/fd8fa3zW2ZnszXWyMhgq5WTw2PZ2ZQxK4vvMzOB8+fZqiUl8b22aXh7s5MSHq53XNq00Vu2ik5pmM3sKC1fzgnnXbt4jeHDqeRHjCh/x0tRKUwmznItXMj+b0oKDSg33wwMG8Z+VkUUlUZuLke4hw/TKGapJBMSaBTT8PenAcey6IeGssjXq8d+n58fz7OsAl5e1vPVRT/n57O42/p88SLfa9VB+5yVpRf7c+eoeLXPWpV1d6d8lh2XFi1YBTp04P+oKIWFwPbtVO6rV7MD5eHB+z92LPu9detW/LoKl0Mp/CrlzBlg5UoqoLVr2QJ06MCaFxXFrVGja/uNvDy2fKdPs1XRFK3l+9RUKuHsbOvWsaqpU4etZECAdcfDsuUNCWHr1rjxtXlriXAIGB1Nj6U1a/h/w8Ko5G+5hXP65ZlaUVQ5ZjMVzerVVDzbt/OR9ewJDBhA83Hv3uWbkSmLc+eo+DWlqhX91FQW/+RkVr2LF4v3Xe2B1pGoU4ezUFrR194HB/Nz06bcrtVdJz+f/dutW1kd1q9n/7tJE47gb7qJVaE8Jn9FjUIpfLuRn0/FtHIlzf5797Ir3rIl0LcvcOONbAHbtrWvubmgQB+GaK1fbi47DhpFW8WiI35/fw6BfH11q0Flhm4VITubXl+bN7NV27KFXl916gC9erETdcstFbMhKxxGejod9das4eOLjeX+tm1Z7Pv0odNYu3b2n6fPz9eNUlpRv3yZCzc0in728LA2fVt+rltXtxo4wqs9MZGdqS1buO3cSXmDgngvhwyhpWXJEuDFF4E336weUx0Kh6MUvsPIyaGTnqbANm2iqbyo137HjlwHVRVDoeqCLVdkzSs/JIQOe1FR7CipFQ3Vkqwsjvq1hRfR0VTAWvHv2JHGMK0KREQYLbHjyc/nFIbmiX/wIJ0ck5N5PCKCVUCrCh066D69IsCMGcALL7DKzJzJZZAKhQVK4RtGYSE9lvbs4eh/716+v3iRtbhZM1oDWrUqvlnOv1cXUlOBY8e4HT2qvz92jCN3gKb/Ll3otNiiBfDvf/MeKFyOwkIqtX37GFIhJoYuMFlZPF6/Ph+9tkVE6O+bNKm+i1cyMoDjx/XtxAn9fWIi/SL8/Njp6dIFuO46oHNnOu+VtQoY4Gzfo49yRvHZZ4F//lON9hVXUQrf6YiPp/I/csRaKSYmcsQL0JYXEsKWLzRUf23cWHfYCwyk7bFuXfu0jvn5bL207eJFTqYmJ9OX4dw5viYnU3bN46lWLbbelh2YDh3YumnTBN9+Czz9NHDvvcD331e97Aqn4tIlOvodPcopgORkGniKKkbN5F6rFufFmzTRX0NC6D7SqBE7CwEB+mbP2aecHLrLaNuFC7pLzdmzenVISeHnzEx+z92dfXrLjkyrVqwGLVteu7vLrFnAc8/RxeV//+N1FTUepfCrDXl5euuXkKArUksFm5KiuwNborV8gYF6d9/HR3/v6al7+IjQ1qqRlcXhmPY+I4OtluWEp4a3N1vepk3ZEjdrxtemTdnytGrFfeVpzbZs4XDnxhsrcbMU1Ym9exnKYsmS0l0yzp5l8T91SleoKSnWClVb3lYUyw6AtnjD29vax9Oyb5yTwz4trlgjNMuDycTif/EiX02m4r9Vq5beHw8OZj9c65A0bUqF3qKF/Wem4uOBSZM4i/jqq8Abb6gARzUcpfBdioICDjG0Uff27Rwpv/suW7mMDL0Vs3TUK7oGybLls3Tg8/Njp6HoplkSyop6p1CUQEFB1TjvXbpEZaz1SzMz2X/NyODSwVq16DionastYjGbrTsLlv1hNzd9WZv2PjBQ70Nbdibq1y+f6d1RmM3Axx/Tka93bwbgCQszWiqFQSiF79JMmULvqAMHjJZEoTCcjh2B0aOZQqGmsWcPMGECw2TMmsXle4oax3yVxsJVuXSJAYEefNBoSRQKwykooCtMecIAuyJdu3I534QJDMTzzDO6sU9Rc1AK31X59Vea7cePN1qSqsdsZuAhhaKcHD1KBdehg9GSGEft2sAXXzAy4uzZjIVw/LjRUikciVL4rsqsWQwvGxpqtCRVz1dfcciydq3RkiiqCbGx9BXV5u9rMmPG0L2nsJAhLlauNFoihaNQCt8ViY9nzvgHHjBaEvvw8MMM1n7PPbr7tMLp2byZnuJGeA3FxtIzXqVXIG3bMnHnqFEcF7z/vjHPReFYVAoxV2TWLK7HHz7caEnsg48PMHcu7ZEqYHi1ID6eCSX79KFicXTgnJMnuSpUoVO7NvDDD3wmTz7J2Pw//uhcqwwUVYsa4bsaIqy1993n2snE3dxUC16NOH6co8q5c68tqExlSUzkGnhFcSZPBv74g2b+qCg1r+/KKIXvaqxfz7BkkyYZLYlCcZVBg5g+wqhkhmfOMBCOwjb9+9OL39ub6/W3bjVaIoU9UArf1Zg1i9nkarI7skJRhMREpfDLolkzZt3r0wcYOBCYN89oiRRVjVL4rkRGBrB4ses665UXEQZlVyiuhMnNyFAKvzz4+QG//MIEPPfeC7z9ttESKaoSpfBdifnzqezGjjVaEmPZvJnZWJ591nawc0WN4uxZvjZubLQk1QMPD67X/+wzZtt74gk9b5eieqMUvisxaxazkGiBv2sqUVHs/Pzvf4y4oqjRaLmg7Jk1zxV55hlg0SLgu+/oA6zl0FJUX5TCdxWOHKGbbU0352uMHcu1WO3aGS1JjcPZgiBqeaGMchisztxxB7BqFbB0Kd/bSpKpqD4ohe8qzJwJNG8ODBhgtCTOg1qj73DS0+kz+sknRkuik5vLV19foyWpngwYAKxbR8/9W25Rsa6qM0rhuwKFhTRfP/CAMYucFYorvPAC53udydCUk8OwDSrKXuXp0YORrA8dontMdrbREikqg9IOrsDy5UByMlNhKRQG8vTT7Hs2aGC0JDo5OVT2qi98bXTtCmzYwMA8I0fqlhNF9UFVAVdg1ixg8GAgIsJoSaoPKmOIXbjuOhZFZ+LSJWXOryratWNUvv37gdtuAy5fNloiRUVQCr+6k5ICrFjhXDZUZ2fPHg5RpkxRy/ZqAB4eysO8Kuncmeb9XbvoyJeXZ7REivKiFH51Z84cDl9uv91oSaoPXbsCP/8MLFgAHDhgtDQKO+Pjo7zLq5quXTmTuHkzo3irTHvVA6Xwqztz5gDjxyubZUW5/Xbg1CmgSxejJVHYGR8fjkJV8JiqpVcv4LffgF9/BV55xWhpFOVBKfzqzPbtnExT5vzKofKA1gi0vrCab656Bg4EZs8GPvoImDbNaGkUZeFptACKa2DWLKBjR66ZUSgMwIjc9hVFW46Xm6sMYfbgnnsY9+vpp5mAZ+RIoyVSlIQa4VdXLl3iHPSDDxotiaKGEhfHHPcnTxotSeloEfa0iHuKqufNN4GJE5lwZ/9+o6VRlIRS+NWVX39l9Ivx442WxDU5c8ZoCZye//s/voaFGS1J6YSG8lVLoqOoetzcgOnTgW7dmM4jM9NoiRS2UAq/ujJrFjBihN6aKaqO337j0HX9eqMlcWp8fICpU7nszZlp0gTw8qKPpsJ+eHkBCxfSkjJxovLcd0aUwq+OxMcDf/6pnPXsxa23AqNG0ZM/NdVoaZyWzz4DHnrIaCnKxsODc8tK4dufkBDgp58YGuTzz42WRlEUpfCrI7NmAUFBwPDhRkvimnh6Aj/+CKxZAzRsaLQ0iiqgeXP2kxX2p39/4L33aP3ZutVoaRSWKC/96oYIldF999GGZsmxY0BiIt+3agU0bcr3Bw5wojUgwPHyVpSS/kNp7NmjJz2PiqLCvlY8PLjQWFFuCgr0OEadO5f9GDIygN27bR/r27d48b4WwsMdO8J35ipnj+pSlKlTgY0b2Uzt2VPx1MSqKbPPs1Ej/OrG+vXAiRMMb1UUb29mthg4kJHkACA2lq1vdfHmt/UfysLDA/j6a35HpfEyhHXrGGd9xgzgP/9hWocNG0r/zv79fGS2toyMqpWvRQsWK0fg7FXOEdXFzQ347jvg4kUq/4qimjL7PBul8Ksbs2Zx5NmhQ/FjYWGcf7akWTMulL3zTsfIFx8P5OdX/vu2/kNZdO7MTWEISUnA6NHA228z+MqsWcBTTzG5SnJy6d8dPZqKv+hWr17VytilCxtfbfRkT0qqcraqxrVWl8rgqOrSqBHw5ZcsE6tWVey7qimzD0rhVycyMoDFi0t31isaBcXfH5g3Dxg3zu7iAWArn5Jybde4lkguzh4FxgX59luGrh07Vt/3yCNAVhaPlUa9ekCnTsW3qvb879mTs2G7dlXtdW1RUpWzVTWqorpcC/auLuPGAWPGAA8/zNF+RVBN2bX9ti3UHH51Yv58tlqWLSvARa+xsUDt2npYMYDd0y1b+D4oiFH5zp0DDh/mvh49OLmWlMTSpS3xO3+ew6GmTW1PPOXlAYcOMfhPvXq0l9aqRd+CvXvpqRMUBPTuzf3luWZJ/6GieHkxEsy5c5RL+08nT1p7bYWF0e589Ki+5l67R2Uxaxa/8/rrlZezmmIyFVfGa9YArVvrjxoA6tYFWrYEVq9mUBajCQ1lsdu2DRg0yPrY3r3Wyqh1ay7lK0piIudlAZ6vWSEsq1FBAWfcYFGcNLcby6rRqxeXsFWkuqSm6j4SPXowauDhw/zNjh0r10lyRHX56it24l57rezwu6op07HHs1Ej/OrErFm0Z9Wty88izFoRHs5aNXs2a5WGuztL8tixwFtvcZ+nJ/0ABg5k8J7bbmOpXbKErfljjzEV1rx5tLcOGmS9NO3TT2lb++wzWhumTGELuWYN8L//8Zy//qINLy+v7GuW9R8qyj330FPokUeAxo25IDgvj/fi88/5v9eu1b1hvLyAlSv5m+XtUhcUUIv961+Vl7MakprKZVfbt1vvP3yY+4vSuLHeIJeEyURFun07R9/2jIY3cCB9DYoiwumIgQPZmFo6C1r+Vy8vNvT338+iYqsaLV1avMrZqhq//17x6uLpyXMHDgRefJHe8LfeyumKfv0qlwLYEdUlKAj4+GNae/7+2/Y5qikrjl2ejSiqB4cPiwAi69bp+776ivtWr9b3JSVx32ef6ftathS580798x9/8JxHHxXZtk1k9myRr7/mdwCR/ft53qVLIg0aiDz5JD//+COPL1tmLVtUFF+//JLHT5/Wj5V1zfL+h7J47z1+5+JFfd8PP3DfW2/xc0wMPz//vPV3H31UZOHC8v+WiMg333CrQcycKeLjI5KVpe8zm0Xc3ERGjCh+/i238JjZbPt6+/aJ9OsnMm6cyLPPitx+u4i/v8iUKSJ5eVUv/w8/iHh7i2RnFz+2ZAmLhmUxOHqU+2Ji9H1z5oi8/DLfl1SNxEaVs1U1KlNdtN9cvLj4d1asKP+9cHR1MZtFBgwQ6d5dxGQqflw1ZTp2fDbzlMKvLrzwgkjz5ta1pXNnkXbtrM+rSC1ZuVLfl50t0q2byHXXWV/vtttEmjXj++7dRVq3Li7bmjV8tVVLyrpmef9DWdiqJSIibdrw/1vKExoqUljIz3l5/E+XL5f/t2ooP/4o8txz1vsKCnjbR40qfv7IkTxWUFD+34iOZifhxRevXd6inDnDay9dWvxYfj4b7zvu0Pe9/jrlf+YZfd+oUeyoSCnVSK5B4ZdVXWz9Zmws9337bfnvhRHV5cABES8v23KqpkzHjs9mnjLpVwcKC2ljmjSJ9hxcsYUePMi1UFWBnx9TXtWqRTuWtuXlMQi5ycRJrTZtin936NCSr1vaNfPzq/Y/2ELL7qLF+XzkEU6KrV7NzytXAjffbD0BrbDJhAl6/HwNT08uP7LlzXz5Mm9rRdYS9+1LL+W5c69d3qI0bsy5c1tLpLy8aC5euZJzsCKMFnfTTYwcV1jIZVJnzpTuRV3R9eZFKasK2kK7v2bztf027FxdOnZkRr1XXgHS0vT9qikrH1XxbJTTXnVg+XKub5o4Ud936RJreJ06Vfc7+fnMIfrXX/q+G27gVljIuWt//6q7Zm5u1f+Honh6soZoeVzHjwdeeIETbLfcQs3y6qv2+/0aQFiYbQ/stLTKJdZp1Mh+Gdfuugt4910WS29v62MTJ3IN9OLFnNvt04fzpHfeycY0Oxu44w77yKVRWnVxRGx6e1eXt97i2OVf/9I7j6opKx9V8WyUwq8OzJoFDB5MV0wNPz925cpa6FwRgoLo9fL22yUfr2gWudKuKVL1/6Eo587x9zXLSGAgW/358+nqeuYMvXAUlaZHj+LOcCL0aC9tHfLhw7ZHRDk5QP36VS8nwFH8Sy9Rqd99t/Wx3r25smD+fBbbp58GrrsOaNAAmDOH/+mjj+wjl0ZZVdDe2Lu61KlDf9fnngOeeIL3WzVl5aMqno0y6Ts7KSm0LRZde+/mRvtkdHTVRRPp04duySWFObv5Zh4vKUap5XRDea5pj/9gSVoasHNnca3z8MO0xY0fT1fYqsbZE8RXMePGsZjGxur7tmyhadxyzfSuXRzNaXzyCRAXZ32tnByaW2++2T6yNmnC4lBSfIAJE+j5HBsLdO9OK8C999Kr/sIF6z53RbBVNSpaXeyNo6rL5MlU9NpyTdWUlU1VPRul8J2dOXO44Pb224sfe/NN2pmGD+eQZf16xrOsLK+9xusNG8aJzuhotnTLl/P4e+8xmUyfPoyfun49t5kzae9s0YLnff019x87VvY1q/o/xMezRh44wFrQuHHxLnlUFNC+PRATw9a8Kjlxgtf+4ouqva4TM2IEMHIk8MwzbJgSEzmCu+MOHgMYcjcykg2Uhp8fl2sdOcLis3cvzef16wMffGA/eR99lGbZgweLH5swgSbfu+7S902axEb1ttsq/5u2qkZlqktVY0R18fRkUzJvHq8J1ZTZxB7PxuPtt40yHinKxZQp7NbZUvgtWtDL5NQpBi4/d44tVlwcW970dHoc5eXR5nTwoJ4JLjCQJSo7mwt5cWXydMwY2qXWrGEpysvjdEKDBlz/P3Eiu7PR0dxOn6Y3Tpcu7LabTMwAkZREG2nHjqVfs6z/EBLCha1l0bYtt8WLOan1xx/scn/3HW1xRcnNZQaO++6rgodkQb16jLbx/POcWLMVwcXFcHOjgrx4kWuaV62i4v7wQ32k5OPDonLvvWygcCU4T1wc8Msv7Ndu3w4MGMDOQXCw/eRt2RJYtIiN+OjR1sfq1wcSEoBnn9XnYxs1YlCTf/xDn/c9cIBWgqLV6MgR4P33ratc164MPFO0avToUbHqcvEiA9cEBvJeNmnCYx9/TLnS0koOBlMUo6tL+/Z0Ntu8mdVdNWUOeTYH3EQc4QqiqBTbt/NJ//03WwdF1aEFex8yxD7X37qVrYTCKfnpJzaQhw7Z9tZWWGOP6vLHH1wFER3N1RmKylGBZzNfKXxnZsoU1gYtnmZNZMuWsjNYeHvTNlca585xGOTvzy766NEcXijKZNo0jojGjzdakqrDZOKIrWtXOj25CtWtutx4I0foy5ZV/bWdDSd4NvOVl76zcukSsGAB8MYbRktiLF9/XXbWjXr1yq4l0dEMpD5sGNcG/fvfVSqmK/P115ydcCWF7+FBU/ioUexXDxhgtERVQ3WrLq++yrK1Y4frGzGd4dmoEb6zMncuvYVOn9azJigqz65dwD//ycWyTzxReoQNxVW0JXI//eS4tKSO5NZbWcV27iy+Lr8m48jqcsMNnN9eutR+v+FKXMOzUSZ9p2XIEHoNLV5stCSKGk52Nh2katc2WpKq59gxoFs3jvI//thoaWomy5bR0rJ/f/my7ykqzXy1LM8ZiY8H/vyz9Lz3iurJhg2OScpehfj7u6ayB4BWrYD//peZ037/3Whpaia33kqv/aJhmxVVj1L4zsisWVx/MXy40ZIoqprPP+fkm61F4ApDuP9+xge45x7OjSoci5sbl0HOncslcAr7oRS+syHCxaX33WedmFvhGsydC3TowIXgCqdh2jSupx4xAti922hpah733UeHtWnTjJbEtVFz+M7GunWcvz94kIpB4Xpcvuy6NvJqTG4u1zPv3MnoaWV5SyuqlnfeAb78koGPfH2NlsYlUXP4TsesWQy2o5S966KUvVPi60sHsv79GRDmt9+Mlqhm8dhjdBB1pbgIzoZS+M5ERga98pWznkJhCLVqMU76vfcyoMn77zsmLa2C4ZRHj6YTpcI+qMA7zsT8+Wxdxo41WhJFDePUKcYQ9/fnuvugIL42aMD39erxc/36DAtxww1GS2w/PD0ZJ79TJ8bPj4kBpk+3X8pehc5jjwH9+nFapXt3o6VxPdQcvjPRqxfQujWd9hQKBxMRYZ3Z182NEek8PNgPNZm4PfAA8P33RkrqOP76i0lWRJjIZPBgoyVyfa67jlH3riXTnMImag7faThyhMlylDm/5rJzJ/DSS8VtyIWFzOlaUvLuKuLWW62jzYnwp/PyGANcyw3+1FN2FcOpGDCAqSwGDGBEs2ee4f1Q2I9HH6Wx0x555Ws6SuE7CzNnAs2bu05Qb0XFSUpiftlXX9X3ZWcz2Pj06SwjdmTo0NKTe3h4MAFgt252FcPpCAwE/vc/praYMweIjAT27TNaKtdlwgR2NhcsMFoS10MpfGegsJAtyqRJegJxRc1j5EjaypOTGSg7JYXpxP76i8e//rrsdFvXwMCBVOolYTYDzz9vt593eu66i0aYOnXow/Duu1xhqahaAgOBO+4AfvjBaElcD6VdHM28eVxseuGCvm/5cjbyEycaKZnCGZg4kUo/Pp4+HQcPAgUFPJaeThdyO6EpMjc328dDQ7lOvSbTsiWwaRPw3nuMvd+5M7BqldFSuR4PPMCoh7Gx/HzpEpPrTJrEUCWKyqEUvqM5eBB4+mm2nmPGACtXsoEfPJheUwpFTAxdlE+f1pW9xhdf2PWnhw+nl3pRvLw4f23rWE3D0xN44QW63fTuzXs2ciT7aIqqYfBgIDwcePllWlYaNGBnc/Zs5UNxLSiF72jy8th6FhQwssctt7Dr6ucHHD1qtHQKo1m3juuSMjM51WOJ2Qz8/bddk+/cdFPxPgaueOw//LDdfrZa0rgx5/TXrAHi4pjp7cMPbd8/Rfm4cIH39NZbgcREJjRavJgjfA0Vt6ryKIXvaPLydJupZYO+YgXQpg3QtSsdtLKyDBNRYRA//sjEOpcvF1f2Gl5ewDff2E2E7t2BunWL/+R993GUpSjO0KH05P/Xv5invHVrVmGz2WjJqg9nzzLCYVAQ8OCD7ESZTPpyUEssV5IoKoZS+I4mL892S6ANC/bv57oUtTyvZhEXx/VuZnPpmqKggA6eGRl2EcPdnaN8S9N9QUHNWopXGbQpj4MHudDmsce4lnzNGqMlqx40bgy0aGEd76EkatVypGSuhVL4jiYvr/RYnR4eHCKoqBM1izZtgBMnuA7fy6v0TIn5+ZzMtBM33aT3OTw8gKgoBkNRlE1YGL3LDxygg9+wYbx/0dFGS+b8fPMNU4iU5SeiFH7lUQrf0ZQ0wseV1tXXl+b9wEBHS6Ywmvr1gQ8+oC/H2LGc+rHV+pnNXK9vpyCZw4bpRdRsZnhZRcVo3x5YuJAe/SJ0yxg7loYchW1q1+Z8vbd3yStFoBT+NaEUvqO5fLnkhtrNDViyBGjVytFSKZyJ8HCa7bdtA3r25D7LBfIijLq3fr1dfr5pU45OAaBRI2DUKLv8TI0gKgrYvFl37Gvfnh79u3cbLZlz0ro1Fy2V1pdVCr/yKIXvaCzdTS1xc2NJV5H2FBo9e1Jb/PEHNbBlUCZPT8ZzsBMjRvD12WdLD8ajKB9DhnBxxZIldFCLjKTi37nTaMmcj7vv5oqQkkz7uIYCQQAAIABJREFUSuFXHqXwHY0the/uDrz2mgq8o7DNkCGcFP7iC6at8/SkF/+yZVy7ZAduuomzSw89ZJfL10jc3XUl/9tvjLXVowe9/LdtM1o65+LLL2kNseXKohR+5VEK39EUjcXp6Umb6TvvGCWRojrg5QU8+SRN+S++yFbPZOL6LzvQvz9HWSolbNXj5kbFv30715lnZTGAz803Axs2GC2dc1C7NvDrryz2RefzlcKvPCo9rqPp0kXPvOHlBbRrB2zdysA7CkV5OX0aeP11YO1adgJK8OrPzs5GWloaMjMzrbaMjAykp6cjMzMThVfW/GdkZMB8xVuvsLAQFy8WwtOTFqlatWrB19f36nXr1KkDzys214CAgKtbYGDg1ff16tVDQEAA6tevD3eVI6JU1qzhGv5NmxgL4fnnGYizpkc2XLiQJn5LCgrUfakk85XCdzTt2jEmp4cHh0+7dtFLSqGoAAUFBYiPj0fKH38g8eJFHC4sREpKCs6ePYuUlBQkJSXh3LlzyM3NLfZdNzc31K1b96py9rrSWfD397/6XjtHIzc3F3kWMU3T09OhNR1axyEzM9PqHA0PDw8EBwcjNDQUjRo1QnBwMJo0aXL1NSIiAi1btkRAQIBd7lV1Ytcu4PPPmXIjKAiYPJnr++vVM1oy43j8cWDGDM5iubmpgEbXgFL4DiciAjh5kjarLVtqXq5RRbkxm804efIk9u3bh6NHj+L48eM4fvw4Tpw4gYSEBJiuRCfx9/e/qkAbN26MkJAQhIaGonHjxggODkaDBg0QEBCAOnXqXH21F3l5ecjKykJmZiYuXryIzMxMJCcnIzk5+WonJDk5GWfOnEFKSgpSUlKudhwaNmyIli1bXu0AtGzZEp06dUKHDh2srAs1gVOnuC792285c/PAA1weGR5e9ncTExni97PPXGMknJfHpE779tGQpWLpVxql8B1OkybMe754sUo9prhKeno69uzZg/3792P//v3Yu3cvDh48iJycHLi7u6Np06ZXFaGlQoyIiED9ajzRnpeXh5MnT+LEiRNXOzOWHZvLly/Dw8MDLVu2xHXXXYfOnTujc+fO6NKlCyJqQLKp9HQq/S+/pJPfmDF05ejbt+TvvPce8OabdLz8+WdmQazuHD/O2VA3NxV1/BpQCt/hNG4MPPccHa8UNZYTJ04gOjoaMTEx2Lx5M3bv3g2z2Yy6deuiY8eO6NixIzp06IDIyEh07doV/v7+RotsCGfPnkVMTAwOHTqEgwcPIiYmBocPH4bZbEZgYCB69OiBvn37IioqCn369HFZS0B+PrBgARdqxMTQMPjEE8D48YCPj36e2cxof2fOcHTfpg2werVrzBr++iv/c1KS0ZJUW5TCL5XcXG6ZmexWFhYCOTmsfRpmc/G45h4eQNH5SD8/hpD673+Bt95iJD1//9JDqCpchgMHDmD16tVYv349tm3bhgsXLsDX1xfdu3dHnz590KdPH0RGRqJx48Z2lyU3NxfZ2dnIzs6+OhdvOScPADk5Oci3LOcA6hWZSPbz84O3tzf8/f3h5+cHPz+/YufYg5ycHOzbtw9bt27Fli1bsHXrVpw9exZeXl7o2rUr+vXrh5tuugn9+vVDbRdMrRYTw8UZP/7IJuX++znPHxFB579hw/RzvbzY1KxaxbX/1QmtaU1PZ/NbUMC5/DFjeFyExywJDLQOV6GtYq1Th+8DAmp0XIkapPBTUji5lZQEpKYCaWnA+fPctM+pqSxZubnAxYuOkcvLi4o/MJClsmFDeusEBTE9WcOGfA0OpnUgPFx59FcD0tLSsHbtWqxZswarV6/GmTNn0KBBAwwaNAhRUVHo3bs3unbtetVJrrIUFBTgzJkzOH36NM6dO4eUlBSkpqbi/PnzV+fIU1NTkZmZaaXg7YnWAQgICEDDhg3RsGFDBAUFITg4GMHBwVc/N2vWDOHh4VVivYiPj8fmzZuxdetWrF+/HocOHYKPjw/69euHYcOGYdiwYejQoUOV/D9nITkZmDmTc/1nzzLTdno6l/tZpuj18GAzs2CB8VETL11iyohTp9j0nj3L/5GSwvfnz/M/ZGZybGUP/PzY1Naty2a1USMgJERvYoOD2cxGRDAWhQvhQgo/OZne70ePAvHx3BITuSUkWK9/9/HRFWlIiK5YGzZkSfD1ZWnw9eUWGKiP0GvXtrahwUa3Mi+PnQZLMjLYZc3JYanXrAa5udyXkcHPqaks/amp1h0Ry3Sp9erRRhceztemTRmOt3Vrbq4waVcNSU5Oxi+//IKFCxciOjoabm5u6NWrF4YNG4abbroJkZGR8KjE8OL8+fOIjY3FkSNHcPLkSSQkJODUqVOIj49HUlLSVec9Nze3q8pUew0JCUFQUBACAgLg7++PunXrXh2N16lTB4GBgXB3d7daZgcAtWvXho9FOTeZTMjMzLSSS1vGl5WVhZycHOTk5CA9PR3Z2dnIyclBZmYmzp8/j9TUVKSmpuLcuXNXP1t689evXx9hYWEICwtD8+bNER4ejjZt2qBdu3Zo0aJFpe5ZYmIiVq9ejTVr1mDt2rW4cOECmjdvjrvuugtjx45F9+7dK3xNZ8VsBpYvBz79FNi40XZYWjc3bp99Bjz9tH3lyc9nU3zwIHD4MBW8tlma4319rZVtkyZ8rVuXTVhAAJtWbSzk7c1XS0dEy6a36Ii/sFC3DGRmsonVmtmsLI7ptI5GSgpVSFKSdUcjNJSKPyKC2fzatQM6dmRQoGqYpreaKXyzmd4be/Yw8tjRowxQffQonyiudN9atOBElqYMLRVjkybVc4ScmsrSWLQjc/o0t/h4vVPQqBEn79q0YQegSxduISFG/wuXIzU19aqS37BhA3x8fDBy5EjceeedGDJkCAIrkAQpLS0NMTEx2LNnD44cOXJVyV+4cAG4svY9IiLiqmLUlGRYWBjCw8MRHBxcKeVoBOnp6UhMTMSpU6eQkJBgtZ08eRJnz54FAHh7e6N169Zo164d2rZti86dO+P6669H69at4VZahhULTCYTdu7ciSVLlmDhwoU4ceIEIiIiMHbsWIwdOxbdXGSlzKefAi+/bD02KIqbGwMqTZtWNR78GRmMErhzJzN7HzjAJrmggFaFiAhGhdaUprY1b+6845LsbFogLDsqJ05Q9Rw/rv+31q2BTp2Azp0ZO6FXL3ZWnBgnVviFhVTsu3bxde9ersvIzmZJbdmS3S1tVNu6NRVckyZGS24MBQVc7hcXp3eCjh5lF/vMGZ7TqBEVf9eu9PqJjNSzpCgqRExMDL744gvMnz8fHh4eGDJkCO666y6MHj26XCbq9PR0bN26Fbt27UJMTAx27dqF+Ph4AEDTpk3Rvn17tG3b9upr27Zt0dQVPK/KSVZWFo4cOYLDhw/j8OHDVu8LCwsREBCAbt26ITIyEtdffz169uyJ1q1bl+vaBw8exKJFi/DTTz/h6NGjaNeuHSZNmoTJkyc7xAfBXrRpAxw7VnYSRQ8PYOBA4JdfirsalcWhQ1xNvHUrFf3hwxyHhYczhXLHjlSA1XgUXCoFBbr1Yt8+vu7fzw6BmxtV0g03MHJi3768D06EEyn8rCxOPkVH0ytl0yZ2H/39gbZtmSg5MpLb9de73OSKXcnIYKmMieF26BC74nl5HPX36MG0Xn37sqvqgo5OVUFaWhp++OEHTJ8+HXFxcejTpw+mTJmC0aNHw68Mq1FKSgq2b9+OzZs3Y+3atVe98hs1aoTIyMirW48ePRAaGuqw/1TdKCgoQFxcHGJiYqy2y5cvIyQkBD169EBUVBSGDBmCbt26lRrhT0Swbds2zJgxAwsWLIC7uzvGjx+PKVOmVLtRf3Q0cOON5T/f05NjpNWrgWbNSj7v/Hngr78Y0HHVKhoV/fw4ZtCa4/79yxcfwJXJyAB27NDV1+bNnDIIDub9GTKEPhYG99kNVPh5ebw7q1bRtfTAAXYV27YF+vSh8unTh59VWM6q5/JllswtW1g6t2xh7fbx4X0fNozbddcZLanhnDlzBh9++CFmzJgBb29vTJgwAVOmTEHnzp1L/E5hYSGio6OxfPlyrFixAocOHYKHhwe6dOmCfv36oV+/foiKikJQUJBD/4srkpeXh507d2LTpk3YuHEjNm/ejMzMTDRo0ABDhw7FiBEjcPPNN6NBgwYlXiM9PR2zZ8/Gt99+i9jYWPTv3x9vvvkmBg0a5ND/UlkeeAD44Qd90Y+l015phIZS6VtW87g4YNEiWgD27GHnoFcvJvkZOpRjAlcI6GNPTCYap//4g9uWLXwmXboAo0dzpUH79g4Xy8EKPyGB2SJWrQL+/JPeEe3bM2vEgAG0g6gG0Dji4lgy165lJ+z8ebqtDhvGZ3TLLbS41BBOnz6NDz/8EDNnzkRQUBCmTp2KSZMmlWiyz8jIwO+//45ly5Zh9erVSE9PR7t27TBixAgMHDgQUVFRKnysAzCZTNizZw82bNiAlStXYuPGjTCZTOjVqxdGjBiB22+/He3atSvx+3/++Sf+9a9/Yd26dYiKisKbb76JoUOHOvQ/VJQPPqDDWkYGlU16Op3n0tPpI6z5Bufnc1bUZOIrwLn0zz+n89qiRTRVBwcDd9zBNMkDBtSoam8XcnLoULl8OeMJJCXR3D9mDDBuHMe1DmA+xN4kJop8/rlI374ibm4ifn4iQ4Zw36lTdv95xTVw4IDIBx/weXl7i9SuLTJihMjs2SKZmUZLZzfS09Pl6aefFm9vbwkLC5Np06bJ5cuXbZ6bl5cnS5culYkTJ4qfn594enpK37595YMPPpBDhw45XHZFcXJycmTp0qUyefJkadKkiQCQDh06yAcffCBnz54t8XvR0dFy0003CQDp27ev7Ny506Fy25u8PJF580T692fT3LChyMSJIkuXiuTnGy2d62IyiWzaJDJ1qkhEhAggEhkp8u23Ijk5dv3pefZR+NnZItOni0RFibi7i9StK3L//SLLl7OUKaofqakiM2aIDB0q4uEh4usrMnasyOrVImaz0dJVCWazWX788UcJDQ2VoKAg+frrryWvhPK6b98+mTJlitSvX1/c3d1lwIABMnPmTLl48aLD5VaUH5PJJOvWrZMHH3xQAgMDxcPDQ4YOHSoLFy6UgoICm9/ZunWr9OvXTzw8POSJJ56o9s/47FmRF1+kgvf0FLntNpFly0QKC42WrOZhMomsWiVy550iXl4i9eqJPPecyOnTdvm5Klb4hw6JPPWUSGAgR4P33svuYgmjI0U1JSVF5OuvRW68kd3T1q1FPv1UJC3NaMkqTWxsrAwYMEDc3d1lypQpcuHChWLnmEwmWbp0qQwePFgASLt27eSjjz6S03aqnQr7cunSJVm0aJGMHDlS3N3dJSwsTD788ENJs1GOzWaz/PDDDxIcHCyhoaEyd+5cQ2S+Fk6dEnn8cTbNTZqI/POfImfOGC2VQiMpSeT990WaNaNB9ZFHRI4fr9KfqCKFv369yKBBtAu1aiXy8cccESpcnwMHRJ54QiQgQMTHR2Ty5Go3VTN37lzx8/OTyMhI+fvvv4sdLywslFmzZkmrVq3Ezc1Nbr75Zlm1apWYXcSyoRA5fvy4PPfccxIYGCh+fn7y9NNPS3JycrHzLly4II899pi4u7vLfffdJzl2tsFWBefPizz6KEeQzZuzr67GYM5LXh4N5BERtMA8+KDIuXNVculrVPgbNnACCOA876pVtFEoah5ZWWxJIiLYPX30UZH4eKOlKpWCggKZOnWqAJDJkyfbNN8vWbJEOnbsKJ6envLQQw9JbGysIbIqHENmZqZ88cUX0qhRI/H395e33npLMm34q6xbt05CQkKkXbt2cvDgQUNkLYvCQpGvvhKpX58j+u+/V3Pz1YmCApE5czjiDwyk21sJs07lpZIKPy6Oc7mAyMCB9EBQKETYosyYwaGEt7fI88/Tp8PJSEtLk169eklAQIAsWrSo2PHY2FiJiooSNzc3GTNmjBw+fNgQORXGkJOTI//+97+lbt26EhQUJLNnzy52Tnx8vPTs2VMCAgJk9erVhshZErGxItdfzyr40kvsjyuqJ9nZIq++KlKrlsh114ns31/pS1VQ4efnc5LBx0ekSxeRP/+s9C8rXJy8PA4v6tWj8l+1ymiJrnLhwgW5/vrrJTw8vJgiN5lM8umnn4qPj4/06NHDpolfUXNIS0uTp556Stzd3WXUqFGSlJRkdTwvL0/uu+8+8fHxkTVr1hgmpyU//iji7y/Sq5eI6qe6DkeP0g/e11fku+8qdYkKKPwjR0S6dqWyf/99ZRtSlI+kJHrzAyKTJonk5hoqTnp6uvTs2VOaNWsmx44dszp27tw56devn3h7e8s///nPEr22FTWPv/76SyIiIqRBgwaybNkyq2Mmk+mq0l+7dq1hMhYWikyZQleqf/xDNdGuSEGByMsv8xlPmlRhE385Ff66dZwI6tGD5nyFoqIsXSrSoIFIz55cF2QABQUFcuONN9pU9keOHJGIiAhp3bq17N271xD5FM5NVlaWTJo0STw8POTbb7+1OlZYWCjjx48XX19f2bdvn8NlKywUmTCB47Fff3X4zysczPLlDGkzZkyFOnblUPgzZtC98557DB+dKao5R4+KtGtHLxQDGsWpU6fabJC3b98uDRs2lF69esn58+cdLpeievHOO++Im5ubvPXWW1b7CwoKpF+/ftKmTRvJdqDfiskkMm4cTb1//OGwn1UYzMaNInXqiIweXe4YCmUo/NmzaTt44w2XCa6iMJiLF+noGRLiUGtRTEyMeHh4yPTp0632JyYmSmhoqNxyyy3VYomVwjn47rvvxM3NTb7//nur/WfOnJF69erJ888/7zBZPv6Yznnr1jnsJxVOQnQ0rTrvvluu00tR+Dt2sBRNnVqF4pWTU6cYma9ePc79dusm8uab+vH//EekTx92ae+9V6TospiMDJGHHhJ59ln7yZiXx45Qu3ZcM6Hx8ss0XSck2O+3qztZWTTtd+jgMA/+gQMHSt++fa3Wzufn50tUVJS0bdtWMjIyHCKHxrRp0yQqKkoASK1atWTixImyY8cOERE5duyYPPDAAxIQECCRkZHy4YcfXv3e6dOn5c4775RevXpJly5dZMyYMXLGztFTDhw4IP/4xz/E19dX7r777mu+3tq1a2XUqFH/z955h0V1dHH4tyy9K0WlKKKiKAiKGgQFYxdRgzWJGjtiiSYmMTF+SYwmJkbTLLHGRE3sMdEoKFYIAqIizS4qRZQqve+e749hF5amCLtLmfd59tnduffOnLtc5sycOXMOASA/P78GkVEZrFy5kjQ1Nas4dm7bto1UVVXp4cOHcpchOpoF0qnwiMidxYtZrC2Abffz9i6PuSWJGgcQjR5N9M8/ipOrpbJxI9uvHxz8wlNrUPjFxUS2tmzrnTL31R86xJ6cfv1k5RCJiNzciHbtqnrN6dNEFhbsuqVL5S/j/PmyCv/TT9nslUdfq534eDYwkuegrIyQkBACQBcr7Sr5/PPPSV9fX2lb7oqLi6lnz54EgP7991+ZY/7+/tStWzcZq0N+fj517dqVli9fTlQW/e2dd96h7t27U0FBgdzlNTc3bxCFT0R09uzZJq/wRSIRjRw5krp06ULFFRZSS0pKyNramhYtWiTX9sViFoN90CDFd9MPH7L5lr4+S5dSkZUrmT8BRzGIxUSjRhH16PHC56AGhb9lC7MTPHokJxHrwNixTHn/9FN52VdfsWFkZfbtY66Lp04pT+ErkmvX2PC6qbJjB/MPkfNMaOHChWRvby9Tlp6eTjo6OvTdd9/Jte0XcfXqVRIKhWRpaUk5ZZulU1NTqUOHDnT9+nWZc7du3UoqKioyoV8fP35MAKo4kckDrvCr8vjxY9LU1KyyVLR+/Xpq3bp1jbkYGoIzZ9iKa3i43JqolR9+YN3sG2+UlwUGsmCrCjaYtXhu3WJpa15gUalB4dvZNR5FkpjIhpG6uixy25UrRB07ElUT61xKQYHiFP7ChcpT+BMmsKWLpkpJCXPg++QTuTbToUMHWrVqlUzZpk2bSE9PT6pklcmyZcsIAL377rtERDR27Fhav359lfNGjBhBnTp1qlJubm5OI0eOlLuc8lD4pxtRfIZXZcaMGdS3b1+ZskePHhEAunTpkhzbZSubykIkYsZXgOivv5h7jrX1S5mWOXJgyBCiSZNqPeWASpWMuYmJQEwMMGWKQhL0vhBzc2DdOpa8ee5cYPp0YPduoFWrhmvjiy8AAwOWB742srOBRYuAjh0BZ2dg2DCW4FjC6dPAkCGAQMB+QwD4/nugTRtgzBjgxg1g8mSgSxd2LDWV3Y+tLdC/P7s2Orq8vqIi4H//Y4mT+/cHHBxY4uR//gF8fIDjx4ETJ5gs33xTLuPixYCdHSu3sWEyZ2e/WB5Fo6rKEkKfPi23JlJTUxEXF4f+/fvLlJ87dw7Dhw+vMbe9IlmzZg2sra2xZcsW+Pj4IC8vDx988EGV86KiomBubl6lvH379oiKiqqx/qdPn8LCwgIjRoyoVY74+HiMHTsWAwYMQP/+/dGtWzcEBgbWeH5OTg7c3NzQr18/jBw5El27dsWPP/5Yp/ru3buHuXPnol27dmjVqhWWLl0qc/zgwYNwdHREv3790Lt3b6xevRqlpaWIiYnBuHHjIBAIEBwcjB9//BHdu3fHjh07ar1HeTB+/Hhcv34dz58/l5ZZWVmhXbt2uHbtmtzaDQwERo2SW/UvREUF2LULUFNjXc7MmexV6V+tRk6fBvT1ga++qv0cW1vA1BTw9mZdr5YWayM0tPw8kQj4/HOgWzfAxQXo2xf46y927MQJoFcvQE8PePYMeP99oF074O5d9hu6ugKDBgGOjuw8SVdJBPzwAyuXdKVvvAHcucOO+/sDvXsD2tpMTk9P1oalJXD48Cv/rK+Mhwe7n1qpMgY4e5YN2WqbQSsasZit2UuCt7yIus7wP/+c7W+oLVKWRAZra9lFq8om/X37WNsV4x+6ujK/gnffZUmPHR1ZfX37EvXpU54Eef58IlPT8u9jxxJ16CAbk/7rr9lWSSK2Bl55hu/uzuqV2NSePWOOhQMH1i6Psti3j8WMlBM3btwgAHSv0o6Abt260Zdffim3duuKZMYrEAjoUQ1LaSoqKjR69Ogq5aNGjSKhUFhj3UlJSWRubk5Dhw6tVYYhQ4bQggULpN+3bdsmE3a48gw/NTWV3njjDakj5NatWwkARZc9+7XVJ7nf1atX0507dyg+Pp6WLFkiMyv+999/CQAdPnyYqGzWrKmpSRs2bJCpY/To0fTtt9+Sj48Pbd26tdZ7lAdxcXEEgEJDQ2XK+/fvT++//75c2iwpYeb8o0flUn2d+N//WJfXqVPdUuz6+jLD7Ys8zOfPZ3vOHz1i3eb9+8yyoK9f7iz44Yfs+/377PuBA0ymMj9YWrmSfffxYU5ur7/OVkQNDJirmIS33mLJhqhMLbRqxczlVPabT57M0gpLktlI6j11ivma37zJulN9fcVngvf1ZbJUk/pBQjUm/b//Zlc1tjBNv/zC5DI2Lv+L1IQ8TPqXLrE6N2+WLX9Zhf/aa+Xfo6PZYhdA9Pvv5eVBQazs4EGi0FD2+eefZdu7c6c8TG1lhS+p88AB2Wt272blgYE1y6MsJM+bnP47JA57cZUS+VhaWkoVR2OgqKiILC0tCUCV/d1U5uAHgMaOHVvlmMTjvb6RAU1MTKQOgUREhYWFlJmZKf1eWeEXFRXR3bt3pd8lv7VEqddWX3Vr+BIz+JYtW4iIaPDgwWRlZSUj49ChQ6lbt27V1lFYWFhlYKcI0tLSCECVKHtDhgyh+fPny6XNnBz2b+PrK5fq68StW0wWgCVObWiqc5OSdI9ff826e21t2blgSQlzQ/PxYd8lilni2xoXRxQSUvU3TEtjg5b8fDYYqfzne/iQXSMZpFSul8q85oEGT237QgICWLuVoj9XpBqTvokJe3/2TD52h1chIYGZrOfNA9LSgEpmP4UQHMzeX3ut/nXZ2QHh4exz587l5WZm7P3hQyAoiH3u00f22q5dgZpMs1eusHdbW9nynj1lj1cnj7J4+hQwNATU1eVSvYGBAQAgKytLptzY2BjJyclyafNV+PTTT+Hu7g5TU1N88803uHnzpsxxNTU1CIVClJaWVrm2uLgYQqEQqqqq9ZLBzc0NGzZswLx58xAaGgoNDQ3p71cd6urqsLGxkX6XtC+Rsa71aWpqSu8HAMLDw9G54v8HADMzMzx69AhEVOV6DQ0NdFHC8tSzsr7SRNJ3lvH8+XMYGhrKpU0dHfYvk5Yml+pfmtJSYPZsZiYXCFgXXVAg/3b79gWEQrZyevcukJ8v25WqqjJV9vBh9de3bw84OTHT/ttvA19+yc41MmL13rzJVpErd6UdOzKzfU1dKcCWHACg7DFWGKmpbJmlttXuqgrf0ZEtygQEyFe6l0UsZuvcq1cDW7YA9vbA/v2ya+eKID2dvRsZNUx9OTns/f332QLSoEHArFmAuztrQ7Ie2Lr1y9eZmcneJU+cBMk6dSWl1ygICAD69ZNb9R07doSamhpu3bolU+7k5ITLly/Lrd26cPbsWfj5+WHHjh3YuHEjiouLMWfOHIjFYpnz2rRpg2zJAmMFnj9/jnbt2tVbjl27dmHevHk4dOgQ+vfvj169euHevXs1nn/r1i2MHz8ebm5umDRpEj799NN61VeZnJwcREZGYtCgQdJXXFwcnJ2dUVJSUq97bUguX74MbW1t2FbQDiKRCHfv3kXXrl3l0qZAwMbxV6/KpfqXZtUqNgf54Qdg/nwgNpatpcsbFRW2/p+aWt6V7tlT3pUOGsSUc6dONdehpsbctlxdmR9B587MpSkvr+auFGWDrcbYlV69ynwYNDRqPqeqwtfRYav/u3bJV7qXZe1a5mQ2cyb7C/36KxuCLVhQ/pf7Xfp+AAAgAElEQVRWBDo67L2CY0690Ndn79u2AZcuyb68vcuHaZIn72WQzCby82XLc3NljzcWUlKY4+GkSXJrQlNTE7169cKFCxdkyt944w2EhITg/v37cmv7ZUhLS4O3tzf+/PNPaGlpYcqUKRgzZgyuXLmCjRs3ypzr4OCAxMTEKnXExcXB3t6+3rIYGhpi27ZtSE1Nxb59+/Dw4UPMnz+/xvPHjBmDkpISBAQE4MiRI1i7dm296quMvr4+nJ2dcenSpSovdTlZhF6FPXv2wNPTE2pqatKyK1euIC8vD87OznJrd+RI4O+/mcOaMggMBI4cATZtYt/XrWM+1j/+CFy/Lt+2RSKmdC0syrtSH5+qXekvv9ReT/fuwMmTzKC9ciW7nw0bau5KUdadNraulIg5KXp41H5eVYUPAB98wGZe//4rH+lelitXmEf+9u3lZX37MpN+QgLw8ceKk0ViFg8JaZj6HBzYu8S0XxkXF/Ze284BgUD2u8Q9VuJGKkHi+d8QyxENyWefMWvG22/LtZnx48fj2LFjKCwslJaNHDkSNjY2+FwR05FamD17NhYvXgxHR0dp2datW6Gvr4///e9/ePTokbR87NixiIuLQ2pqqrQsNjYWz549w7hx4+oty4kTJ4Ay0/i0adPg4+ODO5WfpTJyc3Px8OFDvPbaaxBUfg5fob7qcHBwQGRkZBVLR2Pi9OnTCA4OxpIlS2TK9+3bh+7du8vM+huamTOZojpwQG5N1EhmJjNI7t3LTNwom8Ns3cqU8Zw5gDyNMBERzPjbty/zntfSqrkrrYn4eFYPygy3a9YwY+OdO2yVU1e3alf6+DFT+I2tKz12jC1JzJr1ghNrXN6fOpWobdtaPQDkSnY2i99Y3T7WvDzmLS8QlDuiVaSuTntffPFiL/38fOYx364d0X//Mc+O1FQiT8+6O+1R2SbWnj1ZfRcvsvpKS5mrp8RLf/hw5p66fTvzJiEiysws99q3sWEe+YWF5a6ZEi99yfeUFBbC1t29dnkUzYkT7O9X2cFQDjx9+pS0tLRocyWHy1OnTpFAIKA9e/bIXYbq2Lx5Mw0dOlQm3K8Eicf7sGHDpGX5+flkY2Mj9fwWi8U0bdo06tatW62R9pKSksjCwuKFXvp2dnaUkpIirXvcuHE0btw46fHKTntGRkY0cOBASktLo4SEBFq1ahUBoANlf9Pa6qvOae/p06cEgH788UciIjp69CgBoEWLFkmTGmVnZ9Pjx49rrEORPH/+nNq3b0+TKm1+Tk5OJm1tbdq4caPcZZg3jwX2lHiNK4pJk4jWrKn+2JQprAv86qva6zh9mnW7L9osU9lpr6SEdbuWluXOcosXEwmFbANTfj7z5k9JIUpOZserc667epXIy6vcPz0nh4UKLnv86IsvmJf+7dvl7b75JpGJSe317tzJyiTXyZv0dLbpaurUF55aSyz9zEwWMsnJqVY/f7mwdi2RgwP7K8+axZRgRRYtYsoOYApzzhwW9eH4cfYf4OHBjrVvz56+99+vPfSTZFvei1JN3b1LNHIkcwk1NWVP/TvvsGhxH3/MIhQOGsTanjyZ5ancsIGda2xM9NFHslvskpJYDEoTE+ZS2rkz0dy57LensoHNhx8SWVmxNtq1Y4pbIueePUSGhqx+SSzLzEyiBQuYknd1ZSGSFy8uv//a5FEUYWHs91Zg0KClS5eSqampTJQ6IqJPPvmEtLS0qkS1kyfR0dH01ltvkaamJrm4uNAvv/wic9zf358mT55MAoFAqvQlSjQ+Pp7GjRtHzs7O1KdPH5o0aRIlVo5tWgnJtrzhw4fXet7EiROpa9eu5O7uTv3796e3336bnj17RjExMfTee++RlpYWWVlZ0YoVKygjI4MOHz5M5ubmpKmpSQMGDKBTp05J5b1+/XqN9UVHR9O4ceMIAHl6etKVK1coISGB5s2bRwDIxcWFAssG8vv27SNHR0fS0NAgExMTcnV1pWPHjsnU4eHhofBBW1FREQ0ZMoTMzc2rZFicPXs2mZmZUb4Csovm5LB50YgRislvduwYawtgcb8qJ+zZvJntAAbYbts332Tb36rD15d1AzUNHCTMn8/q8vRkc6AuXYjGjSvfgkdl0eBXrmRdpbo6GwyMGcPmXSdOsHQskm15//3HromLY7La2RENHsx2SH/6afnWQrGYJSayt2cBjrp3ZwMESSRuf//yet99lw0Czp9nXTTAVIMi5stTprCBSqWurTpekC3vwQOmZHr3rhowmcN5Fc6cYYOUUaMUuvXz+fPn1K5dO5paaRhcWlpKw4cPJ1NT0ypJUDic6sjNzSUPDw/S09Oj8Epxbf38/EggENBRBW6QDwlhyVOWLm2eSU3nz2c7kDlV+eQTZtmolCakJl6g8Kls42GPHkzx8w6RUx8ksfOnTGF2NwXj5+dHKioqtGnTJpny3Nxc8vT0JB0dnSpJbDiciqSlpZGLiwsZGRnR5cuXZY7FxsaSsbExTZ8+XeFyHTnC/rW8vZuf0ldmupLGzMqVTNnXwbj1EgqfyszEI0Yws/OGDXULp8ThpKSwBSaBgC3sKbFH+vrrr0lFRYV+++03mfKSkhKaM2cOqaqq0hdffCGT/YzDISI6f/48dejQgTp37kz3K9qTy5LodOjQgfr06UO5Ckr5XJmjR5nSf+stxa/CyhOu8GXJy2NBhoRCoj//rNOlL6nwqcxjYc0alnzZyYnoxo1XEJXT4tizh/kLtG/P4k82Aj777DNSUVGhvXv3Vjm2adMm0tbWpl69elFkZKRS5OM0LnJzc2nRokUkEAho/PjxVdbs4+PjydramhwcHChN4lyrJPz9mYtO165EERFKFaVB2L+fRQZXU2OuSCEhypZIudy8yQzuRkZEJ0/W+fI6KHwJd+6wmPKqqswDIj6+zlVwWgABAew5UVEhWrKk0U05VqxYQUKhUOoRXpH79++Tq6srqaur0wcffKD0TpyjHEQiEf35559kZWVFRkZGtH///irnhIeHk5WVFfXs2bPRPCdPnjDHMS0tFnq2sFDZEnHqS1ER0bp1zF/c1fWV1e4rKHwqc1/87TfmEqmhwbzmuVMfh8ryAQwZwtxUBw9u1H4f3333HamqqtLEiRMpq9IuDpFIRJs3byZTU1MyMDCgr776SmmmWo7i8fX1JUdHRxIKhTRr1ix6Wo279c6dO0lTU5MGDx5cZdavbEpLib75hu3q7dKl0RjXOK+Avz+zcmhpMSN7PVJmvKLCl1BURLRtGzPXamqyhYUrV+pVJacJUlzMUk5JtiS6uVUfP6ERcunSJWrbti3Z2NjQjWqWqXJycujLL78kPT09atOmDX355Zf0TNGbnjkKoaSkhA4dOkT9+/cnADRu3DiKiYmpcl5OTg7NmDGDVFRUaOXKlVTaiH2a4uPZ7mGAbWmrLmwJp3ESHFy+w9zLi2ULrCf1VPgSCgtZcBgHByadkxOLPsBnRM2buDjmKtq2LfMgGTeu6sbcJkBSUhK5u7uTqqoqLVu2jLKrWX5ISUmhFStWkLGxMWloaNCMGTOqbMniNE3S0tLom2++IUtLSxIKheTl5UXBwcHVnnvkyBGysLAgY2NjOtWEps0XL5ZnGHdzY7tjOY2TCxeYcRRg+/9riwdXRxpI4Vfk2jW2N0Rbm9kgPD2Z4xZX/s2D9HT29/T0ZH4cbdqwoEMNMPxUJmKxmPbs2UMmJibUrl27GgO5FBYW0p49e6hnz54EgLp3705ffPFFjTnsOY2TwsJCOnHiBE2fPp20tbVJX1+fvL296Y4kqkolHjx4QKNGjSKBQEDTp0+nZEmotSZGUBD71xUImJn4229fnG2cI3+ysticWRLIx9WVBQxqYOSg8CWkprKwSxLHLQMDFnro+HGu/JsaiYlsD/3QoWwmr6PDQmj9/bdCg+cogpSUFJo1axYJBAJyd3enC7Uk+L506RLNmTOHDA0NSSgU0tChQ2n37t3ScLKcxkVxcTGdP3+evL29qVWrVqSiokKDBw+mX3/9lXJycqq95smTJ7RkyRLS1NQke3t7+k8Spq2Jc/06C0qqq8tWY6dNY8a5Rrw60ewQiZhv88yZbH6so8MCy8pxVVyOCr8iiYlEP/3E7BMqKiz24eDBzO0wIqL5RYpo6hQUsPC9H37I4koCzFozYQLR4cPlsf6bMcHBwTR48GACQAMHDqRz587VeG5BQQEdPXqUvLy8SENDg1RUVKh///701VdfVesXwFEcycnJ9Ntvv9HEiRPJwMCAAJCDgwOtX7+eEhISarwuISGBFi9eTJqammRubk6bNm1qlrEZsrPZzLJPH/ZvbmLCDLT+/vVyDuPUQGkpG1gtWMBWQgG2Er5lS3lEdTlyQEBEpKCEPoyUFMDfHzhzhr2npADt2rEExv37AwMGsMx0QqFCxWrR5OayzISXL7NXUBDLC9m9OzBiBHu5uVWfHLqZExQUhNWrV+Ps2bNwcXHB0qVL4eXlJZMKtSK5ubk4e/YsTp06BV9fXzx9+hTm5uYYPHgw3N3dMXDgQNjY2Cj8PloKz58/R1BQEAICAhAQEIDw8HCoq6vD3d0dnp6eGD16NDp27Fjj9ZGRkfjll1+wZ88emJqa4pNPPsGcOXOgUVuS8WbCvXvA0aPsdeMGyyA3YgQwbBh7mZsrW8KmydOnwNmz7HXmDJCaylTcxInAhAmsm1UQBxWv8CsiFrMny9+fKZngYJZ3UVcXcHYGXF0BJyeWSrZ9e6WJ2awoLWU5HyMigLAwpuAjI1lOy44d2W/u7s7+0y0tlS1toyEkJATffvstTp06BRMTE8yePRve3t7o0KFDjdcQEcLDw+Hr64tLly4hNDQU+fn5aNu2Ldzc3DBgwAD06dMHDg4O0NbWVuj9NAfEYjHu37+P8PBwhISEICAgADExMSAi9OjRA+7u7hg2bBiGDh0KHR2dGuspLCzE4cOHsW3bNoSEhKBbt2547733MGvWLKirqyv0nhoLsbEs5eqZM6yLKCxkimnYMDY3e+01Nk/jVCU5GQgNBQIDmZKPjgbU1VnXOnw4U/JduihFNCUr/MqIxcCtW+wJCw5mr9hYgAho3RpwdGTK39ERsLdnv5qurrKlbrykpAC3bwNRUUypR0QAMTFAURF7Ah0cABcXZlVxcQHMzJQtcaOmuLgYa9euxe7du1FaWoqUlBSMGjUK06ZNg6enZ61KBQBKSkpw9epVBAYG4r///kNwcDAyMzMhFApha2uL3r17o3fv3ujVqxd69OgBIyMjhd1bY6eoqAh37txBVFQUwsPDER4ejhs3biAnJwdqampwcHDAwIED4e7ujgEDBrzwtyMihIWF4dChQ9i7dy+ys7Ph5eUFHx8fDBo0CAKBQGH31tjJzwf++698lhoTw7rq9u2ZUdbZmeWRt7MD9PWVLa1iyc1lv0dYGFPyoaHAo0eAikr5AGnYMGYgfUH3oAgamcKvjuxspqwkCisiArh5kw05AWZnsrFhry5dgK5dAWtrNjvV01O29PInORlISGADo3v3gLt32fv9+8xaArDBUq9eTMFLXt27AzWYpTmyiMVi7N27F59//jkyMjKwbNkyLF++HKdPn8auXbtw/vx5qKurw8PDA5MnT8bo0aNfasZORHj48KFUgUleaWlpAABjY2N069ZN+rK1tYW1tTU6dOgArWa4vCISifD06VM8evQId+/exZ07d3D79m3cuXMHcXFxEIlEUFdXh729PZycnKQDJHt7e2hqar5UG2FhYThy5AiOHDmCuLg4dOnSBTNnzsTs2bPRtm1bud9jcyA7m60AhoaWv6enAwIBYGXFFL+dHTNb29qy7ripd8W5ucDDh2z+FB3NlHx0NFPuRGz547XX2MvZmb0bGChb6io0AYVfHaWl5Qqu8ispqfw8fX2m+Nu3ZwMDCwv2MjaWfTW2mVRJCZCWxl7p6WymnpLC7i0xEYiLA548YZ+Litg1amrsv83Ghg16Kg6A+OLbK3Pu3Dl89NFHiIqKwtSpU7Fu3Tq0q2TLTEtLw7Fjx3D48GFcunQJmpqaGDVqFEaOHInhw4fDso5LIwkJCbhz545U4UmUX1KFZ9vExATt27eXvjp06ABTU1OYmpqiTZs2MDY2homJSY2+BoomIyMDKSkpSEtLQ2pqKp49e4YnT54gPj4ejx8/Rnx8PJKSklBSUgIA0NXVRdeuXaUDHcnnrl271ume8vPzERAQgDNnzuD48eN4/PgxOnfujEmTJmHy5MlwdHSU4123HB4+lFWEMTGsOy77c8LICOjUiSn/jh2BDh2YQdHUtPxdWW4SxcXl3WtyMltzj4tjyvzhQ/aeksLOVVVl3aq9PXtJBjbW1sqRvY40UYVfG7m5wOPHQHw8U4hPnrC/XmIieyUlATk5stcIheWKX1eXDRT09JiTmq4uG6ppa5c7renryzoVamvLPq25ueVPOsCsEQUF7HN2NrOR5ecDz5+z8vx8ICuLHUtJYZ8rIhAAJiZs0czSkr0sLGQ/d+jAZ+wNyMOHD/Huu+/C19cXQ4cOxQ8//AB7e/sXXpeamoq//voLx48fR0BAAAoKCtC9e3eMGDECI0aMgJub2yvPzrOysqTKUfKekJCA+Ph4xMXFISUlBaWlpTLXtG7dGqamptDV1YWhoSF0dXWho6MDHR0dtGrVCjo6OlBXV4dQKIR+BXts5e+FhYUokDzDlb4/f/4ceXl5yMvLQ25uLrKyspCXl4ecnBykpqYiLS1NqsgrymVmZgYrKyuZgYtk8GJhYfFKvxEAREVFwd/fH2fOnEFQUBCKiopgb28PDw8PTJo0Cb17937lujkvT3Ex8OABWw5YuZIpRn19pkTj4lh3V5HWrYG2bVl3q6fH3g0MZLtjVVVZa4GODludRNk8KTe3/JikGy4oYF1+Tg4zemZns1dWFlPw6emycujpse5UMjixti7/3Lmz8gYmDUAzVPgvQ1FR+ew5NZW9JDPqvDz2NOTkMEWcl8eekvx8priJyk3lEnJymNVBgpYWUNHEWPEp1dNjAwQdHcDQkH3W1i5/yk1NZa0Py5cDV68CFy4o1J2zpVJUVITvvvsO33zzDTp16oQtW7bAzc3tleoqLS1FaGgoTp48iXPnziE8PBxCoRAODg5wdXWFk5MT3NzcYGVl1WDyV55JJycnIzU1Fbm5ucjMzEROTo5UOWdmZiI3NxclJSUoKipCfn6+tJ7i4mLk5eVJv6upqUG3gr+Mqqoq9MqeaQMDA+lAQk9PDwYGBtLPEkuDxPrQ0JaHkpISREVFISgoCJcvX0ZAQABSUlJgZGSEwYMHY+jQoRg1alSdrSychqGwkM2ILSyAf/9lXZqEgoLyGXXFGbZEIWdnlyvonBxWV1ER64olZGczf2OUzdsq+hBIumENjfJBQ6tW5Z8NDGQtDO3asQFHM1wtk9BCFX5TIjcX8PBgyn7bNmVL06y5dOkSFi5ciLi4OHz00Uf49NNPG9RL+8mTJzh//jxCQ0MRHByMmJgYiEQidOjQAS4uLnByckLPnj3Rs2dPtGnTpsHabS4UFBTg5s2biIqKQkREBEJDQxEREYGSkhKYmZmhf//+cHFxwcCBA+Hk5AQVFRVli8wB24DVuzeb13CUClf4TYK8PGa34iZ7uZCeno53330XBw4cgJeXF37++WeFzAhzcnIQFhaG4OBghIaGIjw8HM+ePQMAmJqaomfPnrC3t4e9vT26desGa2vrFjEQyM/PR2xsLB48eICYmBhERUUhKioKsbGxEIlE0NbWhp2dHZydneHs7AwXF5dat0dyOByAK3xOi+fUqVOYO3cu1NTUsG3bNnh4eChVntTUVKmCi46ORlRUFG7evInCsl0purq6sLa2RqdOnaTv7du3h5mZGdq2bQtTU1MIG3nQqszMTDx9+hTJyclISEjAw4cPERsbK32XDHoEAgE6duwIBwcH6cDHwcEBnTp14rN3DqfucIXPaZnk5+djxYoV2LRpEyZOnIht27ahdevWyharWkQiURXFWPHz8+fPpeeqqKhI18vNzc1hamoKIyMj6OvrQ09PD/r6+jAwMIChoSH09fWhr68vjSKnqakpdSgUCAQwNDSU1pufn4+ish0hIpEI2WUeV0SEzMxMZGVlITs7G9nZ2cjJyUF2djaysrKQmZmJZ8+eISUlBUlJSUhOTpYOXgBAXV0dHTt2hLW1dZWBjLW1NQ9IxOE0HFzhc1oeISEhmDFjBlJTU7F582ZMnTpV2SLVi9zcXDx58gQpKSl4+vQpnj17huTkZCQlJSElJQUZGRlSZSx5yQtNTU3pQEIysJBsFWzbti3atWuHNm3awMzMTDow4UFumj4FBc3a2a25wBU+p+VARPjqq6+watUqjB49Gjt27GixwVaeP38unYVLtszl5eWhuLgYRIRp06Zh5syZ6NOnD1Bp9g8ArVq1kn6uzlrAaTk8egR4egLvvQfMm6dsaTi1wBV+kyY+Hpg+Hdi9m0W14NRIZmYmpk+fDn9/f3z//fdYvHixskVqtDx58gQWFhYICAh45S2JnJZBQQGL8WViwrbd8RhfjZqDqsqWgFMP9PXZptTXX2fRLbincrVERkZiwoQJKCwsxMWLF+Hi4qJskRo1sbGxAIBOfBDJeQFaWsBvv7FwsjytSeOHu7o2ZQwNWaZBLy82xOZU4c8//4SrqyvMzc1x7do1ruxfgocPH0JTU7NKCGEOpzqGDuXKvqnAFX5Tp1Ur4OefeVSLShARPv30U0yfPh0LFizA+fPnW+x6fV2JjY2FtbU13/rG4TQzuEmf0+woKSnB3LlzceDAAfz+++945513lC1Sk+Lhw4ewbiLZQDgczsvDFT6nWZGXl4dJkyYhMDAQx48fx6hRo5QtUpMjNjYWzs7OyhaD04jIyGDJbThNG26z4zQbkpOT4e7ujvDwcAQEBHBl/4rExsZyhz2OlAsXmCf+P/8oWxJOfeEz/OZMSgrLCGhrq2xJ5E5iYiIGDRoEFRUVBAcHc5P0K5KTk4O0tDT++3EAsAx2o0cD48YBI0YoWxpOfeEz/ObMZ58B7u5AZKSyJZErycnJGDp0KLS0tHD58mWurOoB35LHqYiZGRAQABw4wCPpNQe4wm/O/PAD0LMnsHy5siWRG5mZmRg1ahREIhH8/f1hwrcn1ovY2FioqKjAyspK2aJwGgn9+gE8+nHzgJv0mzM6Oiz8VYVkJc2J7OxsDB8+HOnp6QgICOD7xhuAe/fuwdLSEpqamsoWhcPhNDBc4Td3tLSapS0uPz8fY8aMQVJSEgIDA/mMtIGIiYlBjx49lC0Gh8ORA9ykz2lyiMVivPXWW7hz5w7OnTvH1+wbkJs3b3KF38IgAgIDlS0FRxFwhc9pcnzxxRfw8/PDkSNH0K1bN2WL02wQiUS4d+8eV/gtiJwcYMIEYPhwlouL07zhJv2WDFGT88b5559/8PXXX2Pbtm08k1sDExsbi4KCAq7wWxBBQUBoKHD2LNC+vbKl4cgbPsNvqeTnA4MHN6loGrdv38aMGTOwcOFCeHt7K1ucZsfNmzehoqIC2xYQt4HDGDUKuHcPGDhQ2ZJwFAFX+C0VLS0WkGfyZODkSWVL80IyMjIwduxY2Nvb44cfflC2OM2SiIgIdO7cGTo6OsoWhaNAeKa7lgM36bdUBAJgyxbA0hLo3VvZ0ryQOXPmoLi4GMeOHYO6urqyxWmW3LhxA7169VK2GBwOR07wGX5LRiAAVqxg4bQaMTt37sSJEyewZ88emJqaKlucZkt4eDhX+BxOM4YrfE6jJjY2FsuWLcNHH32EQYMGKVucZktKSgqePHmC3k3A2sOpG7//DmzapGwpOI0BrvA5jRofHx907NgRq1evVrYozZrw8HAA4DP8ZsaiRcDs2cCzZ8qWhNMY4Gv4nEbLvn37cOHCBfz333983V7O3LhxA5aWljA2Nla2KJwGxMWFeeJ7eipbEk5jgM/wOdVTVAR88w1QXKyU5rOzs/HBBx9gwYIFcHFxUYoMLYmQkBA4OzsrWwxOAzN1Klf2nHK4wudUz507wLffskTY+fkKb379+vUoKSnhpnwFQEQIDQ1F//79lS0Kh8ORI1zhc6rHwQG4cIEt/qWlKbTplJQU/PTTT/jkk0/QunVrhbbdErl//z5SU1O5wudwmjlc4XNqxskJCA9XeMzN7du3Q1NTE++++65C222phISEQENDgzvsNVGCg5UtAaepwBU+p3YUHGtfLBZj9+7dmDlzJrS1tRXadkslJCQEffr0gYaGhrJF4dSBnBxgxgxgwADg2jVlS8NpCnAvfU6j4tKlS3j8+DHmzp1b7fHi4mJ89913KC0thaamJj755BMAQFRUFAIDA7Fw4UKoqDTucWxN91AbiYmJ+PXXX0FEcHZ2xsiRIxtMnsuXLzdofRLS09Oxe/duzJo1q1F6/3/99dcoKSlB27Zt4ePjo2xx6sytW8C5c8C//wJ9+ihbGk6TgDicRsRHH31Etra2tZ5TXFxM06ZNIwMDA2nZmDFjCACFhYUpQMr6U909vIisrCwSCoW0dOnSBpMjOTmZBAIBnTx5ssHqlPD9998TAPruu+8avO6GoKioiFxdXcnBwUHZorwyBQXKloDThDjQuKdCnMZLaSkQEdHg1Z47dw7Dhg2r9Rw1NbUqCV7Wrl2LrVu3wsnJqcFlqkx+fj5OnTpVrzqqu4cXoa+vX682q+PixYsQCoUYKId0abNmzcL333+P2bNny5QfOXKkyrnVlckbdXV1aGpqKrzdhqSJi89RMFzhc16NnTuB/v2ZPbGBKC4uRlRUFAYMGPDCcwWVfAvs7Ozg4+OjEHP+zp078ffff9e7nsr38LI05D1euHABffv2lctgolWrVli2bBmMjIykZZGRkfj0009lzquuTJE09iUgDqeh4Gv4nFfD25vN8OfPB4YOZel260lsbCxEIhFsbGyqHEtMTISvry/S02wlaAsAACAASURBVNPRpk0bJCYmSo+dOXMGISEhAICFCxfC1NQUmzdvRlpaGmxtbTFlyhTcvHkTQUFBmD9/PgDg3r17OHPmDEQiEZycnKrMcDMyMnDq1CkkJCRAXV0d5ubmcHd3R1hYGNavXw9TU1OsWrUKvXv3xtixY1+qztruoS6oq6vj4sWLCA8Ph6qqKoYMGQI7OzsQEb766iuIRCIAgKqqKlasWIGSkhJs2LABpaWlEAgEWLx4sVQJX7hwAW+++SZQZiUpLgu0pKKigkWLFskoawl//fUXoqOjAQBJSUkwMzODlpYWPv74YyQnJ+Off/6BnZ0dzp07ByKCh4cH+vXrhytXruDjjz9Geno6Vq1ahdatW+O1116rUrZkyRKgzAfg+PHjSEtLg42NDUaPHg01NTWcO3cOQUFBUv+Ha9euISAgAIaGhnj77behVcdnUUNDA7du3cKlS5eQk5ODPn36YMiQIQCAPXv24NGjR0DZAG3GjBmwsrLCzp078eTJEwDA2LFj5ZaDICeHzeLV1ORSPaeloexFBU4TRiwmiotrsOpOnjxJACgnJ0emfP/+/aShoUGLFy+m48eP0/79+2ngwIEy69+bN28mABQdHU1ERIWFhdSnTx9ycnKiiRMnkpmZGbVt25aIiLZv305aWlq0fv16OnToEHXo0IF8fHykdfn6+pK+vj75+PjQiRMnaO/evdS3b1/aunUr+fn5kb6+Po0YMYL8/PwoJibmpep8mXt4GYRCIdnZ2dGSJUvos88+o0GDBpFAIKB169YRla3J6+npUffu3SkvL096XUFBAVlbW9OtW7ekZfHx8QSAzp8/T0REOTk51KNHD+rQoYPM3+DJkye0e/duGTl+/PFHWrJkCYlEIlqyZAmpqanRihUryMzMjLS0tOj27dsUHR1NAGjTpk1ERHT58mUaMGAAtWvXjvz8/CgwMLDaMiKisLAwatWqFXl7e9Pff/9NQ4cOJScnJ8rLyyOxWExLly4lFRUVeu+992jmzJk0adIkEgqFNHjw4Dr9nkOGDCETExPy9vamL774gt5++21SUVGhMWPGUGlpKRUWFpKbmxsJhUKKjY2VXldaWkpTp06lbdu21am9unD+PJGVFdGqVXJrgtOyOMAVPqfRcODAARIKhTJlKSkppKWlRTNnzpQpnz9/voyy3Ldvn4zCJyJydXUlW1tbevbsGRERLV++nJKTk0lDQ4M++uijKteGh4fT8+fPycDAgKZNmybT3j///EM7d+4kIiIjIyOaM2eO9NiL6nzZe3gZKjvticViGj9+PKmoqEgVkre3NwGge/fuSc+LiIioogx37dpFWlpaVFDB8+ubb74hANKBDBHRmjVrSENDgzIyMqRlY8aMoRs3bhAR0cqVKwkARUVFEZUNfmJjYykhIUFG4RMRTZgwgTp16iQjR3Vljo6O1LdvX+n3hIQEEggE9OOPP8q0WVH2ZcuWEQBKTU196d9zyJAhVZz2fv75ZwJAv//+O1HZYA2A9O9PRFRSUkKdOnWSGVQ1JDk5RMbGRF5eRGWPL4dTX7jTHqfxUFBQUMUce+LECRQUFEjNznVFX18fbdq0AQCsW7cO/v7+KCoqkppsUSFDXGhoKE6ePImsrKwq7Y0YMQLjxo2rto0X1Vnfe6gNgUCAOXPmQCwWw9/fHwCkWxr37t0rPe/PP/+s4jz377//YujQoTKOa1OnToVAIMCBAwekZfv370dRUREOHToEAMjJyUFCQgIcHR1l6uvSpQsAwNvbG9bW1q98T4mJiYiIiJD5PS0sLGBkZCRduqmObt26AWVLAfVhzpw5EAgE8PPzAwCMHz8erVu3xp49e6Tn+Pv74/XXX5dbrAhdXRbz6tgxoOzx5XDqDV/D5zQa1NTUUFJSIlP24MEDAED7Bor2l5CQAJStQ0uUR3Z2NgDgyZMnUFVl/xKWlpYy12lqatbo0f2iOiVr6g11D5WR1JuUlAQA6Nu3LxwcHLBv3z6sXr0aRARfX198+eWX0muKiopw/vx5fP/99zJ1WVpawt3dHQcPHsRXX32Fy5cvw8XFBaWlpdi7dy98fHzw77//wsvLSy73ggq/5/Xr17Fq1SppuUgkkq6bV4fECZKI6tW+jo4OWrduLf09NTQ0MH36dPz888+IjY1Fp06d8Mcff2Dx4sX1audFVHoEOZx6wxU+Rz6IxUBKCtC27UtfYmRkhKKiIuTk5EBPTw8o6+RR5oDWkLi4uMDKykr6fezYsWjfvr10ViwUChuszm3btgFyuAcJhYWFQJkzn4S5c+fi3XffxaVLlwAAAwYMkLGenD9/Hnl5efDw8KhS3/Tp0zFnzhxcvXoVe/bswcyZM2FtbY2VK1fi/v37+Ouvv/Dtt9/K5V4q0r17dwwaNEj6fdCgQXLZTVAdhYWFMr/nvHnz8PPPP2Pv3r1Yvnw57t69y7M4cpocXOFz5MP69cCmTYCvL9Cz50tdIjG9P336VKrwzczMAACPHz+Wmozrg2Tm3r59exllIqFTp05Amcd9jx49GqTOhr6HysTHxwMVTNoAMG3aNCxfvhx79uyBUCiU7k6QcPLkSfTu3RsWFhZV6ps4cSIWLVqE3377DeHh4dixYwesrKzw2WefYevWrUhLS5PLfUiQ/J76+vrV/p7yJiMjA3l5eTK/Z48ePeDs7Iy9e/eiU6dOmDJlSr3byckBCgsBE5N6V8XhvBR8DZ8jH3x8ABsbYOxYoGyr14uwtbWFUChETEyMtGz48OEQCATYtWtXg4g1ZMgQqKqq4vfff6/2+OjRo6Grq4uNGzeioKCg2nPU1NRkjr2ozoa+h8ocPHgQrVu3lgmPa2hoiAkTJuCvv/7CnTt30K9fP+kxIsKpU6fgWUOidH19fYwdOxbbt2+X+i1YWFhg6NCh2LhxY42+DC9D5d+uujILCwv06NEDhw8fRr4SUjNL/BfefvttmfK5c+fi8ePH+Pzzz/HOO+/Uq41//wXs7YFly+pVDYdTJ/gMnyMfDAyA06eBu3eBCqbR2tDS0kKnTp0QGRmJ8ePHA2Vm3eXLl2PdunXIyMiAi4sLnj9/jmvXrkEsFiMvLw9aWlp4/vw5UMFhq7i4GEVFRSgtLUVeXp40ql27du2wYcMGLFu2DAkJCXB3d4dYLMbTp0/x5ZdfwszMDPv27cPUqVNhZ2cHDw8PmJqaIiMjA46OjpgxYwacnJxw/PhxrFy5EioqKlizZk2tdb7MPbxs1D1NTU1ER0dLI9P5+fnBz88PR48eha6ursy58+bNwx9//CH9LSWEhYUhPj4eb7zxRo3tTJs2DUeOHMH06dOlZTNnzsS5c+dkZrdEhNzcXOlvb25uLj0m+VtkZmZCJBJBKBTCyckJBw8ehLe3N1q1aoWlS5dWW7Z9+3Z4eHigV69e8PLygra2NpKTkzFhwgS8/vrr0jazsrKkvhUSvwnJ+8v+nmlpafjzzz+ho6ODyMhIrFu3DmvWrKlisn/zzTfx/vvvw97eHm3rsFRVGZEI+PxzwMUF2LDhlavhcOqMgOrr4cLhNCCzZs3Cw4cPERAQIFN+5coVBAYGQltbG+7u7sjMzMS5c+egqqoKY2NjPHv2THquo6MjEhMTkZaWBpQFkZk5c6aM09z9+/dx9uxZZGVlwdLSEm5ubjLHU1NT4evriydPnqBVq1awtbWFm5sbVFRUkJGRgX379kFVVRVubm6wt7d/qTpru4eVK1e+VOS9goICBAUFITY2FhkZGWjXrh08PT1hUoNd2MLCAuHh4TA1NZWWLV26FP7+/rh9+3aN7ZSUlGDnzp1YuHChtKywsBC7d++WKTt58iSuVUjVNmTIEAwcOFAmGBLKLA7vvfceRCIR/vjjD6SlpcHR0RGDBw+GWCyuUiYQCJCeno6TJ0/iyZMnMDExgZOTE3r37i0NvIMyR70FCxYgJiYGgYGB0rL58+e/lFIWi8W4fv06oqOjkZycDF1dXQwbNkzGnF+RyZMn46233qq302JuLvPE53AUyEGu8DmNioMHD2L69OlITU2FoaGhssVp0kRHR+Prr7/GwYMHpWVisRiWlpaYP38+Pv/8c6XK19QoLi6Gi4sLQkND5eaAyeHIkYP8qeU0KiTr3SdPnsS0adOULY5CuHbtGk6ePPnC8zw9PdHnBXlQfX19pZ73n332GT777DOZ4xcuXEBSUpJcYgI0FtLS0rB58+YXnmdnZ4eJEyfWeo6fnx9GjRoFANi8eTOmTp3KlT2nycKfXI5yIAKePAEqeYm3bt0aHh4e2LNnT4tR+GpqalXW32s670WsWbMGQUFBiIyMhJ2dXZXsgQcOHECfPn2qzVfQXFBRUXmp3/NlMuWdOnUKx44dg6qqKm7fvi0NblQbYjGwYwdgZwe8RB4oDkdhcJM+Rzls3w6sWAEcOgRUSod7/PhxjB8/Hvfv369XxDaOLAUFBTA3N8fKlSvxwQcfKFucZkleHjBoEMsrtWEDsHSpsiXicKQc5NvyOMphxgzAwwOYPBnIzJQ55OnpiY4dO1aJAsepH/v370deXl6LsZwoAx0dwMsLuHGDK3tO44PP8DnK5d49tl+/Elu2bMFHH32ER48eSQPycOpHnz59YGtri3379ilbFA6Ho3j4DJ+jZGpYS549ezZatWqF1atXK1yk5khoaCiuX7+ORYsWKVsUDoejJLjC5zRKtLS0sGbNGmzfvh03b95UtjhNni1btsDR0RHOzs7KFqVJIxIBhw+zdw6nqcEVPqfRMmPGDNjZ2eH999+vdwa0lkxaWhqOHj2Kd999V9miNGmuXmVpIaZOBWrJ0svhNFq4wuc0WoSHDmHn1q24cOGCTC5yTt3YvHkztLW1m/Xee0VgZMQUfkwM327HaZpwpz1O4+TuXaB3b6B/f/yvSxdsPXwYkZGR1WZ349RMdnY2rKys8P7771cJwsPhcFoU3GmP00jp2hUICgISErDyrbfQtm1bTJkyBSUlJcqWrNFy8OBBlJaWypRt3rwZIpEIixcvVppcHA6nccAVPqfx0qsXcOsWtNzc8PfffyM6Ohoff/yxsqVqlOTm5koz/F24cAEAkJeXh59++glLlixBq1atlC1io4aIpaw9dEjZknA48oMrfE7jRigEANjY2GDHjh346aef8NdffylbqkZHZGQkxGIx7t+/jyFDhmD8+PFYu3Yt8vPzsWTJEmWL16ghAtzcgHHjgPPnlS0NhyM/eCx9TpPhzTffxKVLlzBnzhw4ODigc+fOVc4pKCiAlpaWUuRTJteuXYOampp0yePkyZP4559/0K9fvxb5e9QFgQCYPx/YvBlwcFC2NByO/OAzfE6T4qeffkLnzp0xevRopKamyhzLzs7GgAEDEBUVBaSkAGFhSpNT0dy4cUNm62JJSQmICNevX0fnzp2xd+9epcrX2Jk2jSt7TvOHK3xOk0JTUxN+fn4AgHO2tijy8QFKSlBSUgIvLy+Eh4dj6ZIlwPTpLE5/bq6yRVYIISEhVRz2AKC0tBQpKSmYMWMGBg0a1GKDGInFypaAw1E+XOFzmhwmJibw8/PD1dJSYOdOiN56C/PmzUNgYCAAwCkgADh7lqXf/fBDZYsrdwoKChAbG1vjcSKCiooKgoODERkZqVDZlE1yMrBqFWBlBaSnK1saDke58DV8TpPE2toas/77D8MGDED7q1exPyEBRAQnAN+izBOrtJQlJh87lmXma6ZERkZCVEusV1VVVejo6ODEiRNwc3NTqGzK5o8/WCbmRYsANTVlS8PhKBc+w+c0Wezt7eG+ZAn+jI8HEUEXwJHKJwkELBVvM57ehYeHQ1W1+rG7mpoaLCwsEBYW1uKUPQAsXAg8fgz873+Avr6ypeFwlAtX+Jwmy8WLF/Htt99Kv+8AYFHZbCUWA1lZwIIFyhBRIYSHh0MgEFQpV1VVhaurK27cuAGbGrISNne0tAANDWVLweE0DrjC5zRJbt68ibFjx0Jc5o01G8BbAKq12paUAEeONNuoKqGhoVUiEAoEArzzzjvw9/eHoaGh0mSTJ0+fAitXArW4L3A4nApwhc9pciQmJmLw4MHIz8+HWCxGFwCbX3SRQADMnQskJipGSAVRXFyMu3fvSr8LBAIIBAJ8/vnn+PXXX6HWyBeu09Je7brQUOaI9+uvwIMHDS0Vh9M84Qqf0+RITU2Fm5sbVFRUoKemhr8BvNBqSwQUFQGzZ7PPzYTo6GjpdjyhUAgNDQ38/fffWLVqlbJFeyG+voCtLZCRUfdrnZyAnTuBuDhgxAh5SMfhND+4wuc0OXr16oUjR44gMTERPy9ciHRNTYgAEIBaU+uUlADnzjFN0Uy4ceMGULZeb2xsjJCQEIwbN07ZYr2Qn38GxoxhM/z9++t+vZoa8M47fH2ew6kLXOFzmixt2rTBrJ9+woC8PPx38iTWubhgj0AAiZW4qLqLiIClS4H79xUrrJwIDw8HAPTo0QPh4eFwdHRUtki1UloKLF4MvPce86cUCNjOyYoUFbHtdNevK0tKDqd5IiBqRvZNTovn2bNn+G3XLoRt3Ij+qamYKBDAmgglAFQFAgiIWEKevn1Z+t2y5DxNFWdnZ7Rt2xb79++Htra2ssWplZwcYNIkZmSpHDYgIoKFtk1MZEkSs7KA775jAwMOh9MgHOQKn9MsEYvF8Pf3x9atW3Hv1CmMFokwWVUV/cTi8jir69YBy5e/sK6CggKkpaUhLS0NKSkpSE9PR1paGtLT05GTk4O8vDxkZmYiPz8f+fn5yMrKQm5uLkpKSlBYWIiCggKZ+jIzM2Xi3qurq0NHR0fmHH19fQiFQmhra0NbWxv6+vrQ09ODtrY2dHR0YGhoCB0dHYSFhWHmzJkwMTGBsbExjIyMYGxsXOO+fGURGwuMHMnW3CttKICaGguM8+OP7PsvvwBeXkC7dkoRlcNprnCFz2n+JCUl4ddff8XOnTvhPWEC/te7N3D8OBAQgLx//8UjXV3ExcUhISEBiYmJSEhIQHx8PBITE5GUlIT8/HyZ+tTU1KSKVU9PT6qAtbS0oK2tDUNDQ2hra0NDQwNqamrQ1dWVuV5XV1fGe76goACFhYXS70SEzMxMoCzPfUFBAXJycpCdnS0dVGRmZiInJ0c68KhM69atYWZmhg4dOsDCwgIWFhZo3749LC0tYWFhASsrK4V58F++DHh6srQG1YT7BwAYGLAwuHxNnsORG1zhc5o/JSUluHfvHu7cuYMzZ85ALBbjwYMHeHTnDoTJyXhUdp6hoSEsLCxklKSFhYVUuRsbG8PU1BQGBgZKviNZRCKRVPFLLBHPnj3D06dPER8fLzOQkQwsVFVVYWVlhS5dusDGxgY2Njbo0qULunTpAisrqwaTbfdulnqWqKoZvyICAXD0KDB+fIM1zeFwZOEKn9O8yMzMREREBCIjIxEREYGIiAjcunULxcXFEAgEsLS0lFFuNjY26NixI9q3b19lJt4cSUlJQUJCAmJjY3H//n3cu3dP+soo2x9naGgIBwcHODg4wNHREY6OjujRowfU1dVfuh0ilrRm9eqXO18oBIYNA8oSIXI4nIaHK3xO00UsFiMmJgaXL19GcHAwgoOD8fDhQ6Aso55EWTk6OsLOzg42NjbQ1NRUttiNlvT0dNy9e1dmsBQdHY2CggKoqamhZ8+ecHV1hYuLC1xdXWFhYVFtPbm5wFtvsX32dUlLKxQCCQl87Z7DkRNc4XOaDmKxGNevX8eZM2cQFBSEkJAQZGdnQ19fH87OznBxcUGfPn3g6OgIc3NzZYvbLBCJRLh79y4iIiIQFhaGy5cvIyIiAqWlpWjfvj0GDBgANzc3jBw5Eh06dEBCAluvj4piClziO0hUHu+otLTm2Ecv6UfJ4XDqDlf4nMZNcnIyzpw5gzNnzsDf3x9paWmwsLCAu7s7XFxcMGDAAPTo0QPCJr69rimRl5eHq1evIigoCMHBwfjvv/+Qm5uLrl3t0arVepia2qJLFzOoqqpCT48pfVVVQE+PXa+ryzzzhcLyDHY6OoC6OmBoCHTqpNTb43CaK1zhcxofiYmJOHr0KA4fPozQ0FCoq6tj4MCBGDFiBEaOHAk7Oztli8ipQHFxMYKCgnDmzBmcPn0aUVFR0NLSwqhRozB58mR4enpW2XbI4XAUDlf4nMZBSkoKDh48iMOHDyMkJAT6+voYN24cJkyYgMGDB3OF0YRISkqCr68vDh8+jIsXL0JdXR2jR4/GlClTMGbMmDo5/3E4nAaDK3yOcrl+/Tp27NiBffv2QSAQYPDgwXjnnXcwduxYaPBN2U2ejIwMnDx5EkeOHMHp06fRunVrzJo1C/Pnz0fHjh2VLR6H05LgCp+jeIqKivDbb7/hl19+QXR0NPr27YsFCxbgzTffhJaWlrLF48iJJ0+eYMeOHdi1axeSk5Ph4eGBJUuWYOjQocoWjcNpCRzkyXM4CqO4uBi//PILOnfujGXLlqFv3764evUqwsLCMGvWLK7smznm5ub48ssv8fjxYxw8eBB5eXkYNmwYBg4ciAsXLihbPA6n2cMVPkfuiMVi7Ny5E126dMGyZcvg5eWFBw8e4Ndff0WfPn2ULR5HwaipqWHixIk4f/48goODoaWlhSFDhsDd3R2hoaHKFo/DabZwhc+RK7dv34abmxsWLVoET09PPHjwABs3boSZmZmyReM0Avr37w9/f3/8999/UFFRgaurKxYvXozs7Gxli8bhNDu4wufIhdLSUqxevRq9evVCUVERrl69ii1bttQYnY3TshkwYAAuXryIPXv24NChQ+jRowdOnTqlbLE4nGYFV/icBiczMxMeHh5Yt24d1q5di9DQUDg4OChbLE4TYNq0abh9+zYGDRqEMWPGYM2aNeB+xRxOw9C4kmZzmjyxsbEYM2YMsrKycOnSJfTt21fZInGaGMbGxti3bx/c3d2xcOFCxMTE4Pfff+dOnRxOPeEzfE6Dcf/+fbi6ukJHRwdXr17lyp5TL+bOnQs/Pz+cPXsWXl5eKC4uVrZIHE6Thu/D5zQIWVlZcHJygpGREc6fP6/QVLPx8fHYvXu3TJm+vj6WLVsGANi9ezfi4+Olx958801069ZN5vx79+7h0aNHGDFihFxkLC4uxnfffYfS0lJoamrik08+AQBERUUhMDAQCxcuhIoKH39XR3h4OF5//XVMmDChyt+Zw+G8NAdBHE4D8Pbbb1O7du0oOTlZ4W2LxWJ69OgRjR8/ngDQzJkzKTMzU3o8NzeXlixZQoMHD6b79++TSCSSHhOJRPTDDz+QlpYWLV26VK5yFhcX07Rp08jAwEBaNmbMGAJAYWFhcm27qXPy5EkSCAS0f/9+ZYvC4TRVDvApBafeBAYGYv/+/di5cydMTU0V3r5AIICVlRW2bt2K1q1b4+DBg0hJSZEej4+Px7Fjx7B371507txZOpN+8OAB3N3dceTIERQUFMhdTjU1tSo5AdauXYutW7fCyclJ7u3n5+c3Wc/30aNHY/78+fjwww+Rl5enbHE4nCYJV/icerNhwwa8/vrrGD16tFLlMDU1xQ8//IDCwkJ4e3uDiFBcXIy3334bGzduhLm5ucz5aWlp2Ldvn0KjvAkEApnvdnZ28PHxUYg5f+fOnfj777/l3o68WL16NZ4/f44///xT2aJwOE0S7qXPqRd5eXk4ffo0fvvtN2WLAgCYMWMG9u/fD39/f/z666+4ffs2+vXrBy8vryrnOjs7AwAKCwvr1Mbt27dx+vRpzJkzB/qShO41kJiYCF9fX6Snp6NNmzZITEyUHjtz5gxCQkIAAAsXLoSpqSk2b96MtLQ02NraYsqUKbh58yaCgoIwf/58oMzX4MyZMxCJRHBycsLAgQNl2svIyMCpU6eQkJAAdXV1mJubw93dHWFhYVi/fj1MTU2xatUq9O7dG2PHjgXKYtz7+fkhJSUFJiYmGDVqlDRewovkUSQmJiYYN24cjh49Cm9vb4W3z+E0dfgMn1MvIiIiUFJSAjc3N2WLImX79u3Q0dHB+++/Dz8/P/z4448NWv+KFSuwbNky7N27t9bzDhw4gM6dOyM6Oho9evSAltb/27v/mKrqP47jTxC5cAGBASI/i99CorchG0ILkgIVknKjudkPFgOz4R/ZgLlmy+zHmP3Y+jWHjhLmyi0syB/BINIBsxIzWARcFyER8vv3vQIXzvePb9xvt7Tvty/IEX0/trPBOeeez+sy7t7n3PP5nI89IyMj5u3Jycl4eHiwf/9+8y2IrKwsTp06xcGDB0lPTycpKYmXXnoJgMLCQnQ6HZOTk3h7e/PEE0+wa9cu8/HOnDlDQEAA9fX1REZG4unpydtvv015eTl2dnaMjY2xcuVKYmJiCAoKMmdcvXo1v/32G5GRkbS2thIcHGy+iv67PGq4//77+e6771RrX4glTe1eBGJp++yzzxRAmZqaUjuKhYMHDyqAkpaW9l/3NRqNCvA/d9prbm5W3nzzTYuOgX/W29ur2NvbKxkZGRbrd+7cadFpr6SkRAGUpqYm87q4uDglPDxcuXr1qqIoipKXl6f09PQoGo1Gyc3N/ctrL168qAwNDSnOzs7K448/btHe559/rhw+fFhRFEVxc3NTMjMzzdv6+voUrVar7Nu3z+I1u3fvVuzt7ZXe3t4b5lHL3P/b5OSkahmEWKKk056Yn7nhd+Pj42pHsVBbW4urqytlZWWUlpYu6LHDw8PZs2cPzs7ON9ynvLwco9HI9u3b/682VqxYgaenJwAFBQVUVlYyOTlJYmKieZ97770XgPPnz3Py5ElGRkb+0l5ycjJpaWnXbePUqVMYDIa/TE+7detWjEYjp0+fvmEetYyPj6PRaLC1tVUtgxBLldzDF/MSHh4Ov4+V/mMxUtOhQ4cwGAx89dVXREdHk5OTw8aNG3F1dV20DJcvXwbA399/QY7X2dkJQGlpqfm+/9wEM11dXdjY/Puj7OfnZ/E6Ozs7IiB3hAAACHVJREFU7OzsrnvM9vZ2+L2z4x/NdW6c234raWhoICIiQu0YQixJcoUv5sXHx4fIyEiOHz+udhT4vUPd66+/ztGjR9HpdOTl5XH16lWef/75Rc0xMzMDYC7ECyU2NpaEhAQSEhLYunUrNTU1PP300+bty5YtW7C2/jyiQG0mk4lPP/2UzZs3qx1FiCVJCr6Yt2effZaSkhJ+/vlnVXPMDcF799138fLyAuDFF18kLCyMDz/8kOrq6kXLMjf97y+//LIgx5u7cvf39zcX/LklMDDQ3Amvra3tfz5mYGAgAD09PRbru7q6AAgICFiQ7AulqKiInp4esrKy1I4ixJIkBV/MW2ZmJoGBgWRnZzM7O6tajvz8fGJiYszDzQA0Gg1HjhzBysqKrKwsDAbDvNtpbW3lrbfesuhx/2dJSUlYWVlx5MiRebcHkJiYiI2NDR999NF1t6ekpODo6Mg777xzw4cILV++3GJbSkoKWq2Wqqoqi/1OnjyJVqtly5YtC5J9IVy5coW9e/eSk5PD3XffrXYcIZYkuYcv5m358uUUFxcTFxdHfn4+Bw8eXNT2R0ZGKC8vp7i4mLq6OhRFsfg6evXq1SQlJVFRUcFzzz3Hvn378PX1xWQy0dvbS0dHBwDd3d20tLTg7e39t+Pr8/PzKSsrw9bWlpycnOvuExERQV5eHgUFBQwODhIbG8vQ0BAXLlxgdnaWiYkJ7O3tGRoaAmBgYAB+/5ZicnISk8nExMSE+cl8Xl5evPHGG+zZs4fOzk7i4+OZnZ2lu7ub/fv34+3tTUlJCTt27GDNmjVs2bKFlStXMjg4iE6n46mnniIqKoqysjJeeOEFrK2tOXDgAIcPHyY7OxuNRkNUVBRnz56lsLCQoqIi3N3db5hnMY2NjbFt2za8vLx45ZVXFr19IW4XMnmOWDDHjh3jySefZO/evRw4cOCWuwcslp7BwUEeffRR2traqK2tNd+6EEL8Y5/IFb5YMDt27GB6epqdO3ei1+tlDnMxL3q9ntTUVK5du0ZVVZUUeyHmSe7hiwWVkZFBRUUF1dXVxMfHo9fr1Y4klqDy8nJiYmJwdXXlm2++4Z577lE7khBLnhR8seASEhI4f/48JpOJtWvX8tprrzE9Pa12LLEEdHd3k56eTlpaGmlpadTU1LBq1Sq1YwlxW5CCL26K4OBgvv32W15++WVeffVV1q9fv6iz0omlZWpqivfee4+IiAguXrxIZWUlRUVFcktIiAUkBV/cNDY2NuTm5tLY2IiPjw+JiYkkJCRw7tw5taOJW8T09DSFhYWEhISQm5tLdnY2TU1NPPTQQ2pHE+K2IwVf3HRBQUGcPn2a2tpali1bRnx8PImJiZw5c0bVcftCPWNjY3zwwQeEhoaye/duUlNTuXz5MgUFBWi1WrXjCXFbkoIvFk1cXBzV1dWcPXsWa2trUlJSCAkJoaCggL6+PrXjiUXQ2NjIrl278PHxITc3l02bNqHX63n//ffNz/AXQtwcMg5fqKalpYVDhw5x9OhRjEYjjzzyCNu3b2fTpk03nPBFLD09PT2UlpZy7Ngx6uvrCQsL45lnniEjIwMXFxe14wlxp/hECr5QncFg4OOPP6a4uJja2locHR1JS0vjscceIykpSaZCXYIGBgY4ceIEx48f5+uvv8be3p6HH36YzMxMNm7cKA9lEmLxScEXt5b+/n5OnDhBcXEx9fX1aLVaNmzYQGpqKmlpafIc9VvU7Ows33//PVVVVVRVVXHu3Dmsra158MEHSU9PZ9u2bTg6OqodU4g7mRR8cevq7Ozkiy++4Msvv6Smpobx8XHCwsJITk7mgQceYMOGDXh6eqod846kKAotLS3U19ebi3x/fz++vr4kJyeTnJzM5s2bpcgLceuQgi+WhqmpKerq6qioqKCyspLGxkZmZmYIDg4mLi6O2NhY4uLiCA8Px9pa+qIuNKPRyIULF6irq6O+vp76+noGBgZwcHAgNjbWXOTXrFmjdlQhxPVJwRdL0/j4OJcuXaKuro7a2lpqa2sZHh7G1taW4OBgoqKizItOp5MrzX9gaGiIH3/8kYaGBhoaGmhubqapqYmpqSlWrVrF+vXrue+++4iLiyM6OhqNRqN2ZCHEfycFX9weTCYTTU1NNDQ08MMPP5iX0dFRrK2tCQwMJDQ0lLCwMEJDQwkJCSE0NBQ/Pz+1o6tiamqK9vZ2Wlpa0Ov1tLW1odfr+emnn+jp6QHA19eXdevWodPpWLduHdHR0dKHQoilSwq+uH0pikJ7ezuXLl2iubmZ1tZW2traaGtrY3h4GACtVktAQAD+/v74+Pjg6+vLXXfdZf7Z19cXJycntd/KP6IoCn19fXR1dfHrr79y5coV888dHR3mdSaTCQA/Pz/zCVBoaChr165Fp9Ph5uam9lsRQiwcKfjiztTX12c+Aejo6KCjo8OiQBoMBvO+Go0GNzc33N3d8fDwwMPDA3d3d9zd3XF0dMTJyYkVK1Zgb2+Pg4MDLi4uaLVa87MEXF1dLdp2cnLCxuY/M1MbjUauXbtm/n16eprx8XEARkdHMRqNTExMMDw8jMFgwGg0Mjw8zNjYGL29vfT39/9l+ePH2t3dHR8fH/z8/PD398fX15egoCDzNx0ODg439W8thLglSMEX4noGBgbo6uqiq6uL/v5+BgYG6O/vp6+vj76+PvO68fFxxsbGGB0dZWZm5qbnsrOzQ6vV4uLigpOTk8UJyNxJibu7O56ennh5eeHv7y8T0AghkIIvxAKanJzEYDAwNDSEwWBgcnISk8nE2NiYxX7Dw8MWV+C2trYWV9lWVlbmJ9A5Ojqi1WpxdHTE2dlZRiAIIf5fUvCFEEKIO8AncrkghBBC3AGk4AshhBB3ACn4QgghxB3gX8bDpOoL9BT6AAAAAElFTkSuQmCC", "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "display(unification_to_agraph([t1, t2], ftax))" ] }, { "cell_type": "markdown", "id": "a6414b39-a87c-435d-a94f-99e9b74bfbcf", "metadata": {}, "source": [ "Checking OSF term subsumption, and computing the subsumption degree" ] }, { "cell_type": "code", "execution_count": 16, "id": "5825ac7d-e2aa-40fc-bc61-8738c08cf479", "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "X0 : slasher(directed_by -> X1 : director(spouse -> X4 : person))\n" ] } ], "source": [ "from fosf.syntax import NormalTerm\n", "t1 = parse_term(\"thriller(directed_by -> person)\", create_using=NormalTerm)\n", "t2 = parse_term(\"slasher(directed_by -> director(spouse -> person))\", create_using=NormalTerm)\n", "unif, deg = unify_terms([t1, t2], ftax, return_degree=True)\n", "print(unif)" ] }, { "cell_type": "markdown", "id": "ec880fbb-a778-4549-9c0c-2b0f579fcc21", "metadata": {}, "source": [ "The unifier is equivalent to `t2`, i.e., `t2` is subsumed by `t1`, with degree `deg`." ] }, { "cell_type": "code", "execution_count": 17, "id": "0db50580-c338-4b56-8213-8659e89c40c1", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "(True, 0.5)" ] }, "execution_count": 17, "metadata": {}, "output_type": "execute_result" } ], "source": [ "unif.equivalent_to(t2), deg" ] }, { "attachments": {}, "cell_type": "markdown", "id": "1c856bd9-207d-4885-8449-18b8172327d8", "metadata": {}, "source": [ "## Figure 5\n", "\n", "Parsing an OSF theory and ensuring its order-consistency." ] }, { "cell_type": "code", "execution_count": 18, "id": "88fd9c08-fbe2-4e6a-980c-b71679bcd139", "metadata": { "tags": [] }, "outputs": [], "source": [ "from fosf.parsers import parse_theory\n", "from fosf.reasoning import normalize_term\n", "theory_str = ftax_str + \"\"\"\n", "person := Yperson:person(spouse->Y0:person(spouse->Yperson),\n", " fav_movie->Y1:thriller).\n", "movie := Ymovie:movie(directed_by->Y2:director).\n", "\"\"\"\n", "theory = parse_theory(theory_str, ensure_closed=True)" ] }, { "cell_type": "markdown", "id": "9e159f22-46df-43c8-9862-c1ae59332c0f", "metadata": {}, "source": [ "Although `slasher` is not explicitly defined, it inherits the constraints from `movie`:" ] }, { "cell_type": "code", "execution_count": 19, "id": "a5b02191-6ddf-47a3-a812-cd890d15bbcf", "metadata": { "tags": [] }, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "Yslasher : slasher(directed_by -> Y7 : director)\n" ] } ], "source": [ "print(theory['slasher'])" ] }, { "cell_type": "markdown", "id": "df0b4b2b-03b2-4e5c-b0f5-a8b69c92581c", "metadata": {}, "source": [ "Parsing an OSF term and normalizing it according to the theory:" ] }, { "cell_type": "code", "execution_count": 20, "id": "eafc0257-994a-43bf-ae99-aca320c3d3df", "metadata": { "tags": [] }, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "X0 : director(spouse -> X1 : person(fav_movie -> X2 : slasher(directed_by -> X0), spouse -> X0))\n" ] } ], "source": [ "t_str = \"X0:person(spouse->X1(fav_movie->slasher(directed_by->X0)))\"\n", "t = parse_term(t_str)\n", "nt, d = normalize_term(t, ftax, theory, return_degree=True)\n", "print(nt)" ] }, { "cell_type": "code", "execution_count": 21, "id": "82dc8d8d-2ebf-4e23-a27a-172ef0160d11", "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "X0 : director(\n", " spouse -> X1 : person(\n", " fav_movie -> X2 : slasher(\n", " directed_by -> X0\n", " )\n", " spouse -> X0\n", " )\n", ")\n", "\n" ] } ], "source": [ "nt.pretty_print()" ] }, { "cell_type": "markdown", "id": "b7ca278f-1b29-4dc3-858f-1267bc07d680", "metadata": {}, "source": [ "The satisfaction degree of `nt` with respect to the OSF theory:" ] }, { "cell_type": "code", "execution_count": 22, "id": "3d91fefd-bbed-435a-bd98-8cf86da6b24b", "metadata": { "tags": [] }, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "0.5\n" ] } ], "source": [ "print(d)" ] }, { "cell_type": "markdown", "id": "4ad8117f-030d-4eff-8fb3-a396f73d5dcc", "metadata": {}, "source": [ "Additional theory normalization example in the body of the paper:" ] }, { "cell_type": "code", "execution_count": 23, "id": "676a1c3d-70a8-4e89-8ded-81a92cf3473c", "metadata": { "tags": [] }, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "X : s0(\n", " f0 -> X0 : top(\n", " f1 -> X1 : top\n", " )\n", ")\n", "\n" ] } ], "source": [ "theory_str = \"\"\"\n", "bot < s0, s1.\n", "s0, s1 < top.\n", "s0 := Ys0:s0(f0 -> Y0:s0, f1 -> Y1:s1).\n", "s1 := Ys1:s1.\n", "\"\"\"\n", "theory = parse_theory(theory_str)\n", "t_str = \"X:s0(f0 -> X0:top(f1 -> X1:top))\"\n", "t = parse_term(t_str)\n", "t.pretty_print()" ] }, { "cell_type": "markdown", "id": "a4c1b06d-32f1-4385-b764-c1c4627990c7", "metadata": {}, "source": [ "According to the theory, `X0` must be of sort `s0`, and `X1` of sort `s1`." ] }, { "cell_type": "code", "execution_count": 24, "id": "2b2ca7da-23c4-41d7-b0f4-85ff92c84ebe", "metadata": { "tags": [] }, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "X : s0(\n", " f0 -> X0 : s0(\n", " f1 -> X1 : s1\n", " )\n", ")\n", "\n" ] } ], "source": [ "nt = normalize_term(t, theory.taxonomy, theory)\n", "nt.pretty_print()" ] } ], "metadata": { "kernelspec": { "display_name": "fosf", "language": "python", "name": "fosf" }, "language_info": { "codemirror_mode": { "name": "ipython", "version": 3 }, "file_extension": ".py", "mimetype": "text/x-python", "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", "version": "3.14.6" } }, "nbformat": 4, "nbformat_minor": 5 }