{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "db0a27b8",
   "metadata": {
    "tags": [
     "COP",
     "complex",
     "difficult",
     "Intension",
     "ElementMatrix",
     "objSum"
    ]
   },
   "source": [
    "# Problem *Diagnosis*"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "67012038",
   "metadata": {},
   "source": [
    "From [CSPLib (Problem 42)](https://www.csplib.org/Problems/prob042/): Model-based diagnosis can be seen as taking as input a partially parameterized structural description of a system and a set of observations about that system. Its output is a set of assumptions which, together with the structural description, logically imply the observations, or that are consistent with the observations. Diagnosis is usually applied to combinational digital circuits, seen as black-boxes where there is a set of controllable input bits but only a set of primary outputs is visible. The problem is to find the set of all (minimal) internal faults that explain an incorrect output (different than the modelled, predicted, output), given some input vector. The possible faults consider the usual stuck-at fault model, where faulty circuit gates can be either stuck-at-0 or stuck-at-1, respectively outputting value 0 or 1 independently of the input. "
   ]
  },
  {
   "cell_type": "markdown",
   "id": "6511231a",
   "metadata": {},
   "source": [
    "As an example, for the full-adder circuit displayed below, if we assume that the input is A=0, B=0, C$_{in}$=0 and the observed output is S=1, C$_{out}$=0 (although it should be S=0, C$_{out}$=0), the single faults that explain the incorrect output are the first XOR gate stuck-at-1 or the second XOR gate stuck-at-1."
   ]
  },
  {
   "attachments": {
    "adder.png": {
     "image/png": "iVBORw0KGgoAAAANSUhEUgAABQAAAAMvCAYAAACNzn0uAAAABmJLR0QA/wD/AP+gvaeTAAAgAElEQVR4nOzdd5hU5fnw8e8uHQVsCGLDrhgVCxh7rDEmJvbYokYEfTWaxF5iTRQ7ihI0xppERey9RbHHlp+KGhURVDpLkc4Ce94/DiaG7DkzuzvPObM73891zRWzzzPnvpc5M3vOPU8BSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZIkSZJKbXmgO1CddyKSJEmSJKnpqvJOQFLZWA24CjgUaAUsAaYAk4EJS/97/NL/PxGY9J22uTnkK0mSJEmSimABUBJAe+BloE8jnz+X/y4OTgZqlj4mA1O/8/9rgLom5itJkiRJkopkAVAqL6sCvwXWIy6UvQq8SFxUC2l/4MHAMb4V8d/FwBri0YXfLRJOB6Yt/dk0YFZGuUmSJEmS1OK0zjsBSf+2MfAPoMt3fvb/iKfivgo8AjwMjAkQe7MAx0xSBXRd+ijWIuJC4LKPbwuE05f+9xTiYulUYEHpUpYkSZIkqflyBKBUPv4BbFugTwS8BPyJeMTewhLFPggYXqJjlYvZxMXAb0cXflsYnPqdn08DvsI1DCVJkiRJLZgFQKk8dCEexdaQnXdrgMHAdcTFrqZYjrgA+b0mHqe5mgWMI17HcAJxUXDi0p+N4z+bnkiSJEmS1OxYAJTKw3LATBo3LX8acDVwA00bybYOMAj4KX421KeWuBA4GvgX8MXS/x699L/n5ZeaJEmSJEnJvMmXysdzwB5NeP4UYCBwI7C4CcfpAewE7Em8OchKTThWJfm2OPjRdx4fEr8ukiRJkiRJEusC7xOv89eUxwfAjiXKqQ2wN3Af8Qi4puZWiY+pxOs2DgKOADbCL18kSZIkSRnyJlQqL62AY4hH3u0ArNDI40TAncCZxAWoUlgdOAE4CVix2CdVV1dz4okncsIJJzBz5kxqamqoqalh8uTJ//7vmpoapk6dytSpU5k2bRpz5swpUcpl6xvgXeCfwFvAK7jGoCRJkiQpEAuAUnnrAxwCHAys3YjnTycu2N1bwpy6AL8FfrP0v4uyyy67MHz4cLp27Vqw78KFC5k2bdp/PWpqav7nZ98+pkyZwsyZMxv/G5WHT4FXgZeX/u8Y4kKuJEmSJElNYgFQah5aAT8GfkW8TmBD37t3ACcDpRxatxJwIXGBsVUxT1h77bV5+OGH6d27dwnTiNXW1v7X6MIpU6b81///doRhTU0NU6ZMYcaMGSXPocQmAs8sfTxPvOuzJEmSJEkNZgFQan6+B5xHPDKwugHP+xA4ABhV4ny2Bm5e+r8FderUifvvv5+99tqrxGk0zMKFCxk/fjzjxo3jq6++Yty4cYwfP/7f/z1u3DimTCmb/TvqiKcMPwM8vPS/JUmSJEkqigVAqfnaBDgfOJTi38vfAEcBj5Y4l1bEoxN/D3Qq1LlNmzbccsstHH300SVOo7QWLFjw72Lg119/zZdffskXX3zB6NGjGT16NBMmTCCKcpmlOwZ4ALifeA1BpwpLkiRJkiS1YDsTj+4rdlfaJcDpgXJZF3i7mDyqqqqiwYMHR83Z/Pnzo48++ih65JFHossvvzw68sgjoy233DJq3759lrsMfwVcB2wb6DWVJEmSJElSGagmHtlXQ/GFo3uB9gFyaQdcX0wOVVVV0ZAhQ/Ku45Xc4sWLo88++yx68MEHo9/97nfRPvvsE6222mpZFAM/IZ4e3pgNYyRJkiRJktQMrEm8YUSxBaPHiAt2IRwBzCuUQ1VVVXTTTTflXbPLxIQJE6Innngi+v3vfx/96Ec/irp06RKqELgEGAEcSxFTsiVJkiRJktS8VANnAQsprlj0JGFGAgJsQ7ybbWoO1dXV0T333JN3fS5zS5YsiT744INo6NCh0S9+8Yto3XXXDVEM/Aa4Flgn0GssSZIkSZKknOwITKK4ItEzQIdAeawHfF4oh7Zt20bPPvts3jW53I0aNSoaOnRodOCBB0YrrbRSKQuBi4k3Dtk50OssSZIkSZKkHKwJvEvx04HbBMqjO/BeoRyWX3756O233867Blc2Fi9eHL311lvRpZdeGm2xxRalLAa+CxxOvHuzJEmSJEmSmrl2wDCKKww9BLQOlMfKFFGMXGONNaKJEyfmXXsrS6NGjYouv/zyaJtttilVIfBT4OiAr7kkSZIkSZIy0hq4leKKQjcGzGNF4J1COey4447RwoUL8663lbWxY8dG11xzTdS3b99SFAJHA8cBbQO+9pIkSZIkScrARRRXEDotYA5diUeepeZwwgkn5F1jazY++eST6LzzzovWXnvtphYCxwIHA1UBX39JkiRJkiQFdimFC0GLgN0C5tATGF8oj0rcGbgplixZEo0YMSI6+uijo3bt2jWlEPg6sH3A11+SJEmSJEmBXUPhIlAN8Q6+ofQG5qbl0KVLl+iLL77Iu67WLE2ePDm66KKLom7dujW2CFgHDA98DkiSJEmSVJauJvmGeQnxrqtSczCIwkWgkUCHgDkcSlxoSszh+9//flRbW5t3Pa3ZWrBgQXTHHXdEvXv3bmwhcCFxwXi5gOeBJEmSJEllozUwkfSb5fNyy05qmFbAExQuAF0fOI8rC+Vw/vnn511HaxGefPLJaLvttmtsIXAMsE/gc0GSJEmSpNz9hMI3yZ/mlp3UcF2Ajyk8FXS/gDm0Ap5Jy6FNmzbRBx98kHf9rMV47rnnop133rmxhcB7gG4BzwdJkiRJknI1nOJukF08X83JBsB00s/pGsIWfboDk9Jy6Nu3b7R48eK8a2ctyogRIxpbCJwOHIe7BUuSJEmSWpiVgAUUd3N8c045So21J/Ealmnn9f2Bc9ibAusBXnvttXnXzFqkhx56KNpoo40aUwh8Hlg98HkhSZIkSVJmTqL4m+KZQPt80pQa7fcUPrcPCpzDH9Pid+nSJZo8eXLe9bIWqba2Nrrxxhujrl27NrQIWAMcEPi8kCRJkiQpE29R/83vuISfH5ZPmlKjtQZeJr3YMwlYJWAOnYGv03I47rjj8q6VtWgzZ86Mzj777KhNmzYNLQT+GVg+4LkhSZIkSVJQvaj/hncs8IuEtqfzSFRqop7ALPKd4r5vWvzq6uron//8Z951shZv5MiR0fbbb9/QIuAoYNvA54ckSZIkSUFcSf03u5cBHYHZ9bQtwbWx1DydQHqRZwmwdeAc7knLYaeddsq7PlYRlixZEg0ZMiTq0qVLQ4qAi4DTAp8fkiRJkiSVVCtgAvXf6G6ytM+dCe1nZZ2sVCJPkF7keQeoDhi/B/UX1v/9ePrpp/Ouj1WM8ePHRwcccEBDRwPeTfwFiSRJkiRJZe9H1H9z++53+uyR0OfjTDOVSmcdYB7pBZ7Q61yekxa/b9++UV1dXd61sYpyzz33NHQ04P8tPZckSZIkSSprw6j/xvY33+lTTfJmIK6HpebqfNKLO2OAtgHjtwdGp+Xw6KOP5l0Tqzhjx46Ndtppp4YUAWuIvySRWqqtgVOBfsCPga2IRzG3zjMpSZIkScVbAZjP/97QLga6LdP3qnr6RcAfs0pWKrGOxBvdpBV3jgucw6Fp8bfccktHAeZg8eLF0aWXXtqQnYIXA6cHPlekrLUG7if5vK8j3jn9feAp4A5gIPBr4OfATsBGuHu2JEmSlLukzRCeqqfv5gl9pwPtski2mfBGp3k5mPTCzpeEPb+rgQ/TcnAUYH7eeuutaMMNN2zIaMCbiNdVlVqCCyn+3C/0mEv8hcubxGuw3glcQ7yW8C+Jd0ffDtgA6JzB7yZJkiRVlH9Q/4X6EQn930/of3DwTMvTqsCJwNPEhaKFxP8es4GPiEdD/ISw00jVdC+RfuN6cuD4h6TF32233fKug1W0OXPmREceeWRDCh2P4OYgKp1VgCHAAuIdykcu/f8HEf48+z9KVwBs6GMhMJ74uuN54F7i3/sS4hGGRxKvYdwXWBeLhpIkSVKijaj/ons2yTcVpyc854nQyZaZ1YFbgFqKu5GZSFxEshBYnvoQT2VLev3GEfa1qwY+SIkfvffee3nXwSreoEGDotatWxdbvHiDuHAjNUUb4GWSz7M5wD3AfoRZj+/LlNjl+Kgl/nv7IfEXOw8Rj8r9PXAKcDiwO/GMhtWI/30lSZKkFm8g9V9A35XynB7EIxCWfc5ioHvIZMvIscQ3XY25OfkI6JV9yirCU6S/docHjn9QWvyjjz467/qXoih64YUXoq5duxb7fv+UeGSS1Fj7U/zflwnAH4C1Sxj/bw2I31wf04FPgFeIC4Z/Ai4G+gP7AN8jXi9ZkiRJapbSdvXds8Bzn014XktfAL8aGEzTbzZmEd9UqLxsTfoowHcDx29Fyo7A7dq1iyZOnJh3/UtRFH355ZfRVlttVez7fdLSc0tqjEto+N+YWuB2YP0SxF+D+BzOu0hXDo9vl/Z4BrgVuIh4V+S9gU2BLo37J5YkSZLC2ov6L3AnEBe60hyV8NyRoZItE0m7IDfmsRDYMdv0VYSk4va3j90Dx/91WvyLLroo79qXlpo3b1502GGHFft+n0m8uYHUUEfQ+L8zi4hH9G/UxBx6AFeT8gWFj38/JhOPJLwNOId4ZHdvXBNUkiRJObqb+i9ery7iucsT7+ZX3/Nb6kiXwwhzo1Ap06abi6TC+LePJwPH70RcLKo3fs+ePaMlS5bkXfvSUnV1ddGZZ55Z7Pt9NrBL4PNHLc+KwBc07W9NLfGSH8uVIJ/ViTe+eon6lwPxUf9jCfA58DBwGfE1xRZAh4b980uSJEkN0wWYR/0Xqb2LPMZfE55/Q6mTLQOdgSmEuSm4PcPfQ4VVAe+RfhO3TuAcrkmJH/3973/Pu+6lZQwePDiqrq4u5v0+l8JLLEjL2pT0jUCKfYwl3iykVHoQr5U3sTH5dO/ePdp1112jzTffPFp99dWj9u3b512ky+OxiHin5VuAAcBWuDGJJElSo1XlnUAZ6k+8yPWyPgQ2K/IYPwSerufn04hvCmobl1pZugQ4P9Cx64hHAXwY6PhquMOIR8gmuQw4L2D8nsRT7eqdin/ooYdyzz33BAyvxnj22Wc56KCDmD17dqGutcQbyjwQPiu1MJsQjyLdE/gRjR899gTxrvRjSpRXW+DnxH8nN2jIE0866SQGDRpEmzZxzWvOnDlMmzaNqVOnUlNTw7Rp0xg/fjzjxo1j2rRp/35MnTqVadOmMWfOnBL9CmVlAfFag68STyd+hfhLSEmSJBVgAfB/vQZsX8/PzwauKPIYrYg3EalvCuuBwIONS63stALGA90CxriR+GZM5aEN8Y3x6gnt44iLdEsC5vACsGt9De3bt2fChAmsuOKKAcOrMd5++21+8pOfMGVKwXv1JcS7iaftuC6l6QT8GDiSeBOKVg18/hzgFEo7Cr310nzOpwG7X++yyy4MHz6crl27NjjgwoULmTZtGtOnT/+f4uCsWbOYN28eU6ZMYdKkSUydOpUpU6ZQU1PT4Dhl4Ntdil8HXgS+zDcdSZKk8mQB8L9tAHxWz8/rgLWJixvFugY4tZ6fPwb8tOGpFfQR0D7AcdO0Jx7RGNJi4KvAMdQwKy59JJlEPI0+lE5A4t3wzTffzIABAwKGV2N99NFH7LHHHkyaNKlQ18XEGwQ8Ej4rtXBrASctfTR0nb9hxGv6TS9hPm2Bs4BzKfJvds+ePXn88cfZdNNNS5hG/RYtWsTUqVOZOnUqEydOZMqUKf/+76lTpzJhwgTGjRvHV199xbx5IT/mm+QT4t2InyFej7FsE5UkScqSBcD/9gfqn774IrBbA4/Vm3jtmmUtJh49VeopK/NwwWyJPffck2effTbvNJTg008/ZbfddmPChAmFui4gnso5InhSqgSrEH8p9yviLxGKNRr4GfGXbKW0ATCUIndPX2GFFXj44YfZZZddSpxG402fPp3x48fz5ZdfMm7cOMaPH89XX33FuHHjGDduHF9//TXz58/PO80FxGtEPkj8hULBbx8kSZJaKguA/1FNPLVxrXrajqVxU4E+JF6gfFmnAoMacbw0FgAloE2bNkycOJGVV14571SUYNSoUey+++58/fXXhbrOIp7u/c/wWalCrET8Rd8pxNNyizEb+CVh1qY8ErgOKPiB1a5dO+666y4OOeSQAGmEUVNTQ01NDV988QWfffYZo0aN+vfjq6++oq6uLst06oB/EO82/BDxzsOSJEmqQHtQ/y5084h3um2MsxKO+V5Tk61H0s7FPnxU3OOWW27Je/NbFfDVV19F66+/fjGv5wzizYCkUtqMeN24Yj9X6ojXAg5hDeK1TQvm0apVq+jOO+/M++1bEnPmzInefvvt6Pbbb4/OOOOMaO+9947WXnvtLP9WfACcRv3rNUuSJKkF+wv1XyDe24RjrkG8oH19x+3dlGTrYQHQh4+lj7333jvve1sVYeLEiVGvXr2KeU3HA+sglVYVcAzxkhzFfr78kYZvKlKMauCqYnKorq6Obr311rzfvsHMnTs3evvtt6OhQ4dG/fr1izbffPOodevWIf9mLAIeBQ4gXqNRkiRJLVgnYC71Xxj+pInH/nvCca9r4nGXZQHQh4+lj3bt2kXffPNN3vexKsLYsWOjHj16FPO6fky8jptUaqsCT1D8Z8zdFD99uKGOBOYXyqG6ujq644478n77Zmbu3LnRG2+8Ed1www3Rz3/+82i11VYL9fdjKnA9sHGg11eSJEk560f9F4JTaPpF/jEpx27TxGN/lwVAHz6+83jkkUfyvmdVkUaOHBmtvPLKxbyub5D9bueqDFXE6wIuoLjPmIeAdoFy2RaYXCiHNm3aRE899VTeb9/cfPbZZ9Ftt90W/fKXv4zWW2+9Uv8NqQOeBfYlHp0pSZLU7LkJSOxlYKd6fv4ucEcTj90JuCyhbT/iXelK4VjCjUhI0gv4deAYs4EziS/GVV5aA1eTvPnMO8AtgeNfQ0JB6KSTTuLGG28MGF6l9NZbb7HHHnswe/bsQl3vBQ4nvkmXSq0vcD+wZhF9HwEOJF7qo9TWB55a+r+Jll9+eUaMGMHWW28dIIXm5fPPP+fZZ5/lmWee4YUXXmDOnDmlOvRo4qnftwEzS3VQSZIkZW9d4uJSHqOUHszg9wupLfHFcMh/o9sz+23UGHeR/NpNJ8xaWd/1YFL89ddfP+8BKmqgv//971H79u2L+Vy4KPB5pcq2GvHO08Wci7cS7svUVYEPC+XQrVu3aOzYsXm/fcvKwoULoxEjRkSnnnpq1LNnz1Jdj8wAfgd0CfR6S5IkKbBLyKf4FwELgZXD/4pBDSbsv9H22f0qaoRDyPf1G5AWf9SoUXnfh6qBnnvuuahdu3bFfDb0D3xuqbItDzxGcX+nrgmYx4rEo6lTc9h4442jmTNn5v32LVsffvhhdPnll0c77LBDKa5L5hCvE7hawNddkiRJJVYFjCG/AmAEnBz8twyrG/E03RD/NqWaHq1wOgO1JL+Gfwgcf+2U2NGQIUPyvu9UIzz44IPF7PpZC+wa+PxSZWtFvIxBMX+vzgiYR3dgVKEcDjzwwKiuri7vt2/Ze++996JTTz016tatW1OvUb4BLsXNiSRJkpqFXcm3+BcRrzPY3J1K6f9d5gAbZPlLqNFeJvl1fCeD+Ik3xvvvv3/e95pqpKuuuqqYz4lJxEVgKZQqYBCFz8U64hHRoawHTCyUx1VXXZX3W7fZqK2tjR555JFov/32i9q2bdvU65ULgI4BX39JkiQ10Z3kXwCMgM1C/6KBVQH3ULp/jzrgoEx/AzXF+SS/lksIP839xqT4q6yyiiNimrHjjjuumM+LD3BNLoVVBQyl8Lk4E9gkYB69iUedJebQtm3b6J133sn7rdvsTJkyJbr88sujNdZYoynXLl8DR+IGe5IkSWVneeJvbeu7iAu1s23SOj5XB4qXpfbAwzS9+LeIeF03NR99SH9Nfxo4/s/S4n/yySd531uqkWpra6Ndd921mM+NJ4DqwOeZKls18DcKn4ufES+NEMo+wOK0HDbYYINo9uzZeb99m6Xa2tronnvuibbddtumXMe8CewQ8ByQJElSAx1D8oilUAs7n54QcyLQOlDMLFUDvyf+N2zMRfNkXNOrOaoGppL8ul4ROP7KpOzkfeutt+Z9T6kmmDVrVrTZZpsV8/kRer1JqQ3wOIXPxXsD53FmoRyOPvrovN+6zd7rr78eHXbYYY2dHlwHDAd6BD4XJEmSVIQR1H/R9kLAmGuSXKj4ccC4WesLvEjxF8oLiXfUcyHt5utBkl/fNzKI/2lS/P79++d9H6km+vTTT6OVVlqp0OfIEuCHGZxrqmzLAf+k8N+10CPZ/1ooh4ceeijvt26LMHbs2Kh///5RmzZtGlMInLn0XHBasCRJUk56klyI6x849isJcYcHjpuHXUgfLbEEOAdYK68EVTKnkfw61xJ+cfRbk+L36tUr7/tHlcCrr74atWvXrtDN9gzizRKkkNYAxpN+Ls4j7Pq+yxNPN07MoUePHtHMmTPzfuu2GGPGjImOO+64xhYCR+DGZpIkSbm4kORCxUqBY5+UEHtBBrHzsC/JF8QLcsxLpfV90m9+fhA4/oCk2NXV1dGMGTPyvndUCfzpT38q5kb7beI1SaWQ+hD/DUs7F/+PeNpwKFsTj6BPzGHAgAF5v21bnC+++CLq379/1Lp164YWAecBZwc+JyRJkvQdVcBo6r84ezyD+KuSvID3iRnEz5oFwMrQDphP8mt9TuD430uJHY0YMSLve0aVSL9+/Yq50f5T4PNNAvgVhc/FiwLnkLS2cAREVVVV0Ysvvpj327ZFGjlyZLTXXns1ZjTge4TdLVqSJElL7UzyRdkRGeXwbEL8tzKKnyULgJUjaXp7BAwLHLsamJ0Uf/DgwXnfK6pE5s+fH2211VbF3GQfE/ick6DwWnyLiNfFDaWa5DWNIyDaeOONo9ra2rzfui3WCy+8EPXu3buhRcAFwFm4e7kkScpQJV54HJPw8/nAIxnlkLRDYB/8VljN1+spbVsEjl0HfJDU+P777wcOr6y0b9+eRx55hK5duxbqOpSwa7BJACcDY1LaWwM3Eu56qw44gZQv1D755BNuu+22QOG166678vbbbzNo0CCWW265Yp/WDriceP3nlrj8iyRJUu46ArOo/9vY+zLMYwWS1+25IsM8suAIwMpxKMmv9RLiRetD+mNS/D59+uQ9SEQl9sILL0StWrUqNMpmJK4HqPC2JXlpj28fxwfO4ey0+KuuuqobgmRg7Nix0T777NPQ0YBfE36dXEmSpIrzC5IvwPbPOJdHEvIYD7TKOJeQLABWjo1Jv8nZLnD8E5Nid+zYMVqyZEne94YqsQsvvLCYm+uBgc87CeAG0s/DSUCXgPFbAx+l5XDGGWfk/ZatGPfee2/UvXv3hhQBFwOnBTw/JEmSKs7fqf/CaybxdIwsHZaQSwTsnXEuIVkArBytgLkkv94nBI6/Q0rs6F//+lfe94Qqsbq6uuiAAw4odGNdB+wT+NyTlieeCpx2Ll4bOIe90uJ36NAhmjBhQt5v24oxffr06LjjjouqqqoaUgi8m3i2iiRJkppgLeIbwfouuO7IIZ/lSC6WJK0R2BxZAKwsb5H8eg8NHLsLye/xaPjw4XnfDyqAyZMnR926dSt0U/01rrOl8FILcEAtsE7gHJJmF0RAdMopp+T9lq04zz//fNSjR4+GFAHfy+A8kSRJFagq7wQytBXw04S2h4A8dgk4mvov8ubTctYC3Bd4NKFtIa7P1dL8GeiX0PYqsFPg+GOAnvU1XHbZZZxzzjmBwysPTz/9NPvssw9RFKV1ux84OKOUVLkeAvZLab+L+G9/KBsAHwJt62ts3749o0ePpkePHgFT0LJqamro168fjz6adDn0P6YRzxR5LlxWkiRJUmk5ArCy/Jrk13tSBvGfSYrfr1+/vAeCKKCzzjqrmJE1/y+Dc1CVbQ1gDsnn4BLC74o+JCV+dPLJJ+f9dq1IdXV10ZAhQ6IOHToUOxJwMXAOlfVlvSRJkpoxC4CVZR/Sb2g6BY5/U1LsXXfdNe/7PwW0YMGCqHfv3oVuqGfj1DqFdynp5+HwwPFXJ55JUG/8jh07RjU1NXm/ZSvWhx9+GG222WYNmRJ8B9Am8DkjSZIqQHXeCUhqUUYXaF8/cPzPkxpGjy6Umpqzdu3acf/999O5c+e0bssDf8O/fQrrKmBGSvuBxMuShDKe+MuQes2bN4+hQ0Mvyaokm266KW+++SZHHnlksU85GniM+PNLkiSp0bwJklRKY4inuCVZL4P49Ro/fjy1tbWBwytP6623HldddVWhbtsBAzJIR5VrJjAwpb0KOC9wDpcTbzRWryFDhrBw4cLAKShJhw4d+Mtf/sKgQYNo3bp1MU/5ITAC6B40MUmS1KJZAJRUSrXEO64myW0E4JIlSxgzJrE+qBZiwIABHH744YW6XUP4c1GVbSgwJaX9Z8C6AeNPBu5Mapw0aRJ33313wPAqxm9+8xuee+45unbtWkz3rYHXgQ3DZiVJkloqC4CSSi2xCEeOIwABC4AV4oYbbqB799SBMh2BP+Li+gpnDumjAFsBvwmcw/VAXVLjoEGDAodXMX7wgx/wzjvvsPXWWxfTfR3gNWCbsFlJkqSWyAKgpFL7IqWtZ+DYs/ywN2YAACAASURBVICapMZx48YFDq9ysNJKK/HHP/6xULc9geMySEeVayjxSLwkxwFFDf1qpM+AJ5MaR44cyZtvvhkwvIq11lpr8corr3DggQcW030V4Dlg27BZSZKklsYCoKRS+zKlrUcG8ccnNUycODGD8CoH+++/P0cddVShboMIPypVlWsh8OeU9g7ALwLnkDrM77bbbgscXsXq0KED9913HyeffHIx3VcAngW2D5uVJElqSSwASiq1tCpbFgXASYkNkxKb1AINHjyY1VdfPa3LcsAtOBVY4QwhLgQm6Rc4/gvAB0mN9957L3PnJu4VooxVV1czePBgrrjiCqqqCn4sdQaeBnYOn5kkSWoJLABKKrW0AuAKxKNeQkqccjd5ctpsPLU0Xbp04brrrivUbVfglxmko8o0Ebgnpb0X4Udx3ZTUMGvWLIYNGxY4vBrqzDPP5MEHH6RDh4J/LjsRjwTcN3xWkiSpubMAKKnUCs2z7RY4/oSkBqcAV56DDjqomF2BrwNShwpKTXB9gfbQa1EOI2UU4p13Jm4WrBztt99+PPbYY3Tu3LlQ13bAvcTrmkqSJCWyACip1ApV2VYLHH9KUoMjACvToEGDWGWVVdK6dAKuyCgdVZ73gLTdNg4FVgwYfzrwSFLjq6++yvjxiUunKke77747zz//PCuuWPD06Ag8jGsCSpKkFBYAJZVaDbA4pT10ATCxAOkagJVp1VVX5YYbbijU7XDi6cBSCHektHUADgoc//akhrq6Oh566KHA4dVYffr04fnnn2ellVYq1LUj8DiwWfisJElSc2QBUFKp1ZEyCo/wU4ATh/nNnTvXBe8r1KGHHsoBBxyQ1qUK+CPQNpuMVGHuAealtB8SOP5zpCyP8MADDwQOr6bYaquteOGFFwqNZIZ4JOkzwLrhs5IkSc2NBUBJIaQVAFcIHHt6WuPMmTMDh1e5Gjp0aKGpdBsD52aUjirLN8DwlPYfAF0Dxl+SFv/ll19mwoTE+qDKwBZbbMFrr71WaGdziEfZvwSsHT4rSZLUnFgAlBRCWpWt4IrmTfRNWuOsWbMCh1e5WnXVVbn00ksLdTsb2CiDdFR5/prS1ho4OHD8h5Ma6urqePzxxwOHV1NtuOGGPPfcc3Tv3r1Q1zWARwn/hZskSWpGLABKCiGtCNclcOzUCp8FwMp2/PHH8/3vfz+tSzug4IKBTdAa6AX8EDgGOADYDii4wJeavRdJHx0dugD4Slr8Bx98MHB4lcImm2xS7HTgzYnXBOwYPitJktQcWACUFEJalS30CEALgEpUXV3NkCFDaNWqVVq3PSn9mmy7A8OIN8n5CHiaeGOGB4DXl/78beAswr9HlI8lxKOykuwIrBw4fuIowJdeeon58+cHDK9S2WSTTXjyySfp1KlToa47AH/B631JkoQXBJLCyHME4GIg8S7WAqC22mor+vfvX6jb1cDyJQi3OfAs8DxxUTHp/K8CtgEuBz4HTgZSq5RqltLWAWxNXHwOKXG3jwULFvDyyy8HDq9S6dOnDw8//DDt2rUr1PUAYGAGKUmSpDJnAVBSCHmOAISUAuQ336QuEagKccUVVxRaTH9N4PwmhjmeeFRfQ4s6XYHBxDu3Fpznp2blBdI3Kto7cPyXSNmN+Nlnnw0cXqW02267cc899xQa0QxwJtAvg5QkSVIZswAoKYS0AmDoEYAAsxMbZic2qYJ07tyZyy67rFC3U4CejQxxFXAT0LaRzwfYFXirCTmo/CwGnkpp34ew12YLiYuQ9XrqqbTUVI72339/7rrrLqqrC542NwP7ZpCSJEkqUxYAJYWQVgAsuGhRyPhz5szJILyag1/84hfssssuaV3aA1c04tAnA6c3Kqn/tQ7wGNm8b5SNtCpbV2DLwPGfT2r45JNPGD9+fODwKrXDDz+cyy+/vFC3VsBdwCbhM5IkSeXIAqCkEBaktBVcsKgEFiY1LFq0KIPwag6qqqq46aabaNs2dZDewcSbMxRra+DaJiX2v75H2J2Jla1ngLqU9tDTgBPn+UZRxIsvvhg4vEI444wzOPHEEwt1W4F4Z+Cu4TOSJEnlxgKgpBAWp7S1yTO+BUB918Ybb8xvf/vbtC5VwI0UvyHHIOLNHErtKKBPgOMqezXAP1Padw8c/1/A10mNr7/+euDwCuX6669nr732KtRtXeLNYLL4WyxJksqIBUBJIaRV2bK46UiMv3hxWm1Slei8885jtdVWS+uyBcUtoL8nsFNJkvpfVcAlgY6t7D2d0rYt4T8nE7f7feONNwKHViitW7fmvvvuo1evXoW67gRcmUFKkiSpjIQYpSBJaQXALD53EuM7AlDL6tSpExdffDEDBgxI6/YH4qmbaetbht5lcy9gQ2Bq4DgK752Uto7ALsC7AeO/BxxRX8PIkSOZPXs2nTq57GRz1KVLFx577DG23XZbampq0rr+BvgHMCybzCRJUt4sAEoKIe8RgE4BVoP069ePm2++mXffTay5dAXGZpdRvaqBT3POQdl4Lq/AS5Ys4Y033ihmKqnK1LrrrsvTTz/NzjvvzLx589K63gGMIn1KuiRJaiGcAiwphLzXAHQKsBqkurqaq6++Ou80pLLw5ptv5p2Cmmjrrbdm6NChhbq1B/6Gu4xLklQRLABKCiFtmF0rwn/2OAJQDfaDH/yAfffdN+80pNy5DmDLcNRRR3H66acX6rYxcCvxOqOSJKkFswAoKYRCVbbQyw84AlCNcvXVV9O2bdu805By9d577+Wdgkpk4MCB7LLLLoW6HQykbocuSZKaPwuAkkIoNJKgLq/4VVUOclCyLl260KpVq7zTkHI1ceJEpk51r5mWoHXr1gwbNowePXoU6noFsH0GKUmSpJxYAJQUQto6fxHpawQGjd+mTRZLEKq5uuaaa5g/f37eaUi5e//99/NOQSXSrVs3HnroIdq1a5fWrTXxjsArZZOVJEnKmgVASSGkVdmymIObGL91azc/V/2mTJnCkCFD8k5DKgsffvhh3imohPr27csVV1xRqNsawPUZpCNJknLgnbCkENIKgFnswuEIQDXYoEGDmDdvXlqXB4CbUtqvB3qVNKn/9Wvg48AxlJ2jgSMT2qYARwSOPwj4Xn0NjgBseX7961/z/vvvc/vtt6d1OxL4O3BHJklJkqTMWACUFIIFQDUr06dPLzT6bz7wK2BSSp/bgatKmdcyxgM3En4NTWWnC8kFwFWBfwLTA8Z/hYQCoCMAW6bBgwfz1ltv8dFHH6V1uw4YAYzNIidJkpQNpwBLCiHvAmDilxsWAFWfwYMHM3v27LQut5Je/AO4DZhZsqT+1yAs/rU0Iwu011ucK6EPkho+/vhjoigKHF5ZW3755bnvvvvo0KFDWrcuwF8Bd0SSJKkFsQAoKYS8C4COAFTRZs2axY033pjWZRFwTRGHmg4MLElS/2ss4AKFLc/nwNyU9o0Dx08cBjZv3jwmTJgQOLzy0KtXL66++upC3XYAfpdBOpKk0qkCNgeOA/4EvA58Qvwl9gJgIfH16lfA+8AjxF8w/4p4J/j22aesLDkFWFIIZVsAdBMQLeuaa65h2rRpaV3+QvFT4a4DDgC2bWJa37UE6E984aaWpY74wnzrhPb1A8f/LK1x9OjRrL766oFTUB5OPPFEXn75ZYYNG5bW7QLgZeDFbLKSJDVSV+BYYACwboG+bYEVgTWJi4XftYi4MPgy8DjxUiFZbOCojDgCUFIIy6W0zc8gfuK3V+3b+8WW/mPKlCkMGjQorcti4LIGHLIW2B/4uil5LeN04PkSHk/l5fOUttAFwCmkjEAcM2ZM4PDK0w033ED37t3TulQTr23aOZuMJEkN1Jp4tPbXwOUULv4V0gbYBjgVeAGYCgxt4jFVRiwASgqhS0rbNxnET7xZ6dzZ+xj9x8CBAwut/XcPMLqBh50I7EzK+mpFWgScSDyqUC1XngXAiJTz+/PP01JTc9e1a1eGDRtGq1apS/2tTTw9TJJUXjYG3gR+D7QLFGMF4EeBjq0cWACUFEJalS2LAmBiAdICoL41evToQjv/1hJPgWuMscRraN1BXGRpzPN3x29dK0FagXk94vV8Qkoc5ucIwJZv55135uSTTy7U7ZfEn0eSpPKwDfAasFXeiah5cTEsSSGkVdlm5Rm/S5e0wYmqJBdddBGLFqUuSXkrxa/9V585xDfOfySeRrxHEc+ZSjyFYwjxQs1q+dIKgB2B1YCQu3EkDvNzBGBluPLKK3njjTd48803k7pUAXcBmxJ2p3NJUmFrAU8AKxXoN4e4SDiS+G/9LGA28VJNKy19bAr0IfyMA5UJC4CSQkirsoUuAHYk5bPNEYACeP/997n77rvTuswjnlJRCm8DexLvrvZaSr9jgb+SzUY5Kh+FppivS9gC4BdJDWPHjg0YVuWiTZs23HTTTfTt2zftS5EewKXASdllJklaRhVwJ7BqSp8PiT+vHyW+ni3GisTXqgcB+5C+nruaMacASwohzynAqUP8LAAK4IILLqCuri6ty2DitfxKqdDGIP/A4l8lmkD65khrB47/ZVLD1KlTC42SVQvRu3dvzj777ELd/h/wg/DZSJIS7E/y53AEnAv0Bu6l+OIfwAzgPuAQ4h2FDwVeb3SWKlsWACWFkOcIwE5pjRYA9c477/DYY4+ldZkFXJ1ROlIEjE9pXy1w/MRCd11dHZMnTw4cXuXiggsuYOutt07rUkW8rmnq31lJUjCnprSdAAwEljQxxnxgGPFa1n2Ii4lqISwASgphxZS20AVARwAq1WmnnUYUpe7LcQ0wLaN0JEgfbRq6ADgptXFSarNakNatW3PbbbfRtm3btG5rA1dmlJIk6T/WIi7K1ecx4E8BYr4DFBwerubDAqCkEHqktE0JHDtxTYyqqioLgBVu+PDhvPzyy2ldpgCDMkpH+laeBcCpQOJ8eAuAlWXzzTfntNNOK9RtAPD9DNKRJP3HLiltV2WWhZo1C4CSSm050tcALPW6astKvFleeeWVadOmTeDwKlcLFizgzDPPLNRtIPEOaVKW0qps3QPHXgTUJDVOnBj6I1vl5pJLLmGrrbZK61IN/BnwD6okZWezhJ/PAF7NMhE1XxYAJZVaoZvV3AqAPXqkDUxUS3f55ZcX2tX0U2BINtlI/yXPEYAAiQv9uQZg5WndujVDhw6lVatWad02BX6VUUqSJFg94edfE68nLBVkAfB//Zn4DdSUx1zii/lPgJeId5M8Ftgow99Dykuhm9UJgeMnFiC7dw89kEbl6ssvv+TKKwsuW3U67sKrfORdAEwcgegU4MrUt2/fYqYCXwyskUE6kqR4llV95maahZo1C4BhdCQuQmwE7AycDNxKXBB8i/gb0465ZSeFlXazuoB4mHou8VdbLYv7aJWjc845h/nz56d1eRp4PKN0pGWlVdm6AKm7MpRA4jC/adPcD6dSXXzxxWy88cZpXToB12WUjiRVunkJP++aaRZq1iwAZq8PcAPwMbBvzrlIIaRV2bIYStItqcERgJXpzTffZNiwYWldlgBnZZSOVJ+pBdpTdzcvgcQvZmbNCr1xu8pV+/btueWWW6iqqkrrdiCwX0YpSVIlS1qvdz0sAqpIFgDzszbwKHBN3olIJZa0PgVkUwBMLEBaAKw8ixcv5oQTTqCuLnGTU4BbgA8ySkmqT6EqW+jtyxPjWwCsbDvuuCPHHHNMoW6DgeXDZyNJFe2rhJ9XAf2yTETNlwXA/J1KPCJQainWS2kbFzh2NZC404dTgCvPddddx3vvvZfWZSZwQUbpSEkKVdlCjwBM3PnaAqCuuuoqVllllbQuawIXZpSOJFWql1LazgV6Z5WImq/WeSfQjIwDziiiXyvib0FXBDYBtgF6FXjOr4C/Aw83JUGpTKyf0jYqcOw1gXZJjeuuu27g8Cono0eP5oILCtb2LqDw9EsptG8KtDsCULlZeeWVueyyyxgwYEBat98AfwNSv3GRJDXau8TTgOv7RqYT8ALxZ/FfcFdgqWhJuwB/2IRj9gLuSjjut4+vaJkbg+xL8u+8IMe8FEYV8UiSpNc89PD0XVNiR1OnTo1UOX784x8X2rH9E8JvrvBdaxbIZ5MMc1H5WUDyufGzwLGPSIq90kor5f1WVhlYsmRJ1KdPn0Kfqc8GPk8lqdKdT/rncAR8CvwW6JlPiipnTgHOxsfAUcQLJS9K6LMm8JPMMpLC6Eb6OkCfB46fOPpwhRVWKDSFSS3I3XffzRNPPJHWJQKOA2qzyUgqKG2onSMAlavq6mpuvfVW2rRpk9ZtT+CAjFKSpEp0PYVnrmwIXAuMAT4iXuv6WGBTrP9UPE+AbD1I+k6T+2eViBRI2vRfgNGB4yeuP+j038oxY8YMTj311ELd/gy8mkE6UrHKsgC4ePFi5s2bFzi8moPNNtuM448/vlC3y8l2ZLUkVZJZwEEkDypaVi/iL7xvJZ7R+A0wAriSeKbeCqVPUeXMAmD2biB5I4Qds0xECiCtyrYAmBA4/jpJDRYAK8e5557L5MmT07rUEC+WLJWTxI04CL/D6py0xvnz5wcOr+biD3/4A927d0/rsgFwSkbpSFIlepl4dmFj/jgvD+xCvLfBo8A04J/AxaTfx6mFsACYvcXA4wlt3YjXUJOaq01T2r4A6gLHTxyBaAGwMjzzzDPcfPPNhbqdQVwElMpJ2rf5qfMuA8dm0aJiBxqopevSpQuDBw8u1O1CoEcG6UhSpboX2J6mL69UDWxJvCne58CLxMs5qIWyAJiPTxJ+3gZYKctEpBLbIqXtX4FjtyJlEwULgC3fjBkz6NevH1GUuvHZCODObDKSGqRsC4CLFy8OHF7NycEHH8wuu+yS1mV54NKM0pGkSvUe8eCLU4DUqS9FqgJ+QLyh0xPEawmqhbEAmI/pKW2hR0ip8dYk3sX2auCvwJPAbcRDpn8GLJdfamVjq5S2/wsceyOgQ1Lj9773vcDhlbdjjz2W8ePHp3WZD/Qn3gBEKjdpRbjWgWOnVvgcAahlXXfddVRXp95GHAX0zSgdSapUtcRLjK0DHA48RYG/6UXaB3h76f+qBQl9Qan6JS22GREvzKnysidwEfEw6zQLgPuIp76MDZtSWeoBdE1pfz9w/M2SGqqqqiwAtnDDhw/n4YcfLtTtcsLvRC01VtmOALQAqGX17t2bY445httuuy2pSzVwHbADfukiSaHNB+5Z+lgZ2JV4rb9daPzuv52Bx4gHwNxRkiyVOwuA+UgaTjsaRwCWk7WBPwF7Fdm/PfE33j8HBhEXAmvDpFaW0qb/QjxMPZf466yzDl26dAkcXnn56quv6N+/f6Fu/8ApaSpvad/Yhy4Apo4WcAqw6nPZZZdx//33M2tW4ibS2wHnAM9kl5UkNRuLgA8CHHcacP/SB8TLMvQmnqm1JfHGo4nrpi+jGrgJ+Bh4q7RpKg8WALNXDfw4oc03VfnYlXg03yqNeG474GziD9eDKM2aDM1B75S2GpJ3vy6VxBGAm22W2KRmLooiTjzxRL75JnXw9ALiby+XZJOV1CiOAFSz0q1bN0477TQuvPDCtG6X4pcvklSfyUDqtuolMgd4denjWz2Ip/ceCexM+kak7YBhxMstVdLglhbJNQCzdyzxHP363JdlIkq0B/H6CY0p/n3XjsArJThOc5FWAByZQfzEEYC9e6elpubsqquu4oknnijU7Qziby6lcuYagGp2zjjjDNZaa62805AkNcwE4M/Em35sSby2fZqewNFhU1IWLABmazfg+oS2z4l321G+NiAuxLYr4fGGUxmjbXdIaQs9/bcrsEZSoyMAW6a33nqL888/v1C3EcAfw2cjNVlaES7XAqBTgJWkQ4cOnHfeeXmnIUlqvPeJZyieTPpyZGdmk45CsgCYjTWI14R7BuhYT3sEnEBpduxR41UBtwMrlvi4PyD+QG3J1gNWT2l/I3D87UgZur7FFoWWJ1RzM3PmTA499FBqa1NnIswCfolrq6p5SCvyhZ6+nlpgbN26Er7DUmO9/PLLeacgSWq6G0kv8q1P8WsHqkx5RVe8TsBPiuhXTbzQ5grAxsA2wPdJn1d/AvD3piaoJtuf9FFsTXE+8e5JMwIdP287Fmh/JXD8nZIaVl11VdZbb73A4ZWlKIo4/PDDGTNmTKGuJ1GZO3KreUpb5y/0HNzU68E2bUIvQajmatSoUdx77715pyFJKo1riaf6Jk2f2o145qKaKQuAxVuLeBvsUvoaOA54tsTHVeOcFfDYKxIXegcGjJGntMLpaGBS4PjfT2z4/vepqkqrv6u5ueGGG3jqqacKdXsA+GsG6UilkmcBMLXCZwFQSX7/+9+zZIn7K0lSCxEBQ0lePmeTDHNRABYAszcdeI14J53hlG4nnS0pzyndacOEq4Cts0qkgO5An8AxjqLlFnt3T2n7lLCvc1ugb1Lj9ttvHzC0svb2229zxhlnFOr2BfGuv1JzYgFQzcpnn33G3XffnXcakqTSejGlrVI2t2yxLABmbxrxsNkvKO022q8BHUp4vCy0Bd7JO4kMbUxl/b7f2mfpIxc77BBqVreyNmnSJA444IBC6/4tBH4OfJNNVlLJWABUs3LFFVcUGv13CXBdRulIUnNTrmtUj0tpWzmzLBSEBcDsbQD8dunjFeBc4NVcM5JaqLZt27LNNtvknYZKYOHChRxwwAGMG5d2TQLAGVRmoV3NX9muAegmIFrWmDFj+Mtf/pLWZTpwNTA7m4wkSSWyIKXNNR+auXKcMlpJdgJeIl4XrlXOuUgtzlZbbUX79u3zTkMlcMIJJ/DGGwU3k34QuCGDdKQQHAGoZuPaa69l0aLU0/KPWPyTpOaoW0qbM2yaOQuAxfuIeM26Yh5tga7ARsCBxAW+LxKOWw2cDdyJr4dUUnvssUfeKagEBg4cyB133FGo2yfEu5ZJzZUFQDULY8eO5ZZbbknrMgen/kpSc7V5StuYzLJQEBacwlgE1ACfEY9IOZd4M4yfAeMTnnMEcFUm2UkVYs8998w7BTXRM888w/nnn1+o23zgSOKbTqm56pzSFnok1fJpjR07dgwcXs3JxRdfzMKFC9O6DCVe81qS1PwcktL2fmZZKAgLgNmJgEeBzYCRCX1+A+yYWUZSC9a5c2e22267vNNQE4wcOZJDDz200CLzEfBL4N1sspKCSSsAhp5ykxi7bdu2LqWgf/v4448Lrf03H7g2o3QkqZIcBITe3XAz4oFJ9akjXr5MzZgFwOzNAH5E/SNVqvGiSSqJ3XbbzWlrzdjYsWPZe++9mTlzZqGufwCGZZCSFFpaAXBW4NhdEhu6JDapAp199tmFvpS5DpiUUTqSVEl6E28e+jiwfYDjdwX+RvKyIM8DUwPEVYbc1i0f44HrgfPqaesDbAu82cBj9iBef7Dc7A3cndC2EFgtw1zSrAh8Stj3xMvAfgGPn7XvEf9OSX4PDAoYvxcpO2jvvffeAUMrpClTprDXXnsxYcKEQl0fAC7MICUptI6kr8OX2wjAzp3T6pKqJK+99hqPPfZYWpfpwJUZpSNJlerHSx+vEy+5cD/pO/cWY0vgXmDDlD7XNDGGyoAFwPz8lfoLgBAP721oAbDgMJmcFFqTa0YmWRQ2A3iG+MM0lL9QPr9vKeyT0hYBdxD2990rrfGHP/xhwNAKZfbs2eyzzz6MGjWqUNf/I970IwqflRRcoWF2oUcAWgBUQWeffXahLldRvtejktTSbL/0MYR4qbFHgBeIv4wp1nZAf+Jr6rTZoU8CzzYuTZUTC4D5+YR4ikT3etpCz+1X/S4hLmqFGEk5GrgrwHHzUgX8PKX9nyTvfF0qByY1bLHFFvTs2TNweJXawoUL2W+//Xj33YLL+U0i3lRpbvispEwUqrKFHgHYKanBAqAAnn/+eV59NXHQPcBk4MaM0pEk/Udn4s3wjiRep+9T4D1gFPA18ZeIC4hnG3Qmnjm4OfHMwzWKOP444LiSZ61cWADM11fUXwD8XtaJCIC3gHuAwwMc+0ygNsBx87INsE5K+/DA8TcBNk1qPPDAxNqgytSiRYs4/PDDeeGFFwp1nQPsS3xBI7UUeY8ATIxvAVBLlizh9NNPL9TtMtyJXZLyVk18n7RJiY43iXj/goklOp5y5iYg+ZqW8PNOpK8FpHB+BXxW4mP+GXiwxMfMW/+Utgi4L3D8g1IbD0ptVplZtGgRhx12GA8+WPBtUks88vOd8FlJmVo5pS0ifAFwhaQGC4D685//zPvvv5/WZSxwczbZSFLFqss43lvEU4Q/zDiuArIAmK92KW1ecedjBvBTSreD3TPASSU6VrnoBByW0v42MCZg/CridSrq1atXLzbZpFRfeim0RYsWceihh/LAAw8U6hoBx+L6I2qZeqS01QCLA8dP3JCra9eugUOrnE2bNo1zzjmnULffEW/sJkkK5xLiDTZvJXkgUSnUAL8hXpZsbMA4yoEFwHylfePvhVR+PgW2Av7RxONcQbypSEua+gvwC2D5lPbbA8ffHVgvqfGQQw4JHF6lsmDBAn76058WM/IP4P8BfwuckpSXxAIc2Uy76ZbY0C2xSRVg4MCBzJiRup/Xx8Q7R0qSwlpMPLjkOOJlxPYABgJvAIuaeOwlwMvEs7zWBq4n/JePyoFrAOanPbBRQts8XNw+bxOB3YALgF8DHRrw3C+BMwi/Dl5ejk1pm0e8jmJIxyQ1VFVVcdhhaYMTVS5qa2s57LDDePrpp4vpfhVOL1PLlncBMHEEYo8eaYMT1ZJ9+OGHXH/99YW6nUx84yhJys5i4O9LHwDLEW/q0QvYmLjOsAbxGr+dl7YvId4MZAYwhXjG1ifEs7deo2G7B6uZsgCYnx2Ji4D1+Zx4upvyNR84h3hr9ZOIC0/1bdryrdeJd/q9g5Y7grMvsHVK+32E3a1yBeCApMaddtqJDTfcMGB4lcKcOXM4+OCDiy3+3QacFTglmxPeAwAAIABJREFUKW95FgA7kLIGYPfuaX/21JL99re/ZfHi1AEgjwIFd26SJAU3Fxix9CElsgCYn9NS2l7LLAsVYxxxIfBZ0i90d6XlTfddVqFtAP8UOP7RpIzG7NevX+DwaqopU6bw4x//mHfeKWofj1uAE/ALEbV8acPsQhcAU+f4WgCsTE8++STPP/98WpeFwKkZpSNJkkrAAmA+DiFewDPJw1klogap9CLEuqSMviPeIeqNgPFbAackNXbp0sXdf8vc559/zt57783o0aOL6T6UeORtpb/vVBnSinCl2pQqSWqFzwJg5amtreX00wt938dQoKgPc0mSVB7cBCR7BxFPE00ymv/M5ZfKyRnERbgkBRcKaqIDiYuQ9TriiCPo2LFj4BTUWK+88gp9+/Yttvj3B+BELP6pMrQGVk9pDz0CMHH6cevWrVlllVUCh1e5ufLKK/nXv/6V1qWGeDdKSZLUjFgAzM4OxJtCDAfapfQ7DxdTVvlZDTgqpX0q4XdoPTmt8ZhjjgkcXo31yCOPsM8++xTaSfJb1xJvviNVip5Am5T2MYHjJ36xstpqq1Fd7aViJRk9ejSXXXZZoW4XEi8iL0mSmhGnABevC3BkkX3bEO+2syKwGfGOPGsW8bzhwLBGZSeFdR6QNrxuCPGmKaFsQ7xxTr122GEH+vTpEzC8GiOKIi655BIuvvhioqiowXyXAr8LnJZUbtYv0P55XvHXW2+9wKFVTqIool+/fsyfn/rn/F3gpoxSkiRJJWQBsHhrAH8JePzXiHeZlcrNesCAlPY5wODAOaQWhYpYq0gZmzFjBocddhjPPPNMMd0XAf2BO8NmJZWltAJgDTAzcPzEEYDrrpvYpBZo2LBhvPTSS2ld6ohH49dlk5EkSSolC4Dl4W7im995eSci1eM80qen3UXYqUC9gZ8mNfbs2ZN99903YHg11KhRo9hvv/34+OOPi+m+ADgCeDBsVlLZShtmF3r0H6QUINdfv9DgRLUUNTU1/OpXvyrU7QbCbvYlSZICcmGXfI0D9iW++bX4p3K0Celr/y0ALg+cwyVAVVLjKaecQqtWaXuTKEsPPPAAffv2Lbb4NwPYC4t/qmxpVbbQBcA2wFpJjU4Brhznnnsu06ZNS+syDjg/o3QkSVIAFgCzFwEjgF8AGwKP55qNlO560nf+vQn4OmD8vsBPkhq7devGgAFps5OVlXnz5nH88cdz0EEHMXNmUTMWvwZ2Al4Jm5lU9tKqbF8Ejr0mKbNB1llnncDhVQ5eeeUVbr311kLdTgNmZ5COJEkKxCnAYdQRXyTNAr4BxgP/JF44+U3ib1GlcncIsGdK+yzgD4FzuIyU0X9nnnkmyy23XOAUVMj777/PYYcdxr/+9a9in/IGcCAwMVxWUrPQnnxHAG6Q1ugIwJZv9uzZHHPMMdTVpS7r9yRwX0YpSZIkqZnal3jUY32PBTnm1Rg/IPl3iYC2uWVWeh2IR56k/b6hi38/TYvfvXv3aO7cuZHyU1dXF1133XVRu3bt0s6TZR+3AO0Cnzvlak3S/202yS815WQb0s+JLQPHPy0p9oorrpj3R4wy0L9//0Kf2XOBnoHPQ0mSlAFHAEqqz7lA2tyv8YRd+68tcHVah7POOouOHTsGTEFpRo0axYABAxgxYkSxT1kE/BoYGiwpqfnpndJWC3yUV/zNNtsscGjl7f777+eWW24p1O13wNjw2UiSpNBcA1DSsrYGzi7Q5wxgTsAcTiFlatpaa63F8ccfHzC8kixatIiBAwey+eabN6T4NxnYHYt/0rK2SGn7hLgIGFJilc8CYMs2bdo0TjnllELd3iXe+VfS/2fvvsOkKu/+j7+XrggIokR4EAuxazQalETsRoIaEWOPYixJjAUb6qNGxPIzqBEiGmNsaBSNgoVHY0REUWIDFAREOgJLB4FdWdoyvz/OYgCZM7O7c8609+u6zrXsnvuc+4szDjOfvYskFQBHAEra1DbAc4S/NrwFPB9hDbsDt4c1+NOf/sQ222wTYQnamtGjR3PJJZcwbty46lw2EjiXaDeLkfJVWAA4NuK+GwD7Jjt50EFhgxOV7y666CLmzw9dhrUCOA9YH09FkiQpao4AlLSpXsBeIecrgRsj7L8EeBRIurNHx44dOfvssyMsQVtaunQpV155JYcffnh1wr91wB8J1s40/JO+rwQ4MOT8+Ij73wuon+ykIwAL17PPPsuQIUNSNesFTI6hHEmSJBUINwHJH6cS7GCdzY0/fhvWf506dRKff/55ttdMLxoVFRWJXr16JRo3blydTT4SwDhgv4ifK/nITUC0qb0Ifz4cH3H/v07Wd506dRLl5eXZfglSBCZPnpxo0qRJqtfwkUDdiJ9/kiQpZk4BlgSwM/B3ghEpyUwi2gBwd+C+sAYXXnih09JiMnToUK655hq+/PLL6l76BHA10a4RKRWCI0LOJYh+CvDhyU60b9+exo2TDsRWnqqoqODMM8+krKwsrNm3wIUEI/4lSVIBcQqwpIbAS8BOIW0qCT4QRDVqsx7wLNA0WYOdd96Z++8P3RhYGfDpp59y8sknc+KJJ1Y3/JsPdAMuwfBPSkenkHNfAUsi7v+nyU4cfPDBEXetbLj66qvTWcbhRmBaDOVIkqSYOQJQ0t+An6Vo82fg0whr+CPQMaxB//79ad68eYQlFLdRo0bRu3dv3njjjepemiAY9dcTWJ7xwqTCFTYCcGTEfW9HyPqDHTuGvhwrDz3//PP8/e9/T9VsGPDXGMqRJElSAXINwNx2HanXcxtFtH+3zgS7DCatoVu3btleNqlgjR49OnHyySdXd42/jccUgv8vlB7XANRGrQl/LnSPuP8TwvofM2ZMtl+alEETJ05MZy3XucCOET/vJEmSVMAMAHNXV1IEbwQjuvaIsIYfAsvCamjVqlViwYIF2f78VHDee++9xCmnnJIoKSmpSfC3imA9yG0ifG4UIgNAbXQG4c+FH0bc/63J+m7cuHFi3bp12X6JUoaUl5cnfvSjH6V6TV8PHBvxc06SJGWZU4Cl4nQk8Dzhu/wlCHblnR5RDU2AV4Ck83pLSkp48sknadWqVUQlFJd169bx0ksv8cADDzBmzJia3uYl4AZgVsYKk4rPiSHnFgJTI+4/6fTjDh06UK+ebw8LQSKR4IILLkhn3b/ewPAYSpIkSVnkOzyp+BwMDAEapWh3D/BiRDXUAwYC+4U1uvzyy+nSpUtEJRSPZcuW8fjjj9O/f3/mzp1b09uMJdjdd0TmKlOOehjfH0Tt7JBz3wKPRth3XeC4ZCd/+tOke4Moz9x22228/PLLqZoNBe6OoRxJkiQVOKcA55ZjgTJST/F8HiiJsI6/p6rhwAMPTKxatSrbs6fyVmVlZWLYsGGJc845J9GoUaOaTPPdeCwkGAkaNlpU6cmXKcCrqfnzxSPPj3/961/ZfvlSBgwcODCdJR5c90+SJEkZYwCYOzoBK0n9AXA8wfTcqPRKVUOLFi0S06dPz/bnp7w0Z86cxJ133pnYfffdaxsELASuBxpH+FwoNgaAHjl9NGzYMFFeXp7tlzHV0qeffprYZpttUj3e6wjfiVqSJBUYp/hIxaEzwdpt26VoNxv4BcEowSj8L3B7WIO6devywgsvsPvuu0dUQuFZuHAhgwcP5sUXX2TkyJFUVlbW5nZLgPsIpoF+m5ECJeWFI444gsaNzfzzWWlpKV27dqWioiJV0+uAkTGUJEmScoQBoFT4LgH+CtRP0W4JwcL0NV4kLoU/AnekanTvvfdywgknRFRC4Vi0aBGDBw/mpZde4v33369t6AewGHgAeAgor3WBkvKOa67mt0WLFnHMMccwb968VE0fBh6MoSRJkiQVEacAZ08j4DHSm/q1AugQUR0lBMFSyjouv/zybM+cymkzZsxI9O/fP3HiiScm6tatm6lpf5MI1vjbJqLHX//lFGCPnD6++OKLbL/MqYYqKioSRx11VDqP8wfk3vsVSZIkFQADwOzYnyDYSefDwCLgoIjqqA/8I506TjvttMT69euz/Rkqp6xZsyYxYsSIxA033JDYd999M/1hfxjQhWg3e9HmDAA9cvZo06ZNYsOGDdl+2VMNrF+/PtGtW7d0HuevgZ2QJElFySnAUuHpCjwFbJ9G20XAz4FxEdTRgmDdwWNTNTzyyCN57rnnqFu3uDeaXb9+PaNGjWL48OG8++67fPjhh+ms41Qd5cA/gf5E85ir8P0HSDm/UFu1DXASyUP36cBnEfbfgOCXcnW2dvKkk06ipMTfB+SjK664gpdffjlVs2+BUwn+3ZckSZIyzhGA8dkeeATYQHojPmYBe0dUy17A5HTqOOqooxJlZWXZHkCRFcuXL0+89dZbibvvvjvRpUuXxHbbbRfV6J6PCNaCjHJ3Z6VWCCMAT8liXfnu94Q//sdH3P+FYf0PHTo02y+JqoHevXun829AJfCriJ9fkiRJKnIGgNErIVjDbVmK+jY9RgI7RFTP+QS7CKes45hjjkmUl5dn+/NTLCorKxPjx49PPPbYY4mLLroosd9++yXq1KkTVeCX4L+beuwX0eOs6jMALG4jSP7fdRHRz8p4PVn/O+ywQ2Lt2rXZfplUNf35z39O99+DqyJ+bkmSpDzgFGApv+1OsJtf52pc8xZwBkFIl0lNgX7Ab9Jp3LlzZwYPHsy2226b4TKyr6KiggkTJjB27FjGjRvHuHHj+OKLL1i5cmXUXS8HXiOYev02sDbqDiWlZS+gU8j5l4H1Efa/PSEjDE899VTq10+1UbxySZ8+fbjpppvSaXo37vgrSZIwAJTyVRvgZoJpnemOPNwA3AncUfXnTDqVIIhsk07j8847j6eeeirvP3CuXLmSKVOmMHnyZL766iumTJnC+PHjmTJlCpWVlXGVsQIYArwIDMXQT8pFlxK+4c6LEfd/DtAw2cnTTz894u6VSXfffTe33nprOk3/Dvwx4nIkSVKeMACU8ks74Brgd0Cjaly3BPg1wei/TNqZYEOJtD89Xnvttdx///15s9h8eXk506dP3+zYGPgtWLAgW2VNA96sOt4l/6bTS8VkW+DikPNTCP4/jlLS/rfffnuOPz7q5QeVKbfffju9e/dOp+nLwB8IpgBLkiQZAEp5oIRgJ90rCNbfqu5WuR8DZwJzMljTNsDlwC2kt9swDRs25K9//SsXXXRRBsuonTVr1jBv3rzvHfPnz2fGjBlMnz49myHfplYTBAQbQ79p2S1HUjV0Jfx1cgDRhjQ/Ag5JdvLMM8+kQYNs72GldNx2223ceeed6TR9FziXYPMPSZIkwABQylUlwIEEI+vOBn5Yg3usIpju25fMTQutT7DG322kOd0XoFWrVrzyyit07NgxQ2WEKy8vZ9myZcyfP58FCxYwZ84cFi5cyNy5c1mwYMF3X5csWRJLPTVQCYwh+BA3HPgP8G1WK5JUEyVA2EJta4DHIq4hbPRhTv1SRluXSCS44YYbuP/++9NpPhL4JcFzS5Ik6TsGgFJuORC4ETiR2u3SOwz4PTA9E0UBLQk+RF5GMA05bb/4xS946qmnaNWqVbU7LSsrY9myZd8dS5cu3exrsmPt2rxbBm8VQeD3KcFOoe8TrO0nKb8dCRwQcv4NgiUaotIUuCDZyf3335/DDjsswu5VW2vXruU3v/kNAwcOTKf5B0AXoDzaqiRJUj4yAJRyxzEEmzjU5v/LUoKQ7v8yUE9dgg+vFxCMQqzOmoMAnHHGGVx66aWMHDmS8vLy745vvvlms+9XrFjBypUrv/u+rKyM5cuXk0gU7NJFU4FPCKZnfwyMI9odQCVlx3Upzkc9+u8ioFmykxdfHDo4UFm2cuVKTj/9dIYNG5ZO8/eBkzD8kyRJUpacQrC20daOfNu44GiS/10SpL8bbzJfprh/2FEO3EswUq82GgJnEHwonV+LejyCowIYDTwBXAUcBTRP+9FQoWlL+PNln+yVtpnVJK/xlCzWlW/2IpjOn+y/5UTCdwaurbrAjGT9N2zYMLF48eKEctO8efMSBx10ULr/1rwHNI7wuSRJkgqAIwCl3LADsHcNrqsAHgX+BCysZQ2dgOcIQgpVTyUwi2A3z68IRvSNBibjyD6pWN0G1Ak5/2eC8CYqXYHdkp0899xzadmytr8zUhRGjRrF6aefzpw5ae3dNYJg5J/rxEqSpFAGgFJu+JZgo46GabZfRjCqrB8wLwP9twIGAztm4F6FqpJgJ+VpBGsrziCYyju56md5t/CgpMgcQLB0QjLzCX7hEqXrw05effXVEXevmnjiiSe44oorWL06rUkSrwNnEawjK0mSFMoAUMoNq4E3CUZshPkU+DswkGD0X6Z0wfBvJcEaivM3+TqHIOybTjDCz5BPUjruIXz0X1+i3aW1M3B4spPHHXccBx54YITdq7rWrl3LVVddxaOPPpruJY8TrPnrKHNJkpQWA0Apd1xCsMPuwZv8bAPBVNJXgX8SjDqLws4R3TcXrCII9BYAczf5upAg4Nv4vSMoJGVCB4JfqiSzlOAXOVG6PezkNddcE3H3qo558+bxq1/9io8++ijdS3qT4jGWJEnakgGglDuWAocAxwP7E6wl92nVz6P2cQx9ZMJqgunPG4+lKb5fRDCST5Li0ofwzT36ACsi7L8LcFiyk3vttRdduoTlk4rTiBEjOO+88ygtLU2neSXBqL+od4+WJEkFyABQyi0J4O2qI07vEowwPCui+68m2Kl4JcEH33KgrOrr8k3+vGWbcuAb/hvoOUpPUi47k2DH+GTmAw9H2H8JKUaG3XLLLZSURLn5sNKxfv16evfuzT333ENlZWU6l3wLnAP8X7SVSZKkQmUAKAmC4PFC4BPgUoLNSNbx30CuguDDx4qqP68iCO4qqo5vNvnz8qrzFVXty3CNIkmFrynwlxRtbifaX2ScDfwk2cl99tmHc889N8LulY5Zs2Zx7rnnVmfK7wzgNOCL6KqSJEmSaucUgnBpa0daW9zlkKNJ/ndJAA2yVpmkfNCW8NeQfbJX2mZWk7zGU7JYV667h/DHdybR/jvRmGBd06Q1vPDCCwll17PPPpto1qxZ2PNky+NtYIcInzeSJElSRhgASlLAALBw/Yxgfbawx/eXEddwR1j/Bx54YKKysjLb+VfR+vrrrxNdunSpTvCXAP6Ms3UkSZKUJwwAJSlgAFiYGgDjCH9sh0Vcw64EU4uT1vDaa69lOwMrSpWVlYkHH3wwsd1221Un+CsHzov4OSNJkiRllAGgJAUMAAvT7YQ/rmuB/SLsvwQYGlbDCSeckO0crChNmDAh0bFjx+qO+vsE2CPC54skSZIUCQNASQoYABaeowk2OQp7XB+IuIZLwvqvV69eYsKECdnOworKokWLEpdddlmifv361Qn+KgnWkawf8fNFkiRJioQBoCQFDAALy45AKeGP6TSCzTmi0oZg5/WkNVx55ZXZzsOKxurVqxP33XdfdTf5SFQ9j46N8HkiSZIkRc4AUJICBoCFow7wJqlHdHWKuIZhYTW0atUqsXTp0mznYkVh0KBBiT322KO6wV8CGAK0jPB5IkmSJMXCAFCSAgaAheM2Ugc7fSOu4aZUNbzwwgvZzsUK3nvvvZfo1KlTTYK/JcD5ET9HJEmSct4OwMnA3cAgYAwwH1hJsNbOGoIpLzOAD4AngauBw4C6WahXyRkASlLAALAwdAM2EP5YjgO2ibCGwwg2F0lawy9/+ctsZ2MF7f33308cc8wxNQn+EsBzBFPIJUmSilJT4A/ACIJpMzV9U7UceBboQjA9RtllAChJAQPA/PcjoIzwx7EM2DvCGloCs8JqaNasWWLu3LnZzsgK0siRIxPHHXdcTd+jfk3w/lSSJKkoNQf6ACuoeeiX7JgB9AAaxva30ZYMACUpYACY3/YBFpH6vccZEdZQDxieqgan/mZWZWVl4uWXX67pVN8EsIpgVkuTCJ8bkiRJOa076b2Zru3xNXBOTH8nbc4AUJICBoD5qzXBLxVTvd94OuI6/pKqhosuuijbeVnBKCsrS/Tv37+mm3skCKaKDwR2ifh5IUmSlLMaE7whijr42/J4PY6/nDZjAChJAQPA/NQKmEjq9xgfE+26f9ekqmHvvfdOlJeXZzs3y3uTJ09O9OzZM9G8efPavOf8kGCtRkmSpJxQLwt97ggMBQ5Ks/0c4FOC37yXAt8SbASyHdACaA/sV3W/VGv+HV+DeiVJUnHajWDK7a4p2k0DTgIqIqrj18Cfwxo0atSI5557jsaNG0dUQmFbtWoVgwYN4oknnuCDDz4gkUjU9FZzgBuBFwiCQEmSpKK0E+n9Fn0GcBOwezXu3Qz4FfAKyXfGy7cRZ4XAEYCSFHAEYH7ZFZhM6vcs35L+LzVr4mRS7PgLJP7xj39ke+Bc3tmwYUPio48+Slx22WWJZs2a1XaWyVzgclx3WpIkiYYE0yHC3jwtBi6i9iMT2wL9+P6HmHwLnAqBAaAkBQwA88cRwFJShz4VwDER1tGF8McjASRuvPHGbGdpeWPDhg2Jjz/+OHHttdcmdtlll9qGfgmC2SlXAo0ifB5IkiTllccIfwM1DGiZ4T7bA29u0ke+BU6FwABQkgIGgPnhF0AZqYOf9QQzD6LShSBgDK2jc+fOicrKymznajlv9OjRieuvvz7Rrl27TIR+CYLZKldh8CdJkrSZXxD+Juo5ol2P8EqCDzT5FjgVAgNASQoYAOa2usCdQCXphX8XRFjLb6v6CK3jiCOOSKxatSrb2VpOmjdvXuLRRx9NnHHGGYmWLVtmKvTbAPwfwZrSJRE+/pIkSXmpETCb5G+m3iB40x21w4CvY+hHmzMAlKSAAWDu2o1gw7F0QqC1wOkR1nI9QdAUWseee+6ZWLhwYbZztpyxYcOGxPjx4xN9+vRJHHXUUYn69etnKvTbGPi+CBwe4eMuSZKU964l+Ruqr4HmMdayS4x9KWAAKEkBA8DcdBywgPSCoHXA2RHV0QgYkE4d7dq1S8yaNSvbmVvWTZ48OfHII48kzjzzzMROO+2UycBv4zEHuANoF9FjLkmSFJsop91CsPHHjSHnrwC+ibiGTc2OsS9JkpS7dgD6Ar8mvemcK4BuwPAIatkZeIVgtkKoXXbZhXfffZd27YorkyovL2fUqFF89NFHfPLJJ4wZM4bS0tIouloHDAGeBN4imBIuSZKU96IOALsBOyU59x7BOiqSJElxugC4F2iVZvs5BJtyTIigluOBZ9OppW3btrz77rvstttuEZSRO9avX89XX33FmDFj+Oijj/joo4+YOHEilZWRZXEbgP8ALwMDgUVRdSRJkpQtUQeAF4ec6xNx35IkSZv6IUHw17Ua13wOnAFMz3AtzYD7gYuAOqka77nnnrz11lvsuuuuGS4ju5YvX87YsWMZN24cX3zxBWPHjmXixImsWbMmju7HAM8TrO83J44OJUmSsiXKAHB74Kgk5+YSTKvIRY+zeXD5F+DqLNUiSZJqb2+CtdxOJ42wrUqCICy8lWATiEw6BXgEaJNO40MPPZQ33niDnXZKNqkit61fv56ZM2cyefJkJk+ezJQpU5gyZQpfffUVCxYsiLOUSoLNXt4EXgCmxtm5JElSNkUZAJ4Qcv+XCN5YS5IkReXHBOsN/xqoX43ryoDfEoREmdSGIFQ8N90LzjrrLB5//HG22267DJeSWcuXL2fBggVMnz6dadOmbfZ11qxZrF27NmulEfzS+Q2C4G9JtgqRJEnKpigDwE4h54ZF2K8kSaqZ/wHqhpxvFFchtbANwRTfK4Cf1uD6ccCZwJQM1rQDcBNwOUF9KZWUlHDbbbfRq1cvSkrS2aMkGmvXrmX+/PnMnTuX0tJS5s2bx5w5c773s9WrV2etxi0kgC8JQr//A0aS+RGckiRJeSfKAPDgJD9PELwZkyRJ2VcC/Aq4HvgJ4TviPksQjt0JfBF9aWnbDTgROAb4BdCkBvdYDfw/gjWKMzVcrTlwJXAd0DTdi1q0aMGTTz7JqaeemqEy/mvt2rUsXbr0e8fixYtZuXIlK1asoLS09LtgL+YpujWxARgPjKg63sdRfpIkSd8TZQB4YJKfzwZWRtivJElKz97AAOCwNNs3IAgLuwFPEKyRuyqSytKzB/AgwQ69tTEM+AOZWxPuhwT/bboDjatz4eGHH84LL7xAu3btkrapqKigvLycsrIyli9fTnl5OeXl5axcuXKr4d7SpUtZsmQJS5YsoaysrHZ/s+xbA3wGfEywc+9w4JusViRJkpQHogoAm5P8N92TIuozU/oCgzb5flaW6pAkKUrHEfx7t30Nrq0DXEow2v+XwPwM1pWuJgRTPPepxT2WEAR1z2WgnpYEuwWfD3SsyQ122GEHDj74YHr37k15eTnffPPNd+FeeXk5K1asYOXKlVRWVmag3LxQSTAVeyzwCUHo9zmZG6EpSZKkWjqAYKrv1o4nsliX4ncKyZ8LObNgUJqOJvnfJUEwMkaSkmlL+GtIbYKs6jqW4DU4rJ50j6nAjjHWvtHZNaw3AawAelOz8HNTLaru8wVBWJWJ/57FeiwnmL7bH7gEOJQ010uUJElSalGNAAz7ILAwoj4lSVJq7YGXgIYZvN8g4HhgXYbumY59a3BNOUHAdD+wrJb97wiMBnap5X2KzQKCTTomAxOBrwhmh8zLZlGSJEmFLqoAMOw3tuUR9SlJklJ7kmDkWiYdCdwA3J3h+4YZX422M4FHCGYh1Db42+heDP+SmQdMB6ZVfZ2+yfeu1ydJkpQF2QgA10TUZ67bFvgZsBfQjGAjlEXAh8CcLNYlSSoeXYFOEd37BuBvwNKI7r+l14ExwCFJzn9LsEbgQOANgt1iM+moDN8vH6whWO+xtOrrvC2O+QRha0W2CpQkSdLWRbkLcL56HLh4k+//QrBAeJiRBOHeRtcA/ar+/D9AL+A8kgejnwN/JPiAIklfpnQ+AAAgAElEQVRSVG6M8N5Ngd8T3yjACuBU4D7gLII1DZcBQ4F/E/ybGuUOxd9GeO84rSMIbZdVfV1KEPAtJPgF5cavCwg2TZEkSVIeiioADNvcIVNrDuWD04ABJN8ReaODCUYy9Ad6ECyGXR17AQdWt7iYJBuZAcEukmfEVUgG7Jfi/OnA+jgKkZSXdkhx/kRg/wj73xE4LML7A5xJvNOAS4Fzgd8R7Awb5yyDN4j28aqJbwiWWtkY5i2pOpYmORYTzEiQJElSgYsqAAyb+tE4oj5zzdnAcwQhV7quJHgjfms1+zqFYAREvqkPvJjtIjJoYLYLkJTX+ma7gAw4kGC347iXtiiLuT8IRvf/hGBH5ZpaTvCeqYIgvKsgGFm4kmCn4vJNjo3hXlnV1621kSRJkrYqqgBwcci5H0TUZy45mGA60sbw7xOCHRdHEfwmflvgAOBCgoXTN3VjVdtxcRQqSVKG7UdxrG27BjiOYPfjI4EGBCFcBUFIV1b1541h3cZwb0XVn6OcnixJkiRtJqoAcG7IudYR9ZlLLqj6+i3BeoL/3Eqb0cBTQE+CnQQ3qgdcxebrEEqSlC/aZLuAmA2rOiRJkqScVZ3pqdWxjOTTcfaOqM9csx7ozNbDv03dBwza4mdnEUyPlSQp3zTJdgGSJEmSNhdVAAjwRZKft6M4PhzcQ7A7cDru3eL7xuTewuKSJKXDnWIlSZKkHBNlAPh5kp+XAEdE2G8uWA30q0b7UXx/3cSDMleOJEmxKYb1/yRJkqS8EmUA+EHIuRMi7DcXfEgwDbo6Jm7xfcsM1SJJUlzW4yZWkiRJUlHZHlgHJLZyzCYYCZiLHmfzWtMZyTdyi2vuq0G/L29xj7tqcI9cdApbfw4kCEZK5pOjSf53SRDsAClJybQl/DVkn4j7b0awc21YDbU93AxDkiRJykFRjgBcDoxIcq4thT0KcGkNrlm1xfeNMlGIJElVVgBDIu7jHxHfX5IkSVINRBkAAjwZcu7GiPvOpnwb2SZJKg53AJUR3XsqMDCie0uSJEmqhagDwMF8f3OLjY4FToq4f0mS9F/jCZa6iMKNBEt/SJIkScoxUQeAa4A+IecfIlgrMC67xNiXJEm56DpgbIbv2Q94JcP3lCRJkpQhUQeAAA8Dc5Kc2xV4BqgbQx0dCN+ZWJKkYvAt8EtgZobu9zrQM0P3kiRJkhSBOALA1cDvQ86fAjxBtCHgFQQbkrSKsA9JkvLFHOBQkm/Wla4+QFdgfa0rkiRJkhSZOAJAgH8RhHzJdK9q0yLD/bYH3gT64666kiRtahnQGbgHqKjmtbOBs4GbiG5TEUmSJEkZElcACHA58HHI+Z8DkwjCwNqOBvwfoC8wgeDDjSRJ+r7VwM3AD4H/B3yVov144DJgL+Cf0ZYmSZIkKVPiDADXAKcShHzJ7AQMAKYQ7Ca4WzXu3xQ4nWDn4RnA1UDDmhQqSVKRKQVuAfYB1oa0uwX4G0FwKEmSJClP1Iu5v0XAUcDbwI9C2u0O/Knq+Br4lCDUm0ewePl6oDHBlOH2wP7AQcSzmYgkSYUske0CJEmSJGVW3AEgwGLgCOBx4Kw02rerOjLB6UqSJEmSJEkqKnFOAd5UOcHi4RcBS2LobzzBGoPdY+hLkiRJkiRJyhnZCgA3eopgIfH7gJUR3P9z4NcE04PfjuD+kiRJkiRJUk7LdgAIsAy4AWgLXAGMpHbrDy0EHgF+BvwYeA7YUMsaJUmSJEmSpLyUjTUAk1kJPFx17Aj8FDicYITgbsDOBBt/bEMQ6FUAS4E5BLsGjyUID7/ABcwlSZIkSZIkKRanEASyWztWZ7Gumjia5H+XBNAga5VJygdtCX8N2Sd7pW1mNclrPCWLdUmSJEmqoVyYAixJkiRJkiQpIgaAkiRJkiRJUgEzAJQkSZIkSZIKmAGgJEmSJEmSVMAMACVJkiRJkqQCZgAoSZIkSZIkFTADQEmSJEmSJKmAGQBKkiRJkiRJBcwAUJIkSZIkSSpgBoCSJEmSJElSATMAlCRJkiRJkgqYAaAkSZIkSZJUwAwAJUmSJEmSpAJmAChJkiRJkiQVMANASZIkSZIkqYAZAEqSJEmSJEkFzABQkiRJkiRJKmAGgJIkSZIkSVIBMwCUJEmSJEmSCpgBoCRJkiRJklTADAAlSZIkSZKkAmYAKEmSJEmSJBUwA0BJkiRJkiSpgBkASpIkSZIkSQXMAFCSJEmSJEkqYAaAkiRJkiRJUgEzAJQkSZIkSZIKmAGgJEmSJEmSVMAMACVJkiRJkqQCZgAoSZIkSZIkFTADQEmSJEmSJKmAGQBKkiRJkiRJBcwAUJIkSZIkSSpgBoCSJEmSJElSATMAlCRJkiRJkgqYAaAkSZIkSZJUwAwAJUmSJEmSpAJmAChJkiRJkiQVMANASZIkSZIkqYAZAEqSJEmSJEkFzABQkiRJkiRJKmAGgJIkSZIkSVIBMwCUJEmSJEmSCpgBoCRJkiRJklTADAAlSZIkSZKkAmYAKEmSJEmSJBUwA0BJkiRJkiSpgBkASpIkSZIkSQXMAFCSJEmSJEkqYAaAkiRJkiRJUgEzAJQkSZIkSZIKmAGgJEmSJEmSVMAMACVJkiRJkqQCZgAoSZIkSZIkFTADQEmSJEmSJKmAGQBKkiRJkiRJBcwAUJIkSZIkSSpgBoCSJEmSJElSATMAlCRJkiRJkgqYAaAkSZIkSZJUwAwAJUmSJEmSpAJmAChJkiRJkiQVsHrZLkCSJCkDtgdKsl1EgUoAy7NdhCRJkmrOAFCSJOWrlkBv4GKgYZZrKTZrgEXA/Kqvi4AFwNfArKqvXwOrs1SfJEmSNmEAKEmS8lF94GWgU7YLKVINgbZVRzJrgQnAWGAc8EXVsSzy6iRJkrQZA0BJkpSPTsbwL9c1AH5cdWyUACYC7wMjgeHAwvhLkyRJKi4GgJIkKR91yHYBqpESYP+q4w/ABmAM8EbV8VnVzyRJkpRB7gIsSZLy0TbZLkAZUQf4CXA7MAqYA/QFDstiTZIkSQXHAFCSJEm5ojVwNfAxMA24E9g9qxVJkiQVAANASZIk5aI9gFuBqcC/ga64fI0kSVKN+CZKkiQVlCOOOIJ+/fplu4yCsX79esrKyjb72aJFi1i8eDELFy5k/vz5fPPNN8yaNYvp06dTXl6e6RLqACdWHaVAf+ARYGWmO5IkSSpUBoCSJKmgNGvWjEMOOSTbZRSthQsXMnPmTCZOnMjYsWMZO3Ys48ePZ8WKFZm4fRvgT8D/EoSA/XAXYUmSpJQMACVJkpQxrVq1olWrVhx++OHf/SyRSDBp0iQ++OADRo4cydtvv83ChbXK7ZoBNxGsF/h34C5gcW1uKEmSVMhcA1CSJEmRKikpYd999+V3v/sd//jHPygtLeXDDz/klltu4eCDD6akpKSmt24EXAVMB3oB22WqZkmSpEJiAChJkqRY1a1bl44dO3LXXXfx2WefMWfOHPr27UuHDh1qessmwO3ADOAyoG6GSpUkSSoIBoCSJEnKqjZt2nD11VfzySefMHXqVHr16kWbNm1qcqsdgb8Co4EjMlqkJElSHjMAlCRJUs5o3749t99+O7NmzeKVV17hxBNPrMkU4YOA94GBQKuMFylJkpRnDAAlSZKUc+rVq0fXrl3597//zfjx47nggguoX79+dW5RApwDTATOjaRISZKkPGEAKEmSpJy233778fTTTzN16lSuvvpqttuuWnt97AA8B7yGowElSVKRMgCUJElSXmjXrh19+/Zl2rRpXH755dUdEfhL4HPguGiqkyRJyl0GgJIkScorrVq14qGHHmLSpEl069atOpfuDAwF7gGqlR5KkiTlMwNASZIk5aU99tiDwYMHM3ToUPbZZ590L6sD3ESwSUjryIqTJEnKIQaAkiRJymsnnHAC48aN495772XbbbdN97LDgVHAYdFVJkmSlBsMACVJkpT36tevT8+ePZk6dSqnnXZaupe1BkYCPaKrTJIkKfsMACVJklQwWrduzeDBg3n88cdp0qRJOpfUA/oBfwHqRlqcJElSlhgASpIkqaCUlJRw8cUXM2HCBDp16pTuZVcBbwJppYaSJEn5xABQkiRJBWmXXXZh2LBhXH/99ZSUlKRzyQkEIWCLaCuTJEmKlwGgJEmSClaDBg247777GDRoULpTgn8GvAfsFGlhkiRJMTIAlCRJUsHr1q0bn332GQcccEA6zQ8APgF2i7YqSZKkeBgASpIkqSi0b9+eDz74gM6dO6fTfFfgLaBtpEVJkiTFwABQkiRJRaNZs2YMGTKE7t27p9P8h8BwoFW0VUmSJEXLAFCSJElFpX79+gwYMIB+/fqlszlIe+Ad3BhEkiTlMQNASZIkFaUePXrw8MMPU6dOyrfE+wGDgUbRVyVJkpR5BoCSJEkqWpdddhlPPfUUdevWTdX0aOA5fP8sSZLykG9gJEmSVNQuuOACXn31VRo2bJiqaTegXwwlSZIkZZQBoCRJkoreySefzKOPPprOmoBXAr+NoSRJkqSMMQCUJEmSgO7du/PAAw+k0/Qh4PiIy5EkScoYA0BJkiSpytVXX80999yTqll94CVg9+grkiRJqj0DQEmSJGkTN910E5dddlmqZtsDzxKEgZIkSTnNAFCSJEnawoMPPsjxx6ec5dsR6BNDOZIkSbViAChJkiRtoV69erz44ovstddeqZpeDZwSQ0mSJEk1ZgAoSZIkbUXz5s0ZMmQIzZo1C2tWAjwG7BhPVZIkSdVnAChJkiQlseeeezJgwABKSkrCmrUC/hZTSZIkSdVmAChJkiSF6Nq1Kz179kzVrBtwfgzlSJIkVZsBoCRJkpTC3XffTadOnVI1+wvBaEBJkqScYgAoSZIkpVCvXj2efvppmjRpEtasOdAvppIkSZLSZgAoSZIkpWG33XbjoYceStXsbODUGMqRJElKmwGgJEmSlKYLLriAk08+OVWzvsC2MZQjSZKUFgNASZIkqRoee+wxmjdvHtZkN+B/YypHkiQpJQNASZIkqRp+8IMf0Lt371TNrgFax1COJElSSgaAkiRJUjX94Q9/oEOHDmFNGgN3xVSOJElSKANASZIkqZrq1q3LI488Qp06oW+nuwMHxFSSJElSUgaAkiRJUg38+Mc/5uKLLw5rUge4I6ZyJEmSkjIAlCRJkmqoV69eNG7cOKzJL4EDYypHkiRpqwwAJUmSpBpq06YNPXv2DGtSB+gVUzmSJElbVS/bBUiSpLxxOrBvtouocmi2C5A26tmzJ4888ggLFy5M1uQ0grUAx8dXlSRJ0n8ZAEqSpHR1z3YBUi7adtttufnmm+nRo0eyJiXAdcCFsRUlSZK0CacAS5IkSbV0ySWX0KpVq7AmZwGhDSRJkqJiAChJkiTV0rbbbsu1114b1qQRcFlM5UiSJG3GAFCSJEnKgN/+9rc0adIkrMllBEGgJElSrAwAJUmSpAzYfvvtufTSS8Oa7AScEVM5kiRJ3zEAlCRJkjLk8ssvp27dumFNLoirFkmSpI3cBViSJG3qM6BBtotIQ1uC0VRSTtl999056aSTGDJkSLImxwK7ArPiqkmSJMkAUJIkbeqn2S4gTf2AHtkuQtqaSy65JCwArAN0B3rHV5EkSSp2TgGWJEmSMugXv/gFrVu3DmtyVly1SJIkgQGgJEmSlFH16tWje/fuYU32AfaPqRxJkiQDQEmSJCnTLrgg5V4fv4qjDkmSJDAAlCRJkjJu77335qCDDgprck5ctUiSJBkASpIkSRHo1q1b2Ok9CaYCS5IkRc4AUJIkSYrAr36VcpbviXHUIUmSZAAoSZIkRWCfffZh7733Dmvy87hqkSRJxc0AUJIkSYpIly5dwk4fA2wTUymSJKmIGQBKkiRJETnhhBPCTjcCfhZTKZIkqYgZAEqSJEkROeqoo2jUqFFYk05x1SJJkoqXAaAkSZIUkW222YZOnUIzvp/GVYskSSpeBoCSJElShFIEgB2BejGVIkmSipQBoCRJkhShn/40dJBfY+CAmEqRJElFygBQkiRJitBPfvIT6tQJfdt9cFy1SJKk4mQAKEmSJEWoadOm7LvvvmFN9o+rFkmSVJwMACVJkqSI/ehHPwo7fWBcdUiSpOJkAChJkiRF7IADQpf5cwSgJEmKlAGgJEmSFLH99tsv7HQroGVMpUiSpCJkAChJkiRFbP/9Uw7yax9HHZIkqTgZAEqSJEkRa9u2LQ0aNAhrsltctUiSpOJjAChJkiRFrG7durRt2zasya4xlSJJkoqQAaAkSZIUg1133TXsdLuYypAkSUXIAFCSJEmKQbt2oRnf/8RVhyRJKj4GgJIkSVIM2rRpE3Z6h7jqkCRJxccAUJIkSYpBy5YtQ0/HVYckSSo+BoCSJElSDHbYIXSQnyMAJUlSZAwAJUmSpBikCACbAXVjKkWSJBWZetkuQJIkSSoG22+/fdjpOsASIBFPNdVyOfB8touQJEk1ZwAoSZIkxaBRo0apmoQmhFnUMNsFSJKk2nEKsCRJkhSDBg0aZLsESZJUpAwAJUmSpBg0bOhAOkmSlB0GgJIkSVIMHAEoSZKyxTUAJUmSpBhs2LAh2yUoPj8ArgKOAVYAC4H5VcdCYB6wCCgFyrJUoySpiBgASpIkSTFYs2ZNtktQPHYGRgOt02y/CljA1sPBhcDiqq9LgG8zXawkqTgYAEqSJEkxWLt2baomvwO+iaGUrXkUaJ6lvgvNPaQf/gFsC+xedaRSQRAELiIIBpdUHYu38rMlwNJq1CFJKmAGgJIkSVIM0hgB+DJBaJMN/TAAzJQjIrz3NkDbqiMdGwhCwK0dm4aEmx7LgHUZrVqSlHUGgJIkSVIMKioqUjVZHUcditwyYI9sF1GlDrBj1VEd3xCMKNx0dGHY9waGkpTjDAAlSZKkGCxdGjobcy1QHlMpitarwE+yXUQtNa869kqz/QqCtQtLgbnA7KqvpZv8eXnmy5QkpcsAUJIkSYrBkiWhs3uXxVWHItcH+BFwZrYLiVGzqmOfkDblfD8YLAWmAlMIAkRJUkQMACVJkqQYpBgB6GYNhaMSOAu4HzgNOBI4HKibzaJywHbAvlXH1pQThIFTgenAJGBi1deU8+clSeEMACVJkqQYpBgBaABYeEZVHQCtgNMJRgUeCZRkq6gcth1wcNWxqQ3ADGAC8CVBKDiaIChMxFmgJOUzA0BJkiQpBrNnzw47vTCuOpQVC4G/Vh37AlcAvwaaVOcmrVq1okePHlRWVrJ06dLvjiVLlnx3rFy5MvPVZ1cdoH3V0XWTn68gCAJHEwSt44BpsVcnSXnCAFCSJEmKwcyZM0NPx1WHsu5L4A/ArcD1wJUEo99SWrhwIY8//jhDhgxhv/3222qbtWvXsnTpUpYtW/a9gHDT0HDLI5HIu8F0zYDjqo6NFgEfAv+p+joGWBN/aZKUewwAJUmSpBjMmjUr7PTXMZWh3LEMuBnoC9xIEAQ2SHXRjBkz6NixI8888wxdu3b93vkGDRqw8847s/POO6ddSCKR+C4IXLRoEYsWLWLBggUsXryYRYsWMX/+fBYvXszixYuZP38+ZWVlad87ZjsRjBLc+B9mNfAx8C9gKPAFThuWVKQMACVJkqSIVVRUsHjx4rAmBoDFazHBSMCngL8BR6S6oKysjG7dunHvvfdy/fXX17qAkpISWrZsScuWLdlrr71Stl+9evV3YeCiRYuYN28epaWlfP3115SWljJ37lxmz57NqlWral1bLTUCjq467gXmA28RhIFvA6ELc0pSITEAlCRJkiL21VdfpZpiOSumUpS7JhJsEHIx0AdoEdY4kUjQs2dPZs+eTb9+/ahTp04cNQLQqFEj2rZtS9u2bUPbLVu27LtgcO7cuZSWljJ79mzmzp3L4sWLmTlzJuXl5TFVDcDOwIVVx3rgfeDVqmNOnIVIUtwMACVJkqSITZgwIex0JTA9plKU2xLA48AQ4FE23/Riq/r378/8+fMZOHAg9evXj7q+amnRogUtWrTggAMOSNpm3rx5TJ069bvjq6++YsKECcycOTPqdQnrAcdWHX8hWC/wVeAVgnUaJamgGABKkiRJERs/fnzY6SkEa5VJGy0CTgN+T7BGYKOwxoMGDWLdunW8+OKLNGiQchnBnNK6dWtat27NUUcdtdnPv/32WyZNmsT48eP58ssvmTRpEpMmTWLGjBlRlFECHFp13EWwq/DTwEDgmyg6lKS4GQBKkiRJEUsRAIYOD1RR+xswDhhMMH01qddee43TTz+dQYMG0bBhw1iKi1Ljxo059NBDOfTQQzf7+bJlyxg9ejSjRo1i9OjRfPbZZ8yePTvT3f+k6vgz8BowgGDdwMpMdyRJcTEAlCRJkiL2xRdfhJ12uqHCfEQQRr1S9TWp119/nXPOOYeXXnqJunXrxlJc3Fq0aMHPf/5zfv7zn3/3s0WLFjFy5Ejef/99PvjgA8aNG0dlZUayuobAmVXHPODvBFOzF2Ti5pIUp/hWipUkSZKK0MyZM5k3b15Yk9B0UAJKCXayHZKq4SuvvEKPHj0iLyiX7LTTTnTr1o1+/foxZswYli1bxptvvsnNN9/MIYcckqkNUloDtxPs2P0scFgmbipJcTEAlCRJkiI0cuTIVE3+E0cdynurgG4E04JDPfzww/zpT3+KvqIc1bRpUzp37szdd9/N6NGjmT9/Ps8++yznn38+P/jBD2p7+wbAecDHwCfAWQRrCEpSTjMAlCRJkiL0n/+E5nszgIUxlaL8VwlcRrBrbaibb76ZF198MfqK8sBOO+3EeeedxzPPPMO8efP45JNPuOGGG9hjjz1qe+sOwAsE6zSeiZ+vJeUwX6AkSZKkCKUIAD+Kqw4VlGuAh8IaJBIJfvOb3/D555/HVFJ+KCkpoUOHDvTp04dp06bx2Wefccstt7D33nvX5rYHAP8k2NDnPKAwF2CUlNcMACVJkqSIlJaWMnHixLAmH8ZViwpKAriKYHfapFatWkXXrl1ZuNBBpskcfPDB3HXXXUyaNIlPPvmEyy67jObNm9f0dvsQrA/4JXAhBoGScogBoCRJkhSRoUOHkkgkwpqMiKsWFZwEcCnwelij2bNnc/HFF6d6Hgro0KEDf/3rX5k3bx7PP/88nTt3rukGInsCTwFjgRMyWqQk1ZABoCRJkhSRf/3rX2GnvwZChwdKKawn2ITi47BGb7zxBg8++GA8FRWARo0acfbZZ/Pmm28yZcoUevToQdOmTWtyq/2BoQQhba3mGEtSbRkASpIkSRFYv349w4cPD2vydly1qKBt3B14blijG2+8kbFjx8ZTUQHZY4896NevH3PmzOGBBx5gt912q8ltTgK+AB4EWma0QElKkwGgJEmSFIHhw4ezbNmysCZvxVWLCt584DSgIlmDNWvWcPbZZ7Nq1ar4qiogTZs25ZprrmHq1Km8+uqrHHnkkdW9RX3gSmAqcAlQkukaJSmMAaAkSZIUgUGDBoWdXgcMi6kUFYfRwO/DGkyePJlevXrFVE5hqlu3LqeeeiojRozgnXfeoVOnTtW9xfbAY8A7QPuMFyhJSRgASpIkSRm2du3aVAHg28DymMpR8XiGYBfapPr27cvo0aNjKqewHXvssbz//vsMGzaMn/3sZ9W9/BiCacE9gXoZL06StmAAKEmSJGXY22+/zTfffBPW5OW4alHR+QMwPdnJyspKLrnkEtatWxdjSYXtuOOOY+TIkbzzzjv8+Mc/rs6l2wD3EmzickgkxUlSFQNASZIkKcOefPLJsNPrgFdjKkXFpww4D6hM1mDcuHHcf//98VVUJI499lhGjRrFk08+SevWratz6SHAR8BN+BldUkR8cZEkSZIyaPHixbz++uthTd4FlsZUjorTJ0CfsAZ33nkns2fPjqmc4lGnTh1+85vfMHPmTPr160fTpk3TvbQ+cA9BELhHZAVKKloGgJIkSVIGDRgwgLVr14Y1eTquWlTU7gKmJDtZUVFB7969YyynuDRo0IAePXrw+eefc8IJJ1Tn0g4EAe6p0VQmqVgZAEqSJEkZkkgkePrp0HxvOfBKTOWouFUAlwCJZA0GDBjA559/Hl9FRWj33Xdn6NChPPPMM+y4447pXrYDwTIBDwMNIitOUlExAJQkSZIyZOjQoUycODGsyUCCYEaKwwfAc8lObtiwgeuvvz7GcorX+eefz5dffkn37t0pKSlJ97I/AO8B1VpQUJK2xgBQkiRJypC+ffumavJEHHVIm7gJ+DbZyeHDh/Pee+/FV00Ra9myJQMGDODtt9+mffv26V7WERgN/DS6yiQVAwNASZIkKQMmTpzI0KFDw5p8CnwWUznSRqUEm0skdfvtt8dTiQA47rjj+Oyzz+jevXu6l+xMsHnQ76KrSlKhq5ftAiRJEgAfA5XZLiKPbJvtAqQt9enTh0Qi6XJrAA/EVYu0hT8DvwV22drJESNGMHz4cI499th4qypiTZo0YcCAAXTu3Jnf//73rFixItUlDYC/AYcAVwJroq5RUmExAJQkKTc0zXYBkmpu8uTJDBw4MKzJbGBwTOVIW1pNsCvw35M1uOOOOwwAs+Dss8/m8MMP57zzzuPDDz9M55JLgYMJdgmeF2lxkgqKU4AlSZKkWrrjjjuorAwdxPsgsD6mcqStGQBMT3ZyxIgRjBo1Kr5q9J1dd92VESNG8Mc//pE6ddL6iH4o8CGwT7SVSSokBoCSJElSLXz55Ze88MILYU2W4+Yfyr51wJ1hDR54wFnq2VKvXj3uuOMOXnvtNZo1a5bOJe2AkcAR0VYmqVAYAEqSJEm1cN1117Fhw4awJvcRhIBStj0LTE12ctCgQcyePTvGcrSlk08+mU8//ZR99903neYtgLeBbtFWJakQGABKkiRJNfTOO+/w73//O6zJMuDhmMqRUqkk2BBkq9avX+8owByw5557MmbMmHR3CW4EDAJuj7QoSXnPAKupOSkAACAASURBVFCSJEmqgcrKSq677rpUzR4AUm7vKcXoWeCbZCcHDBjAqlWrYixHW9OoUSOeeuop7rzzznTWBSwBegG3RV+ZpHzlLsCSJMVjKXBmtosoIBcCXbJdhIrbY489xrhx48KaLAb6x1SOlK5vCXYDvnFrJ1esWMHgwYM5//zz461K31NSUsKtt97KD3/4Q7p3786aNWtSXdIbqA/8MfrqJOUbA0BJkuKxCngp20UUkJ9luwAVt7lz53LDDTekanYzsDKGcqTqegi4liAs+p4nn3zSADCHnHXWWbRq1YrTTjuN5ctTLid6K8HjelP0lUnKJ04BliRJkqrpuuuuo6ysLKzJRGBAPNVI1TYXeCXZyREjRjBt2rQYy1EqRx99NB988MH/Z+++w6Qq7zaOf5eOKKJo7IldsaCJURGjiRFRARVea0xMolgSg4oalZBEsUVNVIoaFQkaC9hFVFA0gggilgiINJEFkd7r7sKy8/5xICHrzpmZ3Zkz7fu5rrmAfX4zc6O0vfc552HPPfdMZvwm4N4MR5KUZywAJUmSpBQMGzaM559/PtHY74HKCOJItfVovIVYLMaAAQOizKIkHHbYYXz88cccddRRyYxfDzyGn/NL2sw/DCRJkqQkLV++nMsvvzzR2MtA6NHAUg4YBcyJt/jMM89QVVUVXRolZdddd+Wdd97hhBNOSGb8UqBvhiNJyhMWgJIkSVKSfvOb3zBv3rywkdXAVRHFkeqiCng83uI333zDhx9+GGEcJatFixYMHz6cn/70p8mMdwNuz3AkSXnAAlCSJElKwmOPPcYLLyQ8y+f3wPwI4kjp8ARBEVijl156KbokSkmzZs14/fXXOeWUU5IZ/xPQPcORJOU4C0BJkiQpgdLS0mRO/f0I+EcEcaR0mQOMj7f48ssvE4vFIoyjVDRt2pShQ4dy+umnJzN+P/DLDEeSlMMsACVJkqQQ69at48wzz2TlypVhY2uBnxOym0rKUXFPtJk9ezYfffRRlFmUoiZNmvDaa69x4YUXJhotIbjk+7zMp5KUixpkO4AkSZKUy66++momT56caOxPwMwI4mRDB2CXbIdQxuwAxAgKom8ZMmQIxx57bLSJlJL69evz+OOPs379eoYMGRI2Wo/gsu9FwHtRZJOUOywAJUmSpDgeffRRBg4cmGhsBNAvgjjZcu7mh4rQq6++yl133ZXtGEqgUaNGPPfcc3Tq1Im33347bLQp8CrwY2BiJOEk5QQvAZYkSZJq8O6773LVVQkP9F0CXEywg0oqOFOnTmXu3LnZjqEkNGrUiFdeeYU2bdokGt0eeA3YPfOpJOUKC0BJkiSpmhkzZnDuueeycePGsLEqgvv+eeqvCtqIESOyHUFJatasGW+88QaHHnpootG9gKFAs8ynkpQLLAAlSZKkrSxevJhOnTqxfPnyRKO3A6HX2kmFwAIwv+y444689dZb7L333olGjwKexl5AKgr+RpckSZI2W7lyJaeeeipffvllotG3gdsiiCRl3YgRI6isrMx2DKVgjz32YPTo0Xz3u99NNNoZ6BNBJElZZgEoSZIkAevWraNjx45MmDAh0eh04AKCS4Clgrdy5Uo+/fTTbMdQivbaay+GDBnCdtttl2j0KuDyCCJJyiJPAZYkSVLRKysro3PnznzwwQeJRpcCHYGE1wfnmUnAgmyHUFbVB44ASmpafP/99zn22GOjTaQ6+/73v8/gwYM566yz2LRpU9jog8As4J1okkmKmgWgJEmSitqaNWs4/fTTGTt2bKLRdcBpwFeZTxW507MdQDlhHFDjEbJJlOPKUR07duTee+/l2muvDRtrCDxPcF/A0kiCSYqUlwBLkiSpaK1bt44zzzwzmfKvCrgE8DpIFbLR8RaS+D2iHNa9e3euvvrqRGM74MnAUsGyAJQkSVJRWrp0KaeccgqjRo1KZvwqgt0xUiEbH29h8eLFzJo1K8osSrN7772Xk08+OdHYYUC/COJIipgFoCRJkorOtGnTOProoxk3blwy4zcBf89wJCkXjAldHBO6rBzXsGFDXnnlFVq3bp1o9BLgdxFEkhQhC0BJkiQVlY8//pif/OQnzJ49O5nxPsBfM5tIyhmLCbn/2/jxcTcIKk9st912vPTSS7Rs2TLR6L3ADyOIJCkiFoCSJEkqGv369aNt27YsWrQomfEeQOhd86UCFPe0jw8//DDKHMqQ/fffn0GDBlGvXmgd0AR4AUjYFErKDxaAkiRJKngbNmzgiiuu4JprrqGysjKZp9wE3JPhWFIuintd/JQpU5L9/aMc1759e2699dZEY3sDT2NvIBUEfyNLkiSpoM2fP5/TTjuN/v37JzMeA/6Al/2qeE2It1BeXs6XX34ZZRZlUM+ePenYsWOisdOAGyOIIynDLAAlSZJUsJ5//nkOOeQQRo4cmcx4OXAecHdmU0k5bRJBEV6jiRMnRhhFmVSvXj0GDx5Mq1atEo3eDrSNIJKkDLIAlCRJUsGpqKigR48eXHDBBaxatSqZp6wFugAvZjaZlPPWALPjLU6ePDm6JMq47bbbjkGDBtG0adOwsQbA48C20aSSlAkWgJIkSSoo48eP5wc/+AH33HMPsVjcjUxbmwWcCLyZ2WRS3oh7GbA7AAvPkUceycCBAxONHQj8PYI4kjLEAlCSJEkFYc2aNVxxxRUcd9xxTJkyJdmnDQGOBD7LXDIp78Td5ucOwMJ0wQUXcNlllyUauwg4O4I4kjLAAlCSJEl5b/jw4fzwhz+kf//+ye76A+gNnEtwyaOk/5oUb2HOnDmsX78+yiyKSN++fTnkkEMSjfUH9owgjqQ0swCUJElS3vryyy8544wz6NChAzNmzEj2aWuBXwHXAZUZCyflr6nxFmKxGKWlpVFmUUSaNm3KM888Q+PGjcPGdgSexC5Byjv+ppUkSVLeWbx4Mddddx2HH344r7/+eipP/RQ4iuATWEk1m0XIScCzZs2KMIqidOSRR/KXv/wl0dhJwE0RxJGURhaAkiRJyhvLly+nZ8+e7LvvvvTu3ZuKiopknxoD7gPaAklvFZSKVBkwP97izJkzI4yiqF177bWcccYZicZuB46JII6kNLEAlCRJUs5bsGABN910E/vssw933XUX69atS+XpXwI/BX4PbMhIQKnwxN3m5yXAha2kpIRHH32UnXfeOWysPsH9ABtGk0pSXVkASpIkKWdNnz6dyy+/nH322Ye//vWvrF69OpWnbwTuAloDozKRTypgcbf5uQOw8O222248/fTTlJSUhI0dAfSKJpGkurIAlCRJUk7ZsGEDzz//PCeffDKtWrXiscceS+VS3y0+BtoAPYHytIeUCp87AItc+/bt+c1vfpNo7PcERaCkHNcg2wEkSZKkWCzG+PHjefbZZxk8eDCLFy+u7UstIij9ngCq0pVPKkJxC8A5c+ZEmUNZdN999/HOO+/w5ZdfxhtpBAwk+ILLxsiCSUqZBaAkSZKyYtOmTYwfP57XXnuN5557rq67itYBDwB3A6vSElAqbt/EWygrK2PFihXssMMOUeZRFjRt2pSnnnqK448/nk2bNsUb+wHwJ+CW6JIpRS2B4zY/DgL2AXYHmgHbAJsIDv9ZDswjuHfuJGAc8MnmdeU5C0BJkiRFZvbs2bz//vsMHz6cESNGsGzZsrq+5EZgAMGJlAvqHFDSFqG/nxYuXGgBWCSOPfZYrr76anr37h021hMYCnwaTSoloTnwC+B84EeE3wKuPsFuzu0JysEfbbW2CngdGAS8ibvr85YFoCRJkjKisrKSGTNmMGrUKMaOHcvo0aP55pu4m4pStZHgk5Hbga/S9aKS/mNR6OKiRbRq1SqqLMqy2267jVdeeYXZs2fHG2kAPEKww6wyqlyq0Q5AD+A3BCVgXW0P/HzzoxToS/D/OuWb8yq7LAAlSZJUJ8uXL+err776z2P27NlMmDCByZMnU16e9vM31gKPAb2Buel+cUn/sRpYT3B54LcsWOCG22Ky7bbb8thjj9G+fXtisVi8sR8CVwL9okuman4F/A3YOUOvvw/QB7iOoGQcnKH3UQZYAEqSpILy+eefc8UVV2Q7RsEpKyv7T5m3Zs0a5s+fz5IlS1i8eHHYfaHSaRZB8def4B5FkjJvIbBvjQsLF0YcRdnWrl07unbtyoABA8LGbgdeBOZHk0qbNSP4O/JnEb3fdwl24f8c6BTRe6qOLAAlSVJB+frrr+nfv3+2Yyg9KoHXgEeBt/G+Q1LUFhCnAHQHYHHq06cP7777LrNmxT0kujnwENAlulRFb2dgBHBkkvNzgY8IvrA2j+AQrUpgW2BHYH/g0M2vF3bfQIB2tcirLLEAlCRJUi6JAR8CzwLPE+xAkpQdce8DuGhR6C0CVaCaNWtGv3796NQpdNNXZ+B0YHg0qYrad4CRwCEJ5koJdtA/T1D8JWN74BSCXX4dgYa1zKgckajNlSRJkjKtiqD0+wPBbqO2BPeQsvyTsmtJvIWVK1dGmUM5pGPHjvz85z9PNPYg0DSCOMWsMTCE8PJvKdAVOBC4m+TLPwhO/32RYDfnfgSHf3jwRx6zAJQkSfnIYij/LSe4efhFwC4EJ0feDczOYiZJ/ytuy7d69eoocyjH9O3bl5122ilsZF+gVzRpitaDBH93xvMvoBUwkLqfzDwX6A4cBrxZx9dSllgASpKkfPQOwaWiyg+bgGnAM8BvCT6B2Am4EHiaYIeCpNyzJt6CBWBxa9myJX/5y18SjV0HHBFBnGJ0OnBpyPog4DTS//frzM3vfTXuBsw7FoCSJCkffQLcke0Q+pYNwHRgGMElvJcDxwDbEexC+AXwCPAFFrhSPojb8lkAqmvXrrRt2zZspAHBgSAl0SQqGk0IDseKZxjwS+q+6y/MA8CPCblPqHKPh4BIkqR8dTPwLsG9bRpnOUsxqSK4THcpsGyrxzcElwh5Uq9UONwBqLjq1atH3759adOmDZs2bYo3djzBrR6ejC5ZwbsS2CvO2tcEX2yL+z8kjcYDJ0TwPpLyxBkEX+Gv6VGexVy18RPi/1xiQKOsJZMkSZLSrwtx/u3bpEmTmBSLxWLXXntt2OdIMYL79m6fhV+/hagxwa67eP+tz8heNOU6LwGWJEmSJNUk7g7A8vJyNmzYEGUW5ahbbrmFXXfdNWxkF+D3EcUpdP8HfCfO2ijgteiiKN9YAEqSJEmSahJ6ne+aNXH7QRWR7bffnvvuuy/R2PXA9yKIU+i6hqzdE1kK5SULQEmSJElSTcrCFisqPARUgQsvvJB27dqFjTQF/hpRnELVguDgjZp8A7wVYRblIQtASZIkSVJNNoYtVlZm8pBR5ZtHHnmExo1Dz+Q6D2gfUZxCdArxD3J9geAegFJcFoCSJEmSpJqEFoAbN4Yuq8jst99+dOvWLdFYb+KXWAoXduLuO5GlUN6yAJQkSZIk1cQCUCm5+eabEx0IcghwWURxCs3343w8BoyJMohqdAHQa6vHT7OYpUYWgJIkSZKkmngJsFLSvHlzbrnllkRjdwAtI4hTaFrH+fjXJDiwR5G4ALhlq0fOFYBuvZUkSZIk1SS04XMHoGpy2WWX8fDDDzNp0qR4IzsC44AJ0aXKKV8At6b4nB2A5nHWptYtjoqFBaAkSZIkqSYWgEpZ/fr1ueeeezj99NPDxg7Y/ChGO9XiOXuGrM2vbRAVFy8BliRJkiTVxHsAqlZOO+00OnTokO0YhWTnkLVFkaVQXrMAlCRJkiTVpCpsMRaLRZVDeehnP/tZtiMUkqYha2sjS6G8ZgEoSZIkSapJw9DFhqHLKnIPPvhgtiMUkrACsCKyFMpr3gNQkiRJklQTC0DVyrBhwxg/fny2Yyi3NQCOBvYhuMS5KbCU4JLmj4GF2YtWmCwAJUmSJEk1sQBUrdx2223ZjlBoykPWGkeWIj1aAz2B04Dt48zEgInAQOAREtyPdCvbAmuqfewAYGaKGRcCu2z149OBN2uYGwX8OM5r/HHzI0xtstWaBaAkSZIkqSahny9aAKomb7/9dqLdf0uBlyOKk4um1+I5ZSFrzWobJGJNgAeAS0h8O7oS4EigH3AN8GtgTCbDFQMLQEmSJElSTUIbvgYN/HRS39arV69EI78FXsx8koKyJGRt18hS1N4OwFDgR7V47n7A28BF+OumTvwTW5IkSZJUEy8BVkrGjBnDBx98EDYyHXglojiF5JuQtd0jS1E7JcBzfLv82wg8QVDqzSA4zXg34KfAFUCrrWabAIMJ/jt8mNm4KbmK/17G/BfghK3WngQeS/D8sP+vaWcBKEmSJEmqiQWgUvLHPya65Rm3A5siiFJolhPc2267GtYOjjhLqq4FTqn2sVnAWcDkah9fCnwOPAzcvfm5WzQABgFH8O37/GXL51t9f3m1tbnk2GXLia67liRJkiQVp0ZhixaA2trIkSMZPXp02EgpwU4w1c6kOB//HjUXg7mgGfDnah9bApzMt8u/rW0ArgP+Xu3j+wBXpi1dkbEAlCRJkiTVpHnY4nbb5WrnoKjFYjFuuOGGRGN3AJURxClUn8X5eAm1u7deFH4NtKj2seuB2Uk+//cExfHWfodXs9aKBaAkSZIkqSZxC8BGjRrRpEmTKLMohw0dOpRPP/00bORr4JmI4hSq90PWql9imysuqPbj2cDTKTy/DPhbtY/tRe4WnjnNAlCSJEmSVJO4BeD2228fb0lFprKykhtvvDHR2J+BigjiFLIRxN9BeQ7BTsBc0gj4YbWPPQPEUnydwXz75318bUMVMwtASZIkSVJN4rZ8zZuHXh2sIvLkk08yY8aMsJEvcPdfOqwE3ouzthe5twvwCILTe7c2thavs5Lg19DW2tQqUZGzAJQkSZIk1SRuy2cBKICKigpuvfXWRGN/wpN/02VgyNpNkaVIzm41fOzzGj6WjOoHoNT02krAAlCSJEmSVJO4p3xYAAqgf//+fP3112EjnwCvRhSnGLxEcIpuTX4KdIwwSyI71PCx5bV8rerP27GWr1PUPDlFkiQVghbk3r1vCkWM4PIbScXHHYCKa/ny5fTq1SvR2B9J/Z5viq8CuAe4N876gwSX2Ub19/Z3CQ54qUn1LyDEgPW1fJ+1CV5bSbAAlCRJ+Won4A/Ar/ErwVFZTXAZVwWwbKvHUmAGMIfghL85wOLsRJSURjvFW/AQEPXq1Yvly0M3dI0kOLhC6fUQcA3Bff+q2xt4EuhC5i+7PgZ4AfhenPU11X5cAmxD7UrAbRO8tpJgAShJkvJRQ+Bl4IRsBykyW2/52TXB7CpgAsGNuz8HJhNcClaemWiSMmD3eAu77LJLlDmUYyZNmsTf//73sJEYcENEcYpNOfAb4I0462cA/wC6krkSsBvwN8KvvlhRw8d2pHYFYPUv9Nb2UuJkVT+8pCBYAEqSpHzUEcu/XLc98OPNjy3KgY+B0cCYzY/ql/VIyh1xW75dd030NQAVshtvvJFNm0K7pVeBTyOKU4yG8d+Srya/Ijgo42ektyzbH3gAOG3zjytCZhfU8LHDgG9q8b6HJ/Ha8fKkWuY1JOQE9HzmISCSJCkfHZ3tAKqVJgTF7R+B4QSXDr8FXA3sl8VckmoWdwfgbrt5CGexGjJkCG+99VbYSDlwXURxitnvgA9D1tsDUwnKwPp1fK89gd4Eu/lPSzC7xUS+veu/bS3euzlwaLWPxft5bwTKqn0s1dvEHJni/BY5f69LC0BJkpSPmmU7gNKiMcEnKH2BmcAU4GbgwGyGkgQE99yqft+t/3AHYHGqqKjg+uuvTzR2P1AaQZxiVwGcRVDyxfMd4AmC+/TeBOyTwus3B84mOHl4FtCd4O/tZG0guPXH1i5M4flbXECwK29rY0Pmq5+SfFiK79cpxfktqpedjWr5OhnjJcCSJEnKFa2AWzc/PgEGA0/jgSJSNoQ2fBaAxemhhx5i1qxZYSOLCE6pVTQWE9xq423giJC5fYG7Nz/mAB8RlHrzgXVAJcEXV3ckuMz3MIKdcHXdOTgY+NFWP96PoNB7NsnnN+bb95KcS3ALkXgmEpxOvEUHIPSGlVtpDvw2ydnqVlf78c61fB0pb51BsBW2pke+3QT8J8T/ucTIwYZfkgpYH8L/TPZROI8Kgk8gfoykKP2IkN+bS5cujam4fPPNN7HmzZsn+jP70iz8WlWwW/dZov87+p8JcjUjOAxk6+csAPZI8ufVu4b3vCnBc/5Qbb4SaJ3Ee5UQnGpc088zmcueb6r2nIlJPCdS7gCUJEkF5dhjj+WOO+7IdoyCUVlZyZo1a/7nY8uWLfufx7x585gzZw5ff/01GzZsSHeERgS7BS4guMypH8EnHNXv8SMpveJ+gt6oUSN23DHV22op33Xv3p3Vq6tvcvofnwEDI4qj/7WW4O/Jt4C/Ajtl+P0+B64n2HkYZh1wO3DfVh/bFfgXcCbBpck1abD5ed2rfbwUeDjBew4C7uC/t7yrDzwPnAzMi/OcHYHHgP9L8Nphql/u3BroArxSh9dMKwtASZJUUHbaaSfatWuX7RhFqaqqigULFjB16lQmTJjwn8f06dOprKxMx1u0IviH/+0El/M8hJcHS5kS92Cevfbai5KSkiizKMuGDRvGiy++mGisO1AVQRzF9zjBCcw9gCsILmlNp88IyrzBJP//ujdwOrD1P84OAiYRlG4vERSB6whOLj6J4DLc6if/VhLcQzC0hSa4xPkF4Pxq7/cFwb8b3ia49LkJ8L3NuX7Ff0/+HQocS8gp6HG8R7C7cesTkl4CPiA4EXs5UP3o7IcIdkhKBcFLgCVJmRD3EuCOHTtm+yopVVNRUREbM2ZM7K677op17Ngx1qJFi3RderQeuA1oEdUvPKmIDCDO77327dtn+48VRWjdunWxffbZJ9Gfx8ne003RaU5wUvD7BGVdbf+uXUjwRbfanOC7xQ4E9+2rbYZy4NwU3u87BF8gTPV9PiMoAhdW+3iyJx9fluL77Z/Cz6nO3AEoSZKkjGrUqBHHH388xx9/PACbNm3io48+4o033mDYsGFMmDCBWCxWm5duCvwZ6Ab8DXiA4DIoSXUX9xPT/feP9HNWZdnNN99MaWlp2MgSgqJJuWU1wQ6zhwgOpGgLtCHYDbcPwU61ZgR/l1YR3FpjGcEhGzOACQSl3SSCsqouVhDstHsQuJj/Xp6bjFnArwmKzGQtBn5KcEn07kk+522CXYOrUnif6h4juJz4dr59crFU8NwBKEnKBHcAFpBp06bFbr755tgBBxxQ1x2B8wnugSSp7uYS5/favffem+0/NhSRf//737EGDRok+rP34mz8AlXeag08R1C0xfs1VUVQQF5F3T7PbgncT1CGxnuv6QS/hre+r0FtdwBusQfB6cVDgZkEBejGGt470q+meOMGZdoZBL/oa1JBcN19vvgJMDJkvTGQ9jufS5Jq1Ae4pqaFjh078vrrr0ccR+nyySef8NRTT/Hkk0+ycuXK2r7Me8DVBLsWJKWuCcH9uGrcpfPyyy/TpUuXaBMpclVVVfz4xz9mzJgxYWNjgRPx3n9KXQPgGILdiDsT7ERcSrB77yOC++mlS0PgOOBAglKwZPPrfwpMTuP7SEXNHYCSpExwB2CBW7duXWzgwIGxY445pra7ATcSXPa0PZJS1YqQ318TJ07M9h8RikDv3r0T/TlbARwa/S9PSbWRynXXkiRJUiS22WYbLr74YsaPH8+4ceM455xzqF+/fiov0QC4kuAr+x0yElIqXAfFWygpKWHfffeNMouyYOrUqfTs2TPR2L0EJ6tKygMWgJIkScppbdq04YUXXmDGjBlceeWVNGqU0qb7PYE3gCdwN6CUrNbxFvbYYw+23XbbKLMoYpWVlfzyl7+krKwsbOwr4I6IIklKAwtASZIk5YV9992Xhx56iKlTp3LhhRdSr15K/5T9FcG9fo7JTDqpoMQtAFu3jrukAnHnnXfyySefJBq7kuDUWEl5wgJQkiRJeWXfffflmWee4dNPP+Wkk05K5an7AWOAG/HfwVKYI+ItHHnkkVHmUMTef/99brvttkRjDwMjIogjKY38h48kSZLy0pFHHsm7777Lc889x1577ZXs0xoC9xB88rp7xsJJ+WtbIO5N/g4//PAIoyhKa9eu5de//jVVVaEH+n4J3BBRJElpZAEoSZKkvHbeeecxbdo0br75Zpo2bZrs004GPgaOzVwyKS8dSsjniRaAheumm25i1qxZYSMx4DfAumgSSUonC0BJkiTlvW222YZbb72VKVOm0K5du2SftjvBJcHXZC6ZlHd+EG+hcePGHHRQ3AOClcdeeOEF/v73vycaexB4N4I4kjLAAlCSJEkFY++99+att96id+/eNG7cOJmnNAD6EJxmWZLRcFJ+OC7ewiGHHEKDBg2izKIIfPXVV1x22WWJxmYAPSKIIylDLAAlSZJUUOrVq0f37t2ZMGFCKgcW/BF4AWiSuWRSXvhRvIWjjz46yhyKwPr16+ncuTOrVq0KG9sI/AxYH00qSZlgAShJkqSCdPDBBzNu3DiuvvpqSkqS2tx3NjAM2D6zyaSctQuwT7zF446LuzlQeeqmm25i8uTJicbuAP4dQRxJGWQBKEmSpILVpEkT+vbty+DBg2nWrFkyTzkJeBNokdlkUk6Ku/sP4Ec/Cl1Wnnnqqad48MEHE429CtweQRxJGWYBKEmSpIJ3/vnn89lnn9GqVatkxtsAHwC7ZTaVlHPaxFvYeeed2W+//aLMogz64osv6NatW6Kx+cDlBKf/SspzFoCSJEkqCgcccACjR4/mhBNOSGa8FTAc+E5mU0k55cR4C23btk32UnrluGXLlnHmmWeyevXqsLFNwIXA4mhSSco0C0BJkiQVjZ122om33nqLzp07JzN+BPAOsGNmU0k5oSVwVLzF448/PsIoypSNGzdy9tlnM2vWrESjtwDvRRBJUkQsACVJklRUmjZtNU/mgAAAHHhJREFUyssvv8wtt9ySzPjhwLvADplNJWXdyUD9eIsnnXRShFGUKd26deO99xL2eiOAuyKIIylCFoCSJEkqOiUlJfTq1Ys777wzmfEjgBeAxplNJWXVqfEWdt55Z37wgx9EmUUZ0K9fP/r3759obB5wEVCV+USSomQBKEmSpKLVs2dP+vbtm8y9zU4GnsF/P6twtY+30K5dO+rV85d+PnvzzTe5/vrrE42VA13wvn9SQfJPcUmSJBW1q6++mqeffpoGDRokGj0b+FsEkaSoHQrsGW+xffu43aDywMcff8y5555LZWVlotFLgY8jiCQpCywAJUmSVPQuvPBCHn744WR2Al5HcHmcVEjinopTUlJiAZjHZsyYQceOHVm7dm2i0XsIdjlLKlAJv8wpSZIkFYNLL72U5cuXc9NNNyUafQz4Cvgg86kiMw74TrZDKGvi7v477LDD2H333aPMojRZsGABp512GkuWLEk0+gbQM4JIkrLIAlCSJEna7MYbb2TNmjXccccdYWONgVeAHxDcML8QfBew5dG3dO4cd3OgctiqVas4/fTTKS0tTTQ6FbgQD/2QCp6XAEuSJElbue222/jFL36RaOw7wD+B+plPJGXPOeeck+0ISlF5eTmdO3dm4sSJiUYXA2cCqzOfSlK2WQBKkiRJWykpKWHAgAGceOKJiUZPBm6OIJKUFQcccACtW7fOdgylYP369Zx55pmMGjUq0egaoAMwM+OhJOUEC0BJkiSpmsaNG/Pyyy9zwAEHJBr9E0ERKBUcd//ll3Xr1nHGGWfw9ttvJxqtIDj45dPMp5KUKywAJUmSpBq0bNmS119/nebNm4eN1QOeAHaIJJQUobPPPjvbEZSktWvX0qFDB959991Eo5uAXwAJByUVFgtASZIkKY4DDzyQAQMGJBrbE3g4gjhSZPbdd1+OOuqobMdQElavXs1pp53G6NGjkxn/HfBihiNJykGeAixJkiSFOPfcc7nqqqt44IEHwsbOB14Hno4mVaSeAMZlO4TS7nCgW7zFX/3qVxFGUW0tW7aMjh07Mn78+GTG/wQ8muFIknKUBaAkSZKUwL333su4ceP45JNPwsb6ASMITtYsJO8RlIAqLEPiLdSvX5+LL744yiyqha+//ppTTz2VadOmJTPeC7gzs4kk5TIvAZYkSZISaNSoEU8//TTbbLNN2NgOwL0RRZLqYj+gU7zFU045hb322ivCOErV5MmTadu2bbLl383ArRmOJCnHWQBKkiRJSTjooIPo169forGLgA4RxJHq4mqgfrzFrl27RhhFqRozZgwnnngi8+bNS2b8z8DtGY4kKQ9YAEqSJElJuuSSS+jQIWG/dx/QOII4Um1sD8S9vneXXXbhzDPPjDCOUjFkyBDat2/PihUrkhn/E3BHhiNJyhMWgJIkSVKSSkpK+Mc//kGLFi3Cxg4Gro8okpSqS4Ht4i1eeeWVNGrUKMI4SkYsFuPWW2/l7LPPpqysLJmn/BHv+SdpKxaAkiRJUgp23XVXbr755kRjNwI7RxBHSkUT4Nq4i02a8Nvf/jbCOErGqlWrOOuss+jVqxdVVVWJxjcBvwH+kvlkkvKJBaAkSZKUoquuuoojjzwybGR74JaI4kjJuhzYI97iL37xC3be2d46l3zxxRccc8wxvPbaa8mMlwFnA49mNpWkfGQBKEmSJKWoQYMGPPLII9SrF/rP6SuAVhFFkhJpCvSIt1hSUkL37t0jjKNEXn75Zdq0acOMGTOSGV8GtANezWwqSfnKAlCSJEmqhWOPPTbRaakN8Ab8yh1XALvFWzz11FM59NBDI4yjeMrLy7nmmms455xzWLt2bTJPmQ38CPggo8Ek5TULQEmSJKmWbrnlFpo1axY20hmwVVG2tQB6hg306tUrmiQK9fnnn3P00UfTr18/YrFYMk/5CDgemJbZZJLynQWgJEmSVEt77LEHN9xwQ9hIPeBPEcWR4vkTIYfSdOrUiWOPPTbCOKouFovRp08fjjnmGCZPnpzs054AfgzMz1gwSQXDAlCSJEmqg+uuu46WLVuGjZyH9wJU9uwPXBVvsaSkhNtuuy3COKpuwYIFdOjQgWuvvZby8vJknlIJXA1cDCT1BEmyAJQkSZLqYLvttktmF+CNEcWRqvsb0CjeYpcuXfj+978fYRxtEYvFGDBgAIcccghvvvlmsk9bApwCPJC5ZJIKkQWgJEmSVEe//e1v2XHHHcNGzgd2iiiOtMWpBPehrFHDhg258847I4yjLWbOnMnJJ5/MZZddxsqVK5N92vvA0cCojAWTVLAsACVJkqQ6at68Oddee23YSFOCU1ilqGwH9A8b6NatGwcffHBEcQTBCb933XUXrVu3ZuTIkck+rRL4M3ASMCdj4SQVNAtASZIkKQ26devGtttuGzZyJSGXYkpp1hv4brzF3XbbjVtvvTXCOMVt06ZN9O/fn/3224+ePXtSVlaW7FNnAG2AO4BNGQsoqeBZAEqSJElp0KJFC7p27Ro2sjvQJaI4Km4/BS4JG+jVqxfbbbddRHGK2/jx4znhhBO44oormD8/pQN7nwWOAT7NTDJJxaRBtgNIBeRSgu35kqTMOyzbAaSaXHnllTzwwANUVVXFG/kl8FyEkVR8WgL/BEriDbRp04ZLL700ukRFau7cufTo0YPBgwcTi8VSeeoq4Frg8cwkk1SMLACl9Hko2wEkSVJ2HXjggZx22mkMGzYs3sipwB7AvOhSqYiUAP8A9ow30KhRIwYMGEC9el4Mlinz58/n7rvv5rHHHqO8vDzVpw8BfgektFVQkhLxT31JkiQpjS6//PKw5foEuwClTPgdcFbYwB/+8AcOPfTQiOIUlwULFtC9e3f2339/HnjggVTLv4XAuQS3CbD8k5R2FoCSJElSGnXo0IFddtklbOSiqLKoqLQF7gsbOOKII+jZs2dEcYrHvHnzuO6669hvv/3o27dvKgd8AMQIdm0eAryYkYCShAWgJEmSlFYNGzbkootCO75WBJ/sS+myB/ASIadMN2vWjMGDB9OokQdRp8u///1vLrroIvbZZx969+6davEH8D7BIR+XAivSHlCStmIBKEmSJKXZL3+Z8Crfs6PIoaKwDfAysGvYUJ8+fWjVqlU0iQpYVVUVQ4cO5aSTTuKoo47i6aefZuPGjam+zCzgHOBE4JO0h5SkGlgASpIkSWl2+OGHc8ghoZv8zosqiwpaQ+AFgl1kcZ133nme+ltHCxYs4O677+aggw7irLPOYtSoUbV5mVXAjQQ7gF9KZz5JSsRTgKXklRF8tU6SlH0tge2zHUIK83//939MmTIl3vJhwP7AzOgSqcBsOfG3Q9jQ/vvvzyOPPBJNogJTWVnJ8OHDGTBgAMOGDaOysrK2L7UBGAj0AhalK58kpcICUEreeGC/bIeQJAHQB7gm2yGkMOeeey533HFH2MipWACqdkqAB0hwoMz222/P0KFD2WGHHaJJVQBisRgfffQRL7zwAoMGDWLBggV1ebkNwBPAX4A56cgnSbVlAShJkiRlQOvWrTnggAP48ssv4420Bx6KMJIKQwnBF0F+FzZUv359Bg0a5H3/kvTxxx/z/PPP8+KLLzJ79uy6vtxG4J/AnUCdX0yS0sECUJIkScqQjh070qdPn3jLJwONgYroEinP1SPY+XdlosE77riDDh1Crw4uahUVFYwePZphw4bx6quvUlpamo6XXUNwWXZfLP4k5RgLQEmSJClD2rVrF1YANgPaAO9Fl0h5rDHwJEkcIHPNNdfQo0ePzCfKMwsXLuSNN95g2LBhjBgxgrVr16brpb8G+gEDCA76kKScYwEoSZIkZchPfvITGjduTEVF3E1+J2IBqMRaEpz2e1KiwQsvvJD7778/84nyQEVFBR9++CEjR45k2LBhfPLJJ8RisXS+xXigN8GJvrU+IUSSomABKEmSJGVIs2bNaNu2LSNHjow30jbKPMpLhwOvAvskGjznnHP45z//Sb169TKfKgetX7+eiRMnMnLkSEaOHMnYsWMpKytL99ssBp4BHgc+T/eLS1KmWABKkiRJGXTiiScmKgDrA5uiS6Q8cjbBKbLbJhrs0qULgwYNokGD4vkUb8aMGYwfP54PP/yQDz/8kEmTJlFZmZGNeBuBNwj+Xwzb/GNJyivF87eDJEmSlAXHHXdc2HJz4BDcSaT/tR1wFwlO+t2ic+fOPPvsszRs2DCzqbIkFotRWlrKxIkTmThxIp9++injxo1j2bJlGX1bgkt8nwUGE+z8k6S8ZQEoSZIkZdAxxxxDSUlJ2L3HfoAFoP7rVOBR4HvJDF988cX079+/IHb+VVVVMWfOHKZNm8b06dOZOXMmEydOZNKkSaxevTqqGJMISr9ngbQcDSxJuSD//5aQJEmSctgOO+zAwQcfzNSpU+ONHBZlHuWsHYD7gV8nM1xSUkKPHj248847KSkpyWiwdFu5ciWlpaXMmjWLadOmMWXKFKZNm8a0adNYv3591HE2Au8TXNo7HJgSdQBJioIFoCRJkpRh3//+98MKwNZRZlHOaUBQ+t0G7JbME5o0acLAgQP52c9+lslctVJZWcnixYuZN28eCxYsYO7cuZSWllJaWsrs2bMpLS1lxYoV2Y65mKDsewMYAazKbhxJyjwLQEmSJCnDDjssdJOfOwCLUwlwHkHxd2CyT9p111155ZVXaNOmTcaC1SQWi7Fo0SIWLlz4n3Jvy7fz58//z2PRokVUVVVFmi0JZQT383sPeGvz93MupCRlkgWgJEmSlGGHHnpo2PLuBJd/Zn1blCLREDgHuBE4MpUntm/fnqeeeorvfOc7dQ6xdu1ali1bxpIlS1i2bFncx5IlS1iyZAmLFi1i48a8Ofy2nOCy3tEEpd9HQEVWE0lSllkASpIkSRmWoAAEOICgpFDh2hP4BcHJvnum8sSGDRvSq1cvevToQb169Vi5ciVr165lzZo1rF27llWrVrF69WrWrl37n49vmdny4+rFXkVFQfVhc4EPt3r8m6AElCRtZgEoSZIkZdjee+9Nw4YNw3ZQ7YMFYCE6CPgxwaW+JwH1avMijRs35sEHH+Tuu+9mzZo16cyXj2YDEwlO651AcDnvvGwGkqR8YAEoSZIkZVj9+vXZc889KS0tjTeyd4RxlHkdgL8CCbd+JmPLTr4iswKYuvkxiaD0mwiszGYoScpXFoCSJElSBPbee++wAvB7UWZRRh0PvAI0ynaQPLCJ4PLdrwiKvinAtM3fLspiLkkqOBaAkiRJUgS+973Qji+le8Ipp/XA8m9ry4EFBJfufgXM3PztV0ApsCFrySSpiFgASpIkSRHYc8/Qjm+nqHIo447IdoCIrAW+ARZu9e08grJvy7fzgbJsBZQk/ZcFoCRJkhSBnXYK7fgsAAvHdGCvbIeohXXAss2PJVt9f+vHfP5b+BXdTQklKZ9ZAEqSJEkRaNmyZehyVDmUcQ8BJwMlEb9vBUEptwpYvfn7azZ/u2Krb+MVfOUR55UkRcgCUJIkSYpAggKwBVCf4FAE5bchwBVAL2D3ODOVBOXcGoJLZNcSlHZlBDvxVm3+/nqCU2+3nlm1+ftbHlvKvY2Z+MlIkgqDBaAkSZIUgRYtWoQt1wO2JSh3lP8eA/4JHERwIMhaghJvy448yzpJUqQsACVJkqQINGnSJNHIRLK3A3CXLL1vIdsAfJ7tEJIkgQWgJEmSFInGjRsnGvleFDkkSVLxqZftAJIkSVIxaNSoUbYjSJKkImUBKEmSJEXAAlCSJGWLBaAkSZIUgVgslu0IkiSpSFkASpIkSRGoqKjIdgRJklSkLAAlSZKkCGzYsCHbESRJUpHyFGBJkiQpAknsALweWBtBlFR9kO0AkiSpbiwAJUmSpAiUlZUlGnkMWBNBFEmSVGS8BFiSJEmKwLJly8KWN2D5J0mSMsQCUJIkSYrA0qVLw5ZXRJVDkiQVHwtASZIkKQIJdgCGLkqSJNWFBaAkSZIUAQtASZKULRaAkiRJUgTmzp0btrw4qhySJKn4WABKkiRJEZg9e3bYcmlEMSRJUhGyAJQkSZIikKAAnBNRDEmSVIQsACVJkqQMKy8vZ+HChWEjFoCSJCljLAAlSZKkDJsxYwaxWCxsZHZEUSRJUhGyAJQkSZIybPLkyWHLVcBXEUWRJElFyAJQkiRJyrDPP/88bHkmsD6iKJIkqQhZAEqSJEkZlqAADN0eKEmSVFcWgJIkSVKGffbZZ2HLX0SVQ5IkFacG2Q6gotYQeD7bISRJeenIbAeQkjVnzhzmz58fNuIOQEmSlFEWgMqmesC52Q4hSZKUSWPGjEk0MjaKHJIkqXh5CbAkSZKUQePGjQtb/hqYF1EUSZJUpCwAJUmSpAz64IMPwpZD20FJkqR0sACUJEmSMmTRokVMmDAhbCS0HZQkSUoHC0BJkiQpQ0aMGEEsFgsbeS+qLJIkqXhZAEqSJEkZMnz48LDlucDEiKJIkqQi5inAyrQ5QP9sh5AkFZy2wGHZDiGF2bRpE++8807YyLtRZZEkScXNAlCZNgm4ItshJEkFpw8WgMpx77//PkuWLAkbeTOqLJIkqbh5CbAkSZKUAS+88ELY8iYgdHugJElSulgASpIkSWlWWVnJ888/HzYyElgaURxJklTkLAAlSZKkNBs1ahRLl4b2ey9HlUWSJMkCUJIkSUqzgQMHhi1vwgJQkiRFyAJQkiRJSqMVK1bwyiuvhI2MBhZFFEeSJMkCUJIkSUqnp556ivLy8rCRf0SVRZIkCSwAJUmSpLR64oknwpZXA6HbAyVJktLNAlCSJElKk/fee4/PPvssbORZYH1EcSRJkgALQEmSJClt7r///kQjj0eRQ5IkaWsWgJIkSVIafPnll7z++uthIxOBDyOKI0mS9B8WgJIkSVIa3HvvvVRVVYWN9I4qiyRJ0tYsACVJkqQ6Ki0t5fHHQ6/uXQAMjiiOJEnS/7AAlCRJkuqoV69ebNy4MWykL7AhojiSJEn/wwJQkiRJqoOvvvqKQYMGhY2sAvpHFEeSJOlbLAAlSZKkOrjhhhuorKwMG7kPWBFRHEmSpG+xAJQkSZJq6YMPPmDIkCFhI6uAByOKI0mSVCMLQEmSJKkWqqqq+N3vfkcsFgsbux93/0mSpCyzAJQkSZJq4ZlnnmHChAlhI0sIDv+QJEnKKgtASZIkKUWLFy+me/fuicZuJrgEWJIkKassACVJkqQU9ejRg+XLl4eNzAD+EVEcSZKkUBaAkiRJUgpGjRrFE088kWjsJmBj5tNIkiQlZgEoSZIkJWnNmjV07do10cEfbwKhRwNLkiRFyQJQkiRJStI111zDrFmzwkbWA1dGFEeSJCkpFoCSJElSEgYPHszjjz+eaOyPQGkEcSRJkpJmAShJkiQlMHv2bLp165ZobALwYARxJEmSUmIBKEmSJIUoKyvjrLPOSnTqbxnwM6AymlSSJEnJswCUJEmSQtx4441MmjQp0djNwLQI4kiSJKXMAlCSJEmK45lnnuHBBxNe1TsauD+COJIkSbViAShJkiTVYOzYsVx66aWJxlYCvwKqMp9IkiSpdiwAJUmSpGpmzpxJ586dKS8vDxuLAb8EZkcSSpIkqZYsACVJkqStrFy5kk6dOrF06dJEo3cBr0UQSZIkqU4sACVJkqTN1q1bR8eOHZk+fXqi0XcIDv6QJEnKeRaAkiRJElBRUUGXLl344IMPEo1+CZwPbMp8KkmSpLqzAJQkSVLR27BhAxdccAFvv/12otEVwBnA8synkiRJSo8G2Q4gSZIkZdPatWvp1KkT7733XqLRCuBMIOH1wZIkSbnEHYCSJEkqWuvXr6dLly7JlH8x4HfAmMynkiRJSi8LQEmSJBWlNWvW0KlTJ955551kxm8A/pHhSJIkSRnhJcCSJEkqOl9//TWnn346U6ZMSWb8T8B9GY4kSZKUMe4AlCRJUlGZMmUKJ554YrLlX1/gzgxHkiRJyigLQEmSJBWNoUOHctxxxzFnzpxkxvsA12Y4kiRJUsZZAEqSJKngbdq0iR49etC5c2dWr16dzFNuIyj/YplNJkmSlHneA1CSJEkFbfny5XTt2pUhQ4Yk+5TbgVsyGEmSJClSFoCSJEkqWCNGjOCiiy5i8eLFyYxvBC4Bns5sKkmSpGh5CbAkSZIKzqZNm7jnnnvo2LFjsuVfOXAeln+SJKkAuQNQkiRJBWXKlClccskljB8/PtmnLCAo/8ZkLpUkSVL2uANQkiRJBaGiooIePXpwxBFHpFL+jQRaY/knSZIKmDsAJUmSlPf+9a9/cdVVVzF16tRUnvYE8FuCy38lSZIKljsAJUmSlLfmzZvH+eefT7t27VIp/9YDlwEXY/knSZKKgDsAJUmSlHeWLVvG3XffzcMPP8y6detSeepk4HxgSmaSSZIk5R4LQEmSJOWNdevW0adPH/72t7+xatWqVJ4aAwYA1wBlGQknSZKUoywAJUmSlPNWrVrFww8/TJ8+fVi0aFGqTy8FLgXeTX8ySZKk3GcBKEmSpJw1f/58+vbtyyOPPMLq1atTfXoV8BDwByCl64QlSZIKiQWgJEmSckpVVRX/+te/ePTRRxk6dCgbN26szctMIzjhd1Raw0mSJOUhC0BJkiTlhOnTp/Pss8/y1FNP8dVXX9X2ZVYBtwP9gFo1h5IkSYXGAlCSJElZM3XqVF577TWeffZZPvvss7q81EZgIHALkPJNAiVJkgqZBaAkSZIis2LFCsaOHcvw4cMZPnw4paWldX3JKuB54M/AzDoHlCRJKkAWgJIkScqYuXPnMmbMGMaOHcvo0aP54osvqKqqSsdLx4DXgF5AnbYOSpIkFToLQEmSJNXJqlWrmDNnDnPmzGHWrFlMmTKFL774gi+++IKVK1em++02As8AfwOmpPvFJUmSCpEFoCRJKijTpk2jR48e2Y5RcMrKyigvL6esrIxly5axfPlyli1bxsKFC1mzZk0UERYDTwAPAnOjeENJkiRJkiRlTx+CS0B9FPajChgJXAA0QpIkSbXiDkBJkiTlmmnAs8BgYEaWs0iSJOU9C0BJkiTlgunAqwSl34QsZ5EkSSooFoCSJCkfLc12ANXZcuBD4E1gGPBVduNIkiQVLgtASZKUj0ZmO4BS9g3wHjAGeJ/gBN9YVhNJkiQViZJsB5AkSaqlvsDV2Q6hb1lMsJtvJjCZ4HLeCZs/LkmSpCywAJQkSfmqBOgMdAUaZzlLMdgArCM4mXclsKza4xuC4m9NtgJKkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiRJkiTp/9uDAwIAAAAAIf9fNyQAAAAAAAAAAAAAAAAAAAAAAKwFUXlS2J6ta38AAAAASUVORK5CYII="
    }
   },
   "cell_type": "markdown",
   "id": "218ef059",
   "metadata": {},
   "source": [
    "<small> Image from [commons.wikimedia](https://commons.wikimedia.org/wiki/File:Full-adder.svg) </small>\n",
    "<img src=\"attachment:adder.png\" alt=\"Adder\" width=\"400\"/>"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "026fa119",
   "metadata": {},
   "source": [
    "To build a COP (Constraint Optimization Problem) model, we need first to import the library PyCSP$^3$:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "72e79bc8",
   "metadata": {},
   "outputs": [],
   "source": [
    "from pycsp3 import *"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "f5c87922",
   "metadata": {},
   "source": [
    "Then, we need some data. Here, we need to describe the functions and the gates (we use named tuples to represent them)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "c69e47b3",
   "metadata": {},
   "outputs": [],
   "source": [
    "f_or = [\n",
    "    [0,1],\n",
    "    [1,1]\n",
    "]\n",
    "f_and = [\n",
    "    [0,0],\n",
    "    [0,1]\n",
    "]\n",
    "f_xor = [\n",
    "    [0,1],\n",
    "    [1,0]\n",
    "]\n",
    "functions = cp_array([f_or, f_and, f_xor])\n",
    "\n",
    "Gate = namedtuple('Gate', 'f in1 in2 out')\n",
    "gates = [None, None, Gate(2,0,0,-1), Gate(1,0,0,-1), Gate(2,0,2,1), Gate(1,0,2,-1), Gate(0,3,5,0)]\n",
    "nGates = len(gates)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "ee4231ad",
   "metadata": {},
   "source": [
    "Logical functions are given under their matrix forms; here, we have successively the functions OR (index 0), AND (index 1), and XOR (index 2). Each gate is given its logical function (index given by ’f’), its two input (with 0 for false, 1 for true and the index of another gate otherwise), and its observed output (0 or 1 if any, -1 otherwise). Note that the two first gates are special; they are inserted (with None values) for reserving indexes 0 and 1 (for false and true)."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "76a0f70d",
   "metadata": {},
   "source": [
    "**Remark.** Because it is not possible to use a special object as an index of a list of integers in Python (later, we need this when posting some constraints), we have to transform the lists of integers of the three functions into more specific lists with the function cp_array(). The good news is that when the data is loaded from a file (which is the usual case), all lists of integers have the specific type of list returned by cp_array(), and so, it is very rare to need to call this function explicitly."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "d047ae68",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[None, None, Gate(f=2, in1=0, in2=0, out=-1), Gate(f=1, in1=0, in2=0, out=-1), Gate(f=2, in1=0, in2=2, out=1), Gate(f=1, in1=0, in2=2, out=-1), Gate(f=0, in1=3, in2=5, out=0)]\n"
     ]
    }
   ],
   "source": [
    "print(gates)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "9d7cd072",
   "metadata": {},
   "source": [
    "We start our COP model by introducing a first array $x$ of variables. This will allow us to identify the faulty gates."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "b605d552",
   "metadata": {},
   "outputs": [],
   "source": [
    "# x[i] is -1 if the ith gate is not faulty (otherwise 0 or 1 when stuck at 0 or 1)\n",
    "x = VarArray(size=nGates, dom=lambda i: {-1} if i < 2 else {-1, 0, 1})"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "0ac8d63c",
   "metadata": {},
   "source": [
    "We can display the structure of the array, as well as the domain of the variables. Remember that the two first variables are very special (and so, cannot be faulty)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "ee1c594d",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Array x:  [x[0], x[1], x[2], x[3], x[4], x[5], x[6]]\n",
      "  Domain of x[0] is: -1\n",
      "  Domain of x[1] is: -1\n",
      "  Domain of x[2] is: -1 0 1\n",
      "  Domain of x[3] is: -1 0 1\n",
      "  Domain of x[4] is: -1 0 1\n",
      "  Domain of x[5] is: -1 0 1\n",
      "  Domain of x[6] is: -1 0 1\n"
     ]
    }
   ],
   "source": [
    "print(\"Array x: \", x)\n",
    "for i in range(nGates):\n",
    "    print(f\"  Domain of {x[i]} is: {x[i].dom}\")                        "
   ]
  },
  {
   "cell_type": "markdown",
   "id": "2ff2e4d2",
   "metadata": {},
   "source": [
    "We introduce a second array $y$ of variables to be able to reason with intermediate computations (outputs)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "26f305b6",
   "metadata": {},
   "outputs": [],
   "source": [
    "# y[i] is the (possibly faulty) output of the ith gate\n",
    "y = VarArray(size=nGates, dom=lambda i: {i} if i < 2 else {0, 1})"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "36369a90",
   "metadata": {},
   "source": [
    "Concerning the constraints, we have first to ensure that some variables of $y$ are coherent with respect to the observed output. Note that we could have directly integrated these unary constraints when defining the domain of variables of $y$. Here, we post a group of constraints *Intension*."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "f798c708",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    # ensuring that y is coherent with the observed output\n",
    "    y[i] == gates[i].out for i in range(2,nGates) if gates[i].out != -1\n",
    ");   "
   ]
  },
  {
   "cell_type": "markdown",
   "id": "832ed735",
   "metadata": {},
   "source": [
    "We can display the internal representation of the two posted constraints; this way, although a little bit technical, we can see that the two constraints are correctly formed (note that 'eq' stands for 'equal to')."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "id": "afc9f065",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "intension(function:eq(y[4],1))\n",
      "intension(function:eq(y[6],0))\n"
     ]
    }
   ],
   "source": [
    "print(posted())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "f2d31671",
   "metadata": {},
   "source": [
    "For simulating the behaviour of a gate, we introduce the following function that involves a partial form of constraint *ElementMatrix*:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "id": "935f1da0",
   "metadata": {},
   "outputs": [],
   "source": [
    "def apply(gate):\n",
    "    return functions[gate.f][y[gate.in1]][y[gate.in2]]"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "a58e3d8e",
   "metadata": {},
   "source": [
    "We can now post a group of constraints *Intension*. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "id": "71381b6f",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    # ensuring that each gate either meets expected outputs based on its function or is broken (either stuck on or off)\n",
    "    (y[i] == x[i]) | (y[i] == apply(gates[i])) & (x[i] == -1) for i in range(2, nGates)\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "fde04dce",
   "metadata": {},
   "source": [
    "The expression of these new constraints are rather complex. In order to remain in the perimeter of XCSP$^3$-core, some auxiliary variables, called aux_gb, are introduced automatically. We can then combine constraints *Intension* and *ElementMatrix*, as we can see when executing:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "id": "c4ac43cb",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "intension(function:or(eq(y[2],x[2]),and(eq(aux_gb[0],y[2]),eq(x[2],-1))))\n",
      "intension(function:or(eq(y[3],x[3]),and(eq(aux_gb[1],y[3]),eq(x[3],-1))))\n",
      "intension(function:or(eq(y[4],x[4]),and(eq(aux_gb[2],y[4]),eq(x[4],-1))))\n",
      "intension(function:or(eq(y[5],x[5]),and(eq(aux_gb[3],y[5]),eq(x[5],-1))))\n",
      "intension(function:or(eq(y[6],x[6]),and(eq(aux_gb[4],y[6]),eq(x[6],-1))))\n",
      "element(matrix:(0,1)(1,0), index:[y[0], y[0]], condition:(eq,aux_gb[0]))\n",
      "element(matrix:(0,0)(0,1), index:[y[0], y[0]], condition:(eq,aux_gb[1]))\n",
      "element(matrix:(0,1)(1,0), index:[y[0], y[2]], condition:(eq,aux_gb[2]))\n",
      "element(matrix:(0,0)(0,1), index:[y[0], y[2]], condition:(eq,aux_gb[3]))\n",
      "element(matrix:(0,1)(1,1), index:[y[3], y[5]], condition:(eq,aux_gb[4]))\n"
     ]
    }
   ],
   "source": [
    "print(posted(-1))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "4d668666",
   "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": 12,
   "id": "dff29093",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "  Actually, the instance was not solved\n"
     ]
    }
   ],
   "source": [
    "if solve() is SAT:\n",
    "    print(values(x))"
   ]
  },
  {
   "cell_type": "raw",
   "id": "b66b3a69",
   "metadata": {},
   "source": [
    "Here, we have only one faulty gate. Anyway, in the general case, we want to be sure to have a minimal number of faulty gates. This can be written: "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "id": "1370b1d9",
   "metadata": {},
   "outputs": [],
   "source": [
    "minimize(\n",
    "    # minimizing the number of faulty gates\n",
    "    Sum(x[i] != -1 for i in range(2, nGates))\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "610b0852",
   "metadata": {},
   "source": [
    "We can run again the solver, with this optimization task. Note that we need to check that the status returned by the solver is now OPTIMUM. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "id": "640841e3",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "  Actually, the instance was not solved\n"
     ]
    }
   ],
   "source": [
    "if solve() is OPTIMUM:\n",
    "    print(values(x))\n",
    "    print(\"Number of faulty gates: \", bound())\n",
    "    print(\"Faulty gates: \", [i for i in range(2,nGates) if x[i].value != -1])"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "6c392256",
   "metadata": {},
   "source": [
    "Finally, we give below the model in one piece. Here the data is expected to be given by the user (in a command line)."
   ]
  },
  {
   "cell_type": "raw",
   "id": "97ff456b",
   "metadata": {
    "raw_mimetype": "text/x-python"
   },
   "source": [
    "from pycsp3 import *\n",
    "\n",
    "functions, gates = data  # note that the two first gates are special, inserted for reserving indexes 0 and 1 (for false and true)\n",
    "nGates = len(gates)\n",
    "\n",
    "# x[i] is -1 if the ith gate is not faulty (otherwise 0 or 1 when stuck-at-0 or stuck-at-1)\n",
    "x = VarArray(size=nGates, dom=lambda i: {-1} if i < 2 else {-1, 0, 1})\n",
    "\n",
    "# y[i] is the (possibly faulty) output of the ith gate\n",
    "y = VarArray(size=nGates, dom=lambda i: {i} if i < 2 else {0, 1})\n",
    "\n",
    "\n",
    "def apply(gate):\n",
    "    return functions[gate.f][y[gate.in1]][y[gate.in2]]\n",
    "\n",
    "\n",
    "satisfy(\n",
    "    # ensuring that y is coherent with the observed output\n",
    "    [y[i] == gates[i].out for i in range(2, nGates) if gates[i].out != -1],\n",
    "\n",
    "    # ensuring that each gate either meets expected outputs based on its function or is broken (either stuck on or off)\n",
    "    [(y[i] == x[i]) | (y[i] == apply(gates[i])) & (x[i] == -1) for i in range(2, nGates)]\n",
    ")\n",
    "\n",
    "minimize(\n",
    "    # minimizing the number of faulty gates\n",
    "    Sum(x[i] != -1 for i in range(2, nGates))\n",
    ")"
   ]
  }
 ],
 "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
}