{
"cells": [
{
"cell_type": "markdown",
"id": "7e796657",
"metadata": {},
"source": [
"# Step Two: Model Checking\n",
"After creating and inspecting the model in the previous *Step One*, we will now apply model checking to the Orchard MDP. While, strictly speaking, model checking asks whether a property holds on an MDP, we will see that modern probabilistic model checking tools, including Storm, can actually go beyond such queries.\n",
"The section is structured based on the type of properties that we consider."
]
},
{
"cell_type": "markdown",
"id": "9968a722",
"metadata": {},
"source": [
"## Preparation\n",
"We start be loading the models from the previous notebook.\n",
"The complete Stormvogel model for the Orchard game is given in `orchard/orchard_game_stormvogel.py`.\n",
"The Prism specification is given in `orchard/orchard_stormvogel.pm`.\n",
"These models are built using functions in `orchard/orchard_builder.py`."
]
},
{
"cell_type": "code",
"execution_count": 1,
"id": "342e90e0",
"metadata": {
"execution": {
"iopub.execute_input": "2026-03-26T10:39:36.136219Z",
"iopub.status.busy": "2026-03-26T10:39:36.135967Z",
"iopub.status.idle": "2026-03-26T10:39:36.366512Z",
"shell.execute_reply": "2026-03-26T10:39:36.365963Z"
}
},
"outputs": [],
"source": [
"# Import stormvogel and prism models from the previous step\n",
"import stormvogel\n",
"import stormpy\n",
"\n",
"from orchard.orchard_builder import build_simple, build_full, build_prism"
]
},
{
"cell_type": "code",
"execution_count": 2,
"id": "127595c6",
"metadata": {
"execution": {
"iopub.execute_input": "2026-03-26T10:39:36.368614Z",
"iopub.status.busy": "2026-03-26T10:39:36.368330Z",
"iopub.status.idle": "2026-03-26T10:39:38.715217Z",
"shell.execute_reply": "2026-03-26T10:39:38.714623Z"
}
},
"outputs": [
{
"name": "stderr",
"output_type": "stream",
"text": [
"/__w/stormvogel/stormvogel/stormvogel/bird.py:126: UserWarning: State-action rewards are not supported in this version of stormvogel. Will assign None to the second parameter of your reward function.\n",
" warnings.warn(\n"
]
}
],
"source": [
"orchard_simple = build_simple()\n",
"orchard, orchard_storm = build_full()\n",
"orchard_prism, _ = build_prism()"
]
},
{
"cell_type": "markdown",
"id": "7d30416d",
"metadata": {},
"source": [
"We have the following four models:\n",
"- `orchard_simple` is the simple Orchard game (with only two fruits) modeled in Stormvogel.\n",
"- `orchard` is the full Orchard game model in Stormvogel.\n",
"- `orchard_storm` is the `orchard` model in Storm data structures.\n",
"- `orchard_prism` is the full Orchard game model specified in the Prism modeling language.\n",
"\n",
"The latter three models are semantically equivalent."
]
},
{
"cell_type": "markdown",
"id": "b59398a7",
"metadata": {},
"source": [
"## Reachability\n",
"One of the simplest properties for MDPs is a reachability query *\"what is the\n",
"maximal probability to reach a specific set of states, described by $\\varphi$?\"*.\n",
"In Storm and in Stormvogel, we specify formulas in the defacto standard [Prism representation](https://www.prismmodelchecker.org/manual/PropertySpecification/Introduction), for example `Pmax=? [F \"Label\"]`.\n",
"\n",
"In the Orchard game, we are mostly interested in the *\"maximal probability of winning the game\"*. Using the label `\"PlayersWon\"`, we express this property as `Pmax=?(F \"PlayersWon\")`, i.e. maximizing the probability of reaching a state where the players have won.\n",
"\n",
"Note that, for many queries, we get a result for every state and we therefore clarify in the code that we are interested in the probability from the initial state (`initial_state`)."
]
},
{
"cell_type": "code",
"execution_count": 3,
"id": "db29c044",
"metadata": {
"execution": {
"iopub.execute_input": "2026-03-26T10:39:38.717424Z",
"iopub.status.busy": "2026-03-26T10:39:38.717184Z",
"iopub.status.idle": "2026-03-26T10:39:38.729387Z",
"shell.execute_reply": "2026-03-26T10:39:38.728906Z"
}
},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"0.5711805425946498\n"
]
}
],
"source": [
"# Probability of winning the simple game\n",
"prob_players_won = 'Pmax=? [F \"PlayersWon\"]'\n",
"result = stormvogel.model_checking(orchard_simple, prob_players_won)\n",
"print(result.get_result_of_state(orchard_simple.initial_state))"
]
},
{
"cell_type": "markdown",
"id": "3912cbf6",
"metadata": {},
"source": [
"The resulting winning probability is $0.5712$."
]
},
{
"cell_type": "markdown",
"id": "7c58793a",
"metadata": {},
"source": [
"We can also visualize the result of this query on the MDP state space.\n",
"\n",
"Note again that a potential warning of the form `Test request failed` can be safely ignored."
]
},
{
"cell_type": "code",
"execution_count": 4,
"id": "b2799547",
"metadata": {
"editable": true,
"execution": {
"iopub.execute_input": "2026-03-26T10:39:38.731263Z",
"iopub.status.busy": "2026-03-26T10:39:38.731086Z",
"iopub.status.idle": "2026-03-26T10:39:38.939909Z",
"shell.execute_reply": "2026-03-26T10:39:38.939262Z"
},
"slideshow": {
"slide_type": ""
}
},
"outputs": [
{
"data": {
"text/html": [
"\n",
"\n",
"\n",
" \n",
" Network\n",
" \n",
" \n",
" \n",
" \n",
" \n",
" \n",
" \n",
" \n",
" \n",
"\n"
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"vis = stormvogel.show(orchard_simple, result=result)"
]
},
{
"cell_type": "markdown",
"id": "c3d6c27e",
"metadata": {},
"source": [
"As before, states are depicted as ellipses, actions by boxes and transitions by arrows.\n",
"Labels are given inside the states and actions, and the rewards are indicated by the โฌ symbol.\n",
"\n",
"In addition, in each state, the start symbol now indicates the computed result value from that state onwards.\n",
"The state is also colored with a red gradient depending on the result: the darker a state the higher its winning probability.\n",
"For instance, from the state 2๐, 1๐, 2โ๐ฆโโฌ, which should be visable on the right hand side (close to the initial state), the players have a winning probability of $\\frac{145}{216} = 0.671$.\n",
"Following the action `nextRound` we can reach the successor state ๐ฒ๐ฆโโฌ. Here, the probability is only $\\frac{13}{36} = 0.3611$, as the raven is then one step closer to the orchard."
]
},
{
"cell_type": "markdown",
"id": "5b6c302b",
"metadata": {},
"source": [
"The model checking also returns a memoryless policy $\\sigma$ which ensures the maximal winning probability.\n",
"For each state $s$, the policy chooses one action $\\sigma(s)$.\n",
"This action is highlighted in red color in the previous Stormvogel visualization.\n",
"For example, from the previous state state 2๐, 1๐, 2โ๐ฆโโฌ and action `nextRound`, the state ๐ฒ๐งบ is reachable.\n",
"Here, the player has the option to either `chooseAPPLE` or to `chooseCHERRY`.\n",
"From the red colouring, we can see that the optimal policy chooses ๐, because the successor state has a\n",
"winning probability of $\\frac{19}{24} = 0.7916$. This is higher than the non-optimal (blue colored) choice of ๐, which only has a winning probability of $\\frac{20}{27} = 0.7407$."
]
},
{
"cell_type": "markdown",
"id": "63dfc987",
"metadata": {},
"source": [
"For the full model orchard, the winning probability can be computed similarly."
]
},
{
"cell_type": "code",
"execution_count": 5,
"id": "5364ee8f",
"metadata": {
"execution": {
"iopub.execute_input": "2026-03-26T10:39:38.949572Z",
"iopub.status.busy": "2026-03-26T10:39:38.949121Z",
"iopub.status.idle": "2026-03-26T10:39:40.735783Z",
"shell.execute_reply": "2026-03-26T10:39:40.735121Z"
}
},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"0.6313570205400707\n"
]
}
],
"source": [
"# Probability of winning the full game\n",
"prob_players_won = 'Pmax=? [F \"PlayersWon\"]'\n",
"result = stormvogel.model_checking(orchard, prob_players_won)\n",
"print(result.get_result_of_state(orchard.initial_state))"
]
},
{
"cell_type": "markdown",
"id": "d058c7ae",
"metadata": {},
"source": [
"The wininng probabilty is $0.6313$."
]
},
{
"cell_type": "markdown",
"id": "c47d6bb5",
"metadata": {},
"source": [
"## Total rewards\n",
"Probabilistic model checkers commonly handle reward-based queries like *\"what is the maximal expected total reward until reaching a specific set of states?\"* which can be expressed as `R{rew}max=? (F \"Label\")`, where `\"Label\"` is again describing a set of states and `rew` refers to the name of a reward structure.\n",
"\n",
"In the Orchard game, the *\"maximal expected total number of rounds until the game ends\"* is described by `R{\"rounds\"}\n",
"max=? (F (\"PlayersWon\" | \"RavenWon\"))`. Here, `\"PlayersWon\" | \"RavenWon\"` is the disjunction of the two labels which indicate that one of the parties has won and the game has ended.\n",
"\n",
"Moreover, we compute the maximal and the minimal reward.\n",
"The maximal reward is achieved by a policy which maximizes the playing time, while the minimal reward corresponds to a policy minimizing the playing time."
]
},
{
"cell_type": "code",
"execution_count": 6,
"id": "d6409798",
"metadata": {
"execution": {
"iopub.execute_input": "2026-03-26T10:39:40.737757Z",
"iopub.status.busy": "2026-03-26T10:39:40.737573Z",
"iopub.status.idle": "2026-03-26T10:39:44.318165Z",
"shell.execute_reply": "2026-03-26T10:39:44.317582Z"
},
"lines_to_next_cell": 2
},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"22.339093430484457\n"
]
},
{
"name": "stdout",
"output_type": "stream",
"text": [
"20.882785206708473\n"
]
}
],
"source": [
"reward_prop = 'R{\"rounds\"}max=? [F \"PlayersWon\" | \"RavenWon\"]'\n",
"print(\n",
" stormvogel.model_checking(orchard, reward_prop).get_result_of_state(\n",
" orchard.initial_state\n",
" )\n",
")\n",
"reward_prop = 'R{\"rounds\"}min=? [F \"PlayersWon\" | \"RavenWon\"]'\n",
"print(\n",
" stormvogel.model_checking(orchard, reward_prop).get_result_of_state(\n",
" orchard.initial_state\n",
" )\n",
")"
]
},
{
"cell_type": "markdown",
"id": "fba013e2",
"metadata": {},
"source": [
"Model checking reveals that the (full) game lasts between $20.88$ and $22.34$ rounds on average, depending on the chosen strategy of the players."
]
},
{
"cell_type": "markdown",
"id": "dac64f26",
"metadata": {
"lines_to_next_cell": 2
},
"source": [
"## Beyond\n",
"Storm supports several queries that go significantly beyond the classical queries.\n",
"While we used the Stormvogel model checking wrapper around Storm, for such properties we must often operate directly on the (somewhat more intricate) stormpy API.\n",
"\n",
"We use the following helper function `model_check()` for simplicity. The helper function parses a property, performs the model checking on the given model for the given property and then returns the result at the initial state."
]
},
{
"cell_type": "code",
"execution_count": 7,
"id": "3554dafb",
"metadata": {
"execution": {
"iopub.execute_input": "2026-03-26T10:39:44.320210Z",
"iopub.status.busy": "2026-03-26T10:39:44.320024Z",
"iopub.status.idle": "2026-03-26T10:39:44.322828Z",
"shell.execute_reply": "2026-03-26T10:39:44.322343Z"
}
},
"outputs": [],
"source": [
"# Helper function\n",
"def model_check(model, prop):\n",
" formula = stormpy.parse_properties(prop)[0]\n",
" result = stormpy.model_checking(model, formula, only_initial_states=True)\n",
" return result.at(model.initial_states[0])"
]
},
{
"cell_type": "markdown",
"id": "4fb6b92a",
"metadata": {},
"source": [
"### Reward-bounded reachability probabilities\n",
"Reward-bounded reachability probabilities of the form `Pmax=? [F{rew}<=k \"Label\"]` ask for the probability to reach a `\"Label\"`-state while having accumulated at most $k$ reward.\n",
"\n",
"In the Orchard game, we can compute the winning probability for varying number of rounds."
]
},
{
"cell_type": "code",
"execution_count": 8,
"id": "9d4012c1",
"metadata": {
"execution": {
"iopub.execute_input": "2026-03-26T10:39:44.324599Z",
"iopub.status.busy": "2026-03-26T10:39:44.324429Z",
"iopub.status.idle": "2026-03-26T10:39:48.549058Z",
"shell.execute_reply": "2026-03-26T10:39:48.548400Z"
}
},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Round 0: 0.0\n",
"Round 1: 0.0\n",
"Round 2: 0.0\n",
"Round 3: 0.0\n",
"Round 4: 0.0\n",
"Round 5: 0.0\n",
"Round 6: 0.0\n",
"Round 7: 0.0\n",
"Round 8: 0.0\n"
]
},
{
"name": "stdout",
"output_type": "stream",
"text": [
"Round 9: 0.0\n",
"Round 10: 0.0\n",
"Round 11: 0.0\n"
]
},
{
"name": "stdout",
"output_type": "stream",
"text": [
"Round 12: 0.0\n",
"Round 13: 0.0\n",
"Round 14: 0.0\n",
"Round 15: 0.0\n",
"Round 16: 0.004162126278372636\n",
"Round 17: 0.021351772506558953\n"
]
},
{
"name": "stdout",
"output_type": "stream",
"text": [
"Round 18: 0.060203495833722385\n",
"Round 19: 0.12409888742931646\n",
"Round 20: 0.20988036964075973\n",
"Round 21: 0.30158084132994223\n"
]
},
{
"name": "stdout",
"output_type": "stream",
"text": [
"Round 22: 0.3859421091236708\n",
"Round 23: 0.4560420208004474\n",
"Round 24: 0.5102170036741989\n",
"Round 25: 0.5498940328681379\n",
"Round 26: 0.5777848204667783\n",
"Round 27: 0.5967720330221457\n",
"Round 28: 0.6093722181054767\n",
"Round 29: 0.6175629247761446\n"
]
},
{
"name": "stdout",
"output_type": "stream",
"text": [
"Round 30: 0.6227977136574545\n",
"Round 31: 0.6260964497778784\n",
"Round 32: 0.6281506036561613\n",
"Round 33: 0.6294168505012261\n",
"Round 34: 0.6301906201480247\n",
"Round 35: 0.6306598665532833\n",
"Round 36: 0.6309425371167758\n",
"Round 37: 0.6311118037113413\n"
]
},
{
"name": "stdout",
"output_type": "stream",
"text": [
"Round 38: 0.6312126210507402\n",
"Round 39: 0.6312723779854957\n",
"Round 40: 0.6313076401736203\n"
]
}
],
"source": [
"# Winning probability within k rounds\n",
"probabilities = []\n",
"for k in range(41):\n",
" win_steps = 'Pmax=? [F{\"rounds\"}<=' + str(k) + ' \"PlayersWon\"]'\n",
" probabilities.append(model_check(orchard_prism, win_steps))\n",
" print(\"Round {}: {}\".format(k, probabilities[-1]))"
]
},
{
"cell_type": "markdown",
"id": "8558fb6c",
"metadata": {},
"source": [
"Afterwards, we can plot the results."
]
},
{
"cell_type": "code",
"execution_count": 9,
"id": "44a4aba8",
"metadata": {
"execution": {
"iopub.execute_input": "2026-03-26T10:39:48.550891Z",
"iopub.status.busy": "2026-03-26T10:39:48.550699Z",
"iopub.status.idle": "2026-03-26T10:39:50.027636Z",
"shell.execute_reply": "2026-03-26T10:39:50.027040Z"
},
"lines_to_next_cell": 0
},
"outputs": [
{
"data": {
"text/plain": [
"[]"
]
},
"execution_count": 9,
"metadata": {},
"output_type": "execute_result"
},
{
"data": {
"image/png": "iVBORw0KGgoAAAANSUhEUgAABNEAAAHWCAYAAABZkR9hAAAAOnRFWHRTb2Z0d2FyZQBNYXRwbG90bGliIHZlcnNpb24zLjEwLjgsIGh0dHBzOi8vbWF0cGxvdGxpYi5vcmcvwVt1zgAAAAlwSFlzAAAPYQAAD2EBqD+naQAAbApJREFUeJzt3Xd0VGXixvFnJsmkJxACCYFAgNBLQo2IgCwoCIqAu7KKguj6s9A06CoWEF2lWBYVRNdFrCgWxLIKYqSIoiAhgJTQCS2hpkPKzP39ERgIBJKBJDfl+zlnDrnvLfNMzpxxfHLvfS2GYRgCAAAAAAAAcFFWswMAAAAAAAAAFR0lGgAAAAAAAFAMSjQAAAAAAACgGJRoAAAAAAAAQDEo0QAAAAAAAIBiUKIBAAAAAAAAxaBEAwAAAAAAAIpBiQYAAAAAAAAUgxINAAAAAAAAKAYlGgAAQDUSERGhG2+80dQMd911lyIiIkzNAAAA4CpKNAAAgApg06ZNuuOOO1SvXj15enoqLCxMw4YN06ZNm8yOBgAAAFGiAQAAmG7BggXq0KGD4uLiNHLkSL3xxhu65557tHTpUnXo0EFffvml2REBAACqPXezAwAAAFRnO3fu1J133qnGjRtrxYoVql27tnPduHHj1L17d915553asGGDGjduXOQxsrKy5OvrW16Ri3Xq1CnZbDZZrfy9FgAAVB18swEAADDRiy++qOzsbP3nP/8pVKBJUnBwsN566y1lZWVp+vTpkqRnnnlGFotFmzdv1u23366aNWvqmmuuce7z4YcfqkuXLvLx8VHNmjXVo0cP/fDDDxc878qVK9WlSxd5eXmpcePGev/99wutP378uB555BG1bdtWfn5+CggI0A033KD169cX2m7ZsmWyWCz65JNP9NRTT6levXry8fFRenq6JGnhwoVq06aNvLy81KZNG86qAwAAlZbFMAzD7BAAAADVVb169WSz2bR79+6LbtOoUSPl5+dr3759euaZZzR58mS1atVKTZs2Vd++fWUYhh588EFNnjxZzzzzjK6++moNHjxYNptNv//+u8LDwzV16lRJBRMLeHl5KTU1Vffcc4/CwsL0zjvvaN26ddq4caNat24tSfrjjz/097//XX/729/UqFEjpaSk6K233lJmZqY2b96ssLAwSQUlWq9evdSqVSvZbDYNHz5cOTk5Gjt2rFauXKkbbrhBrVq10t13361jx45p5syZql+/vjIzM7Vnz54y//0CAACUFi7nBAAAMElaWpoOHjyom2+++ZLbtWvXTl9//bUyMjKcY1FRUZo3b55zeceOHXr22Wc1ePBgff7554UupTz/b6aJiYlasWKFunfvLkm69dZbFR4errlz5+qll16SJLVt21bbtm0rdJw777xTLVq00Jw5c/T0008XOuapU6f0xx9/yNvb2zn22GOPKSQkRCtXrlRgYKAkqWfPnrr++uvVsGHDEv2OAAAAKgou5wQAADDJmVLM39//ktudWX/mEklJuv/++wtts3DhQjkcDk2cOPGCe5FZLJZCy61atXIWaJJUu3ZtNW/eXLt27XKOeXp6Oo9jt9t17Ngx+fn5qXnz5oqPj78g44gRIwoVaIcOHVJCQoJGjBjhLNAk6brrrlOrVq0u+XoBAAAqIko0AAAAk5wpx849w6woRZVtjRo1KrTNzp07ZbVaS1RQNWjQ4IKxmjVr6sSJE85lh8Ohf//732ratKk8PT0VHBys2rVra8OGDUpLS7tg//Pz7N27V5LUtGnTC7Zt3rx5sRkBAAAqGko0AAAAkwQGBqpu3brasGHDJbfbsGGD6tWrp4CAAOfYuWd9ucrNza3I8XMv+3zhhRcUGxurHj166MMPP9TixYu1ZMkStW7dWg6H44J9ryQPAABAZcA90QAAAEx044036u2339bKlSsLzbJ5xs8//6w9e/bovvvuu+RxmjRpIofDoc2bNys6OvqKc33++efq1auX5syZU2g8NTVVwcHBxe5/5p5n27dvv2BdYmLiFecDAAAob5yJBgAAYKJHH31U3t7euu+++3Ts2LFC644fP677779fPj4+evTRRy95nEGDBslqterZZ5+94Eyxy5mM3c3N7YL9PvvsMx04cKBE+9etW1fR0dF67733Cl3+uWTJEm3evNnlPAAAAGbjTDQAAAATNW3aVO+9956GDRumtm3b6p577lGjRo20Z88ezZkzR0ePHtXHH3+sJk2aXPI4kZGRevLJJ/Xcc8+pe/fuGjJkiDw9PbVmzRqFhYVpypQpLuW68cYb9eyzz2rkyJG6+uqrtXHjRn300Udq3LhxiY8xZcoUDRgwQNdcc43uvvtuHT9+XK+//rpat26tzMxMl/IAAACYjTPRAAAATPa3v/1Na9eu1bXXXqs5c+bo/vvv19tvv62ePXtq7dq1GjJkSImO8+yzz+qdd97RyZMn9eSTT2rixInau3evevfu7XKmJ554QuPHj9fixYs1btw4xcfH63//+5/Cw8NLfIx+/frps88+k91u14QJE7RgwQLNnTtXnTp1cjkPAACA2SzG5ZzfDwAAAAAAAFQjnIkGAAAAAAAAFIMSDQAAAAAAACgGJRoAAAAAAABQDEo0AAAAAAAAoBiUaAAAAAAAAEAxKNEAAAAAAACAYribHaC8ORwOHTx4UP7+/rJYLGbHAQAAAAAAgIkMw1BGRobCwsJktV78fLNqV6IdPHhQ4eHhZscAAAAAAABABbJv3z7Vr1//ouurXYnm7+8vqeAXExAQYHIaAAAAAAAAmCk9PV3h4eHOzuhiql2JduYSzoCAAEo0AAAAAAAASFKxt/1iYgEAAAAAAACgGJRoAAAAAAAAQDEo0QAAAAAAAIBiUKIBAAAAAAAAxaBEAwAAAAAAAIpBiQYAAAAAAAAUgxINAAAAAAAAKAYlGgAAAAAAAFAMSjQAAAAAAACgGJRoAAAAAAAAQDEo0QAAAAAAAIBiUKIBAAAAAAAAxXA3OwAAAAAAAIArDMOQYUjGmZ+l08sF42e3Ozt2/rYFG5z5x3Buf86wc/vC64zz9i16/fnHOnO8c9dd+LrO+fmcPQuPX3i888cvdsyij3LpbS923LqBXvL38rjI2qqJEg0AAAAAgMtkGIZy7Q7l5p9+2B3KtxvKdxiyOxzKdxiFl+2G7I4zy4by7I5Cy2e2y7MXXs53GLLbDeWdt2w/XSbZHYYcxumHQ7I7fzbkMHR6u4Jj2h0FuQu20eltCtYZRhH7nl4vSY7Tz+c4t7g6fRxDBc9d9HZnlx1G4RLs/G1VXPGFCmH2sA66oW1ds2OUK0o0AAAAAEClZRiGcvIdOplrV3aeXSdz85Wda1d2rr1gLNeu7Nx8ncqzK+d0yeUsvE4v59kdBevOGzuznFPE2NntaHaA6oISDQAAAABQbk7l2ZV2Mk+p2XlKO5mn9JN5Fy2/TuadP5Z/erzwmIMeq0xYLJKbxSKrxSKLRYX/Pb3eYrHIes6/0pnlc7c7u9+ZbS0WyaLCx9SZbZ3Hliw6u61OrzuTzXL+9ioYLLRcxLHOfZ4z6wuSn11XeNn5GyliW+eawsvnjTt3KOJ5zlt9zvOdP1709oWPXWhNkccs8hjFbnvhYP2aPhc5QtVFiQYAAAAAcInDYSgjJ19p2XlKPZnrLMVST+YpLfu85ZN5zu1Ss/OUk+8wO75LLBbJ5maVzd0qT3erPE7/fGbM45x1Z8bc3azysFrkZrXI3e30v1arc9ndapGb1Xr634Jld7fCy2e3tRZaPrPfmTGrtaDkcrNYZLUWlFFu1oKyynq6AHOzFpQ/bqe3PVNmnb9/4W0KlzYAKNEAAAAAoNqzOwwdycjRobSTSk47pUNpp5SanavUC8qwgrH0k3mmnf1lc7fKx+YmHw83edvc5GNzP/1vwcPbw935s4+t4Gdvm5u8Pdzk6XG26HL+63522cPtdBnmfrYgc7daKJMASKJEAwAAAIAqLc/u0OGMHCWnndShtFNKTjulg6mnlJx+dvlwRo7sZdiKebpbVcPHQzW8bQr09lCgj4dqeHso0NtDAd4ezqLr/BLM2+Ym3/OKMHc3a5nlBIBLoUQDAAAAgEoqJ9+uw+k5OpR2qtBZZOf+fCQzp1RmNbRYJH9Pd9XwsamGT0EBFujtcdFy7NztvDzcrjwAAJiMEg0AAAAAKrCjmTnalpyhxJQM7T6aVagkO5qZe8XHD/azKTTQS6EB3qob6HX6Zy8F+3sWlGGnizJ/Lw+5WbmsEUD1RYkGAAAAABVA+qk8bU/JUGJypralZCgxOUPbUjJ0LOvyijKLRart5+ksxuoGep/+t+DnuoFeqhPgKU93zhIDgJKgRAMAAACAcnQy164dhwuKsm0pBWeYbUvO0MG0UyU+htUihQR4OUuxc88iqxvopbo1vFXH31Me3D8MAEoNJRoAAAAAlIE8u0N7jmY5S7LE02eX7T2eXeJ7lAX7eap5qJ+ahfireYi/Iuv4qV5Nb9X28+QG+wBQzijRAAAAAOAKOByG9p3IVmJyhrYfznRehrnzSKby7CVry/y93NU8xF/NQgvKsmYh/moW4qdafp5lnB4AUFKUaAAAAADgAsMwtPNIplZuP6qVO47p913HlJGTX6J9vTysalqnoCRznmEW6q/QAC9ZLNy0HwAqMko0AAAAAChGctop/bLjqH7ZcVQrdxzV4YycS27vbrWocW1f52WYZ84wCw/yYYZLAKikKNEAAAAA4Dzpp/L0285jztJs55Gsi24b5GtThwY11SL0bFnWKNhXNnfuWQYAVYnpJdqsWbP04osvKjk5WVFRUXr99dfVpUuXi26fmpqqJ598UgsWLNDx48fVsGFDzZgxQ/379y/H1AAAAACqkpx8u+L3pjpLsw37U+W4yO3MvD3c1KVRkK6JDNbVkbXUMjRAVs4uA4Aqz9QSbf78+YqNjdWbb76pmJgYzZgxQ3379lViYqLq1Klzwfa5ubm67rrrVKdOHX3++eeqV6+e9u7dqxo1apR/eAAAAACVlsNhaPOhdGdptmbPcZ3KcxS5rZvVoqj6gadLs2C1b1BDnu5u5ZwYAGA2i2GUdHLl0hcTE6POnTtr5syZkiSHw6Hw8HCNGTNGjz/++AXbv/nmm3rxxRe1detWeXh4XNZzpqenKzAwUGlpaQoICLii/AAAAAAqj6Rj2Vp5+r5mv+48qhPZeRfdtmkdP3WLDNY1kcGKaRwkf6/L+/8PAEDFV9KuyLQz0XJzc7V27VpNmDDBOWa1WtWnTx+tWrWqyH2+/vprde3aVaNGjdJXX32l2rVr6/bbb9djjz0mN7ei/xKUk5OjnJyzN/1MT08v3RcCAAAAoEI6lpmjX8+5r9n+Eycvum1ogFdBada0lq5uEqyQAK9yTAoAqAxMK9GOHj0qu92ukJCQQuMhISHaunVrkfvs2rVLP/30k4YNG6bvvvtOO3bs0IMPPqi8vDxNmjSpyH2mTJmiyZMnl3p+AAAAABVPTr5dizel6OPfk7Rq17GLbufv5a6rm9RSt8hgdYsMVuNgX1ks3NcMAHBxpk8s4AqHw6E6deroP//5j9zc3NSxY0cdOHBAL7744kVLtAkTJig2Nta5nJ6ervDw8PKKDAAAAKAc7DySqU9WJ+nztfuLvEzT5mZVp4iaztKsTViA3N2YPRMAUHKmlWjBwcFyc3NTSkpKofGUlBSFhoYWuU/dunXl4eFR6NLNli1bKjk5Wbm5ubLZbBfs4+npKU9Pz9INDwAAAMB0p/LsWrwpWfN+T9Lvu49fsL5RsK/6tg5Vt8ha6tQwSN42JgMAAFw+00o0m82mjh07Ki4uToMGDZJUcKZZXFycRo8eXeQ+3bp107x58+RwOGS1FvzVaNu2bapbt26RBRoAAACAqmfH4Qx9vHqfvojfr9TzzjqzuVnVr02obuvSQFc1DuISTQBAqTH1cs7Y2FiNGDFCnTp1UpcuXTRjxgxlZWVp5MiRkqThw4erXr16mjJliiTpgQce0MyZMzVu3DiNGTNG27dv1wsvvKCxY8ea+TIAAAAAlLFTeXZ9/+chffz7Pq3ec+FZZ41r++r2Lg00pEN9BfnyB3YAQOkztUQbOnSojhw5ookTJyo5OVnR0dFatGiRc7KBpKQk5xlnkhQeHq7Fixfr4YcfVrt27VSvXj2NGzdOjz32mFkvAQAAAEAZ2paSoY9XJ2lB/AGlnTzvrDN3q/qfPuusSyPOOgMAlC2LYRiG2SHKU3p6ugIDA5WWlqaAgACz4wAAAAA4z6k8u/634ZA+Xp2kP/aeuGB9ZB0/3dalgYa0r6eanHUGALhCJe2KKtXsnAAAAACqrsTkM2ed7Vf6qfxC62zuVt3Ytq5ui2mgTg1rctYZAKDcUaIBAAAAMM3JXLu+3XBQH69OUnxS6gXrm4UUnHU2uH091fDhrDMAgHko0QAAAACUuy2H0vXx6iR9ue6AMs4768zT3aob24Xp9phwdWjAWWcAgIqBEg0AAABAubA7DC1cd0Af/LZXCftSL1jfItRft3VpoEHt6ynQ26P8AwIAcAmUaAAAAADK3B97jmvS15u06WB6oXEvD6tuahem22IaqH14Dc46AwBUWJRoAAAAAMpMctopTf1+ixYmHCw03iLUX8NiGujm9vUU4MVZZwCAio8SDQAAAECpy8m3678/79aspTuUnWt3jrcI9dfEm1qpa+NanHUGAKhUKNEAAAAAlBrDMBS35bCe+99m7T2W7Ryv4eOh8dc3122dw+XuZjUxIQAAl4cSDQAAAECp2HkkU89+s1nLtx1xjlkt0rCYhoq9rplq+tpMTAcAwJWhRAMAAABwRTJO5en1n3bonZW7le8wnOMxjYL0zMDWalk3wMR0AACUDko0AAAAAJfF4TC0YN0BTf1+q45m5jjHwwK99MSAlhrQti73PQMAVBmUaAAAAABctn5fqiZ9vUkJ+1KdYzZ3q+7v0Vj3X9tEPjb+VwMAULXwXzYAAAAAJXYkI0fTF23VZ2v3Fxrv2zpETw1opfAgH5OSAQBQtijRAAAAABQrN9+h91ft0as/bldGTr5zvGkdP026qbWuaRpsYjoAAMoeJRoAAACAS1qx7Ygmf7NJO49kOcf8vdz1cJ9murNrQ3m4WU1MBwBA+aBEAwAAAFCkvcey9Ny3W/TjlhTnmMUiDe0Urkf6Nlewn6eJ6QAAKF+UaAAAAAAKycrJ1xvLdujtFbuVa3c4xzs0qKHJA9uobf1AE9MBAGAOSjQAAAAAkiTDMPT1+oOa8t1WJaefco7X8ffUhP4tNCi6niwWi4kJAQAwDyUaAAAAAG06mKZnvt6kNXtOOMc83Cz6R/fGGtUrUn6e/K8DAKB647+EAAAAQDXmcBia8eM2zVy6Qw7j7HjvFnX01I2t1CjY17xwAABUIJRoAAAAQDWVnZuv2PnrtWhTsnOsUbCvJt7YSr1a1DExGQAAFQ8lGgAAAFANHUw9qX+894c2H0qXJFkt0sN9mum+nk1kc7eanA4AgIqHEg0AAACoZtYlndC976/V0cwcSZK/p7teu729ejXn7DMAAC6GEg0AAACoRr5KOKBHP9+g3HyHJKlBkI/mjOikpiH+JicDAKBio0QDAAAAqgGHw9DLSxI1a+lO51hMoyDNvqOjgnxtJiYDAKByoEQDAAAAqrisnHzFfpqgxZtSnGO3dQnX5IFtuP8ZAAAlRIkGAAAAVGFFTSDw1IBWGtktQhaLxeR0AABUHpRoAAAAQBUVn3RC/3feBAKv395e1zKBAAAALqNEAwAAAKqghesO6J9fnJ1AoGGtggkEIuswgQAAAJeDEg0AAACoQhwOQy/9kKg3lp2dQOCqxkGaPayjajKBAAAAl40SDQAAAKgisnLy9fD8BP2w+dwJBBpo8sDWTCAAAMAVokQDAAAAqoADpycQ2HLOBAJP39hKd13NBAIAAJQGSjQAAACgklu794Tu++APHc3MlcQEAgAAlAVKNAAAAKAS+3Ldfj32+Ubl2plAAACAskSJBgAAAFRCDoehF39I1GwmEAAAoFxQogEAAACVTFZOvh6an6Al50wgcHtMwQQCHm5MIAAAQFmgRAMAAAAqkf0nsvWP9/7Q1uQMSQUTCEy8sZVGMIEAAABlihINAAAAqCQumEDAy12zbu+gHs1qm5wMAICqjxINAAAAqAQWxO/X41+cnUAgopaP/juisyLr+JmcDACA6oESDQAAAKjAHA5D0xcn6s3lZycQuLpJLb0xrINq+DCBAAAA5YUSDQAAAKigMnPy9dAnCfpxy9kJBIbFNNAzTCAAAEC5o0QDAAAAKqC0k3m67T+/afOhdEmSm9WiiTe20vCuDZlAAAAAE1CiAQAAABVMTr5d933wh7NA8/dy1xvDOqh7UyYQAADALJRoAAAAQAXicBh69LMN+m3XcUlSLV+b5t93lSLr+JucDACA6q1C3Ehh1qxZioiIkJeXl2JiYrR69eqLbvvuu+/KYrEUenh5eZVjWgAAAKDsTF+cqK/XH5QkeXlYNeeuzhRoAABUAKaXaPPnz1dsbKwmTZqk+Ph4RUVFqW/fvjp8+PBF9wkICNChQ4ecj71795ZjYgAAAKBsfPDbXucsnFaL9PptHRQdXsPcUAAAQFIFKNFeeeUV3XvvvRo5cqRatWqlN998Uz4+PnrnnXcuuo/FYlFoaKjzERISUo6JAQAAgNK3ZHOKJn31p3N58sDWuq4V33MBAKgoTC3RcnNztXbtWvXp08c5ZrVa1adPH61ateqi+2VmZqphw4YKDw/XzTffrE2bNl1025ycHKWnpxd6AAAAABVJwr5Ujfk4Xg6jYPm+no11Z9cIUzMBAIDCTC3Rjh49KrvdfsGZZCEhIUpOTi5yn+bNm+udd97RV199pQ8//FAOh0NXX3219u/fX+T2U6ZMUWBgoPMRHh5e6q8DAAAAuFx7j2XpnnfX6FSeQ5I0MCpMj/VtYXIqAABwPtMv53RV165dNXz4cEVHR6tnz55asGCBateurbfeeqvI7SdMmKC0tDTnY9++feWcGAAAACja8axc3TV3jY5l5UqSrmocpBf/1k5Wq8XkZAAA4Hzuru7w2muvFTl+ZpbMyMhI9ejRQ25ubsUeKzg4WG5ubkpJSSk0npKSotDQ0BLl8fDwUPv27bVjx44i13t6esrT07NExwIAAADKy6k8u/7x3hrtPpolSWpax09v3dlJnu7Ff48GAADlz+US7d///reOHDmi7Oxs1axZU5J04sQJ+fj4yM/PT4cPH1bjxo21dOnSYi+dtNls6tixo+Li4jRo0CBJksPhUFxcnEaPHl2iPHa7XRs3blT//v1dfSkAAACAKewOQ+M+Waf4pFRJUh1/T717dxcFenuYGwwAAFyUy5dzvvDCC+rcubO2b9+uY8eO6dixY9q2bZtiYmL06quvKikpSaGhoXr44YdLdLzY2Fi9/fbbeu+997RlyxY98MADysrK0siRIyVJw4cP14QJE5zbP/vss/rhhx+0a9cuxcfH64477tDevXv1j3/8w9WXAgAAAJQ7wzD03LebtXhTwdUYvjY3zR3ZWfVqeJucDAAAXIrLZ6I99dRT+uKLL9SkSRPnWGRkpF566SXdcsst2rVrl6ZPn65bbrmlRMcbOnSojhw5ookTJyo5OVnR0dFatGiRc7KBpKQkWa1nu74TJ07o3nvvVXJysmrWrKmOHTvq119/VatWrVx9KQAAAEC5m7Nyt979dY8kyc1q0Rt3dFTrsEBzQwEAgGJZDMMwXNnBx8dHK1asUKdOnQqNr1mzRj179lR2drb27NmjNm3aKDMzs1TDlob09HQFBgYqLS1NAQEBZscBAABANfLthoMaPW+dc3n6X9vp1k7MHg8AgJlK2hW5fDlnr169dN9992ndurP/8V+3bp0eeOAB/eUvf5Ekbdy4UY0aNbqM2AAAAEDVtHr3ccXOX+9cfqhPUwo0AAAqEZdLtDlz5igoKEgdO3Z0znzZqVMnBQUFac6cOZIkPz8/vfzyy6UeFgAAAKiMdhzO0L3v/6Fcu0OSdGun+hrXu6nJqQAAgCtcvpzzjK1bt2rbtm2SpObNm6t58+alGqyscDknAAAAytPhjFMaPOtXHUg9KUnq0ay25ozoJA83l/+eDQAAykBJuyKXJxY4o0WLFmrRosXl7g4AAABUeVk5+br73TXOAq1V3QC9MawDBRoAAJWQyyWa3W7Xu+++q7i4OB0+fFgOh6PQ+p9++qnUwgEAAACVVb7doVHz4vXngXRJUr0a3po7srP8PC/779gAAMBELv8XfNy4cXr33Xc1YMAAtWnTRhaLpSxyAQAAAJWWYRh6auGfWpZ4RJIU4OWud0d2VkiAl8nJAADA5XK5RPvkk0/06aefqn///mWRBwAAAKj0Zv60Q5+s2SdJsrlZ9Z/hndQ0xN/kVAAA4Eq4fDMGm82myMjIssgCAAAAVHpfrN2vl5dscy6/dGuUrmpcy8REAACgNLhcoo0fP16vvvqqLnNSTwAAAKDK+nn7ET32xQbn8uM3tNDAqDATEwEAgNLi8uWcK1eu1NKlS/X999+rdevW8vDwKLR+wYIFpRYOAAAAqCw2H0zXAx/GK99R8MfmO69qqPt6NDY5FQAAKC0ul2g1atTQ4MGDyyILAAAAUCkdTD2pke+uVmZOviTpulYhemZgaybhAgCgCnG5RJs7d25Z5AAAAAAqpbSTeRo5d41S0nMkSdHhNfTa39vLzUqBBgBAVeLyPdEAAAAAFMjNd+j+D9YqMSVDktSwlo/mjOgkb5ubyckAAEBpK9GZaB06dFBcXJxq1qyp9u3bX/K09Pj4+FILBwAAAFRUhmHon5+v16pdxyRJQb42vTuyi2r5eZqcDAAAlIUSlWg333yzPD0LvgwMGjSoLPMAAAAAlcKLixO1MOGgJMnT3ar/juikRsG+JqcCAABlxWIYhmF2iPKUnp6uwMBApaWlKSAgwOw4AAAAqIQ++n2vnvzyT0mSxSK9eUdH9W0danIqAABwOUraFbk8scAZubm5Onz4sBwOR6HxBg0aXO4hAQAAgApvxbYjenrhn87lZ25qTYEGAEA14HKJtm3bNt1zzz369ddfC40bhiGLxSK73V5q4QAAAICKJDU7V498tl6O09dy/F+PxhpxdYSpmQAAQPlwuUQbOXKk3N3d9e2336pu3bqXnGQAAAAAqEomfrVJhzNyJEk9m9XW4/1amJwIAACUF5dLtISEBK1du1YtWvCFAQAAANXH/zYc0tfrCyYSCPBy17Rb2slq5Q/KAABUF1ZXd2jVqpWOHj1aFlkAAACACulIRo6eWrjRufzszW0UGuhlYiIAAFDeXC7Rpk2bpn/+859atmyZjh07pvT09EIPAAAAoCoxDEMTFmzUiew8SVK/1qG6OTrM5FQAAKC8uXw5Z58+fSRJvXv3LjTOxAIAAACoihbEH9CPW1IkSbV8bXp+cBvuCwwAQDXkcom2dOnSssgBAAAAVDgHU0/qmW82OZdfGNJWtfw8TUwEAADM4nKJ1rNnz7LIAQAAAFQohmHosS82KONUviRpSPt66ts61ORUAADALC6XaJKUmpqq1atX6/Dhw3I4HIXWDR8+vFSCAQAAAGb66Pck/by9YEKt0AAvTbqptcmJAACAmVwu0b755hsNGzZMmZmZCggIKHQ/CIvFQokGAACASm/vsSy98N0W5/K0v7ZToI+HiYkAAIDZXJ6dc/z48br77ruVmZmp1NRUnThxwvk4fvx4WWQEAAAAyo3dYejRzzYoO7dgwqzbYxqoZ7PaJqcCAABmc7lEO3DggMaOHSsfH5+yyAMAAACYau4vu7V6T8Efh8ODvPVE/5YmJwIAABWByyVa37599ccff5RFFgAAAMBUOw5naPriREmSxSK9+Nco+Xle1m2EAQBAFePyN4IBAwbo0Ucf1ebNm9W2bVt5eBS+N8TAgQNLLRwAAABQXvLtDsV+ul65+QUTZ93drZGualzL5FQAAKCisBiGYbiyg9V68ZPXLBaL7Hb7FYcqS+np6QoMDFRaWpoCAgLMjgMAAIAK4vW47Xp5yTZJUuPavvpubHd5ebiZnAoAAJS1knZFLp+J5nA4rigYAAAAUNFsOpimV+O2S5KsFumVW6Mp0AAAQCEu3xMNAAAAqEpy8u0a/+l65TsKLtB48NpIRYfXMDcUAACocEp0Jtprr72m//u//5OXl5dee+21S247duzYUgkGAAAAlIdXf9yurckZkqQWof4a27upyYkAAEBFVKJ7ojVq1Eh//PGHatWqpUaNGl38YBaLdu3aVaoBSxv3RAMAAMAZ8Ukn9NfZv8phSB5uFn016hq1CuM7IgAA1Ump3hNt9+7dRf4MAAAAVFYnc+165NP1On0Vpx7q04wCDQAAXJTL90Sr6GeaAQAAACUxffFW7TqaJUmKCq+h+3o0NjkRAACoyFyenTMyMlL169dXz549de2116pnz56KjIwsi2wAAABAmfh151HN/WWPJMnT3aqX/xYldzfm3AIAABfn8jeFffv2acqUKfL29tb06dPVrFkz1a9fX8OGDdN///vfssgIAAAAlJrMnHw9+tkG5/I/+7VQZB0/ExMBAIDKoEQTC1zK9u3b9fzzz+ujjz6Sw+GQ3W4vrWxlgokFAAAAqrcJCzbo49X7JEkxjYL08b1XyWq1mJwKAACYpVQnFjhXdna2Vq5cqWXLlmnZsmVat26dWrRoodGjR+vaa6+9kswAAABAmVq69bCzQPOxuemlv0VRoAEAgBJxuUSrUaOGatasqWHDhunxxx9X9+7dVbNmzbLIBgAAAJSa1OxcPfbF2cs4nxrQSuFBPiYmAgAAlYnLJVr//v21cuVKffLJJ0pOTlZycrKuvfZaNWvWrCzyAQAAAKVi0tebdDgjR5LUo1lt3dYl3OREAACgMnF5YoGFCxfq6NGjWrRokbp27aoffvhB3bt3V7169TRs2LCyyAgAAABcke82HtJXCQclSQFe7pp+SztZLFzGCQAASu6y5/Fu27atunXrpq5du6pz5846fPiw5s+ff1nHmjVrliIiIuTl5aWYmBitXr26RPt98sknslgsGjRo0GU9LwAAAKq+Ixk5emrhn87lyTe3Vmigl4mJAABAZeRyifbKK69o4MCBqlWrlmJiYvTxxx+rWbNm+uKLL3TkyBGXA8yfP1+xsbGaNGmS4uPjFRUVpb59++rw4cOX3G/Pnj165JFH1L17d5efEwAAANWDYRh68suNOp6VK0nq2zpEg6LrmZwKAABURhbDMAxXdujcubN69uypa6+9Vt27d1dgYOAVBYiJiVHnzp01c+ZMSZLD4VB4eLjGjBmjxx9/vMh97Ha7evToobvvvls///yzUlNTtXDhwiK3zcnJUU5OjnM5PT1d4eHhxU5bCgAAgMpvQfx+xX66XpIU5GvTDw/3ULCfp8mpAABARZKenq7AwMBiuyKXJxZYs2bNFQU7V25urtauXasJEyY4x6xWq/r06aNVq1ZddL9nn31WderU0T333KOff/75ks8xZcoUTZ48udQyAwAAoHI4lHZSk77e5Fx+YXAbCjQAAHDZLvueaKXh6NGjstvtCgkJKTQeEhKi5OTkIvdZuXKl5syZo7fffrtEzzFhwgSlpaU5H/v27bvi3AAAAKjYDMPQPz/foIxT+ZKkQdFh6temrsmpAABAZebymWhmysjI0J133qm3335bwcHBJdrH09NTnp78xREAAKA6mbc6ST9vPypJCgnw1OSBbUxOBAAAKjtTS7Tg4GC5ubkpJSWl0HhKSopCQ0Mv2H7nzp3as2ePbrrpJueYw+GQJLm7uysxMVFNmjQp29AAAACo0JKOZev5/21xLk+9pZ0CfTxMTAQAAKoCUy/ntNls6tixo+Li4pxjDodDcXFx6tq16wXbt2jRQhs3blRCQoLzMXDgQPXq1UsJCQkKDw8vz/gAAACoYBwOQ498tl7ZuXZJ0m1dwtWreR2TUwEAgKrA5TPRTp48KcMw5OPjI0nau3evvvzyS7Vq1UrXX3+9ywFiY2M1YsQIderUSV26dNGMGTOUlZWlkSNHSpKGDx+uevXqacqUKfLy8lKbNoVPxa9Ro4YkXTAOAACA6uedX3Zr9Z7jkqT6Nb315IBWJicCAABVhcsl2s0336whQ4bo/vvvV2pqqmJiYuTh4aGjR4/qlVde0QMPPODS8YYOHaojR45o4sSJSk5OVnR0tBYtWuScbCApKUlWq6knzAEAAKAS2HE4Q9MXJzqXX/xrlPw8K9UtgAEAQAVmMQzDcGWH4OBgLV++XK1bt9Z///tfvf7661q3bp2++OILTZw4UVu2bCn+ICZKT09XYGCg0tLSFBAQYHYcAAAAlAKHw9CQ2b8qYV+qJGlktwhNuqm1uaEAAEClUNKuyOVTvLKzs+Xv7y9J+uGHHzRkyBBZrVZdddVV2rt37+UnBgAAAC7TgnUHnAVa42BfPdavhbmBAABAleNyiRYZGamFCxdq3759Wrx4sfM+aIcPH+bMLgAAAJS77Nx8vbh4q3P5uUFt5OXhZmIiAABQFblcok2cOFGPPPKIIiIiFBMT45xF84cfflD79u1LPSAAAABwKW8t36WU9BxJUp+WddQtMtjkRAAAoCpy+U6rf/3rX3XNNdfo0KFDioqKco737t1bgwcPLtVwAAAAwKUkp53SWyt2SpLcrRZN6N/S5EQAAKCqcqlEy8vLk7e3txISEi4466xLly6lGgwAAAAozvTFW3UqzyFJuuOqhmpS28/kRAAAoKpy6XJODw8PNWjQQHa7vazyAAAAACWyYX+qFsQfkCQFenvooT5NTU4EAACqMpfvifbkk0/qiSee0PHjx8siDwAAAFAswzD0r2+3OJfH9m6qGj42ExMBAICqzuV7os2cOVM7duxQWFiYGjZsKF9f30Lr4+PjSy0cAAAAUJRFfyZr9Z6CP+o2CvbVnVc1NDkRAACo6lwu0QYNGlQGMQAAAICSycm3a8r3W53LT/RvKZu7yxdYAAAAuMTlEm3SpEllkQMAAAAokfd+3aOk49mSpK6Na6lPyzomJwIAANXBZf3JLjU1Vf/97381YcIE573R4uPjdeDAgVINBwAAAJzrWGaOXo/bIUmyWKSnbmwpi8VicioAAFAduHwm2oYNG9SnTx8FBgZqz549uvfeexUUFKQFCxYoKSlJ77//flnkBAAAADTjx+3KyMmXJP2tY321Dgs0OREAAKguXD4TLTY2VnfddZe2b98uLy8v53j//v21YsWKUg0HAAAAnLE9JUPzVidJknxsbnrk+uYmJwIAANWJyyXamjVrdN99910wXq9ePSUnJ5dKKAAAAOB8z3+3RXaHIUl68NomqhPgVcweAAAApcflEs3T01Pp6ekXjG/btk21a9culVAAAADAuZZvO6JliUckSWGBXvpH98YmJwIAANWNyyXawIED9eyzzyovL0+SZLFYlJSUpMcee0y33HJLqQcEAABA9ZZvd+hf3252Lj92Qwt5ebiZmAgAAFRHLpdoL7/8sjIzM1WnTh2dPHlSPXv2VGRkpPz9/fX888+XRUYAAABUY5+s2afthzMlSdHhNTQwKszkRAAAoDpyeXbOwMBALVmyRCtXrtSGDRuUmZmpDh06qE+fPmWRDwAAANVY+qk8/XvJNufy0ze2lMViMTERAACorlwu0Xbt2qXGjRvrmmuu0TXXXFMWmQAAAABJ0qyfduhYVq4k6cZ2ddWxYZDJiQAAQHXl8uWckZGR6tWrlz788EOdOnWqLDIBAAAASjqWrbm/7JEk2dyteqxfC3MDAQCAas3lEi0+Pl7t2rVTbGysQkNDdd999+n3338vi2wAAACoxqYu2qJcu0OSdM81jRQe5GNyIgAAUJ25XKJFR0fr1Vdf1cGDB/XOO+/o0KFD6t69u9q0aaNXXnlFR44cKYucAAAAqEbW7Dmu7zYmS5KC/Wx68NomJicCAADVncsl2hnu7u4aMmSIPvvsM02bNk07duzQI488ovDwcA0fPlyHDh0qzZwAAACoJhwOQ899u9m5HHtdc/l7eZiYCAAA4ApKtD/++EMPPvig6tatq1deeUWPPPKIdu7cqSVLlujgwYO6+eabSzMnAAAAqomFCQe0YX+aJKlFqL+Gdg43OREAAMBlzM75yiuvaO7cuUpMTFT//v31/vvvq3///rJaC/q4Ro0a6d1331VERERpZwUAAEAVdzLXrumLEp3LTw1oJTerxcREAAAABVwu0WbPnq27775bd911l+rWrVvkNnXq1NGcOXOuOBwAAACql/+s2KXk9IIZ4P/Soo6uaRpsciIAAIACLpdo27dvL3Ybm82mESNGXFYgAAAAVE8p6af05vKdkiR3q0VP9G9pciIAAICzXC7RzsjOzlZSUpJyc3MLjbdr1+6KQwEAAKD6eXFxok7m2SVJd1zVUJF1/ExOBAAAcJbLJdqRI0d01113adGiRUWut9vtVxwKAAAA1cufB9L0Rfx+SVKAl7vG9W5qciIAAIDCXJ6d86GHHlJaWpp+//13eXt7a9GiRXrvvffUtGlTff3112WREQAAAFWYYRh67tvNMoyC5bG9m6qmr83cUAAAAOdx+Uy0n376SV999ZU6deokq9Wqhg0b6rrrrlNAQICmTJmiAQMGlEVOAAAAVFGLN6Xo993HJUkRtXw0vGuEuYEAAACK4PKZaFlZWapTp44kqWbNmjpy5IgkqW3btoqPjy/ddAAAAKjScvMdmvL9FufyhP4tZXN3+SsqAABAmXP5G0rz5s2VmJgoSYqKitJbb72lAwcO6M0331TdunVLPSAAAACqrvdX7dHeY9mSpKsaB+n6ViEmJwIAACiay5dzjhs3TocOHZIkTZo0Sf369dNHH30km82md999t7TzAQAAoIo6npWrV+O2S5IsFumpAa1ksVhMTgUAAFA0l0u0O+64w/lzx44dtXfvXm3dulUNGjRQcHBwqYYDAABA1fXqj9uUcSpfkvTXDvXVpl6gyYkAAAAuzuUS7Xw+Pj7q0KFDaWQBAABANbHjcIY+/D1JkuRjc9MjfZubnAgAAODSSlSixcbGlviAr7zyymWHAQAAQPXwwndbZXcYkqT7ezZRSICXyYkAAAAurUQl2rp160p0MO5hAQAAgOL8vP2Iftp6WJJUN9BL93ZvbHIiAACA4pWoRFu6dGlZ5wAAAEA1kG936F/fbnEu/7Nfc3nb3ExMBAAAUDLWK9l537592rdvX2llAQAAQBX36R/7lZiSIUmKqh+om6PqmZwIAACgZFwu0fLz8/X0008rMDBQERERioiIUGBgoJ566inl5eWVRUYAAABUARmn8vTKkkTn8tM3tpLVyu1AAABA5eDy7JxjxozRggULNH36dHXt2lWStGrVKj3zzDM6duyYZs+eXeohAQAAUPnNWrpTRzNzJUkD2tZVp4ggkxMBAACUnMUwDMOVHQIDA/XJJ5/ohhtuKDT+3Xff6bbbblNaWlqpBixt6enpCgwMVFpamgICAsyOAwAAUC3sO56t3i8vV67dIZubVXHjeyo8yMfsWAAAACXuily+nNPT01MREREXjDdq1Eg2m83VwwEAAKAamLpoq3LtDknS3dc0okADAACVjssl2ujRo/Xcc88pJyfHOZaTk6Pnn39eo0ePvqwQs2bNUkREhLy8vBQTE6PVq1dfdNsFCxaoU6dOqlGjhnx9fRUdHa0PPvjgsp4XAAAAZW/t3uP634ZDkqRavjaN6tXE5EQAAACuc/meaOvWrVNcXJzq16+vqKgoSdL69euVm5ur3r17a8iQIc5tFyxYUOzx5s+fr9jYWL355puKiYnRjBkz1LdvXyUmJqpOnToXbB8UFKQnn3xSLVq0kM1m07fffquRI0eqTp066tu3r6svBwAAAGXI4TD07LdbnMux1zeTv5eHiYkAAAAuj8v3RBs5cmSJt507d26x28TExKhz586aOXOmJMnhcCg8PFxjxozR448/XqLn6dChgwYMGKDnnnuu2G25JxoAAED5+Xr9QY39eJ0kqVmIn74b213ubi5fDAEAAFBmStoVuXwmWkmKsZLKzc3V2rVrNWHCBOeY1WpVnz59tGrVqmL3NwxDP/30kxITEzVt2rQit8nJySl06Wl6evqVBwcAAECx8u0O/XvJNufykwNaUaABAIBKy9RvMUePHpXdbldISEih8ZCQECUnJ190v7S0NPn5+clms2nAgAF6/fXXdd111xW57ZQpUxQYGOh8hIeHl+prAAAAQNG+iN+v3UezJElXNQ5Sj6bBJicCAAC4fJXyT4H+/v5KSEjQmjVr9Pzzzys2NlbLli0rctsJEyYoLS3N+di3b1/5hgUAAKiGcvLtei1uh3P50b7NZbFYTEwEAABwZVy+nLM0BQcHy83NTSkpKYXGU1JSFBoaetH9rFarIiMjJUnR0dHasmWLpkyZomuvvfaCbT09PeXp6VmquQEAAHBpH/+epAOpJyVJvZrXVseGQSYnAgAAuDKmnolms9nUsWNHxcXFOcccDofi4uLUtWvXEh/H4XAUuu8ZAAAAzJOdm6+ZS3c6l8df39zENAAAAKWjRCVaUFCQjh49Kkm6++67lZGRUWoBYmNj9fbbb+u9997Tli1b9MADDygrK8s5C+jw4cMLTTwwZcoULVmyRLt27dKWLVv08ssv64MPPtAdd9xRapkAAABw+d77da+OZhb8gbN/21C1qRdociIAAIArV6LLOXNzc5Wenq7g4GC99957mjZtmvz9/UslwNChQ3XkyBFNnDhRycnJio6O1qJFi5yTDSQlJclqPdv1ZWVl6cEHH9T+/fvl7e2tFi1a6MMPP9TQoUNLJQ8AAAAuX/qpPL25vOAsNKtFir2umcmJAAAASofFMAyjuI2uu+46paSkqGPHjnrvvfc0dOhQeXt7F7ntO++8U+ohS1N6eroCAwOVlpamgIAAs+MAAABUKa8s2abX4rZLkoZ0qKdXbo02NxAAAEAxStoVlehMtA8//FD//ve/tXPnTlksFqWlpenUqVOlFhYAAACV3/GsXM35eZckyd1q0UO9OQsNAABUHSUq0UJCQjR16lRJUqNGjfTBBx+oVq1aZRoMAAAAlcvsZTuUlWuXJA3tHK4GtXxMTgQAAFB6SlSinWv37t1lkQMAAACVWEr6Kb2/aq8kydPdqjF/aWpyIgAAgNJVotk5z7d8+XLddNNNioyMVGRkpAYOHKiff/65tLMBAACgknj9p+3KyXdIkoZ3bajQQC+TEwEAAJQul0u0Dz/8UH369JGPj4/Gjh2rsWPHytvbW71799a8efPKIiMAAAAqsH3Hs/XJ6n2SJF+bmx64NtLkRAAAAKWvRLNznqtly5b6v//7Pz388MOFxl955RW9/fbb2rJlS6kGLG3MzgkAAFC6xn+6Xl/E75ckjf1LpGKvb25yIgAAgJIraVfk8plou3bt0k033XTB+MCBA7lfGgAAQDWz43CGvlxXUKAFenvoHz0am5wIAACgbLhcooWHhysuLu6C8R9//FHh4eGlEgoAAACVw7+XbJfj9HUN9/VsrAAvD3MDAQAAlBGXZ+ccP368xo4dq4SEBF199dWSpF9++UXvvvuuXn311VIPCAAAgIrpzwNp+t/GQ5KkYD9P3XV1hLmBAAAAypDLJdoDDzyg0NBQvfzyy/r0008lFdwnbf78+br55ptLPSAAAAAqpleWbHP+PKpXE/nYXP5qCQAAUGlc1jedwYMHa/DgwaWdBQAAAJXE2r0n9NPWw5KksEAv3R7TwOREAAAAZcvle6IBAAAALy1OdP48tndTebq7mZgGAACg7FGiAQAAwCW/7DiqVbuOSZIiavnolo71TU4EAABQ9ijRAAAAUGKGYejFc85Ce/i6ZvJw4yslAACo+vjGAwAAgBKL23JYCftSJUnNQ/x1U7swcwMBAACUE5dLtKVLl5ZFDgAAAFRwDoehl344exZa7PXNZLVaTEwEAABQflwu0fr166cmTZroX//6l/bt21cWmQAAAFAB/W/jIW1NzpAkRdUP1PWtQkxOBAAAUH5cLtEOHDig0aNH6/PPP1fjxo3Vt29fffrpp8rNzS2LfAAAAKgA8u0O/XvJNufy+Ouby2LhLDQAAFB9uFyiBQcH6+GHH1ZCQoJ+//13NWvWTA8++KDCwsI0duxYrV+/vixyAgAAwEQL1h3QrqNZkqQujYLUvWmwyYkAAADK1xVNLNChQwdNmDBBo0ePVmZmpt555x117NhR3bt316ZNm0orIwAAAEyUk2/Xqz9udy4/2pez0AAAQPVzWSVaXl6ePv/8c/Xv318NGzbU4sWLNXPmTKWkpGjHjh1q2LCh/va3v5V2VgAAAJhg/pp9OpB6UpLUs1ltdY4IMjkRAABA+XN3dYcxY8bo448/lmEYuvPOOzV9+nS1adPGud7X11cvvfSSwsKY7hwAAKCyO5lr1+s/7XAuP3J9cxPTAAAAmMflEm3z5s16/fXXNWTIEHl6eha5TXBwsJYuXXrF4QAAAGCu91ft0ZGMHElSv9ahals/0OREAAAA5nD5cs5Jkybpb3/72wUFWn5+vlasWCFJcnd3V8+ePUsnIQAAAEyRcSpPs5fvlCRZLNL465uZnAgAAMA8LpdovXr10vHjxy8YT0tLU69evUolFAAAAMw3Z+VupWbnSZIGR9dT0xB/kxMBAACYx+USzTCMImdjOnbsmHx9fUslFAAAAMx1IitX//15tyTJ3WrRQ304Cw0AAFRvJb4n2pAhQyRJFotFd911V6HLOe12uzZs2KCrr7669BMCAACg3L25Yqcyc/IlSbd2DleDWj4mJwIAADBXiUu0wMCCm8gahiF/f395e3s719lsNl111VW69957Sz8hAAAAytXh9FN679c9kiSbu1Vj/hJpbiAAAIAKoMQl2ty5cyVJEREReuSRR7h0EwAAoIqatXSHTuU5JEl3XtVQdQO9i9kDAACg6itxiXbGpEmTyiIHAAAAKoB9x7M1b3WSJMnH5qYHrm1iciIAAICKoUQlWocOHRQXF6eaNWuqffv2RU4scEZ8fHyphQMAAED5ei1uu/LshiTp7m6NFOznWcweAAAA1UOJSrSbb77ZOZHAoEGDyjIPAAAATLLzSKa+iN8vSQrwcte9PRqbnAgAAKDisBiGYZgdojylp6crMDBQaWlpCggIMDsOAABAhTF6Xry+3XBIkvRo3+Ya1YsJBQAAQNVX0q7IWo6ZAAAAUEFtPpjuLNCC/Wy66+oIcwMBAABUMCW6nLNmzZqXvA/auY4fP35FgQAAAFD+XlmS6Pz5gWsj5evp8vxTAAAAVVqJvh3NmDGjjGMAAADALPFJJ/TjlsOSpLqBXhoW08DkRAAAABVPiUq0ESNGlHUOAAAAmOTlH86ehTbmL03l5eFmYhoAAICKqUQlWnp6uvPGaunp6Zfclpv1AwAAVB6/7jyqX3YckyQ1rOWjv3Wqb3IiAACAiqnE90Q7dOiQ6tSpoxo1ahR5fzTDMGSxWGS320s9JAAAAEqfYRh6afHZs9Ae6tNUHm7MOwUAAFCUEpVoP/30k4KCgiRJS5cuLdNAAAAAKB9LEw8rPilVktS0jp8GRtUzNxAAAEAFVqISrWfPnkX+DAAAgMrJ4TD00uJtzuXx1zeTm7Vks7EDAABUR5c1d/mJEyc0Z84cbdmyRZLUqlUrjRw50nm2GgAAACq27/9M1uZDBfe6bVsvUH1bh5qcCAAAoGJz+aYXK1asUEREhF577TWdOHFCJ06c0GuvvaZGjRppxYoVZZERAAAApSjP7tDLS87eC2389c2KvOctAAAAznL5TLRRo0Zp6NChmj17ttzcCqY/t9vtevDBBzVq1Cht3Lix1EMCAACg9Hy8Okm7jmRJkrpEBKlns9omJwIAAKj4XD4TbceOHRo/fryzQJMkNzc3xcbGaseOHZcVYtasWYqIiJCXl5diYmK0evXqi2779ttvq3v37qpZs6Zq1qypPn36XHJ7AAAAnJV+Kk8zftzuXH5iQEvOQgMAACgBl0u0Dh06OO+Fdq4tW7YoKirK5QDz589XbGysJk2apPj4eEVFRalv3746fPhwkdsvW7ZMt912m5YuXapVq1YpPDxc119/vQ4cOODycwMAAFQ3s5ft1PGsXEnSwKgwRYfXMDcQAABAJWExDMMobqMNGzY4f96yZYv++c9/asyYMbrqqqskSb/99ptmzZqlqVOnaujQoS4FiImJUefOnTVz5kxJksPhUHh4uMaMGaPHH3+82P3tdrtq1qypmTNnavjw4cVun56ersDAQKWlpSkgIMClrAAAAJXZgdST6vXSMuXmO2RzsypufE+FB/mYHQsAAMBUJe2KSnRPtOjoaFksFp3bt/3zn/+8YLvbb7/dpRItNzdXa9eu1YQJE5xjVqtVffr00apVq0p0jOzsbOXl5V10ZtCcnBzl5OQ4l9PT00ucDwAAoCp5aXGicvMdkqSR3SIo0AAAAFxQohJt9+7dZfLkR48eld1uV0hISKHxkJAQbd26tUTHeOyxxxQWFqY+ffoUuX7KlCmaPHnyFWcFAACozDbsT9WX6wpuf1HTx0MP9oo0OREAAEDlUqISrWHDhmWd47JMnTpVn3zyiZYtWyYvL68it5kwYYJiY2Ody+np6QoPDy+viAAAAKYzDEPP/+/sPW3H9W6qQG8PExMBAABUPiUq0YqyefNmJSUlKTc3t9D4wIEDS3yM4OBgubm5KSUlpdB4SkqKQkNDL7nvSy+9pKlTp+rHH39Uu3btLrqdp6enPD09S5wJAACgqvlxy2H9vvu4JKlRsK9uj6mYfyAFAACoyFwu0Xbt2qXBgwdr48aNhe6TdmZqdLvdXuJj2Ww2dezYUXFxcRo0aJCkgokF4uLiNHr06IvuN336dD3//PNavHixOnXq5OpLAAAAqDby7A5N+f7sWWiP9Wshm7vLE7QDAABUey5/gxo3bpwaNWqkw4cPy8fHR5s2bdKKFSvUqVMnLVu2zOUAsbGxevvtt/Xee+9py5YteuCBB5SVlaWRI0dKkoYPH15o4oFp06bp6aef1jvvvKOIiAglJycrOTlZmZmZLj83AABAVffx6iTtOpIlSeoSEaS+rUOK2QMAAABFcflMtFWrVumnn35ScHCwrFarrFarrrnmGk2ZMkVjx47VunXrXDre0KFDdeTIEU2cOFHJycmKjo7WokWLnJMNJCUlyWo92/XNnj1bubm5+utf/1roOJMmTdIzzzzj6ssBAACostJP5WnGj9udy08MaOm8egAAAACucblEs9vt8vf3l1RwT7ODBw+qefPmatiwoRITEy8rxOjRoy96+eb5Z7ft2bPnsp4DAACgupm9bKeOZxXcv3ZgVJiiw2uYGwgAAKASc7lEa9OmjdavX69GjRopJiZG06dPl81m03/+8x81bty4LDICAADARQdST2rOyt2SJJubVY/2bW5yIgAAgMrN5RLtqaeeUlZWwX01nn32Wd14443q3r27atWqpfnz55d6QAAAALjuxUVblZvvkCSN7Bah8CAfkxMBAABUbi6XaH379nX+HBkZqa1bt+r48eOqWbMm99gAAACoADbsT9XChIOSpJo+HnqwV6TJiQAAACo/l0u0c+3bt0+SFB4eXiphAAAAcGUMw9Dz/9viXB7Xu6kCvT1MTAQAAFA1WIvfpLD8/Hw9/fTTCgwMVEREhCIiIhQYGKinnnpKeXl5ZZERAAAAJfTjlsP6ffdxSVKjYF/dHtPQ5EQAAABVg8tnoo0ZM0YLFizQ9OnT1bVrV0nSqlWr9Mwzz+jYsWOaPXt2qYcEAABA8fLsDk35/uxZaI/1ayGbu8t/MwUAAEARXC7R5s2bp08++UQ33HCDc6xdu3YKDw/XbbfdRokGAABgko9XJ2nXkYIJoLpEBKlv6xCTEwEAAFQdLv9p0tPTUxEREReMN2rUSDabrTQyAQAAwEXpp/I048ftzuUnBrRk0icAAIBS5HKJNnr0aD333HPKyclxjuXk5Oj555/X6NGjSzUcAAAASmb2sp06npUrSRoYFabo8BrmBgIAAKhiSnQ555AhQwot//jjj6pfv76ioqIkSevXr1dubq569+5d+gkBAABwSQdST2rOyt2SJJubVY/2bW5yIgAAgKqnRCVaYGBgoeVbbrml0HJ4eHjpJQIAAIBLXly0Vbn5DknSyG4RCg/yMTkRAABA1VOiEm3u3LllnQMAAACXYcP+VC1MOChJqunjoQd7RZqcCAAAoGpyeXbOM44cOaLExERJUvPmzVW7du1SCwUAAIDiGYah5/+3xbk8rndTBXp7mJgIAACg6nJ5YoGsrCzdfffdqlu3rnr06KEePXooLCxM99xzj7Kzs8siIwAAAIrw45bD+n33cUlSo2Bf3R7T0OREAAAAVZfLJVpsbKyWL1+ub775RqmpqUpNTdVXX32l5cuXa/z48WWREQAAAOfJszs05buzZ6E91q+FbO4uf7UDAABACbl8OecXX3yhzz//XNdee61zrH///vL29tatt96q2bNnl2Y+AAAAFOHj1UnadTRLktQlIkh9W4eYnAgAAKBqc/nPldnZ2QoJufBLWp06dbicEwAAoBykn8rTjB+3O5efGNBSFovFxEQAAABVn8slWteuXTVp0iSdOnXKOXby5ElNnjxZXbt2LdVwAAAAuNDsZTt1PCtXkjQwKkzR4TXMDQQAAFANuHw554wZM9SvXz/Vr19fUVFRkqT169fLy8tLixcvLvWAAAAAOGv/iWzNWblbkmRzs+rRvs1NTgQAAFA9uFyitW3bVtu3b9dHH32krVu3SpJuu+02DRs2TN7e3qUeEAAAAGe9tDhRufkOSdLIbhEKD/IxOREAAED14FKJlpeXpxYtWujbb7/VvffeW1aZAAAAUIQN+1O1MOGgJKmmj4ce7BVpciIAAIDqw6V7onl4eBS6FxoAAADKh2EYev5/W5zL43o3VaC3h4mJAAAAqheXJxYYNWqUpk2bpvz8/LLIAwAAgCL8uOWwft99XJLUKNhXt8c0NDkRAABA9eLyPdHWrFmjuLg4/fDDD2rbtq18fX0LrV+wYEGphQMAAICUZ3doyndnz0J7rF8L2dxd/lsoAAAAroDLJVqNGjV0yy23lEUWAAAAFOHj1UnadTRLktQlIkh9W4eYnAgAAKD6cblEmzt3blnkAAAAQBHST+Vpxo/bnctPDGgpi8ViYiIAAIDqqcTXATgcDk2bNk3dunVT586d9fjjj+vkyZNlmQ0AAKDam71sp45n5UqSBkaFKTq8hrmBAAAAqqkSl2jPP/+8nnjiCfn5+alevXp69dVXNWrUqLLMBgAAUK3tP5GtOSt3S5JsblY92re5yYkAAACqrxKXaO+//77eeOMNLV68WAsXLtQ333yjjz76SA6HoyzzAQAAVFsvLU5Ubn7Bd62R3SIUHuRjciIAAIDqq8QlWlJSkvr37+9c7tOnjywWiw4ePFgmwQAAAKqzDftTtTCh4HtWTR8PPdgr0uREAAAA1VuJS7T8/Hx5eXkVGvPw8FBeXl6phwIAAKjODMPQ8//b4lwe17upAr09TEwEAACAEs/OaRiG7rrrLnl6ejrHTp06pfvvv1++vr7OsQULFpRuQgAAgGpmyeYU/b77uCSpUbCvbo9paHIiAAAAlLhEGzFixAVjd9xxR6mGAQAAqO7y7A5N/X6rc/mxfi1kcy/xxQMAAAAoIyUu0ebOnVuWOQAAACDp49VJ2nU0S5LUJSJIfVuHmJwIAAAAkgv3RAMAAEDZSs3O1YwftzuXnxjQUhaLxcREAAAAOIMSDQAAoAIwDEOPfLZBx7NyJUkDo8IUHV7D3FAAAABwokQDAACoAOb+skc/bkmRJNX08dCE/i1MTgQAAIBzUaIBAACYbP2+VE35fotz+ZVbo1U30NvERAAAADgfJRoAAICJ0k7mafTH8cqzG5Kk+3o0Vq8WdUxOBQAAgPNRogEAAJjEMAw9/sUG7Tt+UpLUvkENPdK3ucmpAAAAUBRKNAAAAJN88Nteff9nsiQp0NtDr9/WXh5ufD0DAACoiPiWBgAAYII/D6TpX9+evQ/ai39tp/o1fUxMBAAAgEuhRAMAAChnGafyNGpevHLtDknS3d0a6frWoSanAgAAwKVQogEAAJQjwzA0YcFG7T2WLUmKqh+ox29oYXIqAAAAFIcSDQAAoBzNW52kbzcckiT5e7lr5u0dZHPnKxkAAEBFZ/o3tlmzZikiIkJeXl6KiYnR6tWrL7rtpk2bdMsttygiIkIWi0UzZswov6AAAABXaPPBdE3+ZrNz+cW/tlN4EPdBAwAAqAxMLdHmz5+v2NhYTZo0SfHx8YqKilLfvn11+PDhIrfPzs5W48aNNXXqVIWGct8QAABQeWTm5Gv0vHjl5hfcB21E14bq16auyakAAABQUqaWaK+88oruvfdejRw5Uq1atdKbb74pHx8fvfPOO0Vu37lzZ7344ov6+9//Lk9Pz3JOCwAAcHkMw9BTX27UrqNZkqQ29QL0xICWJqcCAACAK0wr0XJzc7V27Vr16dPnbBirVX369NGqVatK7XlycnKUnp5e6AEAAFCePvtjvxYmHJQk+Xm6a+ZtHeTp7mZyKgAAALjCtBLt6NGjstvtCgkJKTQeEhKi5OTkUnueKVOmKDAw0PkIDw8vtWMDAAAUZ1tKhiZ+/adzeeotbRUR7GtiIgAAAFwO0ycWKGsTJkxQWlqa87Fv3z6zIwEAgGoiOzdfD34Ur1N5BfdBuz2mgW5sF2ZyKgAAAFwOd7OeODg4WG5ubkpJSSk0npKSUqqTBnh6enL/NAAAYIqJX23SjsOZkqQWof6aeGMrkxMBAADgcpl2JprNZlPHjh0VFxfnHHM4HIqLi1PXrl3NigUAAFAqvli7X5+v3S9J8rG5adawDvLy4D5oAAAAlZVpZ6JJUmxsrEaMGKFOnTqpS5cumjFjhrKysjRy5EhJ0vDhw1WvXj1NmTJFUsFkBJs3b3b+fODAASUkJMjPz0+RkZGmvQ4AAIBz7TicoacWnr0P2guD26pJbT8TEwEAAOBKmVqiDR06VEeOHNHEiROVnJys6OhoLVq0yDnZQFJSkqzWsyfLHTx4UO3bt3cuv/TSS3rppZfUs2dPLVu2rLzjAwAAXOBkrl2jPlqnk3l2SdLQTuEa1L6eyakAAABwpSyGYRhmhyhP6enpCgwMVFpamgICAsyOAwAAqpjHv9igT9YUTGTUPMRfC0d1k7eNyzgBAAAqqpJ2RVV+dk4AAIDy8lXCAWeB5u3hplnD2lOgAQAAVBGUaAAAAKVg15FMPbFgo3P5uUFtFFnH38REAAAAKE2UaAAAAFfoVJ5do+atU1ZuwX3QbulQX3/tWN/kVAAAAChNlGgAAABX6F//26wth9IlSZF1/PTcoNYmJwIAAEBpo0QDAAC4At9uOKgPf0uSJHm6WzXr9g7ysZk6AToAAADKACUaAADAZdp7LEuPf3H2PmiTB7ZW81DugwYAAFAVUaIBAABchpx8u0bNi1dmTr4k6eboMA3tHG5yKgAAAJQVSjQAAIDLMOW7rfrzQMF90BoH++r5wW1lsVhMTgUAAICyQokGAADgokV/HtK7v+6RJNncrZp5ewf5eXIfNAAAgKqMEg0AAMAF+45n69HPNziXJ97YSq3CAkxMBAAAgPJAiQYAAFBCufkOjZ4Xr4xTBfdBG9CurobFNDA5FQAAAMoDJRoAAEAJTVu0Vev3p0mSGtby0dQh3AcNAACguqBEAwAAKIElm1M0Z+VuSZLNzapZt3eQv5eHyakAAABQXijRAAAAirH/RLYe+Wy9c/nJAS3Vpl6giYkAAABQ3ijRAAAALmHD/lT9dfYqpZ3MkyT1ax2q4V0bmpwKAAAA5Y252AEAAC7iq4QD+ufnG5ST75BUcB+0aX9tx33QAAAAqiFKNAAAgPPYHYamL96qt5bvco51alhTs+/oqEBv7oMGAABQHVGiAQAAnCPtZJ7GfbJOyxKPOMf+3jlck29uLU93NxOTAQAAwEyUaAAAAKftPJKpe9//Q7uOZEmS3KwWTbqple68qiGXcAIAAFRzlGgAAACSliYe1tiP1ynjVL4kqaaPh2YN66CrmwSbnAwAAAAVASUaAACo1gzD0H9W7NLURVtlGAVjLUL99fbwTgoP8jE3HAAAACoMSjQAAFBtncqz6/EvNmhhwkHnWN/WIXrl1mj5evI1CQAAAGfx7RAAAFRLh9JO6r4P1mrD/jTn2EN9mmrsX5rKauX+ZwAAACiMEg0AAFQ7a/ce130fxOtoZo4kycfmpldujVK/NnVNTgYAAICKihINAABUK5+u2aenFv6pXLtDkhQe5K23h3dSi9AAk5MBAACgIqNEAwAA1UK+3aF//W+L3v11j3Osa+NamjWsg4J8beYFAwAAQKVAiQYAAKq8E1m5GjUvXr/uPOYcG9G1oZ66sZU83KwmJgMAAEBlQYkGAACqtMTkDN37/h9KOp4tSfJws+i5m9vo710amJwMAAAAlQklGgAAqLIWb0pW7PwEZeXaJUnBfja9eUdHdYoIMjkZAAAAKhtKNAAAUOU4HIZe/2mH/v3jNudY23qBeuvOjgqr4W1iMgAAAFRWlGgAAKBKycrJ1yOfrdf3fyY7x26ODtO0W9rJy8PNxGQAAACozCjRAABAlbHveLbuff8PbU3OkCRZLNJj/Vrovh6NZbFYTE4HAACAyowSDQAAVAmrdh7Tgx+t1YnsPEmSv6e7XrutvXq1qGNyMgAAAFQFlGgAAKBSMwxDH/62V5O/2ax8hyFJahzsq/8M76TIOn4mpwMAAEBVQYkGAAAqrdx8hyZ9vUkfr05yjvVsVluv3dZegd4eJiYDAABAVUOJBgAAKp3ktFP6KuGAPlu7XzsOZzrH7+vRWP/s10JuVu5/BgAAgNJFiQYAACqFjFN5WvRnshYmHNCvO4/JMM6u83S3atot7TSofT3zAgIAAKBKo0QDAAAVVp7doZ+3H9GX6w5qyeZkncpzXLBNx4Y1NemmVmpXv0b5BwQAAEC1QYkGAAAqFMMwtH5/mhauO6Bv1h/UsazcC7ZpWMtHg9vX06DoeooI9jUhJQAAAKobSjQAAFAhJB3L1sKEA1q47oB2Hc26YH1NHw/dFBWmQe3rqX14DVks3PcMAAAA5YcSDQAAmOZEVq7+t/GQFq47oD/2nrhgvc3dqutahWhwdD31aFZbNnerCSkBAAAASjQAAFDOTuXZtXTrYS1Yd0DLEg8rz24UWm+xSFc1qqXB7eupX9tQBXh5mJQUAAAAOIsSDQAAlDmHw9CaPcf15boD+t/GQ8o4lX/BNs1C/DS4fX3dHB2msBreJqQEAAAALo4SDQAAlJkdhzO0IP6Avko4qAOpJy9YX8ffUzdHF9znrFXdAO5zBgAAgAqrQpRos2bN0osvvqjk5GRFRUXp9ddfV5cuXS66/Weffaann35ae/bsUdOmTTVt2jT179+/HBMDAIAz8uwOHc/K1ZGMHB3LytWxzBwdTD2pRZuS9eeB9Au297G5qV+bUA1uX09XNwmWm5XiDAAAABWf6SXa/PnzFRsbqzfffFMxMTGaMWOG+vbtq8TERNWpU+eC7X/99VfddtttmjJlim688UbNmzdPgwYNUnx8vNq0aWPCKwAAoGoxDEOZOfk6mllQiB3NzNXRzBwdy8zVsawcHT09dmZd2sm8Yo/pZrWoe9NgDW5fT9e1CpGPzfSvIAAAAIBLLIZhGMVvVnZiYmLUuXNnzZw5U5LkcDgUHh6uMWPG6PHHH79g+6FDhyorK0vffvutc+yqq65SdHS03nzzzWKfLz09XYGBgUpLS1NAQEDpvRCTZOXkF3l5DAAARTlz1tix08XY2TKs4Cyyoxk5OpqVq9x8R6k8X7v6gRoUXU83RYWptr9nqRwTAAAAKE0l7YpM/TNwbm6u1q5dqwkTJjjHrFar+vTpo1WrVhW5z6pVqxQbG1torG/fvlq4cGGR2+fk5CgnJ8e5nJ5+4WUllVl80gndOWe12TEAANWQr81Nwf6equVrUy0/TwX7eSrYz6ZgP08F+drUKixATWr7mR0TAAAAKBWmlmhHjx6V3W5XSEhIofGQkBBt3bq1yH2Sk5OL3D45ObnI7adMmaLJkyeXTmAAAKowq0UK8i0owmqdLsNq+Xqqlp9Ntf0K/q11uiir5espb5ub2ZEBAACAclPlb0gyYcKEQmeupaenKzw83MREpSskwEtDO1Wd1wMAKFtWq0VBvh6q5eupYH9PBfueLcZq+Ni4yT8AAABwEaaWaMHBwXJzc1NKSkqh8ZSUFIWGhha5T2hoqEvbe3p6ytOz6t6DpVmIv6b9tZ3ZMQAAAAAAAKo0q5lPbrPZ1LFjR8XFxTnHHA6H4uLi1LVr1yL36dq1a6HtJWnJkiUX3R4AAAAAAAC4UqZfzhkbG6sRI0aoU6dO6tKli2bMmKGsrCyNHDlSkjR8+HDVq1dPU6ZMkSSNGzdOPXv21Msvv6wBAwbok08+0R9//KH//Oc/Zr4MAAAAAAAAVGGml2hDhw7VkSNHNHHiRCUnJys6OlqLFi1yTh6QlJQkq/XsCXNXX3215s2bp6eeekpPPPGEmjZtqoULF6pNmzZmvQQAAAAAAABUcRbDMAyzQ5Sn9PR0BQYGKi0tTQEBAWbHAQAAAAAAgIlK2hWZek80AAAAAAAAoDKgRAMAAAAAAACKQYkGAAAAAAAAFIMSDQAAAAAAACgGJRoAAAAAAABQDEo0AAAAAAAAoBiUaAAAAAAAAEAxKNEAAAAAAACAYlCiAQAAAAAAAMWgRAMAAAAAAACK4W52gPJmGIYkKT093eQkAAAAAAAAMNuZjuhMZ3Qx1a5Ey8jIkCSFh4ebnAQAAAAAAAAVRUZGhgIDAy+63mIUV7NVMQ6HQwcPHpS/v78sFovZcUpFenq6wsPDtW/fPgUEBJgdBybj/YBz8X7AuXg/4Hy8J3Au3g84F+8HnIv3A85VFd8PhmEoIyNDYWFhslovfuezancmmtVqVf369c2OUSYCAgKqzBsYV473A87F+wHn4v2A8/GewLl4P+BcvB9wLt4POFdVez9c6gy0M5hYAAAAAAAAACgGJRoAAAAAAABQDEq0KsDT01OTJk2Sp6en2VFQAfB+wLl4P+BcvB9wPt4TOBfvB5yL9wPOxfsB56rO74dqN7EAAAAAAAAA4CrORAMAAAAAAACKQYkGAAAAAAAAFIMSDQAAAAAAACgGJRoAAAAAAABQDEq0KmDWrFmKiIiQl5eXYmJitHr1arMjwQTPPPOMLBZLoUeLFi3MjoVysmLFCt10000KCwuTxWLRwoULC603DEMTJ05U3bp15e3trT59+mj79u3mhEWZK+79cNddd13wedGvXz9zwqLMTZkyRZ07d5a/v7/q1KmjQYMGKTExsdA2p06d0qhRo1SrVi35+fnplltuUUpKikmJUZZK8n649tprL/iMuP/++01KjLI0e/ZstWvXTgEBAQoICFDXrl31/fffO9fz2VC9FPd+4LOheps6daosFoseeugh51h1/IygRKvk5s+fr9jYWE2aNEnx8fGKiopS3759dfjwYbOjwQStW7fWoUOHnI+VK1eaHQnlJCsrS1FRUZo1a1aR66dPn67XXntNb775pn7//Xf5+vqqb9++OnXqVDknRXko7v0gSf369Sv0efHxxx+XY0KUp+XLl2vUqFH67bfftGTJEuXl5en6669XVlaWc5uHH35Y33zzjT777DMtX75cBw8e1JAhQ0xMjbJSkveDJN17772FPiOmT59uUmKUpfr162vq1Klau3at/vjjD/3lL3/RzTffrE2bNknis6G6Ke79IPHZUF2tWbNGb731ltq1a1dovFp+Rhio1Lp06WKMGjXKuWy3242wsDBjypQpJqaCGSZNmmRERUWZHQMVgCTjyy+/dC47HA4jNDTUePHFF51jqamphqenp/Hxxx+bkBDl6fz3g2EYxogRI4ybb77ZlDww3+HDhw1JxvLlyw3DKPg88PDwMD777DPnNlu2bDEkGatWrTIrJsrJ+e8HwzCMnj17GuPGjTMvFExVs2ZN47///S+fDTAM4+z7wTD4bKiuMjIyjKZNmxpLliwp9B6orp8RnIlWieXm5mrt2rXq06ePc8xqtapPnz5atWqViclglu3btyssLEyNGzfWsGHDlJSUZHYkVAC7d+9WcnJyoc+KwMBAxcTE8FlRjS1btkx16tRR8+bN9cADD+jYsWNmR0I5SUtLkyQFBQVJktauXau8vLxCnxEtWrRQgwYN+IyoBs5/P5zx0UcfKTg4WG3atNGECROUnZ1tRjyUI7vdrk8++URZWVnq2rUrnw3V3PnvhzP4bKh+Ro0apQEDBhT6LJCq7/cHd7MD4PIdPXpUdrtdISEhhcZDQkK0detWk1LBLDExMXr33XfVvHlzHTp0SJMnT1b37t31559/yt/f3+x4MFFycrIkFflZcWYdqpd+/fppyJAhatSokXbu3KknnnhCN9xwg1atWiU3Nzez46EMORwOPfTQQ+rWrZvatGkjqeAzwmazqUaNGoW25TOi6ivq/SBJt99+uxo2bKiwsDBt2LBBjz32mBITE7VgwQIT06KsbNy4UV27dtWpU6fk5+enL7/8Uq1atVJCQgKfDdXQxd4PEp8N1dEnn3yi+Ph4rVmz5oJ11fX7AyUaUEXccMMNzp/btWunmJgYNWzYUJ9++qnuueceE5MBqGj+/ve/O39u27at2rVrpyZNmmjZsmXq3bu3iclQ1kaNGqU///yTe2ZC0sXfD//3f//n/Llt27aqW7euevfurZ07d6pJkyblHRNlrHnz5kpISFBaWpo+//xzjRgxQsuXLzc7FkxysfdDq1at+GyoZvbt26dx48ZpyZIl8vLyMjtOhcHlnJVYcHCw3NzcLpj9IiUlRaGhoSalQkVRo0YNNWvWTDt27DA7Ckx25vOAzwpcTOPGjRUcHMznRRU3evRoffvtt1q6dKnq16/vHA8NDVVubq5SU1MLbc9nRNV2sfdDUWJiYiSJz4gqymazKTIyUh07dtSUKVMUFRWlV199lc+Gaupi74ei8NlQta1du1aHDx9Whw4d5O7uLnd3dy1fvlyvvfaa3N3dFRISUi0/IyjRKjGbzaaOHTsqLi7OOeZwOBQXF1founVUT5mZmdq5c6fq1q1rdhSYrFGjRgoNDS30WZGenq7ff/+dzwpIkvbv369jx47xeVFFGYah0aNH68svv9RPP/2kRo0aFVrfsWNHeXh4FPqMSExMVFJSEp8RVVBx74eiJCQkSBKfEdWEw+FQTk4Onw2QdPb9UBQ+G6q23r17a+PGjUpISHA+OnXqpGHDhjl/ro6fEVzOWcnFxsZqxIgR6tSpk7p06aIZM2YoKytLI0eONDsaytkjjzyim266SQ0bNtTBgwc1adIkubm56bbbbjM7GspBZmZmob8C7t69WwkJCQoKClKDBg300EMP6V//+peaNm2qRo0a6emnn1ZYWJgGDRpkXmiUmUu9H4KCgjR58mTdcsstCg0N1c6dO/XPf/5TkZGR6tu3r4mpUVZGjRqlefPm6auvvpK/v7/zPiWBgYHy9vZWYGCg7rnnHsXGxiooKEgBAQEaM2aMunbtqquuusrk9Chtxb0fdu7cqXnz5ql///6qVauWNmzYoIcfflg9evRQu3btTE6P0jZhwgTdcMMNatCggTIyMjRv3jwtW7ZMixcv5rOhGrrU+4HPhurH39+/0P0yJcnX11e1atVyjlfLzwizpwfFlXv99deNBg0aGDabzejSpYvx22+/mR0JJhg6dKhRt25dw2azGfXq1TOGDh1q7Nixw+xYKCdLly41JF3wGDFihGEYhuFwOIynn37aCAkJMTw9PY3evXsbiYmJ5oZGmbnU+yE7O9u4/vrrjdq1axseHh5Gw4YNjXvvvddITk42OzbKSFHvBUnG3LlznducPHnSePDBB42aNWsaPj4+xuDBg41Dhw6ZFxplprj3Q1JSktGjRw8jKCjI8PT0NCIjI41HH33USEtLMzc4ysTdd99tNGzY0LDZbEbt2rWN3r17Gz/88INzPZ8N1cul3g98NsAwDKNnz57GuHHjnMvV8TPCYhiGUZ6lHQAAAAAAAFDZcE80AAAAAAAAoBiUaAAAAAAAAEAxKNEAAAAAAACAYlCiAQAAAAAAAMWgRAMAAAAAAACKQYkGAAAAAAAAFIMSDQAAAAAAACgGJRoAAAAAAABQDEo0AACACmDPnj2yWCxKSEgwO4rT1q1bddVVV8nLy0vR0dFmxymRZcuWyWKxKDU11ewoAACgiqFEAwAAkHTXXXfJYrFo6tSphcYXLlwoi8ViUipzTZo0Sb6+vkpMTFRcXJzZcQAAAExFiQYAAHCal5eXpk2bphMnTpgdpdTk5uZe9r47d+7UNddco4YNG6pWrVpl/nwAAAAVGSUaAADAaX369FFoaKimTJly0W2eeeaZCy5tnDFjhiIiIpzLd911lwYNGqQXXnhBISEhqlGjhp599lnl5+fr0UcfVVBQkOrXr6+5c+decPytW7fq6quvlpeXl9q0aaPly5cXWv/nn3/qhhtukJ+fn0JCQnTnnXfq6NGjzvXXXnutRo8erYceekjBwcHq27dvka/D4XDo2WefVf369eXp6ano6GgtWrTIud5isWjt2rV69tlnZbFY9MwzzxR5nIs93/Lly9WlSxd5enqqbt26evzxx5Wfn+/cLyIiQjNmzCh0rOjo6ELPY7FY9N///leDBw+Wj4+PmjZtqq+//rrQPt99952aNWsmb29v9erVS3v27Cm0fu/evbrppptUs2ZN+fr6qnXr1vruu++KfC0AAACXQokGAABwmpubm1544QW9/vrr2r9//xUd66efftLBgwe1YsUKvfLKK5o0aZJuvPFG1axZU7///rvuv/9+3XfffRc8z6OPPqrx48dr3bp16tq1q2666SYdO3ZMkpSamqq//OUvat++vf744w8tWrRIKSkpuvXWWwsd47333pPNZtMvv/yiN998s8h8r776ql5++WW99NJL2rBhg/r27auBAwdq+/btkqRDhw6pdevWGj9+vA4dOqRHHnnkoq/1/Oc7cOCA+vfvr86dO2v9+vWaPXu25syZo3/9618u/x4nT56sW2+9VRs2bFD//v01bNgwHT9+XJK0b98+DRkyRDfddJMSEhL0j3/8Q48//nih/UeNGqWcnBytWLFCGzdu1LRp0+Tn5+dyDgAAAEo0AACAcwwePFjR0dGaNGnSFR0nKChIr732mpo3b667775bzZs3V3Z2tp544gk1bdpUEyZMkM1m08qVKwvtN3r0aN1yyy1q2bKlZs+ercDAQM2ZM0eSNHPmTLVv314vvPCCWrRoofbt2+udd97R0qVLtW3bNucxmjZtqunTp6t58+Zq3rx5kfleeuklPfbYY/r73/+u5s2ba9q0aYqOjnaeHRYaGip3d3f5+fkpNDT0ksXT+c/3xhtvKDw8XDNnzlSLFi00aNAgTZ48WS+//LIcDodLv8e77rpLt912myIjI/XCCy8oMzNTq1evliTNnj1bTZo00csvv6zmzZtr2LBhuuuuuwrtn5SUpG7duqlt27Zq3LixbrzxRvXo0cOlDAAAABIlGgAAwAWmTZum9957T1u2bLnsY7Ru3VpW69mvWiEhIWrbtq1z2c3NTbVq1dLhw4cL7de1a1fnz+7u7urUqZMzx/r167V06VL5+fk5Hy1atJBUcP+yMzp27HjJbOnp6Tp48KC6detWaLxbt26X9ZrPf74tW7aoa9euhSZk6NatmzIzM10+w69du3bOn319fRUQEOD8nW3ZskUxMTGFtj/39ydJY8eO1b/+9S9169ZNkyZN0oYNG1x6fgAAgDMo0QAAAM7To0cP9e3bVxMmTLhgndVqlWEYhcby8vIu2M7Dw6PQssViKXLMlTOzMjMznZcunvvYvn17obOrfH19S3zM0nA5z3clv0dXfmf/+Mc/tGvXLt15553auHGjOnXqpNdff93lvAAAAJRoAAAARZg6daq++eYbrVq1qtB47dq1lZycXKgASkhIKLXn/e2335w/5+fna+3atWrZsqUkqUOHDtq0aZMiIiIUGRlZ6OFKkRUQEKCwsDD98ssvhcZ/+eUXtWrV6opfQ8uWLbVq1apCv6NffvlF/v7+ql+/vqSC3+OhQ4ec69PT07V7926Xn+fMpZ1nnPv7OyM8PFz333+/FixYoPHjx+vtt9926XkAAAAkSjQAAIAitW3bVsOGDdNrr71WaPzaa6/VkSNHNH36dO3cuVOzZs3S999/X2rPO2vWLH355ZfaunWrRo0apRMnTujuu++WVHCT/OPHj+u2227TmjVrtHPnTi1evFgjR46U3W536XkeffRRTZs2TfPnz1diYqIef/xxJSQkaNy4cVf8Gh588EHt27dPY8aM0datW/XVV19p0qRJio2NdV7i+pe//EUffPCBfv75Z23cuFEjRoyQm5ubS89z//33a/v27Xr00UeVmJioefPm6d133y20zUMPPaTFixdr9+7dio+P19KlS52lJAAAgCso0QAAAC7i2WefveDSwZYtW+qNN97QrFmzFBUVpdWrV19y5kpXTZ06VVOnTlVUVJRWrlypr7/+WsHBwZLkPHvMbrfr+uuvV9u2bfXQQw+pRo0ahe6/VhJjx45VbGysxo8fr7Zt22rRokX6+uuv1bRp0yt+DfXq1dN3332n1atXKyoqSvfff7/uuecePfXUU85tJkyYoJ49e+rGG2/UgAEDNGjQIDVp0sSl52nQoIG++OILLVy4UFFRUXrzzTf1wgsvFNrGbrdr1KhRatmypfr166dmzZrpjTfeuOLXCAAAqh+Lcf7NKAAAAAAAAAAUwploAAAAAAAAQDEo0QAAAAAAAIBiUKIBAAAAAAAAxaBEAwAAAAAAAIpBiQYAAAAAAAAUgxINAAAAAAAAKAYlGgAAAAAAAFAMSjQAAAAAAACgGJRoAAAAAAAAQDEo0QAAAAAAAIBiUKIBAAAAAAAAxfh/MFufTBkyPjwAAAAASUVORK5CYII=",
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"# Plot\n",
"import matplotlib.pyplot as plt\n",
"\n",
"plt.rcParams[\"figure.figsize\"] = (15, 5)\n",
"plt.xlabel(\"Number of rounds\")\n",
"plt.ylabel(\"Probability of players winning\")\n",
"plt.title(\"Orchard\")\n",
"\n",
"# Plot results for all steps\n",
"plt.plot(range(len(probabilities)), probabilities, linewidth=2)"
]
},
{
"cell_type": "markdown",
"id": "be75a05a",
"metadata": {},
"source": [
"We see that the players need at least 16 rounds to win the game. For increasing number of rounds, the winning probability also increases, until it converges towards the overall winning probability of $0.6313$."
]
},
{
"cell_type": "markdown",
"id": "8ed243e0",
"metadata": {},
"source": [
"### Conditional reachability probabilities\n",
"Conditional reachability probabilities of the form `Pmax=?( F \"Label1\" || F \"Label2\")` express the probability of reaching a `\"Label1\"`-state, conditioned under the event that a `\"Label2\"`-state is reached.\n",
"\n",
"We compute the maximal winning probability (`F \"PlayersWon\"`) under the condition that the raven is eventually only one step away from the orchard (`F \"RavenOneAway\"`).\n",
"\n",
"Note that we use the Prism model `orchard_prism` here which contains additional labels such as `\"RavenOneAway\"`."
]
},
{
"cell_type": "code",
"execution_count": 10,
"id": "0885da3e",
"metadata": {
"execution": {
"iopub.execute_input": "2026-03-26T10:39:50.029821Z",
"iopub.status.busy": "2026-03-26T10:39:50.029491Z",
"iopub.status.idle": "2026-03-26T10:39:50.082388Z",
"shell.execute_reply": "2026-03-26T10:39:50.081883Z"
}
},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"0.3197951767821407\n"
]
}
],
"source": [
"print(model_check(orchard_prism, 'Pmax=? [F \"PlayersWon\" || F \"RavenOneAway\"]'))"
]
},
{
"cell_type": "markdown",
"id": "85148071",
"metadata": {},
"source": [
"Checking the property yields a conditioned winning probability of $0.3198$ which is significantly lower than the overall winning probability of $0.6313$."
]
},
{
"cell_type": "markdown",
"id": "cfee8797",
"metadata": {},
"source": [
"### Multi-objective queries\n",
"Multi-objective queries of the form `multi (formula1, ..., formulaM)` allow to compute possible trade-offs between various (single-objective) properties `formula1`, ..., `formulaM`.\n",
"\n",
"For the Orchard game, the multi-objective query asks for the maximal expected number of rounds of the game (`R{\"rounds\"}max=? [F (\"PlayersWon\" | \"RavenWon\")]`) among all policies that induce a winning probability of at least 60% (`P>=0.60 [F \"PlayersWon\"])`)."
]
},
{
"cell_type": "code",
"execution_count": 11,
"id": "0deedf21",
"metadata": {
"execution": {
"iopub.execute_input": "2026-03-26T10:39:50.084462Z",
"iopub.status.busy": "2026-03-26T10:39:50.084247Z",
"iopub.status.idle": "2026-03-26T10:39:50.892677Z",
"shell.execute_reply": "2026-03-26T10:39:50.892100Z"
}
},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"21.79470309502809\n"
]
}
],
"source": [
"query = (\n",
" 'multi(R{\"rounds\"}max=? [F (\"PlayersWon\" | \"RavenWon\")], P>=0.60 [F \"PlayersWon\"])'\n",
")\n",
"print(model_check(orchard_prism, query))"
]
},
{
"cell_type": "markdown",
"id": "e00634ad",
"metadata": {},
"source": [
"We see that using a nearly optimal winning strategy (close to optimum of $63.13\\%$) also reduces the expected number of rounds played, which is $22.3391$ when considering all policies."
]
}
],
"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.12.13"
},
"widgets": {
"application/vnd.jupyter.widget-state+json": {
"state": {
"055872764d76400f8cba04b920cdc439": {
"model_module": "@jupyter-widgets/base",
"model_module_version": "2.0.0",
"model_name": "LayoutModel",
"state": {
"_model_module": "@jupyter-widgets/base",
"_model_module_version": "2.0.0",
"_model_name": "LayoutModel",
"_view_count": null,
"_view_module": "@jupyter-widgets/base",
"_view_module_version": "2.0.0",
"_view_name": "LayoutView",
"align_content": null,
"align_items": null,
"align_self": null,
"border_bottom": null,
"border_left": null,
"border_right": null,
"border_top": null,
"bottom": null,
"display": null,
"flex": null,
"flex_flow": null,
"grid_area": null,
"grid_auto_columns": null,
"grid_auto_flow": null,
"grid_auto_rows": null,
"grid_column": null,
"grid_gap": null,
"grid_row": null,
"grid_template_areas": null,
"grid_template_columns": null,
"grid_template_rows": null,
"height": null,
"justify_content": null,
"justify_items": null,
"left": null,
"margin": null,
"max_height": null,
"max_width": null,
"min_height": null,
"min_width": null,
"object_fit": null,
"object_position": null,
"order": null,
"overflow": null,
"padding": null,
"right": null,
"top": null,
"visibility": null,
"width": null
}
},
"547925713caa4f0ca63be16d0ead5a75": {
"model_module": "@jupyter-widgets/output",
"model_module_version": "1.0.0",
"model_name": "OutputModel",
"state": {
"_dom_classes": [],
"_model_module": "@jupyter-widgets/output",
"_model_module_version": "1.0.0",
"_model_name": "OutputModel",
"_view_count": null,
"_view_module": "@jupyter-widgets/output",
"_view_module_version": "1.0.0",
"_view_name": "OutputView",
"layout": "IPY_MODEL_a9d0bd1fb4cc4e149c7aef8c7b2032b2",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"6f2976c368f4472db2b1c5f6ce81164e": {
"model_module": "@jupyter-widgets/output",
"model_module_version": "1.0.0",
"model_name": "OutputModel",
"state": {
"_dom_classes": [],
"_model_module": "@jupyter-widgets/output",
"_model_module_version": "1.0.0",
"_model_name": "OutputModel",
"_view_count": null,
"_view_module": "@jupyter-widgets/output",
"_view_module_version": "1.0.0",
"_view_name": "OutputView",
"layout": "IPY_MODEL_055872764d76400f8cba04b920cdc439",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"a9d0bd1fb4cc4e149c7aef8c7b2032b2": {
"model_module": "@jupyter-widgets/base",
"model_module_version": "2.0.0",
"model_name": "LayoutModel",
"state": {
"_model_module": "@jupyter-widgets/base",
"_model_module_version": "2.0.0",
"_model_name": "LayoutModel",
"_view_count": null,
"_view_module": "@jupyter-widgets/base",
"_view_module_version": "2.0.0",
"_view_name": "LayoutView",
"align_content": null,
"align_items": null,
"align_self": null,
"border_bottom": null,
"border_left": null,
"border_right": null,
"border_top": null,
"bottom": null,
"display": null,
"flex": null,
"flex_flow": null,
"grid_area": null,
"grid_auto_columns": null,
"grid_auto_flow": null,
"grid_auto_rows": null,
"grid_column": null,
"grid_gap": null,
"grid_row": null,
"grid_template_areas": null,
"grid_template_columns": null,
"grid_template_rows": null,
"height": null,
"justify_content": null,
"justify_items": null,
"left": null,
"margin": null,
"max_height": null,
"max_width": null,
"min_height": null,
"min_width": null,
"object_fit": null,
"object_position": null,
"order": null,
"overflow": null,
"padding": null,
"right": null,
"top": null,
"visibility": null,
"width": null
}
}
},
"version_major": 2,
"version_minor": 0
}
}
},
"nbformat": 4,
"nbformat_minor": 5
}