experiments.ipynb

{
 "cells": [
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "278293de",
   "metadata": {},
   "outputs": [],
   "source": [
    "import numpy as np\n",
    "import cvxpy as cp\n",
    "import pickle\n",
    "import matplotlib.pyplot as plt\n",
    "import fdt_verification\n",
    "from fdt_verification import *\n",
    "from fdt_verification_z3 import *\n",
    "from fdt_verification_reluval import *\n",
    "from util import *"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "69ad44fd-ce4f-45ea-90d2-73adcf8d6cdb",
   "metadata": {},
   "source": [
    "### Settings\n",
    "- using more than the number of available cores will interfere with experiment timing\n",
    "- timeout is in seconds for a single minimum adversarial perturbation or global robustness test"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "804ee339-1ae7-49da-9d79-85b5bb2cc88a",
   "metadata": {},
   "outputs": [],
   "source": [
    "# using more workers than can be run concurrently will interfere with experiment timing\n",
    "n_workers = 20\n",
    "# timeout in seconds for single minimum adversrial perturbation or global robustness test\n",
    "timeout = 3600\n",
    "# tolerance for minimum adversarial perturbation tests\n",
    "tol = 1e-3"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "99e2f0c4-2ef8-4ca3-ab5e-36034302466d",
   "metadata": {},
   "outputs": [],
   "source": [
    "# list of dataset names from OpenML\n",
    "dataset_names = [\"shuttle\", \"sylva_agnostic\", \"wall-robot-navigation\", \\\n",
    "                \"banknote-authentication\", \"helena\", \"MagicTelescope\", \\\n",
    "                 \"satimage\", \"texture\", \"JapaneseVowels\", \"hill-valley\"]"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "229a3d60-4d06-42c2-92f4-13175dd42693",
   "metadata": {},
   "source": [
    "### Check solvers and choose one"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "05bf8417-69c3-483a-8413-684621562274",
   "metadata": {},
   "outputs": [],
   "source": [
    "print(cp.installed_solvers())\n",
    "# use Gurobi since it is more robust on the harder datasets\n",
    "fdt_verification.solver = cp.GUROBI\n",
    "# load the license so we don't get spammed with the notification in spawned processes\n",
    "prob = cp.Problem(cp.Maximize(cp.Variable()), [])\n",
    "prob.solve(solver=fdt_verification.solver)\n",
    "pass"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "374fb12a-679e-456d-a6bf-8a9940989cdb",
   "metadata": {},
   "source": [
    "### Check model sizes (same for both sigmoid and linear splitting)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "c56665b8-684c-4947-9579-185bdb4185b7",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "shuttle depth 4; 13 nodes\n",
      "sylva_agnostic depth 7; 25 nodes\n",
      "wall-robot-navigation depth 8; 33 nodes\n",
      "banknote-authentication depth 6; 39 nodes\n",
      "helena depth 7; 49 nodes\n",
      "MagicTelescope depth 7; 57 nodes\n",
      "satimage depth 11; 107 nodes\n",
      "texture depth 14; 163 nodes\n",
      "JapaneseVowels depth 12; 251 nodes\n",
      "hill-valley depth 59; 305 nodes\n"
     ]
    }
   ],
   "source": [
    "for name in dataset_names:\n",
    "    f = load_model(name + \"_sigmoid\")\n",
    "    print(\"%s depth %d; %d nodes\" % (name, *f.size()))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "be2f2783",
   "metadata": {},
   "source": [
    "# Minimum Adversarial Perturbation"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "92116e1d-e355-471a-b6da-32239ee735c9",
   "metadata": {},
   "source": [
    "### Our algorithm (sigmoid splitting)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "4fd5338e-264a-43c7-bfc5-e429820ca20b",
   "metadata": {},
   "outputs": [],
   "source": [
    "for name in dataset_names:\n",
    "    f = load_model(name + \"_sigmoid\")\n",
    "    x, y = load_robustness_test_points(name)\n",
    "    perturbation, dist, exact, times = minimum_adversarial_perturbation(f, x, tol, n_workers=n_workers, timeout=timeout)\n",
    "    pickle.dump((perturbation, dist, exact, times), open(\"results/map_\" + name + \"_sigmoid.pkl\", \"wb\"))\n",
    "    print(name)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "7ea5b90e-76d3-4a3b-b871-1f909e4db837",
   "metadata": {},
   "source": [
    "### Our algorithm (linear splitting)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "3da94b94-764d-42cb-9f48-82b357e5ab65",
   "metadata": {},
   "outputs": [],
   "source": [
    "for name in dataset_names:\n",
    "    f = load_model(name + \"_linear\")\n",
    "    x, y = load_robustness_test_points(name)\n",
    "    perturbation, dist, exact, times = minimum_adversarial_perturbation(f, x, tol, n_workers=n_workers, timeout=timeout)\n",
    "    pickle.dump((perturbation, dist, exact, times), open(\"results/map_\" + name + \"_linear.pkl\", \"wb\"))\n",
    "    print(name)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "88832744-038c-47da-9a6c-da342283c566",
   "metadata": {},
   "source": [
    "### Z3 (linear splitting)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "d6fcb889-3c47-461b-997f-de8f5689fc45",
   "metadata": {},
   "outputs": [],
   "source": [
    "for name in dataset_names:\n",
    "    f = load_model(name + \"_linear\")\n",
    "    x, y = load_robustness_test_points(name)\n",
    "    perturbation, dist, exact, times = minimum_adversarial_perturbation_z3(f, x, tol, n_workers=n_workers, timeout=timeout)\n",
    "    pickle.dump((perturbation, dist, exact, times), open(\"results/map_\" + name + \"_z3.pkl\", \"wb\"))\n",
    "    print(name)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "96a84e49-1afa-445d-90b2-03d79d6a0bcb",
   "metadata": {},
   "source": [
    "### Our algorithm with refinement based on ReluVal (linear splitting)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "874debfb-d597-480d-8497-3c704150ff35",
   "metadata": {},
   "outputs": [],
   "source": [
    "for name in dataset_names:\n",
    "    f = load_model(name + \"_linear\")\n",
    "    f = FDTNodeReluVal(f)\n",
    "    x, y = load_robustness_test_points(name)\n",
    "    perturbation, dist, exact, times = minimum_adversarial_perturbation(f, x, tol, n_workers=n_workers, timeout=timeout)\n",
    "    pickle.dump((perturbation, dist, exact, times), open(\"results/map_\" + name + \"_reluval.pkl\", \"wb\"))\n",
    "    print(name)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "9db7140f-0ac5-4262-ad92-ba13e7aa8039",
   "metadata": {},
   "source": [
    "### Display results"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "48588eb9-99f7-4f70-bef7-bddf20432987",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "sigmoid\n",
      "-------\n",
      "shuttle\n",
      "100 within timeout; 100 within tolerance\n",
      "mean 4.65; standard deviation 2.26\n",
      "quartiles:\t1.88\t3.20\t4.09\t5.68\t17.49\n",
      "excluding Z3 fails and timeouts\n",
      "mean 4.43; standard deviation 1.90\n",
      "quartiles:\t1.88\t3.15\t3.91\t5.62\t11.55\n",
      "\n",
      "sylva_agnostic\n",
      "97 within timeout; 97 within tolerance\n",
      "mean 256.76; standard deviation 633.28\n",
      "quartiles:\t6.86\t37.93\t61.27\t154.37\t3600.00\n",
      "excluding Z3 fails and timeouts\n",
      "all Z3 cases failed or timed out\n",
      "\n",
      "wall-robot-navigation\n",
      "100 within timeout; 100 within tolerance\n",
      "mean 12.40; standard deviation 16.48\n",
      "quartiles:\t0.55\t4.28\t8.20\t12.31\t129.75\n",
      "excluding Z3 fails and timeouts\n",
      "mean 7.09; standard deviation 5.54\n",
      "quartiles:\t0.55\t3.20\t5.01\t9.63\t23.10\n",
      "\n",
      "banknote-authentication\n",
      "100 within timeout; 100 within tolerance\n",
      "mean 20.71; standard deviation 21.22\n",
      "quartiles:\t1.26\t8.94\t14.03\t25.34\t154.74\n",
      "excluding Z3 fails and timeouts\n",
      "mean 2.28; standard deviation 1.00\n",
      "quartiles:\t1.26\t1.63\t1.73\t3.12\t3.76\n",
      "\n",
      "helena\n",
      "100 within timeout; 100 within tolerance\n",
      "mean 112.59; standard deviation 92.76\n",
      "quartiles:\t4.90\t66.48\t90.08\t134.73\t834.66\n",
      "excluding Z3 fails and timeouts\n",
      "mean 92.13; standard deviation 52.61\n",
      "quartiles:\t4.90\t56.23\t77.87\t118.58\t239.73\n",
      "\n",
      "MagicTelescope\n",
      "98 within timeout; 98 within tolerance\n",
      "mean 256.34; standard deviation 573.60\n",
      "quartiles:\t1.79\t25.83\t54.30\t221.65\t3600.00\n",
      "excluding Z3 fails and timeouts\n",
      "mean 80.16; standard deviation 155.46\n",
      "quartiles:\t1.79\t2.18\t9.77\t27.18\t426.99\n",
      "\n",
      "satimage\n",
      "96 within timeout; 96 within tolerance\n",
      "mean 224.08; standard deviation 698.48\n",
      "quartiles:\t3.07\t16.36\t31.72\t144.46\t3600.00\n",
      "excluding Z3 fails and timeouts\n",
      "mean 6.97; standard deviation 4.91\n",
      "quartiles:\t3.07\t3.51\t3.95\t8.92\t13.89\n",
      "\n",
      "texture\n",
      "98 within timeout; 98 within tolerance\n",
      "mean 385.24; standard deviation 644.42\n",
      "quartiles:\t3.79\t84.04\t163.96\t361.53\t3600.00\n",
      "excluding Z3 fails and timeouts\n",
      "all Z3 cases failed or timed out\n",
      "\n",
      "JapaneseVowels\n",
      "100 within timeout; 100 within tolerance\n",
      "mean 186.28; standard deviation 461.09\n",
      "quartiles:\t7.18\t18.23\t33.87\t106.38\t2773.63\n",
      "excluding Z3 fails and timeouts\n",
      "mean 21.11; standard deviation 5.87\n",
      "quartiles:\t13.32\t16.54\t21.79\t26.36\t27.55\n",
      "\n",
      "hill-valley\n",
      "98 within timeout; 98 within tolerance\n",
      "mean 175.04; standard deviation 534.02\n",
      "quartiles:\t2.17\t33.27\t46.64\t86.22\t3600.00\n",
      "excluding Z3 fails and timeouts\n",
      "all Z3 cases failed or timed out\n",
      "\n",
      "linear\n",
      "------\n",
      "shuttle\n",
      "100 within timeout; 100 within tolerance\n",
      "mean 4.65; standard deviation 2.10\n",
      "quartiles:\t1.67\t3.22\t4.44\t5.79\t19.31\n",
      "excluding Z3 fails and timeouts\n",
      "mean 4.50; standard deviation 2.17\n",
      "quartiles:\t1.67\t3.12\t4.29\t5.64\t19.31\n",
      "\n",
      "sylva_agnostic\n",
      "98 within timeout; 98 within tolerance\n",
      "mean 321.59; standard deviation 628.47\n",
      "quartiles:\t7.43\t48.58\t102.80\t286.33\t3600.00\n",
      "excluding Z3 fails and timeouts\n",
      "all Z3 cases failed or timed out\n",
      "\n",
      "wall-robot-navigation\n",
      "100 within timeout; 100 within tolerance\n",
      "mean 7.53; standard deviation 11.16\n",
      "quartiles:\t1.27\t2.89\t4.51\t6.97\t75.48\n",
      "excluding Z3 fails and timeouts\n",
      "mean 2.64; standard deviation 0.65\n",
      "quartiles:\t1.27\t2.20\t2.66\t3.21\t3.87\n",
      "\n",
      "banknote-authentication\n",
      "100 within timeout; 100 within tolerance\n",
      "mean 43.02; standard deviation 141.64\n",
      "quartiles:\t1.39\t11.50\t16.05\t21.49\t1069.73\n",
      "excluding Z3 fails and timeouts\n",
      "mean 3.54; standard deviation 2.38\n",
      "quartiles:\t1.39\t1.84\t2.66\t4.15\t8.34\n",
      "\n",
      "helena\n",
      "99 within timeout; 99 within tolerance\n",
      "mean 129.13; standard deviation 354.70\n",
      "quartiles:\t7.32\t55.65\t76.42\t112.28\t3600.00\n",
      "excluding Z3 fails and timeouts\n",
      "mean 56.62; standard deviation 23.88\n",
      "quartiles:\t7.32\t41.43\t62.92\t75.12\t99.43\n",
      "\n",
      "MagicTelescope\n",
      "100 within timeout; 100 within tolerance\n",
      "mean 29.64; standard deviation 69.32\n",
      "quartiles:\t0.21\t3.80\t10.50\t29.41\t558.12\n",
      "excluding Z3 fails and timeouts\n",
      "mean 1.13; standard deviation 0.66\n",
      "quartiles:\t0.21\t0.77\t1.08\t1.32\t2.35\n",
      "\n",
      "satimage\n",
      "100 within timeout; 100 within tolerance\n",
      "mean 146.32; standard deviation 348.29\n",
      "quartiles:\t3.54\t18.27\t48.24\t123.66\t3044.39\n",
      "excluding Z3 fails and timeouts\n",
      "mean 4.57; standard deviation 0.83\n",
      "quartiles:\t3.54\t4.07\t4.59\t5.09\t5.58\n",
      "\n",
      "texture\n",
      "97 within timeout; 97 within tolerance\n",
      "mean 462.93; standard deviation 691.39\n",
      "quartiles:\t8.32\t92.05\t196.27\t524.38\t3600.00\n",
      "excluding Z3 fails and timeouts\n",
      "all Z3 cases failed or timed out\n",
      "\n",
      "JapaneseVowels\n",
      "100 within timeout; 100 within tolerance\n",
      "mean 50.28; standard deviation 66.42\n",
      "quartiles:\t4.39\t14.33\t25.43\t51.86\t448.33\n",
      "excluding Z3 fails and timeouts\n",
      "mean 9.39; standard deviation 4.92\n",
      "quartiles:\t4.39\t6.83\t7.80\t10.36\t17.57\n",
      "\n",
      "hill-valley\n",
      "100 within timeout; 100 within tolerance\n",
      "mean 35.76; standard deviation 89.20\n",
      "quartiles:\t1.31\t8.94\t14.74\t19.44\t650.43\n",
      "excluding Z3 fails and timeouts\n",
      "all Z3 cases failed or timed out\n",
      "\n",
      "z3\n",
      "--\n",
      "shuttle\n",
      "88 within timeout; 88 within tolerance\n",
      "mean 720.82; standard deviation 1106.06\n",
      "quartiles:\t3.36\t79.52\t242.48\t778.13\t3600.00\n",
      "excluding Z3 fails and timeouts\n",
      "mean 328.20; standard deviation 325.00\n",
      "quartiles:\t3.36\t6.95\t174.32\t698.84\t922.64\n",
      "\n",
      "sylva_agnostic\n",
      "0 within timeout; 0 within tolerance\n",
      "mean 3600.00; standard deviation 0.00\n",
      "quartiles:\t3600.00\t3600.00\t3600.00\t3600.00\t3600.00\n",
      "excluding Z3 fails and timeouts\n",
      "all Z3 cases failed or timed out\n",
      "\n",
      "wall-robot-navigation\n",
      "26 within timeout; 26 within tolerance\n",
      "mean 2669.90; standard deviation 1569.42\n",
      "quartiles:\t4.66\t242.70\t3600.00\t3600.00\t3600.00\n",
      "excluding Z3 fails and timeouts\n",
      "mean 22.69; standard deviation 59.18\n",
      "quartiles:\t4.66\t9.16\t10.88\t13.79\t318.20\n",
      "\n",
      "banknote-authentication\n",
      "6 within timeout; 6 within tolerance\n",
      "mean 3416.31; standard deviation 783.26\n",
      "quartiles:\t1.14\t3600.00\t3600.00\t3600.00\t3600.00\n",
      "excluding Z3 fails and timeouts\n",
      "mean 538.42; standard deviation 1189.14\n",
      "quartiles:\t1.14\t1.46\t5.01\t17.54\t3197.38\n",
      "\n",
      "helena\n",
      "48 within timeout; 48 within tolerance\n",
      "mean 2358.17; standard deviation 1325.79\n",
      "quartiles:\t100.35\t1066.45\t3600.00\t3600.00\t3600.00\n",
      "excluding Z3 fails and timeouts\n",
      "mean 1012.86; standard deviation 425.92\n",
      "quartiles:\t100.35\t761.54\t1042.01\t1289.68\t1877.62\n",
      "\n",
      "MagicTelescope\n",
      "6 within timeout; 6 within tolerance\n",
      "mean 3387.86; standard deviation 840.12\n",
      "quartiles:\t1.81\t3600.00\t3600.00\t3600.00\t3600.00\n",
      "excluding Z3 fails and timeouts\n",
      "mean 64.27; standard deviation 109.89\n",
      "quartiles:\t1.81\t2.57\t7.78\t48.23\t305.68\n",
      "\n",
      "satimage\n",
      "3 within timeout; 3 within tolerance\n",
      "mean 3501.48; standard deviation 563.98\n",
      "quartiles:\t43.33\t3600.00\t3600.00\t3600.00\t3600.00\n",
      "excluding Z3 fails and timeouts\n",
      "mean 315.99; standard deviation 375.94\n",
      "quartiles:\t43.33\t50.19\t57.04\t452.31\t847.59\n",
      "\n",
      "texture\n",
      "0 within timeout; 0 within tolerance\n",
      "mean 3600.00; standard deviation 0.00\n",
      "quartiles:\t3600.00\t3600.00\t3600.00\t3600.00\t3600.00\n",
      "excluding Z3 fails and timeouts\n",
      "all Z3 cases failed or timed out\n",
      "\n",
      "JapaneseVowels\n",
      "4 within timeout; 4 within tolerance\n",
      "mean 3463.40; standard deviation 669.46\n",
      "quartiles:\t60.51\t3600.00\t3600.00\t3600.00\t3600.00\n",
      "excluding Z3 fails and timeouts\n",
      "mean 185.03; standard deviation 94.64\n",
      "quartiles:\t60.51\t131.92\t177.94\t231.05\t323.72\n",
      "\n",
      "hill-valley\n",
      "1 within timeout; 0 within tolerance\n",
      "mean 3597.93; standard deviation 20.63\n",
      "quartiles:\t3392.69\t3600.00\t3600.00\t3600.00\t3600.00\n",
      "excluding Z3 fails and timeouts\n",
      "all Z3 cases failed or timed out\n",
      "\n",
      "reluval\n",
      "-------\n",
      "shuttle\n",
      "95 within timeout; 95 within tolerance\n",
      "mean 299.92; standard deviation 848.04\n",
      "quartiles:\t3.35\t15.67\t31.48\t67.86\t3600.00\n",
      "excluding Z3 fails and timeouts\n",
      "mean 331.48; standard deviation 899.31\n",
      "quartiles:\t3.35\t15.18\t26.66\t61.57\t3600.00\n",
      "\n",
      "sylva_agnostic\n",
      "3 within timeout; 3 within tolerance\n",
      "mean 3520.16; standard deviation 457.38\n",
      "quartiles:\t576.01\t3600.00\t3600.00\t3600.00\t3600.00\n",
      "excluding Z3 fails and timeouts\n",
      "all Z3 cases failed or timed out\n",
      "\n",
      "wall-robot-navigation\n",
      "67 within timeout; 67 within tolerance\n",
      "mean 1396.74; standard deviation 1628.62\n",
      "quartiles:\t3.73\t16.82\t315.89\t3600.00\t3600.00\n",
      "excluding Z3 fails and timeouts\n",
      "mean 15.21; standard deviation 11.04\n",
      "quartiles:\t3.73\t7.73\t11.39\t17.77\t47.33\n",
      "\n",
      "banknote-authentication\n",
      "97 within timeout; 97 within tolerance\n",
      "mean 167.43; standard deviation 633.07\n",
      "quartiles:\t3.61\t17.04\t26.17\t42.63\t3600.00\n",
      "excluding Z3 fails and timeouts\n",
      "mean 8.89; standard deviation 5.87\n",
      "quartiles:\t3.61\t4.96\t6.91\t9.60\t21.09\n",
      "\n",
      "helena\n",
      "58 within timeout; 58 within tolerance\n",
      "mean 1997.78; standard deviation 1540.04\n",
      "quartiles:\t10.48\t343.75\t2369.87\t3600.00\t3600.00\n",
      "excluding Z3 fails and timeouts\n",
      "mean 988.37; standard deviation 1134.15\n",
      "quartiles:\t10.48\t122.82\t508.50\t1247.35\t3600.00\n",
      "\n",
      "MagicTelescope\n",
      "57 within timeout; 57 within tolerance\n",
      "mean 1845.36; standard deviation 1656.29\n",
      "quartiles:\t0.97\t47.16\t1836.69\t3600.00\t3600.00\n",
      "excluding Z3 fails and timeouts\n",
      "mean 604.36; standard deviation 1339.69\n",
      "quartiles:\t0.97\t5.28\t6.57\t7.06\t3600.00\n",
      "\n",
      "satimage\n",
      "9 within timeout; 9 within tolerance\n",
      "mean 3307.17; standard deviation 961.12\n",
      "quartiles:\t12.05\t3600.00\t3600.00\t3600.00\t3600.00\n",
      "excluding Z3 fails and timeouts\n",
      "mean 1211.21; standard deviation 1689.13\n",
      "quartiles:\t12.05\t16.82\t21.58\t1810.79\t3600.00\n",
      "\n",
      "texture\n",
      "8 within timeout; 8 within tolerance\n",
      "mean 3352.58; standard deviation 873.55\n",
      "quartiles:\t73.68\t3600.00\t3600.00\t3600.00\t3600.00\n",
      "excluding Z3 fails and timeouts\n",
      "all Z3 cases failed or timed out\n",
      "\n",
      "JapaneseVowels\n",
      "39 within timeout; 39 within tolerance\n",
      "mean 2364.41; standard deviation 1620.51\n",
      "quartiles:\t7.55\t176.80\t3600.00\t3600.00\t3600.00\n",
      "excluding Z3 fails and timeouts\n",
      "mean 137.73; standard deviation 180.28\n",
      "quartiles:\t7.55\t12.11\t48.89\t174.51\t445.60\n",
      "\n",
      "hill-valley\n",
      "1 within timeout; 1 within tolerance\n",
      "mean 3564.18; standard deviation 356.44\n",
      "quartiles:\t17.65\t3600.00\t3600.00\t3600.00\t3600.00\n",
      "excluding Z3 fails and timeouts\n",
      "all Z3 cases failed or timed out\n",
      "\n"
     ]
    },
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAAAvYAAAMqCAYAAADpagXAAAAAOXRFWHRTb2Z0d2FyZQBNYXRwbG90bGliIHZlcnNpb24zLjQuMiwgaHR0cHM6Ly9tYXRwbG90bGliLm9yZy8rg+JYAAAACXBIWXMAAAsTAAALEwEAmpwYAAChnElEQVR4nOzdeXxV1b3///cnAwlBCUPA2MsUGokxQSiEtojgRDWtGHEoXgRbLB2+Umh7b7mduLdKW721Su2treWnV6XKcEEFbtSaUgxCQG5N0CCgEiPI0JrWRAxCDGRYvz9ycpqTk+FkPENez8fjPDxnrbXX+qx9NvGTnbX3NuecAAAAAIS3qGAHAAAAAKDrSOwBAACACEBiDwAAAEQAEnsAAAAgApDYAwAAABGAxB4AAACIADHBDgCh79xzz3VJSUk+ZfHx8RowYICcc/rggw/8tunfv78SEhJUX1+vEydO+NUnJCSof//+qqur04cffuhXP2DAAMXHx6u2tlaVlZV+9eecc47i4uJUU1OjkydPthSz+vXrp7Nnz+qjjz7yqx84cKBiY2N15swZnTp1yq8+MTFRMTExqq6u1unTp/3qBw0apOjoaH388ceqqqryqx88eLCioqJUVVWljz/+2K9+yJAhMjOdPn1a1dXVfvVDhw6VJJ06dUpnzpzxqTMzDRkyRJL00Ucf6ezZsz71UVFRGjx4sCTp5MmTqqmp8amPjo7WoEGDWq2PiYlRYmKiJKmyslK1tbU+9bGxsRo4cKAk6cMPP1RdXV2r9SdOnFB9fb1Pfb9+/XTuuedKkj744AM1v+VuXFyczjnnHElSRUWFmuPY49iTOPY49jj2muLY61vH3rvvvlvunBvmNxGR2CMAaWlpKioqCnYYAAAAfZ6ZHWmtjqU4AAAAQAQgsQcAAAAiAIk9AAAAEAFYY49Oqamp0fHjx1u8CAUIRHx8vEaMGKHY2NigxjFkyJAWLzbrTYMHD27xgjgAADqCxB6dcvz4cZ177rkaM2aMzCzY4SDMOOdUUVGh48ePKyUlJaixnDhxwu8OFYEws05t11pfvWndunW6++679eabbyo9PV3Lli2TJL+yuXPntth27ty5PRZHd/UNAH0RiT06pbq6mqQenWZmGjp0qN5//32fsu5KlNG6devW6dZbb1V+fr4uvfRS7dy5U7fccoskaf369d6yhQsX6uWXX9bzzz+vRx991KdcUpcT8HXr1mnZsmU90jcA9FXG/0jRnqysLNf8dpeNZ9iArmh6HAUrse/suN19xr635p6ZmakDBw74jNf4V5PDhw97y7Zt26bPf/7zeuGFF3TFFVf4lC9ZskT79+/vchwPPvhgj/QNAJHMzPY457JaquPiWYSt48eP6/rrr9cFF1ygT37yk/r2t7/t9+CI7rJ582b95Cc/abW+qKhI3/rWt3pk7Ea5ubn6+c9/3mJd44NN3n//fWVnZ/doHD3JzHr9FSp6a74HDhzwG/vIkSM6evSoT9mll16qM2fO6NJLL/Urf/PNN7s83zfffLPH+gaAvorEHmHJOacbb7xRs2fP1ttvv62SkhKdOnXKu1Y4UM2fHtiaX/ziF1q0aFGr9VlZWfr1r3/dobE7KicnRz/4wQ/abDNs2DCdf/752rVrV4/G0lOcc73+ChW9Nd+MjAy/sUePHq1Ro0b5lO3cuVNxcXHauXOnX3l3/LUuPT29x/oGgL6KxB5hKT8/X/Hx8br99tslNTyy+YEHHtBjjz2mqqoqrVq1SosXL/a2nzVrll566SVJDWe3v/vd72rChAnavXu3fvCDH+iiiy7SxRdfrKVLl/qNVVJSori4OCUlJUmSnnrqKWVmZmrChAmaMWOGJOmll17SrFmzJDWcNf/c5z6njIwMffWrX9Xo0aNVXl6ud999VxdeeKEWLFigcePGad68edq6daumTZumCy64QK+88oqkhseNz549WxdffLE++9nP6vXXX5cknzkdPnxYU6dO1fjx4/Xv//7vPvHOnj1ba9as6a5djQjT+Mvvtm3bVFNTo23btun06dM6ffq0T9nChQv1ta99TQsXLvQr7+gv0K3F0VN9A0BfxcWz6LLvfOc7Ki4u7tY+J06cqF/96let1h84cECTJ0/2KRs4cKBGjRql0tLSNvs+ffq0PvOZz2jFihWqqKjQwoUL9dZbb8nM9OGHH/q137VrlyZNmuT9/JOf/ER//OMf9U//9E8ttl++fLmuvPJK/fCHP1ReXp4effRRb11paameeuopPfbYY5oyZYrWrl2rnTt3Kjc3V/fcc482b96sO++8U5/61Ke0efNm5efn60tf+pLf/v32t7+tO+64Q1/60pf029/+1qcuKyvLL9kHGs2dO1e33nqrlixZ4r3G4b/+678kyafs7rvv1ty5c3XJJZe0WN4dcbQ2JgCgc0js0edER0frpptukiQlJiYqPj5eCxcu1KxZs7xn3Zt67733NGzYMO/nadOmacGCBZozZ45uvPFGv/Y7d+7Upk2bJEnZ2dkaPHiwty4lJUXjx4+XJGVkZOiqq66SmWn8+PF69913vds/88wzkqQrr7xSFRUVOnnypM8Yu3bt8ra57bbb9P3vf99bN3z4cP31r3/t8H4JtlBaFhPpWtvXLSXVc+fO7bFkuyf7BoC+iMQeXdbWmfWectFFF+npp5/2KTt58qSOHj2q1NRUvf7666qvr/fWNX2QVnx8vKKjoyVJMTExeuWVV/Tiiy/q6aef1m9+8xvl5+f79Nu/f39VVlZ6P69cuVJ//vOf9fzzz2vy5Mnas2dPwHHHxcV530dFRXk/R0VFqba2NuB+pNbvfV5dXa3+/ft3qK++rrMX0XbXxbdNf/kDAKCzWGOPsHTVVVepqqpKTzzxhKSGi2C/+93vasGCBUpISNCYMWNUXFys+vp6HTt2zLt+vblTp06psrJSX/jCF/TAAw9o7969fm3S09N9lve88847+sxnPqOf/OQnGjZsmI4dO+bTftq0adqwYYMkacuWLR1+qun06dO9a+RfeuklJSUlaeDAgX5j/M///I8k+a2nLykpUWZmZofG7MuCccFu8xdPnQUAdAcSe4QlM9OmTZv01FNP6YILLtC4ceMUHx+ve+65R1JD4puSkqKLLrpI3/rWt3zWyDf10UcfadasWbr44ot16aWX6pe//KVfmxkzZui1117zLl/4t3/7N40fP16ZmZm65JJLNGHCBJ/2d955p7Zs2aLMzEw99dRTSk5O1rnnnhvw3O666y7t2bNHF198sX7wgx/o97//vV+b//qv/9Jvf/tbjR8/Xn/5y1986rZt26Zrr7024PEAAEBk4AFVaBcPqGq4WPW6667TzJkz22175swZRUdHKyYmRrt379Ydd9zR7RcXt2XGjBn63//937BY3tHXjiMAALqqrQdUscYeCMCPfvQj/fnPfw6o7dGjRzVnzhzV19erX79+euSRR3o4un94//339a//+q9hkdQDAIDuRWIPBOC8885TTk5OQG0vuOACvfbaaz0cUcuGDRum2bNnB2VsAAAQXKyxBwAAACIAiT0AAAAQAUjsAQAAgAhAYg8AAABEAC6eBdCnLV26VFVVVcEOQwkJCbr//vuDHQYAIIyR2CNsHT9+XN/85jf1xhtvqL6+XrNmzdJ9992nfv36dftYmzdv1uuvv64f//jHuuuuu3TOOedo6dKl+vGPf6wZM2YEdH/7zjp79qxmzpyp/Px8xcTwT7a7VVVV6aGHHuqWvhYtWtTpvhYtWtQtMUSCwsJC5eXlqaysTMnJycrOztaUKVOCHRYAhDyW4iAsOed04403avbs2Xr77bdVUlKiU6dOadmyZR3qp66uLqB2v/jFL1pMvH7yk5/0aFJfW1urfv366aqrrtL69et7bJzecuTIkWCH0GeE6y8KhYWFys3N1Zw5c/TrX/9ac+bMUW5urgoLC4MdGgCEPE7/ocueeuopHT9+vFv7HDFihL74xS+2Wp+fn6/4+HjdfvvtkqTo6Gg98MADSklJ0fLly7VhwwYVFRXpN7/5jSRp1qxZWrp0qS6//HKdc845+sY3vqGtW7fqt7/9rZ577jnl5uYqJiZGV199td9yiJKSEsXFxSkpKckvjgULFmjWrFm6+eabNWbMGH35y1/Ws88+q5qaGj311FO68MILdfr0aS1ZskT79+9XTU2N7rrrLl1//fV69913ddttt+n06dOSpN/85je65JJL9NJLL+k//uM/NHjwYL311lsqKSnR7Nmz9cMf/lDz5s3rrl0MhKS8vDzNnz9faWlpkqS0tDTNnz9fGzZs4Kw9ALSDxB5h6cCBA5o8ebJP2cCBAzVq1CiVlpa2ue3p06f1mc98RitWrFBFRYUWLlyot956S2amDz/80K/9rl27NGnSpIDiSkpK0quvvqqHHnpI999/v/77v/9bd999t6688ko99thj+vDDD/XpT39aM2fO1PDhw/WnP/1J8fHxevvttzV37lwVFRVJkl599VXt379fKSkpkqTMzMyIOWPZ9Kx9RUVF2J5Z7gnsC6msrEypqak+ZampqSorKwtSRAAQPkjs0WVtnVkPRdHR0brpppskSYmJiYqPj9fChQs1a9YszZo1y6/9e++9p2HDhgXU94033ihJmjx5sjZu3ChJ2rJli3Jzc71/CaiurtbRo0f1iU98QosXL1ZxcbGio6NVUlLi7efTn/60N6lvjLlfv3766KOPdO6553Zu4iFi9OjR3vfdub69s0Ipme7OfRFK8+qI5ORklZaWes/YS1JpaamSk5ODGBUAhAfW2CMsXXTRRdqzZ49P2cmTJ3X06FGlpqYqJiZG9fX13rrq6mrv+/j4eEVHR0uSYmJi9Morr+jmm2/Wc889p+zsbL+x+vfv77N9W+Li4iQ1JOK1tbWSGq4HeOaZZ1RcXKzi4mIdPXpU6enpeuCBB3Teeedp7969Kioq0tmzZ739DBgwwK/vM2fOKD4+PqA4gHCVnZ2t1atX6+DBg6qrq9PBgwe1evXqFv9tAgB8kdgjLF111VWqqqrSE088IanhItjvfve7WrBggRISEjRmzBgVFxervr5ex44d0yuvvNJiP6dOnVJlZaW+8IUv6IEHHtDevXv92qSnp7e7vKct11xzjR588EE55yRJr732miSpsrJS559/vqKiovTkk0+2eSFvRUWFkpKSFBsb2+k4gHAwZcoU5eTkaMOGDfrWt76lDRs2KCcnh/X1ABAAluIgLJmZNm3apEWLFumnP/2p6uvr9YUvfEH33HOPJGnatGlKSUnRRRddpPT09FbXyH/00Ue6/vrrVV1dLeecfvnLX/q1mTFjhr773e/KOScz63Cs//Ef/6HvfOc7uvjii1VfX6+UlBQ999xzWrRokW666SY98cQTys7ObvEsfaNt27bp2muv7fDYoabpMhz0rGAvceqKKVOmkMgDQCdY41lEoDVZWVmu8aLORm+++abS09ODFFHv+/a3v63rrruuR29t2ZYbb7xRP//5zzVu3LigjN9TQuE4CpW16DygCgAQCDPb45zLaqmOM/YhyMzelZTlnCsPsP0gSbc65x7yfB4j6RLn3FrP58slLXXO+V8ZioD86Ec/0p///OegjH327FnNnj074pL6UBHOZ7YBAGiKNfaRYZCkpqcdx0i6NSiRRKjzzjtPOTk5QRm7X79++tKXvhSUsQEAQPggsQ8yMxtgZs+b2V4z229mt3iqlpjZq2a2z8wu9LS9y8yWNtl2v+fs/M8lfdLMis3sPs/n6Z7P/9LCeI+Z2Stm9pqZXd87MwUAAEBPIrEPvmxJf3XOTXDOZUrK85SXO+cmSfqdpKWtbt3gB5Lecc5NdM79m+dzgefzA83aLpOU75z7tKQrJN1nZq1ftQkAAICwQGIffPskfc7M7jWz6c65Sk/5Rs9/96hhaU13uVrSD8ysWNJLkuIljWreyMy+bmZFZlb0/vvvd+PwAAAA6AlcPBtkzrkSM5sk6QuSfmZmL3qqznj+W6d/fE+18v1lrDNPKzJJNznnDrYT18OSHpYa7orTiXEAAADQizhjH2Rm9glJVc651ZLuk9TyDdcbvNtY7/llIMVT/pGkc5u0a/65qT+qYf2+efr5VKeDD7Lo6GhNnDhRmZmZuu666/Thhx+22f6uu+5q83aCVVVVGjp0qE6ePOlTPnv2bK1fv77V7c4555wWyxcsWKCnn366zZi6y0svvaRZs1q+6dFrr72mhQsXSpJWrVqlxYsXS5JWrlzpfcBXT5o5c6ZOnDjR4+MAANDXkdgH33hJr3iWxtwp6WdttH1G0hAzOyBpsaQSSXLOVUja5bmY9j5Jr0uq81yQ+y/N+vippFhJr3v6+Wm3zqYX9e/fX8XFxdq/f7+GDBmi3/72t13qLyEhQddcc402bdrkLausrNTOnTt13XXXdTXcoLnnnnv0rW99y6/8//2//9ejd9txzqm+vl633XYbt5QEAKAXsBQnyJxzf1TDWfSmxjSpL5J0uef9x2pYI99SP81vb3lls88vNenjG52NtyV5eXkqKyvrzi6VnJys7OzsgNtPnTpVr7/+uiTpnXfe0Te/+U29//77SkhI0COPPKILL7zQp/3ll1+u+++/X1lZWSovL1dWVpbeffddzZ07Vw899JC+/OUvS5I2bdqka665RvX19brqqqt04sQJ1dTU6Gc/+5muv779Gwpt3bpVP//5z3Xy5En98pe/1KxZs/Tuu+/qtttu0+nTpyVJv/nNb3TJJZfovffe0y233KKTJ0+qtrZWv/vd7zR9+nRt2bJFd955p86cOaNPfvKTevzxx3XOOecoLy9P3/nOd5SQkKBLL720xfE/+ugjvf7665owYYJf3V133aVzzjlHS5cu1eWXX67PfOYz2rZtmz788EM9+uijmj59uurq6vSDH/xAL730ks6cOaNvfvOb+sY3vqFTp07p+uuv99sf7777rq655hp95jOf0Z49e/SHP/xBOTk5mj59upYtWxbw9wkAADqOxB5hr66uTi+++KJ3ucnXv/51rVy5UhdccIH+/Oc/a9GiRcrPzw+or2uuuUZf/epXVVFRoaFDh+p//ud/tHjxYsXHx2vTpk0aOHCgysvL9dnPflY5OTnyrGhq1bvvvqtXXnlF77zzjq644gqVlpZq+PDh+tOf/qT4+Hi9/fbbmjt3roqKirR27Vpdc801WrZsmerq6lRVVaXy8nL97Gc/09atWzVgwADde++9+uUvf6nvfe97+trXvqb8/HylpqbqlltuaXH8oqIiZWZmBjT32tpavfLKK/rDH/6g5cuXa+vWrXr00UeVmJiowsJCnTlzRtOmTdPVV1+tkSNHtrg/JOntt9/W73//e332s5/19n3mzBnvPkXfde+996q6ujrYYUSM+Ph4ff/73w92GABCCIk9uqwjZ9a708cff6yJEyfqL3/5i9LT0/W5z31Op06d0ssvv6wvfvGL3nZnzpxpoxdf/fr1U05Ojp5++mnddNNNeu2113TNNdfIOacf/ehH2rFjh6KiovSXv/xFf/vb35ScnNxmf3PmzFFUVJQuuOACjR07Vm+99ZZSUlK0ePFiFRcXKzo6WiUlJZKkKVOm6Ctf+Ypqamo0e/ZsTZw4Udu3b9cbb7yhadOmSWp4Cu3UqVO9/VxwwQWSpPnz5+vhhx/2G/+9997TsGHDApr7jTfeKEmaPHmy3n33XUnSli1b9Prrr3uvFaisrNTbb7+tESNGtLg/JGn06NE+Sb0kDR8+XH/9619J7Pu46upq3XnnncEOo1XLly8P6fiaW758ebBDABBiSOwRthrX2FdVVemaa67Rb3/7Wy1YsECDBg1ScXFxm9vGxMSovr5ekvzOIM6dO1c//elP5ZzT9ddfr9jYWK1atUrvv/++9uzZo9jYWI0ZM8Zvu2XLlun555+XJO/4zc/om5keeOABnXfeedq7d6/q6+sVH99wc6MZM2Zox44dev7557VgwQL967/+qwYPHqzPfe5zWrdunU8/7c2v6T4K9AxpXFycpIaLkmtrayU1rJN/8MEHdc011/i0bWt/DBjg/1iE6upq9e/fP6A4gincEjsgWDrzb2Xfvn0qKChQeXm5kpKSNH36dI0fP77bYups/z0dV0eEUizNhWpsjXG9//77io6OVl1dnYYNG6YxY8bo3Xff7dF4H3jgAZ8bbgwcOFD/8i/NL23sXVw8i7CXkJCgX//611qxYoUSEhKUkpKip556SlJDYrp3716/bcaMGaM9e/ZIkt+day6//HK9/fbb+u1vf6u5c+dKajhTPXz4cMXGxmrbtm06cuSIX5933323iouLfZLup556SvX19XrnnXd06NAhpaWlqbKyUueff76ioqL05JNPqq6uTpJ05MgRnXfeefra176mr371q3r11Vf12c9+Vrt27VJpaakk6fTp0yopKdGFF16od999V++8844k+SX+jdLT073bdsY111yj3/3ud6qpqZEklZSU6PTp0wHtj0bOOZWVlWnMmDGdjgNAeNu3b5/y8/P1+c9/XsuWLdPnP/955efna9++fUHtv6fj6ohQiiVcYmuM68ILL1RiYqKuuuoqDRo0SEOGDNGePXt04YUX9li8jUn9iBEj9J3vfEcjRozQyZMn9cADzZ8L2rtI7BERPvWpT+niiy/WunXrtGbNGj366KOaMGGCMjIy9L//+79+7ZcuXarf/e53+tSnPqXy8nKfuqioKN18882qqKjQZZddJkmaN2+eioqKNH78eD3xxBN+F+O2ZtSoUfr0pz+tz3/+81q5cqXi4+O1aNEi/f73v9eECRP01ltvec9wv/TSS5owYYI+9alPaf369fr2t7+tYcOGadWqVZo7d64uvvhi7zKc+Ph4Pfzww7r22ms1adIkDR8+vMXxL7zwQlVWVuqjjz7qyO70+upXv6qLLrpIkyZNUmZmpr7xjW+otra2Q/tjz549+uxnP6uYGP5ACPRVBQUFysnJUUpKiqKjo5WSkqKcnBwVFBQEtf+ejqsjQimWcImtMa633npL119/vaZOnaqcnByVlpZq5syZeuutt3os3sakfuHChUpMTNTChQu9yX0w8X9ahK1Tp075fH722We97/Py8vza33XXXd73F154ofcuOpL0s5/53mX0V7/6lX71q195PyclJWn37t0BxdFo1apVLZZfcMEFPmPfe++9kqQvf/nL3rvxNHXllVeqsLDQrzw7O1tvvfVWi2M09ZWvfEXr16/XV7/6VS1YsEALFiyQ5Ls/XnrpJe/7pKQk7xr7qKgo3XPPPbrnnnv8+m1tf+zfv9/n85NPPqlFixa1G2eoYN0ywkm4HK/l5eUaNcr3IeejRo3yO7HS2/33dFwdEUqxNBeqsTXG1TS+UaNGqa6uTpMnT9af/vQnb9ueiPfmm2/2+9w0dwgGEnsgwt1xxx3epUnBkJmZqauuuipo43cUa+x7TrgkoeEkWMdrR7/LpKQkHT16VCkpKd6yo0ePKikpqVvi6Wz/PR1XR4RSLM2FamyNcTWN7+jRo4qOjtaePXt84uuJeJ9++mnvHfkaPwcbS3GACBcfH6/bbrstaON/7WtfC9rYAELD9OnTlZubq8OHD6uurk6HDx9Wbm6upk+fHtT+ezqujgilWMIltsa4LrzwQv3v//6vdu/erdzcXKWmpmrr1q268MILeyzegQMH6vjx43r00UdVWVmpRx99VMePH9fAgQO7bYzO4Iw9AHhwth4ITEf/rTTejeSFF17w3qXkyiuv7La7lHS2/56OqyNCKZbmQjW2xvELCgpUWVmpF198UXV1dYqNjdXkyZP11ltvaefOnT0S77/8y7/ogQce0PHjx73Lb0LhrjjmnAtqAAh9WVlZrqioyKfszTffVHp6epAiQqTgOOpbWIrTvXhAFdA3mdke51xWS3WcsQcA9Ar+IgIAPYs19gAAAEAEILFHWNq0aZMmTpzo84qKitILL7ygI0eOaNKkSZo4caIyMjK0cuXKVvu5+eabdejQIUkND61qvBXWJZdc0uNzeO655/TjH/+4x8cBAAB9A4k9wtINN9zgfcprcXGxFi1apOnTp+uaa67R+eefr927d6u4uFh//vOf9fOf/1x//etf/fo4cOCA6urqNHbsWL+6l19+uUfjr62t1bXXXqtnn31WVVVVPToWAADoG1hjjy4rLS1t9SFNnXXOOecoNTU1oLYlJSX6yU9+opdffllRUVHq16+ft+7MmTOqr69vcbs1a9bo+uuvb3X8U6dO6aWXXtJdd92lpKQk7d+/X5MnT9bq1atlZtqzZ4/+9V//VadOnVJSUpJWrVql888/X4888ogefvhhnT17VqmpqXryySeVkJCgBQsWKD4+Xq+99pqmTZumX/7yl7r88sv13HPPac6cOR3fSQAAAE1wxh5hraamRrfeeqtWrFjh81S8Y8eO6eKLL9bIkSP1/e9/X5/4xCf8tt21a5cmT57c7hivvfaafvWrX+mNN97QoUOHtGvXLtXU1GjJkiV6+umntWfPHn3lK1/RsmXLJEk33nijCgsLtXfvXqWnp+vRRx/19nX8+HG9/PLL+uUvfylJysrKCvojuQEAQGTgjD26LNAz6z3hP/7jP5SRkaFbbrnFp3zkyJF6/fXX9de//lWzZ8/WzTffrPPOO8+nzXvvvadhw4a1O8anP/1pjRgxQpI0ceJEvfvuuxo0aJD279+vz33uc5Kkuro6nX/++ZKk/fv369///d/14Ycf6tSpU7rmmmu8fX3xi19UdHS09/Pw4cNbXCYEAADQUST2CFsvvfSSnnnmGb366quttvnEJz6hzMxMFRQU6Oabb/ap69+/v6qrq9sdJy4uzvs+OjpatbW1cs4pIyNDu3fv9mu/YMECbd68WRMmTNCqVav00ksveesGDBjg07a6ulr9+/dvNwYAAID2sBQHYenEiRO6/fbb9cQTT+jcc8/1qTt+/Lg+/vhjb7udO3cqLS3Nr4/09HSVlpZ2avy0tDS9//773sS+pqZGBw4ckCR99NFHOv/881VTU6M1a9a02U9JSYkyMzM7FQMAAEBTnLFHWFq5cqX+/ve/64477vAp/+EPf6ghQ4bou9/9rsxMzjktXbq0xcdIX3vttXrppZc0c+bMDo/fr18/Pf300/rWt76lyspK1dbW6jvf+Y4yMjL005/+VJ/5zGc0bNgwfeYzn9FHH33Uaj/btm3Tf/7nf3Z4fAAIxK5du1RbWxvsMBACYmJiNG3atGCHgR5mzrlgx4AQl5WV5YqKinzK3nzzTaWnpwcpou7x8ccf64orrtCuXbt81r33lr/97W+69dZb9eKLL/b62KEiEo4jIJRt375dl112WbDDCJq+Pv+m2BeRw8z2OOeyWqrjjD36rP79+2v58uX6y1/+4nNHnd5y9OhRrVixotfHRev4Hx+AvoyfgR2zfft2v7Jg7z/W2KNPu+aaa4KS1EvSlClTNHHixKCMDQAAOq9pUt90uW9LyX5vIrFHp7GMC13B8QMACHeXXXaZhgwZEvQz9Y1YioNOiY+PV0VFhYYOHSozC3Y4CDPOOVVUVCg+Pj7YofgJ9tkWAOgp/HzrXs1vzDF+/Hjt27cvSNE0ILFHp4wYMULHjx/X+++/H+xQEKbi4+O9D/4KJaFy1gXoDiRyaKq9n28cLx2zb98+n30a7KReIrFHJ8XGxiolJSXYYQAAAATN9u3bQ+JMfSPW2AOAB2frAfRl/AwMXGtn6oO9DzljDwBABOvryyv6+vwbxcSQ8nW3YCfxLeFbBgAgQoVi4gGg57AUBwAAAIgAJPYAAABABGApDtpVUVGhVatW+ZRlZGRoypQpqqmp0Zo1a/y2mThxoiZOnKiqqipt2LDBrz4rK0uZmZmqrKzUpk2b/OqnTp2qtLQ0lZeX67nnnvOrnzFjhsaOHauysjLl5eX51V911VUaOXKkjh07phdffNGvPjs7W8nJyTp06JB27NjhVz9r1iwlJSXp4MGD2r17t1/9DTfcoMTERO3fv19FRUV+9XPmzFFCQoKKi4tVXFzsVz9v3jzFxsaqsLBQBw4c8KtfsGCBJOnll19WSUmJT11sbKzmzZsnqWHt6OHDh33qExISNGfOHEnS1q1bdfz4cZ/6gQMH6sYbb5Qk5eXlqayszKd+6NChuu666yRJzz77rCoqKnzqk5OTlZ2dLUnauHGjTp486VM/YsQIzZw5U5K0YcMGVVVV+dSnpKR4lwesWbNGNTU1PvXjxo3TJZdcIkl+x53Escexx7HHscex1xzHXt899prjjD0AAAAQAYzHuqM9WVlZrqXfkAEAANC7zGyPcy6rpTrO2AMAAAARgMQeAAAAiAAk9gAAAEAE4K44AAB00JAhQ3TixIlghxG2Bg8erA8++CDYYQARh8QeAIAOOnHihHrr5hNm1mtj9RYzC3YIQERiKQ4AhBESIqDrOvLvaN26dcrMzFRUVJRiY2NlZjIzjRw5UkuWLNHIkSN9ytatW+ezTXx8vKKiopSZmal169b59BkdHe1T3hEd7aMj7dtqu2TJEsXHx8vMFBUVJTPr9BzC3TXXXOPdB1FRUbrmmmuCHZLknOPFq83X5MmTHYDQ0PBjG8HWm99DJH7nwZ5ToOOvXbvWpaSkuGXLlrmkpCQ3ZMgQl5yc7H74wx+6xMREZ2Zu0KBBbsuWLW7Lli0uOTnZDRw40A0bNswtW7bMjRkzxq1YscLbR0pKilu8eLFLSUlx+fn57uzZsy4/P9+lpKS4tWvXBhx/Y1yB9tGR9m21Xbx4sYuJiXHz5s1zY8aMcXfccYeLiYlxs2fP7vAcwt3VV1/tJLk77rjDffjhh+6OO+5wktzVV1/d42NLKnKt5GxBTxp5hf6LxB4IHcFOiNCAxL5rgj2nQMfPyMhw+fn5LiMjw40ZM8bl5+f7fI6OjnZjxozxts/Pz3exsbFuzJgx3m0byxs/x8XFecubbpeRkRFw/E37DqSPjrRvq21cXJxbsWKFT5sVK1Z459SROYQ7M3N33HGHT9kdd9zhzKzHx24rsecBVWgXD6gCQgdLcUJHb/3/kzX2PSOQfRodHa3q6mrFx8dLkqqrqyVJ8fHx3kQqKipKdXV1kqSamhr169dPUVFR3vaxsbGqqalRfHy8qqur1a9fP509e1axsbHecRrrG/sJNK5A++hI+7ba1tfX6/Tp0zr33HO9baqqqjRgwACdPXu2Q3MId2amDz/8UImJid6yyspKDRo0qMf/vfKAKgCIIK2dqeHVey90XTh8f+np6dq5c6fS09M1atQo7dy50/t59OjRio6O1qhRo7ztd+7cqdjYWI0aNcq7bWN54+e4uDhvedPt0tPTOxxXoH10pH1bbePi4rRy5UqfNitXrvTOqSNzCHdmph/+8Ic+ZT/84Q+D/0trsH848gr9F0txgNChCFyWEY5683uIxO882HMKdHzW2LPGvjWssecVti8SewDwRWLfNeE0p7Vr17qMjAxnZi4mJsZJcpLciBEj3OLFi92IESN8ytauXeuzTVxcnDMzl5GR4U18G+ujoqJ8yjsTV6B9dKR9W20XL17s4uLinCRnZk5Sp+cQ7q6++mrvPjCzXknqnXOssUfXsMYeAHwF/c/tYY4HVAGd19Yaex5QBQBAB3FSDEAo4uJZAAAAIAKQ2AMAAAARgMQeAAAAiAAk9gAAAEAEILEHAAAAIgCJPQAAABABSOwBAACACEBiDwAAAEQAHlAFAEAvWbp0qaqqqoIdBppISEjQ/fffH+wwgG5BYg8AQC+pqqrSQw89FOwwArJo0aKwibUrFi1aFOwQgG5DYg8AYayvJF9AXxIK/64LCwuVl5ensrIyJScnKzs7W5K8ZYmJiZKkyspKn/eNbadMmdJqP411wZhD87G7Et/69eu1a9cu1dbWKiYmRtOmTdMtt9zSE1MJGIk9AAAAvAoLC5Wbm6v58+crNTVVpaWlevTRRyVJCxcu1IcffqhNmzZJki699FLt3btXkvSlL31JgwYN0urVq719Ne+nsa6nk/uW5tB87EDatGb9+vUqKCjQ7NmzNWPGDO3YsUObN2+WpKAm91w8CwAAAK+8vDzNnz9faWlpio6OVlpamuLi4tSvXz+lpaVpy5Ytuv3223X77bdr9+7d3vdbtmxRWlqa5s+fr7y8vBb7aawLxhyaj92V+Hbt2qXZs2dr5syZ6tevn2bOnKnZs2dr165dPTmtdnHGHgDCHGuEga7h35CvsrIypaam+pR98MEHcs751dfW1nrfl5WVSZJSU1N93jfVtK4ntTSH5mMH0qY1tbW1mjFjhk/ZjBkztHHjxi5E3XUk9gAQ5oK9FheBI4EMTaH2byjYx0lycrJKS0uVlpbmLRsyZIg3sW+sl6SYmBjv++TkZElSaWmpz/um/TSt6+05NB87kDatiYmJ0Y4dOzRz5kxv2Y4dOxQTE9zUmqU4AAAA8MrOztbq1at18OBB1dXV6eDBgzpz5ozOnj2rgwcP6uqrr9bjjz+uxx9/XFOnTvW+v/rqq3Xw4EGtXr1a2dnZLfbTWBeMOTQfuyvxTZs2TZs3b9bWrVt19uxZbd26VZs3b9a0adN6clrt4ow9AISxUDvTCKDrgv3vuvHC0Q0bNnjvFvPFL37Rp6zxTjg7d+70vn/iiSeUnJysnJwcn4tPm/bTvK4359B87EDatKbxAtnc3Fxt3LhRMTExmj59etDvimONf1YBWpOVleWKioqCHQYAhL1gL7GAPx5QhXBjZnucc1kt1XHGHgCAXhLsM7EAIhtr7FtgZu+aWVKw4+gqM/tRs88vBysWAAAA9CwS+8jmk9g75y4JViAAAADoWX0msTezAWb2vJntNbP9ZnaLmW1uUv85M9vUbJufm9k3m3y+y8yWmtk5Zvaimb1qZvvM7Pp2xt5sZnvM7ICZfb1J+UIzKzGzV8zsETP7jad8lZn92sxeNrNDZnazp9zM7D5P/PvM7BZP+flmtsPMij11083s55L6e8rWeNqdajL29z197PW0BQAAQBjrS2vssyX91Tl3rSSZWaKk5WY2zDn3vqTbJT3WbJv1kn4l6beez3MkXSOpWtINzrmTniU7/2dmua71K5G/4pz7wMz6Syo0s2ckxUn6D0mTJH0kKV/S3ibbnC/pUkkXSsqV9LSkGyVNlDRBUpKnrx2SbpX0R+fc3WYWLSnBOVdgZoudcxObB2Nmn5d0vaTPOOeqzGxIC22+LunrkjRq1KhWpgUAAIBQ0WfO2EvaJ+lzZnavmU13zlVKelLSfDMbJGmqpBeabuCce03ScDP7hJlNkHTCOXdMkkm6x8xel7RV0j9JOq+Nsb9lZnsl/Z+kkZIukPRpSdudcx8452okPdVsm83OuXrn3BtN+r5U0jrnXJ1z7m+StkuaIqlQ0u1mdpek8c65j9rZFzMlPe6cq/LM84PmDZxzDzvnspxzWcOGDWunOwAAAARbnzlj75wrMbNJkr4g6Wdm9qKk/5b0rBrOwD/lnKttYdOnJN0sKVkNZ/AlaZ6kYZImO+dqzOxdSfEtjWtml6shkZ7qOTv+UmttmznTtJt25rbDzGZIulbSKjP7pXPuiQDGAAAAQIToM2fszewTkqqcc6sl3SdpknPur5L+KunfJT3eyqbrJf2zGpL7xrPqiZL+7knqr5A0uo2hE9Vwpr/KzC6U9FlPeaGky8xssJnFSLopgGkUSLrFzKLNbJikGZJeMbPRkv7mnHtEDb+sTPK0rzGz2Bb6+ZMazvAnSFJLS3EAAAAQXvrMGXtJ4yXdZ2b1kmok3eEpXyNpmHPuzZY2cs4dMLNzJf3FOfdek22eNbN9kookvdXGuHmS/p+ZvSnpoBqW48g59xczu0fSK5I+8PRR2c4cNqlhydBeSU7S95xzZWb2ZUn/ZmY1kk5J+pKn/cOSXjezV51z85rMKc/MJkoqMrOzkv6gZnfQAQAAQHjp80+e9dyJ5jXn3KNBGPsc59wpzxn7TZIec85tam+73saTZwEAAFq2fPly3Xnnnb02XltPnu0zS3FaYmZ7JF0saXWQQrjLzIol7Zd0WNLmIMUBAACAMNeXluL4cc5N7q6+zGyopBdbqLrKOVfRyvhLu2t8AAAQOfbt26eCggKVl5crKSlJ06dP1/jx48NqjN6YA3z16cS+O3mS94nBjgMAAIS3ffv2KT8/Xzk5ORo1apSOHj2q3NxcSeq2xLinx+iNOcBfn16KAwAAEGoKCgqUk5OjlJQURUdHKyUlRTk5OSooKAibMXpjDvBHYg8AABBCysvL/Z76PmrUKJWXl4fNGL0xB/gjsQcAAAghSUlJOnr0qE/Z0aNHlZSUFDZj9MYc4I/EHgAAIIRMnz5dubm5Onz4sOrq6nT48GHl5uZq+vTpYTNGb8wB/rh4FgAAIIQ0Xlz6wgsveO8oc+WVV3brRac9PUZvzAH+SOwBAABCzPjx43s8Ce7pMXpjDvDFUhwAAACgk3rzqbPtIbEHAAAAIgCJPQAAABABSOwBAACACEBiDwAAAEQAEnsAAAAgApDYAwAAABGAxB4AAACIACT2AAAAQAQgsQcAAAA6afv27cEOwYvEHgAAAIgAJPYAAABABCCxBwAAACIAiT0AAAAQAUjsAQAAgAhAYg8AAABEABJ7AAAAIAKQ2AMAAAARgMQeAAAAiAAk9gAAAEAnXXbZZcEOwYvEHgAAAIgAJPYAAABABIgJdgAIfRUVFVq1apVPWUZGhqZMmaKamhqtWbPGb5uJEydq4sSJqqqq0oYNG/zqs7KylJmZqcrKSm3atMmvfurUqUpLS1N5ebmee+45v/oZM2Zo7NixKisrU15enl/9VVddpZEjR+rYsWN68cUX/eqzs7OVnJysQ4cOaceOHX71s2bNUlJSkg4ePKjdu3f71d9www1KTEzU/v37VVRU5Fc/Z84cJSQkqLi4WMXFxX718+bNU2xsrAoLC3XgwAG/+gULFkiSXn75ZZWUlPjUxcbGat68eZKk7du36/Dhwz71CQkJmjNnjiRp69atOn78uE/9wIEDdeONN0qS8vLyVFZW5lM/dOhQXXfddZKkZ599VhUVFT71ycnJys7OliRt3LhRJ0+e9KkfMWKEZs6cKUnasGGDqqqqfOpTUlK8f7Zcs2aNampqfOrHjRunSy65RJL8jjuJY49jj2OPY49jrzmOvb577DXHGXsAAAAgAphzLtgxIMRlZWW5ln5DBgAAQO8ysz3OuayW6jhjDwAAAEQAEnsAAAAgApDYAwAAABGAu+IAQBcNGTJEJ06cCHYYvWbw4MH64IMPgh0GAKAZEnsA6KITJ04o1G5EYGY9FpOZ9Ui/AICuYSkO0MtIioCeY2bKzMxUdHS0MjMztW7dOm/dkiVLFB8fLzNTVFSUoqKivG3WrVvns92SJUs0cuRImZnMTCNHjtSSJUta7bsnNI+pvfE62r47BXNsAE0453jxavM1efJkh+7T8M8OkSQUv9OejCkU5+ucc2vXrnWSXH5+vjt79qzLz893KSkpbu3atW7x4sUuJibGzZs3z40ZM8bdcccdLjo62s2ePdsNGzbMDRs2zLvdsmXLXFRUlEtMTHRbtmxxW7ZscYMGDXJRUVFu2bJlfn331FxSUlJanEt3tA9mrAC6RlKRayVnC3rSyCv0XyT23StUkyJ0Xih+p30xsc/IyPCLLT8/32VkZLi4uDi3YsUKl5GR4fLz851zzq1YscLFxcW5MWPGuDFjxvj0c9555/mUjRkzxiUnJ7uMjAy/vntqLo1xBjJeR9t3p2CODfRFbSX2PKAK7eIBVd2LpTiRKdR+lvblNfZN511TU6P4+HjV19fr9OnTOvfcc1VdXa3Y2FhVVVVpwIAB3uU2dXV1kqTo6GjV19crKirKWxYVFeWdd2NZY9+Nn7tTdHS0N87mc2lpvI62D2asALqGB1QBIaa137R5heerLwr2Pm/plZGR4Rfnzp07lZ6erri4OK1cuVLp6enauXOnJGnlypWKi4vT6NGjNWrUKO826enpOu+883zKRo8ereHDhys9Pd2v757QNM5Axuto++4UzLEBNBPsH8S8Qv/FUpzupRBdxoDOC8XvtCdjCsX5Oscae9bYA32DWGPPqysvEnugbaGY6PbFxN65hiQzIyPDRUVFuYyMDJ/kcvHixS4uLs5JcmbmzMzbpvl2ixcvdiNGjHCSnCQ3YsQIt3jx4lb77u25dEf77hTMsYG+pq3EnjX2aBdr7IG2hfqa8+7GA6oAIHjaWmPPA6oAoIs4QQIACAVcPAsAAABEABJ7AAAAIAKQ2AMAAAARgMQeAAAAiAAk9gAAAEAEILEHAAAAIgCJPQAAABABSOwBAACACMADqgD0CUuXLlVVVVWww+gWCQkJuv/++4MdBgAgxJDYA+gTqqqq9NBDD/X4OIsWLerxcRYtWtSj/QMAwhOJPYCA9UbSitDX0nFQWFiovLw8lZWVKTk5WdnZ2ZoyZUq7fbW2XfPycePGqaSkRO+9955iYmJUV1fXoXG6S2fnGWi/XZlfT8UGIHyQ2AMAuqSwsFC5ubmaP3++UlNTVVpaqtWrV0tSm4lla9sdOnRI+/fv95Y///zz2rJlizIzM3X27FlddtlleumllzRhwgTl5ua2O06w5xlov1OmTOn0/HoqNgDhhYtnAQBdkpeXp/nz5ystLU3R0dFKS0vT/PnzlZeX16ntdu3a5VO+d+9ezZ49W2+88Ybmz5+vmTNn6rbbbtPevXsDGifY8wy038b5dGZ+PRUbgPDCGXsAHcL67tAQSt9DWVmZUlNTfcpSU1NVVlbWqe1qa2t9ysvKyjRjxgxt3LjRW97YfyDjdJfOzjPQfpv239H59VRsAMILiT2ADgnXNfahlAh3h2B+D833ZXJyskpLS5WWluYtKy0tVXJycpv9tLZdTEyMT3lycrJ27NjhU97YfyDjdJfOzjPQfpv239H59VRsAMILS3EAAF2SnZ2t1atX6+DBg6qrq9PBgwe1evVqZWdnd2q7adOm+ZRPmDBBmzdv1kUXXaTVq1dr69atevLJJzVhwoSAxgn2PAPtt3E+nZlfT8UGILxwxh5AwML1bD26V/PjoPHizA0bNnjvyJKTk9PuRZttbTd27Fif8unTp6ukpEQVFRXKzc1VXV2d9u7dG9A43aWz8wy037y8vE7Pr6diAxBezDkX7BgQ4rKyslxRUVGwwwC6JJKW4vCAKgDou8xsj3Muq6W6kD5jb2YvSVrqnCsys3clZTnnyjvZ1ypJzznnng6w/URJn3DO/aEz43UgrhxJFznnft6JbQdJutU595Dn8yck/do5d3P3RgmEP/7aAACIdBG1xt7MuvMXlYmSvtCN/bXIOZfbmaTeY5Ak72lI59xfSeoBAAD6pl5J7M3s38zsW573D5hZvuf9lWa2xsx+Z2ZFZnbAzJZ3sO+7zOxJM9sl6UkzG2Nm+Wb2upm9aGajmjSf6RmnxMxmebaPN7PHzWyfmb1mZleYWT9JP5F0i5kVm9ktLYz7rpktN7NXPdte6Cn/tJnt9vT1spmlecr/z8wymmz/kpllmdkCM/uNp+yTnnb7zOxnZnbKU36OZy6NY13v6ebnkj7pifE+z9z3tzYvT/kCM9toZnlm9raZ/aIj+xsAAAChqbfO2BdImu55nyXpHDOL9ZTtkLTMs1boYkmXmdnFHez/IkkznXNzJT0o6ffOuYslrZH06ybtxkj6tKRrJa00s3hJ35TknHPjJc2V9Hs17JcfS1rvnJvonFvfyrjlzrlJkn4naamn7C1J051zn/L0cY+nfL2kOZJkZudLOt8513zh+n9J+i9PLMeblFdLusEz1hWSVpiZSfqBpHc8Mf5bs7785uWZr9Tw14hbJI1Xwy8vI1uZHwAAAMJEbyX2eyRNNrOBks5I2q2GBH+6GpL+OWb2qqTXJGWoIVHviFzn3Mee91MlrfW8f1LSpU3abXDO1Tvn3pZ0SNKFnvrVkuSce0vSEUnjAhx3Y5P5jfG8T5T0lOfM+QOe+UjSBkmNy2TmSGpprf9USU953q9tUm6S7jGz1yVtlfRPks5rJ7a25vWic67SOVct6Q1Jo5tvbGZf9/x1o+j9999vZygAAAAEW68k9s65GkmHJS2Q9LIakvkrJKVK+lgNZ7uv8pxlf15SfMs9SWb2Tc/Sk2LPxaKSdDrQUNr53Coz+6NnzP9uUnzG8986/eNC5J9K2uacy5R0nTxzcc79RVKF568Rt6jhDH6g5kkaJmmyc26ipL+pjX0UgDNN3jeN3cs597BzLss5lzVs2LAuDAUAAIDe0JsXzxaoIYHf4Xn//9Rwhn6gGhLzSjM7T9Ln2+rEOfdbz9KTic65v7bQ5GVJ/+x5P88zVqMvmlmUmX1S0lhJBz318yTJzMZJGuUp/0jSuU3GvcYz5lfbmWeipL943i9oVrde0vckJTrnXm9h2/+TdJPn/T83KU+U9HfnXI1nrXzjGXafGJtpbV4AAACIQL2d2J8vabdz7m9qWDde4Jzbq4YE/y01LD/Z1cVxlki63bNs5TZJ325Sd1TSK5JekPT/PEtRHpIUZWb71JB4L3DOnZG0TdJFrV0824ZfSPpPM3tN/mfCn1ZDwr6hlW2/I+lfPbGnSqr0lK+RlOWJ8Utq2FdyzlVI2mVm+83svmZ9tTYvAAAARCAeUBVCzCxB0sfOOWdm/yxprnPu+va262k8oAoAACA0hO0DqvqgyZJ+47njzYeSvhLccACg59x7772qrq4OdhgA0CXx8fH6/ve/H+wwJJHYhxTnXIGkCcGOAwB6Q3V1te68885ghwG0aPny5RyfCMjy5R16BFOPiqgnzwJATwilH9oAALSGxB4AAACIACT2AAAAQARgjT0ABIDlOACAUEdiDwAB4CK67scvSwDQvViKAwAAAEQAEnsAaAdn6wEA4YClOACAoGE5DkIZxycCER8fH+wQvEjsAQBBwV9CAKB7sRQHAAAAiAAk9gAAAEAEILEHAAAAIgCJPQAAABABSOwBAACACEBiDwAAAEQAEnsAAAAgApDYAwAAABGAB1QBAICItGvXLtXW1gY7DPQBl112WbBDkERiDwAAIlRtbW3IJFyIXNu3bw92CF4sxQGAHhBKP+gBAH0DiT0AAAAQAUjsAQAAgAjAGnsA6CEsxwEA9CYSewDoIVy0BwQXv1yjr2EpDgAAABABSOwBoAdwth4A0NtI7AEAAIAIwBp7AAAQsVhnj76ExB4AAEQklsShr2EpDgAAABABOGOPdlVUVGjVqlU+ZRkZGZoyZYpqamq0Zs0av20mTpyoiRMnqqqqShs2bPCrz8rKUmZmpiorK7Vp0ya/+qlTpyotLU3l5eV67rnn/OpnzJihsWPHqqysTHl5eX71V111lUaOHKljx47pxRdf9KvPzs5WcnKyDh06pB07dvjVz5o1S0lJSTp48KB2797tV3/DDTcoMTFR+/fvV1FRkV/9nDlzlJCQoOLiYhUXF/vVz5s3T7GxsSosLNSBAwf86hcsWCBJevnll1VSUuJTFxsbq3nz5klq+BPz4cOHfeoTEhI0Z84cSdLWrVt1/Phxn/qBAwfqxhtvlCTl5eWprKzMp37o0KG67rrrJEnPPvusKioqfOqTk5OVnZ0tSdq4caNOnjzpUz9ixAjNnDlTkrRhwwZVVVX51KekpHjPoq1Zs0Y1NTU+9ePGjdMll1wiSX7HncSxx7HHscexx7HXHMde3z32muOMPQAAABABzDkX7BgQ4rKyslxLvyEDAACgd5nZHudcVkt1nLEHAAAAIgCJPQAAABABSOwBAACACMBdcQCgjxgyZIhOnDgR7DB6zeDBg/XBBx8EOwwA6DUk9gDQR5w4cUK9ccMEM+uVcQKJAwD6EpbiAAgYiRLQdWamzMxMRUdHKzMzU+vWrfOpX7JkieLj42Vmio+P15IlSyRJ69ata3O7lgSyTWf67azeHAvok5xzvHi1+Zo8ebIDnHOu4UcGwlVvfX+hcpyEShxNrV271kly+fn57uzZsy4/P9+lpKS4tWvXOuecW7x4sYuJiXErVqxwp0+fditWrHAxMTHu6quvdikpKa1u19pY7W0TSJvunHtvjQVEMklFrpWcLehJI6/Qf5HYo1EoJkoIHIl98GVkZPjFlZ+f7zIyMpxzzsXFxbkVK1b41K9YscKZmcvPz291u9bGam+bQNp0l94cC4hkbSX2PKAK7eIBVWjEUpzw1xs/81lj376m+6empkbx8fGqq6uTmen06dNKSEjw1ldVVWnAgAE6e/asYmNjW9yuJdHR0aqurm5zm0DadJfeHAuIZDygCkC3ae0sAa/Qf/VFwd7nzV8ZGRl+Me7cuVPp6emSpLi4OK1cudKnfuXKlTIz7dy5s9XtWpKent7uNoG06S69ORbQZwX7hxyv0H+xFAeNFIJLGxC43vr+QuU4CZU4mmKNPWvsga4Sa+x5deVFYg9EBhL70LB27VqXkZHhoqKiXEZGhl9iu3jxYhcXF+ckubi4OLd48eKAtuvMWJ3tt7N6cywgUrWV2LPGHu1ijT0QGXpr7XsorbEPhTgAoDu1tcaeB1QBQB/SWxeUhsKFq4MHDw52CADQq0jsAaCP4Ow1AEQ27ooDAAAARAASewAAACACkNgDAAAAEYDEHgAAAIgAJPYAAABABCCxBwAAACIAiT0AAAAQAbiPPQCgTUuXLlVVVVWww/BKSEjQ/fffH+wwACDkkNgDANpUVVWlhx56qFv6WrRoUZf7WrRoUbfEAgCRhsQeQJd0R6IGhIOmx/r69eu1a9cu1dbWKioqSvHx8fr444+VnJys7OxsTZkyxW/7wsJC5eXlqaysrM12CB29+Z311Fjd1S/Hb3ggsQcAoAPWr1+vgoICzZ49WwMGDNAzzzyjjz/+WJdeeqkmTZqk1atXS5JP0lNYWKjc3FzNnz9fqampKi0tbbEdQkdvfmc9NVZ39cvxGz64eBYAgA7YtWuXZs+erZkzZ2rr1q362te+phtuuEG7d+9WWlqa5s+fr7y8PJ9t8vLyNH/+fKWlpSk6OrrVdggdvfmd9dRY3dUvx2/44Iw9gC5jzTN6WzCPudraWs2YMUOSVFZWptTUVKWkpGjjxo2SpNTUVJWVlfls09iuqZbaIXT05nfWU2N1V78cv+GDxB5Al7HGPrKF4i9uwTjmGvdDTEyMduzYoZkzZyo5OVmlpaU6duyYYmIa/pdaWlqq5ORkn20b26WlpXnLWmqH0NGb31lPjdVd/XL8hg+W4gAA0AHTpk3T5s2btXXrVs2cOVOPPPKINm3apKlTp+rgwYNavXq1srOzfbbJzs7W6tWrdfDgQdXV1bXaDqGjN7+znhqru/rl+A0fnLEH0CWcrUdf0Xis33LLLZKk3Nxc711x+vfvr507d6q0tFQ5OTl+FxQ2ft6wYYP3riIttUPo6M3vrKfG6q5+OX7DB4k9AAAddMstt3gT/EBNmTKFRCjM9OZ31lNjdVe/HL/hgcQeANCu7lxn39W+EhISuikSAIgs7Sb2ZjZG0nPOucyuDGRmCyRlOecWd7GfMZIucc6t7Uo/AYwzSNKtzrmHPJ8vl7TUOTerG/qeKOkTzrk/eD7nSLrIOffzTvT1I+fcPU0+v+ycu6SrMQJAI5ZbAUB4CMeLZ8dIurUXxhkkqaduBTFR0hcaPzjncjuT1Hv8qOkHknoAAIC+KdDEPsbM1pjZm2b2tJklmNmPzazQzPab2cNmZpJkZi+Z2b1m9oqZlZjZ9Oadmdm1ZrbbzJLMbJWZ/drMXjazQ2Z2s6eNmdl9nv73mVnjYsafS5puZsVm9i9mFu1pV2hmr5vZN1qagJldZ2Z/NrPXzGyrmZ3nKb/LzJY2abff81eBn0v6pGec+zzV53jm/5ZnfzTOebKZbTezPWb2RzM7v7V9YWb9JP1E0i2evm8xswVm9hvPNueZ2SYz2+t5XeIp3+zp/4CZfd1T9nNJ/T39rPGUnWpr/5nZ5Z64/OYBAACA8BVoYp8m6SHnXLqkk2o4k/0b59wUzxKd/pKaLlGJcc59WtJ3JN3ZtCMzu0HSDyR9wTlX7ik+X9Klnj4az1zfqIYz2xMkzZR0nydh/oGkAufcROfcA5IWSqp0zk2RNEXS18wspYU57JT0WefcpyT9j6TvtTPnH0h6xzPOv3nKPuWZ00WSxkqaZmaxkh6UdLNzbrKkxyTd3dq+cM6dlfRjSes9fa9vNu6vJW13zk2QNEnSAU/5Vzz9Z0n6lpkNdc79QNLHnn7mNeuntf3X4jyaT97Mvm5mRWZW9P7777ezqwAAABBsgV48e8w5t8vzfrWkb0k6bGbfk5QgaYgaEtBnPW02ev67Rw1LZxpdqYbE9Grn3Mkm5Zudc/WS3mg8k66GRH+dc65O0t/MbLsaEvem20nS1ZIubjzTLylR0gWSDjdrN0LSek9y26+F+kC84pw7LklmVuyZ24eSMiX9yXPiO1rSe022aW1ftOZKSV+SJM/cKz3l3/L8UiRJI9Uwx4o2+mlr/7U0j51NN3bOPSzpYUnKyspyAcQNAACAIAo0sW+e2DlJD6nhYthjZnaXpPgm9Wc8/61rNsY7ajhDPE5SUQvtJamjy0JM0hLn3B99Cs3ulnStJDnnJqrhrPovnXO5ngth7/I0rZXvXy6azqO5pnE2zs0kHXDOTW1nm+b7ImCeeGdKmuqcqzKzl9qJsz0tzQMAAABhLNClOKPMrDFxvVX/OLtbbmbnSLq55c38HJF0k6QnzCyjnbYFaliHHm1mwyTNkPSKpI8knduk3R8l3eFZEiMzG2dmA5xzyzxLVCZ62iVK+ovn/ZebbP+uGpa8yMwmSWpcxtN8nNYclDSscf+YWWwAc2ur7xcl3eHpK9rMEj2xn/Ak9RdK+myT9jWNc2+mtf0HAACACBRoYn9Q0jfN7E1JgyX9TtIjkvarIbEuDHRA59xbkuZJesrMPtlG002SXpe0V1K+pO8558o8ZXWeC0v/RdJ/S3pD0qtmtl/S/6eWz0Df5Rlzj6TyJuXPSBpiZgckLZZU4omzQtIuz8Wn9zXvrMl8zqrhF5t7zWyvpGJJ7d2ZZpukixovnm1W921JV5jZPjUs37lIUp4aLmB+Uw3XIPxfk/YPS3q98eLZJlrbfwAAAIhA5hzLp9G2rKwsV1RU1H5DAOige++9V9XV1cEOo9vEx8fr+9//frDDABDBzGyPcy6rpTrWVgMAgqa6ulp33nln+w07afny5T3af0vjAUCwkNgDQCt6OykEuqKt43Xfvn3aunWrTp70vbFcdHS0Jk2apC984QvedgUFBSovL1dSUpKmT5+u8ePH+/TTVn3zMXuibXdu21eFwz4LhxiffPJJHTp0yPt57Nixuu2224IYEYk9AAARbd++fcrLy5OZady4cXr77bcVGxurqKgoXXDBBdqzZ48kaeTIkcrPz1dOTo5GjRqlo0ePKjc3V5I0fvx47du3r8365mP2RNuW5tbZbfuqcNhn4RBjY1KflZWlK6+8Uvn5+SoqKtKTTz4Z1OQ+0ItnAQBAGCooKFBsbKxuuukmvfPOO/rc5z6nf/7nf1Z8fLzKyso0c+ZMvfrqqyooKFBOTo5SUlIUHR2tlJQU5eTkqKCgwNtPW/XNx+yJtt25bV8VDvssHGJsTOqvvfZa9e/fX9dee62ysrJ8zuAHA2fsAaANrJlGR4XaMVNeXi7nnEaNGqW6ujpNnjxZ0dHRqqxseP7h5MmTtWXLFpWXl2vUqFE+244aNUrl5eXeftqqbz5mT7Ttzm37qnDYZ+EQoyRdeeWVfp+DfbMREnsAaANr7HtWqCXB3SFYx0xr+zIpKUlnz57V0aNHFR0drT179ig5OVmJiYmKjY3Vnj17FB0drSFDhujo0aNKSUnxbnv06FElJSV5+2mrvvmYPdG2O7ftq8Jhn4VDjJKUn5+va6+91udzsLEUBwCACDZ9+nTV1NTomWee0Sc/+Un96U9/0v/8z/+ourpaycnJ2rp1qyZNmqTp06crNzdXhw8fVl1dnQ4fPqzc3FxNnz7d209b9c3H7Im23bltXxUO+ywcYhw7dqyKior0/PPP6+OPP9bzzz+voqIijR07NqhxccYeAFrB2XqEk9aO18aLDbdu3aqSkhJJ0tmzZyVJb7zxhiZPnuy9K44kvfDCC947kVx55ZXe7Rv/21p9S2N2d9vu3LavCod9Fg4x3nbbbXryySdVVFTkXX7DXXEAAECPGz9+fMCJclvtAu2nJ9t257Z9VTjss3CIMdhJfEtI7AEAQdXT6+x7cx1/fHx8r40FAM2R2AMAgoblTgDQfbh4FgAAAIgAJPYAAABABCCxBwAAACIAiT0AAAAQAUjsAQAAgAhAYg8AAABEABJ7AAAAIAKQ2AMAAACdtH379mCH4EViDwAAAEQAnjwLwOvvf/+7jhw5oqqqKiUkJGj06NEaPnx4h7YZNGiQPvzwww71ge7Xme8yVEXSXACEn3D6GURiD0BSww+uw4cPa9y4cUpMTFRlZaVKSkokqdUfYM23OXLkiI4dO6YRI0Zo8uTJAfWB7teZ7zJURdJcAISfcPsZxFIcAJKkI0eOaNy4cRo8eLCioqI0ePBgjRs3TkeOHAl4m/LycqWkpKiioiLgPtD9OvNdhqpImguA8BNuP4NI7AFIkqqqqpSYmOhTlpiYqKqqqoC3qaqq0vnnn++zTXt9oPt15rsMVZE0FwDhJ9x+BpHYA5AkJSQkqLKy0qessrJSCQkJAW+TkJCg9957z2eb9vpA9+vMdxmqImkuAMJPuP0MIrEHIEkaPXq0SkpKdOLECdXX1+vEiRMqKSnR6NGjA94mKSlJhw8f1tChQwPuA92vM99lqIqkuQAIP+H2M4iLZwFI+sdFQKWlpd4r/1NSUtq8OKilbc4//3xVVFTo2LFjAfWB7teZ7zJURdJcAISfcPsZRGIPwGv48OEd/mHVmW3Q8yLpe4mkuQAIP+H0M4ilOAAAAEAEILEHAAAAOumyyy4LdgheJPYAAABABGCNPdpVUVGhVatW+ZRlZGRoypQpqqmp0Zo1a/y2mThxoiZOnKiqqipt2LDBrz4rK0uZmZmqrKzUpk2b/OqnTp2qtLQ0lZeX67nnnvOrnzFjhsaOHauysjLl5eX51V911VUaOXKkjh07phdffNGvPjs7W8nJyTp06JB27NjhVz9r1iwlJSXp4MGD2r17t1/9DTfcoMTERO3fv19FRUV+9XPmzFFCQoKKi4tVXFzsVz9v3jzFxsaqsLBQBw4c8KtfsGCBJOnll1/2PuGuUWxsrObNmydJ2r59uw4fPuxTn5CQoDlz5kiStm7dquPHj/vUDxw4UDfeeKMkKS8vT2VlZT71Q4cO1XXXXSdJevbZZ1VRUeFTn5ycrOzsbEnSxo0bdfLkSZ/6ESNGaObMmZKkDRs2+N3rNyUlxXt2Y82aNaqpqfGpHzdunC655BJJ8jvuJI49jj2OPY49jr3mOPb67rHXHGfsAQAAgAhgzrlgx4AQl5WV5Vr6DRkAAAC9y8z2OOeyWqrjjD0AAAAQAUjsAQAAgAhAYg8AAABEAO6KAwBAmBkyZIhOnDgR7DBaNXjwYH3wwQfBDgPoc0jsAQAIMydOnFBXb35hZl3uo62+AfQ+luIAAICIsW7dOo0cOVJm5n0NHTpUQ4cO9X4eOXKk1q1bF+xQg2LdunXKzMxUdHS0MjMz++x+iFQk9gDQgzhzCfSedevW6dZbb9VHH32k5ORk/eIXv1BiYqI++OADffjhh/rhD3+oLVu2qLa2Vt/+9rf7XFK7bt06LVu2TA8++KCqq6v14IMPatmyZX1uP0Qy7mOPdnEfe6DzenK5A/qu7jiuenopTjCO+8zMTB04cEBjxozRY489piuuuEIpKSk6fvy4hg4dqqSkJO3fv1/btm3TV77yFQ0YMED79+/v9TiDJTMzUw8++KCuuOIKb9m2bdu0ZMmSPrUfwl1b97EnsUe7SOyBzuOMPXpKqCf2wRQVFaXq6mrFxsYqKirKO8+oqCjV1dWppqZGcXFxMjPV1dUFNdbeFB0d7d0vjWpqahQfH9+n9kO4ayux5+JZAOhhnEBBdwt24hyIYJ6xHzVqlHbu3KkrrrhCo0eP9jljL0k7d+7U6NGjNWDAgF6PMZjS09O9+6XRzp07lZ6eHsSo0J1YYw8AACLCsmXLJDXcNejWW2/VfffdpxMnTqi2tlbvv/++cnJy9Kc//Um33nqrTp8+7W3fVyxbtkwLFy7Utm3bVFNTo23btmnhwoV9bj9EMpbioF0sxQGA0MIa+9atW7dO3/ve93T8+HFv2ZAhQyTJe2/9ESNG6Be/+IXmzp0blBiDad26dbr77rv15ptvKj09XcuWLeuT+yGcscYeXUJiDwChhcQe6LtYYw8AQITpjnX2PbVWf/DgwT3SL4C2kdgDABBmOBsOoCVcPAsAAABEABJ7AAAAIAKQ2AMAAAARgMQeAAAAiAAk9gAAAEAEILEHAAAAIgCJPQAAABABuI89AAAhYunSpaqqqgp2GK1KSEjQ/fffH+wwALSCxB4AgBBRVVWlhx56qMv9LFq0qFv6aalfAKGLxB4AAIS8wsJC5eXlqaysTGam+vp6SQ1/RejXr58qKyuVnJys7OxsTZkyxW+bpnXNy8eNG6eSkhK/dh2Nq6PbIryF4ndPYg8AYaqnzsoCoWTRokW6/fbblZubqylTpujkyZNyzikmJkajR4/W/v37VV9fry996UsaNGiQVq9e7d02NzdX8+fPV2pqqkpLS7V69WodOnRI+/fv95Y///zz2rJli66++mr96Ec/8raT1G6SVlhY2OIYgWyL8Baq3z0XzwIAgJCWl5en+fPna+/evYqPj9fXvvY13X777XrzzTd1ww03KCEhQVu2bFFaWprmz5+vvLw87zZpaWmKjo721u3atcunfO/evZo9e7b27t3r0y4vLy/guJqPEci2CG+h+t1zxh4AwhhrntHbgnHMlZWVKTU1VWVlZZKk1NRUSVJtba1mzJihjRs3ysy8dc3bNUpNTVVtba1PeVlZmWbMmKFNmzb5tGvsI5C4mo8RyLYIb6H63ZPYA0AYYylOZAmHX9R6+5hbtGiRkpOTVVpaquTkZJ09e1alpaWSpJiYGO3YsUNDhgxRXFycJHnbNb5PS0vz9lVaWqqYmBif8uTkZO3YscO7TfM+2tIYV/MxAtkW4S1Uv3uW4gAAgJCWnZ2t1atXa8KECaqurtYjjzyixx9/XOnp6dq0aZOqqqp09dVX6+DBg1q9erWys7O92xw8eFB1dXXeumnTpvmUT5gwQZs3b9aECRN82mVnZwccV/MxAtkW4S1Uv3vO2ANAmOJsPfqCpsd5Xl6eqqqqvHfF2bdvn/euOE888YSSk5OVk5Pjc/Hihg0bvHctaawbO3asT/n06dO1d+9e/fGPf2yxj9Y0tmlpDES2UP3uSewBAEDImzJlSoeTpta26Uxf3RkXIkMofvck9gAAhJDuWmffE+v1ExISur1PAN2HxD4EmNkYSc855zIDbH+XpFPOOZ7rDQARhOVVALqCi2cBAACACEBiHzqizewRMztgZlvMrL+ZfdLM8sxsj5kVmNmFzTdqrY2ZrTKzX5vZy2Z2yMxu9pSfY2YvmtmrZrbPzK7v7YkCAACg+5HYh44LJP3WOZch6UNJN0l6WNIS59xkSUsltfQ32rbanC/pUkmzJP3cU1Yt6Qbn3CRJV0haYY1P9WjCzL5uZkVmVvT+++93x/wAAADQg1hjHzoOO+eKPe/3SBoj6RJJTzXJu+OabmBm57TTZrNzrl7SG2Z2XuNmku4xsxmS6iX9k6TzJPk8Ks0597AafmlQVlaW6+LcAAAA0MNI7EPHmSbv69SQbH/onJvYxjZR7bRp2mdj5j9P0jBJk51zNWb2rqT4zgQMAACA0MFSnNB1UtJhM/uiJFmDCU0bOOfabdOCREl/9yT1V0ga3QOxAwAAoJeR2Ie2eZIWmtleSQcktXShayBtmlojKcvM9kn6kqS3ujFeAAAABIk5x/JptC0rK8sVFRUFOwwAAILq3nvvVXV1dbDDQIiJj4/X97///V4bz8z2OOeyWqpjjT0AAEAAqqurdeeddwY7DHTQ8uXLe/R7W758eY/13VEsxQEAAAAiAIk9AMArlM48AQA6hsQeAAAAiACssQcA+OCsPQCEJxJ7AIAPLg4EWsYvvQh1LMUBAAAAIgCJPQDAi7P1ABC+SOwBAACACMAaewAAgACxzj489eT3Fh8f32N9dxSJPQAAQABYqoZQx1IcAAAAIAKQ2AMAAAARgMQeAAAAiAAk9gAAAEAEILEHAAAAIgCJPQAAABABSOwBAACACMB97AEAABCQXbt2qba2NthhhJzLLrss2CFIIrEHAABAgGpra0MmiQ0V27dvD3YIXizFAQAAACIAiT0AAPAKpbOPADqGxB4AAACIAKyxBwAAPjhrD4QnEnsAAOCDiyPRGn7pC20sxQEAAAAiAIk9AADw4mw9EL5I7AEAAIAIwBp7AAAABIx19qGLxB4AAAABYalWaGMpDgAAABABOGOPdlVUVGjVqlU+ZRkZGZoyZYpqamq0Zs0av20mTpyoiRMnqqqqShs2bPCrz8rKUmZmpiorK7Vp0ya/+qlTpyotLU3l5eV67rnn/OpnzJihsWPHqqysTHl5eX71V111lUaOHKljx47pxRdf9KvPzs5WcnKyDh06pB07dvjVz5o1S0lJSTp48KB2797tV3/DDTcoMTFR+/fvV1FRkV/9nDlzlJCQoOLiYhUXF/vVz5s3T7GxsSosLNSBAwf86hcsWCBJevnll1VSUuJTFxsbq3nz5klq+HPo4cOHfeoTEhI0Z84cSdLWrVt1/Phxn/qBAwfqxhtvlCTl5eWprKzMp37o0KG67rrrJEnPPvusKioqfOqTk5OVnZ0tSdq4caNOnjzpUz9ixAjNnDlTkrRhwwZVVVX51KekpHjP+KxZs0Y1NTU+9ePGjdMll1wiSX7HncSxx7HHscexx7HXHMde3z32muOMPQAAABABzDkX7BgQ4rKyslxLvyEDAACgd5nZHudcVkt1nLEHAAAAIgCJPQAAABABSOwBAACACMBdcQAAEWvIkCE6ceJEsMNALxg8eLA++OCDYIcBBBWJPQAgYp04cULhcJMIMwuLOEOZmQU7BCDoWIoDAAAQROvWrVNmZqaio6OVmZmpdevWdbpt0/qRI0dq5MiRioqKUnx8vKKiorxlTetb6qu1cToSa2fat6e7++uKJUuWKD4+Xmam+Ph4LVmyJGixeDnnePFq8zV58mQH9ISGH0FAzwmXYyxc4gxlob4PW4tv7dq1LiUlxeXn57uzZ8+6/Px8l5KS4tauXdvhtk3rn3jiCXf++ee7xMREN2zYMLdixQqXlJTkEhMT3fnnn+/uuOMOd/7557vk5GT3xBNP+PTV2jiLFy8OONaOzi0Q3d1fVyxevNjFxMS4FStWuNOnT7sVK1a4mJgYt3jx4h4fW1KRayVnC3rSyCv0XyT26Cmh/j9ihL9wOcbCJc5QFur7sLX4MjIyXH5+vk9Zfn6+y8jI6HDbpvWN78eMGePGjBnjnHPe9/n5+S4uLs7l5+f7bN/4vrVxGrcJJNaOzi0Q3d1fV8TFxbkVK1b4lK1YscLFxcX1+NhtJfY8oArt4gFV6CmsiUVvCIf/z7HGvuvC4edJS99xdHS0qqurFRsb6y2rqalRfHy86urqOtS2aX3j+/j4eDnnVF9fr+joaDnndObMGfXr109nz56VJO/2jX1JanGcxm0CibWjcwtEd/fXFWam06dPKyEhwVtWVVWlAQMG9Pi/ZR5QBSBktXbWgRev7nihbwn28daZYzE9PV07d+70Kdu5c6fS09M73LZpfeP7UaNGafTo0ZLkfb9z507FxcVp586dPts3vm9tnMZtAom1o3MLRHf31xVxcXFauXKlT9nKlSsVFxfX67H4CPaBziv0XyzFQU9RiP/pHOEvXI6xcIkzlIX6PmwtPtbYB4419g3EGnteXXmR2AMIV6Ge7DUKlzhDWTjvw7Vr17qMjAwXFRXlMjIy2kxU22vbtH7EiBFuxIgRzsxcXFycMzNvWdP6lvpqbZyOxNqZ9u3p7v66YvHixS4uLs5JcnFxcb2S1DvnWGOPrmGNPYBwFS5r18MlzlDGPkRf0dYaex5QBQCIaOFwUaUUPnGGqsGDBwc7BCDoSOwBABGLM7gA+hLuigMAAABEABJ7AAAAIAKQ2AMAAAARgMQeAAAAiAAk9gAAAEAEILEHAAAAIgCJPQAAABABuI89AARg6dKlqqqqCnYY6EYJCQm6//77gx0GAHQbEnsACEBVVZUeeuihYIfR4xYtWtQn5ik1zBUAIgmJPQAAfUBhYaHy8vJUVlam5ORkZWdna8qUKQFvv379eu3atUu1tbWKiopSfHy8Pv744071FUm6ul97q0/0DST2CDl96YwhAHRUZ35GFhYWKjc3V/Pnz1dqaqpKS0u1evVqSQooYVy/fr0KCgo0e/ZsDRgwQM8884w+/vhjXXrppZo0aVKH+ookXd2vvdUn+g4ungUAIMLl5eVp/vz5SktLU3R0tNLS0jR//nzl5eUFtP2uXbs0e/ZszZw5U1u3btXXvvY13XDDDdq9e3eH+4okXd2vvdUn+g7O2CMksfYVQG/oKz9rysrKlJqa6lOWmpqqsrKygLavra3VjBkzfPpKSUnRxo0bO9xXJOnqfu2tPtF3kNgjJLEUB6GmrySAfU04/qzpzLGYnJys0tJSpaWlectKS0uVnJwc0PYxMTHasWOHZs6c6e3r2LFjiomJ6XBfkaSr+7W3+kTfwVIcAAAiXHZ2tlavXq2DBw+qrq5OBw8e1OrVq5WdnR3Q9tOmTdPmzZu1detWzZw5U4888og2bdqkqVOndrivSNLV/dpbfaLv4Iw9Qk44nkEDgN7SmZ+RjRddbtiwwXunlZycnIAvxrzlllskSbm5ud674vTv3187d+5UaWlph/qKJF3dr73VJ/oOEnsAAPqAKVOmdCk5vOWWW7wJPv6hq/u1t/pE30BiDwAB6ivr7PvKPBMSEoIdAgB0q4hM7M3MSVrjnJvv+Rwj6T1Jf3bOzepkn3+QdKtz7sMW6pZJ+qLn43hJ+zzvH3PO/bpZ2zGSnnPOZXYmDgDBwRIxAECoi8jEXtJpSZlm1t8597Gkz0n6S1c6dM59oY26uyXdLUlmdso5N7ErYwEAAAAdFcl3xfmDpGs97+dKWtdYYWafNrPdZvaamb1sZmme8gQz22Bmb5jZJjP7s5lleereNbMkz/svmdnrZrbXzJ5saXAzizaz+8ys0NP2G4G2MbPzzWyHmRWb2X4zm+4pzzazVz3jvugpG2Jmmz3b/5+ZXewpv8vMnvTM820z+1qTcf+tyZjLu7ynAQAAEHSResZekv5H0o/N7DlJF0t6TNJ0T91bkqY752rNbKakeyTdJGmRpBPOuYvMLFNScfNOzSxD0r9LusQ5V25mQ1oZf6GkSufcFDOLk7TLzLZIcgG0uVHSH51zd5tZtKQEMxsm6RFJM5xzh5uMu1zSa8652WZ2paQnJE301F0s6bOSBkh6zcyel5Qp6QJJn5ZkknLNbIZzbkcgOxUAAAChKWITe+fc65717HPVcPa+qURJvzezC9SQaMd6yi+V9F+e7feb2estdH2lpKecc+Wedh+0EsLVki42s5ubjHmBpJIA2hRKeszMYiVtds4Vm9nlknY45w43G/dSNfxSIudcvpkNNbOBnrr/9SxF+tjMtqkhmb/UM+5rnjbneMb0SezN7OuSvi5Jo0aNamWKAAAACBURm9h75Eq6X9LlkoY2Kf+ppG3OuRs8yf9LPTC2SVrinPujT2HDeG228bSboYalRKvM7JeSTnQiBtfCZ5P0n865/6/NDZ17WNLDkpSVldW8HwAAAISYSF5jLzUsv1nunNvXrDxR/7iYdkGT8l2S5kiSmV2khjvcNJcv6YtmNtTTrrWlOH+UdIfnrLvMbJyZDQikjZmNlvQ359wjkv5b0iRJ/ydphpmlNBu3QNI8T9nlksqdcyc9ddebWbwn1svV8JeAP0r6ipmd49nmn8xseCtzAAAAQJiI6DP2zrnjkn7dQtUv1LAU598lPd+k/CFP+RtqWId/QFJlsz4PmNndkrabWZ0alrQsaGGM/5Y0RtKrZmaS3pc0O8A2l0v6NzOrkXRK0pecc+97lsdsNLMoSX9Xw91+7lLDsp3XJVVJ+nKT/l+XtE1SkqSfOuf+KumvZpYuaXfDkDolab6nPwAAAIQpc45VFo08F6rGOueqzeyTkrZKSnPOnQ1yaB1mZndJOuWcu7+rfWVlZbmioqKuBwUAfdS9996r6urqYIcBoAfEx8fr+9//fq+NZ2Z7nHNZLdVF9Bn7TkiQtM2zNMYkLQrHpB4AEFqqq6t15513BjsMIKwtX748JP8dLV8eOncOJ7Fvwjn3kaQWfwMKN865u4IdAwAAAHpPpF88C6CZUDqzAAAAug+JPQAAABABWIoD9EGctQcAIPKQ2AN9UChefAREMn6ZBtAbWIoDAAAARAASe6CP4Ww9AACRicQeAAAAiACssQcAoBewzh7oulD8dxQfHx/sELxI7AEA6GEsgQPQG1iKAwAAAEQAEnsAAAAgApDYAwAAABGAxB4AAACIACT2AAAAQAQgsQcAAAAiAIk9AAAAEAFI7AEAAIBO2r59e7BD8CKxBwAAACIAT54F0Ov+/ve/68iRI6qqqlJCQoJGjx6t4cOH90g/3TUW/oF92vPYx72PfY5IQGIPoFf9/e9/1+HDhzVu3DglJiaqsrJSJSUlktSh/4kG0k93jYV/YJ/2PPZx72OfI1KwFAdArzpy5IjGjRunwYMHKyoqSoMHD9a4ceN05MiRbu+nu8bCP7BPex77uPexzxEpSOwB9KqqqiolJib6lCUmJqqqqqrb++musfAP7NOexz7ufexzRAoSewC9KiEhQZWVlT5llZWVSkhI6PZ+umss/AP7tOexj3sf+xyRgsQeQK8aPXq0SkpKdOLECdXX1+vEiRMqKSnR6NGju72f7hoL/8A+7Xns497HPkek4OJZAL2q8UK00tJS790nUlJSOnyBWiD9dNdY+Af2ac9jH/c+9jkiBYk9gF43fPjwbvkfZiD9dNdY+Af2ac9jH/c+9jkiAUtxAAAAgAhAYg8AAAB00mWXXRbsELxI7AEAAIAIQGIPAAAARAAunkW7KioqtGrVKp+yjIwMTZkyRTU1NVqzZo3fNhMnTtTEiRNVVVWlDRs2+NVnZWUpMzNTlZWV2rRpk1/91KlTlZaWpvLycj333HN+9TNmzNDYsWNVVlamvLw8v/qrrrpKI0eO1LFjx/Tiiy/61WdnZys5OVmHDh3Sjh07/OpnzZqlpKQkHTx4ULt37/arv+GGG5SYmKj9+/erqKjIr37OnDlKSEhQcXGxiouL/ernzZun2NhYFRYW6sCBA371CxYskCS9/PLL3seaN4qNjdW8efMkSdu3b9fhw4d96hMSEjRnzhxJ0tatW3X8+HGf+oEDB+rGG2+UJOXl5amsrMynfujQobruuuskSc8++6wqKip86pOTk5WdnS1J2rhxo06ePOlTP2LECM2cOVOStGHDBr8HvKSkpHj/bLlmzRrV1NT41I8bN06XXHKJJPkddxLHHscexx7HHsdecxx7fffYa44z9gAAAEAEMOdcsGNAiMvKynIt/YYMAACA3mVme5xzWS3VccYeAAAAiAAk9gAAAEAE4OJZAECvGjJkiE6cOBHsMNCLBg8erA8++CDYYQARj8QeANCrTpw4oVC8vsvMQjKuSGBmwQ4B6BNYigMAANCOdevWKTMzU9HR0crMzNS6desCqguX8dBxF198sczM+7r44ouDHRJn7AH0TZydBdCWpj8j1q1bp2XLlunRRx/VpZdeqp07d2rhwoXetq3VzZ07t1Nj9/Z46LiLL75Y+/btU05Ojh599FEtXLhQubm5uvjii/X6668HLzDnHC9ebb4mT57sgEjT8OMPwRCq+z5U44oE4bhvm8ackZHh8vPzferz8/NdRkZGm3Wd1dvjoeMkuZycHJ+ynJycXjnWJRW5VnI27mOPdnEfe0Qi1vwGVyj+v4e/4vSccP331ng8REdHq7q6WrGxsd66mpoaxcfHS1KrdXV1dZ0at7fHQ8eZmd5//30lJSV5y8rLyzVs2LAe/znCfewBoAWtnfHg1bMv9E3BPu66cpymp6dr586dPmU7d+5Uenp6m3Wd1dvjoXOaLo9q6XMwkNgDAAC0YdmyZVq4cKG2bdummpoabdu2TQsXLtSyZcvarAuX8dBx48ePV25urq6//nqVl5fr+uuvV25ursaPHx/UuLh4FkCfxJljAG1p+jOi8aLUJUuW6M0331R6erruvvtun4tV26rrqN4eDx33+uuv6+KLL1Zubq6GDRsmqSHZD+qFsxJr7NE+1tgD6E6hupY9VOOKBOxboPu0tcaeM/YAgF4XqhdThmpc4W7w4MHBDgHoE0jsAQC9ijO3ANAzuHgWAAAAiAAk9gAAAEAEILEHAAAAIgCJPQAAABABSOwBAACACEBiDwAAAEQAEnsAAAAgAnAfewBAyFi6dKmqqqqCHQY6ICEhQffff3+wwwAgEnsAQAipqqrSQw89FOwwesSiRYsicm6LFi0KdggAPEjsAQAAWlFYWKi8vDyVlZUpOTlZ48aNU0lJifdzdna2pkyZ0mLb5nWbNm3Shx9+KEmKiopSfX29YmJiVFdX520vqdU+QkXzuQwaNEg33HBDyMXZFW19l6GMxB4AWhCpZ1eBvqYr/5YLCwuVm5ur+fPnKzU1Vc8//7y2bNmiq6++Wj/60Y9UWlqq1atXe9s3bdu87qmnnlJUVJSuvvpq7d69W2fOnFFNTY0+9alP6Z133tGECRP01FNPSZIWLlzo10eoJJWFhYXeuSxevFhmpt///vfe2EMlzq5o/r2H4vfQGi6eBQAAaEFeXp7mz5+vtLQ0RUdHa+/evZo9e7b27t2r6OhopaWlaf78+crLy/Nr27wuLi5Ot99+u/bt26evfOUrOvfcc3XOOefo+PHjuu2227R3717FxcWpX79+LfYRKvLy8tSvXz/dfvvtuuiii5Senq7bb79dcXFxIRVnV7T1XYY6ztgDQCtYOwwEJlL/rZSVlSk1NdXn84wZM7Rp0yZvWWpqqsrKyrzvm2pa1/RzamqqPvjgAznndOrUKZ92zrk2+wi2srIyOed85to4n0jR/HuXQu97aA2JPQC0gqU4vS9SE8RIF8r/VrpyTCUnJ6u0tFRpaWnezzt27FBycrK3TWlpqfdz07bN686ePev9XFpaqiFDhujs2bM655xzvOVnz571S+yb9hEKkpOTdebMGZ+5Ns6nX79+QY6uezT/3qXQ+x5aw1IcAACAFmRnZ2v16tU6ePCg6urqNGHCBG3evFkTJkxQXV2dDh48qNWrVys7O9uvbfO6M2fO6PHHH9f48eP12GOP6aOPPtKpU6c0YsQIPfnkk5owYYLOnDmjs2fPtthHqMjOztbZs2f1+OOP64033tCbb76pxx9/XGfOnAmpOLuire8y1HHGHgAAoAWNF0pu2LDBe3eU6dOna+/evfrjH/+o5ORk5eTk+FxQ2bRt87pNmzZpy5YtkhruiuOc02uvvaa6ujrt3btXX/ziF9vtI9gaY9m0aZN+85vfSGq4K85NN90UUnF2RUvfe6h9D62x5n/yAZrLyspyRUVFwQ4DQB8QyXcjitS5Req8gFBlZnucc1kt1XHGHgAQUiJ5nX0kzi0hISHYIQDwILEPMjNbIGmLc+6vns//LemXzrk3ghoYAAQBZ34BoPNI7INvgaT9kv4qSc65rwY1GgAAAIQl7orTA8xsgJk9b2Z7zWy/md1iZj82s0LP54etwc2SsiStMbNiM+tvZi+ZWZann1Nmdp+ZHTCzrWb2aU/9ITPL8bQZY2YFZvaq53WJpzzKzB4ys7fM7E9m9gfPeDKzyWa23cz2mNkfzez8YO0rAAAAdA8S+56RLemvzrkJzrlMSXmSfuOcm+L53F/SLOfc05KKJM1zzk10zn3crJ8BkvKdcxmSPpL0M0mfk3SDpJ942vxd0uecc5Mk3SLp157yGyWNkXSRpNskTZUkM4uV9KCkm51zkyU9Junu7t4BAAAA6F0sxekZ+yStMLN7JT3nnCsws5vM7HuSEiQNkXRA0rPt9HNWDb8UNPZ5xjlXY2b71JC0S1KspN+Y2URJdZLGecovlfSUc65eUpmZbfOUp0nKlPQnM5OkaEnvNR/YzL4u6euSNGrUqA5MHQAAAMFAYt8DnHMlZjZJ0hck/czMXpT0TUlZzrljZnaXpPgAuqpx/7gfab2kM57+682s8bv7F0l/kzRBDX+BqW6nT5N0wDk3tZ05PCzpYanhdpcBxAoAAIAgYilODzCzT0iqcs6tlnSfpEmeqnIzO0fSzU2afyTp3C4MlyjpPc+Z+dvUcAZeknZJusmz1v48SZd7yg9KGmZm3qU5ZpbRhfEBAAAQAjhj3zPGS7rPzOol1Ui6Q9JsNdz9pkxSYZO2qyStNLOP5VkH30EPSXrGzL6khmU7pz3lz0i6StIbko5JelVSpXPurOci2l+bWaIajoFfqWFpEAAAAMIUT56NYGZ2jnPulJkNlfSKpGnOubKO9sOTZwEAAFq2fPly3Xnnnb02Hk+e7bueM7NBkvpJ+mlnknoAAACEBxL7COacuzzYMQCIDPv27VNBQYHKy8uVlJSk6dOna/z48b06VqAxtNeuN+cSqFCIKRRi6Gl9YY5oW6QfAyT2AIA27du3T/n5+crJydGoUaN09OhR5ebmSlK3/w+xtbGOHTumt99+u90Y2ou1N+cSqFCIKRRi6Gl9YY5oW184BrgrDgCgTQUFBcrJyVFKSoqio6OVkpKinJwcFRQU9NpYr776akAxtBdrb84lUKEQUyjE0NP6whzRtr5wDJDYAwDaVF5e7vegulGjRqm8vLzXxqqrqwsohvZi7c25BCoUYgqFGHpaX5gj2tYXjgESewBAm5KSknT06FGfsqNHjyopKanXxoqOjg4ohvZi7c25BCoUYgqFGHpaX5gj2tYXjgESewBAm6ZPn67c3FwdPnxYdXV1Onz4sHJzczV9+vReG2vSpEkBxdBerL05l0CFQkyhEENP6wtzRNv6wjHAxbMAgDY1XlT2wgsveO8kceWVV/bIxWZtjbVv3752Y2gv1t6cS6BCIaZQiKGn9YU5om194RjgAVVoFw+oAgAAaFkoPaCKpTgAAABABCCxBwAAADqpN8/Wt4fEHgAAAIgAJPYAAABABCCxBwAAACIAiT0AAAAQAUjsAQAAgAhAYg8AAABEABJ7AAAAIAKQ2AMAAACdtH379mCH4EViDwAAAESAmGAHAABAJPj73/+uI0eOqKqqSgkJCRo9erSGDx/ea9sDgeJYi1wk9gAAdNHf//53HT58WOPGjVNiYqIqKytVUlIiSQElTF3dHggUx1pkYykOAABddOTIEY0bN06DBw9WVFSUBg8erHHjxunIkSO9sj0QKI61yEZiDwBAF1VVVSkxMdGnLDExUVVVVb2yPRAojrXIRmIPAEAXJSQkqLKy0qessrJSCQkJvbI9ECiOtchGYg8AQBeNHj1aJSUlOnHihOrr63XixAmVlJRo9OjRvbI9ECiOtcjGxbMAAHRR40WHpaWl3juNpKSkBHwxYle3BwLFsRbZSOwBAOgGw4cP71Jy1NXtgUBxrEUuluIAAAAAEYDEHgAAAOikyy67LNgheJHYAwAAABGAxB4AAACIAFw8i3ZVVFRo1apVPmUZGRmaMmWKampqtGbNGr9tJk6cqIkTJ6qqqkobNmzwq8/KylJmZqYqKyu1adMmv/qpU6cqLS1N5eXleu655/zqZ8yYobFjx6qsrEx5eXl+9VdddZVGjhypY8eO6cUXX/Srz87OVnJysg4dOqQdO3b41c+aNUtJSUk6ePCgdu/e7Vd/ww03KDExUfv371dRUZFf/Zw5c5SQkKDi4mIVFxf71c+bN0+xsbEqLCzUgQMH/OoXLFggSXr55Ze9j/puFBsbq3nz5kmStm/frsOHD/vUJyQkaM6cOZKkrVu36vjx4z71AwcO1I033ihJysvLU1lZmU/90KFDdd1110mSnn32WVVUVPjUJycnKzs7W5K0ceNGnTx50qd+xIgRmjlzpiRpw4YNfg89SUlJ8f7Zcs2aNaqpqfGpHzdunC655BJJ8jvuJI49jj2OPY49jr3mOPb67rHXHGfsAQAAgAhgzrlgx4AQl5WV5Vr6DRkAAAC9y8z2OOeyWqrjjD0AAAAQAUjsAQAAgAjAxbMAAPQBQ4YM0YkTJ4IdRsQYPHiwPvjgg2CHAfggsQcAoA84ceKEQvG6OjMLybjaY2bBDgHww1IcAACAPmTdunUaOXKkzExmppEjR2rJkiXKzMxUdHS0MjMztW7dOm/7JUuWKD4+Xmam+Ph4LVmyROvWrWu1fXfH2nycjozd2DYqKkrx8fGKiorqtnhb2i9B55zjxavN1+TJkx3Q1zX8uATCV6gew6EaV3tCNe724lq7dq0bNmyYS05Odlu2bHFbtmxxgwYNclFRUW7ZsmXu7NmzLj8/36WkpLi1a9e6xYsXu5iYGLdixQp3+vRpt2LFChcVFeXOPfdcl5+f79e+O61du9alpKT4jDNs2DA3bNiwgMZu3H7ZsmVuzJgxbsWKFd7PXY23pf0SExPjFi9e3JUpB0RSkWslZwt60sgr9F8k9oAL2f+JA4EK1WM4VONqT6jG3V5cGRkZbsyYMS4/P99bNmbMGJecnOwyMjK8Zfn5+S4jI8PFxcW5FStW+PRx3nnnudjYWJ+yxvbdKSMjwyfOxljHjBkT0NiN2zftp+nnrsTb0n5ZsWKFi4uL63SfgWorsec+9mgX97EHWE+LyBCK/89njX33a2t/RkdHyzmnM2fOKDY2VpIUFRXlnU9dXZ0kqaamRvHx8aqvr9fp06eVkJDg7SMqKsqbSDZqbN+4fXeIjo5WdXW1N86m8dfX17c7duP28fHx3n4a2zaWdzZeM/PbL1VVVRowYECPH8/cxx4AukFrZ0h48QqHF7pfsL/TznzP6enpGj16tHbu3OktGz16tIYPH6709HRv2c6dO5Wenq64uDitXLnSp4/hw4f7JNtN23en9PR0nzgladSoURo9enRAYzdu37Sfpp+7Em9L+2XlypWKi4vrdJ/dItgHIK/Qf7EUB3Ah+2d3IFChegyHalztCdW424uLNfassefVx18k9oAL2f+JA4EK1WM4VONqT6jGHUhca9eudSNGjHCSnCQ3YsQIt3jxYpeRkeGioqJcRkaGT9K7ePFiFxcX5yS5uLg4t3jxYrd27dpW23enlsbpyNiNbc3MxcXFOTPrtnhb2i+9oa3EnjX2aBdr7AEg/IXqWvZQjas94Ro3wl9ba+x5QBUAAH1EqF7wGapxtWXw4MHBDgHwQ2IPAEAfwNllIPJxVxwAAAAgApDYAwAAABGAxB4AAACIACT2AAAAQAQgsQcAAAAiAIk9AAAAEAFI7AEAAIAIwH3sAQDoo5YuXaqqqqpghwGPhIQE3X///cEOA2GMxB4AgD6qqqpKDz30ULDDCNiiRYvCKt6OWrRoUbBDQJgjsQcAAECXFRYWKi8vT2VlZUpOTlZ2drYk+ZVNmTKl1T7Wr1+vXbt2qba2VjExMZo2bZrGjh3bYh8tjddW393twQcf1Jtvvun9nJ6eriVLlvTa+C0hsQeACBXpZzcB9K62fqYUFhYqNzdX8+fPV2pqqkpLS/Xoo49KkhYuXOgtW716tSS1mICvX79eBQUFmj17tmbMmKEdO3Zo06ZN+vOf/6xvfOMbPn0cOnRI+/fv9xmvrb67W2NSP336dM2ePVubN29WQUGBHnzwwaAm91w8CwAAgC7Jy8vT/PnzlZaWpujoaKWlpalfv36Ki4vzKZs/f77y8vJa7GPXrl2aPXu2Zs6cqX79+mnmzJk699xzdfbsWb8+du3a5TdeW313t8akfu7cuerfv7/mzp2r6dOn+5zBDwbO2ANABGPNLhBewvXfbFlZmVJTU33KPvjgA5mZT1lqaqrKyspa7KO2tlYzZszwKfvoo4/knPPro7a21m+8tvruCbNnz/b7XFBQ0Gvjt4TEHgAiGEtx0JZwTSIjWSj/m23reElOTlZpaanS0tK8ZUOGDPFL7EtLS5WcnNxiHzExMdqxY4dmzpzpLTv33HN16tQpvz5iYmL8xmur756wefNmzZ071+dzsLEUBwAAAF2SnZ2t1atX6+DBg6qrq9PBgwd19uxZnTlzxqds9erV3otqm5s2bZo2b96srVu36uzZs9q6das++ugj9evXz6+PadOm+Y3XVt/dLT09XQUFBVq3bp0+/vhjrVu3TgUFBUpPT++V8VvDGXsAAAB0SeMFqxs2bPDepeaLX/yiX1lOTk6rF7fecsstkqTc3Fxt3LhRMTExmjFjhsaOHdtiH62V94YlS5bowQcfVEFBgXf5TSjcFcear1sCmsvKynJFRUXBDgMA0M3C7c5J4RZvR0X6/NA9zGyPcy6rpTrO2AMA0IeF2zr7cIu3IxISEoIdAsIciX0QmdkgSbc65zr867mZTZT0CefcH7o7LgBA38DZYSCycPFscA2S1NlTDxMlfaEjG1gDvnMAAIAIRJIXXD+X9EkzKzaz+8zs38ys0MxeN7PlkmRmN5jZi56k/HwzKzGzUZJ+IukWz7a3mNldZra0sWMz229mYzyvg2b2hKT9kka2NA4AAADCG4l9cP1A0jvOuYmS/iTpAkmfVsPZ+MlmNsM5t0nSe5K+KekRSXc6545K+rGk9c65ic659e2Mc4Gkh5xzGZLSWhqnuycGAACA3sUa+9Bxtef1mufzOWpIwHdIWqKGs+3/55xb14m+jzjn/i+AcbzM7OuSvi5Jo0aN6sSQAAAA6E0k9qHDJP2nc+7/a6FuhKR6SeeZWZRzrr6FNrXy/QtMfJP3pwMcx8s597Ckh6WG210GED8AAACCiKU4wfWRpHM97/8o6Stmdo4kmdk/mdlwM4uR9JikuZLelPSvLWwrSe9KmuTZdpKklFbGbHGcbpsRAAAAgoIz9kHknKsws11mtl/SC5LWStptZpJ0StJ8Sf9PUoFzbqeZ7ZVUaGbPS9om6QdmVizpPyU9I+lLZnZA0p8llbQy5hYzS29hnL/33EwBAADQ03jyLNrFk2cBAABatnz5ct155529Nl5bT55lKQ4AAAAQAViKAwBAmNu3b58KCgr0/vvve8uio6M1adIkfeELgT3LsLGP8vJyJSUlafr06Ro/fnyX20aS7p53X92PoSTSvgMSewAAwti+ffuUn5+v8847TxUVFZo0aZJKSko0evRo7dmzR5LaTe4b+8jJydGoUaN09OhR5ebmSpJfktORtpGku+fdV/djKInE74ClOAAAhLGCggLl5OSotLRUM2fO1LXXXqvZs2errKxMM2fO1KuvvhpwHykpKYqOjlZKSopycnJUUFDQpbaRpLvn3Vf3YyiJxO+AxB4AgDBWXl6uUaNGqa6uTpMnT5bU8GDB8vJyTZ48WXV1dQH30VRjH11pG0m6e959dT+Gkkj8DkjsAQAIY0lJSTp69Kiio6O9S2+OHj2qpKQk7dmzR9HR0QH30VRjH11pG0m6e959dT+Gkkj8DkjsAQAIY9OnT1dubq5SU1O1detWPf/889q8ebOSk5O1detWTZo0KeA+Dh8+rLq6Oh0+fFi5ubmaPn16l9pGku6ed1/dj6EkEr8DLp4FACCMNV7kV1BQoPr6ejU+d+SNN97Q5MmTA7orTmMfL7zwgvfuIFdeeWWLFxB2pG0k6e5599X9GEoi8TvgAVVoFw+oAgAAaBkPqAIAAADQrUjsAQAAgE7qzbP17SGxBwAAACIAiT0AAAAQAUjsAQAAgAhAYg8AAABEABJ7AAAAIAKQ2AMAAAARgMQeAAAAiAAk9gAAAEAEILEHAAAAOmn79u3BDsGLxB4AAACIACT2AAAAQAQgsQcAAAAiAIk9AAAAEAFI7AEAAIAIQGIPAAAARAASewAAACACkNgDAAAAEYDEHgAAAIgAJPYAAABAJ1122WXBDsGLxB4AAACIACT2AAAAQASICXYACH0VFRVatWqVT1lGRoamTJmimpoarVmzxm+biRMnauLEiaqqqtKGDRv86rOyspSZmanKykpt2rTJr37q1KlKS0tTeXm5nnvuOb/6GTNmaOzYsSorK1NeXp5f/VVXXaWRI0fq2LFjevHFF/3qs7OzlZycrEOHDmnHjh1+9bNmzVJSUpIOHjyo3bt3+9XfcMMNSkxM1P79+1VUVORXP2fOHCUkJKi4uFjFxcV+9fPmzVNsbKwKCwt14MABv/oFCxZIkl5++WWVlJT41MXGxmrevHmSpO3bt+vw4cM+9QkJCZozZ44kaevWrTp+/LhP/cCB/397dx9dV3Xeefz3SLKlXBgUGdsjN7IlJUaKkcFOLLcJjO28aIjagENIcJJiWhhWMtQ1WV0Zd5qGDJTJmqzJAk9X3qgH2uCCXwbDGEYmg+I4Kn6DpLJTuzYhdhQcA5No/CZEisaWLZ75Q/derl7vi67uOff4+1nrLOucvc/ezznelh5t73PuZbrpppskSe3t7eru7h5Sfvnll+uGG26QJG3btk2nT58eUl5dXa3W1lZJ0tatW/XGG28MKa+pqVFLS4skacuWLerr6xtSXl9fn/xvy40bN+r8+fNDyhsaGnTNNddI0ohxJzH2GHuMPcYeY284xt7FO/aGY8YeAAAAiABz96BjQMg1Nzf7aL8hAwAAoLDMbL+7N49Wxow9AAAAEAEk9gAAAEAEkNgDAAAAEcBbcQAAoTFt2jT19PQEHQZSVFVV6cyZM0GHASADzNgDAEKjp6dH7h6KTVLgMYRh4xctafPmzZo9e7bMTGam2bNna/PmzePWnz9/vkpLSzV//vwhdRNlJSUlqqioUElJyZA6qefOnj1bs2fPHrWdTPoKk2zizOWa0t3XfPYVakF/w2AL/7Zo0SIHEC6D376jJ0zXFaZYglSM9yGfMW/atMlnzJjhs2bN8u3bt/v27du9urraZ8yY4Zs2bRq1fn19vXd0dHh/f793dHR4fX29b9q0KVl29913e319va9du9br6uqS+6tXr06e++ijj/qsWbO8urraH3300SHtZNJXmGQTZy7XlO6+jnVusdy/4STt8zFytsCTRrbwbyT2QPgUY7KViTBdV5hiCVIx3od8xtzU1OR1dXXe0dGRPNbR0eF1dXXe1NQ0av3Uuon6TU1NybLUOqn75eXlyeOJY4ny1LqZ9BUm2cSZyzWlu69jnVss92+48RJ73mOPtHiPPRA+ZhZ0CJMmLD+XzCw0sQSpWMdavv7uSktLJUlnz57VlClTJEnnz59XeXm5zEwDAwMj6qfWTdSvqKhItlNRUZGskyg7e/aspk6dqv7+fk2ZMiXZjiRVVFRoYGAgWTfR53h9DY8rSNnEmcs1Jc4Z676OdW6x3L/heI89AETQWDM2xbwhnIIeF0GOo3nz5mnOnDnas2dP8tiePXtUW1urefPmjVo/tW6i/rx585JlqXVS98vLy5PHE8cS5al1M+krTLKJM5drSndfxzq3WO5fVoL+x8cW/o2lOED4qAiXR2QiTNcVpliCVIz3IZ8xs8Z+4lhjn19ijT3bRDYSeyB8ijHZykSYritMsQSpGO9DvmPetGmT19TUuCSX5DU1NWkTzaamJi8pKfGmpqYRyXhTU5ObmZeXl7uZDamTem5NTY3X1NSM2k4mfYVJNnHmck3p7ms++wraeIk9a+yRFmvsARRKmNa1hymWIHEfgHAZb409H1AFAAiVMD2sGaZYglJVVRV0CAAyRGIPAAgNZoYBIHe8FQcAAACIABJ7AAAAIAJI7AEAAIAIILEHAAAAIoDEHgAAAIgAEnsAAAAgAkjsAQAAgAggsQcAAAAigA+oAgDk3Zo1a9TX1xd0GKEXi8X0wAMPBB0GgIggsQcA5F1fX58efPDBQGNYtWpV4DGks2rVqqBDGFdnZ6fa29vV3d2t6upqtba2avHixROqP16d1LLS0lJduHBBs2bNGlLn8ccf1969e3XhwgWVlZXpiiuu0Ouvv55xjBO5vlwUog8ggcQeAPKgGJJIIBudnZ1qa2vT6dOn9e1vf1tdXV3asGGDJI2amCbqr1y5UnPnzh21/nh1JKmtrU2LFy/WuXPn9KEPfUg7d+7UggUL1NbWJkl6+eWXtXv3bt14441aunSpNm7cqM7OTl199dX6yle+kjbGbOOdqEL0AaRijT0AABihvb1dK1eulCSVlpaqsbFRK1euVHt7+7j1Gxsbx6w/Xp1E2cGDB3XrrbeqpaUluZ+os3fvXt14441qaWnR1KlT9dprr2nJkiX62c9+llGM2cY7UYXoA0jFjD0A5EnYl1UgnMI8br75zW8O2Z87d666u7tHrdvd3a25c+eOWz9dncTXiTqp+93d3XJ3LV26dEh7a9as0e7duzOKMdt4J6oQfQCpSOwBIE9YivO2MCerYRPWcfO1r31NK1asGJLcd3V1qbq6etT61dXV6urqUmNj45j109VJfJ2ok7pfXV2tkydPateuXWppaUm29/TTT6usrGzMPseSSbwTVYg+gFQsxQEAACO0trYm14MPDAzoyJEj2rBhg1pbW8etf+TIkTHrj1cnUbZgwQI99thj2rFjR3I/Uefaa6/V008/rR07dqi/v181NTXavXu3rrzyyoxizDbeiSpEH0AqZuwBAMAIiYc7H3nkEX3xi19UdXW1li9fPuZDn4njW7ZsSb4BZnj9TOq0t7erp6dHbW1tunDhgg4ePJisk6jX1tamrVu3qqysTPPmzdPJkyczijHbeCeqEH0Aqczdg44BIdfc3Oz79u0LOgwARSQMbwkKQwzpFEOMAMLFzPa7e/NoZczYAwAmRRjW2YchhvHEYrGgQwAQIZFL7M3sX9z90qDjyISZ3Supwt3/MuXYQkmb3X1envu6TVKzu6/OZ7sAMBpmoQGg8Hh4NlibJX1m2LHPxo8DAAAAGYtkYm9ml5rZj8zsp2Z2yMw+ET9eZ2Y/N7ONZvaSmT1pZrF42T1m1mlmh83sITOz+PHnzOwbZvaPZnbUzJbEj5ea2f3xc/7ZzP59/PgsM9tlZgfibSXqX2dmL8RjesLMLnX3o5J6zOz3UsJfIWmzmS00sx/H237KzKrMbKaZ7Y+3t8DM3MzmxPd/aWYxM5thZv8zHlenmV07yv25OR7bQTPbNWl/EQAAACiYSCb2ks5K+qS7v1/ShyWtTSTqkholPRhf6vKGpMQCzO+4+2J3ny/pHZKuT2mvzN1/V9KfSbo3fuwOSb3uvljSYkmfN7N6SX8o6QfuvlDSAkkHzGy6pK9KaonHtE/Sl+LtbNbgLL3M7AOSzrj7LyQ9Kukv3P1qSYck3evuJyRVmNllkpbE21liZrWSTrh7n6RvSvrreFyfkvS3o9yfeyR9zN0XSFqe+W0FAABAWEVujX2cSfq6mS2V9Jakd0n61/GyV919b/zrDZK+KOkBSR82s/8oKSZpmqQXJW2L19sa/3O/pLr419dJutrMPh3fr5R0haROSd8zsymSnnb3A2a2TNKVkvbGf7+YKumF+HmPS3rezP6D4stwzKxS0jvdfWe8zt9LeiL+9fOSrpW0VNLXJbXGrzfxsXstkq58+/cYXWZmw5852CtpvZltSbm2oTfQ7AuSviBJc+bMGa0KAAAAQiSqif0tkmZIWuTu583sV5Iq4mXD3+/pZlYh6UENPlz6qpn9VUp9SToX/3NAb98zk3SXu/9geOfxXyg+rsHk+b9J6pH0Q3f/3PC68f6OSVqmwRn2D6a5tl0anK2vlfS/JP1F/Jq+Hy8vkfQBdz87LKbUPu+ML//5uKT9ZrbI3U8Pi+shSQ9Jg6+7TBMTAAAAAhbVpTiVGlyact7MPqzBJDhhjpklkuc/lLRHbyfxp+Kz259Wej+Q9CfxmXmZWYOZXRJfFvN/3f1hDS6Deb+kH0u61szmxuteYmYNKW1tlvTXkl5299fcvVeDa++XxMtvlZSYvd8taaWkX7j7W5LOSPqD+HVI0nZJdyUajr9lZwgze4+7/8Td75F0UtLsDK4XAAAAIRapGXszK9Pg7PpGSdvM7JAG16H/PKXaEUl/ambfk/QzSX/j7n1m9rCkw5K6NbicJp2/1eCynJ/G1++flHSjpA9J+nMzOy/pXyT9kbufjL9ucrOZlcfP/6qko/Gvn5D0LaUk5JL+WNK6+MO9L0u6XZLc/Vfx/hIPve6RVOPuPfH9L0r6rpn9swb/fndJunNY7Peb2RUa/F+HH0k6mMH1AgAAIMQi9cmzZrZA0sPxB11HK6+T9Ez8AVlkiE+eBQAACIeL4pNnzexODc5W/1nAoQAAgAn4xje+obNnz6avCITEvffem75SAUQmsXf3dZLWpanzK0nM1gMAEGJnz54NTaIEpHPfffcFHUJSVB+eBYCLRph+qAAAgkNiDwAAAERAZJbiAMDFjFl7AACJPQBEAOuRESX8ogrkhqU4AAAAQASQ2AMAAAARQGIPAEWOZTgAAIk19gAAIIRYZw9kj8QeAACECv8LBeSGpTgAAABABJDYAwAAABFAYg8AAABEAIk9AAAAEAEk9gAAAEAEkNgDAAAAEUBiDwAAAEQAiT0AAAAQAST2AAAAQI527twZdAhJfPIsAAAhc+LECR0/flx9fX2KxWKqra3VzJkzgw4rL3K9tkLekyjff0QbiT0AACFy4sQJHTt2TA0NDaqsrFRvb6+OHj0qSUWfXOZ6bYW8J1G+/4g+luIAABAix48fV0NDg6qqqlRSUqKqqio1NDTo+PHjQYc2YbleWyHvSZTvP6KPxB4AgBDp6+tTZWXlkGOVlZXq6+sLKKL8yfXaCnlPonz/EX0k9gAAhEgsFlNvb++QY729vYrFYgFFlD+5Xlsh70mU7z+ij8QeAIAQqa2t1dGjR9XT06O33npLPT09Onr0qGpra4MObcJyvbZC3pMo339EHw/PAgAQIokHNLu6upJvZamvr4/Eg5u5Xlsh70mU7z+ij8QeAICQmTlzZmQTyVyvrZD3JMr3H9HGUhwAAAAgAkjsAQAAgBwtW7Ys6BCSSOwBAACACCCxBwAAACKAh2eR1unTp7V+/fohx5qamrR48WKdP39eGzduHHHOwoULtXDhQvX19WnLli0jypubmzV//nz19vbqqaeeGlH+wQ9+UI2NjTp16pSeeeaZEeVLly7Vu9/9bnV3d6u9vX1E+Uc/+lHNnj1br776qn70ox+NKG9tbVV1dbVefvll7dq1a0T59ddfr+nTp+vIkSN64YUXRpR/8pOfVGVlpQ4fPqx9+/aNKF+xYoVisZgOHDigAwcOjCi/5ZZbNGXKFHV2durFF18cUX7bbbdJkp5//vnkR5knTJkyRbfccoskaefOnTp27NiQ8lgsphUrVkiSduzYoddee21I+WWXXaabbrpJktTe3q7u7u4h5ZdffrluuOEGSdK2bdt0+vTpIeXV1dVqbW2VJG3dulVvvPHGkPKamhq1tLRIkrZs2TLiQ13q6+uT/225ceNGnT9/fkh5Q0ODrrnmGkkaMe4kxh5jj7HH2GPsDcfYu3jH3nDM2AMAAAARYO4edAwIuebmZh/tN2QAAAAUlpntd/fm0cqYsQcAAAAigMQeAAAAiAASewAAACACeCsOAADDTJs2TT09PUGHMSmqqqp05syZoMMAMAmYsQcAYJienh65e142SXlrKx9bWH9h2bx5s+bPn6+SkhJVVFSopKRE8+fP1+bNm0PRdqKN0tLSjM8d7Zxc2pkMkx1HmK89X+666y5VVFTIzFRRUaG77ror6JDC9c2GLZzbokWLHAja4LcroDDyOd7CNnbDFo/7YEz19fV+9913e11dna9duza5X19f75s2bcq57U2bNk247UQbHR0d3t/f7x0dHWnPHe2cGTNm+IwZM7JqZzLkcj0TbT8s154vq1ev9rKyMl+7dq2/+eabvnbtWi8rK/PVq1dPet+S9vkYOVvgSSNb+DcSe4RBGJMRRBeJfWFJ8o6ODm9qavKOjg539yH7TU1NObed2kaubaeem5Du3NHOqaur87q6uqzamQy5XM9E2w/LtedLeXm5r127dsixtWvXenl5+aT3PV5iz3vskRbvsUcYmFnQIeAik6+fj2aWt7byIaz/lvr7+1VRUaGzZ89qypQpOn/+fHK/oqJCAwMDObVbWlqabCPXthNtTJkyJXks0cZY5452TklJicxsyDnp2pkMuVzPRNsPy7Xni5npzTffVCwWSx7r6+vTJZdcMun/3nmPPYBIGGuGgo0t31vUBX1/R7vfe/bs0bx587Rnz54R+/Pmzcv5WlPbyLXt1HMT0p072jm1tbWaM2dOVu1MhlyuZ6Lth+Xa86W8vFzr1q0bcmzdunUqLy8PKKK4oP8xs4V/YykOwkAhXD6A6MrneAvb2A1bPO7OGnvW2Bcd1tizFe1GYo8wCGMygugisS8sSb5p0yZvampyM/Py8nI3M29qaspL4pePthNtlJSUZHzuaOfk0s5kmOw4wnzt+bJ69WovLy93SV5eXl6QpN7dWWOPiWGNPYCLTT7XxYdxjX2Y4gGQnfHW2PMBVQAAjCKfD5mG6YHVqqqqoEMAMElI7AEAGIYZbQDFiLfiAAAAABFAYg8AAABEAIk9AAAAEAEk9gAAAEAEkNgDAAAAEUBiDwAAAEQAiT0AAAAQAST2AAAAQATwAVUAcJFYs2aN+vr6gg4jY7FYTA888EDQYQBA0SCxB4CLRF9fnx588MGC9bdq1aoJ9bdq1ao8RpO7zs5Otbe36ze/+Y3Kyso0MDCg6upqtba2avHixUPqdHd3jyjLpO3u7m5VVlZKknp7e1VaWqoLFy5o1qxZam1tlaSM2s8k1nRxZBN/poqt/cmOd6J9FTI+FBcSewBZm2jCBoRdYox3dnaqra1NixcvVn9/v5YtW6bnnntOCxYsUFtbW7J+W1ubVq5cqblz56qrq0sbNmyQpLTJdOK8119/XU899ZT6+/sVi8X0sY99TDt37tSCBQv0xBNPSJLuuOOOcdvPJNaxfhnIJf5MFVv7kx3vRPsqZHwoPqyxBwBgDO3t7Vq5cqUOHjyolStXqqWlRbfeemtyv729PVmnsbFRpaWlamxsTJZl0nZjY6O2b9+u22+/XZdcconKy8vV0tKS7Le8vFxTp05N234msaaLI5v4s72HxdL+ZMc70b4KGR+KDzP2AHISlmUSiLagx1l3d7fmzp2b/FPSkP3u7u7ksVSpZenaTv36zJkzcvcRbSSOjdd+prGOF0c28Weq2Nqf7Hgn2lch40PxIbEHkBOW4hSfoJPkXAQ1zhL3qrq6Wl1dXck/Gxsbh+xXV1dLUrIsIbVsLKltJr6eNm1aMolPtNHf3z8isR+t/UxjHS+ObOLPVLG1P9nxTrSvQsaH4sNSHAAAxtDa2qoNGzZowYIF2rBhg3bs2KHHHnssud/a2pqsc+TIEQ0MDOjIkSPJskzaPnLkiK677jo98sgjevPNN3Xu3Dnt2LEj2e+5c+fU39+ftv1MYk0XRzbxZ3sPi6X9yY53on0VMj4UH2bsAQAYQ+JhxPb2dp0+fVptbW0aGBjQwYMHtXz58iEPK27ZsiX5lpLhZeO1nTivsrJSFRUV6u3tVVtbmy5cuKCDBw/q5ptvzqj9bGIdL45M489UsbU/2fFOtK9CxofiY8P/ew8Yrrm52fft2xd0GAAmqNBvM8rH6y5Z8gUAQ5nZfndvHq2MGXsAuIgUep39RPqLxWJ5jAQAoo/EPo/MrE7SM+4+f9jx/yxpl7vvMLPnJK1x931m9itJze5+aoL9ro/3+2Rq+xNpE0D0MPsNANFGYl8A7n5P0DEAAAAg2ngrTv6VmtnDZvaimW03s3eY2Xoz+3QmJ5vZe83sH1P268zsUPzre8ys08wOm9lDZmZp2rrOzF4ws5+a2RNmdqmZfcTMnk6p82/N7KkcrxUAAAAhQWKff1dI+q67N0l6XdKnsjnZ3X8uaaqZ1ccPfUbS4/Gvv+Pui+NLfd4h6fqx2jGz6ZK+KqnF3d8vaZ+kL0n6B0nvNbMZ8aq3S/peNjECAAAgfEjs8++Yux+If71fUl0ObWzRYEIvDU3sP2xmP4nP4H9EUtM4bXxA0pWS9prZAUl/LKnWB1+D9JiklWb2TkkflPTs8JPN7Atmts/M9p08eTKHSwAAAEAhscY+/86lfD2gwZn1cZnZn0r6fHz3DzSYyD9hZlslubv/wswqJD2owYdtXzWzv5JUMV6zkn7o7p8bpewRSdsknZX0hLtfGF7B3R+S9JA0+LrLdNcAAACAYDFjHwLu/l13Xxjffu3uv9TgLwX/SW/P1ieS+FNmdqmkdGv2fyzpWjObK0lmdomZNcT7+7WkX2twqc4jeb4cAAAABIAZ+/B6XNL9kuolyd1fN7OHJR2W1C2pc7yT3f2kmd0mabOZlccPf1XS0fjXGyXNcPeXJiF2AAAAFBifPHuRMrPvSPond/+7dHX55FkAAIBwGO+TZ1mKcxEys/2Srpa0IehYAAAAitl9990XdAhJLMW5CLn7oqBjAABJOnTokHbv3q1Tp05p+vTpWrJkia666qqgwwKAokRiDwAIxKFDh9TR0aHly5drzpw5euWVV9TW1iZJJPcAkAOW4gAAArF7924tX75c9fX1Ki0tVX19vZYvX67du3cHHRoAFCUSewBAIE6dOqU5c+YMOTZnzhydOnUqoIgAoLiR2AMAAjF9+nS98sorQ4698sormj59ekARAUBxI7EHAARiyZIlamtr07FjxzQwMKBjx46pra1NS5YsCTo0AChKPDwLAAhE4gHZZ599NvlWnI985CM8OAsAOSKxBwAE5qqrriKRB4A8YSkOAAAAEAEk9gAAAECO7r333qBDSCKxBwAAACKAxB4AAACIABJ7AAAAIAJI7AEAAIAIILEHAAAAIoDEHgAAAIgAEnsAAAAgAkjsAQAAgAggsQcAAABytHPnzqBDSCoLOgAAAACgGJw4cULHjx9XX1+fYrGYamtrgw5pCBJ7AAAAII0TJ07o2LFjamhoUGVlpXp7e3X06NGgwxqCpTgAAABAGsePH1dDQ4OqqqpUUlKiqqoqNTQ0BB3WECT2AAAAQBp9fX2qrKwccmz4ftBI7AEAAIA0YrGYent7hxwbvh80EnsAAAAgjdraWh09elQ9PT1666231NPTE7o19jw8CwAAAKQxc+ZMSVJXV1fyrTj19fV66aWXAo7sbST2AAAAQAZmzpyZTPATwpTYsxQHAAAAiAASewAAACBHy5YtCzqEJBJ7AAAAIAJI7AEAAIAIILEHAAAAIsDcPegYEHJmdlLS8UnuplLSZH3KQz7azqWNTM/JpF66OmOVj3V8uqRTGcQWFMbDxOowHgrbdrZtZFN/ouMhlzLGQ2HbYDxMTJjHw2T9rKh19xmjlrg7G1vgm6SHwtx2Lm1kek4m9dLVGat8nOP7gv47ZzwwHi7W8ZBN/YmOh1zKGA+MB8ZDftqezJ8VY20sxUFYbAt527m0kek5mdRLV2es8sm8r5OJ8TCxOoyHwradbRvZ1J/oeMi1LMwYD7nXYTwUtu3J/FkxKpbiABchM9vn7s1Bx4FwYDwgFeMBqRgPxYUZe+Di9FDQASBUGA9IxXhAKsZDEWHGHgAAAIgAZuwBAACACCCxBwAAACKAxB4AAACIABJ7ADKzS8zs783sYTO7Jeh4ECwze7eZ/Z2ZPRl0LAiemd0Y/97wuJldF3Q8CJaZzTOzdWb2pJn9SdDxYCgSeyCizOx7ZnbCzA4PO95qZkfMrMvMvhw/fJOkJ93985KWFzxYTLpsxoO7v+zudwQTKQohy/HwdPx7w52SPhNEvJhcWY6Hl9z9TkkrJF0bRLwYG4k9EF3rJbWmHjCzUknflfT7kq6U9Dkzu1JSjaRX49UGChgjCme9Mh8PiL71yn48fDVejuhZryzGg5ktl/R9Sf+7sGEiHRJ7IKLcfZekM8MO/66krviMbL+k/yHpE5Je02ByL/F9IZKyHA+IuGzGgw36hqRn3f2nhY4Vky/b7w/u3ubuvy+JpZshww9w4OLyLr09My8NJvTvkrRV0qfM7G9UvB8rjuyNOh7M7HIzWyfpfWb2l8GEhgCM9f3hLkktkj5tZncGERgCMdb3hw+Z2bfM7L+LGfvQKQs6AADBc/c3Jd0edBwIB3c/rcH11IDc/VuSvhV0HAgHd39O0nMBh4ExMGMPXFz+j6TZKfs18WO4ODEekIrxgFSMhyJEYg9cXDolXWFm9WY2VdJnJbUFHBOCw3hAKsYDUjEeihCJPRBRZrZZ0guSGs3sNTO7w90vSFot6QeSXpK0xd1fDDJOFAbjAakYD0jFeIgOc/egYwAAAAAwQczYAwAAABFAYg8AAABEAIk9AAAAEAEk9gAAAEAEkNgDAAAAEUBiDwAAAEQAiT0AAAAQAST2AIDQMrN3mtmqlP3fMbMnJ6mvG83snnHKrzKz9ZPRNwDkAx9QBQAILTOrk/SMu88vQF/PS1ru7qfGqbND0r9z91cmOx4AyBYz9gCAMPuvkt5jZgfM7H4zqzOzw5JkZreZ2dNm9kMz+5WZrTazL5nZP5nZj81sWrzee8ys3cz2m9luM3vv8E7MrEHSuURSb2Y3m9lhMztoZrtSqm6T9NnJv2wAyB6JPQAgzL4s6ZfuvtDd/3yU8vmSbpK0WNJ/kdTn7u+T9IKkP4rXeUjSXe6+SNIaSQ+O0s61kn6asn+PpI+5+wJJy1OO75O0ZALXAwCTpizoAAAAmIB/cPffSvqtmfVqcEZdkg5JutrMLpV0jaQnzCxxTvko7cySdDJlf6+k9Wa2RdLWlOMnJP1OHuMHgLwhsQcAFLNzKV+/lbL/lgZ/xpVIet3dF6Zp5/9JqkzsuPudZvZ7kj4uab+ZLXL305Iq4nUBIHRYigMACLPfSvpXuZ7s7m9IOmZmN0uSDVowStWXJM1N7JjZe9z9J+5+jwZn8mfHixokHc41HgCYTCT2AIDQis+S740/yHp/js3cIukOMzso6UVJnxilzi5J77O31+vcb2aH4g/qPi/pYPz4hyV9P8c4AGBS8bpLAAAkmdk3JW1z9x1jlJdL2inp37j7hYIGBwAZYMYeAIBBX5cUG6d8jqQvk9QDCCtm7AEAAIAIYMYeAAAAiAASewAAACACSOwBAACACCCxBwAAACKAxB4AAACIgP8PdGg1LT6iwMsAAAAASUVORK5CYII=\n",
      "text/plain": [
       "<Figure size 792x1008 with 1 Axes>"
      ]
     },
     "metadata": {
      "needs_background": "light"
     },
     "output_type": "display_data"
    }
   ],
   "source": [
    "clrs = plt.rcParams[\"axes.prop_cycle\"].by_key()[\"color\"]\n",
    "# change to black and white for IEEE\n",
    "clrs = [\"black\", \"dimgray\", \"gray\", \"silver\", \"lightgrey\"]\n",
    "\n",
    "def set_box_color(bp, color):\n",
    "    plt.setp(bp[\"boxes\"], color=color)\n",
    "    plt.setp(bp[\"whiskers\"], color=color)\n",
    "    plt.setp(bp[\"caps\"], color=color)\n",
    "    plt.setp(bp[\"medians\"], color=color)\n",
    "    plt.setp(bp[\"fliers\"], markeredgecolor=color)\n",
    "\n",
    "sig_timeses = []\n",
    "lin_timeses = []\n",
    "z3_timeses = []\n",
    "reluval_timeses = []\n",
    "for tag in [\"sigmoid\", \"linear\", \"z3\", \"reluval\"]:\n",
    "    print(tag)\n",
    "    print(\"-\"*len(tag))\n",
    "    for name in dataset_names:\n",
    "        perturbation, dist, exact, times = pickle.load(open(\"results/map_\" + name + \"_\" + tag + \".pkl\", \"rb\"))\n",
    "        exact[times > timeout] = False\n",
    "        times[times > timeout] = timeout\n",
    "        if tag == \"sigmoid\": sig_timeses.append(times)\n",
    "        if tag == \"linear\": lin_timeses.append(times)\n",
    "        if tag == \"z3\": z3_timeses.append(times)\n",
    "        if tag == \"reluval\": reluval_timeses.append(times)\n",
    "        print(name)\n",
    "        print(\"%d within timeout; %d within tolerance\" % (np.sum(times < timeout), np.sum(exact)))\n",
    "        print(\"mean %.2f; standard deviation %.2f\" % (np.mean(times), np.std(times)))\n",
    "        print(\"quartiles:\\t\" + \"\\t\".join([\"%.2f\"%t for t in np.quantile(times, [0, 0.25, 0.5, 0.75, 1])]))\n",
    "        print(\"excluding Z3 fails and timeouts\")\n",
    "        _, _, z3exact, z3times = pickle.load(open(\"results/map_\" + name + \"_z3.pkl\", \"rb\"))\n",
    "        z3exact[z3times > timeout] = False\n",
    "        times = times[z3exact]\n",
    "        if times.shape[0] == 0:\n",
    "            print(\"all Z3 cases failed or timed out\")\n",
    "        else:\n",
    "            print(\"mean %.2f; standard deviation %.2f\" % (np.mean(times), np.std(times)))\n",
    "            print(\"quartiles:\\t\" + \"\\t\".join([\"%.2f\"%t for t in np.quantile(times, [0, 0.25, 0.5, 0.75, 1])]))\n",
    "        print(\"\")\n",
    "plt.figure(figsize=(11,14))\n",
    "set_box_color(plt.boxplot(np.array(list(reversed(sig_timeses))).T, positions=[4*i+3 for i in range(len(dataset_names))], vert=False), clrs[0])\n",
    "set_box_color(plt.boxplot(np.array(list(reversed(lin_timeses))).T, positions=[4*i+2 for i in range(len(dataset_names))], vert=False), clrs[1])\n",
    "set_box_color(plt.boxplot(np.array(list(reversed(reluval_timeses ))).T, positions=[4*i+1 for i in range(len(dataset_names))], vert=False), clrs[2])\n",
    "set_box_color(plt.boxplot(np.array(list(reversed(z3_timeses))).T, positions=[4*i+0 for i in range(len(dataset_names))], vert=False), clrs[3])\n",
    "for i in range(len(dataset_names)): plt.axhline(4*i+3.5, c=\"gray\", ls=\"--\")\n",
    "plt.plot([], c=clrs[0], label=\"Ours (sigmoid)\")\n",
    "plt.plot([], c=clrs[1], label=\"Ours (linear)\")\n",
    "plt.plot([], c=clrs[2], label=\"ReluVal-based (linear)\")\n",
    "plt.plot([], c=clrs[3], label=\"Z3 (linear)\")\n",
    "plt.legend(loc=\"upper left\")\n",
    "plt.yticks([4*i+1.5 for i in range(len(dataset_names))], labels=np.array(list(reversed(dataset_names))))\n",
    "plt.xlabel(\"time (s)\")\n",
    "plt.xscale(\"log\")\n",
    "plt.show()"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "cc972def",
   "metadata": {
    "tags": []
   },
   "source": [
    "# Global Adversarial Robustness"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "94fd3a48",
   "metadata": {},
   "outputs": [],
   "source": [
    "delta = [1e-3, 1e-2, 1e-1, 1e0]\n",
    "epsilon = [0.2, 0.4, 0.6, 0.8]\n",
    "for name in dataset_names:\n",
    "    f = load_model(name + \"_sigmoid\")\n",
    "    results = global_robustness(f, delta, epsilon, timeout=timeout)\n",
    "    pickle.dump(results, open(\"results/gar_\" + name + \"_sigmoid.pkl\", \"wb\"))\n",
    "    print(name)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "ecc3d04a",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "shuttle\n",
      "delta\tepsilon\trobust\ttime (s)\n",
      "0.001\t0.2\tTrue\t1858\n",
      "0.001\t0.4\tTrue\t50\n",
      "0.001\t0.6\tTrue\t10\n",
      "0.001\t0.8\tTrue\t5\n",
      "0.01\t0.2\tFalse\t12\n",
      "0.01\t0.4\tFalse\t170\n",
      "0.01\t0.6\tTrue\t174\n",
      "0.01\t0.8\tTrue\t13\n",
      "0.1\t0.2\tFalse\t4\n",
      "0.1\t0.4\tFalse\t4\n",
      "0.1\t0.6\tFalse\t6\n",
      "0.1\t0.8\tFalse\t10\n",
      "1.0\t0.2\tFalse\t5\n",
      "1.0\t0.4\tFalse\t7\n",
      "1.0\t0.6\tFalse\t14\n",
      "1.0\t0.8\tFalse\t24\n",
      "\n",
      "sylva_agnostic\n",
      "delta\tepsilon\trobust\ttime (s)\n",
      "0.001\t0.2\tNone\t3604\n",
      "0.001\t0.4\tNone\t3604\n",
      "0.001\t0.6\tTrue\t909\n",
      "0.001\t0.8\tTrue\t56\n",
      "0.01\t0.2\tNone\t3602\n",
      "0.01\t0.4\tNone\t3604\n",
      "0.01\t0.6\tTrue\t1492\n",
      "0.01\t0.8\tTrue\t45\n",
      "0.1\t0.2\tFalse\t202\n",
      "0.1\t0.4\tFalse\t852\n",
      "0.1\t0.6\tNone\t3604\n",
      "0.1\t0.8\tNone\t3601\n",
      "1.0\t0.2\tFalse\t193\n",
      "1.0\t0.4\tFalse\t253\n",
      "1.0\t0.6\tFalse\t419\n",
      "1.0\t0.8\tFalse\t765\n",
      "\n",
      "wall-robot-navigation\n",
      "delta\tepsilon\trobust\ttime (s)\n",
      "0.001\t0.2\tNone\t3601\n",
      "0.001\t0.4\tNone\t3601\n",
      "0.001\t0.6\tNone\t3602\n",
      "0.001\t0.8\tTrue\t585\n",
      "0.01\t0.2\tNone\t3602\n",
      "0.01\t0.4\tNone\t3602\n",
      "0.01\t0.6\tNone\t3602\n",
      "0.01\t0.8\tNone\t3602\n",
      "0.1\t0.2\tNone\t3602\n",
      "0.1\t0.4\tNone\t3602\n",
      "0.1\t0.6\tNone\t3602\n",
      "0.1\t0.8\tNone\t3602\n",
      "1.0\t0.2\tFalse\t410\n",
      "1.0\t0.4\tFalse\t410\n",
      "1.0\t0.6\tFalse\t427\n",
      "1.0\t0.8\tFalse\t457\n",
      "\n",
      "banknote-authentication\n",
      "delta\tepsilon\trobust\ttime (s)\n",
      "0.001\t0.2\tNone\t3603\n",
      "0.001\t0.4\tTrue\t1023\n",
      "0.001\t0.6\tTrue\t202\n",
      "0.001\t0.8\tTrue\t57\n",
      "0.01\t0.2\tNone\t3603\n",
      "0.01\t0.4\tTrue\t1253\n",
      "0.01\t0.6\tTrue\t229\n",
      "0.01\t0.8\tTrue\t57\n",
      "0.1\t0.2\tNone\t3602\n",
      "0.1\t0.4\tNone\t3603\n",
      "0.1\t0.6\tTrue\t1718\n",
      "0.1\t0.8\tTrue\t156\n",
      "1.0\t0.2\tFalse\t12\n",
      "1.0\t0.4\tFalse\t12\n",
      "1.0\t0.6\tFalse\t12\n",
      "1.0\t0.8\tFalse\t40\n",
      "\n",
      "helena\n",
      "delta\tepsilon\trobust\ttime (s)\n",
      "0.001\t0.2\tTrue\t85\n",
      "0.001\t0.4\tTrue\t68\n",
      "0.001\t0.6\tTrue\t68\n",
      "0.001\t0.8\tTrue\t68\n",
      "0.01\t0.2\tFalse\t71\n",
      "0.01\t0.4\tTrue\t67\n",
      "0.01\t0.6\tTrue\t67\n",
      "0.01\t0.8\tTrue\t70\n",
      "0.1\t0.2\tFalse\t69\n",
      "0.1\t0.4\tTrue\t67\n",
      "0.1\t0.6\tTrue\t66\n",
      "0.1\t0.8\tTrue\t66\n",
      "1.0\t0.2\tFalse\t69\n",
      "1.0\t0.4\tTrue\t66\n",
      "1.0\t0.6\tTrue\t67\n",
      "1.0\t0.8\tTrue\t67\n",
      "\n",
      "MagicTelescope\n",
      "delta\tepsilon\trobust\ttime (s)\n",
      "0.001\t0.2\tNone\t3601\n",
      "0.001\t0.4\tNone\t3601\n",
      "0.001\t0.6\tTrue\t3055\n",
      "0.001\t0.8\tTrue\t22\n",
      "0.01\t0.2\tNone\t3602\n",
      "0.01\t0.4\tNone\t3601\n",
      "0.01\t0.6\tNone\t6280\n",
      "0.01\t0.8\tTrue\t26\n",
      "0.1\t0.2\tNone\t3602\n",
      "0.1\t0.4\tNone\t3602\n",
      "0.1\t0.6\tNone\t3602\n",
      "0.1\t0.8\tTrue\t2340\n",
      "1.0\t0.2\tFalse\t135\n",
      "1.0\t0.4\tFalse\t163\n",
      "1.0\t0.6\tFalse\t290\n",
      "1.0\t0.8\tFalse\t539\n",
      "\n",
      "satimage\n",
      "delta\tepsilon\trobust\ttime (s)\n",
      "0.001\t0.2\tNone\t3603\n",
      "0.001\t0.4\tNone\t3603\n",
      "0.001\t0.6\tNone\t5124\n",
      "0.001\t0.8\tTrue\t350\n",
      "0.01\t0.2\tNone\t3601\n",
      "0.01\t0.4\tNone\t3604\n",
      "0.01\t0.6\tNone\t3601\n",
      "0.01\t0.8\tTrue\t550\n",
      "0.1\t0.2\tFalse\t570\n",
      "0.1\t0.4\tFalse\t2905\n",
      "0.1\t0.6\tNone\t3603\n",
      "0.1\t0.8\tNone\t3601\n",
      "1.0\t0.2\tFalse\t155\n",
      "1.0\t0.4\tFalse\t180\n",
      "1.0\t0.6\tFalse\t264\n",
      "1.0\t0.8\tFalse\t391\n",
      "\n",
      "texture\n",
      "delta\tepsilon\trobust\ttime (s)\n",
      "0.001\t0.2\tNone\t3606\n",
      "0.001\t0.4\tNone\t3601\n",
      "0.001\t0.6\tNone\t6499\n",
      "0.001\t0.8\tTrue\t1029\n",
      "0.01\t0.2\tNone\t3605\n",
      "0.01\t0.4\tNone\t3603\n",
      "0.01\t0.6\tNone\t3606\n",
      "0.01\t0.8\tTrue\t1379\n",
      "0.1\t0.2\tNone\t3603\n",
      "0.1\t0.4\tNone\t3602\n",
      "0.1\t0.6\tNone\t3602\n",
      "0.1\t0.8\tNone\t3604\n",
      "1.0\t0.2\tFalse\t302\n",
      "1.0\t0.4\tFalse\t366\n",
      "1.0\t0.6\tFalse\t454\n",
      "1.0\t0.8\tFalse\t553\n",
      "\n",
      "JapaneseVowels\n",
      "delta\tepsilon\trobust\ttime (s)\n",
      "0.001\t0.2\tNone\t3603\n",
      "0.001\t0.4\tNone\t3601\n",
      "0.001\t0.6\tNone\t4675\n",
      "0.001\t0.8\tTrue\t1730\n",
      "0.01\t0.2\tNone\t3601\n",
      "0.01\t0.4\tNone\t3601\n",
      "0.01\t0.6\tNone\t3602\n",
      "0.01\t0.8\tNone\t7128\n",
      "0.1\t0.2\tFalse\t182\n",
      "0.1\t0.4\tFalse\t213\n",
      "0.1\t0.6\tFalse\t274\n",
      "0.1\t0.8\tFalse\t357\n",
      "1.0\t0.2\tFalse\t181\n",
      "1.0\t0.4\tFalse\t217\n",
      "1.0\t0.6\tFalse\t273\n",
      "1.0\t0.8\tFalse\t348\n",
      "\n",
      "hill-valley\n",
      "delta\tepsilon\trobust\ttime (s)\n",
      "0.001\t0.2\tNone\t3618\n",
      "0.001\t0.4\tNone\t3618\n",
      "0.001\t0.6\tNone\t3606\n",
      "0.001\t0.8\tNone\t3698\n",
      "0.01\t0.2\tNone\t3611\n",
      "0.01\t0.4\tNone\t3618\n",
      "0.01\t0.6\tNone\t3609\n",
      "0.01\t0.8\tNone\t3605\n",
      "0.1\t0.2\tNone\t3604\n",
      "0.1\t0.4\tNone\t3604\n",
      "0.1\t0.6\tNone\t3621\n",
      "0.1\t0.8\tNone\t3618\n",
      "1.0\t0.2\tFalse\t1161\n",
      "1.0\t0.4\tFalse\t1609\n",
      "1.0\t0.6\tFalse\t2162\n",
      "1.0\t0.8\tFalse\t3046\n",
      "\n"
     ]
    }
   ],
   "source": [
    "for name in dataset_names:\n",
    "    results = pickle.load(open(\"results/gar_\" + name + \"_sigmoid.pkl\", \"rb\"))\n",
    "    print(name)\n",
    "    print(\"delta\\tepsilon\\trobust\\ttime (s)\")\n",
    "    for res in results:\n",
    "        print(\"\\t\".join((str(res[0]), str(res[1]), str(res[2]), \"%.0f\"%res[-1])))\n",
    "    print(\"\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "d97c1d44-525f-446b-955d-56472803096a",
   "metadata": {},
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3",
   "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.9.5"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}