From 34c0371324553e255b6cdcfc0dae41bf4da9365e Mon Sep 17 00:00:00 2001
From: Cole Schlesinger <63367934+thatplguy@users.noreply.github.com>
Date: Wed, 13 Nov 2024 08:39:24 -0800
Subject: [PATCH] Convert from AsciiDoctor to Material for MkDocs (#80)
---
.github/workflows/deploy-to-web.yml | 17 +-
.github/workflows/test-tutorial-build.yml | 29 +
.gitignore | 5 +-
Makefile | 51 +-
README.md | 49 +-
docs/README.md | 83 +
.../case-studies/doubly-linked-lists.md | 232 ++
.../case-studies/imperative-queues.md | 323 +++
.../case-studies/the-runway.md | 209 ++
docs/getting-started/hello-world.md | 1 +
docs/getting-started/installation.md | 13 +
docs/getting-started/style-guide/README.md | 58 +
docs/getting-started/tutorials/0.error.png | Bin 0 -> 786536 bytes
docs/getting-started/tutorials/README.md | 20 +
.../allocating-and-deallocating-memory.md | 91 +
.../tutorials/arrays-and-loops.md | 293 +++
docs/getting-started/tutorials/basic-usage.md | 237 ++
.../tutorials/defining-predicates.md | 57 +
.../tutorials/external-lemmas.md | 97 +
.../tutorials/images/0.error.png | Bin 0 -> 786536 bytes
docs/getting-started/tutorials/lists.md | 176 ++
.../ownership-of-compound-objects.md | 101 +
.../pointers-and-simple-ownership.md | 321 +++
docs/help/README.md | 1 +
docs/reference/README.md | 88 +
docs/specifications/README.md | 97 +
.../auxiliary-definitions/README.md | 1 +
.../custom-resource-predicates.md | 1 +
.../auxiliary-definitions/data-structures.md | 67 +
.../logical-functions.md | 1 +
docs/specifications/conditions.md | 78 +
docs/specifications/expressions.md | 3 +
.../specifications/function-specifications.md | 189 ++
.../interactive-theorem-proving.md | 1 +
docs/specifications/loop-invariants.md | 77 +
docs/specifications/resource-predicates.md | 1 +
docs/specifications/scoping.md | 1 +
docs/specifications/tactics.md | 1 +
docs/specifications/types.md | 1 +
docs/testing/README.md | 1 +
docs/verification/README.md | 1 +
mkdocs.yml | 142 ++
src/asciidoc_to_md.md | 53 +
src/tutorial.adoc | 1850 --------------
src/tutorial.md | 2235 +++++++++++++++++
45 files changed, 5457 insertions(+), 1896 deletions(-)
create mode 100644 .github/workflows/test-tutorial-build.yml
create mode 100644 docs/README.md
create mode 100644 docs/getting-started/case-studies/doubly-linked-lists.md
create mode 100644 docs/getting-started/case-studies/imperative-queues.md
create mode 100644 docs/getting-started/case-studies/the-runway.md
create mode 100644 docs/getting-started/hello-world.md
create mode 100644 docs/getting-started/installation.md
create mode 100644 docs/getting-started/style-guide/README.md
create mode 100644 docs/getting-started/tutorials/0.error.png
create mode 100644 docs/getting-started/tutorials/README.md
create mode 100644 docs/getting-started/tutorials/allocating-and-deallocating-memory.md
create mode 100644 docs/getting-started/tutorials/arrays-and-loops.md
create mode 100644 docs/getting-started/tutorials/basic-usage.md
create mode 100644 docs/getting-started/tutorials/defining-predicates.md
create mode 100644 docs/getting-started/tutorials/external-lemmas.md
create mode 100644 docs/getting-started/tutorials/images/0.error.png
create mode 100644 docs/getting-started/tutorials/lists.md
create mode 100644 docs/getting-started/tutorials/ownership-of-compound-objects.md
create mode 100644 docs/getting-started/tutorials/pointers-and-simple-ownership.md
create mode 100644 docs/help/README.md
create mode 100644 docs/reference/README.md
create mode 100644 docs/specifications/README.md
create mode 100644 docs/specifications/auxiliary-definitions/README.md
create mode 100644 docs/specifications/auxiliary-definitions/custom-resource-predicates.md
create mode 100644 docs/specifications/auxiliary-definitions/data-structures.md
create mode 100644 docs/specifications/auxiliary-definitions/logical-functions.md
create mode 100644 docs/specifications/conditions.md
create mode 100644 docs/specifications/expressions.md
create mode 100644 docs/specifications/function-specifications.md
create mode 100644 docs/specifications/interactive-theorem-proving.md
create mode 100644 docs/specifications/loop-invariants.md
create mode 100644 docs/specifications/resource-predicates.md
create mode 100644 docs/specifications/scoping.md
create mode 100644 docs/specifications/tactics.md
create mode 100644 docs/specifications/types.md
create mode 100644 docs/testing/README.md
create mode 100644 docs/verification/README.md
create mode 100644 mkdocs.yml
create mode 100644 src/asciidoc_to_md.md
delete mode 100644 src/tutorial.adoc
create mode 100644 src/tutorial.md
diff --git a/.github/workflows/deploy-to-web.yml b/.github/workflows/deploy-to-web.yml
index 211520a6..c316f874 100644
--- a/.github/workflows/deploy-to-web.yml
+++ b/.github/workflows/deploy-to-web.yml
@@ -22,23 +22,20 @@ jobs:
- name: Checkout repository
uses: actions/checkout@v3
- - name: Set up Ruby
- uses: ruby/setup-ruby@v1
+ - name: Set up Python
+ uses: actions/setup-python@v5
with:
- ruby-version: '2.7'
+ python-version: 3.x
- - name: Install AsciiDoctor
- run: gem install asciidoctor pygments.rb
+ - name: Install Material for MkDocs
+ run: pip install mkdocs-material
- name: Clean the build directory
- run: rm -rf build/*
+ run: make clean
- name: Build the tutorial
run: make
- - name: Move the tutorial file
- run: mv build/tutorial.html build/index.html
-
- name: Setup Pages
uses: actions/configure-pages@v5
@@ -49,4 +46,4 @@ jobs:
- name: Deploy to GitHub Pages
id: deployment
- uses: actions/deploy-pages@v4
\ No newline at end of file
+ uses: actions/deploy-pages@v4
diff --git a/.github/workflows/test-tutorial-build.yml b/.github/workflows/test-tutorial-build.yml
new file mode 100644
index 00000000..121c36b0
--- /dev/null
+++ b/.github/workflows/test-tutorial-build.yml
@@ -0,0 +1,29 @@
+name: Test tutorial build
+
+on:
+ pull_request:
+
+permissions:
+ contents: read
+
+jobs:
+ build:
+ runs-on: ubuntu-latest
+
+ steps:
+ - name: Checkout repository
+ uses: actions/checkout@v3
+
+ - name: Set up Python
+ uses: actions/setup-python@v5
+ with:
+ python-version: 3.x
+
+ - name: Install Material for MkDocs
+ run: pip install mkdocs-material
+
+ - name: Clean the build directory
+ run: make clean
+
+ - name: Check that the tutorial builds
+ run: make
diff --git a/.gitignore b/.gitignore
index 098ccd9c..4d1be0ad 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1,6 @@
build/*
/.vscode/
-check
\ No newline at end of file
+check
+**.swp
+docs/exercises
+docs/solutions
diff --git a/Makefile b/Makefile
index 07f53e90..e525def8 100644
--- a/Makefile
+++ b/Makefile
@@ -2,34 +2,33 @@
MAKEFILE_DIR:=$(dir $(realpath $(lastword $(MAKEFILE_LIST))))
-default: build exercises build/tutorial.html build/exercises.zip
+default: tutorial
all: default
clean:
- rm -rf build TAGS
-
-build:
- mkdir -p build
- mkdir -p build/exercises
- mkdir -p build/solutions
+ rm -rf docs/exercises docs/solutions docs/exercises.zip build TAGS
##############################################################################
# Exercises
SRC_EXAMPLES=$(shell find src/examples -type f)
-SOLUTIONS=$(patsubst src/examples/%, build/solutions/%, $(SRC_EXAMPLES))
-EXERCISES=$(patsubst src/examples/%, build/exercises/%, $(SRC_EXAMPLES))
+SOLUTIONS=$(patsubst src/examples/%, docs/solutions/%, $(SRC_EXAMPLES))
+EXERCISES=$(patsubst src/examples/%, docs/exercises/%, $(SRC_EXAMPLES))
CN=cn verify
-exercises: $(EXERCISES) $(SOLUTIONS)
+exercises: docs-exercises-dirs $(EXERCISES) $(SOLUTIONS)
+
+docs-exercises-dirs:
+ mkdir -p docs/exercises
+ mkdir -p docs/solutions
-build/exercises/%: src/examples/%
+docs/exercises/%: src/examples/%
@echo Rebuild $@
@-mkdir -p $(dir $@)
@sed -E '\|^.*--BEGIN--.*$$|,\|^.*--END--.*$$|d' $< > $@
-build/solutions/%: src/examples/%
+docs/solutions/%: src/examples/%
@-mkdir -p $(dir $@)
@if [ `which cn` ]; then \
if [[ "$<" = *".c"* ]]; then \
@@ -41,16 +40,15 @@ build/solutions/%: src/examples/%
@echo Rebuild $@
@cat $< | sed '\|^.*--BEGIN--.*$$|d' | sed '\|^.*--END--.*$$|d' > $@
-build/exercises.zip: $(EXERCISES)
- cd build; zip -r exercises.zip exercises > /dev/null
+docs/exercises.zip: $(EXERCISES)
+ cd docs; zip -r exercises.zip exercises > /dev/null
WORKING=$(wildcard src/examples/list_*.c)
-WORKING_AUX=$(patsubst src/examples/%, build/solutions/%, $(WORKING))
-temp: $(WORKING_AUX) build
-# build/tutorial.html
+WORKING_AUX=$(patsubst src/examples/%, docs/solutions/%, $(WORKING))
+temp: $(WORKING_AUX) docs-exercises-dirs
##############################################################################
-# Check that the examples all run correctly
+# Check that the examples all run correctly
CN_PATH?=cn verify
@@ -62,23 +60,16 @@ check-tutorial:
@echo Check tutorial examples
@$(MAKEFILE_DIR)/check.sh "$(CN_PATH)"
-check: check-tutorial check-archive
+check: check-tutorial check-archive
##############################################################################
# Tutorial document
-build/tutorial.adoc build/style.css build/asciidoctor.css: src/tutorial.adoc
- @echo Create build/tutorial.adoc
- @sed -E 's/include_example\((.+)\)/.link:\1[\1]\n[source,c]\n----\ninclude::\1\[\]\n----/g' $< > $@
- @cp src/style.css build
- @cp src/asciidoctor.css build
-
-build/images: src/images
- cp -r $< $@
+tutorial: exercises mkdocs.yml $(shell find docs -type f)
+ mkdocs build --strict
-build/tutorial.html: build/tutorial.adoc $(SRC_EXAMPLES) build/images
- asciidoctor --doctype book $< -o $@
- @rm build/tutorial.adoc
+serve: exercises mkdocs.yml $(shell find docs -type f)
+ mkdocs serve
##############################################################################
# Misc
diff --git a/README.md b/README.md
index a94df9b7..89765e8a 100644
--- a/README.md
+++ b/README.md
@@ -4,16 +4,55 @@ View the tutorial here: https://rems-project.github.io/cn-tutorial/
## Building
+The CN tutorial is built using [Material for
+MkDocs](https://squidfunk.github.io/mkdocs-material/).
+
+Dependencies:
+* python 3.x
+* pip
+
+```bash
+# Install Material for MkDocs
+pip install mkdocs-material
+
+# Build the tutorial
+make
+```
+
+### Hosting locally
+
+You can start a local server that automatically renders changes to the tutorial
+files. This is useful while editing the tutorial.
+
+```bash
+# Run the docs locally
+make serve
+```
+
+View at: http://localhost:8000/
+
Install dependencies: [asciidoctor](https://asciidoctor.org/).
-Run `make` to produce `build/tutorial.html` and its dependencies: especially, `build/exercises/*.c` and `build/solutions/*c`.
+## Tutorial examples
+
+The tutorial examples live in [src/examples](./src/examples).
+
+As part of building the tutorial, the examples are lightly preprocessed to
+produce solutions and exercises (solutions with the CN specifications removed).
+
+Run `make exercises` to produce the exercises and solutions in the `docs`
+directory.
+
+### Testing the tutorial examples
-Run `make check-tutorial` to check that all examples in the tutorial have working solutions (except tests with names `*.broken.c`, which are expected to fail). Note that this step will not work until after you have installed CN, which is the first part of the tutorial.
+Follow these steps `make check-tutorial` to check that all examples in the tutorial have working solutions (except tests with names `*.broken.c`, which are expected to fail).
-Run `make check` to checks both the tutorial and archive examples (see below).
+1. Install CN (follow steps in [the tutorial](https://rems-project.github.io/cn-tutorial/
+))
+2. Run `make check-tutorial`
-## CN Example Archive
+## CN example archive
The subdirectory `src/example-archive` includes many more examples of CN proofs, both working and broken. See [the README](./src/example-archive/README.md) for a description how these examples are organized.
-Run `make check-archive` to check all examples in the example archive.
\ No newline at end of file
+Install CN and run `make check-archive` to check all examples in the example archive.
diff --git a/docs/README.md b/docs/README.md
new file mode 100644
index 00000000..20cca887
--- /dev/null
+++ b/docs/README.md
@@ -0,0 +1,83 @@
+# Welcome to CN
+
+CN is an extension of the C programming language for testing and verifying the
+correctness of C code, especially on low-level systems code. Compared to
+standard C, CN checks not only that expressions and statements follow the
+correct typing discipline for C-types, but also that the C code executes
+_safely_ — does not raise C undefined behaviour — and _correctly_ — satisfying
+to strong, user-defined specifications.
+
+CN provides utilities for verifying specifications at compile time as well as
+automatically generating unit and integration tests to test specifications at
+runtime.
+
+This documentation is a work in progress -- your suggestions are greatly
+appreciated!
+
+
+
+- :material-clock-fast:{ .lg .middle } __Set up in 5 minutes__
+
+ ---
+
+ Build and install CN and get up and running in minutes
+
+ [:octicons-arrow-right-24: Installing CN](getting-started/installation.md)
+
+- :fontawesome-brands-markdown:{ .lg .middle } __Your first spec__
+
+ ---
+
+ Check out the Hello World tutorial to write, test, and verify your first
+ spec
+
+ [:octicons-arrow-right-24: Hello World](getting-started/hello-world.md)
+
+- :material-format-font:{ .lg .middle } __Tutorials__
+
+ ---
+
+ Find tutorials covering common tasks and introducing CN features
+
+ [:octicons-arrow-right-24: Tutorials](getting-started/tutorials/README.md)
+
+- :material-scale-balance:{ .lg .middle } __Language reference__
+
+ ---
+
+ Quick reference for CN specification syntax
+
+ [:octicons-arrow-right-24: Language reference](reference/README.md)
+
+
+
+## Origins
+CN was first described in [CN: Verifying Systems C Code with Separation-Logic Refinement Types](https://dl.acm.org/doi/10.1145/3571194) by Christopher Pulte, Dhruv C. Makwana, Thomas Sewell, Kayvan Memarian, Peter Sewell, and Neel Krishnaswami.
+To accurately handle the complex semantics of C, CN builds on the [Cerberus semantics for C](https://github.com/rems-project/cerberus/).
+Some of the examples in this tutorial are adapted from Arthur Charguéraud’s excellent
+[Separation Logic Foundations](https://softwarefoundations.cis.upenn.edu) textbook, and one of the case studies is based on an
+extended exercise due to Bryan Parno.
+
+## Acknowledgment of Support and Disclaimer
+This material is based upon work supported by the Air Force Research Laboratory (AFRL) and Defense Advanced Research Projects Agencies (DARPA) under Contract No. FA8750-24-C-B044, a European Research Council (ERC) Advanced Grant “ELVER” under the European Union’s Horizon 2020 research and innovation programme (grant agreement no. 789108), and additional funding from Google. The opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the Air Force Research Laboratory (AFRL).
+
+## Building these docs
+
+These docs are built with [Material for
+MkDocs](https://squidfunk.github.io/mkdocs-material/). To build and serve them
+locally on http://localhost:8000:
+
+```bash
+# Install Material for MkDocs
+pip install mkdocs-material
+
+# In the cn-tutorial root directory, run
+mkdocs serve
+```
+
+## Docs layout
+
+ mkdocs.yml # The configuration file.
+ docs/
+ README.md # The documentation homepage.
+ ... # Other markdown pages, images and other files.
diff --git a/docs/getting-started/case-studies/doubly-linked-lists.md b/docs/getting-started/case-studies/doubly-linked-lists.md
new file mode 100644
index 00000000..78d94433
--- /dev/null
+++ b/docs/getting-started/case-studies/doubly-linked-lists.md
@@ -0,0 +1,232 @@
+# Doubly-linked Lists
+
+
+
+A doubly linked list is a linked list where each node has a pointer
+to both the next node and the previous node. This allows for O(1)
+operations for adding or removing nodes anywhere in the list.
+
+Because of all the sharing in this data structure, the separation
+reasoning is a bit tricky. We'll give you the core definitions and
+then invite you to help fill in the annotations for some of the
+functions that manipulate doubly linked lists.
+
+First, here is the C type definition:
+
+```c title="exercises/dll/c_types.h"
+--8<--
+exercises/dll/c_types.h
+--8<--
+```
+
+The idea behind the representation of this list is that we don't keep
+track of the front or back, but rather we take any node in the list
+and have a sequence to the left and to the right of that node. The `left`
+and `right` are from the point of view of the node itself, so `left`
+is kept in reverse order. Additionally, similarly to in the
+`Imperative Queues` example, we can reuse the `List` type.
+
+```c title="exercises/dll/cn_types.h"
+--8<--
+exercises/dll/cn_types.h
+--8<--
+```
+
+The predicate for this datatype is a bit complicated. The idea is that
+we first own the node that is passed in. Then we follow all of the
+`prev` pointers to own everything backwards from the node, and finally
+all the `next` pointers to own everything forwards from the node, to
+construct the `left` and `right` fields.
+
+
+
+```c title="exercises/dll/predicates.h"
+--8<--
+exercises/dll/predicates.h
+--8<--
+```
+
+Note that `Dll_at` takes ownership of the node passed in, and then
+calls `Own_Backwards` and `Own_Forwards`, which recursively take
+ownership of the rest of the list.
+
+Also, notice that `Own_Forwards` and `Own_Backwards` include `ptr_eq`
+assertions for the `prev` and `next` pointers. This is to ensure that
+the nodes in the list are correctly doubly linked. For example, the
+line `assert (ptr_eq(n.prev, prev_pointer));` in `Own_Forwards`
+ensures that the current node correctly points backward to the
+previous node in the list. The line `assert(ptr_eq(prev_node.next,
+p));` ensures that the previous node correctly points forward to the
+current node.
+
+Before we move on to the functions that manipulate doubly linked
+lists, we need to define a few "getter" functions that will allow us
+to access the fields of our `Dll` datatype. This will make the
+specifications easier to write.
+
+```c title="exercises/dll/getters.h"
+--8<--
+exercises/dll/getters.h
+--8<--
+```
+
+We also need some boilerplate for allocation and deallocation.
+
+```c title="exercises/dll/malloc_free.h"
+--8<--
+exercises/dll/malloc_free.h
+--8<--
+```
+
+For convenience, we gather all of these files into a single header file.
+
+```c title="exercises/dll/headers.h"
+--8<--
+exercises/dll/headers.h
+--8<--
+```
+
+
+
+Now we can move on to an initialization function. Since an empty list
+is represented as a null pointer, we will look at initializing a
+singleton list (or in other words, a list with only one item).
+
+```c title="exercises/dll/singleton.c"
+--8<--
+exercises/dll/singleton.c
+--8<--
+```
+
+
+
+The `add` and `remove` functions are where it gets a little tricker.
+Let's start with `add`. Here is the unannotated version:
+
+```c title="exercises/dll/add_orig.broken.c"
+--8<--
+exercises/dll/add_orig.broken.c
+--8<--
+```
+
+_Exercise_: Before reading on, see if you can figure out what
+specification is appropriate and what other are needed.
+
+
+
+Now, here is the annotated version of the `add` operation:
+
+```c title="exercises/dll/add.c"
+--8<--
+exercises/dll/add.c
+--8<--
+```
+
+First, let's look at the pre- and post-conditions. The `requires`
+clause is straightforward. We need to own the list centered around
+the node that `n` points to. `Before` is a `Dll`
+that is either empty, or it has a List to the left,
+the current node that `n` points to, and a List to the right.
+This corresponds to the state of the list when it is passed in.
+
+In the ensures clause, we again establish ownership of the list, but
+this time it is centered around the added node. This means that
+`After` is a `Dll` structure similar to `Before`, except that the node
+`curr` is now the created node. The old `curr` is pushed into the left
+part of the new list. The conditional operator in the `ensures` clause
+is saying that if the list was empty coming in, it now is a singleton
+list. Otherwise, the left left part of the list now has the data from
+the old `curr` node, the new `curr` node is the added node, and the
+right part of the list is the same as before.
+
+Now, let's look at the annotations in the function body. CN can
+figure out the empty list case for itself, but it needs some help with
+the non-empty list case. The `split_case` on `is_null(n->prev)`
+tells CN to unpack the `Own_Backwards` predicate. Without this
+annotation, CN cannot reason that we didn't lose the left half of the
+list before we return, and will claim we are missing a resource for
+returning. The `split_case` on `is_null(n->next->next)` is similar,
+but for unpacking the `Own_Forwards` predicate. Note that we have to
+go one more node forward to make sure that everything past `n->next`
+is still owned at the end of the function.
+
+Now let's look at the `remove` operation. Traditionally, a `remove`
+operation for a list returns the integer that was removed. However we
+also want all of our functions to return a pointer to the
+list. Because of this, we define a `struct` that includes an `int`
+and a `node`.
+
+```c title="exercises/dll/dllist_and_int.h"
+--8<--
+exercises/dll/dllist_and_int.h
+--8<--
+```
+
+Now we can look at the code for the `remove` operation. Here is the un-annotated version:
+
+```c title="exercises/dll/remove_orig.broken.c"
+--8<--
+exercises/dll/remove_orig.broken.c
+--8<--
+```
+
+_Exercise_: Before reading on, see if you can figure out what
+specification is appropriate and what annotations are needed.
+
+
+
+Now, here is the fully annotated version of the `remove` operation:
+
+```c title="exercises/dll/remove.c"
+--8<--
+exercises/dll/remove.c
+--8<--
+```
+
+First, let's look at the pre- and post-conditions. The `requires` clause says that we cannot remove a node from an empty list, so the pointer passed in must not be null. Then we take ownership of the list, and we
+assign the node of that list to the identifier `del`
+to make our spec more readable. So `Before` refers to the `Dll` when the function is called, and `del` refers to the node that will be deleted.
+
+Then in the `ensures` clause, we must take ownership
+of the `node_and_int` struct as well as the `Dll` that
+the node is part of. Here, `After` refers to the `Dll`
+when the function returns. We ensure that the int that is returned is the value of the deleted node, as intended. Then we have a complicated nested ternary conditional that ensures that `After` is the same as `Before` except for the deleted node. Let's break down this conditional:
+
+- The first guard asks if both `del.prev` and `del.next` are null. In this case, we are removing the only node in the list, so the resulting list will be empty. The `else` branch of this conditional contains its own conditional.
+
+- For the following conditional, the guard checks if 'del.prev' is
+ _not_ null. This means that the returned node is `del.next`,
+ regardless of whether or not `del.prev` is null. If this is the
+ case, `After` is now centered around `del.next`, and the left part
+ of the list is the same as before. Since `del.next` was previously
+ the head of the right side, the right side loses its head in
+ `After`. This is where we get `After == Dll{left:
+Left_Sublist(Before), curr: Node(After), right: Tl(Right(Before))}`.
+
+- The final `else` branch is the case where `del.next` is null, but
+ `del.prev` is not null. In this case, the returned node is
+ `del.prev`. This branch follows the same logic as the one before it,
+ except now we are taking the head of the left side rather than the
+ right side. Now the right side is unchanged, and the left side is just
+ the tail, as seen shown in `After == Dll{left:
+Tl(Left_Sublist(Before)), curr: Node(After), right: Right(Before)};`
+
+The annotations in the function body are similar to in the `add`
+function. Both of these `split_case` annotations are needed to unpack
+the `Own_Forwards` and `Own_Backwards` predicates. Without them, CN
+will not be able to reason that we didn't lose the left or right half
+of the list before we return and will claim we are missing a resource
+for returning.
+
+
+
+_Exercise_: There are many other functions that one might want to
+implement for a doubly linked list. For example, one might want to
+implement a function that appends one list to another, or a function
+that reverses a list. Try implementing a few of these functions and
+writing their specifications.
+
+_Exercise_: For extra practice, try coming up with one or two
+variations on the Dll data structure itself (there are many!).
+
+
diff --git a/docs/getting-started/case-studies/imperative-queues.md b/docs/getting-started/case-studies/imperative-queues.md
new file mode 100644
index 00000000..043fcad9
--- /dev/null
+++ b/docs/getting-started/case-studies/imperative-queues.md
@@ -0,0 +1,323 @@
+# Imperative Queues
+
+A queue is a linked list with O(1) operations for adding things to one
+end (the "back") and removing them from the other (the "front"). Here
+are the C type definitions:
+
+```c title="exercises/queue/c_types.h"
+--8<--
+exercises/queue/c_types.h
+--8<--
+```
+
+A queue consists of a pair of pointers, one pointing to the front
+element, which is the first in a linked list of `queue_cell`s,
+the other pointing directly to the last cell in this list. If the
+queue is empty, both pointers are NULL.
+
+Abstractly, a queue just represents a list, so we can reuse the `List`
+type from the list examples earlier in the tutorial.
+
+```c title="exercises/queue/cn_types_1.h"
+--8<--
+exercises/queue/cn_types_1.h
+--8<--
+```
+
+Given a pointer to a `queue` struct, this predicate grabs ownership
+of the struct, asserts that the `front` and `back` pointers must
+either both be NULL or both be non-NULL, and then hands off to an
+auxiliary predicate `QueueFB`. Note that `QueuePtr_At` returns a
+`List` -- that is, the abstract view of a queue heap structure is
+simply the sequence of elements that it contains. The difference
+between a queue and a singly or doubly linked list is simply one of
+concrete representation.
+
+`QueueFB` is where the interesting part starts. (Conceptually,
+`QueueFB` is part of `QueuePTR`, but CN currently allows
+conditional expressions only at the beginning of predicate
+definitions, not after a `take`, so we need to make a separate
+auxiliary predicate.)
+
+```c title="exercises/queue/cn_types_2.h"
+--8<--
+exercises/queue/cn_types_2.h
+--8<--
+```
+
+First, we case on whether the `front` of the queue is NULL. If so,
+then the queue is empty and we return the empty sequence.
+
+If the queue is not empty, we need to walk down the linked list of
+elements and gather up all their values into a sequence. But we must
+treat the last element of the queue specially, for two reasons.
+First, since the `push` operation is going to follow the `back`
+pointer directly to the last list cell without traversing all the
+others, we need to `take` that element now rather than waiting to
+get to it at the end of the recursion starting from the `front`.
+Second, and relatedly, there will be two pointers to this final list
+cell -- one from the `back` field and one from the `next` field of
+the second to last cell (or the `front` pointer, if there is only
+one cell in the list), so we need to be careful not to `take` this
+cell twice.
+
+Accordingly, we begin by `take`-ing the tail cell and passing it
+separately to the `QueueAux` predicate, which has the job of
+walking down the cells from the front and gathering all the rest of
+them into a sequence. We take the result from `QueueAux` and
+`snoc` on the very last element.
+
+The `assert (is_null(B.next))` here gives the CN verifier a crucial
+piece of information about an invariant of the representation: The
+`back` pointer always points to the very last cell in the list, so
+its `next` field will always be NULL.
+
+
+
+Finally, the `QueueAux` predicate recurses down the list of
+cells and returns a list of their contents.
+
+```c title="exercises/queue/cn_types_3.h"
+--8<--
+exercises/queue/cn_types_3.h
+--8<--
+```
+
+Its first argument (`f`) starts out at `front` and progresses
+through the queue on recursive calls; its `b` argument is always a
+pointer to the very last cell.
+
+When `f` and `b` are equal, we have reached the last cell and
+there is nothing to do. We don't even have to build a singleton
+list: that's going to happen one level up, in `QueueFB`.
+
+Otherwise, we `take` the fields of the `f`, make a recurive
+call to `QueueAux` to process the rest of the cells, and cons the
+`first` field of this cell onto the resulting sequence before
+returning it. Again, we need to help the CN verifier by explicitly
+informing it of the invariant that we know, that `C.next` cannot be
+null if `f` and `b` are different.
+
+Now we need a bit of boilerplate: just as with linked lists, we need
+to be able to allocate and deallocate queues and queue cells. There
+are no interesting novelties here.
+
+```c title="exercises/queue/allocation.h"
+--8<--
+exercises/queue/allocation.h
+--8<--
+```
+
+
+
+_Exercise_: The function for creating an empty queue just needs to set
+both of its fields to NULL. See if you can fill in its specification.
+
+```c title="exercises/queue/empty.c"
+--8<--
+exercises/queue/empty.c
+--8<--
+```
+
+
+
+The push and pop operations are more involved. Let's look at `push`
+first.
+
+Here's the unannotated C code -- make sure you understand it.
+
+```c title="exercises/queue/push_orig.broken.c"
+--8<--
+exercises/queue/push_orig.broken.c
+--8<--
+```
+
+_Exercise_: Before reading on, see if you can write down a reasonable
+top-level specification for this operation.
+
+One thing you might find odd about this code is that there's a
+`return` statement at the end of each branch of the conditional,
+rather than a single `return` at the bottom. The reason for this is
+that, when CN analyzes a function body containing a conditional, it
+effectively _copies_ all the code after the conditional into each of
+the branches. Then, if verification encounters an error related to
+this code -- e.g., "you didn't establish the `ensures` conditions at
+the point of returning -- the error message will be confusing because
+it will not be clear which branch of the conditional it is associated
+with.
+
+Now, here is the annotated version of the `push` operation.
+
+```c title="exercises/queue/push.c"
+--8<--
+exercises/queue/push.c
+--8<--
+```
+
+The case where the queue starts out empty (`q->back == 0`) is easy.
+CN can work it out all by itself.
+
+The case where the starting queue is nonempty is more interesting.
+The `push` operation messes with the end of the sequence of queue
+elements, so we should expect that validating `push` is going to
+require some reasoning about this sequence. Here, in fact, is the
+lemma we need.
+
+
+
+
+```c title="exercises/queue/push_lemma.h"
+--8<--
+exercises/queue/push_lemma.h
+--8<--
+```
+
+This says, in effect, that we have two choices for how to read out the
+values in some chain of queue cells of length at least 2, starting
+with the cell `front` and terminating when we get to the next cell
+_following_ some given cell `p` -- call it `c`. We can either
+gather up all the cells from `front` to `c`, or we can gather up
+just the cells from `front` to `p` and then `snoc` on the single
+value from `c`.
+
+When we apply this lemma, `p` will be the old `back` cell and
+`c` will be the new one. But to prove it (by induction, of course),
+we need to state it more generally, allowing `p` to be any internal
+cell in the list starting at `front` and `c` its successor.
+
+The reason we need this lemma is that, to add a new cell at the end of
+the queue, we need to reassign ownership of the old `back` cell.
+In the precondition of `push`, we took ownership of this cell
+separately from the rest; in the postcondition, it needs to be treated
+as part of the rest (so that the new `back` cell can now be treated
+specially).
+
+One interesting technicality is worth noting: After the assignment
+`q->back = c`, we can no longer prove `QueueFB(q->front,
+oldback)`, but we don't care about this, since we want to prove
+`QueueFB(q->front, q->back)`. However, crucially,
+`QueueAux(q->front, oldback)` is still true.
+
+
+
+Now let's look at the `pop` operation. Here is the un-annotated
+version:
+
+```c title="exercises/queue/pop_orig.broken.c"
+--8<--
+exercises/queue/pop_orig.broken.c
+--8<--
+```
+
+_Exercise_: Again, before reading on, see if you can write down a
+plausible top-level specification. (For extra credit, see how far you
+can get with verifying it!)
+
+Here is the fully annotated `pop` code:
+
+```c title="exercises/queue/pop.c"
+--8<--
+exercises/queue/pop.c
+--8<--
+```
+
+There are three annotations to explain. Let's consider them in order.
+
+First, the `split_case` on `is_null(q->front)` is needed to tell
+CN which of the branches of the `if` at the beginning of the
+`QueueFB` predicate it can "unpack". (`QueuePtr_At` can be
+unpacked immediately because it is unconditional, but `QueueFB`
+cannot.)
+
+
+
+The guard/condition for `QueueFB` is `is_null(front)`, which is
+why we need to do a `split_case` on this value. On one branch of the
+`split_case` we have a contradiction: the fact that `before ==
+Nil{}` (from `QueueFB`) conflicts with `before != Nil`
+from the precondition, so that case is immediate. On the other
+branch, CN now knows that the queue is non-empty, as required, and type
+checking proceeds.
+
+When `h == q->back`, we are in the case where the queue contains
+just a single element, so we just need to NULL out its `front` and
+`back` fields and deallocate the dead cell. The `unfold`
+annotation is needed because the `snoc` function is recursive, so CN
+doesn't do the unfolding automatically.
+
+Finally, when the queue contains two or more elements, we need to
+deallocate the front cell, return its `first` field, and redirect
+the `front` field of the queue structure to point to the next cell.
+To push the verification through, we need a simple lemma about the
+`snoc` function:
+
+```c title="exercises/queue/pop_lemma.h"
+--8<--
+exercises/queue/pop_lemma.h
+--8<--
+```
+
+The crucial part of this lemma is the last three lines, which express
+a simple, general fact about `snoc`:
+if we form a sequence by calling `snoc` to add a final element
+`B.first` to a sequence with head element `x` and tail `Q`, then the
+head of the resulting sequence is still `x`, and its tail is `snoc
+(Q, B.first)`.
+
+The `requires` clause and the first three lines of the `ensures`
+clause simply set things up so that we can name the various values we
+are talking about. Since these values come from structures in the
+heap, we need to take ownership of them. And since lemmas in CN are
+effectively just trusted functions that can also take in ghost values,
+we need to take ownership in both the `requires` and `ensures`
+clauses. (Taking them just in the `requires` clause would imply
+that they are consumed and deallocated when the lemma is applied --
+not what we want!)
+
+
+
+
+(The only reason we can't currently prove this lemma in CN is that we
+don't have `take`s in CN statements, because this is just a simple
+unfolding.)
+
+
+
+_Exercise_:
+Investigate what happens when you make each of the following changes
+to the queue definitions. What error does CN report? Where are the
+telltale clues in the error report that suggest what the problem was?
+
+- Remove `assert (is_null(B.next));` from `InqQueueFB`.
+- Remove `assert (is_null(B.next));` from `InqQueueAux`.
+- Remove one or both of occurrences of `free_queue_cell(f)` in
+ `pop_queue`.
+- Remove, in turn, each of the CN annotations in the bodies of
+ `pop_queue` and `push_queue`.
+
+_Exercise_: The conditional in the `pop` function tests whether or
+not `f == b` to find out whether we have reached the last element of
+the queue. Another way to get the same information would be to test
+whether `f->next == 0`. Can you verify this version?
+_Note_: I (BCP) have not worked out the details, so am not sure how hard
+this is (or if it is even not possible, though I'd be surprised).
+Please let me know if you get it working!
+
+_Exercise_: Looking at the code for the `pop` operation,
+it might seem reasonable to move the identical assignments to `x` in both
+branches to above the `if`. This doesn't "just work" because the
+ownership reasoning is different. In the first case, ownership of
+`h` comes from `QueueFB` (because `h == q->back`). In the
+second case, it comes from `QueueAux` (because `h !=
+q->back`).
+
+Can you generalize the `snoc_facts` lemma to handle both cases? You
+can get past the dereference with a `split_case` but formulating the
+lemma before the `return` will be a bit more complicated.
+
+
+
+_Note_: Again, this has not been shown to be possible, but Dhruv
+believes it should be!
+
+
diff --git a/docs/getting-started/case-studies/the-runway.md b/docs/getting-started/case-studies/the-runway.md
new file mode 100644
index 00000000..7450e313
--- /dev/null
+++ b/docs/getting-started/case-studies/the-runway.md
@@ -0,0 +1,209 @@
+# Airport Simulation
+
+
+
+Suppose we have been tasked with writing a program that simulates a
+runway at an airport. This airport is very small, so it only has one
+runway, which is used for both takeoffs and landings. We want to
+verify that the runway is always used safely, by checking the
+following informal specification:
+
+1. The runway has two modes: departure mode and arrival mode. The two
+modes can never be active at the same time. Neither mode is active
+at the beginning of the day.
+
+
+2. At any given moment, there is a waiting list of planes that need to
+ land at the airport and planes that need to leave the
+ airport. These are modeled with counters `W_A` for the number of
+ planes waiting to arrive, and `W_D` for the number of planes
+ waiting to depart.
+
+3. At any moment, a plane is either waiting to arrive, waiting to
+ depart, or on the runway. Once a plane has started arriving or
+ departing, the corresponding counter (`W_A` or `W_D`) is
+ decremented. There is no need to keep track of planes once they
+ have arrived or departed. Additionally, once a plane is waiting to
+ arrive or depart, it continues waiting until it has arrived or
+ departed.
+
+4. It takes 5 minutes for a plane to arrive or depart. During these 5
+ minutes, no other plane may use the runway. We can keep track of
+ how long a plane has been on the runway with the
+ `Runway_Counter`. If the `Runway_Counter` is at 0, then there is
+ currently no plane using the runway, and it is clear for another
+ plane to begin arriving or departing. Once the `Runway_Counter`
+ reaches 5, we can reset it at the next clock tick. One clock tick
+ represents 1 minute.
+
+5. If there is at least one plane waiting to depart and no cars
+ waiting to arrive, then the runway is set to departure mode (and
+ vice versa for arrivals).
+
+6. If both modes of the runway are inactive and planes become ready to
+ depart and arrive simultaneously, the runway will activate arrival
+ mode first. If the runway is in arrival mode and there are planes
+ waiting to depart, no more than 3 planes may arrive from that time
+ point. When either no more planes are waiting to arrive or 3 planes
+ have arrived, the runway switches to departure mode. If the runway
+ is on arrival mode and no planes are waiting to depart, then the
+ runway may stay in arrival mode until a plane is ready to depart,
+ from which time the 3-plane limit is imposed (and vice versa for
+ departures). Put simply, if any planes are waiting for a mode that
+ is inactive, that mode will become active no more than 15 minutes
+ later (5 minutes for each of 3 planes).
+
+To encode all this in CN, we first need a way to describe the state of
+the runway at a given time. We can use a _struct_ that includes the
+following fields:
+
+- `ModeA` and `ModeD` to represent the arrival and departure modes,
+ respectively. We can define constants for `ACTIVE` and `INACTIVE`,
+ as described in the `Constants` section above.
+
+- `W_A` and `W_D` to represent the number of planes waiting to arrive
+ and depart, respectively.
+
+- `Runway_Time` to represent the time (in minutes) that a plane has
+ spent on the runway while arriving or departing.
+
+- `Plane_Counter` to represent the number of planes that have arrived
+ or departed while planes are waiting for the other mode. This will
+ help us keep track of the 3-plane limit as described in _(6)_.
+
+```c title="exercises/runway/state.h"
+--8<--
+exercises/runway/state.h
+--8<--
+```
+
+Next, we need to specify what makes a state valid. We must define a
+rigorous specification in order to ensure that the runway is always
+safe and working as intended. Try thinking about what this might look
+like before looking at the code below.
+
+```c title="exercises/runway/valid_state.h"
+--8<--
+exercises/runway/valid_state.h
+--8<--
+```
+
+Let's walk through the specifications in `valid_state`:
+
+- The first two lines ensure that both modes in our model behave as intended: they can only be active or inactive. Any other value for these fields would be invalid.
+
+- The third line says that either arrival mode or departure mode must be inactive. This specification ensures that the runway is never in both modes at the same time.
+
+- The fourth line says that the number of planes waiting to arrive or depart must be non-negative. This makes sense: we can't have a negative number of planes!
+
+- The fifth line ensures that the runway time is between 0 and 5. This addresses how a plane takes 5 minutes on the runway as described in _(4)_.
+
+- The sixth line ensures that the plane counter is between 0 and 3. This is important for the 3-plane limit as described in _(6)_.
+
+- The seventh line refers to the state at the beginning of the day. If both modes are inactive, then the day has just begun, and thus no planes have departed yet. This is why the plane counter must be 0.
+
+- The eighth line says that if there is a plane on the runway, then one of the modes must be active. This is because a plane can only be on the runway if it is either arriving or departing.
+
+- The final two lines ensure that we are incrementing `Plane_Counter` only if there are planes waiting for the other mode, as described in _(6)_.
+
+Now that we have the tools to reason about the state of the runway formally, let's start writing some functions.
+
+First, let's look at an initialization function and functions to update `Plane_Counter`. Step through these yourself and make sure you understand the reasoning behind each specification.
+
+```c title="exercises/runway/funcs1.h"
+--8<--
+exercises/runway/funcs1.h
+--8<--
+```
+
+_Exercise_: Now try adding your own specifications to the following
+functions. Make sure that you specify a valid state as a pre- and
+post-condition for every function. If you get stuck, the solution is
+in the solutions folder.
+
+```c title="exercises/runway/funcs2.c"
+--8<--
+exercises/runway/funcs2.c
+--8<--
+```
+
+
+
+## Acknowledgment of Support and Disclaimer
+
+This material is based upon work supported by the Air Force Research Laboratory (AFRL) and Defense Advanced Research Projects Agencies (DARPA) under Contract No. FA8750-24-C-B044, a European Research Council (ERC) Advanced Grant “ELVER” under the European Union’s Horizon 2020 research and innovation programme (grant agreement no. 789108), and additional funding from Google. The opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the Air Force Research Laboratory (AFRL).
+
+
+
+
diff --git a/docs/getting-started/hello-world.md b/docs/getting-started/hello-world.md
new file mode 100644
index 00000000..29658341
--- /dev/null
+++ b/docs/getting-started/hello-world.md
@@ -0,0 +1 @@
+# Hello World
diff --git a/docs/getting-started/installation.md b/docs/getting-started/installation.md
new file mode 100644
index 00000000..d7eecbd8
--- /dev/null
+++ b/docs/getting-started/installation.md
@@ -0,0 +1,13 @@
+# Installation
+
+To fetch and install CN, visit the [Cerberus repository](https://github.com/rems-project/cerberus) and follow the instructions in [backend/cn/README.md](https://github.com/rems-project/cerberus/blob/master/backend/cn/README.md).
+
+Once the installation is completed, type `cn --help` in your terminal to ensure CN is installed and found by your system. This should print the list of available options CN can be executed with.
+
+To apply CN to a C file, run `cn verify CFILE`.
+
+Install the [language
+server](https://github.com/GaloisInc/VERSE-Toolchain/tree/main/cn-lsp/server)
+and [VSCode
+plugin](https://github.com/GaloisInc/VERSE-Toolchain/tree/main/cn-lsp/client)
+for a better IDE experience.
diff --git a/docs/getting-started/style-guide/README.md b/docs/getting-started/style-guide/README.md
new file mode 100644
index 00000000..2cf0e3a4
--- /dev/null
+++ b/docs/getting-started/style-guide/README.md
@@ -0,0 +1,58 @@
+# Style Guide
+
+
+
+!!! warning
+
+ This is a draft of proposed style guidelines. Expect this to change in the
+ near future.
+
+This section gathers some advice on stylistic conventions and best
+practices in CN.
+
+### Constants
+
+The syntax of the C language does not actually include constants.
+Instead, the convention is to use the macro preprocessor to replace
+symbolic names by their definitions before the C compiler ever sees
+them.
+
+This raises a slight awkwardness in CN, because CN specifications and
+annotations are written in C comments, so they are not transformed by
+the preprocessor. However, we can approximate the effect of constant
+_values_ by defining constant _functions_. We've been working with
+some of these already, e.g., `MINi32()`, but it is also possible to
+define our own constant functions. Here is the officially approved
+idiom:
+
+```c title="exercises/const_example.c"
+--8<--
+exercises/const_example.c
+--8<--
+```
+
+Here's how it works:
+
+- We first define a C macro `CONST` in the usual way.
+
+- The next two lines "import" this constant into CN by defining a CN
+ function `CONST()` whose body is the C function `c_CONST()`. The
+ body of `c_CONST` returns the value of the macro `CONST`. Notice
+ that the declaration of `CONST()` has no body.
+
+- The annotation `/*@ cn_function CONST; @*/` links
+ the two functions, `CONST()` and `cn_CONST()`.
+
+Of course, we could achieve the same effect by defining the CN
+function `CONST()` directly...
+
+```c title="exercises/const_example_lessgood.c"
+--8<--
+exercises/const_example_lessgood.c
+--8<--
+```
+
+...but this version repeats the number `1` in two places -- a
+potential source of nasty bugs!
+
+
diff --git a/docs/getting-started/tutorials/0.error.png b/docs/getting-started/tutorials/0.error.png
new file mode 100644
index 0000000000000000000000000000000000000000..5aa67693c0ec7709085fbb79fd965c10939401ec
GIT binary patch
literal 786536
zcmeFZdpwix{|DY#M=I|^VNRt|gu+H!rHr>zr9x=cNF~W(4rT62B{_^Jk|i?dmMmHGd-W>#H!DvZ)?cz@DekJd`3Wm?bF~wGK9{dv_gJ!I
zSG;!|)q2@Q#d@me!&mB?Hf&gFcih)G*-7^<(rNIf(|6Ji`V1<({rqp;qvLW{u3x+U
zzEtDhhaJ1FTwk~O)xLWVO9!7lnFuLC#Sfo9hN!{YSYsJpn&1Yu2YaciGC$
z)0UWbnrjXB9^M%FW?z)=z|P+Xuk0Rnqn}HVGhwHOwl(Z^cc?9^{rT@n-Hn*dQNpb_
zuc0T^S)shoW&Bf3D|e~{g9+-bF@m29}|
z(_mSTU5^fH#a>E7)$zrmusjNGStR}izHja<`HugF)pO+omTA?~YhAmOuQy;Ew_MLJ
zH`?Uw_hD_oZzR26V{rQ_&cXVSe3YH!(HLflqd+@jFMg$Hyyy@-<0c+XR+nvUm+XOG
zuU@h=;_8wW@T;Zp*EaZT$&zI+mi_lPGUr|_|L^NHzoq|Z_1$%D$&$lMtd1Qy9lVsA
zZk^-ZM0hqI!Ym{Eo)6@vnixOkZM?VX)u#H|)#@7G)zprC`0(TKnnT}T9C3fu@YVL5
z`o9|wZCkN)Lw)YCwQE9l-IeuCld&w_>qsZJdu7VY4I}8r=@_?Tq5Y>cVk}n
zojG`|L-7oxeDM8P&L>81|GJfT)i$oUcX;FKWk=LjulWCe`2XkN{{wL_sG)vyLSw^D
z{F-G+ig&krb9YjF+rNfwKNFnKXD9x`f7+sbjuWBmegikbdTaGT;`DvF{cX;N>Ren&
zcp6a$BVe;NEiUb``+@=4xBNFacRLPRFSaE2mrd_>p+HYmgZmsJ2#bfUB^_RW-=cBV
zp#p?>&Y0M+Xhh8ldnkPqFljCyGp@OqD6S>fB1U5LYb&ak;lBIS{iuFw-;0tY&3&*Vslp@nTp2)Oizuva@p(^H_hiyA
z8z6t1#_+=%O*EF3Upb_4^H<>5>W`6eMUBB1;&H?jgV0FSblfyPrQ%kncX~`~7|S|T
zq?S#jl?=R>f4Mwt2Z!@Uaxts@t>kPPEAgf5x3K!+VcYU9?H7HdK?GEzx922d(S@{c
zc&Sk&MrC>ED%Z_`NOh&^2?3dlsajyRnms8&z`zh)A^bO_R3z)9D
z@Jv#M|6=+oQDQ98^SzfS2^zrbsOCN8QhR}^sDC?t`V>K9B78NKK5@5XNSN@0a7xHU
zJ`vgHw#%GiIK9m~KV6}koxVdfyWvkd$~&}dh2(G9@_S_*YKe7CoZ`f=Is!_
zSzPPUi0#|EW%P-fAeMt%7PX#HF~q?;NR$L<`(D
zk8D+uT4r7j6yo;yY0sU6f5e{TrSe3p<_3AFvg|Z&6Zvt9hyM10XlMuMNd1C)Z~qH3
z-BJV|zNC`-9HO$#^ym1DeM
zJ-1tetq$ozSmxl*_y(k_k8EoK=dbKl*nabgZYqTQ&HA$^*TpQMe!0||o0>=+9o}hi
zzR6~72&-eMoDzo?i|W*2RyQQ2oE5KnuF;gdHv@jMxMXg@Wcnl8g0uRZ>w-eK>3DAe
zSt*H&A(B!yHG*D08ibl`QW|C~_(F7pP=}qLM)d=g8U6U5#Ey?c&N^)SO(_hPp=WFv
z5@3nrXX>j|Ioqs|t8>%`$BOD~M$c&;o}6W36;=oD>{Ek&2Kb2|g|GDx=6)P*tD}bS
zhw9J=Pjpu&UQH;rwcCCyuce1vuu)5^k^7*x_NBrF@-MUDgpoA3S_59H-F2f{p_s2(Nisux}
zJxrf`L4;Zk9#@4@CI6E3eI{*=9h&f|YdpA8H?J&*`derCrCj70A6xNK#HnHXVZE?8
ziDztf-FkogsyQyk(5~+EP5pt((60dv)x|icU)IG5n*n)XD!i77%=>t`+0C#+9`Hp=
zAJ%?gvoJw1WhRKuL;`HF?cN4aeHHH1wt1W25NO$hYM!Z@PU2#Vu3UfbRW-d8;dj|)ubR)oo*MSMWsrsHPHn!pxFhNoVylxcY(O%__Eb&47
zSEcq~D0glByEL#T40ph;`LVgd^@~
zJtb+;9&aNp7`;GO_kFK$GZA0e-XAU)6MM**$YmM3k>(#jbH^1+Rj-WuX?`A_{cuU`
zlEsaV((>S+A52(#Nb5Zs!aj9POxl!?WIPu8Ny>$)A{EjgMzjL`4;<&&1zJ;-`ZXh$
z^ILoss=ZmYowdwZa{-ya{2Vk3mzx)DxSnrXaHuk+QQIKQ}47Gwcrw6|QY@go%RG=Hw=g;}gp9?AVgcw3?w%*wq@f2h3&-@~RQSm7F3w%D~
zNhdEHqm$c9%NK_hZ$h&Am!ou*4}d6#b&Q@6v%fp@1Bt;eT{>
zm)!_d2)eJNv^w|-LH?Pe|8o89#-n>~S9Wd~n0?t2t~a->)vdX~eD=&UBVnTYOb^+2
z{h!A~p4Eb}$z{lysq@p}r+HRU(v!NLmwVyjzI}C!Sx_=t+@}A<(GLs`*sud^_F4t)
zfBW&-W&nkbq>}Pfh&%qy_@iY1y)DAbk$7paw&wIqKYp&VAqje{#2X{11)F<9jD~#54&oUPj=#qY{R25AG
zN4`{C2`%8dn99~ph`RM%5A`4ZD8W}1w4l7!s@~uGT95|=EAJ2&z8UaTuBBYs
zWik0Dhb$LMgXm8jKU!J4Vq_UI?92I+^YXMV7k!bQ+5tE*)*XS~p|va~{lMgIX91H-
zr4&G~5=3U*8WVZ}M>gIp`lwb@E~vTSaL;M4Zr$_l4PKj-!#+0rm^|O#ota#5g|gwh
z%=mVZyjIjgc#G9A^dj|Kjd<@ANdhj}GgiVqmlcu$g_
zOy_H)l`*u|q}{Pq?0_~{V3f|-58K!0=9QnLFW#P2&Vb96^qN2$^36VJVg9=vXhMIm
z+VcLaja6u~u#&Gd*X-7G>CB9DnQF0So&j>t0UCBJM}Y7)Sld+D!;qK*H_WtGbM5dF
zd)mxM=%&dp8T?(BR8|CUz5aTyNtodmgLU!8R9;0lD|TE7=k|NK4HTl*_%#T{ZmiPm
z<>2vReyC#V%+0hp^6m%q%HHzkeynlp?Z=#LB?xpL}mqo~r5>;=YVZ2o30j(+^lnxe~e
zGF%uWntWUcl!n*vT-l)5xTrQNG31j&Aa{=dc--}OP4vT{W>FA40pQR16E{EZ;WMkv
zyF9J`nS7E|$iC{X<}dm>bNyl^!Ebc*rQEn8JfoYM4psOSBJ~D-^0uK
zCA-spu3WdV#4hE*__7^0Emhy;kdTa1O0$P2Z93YbqLEeYg?!g!(wCK$^xRl@ed?K)
zuYSw2k=@Ponz5hD3g1fG7&swr8xl`EC??`D3-!?0!3t|}UK7Quev?b>b<0#=sf|q%9NN0$vXtqA0H8QMe
z)w%^RrMkRucE=a(AlKZF8X+vLhLDpFDRS8|=*7hLJS4GJLl9043_K4rxxs7W3h
zR4pJZo5PMFCwv6*Be6(y!a_SyYbxlx@xt+8xilnKq2(Oq7b?a?a&>Rsf82gw$%@6@29O873<@d?nDAMH(s=flbz<}u`cic
z8wU>2Bf*#Q7N5<(ugQ+7Sh?c;Oy!jTKhEA2D%8@-I3DR*lOTyAd(YV2w4B)LHm6w@
zCE@6BzGkdo)cgareJX9UEvIjAen&G23?_uqt|f#$!y^u$?pjUq!?r>$IG4Yvm1z5+
z>?6e;`gOZrS46$7duXpG#9N58k|xR8-al~iwzaefkBXnpDEO+e;oUp~wlP`=q~>|*
z+@a0)KVxxI>FcUTtAM)}+WQ+tjssM?8A#KlmF=f
zjPoWT$SaQ*8&m^+T|2BYB8K+yfaXo#q1(C8>kY~sN5T^40f34K=Bdzx)Usp28JfFpD5j?<8l23
z_S59i`eRE@m}`eGiCW1H(0^B=yQD91X7Vb6b#>%bG3UkgSN5Hb3Rk@P8mpsLo6ce>
zw=6_G_Z)eejCCav7vJOb2d?i&j>|0$_Ch&aJll*Xa%Fgd1!Oh?!cZ3y=92zi5-5}o
zL{k6nVoyob|6Ab;A$K?_83K?e&fWGf>vzJ1WB0H>w5B#dg##Fq{0cBd-d`)CPFUmr
zn~n(4I~||@TGua&mT4{;i0F|K?htXT!q%?{zVI^P$YJ(Qw#F%Jpngy6LE0oC)T7aD
zHB0b7?@Q+IqReRYTmnf@u$-)1h#}0LpxB(B^9ol}?+gr{RX-B@CCVv4w`FNa0RIxx
zH{LPi`r)3AymCPS(N)xA!VuPn!PTN*Eh?QL{&H=SDMR)6Lgfejj-h;lJMq6^dQ5G~
zc&d9|J5)o&_*D(u^BvaP74R<%KCQ&g5V%UUbwLuzKa-%1|3CD$^3)b0mD8m
z&^33#{D;=rC-Mr!>N-n~3=yL6&qPw2!%fPHgZ6%-qJn565_^2^hk|I;dF`nk5jc3B
z#}!Z-%fj}WU7Gj$X&bR(h4S`@`>c_ijiD;ZMvshysJV_0%*!9z8au5%J!@MRBQPz4
zj%9>zL&22Pto9kq1+(*~Zxq@i`dY2SJTX4K*FqE3N8b|{==fs$RKZhyY|_YC{z-0>
zFr-CF=b50PqDkr?LL8$xMJ*yh&Vck{2Z1!0sQ7b<7{V%OC)}g|_ZkzKS7XxV=I676
z!3&tVusfzJ8i~(LSKhREcu*U9l}j}$?({Ik&pF4NVw$2=w()^0+D8c0%}VbjyPL{3
zq_uu>N2Ii>Z+f>*9Ost*=_5VT@F;4hN4ld@@J55;yOjp4@e?HCVEZ+1a#KW6*d+Ra}YSXf8&Ft-t{&Z>Z+kh>4u2Cuhd9IvR`c1<%l@
zy5=aMoyQUGSN!+2+kK+3)l@TEPA@chEh{6dd+&L>og2l%F5*qj
zUNcK#SGGg@suYJ(s(25)NJ1|M1%yHI5kdFB6*5})m;|3dB=p&(qdOS1YJbCeqmf6F
zq7ZQShAP}|{;ds>R8L>|EL1EUj(Rgx~&~ug?&MguouVeK_7vf92&7dzy
zSXt?Fj@(s1ExF4%Ec596#AOw^jW_o{p-14)QV9N6xmK~tN6#NZ8H)RoP_H)xT#Ybz
z&5O6+ZYFEO;#~RGxXNs^pmnr}c^T(s8#>2WksYDz=bAXw%YMznT&d{%rT8IaK=6&h
zKE-C33~4SO*fMkOhOI;Dj6)J55_M~|TUd`CZ|PY9g-E2S_L0(Gh*t=88DjSp0jIRj
zCij?1Ye}Qf3ymKY_cENkBW-T$lzaX`lv`U^~xRx}7@iX0_f&jf1p}!z1
z4Z}8s`&Lf?ta`^}GB_gW?Oc$mAcn-`1^>}Fp@HyYAD
z;2QY{D6p-*b4N}0z=IOf62)IPl^^a(a0=c?U&RDum#W@h{yj-q=^e_8-MsGb_DRBE
zAB@JIeU`bHS!&xX$n2X(dNEOjiB_4!zSaq+WCVd_Iq!0B{Ps413dZO|Sqs`*j49YS
zvcvW+`sIcu$ih-s?cIMSqNzlnx<8
zFje2(z20lBpCq}aX>s`jB;Cml&Ri{^VSW^s>Mz!^7~BqH|C!xRak}5(B1BDt{JyWx%8p%jSRW-8u34wLJEN4B^doyqR-8$Tf$;Z!l3!IJq?Yo
zWk2KMuPYqE8%y8o*RZcM(kXNu#J2uZ1D`gJU+Up1oa^;C>c|3{7k^^AeXZlI!O9
z$|mNmm(%^;)TCkBR`LoV6IGr=nc41MNIzC)y^?(4!QGyAE?1T=O((qkb*|{9;)kr*
zcSTFrhxP~PDiq5`Dtps9QD&pw*t2dd)t-(o!LE14N=S=NH=kX_ZId&b&2l-!+9))E
z5NZw=i&Ocdi&zhC|EpZ+aX-SfH38^p%iKYv)^CP4k>g9bb
znEl&Ot><^+Ub9#81}_POQV)ny%CxQiaNq3JFv(DYM+~2uc$0lev8_Z+qHY*
z1nWHb>!Yq(dTSb3g1FVO27$Ch_SdxQl2g6$6Z`oLqCB$=oWDJ<3{lcuypeDSdCR+)6@i^-J2KbH|wve!!d%j+vazs_wU
zk{SYOo*$ND^};yymTw%)?ZQbzklcW_idLR)s-p?FZ`>C0_M;`+XZ|2L9e)5pW}g&b
z7GKzJr|1Kd$Mp)FT{_hL*#U~85{x8``Y{-K;QCH&$%&UrcR418Wl1+}(wbJ@^G_L^
z=qUNoqw`87MCFG;Iq>N{k&uhx&u6-c8V<82CAI_C5WUyzQ)51D)02=cA#TS$0B;mZ
z=Vi62wl`w5e~fBS?UPy&+{!43oyi~h$K3rJ;!yvXJ;35cnVIbpn99N_AZf09#Btc3
zMEVWGwHfq~>XW}{bf%&~n2kS@qs(9;fiZFVJgFKT%7hml;BO}VuW!_lWl5W3E-3{1
zJ+)--4{f+7E-=aE%T?9KOhv%mXRgU60uu;9&xXf6uus>opu|Yxvl(Z$v--K+Y|;&m
zwgLoYd
zX`WCCH@KfUXogxZyW%AFEy}>d(%FO6n}=Qu$IP|q6LrT=RBv(ova*_}Qnttox0^dH
zY3LtQzINN|{G3A)(yve5gV^Tpzal14O-{=k5xyxTCW-s(mw@m>GGJ_rSVC3o;$gy2&?AOw3EazfA)aKz;EnFm#sDr5SO>5ZU}VP2BGe1vlM
z6Jnit<;baLL0j0qJqzo0#@))c6T*R5oK?l>o;sy{(($ZmDpylR-4iz#Gvj!fbMq%K
zzPei}f}>_lmyx3!v2#whsb7v6jU#M2kw;*u&CQ-mdKu~@+IyKG+*^R%_AE`P9_nMwkqJ3m}+->)2
zAXl`)cX~e)(B9t<$4`KkADGeI1(PE=O>abUk|xpWiG~UP$-Rgz&^73_n5^Gfx$%13
z3%6mC|1tYd(90X!E3_6O(lP!|$D?FVsgx0>y{u7e!paw@e0qd=w8!Ko9hJJnhqs#v
zXCJVJ?x3{HI3{Q_UTV886V2JqD{9Qd`n6**#f|92);B8Nl_v(f^?izP^~H_VrO*2!
zTkAh6kxN_TOd&UJclnie{j1&L9G;=k_bUih{N3v_&ZaUM31+N4;B0(aHlc41Sb)KE
zXW+U4Q_iaTu;dWBziTHLXeMoK2(}w{`+?&VUuRB}GG?6nZ%OmRnD`JCDnIX}0JpI7
z)6xc2laC1D*a&!Nxg%;NM8@wfHq+WHXca^32fg(!W28q3mJkb;>WC*-gMN=>;}
zdCm?L=*qh4#f~>bVS}rw-%HoZ$g(vPHY}6ndRVK;S&7W@YBm;CV)W3qEw!`uI2Ndo3{H;T#D@FamWtjsQgOZ4*wJIksJqW_XO*
z?g^@9{6e>clD8XweHai>xeyX!iIZl0=#Zppa3Fb}Tm_9vjQNn1zM}B0s&QoPO==bVEfT$Gy9NyRM^BbT*$0>QsJBkz}tH_w8kpG_MW~554q
zLF4-B_H)o*urKAcU`|W+uvGCJ65Zo(L;}rILt0F#A4r26ntZ85`h3JoiceVLHfr~n
zxU>5xo$McK#+ac@JYf$>qC9(U#p*wtpbEm}+7N~Ok5F6KW+u=!qS#sn11c}T5B4ZP
zUBrWqwDIsXDj}pVh|Bt(C&;!Fo$pmXkthEv8ueHq!`KlpYzmOW-X4WHl;l!vm!b>lG@LJ
zh7%>8VT>gS(q!E0Fbx{RiRWy`{LM?bxAj51d=PgXF+-kBEyTPpw
z9ibfpYLwnYpVS5kZS#ma%S%6E=gjE17V+9jH*S<6vOu|ccazVzEhM8c3)$WX@wqs8
zs%*l+ccRaY>igfBoXGPoF+**Vbh2MP#HNJrkbP%(6&vE$r|hU>cbeyzKAFV5eMiNk
z4LB_#G>_kv^~cxAzI
z1Lmxxk&o#GE>}fYj{W6k{P*hTbtF49MPdxkI_>}s0T
zo`gUg{C{`ERXBECVhCuXEkH0KPuyCrFQ9
zd^=CNhDiN>k*A5{#mt3s!#ztFCgb6B8nYDqrMa&cLD+qJ)bB`zpS+Izxm(F*0coo|
zH6mD@Y1J2Ahi648s}`bO-%9kc)xlz8k6|968_tNPuQ<-@3Y?Q$FY^4aI(t`q?i>wH
zm&2=nsoxs9T4nm3j(xB2dmehBZwFSvua6QfOL%XOoP&8SjEBpVrQjEZNaF#
zl7vM5-6$$(aC3JwP@7gu4zbrS)q?dwB_}ESmMXO*)Go!l|Bn}*S~3lrntYdi#r!aS
zN8&SKp{-dc&%FD?WfCEYG_b;)+WCL{LGfTu1FTnz^me5U2$%m%^SCCSqH3+UO?(nK
zpL^EqyHLjMcL>LVtt&zpsY@<)&nO5cwHH&;BJjQLIAIszd8Oo?UT;K%o#ju~&bcfs
zoI+LlSkR{u=$MQoyQME|lx8w|W~b^-*}>&Ix-Z^r?R%SfK%g0QN)_p6vi5b&_yLZ?
z!yiV$EI4M+vNHSLRb4}*aMsZd3TSz^N^o~d71
zITbZ{7lZVJ@n_lC8Jzb!1!Y#Jt7tgS%pegfnpEpkpBTTZEV_cP#Z}I>Z6)G?y8STv
zDFkoX><5*6HUp2+BB_h80RCI97Z8PLut`GYFMSO{FNrvHh8_BlA-o;NhiwJQ#?xT@
zJPdSLl5mr_`TXB9Qtq~h>hlOI<*8RL3xUjj&fAa3I&}vr-i)viJCi467ePMi>_E`6
zc_5%QFj*v1kG+AZ_sok9oH(??jBEI;rq9RiEOETj8|-O&CMd89sedF{|5ixsQWzBLy33y%Z43i}rohfsH%r2A!}X8o5KdO|;?42bDOsNX=
zoic<7lysvL!-2_q%B-G56YM_RTffq#RvXqEwWos6Ob^HzGe0Iae$etu#<#uXk~jcZ
zs!jWkcPF&^CK0wtJc#QolO2H@E`OU&$IrFF|LV47EL4J^tA1u0+_%Vi)h)aNv_QeG
zWx5wM&=)*xHt7UwaafxP9z2}r1bwkmd4l0do9WcvB?8NSi7-4fb|xC?BD7G7<*19B
zL#4NheYly7wi_YJhzWAwI{_ufzWuj&$idj>TUH+T9S+IUl*{t(UKkN~V9z&tp5Zms
zbbVhKoHA4QXfd6CELrg=+Y+_XZtc)%leC!~-TDpj-Rf5~%kTKEp8JfIy_YY`DLzu{
zg-h+BQW-wIeP6%-ay^mCbws0N3mJ+=z1SptcbJMXFLg|Bt8U^>)F$GK_nwZTLH|~9
z8}H*T!~wuPsDzXk&dubT@r-8*s8HJH;T$r?XhzI-QWUcl-}}TNc7VLiK=H|ueElC%
zTiO&goPn$L?UoJpkf?-$`gL01onv%FFT_^7huP@x0odHH!#horvr$h&QIkR~ny1doZc7_b?J(
zP{)jdrz_zFso?0G1e+s!8+sV4bKEQ^+rs3I+~WuzxB5HSuU3PN+7b3Rl?J1U+^bI<
zWeB1;N0rhq?ZRfBdFr~lYFF8RC)L>I&d7kn91W~O`N*5-s=&sf_+6Sn95LW3Ijrx+
z`mCrQ1!qEd?Q&sHkvWnsVkaEM=Lx1jNQYb@ziPcKT_%+tQD|f#q9y3)F+vh*99FsY
zc!Y9P$iO#hWG<_9X;zf0N&)7G;l<@UzfeUMu=q_fx!7#^hXzZK7{j}pn>gc$F`Y_~
zsIwVDGrgU^Uv~VoZuAE;rZ%QZRkV1i4x=O!oxTX$N2D+xNmlU#S*+IGY(^9S=J}=@
zOr_7QKRK_onH?j{NEuRs8izaE{-O!Nfi0+%B#XfklH2zG1c#}xQ@RiJ9ktFN6#
zypUxpha|_zDL7}LmYR74?3&w%rE{^bh%xTDcL~PufWRKv{9JC2fMviPfMK28><0pSGM@)>r
zXPI1r+uU%+N&b0xsNY*sIq+ZcPEn3CV2u>{V6~+FJSWZCe;JBD4HxZ$qc)|pL}X%0PK
zrn7nOUxN2;ugadYN+D7)V&MV!f|2YgA!xZeTsV%3nPV^3zWP{`8TyZCR&(llTg}ho
zqt0)=L&4%Bm3{MeG9mS--B&Ojw%gs$d+%!BF-DG!58O;F(YJ0vU3KURBzQS05xP;t
zxFqFF|D(@}c|xDUd|lqvkyC7&vG;Lut3C7NoX|5Jn?AP88*D_&xz)eOk%gs|lMna0
zP;ezjaDdK{kp7`|c+3=wt@kKIPO<*k%|xq`ShF=~R0s31!zb|ULrG^rHjyP;n14wB
zrdcMD^}-iyZZ9yDyMA;ss3f14g%{n;XscG-k9Z`uvzF=gTtBXTvUK3FJQ7!bSS7vL
zA+=_nodz@DUChFfV`4BwL2^=qa>&6Rq+`M`)|dEkp3
zqQ1kJUmpZ*>mv0=uTkrmJ4Brs3sDhxbI)`Pfo-qU=Z-***^7<{;=dUA(aMHTtMWwL
zD-kebb!WNX>;t1-ey-ynB{r~^GF;<{Halji>Y=hi)c_s3@coGy+!XD$G>MY^{@5X1
zxg1vac4+VGrR1Yj+a}6rTO@nRm7nsek
zp?!p_m3{>O3_R^~$U8eVO$Ugohgpy^dOm9AK_D}z|{ByjgA(|7`@
z!OoA3@?7iJR4jGNX?xnf%S)AV$pJvtZM%K_v3z%E=>slC2o|Yg^%jNU$$BTpgehj*
zqvz#ly*FYr+%l+(@t6j*@0+?b)K=c}%=|uz&30Bw#1Dhe{@tc}^;nk@(t7+!yGmM{
zY+IhnoRSgVu;
zHaeSR5*Ii@%`pd0b{4sl1t+ytyr{MUrHM!D1h5P+-G-iPLoW^{m@4qX?NxLPW)WtfnBcEmY@$5uul-5+8PxoDe`~Vk1dm{AG0_li<>7f9n>9)Bx|g;h
zB=5y~J+@C=^2qAZG^!_N>c`bs#(!+bNFaSq=r0D(Q=7IGMKYgMRY036f2@-$g4%qF
zfmShA#Ql^iz|9&W>RBc+m1D&^l~Kew6ZSPS*u3T_hVU-drE;tf`_LV;F#fQ4G(O?Q
zHADtmuCCl22U}bs#ee3pcgu{y))l`DVu{K{axLGiD`m~?D(z0CuR?OnZZ4ix5*-x0
z2llmNzoTOr(58QJmY!J^@r3oXXu*&6IXGtgi
z?LvGNG^tFfLKU2x8>*zWS~xq;>|rGD=rjHaMEg4^5ZkcZJg)fvNc?540+X*r&{+}f
zRVAkY6Y|u#P>xY>tsR`r6Q#->g-iFg=UInTAL?
zPIHVavM=}qO2%8W?X5$r-92pH%);l+Y*%^bO{G^Uw#aQIIMKLSkAB;`rUGE}X
z59ON7y-`tNZ8m_Vn9{2*w`1?38@@(78?!fM1;_Os0Jzzy${O{tR)<)z^}euc;*&d-
zjw9Lzydj|{-@Fm>FX4VhyB(b`6>3tvMc=>*C~D#e1Bdio(f`K~KcT-$S*z=j?|~^w
z=A|E&aP97t`Qgw|1kIXU`k~0cT^dDQI^zNRr=%o{UV%DWPU8|qTB8CG9^Qw4r)C^7
z^ZA&6t_&w-{ilPpjQzBegOAarpaz9~Iep_yYyKl4!*Z2o3G9)GLNxGDDLkq!KDm
z1bChA4P@SgI?tCd7M^iy9A(otS8W60G>>o!Vh_<+T2loig8!@rR(3Z#OQYmGg8OENjJsZ2qoewnZ{MMwViAR1PfrGUp<2-f(M%yy
z!H;VS5RAK?A6lsF!7|?p+t1FGaSptFBaGTmKJ();4z72zu)D+IVM7wP{VeY#kYlRr
z?d6$96<5Ydo=SuiJn
zv=_^zv*%JsG84a-@3l5ZO}|l^1P?12%k@X_%?IyxL_9Px8_nvkkMOp0d77DL-WG9x
zubJ|{A`X6iv5U{Q$U*gdmHuCHDeXWivF{nzG^m~u7GOSGUPRXPstj!GENDcB&cQV@
zs|k!b*m4(j?EL6ZFSfF{pNZ6v*=>&C)wq0R1_tcy?T+<7X&
zDi?ak>0g_7e3ViIMz#?-ZNFnR;ctB`^$D)id)XmubY=JO$Tj^kiu|ri=(-`EMnjjcA2v>!~EsKXpSN&-p&Vb2<5Dthk8ll-S=W
zTwkKsx2!66rqI;Uz2i;TVvRX@dh&XASV>u9b)ceGCne8TP=F=FLaUFzJ62TuayvTm
z)>EI(rXx#k_BKQe^@L2$Ej`gy5Ng?6fL5c87pSOk4q~ZB;(g!h&Na4K0EBF7UJ5C&B^~%iHmZ|*sV7xuw@<^`tma=f
zk8fQ|f3slUtab#ZCne%|i68rrceT!j=lvp@wv+eRXQ-qn<&LarIE|*ZB?eN~{TC(HTeRU$*X)
zf@vLsRl-+&h^Ea+7)H}=)gu}a*GvhEit`P|y%8i?zr_w=e`!nDghAUC9Pz-Zhjl_n
zrM@I?Q~sioCd+N>XrG;mo7Rsr{w-sT)_pPPE?>LEFkUh4cm!gnzIZz$q;oew^s?
z96GYluJBj_=ke5Tg^4c0QnhnILqL?W*Q{nl2{
z)~IO0Jo_D8@!}TvO_o>+$HjeFR$CUDU3>soRByuEjoRQ*FU<66pNF~*#1lE<&R=HF
z#u%ZUhx*FkjP!iWe+}V$rPw|l39mo^N_WnFgUGv?j85gY
zvrn~+4=RLATFb>vE#4vSp9~E~!yX)i;_{oFR(TnH*mRa)YA7mQlIZ=4w3oXloTv=9
zG*p^{Dz81Lu^R6cV`kRS!(!e5-?-A=t_kop=Nh&?>GxU7ub(B5pI}3>X1CO>-u!-{dl!qB%1P?Qr
Okd0^)*_*BXINX!PA?zo9>C0fk6qTQf|C*lIZ`#l3JE&$^kjSWg{
zL?119n7;g5a7U-w751s;dW}=e#0SBISSd-;STDT&>(QZl7q&fOfu*ev_`Xke88Cu&
zh{mUt-ene?^`Z$|9s4fhgnJy=a=IN?wYvj#^2Bo0-eYr{wv7pPG6*bIU%y!Uzsf+HsSbT=isEK`czbG@iw1jh78+O0pD#sdB-KnJxbvp%Z
z1@5pckW^t-cU?`9&3yj0;9YltLgCi5-fH^X3CxLrtddiFF0;O#R>2
z$i9ci64Pg#-iBSYQq$uunU`7BYNEEH74^^D)Jt`&sk@z$iq>elDd9?J^6WQfmcv8r
zDMy{Wy5mY{LE}^JZ;d<6yepEgYf@s+al{gPB3y~J21WUa78b(-O*x>zOLsc-@{4
z_iBN&FS%9MH60Ni^)GdU3os+g&JJ%8PsQ3@c*PhuFRq0usCVqUaBzFiUp#LUy+7lW
zQJ|vrpa+!VyHsb228IU(ER!c%AYMt&Pa(SDvmbxG8nJxlZwgo8x61Dw(&I(G`p@oJ
z(-ALV4v&;ZjaI7LXr?LEjbc)eKn7PRZ>HYWuLxw-U>{1Ve+x@~JXaNhc9?DhUaA1H
z75oa9U9Ci>&Rt^$_NlRlkxv(mM6nmIg5wSt-bMm9p}V@rx0yv}`r&iy&Jxb3l-NIg
zY4d&T2@&=+nY&FIwLtsXq-#a78zf!3y%0aAOYo_oY&+^Y>-CGTnP5AMFh!OKF0`0_83Xb@J)A4W`9Mu+B^_(J=3siK7>H#mi3r>gdx=T^mg$75_
zbO%0`C_+JX&x8B9I@#w5FBHxdlJ+ek!J=BS?~NL=0Hr;_I`OS(s)mwo#3pUH(k|}A
z$C{yvvA6~l^7JTtaCfQh;BuocRQx8WMh8A|ERPp64}y1b!;C8E9(I@?dY&c?`?)1B
z*oT49pFWi?O#K9x=l0U%d1#e6++~>_i;1bmCbLEMq||C3L1)6e{ghh7dn!v>wilM)
z2TtVauR>QfZ38|9?GHjP9GaT`0LodscB2AUyQ>I9cS#7n_dbSaz0f^nikQumxvkYu
zA^g4=6gn~!L7f$suRlWyNslOnt2l(vyrz`vvd`)H=GkqZOji0+-{h_TN=nk(S~?AkmvdNL54j&DbMkmVM4
zCA?^>hR+iQpWONK_Fhw9R>(c)tKq(br#FdvWj>UJYV|4?C6qJ!LF;rxO*sLmZ!P
zS#B9pYN|*L729BYbOs*&(PKGw1SQTLj>>S!}qf6qy4%I@C;usBB2S=_Rc+t
zYpT%q|1kF6K~270*C+}KiVzhAsSy!DL9l|fL_wNJ7Z52?5$S~9LWoKiq!$qoY0{+k
zk_1Jm(tCi=J0TEA0trb@p69&hJKve_dC&Ws$zRN5hWom&z4qQ~uf1}4%K?aWnCkfM
z`Az6w;#c|d$RFt5-PD6OTMrzM#8wJ}J($3u&%DRi{*@>rN`Gs4cDFy>`#pQ;JUeHu
z#4xrizaqSHl=Uy3;5=frfw^$B=*lD#fn=*ard%4^9mFZ}TkraREgUpOq2IsU#60NU53A|*WOAma@-o$;G63Z
zgzTN0ZwrU%Is@pz?B%!_6x^wlw$dx8yG_(iInvnF!XCQhPy-6py7iK2z)r1yEAGq@
z?Vp%#Apfp}{zV8dci8@G>_Q1*s-;>GR9(?oAb}?SzxEIB&t^rk9@4jceY4-7t%z}S7Hrz=MykBIj^y&UNMNx`D8R<}GXb?opgi4huNW+s0
zwhn5cf;0zMOMbyDZQB>I*a0FfB5*J?nH3m7vcd--qUwBI-LwN3LCv?8#c4m2X6?T>
z{N}hRHWzH^$|e6l+U~S2KmKO@#Ilb+v)Fwd&x(GYyODdYM%Ujvgz|9RMVP;v`0C(R*CQ?15TcGm=Oyco9IEw9BHkBMyzh#5Um39GN!L
zu{{IRVQ|J#;opuNbtM1CgZj6X)7$`u+c{V@?es69c3B$oi+r3($J!Xy&DsMe18(aGn|mbe0r!}-hUa|5Psn4!E0$|EBZop#E%EqZ
zHhW;jH{)=>xdcGGV&Hyu8~a)t5NDsBF?++{t5D|J(9fd8LbY5tRpiYqsmxYnGXcJ}
z%P1$9{eT|+mH_Q$18IZ6Ly3N6+KBvKYH>OE&5M7Vdi(>&szi;sYYZ`)=0_CFo-A|A
zp1y^q@Byh49YOh%2Oc_>bsptvgt8(m!W}I(O9lE(i@WPTUO+_(fx4*W0f)I?$6A^o
zYV1v-E=Kjr_iKRN_CUG}i9hift_O&-fK-8Fbf{}cx2rGtTwZ=?Z;;%SRz7=vG0e{5
zM5^4B6WD+0fwlJ%W)=jpbn){qfqVGxi;6avz==v_W8OJ~D7nr`Z6$ay&D3i2&@Lj&
z|7f=ZJ#U;v839x1fS{e+(wJU=88UezT$Jp|xIcDjY
zbZ82C^apz8LXJWq2X_5%YBS;;W9@L>>5RmMf96Z(X39~+X!gdh^jg3WJF|=qS$Z$<
z=qG}nFAHCf>LqdBL}JdT%3~RBML)97crH?`B?fNaNO0#>cIN)h4OohSj6fFMFo__DqoJO-V4LM7tK@M8k
z!3T*rSqnzPrw?f7TO)+;Ipm
zZvhMkZT#r__;geou{1jQQ3{?^YlSNT&@4Tek?fwWPu(}JC%IqMf+r=57G#FNBZ7{W
zr5O^N7GUBYm;sn2e(~s8!Xx%{0h4{ez=S|6l}HSasLz()sK-mzg%p5
z*#7k(eJg5)NxzMvY>G+i@_iksiLj*clZQjk&F!Iw2OZ2kCNKd2I?{*0cIGt1DB&Oe
z0aP(h_vZ9$bQ|)irP0zl7Z`i`A5_*|2+3h
z_?1xl%hL~VJ8SF!551kFaA>B`(D$ao;jmygm@N9DM2_z2ciov$RNeYF75}lW+D{ox
z#c&zDd7ZkOlbWP1-V;%*(k6|^SDlE8P`ZXsf8l<^qP`b)onrpI6pJuSm4sI5
z3kGQTcSLYwS~_ydba7J}!b;XMVp2u@pq))xy2lEpaIp&a)RR5vyN3LwlDSi76}}~2
zDggvfSMEJ@oHaza?Pln_E|yEKLcuI0nOLE9$0%UiQ=5t
zMXKmsKFdy7K10Ufy}Mvqn?C4pX$k^!=>n%e{-+6e`m7&~7!Je9tfnI<1&9rN?W2~W
z{Ein3A`#6Z+wl#Y1lLHI7(VfZyQ5l)&yqMktI+sgkLvEuR!+)|zL`jxPrQsr+lyVd
zAU>PgcW==ljRsFAfI7-(x@3e2ps6qU(qHw`=o2AV#-0<5td8rKLe^_fQi0*Wk08mF(%C6bN@%Cx
z`ddb`xok^wQ}1}JKJosrsu=gy@+JIow5GxJHu)|-11jYfONv}Xk3j^x>|ji;Br8PN
zI^tLEOgI~ay40DNJC4#JnV*TNz9^w8!IwV@;@Y@cpi5nfHls$LQ0+iw9ZbX`)+#%;
zQ3?#%%@FONf8>5S_v?yVJ#Buv13{1gjhsAqtmA93fbD=uZbwLtQwvNpx1$^O2=oZ5
z1c!p30g{mrjw^l_(`~-R@@~3AXzbzQ=`)d=)BtZZIh$Zob=w9JU`gqBscd7S2sVG?DpE$f8b@r
zkC=gvB|3&%Haf7HM}JQV?+1Hb>gjZ1i2T(UiB~Hi4etGAN8!r@8Equ}ldFukF7_e+
z2$J01pPQ>%r6G1@X`?ABqvw59&yw}ACk)Bl{Zt9e0ju%`7VJMe@|?$<98-h^i#}|2
z2}d$=fV5hDYdqSSOpj7r%H*}hqa|}Wjbaqc!}=$R#t$t_3l!tPe6Js_YJ=F`6W+64
zdz0zI1E145uB&8=IrjN+T3(x|*kDYH-k&ygUQO&K!#_(N(bUpmr6X@WSaBQ
z2oh1XooR@SU7$zO7io!9k|k?CC#C^h|CFXXjj3mC%cgzV(A15H@$<(oCv1KBCammszpd
zCoaJl`Fi_BsUFNdSXAT^%`Dkzt0>FYXk@*ImU<7P$=ue!y1P`x>N#fzvt=_ynIc7X
zCMcX;0_T3(CBf)t6^@Aj)rbC)N${5=@QMBE%%IV(5q+7#epKDCscqn;iK|7ksG5@8
zi)N|iYXd0U=*g;`_;~%8PmaS?iZ%M+2u0hWnR>*cJd*1~_CGY!?Rno?nl4Yql88`h
zm>hMa9y-
zMq{H;Ywu1mAg+WDln2^U8_5jzelwU4KNt~p5zU<*aZ3RU9hqZBOix^33HT#I<+
zxj!}0Z0>W^ojy)0W{Iw+3I?315@zlkYBw*NW_0>&uIz~JOXjLT%`Uz0ga){RcU2*&O2l3N4>LLm2CY-&(>3mYDG$t}VYG)|+I1$yENiXqGq4&p2pP
zN0_85J?t2~7@m2Sx?e)E@U{)UbFVI!+P4@BrV|eff+Ye8V*e=9rJj5*-!h+8?i9TI
zRr^H~f{>E{6WvZp+6{{Gk&$sA(>WEUm~!Df?hPVc8`KiO2z5xq7?HW^7?Ai6NfFSjS_VrZwoJj7XUY2CNw50aU8Q5K$8T77j_;SbcwZQXL
zYlHF3VkmJ~--=n4rEG~oflTEQk5nw&%Ly{Ga~ZlZ?-W%P=u#NlQ
zyDQ=)JA=*^R4Bw~@`Z>T5?UBJNG!}D3xp}iywliV5IzzNU%h)jV>H(Db`x0P=MT?|
z_b^X)Bw2Zv+HRTkg-4v(%b5`p35gEKXr@*C3mZtoWrs{1u~yCX@sEjc=Z7}n_W4T{
zW>eQ~&>L;;P%H{Y?K)C-QoHicnj)PKt-T~fjYr3DSP$(i8EpN0Ovi9Ls-;6UOp&a&
z!h8ej?Xas$m#O~bJYkIXP8X6fgd)GdniLg8>eZ!gqwS6R?X&1HkEWU@%<3@Vs|`XD
zb+wPC(uT|hy$CGbd8M4ZiS?FK@QIqkTlV#OX(2p*>3V{11QkeH%3Ciq$JiG>JHovC
z#Hpp!ZctU{GmkS9159N?xFxgt2nVGMnswyU)9dlm$V9Zg%i2Fo$J%G-V%N5(ksXlg
z0JGmSv1IKX>APZh^qh&&+f=FqZlHtkY8%~x7)I4;!fUr_f(mj-MwK$gOhWF4$X|dt
zM!W~3#&kIDk8ZgLmI~HO$>=(LUV*KGm}B(rgr$GGu3(@x%P~P3vpw%NX6hmeozklS
zPek-sWAlRci~HU0j};>^^#DQ)yhfInxsADA0>??h>T7iu8@w0Wt$1x@EZ)ohvlqmK
zzg|Ik5ht-_?o$HzEJa@wvt-f+k@YM`JW|>GQGC`DEE<8p*N$6HF}u8I23L17y!SYJd>DH89$T8fkh`xEGOoQ3A~o02DDy_NNH+JkloJ>^@-0LCbi-6i&A
z7Rzc+jb;WL_ux6U|1*V}2_8e;B&fvWKh|3`!B)4iNSJQ{#lL?VFWi#5hfATT(^zk#
zhxHgl=_ECpY>o~7xq3c%x)LTk_M8XZ2ZSeA1jD@svfQ20h5S8M
z?~_Et10qWl{T;g1oz$-`|A*|}u*D&b
z+$3lU$AWi%V|il1DDs5Ok^9o*`B^1D@M`K;*}LxkTtTbu^8xtC0?<|feg2_`
z=929dTNG(5>hgBPWqe88uJuPb{O2{z$>u^+%T3nVprxy_sRR*>C{Qj5$JFB#IMJo@30;hZ@--MCCik*ymfsgW~IY>OuJ!Nmi
zn*bVZg*h|xo{WM3!d3>gQ1swe%AqbxN8uTlv+!DIrlrT$hN|fY35d!>5j+n5J>M5e
z8RBFp0MES_^GZJVGBKzKt~EXmgodA#Lq$;p4cS#VSLQR~Y(<~wUGYYbGRv8_tuSMI_
zE`G3=1JGapKlRY4y7;v5c@nl;D@qO2P;Hpfax$i=IuVUbZj45TKgkVwnA=|9-L
zs+2(1vp(+M|Jzo2iDr}>3I%shzZ(6`q!>r@xtZ-?iQ?!g?HLkL-AmUcZWw!y-b8ev
zTsmR$?0^|eUhnO;@DYgTK}_h;NaU%^i>HpW+-f{`cC%(uCL%iij-r<3!_z`l7oTOk
z^V!$#oM1OkNc~*%2xBJeEvw{E-j^>!F{SPgg6<>_lyGeYBjGM;)|vYqsD3SEXKQ-9
zn>iyVRy*WF>m!aGK|`~{gych*`(Ilr&*hpQAN}^#
zpl=Y7mLIa%is!4g)4fSodjsO~>!aD4lJlOl?6VvfppWkMTy(qsAQ?BC?6SA3xrF
zePg1~S8r+?UDGzP6^wdzEu&Cj+-G`!-RHx`$)jZn4>02S|#AFS>!;=cigh&JW!YER~tbqg3;B12j$4)ASp1*2x
zq%%foo%oHEeA(AbPgZ0|NHHuc-sf*TRp1Z`VF?Om%xOxfGjo^LNoMYfu~>q1}r>08{;WBdmg4C?TMx|jwpwf>A}xM2-oyGBmz<3_Ag
z_HbqizhNh+{bCLcN2Uo5z(SwG)2SFKiq;#a2I5
zmv~ptA9SfTpDQPearYI?xFVqWlQhv00yEL)NfWuEjOk)J)f%S-AfL~?0fMTA{w)Bz
z3(C}@{!K=mr4)|)|6=w@QlTu2eKv*$-30xHnB5q8chw5;FzX0M;zMhIE{X$=hd*Rt
z{EXH6Smin%e@0}}PpCkSmh}Ud#kry$&)3eBh;rGH7`;Mv)9Zr&A0Zp7
z>@lTp3S*1(6Ur#$nB2eu6>bz2;nik!_V>GH;yrnT
zb@v$ieAZ5g-R7eEN0%#8Z2&ekkPoqmRjgmc*h7
zh-~Bq!op8RR{*unj{4sp7tb+zRkE)=HXjl=ADYQHfeaqlv6}T|1TV>YHhX&Y72Hpy
zfxqwRK#`gY+#Cz^Qz+)xffM^7+~1yv6m+9Owr*@+v~?qYZ>wyTu^_!h5TK1yB(WQIQZPA
z+wL`9TqE~33G4JRQv5^vMDXb=Mr`UAj&WZ3xS!wY8?=XI;98o=$eDV)%Q5`>`n$d>
ze--TdkiOeU&y@^qywyxu%Mq-RMM6(P+dSv}W7f!%=ee#5Xx)pmzdZQx|NTRuHtVI+
zhbb%64CtoOyI*HFr_dMf?G0Xjx_jIruoM_oDR`s1fKmurO{`|~u3~h4U&4Vk_?plA
zh{jZk8OF|VTn2=Y3Z7|q`-oF{aL4@K3DzPE*)LR1DhLcHsCue_a7P#)q)A
zcfe(RrNKNEf474oVgGkF^TpiAV|fdB&W**`3zoo|>>?h`Rn-%2Pcyp>j(2PXmihe3
zMJB1;2uSH2nETcCL`~RBjbbEobf~^L$ca19*65)miU-ZBvwvMO1m+wS6>taatKrn>
z1IK=Yy^|<9nM-+}ppatizj1~M`u7GV1P0nRscV&`ARYF`zCWp)_ePd}X?62(jaakh
zH+=Q#-4G~KA)5e=;VIl}@q}UvBFvmBQrJKA2xnp15z@Y(9wl_IXR5X&CNAke9OeIZ
zwhH%K>+gw_23pA81(@*zJmm_rRY@Fh>i9eBRmX#9VWqL&uPV&~T*}_zT!N9DT6{F|K`p@^v@*(UEWxwQz9hTl0h7!e>;(KDWU>lDuyheGO#7|t$
z$$QND+Dr1;Y2o?L+zF{3(&-B3it!_ftKnBzM&pN45{sfD?_hRvAwp4znyg|7w1t1~El27Cy=TxaAqH+1XCels8G_CuOTE~K{rBSysm+P;v7e8Mq^Jv{0xGW&~
z=RUI2TEy>c^+u8Cdsx-9=||$)U|aY~p%ng$*Dc?3YLAaco_vz~-pEq_zEyR8e2s(g
zDeto@>2)JS39IW~6>qfjA^uZipfeWru2zU&*OGYt)8+lYPrTK!@E9uJqTXSVt28-T
zCrYlSO0(ol9I>d3Ic2*#)_GdL#X>^=>sA=I@QbV~Z|qZF2Z^ak`<`r$byj;)sT1lW
z>ij(E72--i+iftv?alN`aFL$vTuiLb4;2=KB(*h%n?Bwy?RU4x&v
zU}qj%V1qd(6eZ`vGFoJLr#MC~M;5DiQj?gF{Oq9>@=@VCqr2HWUgz`IKFodgxKNtN
zH*S7Csn57vPDn>|AcUL6D$@(&ab_e1{pPI8+K^l~#CAXksqlX`5J;6<{6L{@DwgKWaW9Telh(V_X?Da(OC^
zP0Dy`;_dEJ?(jh?GbF~Ul`v~z}LNV#W9AdfXEDaD@dZh?<3!8_(n
z%q8LBCh6N%auL6HuKhP?p>?kU@{Ht1(Nxr0}oWfKhZROZfvPeyjM++bAEaw_=cZQNsNvCOZ{I#
zY;Hf~MtaJwiOij5|5^nO^_x=#SO&4!9zBR5glDa3iAWI+M6KL@XWaub;=cN=E&@qF
zEXx7$IMKmgeXSw!spi_%(Ab43iL@M+R+FbWfP)HQta-L(dhOIiZMpRXz;
z+#7soJkTmX8@O18qBzzM{Cagyt^(4^obs#!DH0iOsy0zPJ!svMw`H&b-ZGP(zj5cI
zQcdi0M;2_QX81f)n=cB4R-a7>e$4u*{C&PoYLj8EM&se$suHitRz(|knL4M)Xo*D2
zUY}A>vcx=sBeS|)!0CsauoX(0*koebzNya)l>dm_{{=VM0`{Y)_df7n8k(I5tt*!e
z6ngvpY1)FAIdN-pn7BFK-#=UN?P!WgwmUa7Ia#jKglyZM6xUxNr%+rc$MrH5{i&VN
z{C9<{D{8EKXS}UuQSi~ct^x-tHwpOGBCYk8-c><9|H-UEyDNN_-L~?-=#PbqFdsBU
z3>ss!ZJQHlQhEGCam-~wD~tg*7beu(=XqP}^RO#NrfkkDx*a?W@F(5sUWx2)-
zqJ8Ym=^j6&s{msW%V>^SOe^q%qP3c&UY3;Q4{tUjsbQg>G1Zv
z?Vg`y-sGGFw)0$h_inxZ&FuJU{r6T}6Lsa>t(tv$`G4`XZLJOF!WZAOvNw5;nHSib
zyq-H;%Z(KR_`dx6`L-*j#zA*u9{WopKWls9Cr-JrR1CuRykbd-yw(}I{U`xuMDWSKMcP=nque)RFsRP(F0aXtgseC^U)nSu
zCKzB-vL&*1HN*{N)0d%ua$NWwiS04*3%U4KhT}!a@w`mdiW9qSDArQMsc=uR@Co;tpTcCs;-MC|=W7XV-Rrx0xwE9XMN7#5?G-ioJ^
zbZ$%X9V(;@b+u`_Xe)e2cHi9Gt9euwSMT;S`_o2Bo2B*2!b^@%N(#9rTBdPz?o&CG36!p~#n~bOA)x7Z@m_c)+JF=a6Cl
zO_FQpd@o${#>-_fQExN5wOKS8#>7lGU#cu*yQ8*OZtAb>J@Zj&DH3987rSIa6A~v#
z{GVmhf4ww!fzK+ix@Iz+eOh28)Bo>n<|^WYkCUZ`->==dHanqv?A8q@5x&Liix>+!#kGdJTJ)$HSwda0!=D5zBYX_1r^a
zS$a)>M^?bW6Pcd36m4teBqLLgfk-KZS7KW1hNgvHgc}8mEVh);4lm1tZmE1B%<;iI
zq06Bl2`!1I5}cNVyn)2%98HU$g%cv+ax=wD9rwIzi(}d9KqcrEq>~N>S#w@29c!ktvW24h3JW(Sa->a}VBL#_ZhxVqe
zUF)Y!z+Wg#^^BL`Ubwd1r!@8|LDzh?>e8kHdfVg6Zzuf{31yMW6xb8(=KSR|<&t{4
z=1E!mfVNOSj=iqPv?cJ*6EeP%q+0!~O<(RwR@u#&x=p)!n|GK#dpMA*6scJ6hQ<^m
z0`mq(hHZEoQ?K3ZGJWAO@=f6R8`!6pZ~g?E4CHD8Y9PD*`aW)Ioa@r9*4yC6
zd3VoLUb5I-v3(z4eDca&ftP9tm2nPcTj1l9#SfoZhiT1Dblb{)I9VrYG+&(QX6tLz
z9a2F^As)t|w~Xgl@*20GHvoshz&df+$#23dp;G3hiZ;e)97664iUe+$a3db>GhH7O
z)ZhXy&ZTgl9(fcq>Q30WB%E*Qx0H+X_ApGipbKo}yeRR-5qM+5V2`kR{Lf7Rff|7R
zyZsZg$vvSjY!@6P&A$a1a>Ok0p(wFVpAUjLwSsp0_ha9)=k^t|CF7&Lllx=bbiTr{
z-nA;@V-**rVvysMeLe5sTkluWs{OVe$gg6lR#Pe@w^A~8IGM}ka~B~$E7o1-yYeQl
zKL2);m*uu%y$kM3sckWS^1Ape;e_jQ!fn^VB>Cxa{PZGbe|ET5u%X;()W$wIBWxTU
zFs^b3XHFj1|LQ5Fg!!1|;}Y$wQ*YW+Mprd=roeJNT40C6gWLLvB5vV7nwymZXOPn*
zCl}0R!u@MJDiKOvYXhHO`(cHHQ$@Q**HrUQJg*K88@dts7T)|z1vFHKE6(|0$?P3V
z_+LDV$W0!-_29vq5@&sk=BHU5yb1rG5DM#FoyvsU3Hg|VG2PGRGft#|(w>`=l~+NwC_NI<4rh!PY!)LBEQcD=GfNFu5
zq%*~DBXu#VX%`uq>_5{!>ZB|Qnrd@&SugsZ?i#dpt+yro4@!s*}wtDYh#
zp<)fnaElW0AMvjKS!EmRI;P|eK8vg^%Jxokn#!Ig%E>k_mm@dcB2_T8U;@WD=^HES
z?;$%rB)P%jU^}?XVhTF_<>K4cu1-5gNE+zo&GhEC!rhks;dNz!r59Zf<;A9d@M$)Z
z)M9*G*oBP(vX6hP4?6Jm9bVF$$>83zDhSH7ib}c0VWh+vMWxKZC_sMU$#ddz)_;&TN?QI@!I{z;2j^m@Heb<4aKRyKFk>r+esrIo-n+^)Cn7RLg8*SVy
z(VgX$wp;_>D0q4}aI?-g|J6#e@|(_Upq61{eXxyGpj{JdPy>21_m9KaUhG!xE|Prh
zkgpd`!VKeWhvQDCy_E`)cv>+)BgLO#>_3@~<`8p!B}`>0t;e#+yU~bum%B%v$+j4M
z2Tozv^;L+`C2MB$q*>oAqXgHX8UeNOKay9oS~A)IpwA1ST9ph;jVq2Dw8qrt2i!jT
zh)l(%-BB%bt#31_
zSF1C$upkt#*e1EwWvb2vSxNjE4y&8Rn|5k3#91xR!REx;ba@
zR^VC0Zho}#!_%k(&oe0d=XEs(St%z&GzU4#^$PcrhP91G*YlpovkMyoLR|81bsPLx
z3vuYoQufPv|J3qw!Y9S`;{uLO=Cff*caqhZEdG&+roe{-RS2#Spns=kf9x_n=~#lf
zOEu*)>Xh+k-6Q-j*tX}ME4r<;C)~`=;#2VakW&x+O^qgbYy9u&&N};*7e3o-0XMC-
zzeDyU$TKbeWk(ZPV>?PN2g+zD#ect)ZQtnTXc
z&OI^TOa6{papfAGT_EId|Ghol*m!Lg&n~PJjOVgs_DtKG<>;WW
z{$gg+gs9yV;K&>!qlwgb!h&?`#Kh<9HgQdxd^lx)H>_@Vv4a|W3MAS7NpO|R8yP@!
zl&(CFsvY<@AAs)zjaSOYzU#VvrZiV0)~9~Py+HQsZO^dgjc%!s*ROIq8erSavp~kn
zaVsI)_1m@M+BTPo(nxn*9g
zv&r3>m0{n))v!+aFzF~~*$N9+WUnv&cNQ?q*1ojYd-rG3brOhBM{VWpx>Z+E|AIlM
z1+F#C_`I_0!v={JYw~ip9Ceq(6kfnj9sj^vm*D=5|AIWmO|70;d^H(`b43$mNq$R$
z&?Y53sw466uj+wSP}iT@D~Fg(#$La?DDWVcwaTlUU;%Az(@&ruv;s%F23|PBx(v7c
zc{5dwR$v;+j275@DBn!SFh~yn^$A+HkA)L)5Ip1KJq4|I5nU>tmm6tdx~rBq)(=y0
zxSBTZ6=V`v;Cc4JsNz`XiN}-v>&s@-;lQA^?|~0S;rE$8DZ4f`UW%p%xJLNDbh+cV
z7!Y3}w`k&WsXybesIBwvs|8q)Oz7<&_$Ih8+1{nB@%5DF3;?mMK>nfrEB$c2fKJDc
zm8L`9`HjSfH?LWL8U$UO0zE0uj?Kl7$y9^yU67
z1pPSv>K!OunSnzUsecdf-qDgdDkEj8sXjr2IM-$uCYU6-z?a?A%olF5+?0CIUrU)X~~
z^PZN8CJK9b%d#j(SBjk
zbvwPj0mUk8a$)-z)-bRQ9IY1e;e{Y(bnv@f+TEXwPhF_t^
zg=IHN-MDe|dud~86GM!y=xPDZ^?uAw28NlLdX=9BUaH+(-U#>ZtsS?G{_(WSz?k&+S?qIpZ6x
zd?zO}kD{0hngk!wCy8C2LC{8=965`Ro*rKmtNyji*8b)Nuv*P2+lIP-;nm*{GLh~6
zZ4*bGxv`CE&Y;bL4xyQ=D&w;ix6)G~{w8Bgg9O`z(A|vv@GjTXOkWQMIUO=JZ9H1v
zK+$5t2`~Rw-=Cq_PQfADM+@k1fUhi)P}RIpr87g}&6no>=mONN&hE**E<+qS
zmK2G8^8um7ql}3_Vthwa-!;oE@xwKhToDos-ai$#Om6Jz&sjhHP*8HcS;?<{;w?4=BZf;7hm1hfa1@
z>4xX+L>)D6Mfplw?x>YP5rPA!BsTlqUdS;B5tolAhTjdI5`K5|EM4L{eA9UFXRi=7
z&cE?Xpc8b(@FQ&xvsJnMoeXq$GV$6yIh@R^H+ftnuk(v*=b=sFAD!+julr`_H^f{V
z61Qif+ja5a4Y}Io)rua_1Zc$~@lMy`xD^-@eqDC}R%Hq(KoxROS9U|7HN
zoLJ1QpHMbGL+He*;ga$lXK4E*ldy2#{G44^&F{tUh_c?vOsD+0Bk$3D-mJ@B;MmU3
z6Du;5J{mq)Jmzdi=bx`XW?xKZ%6>Qft^Vb$@SVq7C~XTf-b=xn@Mr6&&n22#ya65t
z-%cJq4&^s*3)N_OP_8Q5e}dHD=0&>ys+@=9Fxvd0i5=S^j$A~}AIOPNP>D*v;V
zl`!s^d!89@Hp<>xQp%M6G}SvlsTvuH>JVX+G~?g1tGsCTahdU%a@`!e5BTK2qO!Z)
zy!cm%$V!gX6`^m)Ggh}7H~SpFmf~CPj#+uF+hQ%Ev|DF-)!bPvUIvGEFf?MkLcIUn
z-IBMXV`tnqZ;oQduR_#Dp~%sc?U2P-Psl_b6+oUUH+3#Y?|zpSb1D_Mf8MBawNd8v
zp0(TP==g(ZewJ4k>n9zh@aH1g_XVM-6>?h
zCR@+1*lDiKgO7H<{FNWW!nW6QgDQlFXX(2k)G;iTDIBy#BNp^yK*a);ucy>@nl>2;
zx2p)Qj~@_7y!6D|yF|t(uPEM|K77_*kgqoHa*V!rNP)7R_}4*
z>yMR2$1!7kqoc<9$o+S%*Kf!DiGm^weD9vAxb%VR#bg_0le9N&lNEh{z4QX!kqFk+
zU=0CqbCqrqJLPI#8+>B@#U37JiV3~-N`s`c`u3vjb}G#K4m)L}7Pzq8WN6{LbS^2{afQNoNnTOg4<2|bs&LmFa2d{p@SaTtT&Y@
z_KC|KWD{fn_E1(=Mqxv!O%RPXrk!h(i#5W%SLW0+rJ|(|nl-)aIlo?kUd(
zv|;@%e)QwK_g1rw@FI*upFuSTld2ID>Z@6)-nw^JAiLpU#cS2(FXdd19@LMfScLVa
zKmFRZqpD2UUFzsO{Eur3v)TQ=(?vl^PLb4
zZ{U@#TKncp&>^2h6YZu~d85w{8+@H|
zt~@>#y!SI)cspva*BwlCxR8%=FUl$>DgdprYD%tuKX>}tXTx2GyHzsP6^+75%vZcs
zf&9M!7D4I08)VxB@ID~mUc>_)z}S4`kw>U%wMa3TF0h3sI971JHD3|!91B>8)D`vW
zX0Z|B*)gKVZIPtK=FnSgHi<=x7P)q|y+>1qbm(BF^!YI{8BS=Dm;H%6^&A7TBVj#J
zIXGb(>`AguL0<+*%X&Q8QZ9fF$IwtJ{x#XZga<9j1b^izm;H@AJgDPG9)Lf`g0L@9
z{?vu_Asu87@yP>WUsEL|_$%TiAXSY7v=Lf@t79NaX;LC(QXYz=UhSzPuVb~1qsxhe
zj_@s;#a~8B(TL*@PRL(*@rNc5nq^8H4h-P!W$+opNtaVcmSSII8B1GqY~vP98SbE6EW9~q
zy!-2n=UjQGcHRbz4l$#81FDD{TOYQ?^oD!%)%*^&Y4Lws^+vpcHpi0WrKCL=(E^N2h
zjF^ND77Xgu%ALMvypdHnNV`2yLrFXu3Op&TpgpTWNqscxbn=cs#*1OyiA8iLwdx1tQ8d%tA6L|
zsRyiZ#1bg2imF8)Of1z0Fd>6C1>Ob=7A`Ca3$2W2f&eeB5SVC`
zQEYIGw`)!HAuT?>zp#D(rr5`{CNRVLn(~D4#1pbq{jP~0AUCv`6x-L}S
zV*46*Zt}^yY+34FVHG>ZoqWIq3-s}l!YeR3L6fg-zB=ekpFYFiPnwXxgnxDR=rasKOaAJ(>gvFEuieWT3_FT9v(O6ce{*IYAmOa>3X%Pze*
zGbt~fW+4R!#g1EQPe^R?H36R9T;muAF23-5_w(b9&D*3<{5WDYjg4__YEu?IOYk<#
z2O~$O77gH`PM@RCDLga}`tgCD1fEu7(hCmq(JaM%$Tt-CO1@_T#$Uph0=;_mbo-bg
zH3YsX4*v0veG#%hV-6J|6x$wJ|9bMN3`xens1f>z!w>Tdtw4Hq_y})2$uzJ`vF$@z
z=t|EE7W&o|2)m2{xTb4I^z*%23#Tq=ZJ)1<(Y(X*u96R!gY-W?A({^}Rfj&Ijdx})
zgIY+%&vAwYdGgTaIe^Th`L6RkWE!k$>eP?iKmYkJZ)9b^=2K5O*=;s-Xl6V|5c=`(
zBagc27Fw5a^ccGzI$LCeRUH^lnTL4gl~>%0FTUsvs4|GM#ZmOUbIrW<)?1n94r2n(
z!}hk|65v{5izN19jRJeX3Rr9|p3Dc=<~gRe4Vk8Of&B@vN&O6vXS!b>Ke8u*OIgYk
zV3~AYc%p$tfFH+7u|I|OGds*2N9j?Qi@)q;VVjUYJSDH_kVfralt~`ZQopIAjCw%y
zLVUFe@uK~wE&Z=Ipi}h?p;FWt6ru|O1xN`x+0^kBO}S*Gj$`PF4tbqW%ldlSGUG0H
zr;tB1U%|=Z?r@YPW~8*R0pJ1h50j0U2App_nrJk>D-rKYEd(QgWwZjSr
z?N;44p=F)nl`rjsx`UBrBFT)T=&G6briFD{F1%Vzwv2dojJef&z6!^hu1tqJZecPu
z>)71A`sF)r>otp$ug)E7z=o_^S{O_yqszK{j5najjn0aYxpa$8B07=wFfMF#hz`()^i^H+AXY1-%mNZ
z`SpSoZnk;2F4xGM18?`iZQYNyu!SXQSZ1NVul@I2_x|TqhG5kdl5RDiwQJL=nd{TF
zrF+A|9)F%A1aWVx-?D#eKU899eSUoY52Qk5Xlz_U#V{eM4=0{|gqrDX`#dF(UjrB<
zw%B3|H+uBwjMwB;o22JO9&g|T8czdE2;E^5&icSak}LjjRc6mF!Uf|^z{lW0ho)Ao
zvtqrFiD@Qxn81|xka|1VKJ1VE=}+7SIj#Y}Kax#i587~pY7>Q`p_TEhB#yq1zV}|R
zKWohXt-0!NzV$ZuZ=1X$Oya$F-Qk|FiHOJl`Zu@Gp63Ggu08J9pE>sD41r0kqkr-<
zUv$dJzwk2s9QIC&N__SaC%I6O|
z^bmK9c?-pX_UWUJ$?r|mTUju{`>2Hx#ZyZmzQCa$$a&hSr}&8y%7Eie_=OMqsB@1|
zY`+6ildruk4A!kT-TsxiRMwX#IY#jzPs8-gKddH`3U0mq4j(#|`|($2oL=K(zS=2eti1E?d%PE{-U(Suw%abdxZ{sM
z)*B#&8*6MlZYV}JD!=9~9Az`m6jTjQYnTHP|m^XAXXQEVPp4Z{4-BUvus}z^bJEX2sUV%=x&D;xJ531Tk3RZ1tG3wo5ED%zkKm;l1+KG0
z4>{OhlZ=a>TIkgQ{rhLoifu1KT<`3MiSby#b^NoR9OIuCM;vvGFUF&GzkT=d`RIGj
zT4oG-=;25G!YIAF@XX=9*=ffeM7CO*@7=l@asdUop0AMLo#HOW)wf1vEkeSZ{)hG*
zLWBjq=l|yae&@cng@hcpXwlrw{%W>6_4G6R^}<+n*6+^Dl8SqO_;b(uF#tUn*sivr@bLxzg9x6sSA%Arid_c;V!Z{WV)$17L37Akjk`fM)1vXH6BPQka*wp6qx!XR87O%jH`uaWBrd^v9Yr8V!uL>WZM-2Oi
z%2Fbv_{3hz&@!M
zTGx++4Thdzw~gCo45^es=j_0c+Ou;DciEv`Tx&C00(gpIn0)cQCH^@2hdo)Zd3vt<
z=*#f^B8rtdhR#oROc{nLSz(JJZW#Wp8Lf*mvO;T#dBtLAMHO4E*T%j6{t`EPUS`k&
z#T%KoFi+N0&z$W+tAWW^uhM_wjI4tP54MS?o~v}f8d7-n$lTIG4vw;w>RN2_u^G{L
znP)$^1R6&JeDuY=$Ei#og&arAY9sNC88h9v=UtFxq*S}{<0rWDFSyA4>FPgL+dq{L
zSA~besQIU>uTry2ig&0c)mV)k1;Q8tc-=5z7KL2(D{MszeO+OOOTunqxQxOiTa|pF
zh2FdFnrr+dwCYy|dV2fqcWkoet&HA;LyA!p9`cT)3>on>VZ!E>S6|I(Xnpmy*L+(h
zJ~mDpkeQ%5^Y>@_5RT9afyr6IB{Jd8o}%5lr6yRJ6wo;pzK%l=XX@&D9z{2*Ym8D2
z*;nMK?YRLrDlcWrmgmuzozD;yt~D$p&;7)N^ZOr6ao5^49i3#3;)lnyWf27TO$eMb
zXtI|kixP4{UC*KJhov?#^oKuQ?f3nR;}Ko7!Gsj!JJ;sevG2Om&N#zec;0z#$dKxb
zEaUVY$D=l7#oR~G&n1iW!2V=c|LNLlAxL!|n54b+rW>p6*EMF$J6?af$J7_Rm9D?x
z#*Fv9%4?GjTz`GXFCWM|3>=LY!pDGi=WVy@Fg8U##tI`u=a%?|=_p(9^~$TS`67%ZTrb=^wFRC{
zzd7@F83Vi8F{Tr0ceYKo<2@N?AOg28?Tb0j;r;OHYp>@tv{HxuFoF%)WD~E$#dhxk
zy?gccX|6v+dk{>T{C<|9wb*fs_r;4Zz1(|%iw7xV3(qyiQpP=G=NyD^>M19=z4q9n
z)<%v(@pZlC8ynd(895mTxfkP%TZCy<^a=1oxcQdb+_NJ_ghf7&(UN^i8Luul@0_gr
z3!@)KZ*cGmTyMaDYVCPu2%`1sS6%Ky(Nv0;b5wp7t)Yu^&i~x~@efyKEdUFRA5jl`
z(ZrjKdjcAte)g$~eOhdLuA|Rvu>ingz+48h@Hs|Q0~uP2ZSNV|AI=YZ3rB(Lg#BL+
znsH!eybG`U@IB`}8-uy_qF!^1$?Uznc*$aae?)oI^llx+FXTAa^A(xSv+n`kQw4g5
zz({)cz4zHOZCct=r?s>P2j{htIVKD|{a&w!=AO)ZI+}X3g@}B#P
zEDFqKn+?sP)za`npiPQT_WTCVH|{m)wrJkMUo+q#2gYFJs;@{vp?rnpUwrW;+i$nh
zj~lz$zU)!pnv#*9Zw)+IyO_anbpbuIScrnhDaKIdDdL{noLd}c0Ol(~BP(UR$8Wmn
zrha~dbB6a>lO3Kcf~`@NBM&TD6NS;afMJ9eDOr%;7rM?nGjsrJoUw{n#qeVnQ;;_vdWr<$e3
zUpZ#G_S-0$@xl>)s?k&@5V#0(#
zz!*+b9;>j+NJYj9Qbt#>4D65DdT8NA!>g6@GTW{C9qqx9Vr#tZQVbi|34XrmnXRCEGJK5t7H?ux}kB_OXVs^-Y_c)x_;ITfNRlPE+5n
zBzLb??V7#z+|%z*_sR56+@+Ua={s|xc}Q$&9>_pAdF~4e_`}Nj3op6U8(H~y#Y=OT
zO=R!^M+izh{+MtB=ej>#o#mA=>g~5}Vlp*`VAN!#crj13<(>vB@dd@4N70DWbwl=5awx6o
z+{DR?@oc#n;cvM4W^Zg{)jJ-=K+Bd@pGXfp^swI(lX51o_uhL?xACBjZ1VOqM@UC+
zjIoKE3og3EPcoO6SG|wWCKs?ToaACscb|Rs@^qP){I5-#Ve|?o&qF$;IEPHW;<1Wh
zY^R-ea{Vg$W>_$hi`P2egm`-V`j@BMepMTKBimb}M!Q>XyWQW<4?g^Gtf5u?%5|@1
z7}YXU*J}&%HOazWr%YZGYIo1wclQe|2#3k}!OQuJFJ`%?Y|k@==7c7mqZp~t4`UJD
zmRs7yTRS`VjD`O+Z@e(vByEZXcyZtV`7bwkQe2DdMOrA}B`*jUvLg`-5-5M9Ou841N#X({eQ
z_~0dc!2bLBF<{o0v)#S-VKkfM7iq9BZg{WYJqNUH+s1p*NtS5Zt=n3@h-(j{kPL3c
zwkN!?zE8TR7o|mca~vAZW(46vi){~W!pier2DGwyOgzzvIDk%AwDiQko^M64?f6$
z7fycv18?w~WQ$?mw&w`Xn!y`yTC7GNm*?XS-8-xs`h3pkg&b1{}+
zWF?{uQ4|39jkASoODmVUH_d3zI}6S<+-tnwu_)%Pw?=tf>SSPR6L^VZWS=$bOHZ4~
z16(s0%`jr}zRtT5<7=6ZZE9_&}_333AvTkDmq=#q#mH9MX?kCWFL8_cya!8t)T(<)6
znrUgvR&Ir@;4KzbEHL@jCfo~*0zl4C?)20I
zKL%GBS_he-mFqn8XeFdC##2F;_8R87Usjp{x4NN|P{Sdt*}>l&VUf?{)r$eRHbB_p
z5dQkcLN{_sst;j#UGoc;n8%D6Rx!2`(z&IHyxqXo?iDM;xQgKw11zw}4AieoUhECk
zsghOyFCSj=!lXA$Y%rPJl%Ic1RqK3!Xc7Y%851=@(o|($o#kQzkYDA}s__DYX09-S
zh3Mj;had6#n$qT%r=99{4?>Z%ugy24w6uMQ6nof
zWpKm;r(Z<{MHx`oVG2UyfDme`7akLnmt1&3#zO~>E{xFJ`-EC#BH|efVTTbp3apgA
z^x}(rc)w^}uH#*I+1cIy;6r{=2%}j=-@aL>ubF{I#^oObtI!EuhxY{`1b=o5>092`V7QP{>N?*NReap%35^9bEsx^Bq6B1Z`M&P^_Py{ak1x6L@_S?{>=ZYHfFzLVbd^T0fYmWClWd!q#={K
zua6w*@0-Po7u&tvRwQ#?9~p!?Wa@ftLu6Pa>|=P&F>(+_^Q?2u^?Hi(D&+WP3wzF3fQKCmFSJ+%?<+znGErX$FsV-%
zbpT_@R<=+|z+^Nb5xM5a+1_NKp>>Q+hy&bbOf-+S>+%qrI2ULf;`u*hlOZb3N{bnL
zvj_zT58J(oAq4p4X{TijiUCTkvKXh%IqUbCcR)OYx7~Vc^VcGzxvZ|oUuiz=eyA7kUIc20oJ
z?Y&2f+qkbDw09_g`|OI#F3Hq!y=}kUw!ZKGdEvj_U^#Bw_^ff4(EltdU{TSPSN+k`
z!Dy%VZ{EB2-Dhw2lcSIJb-Df&dmpke=c4n^%iL?JvGPK9+|N(&?<7$pK87oxTM*hf
zPPQKD(5>i?>kOR$MYm5IdZDFfKKUqMG-K-r#@Nt{R)${i>(ZWfk3Igk%s1z0wr^(m
z?#$u`AKuy`nCO{Hn>fJWc=1ISWJNvT`7`g^c@{?ZIlrIx8*}8|&Liy`6lbybxoVItcsQvhr7C$Y0Tt)()o?+Gw-z+T7@5n
zvx=29GkG=huarqkepoA*03{C|DaYioFL5K#CUrxk%G8$0P0B?_78>!eDo=-$GW|G)
zKK3`t#NV>9{Hd25!iA^!Lkr&G8}hMY&r4;(p$!wp9E-kXGkqbia#?gJQy--#Qt_w0
zE-uRXfh%Q;zh?7QZz$FH
ztDX2NErdV(z=x0eX4y=h@=zC&OJ$OqHsY_8vK2g7nlku@85%$h(gv16^8QEO>ewUI
z1BC{(0T1J*|LNFNhNaQUntLRW>keK%&k}~7X^I$@3(Db5IpQHtb9noTRDIf*>2bmH
zvZYBh4^Mfjtl+;!()+L)UB42{(?^Ds!POg6kr9z1{C$yCU>o*%li#ui=^9*JzX$NZ
z0}r?-pL{a&d&2fZ7@2;d`yO<^pe|yVi~~w@RK=m!ScV}m^b%dqLIH1t5!K&s_9kHa
znodlI+r`i-Xy2x}+sMKP_v%u0Z-w5hgw_rBll^9ag@t4kjlgH$@QA2_aKG28Qs?H|
z-mc3TrRxBLdZmoQb!eKi346`HYKB#Xb#7&r)$Iqi@jnc&00wbz7S*ulYzlkT`AbL`
zjI9Dbsdt2CmS^DjdcM_8lx12o;Gz3~w@UgpACuW9pLk-m=9>@O%$LbQm%m(TrfcdD8%R39-;84vHCj
zJ_S**VYASSW7ERs-fBWlSWnJ^sVIVu@q$(XL!hqT-Ew(*$3O&zEnrrcc440CJ
zRAoJSbk7Rq%wB|oORu=HTG(*LyR*+ZPbfYO!<6c}r=l+7R`_0U`e~nLs^$N8SGdWV=dZ+_PPtkCD$XW!^cZQ)v+*SXrp$3e?ZnLcmV(nqB1U!+WKGG$90_@tC;a+kcyMTO$T(dRf+xOnMgQ70VApaX~wdGRM7<*&AsljjEwXu*qP>L}wE$KQ%mJZdvIf!tWo
zjIbgW7R{_5)-$Qfq{$d7(<&hG-IY2l1s&@S#+Qth2h|wZi*gJ57%3K-w=?;cFHFgY
zMba~cYMMV~I#a&bj=k(@ImvrNF>T2kGTEgoT(h?3iCQG|Y1`c`vOTF_@}M~Gr(GzSDW$nqFGB{<|$a-{w-g=)b(m>eg7T+d$h9Ixqy{Wo7mnr2~^hr
z22YH4%goRjLceY;ZQoNa?9u`Ist!o+wTc0Ck4>s3dI%T1*bIiiCtodh-z;3=I+v%0
z}$3^>kb>V@#hNfRsnmmVr0epb#(*6+HPeY3~$+fi>yWm2*1Td24RGw6RxXU|4Y%I
zkIcK~0}F>GU@Y9sLScoIC8|r(RbK;4=xMTO!TbeI9!}AoePet30m2RInT%t9);M6&
zUX!?S9;UOYFlu)}e{hjhPw72c>Z^`npDQ0hF9Pnbu%Q}E1SLWC9e
z0Q(@ypb<{UMwv4iz#e0G4=h}`z^AWTh(&;BR3Y!~r8tlIblq5e&1YoECvQ~O(c=$-
z1p}!GyeLM>@XbUi9!rFFt__4nn+;v7PYd#R#tUy;p9S?qvE
z36oHd|MhQvLCua9l5mLaWsZl6-ixvtr4NeHcN{&H)#ci%jV$yt>On7_7zk@p++#p66ifpC_1_QQiPqbw|#F=M8W`oRJZ4D3&t$3OJm9rv#H))Q~Jw~bQZN?@HZiH8zHtiEP*|uZgo@B3SLeAsuo@-qt$4(vnSh8@T&5z}Qg^Q}{JKDG-D7JmLII1QY7A#1~5Jo90
zwmqJYGWZesB^Ts+4+!yd8Pa6@1DAbTL#XN9I>aqBpYQp~LJ;2RS#)snsi)ia1UuUJ
zxrKcLY?yPr4f!*_SR3Fu#eS?ymo4>%&q@m$tasu<7a=ls(w2LN{fwbaUiXqOw`*JU
zml=+XcD0eUzHoGXu{f+0z1$RKdf2Y8dodYGnXD5`mg>e!O_WyI
zj=&dSXHq?F)K2s{hNftVhw9-k8k7l-b^=YVikA3uEPAvH+lZFhh?el-NgMT>6x>|=
zMW2+m0QjP>dS8+L11|vimG=e3{y}M_1Uj!yMHQe9l1i!SkWLJ;kf$v;QmRg@%GF-S
zq|ntx$T4jJ%JqXbdFYWBFX5BwC;lNmb(B*U;)yPIDHj!W;%`}xPYNCY4f5(A_&OJq
z^HZP2A6&|5D`@h2w6^G5VY7EOv5TPh1FcbRF8J?g$L3YqV?b=9+ObgwP|F@@RdC
zTS$KDtYxl$_o|n*gSRYqlPyd!A(=}F-z>BcfbUnj?akOKPgab~gcio@b#(=pWH42<58q)ti`+9q&!Tz!Ro&%$Rq)p_NdIT=T%Nv`1`|cClk`lpf(#bv+*Y
zv!B*@zeU@J$8p!N>Un-~FVMeS3vh~U53jnMXS|vTIgG(H3?KZ4h3r(=;N5oJMP13H
zhnrV2^$*#8p#TPaegeWEJ{jmX5f
zx!W!~dmV=1gSl_m?->a9#^pGCmello0AIkly6Do&{58nEd7NGEoSzWbvzu_jcrNme
zL3E5bPy15bhl>0W@+aTQz60W*SI=I4u?AsW^8q1Y1>rnPvF$NR3udLmjO#c|F`BUW
z4G7zW`MR`cp^Bha&z{OwOXC*4M3Hjp-W(`$K~3-0x!TpHJm2$`FttR(AY47~)6dw#
zAbwoK8{3|&yYIG}50{1O#L1Ba>hi78!XgTi;$hA<5x&gw;4HIi#;nFsG7WyLkkk3zQ4103<(FS^|FiE8#+h6T
zGYX;C5V(vPMA_n7X{LqG<_B}X}
znQ{Jq|NEa0D;(_`v_oFe`o=m=e>XFs$t?bN>0f9M(o8>t3HB$ZZoySK$7)ZCZHW{b
z0J!ACb}A>8y^Os0)1Dv4q_l;N2J|Jb%EeR1q~b55uKH$G
z9zys}JCZ{3(y)4?RHm@CJ}A4&3CHWfQnLJTxs+x|!K0i)88UrY8p-FI8O=)9!d5313$42i
zb_*BVLsuYPl7Vva$dVQzU65)aFJ0(A0kx6ll&W!*MP;S}+A*cuzUrMCCPN;3lU
zQ1M}a;bTI1ag4u2UFl^=JUl~~K1ai5s&v22
z+J)6Vzu(a8GUyZwqd%&2m;U1$7t(5OW8P_dcJ%wt7E3?ceva);`?`6yvZpQ{ta!4P
z%3vJj)s&8zG~CkmcnMeRGvW01+izzks+y9#O+gk`&PR=`n{U2(tqp2Tp$~}+g=-*c
z=p#g3+z-llHc(dxj8BK4=AH~g=t6@@1clujY!ft5sHr}R-_XY_>ezm}?L1qB3g$qb
zFPoYdebg)MfrlP;mtKCQHzuHaKK2O%iEc24)D?<7k2UGKDfJZ{)g*6S_1IADc<+uv
zvF9*KFV`{q&)$329e!dTk2lG}