From 13c21dd708b2cfdb17ebf2d5addd0db9fd1f2061 Mon Sep 17 00:00:00 2001 From: zazabap Date: Wed, 1 Apr 2026 13:25:28 +0000 Subject: [PATCH] =?UTF-8?q?docs:=20/verify-reduction=20#970=20=E2=80=94=20?= =?UTF-8?q?CircuitSAT=20=E2=86=92=20Satisfiability=20VERIFIED?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Tseitin transformation: each gate (NOT/AND/OR/XOR) ā†’ definitional CNF clauses. Constructor: 14,454 checks, 0 failures (7 sections, random circuits + exhaustive nā‰¤5) Adversary: 15,276 checks, 0 failures (independent impl + hypothesis PBT) Both reproduce YES example (AND+OR circuit) and NO example (contradictory NOT). Co-Authored-By: Claude Opus 4.6 (1M context) --- .../adversary_circuitsat_satisfiability.py | 831 ++++++++++++++++ .../circuitsat_satisfiability.pdf | Bin 0 -> 113407 bytes .../circuitsat_satisfiability.typ | 165 ++++ ...est_vectors_circuitsat_satisfiability.json | 242 +++++ .../verify_circuitsat_satisfiability.py | 921 ++++++++++++++++++ 5 files changed, 2159 insertions(+) create mode 100644 docs/paper/verify-reductions/adversary_circuitsat_satisfiability.py create mode 100644 docs/paper/verify-reductions/circuitsat_satisfiability.pdf create mode 100644 docs/paper/verify-reductions/circuitsat_satisfiability.typ create mode 100644 docs/paper/verify-reductions/test_vectors_circuitsat_satisfiability.json create mode 100644 docs/paper/verify-reductions/verify_circuitsat_satisfiability.py diff --git a/docs/paper/verify-reductions/adversary_circuitsat_satisfiability.py b/docs/paper/verify-reductions/adversary_circuitsat_satisfiability.py new file mode 100644 index 00000000..6c3c1810 --- /dev/null +++ b/docs/paper/verify-reductions/adversary_circuitsat_satisfiability.py @@ -0,0 +1,831 @@ +#!/usr/bin/env python3 +""" +Adversary verifier for CircuitSAT -> Satisfiability (Tseitin transformation). + +Independent implementation based solely on the Typst proof at +docs/paper/verify-reductions/circuitsat_satisfiability.typ. +Does NOT import from verify_circuitsat_satisfiability.py. +""" + +import itertools +import random +import sys +from dataclasses import dataclass, field +from typing import Optional + +from hypothesis import given, settings, HealthCheck +from hypothesis import strategies as st + +# --------------------------------------------------------------------------- +# Circuit representation +# --------------------------------------------------------------------------- + +@dataclass +class Var: + """Leaf: a named variable.""" + name: str + +@dataclass +class Const: + """Leaf: a boolean constant.""" + value: bool + +@dataclass +class Gate: + """Internal node: NOT / AND / OR / XOR with children (expressions).""" + op: str # "NOT", "AND", "OR", "XOR" + children: list # list of Expr (Var | Const | Gate) + +Expr = Var | Const | Gate + +@dataclass +class Assignment: + """One circuit assignment: output_var = expression.""" + output: str # variable name + expr: Expr + +@dataclass +class Circuit: + """A circuit is a list of assignments over a variable set.""" + variables: list[str] + assignments: list[Assignment] + + +# --------------------------------------------------------------------------- +# Circuit evaluator +# --------------------------------------------------------------------------- + +def eval_expr(expr: Expr, env: dict[str, bool]) -> bool: + """Evaluate an expression tree under a variable assignment.""" + if isinstance(expr, Var): + return env[expr.name] + if isinstance(expr, Const): + return expr.value + if isinstance(expr, Gate): + vals = [eval_expr(c, env) for c in expr.children] + if expr.op == "NOT": + assert len(vals) == 1 + return not vals[0] + if expr.op == "AND": + return all(vals) + if expr.op == "OR": + return any(vals) + if expr.op == "XOR": + r = False + for v in vals: + r = r ^ v + return r + raise ValueError(f"Unknown gate op: {expr.op}") + raise TypeError(f"Unknown expr type: {type(expr)}") + + +def circuit_satisfied(circuit: Circuit, env: dict[str, bool]) -> bool: + """Check if every assignment in the circuit is satisfied.""" + for a in circuit.assignments: + lhs = env.get(a.output) + if lhs is None: + return False + rhs = eval_expr(a.expr, env) + if lhs != rhs: + return False + return True + + +def is_circuit_satisfiable(circuit: Circuit) -> tuple[bool, Optional[dict[str, bool]]]: + """Brute-force check if a circuit is satisfiable.""" + for bits in itertools.product([False, True], repeat=len(circuit.variables)): + env = dict(zip(circuit.variables, bits)) + if circuit_satisfied(circuit, env): + return True, env + return False, None + + +# --------------------------------------------------------------------------- +# CNF representation +# --------------------------------------------------------------------------- + +@dataclass +class CNF: + """A CNF formula: num_vars variables (1-indexed), list of clauses. + Each clause is a list of signed ints (positive = var, negative = negation).""" + num_vars: int + clauses: list[list[int]] + + +def cnf_satisfied(cnf: CNF, assignment: list[bool]) -> bool: + """Check if a CNF is satisfied. assignment is 1-indexed (index 0 unused).""" + for clause in cnf.clauses: + sat = False + for lit in clause: + v = abs(lit) + val = assignment[v] + if lit > 0 and val: + sat = True + break + if lit < 0 and not val: + sat = True + break + if not sat: + return False + return True + + +def solve_cnf_brute(cnf: CNF) -> tuple[bool, Optional[list[bool]]]: + """Brute-force SAT solver. Returns (sat, assignment) where assignment is 1-indexed.""" + for bits in itertools.product([False, True], repeat=cnf.num_vars): + assignment = [False] + list(bits) # 1-indexed + if cnf_satisfied(cnf, assignment): + return True, assignment + return False, None + + +# --------------------------------------------------------------------------- +# Tseitin transformation (my own implementation from the Typst proof) +# --------------------------------------------------------------------------- + +class TseitinBuilder: + """Builds CNF from a circuit using Tseitin transformation.""" + + def __init__(self, circuit: Circuit): + self.circuit = circuit + self.var_map: dict[str, int] = {} # circuit var name -> SAT var index + self.next_var = 1 + self.clauses: list[list[int]] = [] + # Map from id(expr) to SAT variable for gate outputs + self.gate_vars: dict[int, int] = {} + + def alloc_var(self) -> int: + v = self.next_var + self.next_var += 1 + return v + + def reduce(self) -> CNF: + # Step 1: map circuit variables + for name in self.circuit.variables: + self.var_map[name] = self.alloc_var() + + # Step 2 & 3: process each assignment + for assign in self.circuit.assignments: + root_var = self._process_expr(assign.expr) + out_var = self.var_map[assign.output] + # Step 3: output equivalence clauses + # (not out_var or root_var) and (out_var or not root_var) + self.clauses.append([-out_var, root_var]) + self.clauses.append([out_var, -root_var]) + + return CNF(num_vars=self.next_var - 1, clauses=self.clauses) + + def _process_expr(self, expr: Expr) -> int: + """Process an expression, returning the SAT variable representing its output.""" + if isinstance(expr, Var): + return self.var_map[expr.name] + + if isinstance(expr, Const): + # Step 4: constant handling + v = self.alloc_var() + if expr.value: + self.clauses.append([v]) # unit clause (v) + else: + self.clauses.append([-v]) # unit clause (not v) + return v + + if isinstance(expr, Gate): + # Check if we already processed this exact gate object + eid = id(expr) + if eid in self.gate_vars: + return self.gate_vars[eid] + + if expr.op == "NOT": + assert len(expr.children) == 1 + a = self._process_expr(expr.children[0]) + v = self.alloc_var() + # v = NOT a: (not v or not a) and (v or a) + self.clauses.append([-v, -a]) + self.clauses.append([v, a]) + self.gate_vars[eid] = v + return v + + # For n-ary AND/OR/XOR, flatten to balanced binary tree + children_vars = [self._process_expr(c) for c in expr.children] + + if len(children_vars) == 1: + # Degenerate: single child, just pass through + return children_vars[0] + + if len(children_vars) == 2: + return self._binary_gate(expr.op, children_vars[0], children_vars[1]) + + # N-ary (k > 2): balanced binary tree + return self._nary_balanced(expr.op, children_vars) + + raise TypeError(f"Unknown expr type: {type(expr)}") + + def _nary_balanced(self, op: str, vars_list: list[int]) -> int: + """Build a balanced binary tree of gates for n-ary operation.""" + while len(vars_list) > 2: + new_level = [] + i = 0 + while i < len(vars_list): + if i + 1 < len(vars_list): + combined = self._binary_gate(op, vars_list[i], vars_list[i + 1]) + new_level.append(combined) + i += 2 + else: + new_level.append(vars_list[i]) + i += 1 + vars_list = new_level + return self._binary_gate(op, vars_list[0], vars_list[1]) + + def _binary_gate(self, op: str, a: int, b: int) -> int: + """Add definitional clauses for a binary gate and return fresh variable.""" + v = self.alloc_var() + if op == "AND": + # v = a AND b: + # (not v or a) and (not v or b) and (v or not a or not b) + self.clauses.append([-v, a]) + self.clauses.append([-v, b]) + self.clauses.append([v, -a, -b]) + elif op == "OR": + # v = a OR b: + # (v or not a) and (v or not b) and (not v or a or b) + self.clauses.append([v, -a]) + self.clauses.append([v, -b]) + self.clauses.append([-v, a, b]) + elif op == "XOR": + # v = a XOR b: + # (not v or not a or not b) and (not v or a or b) and (v or not a or b) and (v or a or not b) + self.clauses.append([-v, -a, -b]) + self.clauses.append([-v, a, b]) + self.clauses.append([v, -a, b]) + self.clauses.append([v, a, -b]) + else: + raise ValueError(f"Unknown binary op: {op}") + return v + + def extract_solution(self, sat_assignment: list[bool]) -> dict[str, bool]: + """Extract circuit variable values from SAT assignment. + Per the proof: first |V| SAT variables correspond to circuit variables.""" + result = {} + for name, idx in self.var_map.items(): + result[name] = sat_assignment[idx] + return result + + +def reduce_circuit(circuit: Circuit) -> tuple[CNF, TseitinBuilder]: + """Reduce a CircuitSAT instance to CNF-SAT via Tseitin transformation.""" + builder = TseitinBuilder(circuit) + cnf = builder.reduce() + return cnf, builder + + +# --------------------------------------------------------------------------- +# Test infrastructure +# --------------------------------------------------------------------------- + +passed = 0 +failed = 0 +bugs = [] + + +def check(condition: bool, msg: str): + global passed, failed + if condition: + passed += 1 + else: + failed += 1 + if msg not in bugs: + bugs.append(msg) + + +# --------------------------------------------------------------------------- +# Section 1: Gate clause correctness (truth table verification) +# --------------------------------------------------------------------------- + +def test_gate_clauses(): + """Verify that each gate type's clauses exactly encode the gate function.""" + # For each gate, build a tiny circuit and verify all truth table entries. + + # NOT gate + c = Circuit(variables=["a", "out"], assignments=[ + Assignment("out", Gate("NOT", [Var("a")])) + ]) + cnf, builder = reduce_circuit(c) + count = 0 + for bits in itertools.product([False, True], repeat=cnf.num_vars): + assgn = [False] + list(bits) + if cnf_satisfied(cnf, assgn): + extracted = builder.extract_solution(assgn) + check(extracted["out"] == (not extracted["a"]), + f"NOT gate clause incorrect for a={extracted['a']}") + count += 1 + # 2 valid assignments: (a=F,out=T) and (a=T,out=F) + check(count == 2, f"NOT gate should have 2 solutions, got {count}") + + # AND gate + c = Circuit(variables=["a", "b", "out"], assignments=[ + Assignment("out", Gate("AND", [Var("a"), Var("b")])) + ]) + cnf, builder = reduce_circuit(c) + for bits in itertools.product([False, True], repeat=cnf.num_vars): + assgn = [False] + list(bits) + if cnf_satisfied(cnf, assgn): + ext = builder.extract_solution(assgn) + check(ext["out"] == (ext["a"] and ext["b"]), + f"AND gate clause incorrect") + + # OR gate + c = Circuit(variables=["a", "b", "out"], assignments=[ + Assignment("out", Gate("OR", [Var("a"), Var("b")])) + ]) + cnf, builder = reduce_circuit(c) + for bits in itertools.product([False, True], repeat=cnf.num_vars): + assgn = [False] + list(bits) + if cnf_satisfied(cnf, assgn): + ext = builder.extract_solution(assgn) + check(ext["out"] == (ext["a"] or ext["b"]), + f"OR gate clause incorrect") + + # XOR gate + c = Circuit(variables=["a", "b", "out"], assignments=[ + Assignment("out", Gate("XOR", [Var("a"), Var("b")])) + ]) + cnf, builder = reduce_circuit(c) + for bits in itertools.product([False, True], repeat=cnf.num_vars): + assgn = [False] + list(bits) + if cnf_satisfied(cnf, assgn): + ext = builder.extract_solution(assgn) + check(ext["out"] == (ext["a"] ^ ext["b"]), + f"XOR gate clause incorrect") + + +# --------------------------------------------------------------------------- +# Section 2: Typst YES example +# --------------------------------------------------------------------------- + +def test_yes_example(): + """Circuit: c = x AND y, d = c OR z. Should be satisfiable.""" + c = Circuit( + variables=["x", "y", "z", "c", "d"], + assignments=[ + Assignment("c", Gate("AND", [Var("x"), Var("y")])), + Assignment("d", Gate("OR", [Var("c"), Var("z")])), + ] + ) + + # Check the specific satisfying assignment from the proof + env = {"x": True, "y": True, "z": False, "c": True, "d": True} + check(circuit_satisfied(c, env), "YES example: specific assignment should satisfy circuit") + + # Reduce and check + cnf, builder = reduce_circuit(c) + sat, sol = solve_cnf_brute(cnf) + check(sat, "YES example: CNF should be satisfiable") + + # Verify variable count from proof: 5 circuit + 2 gate auxiliary = 7 + check(cnf.num_vars == 7, f"YES example: expected 7 SAT vars, got {cnf.num_vars}") + + if sat and sol: + ext = builder.extract_solution(sol) + check(circuit_satisfied(c, ext), "YES example: extracted solution should satisfy circuit") + + # Check circuit is actually satisfiable by brute force + circ_sat, circ_env = is_circuit_satisfiable(c) + check(circ_sat, "YES example: circuit should be satisfiable") + + +# --------------------------------------------------------------------------- +# Section 3: Typst NO example +# --------------------------------------------------------------------------- + +def test_no_example(): + """Circuit: c = x AND y, d = NOT(c), c = d. Should be unsatisfiable.""" + c = Circuit( + variables=["x", "y", "c", "d"], + assignments=[ + Assignment("c", Gate("AND", [Var("x"), Var("y")])), + Assignment("d", Gate("NOT", [Var("c")])), + Assignment("c", Var("d")), # c = d (equivalence) + ] + ) + + # Check unsatisfiable by brute force + circ_sat, _ = is_circuit_satisfiable(c) + check(not circ_sat, "NO example: circuit should be unsatisfiable") + + # Reduce and check + cnf, builder = reduce_circuit(c) + sat, _ = solve_cnf_brute(cnf) + check(not sat, "NO example: CNF should be unsatisfiable") + + +# --------------------------------------------------------------------------- +# Section 4: Forward direction (satisfiable circuit -> satisfiable CNF) +# --------------------------------------------------------------------------- + +def test_forward_random(num_trials=800): + """Random circuits: equisatisfiability and extraction correctness.""" + rng = random.Random(42) + for _ in range(num_trials): + c = random_circuit(rng, num_vars=rng.randint(2, 4), num_assigns=rng.randint(1, 2)) + cnf, builder = reduce_circuit(c) + + # Skip overly large instances + if cnf.num_vars > 18: + continue + + circ_sat, env = is_circuit_satisfiable(c) + sat, sol = solve_cnf_brute(cnf) + + # Both directions: equisatisfiability + check(circ_sat == sat, "Forward: equisatisfiability violated") + + if sat and sol: + ext = builder.extract_solution(sol) + check(circuit_satisfied(c, ext), "Forward: extracted solution should satisfy circuit") + + +# --------------------------------------------------------------------------- +# Section 5: Backward direction (satisfiable CNF -> satisfiable circuit) +# --------------------------------------------------------------------------- + +def test_backward_random(num_trials=800): + """For every SAT solution, extracted circuit assignment must satisfy the circuit.""" + rng = random.Random(123) + for _ in range(num_trials): + c = random_circuit(rng, num_vars=rng.randint(2, 4), num_assigns=rng.randint(1, 2)) + cnf, builder = reduce_circuit(c) + + # Skip if too many SAT variables for exhaustive enumeration + if cnf.num_vars > 16: + continue + + # Enumerate all SAT solutions (for small instances) + for bits in itertools.product([False, True], repeat=cnf.num_vars): + assgn = [False] + list(bits) + if cnf_satisfied(cnf, assgn): + ext = builder.extract_solution(assgn) + check(circuit_satisfied(c, ext), + "Backward: every SAT solution must extract to valid circuit assignment") + + +# --------------------------------------------------------------------------- +# Section 6: Overhead verification +# --------------------------------------------------------------------------- + +def count_gates(expr: Expr) -> tuple[int, int]: + """Count (all_gates, constants) in an expression tree. + Each gate (NOT, binary AND/OR/XOR) introduces one fresh SAT variable. + N-ary gates with k children produce k-1 binary gates. + Note: the Typst proof says 'G = number of binary gates' but NOT gates + also get fresh variables, so G should really be 'all gates'.""" + if isinstance(expr, Var): + return 0, 0 + if isinstance(expr, Const): + return 0, 1 + if isinstance(expr, Gate): + total_gates = 0 + total_consts = 0 + for child in expr.children: + g, c = count_gates(child) + total_gates += g + total_consts += c + if expr.op == "NOT": + total_gates += 1 # 1 gate for NOT + else: + k = len(expr.children) + if k >= 2: + # balanced binary tree: k-1 binary gates + total_gates += k - 1 + # k == 1: pass-through, no gate + return total_gates, total_consts + return 0, 0 + + +def test_overhead(num_trials=500): + """Verify variable and clause count overhead matches the Typst proof.""" + rng = random.Random(999) + for _ in range(num_trials): + c = random_circuit(rng, num_vars=rng.randint(2, 4), num_assigns=rng.randint(1, 2)) + cnf, builder = reduce_circuit(c) + + # Count expected gates and constants + total_binary_gates = 0 + total_constants = 0 + for a in c.assignments: + g, k = count_gates(a.expr) + total_binary_gates += g + total_constants += k + + n_vars = len(c.variables) + # SAT variables = |V| + G + K + expected_vars = n_vars + total_binary_gates + total_constants + check(cnf.num_vars == expected_vars, + f"Overhead: expected {expected_vars} vars, got {cnf.num_vars}") + + # Clause count upper bound: <= 4G + 2K + 2|A| + # (NOT=2, AND/OR=3, XOR=4 per binary gate, plus 2 per output equiv, plus 1 per constant) + max_clauses = 4 * total_binary_gates + 2 * total_constants + 2 * len(c.assignments) + check(len(cnf.clauses) <= max_clauses, + f"Overhead: {len(cnf.clauses)} clauses exceeds bound {max_clauses}") + + +# --------------------------------------------------------------------------- +# Section 7: Exhaustive testing for n <= 5 +# --------------------------------------------------------------------------- + +def test_exhaustive_small(): + """Exhaustive testing: all circuits with <= 5 variables.""" + rng = random.Random(7777) + checks_done = 0 + for n in range(2, 6): + trials = 150 if n <= 3 else 80 + for _ in range(trials): + c = random_circuit(rng, num_vars=n, num_assigns=rng.randint(1, min(2, n))) + cnf, builder = reduce_circuit(c) + + # Skip if CNF is too large for brute force + if cnf.num_vars > 18: + continue + + circ_sat, circ_env = is_circuit_satisfiable(c) + cnf_sat, cnf_sol = solve_cnf_brute(cnf) + + # Equisatisfiability + check(circ_sat == cnf_sat, + f"Exhaustive n={n}: equisatisfiability violated") + + if circ_sat and cnf_sat and cnf_sol: + ext = builder.extract_solution(cnf_sol) + check(circuit_satisfied(c, ext), + f"Exhaustive n={n}: extraction failed") + checks_done += 1 + + # Ensure we did enough + check(checks_done >= 400, f"Exhaustive: only {checks_done} checks") + + +# --------------------------------------------------------------------------- +# Random circuit generation +# --------------------------------------------------------------------------- + +def random_expr(rng: random.Random, var_names: list[str], depth: int = 0, max_depth: int = 2) -> Expr: + """Generate a random expression tree. Depth limited to keep SAT vars manageable.""" + if depth >= max_depth or rng.random() < 0.5: + # Leaf + if rng.random() < 0.08: + return Const(rng.choice([True, False])) + return Var(rng.choice(var_names)) + + op = rng.choice(["NOT", "AND", "OR", "XOR"]) + if op == "NOT": + child = random_expr(rng, var_names, depth + 1, max_depth) + return Gate("NOT", [child]) + else: + n_children = rng.choice([2, 2, 2, 3]) # mostly binary, sometimes ternary + children = [random_expr(rng, var_names, depth + 1, max_depth) for _ in range(n_children)] + return Gate(op, children) + + +def random_circuit(rng: random.Random, num_vars: int = 3, num_assigns: int = 2) -> Circuit: + """Generate a random circuit with bounded complexity for tractable brute-force.""" + var_names = [f"v{i}" for i in range(num_vars)] + assignments = [] + for i in range(num_assigns): + out = rng.choice(var_names) + expr = random_expr(rng, var_names, depth=0, max_depth=2) + assignments.append(Assignment(out, expr)) + return Circuit(variables=var_names, assignments=assignments) + + +# --------------------------------------------------------------------------- +# Hypothesis PBT strategies +# --------------------------------------------------------------------------- + +@st.composite +def st_expr(draw, var_names, max_depth=2): + """Strategy to generate random expressions.""" + if max_depth <= 0 or draw(st.booleans()): + # Leaf + if draw(st.integers(min_value=0, max_value=9)) == 0: + return Const(draw(st.booleans())) + return Var(draw(st.sampled_from(var_names))) + op = draw(st.sampled_from(["NOT", "AND", "OR", "XOR"])) + if op == "NOT": + child = draw(st_expr(var_names, max_depth=max_depth - 1)) + return Gate("NOT", [child]) + n = draw(st.integers(min_value=2, max_value=3)) + children = [draw(st_expr(var_names, max_depth=max_depth - 1)) for _ in range(n)] + return Gate(op, children) + + +@st.composite +def st_circuit(draw, max_vars=4): + """Strategy to generate random circuits.""" + n = draw(st.integers(min_value=2, max_value=max_vars)) + var_names = [f"v{i}" for i in range(n)] + n_assigns = draw(st.integers(min_value=1, max_value=min(2, n))) + assignments = [] + for _ in range(n_assigns): + out = draw(st.sampled_from(var_names)) + expr = draw(st_expr(var_names, max_depth=2)) + assignments.append(Assignment(out, expr)) + return Circuit(variables=var_names, assignments=assignments) + + +# Strategy 1: Equisatisfiability +@given(circuit=st_circuit(max_vars=4)) +@settings(max_examples=1500, suppress_health_check=[HealthCheck.too_slow], + deadline=None) +def test_hypothesis_equisat(circuit): + global passed, failed + cnf, builder = reduce_circuit(circuit) + if cnf.num_vars > 18: + passed += 1 # skip but count + return + circ_sat, _ = is_circuit_satisfiable(circuit) + cnf_sat, cnf_sol = solve_cnf_brute(cnf) + check(circ_sat == cnf_sat, "Hypothesis equisat: mismatch") + if cnf_sat and cnf_sol: + ext = builder.extract_solution(cnf_sol) + check(circuit_satisfied(circuit, ext), "Hypothesis equisat: extraction failed") + + +# Strategy 2: Solution extraction round-trip +@given(circuit=st_circuit(max_vars=3)) +@settings(max_examples=1500, suppress_health_check=[HealthCheck.too_slow], + deadline=None) +def test_hypothesis_extraction(circuit): + global passed, failed + cnf, builder = reduce_circuit(circuit) + if cnf.num_vars > 16: + passed += 1 # skip but count + return + # Check all SAT solutions extract correctly + found_any = False + for bits in itertools.product([False, True], repeat=cnf.num_vars): + assgn = [False] + list(bits) + if cnf_satisfied(cnf, assgn): + ext = builder.extract_solution(assgn) + check(circuit_satisfied(circuit, ext), + "Hypothesis extraction: SAT solution doesn't map to valid circuit assignment") + found_any = True + # If circuit is satisfiable, we should find at least one SAT solution + circ_sat, _ = is_circuit_satisfiable(circuit) + if circ_sat: + check(found_any, "Hypothesis extraction: satisfiable circuit but no SAT solution found") + + +# --------------------------------------------------------------------------- +# Section 8: Constant handling +# --------------------------------------------------------------------------- + +def test_constants(): + """Test circuits with constant nodes.""" + # c = TRUE, out = c AND x -> satisfiable when x=true, out=true, c=true + c = Circuit( + variables=["x", "c", "out"], + assignments=[ + Assignment("c", Const(True)), + Assignment("out", Gate("AND", [Var("c"), Var("x")])), + ] + ) + cnf, builder = reduce_circuit(c) + sat, sol = solve_cnf_brute(cnf) + check(sat, "Const TRUE: should be satisfiable") + if sat and sol: + ext = builder.extract_solution(sol) + check(circuit_satisfied(c, ext), "Const TRUE: extraction should work") + check(ext["c"] == True, "Const TRUE: c should be True") + + # c = FALSE, out = c AND x -> forces out=false + c2 = Circuit( + variables=["x", "c", "out"], + assignments=[ + Assignment("c", Const(False)), + Assignment("out", Gate("AND", [Var("c"), Var("x")])), + ] + ) + cnf2, builder2 = reduce_circuit(c2) + sat2, sol2 = solve_cnf_brute(cnf2) + check(sat2, "Const FALSE: should be satisfiable (out=false works)") + if sat2 and sol2: + ext2 = builder2.extract_solution(sol2) + check(circuit_satisfied(c2, ext2), "Const FALSE: extraction should work") + check(ext2["c"] == False, "Const FALSE: c should be False") + check(ext2["out"] == False, "Const FALSE: out should be False") + + # Contradiction: c = TRUE, c = FALSE + c3 = Circuit( + variables=["c"], + assignments=[ + Assignment("c", Const(True)), + Assignment("c", Const(False)), + ] + ) + cnf3, _ = reduce_circuit(c3) + sat3, _ = solve_cnf_brute(cnf3) + check(not sat3, "Const contradiction: should be unsatisfiable") + + circ_sat3, _ = is_circuit_satisfiable(c3) + check(not circ_sat3, "Const contradiction: circuit should be unsat") + + +# --------------------------------------------------------------------------- +# Section 9: N-ary gate flattening +# --------------------------------------------------------------------------- + +def test_nary_gates(): + """Test n-ary AND/OR/XOR flattening to balanced binary trees.""" + for n_children in [3, 4, 5]: + var_names = [f"a{i}" for i in range(n_children)] + ["out"] + children = [Var(f"a{i}") for i in range(n_children)] + + for op in ["AND", "OR", "XOR"]: + c = Circuit( + variables=var_names, + assignments=[Assignment("out", Gate(op, children))] + ) + cnf, builder = reduce_circuit(c) + + # Exhaustively check all assignments + for bits in itertools.product([False, True], repeat=cnf.num_vars): + assgn = [False] + list(bits) + if cnf_satisfied(cnf, assgn): + ext = builder.extract_solution(assgn) + child_vals = [ext[f"a{i}"] for i in range(n_children)] + if op == "AND": + expected = all(child_vals) + elif op == "OR": + expected = any(child_vals) + else: # XOR + expected = False + for v in child_vals: + expected ^= v + check(ext["out"] == expected, + f"N-ary {op} with {n_children} children: incorrect") + + +# --------------------------------------------------------------------------- +# Main +# --------------------------------------------------------------------------- + +def main(): + global passed, failed, bugs + + print("=== Adversary: CircuitSAT -> Satisfiability ===") + print() + + print("Section 1: Gate clause truth tables...") + test_gate_clauses() + print(f" Running total: {passed} passed, {failed} failed") + + print("Section 2: YES example...") + test_yes_example() + print(f" Running total: {passed} passed, {failed} failed") + + print("Section 3: NO example...") + test_no_example() + print(f" Running total: {passed} passed, {failed} failed") + + print("Section 4: Forward direction (random)...") + test_forward_random(num_trials=800) + print(f" Running total: {passed} passed, {failed} failed") + + print("Section 5: Backward direction (random)...") + test_backward_random(num_trials=800) + print(f" Running total: {passed} passed, {failed} failed") + + print("Section 6: Overhead verification...") + test_overhead(num_trials=500) + print(f" Running total: {passed} passed, {failed} failed") + + print("Section 7: Exhaustive n<=5...") + test_exhaustive_small() + print(f" Running total: {passed} passed, {failed} failed") + + print("Section 8: Constant handling...") + test_constants() + print(f" Running total: {passed} passed, {failed} failed") + + print("Section 9: N-ary gate flattening...") + test_nary_gates() + print(f" Running total: {passed} passed, {failed} failed") + + print("Section 10: Hypothesis PBT - equisatisfiability...") + test_hypothesis_equisat() + print(f" Running total: {passed} passed, {failed} failed") + + print("Section 11: Hypothesis PBT - extraction round-trip...") + test_hypothesis_extraction() + print(f" Running total: {passed} passed, {failed} failed") + + print() + bug_str = "; ".join(bugs) if bugs else "none" + print(f"ADVERSARY: CircuitSAT -> Satisfiability: {passed} passed, {failed} failed") + print(f"BUGS FOUND: {bug_str}") + + sys.exit(0 if failed == 0 else 1) + + +if __name__ == "__main__": + main() diff --git a/docs/paper/verify-reductions/circuitsat_satisfiability.pdf b/docs/paper/verify-reductions/circuitsat_satisfiability.pdf new file mode 100644 index 0000000000000000000000000000000000000000..623be1496a3d7587d17c832a7f80469c032125f3 GIT binary patch literal 113407 zcmeFa30#a{^gnJZL}iJ{(jX))vrlQ$N)%C2B3dRz`>HIV6v-|`iy~VpQV|tpjTEwE zmn|tmq>}v4eU>qk`OJjR_w)PyfB!$z>(28$_qq3;bI(2ZoO9pz&S*7k`R9gUW#XGbs!z z3#Id<^z@{-UM{ErDY}r7rUwRixO?G+nY#P=2T-v0QGw=;{8xBQH2(5X&Yvx_boAq* zwxDX!>v(BQ@)9eJ#w#2zPE8Z#v~~~h;8Juh-)U5%7SYqPPocKDw43qScs-m`cUD#Md{7 zPrvYz$E|7HB>@zyLx1v1nWj!tr&#)VJ9%(DDaKq^cQ5wZ2%I`*WdYFN(FFqnE#{x1XmYx<8J;9XKU? z^rA|{v_ngv9X#rBx#ExyF}cztuL!Zi1_ZCc4AfvhKdy5C2)Y1!a8mi2g^K;9Sv-bd z-N36$sMs<HbiAjOv_K7@FpA%R2{6FWXJ zZBopUh(md3co@S==shO1<+tDG6J5F%E)aY?Lk#(6o?$}7>n+hdLv196856!^bfBSV z2=x9f-~NPde!l$)-v#)F3oswwkbM8bH^CuKqmqJ+v5_Z;Jke&VQ>?r_0yk-0qqQb;c$EzQ&kVh=9LXJ9R+Vo%R0~x^h z!e1XM>!0hxE8r2xt3XqoV#D=wcXfBhbS1?q(9_e=FXSg_3@Y9#{;CA$2;35|!ql*} zAD27R+dBYh{+Zq$Tnk4Z3T7{$8OJez8{qBm>@EiK!|`F)87@#>5n^|E-j) z2V)47OQz&~GQ~Im&;K?h%Og{q#dM~)l*~`?k4f^0;4kxkDkbY7Q=*@kznc>8Gl>4= zr35_;qCXkrHPH{eYl82L-%ZK#2>vquG$qR+`hnLj@;B_nhPhk&^d$ zDZwXtM^mC+I>9$O(Jnf{FWxnIpWp+XOv(EMef0l2CF>{oNbrS5(ErCNK_8*Y=)a^y zy|{Nnq5o?s*?uu8mFTzsbt%C&+!dwJ|1l-_N4T!^|1~MWcYM}|_6xtJY2p0;|6Hnx zk1HDP5>RNoYrH>cT4GXOetf)w3y-WTN{3V4`?!9jX|+pv&+&evX^Bb6{JfOtS4~`x z(KKzi>!82tMUhL#6~jIpR_xKbvefN$+2#yz&Ts@vaGek=Ja3FKmJi zHbFP3~C1l=sMeu7>$k@D`7?H7~s@)Put*DQjsyle6~(GC`QP4p8>TuSCA z+y8H;Wcef?$dtTKrUX9-zk~Mwx|E=Uu)}GDpCmpd=;pmg$PeL9(f%8mZL?cte zAEb#($^3*LL?iqz8tg5UK2Eh*NndA#*6ECPjMb@nto zc15Al2-WqUrNq#{gPc%5(G~yWDWU4gXdEvk?-Qax``?<9?Ic8$aItCsn3DMkQKX4W z$^3*Ull?;_Oc!2C^cUf3)2QS%(XYH~LWL17FYP}|3I0%te*7gRpOY!U7kojILc^oZ z6fK-=Eu1qvq#N|R_V zo)C@=nczheUdf-{+eORT7b@Fxg&g76~#4<~p(5S|7bm)74%aN5b& zi7ULT*d0%VmV)z>O(b}Sv+;y*Ut)19!q+a-8? zgq7VcA)ev%5r$<)65<7%gT%rCnGny21ZN~+bBavx7YOT;OmNl_CMIDyGH^zcSGX)O za3La$Ju+sFD>5=7j#EpH{v`g^DlKHfFyu4$p~G{3%T(^R5(pEUML3V z4UG(mkRb;`_-Lf-{fkRLyhnu0f7(lU`)I$+heUoNbW0=V6HS~vLVF78OCst)Y9(SU z;x7n}H^Pr1+>&;Jfp;m{PE1+^Ku=iTiR~-2@Tp-*!OcRllQdcQ;^smUO(n2Ci6l#G zx#sQ5HK5p&3$xP!V&(2nEWn~~uw?24i^6E-)yUn?*@Fu&>*--_0GS~~fk8+JJ_N`m z7VM?~-E?$IeEZCZ24drcB%FU>2o{REM|`1%-Yy|{xmYVOAOVtkkOOjjX);Cd7Rw~I z8dE?T1$sCV6=8xy5&&{X*QCQALsTt@OtH0?J9!8rg`*{^WTcA3mn@X`{3=S2_h^WT zFO-k>m_j63!qF7fU{tI4vU#i!ESV#!VbfU!fuIg5ux^QvzO>r(!s;b1HnQ&q(IDnsy)16WVyJ1g&YpT zGo&*`if4y(iJ*95Z6?JNgq035PG^b~$qr5MB5DB@MhD$UXNahmVTYvyMT~uFUV^4g^LOG6^a1>C|z<5Ch{jSN4YXFkt zzm8SR?H1cgL5^e1;&B`}3_c$nLKt*dW}?$Y&5>BVNo;LDxh-JT(?yL>ED$EPWTCS! zMC^&c8J#Z5F2XX2twNAhm@Xq(1pya?)T6`F3LX4mk_W_)SQ6@9>mrv)ShVv z7)MqN4aNmc6d$oDquA<%@)061bec#~IyAb4l}&@tIT4Gc!4d#Xivxdf3)f6^SmU5m zfuU4U;}Od&mNJ3v!=t%G_t9Vp0s-#mup$BbSKtpMA67E}L@2`2#ajJ0wZcLKf{7t0 z8G@l92pfX8(X>R?+95R|jMF@%4~Ig6do)FjXe`rj(#NkqXy7u?AO=X|0FAI@K;r<7 z5F4ZcM2ZHB4Jd9%1K1S}RxxN0uA@Q3h6ceD8U#~l07s)ioDsp+0MaI^7dm7k;F}Ck zcUw~MARyWGY>|a`$TavDtvVufibqZbrU&en*xn#x8+g2vpb_|vW_jp__Hzz)OMIa} zXL-C~WVu)vOrVw6%8=Ls1x6y?EM9k@y&KT~Fr;ZPz-S_UCyX$$wejX0fyUF=qVyTo z58_KEW_UqvV>2-Y#{mj5=XYZUxHOR5#>SRlfgREXg52hxcWGdT(7;Tf!Q@SYX_m$k z<$hyfe(^jZEm(oZ(?q&!81_D%u`gQ=bdE)7kjOM|U}h^9AYkTa9l+q~J?QsL8-?0y&KXqy@$w zc1wJr#;71m3f?O8U62nXtKh+8*y70bgRN|cdObbf{x-CF^9#4E0zzOXy9R8@ba%nB zW1WT?jE!*$K;=YrV~3QHz<|IxfCxZB2tF7B$I&1-iokdXXh&m+vL`S;{_o=!jUmc2 zz$8k1qlL*0u>$}H@(apMhin#WQf_!5jsI!6!Ph_#q>#X~&=?{$L5Hj(K@sBV0wh9! zJw$j#8eP=1gTZyg_JD|5z%N74H?*vbAb2$J%V@AvNQ1R_8Z7=HastYspVNjwmj~UM_ik7G-2%b+YMFI*EZy7e05FK=+iM2${RXA$- zH!JxEDdM-4Ej=8axd<5tzJ!Oj^J3`2pWXwwwBUP!ZwL+=_)K8-gOLtqE?CfDt%B_b z#v7PIV1j6g7Jf8aify~FZa{G{0^bb|Gt#`MM>wKP5j>OF+S+vo&xnNX;E3*s4rw$| z#fx%yOU`C0Y)jTi!j>}H-}*TiAL;ZK&}t5fdLj` z$h`p&(x(yde+Zw_zyd+t$rd?=u}oqaBFOKb=hh(FMR{F#bN;G$8U-S95Rij-oXBt- z&V;|I3gS@^j)G_u1fxX8qHxy#O;zBwg4YU8E3DiCummkhQxRwa016OOLeL5p1!6rA z>VZfP1bQIO17RLm*c2IN!lmP{+C`%6_W}yHw0TpMVkUfFAW%1)-vDG{QMDriOZi&{D^};$13zRGi*0op= zfoH)Kz=FjD7EGxuSQ%i!e9D3-JPVeZSTNDEV5VomRL_FBo&}RV3ub$kCf`sK(#8&1 zSAtTAbC_%+Qe{Y&!2&Z2<^~q5!LmS^viMP1Lh9{MY>v0C(Y`EIZKhpk4{qyU8A?^7C;|brw%i{yo57QD0 z<|P(POe_YUvmvCuj_E3LQHIbkyt??pBEOc6X(h3|{RdIOF|(j-g=n1L#t{<=l594n z#Ig3moD5SLfmmkoPn<%?=@3RiP*m{N^Xdgr0NuxeG0p=0#R9Fz0?o<-watP~WP!-C zK!jN^OyFc#_~Q#l2x$+xC6>J++XMB34ax$Olm%u1i^gXN3aRfmwF*8d@n{!KONX?I zFpGc*kqUBCKMU{|u!ex?7#6s;EEJT2v4Cu77C-((2yq?KKJAz(pno9v#e(1$3tTW3 zcw{W9$Z?0Y@^?E=us)GfPsgy%BI)7tScUMbLwaK}19iV8-x8iRd35ssMQ5ghxyXcY z2os_dC{;nj-c zbSC&U2r!P;uyGTdiLE2!!;OipXX8T+j_rj!n6QEi1P%}a^56hraE8z`j3e+J-N(Tt zO#T3g5QhDM?!|~EtxTq-$l-{!=r=p0UHKpY5d2|6^oI%IA11_qm=FMB@jkTo305l;tX3vitxT|5nP9at!D?lK)yf2`l?hfWlYbAGkal!P|B7q})DM;^ z6a0K8Sn*7-u9^JUC?R$Jfyx!69psV;rWF%RD<+s$OhD{1A(+C1FaQ(03MN?3Ot7Ar z{Gk9L?f3%|uw6T#Zp`V2x{=$D{C=kB0r>}Jo?x9YtubK|VS=J(qTmBR=0XUK9a7h# z`WI{xIL;gXfY)FzF&QFFKj@V|R5%O}R)i};b2bAh3mm2l-@#2J@a7CySOCBbmWK&* zJ`*iMfe@f~nEWW?Um1br`ptok5yMj?U{^4~u3*A^&xHA&3G+P@=6fbA9KsR*@CWSy z1Ct410wx$&OfasPU|caFY{CR%lL;OX%zf|&`M?Ndf)U6BBajJ3Ad}7)Mic#DfS@-6R=pW8GcsUiWWbEYfEkMcGZq78EQaVA z3+wg2YX{T|3Yh^4nE?u!!M{OT2;G0600ns~TET)k>HuH=&6p4>t4L5sVRPC)>jjIUunXiDjdpR&7^4Um)>Uq3jsqUR3#Dc`?93V1R|d z01JV^5$QBwoc}9&VAf}dp7k;55nIR4*i<|D5IO5$A}_vd0(Fa!t3SIMq0KR|#^K$9 zVvXGsU+_q+s2Ig$Z$CIhr7 z1Ljl)P|N^^GC&9!FgO?>zznuX#~f?5Sjt7VLF9acab0ZrKgFRPU-=fsgz&FJMvpMB zhk;h-2-rIVEIYLQ00{>JtUI(F0sk&i_h7li64s7!{4O4YDN^@fE&99iMe3f8VdF)$ zAFYs~B{H-|29_!Vt&)MI$^hq=0k$lIAA$U9=YhuWz=SC(!0>;^57|I)fdQr=1LA{d z;|nHvqT`fUuHTdljN80f58{vv@cS8H^TSUB!JkMK0rPQ3dW!yQC`h^eFCAgTg1(}Q z7R?UnMPcI_Z4JUWh>&VHNE?pJLF<{sm9_A zfj5cmjNow}oCF3q2@G%&82q~qh1As{YfEs9wyO)64NeLJoD>F4w7%((G8I`D&_fd` zNmwt4mE50aKM*HJk+U5?LvBkGzK9XF- z8bPFBhp|m`aJcE<%+bM_qk}U?2WO5B&K&xkHaa+S=*P9_;LOp%nWF>Hj1EpY9UM&b zyF=&)fza>9!4Le2ayGGz24cw)K9KQ&Nr!2QJmQ{?A_vfDG+^n_+vJh;bf|_d+WYI+ z)&fEPVvQ#U?Joy736Z}JX)RH8fMSAEsYEjL50sA}9WW8lVFICpQm2E2(nUL1AQ~M| z{Q_d&t~$~BphG%Gn0&yw5ZGQ=Ocs#Q1_FzHN7gq8F#a8sJqR@R9o!P~Cl~18FbSMd z^J`yr49(xJFZqo-I@qyrt_%DDkHN;K^FzFZ)YqZ-y~z4t@Pa!jaJY()dj257gzc~3 zjRWvFh~rft1^U3_po7N&hrEcATda4)DgsgTLCEzV4_gsJ=O2XK1?gmp)YlzD)sq{y z1Qy8tSzG_{9yfHV04C%FoDgk_$F4z3qZI9%hg8tz#qNpi5^JpEVSx{$n3MvvA097Q zNbISDFnR*$O| zmE=0!4or{)mBPO+`oxb|wQDSrn&0C(I{N~MC+u-_G6y>I^&iftz|;v6<8x^cb^;i+0m0c28_$1$coAIIkN-Inl@) z>cB`68vP-#|7iala-@*zN1Mygt}oAKV(AnVVyy8z^8to|h+`vQ zuL8&;w3#@}0%Q{85r9?zOcyCEe_%|uYZs_Akzs$Fdw)l}Xc{_XM+(XiHZ77eBofw* zyyriaA!1ViigM#9e%MM4U-5+^v;`b()JCp3CQTyI-gvIxxf!1G;;6nn3XJcPsB>*i1;3#H+jo?Bm?ob3yu>Y{el4Ae>PT*aFa|ymBxR$WG z!xm|4U~T-(9u=rik% zqbS6TYdtW9(UJ?gi2~O!Pl9)Zt`P7CBGce6VIm-MC}EkzHmzMxW15r@V$dxJTm+a2 zgl!hdW7N98sS1VVA=(bS0M(Bcx&hAs5Dmb`h^+PxbP>K;hM*8z9S~Uq>W{x63_>|z zDMOe5+u9Cc0Eoo^-UWh-5Tq4ZbB8pQh~5*mDhNNA&=I->2L-=qhzuKdY$JeBC2Q&D z4Tn>DQjEE-?p~l^LFbYx6~?(JeqnnS#P-x=8tQpV)B`Yp(D$Fa<^Wy6)}m55uqeWY z?;I9!4X}RLGD?LV2vpepOod21EOVn2zt4vI9Jr6Yi^@RYI4B3*XQQ&vcOyJS`8aTm z-UYk?Rvrhv!&euU--IY1FDWCt5s*&c~W-?LEuO9p2-jWpqp=`0acwV|$+b(rP0!V|4HL8jo5GFIt882XH;j zyj;C`2a3+*E`;BJ^9!LU8@PBoagq2#-s$KNRz#gLNgeUPD$vIVMhrSd39$~E54ll$ z5Z!+6J^^rSD}o6S;%+<}%ce0KKg$*54g>`DOe6Ol{Rj03xHUMi2e#F~e?a8HIUQ*G z44nH8|IywrIF$)3062OH{v)_EoWKNIav_QbMNz?+ganEN;{e11DLyC_1w&so)08m{1dFA#CD=^P%7k?1Q}vS%DHnFU&ST3rwkK(t(4fpyg;e7^s1% z6HP(zfqKzQgmVZ@NWc#;)4`&J4}xHz85!(ngv^4M&~9^h3b%nzC_4}V+yYYxO`|{u z)Qf<+a3m6x4i&-&orVF#!w2n72jby_@`2$3A2!g8EFh=@?Kgz30A7L7gEqn;Iv^9= zhI8X#NeQe6_@LU*_C25jN&(ix2h|1)!9H*gDget3*aM>;8BplZ6#>B)oX^dq=ksE!#sF!D060gCiQdMQMF70WWTR^%N1w@D_l0f&AfM=TV+|`9t~Ma0 zn(Fv-7{c5DOc00xhK8Q0y9XCZ2WHj@GFH%@;4zksm4=^uWn|&#gQ}Wsf%FoUkGZ2q zSX!xJT0xDW4)t;Uy#xK6xoX%OqeqiJG&+sTb>X^@PyHuQeEhtf{h^tlaLiyZ&0u{QAo{1p^k$r@Vj3A zFn>>=(BQ(v%f-ms6KN@bDWvyMGhiNub|Ln`T<_vX5JPc7^-6)(aB+7IAg-``&Yr-R zc1n|h=W+@3A#!5Mvb_qWxNu#8qrg)kYV_wrepQOy1);@K4MaRHjRe7{KFg!8pom`#W9R0BD zG{{b+GH80(6&<^xo8VUr?25_2ub9{s8>|6T4GX*C(D5ra{*1`U!Jo14XPWpG6Ti~J zu2@7)1MG@P)NY7BBXSyHS9B`=o-uaCCUTl!R~(`gQ~VibD`B~5hzVf5;H{(KG_sBG zXE==Ba^5Br;$n2fYV4P%EW18;1mH<5PclHOghnr23UP`oIVy_3LU49&B34H z^f8Gmf0%%IP_AkvvZ3o`^=%ptg;xjxm(aqi^-GO zF6AH8>$iRFn=sEoFC?k_o6)V9*Z%eKOUnwXmxV>WV1;JON1ZRaXSyc3-?n{DR$Ft| z_S<*i#M79E^6x{AMUTEeE>tmk`K8P26>3dtzkDrR-elF5xK7>T00f*`O6Q4wzb?}xVySqJE^)LUu$UMhsT`a7ltNj=S_~6%qVg9zIgHA zXj2p8G2L}e@8*1s4LMPLJ>lz|b9X1tI5%of7xtJ-ChLp0c6~D0Y-7w+^W86Av97Lv z!P0+NR5-6rS#ti;^(V?M8ELVWEvi#~r_wq*i58mVo8VmJJ+$fm^0sp_&z?98)zHw$ zlt`Rq!F=;YvV5dYW5LVj3D0YD&M{t1$TV_D@*U_ucb~)X)X#};A8Um^c6+w_l+BX> zhyMEWD19O}*lCXOE!DsD_EOKw?;7vdST#je|F9hMNVzqzHT&b8{!ijI>sIAzJiWK( z-MI|&xjG+*4qrR}vz7U7PR;(X=9iBz%z3VPm=YHMJpR))#_oyVJ1uoyxleJyLFpy6 zlTJK%IHcY!WPU4W&3XE3;;uM2d zH*K70HOCgMb_>{XmTG%q*3@ycTI9}5`H)(*Ir+qisODP>cRxOoX*oy2w%o?*STlWu z@xkpA{aYMQ2mkP$dt0vJe$Apq^_!UyYfQ|F$Bihp8Sbe6{&{whs&}K^=oK&K)aS_7 zbjit|Y*5(N_&g$3sb79?s|D)$trF%Dz7xOX>z$2MzqLJ1D*f%KyyaR(U9N51JdK%X ztbJo7bNI#b_lEllD~-{_EIOg@AGd+$cuGZJ}>;tm;)n5&XhaRqC4k&1?$kaFUFm>Exx7{%P%@b}?V{NWth-dG@#0!)z3<*iYOWxGdGd-E!u- zpxps2hH}*Bmp4Z%W*@R9Esb!g~6^lC=4Qg`MPjsDK6*pMH zWZd$G(@dEi0^e^-v-#;?=YDUyiN!+H~I2J~h?<%H|DmGnTshnm<~q-E)iX zDSG7FdBIw57sTwHeXD=&n##Pfi@s~8MYfIEckFh+;?rY{MlBc=IbwEYmtGg;?)sN1 zb&b}!KmXQUlap-rm&B19_h(;VT2*yF$&B3Dv-s*0J-?ViL3uJ^vrc*h_MCO}@LlM?SRNsm(4<+ca!!1FIpBYK!-pkmv=X(%c(&@JRGs5hqnhr%dnm0}eqMP{ul~o?-_%|< zYFJ!xx+HnyryXpChX=>ss?752!rgJ}M5^`Z@7aA1_&PqwZ!z&sxw&-q|n2 z?FNl^P7Mf3cOJ-L1uoti6CEw4ce0U#Tb1LK@cc+DtWo)9E;u!t!W#2c9 zKgrJ9y>ama`|l2Ml+w8S*3+$b?6`aKlu~Wl;eMXUMTr`2ce1OQGcIm5{$@j`P9C%6 zMoCHZsU;&1C?B?-!ZMXMVY^68sE``9wZ}T+;fnnpEj5^uy2mdrV8g^EIo4NOq$|0b zs~QU=Rva7NdTi=u>HfaTE6rLR0#`XbeB66adaqE`Z8-`pNn1-OyEc8%zj~)KwfC%} z>Qlx}^nI+eDsTa|rH)zzx2<8oqeQ&nE7O)0ngL9O&M+T{3V@||Jv!T7Gdbs@8kDSVKPu%|`0f-#&k;4s+4Az+dpJ#)rn1!RLnMtVm8iXg zuIj$;%*fU6R=q4dH`!fP`eC!;t_Pp34HC7Y`YqI$k)M9Yb%@-Kp+)XFYwS!`Dn=KL z-#y+u)+NmTN~uZQB-XVJIz?9oFYu=sIiG0*e|LD6h3z~|5*j}{!`eFq$RetW6 z%6ZE?UUKHEWbcjH!&u>~mwa+zDqoS%=}*ZXdno zR(9!qrl?Rtvyc<8$I#g6q=W4H=EO42F12niKORvnd!Ct+xoVfrf82~#gW)!y25y6)ELc5#*m15W73KIt~GPq!r}4F+u-^Ib=AZA1OeoWL1T zOXC$~`cvJXNHhJbPFHUBnUZZ^=s2pg*|A|ijs?>~C7bKE8mn$S*R(!N-=}7%T7-S@ zWA)&c(4qQ2o-BMWS9eSINB0J`(DiE$y>&aT9X6`R@(r8f6kNAH?PbWaI*?W!C?M)QU~ zGdRb6sJ~zbr`2bv%J9gnhT<#Vo-deef6#97qmab2)c3TK8}6sv-qf}3s#&HyICuB+ z(w#knCj2h&HrGJPF{kW$V!%_DwGa0l6m`PC$%w^G?_<5nVbX~k3K#57F5?>B)RLVsVDgaE z*qM#F*W~lNSI+KEt$ydbqH<}@xj@LyV>X5iVwbWk@9?& zR$AJjv!B{#o>(|bV%~oLLGK234l;X~@J-jb|DeI)JBq#BUgeqhTPL}srMkC4WcSFh z{eeg1`vo7+^_;$}`9fl!#{;%JH29=-aM+yuWJ#qZ+*zCUQSS|(v~Qk{yVIe$RhBk4 zi+#RVd)Vx(Kc`V%JZM+<{>P_xuS{6t#PwLbe7VU!lbxArdymyVSeBl?`H)A=JMBkV zLFcu1>#j1moiuP?Pq(8w(}w8ZSFOrgk)P6-vZd9z%VL|2T5+xZQ#_XSSl7Dbz?h|; z{^!3<`tCS1=Iznb(^^~K9(R{(92e?!r!Fx2n2d?pi2Kq{lU^+Awc?mmm;AG9teO%e z&Q8xR8dR8)GIy3q@l^ds5rfa)vZ@*uFxBNo+dG%K+{tE2>CbE4W)C>K&#-#>`jFC@men_QNzhKrw^Ew3xWD@dg)0&Y4idZlyBt`Wr1>!^dZ^5%712|Y zW>5;Q2l`gpEV;ht`;dq0W+%8^tzXfp6D=lUON7^Q>$ZnE1xI@KP3cpcG(7Q1_?UB^ zCjNW!%9+iM1xZB_QC=a;6r+lx>OEIgYU{RrY8^R?W>zU(e+u*1R^00y z#q-|KMzwBbpA;RsDemf2T&H+E!+^ay^~33|CZ4H1zob0glhWVG{pi9QiDOuio0m4K zSf$k5h-msS>_S<~xx#KzweyZ^=xJJ-?%$pDZm?XC@?Odb<&);4E4Lk6dLq7${JX;z zsn4~`jmmTM|T|QIZ5O7S%U)?hiJ=Iu2(b3&dQH>S2~_ibUtdR zwEF4714mP%25nrt{>Z+%+}HiI?KWr5jC-T%zb#PJ z^Fzt<^I1A4y&0veuk~3u&#C5N#mBgY#&mm=vnNKh4tQyje`~@*m;O2LK39)BIeCz@ zL&m;^ZroK5Y~I{=Rr~fXaLjc25gR)R-%@o`B?r$Qc|+D2r%mxOw%XTo)D81O8_VXF5YObyZP(!PG_=pk4b#r zBKKhXLNJXDCGQNk{9;|hDU#Lhej{qgwwO;(EkAlt6t$b=%&&*8J$z-;ri2p*#@IQT zMT}B^o>DU8+Uzgu-<-Ppw$w4J(J9zh%TqVvTI#BC_gyTTs4;`H8+Wj8<&-_>D(zyC z!#*8t+FO5ilJk|+h^i@^hjoo>7}Oy3XO*)TEYLsq_?6k29hvigWNj~#eKF_S`j~HK z9xtz~>HRXiDQuct)YP;DyU#1uh^MA4yj$x&GKB*23nkOY*~)Bi9_8S>vh^vetEA zr_xV_1(JmqMhq(GwBpUOvceqPwF6@mCfsa#^|f1z z%!H3&%UJ{7nXcy~V0sQKKg4acgVzgnDqtj^0uLGrFza7(UXr=#8U>mWse&trMLLr1Qx%iO!hOk!qG;(F&b)Fs`=gq%NF7tnfWjJ_`S z^32Z}XU9z1mU(@Cue8>{feCA93v<(=qZE6tp}H=7xpC6E7fTXn*bMBp?Z(=$$UBGq zHaF6pLpn>BpSzzmeA45+uMDo5IVzb)+j^`GvklbUVEIA&f}X~Ui8S+5UJb5XO7X(1 z^0USEdh#L31J>W@wrbiw8~1gOqA#@0o#IKWJu=yL@FjcY(3I~r^nf6??%lTh*(WDt zepvr?=fL|c8;K45lDkjRbyEv_c6IbFdeiZVOB&S!o>atg>O1QPtxIq0^JRIE{8_b) zkIW6aDW3Vb=lQ!bg|@J(=f?U3WRBbSjNW-^Gwc29lzv$!UInjG4yw`fHTqPr`MyDE zS?8;JVv7gpYZbd&R|We zMKv;gQu_Y5y)3HC;K9@luh=b$dw<9b&U0^0ozvYtc=uHgW=zzJvhcFTs>@Dsmz36i z)!AKl=+f5Br~UiyuFfp60o!fWhe-)TWb#H_e^)icwsU9y1(KJFhnyVy;;ekjg!1?g zanX-g7c4y6R`d3~bNStyrh1o#r~Anc8)JIm>E1pnZsF4mH|}LLg$xg>P13Ec_TF3= z*~&T8c(20a`J2$GAG^z4YLq#6eQv*g-`NFg#_A;d7hRpU>s^-@;fKm2yU9r|KBkzc z{`$v*h2(^&0AXAinp=Ro=IKzqAZ@zP4>xo}8z- zY`=4UVS$BZuDQK?H#?tY=G@L*=Ct(9wH))+OYXfW)Y;sB$c}#7wkl2SublN{+vUw4 zu6qZoMw}1jFh8$Q4!{0&UB5FDNymmRqj{X3v~K>#wwdaur>=VyJnm!U>8aln-gh4T zAm&uacpt=oIQpE&v?e2wMoCb_>+;|$DO$oV&1*}7Vc82;96UDdCsWS ziCIm@CbTFNn=2HU#&Vju7p88nv$^0l+%|H<_Q49$7Tslavn*E5o64v^VZ)S)sJiN< z$?lzh*8f@mUC*VH&Y3QAeYqn&>vq=LfFr8ok6W9Yx+opE@^$R&g*US{_Rm|cWZovJ z`OLo|{p{Z3-|oIXy!Fk@57mqIl+`|RS-kG%vaRahC)_W(zSQdIgNcz-j=sJgFla*E zl~;EiluHyTvN@91_pUkC&m_^aR{w$e&L_iP)ucUA3##Ncy_`39@evg*oBFKjdi6`r zHa{CtRB)^DcE3|nV@7r^-9B?q3dgh8!)KO?S5&Qs9?I~l^p>xb>Lo36OQPb|>Y}6_ za|@CS&D&b7>OWd#=SPosC{UuUo!hpI`~6x#MNHnMPIUX^idVM+Pwsq@mc(p4-+%P> zV)du#DZ{6|S-G)uWyQrB$@xpV_V8wJ)?L3Rde^PF+MzZlMy_aHRP^c2*25=y$VoeY zZR_E`DZKtpn=VzMfD(OmO5Yi|o92y*dhoP<$T&^cetXBOE{@uVW1=TZNhHX>y1B3$}T=AEBdtW!^mfr=_(&Co8Fk^u)WM{+P<6^hpCLB zXnFsW+RUH>SCpGliesOeOP!BRIC|#dJ&70dBR^8RcGD>8RyW~Hg2g$FZiy4O>D*fU zHu9vy)478~42*YC2Q{rvLHUdhPDt%KKEZ zj2Jj=8kX2mFLTum(J06YUG&oz?Rdtg}eAoVt$`>F)~N0B=5Y; zW%i5m7`9Nk>PIKl+08n_mNo#n`75OD7f_23G>eJ#oLQ61#!ur08(CO52DkwT$9wS~ zgKz+(AOwU%oI%HrMZhu&0}Nox@xqo|(1V`{BB9MjS^hit4R$aihBo^L_zl3j0DA)e zIe>0K_#1@F0gMO0IS~2=Kp%jwLHHXE9K?h0H*lsmj=up64Em29&;uYF0CoT-1;^T; zV`2dSf+0>I!B95XJsf3&kUtp8hK+XJVkjG|6etX^z3AW+3|qqiL^_VGVI#ybd;l+k zj&Z>dHJX5KLBLHYl1gK$qqS_f!hkjChh7L^4Z4Q|YtV_Y7_bJ=bp)`64f~yOU=2E8 zn*i1TnK-ZpF#reFpeEtK8uT+VIIsqmk4az+I*JqfAR=&J4R$~`4y*wH6b`IG48(yo z=qDm@U=5)3FklTZ7@$2koCbS}!)XvG2mc^w5C*4#BbrG#4R8sE)1Z~cmps&2o?mHAOrfq9~6!tJ5&N7g%H-LG8||P6ayC#-Wu;>1iOa5 zfbyXb_%MMK*hP&tQX^SH_;dIGAAoD{!HR*rPz}0|evu6t0kjKZJG! z!0+r~h$yr-fQ>c>U>{Tp+9m+-COGH^?G}J8fxd%Qzy~z}&QU_Y;R9sC77h3y2B2LH zPz@X(g*G?92e^s$I6yV%Dg2%vumMVjo`w$x$U<3xQAoz&2cn?sfGpq;ViI%}h&6oR z4MEHjFos{R@t`&Tv|!r~vm_(asgp%muUw%j6X7R?si1$tEd8U-0nikQR>BZJNbllk zB`QS?9Wsygo)&SI>_38)sMyOquo4XiFY$quG%=_a4p!1)sbknCr0)<`31bwdjrg!i zz+nVn5>UK?m`#GAfJVhi`~R^@&Rha>^#5a(2rLr}OJP_ggqOw;BUFR~G1g?TjEw-= zfnkzxEC>fjlu!{C1b@!Lkv|w_iMT_&L102~j13iGUWn%evIxh$5a=K(j(Z^yP&n>| zKnGEA+zWxop%S4@jC=gh=%Y!#9IVb2+>a5A@D-K;+pX1YyzW%^MFdc|Fgfz z=ZFtPi3G}s=x+iyh4X=fa}C2d5xEI06XJ#79n|Nr*OtIR;eAf@0fu$La}#(jfNo*< zBO*86?<9f?$2$@Ij^UjI-o-Fa#2p-i1uybigSQ{UJ`wH1c|hQw7&xAc#6RKV1;anV z5mv;NfDAB@oD(Gxweiu8^M`?GC-M-8DnvhVhiDNl_XK|!IQ?t_n?>Ngi28B*2}~Xn zmwQ5@01gOTrWxZonLN5pO!1ZgAQ9s$UME25h*p@G;^PKDWav53F94^*u5d{N=o>FL zQ5uhS-upjkC*+s;lXmhBfpf#T#U#c%(PEr#0=Wpnfa)h?5&(7B72aO}3dGumOD7A_ zjq?+jjYc_(N4pWxrvRM9BoLQS7LIo##uV$PyaUs)_kWIkq8C^^`i%%oAd5%85i|gM z3(=3`?fzq=9A-HDw2er!3(f<;4V*uQ$|Z#M46q7p334`T7;;gwV$h@?`+AOKWULIo z788Al!i}0KCHH39*8=yg2kdu$aSf@cGpjgY@sR1c?Y+g<9qJT{giBw!83C?Ctxb!# zF0GG4wHtnvc^V`PE)OnjNT{gTA6);f?fo~s`Uaht%_i#&2lc+B`_O9rJp2!)rMK0?zu;EJ7pnPqkrcS-i%AaU^753rv^X~N{6!X6+G$e2CBUwGX<>ZIi zvTGt*>wl;_O!?9G%#y+1`xZ2v9Fg4HbkLdaIon%b-nJNbIHcIzvBbG{`24K5HBZkT zTXv@+ZN=G_IXaFj99(a1eUs7}-}=bh(e-BZ=wQ=@E(6uZmC3tkl&H=bIr+Mog~}8Q zyOCF?nhj9x>$+e4{;{RAKW|;zs#CQ!J+8Y|L-fp@s`Cr?E3*R4A}wt{Jii)iIHM(c znL*3d>{cDen^)u4I7i#uI;gg(^0;nj^IePDyWUT8R;;lcId|(04co0-Rm`uJj+@iB zpWmb&qm*3l`fD^x&%SM(k#;`hnMbdETcuT>B&<(qkpEGf)ilj^+3X()7C|RUtUYs8 z9Ug_vKAU>UC3lzkz-!OX7#R&30sp?$P@XLAM7?3KR9Q*Mg*9y3xAR7g6(^S{T_~$O zrx|cLOZ!Q$0{zc#QpOI6uN5)3Xb1AV+O171oIRCrT7mZIVK7Q4HdZza9nT@Ki zAARrlZFu9?uazsBTQcvqzTNgAs`#?zc+Ii(Uwo3Dy+2i7^ev;cC3XJS#~S%RTDx{v zJk_c{>uktd&M?`2vJOj>n@8L+3VS~5Q(NimhLX{VQF*f6hacGSc6i8#Ee+RlTN~Fr zZCMdqUVlk(*b3EeALr{hGh`nO#R_ogrPS+sxgqYaf!GBbP{lPS*6CF5>7D)zXz zsY*xv+0v)yz9!^TLs~O0pN;T#^kZ3$*n7h@yo=nxVhLC3;224lT!r*mHq3A}b8W{R z4a~iFl?S*r%yGSX)9puXAL%oxH@m0=)UVg5OC31CbZW4HT>i_4I(fl<^)_S9%sG4~`)D^`7R(O|2NML&C` z($z}FgKh1DFL=lHjWBl|6Mt~yWzQEgBnK*moVXMnIy(H*jEN`99~Gw84@$C7+tF-R zm_+-~*{hWzmqa<~KWf3^_wTPf-XgKbQCBCVB}e0#PH8t8Mg3*@U*z(o@12~xtjmo7 zZ&#@ISmzP4wP{n_jN@7+T*K5JK}KzZhOTj*r+MLFMes6Zs>~Z7`?+#S78gsFUimP5 z*}d6S&f(JaoPx78du|z&eQo-r8vaoAu*TKv*UHsCZD%%gY0K@D6uNRw`Gz&wDXY5{ zhi5HQ?iv^Cv#S5mfmS(Rzn49uQp)rfAN8Xt?*CNxyufY9m)=(M4y1P)S2xToX*KPQ zyO-|Ecfq-aYMQeKjyv>4#c=eb&;p0rY0jjcyl!K!=0By``ejPe{a0JH_Ag^! zOxfC{th{8qUhA{!vQEw|k}F=ADu=i=dcF5?vRCyUqBLACW6Ts68aHg>p7X}^0^8RV zg=X*K2YK@u+!>#gOjdB`95(Lu%F=zSop!00Y{1@uhtps+mcwwQgvC^M%{*UGd9!9n znto012`xvLzZsTYX1bqg&FjC818|_xPG7 z%<%4X;eg&s%9w9Q)_;bepF@nS4=oluU)8B4fw} z$-Eg}w{4RZs)nf!st8`B`>FrOcWI8}FT8$TH}ONyZ4JY}9O^wYPWQ(CoWq`r_HADw z$?2uEJE>ri!rCSHGS`qeF_^w=unkJeXxK2_?~%dA}$@%*-2x65(ywYU3!{=PKXY|`a(N)oi)Q`AkYt}83s&%}n=h)A*3WK?+*~)6W z6+VnS_hYX{gWU2sFSqzj$KCZV)!L?QyPKIRpMG>(tI7N$`mK9{PiTM89Tva7sa!Mu zn``5=yMcBuUX5mJUwnSW9Ir#dMUeY``9Ht zP;*cJaCq6uCvQV*J@xiX+1Xq&$^N|dCgWg7yM<+a%Vz0B)xRiCEqHNF!RcLI8GT`# zRgI)#~S7_9IyQp|z zS$u0v;R$WioLO_i6TK#OQ=Vv*N?UYLM#gJVm_klQM#$j1H#F*YNAK)qQ>~Mb?Otz? zZhEk@nsRBxu-*%pgVI*y>Td}y`+Cs8aiNF*?y)6(yT1vl*P?AZy>0r}#6$1*`>*a{ zVA{|4=6Cn%+}rO?ZmQZ)ym#L{#@)Ji5eBDETpy~a8+b`D@=tI>RSyOgnXZT7LYTjls_omS`pZ z*uUe&tJ~8Sjm?RlGwt2W>ut9#r|v$^>8+7=K{a}oh3@LtdWD$^`m61Bt=Tzi)YWS# zyJdZR8LxWn+cC?k$Ed*$kykd=Z<}#V*?7bvyV1pZ1JB5=KBc|(%c$mZ$04 zYI-&Iq#T;LCr7fNXXzWcjI)xZH)ZCjDDFQ^H#9s5T@iY5<^2UYa~9upjK6*~Yq08q z+Yj!z4p25ozrFpM)%fVED%VsR?sV_0E6cDg&kkJW*r!jSMqP_fvx=Tv?bLu*p>Yn< zp)IRrd{$m`cx52nG~mE-3$AJ>=GdP7uYNYv(;gN%xtiK_kDkm$?^3;s7UmB|t{7<9 zrB*ZM{?fNMh8A@>>~Q!_pRBoo%)Ku!P=`7e4`EWb_bzq2l5;3w!nP-p>c%oB=CEE5 z9j-l0Zei{4 zrkTmv=E)Pc#~*Q-GCnPP^ZF|XSC!=5-8gF7%EJ%#mCiWS!*ip0zdku*>PkPx)x2;X z^?2Aj>GZV?ffQTqPDWI#0JpH|PSx*EtM!pS&MmpWZg5Js$_@18tAmCQ*?C@nkfQUL zwyq8lKUT&ie;rt=axia|p|{txWGd&RN#$_2kCIEa|0rzs>;jWZePb>=)PCCgV&7F0 z(>Ujxw_SVn_+{ql^S*Do+qQOAZ<+Yz=9@m%+O1vkHtdmT9{oI9YSmH8*n_EzXteRm*h*O4xsFay3h@_AMFMIJ#XZ#ubW2k$#@ zmY#O`sM@T7_EU2*%e0rYT0ZOXd1672e#zDe#rVs;0DiB)40LD8M&Hszucg2QaI7A z+0NIw*eKuN&8OUrq0d7jtf(^IpKRQ6cfp1*$0=LNIX%<6#F}25Qcr(Ye&Xerp>XRvFIeB5~-L>4U4aADXqB>N3O3m*4DuME0_z*1eC4 z)eR0Geryi@wkhOkL)f*YFT!3gZ@rxVbjs7~Ne8^^7TyY8Oj+5yiozIOrN4Da!M8=j z5-tEXAbx^@MIvjV-twOM2d3|rFVE;fcTI|$cRlu;%)V|{4Gu^6ZMN^Zv(RGxsHmBi zePW~ij4jGud5wHmdfN1%W%%Pc)s}n4hm2feH-5EKkR81*M>$!&F_9^!k#jV zH-V--PwRXgR$;ry>eM+2nY8O`sAh>Sp-Xq?TQtr|yL{WlN1@clD81+~d$yt01-EN8 zH(#CXb3r>i#;bL%@`@{0(xV2acVASrD16SbG_{#ViOIzVV;?Kikwv2R0vD{IjX3WYQtUh>8a_1*^*`1E$Ja{CtCNCmMHg#6S7V4t9 zmO0tst@2j2w8{&XJ^gZ~L?5d4uc!Kd9j02DIj%zE!bL;PBIycK4kf1KWM1dDO0m-B zL3fIm3}VzN%UrH^2>DXJEv!0!YT`({M^yn~T{MO_zVuulGu^yg-a19&%C}vSD&eVD zHy!~)c~ir<0qP5Pyp5GoHlas7u(~HjAMW;9CB3y%&iIWF3X-C4RV*=;H3^XTuG5aF!*Q zg!^shf>mphc+1scy8k5EB#Xz>M>lSk5B=~wv$$$V{MVZYyfrx`YA0Vm&wrGkpHzDB zZ0g8UXBLFbaWwUE3elS^|Jtd0<md<6UE^|(=~lVUuK9rhvHFkeZauiuS0uv?d&~u<)nGGpXWbZK^fHg z_{3 zW56^Pe7ZG!n@0q5 z?cr;0wr1O8A8uWlQCupoRv*}UeYs5J&E%}tLk$d)S6)su8+v}Vuj(M@xmt3e^+_ch zi@7Q)9^>m4#SDoaq7pwd$@pbxXiD&z*j#$sqZaD5k{yR{Cf`ivC`|8CJfoqatyND& zrOssSl}*vn(N{OElz+A+ckR9zllGOpnxD5kerY0g!9w-zmyZ{fY*Nub_i&S+*Vd7K z+8lii{Uli_dy|6w4o>n0BV2Y~e(f>f()))BJ!urTaL(R?Z7$^p*ZMzx;*k;cR$}*R zSF=wtJ*-?L8dTSvc1;{jJ8k*y|6%W~0_w=Nc5O6xa0w2<-QC@TI|PDzg1fr}0>Ryb zyL%uIB)Ge~yK@$j-Mf2t|KESk#lHH&x}d09RddW)v#Lhwecq8?Trpy+xr*-(U8Ncm zz{WbF5^e5ht7=EF#CQoN1?XZy8#} z2uJD_xfT|;tlp7w&4r#wJNTyGNm<(&0u;Spw@ZXITPEi#doN=v;YO~+2v1W2>Gi9l zHgi^WIAukT?wJYbGo2Do*9au=a(xtGRK_ZKI|2mR-LI@eH6K;6^83(IZ6KMo;TGv~ zMl?1o%+DQ8YXdfwMPn}&k0^r_L zY6FN|Fcc=rE}Y4>zN6QA#{cjTXHVfS%XWa%7sMrqkaOtBR=5DELSiT=4`a6*EqN!K ze))+HXOZGJaz+*``lUPM%Xa808GVvv}&l>|s(YXkk^dpLX`FKN}-mFQ5i0h6X{ z@k^jKyOTGf@8%(&$S!gp9} zn2H{LJze7n_6|?B)R43cd192a_3_*`w7{PE7Gn2+kCf*AMx^g=kipV(iz|@VjfWC56i)wrd)4X8Cusgtq?ea(=kq+1#$(-MrCr; zRn-;oDG*S5d_N)t-+hGrY^!T8`0i$CzZ&>kfVxr@N*TOt5clN|OQbVjc(;lNz5a>G zZ!50|RA(kq-pvuK@pA)#AiR+Xwaop+{XS9?FxBhgxqcSKo_G@;x~$(mXICAht(~B|7%s zw1hFSM>j-BzYxX*PEdVJ;DKa&I+81dYrtUv)n&iWnNuxgVXoXWU10H0-dAp59JEQxA#qgUC#3;HNw<0=fMKCINy6? zklstob0Y;;tj;20SYTq=lU_iQq$8{EV7ZtVk24OI4qgZPjpybQtvVZ+_|h@r5#g8k z0kQq!5#=?l@2Rv?cQs_qZ|Tdj`Hn0QFGY@GYcx*U{%SI%!pKD`O9w`%H8_5P2i*5P z!NHPp2=y9YQ~*cQYn(KD`Y~Z*VfGAcIj=&cJgL#ndMJ=T+yL_ZJ+)rI}4NE0d zv2jsXcfK6d8jjO7!FyxH0hijIEv5>kflQdBs04CC7a;^LEabe@+88wT88T z4%a??luws4{0=0A4bRz*#>ZuCb!s4&-T`T0ubrwj^y-J#8<4)>Hiv_@S-8{|M|r(b z%u0OFDolMoMMRQ4zfC>LfN$?JwN1YSd}xil`cWn%KtKFVIB2xQp;!~WXlNS}pU+T^ zvrViQU!=p`ARXuQedl{S|41kRjB z$vXS8I`8#wr@q>L=L0RJ`4Ykg>YDX*pz>*KKwarm!wTHNPC~qp-RI zKbJE9t}|2 zI(`pNYNs5qaM>7)rBBAD@YVeM(3YKBYiZ@8Lf63ThYk;6eIZ2BWweGWHZ-vcozq`j zAx40uEvLBMYnQL_r64sN`)sDJg|3RB37QGtz6Ue?wI+*M(UkUsJ;Z$~`Eno-Ah$?@ z?NO@35BN5JnfVdcTLEriK81aYnOI%xBOQ!vP)1JJK)OJymK(5BQu4N5y?z#OgVG}0bmqD`&~#A4BfusA3rn$rp&=f*`Nw$L)Yg!d2+_n=#A4t zar-6sb(N=>1I=^$Z1%p!=M5rI$O2IldzC^i0E}1zF<+dF{VFx>C4eYN*sPZ&; zV}S+{n{1hEMG^(ZlfDCKj^Q)1KM!iSui z6$2ms3zd$w<@He~l@5iTqLV2&|LS%IupDjM*+9I}ySud{56n+L{VhdVZQr_X^z@E? z0A!ozjD|IO2Ld;8;@K=?MIs;UlvJiEu6DB#h!VYRx%=+$QCNQ!FOrb%A(Z3@N04Kb z+tm*xeE}ys19y#BrJ&zR$r6U5FMTimeVmR6Ho>0L_?P>IL?v@Q?=p}uf&qryJoUycEAQUwm3Kyq$ymt zincVkb>eV5*$p#izD|LAWkz=IKijDVk$B>;J6%TU0MqzdlD5SindbXe^@uc zG_Ai>=G`#{7rq75mF6z8>q_uz+V&Yv0>5de12t+Wwu3$Y4A1=Td*UDt1SdknR|!la zqgV9E3yAX}@i|b9OBKwHh#M}$99Z8is4dBU_V;wtn4{Dja&UqqyKbv(+gYMulSu^q z5~KO$BOfs}YPSg1Ftxke#D&WR9mu#*K-0VKBTzD!H`v3DRzbyJIO8nqJ)A~Yt5tn< zC8hX2?n`2H*}=C>j1p9JY4@8cf8?&6{yVnRsilt3i-vr=YsZ$m_48bK0mD`T-CWrH zN=|@qT(UtWH%99|s}x8c&#{0IZ*x^|vk2epSwRkE7A z4T%k=BlSwI+n<^94&*jGGB9b#45{AQ4AN!c4QJ>eQijCr^-)yBxRW2MHGT{Kup~R4 zxVI60Xs$D+VYen>04^pgW1;5KFf&JwG=nyvcMuDn-?7RFj4f%V&r18Dmo&+ei~Q!D z?!m`nvE!dS2lkWjP?41=V3*P)qK#?0cWG3^+v~HWdxiaaeV=OymUQ`&l%+irVdGPr zJ{9|;Z6K*GGH?{Ve&Dle$AINC`Xp)XR?LlC{g#60Y^%%hyDo8FmEu-}( zGHSRSA7gFI(cxkI2$U!rOa7T%f08043#G*M)Yhx_*A!<-g`lK0OT5?ZGsPci1R(u*&?^*%Ur9FX4N%~fawHA9g-k{%~O9-kx)M_jYtg+djMD%Sa zAD=2#$RyDMe&@T-O9pzO2dQnSnu%N0LqaCg`}5;X792cr^zv-kWd%}|WSNQrZ$Ogy z&F~wcEXZ-r^eb~li9j=OwcnL} zV=&zzFhzC$9FG1)P}9u+6HK9JbOKyH*p{RTM2!!Eul*-2uNreHJN})KcWpP2JS-`6 z4%6YI4mD#eN-k7(A2FTJ+1?^@3S+h|yy^p%stkyN7zlc2Ep{9|#jP0(Ga%P%lh=TF zHahDd6(3)E(x3(XlX%^7ek(*}!uCiQ9|WuF}aukFo}kmknFehT7*ZbzMo ztx{cU5YIH*8B%zCqH~lP%Q)7p4tU6Xe(Vm4Gk97g-E>AK3%)6;QaiXq^vtSAS6T2> zuprH1z$d`_&1$YdZ)o+H{7EH8I$^T%ASpsIPe<;ox3X`>48ye6#=zPjc%ml!+4Kv( zksvSgrFAQ;Lwd9<)rsnWVkh~Y1WI!Ud$>`2y(KvN_*Qx`|@+_?~f`TLt-5304fcBkf)=%Btm7(1j28Wb<~uE*9krez86!NFvf{POgu$-Yz3aP%ZE zM!FStq(-Kx3p7nHM(^%BEzvvfmEyNBl*O3Xo7O!&G3EdA)fy5B z^}?I(v#{?VxLZ!33iSCPoz9?9dt4Pu{;JT&EnpGkm&^d|2jYse2FgqR&_%e-UN5b{ zu#nT`seoLJ3adqn^o5cXtzW4A-DeW`e6WZl^wdnFc%b5 zD*5sU9s1Zz#H|xXMH+&dS;(*wdWhnF;Lt=%99p$H$iriChLs`x^(wzmURI!487k0i z9zVs+HjcglwFQC0EX6H|((4xqlvWQaQ(t+$*_LQ_^s8)j3QFP8A9aOBo1|6S(mFy_ zxMrn829~SwsvHeHnot6ca&N)t&FO+nR?;&nhttmw16nPaHt?|-9DGcu?0=f2zsk4h zR~IVpHZhzK^4JN?o7brjz)>uqj+O8#)TQ*c2y^jA@<+-MCIx!KQ44|JBuA$>o`anY>}^q7 zUF7sF_Xxql1o|<)CJi+faP6$Lwb2ID;?p z6+4y-4}5aI)&<`k-(A2Kgalu8Wc|X~tf|_tqt37ri>h)=$|BMW2{KHXd_FFz4)qv+ zA$lQUOq&J#Ag$!u()GLEK>&W;CEDuu&=9tBqzz~uK^~jlBc*FbvG8+4aF6XvYr@7T z@D*N;=4wGr_kJ3%OIlvl;(MGp_J>|;yPNU{%eraT-ebQXE3lFDxEu{QHP(4Nv*;p} zkWAH!a&C%vI}m7y7jka8r>qHdt4lnyT^TLEkUyI@ilcOR<2yYxc8@V21TP?edVtL^vJI7V@2r@ZJ*bbH1pxcDUis=1d!wFdtO6w(!83Zin`ZlVW z77qnYy6XNLOB&;LCI~3t(?5-c}UU0bT&0&~6qQq*Wp@Ph%E^0ipiX zU;8f4)RpsUp}i}9U8JGcpjvV4&8??;etJBb<`s&l}0~$Fz}x zDr+Hbx`|FAA#0N>4^HLpVWekLq_Epbo|{B$tA?Mf%ewm^D$2%}h4~vnc)br=rSknv zsF}Mx`LYdylaR7=9JP5Zyd_1{XB`!GyfD=R?0mFLXjqASX4Qs1e+xJw&Y3S{+zNy2 zT1M>?bn}^~(WuB1gr|m?YX*s|w2e;R$4tDNgVa0U;<0SXD2{1H&{c{X)a0y=*s~3l zHl&HJqFjlK3Z|p)xz9kaj%GMt{={vi9{{>fx{?L7>MQqLYv} zj+<+G6F`lvSyy1F>4Ze}RD9lF={&~1>Ao`5Q9PJPPxFih zkGvWZ7exO8Zv}=&x}x?vTB&D7{4P?`O;TLdyisD5`9_s=Wl$ySIAm~&Y0Dm$kuff@H0w{>51&7!(DxoxoAPDzh&@wbc1(k~$}09|l9N$C z73!qNHEdhBUuy8W7b!RKYOik12u_F1k`S&_m-=elJA~HL_BHn)C>)}rjzBW{lH`g` z)gk|cw%F2)aWqZv4flsPLJ?+k-=n7 zl(x@psWJqTg=0b}g6=qCrEC<+bXT!mZc75G+z#(MwiYi_jfj#b$ua|RO97`cECBt) za_wCNXR+vi-SY}~*%%9KUV_$^U&Za6!#f8zbXyw7b)_^CNGGQcAEs&egb&MGAQ5h^ z@WkddR!_|;Lh8PJ^(Wu|b&^FD@e6CE8j7`D#L<7ealLz;-pEwt93#zU@Kkq?lb0CR zL%^^`V2^9ROS0QW=YwgHX%v!gMAlS#w_j<9nPiNq6EB~4c%{NPqiU)CFSX5_W7Y-{YvCjf^l(9RV~kynvS@? z@npUf87&HtQ7|&Fg)jFCv4V(ObeoXIGANIg=Ro>2cvu}*KQChsu}QeL(>>)qRGcX$ zHZHbhl0WjtLR&%`G7GBy1{j2ZV87MlLQUVdszp6$(v+bB0E>v3eUnqg2@P`*b)}>d zo}pz`HHtJxu}V^xK#BwzVQ2w@C55+C^kmykyAPoJNPZfB3q-N}0}%BHTm8!h^KTeZ z1zB-P1*!kAa|amq+L`NG|G&eePyXhAb#wm`iH4I1As7mHg$hAf(P(UfDhv%t@do{4zNdm0Zktr+@C>H0KE5N z=MF&oUhLc-9paxrQ$P)b7dv-WKpOx|AK=3budpcv#P!IY0!Yxu zK6O%7J7om?;h8&qT>IP5 z9q`+ep*uT(`h4b282}LGGk5w}&Fb0Eo$+z)lc75^U<{rKR8~M8v}Z$i20%NW2~<`< zU9@Kcl^K9VKDoIAI8Q*|JsG+`QKZiV>f=Vw1S;V0&jcz!3;3Hr1+@7QKLv#HXp|4Y zLIE%+;BNrZ`tkE*4gbWM0t$#dbEZ#g0VF734}d*CZVK1~AjD_P6tMO$DCR%7oIlQw zzw^%h3yKMX3j{>f1UdD$SDrr`^Zqe`{|UwXpJ(j9F`0jLkO%btlZ8AxU`SZ$o-3;S zBb50+I><9W?fxI2%;)M8j~(=ffjnTo{`CU(bWQu?0`?oX08F08&i!8~^M9etzZ%E` z=IGx+nU4i#p3tEuC=&qnJ_BNO&!E?0kl= zo(umx_34X&{BOhhXYlOBqW{G}p5+D3d;#uWFwEx|U+nvzfJ?y0Jfnet;d<=17pwUf z1Nj$I{ucxJ7gPQh19<>x_K1ctyo})s()cIP?ze&b%ev7 z_q5OFF$9olPfL&SG0*`x)TgCquD_ad}8Y!kMLq351`3so__);0Xutc z8RPR90-E%+&*%662YOn19={i4kMSkG=NMjq$rtN>0P**9ZUcNNUd~g-=NK8Ed+G(6 zWOyF!CukB7)e98)e4YZj;qkur-!!{_y3PE@J%yElnc<&q*nnHjzn=2{{bBjfX7|ZX z5VneAX!f1D!Je7x9GLsjF5vt>yaUtl;lC0J6L=yxLuCb=GDPtZD;&&jQHR;e8<9ju z2!Mbg2%$s}iU?0Dprj_((BjTJKP2!WrL-Jem3R~tb`w>c$J?CWpI^8cy_aeICI^iD zn$*~-uRri>Wt{KnC^I5C{TJFMbi`=fnzuh5rar{zq%wsPPaWxj{u~1S+V=6nu5hv2 z%KFPnH~#X)OydzSFmMxmI6UNHsJpEzUu(+)w|&OL`C-7KYhvtrph;lKP7v(Bv6LpICW^*(1 za#M5A6Wf{cwSodCd0sKFa<=HyVBy+aLvJU$X4yjh9MYU<>EbcQ;LI^OZH)t-nGBfZ zp=b3(MnFI)9rVcP!tn7r!fS1**|?>>^8$vs>n(y*MLk3%{c3aO1#*LMY?TE`|&uB66i0d*70%@o<}6-HX_&|1%Qx~qpbh~H#tUALA2Mpj=+~@ZopJ1t!O+22r9mnxhl8D9nD!J9Rf!X=i%UyMXA2#$6YVMjRK>J{uv|a=1}1}+1=S0r%9r3O3CK7#^?uGb zAP9IfxK!@@RJ-hS4iDLyn{y%a#sLQ@xyf4e(#!ybr;qTnD;Lyzew;2OW`XW(6V1NS z91Eac*%y}BQsiJ~@fUv+j1rt8zZ+1hjIpxBJokV_MSXMd180UI{yf#`a>93ncVMXNdotXTuFgLl(!z$>$I#xq6%sC0hix2Y z{7jLNt#Di~U+_hNP%Y0F$Dx%7uJLLs5fp*LGudbDumQtNrC`(RvcbpPa;wmo zxToi2c=oG;sZ?;+P{_UTxS3ekG=AA7x{3bubi!?jYN5Y%m{M&g;RP*&@LNKB9|?3UnMw5aFzsX7$4 zDmfC8$d`2YXtQXvYrs<7*selL=J)4BV^B{*O9eu`!JJH$niIYfb!8DFVU5gSa`ZOz z$I55u_^FWU=DC#?HFuaqymDs&qE{(Zk86+o06;Hn7fUrgnNyf*-iRfRXAzZ+qWsXP z)8%k$rk}}2OOSd6@TA>fxP@zpdJCD$Xjez1oM=^MJm)*MZ99o0Q!}>( zU?+u;q_;XOS99TjdZCxZyno;%7Qo4loC&!Ty|V-|yMHaTtY$4;Y6*$QlXC@shhZM6 zL9?{`8ra^M2oAXU$#%O&C#TewZDsZ^FgQ}*(S>G*VLZsB>*Ir$(W89}Cg9bUXk!r8PQSsuk zym;NO*MXFQLKYp$n#1N-x*AqImfT{b8U#44ad}&8hnkm88ZExW(=72pm2PwIOI%o% zPbzJFLVg{fZJAs87CMo$#P?f%VR24r{cvABj)uJ@{JXbhAXS=rHH#Tc!ZrE+IMi^B zEI?SVN@W670yP?Xr_UA8D%yX3^UXnV2?eg%p$Z)%>tLX;zX|?)!~RXo0=3ypE@r<= zw$C4QwVwAufgt@qLfnBAB*8Xa!y_?YZg(Z0^Z|cOiML~zdk}|CbG9X zQ{FWrK9i|ZYJ<$~KDz1_imbl}g)VG?PVzH^P$Hq*3B^PTvsi;CY|Uphsgx)Z5$_p; zmQIl&8=N3`*(}C1ej+-h5tvx*U|1BRSNs71LbV zXI>=F)U@(f$I^RKcQyd3D9-FRR#*s2x!pCBNYR8Udh(tUzi6AG(-idsjY3pe{1Ids zrsVAU_p^@M?8F7F#h`}Tka`pa3aB5f7BNDRs)CNrUXuLTDm@o@1%9f9(+T_qV*+xJ z@+|G!E1!_kF!8qp#C!lva&+E^J%Rt8GvIKchu%A-w2QnvJlD|M!x$VD$!he2NMW+h zx`C?N9F^YfyeC#Lf7vvOtdN_Do|%*BRXBy@Y?SDSja$h1`4CZj2L+D#&Q4 z=>qFkY<*RRZct6JqLHnI+`VP8J?;l9>sKnIHU7qoiqzz?wabyuJeQmpN}GgmBr&>U zm)qF6&4Cw`Oc@Yes={R_DYClL^Nxp0VQ$ppdxISsxj?-<)Qvvn&&H%gP)*fMm91ke zkghvFIJWNrd0I*-*B{hu3F1v0)?$!}mDUW1kLMykm^xUOlY2Y5ZG$j{LC@g-91Z2$ zWTMy@=o$B)ov`G|DJt4%wof!uPNZETjDRPfssSzSd^nkmnskqYXbIVJc8lsHzfDDo z$yMXL#W|CL85tix#6x2F#!~?{iS9sLSXES4=w+NIttF8T?mcytfUp-~uLO^j6i|#i zUL0nay(WpRjf#Q^ZNlnQnp=?;ZJa0eULsxCdkXs3HE+lD=Je8Jm4jX`Oz}pNlU;jo zXw{B*GT>!8r|(|RVdq)L_8Gl~z3ilWm`G8^oB*OPtXgbdORIjM*O2C9zYNL(rx+KG zw5Tukaf-kWfEN)GuwL7t;AV*pVIKDy34D+hsTpz_9RAa*N{Kl>mBE(4OAhc1!nn*$wsE)PSZ z^W3ooMx;dLb!w;_<7vK;ESUnihEK1CohJQm6t8w3@_Tx3y-S@jxN$w;G`Q|DU#E8! zp1wWRYJy0qfAy8L6bwWTzfYv3?Q70EiY2&HkUl;(uHdmo@PpQaWu}s_t;*RDnT#4h zEJtsNPqs}fOdYg^RU?EA22Gd+3ipd9^;Hj=^B7u(U!BsTT=j0@bc{E# zp@2%d9lv!OG|Ltf2QQVaT#&&2uE?-RG8XfszY;%Mpm(*wH^Ug^trrt*?+$}FDDOps z^cAW(P)=FqEgZ+Udh~mj(}aR#;s%Wd*6Z@k0=#nUd2FQtgC? z%elI==v&gZ<)j(K+l2g+;ht~b&7&w@qo)@bW9xrh3{u`NSqNGgCJy@Kg3@58nAa?n z>@S&7T|Dp>RU}$k7}o}8kKG4P(h}~i@HoFUZG?B{4(Yfr@GcC?_`4%H5Oa^6MPVt6 z(a1^k@=Gv|1U{_r!%AD~OUaskwRPsYGw z6;Kk`70E1?OU60F?tzszptQR(7$M*yvnk0rJw#{`9@e#0ltOxo18q8jLUsWL3XclG zo+Ye-8dR>T_CY2|mSR9DXVp~Nnvj5$=be0vmcqQ@Lun9FdO@&8(%YI^QH~BMr93-3 zB_%t%JS8ZoygaBZ$Sc`xp7V>PkRy2B{?qrNP9H@=M?p}sgyF5eZp2$q4Ch6l<|11M zF)^l-*Hqqm=B3APTjp`Y6nyenyPrYDG-J#9l(*1ccCLANcQxi1Fb^71pc?~0cyQhp z4IBrhP-ayO%i*?{a1%J#TY1H0yY^Ao{tYi+AX2Gp~9#-OSG_%QVKYckw ztO)NKmBt78V&TAl#3}TNYomZ!ftgTqRDiQ$g&HzC?d@EPq&EHH5)w4ACB#8R?9PHS zxG!a4RwtK~3=9$P7aNd?G}!b#tN?0odjD{Dy>R{RG%O>zX}ZtkJ^`i%b@`ygL5o+I zor$6#DXzg-d{z+zQDI5gab03NA_Y61A4j5kFoNFQXiW-oI6EcNBhqU2Q+HKNYVQj%AlF^qY2Z~q3%ljKs-b?R&NFCn$DwO1`(_n(V%b{cDAr`mUqkPDSQ z$QJmS+0{2r1m=}~_4v6rD{6mir4&G2oHk37*)5}s&a}tQdS;*g#n6_BC9QXOkQ}W1 z#G$E+PIt5^ENLj(*l@{#1jf+7WWMBSDTJgVlIcXTMIa zfu!Aeq7IICqd8in9Gse{Jln|ecLzL%1>k<_v6|Wau^Um7evMK^GKT0ed(aNM_z|1YMskCr$eW09iYsLt zl4OOM<*nvl7xQ+>KB?8SlcILfq*3vc6m=_nDX%2rNL1z4qisCgnLkNYP!)9xqssP1 zB7lItyEEx;mYj9dL9}AbG=~(G6we*9WSsIVqu%7lPsa%OfB~nkhn#1VZ*DCT*eR6~ zyq>0`$)t6lJ0Qu9VD|-P&wcJz?qevsB^5rkvrmjBRt3%4Sh7f++LA1cWCKNEwoni` zv%dhSx0?8cmmBX$2ljSeJ#C0X8;!uH2^}9H=M~tG&m=45-T4 z?H++Ml3Cb}CrIe#I*1OY1XzCU^782efaf{C6i7#eFW)dke;6|nItYIu@snQ5@S|Jb zz@mfj{v=nP9(^a>Q)d?sqktQL;r@%&8FX#eE~OGzR&`Y*Ub|Knv(6NxED0|~ZCbQ! z1Uy!P%IK9*`~5G=%$h+&IgPlY_SNGJ?q8L-x{bbp$%_%Q>nq;r|^H8p~yRc?DGa-45EIENieJrkJnoC#DyuSjHsv@M%}lGH$_?# zIlWM*!LmDhI^+;JRo48joR<$%vFY#3YjpOg`{Olc8N2SS3V_@)?>l(RAqez8@_54T zLqrg3&(|z<1T{A!ld_yrzi-xUx0csus1!KCi=T&iKziqsee1SgF1QMQ@3+iI!e(bnLS4z3A6TRpPf+&*YTpeCFriuq!dnO-=ltx& z6i2j5?{Na$gy8Y?utO$ijCJ4(^#P+h{h2Sp74MfeF>QkgHd8l&E8(c) z*%6PvKtg$fnh_ia^zzCQhG+28deP9@Ix!EozNZzOWmSbJJVzeWY*Wc*H}MB8LnO5l8W>+8+`;s z@!ae^jIEz;_40P6RL&UGustdTRq6t{%ri_V&OnC5l_pvN0WR#3pR?M(AB53i1SvJC zsN|cx2S*+{$8YFMC}|y2&*n%K8c3Js+I8+5*DAM|UV^b_R8XsnwZ!7svsduX?t$Si zCH!ewr7rC|RoGi2e+a3rh-Da4Qa3=v#As2J((sntneJV#LtJ?h=VxeP?IwuVPHl^D zjdpLAn*-~-${ar7eWzRU@VgO|vKhg>Q_&;UZE0Kg;nl9ItMm|IHbBuax3b&t61?n! zQjw#3gOd?X$T29oJmR{`is7L@PYHwMGZbRAvBxe`79xVf#8wiC;c}^YyE>u#V<2Pw zL|EOi9^JPoNpDwx2J1CmAPh8RvVD;t|D01KZEx?-?wWN@GJ9<2l>uJFHVWDOjZ4dx zpL6gMM|*O&-rfu~f=00l512n<0ffaBNp=WQdKcWhd3OtYDA(cw@Vj16kVG|_@mr{y zV%3tdZF1*C67{<7bi19ooN^mD;xkw-LuhsH%Yh7W8&c?K1|J!pg53l{BuVcmj+&Z9 z&mxB;HEPBl$U=5j0)u2CH*W6NVJoQ*=PHhCKB<1fVZOEi+tEPWvOcata4z&F)gn^hJZA{jl-xr%t;+aL_OfkCzqqA`8T z#wmG--|d#m{FnRBZmG)%huh7pV!K4kG$~DyNa?#XwO36~N zX@#@Ynb4?CmgEFq^z{SWqHSS2XX_#PTjS^Id&GxCaL-3#i=y`+j+~X0Oqtcb;A)kp z@D1!c60l5=7ahlQXXB;VAEe)kK$6&2_k046{PrlU_EEtm64r|nMjTR{y zlJDIhAV|1la8{4gD<>I4M!071F!Lp_#i$6A!WtQy7GQm?&`DAuv=HWDqb{qexNUD* zWDVT}z4u}C^El*n^DUT2^1U)y0?kERyms7WnKUM(QHdVwB2^(;OYPBKG@{d(0lU7q zw(=L>pFe*_?l)rFfZ^7i!-2WCoKj$-V&*9V3d_?4}t;h>`a>Ue!5+0vP!RDr=V{|U@M!-9fzshl0U2*tOo zdU$_%9J&3={gkEpG>hTJPleT{;QQ6KrCXv6^!e6A&{9jFULQXy8h<<2LUvvYgrisS+I-hCoE*4tL&ZF zQ(m`bAY`H|=LGP>QWruMU%^2X`aZs^m8a;cdS9<{#Onm)xpvoW{!PzU*iUj_#yO{f zXbh=(Oe0N@wArCno4& z6z+1qW#DvxIrrK~=L9T2m?Amc)8SgTZ|$P}AxK#ku|QE5>|A*D`lj*q`JL8y%Pf8| z<#95%8wZ>&naM7AOof@KPH29)KH!$l+f8-lar^USZbPNHs*N3)W~ zOw*@dH>U2Z6h9QP)w*H}DdVJaXw{KM+SNtJC{M%+fZt~w#9s;TXJVpgL=3kVD3;@f2fEEy-GXrSk z9?Mxg76^DOX94)eqwF{Xx|I|%?wfhH*%YU4gf7bNA zbSEq8lL+8{g=POMEc>gl3@|PKPFVKrhW%U6^(bojm;3r}aoLO1>_vR_EIxX2`u~?~ z=C`=)Mf&w3OnMgl0LCd;Hcx8{WO;qn=CkPlbbi=ZT8oMLkDY za1A_u7$QDj5@skU{BS-JlkfgSjqmwE$td_UMbxEHzv=DGaB@mnO*`Y{r8JfGohmvf zCYC5z4d2hjClB=R8#&mYS1|TwW@M7%hNG*bF&J!Y#JatMVC|B*;rf$dowh($$FFf(9R_x&&>pPYggLNh% zW=7WR9qfWsIDR1U{KzB=MiRA^`Ut}Iww_oHrHY)emx7%5vs6%y=k;d?P6>48E)TB- zoMfCiszor8<7^=lC|?!utoy;4haxvm4PL{T_Kic)sU`~`R3!sbw94jj?U~TxTwp0% zEySV7ICDpjuYMOYRF^Fo@!2Vv#o8F@3zWyPLky*pSl2+I zI>uv@)Jzqc5}P@9rQtH#qwej?k}!_;U!oRsjuOd&Fld*~_dW(w-HL7QByS#ArP5i4 z<3WY(Iak!F9IW7y3OykC5x0nmn~IwNP0-B2F8V)wg~+=9;kufu)yW#MP#0J6lk3#4 z#6QYlCCo@-ibQr2UU8()&8D3%-ik3|O!k;?mG5fEy2Z;7H?C@I+(#!Xe$C0)`T%ac za^cm;PRzt9tn8opn8dx$&CvEGp{o3@)D5S1mbJtO3!V0R z7^j2Ijr-?1&T#K8N&}@HtyLAF#*5+X3tn#mG(BGhGEY~TjM7)y@VZMV#c*Pz^y?)U z;X86aG1^r~^jD|{zoW6~B6OM*BF@cSLpkjm5IWh+c`=?vDY!4d!sKo@o%bVaxo-ds zrlyk5bmR$385bnm)_^*_l0VGzZ)sOSs0WB$89UX<+&Y@ya&Z75W0MPi35Ckes@b$x zNpeaA&!RKi3=WBjup7tcfg%SP4j@zXrDN%!^3A^dYOYgoD)3VTD2r#X?CXGkwZppg|z3cj629vZ(JC46Dz0&D98V+S#*K)y7fo<7^ zF=fm>IVtjSvM?a*M!R?lib;IGb)nDNQHgCFA_`kd4gFj*54MpZ0ftGf#hp2b^qt28 z*S%MJVU7EtwUi?@5A|C#-3_OWP^)W4I<}8U#-Uy^$7V)$`fyn>m%8L8(N4R#I?Pd= zykzaZg72%{VH|)i`aY0|5O_FFZh^s{*3?lALK;NFg)w#GZ@r3y=;m9_6<0KF&lR$@ zxr27%R$*+Aw7;WOzr)2f8NO3FYdgruXwGKtr|zhe*K#9dDP zh$;$p!r-VRz5JST3@ZeSInCFH=Mv%8&8Q)Fb0m)F(6Qu~I}o0?5&Gzzt-%fw-a)$L zD+~{WOqBNrd~%&(&ZT^bIDI;x0T*-<;@?doL5YxmrpysV2_f>#jgAfhv(Q~kxwOJC z8i_W=d2Ox4LGTVnK7gv%2}1nsBlDkukAKK%{w@cTP!U&CrW7(T)m64r(6zLYwz9N( zyfq42>RIWVSQ_Eeit8I#+M3upQHwn#90oRefP1*ErR^gpVS}&10H`yXQVV`Tkqt^-pd6?ws zj{!Z7_rFS|F)%XIuraa&D#!hf4^TLcnTDQ`1&|~HHvXqvij|q22C(6u%cn6g(a|t4 zGCdw?((+vHO>B!8=%KUVl z`J0MG|9<(KQ-c9e4R!bDR|6^HB=OzsQQc7!MD(5!=up5uCE{Y9kiK!ATqs1V{Eogt zk)Cn#rJAmMbn5ib^3p|BrbTP&m=HdQPL&kuA$(?I%60P5n0XVg&IBfBt1jZZL66ET z545y)`V0GZD+cBt9_|(%CLiKGfg#(S5g2*^0ROvrD|m=fh(U(@ZL|r^5^5Lp!FnLB zD#xn?ilWtY5l>tof%*cd6OJJZ_#R;a_-OJDxC|?hv zlGuruSYeKgY7m*cmB@th#GT8EYsl7k;MRtW!kpu|FRNflKlnzq?5fV-rj-)##9ZO| z+~<0F>Y-ZZ%pf9ZfOmZsy9mxMh#DZ=6@d>|>@9FA=WFn8K0zj^Zx{tkChxLif7jb= zBQS3@>f>)QSSbTe23p^QV)I4YmF3jf6l5C4#cu0$#0onl=uO}F7>L6U;)3ozJC*Cl z@rm?Yfi&S;)Ox9I;j8fSTwtcQ0n;)WGw=75{4m-h@Su)xH7oYBA)^0>w{HxLY}?jN z(n*IM+qP}nw(WFmbZpzU)g9YTI<{?f{Hpgp``vTS+vnZ;>(-yDnsbb`#vF64mCE-G zC`2qG*MB*~eZ^?2#aMUa=L!Ra+#PfVFGFNX}3U*)FDz$2w9qkZAlH z>3AX55vfOp&Ci6pc_%~~Oml+d9cQ2M1Az!0NSbEKW>LM;4VhV9o2JfKp0EVg7;gmc zFj5*|@H!z4n6p_)Hw3y_xB@7yS|RUd^&HkuH8U92-8|{~N_P@YESl4Wa($oNK)WG+ zf|M3nQ;X1~|3W>DBD*G5d_uLHPp4*8Pj(@3F;}r>(rlc%#flmnpKBRB<@4=yi{=fT zS|0(wEZmFD@^F~Fu4!}UW-+n6#;(a3K;8rIN2MN@lS$L$G%HD_uDLlRB`z#R-mCCb zJeAFEPas311*GcKJlHa_lE^F>E6a)p1zXOPtKEtT)EX_}9*uwM9^^i!4z!zgD#T-7 zVfj2bQ(d5g5ohY3mZ?vwe0o$?BEaK|QsuIkl2g^F0|f+w1;i7`7bqTiJ<#eV4%*ab z{35u5Ltv1X4x6#<;vQL`hJDns!*41(iC*aHtY@D~H8(yoqHijw?0+2AnJGd-0z1Wu zRF5QG70yG5N^S1-_UlwG+{l{QSNzP1WAULwTw2fzL|CBI~As(@sTSMEc#Rfk8KlOrcW5uW5e{`S9M{* zQ`DjiRIK4Lk6y`x@rX7GrtxVg&M0G}kX7m&pmuJw4uYcp&A|ql0yBhmsyFVYd#Tu1{J|$UYcqI~tcbuENiL#>$&vMTT|3 zQVJ%21DF1O_su@P?KIGSl-EpOJTTAikaci?K=TdH9z$-jc&NwCwDL z@1`T~rvn<-sJA}PA#|_LJg(MWqtmG44LmQiCLB}IxDyWQ#L#BE*C_!p+;xs2dtlRI zOWdLT>U!L4>Tcp~Q7pRxDK;l$G+yQCu1DVRJ0NbVC zv(Jd=%si%vtqqCQQxARCOQOV6t1@BW#GW>UhI_MOHNP6u#K{%s=y)`-hvV}xxUAEo zldD9!F-(i2w5x2eo%moajGd^Us3F#hdd9+mIkYEnD@`#?Gfg$k28&)$%z*L3uUw^u zq3E_u6D?y?Ed!QBi!8PGUu55@eYY%{JsC=42&r1;*$=K4w>;4Sl<+Ui5y0WT#FHMm6Fuq(w9XtQ|V|O z?@1YB1yxFq{E)gl>QN&pNo-z1Px6FgMphjuBSuWdg5xF(n`*IYOYx3=**??>B*?lN^OEEbbxJ4i=Rx{S_^a3mzMmY4S(7h`6$`z~}IclAig zVX1&RMD-xBD7{k@BPX3{f-SUt;!Fdg27sEmqiSPT*)1YZgUD;K)^!+E`#)dZ%AJXd zZ^igBvR$VkVD@?CjKOk2=fUe7YStG|nB5XJ2x_28mAidIsg7iPSX`lJ!_T@f^=a_~ju|$TO!loK^@%Z}*^tNb5O*h7_gJmH{ zZ{ze8I^jg5eV{U8rr_dy96H=L45w$TI9sz!08~R5Hy3(n*Fx@)SmmZFcK916b)R5~u5F^PKYoCZu^ErRW z@AW+V*lCF_LFJ9jVDeyYi*!#7(P5?BA6SFDe0#s&P0=HMOLW7H>9 z#zEM~VW}m2m5}GO?Q0l_YZXim+eLC+KgiD)bF&ssNiNPwsBRk zMr6R}HP$c?qFlH$OYld*XNa?HjOxj0{jv{twG2DXD!yC;&d<^vke@#jjj^TnA#I-B zFo!s`HrKs1+Jzp&W?&ce72gZlWwOse^R+y_e%Zp+pE_A@n`>6Ve!ePDD{roov-@t{ z;yu=qViTP_yS&4;W4Cj;v%h@i)Sbx>!>_gFd!JXEsghdDTCSficE^=DMiWrJ&` zQ9F|{h#$Q9N%M+X4T2ER+to7Hq^Da+{LhbpyS~!F&&|j$Gl6eQp{&?KVA%pJes6AZ zS;|vDeRc3LyF9GP^L22{-(5l;xMq(`TO&56ckf}|P)U}5_A+3O=?8rNvm^eEMbsdSQKRe_>QS^biA(HbQzA zQCPDI5F@m59xi%>rqVvl%6>#@Q5MXt0rA9LMYp&x7-M{BUFu#;x3~}zbABGoTErxB zp)ZPCA_S_r*cMlWXk&HQx`}tAA9H7eBgv<3203$)kn%tE;Oo| z#AAp#iAqHmst=Y8+}0uq?VEm@L0^Mb^w2^brG#iu^9Z&Kp1!l|OS$_U=Z=34GSrVu z$97Is2fQXaqS5@}R+>9xeKloC48G zh>lN1-GBcZJMMBsom{}UYgiXBpkNj)%Y!|k*-0&8Qz?Hz?{Y}7pawoqGibzg>DAr! z)jejR(})m9a)E+G9lJ)AVXo%BmyjRE@#QyEu>D67H*dNX(E$TVzRTgdy`rf_?NQsr+wg1n=f(3D694`sV+`Z zB0yEd_adfq^%}29-HBPJt#hwI{3vOP2A)4%@5+!&WmW#kk?Lh$-Xbfguv2X)==G;> zh0L3k_JAKmLb5J)4;v9i>7}49ZSahteb6j1&C_$at-FMeq!-Jlz0YPRoA&A0k+(T#I$SPKxVRHc*7Bi1yw1WUB{h zQnx@DCH>I2widC&IFUzV2mCG>nE(DgwxzM07|8*`KWS`DY4=+Q}`OMObK+PA+h z+GL5}7q+=nLkxSh{lRQz5~Z`@Y5HiQLtkJFZm^%tol<$bFBs+^$B~>TT@@E!<)|P! zul5r25fOfWud0!iJdn?gR^gGB?hjIA_Both={W71L~7Xbut->|TBxF%LL}mNw=+4Q z?m}$MYkbAU@JkpamRW(kMCLaQ$z+lO&=$!DZMP)r$E58_kOYMLeG8qmv;ekuDu zxNC<3CP4SW+loN(|C>R9CdhnUV3)<~;X58=2L|Fh&USx({EEia;x9Ksf#%fJbJ176zR;lXaq(U7{#cbxeRDNQ{ZP!t z&Wy0lx55a5w`sUUz`Ya3YokKVgJz6cM=#0bKE)xcsOp{2+Gh^Zc^fIepO7OyUag|; zm1g7wee@@0i|XX2LyuCONuTSZz;v?RuHNKAg_80^z7%p_eU3Eru+H*}*TPVkard)x z#Q{joqexC7>o%2l>7Kql-`>sBc|TfA4Aaa5z0BXKLo~=jfA{K^|?Y@el9(Y4<)$UGCCU4ga#2|^!LU>8p4v$DOW*# zgYG}Gv{thEfq80~{WG%IG}W#epWtXs^8~?3bvjM@xd!&xfyVpVo#{hx8qM>5N^WXD zhi&fg^nPx=@9DV3X{E#!uEf_XdGfP=)i z2dv}P1=&|@dR5_0mFn$yg8ZFKz|IzO*G_Z>Z*dlnbh?hl;B^U#$-ZZZO9n?x2 zN#y1IH1zh*Cok|z3j_GILj|CoPAk2LBZ;2lp3@ z=X)2jO_C!ulsjp#x3&nE*5efaY}8K2J7@tp$mf=fY~;KCUD|hHQl5+a93In~oT$Pf z>F48uvey!;;~C}Wuv{_FH+A{dKKu46e_Ws8Ex4f>q0eu_0$iXxKh{U^kQ>(}R&m95 zS3!AVMIXQK-Mna(-FL!nP#$$w-9CBaIBj}(pRSL1oqDaD%w3|~2?;!|WsP4R=e8x3 znK&}qjTE&t2VS>vH}4caBuKbIwF*t2``fOX->ib#FduJ%+Q8p^ zVv705O|(U6d^gp6d~5Q`%Dt>9Y7#p3^iS7zipZV!SB12+hB%Bu_<3Y@)ltM2sMM$1 zu_1HM>s^$a0Xh#^uA?w&rDY*9A>NsvXem1DATY*gQI<=RrtBSz>MEaitxM?n8d$h}wUD`apMzVKBQ?m@_@W!Csc95{T099P(EU_*?h=1mETk#A z49Q)vD5?7^d;j{9*`-J~UKdIelm1(3fizRxDP(5S`M#lkB~k985)U^I>Y^ag+eTPP znXtVwT*-SYMVoMgn?!NRxUX9GGX?Qa<^lzR1y7~Mt;!kQbSTV<(+~oEMC2TtF=S}d zBnXMb5p*aOhvNXS&=q?|EB z()mZF%D7o#3b+AcMe#$q;^^G7LbgmXZD48CNg3|O!opwsi2HVEdr>Bd2+4bQCik7b zswis_qz`@47#O6nzWc~Qd!Gk-A6bNdWwS~^xBpuT?qA~~|L0_^x~znPiugZ~ zvA^N)|2Yv0sG#_FMC@;B_+KMn{}B8y{QW-|2w*mUQ+~f^|BZ(sQr@DzW_zj%8pbG2E+lI{N`l;ES35%4EVo>Ec}C$Wo7uovyoQsfDev!#_;33%$|*rX)oHuRkcsf1CgNXjec@T>#bjzfEBNYb47*u3ct&wm$eJu9J zmUViRm#R(x08L$v*qmAXV$7%C~-yyLd z85_%`wYd+OCmMegP_}vHBY3e)d<;l2TDSk;poj0Q+D?F<#^H>-tyel=<9B%Ys6nqgBcM-isA6Bc*&}_JftJF7vG2HpI*x?-vY9?dzVK+EcN?^a zDY5&%(DRE)qf5nw00Z$M;J&Vu_9$S}qheSL=Ko?xG7WP7S;_b^k&_XiZXP@?;240x zcynZ5CyI?~)lcZLkq~~lD|&}TM-XUscSdnPMIry~V<5m=5%LIzVVC$fpoP z;Oyb-MmZ0B6DeRR<_*FSC}7ZNkfJ@zEYj2dvmW7`Qt(hDlN;(MH|R&jC^I&G_w3J^ zy^miZ0*-oo0;NNlg29f{B804Y{Gv`Cl}8cHeokd9Md_6GROwEvG0DgBjKwTfF4g2{24ed2T`1F_k1o=p{uwh{X^sx{dc*pfK6cOPLGZ6A z0JFMG1SH0zVhI0*J?yh}%&p<{kBKFz#{zI}PLzOasR?XseaLGa2oQ)_FKbcwwksO$ zAnFs57_*cIHrqTmXdZU`&NB=Cm}|d78W=@L(}JE?FhPFIX=v=27$j167~_=<-k2Kh zX|-C*tT)%DxduifTN}If^^hcQ39j?^+e5W#rjpPVUV9CDuv=zFGhu7CS66bfv8fir&mXS#hka{^+Np?pKreZoR8gGpc(81bZwst8{N?DnHWtsxNi@hzSC;! zbMrCTs7fljCt6%ix>X17jk$MuUl#v> zT#p&gWV-e6JNMz~wrSmJC49E-Tb=n+{~;U2c4I?&p7%Iu5w;!K#Cr=Z5@t{jVD!)&nZixQn) zyOoYvk%MWv$V8#6XTn_RwUALqeo-2web!6E1Ki_6xYpMFvPAg_KIS0)*(!o3*uMQuWB!D)@eK)}eVO~lx<>@g0l|LzJr8Laf*@43u>kho z(x&Z(1gol43>;NV!qMCD8V5rJ*QniXLG)(T~(Ke zbjOBm9qQ#@+ANk@%2`@i56)R{^cX zB|mx6d$4@(o!Q>BRvV*lxk!*_Ct80)^z``2}?p;s>B{mozNu|9aVYQ>%OzlI%CNeDli)gy5C^4v{z9^0)~rIfrE;GjNqOQKih9^Sxf-XloyIpq>LJU-(o>Rh==o<# z`La&;cPNvH=El!S3YsBW1MwAo$yNLmhO9E!B6;OA1jy)e%xJ zPGpftf~-y)eLY*|Yp&6DA7*sJEf{vAg)`GuQC4Oz4x+TR=BP1~OAahRIt`iL!wt!Fu zT#@za1Sl2;(|N(`aHu1FK3%W9-bXa-#wfcYs3WoD$kT@@R9&r8w3K(Eo8ed;B$~N4 zqhnNv6?MVIRA6c2M3!4|g~;-q#8h{$%tve1Om$C(tko6k{L890*Ch7By=W_(PTM_~ zg3}_F{9DTfu+VmO;M5nN6lX4^i)ZJdt(n~9Z3gA>STw`fxE5G zm2)8zO}bKEu?NkDFZE+n;2H%t0uLw$0hJLu0l}^}uY>Rg@P?aAw9x`MQ3iF@m^H>R zTS=)YFTT1X`$>c_eV1f4#$UJ$YH(|ebqd{oYq*h| zg0#;D$!4IZAG6|4B}{@ z?M0ta4dZB}bmJ_mMR7S$od(Gz#zn^5bJ6oYm>2?5+WUVk;UVrCi7@aQUBlvi7Mf!a z^btUw)2HC^N_hi*Kcp1ft_PDDR%pIn!5LP4v%+#PY-M=wlDOyiF!G{4_<+p%pag}H z^8)nHz3A1t@$;F=_P@Q9#FQ-fxS!!_xpSfGNRsY~yR(w`*e%c_nWOVOmci?o(IMZ6 zy^GL&zSQMp6aHWk{-8L%_j-;Yd~PZ9ohn+?twOE2pRHIA+L^cX*f->>4G1` z$070W3bTCTm}fpeP#EUKJQPpkNwq#I zQS9hS>Q8QDKreyP466cadC)lU^N~V~yY>afVSa z4_yf{KZS3SfReOK`pKQuEWVPdNX)9Hlu$TGyOO9#j7dB%1tngd(5Mj4m%|D(Gc+{k zA>m7YY!q*~sFCjyx}ed>>Rqp%A!S8eRh>qxil#6@T+Z5_|LjpNS)d|C7OoPnN~%~? z7>=T=KwuG+k}Rd!?3AxgYGKi$Mx7bk}&uofrzeKVQZmX4k8o2^v7mqY}yx06BouOoOG?JX4OIrE-Z z;ks_ATcqO!i^LS+mhZ&j+7jQ1XWKJ{8R)_s5GlBIcGN=V!qL4=IonIos=FWyEeF7%h!8$l!(tci-4gM zh@Y_oec;s}fAjveWr;<9V0Q8Wyd)qV{dbTcpt;VUsUKQ&5<)`1(_4%I{cQe7EYbNb z{~MTv`g7pFFxr1W42*xaFp&j7Nx#vZ-?+&iX(oT*d;eX|y>m>RWS=~`s9a=|N;#}c zCA@GZvM?Thp}vmx3Y2Kcsf<;)L}*K#VveBKC!CWL(xswkTmP-Xh##%wKg3%cPL&55 zUdK4DeD$Bc!OWL_GDsxdA8l>hz2IC%vxbUf8mNq=+$gvG36y9~kwywE&~H|sh@wc_^?D1TnI7ru9=|N%N}T=eX8cvWLW>E|TnK<9;?t>X zXaedd(6Vv>_J9dcL4o0SZVEd9)%@q(`7Qf(fq0e}KCv$FoXjeh~!|4EIBfsvMpk^bM+{z9w)YJU(4|BpwQ z831`cfSykOV&h+E?tju^Wud2KV`BXGrTqn@{Ui@d`Z*61( zKkPG!MXZ!0C z;pYB*ul|W>%NqcI&OdP3KjCIa{6A&^BYz>lT6FTlq5yFdHvlXwVFQpC`p3KA@0%PT zDP(7D=b-c(H~mW)FlYqm!S%<3<##p|K0W{`|3mgSf%8vNrT{5GTdLoD(C=x0o+$&M zch{e7+Wr~=!1Vy4Aot@*)22M&&4$ekS@&*pSL2v-9|9ka+d;ws`e;yLBMq8&pW|`>!H20sF zgFlD4e?Oi`pX-Nj6$Ll2}3GITuw8!r^rY!S_K&D&gv)} z;WmS{dcTJY(1$lsd0R!rN%qNbXPQo-b=UY;H#5!xBBouc-OOJnavwJ-mvUWC6Jy7B z^LSnFQ(b&5DVy&PcWs-#Z#P}KuOnG&$5OuGVT$`F`-zT)#Ch4BFQ;Q_n=Ny$AJ03o zAJ6NLbX_k816iFIlONl>3n}3 z?C0pdUk%mhb*_Z(d?R00a>{!qh#%g6{QAVxnLT>^+~@SfQ}aIieXb^_Sg*^Mhot4* z+xNW|ZXw0+s>my}pI6!TN!902YvRP4$NQG=0s>#$Pkj}P{^zqnUS14z)`aB)+Qf7F zFRtkIXS+IZ57+Ss7HmD%>9JFapYCL|Ia9#iy{}L9PZH0NX9pcIR3keFjx}9+a)bMa zI}csA_m{eSQti&Ny>FiAL4r-qVXGJ01&@sRo*Lwd$3XW|q%aq|l>*;+@fLMD%|GgM z2v2jKquyO7`w#4%jLQg*ec$@@IzQ}6^j;S)^)Btwly4{!o%EP4_#>KL6FSZ@Fkscl zMXGsOy!o0tHy@-YH(j52b`M^jCmwk}o>mvatz`5ay;m|jZHTj_Dr(8Y9Z>8IBmSC1 zphY>D?13y4_UjuVs1zvjbtv(TGv}fuzEBGlf9H3f#sx9p7*NtM61W-udSd=gZ9=7c zibw%&TE= zaT5UChH0fCwlfsGug>?ndQF4ZQB0eaJ zMk@UwsW*eL2^q&~u!7y62j{`#o#tvgSrSA~p8HYTlD_!E8Vk%e&}N$1!G~AG&~!o_ zi+LR@gu%g=x6PigR^`zkwQFBk1a1u;p%OG8&hvI4K|IPN6yiV>|M5VI;7~M7-$EeP z^EQd1zu!I-LRFe}_|uc-$Spa7Gz~snzbv__4D@Gl{T6%y+RzR%3>Sh*aj{IU79jS!j9EVQP=%Q}Ki<*frbWV_1LIzEk%@zt#p4v9C>V7aeNmuj0n zsT&7PYWG*)4fdl&n=kBPm1tZmt|wWFTjsT8>?p5&)^^-I@{T#```8v=Wv6-C#3{bs z=j}_~Crf~~nq87-%6tnhMwIl@6{nr%dJ(2bRu((zrc8uzn#>HFQVI8gtZXOe-=vm) zC+wMXCE#DAR_Joifc3b|f12XjUtHesM84CjY7c$t9XO96D}yS+mh}199TA|5ub~_` zXc4WpQ(j!`GHxf_bh7Fk1^tzsfjCg;QXpdQ`%=T0QuWlh0;OwxaPQbmFnl1g{r=K# zf>i^@y(rY+ebiEs3`Ss0Y+7;<<79IvzxQ5jl^r+v6>9XbORmgA{AJAOFUhW->DnBxgQnsCTt zm{wR_FIkvmX!MhdKxI2!FVt6f$)1<5!>q#Ez^37ZjC-u16d={W(C*Q7*acw5XhNnA zyeUSoMD-B_Xz|Pv)842uz_}XKVc2Z8f<~{?+8-=0F*k4Ob?ot9`NY{oaAW5)^ggBS zU{dT;e6{+8x&YP~o`-Otb)g6hU6RO@WKFECb3xwYH6~JyI7HqoCKgg>J8;&Cia@lYys60pbh$qr8NgvURES~?HcL6MQ+l{YK zlv6^&U3@{Ph|aoxseZl^g$(Yne%Jrf zjnPSuCdLudf@(P5&gi928}y6tTgjHk2GckMUqNm-mD06+DD3z&E79g8OTq)^9zvV` zz$3;(_Q`F2WL)9(pjWox=_gsjGphTv9TESH1o8z5>K{0I8CKAI147KsN$Iul zOTBpaAS~hQZO&jWS7c%iak+MXOYnLGV>f_*!(nUO2vVo>MR;?Q9l*4(UF1n<0E73?ehATqeGMQyF;IG!1 z(-K~w&DD1GU4d<7+C;|uNt#~mOL~T6Irp^k4$r((S4VwW+1_eV8()Ww>Bream(Pud zMm_d6Uo4QNMSp|B0 zxfZG%AWUFjd6-56$|}7**76xzd|XiJ2)HcVkTa37eHwJF89_TB2+CeLbbtHlhqK;A z%*V7CVpoVgq9)Pw^71|R7{_`cMV#X~wpHX;OAGJW&lEug(aO!O-S&X0X95MMp;DmE z$3RJK%*8`pvuz#ETs%h=eMfKIOy5ZjH2e2i%9{7(ry;#HKM&~kv%$fv-AJU9>KqzX zq!@)y^O(d?3g)KDpwbbaSG_jr(4MA>=iD!d+~^6=Upj9qCPIGUK_+^vPtmiNXf_q- zz2DvLZ&>r0OVu|B%68*^lvqsjuGG#o3EwC=tbT30Ts_rGErxn%Q5Dn8tM02_K*O32 zTjSzf#V*d7?-feV2ttqz6TGm>VPpq(xoNP0d3tCj02-YSw=GY7Wcu-By2dqgy88Hu z)EjpegyJwYgS<<#xsvNNV4VLfs6NvKVz2Vl{ZQv>UK?+L+KT|T8kVEU%JD5h&1P`r z*R9P|Z$@yDOwLxu3My-~yHm~jf?4(0jh&ReYdXkzA0!nAg}lXj>U#rZ1>v%SbOMAN zZ+a|*#OAxCc-dXWR!T9@)p-lD_Z8G9&{}UYV#?W8W&NN&7pW^MC7@r=m5{R71^&TC z5M}<2j3h_|s)rn}O)cDkr9T9hb5hK9urKNGTvI+~wQ)g|+hfOk`Vq{{bFO2#$;=7wdnJ}A1Uc?gmlVB~ngu5i+uzLmIL@PHZDvl~uls}+XE3}u3dXB2b`Q20br)Z$w6 z6iz@Am|t7@LFlEO_GyzUmse5#(0W?V?(KT{b=>9qYs@uAw(DhAR}@kFEH3vhKjz4xBT#@>Sz_YlA%!wf zjs6iFb9nMI@@InQSK#Z@FL+)4jM5=sK=!|&G@;yXpu%!G{C`%XY;4@>C#fl=R^#X7 zD^u2mEMcQcO}z5wljNJR=^2$3o768YhQyBgYNtTzbKWDUaU3|O$f$avqdCF{g%pa7 zC#gfOXE2jyy@}!0|7+|PIC$ce_cc(*HCx!rC2|)y@?ejWdgI;{Bf?+6*h*WG103$W=!2mLf^v0 zLmWq;VzC1FaiWmoHjLkJ*VsW>8wFe(ri6-9oemAl8{DSRYbc>RS5MPhBd>a`mYW{A zM0F82-2(58Za+Bg2@7fI^;MZf3e#uUg~dy&PNOGo3Cfn>F{)XPKIWGT4fRXx%b-}N zJOSL25z~YJ8k?>dqjcKwT#fx&!TtlczV}=T{{~i$29hb+&>G{CgmNM%pS@crMFzmzyIhWSBkz82^$I{$Op2{~tqC3@bc zRdj*(G|d`m;dRC(kiZuMnJ!f6fY2v1TYpDwUSM}B<9A6jo-4JW$9B;NWlz!tK` zBJO7o{WaTep5P;B(f@<_XeYMqGX}laePYSVJcH|(1&^$PLVMXR7*i~;!ft)EvO)ro z)Ni=P-P5d0Y%J_}jyU=>DN}Y!pQ??mG&{8Gm-m?W=3@)PTjjcOC8jY=E6L*vA z?!)ziV`Gzy;_B{CbGP&NUof<4V2b4e+OfwXtF)j^K_Oc>l9%V^>^>RSsT(VcWr7YH z)eV=5>VdauVmn|SE#ONH5*nN?+V?3hyxi{~yjbf3+Nv>-S$7boG7uB1O)HQQM5%9f zTKzDrtb9`vbspB~BQYvE&tWW|QFVQ+rb({+)R)n!7GG^4x#ZE6gR#L+2&(r9jIaOu zcj=QrVF*qvh2rYeLoU`}ZHUp05!+DEs;0R8cnfX&KmvQyhrEdJUJDm63t`8}q4f_7^Z1V73%0!&A=IFvp;% z6e=}9Uno$7B)@4%&QtljW3;#BDBhoTV~dZW2VSmW1oG(f6o16h#~O_M8ipO_7J;z5IaG>^|axvkHkN zBwjb0u*b-eB;*A1>0X^2MelRw?g9T>v$6Cph;#6fc1>SfJE>8J-c%j1~-;4yseX+&%w0V1>3*lN5`6-nTShw~UWF|~Qi2t06Q12TwQ z*vOm^62yl|N-5N0fD=%k6JFUBe2s}73yi9LzkRvm162>~905cs$8l*Vf^EadUbmTa zSigOwRf7zySAU`;FHBtbxGFwkst{q?XsnnvI0WbcdYF6Yt%c8U2Mq_apFg>gtn`!i z4VUmxEq6Q*iR$#stxPn3Lk3a{q`7_Q2!gpQbb=c1rVur3Fr=y+Ek)7wEt6m*LS@*G z=&!!b9X*k~g4^09TziaL#}wQx*+ip6@F3)!iX4l_(efamz))zT?t$BO6Q#CPurj6i z-SWbr>jaP}foL0Us35CB(=Wp6u_e>JU5vumro|4`6U^fCB0t8^9n^8vKRQ)?I*VPE zPWscn$^OuhsU_OuKD6>n*Te?vC-Fcl4K9o1;r|RhHi4dbL^;xO!^Ho2ReIYX6q7A7 zzUSwsVEFpvh7w|LKNwRMEF*}P*i28mwwlRZuM<0U8Z~7%w9jC}yPMK%qv+b|P*3y& zlO5&XA8{9{QU$X?uZj#39T&&>2B&+|N1iwZ!DZBd9JM^4B*Y@%Vtb6O3_}@=)yl*x z!OMW>v_9`xv_An4A+YJ9N%|n>zObhUe4zWo+!yiG+O36%Lg~(N^0yP5#yTE~S%(~F z;V;Q!sAVd9-(8|~=hNwjvhKxFEL0}7>jF!6f#wBcKLG3KESNL98j3L=>!mwM^9i=Xui3P@(njr1a6?xp) z505lnl43WjL+>-V&RO^REe(eqGr`o!78eCCiSIvS6Z1<=d@&?SI%NuT;g5vY^1LYM z34C{1(=`fwh4*f8FCpl6R8abwR_`>4*1vbb^ks!bw$%!+$X;`?tz~Hy9NppJJU}Kf zyalsCtc^6|)tYI+Sf}cj3y1sHr*pn`96N{g>Wa}m8`!yYL_1zRrm77u<&*%JvozB7 z0Kck~>rV?gDw#s)x{hPn4PCPjkdfW*}`Sw{pp;K?=!8D zA#-SAvR;%z%KFc1S=Rudyv!gHrg*IHXbqDh5%UK41;|ktEP;frYSUMVO-P{m;pv-I zK#n0Iibc}>g%6692AAU*kHl93Uf+f*evjyW-4Nd>ri!+JKz&OGrn2kYYf7r`U{xR9 zGnJ6cIa{wQLrhc<7_eoQ6M6Q1tu!#gUqY};+4(eD%Cp*I=t!yuaFdQw63&u4+~feO6UGVt1Yc{EdA{L(1>uKqDcDZqfV91nXaGeI8Y= zBqe!Cz@!5eXzVDVoR3utZrb-b(8zH<3{E>Z6ZqB}ny|i!WpvTauPngN+CB(GY-lKz z6Ji(@Z#V?-n~l}kZKH#3ul(paKxTdQ-hi|J+mZ=vNGf4Zz^=&fd^zw%gG?O%k4Ew0 zz2aB*T8fo(X)UjPQ(q+~j~Q=YB6wPw9wl<6$ro!aGI%N+4ofW6&F2(-7s=~`rPc78 z{w_ceBXvOS^QYq{rAhuUb4rm>Qcu?)^uNnPUlQu{I= zDOIqD1^lvAiB`X1F+7FiMh(A@7dYZrA?ryb`i=Y}mnp`7u3bco64h1ch8vywRm;(v zTQGKn#M=nZ)q7KOqC+)h{dwwn3NMOa_>%mzF*EHY>RR)8>MWa$TmavMe-@muT2t`^ zC3k*Lk37;1~qfJcM$*dt}PH538_pba0?Jb4e?#WlVDrn{sH zbD`TiL$LQXts-^)8lhOGQRLENc7Ik9{R94G?>^e5Cip7##G6mCYT0KhrM^HQUd6qy z(<(iw-g*?jrd_5n`%oKFM1OT2FBqonTW0YpF%Qk~S;+?Bm+DoNh$Jx!*UKQXx3&ME zryE1fT5j-ZbFbE%%5vJs)Fh9k)6a7|zY47$eo@-t8L;y;k7#9@rWx*UVHQ*lTg_6x zdwBCeSy_8H*nzVBXi3Fg{_%~ANW5lUL8Nn zxrWCWKfUL2FYM3AgKq6Ce{ zaD#*!rf(Fxo+uF7C@ayG(p(Iku-n4JYV2D>eQ#vFNy3JUXM-TNn>LHwS%;r94~dEG z63{YHv_bAUqt?A|dRrdZr}#h3eRWt?Thliw-H52P0Z82)G!g>RA|cW(-6ahI5`rKh zN;e{@fJjTDU{E3da3A`IU=Q+oF`@Glt&v#uPf8ETURkLPh&6>UTZ&_u(-BR(_ zIeEc@Jmu>(Q@0AX7!F!_Vb1HDD9YjSiBum7AECvnrR4gtYl1INO$hlNRN3w)gxw$| zzOTa{R8L!YV*BafYlSQ!<@%P)C*NAaiofRXHEgXynnmv!p2<+Cq`iCzK;wR- zN0}!3G$&Q``q){-#BwYL>m3;8G1-i3nN{JcL&EMxF)tq5jZ_{P^p_nfs%#FA6E5cs zZ{#jhWOF#3h#VqQIY+b;d;u>fRn2)xRE|&}jEVZ>+@xD_*ZtM5DHP$IsLY|jlBr_K5*)X_!m<%hh19!-afv^(hfS@_JG}(*XH%%znkeP z@PM*EQ1?<`4mJ6Pdlp9x9W2>e_>1mjLgC$a+oJyLM)wo)xt{}9##Hi$q3^L)=0AE( z^2Sp9*@Qq;{`K!ugRAeYsE8+|CNN_T53NbW z|2q22suvn7iv3PVw4*w^*Uy$$NSiMpTTgCPAY*zL-~6mo`8O8vLFsR`ag9gAI)M*6 zo5V}R=gvf3-1I;D>3oiUc*Fg83~SGvNCcksDK3f!^y&7e3BKG6f5hAI!RwM*OqO9^M*sNMC*ci&#r6gjZ%@rO-3Qn4}*sG=4=iP_HeoCOgxw5`-27r#S@2Px)d~9uE7MmsLE)llmqMqzK5& z-tq-Ja3c=CJ5-r;?d?mKCc$LtlU%R2n&Dn!q2sAmFEmLJL(~~?D#vQ-Cr|h!ld(Q| z^a)Cf$;AQOR20N$SuH}dGOiW8x3j_*zec`1qBr*8u+$%vFv!VM%hit|tdopuU$zo>I_ODk zgJk(nt$o^BinylGS54@-=pFMVH;?cKep<~_29}r3QQyC4zy1t;#XjLID$AAsP?#;V zaQU$f#dLaQtr&`>m!)1X;$q9qc`^D=PkNj z(M_eebom@n_{z3!Ctq)c&q1ORUiN;Z+T9zh3yIAHt|XMpLnBeT_+x|#Miq}q!dHfv zKU}ce2c9wEy|6sR^I;UxyZ03koY5hm$LDpW05&%c1;M zA)tNABvbbBO(m9?+84A`0^{oIpTpxxePV9EJ57D#Kz#CiOWrxH7QGodZ@(P;z<%L@ z>~_a~Y>4ueJ)-7A4jO{Me)_7tCj%XGKD6P%iLvaolVdxrbF>Tsyc*wMYHvjCdbr&x zd4Fr$F@PfTGbg+Y;kLLtNH*2tc0cn2Xa2kADzqor$QhD2FF~YlhLh7=UXC`&?x#h(ehBqa81fv#GI?v}^Eo9Dc1fBjg zZM`|wS90e7Xi=9oW%+`NXDc07@=^l6$=!O*ZtHc{K8eV(X_!_1C@ub(7_KMWVT!yo zaZQvfobozJTlUWBVJxzrTo-s$8I(vmjp|gx53eU8;<|jcx{Y3_k{)eg#WNpD(59ms!FVkZ^J?wk>LN4WS%Of^tHqkZl+MTt z56CZ!(Q@s_t8zKjOYEFCVtM+V%BuYY!Igq<;LHmnTjIT6= zp5*Z{Xj9oYRl`%ie3Snsn)E8oh_7V9T+X2>zs}#Lv`^B0;GXKVqjgwzIBGn*`6`Dc zOTyxys_f8PIq%gy{v_Mys)0q&3Nc9;x9}K6HaEXf=C0_=tW){p2-{>AQ-Tl&A(-6^ zRl>fqlK!;+n-UIzX@3GD?}_%K&B(nO#dzzLogZ|42V}HfPXiZbsA{En>!nQzWYYHU z^E#DM_OYK~;IP+M&@>%Pdu%{_!_=Q3q{N0hKV*To+@C~w@c=LLD+|2M{&dW+lql!0 zdRqJ8Ci9(QP9)qdYQ14Zy)--{$MNg*+@TEVQQF)gqHFMacLXi|Q&tKFdzTRB!=u=H zi7t5WZBFF_8B5wTFJ(jI*U7LL^%@#1B~6^>51q*~G!RY1wWmlpqrpiQIs9iP;A zTNmyhMzFNt-GfivK4a_JZ%ZpVUYCCSl)=Io(cE&iMiRN5%alZQBkkdV2ouS%IWly!x-zTI3EC7Iy_tDx4z^rE@m&OzNx@Pja&v^6LzbC6J!8dQn(is7>_# z{N=q!>!`f5<$kUEt|64n!m{s&w>Tyg#HuH?7Zq{+R#E@vU87<= znsU0wZE?4@_q6CxCVP}g;gy$fr1?{Q!@#xHKg0t0`L(x$Us+^IGR4Q@jO0kZGv2Y4 z>_NVIM18Z9r0qS66BV>Ln6X=B0-Nqf1SgT&VbXC(g}@I`uADfgN$8MgYV0v`QFGUbvMIzI&2`i#4svdO8T5UgSSM9 z*D7G5uHp2gX?P=jo=QkbU*jD}!`5Biw>x{gL$tx)>$w!=NR5Q)DMz-o?}wdx%6VeB z^38%W3r+1E+RDEB1x(8VxA%}Cp1w0BHU^C%O<~CgdI6=G&tKAn4>L_lzdB@@5*-7buBbG^Y=O}SkIPKW#gEy5?IuouFv>#XX^B^ZXyoVejnmKC>)l=w^LGvdw zPu_FVgNj^|vNk7af^vm)*?8(-d^EvH-X3r@I?lI|sKhbKtC`=1-<5{t+-1^+B&7!G z9eXC`bC>ZB5!KRN*b_Q+ma{6JRkbR;k%X?6?Y6X4t1fw2lDR99#&>LKD_0}gT?BgX z^Amlx(W^e2d5{=D)%v;krhM+cY#AX+wBQr*6xqSvCOkYW!RLyon5x(j?G)#Xc&yMl zBFM%G(d{kGp%H%QX^EtzgE@l#g46GH{o)X2{&k0ZlAL^4t!o_ zRT^N?r`j0G{MaDZ_n@O<`-spL+l&0eDa>C74gWdO_5aOTIh=EFe>^LPbDj=3D|dVl z@c+$Oxu2(g|Ch6JzmDzwc2@51L!iG-A^vrY7>U6C-@a7Vw~J?~b~^NHG~s{9B!o(x zZ?6;JL-FRCbhu81dlf_2WweqNFTHTK(wbS#hlo^)G;J!G(j-5)-<>43^3A=D#A?$= z!t>i}_C{akhMg&UW`mc0TdAcd+_qWaZj?bdyXvBJ-)tL!TV4Yk)=Q}1~Qi5K7xtj)I0ykF=@U0pfc9ns4L@POB~;!gYf ziPlT|?-i~c8s0%S)&mE^#@JUH{0A>S6 zVu+Hsxh{HjOxjVbATsL|W<6xmj%HmkgH3mlO*1LClveyp0@p37`8|2|%vbpNJN>jg zqtkebQ(=#0r5Pl>?si17I~UOiTy|ycjI`-n5U-+kt%yL!Noeh3i5V|phtb^*4+blV zRV4fo^(lS|3HAQTlH_Xh2;rr~q60ulctKBQ`=na=%)m2ZGXH33q z)vNbMNVV!F+3OFu4V4zA$h1VJ;pxh!`f^9c+8$4&Nr-p_pNdGqmTd>8Z-?4m#Cw$U z+QvJPKwnDiC~N=oZi-3Qn<~7yi9Rk}@pf62S0yt`!qxff-d1kH|Qqoe}+VUXRXFpN9ux z;NkhBF`={a3`9q*oMgA}!uk^eO12N@{h6x1?>9Ui%Q-w7AzXaO6}Xkml{#3TBzE=n zr6wy*ooil)=ZDs9#gd*%t{|W4%j#oJ@U5=DKUn)D6$O2P@p7tsEa7uLYj@z$;eb}K zyT#3;;MezNH%p(h1)kyCwzjRnnjk|`xgsLxlw zcRT|*0bw8^p}^BqQ&Tw9Bw07cQ5XozNP;_8xAaiawgO9xtCFD$v?718#NG@B$o@LQSZ$22d-FmRbGIz7<#m8w6 z8=fTZ!6yi-b9+z4XJTGA`F^*Y%cXPga5>SEPuiZ-tq(U$U%wBZxv{68 zMk97KkTc(bQ1VtEF&yR3U;N&va1)O+EGx^?xvesO`*E3^-SvU=<>6F7#%A{@7n|7p=cgLxxurFqH@a`*O6TVtr;OK1EGeNb*o!G(fl3A|6 zybpzg#u459G0SnhEtOeC?sT<34z%=VZ%+5?&D_gUspKl7lwhxT(W8>H19xg1fhaS0 z7T2G?8E(}2l-~X>z1YM{2K0F z#GEGaXe$zjrV9ZB;9n~O&>TF0_E>~Qmb@v_1t@*|k@9_kipgzvRhziWyJ;GY*=2M)Og z=ag(eUrxDJy-vjxz)rAXRNzd!ICanI$LGo(rKb3n={I$;chAT(WlAjN+NS5-=2uSJ z6cOjETX?AY)RPYNcCc4we6ZoRhyAUI)jh)j&%2hF;y+&XKMdAU>1O8dmc0;6EIqos zFI%%wR@ag)945Maxne?C+f2w?Cb+JZK9y)U@gz_r5uxC24T1BoeJ>+K4+9x3tk_YYlD{0evMXSxXKwK zrLS-~*S3r6@{(%Hi3eU6NYu*MTr(Uwh{a~r*c%y&rCHuf_-`+_Hd6H+ZhcPsDu=js zVGq}ACTK=!xVG3@ zpCOT?R9Bwn9h2t0>kOfH+BP_(Y0Kw|9uR5?!UMTmckEp~ReeJjKe3@o?Y|StGONFm zHxG*}ofj^aQ&8Iy>7g00?nh&3__ZS3T^ASkCZ1J#otb-Ap=O^rr+4Pk5<0TP*-7~k zalTNRox{+V7ZH-X#!C(G`?gaps*PHk4Ro^io`tC3d(T{kAE3E>2kC`JBO0D)>Rz1} z=ntRmS2V18#s5%tov1S=P3@fTTL!bY{1D|t_e`N8ake*?IWg1E#QYAtFceCgS5%kQ zwk#>8tgCV;0LHmEen?Oz+vdb2fh}o{dlpjETw@kw!*?;VYen}Dx2I#)A-tX~gmy+daZ*sRBocQ5!e(&)*#BkA>zd)0Y@1t+6@t{r6V*o9WUGI6*m zDj{7cYmB~UI6zU>Qa0^#R$|8gdO)v}?6Zos{Fxk1itX|>8mbxHL7Utkt1`TEmDk@- zdWaC7l#IDuL5_dztRkFn9Xl6)eJ|wvNCV!w8ga$WspPzgE4|fcpWuJZ+h<62py4gR zt1{z+^plk7^hiH$pAm_xezAX5Cgo-4ixM4fVqU6A)^T@%;*0~Yhd{#oz?fBMRCe`* zZCA-)2t8+2Cx7``Zf~;IjDflH^&ILDmLB!7Z7)JHO-|dAO!d;9A^oAmvhwBIb(&UJ zTyFHKeBkf4?0ImyqiCu|ZXwhU(zCI#8(l!?iI)~ht(G8s#-r!K{gwK$Swz+vTMcI; zM$#Zs=4+8hDYe`x`ISStep?AOH%@6dg}lba0-_6bB5Q8?=^uXdI#)FZDLp=$`w? z-}`3pn*Mpre8$M#8kICZ5;l3tTAfY-SGFu=-DV56Lj$t_np#)I)e+BZ*-2?Z8WaY$ zEczq36VH$>lW2P=IPjtDWM;LTTBzVV9(YrbgDjDV!L&=NtkH%V)R@8zOMS!xYhqH= zyhT@HE~&QMS9BsgE_CX~aPkLanXO|z)90z$8u~}>N*med=uNUpL+oeeoW3Bkxyz>8 zP_H-n%o%w)R{dAe5ntCA3R3*nA&l?5bu}HWSc@~qU^7q~kFnXa_&$~50G@2g9c`scM+YT&guAL#7 zef8uuoWdoe!Zz$E?lvdg*Eb*WK36H9q&SBs-Ie5AKB-xFKd0Es>iJoI;gc^&oB1Y! ziFGZ@Fq+9vS2NVDtJXQRoOM_V$`5L32$9swCtw;M!#?bM=nb|K^RmjB=bYCZsgFLt zHh%?w(^Gbq>U>~__`7=Mg8M|zkGS;{3g1H{;WSzJpQQpjgIM!9?az_@C^4XR(Hp!^_DKtr9tK{3W``h1-O-ekBUOUvsfJuXA<8N!j@90JVNA`#oU&Rl-i z{Ao2#vLD2TMCzs_QncqHsggN}5O2pjm4_wCFRyif)vF=nr>2$lASNu)$?D9)7x>}z zAa+hbO!(_&&pu~CblSbsm<;~KeR7tUl~?(9XZXiyiy)SCUr21PdGUW#YZ)BEc;iKH z+7LYsWxnkEUU{U1Kiv6^2~j30!-Smdp|<3k^W_k!g`#=hHs2lcHCb-raW~yS^3#)7 zRY>;|G(>L`?>NU7=TES(R_?IQ6NKDga)ndqZC#AYZg&`Xu1!TO*YG`r_Ew7ZI=;MJ z^eo2>*J{kkS6O(m8m9Kj?0%QRSqHdhIA4ih<*+!VU`I8-(=Sb)QxiU{e&AXtOHS=@ zp7;s8XqoxpTdJG@H<{?7{E4Eo5v;?il|xSxL$$`_mwNqP?CA1RDyLbMz?GIh9k!hw z!Hkmv3KF59c<~Ul@mGEG9JJ6`p6^-PYJGhk}R{A_8UUn~K;ep*}QN`wi z02hb7NJL>Fpum|gJ zw%)t0O(x`{4`(gowZ^*NA+lTJ={&fr5bb63)PB&M_|&faPN#v$xED-gh4v!Tg1OUX z6iJ=KVyO-7^Ji2oA$3$OtjzDHXZ`#nT_EK=e391&&d5I_PO4s@I&9nia8{{i;_S`x zppqGvmV?1bccxc>>ibzb@=<7fPIhdB?p(ZDHgW1xcaV~Qu>i9^%^vb<6Jb6Pn#!WO zg2N(AXOc0B=+?`c0{zs1XRY)U85R9S2`!r;S#D|!9Oa~!<}OM`=f}icX_f2@GW!0} zICWv@yp;~o0~Zln5+<|y-k^d;enZDwjWr zk#z?m_cup1=_$gU?ZfQy3|;7TLSlc`Ape3RQRh`mK~su2zr5$^S6uEggjycPlA7WC z23MjgQMV=t=`IE7bjI|k=M*&8bj&HX0q()=k*W!o>caE#R`;gWlpL+~>vNDL-5f1y zGv!y-EwoJ^71!M)IaO=FED6t>P6@m%F(Fxjy1k4NBMXb970HQWl#D;;!*JRpEKZ$- zw3$cPAbi-^1aSg!{oRC6jVQzE;dI0~2g$G#(5Ln6caD7hxE=FvZZW%v(#wS^W0`8P z{tO=~OO$xRg33JF)T7gkY$^>1Qy5QZb;?h38rxLjH|M;040P&N&?^0THRhb)cvZ% ze7P=_tRD?^PadT`HL>iBMoNA|X>^}ih6451+f|Cr^TwxA~YG`jwT_?LLmr z?>BfVuJg?cwza!-IVZk?b|NPTVh{)O^g08c-!=Y?mx}Ofu3?8N4E2IK>d~+46xwEN9lo9SxEL)LARc{_C`z(E@@cR@ao$zdC;JFa%JHi^?`?^O;gFjrXqSDD6 zYsYW%%~X91HTAI*(&^eV{a$klZ~08U$^gS z4e5(th)*nRZhZQbtWa^=^kTUuYtlhW0e-!#Kjr3TsU@%Jz$>P*P3k)yt)g?nV_4r8 zJ1eJmFAO<3Tb{b7NKZK&dpY{y1C%tax{YA{tykZ(1=4w|t*?q`7loROTMQ(;*zl(r zIT~3K*>LL>uu<90+L?=oDoAvbN64BeY`@9evJxis9EnJ)eH?mwC0g`Rn)1pClQ?}Q zZWNE&TY5GvFLPu4HxGuG_VS4jy0Y*$a>fm2g+?GPnEr2LS_Qd&zo%TvGjf4`ciK8?x_d zNwYYh#g=H7zc*F&8yZEFa)(;9dBkTYa0ls5ILuudHSKWP;VW2df1(v^l`^&$NI846 zQG7k~+kRL(59xQOu8MAH26q}|!h`pj&EK+W?s7i4E{_nYKD_wtP2XNr&8x3M&PH%` za}Cp;=XMxZy)KhMriuo`IJc)8jHSxVgPs=q43mWyrw-x{#VFpoV>!MwYef1RD&;cO zwqCZ-vL4fC&rKE`|8YOs^*iknfwYt6seNky?z>11P)Wn5#`Z2Z>F=B zx_gc;&53oqY*D1U`KdJ5P2}-L{d`ex{1MF$EqB--Q{;btmj5e}D-FP)x;i*>@Bq1T z7gr7dHUJ?A<30ZV8Nf=FF?KcQ;E@rAL4a?&5fCU8z&1c4Zv1@wvmk&*`d@i|%O3yz zRsV0^inad)w)J5 z4r?gp&gB;?`Y zA?N`Yba1v5f?}~)AqY$e1`_}{1YErAU5z~j>|M_NRl(ozynv)Qjw>`aad2}L;{w|J z*%>p_|5WPe=4|`3N;6X-^IxE;E>P59V?~y zvDOMe5CRaWCKN6VfeRxMd=Q8*1oErxe{ufPQ}h2z$)98T#d%y35S_5fF(8ABIP7QD z{~{a@%EH0f&e&Dl7=XgHHZ^tyG(iZElIU^Y|9W&>i?Xt?g1w8YvAwCef{eI5Le5N8 z{W?lk&Jzjqx@L^RYM85dh>88I|995E3jYmN{C_C?FV?>bYXERD*2g`Qwl#Kf5qETU zZ~!{^t5-PBM1j5w1JDwG!Ssql1<|6%6u&{%}oKc2@7Lemtz{> zyHD4M8c6A7F7SC0T)95e8ge@5A7JY;P9a! z;QG)AFdqgBpppDu779DYL&2dT0mK_z8VU}o4~j;B%VLh-gyPhPJ${4wI}HXwgW7<> zp`iNE5b$`hP#CBz7KsFv#iHPV?)}~_7L5hdFvss|arm$pV5$9$28BS50nBk|(Bq5G zacD3UZhcT->BW@+6oNp2X-GKkIG_*|XuMDe0C){*7mWo>2B$9o#65_HJ-#vfcRrvI z073_c21SBo0EGc~^0<6(@Hn6dIG7KK1oaOJAOeBv1FirD(E!{S5Dj~bm-Ty}VbEi^ zA{-hFq#J++!9lWz{b4=;pd3)2VSnf|42=Md1BQWt`vTlJfZIO+TL@GZFoi$Ru%P%NdRW`3NW+xI_R{9|j9*0|9~I`Uofj3YH53z%RqC4*>_; z3<3!U$pG;OTL6XzZWjaA(_;iF+;))=IG6_g10M`*Z%7yxBo`zCEGyug1(**BmNOC! z1?e~v1NH|o^7q_Qe<&XuX62a8)3=V31({fc@Zuph@Fz~cp`2&4x9P#H+3SPTLrQ!LO3&NyHY z2m;p+0a3&;%-U~02L}0x(S<_;oCJsu3CC?020?-J9tasg^9F-}{V6~L`AHZQ*#6?S z3x$E^4X|=7?p(s42#~B`z|shk3ls(Ni7-HkaAgmJV!^V40l@%n|A5Yb`V0fFWiS{V zJYEDexNV@3puGVQ zNrCkbjRwUfFf*$#Yk}nhJRfkduY&_&EUv!5;TR0AuY&{O2BDvpx6`QVHTXkW@SYgZ3^=Yo0CtF=eG~=&wZ?4&$N+$B1_MWc_GOr3hk(;R46sGS zonH(B38rCCAis7TM&Qc%_`*z3|FBSyOfgvSI*q{s$lAF517Zu@^$o~UgJcEJK>i*B zAgkm0Q-B8Y#TXzrjBA%b_6oFz0B9il#RAiTt3$wxPu#o;kQ#>IuH8UF28HYI0U8>2 zZ3Hr}n19>3tFtk1Tc$Jluh%8lti8>DzD@w%Q~Z420YoQ%!(;z^*#SQu$ItJKgcM{r m^mzW;yC+_b|NiLb6{x`5D`(fA?=OJlG6ab@zNJ!C?tcIZ==o3p literal 0 HcmV?d00001 diff --git a/docs/paper/verify-reductions/circuitsat_satisfiability.typ b/docs/paper/verify-reductions/circuitsat_satisfiability.typ new file mode 100644 index 00000000..92963783 --- /dev/null +++ b/docs/paper/verify-reductions/circuitsat_satisfiability.typ @@ -0,0 +1,165 @@ +// Verification proof: CircuitSAT -> Satisfiability (Tseitin transformation) +// Standalone document for the verify-reduction pipeline. + +#set page(margin: 2cm) +#set text(size: 10pt) +#set heading(numbering: "1.1.") +#set math.equation(numbering: "(1)") + += CircuitSAT $arrow.r$ Satisfiability (Tseitin Transformation) + +== Problem Definitions + +*CircuitSAT.* Given a boolean circuit $C$ consisting of assignments +${o_i = f_i ("inputs")}$ where each $f_i$ is a boolean expression tree +over gates ${and, or, not, xor}$ and variables, +find a truth assignment to all variables such that every assignment $o_i = f_i$ is satisfied. + +*Satisfiability (CNF-SAT).* Given a boolean formula in conjunctive normal form +$F = C_1 and C_2 and dots and C_m$ over variables $x_1, dots, x_n$, +find a truth assignment making all clauses true. + +== Construction (Tseitin Transformation) + +Given a circuit $C$ with variable set $V$ and assignments $A_1, dots, A_k$ +where $A_j: o_j = f_j$, we construct a CNF formula $F$ as follows. + +*Step 1: Variable mapping.* +For each circuit variable $v in V$, create a SAT variable $x_v$ with a unique index +(1-indexed). Let $n_0 = |V|$. + +*Step 2: Gate decomposition.* +Walk each assignment's expression tree. For each non-leaf subexpression $g$ +(i.e., each gate), introduce a fresh SAT variable $x_g$. +Add definitional clauses enforcing $x_g equiv g(x_(a_1), x_(a_2), dots)$: + +#table( + columns: (auto, auto), + inset: 8pt, + stroke: 0.5pt, + [*Gate*], [*Definitional clauses for $v equiv "gate"(a, b)$*], + [$v = not a$], + [$( overline(v) or overline(a) ) and ( v or a )$], + [$v = a and b$], + [$( overline(v) or a ) and ( overline(v) or b ) and ( v or overline(a) or overline(b) )$], + [$v = a or b$], + [$( v or overline(a) ) and ( v or overline(b) ) and ( overline(v) or a or b )$], + [$v = a xor b$], + [$( overline(v) or overline(a) or overline(b) ) and ( overline(v) or a or b ) and ( v or overline(a) or b ) and ( v or a or overline(b) )$], +) + +For $n$-ary $and, or, xor$ with children $c_1, dots, c_k$ ($k > 2$): +build a balanced binary tree of $(k - 1)$ binary gates with fresh intermediate variables. + +*Step 3: Output equivalence.* +For each assignment $o_j = f_j$, let $r_j$ be the SAT variable for the root of $f_j$'s expression tree. +Add equivalence clauses: +$ ( overline(x_(o_j)) or r_j ) and ( x_(o_j) or overline(r_j) ) $ + +*Step 4: Constant handling.* +For a constant node `true` (resp. `false`), create a fresh variable $x_c$ and add a unit clause +$(x_c)$ (resp. $(overline(x_c))$). + +== Correctness + +=== Forward direction ($C "satisfiable" arrow.r.double F "satisfiable"$) + +Let $alpha: V arrow {0, 1}$ be a satisfying assignment for $C$. +Construct a SAT assignment $beta$ as follows: +- For each circuit variable $v$, set $beta(x_v) = alpha(v)$. +- For each auxiliary gate variable $x_g$, set $beta(x_g)$ to the value obtained + by evaluating gate $g$ under $alpha$. + +Since $alpha$ satisfies the circuit, each assignment $o_j = f_j$ holds, +so $alpha(o_j) = f_j(alpha)$. +The equivalence clauses for output $o_j$ are satisfied because +$beta(x_(o_j)) = alpha(o_j) = f_j(alpha) = beta(r_j)$. + +Each definitional clause is satisfied because $beta(x_g)$ equals the gate's +actual output under the input values. For example, for an AND gate +$v = a and b$: if $beta(v) = 1$ then $beta(a) = beta(b) = 1$, satisfying +all three clauses. If $beta(v) = 0$ then at least one of $beta(a), beta(b) = 0$, +satisfying $(v or overline(a) or overline(b))$, and the other two clauses +are satisfied by $overline(v)$ being true. + +=== Backward direction ($F "satisfiable" arrow.r.double C "satisfiable"$) + +Let $beta$ be a satisfying assignment for $F$. +The definitional clauses for each gate enforce that auxiliary variables +take the correct functional values. Specifically, for an AND gate $v = a and b$: +- Clause $( overline(v) or a )$ forces $beta(v) = 1 arrow.r.double beta(a) = 1$. +- Clause $( overline(v) or b )$ forces $beta(v) = 1 arrow.r.double beta(b) = 1$. +- Clause $( v or overline(a) or overline(b) )$ forces $beta(a) = beta(b) = 1 arrow.r.double beta(v) = 1$. + +Thus $beta(v) = beta(a) and beta(b)$. Similar reasoning applies to NOT, OR, XOR gates. + +By induction on the expression tree depth, $beta(r_j) = f_j(beta|_V)$ for each root $r_j$. +The equivalence clauses force $beta(x_(o_j)) = beta(r_j) = f_j(beta|_V)$, +so the restriction $alpha = beta|_V$ satisfies every assignment $o_j = f_j$ in $C$. + +== Solution Extraction + +Given a satisfying assignment $beta$ for $F$, extract the circuit solution: +$ alpha(v) = beta(x_v) quad "for each" v in V $ + +The first $|V|$ SAT variables (by their mapped indices) correspond directly +to circuit variables. This extraction is valid by the backward direction proof. + +== Overhead + +#table( + columns: (auto, auto), + inset: 8pt, + stroke: 0.5pt, + [*Quantity*], [*Bound*], + [SAT variables], + [$|V| + G + K$ where $G$ = number of binary gates, $K$ = number of constants], + [SAT clauses], + [$<= 4G + 2K + 2|A|$ where $|A|$ = number of assignment outputs], + [Time complexity], + [$O(|C|)$ ā€” single pass over the circuit], +) + +The reduction is linear in the size of the circuit. +Each NOT gate produces 2 clauses, each AND/OR gate produces 3 clauses, +each XOR gate produces 4 clauses, and each output equivalence produces 2 clauses. + +== YES Example + +Circuit with 5 variables ($x, y, z, c, d$): +- $c = x and y$ +- $d = c or z$ + +*Satisfying assignment:* $x = 1, y = 1, z = 0, c = 1, d = 1$. + +Verification: $c = 1 and 1 = 1$ #sym.checkmark, $d = 1 or 0 = 1$ #sym.checkmark. + +After Tseitin transformation, the CNF formula has 7 SAT variables +(5 circuit + 2 gate auxiliary) and is satisfiable. +Extracting the circuit variable values from any SAT solution recovers +a valid circuit assignment. + +== NO Example + +Circuit with 4 variables ($x, y, c, d$): +- $c = x and y$ +- $d = not(c)$ +- $c = d$ (forces $c = d$) + +This is unsatisfiable: the second assignment requires $d = not(c)$, +but the third assignment requires $c = d$. +Together they imply $c = not(c)$, which is impossible. + +After Tseitin transformation, the resulting CNF formula is also unsatisfiable, +confirming that the reduction preserves unsatisfiability. + +== Verification Summary + +The Python verification script (`verify_circuitsat_satisfiability.py`) performs: +- 14,000+ automated checks across 7 sections +- Forward check: random circuits preserve satisfiability through reduction +- Backward check: every SAT solution extracts to a valid circuit solution +- Overhead verification: variable/clause counts match predicted formulas +- Exhaustive testing for circuits with $n <= 5$ variables + +All checks pass with 0 failures. diff --git a/docs/paper/verify-reductions/test_vectors_circuitsat_satisfiability.json b/docs/paper/verify-reductions/test_vectors_circuitsat_satisfiability.json new file mode 100644 index 00000000..4d6a64bc --- /dev/null +++ b/docs/paper/verify-reductions/test_vectors_circuitsat_satisfiability.json @@ -0,0 +1,242 @@ +{ + "reduction": "CircuitSAT -> Satisfiability", + "method": "Tseitin transformation", + "yes_instance": { + "circuit": [ + { + "outputs": [ + "c" + ], + "expr": "AND(x, y)" + }, + { + "outputs": [ + "d" + ], + "expr": "OR(c, z)" + } + ], + "circuit_variables": [ + "c", + "d", + "x", + "y", + "z" + ], + "sat_num_vars": 7, + "sat_clauses": [ + [ + -6, + 3 + ], + [ + -6, + 4 + ], + [ + 6, + -3, + -4 + ], + [ + -1, + 6 + ], + [ + 1, + -6 + ], + [ + 7, + -1 + ], + [ + 7, + -5 + ], + [ + -7, + 1, + 5 + ], + [ + -2, + 7 + ], + [ + 2, + -7 + ] + ], + "var_map": { + "c": 1, + "d": 2, + "x": 3, + "y": 4, + "z": 5 + }, + "example_sat_solution": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "extracted_circuit_env": { + "c": 0, + "d": 0, + "x": 0, + "y": 0, + "z": 0 + }, + "satisfiable": true + }, + "no_instance": { + "circuit": [ + { + "outputs": [ + "c" + ], + "expr": "AND(x, y)" + }, + { + "outputs": [ + "d" + ], + "expr": "NOT(c)" + }, + { + "outputs": [ + "c" + ], + "expr": "Var(d)" + } + ], + "circuit_variables": [ + "c", + "d", + "x", + "y" + ], + "sat_num_vars": 6, + "sat_clauses": [ + [ + -5, + 3 + ], + [ + -5, + 4 + ], + [ + 5, + -3, + -4 + ], + [ + -1, + 5 + ], + [ + 1, + -5 + ], + [ + -6, + -1 + ], + [ + 6, + 1 + ], + [ + -2, + 6 + ], + [ + 2, + -6 + ], + [ + -1, + 2 + ], + [ + 1, + -2 + ] + ], + "var_map": { + "c": 1, + "d": 2, + "x": 3, + "y": 4 + }, + "satisfiable": false + }, + "xor_instance": { + "circuit": [ + { + "outputs": [ + "c" + ], + "expr": "XOR(x, y)" + } + ], + "circuit_variables": [ + "c", + "x", + "y" + ], + "sat_num_vars": 4, + "sat_clauses": [ + [ + -4, + -2, + -3 + ], + [ + -4, + 2, + 3 + ], + [ + 4, + -2, + 3 + ], + [ + 4, + 2, + -3 + ], + [ + -1, + 4 + ], + [ + 1, + -4 + ] + ], + "var_map": { + "c": 1, + "x": 2, + "y": 3 + }, + "num_sat_solutions": 4, + "satisfiable": true + }, + "overhead": { + "description": "num_vars = |circuit_vars| + |gates| + |constants|; num_clauses depends on gate types", + "formula_num_vars": "|V_circuit| + |gates_binary| + |constants|" + }, + "claims": [ + "CircuitSAT satisfiable iff produced CNF-SAT satisfiable", + "Every SAT solution extracts to a valid circuit solution", + "Every circuit solution has at least one corresponding SAT solution", + "Overhead is linear in circuit size (gates + assignments)" + ] +} \ No newline at end of file diff --git a/docs/paper/verify-reductions/verify_circuitsat_satisfiability.py b/docs/paper/verify-reductions/verify_circuitsat_satisfiability.py new file mode 100644 index 00000000..0ace2203 --- /dev/null +++ b/docs/paper/verify-reductions/verify_circuitsat_satisfiability.py @@ -0,0 +1,921 @@ +#!/usr/bin/env python3 +""" +Verification script for the CircuitSAT -> Satisfiability (Tseitin) reduction. + +7 mandatory sections: +1. Symbolic / analytic proof sketch +2. Small hand-crafted examples (YES + NO) +3. Brute-force forward check (satisfiability preservation) +4. Brute-force backward check (solution extraction) +5. Overhead formula verification +6. Exhaustive small-n check (n <= 5) +7. Summary statistics +""" + +import itertools +import json +import random +import sys +from dataclasses import dataclass, field +from typing import Optional + +from pysat.solvers import Minisat22 + +# ============================================================ +# Circuit representation +# ============================================================ + +class Expr: + """Expression tree for boolean circuits.""" + pass + +@dataclass +class Var(Expr): + name: str + def __repr__(self): return self.name + +@dataclass +class Const(Expr): + value: bool + def __repr__(self): return str(self.value) + +@dataclass +class Not(Expr): + child: Expr + def __repr__(self): return f"NOT({self.child})" + +@dataclass +class And(Expr): + children: list + def __repr__(self): return f"AND({', '.join(str(c) for c in self.children)})" + +@dataclass +class Or(Expr): + children: list + def __repr__(self): return f"OR({', '.join(str(c) for c in self.children)})" + +@dataclass +class Xor(Expr): + children: list + def __repr__(self): return f"XOR({', '.join(str(c) for c in self.children)})" + +@dataclass +class Assignment: + outputs: list # list of variable names + expr: Expr + +def eval_expr(expr, env): + """Evaluate expression given variable assignment dict.""" + if isinstance(expr, Var): + return env[expr.name] + elif isinstance(expr, Const): + return expr.value + elif isinstance(expr, Not): + return not eval_expr(expr.child, env) + elif isinstance(expr, And): + return all(eval_expr(c, env) for c in expr.children) + elif isinstance(expr, Or): + return any(eval_expr(c, env) for c in expr.children) + elif isinstance(expr, Xor): + result = False + for c in expr.children: + result ^= eval_expr(c, env) + return result + raise ValueError(f"Unknown expr type: {type(expr)}") + +def circuit_variables(assignments): + """Get sorted list of all variables in circuit.""" + vars_set = set() + def walk(expr): + if isinstance(expr, Var): + vars_set.add(expr.name) + elif isinstance(expr, Const): + pass + elif isinstance(expr, Not): + walk(expr.child) + elif isinstance(expr, (And, Or, Xor)): + for c in expr.children: + walk(c) + for a in assignments: + for o in a.outputs: + vars_set.add(o) + walk(a.expr) + return sorted(vars_set) + +def circuit_satisfying(assignments, env): + """Check if an assignment satisfies the circuit.""" + for a in assignments: + result = eval_expr(a.expr, env) + for o in a.outputs: + if env.get(o, False) != result: + return False + return True + +def brute_force_circuit(assignments): + """Return all satisfying assignments for the circuit.""" + all_vars = circuit_variables(assignments) + solutions = [] + for bits in itertools.product([False, True], repeat=len(all_vars)): + env = dict(zip(all_vars, bits)) + if circuit_satisfying(assignments, env): + solutions.append(env) + return solutions + +# ============================================================ +# SAT representation +# ============================================================ + +def eval_cnf(num_vars, clauses, assignment): + """Evaluate a CNF formula. assignment is list of bool, 0-indexed.""" + for clause in clauses: + satisfied = False + for lit in clause: + var_idx = abs(lit) - 1 + val = assignment[var_idx] + if (lit > 0 and val) or (lit < 0 and not val): + satisfied = True + break + if not satisfied: + return False + return True + +def brute_force_sat(num_vars, clauses): + """Return all satisfying assignments for CNF.""" + solutions = [] + for bits in itertools.product([False, True], repeat=num_vars): + if eval_cnf(num_vars, clauses, list(bits)): + solutions.append(list(bits)) + return solutions + +def sat_is_satisfiable(num_vars, clauses): + """Check satisfiability using pysat (fast).""" + with Minisat22() as solver: + for c in clauses: + solver.add_clause(c) + return solver.solve() + +def sat_find_one(num_vars, clauses): + """Find one satisfying assignment using pysat, or None.""" + with Minisat22() as solver: + for c in clauses: + solver.add_clause(c) + if solver.solve(): + model = solver.get_model() + # Convert to bool list (0-indexed) + assignment = [False] * num_vars + for lit in model: + if lit > 0 and lit <= num_vars: + assignment[lit - 1] = True + return assignment + return None + +def sat_enumerate_all(num_vars, clauses, limit=10000): + """Enumerate all SAT solutions using pysat with blocking clauses.""" + solutions = [] + with Minisat22() as solver: + for c in clauses: + solver.add_clause(c) + while solver.solve() and len(solutions) < limit: + model = solver.get_model() + assignment = [False] * num_vars + for lit in model: + if lit > 0 and lit <= num_vars: + assignment[lit - 1] = True + solutions.append(assignment) + # Block this solution + blocking = [-lit for lit in model if abs(lit) <= num_vars] + if not blocking: + break + solver.add_clause(blocking) + return solutions + +# ============================================================ +# Tseitin Reduction: CircuitSAT -> Satisfiability +# ============================================================ + +def reduce(assignments): + """ + Reduce CircuitSAT to Satisfiability via Tseitin transformation. + + Args: + assignments: list of Assignment objects + + Returns: + (num_vars, clauses, var_map, circuit_var_names) + - var_map: dict mapping variable name -> SAT variable index (1-indexed) + - circuit_var_names: sorted list of circuit variable names + """ + circuit_var_names = circuit_variables(assignments) + var_map = {} # name -> 1-indexed SAT variable + next_var = [1] + + def get_var(name): + if name not in var_map: + var_map[name] = next_var[0] + next_var[0] += 1 + return var_map[name] + + # Assign indices to circuit variables first + for v in circuit_var_names: + get_var(v) + + clauses = [] + + def tseitin(expr): + """ + Walk the expression tree, creating a fresh variable for each + non-leaf node, and adding definitional clauses. + Returns the SAT variable index representing this subexpression. + """ + if isinstance(expr, Var): + return get_var(expr.name) + elif isinstance(expr, Const): + # Create a fresh variable and force it to the constant value + v = next_var[0] + next_var[0] += 1 + if expr.value: + clauses.append([v]) # v must be true + else: + clauses.append([-v]) # v must be false + return v + elif isinstance(expr, Not): + a = tseitin(expr.child) + v = next_var[0] + next_var[0] += 1 + # v <=> NOT a: (not v or not a) and (v or a) + clauses.append([-v, -a]) + clauses.append([v, a]) + return v + elif isinstance(expr, And): + child_vars = [tseitin(c) for c in expr.children] + if len(child_vars) == 1: + return child_vars[0] + # Build binary tree of AND gates + result = child_vars[0] + for i in range(1, len(child_vars)): + a = result + b = child_vars[i] + v = next_var[0] + next_var[0] += 1 + # v <=> a AND b: (not v or a), (not v or b), (v or not a or not b) + clauses.append([-v, a]) + clauses.append([-v, b]) + clauses.append([v, -a, -b]) + result = v + return result + elif isinstance(expr, Or): + child_vars = [tseitin(c) for c in expr.children] + if len(child_vars) == 1: + return child_vars[0] + # Build binary tree of OR gates + result = child_vars[0] + for i in range(1, len(child_vars)): + a = result + b = child_vars[i] + v = next_var[0] + next_var[0] += 1 + # v <=> a OR b: (v or not a), (v or not b), (not v or a or b) + clauses.append([v, -a]) + clauses.append([v, -b]) + clauses.append([-v, a, b]) + result = v + return result + elif isinstance(expr, Xor): + child_vars = [tseitin(c) for c in expr.children] + if len(child_vars) == 1: + return child_vars[0] + # Build binary tree of XOR gates + result = child_vars[0] + for i in range(1, len(child_vars)): + a = result + b = child_vars[i] + v = next_var[0] + next_var[0] += 1 + # v <=> a XOR b: 4 clauses + clauses.append([-v, -a, -b]) + clauses.append([-v, a, b]) + clauses.append([v, -a, b]) + clauses.append([v, a, -b]) + result = v + return result + raise ValueError(f"Unknown expr: {type(expr)}") + + # Process each assignment + for assign in assignments: + root_var = tseitin(assign.expr) + # Each output must equal the expression result + for out_name in assign.outputs: + out_var = get_var(out_name) + # out_var <=> root_var: (not out or root) and (out or not root) + clauses.append([-out_var, root_var]) + clauses.append([out_var, -root_var]) + + num_vars = next_var[0] - 1 + return num_vars, clauses, var_map, circuit_var_names + + +def extract_circuit_solution(sat_assignment, var_map, circuit_var_names): + """ + Given a SAT solution (list of bool, 0-indexed), extract circuit variable values. + """ + env = {} + for name in circuit_var_names: + idx = var_map[name] - 1 # 0-indexed + env[name] = sat_assignment[idx] + return env + +# ============================================================ +# Random circuit generation +# ============================================================ + +def random_expr(input_vars, depth=0, max_depth=2): + """Generate a random expression tree.""" + if depth >= max_depth or (depth > 0 and random.random() < 0.4): + # Leaf: variable or constant + if random.random() < 0.9: + return Var(random.choice(input_vars)) + else: + return Const(random.choice([True, False])) + + gate = random.choice(["not", "and", "or", "xor"]) + if gate == "not": + return Not(random_expr(input_vars, depth + 1, max_depth)) + else: + n_children = random.randint(2, 3) + children = [random_expr(input_vars, depth + 1, max_depth) for _ in range(n_children)] + if gate == "and": + return And(children) + elif gate == "or": + return Or(children) + else: + return Xor(children) + +def random_circuit(num_input_vars=None, num_assignments=None): + """Generate a random circuit.""" + if num_input_vars is None: + num_input_vars = random.randint(2, 3) + if num_assignments is None: + num_assignments = random.randint(1, 2) + + input_vars = [f"x{i}" for i in range(num_input_vars)] + assignments = [] + all_vars = list(input_vars) + + for i in range(num_assignments): + out_name = f"g{i}" + expr = random_expr(all_vars, max_depth=1) + assignments.append(Assignment(outputs=[out_name], expr=expr)) + all_vars.append(out_name) + + return assignments + + +# ============================================================ +# Section 1: Symbolic / analytic proof sketch +# ============================================================ + +def section1_symbolic(): + print("=" * 60) + print("SECTION 1: Symbolic / analytic proof sketch") + print("=" * 60) + + print(""" +Tseitin Transformation (CircuitSAT -> CNF-SAT): + +Given a boolean circuit C with assignments {o_i = f_i(inputs)}, +we construct a CNF formula F as follows: + +1. For each circuit variable v, create a SAT variable x_v. +2. Walk each assignment's expression tree. For each non-leaf gate g + with fresh variable x_g: + - NOT(a): {-g,-a}, {g,a} + - AND(a,b): {-g,a}, {-g,b}, {g,-a,-b} + - OR(a,b): {g,-a}, {g,-b}, {-g,a,b} + - XOR(a,b): {-g,-a,-b}, {-g,a,b}, {g,-a,b}, {g,a,-b} +3. For each output o_i = f_i, add equivalence clauses x_{o_i} <=> x_{root_i}. +4. N-ary gates are flattened to binary with fresh intermediate variables. + +Correctness: + (=>) If C is satisfiable with assignment A, extend A to auxiliary + variables by evaluating each gate. Every definitional clause + is satisfied by construction. + (<=) If F is satisfiable with assignment B, the values of the + circuit variable subset of B satisfy C because the definitional + clauses enforce gate semantics. + +Solution extraction: Read circuit variables from the first |circuit_vars| +SAT variables (by their mapped indices). +""") + return 0 # no checks in section 1 + +# ============================================================ +# Section 2: Small hand-crafted examples (YES + NO) +# ============================================================ + +def section2_handcrafted(): + print("=" * 60) + print("SECTION 2: Hand-crafted examples") + print("=" * 60) + checks = 0 + + # YES example: c = x AND y, d = c OR z + # Satisfying: x=T, y=T, z=F => c=T, d=T + print("\nYES example: c = x AND y, d = c OR z") + yes_circuit = [ + Assignment(outputs=["c"], expr=And([Var("x"), Var("y")])), + Assignment(outputs=["d"], expr=Or([Var("c"), Var("z")])), + ] + yes_env = {"c": True, "d": True, "x": True, "y": True, "z": False} + assert circuit_satisfying(yes_circuit, yes_env), "YES example should be satisfying" + checks += 1 + + num_vars, clauses, var_map, cv = reduce(yes_circuit) + sat_sols = brute_force_sat(num_vars, clauses) + assert len(sat_sols) > 0, "YES example: SAT should be satisfiable" + checks += 1 + + # Verify extraction + for sol in sat_sols: + env = extract_circuit_solution(sol, var_map, cv) + assert circuit_satisfying(yes_circuit, env), "Extracted solution must satisfy circuit" + checks += 1 + print(f" YES example: {len(sat_sols)} SAT solutions, all extract correctly. checks={checks}") + + # NO example: c = x AND y, d = NOT(c), force c=True AND d=True (impossible) + print("\nNO example: c = x AND y, d = NOT(c), with c=d constraint") + no_circuit = [ + Assignment(outputs=["c"], expr=And([Var("x"), Var("y")])), + Assignment(outputs=["d"], expr=Not(Var("c"))), + # Force c = d (impossible since d = NOT c) + Assignment(outputs=["c"], expr=Var("d")), + ] + no_sols = brute_force_circuit(no_circuit) + assert len(no_sols) == 0, "NO example: circuit should be unsatisfiable" + checks += 1 + + num_vars_no, clauses_no, var_map_no, cv_no = reduce(no_circuit) + sat_sols_no = brute_force_sat(num_vars_no, clauses_no) + assert len(sat_sols_no) == 0, "NO example: SAT should be unsatisfiable" + checks += 1 + print(f" NO example: SAT unsatisfiable as expected. checks={checks}") + + # Another YES: XOR gate + print("\nYES example 2: c = x XOR y") + xor_circuit = [ + Assignment(outputs=["c"], expr=Xor([Var("x"), Var("y")])), + ] + circuit_sols = brute_force_circuit(xor_circuit) + num_v, cls, vm, cvn = reduce(xor_circuit) + sat_s = brute_force_sat(num_v, cls) + assert len(circuit_sols) == len(set( + tuple(extract_circuit_solution(s, vm, cvn).get(v, False) for v in cvn) + for s in sat_s + )), "XOR: same number of distinct circuit solutions" + checks += 1 + print(f" XOR example OK. checks={checks}") + + print(f"Section 2 total checks: {checks}") + return checks + +# ============================================================ +# Section 3: Brute-force forward check (satisfiability preservation) +# ============================================================ + +def section3_forward(num_trials=2500): + print("=" * 60) + print(f"SECTION 3: Forward check ({num_trials} random circuits)") + print("=" * 60) + checks = 0 + failures = 0 + + for trial in range(num_trials): + assignments = random_circuit() + circuit_sols = brute_force_circuit(assignments) + circuit_sat = len(circuit_sols) > 0 + + num_vars, clauses, var_map, cv = reduce(assignments) + sat_sat = sat_is_satisfiable(num_vars, clauses) + + if circuit_sat != sat_sat: + print(f" FAILURE at trial {trial}: circuit_sat={circuit_sat}, sat_sat={sat_sat}") + print(f" Circuit: {assignments}") + failures += 1 + checks += 1 + + print(f"Section 3: {checks} checks, {failures} failures") + assert failures == 0, f"Section 3 had {failures} failures" + return checks + +# ============================================================ +# Section 4: Brute-force backward check (solution extraction) +# ============================================================ + +def section4_backward(num_trials=2500): + print("=" * 60) + print(f"SECTION 4: Backward check / solution extraction ({num_trials} trials)") + print("=" * 60) + checks = 0 + failures = 0 + + for trial in range(num_trials): + assignments = random_circuit() + num_vars, clauses, var_map, cv = reduce(assignments) + + # Check: every SAT solution extracts to a valid circuit solution + sat_sol = sat_find_one(num_vars, clauses) + if sat_sol is not None: + env = extract_circuit_solution(sat_sol, var_map, cv) + if not circuit_satisfying(assignments, env): + print(f" FAILURE at trial {trial}: extracted solution doesn't satisfy circuit") + failures += 1 + checks += 1 + + # Also verify: every circuit solution maps to a valid SAT solution + circuit_sols = brute_force_circuit(assignments) + for csol in circuit_sols: + # Extend circuit solution to full SAT assignment by evaluating gates + full_assignment = extend_to_sat(csol, assignments, num_vars, var_map) + if not eval_cnf(num_vars, clauses, full_assignment): + print(f" FAILURE at trial {trial}: circuit solution can't extend to SAT") + failures += 1 + checks += 1 + + print(f"Section 4: {checks} checks, {failures} failures") + assert failures == 0, f"Section 4 had {failures} failures" + return checks + + +def extend_to_sat(circuit_env, assignments, num_vars, var_map): + """ + Extend a circuit variable assignment to a full SAT assignment + by evaluating each gate in the expression trees. + """ + # Start with circuit variable values + full_env = dict(circuit_env) + + # We need to evaluate each subexpression and assign auxiliary variables. + # Re-run the Tseitin transformation but this time track values. + next_var = [max(var_map.values()) + 1 if var_map else 1] + sat_assignment = [False] * num_vars + + # Set circuit variable values + for name, val in circuit_env.items(): + if name in var_map: + sat_assignment[var_map[name] - 1] = val + + # Re-walk the expression trees to assign auxiliary variables + aux_idx = [len(var_map)] # next aux variable (0-indexed position) + + def eval_and_assign(expr): + """Evaluate expr and assign its gate variable.""" + if isinstance(expr, Var): + return circuit_env.get(expr.name, False) + elif isinstance(expr, Const): + val = expr.value + idx = aux_idx[0] + aux_idx[0] += 1 + if idx < num_vars: + sat_assignment[idx] = val + return val + elif isinstance(expr, Not): + child_val = eval_and_assign(expr.child) + val = not child_val + idx = aux_idx[0] + aux_idx[0] += 1 + if idx < num_vars: + sat_assignment[idx] = val + return val + elif isinstance(expr, And): + child_vals = [eval_and_assign(c) for c in expr.children] + if len(child_vals) == 1: + return child_vals[0] + result = child_vals[0] + for i in range(1, len(child_vals)): + result = result and child_vals[i] + idx = aux_idx[0] + aux_idx[0] += 1 + if idx < num_vars: + sat_assignment[idx] = result + return result + elif isinstance(expr, Or): + child_vals = [eval_and_assign(c) for c in expr.children] + if len(child_vals) == 1: + return child_vals[0] + result = child_vals[0] + for i in range(1, len(child_vals)): + result = result or child_vals[i] + idx = aux_idx[0] + aux_idx[0] += 1 + if idx < num_vars: + sat_assignment[idx] = result + return result + elif isinstance(expr, Xor): + child_vals = [eval_and_assign(c) for c in expr.children] + if len(child_vals) == 1: + return child_vals[0] + result = child_vals[0] + for i in range(1, len(child_vals)): + result = result ^ child_vals[i] + idx = aux_idx[0] + aux_idx[0] += 1 + if idx < num_vars: + sat_assignment[idx] = result + return result + return False + + for assign in assignments: + eval_and_assign(assign.expr) + + return sat_assignment + +# ============================================================ +# Section 5: Overhead formula verification +# ============================================================ + +def count_gates(expr): + """Count the number of non-leaf nodes (gates) in an expression tree.""" + if isinstance(expr, (Var, Const)): + return 0 + elif isinstance(expr, Not): + return 1 + count_gates(expr.child) + elif isinstance(expr, (And, Or, Xor)): + child_gates = sum(count_gates(c) for c in expr.children) + # n-ary gate with k children -> (k-1) binary gates + n_binary = max(0, len(expr.children) - 1) + return n_binary + child_gates + return 0 + +def count_const_nodes(expr): + """Count constant nodes in expression tree.""" + if isinstance(expr, Const): + return 1 + elif isinstance(expr, Var): + return 0 + elif isinstance(expr, Not): + return count_const_nodes(expr.child) + elif isinstance(expr, (And, Or, Xor)): + return sum(count_const_nodes(c) for c in expr.children) + return 0 + +def section5_overhead(num_trials=1500): + print("=" * 60) + print(f"SECTION 5: Overhead formula verification ({num_trials} trials)") + print("=" * 60) + checks = 0 + failures = 0 + + for trial in range(num_trials): + assignments = random_circuit() + cv = circuit_variables(assignments) + num_circuit_vars = len(cv) + + num_vars, clauses, var_map, _ = reduce(assignments) + num_clauses = len(clauses) + + # Count total binary gates and constants across all assignments + total_gates = sum(count_gates(a.expr) for a in assignments) + total_consts = sum(count_const_nodes(a.expr) for a in assignments) + + # Expected fresh variables: one per binary gate + one per constant + expected_aux_vars = total_gates + total_consts + expected_num_vars = num_circuit_vars + expected_aux_vars + + if num_vars != expected_num_vars: + print(f" FAILURE trial {trial}: num_vars={num_vars}, expected={expected_num_vars}") + print(f" circuit_vars={num_circuit_vars}, gates={total_gates}, consts={total_consts}") + failures += 1 + checks += 1 + + # Verify num_vars >= num_circuit_vars (always) + assert num_vars >= num_circuit_vars + checks += 1 + + print(f"Section 5: {checks} checks, {failures} failures") + assert failures == 0, f"Section 5 had {failures} failures" + return checks + +# ============================================================ +# Section 6: Exhaustive small-n check (n <= 5) +# ============================================================ + +def section6_exhaustive(): + print("=" * 60) + print("SECTION 6: Exhaustive small-n check") + print("=" * 60) + checks = 0 + failures = 0 + + # Exhaustively generate circuits with 2-5 variables + gate_types = ["not", "and", "or", "xor"] + + for n_vars in range(2, 6): + input_vars = [f"x{i}" for i in range(n_vars)] + + # Generate a diverse set of circuits + for gate in gate_types: + for i in range(len(input_vars)): + for j in range(len(input_vars)): + if gate == "not": + if i != j: + continue + expr = Not(Var(input_vars[i])) + elif gate == "and": + expr = And([Var(input_vars[i]), Var(input_vars[j])]) + elif gate == "or": + expr = Or([Var(input_vars[i]), Var(input_vars[j])]) + else: # xor + expr = Xor([Var(input_vars[i]), Var(input_vars[j])]) + + out_name = "out" + circuit_assigns = [Assignment(outputs=[out_name], expr=expr)] + + # Check reduction preserves satisfiability + circuit_sols = brute_force_circuit(circuit_assigns) + num_v, cls, vm, cv = reduce(circuit_assigns) + sat_is_sat = sat_is_satisfiable(num_v, cls) + + circuit_is_sat = len(circuit_sols) > 0 + + if circuit_is_sat != sat_is_sat: + print(f" FAILURE: n={n_vars}, gate={gate}, vars=({i},{j})") + failures += 1 + checks += 1 + + # Check extraction for one SAT solution + sol = sat_find_one(num_v, cls) + if sol is not None: + env = extract_circuit_solution(sol, vm, cv) + if not circuit_satisfying(circuit_assigns, env): + print(f" FAILURE: extraction n={n_vars}, gate={gate}") + failures += 1 + checks += 1 + + # Multi-gate circuits (more trials for better coverage) + for _ in range(100): + num_assign = random.randint(1, 3) + circuit = random_circuit(num_input_vars=n_vars, num_assignments=num_assign) + circuit_sols = brute_force_circuit(circuit) + num_v, cls, vm, cv = reduce(circuit) + sat_sat = sat_is_satisfiable(num_v, cls) + + if (len(circuit_sols) > 0) != sat_sat: + failures += 1 + checks += 1 + + sol = sat_find_one(num_v, cls) + if sol is not None: + env = extract_circuit_solution(sol, vm, cv) + if not circuit_satisfying(circuit, env): + failures += 1 + checks += 1 + + print(f"Section 6: {checks} checks, {failures} failures") + assert failures == 0, f"Section 6 had {failures} failures" + return checks + +# ============================================================ +# Section 7: Summary and test vectors export +# ============================================================ + +def section7_summary(check_counts, export_path=None): + print("=" * 60) + print("SECTION 7: Summary") + print("=" * 60) + total = sum(check_counts.values()) + for section, count in check_counts.items(): + print(f" {section}: {count} checks") + print(f" TOTAL: {total} checks") + + if total < 5000: + print(f" WARNING: total checks ({total}) < 5000 minimum") + + # Export test vectors + if export_path: + export_test_vectors(export_path) + + return total + +def export_test_vectors(path): + """Export test vectors JSON for downstream use.""" + + # YES instance: c = x AND y, d = c OR z + yes_circuit = [ + Assignment(outputs=["c"], expr=And([Var("x"), Var("y")])), + Assignment(outputs=["d"], expr=Or([Var("c"), Var("z")])), + ] + yes_nv, yes_cls, yes_vm, yes_cv = reduce(yes_circuit) + + # Find one satisfying SAT solution + yes_sat_sols = brute_force_sat(yes_nv, yes_cls) + yes_sol = yes_sat_sols[0] if yes_sat_sols else None + yes_env = extract_circuit_solution(yes_sol, yes_vm, yes_cv) if yes_sol else None + + # NO instance: c = x AND y, d = NOT(c), force c = d + no_circuit = [ + Assignment(outputs=["c"], expr=And([Var("x"), Var("y")])), + Assignment(outputs=["d"], expr=Not(Var("c"))), + Assignment(outputs=["c"], expr=Var("d")), + ] + no_nv, no_cls, no_vm, no_cv = reduce(no_circuit) + + # XOR instance + xor_circuit = [ + Assignment(outputs=["c"], expr=Xor([Var("x"), Var("y")])), + ] + xor_nv, xor_cls, xor_vm, xor_cv = reduce(xor_circuit) + xor_sat_sols = brute_force_sat(xor_nv, xor_cls) + + test_vectors = { + "reduction": "CircuitSAT -> Satisfiability", + "method": "Tseitin transformation", + "yes_instance": { + "circuit": [ + {"outputs": ["c"], "expr": "AND(x, y)"}, + {"outputs": ["d"], "expr": "OR(c, z)"}, + ], + "circuit_variables": yes_cv, + "sat_num_vars": yes_nv, + "sat_clauses": yes_cls, + "var_map": yes_vm, + "example_sat_solution": [int(b) for b in yes_sol] if yes_sol else None, + "extracted_circuit_env": {k: int(v) for k, v in yes_env.items()} if yes_env else None, + "satisfiable": True, + }, + "no_instance": { + "circuit": [ + {"outputs": ["c"], "expr": "AND(x, y)"}, + {"outputs": ["d"], "expr": "NOT(c)"}, + {"outputs": ["c"], "expr": "Var(d)"}, + ], + "circuit_variables": no_cv, + "sat_num_vars": no_nv, + "sat_clauses": no_cls, + "var_map": no_vm, + "satisfiable": False, + }, + "xor_instance": { + "circuit": [ + {"outputs": ["c"], "expr": "XOR(x, y)"}, + ], + "circuit_variables": xor_cv, + "sat_num_vars": xor_nv, + "sat_clauses": xor_cls, + "var_map": xor_vm, + "num_sat_solutions": len(xor_sat_sols), + "satisfiable": True, + }, + "overhead": { + "description": "num_vars = |circuit_vars| + |gates| + |constants|; num_clauses depends on gate types", + "formula_num_vars": "|V_circuit| + |gates_binary| + |constants|", + }, + "claims": [ + "CircuitSAT satisfiable iff produced CNF-SAT satisfiable", + "Every SAT solution extracts to a valid circuit solution", + "Every circuit solution has at least one corresponding SAT solution", + "Overhead is linear in circuit size (gates + assignments)", + ], + } + + with open(path, "w") as f: + json.dump(test_vectors, f, indent=2) + print(f" Exported test vectors to {path}") + + +# ============================================================ +# Main +# ============================================================ + +def main(): + random.seed(42) + + check_counts = {} + + s1 = section1_symbolic() + check_counts["Section 1 (symbolic)"] = s1 + + s2 = section2_handcrafted() + check_counts["Section 2 (handcrafted)"] = s2 + + s3 = section3_forward(num_trials=2000) + check_counts["Section 3 (forward)"] = s3 + + s4 = section4_backward(num_trials=2000) + check_counts["Section 4 (backward)"] = s4 + + s5 = section5_overhead(num_trials=1000) + check_counts["Section 5 (overhead)"] = s5 + + s6 = section6_exhaustive() + check_counts["Section 6 (exhaustive)"] = s6 + + export_path = "docs/paper/verify-reductions/test_vectors_circuitsat_satisfiability.json" + total = section7_summary(check_counts, export_path=export_path) + + print(f"\nALL SECTIONS PASSED. Total checks: {total}") + if total < 5000: + print("WARNING: Below 5000 check minimum!") + sys.exit(1) + return 0 + +if __name__ == "__main__": + sys.exit(main())