{
"cells": [
{
"cell_type": "markdown",
"id": "95a492d4",
"metadata": {},
"source": [
"# Quick Start"
]
},
{
"cell_type": "markdown",
"id": "80685d54",
"metadata": {},
"source": [
"In this page, we give a quick illustration about how to build a simple model."
]
},
{
"cell_type": "markdown",
"id": "f898fcd6",
"metadata": {},
"source": [
"The first thing to do is to import the library PyCSP$^3$:"
]
},
{
"cell_type": "code",
"execution_count": 1,
"id": "1500590b",
"metadata": {},
"outputs": [],
"source": [
"from pycsp3 import *"
]
},
{
"cell_type": "markdown",
"id": "ca4d6513",
"metadata": {},
"source": [
"If you have a problem, this is certainly because you need the Python package pycsp3 to be installed on your system. You need to execute something like ```pip install pycsp3```. See the [Installation Page](http://pycsp.org/documentation/installation)."
]
},
{
"attachments": {
"graph4.png": {
"image/png": "iVBORw0KGgoAAAANSUhEUgAABfcAAAGVEAQAAACpCd88AAAABGdBTUEAAYagMeiWXwAAAAJiS0dE//8UqzHNAAAACXBIWXMAAAEsAAABLABziOlSAAAAB3RJTUUH5gsECjAbrM+OsAAAPU5JREFUeNrt3X1wnXdhJ/rvAefW7Ewci5tOjBfyoiQXb7tNTGU2vkl26wQ50NllKwxOKFw6k5pYQHZwmQTkOjvF7GyCBfFQM2uK5Hqzc5mFErHBtLudNtZCaEOuU6zWSZde97pRYsPm5da3iu3dbdiYPvePRyeS5TfZlh6dR+fzmdHoHL34POfROb95/H1+z/fXKIoAAAAAAAA18jq7AAAAAAAA6kW4DwAAAAAANSPcBwAAAACAmhHuAwAAAABAzQj3AQAAAACgZoT7AAAAAABQM8J9AAAAAACoGeE+AAAAAADUjHAfAAAAAABqRrgPAAAAAAA1I9wHAAAAAICaEe4DAAAAAEDNCPcBAAAAAKBmhPsAAAAAAFAzwn0AAAAAAKgZ4T4AAAAAANSMcB8AAAAAAGpGuA8AAAAAADUj3AcAAAAAgJoR7gMAAAAAQM0I9wEAAAAAoGaE+wAAAAAAUDPCfQAAAAAAqBnhPgAAAAAA1IxwHwAAAAAAaka4DwAAAAAANSPcBwAAAACAmhHuAwAAAABAzQj3AQAAAACgZoT7AAAAAABQM8J9AAAAAACoGeE+AAAAAADUjHAfAAAAAABqRrgPAAAAAAA1I9wHAAAAAICaEe4DAAAAAEDNCPcBAAAAAKBmhPsAAAAAAFAzwn0AAAAAAKgZ4T4AAAAAANSMcB8AAAAAAGpGuA8AAAAAADUj3AcAAAAAgJoR7gMAAAAAQM0I9wEAAAAAoGaE+wAAAAAAUDML7AIAgGo1Gp2dydSPjo5T//TISPl5eDgZGyuK5n2AmR6bOjqSrq5yPGp+7uw889g0MlKOTcPD9iAAQMXHb0VhJwAAzPpBV2Pt2qSrKzffcUcev/LKC/vXhobKsH9oqCjGxuxd4PzHpq6upLs7GR+jLsjISDk+DQ0VxeiovQsAMMvHcsJ9AIBZOMhqdHSUgVl3d9b98i9n58UXN7+3YEny9/5jctXHy/s9P0n+/oeSu+6e+P1HlyZPXJ48vTYZfSR58aeSI/978soDUx6o77HH0v8HfyBMA6Y/Pk0emy6//LWvb0gu/tDE2HTDI8mbfinZvGfidw8cTP79HckL30qeXJMc+5Pk8J7k2FeSYtukB1l36FB2fu1r5djkiiMAgFk5rhPuAwDM4MFVo6Mj6esrPyYs3JTcsDX54NYTQ/xzdeBg0veN5In/lLz0nanfHR5O+vvVYwCnHp/6+nLpxo05vHhx82sLliQ/21kG+QOXXdi/3/tSMvzm5Nm7pwT9Nz/3XB7/7GeLYnDQXwEAYAaP74T7AAAzcFDVDPXXfexjzVn6l92SLHsi2fTG5LbnZ+dxTx2mDQ0lGzeayQ+U49P69Vl3333NWfoLNyVvfSy5+wMXdrLxTHZsT7Z/NfnBaHL8xfEv9uzbl12f/KQTkAAAM3ScJ9wHALjAA6rG+vXp+fzns2vRoiRZtDcZevfsBfqncuBgsvYDydNvnxzyDw6WIb9efmjPsam7O3333Zf+VauScpb+fVecWLNThTVbk997cFLI3/fYY+m//34hPwDABR7vCfcBAM7zQKrR3Z2bd+xoLpC7aG/yiburD84mO3Awedc1yejx8S8sO3Ik+7/85aLYuNFfDNplbOroSB5+uFz3owz1331v8sg9c7tdy29yAhIAYEaP+4T7AADncRDVWL8+GRhIyuDsV/ddeF/1THp0afIryyb38g8NJb29QjSY72NTV1cuHR7O4cWLGxuS676fDH01ufaK1ti+k64y6tm3L7s+/GGL7gIAnMexn3AfAOAcD6AaAwPJ+vVJcv2Nyb7vte62bl6Z/KuVk0O0975XFz/M17Fp/fqse/DB7Lz44oWbkqfXt06oP9WjS5NfujN55YEkPUePlgH/0JC/IgDAORz/CfcBAKZ54NTo6EjfI480+6vf8+Dc11xMx47tycefnxyi3XqrWbIw38anLVuSvr4k6VyQPPNq62/zSTVi2bixKPr7/TUBAKZ5DCjcBwCYxkFTo6srPb/929m1fHljQzJwbXLX3fXZ/gMHkxWHk6Mrml/p7S2KwUF/Waj72NTRUVaErV2b1Oek42TLb0qeeqJ5b3CwKHp7/WUBAKZxLCjcBwA4ywHTpA7rVq+6OJsTQzQBP9R/fNq7N+nqamxIfmPP3C7ofSHWbE12/bC52O7QUFHcfru/LgDAmb3OLgAAOL1Go6MjPb/92zm8ePFlt9Q72E/K9QHe82Dz3sBAo9Hd7a8MdR2fBgaawf7AtfUN9pPyaoOBa5PGhiRZu7asGQIA4IzHg2buAwCc4WDp333zm7mzp6fuM/anem0Gf8/Ro9n1trdZZBdqNjY1+vqSLVvqWBN2JptXJp95snnP1UUAAGc8JhTuAwCc5kBpfIHKxobkDx5Obnt+fj2/JbcmL30nSc++feUiu2Nj/upQh7GpuzvZvTupZ8f+2axamHz3x0nWHTuWnbfcYgFwAIDTHBcK9wEATnGQ1Fi/vlykMvn0DfWuuzidAweT6waTVx5IdFxDXcamrq70fPvb2bVo0fU3llVb89HVFyWjx5Nc+vLLOdzZ6eQjAMDJdO4DAEzRaHR1NYP99zw4P4P9pKwY+uJSHddQn7FpfA2QXYsWXXbL/A32k+SZV5OFm5IcXry4eZUCAABTjg/N3AcAmHKA1Ni9O+nu7lxQBkzz3Ykd11dfrX8fWnVsKqvC5tsaIKdz4GDyMyuT4y8m+vcBAE5m5j4AwCRll3V3d2ND8gd/1R7PefOepHNB815fn1cBtOLY1NGRno9+NEn6/vP8D/aT8jm++97xO+vuu8+rAABgyjGimfsAAJMOjj588GB2Xn75L/xU8tgr7fO8H12avPOF5r0VKyxgCS02No3P2l+0NznS1V7P/Q33NdcG6e8vio0bvRoAAEpm7gMAjGs01q/PzssvX7CkvYL9JLnt+eT6G5v3dO9Da41NnZ3Nq2oe3NN+z7/vP4/fWPexjzUaHR1eEQAAJeE+AEDTeO3DazUQbWboq83Fdbu7y3oioDWUwX7nguSuu9vv2W/ekyzam2TnxRerDgMAmCDcBwDIeOXFzssvX7gpeeSe9twH116RXPf95j0BGrTG2NTVlaxfnyS/9dPtux8mrljo6yuvZAAAQLgPAJAkN99xRzKp/qFCBw4mvS8ly2+a+Ni8cm52w9BXkwVLknL2fleXFwbMtbVrk7I267bn53ZLDhwsx6cDB6t/7Lvunrzwd7lPAADanXAfAGh7jUZnZx6/8soFS8r6h6o0g7K3fiH5nR8li0eSGx4pv3f/weSiN5Whf5WuvSL52dfmxArQYM6t++VfTpK7PzC3m7F5ZfIzK5Onnkj+/R1zsw3dPxq/0fP+93thAAAI9wEA0gyxLz9c3SMeOJhcN1gGZT1vSY50lYv4DlyW7Pte8hd7yu0ZXJJcfVG1e6PnJ80b73yn1wbMnUajq6u5yPdcdO3v2J6s2ZpcMpJ85snk+Itzuz8GLhtfF2TX8uWqeQAAhPsAAMlDH/xgMmlWaAVWHE5eeaCs2jhVx/+1VyTPvJos3JSMHk9WLaxu2zbvEaBBayhPPP5she/CzSuTRqP8WP8vkt97MLnq462zR67a3rxl0W8AAOE+ANDWGo3Oztz5cz/X2FDOCq3CqoXJ0RVlgD701TP/7K+Mh2p/9JHk0aXV7ZeJAE01D8yZ8atnXruapgIf/Hry6RvKjz98U/LqC+XVRK3i+i3NW8J9AIBGUdgJAEAbHww11q9PBgY6F5Qz5atw0ZvKeovpPmajUX6ucht7XyorgZLh4aJYvdorBaoemzo7k2eeaWxI/u43W2F7Jm5/+oZq1yeZ7MDB5H+7snnvjW8sirExrxYAoF2ZuQ8AtLly9ufEbNDZ1fvSRG/1W14/vd9ZtLf8/GyFndsTVzF0dzcaHR1eJ1C18qqZiatoSMrKsstuOXH8BgBoV8J9AKC9XVrOSu9/XzUPN/zmidurlk9zE1eWn4ttZR92VZonFZKuLi8UqFq53kWVa4HUxZIfG5sAABLhPgDQ7g4vXtzYUM4GrcKhS8/9dy7+RxO3d72+ul0zsYimRXWheuX77k2/ZE9MNbEGgbEJAGhvwn0AoG01GuWsz4s/VN1jNit5kuTGQ+f++89+cS72lAANKnfpihXJ3HXbt7K//9qYrTIMAGhvwn0AoI2VwdAbPlnNo02t1Lnt+XP/N/7nI9XtHbNjYQ4dXrzYTji1u15bf0TnPgDQ3oT7AEAbK4Ohif7m1vfKA9U9ltmxMDeaVxVNrHvBSftog30AALDALgAA2l3nGvvgVO66O1n/L5JkxYpGwwxZqM7b3paMX1X0bXvjVC7+UHJ0W9JodHcXxfCwPQIAtCPhPgDQ9q4bSnLP7D/O02uTPFnHPbR4cbJ7t1cKVKtOVxUBAFA9tTwAABUZfcQ+AAAAYGYI9wEAAAAAoGbU8gAAbe+xfdU8Ts9PkqdquYdefjlZu9YrBarytrcln/vcs1+0JwAAOD3hPgDQxsbGkuTlLnviVDavbN7au9eClVCdRqMcmzi9Y18pPxubAIB2ppYHAGhjIyNJ8uJP1WeLGxuqe6wXvtW8NTrqtQLVKYpybDq6wr447T7almTZkSP2BADQzoT7AEAbK2fH/u3nq3m0Gw+deH9iZvz0Xfyh6vbOk2tO3E9AhW5+7rkkOXDQrpjqtbFz//e/b28AAO1MuA8AtK2qZ8fe9vyF/xuXrpyLPWXmPlTu8b/6qyT593fYFcYmAIBTE+4DAG2uDIeqmh27aO+5/87k2qDrt1S3ZyYW8xSgQfXKk49PW8r6JLte37zlqiIAoL0J9wGANlcGaH3fqObR3nbTxO3H9k3vdybXBn1kazXbeeDg5Csayn0EVKk8qfbEf7InpvrLVcYmAIBEuA8AtL3h4aS6AG3TGydu//An0/udZsi+aO/MVPtMx8TJjqGhojA7Fqo3NJQk/+919sRkBw4mrzyQpOfo0aIo9xEAQLsS7gMAba4Mh176TjXVPLc9n3QuKG8fuvTsP9/70sTt97+5ur0ycbKjPPkBVKsoxsbSs29fse3EcaDdvXbicdcf/qG9AQC0O+E+ANDWimJsLA/t2pUkDy6s5jF/66eTxobk+IvJmrPU7PzOj8rPi/YmA5dVt18mZgubGQtzZtfv/E6SDL/Zrmhy4hEAYIJwHwDgzj17kuoCtNueT35jT3l71w+THdtP/XNrtpaVPAs3JXsvrW539L6UFNuS9Ozbp5IH5lJ5cu3Zu6t91M0rJz5WLUyW3Hri9/vfUX598s9VceXTgYPlVVaT9w0AQDtrFIWdAAC0+QFRo7MzeeaZxobk736zusfdsT352L9OfnJH8k++nOz4y+TaK8qvb/m1ZPR4OWN/76Xl16ty9UXlYycbNxZFf79XCMzh+PSPn302j1955eC/Se6qKORvNE799UV7k2NfGT/5N8Wnb0g275nd7ep9KRlckpRrgdx+u1cHANDuzNwHANpeUYyOJiMjxbaz1+TMpLvuTl59Iel5S7L/xuS6wTJUu3dl+f1P35Ac6ao22D9wcPIsYTNjYc49/vWvJ+UJv+rGxFN/HOkqT4Ce6nuzHewnEzVlyciIFwYAgJn7AADlQVFj/fpkYGDBkjJwb1fLb0qeeiJJhoeLYvVqrwyY67GpvLIoSaqcvd9qNq9MPvNkkmVHjmT/VVepDAMAMHMfACBJUhSDg7n5ueeOv1h2SbejR5c2g/0k2bjRqwJaYWwaHU3KeqzmVT3tqP8d4zf2f/nLgn0AgJJwHwCg6fG77kqSP/pINYtDtpqP/nXz1uBgUai9gNbR3591x44dXVHOYG83a7YmrzyQZN2hQ0XhxCMAQJNwHwBgXFEMD6fvsceKbcnaD7TXc9+xvbmIbtKcJQy0ytg0NpadX/pSknxhe/s9/997cPzGzvvv92oAAJgg3AcAmKy/DI+efntZU9MuJuo++vvLGhCgxQan/qw7dOjoimoX/p5ry29Kjr+YpGffvqIYHPQ6AACYINwHAJikKIaHk8HBYlvyK8va4zmv2ZocXZFyoUqz9qFFx6axsebM9V0/bI/qsB3byxOtSZJdn/ykVwEAwImE+wAAJ+nvz7IjR176TjlrdD7bsT355r3jd/Z/6lMWqoTWVc5cHxkptiXXDc7vgP/AweTjzyfFtqRcB2R42CsAAOBEwn0AgCmKYnQ0+9/3viR56on5W4Hx6NKk90Dz3r59iToeaH1//MdZ9vzzrzyQvOua+fssVxweX0S3Z9++xCK6AACnItwHADiFcpZob29SzmzfMc8WsTxwMPmlO8dnxS47dChZvjzZvbvR6Ovz14fW02h0dDQau3cnv/Zr2X/kSNYdOzZ6PFm1cP4916svGq8K6zl6NLve+15XFAEAnJpwHwDgNMoKjHIBx94D86sC413XjM+KXfbcc9l/+eUT39mypdEYGGg0Ojq8AqA1NBpdXcnevUl3d/mVf/APsvO//Jck+e6Pk96X5s9zXbM1GT0+fmfXrbda4BsA4PSE+wAAZ1AUvb3J8PB86ri++qLx8Kzn6NHs37AhGRk58SfWry9n8Xd2egXA3Go0yvdjMvX9+Ed/1FwAe8dnk80r6/9ce1+atAZIenuLYurYBADAZMJ9AICzuv329Ozb98oDyVu/UN+KngMHkyW3Tp4V++EPF8Xv/m6yenXzCoUJ5UzhRqM5UxioWqOxZUsyMJBMvpJmbKwMvjduLIqNG5PBwWJb8pkn670+yPKbksElzXv9/eWVUwAAnPF4sSjsBACAsx40NTo6ytmzXV2NDUnPW5JH7qnP9u/Ynnz8+eYClc0e6+HhE59jX1+yZcvJv71xY1GUM4SBqsabhx+eqOFpGh1Nbr996oz28iRAuV5G54LkmVfr81wPHCxrwl476Wi8AQCY/nGjcB8A4BwOnhoDA2VtTXL9jcm+77X+Nm9emfyrleOL5/bs21cG+6fusS5n6j/88IkzhZNyZv/GjRa2hNkeY7q6yvfg1Bqe4eEy2D/1e7Cs7xkYSJJFe5O9lybXXtHaz/XAwbLubOKk44c/XBRDQ14FAADTPHYU7gMAnOMB1KQQ7bJbkj9+qHVDtFULywU3S0NDZZ3HmQP6smv/4YfLap7JRkbKcNEClzB7Y8uWLSefXOvvLyt4zvb7XV3p+fa3s2vRooWbki8uTe66uzWf6wknHW9+7rk8/r736dgHADjH40fhPgDAeRxENbq7s+wb38j+Sy5pbEiu+34y9NXWCfk3r0zuP5gcf7H5lemFgxPPr6OjDBnLqxQmjI2VAf+JlT7AhY4pE9U6J77fNm48l/75RqOzMz3/4T9k1/LlSVnT81s/ndz2fGs8z0eXJr+yLHnpO82vnPmKBAAAznDsJ9wHADjPA6lGZ2c5g7/sxV6wJHn3vXPbxb95ZfKF7cnRFeNfuPm55/L4pz51vlUXevhhtseRc+vXn/6/2dc3+WTB9TfO7QnIR5cmH/3rSd36PUePZtdv/da5nHQEAGDKcZ9wHwDgAg+oGt3d6bvvvvSvWpWUIf+v7ksGLqtuG04dnD3wwEwE8Hr4YbbGjvPr15/+v9/ZWQb85RU4zauMqlwr5MDBZO0HkqffPl7BY+wAAJi540nhPgDADB1YNdavz82//ut5/MorkzLk/9nO5IZHZifof3Rp8sDfJE/eM74gZZKsO3YsO7/0pbKGZ+aCMz38MAvjxQX065/bY3V1lY9VXh3Q2JBctT25fkvS/76Zn81/4GDS943kif80uX4nKUP9/n7jBQDADB3nCfcBAGb4AGtKyJ9MhGndP0rufeX8w7Qd25PtX01+MDq5Tz/JsiNHsv/rX5/N4EwPP8zUe2lm+vXP/XG7u8vHPbEC6LJbkmVPJJveeP7d/Kc82fiaoaFkcNAYAQAww8d3wn0AgFk60Gp0dSXd3Xnogx/MnT/3c5O/t2BJ8vf+Y3LVx8v7PT85+fcf25e83JU8+8Xy/ms9+k0P/ehHufP3fz8ZHj7fTv3ze156+OH83jsz369/ftvR2VmOTb/4i7mzp+eE721ILv5QcunK5OJ/lHSuSa6bMro8vTYZfSQ59ifJ4T3Jsa9MrtxpGhoq64WGhtTvAADM0nGdcB8AoIKDrkZnZ7J2bVlrs3bt+f9Lo6NlaDY0VFUQeOrno4cfzu09M7v9+ue/XR0d5cmG7u5cevvtObx48Xn9Q5e+/HIOP/xw1ScbAQDa+hhTuA8AMAcHYY2OjjLo7+wsPzo6kttum/iJv/mbZPfusqpjZCQZG5vLMP/Uz0EPP0zvvVJdv/7MbG93d7mtzff2P//nyRveUN7+279Nfvd3y9tlzY66HQCAOTpuE+4DALTIgdkJR2atGfqdvM16+OHM75G56def2eewe/dEldDwcFGsXu0vCwAw915nFwAAcL6KYmysKHp7k6knIjo6kt27y35+aD+NRkdHGYpPfQ+MjiarV9cl2AcAoHUJ9wEAuGDlQrqrV5czkifbsqXRGBgoZ/hDeyj79ffuPXnh3OHhZMWKVqvYAgCgnoT7AADMiLKCZ8WKsnN/svXry1n8UxcShfmn7NffvfvkhXP7+4ti9WqLTQMAMFOE+wAAzJhyEd3Vq5OplSPlTOZyoU6Yn8p+/YGBExfOHRtLenvrsIYGAAD1ItwHAGBG6eGn3ejXBwBgLgj3AQCYFXr4aQf69QEAmCvCfQAAZo0efuYz/foAAMwl4T4AALNKDz/zkX59AADmmnAfAIBZp4ef+UK/PgAArUK4DwBAZfTwU2f69QEAaCXCfQAAKqWHnzrSrw8AQKsR7gMAUDk9/NSJfn0AAFqRcB8AgDmhh59Wp18fAIBWJtwHAGBO6eGnFenXBwCg1Qn3AQCYc3r4aSX69QEAqAPhPgAALUEPP61Avz4AAHUh3AcAoGXo4Weu6NcHAKBuhPsAALQcPfxUSb8+AAB1JNwHAKAl6eGnCvr1AQCoK+E+AAAtSw8/s0m/PgAAdSbcBwCgpenhZ6bp1wcAYD4Q7gMAUAt6+JkJ+vUBAJgvhPsAANSGHn4uhH59AADmE+E+AAC1ooef86FfHwCA+Ua4DwBA7ejhZ7r06wMAMF8J9wEAqC09/JyJfn0AAOYz4T4AALWmh59T0a8PAMB8J9wHAKD29PAzmX59AADagXAfAIB5QQ8/+vUBAGgnwn0AAOYVPfztSb8+AADtRrgPAMC8o4e/vejXBwCgHQn3AQCYl/Twtwf9+gAAtCvhPgAA85Ye/vlLvz4AAO1OuA8AwLynh39+0a8PAADCfQAA2oQe/vlBvz4AAJSE+wAAtA09/PWmXx8AACYI9wEAaCt6+OtHvz4AAJxMuA8AQFvSw18P+vUBAODUhPsAALQtPfytTb8+AACcnnAfAIC2poe/NenXBwCAMxPuAwDQ9vTwtw79+gAAMD3CfQAAGKeHf27p1wcAgOkT7gMAwCR6+OeGfn0AADg3wn0AAJhCD3+19OsDAMC5E+4DAMAp6OGfffr1AQDg/An3AQDgDPTwzw79+gAAcGGE+wAAcBZ6+GeWfn0AALhwwn0AAJgGPfwzQ78+AADMDOE+AABMkx7+86dfHwAAZpZwHwAAzpEe/nOjXx8AAGaecB8AAM6DHv7p0a8PAACzQ7gPAADnSQ//menXBwCA2SPcBwCAC6CH/2T69QEAYPYJ9wEAYAbo4S/p1wcAgGoI9wEAYIa0ew+/fn0AAKiOcB8AAGZQu/bw69cHAIBqCfcBAGCGtVMPv359AACYG8J9AACYJfO9h1+/PgAAzB3hPgAAzKL52sOvXx8AAOaWcB8AAGbZfOvh168PAABzT7gPAAAVmA89/Pr1AQCgdQj3AQCgQnXt4devDwAArUW4DwAAFatbD79+fQAAaD3CfQAAmAN16eHXrw8AAK1JuA8AAHOklXv49esDAEBrE+4DAMAca7Uefv36AADQ+oT7AADQAlqlh1+/PgAA1INwHwAAWsRc9/Dr1wcAgPoQ7gMAQAuZix5+/foAAFA/wn0AAGhBVfXw69cHAIB6Eu4DAECLmu0efv36AABQX8J9AABoYbPVw69fHwAA6k24DwAALW4me/j16wMAwPwg3AcAgJq40B5+/foAADB/CPcBAKBGzreHX78+AADML8J9AAComXPt4devDwAA849wHwAAamg6Pfz69QEAYP4S7gMAQI2dqYc/ee45/foAADA/CfcBAKDmTt/Dv2jRiff16wMAwHwh3AcAgHlgood/376Tv/t3f5d84Qv69QEAYP4Q7gMAwDzQaHR0JA8/nCxfforD/tcln/hEozG1ex8AAKgr4T4AANRco9HVlezde3K//quvnnh/y5ZGY2CgPBEAAADUmXAfAABqrNFYvz7ZvTvp7DzxO/39ybJlJ/fwlz/faEz9eQAAoE6E+wAAUFONxpYtycBAMnkm/thY0ttbFBs3TvTwDw6e+JvlTP9GY+pMfwAAoC6E+wAAUDONRkdHo7F7dzK1Q78M84tiIswvirGxoujtTaYuptvRUc7g18MPAAB1JNwHAIAaOX2//vBwsmJFUUyt4SkVRX9/OYt/bOzE7+jhBwCAOhLuAwBATZypX78oVq8uiqnB/YmKojwBoIcfAADqT7gPAAA1cLZ+/en+O3r4AQBgfhDuAwBACzuXfv3p0sMPAAD1J9wHAIAWdb79+tOlhx8AAOpLuA8AAC3oQvv1p0sPPwAA1JNwHwAAWsxM9etPlx5+AACoH+E+AAC0iNno158uPfwAAFAvwn0AAGgBs92vP116+AEAoB6E+wAAMMeq6tefLj38AADQ+oT7AAAwh6ru158uPfwAANDahPsAADAH5rJff7r08AMAQOsS7gMAQMVapV9/uvTwAwBA6xHuAwBAhVqtX3+69PADAEBrEe4DAEBFWrVff7r08AMAQOsQ7gMAwCyrQ7/+dOnhBwCA1iDcBwCAWVS3fv3p0sMPAABzS7gPAACzpK79+tOlhx8AAOaOcB8AAGZB3fv1p0sPPwAAzA3hPgAAzKD51K8/XXr4AQCgesJ9AACYIfO1X3+69PADAEB1hPsAADAD5nu//nTp4QcAgGoI9wEA4AK1S7/+dOnhBwCA2SfcBwCA89SO/frTpYcfAABml3AfAADOQ7v360+XHn4AAJgdwn0AADhH+vXPjR5+AACYecJ9AAA4B/r1z48efgAAmFnCfQAAmAb9+hdODz8AAMwc4T4AAJyFfv2ZpYcfAAAunHAfAADOQL/+7NDDDwAAF0a4DwAAp6Fff3bp4QcAgPMn3AcAgCn061dHDz8AAJwf4T4AAEyiX39u6OEHAIBzI9wHAIBx+vXnlh5+AACYPuE+AABEv36r0MMPAADTI9wHAKCt6ddvPXr4AQDg7IT7AAC0Lf36rU0PPwAAnJ5wHwCAtqRfvx708AMAwKkJ9wEAaDv69etFDz8AAJxMuA8AQNvQr19fevgBAOBEwn0AANqCfv35QQ8/AACUhPsAAMx7+vXnFz38AAAg3AcAYJ7Trz8/6eEHAKDdCfcBAJiX9OvPf3r4AQBoZ8J9AADmHf367UUPPwAA7Ui4DwDAvKJfvz3p4QcAoN0I9wEAmDf067c3PfwAALQT4T4AALWnX58mPfwAALQL4T4AALWmX59T0cMPAMB8J9wHAKC29OtzJnr4AQCYz4T7AADUkn59pkMPPwAA85VwHwCAWtGvz7nSww8AwHwk3AcAoDb063Mh9PADADCfCPcBAKgF/frMBD38AADMF8J9AABann59ZpIefgAA5gPhPgAALUu/PrNFDz8AAHUn3AcAoCXp16cKevgBAKgr4T4AAC1Hvz5V0sMPAEAdCfcBAGgp+vWZC3r4AQCoG+E+AAAtQb8+c00PPwAAdSLcBwBgzunXp5Xo4QcAoA6E+wAAzCn9+rQiPfwAALQ64T4AAHNGvz6tTA8/AACtTLgPAEDl9OtTF3r4AQBoVcJ9AAAqpV+fOtLDDwBAqxHuAwBQGf361JkefgAAWolwHwCASujXZz7Qww8AQKsQ7gMAMKv06zPf6OEHAKAVCPcBAJg1+vWZz/TwAwAwl4T7AADMCv36tAM9/AAAzBXhPgAAM06/Pu1EDz8AAHNBuA8AwIzRr0+70sMPAEDVhPsAAMwI/fqghx8AgOoI9wEAuGD69WGCHn4AAKog3AcA4ILo14eT6eEHAGDW/y9WFHYCAMCcHIg1urrKQLwZ8t1xx8R39+9PnnqqnPk7NpaMjLTa7PeyXuThh0+u4RkdTW6/XQ0PNN8rfX3Jli0nf2fjxrLGp9W2t7OzvAqnOUb9wi8kS5aU333xxeS73y3f5+VHeSIDAIDKj9uE+wAAFRx0NTo6krVryyC8u/vEWe7nYni4/BgamstArTwx8fDDJ9fwDA+Xwb4aHjjxPdPdXb5npr73BwfLkH/u3jONxtq1ZZC/du3J7+npGhmZGJuc2AMAqOQ4TrgPADBLB1qNzs5k7do8tHJl7uzpOeF7G5KLP5S84ZPJkh8nnWuS64Ymvv/Ct5In1yTH/iQ5vCf5H/8sOf7ilAdYd+hQdn7ta1WHaWW//pYtJ4eU/f1qeOBsY8LDD5dB+mQjI+VJsWpO2E2cbOzqyrpf/uXsvPjiyd9fuCn5X9YkV328vN/zkxN/f9fry8/PfjH5n48krzwwdWw6dqwcm4aHi2JoyF8eAGCWjuuE+wAAM3yA1Vi/vlw488QA77Jbkhv/afKRrcltz5/fv937UjL85uTQpVPC/pufey6Pf/3rZcA+ezOAy379vr4Tvzo2Vs48ntotDpz8HuroKE+OrV9/8vvo9tvLxXhn67G7u8vHXbt28tcXbkpu2Jp8cGty193n92/v2J5s/2ryl6tOEfZncLAcm9T3AADM6PGdcB8AYIYOrBrd3en5/Oeza/nypJydf9X2pPtHyb2vJNdeMbOP1wzTfjA6KehfduRI9n/5yzM9g16/Psz0eFFdD395xUBf3+QTCpfdkix7Itn0xvM/2Xg6jy5NHvib5M++lxxdMfk7Qn4AgBk9zhPuAwBc4AFVo6srfQ8+mP5Vq5JkwZLk3fcmj9xT3Tbs2J7cu3JSkLbu0KHsvP/+mZhNr18fZmvsmN0e/vKkXF9f82qbxobkuu8nQ1+d+ZONp3PgYPKua5LR4+Nf6Ptv/y3927fP9lVGAABtcTwp3AcAOM8DqSn1Gs3gbN/35m6bNq9M+t8xqRajZ9++7PrkJ8+36kO/Psz2ODI7PfyNxpYt6fnoR7Nr0aIk6VyQ/NZPz/ws/el6dGny0b+eFPIvO3Ik+z/72Zm+SgEAoK2OJYX7AADncRDV6OrKpcPDObx4cZJcf2O1s2HPZs3W5PcenNzLf+5VH/r1oarxZOZ6+Mt/a/fu5smCRXuToXfPXag/1eaVyRe2T67rGRpKenvN4gcAOI/jSOE+AMA5HkA11q9PBgaS1gvOplp+U/LUE81706v60K8PczW2XFgPf6PR1ZV1jzySnZdf3tiQ/MaeZPOe1nyum1cm/2plUmzL+BVG732vLn4AgHM8fhTuAwCcw8HTpNnsnQuSZ15t/W3ufSnZ8dnJIdqtt54u4NevD3M9xpxfD3+jsXZt1u3cmZ0XX7xwU/L0+ta5kuh0dmxPPv78eI1Yz9Gj5djk5CEAwLSPHYX7AADTOGhqdHSUs/XXrk2S9zxY7YK5F2rH9uRj/3q8pufSl1/O4e7uqSGafn1olfHm3Hr4p550/IO/av1gv+nAwWTF4ck1Pb29ar8AAKZ53CjcBwA4ywHTpA7rVq+6OJMDB5PrBk89S1a/PrTiuHP2Hv5GY2Cg+TO/8FPJY6/U8/meWCHmhCIAwLSOGYX7AABnOWBqPPxwsnbtwk3JF5cmd91d7+dz9UXJ6PEky44cyf5Vq5LPf16/PrTq+HP6Hv4y6B8YaGxI7vr1ZOCyej/XNVuTb97bvGcGPwDAWY8VhfsAAGc4WBqf0d7YkAxcW/9gv+mSkfEajGXPPZf9V1554nf160NrjUOn6uH/0z9Nfv7nk/rVhJ3JqoXJd38cHfwAANPwOrsAAODUyg76sqrmN/bMn2A/SfZemizclJTB/v79E9/p7y+K1asF+9A6ygqeFSvKzv0k+dGP0nPNNUly/Y3zJ9hPylqhzgVJdi1alId27SrriQAAOBXhPgDAKTQaXV1Z9+CDSTkrto4d+2dy7RVlxVBjQ5IsW1YG/L29eq6hNZWL6K5enfzmb+bm//7fs2vRostuSfZ9b/4912deHT/5eOeb35yeb3/bXx8A4NSE+wAAUzQaHR25dHg4Oy++uHPB/JoVO9ldd5dXJJSWLfOXh9ZWXlHzD/9hHn/rWxduSv74ofn7XJ9enyxYkmTX8uXlosEAAEwl3AcAOMmWLTm8ePHCTeUM0vls857yyoQkyaX9/SowoHWVVWHd3Y0NybceKq/Ama+uvSL50r9sXl20fn257gAAAJMJ9wEAJmk0OjuT9euTMjxrB4/ckyzam+Tw4sXNNQaAFnTzr/96kvS8Jbnt+fn/dO+6O7nu++N3+u67zwsAAOBEwn0AgMn6du5MykUq2yE8a/pEc7HgdR/7mNn70Hoajb6+PH7llQuWzN+qsFMZ+up4PU//qlXllQsAADQJ9wEAxjUa3d3pX7WqsaEMlNrJ5j3JZbck2XnxxcmWLV4N0EpjU0dH1pUz1++7or2e+7VXJO++d/zOOrP3AQBOOE4sCjsBACBJGhu/8530r1p1/Y3Jvu+13/N/dGnyzhea966+uihGR70qoAXGpsaWLUlf36K9yZGu9twHF70pOf5ikvT2FsXgoFcFAICZ+wAAScYXquxftWrBkvabtd902/NJ54LmPbP3oTXGps7OLPvIR5JJ9Vlt6Ff3jd9Y9rnPqQ4DACgJ9wEAkjQX0X33vWUNRJV2bE+W3zTxsWph+bW58Ad/lTQ2JMnateXiwsCcj037L7mkc0FZn1W1HdvLMWnyGLV5ZfXbMXDZ+MLf+y+5JFm71usCAEC4DwBQzoxNV1djQ7ULVW5eWVZNrP8XybNfLD9+MJp898fl1y56UxmqVenaK5KrXjuxIECDOdfzzncmyYcqruPpfakcgz72r5Mf/mTi689+MfnMk8nrfq0M+g8crG6b3vFY81Z3txcGAIBwHwAgzaDoqgpnyy+/qQzIfrYz+X+eK3u0j3Qlr76QfPqGZOGmsl/6uz9O3nBftQFa94/Gb/S9611eGzB3Go3OzuxavryxodpZ+8tvSv7t8rIK59UXkmdeLdch2fe9cpx6z4NJsS156onkZ1ZWd6VR//uat9auVc0DACDcBwBIHvrFX0yS6ytqmV+zNXn67cngvynDsqk1QJv3JE+vLwP+JHnlgeS6weoC/oHLxm/0r1olQIO5VF49U+WJx96Xkr9clfzFnkljwRSP3JNcf2N5+/iL5ez+Ksana69ILrulec/sfQAA4T4A0NYajY6O3NnTk0yeFTp7DhxMdv0w+SdfTu46w+KY116RfOuhifuvPJCs/UB1+2UiQFPNA3OnDLBfu5qmAv92eTne/MzK8kTk6dw9aTw6/mJy11ur2b5lT5y4bwAA2plwHwBoc2VAdNkt1Syku/YDyeu/njz2ytl/9rbnJ4fs5Wz/qmbv3/hPT9w/QLXKq2bK99/pZtDPtAMHy6A+KT9/897T/+zUk5N/9r1qtnHTG8dv9Lz//V4lAEC7E+4DAG2uDM8mZoPOrme/WIZmjUZyycjZf34iZC87rh+saIHd165iGF/ME6haedXM5BN8lCc9F25KsmvRokbDlUUAQHsT7gMAba4M91+bDTrLjq448faZai+S5LqhE+8/uaaa7bz2iskBmtn7UL3OzuTEE3xVvO87F0zcb/bqn8qjS0+8f+nK6rbzrY81b3V1eZ0AAO1MuA8AtLkyQLvt+WoebcGS+uyZiQDNorpQvTK4nnqCb7Y982q52Pcfvqlc8Pt0/sOfnXi/qgXJk+SGR4xNAACJcB8AaGONRhmeLdpb3WO+e1KH9cJN1Szie+HMjoXK3XzNNUnywa9X/9B33X32E57Db564vWBJ8sg91W3fm36peas8OQsA0K6E+wBAG6t+1ucj95QzYj99Q/K39599Ed/H9p14f2LG6uwzOxbm0ONXXplUs9D3uTpwMHl20oK691W8jZv3jN9Y9va3e6EAAO1sgV0AALSvckb6VR9P8r3qHvW255Pbpvmz+29M8p3ydmNDcu8r1W2n2bEwNxqN8j1X5VVF5+Jd1yTF8XJM6nlLsvmeOdhHG5Ji2yWXeLUAAO1MuA8AtLFyRvrikdbcukeXJi+9MHH/uu9XO4t3857kM40kueYai+pCld72tlbcqs0rky//veSl4+WJhwf3lBU+c+HiDyVHt5X1akUxMuI1AwC0I+E+AND2Vi1vze366F9P3F64Kdl3/1xtyZVXJrt3e6VAtaq+quhUXvdrSbHtxK9ddkvyf767uoXIz0xtGADQvnTuAwC0oB3bk9Hj5e3GhuRbD9knQPX+7jeToig//vBNyXseTP6//zt55wvJJSPlWAUAwNwQ7gMAtJgDB5OPj8+IbWxIBq5tlRmyQDu77flyUfC/2FNeTXR0RdJ7IFmz1b4BAJgLankAgLb39NrW2p53XZO8cnwi2J+rTusT9fd7pUBVrrgief/7X/yp1ty6a69I+v5z8pmUlT3fTNL7fyQDl/nLAQBUSbgPALS90UeS3NMa27Jma1nH0wrB/kTdxvBwUWzc6JUC1Wg0urqS97//bz/futu4eU/Sf1/yygPj48Vnk3s/Ud2i3//jn5Wfi2J42CsGAGhXankAgDZWhkLH/qQ1tmbN1uSb95Z1F3/5ibmfsf9fv9K8NTbmtQLVKYqRkSQ59pXW3s63PjZpm7cld721usc+/qLXCQCAcB8AaHuH98z9NuzYPhHsP72+utmvZ7Lr9c1bo6NeJVCxZUeOFNvqtcl/9r3qxsuSWfsAQHsT7gMAbatZ5zDXs2N3bC8XpexckPzt/acP9h9dWn5UT7gPldv//e8nyeaV1T3kmq3J636t/Fh+09l/vucnJ96vaix1VREAQEm4DwC0t0tffrnYlhw4ODcP/+jSMti/anvyzKtn/tlPXVV+VOXZLzZvCfeheuX77oVvVTcWffPesl6n2JY89cTkGfKnVtW2TfXYPmMTAEAi3AcA2t3h3buT5MGF1T/0gYPJL905vWA/KcP2qTNlZ9PELNyy/xuoUhlcD7+5mkd74vKTv7b3fWf+nSfXnHj/4g9Vs637bzxxHwEAtCvhPgDQ5srguqoArenAweS6wWTp56YX7CfJ0RXJjYeq2b7el8rZu8nISFGovoDqDQ0lybMVLaw9dWxpbEje+7Zz+zfedtPsb+eBg8lL3zlxHwEAtKsFdgEA0N6GhpItW6oK0JredU2STyUf6ppep3Zzcdvbnq9m+yZOdgjPYC4Uxeho48OHDhXbLr98x7XJXbM8Rt32fLLgTclP7kiu+35y97VnH29+MGnefGNDsuMTs79fJq6yGhpy4hEAaHfCfQCgrRXF6Gjj3/35nxd3/tzPbd6TbN4z+4959UXJ6PEkDySfOYffW7ipuv3y7N1JtiXCfZhDO7/2taSvb/tXZz/cT5L7rkg+sy3pfPDsj7dma3L8xYn7d/16cu1ls7+NEyce1YUBAKjlAQC48/d/P5mYHT+blt80Huyfh0v+r2p2x47t45U86w4dKgqd1jB3ypNrP6joXbh5T/KeB8uFdZffdPqFxndsT3b9cOL+ex5MBi6rZhsnrrJy4hEAQLgPAFBhgPbUE+f/u0t+XM3e2P7V8Rs7v/Y1rw2YO0UxMpJ1hw4dfzF5dGk1j/nIPcmnbyjHw7d+obzSaM3Wsj5s88oy9O89UJ4AXLCk/NlH7qlm215bC6Rn3z4nHgEAkkZR2AkAAI1//OyzefzKKz99QzXVPK3sojc16zZWrCgK1Rcwp2NTY2AgWb/++huTfd+r9rF7X0qeXJM8+8Xk2FfKr138oeTSlUn3j6qbrd/0WqVZ+vuLYuNGrw4AoO2PFYX7AABJo7FlS9LXt2hvcqSrfffDqoXJd3+cJKOjRXH11V4ZMNdjU3d3snt3Y0Pyl59Irr2iPffDo0uTd77QvHf11WbuAwCo5QEAGNffn2VHjhxdUc5WbUcHDiZ/9JHmvd5erwmYe0UxPJwMDRXbkndd0777Ye3vTYzVgn0AgJJwHwAgSVGMjWX/pz6VJP92eXvug7UfGO+z7nvssTJQBFpDWUEzery67v1WsnllcnRFknXHjiX9/V4PAAAl4T4AwLiiGBxsLl65Zmt7PfdHlyZPv338Tv/993s1QCuNTaOjyeBgkvzKsvZ7/l/YPn5j55e+VBRjY14RAAAl4T4AwGQ77703SXb9sKypaRcf/evxWfsZHDRrH1rRxo1Zd+zYS98pZ7K3i96XxmftLztyxKx9AIATCfcBACYpiqGhZHi42FbW1LSDHdvLuo+S8Axac2waG8vOL30pSfrf0R7P+cDBSTVp+z/1KbP2AQBOJNwHADhJGXA/9cT8r+c5cDDpPTDxvC1UCS0+Nt383HOvPJBcfdH8f7YrDifHX0ySkZGiKGuJAACYINwHAJiirKXp7U3Kep4d2+fn8zxwMLlusFnHMzxcFOWinUCrjk1jY3n8fe9Lz9Gjo8eTVQvn73NdftPkOp7bb/fXBwA4mXAfAOAUylmig4PFtnJm+3zs33/XNckrDyRZd+iQ8AzqMjaNjGTXJz+ZJN/9cdlJP9+s2VpeOZUk2f+Od7iiCADg1IT7AACnURS9venZt6/YVs5wn08B//Kbxnv2e44ezc41a3RZQ53GpsHBZn3Yjs/Or6uLdmxPvnlv815vb1GMjPiLAwCcWqMo7AQAgNMeLDU6OnLzn/5pHr/yys4FyTOv1v85rdk6OTy7/fZyEWGgfuPTwECyfv2CJclf7EmuvaLez2fH9vJKqbIqbHCwKMp6NAAATs3MfQCAM5jacf2G++o9g3/5TZOD/Y0bBftQZxs3JiMjx19M3vqFes/g37xycrA/PCzYBwA4OzP3AQCmc9DU6OrKpcPDObx48YIlyZf+ZXLX3fXZ/gMHy4790ePNr2zcWBRlrQdQ57GpoyPZvTvp6mpsSHrekjxyT72ew6qF5foBpaGhso5HVRgAwNmYuQ8AMA1FMTKSw52d6dm37/iL5QzTuixkeeBguWbAax37uf12wT7Ml7FpbKwoVqxoLgD+zXvLK3Tq4uqLJgf7/f1Fcfvtgn0AgOkR7gMATFNRjI1l1623NkO0wSXljNNWtmN7WdfxygNJ1h06lF233qqKB+bj+NTbm5RVNk89kSy5tbUrxA4cLGvORo8nWXfsWDlbf+NGf0kAgOlTywMAcD4HUY0tW5K+viRZtDf5xN3J5j2ts32PLk0++teTa3iGh8sZ+2bEwvwem7q7s+wb38j+Sy5p1Zqe5TclT799vF//0pdfzuHu7qIYGfHXAwA4x2M/4T4AwHkeSDXWrs3Nn/tcHr/yyqQM+Yfendz2/Nxt04GDydoPTArOkpRVF2bEQvuMTV1dyZYtSXd3kixYkvzqvmTgsrndrjVbk997MDn+YvMrTjoCAFwItTwAAOepKIaG8vjP/3zS3591x44dXZG884WyQ/rRpdVvz6qFZQXPU080g/3BweTqqwX70G5j08hIUaxendx+e9YdOnT8xbJG7JKRZPPK6rdn88rkojeV6wEcfzFJz759yerVRbF6tWAfAOD8mbkPADATB1WNjo6ypqes6kmSzgXJ9VuS/vcl114xO4+7eWWy6/XJD0YnzYbte+yx9N9/f1EMD/vLAI3G+vVZ9rnPZf8llyTJwk3JDVuTTW+cvSuNHl2aPPA3yZP3jK/5kZTrfuy8//6iGBz0VwEAmIHjPOE+AMAMHlw1OjvLgH/9+slfv+yWZNkTMxOm9b6UDL85efbuydU7STI6Wi5KKdQHpo5N4ycgl33kI82QPymD/rc+ltz9geSuuy/sMXZsT7Z/dcrJxmS8V3/LlqLo7/eXAACYwWM84T4AwCwcZDU6O8u+6+7uZO3ayd9buClZ+rnk4n+UdK5JrhtKPvj1k2f3N+szdr2+/PzsF5OjK6Y80EN//ue58/d/PxkasiAlcPaxqaPjtbGp5/3vz65Fi5rfW7Ak+V//QbLkx8nikWTV8uTGQyefkNyxPfmvX0ke25e83FWOTce+MuVk40M/+lE5Ng0PF8XQkD0PADALx3bCfQCAWT7ganR0lAF/V1eW3XHH5Fmz52d4uPwYGiqK0VF7GDj/8Wk86L/5jjuai4Oft5ufey6Pf/3rTjYCAFR0LCfcBwCo+ACs0d1d3mp+7upKOjvLj6axsWRkpKzaGRsrP4+OJiMjFqAEZmds6upKOjrKMWnq58ma1V8jI5PHKicbAQAqPn4T7gMAAAAAQL28zi4AAAAAAIB6Ee4DAAAAAEDNCPcBAAAAAKBmhPsAAAAAAFAzwn0AAAAAAKgZ4T4AAAAAANSMcB8AAAAAAGpGuA8AAAAAADUj3AcAAAAAgJoR7gMAAAAAQM0I9wEAAAAAoGaE+wAAAAAAUDPCfQAAAAAAqBnhPgAAAAAA1IxwHwAAAAAAaka4DwAAAAAANSPcBwAAAACAmhHuAwAAAABAzQj3AQAAAACgZoT7AAAAAABQM8J9AAAAAACoGeE+AAAAAADUjHAfAAAAAABqRrgPAAAAAAA1I9wHAAAAAICaEe4DAAAAAEDNCPcBAAAAAKBmhPsAAAAAAFAzwn0AAAAAAKgZ4T4AAAAAANSMcB8AAAAAAGpGuA8AAAAAADUj3AcAAAAAgJoR7gMAAAAAQM0I9wEAAAAAoGaE+wAAAAAAUDPCfQAAAAAAqBnhPgAAAAAA1IxwHwAAAAAAaka4DwAAAAAANSPcBwAAAACAmhHuAwAAAABAzQj3AQAAAACgZoT7AAAAAABQM8J9AAAAAACoGeE+AAAAAADUzP8PheWJ15JwhaIAAAAldEVYdGRhdGU6Y3JlYXRlADIwMjItMTEtMDRUMTA6NDg6MjcrMDE6MDBFR9R9AAAAJXRFWHRkYXRlOm1vZGlmeQAyMDIyLTExLTA0VDEwOjQ4OjI3KzAxOjAwNBpswQAAABR0RVh0cGRmOlZlcnNpb24AUERGLTEuNSAFXAs5AAAAAElFTkSuQmCC"
}
},
"cell_type": "markdown",
"id": "ec19cc24",
"metadata": {},
"source": [
"For our illustration, the problem is to color the nodes of a complete graph (later, we introduce the conditions to be respected). We consider here a complete graph with 4 nodes:\n",
""
]
},
{
"cell_type": "markdown",
"id": "7776043f",
"metadata": {},
"source": [
"We use a constant n to denote the number of nodes:"
]
},
{
"cell_type": "code",
"execution_count": 2,
"id": "55ecd7d9",
"metadata": {},
"outputs": [],
"source": [
"n = 4"
]
},
{
"cell_type": "markdown",
"id": "b021c396",
"metadata": {},
"source": [
"Finding a color to each node implies that we introduce a variable with each node. Let us suppose that we have 3 colors only. We can then write:"
]
},
{
"cell_type": "code",
"execution_count": 3,
"id": "55dbebcb",
"metadata": {},
"outputs": [],
"source": [
"R, G, B = colors = 0, 1, 2\n",
"\n",
"# x[i] is the color of the ith node\n",
"x = VarArray(size=n, dom=colors)"
]
},
{
"cell_type": "markdown",
"id": "fb942a15",
"metadata": {},
"source": [
"We can display the structure of the array, as well as the domain of the first variable (note that all variables have the same domain)."
]
},
{
"cell_type": "code",
"execution_count": 4,
"id": "347b7e18",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Array x: [x[0], x[1], x[2], x[3]]\n",
"Domain of any variable: 0 1 2\n"
]
}
],
"source": [
"print(\"Array x: \", x)\n",
"print(\"Domain of any variable: \", x[0].dom)"
]
},
{
"cell_type": "markdown",
"id": "23daebc2",
"metadata": {},
"source": [
"Let us suppose that all nodes with even indexes must have a different color, as well as nodes with odd indexes.\n",
"We then have two constraints to be satisfied here. We post the two constraints by passing them as parameters of the function *satisfy()*:"
]
},
{
"cell_type": "code",
"execution_count": 5,
"id": "f7cd740d",
"metadata": {},
"outputs": [],
"source": [
"satisfy(\n",
" x[0] != x[2],\n",
"\n",
" x[1] != x[3]\n",
");"
]
},
{
"cell_type": "markdown",
"id": "d5b9a806",
"metadata": {},
"source": [
"Interestingly, by calling the function *solve()*, we can check that the problem is satisfiable (SAT). We can also display the found solution. Here, we call the function *values()* that collects the values assigned to a specified list of variables."
]
},
{
"cell_type": "code",
"execution_count": 6,
"id": "91ad3a0e",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"[0, 0, 1, 1]\n"
]
}
],
"source": [
"if solve() is SAT:\n",
" print(values(x))"
]
},
{
"attachments": {
"graph4b.png": {
"image/png": "iVBORw0KGgoAAAANSUhEUgAABfcAAAGVEAYAAAADABe3AAAABGdBTUEAAYagMeiWXwAAAAZiS0dE////////CVj33AAAAAlwSFlzAAABLAAAASwAc4jpUgAAAAd0SU1FB+YLBAsBGPJZso8AAGU0SURBVHja7d1tkGRndSf4UxqEYAK91CJCJoyY3jIh9yqwkNRlD8yqQWZbY4joYXokGmPLg3cGb6Zlj/EsQlSBAgmJEM4EpNmVw8ZZazyLB/mFtlgNozBMdAXGau1gjAo1GoeipcW1vRJem5CYRhIxsiSvaj+cfPpWVmfm7ZfK6qrM3+/LqXuzblXlkzdv3uj+P+eZWllZWVlZCQAAAAAAAAAAAAAAYATOMAQAAAAAAAAAAAAAADA6gvsAAAAAAAAAAAAAADBCgvsAAAAAAAAAAAAAADBCgvsAAAAAAAAAAAAAADBCgvsAAAAAAAAAAAAAADBCgvsAAAAAAAAAAAAAADBCgvsAAAAAAAAAAAAAADBCgvsAAAAAAAAAAAAAADBCgvsAAAAAAAAAAAAAADBCgvsAAAAAAAAAAAAAADBCgvsAAAAAAAAAAAAAADBCgvsAAAAAAAAAAAAAADBCgvsAAAAAAAAAAAAAADBCgvsAAAAAAAAAAAAAADBCgvsAAAAAAAAAAAAAADBCgvsAAAAAAAAAAAAAADBCgvsAAAAAAAAAAAAAADBCgvsAAAAAAAAAAAAAADBCgvsAAAAAAAAAAAAAADBCgvsAAAAAAAAAAAAAADBCgvsAAAAAAAAAAAAAADBCgvsAAAAAAAAAAAAAADBCgvsAAAAAAAAAAAAAADBCgvsAAAAAAAAAAAAAADBCgvsAAAAAAAAAAAAAADBCgvsAAAAAAAAAAAAAADBCgvsAAAAAAAAAAAAAADBCgvsAAAAAAAAAAAAAADBCgvsAAAAAAAAAAAAAADBCgvsAAAAAAAAAAAAAADBCgvsAAAAAAAAAAAAAADBCgvsAAAAAAAAAAAAAADBCgvsAAAAAAAAAAAAAADBCgvsAAAAAAAAAAAAAADBCgvsAAAAAAAAAAAAAADBCgvsAAAAAAAAAAAAAADBCgvsAAAAAAAAAAAAAADBCgvsAAAAAAAAAAAAAADBCgvsAAAAAAAAAAAAAADBCgvsAAAAAAAAAAAAAADBCgvsAAAAAAAAAAAAAADBCgvsAAAAAAAAAAAAAADBCgvsAAAAAAAAAAAAAADBCgvsAAAAAAAAAAAAAADBCgvsAAAAAAAAAAAAAADBCgvsAAAAAAAAAAAAAADBCLzEEAAAAAIyzqampqampmZncqqvT0yf205eWercXF7MeObKysrKysrL2cQCAzX7fVO6HduzovT9au13un072vqlsl/umch8FAAAAAONpKv8hzEAAAAAAsLVl0Gzv3tzasSO2R0T89E/HoYiIbdtO71+3b1/WEkjbty//Xe7IEa8cAHB67ptKEH/Xrqyr7qNOqxLoL/dP5b5pedkrBwAAAMBWJrgPAAAAwJbQ2wG2BMx27Yo9ERE/8zNxT0TE2WevPe6Mb2Y963NZz3+09/HLvpb13P8j686H+v/+h5/LuvzxrI//SdYnP5z1qY9mffb/yfrCNTVP6L0REV/9anwmIuLLX86dgmkAwHrfPw26b3rta4/5/m1ZX3Z1//ummf3d+6ZXZN19S//f+92dWb/x1u590g+691FXZf3bd2T9waHu9heyrhwe8ET2REQ89lj+3b//+733TVY4AgAAAGBrENwHAAAAYFPqDerPzfXWY515d9aZD2X9id/OOiiIP2olsPaFqax/+XzWp2eP5+jSmb/dzn+/K9sAAHX3T3NzcX5ExPx8PBkRcd55a7+vTGz84Zu690/dQP61t5/ev/+u67M+/OtZn+xOmBwY6N8eEXH4cK6w9Gu/lvdNCwvOBAAAAAA2I8F9AAAAADaFY4L6eyIifumX1nbSP+eBrK/+2axvb2a9+Kyt9XxPLJi2b1/W+Xkd+QGA3vunRiPvm268cW0n/TKx8Yf+bdYrP5j1dE1sPFkHLsn61U9k/atbs754+ZpvvCIi4uDBuD8i4oYbTIAEAAAAYDMR3AcAAADgtDoaOLsiIuKTn8yg1TnnlMdf/v6szR/OutUC+serdOhfuDHrd/4ia/8gf+kkW4L8R444kwBgUu6bdu2K90ZE3HhjfCYi4sory+Olk/7uq7r1lvEej0+/Oeu3/i7rMUH+90ZEfPWrOU633SbIDwAAAMDpJLgPAAAAwIY6GjjbHhHxv/1vcSgiYtu28ngJ6l/12azjHjgbpAT57/x61icaa75he0TEU0/l+P3Wb+W/883PO8MAYNzum8qKRJ//fNZdu8rjJaj/hpdkve6+yR6vj305qwmQAAAAAGxGgvsAAAAAbIijnfUjIqLTKftL4Gznm7Jee7ux6ufh57L+zluyPj3b77v27cvabAqiAcBWv2/asSPOj4hYXIwnIyLOO29qWz7+mtdnbdyW9YIDxmy12pWMroiIOHgwV3r6hV/I+6alJSMHAAAAwCgJ7gMAAAAwUhk8K0H9xtG+8RfuzvqRtxmjk3HvzVn/w9lZ+wfRrrkm//1vedmIAcBWuW9qNGJPRMSnPhX3REScffaZd+fjN70uq6D+iSkTIH9jW9YXrll93/T0070B/jIREgAAAADWl+A+AAAAAOsqA2fT0/HeiIgvfCE+ExFx5ZXl8cseynrdfcZqPRy4JOsfPJG1fxDtrW/VSRYANvv9U6uVW3NzZf+rFrLe9rwxWg+lE/+dX8/6RKPfd83P531Tu23EAAAAAFhPgvsAAAAArIsMnO3YkYHx3/7tDIxfeunUtnz85343686HjNUolCDaxz+b9dk7+n1Xs5n/HriwYMQA4HTfN01P51ZZmWjv3vK4iY4b42Nfzvr4vf0eXVjI+6Zm00gBAAAAsB4E9wEAAAA4JUcD++dHRCwuxpMREeedd+bd+fhNr8t6wQFjtZGGB9EE+AHg9N8/PfBAbu3YUSY6/pNnsu6+xRhtpE+/OevBd2RdObz60X378r7pXe8yUgAAAACcCsF9AAAAAE7K0U6xV0REfOUrpcP+Od0I2g1nZhXYP71KEO3BS/o9etVV+e+Di4tGCgA26v6pdNhvNKxMtLkc6N4vfe49WXsD/O123jfNzxspAAAAAE7GGYYAAAAAgJPyyYiI3/mdEtgvHfYF9jeX6+7LeuHuNQ9cERFx990ZIJyZMVIAMDr5eTs3l1sC+5tVeR3Kyge95ubydWw0jBQAAAAAJ0PHfQAAAABOSAaWWq3cmpsrwbNf/ZWsF59ljDazD7wx69Oz3R1XREQcPJgTMN761vz3wiNHjBQArNd9065dubV/f9l/WTcgXibYsTndfmfWRx7t7tgTEfHMM3FPRMRP/mTeNy0tGSkAAAAAjoeO+wAAAAAcl94Oo6VjbNWRVGB/aygrIpQVEsqKCbnR6RghAFiv+6YdO8oKN2V/WQFHYH9ruP59WV+10N1xT0TE2WfH+RERi4v5Ok9PGykAAAAAjofgPgAAAABDHQ2eRcTqYHfpFLv7FmO0lVxwIOu7X9V9fbetfnTv3t4VFQCAE79vmp7OwP5v/3ZOkDvnnHMeyMc/8jZjtBXd9nzWoxMfn4yIOO+83KhWUgAAAACAYQT3AQAAADgOVZC7dBzVKXZr29mdeFFWTOg1N5fBw5kZIwUAJ2purqxoU4LeZcUbtrabXpf1jG+u3rtjR+/KVAAAAADQn+A+AAAAAH1lAGnXrtzatat0Zn/fPzQ246SsmFAmZPSamzNCAHC8902l0/5115X9b+9GucuKN2xt5XV8w0vWPLAnIuLGG40QAAAAAMMI7gMAAADQ356IiM98pmxe9NKsgmfj6dq+nfcbjQwi7thhhACgTum0f845L39/7ikT5BgvZeWpsqJC3BMR8drX5n1TtVIVAAAAAKwmuA8AAABAjwwcNRolgHTGN3P/9e8zNuPs4rOyXri736MCaAAw+L5pZia3qpVq3rnH2EyCsqLCUXsiIn7pl46uwAAAAAAAqwjuAwAAANBrT0TEjTeWzTe8xJBMksZtWae2rd67a1cG0HbtMkIAsFYV2H/VQtadDxmVSVBWVCgrLOTE17PPXnteAAAAAECE4D4AAAAAXRnMbrVKp/0z7879191nbCbJBQeyvub1/R4VQAOA6r5px47cahztu37tM8ZmEvVfYWFurndFBgAAAAAmneA+AAAAAGl7RMRP/3TZfHtjMp72d3dmvev6rB/7cv96782TdTqUzvtnfHP13tJ5vwQVAWCS7d1bvrpwd9aLz5rsESn3VeX+qWyPu7LCQllxYdB5AgAAAMBkE9wHAAAAmHBHO4EeiojYtq0EtXffMp7Pd22g7KZ/mvXPfznr338068z+3uPu7W7/4j/KWoL+46p03v/hm/o9KoAGwITbExHxMz9TNq/84GQPR5ngePP/l/Xxe7N+462TNQ4X/8qaHVdERLz73d4wAAAAAEREvMQQAAAAALA6iP3KB8bzGZbA/q3fzvpCN1B2WbdD6nX3db/xfQOO/3tZ7/x61j99LuvDL8162/PjOW6XfS3r42XHFRERP/VTuTE/770DwCTpXXnmta8tEx53/qfJeP4HLsn6F+dlPfS/Z332e91vuHyyz49rb89636eyrtwfEXHppWWi7MrKysrKyvKydxIAAADAZNJxHwAAAGDSfTIi4tpry+YxnULHxMc/m/WFa7JeuDvr0cB+jdKBvgT0z7w76xONrLffOZ7jVlZemNrW3bEmgOYNBMDkqSY89l+ZZusrHfQb/6q3/rs3Z/3W32U9/1FnQz/nf7jf3l27jAwAAADAZBPcBwAAAJhQR4PXN0RE/NiPlWB26RQ6Lkqg/tk7us+7+zwbt53az/1HP9u7/Wg30P/wc+N5vvQPoFXBRQCYCD0rz1Qr04ybH/9K1ne8srf+6+594m91Vxj4yNucEv285o399gruAwAAAEw6wX0AAACAiVYFiPoHs7e+/+sPerfL8ywd9E/W2gkOK4ez3nX2eI5j/5UYBNAAmAxHJzyWlWe25f6yMs24KfdJ5fmVevFZzoXjcfVKv7179+Z5ND1thAAAAAAmk+A+AAAAwESrgtf9O4NuXXddn/XFy3v3/zefWt/f8/L3924/+fHxPFP6r8Swa5cAGgCTo1ppZlwnPLI+ysSHcx4Yfv8NAAAAwGQR3AcAAACYVOdHRFx1Vdns3xl063r41/vv/9Hvre/vecX23u3Sef/em8fztFk7USHt2OENBcD4m5kpX/VfiQZ6nftR900AAAAAVAT3AQAAACbVkxER5503tS03S2fQcfG92Y35PS/7Yv/9D75pPE+b8x/tt7cKMgLA+Ko+7859hdGg3mVfc98EAAAAQEVwHwAAAGDCTE1NTU1NVZ0+X3b1eD7PFy/vv3/mwxvz+5+8aJLOKgE0AMbc+RERs0enBe6+xZBQ79z/o9/e6WkjAwAAADCZBPcBAAAAJlIVGDrzZ8frmd178/DHLz5rY/6Ov/vvx/PM0TkWgInUXanIQHAidj7Ub++uXUYGAAAAYDIJ7gMAAABMpCowdO5HjcYovHDNeD4vnWMBmCRrVyp6+fuNCSdxHm0zBgAAAABEvMQQAAAAAEy28z/e/eI+Y0G90jn23/XsnZ3NYKMOsgCMo8suK18dXanoz4wKx+9lV2d99o6s5b5pZWVlZWVlcdEIAQAAAEwGwX0AAACACXfhT3a/uGU8ns/jf9L94hKv7cY577ys+/cbCwDG2dGVit5mLAAAAACAE3OGIQAAAABgnDz5YWMAAAAAAAAAbC6C+wAAAAAAAAAAAAAAMEIvMQQAAAAAk+2RV2bdPSbP57KvZX3cS7uBvv/9rHv3GgsAxs9ll2X9xCeevMhoAAAAAAAnR3AfAAAAYCIdOVK++q8CaJyAe2/ut/eBB1ZWVlZWVhYXjRAA42Rqampqaqq6b4KT8bdf6N123wQAAAAwmc4wBAAAAACTaGmpfPXUR43GKExtG8/n9dQP+u1dXvaKAzCOMmBd3Tc9e4cx4STOo8PdL7ZHRDz1lBEBAAAAmEyC+wAAAAATqeoc+8Lvjdczm/nw8Mf7d4xffy+7ejzPnOWrhp9PADCWtkdEHD5cNr+705BQ75j7zkMREd/4hpEBAAAAmEyC+wAAAAATZtw7x1581ub4O16xfZLOKh33ARhzhyIivv3tsvmNtxoS3DcBAAAAcGIE9wEAAAAmWhUcGrfOsS9//8b8nqc+2n//a944nmfMkxcNP48AYHxVEx8f/xOjQb0H39Rvr5WKAAAAACaV4D4AAADARKsCaF+YGq9n9tp7++9/5JXr+3te+L3++9+yf7zGs0zs6L9CQ3UeAcD4qiaq/eXzRoN6f/Mv3DcBAAAAUBHcBwAAAJhoi4vlq3ELoL292X//f/nA+v6etUH20un/4rPGazz7T+zYt29lZWVlZUXnWAAmwb595atn3mk0GKxMeHzhmu6OKyIinn4675uq8wgAAACAySK4DwAAADDRquDQ07NZS9BoqyvB+Vct9O7/3uz6/Py7ru+//yd+YzzPlP4TO6qJHwAwzo5OVLsiIuLgwZXDw+8HmGzHTHi8PyLiP/5HIwMAAAAw2QT3AQAAACbU0QDaJyMi7rmn7F/8ifF6ntc+k3VqW9YXL8/66Tef2s/981/u3S6d9q+9fTzPl/6dhXWMBWDC3B8R8Qd/UDYf/nVDwrFMeAQAAACgn5cYAgAAAIAJd0NExJ/9WW7s2XM0gPb8eDy90nn/n3QD/F/s7j/4jqwHfjfrzoeO7+eVwP+z/yrrmXdn/fDrut9wYLxOj9JJeOW57o7SafhAd+IHAEycMnGt1Xry491dHxjPZ3rvzf33P/LKrH/9e8OP/1J35aNHPpT1R7/X//t+/CtZL9ji91Fl5aqn3zDsvAEAAABgUum4DwAAAECsDhIdDaCNmd23ZP3n92Wd+kLWz70n6+13Zi2Bq+LAJVlvfGnWB7vbpcP+Td3A/gUHxnPcjukkvKbTMABMklyxaHk5tkdEHD68crj3fmHcfPF7/esjj2Z9erb3+8v9UVnp6IVrer9/0M/7xlvHY7z6r1y1b9/Rla4AAAAAmGhT+Q9FBgIAAABg0k1NTU1NTT3wQG7t2HFZtwP9dfeN9/MuHfT/srvCwLP/T9YSNCsBtFdsz/qmbsfYMhFgXJUJDDf906wlmJh+5EeOBhcBYGLvm1qt3Jqbe1W3s/xtzxubSfar3TujZ+9YvXd+Pu+b2m0jBAAAADDZBPcBAAAAiIgSQGs0cqvTOeOb+dVv/SdjM4k+9uWsj9+7eu/iYv574lVXGSEA3DfNzOTWX/5l2V9W9tn5kDGaJPfenLWsIJArMjz1VByKiPhv/1sd9wEAAACIiDjDEAAAAAAQEZGBooWFDBodPvzi5bn/9juNzSR5+LmsvYH9Yn7eCAFAuW8qK89UndT/6B5jM4m+tLBmx6GIiN/6LYF9AAAAAFYT3AcAAACg16GIiP/pfyqbjz6f9bs7Dc0kuOvsfnsXFjJ4trRkhABgrXY79kREPPPMs3fkntKBnfH26TdnfeGa7o49ERGPPZb3TSY8AgAAANBLcB8AAACAHhk0WlyM90ZEfPWrK4dz/8KNxmacHbgk6xONfo9WnYQBgLX3TUeOxD0REb/5m2X//p83NpPgW3+3Zsc9ERG33WZkAAAAAOhHcB8AAACA/j4TsTp49J2/yPrwc4ZmHP3RPf32ttsZSFxeNkIAUKd03n/ssdJ5v3RkZ7x87MtZX7y8u+OKiIiDB/O+aWHBCAEAAADQj+A+AAAAAH0d7bwfERELC6Xz/u+8xdiMkxIoLAHD2B4R8dRTuaHTPgAc/31T6bxfTXw8+I6s391pjMZBWaGoTGg96v6IiBtuMEIAAAAADCO4DwAAAMBxaLdLoPvp2dxTOo2yNZXg2YOXrHngUETEBz94NIAIABy33o7rS0tl4uOt384qwL81ldftD57ovs6HVz+6sNA74RUAAAAA+hPcBwAAAGCoDCItL2eg+53vLPsfvzdr6djO1vDwc1k/955+jx48mHV52UgBwKk6cCAnPv6//+8L1+SeO79uVLaij382a3kd44rV903z80YIAAAAgOMhuA8AAADAcentJNpslv2lY/uBS4zRZlY6xf7Gtu7rebj7wPaIiMcey41LL826f//U1NTU1NTcnJEDgHr5uTk9nXX//tz7r/91Tnx86qnYExHxzDNPNPKR2+80ZlvBjS/N+uwd3R1XREQ8/XTcHxFxzTVWKAIAAADgREzlPygZCAAAAABOTAbTOp3cajSmtuVXt/77rBccMEabSQmelcBgBvYPH85A4bZtw49eWMg6Py+gBgBr74d27Mitz38+68xM/+/+2teyvulNZc9bzsp67e3GcjMpK0o92Hdi6uxs3g8tLRkpAAAAAE6EjvsAAAAAnJQMLJXO+4uLpYP7rd/OWjq8c3odE9gvnWIPRUT86q/mzrrgWaN7dOnEPyiQCACTIT8Pq8/HrHWfj/fdl7XdPrrn1VnvvdmYbgZ3XZ+1f2C/2RTYBwAAAOBU6LgPAAAAwCnJ4Nr0dAbCv/KVuD8i4tJLSwf+n/vdrDsfMlYboUyY+OQLWZ+e7fdd73pX/rvgvn1HX7+IiGi1spYg4iCl4375OYuLRh6AybnvKZ+Xc3PH93lZVqwpK9gcu3JR2X9Z937puvuM9Ub62JezPn5vv0fb7Xz95ueNFAAAAACnQnAfAAAAgHXRGwAvnWd37CgB/ku/mFUQbTQOdDvD/sETWV+4pvtA6bB/f0TENdfUBe3zdSxBxBJMrFMCiVUHYQAYv/ubz38+665dw49aXs5aJrgN7tA+aCLAq7oR/9ue9xqMQpnoeOfXsz7RcH8DAAAAwOgJ7gMAAAAwEoM6yV64O+tH3maM1sO9N2f9D2dnXTncfeCKiIiDB3sD+yVIeLyvXwkmlqBiCS4OUjoJl6Bb6TQMAFvxPmbHjt7PwZmZ4UeViXElsH/8n4P5+8r9Url/inj5+7N++OezXnDAa3MqSmD/1m9n7T/R8Rd+oaxMZMQAAAAAWE+C+wAAAACM1KAg2jkPZL3hzKyCaCfm9juzPvJov0dL0KzZPNUAfb5+JahYgoslyDhI6SxcgovHP2EAADbPfUvphF83ca3dzs+7+fn1+f07dmSQ/CtfySD5OeeceXc+/u5XZd35kNfqRAyc6Lg9IuLw4TgUEfHOd9atkAAAAAAAp0JwHwAAAIANcbSD+/aIiD/6owxInXvu1LZ8/DWvz9q4Lasgf68SOLt3f9YXL+/3XesXHOz/+pXgYgkyVisp9FcmDJQAf+lEDACb8T6lfL7NzR3f51tZYaasOLPef8/MTAb47747A/yXXloef1X3N177TNaLz/Iarvbwc1l/5y1Zn57t910nv0ICAAAAAJwMwX0AAAAANlRvB/fSgX/XrvL4Gd/M+oaXZL3uvskcpxLU3//zWZ+9Y8039HSI/eAH89/5Sqf9jXodS7CxBB3rlIBju+2dAMDpvx8pE9LKijLV/Uh/ZQWZEvQefWf23r+zfO4eO7Hgwt1ZJ3UCZAnq39XtqP/E2qmFV0REPP10ToD49KdHNdERAAAAAIYR3AcAAADgtDraif+9ERE33hifiYi48sryeAny73xT1mtvH89xOLHA2cc/vlkC8Edfv4iogo8lYDhI6Uxcgvw63AKwkZ9bO3b0fm6VCYWDbJ7O7L0TIEuAv1oBZ+1KRh9523i+jt/d2b2juDHrd/4i68ph9x0AAAAAbF6C+wAAAABsKhlIazSyo/yHPpQd5bdtK4+XIP8P35R1Zn/WrRLoLwH9L3XXGlj+tawvXLPmG/dERDzzTNwTEfGbv5k72+3NGjjrDRKWIGQJRg5SOhWXIGTpZAwAI7q/iIhqpZi6iWblc3fzdmbvnYhQnle1ckAJ8p//4ayveWPWq7v/N7jZO/OXgP4XprL+5fNZn54ddlQJ6pfXz/0FAAAAAJuD4D4AAAAAm1pdkP/o93X3lGDaxb+SddefZ93oYNqBS7J+9RNZ/+rWrC9ePuCA7RERTz2Vz+8P/zB3br3AWb5eJQhZAoSNxvCjykSEEuAvnY0BYD0+l8rnUelQX/d5VDqzlwD4Vnu+Jbhfnm8V5F/rnAeyvvpns7692b2POmtj/+7jntjY1759WRcW3EcAAAAAsJkJ7gMAAACwpfR2lt21Kz4ZEXHttXFDRMSP/dig40qn/rM+l/X8R3sfv+xrx/f7H3ll1v96UdYnL+p9/Nk7an7AXETEd74T7YiIP/7j3Lm4mP9OV4Jn4/Z6leBgCU7WKYHJdtsZD8CJf+6UCWRlBZjBwfVUJsiVCWRlRZhxGY+yIk65b3r72/O+ac+egcdty/qyq7O+Ynt3+4vd+6iPZ73wJ4f//sf/pHu/1J1Y+bfvyPqDQ93tL2RdOXw8z6bcJ5Vg/r59m3UlIgAAAADoR3AfAAAAgLHQG0zbuzdrCfiX7Y1WgoAlaFYCZuMTCDyx16cEJ0uQsgQrBymdjkuQXzAPgGGfM+Vzv3zOlPuCQUoAvAT2J+dzpneCQ/l83rUrzs/xiCcjIs47b8P+oPMjIr7//fy95fUb34mNAAAAAEwmwX0AAAAAJkJvQK0E+0qgr9Ty+D/+x/1/yn/5L1n3789aAn4liH/kyKQG80/sdSjjXYJ55fUYpIxnCVaWCREA+FyZmpqaajRyq6zsUjcxrN3Oz5P5eSN4PONbgv1r76OKd3T76L/85b37n3026xe/2Lu/TJiIyNeh2gYAAACAcSa4DwAAAACrZEBt0L+YCfqt7ziXAGAJWpbg5SBlokQJ8Av6AUz250j5/JibO77Pj7KCS1nRhfV5HcqExhLwL0rH/KuuMlIAAAAAEHGGIQAAAAAANloG+coKBc1m7q2bEFGC/vv3Z1CwLqgJwLgoE756g+J1nwNlhZarrhLYBwAAAABON8F9AAAAAOC0y0Blu51bpTNv6ZA8SKuVAc5Op7eDPwDjIq/vO3bk1gMPZF3b2X2tsiLL7Gx+viwtGUkAAAAA4HQT3AcAAAAANo0MWFaBy6x1gctGI2vpxD8zYyQBtra8nlfX96x11/d2Oz9HSof9uglgAAAAAAAbR3AfAAAAANh0MnC5vJxbpQP/wsLwo6qOzBn4rOvIDMBmk9fvViu3Op2sg1ZUKcH8ZjM/N+bnjSAAAAAAsFkJ7gMAAAAAm1bpmJy12cy9dcHMEvAsHfjn5owkwOaU1+np6ayls37ddbua2JWfD3UTuwAAAAAATj/BfQAAAABgy8iAZrudW6UTf+m4PEirlYHQTqcERI0kwOmV1+NqpZSsdSulLC5mnZ3Nz4OlJSMJAAAAAGwVgvsAAAAAwJaTgc0qwJm1LsDZaGQtnfhnZowkwMbK6291Pc5adz1ut/O6Xzrs103YAgAAAADYfAT3AQAAAIAtKwOcy8u5VTrwLywMP6rq8JwB0roOzwCcqrzetlq51elkHbQCSgnmN5t5nZ+fN4IAAAAAwFYnuA8AAAAAbHmlA3PWZjP31gU9S2C0dOCfmzOSAOsjr6vT01lLZ/2662w1ESuv53UTsQAAAAAAtg7BfQAAAABg7GTgs93OrdKJv3RwHqTVyoBpp1MCp0YS4MTk9bNa2SRr3comi4tZZ2fz+r20ZCQBAAAAgHEjuA8AAAAAjK0MgFaB0Kx1gdBGI2vpxD8zYyQBhsvrZXX9zFp3/Wy38zpdOuzXTbACAAAAANi6BPcBAAAAgLGXgdDl5dwqHfgXFoYfVXWMzkBqXcdogMmT18dWK7c6nayDViwpwfxmM6/L8/NGEAAAAACYFIL7AAAAAMDEKB2dszabubcuOFoCqKUD/9yckQQmVV4Hp6ezls76ddfFauJUXn/rJk4BAAAAAIwfwX0AAAAAYGJlgLTdzq3Sib90hB6k1crAaqdTAqxGEhh3eb2rViLJWrcSyeJi1tnZvN4uLRlJAAAAAGBSCe4DAAAAABMvA6VVwDRrXcC00chaOvHPzBhJYNzk9a263mWtu96123ldLR326yZEAQAAAACMP8F9AAAAAICuDJguL+dW6cC/sDD8qKoDdQZc6zpQA2x+eT1rtXKr08k6aIWREsxvNvM6Oj9vBAEAAAAAegnuAwAAAACsUTpEZ202c29dELUEWksH/rk5IwlsFXndmp7OWjrr113HqolOeb2sm+gEAAAAADC5BPcBAAAAAGpkILXdzq3Sib90mB6k1coAbKdTArFGEths8vpUrRyStW7lkMXFrLOzeX1cWjKSAAAAAADDCe4DAAAAABynDKhWgdWsdYHVRiNr6cQ/M2MkgdMtr0fV9Slr3fWp3c7rYOmwXzeBCQAAAACAQnAfAAAAAOAEZWB1eTm3Sgf+hYXhR1UdrTMwW9fRGmD95fWn1cqtTifroBVBSjC/2czr3vy8EQQAAAAAODmC+wAAAAAAJ6l0nM7abObeumBrCciWDvxzc0YSGJW8zkxPZy2d9euuO9XEpLy+1U1MAgAAAACgjuA+AAAAAMA6yYBru51bpRN/6Vg9SKuVgdpOpwRsjSRwqvJ6Uq30kbVupY/Fxayzs3k9W1oykgAAAAAA60NwHwAAAABgnWXgtQrAZq0LwDYaWUsn/pkZIwmcqLx+VNeTrHXXk3Y7r1ulw37dhCMAAAAAAE6U4D4AAAAAwIhkAHZ5ObdKB/6FheFHVR2yM4Bb1yEboAT2W63c6nSyDlrBowTzm828Ts3PG0EAAAAAgNES3AcAAAAAGLHSwTprs5l764KyJXBbOvDPzRlJoMjrwvR01tJZv+46UU0kyutR3UQiAAAAAADWi+A+AAAAAMAGy8Bsu51bpRN/6YA9SKuVAd1OpwR2jSRMnnz/VytzZK1bmWNxMevsbF5/lpaMJAAAAADAxhLcBwAAAAA4TTJAWwVqs9YFahuNrKUT/8yMkYTxl+/36v2fte79327ndaZ02K+bIAQAAAAAwKgI7gMAAAAAnGYZqF1ezq3SgX9hYfhRVcftDPTWddwGtqJ8f7daudXpZB204kYJ5jebeV2ZnzeCAAAAAACbg+A+AAAAAMAmUTpiZ202c29d8LYEeEsH/rk5IwlbV76Pp6ezls76de/rauJPXj/qJv4AAAAAALDRBPcBAAAAADapDOC227lVOvGXjtqDtFoZ+O10SgDYSMLml+/XaiWNrHUraSwuZp2dzevF0pKRBAAAAADYnAT3AQAAAAA2uQzkVgHdrHUB3UYja+nEPzNjJGHzyfdn9X7NWvd+bbfzulA67NdN6AEAAAAA4HQT3AcAAAAA2CIyoLu8nFulA//CwvCjqg7eGRCu6+ANbIR8P7ZaudXpZB20QkYJ5jebeR2YnzeCAAAAAABbi+A+AAAAAMAWUzpsZ202c29dkLcEgksH/rk5IwkbJ99309NZS2f9uvdhNVEn3+91E3UAAAAAANisBPcBAAAAALa4DPS227lVOvGXDt2DtFoZIO50SqDYSML6y/dXtfJF1rqVLxYXs87O5vt7aclIAgAAAABsbYL7AAAAAABjIgO+VeA3a13gt9HIWjrxz8wYSTh1+X6q3l9Z695f7Xa+j0uH/boJOAAAAAAAbBWC+wAAAAAAYyYDv8vLuVU68C8sDD+q6giegeO6juBAP/n+abVyq9PJOmhFixLMbzbzfTs/bwQBAAAAAMaT4D4AAAAAwJgqHbuzNpu5ty4YXALGpQP/3JyRhMHyfTI9nbV01q9731QTa/L9WTexBgAAAACArU5wHwAAAABgQmRAuN3OrdKJv3T8HqTVykByp1MCykYSSmC/Wqkia91KFYuLWWdn8/24tGQkAQAAAAAmg+A+AAAAAMCEycBwFSDOWhcgbjSylk78MzNGkkmU53/1fsha935ot/N9Vzrs102YAQAAAABg3AjuAwAAAABMqAwQLy/nVunAv7Aw/Kiqw3gGmOs6jMN4yPO91cqtTifroBUoSjC/2cz32fy8EQQAAAAAmGyC+wAAAAAAE650AM/abObeuqBxCSyXDvxzc0aScZLn9fR01tJZv+48rybC5PupbiIMAAAAAACTQnAfAAAAAIAeGThut3OrdOIvHcQHabUy4NzplMCzkWQryvO3Wlkia93KEouLWWdn8/2ztGQkAQAAAABYTXAfAAAAAIC+MoBcBZKz1gWSG42spRP/zIyRZCvI87U6f7PWnb/tdr5PSof9ugkuAAAAAABMKsF9AAAAAACGykDy8nJulQ78CwvDj6o6lmcguq5jOZweeX62WrnV6WQdtGJECeY3m/m+mJ83ggAAAAAAHA/BfQAAAAAAjkvpKJ612cy9dcHlEoAuHfjn5owkp1Oeh9PTWUtn/brzspq4kud/3cQVAAAAAADoJbgPAAAAAMBJyQBzu51bpRN/6Ug+SKuVgelOpwSojSQbIc+3aiWIrHUrQSwuZp2dzfN9aclIAgAAAABwMgT3AQAAAAA4JRlorgLOWesCzo1G1tKJf2bGSDIKeX5V51vWuvOt3c7zunTYr5uQAgAAAAAAwwnuAwAAAACwLjLgvLycW6UD/8LC8KOqDugZsK7rgA7HJ8+nViu3Op2sg1Z4KMH8ZjPP4/l5IwgAAAAAwHoS3AcAAAAAYF2VDuVZm83cWxeELoHq0oF/bs5IciLyvJmezlo669edR9VEkzxf6yaaAAAAAADAyRHcBwAAAABgpDIQ3W7nVunEXzqcD9JqZQC70ymBbCNJP3l+VCs3ZK1buWFxMevsbJ6fS0tGEgAAAACAURLcBwAAAABgQ2RAugpMZ60LTDcaWUsn/pkZI0lECexX50fWuvOj3c7zsHTYr5tAAgAAAAAA60NwHwAAAACADZWB6eXl3Cod+BcWhh9VdVTPwHZdR3XGVb7+rVZudTpZB63IUIL5zWaed/PzRhAAAAAAgNNBcB8AAAAAgNOidDzP2mzm3rpgdQlolw78c3NGcrzl6zw9nbV01q973auJIXl+1U0MAQAAAACA0RLcBwAAAABgU8iAdbudW6UTf+mYPkirlYHuTqcEvI3keMjXs1ppIWvdSguLi1lnZ/N8WloykgAAAAAAbAaC+wAAAAAAbCoZuK4C2FnrAtiNRtbSiX9mxkhuTfn6Va9n1rrXs93O86Z02K+b8AEAAAAAABtLcB8AAAAAgE0pA9jLy7lVOvAvLAw/qurQngHwug7tbBb5erVaudXpZB20gkIJ5jebeZ7MzxtBAAAAAAA2M8F9AAAAAAA2tdJBPWuzmXvrgtol8F068M/NGcnNJV+X6emspbN+3etUTeTI86FuIgcAAAAAAGwOgvsAAAAAAGwpGdhut3OrdOIvHdgHabUyIN7plMC4kTw9cvyrlRGy1q2MsLiYdXY2X/+lJSMJAAAAAMBWIrgPAAAAAMCWlAHuKtCdtS7Q3WhkLZ34Z2aM5MbI8a7GP2vd+Lfb+TqXDvt1EzQAAAAAAGBzEtwHAAAAAGBLy0D38nJulQ78CwvDj6o6vmegvK7jOycrx7fVyq1OJ+ugFQ9KML/ZzNd1ft4IAgAAAAAwDgT3AQAAAAAYC6Uje9ZmM/fWBb9LgLx04J+bM5KnJsdxejpr6axfN67VxIt8/eomXgAAAAAAwNYiuA8AAAAAwFjKAHi7nVulE3/p6D5Iq5WB806nBNCN5PHJ8apWMshat5LB4mLW2dl8vZaWjCQAAAAAAONIcB8AAAAAgLGWgfAqIJ61LiDeaGQtnfhnZoxkfzk+1XhlrRuvdjtfl9Jhv25CBQAAAAAAbG2C+wAAAAAATIQMiC8v51bpwL+wMPyoqoN8BtTrOshPjhyPViu3Op2sg1YoKMH8ZjNfh/l5IwgAAAAAwCQR3AcAAAAAYKKUDu9Zm83cWxckL4H00oF/bm7Sxi2f9/R01tJZv24cqokSOd51EyUAAAAAAGA8Ce4DAAAAADDRMlDebudW6cRfOsQP0mplgL3TKYH2cR2ffH7VygNZ61YeWFzMOjub47u05EwDAAAAAGCSCe4DAAAAAECUAH8VOM9aFzhvNLKWTvwzM+MyHvl8queXte75tds5jqXDft0ECAAAAAAAmAyC+wAAAAAAsEoGzpeXc6t04F9YGH5U1ZE+A+91Hek3r/z7W63c6nSyDlpRoATzm80ct/l5ZxAAAAAAABxLcB8AAAAAAPooHeOzNpu5ty6YXgLupQP/3Nxmf575d05PZy2d9ev+7mpiQ45P3cQGAAAAAACYbIL7AAAAAABwHDKg3m7nVunEXzrOD9JqZSC+0ykB+c3yfPLvqVYKyFq3UsDiYtbZ2RyPpSVnBgAAAAAA1BPcBwAAAACAE5CB9SrAnrUuwN5oZC2d+GdmTtffn7+/+nuy1v097XY+79Jhv27CAgAAAAAAsJrgPgAAAAAAnIQMsC8v51bpwL+wMPyoqsN9BujrOtyvn/x9rVZudTpZB60AUIL5zWY+z/l5rzgAAAAAAJw8wX0AAAAAADgFpQN91mYz99YF3UtgvnTgn5tb778rf+70dNbSWb/u91QTEfL51E1EAAAAAAAAjofgPgAAAAAArKMMvLfbuVU68ZcO9oO0Whmw73RK4P5kf38eX3X2z1rX2X9xMevsbP79S0teSQAAAAAAWD+C+wAAAAAAMAIZgK8C8VnrAvGNRtbSiX9m5nh/X35/dXzWuuPb7fw7S4f9ugkGAAAAAADAyRDcBwAAAACAEcpA/PJybpUO/AsLw4+qOuZnIH9wx/x8vNXKrU4n66CO/SWY32zm3zU/7xUCAAAAAIDRE9wHAAAAAIANUDraZ202c29dcL4E8EsH/rm5rNPTWUtn/bm54T+nmjiQv79u4gAAAAAAALCeBPcBAAAAAOA0yAB9u51bpRN/6Yg/SOmsf/hw1sGd+NPiYtbZ2fx9S0tGHgAAAAAANp7gPgAAAAAAnEYZqK8C9lnrAvbnnDP88XY7f27psF83IQAAAAAAABglwX0AAAAAANgEMmC/vJxbpQP/wYPHd/SLL2b9N/8mf878vBEFAAAAAIDNQ3AfAAAAAAA2gampqampqenp3Pr857NeeunxHX1G99/7/+f/OX/O3JwRBQAAAACAzUNwHwAAAAAATqMM2u/YkVsPPJB1167hR73wwvDHW638uZ1O74QAAAAAAADgdBDcBwAAAACA0yAD9Y1Gbu3fn3VmZvhR7XbW7duzLi0N//7q5+fvq/v5AAAAAADAKAjuAwAAAADABsoAfauVW51O1kEd8Y8cydpsrqysrKyszM9nXV7O/VddlXVhYfhvrTr65++v6+gPAAAAAACsJ8F9AAAAAAAYoQzKT09nLZ315+aGH1UF8zOof2wwP/cfOZK12cy98/PDf26ZIFA68Nf9HQAAAAAAwHoQ3AcAAAAAgBHIYHzV6T5rXaf7xcWss7MZyF9aOt7fl9/fbudW6cRfOvYP0mrl39nplAkGXjkAAAAAAFh/gvsAAAAAALCOMgDfaORW6bA/MzP8qHY7g/elw35d4H6wPL6aAJC1bgJA9ffm31/39wIAAAAAACdCcB8AAAAAANZBBt5brdzqdLIO6mBfgvnNZgbt5+fX++/Jn7u8nFulA//CwvCjqhUC8vnUrRAAAAAAAAAcD8F9AAAAAAA4CRlsn57OWjrrz80NP6oK0mewvi5If+pKB/+szWburZsoUCYclA78dc8LAAAAAAAYRnAfAAAAAABOQAbZq870Wes60y8uZp2dzQD90tLp+vvz97fbuVU68ZcVAAZptfJ5dzplwoIzAQAAAAAAjp/gPgAAAAAAHIcMrDcauVU67M/MDD+q3c6gfOmwXxeQ3zj591QTCrLWTSionn+OR93zBwAAAAAAIgT3AQAAAABgqAyot1q51elkHdRxvgTzm80Mxs/Pb/bnl3/n8nJulQ78CwvDj6pWHMjxqVtxAAAAAAAAJpvgPgAAAAAArJJB9OnprKWz/tzc8KOq4HsG4euC75tPWREga7OZe+smHpQJDKUDf904AQAAAADAZBLcBwAAAACAKIH9qpN81rpO8ouLWWdnM/C+tDQu45HPp93OrdKJv6woMEirlePY6ZQJEM4sAAAAAAAQ3AcAAAAAYMJlwLzRyK3SYX9mZvhR7XYG20uH/bpA+9aVz6+aoJC1boJCNZ45vnXjCQAAAAAA401wHwAAAACAiZSB8lYrtzqdrIM6xJdgfrOZQfb5+Ukbr3zey8u5VTrwLywMP6pawSDHu24FAwAAAAAAGE+C+wAAAAAATIQMjk9PZy2d9efmhh9VBdUzuF4XVB9/ZYWBrM1m7q2byFAmRJQO/HXjDgAAAAAA40VwHwAAAACAsZZB8arze9a6zu+Li1lnZzOgvrRkJPvL8Wm3c6t04i8rFAzSauXr0umUCRVGEgAAAACAcSa4DwAAAADAWMpAeKORW6XD/szM8KPa7Qyilw77dQF0ihyvasJD1roJD9Xrk69X3esDAAAAAABbk+A+AAAAAABjJQPgrVZudTpZB3V0L8H8ZjOD5/PzRvDU5DguL+dW6cC/sDD8qGpFhHz96lZEAAAAAACArUVwHwAAAACALS2D3tPTWUtn/bm54UdVwfIMmtcFyzlRZcWCrM1m7q2bGFEmWJQO/HWvIwAAAAAAbA2C+wAAAAAAbEkZ7K46tWet69S+uJh1djYD5UtLRnJj5Hi327lVOvGXFQ8GabXyde50ygQNIwkAAAAAwFYkuA8AAAAAwJaSAe5GI7dKh/2ZmeFHtdsZHC8d9usC44xKjn81gSJr3QSK6vXO17/u9QYAAAAAgM1FcB8AAAAAgC0hA9utVm51OlkHdWAvwfxmM4Pi8/NGcHPJ12V5ObdKB/6FheFHVSss5PlQt8ICAAAAAABsDoL7AAAAAABsShnMnp7OWjrrz80NP6oKgmcwvC4IzulWVkDI2mzm3rqJFmXCRunAX3deAAAAAADA6SW4DwAAAADAppJB7Kqzeta6zuqLi1lnZzMAvrRkJLemfP3a7dwqnfjLCgqDtFp53nQ6ZcKHkQQAAAAAYDMR3AcAAAAAYFPIwHWjkVulw/7MzPCj2u0MepcO+3UBb7aKfD2rCRlZ6yZkVOdPnk915w8AAAAAAGwMwX0AAAAAAE6rDFi3WrnV6WQd1DG9BPObzQx2z88bwfGWr/Pycm6VDvwLC8OPqlZsyPOrbsUGAAAAAAAYLcF9AAAAAAA2VAapp6ezls76c3PDj6qC2xnkrgtuM27KigpZm83cWzdxo0wAKR34684zAAAAAAAYDcF9AAAAAAA2RAanq07oWes6oS8uZp2dzcD20pKRJKIE+dvt3Cqd+MuKDIO0WnkedjplAomRBAAAAABgIwjuAwAAAAAwUhmQbjRyq3TYn5kZflS7ncHs0mG/LpDNpMrzo5rgkbVugkd1Pub5WXc+AgAAAADAqRHcBwAAAABgJDIQ3WrlVqeTdVCH8xLMbzYziD0/bwQ5EXneLC/nVunAv7Aw/KhqBYg8X+tWgAAAAAAAgJMjuA8AAAAAwLrI4PP0dNbSWX9ubvhRVdA6g9d1QWsYrqzQkLXZzL11E0HKhJLSgb/uvAUAAAAAgBMjuA8AAAAAwCnJoHPVuTxrXefyxcWss7MZsF5aMpKMQp5f7XZulU78ZYWHQVqtPK87nTIhxUgCAAAAAHAqBPcBAAAAADgpGWhuNHKrdNifmRl+VLudQerSYb8uQA3rI8+3asJI1roJI9X5ned73fkNAAAAAAD9Ce4DAAAAAHBCMsDcauVWp5N1UEfyEsxvNjM4PT9vBDmd8jxcXs6t0oF/YWH4UdWKEnn+160oAQAAAAAAvQT3AQAAAAAYKoPK09NZS2f9ubnhR1XB6AxK1wWjYWOVFR+yNpu5t25iSZmgUjrw170PAAAAAAAgCe4DAAAAANBXBpOrTuNZ6zqNLy5mnZ3NQPTSkpFkK8jztd3OrdKJv6wYMUirle+TTqdMcDGSAAAAAAD0I7gPAAAAAECPDCA3GrlVOuzPzAw/qt3O4HPpsF8XeIbNKc/fagJK1roJKNX7Jd8/de8XAAAAAAAmjeA+AAAAAAARUQL7rVZudTpZB3UQL8H8ZjODzvPzRpBxkuf18nJulQ78CwvDj6pWqMj3U90KFQAAAAAATArBfQAAAACACZXB4unprKWz/tzc8KOqIHMGm+uCzLC1lRUksjabubduokqZ8FI68Ne9rwAAAAAAGHeC+wAAAAAAEyaDxFVn8Kx1ncEXF7POzmaAeWnJSDKJ8vxvt3OrdOIvK1AM0mrl+67TKRNmjCQAAAAAwGQR3AcAAAAAmBAZGG40cqt02J+ZGX5Uu51B5dJhvy6gDJMh3w/VhJasdRNaqvdfvh/r3n8AAAAAAIwLwX0AAAAAgDGXAeFWK7c6nayDOn6XYH6zmcHk+XkjCIPl+2R5ObdKB/6FheFHVSte5PuzbsULAAAAAAC2OsF9AAAAAIAxk0Hg6emspbP+3Nzwo6rgcQaR64LHwGplRYqszWburZv4UibQlA78de9TAAAAAAC2KsF9AAAAAIAxkcHfqpN31rpO3ouLWWdnM3C8tGQk4dTl+6ndzq3Sib+saDFIq5Xv406nTMAxkgAAAAAA40FwHwAAAABgi8uAb6ORW6XD/szM8KPa7QwWlw77dYFi4GTk+6uaIJO1boJM9X7O93fd+xkAAAAAgM1OcB8AAAAAYIvKQG+rlVudTtZBHbpLML/ZzCDx/LwRhI2T77vl5dwqHfgXFoYfVa2gke/3uhU0AAAAAADYrAT3AQAAAAC2iAzuTk9nLZ315+aGH1UFhTM4XBcUBkaprHCRtdnMvXUTacqEnNKBv+59DwAAAADAZiO4DwAAAACwyWVQt+q8nbWu8/biYtbZ2QwILy0ZSdh88v3ZbudW6cRfVsgYpNXK60KnUyb0GEkAAAAAgM1NcB8AAAAAYJPKQG6jkVulw/7MzPCj2u0MApcO+3UBYGAzyPdrNeEma92Em+r6kNeLuusDAAAAAACni+A+AAAAAMAmkwHcViu3Op2sgzpql2B+s5nB3/l5IwhbV76Pl5dzq3TgX1gYflS1IkdeP+pW5AAAAAAAYKMJ7gMAAAAAnGYZtJ2ezlo668/NDT+qCvZm0Lcu2AtsJWXFjKzNZu6tm5hTJviUDvx11xEAAAAAADaK4D4AAAAAwGmSwdqqU3bWuk7Zi4tZZ2cz0Lu0ZCRh/OX7vd3OrdKJv6y4MUirldeZTqdMEDKSAAAAAACnh+A+AAAAAMAGywBto5FbpcP+zMzwo9rtDO6WDvt1gV1gHOX7v5rAk7VuAk91vcnrT931BgAAAACA9Sa4DwAAAACwQTIw22rlVqeTdVAH7BLMbzYzqDs/bwSBIq8Ly8u5VTrwLywMP6pa4SOvR3UrfAAAAAAAsF4E9wEAAAAARiSDsdPTWUtn/bm54UdVQdwM5tYFcYFJVlbgyNps5t66iT5lwlDpwF93XQIAAAAA4FQJ7gMAAAAArLMMwladrbPWdbZeXMw6O5sB3KUlIwmcqLx+tNu5VTrxlxU8Bmm18rrV6ZQJR0YSAAAAAGB9Ce4DAAAAAKyTDLw2GrlVOuzPzAw/qt3OoG3psF8XsAWol9eTakJQ1roJQdX1K69nddcvAAAAAACOl+A+AAAAAMApyoBrq5VbnU7WQR2rSzC/2cxg7fy8EQRGJa8zy8u5VTrwLywMP6paMSSvb3UrhgAAAAAAUEdwHwAAAADgBGWQdXo6a+msPzc3/KgqOJtB2rrgLMD6KSt6ZG02c2/dxKEyAal04K+7zgEAAAAAMIjgPgAAAADAccrgatWJOmtdJ+rFxayzsxmYXVoyksDpltejdju3Sif+siLIIK1WXgc7nTKByUgCAAAAABwfwX0AAAAAgBoZUG00cqt02J+ZGX5Uu53B2NJhvy4QC7Dx8vpUTTDKWjfBqLoe5vWx7noIAAAAAIDgPgAAAADAABlIbbVyq9PJOqjDdAnmN5sZhJ2fN4LAVpHXreXl3Cod+BcWhh9VrUCS18u6FUgAAAAAACaX4D4AAAAAQFcGT6ens5bO+nNzw4+qgq4ZfK0LugJsXmWFkKzNZu6tm4hUJjSVDvx1100AAAAAgMkjuA8AAAAATLwMmlado7PWdY5eXMw6O5sB16UlIwmMm7y+tdu5VTrxlxVGBmm18rra6ZQJUUYSAAAAAJh0gvsAAAAAwMTKQGmjkVulw/7MzPCj2u0MspYO+3UBVoCtL6931YSlrHUTlqrra15v666vAAAAAADjS3AfAAAAAJg4GSBttXKr08k6qCN0CeY3mxlcnZ83gsCkyuvg8nJulQ78CwvDj6pWNMnrb92KJgAAAAAA40dwHwAAAAAYexkUnZ7OWjrrz80NP6oKpmZQtS6YCjA5yoojWZvN3Fs3salMkCod+OuuwwAAAAAA40NwHwAAAAAYWxkMrTo9Z63r9Ly4mHV2NgOpS0tGEmC4vF6227lVOvGXFUsGabXyOt3plAlWRhIAAAAAGFeC+wAAAADA2MkAaKORW6XD/szM8KPa7Qyelg77dYFTANbK62c1ASpr3QSo6nqd1++66zUAAAAAwNYjuA8AAAAAjI0MfLZaudXpZB3UwbkE85vNDJrOzxtBgPWR19Xl5dwqHfgXFoYfVa2QktfzuhVSAAAAAAC2DsF9AAAAAGDLymDn9HTW0ll/bm74UVWQNIOldUFSAE5WWcEka7OZe+smSpUJV6UDf911HQAAAABg8xPcBwAAAAC2nAxyVp2Zs9Z1Zl5czDo7mwHSpSUjCbCx8vrbbudW6cRfVkAZpNXK636nUyZsGUkAAAAAYKsR3AcAAAAAtowMbDYauVU67M/MDD+q3c6gaOmwXxcQBWDU8npcTajKWjehqrr+5+dB3fUfAAAAAGDzENwHAAAAADa9DGi2WrnV6WQd1HG5BPObzQyGzs8bQYDNKa/Ty8u5VTrwLywMP6pacSU/H+pWXAEAAAAAOP0E9wEAAACATSeDmNPTWUtn/bm54UdVwc8MgtYFPwHYLMqKKFmbzdxbN/GqTOAqHfjrPicAAAAAAE4fwX0AAAAAYNPI4GXVSTlrXSflxcWss7MZ+FxaMpIAW1tez9vt3Cqd+MuKKoO0Wvk50umUCWBGEgAAAADYLAT3AQAAAIDTLgOWjUZulQ77MzPDj2q3M9hZOuzXBToB2Gry+l5N0MpaN0Gr+jzJz5e6zxMAAAAAgNET3AcAAAAATpsMVLZaudXpZB3UIbkE85vNDHLOzxtBgMmQ1/3l5dwqHfgXFoYfVa3gkp83dSu4AAAAAACMzlT+Q6eBAAAAAGAyZHCvBPlKQHxtkO+nf7r/0YcOZf3Wt7KWjr8lUL60pPP78Yx/GffPf77/+K9VgprveleOb12nZQAm63Nlbi63ykSwOvPz+XnSbhvB4xnfsmJBqWvvo97ylqw/9EO9R//N32T90z/t/Tyvau+EDAAAAAAYb4L7AAAAAIyF3kD43r1ZSyC81EGd3EdlcbG37ts3qQG13gkTJbBfAoB141cC+yZEADDsc6Z83pfPmbrP/dKxvwT5J+9zJset3DeVz+myXfc5vd7KxLy1900m7AEAAAAwHgT3AQAAANhSeju/7t0bEZ+MeOMbI+KGiD17hhy5LevLrs565s9mPfejWc//eNYLf7L/8U/9IOvyVVn/9h1Zf9Dtwv/cz2V98fKap7An4rHHIuKeiN///dw1vsG0fL0ajdwqnZDrgpTtdo7H/LwzHoCTv08oAf4SSB+kfP6WiWLjM8Gu/8TGHTvyfuRnfibvR84+e/BPOPPurC/5P7v3S4/2Pn7Z14b/BQ++qXf7yYuy/t1/n/WFa+rvm555pve+aXExX6d9+5zxAAAAAGwlgvsAAAAAbGq9we9ShwXwznkg64+8NOtb9me9+KyN/cvvuj7rw7+e9XuzWQcG+7dHHD4cEYci/vAPc1cJsG+9DsD5upWg/tzc8O8uz690PC4dkAHgVD6HSmC9fB6V+4i6z6MS4C+d37fa8y4rD5TnWwL7/ZRg/syHsv7Eb2fd+dDG/uUHLsn61U9k/Zt/kbU22B/VygnlvmnyVjYCAAAAYGsQ3AcAAABgU1kVOLsi4pOfjIj7Iy69dNV3bMt6/oezXvwrWXf9edYLDmzuZ7g2mPZXt2Y9JtC/PeKppyLiUMRv/dZm70DfG5AsHY5LcHCQEqwrAcnxW3EAgM30OVUmkpUgf50yoazd3tzPq6wwUJ5fvwkKZWLjq7srDr292b2POmtzv3IPP5f1S52sj+3O+uwdg48R5AcAAABgcxLcBwAAAOC0ysDZjh0R8d6IT30qIj4TceWV1Xec8c2sb3hJ1uvuG8+RKIH+P7on6zGBtD0Rjz0WEfdE3HbbZulMv+r1iyqwXwKEg5QOxiWwv/VWFABgK993lIll5XOrTDwbpHzeliD/6fvc6p0oV4L6q1e2KRMcX/P6rI3bsm72iY0n6rs7s9759axPrJ2s8N6IH/wg7yt/4zdy19ZdyQgAAACA8SC4DwAAAMCG6g2clY63qzvDrg2cfeRtkzlS996c9UvdsOAL16z5hisiDh6MiPsjbrgh/52vBOI36nUsr1t5HeuCjyUwt3lXDgBgku5HykSzEuAvE9EGKSvDlIlnG9fJPf/eVis//6+7Lj//zzmn+o5Xde8Xrn0m62bvpL/eSmf+u87OekyQf9VKRr/2a5t9JQUAAAAAxpPgPgAAAAAbYlVn9vO7HdefjDjvvOo7LtyddVw7w56qT78567f+LuuLlx/7PaUT8OiCaKuCg9Hb4bef0tG2/F2nf4UAADj2c23YhMJhn28lwL/+E+d6/679+7Ounljw8vdnbf5w1kkL6tcpEyD3/3zWY1Yyioh9+7pj2NSJHwAAAICNILgPAAAAwEj1dmbvdKpHBM5Ozce+nPXxe499rATkS2D+5INovcHB0pF4167hR5UOxCXQWDoUA8BWuG8pE9NKkL/O+k2cWzXRcU/EF74QEfdEvPa11YpE/6TbUX/3LV6tE1GC/P+h25F/5XD3gVUrGF1zzUavpAAAAADAZBHcBwAAAGAkBndmf1U3VH7b80ZpPdx1fdb7Xp21XxDtrW890QD/quBgVIH9mZnhR5WOwyWwr3MtAFv5PqZMVCufg2Ui2yAnP3Euf9/evRGxJ+Izn4mIeyLOPjvizLvzO256XVYrEp2aA5dk/YMnsr5wTXXf9PTTvfdNJh4CAAAAsL4E9wEAAABYF72d2Utn/b17q++47KGs191ntEahBNHuekXWFy/vPnB+xPe/HxFPRuzaVRdE610hoUy8qAsqttv5c+fnvQ4AjN/9TZm4VgL8ZWLbIOVztkxkG9zBvX6i4/v+YVaB/fX13Z1ZP/7ZrM/ecez3NJv5+pUJGQAAAABwas4wBAAAAACcit7A/v79WffujZjall+/45VZBfZHa2d3YsQtfy9r6dAbT0acd15EXBHxla/0dtJf+zqW4GCZeDEosF86CJdAm8A+AOOpN3h/1VVZ64Lc5XP2gQd6O/ev/dwtn7erA/s/elHWsjKRwP5olHH9X7uTMi7cfez3dDq990cAAAAAcGp03AcAAADglGSgqXSg3bu3Coy/+1VZS6Cc0+PGl2Z9ottFP7ZHPPVURByKuPLK3PXJT2Y9NljYqwQXSwfhwZ37AWD8739K4P54g91loluZANfpVBMd3/zXWa+93eieTp9+c9YHLzn2MR34AQAAADg1gvsAAAAAnJTeDqRzc1Xw7Od+N6vA/ubyq93Q/bN3dHdsjzh8OCIORWzbNvzYxcWsJbBfAocA4H6o6qhfJjIOWrHmm9/Mevnl1b7LuvdLVibaXG6/M+sjj3Z3XBHx9NMRcX/EW99qAiMAAAAAJ+MMQwAAAADAiciAWqPbvb10mo2I+CfPZBXY35w+/PNZy4oIqwP7hw71P6bdzmDaVVcJ7APAsfLzsUxwm53NujbQ/Z3vRMQVEa97XbXvwt1ZBfY3p+vfl/VVpbv+/RHnnBMRcxH33JP3w4MmaAAAAABAfzruAwAAAHBcMqC0Y0dE7In4kz+JiHsizj5bp9it5sAlWT/3nqwrh6vHSoD/3/yb/HfDhQXjBQAner9UAt033RQR2yPe/vaIOBTxoz8acc4D+din/sxobSW//OqsL1zT3XFFxMGDKysrB1ZWLrvM+AAAAABwPHTcBwAAAGCoVQG08yMWF+NoYL90IBXY31rKighlhYTVtm83PgBw8npXqHn96+NoYL+seHPDmUZpK7qpu1rCGd/s7rg/4tJL8z650zE+AAAAABwPwX0AAAAAjkOrFRFPRpx3XhU8u+1547KV7b4la1kx4ajzI9rt3o7BAMDxyM/PRiO3du2KmNqWX//y4awXHDBKW1F53a79QfeV3lY91mjk675rl3ECAAAAYBjBfQAAAAD6ygDSzExulQBaRBU8YzyUFRNe/v7uju4EjYiIuTnjAwAnZHvEhz5UbV76xawXn2VoxkFZueg1r1/zwHsjbrzR+AAAAAAwjOA+AAAAAIO8N+Izn6k2L9ydVfBsPF312TU79kT80i/pvA8A9fLzcm4uIg5FbNsWccY385EyQY7x0rgta3md4zMRV17Zu+ICAAAAAPQS3AcAAACgRwaOdu2KbgApYmpbPlICSoyn3bdkPeeB7o57Is4+O79stYwPAAy6b5qejog9vR3Xd19ldMbZBQeyvuElax7Yo/M+AAAAAIMI7gMAAACw1nt7A0eveX3WElBivP3LPz12X6ORwcSZGeMDAGvNzcXRCW8vf3/uKxPiGG9lRYWjnffviXjta3XeBwAAAKAfwX0AAAAAIqJ0jG004min/RJA0ml/slx8VtZXLRz7mM77AFDdN83MRMT2iF/8xeqRqz5rdCbRzjet2bE94hOfWLUiAwAAAADESwwBAAAAAJXVnUHf0P23owvuG+/nfOCSrF/9RP/H//6jWX/it7PufGgyzoX3/cOsN23LunI4Yu/eElRcWVlZWVlZXvaeAWDC75sORZx7bjXhbffzk/Hcy/3Tn/9C1v96Uf/vu+xr3XEZ8xUIrr29Ox7de6Nn78jzIiJi796sCwveMwAAAACTTcd9AAAAgAm3qmNsROzYETG1Lb++bkwD+/fenPUX/1HWf/fmrE9e1Fv/6tasjzza+33luNvvHO8z44IDWc//8LGPlQAaAEysKyJ+6qeqzTd9aLyf7l3X994H3fWKrP/lA/2/v9xPffF7WZufyvqxL2f97s7xHKft/+Ox+3bt8nYBAAAAIELHfQAAAAAiojdQdDSoPWYdY0tQ7PFugOzCm7I2vpW1BNWP+k9Z7n1l1i91u6S+cHnWR7rf9suvznrT6wb8nC3u4l/J+qdlx3sj3va2/LLd9t4BYJL0Tni89NJqwuPuD4znMy73T3/V7Zy/801ZS4f5o97W//hPd1cqerDbof/xw1lv7k6QvLa7f1xWNLp6pft8V+0rKxZNT+eKRUeOeCcBAAAATCYd9wEAAAD4ZMTb315tvuaN4/X0Pt3tlP+dv8j6z7srCXykGzCrC9rvviVrCeafeXfv4y9ck/XWb2cdtw6yxwTzPhNx5ZUlgObtA8DkWb3yTL+VacZB6bD/N/8i6y1/b8B9QY2ygtOFu3v3v9idCFk694/L/VO5rzzngWMf03kfAAAAYNIJ7gMAAABMqFXB6xsi9uypHimdQre6EgA7+I6sF70068l2dC1BrF8+3P/xEuBfuHE8z5h+AbTVwUUAmBSrA9hlZZpxc+Brvfc3N/9/WcuEyBN15Qf77y8B/s+N2T3Fq392+HkDAAAAwCQS3AcAAACYaKsDRCWYXdeBfqsoAfqpL2S9/n3r83MvPqt3vNYqnf3HrfP+j7x0+PkDAOOrd6WZ1Z9/J9qBfrMr9y8lUF+U7QcvObmfWzdx8rHd4zWOb2+u2XFFxLvf7Z0EAAAAMNkE9wEAAAAm2urgWb/OoFvZkxdlLUGzxr/K+qvL6/Pz+wXZIyJWDmdd/InxGs9jVmK4IuKnfsp7CIDJsXqlmUET+CCimuh55t3dHfdHnHNOTgCxYhEAAADApBLcBwAAAJhoq4P7x3QG3eKevWP4/k+/+dR+/oU/Ofzx5avGazzLSgz9Amg67wMwCWZmqq8HTeAbl8/7Vy0MuP85yc74Dz83/PFXbB/P8fyhf3vsvh07vJcAAAAAJtNLDAEAAADAJFsdQCudQcfFGd/MWjrusz5KAO3xVfump40LAONvdeD66AS+W8bzud72fNYD92V95TdO7X7xwQ8Pf/w1b+x+cd+Y3Wvvd98EAAAAQKHjPgAAAMCEyQ7pq4NnL3//eD7TNwxoWlE6xl+94mxYLzrHAjD2tke87nXV5o9/ZTKe9s6Hsp7qBM+Hf73//jLR8rr7xnP8zn3FsftWT5wFAAAAYJII7gMAAABMpEno9FkCYP/69qzveGXW3/jrrBccOLWf/8grhz9eOqyOm37PS+dYAMbeoYht26rNU72PmBTf3Zn1yY/3f3z3VeP9/HevXZFhe8SP/7jzAgAAAGAyCe4DAAAATKTVHdLPf3S8n2vpEHtMcOoU/fXv9d8/tS3rrj8fz/HUORaAyZErFa3+nBvXlYpG5c6vZ1053HufdNlDo7k/27RnUvd5x6GIc891XgAAAABMppcYAgAAAIBJtLpD+t8vwf23GZfj8fBzWZ+e7f/4a16fdVw78ZaA3Rf/VbXvda/LYOOuXc4PAMbPZZcZg+N1781Zv/ofe++XyoSHd+7JuvO+yRqXl12d9dk7IsqEkB07VlZWVlZWlpacNwAAAACTQXAfAAAAYOL96PeMwYm46+z++8+8O+tH/nryxmTbtqz79zs/ABhvR1cqmvDVZpqfylo66R+jG9g/54Gs//JPs178kHOoWD2RFgAAAIBJILgPAAAAAMflwCVZn3hz7/6pbVl/+XB3x1nGCgAYb50P9N9fVib606uyfuvvsv4v12c9pvO+ID8AAAAAE+MMQwAAAAAAw3x3Z9Y/eKJ3fwns/9zvZr1YYB8AmHDlfui6+7Le8veylpWJnr0j6+fek/XTbzZmAAAAAEwKHfcBAAAAJt7jf9L94j5j0c+dX8/6QiPr2sC+TrGVdtsYADB+/sE/yPrud0c89dHuzj8zLsfjggNZ335z1i92968czvpgd0Wju7qB/2tvN2YAAAAAjCvBfQAAAICJ9+SHu1+8zVisVjrAPtENlAnspwOXHLtvcXFlZWVlZWV+3nkDwDiZmpqamprasSO33v3uiBd+r/vQjNE5EbtvyfqlV2d94Zrex+/r7t/VXemoBP7HxXM/1/3ijoiIvG9aXHReAAAAAEyWMwwBAAAAwCRaHRT623cYj9VKYL90gD3z7qy3/vusk95h/6l/duy+I0ecNwCMowxYLy2tum/6glE5FT/0bweM9OGsn9s7ns/7xcu99gAAAAAI7gMAAABMvB8cMgYRVSf5tYH9m16Xddw6v56sB9907L7lZeMCwJjbHvHUU1XAnNF4bPd43l+uptM+AAAAwKQS3AcAAACYMNk5tqfj/oR3ji2Bqs+9J+urFrL+xl9nPdHA/sPP9dZJILgPwNg7FPGNb1Sb9948nk+zrDzU/FRv/diX1+fnX/a14Y+P232plYoAAAAAqAjuAwAAAEyu8yO+//2qc+x3d07W0y/B+hLYP//DWW97/tR+7t1/0lvHzZMXHbtPcB+ASbD68+6pH4znfVFZeajcH5b6+L1Z+3WQPxHjNm51Hnml+yYAAAAACsF9AAAAgMn1ZMT+/dXm4k9MxtMuExR+Y1vW9QrsHx3WbrC9rqPsVtWvE+7SkrcTAONvdeD64V8fs+f28eP7vseuOsXfU3P8y64er3H9698bfh4BAAAAMEkE9wEAAAAm2urA9bgF0NYqgf1bv531vO9lXa/AfvHsHVlnPjxe43fX9VlL5908f1ZWVlZWVo4c8V4CYPzt21d9/eTHx+u51d23TG3LetmIn/dr7x2v+86nZ4efRwAAAABMkpcYAgAAAIBJVoJDrdaqANoHxvO53vn17hevzPKmD2Vdr3zYg2/q3b74rPEav6MTOxrHnj8AMN5yotry8tTU1D+bmnrssYiVeyJe+9qIA5fkd+x8aGs/w3LfcsY3u8+42/n+Na/PeuUHu993is/zr26NvjdgZWLAz5V7iwNbezz7rWS1b58JjwAAAACTTXAfAAAAYEKtCqB9amrqP//niJUbIn7sxyLuvTm/Y/ct4/FMb3xp1icavfu/uN6/qBtAO/Pu7vZfj9cZ06+zsOA+ABPnnojf//38cm4u4qufyK93vm08nt7uq7r3Sd2Vic7v3jDtvO/Ufu6n35z1xUv6P/7m7n3TBQfGYxz7TXhcvdIVAAAAAJPoDEMAAAAAMPFuiPjjP64213aO36o+9uWsawP7o/byfzBep0fpJLxyuLtjT8Rjj5WJH94+AEye1RPXjnaQHxNl4uZl3c76D17Se1/13Z0ndx9x8B39Hy+/59rbx2scTXgEAAAA4FiC+wAAAADEeAbQHr/39Pzecz86XudG6SR81D1Vp2EAmCw5cW1pKboT2SJevDwfefi58Xqm13U77L/jlb33hzf906xlRaPSSb+s2FRqCfp/7j3dkTuc9Yxv9v7c6+4br3G76/re5xtXRBw8aMIjAAAAABERU/kPRQYCAAAAYNJNTU39d1NT//f/HRGHIrZtqwJVpfMqk+kX/1HWEkyMiJidXRVcBIBJvG+amprqdHKr0Yi4cHd+/ZG3jfczL8H05auyPnlR1r/9Qu/3vezqrK/YnvXiX8k6bp311yoTGlav+NRu533T/Lx3DgAAAMBkE9wHAAAAICJKAK3Vyq25uYiXvz+//l9njM4kuv3OrI88Wu1bXs5/T/yRHzE+ALhv2rUrt/bvj5jall/f+u+zXnDAKE2SsuLC/3L9sY/9yI/ouA8AAABARMQZhgAAAACASrsdEdsjnnoq4tk7ct9d1xuXSfLdnVkfff7Yx5pN4wMAERnEXlzMrX37IlYO59d3ft3oTKLOX/W7rxbYBwAAAGA1wX0AAAAAIqIE0I4ciYhDER/8YPXIga8ZnUmycGP3jDjc3fHeiK9+tTegCABU5uerr59oZC0d2Blv996ctUx4jT0RzzyTX7bbxgcAAACA1QT3AQAAAOiRAe2FhYjYE/HYYxEvXp6PfPrNRmeclYDhd/5izQOfibjtNuMDAIPum0pH9YWF6pHfeYvRmQT7f37NjnsifvM3V02IBQAAAICjBPcBAAAAGOSeiA98oNo8+I6s391paMbRXWdnPdppPyIWFnTaB4DjNT8fRzuuPz2b+0pHdsbsvun6rEc77W+PeOqp/FKnfQAAAAD6E9wHAAAAoK8MbO/bl1uLi1Wge+FGozNODlyS9YnGsY8JngHA8d83HTkS3Y7r1SNfWjA646RMYD3wtTUPHIr44Ad12gcAAABgGMF9AAAAAI7D6gD34/dm/fSbjctWVoJnn3tPv9c7g2fLy8YJAE7qvml7xOHDES9ck/tufKlxGQcf/2zWFy+v9i0t5X3TgkkaAAAAAAwluA8AAADAUBlEWlzMrWazeuTgO7KWju1sDSWwf+u3u6/w4eqxxcV8vefnjRMAnOx905EjEXEo4p3vjIgrIp5+ulrZ5vY7jdJW9LEvZ332ju6O7RFPPZVfvutdxgcAAACA4yG4DwAAAMBx6e0kurBQBb5Lx/YSCGdzu/PrWUsH4NgT8dhj+aXgGQCs333T0lJE3B9xww3VI488mvWu643SVlBWmCorTh11KOJ/+B+sUAQAAADAiRDcBwAAAOCEZECp2YyIKyIOHqwC/KWDuwD/5lQ6xZaOv6UDcNwTcfXVqzoEAwDret9UJj6229Uj9706q5WLNqfyujzY5/VpNldNzAAAAACA4ya4DwAAAMDJuj/irW+NiO0Rhw9XHdxLR3c2h4GdYu+P+IVfEDwDgNHLz9v5+dxavXLRXa/IauLj5lAC+2VFqdUWFnonYgAAAADAiZnKf2AyEAAAAACcnKmpqampqR07IuKKiK98JSLujzjnnIgz787vuOl1WS84YLQ2Uumwf0xgPyLm5/PfBVd3/gUANua+aXo6t/bvz7pjR8TUtvz65343686HjNZGuvfmrP/h7KxlYkVExOJi3jdddZVxAgAAAOBUCO4DAAAAsC5WBfjPj1hcjIgnI847L+KMb+Z3XPuDrIJoo1E69ZYVD55oHPs9AvsAsHnum4YF+C/9Ytbr7jNao3T7nVkfefTYx/bty9ps5v3TkSPGCwAAAIBTcYYhAAAAAGA9ZKBpaSkinoyYmYmIKyIOHox48fL8js+9J+td1xut9VQC+7d+O+vRwP4VEU8/nV++610C+wCw2e6bjhzJOjubexcWqk7vD16Staygw/q68aVZ+wX22+18Xcr9k8A+AAAAAOtDx30AAAAARqK3k2yrlbWxqgv8j16U9fr3Ga2TcaAb6CsTIkrQL/ZEPPZYRNwTcfXVqyZUAABb4v6p3C91OtUj5zyQ9YYzs15wwGidiLUTHV+4prpveuaZvG/6wAfyvmlhwXgBAAAAMAqC+wAAAABsiAyilQD/3Fz1yMvfn/Wqz2bdfYvR6ufh57LedXbWJxrHfs/iYlYdYgFg69837doVEdsj/uiPIuJQxLnnRkxty++49ItZr7vPaA1TViz4zl9kPTrR8fyI738/Ip6M2LXLREcAAAAANoLgPgAAAAAbKoNoe/dGxPaIT3wiIg5FbNtWfUcJ8jd/OOvFZ03mSJXOsAs3Zj0mcLZKu53/zjc/7wwDgHG7b9qxI7fKBMhdu6rvOOObWXe+Keu1t0/2iH36zVm/9XdZX7z82O8x0REAAACA00NwHwAAAIDTIoNo09O5NTcXEXsifumXIuKeiLPPrr7zVQtZr30m67gH+W+/M+ujz2ftF9Rf6I5JCewvLzujAGBS7p/27s37pk99Ku+bXvva6jsmbSWje2/u1v1ZjwnqXxFx8GBE3B9xww1531SC+wAAAACwsQT3AQAAANgU+gT5V9XVSpD/NW/MenX3X7cuOLC1nnEJmj3Y7ZD7V7dmPSZw9t6Ir341Ij4TcdttAmcAQO/9U6MRPSsZnXtu9R1n3p115kNZ397MutUmQj78XNYvdbIu/1rWF65Z8417Ih57LCLuqe6byoRHAAAAADi9BPcBAAAA2JQyiDYzk1slwN9oDD7inAeyvvpns26WYNpd12d9+NezPvnxrP066Relg36zKagPABzffVPPBMjtEb/4i3FMkL8ogf4f+rdZr/xg1p0Pnd5ncuCSrF/9RNaBExuL8yO+//2IeDKi1cr7pnbbGQEAAADAZiS4DwAAAMCW0Bvk37Wrt+7dO/jIEkw773tZX/bFrOd3A/QX/mTWH/9K1rrO/aVTflE65hdPXpT12TtqntInI/7zf46IGyL++I9z1759+e91S0tecQDg1O6bSpC/577pioh3vzsi7o8455xjjzzjm1lf8WLWcz+a9e8/mvVHu/dTMx/OWjdBsgTxn/pnWR95Zdb/elHvfdPffiHrwImNcxHf+U5EtKv7psXFvG/at88rDgAAAMBWILgPAAAAwJbWG0wrAf4dOyJie8RP/3QM7DS7kUrH/FJLQL901gcA2Oj7p55A/6r7pm3bTuOftj3i8OH8O/7wD3vvm0xsBAAAAGBrE9wHAAAAYKz1BtOKtds7dmQtHf1LXevIkawlOFaC92V/2S51aSn//a08DgCw2e+byn1RmRh5vNuDlImLRbmPOva+ysRGAAAAAMaZ4D4AAAAAAAAAAAAAAIzQGYYAAAAAAAAAAAAAAABGR3AfAAAAAAAAAAAAAABGSHAfAAAAAAAAAAAAAABGSHAfAAAAAAAAAAAAAABGSHAfAAAAAAAAAAAAAABGSHAfAAAAAAAAAAAAAABGSHAfAAAAAAAAAAAAAABGSHAfAAAAAAAAAAAAAABGSHAfAAAAAAAAAAAAAABGSHAfAAAAAAAAAAAAAABGSHAfAAAAAAAAAAAAAABGSHAfAAAAAAAAAAAAAABGSHAfAAAAAAAAAAAAAABGSHAfAAAAAAAAAAAAAABGSHAfAAAAAAAAAAAAAABGSHAfAAAAAAAAAAAAAABGSHAfAAAAAAAAAAAAAABGSHAfAAAAAAAAAAAAAABGSHAfAAAAAAAAAAAAAABGSHAfAAAAAAAAAAAAAABGSHAfAAAAAAAAAAAAAABGSHAfAAAAAAAAAAAAAABGSHAfAAAAAAAAAAAAAABGSHAfAAAAAAAAAAAAAABGSHAfAAAAAAAAAAAAAABGSHAfAAAAAAAAAAAAAABGSHAfAAAAAAAAAAAAAABGSHAfAAAAAAAAAAAAAABGSHAfAAAAAAAAAAAAAABGSHAfAAAAAAAAAAAAAABGSHAfAAAAAAAAAAAAAABGSHAfAAAAAAAAAAAAAABGSHAfAAAAAAAAAAAAAABGSHAfAAAAAAAAAAAAAABGSHAfAAAAAAAAAAAAAABGSHAfAAAAAAAAAAAAAABGSHAfAAAAAAAAAAAAAABGSHAfAAAAAAAAAAAAAABGSHAfAAAAAAAAAAAAAABGSHAfAAAAAAAAAAAAAABGSHAfAAAAAAAAAAAAAABGSHAfAAAAAAAAAAAAAABGSHAfAAAAAAAAAAAAAABGSHAfAAAAAAAAAAAAAABGSHAfAAAAAAAAAAAAAABGSHAfAAAAAAAAAAAAAABG6P8H+QojOP7nz9kAAAAldEVYdGRhdGU6Y3JlYXRlADIwMjItMTEtMDRUMTE6MDE6MjQrMDE6MDDl9U8tAAAAJXRFWHRkYXRlOm1vZGlmeQAyMDIyLTExLTA0VDExOjAxOjI0KzAxOjAwlKj3kQAAABR0RVh0cGRmOlZlcnNpb24AUERGLTEuNSAFXAs5AAAAAElFTkSuQmCC"
}
},
"cell_type": "markdown",
"id": "c65e10ce",
"metadata": {},
"source": [
"This solution corresponds to: \n",
""
]
},
{
"cell_type": "markdown",
"id": "366e2b82",
"metadata": {},
"source": [
"Let us add the following constraints with respect the other edges:"
]
},
{
"cell_type": "code",
"execution_count": 7,
"id": "0d6d6462",
"metadata": {},
"outputs": [],
"source": [
"satisfy(\n",
" x[0] != x[1],\n",
"\n",
" x[1] == x[2],\n",
" \n",
" x[2] != x[3],\n",
" \n",
" x[3] == x[0]\n",
");"
]
},
{
"cell_type": "markdown",
"id": "70d17bca",
"metadata": {},
"source": [
"We can run the solver again:"
]
},
{
"cell_type": "code",
"execution_count": 8,
"id": "eef80067",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"[0, 1, 1, 0]\n"
]
}
],
"source": [
"if solve() is SAT:\n",
" print(values(x))"
]
},
{
"attachments": {
"graph4c.png": {
"image/png": "iVBORw0KGgoAAAANSUhEUgAABfcAAAGVEAYAAAADABe3AAAABGdBTUEAAYagMeiWXwAAAAZiS0dE////////CVj33AAAAAlwSFlzAAABLAAAASwAc4jpUgAAAAd0SU1FB+YLBAsBHYIzRgAAAGX7SURBVHja7f1tkGRneSd4X6VBCCbQSy0iZMJI01smcK8CC0ld9sBsN8hsawwRPUyPRAO2vPiZxZtp2WM8ixBVoEBCEMKZgDS7ctg4ay3P4kF+oS22h1EYJroCY3U/gzEq1GgcikYPru2V8NqEmmnUIkYW8qqeD1fefSq7M/P0S2V3Vebv9+Wqc7JOVeWdJ0+e6P7f1z21srKysrISAAAAAAAAAAAAAADACJxnCAAAAAAAAAAAAAAAYHQE9wEAAAAAAAAAAAAAYIQE9wEAAAAAAAAAAAAAYIQE9wEAAAAAAAAAAAAAYIQE9wEAAAAAAAAAAAAAYIQE9wEAAAAAAAAAAAAAYIQE9wEAAAAAAAAAAAAAYIQE9wEAAAAAAAAAAAAAYIQE9wEAAAAAAAAAAAAAYIQE9wEAAAAAAAAAAAAAYIQE9wEAAAAAAAAAAAAAYIQE9wEAAAAAAAAAAAAAYIQE9wEAAAAAAAAAAAAAYIQE9wEAAAAAAAAAAAAAYIQE9wEAAAAAAAAAAAAAYIQE9wEAAAAAAAAAAAAAYIQE9wEAAAAAAAAAAAAAYIQE9wEAAAAAAAAAAAAAYIQE9wEAAAAAAAAAAAAAYIQE9wEAAAAAAAAAAAAAYIQE9wEAAAAAAAAAAAAAYIQE9wEAAAAAAAAAAAAAYIQE9wEAAAAAAAAAAAAAYIQE9wEAAAAAAAAAAAAAYIQE9wEAAAAAAAAAAAAAYIQE9wEAAAAAAAAAAAAAYIQE9wEAAAAAAAAAAAAAYIQE9wEAAAAAAAAAAAAAYIQE9wEAAAAAAAAAAAAAYIQE9wEAAAAAAAAAAAAAYIQE9wEAAAAAAAAAAAAAYIQE9wEAAAAAAAAAAAAAYIQE9wEAAAAAAAAAAAAAYIQE9wEAAAAAAAAAAAAAYIQE9wEAAAAAAAAAAAAAYIQE9wEAAAAAAAAAAAAAYIQE9wEAAAAAAAAAAAAAYIQE9wEAAAAAAAAAAAAAYIQE9wEAAAAAAAAAAAAAYIQE9wEAAAAAAAAAAAAAYIQE9wEAAAAAAAAAAAAAYIQE9wEAAAAAAAAAAAAAYIQE9wEAAAAAAAAAAAAAYIQE9wEAAAAAAAAAAAAAYIQE9wEAAAAAAAAAAAAAYIQE9wEAAAAAAAAAAAAAYIReZAgAAAAAGGdTU1NTU1MzM7lVV6enT+2nLy31bi8uZj1yZGVlZWVl5fjHAQDW+31TuR/asqX3/uj47XL/dLr3TWW73DeV+ygAAAAAGE9T+Q9hBgIAAACAjS2DZrt25daWLbE5IuKd74yDERGbNp3bv2737qwlkLZ7d/673JEjXjkA4NzcN5Ug/vbtWVfdR51TJdBf7p/KfdPyslcOAAAAgI1McB8AAACADaG3A2wJmG3fHjsjIn72Z2NPRMSFFx5/3HnfyHrBZ7Ne+njv49d8NevF/2fWbY/2//2PPZd1+eNZn/zTrIc/lPXpj2R99v/O+vyNNU/oPRERX/lK3BcR8aUv5U7BNABgre+fVt03ReyM+NmfjYg9EVdc0eeITVlfckP/O6eZvd07p5dl3XFn/9/83W1Zv/7m7p3SD7p3Utdn/bu3Zf3Bwe7257OuHBrwVHZGPPFE/t1/8Ae9901WOAIAAABgYxDcBwAAAGBd6g3qz8311hOd/0DWmQ9m/anfyTooiD9qJa72+amsf/XDrEdnT+bo0pm/3c5/vyvbAAB1909zcxFxacT8fEQcjrjkkhO/s0xt/NHbu3dQ3UD+TXef22dw/y1ZH/uNrIe7UyYHBvo3Rxw6FBEHI3791/O+aWHBmQAAAADAeiS4DwAAAMC6cEJQf2dExC//8vGd9C96OOsrfy7rW5tZr7xgYz3fU4ul7d6ddX5eR34AoPf+qdGIiJ0Rt90WJ3TSL1Mbf+TfZr3uA1nP1dTG07Xvqqxf+UTWv/5o1heuPe4bt0YcOBAR+yNuvdUESAAAAADWE8F9AAAAAM6pY4GzrRERn/xk7I+IuOii8vhL35e1+aNZN1pA/2SVDv0Lt2X9zl9m7R/kL51kS5D/yBFnEgBMyn3T9u0R8Z5uUP++iOuuq76jdNLfcX233jneI/LpN2b95t9nPSHI/56Ir3wlx+muuwT5AQAAADiXBPcBAAAAOKuOBc42R0T87/97HIyI2LSpPF6C+td/Juu4x80GKUH+e7+W9anGcd+wOSLi6adz/H77t/Pf+ebnnWEAMG73TWVFos99Luv27dV3lKD+616U9eaHJnvEPvalrMOmQJoACQAAAMC5IbgPAAAAwFlxrLN+RER0OmV/iZtte0PWm+42Vv089lzW331T1qOz/b5r9+6szaYgGgBs9PumLVsi4tKIxcWIOBxxySURU5vyO1712qyNu7Jets+orVa7ltHWiAMHImJ/xC/+Yt43LS0ZNwAAAABGSXAfAAAAgJHK4FkJ6jeO9Y2/fEfWD7/FGJ2OB+/I+h8uzLo6hhZx4EDsj4i48cb897/lZSMGABvlvqnRiIidEZ/6VETsibjwwojzH8jvuP3VWQX1T02ZAvmbm7I+f2N153T0aPQE+MtESAAAAABYW4L7AAAAAKypDJxNT8d7IiI+//m4LyLiuuvK49c8mvXmh4zVWth3VdY/fCrr6hhaxNGjGeB/85t1kgWA9X7/1Grl1txc9cgrFrLe9UOjtBZKJ/57v5b1qcaJ3zM/n/dN7bbxAgAAAGAtCe4DAAAAsCYycLZlSwbGf+d3MjB+9dVTm/Lxn/+9rNseNVajUGJoH/9M1mfv6fddzWb+e+DCghEDgHN93zQ9nVtlZaJdu6rvMNXx7PjYl7I++eCJjy0s5H1Ts2mcAAAAAFgLgvsAAAAAnJFjgf1LIyIWF+NwRMQll5z/QD5++6uzXrbPWJ1Nw2JoAvwAsB7unx5+OLe2bIkoUx3/2TNZd9xplM6mT78x64G3ZV05VD22e3feN73jHcYJAAAAgDMhuA8AAADAaTnWKXZrRMSXv1w67F/UjaDden5Wgf1zq8TQHrmq36PXX5//Pri4aKQA4GzdP5UO+41GFdi3NtH6sK97x/TZd2ddHeBvt/O+aX7eOAEAAABwOs4zBAAAAACclk9GRPzu75bAfumwL7C/vtz8UNbLdxz3wNaIiAceyADhzIyRAoDRyc/bubncEthfv8rrUFY+WG1uLl/HRsM4AQAAAHA6dNwHAAAA4JRkYKnVyq25uRI7+7VfzXrlBcZoPXv/67Mene3u2BoRceBATsB485vz3wuPHDFSALBW903bt+fW3r3VI9d0A+Jlih3r0933Zv3W490dOyOeeSYi9kT89E/nfdPSknECAAAA4GTouA8AAADASentMFo6xlb9SAX2N4ayIkJZIaGsmJAbnY4RAoC1um/asiUitkY88ED1SFkDR2B/Y7jlvVlfsdDdsSfiwgsj4tKIxcV8naenjRMAAAAAJ0NwHwAAAIChVgXPYnWwu/SJ3XGnMdpILtuX9V2v6L6+m1Y/umtX74oKAMCp3zdNT0fE1ojf+Z2I2B9x0UURFz2c3/HhtxiljeiuH2Y9NvXxcMQll+SXq1dSAAAAAIDBBPcBAAAAOAlVkLv0G9UndmPb1p14UVZM6DU3l8HDmRkjBQCnam4uIvbnijYl6F3WvGFju/3VWc/7RrVvy5belakAAAAAoD/BfQAAAAD6ygDS9u25tX176cz+3n9sbMZJWTGhTMjoNTdnhADgZO+bSqf9m2+uHnlrN8xd1rxhYyuv4+tedNwDOyNuu834AAAAADCM4D4AAAAA/e2MiLjvvrL5mhdnFTsbTzf17bzfaGQQccsWIwQAdUqn/Ysuinjp+3JfmSLHeClrT5UVFWJPxBVX5H1TtVIVAAAAAKwmuA8AAABAjwwcNRqxJyLiiivO+0buv+W9xmacXXlB1st39HtUAA0ABt83zczk1uqVat6+0+hMgrKiwjE7I375l1etwAAAAAAAxwjuAwAAANBrZ0TEbbeVzde9yJBMksZdWac2rd67fXsG0LZvN0IAcLzVgf1XLGTd9qhxmQRlRYWywkLsibjwwhPPCwAAAAAQ3AcAAACgK4PZrVbptH/+A7n/5oeMzSS5bF/WV72236MCaABQ3Tdt2ZJbjVVd1296xuhMon4rLMzN9a7IAAAAAMCkE9wHAAAAIG2OiHjnO8vmWxuT8bS/uy3r/bdk/diX+tcH75is06F03j/vG6v3ls77JagIAJNs167q68t3ZL3ygskek3JnVe6gyva4KysslBUXBp0nAAAAAEwywX0AAACACXesE+jBiIhNm0pQe8ed4/l8j4+T3f7Ps/7Fr2T9h49nndnbe9yD3e1f+idZS9B/XJXO+z96e79HBdAAmHg7I372Z6vN6z4w2cNRpjje8f9mffLBrF9/82SNw5W/etyOrRHvepe3CwAAAAARES8yBAAAAACsDmK//OHxfIYlsP/Rb2d9vhsnu6bbH/Xmh7rf+N4Bx/+DrPd+LeufPZf1sRdnveuH4zlu13w165Nlx9aIiJ/5mdyYn/feAWCS9K48c8UV1do02/7TZIzAvquy/uUlWQ/+H1mf/V73G66d7DPkpruzPvSprCv7I66+ukyUXVlZWVlZWV72TgIAAACYTDruAwAAAEy6T0ZE3HRT2TyhT+iY+Phnsj5/Y9bLd2Q9FtivUTrQl4D++Q9kfaqR9e57x3PcysoLU5u6O/ZHrA6geQMBMHlWrzzTf22aja900G/8q976796Y9Zt/n/XSx50P/Vz6oRP3bd9uXAAAAAAmm+A+AAAAwIQ6Fry+NSLiJ36iBLNLn9BxUQL1z97Tfd7d59m468x+7j/5ud7tx7uB/seeG8/zpV/8rDe4CAATYWu18kxEtTbNuPnJL2d928t767/u3in+dneFgQ+/xSnRz6tef+I+wX0AAACASSe4DwAAADDRqgBR/2D2xvf/+8Pe7fI8Swf903X8BIeVQ1nvv3A8x7H/SgwCaABMhlUrzeyPuPrqaipgWZtm3JQ7pfL8Sr3yAmfDybhh5cR9u3bleTQ9bXwAAAAAJpPgPgAAAMBEq4LX/fqCbmT335L1hWt79/83n1rb3/PS9/VuH/74eJ4p/Vdi2L5dAA2AybF6pZlxnfLI2igTHy56eNj9NwAAAACTRXAfAAAAYFJdGhFx/fVls19f0I3ssd/ov//Hv7e2v+dlm3u3S+f9B+8Yz9Pm+IkKacsWbygAxt/MTPV1/7VooNfFH3HfBAAAAEAhuA8AAAAwqQ5HRFxyydSm3Cx9QcfF92bPzu95yRf673/kDeN52lz6eL+9q4OMADCuVn/eXfwy40G9a77qvgkAAACAQnAfAAAAYMJMTU1NTU1VnT5fcsN4Ps8Xru2/f+ZDZ+f3H37NJJ1VAmgAjL1LI2ZXTQvccachod7F/+eJ+6anjQsAAADAZBLcBwAAAJhIVWDo/J8br2f24B3DH7/ygrPzd/z9fz+eZ06/vrGC+wBMgMMRl1xiGDg12x49cd/27cYFAAAAYDIJ7gMAAABMpCowdPFHjMYoPH/jeD6vfn1jdY4FYFwdv1JRxEvfZ1Q4jTNpkzEAAAAA4EWGAAAAAGCyXfrx7hcPGQvqlb6x/65n7+xsBht1kAVgHF1zTfX1sbWK/ty4cPJeckPWZ++JKBNCtm9fWVlZWVlZXDQ+AAAAAJNBcB8AAABgwl3+090v7hyP5/Pkn3a/uMpre/ZccknWvXuNBQDj7dhaRW8xFgAAAADAqTjPEAAAAAAwTg5/yBgAAAAAAAAA64vgPgAAAAAAAAAAAAAAjNCLDAEAAADAZPvWy7PuGJPnc81Xsz7ppT2Lvv/9rLt2GQsAxs8112T9xCciDr/GeAAAAAAAp0NwHwAAAGAiHTlSvvqv4mecggfv6Lf34YdXVlZWVlYWF40QAONkampqamqqum+C0/N3n1+95b4JAAAAYDKdZwgAAAAAJtHSUvnq6Y8YjVGY2jSez+vpH/Tbu7zsFQdgHGXAurpvinj2HqPCaZxJh7pfbI54+mnjAQAAADCZBPcBAAAAJlLVOfb53x+vZzbzoeGP9+8Yv/ZecsN4njnL1w8/nwBgTG2OOHSo2vzuNkNCvRPuPA9GfP3rxgUAAABgMgnuAwAAAEyY4zvHjlvf2CsvWB9/x8s2T9JZpeM+AGPvYMS3v11tfv3NhgT3TQAAAACcCsF9AAAAgIlWBYfGrW/sS993dn7P0x/pv/9Vrx/PM+bwa4afRwAwvqqJjxFP/qnxoN4jbzhxn5WKAAAAACaV4D4AAADARKsCaJ+fGq9ndsWD/fd/6+Vr+3ue//3++9+0d7zGs0zs6L9Cw+ogIwCMq9UT1f7qh8aDen/7L903AQAAAFAI7gMAAABMtMXF8tW4xc/e2uy//7+8f21/z/FB9tLp/8oLxms8+0/s2L17ZWVlZWVF51gAJsHu3dXXz7zdeDBYmfL4/I3dHVsjjh7N+6bV5xEAAAAAk0RwHwAAAGCiVcGho7NZS8xooyvB+Vcs9O7/3uza/Pz7b+m//6d+czzPlP4TO6qJHwAwzlZNVNsaceBAxMqh4XcETLYTpjzuj/iP/9G4AAAAAEw2wX0AAACACXUsgPbJiIg9e8r+xZ8ar+d50zNZpzZlfeHarJ9+45n93L/4ld7t0mn/prvH83zp31dYx1gAJs7+iD/8w2rzsd8wJJyo35RHEx4BAAAAJt2LDAEAAADAhLs1IuLP/zw3du48Fj/74Xg8vdJ5/591A/xf6O4/8Las+34v67ZHT+7nlcD/s/8q6/kPZP3Qq7vfsG+8To/SR3jlue6OrRERBw6s7DvWeRgAJkyZuNZqRRz+eHfn+8fzuT54R//933p51r/5/eHHf7G79tG3Ppj1x7/X//t+8stZL9vgd1Jl7aqjrxt83gAAAAAwqXTcBwAAACBWB4mOxc/GzI47s/6PD2Wd+nzWz7476933Zi1xq2LfVVlve3HWR7rbpcP+7d3A/mX7xnPcTugjvD+it9MwAEyOXLFoeTkiNkccOhSxcqj3jmHcfOF7/eu3Hs96dLb3+8sdUlnr6Pkbe79/0M/7+pvHY7z6rV21e/exla4AAAAAmGhT+Q9FBgIAAABg0k1NTU1NTT38cG5t2XJNtwP9zQ+N9/MuHfT/qrvCwLP/d9YSMyvxs5dtzvqGbr/YMhFgXJUJDLf/86wllph+7MdWBRcBYELvm1qt3Jqbi3hFt7P8XT80OpPs17r3Rs/eU+2bn8/7pnbb+AAAAABMNsF9AAAAACKiBNAajdzqdM77Rn712//J2Eyij30p65MPrt67uJj/nnj99UYIAPdNMzO59Vd/VT1S1vbZ9qhRmiQP3pG1rCAQmyOefjoiDkb8t/+tjvsAAAAAREScZwgAAAAAiIjIQNHCQmyOiDh06IVrc//d9xqbSfLYc1l7A/vF/LwRAoBy31RWnlndSf2P9xidSfTFheN2HIz47d8W2AcAAABgNcF9AAAAAHodjIj4n//nsvn4D7N+d5uhmQT3X9hv78JCBs+WlowQAByv3Y6InRHPPBPx7D25r3RgZ7x9+o1Zn7+xu2NnxBNP5H2TCY8AAAAA9BLcBwAAAKBHBo0WF+M9ERFf+crKody/cJuxGWf7rsr6VKPfo6s7CQMAvfdNR45ExJ6I3/qt6pG9v2B0JsE3//64HXsi7rrLuAAAAADQj+A+AAAAAP3dF7E6ePSdv8z62HOGZhz98Z5+e9vtDCQuLxshAKhTOu8/8UTVeb90ZGe8fOxLWV+4trtja8SBA3nftLBgfAAAAADoR3AfAAAAgL6Odd6PiIiFhdJ5/3ffZGzGSYkTlnhhbI6IePrp3NBpHwBO/r6pdN5f3XH9wNuyfnebURoHZY2iMqX1mP0Rt95qfAAAAAAYRnAfAAAAgJPQbpdA99HZ3FP6jLIxldjZI1cd98DBiIgPfGBVABEAOEm9HdeXliLK1MePfjurAP/GVF63P3yq+0ofqh5bWOid8AoAAAAA/QnuAwAAADBUBpGWlzPQ/fa3l/1PPpi1dGxnY3jsuayffXe/Rw8cyLq8bKQA4Ezt2xcRmyP+n/8n4vkbc9+9XzMuG9HHP5O1vI6xtbpvmp83PgAAAACcDMF9AAAAAE5KbyfRZrPsLx3b911ljNaz0if2Nzd1X89D3Qc2R0Q88URuXH111r17p6ampqam5uaMHADUy8/N6emse/fm3n/9ryPiYMTTT0fEzohnnol4qpGP3X2vUdsIbntx1mfv6e7YGnH0aETsj7jxRisUAQAAAHAqpvIflAwEAAAAAKcmg2mdTm41GlOb8quP/vusl+0zRutJiZ2VuGAG9g8dypUUNm0afvTCQtb5eQE1ADj+fmjLltz63Oeyzsz0/+6vfjXrG95Q7XvTBVlvuttoridlTalH+kxNnZ3N+6GlJeMEAAAAwKnQcR8AAACA05KBpdJ5f3GxdHD/6Lezlg7vnFsnBPa3RkQcPZqB/V/7tdxZFzxrdI8unfgHBRIBYDLk52H1+Zi17vPxoYeyttur9r0y64N3GNX14P5bsvYL7DebAvsAAAAAnAkd9wEAAAA4Ixlcm57OQPiXvxz7IyKuvrp04P/538u67VFjdTaUCROffD7r0dl+3/WOd+S/C+7efez1i4iIVitrCSIOUjrul5+zuGjkAZic+57yeTk3d3Kfl2XFmrKCzYkrF1XHXNO9Y7r5IaN9Nn3sS1mffPDEx9rtfP3m540TAAAAAGdCcB8AAACANdEbAC+dZ7dsKQH+q7+QVQxtNPZ1+8L+4VNZn7+x+0DpsL8/IuLGG+uC9vk6liBiCSbWKYHE1R2EAWDc7m8+97ms27cPP2p5OWuZ4Da4Q/vgiQCv6Ib87/qhV2EUylTHe7+W9amG+xsAAAAARk1wHwAAAICRGNRJ9vIdWT/8FmO0Fh68I+t/uDDryqHuA1sjIg4c6A3slyDhyb5+JZhYgooluDhI6SRcgm6l0zAAbMT7mC1bej8HZ2aGH1UmxpXA/sl/DubvK/dL5f4pIuKl78v6oV/Ietk+r86ZKIH9j3476+qpjkePRsT+iF/8xbIykfECAAAAYC0J7gMAAAAwUoOCaBc9nPXW87OKoZ2au+/N+q3H+z1agmbN5pkG6PP1K0HFElwsQcZBSmfhElw8+QkDALB+7ltKJ/y6iWvtdn7ezc+vze/fsiUitkZ8+csRsT/ioosizn8gv+Ndr8i67VGv1qkYONVxc8ShQxFxMOLtb69bIQEAAAAAzoTgPgAAAABnxbEO7psjIv74j+NgRMTFF09tysdf9dqsjbuyCvL3KnGzB/dmfeHaft+1dsHB/q9fCS6WIGO1kkJ/ZcJACfCXTsQAsB7vU8rn29zcyX2+lRVmyooza/33zMxExNaIBx6IiP0RV19dfccrur/zpmeyXnmBV3G1x57L+rtvynp09sTvOf0VEgAAAADgdAjuAwAAAHBW9XZwLx34t28vj5/3jayve1HWmx+azHEqQf29v5D12XuO+4bNERGHDuUEiA98IP+dr3TaP1uvYwk2lqBjnRJwbLe9EwA49/cjZUJaWVGmuh/pr6wgU4Leo+/M3vt3ls/dfhMLLt+RdVKnQJag/v3djvpPHT+5cGvE0aMRsT/i058e1URHAAAAABhGcB8AAACAc+pYJ/73RETcdlvcFxFx3XXl8RLk3/aGrDfdPZ7jcDJxs4ijR2N/RMTHP75eAvDHXr+IqIKPJWA4SOlMXIL8OtwCcDY/t7Zs6f3cKhMKB1k/ndl7J0CWAP/qFXCOX8vow28Zz1fyu9u69xS3Zf3OX2ZdOeS+AwAAAID1SnAfAAAAgHUlA2mNRnaU/+AHs6P8pk3l8RLk/9Hbs87szbpRAv0loP/F7loDy7+e9fkbj/vGnRERzzwTeyIifuu3cme7vV4DZ71BwhKELMHIQUqn4hKELJ2MAWBE9xcRUa0UUzfRrHzurt/O7L0TEcrzWr1yQAnyX/qhrK96fdYbuv87uN4785eA/uensv7VD7MenR18TAnql9fP/QUAAAAA64PgPgAAAADrWl2Q/9j3dfeUWNqVv5p1+19kPduxtH1XZf3KJ7L+9UezvnDtgAM2R0Q8/XQ+vz/6o9y58QJn+XqVIGQJEDYaw48qExFKgL90NgaAtfhcKp9HpUN93edR6cxeAuAb7fmW4H55vquD/Me76OGsr/y5rG9tdu+kLji7f/lJT23sY/furAsL7iMAAAAAWM8E9wEAAADYUHo7y27fHp+MiLjpprg1IuInfmLQcaVT/wWfzXrp472PX/PVk/v933p51v/6mqyHX9P7+LP31PyAuYiI73wn2hERf/InuXNxMf+drgTPxu31KsHBEpysUwKT7bYzHoBT/9wpE8jKCjDDgusREWWCXJlAVlaEGZfxKCvibN8eEZ+MeOtbI+LWiJ07hxy5KetLbsj6ss3d7S9076Q+nvXynx7+Fzz5p907pu7Uyr97W9YfHOxufz7ryqH6Z1Puk0owf/fu9boSEQAAAAD0I7gPAAAAwFjoDabt2pW1BPzL9tlWgoAlaFYCZuMTCDy116cEJ0uQsgQrBymdjkuQXzAPgGGfM+Vzv3zOlPuCQUoAvAT2J+dzpneCQ/l83r49Ii6NeMc7IuJwxCWXnMU/6dKI738/f295/cZ3YiMAAAAAk0lwHwAAAICJ0BtQK8G+EugrtTz+T/9p/5/yX/5L1r17s5aAXwniHzkyqcH8U3sdyniXYF55PQYp41mClWVCBAA+V6ampqYajdwqK7vUTQxrt/PzZH7eCJ7M+JZg//H3UcXbul30X/rS3v3PPpv1C1/o3V8mTETk61BtAwAAAMA4E9wHAAAAgFUyoDboX8wE/dZ2nEsAsAQtS/BykDJRogT4Bf0AJvtzpHx+zM2d3OdHWcGlrOjC2rwOZUJjCfgXpWP+9dcbKQAAAACIOM8QAAAAAABnWwb5ygoFzWburZsQUYL+e/dmULAuqAnAuCgTvnqD4nWfA2WFluuvF9gHAAAAAM41wX0AAAAA4JzLQGW7nVulM2/pkDxIq5UBzk6nt4M/AOMir+9btuTWww9nPb6z+/HKiiyzs/n5srRkJAEAAACAc01wHwAAAABYNzJgWQUus9YFLhuNrKUT/8yMkQTY2PJ6Xl3fs9Zd39vt/BwpHfbrJoABAAAAAJw9gvsAAAAAwLqTgcvl5dwqHfgXFoYfVXVkzsBnXUdmANabvH63WrnV6WQdtKJKCeY3m/m5MT9vBAEAAACA9UpwHwAAAABYt0rH5KzNZu6tC2aWgGfpwD83ZyQB1qe8Tk9PZy2d9euu29XErvx8qJvYBQAAAABw7gnuAwAAAAAbRgY02+3cKp34S8flQVqtDIR2OiUgaiQBzq28HlcrpWStWyllcTHr7Gx+HiwtGUkAAAAAYKMQ3AcAAAAANpwMbFYBzqx1Ac5GI2vpxD8zYyQBzq68/lbX46x11+N2O6/7pcN+3YQtAAAAAID1R3AfAAAAANiwMsC5vJxbpQP/wsLwo6oOzxkgrevwDMCZyuttq5VbnU7WQSuglGB+s5nX+fl5IwgAAAAAbHSC+wAAAADAhlc6MGdtNnNvXdCzBEZLB/65OSMJsDbyujo9nbV01q+7zlYTsfJ6XjcRCwAAAABg4xDcBwAAAADGTgY+2+3cKp34SwfnQVqtDJh2OiVwaiQBTk1eP6uVTbLWrWyyuJh1djav30tLRhIAAAAAGDeC+wAAAADA2MoAaBUIzVoXCG00spZO/DMzRhJguLxeVtfPrHXXz3Y7r9Olw37dBCsAAAAAgI1LcB8AAAAAGHsZCF1ezq3SgX9hYfhRVcfoDKTWdYwGmDx5fWy1cqvTyTpoxZISzG8287o8P28EAQAAAIBJIbgPAAAAAEyM0tE5a7OZe+uCoyWAWjrwz80ZSWBS5XVwejpr6axfd12sJk7l9bdu4hQAAAAAwPgR3AcAAAAAJlYGSNvt3Cqd+EtH6EFarQysdjolwGokgXGX17tqJZKsdSuRLC5mnZ3N6+3SkpEEAAAAACaV4D4AAAAAMPEyUFoFTLPWBUwbjaylE//MjJEExk1e36rrXda66127ndfV0mG/bkIUAAAAAMD4E9wHAAAAAOjKgOnycm6VDvwLC8OPqjpQZ8C1rgM1wPqX17NWK7c6nayDVhgpwfxmM6+j8/NGEAAAAACgl+A+AAAAAMBxSoforM1m7q0LopZAa+nAPzdnJIGNIq9b09NZS2f9uutYNdEpr5d1E50AAAAAACaX4D4AAAAAQI0MpLbbuVU68ZcO04O0WhmA7XRKINZIAutNXp+qlUOy1q0csriYdXY2r49LS0YSAAAAAGA4wX0AAAAAgJOUAdUqsJq1LrDaaGQtnfhnZowkcK7l9ai6PmWtuz6123kdLB326yYwAQAAAABQCO4DAAAAAJyiDKwuL+dW6cC/sDD8qKqjdQZm6zpaA6y9vP60WrnV6WQdtCJICeY3m3ndm583ggAAAAAAp0dwHwAAAADgNJWO01mbzdxbF2wtAdnSgX9uzkgCo5LXmenprKWzft11p5qYlNe3uolJAAAAAADUEdwHAAAAAFgjGXBtt3OrdOIvHasHabUyUNvplICtkQTOVF5PqpU+stat9LG4mHV2Nq9nS0tGEgAAAABgbQjuAwAAAACssQy8VgHYrHUB2EYja+nEPzNjJIFTldeP6nqSte560m7ndat02K+bcAQAAAAAwKkS3AcAAAAAGJEMwC4v51bpwL+wMPyoqkN2BnDrOmQDlMB+q5VbnU7WQSt4lGB+s5nXqfl5IwgAAAAAMFqC+wAAAAAAI1Y6WGdtNnNvXVC2BG5LB/65OSMJFHldmJ7OWjrr110nqolEeT2qm0gEAAAAAMBaEdwHAAAAADjLMjDbbudW6cRfOmAP0mplQLfTKYFdIwmTJ9//1cocWetW5lhczDo7m9efpSUjCQAAAABwdgnuAwAAAACcIxmgrQK1WesCtY1G1tKJf2bGSML4y/d79f7PWvf+b7fzOlM67NdNEAIAAAAAYFQE9wEAAAAAzrEM1C4v51bpwL+wMPyoquN2BnrrOm4DG1G+v1ut3Op0sg5acaME85vNvK7MzxtBAAAAAID1QXAfAAAAAGCdKB2xszabubcueFsCvKUD/9yckYSNK9/H09NZS2f9uvd1NfEnrx91E38AAAAAADjbBPcBAAAAANapDOC227lVOvGXjtqDtFoZ+O10SgDYSML6l+/XaiWNrHUraSwuZp2dzevF0pKRBAAAAABYnwT3AQAAAADWuQzkVgHdrHUB3UYja+nEPzNjJGH9yfdn9X7NWvd+bbfzulA67NdN6AEAAAAA4FwT3AcAAAAA2CAyoLu8nFulA//CwvCjqg7eGRCu6+ANnA35fmy1cqvTyTpohYwSzG828zowP28EAQAAAAA2FsF9AAAAAIANpnTYztps5t66IG8JBJcO/HNzRhLOnnzfTU9nLZ31696H1USdfL/XTdQBAAAAAGC9EtwHAAAAANjgMtDbbudW6cRfOnQP0mplgLjTKYFiIwlrL99f1coXWetWvlhczDo7m+/vpSUjCQAAAACwsQnuAwAAAACMiQz4VoHfrHWB30Yja+nEPzNjJOHM5fupen9lrXt/tdv5Pi4d9usm4AAAAAAAsFEI7gMAAAAAjJkM/C4v51bpwL+wMPyoqiN4Bo7rOoID/eT7p9XKrU4n66AVLUowv9nM9+38vBEEAAAAABhPgvsAAAAAAGOqdOzO2mzm3rpgcAkYlw78c3NGEgbL98n0dNbSWb/ufVNNrMn3Z93EGgAAAAAANjrBfQAAAACACZEB4XY7t0on/tLxe5BWKwPJnU4JKBtJKIH9aqWKrHUrVSwuZp2dzffj0pKRBAAAAACYDIL7AAAAAAATJgPDVYA4a12AuNHIWjrxz8wYSSZRnv/V+yFr3fuh3c73XemwXzdhBgAAAACAcSO4DwAAAAAwoTJAvLycW6UD/8LC8KOqDuMZYK7rMA7jIc/3Viu3Op2sg1agKMH8ZjPfZ/PzRhAAAAAAYLIJ7gMAAAAATLjSATxrs5l764LGJbBcOvDPzRlJxkme19PTWUtn/brzvJoIk++nuokwAAAAAABMCsF9AAAAAAB6ZOC43c6t0om/dBAfpNXKgHOnUwLPRpKNKM/famWJrHUrSywuZp2dzffP0pKRBAAAAABgNcF9AAAAAAD6ygByFUjOWhdIbjSylk78MzNGko0gz9fq/M1ad/622/k+KR326ya4AAAAAAAwqQT3AQAAAAAYKgPJy8u5VTrwLywMP6rqWJ6B6LqO5XBu5PnZauVWp5N10IoRJZjfbOb7Yn7eCAIAAAAAcDIE9wEAAAAAOCmlo3jWZjP31gWXSwC6dOCfmzOSnEt5Hk5PZy2d9evOy2riSp7/dRNXAAAAAACgl+A+AAAAAACnJQPM7XZulU78pSP5IK1WBqY7nRKgNpKcDXm+VStBZK1bCWJxMevsbJ7vS0tGEgAAAACA0yG4DwAAAADAGclAcxVwzloXcG40spZO/DMzRpJRyPOrOt+y1p1v7Xae16XDft2EFAAAAAAAGE5wHwAAAACANZEB5+Xl3Cod+BcWhh9VdUDPgHVdB3Q4OXk+tVq51elkHbTCQwnmN5t5Hs/PG0EAAAAAANaS4D4AAAAAAGuqdCjP2mzm3rogdAlUlw78c3NGklOR5830dNbSWb/uPKommuT5WjfRBAAAAAAATo/gPgAAAAAAI5WB6HY7t0on/tLhfJBWKwPYnU4JZBtJ+snzo1q5IWvdyg2Li1lnZ/P8XFoykgAAAAAAjJLgPgAAAAAAZ0UGpKvAdNa6wHSjkbV04p+ZMZJElMB+dX5krTs/2u08D0uH/boJJAAAAAAAsDYE9wEAAAAAOKsyML28nFulA//CwvCjqo7qGdiu66jOuMrXv9XKrU4n66AVGUowv9nM825+3ggCAAAAAHAuCO4DAAAAAHBOlI7nWZvN3FsXrC4B7dKBf27OSI63fJ2np7OWzvp1r3s1MSTPr7qJIQAAAAAAMFqC+wAAAAAArAsZsG63c6t04i8d0wdptTLQ3emUgLeRHA/5elYrLWStW2lhcTHr7GyeT0tLRhIAAAAAgPVAcB8AAAAAgHUlA9dVADtrXQC70chaOvHPzBjJjSlfv+r1zFr3erbbed6UDvt1Ez4AAAAAAODsEtwHAAAAAGBdygD28nJulQ78CwvDj6o6tGcAvK5DO+tFvl6tVm51OlkHraBQgvnNZp4n8/NGEAAAAACA9UxwHwAAAACAda10UM/abObeuqB2CXyXDvxzc0ZyfcnXZXo6a+msX/c6VRM58nyom8gBAAAAAADrg+A+AAAAAAAbSga22+3cKp34Swf2QVqtDIh3OiUwbiTPjRz/amWErHUrIywuZp2dzdd/aclIAgAAAACwkQjuAwAAAACwIWWAuwp0Z60LdDcaWUsn/pkZI3l25HhX45+1bvzb7XydS4f9ugkaAAAAAACwPgnuAwAAAACwoWWge3k5t0oH/oWF4UdVHd8zUF7X8Z3TlePbauVWp5N10IoHJZjfbObrOj9vBAEAAAAAGAeC+wAAAAAAjIXSkT1rs5l764LfJUBeOvDPzRnJM5PjOD2dtXTWrxvXauJFvn51Ey8AAAAAAGBjEdwHAAAAAGAsZQC83c6t0om/dHQfpNXKwHmnUwLoRvLk5HhVKxlkrVvJYHEx6+xsvl5LS0YSAAAAAIBxJLgPAAAAAMBYy0B4FRDPWhcQbzSylk78MzNGsr8cn2q8staNV7udr0vpsF83oQIAAAAAADY2wX0AAAAAACZCBsSXl3OrdOBfWBh+VNVBPgPqdR3kJ0eOR6uVW51O1kErFJRgfrOZr8P8vBEEAAAAAGCSCO4DAAAAADBRSof3rM1m7q0LkpdAeunAPzc3aeOWz3t6OmvprF83DtVEiRzvuokSAAAAAAAwngT3AQAAAACYaBkob7dzq3TiLx3iB2m1MsDe6ZRA+7iOTz6/auWBrHUrDywuZp2dzfFdWnKmAQAAAAAwyQT3AQAAAAAgSoC/CpxnrQucNxpZSyf+mZlxGY98PtXzy1r3/NrtHMfSYb9uAgQAAAAAAEwGwX0AAAAAAFglA+fLy7lVOvAvLAw/qupIn4H3uo7061f+/a1WbnU6WQetKFCC+c1mjtv8vDMIAAAAAABOJLgPAAAAAAB9lI7xWZvN3FsXTC8B99KBf25uvT/P/Dunp7OWzvp1f3c1sSHHp25iAwAAAAAATDbBfQAAAAAAOAkZUG+3c6t04i8d5wdptTIQ3+mUgPx6eT7591QrBWStWylgcTHr7GyOx9KSMwMAAAAAAOoJ7gMAAAAAwCnIwHoVYM9aF2BvNLKWTvwzM+fq78/fX/09Wev+nnY7n3fpsF83YQEAAAAAAFhNcB8AAAAAAE5DBtiXl3OrdOBfWBh+VNXhPgP0dR3u107+vlYrtzqdrINWACjB/GYzn+f8vFccAAAAAABOn+A+AAAAAACcgdKBPmuzmXvrgu4lMF868M/NrfXflT93ejpr6axf93uqiQj5fOomIgAAAAAAACdDcB8AAAAAANZQBt7b7dwqnfhLB/tBWq0M2Hc6JXB/ur8/j686+2et6+y/uJh1djb//qUlryQAAAAAAKwdwX0AAAAAABiBDMBXgfisdYH4RiNr6cQ/M3Oyvy+/vzo+a93x7Xb+naXDft0EAwAAAAAA4HQI7gMAAAAAwAhlIH55ObdKB/6FheFHVR3zM5A/uGN+Pt5q5Vank3VQx/4SzG828++an/cKAQAAAADA6AnuAwAAAADAWVA62mdtNnNvXXC+BPBLB/65uazT01lLZ/25ueE/p5o4kL+/buIAAAAAAACwlgT3AQAAAADgHMgAfbudW6UTf+mIP0jprH/oUNbBnfjT4mLW2dn8fUtLRh4AAAAAAM4+wX0AAAAAADiHMlBfBeyz1gXsL7po+OPtdv7c0mG/bkIAAAAAAAAwSoL7AAAAAACwDmTAfnk5t0oH/gMHTu7oF17I+m/+Tf6c+XkjCgAAAAAA64fgPgAAAAAArANTU1NTU1PT07n1uc9lvfrqkzv6vO6/9/8v/0v+nLk5IwoAAAAAAOuH4D4AAAAAAJxDGbTfsiW3Hn446/btw496/vnhj7da+XM7nd4JAQAAAAAAwLkguA8AAAAAAOdABuobjdzauzfrzMzwo9rtrJs3Z11aGv791c/P31f38wEAAAAAgFEQ3AcAAAAAgLMoA/StVm51OlkHdcQ/ciRrs7mysrKysjI/n3V5Ofdff33WhYXhv7Xq6J+/v66jPwAAAAAAsJYE9wEAAAAAYIQyKD89nbV01p+bG35UFczPoP6Jwfzcf+RI1mYz987PD/+5ZYJA6cBf93cAAAAAAABrQXAfAAAAAABGIIPxVaf7rHWd7hcXs87OZiB/aelkf19+f7udW6UTf+nYP0irlX9np1MmGHjlAAAAAABg7QnuAwAAAADAGsoAfKORW6XD/szM8KPa7Qzelw77dYH7wfL4agJA1roJANXfm39/3d8LAAAAAACcCsF9AAAAAABYAxl4b7Vyq9PJOqiDfQnmN5sZtJ+fX+u/J3/u8nJulQ78CwvDj6pWCMjnU7dCAAAAAAAAcDIE9wEAAAAA4DRksH16OmvprD83N/yoKkifwfq6IP2ZKx38szabubduokCZcFA68Nc9LwAAAAAAYBjBfQAAAAAAOAUZZK8602et60y/uJh1djYD9EtL5+rvz9/fbudW6cRfVgAYpNXK593plAkLzgQAAAAAADh5gvsAAAAAAHASMrDeaORW6bA/MzP8qHY7g/Klw35dQP7syb+nmlCQtW5CQfX8czzqnj8AAAAAABAhuA8AAAAAAENlQL3Vyq1OJ+ugjvMlmN9sZjB+fn69P7/8O5eXc6t04F9YGH5UteJAjk/digMAAAAAADDZBPcBAAAAAGCVDKJPT2ctnfXn5oYfVQXfMwhfF3xff8qKAFmbzdxbN/GgTGAoHfjrxgkAAAAAACaT4D4AAAAAAEQJ7Fed5LPWdZJfXMw6O5uB96WlcRmPfD7tdm6VTvxlRYFBWq0cx06nTIBwZgEAAAAAgOA+AAAAAAATLgPmjUZulQ77MzPDj2q3M9heOuzXBdo3rnx+1QSFrHUTFKrxzPGtG08AAAAAABhvgvsAAAAAAEykDJS3WrnV6WQd1CG+BPObzQyyz89P2njl815ezq3SgX9hYfhR1QoGOd51KxgAAAAAAMB4EtwHAAAAAGAiZHB8ejpr6aw/Nzf8qCqonsH1uqD6+CsrDGRtNnNv3USGMiGidOCvG3cAAAAAABgvgvsAAAAAAIy1DIpXnd+z1nV+X1zMOjubAfWlJSPZX45Pu51bpRN/WaFgkFYrX5dOp0yoMJIAAAAAAIwzwX0AAAAAAMZSBsIbjdwqHfZnZoYf1W5nEL102K8LoFPkeFUTHrLWTXioXp98vepeHwAAAAAA2JgE9wEAAAAAGCsZAG+1cqvTyTqoo3sJ5jebGTyfnzeCZybHcXk5t0oH/oWF4UdVKyLk61e3IgIAAAAAAGwsgvsAAAAAAGxoGfSens5aOuvPzQ0/qgqWZ9C8LljOqSorFmRtNnNv3cSIMsGidOCvex0BAAAAAGBjENwHAAAAAGBDymB31ak9a12n9sXFrLOzGShfWjKSZ0eOd7udW6UTf1nxYJBWK1/nTqdM0DCSAAAAAABsRIL7AAAAAABsKBngbjRyq3TYn5kZflS7ncHx0mG/LjDOqOT4VxMostZNoKhe73z9615vAAAAAABYXwT3AQAAAADYEDKw3WrlVqeTdVAH9hLMbzYzKD4/bwTXl3xdlpdzq3TgX1gYflS1wkKeD3UrLAAAAAAAwPoguA8AAAAAwLqUwezp6ayls/7c3PCjqiB4BsPrguCca2UFhKzNZu6tm2hRJmyUDvx15wUAAAAAAJxbgvsAAAAAAKwrGcSuOqtnreusvriYdXY2A+BLS0ZyY8rXr93OrdKJv6ygMEirledNp1MmfBhJAAAAAADWE8F9AAAAAADWhQxcNxq5VTrsz8wMP6rdzqB36bBfF/Bmo8jXs5qQkbVuQkZ1/uT5VHf+AAAAAADA2SG4DwAAAADAOZUB61YrtzqdrIM6ppdgfrOZwe75eSM43vJ1Xl7OrdKBf2Fh+FHVig15ftWt2AAAAAAAAKMluA8AAAAAwFmVQerp6ayls/7c3PCjquB2BrnrgtuMm7KiQtZmM/fWTdwoE0BKB/668wwAAAAAAEZDcB8AAAAAgLMig9NVJ/SsdZ3QFxezzs5mYHtpyUgSUYL87XZulU78ZUWGQVqtPA87nTKBxEgCAAAAAHA2CO4DAAAAADBSGZBuNHKrdNifmRl+VLudwezSYb8ukM2kyvOjmuCRtW6CR3U+5vlZdz4CAAAAAMCZEdwHAAAAAGAkMhDdauVWp5N1UIfzEsxvNjOIPT9vBDkVed4sL+dW6cC/sDD8qGoFiDxf61aAAAAAAACA0yO4DwAAAADAmsjg8/R01tJZf25u+FFV0DqD13VBaxiurNCQtdnMvXUTQcqEktKBv+68BQAAAACAUyO4DwAAAADAGcmgc9W5PGtd5/LFxayzsxmwXloykoxCnl/tdm6VTvxlhYdBWq08rzudMiHFSAIAAAAAcCYE9wEAAAAAOC0ZaG40cqt02J+ZGX5Uu51B6tJhvy5ADWsjz7dqwkjWugkj1fmd53vd+Q0AAAAAAP0J7gMAAAAAcEoywNxq5Vank3VQR/ISzG82Mzg9P28EOZfyPFxezq3SgX9hYfhR1YoSef7XrSgBAAAAAAC9BPcBAAAAABgqg8rT01lLZ/25ueFHVcHoDErXBaPh7CorPmRtNnNv3cSSMkGldOCvex8AAAAAAEAS3AcAAAAAoK8MJledxrPWdRpfXMw6O5uB6KUlI8lGkOdru51bpRN/WTFikFYr3yedTpngYiQBAAAAAOhHcB8AAAAAgB4ZQG40cqt02J+ZGX5Uu53B59Jhvy7wDOtTnr/VBJSsdRNQqvdLvn/q3i8AAAAAAEwawX0AAAAAACKiBPZbrdzqdLIO6iBegvnNZgad5+eNIOMkz+vl5dwqHfgXFoYfVa1Qke+nuhUqAAAAAACYFIL7AAAAAAATKoPF09NZS2f9ubnhR1VB5gw21wWZYWMrK0hkbTZzb91ElTLhpXTgr3tfAQAAAAAw7gT3AQAAAAAmTAaJq87gWes6gy8uZp2dzQDz0pKRZBLl+d9u51bpxF9WoBik1cr3XadTJswYSQAAAACAySK4DwAAAAAwITIw3GjkVumwPzMz/Kh2O4PKpcN+XUAZJkO+H6oJLVnrJrRU7798P9a9/wAAAAAAGBeC+wAAAAAAYy4Dwq1WbnU6WQd1/C7B/GYzg8nz80YQBsv3yfJybpUO/AsLw4+qVrzI92fdihcAAAAAAGx0gvsAAAAAAGMmg8DT01lLZ/25ueFHVcHjDCLXBY+B1cqKFFmbzdxbN/GlTKApHfjr3qcAAAAAAGxUgvsAAAAAAGMig79VJ++sdZ28Fxezzs5m4HhpyUjCmcv3U7udW6UTf1nRYpBWK9/HnU6ZgGMkAQAAAADGg+A+AAAAAMAGlwHfRiO3Sof9mZnhR7XbGSwuHfbrAsXA6cj3VzVBJmvdBJnq/Zzv77r3MwAAAAAA653gPgAAAADABpWB3lYrtzqdrIM6dJdgfrOZQeL5eSMIZ0++75aXc6t04F9YGH5UtYJGvt/rVtAAAAAAAGC9EtwHAAAAANggMrg7PZ21dNafmxt+VBUUzuBwXVAYGKWywkXWZjP31k2kKRNySgf+uvc9AAAAAADrjeA+AAAAAMA6l0HdqvN21rrO24uLWWdnMyC8tGQkYf3J92e7nVulE39ZIWOQViuvC51OmdBjJAEAAAAA1jfBfQAAAACAdSoDuY1GbpUO+zMzw49qtzMIXDrs1wWAgfUg36/VhJusdRNuqutDXi/qrg8AAAAAAJwrgvsAAAAAAOtMBnBbrdzqdLIO6qhdgvnNZgZ/5+eNIGxc+T5eXs6t0oF/YWH4UdWKHHn9qFuRAwAAAACAs01wHwAAAADgHMug7fR01tJZf25u+FFVsDeDvnXBXmAjKStmZG02c2/dxJwywad04K+7jgAAAAAAcLYI7gMAAAAAnCMZrK06ZWet65S9uJh1djYDvUtLRhLGX77f2+3cKp34y4obg7RaeZ3pdMoEISMJAAAAAHBuCO4DAAAAAJxlGaBtNHKrdNifmRl+VLudwd3SYb8usAuMo3z/VxN4stZN4KmuN3n9qbveAAAAAACw1gT3AQAAAADOkgzMtlq51elkHdQBuwTzm80M6s7PG0GgyOvC8nJulQ78CwvDj6pW+MjrUd0KHwAAAAAArBXBfQAAAACAEclg7PR01tJZf25u+FFVEDeDuXVBXGCSlRU4sjabubduok+ZMFQ68NddlwAAAAAAOFOC+wAAAAAAayyDsFVn66x1na0XF7POzmYAd2nJSAKnKq8f7XZulU78ZQWPQVqtvG51OmXCkZEEAAAAAFhbgvsAAAAAAGskA6+NRm6VDvszM8OParczaFs67NcFbAHq5fWkmhCUtW5CUHX9yutZ3fULAAAAAICTJbgPAAAAAHCGMuDaauVWp5N1UMfqEsxvNjNYOz9vBIFRyevM8nJulQ78CwvDj6pWDMnrW92KIQAAAAAA1BHcBwAAAAA4RRlknZ7OWjrrz80NP6oKzmaQti44C7B2yooeWZvN3Fs3cahMQCod+OuucwAAAAAADCK4DwAAAABwkjK4WnWizlrXiXpxMevsbAZml5aMJHCu5fWo3c6t0om/rAgySKuV18FOp0xgMpIAAAAAACdHcB8AAAAAoEYGVBuN3Cod9mdmhh/VbmcwtnTYrwvEApx9eX2qJhhlrZtgVF0P8/pYdz0EAAAAAEBwHwAAAABggAyktlq51elkHdRhugTzm80Mws7PG0Fgo8jr1vJybpUO/AsLw4+qViDJ62XdCiQAAAAAAJNLcB8AAAAAoCuDp9PTWUtn/bm54UdVQdcMvtYFXQHWr7JCSNZmM/fWTUQqE5pKB/666yYAAAAAwOQR3AcAAAAAJl4GTavO0VnrOkcvLmadnc2A69KSkQTGTV7f2u3cKp34ywojg7RaeV3tdMqEKCMJAAAAAEw6wX0AAAAAYGJloLTRyK3SYX9mZvhR7XYGWUuH/boAK8DGl9e7asJS1roJS9X1Na+3dddXAAAAAIDxJbgPAAAAAEycDJC2WrnV6WQd1BG6BPObzQyuzs8bQWBS5XVweTm3Sgf+hYXhR1UrmuT1t25FEwAAAACA8SO4DwAAAACMvQyKTk9nLZ315+aGH1UFUzOoWhdMBZgcZcWRrM1m7q2b2FQmSJUO/HXXYQAAAACA8SG4DwAAAACMrQyGVp2es9Z1el5czDo7m4HUpSUjCTBcXi/b7dwqnfjLiiWDtFp5ne50ygQrIwkAAAAAjCvBfQAAAABg7GQAtNHIrdJhf2Zm+FHtdgZPS4f9usApAMfL62c1ASpr3QSo6nqd1++66zUAAAAAwMYjuA8AAAAAjI0MfLZaudXpZB3UwbkE85vNDJrOzxtBgLWR19Xl5dwqHfgXFoYfVa2QktfzuhVSAAAAAAA2DsF9AAAAAGDDymDn9HTW0ll/bm74UVWQNIOldUFSAE5XWcEka7OZe+smSpUJV6UDf911HQAAAABg/RPcBwAAAAA2nAxyVp2Zs9Z1Zl5czDo7mwHSpSUjCXB25fW33c6t0om/rIAySKuV1/1Op0zYMpIAAAAAwEYjuA8AAAAAbBgZ2Gw0cqt02J+ZGX5Uu51B0dJhvy4gCsCo5fW4mlCVtW5CVXX9z8+Duus/AAAAAMD6IbgPAAAAAKx7GdBstXKr08k6qONyCeY3mxkMnZ83ggDrU16nl5dzq3TgX1gYflS14kp+PtStuAIAAAAAcO4J7gMAAAAA604GMaens5bO+nNzw4+qgp8ZBK0LfgKwXpQVUbI2m7m3buJVmcBVOvDXfU4AAAAAAJw7gvsAAAAAwLqRwcuqk3LWuk7Ki4tZZ2cz8Lm0ZCQBNra8nrfbuVU68ZcVVQZptfJzpNMpE8CMJAAAAACwXgjuAwAAAADnXAYsG43cKh32Z2aGH9VuZ7CzdNivC3QCsNHk9b2aoJW1boJW9XmSny91nycAAAAAAKMnuA8AAAAAnDMZqGy1cqvTyTqoQ3IJ5jebGeScnzeCAJMhr/vLy7lVOvAvLAw/qlrBJT9v6lZwAQAAAAAYnan8h04DAQAAAMBkyOBeCfKVgPjxQb53vrP/0QcPZv3mN7OWjr8lUL60pPP7yYx/GffPfa7/+B+vBDXf8Y4c37pOywBM1ufK3FxulYlgdebn8/Ok3TaCJzO+ZcWCUo+/j3rTm7L+yI/0Hv23f5v1z/6s9/O8qr0TMgAAAABgvAnuAwAAADAWegPhu3ZlLYHwUgd1ch+VxcXeunv3pAbUeidMlMB+CQDWjV8J7JsQAcCwz5nyeV8+Z+o+90vH/hLkn7zPmRy3ct9UPqfLdt3n9ForE/OOv28yYQ8AAACA8SC4DwAAAMCG0tv5ddeuiPhkxOtfHxG3RuzcOeTITVlfckPW838u68UfyXrpx7Ne/tP9j3/6B1mXr8/6d2/L+oNuF/7nfj7rC9fWPIWdEU88ERF7Iv7gD3LX+AbT8vVqNHKrdEKuC1K22zke8/POeABO/z6hBPhLIH2Q8vlbJoqNzwS7/hMbt2yJnRERP/uzsSci4sILBx1//gNZX/T/7d4tPd77+DVfHf77H3lD7/bh12T9+/8+6/M31t81RTzzTP6d5b5pcTFfp927nfEAAAAAbCSC+wAAAACsa73B71KHBfAuejjrj70465v2Zr3ygrP7l99/S9bHfiPr92azDgz2b444dCgiDkb80R/lrhJg33gdgPN1K0H9ubnh312eX+l4XDogA8CZfA6VwHr5PCr3EXWfRyXAXzq/b7TnXVYeKM+3BPZPVIL5Mx/M+lO/k3Xbo2f37953VdavfCLr3/7LrLXB/oioVk4o902Tt7IRAAAAABuD4D4AAAAA68qqwNnWiE9+MiL2R1x99arv2JT10g9lvfJXs27/i6yX7Vvfz/D4aNpffzTrCYH+zRFPPx0RByN++7fXewf63oBk6XBcgoODlGBdCUiO34oDAKynz6kykawE+euUCWXt9vp+XmWFgfL8TpygUKY1vrK73tBbm927qAvW9+v22HNZv9jJ+sSOrM/eM+woQX4AAAAA1ifBfQAAAADOqQycbdkSEe+J+NSnIuK+iOuuq77jvG9kfd2Lst780HiORAn0//GerCdE0nZGPPFEROyJuOuu9dKZftXrF1VgvwQIBykdjEtgf+OtKADARr7vKBPLyudWmXg2SPm8LUH+c/e51TtRrgT1q5VtyvTGV702a+OurOt9WuOp+u62rPd+LetTx09VeE9ExA9+EPdFRPzmb+bOjbuSEQAAAADjQXAfAAAAgLOqN3BWOt6u7gx7fOTsw2+ZzJF68I6sX+yGBZ+/8bhv2Bpx4EBE7I+49db8d74SiD9br2N53crrWBd8LIG59btyAACTdD9SJpqVAH+ZiDZIWRmmTDw7e53c8+9ttWJrRMTNN8f+iIiLLiqPv6J7t3DTM1nXeyf9tVY6899/YdYTgvybIyKefjoORkT8+q+v95UUAAAAABhPgvsAAAAAnBWrOrNf2u24fjjikkuq77h8R9Zx7Q17pj79xqzf/PusL1x74veUTsCjC6IdCw5GxOoOv/2Vjrbl7zr3KwQAwImfa8MmFA77fCsB/rWfONf7d+3dm7WaWPDS92Vt/mjWSQvq1ynTH/f+QtYT1jGKiIjdu7uj2NSJHwAAAICzQXAfAAAAgJHq7cze6VSPiJydmY99KeuTD574WAnIl8D86QfReoODpSPx9u3DjyodiEugsXQoBoCNcN9SJqaVIH+dtZs4d2yi486IiM9/PvZERFxxRVmP6J91O+rvuNNrdSpKkP8/dDvyrxzqPrA1IuLAgVzB4MYbz/ZKCgAAAABMFsF9AAAAAEZicGf2V3RD5Xf90CithftvyfrQK7OujqIdOBAR+yPe/OZTDfCvWiEhqsD+zMzwo0rH4RLY17kWgI18H1MmqpXPwTKRbZDTnziXv2/Xrgzs33dfBvYvvPD8B/Lx21+d1XpEZ2bfVVn/8Kmsz99Y3TVFHD2aAf5y32TiIQAAAABrS3AfAAAAgDXR25m9dNbftav6jmsezXrzQ0ZrFEoU7f6XZX3h2u4Dl0Z8//sRcThi+/a6IFrvCgll4kVdULHdzp87P+91AGD87m/KxLUS4C8T2wYpn7NlItvgDu6DJjqWaY7v/cdZBfbX1ne3Zf34Z7I+e0+/72o28/UrEzIAAAAA4MycZwgAAAAAOBO9gf29e7Pu2hUxtSm/ftvLswrsj9a27sSIO/9B1tKjNw5HXHJJRGyN+PKXezvpH/86luBgmXgxKLBfOgiXQJvAPgDjqTd4f/31WeuC3OVz9uGHezv3H/+5Wz5vq8D+j78ma1mXSGB/NMq4/m/dKRmX7+j3XZ1O7/0RAAAAAJwZHfcBAAAAOCMZaCodaHftqgLj73pF1hIo59y47cVZn+p20Y/NEU8/HREHI667Lnd98pNZTwwW9irBxdJBeHDnfgAY//ufErg/2WB3mehWJsB1OmWa4xv/JutNdxvbc+nTb8z6yFX9HtWBHwAAAIAzI7gPAAAAwGnp7UA6N1d12P/538sqsL++/Fo3dP/sPd0dmyMOHYqIgxGbNg0/dnExawnsl8AhALgfqjrql4mMg1as+cY3sl57bdlzTfduybpE68vd92b91uPdHVsjIo4ejf0REW9+swmMAAAAAJyO8wwBAAAAAKciA2qNbvf20mk2IuKfPZNVYH99+tAvZC0rIqwO7B882P+YdjuDaddfL7APACfKz8cywW12Nuvxge7vfCeD369+ddlz+Y6sAvvr0y3vzfqK0lt/f0TERRfFXETEnj15PzxoggYAAAAA9KfjPgAAAAAnJQNKW7ZExM6IP/3TiNgTceGFesVuNPuuyvrZd2ddOVQ9VgL8/+bf5L8bLiwYLwA41fulEui+/fbYHBHx1rfGwYiIH//xix7ORz7158ZqI/mVV2Z9/sbujq0REQcOrOxbWVlZueYaIwQAAADAydBxHwAAAIChVgXQLo1YXIxjgf3Sg1Rgf2MpKyKUFRJW27zZ+ADA6etdoea1ry2B/bLeza3nG6ON6PbuWgnnfaO7Y39ExNVX531yp2OEAAAAADgZgvsAAAAAnIRWKyIOR1xySUSJnt31Q+Oyke24M2tZMeGYSyPa7d6OwQDAycjPz0Yjt7Zvn9qUX/3KoayX7TNGG1F53W76Qfd13rT60UYjX/ft240UAAAAAMMI7gMAAADQVwaQZmZyqwTQIqroGeOhrJjw0vd1d3QnaEREzM0ZHwA4BZsjIj74wbJ59ReyXnmBoRkHZd2iV732uAfeExFx221GCAAAAIBhBPcBAAAAGOQ9EffdV21eviOr6Nl4uv4zx+3YGfHLv6zzPgDUy8/Lubk4GBGxadN538j9ZXoc46VxV9byOsd9ERHXXde74gIAAAAA9BLcBwAAAKBHBo62b4+I+yKuuy5ialM+UiJKjKcdd2a96OHujj0RF16YX7ZaxgcABt03TU/HzojVHdd3XG9sxtll+7K+7kXHPXDceQAAAAAAqwnuAwAAAHC89/QGjl712qwlosR4+5/+7MR9jUYGE2dmjA8AHG9uLvZERFx44Uvfl3vKdDjGW1lR4Vjn/T0REVdcofM+AAAAAP0I7gMAAAAQEaVjbKMRxzrtlwiSTvuT5coLsr5i4cTHdN4HgOq+aWYmNkdE/NIvlf3Xf8bYTKJtbzhux+aIiE984tiKDAAAAAAQES8yBAAAAABUVncGfV33344ue2i8n/O+q7J+5RP9H/+Hj2f9qd/Juu3RyTgX3vuPs96+KevKoYhdu0pQcWVlZWVlZXnZewaAib5vOhgRcfHFZbrbjh9OxjMvd09/8YtZ/+tr+n/fNV/tjsuYr0Bw093d8ejeGT17T54XubVrV9aFBe8ZAAAAgMmm4z4AAADAhDvWMTYiIrZsiZjalF/fPKaB/QfvyPpL/yTrv3tj1sOv6a1//dGs33q89/vKcXffO95nxmX7sl76oRMfKwE0AJhQWyMifuZnyuYbPjjeT/f+W3rvgu5/Wdb/8v7+31/upr7wvazNT2X92JeyfnfbeI7T5v9Pv73bt3vDAAAAABCh4z4AAAAAEdEbKDoW1B6znrElKvZkN0J2+e1ZG9/MWoLqx/ynLA++POsXu11Sn78267e63/Yrr8x6+6sH/JwN7spfzfpnZcd7It7ylvyy3fbeAWCS9E54vPrqMt1xx/vH8/mWu6e/7nbO3/aGrKXD/DFv6X/8p7vrFD3S7dD/5KGsd3SnR97U3T8u6xndsNJ9vj17y4pF09O5YtGRI95JAAAAAJNJx30AAAAAPhnx1rdWm696/Xg9vU93O+V/5y+z/o/dlQQ+3I2Y1QXtd9yZtQTzz3+g9/Hnb8z60W9nHbcesidE8+6LuO66EkDz9gFg8lQrz/Rbl2YclA77f/svs975DwbcFdQo6zddvqN3/wvdaZClc/+43D2Vu8qLHu73qM77AAAAAJNOcB8AAABgQq0KXt8asXNn9UjpFbrRlQjYgbdlfc2Ls55uT9cSxfqVQ/0fLwH+hdvG84zpF0GrgosAMDmqAHZZl2bc7Ptq793NHf9v1jId8lRd94H++0uA/7Njdkfxyp8bft4AAAAAMJkE9wEAAAAm2uoAUQlm13Wg3yhKgH7q81lvee/a/NwrL+gdr+OVzv7j1nn/x148/PwBgPHVu9JM9fl3qh3o17ty91IC9UXZfuSq0/u5ddMmn9gxXuP41uZxO7ZGRLzrXd5JAAAAAJNNcB8AAABgoq0OXvfvDbpxHX5N1hI1a/yrrL+2vDY/v1+QPSJi5VDWxZ8ar/E8YSWGrRE/8zPeQwBMjmqlmUHT9yCimuZ5/gPdHfsjIi66KCeAWLEIAAAAYFIJ7gMAAABMtNXB/RN6g25wz94zfP+n33hmP//ynx7++PL14zWeZSWG1RG0EkDTeR+ASTAzU74aNH1vXD7tX7Ew4O7nNDvjP/bc8Mdftnk8x/NH/m2/vVu2eC8BAAAATKYXGQIAAACASVYF0KreoOPivG9kLR33WRslgvbkqn3T08YFgPFXBa6PTd+7czyf6V0/zLrvoawv//qZ3S0+8qHhj7/q9d0vHhqzO+29J941uW8CAAAAmFw67gMAAABMmOyQvrrT50vfN57P9HUDmlaUjvE3rDgb1orOsQCMuc0REa9+ddn8yS9PxtPe9mjWM53e+dhv9N9fplne/NB4jt/FL+u3d/XEWQAAAAAmieA+AAAAwESahE6fJQL2r+/O+raXZ/3Nv8l62b4z+/nfevnwx0uP1XHT73npHAvAmDsYEbFpU9k807uISfHdbVkPf7z/4zuuH+/nv+P4FRk2R0T85E86MwAAAAAmk+A+AAAAwERa3SH90sfH+7mWHrEnRKfO0N/8fv/9U5uybv+L8RzPfr1jdY4FYDzlSkXV59y4rlM0Kvd+LevKod67pGseHc3d2bo9j7rPOyeAXHyxMwMAAABgMr3IEAAAAABMotUd0v9hCe6/xbicjMeey3p0tv/jr3pt1nHtxVsidl/4V9W+V786g43btzs/ABg/11xjDE7Og3dk/cp/7L1bKhMe3r4z67aHJmtcXnJD1mfvyZr3TVu2rKysrKysLC05cwAAAAAmg+A+AAAAwMT78e8Zg1Nx/4X995//QNYP/83kjcmmTVn37nV+ADDOjq1TNOFrzTQ/lbV00j9BN7B/0cNZ/6c/y3rlo86hyuqJtAAAAABMAsF9AAAAADgp+67K+tQbe/dPbcr6K4e6Oy4wVgDAOOu8v//+si7Rn12f9Zt/n/V/vSXrCZ33BfkBAAAAmCDnGQIAAAAAGOa727L+4VO9+0tg/+d/L+uVAvsAwEQrd0M3P5T1zn+QtaxL9Ow9WT/77qyffqMxAwAAAGBy6LgPAAAAMPGe/NPuFw8Zi37u/VrW5xtZjw/s6xVbabeNAQDj5x/9o6zvetfTH+nu+nOjcjIu25f1rXdk/UJ3/8qhrI901zO6vxv4v+luYwYAAADA+BLcBwAAAJh4hz/U/eItxmK10gP2qW6kTGA/7bvqxH2LiysrKysrK/PzzhsAxsnU1NTU1NSWLbn1rnc9//vdB2aMzanYcWfWL74y6/M39j7+UHf/9u46RyXwPy6e+/nuF90VB/K+aXHRmQEAAAAwWc4zBAAAAACTaHVQ6O/eZjxWK4H90gP2/AeyfvTfZ530DvtP/4sT9x054rwBYBxlwHpp6dhd0+eNyZn4kX87YJwPZf3srvF83i9c67UHAAAAQHAfAAAAgPjBQWMQUXWSPz6wf/urs45b79fT9cgbTty3vGxcABhrmyMinn66BMwZjSd2jOfdZS+d9gEAAAAmleA+AAAAwITJzrE9HfcnvHdsiVR99t1ZX7GQ9Tf/JuupBvYfe663TgLBfQDG3MGIiK9/vWw+eMd4Ps2y7lDzU731Y19am59/zVeHPz5ud6X91imyUhEAAADA5BLcBwAAAJhcl0Z8//sRpXfsd7dN1tMvwfoS2L/0Q1nv+uGZ/dwH/rS3jpvDrzlxn+A+AJOg+rx7+gfjeVdU1h0qd4elPvlg1v4d5E/euI1bnW+9fPh5BAAAAMBkEdwHAAAAmFyHI/burTYXf2oynnaZoPCbm7KuVWD/2LB2g+11PWU3qn69cJeWvJ0AGH9V4Pqx3xizZ/bxk/u+J64/w99Tc/xLbhivcf2b3x9+HgEAAAAwWQT3AQAAACba6sD1uEXQjlcC+x/9dtZLvpd1rQL7xbP3ZJ350HiN3/23ZC29d/P8WVlZWVlZOXLEewmA8bd7d/nq8MfH65nV3bVMbcp6zYif9xUPjtdd59HZ4ecRAAAAAJPlRYYAAAAAYJKV4FCrtSqC9v7xfK73fq37xcuzvOGDWdcqIfbIG3q3r7xgvMbv2MSOxonnDwCMt5yotrw89S+mpqamnnhiZU9ExBVX7LsqH9/26MZ+fuWu5bxvdJ9vt/P9q16b9boPdL/vDJ/nX380+t5+lYkBP1/uLPZt7PHsv47V7t0mPAIAAABMNsF9AAAAgAl1LIA2NfWpqan//J8jVm6N+ImfiHjwjvyOHXeOxzO97cVZn2r07v/CWv+ibgTt/Ae6238zXmdMv97CgvsATJg9ERF/8Ae5MTf3lU/kV9veMh5Pb8f13buk7rpEl3Zvl7Y9dGY/99NvzPrCVf0ff2P3rumyfeMxjv2mO/audAUAAADAJDrPEAAAAABMvFsj/uRPqs3jO8dvVB/7UtbjA/uj9tJ/NF6nR+klvHKou2NnxBNPlIkf3j4ATJ5q4tqxDvJjokzbvKbbWf+Rq3rvqr677fTuIg68rf/j5ffcdPd4jWO/6Y4mPAIAAAAguA8AAABA9AaJxiWC9uSD5+b3XvyR8To3Si/hY/ZUnYYBYLLkxLWlpdgZEfHEEy9cm/sfe268nufN3Q77b3t5793h7f88a1nPqHTSL+s1lVqC/p99d3fcDmU97xu9P/fmh8Zr3O6/pff5xtaIiAMHTHgEAAAAICJiKv+hyEAAAAAATLqpqan/bmrq//q/IuJgxKZNVaSq9F5lMv3SP8laookREbOzx4KLADCZ901TU1OdTm41GpfvyK8+/Jbxft4lmL58fdbDr8n6d5/v/b6X3JD1ZZuzXvmrWcets/7xyoSG3vWe2u28b5qf984BAAAAmGyC+wAAAABERAmgtVq5NTcX8dL35df/24zRmUR335v1W49X+5aX898Tf+zHjA8A7pu2b8+tvXunNuVXH/33WS/bZ4wmSVlx4X+9pd+jP/ZjOu4DAAAAEBFxniEAAAAAoNJuR8TmiKefjnj2ntx3/y3GZZJ8d1vWx3944mPNpvEBgIgMYi8u5tbu3SuH8qt7v2ZsJlHnr/vfVwvsAwAAALCa4D4AAAAAEVECaEeORMTBiA98oHpk31eNziRZuK17Rhzq7nhPxFe+0htQBAAq8/Plq6caWUsHdsbbg3dkLdNdY2dExDPP5Ea7bYQAAAAAWE1wHwAAAIAeGdBeWIiInRFPPBHxwrX5yKffaHTGWYkYfucvj3vgvoi77jI+ADDovql0VF9YKPt/903GZhLs/YXjduyJiPit31o1IRYAAAAAjhHcBwAAAGCQPRHvf3+1eeBtWb+7zdCMo/svzHqs035ELCzotA8AJ2t+vnRcPzqbe0pHdsbsrumWrMc67W+OiHj66dzQaR8AAACA/gT3AQAAAOgrA9u7d+fW4mIV6F64zeiMk31XZX2qceJjgmcAcPL3TUeOlI7rZf8XF4zNOCnTV/d99bgHDkZEfOADOu0DAAAAMIzgPgAAAAAnYXWA+8kHs376jcZlIyvRs8++u9/rncGz5WXjBACncd+0OSLi0KHnb8w9t73YqIyDj38m6wvXrt67tJT3TQumaQAAAAAwlOA+AAAAAENlEGlxMbeazeqRA2/LWjq2szGUwP5Hv919hQ9Vjy0u5us9P2+cAOB075uOHMkO7G9/e2yNiDh6tKxrc/e9xmgj+tiXsj57T3fH5oiIp5/OjXe8wwgBAAAAcDIE9wEAAAA4Kb2dRBcWqsB36dheAuGsb/d+LWvpARw7I554Ir8UPAOAtbtvWlqK/RERt95a9n/r8az332KMNoKyvlRZb+qYgxER/8P/YIUiAAAAAE6F4D4AAAAApyQDSs1mRGyNOHCgCvCXDu4C/OtT6RVbev7G1oijRyNiT8QNNxzrEAwArPF9U5n42G6X/Q+9Mqt1i9an8ro80vf1aTaPTcwAAAAAgFMguA8AAADA6dof8eY3R8TmiEOHqg7upaM768PAXrH7I37xFwXPAGD08vN2fj63FhbKtMf7X5bVtMf1oQT2y3pSvRYWeidiAAAAAMCpmcp/YDIQAAAAAJyeqampqampLVsiYmvEl78cEfsjLroo4vwH8jtuf3XWy/YZrbOpdNg/IbAfEfPz+e+CVedfAOBs3TdNT+fW3r1Zt2yZ2pRf/fzvZd32qLE6mx68I+t/uDBrmViRFhfzvun6640UAAAAAGdCcB8AAACANbEqwH9pxOJiRByOuOSSiPO+kd9x0w+yiqKNRunVW1Y8eKpx4vcI7APA+rlvGhzgv/oLWW9+yFiN0t33Zv3W4/0e3b07a7OZ909HjhgxAAAAAM7EeYYAAAAAgLWQgaalpYg4HDEzExFbIw4ciHjh2vyOz7476/23GK21VAL7H/121mOB/a0RR4/ml+94h8A+AKy3+6YjR7LOzubehYXS6f2Rq7KW9XNYW7e9OGv/wH67na9LuX8S2AcAAABgbei4DwAAAMBI9HaSbbWyNlZ1gf/x12S95b1G63Ts60b6yoSIEvWLnRFPPBEReyJuuGHVhAoAYEPcP5X7pU6n7L/o4ay3np/1sn3G6lQcP83x+Ruru6aIZ56JPRER739/3jctLBgxAAAAAEZBcB8AAACAsyKDaCXAPzdXPfLS92W9/jNZd9xptPp57Lms91+Y9anGid+zuJhVh1gA2Pj3Tdu3x+aIiD/+4zgYEXHxxVOb8vGrv5D15oeM1TBlxYLv/GXWY9McL42I+P7343BExPbtJjoCAAAAcDYI7gMAAABwVmUQbdeuiNgc8YlPRMTBiE2bqu8oQf7mj2a98oLJHKnSG3bhtqwnRM5Wabfz3/nm551hADBu901btuRWmQC5fXt5/LxvZN32hqw33T3Z4/XpN2b95t9nfeHaft9loiMAAAAA54bgPgAAAADnRAbRpqdza24uInZG/PIvR8SeiAsvrL7zFQtZb3om67gH+e++N+vjP8zaL6i/0B2TEthfXnZGAcCk3D/t2hU7IyI+9anYExFxxRXl8Ulbx+jBO7p1b9YTgvpbIyIOHIj9ERG33pr3TSW4DwAAAABnl+A+AAAAAOtCnyD/qrpaCfK/6vVZb+j+69Zl+zbWMy5Rs0e6PXL/+qNZT4icvSfiK1+JiPsi7rpL4AwA6L1/ajRic0TEJz4RByMiLr64PH7+A1lnPpj1rc2sG20a5GPPZf1iJ+vyr2d9/sbjvnFnRMQTT+SEhnLfVCY8AgAAAMC5JbgPAAAAwLqUQbSZmdwqAf5GY/ARFz2c9ZU/l3W9RNPuvyXrY7+R9fDHs/brpF+UDvrNpqA+AHBy902rJkBujoj4pV86PshflED/j/zbrNd9IOu2R8/t89h3VdavfCLrwGmNxaUREd//fhyOiGi18r6p3XZGAAAAALAeCe4DAAAAsCH0Bvm3b++tu3YNPrJE0y75XtaXfCHrpd0A/eU/nfUnv5y1rnN/6ZRflI75xeHXZH32npqn9MmI//yfI+LWiD/5k9y1e3f+e93SklccADiz+6YS5F9137Q1IuJd74r9EREXXXT8ced9I+vLXsh68Uey/sPHs/54925q5kNZ66ZHliD+0/8i67denvW/vqb3runvPp914LTGuYiI73wn2hHVfdPiYt437d7tFQcAAABgIxDcBwAAAGBD6w2mlQD/li0RsTnine+MiIP9Os2eXaVjfqkloF866wMAnO37p1WB/s0REe98Z3bo37TpnP1hmyMiDh3Kv+OP/qj3vsnERgAAAAA2NsF9AAAAAMZabzCtOH57y5aspaN/qcc7ciRrCY6V4H3ZX7ZLXVrKf38rjwMArPf7pnJfVCZGnuz2IGXiYlHuo068rzKxEQAAAIBxJrgPAAAAAAAAAAAAAAAjdJ4hAAAAAAAAAAAAAACA0RHcBwAAAAAAAAAAAACAERLcBwAAAAAAAAAAAACAERLcBwAAAAAAAAAAAACAERLcBwAAAAAAAAAAAACAERLcBwAAAAAAAAAAAACAERLcBwAAAAAAAAAAAACAERLcBwAAAAAAAAAAAACAERLcBwAAAAAAAAAAAACAERLcBwAAAAAAAAAAAACAERLcBwAAAAAAAAAAAACAERLcBwAAAAAAAAAAAACAERLcBwAAAAAAAAAAAACAERLcBwAAAAAAAAAAAACAERLcBwAAAAAAAAAAAACAERLcBwAAAAAAAAAAAACAERLcBwAAAAAAAAAAAACAERLcBwAAAAAAAAAAAACAERLcBwAAAAAAAAAAAACAERLcBwAAAAAAAAAAAACAERLcBwAAAAAAAAAAAACAERLcBwAAAAAAAAAAAACAERLcBwAAAAAAAAAAAACAERLcBwAAAAAAAAAAAACAERLcBwAAAAAAAAAAAACAERLcBwAAAAAAAAAAAACAERLcBwAAAAAAAAAAAACAERLcBwAAAAAAAAAAAACAERLcBwAAAAAAAAAAAACAERLcBwAAAAAAAAAAAACAERLcBwAAAAAAAAAAAACAERLcBwAAAAAAAAAAAACAERLcBwAAAAAAAAAAAACAERLcBwAAAAAAAAAAAACAERLcBwAAAAAAAAAAAACAERLcBwAAAAAAAAAAAACAERLcBwAAAAAAAAAAAACAERLcBwAAAAAAAAAAAACAERLcBwAAAAAAAAAAAACAERLcBwAAAAAAAAAAAACAERLcBwAAAAAAAAAAAACAERLcBwAAAAAAAAAAAACAERLcBwAAAAAAAAAAAACAERLcBwAAAAAAAAAAAACAERLcBwAAAAAAAAAAAACAERLcBwAAAAAAAAAAAACAEfr/A/Z5IzgnF00vAAAAJXRFWHRkYXRlOmNyZWF0ZQAyMDIyLTExLTA0VDExOjAxOjI5KzAxOjAwhCIu7QAAACV0RVh0ZGF0ZTptb2RpZnkAMjAyMi0xMS0wNFQxMTowMToyOSswMTowMPV/llEAAAAUdEVYdHBkZjpWZXJzaW9uAFBERi0xLjUgBVwLOQAAAABJRU5ErkJggg=="
}
},
"cell_type": "markdown",
"id": "260ee497",
"metadata": {},
"source": [
"This solution corresponds to: \n",
""
]
},
{
"cell_type": "markdown",
"id": "13875636",
"metadata": {},
"source": [
"We can check that 6 solutions exist:"
]
},
{
"cell_type": "code",
"execution_count": 9,
"id": "8efc2167",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Number of solutions: 6\n"
]
}
],
"source": [
"if solve(sols=ALL) is SAT:\n",
" print(\"Number of solutions: \", n_solutions())"
]
}
],
"metadata": {
"kernelspec": {
"display_name": "Python 3 (ipykernel)",
"language": "python",
"name": "python3"
},
"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.7.12"
}
},
"nbformat": 4,
"nbformat_minor": 5
}