From 25fe94ab92c4f57a3aa76d38809ad8a662505a41 Mon Sep 17 00:00:00 2001
From: "github-actions[bot]"
<41898282+github-actions[bot]@users.noreply.github.com>
Date: Tue, 21 Apr 2026 18:24:50 +0000
Subject: [PATCH 1/7] Q1 2026 development update
Signed-off-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
---
.../active_contributors_per_month.svg | 4 +
.../2026-q1-dev-update/commits_per_month.svg | 4 +
content/blog/2026-q1-dev-update/index.md | 266 ++++++++++++++++++
.../blog/2026-q1-dev-update/prs_per_month.svg | 4 +
4 files changed, 278 insertions(+)
create mode 100644 content/blog/2026-q1-dev-update/active_contributors_per_month.svg
create mode 100644 content/blog/2026-q1-dev-update/commits_per_month.svg
create mode 100644 content/blog/2026-q1-dev-update/index.md
create mode 100644 content/blog/2026-q1-dev-update/prs_per_month.svg
diff --git a/content/blog/2026-q1-dev-update/active_contributors_per_month.svg b/content/blog/2026-q1-dev-update/active_contributors_per_month.svg
new file mode 100644
index 0000000..b0edb01
--- /dev/null
+++ b/content/blog/2026-q1-dev-update/active_contributors_per_month.svg
@@ -0,0 +1,4 @@
+
+
\ No newline at end of file
diff --git a/content/blog/2026-q1-dev-update/commits_per_month.svg b/content/blog/2026-q1-dev-update/commits_per_month.svg
new file mode 100644
index 0000000..b23c4de
--- /dev/null
+++ b/content/blog/2026-q1-dev-update/commits_per_month.svg
@@ -0,0 +1,4 @@
+
+
\ No newline at end of file
diff --git a/content/blog/2026-q1-dev-update/index.md b/content/blog/2026-q1-dev-update/index.md
new file mode 100644
index 0000000..afa264a
--- /dev/null
+++ b/content/blog/2026-q1-dev-update/index.md
@@ -0,0 +1,266 @@
++++
+type = "blog"
+title = 'Q1 2026 Quarterly Development Update'
+date = 2026-04-21
++++
+
+This quarter focused on hardening verification correctness, deepening debugger support, and tightening integration across the TLA+ toolchain. TLC received several critical soundness and liveness fixes, including repairs to FcnLambdaValue handling, ENABLED semantics, bogus safety counterexamples, and truncated trace reads that could previously yield silent wrong results, alongside a new interactive debugger, trace replay, and ARM64-native builds. The VS Code extension, Apalache, TLAPM, and the examples and community modules all advanced in parallel, with integrated formatting, richer trace visualizations, improved JSON-RPC workflows, and an active community exploring liveness, refinement, and real-world modeling patterns.
+
+
+
+## Development Updates
+
+Summaries of merged pull requests (and significant issues or releases) for
+each project this quarter.
+
+
+- TLC: Adds interactive state-space navigation in the debugger, letting users choose specific successor states and backtrack to any earlier state, including initial states, for more controlled exploration of behaviors ([#1270](https://github.com/tlaplus/tlaplus/pull/1270)).
+
+- TLC: Introduces debugger breakpoints on `Init` and `Next` that halt when `Next` is `FALSE` or a breakpoint condition on `Init` holds, making it easier to stop exactly where a behavior becomes stuck or violates an assumption ([#1275](https://github.com/tlaplus/tlaplus/pull/1275)).
+
+- TLC: Adds debug expressions to serialize the current trace in multiple formats and refactors spec-processing so trace dumping and debugging can reuse resolved modules, enabling richer trace tooling without changing normal runtime semantics ([#1274](https://github.com/tlaplus/tlaplus/pull/1274)).
+
+- TLC: Fixes debugger expression evaluation for scoped identifiers and operator arguments so watch expressions and debug console input now respect local scopes and parameters, avoiding incorrect lookups reported in earlier debugger sessions ([#1278](https://github.com/tlaplus/tlaplus/pull/1278), [#1279](https://github.com/tlaplus/tlaplus/pull/1279)).
+
+- TLC: Extends the debugger call stack in BFS mode to expose the full state trace, aligning BFS debugging with simulation mode so users can select arbitrary states in the trace when evaluating watch expressions ([#1280](https://github.com/tlaplus/tlaplus/pull/1280)).
+
+- TLC: Adds ARM64 build targets and release artifacts for macOS and Linux, allowing Apple Silicon and ARM64 Linux users to run TLC and the Toolbox natively instead of relying on x86 emulation ([#1271](https://github.com/tlaplus/tlaplus/pull/1271), [#1281](https://github.com/tlaplus/tlaplus/pull/1281)).
+
+- TLC: Standardizes PlusCal translation-hash mismatch warnings by routing them through SANY’s `Errors` infrastructure, improving consistency of divergence diagnostics and making them easier to consume programmatically ([#1215](https://github.com/tlaplus/tlaplus/pull/1215)).
+
+- TLC: Makes multi-process (MP) output formatting thread-safe by replacing shared `SimpleDateFormat` and `DecimalFormat` instances with safe alternatives, eliminating data races in concurrent TLC output while preserving existing timestamp and number formats ([#1267](https://github.com/tlaplus/tlaplus/pull/1267)).
+
+- TLC: Propagates SANY parse and semantic errors for breakpoint, watch, and debug expressions directly to the debugger frontend, so invalid expressions now surface as clear user-facing diagnostics instead of silent log messages ([#1282](https://github.com/tlaplus/tlaplus/pull/1282)).
+
+- TLC: Adds `-loadTrace` to replay traces previously written with `-dumpTrace`, and later allows `-loadTrace` and `-dumpTrace` to be combined so TLC can act as a one-shot trace post-processing or conversion tool; trace formats now support subsets of variables for more flexible replay workflows ([#1285](https://github.com/tlaplus/tlaplus/pull/1285), [#1289](https://github.com/tlaplus/tlaplus/pull/1289), [#1297](https://github.com/tlaplus/tlaplus/pull/1297)).
+
+- TLC: Adds explicit warnings about debugger limitations when multiple TLC workers are used, clarifying that breakpoints and trace introspection may only apply to a single worker in parallel runs ([#1290](https://github.com/tlaplus/tlaplus/pull/1290)).
+
+- TLC: Fixes XML export for `CASE OTHER` so the generated XML conforms to `sany.xsd`, preventing schema violations when specs use `CASE ... OTHER` constructs ([#1292](https://github.com/tlaplus/tlaplus/pull/1292)).
+
+- TLC: Replaces `System.exit` calls in SANY and the XML exporter with exceptions, allowing these components to be embedded as libraries without terminating the hosting JVM on parse or export errors ([#1300](https://github.com/tlaplus/tlaplus/pull/1300)).
+
+- TLC: Removes the RMI dependency from `FPSet` by dropping `UnicastRemoteObject` inheritance, improving compatibility with CheerpJ and other environments that lack native RMI support while only affecting already-deprecated distributed TLC paths ([#1301](https://github.com/tlaplus/tlaplus/pull/1301)).
+
+- TLC: Fixes multiple soundness and completeness bugs involving `FcnLambdaValue` conversions, including incorrect mutation of `excepts`, crashes, and wrong results when checking liveness or safety, and adds regression tests to guard against future regressions ([#1304](https://github.com/tlaplus/tlaplus/pull/1304), [#1316](https://github.com/tlaplus/tlaplus/pull/1316), [#1322](https://github.com/tlaplus/tlaplus/pull/1322), [#1333](https://github.com/tlaplus/tlaplus/pull/1333)).
+
+- TLC: Fixes handling of part-of-module `.cfg` files on Windows so configuration files that share a base name with their modules no longer cause errors on that platform ([#1317](https://github.com/tlaplus/tlaplus/pull/1317)).
+
+- TLC: Extends the XML exporter and SANY to expose additional semantic information needed by TLAPM, including unencoded decimal values, proof levels, `LOCAL` tags, and `EXTENDS` clauses, and enumerates built-in operator names in the XML schema with richer documentation ([#1314](https://github.com/tlaplus/tlaplus/pull/1314), [#1307](https://github.com/tlaplus/tlaplus/pull/1307), [#1308](https://github.com/tlaplus/tlaplus/pull/1308), [#1309](https://github.com/tlaplus/tlaplus/pull/1309), [#1324](https://github.com/tlaplus/tlaplus/pull/1324), [#1346](https://github.com/tlaplus/tlaplus/pull/1346)).
+
+- TLC: Adds direct support for `x' \subseteq S` in specifications and ENABLED expressions, enabling efficient handling of subset constraints in next-state relations without requiring user-defined encodings ([#1287](https://github.com/tlaplus/tlaplus/pull/1287)).
+
+- TLC: Introduces a `SanySettings` API and updates XML export to skip PlusCal validation and optional analyses when requested, while ensuring linting only runs after successful semantic and level checking to avoid crashes in partial-analysis modes ([#1305](https://github.com/tlaplus/tlaplus/pull/1305), [#1356](https://github.com/tlaplus/tlaplus/pull/1356)).
+
+- TLC: Improves configuration processing by correctly handling `LazyValue` and `LetInNode` in `SPECIFICATION` and `PROPERTY` declarations, allowing temporal formulas to flow through parameterized operators and LET/IN constructs, and by permitting variables to appear as `PROPERTY` definitions when used as degenerate actions ([#1321](https://github.com/tlaplus/tlaplus/pull/1321), [#1329](https://github.com/tlaplus/tlaplus/pull/1329), [#1323](https://github.com/tlaplus/tlaplus/pull/1323)).
+
+- TLC: Fixes a crash when using `@Evaluation`-annotated operators as constant substitutes and resolves a bogus error that claimed a constant was substituted with a non-constant, improving robustness of advanced constant-configuration patterns ([#1110](https://github.com/tlaplus/tlaplus/pull/1110), [#1330](https://github.com/tlaplus/tlaplus/pull/1330)).
+
+- TLC: Adds JPF-based verification to the GitHub Actions PR workflow and enhances CI to run on Windows, increasing automated coverage across platforms and catching Java-level issues earlier in development ([#1334](https://github.com/tlaplus/tlaplus/pull/1334), [#1343](https://github.com/tlaplus/tlaplus/pull/1343)).
+
+- TLC: Fixes `BufferedDataInputStream#readString` so truncated streams now correctly raise `EOFException` instead of returning NUL-padded partial strings, preventing silent data corruption when reading serialized TLC data ([#1335](https://github.com/tlaplus/tlaplus/pull/1335)).
+
+- TLC: Enumerates SANY and XML exporter exit codes in dedicated classes and updates XMLExporter to print only SANY’s user-friendly parse errors instead of Java stack traces, improving integration with external tools and command-line UX ([#1319](https://github.com/tlaplus/tlaplus/pull/1319), [#1327](https://github.com/tlaplus/tlaplus/pull/1327)).
+
+- TLC: Migrates Maven snapshot publishing to Sonatype’s Central Publisher Portal and improves GitHub Actions security by pinning or removing third-party actions, tightening the project’s supply-chain posture ([#1312](https://github.com/tlaplus/tlaplus/pull/1312), [#1364](https://github.com/tlaplus/tlaplus/pull/1364)).
+
+- TLC: Switches the rolling-release versioning scheme to calendar versioning (`YYYY.MM.DD.HHmmss`), clearly separating it from the 2.x maintenance branch and making build timestamps explicit in version numbers ([#1328](https://github.com/tlaplus/tlaplus/pull/1328)).
+
+- TLC: Updates `TLCRuntime` to report 32-bit vs 64-bit architectures instead of x86-specific names, fixing incorrect architecture detection on ARM systems and simplifying downstream logic ([#1345](https://github.com/tlaplus/tlaplus/pull/1345)).
+
+- TLC: Adds a deprecation notice to the Toolbox welcome page and release notes that points users to the actively maintained VS Code / Cursor extensions and CLI tooling, and expands README/USE documentation for using TLC as a library or via standard formats ([#1339](https://github.com/tlaplus/tlaplus/pull/1339), [#1340](https://github.com/tlaplus/tlaplus/pull/1340)).
+
+- TLC: Improves liveness checking by fixing bogus safety counterexamples, implementing lazy evaluation of operator arguments in `Liveness.java`, deferring certain configuration warnings until properties are classified as safety or liveness, and showing which temporal property is violated in counterexamples ([#1348](https://github.com/tlaplus/tlaplus/pull/1348), [#1350](https://github.com/tlaplus/tlaplus/pull/1350), [#1351](https://github.com/tlaplus/tlaplus/pull/1351), [#1355](https://github.com/tlaplus/tlaplus/pull/1355)).
+
+- TLC: Adds fine-grained SANY CLI flags `-suppressMessages` and `-warningsAsErrors` so users and tools can selectively silence or promote specific diagnostics to errors, enabling stricter pipelines without patching SANY itself ([#1344](https://github.com/tlaplus/tlaplus/pull/1344)).
+
+- TLC: Integrates the TLA+ formatter into `tla2tools.jar`, making formatting available alongside SANY and TLC without a separate binary and updating the build and tests (including Windows support) accordingly ([#1347](https://github.com/tlaplus/tlaplus/pull/1347)).
+
+- TLC: Fixes a subtle ENABLED soundness bug involving INSTANCE substitutions and Java operator overrides by correcting how primed variables are resolved under `Context.branch`, and adds regression tests to capture the failure mode ([#1342](https://github.com/tlaplus/tlaplus/pull/1342)).
+
+- TLC: Discontinues macOS code signing and notarization due to expired certificates, documenting that users must now manually whitelist the Toolbox or prefer the VS Code / Cursor workflows on macOS ([#1365](https://github.com/tlaplus/tlaplus/pull/1365)).
+
+- Vscode Extension: Implements interactive state-space navigation in the debugger UI, allowing users to select successor states and backtrack through traces in sync with the new TLC backend capabilities ([#475](https://github.com/tlaplus/vscode-tlaplus/pull/475)).
+
+- Vscode Extension: Expands the animation guide with the `AnimWatch` operator and a shared `AnimDoc` abstraction, updating all six real-world examples to a consistent `AnimView`/`AnimDoc`/`AnimAlias`/`AnimWatch` pattern that clarifies when to use interactive debugging versus screencast-style animations ([#478](https://github.com/tlaplus/vscode-tlaplus/pull/478)).
+
+- Vscode Extension: Restores the `>>` navigation control in the model-checking panel so users can jump directly from counterexample steps to the corresponding actions in the source, improving trace navigation ([#481](https://github.com/tlaplus/vscode-tlaplus/pull/481)).
+
+- Vscode Extension: Adds automatic counterexample replay using TLC’s `-dumpTrace`/`-loadTrace` integration, so safety and liveness violations can be reloaded and debugged in seconds without re-running the model checker, even for very large state spaces ([#484](https://github.com/tlaplus/vscode-tlaplus/pull/484)).
+
+- Vscode Extension: Introduces a dedicated output channel for the MCP server, surfacing logs, errors, and the server URL in one place so users can inspect MCP behavior and reuse the server outside VS Code or Cursor if desired ([#487](https://github.com/tlaplus/vscode-tlaplus/pull/487)).
+
+- Vscode Extension: Improves robustness of TLC integration by fixing filename variable substitution in custom options, handling `STARTMSG` lines without severity suffixes, rejecting missing TLC input files early, and correcting deleted-value handling and sequence diff alignment in the model-checking UI ([#486](https://github.com/tlaplus/vscode-tlaplus/pull/486), [#489](https://github.com/tlaplus/vscode-tlaplus/pull/489), [#490](https://github.com/tlaplus/vscode-tlaplus/pull/490), [#491](https://github.com/tlaplus/vscode-tlaplus/pull/491), [#493](https://github.com/tlaplus/vscode-tlaplus/pull/493)).
+
+- Vscode Extension: Hardens model and config resolution so custom runs can pick embedded `.tla` configs, and refines artifact naming and Windows CI expectations to make model selection deterministic across platforms ([#495](https://github.com/tlaplus/vscode-tlaplus/pull/495)).
+
+- Vscode Extension: Adds built-in support for the TLA+ formatter (now shipped in `tla2tools.jar`), including fixes for specs that `EXTENDS CommunityModules`, formatter version updates, and configuration so the extension uses the integrated formatter by default while validating AST preservation after each run ([#327](https://github.com/tlaplus/vscode-tlaplus/pull/327), [#496](https://github.com/tlaplus/vscode-tlaplus/pull/496), [#497](https://github.com/tlaplus/vscode-tlaplus/pull/497), [#510](https://github.com/tlaplus/vscode-tlaplus/pull/510), [#506](https://github.com/tlaplus/vscode-tlaplus/pull/506)).
+
+- Vscode Extension: Adds a feature to generate PlantUML sequence diagrams from TLC error traces by parsing the `trace` variable and emitting `.puml` files, making it easier to visualize protocol behaviors with existing PlantUML tooling ([#498](https://github.com/tlaplus/vscode-tlaplus/pull/498)).
+
+- Vscode Extension: Fixes MCP TLC tools to honor an explicit `cfgFile` parameter instead of re-running config discovery, enabling workflows with multiple `.cfg` files per module and aligning MCP behavior with standard TLC usage ([#509](https://github.com/tlaplus/vscode-tlaplus/pull/509)).
+
+- TLAPM: Updates example specifications to avoid identifier shadowing that SANY rejects, aligning TLAPM’s examples with the stricter parser and preventing parse failures when checked with the standard toolchain ([#251](https://github.com/tlaplus/tlapm/pull/251)).
+
+- Community Modules: Adds several new theorems about folds on functions and sequences, including results about how `FoldLeft` and `FoldRight` interact with sequence concatenation, and adjusts Graphs/Relations syntax to avoid tuple bindings that TLAPS does not support ([#118](https://github.com/tlaplus/CommunityModules/pull/118), [#119](https://github.com/tlaplus/CommunityModules/pull/119), [#120](https://github.com/tlaplus/CommunityModules/pull/120)).
+
+- Examples: Expands the animation catalog with refined formatting for EWD998 and new animated specifications for the Tower of Hanoi and sliding puzzles, demonstrating how to build rich SVG-based visualizations for classic problems ([#193](https://github.com/tlaplus/Examples/pull/193), [#194](https://github.com/tlaplus/Examples/pull/194), [#195](https://github.com/tlaplus/Examples/pull/195)).
+
+- Examples: Fixes a failing proof in the ByzPaxos example, adds a new “dag-based consensus” specification, introduces DieHardest.tla to compare jug configurations via parallel and interleaved self-composition, and corrects a typo in the Bakery algorithm pseudo-code comment ([#197](https://github.com/tlaplus/Examples/pull/197), [#198](https://github.com/tlaplus/Examples/pull/198), [#199](https://github.com/tlaplus/Examples/pull/199), [#203](https://github.com/tlaplus/Examples/pull/203)).
+
+- Examples: Adjusts dependencies by logically reverting the use of Fork-based function libraries after their removal from TLAPM and adds a fallback to Apalache v0.52.2 in the Apalache download helper, improving resilience when fetching the latest Apalache release fails ([#196](https://github.com/tlaplus/Examples/pull/196), [#202](https://github.com/tlaplus/Examples/pull/202)).
+
+- Apalache: Releases v0.52.2, v0.52.3, v0.54.0, v0.55.0, and v0.56.0–v0.56.1 with a focus on JSON-RPC improvements (new `applyInOrder`, `compact`, `STATE` query kind, and compression), Jetty 12 upgrades, better UNCHANGED inlining, Quint `leadsTo` support, and bug fixes in the lexer and printers; the latest release notes are in [v0.56.1](https://github.com/apalache-mc/apalache/releases/tag/v0.56.1).
+
+- Apalache: Makes `Variants.tla` compatible with TLC by redefining variants as functions over singleton domains and adds TLC integration tests, ensuring Apalache-generated specs using variants can be checked consistently with TLC ([#3255](https://github.com/apalache-mc/apalache/pull/3255)).
+
+- Apalache: Extends the JSON-RPC exploration server with `applyInOrder`, `compact`, and a `STATE` query kind, plus gzip and Zstandard compression, reducing client round-trips and payload sizes for complex symbolic explorations ([#3280](https://github.com/apalache-mc/apalache/pull/3280), [#3285](https://github.com/apalache-mc/apalache/pull/3285), [#3288](https://github.com/apalache-mc/apalache/pull/3288), [#3290](https://github.com/apalache-mc/apalache/pull/3290)).
+
+- Apalache: Adds Quint-to-TLA+ conversion support for `leadsTo`, fixes a LET/IN-related bug in `setBy` transpilation, and properly inlines nullary operators in `UNCHANGED`, addressing subtle correctness issues in translated specs ([#3294](https://github.com/apalache-mc/apalache/pull/3294), [#3295](https://github.com/apalache-mc/apalache/pull/3295)).
+
+
+
+
+
+
+### By the Numbers
+
+| Metric | Jan 2026 | Feb 2026 | Mar 2026 |
+
+| ----------------------------- | -----------: | -----------: | -----------: |
+
+| Open issues | 48 | 51 | 53 |
+
+| Merged pull requests | 40 | 41 | 50 |
+
+| Commits | 138 | 74 | 143 |
+
+| Active contributors | 14 | 9 | 12 |
+
+| New contributors | 3 | 2 | 1 |
+
+| Google Group messages | 32 | 31 | 40 |
+
+| Tool runs (TLC) | 263941 | 97573 | 209261 |
+
+
+
+
+
+
+> Tool usage stats are opt-in and anonymized; actual usage is likely higher.
+> Source: [metabase.tlapl.us](https://metabase.tlapl.us/public/dashboard/cf7e1a79-19b6-4be1-88bf-0a3fd5aa0dec).
+
+### Community & Events
+
+
+- The [abridged summary of the tlaplus mailing list](https://discuss.tlapl.us/msg06624.html) highlights one notable update from the email community.
+
+- A thread on [checking if a set is a singleton](https://discuss.tlapl.us/msg06626.html) clarifies idiomatic TLA+ patterns for expressing and proving singleton properties.
+
+- The discussion on [constant operators and refinements](https://discuss.tlapl.us/msg06637.html) examines how constants behave under refinement mappings.
+
+- A user shared their [experience proving liveness with TLAPS](https://discuss.tlapl.us/msg06610.html), including practical tips and current limitations.
+
+- The [font dependency specification](https://discuss.tlapl.us/msg06614.html) thread documents how TLA+ tools depend on system fonts and how to configure them.
+
+- A question on whether [ENABLED P is always stuttering-insensitive](https://discuss.tlapl.us/msg06630.html) led to a nuanced explanation of ENABLED and stuttering semantics.
+
+- The Outreach Committee invited community members to the [January 15 TLA+ Outreach Committee meeting](https://discuss.tlapl.us/msg06621.html) to discuss ecosystem and education initiatives.
+
+- A modeling advice thread on [capturing safety properties](https://discuss.tlapl.us/msg06634.html) shares patterns for structuring specs so that safety is easy to state and check.
+
+- The [presentation for the next community meeting](https://discuss.tlapl.us/msg06618.html) thread coordinated talk topics and materials for an upcoming gathering.
+
+- The announcement for the [TLA+ Community Meeting 2026](https://discuss.tlapl.us/msg06633.html) shares date, format, and participation details.
+
+- A new [TLA+ Debugger for interactive state-space exploration](https://discuss.tlapl.us/msg06620.html) was introduced, enabling stepwise inspection of TLC runs.
+
+- The [TypeOK for primed variables](https://discuss.tlapl.us/msg06622.html) discussion explains how to write invariants that correctly constrain next-state values.
+
+- A post on [verified spec transpilation with Claude](https://discuss.tlapl.us/msg06635.html) explores using AI tools to transform TLA+ specifications while preserving meaning.
+
+- A thread comparing [\subseteq vs \in SUBSET](https://discuss.tlapl.us/msg06611.html) clarifies semantic and stylistic differences between the two set operators.
+
+- A PlusCal-focused thread on [adding raw TLA+ to process states](https://discuss.tlapl.us/msg06660.html) shows how to mix PlusCal and TLA+ for more expressive specs.
+
+- The [AgentSkills call for contributions](https://discuss.tlapl.us/msg06642.html) invites reusable skill definitions for AI tools that work with TLA+.
+
+- A discussion of a [discarded prototype TLA+ syntax using @ in proofs](https://discuss.tlapl.us/msg06657.html) gives historical context on proof-language design choices.
+
+- A practical thread on [avoiding *.tlc dump files](https://discuss.tlapl.us/msg06667.html) explains how to configure TLC’s checkpointing and output.
+
+- The launch of [tlabyexample.com](https://discuss.tlapl.us/msg06649.html) provides a growing collection of small, focused TLA+ examples for learners.
+
+- Another announcement for the [January 15 Outreach Committee meeting](https://discuss.tlapl.us/msg06646.html) reiterates how to join and contribute agenda items.
+
+- A post on [module instantiation semantics](https://discuss.tlapl.us/msg06643.html) clarifies how INSTANCE, parameters, and renaming behave in TLA+.
+
+- The [performance when using tuples](https://discuss.tlapl.us/msg06654.html) thread reports on TLC performance characteristics and modeling trade-offs with tuples.
+
+- A discussion on [practical applications of absolute fairness](https://discuss.tlapl.us/msg06647.html) examines when strong fairness assumptions are realistic in software models.
+
+- A user debugging a [TLC error in the Bounded FIFO example](https://discuss.tlapl.us/msg06644.html) receives guidance on configuration and spec interpretation.
+
+- A second announcement for the [TLA+ Community Meeting 2026](https://discuss.tlapl.us/msg06656.html) provides updated logistics and participation info.
+
+- The thread on [plans for Distributed PlusCal](https://discuss.tlapl.us/msg06671.html) discusses the current status and possible future directions of the language extension.
+
+- A post on [describing an unless condition in Lisp](https://discuss.tlapl.us/msg06687.html) connects temporal reasoning in TLA+ with constructs in Lisp-based tooling.
+
+- A SANY internals question about the [APSubstInNode AST node](https://discuss.tlapl.us/msg06676.html) sheds light on how the parser represents substitutions.
+
+- A later [Outreach Committee meeting thread](https://discuss.tlapl.us/msg06684.html) follows up with notes and ongoing opportunities to get involved.
+
+- The [“Leader backs up followers quickly with persistence”](https://discuss.tlapl.us/msg06686.html) thread discusses a replicated log design and its TLA+ model.
+
+- A popular thread on [modeling a network using a set or a bag](https://discuss.tlapl.us/msg06689.html) compares different abstractions for messages and channels.
+
+- In [“Request for review?”](https://discuss.tlapl.us/msg06677.html), a community member receives detailed feedback on a nontrivial specification.
+
+- The [stuttering: abstraction vs. implementation](https://discuss.tlapl.us/msg06708.html) discussion clarifies how stuttering steps relate refinement levels.
+
+- The [TLX project](https://discuss.tlapl.us/msg06712.html) introduces writing TLA+ specifications in Elixir syntax with TLC integration.
+
+- A thread on [using TLA+ to fix a difficult glibc bug](https://discuss.tlapl.us/msg06675.html) highlights Malte Skarupke’s C++Now 2025 talk and its lessons.
+
+- A follow-up on the [plan for Distributed PlusCal](https://discuss.tlapl.us/msg06673.html) continues the discussion on roadmap and community needs.
+
+- The [2024 Grant Program call for proposals](https://foundation.tlapl.us/grants/2024-grant-program/index.html) invites projects seeking USD $1,000–$100,000 to advance TLA+ in research and industry.
+
+- The Foundation also announced new [grant recipients](https://foundation.tlapl.us/grants/grant-recipients/index.html) whose projects aim to improve TLA+ technology and benefit the broader community.
+
diff --git a/content/blog/2026-q1-dev-update/prs_per_month.svg b/content/blog/2026-q1-dev-update/prs_per_month.svg
new file mode 100644
index 0000000..96c50aa
--- /dev/null
+++ b/content/blog/2026-q1-dev-update/prs_per_month.svg
@@ -0,0 +1,4 @@
+
+
\ No newline at end of file
From 90c53210f4b0f137b54c9566f690d543d3d13c53 Mon Sep 17 00:00:00 2001
From: Federico Ponzi
Date: Tue, 21 Apr 2026 21:26:08 +0100
Subject: [PATCH 2/7] s/liveness/completeness
Signed-off-by: Federico Ponzi
---
content/blog/2026-q1-dev-update/index.md | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/content/blog/2026-q1-dev-update/index.md b/content/blog/2026-q1-dev-update/index.md
index afa264a..aa0321f 100644
--- a/content/blog/2026-q1-dev-update/index.md
+++ b/content/blog/2026-q1-dev-update/index.md
@@ -4,7 +4,7 @@ title = 'Q1 2026 Quarterly Development Update'
date = 2026-04-21
+++
-This quarter focused on hardening verification correctness, deepening debugger support, and tightening integration across the TLA+ toolchain. TLC received several critical soundness and liveness fixes, including repairs to FcnLambdaValue handling, ENABLED semantics, bogus safety counterexamples, and truncated trace reads that could previously yield silent wrong results, alongside a new interactive debugger, trace replay, and ARM64-native builds. The VS Code extension, Apalache, TLAPM, and the examples and community modules all advanced in parallel, with integrated formatting, richer trace visualizations, improved JSON-RPC workflows, and an active community exploring liveness, refinement, and real-world modeling patterns.
+This quarter focused on hardening verification correctness, deepening debugger support, and tightening integration across the TLA+ toolchain. TLC received several critical soundness and completeness fixes, including repairs to FcnLambdaValue handling, ENABLED semantics, bogus safety counterexamples, and truncated trace reads that could previously yield silent wrong results, alongside a new interactive debugger, trace replay, and ARM64-native builds. The VS Code extension, Apalache, TLAPM, and the examples and community modules all advanced in parallel, with integrated formatting, richer trace visualizations, improved JSON-RPC workflows, and an active community exploring liveness, refinement, and real-world modeling patterns.
From fd8e00639e210eaee04b3fd21a17f23ebc910f67 Mon Sep 17 00:00:00 2001
From: Federico Ponzi
Date: Tue, 21 Apr 2026 21:46:48 +0100
Subject: [PATCH 3/7] Add section about fixed completness/soundness issues
Signed-off-by: Federico Ponzi
---
content/blog/2026-q1-dev-update/index.md | 18 ++++++++++++++++++
1 file changed, 18 insertions(+)
diff --git a/content/blog/2026-q1-dev-update/index.md b/content/blog/2026-q1-dev-update/index.md
index aa0321f..d33162a 100644
--- a/content/blog/2026-q1-dev-update/index.md
+++ b/content/blog/2026-q1-dev-update/index.md
@@ -7,6 +7,24 @@ date = 2026-04-21
This quarter focused on hardening verification correctness, deepening debugger support, and tightening integration across the TLA+ toolchain. TLC received several critical soundness and completeness fixes, including repairs to FcnLambdaValue handling, ENABLED semantics, bogus safety counterexamples, and truncated trace reads that could previously yield silent wrong results, alongside a new interactive debugger, trace replay, and ARM64-native builds. The VS Code extension, Apalache, TLAPM, and the examples and community modules all advanced in parallel, with integrated formatting, richer trace visualizations, improved JSON-RPC workflows, and an active community exploring liveness, refinement, and real-world modeling patterns.
+## Soundness and completeness fixes in TLC
+
+This quarter saw an unusually large batch of soundness and completeness fixes
+land in TLC, most of them tracked from [#1332](https://github.com/tlaplus/tlaplus/issues/1332).
+Several had been latent for years and could, in the worst case, cause TLC to
+silently miss property violations or report bogus counter-examples. Users are
+encouraged to re-run their models against the fixed release.
+
+If you're using the [VSCode](https://marketplace.visualstudio.com/items?itemName=tlaplus.vscode-ide) extension, you're always running the latest version of TLC.
+
+This is the list of resolved issues:
+- [#1302](https://github.com/tlaplus/tlaplus/issues/1302): `FcnLambdaValue#toFcnRcd` mutated `excepts`, corrupting fingerprints and causing both missed and bogus safety/liveness violations (latent since ~2011).
+- [#1145](https://github.com/tlaplus/tlaplus/issues/1145): `FcnLambdaValue.toTuple()` dropped `EXCEPT` overrides when a lazy function was coerced to a tuple (e.g. via `SubSeq`).
+- [#1348](https://github.com/tlaplus/tlaplus/issues/1348): liveness checking reported bogus safety counter-examples by short-circuiting on accepting tableau nodes without checking the negated property's `PossibleErrorModel`.
+- [#742](https://github.com/tlaplus/tlaplus/issues/742): universally-quantified `WF`/`SF` conjuncts spuriously failed with "temporal formula is a tautology".
+- [#725](https://github.com/tlaplus/tlaplus/issues/725): fairness in instantiated submodules referencing primed variables via `SelectSeq`/`LAMBDA` failed with "undefined identifier".
+- [#1112](https://github.com/tlaplus/tlaplus/issues/1112): `DiskFPSet` could stall indefinitely after a duplicate-fingerprint warning on long-running checks.
+
## Development Updates
From 0e07ab877d824bc462f33435014c3b3af24f3684 Mon Sep 17 00:00:00 2001
From: Federico Ponzi
Date: Tue, 21 Apr 2026 22:15:16 +0100
Subject: [PATCH 4/7] Add section about tla+ debugger
Signed-off-by: Federico Ponzi
---
content/blog/2026-q1-dev-update/index.md | 33 ++++++++++++++++++++++++
1 file changed, 33 insertions(+)
diff --git a/content/blog/2026-q1-dev-update/index.md b/content/blog/2026-q1-dev-update/index.md
index d33162a..4126c23 100644
--- a/content/blog/2026-q1-dev-update/index.md
+++ b/content/blog/2026-q1-dev-update/index.md
@@ -25,6 +25,34 @@ This is the list of resolved issues:
- [#725](https://github.com/tlaplus/tlaplus/issues/725): fairness in instantiated submodules referencing primed variables via `SelectSeq`/`LAMBDA` failed with "undefined identifier".
- [#1112](https://github.com/tlaplus/tlaplus/issues/1112): `DiskFPSet` could stall indefinitely after a duplicate-fingerprint warning on long-running checks.
+## TLA+ Debugger: Interactive State-Space Exploration
+
+The TLA+ Debugger gained interactive state-space exploration: instead of
+waiting for TLC to find a violation, you can now drive your spec by hand —
+pick an initial state, choose any successor produced by `Next`, and step
+backward to any earlier state. Combined with Watch expressions on an
+animation module's `AnimView` operator, this turns the debugger into a
+graphical debugger for your protocol, where each state is rendered as an
+SVG you can navigate through.
+
+A few capabilities make this practical for real debugging sessions:
+
+- Conditional breakpoints on `Init`/`Next` (e.g. `~ENABLED Next` to halt at
+ deadlocks), and halting even when `Next` is `FALSE`.
+- Watch and Debug expressions can now load any module on the TLA-Library
+ path, so you can export the current trace mid-session as JSON, TLA+,
+ GraphViz, TLC binary, or a replayable trace expression — without
+ preconfiguring the run or forcing a violation.
+- Step-in / step-over pick "close" vs "far" successors via Hamming distance,
+ and finite stuttering is preserved for faithful behavior replay.
+
+This is the first step toward [#860](https://github.com/tlaplus/tlaplus/issues/860):
+craft interesting traces interactively, export them, and have TLC re-verify
+them against the spec as it evolves.
+
+For the full write-up by Markus Kuppe, see the [Reddit announcement](https://www.reddit.com/r/tlaplus/comments/1q7vhod/tla_debugger_interactive_statespace_exploration/),
+and watch [Interactive State-Space Exploration & Graphical Debugging with Animations](https://www.youtube.com/watch?v=ZrzoIYjFeHE)
+for a demo.
## Development Updates
@@ -282,3 +310,8 @@ Filtered items (editor: re-add if you disagree):
- The Foundation also announced new [grant recipients](https://foundation.tlapl.us/grants/grant-recipients/index.html) whose projects aim to improve TLA+ technology and benefit the broader community.
+
+
+---
+
+Part of this post was generated using AI.
From b84413d4cf396c04c1f4fa2902f984ebb90b38ed Mon Sep 17 00:00:00 2001
From: Federico Ponzi
Date: Tue, 21 Apr 2026 22:22:36 +0100
Subject: [PATCH 5/7] add section about divergence detection in vscode
Signed-off-by: Federico Ponzi
---
content/blog/2026-q1-dev-update/index.md | 15 +++++++++++++++
.../pluscal-divergence-modelcheck.png | Bin 0 -> 88707 bytes
.../pluscal-divergence-translate.png | Bin 0 -> 104720 bytes
3 files changed, 15 insertions(+)
create mode 100644 content/blog/2026-q1-dev-update/pluscal-divergence-modelcheck.png
create mode 100644 content/blog/2026-q1-dev-update/pluscal-divergence-translate.png
diff --git a/content/blog/2026-q1-dev-update/index.md b/content/blog/2026-q1-dev-update/index.md
index 4126c23..7d4eed6 100644
--- a/content/blog/2026-q1-dev-update/index.md
+++ b/content/blog/2026-q1-dev-update/index.md
@@ -54,6 +54,21 @@ For the full write-up by Markus Kuppe, see the [Reddit announcement](https://www
and watch [Interactive State-Space Exploration & Graphical Debugging with Animations](https://www.youtube.com/watch?v=ZrzoIYjFeHE)
for a demo.
+## Detecting PlusCal/TLA+ divergence before translating
+
+The VS Code extension now detects when the TLA+ inside a `BEGIN/END
+TRANSLATION` block has been edited by hand since the last PlusCal
+translation, and warns you before silently overwriting your changes.
+On `TLA+: Parse Module`, SANY runs first and a checksum mismatch surfaces
+a confirmation dialog so you can choose to keep your edits or re-translate.
+
+
+
+Conversely, if the PlusCal source has changed and you start model checking
+without re-translating, the extension now flags the stale TLA+ translation:
+
+
+
## Development Updates
Summaries of merged pull requests (and significant issues or releases) for
diff --git a/content/blog/2026-q1-dev-update/pluscal-divergence-modelcheck.png b/content/blog/2026-q1-dev-update/pluscal-divergence-modelcheck.png
new file mode 100644
index 0000000000000000000000000000000000000000..6bbf0ed06d1f704095eb7be902513a74768cfcc0
GIT binary patch
literal 88707
zcmY(q19T0)m$i|EUNB1ZD*U1S|;!@%>Br&TQHD8<>-@gfi6k;SFW{`};eV
z^DlL0B|B4RHv>l#ATwJ#8xuMwBS#YxTPJfn=PS@|{_l&(|G7xS(Zs;n!p@dZ*}}#I
zNap(kBRipxy(1wrBQrZ8GYdB>8#fy}a-<^z5D+1d#7`k*_pI{`A8loo&z_rDV%@%u
z=N>}p!jmYuJSw9ibFzDynGY&UvQOq(nM$@9MQfTm702fB4M!VzE7;1v*5F=98#30g
z>umXuy^4c?-dQX(EXCHtzi0tl1pYmY!*Jt3haTO!UB;K|VNO@;UWc1kS$BLF)ZYgZ
zn2>o;R%K2VYc7pSRw)8rg^zamS5;|g>0Nb4M^;1xOjY}38+m23PP^+RO$}sHQt9)v
zIR4h;NFv3_LPhFO^B!P!_I8n8I1}XuQ%qo>(nGPAhsO^*z95PmcNhW!g4oo(rnNzN
zWo0nIqseTKhlOqy$9)<6tt$HmPVeR64L7+;7Mt-jChO&E)icy#iSlx0!@rES?HBC2
zem)|FcLHDUx#F^$%4Vy2pSQ?~J6u
zVFaJqYfD?2#WIGSpk5gz1S1Vgm
zOF7+-XScVGtKs_5gito|EGkMOcdSi-(noEQKsI7^l6gu7hNJCXyX9^_0roZU_xHB#
ztE;JK4unECJDbSly=wy!ugCLzkuZdHpC>-&v&G7RCOU0AYjzw+M0^0t#FU)r^)^wZ
zGVxJTYUc{8X6{pjob+&~_D4bA=
z$r8*(aJ|{o?S|V{{sP2Ig_>P+b$25!w{sjUhP6vE792!JXQvhbu6xmlrUBtiUq&Ru
z>uOcLrnsOW(DmZKQ&Lh2qKheRuUMF9lm@fXq*r%3ou~4AJU_X);FJQh0u%biK}!lN
zI-qryuc9!8?eUJMt-9*7-4&?h`)?2?F|?4tdharjOC89>Ndh^loXFLUzQFfRJ=eI^
zo+>NthBR!-XafnMzR#RR`6n{5D~|h|3Zcx^
z|0w$V;=XDHqsn%iHVn(9stvTeS!Fk~@=km);7l4Dy??}Np>DxWx>24!)bw^o>&5;7
z`0=l(&y5bK_7>-xL;MOgg%)a_7t%;28BmK*fz#wIvwSC#)i|$f=}Z5SCy-DZXZ^;g
z%BQE~)#ZXPst_oeWev3#TL@{jp%~1R7p$ymuduMj`?(*A1$s$=lDhwlyK&Lj9@ekaQ0x6A05j7n^p_@H$2+c
zciZy?;pf4O&x2SWuXsG^{?#D089sy#{9jfIbrO8pv;W^s^IaHDVjLf<0U4{U)>$vW
zt)Lh-m~vSnR8PdEZis>289MkvNW4`^y95)sl#~M$H57%maXOlh_wj|^UQG>`#v`%4
zK@IoUE>=RBe^+c38cSMVy9*z}A(e)H)`
zOtrV!){YD=rn2LFyk%$0e>ae|Rg3l6@%yyld^w^>NyW>vs?tWrSd^j&R^yNws(8a-
zEBlMDAL5m=`cr#}G(DYz6LQDBedZw?WZQ1xm87tf1!rNJD`A3bh;$dD(8|^KR9#u`{TWltraK9@fIiLV=VaBX)j6Q
z5ObH5(vtIqVwZae7t2=9K3ZR&pLH4ZVkx=e?orJNW-zU1ES&?y&yHdn8m21}Uter5
zZaBja9$5En2+HSspJF~gFqh?xbE&pOp+|>l=8*9}OX)9i;GWStdROCy+EUtL2?TqW
z={+bMdgZilCnO!6W6}<=*4W$kX6^2e8`^buhk(cs0MY^;$-o+Kl
z;hr;lYb}$_CS{Zh)~&a~=Z$^KP~<;yA_Z6I{rUxNa&WLr|33bb%V3`!i@3Ro
zcM5KF4$2092#9Yx(fIW5GLdA^F2-)IKS80%GdTtDOiMOyB}0XK{)V>W?|Tf?A^n>B
z`B$4y5%df>xFTHdE1%c?iSYIGjmcY{P)C}l#Y;ukWDK98jZ7y;yMzbfXB4#Q11LAQ
z+iBFig79DS|DfmFy;5DQHWmh@Vr28YJM(0hys*l$>v`ABeE{T
zSJZZ8qoJWS+@1D}Zf(h6Xbg%W8_4`?fWC*<6l-_Y_9bt%-{HmMcDA(Nqye|%miD46
zI<2l+=Q%;RM6}N1Q5vyezZ^CllA{JHzu-mpmnzZdKHzIwxJ+1BZmV*z{1hWCNe6~U
z!Ox1=+&Si9CVKkIXmF==KKd2+=iVdgU7+$vYl)JptFMnl)_SR5=JURJ4-K9q6k>DNCo$QTRA$|?gxC5|mvYNDB^`n08!*BYS*eQ1tT+KRPVoY6PhAI%YyS%syO
zNurA`bTmrK-DK%L?1b(R^>!}P<;4-Gtnq23q^_Md#3WoH9b2>m+b7cfmP{{O`*CLR
z@>@DWqNWhV%+NA%=o45h9_gmH%+2*|ci>I$CZT(RiI!v}4os0t7b0bw7}4mJ#Yj#8
z;aMOkTwiQNMK;Dwvb@?HY9rwc;hBEF?-RF|I(dTHC~=wacYfbM*?rw1*^y5YzlNsZ
z?2O=PWA&C56o6dmdbYV;k+<<2n2g
zGU@3$SH*Ek$LDo~I@KhGi*RuGr;dL#`H8tEz=oxtZSIqU7<8FQ%mx|BUBKU>v{oA2
z*h9Bian~K3B$#{>0=&=W&ZWJ7Behzt9uADZ_tOKuG<#wC<=H3UYppH{6PjDeg|sW`4O@lZj4Y?
z3yM0I!9_X4x26v`HB7e)ys
zw7eE7=$Mq#&=GtAufMJFw3PV(^|!l&qPgoVVO2j~Xf^x)FEoH^bZ@ki^YC~%SgL}9
z-#m0$EKQM4Sn3QINe+P!{yC4yS{^?BM{W6Zw1*`Dn9Gqmv?|B^CO_^;m$`isqz&uu
zdYMfJXWQr^+uNss=~AZF2&|s??|xe)d_pXBOo4W4c~HXq+^(dM+;gK}#eH2#7yB}Z
zWjOZK!`sn+Mg^mt=M;4-(Mo~iSUrgky9EE*sVKVzTa89=B|Sn^dl#_sUzsqY+$*hP
z1M`x>)XQ4CLT-;GS5*pny1nY+=6rKLG&ri|q2hU7K|^V2R+4Os&b=ZcLsQmJ
zL|x*e3e<#p)9b#k2I(_wDr*>&^L8o;Phww|gj8l0`P--3sRBc&s`R1P2l_`eAoDbC
zKha9TSUiRi89FO(C`?vl5d$L2^u$PU;N$k!7Lzj@;Zz}MJRI>2zFX62JPsDyeuY^Z
zf%umPIbQB@-<%31k@Pw6|5>{#h)LeLh7bLT9xT8Hb78m?j(XZNKJ12OL9yb9lvj`r
zxZt$1A#pZAgceLr-}%?d&&lp_?}itW!wqg6AJ{*hGZ2VmJ-x0V5IEDGCUI)2zefOq
z_Ab}rMT}FyXo4&W*Kz1j)E*YUpFc#2eXm|*8ddmLKjE%+^*!C_`n`nO%94x(Q1es3
zcb$@p;~nRQ`tm;bkyRt@Dx+y)
z=&jKRX%qt6Ny5VvDs#SdNnuOr1GS4b{4#k}G~{DKqQ>Es1$Jb(W^w|Cma2RX
z9(T|pI`xdhvb-JIlZEg2n&SV=?xOaIN0IBM%$vumZ_VLSoc^;lKGg^orT^z8CUIa!
z4T8kfU&!Kwq*mxVip*u(te!rDoO9SBMQf{VJS~?vQQ;IT6QP@g>%r6}GVnjlZNrHUiz|7*R1m1NnA2`bpv`%g+Xml*uo|WHszahZnF;D)
zko=p>F8t%8OylseP$YYaZUNLryv*gQHpIR54nn{~*7iXk)9c;uf13q>-RGKf{etL<
zu21FD$BF?-^-WU#N21Y=Y2cmEW2`3Mf%bp=esId-{84%_q}898WE}(gl^SjP`}!^~
z?FZ=4WZovV#_}1_0mhq9Q!oba2WcOB5IgTiJSR#>k?E#nVW
zjLq(dfHm=zBO(dfoIuLmeCVjG#VQX8)?DQ!@hm(_x?3~4f5(GUT6zsyq7PzGy~nxd
z2Rt(^KJ6P@k-vaI;`mx|#yac3pkMud>>DS@^M*Hzl5LByRXYAhI9%DdP2%V4TgRsc
z@IVf4_5Z>uq+l9Lj)wydnkX}R5JI;T;pv0id7iuzjL|!{hyE=E@sjny96#HmosT01
zx!bG75dRp#u>XcV9g;)Pt{4k{i#-z6Yt??CG^Y4frSGQLN*&INrQQFfPpU$3-wA3Q
zKRz2=WLt#GY4bwRq9e32My&v;%VBChjhB8Key*avEy(Px$kfvhEL5nRJiHz)M7*8d
zEcfVS4GxYrC>7m#%lg>IRqAnrn=1Zx{Z-(Dgmx99s7=-GIq6@{^jk4gHI$EJGWzmE
zN)+-~6mi1Te(z|s)`r=RDcaU0pm|w5VYPX$dOub|
z*d?(?#pX6s9pV$+eY6FH+m%HLBPNyUtf-9(OEsT>ArSFx6h^wbMgd{xPWcc&IePgR}%{!&XmgNQ`#)VGcA3
z*uU7ATts9p2Vv73T*sJ5%UQC|8;thEB)>hJGs0YW!RY!t2clXC$e8@_FqGK~!1l*C
zGP~}ra6_ql((cL-Gu`iEKx-sCF6uPNAb
z>8yZ7n_6hJxizP>q#8svdzfn9nx>te@Cy27K>Tm@2PT{^xkyX4cr)rhf8e}9Adm{?
zShE0&ITI07Thay&2XUMHz@SiAr4Am)j=j+AA=R;2yIC;Kw?;Mearim-(PO_5P~g;L
zobJ0nwjRGm$Hr*1&M1$5jeS!O|3UF;mJ&EcJdd7VE1HZ5omF|RPr24&!%Kd9wQ2-Y
z$i5$qe@a>XrM*!egrG11R{#7TAM3_*;+I@<;=@xubf9=vPdIF!IrPVcJc8otrna*E7tRbu8jZ+W#8pzJ))oAUlKKj7yj}A4Sb=C8H!aIODyj%pPnDwLOSj_XEB{
ziR3l(wbR$@|2fm|v;~b=eUC^{9}2?FMaI$}z``hcv|{t^$&9zkMH}k==WX)o9PiI}
zrOz_R5jW`m=Mw&Ldo8)<8YJ@zHl($FUSXxk1R(dol{(n@l`ZN$TZfgTpZas?1kIc|
zPXyC#WYr1gzexU1-0}29Hbd5L8bvdTM>MD$AGrMS%)AP|bzq7P@{Sg#{K52WS
zm4Kh0zfu+9|CE`MSRza4)|K;kLBqqY0%>tB7KU6X^c^<0NNE5so_lebj~C$j3${hC
z57zuJaF3KN{*M>wTi7*2`SL!q;ped|IzCba>hSrvKC2>m|AfTa+Gs*qBt$x+d2N3ButDJX@}xAq=dX<$ccx08;-kkl2X*aU02_%yY!wor)-=Q
zPYs(I-ihSHWxn!yMXW2fkz38>+QH(MRNV0t5m65=m7ngevp;(@K~oR@(OBO1G1CnWIq^({i|q7
zk6>%dsfBE5Bv49WQm$muB2}(Ia?jYzS%J;pO-LDrB2jZ~aJus<%qI2;m=fHUgBztq
zQA&RiSQEB%uLFWta@GY@=!%bVZ9auYUr(sf2TBT`Lq%3Si=P~JewPoRW`j56Q0t&1
zQyF(+56#k|~{IaSP
zEiF~0iQtJ<(CUuCc4|x|@K>~EzkYbAN>{cm+-^x$e20QN7k=Q`+;~MkhAn}KQBsEa
z+-y`c>JMdTR3m9g{b$_?TTYK+IX#a_MsIol3uRB!9hkd1KK$;%XMbWwDwX8
z=9L;xG%L4s>@<=7=irGBR;8`tQ6IMWK;h|^;>0yIIr*cE!qRiO-4%?v?aiM#-9vnZ
z!;P2>&=-Pu%%=PLd>Iwx*TRK=k7%GK+#2=7;8XN^)9NA?z9{z}j}}?n#Bnxi9dWj7
z{nA|s@cQkp%?CGKX__}nhuR4mY5@meDdZS<#w_#Zvz}GQt#AMac(3RP&$ud&&Jx8b8gQ@6(t%lRcs2_5!
zVLx#C&CQhKmtgB5A49mmP$gbznH0*8F{LlFo^FyX0WEQZfRIAH;>3*j@zJTKyBm~D
z4Gspd)*BU%w1|T}720K7BkwW+V9n3zF2QU{}@-IPjjTMb|inWL?zn%p&adV^n
zAGOweNLCyw1D>Rb8*eh06JPNy)6GvlS$puWCA=vfPUa8%l^v7
z2q&fG>-ccRyyLa6x{rTex9ywv;aP)~0gZhGiVUJMEzwhpexn#Txx27$Xc_$a{g6H$
zhg}BGP0E4ExpyP$ujp8+dX9wzW}n$U*)Yq?(mWm)$%xO3i;*|L+?NZ@ALI)Ekko@rHzo?M6
z!yX42`$U_3(+Y`@k%bBiF$oNoU`%vzW52O;170!gNtF|wpQ*7v`j+pT+c)}b9L1hq
zGqiZO`_9Ok+HN@lCT0#D^V`(c3jIHUO0Nn#3c=S|H|pLH9TV*D>xrXC2FGCr>X65!
z8MArT;;6YL*tX{lcL6zi0%1{6^f2G|@Y%Dr!gi)8E!&o!%kJ)9mtBa@oYF%{DcE$U
zo_KB>UXWX#A4&+t9m7_v_%&tF^X_v;ljfJFYmcC8g#U2uP?Iza+a=XY_Qj~HkhDd5
z-M-0{rlXSzj`_hcOOUf&oru1msXyFFgAzy4r9GUE9i`HwWLWt`esRTz4FKeK=?X6j
zDTd3MhNx3O(~S=@*%~?VjQ5JmK_FSAm6tN{Ni4loNU;k)L^JO)nOPoPqWb}0Y
zotfcYp^kVIXT@sJL_IANYv7ET?~~!spbS3dz_JKSXaxcVGtZhPa(qi%;GUYkSz_cc*i0_)jaBty;i?ID-N=)G5%2^m$o}rs>Rq%?M{deetNswD@h^VN|@|S)=t*
z%Y{GlX`{r()6n9AgrRV7LaVGu4!EoaG?jlpfS7yoyzxmNwA%LtAHWT7fJ{GI#o@Hl
zC+~3?n;q%55f*kcMa_^jMEjMf*onnY-%lgYPqgkX=!9if6&45s79pw%Ln%$`9!(71
zXJG2kH}d4+;LqI>V`A4zDaG!FCntK1!DZz5Ugd+dx^d2E4wN4ujnjIs4zZ*ODu${%
z@i&IWOHv*$Ot$^5IIg>0&$9S0aAG==MFzVcSsvY*7bYzBm^PooL{XZ77F8gvNAb;U
zjrDMK&>KP7+J@B+<#0l`RG7yT{_Q0Z^+=F9EBIV#rteB#?o1n%Rk%0bsmCcvc?h}X26!(1>|de
zQ~uV|EY`faZ@94<8F^gF)doMgilGXVo5vxf^Cq4CjD_EzO-`54K^my@@yzk|V{w99
zw$U3gaJhG8FJg9_&tw;Wj$6CNFG7vqzyNp
zC2q8{A+_wYXxl~}HQ@J213SoGqLm?enQ=1iPB&%S7JQilru!n&AmuZVEJ6kFvEVDq
zO+OZf;wT%M=i-(fUXM7iCcITDR;VRP=CS>(@ZCrVF
ziin;csc7AqV{SgIDwWyl_hKF1ANFu*A9GQVds$G_c{O+TniIu0^voD$qM~-nk{zU7
zck>t9te{Z{WJoC4qbp-Wl<_dojBb^9JDE`Spdq34+fUPZ{m^Jkaj*rhcpC|-dM1RfPFBLB0oHjGZF3byLVm_s^>ZZpKwN3o57r-!;sBL`o(u}YgO7jb4f9>dVhc_!C`XeO*LZFFTVQRAc;OC|w~
zS^b8$BLV2%Wo)&dPB}R{FY3UlbvyRF)Yx;$()Igz+a1jtiifuevqo6u14_4-1ym17Sd&grh%aYy6^&;3T4Td0nm?ZRrNk_q
zXSLVEi9L2cRqf_<5zuy&1^DHbjb&Ef>UGHt((1=qzpJ+$?|=|!V*)eyqKD
ziszvXqNNuuq}C|^{pfx8as!Sk#uA2B+k-T;%r=-hvNHtLmqstDbvuG5!p^54;OD-&
zf{uuJ=c9G_BqlLll6Hp(`}H}%X*zCj>`B_roH*S{GlLdqe%@P__Cy
zZe^Z@!F7>jg3v`pWT|FPC+$gu6OixvAO1#qW=QsHKmRPgJ07DTxVr3CapVm2(R>ub@6sO
zAy!e42Oc5W5{GHE`&(<>9-jAG9X}oK*K-XJC3F0f3W93(=dCZzmT`QczqcA@?92MRMM(8~<`255}CR=By-cC00RMcAmSz{MTe9_2_!e~ok
zHedWP*NpfuQD!S|%zQqw@h#&zFEef&!xE#2h&8gzftG6!-tEcQ)FYwt1O3A)&;
z4~c4|d#%TN9aYDkJ?ejVXv7LozYNlT-U-2^Ywdct!-{vpN9AJm9~)@CkB;yAW{IBW
z7^m1aqA5YZg5ZX-82g2bz)B5DLqgDM!Q{#dUHd-beAe0wVg4LgxqV=J{#~
zWL~0x$Ev_g1u_DQDgsVwCb>N%ZPS%)G7r>;rcxQU;qS7x>6Ml`c=l<3m%B+sEh+-|`ISGSa{t)EPDQPBpI
ze;A!Vk&hVkQn_NPrKtR`)4=xAfC9bA<|9=B0vW@bDSu-G=z+GBb<2}+bs95$cOY+^T;q(=M9Q
zfc+Xbx@keW$EKubbYkU5oX<8rnuK=K5sSzfxv7=LFBNJl)n_uTHJhS$B^WmTK%qI#
zepPFq0Y!7%QtuJ5s*`WSPW#kHC4sPjK7~7y+c&s{uXvfX7`<^wPZ{z1eYE-6$S>1P
zC~Qo9wu&aT>@7}AOP&LHmF-W21faNO^tC8alKNr5Z`<70X^Pd>W!k2+VcTg_=L;Ru4+4bE*&^hpuP=vay*WR?
ztJAlqST@ge)(~9=d)?8)W&P*B-4I!MIqFkPPQdOVKTx^ha|iLGisS>~U^$b!LKEJP
zYT&{JF{V8$tpX{AYM*;g_5Av<{HA!(31oM7-c;ioNs_ZLMJ9p*Ey?+qpbN`QR1K-e
zuF75R7+pYmrH^)!jM>j44~w8DI%?%7j4wunehCZ6AAOP!v$JS;-R4=5N~H|xe5xR>
z2)g@;TmZ#wb8HDvC56RmDZK1{W{PhdTQiMxnM0!
zuZgJi3$JQD$wr=7hn#hP{UkeA|1ng-4apT|j8`}$hP>Ioz?X78hXsY>buiQP2gj_I
zw5eD{_Bq%beLU9S!mgyApC=h_>sP&duugg#1j5Ob)XDucb$kyyXr;Y5iLI1@
z-L=9jp0D*L0-5(HxstonQ&idv@f@koij965)_QWtyXy^TR$lZhoR+exI{b0MHJIL7
zXj;E%d6&r%FslZzSl4`BTY+ZWECv=M4`Wwi#1B{avKxncgw-C9H>dR+$W!OkE+zYX
z1gEx1TYIw+KZby00<9To^?_oHbIpq=c(K5sYFFug7KYE4Nq_ioS9c|f>=X2rFP0ceOKdM#hirRft~AV7saQzE
zHM>Rc1{jMCwb3{0h}FehZ~a{Gw)^>$*~gc*T}|4|K$4tCfC=S6f5I)OP9WS2rC$E^
z=iTTUbX4`6Fm2Y&1UJ9THd!GoJcYIShaJO%Iy%8oxp?88#^+BND}q)l&bIsqQ#S@X
z_~yT~16r>*)t6ingQ49!7k8Xb2zM3fCC`Lwx|&j=!2TRv3DE_10w!~jL$!RLoO^GJ
z!LE{iuUXA{zS#`EAX}gDF*y(z?n5py}GF>kCjukHn5N;ig
zZI=$EePzD3x>rG{8N`1RlA385kz{5*CX@caV^Ftl^vA>xx`JE$0rDv!WKW=ytINkg
zvpwSE8?-_~_>h(^6Y{aewRBoS*gUCkcFpY$PqX@In6gN!bx)k;DHkB$wdbcX2f(L#
z0Dk;B&n8Phs~#<=b;>9&G<<5P;V)p)_qNt*)QoLLXJmD{lu>%!%XtYY^BM?xbxwyv
z$v22R!XJRDgBuGjk?LhS|c%hafn0O48`hSQS%fD;D}*F$p`UGB#=dPS$jGn
zm;y6EX(N2<>fLJrB%i%eT?!BbeKR2KMkhr??hU|LA@3xMo;uVSa>U1vR8e#OhU3K5
zTsY>VzN|MaP3JO1A7EfpQDmdN)zb;29vv#tYp3N>$!6gXY2X#@kVJPqtz@ykcgn(q
z1t$#F!lL!u=u}EL?z3m}AWj*NPR}7IJnHEVr;ld
zGsF+M)ggLHf)ds0D5^;q;0q~!AqPw9R@EM6F(?hc5W*Kyv-o~bP%t{X7?%K10rrl`
z%N+;7!wRbN%3+uMRHiEoH_)$@hsnB%5<*&ZTpBASRy+L`m~k(@NdGf+@@!&6xz(
zO)cIIN|Yh!*2v`UY_PO+pL~GXND@`4sNIxWZT
z<(mcO%NQj2J9QpAdKx81?2d3}DaL_feLma17J*2>Ic`)4HNS3N4uh!6uDVWogdtm^
zA7>cgoVE@jO@SsVC2b0CoSRu&Yr58CPZMI3AcRkj8!
z#qPGIA$+EZjFkh7s8Dg)9H}BAl|U%KSCA>h?DQ%a7gIicNnD`^1-MLB=-3me$#7E7
zdeAeYhCt>uY7CIpH7X($X%K7{2$-~2(;*9!)o*|R@T4;G(8q6xZ9JnM#5+lmyK9s7
z>Q3soT~^KE%=frS!c&|wVw_rsX>n$YEGoo>2BR#Nq??%#Uu~sK)YF?v?Iky)}NIzN?#0dQpXwW2_iyTeNv6iiTmi5
zIoegpGFYsdMDVmonoI
zY`2V^C;c(40x^!t8*dM
z%+;4vP@dCT`DU~1Fz@L@h{cCHfGcpqFvm%+y!X*NkGQAi;Uv8O>3LJh{@zR@U{t*b;0xkc5Y9>%3*##8*M
z?85&9Cun=ABrCF1lpuDRyQh(zaMZ$UM{$M3UjKou2jehRszP}bG;
zO{N@G&1X6_R&B}O^eFo7+yyLQU*rfO?-MZp-cq1R#S7^?!_Loafbz|>yqu=L9Zkd`
z4V}i$sekBW;|xt0-Mnl3jJ9s=al1j>it|H1-V8sp^ttTXFz()2a{Xo}WmY$`ml_Pp9YKo@LUpXg|(sF^Y7Tx0&X
z$=F;T`l#D02Ia{A>}cB0zVs~F=S{E;F}856HjGp08ClFPZSXqagI9jBIKHFY79N-P
zC)kv=IanICuh4N;%U41iR8Hz}F=Ta?-(Rw-_g5MVC_if!0+~rt8!Kj<=0ElP^w|#?
z_Bqn;G)`i}{=wcNNX#DUQ6B1J!cdOvb`vYKi}ad3p;u&q->%qR4Jw-lXr45{8Mn_N
zRPxhH%H3RrT=L2uoi@t!r@l#@?n6QPl%AY^zb}RA95AUKw0x`kNMq*oq9>|d3WAD`
zy*8&@c{R8gT^=c~4=(At3&l#(hrP!ZH_!!5YTNSP6igYN$sca>Dz|awx}E}o8U!UZ
zHcH54TFCDDW7N(w4A+AM1zENm+rPyoD<276oNa!5vvg{TUpz(7E@?_GkI8J^WF(v&
z^kabY&pquFn`YwJoT1w^M&~Y-Tss8>txCrd&_rGq<2`I>rc()&rK#e*I-dY-)h#{T
zc35;0cewBM!E^Hd<-7gJjr58pF0OqfdE%CgF0^(+yza=A|JfyBJE8A|{QXpg>)ed9
z9-k$#(FJWxwW!|n7jo!6r?AO19BW?U?8rv0>|rg{xT7O0)R`L9A0NaFug_7OsnzJw
zKXk@xG!syZ%j3qjV?X2Jcw2otH-0M;iF+;aU;ug%Wz+<|9bK9poGkA-koX4MF!H|E
zxVp+T=ktLgpV43eP-hU7y+{T2lo|IAORH70^Dt2*4}OhGm?~DXIAbh%1vE1)KDHL}
zrzMqy&}oUjUmiEEjbn
zmnITLH+XDl0C)%`eAd*2BXN)omMSJ=EQf9kMT1r4lQr{T^HQ8gTPsd{T$@FlJd;mq
ztYWbn^-0UVTI*E`GxWxUfttCEiWL^uZy;#eOI}?%4?GEMkT#%_iDaGBHeG{7a$JJc
z$i2R-?;?W+FL#ER>``13eU1s01V9@@bhv(}3ej;pNioJRW4O%^_YbCkZMa7kr0tms
zhyTn#&pl)Tl@CwI`bVxKZcjT#^ZFN1_skNX{$|EnT5|)*Rh3_MXD)eN@pCin>xIp|
zbx5`STCFpCM?zn-fLCEA>e%~m?{gEu__!m&L7yNjP27@=H#D3EYQab^#LB<*RZ;x`V`yiqPMZQ#p_PscI*?3
zphCKF-8|7*#T?KMv8!~x9mcFezVfDn&)NOKP?I+c$m~2hVwVX!?aq(N4;85pvIdu=
zbd>2GZLaN!FKX186*S^tCmD==cRJo%uY
zO9DE#EbN0AZa@I{+K;lZfExZh{0Y*Eo)4GbfD`r1L=*=k|_RYVPmcr+-Y8OVN{f>$+QSM>dl7_OQca
z>JXEtvc6Vcoa9ao^k0o`q_2Qere;TY_5uokmt*4Ja)VI!#%jKtkV?yTIXDx|M2tjpL6KG@9Y@IV*1CpRY@sAr+2I*vM-z?
z6a(%}0Z39TKP<}8y&eY&yDlDa@$WEH;WSB)g*&CB;Gq-}*~7e-S`ks5hTue*W-z-#
zy@9vL7nV?CYX1vXOx0<*rOFpb>YKQIU8vgfierQ%`S
zp;^JB4?S>nMxb#Z4^yExCY&tX;^tTxAEbuo5#&6xGcECo!_S&`5>3
z@gYrbb)6{4bZB@xFTy5xC7!~I9xgg!e2@hW*hp4;_$V;k_^u<8(F`|iHCGWu|~Im#@7O<^sG^-EX;Xzq3K~Up1-8c+~)dp=1y(87_YM1&yR-3HM)XSO|yf-=$p@$ud`wmz0L8(lue0YOcDq4kHe7Id_u*Y}kjA?xp>RW2}up+PAXC
zmiL#(Dk^IatUi2*{
zj{a@v{iP`o`xvuZh9RwvFGb4XfR2Lr_j)+W-Z{I%5qTM~@7EY})3%hLQK(bWm=m(iL_`
z{^?YM1XbEDor)w17d#Fc&iesJ>rNVa18N+{8ucZD%)k^|L?uBRDQl>4q4|~5=E%T=|>!CbCxj7TWN4x?jF|9!4bmCm@v|xpx$nV2Aiv(
z!Aun#gE4{o%!*=S%{xZXSb0gQ)=lm^SQo%GHE5KT+7q)SH*{-4>vT0ccT*5}kd}@j
zU>dJ>wGQbST(7S{x-#{r-gT2UN{JW?qkL${bkMq1f4ougD(ezS@R*Sgci8Zv4s1RQ
zgONr!a=*B3G@~}cWKCIg{fDT1UR3btOCay8uFPOy=*XT3-#lGDld3B(cX~mZ$GTTV
z&SXS7sMnnMMoth~`1BBRno7G=VOXqEVvA;2tESl!$q!zV0E+sOdPg-7rLX$*o2Q>l
z^sHbq6d~`O?ZX$S{dcik_{D8Zim{C3(a9sPoFPL-JMmocU~X08kglIU5pr{TWaQKo
zO>$DDuH}Wf&j==reJ+~WG>uW)3CpC-rFkO-a>rKB*~VM=lBe5=u>=a5cqfV=ZPJvE6SaR)j`fX{B4T+iD0Rt%vK7F<(_NFjf
zzIBOHVFKf&XR?mRW1Z&{T(V`kF^Cpn0%S|p{nb~|!7N4Hjpi7ovx#4178^YKIYBvlhUtD&jPJOc%3gZ{x4!7f{TUpeV;FWH@T&r&
zpoMtNw3b%?srblR2oVdsUxPLv7A;-3pEws~M$T%-_#lgXhAU~8c!f-_UG|sczxebW
zqi`n%`q}LV-f+nxEQ@Yc*|2y-vl51;CV;xT*btYs-!5lo4PEYMJOy1cvpUVk(acGE
zXJF7#k0H;k)JRNSpi~56>0%EGWdD^?1YxiqA!TDqoL_|<)$F@u%&VkNwJaJ==#RNb
zKd)H}!ne7Nz=sQaO4ivud`7Lq9+POO6vNPBa&;m%|EiLT}#qLpn9N^k!6<9Hi~
zxmaYray^T^DWNgYm-JeZ!XxGCmWkZvrMn$1<;(l#DB0NtZtVPHC#p0XVn~YIdIvj&
z#sRRI(>I8>^K+x>*WN))o8&JprQauWtjq#U?TeiaQL%dc5#g0+gh^1@`gzZtDzue4
z4fqhn0?1Q|EO0J&Q||YiY(50q<^37*W=ne&W{Y}CH(oaIXW!WwkB3a9PcpO*W7|n#
zn}lXDgWgnlq?CF$MaV)dH|NRQ+sw?s{#48e*p&8^ShHz-7f)oNnes8=PBkovV_GuC
zrB)w4K|8HpT>yBswP<2XX!MmyLOVo?EWCa#qIn~e*xZ)QTt=#YcZf@UYYHH1!
zBT=8aw-9(EQUz1?e3WzhnV_)S6t%7gZHI)=Pcx6FwrDCh@5yF@gBmJ>ADN?8%}h);
zHns?2e(gzbqE@G1%#w1Ssec;n;=QUY18)eu1UyTaf!(OwpK|{u#b>0z`YubqTZx!>
zybtk?7aR{J;CSu%-F?tfw+?6QPrVSo*mypAXMJ6)J@&KxyPaIK9qFI_wzw)B3v;+1
zdT#`R9v&W@CkF=ys5D0>3-uBLLGx;lpobeA4u2gHB$}f$`%8A5LJ$fMMnw@izL3nm
zn;Bs-`CT@WQSOuR50|^`4!p*={s8l|9z2GN+jNRprbj614=U;xVPakQBL!+wi6q49fCZ
z{fcLmC5vvj)b9D)A`J&^0mxjr9@ZI!MoFnBe40Tf^dquNOeX>9m{~e9QplaJT%dS!IeV1Rx-KBgj1N$r62#PyMo$PDz_M^EiXDFP+cp
zl9kaP!VM^MY3iR)%{9`!{E$9Nu1&?)A)q*QbhCalXGYx0_CJYv@P1AmhR_0(sxiWAqMD-A3Koy_ffUOQu)ASrJ-r#r
zFCyj`DHLmWW5E3NpcnHNwHt4Oh@!bs-#srmXhq}kln4J6pZGi><3q*wiKgcrFY+l@
zv~8yUI2+d5NY*ZxjGp+`n|V$a^;R71XnrXsrZ)
zcNpXRvg!_h{72O+OR$QD|J}H@_p{H(YZlC&O2Xp3!#+tQii#
zGTidlMY$ik=;Ln%W>+0$bl5ccBmpzP(*Sl8&{UeY2;i5oT*hFO-~sA=iOZ6BN1a)L
zgRN2(J|op&jb@FGUZ@Seoc?J0yU4)K-nu5gu7)GT7DIk59<28@R3$<&r*NeO%cs5Z
z6_ci_stjUDMuM0#@^m~uMjVmK_$xrA&W)!t$msvHlz7LRv^?P4CBT;L>Ar9}45dTx
znck5}xNu-Fn1oXq5e;jlC#%*AJovUY6c&D@8txcFg=q(ox{*@foCDDnMuNk0$
zb|jyV@rfQ9RPT{2UlV6&mRgSIy;39sGl(c?ETQ}Q8vosM%C6q?Z>IsH{_pdtiFD_w
ztaR{Hy7T2JZINM#Os|P;PfAJQ%_He5S5os9yvT#D*uvp>_`tZJ+Z$z%Bl~CT<~!(X~NJ0>3BlWZu|Fp_d4hNlMibO?YFlHXi-X4-!CFupV?mQ
z+Z+fSoaF)|%|4S4g@JYO>UIYzFawyBEQ#73-&Kb#>+UwNjr#lx2&(ey=YkJfk>gnk
zl4h~x>Q+j^2-!s*v(?`vj5b---g}m|#ICvqD@I%OZwrnXn9U(s6reT@;g-I7#O~G<
zIXq?`Usl#YZM~$fVxPSSAC=p)&J1H={>yE^@WJAQ8$9jjbUlHU^_ijl5fBy87NGo2
z(!O{b^pE(J=?_xGf8}L>ToaKr7fwj7fkOny?|**~zyFgA{m%v_|9>ZP_*aX*4P@S@hoAOG8C
zz3N{7z*&-8YAmUY>J<}2IC02InN=wpZE}CD@{*@9_6?<cA&E@cvKgVi)>5Ny;c^
z&3Pirp(g(*NFY!7)f6GoUdrfoEAzN?zxdBRm#@Qt1mCN!?P5O$x;=e~4nbV{@*8U{N;oml(J?8=>;5~8|X{Nc4mQA3UesArr7O9O3w?v-x>9bg^M9}Jqt|a
zdMJqKQ)31Vvfsk*%h_+W3Tkm5KH+Zm5EVBYaVc*#8%M`K@urJt9ziX4kfCs^OX{`j7GV?FnlUVl;GeKBNIxd?pEy&${g%>E;0sYwDt;VN
zYF=IVb`bfsg?;6g&HhdEpGl7x+f*-4cV?3yKqTD2cnylz(=C7QR-E9x&y4OlF~VgR
z*A0_lfR4pg$ole(@?gs89;qWE0E?yVjHVm8_%P9L;;qkb_c#*3=$f+o{PsJR&^NO^
z3|m7mwVyxn`MVN{IJ1d9$%F2eN6CW2j&07?SwZzf%X%yS`A?xEY
z?H}5h(+LQgq-*Fx#0!DMUSg6L!K(ujusx-2wQ=n4%E&D?re}PP+ZzcXC2X;-@2cbS
zvFNpj8E#ILB7I!5K~X5H#u7OGIHd$M`G%P&{p+7n)=OQw{J%E#X11V(WHxBmg9b$b
z94gEm{z+G_N}iHYLu|@FNe$C2v4hSOzuJn`AQ*6$Ki_D-oFD`sI~ybpHs{;WVF6vv
zL>2=6i@7M$r_9>1!+
z4~D~%A`#P<7IdGPP75i(TQ8I-uWv}@p+NV22VU2>x%}5de|9tCd7ZA0Bp?-O_oUjjqoP6&tfOWy
zHtd!Oxv=H#&SBjP6EpHrd7T_btl7HwMg7yc;Jtf2^maf&4`Av`&5sezqPQ6%e#(&A
zyttO@JL+|ovamZ)#EN@GbfIIQvmk@ZHkG6_^S6pLfOm1U1F`DQ>a?(~*%+hR&twon
z<4I}@#=5$;{>LWx{iKN!#%Our?cmuNm7HD3h2-d_(l*yc%G`X5BUR)8(;GwF=3&Cz
zs?tM_7}2+%(mR*EqI;*J2KU|jzSrwDyYQo!B)^Jy({QBX;vW^(W-i{kT^@mZ*G1XI
zUK+j&YpK+jA;a)N-)Pjb8pbRrp0!b(7oxI->{+AMD9?numkPmliAf`@oED!)wm2k>
z)A_Ts_Cu1YToq--rTm?Q(Oc3PY;!mJ4b;js#bE
z;#Anffbi%hW6Khm#82RA+Y^8WJjd}0%9Yq9VY9bdoo(D$Sm
zzT$@V71zz<67L1?KPBggOu9o{)hF$*?31C^Jzu7uX+|XEG>45d=gOyo3J4`Lq^0Vw
z)N&#T>=zQ)7=nI=_obv}X)x0Ukjh^A&7@4FJ5nsCj}XWEJ}nSJq(ahr(VDw%aq
z#=0w^+{0#=Ttnrb3)=(2-oxh^%-V!KAty>{tBamQPcy9hDl4DPv7WOufOhc
znX92SI{U~8@a@S3FH_w6Y99NKZBkyC1vbRYhSPc+hVp=N7>qld1?|-PJkHdL2TKwh
z0VMkjQw{CM<`?6j)mJ}Q$Bqq;*b}K)i6{!%E6$R{92TTqAv_!BxF1|TS!ZS)9=_9{
z)0-b+IK$ttIK#nZtZ6218h(_Da1jcwz6dwDZY@u`eQb=WNGQd|KYTkO<0&9}@DFO!i(i}om0x22e+3((|VkIkcvR%`gUV~a*#^S8qCP8OwBFmxvyqj+f#lwo1
zJ0^&jA^X{>Ass_b5qTr@gq?B3ZKvASj}PO{kl6Zs+G2WE15Y(!^)i$)jlFpFn8rE%
z^;Ls5OsRIAEp);wP)=2-0H{h4d7~#4?rG!MST+R#N}G^?$SyD(p9tNO@Ifsn74#+~fhreds1Dez{hV%0qCc
z3l`j)JkGIZthF%bXLPkyjw>5Eqo*MaP&kK4ZdaIB1E49IIMu|%Dl}5d*`APh({?jP
zD$QTD}#blrfL
zc`vD9&#mE*?mHqbi5BZfX^m~(0F;;lsZZ}hOztm2?hfg*bb~UHtz34?gNR&$VYPZ
zE%bd?GuABrA#nVOH(4Z=Os;{&V}Pt6Dj}|WhRd@r)WU!{(_qY~4qbdS5MCaO8+S3Y
zzRj-#OVk@v7L#H(jSp7==txv5!k!L-p+JXy5J-zL`wKR4d)!<4#jr+ygw
z%`#LR$@&^db5EcVZ(&*o{F$wc1$CGufK*&2KitBGD+y$9da^`}M|(P;IeylsF`zRY
z?oa=!J+wOs!?dK%s4l5ic!X1_V>tX3zC;mNR_(I0zL($57Mh%zv3l+Lp%@Q5o1RCNMw5geS85tc-4$UNR{B5QJN(5}GpeL&2360*yU2c;xtE~v%81lFC_Dci
z%;Dct)5NSN(KG_h2%^A`c<0iV$MI;z
z^=EMk8_$a#F-MS_b!Ulag()g%o=8I(EJJOU99&rnO%lCgKlLZ%q!L?lL0MH>c$I_l
zbI(}7&Q1y^X7*l{zU-tj(oiE!e@i(SWZ>3dVM37{TECigFdM{hGws*{EFG
z+Dh7ziCt&>{SCiIyLv2$5;A^8ew^mD>(pV9DdAk|ic39HG8nfI*Z;isXqrMVPwCl?
z)7G7W8yi^;1T^HJbj9W9Tak)Tft-i9wOmf{?XVedz-`S}7+BR++?7e0Ezuj)!dXvz0#KT&@zc*8{mvk{<*1a{&isxMG?n=F~u}ksCMDm>Ee5N$tm{r#Yb9kiaSr=S*oCJ!%}<=5L~e~oKRLpX!mQo>i(BFcAWvQ
z4)l*8VKYlu>tmnOHy>*Crd|{W>etBd$42l?RQ$%l#S}aWVF++$UdOCp|>G7zX~?}`A=hY$8c!4Mpx!5b2y()T@F}Yn4}5_
zB|ArG;U^FOus>)#Y0sMy<7NmYTi^0$>EpOa4vm)dPO`jUxuzqp?8@b>TOre;Zc}?u
zg5dJ6&-``?LDyYsm~YmP<}Ek^KS*v^-=gtIjMJQ?ccT<$mrk_rok^nz6y@wwR!byT
z^?h(!_NvGPuj+@W`viS6*?VaIFi$(a-PEOqJx`rYwB@6e{Kae+&qkk9s&>3e3~%z5-hbDy)y5Dhyxzln2^7ZkS&MS{#WoDQ`e-3Ev3hIUU^aSyi=N
zEO<`*QbdH!aCkSR%~q49rj6Dl^frL+1RLr!eIlA7X
zNwODSKcsJbFd7&Ssz42nf+mKOK>`7?cIm`K(Bd+9&o9
z!iw=~jbubKG&+{qcnG9wn`G9k^j2chUP$ntOBMdCV@AVw+!d@6bz!>W^Y&a#33*Vb
z^o=Uqt0Z=onCHkhGak+eKRdg<6~RMQS>>oBGix}#H@DsGL`)&DDzW7&0qm`?KGiub
zRjx?6{+8JGaUQG}KNgmLMWvM-xfCQbwXUZ8V;UGYQNf
zOXL&Xj!EKk<5L~W&#bR)6nJ+5Dg<6G-RKKQe#&xCxs3W|EB7gu?_I1Ry%$ZYeKjU4
zN2FI4k2=?$v`Squ-7ec%q9&uaSytD0A)=>w<96Shm4k}-NC5xnjVf?Lt|sVZ*E6J~Wq
z+CUegjvPCL1+n3qLqCo$3m?R2wBCKF6Bt(id4XKe2yE)tjt0V=Zmno$mDPo4l#pWNx{yR!`4xH=;@cR2Ma!NR*IVytYY&r@i5Z{XnvK!XaeU>qsd7-8KOFV|01y_|+jxgKzrkvAKZ9M)`1mKDJLAVyIe-
zPrj%-EY7*PelzU{rO5Yw9T%RO1D^y!;EY62nN8kqGb)?`H;nvnPfd~!4fej7^T}OR
z3wR1jo~Lmr`j!d*?Ia7CCgQ;
zf#TeSaKJtHkNr^ocGAQgtug>4R83@<75$OstkGCb;1GB@$TF1L#V6BCRlNJzY?e>t
zyv>6klV5O>QxU-Q8}ZCA8a=qzy#L7;PIXwHr_72jX*;SLNYlKgb8A>4pCn-tb6y0{
z*%+@rXxWBJ^3xl^mvxxTxZ0Xaw_lqq&geo^JM{luH;gQo*ucr&?q`qlpGWe3^Nc$Q3+rRD
zV}t&oe3BvX#oc$oIvR?joW|9HJmiF@pHxUtFZ2yE$ndHuVz7T?T0gY(1A^d4>sW0@
zIjQC?gPFK&w2tcrMn;D2B`;?AIyWZ9IZP*5@v)mRx4pTdc?EPv
zyCM?<@gB&sj^H)%W;g0>6}@bC!TboS+%VL?lp%9BNn$q%*qUzLA7&C+BCE2K$3XWc
zul2{$`_ix3LN;E3bTZ0Xl-NeOu?0;$L8Myq^T0*G!H9oE$y#&>Dk$k5m@G?$NsD0T
zO;maaJ%7VD;H1*+ib0`8SRVZvl;|5ywD##hO(-Uo$xTSe5?~^y-~VOQr#9~=&9zfE
zZ*{hCP!Ux(uP{vPP`Jr3w?2xA#J$gT(06vEj5d~@fDAX2`ANpVX2uum6RdOxZ_x}9
zL{fRDtI(MAlRHc4UEI#foK|*YgyTkfRu#RN)9^>Qdd81%@TCRYH_kX1IWIG@8npuM
z?3uIx6gp44@$Fv)KKXg1Mr>3B)vAP`mFnY?g`rR+;Vi~NdnCzEw@=NS@V(YT{AHp+
z@pUrOfJ=pWm$A|I(2t`-^@Gkl9zWK5Twisc!1>vM*O_RLSm0xJh#?WC3%SUUAuf^!
zciB>2!S^GYrrb}d*dQXIrsVFj;k+-J`ZQPEHe;d5ZQ`v6sjTkS#L}`2BU!04dlTIJ
z@`@`r90T=dx?Z*>g5dn0?TYMSOeRrBzX-zPn6WdCpD5*ByE;H8hpn^zsu-1z-QgGn
z40NjQJl^2ND&XeH!3fN;!m+>1)ma_7dvjy)XP-B?Y3`CiTxPl4{wPbzXMM+=Tnjrs
zMrbuY*mcYLXq>tNuTBi%Lu<&zW>tgsKBeCb!HOd|DqIt3gG*teEM#qQ5F~%wu%U7P
z<|k=!F&h%f24qt{TV$Y)a9+Md%GlhI$XBQ;LKaeCiXyahj}l#wN>3Yc8!8BY#7x!2
zgtv5P&r$4mWhK7-l%0{9(!ezx&aouCKc`kaz~)B1B=~UEV&SyvUAst<5U^Wq>_*N_
z%}BkoT7`jbs;TsgtJQt?8$E3CnIc5(Mq%7}JEL*Zg{hc3OC!mIp%l;_TpGT13~802
z&M&jI(l7DKAS%(Vd^e-W+)A!3+>hg)9~&|Hz(W~pa}Yi}2AbfT=M=G&43(DWgcq)K
zHAP4J)#PPFIE2?VHHU6RYFjNgs6lzc%Cg<_WyHqbVO43IW9G||{X@sSY{^Y0l86|}
zRJKtKgezU<6dJIUc#}n$KH3-=zn6vtHbtgD1h3}gtG)*DQxCdCf><2sCwXFP)xa!r
ziiKOm6^@-wH;}~l%028Tqpv#QA;Mn6ld1kYhO2=`12LzDw5VtWHORZBSb0ko-CUBs
zAEVEJyn%WxEbEp?Z^G7a2U))cSERe8ji#qq-0-Ds@x!!lRJ5x|fa@;!!Gv1lM0Opa#y+u@muc_
z1D%oF1}-n7VdsN?GW~YwiD)hDud^JmRtyyDLOF<3U>hCk`uw@d{97GKm&Oc-*1QwNKzAEP#&dNe5tz)J2`g?@$*!mauy+mSm9eeQW}Dw^bP{LkGn?vCus9pLP*3#FrAAU|M<5yi4bRz@
z){kLtOMkS2TNwb2p1Dx?hr4f8>eJcVR0XDR3r?q`NECNF;Swrgde_jh<`C(sgQMPe
zmPEi0=p6Y|D)Xe?CRAFA^n+eOH4!hSOIC|8+~LBLx{z_w9QLiS3bqftLtp4S+l=%@
z{Q1JJg3qkb88woGmNE}6eOr$hAltMvFKOC1F
z3hAp!|K=w84U~A0$oje%A}EsTnFy;zL0ahPckoGCkgYE-YXN-Ucc#Wbc2Oh$ZHVkx
zRit+GT`yGznCgt)EZO%|5KM-tUiTbmi~dTUZ6yeQeWc8JWN~cyuxQ?Oqz5o;rE6)8
z$7bN%*gSHzygQ@Ew}UeE-+n7xzOm}~S)
zxEL>S`o&qx>G$BPUzOq3ETVDA$X8<0*bfRzjy#1W253=naWhsk?S2Op)-+8PLfvCx
z*qi0>`jTKr0W^`Dll6@IXJfxfH!
zmb~kxVT&T$n&GWUl!?IUFH+il$n)t1<4wbTcFsZq7a`~->o*bwaY@-7QVXZ&O!{HS
zys(hw1{l-~-S!obxw@GwDz8e=L=n&nH(^an6G#enp{y8f!t5r}=vUne7iO=7%aaTC
zjUd%YaHO`Ey>!TowZ>Evx2wixTGc!hRYUF^0*Q3ymYiyzUtw{~gBG=?Zj{x-xHmOm
zEv)TXSzECgGmxl{UJNSBQmfYAIj8c6Hf0N*HA2|j)-rF=&*VQ_!}-@QkYh4eMiFe>
z>uwkY66`NFtoP546P-2BSn58JPBLVcF_8~NKw
zJ+`)4W4wR*Ut`xc<-bQ;S>hXV1+nDVm>etN8a~d)g8%F`*b1U7+@Khk4A@MpU>oz4
zyQB8wdi{Z(aw-?d^3e`p-I3Kp
zX-pIwDzAcwpic0C>39vIV;NZ#l%Ex$V%PDP16gH)gc8$BDLa<2aHl0crJ#}uMB5e{
zh`v-$a-`mQX(Rq{Vx#Dq&~k8ygsXER%b{mBJ@1L`2RDYI;+U0*LnYFCUtmgyO2f(l6NT@h$toF}Jhab4)(S4MYCTytyTAcg7urf7vB1&XDVq|ANrs*eMx1mBzmKIrTTe
zbLmVQlfwlLFzp%t+Gfl7c6YeTK&YcU+$-?gL1_2S63P8CR0^2xbd;@hL`!u({5^N^
z^e(A(G<`}{@Ob<5V|Ll<_-4l7ip~aIsk#@p2g2{LyAJw5c9jXX9ZHc!0Irw8W;Cyn
zV~t{+doKzTKG)PaXN+^`;L46`X^3BU^v&e7e`FdOXHF?{fNH;F%n!uBS#N2aTNMSw
z_W?y{lCkYQpYnPNY;5(p}H9Z{dPl$zaE5_t0x}W3sY)ld!p7
zV-h1;&@uPST_1sQe9S)!M}sT3QitbYT~fAe_I9Ry@SiHa*#eO(?9SU?}jwf3v83a#0|v*s&iz1W&3{fthXC>Jld%Mh2groo6pb$mlo2&@#hJY`D!j
zoVEGn$XQ31T5}j(UP7}U*KX01m?or#x@UuLMr||_Ch1ktxsLXe`R%H;?=6Q_XC`=j~@+mrq*Gz4iloydKf93Rj{2I)}|6*
z8%o=qNk6+6Zv!%f=hzYEuxN5Nf-C(-kyPuoTub;L^$m#$Ime>4E8DvwcypYuXR@^P
z({hCRTB?m&NUtwXly<3^aD;?`tpBvMGilI*{-n1uVRv!&mpJ
z_;?_F=)L-%E|$n9_j`w-)nC=zJofG%5IKtyS@HrV#XUXZYPXKR)(F7|F4f|sO4eR<
zeRzIrNwC=CvSZf^;A=F9!DVxKXNVZ<@|W`l{)mObnp1C(R%9@>uZ!&x2RXi<%x!)N
zfnK-K>PEQPcb%}x2mn-U4s@Z|*n2a2Igx~a1K8>|vmD%uHJe^YxK^3igXR=}j#s{zKA91~
z8V*HK_5x8sw9_hA6GR^76R~ad48{F_VrE$99@RAV$_`O%O{bj)wah1b^QE-rZaj4-
z&G(!cI1buZ*3E^}l@AbD=@buky^A8qIh(!Zg~O-K#+@ma1l!{41NYGJ=>&WJwn7_wkshMv{TUfE
zS>2k~dY}72m~FRxb(FX0ntw(|yApM)#E|)rqN=35X^dl48U2?_m9gg&$aC`((^7Bc
zxNfE2ug*Ou)&?zKd(4KlPM9SwT8;38>2?bl$1{e3hUb@-v8dCbE5~-_*yL4OFiOwV
zD<17i=ir2VL#AEEahIBnd!9J2RC_lT5n?dOuYz)4-69Mw04I4w_C!-`!V*An%d09H
zuHL4jf@oYhX54)K0;zJE_Sb3M-a+g(+~?;2zVj|x_C~8^QGPoTbo>W&RVOonlU(}2
zJ0SPx8cu*lbG@bA!#%yt(+>V>D={MHfeM=K&MZ>!DfeOFX;@-?O^;^nRuN}+%0mA=
zbDDJwGAP?Q-*(+8Gq4^u%W~Guu3NeD6FH*(meQ8zSw(Pi>#%1+9bJbxN7`+v2t>czvufN%)E#`6`;S736ZeGi=*zl8NK=)
zWIg+hG?pTW`48%49sh}Win`_3s_zgKExwMY*l3~a)YTKueuj)zHWxI8;KiFv`>Xz;
zj#v9yPJMndD~QDtcfOmn;I$y))gC+(FYSFj&6n&=3~N1g{YHe4c7F+qX0>!Bzy6U!
z+Yz}yn~_3KYq+-7QWp7$sVVL~^qkwTo+9mSZ^LhY&N~Lmh0+!4tM6C=f*uvT#A+bO|Lz7fQkGW6$y8$L7WXunB6~KP%kkg
z-S(XZ_e=su!-++C^ZH6POad$g_#oo0H7?VSM@y*Ut0A{szGKQxk4;s)k`K{wVJsPS
zjSuMW>ld+YSC4GC{-v~)T0@^boo3j7#I%<2Lq#bu8JL_eC5_t7c?ILlb8*{X8RqT7
z-q9T6;1mr`9hOQ$GDAKA4H+b2Sxq1r4cLhYV{_X-AoeWyn;D1g8hv(IKcbIJab7^joBoWl;!#-XpA<6`KFj_>1ibQ*TlQR&6=48a$~`DEb}QZv0eLsq-FGQm
zlUj&UoB&S9>dX7})~Ynu@Qm#53x8OkiocHOFRQ%}J(Vt!N9|T&ujv9@3J77@781Y5
zTJcdVcC}5si=(OlnaOEI4_{}n)*2Jd>2|#=n9iGlEzyVVHlp)Z+%OPu)Kgg!yH4(~
zcVV@+RP)MDDU!pOt+fy#Lowk!*P;tU$$QMIX^xQaduzb
zxgQ8vpW|&k!Wj61$@?Yb)232xrIudmBKRpo|Fp6PE?&LbP&-4R&HH9dEigr2GwSiD
z4#H<@UDuB_@93FwVTK5FsC`9$Mj(9BXU8L??LAwMeqP6#o!7d`J<(p%{{{11gjm3W
zmbd4btAc1{;7yh17~r+~w$w&6lJ*TVgv+OGCXYE$tE+FMy2MTCn0w+m$JxL;l6$<~
zgQn_62l6o;rU#Edkhm5{G4CQfMx0Lo-6a+j7s
z^UZ-EQFeb<5A?_?T^jvF8Ah=wR+!`tPoOzuMcj{L$V^&?Lh{@b76zLGM*;AjS;;Go
z8(LkJh8cw}PI7J#QfGwf;M0u`2IGq+^_wMZ?D`Kpt)IAXW!Z>5o3^Cw44|(r>X0xg
zgxbd?N{j}(8eWoi`E?gYyZ1Zo>pTT?UdwbmJtqZcj=Km%{jwv0ylnQ*6r9^*uPq`j
z4asjP-B3$WVVdl{7dH#+@^X(_bG3hWcGBFYar50>1JMHUh3K($?sn;KGGxiiJ@cQ)LRiXy@VkxcO2qDP2
zkD0zzr=If)gy`5yDSM{gSbM~c`v>OMhYhKf
zLSI(+4#GUIxKvT;jC29L3~8qUMGH|+TsOP}Fo+A}8uR23?Gu9B#JnRb=rocNhHh85Lgk_#0oh2xO(WSMjzICyb5At|gWypGl_*+iRPytU`Z%QwKLB)_ksM
z|I$U(uErwTk}TL8|We*i0VWX4R$oLif?I`nKWY5Da09PhqCUB!u-UO!9d*N
zDX)aB79zuqoB}x~-To4jcnZ3q*71lMHmbJSu~6i2uR@SNl`$pN@Ve+$q^CBwks;~=
z(Lk7LMC}B+oQ{VSOix?U)Dk#
z|HXm->pRHzo7i;5heeE{mjTyy0A3vB`oQ>2PoVJaHqH}Cl-#&)4AvYjwl5fhK_<=o
zrSk*4e--q2+ePkvFCR3ReEaDC@|wHjeG5~Kekc9!LK0tsup1=41__W3{a2wrNI4Rb
zxeaFP0qcJx_5RQ2f5*ao&?>pTADP(M*?sEDz5qM^(-hK6-+YUIRSW#r#{UD5IZI{F
zx9={w8mfcavAEa*z)wrz2xvk={m&2m3mk})#~_VLW|iE+qU~Kp?!Web8os7JFO`mm
z;d!A#<30}a=3dVpRCV_}8Z)%fC8Qm0>pCgJ(!yu$5wR29%vyZqe_|=t-JC*!vhai~
zh-^O7IrwH8P3t!~@&yx}ask8@EvD=~j+(4f6NM6ie
zn`l8vBX6*<&7eC}FIXnUS#4yoEi%zXSOb6g_O8Kt0#>wwa~!R}=e#_gqYVS!LRS!$
z8H3Ve{GPKfVl2$o7GDO|Y1Eu__QE@RuGUK~v&DF8-bg}Zbr`+(O>#We2UVLUn{j3z
z)kUjfy)?a6yg0(3V>5rhS7i?*p%R}K{C$JYs1-%H#ksJxK-MI2m^htTI
z=}!2q1wAy8$W-jt&oMjzBSH)?#XGrwmkEte$383GylMNxb+a-g$dY9E;q|JAL}C-p
zI^jr&v6#6)_x}uGMS3Z?r$hQJxXCxx*FRj={rp@R8F`vb5Ko%!q%8)^Z$a|7^f=Od
zgz=wyH;4(XH>3A(L0Bg8z5r?|DOfJj3fyEPOTMAp_oE~=VMnhJv~O~{xXF&Hd*_1(
z>e)Kp72O-SER;+47Y0QN
zjty=fkF3hV*&;|j`q|Yg8>%s{^BVw
zPM_28nD%zA(joGt3uuTw>ccN#I8C)zk7IXZoLhXVs-=hVOedewm
z`ui{ChL)tARNb94><>@7*zejH7gmA2e!9ReNKLxL#>Ny~y$t>?iAIqLg|T+EjiTsa>0i*3AfJ9T604
zCP`V#&@bBQdQwQ{3UA#}W~!lblV|Ktupm!MPljq>@G&Z{2cPm0kT`Goc9@wWx{37$
z2It@egDbWOvL@YnlV1(ITCkLYxFc{#r-}mpaT-{TtpQY5AL8ew449gBH4#ZBC%X7i
zKP$a!4OC|ke_eV58i+Sx1pSJ}j<(AGM5RT6+v>pR!^T&{y?(zdZX2lYU>XW2
zOEq6vK*p@!DH*Nw7+s$Jcybvhk-;4OnPgI{8vn4js#i&om&Jdc&}cwlJVw`GFvh2M
z+4}5{1SX@L$wqF-P#xrAl0$kyai`zR--3t1L{Y*DS^$d&{%<(c%up=05+vvVm2e~f
zcBpO>xh+Qx`Xxq1_S&3KxOML?@}wGdp;fuvrwNdV`o(GPnfZW{v0U`^z{V#b-@#3i8yXFNzk6L-698|!$z86O}S$M870
zdDD<+c1VoB*;YO;#~Xhz{zo+u>|2*c9s&s}>}O906Jcy8iB;*e;#w2;&r=0BS`Xxr!lTuEMZ$FnhT;h3_IB(W()F#G_OuKrebhOTg=I3dPh(KmiQu9?f8~kkXE_b2vfqO`Hz#H%1e;*}FJbUu4wwM!Z
z_Q4ZZx{Ck;>qa25D~HJ8u(6?u(VrQ0M)qMB2w6&8oGIB{yyH18zKBZHUTBDKPkzrs
zD^o!sA-F%Jem3N%E1rl>mw2{Pg5BYJU1a?j3syQIN8FvbwW-G^cqgW;{=t}GI^fg=
z^&F)CW460g)Mq)eMZ>})X)dtw#8PrYO+#~AUAS#MihD`ow6)tdyhGKuy*NLoRQy$|
zfcQgy^iuQD68l18Q)xL2DLUeA)W}BHuk+q^mqp1*W()}`ssf2n_n}083HhRL%cw*;
zV)M*s)`K$&sQ;6&mtYOSZkxvmZg8vxJby<%1xJB#c^#MWI?jEn${rye11p|{IoDU@
zj`Jm-|Kj-NS$*^fB5h^9KI280p9K-(ywv6As^C2wAySzHR^DtZ4G(JtiJVq?B%KwV
zf+I7<6K!lyb|}?Py}RS;zXhZ7*$gp*MEVEO-fSP3IXga0QwzB<`8Ee8eIM>Z4a$S0
zq=kX6Do-LQfk{ix#EfNL`6hR(rZQhrNA50oE@)%q*B(8PR*iL{X>rVbtAB#RNa9-^
zeSoDaEXUaWk=<3yZ|X+Jkw_5fV3dpdg{aH-t6BJ5ZpzURnczMj#49Ne6O1^(~R_tUcC`z;Es
zR*MbyU?`wx?N{9O7Ow|c_bcB_tc~eg>`hslK&ox#oE3PeBF4f5!8vz9YE^BDlvQT~
zF{{+@D3*1Vl_Jx2P+N;cl&;4=;%4;O!!q)lpU?P~tRuG#DCs9W5ijA?ez<1&W$uqm
zU(e3K#wzvP}{gtw#HuC3jdFPQ%&P?qpJ2nxT)SSQHc-VPwv>(){r`!R8
z(Q!)Ej+Zx*gl4m3ZG$X6UK2kd2S3l*ti!Pu<#SJRKB+J`_tee#OS#LHotB8Pq*z=p
zIb7bLe+^?a+C=*EuG(kXZhK?#o9W`ewG~uQs$G$xDsxoDW*JSS;+1WFq`b&2cEZy{
zTX{_%d8*f;DGoTEsrtt1>seSpC-F17U9kj;<_-I8FM``)t
za5tt{upqsd?8ZbjdkjY}+PiFITIO!wlOgwXVJ6=EdSW}#%w=cN@K{rkhfb5lb(F3Q
zN1+LiJ0-d)ziq5rYZ&{(e%#RA0bWbt8Hu2#yKS1DQerL!8f!Ngu5%%#x3eUS7<3
zi-B*^R8CwY=+;wi76c+97
z6=CDu)Ap+F_T5IuJfiXS97fOu?R8bI6+KodSan!zCik%<*Y|n
zR%#S;R%dV3>Bwnzh4JPgA+@fMY1Lo@*2JVl@j0>2N6tt+!-L&E9jneG(!Kl@IDmVx
zWmc2V?QPXSMze<^$9Fpn&w#)ru-gtrCJqMtlOreK=EhOOiyQ2Dka-dH1SE{Spc^Ql
z<-#mJDIGG|Ju4&4Ve!PbHPU1W%ncPnh6LV6}8WW
z-~1OMKWQ^+x5=ti^8bah^S5q(i|1hROB_U+1ezlCEUc?-feggne?|C&s{h5&uGBZQ
zSQv~x;_<CjyR*s%N&E
zXATuRMf0&m2}IKETV~EpDK8VSFaMHk++8C^6H9K9yImoV;eY^RdS*2%skJ_GmyQB>
zN_YSHm9K#r)~jLX|LOafUIgngl*>A6d0L(DY^8tnj?(*KvX4k=MvifMW%?Cw*)6uv
zlC^GrGEKq*Qg(vJ*kVl?W#Lz*28(q_nzUSNEo2h){g+pB!yY4zp{d)N%|xDrj`5DP
zVv}-$f%xK*%Kf_~lJF+!U8Jlr1L>w4!*}P;g3@e>TCK6%9Ve?zck(&4>rzt#8XMLk
zM`O4@;fCM>6YeF5QTPueBF6JfMI|!vijr33%q?KQ)y`ga9}mRFH)gS$=A2}s(tqP!
zlCwFm5E&G6l8BbG9opVt3y7`7AWILh>M@h
zckU8&h)c>DOh`>(hX4-WEiQO0Km32UY(VC0Wp{4a1FTThq3uZQHhOPuu3SIc>Xp+O}<1
z+qSK@?(?nl+~@mKYgO&6y)z?oM`lD^5tr>${x8+dwF^E!{O`bj!%o@eeExHrRd*~X
z95kRKSlkqu4j0ocdo~`_1%_vuyvmJ38kH!
zB0W|?O*^SED^Xl`)wa@37?A-w6L!dn*nBV?lgFvqMHQ?}OV(Kz_Ug)yWxE2dOY%t@
z>p8}jqxMv$nRpdvF=TI|sg@}4gFPUA1Lzk4XZNPJtV+mM%onU$H2WrC>QbtQO7IM!g_
zrE23XN|r>q8ozI%*+iYafelCrg->}%6JM`mTiU|yVU&Q~tQtogMym+ESYh5a-F5
z*!#0UeXAqsMH0~idQ)}YOPLEKOX&lkgG&D|P)aLtB$!q7voOzp}qrQLlG$@U8U!0&7^5qS^V*8Wh
zkG0Im$IHkMHjB#F=A)UsJi?agR#Ida$Pd^do#vfe+z2VlK|XD3v4t2n++A2cb~
znDP{L4}?!=EwNC;bV`w{p_&#WI;ia`v@J0RI_Y?y!ML$yJgB@nTb}^
z!B6Q)^D0gD>aP6Yb{lJ16C%!!%jzy({S;!xf&+TWkzP!$^P1X}n+ILTkiKMbQ*oE^
zOFrAvwoY*YM%u7Q8%`({xW2TavW;N+(qF4V-GCG?tI90k$UI+{#8(e`*D=6nJ>T#o
z2T0OcwS$~EyyE~aWClv?Vk1Nc9Al!(-->_fL`5|PUGIgY#74|(AsVgVEvf%ycE-pz
zUa=E+I7lb?3h`+64jW^H4KurIi|i+U0e&PFm~z&K#_)83E?5fMth;+JSgvb0c4f+x
zQ=r`%Do3sRozMPT%LfaSqTXO@-%6`Ug2_&oeGpXSA02iqGAmxt%)F+e7b8p(DTu%W
z%Xx-#fLa+3Gsr(lE|gUGrb62e_OM2N0!SZX=7(jLy3RcXxd{P&WVGYI|KkU4YYRS+D
z4mC_fkgSJiT8VrW{4JQ*hO9B6=cihl-8LO@avfk@Fa64pXa|JU@mQA18@Ocukd~ow
z2WBHEhiA|FVdic_zF>?;>Xn_;h3e2Nho}k*tOP`h4`BxCczZ9(^fGHqP<_fm_);0k
z0pr>VrDx9V`dHO)kp2+ko=`+R!d4Nu7^DCoVF2nIGMtxc=O1v(AYBrAH+V~!H73mI
zU?PMT6C3l1eC4zLeW(FCH`%}vx%1#y>g*VrmJR@LE
zS@9VD^hDv2=C}zX%~@)3pZx(4f+z6hb4R2-E-tjt%se)GQm7~tc175G^V8eCuc7{a
z#vbnp+j^v!YB6dZivY?28fk7n~cQpLgAKp~1
zI>&mVC`6wfLMxS5o@IA++1QaDf>}?*7JA%reD`soy9KXcdiCij8fPtpUgf8LQD}PS
zhQ7m@B{_QYD+cBGkA6`+CkaWOsqe38qzT25(*)4%-%!;_%tkFCi*F8=-)}aEQm_RU
zn6qCM>Pz-KrN!Cmil0Q!7om&9_DmK^u{L=u%r|@esh~u97$H9_lX2MO8hy{n4byW~
z$~nPxm!fj$=u71R$MMi-#Gs{I-d8@QJQJt;IC=4GJdJ_K9@!OY$%r$?Cb}0`vtW&A
zu#u2=Y<;70fV!}^(8#cmIb_L@c396ml=OelVsdd)Y(IW)r^W`@eSi3@u6qb|RBXN;
z(UvNd=dqaB(&7}#4+9y1$2q@-tXOdv-f_U1USkiGADFNg7)Y6_%4%~EjXoQ`{34k}h6EP@ZQA;{85j#oO>d$pt
zu+UjF>SZpWJ9XA%pm@bSy5^6q5~zSL23`1*aSWfITj9rm#y
zasdnlzTZ`-M}0y6$PRIP4E@U}Cv7&cf(6TQeDjoY%O
zXi`fa#+;&*jOBIsEOp9Wm3MtXEAjI8Kv$D`4db6lS(B>}3VsJKY_OW2Ei|Z&6gb&i
z(!yS#2}3$7t^84Juh_J-<2$bj5g*$$a2bH$xl@>~p~%12d1YnMA-g|0FN#j`LJpO1
zOY%|Cgw0ZX4tfjMpp!c};j+u>lW%5s;Kp2JKbr!cHmtP;s;borM*acb+!meIm=5We
z*3oP{^Iasn78yzjWqy37W!x-Q6*)g}#k(wVaefnjA*e1XfG90_{lKQ9L$|ynqBn=P
zgs>~$F0mT&Rt|XDr2TTc>PR)Q@y4{2<7zsZY7ol2HvEr{{v(dc#ha~0_&figwM(9i
zFHmrn6F4hYN{;s9WZz_l8Pdk4JeB(mz3tT|bG@iP72XL1UmkZ>p
z$`nRU5Xm|k1!L##;B>CaevO?!4WQqR5O68Ts
z$Qu5rP3EZZa)sw*u}&JFV)zy`JyRmV{!%XxJ;Bl|7D8GrLI{V_KqopW-FGiUF(Xiy
z)mdB~ve6nAvWt`R>_k0hN;1!^$zD~>k@H&Nqu#h%sLZDx2zye)M8vk5OmO?PYeMzLXCnDX>E9&*P;#^JJKu%3wsNK
zRAPclUei5bB8+1mZ3CARQ2$zQSG*19`>nrI)2mYr2D+ASFmzl2V*0TBa2EgNF!aE*
zDm%zPSLwAX)%QCzTq?V38}>&wc)r$x7WMX6J01rS)6uktc++1~b%Z$7&UdCrk+Ge+!yRz5%#ID@j{Fl!B5*zoD;m@FD3U}2N
z`@p>5gsBZYbI7GJKmj5$%<@>;Fgde(Ge-IR5Y&)9Yfo6s2P<;4qeIP8Tbz2BNd+1P
zX*1K2xxkM{4sE8BUX`?{3QxX0iue->s6d0mNq>f!UdqQ7)caX59XNrNn_Zl+dLEH*4&}^7Nw#d$T_U@8CxG)_=g1_rIvTU7yD
z(kr#GjPkltzOwzS{27W;`DHibXDwiThoV?E+~hb{8yuqyP>`Z1-{*i3M_b739Hv{A
z+7rQd#w1$}sOgmUtB<2wsVwhjx9O@6E+f7S&X#MU`i9@f8^Dy%=Z;L~G8b~%tLA^K
z99!y52xq)qP_;W_l8XXz2T8~F`9w?NLT7XzzK5cV7n1d*2!?_I$pv}mzw?MX&bFq$
zCJ-_8*@7lQqFuf4+_VPTm}9a&@fY1^?CDOyPRQOKVZb{7`ppw0@U!w}rZf~tior&i
zcvYQXD`S>h4?V&)O^?*Ek|mzDj5@GpVqnKMOXSW;VL@TX-|THHbk;ilxvd&My`MYH
zxVKw6g~?@t0RPS2-JI3(9LQEMj75sj$nt{#`A;wMD~
zvV!E)N4;rtMp*DX{z23)k;(&j6DA|OK&uzfftkge&+PUAOd&(4p7<~IKuQoH9^4Rm
ztu7$limu>1G>n2d>NEZLpeH}c)EG1D!tw3RT0NwO9*plaqZ=&Br_hwa^qC#LVePpj
zSTyJz5sMeT$5ZP~lXT6d@SqEB;+g4Vq^)!&m8q2?y1N`>f1s_ptrG_o%V98E<+w(I
z_z)vsV=#N%BOJL;5j<3bR!0>$Y0}w)rhOcRXlZPv&t9!JO4%_+17mtokj5v?QjZam2p3vmce^Rz}C^EnF$F?P&Ky9d6
zO}kJti%}&C49rA`r0hA1LwEe>0A*4d|F|aknU{QiV_D;E>OfNQL6v^2dpu|%aaxX^
zs`U1R;p0z^wO+{_xfsf#<_SN0IMP3XCidKM0-#bzgJ?{ukYlowh1BS&CCaVrfpynf
z;o;$AK8+AvMSJUA!AR&d_qkT|#vviZyf`}TXd@HUyz;OM5@)-unU|rz!)APATl49v
zB97)_59$wAeGY1=eiIZ(oPn)jGjy=imMVg(_>cj9`XG(vGs*TaC1DV9<@>Y7Z7Q#0
znUL8!p}&3D;=zWL3>sGLhf=q6eQ|T$g^TKY%I)_R9Rg1Xf?IG+et#cMIz)mWA5`S^
zr86XqS}fJO?@>|YT>pN#0cmtW5`X`*oNq0!jI^pch(@Y3nZt#5!>mc
zyvt}Xc;O;d>W4lFqT1A}wDIsX$@4#`#WuUP75P@jFc5;1rgI3SB>uH^Qoca%G@^9s
z%&yJFJ}pVfk@IQyA;X!0lr7wh0W
ztd&hbiOGb`iojg6r|!jQus|p0H+ZiWXY}bKkDcA
z(p))1LmbV$+~zpDIWpB~;BFr3Sp1E6iSgAe6B9#ph=ZSgp6X&$-l37?2MV}
zK9@F}eQ|a=qXJi3+(V48l^-Mxdz+Cdv%;o*$7q>TjAQ6y-Ie%7PksHK73F#qO?Y>;
zZ%8vl&@~J2EP|adIatyqN7lut%`J$hz|8!3DhJ=y5!4{m_kda@NYpAE&nW8|f$&LJ
z>A@A1b$CAt=OE9}mcC5b6ISrzV2-&nTK$~4B|blY9A5DSojjnd`5HYwpkSf$as~#A
zOGbgVQ408UL3Lt)x!KdqjV*jC=jO{-`N{a4@S@%R>o}<{{^mjk&!9EDvg*_pK8nJ}
zGC97Il{LpKy{}R~L0-N)vtO1YG@UIKheA^aJy{%wIkZ$+=7xT>3PCU
z|4@ZSQ5tS^RjD_ly{(s(E+!diRp;q$Yg6_>6u07;d+yr_*62}K?c6?+;;!AcK6X6~
zZ*CT@Vd>Ewf;dk4sOm!!Zyj#MyX@Dz+>FiSO21rdPWbMt!Z}-n{Z1C)3Cc#niR7DO
zd8Lkx@zBKS!Nr)_QqBfkkJPdlsuzmfkuo4^aeMkh0E5X>f-MmY
zntuBaK=cn#eC}-LD-JVIq{{xlbh|MQ5BtnHx_V7?+<)z5i)5t+!~;xVH?x@ty2Cj}
zVJc?)mEKKZJ+dw5uVz7YG+|LnY0r%Crv9T3tO&651_sNLy8MqOeRj2uO&{g+lJ{{0
z50YMCe+r>|QpBRI?z7cC1kz+aT=eT&P4mNrJ5+~-YE}E${WDzhH^Cag
z8$EOWbB$53AJEr}fl7sFyklB<_3%R<_>
zA}#S{F%xD0O+}m(*08wo<<(%@RG@t%^aLF;>quPp`&Gv^_Z!9g)8+oZit2t-X4i)*
zzu9LDXl|asu*~}ru+Nq!fdKoS&*r{c;AhIh8FqD-`3|{Pq2CC+mw7u2q5
zHWM7G7Rg3sp7K0(Zwc1kn*0>++hm$7@nO!zd9OgNB^j&oxCKAx_BFv#Mw36`RzYD-
zwbAvkO=qF(lEa*X(YsDq653k+8m#{^F>dE7-aMiLEHN5Jyb}cdkDKLIIbRCvk0#>}<~&_no+{NF
z{A$5VlxQo%k#JUy@#OgtRt7HT0hdN7%dQVPs&`|Ki)sND@?K=7p0vMW0tMm@++7#Ba&C)-%?XI{ZY3Z&Z4?_hZ0xS7ChMYm{GTDw3-
z`b33s)`O^#p$FN^t`~eEf~I3vAjyG82skubMcM
zHf=C~?gf;H)n*X*5cxPp!2gJu2pRfE5Fx4^8-Vpg>_1=rXVCw@8CXRg#`%v3{@;&5
z@*)4{Z~xQMg(Rd-{Qooo3(P|!j%NGsUH)?|8ya|?`G0r$&$Sa#m$nUT-GPH3ucyOfqe9PwGQIT98#S%%9`KIUKM)KWU*
zT;86}l>ePB0m+cMBk6+!f_fJB0??E+t!Qk;XNy%FnNB^(@s;={gc>(4X6jbdR<1Ap
zuatXMC;|PUh!2R)R5z%ej@w^1xjR*hECI>r8jejf#$u|FuMEWgs541B;30!d}3^Jy^5g|GI2-QE5^(^R}hyRcGp~7Y>
z+vXMZOo53L7>p7lEOW@3@#5c69((p{z4LLKmG2Ak<{z}Mz7kOvZwihtQ$O6e6y^rL
z;J;bEXb?^5_F0bQ<#RwhUpye!uJ(pkcut;^%oDkl`ujdwZZGI|4=m{A)w6=OmKQAI
zV*-0*4G)TLM}?J(O-{VQd$K*j?dd-ME|~dS1fR42Mzl9XJ-EpC?QF8*fT#|>_J6N#6ylI==8TR)3C33Mfub2N_Xftxnu|vyL%?+@ik~f||0s3-386l}KL~Nm|6&37
zAb@)h<8G`JZMGG0tBncvM+T|)Q?1pzz>EKTr;n4O*)m}9i5B#~uU2a%w8<1k*xfES
z`(Lol5o7^pbSD$Yv@7$H>DaxPxR$&R@+7;6{WP}9!sM_S<i33MxY!%I~Ki>$zIPw>AHeJ`cRw4bVgn{rQg%
z%4fJ<<9d`(@)svsI|S4md3a%&e`?Z4f`nqj-K^9;x^*
zC44PEnF$`kxcRyS=@DKYA>j_+91)r`4r$KpDSHNWb@*P~`48n?(CTlT9L3Xz_w_Lg
zm8!~rua68TSG>x88r&s@kt{!dzSqRHq;`#UexUh4-RNOf<2txX{0#fAp3!ys&$2D3
zkDju*R{}9{;YE{^!!>wlnKTw3{i&XEMdtiTP{Pku;e%ji<))+k`*?
z!V157Q=}8x5NSnZb5+0E$<-&XY>U@j&H0RPO&P9VC{1Fyl<#>U8P0aiF#1Tw2!yec
zq%%2YdK@EAuKls$ba+7&N2of~bG~v$H2pM4&M$e!-*|JO6G7-z13%&LBUaic9QLP=
z*N{hOw;5(}0=&5Sm9$&(L#5Yr3TfHU<3R2gtj}pKR59!_&4n!U1D+wTx}U?MWHn0s
z6?U*JBO^;dH$l7i2z8>UIKf?T`%RoF^%)mI9$>R2wfili{SS#oA|qcK-Z5!m5jqX3
z{9i6B(>W5q^m;ntuiuYiEhhM0eVopq#lGJnt-!4-3cUOhXn=>PNTG-La
zuAtvyEmjz+ORM>)p}Tx>KDV5lKC<8pPW`dC8jtY&hqiAn_#gyxPb9Fo%b0>?k=p~d
za8iFtu^ZKC#ml#RWa$3{ze}Dy2W~wodczhoYEJ*WI?$3wsMqum1#9LCBiNTQQ%=Vb
z_9f7|kBA_W57CqHj%~{l!q_}9jGj>7uOPR5HJlrl*_Lnbw{FHFYN);o5*r>W5oNyF
zB)-02I%ooO;rDaOMPL9+KtBaCG(DUj!Xq4lmcNwwG9lTT6oee0WtvA*Md=s$gD?FO
z$&y)rO}-yBvHQ`{a$cNe*{@M2nKN;b)$5W<5XA`L
z9U@u&jK7uu?6*HULXy5Au%>&J22L+TQdw;wX#n)hF5uZT9;F+_mDXF
zY{Mxmlq&{@8~qCY{2`#A(dI(FF(KF$U;Hk4Sqoob$Aa#VdboK+Empd+CqI3f+y~#(czNo_)($GYb!WL7nd|*9
z$77OyD!FtXrj`>HGu@UjUg>EJKX<&aNiUNF>D*Xpo?PZfb06Qs4TfHY;rIRd;0)@&Zwh2nqqfw6%^9$2phFlJ(&FGGq`Q5O1df)dSfaHX?*)A`O
z365{Rh;5`}J)1@}%3E-k4#+lxh4ri-_>*nY^6E1LLYwVqWJ`DgpBRD~UeA{Vy(Wq^=k0(Zt&!1tgi?jvs<(TC^)|cyC+oo7>wxQ(@8Af?
z;(P+SfqgXwtc4)2(NPVk!fQH?F6nYFYPv@@W8MmJN)+3ALu;4ZoUrN*xNv&!I1lGlr&=ru@{-%l;e!RW*OgP2;vgQXX}zDAc!sm(aL8-C9c)M
zTj#4C&9o8OOHa;gt&Uk*K;z#yt0aXcL*ccBEwDzfL0>})d{aky{O%jYh}LCVrZVBl
zA00+kPeO#lfJ|n!eykJSo-n7CnD^Y@y!;rZe0^_*@WcS_8IRqZTpP({9q7~TVJ$(r
z!Xi~6W^EX3O$LOXF#8@jdzmf-SJXZZO{PcCUl_c9Xl6}GiNP~-_7_deJfvkDy*tae
z`G)(dVZpsG*|`MATHzDlZyA
zE@dGiON>s^bX{>8ebZ_ER$&TN(s?_b+X1X6q}u6J^%T$eQ~B6K1{a%gzF6338SOn?NL2l$||&OWJbsg$7b{rxP)-IT6|C
zx6E+wzgr_iP?k8p`iIWEQAbZvC(c)`R%YV33|c+z`+hjZrboPrKq`n~CkV
zCkL{hlC$?<;cJ#o)a-fjMZDK1Q{+~%ho#%BWLZn7PMx6#_htLZlFcGx0AVgz0s))p3V~JGwddlfB&pS;H6CeD*)3Sd&+n%
z;^zxuLRc8^gT^*LNeh*d>r3E|3$5XX;XNM}x9UqZ`aOSRr_~#cxuJ=9aQ7DK
z*v)s8wbr8KP^mW<84V_lo9_L)H*&X|rhFdBKY)y0wI7((4XDO*NIO$D^(Ji>z0L@s4%w@ux(;OC;{hvddEEvSAyw1W_^D;2%TJz
zs