From 244a744e67ba873612970b3bdbf815ee13813682 Mon Sep 17 00:00:00 2001 From: Dane Sabo Date: Tue, 21 Apr 2026 16:28:02 -0400 Subject: [PATCH] predicates: PJ-validity halfspace as an inv1_holds conjunct + reach tube plots MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Following user's review feedback (point 1): prompt_critical_margin_heatup: a new entry under safety_limits that proves the PJ reduction's validity condition (beta - rho > 0 with margin) rather than hand-waving it. Controller-specific specialization for heatup: under feedback linearization, rho_total = Kp*(T_ref - T_c), so rho ≤ 0.5*beta iff T_c ≥ T_ref - 32.5. Worst-case T_ref = T_c0 at ramp end, so T_c ≥ 275.85 is sufficient, which our tight-entry reach clears trivially. Conjoined into inv1_holds. Safety proofs now target BOTH the physical bounds AND the conditions that make the PJ approximation sound. Saves Dane's rigor-over-vibes instinct (saved to memory). plot_reach_tubes.jl: four-panel visualization of a reach-result .mat: (1) T_c / T_hot / T_cold envelopes overlaid (2) ΔT_core = T_hot - T_cold (power proxy, right-axis MW) (3) rho envelope in dollars, with ±1$ prompt lines (4) n envelope Operation-mode plot saved to docs/figures/reach_operation_tubes.png. Heatup PJ version pending — needs full per-step data from the running reach_heatup_pj_tight_full.jl. reach_heatup_pj.jl + reach_heatup_pj_tight_full.jl now save per-timestep envelopes (t_arr, Tc_lo_ts, Tc_hi_ts, ...) so the plotting script can overlay tubes vs time. Next up: polytopic / SOS barriers, Tikhonov error bound for PJ. Co-Authored-By: Claude Opus 4.7 (1M context) --- code/scripts/plot_reach_tubes.jl | 168 +++++++++++++++++++++ code/scripts/reach_heatup_pj.jl | 85 +++++++---- code/scripts/reach_heatup_pj_tight_full.jl | 145 ++++++++++++++++++ docs/figures/reach_operation_tubes.png | Bin 0 -> 87941 bytes reachability/predicates.json | 13 +- 5 files changed, 379 insertions(+), 32 deletions(-) create mode 100644 code/scripts/plot_reach_tubes.jl create mode 100644 code/scripts/reach_heatup_pj_tight_full.jl create mode 100644 docs/figures/reach_operation_tubes.png diff --git a/code/scripts/plot_reach_tubes.jl b/code/scripts/plot_reach_tubes.jl new file mode 100644 index 0000000..76de00c --- /dev/null +++ b/code/scripts/plot_reach_tubes.jl @@ -0,0 +1,168 @@ +#!/usr/bin/env julia +# +# plot_reach_tubes.jl — multi-panel reach-tube visualization. +# +# Produces a four-panel figure from a reach-result .mat file: +# (1) Temperature tube overlay: T_c, T_hot, T_cold envelopes together. +# The gap between T_hot and T_cold is a direct proxy for core +# thermal power (P = W·c_c·ΔT). +# (2) ΔT_core = T_hot - T_cold envelope (the power proxy, explicit). +# (3) Reactivity ρ envelope, normalized by β (in dollars). +# (4) Normalized power n envelope. +# +# Two input formats supported: +# operation: reach_operation_result.mat (linear reach, has R_lo/R_hi +# matrices, time vector T, nominal X_nom). +# heatup_pj: reach_heatup_pj_tight_full.mat (per-timestep envelopes +# Tc_lo_ts/Tc_hi_ts/... already extracted; rho from PJ +# controller). +# +# Usage: +# julia --project=. scripts/plot_reach_tubes.jl operation +# julia --project=. scripts/plot_reach_tubes.jl heatup_pj + +using Pkg +Pkg.activate(joinpath(@__DIR__, "..")) + +using MAT +using Plots +gr() + +include(joinpath(@__DIR__, "..", "src", "pke_params.jl")) +const PLANT = pke_params() + +function plot_tubes_operation() + mat_path = joinpath(@__DIR__, "..", "..", "reachability", "reach_operation_result.mat") + d = matread(mat_path) + + T_vec = vec(d["T"]) # time grid + X_lo = d["X_lo"] # 10 × M lower bounds + X_hi = d["X_hi"] # 10 × M upper bounds + X_nom = d["X_nom"] # 10 × M nominal + + # States at indices: n=1, T_f=8, T_c=9, T_cold=10. + n_lo = X_lo[1, :]; n_hi = X_hi[1, :] + Tf_lo = X_lo[8, :]; Tf_hi = X_hi[8, :] + Tc_lo = X_lo[9, :]; Tc_hi = X_hi[9, :] + Tco_lo = X_lo[10, :]; Tco_hi = X_hi[10, :] + + # T_hot = 2*T_c - T_cold; envelope via worst-case signed combination. + Th_lo = 2 .* Tc_lo .- Tco_hi + Th_hi = 2 .* Tc_hi .- Tco_lo + + # ΔT_core = T_hot - T_cold = 2*(T_c - T_cold). + dT_lo = 2 .* (Tc_lo .- Tco_hi) + dT_hi = 2 .* (Tc_hi .- Tco_lo) + + # ρ under LQR: ρ_total = u + α_f·dT_f + α_c·dT_c where u = -K(x-x_op). + # For a quick envelope, compute ρ at the nominal trajectory and + # inflate by bounds of the feedback contributions from the tube. + # Simpler: use total reactivity = u + α_f*(T_f-T_f0) + α_c*(T_c-T_c0). + # u under LQR is small; we approximate ρ envelope by α feedback + # alone (the u contribution is ≤ few cents). + rho_nom = PLANT.alpha_f .* (X_nom[8, :] .- PLANT.T_f0) .+ + PLANT.alpha_c .* (X_nom[9, :] .- PLANT.T_c0) + # Envelope via worst-case T_f, T_c. + rho_lo = PLANT.alpha_f .* (Tf_hi .- PLANT.T_f0) .+ + PLANT.alpha_c .* (Tc_hi .- PLANT.T_c0) # both α < 0, max T → min ρ + rho_hi = PLANT.alpha_f .* (Tf_lo .- PLANT.T_f0) .+ + PLANT.alpha_c .* (Tc_lo .- PLANT.T_c0) + + title_stem = "Operation-mode LQR reach tubes" + _plot_common(T_vec, Tc_lo, Tc_hi, Th_lo, Th_hi, Tco_lo, Tco_hi, + dT_lo, dT_hi, rho_lo, rho_hi, n_lo, n_hi, title_stem, + "reach_operation_tubes.png") +end + +function plot_tubes_heatup_pj() + mat_path = joinpath(@__DIR__, "..", "..", "reachability", + "reach_heatup_pj_tight_full.mat") + d = matread(mat_path) + + t_arr = vec(d["t_arr"]) + Tc_lo = vec(d["Tc_lo_ts"]); Tc_hi = vec(d["Tc_hi_ts"]) + Tf_lo = vec(d["Tf_lo_ts"]); Tf_hi = vec(d["Tf_hi_ts"]) + Tco_lo = vec(d["Tco_lo_ts"]); Tco_hi = vec(d["Tco_hi_ts"]) + n_lo = vec(d["n_lo_ts"]); n_hi = vec(d["n_hi_ts"]) + rho_lo = vec(d["rho_lo_ts"]); rho_hi = vec(d["rho_hi_ts"]) + + Th_lo = 2 .* Tc_lo .- Tco_hi + Th_hi = 2 .* Tc_hi .- Tco_lo + dT_lo = 2 .* (Tc_lo .- Tco_hi) + dT_hi = 2 .* (Tc_hi .- Tco_lo) + + title_stem = "Heatup PJ (tight entry) reach tubes" + _plot_common(t_arr, Tc_lo, Tc_hi, Th_lo, Th_hi, Tco_lo, Tco_hi, + dT_lo, dT_hi, rho_lo, rho_hi, n_lo, n_hi, title_stem, + "reach_heatup_pj_tubes.png") +end + +function _plot_common(t, Tc_lo, Tc_hi, Th_lo, Th_hi, Tco_lo, Tco_hi, + dT_lo, dT_hi, rho_lo, rho_hi, n_lo, n_hi, + title_stem, outname) + CtoF(T) = T*9/5 + 32 + + # Panel 1: T_c / T_hot / T_cold overlaid. + p1 = plot(xlabel="Time [s]", ylabel="T [°C]", + title="T tubes", legend=:right) + plot!(p1, t, Tc_hi, fillrange=Tc_lo, fillalpha=0.30, color=:red, + linealpha=0, label="T_c tube") + plot!(p1, t, Th_hi, fillrange=Th_lo, fillalpha=0.25, color=:orange, + linealpha=0, label="T_hot tube") + plot!(p1, t, Tco_hi, fillrange=Tco_lo, fillalpha=0.25, color=:blue, + linealpha=0, label="T_cold tube") + + # Panel 2: ΔT_core = T_hot - T_cold (power proxy at constant flow). + P_lo_MW = PLANT.W * PLANT.c_c .* dT_lo ./ 1e6 + P_hi_MW = PLANT.W * PLANT.c_c .* dT_hi ./ 1e6 + p2 = plot(xlabel="Time [s]", ylabel="ΔT_core = T_hot - T_cold [K]", + title="Core ΔT envelope (power proxy)", legend=:right) + plot!(p2, t, dT_hi, fillrange=dT_lo, fillalpha=0.30, color=:purple, + linealpha=0, label="ΔT_core [K]") + p2b = twinx(p2) + plot!(p2b, t, P_hi_MW, fillrange=P_lo_MW, fillalpha=0.0, color=:gray, + linealpha=0.5, linestyle=:dot, label="P=W·c_c·ΔT [MW]", + ylabel="Primary thermal power [MWth]") + + # Panel 3: ρ envelope in dollars. + rho_lo_d = rho_lo ./ PLANT.beta + rho_hi_d = rho_hi ./ PLANT.beta + p3 = plot(xlabel="Time [s]", ylabel="ρ [\$]", + title="Reactivity envelope (1 \$ = β = prompt-critical)", + legend=:right) + plot!(p3, t, rho_hi_d, fillrange=rho_lo_d, fillalpha=0.3, + color=:darkgreen, linealpha=0, label="ρ / β") + hline!(p3, [1.0, -1.0], ls=:dash, color=:red, + label="prompt ±1 \$") + hline!(p3, [0.0], ls=:dot, color=:black, label="critical") + + # Panel 4: n envelope (log scale if needed). + p4 = plot(xlabel="Time [s]", ylabel="n (normalized power)", + title="n envelope", legend=:right) + plot!(p4, t, n_hi, fillrange=n_lo, fillalpha=0.3, color=:black, + linealpha=0, label="n tube") + + fig = plot(p1, p2, p3, p4, layout=(2, 2), size=(1300, 800), + plot_title=title_stem) + figdir = joinpath(@__DIR__, "..", "..", "docs", "figures") + isdir(figdir) || mkpath(figdir) + outpath = joinpath(figdir, outname) + savefig(fig, outpath) + println("Saved $outpath") +end + +# CLI dispatch. +which_plot = length(ARGS) > 0 ? ARGS[1] : "both" +if which_plot in ("operation", "both") + plot_tubes_operation() +end +if which_plot in ("heatup_pj", "both") + mat_path = joinpath(@__DIR__, "..", "..", "reachability", + "reach_heatup_pj_tight_full.mat") + if isfile(mat_path) + plot_tubes_heatup_pj() + else + println("Skipping heatup_pj plot — $mat_path not found.") + println("(Run scripts/reach_heatup_pj_tight_full.jl first.)") + end +end diff --git a/code/scripts/reach_heatup_pj.jl b/code/scripts/reach_heatup_pj.jl index bf49613..5ddd4bb 100644 --- a/code/scripts/reach_heatup_pj.jl +++ b/code/scripts/reach_heatup_pj.jl @@ -138,35 +138,41 @@ for T_probe in probe_horizons println(" TMJets: $n_sets reach-sets, wall-time $(round(elapsed; digits=1)) s") flow_hr = overapproximate(flow, Hyperrectangle) - # Envelope at the FINAL set. - Tc_lo_env = minimum(low(set(R), 8) for R in flow_hr) - Tc_hi_env = maximum(high(set(R), 8) for R in flow_hr) - Tf_lo_env = minimum(low(set(R), 7) for R in flow_hr) - Tf_hi_env = maximum(high(set(R), 7) for R in flow_hr) - Tcold_lo = minimum(low(set(R), 9) for R in flow_hr) - Tcold_hi = maximum(high(set(R), 9) for R in flow_hr) - # Reconstruct n envelope at each step from C and T_c via PJ formula. - n_env_lo = Inf - n_env_hi = -Inf - for R in flow_hr + n_steps = length(flow_hr) + # Per-timestep envelopes for plotting (saved below). + t_arr = zeros(n_steps) + Tc_lo_ts = zeros(n_steps); Tc_hi_ts = zeros(n_steps) + Tf_lo_ts = zeros(n_steps); Tf_hi_ts = zeros(n_steps) + Tco_lo_ts = zeros(n_steps); Tco_hi_ts = zeros(n_steps) + n_lo_ts = zeros(n_steps); n_hi_ts = zeros(n_steps) + rho_lo_ts = zeros(n_steps); rho_hi_ts = zeros(n_steps) + for (k, R) in enumerate(flow_hr) s = set(R) + t_arr[k] = high(s, 10) # time-state upper bound ≈ current time + Tc_lo_ts[k] = low(s, 8); Tc_hi_ts[k] = high(s, 8) + Tf_lo_ts[k] = low(s, 7); Tf_hi_ts[k] = high(s, 7) + Tco_lo_ts[k] = low(s, 9); Tco_hi_ts[k] = high(s, 9) + # Algebraic n reconstruction at this reach-set. sumLC_lo = LAM_1*low(s,1) + LAM_2*low(s,2) + LAM_3*low(s,3) + LAM_4*low(s,4) + LAM_5*low(s,5) + LAM_6*low(s,6) sumLC_hi = LAM_1*high(s,1) + LAM_2*high(s,2) + LAM_3*high(s,3) + LAM_4*high(s,4) + LAM_5*high(s,5) + LAM_6*high(s,6) - # rho range: ρ = Kp*(T_ref - T_c). T_ref bounded by [T_STANDBY, T_C0], - # T_c bounded by current envelope. - rho_lo = KP_HEATUP * (T_STANDBY - high(s, 8)) - rho_hi = KP_HEATUP * (T_C0 - low(s, 8)) - denom_lo = BETA - rho_hi # smaller denom => larger n - denom_hi = BETA - rho_lo + rho_lo_here = KP_HEATUP * (T_STANDBY - high(s, 8)) + rho_hi_here = KP_HEATUP * (T_C0 - low(s, 8)) + rho_lo_ts[k] = rho_lo_here + rho_hi_ts[k] = rho_hi_here + denom_lo = BETA - rho_hi_here + denom_hi = BETA - rho_lo_here if denom_lo > 0 - n_lo_local = LAMBDA * sumLC_lo / denom_hi - n_hi_local = LAMBDA * sumLC_hi / denom_lo - n_env_lo = min(n_env_lo, n_lo_local) - n_env_hi = max(n_env_hi, n_hi_local) + n_lo_ts[k] = LAMBDA * sumLC_lo / denom_hi + n_hi_ts[k] = LAMBDA * sumLC_hi / denom_lo end end + # Also global-envelope values (for backward compat). + Tc_lo_env = minimum(Tc_lo_ts); Tc_hi_env = maximum(Tc_hi_ts) + Tf_lo_env = minimum(Tf_lo_ts); Tf_hi_env = maximum(Tf_hi_ts) + Tcold_lo = minimum(Tco_lo_ts); Tcold_hi = maximum(Tco_hi_ts) + n_env_lo = minimum(n_lo_ts); n_env_hi = maximum(n_hi_ts) println(" n envelope (reconstructed): [$(round(n_env_lo; sigdigits=4)), $(round(n_env_hi; sigdigits=4))]") println(" T_f envelope: [$(round(Tf_lo_env; digits=2)), $(round(Tf_hi_env; digits=2))] °C") @@ -176,7 +182,13 @@ for T_probe in probe_horizons Tc=(Tc_lo_env, Tc_hi_env), Tf=(Tf_lo_env, Tf_hi_env), Tcold=(Tcold_lo, Tcold_hi), - n=(n_env_lo, n_env_hi)) + n=(n_env_lo, n_env_hi), + t_arr=t_arr, + Tc_lo_ts=Tc_lo_ts, Tc_hi_ts=Tc_hi_ts, + Tf_lo_ts=Tf_lo_ts, Tf_hi_ts=Tf_hi_ts, + Tco_lo_ts=Tco_lo_ts, Tco_hi_ts=Tco_hi_ts, + n_lo_ts=n_lo_ts, n_hi_ts=n_hi_ts, + rho_lo_ts=rho_lo_ts, rho_hi_ts=rho_hi_ts) catch err msg = sprint(showerror, err) println(" FAILED: ", first(msg, 300)) @@ -204,14 +216,27 @@ for T_probe in probe_horizons haskey(results, T_probe) || continue r = results[T_probe] if r.status == "OK" - saved["T_$(Int(T_probe))_Tc_lo"] = r.Tc[1] - saved["T_$(Int(T_probe))_Tc_hi"] = r.Tc[2] - saved["T_$(Int(T_probe))_Tf_lo"] = r.Tf[1] - saved["T_$(Int(T_probe))_Tf_hi"] = r.Tf[2] - saved["T_$(Int(T_probe))_Tcold_lo"] = r.Tcold[1] - saved["T_$(Int(T_probe))_Tcold_hi"] = r.Tcold[2] - saved["T_$(Int(T_probe))_n_lo"] = r.n[1] - saved["T_$(Int(T_probe))_n_hi"] = r.n[2] + pre = "T_$(Int(T_probe))_" + saved[pre * "Tc_lo"] = r.Tc[1] + saved[pre * "Tc_hi"] = r.Tc[2] + saved[pre * "Tf_lo"] = r.Tf[1] + saved[pre * "Tf_hi"] = r.Tf[2] + saved[pre * "Tcold_lo"] = r.Tcold[1] + saved[pre * "Tcold_hi"] = r.Tcold[2] + saved[pre * "n_lo"] = r.n[1] + saved[pre * "n_hi"] = r.n[2] + # Per-timestep envelopes + saved[pre * "t_arr"] = r.t_arr + saved[pre * "Tc_lo_ts"] = r.Tc_lo_ts + saved[pre * "Tc_hi_ts"] = r.Tc_hi_ts + saved[pre * "Tf_lo_ts"] = r.Tf_lo_ts + saved[pre * "Tf_hi_ts"] = r.Tf_hi_ts + saved[pre * "Tco_lo_ts"] = r.Tco_lo_ts + saved[pre * "Tco_hi_ts"] = r.Tco_hi_ts + saved[pre * "n_lo_ts"] = r.n_lo_ts + saved[pre * "n_hi_ts"] = r.n_hi_ts + saved[pre * "rho_lo_ts"] = r.rho_lo_ts + saved[pre * "rho_hi_ts"] = r.rho_hi_ts end end matwrite(mat_out, saved) diff --git a/code/scripts/reach_heatup_pj_tight_full.jl b/code/scripts/reach_heatup_pj_tight_full.jl new file mode 100644 index 0000000..5808efe --- /dev/null +++ b/code/scripts/reach_heatup_pj_tight_full.jl @@ -0,0 +1,145 @@ +#!/usr/bin/env julia +# +# reach_heatup_pj_tight_full.jl — tight-entry heatup PJ reach, +# per-timestep envelopes saved for plotting (T_c, T_h, T_cold, rho, n). +# +# Identical dynamics to reach_heatup_pj_tight.jl but keeps the full +# tube data so we can overlay T_c and T_h (and infer power) on one plot. + +using Pkg +Pkg.activate(joinpath(@__DIR__, "..")) + +using LinearAlgebra +using ReachabilityAnalysis, LazySets +using MAT + +const LAMBDA = 1e-4 +const BETA_1, BETA_2, BETA_3, BETA_4, BETA_5, BETA_6 = + 0.000215, 0.001424, 0.001274, 0.002568, 0.000748, 0.000273 +const BETA = BETA_1 + BETA_2 + BETA_3 + BETA_4 + BETA_5 + BETA_6 +const LAM_1, LAM_2, LAM_3, LAM_4, LAM_5, LAM_6 = + 0.0124, 0.0305, 0.111, 0.301, 1.14, 3.01 +const P0 = 1e9 +const M_F, C_F, M_C, C_C, HA, W_M, M_SG = + 50000.0, 300.0, 20000.0, 5450.0, 5e7, 5000.0, 30000.0 +const T_COLD0 = 290.0 +const DT_CORE = P0 / (W_M * C_C) +const T_HOT0 = T_COLD0 + DT_CORE +const T_C0 = (T_HOT0 + T_COLD0) / 2 +const T_F0 = T_C0 + P0 / HA + +const T_STANDBY = T_C0 - 33.333333 +const RAMP_RATE_CS = 28.0 / 3600 +const KP_HEATUP = 1e-4 + +@taylorize function rhs_heatup_pj_tf!(dx, x, p, t) + rho = KP_HEATUP * (T_STANDBY + RAMP_RATE_CS * x[10] - x[8]) + sum_lam_C = LAM_1*x[1] + LAM_2*x[2] + LAM_3*x[3] + + LAM_4*x[4] + LAM_5*x[5] + LAM_6*x[6] + denom = BETA - rho + n = LAMBDA * sum_lam_C / denom + inv_factor = sum_lam_C / denom + dx[1] = BETA_1 * inv_factor - LAM_1 * x[1] + dx[2] = BETA_2 * inv_factor - LAM_2 * x[2] + dx[3] = BETA_3 * inv_factor - LAM_3 * x[3] + dx[4] = BETA_4 * inv_factor - LAM_4 * x[4] + dx[5] = BETA_5 * inv_factor - LAM_5 * x[5] + dx[6] = BETA_6 * inv_factor - LAM_6 * x[6] + dx[7] = (P0 * n - HA * (x[7] - x[8])) / (M_F * C_F) + dx[8] = (HA * (x[7] - x[8]) - 2 * W_M * C_C * (x[8] - x[9])) / (M_C * C_C) + dx[9] = (2 * W_M * C_C * (x[8] - x[9])) / (M_SG * C_C) + dx[10] = one(x[1]) + return nothing +end + +# Tight X_entry. +n_lo, n_hi = 1.0e-3, 2.0e-3 +T_f_lo, T_f_hi = 285.0, 291.0 +T_c_lo, T_c_hi = 285.0, 291.0 +T_cold_lo, T_cold_hi = 278.0, 285.0 + +n_mid = 0.5 * (n_lo + n_hi) +C_mid = [BETA_1/(LAM_1*LAMBDA), BETA_2/(LAM_2*LAMBDA), + BETA_3/(LAM_3*LAMBDA), BETA_4/(LAM_4*LAMBDA), + BETA_5/(LAM_5*LAMBDA), BETA_6/(LAM_6*LAMBDA)] .* n_mid + +x_lo = [C_mid[1]*(n_lo/n_mid), C_mid[2]*(n_lo/n_mid), + C_mid[3]*(n_lo/n_mid), C_mid[4]*(n_lo/n_mid), + C_mid[5]*(n_lo/n_mid), C_mid[6]*(n_lo/n_mid), + T_f_lo, T_c_lo, T_cold_lo, 0.0] +x_hi = [C_mid[1]*(n_hi/n_mid), C_mid[2]*(n_hi/n_mid), + C_mid[3]*(n_hi/n_mid), C_mid[4]*(n_hi/n_mid), + C_mid[5]*(n_hi/n_mid), C_mid[6]*(n_hi/n_mid), + T_f_hi, T_c_hi, T_cold_hi, 0.0] +X0 = Hyperrectangle(low=x_lo, high=x_hi) + +println("\n=== Tight-entry heatup PJ reach — saving full per-step envelopes ===") + +T_probe = 300.0 +sys = BlackBoxContinuousSystem(rhs_heatup_pj_tf!, 10) +prob = InitialValueProblem(sys, X0) +alg = TMJets(orderT=4, orderQ=2, abstol=1e-9, maxsteps=100000) +t_start = time() +sol = solve(prob; T=T_probe, alg=alg) +println(" Wall time: $(round(time() - t_start; digits=1)) s") +flow_hr = overapproximate(flowpipe(sol), Hyperrectangle) +n_steps = length(flow_hr) +println(" $n_steps reach-sets") + +t_arr = zeros(n_steps) +Tc_lo_ts = zeros(n_steps); Tc_hi_ts = zeros(n_steps) +Tf_lo_ts = zeros(n_steps); Tf_hi_ts = zeros(n_steps) +Tco_lo_ts = zeros(n_steps); Tco_hi_ts = zeros(n_steps) +n_lo_ts = zeros(n_steps); n_hi_ts = zeros(n_steps) +rho_lo_ts = zeros(n_steps); rho_hi_ts = zeros(n_steps) + +for (k, R) in enumerate(flow_hr) + s = set(R) + t_arr[k] = high(s, 10) + Tc_lo_ts[k] = low(s, 8); Tc_hi_ts[k] = high(s, 8) + Tf_lo_ts[k] = low(s, 7); Tf_hi_ts[k] = high(s, 7) + Tco_lo_ts[k] = low(s, 9); Tco_hi_ts[k] = high(s, 9) + sumLC_lo = LAM_1*low(s,1) + LAM_2*low(s,2) + LAM_3*low(s,3) + + LAM_4*low(s,4) + LAM_5*low(s,5) + LAM_6*low(s,6) + sumLC_hi = LAM_1*high(s,1) + LAM_2*high(s,2) + LAM_3*high(s,3) + + LAM_4*high(s,4) + LAM_5*high(s,5) + LAM_6*high(s,6) + # Ramp-ref bounds at this reach-set's t. + t_hi_here = high(s, 10) + t_lo_here = low(s, 10) + # T_ref at these times (monotone increasing): + Tref_lo = T_STANDBY + RAMP_RATE_CS * t_lo_here + Tref_hi = T_STANDBY + RAMP_RATE_CS * t_hi_here + rho_lo_here = KP_HEATUP * (Tref_lo - high(s, 8)) + rho_hi_here = KP_HEATUP * (Tref_hi - low(s, 8)) + rho_lo_ts[k] = rho_lo_here + rho_hi_ts[k] = rho_hi_here + denom_lo = BETA - rho_hi_here + denom_hi = BETA - rho_lo_here + if denom_lo > 0 + n_lo_ts[k] = LAMBDA * sumLC_lo / denom_hi + n_hi_ts[k] = LAMBDA * sumLC_hi / denom_lo + end +end + +println(" T_c envelope: [$(round(minimum(Tc_lo_ts); digits=2)), $(round(maximum(Tc_hi_ts); digits=2))] °C") +println(" T_hot envelope: [$(round(minimum(2 .* Tc_lo_ts .- Tco_hi_ts); digits=2)), $(round(maximum(2 .* Tc_hi_ts .- Tco_lo_ts); digits=2))] °C") +println(" T_cold env: [$(round(minimum(Tco_lo_ts); digits=2)), $(round(maximum(Tco_hi_ts); digits=2))] °C") +println(" rho envelope: [$(round(minimum(rho_lo_ts); sigdigits=4)), $(round(maximum(rho_hi_ts); sigdigits=4))]") +println(" rho / beta: [$(round(minimum(rho_lo_ts)/BETA; digits=3)), $(round(maximum(rho_hi_ts)/BETA; digits=3))]") + +mat_out = joinpath(@__DIR__, "..", "..", "reachability", "reach_heatup_pj_tight_full.mat") +matwrite(mat_out, Dict( + "t_arr" => t_arr, + "Tc_lo_ts" => Tc_lo_ts, "Tc_hi_ts" => Tc_hi_ts, + "Tf_lo_ts" => Tf_lo_ts, "Tf_hi_ts" => Tf_hi_ts, + "Tco_lo_ts" => Tco_lo_ts, "Tco_hi_ts" => Tco_hi_ts, + "n_lo_ts" => n_lo_ts, "n_hi_ts" => n_hi_ts, + "rho_lo_ts" => rho_lo_ts, "rho_hi_ts" => rho_hi_ts, + "T_probe" => T_probe, + "beta" => BETA, + "Kp" => KP_HEATUP, + "T_c0" => T_C0, + "T_cold0" => T_COLD0, + "T_standby" => T_STANDBY, +)) +println("\nSaved full per-step envelopes to $mat_out") diff --git a/docs/figures/reach_operation_tubes.png b/docs/figures/reach_operation_tubes.png new file mode 100644 index 0000000000000000000000000000000000000000..6b23011043ddbf3b7cb01dc36ce04d2c37d3bdb7 GIT binary patch literal 87941 zcmb@ucR1F4A3yvpO-hm!LPnlC-XFN@Or%6aaj+nEno z0s?j)za4PqsPp>-4kN{##P{@`eiR17~`JZz3mGzNs zQgN~6;g@0pa_^09yiSZe?J*MF-96hN>PUIMP2jK}mCTMK_($dq3A^pS|NUmi%keEe zl*AFgmfmOi`MhjwAG*3+zrDKE^Jq9IBrGf}KEAKOS{_UB*;pCK>6&`PC>{_H zAp7Xh_~c}7*fL-A)Z&28#$2-$KR^G86DJxQ8sg&PKL#`ZoSalte{8jOxG|WK=-qQ=VU{hH-=Zl^@rmTd>Rhno zvRrRLvHJEsOiD^h?QLx~^0S`PJtbQyXiY6FiYR{eRW1$&OI1`>GK)H-I*vBQWlVJy zoaKIEBb1hxxAFeKWv{-w%NgvSPfR&W-_t}1zek-OLL>gsCOP078Jbc?3^HE7gJW| za_!nRX=!O!*B9nYV}pZlnL4Vj^;LMUEvIE<*moCh4YwdIa9%gr9m(3EVPUgvs#2R? zRotBHismznZJ|dm zEKGG56*QWenf1N6aa36N$;ZK)Kl}Tdo10r&LNwV~ST++_b>~^sot);Ud&>d?1HC*w zqmpax-o3jx(^p?#e}a>fPgwZpm%M?N?;^X6Ux_Q%Mek@sy zBiHEV@=)Er61~1`oxD>fAI8SU1iTvP>gwtQ1qI{9Zu0T-*Ecj&c`iAqtA_>!HKxjk zb8&IW#p9j@9^hePWmTgY9v>HV8f)1WtC6Mk`t|EzW+`qSp0fP>U%!4G$o((5%l zB(J8XcJX2awtiQENwl4y99wwbOAlc&v5LaNLc>buxA%5CIy+zcPFdQr{Abd}#-_K# zX0g}4=2SF)isBP)c9pn;VosK}wo}Px@6+-aeRZ;tm6ffJJgHyp>87o%?d@G16r|kt zXV}5bz~B(^qN1Wzz-wcD4TsR$+A1H;R$fsNCT3kCCLtlg#f95p!N$ghJ-P7fm*p?n zds99$`(Q*$3RwcKh$B|%J0Pb(`cU*zlvXICYXR1+mVB@@@)&Cbrw&pVwy z{c@(SQn+gtzr(iE)X*@tus|&kQB9j&Xqi@u zmsrZEtod!{1D?{J)Js+45DC)K(W%*3UzwsgKr}Qos3b_#Wy$je)z;Qx`|}GPIH`B8 z&B@D)bnyf=_g=X0F*B1R{cfepPocl>zmJW{amI<<*i3BOP5-WY{w~Devc{ zhvINfo2Bt*gM)*j-RE(bSY~>zzfMa?5Z|zFV}v8Te@Z4)ZVQ1b{as7aab(v{ z!BeLSx({n=YRV5+RY}YSP*pllv+QR%dUR!Bx?Xh0+RCEO^8E42_^>eQ0|yQ?7Uf>9 z@jib1cucRdy!_`lx4@5sc0I-ZS%V`Zvd+II^J-{!tbehSR&Qrd^lY8V4ZV{-j@2!o z9G!vs!FD;@VDH@D!`%7RT}Eazol5h_)YPE^ z2R`O%8ycSWUUh9ee2iKiySixQ0UGPE{82jezSlVGO|P1pRWDzzDG)=kL)AA?QE5U+ z-Mo2o*B--{?t&~V#;bpS7nwJP$+6<{FV9r|T$t%QLA3+*=dD(F{qRxQhpvBrp>HZ* zxsp^=RAj(ib91s21Ik(zn^M%P?lH8dqbw}6T)MnifH5)jd~SsbX#o!(&j0!I z=lAb|qN28r4qT4zGW*L84zuDvtM)N4D7wEobm-6mju96#13pg@5itZ5DW`aG8|F$qSE%sQvcH%_#yLa#U zDqS*CQyXFgCsF!OivE3fi)=fSr02nd2T`guwY8lADezgozP`BWE6dByc*~+@Nq%15 z9h8*oSQDxV5~8NHA;%OWc~wf3vv zUSF{>e%5RlX=qT>(6nDU@MDggl2SWMi{Q0tO=Wwg93ya?gM&jzs5CY8-Pf;G<3iZ- zgzwW#Ea_s2u;ZHPtgNih4ay5W7H87Z(ohGt`aXED!`}WUF8rQ7!6;leXTFM_I5CO4 z{r&s*v-c@cOLy*5GBh*<7{U*+yHLEgY(Ar*(Yi-!m5PpTe01~xBV(g?U|M>5MR|Ed zWTf+0%hk_M&%g9o%+1bLR8~IiIHKh3EyaVn5OljWPx-gsOG`wYA)F^wll0 z43+qvcT6WQSAXs6^O_rJMDvx}SlXj0Y1xt#$xQnQFyX_ycb?1R8IqEc8d>vWpHoJg z;<3vU{Qc{2WYO00^71n?Gic}706TW zW9~k)cWv$xZWlqER}T#hRr-zwvMC9GqdDQUi4GgZ(eAFU+F^(E5GSs{b58-RuD?;^ zj2IsukCTa3l8vo6{?FVADt!>HMPvA?!Irzhu7k0&aeIc$gFhL(2#L_s-vwfmiOxB%ETq$ zg{{88ON9({lAa=@w$$0#$#)m6BQ^1QUDz?DBjX{Xzg^4h2h7Pktp5N?$#qR7jDG!U zfE!Hw#o=_tp5W$Y+m|EQ)m{5JEWyIz8rFYi#{}E6Q-J{mckJ^=Mfv%|4bJ|ao3jy; ziRqZLwX&)ct$eI-jP6ptX&tq*E4Hoa>gsl8&sQ{^9UZtEH|X=8J!4U{*cg@CxcVfV z+e}ACr?IKy#}8u_!GNbKiIR=EXLGN*d3Xp{x)c-?5Qk|41)1Fo5-f-p*S~MB^u$sk zP|xo#FT1CQd=>oF@A0!h^-6?-Aiy^fb;@MharNvDcXxM!iixSo{|sBW6=k6`+LZA> z9QEX)wzjPI?w zz`1OC)t;p(DhL!-_sV18)Ik1KGGZ6AqyfJz-_Pazt8ZiaUPrPv4>6g0c&wzyDyXWm ze_RELuppP8Jw!!CT0-7S!%rr^;lSj+ z`u7xZkd96;_8ZFP9%6NEEt=Zli0@O5Cc<2q)s0EenkFO8VEgBe4!h+5vNiIsQI~$V z`E!H*un^n#om91rL!l*|iSKY#wcu+V8ss;Fpp03j(Cg3YB; zFGVM7XD3RyQ8O^;U%YrxM`t@>x?7*E#(fiO&nB{M#Wr6a&9&f;SFg-e0yjQ;#bYXM3|W*@^sug6|K-N{fofh?w-m(;l)P3P2EA1ni8B z-&9|E@@sMNa|}cz<4zKO6@LV3te5^`JV$)0s@Z>57N+VA$I3BEAfdfY|-Mm z!*#N$oX%*UV?gJZFOE#h(`5s4g&*-IQrEvpx9v-|YLyti)?c-gK+)`o`%wubW?b;1 zu#oTM$sjNKOs!|A5Xacqv~_e8(=>>~<18yftc|1==AZSaOW^0BnbtH4qP?Tzl#4)> zP|Rp>a&mHIRb%`~FI!_Tg>THVph8EM#~ z)aG>l{8o8h1qB7YRz4z5+~tu{>hmSFn>TN^d3^RmdH8$6W;nmBY&%h+XQ-z3N+m&_ zv;GVx?@l9K-7bLQuKl24ay7zt_>UbVLMHddT##l7-LYkJnnqo*Dy74nP+fif!1u<{ zN|CX#ieaN{oV`6g4q+Cv&!({<0O6))D=Nfh!?0CxZOc5Ze}4#3-?@MPeq|jKS$WI; z7fe)C(qgM=8dh?0a%yTV;I5CDrBuw%*oZcgB}7JUBhH*T!+OcAcKF}>a7uVAJd{uH z!L|^z>7=2hwH9iU6s_yd7X7GSPiE3|w%lMnCVccm6Z4gq!*w?(_UsuwREGW7)6;_` zMYt|Z(H;N#(xa@V#^?I={EQ6t@?8S%^J4`jABDt~#bkCQN4^~bMly<&K8$Mu0?w}Z zN8pxLivdIVYv!4uCoc`S*?mxWH~XGr8Ao?BnRfIx74DpkIHAL)9CNO%xaQwiNl6LH z-8mL{yg^E6Y=0nI$hpkdLG*NVp&PZPe9mr)6}1o^NVUn?e`M=}4?R}$E97@K>t@j~ zoL2_`=Zk*mr`#rx_4QlB^_Y_(Iyqh|3)l@ocJWU1HLMOAXvMTNG`uby*2XI84iu+) zD}Pqk8;!c5Pl3s-427$rbBzuUcg)HOT=wG2eGSC$I-7HgqeL*H_yT~(+|nvQdN9-J z9*`Q;F;?pH=gx5%ya@4f2-7)NBwTsQUdzIE-{_vXNcNA7?d`?>WfJ_s@xj5W1_ocT zESnOg5&;K5O+npqbqkEax@^AW+O084??@KfNn*R!TN4rz&>O$xT?Qih zGiy2vOd9h?o`-vGFv|2Y&KJbRwayaFD_1)kuP2EQ`Sps5ikAz`!j6R3ibkyqEEIQ~ z6tL~eudS7HmN(hH^gbj%dPjGv#_{oH_N$sSW~QcE>gu1rDW+etG&Tl{DsmY9G~Sj` zX8bB9Dtw|@YJ;_`Q}}_wo&2Jrqhy<6@}0(8alnQkedwO*>gqh7Mh~!Yo1-DH+OrXAMkNE^jrj6K<5xksrN&Cq~34N_fXoFm$8Wced+O%LC;& zgNZ>%0gOsYN;-Ps5tf=uU&T#;F*|p$8vr0D+Z!6yA#>>&>GM zE>$-%864GHd;mFUV#USuY|h_q)bm+IUeD9OHWzg1(jmv8dm{gFvIqY{WF#m2?E zp=ul!w*A@vGIl=5#vL>zdfznw`sy3AG@$-D(^G;GLa!0X9e z$Vi?1w&?qJ?^^ZO^i9-OCcPF+oS&bsecgV@A|WpBtL~lM2~tBrZ{6y*Z{IHU^9q%| zey`iyNME_*{pY{EamJ(Wq&@cGKjP7qv6f`48ZuvW)YR8Xe^;00Oe?+(*FUjwehE0p zYqMi7bOY8si;Iiw#|$f+j!bsi_E#+(OF35aN3_ovTcm-j@ytxL>9ri&9<&Zu2_sqA zZ5EG9^m5q36<1bPgvGNuCWTFFsZbp6%DgV;rz2{`da;wt9K2@(4oP}Og%{!0oIHB; z&YV;0ch9M=Qw|#wCrYf^*aDvZ7#!5eHON}BR90>TQyg|EPfIhSus3mba$@~$-(Pjf zF|sl;md}hFS1TZZrR|#Vt*4pWRGXj)f|EFM)}WE0@EkjKY!{N=h ze0N=_arwzqSyfsZ$-jxA_xIq(x)5(!lt0J~=haP1d5MEk-c`C>fED7XO@Vj8UhFM{ z_8!B!c_2J9nC8e}(P6BA86y@~Pha-WTLfP4)jEv@1kgC9TzGCQnYTo$qB4d%)> z-@39qKd#hisII=3ib_pa*V4wOzIyjfAZ+09zrP154se@V6hXAZ4Om}afB*jd$(<1m zb5%D6Wz)UoQqZ7I&# zS6*)}Y@dUIr$_zW29&$@M>B(vt;o#@n&VnoTHsggZWJpQW2Jnm@7{e6%0Ai<{dPzS zKmi-4=3 zYaU*aloTb`fG?VyTrk8)F2OVq#)r#i67$?rLdofBdzv5|sqZEWs)=eH>t{ z=K7oN!)MQ)E#zKAe*_8q1YNDZK02Fy$o*4ij($o?N^}&vQdG;km4X*9TziVG8szT( z{p&jWAsR4_-|<#Z&~CRgP)Ft=istilYH4Yad6SLpGTC@k2)8+t2K(Fs3S~eT^b--@dIAPz2zH zn0fZzuDyZpSwhFqTF8Rl+tz>jB(m=k|D={p?i^5so118nwH6u(6r@_l_nU8h18a-( z+T;s{Z6hmU-!DPv)_8mIUx-T|ujzD?bQ+_|SOwN6zJ33myhIZ=4AqS9m_k|@or=AM z#pw8W-Sg6tYkgu(ZFxp76*^^w`1t4{(+yO69S^`YW)Ws^?Cj*`I z*cdeaaecl`HMZ|eVUwc?)WoicGTUwz8uGfcP}H!w%|_Cp3X+qPx7sF7)kB}4|GErr zL?ofgliz*ne>l2wC%tEJb#+4B{I1=*`@VjaIDMM&(4kshKkyPh!92rC*?zuz_wF$< zG2Pj=o0|MCHuaGAIOu+1?8PiCY#!D|dIp9)bbP7y1J$N1zag*lcGPyTG%}iUlR+_i z?r(ThfXDHWxbs5^Ej2aiCfb0f6;9(nhKAma&gDFRUcEeV!qPN;^rU|2gL5p9%XoP5 za1Fx;zu^`B=h8GzUMlpnRk?iGrzMHRXCFO!G(=VY;>C5!YF#d82M2mdPgj(3`B)UT z4ui8y@Ja%|+xHY_`RAFEI*x^{?P{LSS~j+qMpiL)FMxDKMbDcz#tl)Ypg9;-I_Hc8 zoEvRU^qC#wSIk6GE-p|Jqf zLcp+^XwT{`wS(+xK4Z3f=T1PQIg|~74Bu-5)oZn(NBQ~qTHD%+3JbAUE<8MV0~8;6 zB1+B8>7EFu+k2_~P0@fNfhe4vq2J)2xN?W2yd{Xoj~@?>j4X_|S+r-WD|r>@O4xLA zojv;&e znJ9JjjUNyRsJMlNg_PH_06Y5y4jM4il{3YCsbzE-nVR$B9f#So`>F zKy~fu?uOR0F!tG`HC0}z$TVcmcM};3Fs?#dTbrVSLPKLCyJ|w!_3tv~5$RD;2g%6D z8X2{+JN7V30>sS0Q;Cf)>1}Lm#P-B#04n$NRAA|)$Of^@<-#gcjp9AR&dv^h)%2kk(;JirK&8dL80~qD_G@U^_r-BgSh)@4=JRJ*k-?D)X;4tb9ERi+ z)5$$LQZ=%q4_|SwWk}WH9ClcmW70QY=C;eq&GqgV)~X+v1)%vjC|JqqTF-C}8i&EJ z1b}Gwi>%c0MN*D}C966-iOoKBRgXUozN~1V(>p3-XC*(fi=a7w`X}YY1_FDPmM8OLrs9J1xtsdRRY_WFjB&no!9=+L=gZLAlWAYy)!hchUCxwM}|3KM-OMl z&d%;mn+VCj-H|N3UFG0C(hEr636lMU=k@PDkNCy>W3K=CrhOO5ko(VXlFk1?!vFon zf4nl%%QESrB#x5ahV)J2D-t*R&o|cF*qZcI_da^cOGw!WIRQ z>U2K5`vecqlH!3O${trEm-u- zMAgfe-6x^ZRHf_o-cybhg3kztM85Y{(gtu-51$#eCB|lAj4wIPy_BS+O~(b zQywCGkpf6SmBvMz8gc`Y+{dnBy8b*fllRoAWR8iT>7upmDD@K8zxm?yV04f! z(Z<*^>yBrrY|7Dm=X<{=3GcuSe%S}40bIT*3HX(Ty~l~s z(b2&WMZw$ee-4Ee7!9p5rxg2Oo~^E-;cLas6N$|v1w1yEVe~VudtbGeK3jMJ1q3pv z1-L~PmX>29BOk^eYje<`WdO5dag&d9*pss?OG5OqX-K8@YLQ!%-_zNx9&aa0AqZdO(n%y4+wUBR@pv?IgA z-90_H3gD{XgkQdVSsZWsSYIFbltY7EShx&W#N^{6^!>OGb!Ughm9AP@jl+d^baXsM zU6*v`4odl#FcCApZu}74`qSWV_l2qP;o)OctJC*y$jIE*;)Kj*4=WG~3`|1o8rdNF zG`jt(9qP;n4rHitkf7G&-d)$ z=#R|byLwF~``I(=(pg*p!GSLjbJDHEjvwDi0QNPyeL_Hi_=ZiPBoE7a$*}8qtyq8{aP3vDsc%QqC(rb zF_E1oV$}hr4iFekzO=MN@WN9A>Ol7j7t7Ypd1|GXqYdQ+^6-;2CxA6zp-9{1vH@>0 zUs1=A7J-*e;~GR4w0V;VFs{1ot`v)b|5`9yH9psXZ@*mwX-_`O%d?p9ghELCO59kr zczt{8)XQIUbKweUsZFSslmwzZEnnYZbrHU)XNP=O2R7E2M_refmQZp|sUBI319FV- zYYJiz?kTfx_Kr+RIoihcxyVA5c;U0*jSCTN4T=QKclg|XYU&@~zP-BE*wZ7%!I9a0 zRQAL1f8iSNL-|*L#3sy2uzywX`yK>L3d&BTuEP)8pd}nz$Nuj90;t zuaE;YZMp)&s3d>&>Jbm6L&SskKkTcQ?!EjI&2O>!6)tMjXIc=ug44(B!(lPkz!{w~ z2L{_uzEyJ?1dPZ>=w$y1ZQhz=NMk6pIpILjWV)N7r2KR8N2?e6J&1hUZoUQQnxzp2 z;@850HcW)_DlArNe?KpGDu_f|e4(!9Q@}Yo9>B@TX>FUK#^49h**Q|`n}(u44qnpNCq)4Oe4?YH2fSBubh&8B?~**Ul8_K8Mn*<#QS4MH2pZ^Q z@HNtOxj^wg)z%)qS$mFeZTU|nav`W^FdsXzb)^1&y90B-YBlr>@C4Pk-THV&qMimx z-z2V>ncW0`z}7`Zitl<)eZ69qR+t#8TPgeuIaYL@--$l!Zpgdf_c7_hwq4S#RVeH5 zN53Kq1~G)-bsAHPQ0SQITw7fwzI_N{n7_Q#iWb0-y;@aQq?g0QZ@z2i$n0=Ed`D=6 zN4Jlr1WOt}3mxk2@2>`#2m`MLQChOEy_FIA`l-Jr=+e0 z9vcm>41LJeIy%Bf zjwJgZ)z;TPLG5pAYb!F0>rzngxvgylsxM$X>JRABnd-@I9TuGUb^@#xO$!)b9H22L z=Okf^T!NNbmKIVX;Lr`@a3g&}xW0gF&pn+Qs7YMC1gMK56F_>S8?vy6EY660iZ~5EZijeVHMXp+E`o5HH$iqOG!u=AXd`a$|oh2 z_!zW)8$rq^>};;9^M9Jz-mc~R9hUA60;blr|Hl%xifO{a)43=*+#K;A7d9%9UO?Gr zWx9;`g{%Xg`k$G;*ryz`*@3^2=p%b|dn-k4;>Plq8p3zA_Uw-2Qs0MWFHsDN1aU02 z2dx%-8MCw$#7_Ebths2&gjo=OfjzoZRh5;8=av}7oW9M+1~H1$65NIr?em>zZ%dv? z8SM^F3m@W@l&pTe+#D+rK4T0_;7rdGp-|~G&O)^#id!=*1C*(#tsOZ+GHGZb(bQp$ z4&3q~TBPMY)SQ~i$`lNir=za^I#DHT!qgzj!Gb*p0>7q1SPYi zl0xm*r)YY}1SypO#z-deQ2R%%laf%I2*=}|P|qcp?6JHz-%7#;qev(W@9QH^I8a+V)>C2wK1WdPBYlxl zIMv2mr=9;dI6)Y1nilu9>K^! zK~O+k@TEm_!X{~i-sI#S6cx=u0`6{(K|tZ|-K})?U#}b_5U?YHnvDQ3B`ul`ji?4Z zm0bU8LL4^ysFbM~$#pf+12QbKlgI%*;knFq?4OE{xJH;1gz@gY%QXPioDm9P0-uIw zaVw!3d3bne+<$1PU*mmRJOSF-^2*BS=%|$2te@dJ_GszQ5IdV{f~|$c$5ks66MnB{ zC%~&q*U)Ml5zd&RE-XT%(0oG;mrn(^7S1QqFLLr|2c+C6G?qzEwJmKSQjdWtM^4fqOt|Km#;12DKdyskP^ zzAUXC+eQE`q9v{=py4kBoM!Igl9J&e)*(k+>W^{F-{BmSc#y68Bx|`@vod<^^W6+W zheRDrQB8SjnD*@a2`yeJK^85`^4^ymec`4ygczTMgd7g9tJS%eoo$1=2=h1*jb`L} zh1;At@>_WGXshg6T7U@A?S82xL5v|oL#AmO6C*=K*ogR21^3fR!MZUUY&zR zOkDf`E$xSoA8{rZWMwz|Dx|fpItl zS4bf@x2M_JlcW}yLhz!{6E9%(fXPshlf&fG&e0RJ?c!w$c9|PdhPKqwg0=n0fG#gH zQ%+U&OGgJOvYBD#AcvOJy~q^4zC`=ukdk>ul;zH*Dl?_6O&%8xQ@wccVrY2y{l|~| z7VWqoIA_IKA9T4!!B+@wdM?cl0|SNI=z^zOG{qGZ7PcDv41c%}xdW>u%BMaOB!OWg z&Fy!r5(gp;yM4SqLV2<GtWyYA3(DLyaxW5gyT|rL_gBWrOXh1v;Au)GHk@l#3VNOa6_y{3zA0%E&Yi+(PbWn)$&v|IY4O zrO&3WPtwhs!)X&#Kc z{aHdiwq>3t=tB?e8N_b6XdQE12%nOWj^ME_3KOKaY^aVi7J>>Wg{%l@TDiGnuT zmySj;g+cp;p_i4KIs}3ToJZq-4$E_Gb*@?e<|tzN%4gE)M|LS*qgpy_xBNEp^`%l@ zw`EXs`c+(WYG-ViI^sWL%3MLg7>4N z>BAJU%9)bKc4V^&n); z%{&MZq83GJ?$anv2);n_+gOe1LSu}rj_CIhtTFBDkFT2{q2lWQ&3$kDI^pL zNM#*%5W;X&ouqy)N-53xQ;U-htZZx!?m2Z-H%26mY#a$xFR)5bX{enB6WK+_=l6U{ z5cMS{9i5wb?_LrSGtW`L`@&sDCljRYs{ckR9U_YHHY}BI-F|Y=kUNkG6%~=+HHJ9} zQir*WH8dSyT+%Tkxt!COD0P{YdU~KnN<>6NQgS`srT;tETY1oaGQ#4Rb$h3kOEsTg zNcw2Joqn>~uccL7I4en0ureC*?s}Pf_wR=@Sv7W-BE{Vmt~=9HLZN%&38pd}vcpD} zBL$TC`R%M#$}b_Grmh9DpjXI)1|h`KMp^md1@DO;ydYI0&50XhpO40*Pfkq88GlHK zsm#rN^!&Bs`l_48o9A;4R-A%@7Y|cK#l-LxvG8kgUW6cR@;%gSZ@=4U{5Ixe6kC5H zHK4g(Rb&^QV1ymeD2FIv(JSg`yA`0`Z|z5xRFUJV3^8!^`uTEE&f>TQ;|KtwWTO4G zYfTBSqEV26fQB|=@CK(Q8r)U3jQd@#a5}Cj(>jPq7Vlhmo4^`khoSaL>3$8RYio-G zHca8>8OdxXWNv5=8FNeL2Zt%7u{c^n=6v`#Bzqf>j0syK1Ozs=dmjg(yd(Ua&MPc@ z0NZ~J0-oGeW#ynpk5q6)zWucE|16-qEfBd@dB-*W1*Xup>SJ>aZ9a{qCuzu`fJD84 z>R+G>Ton))D8I9u-v^8$F2e^jmiRU~iLNeV{&wa|9vk~mJ&a;B)YM^daTvW31imN!V!}j!{1-_Y$$$h5Oio;}w0wcV z9u%lPjPiWB>|+S{SQjZjtJEe?9^C%s%@4@SxC)i-e>m$NbOmk|io}^f$#o|3i;Gv6 zC-X>gm3{jhzrVQ)<+QuEH&NUrx8RqY^XTAUQN3e#fUCbtY=Xyei${`X``wzw1 zSIf)E?byBhnA;Vo8qpC?Eo0cWf9>cX1%6@aq3k1ewaFJkgQL*7ZK0b8aR(kA9u3#; zZ?-xQLx*flL5BDy+U$b|46`oEAxvc_tVs z@uj^z?2CIL+?oy`h}W%X zQMBha!q9i_oK;+)EMbI^G5^8s){rO$Rbb3FoR$G%XB$R&YS1}KGH2|1O9fvv@x$an zp3~zyQY%GL8>`_($s}#?1Q#g-5tVob0@n|vrq_eNF^mLVRFU~0Od`j+;aT{{s1**9 zN3cluFiF(TyzVWs*fUDm?CVP`Z1>(*$FJOm_bVDXqz(bWoOX6tPDQ1&%B$iG(%@6< zlJ;0_#WKmd2*gH5IgF6WEET89B56nU>xzPw)VlL(Ad40MYyE5lYndJGS&5Yey<0@M!_Ekhq_qZ z67V-#y;pIp50-kXl>0&IH8)|t#N$- zk^JdXmb)@nEiG#swB)fPjdC+Gu(8^(R*@}$yNLHP56FWTou<)U?r0IMV^5A zy+>s&Rcz!*b2sPDcXW2@>FL2^{WIPBWUUctg zBlxpew2%@}-GN*iRcE0jLwm<~1LXM1@^VCD@2+Jkq~XWZf$vifsD~SH`~3QLMo%wB z55__%;sM4ME{7og#e`oL0OfdiS|?I32g#xoj%P?foOBaQK`s(BLtI=RcB#HThvOk0TGf0H;a(Kk2Hed} zO+o?!rkyVkzBq4bX{n%qWYo{@qEQ&gT?1ysH%z85Ghf!!JW4}OYFweASFNqZjNd)@ z5Sf5*YQTdBnYp<_umnm<0JiMh$(=~~1k?T8BZ1-o=wN}+n51s}IOpxX4yzkD1*+Qj znVBa4kXo1zAb5a#*dq5R8K1dr-A-_xIDy-8o@MU}r>JP@=3B2iJ4;`8fhj_R4-5#v z2#Poc&7cP^%vymI;SwoVaogg)L9``hvMd^+_R`TUVV;dCcywk)MfU9t89pJQYu9;* z!;srKITg5{K=SHtYYXod5Y2;rF{1itb=5Ok>4WI7Wz5Xyl#e)I5Lkw!g}z3ZsmhO`2+w#qdskFYH9-m15g0@4?}MU!bf$=`o27jm#~3if`HZidbNv~$)S4(Vgtx>L%a=DMZoAEu z4EMnpRY=q5Rku{u_a5KmQnUMKHHb}iN6(`lyVJC@$u@7+Gpae6DA!Wzl9+CFS0;Iy zqgXast#~-ix@R_ekDbRN7{5ZA_0?hcNl=5TTV0EX6C)*bw6(Ww-C9yrja_#0b=6YO z>LT?(E~Ize)sPE@6G>@&7DK}|A+sbpwDpmH&PC246H5AL{Iv)N{an3ZQUym zopu+Hkf=iCLII$l<;pKC-0Tao0q5$}%`KZ>1E(3CED|ylP*f1IFqwQZ)-8Vs1CaC31z2O+>m!aSrG zuv7y+05pIy-wLGi^z7n-%j?$t<1CdzYmJA=J0tseX#i6vpljh@uev()M;TF z*_)h-8Sgu*{n7a5-)lSjHNDw0CVj%})e}q7M?SV+yxGj`{rA?Y1>69LA#m1^tU|NK zSL!PKE~Es#PQNZLv$nUi{OewN7Yp{~&VPXnnK3(=HYYVTDgqwF9Ye&zkWv>y2I|Yc zdkN=M55H3Uh3nNrwc2wQ|L&)U*+iN(Ij;`is3<@Gij)&3BcP8}U$^H~ZbSYp-UH0i z6UZ&7BQHCvEn+<2{f`5^hp>GBYCs{F{`Rc}!2k_R z=BmOGMC9+lwdkiDOu@otpJ>wktg6mH=HX0+@H%t148wmrUK;ke&ni*OpLxAv(Xfsa z$~;Nse-3$1Om0=*7~B>5mIjst=3;%&t@ zNt-*TD{=D+@D>*of}qQ1$y=9Hyu9hL&tzYgQcOZ9B@r)vGg6Lqc>l25RyUgSH(kak zt!sH2cu4Q?-cao3Cg1tzPFY&kwzgmUpPjb4pKir)f&qVx@q@@{sQ=Cj71Vu&0fo2U zY-S4nlA|arnV6^(qN9EZGl>;FE)kt_{NeoQUTrGI3QslCrYze&x4+Zk3{Ou@Bc#i? z`*8G^+%BnjQ=)f$Z@JSvI=X)(;&J4df)k^dI3aEAZXI9T)c&qGMfpOBUVKOx{9iF$ z7hZnB@K32(<5@&YM|F1Yxw5LK65>3uR_tYm%Zi^Dk2^=Xc1?%4x=JKy3bUs(`s=ph z$Ot)k#n4Zw%Ef2foG!#Zy0V$4TgB%6TuiUOYCxV&du(iU*)@sZb-%4kV%+-bmIhn8 zle?Wo@>a61UC7bUq1CPy{arQUT$^aGB9T`V|MUmTty@We$tPDI{mpo~el<{FWM~Kz z^Kb{s^1W}~EIH%F$6;e+rDgvd*#yHrA+hn?e??JD%+BczZk`%iJK_UIedQioK?ysv_Kt-7QGsDErwXI%5=ng3iez;80vjW64X! z@L&szU`}pkHbMUIovbHQjnSpc8JUBco?fAn=hgYrl+r`ScQ`rStsvAgGBq=4SgPf? zXvn1PyiO{&87J$$+SejrsDGJ)a2Io@Ie)xEAzJ1`ife@!UY_?nPp5;zb@S}GXpMBO z?vU2vY zf++Fet}!`Bgxl{%`5z7G0^^^II zXd1{&A?WWcH=>DjxEt=5K& zhO_$9%<`NOrQM5rF(Low4~sg3;UuITqr+6cTgn% z-fZX9B}Dip;=K z)1-%vBT<_B{2gXDld>^h$~pUp{Jv&l5iFL&x#GnhCGlHiAgLReBV&SpVW^ z^CJ*GQ56L?yJeN$`R`AYOEC;~jGdh{1e}y~rQ_MfskEy&Ay|MoSy7*LPvBDx-HR7X zzy?7UFsZw99~*DPSs58fn>JUjP#rwj6;Q8f(#%f~V^NmkoBtPmYkTwdEzWk&A(4FZ zM*0%H#>dEYJHVcRFsrPp>f-2_ot;gFd9KqKmjNM1qZ)*cgQsyE$Ra%e1e4=VnE8JC z)cBR}CbWs1{Y(oIWQ4CYv#VHA?iXj$^&ug&cG=xb5_m)bkDy=)*H>ez>&7nd*O^ z#G{pl!K}7y-(IHe+BLU&;D&f+ecS(eyZOlO7dK2W@37>9f6Q%Yt7EWjbPfVq9fp=7 z!FLJL9K_Y%159fF%UkJOK4kH!&;lnlp zPCoU%eey7w^|ZCkVSm}$KF`QN<_>Pg``lGN43}W=3}XTPa}7^Tc2)3rnEo$YSwaiL z6cgq^3FHK_tO#`iick>f6)^red3d(_O0EA*!41ap*-H5M_-I_p(t=(TspTyXg=7FT z%?lD6@!mRWbvGLSJ;ema?cNA+7ww+&N&TiPKs2yRF{nrU!r<25l@$b$u&zW!ME))< zZIXte20xP@Ss%!X2FO3dhE5HI(Su=%upi`||-W@?vre$rE` zKa)e~?G(tF{zh8`J66%|5%)j%!bP&OP-<@nUsXINC2l{F4PrhghH6T_L` zXG}M-1ieobtW4?POzOyE&(zLn&DusrMk>G%RkX9Dxe&GWw!%VRG~lfVO{ z+n)94wS2*j>q(BRU+Q_ZiS(iN$CVNi_odx<_t$>z6b;9j!=Ih0^kgV}HEtyZu{9r7 zyCvOf9zI&?HPUuit*oz4r?kTnp?@kFp4}F`|L-x_hh=WHr*KB8cF0P?`~L~>zI=#yFhX*I`gRccew0=SG2sK|wUO3RR8`&nFY%lFiI$Xu$B|INt3Vm zHJ+v+=`v%0N6maoL6YR4xU(%nDK?MDNf+Y31ZwO(3@j=6z9t=}uR!^J03TFzd|0e_i`03z*#RtEikRi*NrXn5f z7gn&9(o))gO=v8Q&&?cTt*( z>mbeEmIubcGE*W>$9QFCvTZ7w-!b8HN4JFv-F=Kfq70;yX^~Ujf9tdZPw(R7gKCPX3k#_|W#&QG z#(V-YM`L(CRZkBklSJ3&&!;d*Ex#bz7J_(xk!FPi=PG5>_eI^>|z zgA>6oR@$DXR2#pE@D+@UkKZ{$`m^?rxKgM_<95u8L~0ds=y&Sf=HUdy)4JzrS)BCBYDfGa1qCkH6JY9O%Pn_h#@1JeA#Dh ze;qoWbl=u3TVT$#8<5`g*-qKC5OI9CIQBd8!`xzG^#6Gk2J!KAig7Dh%iJzJGUqd5 zKp38Oh^EA=3Hl>LO$70Zk90J|#5Fu13TS7=v;;XL!*YkT1UrB*z*&gec%FlGC4?x< zmOTy+*KB694z7Q%itBpiz}F?b)5Ntu6CD^^O?>VQu7=#|vcTi0D6AF<$VeC!LdF#a zf^4-7TnYqVQC$I-`w&(1(p%a!M!F@=9LJA~LbPg#=064Jmq;=K)lSdLyX+W`2rI0* z8p#}lg)st#)HIb0l1y+E1YCbzk*Nh=EVUn4$7Bvh!_{amYG`OAYU7}iVxR^haP#KV zCx!AlM;sn98<0u`1q7Z&j*g7XE_vb+PS$@gcq1Sn(9g4-AS|OWoeD=oEj9+(-9J`x zKq1v&lZUDOIRbuM7eNY3H~-2Rq%mPQK%K(ZMB66|X%Y&_zXR_ZdbWl}7fO z=*B1x-VoH36i_kXUc|r#F7C+_CsH^_9Xx`lNB-1v5wgg$nh7AZ3g?=^QNB~q;DBo`OFf$ZruJlqZMbaqFm94jngM2VB@ zNnJiM!6Hj5CMJe+1B24YaOjT~VRHxwKZ7-&@A6#2Q`tBp0^S>^lU?1m7W}A$@q+F8h$hWNBO?`cnzmcKXE|tQ zT_u1!^*Z6cJohp)gW;rw$wzEWM8r{3NKdPop5A!`tDOOt5bYU~E|eoN%#ZHh`mS|D ziXeP%A`)I|+dT_Q?YOWTTqvnE^G86Bu*+^@ML8|O6~@dqf-B0)o60f!ke+T19Ec#) zk<_H5R}Br%ubsqW7?6$5NK5Njr;1!uELxZyAG(BRrj1KSz5ae3$(~EG68mU<=8gya za44Uje58vA)^t(W=(hL${p(0=V8DZB#}+);Ek@Ll?PXy)yaQlpgmmEEAXbRS2BgNg zcC9j_)Z~8xq!vP`dTQ$V(?tn=U0s?32ikf)7N#x%L!k|Eojf^CO?iKCVuBu_HB4{r zK;q~(n!6iA0T~Qe*Zg(RA_Xe6<0$f7dmxHU3->`hTLa)oE>4m zlP7aXBpxa)Y!g3H5F6^|8th3}Y52k%$p6LFn}Frmer?~EIa4ml6s3|Rl%YhDqzFZ& z6jDSaB7`E9M8=XN6-|_i5QWH)Bq7m&3=xqcLj#qe_jg|1&-Xp=+xBe#=SE$f!*Q%* zt$p9uzU=$0rmPq~?~I$fI~>j=kMD2E5Dv@s&s~qsmfan1~(IG2QW{VK;htT&s zZLQjH&yRJ2nwp;^QnHG#di-!Cq3^83DM@4L9=hg(f`6mJR)MI%AttQ{yTS~nzh#cktiD=J~BI+FxJPDr43TQ+cKn*eVpl_j~JE0 z#_Rh*1k)d33N0-4cqaG7a&qb+d7o;?eCXK$Nl)f%!()gBEwm3c@W+1}uT+(<&lr=m zzeZiz6le+4y7WfB^%V%4qTw;6LwER=xbUQ~KR% zi@+OUHY>?4VKCdtxeG5shob?-pVA%r;c{~;QH_`y$6Fo!$!=Qxmi|VOOt~L=aJj z$AyJN&S}ohiP%|jyucu_n5b6-j|zpLTzB`G+aZ(N5e%4bZ5$G}JAbF491mS@-to!}bHDT)FZjy!9okm97 z!Hmzp7$^MZp6i9*+^h9kIdE5KU}gC(rz>jNwQDEyS~%uM$sfKT*&ol}q6Vm|ucsy+ zEPR+q)<8AnK>x8HsbHH4qA*}@GCfIpqF4gn2%t;@60{^QrvuFy^-x59LisQ1BDA%F zfu`7BM^-lxFDoUba$-Fp>Lsp@yzrxevxiC2lo3CEf4hl_zK?LXzHNn9MJ-M?d_5sS zbx|B$HmoE*oPUTaeSWxuvi!t!{Lr(?MZyjvD95@&M@y@i zyj?kX{{Wr9s!xa8wyrQqx)vjpRfz7wNjj;6PWQ3TSf2yG$U>BoT&(2Xi*i13R>0L^ zez;(PT-XCw{QamtBi(+j?sY?pTmPjbq(JBP=pHy2YC$>TLB6i=L9yQB{&U%Epk?pi-cSIk({G z!Gmu6Hx(ocOwr>5eX#J->I{x#%G)`U|5kkdyvoT*8)b6BiMi6P zpX*^w0_5Aa-+%$=F7dqarctH#HY;qJk&&~D%b0#gYg?mt>qk5C1oVi%>^TfIX<$P` z&&#ZeIgB)hqoehC?<{v4&xYq~&?|IBataDxX}5ouc({G*yE`fgBg!O-%E7y<)MPvT zub)lq+WIgS1J;QQ-k&E*dG^-A;)2=_CNHc3rm2NNV($F|<0k@Zm^2@TC)MgrHNOl|Pg<-jm~ab$H}Q{9oM4 zZ$|`5Ql8a*|5YuBWZ1;)ji(9g&CL()+-bZmf}9;7;y0=E<5P16p>!j;r01HiE$1>a zns#*`P<=#i!}x*v(SrsK9HF_+&8@LQX`?g8d`z&RaP#JyIlKufDNeN`qSNf=fN()V z0U7bX)aNSM3pS}I zCT*^HVeO>llC2^h)6&ccV2>VFfm|moR z27|=iH8JzMWCauplA!$TOIsVNKfHTqSul^Z>cYi~2*>HfM)?*PD81<41I?Qw=3h{u zH`91uA2Qa4)gLZOww>(okt5BNgS~#_^z|2m9O9=!9r`5iqNyrUC0h2-_*&Z7oche# zXhz%XFXlz}>*w+DVSmY8cYh`bH435~rtU;&)jYJoUyR0J=+INY9-x$mv94>5ZrQNz zilj~!3y^PQXsGepQwa%_?Zq{ETnkO{+S(;-^0-8FdrcY&L6<##yu%PE)mHErB>rH- zK!&(*!Gglxq=tw`?F+gl^_RTxEh|eed|>0PN;EI%eQCf5$=)7`2f__UC+ro70Iwf` zBI+%@yPwxeYv&Inors(*lMaiK&LbDjd;ddiFO4DLS}O~o4DL9NR`Sn%|0Fj#DQS<9 zvawzMbV=+^>`S5B^dRoJh+sXqj&gBT@r<>H_07RGZtJ4!gxgxl!^z= z8^#}_6Kw7C^HbDh<@)tQG6E3zB>NoF=>>SV-Td6xUh*K#`$__a(#MnQG zYuO+P@$rJ&$k?$P1Sxx%=BeSD_L(@EmfLC2L@-!acMHeVOtiPfSj>sEToIZ(TwLD0 z$YNA`A=0bK{Vn`R?*m{yElt2CAx-G#?$FhPHNSL1pfp zJ8D~-OeJrjcoD!US@$h>*@th}|BzB3<2Xa8{T6fsccE^bJ2x%H1Vs4ykZUX@$w*=X zC22!zKoV8A?YfIJrS;hI)%{nYmy#G#v4hs=|czBF2vQU%n(~bL>m*pZ!R5p=1 zLF^`+FxTB{ZW_SDiqZ90PD~PQ{4dLU^;7uE*`tKR?Rop`OF~xkkmq;jj(?TfVd-

NYIH<)lkzQWm6d`Ta9x?^N#8_ip>vb8-1_ z{-kz`@@S}8M7_5sw+1k2Jt#+n8lozeqPR@h|MN2XOWc|0dUZNx7m5K54KmZEGPX3h z5btpX_Uap5prfNRXw+g~{5CWUhP)R`>XYZOTWayMk%FZ$Qd;3d&5stJeN9t8r(sK~ z3r-poRv>rvxjaCsfvHNoQ7u(jb@L) zbpL?^DV~O3@I!ch)2AgNSPxZbFGDuE`AE;@?WDt|<{g~GG8}F-CyI3M46BcQ-h`z*1Ttm)c`0jLz8*Q|Kh9=}0ot2P-HVT=ax;m+iu@r__#-wV%feu$c zB01&Yw8l6MY4nN$h3y8IZqt&ATMaOvmbNyuDiXQmgT5JdXGsxIc%P|g+JL>_2>Z-N zvL$w@zZf%qkczYOFD7($KksAp{+}{0)@xVGkOFunp-FAirk{8y$2=b=WMY|_g4i{+ z3t9W!yB}$pq9FG_Na{xpUy?CFI-uyVPl8A^ss^+aa+2i68O{P34RuV(b*$0AOKX?B zgxNYWCmxLgiFR!SFNKB(WHDq@O_=owMk18^f+3ZvDjoIFx*J`nM{$uz&P;2*S5N?z zv5@!N>ep?g>`BSw;n7Ha2J(C^Ha5%McjopEm)rREteRiN|EaIBQjtl5NxounH@sg& z+M1GxDmA$--n3<&v|LHVnLRs@W=ZmPp*5+cZm$t|XQJlKKbBLc4%X24$_$NKoyFI^ znk?01WejNu9kv%xm-}5nTu?@{PJqQ_4BNMza@;1n z86@Y5-Pv8c?gBOlLRfB+o8lz`UdtGQ-3m^R7cNBTtUY`0Q|NLIZ5|tOfC{Mg_NPzI zlPBMV-Q4l@;My&6zx#C&IiDOS|NQU|jqE#(CyES1w=2sAIK6kB`C#UQy$@#p_1ary zz%4>&g*`~WbSaAB7CJ$;L1X6LxTj|q4G@cOmAjdmnSm)!rkLCE47)jCauCld2N|+? zx&%pyX@SumJNEth3=YP*Zy&EC)h8-u${k7di2h?et)y(_GG}L#wK(=Zd4G&vVA6Ep zrBAgijNyuQ)|{B#rKA!gCiF7AO65Z8#ZizDp?C4i3Kfx-tgLa0UHW>#vbs~@ok{fk z7C$?2G%&7BIZB`5?=$7(+yJ9T^=2{=g%Em ztNQ2A@?Qo6IcHAG&ESo-rH|4`&`=v2-s3Hy`K=m@o!WY8teFQKW_ak8b$X_VO1nOC zM1)GWmz)wm&9@{p&(9k*W`)Ri*EfbNG<^R~y8FGp-iu8~W?uCn%Ne;W{lh>I?nsGg z?#DEaefi_$QVNWFsllC=Hcr_3(B3~#NL+vll^M1KOv$4pgE$NB-8fQoawz`%~KuJo-3 zx%8&3PH5l1a%DVDgZvv6H&oce*5m1v!w@qmN{=-_S)jDo-Vx)cN8icHQo;p9OUoUD zRraH`!@uJ1z}hvX7f(^E0h*9ivp0q22mr)u8$bVKQ;wBCe!(rnE@3JMrg={xpY1+v zUmv4|3yod3{Yh!>u&tqFXwaqf^pvLu?5v>=$%B+z#$#F8l%~}bahP8<*xwyky{GEw(~>^j1@&@f2XHMwgqLn@mi8jG4=Z+0mg(0##$pFWbtlO8qdV62;*F60qK zuh8>MSK#=8IggAHP$OyFPi5-l^nv)vtc7I#j~+P3VUGi}O&%`${L?9+GVo2HYh)?B z)=;6wiRmaTyTCx}S)X*QrsRLhDU^Ni^5t)Gq59LYXtKdLKM2KDBp@!X=$|UzCHo5* z)Z>c0H|>NvJSIzRhSG<%R>end^m?Lodci@i0iZJFNO15IytI>h-=(!xRTU(~KBK3M za-V%b4p)H$?_M}oL5$-ybojP04hq@!!J)|_gYC!^b|R|rLu&2S$oDxEi88%RFo0(O<5=A*${o#YPl@&H5Hm-)Xzvm38#sYCY?M-AU&~4$6><07t+-+xf=SxnDA11;2NTlBQB85$aD zG(vSu|DJnxTitgzPtG1WeD3RNqwd|NE0>$Z8%^CIFfAiBhqi4~e!hOi+8vD_ZLGw5 z9mnr#!6~KJ^^VU8(I+jd@CTjjc@I>kd-v|zT!7lpp}7Ff`fDakn)G+a+R10RXgcOc zE+s91=PVgx8EgW&ybQD8({run9qOw&-f^_Wi|l_GnL<2qM^*zqoi%{yqV6XXB5J{6 z#03Ndut;%?;xw(&2yBi~OI}d>hiZ3@s)Wckw>C1m!@3s+2?1WXI6K$VBJn5$%Bi8m z#-T)Yh0st=PW zF^d{-N9X35GZrmPn4O}{5y~I-IetA7=!UTqYhg~{14%~M(DnpM!9Im95&(^!JU&|c715AM>VDq`}V@7ajusd}G53(#eQQ-o|6 z>|Hl}xZj(^k6v(|f78W3L4}VMH*Gp>o_KPy*wDnqrP{_}TYTojaB*Bh0#09AhWEhc zXwkuAi}UX~qHtQk`4Uzv#|QPi01(K}o_)@36IptJ-Wh4LHXvv2K%Qh7gOE3<1H_zM!DW^%=0Df~tku-O8$%TUtOHGNdu6U;%VK z_#)d6T^lWU>m5EMsz8vB+7pg@BkPok}!n{ z>s7{&KPpz1*~6GHLH9scEZZz#*DfGV>HcGu@!;W3+04f2m8C#eqsETiDiC3PHC=9O zsPo7~y@3*kLmW6?#*nI~k%iW(>L8sr!-_Mh@4{K!1Fn~I%@)>QSfZy;@bu{>$8L1f+;xuM04ojFpm)zXWcku<#!hY^YikWs0x5E|B6L7auROAmg{moEfeBB}1?uYU+4J{MA0Pw^*D+5t<3*Ht#V6>M0u<|}e9 zlsn@OWGtn=K75kO2_3(`7)vKoHi9rjPnfsCY^jw`;&O<5MCyvlN}HBTpDN53F5Jr5 z47L(AYRPSa9X|P+o9kB^?&hhvyQdi`FY&Uk=SqkpG%h-!S93b%L*B<@zj*nwrn>qI z_6TiNt=ff80e$@s3VuYupKD$}+PLdYXOU<4 zJDJ@eV+dsgO1HeZqYebDudiqeRd5L_v$K+{F=9Fw&_`aGqC{IjJP2`RIk34BVqy%! zer)$R(A|ex|63SVYKi(FA!9CIEY?qRyaG|4tqcuSh4D9%@@%M{d~TL-pBfq(lmFJw?cVz;1p{eD zvrhf|QL6`teEan5IePIek>^>YE6?A)eT!e{f&?o*l9Tr=^=EUxG*0&)KYoxfD*02Z zWAL5u!h)7Cn%M|2jFf3S<6JfHJbW<7EY^qr&MYn6uW9wMdKd_f3`i^+NMW?&9ah~^ zhM+k*QmRjtf_MMTXdq5&gb1et->oT04z*GjhPMFlV$)*FV&9pg?4KHgMv*WMVn*l^Za~#$Ol6h;ubTn=EJ`Nkcn`Yt4g;v0Ja$Jwo-phuNo=M z({m1U!iZ%6n8wqm1G+!^*o`HC?g#D#5U7`AN*_m7cWLP;JZTLS@rCZn6r;EK9b$N})CE4?q{)bSo;G!{9Ma3%8Ha;n-KSp0f`>U0gD1vVOseM2!qdNLk z^RjR6-p1I64u?w=#-I5ggvf1EPhS4<{9?o=zf2XYM z3{{-e_ZpZ*fA65~vTr4Q5!`y_mIe$6Dt>s>ZZY`^;34d8vOX!f(Of^*2ClnBP>Dsd%NrXP^Y zvC@0|c=014S+>(Y8?{rR$f9_ry?t4NS!8nWvkNcJo{^7S{CCI$7vgE*tm7+Jtr|XT ze?l7obc3l%Aw5I8cYL>ghU+v197xF;tw)a5(Xp9l`naFK05zHd486E+odhbAmZtw? z&Z7_OKg>ElrMrL_Ysn@hRpbxojjN8)!-xOo9*T_$Vm>)fXGyBa75rbk#^o znB3vdb;%e~Y1XCc$UVJF%pqWx&50t{9>i$9k)F(-p-297Q{FF}qrM6v$Bgn@5+y?q zq0}Sr60v&yl`AK-wqkEj?QSCJLixp^Nm=Z^$5a(cS!eX;A12#1_g1O`t6^+%@4AS_6OA}Qlz`-h4SNZ<^llGt9)x%IC3hX2>6mRP&B!0Cz z=E2X62`BKLq3j^Tp^d)ZXh$PhO=u5J55QK<$rWfO(Y}y2$w;+lA8u(m#-Yr@W6t1J zSRJJbs_sFnCZRSX8wE9DrP`;vlpy&biP^--3MJ<1S_4E5eRb30hoRHACldhQD9U(0 z4w3hf&pEpcKP#-IT|%Y;(ov-rafNJhw7g;VZGiOk>B@YmdR0r6Y|i?0v^^9ri5y_RX54@nftW@=sF7bknG3XXc;y;$hWIAaVw8x$^5u@2#I# zewk}M4zZGLV|3ZAukFI6W80JyIWI2==1`@g9}LA|kZogYn}}#M{UrX`_+-|#ICwK+ zRCx5ihChB;dqB=@{J`p#o0m?%F#42SIgF8C{<5+t(EK=7uX=$Um)veQM0j(fmY5VM zP2D1GvF-%$a{b)Ji%0&$pE$X9$;TCl5zo&f!y;uE%N#+^8Klirx;R5rjm|?zgto=H z$2xa+FJ?qum+#y6S5^^~&h8w?EiWHG9yN4mK-p|l(=!Wd$N)H;>OHYPt@40;eG~26 zUENpE@7z-O12P>^1@IR$y0f%2zo`xxjxe+F&>;wyFitD8D7^_xm1Sx2D+OSMSAAMx z3>FQWH*bbruj!lpV-v}KE+Ji^KPq@s>Muwm0at=^%GKP!Bfp)!s&z-&(v@?7?N8)48de^`(_kZ~jQcrWX+sB=3xmKN)9e+~!lY%ulbsM6f>O;eHi(d5~S5m&}>SIx2`ZShu1-QaQVUs z%Si%VswJzdYcxHeO7Y)kX!gDuc8LoLW2bg%KK@YgRBSBtyu&E@4pVKLrKDjhC1Kp_ zFdF4_?*+7mCHQUcC?yDqd?yL7^44^sB41q$P(G;hLjb@=e2 zmColvc1`OloJ!|AN#tGz@)ElJr-8uw#f+j5zyM~P(lY8rJn#k-m8;1MwD)4k(IeW6 z2QR<@w8t!|42C?wOc(VW_P@WwyoX7&AkmlHsln^mIzhtMR``XY;@0o$+{(XimOQ8- z|9#)OjK+~Xh%>$epshv4?Ys$|qKR( zyXXj#%*2Tg1-Vs+tJr|^q9|xcx=`T`)5LOlE#L&c7));rIdtgLZRA=oC(mELjEs!b zT##l`n%b%t>jn)e%&xw2MQq4E7(?2a6XipopmB_rY(x!Uqn#IdkVZnRlDHDEmlDCz z9j6}fmJuG5xh#_-Xpm!qjK;{3HRu+Vl$0oR{SR_-p&?a8JIu-_{$L{I{+H9g)+3W6 zkn)>wL-&AjQu&Y2EdmufZ$7q3*GH3I?2LYe8>ylq!vrg-L4oH{12d>4IByxf>_VZQ zpMP9ut^NG@r7Y&&W$tD|SA(w~1%i;?{xU~hO1ehwe{Ml~HJ?CCW5`P{rDfoE*aYU? zy9YJ&0ogetO7q|UfN~@@Y^8+YF{x?lN#59jY$1E=PIDAE4@cu|Cdcs}YP%5S=KY-d z>(@HZemNaQw>D7~0&LZ9qWjZGIq9V*0vo6uFhZC$DJ5VNkO2RKoEx1wb-Efz0vjAm zmqvs{)RmB#NmV5**~*>8-GpUha3VN7e7=>HJ0qHLE8*)ZM&=ZQe8E3BBLP*H?kq?N z7E^hn1+Twkt_GX1abgfxfrf*0gQ+;~yfczk@E=1HrX};0838*$aKlW_nBTv^y6fl7 z^3lE$ZPpW8s#0(^G@6uhDQC~l?yEX)+pn*Sn#_|5a?0I^#+-OB*flt-m>nIpJxQ*2jJEa=e|#hh2i)J$dKpqZdJL6RvmAGL~F>`@;|*pmbfC6Fd%sbr9Q^5DOaaHdWoQaU+hFYdb4Z@1h}$9exr;P*~XIl|{R9 z-}AyaR$@Tv{SQJ4akay={}Wl6vX8jO_wU|)stCVZStnou=v;N9k7SqARpR~ALL#Hd z$pFJlN*WfB-Nckb$aCbxGo(68N!g}3KOwo|sQAS{&{N_UB|8Z+jtccjX{msr0)W9R z-Ip3RY80NeQ4$4&vn(J1>a6r{Uk~2>A1y$-wj_H4IisleKggA^PZLj{##IJ6gZtN4 z^K-T@5sp;z7;0f4L++2EyVGzl-*A{@|148%m*pJ-L8QTmdwmiLp2#@D@nj{5ba4f@+Jc%<4R*=Q$>9;hS!Cyb*rz1Idx}bkz`7 z$vnja;tMPq?3I|IhIClv7n%C^QXs3NM0sRjC}AR;^@(P z4+QNYFd?&TD2~XTiZ6!hN<#aH?XmNSDP7KUX&@LZ6IB%z8cGgnXfe3GIH`!$E?csf ztyc0dJc0Gelvb0Erjqcys`Y|=De=j?gkRw=mag<^I!XNtC~^oDB_b1AnDK$F!Pb{`5jEL|h5Ws#<=SPoa~V_O6cv3D`*s&} zrH?CI%QBl#rg|(8&L$Bs1UdqtEyL7wzo{x?X9d?r06MZ3!TH+V{l34T8hBhhi58nU zHOWD!hP?STpOL%2|NHXtDN_AGPnAw0<|Q65C)!C@SCX}g&bJq$w?tX|i_J{61{%0w zZyW|X%}BY5m7lBckR+Hg!X_8VE=K=CUlR3(+16ckzgy+kv3Dw(n4LvHQ9(g@ zSD$JL@H}6dG`4Qp@`zrz8|MWtFs3!5dP7q$Fp27#EM1XP;#I4DTU$9t!#z5gq?{WW zj(lf#PwG}6AK@esy3#E*p zG{;(}%D_rmqCwgr6CF%C^sD|ZcL4DAg9;wynjkrZ&mk&8P_Rc>xQsH)fEuJpER&)H z8cl47%3W4Y?kY~E9|-uO7+YSeKtD0FP{49)YAAC)T;sfp__>$H_2CMpYP8ztOIDWP#-jn{VJf7oXu345BF zVPTwuv^JNd7{{6)MR|(nqh}t+;VO@;3H*=5)CBQ+gH^r6RokI`*+#fNG_$JyR= zpWmzhYb1K)F1w#zUp)m(xKoZaAii8R`G6;2Hrf54S05@WtR94DO&h2%t3{h@f2pS9 zDb$x(&N2UIJh?i>1)wi5!n}E^=M-hTq^G5|Z`&s90VBK4EU>-YhaNkk*AWO?LEB5S zca!b5y>TwjUsj|x{eLY&{Z6E$idBwVwOOyKLpkBwCYPT$-_~1@kk!$FjmLyZULLfNZp= zpGr=L-Hz)-Zl#SA%ArHGv^vn(jv|0rf9^&z16nu4{j24`5Jb8yyz?&*SP~ryLY6Wh zbIv{ggH+krlReo{N(Wh$=Od=SQT~#-%F@Gd_>NHuf2peOucl;p4tlrjRBR+9A{H}Y9{F-X9FfC z-2mTUw1xj6$!6Gvc`@Mrh7EO03&<%gov$2B`Rt6QfLN^)<)1g31po<9f?Y6Ul2{=EdY_55gh5y9V&A2VjobW~R_xfQX50=VPR zQ;;JuB1mXBh;LzV2h&iGH~dJHDVs+p;%Z5TW6*}E1_4n@W32VRww|%(R~&Qpa`^Mg z#tewOuq2;ow78vhW^xxkERP8?LR${3+eMcWb@H|(t7f)3$5{Wd%Y~sBrqfT^Niu

obkz2X#DyN3Q-~b`#GHAmDT@I8o z&1X-aJ}M}%*`}B5-+ED!q@c^-d7)H~4alOc$^X!in~Gh4h^@nY(*0j*c|o!P-Ws_zXA47Zyv;3BWD5j~k&47OuC zqU?gxEY@Xs;OvZ6nXd0Oc~+z&#PmmY3OC9DM!Y!2U^&z%@af@!v#S34R^gIGJFA3& zVG5J*b&S10f{31r zS}V7%K?P`W`TO{6A?EttjfKvJ`XTUhZWGD%%39*j2>Nr7o3IBpDEY~-tJ_IBw$8T^ zKG^r}5|ULYiQ;0xY)((%8+GqKn4RB zl)FhOStgNOHgK$lsG5NpKchL1@Ts(nhry>vx<6vNNls|FPP!XZ{mo^KEe>N6tVEaI zH2W-2&$u|h?YAU1XDhimgV#dA+nS^$ul$N+ay)n^+tt9}76^FqS9F~iTnc{npS{+H zo5Gf zAq*(dz6)cK45f@MXqEFp(?J^9^hdX>l*>U`2rT(|)A$5PT7!^)g{&Ea_j4f!Q&P;N zV%1#O^k~Y2^rx`UQC%TQ&c1;tY&K9>lOnk`skUEGMORiLBJGR!D<-ZKc|8q@VtnoJ z^Yf<5(@-k9z~TCq^y+NM3)b?yQo_#`&te^&o5szb^%?G^F9=H6uXw9ar_g&%gG_g& z3VKFyT6KMM<2r#nCB?NQ=d$&l>|8%VlXFMXAQEFw!H7SuOClyM4lVP>4}8Q>osQk* ztWp?S%GdROmFI>EIx%0>9+C?2I%xwqaafgFzg?~3p7ME|TB3#=>ugQpm-9O}jB7-` z&60jV=UPd!T6~-pijFIP4Wb0If4#wynQY@(>NK-&=M8!3`MsaXS80WP|~jlpbtgs3lc@w~R9$v-9Up z7gm@Vsc<9`MewtGdnYo;$@kE)Nn4+i5n`i_?=&4Zf|Lh(|0B(1D;|BxvVOmQ{J?}0 zT#{{13VzZBJI)r`!Dc-v{FCLEQs*% zQmAfJxf*>?D9w%+-h@HXE=jR_gHG#HW|1@z)X-%oSm=Rkg7P0FX8~2kbF=74l9Uii zoL@-ZpxS;?IMNO5>M626BfKTm!8bKwhh@(j9s5`k{1dwUn!qh~m}_Gryh46A-z>OB z5?T`mTXu+&oDng@Bv%|Wg4~lni6y#SdS?N5jyo-Dosc=3KYoyz*F{@fD?HG!#I(Da zSvND3k+G7pO4Q}nvpYduL_c-i{@wal_nU5{EO*8GMm=v|_*L3i#=vTk4m46 zy|s;nC6X0lP9#03d2@%hFk;rUQ`^0S#S<0|L5{k6cfDgFNlGQYQNR~tk~oc61Op_+ ziMdGIOj|m@X|No()&V>ZbsM8)B@e?_+3j(Yur$ocK1h+Boz)VCZtG_peB02{&h-9$ z6Q?0P_w6xdT^ULR=j}GV>+aRX(*99Vp`)(UE)$i3;rmaYedIo{TTl2HnXsvW}K*Py(-d&h`L)h1@M4pfOnF|qKVgx8PjGx%UT4Gbgt z^zDm;wQ$B-vS7GVxAE?U3oR{`LuX1-^6geIup{Hu?%%rQOLqO#GooX#iIIg>x*;jQ z#xI}G*2lpB;NpR+Nc|hurV70m<=OrRQGu2|e_q_;Z&nDVe}3`vmWs-d%WK1>>1~O5 zVp%ke9o#Y{|a-YIDz1n8~)908b#j^ zxMQrjiJ-<~)*4@6@`cZyow_V^=QSJz;6Pop*GSpWgxwsFO$2qBx4~EKC zAR|K(fq-gim>#+mFqyQp;?h!KW>Ni5I-!&0`}OPhsj_ltOCrn_1?`iU3^tKcB4UpoJN6o9{`KLE4k)N3^x50k!0}~pwBNsSOVt1k11==DZi({hT852K znYr}{7k{gZ-hr0fvTb*b*QIZ7JNa7i&iD~dVP&Z?ZQJ(jJwR5c#)-ld=u!U^bK6mWJy~U}E+nv-IX4#?2b@P%3uX595{zVy5ilt^?)Cb0=q|f{<}GI=1F;Wq3H47VTo$r)nl_=MYsB@ zuoOp*%r7jIQPKi@2G`otg*?WA*3|g;ApzN*WGEa-P*;MwTHxabOaxKq7}m5sFH$Og z{8-$#Z)HV=(WxTpE}%)KT_ARc2kb4o;7S8P?FzKbFtQsrZ(h54^$0aJ11VvNSy|aG zTsYX@-*Cy|#c#m}$)PK2YL25-TDGj-GoP}Xd7K73G)U2XIk$hU9xRAMjvqS)-cj-P zt+;n@=!PM(U3d@0K!;Q&@S5IbUvvx5rQtZJ02fCwf|~$k2>dq%1hMAOicXaF-}iAC zqwnt6sS}=~*Vj*-BEwfR2Y!w@x^#OW6}$1Td6oZT z&N)xLJXhI(>?}=m5bPSxtwnMN$Zvc0>nF&! z3syn7*V05JxE(+UQ^#1e&~<)~CqThIefo5UBp51+1>zDnI*J~lH>fiIY>2ph@WF#` zQRI_Mo;syNQN*OLOi}-C9lfVuhsW15TAJWU9I$UAsiz>V%KZMeOx<6coHWHSHf;w_ zMRawtv9|Hb0RF2b?B>lD#9|zM1iYCio`?;h70yK}oil!~!pUBklhZ+o6)4lYcLRqi z%qsZJV1Jre(Jv>*#3=UJH`%K(=G3WYTSSlpR39=si7G$q>ax$#MyieX*T9$L8pMdw z%;=h*k!%v)F`O}*$J8YQ?+SniWQwd65ZPnLkMkY`#rvru*VU`_w{AMVecB0LZXFyn zHbvMD%`!1LiiZ224b%)TRmg9ui-*0^UI0M~1F&O9yR(9}?AWnaN#$9g*x)56AKD~@ zN`s)7L}_w`x3iY4Uj1Dx`2 zF{87C-!v(V)`zO9Uh)n(PiHy(4w5=&LHu=9Fn)Y?-wvDWZ$wsv8l@OnS>tT?*f zeZp0IQa33QDujsz>9r0(y`b^{d&2x4fi~JnbGOiWsiJby)2S80&%1x06A`LrJ(_Kq zVZ#lb;j<`Lm{9v0m>hdJx;qmK`bA?qn7!C4d32OR#bd@F=U0@fn5_jhA0A` z;}=gD1pIn;NPtvP57zY0I(-~?<6dkgMeRivX+h*{>K_P0X4!Mta3jJj({eW`Yu-Km zB98tC(K29Qf;A<)BNMm-C;JT=&!C>AskZXPF-NALyKzO94=H=AX;45?G zmW~OhZ@w93h48?%u^a0@%&hjwaZKekZtRxA#)2H^)qeZhil6oMcYr$fckWc&OpBuxWUxlxzX30W zG*I-t#p3BaA=y`4#H1P!iQoHs&~@Y2EGUa9{TppR3j1#i)My1191YN@cihL@~6)+yW^^5yNk)4;d2Q;BnO#pqXw8 zxJr(y1r82A#I}Jyp(|*#0-vS>jShqzTcuAtaV7-(gZAZhqah~9d699??oPY6Rgd4B zx$c=4)EmRcK+o0g!_f_wp zUTaOVRcPVh>|lT4MKf;obKg04@vai=*2j&zl#n1GL8hv6Uo26cZ#;jO>JFPW?dG)+ zZRsg@Ky~=-Qn~wSq4544QyKFqSf|ZNfNy?$u zey2_i_5Q)4B`+OLzc!*aKsV&4(B1$-h24W@8r#JC&3|I`My19;xC7~_-%eI_Y2TKH z7s4(H4He&&jEv6h+xnY3ImI(p26UXT!Rr#*3+yJ-eDn0_IA}_6TXHh%McTDvrYP#) zT*W+X(pVb|4`44*N-)yz?(2B3SZ9;1zL#3hEnUkMi#(5nhN6nk+Hr`^i~;@oPxAhQ zCRdoL3vPxQeVP>HE34)a10SZH5GY!}g6ygOP|X^OiZS_RmAdVtgQViReiRY}cVE=> zLJS-^(v|Kx`K@7cQv?@@;)(CL7rYo7OM6*8o%i&7aiZ74(w?})ibRFa=I4z)FfBWL ztf2{q<+N!Xd(1l$5;FB?_!?K&^o_K;lhQb#W4dokfdMPM_ZQfJ`6le$Dq`n~M{NwygF0I3hv%qWb0J8z=4W zwOBTfZ6|WS;+^oHzMyDB5c)W!#|hPkT`T{v`Q!1oSS_3uwXz~QiO_G~XOp)T_P4qD5vmT>mQ0m>szIVrOGx|A~6J zuMZ#cS!dLKyHQ+$bmcx(%{gkr8VVn@F;r6O)2p`jdRkMLF8*=KPZl!g`ufLS?XxO- zb(^N?dc&mnzySM&3kUS-HP-Qtl&5DC#{i=ae~|z*I2x`yJRUc=PV|C9u67^L%Pn_b`BqMR#sUr+t} zzO~!cn6R^TGP*jRAd-*ZM8F9tx`Jlej(AF}C37yuZ~zN123gT@*>Oi~Lc+WS3tSu> z{ls{&uy>j=CkSHHq$K(AZZXFjCLB}k-MgtE(x!(wV_8>4YKk8tvxsxlbgf#u>-qm^ z0lc?u3%PK?>)iF)SCP-W{1oNn+M6!dbfqGj>Yi^J)pXgc2|U)p8%b3WNg1~nKuy|eS=c{@%jZ|)O9#s z3THz#6_sVQ6dmu2EK&5h1|KGJ78xa0Z(`Hr1Jh3ECxYCFd}kNV&)a}@^zg8`tkt|g zUHT;SFrXvhggANe{Q0uw%cH@@EL1TBJC##;OEtA zkFI(ynlh!FLDEto|Ir8+-5aI1mVWDKBr+xQlJaXVMC|YzUOyEBN4K`UW zmVtvrCjLabuDK8o#*vGzTD`C^F{2d(^gdpGXYm(Aoaj*a%Y3+@tu-mr2`@BD9NZ*p zDae4)C(fFDNwKZ5kqR!P71B+tdTIjuMVZ3K58c6L*SE`2*fA5%gV~0 zS#)il@Rx*RkPiN`e&f^76(oV=32CDy&o3oWNNel~jd#{zFekP!JlZLvxo`Z{tIhmO zVW6Q4+MTU6O9mOLO_+dVukE|wy=8;-^o}X+E^E5C8J3QIqqGwTBQU;U+0>|Q*-b+f z>K1t6Srf&>-qtk<<^fzI4rtH&PrAOjFOmpU9>P_zoM?p)H%&-u7wiW;#WA>Yx{@}n zZp1HscXP~3Enb1-E2fozYW;)jr}}kK*P={R?&syLT;UXJZfkD-c;dG*YE+_Ejl;Z2 zrnHd}(a*W+hdmfMY*``3iM{saT)$W&6-)X?jbs1v4`d*U8vB=C!6qb0xgXZY%kP%OmlrIn;l;Td zBo}`t|9SV$G1mNfsnU!NDFF=;b!3mE(fDy+zKF$U5{bdLfoJBZ$b^Q4{d!TkiRFSq zhxD6gAfT?QAxRWiH3lb7@UZdD=Q&Mhfsskj2PJ$@M1&kA45!7Wr%dd8N_8+%`=n-o zxf%t%bBlD^nKPz~7G2-G>93jChzdqw)y2N=>Y9M+z&2iNH<@m29g3c0N7lhjiiH-I zmbaH*+*(<>f=4)ie%|tn+>kqc4*PN(t*uLbT0z;Gs$QJFDe!TTBv)vC71<4U>!!87 z2>_j;+XdXY^~<@Pgx!<;!Jw6NYW;^7tqhpt505)am?g=7`;KeHeTzn<&K7IcD z=&@rX`s@SyNNm6^7Z)TPdsU8DU%vbP2XBxikaq}Jg3I9)0V;IKN2!mG2iRxzh3W)C zfrp*~@`Ac1w3qhwQGaY`2|~4IG`7jh8=Pc{Smw0RFOCezBs`SnkLZ)3&*)-`V@8b8 zGVAhzo1-`Ye}TbW+5Y9oZL7x?)>+xu6gg{gvo7VtOI+!Pcu$|SIvl)!_G>%4GrVYy z?!PwloFmq|BYimcJu?rAs@zpWNHBa7a0H+aJ}@pT@uY-B!~ z#6;3^S~oOm+;sPmqVCHvltS3KbHr*Fmk2#i>?(dhL;wJQ*SLB1Sg1-8Hc&d32hR=J z*yt!Lw+-8n@d|{GM5+Gsv$gm~@lvnosi+vunzf38fH%j8ox-k}OONSpoQYR*Sy>rg z;;&xmjUL@Ij5-%{?jHTeU<=(41AdYR({3j&^4}pTE z+@pJ}?==L)PgTDOg#kJQI~osD;2Uj99Z;&}PlE9Rr}VCIYAC$i^dv9==+k1<#MEb_$o z_zx^2$+Lum#*m-Z7vO7#=VorIk<;ia)t<)yJ_KO5$)-FKfk;-y1wnV zegMFviG%b!+)y{Ovp|gYK7ee+D3$J1FmpttDt-2?Ya%F80FlhzFL%3l|MhVLMJ6*F zNFhGA6B_i_uPFcgdDc?~5)6sV2UHz3dNf@>VY9Eu=Sl>-@8mxLrsUOfN?k1dBFqJ4 z_`J4u@4h&6lV0OZ?l%4y*pA82chaF~boinTl8{fz)D`nZKqodQlh6P@Evda9px%nb zJ1yv#AW*rUc+KjYSrp7FHlWkQMq9RAJ#>g;JUDG|wJh6${>4idF2t!8kTGC1Bo2Ep zL`rbIfM>h)0g_eM`_K3%bC1km<3r|pZ+m;IjQ~V6!)%ag@F02RG~WQ!DM=aPu!gSq zhF7@aZcaeekonfuLsITdG-4d9x!Rp`lsEq{t9bv6l&ciS;wfUzwh?`XD=BSP+zrZc z-gd;F1491=rXXRK#qz6ZBt#;t90JVo3RgCq76}N)j-5Gq5{rbH;yXy_cpE&5&VJu( zYZm}q$S(aV24iK-$?U{X0#+h>1%}!5Vmwi{`}*#kFrnQ~krNtp;@a=n9znTdM~|N1 z)i}y~-_3b`iUNE^b55!)22RYv`0hfR@aecX8F_g#@g0x@mO+QM+tZZ4O@nzRz2;=X z$C>e}K@(o9mUBQ7!$De$E1D<|2@)QiQc=;6cb2b56qKn`)&GGC|DmBFeN!LOmjF^0 zYnSPf3Yds-Bu6XCu4@)%03FMI=+FF|rB^8ybIWB14!*W(-3ff*$40Io{ZH z@Et!z&`*9EXCWy+{C8+Bxqt7Tq7>9G!xCrDwAg%}!T^!sz6d=y0BBF&#?33XN75^k zzx?8lN5!O$z~h$tGp5p4!gbrkeMde(0Jsv4GB_MoOM|uFjK8Rn*vQjU5dQ&sULF4; zkd6xC0Y+K7-W;0vm>w9~q@;El#+rYsuHI|Yj(Bq=lMhQDgyx z|8+l2#QqSr0Bk1*Se`m$5{3DhQB=RXxoz4{L8xvXCMfZ?7LM`!_a}onKKe7hR8;sE z^c1(p#Mzja?x%>|QF3hTl;x2e3#i8m_g>0o*0K-cyY^E^Yl@uHNMY>sS)7#h;`Zh5 z-?M}U+SwuyK2=1<6yMu*I<8GZYd9Y@Q?-CBkSrlJwdYNFzJDeu2ly7Zc)x}Yxbmu~s8{sDsvEeS!MZ9*0A_=Hf3h(q z?tK5uLoz)!K3H)#W^Uk@Zw*sz&zv~XtAGE}4@#TIa;R&`)u2pjtU*#VM`2}y2?4FR zqV&N70rqO#XlFNYM;4|#jB<;4;#{Hm_1d=^pJzN^u4d%46XkVl5JKiuN=f+%gJ+*S zQIb*~J9h5u*?fj{7}@KMPOmbjVT+jt%sfTRdzvyu34$jKJ#wFDKViZEko3AG+qPjP z<%L>5Ev`ll%@}e6u%czPbPbvC+|F3+5QK{6~TRv zK)Ad6D&FL+v(JTRZ0* ze?tOfq-;@OugaMSe3&(71>C}1aN6jguDpl50NZ=DYlNo^Ps`cOO;DN)GEAhSp5Zb! zHhparZ+?KNB+%Kx91hjgbl|*8IX@9V{5^cf-@kv8=BTtzM-AyA3ds*^G$w(8-r2P6 zp*%}wK2#kCD*+;Bh|DT)7$g=y=su|r3B>%e*FKE|ipED?RF~MSfBP0BX09s1uwv%y zzvUr2wdC^e+&S6l&-aN7aX{OV#jDI(yY-fC-3*m+eX;+}%p9oMizjpB*GZ>$-@Z*o zugEVbUOg5+?faE=e3h;q*Oa)Sz?t8D92G8&ZY{rVw#ZLd-(HE(N#$tb>Rl(FNGn!A zcGcI&o~gE(Na3Mr_PtnS!j%%4N|zYzn`lm%j+20$-K&Pto6m3xaU7j5{X)y(JDKVT z$h7@pkXv;PjXqs==G*M~I-K=3XAUROI>O*U=}v=m(N(zOGSMO~Fupa>U@N)$V4fv%bFZi@}l5 z)!B})>S-L;WDjD)L8}t(Xd2>ccumI#QW)i8gKwL5i97Qn9c*j@B2r|eV!xLCfhL5p z3_Eg!@#&x0E^wjknoY)TEsJolwr=2c@=FGj=`#Hls|89nmI!uqFT7qojC%G*Lp1Sm z+4qUc9CKaE^XZc(WM9f}=2=-C9QtHyJL!PA z^XKnzp#5P~xT$JLUb)+riZOziobFo^*?X(n%H&tNjn|UHN+a*V#n*i!^UJ_bIkl*A zGa2#aFAm7YiLFP${<4-geO`;T%NJe<+&^+0-~&6h0*McIsQ+{1 ztTQt1y2taE&l*}U?YMZcufqu2^9H=-Z+}!G_SkIY!a%;n?dO-J+}z@SkW>)a4HNVv>39WVVYSsVp z*Sfg8NL|`#Uk(G|2I;R{Pg4_EX;96G#M4I5$D~)6*XYN6F%Z#i}BwLS}?)7p9?=2%in;11yCI3=7|KKYORjdnHhc^4r`03o>2o`&tG zFv|M9LWixLk;-O{G>{5*{TBS7g2gBJcl)&5U=+lB=e29!WHymGXJlkFwmojH2At^B z!&#p}mslQjR-zs}86V$(=GyMxm(sDXOsj>XaYAH1ZefS#rL{mzzd{0;VYkNGy0>?? zbF3c~8MIlSNYolHDRW#-_6dyC{ITzRdU|NTBMHB6cWu)n$#L!4pkIDcv7B(6sleBu zau6ouZ+5fK%DjGtX%4q>pg@dswO(Pj=6gNRsVJ$cc5KmQg|Z$nNgi?i`L#|&c_gQ`#J@1i!PF-W1G|~LRs7aHK7gS>I<=|5OZ-theD;?R6saKMdyG+iqTC`}SSc(LY zWP-Q0PWwWW%uOk3;ji95!&PLv{O|}!ER9%;5h2`8e7qCGJiS6c-GG>H^wPhP*H+02 z8sWZl@uNo?W5@QYED%r@hnru&=C9SPnzUx56Xz7L(4O79nY6T#E4>#Lx8eezzyxV)GLjEpzy4#hp}VIe^?jg* zTW+kNs4+3w4dVy$7T79a*RO&>Tj%;Ju8?x zQK6`#S%sG1h-+L?n9`kO1RqJN4Z1^8P;9JuLaGeyOM1>ACSue~X{~n^6#1ua2-yM4GfX93E<#g~d8VrWMk%n@2^3hx41afU-itF=*$VlDd>1 zZ?XZ`H(Hxv=2om+S^9cw3a95MCL(Nu@Bpz!sdaE$vY_aoc&7D&G>q!w%D(a24G?-~ zAh)59i~cLP?HOb1rBQ?KRJ-o_yRorb|1l~&7Wzub`>)`!WjSlsXXpxHcVp-S1s*R~ z>jPGX#AF+}9ALQcBoMs}QswaGjS5rD3C3iID%W01rs`lx)bekeo?ZXa*ag2Dpj*9u zz23}oeobH0jk4L|_FuOW4)&3>0Ps|JtS0+IgjUO1<2d~M<;#eYTh{_5Ak*=ivjVPN z+ltQsE$=9%Nny4Y-ur09E1_AS`sHO!!%wU+`a)>)U`WUMO`C4GR|zU|gr)r7uHixb z$0p!~fbAS{*4OC}tS1??Y?n7Jt9Zs#R8;*4(rBDEnK@H1&Jj|{ZM5(pOJOI0-+ih``7RG>vp?tm$&g6=lMJz<2a7T z@etZGB%s>dV|Ivke$b zWThfgFBIisV?`Afw~ zw$fFG1^4dFF*C#TK;YE4Q4QPns9$K~fX$mf9~$X(PL3@nXhYe>Vwv`Zyj4g8$`AT@E3uOiBpe|q+$*9c~xr0i%Z8l*RG z&TF}APMfxyCl!6uBR@Vx0K5&nEc7kEb2_cx->s^jN~5rg{?E^g@DV$AV8zw>Qx1zR z(54+fw*MQ7{r>{(y?m4Rb~%aJ8r3xw>GNP?>J2bLx1V3WT)J|lL~r8=@4xgsEl!<~ z-US(9_Pu%$#V*&5BR$Jmx9k27gp!6j((=PiH&(|eNq7RBA6fhE-8%|4`#pOxYSA7g zs#7#YL_~qXq|q80Etc(q{)GfUmc+|aeb#9lhmN<{S~GEI#>wNyovEDQE3vSyDy<=6Kj zfMB=Q7qvM2p4i$+-85_F%-wUA@j3Q&S5dh^p8Wh8<^}g+>|a$UPrf^v$V2?&68$>_ zQx0e1Nx`ORJr07Rp7QhCNRVGkvq*w9m6Ux1$SeLpayTwBUJ*XWtWVDt0B< zG-wSrkL7H#dwYGpocK-mDj|YRvp#eB^l7kd9#jNzhyZ&gi}R_Nxq2Z0plwJ`6nX;MZCRn#o5~C|2N6npUNxwrk*}99-MGSR~ zjE(QfGT!V$Y!Tk%#g-3GRYZzSNH3c`&6K6o=XkG~DT978}=EV=Nl_Lz=t2TZ5 z-}?GTbz=+ye1d~H@Ov1o#67>9Z>OK4}>KOA{Q2|Sn-!>+J^ccG-IR;M~VPazyeWhBQ!W# z^yo7j8DPE-xCR<^>~{V39Xl{251wMF%kG7^LaFtzk;p479PJQ_&}@z<-}9!GE+>ZLLb*#f6dxN~`C${1HQA0U zM*aT91}aBjl82b#&HbdT_V;%N^&ok6iD|e|lNmd2V%Er&$ssCUVh3aBCwR*7+aI-> zn=N7=W>~bJbtFa(p9P#eey?08~o-x z6|Bg&O5fj$iJqLuqIq+cl?_rPG4Q!ATyQ0z5p1bKKqi-X3GAMaIx&x8LbY^1it>~T zOS#Iz@`$lxMMXtJ^DB^(5n9R%0=kIE2*V{#GHfg0U+)Q4v^zxKO1;H{N*l;CedK|l z-E+By$QGRT90RekQI-}Kli?h26+k9H%iqtlugHskm|6>c{ky&%s4E2TQPSdr_1CoJ z5a3`KxTVZO8nsA6X?q*s?E!HH%*g8VMU5Ya3a{^Ui4g`w^)9RgqP6D^TnMi^;TP1F<5AO8$Oym7F-kRj)D6 zfH^WVa|G{V0bjsu=RHDs00GsGn>c2ffl zU>93T8Nr+AABUO79@(N7FIWu))zA8k2Yu2#TP{H4E7xONSV&IR?a$axuGR`lJ%gGbx=={pkehaAa6i#WF7Z}QN^1*#^h4J0#Y)8O!n9ou@k6*nonD9 z?4(JZ6Q*{DeXaPeycqB_K|8V|heA9esconhsO0pO+u!Z!|A*91J?LiLK9JPLvA+YG zF=l?<=vfG8cj3Yc2+2>u`xla{H|n(z^rwB{B!MKh&KXm7z5l2`m$F>K=4v73co4X^v- zD;S;$n*bg!i^D675`kA#chTkQmlC{js@lt37-2s-IoU4l`hf%Yg?C(&g0HQmhMR)O zhu+<@cHRE-^PPYFBxE^ZVN=*V22_vlq}~*C$p`GClHLsL^%745&d6%9E=Qvbxcr|_O)C`XXX6cr(|$lH9A zqB%D}pxfTHxDD%bxHf|)c~!z?&|g#2rAwPvCZYgAoWl4Ciz0B$=L-rD+S4=RP=Kkd z$~)KV(0x9bdr5M84Eu>kt0@sR(edr&w9U(b4PeLkO-J)@Dtthe3;Rf$!-RoS;+9Zy zHL$CQ{VdK3MKlMZ`<#Uur3J$;EE(evT3{U6MP%)ug~3|F@xTuXX>nkn8M8o$$E~fb zjx-NHdkj@Fmk{3w{WFLMF&20GG2oRq1gAsC49`gYHZ-#Q4cuVuwJ(3zMW-Oc<}k#B zPV#?ApFF69xrGJ>Tdl^7R$dYajjpH&lI^hLl_2~C2)v9d%B4$Rhz(>L{EK_{>XpLK z&5FZ$-7t6KrJ0Ml(feDWOXf~!X#QI*V`C;2D(!(yzc%t9GgKJH6#i2ygm&#oJ+o@Z zRM*z_?)YJ)6^5YGrc7ZjpcyJKLdO3R0-kxgy7a&_&rGSu2sOyU68C_NT$V`a&VwwaobKx?|;P$!I25-EQ&BD z%KRhjW)ji1Q=ITqBy|G#7V&?1g>u zMD(x1u%Sbbh%?G!qq(CpgOmsL!S|gp{Nzd{x7u%gH6`&t88t~Ct>=u{voAdU+*fik z3mc8sTk`;FjId)kXM?|=GVX^IT}u`(9_%@fypE@=Z*;q`()PkOOUum9zjbtUXyKV8 z5SCumFZ9gx_47+aQyy?@p~5k5Z~q3!TEMZBUS3~!reH<~gS+MH$@Q^JvVgDq`}>nf zSb8c9$2FCbphMq zX3B`@7b_=Ys?h5B$#g5!I~5N?+n)VLaHs3)>m&0kaBzf=3YmV-5EVM>!(eI=q-E*c zIY|`Vy|@pDo`1wFd|`gR{*onvV=I#k*uDV$M3>4SqS4n!f{)-9*q>xSR#}IAW>qXNYCZ%0Ae84d_;YL^eaic& zjT$wVoh=U@2rTc&k>OXaFzx!ZxcI^kktFa0%1Kdq?9Qd7kN4)&<>chNTho;!N}=C`wF$-ww~^z3;gDMQ}_n*B(r4zv_y^*;8ONn=6b*9UQ|sAk+M=!$HarCZWJ>+efF&4HAA)lvNN)4 z-BOI_M8k0IzRsGwRyv^q4LwuSJ?LZ#ewD*0h=vL3o=-lm7!q+p3o3AV#qmUJ?Z$_j zRf}l29W~4+WFM0|ierPv3&D#%rnX~}0}G6Trc0Ay?MZrJVXXe1EAEk)xSNT&wiO&B z=g8{Pk3GBSo{*fQENISkgoX6~4$S1a9iT(>S_>6icUyYa9uOa8v!4tRh=vi|htJ%J zDeH*Wg34l!IG;%3b<40mk3c$Ob~REz?6@fOEpH!9Z?e&>l-R>uYV|Z zK#tjNHu2TgjuQPuN10=V`}M&w*9Edm*o+)qI~y6s1F!d_V=CuI?QnmBjb1<~t6R|= z?jG52SeUQ0mN&mhax8JmBt_q%vk_XtBM-ji-MuS^hi;BHj~H%li?*H}y=MYN+&oc? zFua}gf^;uBIy?LBPTE#{Ok5oh?!lkmB0fkA1VSF+-Lnv_kW^1X8XP1Qp`6xkwk7@f zb#E~1;0;Hr$WF5!w0jrCxwsCG7JeX7iIMat599~V5eJ|1eUrKhNZ)e4i1v|#UsC>E zWe`jy;+5>MVG-&yy3Z3Qo{{fBIygbXn3>u+2GhuiPpmtcZ^}WCf0~e)?rkoF+5tN5 zEx&v2ZkjP#P{ptboxYyTfF$+OB436odmX@k4un8MXEO!Xx_0E4^KN`;gvR{xaZ(`- z>;N61d$x3 zv=WYYj!yh073f6EmS-tw)k|@Ufd|H;(ei>%?n0@ISK8Rk9RA$*} z;Uc`cmvw^+i%btf1o|Ab_fWiQnC-?FG+z2L%;A_|E#7iANF#ZHz5SooJxH}SZyYI+bwgWj#-1MmVAV(~pgq5L zIr{KZeRuHz1M-^ex7S>bihBHUJL~%b*bI!%SWAQp59Nkw=QX5REIw`={ur|f#Sj;Y zin?%QE%~U>cs4NpU?ZGTdb;4(bxQWJO^lF2uCbrag5ayIEs}2d1@y;avLw>Gy=^UE z4Kva+9hr~$Vzr~=T{ldnh$8osm8;iCUdQemYcQM_Wz_ws0@2sSG8h zq(*w+gCVd9f51NyMVi_;h?g}!0Z>cj+!W;Xl@f+O&FsBxOty=!)mPOV#% z6?41KVWb-xopvs{Ev=hK`i2>fY!SjdtAx2s&=!~*RSvGl3u4pib|R52FIDYX!FQo$ zgC}sg-i82v!?Zhtg<@g*_FIgttyyy(xV%J(jTxVWF=u$jyZgFG+?e6srlIpBJG*xV zWmCfk!LNn~Y_XwXhQqI5LC3$D$MQ>5(3o7F#<`+QM!LJVqq}5pmtl}9jIE8$aqmw@ z-F>Zw9ET2NrSUhi7k>dviXsBK6k2PiHJk}z9u%LQW*r1hN}{Oz3eInX(oB(1%Q-dg zCrV^NBV^cDNN5g~95iU2DH+zhw)QwmH+%Io$D~Ee(Qbx^)355BdGH8*&! zR7zt1;HgtWrM~heHa$f}L^I>uQR402>ao_5*RO8;27+%C_i1CArGY25g#0Cx%V`n;h!=72oG@XvkS{95LBK z#QMlLhwetkzGcQ2bw8G#;$m~y-u1z;A$g1l<;1I~gT7WCMjJLLm|-zooj>r4qw9H% zQ6AXKM9XIE{3@m+0MrGg1stUTIuutM#E$sl5Vx^r)s#8n*pQ3~R;;V{qBfzSU=ZPY z_c6H=H->o5n~}q642_8&cczGj5nYl~%C7=TF74kIH0t(qWEQ>;GNQ9o4!_PlaiWiB zkVF9 zrAvLUU7MmamVVYRciY?R|FpJ8$@Mz$BqwL%WXS^OPupwW)1_DDnDS^Y5M>g@M@cZ_ z5MA^`_V*ArmWXBa6%*4D$fXq4cZ>6r>}WN#U>GHUMbb6VJCM8;{K z0`fxkDWDFdtnfWV+`Swd8w3t|?qL6EN4zume1dOhH5D@SliQChTMr{nKFkD4K6sLt zugt~*rQJ_nz0~&2)%{I-kf@4=fvB`F_RIcgib>;;nf=AYKJ83FAak$3Fmr7Sk`p9ib^vf4{rn7;}}0I`nFej@qm0@-J^P*xDFCT zQF&Qe*~$y`bodC?Mz^Kqwpdo@T$3<-*(U5?P!#=i&MsYW4@Y{y1S9f^qQcfv ztf}~;_VwF0uF5D6o+G*IOEs&^ZJ=-?gFQI)rV%?$W@I};JId&9?` z*1fKL`1y0O>zY#9qK6L|d07=M>%pBck=4HIf0@Gkch;n5l=tu7-vP;_t!pytcSMjv z)+k?C0%)!)Dlqr6`<`JQ9`=wjk^PDiAC@ulFUUN=HJD06tAJcbog zHH(IOh(A9TlmGa&4y57Sv)qpP^X38Bep>MHMaHbZRAwe2)$1oq_8y|d7z}cBE~hey{9B(ST~u&t_OG` zX~e4=TR1V4mt=*?{AstwD9gymxWp+h2RoS~PASsxXvz680?Eh>>&=_X#tu3?O;9^t z@bKvF@dEH|mO>37{GT2@f&mWba&C41B~e}Vap__?$#g-I*1gLt3-;fGEOuZ_n49t8PO9TYq%c5FTXHKKfHp-5sX|> z<0_6Gow!r%@RBI~^J0yYf*fWX$zU1OAnSEhh*_GcS505}5MZKE=-$5c$YG>Ub&NPl zNzW}z20_@-i5oXZuq*R)d9n8TpG^VO14g-h$*NwGQ$`ZHkb@W+CN$&}k%p+kn8Uh%KE&d*_)!$QgcO&aV@brrePztnZH^1YrSISU?+ z5_A-0W#HB>Wio@)Usq6W7c3TcGhMR2si2z>gupe2$d-Ljokek=Ai+A@kQ04>2_kYg zu)4~E?Z3{+zDxNW?@+6`=C_}fXIg*mNx8^N_>qU}2M-#AL;_9E2T5>Sg_D;>4?qmW z%UXzZu!tddb94L4PGqVDISS$BBjqbZ#3NUyk5P++^P)HoE!wHsy>KUy?_8JCb_kW=u>4H;#PC1))%;Kh;g(6{L$yR7YP>()5Pf8n1<#XR3JW;&*s>zGuCa2)y`M(&|o%A$t% zxDCyHZ0?eD?b^M6BL%N7)Z(xfNJoH?*m^(s?f0F>g$p&&D+z+>*28{3H6Pu-zaG|) z-(`)OI!lVazn;&TC^|29VTqlgdz7u4!^+y<$F#QeJyl-YKOyU`+0b-VCG%N#dB zP+ddq-E@z8d2Oz0vQ;_^Bo_{y<8X>~kcu5^Hww?aQ{DKwKc60du)AbwsM1B`(kIJv z3wD0+{#NaF_VH)etqzl}4LcPuzcvRY93OcpD+Eb4|F&!`pvd2%DphxSM)0`ww)ZY4 zWqS{{yIhoFYq#Td?xq`Yv9S~)mck-}+UBI{%&D@yyNOi4m2+$xZm-_T^x`qrVu^_r zanDf8=Vdsa!~^ufKf1lRD5L<88Sur6^`Uz|Kk92e%|$+fm^-)Yqtz`OQhMYaFtGeJ zoiJhHM9A#Z_ZYu)V_y)EvOogyLA&m^K$I@A;-$ieuLOqkL;l)^%rQ3?T-;a(`-HfM zK6|^joVmHV#4ezTYHBOZEl(Q`<{0k$oc~gyXL(NCM~UlF!K*k>G-_Jo`uwr$w-k~i zZ@%LZN=?!ZQXyep7- zjtUCVms(t6WAVBi!|gscqHYr21)rp9*4|XP|E&#)@hQVeqdclzhtC*gn`;_Tw@W=F zHYa}A9C0c{+`&8nJxcmjXHUvd&G5W7zhSC#?Pp_<)qTlXTh(q~JQ*aegMez5ds_>S zaC+mnb7UFHO0N;KgPc|gyTr4U~mj!!6lF#o!>eTtD#LCbI8& zx2)PSs)kY;LN}%H(m|e0ofCb zR!hO!%1wb-QS=+i`zaTwCE6SxlLOw*Y@A46VH? z8tF1e(%ZYxScvBUFWff%^#{T=k1*=8*^Q;B{b?nb#iH-O>3(!!%bfSBj73_{tkOI- z{L)bN1db6s5VZ9}-i@sEMEWaIfz~8P)|!lqM=^wqs+#Mv=?%0K_;wbQlrzeX5MH7c7$QS(9 zX}<_DjugG}hT~ohtDQel??>cq&T+qVE6$}C@Ems=h!5yX!h60;u&LUBWqW^)UJ$euuF?crPH55&R=89n*$v+G8y;bvV#isbyZJx#qZ zs>Ic zw7nhqt^KM)=?>#HHnMkf)y|r4ToG&0ZJLGp6*zy_;2`yGBdj!PA_i3=u|u}aAojD=O}U$1jhgBc(2yY?Hw=ZkxlY1J@_+w zP|?Q?i5G3ZFIg685>syf@88eJEr^DxmMO0fw1uJ%-hJdqVZ?>9lqUVc1@9uQvV<8Z z^Tla-Nr;gsN*pyxsJU(4k9FOztu*Ajo6I)$kve!G1NBO}`Y106?FZFVaKT~Uxsu>`8~pW#pgBMoVs+=KB!%@W=w)!FhvjuIYb7%#35)0RGAunhUc2&w*4eF_5k$qS$?vB-vs? z_>yh|^}mY6T@hOur{R>^uc^aKWs!8>V$%W-2Nk7Jo@( zhc^r|bCd6(`iiPL-bJSalW!8|+74k-{IuZ08#TtwOx1dUbiXD0Y*Z&fT}T5@k3e_85`a<>-$QO4&=FKA$SH3oa?TQ;_v0FFkdUU5;$ZCQx4ji zTif>sKej>hox0B8g1VpE7+^(VEC}90Xd(Eb40bw51q+%j&=5g9^K`J-!$0le&h|$< zJYE>?-gU0B{NqvLc>7zc5U}{%%uGuHz@MB-pp%FNNj6*UYYg12p)&=$DX6;vBSvt= z5X?Nk@G6?s6x%#ozxuDmV_i~OTK}&!dF{2S^YWU@rg0T>KGV1}WaP_tkdgWM;X|nZ z_jJb^1H&mSbBcuX!1w88j3uOueTL^BrNv~%Vpb#r=W)?&-u?!&NqzT`b^wPkKVCyx zTDXaTg)au1PjHN!w2Dr`wNtB6_?;&}-&fOq*>2Ml5!q z6(-5SNWm9^BiKjx@GXNn7@#v`lKGnKlijrQ|0-tfnm_*^*J&B9sbm!*IDaLjV^)&jZ*=&2{(~_`QT$-Dc6A`yOq^yzO z0dactXcOJXAFXvx@0W5ee{M8VcVriHRM~dc5iH^8AuGUo^5VtMKmmz12n{CtXQRqk z%{UAx8gh!IsTF`njZIC^tjURYEJcj876yO+vOEh1W3rW;dj24m!>oraaB}Fg%FL|d z`6?H-R1}*(AVT8J74feBZuddfszGGz%DVNoxF0j5nk0CK*hei5FB|N#oO{z?V0X>w zn8|EM)3`#K``6#iuiSouSNkrdMfuVR8VvcJ|4RVqpzDi0FNX!z8-Sii`=2FtEb@Y$7apP1ElLo2hb zk9A@b{d(T_XNI}c{>|1XQFS`4khXP>gVOrh;F5`#7l#=M6eVC`>Vi;qOajyFHhkoD zY)LS>{5q$8NS?v{B**knXHug!x9(9DC-T-d>HBe~t&W95tRY#6cQC4OttioOYyD`NJ>V>FKzCk-BVmjD%Rl*do548)$!#bOlDd>>htr(ET#!2 zCIo9N9aKm6RPHrw)4FxP;iGK+>e#isqaP+#`Kl}A(nK>l(`277QoYB~_e)@SG>9(< z^7p>q)>~Uk4Hys>U%M(xrLMGBi05;z*&wlpOa%PVJ;V~pUul1X>#elwgnz{y|6W|G zO2q`)Zu?J@(l7MvXri5Ni3P!ll>EqNZLOwjYSU&p5cSmJPa>gV+oRjHZcQk_d+&Jg z>-46yGZLN(T3WaWe1D$ci)XCisI80>RaKS5ub$3uXmJE_K@g^pTA2I=(?ZFI+9vgN zbXBXDhYx5q!GvK#4DHyTQD0f8KP$x76uxHm+1&&rOfe9MBD29Jw)KcUtBwyLITbrp z_-n7ygbB`#H4z9bwy7-v=f3nf8_u~PM*_#DcUVBWfw~u#9f-y9u?BobLBeyP0+@Co zb7OJNNvQOOv9nM5n5SC^7(!fb=v;SoXyn8`WzCd&LXCUo3_xjWN(v(7fB#;5mX(EC zixcWJcj+c8tIo+Uc;4S>e@pVE4>X`9#JKAZ9RT}Q+c`aauP0x3f+5i;OIc!3+qq^s zg_&|b(eK|e*|#2J0t)6&kPWNqGknneH0wwD!m`OFH`egH61&=4%Cx4H$i5R6;h_iz z+Qck91Qlsu;382pXs@y_NEPzrBA;$xt(oA~k2WBE&(9#8uySnIOa933OlbiRNW2rl z^d~F{6Ug>^_PB8j{-p1q)}b&Ia_CpkPz4Rpb$=YLQWq7yHG<3K@g|SjTRjUe ztnrS(26%+R*=-XT^te>^;H9*U_C$YZY?Siz8mf4y$KPoGW=pAW)hP}5D+5Gg3-so1F1$OFbJPk;N z*eBK;DtQx45#}#sVG7}wQO?Eg^Vl~+5nIqab3up+Bj9LrN{Tq8<@(2*GTiN9H6JoY z&A@(OAd&{Q3|01%uaA{oA>sK2S`6?5e|T>63+atZ6@B?nSV5eIxC%sIv^rRhA)%~j z4ZajpSc#m3OUlLk@}(ekx6Q$W4kFsEa*l_cOvd|xjBz1cAaZ1GByQ53?zpX>uNSkD zP;lVZw$=AMfLrbmRVxQBQ5$btGkoY!t7kteUoH*~JQlVmHA^M`n(7t~*_zvXY;|-F zoa%3h5C6q;8Y(iqMOw7#&c}$pQR4F>vIZ8-dj33Eb&JF-6)VeC;DgwT0whVf{6E# zpc^B{jq|J+%fH#DymxWZ>yfHvX!=-yhG(NNh@-5sYPvH~E&c8FuuXodngp=4cXzz@ zjo7Hl^vQ@}egj-IGnl`Dd&!rH4PEr{_ufDIM2n{U!~|O)$qpPmm>1t8H0EB1n>lYI z(&IzN_5A}`6LPI~GBjYQi6Ha;$mwZI{+LZG(Nl9+)HLs}~_yAH7RbZoNrqXZNy3>1@`^`l>?B z-Fx-`ImLtp$4wY;Jno1N*&%;ZQSum5)22gTzkc~`nVG$F#)HR4s`oa1b#(mluy^M1 zb3vzQLGmT%p?c~I3t={^N>SW5#iXQA+BvqGj`q_# zGH9spFqNC5r#d@NSn#-V+VadJ6NV_C#yGv-g4ItJFPd^;THHiw6QzG+rKZkH@NxeW zo%Jo}@X&ADH_URdE=qnqL9Ov`Mk7&ZO^}3G#27<_glRkTH)h|esOT~D^2`V%r-QFv8S(2~yQ59%bR;Vce>47xGL&AE+QmD$ zJ@Zeq;+tE>OK0EC&)<+9)gC2ZGW}S1cd5lcZZa?(2OWwZXJKEvGl0!MfMqf>(Ts6bt!8;9z5_!^!NJD zQ$%+*R&VSemJwtIJzch(K|(60C|Tg$w6kFkxpn(?>`Yk`VKPMqTgH9AC1a)+k=@A! zARz*R$_y}qm1`?qz-l;l7x04>pUNLl|0S`}l~R~iOjEOD#(o|u?b+nySM}!na?ezg zn)7GQ2&fud@*$l8($e@lkAeA>@MHs<-U^HtqGMwjX!By}HV&BTg)=OKheNfmUc}2w zMa32TIwycMX$ z=ymbg>-|2z%;*)fY*n_8v326Ai+QTnB7I(NR^6F$=UVAUMSVqItSevjlQb2^KfG-Z zzPZyZcIZCTZN=Dt4zaOF<;8jr(+CqX)^b#~5hj?HEgQdlydNJ=@ht!6@U(wg)Z+8Y z#uqNRmZdgm{C>G)#-hP264>)$1V1;U0Z{2S^ z-Va>`q#~f5o$*w@xP^E}FpBPwtii@bb+g1%O1hF$`drybjRzjfgBf7 z%|!G@$Au5-hN)&0Ot{g&aIC-V!@IxvM_EWX&!nfUe-Lea5!naYkT+5jguTs7<8l3% z0;la{mxkH3^@mU{^7t{=QjM{%gbv^=lS35eLq0!ZX~JEx&BC5jixDAqA9mJLZQ*Ud z&c;Sxl%N{#>zhwoB`S}^U@vHBg*vTG8)9gwS;9co9-VAb_ubWU)2FXckk}G(?BORk z($x2PdB&?*2eve$Zt0*1lbFaQ7h;urQBn2o?Y!JIWz7{Tx8(Ru+F?eRAx2)b=rP|| z?2wLg_Uw0K2Z=%YeZ79O)w44-QI`c8nEsul8In7FuW^HIK_3UE@j@HP4uBHP%i>M* zGxP}rNj$5)x*uqY56NT+_jv}zw+P$cZ5ji4^vup_iSPME^dS9KxlfT1Re5vg7bh_H z>rS+6#R)R1ucwP)FUvQ%`}S=ksi`Q6YlyXxeM(ZI+3J;A2w{OscVC804B8l{BQx!_ zu3st<82&bWG#M4V!GC zO|wn!(MulvJ_S}FebVvc*=X{FF>g#x2)b@{g)1l)J$w*3{H-jsL32WxJ!Q%c{;2`G zF+{X$Jp`M&eU6mi3}NSMvYz6SY)jMkgreX#97b6V6-sG@I;@JfzSV+kFeLafa zGKxH`M8JiFl}#v>Kt}7UiqBP8cy&BISNjV0bYGA#vZ$(RPeRga{j-$z&*t(j;vW(L z!76>?M3$iCJ{drW-Iv!b(zzo5;kI?HwI z?pbW*buGF-(hnXeApr`V%8t zVNHYAscCoK`%#G+?hNzOt_v0r@(MF%;6YeSV9AfmN67|9^7#Q@RQNG+c(mEkG-es? zXg{VELtx;{@eFfHB)5PJvlkO_15J$NQn+`N^xy@*zJFisZ98tzF>nJ;jI};kn;H>n zMWKJzhOYZVM@U^bFh88gI8 zyKr$($?Gh{vzh~|TvzJ+D-FG4q1|d`oME^-a>^ue(UtE+=C90XX2C|{ZA14zmlp@W zb@{S%(8F)VE2yhSB#gLiXbi6#<<{0{g`k7!Yugkm8%Q!!(;*!X-KJd0zZ!Tv_SbCq zKttsrp14YwU6h}DSX>7rj@vj`?4Q<^tJ`6}xgL{sEcm3m!%XAY4M@}w;PXS&$a~_~ z4}N7X^e(TazO=PNCEds*OXnl0GQxYP0Ft9u>Mbhz(`ykWy0H9sOstklP!W!(nw3&SX!#EC51ggq63aU zUjpj|05AvNstQ7w8ZVAA%o+n83|@D9>UOGf~6ls3*HIkQB+ITiK%e4fFB#w zCP#LJjihxITWM%S5+IG+_&7KTs-p}wH9brCWNiolc*+{f6C;E%r4t>crO^su4f;#! zHe-J8Khaup2y0%xeH$`-`1?eg6|a_@iSI2`ko#<3yrq1-E9|-8?)>Fg&p$o{q58*+ z_Ex*%UhKRV34Pn~vKDW^GLIcU&Ue%jp07K1*t%o?{Atr;`kWM&?$I2v%ohRk$#{H-#c)4Nv*eysXImE=afOIc5f3WNpW zv>^ix=+~E*JJF>hi5*Vd`gSMBnes-_gW>55TJG%k&1V#wEn9TdXsZo+KIy#eah*A3 zf|u?t#2QY|t}-2UES%BGlr{FBxmTOpI_eF{A^3;Wyn*PmAe|nEEnDd5lxEDh1*Yzz zsc#tB5%EmdRW#zF@F9^s3g$7(4l~ro5YOSm2MMij!8AKW1yY4AuD%hvZf{(iY>+5!#F?t7jUT1Q@_q7~Ui#O1V?C#}x6U0dnk|clFItFQfmZYJ>51*rE%=#~K zC;T3!?*_pdf!T!_ca{CK9e%tK4CWb{rv=8Vd4LWCI`JnVUd5$hJ0iy(o{#1J_hn;K zSptZrviY5r@up*#JYt(G)-mWZWnKRm&$V5Tg)5(Rk5or;b>S%%=L!IOy&iFBnmYRu0VrMZX*7?GEVMfAvC&gnx z%ah;bHKqx&l9IT4i^>Ct-@JPD7Mi_nhv0)rHBQ^7j_@w~@dMa)fiRZ(hiOh>88;Mi zU&+&RgsPdlEwsT#V-SF|RVe`z@bV}WLoE%zwOXnVZfoA225OnOIZvl~nSun7tI~9D z*#!qCme`B-FO!SF*j!Dv2Okn&zhw){Dz(Ap5cEMpy8>&_cE&Fd88jbGoUdrD&%}bT z);PAwBxYHd(UY$=PFv%Kv2UT!PS2{BfKWQ@!$>l&@N(-PlAeHY>O~L}!|jH~_TI0p zy|&-BO`Q)cS1T0{QG0F-)g=07+{~FfX#qjTiFduFW$B&1regDQeC4F=-hk4Iz?NeXzV-7PnqTsZmp-pj`?NB9E1WPYI&IHR;A zw&7xf8p%9C2LONvcj+(5TWhwF6N@LXPvBcq?Gw3){@FFIR<%{1^R3jy9$j_(o6`Q! zUapU2a~r`x@{&mm4=mOTaVs>pzL|_@Ag!&iPKEtvFchpX)Omsg8c(xwj~0YMMVG*r z-xU?HZ>W(o%wyHggjg^6qI&CN;pm|pm};KhKk{Vt1Uku;oiId?>P8nHF$QJ`V1~&W zfC1zEz$1R=OwZ#fCABm+Hw*5AFc~PL?X3k1A3Pech|_sO7VRa^qT11;H$sFG$US_3 z7fMoh{lf6<~qY!Udxvo$oNHViC< zONQJQjG2Hr7<^2vzLBfBG_LT^XCUO#)ZI)I{i!NmJxlK`9vzGm)$&lXs1`$)XU)Gm z&Rb_5nYCD*N1 zR?{u+iloi&-gORJ#Y#3@tm{}vy7HgS{7JdwbZk!ISHZsJTN79(xJdzGAu`_>x9y-AJHpKyfy;R0VDz5PGkP}nf2T6s zId#Gq70R2y=)>u(4LeiLpNf|3NUbXmxuZa6GG+voCnvy*3>n(%)9<~^DuCNT2>-~B z>i=(mpWif$QEY6!^PQ(kk67A~W>+54vMw0gWZXGkbt8}Krn;B_APc&qt-X)A{kS-r zMT@d1YGE;%NnkoT;N;0+oz=)kVGd3Fz)i}5&>_@J1l?8v)RT~atfjdbJYc{S+ELUr z)NXw`&j2etfA*56g{oM{n+2&t_EIz;ocFEJ4id9x@3Dw!V`)sR054iwKivwmcG*N} zT>9@Hhj%0uzD)gkyXw~~%Q-9(W^}^t2xTT|foTIJ zhS0=MpF5ZR`S(0l?CzM-O{n4Sj&FC)dBc7{FaG1vya9Ug#?obmbGK9u6?`S2f-bKP zH;I93W=!zi%`G>m{JFzw56=A_;-eQqo5g>%m0$Eei?V5`?t%q9|M_Q%wB*6ggB_YV zSVY8mi>lC3czyGWsiRV)M7^^5bWqSLJ}hP@91dYuB>~}g=2i*Xf<2(Wu!XH8hNAnd z8AWFSjyqXW^5B1N(*!@gz>_?HlG`B)(XZ826~6-=Bw!Uz*sO{}(epl1stc2uD>PCX zlE3&QvKmgYu9*K8u6Ogdb9NXJ?tc7=td*!Ow-@IB;QlG1otL78xhG*h&)^8JuRGd5 z8&VU{gZB2ckB>OkJ00A@<<(=@=_uIXueuqXF1QCVs(72IO_?Y?VT0m0zo%494keBY z63&Bqro6{WUpIWcz}{_kBj(c~+PEwVGr|O3a^{FfOwZhKH19RLh2Yp%h$8QRhKljx zWX-GiCqXar-5FmFz=O(HF(p>3vtPcv4*kaT2X=Dm*ti41>b`h3K(K5t=f?BF3Y9Z< zd_D~M$R_Tk`=|8gRaLbp{atFl&{Pl1->=$B!t)XXi&TLIJzp-XCYtywncc@Ppku2~ zuDu42V;}HQCK`*P7}F;RIPIomb3&$63Meei!zT4(iXMid6(An;lkBw1 zzehlXo(rPpALpk>yS>0z5Kz~ zU%!4~y=EFW%f7t2Ja5#gg@dG}v+XyZ_)iN^`t+$anWN)2KZ-OOyNQQx$EOE^wJ#na zc26T#HEo5)U(Dh}>U8>Dh83 zec3z>;t8J+6FKqCz0q2rRJ*e-vj?L&JuEFd`X-CPZIntUt_D(@>?waCOpfqSNh5}& zX|#8D5!azo-@_wAUJ}ZAj5aSgl>Gktce;*+h={?I!2wA-H$Su=G!0AdVm1Z9t}BCO zl#%?g{jGt3WZ?hhp{apeI|`$OO;$B0wy`n(?)XOmYZRCXoH((HOL+6zwLtPof3247 znA$K>Q2y#I&j;-d+yXxWr9$^6t>yU2NXm1~$fZx0N%@(?UmB|yVLWVRk5Rr06^2ah z?PL{r^5L6h3#PvlTr$DJTBdeAZ&YT5yz;7kr zA+Fkwma1Mo&D+~>)vBOvH3r57m?kp2QxOH%$+Wno~>5P*BZqAomKN1XcVo$h!$zHy5l-;$!abw5AQX*_hN@`lwW2SH1 zmx_NXr2M`uK5d2Yh=kmC*wjm;g9Rst_YxJ2{u>+A^Hp2_E+VF<^dbNnraw<2tI_{S zTjro0rOB$PztX-)TvWdO-N(v&LoGoNHp=!QW?(>|%>}PsF-vNc%pTf6K&pC2I!fUa zlqOv=*|KMkntyg8QJ8QCHNisB8#h>ziusSANoJP^=@dT`oXi-*UQ@iLx&HgP1-r&y$ z_B1%NXv6qJ*3Ay@Ms*!!nzJ&(Bzl=xVU(|?m*|Ox+(+%vgT^mPxil`JY|&F+#lhZF zUe|v8G3neg4PEox2R@#kyFQ+FVegx(!8I>yoZ5%ls^JI_jK4{$K8X2S!0fE77~)Xk zG6qP1ER8Vs@JcX|(u**P4@lKfkWgNE6=#J{NSvud37GATx$Y2__#v&gvWjv@$CamG zwKseae?w53Q4=8ed|m9nsfU0#1s#BbV#xGPy*hV>A>`?LGjfJm6~-?2@Bs!!`ILHU zVmO<3*OM7>H3 z5{jw3)we-{AxBU^zzfUF*k!RWf-E}!TkMy$ft&aA>9O3hfqWZJ7V_P=aq;z1bMqyl zj)hKq6Rem^Q|oA3UwHjotT4jz$^toYdJB3gMG5ayuYJ#*vte0~rDguSPg81~%Ddft z@*6BhX>Gd3j2Qu{QwVKj$`{f{sLsEXmEor_KnH4?T_tQMTYVKr-I1qWd=)zs&OD9N z-w422PC~_HX+9MO{W$FD`y*}oX1$dr{I>LaW-6Bu3Rq8 zK5cDxc7NHK!i=kd>Feg+TmV{YqJ37He?Qr;j?bq!Jji6s~0hfd9mQW7C$uEiHA&=9-!q7Tu{#=~y^l0OQBHwt0MH z8E6JTxlZ=|Tx*n_xI5YTITdQwI_jP%kNzf|d zR&+B4q(#DW15L`GX{G=VJm)}WgNF?1C#|N0f26OWCW^_bsw!mZj7af?Fst?__%2i+ z%ePxNO)6F%;SqBA=|B#0I-uN=x*%-Kcd z1wA{E4d#Ko0JaP>h!UTFeO~P`>C{3gXX%oX5`sG_(iZwC@8L5~`};3&A5Z5ti=uShzs|HdXKBfp9*L%j}JvKae`C7x20i<>ox5N6OQ5F zp+hO;QeiI8?qz?4Hf*M?|MPwYN0!RMl>g(=A|ML5E*FeB{mYNemQnq=@+m#UBTURp zOv2Ob9C_|Wo_g|OB8V-_k`Ry#D<%%^yNzq@G_;P~@~fg^n5=AWaNreT5f?0wfL#Zv zG!0LsR=~mmxM;!r`4#3R#bk0WtkCX;ToOJ|Y#mZzt#RWPjU7atwhM&>Q8WcHs5+NLSRDaXZGP7<5eV&Gu;sy^mb$*$4jqV}>A{GJxAFsJZF zP;Q}v=jSP-v6o~s&QgMq3&yg+o!wpR9GN})-`hj&!a0Ae^+jTonfaN5DWNhBqBqJR ze}?nb`saosA{X=0&TNHYMxb&l)I3-2=gbS5la>y`8)GFFNzL`PsV>AsVI9;_pL5D+ z6|re7V1N=$F}QvQIlb)uqnTF&ZkpPteYhMy3iwD zg+Y(^t*aAI`F%T5qgFuH{CuFxRCa;PS>&->U^f07BvJ30ah?cDegJrW)i5O^LTH$; z4w`R_`VxB|R`&R$rMcE^TZLm|5o=Yk`ymmwCb+jEZhw}UdGX|ggy`r1Xc>(B!SM1U zP=v@PvJwXPtw$e8aY@NHVRL)hex-wN;cOK}{aGpL;lnjxxN*?Xp#rqV)C)}{IfN0I z^Q^0@N)m8qx=>rp<@m_L@2ynAj{o!b4B2VbfB)j|F|~MyD+xKl+HsrDyjJByLUDeg z7C95TW10cjEuPCddT}%ePJ8zvc`i3)L~#ee$M)?jX-v?ivz3+D&ht*pn8hXzP-U8S zc${=M*ZXE&g%(&JPxjr|&(qLscW@}Zx~^NX$BZp66?mD{14vl7Z^Gyidu?pEqMY=L z*(jl+WdfXF$I0dwWkI8C9*^kXuOIFqcPY)W$+^YkOX_5G^(G?p6P(L%@bj97dr`CV z_wWS&xWYUr^jf=*&Wm z5r*3w=_>C51>`ki^y=53O6B=BP)j5^$h!=(5biKgi1+A&HK(D;FUigQg|eFr@b1-yCVlA1!wcwn|)eVYUANb?E~*JpLOQI9cjh z?d1*y%hnA%k22+P_j(=D(cNShgl$dcm1=;2wXSu3_pF(_khU39Z(%FeMdZi5&%bHR zknaU`XP0D+z&P8pA=hFV_>sMT{G-VoD#=LImrrdz(h*;saH;Hq+RFIAx{prEmw(=c zl~Z~kOX*FkR54B+Z007k!f1&sqIlg?Y*pmNMQO3Wr^nJuM%}ryX4dSF@4~66(8I3- zTIkz>?u>X(7FrRqABgS)N1p?(;Gr;jbVW&gE08qTH~m#CPa_C>N{^HMgF0DD=W58q zuRCYvucMV$p$wWiyx(l;fnMR!7`0KR{&Z6I%|b4Fb1-IS3AcM3(&1)(EiaFjIdB_S z3oWfud^;Mwlt%hz!-SignZ>Mr!=w7DpU&a40>0c|Q~p72u6G66>AP>BDuoV^ew*b{ zm6eDF^El}3%v-?GDEhLQ_YasHO(^O2g6b9%CRBJ9d&xu2o5N)xOr>sEENaFw4DLf( zS{mhzP-Q@K09jzTuctIbi+Ic=7A5dTrv=iwxL^XR{QdbZ$|UBGIfF}Vlsz%;;fxNR z&bgXQr)NB9w%oD6z+pC4Rb50TU#Hg5a&0Qe%EG#JpEyDRVUUrOjXgRu4kWnP!b%i$ zOmO(0IfH-Z&Kc){j&VGljXx!kk1`av!!^FHeA~YxPk9_UV)y2%{K%09#IY>W^N z66-N1-QoZ>1V`^Rd;>xe`83iXa3?Ae#+(w&ZajMa{A5MBb)Quv{lg?l*TL`&o_Ai~0Mt2se_LT*T#`}%H2an}MDJjH( zvaerJaj*u1NiX3m4cnrd0Zi`j|}KLD&zu+2tpaSNq^ws^ZnIN#@Wbg z{qpms^bpWK6$(yl3mBIwT#JlYsU>PC{#y2;i$%56)mJrlZ$)@}LXpcde!O0@Jpr`n zG0BL!Do^w0i?B>W$W23*SO{x0oh~m}K{x5ObYO<*C~IC3-I=}q*khHD);(oi#7B(S z*5TotLmW>{xSC}WR|u#?^Qq_o!ui7XhldX!FHse@m8Q`{bkIp{-h|^aKfs{l{nRq9 zX?#em<^g(Pev3j+sX%f&0Z(qJC52pV%%{2AqNvx-7Zb(r_=Z(Z!llFsKzJZAl zct@{{3A#MCz5xLXMN!hG5_Aw$QBfnCXY#(pu}miNqGg{BI)8S90W62eGhrhS!IO@Z0Nc=IH)*pw(cT=w@dTmKv)W ze?ris=KlC7HlWPdn)J~|P3^Yyt6!u|I~#ASc*fnEFfNCxC}jUBM=2BW+JH-f`)?z2 z;11z(mV8`mf2xCc%lj&zDWk5VA#K23S(}aqFmN@FAdneg=3|a0X`KnCD@{MTp=kAM&FFd~LA5-(`XaAKb#Bx8op9T`I~i2!Q9s6_P9g zo)8w-_BCo1KK%PV^2jlu0m0f^V=^wFbwFo`U~;)&WzPF5s~nl*8yVbfhXOsKys8VEHf{b} z-ZBpuZDhmQnj*#;GymH_c29RHYrRGd4gvRs)$_0(8)*;GWRoqdcY^$pJN=Zo>R=R3 z<|#K|ta1#OQe3emv9DaXkRtC&O_!R{^EcCQzw;_y;Ic2@zh9bN!VzRWVbY|vkJdj5 zRrZa9{)enaL08_O<}&wY@K#ET=z$RKp5DKIcH7HT49rA)AL5U8!+#d;QKyzZC@&9R_JF`y zHkK~r!Gj04jkd_T_-Q{z{!D910BQ#J z`$(O*#LobzJF|Q?J#lZ@DCs>aUPwh2TdE}9Wj4d`Mw9UknR6gWyevfx#40Urn>`(AMqdN~P zq>ni8S|<^PWPBq*`wtwDqm!-wCYkfTRrGRAW=s&ix(wkG$4_@@*7f)8Cz8wo$}h6A zg39ZIP082cfd`UvUwd$3EVwTH)I`t}Fe4iz4&)No971GX;{sY0(-2#R~M9P1{gY4>OF~@b(^_(6tj(ZaB=ZAx#D_;`_nt&{xJY za9W=po<5)k96yef??BvScw>I+7`#77p>+Z7^A|1_)TU_Zdrsdm{RKsfv(fQN*G9-A z;G;mGc#(9M(#VhP*^`BLIrzI6#3>dm8-8_IIX@MFBVth3R z4)&nc(fFaK;z`or1ivek4l!sNeQvq_TJ*JQ&c(Mle!TxG^ioOsA9H&I?wI<^p+V<6 zoFm-L2fDA#@eIbrhAgKv-KROC#^RtS~gdPC-2KOE)}!>ZNe z5(=u9ZIPR3n0UD{HA5)fW|c0wawqR~!f}b?#7W_2zWA-x@yQ$<)+s3aJtZod?XdA$ z7CVJP%X>H~Q6_l{FMx*59`5c8v!5lg%D2w5r?WLr?QLPdadvmv#sHYpBl^;d$Ff3L zK0faFFBIyPwZzmK!>)B-`V_5tzjKrPm9T^baYR?Ran{1z5A_s}YiInKTZ)oxJtgr?%^ z>jF*V0!`;Isqk-rv)nPwo~<#*!0xNsim*9{+H*u^VZxAOW#B)FusrKt3nZhimy^#}q3^#R$P z!;e^7!fLCs)n-rcImc)2>$}|6cEhLV)1U!!U|mT~HJ1n7Vb+eh>*%lEzqF+-D40hK zgN3Jbk?pfmtYU8o2Rq4t#8Ikua#%KclAJJsbaT77e9vEhWs-Mijk6z%gjvH(d%)bN zd<`LI)~mZQERqZGt&-<1YXC20h7up|Loy;_X03~#Y;bX3i* zx_r|`B(v?M0b213a1q(Fn99ZC1A5ry)dO~ee#0(lNwZq&j&R}^tz#e1lTrIVL%~?&pen`hQ6kE<_pGrHE~)Rb*SBSBZP#` zrfokp=xPp6kR1@9{^IK7lqQ}jtG5YuQIf78S&b4(2hG)}&*))uq+X}FSkv6;g3GHM zaRQ2INN5t#8pPt(zSHZ*>QZU&kd@xM<{6+DBcD&NZ>$t-koLhE)L$~8QsG1EkIFdo zSRxLB*8Ag2t-n?J(|Q5YM>kRW0A!4%VvHxPqD9S4(i)|8Oyq-M|I@GhKmE`iI*mfO zNM7OndZ);!WI{WSKpJwbwYKz@oWFR{PUsr{^JQ_)2Tv8tTIRvLORJRt0tSfRE#she zROoy!w92?crG?!;-zYBVKOcJj{EGknP;rz0d|9flwwDvXNJg{Q7{MR>zxmMQWc&a6 zP~XfKHupJBG}cNN)U}T5DmmAJCrK~e=GRNE;?k9*m#)!9{HINs^eKCHhZ7+Am$)N? zfB)ob9?d`BE4|G+DdkpXpY-wn^Pz42@Rl-FL%aX)K6l;aB{>S*jeS??z4i4W8!H$r z?y^toMfIb}ZREp$JXj*Vl&jro#n9+|3^$MLDBJFQ)kt}Hc|6OKfKIX6f)+nwCslfs z?2>f%%PXUP>WZK9R*=>x*Rx!Bk|7YuriPptHPBaa?EYT&1M%koWo4#$vg?3)vppNm~0Q%AwmvwQbxfgG8` zd(6g9Yk52JI^a5N!%s1LmdHY03@K~4pr8nsI!+BScKPA@7Hgi;k};b`vw^f_7{8pUap?_f7B#30Ji&I9Bd0LuQ~65X%Te&s1fgu>(Qi zxMDadTrzLE53d*Z{F>hu(Feq;7v)8lw4! z-Zi(5IVT)ban4W5tAG7@%W9M3s=X5$e{~ku!((4m>fX9pbLwhqh3WMo@*C1WYL8vL z7>k8?k1R&|aHxe$=FCx?wC3pY{(y@J-yZM(Bl86V57NGrcH;2Kj1r5%{;xD2QFN8{ z6Jv5oZdqI^z9l#T>FLQ#4hPl?p^I!PU-{}))I2qH8q8*gmyDsnbGNY>q;E#I5_l*w z1_cD&Gm^7_EPGSjmsSY*j<>xusCjSYycObJU`@R67M`)}K5*dNdknm1TD7N0nycw6 z!Le5C(c>kp)52kohpZYdP(qBE$%ysK} zd!DK3Zwd+&P~~@<#)a(5%`3FoP*>=bv>>jsu2B%^a3p5Z6@*OQvrS#-+yXZUH^+|k zM~m?|VcwK%Z?W{u8?W5e_I>Ewb62n(u*a_Lj7$0e!xVR( z$RtJpe){sobJ1%fv%_TmjQUK=9LVQ0BE>lCsGp(Qk#YU$Ed8xwmazq^v2WbbgLpQ% zHL4g<=LmfqJO!D3e}|qBJim9g8{h-^-Tu_hLsbZ+R+n5XD^Um1sP z9ELPbVf^#2D8~rH)8IJZ?zC>R)gWtb1Mq=kb4o=-5>j&fomXZ{Cs*bU*3_KGpx%m# z;NlHqNg+P*zjYuS$JC67iX zFG;ySWbC=?n+x32Yg5W&s*bl=(OkUh>D8<4%g@$*UFh+(|02&K_nm(NMI22{ZC`HE z6u&G&^-Gvle34U_DXmetsbr`_n(QyEVFrR!fi|JsIendY%~ z4NsXjmb^WMAHeVqKC~dJ4M$DY-g5SA-s6hKZ7<{ZAdOPhLjhCR071KEJY+7w9$f z=NUL*kN#{oZ|J6bvoi|SCtUX&dS#8fPK$Vo79S?XnMM6R`bzrLOt*}z`1p9mAO2fy zlM7bu%U`Q${8;tKf;QJjmi>IaIy$d!Z285F8xco;J>>rFR&)E?=dg8PaO^CqEX`0ffhtBgTF58lKYn!m6drVC#%S5j?eM!DihJ{|<@-wJfrLP4} zwEq6rxoPaE++P@79JQXppMzvm*>?+|ljf$4T(S{TeIsRV|8q}WY5r!FugLQp*863(9Wq!sxpj0qk0PVbrT7`n#2ik1pi zv762sGHfrp;M|4x@M>XbJbILv+&C`e%+;$$lX4$BC4t%;&aUKUz2RNp<6q?2z_+zH zWcJy^=s1&H#U4Yg>doelK5_Eout9^aHR#K2@{BltejKp!CY`lh$S*@K7OU`!}#&(0@O)m#xl? z$ai4$$g2(yXo!-KY|{CTaF{WwH}bCW44ZJ%I)+vB(6@2`@F=~+jpU3LC5-r^p*3;9B#u?_=i5waHZK0E z`Hx48-hZ6>{$KyoJH;-mhs4%qAG|F?!&jfTh%(^L!>il_`p*M*#*cERbe}zY56{LY zGr!Nh%32HHXz6JkyH66B=t+N-*1)V`rynm=#xE8!JbhY^*$6^l_6u`+KfmRv!{UjRYqR0|~QWdK@f_G(A&!GQ~vyp8W6F^n#Nc?PQ$W=(U` znSyFu)QLj+L;ROll3XI8Ls3ksto-MM+3MdF#_G~#sa*Fv-NjuyLGKm<5Tw1oo71#I zQvLMlQOUU1oSX@sq(fM3BBkd@_$0cNy(3 zN0oNk$6W;5v%rH{TD#IOf_iV6#95P|2=a~p&CK0EJl*rM>G zQ#R8E`PS6bzFj+L8NvgO?AcUi z2{7~+kJQ6pInQ!)M-LftuJ)IFjX}mVIJ8p?I2fjp1df`r>~7SGs9*fd`6D zI!oa5RD0hUe=_TGNJADiFW@R4496DT2Jp?SdxcJ-=Yk*yI*OhNE};U{JcL5Hk3zPl1y?lrJ1s0JJyVp38jsj})|-ZRO# z?(5eBzP_hpV+U8FQ3T{v-hLl~;m8eUDJox-^Ek&@5}L;4S2pL}zAa(mZ}slbTj1$L z2ekBEr5)FcD8k1C6=+U{m_xJb&|#jAC$H(^<@(uJF525GFA_{GIv0zU!I*@c#I9Hn zM`GMUwe1jEHc)3tbO9bih$hb~&Re*UX>Xi51)7X5?GA+#Udg-)<&&&z zUOD%GD479QtGlHXZfNCJ#l)y&Ry5MY`cz*(tnE$F_4x7WU*=`VFUN%j&kUzOiF13v zD3;zcrh0Z&0WtR^d3SQ&UZr?iMyB_T*)yiib9M|B*2c_?)UTl!kGIY^E~)0(BBKWv zIT&%xFN%p;Ef$G%&Uf$bcwQUIHSFsG&E|@%o^?R32* z)esglb-2F+lN+*7B5_xDr@chc;ku76(sO_@%Nrt#MJt~-ksB3!SxMxCRC>GJ=mbit zX^wXDu~@Ri=pNIgQy9w~DuKjw`@q1tozaL~TJnKg4fZXvMEUfPkPJ7eCZLMIN~@Mb zul78#zM^9Z>k+Q*tj-XgxQD)-p6mvt-@uH5=GlW+;C4akXx9ke8P#chx%Flo@>Q|E z`*m{iic}Vs04bPlhNv^s=t*|=TVlA~R)M6Vf;WC(s<1IQkjby0`$qxtQyac)ND2 z1@ZI3sAJZ0#>ivNxoOixi+sgw;ujNG0g~#oHY{I0I4Ii#RYt4^PARUxy5J|lqg38W zs6{|G=*|M8g)?T{1m&warY8i>@Ij0Mag5liecVVHiU3D{)6n~L|0%il7bHfYYNrnowq zOcYwdva!QqFeVZW?1~vMO{j@04BZ?q*i6tPDn6XSemE1yud0CQ_`5b6k7{xaSYU46 zgXIsQkvD=w?a#;WDZhUT-To<4-ewzn zWRlAbS@;@%MZ+QfTxUq6$}tmMNKaa4$xd?j80?dYPx{2aWHT<)2*P6_cHW$2q1UzQ z4m|pP8FCM#y_0i!HtA1~Hrc@d6cg3gtvhl2y8?DhBt-C4=p1{+UD&G0F9!`YX1YDy zdaIN*{q@a=sHAa;jd^k>$OULgJ@PVe(|RU~KDynCCVdWZYfyv3HD2y)%h{7+5Te$MOwXlm4n@Oe+(T$lT`wl-3Q_ZM^Nk|o)9#+=}@9CJJ~`ul^RY!2~1xO8Ss z<#v&YHtmtivCX?YmN4+Rs7TR7hSG>Ez3;y0omrKx&2mG+^QcD1F~$UiIfvi8bBAVF z{GtoHuAX`9?z;QYsIWYto{reN*N}sO6H4Dq-Pt~E^q+ZEVcY8HBhy?wNHJcT$Xw8D zyKyy_=l>b0VzKt8SIhTuv_XVM;b%mF3l<)^?4eQJ;yMU6%nKK*7%PN>2Q{$7MAb*v zI^Usd*xXP@&)l`Y^wld)>|fmOk)V@e&8rnPVeVAO(y%j+xL z*T!`QM*ZDgb3={p<=T|TlK3N{L#5p6f-khWgsYgUiSB`NCq@|`$9s+B{AVRr4-Fmi zi}i;1Q~&H3#aNXm;H&WehxiAt3>O0;_&vDxH*ILs5DE(kI%i$(LtzuibLB*T@Aw7(=Oc#0d%l z@T~gxK*0SrVcGaBCw?c@`J94_=}%8)Z2OxOF_)|Y zl#np1rzZx#<7!Xhw!Cikc-ike#s#tV;ThD_IK?k8{Cn+}?pN_WH0Km6cGUL@evUn- zyRqglraY>#kKNh35vC4--{r_g*b|G>-5b4r)`inod0bfNpVraCkQY_^LuO8hXWiSH z8uUH16o8(mbqjTe>_-{wUTm}c(j2ItAQk~@bXID3-@bX1ROu&Lsz)u&ft9Y8r$-D@ zN?#BcfBN*0%BJ}@+#nV~wZ$O8H`X z0l9;n!L&d|SdYkPC$C>!x+c&=C~SqV1mane@}?Vv(W)>euZJSNGkE~hkHLrI9ny~@ zvH^tBH)EYr3h=%LSE7X&lB@YHfPOFTl*r{JkuF*^pP^S%K%#qgRa(aKSP+Ncr5QHQ z-Ie;9#@6ZXA(|Owy}K(aT75jHDcS4RX6wm0q~;3kRDI`|n2;+a!^>%CNIG{;bdFRX zC-jiSA;O||8$NTln^ym=54$!TlGQ~jN#bYsmJty-_wLm^h-kavTv&VNiQ&!uBd?<& zfvRKY&gZf2s;#B3YhN@1$B+RAV&%S*vncc}0j(fRLjoUa) zS$x`mKG^6LKfqIUB5G@xin*G6M8;oG9cmOVdeKd1} z3hQ$dQuOgc3vJ3@H5I3&MiYFiq&IM;^f} zVB^{=`w!Wh%v|{h=Nb9FK+^9AkIn4bG)z@B3)e;(D4)GJ4Kj)U166wbG|Xq9Z4*o&e2PKU>DhC-1;}9ty>U{(g~uD z(&&@Woit<>nn1`3Q(+eY@nb-eb#Y+D{v;B$W7=CEW@kIo1Uv~@sbqK>%lC>MUrNOb8lE`BA?Yzyp%=F zw4PQE1S7WOBd{Wi@PThuV$6wgDBOFVwGv!5_Co=1{y7Y#VM2Q`&zpq5xjsNh3<(9( zr{5qvyR`RkeOokICtMc~n`W6g%6;=ty02S@7Fc&%eN0%G($*R6j0?z2gpE9r0Vllo zRaL8ME)=2eSdK_lsI@pIdiUrN8E)YLY6K3*YqUz+mSn0j%;IKjp%VrLc@UhT9FbFt zmlY79R7et`@>g*(X(m0mqrt&U?sjK0nExb2hXmi!T;77N#0~8SGt%xj+%*hqH?=C~IhZqNuD`zp|-Qq0!?ESg>%wmhj-P zD5-F#RsK$ga@2WA9U&f|<-6pdWw%ZEbgIEeI><^xh++`d1A&N>xP#j-KVuo;Bm3k(`vY za^g?rL)n!)^qIUsVw7-tL*(oqdx3M4{sfsHx_KBFcatVTNTVap%a~(i#C+!pBoAGy zipM!(Lx0L#ma(E&`(c3u%0rotITFTDOe|)Q8a*L&;CPRHrOzb#!GFo=*l1QrA{~W! z9>*f5E65X?YH{9+~8O!7y$>XhQb9>0_A-Lychj9_&yWdXZ50HVT5GoR5VHs}|5LbM8$p^8}gs~?AOG;Qwo%84FIMv*pkOiS{O!4qH$U%&h zOOu>~Fq`2e@zhm(dvyGj&7gz)oC=$oOP488&0WnU)Mdmp{1zzxckbGS6o1dYL3DGT zZ7#>~a0{9dik`3H<=Y#~m_bYY-P6k!V}jQ5eL2JJAC|!YLRiQheQx~0QR$yHgUAI} zSWFwD=gcYi5!0+#LD?Y%CB@pZeLI_an(o^~+QMGtX#(CAf7I=iM+CM0RVGwU%H!Z) z-v61r;_#2R`2WZM^lpdQ_O-X7Rs|!053s?@6bb_7c3G}=b|(pIBh^OA`+~8b7e22H z0DbxbLdB1v$cEr85}KSp$k8PrxDU=grnQkSa6-(PLMQn5a_9T??yY=ePS_M}nJu#Y zLM6g>s%CMb%`^s*Xa8)1(TH-m1@-|eJ-7dCE24z-9v(a} zMU5F0#9~Z0i!zw7d5g>^#dWV0o*P$u{HPw3omETBQAgVjVf*de3QV9`?N^z9HM(~m zq9kAk#WM_YI!-Jk8&^;$ZX>LvA8{NMV7Gk!DAS8ry__B*(L4-bH)Zl<7Dey9t4MQ^ zmpCPc>J7s9WgC3x@NnxcGup`{;4F773=NCULv23)A`!; zCl0?DiAi-nvPuSl@Gv+ynau|&+IiKgJ5_bID^>vYgV3N2sIzH!qUn(`YA8wFv1&c?_0*K{!D zWCu7v+<<@2{sB{ci+j?t97d49NA2KB#PD!^i6L0#Hlz2Z&Vbloi4F~=mcY>{?fG7q zQ{c4sL&p0&8i)!IxI!3v5f`v(NJwu|V>xru`ZYQnGnqtI6FZOWZp@w;=JV#Eid4j9Ihpf{Wi3EL2YrG-{ljV^e}6V;CukI-LJKRI!x{Vmo56F!=Ewm_RTv zf>toS@h8B}*X8cf7v%ma7P3ygLUsfEwfeU3mDd~rpNEKaF#7@rWd^h)A&(=glh@au zInz4T%@H2$u&rfOS7_j9&CZg1+3oA=x^ZKFy1U|Rni`>O2Bm})2atOW4yGq(cy(8h z3H}u>p^b9akI#o}*i(JS-ki#PZXiPA7au?7Rn={1VYJuDf@-u6N_7lyUWQF8vIKHX z)F%cm(Ejuc5xwV^KlxGfi%9k%A)v<74GSDbmNPv9b6bI$ysh~&7>A>=(0Lq}K@cLQh zMR$+Hl3Z_JF$@;(-t`CCKLC@@{6!NNxyTsK&D-w3h3Dzg+78NY#yWKAk|i|KStkxT zfiimIA--MH0<~a%Mg0aHCKej}^g*`EujFvYlQaTrER^${b-9Xyi1rG;1W9E0Ks}DJ z^1Cg+k<0TIDa?70u9u&(y~!gai)`D=4273?O^Xl4M{RY*^4f);K7S6OV#Lq*qSbo> zwO>2xp?_tQgQsM?Y-AD^6yf)b%O$blT} zmAXEB;r+Bu@<+CPj}|BDY<-g%XQ$iz`9A>h CvK^`b literal 0 HcmV?d00001 diff --git a/reachability/predicates.json b/reachability/predicates.json index b0c8f82..3dff282 100644 --- a/reachability/predicates.json +++ b/reachability/predicates.json @@ -124,6 +124,14 @@ "halfspaces": [ { "row": [[8, -0.4587], [9, 0.9587], [10, -0.5000]], "rhs_expr": "0.01389" } ] + }, + "prompt_critical_margin_heatup": { + "meaning": "Total reactivity stays safely below prompt-critical; keeps the prompt-jump PJ reduction valid. Per-mode specialization: for heatup with feedback linearization, rho_total = Kp*(T_ref(t) - T_c). Requiring rho <= 0.5*beta gives T_c >= T_ref - (beta - 0.5*beta)/Kp = T_ref - 32.5. Since T_ref increases monotonically from T_standby up to T_c0, the worst case is at the ramp end: T_c >= T_c0 - 32.5 = 275.85 C. Approximate as a constant halfspace with the worst-case T_ref.", + "concretization": "T_c >= 275.85 (ensures rho <= 0.5*beta under heatup FL controller)", + "halfspaces": [ + { "state_index": 9, "coeff": -1.0, "rhs_expr": "-275.85" } + ], + "_note": "This is a controller-specific specialization. If the controller or its gain change, recompute. For LQR operation and constant-u scram the margin is trivially satisfied (much larger)." } }, @@ -138,9 +146,10 @@ "fuel_centerline", "cold_leg_subcooled", "heatup_rate_upper", - "heatup_rate_lower" + "heatup_rate_lower", + "prompt_critical_margin_heatup" ], - "_note": "dT_c/dt is linear in (T_f, T_c, T_cold), so ramp-rate halfspace has 3 nonzero coefficients per row. DNBR not modeled — would need an augmented correlation-based predicate." + "_note": "dT_c/dt is linear in (T_f, T_c, T_cold), so ramp-rate halfspace has 3 nonzero coefficients per row. prompt_critical_margin_heatup proves the PJ reduction's validity condition (beta - rho > 0 with margin) as part of the safety obligation rather than as an unverified premise. DNBR not modeled — would need an augmented correlation-based predicate." }, "inv2_holds": { "meaning": "Operation mode safety envelope.",