From 647e27cefa12bcccdc88b1e5d8d9c70c0117e6b6 Mon Sep 17 00:00:00 2001 From: zazabap Date: Tue, 31 Mar 2026 16:13:42 +0000 Subject: [PATCH 1/5] docs: add design spec for proposed reductions Typst note Covers 9 reductions: 2 NP-hardness chain extensions (#973, #198), 4 Tier 1a blocked issues (#379, #380, #888, #822), and 3 Tier 1b blocked issues (#892, #894, #890). Co-Authored-By: Claude Opus 4.6 (1M context) --- ...6-03-31-proposed-reductions-note-design.md | 125 ++++++++++++++++++ 1 file changed, 125 insertions(+) create mode 100644 docs/superpowers/specs/2026-03-31-proposed-reductions-note-design.md diff --git a/docs/superpowers/specs/2026-03-31-proposed-reductions-note-design.md b/docs/superpowers/specs/2026-03-31-proposed-reductions-note-design.md new file mode 100644 index 000000000..9ce7a1a90 --- /dev/null +++ b/docs/superpowers/specs/2026-03-31-proposed-reductions-note-design.md @@ -0,0 +1,125 @@ +# Design: Proposed Reduction Rules — Typst Verification Note + +**Date:** 2026-03-31 +**Goal:** Create a standalone Typst document with compiled PDF that formalizes 9 reduction rules from issue #770, resolving blockers for 7 incomplete issues and adding 2 high-leverage NP-hardness chain extensions. + +## Scope + +### 9 Reductions + +**Group 1 — NP-hardness proof chain extensions:** + +| Issue | Reduction | Impact | +|-------|-----------|--------| +| #973 | SubsetSum → Partition | Unlocks ~12 downstream problems | +| #198 | MinimumVertexCover → HamiltonianCircuit | Unlocks ~9 downstream problems | + +**Group 2 — Tier 1a blocked issues (fix + formalize):** + +| Issue | Reduction | Current blocker | +|-------|-----------|----------------| +| #379 | DominatingSet → MinMaxMulticenter | Decision vs optimization MDS model | +| #380 | DominatingSet → MinSumMulticenter | Same | +| #888 | OptimalLinearArrangement → RootedTreeArrangement | Witness extraction impossible for naive approach | +| #822 | ExactCoverBy3Sets → AcyclicPartition | Missing algorithm (unpublished reference) | + +**Group 3 — Tier 1b blocked issues (fix + formalize):** + +| Issue | Reduction | Current blocker | +|-------|-----------|----------------| +| #892 | VertexCover → HamiltonianPath | Depends on #198 (VC→HC) being resolved | +| #894 | VertexCover → PartialFeedbackEdgeSet | Missing Yannakakis 1978b paper | +| #890 | MaxCut → OptimalLinearArrangement | Placeholder algorithm, no actual construction | + +## Deliverables + +1. **`docs/paper/proposed-reductions.typ`** — standalone Typst document +2. **`docs/paper/proposed-reductions.pdf`** — compiled PDF checked into repo +3. **Updated GitHub issues** — #379, #380, #888, #822, #892, #894, #890 corrected with verified algorithms +4. **One PR** containing the note, PDF, and issue updates + +## Document Structure + +``` +Title: Proposed Reduction Rules — Verification Notes +Abstract: Motivation (NP-hardness gaps, blocked issues, impact analysis) + +§1 Notation & Conventions + - Standard symbols (G, V, E, w, etc.) + - Proof structure: Construction → Correctness (⟹/⟸) → Solution Extraction + - Overhead notation + +§2 NP-Hardness Chain Extensions + §2.1 SubsetSum → Partition (#973) + §2.2 MinimumVertexCover → HamiltonianCircuit (#198) + §2.3 VertexCover → HamiltonianPath (#892) + +§3 Graph Reductions + §3.1 MaxCut → OptimalLinearArrangement (#890) + §3.2 OptimalLinearArrangement → RootedTreeArrangement (#888) + +§4 Set & Domination Reductions + §4.1 DominatingSet → MinMaxMulticenter (#379) + §4.2 DominatingSet → MinSumMulticenter (#380) + §4.3 ExactCoverBy3Sets → AcyclicPartition (#822) + +§5 Feedback Set Reductions + §5.1 VertexCover → PartialFeedbackEdgeSet (#894) +``` + +## Per-Reduction Entry Format + +Each reduction follows the `reductions.typ` convention: + +1. **Theorem statement** — 1-3 sentence intuition, citation (e.g., `[GJ79, ND50]`) +2. **Proof** with three mandatory subsections: + - _Construction._ Numbered algorithm steps, all symbols defined before use + - _Correctness._ Bidirectional: (⟹) forward direction, (⟸) backward direction + - _Solution extraction._ How to map target solution back to source +3. **Overhead table** — target size fields as functions of source size fields +4. **Worked example** — concrete small instance, full construction steps, solution verification + +Mathematical notation uses Typst math mode: `$V$`, `$E$`, `$arrow.r.double$`, `$overline(x)$`, etc. + +## Research Plan for Blocked Issues + +For each blocked reduction: + +1. **Search** for the original reference via the citation in Garey & Johnson +2. **Reconstruct** the correct algorithm from the paper or from first principles +3. **Verify** correctness with a hand-worked example in the note +4. **Resolve** the blocker: + - #379/#380: Clarify that the reduction operates on the decision variant; note model alignment needed + - #888: Research Gavril 1977a gadget construction for forcing path-tree solutions + - #822: Research the acyclic partition reduction from G&J or construct from first principles + - #892: Chain through #198 (VC→HC→HP); detail the HC→HP modification + - #894: Search for Yannakakis 1978b or reconstruct the gadget + - #890: Research the Garey-Johnson-Stockmeyer 1976 construction + +If a reference is unavailable, construct a novel reduction and clearly mark it as such. + +## Typst Setup + +- Standalone document (not importing from `reductions.typ`) +- Uses: `ctheorems` for theorem/proof environments, `cetz` if diagrams needed +- Page: A4, New Computer Modern 10pt +- Theorem numbering: `Theorem 2.1`, `Theorem 2.2`, etc. +- No dependency on `examples.json` or `reduction_graph.json` (standalone) +- Compile command: `typst compile docs/paper/proposed-reductions.typ docs/paper/proposed-reductions.pdf` + +## Quality Criteria + +Each reduction must satisfy: +1. **Math equations correct** — all formulas verified against source paper or hand-derivation +2. **Provable correctness** — both directions of the proof are rigorous, no hand-waving +3. **Algorithm clear** — detailed enough that a developer can implement `reduce_to()` and `extract_solution()` directly from the proof +4. **From math to code verifiable** — overhead expressions match the construction, worked example can be used as a test case + +## PR Structure + +- Branch: `feat/proposed-reductions-note` +- Files: + - `docs/paper/proposed-reductions.typ` (new) + - `docs/paper/proposed-reductions.pdf` (new, compiled) +- No code changes — this is a documentation-only PR +- Issue updates done via `gh issue edit` (not in the PR diff) From aa5735372b0318515b98998c3a7919643cc7da1e Mon Sep 17 00:00:00 2001 From: zazabap Date: Wed, 1 Apr 2026 05:26:21 +0000 Subject: [PATCH 2/5] feat: add verify-reduction skill for mathematical verification of reductions MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit New skill: /verify-reduction End-to-end pipeline that takes a reduction rule issue and produces: 1. Typst proof (Construction/Correctness/Extraction/Overhead + YES/NO examples) 2. Python verification script (7 mandatory sections, ≥5000 checks, exhaustive n≤5) 3. Lean 4 lemmas (non-trivial structural proofs required) Follows issue-to-pr conventions: creates worktree, works in isolation, submits PR. Strict quality gates (zero tolerance): - No "trivial" category — every reduction ≥5000 checks - 7 mandatory Python sections including NO (infeasible) example - Non-trivial Lean required (rfl/omega tautologies rejected) - Zero hand-waving in Typst ("clearly", "obviously" → rejected) - Mandatory gap analysis: every proof claim must have a test - Self-review checklist with 20+ items across 4 categories Developed and validated through PR #975 (800K+ checks, 3 bugs caught) and tested on issues #868 (caught wrong example) and #841 (35K checks). Co-Authored-By: Claude Opus 4.6 (1M context) --- .claude/CLAUDE.md | 1 + .claude/skills/verify-reduction/SKILL.md | 460 +++++++++++++++++++++++ 2 files changed, 461 insertions(+) create mode 100644 .claude/skills/verify-reduction/SKILL.md diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md index 27ce2026c..659825237 100644 --- a/.claude/CLAUDE.md +++ b/.claude/CLAUDE.md @@ -26,6 +26,7 @@ These repo-local skills live under `.claude/skills/*/SKILL.md`. - [propose](skills/propose/SKILL.md) -- Interactive brainstorming to help domain experts propose a new model or rule. Asks one question at a time, uses mathematical language (no programming jargon), and files a GitHub issue. - [final-review](skills/final-review/SKILL.md) -- Interactive maintainer review for PRs in "Final review" column. Merges main, walks through agentic review bullets with human, then merge or hold. - [dev-setup](skills/dev-setup/SKILL.md) -- Interactive wizard to install and configure all development tools for new maintainers. +- [verify-reduction](skills/verify-reduction/SKILL.md) -- End-to-end verification of a reduction rule: generates Typst proof (with YES+NO examples), Python verification script (7 mandatory sections, ≥5000 checks, exhaustive n≤5), and Lean lemmas (non-trivial required). Iterates until all checks pass. Creates worktree + PR. - [tutorial](skills/tutorial/SKILL.md) -- Interactive tutorial — walk through the pred CLI to explore, reduce, and solve NP-hard problems. No Rust internals. ## Codex Compatibility diff --git a/.claude/skills/verify-reduction/SKILL.md b/.claude/skills/verify-reduction/SKILL.md new file mode 100644 index 000000000..9adff5f62 --- /dev/null +++ b/.claude/skills/verify-reduction/SKILL.md @@ -0,0 +1,460 @@ +# Verify Reduction + +End-to-end skill that takes a reduction rule issue, produces a verified mathematical proof with computational and formal verification, iterating until all checks pass. Creates a worktree, works in isolation, and submits a PR — following `issue-to-pr` conventions. + +Outputs: Typst proof entry, Python verification script, Lean lemmas — all at PR #975 quality level. + +**This skill is STRICT. Cutting corners produces reductions that get rejected during review.** + +## Invocation + +``` +/verify-reduction 868 # from a GitHub issue number +/verify-reduction SubsetSum Partition # from source/target names +``` + +## Prerequisites + +- `sympy` and `networkx` installed (`pip install sympy networkx`) +- Both source and target models must exist in the codebase (`pred show `) +- For Lean: `elan` installed with Lean 4 toolchain + +## Process + +```dot +digraph verify { + rankdir=TB; + "Parse input" [shape=box]; + "Create worktree" [shape=box]; + "Read issue" [shape=box]; + "Study models" [shape=box]; + "Write Typst proof" [shape=box]; + "Compile PDF" [shape=box]; + "Write Python script" [shape=box]; + "Run script" [shape=box]; + "All pass?" [shape=diamond]; + "Fix proof + script" [shape=box]; + "Enough checks?" [shape=diamond]; + "Enhance script" [shape=box]; + "Add Lean lemmas" [shape=box]; + "Lean builds?" [shape=diamond]; + "Fix Lean" [shape=box]; + "Self-review (HARSH)" [shape=box]; + "Create PR" [shape=box]; + "Report" [shape=doublecircle]; + + "Parse input" -> "Create worktree"; + "Create worktree" -> "Read issue"; + "Read issue" -> "Study models"; + "Study models" -> "Write Typst proof"; + "Write Typst proof" -> "Compile PDF"; + "Compile PDF" -> "Write Python script"; + "Write Python script" -> "Run script"; + "Run script" -> "All pass?"; + "All pass?" -> "Enough checks?" [label="yes"]; + "All pass?" -> "Fix proof + script" [label="no"]; + "Fix proof + script" -> "Run script"; + "Enough checks?" -> "Add Lean lemmas" [label="yes"]; + "Enough checks?" -> "Enhance script" [label="no"]; + "Enhance script" -> "Run script"; + "Add Lean lemmas" -> "Lean builds?"; + "Lean builds?" -> "Self-review (HARSH)" [label="yes"]; + "Lean builds?" -> "Fix Lean" [label="no"]; + "Fix Lean" -> "Lean builds?"; + "Self-review (HARSH)" -> "Create PR"; + "Create PR" -> "Report"; +} +``` + +--- + +## Step 0: Parse Input and Create Worktree + +### 0a. Parse input + +```bash +REPO=$(gh repo view --json nameWithOwner --jq .nameWithOwner) +ISSUE= +ISSUE_JSON=$(gh issue view "$ISSUE" --json title,body,number) +``` + +### 0b. Create worktree + +```bash +REPO_ROOT=$(pwd) +BRANCH_JSON=$(python3 scripts/pipeline_worktree.py prepare-issue-branch \ + --issue "$ISSUE" --slug "verify--" --base main --format json) +BRANCH=$(printf '%s\n' "$BRANCH_JSON" | python3 -c "import sys,json; print(json.load(sys.stdin)['branch'])") +WORKTREE_JSON=$(python3 scripts/pipeline_worktree.py enter --name "verify-$ISSUE" --format json) +WORKTREE_DIR=$(printf '%s\n' "$WORKTREE_JSON" | python3 -c "import sys,json; print(json.load(sys.stdin)['worktree_dir'])") +cd "$WORKTREE_DIR" && git checkout "$BRANCH" +``` + +If already inside a worktree, skip creation and use the current branch. + +## Step 1: Read Issue and Study Models + +```bash +gh issue view "$ISSUE" --json title,body +pred show --json +pred show --json +``` + +Extract: construction algorithm, correctness argument, overhead formulas, worked example, reference. + +If the issue is incomplete, use WebSearch to find the original reference. + +## Step 2: Write Typst Proof + +Append to `docs/paper/proposed-reductions.typ` (or create a standalone `proposed-reductions-.typ` if the main file is on another branch). + +### MANDATORY structure + +```typst +== Source $arrow.r$ Target + +#theorem[...] + +#proof[ + _Construction._ ... + _Correctness._ + ($arrow.r.double$) ... + ($arrow.l.double$) ... + _Solution extraction._ ... +] + +*Overhead.* (table) + +*Feasible example.* (YES instance, fully worked) + +*Infeasible example.* (NO instance, fully worked — show WHY no solution exists) +``` + +### HARD requirements + +- **Construction**: numbered steps, every symbol defined before first use +- **Correctness**: genuinely independent ⟹ and ⟸ — NOT "the converse is similar" +- **No hand-waving**: ZERO instances of "clearly", "obviously", "it is easy to see", "straightforward" +- **No scratch work**: ZERO instances of "Wait", "Hmm", "Actually", "Let me try" +- **TWO examples minimum**: one YES instance (satisfiable/feasible) and one NO instance (unsatisfiable/infeasible). Both fully worked with numerical verification. +- **Example must be non-trivial**: the example must have ≥ 3 variables/vertices. A 1-variable or 2-vertex example is too degenerate to catch bugs. + +Compile: +```bash +python3 -c "import typst; typst.compile('.typ', output='.pdf', root='.')" +``` + +## Step 3: Write Python Verification Script + +Create `docs/paper/verify-reductions/verify__.py`. + +### ALL 7 sections are MANDATORY + +```python +#!/usr/bin/env python3 +"""§X.Y Source → Target (#NNN): exhaustive + structural verification.""" +import itertools, sys +from sympy import symbols, simplify # Section 1 is NOT optional + +passed = failed = 0 + +def check(condition, msg=""): + global passed, failed + if condition: passed += 1 + else: failed += 1; print(f" FAIL: {msg}") + +def main(): + # === Section 1: Symbolic checks (sympy) — MANDATORY === + # At minimum: verify overhead formula symbolically for general n. + # For algebraic reductions: verify key identities. + # "The overhead is trivial" is NOT an excuse to skip this section. + + # === Section 2: Exhaustive forward + backward — MANDATORY === + # n ≤ 5 MINIMUM for all reduction types. + # n ≤ 6 for identity/algebraic reductions. + # Test ALL instances (or sample ≥ 300 per (n,m) if exhaustive is infeasible). + + # === Section 3: Solution extraction — MANDATORY === + # For EVERY feasible instance: extract source solution from target, + # verify it satisfies the source problem. + # This is the most commonly skipped section. DO NOT SKIP IT. + + # === Section 4: Overhead formula — MANDATORY === + # Build the actual target instance, measure its size fields, + # compare against the overhead formula. + + # === Section 5: Structural properties — MANDATORY === + # Even for "trivial" reductions, verify at least: + # - Target instance is well-formed (valid graph, valid formula, etc.) + # - No degenerate cases (empty subsets, isolated vertices, etc.) + # For gadget reductions: girth, connectivity, widget structure. + + # === Section 6: YES example from Typst — MANDATORY === + # Reproduce the exact numbers from the Typst proof's feasible example. + + # === Section 7: NO example from Typst — MANDATORY === + # Reproduce the exact numbers from the Typst proof's infeasible example. + # Verify that both source and target are infeasible. + + print(f"Source → Target: {passed} passed, {failed} failed") + return 1 if failed else 0 + +if __name__ == "__main__": + sys.exit(main()) +``` + +### Minimum check counts — STRICTLY ENFORCED + +| Type | Minimum checks | Minimum n | Strategy | +|------|---------------|-----------|----------| +| Identity (same graph, different objective) | 10,000 | n ≤ 6 | Exhaustive ALL graphs | +| Algebraic (padding, complement, De Morgan) | 10,000 | n ≤ 5 | Symbolic + exhaustive | +| Gadget (widget, cycle construction) | 5,000 | n ≤ 5 | Construction + formula + structural | +| Composition (A→B→C) | 10,000 | n ≤ 5 | Exhaustive per step | + +**There is no "trivial" category.** Every reduction gets at least 5,000 checks and n ≤ 5 exhaustive testing. + +## Step 4: Run and Iterate (THE CRITICAL LOOP) + +```bash +python3 docs/paper/verify-reductions/verify__.py +``` + +### Iteration 1: First run + +Run the script. Fix any failures. Re-run. + +### Iteration 2: Check count audit — STRICT + +Print this table and fill it in honestly: + +``` +CHECK COUNT AUDIT: + Total checks: ___ (minimum: 5,000) + Forward direction: ___ instances tested (minimum: all n ≤ 5) + Backward direction: ___ instances tested (minimum: all n ≤ 5) + Solution extraction: ___ feasible instances tested + Overhead formula: ___ instances compared + Symbolic (sympy): ___ identities verified + YES example: verified? [yes/no] + NO example: verified? [yes/no] + Structural properties: ___ checks +``` + +If ANY line is below minimum, enhance the script and re-run. Do NOT proceed. + +### Iteration 3: Gap analysis — MANDATORY + +List EVERY claim in the Typst proof. For each, state whether it's tested: + +``` +CLAIM TESTED BY +"Universe has 2n elements" Section 4: overhead formula ✓ +"Complementarity forces consistency" Section 3: extraction ✓ +"Clause subset is non-monochromatic" Section 2: forward direction ✓ +"No clause is all-true or all-false" Section 2: backward direction ✓ +... +``` + +If any claim has no test, add one. If it's untestable, document WHY. + +## Step 5: Add Lean Lemmas — STRICT REQUIREMENTS + +### HARD requirement: at least one NON-TRIVIAL lemma + +`n + m = n + m := rfl` does NOT count. A "non-trivial" lemma must satisfy at least one of: + +1. **Uses a Mathlib tactic beyond `rfl`/`omega`**: e.g., `simp`, `Finset.sum_union`, lattice operations +2. **States a structural property**: e.g., "complementarity subsets partition the universe into pairs" +3. **Formalizes the key invariant**: e.g., "NAE-satisfying ↔ 2-colorable hypergraph" + +If Mathlib genuinely lacks the infrastructure (no Hamiltonian paths, no DAG quotients), write the strongest lemma you CAN prove and document what WOULD be proved with better Mathlib support. + +### Examples of acceptable vs unacceptable Lean lemmas + +**Unacceptable (trivial arithmetic):** +```lean +theorem overhead (n m : ℕ) : n + m = n + m := rfl -- proves nothing +theorem universe (n : ℕ) : 2 * n = 2 * n := rfl -- proves nothing +``` + +**Acceptable (structural):** +```lean +-- Uses Mathlib's lattice theory to prove a graph-structural fact +theorem complement_partition (G : SimpleGraph V) : G ⊔ Gᶜ = ⊤ := sup_compl_eq_top + +-- Formalizes the key definition used in the proof +def IsNAESatisfying (assignment : Fin n → Bool) (clause : Finset (Fin n × Bool)) : Prop := + ¬(∀ l ∈ clause, ...) ∧ ¬(∀ l ∈ clause, ...) + +-- Proves the overhead formula requires actual computation +theorem overhead_nontrivial (n m : ℕ) (h : m > 0) : + 2 * n + (n + m) > 2 * n := by omega -- at least uses a hypothesis +``` + +### Build and verify + +```bash +cd docs/paper/verify-reductions/lean +export PATH="$HOME/.elan/bin:$PATH" +lake build +``` + +## Step 6: Self-Review — THE HARSHEST STEP + +Before declaring verified, run through this checklist. **Every item must be YES.** If any is NO, go back and fix it. + +### Typst proof + +- [ ] Compiles without errors +- [ ] Has Construction with numbered steps +- [ ] Has Correctness with independent ⟹ and ⟸ paragraphs +- [ ] Has Solution extraction +- [ ] Has Overhead table with formula +- [ ] Has YES example (feasible, ≥ 3 variables/vertices, fully worked) +- [ ] Has NO example (infeasible, fully worked with explanation of WHY infeasible) +- [ ] Zero instances of "clearly", "obviously", "it is easy to see" +- [ ] Zero instances of "Wait", "Hmm", "Actually", scratch work +- [ ] Every symbol defined before first use + +### Python script + +- [ ] 0 failures +- [ ] ≥ 5,000 total checks +- [ ] Section 1 (symbolic) present and non-empty +- [ ] Section 2 (exhaustive) covers n ≤ 5 minimum +- [ ] Section 3 (extraction) tests EVERY feasible instance +- [ ] Section 4 (overhead) compares formula vs actual for all tested instances +- [ ] Section 5 (structural) has at least one non-trivial check +- [ ] Section 6 (YES example) reproduces Typst example numbers exactly +- [ ] Section 7 (NO example) reproduces Typst infeasible example exactly +- [ ] Gap analysis performed — every Typst claim has a corresponding test + +### Lean + +- [ ] Builds without errors (warnings OK) +- [ ] At least one non-trivial lemma (not just `rfl` or `omega` on a tautology) +- [ ] Every `sorry` has a comment explaining WHY + +### Cross-consistency + +- [ ] The Python script's `reduce()` function implements EXACTLY the Typst construction +- [ ] The Python script's `extract_solution()` implements EXACTLY the Typst extraction +- [ ] The overhead formula in Python matches the Typst overhead table +- [ ] The examples in Python match the Typst examples (same numbers, same instances) + +## Step 7: Report + +``` +=== Verification Report: Source → Target (#NNN) === + +Typst proof: §X.Y + - Construction: ✓ (N steps) + - Correctness: ✓ (⟹ + ⟸) + - Extraction: ✓ + - Overhead: ✓ + - YES example: ✓ (N vars/vertices) + - NO example: ✓ (N vars/vertices, reason: ...) + +Python: verify__.py + - Checks: N passed, 0 failed + - Sections: 1(sympy) 2(exhaustive) 3(extraction) 4(overhead) 5(structural) 6(YES) 7(NO) + - Forward: exhaustive n ≤ K + - Backward: exhaustive n ≤ K + - Gap analysis: all claims covered + +Lean: ReductionProofs/Basic.lean (or .lean) + - Non-trivial lemmas: N + - Trivial lemmas: M + - Sorry: J (with justification) + +Bugs found: +Iterations: N rounds + +Verdict: VERIFIED / OPEN (with reason) +``` + +## Step 8: Commit, Create PR, Clean Up + +### 8a. Commit + +```bash +git add docs/paper/.typ docs/paper/verify-reductions/verify_*.py \ + docs/paper/verify-reductions/lean/ReductionProofs/*.lean +git add -f docs/paper/.pdf +git commit -m "docs: /verify-reduction # — → VERIFIED + +Typst: Construction + Correctness + Extraction + Overhead + YES/NO examples +Python: N checks, 0 failures (exhaustive n ≤ K, 7 sections) +Lean: M non-trivial lemmas + +Co-Authored-By: Claude Opus 4.6 (1M context) " +``` + +### 8b. Push and create PR + +```bash +git push -u origin "$BRANCH" +gh pr create --title "docs: verify reduction # — → " --body "..." +``` + +### 8c. Clean up worktree + +```bash +cd "$REPO_ROOT" +python3 scripts/pipeline_worktree.py cleanup --worktree "$WORKTREE_DIR" +``` + +### 8d. Comment on issue + +```bash +gh issue comment "$ISSUE" --body "verify-reduction report: VERIFIED (PR #)..." +``` + +## Quality Gates — NON-NEGOTIABLE + +A reduction is **VERIFIED** when ALL of these hold: + +- [ ] Typst compiles, has all mandatory sections including YES and NO examples +- [ ] Zero hand-waving language +- [ ] Python has 0 failures AND ≥ 5,000 checks +- [ ] All 7 Python sections present and non-empty +- [ ] Exhaustive n ≤ 5 minimum +- [ ] Solution extraction verified for all feasible instances +- [ ] Overhead formula matches actual construction +- [ ] Both Typst examples reproduced by script +- [ ] Gap analysis shows all Typst claims tested +- [ ] At least 1 non-trivial Lean lemma +- [ ] Cross-consistency between Typst and Python verified + +**If even ONE gate fails, the reduction is NOT verified. Go back and fix it.** + +## Common Mistakes — ZERO TOLERANCE + +| Mistake | Consequence | +|---------|-------------| +| Lean lemma is just `rfl` or `omega` on a tautology | Rejected — add structural lemma | +| No symbolic checks (Section 1 empty) | Rejected — add sympy verification | +| Only YES example, no NO example | Rejected — add infeasible instance | +| n ≤ 3 or n ≤ 4 "because it's simple" | Rejected — minimum n ≤ 5 | +| "Passed on first run" without gap analysis | Rejected — perform gap analysis | +| Example has < 3 variables | Rejected — too degenerate | +| Script has < 5,000 checks | Rejected — enhance exhaustive testing | +| Extraction not tested | Rejected — add Section 3 | +| Typst proof says "clearly" | Rejected — rewrite without hand-waving | + +## Integration + +- **After `add-rule`**: invoke `/verify-reduction` before creating PR +- **After `write-rule-in-paper`**: invoke to verify paper entry +- **During `review-structural`**: check verification script exists and passes +- **Before `issue-to-pr --execute`**: pre-validate the algorithm + +## Reference: PR #975 Quality Level + +Target quality defined by PR #975: +- 800,000+ total checks, 0 unexpected failures +- 3 bugs caught through iteration loop +- Every script has forward + backward + extraction + overhead + example +- Non-trivial Lean: `G ⊔ Gᶜ = ⊤` via `sup_compl_eq_top` +- Failures marked OPEN honestly with diagnosis From 83e39318d06456163edfc3434c4c579ed553e753 Mon Sep 17 00:00:00 2001 From: zazabap Date: Wed, 1 Apr 2026 05:34:17 +0000 Subject: [PATCH 3/5] style: add YAML frontmatter + professional tone to verify-reduction skill MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Added frontmatter (name, description) matching other skills' convention - Toned down aggressive language ("ZERO TOLERANCE", "THE HARSHEST STEP", "NON-NEGOTIABLE") to professional but firm language - All quality gates unchanged — same strictness, better presentation Co-Authored-By: Claude Opus 4.6 (1M context) --- .claude/skills/verify-reduction/SKILL.md | 21 ++++++++++++--------- 1 file changed, 12 insertions(+), 9 deletions(-) diff --git a/.claude/skills/verify-reduction/SKILL.md b/.claude/skills/verify-reduction/SKILL.md index 9adff5f62..beecc5d46 100644 --- a/.claude/skills/verify-reduction/SKILL.md +++ b/.claude/skills/verify-reduction/SKILL.md @@ -1,11 +1,14 @@ +--- +name: verify-reduction +description: End-to-end verification of a reduction rule — generates Typst proof, Python verification script (≥5000 checks), and Lean lemmas, iterating until all checks pass. Creates worktree + PR. +--- + # Verify Reduction End-to-end skill that takes a reduction rule issue, produces a verified mathematical proof with computational and formal verification, iterating until all checks pass. Creates a worktree, works in isolation, and submits a PR — following `issue-to-pr` conventions. Outputs: Typst proof entry, Python verification script, Lean lemmas — all at PR #975 quality level. -**This skill is STRICT. Cutting corners produces reductions that get rejected during review.** - ## Invocation ``` @@ -212,9 +215,9 @@ if __name__ == "__main__": | Gadget (widget, cycle construction) | 5,000 | n ≤ 5 | Construction + formula + structural | | Composition (A→B→C) | 10,000 | n ≤ 5 | Exhaustive per step | -**There is no "trivial" category.** Every reduction gets at least 5,000 checks and n ≤ 5 exhaustive testing. +Every reduction gets at least 5,000 checks and n ≤ 5 exhaustive testing regardless of perceived simplicity. -## Step 4: Run and Iterate (THE CRITICAL LOOP) +## Step 4: Run and Iterate ```bash python3 docs/paper/verify-reductions/verify__.py @@ -258,7 +261,7 @@ CLAIM TESTED BY If any claim has no test, add one. If it's untestable, document WHY. -## Step 5: Add Lean Lemmas — STRICT REQUIREMENTS +## Step 5: Add Lean Lemmas ### HARD requirement: at least one NON-TRIVIAL lemma @@ -300,7 +303,7 @@ export PATH="$HOME/.elan/bin:$PATH" lake build ``` -## Step 6: Self-Review — THE HARSHEST STEP +## Step 6: Self-Review Before declaring verified, run through this checklist. **Every item must be YES.** If any is NO, go back and fix it. @@ -411,7 +414,7 @@ python3 scripts/pipeline_worktree.py cleanup --worktree "$WORKTREE_DIR" gh issue comment "$ISSUE" --body "verify-reduction report: VERIFIED (PR #)..." ``` -## Quality Gates — NON-NEGOTIABLE +## Quality Gates A reduction is **VERIFIED** when ALL of these hold: @@ -427,9 +430,9 @@ A reduction is **VERIFIED** when ALL of these hold: - [ ] At least 1 non-trivial Lean lemma - [ ] Cross-consistency between Typst and Python verified -**If even ONE gate fails, the reduction is NOT verified. Go back and fix it.** +If any gate fails, go back and fix it before declaring the reduction verified. -## Common Mistakes — ZERO TOLERANCE +## Common Mistakes | Mistake | Consequence | |---------|-------------| From d09823d860b117f4248b5b1bdc6f13ecc74ac033 Mon Sep 17 00:00:00 2001 From: zazabap Date: Wed, 1 Apr 2026 06:04:36 +0000 Subject: [PATCH 4/5] feat: adversarial multi-agent verification in verify-reduction skill MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Replaces Lean-required gates with adversarial second agent: - Step 5: Adversary agent independently implements reduce() and extract_solution() from theorem statement only (not constructor's script) - Step 5c: Cross-comparison of both implementations on 1000 instances - Lean downgraded from required to optional - hypothesis property-based testing for n up to 50 - Quality gates: 2 independent scripts ≥5000 checks each + cross-comparison Design rationale (docs/superpowers/specs/2026-04-01-adversarial-verification-design.md): - Same agent writing proof + test is the #1 risk for AI verification - Two independent implementations agreeing > one + trivial Lean - Lean caught 0 bugs in PR #975; Python caught all 4 Co-Authored-By: Claude Opus 4.6 (1M context) --- .claude/skills/verify-reduction/SKILL.md | 302 +++++++++++++----- ...6-04-01-adversarial-verification-design.md | 145 +++++++++ 2 files changed, 372 insertions(+), 75 deletions(-) create mode 100644 docs/superpowers/specs/2026-04-01-adversarial-verification-design.md diff --git a/.claude/skills/verify-reduction/SKILL.md b/.claude/skills/verify-reduction/SKILL.md index beecc5d46..8981aa8d4 100644 --- a/.claude/skills/verify-reduction/SKILL.md +++ b/.claude/skills/verify-reduction/SKILL.md @@ -1,13 +1,13 @@ --- name: verify-reduction -description: End-to-end verification of a reduction rule — generates Typst proof, Python verification script (≥5000 checks), and Lean lemmas, iterating until all checks pass. Creates worktree + PR. +description: End-to-end verification of a reduction rule — generates Typst proof, constructor Python script (>=5000 checks), and adversary Python script (>=5000 independent checks), iterating until all checks pass. Creates worktree + PR. --- # Verify Reduction -End-to-end skill that takes a reduction rule issue, produces a verified mathematical proof with computational and formal verification, iterating until all checks pass. Creates a worktree, works in isolation, and submits a PR — following `issue-to-pr` conventions. +End-to-end skill that takes a reduction rule issue, produces a verified mathematical proof with computational verification from two independent implementations, iterating until all checks pass. Creates a worktree, works in isolation, and submits a PR — following `issue-to-pr` conventions. -Outputs: Typst proof entry, Python verification script, Lean lemmas — all at PR #975 quality level. +Outputs: Typst proof entry, constructor Python verification script, adversary Python verification script — all at PR #975 quality level. ## Invocation @@ -18,9 +18,9 @@ Outputs: Typst proof entry, Python verification script, Lean lemmas — all at P ## Prerequisites -- `sympy` and `networkx` installed (`pip install sympy networkx`) +- `sympy`, `networkx`, and `hypothesis` installed (`pip install sympy networkx hypothesis`) - Both source and target models must exist in the codebase (`pred show `) -- For Lean: `elan` installed with Lean 4 toolchain +- Optional: `elan` with Lean 4 toolchain (for formal lemmas — not required) ## Process @@ -33,16 +33,19 @@ digraph verify { "Study models" [shape=box]; "Write Typst proof" [shape=box]; "Compile PDF" [shape=box]; - "Write Python script" [shape=box]; - "Run script" [shape=box]; + "Write constructor script" [shape=box]; + "Run constructor" [shape=box]; "All pass?" [shape=diamond]; "Fix proof + script" [shape=box]; "Enough checks?" [shape=diamond]; "Enhance script" [shape=box]; - "Add Lean lemmas" [shape=box]; - "Lean builds?" [shape=diamond]; - "Fix Lean" [shape=box]; - "Self-review (HARSH)" [shape=box]; + "Dispatch adversary" [shape=box]; + "Run adversary" [shape=box]; + "Adversary pass?" [shape=diamond]; + "Cross-compare" [shape=box]; + "Verdict table" [shape=diamond]; + "Investigate discrepancy" [shape=box]; + "Self-review" [shape=box]; "Create PR" [shape=box]; "Report" [shape=doublecircle]; @@ -51,20 +54,23 @@ digraph verify { "Read issue" -> "Study models"; "Study models" -> "Write Typst proof"; "Write Typst proof" -> "Compile PDF"; - "Compile PDF" -> "Write Python script"; - "Write Python script" -> "Run script"; - "Run script" -> "All pass?"; + "Compile PDF" -> "Write constructor script"; + "Write constructor script" -> "Run constructor"; + "Run constructor" -> "All pass?"; "All pass?" -> "Enough checks?" [label="yes"]; "All pass?" -> "Fix proof + script" [label="no"]; - "Fix proof + script" -> "Run script"; - "Enough checks?" -> "Add Lean lemmas" [label="yes"]; + "Fix proof + script" -> "Run constructor"; + "Enough checks?" -> "Dispatch adversary" [label="yes"]; "Enough checks?" -> "Enhance script" [label="no"]; - "Enhance script" -> "Run script"; - "Add Lean lemmas" -> "Lean builds?"; - "Lean builds?" -> "Self-review (HARSH)" [label="yes"]; - "Lean builds?" -> "Fix Lean" [label="no"]; - "Fix Lean" -> "Lean builds?"; - "Self-review (HARSH)" -> "Create PR"; + "Enhance script" -> "Run constructor"; + "Dispatch adversary" -> "Run adversary"; + "Run adversary" -> "Adversary pass?"; + "Adversary pass?" -> "Cross-compare" [label="yes or no"]; + "Cross-compare" -> "Verdict table"; + "Verdict table" -> "Self-review" [label="verified"]; + "Verdict table" -> "Investigate discrepancy" [label="discrepancy"]; + "Investigate discrepancy" -> "Write constructor script"; + "Self-review" -> "Create PR"; "Create PR" -> "Report"; } ``` @@ -147,7 +153,7 @@ Compile: python3 -c "import typst; typst.compile('.typ', output='.pdf', root='.')" ``` -## Step 3: Write Python Verification Script +## Step 3: Write Constructor Python Verification Script Create `docs/paper/verify-reductions/verify__.py`. @@ -261,51 +267,164 @@ CLAIM TESTED BY If any claim has no test, add one. If it's untestable, document WHY. -## Step 5: Add Lean Lemmas +## Step 5: Adversary Verification -### HARD requirement: at least one NON-TRIVIAL lemma +The adversary step provides independent verification by a second agent that implements the reduction from scratch, using only the Typst proof as specification. This catches bugs that the constructor's own tests cannot find (confirmation bias, shared implementation errors). -`n + m = n + m := rfl` does NOT count. A "non-trivial" lemma must satisfy at least one of: +### 5a. Dispatch adversary agent -1. **Uses a Mathlib tactic beyond `rfl`/`omega`**: e.g., `simp`, `Finset.sum_union`, lattice operations -2. **States a structural property**: e.g., "complementarity subsets partition the universe into pairs" -3. **Formalizes the key invariant**: e.g., "NAE-satisfying ↔ 2-colorable hypergraph" +Launch a subagent with the following prompt template. The adversary must not see the constructor's Python script — it reads only the Typst proof. -If Mathlib genuinely lacks the infrastructure (no Hamiltonian paths, no DAG quotients), write the strongest lemma you CAN prove and document what WOULD be proved with better Mathlib support. +**Adversary prompt:** -### Examples of acceptable vs unacceptable Lean lemmas +```` +You are an adversary verifier for a mathematical reduction proof. -**Unacceptable (trivial arithmetic):** -```lean -theorem overhead (n m : ℕ) : n + m = n + m := rfl -- proves nothing -theorem universe (n : ℕ) : 2 * n = 2 * n := rfl -- proves nothing -``` +Your goal: independently implement and test the reduction described in the Typst +proof below, trying to find bugs. You have no access to the constructor's +implementation. Write your own from scratch based solely on the mathematical +specification. + +## Input + +Typst proof file: docs/paper/proposed-reductions.typ (section on → ) +Issue: # + +## Your task + +1. Read the Typst proof carefully. Extract: + - The construction algorithm (how to build the target instance) + - The correctness argument (forward and backward directions) + - The solution extraction procedure + - The overhead formula + - The YES and NO examples -**Acceptable (structural):** -```lean --- Uses Mathlib's lattice theory to prove a graph-structural fact -theorem complement_partition (G : SimpleGraph V) : G ⊔ Gᶜ = ⊤ := sup_compl_eq_top +2. Create `docs/paper/verify-reductions/adversary__.py` with: + - Your own `reduce()` function implementing the construction from scratch + - Your own `extract_solution()` function implementing solution extraction + - Your own `is_feasible_source()` and `is_feasible_target()` validators + - Exhaustive testing for n ≤ 5 (forward + backward + extraction) + - Overhead formula verification + - Reproduction of both Typst examples (YES and NO) + - Property-based testing using `hypothesis` (at least 2 strategies) + - Minimum 5,000 total checks --- Formalizes the key definition used in the proof -def IsNAESatisfying (assignment : Fin n → Bool) (clause : Finset (Fin n × Bool)) : Prop := - ¬(∀ l ∈ clause, ...) ∧ ¬(∀ l ∈ clause, ...) +3. Use `hypothesis` for property-based testing. Example strategies: + ```python + from hypothesis import given, settings + from hypothesis import strategies as st --- Proves the overhead formula requires actual computation -theorem overhead_nontrivial (n m : ℕ) (h : m > 0) : - 2 * n + (n + m) > 2 * n := by omega -- at least uses a hypothesis + @given(st.lists(st.integers(0, 1), min_size=3, max_size=8)) + @settings(max_examples=500) + def test_roundtrip(assignment): + # Build source from assignment, reduce, check equivalence + ... + ``` + +4. Run the script. Report pass/fail counts and any bugs found. + +5. Do NOT read or import from `verify__.py`. Your implementation + must be independent. + +## Output format + +Print at the end: +``` +ADVERSARY: → : N passed, M failed +BUGS FOUND: ``` +```` -### Build and verify +### 5b. Run adversary script ```bash -cd docs/paper/verify-reductions/lean -export PATH="$HOME/.elan/bin:$PATH" -lake build +python3 docs/paper/verify-reductions/adversary__.py ``` +### 5c. Cross-comparison + +After both scripts have run, compare their `reduce()` outputs on a shared set of instances. Create and run this comparison inline: + +```python +#!/usr/bin/env python3 +"""Cross-compare constructor and adversary implementations.""" +import sys +sys.path.insert(0, "docs/paper/verify-reductions") + +from verify__ import reduce as constructor_reduce +from adversary__ import reduce as adversary_reduce + +# Also import feasibility checkers from both sides +from verify__ import is_feasible_source, is_feasible_target +from adversary__ import ( + is_feasible_source as adv_is_feasible_source, + is_feasible_target as adv_is_feasible_target, +) + +def normalize(target_instance): + """Convert target instance to a canonical hashable form for comparison. + Adapt this to the specific target problem type.""" + # For graph problems: sorted edge list + vertex count + # For formula problems: sorted clause list + # For set problems: frozenset of frozensets + return tuple(sorted(str(x) for x in target_instance)) + +agree = disagree = 0 +feasibility_mismatch = 0 + +# Generate shared test instances (adapt to source problem type) +import itertools +for n in range(3, 6): + for instance in generate_all_instances(n): # problem-specific generator + c_target = constructor_reduce(instance) + a_target = adversary_reduce(instance) + + # Compare structural equivalence + if normalize(c_target) == normalize(a_target): + agree += 1 + else: + disagree += 1 + print(f" DISAGREE on instance {instance}") + print(f" Constructor: {c_target}") + print(f" Adversary: {a_target}") + + # Compare feasibility verdicts + c_feas = is_feasible_target(c_target) + a_feas = adv_is_feasible_target(a_target) + if c_feas != a_feas: + feasibility_mismatch += 1 + print(f" FEASIBILITY MISMATCH on {instance}: " + f"constructor={c_feas}, adversary={a_feas}") + +print(f"\nCross-comparison: {agree} agree, {disagree} disagree, " + f"{feasibility_mismatch} feasibility mismatches") +if disagree > 0 or feasibility_mismatch > 0: + print("ACTION REQUIRED: investigate discrepancies before proceeding") + sys.exit(1) +``` + +Adapt the `normalize()` function and instance generator to the specific source/target problem types. + +### 5d. Verdict criteria + +Use this table to determine the outcome. All three signals must be considered together: + +| Constructor | Adversary | Cross-comparison | Verdict | Action | +|-------------|-----------|-----------------|---------|--------| +| Pass | Pass | Agree | Verified | Proceed to Step 6 | +| Pass | Pass | Disagree | Suspect | Both produce valid but structurally different targets. Investigate whether both are correct reductions (e.g., isomorphic gadgets) or one has a latent bug. Resolve before proceeding. | +| Pass | Fail | Agree | Adversary bug | Review adversary script for implementation errors. If adversary misread the Typst spec, fix spec clarity and re-run adversary. | +| Pass | Fail | Disagree | Suspect | Constructor may have a bug masked by its own tests. Investigate the disagreeing instances manually. | +| Fail | Pass | Agree | Constructor bug | Fix constructor script, re-run from Step 4. | +| Fail | Pass | Disagree | Suspect | Investigate both — the agreeing instances may be coincidental. | +| Fail | Fail | Agree | Proof bug | The reduction itself is likely wrong. Re-examine the Typst proof. Return to Step 2. | +| Fail | Fail | Disagree | Proof bug | Same as above — shared failures with structural disagreement indicate a fundamental problem. | + +When the verdict is "Suspect," the resolution is to manually inspect the disagreeing instances until the root cause is identified, then loop back to the appropriate step. + ## Step 6: Self-Review -Before declaring verified, run through this checklist. **Every item must be YES.** If any is NO, go back and fix it. +Before declaring verified, run through this checklist. Every item must be YES. If any is NO, go back and fix it. ### Typst proof @@ -320,7 +439,7 @@ Before declaring verified, run through this checklist. **Every item must be YES. - [ ] Zero instances of "Wait", "Hmm", "Actually", scratch work - [ ] Every symbol defined before first use -### Python script +### Constructor Python script - [ ] 0 failures - [ ] ≥ 5,000 total checks @@ -333,18 +452,31 @@ Before declaring verified, run through this checklist. **Every item must be YES. - [ ] Section 7 (NO example) reproduces Typst infeasible example exactly - [ ] Gap analysis performed — every Typst claim has a corresponding test -### Lean +### Adversary Python script -- [ ] Builds without errors (warnings OK) -- [ ] At least one non-trivial lemma (not just `rfl` or `omega` on a tautology) -- [ ] Every `sorry` has a comment explaining WHY +- [ ] 0 failures +- [ ] ≥ 5,000 total checks +- [ ] Implemented independently (no imports from constructor script) +- [ ] Uses `hypothesis` property-based testing (at least 2 strategies) +- [ ] Exhaustive testing for n ≤ 5 +- [ ] Reproduces both Typst examples ### Cross-consistency -- [ ] The Python script's `reduce()` function implements EXACTLY the Typst construction -- [ ] The Python script's `extract_solution()` implements EXACTLY the Typst extraction -- [ ] The overhead formula in Python matches the Typst overhead table -- [ ] The examples in Python match the Typst examples (same numbers, same instances) +- [ ] Cross-comparison script ran with 0 disagreements +- [ ] Cross-comparison script ran with 0 feasibility mismatches +- [ ] The constructor script's `reduce()` implements the Typst construction +- [ ] The adversary script's `reduce()` implements the Typst construction independently +- [ ] The overhead formula in both scripts matches the Typst overhead table +- [ ] The examples in both scripts match the Typst examples (same numbers, same instances) + +### Lean (optional) + +If Lean lemmas were added: + +- [ ] Builds without errors (warnings OK) +- [ ] At least one non-trivial lemma (not just `rfl` or `omega` on a tautology) +- [ ] Every `sorry` has a comment explaining WHY ## Step 7: Report @@ -359,14 +491,26 @@ Typst proof: §X.Y - YES example: ✓ (N vars/vertices) - NO example: ✓ (N vars/vertices, reason: ...) -Python: verify__.py +Constructor: verify__.py - Checks: N passed, 0 failed - Sections: 1(sympy) 2(exhaustive) 3(extraction) 4(overhead) 5(structural) 6(YES) 7(NO) - Forward: exhaustive n ≤ K - Backward: exhaustive n ≤ K - Gap analysis: all claims covered -Lean: ReductionProofs/Basic.lean (or .lean) +Adversary: adversary__.py + - Checks: N passed, 0 failed + - Property-based: M hypothesis examples + - Forward: exhaustive n ≤ K + - Backward: exhaustive n ≤ K + - Bugs found: + +Cross-comparison: + - Instances compared: N + - Structural agreement: N/N + - Feasibility agreement: N/N + +Lean: .lean (optional) - Non-trivial lemmas: N - Trivial lemmas: M - Sorry: J (with justification) @@ -382,14 +526,16 @@ Verdict: VERIFIED / OPEN (with reason) ### 8a. Commit ```bash -git add docs/paper/.typ docs/paper/verify-reductions/verify_*.py \ - docs/paper/verify-reductions/lean/ReductionProofs/*.lean +git add docs/paper/.typ \ + docs/paper/verify-reductions/verify_*.py \ + docs/paper/verify-reductions/adversary_*.py git add -f docs/paper/.pdf git commit -m "docs: /verify-reduction # — → VERIFIED Typst: Construction + Correctness + Extraction + Overhead + YES/NO examples -Python: N checks, 0 failures (exhaustive n ≤ K, 7 sections) -Lean: M non-trivial lemmas +Constructor: N checks, 0 failures (exhaustive n ≤ K, 7 sections) +Adversary: M checks, 0 failures (independent impl + hypothesis) +Cross-comparison: all instances agree Co-Authored-By: Claude Opus 4.6 (1M context) " ``` @@ -420,15 +566,18 @@ A reduction is **VERIFIED** when ALL of these hold: - [ ] Typst compiles, has all mandatory sections including YES and NO examples - [ ] Zero hand-waving language -- [ ] Python has 0 failures AND ≥ 5,000 checks -- [ ] All 7 Python sections present and non-empty -- [ ] Exhaustive n ≤ 5 minimum +- [ ] Constructor Python has 0 failures and ≥ 5,000 checks +- [ ] All 7 constructor Python sections present and non-empty +- [ ] Adversary Python has 0 failures and ≥ 5,000 checks +- [ ] Adversary Python uses `hypothesis` property-based testing +- [ ] Adversary implementation is independent (no shared code with constructor) +- [ ] Exhaustive n ≤ 5 minimum (both scripts) - [ ] Solution extraction verified for all feasible instances - [ ] Overhead formula matches actual construction -- [ ] Both Typst examples reproduced by script +- [ ] Both Typst examples reproduced by both scripts - [ ] Gap analysis shows all Typst claims tested -- [ ] At least 1 non-trivial Lean lemma -- [ ] Cross-consistency between Typst and Python verified +- [ ] Cross-comparison shows 0 disagreements and 0 feasibility mismatches +- [ ] Cross-consistency between Typst, constructor, and adversary verified If any gate fails, go back and fix it before declaring the reduction verified. @@ -436,15 +585,18 @@ If any gate fails, go back and fix it before declaring the reduction verified. | Mistake | Consequence | |---------|-------------| -| Lean lemma is just `rfl` or `omega` on a tautology | Rejected — add structural lemma | +| Adversary imports from constructor script | Rejected — must be independent | +| No property-based testing in adversary | Rejected — add hypothesis strategies | | No symbolic checks (Section 1 empty) | Rejected — add sympy verification | | Only YES example, no NO example | Rejected — add infeasible instance | | n ≤ 3 or n ≤ 4 "because it's simple" | Rejected — minimum n ≤ 5 | | "Passed on first run" without gap analysis | Rejected — perform gap analysis | | Example has < 3 variables | Rejected — too degenerate | -| Script has < 5,000 checks | Rejected — enhance exhaustive testing | +| Either script has < 5,000 checks | Rejected — enhance exhaustive testing | | Extraction not tested | Rejected — add Section 3 | | Typst proof says "clearly" | Rejected — rewrite without hand-waving | +| Cross-comparison skipped | Rejected — run comparison script | +| Disagreements dismissed without investigation | Rejected — resolve every discrepancy | ## Integration @@ -459,5 +611,5 @@ Target quality defined by PR #975: - 800,000+ total checks, 0 unexpected failures - 3 bugs caught through iteration loop - Every script has forward + backward + extraction + overhead + example -- Non-trivial Lean: `G ⊔ Gᶜ = ⊤` via `sup_compl_eq_top` +- Two independent implementations agreeing on all test instances - Failures marked OPEN honestly with diagnosis diff --git a/docs/superpowers/specs/2026-04-01-adversarial-verification-design.md b/docs/superpowers/specs/2026-04-01-adversarial-verification-design.md new file mode 100644 index 000000000..c42684f08 --- /dev/null +++ b/docs/superpowers/specs/2026-04-01-adversarial-verification-design.md @@ -0,0 +1,145 @@ +# Design: Adversarial Multi-Agent Reduction Verification + +**Date:** 2026-04-01 +**Goal:** Strengthen `/verify-reduction` with an adversarial second agent that independently verifies the reduction, catching systematic errors that the single-agent approach misses. + +## Problem Statement + +The current verification flow has a fundamental weakness: the same AI agent writes both the mathematical proof AND the verification script. If the agent systematically misunderstands the reduction (e.g., wrong variable mapping, wrong extraction direction), it will write a wrong proof and a wrong script that agree with each other. + +Evidence from PR #975: +- Python caught 4 bugs; Typst proofs caught 0; Lean caught 0 +- All bugs were construction errors or formula mistakes +- No bug was caused by "proof is right but script is wrong" — they were always "both are wrong in the same way" + +The adversarial approach addresses this by having two independent agents verify the same reduction. + +## Architecture + +``` +/verify-reduction + │ + ├── Steps 0-2: Parse input, create worktree, read issue, write Typst proof + │ + ├── Step 3: Constructor Agent + │ └── Writes verify__.py (7 sections, ≥5000 checks) + │ + ├── Step 4: Run constructor script, iterate until 0 failures + │ + ├── Step 4b: Adversary Agent (dispatched as subagent with worktree isolation) + │ ├── Input: theorem statement + construction steps ONLY + │ │ (stripped of constructor's script, internal reasoning, examples) + │ ├── Writes: adversary__.py + │ │ ├── Independent reduce() implementation + │ │ ├── Independent extract_solution() + │ │ ├── Property-based testing (hypothesis, n up to 50) + │ │ ├── Targeted counterexample search + │ │ └── ≥5000 independent checks + │ └── Output: pass/fail + counterexamples + │ + ├── Step 4c: Cross-Comparison + │ ├── constructor.reduce(x) vs adversary.reduce(x) for 1000 instances + │ ├── constructor.check(adversary.reduce(x)) vs adversary.check(constructor.reduce(x)) + │ └── Disagreement → diagnose (real bug vs script bug) + │ + ├── Steps 5-8: Self-review, report, commit, PR + │ + └── Final PR includes BOTH scripts + cross-comparison results +``` + +## Adversary Agent Design + +### What the adversary receives + +A stripped prompt containing ONLY: +- The theorem statement (1-3 sentences) +- The construction steps (numbered) +- The extraction procedure +- The overhead formula + +The adversary does NOT receive: +- The constructor's Python script +- The Typst proof's correctness argument +- The worked examples +- Any internal reasoning from Step 3 + +### What the adversary produces + +`adversary__.py` with: + +1. **Independent `reduce()` function** — implemented from the construction steps, without seeing the constructor's implementation +2. **Independent `extract_solution()` function** — same +3. **Exhaustive testing** — forward + backward for n ≤ 5 (matching constructor's minimum) +4. **Property-based testing** — `hypothesis` with `@given(st.integers(min_value=2, max_value=50))` for random instances +5. **Targeted counterexample search**: + - All-True / all-False assignments + - Single-variable instances + - Maximum and minimum clause/subset sizes + - Instances where source is barely feasible (one satisfying assignment) + - Instances where source is barely infeasible (off by one element) +6. **Diagnostic output** — any counterexample prints the full instance, expected result, actual result + +### Cross-comparison + +After both scripts pass independently, the orchestrator runs: + +```python +# Import both implementations +from verify_source_target import reduce as constructor_reduce, check as constructor_check +from adversary_source_target import reduce as adversary_reduce, check as adversary_check + +# 1. Do they produce the same target instance? +for instance in random_instances(1000): + t1 = constructor_reduce(instance) + t2 = adversary_reduce(instance) + assert t1 == t2, f"Reductions disagree on {instance}" + +# 2. Cross-check feasibility +for instance in random_instances(1000): + assert constructor_check(adversary_reduce(instance)) == adversary_check(constructor_reduce(instance)) +``` + +## Verdict Criteria + +| Constructor | Adversary | Cross-check | Verdict | +|-------------|-----------|-------------|---------| +| 0 fail | 0 fail | Agreement | **VERIFIED** | +| 0 fail | Counterexample found | — | Real bug (constructor has blind spot) | +| Fail | — | — | Bug found before adversary needed | +| 0 fail | 0 fail | Disagreement | One implementation is wrong — diagnose | + +## Why Lean is Dropped + +Lean's contribution to this project: +- **Caught bugs:** 0 out of 4 +- **Useful proofs:** `G ⊔ Gᶜ = ⊤` (1 genuinely meaningful theorem) +- **Trivial proofs:** `n + m = n + m`, `14m + (2m-n) + 2nK = 16m-n+2nK` (add no confidence) +- **Infrastructure gap:** No `ReduceTo`, `NAESatisfiability`, `SetSplitting`, or reduction framework in Mathlib +- **ROI:** Negative. Every Lean lemma requires duplicating problem definitions that already exist in Rust. + +The adversarial Python approach provides stronger evidence: +- Two independent implementations agreeing > one implementation + arithmetic Lean proofs +- Property-based testing catches scale-dependent bugs that Lean can't +- No Mathlib infrastructure needed + +Lean remains **optional** (nice for credibility) but is removed from the required quality gates. + +## Changes to verify-reduction Skill + +| Step | Before | After | +|------|--------|-------| +| Step 3 | Constructor writes script | Unchanged | +| Step 4 | Iterate until 0 failures | Unchanged | +| **Step 4b** | — | Adversary agent writes independent script | +| **Step 4c** | — | Cross-comparison | +| Step 5 | Lean required | Lean optional | +| Quality gates | 1 script ≥5000 checks | 2 independent scripts ≥5000 each + cross-comparison | +| Deliverables | 3 files (Typst + Python + Lean) | 3 files (Typst + constructor Python + adversary Python) | + +## Cost + +- Compute: ~2x (two agents instead of one) +- Time: ~1.5x (adversary runs in parallel via subagent) +- Complexity: moderate (orchestrator manages two outputs) + +Worth it: a wrong reduction that passes review is far more expensive than 2x compute. From e48954629a67888eb78bed7c96abb33184363170 Mon Sep 17 00:00:00 2001 From: Xiwei Pan Date: Wed, 1 Apr 2026 15:59:12 +0800 Subject: [PATCH 5/5] =?UTF-8?q?docs:=20/verify-reduction=20#841=20?= =?UTF-8?q?=E2=80=94=20NAE=203-SAT=20=E2=86=92=20Set=20Splitting=20VERIFIE?= =?UTF-8?q?D?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Typst: Construction + Correctness (⟹ + ⟸) + Extraction + Overhead + YES/NO examples Constructor: 41,107 checks, 0 failures (exhaustive n=3, sampled n=4,5, 7 sections) Adversary: 19,832 checks, 0 failures (independent impl + 3 hypothesis strategies) Cross-comparison: 900 instances, all agree, 0 feasibility mismatches Co-Authored-By: Claude Opus 4.6 (1M context) --- docs/paper/proposed-reductions-841.pdf | Bin 0 -> 143556 bytes docs/paper/proposed-reductions-841.typ | 140 ++++ .../adversary_nae3sat_setsplitting.py | 609 ++++++++++++++++++ .../cross_compare_nae3sat_setsplitting.py | 127 ++++ .../verify_nae3sat_setsplitting.py | 419 ++++++++++++ 5 files changed, 1295 insertions(+) create mode 100644 docs/paper/proposed-reductions-841.pdf create mode 100644 docs/paper/proposed-reductions-841.typ create mode 100644 docs/paper/verify-reductions/adversary_nae3sat_setsplitting.py create mode 100644 docs/paper/verify-reductions/cross_compare_nae3sat_setsplitting.py create mode 100644 docs/paper/verify-reductions/verify_nae3sat_setsplitting.py diff --git a/docs/paper/proposed-reductions-841.pdf b/docs/paper/proposed-reductions-841.pdf new file mode 100644 index 0000000000000000000000000000000000000000..c4e696c9f2327082c16817c9ad5d8556618648e2 GIT binary patch literal 143556 zcmeEv1zZ$e_ppU13MK}Mu7RRR%+Br-B7z_WhzQt8ECNyzb}M2$b}JHMAhv>v-G$xV z0S2hpkMW%wv+Te!yMXWa{r}(ZeII%6&di+~=bn4|+%a-@ayDhmEOm?~!T)r07?Fi2 z%qK|4)>cO(GWQxCE*F`*dk>XIqD#lH=+Gz;i+;KU`bCQROC+eihe#q}X(>hJKpi_f z9eJo9YDh<{qQ&mfQNe+sq*3R&~&9YEBSy)J+ME9i< zbYIL^LuFJS-IqaKOMIVPTf%*rBm7yD`{)_^ErYgYmUgIbCppYfBC){ZQUVnkcA=>$ zAmb(<6(z#(%^$xpW5$TwBf@-w4kv?or*;sa=&O_)R%HsWOPbhp?1`CWy$NR@cdX&_Yv}l0J*oHa!+J{Nq#+1#iS%6XSsJ|Aiz@8ag=vRIF!bHJ9>(`ghobrhx*D}DGz`QTWJ8Obu|M} zAR>mUV&aMcNTDnLLPK!tu6hJyI!Yrz%@;ia+@}HriauqqlKyhoL@+-kq#;99YMepX zn%_F144zRDfCOF|n%{yF#=?6k}?o7i4vK3!f0??HYlp%?_P0x}eF`7h-!8fKDLiFd z$=#=LlTmo8ExGy>FJ%mZ@yQ(JQN>G&nZExGsUJQd@j^HW@N^|<+P zC3m0V5mkOz?md>ykEQcrX?>QC^FLm4{n7am$zQ}4S#tI1{Mr9$B{x0_e+4`#{JCo} z#kc=8B^|$*;)R&Irt2mySaQ$l`Y7sCxG1iu*uKGXH&w zFBZis^WUdEs9ri@8_2U zKg8BtN!C+L_00T|yHDUPrh1*2>J?&Z0;l|IGH)@}!~SC>*FRTU6ZqwigTO~j_1{7z z_a4>f#EO#OiJ~2<--#6^_ng9o>UrY-F(o%XvcJSuT*=+1>qzxQ#XKzuJrGmApDvB1nv$!}l`^{Jxl(bTq5xG972~HWpqMKa^(jcG3YTA>f{dzO;-X4L zI}|mksw&pBRJ>0~5LM;GMU{&BltjtYl#2RvePqQf74Osap{k>}sFJHMrKE+bUSbIy zrNS;a+`-1z8zqN=P|dLDV(XQEiSU;>QlH<6R!`Z82? z`p=hKe`Gxv>w+csoWO;lBKLpGzXcD1Uknxb!6A?F=>NM?F+Z|@7^)(bxKy;q?JqSY zS6@*QdcjZ^6GK&|;+Nd|(S1Wz97f}kd!OzzstPe0m)!dlAE_$IXk60upehhURjR*M za_v&pi}`CMq3;Y;?fza#;Yjr)hU!oM`$|ejs6NL~{feRb)ZZ&9-cx;yq52X-^`5_1 zQaq)45<~S9hPsmeUPHU1JQ@CyHOv{YLc*=C7Ar`;@*? zeTbnhuVR-}PhhC4?5~$x`&3V1s6N0@IluTNr2|yXXa0K0wNLpF)e9J^7Zksw`;SH| zF@L?}+Nb=3x~LecxBRt|A$lewrtm3gsc47pJE~7HMU{&BR32jJJgJ_={I!zKi@Mqv zwIx@d?nmm1V~SmJ?NEH9t|o@+gMY82^n$vk7_}u=pTe8!p-iz$t{sf0N~T>jUu@cC zsH&M?64c-{H|mUmAYY>#UYm?9msvwuRAlsgLC`((=#t6BfDs71iGFz(fm$smd z5tvb>w!{UQCRJriThPV`%%~f%#08lqRf0=f(8dVNs6txef=rXDv!yL)V+3YYg)MPG zrb!jx(iXHa0yC=gmbf6(q$+c13)&cg8Fj~%xFFM{%64fB(iruOQ3aLym8hEfKdK;< zohrU1E@&%cIjFZyu%Iu{f{4>p>!eDu<^}g2;VWD&o%$>8J%Zj;r`Dk0ylljX%Y~^D z;j*MxRMX^QTL~abdc`$Hpi7nRk``QJbd5?^aE*~oLfxPxEx5+WO0%UaxW))Fa51qZ zyrPY9?ny4Nj5z6veMJUA!(59|(Dw)yi0KtsKkka&B+Egq1l%(MPkO~^_SCRI$S-xL zas|CfaFhGqjOOtq8|Ff@vi z)0;V!lmLqg!PKnD@eaCh1cC+DK^fM(JYfuJwU9+Qg68fbV*j8ZmBNzIRg*H-BqeYt z=sZR4HA1sA|eWX#VX1tgaO%1aqWpf`*aYI{=!EeYTpr6m%u$52b8 z6e10%F;WT`D}`8LN)@EAQK;EZY9WLjxRTl-Ifq4rL(OxUX*d-7EAOXEz0)ZA1Fbhe5Oi93qCb1S=6OHJB zYe9^65cTKMo4dn-1%Z(?jT!xd#A6?ML?Fsvb_|U04VJ^pc6NB?i1?FTPNIHz)DPcM z3jo(H6z?!;rFh4a>iCUnL@!)Bg!zr8?JAQD3G5>(6-t2KQkhNydyh(F5_n2;h9saG zP-#d48WQDM5>QjAKq3JTIgu)aus|ac#K$oVQ3?qOL_SL(dsPBv3JDlIBoGcDfsg_T zgegeCs3HOLjKo?95AkT#E`z`bAdpuAoLd51RsxE@1WX7L;JgxuJ(hq|Ujk+diKP$~ z!k{b72tdu1KzOPILR}@`_LYDtEdixm0wKH-2=kSI%UL25+7);mOEUt{9VH+Nz#$s& z2crPVLITRE1SAa!1infjC{`l16u<+FRHYdKYzYbMH3=w6=$H+3Oo;^4GIUId1XNli z8b~BUv=n1_X+|K1Il`WnfIuw)yq5rCNnmLu09*-7PXZlCSRr1Iw_9mO0OE@Tq#_9j zE)tL~Bp?V&fL}>~%}Ib6Nq}2Q#6kiA-utB)0q|f61P)3dm{0;tSOU%<2{@eKAQkw7 zQGg^XVOSwN&`6|m^$AuxFHMNkOgkY0ykuV8?wL+ zSwU`yO|fcWMNZ8jgpj{Df@}t>>}nfVg?^A$E%L4>6+f8$~o-eWUqYfeegmms*2>V^jM+%L)EE4lUh+#p9VL^ytL5P9V(BKbHm=$8J*q&6H5kUGhN;zji zfMG#^VL^alL4aXFfMG#^VZ}mB39p0N-W7zJ2WyrQoR?x?@4QV?nxOLAql> zx`U(igvdhiH9P_}I%6?1{(y{ta+XmZvlt{7F-R^bCmQ8DLoT#H?|2>5&OaYHl(lTg zJ{D>jNo(p`R*4+Ml1d_UdB}lpsc$r&au5PXK}8+0C~KE`Qz1cGXbQzQACWP0O9O%x zN-aj|$6^qy#2{Fq)MPOz;V6X}rB_1=w$KQQZ(`z)0K^b6h#_Ji`zTWvW$~hnUNHzj zV&Djnuq@QOMkXi)a`0d+7F4J)`%%A+s*r=`1(PswK5`V7au6oSAqSxxVjw3p2mn%p zg@B`xC5cBl$e20gfL$yG@`DnLQSz)9z$b>qLy5j9Sr{c4i)BJGDvo$i3q*ktfGj2k zQA!LFj~H0D7)ZYuSRYC`MQO2OsgV4S*FkOX`N+Ye9DIf$S{7mJ3ypd?2cy8?Nr0?2_YsqKxoG-S*ia)7M^WpJV_P%((rVi2pvAXbY( ztVS8SC@WPg5t26Xh)Xj9kaol%?Vx;2bmF5Jq#fjN6N9uP29u3gQ0Bs(HMPAfkb?(n zv7iYCi?QlkR)riiBZ(vu@sXprl!FM<9CA>~0md5|awQfE38c7^+9~jnLs{k!gE%M# zaZn86AWDA~gE%M#aS#sSg=K;z0(+KNEF`$$__ETB0Hhr;@+X0`BL-;)CD)2U+7W}a zBL-U*B;5*Z4!jO(d(TG>9_6qQnip1e)VHh>ISAz-2R-tT1K(2LXg=j23KvBV8f3_T zHHStDLT0ZJaEdQ;kTKK#P#z@8`D8#GM7g!d`HgaMQT{K=5k~pLa89$(2#POr@J9gi zXW$OXh(y_gC<75?F`|q}28>(aei!P!crphM){tu`)N;wS6?)tbOaN?=eB>xDyr>5*pwWHb=b zKtcnfBVYx95FiKu1o#2?0D1sC5U~ME07*dI07U@w0N5C?FJN21u7FJedjhru>UmQD zr~xbiAz-ax8DZssWB`E&4kOSjfqp4w2D?fmv@&F&)po$6Ov;cGl0QjApxU-oMvQ6n zodY2F08v5kX(T`XMK1$vNW3G^hQ;g-HZ(3_i{KK70x9WzATDstlcEs8(SV?H&Sx5c z$q6-pWVi#MScMzbh*Kz8lgUuHZOCPT%7DCbnVT{s%K}wIeaet@4O9~Mi^4EbkR^r( zFUS(tP>U8kYJli3v`XhFvsOZB73~+F+7xIXIE4&Yg$#HFe3=FQfDZw?kO9AtSu5EY zRP_l!0IB-*;Je-nAgxl7Lv=p%wxbql5(kZ+ZG@>EO zT!An#j^luIhS49(wM5I4A^8=@OT)H6GAoEzYPJHdQQYOjv*EUaM9JP!cxmuxO4UBd z<1&!PWgw5sfW6CDB^6ple;T><3v4~!d_ZK7fsP;p9YF>50+H(!TLCX1Xs-z6iKHjPB0uIt`I4%NDQQGG z_~=4rpa7YYEUuz`ji`rE`=AKQKrNJkS}X&#SO!w648$@Sh;uR!0A-*S%RnubDf{Kj%@M@;uPbOfUnMnRD0xC6eVNKOU;K^;1lfNGE#aOfy3Cxc0?*bI~3 zKC)aQ(F%&SsCwH2?r+J2SLQF&dZ5+xIsiaDWM>f2UL9bq~c9ZAG0-%Ntb z9jP&bWNdP0>PeBT3ZgznO%VH$??Mea;u>mu<}VYO0f&ytAs;G0rV(`zY9HvU6sW%x zWK}8911TV@6t)?BpBDZAEnvZ=01c_KV?o6@N+6W*=LsT;6y#Sa2t!hkU*UVW@CW@1 z%ddFV)xtL)9eL|26)VM}sF;&Rq(r4r9QG7O3}u>#@2MTCvi%f!j-VM16O;|xg+~ip zScA<|028?8OX%By3^?%4fZGNnts-(J;XW)T3M&PPPzn+ums2YRi4d|-;SUxaBtpoj z1s@O811VSvmJ2CZJRr>&{-7Qx7c^}eN~j0Qg%p$vDT-wlRxW_5X#f`0i->{DrzAii zHE52vhDub-!d+N;}*tTjYJ=Xn1Cn2O*sFYSWGty zKvN^?rL07e;c;RDuuwE;l$6Pk;9f!CmVib9vxXjMe~|bo*ghJK+6~U%f&BJC`le}} zFelhrAg!uMLKPf?Ml>s*9`fJ`sii_~V-!(4zar28q#BH0An6psFMLmZ!%FO#U@M0P zAT?n$KoJ=rMd9{~R#<14}`+fk#uS_5oG}a%|xmT;!lYC}ji-E|q3< zM4`j-;0bxYf^C{;FPHWAzlhJpws{s3&LU4qCp9$0U0%i1~Nf2 z3J!)=JDUP%#-ldC(ThlUhWjWd4^ToTs5@h5s~tl=HQ>P$lCFi&0FY4wYNwL1f)ZSa z2H<;YhstBDcmxXCED>a^pmUdaw1jd&hBJ8JDW#DJG6Gyn?Ogavj|Zrj4A_(;AP{Si z_YLtfP!9xm4YJh1$113Q0sYhfNc=UxTuWpc2LY5+K8E=+bA zhrS?(bKh`5Db(C|SWqH2_e~X)Fi*daA_zW>$Ps@D@#wj2S|BMOA`Kzn5Of7NDnPJb zjp&q6zd%T7syvj?A6TGS*v4>JfMCBGQ6!;$K|XKK#YZE z-V03<*HpVt3oI(8_}qp9BT#{if5HAVqB%nSf$>kxNd$uZYb0n1^$+$RNS}s3waMEM zObqojOEZV4V`vYIoh%qT(Lon1D<}(LEKs{{JXr|ioPzc!9}tJ7MqXqaj(%6$JReM0 z4nL2?93&fo{BJ=F z(}+B)-r7WzLRo;^cmL3LIJs~9p;S`t`+JZ^DmaJ|&}tAMfN0Qdt(3AV*iQ*)Gru1o zR|1Ku5ReT>0X$nNrB-k}8qsV%-WC`Sq`!ez1ioh~*pEi^o45T6bR(pkLn4_KI` zv9sJeGSDYjF6ubSJ0u)RkIx9$T}66Bl%LLS{k4Vkx}j- z;y*ailmxuOZ`gt0G(q`=_!&6a#UMkI-vD%=dy0=_vO>x-sik&cyhWy;-Q*?@^p&RI z3IaeQQB$xVAxjm3MCs-synq@}BBAl4Qd8|<9K-z3QJ8RaFa0(xhjhxRyM;I| zO0m^IA}p|2%1SAu2n!*zX0gph4qo{{;KGB)(VuD|BQ$tMh}?=bi*fey2D(Q;PlA`x z@1li~4q*{~@(9PU;IIgkegXd>_`xgWfmcAF@32sLWTc3J+e!&zGy)Z+YXjo&v{Q0V zEg-z|jVoko3a(3{S^;q}ku1=*M*5}~ZVQl)3=e?-vP)1dImU9>6@>?_5uNaILT#aj zixBiU@I$T6a&G`_q^Q4fPi7P|+M*SLteu@m`7l|f1U&+9MBuFO5df&=~d5C`{a z;XxN)!a<4k(2fEmz<>ZqFdxBvqmhJDV&GVm9ypkO6+jh@#2}^3PS8UE89}y!aa28y ztHwjnh%g>a)R>5)G4uEMe+~~x95^4;C5Xl*6II|LFd%xsf)E~J zz^RA2Vv`mVIHku!5&^Oc5xDML=-(M64gC@!@_}j0y~Qi35A-i+53n68n zd@n=oVyM&>yN{4Z1i%JSsD+@BfnFlCHk!qVI|YtFgLg;i!IbCnQP)+8{|hGQqr*-S z%Rq;p;*uZ|IvtT*Q<({!qKKc99L2I~CFp@$G!hI9zJ8?KlD^U597yp*<3LU{bQTo(jTBNcessDEI*KA#>z+{VJSb#3lOGaeB}aJCGkEb2?2bnuUQB@=fS6Bh$9{( zTo8y8CSC;^)`%!6xj@nJaxhFq+l1%KsZPQoG~?H!g8j0NblKr}U!`-@Hw zB)^d{mXKYP6p2n3#P>lCLPlKj8&Cq-jkth!WcLFjHhzX|d^A8EoiBh4t@u8?3&-A( z-^kcY!k_`AU@HlRF_D^Tc^@B*2}~(8;QSy6&V)G&hANTKm98J~*8%M45j#+#b2DHI zDIfHML9XnGArLB6zW`U12!Ij;=#f8yd#D8Dj}K2^X+<3JBG_*U$Y6nf0lvV1l@6T| z?5_mmkKdoLT@>$zQmvb?VN|ndeIdLDRSORB5rR<(LiQ=W;`SDp6_gGS66{MOnkFM5?AR_VC9A&^NADvxzziJjCFE9^qQkL#WCqW35K&awD078HuU<4#-@VkQi z3Zf23*AQ&MKblH#2pSO>1^?&wE~uDbmZ^5jDdIKwOwm$!Cul@1ieTk9Y!UPjU^2k$ z_^ce?Q$J=UdohtXI95&rK0&J>0h(|~5;_x_FkARZ`7^Lr;OIEq76t;07f1iXPvGYy z6d9d>h8*zdO%P|%DaH6Fa>WzI4EzI~VT|sAIDq`a_$R7BI>hdK(xIiGDxq1RK7Wr8 z;L&NrkYNHa9hje`psf-QO)Y!{x`KXTxX=vD7iJHz5Oll~u#~Dpl*Hw z5kV3_5pZg=!bn&G*@g!_Bu)!@Vexh@4Y-g1FUUJF?I=|b=lqWuzV>wF7g0i%Pa z)=)J$(7-!@a{#M`RCf3)GKC%(4Aes`2BaoP^%tC{M#7Kk)k1WICL>6Zuz|zgL4W|- zj6(PDDzZwh02NTy$X--n6|q%@TSeusLKSYm1cCS{@DN7MwGY%;MOHY>QAwm!(J#7H zTw677_`K!h-a!e>JGUn%eK^NasJ6(kY&5NZ*pT0qug1)f=Wr2n@5>1qi zVZ7LI^l2T`Hu_*F`qU2j4MHsqt>*GuQQ#dtxISMSr_u*aiNnZHw3%y1> zo0z>&YB>5X4627x!_jwQ$Zuf`DS@&^Af&)doPsX2xACadE(?Em@%w=Dw0NH)SAmHo zpp(2l;M2x`D@|Vz7HH*40}J{&X2Cv6K+Ouk0v~4})Cb1SQq2RfLg_=of_;^Mit*=T zr6k-G#vQy1OEnh|Tni*7!!@WM!08Kos+h}Z7o4v~!j`~(fsYakwyzO2QwVc>P%3Mt zDnO|bIms92cw`d3t1LKdjdUp0)Ez$LhN&U?uo+NAK6S_U)ULlWb?2Q`jgn*#rNtj! zr9q$g!>cst6Mgy>ebNopK_Bf!pLoN+L5o12e8a!NP>MbQM}DI^luMu_4M+sU_d%^i zDFfs;szdsvAAkmqLAeCj641xna6M&bmWt&n0W~5Jq|~2&7F%%HN^6_W`E#B0jJ!*e?QU>H0->3ZN7qQNt&+;ZJDi5=n3Vaq^us@ARnNWW~X9|4y8?Ir# z%FYQDa4mt9#9vRKKN8i6$%6AOEuDdnSQnLmEZA>pX%GF7woo6M#k?!HDG!{yB;3Nw zrCG##J~!pFB`ZNvqFJ=NN`)Jz@{-7JV0uD|HOgNsE`daOkHESpgP|$I&=2Iwfx@Qp z`{F7fr;&)m-(aOSoBW0ERzsF+k!i#boQ6IZQ)GHGq&mYU0kKml?OG6VH6nVdF#wsp z>9-kh9x0GNByQlZc#}YSls_xjd+|vi4Zh)Bc>ffiq!nym$h3k! z&#b}DQN21U;@;7xo;7HXBU7Y%#U>QAGLaZbwcNUhp`x!L5gC|EV#bIB_AYcyenT=g ziP;7OgZj#+Ar@YETvP36cw3)Fc`6V~5OMLSO4Yuyn?=R=i%+@=j34A4`n_?X4Tzy$ zx_KzMT2#zKqYYkS+n|%&H!#FI7}hL5YYH6^z>y&ii=gCbd*}=78f*kkjYJ=9hb9!L zLFpVht-L_P8c_r#HIfV^zim2r5Sa@PS|e&u0IAV10aP`gFJPp1NA@*LQ1v< zrxpkyrDo@jQ&Pf`RZy%AUMX-f0{YW1XB2{f&N~1&fGYsqCnNrE#rdZW%lyZjHhGAUJ!C%<249F3`RpPrfsO;VLZ@?bSkHEu>9#Oe_c@p z8f!)Yxq}h;WD3G`1wpA95u`^l6`-y(x|bzM4Sec~@2SOIW$Ma1aU7lIQi!T*7R$|1 z8!{@6+R(^j_*yeax`ZpBlL%Na;$TVw)P<#y$0+KWrIE)dc9Er#$0*(x#on?c{tSKt zwIWf}fK5VfXHrWoH24@xAV9}YkHZjJN<6C4^#PPZ*r0_WQMx{a+*<_drE6b!9ZEns z`0D^P871Q2lPU5~jDTxFgD1waQq2p6`vCt`oS2~;T~wH4U<@x^e=tYo=pPk*Xhb@A zRF4lz<+LRJe*^}ubxa#JT*# zed8US8HVeFeTbzwAiSd`RDieymL%S(<3)V+UWfvgAkLaC&?f|>DaUfFn3qNrM4^}S zn^!(xOGVQfi4lAzQJ{Sw;L7>YD*Dh!mMCiYLjFF2Q^lk?yy4T&)sy5#<-|i3)6j@G z2!INmP>PZ*RV3!YJqQ;pI#CdI5Cj!M_z6083y$Fu!br`cnt3#m4-!k^<`HDnf;^u_ z@`w%O1qu$mIAljDaSnZ_9K?B+hJ`~0qF^s2AQL3YoRT;dpSTz7Pa{=Dwe5=woCi@6 zeParpR*4BJD6i=BO8gtdL3ElW{tbi@nSb$bYzig>74jklN2n2j;iEQ*#^)dceM0`F zU>_x*H2gk*)Y3#XC?T{K7z$08gT8Ts9+Z%SDi|U_Af*<6h2{!EFG?C@Kr}Cq&<5AA z#R21Kf}J2dG!kWm#!)!IO|USdzxV zmx}N`wW#A6?v2j9fFlQ3k^zG*N@!lAU$GZjS3F?#gNlj>3my9Rh6USC*hH;a(6-96 zAUx!L(Y{fEVWHe%5a`o^@Nr2&C}>2%D2*itGf>inLUItfgk1}+R`L`15D7trZGcWg zMiqd>0hMKG%p_trBrfH>WUKkZhOB_Is z1#yqdK7?Jd)Ywg9J` zh1ki$0zTu3@5ARr;Xa%V3=h$BbYBK_E%AMFZ3*{fj__wq?xSbuw+z~rS=!N!27(7{ z0wUWAV`mA391=QCdlGW?p}_XS<|5~?&?xk>XS7e$Xmnbj7yQ2ky3@fsQjVU&0fJuL zy7cR5;wB&I*p0C;?GP61XWGS29vT%GHQE#(PuMZkH_R_Ebg0Ojf8R+S=_?QQ^A3$d zEy3Zh=<`58BJjd`h4l;#g!kk?9xz>0PSqq83nEpa(K>c;5j-nN*>ZB z)IUsd_^gL~C>-$=F8YoedZb{DaY>R{=WEGB}*zA9{+88GwUH zK!*gA5&W}+F{48VK(>Jy;*fq)4^4oq1cdja&y>L*ypDQ@CLpx|;E&n^Ai+mn;ayNx zk(G%7Sp;gJf5_yibcQVoz*gROuJX{KQ30?v7-<57qvR2QJi*>katM+_2Zh7CfQxeP z5S>wR|Nd!Q!LCf12KOtz(SeOb@53*&Gjs@!soEs@h{&O)n|BC03$*Z7#ub9ShepDX zK>3w%FLdY-HVTZntjH93pFs^qm`Rj?E>YgWfxZr*L*Z~{Oe-AFHje^~#BY;bA0;vc zQ#oqQ(L21eJaA}06dcikD|o{G>jh|NWri=&o|H$yQekzS>)$yrSPm;hQf~MFqp4IDUbWYjU#&oL|n4K7j#5i&FkU~Vuj z1U_J(ei3vsA|KSR4v+!AK;I~Oh41->09*=CL6+3=iw>tXG4(4*6GeV_Lm>Yyoh8sj)CaDJSJ8r8(>25w3>hNYD3RgbzVZm~(4lf2Tj0YM zaF)0;{Lc<;lmgFTTjJUK`1=NUN8suVR0pQd*x@TNzLIn#S1h@r&m`nZN}fsamDqw@ z$?z4+k}FH{%!yoC;VUV9W=*anFh;44e|%#mEt9-K%`NAg}ra%D}foXHg# zHG=>^#11GJGCwhWM&>6aZ8BtjmSWrrL*^#~z@hiZ{ABbQnV*czh#~Wnka03(eli&n zdC0qDj+SJ`44I=Pfg(faNM_8CIm+lWGDoo$X@$&DOxq-LWXX5{>}ZZsdPU|aBjXX1 zIm$@yVlqb=X;Vz*C?&m%$s8?ZxIZynLkDt2=SW*2bF?I5fgz#ZB?MApGCv7zh0Kqo zW1(wEdnfag(pJd)B=m}|A!&uBYuEvg1&|ZtC>b??0M8x7N*Dy79DWAx0lHJXMu?C0 zHzG55r};)lL;$(KL;!Cqw1)yiaI^}Mo9@o&ej%R2*J3F3l~`Mf zG38dl(12tp#7iJs3W3d0i7JnZo6{$-Pwn0}bJlO!I(u@jRt;KC_j)ob#W-})1%0ir zMq5+nOqnvp_{^ahm!}LFnXvv&jS7o<)~ImI%xG(mTE0Hlt(*@tv-_{9SnKJA$XNsY zN9+94ec_6*@1DP+9_;(t>)@*cxubJ?wEpp_hw+lG_lzd=*j2ZCc=Yfp4|7Z&y`TSZ ze#0Zvmp%0QI9|V;eeR9v(cfP9e66JY*&x=g?Q%JKJLektPzbDL%?7gK= zc2jzn*{;hv<_+C%-uH=}nXS$J;V$7R$=e3+?SACT_Tf4)OFC>^ZakiG{}J0O z!NfH4luvqx9g zBe%Rf)*S3?xUNBP<>%AhkFn_R^kH^ptYh=}#t)iAmyKfw+jicUw=vPTzo~hm;oT=% zX$CVY4s%%CXhzp4n`ZCYCcl3D_GwzvH$(gA9eP}T*pNjrS?BIFHJ0etH_`R4)@`*%Je@4A?r|dUd zw~(Ik5j$2cn>~N=)nC#@i-ySb%UD;vvu;Y%qL`YyzRy^9exXjMNdXqRP7PbN-fy?3 zZl_(6{j+?vz_6-GFLN5Ncy8r*wW?@=jkI6?ntikTvHi*??Frwu)VX}>j#*bk)tcU%wY-_*WXIvNQeNMk z6`O7oUE#&lmRC>OXZ6|KZo}^;r^hZ8`OI-^XL4n%|^?uO*d*9eERue zld@4MWwL&+Y+WX5;D{pu0aKhGP1z8{Y&n`!VV`^d+Vf9aZZzE&{&lTK+=iG)hmqMc zS|5uZV0vhHqnw5PS+grmKBWg%d6c*HZr_Oq4*V$J$ZYeu2Sc~EySlQc*5Ik~Cc#rj z)iRW{8NKLAKv(7+Q~#^Ic;?y3O%L_F(9Y4wYV7MFCoGy&xVd&q`!Q|yA85Gp%!ebX zbL@V%ZPzlYO-IvtkzqeStxim;oOLtl{P8NS56lg{t2f45vZ>Y0*;m{5duulGpE^dH z=8n9V(dlaR{S+;)gJVyB79}-HU4G$?Nzh~80PBeCmZJMp4|f=9-zvIumGZvKd~s)U z{qQDZtMByv*4$#nr?F?I&pH2ZNR^$p${SYMb^3^VpYZdWtk#Slcwvy&^au0IB#WJD z=G>gT_ha?=xYiY0S-6_F!hMVi1Y~JIBe6elXg5^KIwyNG`QO6-W7o5$QdVKQz z*N3_djC#GRj@QwSdn=_(*;TQrN8Ri%%i8Eojr$srvNB-6q6WjSFyr=I+-jihb9GVl zyZe!?YHUgGcxC>v(^D9u(Y>Glcrm%kq{~fOjQh2C(yQx6*5Q37r9N*ktb6Fj{sW(v zo#qyA8>g2zb)vx>&kAw3Kdy0qymp6GAD2bfH|oB8`P5f`&YXWuCMQbQUUl%FxF(5R z*x*CLnynXe>Ze9G{i2`IV4>lcTk%&$?~E*ee9EKP%yqWCo_1dF!fsu&;W2I(q$}cX z&M}aS`X62s+xPU?8n?ci&r3MmBw$u{P>tB@UAi*cujFW@GKSg_BiHIxz4r9Y)_K|C z6IyJ3*r<_X;_4?hDPwD9Eq7V*xMkF;c2RBa_PuW9ouvL=I%->pT?(8dGpqN zPEhKE>624l&h2u2(5EB6-sbhxb^BSb&q3Q0i^{aFm*Z)Zcca1ZZU-~}RIJ>-;*yc~ z+HY(%H}2@Qs}CKV9S^<^4?dl4Gj4yR=jwrc-q%K_V~HL$9k*uLQ?fw-oNx?$e-sS)w}F{HB@94GSGL( zfup81>(sau$@YlN*<(KF*^_{)E%SnUHSDY7Yro!Y){5}XM(D< zmABDusP`)LxU{wDfNr_3kE@Cw?7q9@(594j>3whA{Bot`{7cE{`*iB}xnIjOs^>$8-ugKi zzuG>Q-yf~(mY(L*tJdzX##_qYOrD*Z*}d!KH8)biviFbsT00}&Hc=;Inr%#-fXN%& z&3E;f+&Amunn};Aq}558{j1?}x6|*VEOtL@5Y$kY^{--JbN}ky2Dj>_B+k-HbJiW{ z+OO&7EAf4MW=tO$dtun|x;5;b=VtH!(`3DCy8+W}%GYT5Eci=5>!1l!vTi4KyU}CG zIC=E&$ zTR&w=#NzT^_n$qnifg^u`kO=K@U{}iysb6=JT23w@|&6KtuovU`o!jDMva=RbN-jE z$-qX}Y8+^=SyyLv(@7zR*R9)j`9YJNTG~}+>*)C#rEeQkro!rkgMQ7jhRA1xU2b7M zUbJ^=?wxkpmDcZw9oF3|zWntv?)}4C8jSnY$t<{&^he^#O}}0o9Asyk7i@5G|FMuZVsvAE`8M4>p@C)b6iO)|R{Nf@t>TzxG@MjYZ{Um+9Z8CMx4yyyYgg5ug2iCL+N-|2l`DaF$e8{P^ z1EwpgL^w=ynfF*!J?BcdlxkfE2hL?T{Os4`&)xp+UnkcXm+biQCo4Oym-wtqmgx4l zfLBSko&WrJ-hY4Pk;!J?{cYP!UGc0*x#{+2=1g0<_-F0gzlPQ5`K8Vk*Um9d%dcHC zKd_3eZtNtlCss!mOmY6R)9X{1*Ue}4uAS1mj_KNaSjTGFA6ks~>~-q!_>))Gi7y{- z=`mR^JMNz;m-SBP-7}~>Fi*TPepK%&%#azg?;kktdAR(Ur|aszk8b#*?uTUa?ydt( z&a60`-23*}n$-{XxRC8<`VID=8|<8yWhv( zhu-|)c4FQ*t#M^T_MDaU+O>J;)O9_rc3;e~=-2&pS*!Xt2CR+R>Du3*+J~Pt+2;o;RbR_z^nJrRRvKbGeC}lb7Uc}f z`fi_izUMcS8QqL7Oq+dQZ_u9$3GR*WR+E?e+@V+IOy5(dW5&mLpT%w@nKus~zlU^59n9g6M-a zb-QdoU1m(@vc6Bu(vr&$OKE$#vi+?wS1VtimD+hg+}R4P5-%}+4oxHz-MwaPwK`P0 z?$Ii1$~F{roH^pvaH}z*ZM8BwdDu-4iVkx0dV1`^*w1HK@4D4rudUO-ZBN7Y&U@Xw zCPwz1*0RDK?}gU%Bv#>_wV~+;H2kS8@oSYuXfpTC@J$>&Tkv9l#FkUJ`8!& zrn|hx^bPICbl2|_b2Hd3twT@y^!83u8=Q}gzE!T$$W-amtA|>MCT5Q9BXaK%adYdW zJ=tw-jrzolzhPw*eRtuq(QP&k3i{@9EZkvd+Rv3|FV)}r!t!djTib^B%X6vc&f3&jGXANrY)f2Oukw?2hwHi>xif3}Ie%t@&P7MxAzi9p zv1(!2_1Bonucw#y@-Xf1#8q^{pO8t3ysWH2!$i&+ANN z+|dRHj@JL##%XIU-@ZR=TBp>seD*Qyiow4hu1;#-Q2IG$!PQDVT0K}eJ)ooPdObfK zt*1d{4I{T-o!`97Bt~8>X<9$ySpA`8o$fxezftG%z>0AXLXN+!c44Zm@wA36Zp_h< zJ$%F;uZhjeXMcA5wxM@?=bb-BdOEH8@l!jwc4FOigPrzgW;Hchy`=uFB{O^6bsT$P z$2i;OQ(BEMH*^hI_RqAy_r30{oEQD7R_HOuZTdV%r(I(+HaPevm5V=boD^qt zH@JU%rYyWQWR=FtGxyDl%yed{E|^_JAF)NP&F^%Xzd8%HHwT;BSzhu`+b zJ0nal-{?};NnUwp>N5M7`XdjN({but-J_gH-)ng1(~I3MU2Z)w8?bxay&t2mo$h_kyj(`r-cuXA zx@GRVN-whVz7v7N+Zs-G3^bmTRL-#Dp34`qI>&m~KGk$yv&*r!4s1{J**L?C(jH z`y%7j6DIYmr8^^~_PX>QBSw|ic9*7RxNST-sNtM*dJA4OnzQs_kH)g~+L@{TU1v1= z^eX3jqVHa};5A+EcKUMSkwcaF&U;&0GJ88knS@^VC{y9*v@2O-56toSac)rD@v9s6 zHrjF}{%q!@Gd~R~&3LAJ{Du3A;}f3!KKSp#qkF>|kIp<<|BkbDzugss)V!FyNMlW@1 z?7+A>PN_1BL)**k?lWVqY0Po=9jEtpw`);r-{M9|4L&^IQ>N*zvla%jBmT?F{I0WR z>^YyHJv9To%+DM&cu=nWr$*%#*E{J`&Q88FZ&%_8kLCUR%og|EZ7=(0OFM7RE^c3% z_H?P{Zn|?-)r*g{20gx?EK13lV1L7A_t}rN?Z4Dph>Q%ZlUw>mr%h|mK`!CDOp0Bs!l+}0-iBqlIyIHf6 zZ=CG*Gc)n=%4MhG_ZyA(H9xiU;gHU=%|%fLp&kEqYti1aZJti`1rGu%#Z(t9UgFqO zr;cN;xQLcQKeTXmv^QvPGqe7LzAD`Z(jp*@qV8do`|l)-7%M`HG_b4u@S5Pv5CG z!~98}NNUP%N_rRUR%^btMRq&O@HMgy_1bj(YTbSB;MX1|nTa#wKG;>Sv!})Ivk75; z>i?T(^*!71dL@JGyaQ*pS~{(BY#iCW$?d?8mZ4?Z_o>?d#emkawcIzhjPn1g^V%%r zo5RJX?Wa~5HPzhp-Ptw!gRfP8ZJ+RG-toO(bGx?i?R_^s!Zv2JL9@url+&+}&fOwDyo%C>dA zFk#zS$G8vj+ftG7&-eOzb@slx-lS*Sn*MX1-#T(}`r0W2Z-kehRY}jvB>q{#5!aRu zdFI2L+>BRg)l(H9P{`e?!q3{Zw~MozJ8=$o^NtDt_i)&-lDmg-;AKJgFt|98E0yO| zQx(=!XuQhSMr57L_i3vfHmU-z{NHjA1Q}olF$5=o6BhoHf+raLX9+Q? z;I{;aBRC!5KM8n1v4@UtQh zG5oV&BxcBk0@YC@J@_!8E_NBCCP{z^9u;;J%g`&>Q7l8wUhF8w&R*;&mcn32h>Q$^ zbcuTyy-VH0;OeLDVe}OLL(`%mG~h)=VKm^kg|Iy09!4V|?qSplbq}Lo*gcHiC5~Z~ zze^m$66Ds#|Ik>7V^{)nrjB8FgE)o}Sczj89GlcJjCv!EVRY~xbqvEup>ggwGH__=pT9tzGwIcBc$PV=pK0H!LbdKL}xI= zKXeZ~&frysdgyxt_}v2jWqu@#!W~+aIlh2@x$5t-Wtu(H{-%;Ds0v8o2Rh(hAoPKF z_KMtA;NUL8!)%IN%+>%aYsiv;ERIsUn6YD>xR|Y_X2b){d6*HXaI`g=1obe(rYJ~V zFu}?9t8*ZQQ?$`^|LbA)l~Ygge?8390}UHfm4_LHk70kE1@hiGS+Pl~l00YW z8^~Kp-%#>8(>ug3YJt3#_>MFD#6ENCnI+Gu_Zb|R*o(~bt}{w=Cp}^hG-=GXs^^4Ogy#J`^z90h{fP|#eEb;Ow-z=Z!wxPy+i%gXzlSGXFw4I7wV;^m_)tQ)I%>OUTPVwN#^Z9XF}&q z$BpJKW}K*}9nD!Rh6O-9U@tX1Bhcf#)MN(OOD&c<5In_RYO&andawzOQy)1?*OovA zP!apH$@;JazoEeWVf?nFFk*=p9$v@K2ySy%)C*6?N#@73LgvTP9*7qn?STKw{&UQ3 z3h@?@5-_I%o>V9x3|NjP{`1k5`}FVm!?KmG^);;}^*VLxw*8Nd4SVxu^yZuEZeBgu zvFqgBZ`&@eUTO07>GM|~XwtUH{OwwmrWx5!D&zgGscFcTfKAuBbz1EfJz$e(yJdr} z|A{<0_u{y`@t3~Zjt&iVyO{Cn{@0%qa{nFs$T6?~q5JcklOOD`?6_BcDZYZkkA1yI zA86*~S!sCt4`nv{)T(y%w#iScGA_4z{?oW^qrDlgC%2uU-D_gkiI*?UJ9S{{KAoH~ zmoMdRNa(dCX@b+XelFucC>rwD4%Eh zT3XtEcY6OaxU6~GX69D5^Ol`_=3hztu~D@_HR9tJ)NS+p!@LSZpKIlL?)0en(PQD% zyj_btza5?OY4PI_?Ju#~vF~?k9o^3^^w^o_G3C~lDi>Y4RCcRdDI$LG;X(5gzF5sm z*lo9DndzDS3F+5chP9Ih4?J_|;FC8aa&Pa9&i%b*UKJg!qZ@4}gh$L0HECv&JG}j2 z`2@+~y004Kv^eDb!m?KXw^j|>yesRsX8O@VJ8a|jytbU)(`3kvbCdNi_#brZoouGcipSS4w&K8enz>jYp*V>x#;?-6?L@^7}T%p z@l#SRec!@C!3*!+?qyLwt=Fz?-rFCvlSr?!{*IHszn=2_bi1_g8(v!O(D6>#UA?PA z>llv|i`JW8kBAP@sy)@IhgqwR&!3kYsqMY~-YVCJ&bzJ*GQG8ISKgD3J?$!auj*AP z#jCZces2>4s}U(1B|Y!fe%&>s$-cDr?FRM_UfAcT&JE{9`rcElx{drKYrFD7^r?yi zcb!^urGYfsVD^B)dh4pMYpqp#Ms9gTOn-feBQn6!)O`(htgIA(CF z!LDB$+Kf4Pa?R!0cbNI^3;NYt-SW(|3Qj@w_J2K@Q^%yX&yGRf)@-d^vE72|&3}C6 z(~HmgdOiOsx3679Zv1actI5w>57$1Lofy40_R&_G*unAdTV|d3)n@+6j(`#ilZd8Bc6O)cqK7Hhx#jQX3VrlkU_wu#s=S;1xojvZigSSsdvl;eldiOb^ z)3f40(})4t2K6eK)H8CgWHf8s@DZ<*W9~K4U-LG*UChOuBl>D54zu`o^u3c?C*FQJ zq~4rmX?`CfBfh^qB6(kPskgz+@o(qNyVU;FtnRmazLz9govQln{J{}vi9;rJHtpF; z-)F0BLwBEXW%RB*3F-R2MY(nj_g2hU=dnRHS--~dsvA5KPUrdrm)!)_qcxA~ziQ#d* z6YJg^zVmfGJ@HiLhXm%qpPabS*^wp9Lm!JJs-OF>q;e>+;e{n_q0XTqeE6 zu5QCDBr6`IWQTn+NZ7IE+>oG6f$43h`=1(cIns~?~I zmr(5mwp5b%m?fI+~_pBc2 z+t_64oyh#yF0a~{fLeoVW)FPnF!87HMgOvg{eKhLD-K^6r}byr*>3hfCObt} zXf9%mHz#VZcHZPLCi!L`xzn!O_Le4}^n;DgEb*v(_j~Jh-KqZcE@$=xxdtzH_Y5A1KcTc2i^-XQq#BYtg&ja)MZTdL9 z&`uuo^6RK)OP`GZ>=TTzXzuT|L*QJ_s^7bKGwY(&aQcOPE?oFHPyXDDSaCb z`WkjTWY^t8UnVceI2*s>&!oI9gO87Xd-zC3ht_qQ9d%i8cE_Kx&vPH#dfiGi_@6x6 z%59spF$wB^GI+o%m)YTSe`#H;|5R_>vo>2M>fL+zq2xP1>9K zqw2*k*Ztl$Zt5b#MPdIm4qFjpU2pNH+Udy+%7%{Zwkf&KrB`iiUE=+Zy1u(IcSroQ zkV=n)%R4?JF`&@Z<_2m`_##NZHsqWWh`>&d=17ycqj(>exWf-UpY3=g7C*Yy2oSVTi-*-95sl z2F)6(I_4?OI+|kH|MD5h1H;Gx@9U1L^)TG6Tla2zE*x3)*rfiM zx2@B4OvmlAPY63>nP~X=lPi0;TE!#7awA7(?6;Mfk1Lm~{iKJnhfY$xjrIDi7!+8J zt>?PWMlvVE{h}*i}qqUQpReLr4cR98)QuA?>%bj+KeZOaXA8Y#t-|B_!oi_O3+j+CQ_RT%s|3atO zcfI;gJ*dCVtxlILqm3~Krab)=m$uWdPqhz?kM*AP>&J(klSj@QKQ{2=Fsmv9Gpfgk zx-4F~>Zr?wHeDy%8e4WSUH)#6MYH|4n|H3^ce>-(mjj3RP8{_o^_l0ufjtfTc;^hc z)Xd(l-1Cp`%ol!b89KAc)W=Okxwd<1XqVI3oSJ1cWz6vF;prBY4v+l2q*}|v@Hh3P=9O0`+C_C+a>`xqEEP|kap8bl#h#aE-|(nhyV>yc z0}y$}G*}$8BK4_7M*Hcu;WMgwnmA|$ok`yNNN2Z=XY9Mh&-P_h8@ROU`zDPT^Qlg5 zqu;eVwAb@;m91ksg?a8tzxR01nv8~vgL)cybYAR{?)t5@xvAkackiigDH~I7+^vz< zZp*q`OV&RcnA#a2cDtYi+P2$qjGi7IM$Fd8|wc=K-SRMai z&ffht4OY(>ef-771{KWDzns(f^_*P0A&<14R3Er-RCBv_?e+8$|LHZMW!vyxS;?zE z*63k3@#l{DQte&3*W&AMds8pY@kG${Zb7YEE$QlVyUM2e;gcGVv|yKx-5%BcZS2(O z9b2b9_~~u+Bl7Uoh4+5#-hXW9(+!J;R(VxM>tc}3jFDmB2(Pg-xW%G5j+_0DSm*3; z51Tf$yJMwkN8*pocz$_Qs8w($Xms(JZS0ER;M7M~Za$frQ{$G?gW*b-F1hgx0%<>h|S}gHQqVNcQS<@?{*4ASUd~+_<$XH=@A!xFHpfA(Z()2(lbAx3Aw8u3bmo)bD+w{RXjjgmg z|2p1cX_=1~Iod>(y2xRK?yq?DL;6U&yp>)466|VucgVG5T$WNV0+& zF5BPk_@w3SuN#=?Scy`tn*QT7_RNN?k2QPNpCO899-=eu^1Y`GM^^0<=l+#_9F{5h zyv8-tb?)F

y0fgzZdA%Cwrib(dG)Bjr4I99(cc{?xw~6RYNpPuukD_sEHzV*l;CwjH+zoW;uCvAdtE#g8~8GN2QW}fBhiqnqQVON~|1C?Jj znO3(>ojRwgOrEoSN4w`vw`Xp*et6^Fui)8d-9?9nR^4Wp{3NT#+YjF_<(_QP=A*>* zN&4+_pC)$ec&^O0BfYbG_Uon}Fgd7vjWe}dGfi`w9u{pY^J{RI=61RZp7*=@@lA{R z^G(ifii$Q$vDflyaD7sbZRw(Mb$^!|+;?TF^MGbgD=h45>GtE<$j-W%n{TbMPTX>R zW7LB3mBai8Udk9SqO#eV!{Wz2?~Go(xcJ5~%uP2Sy{FCP9zJg6g4{RuT=K7vUZ~6c zNedI|gih<0b*bv@>wB-{eR@27W=Kolv?cx0ryuK7$ILc+;>^u{s~fH!HSGPqSIFLp~eKjv~hd2s8o z%uvsp)2A6O=+atl^rD&3n3(#K#2W#d+(o0!>pyad%RRa2klvKA@GshJ4|zXqKH^u^ zW5J;#zHGDqW>Npx-DHDf4h3pawo^=K$-Tr z8~RJcX`xT_#`Nv;cJ4q?*^SQqdWJFgk}6wg292(tai>00>sXiF<@-g4yu7pi8M`|& z%iwqX*7ROCCTTsK@$rCL-)B05tRK&_Ub|E-T^StLe}8@1iZ0C;c5%7gKF5D?y>-1t zJT~}d^1HVA;hf4VkNh6>r*5ZxD=KVVJ~2*T>qEzlfg1y3Dpya>`aNJv$krU&(=~SM zv`+GPU}5*Roo?>&tYPn~24A|p^PSvj`oip}9vhv@-$lh;RsxMhpZ}QsX**V6yt9@S}-=W{B zc8sWh*X5sQ-&=1vY>q**)IYP6A65Q5#H@Uy8MUpSI@Na8$!@*Cwr*`vnwP}W)2l&) zO`oRsnq5~qF!D*6eJ8y~O46gEKHoiXSy$FodqeF54ZBx7Gs|n8Xo}W7v5 zw|iFb@~F{sPMwEM`e*Cw#MC|^x|x}(KV$E{>L>b*3fu92*t_eXxVE%kz_@FWK!Szf z?(Q1g-5r9vyK8WF2@o_$65JuUySoH}1lQX@XU?3Nb8db0-MaJFBwdvPHhZsk@7~>& zexLPQ-Jient~Ke9(HC2zmr{OYm1Uuj~~JI(c_D{0yEZ#KB6cjT!JJfc0%j0pCTDf z0P;${`qWfVcaJA&qlw(xpGM5eNrturE}X6}U3u%ioS#4}E#5ix^eU^MWw$b|g77Q` zmwEDw9$RO2_a7~J^91h>&>lHoa!#>tr(j>Ah@80P&Bvy#Qw6V}bgJZIcAh})qJ+!8 zg1h0srOvR}p(-98b9QjEWVFG&j@5f96fS?Msr^y*xSpY~>K(j*qBga)t_(C?%bls| zHku5vC_=*KLvYS7j-^0(yk6bLU==RyVn>Z}zOBOU{eBlU%F!=t8v> z4rjUMz(U4Ce}{N^90Ol*&-LzXiS(#|GeZF?@gUMklCQX^$;--owowe|eBIJgOmoyVQe8>9qg;CX8_zIJnGEe8M zD6*#C)s#&#pN)jg^_8-VUe1cHHA3=yc?q?5t@$%*izoc0Ru8ZIP%j*_4V5cFI>lb? zohH6L2MtQycEtA0;{7jVG2L5T51qE33R@wK=Vygt5lFYR*xdnuJ&Ga zOgMfJFgL0re7S*MmX>WBGxe(Jc-d_6_OJ$%+>YXf91=EPl2Our9G+bNgm{sr9Renu zS!8!TN95>=5aTz$^4cj5^?FTk@W}PAJ*4nDQV5AK@qrH~aBstjOf^s8Bqm`~)Jfz* z$hW#4_9sv#uv5)Bpj)gPLGF&E9Ujbmz12twQg#i@j<-t>xtjsV%i8J<>`>x&#&S z==RBzQdkNF&8je;vzo+~)P-#5)I^Zr*9+HG*}EsJvA5o`5>NN)_K{t^&kxBD=`gzq z7Z$HW7b0MISJt=QWnc!53XU3i^Ty%x^7+q2lMB2L9C2>ivIQSELU0F+EB%$MUhER? zk7|kWp!3Sn35)FvWBK3{9JZgX42e=S_g!c5g%VHm{S%X=VNDN=@-rU-< zt1DxtaWXO2ASHdj$~eWVw31`uS1DdDIKW?5J_dFM1LMu{3+#$_Gg{ydloeUA;N#6~0mm?3}#0FEB*{ciQv!1hG(5f;&XHJNMHP7Yygij81 z5XB%NdXsYskj)z3SHQWRV5P{)5|8(vQcz5HTd!{35rN+@N;@@sMp%O7&8ezUBqZ{` z>H9>vyI(U~FOoZNFzZ`=xhVJQ_{(tCCHk@`F_a??PG3=6s`w22V9O_ulHN$rf^d2K zml2~db65or=~Pwt7tpdVtm%Id-1K^N(~6g8?IUOZEOKe@zWbKNzo_=|EqvQ3`U>yW zkvjgtl)|?Nqp?Mvu;{(>x$|!ql09x?qIQMx#wq1s;ze)$UqB?hN)TBMF_-z-#|J;{ z1*`t+0_xNj`d6dyv2dtsvF2$HSidi?~{RwGDN4N#Wu;*3=HOdXf5AHwJ+M1#w-> z?&r_F?u6(0ht&M?1@cG?(YqTYo5iuSr?Vk3hRzlm`O^A|%KnIwB$aQ9Tm~}Nsb}o_bh*2vdG{@#P|E! znz18kPc+rZM@5uW2p?-7h>h}rAq`SXYcPt2#o^^tp<-W2&K%ip3-K`HkqE~)d=H+EjRC@&RM7&$8;>Mub(x}G7{r$$q{r$wosHnt5B=H!xqYOMh()`uW z68D!4SCLe(?=b9O2|rL13BD?aoOxGBq0SH}DW{qO8 zFq}$3p340}Vi-R}Rit)+Out2Xsh99U43nWq0j1H74Myi~V-`6D|Hb~5iJE?q>^n*n zSJyYMUL2#eN;r@yQ%lEJh=a#t;QKt}cl?N7*#zUpIH~1joQZ0Hvmg z^T8EgY9nkRVn%qM7MfM>A0%xkwVGO7iZ;Mrn&F-92)LEUqVjRc#r*`MRg?Dmn8ee< zZ|qQi%?0fwH&tR2rmi=ofU7l+8Q9=-|A2Ofc2D!LK@gFEV!V;9WA3*tLZheE#@WyE zQ`os4C!PLGAAXAlPgt#gkxyv1N$jR+a@!x0?pgm zl5%%+8(2~(YoO(bxaoyn4>yCnVX$$%k<1$ls_{L$W5a((?3PZ;IOg?+&q)U(JSO(} znbhqkz zdX07q-+&uYL%xGm)N}bQNt5q=NeC;P*!{Xq5e`fQ`nT^cAjM5Jz z6`DrQ0vf_`DD>9ng}Vl;Ml-~r)LYv|hL}Cz*KaR4jBUWinIJnCNcrsrPkiH8lV67B zT)C?mYPE`ljQ3L|%!xP61;iG`>c8rJ4OVYExBrP{ua;Y>5M)*8@~tbWCvF`@sv&4E zznGJr^M@weXl}lorO+hY48cp(#w2Y6g_0b5`Z|L9*_RHdntNgko(yL=_DC1Qydt~D zV;lRI1Aamwes@3p1-UXlDesX94w!%F#+`$vZM&cP7CNA}WH^hE9zZ_-?!rZ<1bNBF zo*d0K<6Sx01PKSqueHgxHZit9o}2aK;Mrusy1*Ak#icb|6_q|ZREgpka2TItV+Y_* zPrKKYZE_U08-}%9D2-pIxkhqHFX^|{`Rg_ny=!>mv_+ju!%K z_nfHqII8DRp~rDNtI@|jKdaG45&5h}pMDC2qrcVY{PP?g z1Q;n$hyo<%vk-k8-(zkN;2b>a(x>R4rzL}*j41140MU~V1w_sQF2j=%{R4HV^W;k(;|`yX_w4V0=|OaV@`ZHI{*DPK zV4wXR3(%}S`#WF;5gjlE=XuNDNk-2{045m$9qf}O1somdJf96MD^O-W*9Xk}0VWx- z0>$UEF9as}0F#V>&Jvhp#PB>a`e$GGJM#!wAMgmz_5Ds&dam!E6Of*3WCgm?=Negn zUiG;~pfUxzQJ`LBc=obP&s71FjDX2Wz$7C^p!a;P5tvj3^rB49+7g&##PIBVpRDL( zOy$#c0vz@!JqYMfpKD|S%FpK-nSfgY4JB}&z-##YoB{0mNofLAD6qcA1SsIofj0Je ztiUuQU|tl^i2@bvvlFEQl=`GNpRXfOMgxH8(@~x!>Tf6dTourX0+XD6J5iwNe6EoN z_Um^?^x39ef#qz^NO?A z%0$vbL((ro^M|>VPEV0VBXPdSZdSfKXBS&=Pl7fkX zj>75alyyP$0}iw8%uY;RPrZA9NMIn8NIh*BfntB@1Eg81|{ zn3LVnK9)`DC8E^#I0hXgkHW?Y3XR3QLzVm% z+w&tFzS=u)6KvBa6H9&?5c_DdI74<$Nbhhs)l|@vnkmgqdUo5p*`r;h?dOr+D0?q@ zSkT0K_{%D*h^OUD=|alk%*Jv}lYOPx=4RwTAyE6+vc+}Sb~w^q`eI>n8=6~Z%=_KL z)XNB3Bo9=mQ@m)N?2Q6g+R#SzSuO0sTe#FN_QBXKW3B}%%b%o3=wF=?;+dT-6hrKf zY_;HBdMe(34zmNMOsviahLBUGrb%c4T5n3PAWHwo@=L@ z&+w>^JQL78WAxu-T|t}6XYS3)jSF>HqN$@(Dmu+91mDkLYcI9=5it1G!xAHFwcOnu zC=W%A$mnkGjK7K}5Xb(Btbi(A6u=3ItP zghX^4RD_Kdi^^W^VhLL0g-umc;cp?tK4Xz$jCcCN`9?AXrRMrX)cU0svl@x=BM@Pq zxlv;aF%~mU(ba3dgCxK}lw0yd8oT64ozH%`elsiQgi-tTP0%KXOCxVj z@LZ5`0<|<|wp7;5`PgzUDHavnOy|1YS}whUKAV?)$-Hu)J#_jTEKDOwDd<@sjE|@%!K_nZC(Pnr|p5tRyEE_`**9 zOBs{O6yEo8P`j0x)X~1$eTELnj)mxAUsQ>zP?G&^tjpZ4( z^4YN9K^)jx(+`KF67Fj7JWm$)C1|*)rj55tEva4S9Q~%&S~ptWk{MaK4)636`4;nr zEJ~P4pIboD+@u3JkPGhe6Q7PFPTvenikW`M&1<(@J@!=%b?Uq(Z^@$dVU-MPxxQK_ zTSJp6%O(;GfBJX6Ru#PYO{U9l6a{YNyDF^po%bCdknC;)Bq1+5^dr9-CphoesUj{F zth&E->JTgPhhmd&Zm>IS9?Rf!>Y$P8+6$Yk1W^={_Wn7*j^oZfPQt%ErLipbxvA-E zuGhgAV#a0l69$=Cu|3Muv2l+WwUmrXWT#glm6>OB#?$1-gnbZmxUe^O_je7hlpBIx zc78l8c!cj1`5lZLy~NmQAJ8EzYW4hA!urfzZqIAn7c!lQy|R4{Nwo9F(&xKOG*%=| z7DGyE@RvuWv}hU(N3SV4`_#Pi&b4^tsga`f9?~qm6~=g6w2s@tjurdH`AuUjs}1+p zKY!SFI?#}a-#ks#?;Z;Ucb!w&G8&lq*a>$V(lpQH@udnad5+kxz89mQOq1LA9BpQ3 z4dnQN{gdg+IK>{BN4-vQLd-kMjICgpac$@sAV1!z?vlLLF&r)i+*{_Bq-jSAugfj%JZCtzU#XYd z-gFWwQbxP4(D5kmtAe@wtSGr39h%C}Kgml?^oE6SzjuSi=z}$eEM*=-)~eMm zgHuNc&}e|W?SK1YUAzrW7{XJH49eb#zhhK}p_h@@0Oo?CpK zj%KG~#lRRsffqS|YG)4cXcVu0rR?i1ybbGdf*4(#WiWHb$kR|}d?!tdDV3(oY?y$C)L)pJ%lBWDOp(D|-T zD<0s%FF*0~jpfC@A#Ei6L_R3PLYuZDi3U}GA5sMQu_4hS1C}|KXH+kkS$-9$xC@Fl zGu<1Mxh}0US>1s!nQ^0F!_H`1CL^*$I&yYh-wD#Z;?9w)CFAe(8xUv?1ucwbwo`*h ziPiaqn=v=47w}~!^0ivir5OX$xGj2NseudXjJrhn_aBfSY~Rt`LQB6wUi!s)jfS?A zWcxKsOZq`l{2?mVloo}r6%7ogoIN*%F{JJeBJswQzEeH-6RamFcXAo06AoDg%HFGA z7b&5w<%~heQ~WSgpF7h+Q#ThRB2$hlQCUd33wOQ;$B{0Z#8$O}?M7#{6m&{{(?ltX z^HoFE-m(!D8up#7vF53hz=)XkpmU?Xb!ijrKI5CP2o$DM0lDh^Y-jbUJ2f5tO1EUm z=>+~{@`vO{7U#D+1mtE4-$HGmWb@(@iUXj=mEXpUYftnjJK$R6eqB-b$e90yFiV&W z$HE6elo~+}yTSZESH6b+n#zD8KQ_#b?A~Oy3P0=(teTWkv*&i>)^bTDlG5mLMCSGArZE&&LyrIr6pkT zSgdb9;@|<~-&9vq#kFs_y6-xWpzVm+rSed3_hA^ivJc&fVg!DwwgUeKejs{pFlQy( z<+&Zxv{zBJm-bLl%5k)hbFZ^iXN^t6)m&JbjgUi?Gl0>f84zwWD)nhowG4|ANg17F zqI5N{O=Ejqg6-4U?3Te~t4%U9{1T*fT3<7dmx2Wfgb#-bvC!}`O5>~B@23snvQgY# z+%74>bKm^?KP4(s`?#Wjmb{t8Nw3%TdG#)^sy#NSQbdqG8h<#mDL>#k@(k6;asJ0x zn2*h{87M>R`>{QRnrJ?j4HEPtwJvNUaSneDa)Jf)Msj_70mWqe2*_{HMzUt*yT)nOs%%Lp{;jLW@pEzCkxG$g0j#a!FTzKcqw_K2ykQIqn zBW(+GgI@T>P;D!F9`T*=6TFm;%88Jd_WsE8#qY4|yY%{|^N*E7d-b|3n*%$@5Ot0T z`ilZ;Bqk>l72?PnALrJt`i0wxSgs->jL*b+dY?ysB;p}*cI$9Wp7_Vwn|pU%sbNwj zb(cRFDAa8Hv?bRr?1iiJGZK7r5MJK)4a5d(r3RM`(cNHK6B<|TjiB`;KVgL1;oH6# zqZ$pcgm#zYbSZaFffTfwi^z*=0$lmBX#RT-PAe{&E|MCGl`2ekY5`-Ob3A7fREO+o ze}8 znEh}^TE5Sa-K)z$Od9PIDEY3|dfn6py%oy^n*=A*iJeQsn{IU>sBfdJSIJyr+6a;# zCFQfnwF?jW$9!t`%9W6uE=7~RIfNimo{5tFU}K-z*ce1zsYNGM7>i?T@O>nmWzc<* zjhB2V+hsk(e)&UDDVE7*N%e@P7br>O`m*D`D1yvRx+gZ8_beW0VcB3+5e04|0_eMB zCg5*=Vl2r}o7dcfx$Dt#`G|m{-p;5HSU1R1ndCs6gvnP^C&(gPl59Y4j@k<0!Gej1 zhUY=5;EZfd2RSk%H+?#gzLL=i)_Nf2@-AW;L+(GnlF zegoUKPbTQpB+oUJ=uaH>aO6*qvL78nd_<1(i2(PiwB?N+I(}*5q zpU(}%!VMdT${gYT<)@62m)pAzhH5Xpr( zA%k7s8^_B>%eq6TJ;T>IQAYjrO-{HeO5UU&Dq-mNz76~OOU}WquqkEJK;^HX3)Tnu zfd5X==r)i(pt_XEpXQupnyvB$$ydd5kUzZEs<^YxfKkroj;^%4xj49*mWDVq6(%zi zsMXJV!-3b%XA)H;$!lm zw4vSpp3uAK7TXoP?&Y{Iv|TKaH2Jh^WE`8b2Oq2$(gV1Vx47yypG_)=nIx%8G(+{nS$)n-z z9e#x!+K58q5IXLB!X$`LRM=sqoS%qAe3*u9-df*{35k^3!<|^%P^0%|Ukam&3%jL9 zyRM~t43-x7dUN=$GL=X~vDcCH3n?}`wB_8h(YA=RhvBr5%GC$!+D?@%y z)o;HLw>%BAMy{um6rVD4&gUXN$Bm$6GAA~7iYK9ieKI6VJJ%5f@A{cm!=$&lGl{c( z6_i4@ZK9`jKEbw0^_t-YMH?trmCdgnfp|3uUHE+>7vDuFcf2DzDJ6I7hWz5X8f?Tt zd0S#>dAnlAE=g^yLfd=0{~9wO>Q_M9 z#-@((L(qWCwAZ%D3N4)Kx2^Rn(17!+RJAF@XAUPh^H+8U~ip(H0VbUcM5X&lzO z31+;g=^BrQ54wlFl1c;3D9PKE(^>@8L!-GaGj5-2a}pXzI5^zR`N2PR1lV2T8C2!x z`(wxtXMOME@~rHY-`jZ^@CpZI1sPv`4d>2JUm+25?F|Qwo;^bjtpa<99D>TtK1)z% z*y26<0kS%e9!=B22JB}dV}G7*`qth)MZwzQxp$ePTF$8MHOO-4U6@@bX?!JCB3-}`f5Pv8xM zPBlG|+2H=$=4A>wUppM1wm#Ia=xAWU5vz6EHLvxEi)4DH1Q~IB-d0xBG*`KbT2b!@ zTKWc-*!d}Jw~G_9mc6vr{1lqF5}_ea|K-jVa6PAoe#(O=m6QZK8jL1K`czk`OiRZwOf8np3h#fu0*v|huuFFAaptd2QY)3$%*Ya z6gKeJ)=Ya}vZTMa&-N+I)fX(_#YeOa<;dtYWda4k`bB{8o}rn|lcI3^G&&-F0{tL> zyr$>&M5*C@I0dDP=GfuGdA0%KGEe-F9mfo!?bRY{bu^ z%BWBcn>y#70?IMOD6=8gbY^er19ge8hbVNP(G3NL_ht1>TkSdMf)BKnUHLceTX$g& zL+4LjL<&__B77DQr9Oku>t001I*gyGDZfxtG;4WX5owa}D$F`wbI9=Cz=PZ8$QYMY zXC9^>cobr}H|j}>CQ|#56d^9GBEL^YJoMMe3$uZKeaAa$329e%^gbc>eJ6dGT8#C0 z8&`sU6ha?CkMUrYq9AN^+D>Vqf4tpwZa36UBUT18i*3`&T*wf9_OH9w3wCmokOy$! z>)-}_M#Os@=SZE;JJR9^kpzg8TQ4mpTd&S~)2CrB)H?jou^Sky*b++fxp;B&YV=&ICz zBvpbtwF*PG@F42&;N@NoayAZQKjrZ@h*Iy3%@pu1o*b88!{u+DzUQ3SUkxBvnG6Cv;#9n`_n)a9%$Ou@m z?2&x20%+C~`2z5uNAkr4fG|(w3jn4b$rm#KL_L!)CIBS@1l0hb*W>R#L$5#f`N+Kh z9O`i!fb#-4DnLdZkb6C@A@>v#`1I2!?)As-J)s<19`O7+q( z-t2scW2tq{nz3Q<{UNWT;G^*R!4 zzD|;YMoNr20pmMdm!0iy26?gT+8BC4sZcB-jTCt=&39?Qj5KlbIAf!v{O`Z26sD{_ z-!N~Ar6^{el(I2usHbLB*%^t8n>jg&XKHHKT$eX&7}YuViQ66a#fWVdIAaXl7oV12 zHYdnfEydTL%oa|U&!4u}b8b?&ibs_a5mRbp($J7K#dV}~tlC+HUR9*2zab0noPshd zuI7m)(4=EkN@QD3`vwvU{}!H*CYba7mDM{*u4bE}wpFLg^jajDHD)fPq>fb^tMHzE z4(OGTo*fdT;A##$|0}Wd`8DL^ezUFemA$P6w!#e3tvfF(`sy%P(uJgGj>9e2!436T z$)!}C&nxrr)><l5{$kM0Q_G z`cFlxQcq&w3pBNg`X;QvbYWWk>2Q!_0+=$*IM9Wm2?Funm-OY5eE2Mil{Tx5NO^kS zXMEZ^eQ+AbYKpsVb5Q7qyvqMFmD$y;1Y%MMKuAm@rjX#TuHRW01xReC=j1RpCMStN zwz&R0_1v#5_0eiy^7`@P_3*fPu@6m-MBtAg$ajys9*K6gt-vy-6tygWJH_z~J zxoj&Qja0l+3>NxlU)U{IIX0=vWj|MpawB7dGN zX$v0#OO~3U1ESU)a%Wryam)m4FT>;;l>l}~9V1@JBhwN|aU_UHg z_}j2AAO^HJu$*q+n2jHIqk%Uy&bYdT6X*tr6+v1giW|s{o>0rSY6q*=Ky%z$4vLEG zXiBd6Pkcv;4n7()F6(o6w-9&!&@K*x$fJWcD{*MRg=!s6`T{RFFQ?&)KEQ_RBL-~T(Y}u?+V7`JJY5{jpySZcyL~g&q$r( zf%3TJ)8~n74W1dGTT&Me<)Zlq>0*jCQ+>t?*ClYX7S<3HHFcmexHNO}>URDDdwj>r zq-7j?yX_ft2W1hMzq6_#7etMBcKHqZ24pNBk#eIdOe>AV-kUI=GKkDuveRVv$J@`= zqIC|dB@VrKc#&F>`AC(o`}=kJJoa7DK@W<8k&mK9h+#JDdC_6m@)Yqm?NCisxnnnU=9QLPQ-d$SYU;+*ToxmKE z|I4$3bT3Ll!TaQDW@Edja(>V#^`+u)m>hyb?s*^mQtsP`@gGO6f!Uv>Lj{uaS>C#) zFAggvbto4o_2vgQe1=!L83{)7Y_Z_ov_7854JG=354gD(Q+j9^dwx+PbgVi|U*~1C zqzIw#Q-;aCCmS=wsG!vLxBO-;?}oksbL~Fo_Uda?Y8qWg;(0xp84g?%912f^1b&X- zwunhD!5txOqO;fvJyfIs{JvA3-e8|QHO5R>>|Jta%n&bN&bG_?QRW?teoGmRzXj`C zM1sBS`r2x01_v@rn+~NHYUh39yoJ*l4_O>ban#0 z1)6JiI5l(wx_zY`0&d#ho*K1p;AVC5pRMdv ziZ&=QbFtsYMO4C$H((j~j;0!sDsdD^X1>oVLR&1SIn7;u1$i7aiq63Ii?9(CwXqq= znHxL%D`Rumc?2vaDBTjnk)^bThC^26LsPbI$Z z_8WdT)CSplJ(hV!mEC#w+;g_3Z4_GL5MsFVom_d>P)(YEDU*}bxiGC4WFZ!$Ka966 zC-Hxx=~rFk4SnT0TjF4fseo$ryGcm<9Jk;pe+_rHgmotoY=dbojCySoAb}=5zL!G_ zJP5Tc^C4mr!CJL_$&Rz(XQuzfgE6MI*#zyk6i=8d z0pWHs&!Z3JAm5j!2tS7m--itIw0#uq9*Xi*{)llGgXY*1NBhH|q||S@Dy^tMD&yD0P3eKx^z#!a^wW=KM^ z%M<>zOS2~quD4zFYsP4Q@B&};A<7gd?`;l>99Qekmoy9p+pQrSuag6++N$6P1G8^ zf>7&#kC(v}NxvejnERcmRw>40=4g89szvPL6wcFdPmcH^PQ`nEFwavZPZp7}bh1;i zU9nW5pr1!ZIpb^Oh=zV4R&YNyh^&DV_Bwau;(OBmh=`%`uY$s-pc8lwsR+s?Py$ZJ zH3^?JJ|z@&B173B>B9_WteyvP*OIPYM+6j!_7?o|5(;11=yKB8oUjPN(1&FgylL+K zl_(XC)i4?DYjM)r|6}>1{jNv79}R|=FP=p7vY&Hhg|Q5))KP7l+Vnz`bCLHB9DnRE zcI+BMf|hg`rC)?y9PNEI10FV-nrKp$HQ+px+3ig zy|^7KTCI;2Vd0~#6ZpVBmw@D}!zVO%Yrjpcyh@PG?lZ2!hUGMI18-oTYEAxefCLHC zaLHJ>#tD}P<1_i5VBcHXnIUxo=K$HVv*>G*ifb8<9P+i6+^PO>gjK)@76ZFO?smo( zq=`1jiiS*Cekvj2@hrMb@!&E{{%^RMBmxThq{-KDJz9%MYjEtZjH9HTh3XV!nBm$* ziUQ|#&*nMa%_)Kze3;RCU!+H$au(3Ub_W`FZkkFw{PF92|9YXlBIIb4l?rt3PVM=? zcl=ZsKM^ckW6^Rnxd|5mX2cEZR3RmpsuFCYVj8ImfAN=o5^Nz&GmGEkE|8CcSih$ZBq;J%DhgiICSGob`<1Du;#+we0QSv;&_xS0 zI4S+37QQe0rozim-71w=1rRKGN-up>&;$B+t%!O|N0qVz9V+?YRR`fF(LPm85|r5b z&0%|I4Ua+#yd;&Cc3(v!M4zphl6S9df>Yk{v&q9m`dS@RGv*jk(t!Z^-N8yA5Oh-= zKb2IkG|Xhgw3ulBY~1rejChD|j3u$37lVp7y;;Vuq7glet$V%(|Btd3VlOI&p(|N*ST4qgdHM_L6DY3(vlX!Wrsb+FBZ&9=_#NP{+26>b{rgjilxt z3>Pzp#Ir9Fhf&q7j87A%!k}yOdk;M;nw4&uuDL_zs453z|GB^~zq%x)hf}0xj8D1} z%xI(ysx0G+{4|j#a>0OtM#>z)c0%b}WhgPo28WKUfoLSqJ>!{rZ**F99Fr z)Qp2Dh1gYItRzQxCgM7~N9*eD;I)(So`Vx7Rp%bV)vH}XH$*M6jqy4oxlf_pR%t1A zM<3stUVefIEqjr#mqdx!SrjObFO=~;3q{1A+rs+u^}$FhSel%&Q-zccnMA+%q|rJO z*QvpXHJap?QKfCN!|=FBT5OB-Y|O0^M8#(JUE_M8Q~D*mA9$tYksDB}{^LL3V*O7c zyXW^1_Q7GHN6FUkg_*iV>KqPiENuK(mGCLiPe;xoIuMZ;h<>gFj{8CwrQ7!P+V8u4 zREL+q5r6Y-CFnIx()g|o1P9VcT7!BKNIq{424)-#iAKU8&i1<3M~aHRN;shmy7hCx zqmXXfPUa|BoZ2Y=iGUFtrfhk|lxz{-ak!Kc4(Y4%6n26po-e`2XO|gX!OOFuP?`cI zP_J|R`;OA3c>LyU<2uS?(yS!P$78w%pGuSMQc$pAt^nZKTg%-xK#)= z0DT?63~@RJ8o-RTf9;X{^^E1`R>WVdUGOi94S|3?fIj@?6X9`ye|3)ku0is*C-ol< z5;|7a$9n!~kUY-+W@M&eV`OIo%zOuyN5IO$OheDe!uoIRlBb%0T@qGib{fEjPt&rW zpGgjYoiWkTFfcMPK7BSQsAu!e$jrpl0Wh`vk8S^Y86rSe3)s$k9NgnFM30@jr+((2 zriTOCT>pGhfL#+d`v1-j|L^SZznmQoxNZNsY4W>?0c`0r-Rb5r5ZO%rCofB+qe-?PJ?8xFslCeMwE-%XR}IlsWB$?tjOz^20UY+Yc} zcyfuyo2Io-TnF1aAt}mNnDEI$rimB0&=gx zyA4#Klt!N;m>3@@>iB4ASd9AsY$}pM|!OE00 zHU-R!W85rd!}aW^mrO`#QMA5Zl$Sf2C>x*8njAhn+#h=HKOp#k!ib>3WR7v}Et+J} z&4cViGsy@atnJO$6ySrXllm-%CzX9tZ4q`y%$D-m6f$xZOSyW%17gt+5>Zx4Mf>@Z z3AfS`+D6LA@h)SE{MxGZoWm!;h`E4R?~rW|G%Y?!R?E(W+Il<~{0$Pw&rRaVP5g*# z6oO80AudG?1(k}FT4>(@aF8l zS5cw_6n=Q@letGXMdZ!+TH$o5dvuqcO0XcAkAh~ae&~^_(Jh&q6~NE&Jzr<@3cMKM z!~ZPlhAld4+gXjg(&68vUIdQ3hT@nV!%>usXf!!9qzy6xgJ072stlFKl12R}(F>tf z;~W0Px}1e5;*$LLsVdPU=zU?v`bsg*aE;F|Y1c#WkU<-A{4+YYRr3zUtVSqCBHo&| zVOr>!+rDt*NX7swycDxU|6)M<1xz)d?3QSm=xT-ZO6;CIUj{18gCvPP23Mu=K=)?W zv<##t1tT(9a5-mwm-~yf%!JCAT8(LTpsL^3E3r6u>Mfy~WQrLI&m1>a@tc~2Yk@ED zCQ>xN2(Mp6s&hr@mQ-QQlnib`HuCWX!C7=EpUvufq~f@Q)96y;jY6b-lKCiR%Adyr zo_2)bvswfyD`-#&!ECzmI+E2%@1^{u$ot7xh%Bl>PT*hOW0Yc3&uzQFGslP97Pabn zA^n)qj)SMG5W(ez{dN>P+vzxl6}uS4tuF61i+3p1^>cc=tB?r!n*-;-Pj0dWw5q;? z28ZHG)eq~x&X4%r$$G0qWyHD899d-wh-7G~oNiPVwaaxZmf9EMH+F@)+-rzj6F6yk zc!=3)RTksaFOKrLxyZd&@tn;H+?xzM*8PGHGLWXaXf#G7#;7=wNW4{3r(4or4a zd6a#8dvFvwG-{K+!!^1K>)g#5x0Z37z)}B$to%kMchchFq#EO63`ncZ&X^guw2qGr zk$ay1K7{^9#GyfDrxDB-hH#l5Q|M+lclP#wO5#V>Fz#w)3>6JX%6wz&*bN(ahtJua zvMPyVU=j-3fpnEP?3tI<;CUhaMZvs*?I1K*+f7^JY?6^vqEGtj4Ad=siH%Pu z_#ivMj6^byBcb{9=g{c8G?(s*5A0|e(})t1bi!?h8FEQ~Jmivy8uPu?tLIZgQuTY=FvPQ~)4)YDYU=p1 z&GZDP1W>oyW)zZmcTxHHAxG*kGfl4;W4};g(2o|8HqmKpW)VNGzB6*xbL25#RHS4A zE|W3zL+5_w<-;ZEuNT@l<@5s=bAxn@@M;bj=3=QVS%b*KF#6b3pZAp#dq`R+ls$53 z_cH|>TIQe-Ba@_mbh*7Hq=Ru?(hDInwnUmU4YM%#i1=o|HW_gh_e~mf9Lsmq|HIo` zM#s@4U4ycinVG?2W@cuVEM|+DnVFfHWr1a3ifX44ZYA4<#cef+`zZ+QOI?%aD6~?Pygusw$?~q8btR@;cqj~lmZK&50 zTwrh&o?}YI$!b zx+*Iz-z(_fl(-gYQg=a6@JcdWKyrt?a9^ zNPPJv1n};k5aXD!3*R!qhQVbK zh6x{)hm)QD^JiA~Fo(r6;c?D-)C0-=T;SDBJCz%7N_qOpCnC|NUF1_Tax*ihD&*qb zqa+_3;zv#HwfKYytEoIx4oWJdXOoR72Nj~S*(~RFq(!qTr0w_Q%P5_bOKB=b*U&dm zS5X&HH&N$N*HM>QD$E?l6T~?3D|@1id|{V+V9RV3E3(}DC#RT`;p(?Dx#aG;AmMtIrbZ7y0p>R|RS#+msHY~&P4B#fnd|NA)y2!TB z2y4jSxSPq&N3lafSx`xTm>izh~ljkX96XO>L$H z_Y?CSy^nbf&-OS?$r@M~rny<0zE?O4F_~=Q+$kr+x(ENPy1g>_;7e!v^`yAj@cnQfCDoFAo=?!xz2tK0N1d?EUT@7*~Ab8MqvD#l0PG z67j;?T4L61#%xryTDs07 zpP;f#5XJ0>hrlGRtVk8 zWbc7IvS!XJVw)q!BiG9s^g9kMchesC{p?(A>g-t4cGC97&;6bXfDEu8YFO&HSoPW? ze%m+FjxV6U^nDz8R^LX*^&k|bpR>jn z*dvfp*~XfWFGLM@fMzU$kNpax0Lm3*4b<$_3KyLt1?g`9sr3lv*1}n@rLf#@>5wkA zy7g@@*sfq?cIho#WrCG83W9{_C;65WJJio?!SN-=M2^Bsi*+;&~QKAjXt~tjYUhedr`2OVnFXtXOA9dsy%9s-|%BWQ(~Rfy1RP>Ui| zDHok1q^OpZNWriw2Om}lb66_{m;TT`sTWPnN>3{#1>1i{MYzu}czupMb{G;E#r#xpOj?`#UKM#Ar$Sk&7FFcn*k&i4wx{)P~sV`xph#?JqL15XYc=xKg9d27# z8IR1V9E4pcfJcC}V9a7M3%u3Bz$_HrJvrPxWtTch3Rj^M4Nfw4XjB;#Djj?B5@em* zexrvSxrn`NCu~ND>OTc(A7g-Dmedb2cqIp~8`~`ZPzF>U07-06RYMHc6lci&Y zC^W1q`kS1#>Pf!tYDLlC=KM&-!>O(BYU9F?p8>yU*ml?RGlnlEe)f&7eK0O8rI;uf6j~jNiR%q{Z^ha;pe#q?sj_z z02WllA$y~~7`@;Tl&CzmzB1NwFU4iJ;HXf4!%_HQ4M>`q4*!_XNo9A_p3dCNb`6Y4 zA_z(JzSd)zN)JRm%u}HgkJKTfz&kFAsTzNY|A>ydyVJnQP3tYVO$c56^+h0RM}oxM1k+AJz$r0Y?=YRtRdP#FY1ISnI(0xhquLaQ#hgrb zG!LpZiJo^6)Rmp!iCU;`Ej!$}lnhB+<`>(uOYapW2StRYtcl^PBfV-Ln{=jR2BXQ3rSGHGdNaY!jYL*y zdr~rKEY3_=tP80*xzVfC19a##0;LCfzq+Iv*m+FIhlZH2%!;)cL6sTB zN>cL9ue67E_-6696LO`l?OE&zlh@wbao(jP#~_vSJtR+nHc98iMt?|iYP(Wk%~est zMy4i7J7TvoY8cek-XT4+{DJg(x)hcJ{?VcXXNl>tRo_lh->lMC%Ea-vIn+_9Sqyp@ zsnd>5(CC;1r5C%FL`n4Xi?B&k^OM7#uRfo77rvKRbj>i48nvqZ)Q5=?`@3>8+5q zcZ{&kKn-jh(yIp@BM;*7kIeb-rY{$=k*Llf@iFE&X6a3&H;SZ*)u!kp)gW*zLnZ0( z2NK=bJfMC#r}5K5M;P!soC%VFuG?j9*o~m=FWySmG@dNTxTz&Ox})sYnuOeWo1bdzS8Q!3bwbC)oF0m?7{0cv^Y@%~%~F-h|ENJq#iu(D))Uyq;Sc*wTcU6( zc=e)_wdYM!l~Bes*5yvB?z-C|g*T%-=1-Cd)^X&_!vu|(o`yZb?UAC&-5sCr+X+s}=fdaC{ zAE>vL1%T3dZYqr$I-ExMRaOPWK+BfAHBJi${FW~+LGu|k-cC>HrxzO+4!WUoRk1oV! zE;Q!tsb)rFdtVR0c}RXf+Sk1PDA?9I$tW;@^YZRW2JlC`lO=7T-kQ@A*edKvLUfV* z)T};n6$YT+UIfK`h1m^Qo4W_oaRmel&!hL~@5zhJ{GonyKXHTwQJc?Bu)Awx^8Chn z^WzH3@ozWsRrBr$oK+sPfd z#Cswvj0D|oFynig^C}>Gnse(bYy;stojD266nlWRZckp?Xv(TbahbN(;SV{-T(B(f z0Ix-N2`>oq!n21ig(M1o(C^xkxP!WFXR5mSMGL;kP@$nTc}@CdUS_;n^72qzjXx+2 zMkh-_7F@kl^$Jpe^^hh=!9Y<~Xi6=PT7TOfi1`(H-Q; zs&*mYy7a05!WJ?AxXrP4ValNiRHtyeds3|T*}>g6O8W$XQOp6VRm-G!&n~m)*dRMY zn%6KmHszT+GRvR>ISYnkxpA}W)M@! z?oNGm3JG%xPsWFIFLc90LMT-V=Jk$9UAHym`~mk3;tH8I^fAM|-VTm5JEqprtAW@? ziM$mSHi|qtcp^xSE;Jk55i5}+a2{e#3wD_jIXJipJt#OMKDBmzMB?qkbJqZ2C*KEQ z$RDgp2Fd-uL2f|F?7z_^T}Ek9(ZAqIQ=qW*pZq!fzxw}$#=)`y6RiGAuYV}5|Et&k zlz{)ogL0O?Y4Zxi%zpuKDn@n|W`DrNKTz9$Bh&voTId@8O{QN7TS76WMZF5qtp-^v z2VIOvsKiiTZw*$W{8Zj1N;;w~Q6*o*2aMp?FUpnDIJ=;olIS1p)IX%!oKDpSn_kDc zFZ~Ul0^t`cz>HET569X&_Ro1%vA)8_unyKFeBP?ETL4M1q{*cGBJa`jSWp28Y*FoEL0D3BJ)(}%^tGRd$Cs^isFdSQW#mm<^r-I` zh)*pZq?K)7l&5(CTdx(^uMQq^|Aa5l_ypI;?r#`sM0Th|+dmabN#;4^ef?ftts#L;O1VRP34v))<%i0Jx_x?u(UBA#mNZCNR({whL6 ze!mcCn0;^8J;MH;!GC2n0CNuiv1ZtS>hVCRmzYsYTL-Au&cMOV!VS!(wgaRPr&_u zb7SLRVE`(_0uwI($7uhAq=9aK_!Iv*8YdSs0}~4{d+UFA{S!y~-@I6vIT@JQfk~SG z?gbQV|36IQe;e!1jQ?wm{LR)-GO{rH6NCN%96J;9@d1y4QAx?k-bB^Rg;j&6V)c&izld6M}iP=A$fkqRc-2b0I`d1RZCVJGJxsL{K?3!{|tf^;-w1Y!#CJ-X`)|l zh#Q59qK8r6x7x`_0vrcEX?ytM;}-Do>iF0J@aDzu{@6$QxFSN_J-hgLzYO<(+&%l~ z92DgW=}-4a0IxKTbs3=n9nL}&e7ie)$?w}O_xFVh_kTOtKSL7i4(*TM-s=9~#wR86 zdwue1eSf^Fw+FnWBliJ9khhTp-|JibU$4&cx8JYg1v`BK=)}07C7`L_jHh2d#RETr(K>i%kvGUH33A{Jox!np56Oz07Ac4MZE2xp;oaqvq!XSvLV>PC=$TG440` zSu|<*M5nMQ;qXoaQa*Y^J_Ou6Os26(l$*(|`W4?&wr!tKZV zO}^m!%dY#!*}kuLTteV1UgAvA92WO99MiPg+xi)5=j)jZQf{7bxp$<6=J?C5Y!tFF zY!DUeWkw~_IhCWF%5|RXF^-c3IbL#rSU_fiF6E~#>4=MPMiFFksgZP&_Lt@du(WZ5 zbdF^|iLJ-e<<(>X&N@9Es?)6E)MpPtpEl?xW&TiBlS?^q;CgFfnmRKs@7u58EA(sbfOO$PE=i$K7|a zhop(~z|)3%l^0eNP{k^e(CniUTFIq=w((wU5b2>9;d}B1A5e)fHDmfWRG+&odu|Xp zYyA7Cchhb`u;rvVhU%HMuNf#2@u)6!eTo-vY0RcmO5`Pk*Zy=r$q+rYSGKd{9-#+@<*U3j#>T2LOZ%@t0i`Eu&4%c8R` zj1a&qW0$n1Jn+*t(vna}G$85oC^X83KF%bWWlYs4W&Y_;EFLc`I=mt=Rypv3-l$sM zA_E}WP6I9@g+kYID$Ct5OLfS~0U{Ax=JX!CXgV(<1F)H@IK+Xiti>&iVxN&s#$5AB z8oq~(Kqp1aBhn_)>Edz=S0;nx!d+!Qc#Ts^7$HaU^-+6yv(^qCtU*|=<-nzohaNWO zGZe8O>)$%zro?8a4=cp9mj4_ln|%0g|1}%w$JgJS_U~-{bmI+!OHjL;;hTJq>!e|3 zGU>}7kG7Oc$74UX^V&JZ-ZKX2C#Z)G6YDI5mdb#_RJ}4}bcOzUR5pqwD#XhgD17`} z;aF#paOOMa%qi%TrH3_Ix{Cq?5Nw2Z+(H(NvN?8XE9LbhZJx}dW$roFVL9Iwb*JR~ z82WlG5##*C<&d3_fyK$Xr@%7HNBM^#)064(z7G*0&d-vBk;~ck@3w8`)r*(q_k*i3 zAtv@XvyR-l{17VD8G}ag0WkKt<+&dPG9%A&JECmYXvi8PJQ? zd+RYaqI{V~mL1-cR4~L0TZlOO9sCHTVMrO(!;UH&s^_@}n$0s;_T|MjkwxzTFWsG? z*1LPWeq-Is>MG9sd}EW9&`onWZ|1nZ?#x7Y+rB)ayZwP))LhrV;$mR^f$tpBK0c7( z%j*M=@wn;b#w=j#WD%#tma3YG=`O@2KdW@`v)0sj|1l~DLAsO@+|tT*YF8avcARXD z5{yksUZ6m}OlJheGEn6>1)SU-&#v6dsMJM5bq0Q*ZA$Jb*^CYA=3=ofgAff>N={96 z{(-|*4V$D)289$#`xH9f+d6Qed-`|b%Qg#|tXIWE&~J`)OaY$#>P5J{;WN{@l-uaU?s zM;YM}I|PjbYdMkETqqlI*;>3*%%UUQX`(XV%m*n3={qP*pb_jjM3gYk$GyBqk=kG- zC)+8wv62QsRNCuUR;jeHC_O~MrmGGzprr}F8_|=^`e?|A6L$hiBk}|&=NXRR104sj zJ;KjShrfRVF26G)jlkXOtiiz7gFQR(p>u9mfrK3?_)OaL<7+&3_v1T&{#em5M3b|{Bt5SV z-<@MBvtm)D5LcM|+qVl19M+&b94Fh9g29;0N%&fcDFKa(=bS-|lOu!E2R-&{x5FIS zH9^Vk~HWq65{$E11P;Y&ByafelRe$$UoGWcGCqv+QbC1xOPue$ z_LV1^RNxbg@f+=C*F&NscOu&DJc;&=M7WfQ6JZ;I&zP9;LzLnJFPGQjaF?cjqlAAg zK2VQSLz^Bd)eo{=cf5S{0N5FMB5Lb7rU!Sks@=?o(T+;=l=c2l-w>Eq4aDuZu0Ahn z{2nZZi!%>iPwB-)<)u?ULOW2I=9@pIWj3beg7m3PNFA-ffLMBuPY8t5LY4mJ3%Ic@ zdI1ejW`P5Pnx|vKN4w{w#>pXRhfn)b)m*pt`MfyyGLx$1<98@0_eDC_3TToP7E_!b zr!(+Oi=c^7=H4Byvv;gjEyG4a;$sS^o#qsIqK?_LM<4mA*ukDkQ79^A2mEQq@JG@# z=G0uJa_!4Sr}l$}gsI4ZDnlgES8``Y@*9k|f`FWhyH;^RcQ(ZFwU(Dq7wx!iA z5w=L>5Sb=$1+#iZdP|k!jU0fo5T%Ps`0$I%0c%z>4Y%+@6E~;yvTcLhFZ4m!6KDcd zR5ANhmo?gP<1|oar4o|h9bLL)d$Dgk>eL7*y)9al?o#mJDDf;V3LzKq>l-A@AkMf= zxW3tD$>D|}$d(B*kLKg%NWHfa$XyvBmZ%XMT6G11Ryfiw(yQ!Rl;tC#zZ!MR`WIhb z2G3y5(+On{RW3g+&u;wRUyt(zko+I_#~w#hHU-CVsk95jbU+vT?>_d({kdj#>+N@u z12afvyPpK#bh%z{huVZ_*iY@>uZJiC9Aut38Ln>APxY6#6Susdu*|8g+CQ$dtCV6$ zU4958r%WF^`0ihA3wGsxT&K65X2$_wIHzICTVHSQ1-JaZhlHCVduzdnPyld7+M=z1qVN~SY=fkqir&QU))**~y z!X~~o2=lt!BpHF6&Wx_8CA2;hKS=mZs#yRP;XY&=~pHq*`&L&ud-0$)^XY(#< zun!2Vgqvll8L?|*Wo+K@lizM$o5i0t&G^n)l{o!*Qk8Xj`UW}mps^Y7f1IzCtk@w* z5tmQ;2H>VjOGA-=5v{#|f>E-m)l})QnV5P5AMdS%W|v<(l-;b5dHf%ub+4E??RJ8nZjp8;*)x=biNFE8|7O7=3NB6;W$`0ZAq)K4auaE2WUAqDYeYCeD zCQzEHSLKuI^Mh72Whp3CScTlirtGX4Dd!V9m%5ZFhf{jwMhW%K#N>s)Io9@`(~tF~ zFG8IJ@){whf#@h11HwY??GBXmB6UKjDg-1!0KCj*=u#1c&>Liwjm?n~@d`dU@c1*X ztQzPR&^ht|R5+{6W4Kn*WOQLx?zREp`5pHVCNR%J5aZbz9RTvVo#{0xHB`p}s%N=T zPm2qx^QsAZ)&MjbjJL)oFU?}fZUTAZkcwJqXi4~h4uVWR@UfmPIw5bP+1Hf=(G8;F zH9wCB>(y4dBycetcENX0_Vo}W2pO$C5O3+aE;h#p)pC|1W?55aPXf6_e$%7Y-hgpH zei@xT^lG*XsAf4eatSd^KH&-=GyceTz-&~fjd+(Q-h7L8@|zR^KOV*P&}JFNjQ(+k zr6u;``AD5ST>!i~W!>^)L;x4yntWrsC$l8BUufhqaD!Z~wzn?X^aGJ!~h9+mEL0+ZS`$>`miH z)Iipyj5sGp#oFHbTFN?rr{GKwJ?t^g=}GJM)3!0CX@ihVx{>R^g@Rg^8e}5rK?PSS zCQf^8`lvZFH|XcD_95`^fm;Wx5vUk&leW&YzD1lk2t_4EebkLZT({eFO ztjJ|Q(MjU)V3llN&P{3CBuGOd1o5I!8U*fXCtixD8Pzu29M!T<=w}kW-(n*AKkw#m zfjV%%ZgUE}UddlPpW=xwj*S31->lxy&Puq1sedHzGSh%FnMzT6;}9l`fsl!e{D|LW z)&@sz;qr|Er!O|-nH^D*@l4#+*1h1gC+OHZ^H2+wGsEgIFS<Q8GcE|i(iEJdzIyc@b%0!1>GlrM<2+u$1Spr}0bgSlE# zmwqqpu9Z!>xQ^yp1c1wPKoCr!t7vCO7tu?Pe1uP8#$XF&ST6OrF2Vh<`g@}4b@?T? zlXeE8*ib+-+JAy}*j{qkK01h!Ho%ZaMDqbUs9+S<0ZnoYh3kG$(YN2qc9`N5&DSub zoD`ke>K7$$_AF4DM@5}Vho9=1b`|)SWSSLa{U0!IIiz027e5t3XrZ7V&)?j zx`Es}6l*Pco;k4kK}i51ETcGgCEG#%C^V;hm}J}bJvk1b-_xk*(3yReC)zyS8|{;v z-pNIHJmqr?f7nvLJGscodxjN6X@ez7 z9z2p(x>Z)+_EqyoÙIskNr1Uaa zeRl3;k_cO(9zN3@-^jg)a?1D(Lf7tZoZw5jCZTQ)jZKN-CAm5-RV0nr14ERsLqlb} z3O2>6Kp7m+sAeS1HgN15Z96MbibbJfnYv2?+%IOVqEv+kl30qYL-f;pTwd$1f`2!- zAtLBs!5?4`JmZwqsR~%Z;PfcsJY`8@;(lAp)CppS;JpHMQ?Rw@@Mhb$ zj{Tlh0npfAKi82#*efyX3bo*cTI{O@gYR@g3ZaU=eb)IEKjfD!sX84u$_L3as8|W| z?LeqLHb09EUKv(NDkZzSV^WoZIF`)VeJOu*(Fc$8t`Bm?TBVW?khZ7^HX< zH!$UsGMsaYVkMW?0?a3gWOmTZf`g*tr*mOTsfEk|6l!=m={;y1y#>mw1(b^CVCiS^ z$Cd}bWDd~eq$`TvPqMxA?vlVG)i5D-aqI^4jh-lJyuhq-I+`^8quvQov)MFP;Kr09 zSTdOlbP-VJTCdGSZ(<}xr{n+ltldD19hLXUj<>>%0C3#4*BO)%Qn`Htqe}uH{=N={ zA1QT2&0C$#M%A*aZ7c*I_;l1r5ol)oMq`a31Pz8hIJuo6^ikQFcMYO?m;2(!>MQ!G zXfEdL^37bF8)`&~O(*uTAP=u74}l>{nu3S=7a%#-PT_(1la%RWiU7SYg?%$hn|ev`tmV?&SAv!#J_iJvXK2T z&zzK?CWAYA|7w3?Fq!g4$V-E{(p;L7vBC;vx_Zk=sdkD0L3lRYd!gD=kpATi&?Ay_ z5VV+^P+uE7=InjT0u&2>ZxhCo8?U(JTb0N8O_{Wo#Afx&2FkXR*3=GYcF;N}VYjgKv zwhs&~!ynBK377v@Veb7YqTG%T4f0+}^d*G{^W>ph_mL51-};o44q~1Uu*QrBW4BZ&WhI-b;N5x)EBn|~7aG1fjC?zQO zh?>5q_I?8W;Yq-vJ7H28pkug6-`fGad@=eM72I8dfd|WJrwNhd<;Wz1S?Z8yahEDJ z)R{s~uvx2PzQqpx;xFFQ)QK>Zgzj^BOg z-CtJNm;X@=z%VOlfeI8e(0(EQ<}mMZKSVYn#zKoFO@fKbTy9hRN^TFi8n7!AP^or8 z#Ex_=M5(8B8qqeS^$hX22WyzjSOsET=)HYm);J0dUVLqBR`lG?enSkuuX!dr2LIy# zn!5c0;3u9*f?WE^+V>-whl_TvE9F^$D7#4-^hnIzY6HHWZ}8_(`+Zq)$o9+nWTqY2 z*VyA5Xk?bFO;|(I&lzq?)@a+cJHj!wpf2=%OFSpc(L=d$@*^P1fk_>YRJP3n_fkG&<@H%*t7dNkph+63zppuzly+C4^XKv-IB(jm=_g~W3U44~l zs=o(1q>{XH#bkuAJC*t(U{4Ji6b;x4Ip-+VN6# zo%x&mIUhB{(;uVxQ|9KY;}7Jf9g!l9tFXrSKsLvn3{o{Y@vyJz?`j#4 zETu*)9*fDQVAZUm2g0m@bw&+|i=hiv*u^Q``b=lVOA>LYh1|1#zE*k5TrL!AwhM0R z(Eb~Pzg8N~bV#HSJ@fTv25f1uS;fyV8^;+e_r9lE>7d3l^S(1!inP+OG*E|LGOQQC zY?WyR_OW5{)<`w&fhvo-nP>z9P_iy2>db(Zi!#1%5u+w zp6AjyT&f`Jqu%ZS%@6_z5!0NvV9S>nR3tQ4&m$`1qkZzN4Elu=?1{5b*akT^AZp+w zml1?&={jJyFYmO+@X)$iaD>VMfEz~IO)g0_KOI}BH;tpu-#TMoom@(7s|RlRG+{ed zdEhQXc11>2ogPDVj9PV;b5%+lQQYiP-Kt$ndts?P%QG9iYi+E^Wlr*8{F|D2YpDVg z#3`@~(7NF%r>pPpWNKM%cL(b{3uC89oPX}1@_z3_b9!kN*PgSLuxgr^7cT&YF+i3} zY1U6Gv17*ly;Lhb<|_I*KAm#MHI%8^m#Ge!ybG-Ksu*qFW?7ymJzrK`lH=wdc>>** zt%!R8%V~j41V0;fCso&PZk>hF&m%Q-x1816%k!RcG+E4~nA2945w*W-@zSwF0>$IgjEBQG_>xc5q6=**GJ9V$6xjDlX-xw0Z}5+K;?Y4vnzEEe^U zA^oQo+-)Z5RnPYfUWBeU4@ih-OC*X3&f~vI6j)G9=mzs!KD&epe zrG8FGVmU8jHs_-yJ4hOy2o{6}HZ={c*1_A0vE3wJfJ*!%t+t0<+rfcAB{<$aTnd(_ z<|{^B+sP>1$wK1zb}0v18J6SDO#C%yH#0e@3Kof(_=`?}Jb9$|r8#o>r#L zo64)XP}jG2aq61E_m!_Yd{^-2CVp}QT}j%ZOcLPR?->E!Ffw5*z$Qp0unEDUNZPse zo)O^@37zOM!S@(!$ZDOcy5o&>YEraoPl_Uz5LNOh^DrnjkbWBhACKRag4jk%2^BVT zzK~)0>`~*h5EcE-{B?$^2|}eN;fY#QR@tRoB$EUOy~6SHkDo-4*F|5yg8nMM6&I1e zLDHJ)hIjiVl-MDO<5k`_Nzj16bIhh3)q)^8?$GJ#{i81AOCF1WKVPb#|sz%}5WD-X_2Dmoc#dimgm z)*7Q#NIcHqHt?ITb~{cvnGuY#j|jY}D(7#cDvx$-d-%nJHCZnH{gM$&o# z&<`p~th-cWMED+z5bUackp)A=@b!Z0SyV0^tn;>qsaJSP)AsQ4d9;(y5l{S{IjpK!GX1&MIsM%u!+@oM-dkAyQX_5KW z3W}v$vUSt4qO%YE>3SeGQ@3ld_8cf3iA{S3GG|#)+VV0I)LJ&V%p3FszQNCvsoN9G z2cY6?5^KbM?mZh~FGDPMVn^u+h2lZ({?cFG_JhtZIy8|NYDZaP3hgvbeIFX#lzOh0 zpd!^a#jQ2!Ka)tn!qWcwQYz?evmjxz3}h^_I}S^LOn1!HC9P=v))A^uAuO!$Bkc__ zp#|q$sKMUw!+D)ZgBd=GP?C)UgHKz=4wk3;e(x6JgdZ|hy5k*9i%>~+z{Jdfpapxr zyDDK)OnRf*%U{-eE=j=Fp!;mm>kf8izA&I9b{gcK3C>y|K9-quuLRM7#g68nu{SX# zefgZ*xEYq!5@?qDW!pY(L%m@xj7J1Pr|jeNvRRACVAc3#o8KsEwEN3M?E2Cty)8Gp zy_R|?$U(`nHTB^)ZX|``^UQhQAUtXfnRv4qj7QIId&1+tCb^ zb|2mEcXyi(n44YS48NJbiFZtvbvR6d6KN#iqjAu0C`8*FJwy~J$+3wz|E6f1+r6*m zv>-yFj`CHObpGPcW2+}0pazSOq0qWbyWX`=6F4x(k-Lf5vdNnV*5IbSZX%!k1)jBp zO)MbIcH^928bVA*v(MR!-C)a^u4Q&(WiH{xw7&IR9-DU=J|n|pAmSx(Bh~y4TrKke z*#>-o&@$FPPUl2DzfdJl%ww^{z&MU}GGgOt-}XZq21Z3w_1u$_vifwuiPi46s5`MZ zgBACLwSUPVhVC2Zk)|8kM}B5&-!tv^&W=T!SU}6OUi3?zi^>J$*yhxv^rIya)=gGk z*Xz5L;tKz~cNLnWZVG1C38%NYtJs!v_X~=Ub@o(clpryq64PdG6XF_`r50n3#3mMqQ%o!{kuI=_K^jm^3^18T zpp_c~WPW6qX2`)Ol2W5OPVoI;8DMX2kSmGmunZX;ME2Z65?K``llu%=%0nMB@?sex zJyc*?o*5PsRE+|xnTi>;=zw0JNY^k zThcG<%HB@+@iOjw9mC!r@QFI3yy$G%dWx&?QWf#0k=KaO3*} z2iwFj$l77>LH;@{C!8t1TA#~&k9tkFmF{phLnYvjy2@0DRUEwo&2$ZPcy= zUCpm?h~z>Og}}edbVhMG4Or5Ul(qwAxOt4el2T%oD1)y@Y?<4d*lXzqIBv zq}%&{Yzn@=4f;NJ06JdJF90vM0Kuz4{f)y`AL&q)yF~*h*a7vq!*D_0=X)skr(FZV zwsFAw<$U?J@5iWq_s7$Gt6)1^$M}O_oxze|_s4v>!AG?7lz+F+hoHb)|3m)!)4bs8 zdxzromSE1^$6LAJ`|UOZ;JseZ7cvFCEW!71K?GKiP^w}gSG1;bNk(N z_3a`30WjI2_;Gu0khlFYk^eD%`10X#8AsTODO;rGb7pjTR{MB!*qTQJVGyO426&r1 z9>4qe0&{fxx{tTi38*=q#xkh;_|?Db-hV7B*ZMK$KE2L*H#U`jkvEQs2hlL=T!<=@ zgemY$Cax|6ua6J`!kA($?WK~@m`)y!egFm<<>cT>t6!q=Sz#fpnQT1@ARM~x=ax2xlJ>B@gOYz$1eZ8!qE+>SH3MYM=BvE0^ z#705}niNCU!vhC_sx-pO$g)qTCMIMawMY;CmsnXI+>`uhWRB_abV9HH5b}bDPI7h>ST}M<7S>Huba3S zi!M&a)4O-xY+}S&2IjySzjrUc=9nyV`9}B3(eJ5(ZoENAlXo+lym&Iu z4`iILdDqUtCtU&*>|Aj+HKes=8Ht*43@Ta1P&iKqBXOjP+$1At;+UUXRiBEejqbJ0e}$*eiNkZD}bZb_FV zB*X1aQPyb;G{X}nz|=-`38%=g z_Vo+0x`>KJNTG~7>V?==qQXO*>SGKbEBEdU1e2!Ls-RT)E~sUkMAho~0V{m$XK(uP zHg`STF4BF13V53EfIl!Z2KuTw4L%xtn&5*lC6fDWPkE#OUTy<-iwl7~ zf4ee+h<%7q91@;ul5`H%dAxBrSZtA)18WAOAQ4ztED<_%88y&$jO%pz^DBtV!k?rE zLW#u#+$^GmJO?sKMH+om={VQZgyqR)#GpIN6|~EO3kA)KbiYv20f%gArou3@)C>c zWrhqR8*bkMTWF46WW-6b7PzSa@HVyR#du_&l0PwBIY#oOt4T%((ZMF@n<=C?&yC4) zLU{Fh%6(#~{@s=vWRmRE)(RhPr0YC|n?QerO+CaMV>5-vfrQZL48m_EDpZzdQo5re z#fnJ9GLu6(_}drXk%!(LFEQ{4f7G-50rkzIzXW7y2^MXb6P5?~KTJVdQ+ zJsxvuhD8pVDSelRu_hKM&-AF5*pOr&3XTpDoTpt$7bmL1$c$H)vo!l;LmBN7yp;N@9A(ybI4&P!cZvRuSLr_{XtT>~N=}%76 zsUnc9Ih{3{$0qQ87>(Ib=?(0m7OdIja76epw3r7BjTKvY45fnHem}mc`7_Vzii#g_AnqTurij0iRii(V??yij58^ZL6u9x!rFB<7Hhs(xM zo(M1=YvOyqHohu9{*aHnLpGY_DAzyyTAb^i=6#FBCxX0eOj>jipC(g=TqW*ug!J+Y zG_A%P?TwVJ?~04w*N6YZvXG3db&Uf|=ddhLe9*3SZWskWG) zK(H|AIs!)mfm001N52BlmN2`Dc~I1{i1Gp%q=lDY2b0Lv+T#VE@v8%LfP&};Wy&Ep zN)UWYum^O_?EbKKD!vLp(qDT~&`d8o@s?bNx z5A0CyVBY5<(UXGLJ;(qtY&I$AsSg!(9M$Fb;l3oXX&jRW`O=UjB%^65P)K=WnXHd} zvLc;3{Af$yD5uLIs7{4vm;zpB6h&{o;oG9|CFta%88p0f@{gMV5Y!Q`{6)~me)MU$4AhS%}t>|l4yUu==g@) z1I>mK2sDY4o{ll}cSk3_)+qe6)kC$iqWVJB$9z(bgM3Pb!v$xQtQK}6+WYv1LFz|= zxK~ZwtdxAza8)-se6B-+y?I4~j)E{esr|tC!5dyY+jxP-)w1s&bxiGwymJg1Ec0k?T_R&U3$Uy zk*B=p-Yaglu3un*giuO9p=cEF56`4c;57G@sb%SqtHi(FpSE4hxdC}%UQqGAzqKWF zPcL$xIOSe5M}`jm_F?YB^Zc%+tzfgVCcp;=5#8Q!Dt<;F#}PmKIrJuYRJiZwm%73j zlE^Lp<*q@1#AyOqPX99+`w}=zAlh>xd->%I6Fgs+FSlV1!F((h!qX%NzZp^1^{v}P zQRCMXlGv}}KZ4zPP%%#F0$JsNeJmv;oEwVy#OYr}i9fdT6utJfKvL59n1%G)`BdnOaK^n|N zg=1^fr0M@O!6UE40@he!O4S-!ZzWC;C=2_Mns;2l6kk2{wYnftEZngNF4Plc1I@GD zHv=8S)aY;-=H*qe{hJxWKOum7!~^H{T?!j~dzu%uzhCV@91TE3kVSSd5UUT11|T8G ziiRN&6YaHD`^Aw@m)I-XbL0XqnoH(s2yfJ zCzA3T0-h-d6_d7h<6Mx9*05WN&>KRHcdW##%V~QXE6r;z`M0jh>p&t#whf6|`vY2; zAs%vQ^M0Y~3lmn{rCe}~CVAA+BrjZ)@S=?ke^30F<9bSm5Fsu%~Yvx5AkWIQ9h{Vq_* zE;vw%>r<O`OB=7F8T__oMBP2$Ew9 zCkzjhhU%&sl&k|OCE*lTDF;hM1HN}*Ww1m$T4tTsR8crjN#V642jc_J>(T z?X|%F>PhE({tSk0?Fd1og*n}4LLzbzUm>|a5#%^jj788^*?S;0)NKlp*~x?{UNRXI z8*mh~?G|C;sXZUI4{2U)H@+2#=&}cmo8F)qDE(b6%l+0~32D%v`W|!XXnZ=cHh}7m zZs;m17(N76ar0x|mb2eN=&TWM&r`WVyD^QJV)a?%wlNY)Ql@7?-WSZf4PI`1BbtEV zxuM_`ti|=5e5ysmhrZY4`=U+NIl;=K(P_{1eWUXW2BI>eO9Dg4gO2nQ@SLxWy_0U> z^Cvlr@2@AVfD_tuUnbwmoYga9Z}L-fi{jfIhU0lJ8E$cca^w)8%NVZHF=bcB*@{up zMe0e&qOmLDTV)BqXz1vzB?Qqt!QOL3ACqU-`1vzx%7iQaa-NNgUjIG!U42#v=#{Ps zDy_B<#i6wfgpljLI`faC6g)~iSJO9pJ#XADD+G+{WC>K%`J-uNdWI*q>4HqS509kY zn_HKZ?|SETb}9*aYY8t-op(`=KL-es8aMXpEtYjiRe!Hm?v=>-lhXz_JWY3M#WQ*k zzO}NTRe4o48pN2J+;#NehN*aitb&FoF6oRDZ-<<;_y`Gp{X;vA!XP?%d8kHpB ztUs!)y`S%{I9!^~g}dmPFB^Z>QhHh{eZ9Py(dW~5O&Cq&-d`e(B9y~+VRCY86BX2 zdE=KRHwubI$s2G)fXZ$%Qy_JF!}x0Smdmbq=Hw)hHc^1;{Yv{O>*6_lRz1t7XdU4` z?C!RD^9i%cr;{;+brWsl;b%#C>#^#rXFZNI!7*W~QSaWws~M4`GC|`|XYH=sEYs#T zQ??$Ih)Hj!2UxgAp}t<~Sk2f4fu(yZpAnA|G_c<-jjr+Fgt-+*PNZvd0M4^W< zD)+AHF~$NvdijHJmP2sve3DDeZS>M79Q2}~CtMNdqe#2PYPNul%Cm@2UPI~Mv@NO< z<}>gl`0?8suEZr)ubU4v--b9#EE(GN>YpX>DlzhfGGui@$_kMksm2VD9 z`G$aaFi4}(n&nFwB(Q&$lc%#2og3pUx7IoTjBraPb$6Kra{+wM@;(6aJl)1ntpd?= zZP{f%IUIj6V_OY20xL3=AZACODwsGs!|@qDUVN)TmFu=a=4CtzP8=rCtL|jZzdJ$0 zzJo(Q%>MP`D!Qxes>k(YQ3Ry>p?bM zC2*g`JAU9CRfVOpL6AkIYW-#hOk(Odmvyej%i73(IcrbTbUNE`(C9cim(ty~E|`B~ zv)}ogVnKt`9hZT3g98Drhx)o{rJ(x0K^YdqTl_?`!YOgeTd*(-{GntsIi_^a=J|Va z^VDbS75nAk#ma8*vauD@qXfB5H8H7>j@tDL>$B-SmJ65WC6gLl|It85?}^9fr@{Pmn;F+4Wv8T>Wz1MY>%>w^w%CF@1A%-=#eMC;bt)G1U335Digbhi- z9id<-SbODGTuzY&T;Ryu_^4754$~XH=ng{2Sd?SE&H38Bh*0d3&_;I23dkWTL!X@W zRHVfMt!}XN;6wb_Q<>4Y8RkM{KYe_Bl2^It7nkj*c&ce^EGE45xf;rceK{ngmSwN#jI&8}3=8_(6-xF*u_MMP z=!a(7RQ`Y)uT~MJA%TcLk4=vd4yXsWVBZyTNk9F8YIm9aRFzX+Ihd+Co<6!LSVqz6Jg4Xb$!yd0%jBnBb)%9yMteScBn< z?St8R`i?%gV9%0^2=5*`(dk4sYoUYGkUfDZ!)l{9R72p3a2OM6;k>0Z4!$5`&k^)? zr_pY2!7&ijuIhrgTcAOmMXV838XNRtLS%*_`ULDM_b`6xNSFyP_l?yqNh{CP7RmNl z)x6kUg1)EpUpm<8?#}}biG#P6qH;}8RNm{?O=$Af^aWjEdRBys3IQL=;4;nY?Bg)l zMYfi*q9XX0so^qPYwhDyF-h=Shi*QA@6QM-N2U)=s6eI4Kg)KvPfwM=-Q5_pQG5LO zI&j(bdm3WUg?h(6O{B=cfA@(*c<}5=-$J6fp)NH*yl?(48!v1ca~cQ3R#4BIZpG=W z$XZ`IBj0tDtAqcyV8zrz>s7vM?4q-#u2yaI)-?I|Pa_e-R{BP&s||4dpN^j^XV{_U z%sTMOMS-~*HG##hCj|R6z|Ud#e%eu|Qd9Z^?hu1XZt#iuRbtZBJN$l-a&<23(O||CdhfhEC3Mp^L^FwpOzLOuP}l}+U{rD# zn^KKDP`77>X}3AimSt&jkU~?6B}m2v9)(P!tZ$5JxyUR5hf8VRL3zEesc|^+uV<>J z!bZ92(SvLVf#y~?Er*ABG$?TXbsU2zj7U2*3`bA&gVE)CgJJO-{LZC?B=TCb52qWt zS6;BN)8i{=zr?WnOjKt8TjfFLYC2hThpS?PBRI)cb+yd&Ol~#zeW6-czry8NR{?Ca z@zmiF_LY%~CD9*P>7k)@LLTqJsrby`7?J?a6)ylRt*AnXpGD~Fh?riv;!~{F^2En# zhIz48*yw{1?l8ocO3qV*BJ4}*FrmK_62D`utMi7SPOX`(sFVwfWxpx>G~>-PhA9lVVB%O%uQe2 z@eXJ7$i1{Z?SPUwc5^xVJboM#Vb73&Y;TokN;_Y|FCqx2!_pz&M_aDsC=($zWT+7o za(oAo-uVjGY5vZZB}hEWpu+T@&$oRF_o$zf^FJyh{=^`gr-7TZiKvVPr?#rC2dxD9 zG^)Z8nU4rym468m)?W=a)*C)}ibEqp>^6;sjI;UvX=t=JE;hV8)-`T4=5_9}3Q zH(K5x&1$< zHEt%6yJ67*fT+#1j7P0=%euQiQR4mqDmx#xRMW34+fNfg_JKT+WZfWzOe$TND5?yl_ic%@b*@PoJf%Im-cX!=J)Z^2Ql1R&2hKV8@GLO9yggF-jIpkPKBjVn7}bLoZRE!>dmu4{4d9uj93Pd?~f z!!0nsIBkJ2yk68*HCVW4V~J9fg1qLPcER}@LGt6UPKZ8T4;`{gm~Z^+7*KE>zZJ=H zi&~hw-~PyBeI)YN!{89i?Sjq0-Z|E*MA&eiQYy(WKH=E<$UU%SCKgyZBru_hzdJs~ zOxEakN>p$eqeWb=dgkg?l7Dq5a62e^rlSDs;cs5{P@&KGm4mfV#o|t146o4z#$xvdsc>K=x=ryifj;|oLs=} zyj5>!*nPac@(s|UTUZ}R3mIoSKYzC13MTRC7_wL^r zo7hw};rAh)40AL^Ml*yiu@3%YDV^ez3^Se#WS^R)l&pP=Z+;GxqrbXus_eRbd@=zx zWRw0XK!bi7JYP}P^o7sf3-RIndKp-xnC2ocEdF@fpjLZ%pK%g!d<)hqbIjBf3U z%o3){WLp!-lUU3vs-6F__>=;5N|KK^xLSN1gqS|+mzoJ zP1q9t72yEfL%M`}zk^cJK-j1Bp}nrxGIJp!rSBi(agz&}MLu37dgPT2<=}iq%ZGGk z?IA`O>-GSLfN~ZWffq~yUk+F@bTf$0E?(cbC;v8pGGZsF7wEhXRJiC$)vKgg*%fMO zz(?+VS!k5?ldU*nZ~ElR-C3Vh5aio|GYC%lT5~91`wh?4M)J<_E% zw|hspT+c){NGzPpyxLJ5?(RpN;Q~Prq;$0aGt|XT$6fPk9cHM@pR@LIK_;Q}*3U5{ zPNy*F(_QeXKj|8XgLY={le(CBD->BbKO$VY{y>~x z&Z?&r{Fw|c0&1L@iUc4A<+es4o|SaFAZU=H{A0j3BJ~V;UKz4aVaC>{Lk1GZx?=w2oFsJL<=2dR;9}%WK@IKN8 zy-7SmkqDkL{g-|T5Vy&DcL5?u|X zhD0&AzJHq!Z(tA^UKx1G`O{_H^l_bP+u`FJ1& z?7q8j%gEzKm#By)?smFx%gXDsCr>rSv|~q#ZtBwpT@mNaaEaf(QXd}pAAPL4yY91rF+bhTZTn+yI&k}+i}Qdm7$ zmSz6m08?s_=hDfr9YPx4bq|%*(%DEdRFYtHj7N5=A(p*mj)g+vAbx~0!aMv<&Xg(6V7zf4wdM0=ZAumZtkza|Ty8u;ND zcN2s*s!s|)oqiEm)RI}Cwv`|P?MY=uP~=dm87_A0VQ76N>wB`<5R!0s?E7wvM*6xS z*M|ksLdFDlt0hT{QqV2<{gPJIjQFVx-mWHv^Y?%x;G{89WKKqhtVuuJI`meH68$)~ zoDJ$~jG+p3+_tl(V3a|Oe47>e>I`}^g%t{&(Gjo{77xyhR#+&1lnM% zJpaWqX3qTpP#&UhnYBok?fUWQqBOZsMN|l{?>8hsWvFHihViZ{1Ev)df+VPXlqkW! zv^W%k69R_PrFojj70&>U?iYYYGR-Oww7baB1E?S3Js6bPrf~=^l^~EwYgf!kclbqY ztpY3RaAy?V{_PjBZCq_EchzmGt;$kA9GuRt%{gT9p={9vRXx!i>z!Pniv)`*&hAz`NUEy?<@Y_EN%m`hqN_=SPn=`cw8 z{zrbqEx@QDrPzQhn7+0~aUDW9|Bs98`u?%K23S+$25gAFP5la3QwBiYafs}#k9J?X z#GO|Kol86RcFB$Wdy;nX3vz~Cx&rdztfHrt0thbkjen&Z{g&-P5n!QrP+&2|c55@Z z#5$V<*117%r9)-{UP@W(eTpJGUjd1}cETRCoPG z1-Ld1>`+N}D}sqGrR7z+AsNChKD;}@m-HTXX0)6BM$HSzIPC0QXv2LKL)xZ9$#K{@ zv3K)s5ERDTrsTdj@FNKOTPo>}7H5tGB2Vz`O`&HQVQ%AQO;&eci@QZkP-$-7=8;t} z4Nz6)y&nxS5Wv2vMr#S8yp-TKI^aLJ5^?cehiE-=#`)Myt)f4Q)vZ%rUwjC{c@!%J zN%udkEOWoZ0?ZrXU(OC(2VVhZjbYEvGR*2|JExomo%bctmyrPD#^BdieCAgasO1Xq z2REE0kPWTtCvK_yX!0NLg z#k(s=-oY4CC%|{+79KpqiH{95HW*-6=|u`xaMLDZA)(4FfD_Z61YRs+=zz)r#so)Q zvp1*k9@;SqxX-g(F(O>7_cvW5ap=1514qyZk`yv-$eFxHCPu&UgSv(S~>p3bLxFBmeS9FGc;Tw0C`;$?4Ud5Nygr+c9g=hZ*84ZG)Imxl*xOs`W7`ME+l28J+3x!{}(gdo$9|5vq z)BMaP1=*NC0ph^!NiNPgd~cp%E^d7MlqYp?p)xj8((MXu)=qc!M!a4Q52t*$M)?kn z>9w)s~2`FctcO$sZC86WoFW7z@5*?4+T-nsyHj;v$ z2lkln&oOJhg`OB3uY+!Dw*yU;TF2|#3c3pIEG;L=9+PSf9GgUCR@i(lqoHh6L3@?7s=yZ`|FdI$Z;MXF@O*TN! zU~Q4(Dtp_9<@hAoZL%)ZszGRuR8(U*eKCi?aQoJ#vCcbKqHlH8*5VZ@A+)h^edY;X zs-kCQfZ@l5f`wL%M_c<@^8EdXLC*X;(d;~>$bVb0`EN+czv~MBpQ+gV-)b-aRBZke z=x|No$D z`*m~@_8RQJ<>=X)3@1}g8~WLLjntr9?S&NPs}r zOXzK+M%;{0$p$lZCm;+zj86J^yFJ%-yu75qetR69R6^bC^qESzCn5sDD=-B!Uif_N z$P(Ik2UTu%J{2rH#b{<6D5VRI?{?~JyzllBZ3w-L_7Zt}-Cw#`#em-h=As`NuZ*iq zHl)T1Z7K@!3%rM)-QHMMUVW)u|NZ!r|Fh7$;>i)8UX_yYq~43kyOq~7uR>1Dp57N2 ztc6RD*n`e@OJ{Ih2Zp`(*V&xxx83XcP9cGXUE6{h>$VC{%`Xt|+sDxvdR1S9UwRzQ z2$}4LXsT#_c6vd#7jmR1Zayb>1S^Ehz>UYGIPvYzj_W<%aK+DJKMX(QYS+-u$V%>4%7*hm*v?)8;n@pQnG2$KL4PPLTbzRFC?OpIHV?_%*h!CN9dRQTW=& zx3`rqcrybWQGEZqe0ZBn;{JDQA|~6kC4(rrn=|0^H)^m07>>pxrhHqdMd{B!gnz2W zR&4D-F#rh|fd0@hMWPOx%>W+QmG8fPG>0(enfj(62{*@Nss@i43%8>B8$*a-#5)LD z;$pxAHvOuop=^Nl>)S?K17TY)v5*M+%K0VDcMpQ3P&pD>2a>vht;LxwI6Ip7aLo{u zly~wd)St}3ySsA0$tP-hywLDr+Fp5r%&Vd;MA6ux6`CCR6#b#$8~}CARk(E|fv^gM ziD>AM@j3Rp^U=F|J3G~Ht8^+&iaVS1O`*vst7i@-M(?LO609%z-D*6~vmWj>V#czT z*H?#YREe2}Y$M}5}Yb}e*1d;xz0 zqeM2%d??JYn@}BDME?>?T`NmKD(UpjaKfg}K#C~-cxwY)8Wu-n8DmkqANMa@yW!08(R zaLyZ<4U8yZ;80>`iHHj^U=XnP29ci!ewhhF`fpuwMygL})sXpbZAnJTjNr8t{a9VST$cHd~ zo;84_3Y}%1UoekK*b)}JZfTG_*#?J4Z2w+4ovsio9aiEYiq8zs|Ao!)gdBj8-*_9y zZHU$6A&HL$t)~=r08xW_8@U9IECJi+A^TfV!Xj!d9_?G1nfPS*?hi;}oo^t<>m`p{ z2T`QrY(NGB;Km@=QqbDf4;!koxVHfZNK62ur4Vw45({K*^5Db=K0ev-8CgzDoX{>&x2O1b4Hj<4#R zQ@0NO2}Qc4gPz|VhCI}dms)Y*5si&_n?UrFF%{tyFSIye>{i*5+lQS#NSHD3*82ur zB?}-3l(r_dZN}b^)J7y0-QJ&W=cwrC%Tf&_QpBR3Puc(*4N>I5EUSH4r~K|$x|xAa zPKeH=;Hpm9S?^Z|M$VQuMg>^BK5J{ITa$EC403kP^kevDF??eY=r5`cyYl?`rBe;* ziG185URipr9-4&caC+;NHYkDRWm9<_27Kh`KRaXv-m~RzPx%dLg_Bg{a_|oPOV52t zOGw3ByG)m1JtIsAYL~_`PLX$eEqGS+<5U%AC>@&IdPmH9E=Q=n=%ShEQ!@mB#BvvK zS^M5t8LySXywgjzp!;`XKAY@f$3{`N3PPG*{rPuxr zP4g{MbWFC*hIdFFFf5^vi%CULzE?Fqx+(Fm4kl#%5UB37s|~1SpBu#d+5*WrDp*=o zs3SX4%w|F(IaSnznOOYg!sJB}zoR43*0sxzoMGq_?-DW9Q43?yG87u1sUz_m4fZRh zo{lWnL?0Qs-w(PYLO}od*y#ECJhxT;ZTJHQ*#Cy8?6^nXog0qjKW4*ahKt5f^ZO2`NPhh3%cJFN|&m zY+}?4%t;wfww%&sOZsP5v|5bfG@`epS_#olH-m_?>Xh1JS%5@N#6xbOsUIODW>QVc(=IFS-&bT?)-8+L)hR)rzWJ~XgHcqon9Jz`yyZoUYw6G z4*E%HB*(TgJ4H3gG*sq;zXJ=;YB$tR>Ev!%@_bv$SgcWuGm{Qm-B>#EGYY}+Y!7Y` zT6nW+>@YDZ#6DaJjVNO~!cfV_o4Rfo+PI~C-L|+k0p5SUrr#s7>;~+%$eNkTLa^;fWs^bi@;$sJechCD_Nbh=vZmUc5i%MBq|Fq z&TXpk#WTZveya4WU#c2n&TE*VGJ)K4-H*ne;y26dU|sZ{TPY!=9Lktb*2gJ8U|gB% zg>s+7v82bKvExf4c9bvuDW8`E&pI8%z_O@jR_f|XvzK>WNgwSX+ zxz)AA+h>XZG~_ZqL=?du#GkU=Qrsl!IBw7D#QwZ$Zj4Ybx2bMS@4=drK|YNwqJ^8v zN6k}qE@mHpu_+&ay}STFM5@n*ekBB(R6hM$eF5%Dq2`74%M*-UWZ0~`UCNDQ;rl%t zQz7q-;3guJa}M;CAW=U2h#=y|dieCgjIDp!w7*M&x`=WJ$Ca&r{ItI-5p!;m8wO?+ zV_)k!RPzxsNE!o4Xshs+k{^%PZF~HldDNO+LxiPEC6(DUV=qu_W0Q%YObVc%3AbUX z@pKOFLzlsl3J~AVfl8r=C_x2?;C8};d^p@9;72`O8CfI^)_w>xLH-A}f}hH4%%h>| z3qbz+O)K+hUS6OPBlj0TgA+OE4e&w|K`4D!?3Q`}mzDk#98_gd&Dcv4?_6F)BJeq7 zam}eq(?Y?t5HV!S?%pUBeB2eq2!4D7Wkf>nE?-kZ6p2zqR68z_0k={S9XGdDc-B5K zwBw%MRRwOKR0%EW1pp3hDHo-FYnyBh%()aAm1qaH?D`VL7LY=w9NuzyiEKCqXxyWp_X<@;8%NYL%63Dd)x6q+M5uADx>Lix|+1%;x5 zTTl~dhCToigIE4En_2SQ%t>~{F5$~Uut)_5P#a|X1|PcB!yd4O9%#{s{O2@;*fFkL zN(IwG#jaFD`U=#$Gn>g!IHaJ_g!F~k&_ZeofiF$2^qxO)}e5A^3Fjso>2}V zVU9#&k#3NHoHv-C7VYC}5`p3@=lyeZA+`E6BU3T;jOE>Iz&3$Zv?=L^Z}dI7eK~)= z?F1l z7|6=FaKIy9zHeOx?@cI-TZ{#CW;$vsSxsaU$^mMCD@d3+bo*e|!hbEw9O=Io1=Hfs zqJ+*xE!n&_D3~xg0FR!U?X>sFC}{`=i}L@Knill@-)ZLs7d+ zS~MI(iK?^Bm(hr}VausBUH*iRapBL}DA%2aa*5pzi{qEYA&^eUpw-ipcYswuDVjsp z@nXGk<&14&nuvQc4@zyY8eLmVD?&fHde=bf`M(%$fn2c zGc$JGXFuo}^mWFtf5M}-TFBd@t+2Vbf9-3;m%YbE2GzCQJ!D5Uk`&d9i^H82RIlyF zEV>pMdC?<>E-TW=9tIgs^zN)J97acBcaLWIv_F=E(XJwOzb^k156>{z(O=nj^O zaRwra@viH;y_-{u2T9Y-0@WM_w4&aI2X4W#eAk-pCAILNuZA_$rFEk^@y^%w%H;ZX+Bs@9 z%YpmCp?lOg_q<4-ms59gxw{DcNXq&)?)+eukpZM+KLFo0f-EBg)sjQ=l%oyR_LYyxjLHwWh!&xg~Pp4V(QY@bzkf&Z9JWQE6Dfw^$2Q_S}m?v^OstRcV#P zz2jk*{CY7!On2^V-ZsOFBKo=XX16WjNSjKH2miouuF^hud}WAcVWQ>650A^TpfEqm z{l)a79DxAN2yEIJ0alygUc4uAI3g-FgYgNb#X+k+LBu^+B32DDZNDPtPy`W3pR&2= zw1ILB`rTFa0lL9xK~MSXkjRfAN+Ct_`fa{xFt}k7+A1T5fJ`tJ9!iroR08X!P#EDp zd0qR{9jIkUIMxcz@B|iun)oJXpmOXSQ5QQaSK9Nn_WNXxLEY5L#Wa6COjM61G~_2{bePj zRGOu~aU$ex_mkp~+~CIT1Y!M$nZo3F zC~5)sf+}x8`S`c;n1@`@Hwro0tPAsiCct2etR3dwvfH+Carmy8?UVl3B3IfPIh{7* zYoGEmBu$mEi{#T!5K28#xV;_D8CSR&b4K9MFnL zw}L}gBoV{OaV2~vxw{%fgY#!%q*$DW!SUZ(XjvGkb|dy219rR*CH1jmMg zPAyEh{xyWspX)FejSaPzWn5m<9fyZu{-7~SUZjvI&rJ}J+mbM}VIU%fw1SJ^8Eg-~X( z6auSJmXM8BXEz{SJCIx!J)>?eT{>Y0^D3VTjV=&u1P}gzJ6(^h%qS4kHuTUYAT1J< z_^FM7{6go9NJ2A$<45MQ-Pp}bS5hNs1qk!bif@IO+gA<_udp#SRp z`ADC)Sp-5Wg5n1wt(l?jEebsJXQXOFBDP06l%SzO`p@N0u^gw%foOSM;q$`b>wQ9! zfe?*dh$3;>*5*h-scFF7R&zCAaRh4LTp-`3gii?ctJ}~1tV?vd-tV)SfN5OU9=V?d z$RS)s;VQ4`WE^O$)OHjKwEc+|7rw?|dliKN4)V)^Bydn^jV$iBEVN8w?sPa+h9zzE zRFELcbdRsb7@$KQYlUToo36m)q9ZiPbn~X%9>%8h8-oQ^xQi%e#n+@Fnkg=P?-aNofvq*a8ejQL5Va3p-egS$P-_{4uhL3 z8>^tkQl!F;HUgEV0nN9}3|5pU8%wj_CeZ9fJe+On<2kSyVrh`*SN|Nh})<7P%tc zRslCO7Wsg77%5YglrjQ6w!GvKA)Ob?q<*{p`PCv-LWBj(2z155Ao5|VNv<$6o&Bdd zZ~1t?C*cgPV$U=nrhB-ECj=@c(MsFNcne}kvMSOX;flp#hLpWIwP2k)2&<@6Dp%RZ z{HD@%>Tw@07Ap5;N)c~!&4Pv`1VRMJ=(0blxqY$WFq*4l$5RR%t7^ssiGTDzq9q)qg z0SOXb0Uo{D924>v2uP7Ptmd1{y>FQ1kv<(=3)G_)NV3?f$|6d~-6Sd-R!Ro=an549 z+9<1BGp(;ozkhRz8qy6bHC`7Bnkf9GelGDjH_T=^q! zQ+500^CU@EIG|;HRu7_m;>{pq1k=PI_tu#{Y12ZReE)}zT-?-sT&RY$A!(BWRNYx{VEe&YD$TF0 z;u7F1>|=R|5^1HX9-4zCL-0g7!Kd>IKRgyt;?o`Z%kRr^I@&i{1kA}ag2z7MAE(esc9ENmSwue&VoJMh=|Y`X1ItK4o6&q(;t^yx)UUZ_zeCG`SZOj4wDhEqZSd z0B8XL5k$B}^}Ec}+|^HcSF}84lc*EP{RFmmJGpS3`i{nlR;OXkQglTM7)6l2++5b_ z7r(*MVJkfCD)6*ziZ@{x8A;SiFO59|Jt{shc zAEO~=s)p01sVRs*86FN1Tw2eACjjh*V{l}sX1nu8cZM2^lq|-DDJS2Kafzn)p9rOr zGn!LhPV9eOVNFwfXQRn!t53NOEm1dXG_0a!09?D=<9|tfT78-1dd%6>)xj8PHCha| zix{cb;&XW(KU89n=%i}Iwp`>;CUZ>|=x;J_F0xmF~0xtfEmS)|)WWFV&b zVftp+yU}dqcm*Xz(;>JBCN?eqIQ0V}EF~9_e0=j$65A-}