From dd1156d61a310033b6e3d0978089fca4897bb491 Mon Sep 17 00:00:00 2001 From: Jake Ginesin Date: Thu, 12 Mar 2026 03:32:06 -0400 Subject: [PATCH] moar --- tests/paper3.yaml | 122 ++++++++ tests/tcp/no-network/tcp-phi1.pml | 149 ++++++++++ tests/tcp/no-network/tcp-phi2.pml | 149 ++++++++++ tests/tcp/no-network/tcp-phi2.pml.trail | 55 ++++ tests/tcp/no-network/tcp-phi3.pml | 167 +++++++++++ tests/tcp/no-network/tcp-phi4.pml | 156 ++++++++++ tests/tcp/no-network/tcp-phi4.pml.trail | 43 +++ tests/tcp/no-network/tcp-phi5.pml | 158 +++++++++++ tests/tcp/no-network/tcp-phi6.pml | 154 ++++++++++ tests/tcp/no-network/tcp.pml | 144 ++++++++++ tests/tcp/pan | Bin 114744 -> 115048 bytes tests/tcp/tcp-phi1.pml | 14 +- tests/tcp/tcp-phi2.pml | 14 +- tests/tcp/tcp-phi2.pml.trail | 104 ++++--- tests/tcp/tcp-phi3.pml | 14 +- tests/tcp/tcp-phi3.pml.trail | 62 ++++ tests/tcp/tcp-phi4.pml | 14 +- tests/tcp/tcp-phi4.pml.trail | 363 +++++++++++++++++++++--- tests/tcp/tcp-phi5.pml | 14 +- tests/tcp/tcp-phi5.pml.trail | 86 ++++++ tests/tcp/tcp-phi6.pml | 14 +- tests/tcp/tcp-phi6.pml.trail | 122 ++++++++ tests/tcp/tcp.pml | 14 +- 23 files changed, 1967 insertions(+), 165 deletions(-) create mode 100644 tests/paper3.yaml create mode 100644 tests/tcp/no-network/tcp-phi1.pml create mode 100644 tests/tcp/no-network/tcp-phi2.pml create mode 100644 tests/tcp/no-network/tcp-phi2.pml.trail create mode 100644 tests/tcp/no-network/tcp-phi3.pml create mode 100644 tests/tcp/no-network/tcp-phi4.pml create mode 100644 tests/tcp/no-network/tcp-phi4.pml.trail create mode 100644 tests/tcp/no-network/tcp-phi5.pml create mode 100644 tests/tcp/no-network/tcp-phi6.pml create mode 100644 tests/tcp/no-network/tcp.pml create mode 100644 tests/tcp/tcp-phi3.pml.trail create mode 100644 tests/tcp/tcp-phi5.pml.trail create mode 100644 tests/tcp/tcp-phi6.pml.trail diff --git a/tests/paper3.yaml b/tests/paper3.yaml new file mode 100644 index 0000000..76f4cbb --- /dev/null +++ b/tests/paper3.yaml @@ -0,0 +1,122 @@ +unidirectional-drop-abp: + - command: python src/main.py --model=tests/abp/abp.pml --attacker=drop --chan=AtoB --output=temp.pml --eval --cleanup --mem=1 + - intended: no violation + - explanation: abp resists drop, see https://en.wikipedia.org/wiki/Alternating_bit_protocol + +bidirectional-drop-abp: + - command: python src/main.py --model=tests/abp/abp.pml --attacker=drop --chan=AtoB,BtoA --output=temp.pml --eval --cleanup --mem=1 + - intended: no violation + - explanation: abp resists drop, see https://en.wikipedia.org/wiki/Alternating_bit_protocol + +# ============================================================================= +# TCP - shared channel model (AtoB, BtoA) +# +# A sends on AtoB, B reads AtoB. B sends on BtoA, A reads BtoA. +# Korg attackers directly interpose on the shared channel. +# ============================================================================= + +# phi1: safety - half-open prevention +# always (leftClosed implies !rightEstablished) +# Expected: holds. B reaching Established requires A's ACK, which means +# A was also in Established. A cannot reach Closed from Established +# without a full teardown that also moves B out of Established. + +tcp-phi1-drop-AtoB: + - command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=drop --chan=AtoB --output=temp.pml --eval --cleanup --mem=1 + - intended: no violation + - explanation: dropping A's messages prevents B from reaching Established; no half-open possible + +tcp-phi1-drop-bidirectional: + - command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=drop --chan=AtoB,BtoA --output=temp.pml --eval --cleanup --mem=1 + - intended: no violation + - explanation: dropping on both channels prevents any handshake completion; neither side reaches Established + +tcp-phi1-replay-AtoB: + - command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=replay --chan=AtoB --output=temp.pml --eval --cleanup --mem=1 + - intended: no violation + - explanation: replaying A's messages cannot create half-open; B reaching Established still requires valid handshake, and A cannot close without teardown + +tcp-phi1-replay-bidirectional: + - command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=replay --chan=AtoB,BtoA --output=temp.pml --eval --cleanup --mem=1 + - intended: no violation + - explanation: replay on both channels still cannot violate the structural invariant; A must pass through Established before reaching Closed + +tcp-phi1-reorder-bidirectional: + - command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=reorder --chan=AtoB,BtoA --output=temp.pml --eval --cleanup --mem=2 + - intended: no violation + - explanation: reordering cannot bypass the handshake dependency; half-open prevention holds structurally + +# phi3: liveness - no infinite stalls/deadlocks +# neither side stuck forever in a non-terminal state +# Expected: drop on both channels can strand both sides post-Established +# (e.g., both in FinWait1 after FINs are dropped) + +tcp-phi3-drop-AtoB: + - command: python src/main.py --model=tests/tcp/tcp-phi3.pml --attacker=drop --chan=AtoB --output=temp.pml --eval --cleanup --mem=1 + - intended: acceptance cycle + - explanation: handshake completes via nondeterministic pass; then attacker drops A's FIN, stranding both sides in post-Established states with no timeout recovery + +tcp-phi3-drop-bidirectional: + - command: python src/main.py --model=tests/tcp/tcp-phi3.pml --attacker=drop --chan=AtoB,BtoA --output=temp.pml --eval --cleanup --mem=1 + - intended: acceptance cycle + - explanation: attackers let handshake through, then drop FINs on both channels; both sides stuck in FinWait1 or similar permanently + +tcp-phi3-replay-AtoB: + - command: python src/main.py --model=tests/tcp/tcp-phi3.pml --attacker=replay --chan=AtoB --output=temp.pml --eval --cleanup --mem=1 + - intended: acceptance cycle + - explanation: replay attacker can consume A's FIN and never replay it, effectively dropping it; B stays in Established, A stuck in FinWait1 + +tcp-phi3-reorder-bidirectional: + - command: python src/main.py --model=tests/tcp/tcp-phi3.pml --attacker=reorder --chan=AtoB,BtoA --output=temp.pml --eval --cleanup --mem=2 + - intended: acceptance cycle + - explanation: reorder attacker consumes teardown messages and delays them indefinitely, stranding both sides + +# phi5: liveness - SYN_RECEIVED resolution +# SynReceived implies eventually (Established or FinWait1 or Closed) +# Expected: drop on AtoB traps A in SynReceived (no timeout modeled) + +tcp-phi5-drop-AtoB: + - command: python src/main.py --model=tests/tcp/tcp-phi5.pml --attacker=drop --chan=AtoB --output=temp.pml --eval --cleanup --mem=1 + - intended: acceptance cycle + - explanation: A goes to Listen, B's SYN arrives via BtoA, A enters SynReceived and sends SYN+ACK on AtoB; attacker drops it; B never completes handshake, A stuck in SynReceived permanently (no timeout in model) + +tcp-phi5-drop-BtoA: + - command: python src/main.py --model=tests/tcp/tcp-phi5.pml --attacker=drop --chan=BtoA --output=temp.pml --eval --cleanup --mem=1 + - intended: acceptance cycle + - explanation: B sends SYN on BtoA, attacker drops it; but A can also initiate — if A goes Listen and B goes SynSent, A needs B's SYN which is dropped; however A can enter SynReceived via simultaneous open path and get stuck + +tcp-phi5-drop-bidirectional: + - command: python src/main.py --model=tests/tcp/tcp-phi5.pml --attacker=drop --chan=AtoB,BtoA --output=temp.pml --eval --cleanup --mem=1 + - intended: acceptance cycle + - explanation: dropping on both channels after SynReceived is entered prevents any ACK from arriving to resolve it + +tcp-phi5-replay-AtoB: + - command: python src/main.py --model=tests/tcp/tcp-phi5.pml --attacker=replay --chan=AtoB --output=temp.pml --eval --cleanup --mem=1 + - intended: acceptance cycle + - explanation: replay attacker consumes A's SYN+ACK and never replays it (terminates with empty mem), effectively a drop; A stuck in SynReceived + +tcp-phi5-reorder-AtoB: + - command: python src/main.py --model=tests/tcp/tcp-phi5.pml --attacker=reorder --chan=AtoB --output=temp.pml --eval --cleanup --mem=2 + - intended: acceptance cycle + - explanation: reorder attacker consumes A's SYN+ACK during the handshake; even if replayed later, the ordering disruption can prevent SynReceived resolution + +# phi6: safety - strict closing transitions +# Closing implies next(Closing or Closed) +# Expected: violated even without attacker. Closing transitions to +# TimeWait on ACK (not Closed), and TimeWaitState is neither +# ClosingState nor ClosedState. + +tcp-phi6-drop-AtoB: + - command: python src/main.py --model=tests/tcp/tcp-phi6.pml --attacker=drop --chan=AtoB --output=temp.pml --eval --cleanup --mem=1 + - intended: property violation + - explanation: base model already violates phi6; simultaneous close leads to Closing, then ACK transitions to TimeWait which is not Closing or Closed; attacker goes to BREAK, preserving the pre-existing violation + +tcp-phi6-replay-AtoB: + - command: python src/main.py --model=tests/tcp/tcp-phi6.pml --attacker=replay --chan=AtoB --output=temp.pml --eval --cleanup --mem=1 + - intended: property violation + - explanation: same base-model violation; Closing -> TimeWait is always reachable once simultaneous close occurs + +tcp-phi6-reorder-bidirectional: + - command: python src/main.py --model=tests/tcp/tcp-phi6.pml --attacker=reorder --chan=AtoB,BtoA --output=temp.pml --eval --cleanup --mem=2 + - intended: property violation + - explanation: same base-model violation; attacker presence does not affect the Closing -> TimeWait transition path diff --git a/tests/tcp/no-network/tcp-phi1.pml b/tests/tcp/no-network/tcp-phi1.pml new file mode 100644 index 0000000..243cfd0 --- /dev/null +++ b/tests/tcp/no-network/tcp-phi1.pml @@ -0,0 +1,149 @@ +// models: phi1, phi2, phi3, phi5 +// does not model: phi4, phi7 +// not yet implemented: phi6 +mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } + +chan AtoN = [2] of { mtype }; +chan NtoA = [2] of { mtype }; +chan BtoN = [2] of { mtype }; +chan NtoB = [2] of { mtype }; + +int state[2]; +int pids[2]; + +#define ClosedState 0 +#define ListenState 1 +#define SynSentState 2 +#define SynRecState 3 +#define EstState 4 +#define FinW1State 5 +#define CloseWaitState 6 +#define FinW2State 7 +#define ClosingState 8 +#define LastAckState 9 +#define TimeWaitState 10 +#define EndState -1 + +#define leftConnecting (state[0] == ListenState && state[1] == SynSentState) +#define leftEstablished (state[0] == EstState) +#define rightEstablished (state[1] == EstState) +#define leftClosed (state[0] == ClosedState) + +proctype TCP(chan snd, rcv; int i) { + pids[i] = _pid; +CLOSED: + state[i] = ClosedState; + do + /* Passive open */ + :: goto LISTEN; + /* Active open */ + :: snd ! SYN; goto SYN_SENT; + /* Terminate */ + :: goto end; + od +LISTEN: + state[i] = ListenState; + do + :: rcv ? SYN -> + atomic { + snd ! SYN; + snd ! ACK; + goto SYN_RECEIVED; + } + /* Simultaneous LISTEN */ + :: rcv ? _ -> skip; + :: timeout -> goto CLOSED; + od +SYN_SENT: + state[i] = SynSentState; + do + :: rcv ? SYN; + if + /* Standard behavior */ + :: rcv ? ACK -> snd ! ACK; goto ESTABLISHED; + /* Simultaneous open */ + :: snd ! ACK; goto SYN_RECEIVED; + fi + :: rcv ? ACK; + do + :: rcv ? SYN -> + snd ! ACK; + goto ESTABLISHED; + :: rcv ? _ -> skip; + od + :: rcv ? _ -> skip; + :: timeout -> goto CLOSED; /* Timeout */ + od +SYN_RECEIVED: + state[i] = SynRecState; + do + :: rcv ? ACK -> goto ESTABLISHED; + :: rcv ? _ -> skip; + od + /* We may want to consider putting a timeout -> CLOSED here. */ +ESTABLISHED: + state[i] = EstState; + do + /* Close - initiator sequence */ + :: snd ! FIN; goto FIN_WAIT_1; + /* Close - responder sequence */ + :: rcv ? FIN -> + snd ! ACK; + goto CLOSE_WAIT; + :: rcv ? _ -> skip; + od +FIN_WAIT_1: + state[i] = FinW1State; + do + /* Simultaneous close */ + :: rcv ? FIN -> + snd ! ACK; + goto CLOSING; + /* Standard close */ + :: rcv ? ACK -> goto FIN_WAIT_2; + :: rcv ? _ -> skip; + od +CLOSE_WAIT: + state[i] = CloseWaitState; + do + :: snd ! FIN; goto LAST_ACK; + :: rcv ? _ -> skip; + od +FIN_WAIT_2: + state[i] = FinW2State; + do + :: rcv ? FIN -> + snd ! ACK; + goto TIME_WAIT; + :: rcv ? _ -> skip; + od +CLOSING: + state[i] = ClosingState; + do + :: rcv ? ACK -> goto TIME_WAIT; + :: rcv ? _ -> skip; + od +LAST_ACK: + state[i] = LastAckState; + do + :: rcv ? ACK -> goto CLOSED; + :: rcv ? _ -> skip; + od +TIME_WAIT: + state[i] = TimeWaitState; + goto CLOSED; +end: + state[i] = EndState; +} + +init { + state[0] = ClosedState; + state[1] = ClosedState; + run TCP(AtoN, NtoA, 0); + run TCP(BtoN, NtoB, 1); +} + +/* safety: half-open prevention */ +ltl phi1 { + always ( leftClosed implies !rightEstablished ) +} diff --git a/tests/tcp/no-network/tcp-phi2.pml b/tests/tcp/no-network/tcp-phi2.pml new file mode 100644 index 0000000..960a173 --- /dev/null +++ b/tests/tcp/no-network/tcp-phi2.pml @@ -0,0 +1,149 @@ +// models: phi1, phi2, phi3, phi5 +// does not model: phi4, phi7 +// not yet implemented: phi6 +mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } + +chan AtoN = [2] of { mtype }; +chan NtoA = [2] of { mtype }; +chan BtoN = [2] of { mtype }; +chan NtoB = [2] of { mtype }; + +int state[2]; +int pids[2]; + +#define ClosedState 0 +#define ListenState 1 +#define SynSentState 2 +#define SynRecState 3 +#define EstState 4 +#define FinW1State 5 +#define CloseWaitState 6 +#define FinW2State 7 +#define ClosingState 8 +#define LastAckState 9 +#define TimeWaitState 10 +#define EndState -1 + +#define leftConnecting (state[0] == ListenState && state[1] == SynSentState) +#define leftEstablished (state[0] == EstState) +#define rightEstablished (state[1] == EstState) +#define leftClosed (state[0] == ClosedState) + +proctype TCP(chan snd, rcv; int i) { + pids[i] = _pid; +CLOSED: + state[i] = ClosedState; + do + /* Passive open */ + :: goto LISTEN; + /* Active open */ + :: snd ! SYN; goto SYN_SENT; + /* Terminate */ + :: goto end; + od +LISTEN: + state[i] = ListenState; + do + :: rcv ? SYN -> + atomic { + snd ! SYN; + snd ! ACK; + goto SYN_RECEIVED; + } + /* Simultaneous LISTEN */ + :: rcv ? _ -> skip; + :: timeout -> goto CLOSED; + od +SYN_SENT: + state[i] = SynSentState; + do + :: rcv ? SYN; + if + /* Standard behavior */ + :: rcv ? ACK -> snd ! ACK; goto ESTABLISHED; + /* Simultaneous open */ + :: snd ! ACK; goto SYN_RECEIVED; + fi + :: rcv ? ACK; + do + :: rcv ? SYN -> + snd ! ACK; + goto ESTABLISHED; + :: rcv ? _ -> skip; + od + :: rcv ? _ -> skip; + :: timeout -> goto CLOSED; /* Timeout */ + od +SYN_RECEIVED: + state[i] = SynRecState; + do + :: rcv ? ACK -> goto ESTABLISHED; + :: rcv ? _ -> skip; + od + /* We may want to consider putting a timeout -> CLOSED here. */ +ESTABLISHED: + state[i] = EstState; + do + /* Close - initiator sequence */ + :: snd ! FIN; goto FIN_WAIT_1; + /* Close - responder sequence */ + :: rcv ? FIN -> + snd ! ACK; + goto CLOSE_WAIT; + :: rcv ? _ -> skip; + od +FIN_WAIT_1: + state[i] = FinW1State; + do + /* Simultaneous close */ + :: rcv ? FIN -> + snd ! ACK; + goto CLOSING; + /* Standard close */ + :: rcv ? ACK -> goto FIN_WAIT_2; + :: rcv ? _ -> skip; + od +CLOSE_WAIT: + state[i] = CloseWaitState; + do + :: snd ! FIN; goto LAST_ACK; + :: rcv ? _ -> skip; + od +FIN_WAIT_2: + state[i] = FinW2State; + do + :: rcv ? FIN -> + snd ! ACK; + goto TIME_WAIT; + :: rcv ? _ -> skip; + od +CLOSING: + state[i] = ClosingState; + do + :: rcv ? ACK -> goto TIME_WAIT; + :: rcv ? _ -> skip; + od +LAST_ACK: + state[i] = LastAckState; + do + :: rcv ? ACK -> goto CLOSED; + :: rcv ? _ -> skip; + od +TIME_WAIT: + state[i] = TimeWaitState; + goto CLOSED; +end: + state[i] = EndState; +} + +init { + state[0] = ClosedState; + state[1] = ClosedState; + run TCP(AtoN, NtoA, 0); + run TCP(BtoN, NtoB, 1); +} + +/* liveness: verifying connection establishment */ +ltl phi2 { + ( (always ( eventually ( state[0] == 1 && state[1] == 2 ) ) ) + implies ( eventually ( state[0] == 4 ) ) ) diff --git a/tests/tcp/no-network/tcp-phi2.pml.trail b/tests/tcp/no-network/tcp-phi2.pml.trail new file mode 100644 index 0000000..319ff39 --- /dev/null +++ b/tests/tcp/no-network/tcp-phi2.pml.trail @@ -0,0 +1,55 @@ +-2:2:-2 +-4:-4:-4 +1:0:121 +2:1:114 +3:0:121 +4:1:115 +5:0:121 +6:1:116 +7:0:121 +8:1:117 +9:0:121 +10:3:0 +11:0:121 +12:3:1 +13:0:121 +14:3:2 +15:0:121 +16:3:9 +17:0:121 +18:2:0 +19:0:121 +20:2:1 +21:0:121 +22:2:2 +23:0:121 +24:2:9 +25:0:121 +26:3:17 +27:0:121 +28:3:1 +29:0:121 +30:3:3 +31:0:121 +32:3:22 +33:0:119 +34:2:17 +35:0:126 +36:2:1 +37:0:121 +38:2:3 +39:0:121 +40:2:22 +41:0:121 +42:2:42 +43:0:121 +44:2:1 +-1:-1:-1 +45:0:121 +46:2:2 +47:0:121 +48:2:9 +49:0:119 +50:2:17 +51:0:126 +52:2:1 diff --git a/tests/tcp/no-network/tcp-phi3.pml b/tests/tcp/no-network/tcp-phi3.pml new file mode 100644 index 0000000..35a9049 --- /dev/null +++ b/tests/tcp/no-network/tcp-phi3.pml @@ -0,0 +1,167 @@ +// models: phi1, phi2, phi3, phi5 +// does not model: phi4, phi7 +// not yet implemented: phi6 +mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } + +chan AtoN = [2] of { mtype }; +chan NtoA = [2] of { mtype }; +chan BtoN = [2] of { mtype }; +chan NtoB = [2] of { mtype }; + +int state[2]; +int pids[2]; + +#define ClosedState 0 +#define ListenState 1 +#define SynSentState 2 +#define SynRecState 3 +#define EstState 4 +#define FinW1State 5 +#define CloseWaitState 6 +#define FinW2State 7 +#define ClosingState 8 +#define LastAckState 9 +#define TimeWaitState 10 +#define EndState -1 + +#define leftConnecting (state[0] == ListenState && state[1] == SynSentState) +#define leftEstablished (state[0] == EstState) +#define rightEstablished (state[1] == EstState) +#define leftClosed (state[0] == ClosedState) + +proctype TCP(chan snd, rcv; int i) { + pids[i] = _pid; +CLOSED: + state[i] = ClosedState; + do + /* Passive open */ + :: goto LISTEN; + /* Active open */ + :: snd ! SYN; goto SYN_SENT; + /* Terminate */ + :: goto end; + od +LISTEN: + state[i] = ListenState; + do + :: rcv ? SYN -> + atomic { + snd ! SYN; + snd ! ACK; + goto SYN_RECEIVED; + } + /* Simultaneous LISTEN */ + :: rcv ? _ -> skip; + :: timeout -> goto CLOSED; + od +SYN_SENT: + state[i] = SynSentState; + do + :: rcv ? SYN; + if + /* Standard behavior */ + :: rcv ? ACK -> snd ! ACK; goto ESTABLISHED; + /* Simultaneous open */ + :: snd ! ACK; goto SYN_RECEIVED; + fi + :: rcv ? ACK; + do + :: rcv ? SYN -> + snd ! ACK; + goto ESTABLISHED; + :: rcv ? _ -> skip; + od + :: rcv ? _ -> skip; + :: timeout -> goto CLOSED; /* Timeout */ + od +SYN_RECEIVED: + state[i] = SynRecState; + do + :: rcv ? ACK -> goto ESTABLISHED; + :: rcv ? _ -> skip; + od + /* We may want to consider putting a timeout -> CLOSED here. */ +ESTABLISHED: + state[i] = EstState; + do + /* Close - initiator sequence */ + :: snd ! FIN; goto FIN_WAIT_1; + /* Close - responder sequence */ + :: rcv ? FIN -> + snd ! ACK; + goto CLOSE_WAIT; + :: rcv ? _ -> skip; + od +FIN_WAIT_1: + state[i] = FinW1State; + do + /* Simultaneous close */ + :: rcv ? FIN -> + snd ! ACK; + goto CLOSING; + /* Standard close */ + :: rcv ? ACK -> goto FIN_WAIT_2; + :: rcv ? _ -> skip; + od +CLOSE_WAIT: + state[i] = CloseWaitState; + do + :: snd ! FIN; goto LAST_ACK; + :: rcv ? _ -> skip; + od +FIN_WAIT_2: + state[i] = FinW2State; + do + :: rcv ? FIN -> + snd ! ACK; + goto TIME_WAIT; + :: rcv ? _ -> skip; + od +CLOSING: + state[i] = ClosingState; + do + :: rcv ? ACK -> goto TIME_WAIT; + :: rcv ? _ -> skip; + od +LAST_ACK: + state[i] = LastAckState; + do + :: rcv ? ACK -> goto CLOSED; + :: rcv ? _ -> skip; + od +TIME_WAIT: + state[i] = TimeWaitState; + goto CLOSED; +end: + state[i] = EndState; +} + +init { + state[0] = ClosedState; + state[1] = ClosedState; + run TCP(AtoN, NtoA, 0); + run TCP(BtoN, NtoB, 1); +} + +/* liveness: no infinite stalls/deadlocks */ +ltl phi3 { + !(eventually (((always (state[0] == SynSentState)) || + (always (state[0] == SynRecState)) || + (always (state[0] == EstState)) || + (always (state[0] == FinW1State)) || + (always (state[0] == CloseWaitState)) || + (always (state[0] == FinW2State)) || + (always (state[0] == ClosingState)) || + (always (state[0] == LastAckState)) || + (always (state[0] == TimeWaitState))) + && + ((always (state[1] == SynSentState)) || + (always (state[1] == SynRecState)) || + (always (state[1] == EstState)) || + (always (state[1] == FinW1State)) || + (always (state[1] == CloseWaitState)) || + (always (state[1] == FinW2State)) || + (always (state[1] == ClosingState)) || + (always (state[1] == LastAckState)) || + (always (state[1] == TimeWaitState))))) +} diff --git a/tests/tcp/no-network/tcp-phi4.pml b/tests/tcp/no-network/tcp-phi4.pml new file mode 100644 index 0000000..68c2d48 --- /dev/null +++ b/tests/tcp/no-network/tcp-phi4.pml @@ -0,0 +1,156 @@ +// models: phi1, phi2, phi3, phi5 +// does not model: phi4, phi7 +// not yet implemented: phi6 +mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } + +chan AtoN = [2] of { mtype }; +chan NtoA = [2] of { mtype }; +chan BtoN = [2] of { mtype }; +chan NtoB = [2] of { mtype }; + +int state[2]; +int pids[2]; + +#define ClosedState 0 +#define ListenState 1 +#define SynSentState 2 +#define SynRecState 3 +#define EstState 4 +#define FinW1State 5 +#define CloseWaitState 6 +#define FinW2State 7 +#define ClosingState 8 +#define LastAckState 9 +#define TimeWaitState 10 +#define EndState -1 + +#define leftConnecting (state[0] == ListenState && state[1] == SynSentState) +#define leftEstablished (state[0] == EstState) +#define rightEstablished (state[1] == EstState) +#define leftClosed (state[0] == ClosedState) + +proctype TCP(chan snd, rcv; int i) { + pids[i] = _pid; +CLOSED: + state[i] = ClosedState; + do + /* Passive open */ + :: goto LISTEN; + /* Active open */ + :: snd ! SYN; goto SYN_SENT; + /* Terminate */ + :: goto end; + od +LISTEN: + state[i] = ListenState; + do + :: rcv ? SYN -> + atomic { + snd ! SYN; + snd ! ACK; + goto SYN_RECEIVED; + } + /* Simultaneous LISTEN */ + :: rcv ? _ -> skip; + :: timeout -> goto CLOSED; + od +SYN_SENT: + state[i] = SynSentState; + do + :: rcv ? SYN; + if + /* Standard behavior */ + :: rcv ? ACK -> snd ! ACK; goto ESTABLISHED; + /* Simultaneous open */ + :: snd ! ACK; goto SYN_RECEIVED; + fi + :: rcv ? ACK; + do + :: rcv ? SYN -> + snd ! ACK; + goto ESTABLISHED; + :: rcv ? _ -> skip; + od + :: rcv ? _ -> skip; + :: timeout -> goto CLOSED; /* Timeout */ + od +SYN_RECEIVED: + state[i] = SynRecState; + do + :: rcv ? ACK -> goto ESTABLISHED; + :: rcv ? _ -> skip; + od + /* We may want to consider putting a timeout -> CLOSED here. */ +ESTABLISHED: + state[i] = EstState; + do + /* Close - initiator sequence */ + :: snd ! FIN; goto FIN_WAIT_1; + /* Close - responder sequence */ + :: rcv ? FIN -> + snd ! ACK; + goto CLOSE_WAIT; + :: rcv ? _ -> skip; + od +FIN_WAIT_1: + state[i] = FinW1State; + do + /* Simultaneous close */ + :: rcv ? FIN -> + snd ! ACK; + goto CLOSING; + /* Standard close */ + :: rcv ? ACK -> goto FIN_WAIT_2; + :: rcv ? _ -> skip; + od +CLOSE_WAIT: + state[i] = CloseWaitState; + do + :: snd ! FIN; goto LAST_ACK; + :: rcv ? _ -> skip; + od +FIN_WAIT_2: + state[i] = FinW2State; + do + :: rcv ? FIN -> + snd ! ACK; + goto TIME_WAIT; + :: rcv ? _ -> skip; + od +CLOSING: + state[i] = ClosingState; + do + :: rcv ? ACK -> goto TIME_WAIT; + :: rcv ? _ -> skip; + od +LAST_ACK: + state[i] = LastAckState; + do + :: rcv ? ACK -> goto CLOSED; + :: rcv ? _ -> skip; + od +TIME_WAIT: + state[i] = TimeWaitState; + goto CLOSED; +end: + state[i] = EndState; +} + +init { + state[0] = ClosedState; + state[1] = ClosedState; + run TCP(AtoN, NtoA, 0); + run TCP(BtoN, NtoB, 1); +} + +/* liveness: simultanous open */ +ltl phi4 { + always ( + (state[0] == SynSentState && + state[1] == SynSentState) + + implies + + ((eventually state[0] == EstState) && + (eventually state[1] == EstState))) +} diff --git a/tests/tcp/no-network/tcp-phi4.pml.trail b/tests/tcp/no-network/tcp-phi4.pml.trail new file mode 100644 index 0000000..08508a0 --- /dev/null +++ b/tests/tcp/no-network/tcp-phi4.pml.trail @@ -0,0 +1,43 @@ +-2:2:-2 +-4:-4:-4 +1:0:122 +2:1:114 +3:0:122 +4:1:115 +5:0:122 +6:1:116 +7:0:122 +8:1:117 +9:0:122 +10:3:0 +11:0:122 +12:3:1 +13:0:122 +14:3:2 +15:0:122 +16:3:9 +17:0:122 +18:2:0 +19:0:122 +20:2:1 +21:0:122 +22:2:2 +23:0:122 +24:2:9 +25:0:122 +26:3:17 +27:0:122 +28:3:1 +29:0:122 +30:3:3 +31:0:122 +32:3:22 +33:0:122 +34:2:17 +35:0:122 +36:2:1 +37:0:122 +38:2:3 +39:0:122 +40:2:22 +41:0:119 diff --git a/tests/tcp/no-network/tcp-phi5.pml b/tests/tcp/no-network/tcp-phi5.pml new file mode 100644 index 0000000..417ac59 --- /dev/null +++ b/tests/tcp/no-network/tcp-phi5.pml @@ -0,0 +1,158 @@ +// models: phi1, phi2, phi3, phi5 +// does not model: phi4, phi7 +// not yet implemented: phi6 +mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } + +chan AtoN = [2] of { mtype }; +chan NtoA = [2] of { mtype }; +chan BtoN = [2] of { mtype }; +chan NtoB = [2] of { mtype }; + +int state[2]; +int pids[2]; + +#define ClosedState 0 +#define ListenState 1 +#define SynSentState 2 +#define SynRecState 3 +#define EstState 4 +#define FinW1State 5 +#define CloseWaitState 6 +#define FinW2State 7 +#define ClosingState 8 +#define LastAckState 9 +#define TimeWaitState 10 +#define EndState -1 + +#define leftConnecting (state[0] == ListenState && state[1] == SynSentState) +#define leftEstablished (state[0] == EstState) +#define rightEstablished (state[1] == EstState) +#define leftClosed (state[0] == ClosedState) + +proctype TCP(chan snd, rcv; int i) { + pids[i] = _pid; +CLOSED: + state[i] = ClosedState; + do + /* Passive open */ + :: goto LISTEN; + /* Active open */ + :: snd ! SYN; goto SYN_SENT; + /* Terminate */ + :: goto end; + od +LISTEN: + state[i] = ListenState; + do + :: rcv ? SYN -> + atomic { + snd ! SYN; + snd ! ACK; + goto SYN_RECEIVED; + } + /* Simultaneous LISTEN */ + :: rcv ? _ -> skip; + :: timeout -> goto CLOSED; + od +SYN_SENT: + state[i] = SynSentState; + do + :: rcv ? SYN; + if + /* Standard behavior */ + :: rcv ? ACK -> snd ! ACK; goto ESTABLISHED; + /* Simultaneous open */ + :: snd ! ACK; goto SYN_RECEIVED; + fi + :: rcv ? ACK; + do + :: rcv ? SYN -> + snd ! ACK; + goto ESTABLISHED; + :: rcv ? _ -> skip; + od + :: rcv ? _ -> skip; + :: timeout -> goto CLOSED; /* Timeout */ + od +SYN_RECEIVED: + state[i] = SynRecState; + do + :: rcv ? ACK -> goto ESTABLISHED; + :: rcv ? _ -> skip; + od + /* We may want to consider putting a timeout -> CLOSED here. */ +ESTABLISHED: + state[i] = EstState; + do + /* Close - initiator sequence */ + :: snd ! FIN; goto FIN_WAIT_1; + /* Close - responder sequence */ + :: rcv ? FIN -> + snd ! ACK; + goto CLOSE_WAIT; + :: rcv ? _ -> skip; + od +FIN_WAIT_1: + state[i] = FinW1State; + do + /* Simultaneous close */ + :: rcv ? FIN -> + snd ! ACK; + goto CLOSING; + /* Standard close */ + :: rcv ? ACK -> goto FIN_WAIT_2; + :: rcv ? _ -> skip; + od +CLOSE_WAIT: + state[i] = CloseWaitState; + do + :: snd ! FIN; goto LAST_ACK; + :: rcv ? _ -> skip; + od +FIN_WAIT_2: + state[i] = FinW2State; + do + :: rcv ? FIN -> + snd ! ACK; + goto TIME_WAIT; + :: rcv ? _ -> skip; + od +CLOSING: + state[i] = ClosingState; + do + :: rcv ? ACK -> goto TIME_WAIT; + :: rcv ? _ -> skip; + od +LAST_ACK: + state[i] = LastAckState; + do + :: rcv ? ACK -> goto CLOSED; + :: rcv ? _ -> skip; + od +TIME_WAIT: + state[i] = TimeWaitState; + goto CLOSED; +end: + state[i] = EndState; +} + +init { + state[0] = ClosedState; + state[1] = ClosedState; + run TCP(AtoN, NtoA, 0); + run TCP(BtoN, NtoB, 1); +} + +/* liveness: SYN_RECEIVED resolution*/ +ltl phi5 { + always ( + (state[0] == SynRecState) + implies ( + eventually ( + (state[0] == EstState || + state[0] == FinW1State || + state[0] == ClosedState) + ) + ) + ) +} diff --git a/tests/tcp/no-network/tcp-phi6.pml b/tests/tcp/no-network/tcp-phi6.pml new file mode 100644 index 0000000..2cf306a --- /dev/null +++ b/tests/tcp/no-network/tcp-phi6.pml @@ -0,0 +1,154 @@ +// models: phi1, phi2, phi3, phi5 +// does not model: phi4, phi7 +// not yet implemented: phi6 +mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } + +chan AtoN = [2] of { mtype }; +chan NtoA = [2] of { mtype }; +chan BtoN = [2] of { mtype }; +chan NtoB = [2] of { mtype }; + +int state[2]; +int pids[2]; + +#define ClosedState 0 +#define ListenState 1 +#define SynSentState 2 +#define SynRecState 3 +#define EstState 4 +#define FinW1State 5 +#define CloseWaitState 6 +#define FinW2State 7 +#define ClosingState 8 +#define LastAckState 9 +#define TimeWaitState 10 +#define EndState -1 + +#define leftConnecting (state[0] == ListenState && state[1] == SynSentState) +#define leftEstablished (state[0] == EstState) +#define rightEstablished (state[1] == EstState) +#define leftClosed (state[0] == ClosedState) + +proctype TCP(chan snd, rcv; int i) { + pids[i] = _pid; +CLOSED: + state[i] = ClosedState; + do + /* Passive open */ + :: goto LISTEN; + /* Active open */ + :: snd ! SYN; goto SYN_SENT; + /* Terminate */ + :: goto end; + od +LISTEN: + state[i] = ListenState; + do + :: rcv ? SYN -> + atomic { + snd ! SYN; + snd ! ACK; + goto SYN_RECEIVED; + } + /* Simultaneous LISTEN */ + :: rcv ? _ -> skip; + :: timeout -> goto CLOSED; + od +SYN_SENT: + state[i] = SynSentState; + do + :: rcv ? SYN; + if + /* Standard behavior */ + :: rcv ? ACK -> snd ! ACK; goto ESTABLISHED; + /* Simultaneous open */ + :: snd ! ACK; goto SYN_RECEIVED; + fi + :: rcv ? ACK; + do + :: rcv ? SYN -> + snd ! ACK; + goto ESTABLISHED; + :: rcv ? _ -> skip; + od + :: rcv ? _ -> skip; + :: timeout -> goto CLOSED; /* Timeout */ + od +SYN_RECEIVED: + state[i] = SynRecState; + do + :: rcv ? ACK -> goto ESTABLISHED; + :: rcv ? _ -> skip; + od + /* We may want to consider putting a timeout -> CLOSED here. */ +ESTABLISHED: + state[i] = EstState; + do + /* Close - initiator sequence */ + :: snd ! FIN; goto FIN_WAIT_1; + /* Close - responder sequence */ + :: rcv ? FIN -> + snd ! ACK; + goto CLOSE_WAIT; + :: rcv ? _ -> skip; + od +FIN_WAIT_1: + state[i] = FinW1State; + do + /* Simultaneous close */ + :: rcv ? FIN -> + snd ! ACK; + goto CLOSING; + /* Standard close */ + :: rcv ? ACK -> goto FIN_WAIT_2; + :: rcv ? _ -> skip; + od +CLOSE_WAIT: + state[i] = CloseWaitState; + do + :: snd ! FIN; goto LAST_ACK; + :: rcv ? _ -> skip; + od +FIN_WAIT_2: + state[i] = FinW2State; + do + :: rcv ? FIN -> + snd ! ACK; + goto TIME_WAIT; + :: rcv ? _ -> skip; + od +CLOSING: + state[i] = ClosingState; + do + :: rcv ? ACK -> goto TIME_WAIT; + :: rcv ? _ -> skip; + od +LAST_ACK: + state[i] = LastAckState; + do + :: rcv ? ACK -> goto CLOSED; + :: rcv ? _ -> skip; + od +TIME_WAIT: + state[i] = TimeWaitState; + goto CLOSED; +end: + state[i] = EndState; +} + +init { + state[0] = ClosedState; + state[1] = ClosedState; + run TCP(AtoN, NtoA, 0); + run TCP(BtoN, NtoB, 1); +} + +/* safety: strict closing transitions */ +ltl phi6 { + always ( + (state[0] == ClosingState) + implies + (next (state[0] == ClosingState || + state[0] == ClosedState)) + ) +} diff --git a/tests/tcp/no-network/tcp.pml b/tests/tcp/no-network/tcp.pml new file mode 100644 index 0000000..4e39675 --- /dev/null +++ b/tests/tcp/no-network/tcp.pml @@ -0,0 +1,144 @@ +// models: phi1, phi2, phi3, phi5 +// does not model: phi4, phi7 +// not yet implemented: phi6 +mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } + +chan AtoN = [2] of { mtype }; +chan NtoA = [2] of { mtype }; +chan BtoN = [2] of { mtype }; +chan NtoB = [2] of { mtype }; + +int state[2]; +int pids[2]; + +#define ClosedState 0 +#define ListenState 1 +#define SynSentState 2 +#define SynRecState 3 +#define EstState 4 +#define FinW1State 5 +#define CloseWaitState 6 +#define FinW2State 7 +#define ClosingState 8 +#define LastAckState 9 +#define TimeWaitState 10 +#define EndState -1 + +#define leftConnecting (state[0] == ListenState && state[1] == SynSentState) +#define leftEstablished (state[0] == EstState) +#define rightEstablished (state[1] == EstState) +#define leftClosed (state[0] == ClosedState) + +proctype TCP(chan snd, rcv; int i) { + pids[i] = _pid; +CLOSED: + state[i] = ClosedState; + do + /* Passive open */ + :: goto LISTEN; + /* Active open */ + :: snd ! SYN; goto SYN_SENT; + /* Terminate */ + :: goto end; + od +LISTEN: + state[i] = ListenState; + do + :: rcv ? SYN -> + atomic { + snd ! SYN; + snd ! ACK; + goto SYN_RECEIVED; + } + /* Simultaneous LISTEN */ + :: rcv ? _ -> skip; + :: timeout -> goto CLOSED; + od +SYN_SENT: + state[i] = SynSentState; + do + :: rcv ? SYN; + if + /* Standard behavior */ + :: rcv ? ACK -> snd ! ACK; goto ESTABLISHED; + /* Simultaneous open */ + :: snd ! ACK; goto SYN_RECEIVED; + fi + :: rcv ? ACK; + do + :: rcv ? SYN -> + snd ! ACK; + goto ESTABLISHED; + :: rcv ? _ -> skip; + od + :: rcv ? _ -> skip; + :: timeout -> goto CLOSED; /* Timeout */ + od +SYN_RECEIVED: + state[i] = SynRecState; + do + :: rcv ? ACK -> goto ESTABLISHED; + :: rcv ? _ -> skip; + od + /* We may want to consider putting a timeout -> CLOSED here. */ +ESTABLISHED: + state[i] = EstState; + do + /* Close - initiator sequence */ + :: snd ! FIN; goto FIN_WAIT_1; + /* Close - responder sequence */ + :: rcv ? FIN -> + snd ! ACK; + goto CLOSE_WAIT; + :: rcv ? _ -> skip; + od +FIN_WAIT_1: + state[i] = FinW1State; + do + /* Simultaneous close */ + :: rcv ? FIN -> + snd ! ACK; + goto CLOSING; + /* Standard close */ + :: rcv ? ACK -> goto FIN_WAIT_2; + :: rcv ? _ -> skip; + od +CLOSE_WAIT: + state[i] = CloseWaitState; + do + :: snd ! FIN; goto LAST_ACK; + :: rcv ? _ -> skip; + od +FIN_WAIT_2: + state[i] = FinW2State; + do + :: rcv ? FIN -> + snd ! ACK; + goto TIME_WAIT; + :: rcv ? _ -> skip; + od +CLOSING: + state[i] = ClosingState; + do + :: rcv ? ACK -> goto TIME_WAIT; + :: rcv ? _ -> skip; + od +LAST_ACK: + state[i] = LastAckState; + do + :: rcv ? ACK -> goto CLOSED; + :: rcv ? _ -> skip; + od +TIME_WAIT: + state[i] = TimeWaitState; + goto CLOSED; +end: + state[i] = EndState; +} + +init { + state[0] = ClosedState; + state[1] = ClosedState; + run TCP(AtoN, NtoA, 0); + run TCP(BtoN, NtoB, 1); +} diff --git a/tests/tcp/pan b/tests/tcp/pan index 7f43cf263f13847cb8ce3081baea76e0eb9e619d..8d793e184112496130c107237e4ec007f5329cff 100755 GIT binary patch literal 115048 zcmce<3w#ts);`>m%s_y|4wpzo!32UP2$*n_D5EnZ(GE^Da?vPqi31T70bv5si5`F*Q_xt_> z>8?6edA z#4_VA7|*7;g7@?&1mYLG$8fI@jXU8MYT*l`Z19oaMmHg!T|@U^>U6hgVf<#(eEdH1 zE*>*@7lb4hPE?Y$Z5j`6n^wr^!F!#^yn^7??i!B7Bb+du?|VfW9Qd!KXIh~XoyyB4l%=gk^6Z|?l!l3^ud z#|#@YYWU&>!$&Y3Q(j1}TW*`e(hHVZ5`2U4mxjNq@Yf4}eep-XSbh@*X!iu%JIc-# zpbx@dZ!I3BMLe&>Uq6kOsNI9N%ith+2I4P8BgWz02Y=o0mxRCn%`a%@q`RvPfUcU` zSl*Wy!n+&XzFv?u7oIPUy!wpk$d}$g~cwXuy|47{8>WLf`zl^Q^fhshZfR(k#o)>Vd3mWixw;r7SFwZe&IYG z3O;}>ri*hM{ zI%5XqcE(~?;Ud?JhYIJ;7nT%hIb8h6V&?)RcZ(x;eAbK+!$<0_j8VGtI^8v5_-Nt( zeOGtA5jtk>{JD?L9bGtQ-Xn7!E-6{MBxBK%`RStzM~t59EL`;Pu=}0PVb={GIXoS` zBRa{s_aPhiKeS-JmW>%yx>4G{Xx$a0gx@Kq`FG=3SSa-eX4WSJ#}U2f&P5kz5#mvA zi1zeTe?xa+7W!%azAQXi7_9k=`^`mH7$sZ_KmFQf6tX)&te;{YT+SNk)JF$@LHngX z(%3f!?U(4(KLvk@GdX|iJGCTPP?CX8eO>UEYM>kY!*l~ZIQAmUSOY!SZxh{Spi|z0 zKgmERnS#H313g$bDXhRir!hqEH`72j_WN@TbZSF`zl8>Ra12CYB?dZ;Rf4}#1Kl{r zs4&ojHb9uQ20D!`g1>bJy0P6`Z=eUqScG}aK&Nq2@VCK0H;!eh4D{d_k1%xxx^bMg z#XzUFIQVNZ(1YVU3fpU-)3_=4Yc^4a! zqTM#olMVEE1D(d7!C#_*J}5}UJ;^{1j#Vi*)j%I?h@WntUuB?6?qe~M$MWwxk_D-} z&J`7Ck=&bN8il~<7eNXPei>KsN*i3{pF>DrYXHB&{~$kANnZ=||AqWi6@7Kg{{;D| z3i>uM|6}B*s^?qJ{Ew2Ks+?~v^DiPlRW)BJ^FKg-s$#x{%zq#GscQLVGXFi~rz+*k zXa0%gr>f+$G5-YeQx)>1Gyizf!;n12ZQY3S{1y9mPI zf#jzu<7;L9e&naB;%j04UgW1L;;Uo+?&PPc;oHFcQRJs8;akuA=knpFrqQ>S`A?Fc zs)nzW`HzyHs)TPL^B*KXRR!Nn=HEwtssg@z=HE$vGJT(o`L~guOx~By{0-zMQ}-n? ze+~J`#C`G1|1SB-w0#2ezfOKKXM-W z$z**S;LkXoEAN;t$pH zLFdpT#6bw+ORZ1ci_8@Fog&GH)fLEalVv3+rfH3g|0&#TLeX&X$}$oJNy&$&`DMF& z((XPOZI^$t*Z&%oQ@(Y@ZFa9c;P7UzHcRraVx`?w-x?!U_B6Ga+QiC-qw9~rcSn?I zPyLY|^2v;b`qp^4DPxc1t~bkV^=c1OlOwafxS5zp-es%JcK5j`*IZnqUE^>yx&Gws z^9u=(u}3~xf7D_+DYw+OnloDDhWevDO%3F`jQhHnTI4!Owq!OY3yorBU(+73@-9>T z!5EH-7b}-W)gS4V0V(7?^(T6m_V`~CE4z}MOHGi|)C7rIdt}f}?P+TAm$Oj0ss2cJ zBJNO4O}_ciRJQl#uH~n*#oQ)){n_X|XB_}%udG-5d;4^8AMBde;?0k7IJf0ep4?}< zEX~Pv*O??|lVm#UKG${W7>kk)rR4cX<26JLIiWwCG6Nkqd{sL#p>( z@C$J_%8;kur8jX>Cx0ByW@I4|bC>pp)%VS`&rK zO;Y`d7zqXn2*T4q`U%RrDgxD4%4lGyJ(AplN@tNWz!DO2M)iOUk}`gRW+fTCw)3Pi4FiHUlF<=i3NXb#!u^I|_1}~Va0YasS+;5RQahqRG7AQh8*ogU)@ zYGX4S^#yNI`Ds@l>O+;5o^~`~hu=p^)PZWzrc7cTtbAUQe?d39*G)efFjm zJ(QSU1lj_{2wkh4>44!ESUI@fh#T6RjlnC3{CDW*+MStzDGn^FplnD%nY zT6TXkWj(vUpR$47KT4^?y*WE2hPrRuW7Bb$yk#k^bO-Zz$(x;$M6N{1J2@prk}pag z>)tz)1vTr}K!9mpTD6Hp`~Oo!xAkWvDHO+rCn#V1Ka$;Jy^;if;%p$`ue9G~ztcX& zKA9N;RJsf~EDyMn(DOm>0agqr-=gN{3`Sn6NwNlDU`zT)9@2$-Q|i=d_IvHq?9=Tt z8f!}z777eeP0vD-eCCw&26N&rd0Z)p3dK-MPX_{a1-cS)o0}*V`^V(*(bXXz^rZvr z-i#J_Guk|}!J$dy=1fWdCGp_2b@a8&y1j`=Ms?C(o+P16hkoHG)A;pv%F@6=x z9zzbAq6LT7X<~(#op#nPH%se~(;kwAU}R-5uoIHptls%cARty|nZ_*_%MPLme?pA%IS64r(RdR#T2KEe66!l?ZX(powfqrc&d1Q^1wAvdYO72FJ zD@m-p!B!Sgn z)k~47kL`#>xiL%L0u;=*60CRmsX(CA`UB!(Nau;`0v2AoNw!=7rF^US+<*zl zgM6^IcdA`bl0MgJm--{qRYJ_o$%1^sK))Y!xe;boAp>7a0A&oIyrkwLO?fYxDH5Bi zZDXl*Hc23s#iPbS_8;*Gpv!&_q6cLc%jua#lfC|=7T~)FM2E*xlFOy+5iVser14Eb zl-l7;9Y3gF0+}msB4td+2&vS11PP)!^H?m9!z%^Kx2~Ln?&E5WVMMmiLLz&UIb}Hd zj@X=tygx{}qrA&Byx@7iOwap6NLfjTS6z&FzF(*gc`ORm4yZRm@U@8I{~Pr29Uc*M zeN3Qi*YmOz%jua#)5kkMX#u{GM5NBPt`*Ik4*+!T6RVI2b-5IBQjE9MW4x=_dZAdL zbwS+;ILL9YgIpvIkL!22Nmy!O2#Wn4RCH3DUa!p25$l0)TYrUcg6m6yKFQ(~#4Tm_ zc*_j1VwegYGY=U5>(tw)qqFxeONm!=Nxo|=?{1`Yf82Re5{I;$6nmn3Q;7B!d7jr6>s(8BAC>R{2X zaG#H2b|_}=RanLsAPVZp2qdHAP|;Mh0kb!(M@q~VD+jlHlq}fA%42Tp7kK^>#PUPH zXQR81&8D^z4zs+=;jvb|n=Gula1pX&=yDf01`>XG1N8~b-%cQKub_d3`@C6v@*Ozr zwe+};rs8%a@LE@~Y$FlH%H8hPuGKUYz#z{v`gPQ@ir7m*{~4y4f~Y|J6-2SpoNn48 zIa{R69g7Db>@^UZvU>(h)K7x!i93xEj+D7==|Mp5(;$)wL&vyp5aRF-9fN?o5l|$@ zF3fYDc3?;wolr+8IiVUijQMurhNh>&vXvaxgSRE4*hLHg*(j~6_+$d4E|L@8B9zne zHo~RM7D*i6AX{D}kF&AJ{gKduPEJ^HEweevd5Xzry^}C$UqaGjs83DiOcR)j%F|;g zc4ou!uOQwC#BpE%?n&6f;zXIGRo2Tu3}Es^T)iK9azqb%8ezGjvK;MZGc~u!Ni9MI zbdMuK^4y5d_!s8Y%OFr85 z9Ycun04vm_*OLWb4(gh{md%%3PfoFN6GXg_P1%SNe0iWL8_4{b6c3#U1Zv2tYr7Di zRy|-c0%~a%NLdcvJhBZmZldGR7b!yTV8GP~@QhBbLH+%^9=jLC-pB-7{T~SSBT{A= z7Aqg4j>O&C=H6niU~bTJgjMS)y8*EckMO&T(RV<}-b%=AGnpK+_2k=V3UknoY)UkY zt=e&n);UfQJWR8LiDl`h`7-l0S*B$X?`F&B8OeeTkD&e++cAmij7fZu$yf)N_-3Q3 zwga0CU_Gy*drLm2m%ca<*=%dF^dAovEay$7gFq5|mvVMFLg{+aP+K@_u!xUfG29kp zAy(d-Vy;+6d>Bje$5gCK3Hm+vro_tYQsHIOS{To)I+loPj^X-_f5X_z17aDisnvcv z1TD^;$I%3$H|maFkz(QT1U3FOL{#cfqUxAqK}#5M9x=U7r_g={_SB<%p<6&aV)^!g z>4*3ed}nc?Vc%DNYX1k{gY4I!iVC#{fk5ZajqDmE?LLoj!DO$S~QsHhD3N*&eH78vbP!P6U(d+`$NiO z6CUo+u@>3!#2A;&w`NC8Om^&jz*KPDB<$2e+$z^9GC`maTN-l>tex8 zo$KNTaB8QEJ(LUTK~PUd0Ng=6i6#j=qbJ`&tZCRXUIn4q61b7q15ez31YyivmJDrh zv+vC4HzK+4{7s>JQ2x%NejCbq7$w3U*<2HlH<M{wcE6a7mJ^)FS0ixW-7*y)8vzYJ*ZjmWjqqP_GAXdH@-SD9Qw|tfB^9 z9i)*@VWdU;7Bha2aefvHBA*lsEXNV5tS4R!bmDu?>sulh>b$(cxQ-qmzG3BT2V(u1s`;H%7akkUVCf8y28B<1^ z|JzfIEGnC@kT2NfpIJk}>>aC*j`fFx6ta6v~#rng5ZkH~lc7^?>@N08)Mo>+=C z!t&=4Dml?EV=8}h(z}Ji_|kD>L8lpOJ}F=O4OYpq8-dTui)9}W!ZQU+K|5VXm4RT( z=EJZydg>MNnR@Xrbz|$rvL^^XgaW%zd>+_9fepM3cgSiDLImH)015;0*V5FzAqRVq zt}hFLstdykjFW55A%Y}kV;Qzd$CDyc} z2&-$c+1@!9bKRSxJ|rt)fqBl0{#aTWL&u$)x!-k@{FS|Q+!aExA9i*j2|X+ZzyZxSZM zM>vs7QNiG7ag0JEYjq1n6qRV{220$l$%3ngQVAx3gwnqurpIC;fV(77DDI)W%>wS{ z0qT7eZcD@)d9yCkQ!^+7m4_iSu@5dyiCUU&mFDR{PGh*CJF+5p`Ib!Aa6J+z@nI9Ko5_Q;I zkV`Eya5ae=Cq;=$gQ(nUmYdSHXSS_K!JZIN*$Itdn}OF6kBPg4_tV*gBh_0hGj1t9 zhK$D$Z+A&5WxS4MeEwf4HOr6xrkf4Rtd{TL3>#h9<=-UdcanGL<%rmXP;p~Ea%Z^# z2^7hF3gFzpsmQ%00n~~b|eo9N;AmlMnOPR}k1^`Pa3$iArpN zShLJa)bc9Qpvlxy+>2z(zbHwM239;rL{BNP zs8?gL1c6rV7wS+-$8`~0Q?Vp%rbSizMJ%e0moiVfMgkiJGT;>qejoxK`x%Fu&`vRt z@W4XNo!dHKOfnv@+f>^87<`J!_D<&;xxTg6pO4PLT<4nG5E~CDeE&iW=4l2&;vBCt zFu^(SFF6pRFUYt z8|yb;BlwC$7W{3l^IIMmMS)SB1V&R}bSHsk3N&{TXrVw$CxKlkuuDgQ&@6WA-4m!t zbl1n&-3?vyoI7t3EBnM}%b#SY?E*wHHA#L9^= z6}_c(P*xxQ9E{CU&}1W$K;RSsfzB3$#>Ur>`ms;Sxl=Oj!Ztd|`w;%}Ogt90&oM5e zG%l<>FwHR+;iigcFZMJzcedyA|Cxa%WBUw9SSue!y711qL~ej`#oVLr!)MbryDxNI z>XOw!%I2i*m}19J#pjz0%`%sN4R&`(-l-<-CV8{Cvw-gvoWyS6gjG|tsT0^@H85=eWCRiqsmXOxXpVrc7!@sn{(x}&@dJ#55(Xu zm>NtwaL9*JUuXjJ{dUKuSJ zTfpO74^sne2{lA(fItTzAj#F!w2iieil!a%w)%tJiMZoe(>85O=xw|u*^Yg&*b=%` z-x3tTRwOX#n(C3I^b<+GV6ewq#E##eVm{b5@|V}HtZ|H`(6{;F*Wg${Uz z*apiJ*bl1j$=rhtm)H*)xswz7K_hl@9>so89mRKYwqi?YBoMnoBZ1fzsskxGYzbwk z;QmkS2W1enYuF8ot*%(OpMzm8>TbR7XN(r;ehzoutp%c1EM?QHs{*Id9Ikkvie`6L z1&-pjVps{)(wDuF9)RiFy547jdd6?iia_rYwpN!&Fw z>hA8r6cz1Spa!I|3NWFuiXO}ws{j=+bM3y^ZRtSP&aa2%dT+Vd=w00%^J2JN`Ww3q z#Kb$BF;=c-JS(37Pk=R^CWzb^_AnL0o=fQAr*DyaB?bY>xWx!I@vob0V&!o>tH`R} zpz&RTm=<$*?~ihLmv&)bzi4+~FclBUb#IEw%lz53Jx~6@j>nZ0bt`1E%bQXER(#_= z+s*am$FP!s|Gx;mDO*0F4uuc9$YMlgQkTpIS1-x=MUk96sY`anyxzT#wEs=9a#FAC z%%jDJ{V!0r<1v3R^GobaaNd#xW5W|iZ2HYHu^4!nzgVx)!-zCCp~z@k)5ph*LjB!J zap^(Jb5{~Zhx_l}E4Bir|M!xgR@+y@g&&&3xn&uTLFG}%kV7`OG<&}0<(gKlep zIqn-TDt+$2V{#Q{B>05D>d)wj)V-~by`nEf*s@R)!E;3mHUYYZO3o}SNL;ab{WfG^ zQc|Am%adEN-4QdScrirqZNC{5hzl_-9_~nE&1>mib^e`Xq2t9o@W-};IV$k1c z&moxxgIdA3mIr3E>EMdh@TuSeXBh`s^PtYL@cJD|}+KeoeqCV|DcsL(dcz1lX*ydlYgx(*Tj zU%0K`!6Uf37PE37HrD-aR>9O&9E?e7R<9&aY^1L4F zVdAn?snH2DiBKihVq5FzK50)pWvyWJJ|IbcW?36rOUdT<`?fqpprx; z_t&j}?p8hrFZC<9bDjHhotUpMZ{}8l$&O(ffm)i7b^-VE z-{+7III#HgEw(E3L)Vdqi9>|A`ns)S80@=XD7~BIZv~SZg0gt7z*gd~U00$3a$sgE z2COhCWd^6=hW6(GbQIq9P*-QK5}buXwG9{cEK<7|(krF+6$)zNF?1GHwpj>Xhzonz zsHKiiNrhMa)lb3eDY%7#qY%RPf|=(dcpnQEW)pK)_%o z-DY^9teXe0$8J2Vma@m@R#Bfnyj_p`cY@xjd!K-})VlU6mhO4vPkD$E7)h~S)ML$p z*KOU*V||ZUZVsv4MH$$G3$*Iry1@$TLRCBP>!CS6@6yzNJC4y+h`XvCd zS{=6-cX|WJ-Ef6ik%^RpTU8rQig$0pCRGP!bv>3ofT2%{mb`s7qc{Z`O4c8YrY5Q) znWF-m`>##K53bupS{7B2@J!hpP(NeRGiP96Zs}N`t_Fi7i z6HAwz2}$G>-)^A29~HYyOuVg>5H^fjy0UmpNr=$IBDC-b!9BPI+rY3MNjPZB?Y(ig zV{wcq5MwWsN$h!VN-9?08^zUQNaO2H0N&OLR zAdhC<#-lAGMybt;gfJe}&Lg-eTk%K-DW5{7;YW)7-GGUYPX|+k;S-FOam!*DU6Bq4B3d@M4lHKF+5)UG_0nmg*EE2%VLS2q(fNE(;RGFmP z$-hDKJq4c10jgAYlJ{9OKuRfT;1=?}Ox|)>s5+Ls0vaIYbMmHivb%DinpSqZViaTiWenUu+^7{ zkt@CZW(Z|vyAz>1eU~GY+xE?vk%1cV(hbyzk`N!Kl^5R*ijYM@76&6xXGCr2HI#$cAMp(9H6ZJfmN_jB34Jn1p8rLv>{y)t{d8n1NZx za}X*Y*&({*!ek&@bmY4n$!i%@PnL4yD9rF;^T_~U#nnGSU6g#PMvYr`9WT^=kEuhI$f`q9Q>#%3?k6Q3U#50ND})W=e^k^FjouBk|fA z^{A9+KH$*%T-=mpI{tc%`3T0mz|xO`pV5Oa*Mi+gxq3%Z@EdyYZ*@rIbEpo3&J9;4 zqYFj+U>6#r)F7g|j^ezI*U)IIg!%+Uz}~GSj1Eff4{8oANrC0dB+6e;%jdXHZB&{F zJQZMNJu;=H-)QHL9eCP=)se zlVsK0zgnBUrwzj|fDuH*&YG^S7|DI;EEeEmq|E*b)}R)Rl03s|;lOKR{SnLZF1geC zzeG2A9~&&tj?T-GBp#JW1+>d})p=p936&QYNzB6Qm)83LP*0M^WXpWGgW_23hKIC} z%kDibcHGgkji8%sxdAt}v5Ak{pXFkUmDbmxhG?t#QgBriaP?S(0YG@imB*4X_ou;@ zZ0W<99qx}H>L$zUR%EbowB+0c$S>&x8M;>e2;$2*0*#Vc!23Z!X2Y`G!A!xPB)7E= z7{PTZ`hSrU#JUv-9`jmO`s%$%*MEp6>^+v137A@57$uKh0*6wHlHo-j zGC(nZ$Y&`vBE()BDK_K!@604W|_LBfpN ztIj1XWkl|O-GFH+CPRMjJvL&!I>*+W&QsITLmvT9F)&upNw0 zf<^v>S`ce#nMIuiRcPwvPav~d$CE>V^$bt|r_~F9I)Mdcfq|u*1?3~1@fZamJx{^| zETQ};w`DbkI3_j?s`d>*CboxMr$Z()$PFkvZ3^K0Dl8#mW~zts9n=v>_;U#|=EQp4 z(9LYo3J(K#O=}7*XmJA8B0T2(d~GWS2IG|$bHDL%t#%`t+ zV@aNnSS0rYwGX2{8qaD++zKF3_M`05swP&9|N4lY74ZU*#mR$W7h)0h%he==#m3Sx zr?Yq1;~GHB{A|S_Oh0?41mrK%KF8e3SUjA@Nr=~EHc>^z)PGCyvC?55AhK2?yK~0l z7HV(cu$D)C`9tW_V|fViuq65fCCFMJdTF;&q4%8C-sd5koRfrTw;|l&nS(qX* zsIwR=Ac%}@BteNat zB?@urMb`JJB%FKj7E~{`lsH=INlC=z;wEmq;*O%sdvCrdu6YL0SWQMFdIsi-nhPc$ zgBKps`!i(RB@CG$;x=B~IBG~yrptbD<@P-1Z+OnVNn&r*dMs`66s(v_vOUA@1>T;v znYQKpjaAKI6G4%A909xamD;`|!suk14x3hIR@Aj3o~ zUEyR8{e2FzC3!hNu_&8XbS=lrDN;cfI1j=pc}n7QonOE=8Js4-VoHJ*^I#1X9J+KV z+HxHNVNO`%@BcDTrNchP)kHv185>sIA5^pAJ}pvCE6ro2G)zSIUx4V@nWvV+rW)<; z6DE7ww-daMbXtG^88PXFDQ;7I|AGzCVJy>d2zPRq&46%$$J+)u?>M~xtn2v0V%V2rB&X6^%$2W zZJT!@8n*ssgwj;5Hx|2L<4$9c$xdgm{0x`Y*M6tIT}6!uZGLv1Q%A9s8~rE3jZ%I4 z0L?Bpxvgc857T8$maB)tku9HAXw^^seix}Sp)rl5wTz?oO`AuZpY5^c1C%ZQlAU$| z?~&&@f5`K`nL;p$_QArSgbChdgHT{c9hj)T9rDNx=#uWFr@=h3F82*+i}^+Tc@}oSUCk32 z!4qjj2QNO~AXe_gb^>1yivFh<0qp(HlY$i1kzss*LkaLGA>frRR(a%9|3GN%!qt!z z=UXh{TJv8*7*7xr4a0JRzdSA0Z7oJ_1XmU$yay6OxZ(l`2F)JOgsZRwco~!~BW`FN zy~`7GoqKAT*}PYYw=p1{;J*_IPU|SjT0}uB=D$A37mx75uGR|6tDJ9YN1&<1mm+4% z2X-Bjr=bfS7Ptp01WCXXYk)YAC&^FIyHDLuhmXY?(*hO`|~ag;kCi zyNo?6cKJ)Y{AsqlIZxiMj72J{4{vn44_zhib8m}*mTiKVy{|}4%$7@%u$4@rMiKXX zY6TtgLeS@=WXm&CLL`((ZS52C(p_MXL`IR!b_&SE1l@9dgyMpLVi9z&f3|KTYVrvtL zgBKADz6=u$${${#XGE%NgnptG@Qy<;7(BJ`(x;7BD@*a3P# zMB1SedW_I(I64XFK^>s4i9m-WFDG<9M^mSJcuMbsz)?sV1^y^APOguk@GZCmFwlF4$ zFR*17E;xDlgvqO%i3Iexa5SsNk;QxofV@h1;8N#u^c^sNj{i}%%Z;R_LP2+E&uQKxV;RobHy znNE;)$ao7Fnhb&M*RG+Go|i{Xml7cAdN~C@DyI52WQerAI=%`2>+Yrekq~toGmr?d+uO5 z0Xn3U&YSxsgpOwD|AXe9p+4h-N=g3THuntm3`4PIU}%`6bIzcJegMV)I4c5bv8w4} zFrGyu?46teDaxN8menqVev+YSdZ(H$h61E@GBuH-$$0)7hMx1Qmi#)#0QEztri;OT zT*Tl@c90S4mgj{rc)(1_zrfH`i>v8kNWPfRf9GhjpW)%?4qF4(oB@ZaOF~cOXlnG^ zZZ~E~tnY1NK-RYo-KyFfD~FPdF`(rc#yB+8K%QP_d7`O_ zYPuK-1U^CCd|J2MdxGFlWv*smI)k&CE;Ur6d3B@?S*_q;Dv$mV;0^{kAuzerTR9ln zv9#Vs`uN?^3J_Y#)G(=+FfjFEV}Gxzghne2wU><`sjB?$7$?-|Fw~0-MQQymisEwJ zFw{JTVpYY&vKQ7#H!;OhruYCb)ZJ45r(Vm!)Xr_nBi#hSUCB&$GH@>f)1`*JFb9XA zP=3{ueC(M7@aixyv(kMLDTlz6ZS?~VMiXb5&>pNtfFA~g=b1VnwS9Q>K<)y@(T!P^|d?|4#(C14|5n$)(ma zu=_Q*fuF?i|4U;eS=3bw4+AM*Pb_|?=?;zL7*JxsKeR`xw>+;5)hn3X@7p7ph5_{r zJIsmM3jf44XHYVfvF0W zXzF2x9EqYfpAP^TDlH^(?F56!4;X4e0wC3NsiF3sgGtNkF`O3#i|7EXJX+iHxP6!k&QV<7|(j9^{i zNeoZ*ubM73)WY%tBh{JSWgvOaYV$FJk~b5gr3L^cVb#)yhk zP38Cv9A6WGhy3GM`j;WRnl3fNaN#PXQdLzp&~?*;HdOd%1ipiYA%rKF`WnYCMBaeE zzCFJ4q1jNv&tZ7fZ}%Kx@jDFzX`c(ufY&nMA9guO;izBPDD)4TleBPDBSZaRTGxc5 zynMtqhGMPfNTaNJb{$OI%YmwQJY1d@J0P|7>Ia znf#qMrlbya0LQBwzrl!)C;}3AT!KJ>*@a`C%-5ZT8c>l{Smf}{^#bB`{zdDcO<2nA~c!LOB-JM%3Numzr z_(YDcHRAOw@E(+stENj0sf(BRAY$S3u@X<>EdFF`@%2fZu@u?htLwkH= z_Z6x%R}+3N$J;pmyxpLJh%8W!tLaiR1Q(u#RAO-zXCZMGRYn#aXCWj4HS_8boJItT z%jftKBfg_S0IAK;iIXtuOPoakXEEByf{W1kAb|P|)yeTQIsO-$K?@uosl{}lxC(|7 zeh|l(aQp`mcnkt&v!;(qteP%0qjmhXgg^8HQ$Z=m7f0Yb7zBjyGQ;)SnKs5?{~p?)Ladiwkv@V+j8a$5(NDRsnt0sl>gAv7VwdV1CW;fO@#mHd&)lyr<{%&`aO%w z3>O9xX~sUid8 zNPVWE7sBvtII%inI26KDmetP>F$-zo_(CIIH_~Sq3u;BH=~6Qe7hcHM6N^7{7JE61 z0Y()ySgbdS=t{RG6yF@n<>y^7i=1dKM}LJK=LVo=zmiDCO(x z!&QKK_BK-iJrPyYrRG*#xcuV@-;LuFIsTs!_zvn>2v06`D>hJ|S)R%9QyKn$S?r1E;TcBJmp%Q#qp^ee|oGz1a4#>Mc8==Pm-u9 z9G}kdl}5at1>U7mZ(mK9nmcjfc5*YZIPe`S=dql{Vj~MK!qx~8LU<|y^#zW%ar{Ul zUKfE^HR?gD=~6@G%terh#dOX>;w;*(Yo~?Cp=iidsXWyI9G}ne8`|R|t6HeFa1j36 zZ#*&HXx< zw5~2FgF_QRMVw~l*EfGpIH3(4J+;n z&SI63MaM0BsJKWI>f0Q@mgDX1@sZ{hsxgxZzkuUk<9Jg99_IElQvr?ps_9a5FD_jE zDTKe4<2P`8{V0P9xcrgR6(Kyi)E~cQ`B%04x5syGZc_>WHp7#-wGxZpF}J&P!5MG~ z1OB18-4l+oF%&bmFGd>jsuwqJqiL91O_!Pi9Z!l^1)kk1p54C~Ss2^sF@&c}%>o@y z@~d_Gn7ZmXeqtD&S*$5Nd@oH1Pm-vm9KVI*dl~V17I*_mb|#{8 z!5MH91OB1K-WQHq!%)m(2N`A6i<@`JG}x}Di^1YZ@#<|1@1`%RW9ZkK-Y&bHTii^- zU&8S*9KYU(*G1qKM}zfhy3|m1dBzKg#V21fi;3qfrWsjuY;mCyBW0)_j!)$H{_XLR z78h#fXA}Nbj!) za;cx}Vfmk<EA@@)1_t+E?j>L z34a;KS7`Y+;v@FZ*bu#%E;abmSUe1ux@Q+t!CJ7xK? zhW6ido~B6X7>9M+JI(_}}{F{X)hhC?cS z1JNcqn{hByG<)mCZLK_#Bt(mA*!(R5g2$NNhT^CqZK@NIGB$Ikn^xSB=ln6Z{&2MY zqZkByOeN%?^Fqh(w9gcs? z`lKDoFc-Q>w|k0{vgMz$<#VL(;~VMCrf-4=SFFu-PDuj$zlPZ3^euYd!~G}7^d8F| zzJap$0x{g&0mEk*!(%Ldaf{pXkGrsK7Vjo_Mn45t4vtSrYqmTFC;gbd#Wi2`K%VHJ zbket-y!I><_D%C-n5&*CH$3r-$9M_*@LQ;9=C@R4AQ3f+#uU!#)cm z-EbzBSY85O@-0J@ny7liaYR>9Hxy(*U#5;kbW-1Hx(zQKCr(vH^R_m1E zpeQfEtA4)Z72IBKM#(!KM)hy;??h7_&QziPM_I@&M_R z+8q8FCuSFZ(8P^dcn3*QC3!zSlR$^TiDgeQ`V<_CwbRwDD6>T@uOxKv5byVSa1=sZ zdnwMYY_#V08nXPhp20k13*VoECS1i))ki?bml~8~diXGeD?3R6hf1m5;GiVW;zT7X zBiM_?B7%<&V(5_l34oM(o!fWhW!(M>m#+pet@WFMqC)p!a%9fJH+;*y$b#G2w>62f zyB2jEMp!`SGJ5*31D9}+`9LV`5tgobv+yB1+dK)RB9J00XVswg#pHU58i~?zQNY|z zY|!KKE(#yxLV}W0LTGov49TgVno&~z;xkR+U+QgRw-czez{0;uGyS?zdOzx$9kR6?o$er+ljPQR10R*dx+QFNX4!(4VteKg&GI zbtAfwl~+=GR(1(Qmb|W%naWrlFc|=U3Mw9dGa5Cs_!}i1!Romc2ia{ z4;SYlBn8Vp9z39zQA(c9_5z~uK}9k(9I137CbX9By$fdpPwpAjgk6Eu65uW7pXn4R zH02n>;N`JVV3baSie$9UZmYVVioTpGh}-Jto>WW{xUKhm%Z%b5XIO^a~JA)JD56WH*a4AjNG8Djf-!v>Y%l-V=O;Wfh>uF~Duu3@$QxHTBPs*F#2)&TXe_L^e*hCS(2p(b$VL^of8v*mBwyv9=Cc za_>S#n1~*IXYn3<@opuZ^k~Y-JSeWA;aRqP*iI*YzG>izPvo}vhI75^Bi0&Ss`ZeC z#xBYiI>}4o9U(!pbU{~o=p(Nf5O-`~>2H&P_5LP_+LlSbkmrf7ndi+5%HYf_`c2k~RV{s6WLvG1~bF{+)8WoU1S%#Ybsnl#s2UNgW zuKrKhyn6#aeT<>djd|$aGaYOpDo2X=%Aa6$ zJyA4aqs%^tkKXMrCITCrv(XQGRKS_kEgod(S19#)2$jT<)!c#CdFdFN&zW5b(C9f=t7)dJM7b zONh@p3SS+|NCQV+ha&WEq6hRq!n!MxaV*$7NZ$A{cuBpqoIYXkh=@l}$?yn=BUw?_ zFMXawXAPJOWi zvC8X8{w~Q!q^e<~u4n%x*_={D@6vaV_-b0{!|phBl<@a)yjU>>S;Fx%fB%y7v}QL- z%Kp(g#Qd-hoD8cLLQcSjIJWg3XT6+Z&aL8x4F2VlJkj^VDZK$AtD@8I##2nQ$M zPobl9=xEJ7VrBnVvCj~1svoki`i%zWIGrUMOacifM&L|^3sGX(8tO>lSaUOTMDuex z-51Pa`C3qlnk}^J$wZEsne?eGyL=p(9}d3sf#k;!N37fx_I>2XK1-tSBjezX7{s!B zC&$s#uG}JK*Nc@n^d+GX5pX(uKT`vJA0@M%eJgnxh)vlhd@K1V&M#>IdK+yJ%-q7h zl{}n5%!&M4$s5?#K}#Bl_)c;`p7R$6j_Z%MtRuQ?c?!2u%Nw|waB9V?M06&+_63S7 zvjLw$ZjlrINggYGuXsrhB|V8W@=XRklpkM_gxs}!ieUOcO60eT?_YxQz|@p*y5vpE`aFBzyvp&yAsg@YO3c3l)~~Q~d9h9=xj|mf$kRY>w%my;{hBTLy6bdOkk+QT@F5pwjnt~(1Oa@# zNdC+_BY-d9-KrEYtq)Jc8~$@yo~F`_KOG8Wx#JV2ethD@`ve`9gKr7*TU+TPCVUgR z7c;s?Oo5aOZQbn%w$x!4VdmbYb^iBIAuCvHI?uUcRz?&`LoA~QCOB5aD-|r+jeT)O z)*cX*4b1;4`7v-7I)=X)0WYEG&xGJ}$iKQ1xa(m`IZjL2im3h>TC(Znnb=X9u5m_C z48PV~XtpSZD1nE7s@fC&My>{Up) z&U>c`4~OjdSMBtsU*z-3i#oe}u%jcKsWe9Ir*n;zz0ea+Ya{~2jZa_BS?*jhn12CB z`_vIT-Uf49qN3>ROhB;1ibrjxU<@d)8X4qvco8HQlBos`M8>MfT(uca9QcAczashl znCegffs`d$Rd=?|Ihg~RTADW30 zpRU6RP5#@$y*Gt>)5E>VVYdF>LRd^5%Umj!6_`;5=ft(%4+n`;2MB#`=i=Ix^-Nr) zH=3K7410{02Uv4+ut{%jSj$mbLXFG{JPp#PFYs9h8^lK=Gj$wmWVZP~X3vZ0EQ;|- zh|loB@t7!daF{e?katO6HnDQM+h_8w2-qrE#xp-#ev{<9fKzA3+N+@ZfIUq`q|ZQc8A5l@1 zhgnXJ_Co9P9sHe$wTU&C|98YH2#Ga`#F9D}YuNuqvFcGJG;Mv<6Josse<#}d8-m2j zPPKKT!?_tB%AwPo1T13llJsdMnIV}j@Sd@J%FuPKCeaW` z5KLjI}S@CA2C39JEe$_N;)9uqk-KvCseJa9r3-F1||HH@%#}p?40-fEi-zA}X1 z`458%!G%*$Js9o^uKtL-4cmX3Y$kk&eNtvJrhK2S^O|kGDV)*28d+r$JfV+5ZGntU zn4G~^!6t~6EuPWcz*A{Kh2$N|!FlvW`&96UML-zqQ|SNIXQ2WAQ*P^^pa5N%0J9-L zE)yWe#NcNv+c1JUgBm54?MP*rNn_#NOqlrHea7;J7HkurZbms_okEqrsy&P3)$xzB z;oPqyDMPWQDjNUz{>+)|Zs;&07ck|dXT%0U4H>zNWn?NwrCLU|Y(qwNf$F;%^0}>d zAwE;)7{n1=nB%f6XK9Nh>(2_o)Q>hG>RA-RnHDOB3s6mq(EpdWxF2Im@BEoAo1SM7ajujCZyABc?Dw(P5D1y)mc-1?7*P%sXdBR{z))`@;4%WNcmfuneyLA zp{zG@&vWn~E02Rmr1JkUm*r=%mS(u}ms4O+`7`0+%D)}#kgsRZBsbZ}c&*ofv#Ojn z=Bqr7Nsvhrkn+cpgDJnOmKJcQ&@dR3|K7=<@{bK-67NE|LHWn$Fkzd}S+uv5777ds z`yM<@`6sdGrpXo)svzUv467h+B!s*)vS=m~7MqU1I}0gzO7L+Aw4(SjID3>-Js5RL z>pXqRTWbmlvj7i(XiDH3jp(SdsqG*I3}P26zmPeMw>FpXL~mn>Mgzd8w6rFxN!G8^8x!jL&GL;zkJO;E_SrV;w!z^9M8p{_W zrrYY?jKZQ)dyE{#X#m`z0k{!%1#4bm0(jk?SD3LpkyI8D^;oYoye6mL9|-WXV8SZ+ zWgzRt_FEB(?Jr1eB$Ko|Q;p}*h=Pb>nM6ToIyo{RsFOFb5Zz9NyH*->LUoMmL{4Tp z*@~vC$<_l_{HR&oamuKSvLZxjw)DWzg6FwmOJ{zyx1bgyWUWljDp{b4ejty6k7$wdU zQw3_B%<#Ict&K^jB4u=STfgR>N_YT#g#q);k#+s8*&UX^Ga&0F@F+aIme1wP{)3i| z#tqOwm+miV2NI2p?naxh~_;i5-J8p}?+fX|Jk2j_ksE5ocRM;J?V$D$sa zWf1jqc$l$tVIszH5i`R@eCbNk&wChHFcIG+M==gBx2$3*muMndgrGfNOJ@XlEbpR` zYO-Bo;?hn77ZCG0k#-6s;paYunf8rFX_HCX)nHPl=Jqy}a;1|uEWT^qr(=6Ea*0>Z84Kf$OWtJ#KFn$^5skNjhW8R@vK|K^@jc#y_I z25fINB~HxhC(MV`;hn=w&~>xPf`^;U2+nO0n#3ksFKTLTxtxTzb;GdR*N2BrW}$sM zuHJ*N!o=EHt$KF_o;P`)VJyX?rJiMHq;LNt6iE6T4#`Qzh z(_oGFBTBO+77~+)NI8$C+`jpn8`7)$oJA}j&Up{e1O?KGrs)rwKO2hKV|lShP(Q87 zT499rV?sKbeh$?_4D@34r}Q;kahk12_CMW2RO6W(ULXU z`ti19|8b*!%5Pzb-$jX2^LHmXSo1fSi{7qn+2sRwGErYF=l&a-{EnJGbH}0{pJ5QS z1s>M?b!8%6!9~12T*R0Ak$&F)SQGI*axf7eV=1?9{?c_3=K>0C-rb3ag-E`GHgAGa z#9=`ZXQAP2vL$gVn|I8p#WEAp!T7hEZe>4Uh|^Imj1FauS=pA$n1EF*I;({j-upu< z+m}dIHV&!r=JL^CVj(O0C*;$t>`xy-Ut-yGq~x|P;hsBqvUV-m$WAtQdWU)$0kUpo z3Gi?$GjnFyXnUJ%$y`4U9Nl54g$EKzKaa=g`uTs@dlT>`i|%ju?h@J*XbQ3kqBl#W zl?Kb+7J^-&g;JK5wO|QtS}NUW5-7-0ObgUnzy$@DN8CkGQKYhmwFOsD5fBj&ki@E> z>>$niJ2P`9=>quuzwiC7_r0zsTF%UwGiT16IdkUB+*>umoyPQY+EtGQA@8Ch25==K zXZkt*$zAocxh?7EKD5U5Gf`>GrJu*qj?ho)7N(y;XbJYuGd+2;okX+s^%Fd~Q7_dJ zXs3QIPg3-ArY-A3SNO`R$j;ov$NlE6pVFNmvFHwN7AAgx63oP3#pP+}slhB9jyDDH zS-6OEpUDUtMy&H8Mk6Mk1+-Jtp~$dVxDd{+DzYmd!ZOSvw;{YA?NqCFH&KSLV;}7H zFf_NYBs4aX_fijOS$_^y_&9v4kh;doxRIJh8t=s=k^jjTUBH*@8uh|I=u`7Nww;@%Gt}Ldsr{qDxypH zZKi*=(?7P}q$KL)hp57P`8x|0>V&+_UA_EcqfE2$Kx^uyjc0ZvgI=y@6&v<)%S7ts z$B?>iFW&&(*~>-9@LrlZw+--lRgv8(czLoV4G|As#_`e@SZQeE!AmAx2BJ-(2wsMw zJ`Y|3Xnm`{r|i$j#eU5TTH(RVAFWugw5+9`T-$xm)zS9nAgNa6dn?*jt!v-7F@5Q( z$K2-AocBUT&fG%Phw|MP=Ql8vK>+_=J3H)k-fQoT4P$f&AInLQmq={rRb;Q4s5J2 zpk?tr4;Jh^z`1J} zVM90D79HNq>ebmjNkBWN=;^V-&9-ME4&X!HxsHe>pS7SNpX8wox#|@xW{vsRO|E*D z8%;E&^HC9s&ST_kO00kXu2W(;?5SM!x1?ALUFT+vxvXUr+7Z^$^Hb18S#%*h zfA+@kzp(4I40sCK7?t% zxQkeFNkc=p%Ap+Rcl5*V4Bh&!b>ky>o~qNVeGFCjtbJD@b&UhPvqX%;norm`JcV{} z-G^ruAcHpYS;dC4c2)|_+FVFoch;r>?;MC|WcWbzXL9?nmSVX+HK*$6^G%Rcs}gDzeX5=W|Hh`o+pcy(&>!NR%KEoCS=Dvh~@Vi4L9LvjDdY$!a?l0|nf&s=KGx^xE1 zO=DBy_tA|`i9%&R4E?%`b222&!6L~S@F9NIWlZY#4-_w@F7gZtaFK2a;g~(;i7+> zL&(0@)yN^_X;(eA(7%g{Fzb~pg5mN1+jkwp&Deh<{zq$kHce!;>qKOalULwtVCqL~ z2nV4h#Q!|glQ-K*G+Te64<6O1URna}9Ky>Zl_5OSl=Y!2d}~!?0@qK-&vo>(6C~BD z%$tgSIv&R61^r%)W820oeJfQbm(d?pcqh#Ysmo5E2bJjL%nw;7C!igRZU)aJa=8Yw ziVa;xEILr$Is#JHbr~VRJA0{d_OjNG^>PrrYgJ@Y<1V9lc3qe8myhByKBI-G{zCsV zE`T^s#b|NmF5@}g()Vz6Rgok3l<+z3uFujLAhGBcet=HXlqjYIn-U|?j%$^0E%fvj z0X`-AaqbT?!iEcdj}eW|-nKwHm2x9VOo^UM#8G_6!!hgJro`838gk=x=a8SlJ_$qq z0fL{#hI~I&ry-9;6+YxoD5S0-e}kqrw`@s>rd84|#jKG~%|GsKq{suM&H3+}mKtYck!2oG#Gt zA%D%6$$bibsw#3E*Qfo*I{KUs5?ueirsz|Z0sf6CviO*@9$O{iIPboUoVl1eugiDa zON@i%ma8^hRfgg!Rt?seYbe^G9WfNw-eW^?3>~uQF7nLR$Y3b8vx*IeqAIabJNpP| z=SVz*3?GSwoY_wJtE$NHd`et8>g*@3kC#5m8qcG~X-ec$f=!8mT=WJ<48I)$ceYA& z;oR@xqBdA1I*_OhR|#)-QO^w%Q{sLm;zT}#57rT}WDDja?q0s43}MHE*v3FdFCwyN zY$PkGI!%e5sKTd2zC!96hvlFW<4~}MjYBfpvFN7r%wS~DMn6`u;W!L};J7ycQrDdl z4+8HT2sJW%Ag)0V;1&j-S{0er_>}O;s5>QUJe4W&F)dv6z2FhLMxk5|g{_Jyv6Q#; zHT+an%g8X0RI4srRP@tPk8KwOcu0{P%632O8BFRWd)tXB+}<2G zgsnI4Wl)JuO1xjEaVTQZ-F%z%_y=UrMir~ru#;cMlfCVM)OGEx5_o4XS0TfDDP9S& z56-J9GOKZWdjZ!=++FbF*zR!`90eg7*xNKlE&_FUcwuk%bGaX7EluP4%!G?@TheaA zTU4u7|E=g#bqY~TWA=8-Rgc-*E>wh0K4Ij{-mboUS9|*&gN1pE*7#7El*U|Be+9WP z3^KHDev4^;JX*5o3V3E1Z+3uawtkcsGo(>_3jx|W5*lRqNYtWP^kER3WL4y2Tt9=q zucM!1AgNXr|E1`s<6qd*pw4D2CXK1-2dYl?HVRdECzmOtu1>B4mFVR1H(4i*D8zk$ zJd?@g8p|p+w6{kGlf9)t>bmwe70?ZDMjHN`X3;Y0a5^5)YVG+V%mQD# zjgGHaPWLF|OUEyOMYXB|fe8(~>&dNh*WH^t@FdRiU&)~GQjYTb@XYctQzwn}kFr1U z^p?$tsZg@R+*Wyj&(1|`#(`=hvBh;{G(f+^vcN#JNVl=>cHVj}cP7yTsR?#FcJeBu zD*B9vsQ&R4oA{F-Pjj%#Vx#ASmar@c+Gr}Dp}WnCZ+MzU;-8uK7vJzQ^(wyMZ5|W9 zvMSaG-?1%Mox*Mg2i46}cNgFAFb{MU>=OkwXI;2Y72H7=Znc8jX8n^X`Xh`P@8bK; zTlg=s`}gC@_QqDsqDNesTH{&IhMkr1SojslF?*$q`-bs7W{p)7Um?2mvAA8lirv;d z7z)Ef50Oh4ng}(OWvqwS@vzou=&<;@=gdcouj4_jRpw zj)b3p{a5@HR`%Vf@jn*BJVz0srr>|hq_2}ncTMF`59rGD2`TJBrZ6}VNAY!UP02U4 z&bzD6VrZSWRioqPbGWVlPbZr*t_PSjm4jOjY+`B~PmdP-Gf-{nvIQN+V^}nRHAWiW z>&(v7mJ1$qL&s<@=tE;Y6NRUnanouCIJa252;jM0;$b|^e|F$eh)xIW!5|#yX^JnN z+p(p}G=YGZ$w0u{G$Y<}6OZDz012K5=y(q#SV7;aNBeJNTINn}(nPcPC>9*Nb7*oC zN7qBe&7-6!P362Mwqak>!fJ^uCTxAME$~0riHxr zV&EZRUoPQbF5zeg*3vumBG^ItM8thTQL>bAYj z5zVS?Rz|NWndoeGir}TTea*^DqPOu*d?jyVt-Y@kRirfAnKwItE17B6%akFMd>Iel z!Nh)L9v=55MvKOe1JC<>8pa5UJqpDzF2cvWbT2P`TPfA@R$sKQi+~WT_d5qK-<@o4mc% zH4g&oqhQlH_UW1ct4AMNA9UD(v)XRYwz1Wv{%5=~(>_Mz1!tFu*WLI=(U6l~e!_mG zc#3)%k}Y1s3KOn+0zmWB=K=7kx_qQ@4T7SBVqGd_aPMIo)^hm?nSGP{n1O#Dy9;7S z`X+Y=iY0NsH1Ul;7;r^J0iTDd6>!UOFoXs=Q3Fc{vP&7-NuY}_pWIGU8P{}4Y}clM z%>exXeQ|@VEwpRBVh{DZ-lis&lm9Gp^#TobtZ!p}v)>+IlafA-{%qyWn3hP3aMI)uQ_g;ReL~j{2?o4~X#~Y!x!}t@ptY z=x@y=Rg-kew@~#%z9s}hZNSFoO0=J+xyhC2Z#_+q#FzKog)^N^Y!-$0O#)BN(na8c zfq9y2151owd1N!#)F;cF;*R?X;{NuJ!@=s=N%b@#@$|*aFlv6;RBCp->Kxcn^CuX5 zRMo#6PjqW~sAi$u82ER*Cgezbct;Ot&Dw ze#P-Uch~H(b)QAksN)Xw4t50j5Dqb~5&zxEOwIWnsPxbd2-N&h2!Mw7&0J+GoK0s+ zS5!H4|9~moqFeKVOnTHamlt`2z3wUn85k(uLQ!1QPMRHKkKqUysJ*Z$v|~{{fok+v z&n?@=t2Csh=0F+nxpJ3(Wm@I7WJdR;es zKXM)YQbKi1z6+Yl(H@pxG)q#t;{8I+?H4eU^nSImOR^(l%VvaWD!+w?LBWn6Nsm09 zw=ZNKqV-lH9_r^|e*<|n|f-)MjbF(T2j4M0O z9f$qubwqt**>pPp7b&3izVonVxIfFub_3htO=xuRY|&<~z!(9pL1`Fs4T&hgs~n+J zyc!Dc89Y?{gC39Cdw3+I;|+7IL>5mgL}b9RFY;su*sUY3!FiYcweuAGdNd+Jje6gb zXb)g^*a_olIeCFFo?`E$DY?LpjC-No__FaMVLO*;kEPj1dn~-M%c5)d6!TfbG5=vq zJDwv!%UgR;g^HnguT1kRf1=GLk72kA!-}UyUoTI_OBLsL!z^BlL*=r=JI|r%BoE6e zjr#hMB##}xQP$IP>Vo?7C1X7;x@};Ix0?LJY`yin;1*vtv0dzvsaUT}UHu}L6gC5E zZ#4Q8%AnXe{!5~pV;~TKsvf7=Yq^G1hhCfoq%Rw*l2@_)My?qz8;UY4(#<^TFVc4U zm@(c7)y#GsA*Fp1Ik~vdGS#0rSh6Q6xigfDWIX!rL)!AEhZPfEvXx-o+Pm?BkK7BU zQ-MF#C*H3RZwa|-)$o(hAFARpUoSjyQ;bSc%sXr*hTG{MTgSgy-1VP7Fw^K&J*o^G z3NIPyW#0xBp;8hm*+Ov_c~sdR`x@Y?RaX!&xUuct7~3k;0J9-Zw#@}w3ar5PG6Esn z(F>gIXyBOarzSx5Sjy39?h%+0UM|y&KZ4^+7gJW2j|mlz)7bB8obKds7aiS*WxoVR zgJU8u+hd}+(?B%Rz&rITZUJ4j%GcT3B5$re{+)7{3V#G&`%nyF073L(T3ZoY&2{Gs(U^bBKp;#dPys3*|J5W#Lx1UmLR?@kJ<{aVA?_4I3`+T9qjNf6)8 z6yk~WAM&;h{m2fw?jigL^AF#Hj%jG95NJ0Lxc+mOHqLDk?h|-7EZ$FK(Tq{_**>Jt~=M&RjjCjFa+D|4@pT^t&f-XL|5Bdo_u-b^6 zZ`7yzjOb`t9h?mAYmh4*dN9CVNr|~#n|jSuQvg-^C-SkHN<>HY)2`$ZBr|c?hquRK zm5s9e;bFfY35%{j!W>*qW_!48*cGB`-=7doMPaeGoL;tMvYKz}`PPzH%zsQo$sH{S zS?Wf~pCD4X-M+Q?hHpU6Lg7BUt~9~>Ycnp;IJJEP79YGCb2B3!P4M=vfqC~20QLJCx+B*_5PB9dYmmD)YQ8oNtV zlPhrtz42nv;RikK-B7^l??$2JixRYB@5Si6O)(|MiXOp>Ujy*AGfl}RU^hZ^>^tMA z|EBx!;Qm7tbMC`gDE+?!QK#p3C$App675?S?Q36*8pZP4d4d3A5`LP% zv;Y{yzMe}|zh9)im`X{Tjn=K~oJvGLox1cha)LB$L_@DjqsOK@;YI#yDxYLyxo z`XSi{G&mEYQ9t|(kxvT{@5_l__`5Im997<3f&I1aoB7xq={}FY`YqlS*v1jRSsR-) zVsKQ#==idL%<4#AZ1q=mR^H$t2ZQ^OwB&_kivLWmVsx__9r{2n1nxcO8J z!Rp-FidzT5cg<>7R%28b z&zb21aZzavIy=zY9KQ`vyt7F%MOdGAGVMc5)A!=lHeQ~5i}VRLQ`S{Zf_p%Km*8kB zy~1q^s;s11TmFM^Ff(9-13k=t)M0(XjrCDb)nz@dF6)gTaIvm=qYkGPZk(1i;MBY> zr@T6x>|-ICJ2Op5EHG{i2Q^^06|>o`*B$FJRMC9HOt8KTz1VgHf_4q1Dk-&*Qfnzy zO{v!@^#i3=QtBL~mQv~(rAjE}(-)~ZNMUPu6lWKj z`~(R>{~o39;q?FE^u3()nVfzR(a>9NLH{_VPp@bE^Ev%+Cw)IoKaObTa{5F{ujllU zoPL^&LrhnlrPjmT4@SPx z>3iNJ3U=YR^W)6C>78Zkx{$wo(b>QP5T))$z4x7{9A~}X<~ZwZqtb$Sjx4h%A5*&HPc$BHWMFJP@>CLV9cnE)s6#Mu_-?>k~ zl^=1ca|~FOx4tTWBnZ6{0MYNhQudUyhR=b z*W6;e(oq)<$@Z?+!^K!}G}yNtwW02(80lY~sh=HN&O~JhH4e4rqSiUhMtQ1U3fKK* zmL*dQeDnb?Qay&(C0lj`gol~Wmv3O_jejVjHwNWm^ivV>i-6}2zc`JxzsVj7fO_M>>6=W_7F zn*B>LitwvB8dd&jSJCf!{df=TAkA3nMpStTr)tm<{_;!S8Jmn6b@_q8d{Vvb9`uI3 zpny}yLm2X0oJ@u9(p2n%5InSQzH62&C2Fi)qlQ;-kx+NA`(R_Fdq8ftk@le;murJe zG}4Ikv2KybtVJ={-Y7G*M%aVF21Rq`IN5;LxOFP33@=l=VDlj%HI;`o)|4>_S=>kb zW%SL?F6_GoVhQ0qz|mHKGl62=3%|>VO8PTT53@Z43;u(Q5c`FZa2n!F8b_{6aZExB zjrBNGF%`AKchCKrk97q4z*pXQykfN$>e(Kdj|sl^0d~mW1IO!Yh^OT`CP{4bjtl70 z!#z+-MS%xi>}wtCG>6|%gE7E+kFAWycwlgi7gZ{zd6a37BVp0C#J|{#JVPz@!HPgf z!Vi;P@fA*bqh~P+igoYJmvPn3cYrn?jhj`r=(j__dbEB4(dI z2cpiWbol4<+YR(EWyF{5i{EK`gx;}x@H!5Y?T8nuR4E|ADRbXr$XTT>$|MeftThR? zC!wjD;W&)$&B!b&;}M*i+owCo)V23>r1nvUqyT_ET~PA|-sOTh96%r*$F2k(GxM`Q_QRraSab*wX>QQPGEG1ME7r5B?HIi*|# zG+yx?WPQ@9b|X>#1XbWZ8(e7#fqTIxg?=z4CX|Qa1}7iV+L_q!)UM{At*e~1bi^pO zYe?BncAh_mCLPYq$9R^T3xk~mNMMo6Kl+>eR$mvy95l7Bi1Nj`S+v;$== z0)_2Wq;MgaCeuLgS<&!C}vho$?YZZ zP;SHe+4eUMg5d1K+?>5dcX%$0#B|!aj@s-_t=lNoiBfV`q}n2dXRnRe&V=v9Tc^EVhLDqRd8eA(FSWA-XE@JhT zinhn%rS2iH**|Q!kP&XvJQafCxH9{2Tu8%o9R$&m;Dd@1D%LWGr>SH^p{bf4rUTI<4*W ztsIN)6_U#2Q>D7E8VNB(7z?(z5e;3SUQ>wsy5K{K;#K6Su`PS#XBsipv_tIVzyo&y z;p;W*hPmhu>0*wi^m%lvT=gt!GEGlG7Md<2v^^RBSac6j)8=kUo9PG2TdgR@l4`ku zooXD747T0$&TsbaPkN_5KKb+;ChB{L6Rc;Qc46tj=1ho$Ut+oT+L3>I?Xwzb1hbMOpkyRHwneTf}B&DV+|54^OWEb1lH4X>X2rM(ww<11+) z_Gz%gsPgBysr-hp;vlYMhNpCGXPU1x33X1-1$TPAYjZE`UnxRi7qthdhN8d}7zL+U z1}O@$eu3x=Hk;(*pt67gLjuevV__sA(9C{BDSeWxp8b{X)!YlMq@xhuX7i4>YzzWt z^z9uma8oZ_0T{Hi=&lw~*GtWa1uZ&H#9hez2^Cm$c3zT-l46}{4=Wji0d+Hp7eHbS zayDInrj;JTB+7DbZxRNS)i;UV#GKwrduNlFh-q{?llT)ZTrr8wWD)V2xC8af!8*n% zuodL?Iaq2i9$z2~v9@;>y@?{FFLV(2fb|;KaSK|4GBN_3J<%v&rY$(d<_IpZTV*E; zy_+yrA=vdtNd}Ps*AYaxDK(k|aVfQfn;?nhx<1oMsSeZhM&?-n%1jT4c~*pZ z<}l^BEA(u=Ifna$9-#2Y7r{9Nt`A^sX*G`GAJ-&%xh)xUomg=*y&2Lv(AkOEAhG`{ ztiR@4HV0-g!rVsYbh=oUS0<@{E&v=5dMoN!I*8pJfZ9R?@azq^JB1Rr0o zIjg_3B@MOI4=rI2jL#jaIzUzQL(&)V3H=hwRZ+*`uFF)>2jB#8!0HV-no$uZ>z}_+ z$YRP)EN?yx(+p-b(l55`u;m=?9oRwltYh(J64eA$jPyWHn(1zUylwhX>iC{^yKTCwh>m`vg8=lr4f;esB-@f7 z!_P_^xp>RDYwR}X_~7dccecV(wA1cYwx4zHV*L9c-+D@xT7ewj4LHn_wlAlU8>mL? z+-xK1Ofy`y1(`C{1`4&SRen%yF&qk#K1c>-u%tJV-dLA`rR#MkIkxsES(09Wr5M4; z)`s7C_6N$XYC@fL*iQ(?bSFoQCj?`< zjw418f-!xSBL)+KFwh z$&oCnqU3Ov)KGFLOL}_XIvRLWFRN7#B1Jl@R>??F1J$bbNKuEXRjrVsp5X4q8L(9L zYzQp-6f%};_h=TKLmAF8kj1x0N`FQU&7>Y9k^Gq)EZLNjA8a7(3=cSvzcJEL8)-Id zicHsw56zM|EQGMFf0Dim)%@jOh>9l4rULxKpFAW{*$t$&3Qjd>KT**f+H`=ZC~n$L z-LR5-uw`+oc*cvS*QQ8=!i&1d$0-U_7F`c?1M9s7Xp61|WlS=csOLSnmO}I0a`IY5 zq;Hw(WC1Qyv_Q0C&2+lhwa8nGC}^KbsoBngXDPc3Sz7|7Rujo1lsZDGzLW|GM5;Tb z&v}gPN9R4|u<%J#ZDNj+rRmx>I6Ur`O2;a+REWfM9NUHAJ zCevv5YvdxuzWA&7Dl0CkS*|V6EP5Gj;iF=jrF1t}LIrNftB9!`USZl3kWjrBD#QwI zmaJ2-z}eQ21}Mcu#aE-0kMLwx7pDP@<}G`D6T<&Af5FJy+g3 zpMkw4U>oCGJWtYUO6|BR618n@Xq05{<^vPh@dKJ(s=)#Y$BK*0L(ok!qr|db>^7KE zmFhUca1Y8JW!W#4?B~cK3THVcqCM$;7&s$DB>&Td2aRtukHAgZ08|fnd+8-*5_aB zqd{O%Ayg%)V%q^=`o2imuvm5mglbCU*@fB07EhYe8s?==912$6h zmDmCgUsGtk-gH85;#Y3E1O}VILyEup*OJz>4(1_h9N%`Qbn`U`H8yv0k`)nIAjqh>?a)%aZbm>`xXx3i>WO+p^CHod zH=jyuLY!XSPr_)>r@$(dDi*sF z6!m!Mzysf5wp{a=bq}842`LWTg2rm87ta!PdGqq!Py>V$N+}hv4;gVfnz(-x5UOj$YiP9 zrN|N@WO)k<5fKD&f)!4JrXb*J*+Hc0sjn8S*$vU`e&`9RU;EI7^cJeGzvHGf0$i(A zD<5+Ww+@)%d7jDUPGIHb<~!DdRhjA)J+Ih?#3|SLLk!!^Al9x2Ut3S1SGJjc?A)XD zVeIV|>M~F%94n70yj(X4>53t^bdijN%^yrLhSfVUhP@?a42#f5+da;HT_+-ZYkDD* zpabgFd{(cYZCKIPY%bhv*e>3$i5wZR{XOjOY?p{h9mBl`;qrTv$P_TF7~UAbdTg!e zMw#j;XNzwGA^|gM55m$N+lBpHwyuM?+;GmTx#3(xvtT7GE0)t9Z+d(ljM`C|cm#rzC8I@ha+whj!R z^%iz~xcDvwKsis~a-#h$M%u0+omUij z#ZPyH+2#yETb3QT(OaeZnvF%1oe<&WzbKCQ2prJ{J`4K@ljx=GkSLHi6V|$#BsvGq z5Vn|#IysB>QPGzu!u{W94i;v>T5P{W)hImrmvPUFnB(|r7!=Cq~Xw`(%UN{QSph%vLtJkC2*49wX(FhMI^3ld}kmYE#epI0w?gH z)0FlhqHdfMVVIj1FyGr-Y_-0MX$4F)X)~Zke~}?nfI44e9prV%;28!XDqV z==ShTFGjYEbI3*p@6v(jq(M79=f{>Hocc1W#qx>u6W^{+!0pS!aN3dCL-RlhNU>92 z&aPaPIq3P(#EQT_Q)FpOe1(=^azfb^eC#VR_$)gZ*m=v#)=dRjaVRVIJf?6+Ec=ap z1kw@ZX!R34@fjapW5!WJo$I&DT`gYREx{?^paB#}LS&lrlH_?$B!dpj0s2L?=I}3( z4;T5v;W^0;(V3d2f;T5cw+uIsUwWHUYPYas|FF@^1_Hfqe zTtV083ts+`$Zrs^-|HOj`38qe1>7d!?*eMyfY{5k;-yvOs#_c`pemP4NpI1ChUnSdXC$noEN#9`q&4qJcBVc$AmGzScz)4spiZ5-?4`Ck6aOz#j#SI>+g&f93F)fWHfPOF(}?_ke(* z0tP#Hy%VY^iGD*w-YTGv#PLdbs7KxWyQ2I?J-Yhzv+C75EAq>{IKS@&Ty zNfYuZ`5hwvaXq|J{%>Jh(a$ge|0Ccb0nZ4i@M|Ob87ScP+w>csxnufF7Vx`z{Xg%? z%Xf)>`_$|2y`o>Udc(sIovLs43GUbZPhHs=}51qJzq zCPRjtm!GH2Fl6e@IVPD(nUMIWAUi`g6r~#s8AiEKpOv-GZd zeg*ox2-%RMFEE0;DLdC72lnWlB^wPyYV>pRC$d7l3B}<(!ccBP+W0Uh0~KSVpP40_ z(7G|(l%1a^XMpW&uC-rEqja3DJDD_1Z=5D$XfkuM(@n+* zF&aUI24jBCOjol~L4MBcy!_m3eNKcNS`^qLtO(LkFR~3rr{2=@%{gRJqKkUjRSU+& zRRem`3DbwEaJHC@z1p*_R6MX9w>vYefj2ffL941J*~C>VOl&(V|Vxa>}?ohnm*joBH7LOI(c z>+@tbh8SdF@HCjPHJG?ICp$OW#N<$GV`W%OHc3gQDx36EF}~ETjC_+eGrthZ2eS+s zy8=H+t<7kZ-bJCvZGb$OqQsKy#wdfA3|r%3DUz$TanAl_=grjT(EMbr(Y&GdrX|s= zaMLCYt(K`YDI&B-k3Qkya*&wnM(VA0S}2X2A_udCEJL1w%}PDZ`i%TsnQ?I&N0JUT znM4oDft_v{Di?X41$N^1c>WwA?D3$&Ul`&ao!g36<0s4~j z3u(mjGvz$6hn<=8Fn;h6yoOqvBlC$#9ub_gFa?Zq`s{QXW$hr@$u~EN`4DCxauSBy zP=HA&6szkQI-O}kt<94$6CkqDM5;i$<~$5D%};JYykWI=6nH>Epiz&Y*tHFlWQi4Y>uT*>d_cct|qDhE_rJg+#B}$ZZ^s1<6OB+j+DmFknWV*FifKkhPU9JK zTaJ(`KgXP#hmp;Y^UbCLjCN2RQQhqp<~XvECb<*VLKY*OR5}#Qys}^i!=gn(P7-26 zo~+x-(_PLrrpsC8Y-J5(`bmb}l5R|Bq5un11ja3AHqF68cn|n^2+tfwrje|A7H>&S zo{ddZKEJZ(FbBma3S1ua$0j08<=f0aGIm~s=F+F-=Yv#RkXD#aekm!0(glV>TJS?) z^fF5LG++X#wJCM|4PU3oe8@_)tPi>Q8Lsg(DfLM|d_M81getS9Wy1@*uST>48j1>X zX#JuF)moF$oXJ&`ZjgKMQD8p42Nl598H%lzOs``VznMHTAxWkN$@S-%bEnemR%>U< zgq+HHt!2`ad9n#mZ-yz8kIOMDiTN_-w`n@|dNc_hlr3PG+-hx+3{TD$uYB;IRftuW zEe=Iu26M?3Q}qo;j9_>-7Z$pppDZVXSt=%CexVLy8Dcce&N1kw=I3Ng9sq82 z%Hb;wdG#q8;WIVIY;YqBF;3GL5YHmUl2uT5mq!aLOM#J#$ZrJsZggIflF7)mGY#p8 zkSL&-I-AU#J7dMY2IgciIwM(Et|2!cVTReLM+_STn;mY*(o-#Ca0FUJoYXs0P5u<# zlO}T=dbT35$dva6{SM+m)I&jaBEnKeEx{^uwdD3BXWv!DKZdmU!4m)3vaE4JI=2kBegwU^Tu z!o6cOm`fxw7-Ft-KSy+#hFNIqj%1QPopyvI0&8?&pm7jwV1oI66+2okro@7j5MoDC zilC9%8jHq6=#5+8Qwxog<@6kVb}o6DhW*MjQooRLf8v$h~B0$aPXtO}>uOJ`p3ERs$krkFM(=^O7Y7M4Lix+;Zo-o=xLlFye zl~r?0Qr!5sm@z3)(TQy3M13g5dUE#M|S3_$DI@GE|_;pempQEBrs#1 zoEm7H44p>l^d=lHqz{l|bs1?iBm?9`9UIjF@(^8CPX1IqO{k=NlOe*z9R9yBi^QFU z6%!rE=pm1wD4c?%%n=AMqNJ~31#smjkhyo0GSW}>63fS|g!@OP) zh2vyGvQ`h%>rH+nBil$v01ahfmM!cWyGl9^(a*%DhfxP9$4C5_BQ|Lyp9tFFJZ>BU z!z5K=ywDA8tg?0}_Bl&m2p5_qHXHef^|%ibI}SvkN#YoUTPm}Uso4JUP!v&WYG}{N zA$4e|pNvk#_Zjj-w3y8_Jfs*KKcS#FJW$LO!7dP|gM2dzZ_cJD-_D5Mjf@*Td`wDQ zte>RJ4NB1d18HNy884ucuu+1~p0@w(R zD<&L96&9_;OUMVM+!-6uSKGT5hIp!;^`8fAt zW7Rr+St)?Q8DpkV2lygEi)a+Cl%Hm5wX{q_uY9+y)k?1ATsfMR$S9fT)Y1_Ir6jfM zbXA!i;%L@S5+_KpO2DB@;+UjCffx(@R2&;&xa)|?&RI!F=Jsg~WD*yc12f3EW#(l!MWk7WmZBg7UHn`*3KY78Zu8Z^sCTTi}YDEn3O7HHQ~1%U4p2C;qHwFPE7~Sv^h`?(9jn# zt&KBrNI@GW1u>&uo(@4+xv*etJPRY-bVe&?O~Omk_8+hCCW_$uB67 zHgDsU1tggty3+DQqo0EqJ43?ud!z_`*`6DlafCt?`bvI-;Xe3khoB3l=Q_286}Y=2 zzGh-e+a23w)~K3qLudhUoyn^)oq`l�FQ!5k9%9V5vJc>X~eM!&r>z@Sim9%o3m~ zH|xhy7C)d>Q=LqGb|DUTadC&O%(SaT3)DfQA%_huYAX|%ZzSMZjcP4DdBaz8I#7@$ zZ5$WGPjc%PxP|aDOu9@0pMx_==uK=Tf$GsKGcXWTh^*OGgZ9ilrw2=NcNS*SnS=9` z06qyD`!L$&N~4kL-y<|jilu7~ltECMOyQH!Nt5C{3vuCwvy%;wupF+3qgqPeb>l(uS?k5y;dLA@Zba?ED~wsq7qWlxL{5^YmSw;SMJNDrNV@yAw1*c z(94~&A1_RdN=`{5`P}60&x=wLhQ~E%Ak3XG+&$A%8En>fZBS1PY+gZHu!I2^DfeW{ zE=%@uC3~|ZGgJ}NgeYg1A+jr8;1N457P!blo|1xgKAp)aIm034*i*{QE`kfEi_QF^ zF9;mU#~#z0C9%+LmAOvaXnss!Rf4g8a&X0ho&IAcoCa*1hDFil1Xi!+VK zCFX|G5cob0_mEGUBm=Mo0z>PDu5(yO&(O{TuzA2?3is+bGgXM4zEGN{ELYA2k+m&} z&bZdp2s#PEYK3)L^ourLhMY_-o$yMA9HXIeR%~b`xGO~bc{tO{h8}1|>PA(%$xORO z31$+NSa(&{_QEO^q3s11+B1UvkI*G2gOKF=*toI9SEiG43ba{7MaR{y!NY#aY%sD& zk0o)%385ZKN;B9|4h4ZM-$mjSSpR4%hfDpm9{JU&%c}6Ei?D%bS9x7aiUIMRgkj;Q zmbB5NxSHHK6SfE!RU4~8&du#$h!~(QKNgZuy8*}gNQ!~$gb4=I42lx6bL$G9M&Y+K zgU&u=w{9!@ZJaoq`-_v@YhK~;0^ufv5TAVm531y zIXL0KM1en(XtRPlGV*BqnGpn6siR{Avbf+njqu|e#6i>Zu=kZ`Adb<>=m{)N;%74a zcvhUUvlF!flPd^CoFM`;YMChjQ;uEmWbG6hOy)wI$CKn~<~%y~%Se+(jD(9Gotz>u zrzS;3j~Jc82aM^6f+<>RQ>Dov5R!$)i5H>nDXH11AuUU|-vag#p~k@-M2k?1B3jXIQ$$PG zZHj1lYgj}#8Q{m=G8|NdnslIa7$eLPjU9Pmg{9*zE-qHFhRj(6NbM6=nPdth(O zb~Tv^y2-*g8GeMt`g9Eh(TN<`i~KRJsnomh94vLAdYD!Q@-~o%W*`!5GGTur4kg)j zhk^9N+BiBz9x+&snGlm0H;8_;X;TieSocTc&KvAq;i*p%lNWCb0t+$$3#%8Y1raV6Kw3Sw{UV z=V4JGPFBUq3_F{oZF~-#jRZTB#PO;WK?`GqMCS%l1eW~>DUFWG((+~&_AuoZ&?${1 zJ>KfWA*be)Ji>Fzzj7o`tsBJQ1d$&oU})5ftLV2$)Jqch3nG6q#-oGRfKR>fum%{c zJ5=kCypcFk>o@@1VZb2de>z(07znuPr&`BIz?T3s0AB$t0(=$lDZtkNR|CEQ_$lCe zzrCz6rP$a0lQ~z@Gqb{8j6?2H5}aT1P8iNg59r1o$3cEZ_;i@qisJ z);dZ6M_)q!0S8{Ib({n|e!bQaqL!rlZ=yZGd4SIW&i)7O0H)MJ|2W_J05Ay9*8#l) zz6FTG1nIn|!|^UbFNb3*puUO2aRBfPpbhXLABRI~DoLjR>GRZKc-CbK;DdNTXC2^p zz$1W(c=ju(nIu)>k+K}X*YSAZR={p}nDKkSpjO}qcnQ$Exg9<`gieFv5}rg_y-L3Z#Pua zbe3^+Jz*pr#7>*kcxDtMY-d|0>0Q}|PFABaxpct+gxQFZE zo&&C9J>0v%HLZu+3f%R>b@?3t?i_H`9{mWO!QW}%FcsL3aM$p66gZeO`w^}gOy15J<~)&XA)yhY%1 znHF$83HdKk)&pxo0hNK7#WU7F(sQbxqIcqZ0W@0V`Mp-A=4(ZqP3$942 zNAKXdfwfRa^-!i4IwsjdQP$x%)T1)|h&~p$AmBz50x61}KWeAH@yJK--_>1np9??FzE(r@Udpi^#SuO=A5=dj8_aj2c$u zZq%f^GvM(=O|9cM^qJcQAM<~JPr(}hn&5rMc{9>$p~r2;oa`qaW4#9PK-9nCHN`8) zqp?W{KBUj*!0SJVDbkSU@_J4teUk3hq3jgO{-LsZy7Ro`QXc8{C(wS3*n_^1e0$w_ ztw+Ct>Zy(Uf5b$Ih*c&~TXlSa=San!(HO^qZXW1Ti4H%)jR$TIaIY{7^bD8--0;h_ zj-fOT6U10PMSfrrjip5u>mTYB>*4RayXwoYAH%q+7I{DAwbavVqL2_i0$pZ4ViKof zZS4WyN3J18qJH8>?H>WIJL0NB%y;^c9Z-x{c2oEc&x!s4DgM5M_lCp21pHtkoX*h9 zC)@{oXT)Hi5grZS(LN%xZetx>o@wA!0bb*X7k-KOn+x0l;Qk~;-d*^Q^n9l=lZk?^ zzWVwbHeO$XU*4@+M=#=6XS}kN;bQGx0$ma4=#3!KF#muGnp5@0!Sl3#Se$?4ME_9F z#oRpHl<$cZkJ?4`Nc>TZdmm!a$L_$-t7XG6oGZAHE|!2tw1hYdX=&(Pb+P|Wx}Y&V z0)9V(Un%h;|5ohpOLjpY85`!|aCpELfRCj4=8YIT46*T-NE6O;Hg|Z$M@E?qWixqM zfaeU(Ck*((h@xBGlfxJVAv+Ca+fl}Bsm|DVrns*OT|rB+e*$9i z#|0m^IHFJ)NNR5@=w1dLi|5eCG~uVIy(1`lA7!5tkNSRMm&;EOtv3Rr1iU)n0@2o$ zP46xn(T0MyIra%f4QWTZ(}tmZ5@;uYcBSw?joF!3OhdbfN8OdEy8-)1OFWGd4#`P+mW7Q8f$u^uO#gQpUvR2A_RQu zjNuFl^g^Tk!=n8oi`>!$w@JIx{C|~pZ_AzM?eGiSWOJu)n2uxpGWpAs|8*62Rou0@ zyM*p(E(x!GJE9Eq8i%ynA}S z8-I@HeB5Q=>D%GCsvFWb#Q&SVG?ckvySL+WXZah-b7z?ww(Cy+|6YbW^S`ss|4rRH z_xFD$|Np*r8;<+!8GKb|E8_m(cBJyXW9O}9o~-5|L%7G4gY^b zb36I(JVtl+1ONB7>+Ta~)m@0)&C-1}%vHizwr?pxfb?u%2j45!iCsLOQwS+0Tnjqi zehvqHPx~&h5{{L;JlEbPCZv79HSlT~i}y(*O>r9WZ`K;IEpQ);c=e9^y<(5yw_z{Q z-g`WF6~;LnY7tX5es1Aq649^wkp(*gSc&=rhBzFHNj~TVXDX$120(H3rzm?HWee{V zR~LA&O}%s1hI&ExyMVei@eao~NK5)UXOzzq-JD5&=+v5CYxWiE!3`UT@k-bWR*RR11w!);-Sk#?9%i-8d@}aK#`KISKCLzu& z_<4E(XuXSYor7rkxZ*&TPK9wj2!G2_z82*t#Mm~jN3X4o*$wI70O}8$<8Zt|XDp5P zBh;(ht3f~FLEfyLBz-auU#)M+>)z4+M|vGd^}ur2DAINJBc4Udn1Mtp z#y>@%OCh=;{>uYA6WO>^*~|E69m?LNGTOtBzfjreEa(+(l*PP`y)4cVnQrb^G2MhB8-}u>@8Es0 z*jtkfjoT^CWl>B&+UwG_HQUDyhk+0-x#OJIDdOomMLb=n815fg*qFN5+1{t%6M$=F zG|m6}`>zK6tAYP&;J+I9uLk~4(m-*GNG8rm0V#x_p90x6S>y)@L^D>3INCpwrEr@J z`(>!37{rp#eitU|8N_WS>_@Q*{jemm-!)NA@eBQwa&MlMPI^YN6fVQDOZ2ig&(ji5 zKiM~uLApFbzj#qj%RK#d3wbGCr5}qS0I{v8^P`Z6{ibkvm9=_`D8TlM{V0T?AHr7l zv-w3bsNk1~ywZ;;tQ7C}5Kw6!FQ;Yw2@~{qH!aHxait3)e?}cCYX1KW9_4zd-|9>; z-iri$Uck2ntQ4?Hz#jzsRlq9(Hqr2YwGr?^0s9F!SirFYW(qh{z(oQ+FW}n(Rti`p z;12@+D&Q3Xn*@mV1$wFwaY+w$`JHI!9oOzZ zvVSr?vcq~sjI0}8-c7&m0`?X#Lcm7^WJKa04{)l_i@u-L=+B^M=+zk9xqb&&$`UpJ|f6pX)zq!6ix^f2x* z(n`JYUmyI}UFwIw{!%!0)AZjU{1+ib;=gDq2D^|r{1+t+VSht#^)DW~|DpIBCJo1b zN%${O8il{n(ir?VP8u&wkS5~4WN8xqCQDQBFyd4RckWAgGDLb*%EI3?=`s8_9sgxZ zx%kVI3Zxn6l@b5t;||(V9n=8%7e+%&6JZT~Ro{%h3skDf?3fLX);0Ri2YvOy zt*y;KiF+gQvk5zsU)8hPCl3o)%%OCYL;B7F{jg53-;NC&PwR<-^FW&Z=$D?x#3y&+p%zXZ??L zdUZ#UPwkdwyQ_!&wtx4{)LY4U1CKZB^}f25ch6E&Ueqmf$1|EHdw1`ArM=w!+|SRZ zh3Yf*{ybyv-cGk(J9S_5P1P{Z1@|r)b>rr&7ji~DJG{9*Y`yQr1Dn2lx?77r`wvgG zx9DuDcx}kbUu8cYlTo8NllH|u`r>B~oeEe#s@)S8ADE+R`qR%#d!`;=KH*|odf%^( zO&j4D88EJJ-LYf+(&Nqde`HzJ_TiXw=ML;lt+~``=dSyggm1XmrTNAaIp3JRpRwlq zLob~Dw$s%X{T&;=8sFoQqo-?vzMuYG0EWS~G!{%HLVukGC1`)2!9Q_B{ge`f!r=97yTyyW$wZ?`X#-&p_rC*$`2ym@rbGi~;d zySJ@+RPL%))xGB1CU3d*sn=tjjyoPXK78Dyc{A1K{j&$86udv;^V+>-kFQ^P>+9F$ zr<<<3q??fWmqBy+@$#HO=Hm-fZ(e@%`@cu*hR>%hJDh-^W4@~ z-+lan`=_1wu=Z$?L69+fq!{h?IfuMQ24J~z2(+j4v9s;*aG9-i8z z%hUGoi#yUrUAPwYaenZVqh4J;b;S>=kT3puRQ;E!^_tyPlQi8wf4$4jL8_{SC-1F! zA-sd`tBZTr^-Vo;_OERp-?yyWvSzyzo)}e8sekpAr%!&cJNQ4dN}pSMY)!(c5OvqY zz?*$i<+Aqg?<)-)I(^ttuP&Pwy|(PF+$Rz~=pXUz{&r2LE!dX-=Jk*e7{@nP%e$9+ z+PuheX1e*C%!U0w8}wG&&!aRQu1`3cb@Lfb?@4~g9`P9bQJ*FQdSC9k{2hPsjXn5_tKEkF(9%)x&L1y$_Il^7Rs*-?w?6Rv zies%kx?i5Xpi|(Xx3_(tzB>HmhL=|?{3g2Zv>9I*Tkh)6?Srg|ajF5svVII{Grdij z_nIcRO6PfXAA50U>ZeJ6V4yJ5}0oieH8|3vf zet%WdVcYIE+CKC5-|6e9F-7>ZRfpgE^J2qkd!$BKIU0gb-v}VhbFI~?} zQ=PrquUm5Z{0hUCh*s-2bWb|bzQ^L^eV;EIm-o$Qx&>`pM!l`=7?@G&b3FNv9Y<$$ z4vdLkJbT0bcm19nQ9NJm@2kCaJUD!tE~a1Gr^fyeZtwc*`Ldqt9p%3U_wM@PldDpC z|N6>TH})F-nYitp5##6dZFTSa=YQUkaq7sVS5@0zTc6yv*|r5C{_9$we*Uqt)^9xj z(Ph8Pn2MMkMq_&06SgTC_KLW9k32K|aGH01&%Ot~7`SlwmGtbR%a1)*FvrQy>3(Wy`aRZbV(4+wtpHLb^;Jrc*B)_JLQgwC0C>%!zx# z&hKCBdwFf|cBKoZykRu=o44EXrvFa0_Ja|b_s_X}BI^9pea3n{;CC_W{PnYwy3L7y zecWuHv$y)yyfmuinKtKFWp%1}pqZ*N&lU?rxsjRlP3ilg=e>ObeYRdKfB#TO?(XY@^a-7Q-T3q^Z|{$f zj#yn&cKWR@+hSH+e=X;O_Y<0R>Yi-BR6WSmKfN<*b^L&^ho|@c^i6$-E+2hY z{fOt@6Q%FHHLk^1tA}4{68*nwyY~3DiYq;`9QlgGiEINl;pG$>9H^ghh|>}x=Y>OF z#x_j|lxta*EG4!iOLAhTT`-R{p@kACq1jTXpKg~iuq$@ zn;-brpH}Ypy_xvBG-SeBkX^)@$ z#v|8Wv%U0^*RLP?LS>*SvgG^?Z+yJ!(79{xUevK;#p=~_PVnFGlDxTX%cJ8D zy&1meJM&7nm)-NT+i$sX?YA~=z2o6=_tKkQpF3-Aa{JrOU-8d!w&lY2zFhn4ZOg7X>)Z<-n!n{IuRgQ>jt5&t9^3QS zN&eQInse5jKd*X0-Tb-+l?N1h9^@Xub{PA4;P4b>--t%Mf zUBTSj@lWUU33a#&Wb*T(Fgkm?{?s+a+VX#hnG^&`7M}w|4iY4 zvkDBof1z-d^9qGOqHwiyD#`XSg=_o{@lhVSY4Bf#v)98nE&gH>y@+pu{wQaMZ`%C# z64^AqY4>j+#y-B;=%-0?UdPh`tlNJcksamPh?|)IIg)FJhXhXfcM-P$-(>xtrF6|O5PjKazt{g5F_`C>2eL8$JtXMqEY3dvABgM>&)*=3QkBkGK=BemiRLRIMwoX$aL=2ir} zYL-)68pExlz_56hF188^A6*3)eg8*6S9}abDQW|sX-5;wq9$GQZ8|@t@Wq#aLydDYh23(*ZE!Xd&+df?w>U3S+|UMugN_Ss zz6kMbb8e+@l)`JAgA})q!tKr-6pm52%b|@FeOoBJ(K(Uu0V<+yWaBHiEBOf?H~7+& zWoH}~<;(hzjB*kbZHU5-b0yBc5n>T=#)#%`D15ZDf!JL};VNekXWtc9fwI~eAo?q* zbZU?cDbnYBh;w;85jn)v=jbq5ND)o^@~t_M;Ztx9WB^dkb(s*QDms=PuV2bURGwUL zq!K1lMKnU)*WSa=V>nl2a?g(bh%)04;N#4c?_fbl!jjW~27F%{$Hk!?0ex4KOv<^H zsIMWTaJ1gOLL>oIN@{xw!DGk})vRF2JerW|T#1{KGpW}LiVFZp+*S>+w0D(@`9$$KjWm2)=ud2gf2?>H`z z-p)mWJk0^-bFKza3IYB$0~Rd-NSRdNELaqqv*K(%&g zhL87=6X}KB`4VDze?apu9A`IZypQieIN+?OXivU`aFz25qJR1wgsYt)qIrhGHO@^G z_ZKJPrN6=X9nt?A;Vn)N(L6_52s#Z!^E`z|RRuYfGCDzg64&RDJb{Z5Jl{MjBcm$g zTRwHu1FAdv6xFdW#HF14xX&RfpFNfBtVZKH788C&$$U_HcraB$=oXjB<1AEF~Od#&gXmp!sC7jrY#=ti~k8?-4^|Z zcq`o&{g%RxZi`-`a6q?32Pj;n+oIo5xY}{R$on#dYaDKheox^Bhg+impm2-B4biI< z4m#Wpy++|Shnu0-DctVRlxgoFsxKRz8Y;{;DctRF+wcb}x!7!OPX0(D*LY?>MMQ5q z@bV2FRZ8mdBFw%Up5sPV9SsmDCzyRZwLJ3N=gekXI0d};*%I@tLLL7acsV<%794*g z%+T3I!4rm%QGeBD(D}V7>93Si^`J?x=pBV%`i_U{8XaU66Fm}5kztDCz&!{G+Ol_o z!cztpQRXT4cxN6z^OG~FnNglH4?@!k3E&rrqGOeJ=BKBBX8NiMfFefrsWhPo(0 zNH%R2P*@0Eh^nLl{H9N*NFLler8y2QAoI)Zv{e;!dzA3UEoNO-dM4t{n1}~;c|5Bs zh}+CLYE?x&BF?JFqYWJ6Iqf)2P&N$&D1fc`& zv6&a?r5DQ)Vohk|m6;$2o9CwpqDHwcQlTX<+$;dpt8M6An{Xc`2N=cboSz3$&`|{AyjsGHicb`JBc`} z<9$kbii&}K?*E!bVj>OmuH!w;vzjdd37GdC^ky|SNmAH@wyye~p?H69eIL{pu5GGo zT38>>3@N+{R=0LmH`UE=fHtv2h?`aJs`Xg^1G_+_vT5aF1(5Gn=uO0{;4Xd#Y>KH&xf7h!?|Z5w$kj zzG@lHi6lVU+M|}%g^6OVc7PyhSyUTO@Df_JQCc22Qi}~3YGE$O7nU&wQJPkW!J1V_ z4=ZH~CkRaYzGSgbU=nM=Mzj5yTG|Mse=(U976Zp(pph`?0$_M+*5&1|aF6wGu=q4B z9)?Flv?T^B-MH&ucY09iFy&MZ#VKh%>S=U^-SS6B-13S;q(_Ul(SIVePFqg^Rq#Nqr z78=R8i6qzdiTvXc){Kh9qr?Krg$G0+6N5dvSo^TIA7&yM>B%Oyg*E4GST5S#%8S~w z%qa3L&=}QVh!Dk25?E2uC55p%kOG$B#iBo2FGlyE!H#9%-y6z?m=AB*p$%LTWzA)X z6B{y?Pb**rhLLn4)bC<}Eas32ZH*X%-4>21{D;z1f>>yYN(@U=W}1{sHbLT|Sdo5S z&RlFQX6ivU$rX&89Eh?>mzKLih-J!GE*6|lk}2X@UPVOoJU!D6HhFnuE08?qm6$e} zcp|E;ii9TNQ5RRPTC+kNX+GN|7do6i^2CL}#YfIptAk2}lmna7naA2-qCwIOP-v(J z7gO}6aKuuy*16mu1ed!mEnWI~<|p+621P2w%36Kc!a*E4=>e6BlYwYhL=8b+T?tn# zz}Z6^?I4I^5go&txol`TbUc8SpV=&$U?-S!U|ir@o4JZhQDHI~O@(?F&{}1r1eAP! zx#`k3IfmpSb}T`G6XriNpMcXb{uxnYPI^c&1%4bmnTuH}PEgj%VTxNWa*``)jWF zkfl;Z!AYcEwCdwi;@;f2q5Mendu(-aFdyQu7d;6xZYcku7hMW7zNio{QB#e}@!~^} z8P8Kl?^kAAP$7PlGUJB|@#(p7RfYHr)h+rg#7mXwTNdIobKhMH@mcs<*P0J;*o!X( z`==N;;>9AE1#KHRVXvAs}RR1swu`5c`+L6up7!J6?u+D=WQyyQUya( z;ZOdff(8O^Wf`kXkf)gM@HwbRV{h5b%BH+Pjxr3rll8=su z@b8(Td=CI8{$?B@Zuxi_!WY;S@>544+?JdaEstw7X5vOJ{i&p;+~F2aGk2WPQ!bf2maxr4Xv6m?>rU# z0?^}yf0BP#$$TdJhxI~l`x*M0hmTH^{1tr(^r*>x)Djc(}M4_ z@Mnepz%iQt43X#eLciOhr!Q0_=K)FgBPqv2!snZ3X+CDXnRg8R_ynOsI&Df)4W=r@X-#-3}0ewE}4$??%B^lGQ(kD}&- zzCRP6HjB>+!JEZy4gXcb|NNF9$LF4YQdR)c_BHgZxjAv52qUZyBe>NSaras;vZzZR9$*OkSR|Q`g55N z@+IR{8w9^m__qmvqn|FJS2F(9&|hr$2>uD-6BRzYEIa8Jyg}^NBlNW97}cXspA=+d zE$->~0@GKje-QoxEBfJ>%GZpyg(v0X8pf;C(^k6I11J7JeJjXxycQBd^phLux!ua| z&BCW!a8tgw3!m9i-|@AUkGloGrYXqxt&*{>(y7bkUglq^c1wT5=$U?7CpphKR`Zc! zS5FGQQ~ER0g#S)BMv}kE@&nHZ|8D6w8vf52KA+J1c?~>Be1PezRQG+_t_=Nag2ycU zEx|_xH}&OR-~p7&eyd;l7vPkyZ+=FnYv_HV|4|v=Sp!+<2nb#-V01*7Km3xEi?Q2&p>N+AWICQhk5E?d55yks=BG-H!QYgt$?rR# z7yA46Xg>cain{_h+qvbJt`Yi<*EIc@(C-!c1EL30USo_`sxhgL#!miD_}u$N&F5y3 z^X~4$sUqoKS`mVE%c+79!?fqJ*?$7 z^`b`b2EmQ}Gz#vBA28*zMDTG-o>hXk2_Hk>34AI&#~3eF&KW_LyhG$47X0~@8s~M} z@a$6I-!1%&|GY}*N2FeSUie&R=)bS?YufR>LVxCA&3{}v7Gs9~M}_749l>K3{$0i^ z)wq=V)57Qb!vBRen*UElp2vjGsPMT`@F#@6;uTGQnc&YcE;o6XH<(YQ8kTg8p80ob z_{pcm59m1oSocEGebBOpBFIbj^T2UB-M^JIW(xl8wHoK~5qMT9_-m(Ye2&o15qw1K z9JhQlBS3cR{J2n`ON9P`p9h(a*DXM(p6#EZg40Uj6R`N4D|mxthaG|+w(@&{;L4(> zb-zi@YT;iasSf}r{ah>dNdwa8NE<#@z1S}Fzpe=~-SvFNn$Cv5MSm^R3sK(X?jzuj z90C8O@b4D+O}+Rn)0e8N<^`Gi9FI=qbwmGnVY$2|^zGtL%ommqgg$1`)2IN_Tgt*| zAR6JLf*W~`2TuAN7yZ!h@^sV)eWU0{#8gd;S7J?WEvNC5PvDno=Kn;Y{0l)({RF#T zO>0$7<$pFZUaHnx?@b}W555v)`S$S{{W`%{TlCw2Q@`^i}uN3DnRQ28xWIA4(2BD3@r_?In9-$wXe0`f^;pcazuTMkgg|juEYN3Bb`0SK=YVc;H}V4 z0DkZA0i7>_)eTIK_YUiO#VvxHdA0{7!eR(a`7*x~8UJ&;$dmlrAXDxX`hOI8g3s%8 zam&YpLVts_FI|E^%Jk^Ji99m}r$NqCzH5Y!(esnS=LhS8Olj)rv%;rZ>P5Toc~R*9 zyiC)Z?-j2I9yz3OUfT$94hx?#@t?*{-WPnoWe>EbF3H(0a+>lz3OMQQJ5uk)z?+Wa z1b?$3$oIE;_@d?reqM*h_X<8&_@~4k4F6i-RKE82fki^!E%MZ8_G+2%U;U)!|0BUy z3x3i^8s~M6@Ql{?CHafxee(jLzew;6@*e#y!TSU+s?~gW4SGBq08aWjTKYMr9A6Us zJ4-eFJCfh5(C@PJxn20be}bkr{irVrebA~$*9!fnGc^4IrH_9?`%eC6%xW*bDtsQd z^xPqQes!MaGc0_*F7#uTp1*DQSn_{I_{>|N`S4ox;6?k=kbcbkUE{~@Gx!T3PSKS6 z_XIcdd(HRxe-Zp5OAkK=PUU#}9-Zzi=7#-01RoXqgd61J_lEzAh3UR7^e_B0$aK7J z8$uT$BJqDx^t@2Y@i6m2KgaUtbjtoa|27O)VBp+`3;RfCHUQf-+8*m7Ylwr z^RHBUt$OsYOfN)vmuH#2N=+9z#Z1(Tf)88e@-p*5f3ilWTPM6;6Z)W)uRjUiEx4&i z9|#_^^yB64$))PX6E**o@WQ?EF%}%dB*-68t@@Ty_ipcctCG zObYTw!Jli@`Dzj!-7I{%EdAduc#YVz@o#rAj{d*2zedh`g}&P2^DuDoKPPR{>GHbp zNc)F^N57_VKk5}7KNGxTWsvW8@L8$n1oxe!@n*qa5 ztme}#^luCPRl(mBdEN(3cJe7JUmpp5|2)m-MB(FyLnHceNw-??a={N+@|*~q^s`p{ zydWG>h5kH?&zX#i5P6q#fm1s>YWe?8!FvQZ^4!DiNFDlZx>Qf6hFC6S!5KhONnij=l z(UwGi|F+Gs?R`C4`-T_vHq>J9d@WC*{ojYuYchxuNm6Lm>!n3_fiL;Wy-bO5`- zV()DlU5RmmdJ|K(7lVv5ZfIy2Tl&i8>vano<}aL@2*ZUFaW|Ashej}FFq zy1hdK10y`jFn6a1@#d3a^GysA+}y~!GOEo@`pRRH*SQ#oOT799z*hA~FqSulVX&$% zo!q9d>nv?!>tYA-T$qN9t5%nH@C2B`2=Pd7W8H#=<^{Ri7P?)SyKP)R_t-F+b|9}? z(731tJJyC$5Y#oBTh=u%YHU(8d>KPs>lQ3%TB!cNO9~@AQBJPAvZEDyU9VWT+;wrs z<7tiZFsyX>1?yUAd-H-Pu&FeS?Zi-fcSW0UXj|TaVc%=kFKu1pu3x#bb48a+8-A~F zvDtKPLtxjX!TK)7>2ryyR2su$2XKkdMx6@gA={a%Od4doiEyGniIJo$V~RJ`92m+* zFhrI{B)6a6rOtDcDv8n7nHc7skR@T5_BNFo%F+nkVDOwZtClWvF*l%YfsP(_F(g^7 z#en!^SoICXc~4!+w2BO*vLl!qfO#TV4+z^h!yY=_R%S|j+^gPbhO7mnx=}`naB8HG zy=?W{tP-8EP%m3gC>*14vrImaDkRTrb!qsm%3v@s^0K-KTa@znUExDJiqjD5!dU0I z8P)DWOW0O4gR#QIdy*t5t4uPyXptMuU}xs&1c!wRqwcW@axRzIWQzPlgcO#Upkr-C zvThsK4k`&6t>4IHLLuzg4y->hU$u9vU%EoIwRX0->pB$nwx)e=RWi{(!U0XzsA6Hr zOZpqqa|Q-o+WeYFy(d#C3}42G{w)gC3_C1KIbqjjmj+vh`V|7v7%FLG5b`H_VIlE; z)Y1&L^HyuL{OvBv25Gnv9$~F5Vm@jVb_drKv{5<|8qBy{&}?e42;`s{7b*%5m5CH; zfURjDvqdEaLO2hEwqU*prwxa~8_TMtdL|HdcBbuYRXbU8l$6P2G}u~)V9GQh0P{s) zSpyinoq-90CyEXu+o1|AV>UgM2xEvn6>7|~UK+_5wmFG81RFQP z^YH8z(vh~<-efN}!Hv40SDRYfJJr^BMyI(h-ANXZQDK@mfg$raqjFE|kIR*iEfZo* zmP@wPb;F?)wzrP3XB$ePPKF11X$}gtLtM89wR!iEu26ouh$afCSzFPv_3JvjR3-uU zn2lq`Kq{qBiNagLBjJ7s2@`=gv2*~Fb2D4wDb*TJt3+B)0LhRwx@3S^jDjbI7>7WKl- z@D9qfA#}W-r`OPwi(Cz8AYZ8+2lkc^XT`hf@}mhDLn)qhK@~`hfb7r~0e+L*Wh1sf z&&Dxdgz9+)sW3Vp-V(E0kS69n!PKex7Um!u>eCh(8OF4`3^>4-K(8>kc(2<}(I9^! zGmz{{#G`2D69ec=^s_e^q}dVBWZwX08fi_ss%!1~+UW<@*1+mk?e=X#Y$>Y~jcCEn0Ji^eM&A6A} znj~Z_ikedWoa(KvG^-oo0l4v*kA$hID=Y+g*r>O)kJ4l?6^)`eVuf@W?(7)N{vlC@N#Y4MnqmPzOqb!goxHonM+JQ(*0uRUSM*}$rqamoXADPEg zA#%K=L`~F$mRUE~bdL~fAdELnttNM)v?NrZoCr&&dk&p$7kYQBI85E@b+?7k&JRPm z;6zq6sFuYr4~#mdJ(-LcJs9*3H4!t zLCP*HVknsn!S+l+q*XK&N3(;@!vLo3FbDXha9G^Nnl-#HIV%t?7|NgKC!&4lszbY* zQ=56dD09MJ4WUbf+;8RL8A^~(fHkrUB&TV$!OeO=@e6p-_@& zfMZk(my)VPwb~rnjl#2Yt19lg30*7JyWFFOXVdsA%;KQ&lRe2nnCKwSp>@O5^>KU1 ziA|8tM_9ReDOH!ibkw@mrK@Vu zZm2rUZLMQ@>v~5Lh^+XElI16`vJB>+7TmaahFM}EB9u@H(+UqE#X69(hZKpb<>`rz;BRL2QuX7DPi4(^O!F6(+DJwttn z7fSS@n;^G5U(r13=|OXBo^bC;omV7J6?H;R!M0qc6172o_myk7{v z`<_Iw;u&`n3DLx`h4mM{TXzR72nKX+~1

KZW0Y@{j8L8-!oRKgnX`AD8dK`v-LV1~jnw zM|J)U!mr_t!?#Q%haYpyyDJvxkkgXNPRko2F<2NAaQ`SB6r?@ws1FB?S*A3Lq- z0Bnp%uivK89o9qZR_0X-^Sn#th^E|bDyBTM<9`wWVYdFR`@E*4b+Gae6W?61GSigu zAC@1aM)M;hZ0nEsSR!(a)a5#bjdL}FIk+sxzfq_0zvQ2c?PyAUete&ff1CJG^Gu`W Uj(!`NI{xMdH09Y=1nXA)4}QWB4FCWD literal 114744 zcmcG%3wRVo7B<|I%s_y|4vts*9_JBw{)jNB{)`C?X03r}m`PMtbcb-KE`dif~Foe?IJ5cow1w+j?n7n{jQ{3r;;>w{@Bg><2-kSX*Nt`j;T zl^K75beY;!;G7zPNc;llC>|6daVFe+Eq;DPCPEa>q?3@xj=^&vcRE|NIDX31Li`*% zk*5rt1;NVViAu7b)Z$N0oXY5dvsGk4VeJZj4&X>U!U>az1D!c8a6YM#1Lr{bsBH9C ztCg=dA`>ABXW|&(9z0W8`sE#QPN(bE+d1Rb+wF`VIBy`u;TJduaQ6Yn8%($g^`oh`8sSi(^I(XLf zTOWV?vEoHThfXV=`{zb^Q*;_rX?1?-%3cY^`YS-UpY z_Z5ctu7+#6BpV@}kcnT3zrgQmTy)1@H~jU{h>19BCdMd)qr9m+EI+z1#YPZ~^p(=* z*=sURyGc#${t7`Qy@&rE1ff0pZ5_}lZF}ke*a3ZN2lQPX(BJBS{!IsT>N4AtCtzoQ zh5WJ*YA=0J2lTf)p#Rtb{gw{st`6u&JD`v0fKCR`p8OwyZUrX%Hy4EV(!bUL{XZSh z$u`^LGqeMGO9%8J9nkOYfF9LBdHo%vujqhI{Y!iDQy;Y?wnb3wuU$AuZivz)@h`3q*v zbruSfbMBoyzsOl2EL<>k?sTDW-uxMJDdF6LN9WUdLBY%g!u%Nv7R*~9ES&Z5+^KVT zEcgJnkPZbiry|a|z&US@@aT+37tR28=K}nv5N9)eUXfFnJbBi_c?B66lM5FXOr2ZE zV!@`cV9vaSGlWN{&Y3e0VnD{Jl(xY6`1~1@r%mR>>5xDuT)beGa|TNSp`5cGow1Mw zAnD}ERNBc4ol_S$CqFuM)?8sxp;p3$k1s5khwSchLs{c@OoHE7@v z;s5_oH{1vvI&1E%CuR+qI&;qBGaoB1Uc4x6!J@gTL#7TIGOJ+fg2x6tTu?Az*uYx{ zrebu&AUSIqit+HH^X6*Bm`t@Bq5X^0uL6|NGo>{DW*Q5NrSZVb#)N<$(R0=;3~?4A z7VU;;FZ}V(7%t30Z!O%5#YYPLwQy1ISr`f;kUrHwzurKXTt7rfZp$0@B??km ztuw;kEV(vDH3D67Cud3 zY8u`W7Cug4Y7*Z0EPRN<)D*l^Sa>gmsR?-VSa>Ie$@IOMEWDM%Wb)or7Otl-nY!1? z!qpTe6Zgil@P8>xrtKA2_#Fz9NqbLTqVoTP!d42mu<*+iCKL8Hv+(m2Ce!uSvhXt$ zCX@B9Lpbfn9C^niNj@aG4xh{$m(x_+e1%<*n(C&oQ&ViDUGT?Wd2gcdvv_T`AdIh! zg-0XV*ik;>>{SU)%tT`*Dn#_Ruyhj}3fZ}aXyc_7Cp3UmcR5m$PfB&_9g?Y0+Hu(# zuXE@YX7%G_is4KZ8@IP&iP$wv+@xR`QXFKG`mx zw!02R+T~OBx?dtjm2FvekKJSUJ3QGd&650!SYbESwM2;(-A&D=lVZhVk#$EAx-Y`C zyY6T=`E*)+T}!Oon6_JT)tTj!b!stB;b6T@pUw6E_sh&bt@lYpIvs^35mT&43g$A*rmua_H@qnrB zP!z|+iWQ3^>W=nEgB0@ax)a?@yM6x@D>{>$i%pQz)Ch@Mx~0)c?QUxHm9bd4vF>PB zBJNO4jo!J?RJP~N&SmGa#hgZaU29}+K`j8S*Vd_hJaL^|hdQS;d-9?j1zU5dOs>{W zi$~?SYE4o>qhxAzUFf`csJzpk^py%bXhaQrGELe^^5pT$k*3B7L>NOzB34*dqJrG! zGV2UjN_EdAqnB4bKJ4!~uGR?g>0hBDDe|r;De{3>hbJ!9A#af)MMuhx99+mdq&n|S zjlu{2;PMtT(k%mB>WI$ct7S+pu+9ApH5~`&w zuwPqXT3cW@18@fMjbQUQMEFmFhR0l{uDeV+AE6L!so#&M% zrJbgXQ47e30lR5H%8v4m)=(%jc)?r^5UNF#ezW9`vAmA)3kedzW=QjF1QL;XObuPh zmal8*6rZ{R4FO8?zKsrv&i}#rOauQ1bDFs^QOIZ&|6VIr)Hb;85X2YQRa0jg@z%5v9H*LKtS-DSIrvRsEQ%RP~zIhcZa>RpYA zr$I-)6DBq^jRFRy?~Z?mrRoYk)r`-fEj5Ayq>h0 zo!?Db%g!Gqtz+j6NwqjPWhX_^;Ei*1D$bIpG^vHoU>+-ZvXiWIl^}V>B}GZ{Wyx(D zet)8%j{3##XPTE*Y$VbCUyA6m-H$AVqL|PO<;(w{WOv(EjECUQw)*|P3i|{0`|acH zxWFEsB%eqzl)^_bAG>Ffv$v{rbf!e{wW2#bacpvyr}@Y zHlhFBgdWc@9kq$nGUcQ53ONI=@pY_))4m0`?#80ec2IfBO9#8T}Yb7|R$s z&>wiRyZ*|{E%Kg=*r*Rd04h{0LNlGdQ4-6RXa$jV?~CnUK^%|Gk+ixpX>5lh9=Lud%4;IJ2G zXi0L_o5YHU5lfxs(%Pa^NKrNuF>D+fY2rrf?sJ!f_D-4`12uCkZ$PTt0)I~3v2OOp zl?N72C6&%eO7Ny2LhBC-Snuq%w7dkk+uSO-Z$2rN{aAFb)`pdyC>pD2H69{Lt_G9S zDpuT4fj6r!)#z|*?mX?v9 zsY7}V<~rCp8}80Ns2aUu1Iyq{18XlUe!wh)P-1&(44g2rl;#;Fcb^!9YG}?BHmD|` zP@me7ib`XaJo%`Y{SvHq`5C{z#Fm4!aOm7IGjZXun`FymT$F7QpL>%riAiG#bcPyIh4X3pT?;k*PxGnW$WRS97sFZg@8t-@{sTs)B zaZLRN$Q*eiDPt1+qY|4$*%!sQEf3?uBl*j=ET4(t<1vk4Sg|iaB737bX&}aqD@KKt z{ZT3%m0c$1f|or_FZ(>?tVjr|MM&p8OKr$)>C(R7&m)QN&(Mb*Hwd~u98~N&UYBAS z-LYu;`0$h#;k}iJG}ul#fNstQ0EYITE1(@3aw+Dt7;7o0PZX3qjI68!P`?Bm4_#`v4tThbv!h4TAWm;6zhn80O7JtfN+BIYl5D_ypK=7@L&1K&fb%Nlj6B<+zmEb!wR=()6z0ZjgvsfBOM6u#aS4-zAas}Yxxrh7=ODm7Q67-*8nvF;b!~qb+3UjJyvsBP5W$akk zm;53S8?(FnO*Bq|?2cJOsWY}NJ_N|S8bmU|ag14p7>DQPp@{e=A`0c``MCw>9B^nO zUdm{e#F6!~ z#Y};MhCNr#f`<_r^xjP~U?9WaVazte*`pqWlZc&mNXi!l5|AaO#D&yf# zJw*{{5&!)U>Jtu?zwF0s@!po~@_$f->moYQ-QY$St9r4E2(fetyNE2xU`)h{r>Jvw zwY0i6N0zf|&_@X?))EVU=T_VlKM!}+1i^QGj3Q;4Ob*$Wi5xwn&^9+F82lA(E8Ls* zeXl&lEN0VNiGo+f7-X+uQ!)GKQmojB@*mG49Yyfz2BntT7As5cgoAQY zkND+B^h7klq`U~;Jn<3Gxcwja6<4tdfr!r$;T}?0iO%5zJ@tA@{RI>3W)kdq^f0jF zvShR!R`8Owq>t86<#cv!j^fHG`A0oPH(K7$gi;tntavENT)w6ObUhqZzGh<}?0zUI zT3)jmL2o^B3*`*8N9bxFFSuEi_9wlUe4Z+^P^0CpkyHUqmcEk`h1Ju+=ZW_Cm^$JU z72wnNZt(Hi0ESz#;)evZR(RdfZ@^~D{9-9R7^^8sN5}C;Xo&`ut{B`X749<7aKFbL zm$C=CQy=>wpz}vABBkerBwBR9ZeElhbzR?$RNlQ{`U(C7Zz~Suy~Tkn$^G})6NPHn zqEK@I2#n#pIt!6Cv)pS@&n{adoQ~;YX%5)S`<2XuK;{1A^ZT1DZ%{0;ZL&NAcET-S zxo@ajy!Z95L$Z8oAmphwI zCet7;lLaP2K1nt*;UhB3a}iJym*u ztiE6zY&R? ze^W<0slXvRnong$4VQh3KF6R72}}dJxE>YHb#eOkj&-pJoZ9H3JBZ$WOx^uI2DqJe zayv=j9`X}hR&MJ{RS=piPa!$gw>zfzF6R1{CPEwB>^n00(~vr}e5{fw-6EYvn zc{O)Ks*X(lIV5e{u2Vn_6s9}7P3zw{qTRyWOIiJRftB~4?I*dJl6b*og`Zru#eLZ= zp5;ZP7T24L3(=o6rj*l+TS|l7l7`g3}`^`hrEt)pR05@2NVEK$WFQ7eSz5!yoS|hY%|^Qg#hI$zw?3 z`yS5n`LFAKx;EpC_)2YJQ_WCn_H_Rw@0p{_dDQC_Yt2Wi82i=nFpv&(#Wece&^zd-&35QWi6<^QyJKz#gcVZS)xzevWQ&WZaIB&^S(po~WUPdnC-)sH27UBq zS+QV!X&mKvIRiN^zXE)7IqE3La2XG+4FhFOut` z)tMmvbKk;K?!kXsyKyS+j}Bo1>CX_G}7=3DWj znM4skoTL4MpJqex@DYv(n>?~_ux^?v_-@RWk7ME?nW_~QBdD=p9eIWdBz4~gZkJUbx->bP|MD)PmC7$d|kyjq@VLH`-gB&WcY#P;!Yoj&b<~LN6 zEHx5Dh3~iq9J$0N4p9xptOTJt36gMUuo%hI4^bH2m;VJDS<8hNlzK1t*u8kwG}awg5hq_0M%$G4oU z61lTRrU@rbPVNozNliegL?h=D`5TRVolY(xa=k{TN2#32TSWf1Mo!nsn~D5_M$Xd7 zQCEY!6lB=@P|TR*Aq-EGE4u6;SIP}~@)AmZkH#fMC%;AHVH)`+oxF$0R*f7iPt-La zchShfdbmhRIjv<$kE(fj#8i;K)yVyIaw;*|sF8zKkWb|IG&0RyaV8~1{W5^7SCQaEY0D%rD2fE<}l?+bBx@G9y1~xtft5z2tj090|#ts^p+FyoK!A zhrC_Cb{1EzMPl3l3L*5 zMb`5^+###gh!MQE`cWB>zlLVu4JGIfF}+!cRNsRu07tyK2i>@d*?5-Ps7%m{bL3y~6foM3r?r>?#N%^%AXQM0r|l(EF++qw z;wC&)b{68WWR$DbygU=Jl6&x`wTM>c>jI2}0KU-}96ni@ND~WA;u1)wzKK}6vG^~_ zpHt8npewKF_&CCMRh|Js-TW=4f=N}bB}vhyWrcW17M<;xc{#_mDdH2d5*C?TaM>44 z54bRJ=Va`2-XVWuFBx%-P~?N1UCP7=3kNt~cYqOR7K*;0CvLH#G9o`4lZ5mzO}+b) z-*4LFt3;JVyN;XW-6?whMP<{%tE@&XDLE*=i!l89KV*6@ucT$$!j3XL^ktl zc#W9X5i8=SL$cDH&TI%Yh07aNQbi>ZiiYy%Iy*gMa6=u9=Q^96y#mj5N~&2J=W*8R z8kkK5j#Opz3@Hk%OMWpeS_IcEn)4os=S1t+oa52X?h;~wH87Zcg(aM&Mp!bUli-|y zr*UR_o@Bp_=Sd@_jML6rk#7XZfR{7)!7zCAHV!wTZkb4M^2kJ7wzBj@+?1SDY1LQ2 z^UL;3;wxD8+v_eyj>7!Vs(X+cP91-A8-;t@1-B#$qdW!v(VjWSptlQERIE=jpTfhh zD&mZ1Smjsc_QfAE(lxay+puKLco1v~E&E8=3a z<x-O&3?GDAr=ln@$lSTB$ zq^q)X;;QwaLZOKRF>QPgS`k(#kSNv!e38^x9@5rIaU!0Zh*x+87<*BqV%lEzHkvjXZu&$Xc#~SIU=PyMk zaZA^U=h2`oh^xCCQFdTau9E?Y{YIEE3JhSO*`bRb%(kVamO#Ft=d|+dw5T>9SZ`n7H*5a7B0FIo_42f_DE6aA=pi@ zwid1q2FTXJ{X%Quw)m5_y@l$hStR3HIILnMirv&`!pRsSdcjUS%PNK+7g!Eg61|v9kp4KY26pr!i58|7A_o!wQ%7;tcBBon;}880o9yS*V3ac z+x(63<`AlCTdnWeaf zCQIZx@6Yf}=zIZZKCJm8mMvyeQY-xD&>b$DT}d-yEBwcCS~jr~vtbDAw;+&Li6a6# zvC?Q+)(Zbdtf6+MtngQ2t+exo75;Z)aPH3@v|G~1J?ZYjZ9P4(r4FQ_5-_2mlAPIw zNgViXY+M$*SI=@dZ+tN^p1{j&OJucVb|lXm?#Q z72TNQ+8B|W@w0P#u6)c67cWWO0@>{HCbYk0-?>`5IKTcBR^s=)huAx^<)ct_9P>z!tGER%0!%$G!PI1+D zI6DdsI4CE}I}6zz)1J|;5zUweszqFg<`Qz{ZMpKs9C^Fk%Ul9 z+gyhdN-o3}EzN2)cQ@Hf#3+|-EIb>*`H0I_$S$Uh6qUI9aBH#I8n}sC)l6QzYipdn zyca~cAs~YLnr5tja^5TzWMLBbnoVoBpa5g7xw1D`Zox_~%qqcES5v7Gx+h>&(ziul z+DmTu2{mVYRD4GBXyr2wOlC!p_P<@$OOjR3SoHkk;!P#i@8Nr5SZXf%nb$hz40np9 zUf7MkzAh?9-X_VrhU%(Al#zwdoCMg*(L4I>sLDcmN&4qAF z%07c8m5Dg0BFIv~*-@f0t_XJvk#c>Z>rhnnt-#r<77eir4sq1hoPsamNwaz{88Jwx z{`>8St$Y->W{9oVV!0EF*egJ?f{wKGF%Qcm5z&jJv4^3H-2*xSI0Z#p`1^ z^6;(3V+5-6$su(v$zR!djgPS^^K|q+AjI{fNRL;&Wi1;0R+RGr+!b^MyWS%nD*Co$NmtX{qAwAtSjpsG`5e$Ml_u~~TX3CIurH?o%OcF1xRv0p zaDYajo~C332&uURhjCAPgc}(Mw;Gg>eoRS73>f-0V&6=(be&d3v<*a?qSM|WTGbiW z`y7H?p*@SE!0#x)?Xl(hd8`j=MIUq$ebC!TN&VDoIN$9tr}G>6MVbC6qBpVVDHKhsG5AUqdhJNb zL{NPb(Nrrm_@%Q+EWZ3}!)JKJNE6@6PThQxL37#uLgf@o$7A4D&XYOp*h=IZ8M!Q% z$UO#uTn(~v3$A!q=0gzL_{f?_6A-u?E#XUfI_r}vcj;*rg5IMC*CAM9yE294docnT z%%BV&q*O2Ksh&a5WxJcFI*e2<4ypN!3a}jq>Y|hnbO6Ke(SxIj-A{V(HkRqyWR~gc zl<6hJsfV{vG2;J*Y}`ZsiCATwZk$noxQ8r4loEeypxkE|z!r_9>UtzlQ}HZ>cTEyS z6%3h(C_MCvNdXX#@M3;JnBHx0)n6l)XCUXmGQ9fJ;)9#90MCJ`F4)x#Nam`Ilss{p zP@Mw#igkw~sSheo^?ooO3&XK znMmC+!4up7S!hvsiY#PN<5h@ohMsDjFOv_d_C#IJb{yn6^ncz!5I`9VdU87)OpzT)04my zu~-rfnooRs01H3Z$A?(3!=uYdo0NW3y)5@QO|&^EIM`W6uyZV4P(Z?y05lS{0$`;? zm*YSa8W%k$QtsC6nh>9+>1gi`N^lzq z`PV=Ks%=}*Inw>}NaEW9bF@%ciR~BA^7}~aJ%d<^dywMN^|-gphfJ*4|J)av!hBs?=1 zYAbW7{dAwh49vEUgV6ZM4l(8)>jz|uj@-kU^Hv7clcj9LBQz+)@+`38%2QAmcw64r zsEZi&yhhFA{4ELn!FGzSkQHFdE8*Bi>JrtYL`;r$aoKL53ulbWb^&sr3;&EN1Bw&W zF<+uqF#zzzIjJZSmIh}$!y)X~8c=_N`l*JBhsbD1P>%A59=R5g zzSlsuECMs7Trc@bM5wpol^hx}Dbw93D6Kmpy*qXM6peW$$h68}Ek!@4N87dNQ!qHP zoGOa`ryhMBW%3172d{GIb%}y{5QM-G8m0Uf3Dp`*II8d96&reftgfR3SkPj{@L&9J zpv|Et$+t{oB6PQm$9Y17QbS;xtyI>bQ0ij3+Cx{5;>tbbR%E9{B|%B7*49vTI)dsw zbTx&pvT>!RB4^B=Q6v2xO?Yo0OV-SNE4Ar)T1EL97(qlVH|Xq)l3d@n;;BTGl+kC@ z;6!1;V97lo8y9#5rVmnC(&;*-PYRvnz06slWo~w4iF+YZ0WG~;aZy-pLQ}&*60`7X znN7Vl5szg_V^|N5>wq|x0|<~7zF_C>mL{ArvQ^Saw$$OoR(o*A{1q;?SYb@oY^B3MZ;uS?XooHC`$#q0C|$4JvXmb4?%o+ zlt6AUix?gNWYjPDGEgYklZ5*VURhH6%ywEz$eQNugY-?7w+10A{M?p*5G(02 zYZtUU1%@=7mBYS)nhK;yFCk$@>`})NmI@;GnFGArQpm9mxrLA!4GVTa_AZoMj_-}! zkm=RzG~nmu5NQXQUj#&COGY#^aSvE65&wy?Tc>TBHyi%M36gtrl&dYudL2uqYn zi(;nWQd}SZ+LfqkIS=nxS?*zx@hbr=lw(1#F+wq(g~l%cv4%a0Dn`zl!ud_dST+=m zB0w|)0!9tN zDTJjD$Y!BhlyO=-=t}m;%d#&8>xo3R;??0Ea3fOWxRzSc!AC)AC@29GD9DORkD*Aq zZ;Rr9DH#6!Jv8=ts z?2SVjQ5kHPRy49|{6L}GL%c3wQFv7Je7y4DW+2NeAknK6?0wysMIdHuTh@!_&;$ zDMQvL(JP7#3cb~-ny~&cM;>KGvIxXG+%qvDX8Qsox_T7e1ER>-j+Fz-6gD#1W%&rP zChtdRrk;CDcmjD4v8)5m*g_RGt+=N9~mTiZJ%_WmH=e`C>#xj5TBAQpIg$|hR9@MqRo2Xq2O;x;mn+sMx= zNuEsDh{ek;K7_7E>IsnB|{R#bJ<_A}xPHB+Lm9ll$ZYRWjf)98Cli zmGqG6-m-yJ_ZTjhIbBM@+;g9PNS>W>W+`l{!R|U?vZw4H?Qx{SrsDIElHTCpHnq9v z2gvgC)67`91I2sT(7SI|8Eiuge)VTq0k@>}Y>Z`=R0$pux1_S(u%uUb6j{>WSQIrq zvZUFFHF;No$5_t;bPxA;n3k&vCg_(knwHz-9e4!ew4`kHj6uiNrx>v`d+UkDqQRKi z6iUGZ5z9$bsPGk#keAutS6Y!nBQ=m!rd*A2ut!qv@GUo zUq!ZjUTuMXs9SW$|LZ0uPd>>b-`woAgU2Z9>d4*4gmqSe9g|sja-Ua*_W`%Nj+*3? zxM`tRqYg&wYDsL$Xmw7eOz&rzS{D0>B1=S#acG|LJj_Y zLdktTokZP0%(_x6G{o(!aIOxoISnV+!H7zngk3FVSy(7^10{D`-n@}zG7OoBuhxqd zJF$Ym+l`Vx86|+d?^RNe!Ui&U40r__Hx~lld|{18PWD{~tvyCe+?MN#xz>DF5XK$A z;EmZnU&AesCq}z$USuRVvmoIWkPyNZw9@3hR^{E zCqjiF3Am>XZKLGuyJMcb!r)W&rq_~X%e9Na976zmvZLZ2hx_RvjU&n~W0{Iw{@N~o zo-J?6mA5PD$VL4c@2|SPzh2(!+8PBdX9{BW-aZJ7t6Nu(VrT@@V+x?N0pe#zQQR#c;9UN>?*+?MV6 zfeK-XrolL_9kgX|Xx{X+lvmg?LVv~l(X33McRvtP?sg^bs-u?^`X!E*fL;@V zo=FdINpam+_GBehbTBBcgc#h<8RVhAdVm;USvMbfZFrd(7K;JHay#dYdo!)Uz$Cge zw)70SiVl3j8yAAI00-3%4^Tr3Iyz_)eHoe>8Cwro9W;HKaaZd&nrgHDex?)Tt)Wq* zn;4p&Kv&VBI@ko9gm!T>jr^tUphq$^ji_v)W;Kb=>!XO!qd1yu;m#0rm`14@tLR|R z=ptfZ<_usCeJsR)G`a=_RDC~@PB1c9ejHDQLK6$>^FbyR)ov9X4EjU}YiHSOKCCv@ z1;9ad&SYSE+)zb_YSIcX64|S|fP+b$3&X(ebbUcEU8zGjnCx>X11B4+qT`;ADpzf# zSt9C*N2UK3Dp>stRnJhr+g}E&ouQu9^ZL#HlG1YBFx34F#rn$!#%Z+@w6r3oSRk}v zA=vt;_fxOpV6wE{A>hul(L`1-FinEnmz^=D&4gA{-|34aIPr^UK@G!=*wZy{E zp@ds8H6kuG0}f)q-?c}YZ7`sI#ST3G!}#4J6xGO3%pPgq5Y|hOJhib}?gV`M9UpROsz_bsct}G7z zG^`cS)C8{|l0kilgXaT0(FoQx{RP9*-i}ptsHOwQQ$f^g7~WNaYq02TWWjyPaHk_^ z&QuolJLZwP$~k`Ty$1Pb(kd*f?5~1FAUiRP3M7pB7tUfeXYrDe1sCB!5YIdp>a}NnT~Mv`6R zcT@e}V^Bf+Zg~(-SL$Clem=?u{7Y@|;SC!gE&rPd{~*JoVY_A$i{I!G5<-Di2BdNA zH^&-lDC#)dtmb$7k(5x>M-275dEFF>TE zu3B6}wIhryc-6E9O$%v^UQizd)yvF%B-NfI76#RZ1Fu3nw+RN^#DHyz8;+vqx(3v9 z+*_p~ZMCDl;$CFplGRqxp}Mz@r>a%&Wq8+ST!Tffk%h4*BCD;ULv=b1Jb#j36*;~c z*TBbw;F%vEIVAKhAc!YP)Gto5mavE8x7}?h!tb>NsyOvIj&J37PY9lM!@MV@s;#0! zbt(>A{;P4N-plbVxTf-l;Ftyw$Hy4)y2bG-NI;S*I#gee0~g_1T&bTk z_t+)y#=Ld(@2Vh(rz`bYj!)v8lh)86@h0Ghj~!Y-6$E*(HUd z_R*3cnh|hY_U9PNs;i4PP_nKnI#ge$7jXrz? z4c0g*Q+=7^lR17(TYUKN6&yZpAp9RVK9l3~jrg!4kd0T-q54J~coC9`MK8`m;w<8g zEZQ$ZPz37c)vteGD#+vbukJFapgkvmdPsv4K*Fdma2ENT#q&lMT!fCD02(vYaU4H| z1?!dnRcCEMi1Rl@N*?=+~O z{jM*Frz>r58rM3l{B7~!4G|zM|G|VG$MUCk{}!<@j8x&kv{2yH4EVe4{?<^`k>h&1 zKRU`#R^8%wH%VP$6&(!imK3kP!SJqfUR>JOEa>+BPP--f)fpVWn&S(McwGeEZmmdO zMTctA6R)vBxKgjufuwEXWN{2`Uf55p;=4H|yS;xa;kZ!_TUI*_-8q80|S`)z0S_E40Kq1gCzdzMkd z%$*p>G)x0Q6&^E}_Umj`1Gb0@u<_-n%RAjaG7{fPne2o#W8|j^l z1q~!sbf_MI1Fz)a#9}FDv4^vG(#XO%KGHx^MThEpbUf)#wQ+n4$KMu$XGORttO!9o zNupjl%8H$ z_8^|F)M}2O!ts?1|39{~(S(13;i;YF6N}&I*|T-Q8PLvvzuV643Pp7bWcSQY~1c$bwc=}$%$Mmr~OrHT&KlXX0mS{={v z$s9j61kddJkuW?EDDXujQ` z1#TzBVIlHD^uP!(P?#7yl|6!K&zEIR!hGLE8 zwGl>L83res;i;lS^}{-tw5}E~u&bDtb!rHnS^SG(<`%@0@Y-H6t`d$sWo*ngX`2uy_VJD*^6ktWo&9KV|5|K1iKZf?OAGmh|6IQ}h; zpA?3Nx&4!=U?9>~(V_Yw9Ju`B32){2bsXO}4Bw8q1@UyH?G@uvwek;dQ~r+4Z35xf z9w4hBb88_MzhQ0<=z=rg!wmSlKKma+QE3dt%x#cSR=v7;A5FJ2RdlG%*YTuy_0)dW z!Bz6&{*+-Xu3>hD{QD|8RL|4#B)|Fr$JcWFe?sugT-JqIY!FY9sE={{W{#g{#Op=i z9VFc%RMDZD)WvK3L1HnGvuNflZZ@)Lzk>|cI4M&-v5%=>56AzIZd3s)Lb$~Shnb0l zf1l$|a{Rktcv!5$R6zG9RdlGHjsur}65;1^d@IM#3B$Kzu|YgtsRKDaIg&7DxA%RdlGP;_`w|B^Dbvi&)O0 z+Q_1Piwo8mDMMv@^T7M$_$S)p!!0h@&CekG2%di`#}5y~!{R<4LQ}eQZ(Bu&>Nz-Y z`3njE>t3dUbdJ9;#GnE$fB56hAfB$&4IDpHD}P&j#}@Yp;g>Kx^^sGE#cx>LOkHpW z%woXbwYb@#s2GM~7I%eF)-a133RD#x4AWSocy-%1OkJ70xStJfqppspu}FT^!|@Ww zyN!5V1a5IO2T(mH_p`5eFb)=(9|;=W-PM|ap&bTFuJF5#cy_+pMP55uF6>sW;(i8`9&OSJNb;gSC_ zmOtI0SJ9z*0S;V$^9kRTQJFPF6$89khcisagl6owW~Fu=rHYEXWT27eNab| zzfhMl?xd|EtiEkhA6tcYVn!v&SxN3u$#Pb*d(_Qx*3Gmt5SDI2IKy(y6+g^`^6au7 zuWP4b55B>)`C9_L#hpwafXb8#ny@uYBwGaUvR(b7RfrTkB!fz978p*ku_o9Y9| z8EZRJP0Q}fE%+&??ntD4Llh!Dr5bY3E^DaKy{YUa@MOHdO)qdcuVNny+AE*Pmi_9L zHPDo{bHp)h9Duz%qB7OH@pYK%%ULTYHvT6KyX``nK1Q!o3Mtpo@2wd{*q=7a=~k2}!inq)8Mw)suM{1{Oi} zYt<@gPEu4htRda|8Zi&nfLKc39YDEyqg>d9AT>~b-#TP3USH$&cmD=M{rPIOs>JSc z1!GAk`>{$M*krt2)l7T698h=uO3K6TC3oUo=qzhvwnZ?x7g|v**n8{(eVXdoYHSN2 zAN4_TbCM*sn*=Pv3VFI>@iJZwb$F6~gsiAb%QBt6StZlJ>sk4*k#C)NmzvgJ;q_T; z26$JYY@Vk{SCK2`~w4`cr_sD~-gm<{7Cne*PIpz=v&#T9)^g@fJ6QFeZ z0+i&Ck9aKzVDCh6RXJqMF|?VULj!H5pBpdPUJF|o?J*x=#Xx1GBlrIfFxU^2jW^Zs z8G{?Czl8NDm268JdMBU}mC0;HEPWmf&P8JV`+s=_Q^m&S$k;?-dXm+L@6~LI$jSJ@ zIV?v$L0=b9*R3b{IxXvhU2(*+Vu0-8dTh~A>-@6twk*D)Ud#p$;^V8$buUM&z$W1K zbDfb1y*`lRnHQ1kdAO7BUDA#f_7#gwG^rrijHi?MTnnyHm?La;I%{jx81R)j$&Cw$ zUz!Fk=LE33%#yM;EtX!*sYNHe$A}lU@tG$#sxHVY*Rjrqc523}OpqQsH7m}nP8r*a zeiSR5k=Uo_T+#QgR?D*cEC2n@J2%?T|A_CI)wN!mQtvU3G1X?vKczIutBQ2Js5RCaShlLWg1_v6dMsN=waYg&i7aaIeGc9FzAS9Y>O`f?PD;R5 zI)kSuef8QMCDR_FCzPQ&r@1)&35pMJ!nBM{@{`Qj~|41 zWd(w&x{}%rwn}j?Oi(`16Ld!cFTJVVF8eb8Df9KjhbhRoy^JewHDFrrHyKrh;lt#} zn2rw^mU>VGmu<;WD;0M&+Bl3bpLS+*$FVI}u>I?GP}<`xU+ltC&31&ff>a1nc;k#` z?}TXftTj&OAE}cl84&@@y~GA1E+3-s2@_-}6-bEfDmcCD3%#U4DH~l53oV52$?KM;M>u52A?x; zW{NL0iqF?&rf)CWFq&RA{DAh4!N!43d)6ic*lfDCNg!6U`Bg?O){;c#0h%9-WNmG<#I^aP7d`W0{{6$H$%%bm< z1Bh1rWr*pjY^CcnxK@6mD=)4%4{QHGZx|0A(92-uSDkGHNZhGNq>dw*_QZqMQauk~ zchGU&BO3800rdp5R}}37gTVzp4BjOf3`VKsR9uVx*=5T;OjTb-4a8;3^Ai+u zo7wvWA%?Zvm`z_@+WWyM*lN-22kTL{AxgQ2ay#Y16`8zx)1M%(n~WNR+fL`8Z0v7K z#ylO#*vkgAv2rbJIc2k0QwuG*cA+7R!HB-IXg9tSw4C;OGmXkPB(5U&EL%Qer#=7P zHSomu0h_%8x!!e;b(SvG8<2&37o}7uJx}7jNPh(Q zma$kZ>azWGkOkhwz>e=3@IVG)jCy-r&$BOb(pKKq@Sfpd528j1qvg1$9BlfU zoAJ5xcJi?B&gg(){b>+FBp;)lSLe!m95Niey}oinV=J1S&TbBQWUB8Ih~%qq;P3(V z!Dz9P2JXXRQJ1aDK^DkHp#4IpJO!)kj;aaqGUI5aDfTr=3LOX8t-@~Bv~_3G`vE1L zKn@-@=BqO167;X|i4&tf=`IAj`(is9WO6SuF}kw26$!esZUcAYt;q65@BA|`HZV$e z**c@hrsbt!&U7B%OMo2dhv*<>V`uYx?~-3gF<%}a#guIjm`j-Lj%NK0-@+==@(FgX z(9r0^QoT38g7EGyFyzFqdOysDqVx`DZ;5V0%~;ZDu%Td?y(3uFjA0U#p1nZgOy%PA zVV0WAV;;DuRa!LL-Wq(6)T~GA&^M^hMJ*a{ei1<* zirFrm-z|CW$56W;Zk_tCbH>;_(a93+Z5 zg|j*lT^0onBj62h!Ar_w#rO6Vzg~ve*sS3UnE2z*U_#t=37-;N zMFS}=R^_mZNU?MpyD*DowB)F;$ubb@g-mo|!Lwo$K6-+C7b<@<7SGWKB9|kXSg|YQ z`;edSveNe<@hbm2NM-koi=i7{xmnDv6DzO{MEt*z0B_CrHr3O{@)>pPTak?*HfEdf zt;plp(V!maIkZ48V>A0!WHE!76Zp3x$50I3j{*_jiOkO}IP1Wk-I12zM3*hM;#6YE z#nFUK4|0fD5a0DX)L2G6J_Fe-$6xvu0ULd^RvBUCh*ToeNz%cPRQo{m0#L;YOryj<0Fl_I7|TGyhm-i+7-|O_ z!k}9yw`60jAD?D}rz7C@b2}psBr*sB`z#~K>lrygPi^L@*D`Vh$W4}uShh#MCd*m< z>b4sKv?1Engofar9rTGFZ2I`QXEOZAqPvx1rgC>*yzraA$~0vtRT7ND^7kD~w{iK} z=P|{KXJ`uzvEo!ovB@m1?8hvw*yK;Tlpbpb-7*70Wb9d7OVbPS=WoS^1|ydWC2%RR zt!w$5)Chb^0-oSG2uxSYVwJa8?lH*S+XAZ6%)*!YAl!^F{OfX-XDEY@!x?-|fLDVI zHc;t*BPshhXe>j zN+vu$88D1eV0YC~V#VRnviS&Y(^4o8$fgV`*ax;e#iq=1TPhKhMOQm`_(u4ih~+$5A;vS)rVQWGMC_Y!ewQciCduQ7rCl?6Lq;?OI;MZ%lI!Nf@rrCsfGW`R*j{y<-0p4DOqz~|7LzbSn z&J~rp<{Z;Dhdkg{ESt;W%EdQMugq~Tid9>S;YEnb6%G@;s+hefy)=8ZX=DQnP|v#$JZl73~m%F{;0VN_{MGz?Hjx3&McKI zeUxcb*6wTvrI*F1L(uoRd?viATy#e7<&ovZ&v|>v z*Mwoa$&(YMzJR#`%v*Qmx7|n{?6cq! zmVG}xavmZ{FPu@wddbugwl)Hf*W(gNV6K;nULEO$vQnRb!~UCk+3gJ1%NboS)reDC zm|pHhHolhv{Rr*Xk;6vVT)7cF{BT9MfvhS8sZf_uYph>R#pLyu4telbROb%)X10OV zxrT_Me&-sn8Dd^`B{Y;={rtz-Fs-c3nn z*;QXj+0iJzXN%S}FoIBT9ryr_d?|p)V~BDc@g_&a<(E|R!DoW@X=@BV<*{~wf33zO zzEF!jpM3X(2JZ+BriKO+Lq^Ab7AA`@QHs+^n^?eFI6SK2OfX##O z_37jY_{U=D%M8Ih50}@}$i5wo6gwKTWATaYC5UBHRR9;^dlcIMjN-tlK_EukEq0(i zkNGpp|4W+B&e*nexMwN6A=;NcJ)#B`=TA9-bojvH6&TUdBXelXfFOe;86S`MC9`~R z3Vl(;kx^fC9G}A&*_a&_LB6qAdY*cof3os#kAt^E6Z@<%*Mt{l8)7uqt)0UB2eBO# z=7k`z{la7z3ghr(r$+`$UF*EvT+5S3Ebb$* zuU?83-?;BeMhn>k6JwU_J%<%S$~GoD?a#!C2SF@!*%BMAf*&o&W6tz$2Z=?3-i6W2 zJ^=}B_oHNtofVl~v2D}{(^a*umPqewh{4q^*T9C;ZII)eHolTW=^XZM}{FZHEtxhm}f@(9=q_p7PQi&cdRy4bZL_lEWEpTGu zsZY+MZ;tnY@RUEcO?(E!zB*(+ZlBZ8C|tIy0tIY^gC{sK4Q*M>^6pAv|IEZzyJAua z^O#rFo^K}AJUxgh?Wc|Hij!&-XCbmPi1Wi-66YCYrHMoSg!(3g^gSJ@nR#IA7t0cP zCWqi*leQt3h`TIzd{G8G_`I1-mYKMqA6L=ov|!y1;2aKs1Q>lcurU*!tJ|{edg3rF zz~ROa4(kjYd<{&7zi|$e7>7taf`~ZCfLlVG#>e76ds8&d-8#kn15X$R0deVS;>) zz8;CrCj|tV*k1CtS@I@x86~G5m!a;KpfY}~V=}xC68JsLWH6J#M1!GNQ5>nJwbFie zOnKN@y{r@|UAApot-N#ioGyy~0Km6+VoZQ4(tmKD8}%@~gNx^+TC`etit&p;D*9T) zV4m~eSafD2och^yR{rs3Zvu~7!Q%2FYxZZ@1;tu5RcqniIetISC_mMXsi0%L;qL?) z^NB2>`Y{6DNoenZ+V2MLXk(uaWCdP?ezq~QD^t4ri9oe$+MZ3%yQtbVZOi=v+WrZB zZJWxujV0H#O-kU}9?NrzW;u0()jwfYr{SG!^7HAboT$VU*IG&Ye*sr~YRk+-&DbH9 zC2;5pMlUw2Po6VYMd>dCXjW!DycEg}4Dz*vtcmibi3maMfk$Cl6}m2T7Rzb@MDi3Z zKU`i(5@0jcyvy1o0NvuXd^J@t;UkELpmu-!zhP^5{~Wn_=2M0G@I)2$ZRYjO@_7gH zp?`;m#0HLabWud#kx;a>>MR%oB%x_0s{COP1k+=S6x4~|n}SfFnx+#;EV~jU?=Ns- zz~l+WB+pzU3=c7bL$lj8gU>+L&ES0myl@3|Gca@h6*n_Y%)=6y#>{A{oJckEtgbCG z_&*_u%l2K9R;X|3f*JgAJl<{3;LrTP#QjW*R*OzBegT8e;#t1SqM5-zUK23*8+hDm z7T4C`TW7Uf(t{xDCEbWXh{5*;cWCnSn^;N9(7!ci#_*EfkB19}ru{aOxNN849D%?ZQiXkhu`(D%^PG8vFt!eUN8a&pixk+RuF&D5;Idy~*O*mh=iL zDa$CNX`i2IDCu4VSV>_Uh8Wbkc0o|IuHMKLNp9m=1zQ)rFb;Y@F1=ap zgNH;xZIu2M(M^^IdjwinpJ%ScJplX@jK$3E!QHSZQGJi#Su@?18v)@>WOE=XwNKU_ z)s;x)vaNzU!*uMS3)Vzl(bB4SLaBx(5(hERM8u!L^|=6@njMIV8+uK2)mO0M;-WM8~* zJ)g`(TZfLUF*AYJekZ*9ZRlICflT0P1J{tgbpwa?XLR(f*YaTrtXa?WH$*pCCd3A6 z-|{QQ{PwE7B8X#s>vYa{8%xgi{;sZu1i#(4-V4*hKHg%$aGncf7BrlDkdMnYz5(_^ zPWd>xV1`qmrB!3_?zh2kzP*7NPH*IndfkRlpqiqHB$ic!6zE&~YT}0XtxwNrx5t?W zvTiqH5MX^P)O_`0bk5)Q4)~VdTb}uqBXLuqHM_ zK9}vYI;|$Q(gmxDZ{Q!0iKs3$q$cizAZWs?D_KosArz>IWkeFoQb7vT#0!i`+a~;L zLAyQT5s>wo*o;8PDA$+sZ|=`DA)}{j%x?p|3 znHNfP>wQB2dx?cw8-uYg^J}l%kzcuDh|MKTp+43T1Cb zXVsW#<*lnP#4z-8gOMqcjOSSeN4YQiF^$-`^k#J!A6_(VlzxopCd~ z?Li!CT}wFMBUaK1>*scU3<-X_bv@jhT2~k3##`6F7&^p1o<27 zjX2pD;PieD-u&rA#&?32AF_~0g5R!*eF;<(%aI$ei9UhMOpu4WD&Ijqm+gCa8UKg8 zFM*4)isJoPMi~?aw=|dhR7gn1+yitB1QZMr1y?jg7?xy{nGsx4Y(OO>O>HqNHJ3Kq z&D7Fy1+B~_HOopZ%Nc1g%{`s>Klk2mm|?Nrd%yR7zxR8i!@1wN=bn4+x#ymH?)~Pw zAM1&qD8YK-FE;(71*?8`>4|Iz0zdc0N3183ai#Rc^Mulr#Q>%B#3sh1zMpHI(%_79 z2WvP-Pn^Yti=P|7`CB0&n!gqL8Q&qS>w>cSNIK{XFP$?QQj#pJX`cHOd8hMmU?`aL?GZTboQO+mGu2z|vDmK?? zV`~=UY6N{ygi@GIOwPu2x_IzKyy#!|i{7t+)bi}PK{$k|-FfF!uL2k!vWs!;9lPz)zosjSv;+M^!a2S8}V2BJ&}W;hQk zE%^2a7sGkI12ddo-(iNc5?6}h948d)A1K9xU&Itb>Zv=Ij-Jq$o{__Y@{F?9~dm7>lvLTSn#0ZJK%s~D5|>hu^-<8UREyt27G zwQd5hyd|qVl=|1h`ZM?ZD8`l@13+Td%|pDxR63UuY}rwXTg5cra`iU>Iq#|GzlE^q zCy{M!cbaKjnT~&L$J#rRWwYtHBV=K*y6tnG*O%qhpN?0Jh1s%-T((F`fp(Z}CN7jM zr-AUBRpA4<**^Q7ivxN6EoQa{uvzNjK!$M<-e-6OP;YU+jn*-<4McXe>Q}pRk4Uvp z5N;z1Cwq;k)uQ=U6HVElZCSI&i~69TXp-RG4&*!ZbA@USYU38)Ua73s;=hG_X5Co? z7p!~EP=Z&s_;SF=JL-l8A%Wd0r!B!tZSw;%9}NcLcsfZ zqw0l#UB6*AcMA@eOwzjkl#9(3@+wcWY-V$ByrJ0KSe|ELdG&3sJ6h2|2iC0w{0)E|wX=D(W-qSh&bDh(qwHevfs=_;p&2?Jm z&0J-3L0{MOs;D@*%19L9hI5Wh?JldhHJ~!?q`u*t8cnV;4@z=%mAimbc4wMlM_>Z76V88NqA11xHjB9>qH|;iQWL z$$(7g%!T0U;y{}4qWKID2a?Sv9I$2%*k$mR8n|N53p6O-W# ztHPtX1L?^p8PXOxkoh1n>pn+l!Wwmu5^T~sg(#zT(yHA-I(LjYkZmH{ns%JES(&tY z^D19r+021tLKZ%0wc&YlSzdhy^6SV39mrvz9WDJ37s{ly04}a7d>FU6@4t4jxy$RA z&9&lH)jE)6Etp1bW4d52|0;L+LK~$9WLK+t-*njAF+o_@<`!d)6pn{Qy?@63pg8l@|Pr{&4a=ANVnwyYw2f zxplZwZ0<)w;qeHd6r20ohY!iRQSYSq274kJXh%;3;zEgf|A7yy3XkPIF&Y9nx$-Pj ziy>Gps$$Ym)awN~fS=Cr82!`uM5OeDO+!8L`gNrzI-SB&1oRPtzHW!yrsCwvi&2CR z;rkTQT6LZP74Cl`o?z-cO$nyXi_L{WtT^hT&Z!UsLwN04rp_c>De7E8C{0-eP>L(x zz?jq@!agI&m9K-6TwVFqI46Cc!i9?~@5w7T>&x`C65gyTJicL9Ua1EoCs)1+3n}i( zTSBCIuKaOEE?hZ9iQJXXKut>PK3KzAm&Pma$SNPn9mwzS?zMAnSvW|{x^hG;Or?t` z!5qj7*cq*LAS@U~RX9}bD+r5z64}A;bxnnkk*>*1E4bN0uU529s5&)nQdQ1 zj31y>Cok}Jb7r;|Uu99o&a{%(_m9W|$pxqy)2r9!d*N zeCc8b>%5sA{PZ%jgXeIi*ufD(Y091gN|_CQ#Xe|5b`T%a;IMiGXonfJ$AwD-Qo#9l z1%H^qX}F=P@bTP%Y~nK(X^SEdyP6zG3?d@ds9}^~4rDBoM_D%4Mj$DlqhjoTh-~Y* zFIbxu2l5{HA-f&RW)9?+Rf+>y&h!4krY2fi??+ha!y26TMgZ+-X)jzT4#bl+Ya+L~ zi4enS-YY<*5aU^1Rc!>~$3>XQ@NggoKH&&$l>X&KHuv5o#pXJl#nJ?PVg-F&)AJx@ zk^?D05$-@9P)KVH=Lb}R-?$xCRlLL7IVqo5T^Cf0DlW?UN z&I^Rnl*Iz2IFNT3llt>so1x@D-iEh!bs%@5o%DGY7cLHD0I$G`5sr4Rg@>yOPifeJ zJoh*lIXRHc|HxwAYY&m?IgkuSE*uEt7Y<}Dujvt1(-hvBl?PoM$hwuR6ZRnnahVMw zdC^S_kIvkPNyN#4_#?Yo_0u0pXR6GCux>Bv_#8+^z{1HIOqXbUlBf^K2$JC54&)>( z1@kIu6Y-ByS*;zMfP9F5*2>%tPE&%%KZqEZ9jrLuVh2+p2*p1yGCN4Zm0|}=2!;3u zD8+$nU`*=UflpL}!|Gb3lNo%A3niR<2i~kId@An=4+!KmtnNp(P)C@kib+G^B%Rm* zd{?C%9r=VP;Y0KCOUSNPjsIQgiB9FW7@x~WZz{uTuUiAd zO2f#-u!46J!>T*4=`6faRd^Qf%mGy{!zvCkL6}@{bs1K_;SLAzV;CO8Y9yc4z?yaD zA!JvpDr%I@R0Rvdy1n>oZ8%np_dTB~lqiybtBAh3hss2$yO2UC|~2O)&glwAZ$8CLN^+`6l@ zE#VCgtJOd|%-|_pD8p(jd}3Aj6TBxj?QJW~@^4v&*1Y(=gO3v04jj zpH^5u7rl2wdCH`w8y;=xh{`luhTypzPtyY>v(yrM6R#$APmPN4tv#4yFRK8ryvOs` zaTNiHkgYP$E%Xi^P4*0erD?Xbc?kZCk%nH>ELcMAPosCtcY|0M&YnYJDwncH zt;^f^fkm~d3PA&O$Tb`z(m=~*}nz}>o zHruZ-4M*bvP0y0y$J{U)eqTzXA$f1fEjQB$2c>E$qYU?{`K1;&N5LI+;M!!>=eUY- ztl4CdSyyDBSGf{iay-q6cdyg4htcKxD)Z^U1Uz5K+CK3IYCCmNF_^?uwjP3}x$|e1 z@uajdxde|wYb-5m8>=Z@19eh^dr^aDQG-ViX-gbzg6HD>h)>$r>=8qHuy7Dmi}Uo_ zx!3fe7I#(hYI?(=xsmn~iP;0hObcelkHm9wtFiKSJRnC!FA%%m9qfLlO7YlYZB<7d zdDTt=&0FFs(Ay5GwT{Q(yfj;ewj9*N*fxfq()?$T+Su(=vYH5XFhGp~BF?r_Mrpy7DrXuRy$BHFqCmVFTD_WNZ6lC zIFw5`nn|cBn+P96teaY=ikS&3O8$g{EnYBeYMss*?%)guIPepA-J5LP9HjyVgON=ld0B6{4xv13yivw!Z_VRjTdEs~yOd%(UxaOczSNdIvL5h3XC_ zX#~9<*6VwCn|}bFxA|unBPdQQ6cQKV1D?B|=k8E)e`4iLFWENnjP**!t2|?oZ8USwft6MVy*(kY%KjZDiTT%}kb>LCET-WKH1pt*Lns z*asABJC1#}#?R81d92NsgvW9^ScLg+OgPR*MzzC8JAkMQt~djSk9tK=my=!+vA8Ok zqF#cebvcH6sA>WNC(Ytn*vu}`4MkeQ@u#3I(elguz3}*+HLAko36}u5o8x@oC*mo3QF&w9jM9Aaq%SD+KIYlMVVZ?U5ujHj z24lS6z<94xEkrGDmIU}~>lghH=7eAXBFNbIG=)&5O`!s~?`&%Jz&1}n?zuQAt4%6z zKp2FApH*Mm<7sSS{^_4Z32L+lYA8X-MhA=JGBqTAL$a&pfF-;=N;Ethw?09~MnY77 z_vq5|#ulP<8KYvF2`(I*(-kn?Uig(S^0qC)5Rduhr#0t>RWAVZIx zLF4IoIlQ-(A-or6MB$uVuZ-x>JDSCBHD???BMzF|!hvrd-Sea@IrT{%J%%`-j01-kl@x(n{#yCS?fjOfH7hqzClfViVEPFXqI zT_0>*V6Y(Wn-N0Qe>jz@9k1%j#Au;v&*0;#mSwV(q3Nl53HgSA%Q2eZQ!$~P20?44 zzNqjDRuYggiRvv+@UvB*25QALV#kQt;D-g2#Pr@L{O94ZE7#5DHp~xs>AzJMkye3{oyVx-lyRFSI9xiFNjCM2s)O1mj zKTcxx*@snBNvikVs72Y~QRUM^G+T~gX8*r`J(*FYP zb%&SY^oAQO-{-;tR(%W27Iut<`9jl*Wn_H2FT%wf!=c%C!cQU$9n@AbMd2h@_i)XY zYjpZu<)Be9p@%i49}pXjr3K|_wtPr2tNGVDJo;VbJnoZ>U!cXFTqJj!31zQ&xNFL2 zBE2@`C`R=(jLE7YYEMEl-egwEQ@B~}T_Q89{uD5}{7*iXZOONA_`xDJoIdA1HK~TG8ga3n)-I9A|L) z97Zx~(G%$K!jO`wLvB_i%4Nsq2I0`60LW80=mZxh-pzcjsru%kc(+{_Axpfw`P>cl z=ZnU=n{|JKDb6~$!R)=wJYrowv0c=nspx2cvu^%r}IHKzgzMDviVv6<5u9-cX2-Nz{B(t}}_+wqUH_1l{J=4?o5nGoBn>bgy!i z9+bA>%2hI54Prd{KT16QaI;Xetiv#NZQXdrgU%T}DZ`t}6YsIa`yaHAEo@JrLvWmB zbN<}<6aU%VDN!--Y3c6}l=)X$XnwYL<#Lepyt6ZCN0rJ|4K+L57^Ac}PhJyG}AjU9u zJK*x`Xr~Ul7l~aUBVJmcxQ;5P5%KNYqHcqz>LL)>eHEn})7-;U*1|};{|l)nk*)w~ z19o}#c3d_ zRgv`tYU0|F4^S=dDy1J3rC(vCRsSO4PoTCHg0uk*os6oZq2Y|>hlnleXsC`rmBh4@ zBG7Yx@a8mUrH%DV*D<7#RQk+KYWpxj+?am-iF7ka8<4(TUFjEtj_KD^2sE43@$+%s zoW|7j{}+KCrm_}t z)3ht->O8yE73c-V(vEnePM6hDI=zJ5_5>q7CWsqT$a_TkXv6id8&XFhZ5hjX|5`u2 zgxz-WI&1&G)c-J%T0q)R`|H;KLc?^oBkIVRPjoajefloAr{bz)_)$Mw9wp}ZH}jaG zra+`@Bd!tWA9F`Spsl&UE|8jGk>JBECT?ieqi8;F=`pXp{*$j~B0Tj+$e!3Km&@7n= zhleeKcFMLO-uHv%Xer){F8$r~uvzyG5t=%otm(kDy$Dy2K$9g;9+foZ>%hu(5SP{t zkFk~BcaUeh86sna6f;oO9YyC>Q5Q8IzjAjvr-A`FHSU>qXIO zn=c8j+48$%MPdH=n)wS)hf0Y*?XOlOoT62eX3KbV17vy>%_u2`OpE$cgDTo=A}I#8 zA>lPkDAzU)f6xeHlWWmOJ@HzG5l7u^v*Gku`74mh{6#71u~iTq>-Uq?yfX+v=y1p9 zcGm=P2<`(Q0~s}2|0VH2-5XWW^3xr#^dL_0MpGz%naIBki75Xfpv|2s9&!|`*iWv~ z_)xpq=)`feE)uygzBf_pHC3-a$wtfC;UcCYnpSH@&ytvSCDcQ$kVk9u61{qfv$@$k zNPg8-Y~P@$geKJNW#ht&S~C!Ts9w`z+cOwnEaOkGFFmbU6o@>$Cd3bi&TC2!Ao|z} zrNG?hkVwXkIQMBSn3f;FUM>CKg{a&8>$BI7bQ|JTKE%uRJWB8*AaSa75h&4DzTXqb z@;)vfuU#o3@U8Aw_o<1{F^r$wE5P^oIwU|{Hj zWM9x=$A(I6I!)wRe&TSznEAhXVck*X=@0C$t|ytZ6TClA2~E4 zc63a+Uq*Gf7Z&`**brikwqETD?(_E%uf23wXo=476sk8q#Lv-+U{u>kob51wX(#=` zL9`eNS9+r)9VYs(lm|gsa~yBT!Lf7gEH7d)w~g+7(YqLSYnJT^Icjvj!YVJXGT&&b zS!hOP`7WFzcce8A(s>Q^T-Jz(M2(i$9XKs;H5V;!I}jZS@vY?p2cj7v4p_GJQ`p=J z0^$=(pZ*HMMu?4;G6%&eLOf@o=WKY*)r2VJosRQ~akFYJc9KH(6t%>%Y{?;k)>O9w~6Tb<}us>@9RuZm79=3>Jo(yd%ofdpbhywD!Kb3l8q|aNWKjqdid~Y)*bNHZGsoM)M(pxnv`=IC9BoYE@&w1k zRc;`kfV)vRt{>Y>cxfPiH--fpbNx>skg+`EkTo84;1KeW1!yFM8i!JIQ0hX{t5d{5$d5fu&%G zxpFnp;8XK$M8#%*(e66!Xv*6$mYNY!QOc?6HAGWd13tVl(H+ooSAJ;DTvEL???L3j zJz~f21iJi*U#ZJAm3vT_N5MXs(`6}6WATp|QOQL@*`dyzjh?QV>C)5bs1U0GeIE5R z4!M2U&Q#B86rCM`JYyU75>uk^0fp%B8mC4@lviVO**cYk)NJ`iV@Vo=P{Fy!Z??xI zarmxFNBlxKH*mDl=0J&V#V<0Vfk&9Hh6SI11ur8b#GZD7X3P6xN0_!dv136~h2;mR zA_b*F_s;o>_w{p_J^9=jgI7V^g?e_b$;0SYqb@{xJ+ZkRPdv>xF-W3(zAL7U|07UK zWq})BKw>F!n8PrXU<~kn77OF?@%^w`)jA^1ax2%qgoIgl7#y%}SVlEvz~j?)>|)Yu zIbK+_OH*2cj1pZYQJK63YJbnitqPU(rInz-=$VBEj6_~3C>MYdPVF#FyGpAZEAqQF;-`(VN)F-3Y=eRSS?{hqwQWxU%eWIEr$}S`%x18k(vZ zfsNox$i|+v>c~;-S=*+uZq%OUNbRQ#NmDpB-`#4~;Y+MmhxOD5bhh(d&k*YrxE{Q#rX7*RmRH%9V(3_wL8I2~z}dFplHMn1bx8R$(0CP5 zpyh3c+K&+Bk5C0(e2V)V!LT;G`t+nRKDHtRKdxy?T00*Vn(S}-(X!o9>Lp?nmO|PMg^AFx$oSQ1SzMaPd?AZ;%$*iMw+f8h}AA)fU&$tO!Qt{3x zynregcKho&+(-zuY8KNPC%W8*7b@JrkUf(lOY!hS#j%x}n9~!Tq1i%H(#mb{Qk9+u zA}SVhk7$Ey{|oOtgYGV&Z}BS=74;v442|?RwshS2xaBEHz?g6_?d*2egwBu%x2XNh zy0Ijcv1yg+<6TIIPC{?6365y!uI+FLH5`7V*zuZ!kZ-8ZRJ*^zqBBPAhTq8GO`Gfo zTk|&1%@j@93N#D95kN_%>&I~kU6&KuHVS`m9uQ&$$<$q`Gwn!4>*q>Rao_3|)}YbU zH(2zg6a5)n(EGpedfJN^tZ67{X`)k1@B21v+yqPb#8qfdWXTe}zc&v*9&yaOWVD!k zKR}+bTlvYD^4)QGvoy#wrN@v%$Cfk4Jk!r~j>b)W@4OFDEVcpck#NsXGWXoUA;CmQ zK<~c8I(1jX)|Nf-#wJblu8PM3>&!>E4H9T+_mCoZHx#q}g)I||dM15|?(i8Iy-=EW z2PO--@Efadpytn?fVN%zxV6bOF=mV1%I7ePT7j~m)pNeI^+IX9(K*;KhxPL7)dZRbC6zu8gJ?5&`MNmXeAAqc#pJajCrdUIHPT^gMpKJ`Hv;q znRV|MQq#)}|B!8b$}j$a9A@2X{9*!fN_0Lu8QB0C*iIG^qlrFJ#~ds(90Iokxvdz}4f>-Lp@?OmBkNAf z+P2WXU1y6Q*lmSoBkeB2lWC*+PrgYjNlfxCBngCJIEAaEJBzYF<36lcaXdQ z65DkI5>DgnHl}(fr5c?CiL21%>Pe|~U(j@> z5GVz~GX<}mF}t)LM=?&7$6AAXNCiw?4jqW71+792q0D_ONQ=R2uM@?B&(*V?jl`LM( zt~w4?(Fe)hnCa;ghvy`4dnT@2wdx?8Al#%UM#@^iy|C;7p<#zsdwRw4^!w6W(-s$v7aq)NZOl*xDMw;?pdwJ6GpMfAd59 zMt=**xF^E=xqI}Y1pHt@wF(tg@nhhZQc`j=>oQ1MQ!A1TW2qTM!+@`J2-S7P1<`N!YMQfrXohqFgm(%ND?xq%YI&&{`z&NL%bMqHGu^6(cW zJfPZeI20r$B-1e&BYEcpu<0y$3rWA@Fb@MtTa)4-ak=U*kXo7$B9bGlglI;HJ{)m| z5b%T8UFV3CgkU`UI3m}KT-qa8fHi(5n>NV z(2ELqk9@!p89=}a7rsxnT1e-8m9nIYlJi;8o04-`(%r3E6@pqx@M={bq^NhRRl!J+ zsMV?mks=w*y1s}-JlHSZVNBg|VZPByvtSGI%2n-fiT4tgy@M+-|Moc5uBLkKzDLRF zZWyRPL;Vq3$?CRAX{lnHm1^dTr`2=mO|d@O?}>^Ga$7H$B8xnBl2jI&RoSZ;K{awO z;{}3kONojIc9O&v8iv+H@G|Q*Op|HGGy`MSEussf%w9wt*DtqQ5M;otnRsG{yI>A3?=d9~=HGqsfWwVvD!!!0X86w`0ryMlZDkd$4rd zgU(V7|3s!<9MHgC`+=D2N7$Vp^No3$1uvr-yh~W~%xE<>0xI$AvdYN2BPxyi{9>#3 zLzkEgO_HSqbA|O2QU#@$sCZed^6t%y>XLatqk8jxuh`H(OkXfE=eiYARg7`ptHU4|)_pX0JxHC@nGtI|Zu8jps=Xm*alucD-DQ3-DNy`!g!)PUD{ zE<>SMiepPcw3^Z#PzrSV3v`ONn8j8m;b(IOP{dR|>As!zkJw~sy#w*eRf$t*s{6?{ z8U$w5_lUFI%&K1q5Oxs5o>VTixU5n=OPAHEHYiCSoHs!Tq^N{9Bgs)p+=htNs*Qrc z7EFDE_xWtcT!J@HLY3AGHM`x{vRW1B#AYwbVR|>=m#o)}QPxq-@Pc~H&TDA2k9i<_5$cqW4De>8>v_=c6D%A=qRHb@aDchD|=O~w6tTLaTsBC)=;zp{m zc=Z6wi6mr&t`*6#0lP-n>u8H&+q*c(LWry{$Vlv+&{Cad#z0%R@lmc?joF@PULu+b zpCh>3PHPcf+Z1B+8)&UtzPwKSOpJhFi&V`!^byTZbHZa8;5x#8SEwO}PI#fvmjh%DM)tXBOE zE+iM#d6+{e9DMgsDf51J{N6o%B0_`@acy0TmE6uX_v4mrOR(Y9JP%&hgmW~_6G;UY zq-Iq(u?5eXxpf-h#Tqdh94U7SV*gqJYDQr~&YUXKP%OYGB8tIPs`bDyUVSt>kL~P+ ziqY2z$mjKMMEyWK3WW72?vqj}ax66-_=C|LS2@*-&DAGKr4>*3@fq^~u4s#_a)@P6 zXwe2No^UtXuMLzl1{*fEEsWU5whgw>9qr<7?M1SMHfRDW{0dptDX0)V7ypJVEp8bu z+1Lg^wd#*CvLraXP8=R`aM(p0zJ|!Q4|xp>DZh^+{}SbYMEShDE|aRc36Wr#$*#Nt zwV++dn(q@%S?wHb`cg0F@T>sJ>gLEAPo+ljEN{wc@5qXyQUj31hwv_}RZ;6NTR~Ji z9!jWu3lN!gQ&VLqu}p`S*e3GkY$f6V2gj{MeBOicd4;mNII_-C)^b)^L1U5cwcJD=m*TO&?tNM*A6I^n zy?NdqVQ>9CJ=ho%T4TbVfXmI;r5QaH`YU@SxFqZtP%sY(+$8cilH}ehoIyKAAbld* zaQK(F4i(owi|g+NJR#txk8t|e1pH0FQ~`eyP!{m+08amdfc_!;I!3@q0W|^+7SK(= zTY}FO0e!=G`DOyT58~H%LOHxOki$R4wN=1#0&W)c3S1?wR|~jNz;^^ZB%ngCKm|W( z1+OnaK-+SD{f2;31w0_~cMDk4$n~sMy!8v*{CbFh-U3c} zmE-3LxJ*EcfNNIs{NObl<_Y+|fSzkPe!PIo1nlq{$FCM}={kPxv!25jHgGt9BZt#o z=kU`vIQ&h(>^J%KmA5#2aubJ{?{GNkT@Fvb$D#fM4o7~-;p&e#{Btvh^2Z#$B4GDV z_;t}%4*wSL$8G#N>r)O#f5zc!J2>pTlfySH94_C*VW&MD=I-V2qJYQu@oWDo4%Z6U z;{d;IbC5&*=N$edV9uBP`m;kEhJMB2-oqTWI?CZv0lkm$Yn_0}0`5M+@oxw?{3O5L zEnvtu{Q5ls2cP2CTYlv5?K)7wC!FQ^j|-S1;4A@`3%E(Z?E?NJp!YdmzJq{~0u~53 zU%+JoDst=)*S`qZ@+Z#cQ2`SKOcn4M0Y4S+O98J7sPOIjbGSsG;Q|&3_?m#93wT;U zuk)P#egUHd%n@*%c&Bd+Ir@$yvyKCR~0D+N^ej1uxG*B^@Ob#?Gc{(psP(Y}WS zTq3XmnvDA5l9W2!O|MTk$c3qSnR>al%+#5(!Zs~GFFmCwwYHphL26!@tj|d;Fo3%;8#l57diKqf z4SFIqcsuwLSz)RX*`Yl{kZ(lV@GvI>6=Rb+BU3h_c0;x?J3miO2iuuo*FRG>fspay z)fE=z7lz5k{Cqh#H4oAi=BMcm2E9SnYUMOjVWB=xX&4BK1vgN z2Iv%;9=WN;v@A~BARTAxOeSTe8nR?`O-4?3n$Zv@dLytH!re(=}di4(B7Nyok$Z~dO z9`q)sqU#HdfkDtqeoiWxPOaUkwNqtkuOT~KUnplA<9AH8jwKiJ@73)o6ZO9_OWH4fQ!3?NRXe<(4tSskbPt(iV>|lAS z3A!%8FfY!A+93xtk&$XJ>OrZrXSj^PIs=xYm-Wz>oL@*io}VG-fj#WZl!yLx;%MQM|@yv%X1Cis=-TDFyLZMh)?_SfGCe+$I86yEA z8;qn1)N9H^H`Dm!7Q`!7Ye#_x6hy9)+nWqa*B9&4Ow8$_AS%qxga4)yYVCAt*K|`h z3|*gFV4NwZWx+#|A=bAFqAw)+)O4mJ&Q@5O4BrUrPfbskwKIaXdBNI*_+V{ju$G>8 zrgF?4$wlR*!i_h^1r-yGP&~@T*QbovqBF%XBO|B&jBJ!6sMh)8%}Vu>idt z=pw4K-NGCb8mN*xVJ&1az)9g(O&lTE!LVqOkmH5ekSDWId3wmXhBP_Tl&#ExOh1XR zThfgYRTN-i3PZo;%%m|`2=4(O58;`^$S{yq7x9|ZM=R7IRR1pupupe{3Mq zP;O)dlCkqFRF{^OpAS-PK}umh`K9<^N*Cx0X~GYN(aXr;!+;5()+V|78$M5w`H+=p zSsQZm(`)(4XgPNmVU*3OU#IhD0q%cLjsWCNhi2vY_h zm!l}2`7-9WX*l+IJRTmDO<)+@YHhI$PtGQ)4-X}l&9+9*mH97i(nR0XR^K^m!eK}Gy%HHH044huwc#U zjxneVzwW^@nn|97W+#Wr9DMks6p)TK=dmCJF;1$Slb>I}avXGOLD(0AKG0Yw2lP!3 zf_JOMLKpOrih&6V7ot`4+NIZB*pQxVVUf#AvyjoSC1W9?U`n%q_VEG`GX6kbh*o#py>xU=e_> z=!U^+L@e>Jfre{g-4aY>;vW+UQWhT(PqdD)tc^=>$>bOko0OOokwkJ}5rxpSFf|QE z>q;o(U~w_T%brDJotX1(MT@Cpd-jw$VPKa)`p?E~a<9ocU9X^^IddGC-oW$=qL1J! zV&X3Uxtu5{%fpi7WXC`iqZc7B=H}p>)T#O$UDp6ZSH}Q$teN0{XgwyDP5N|%+O%Rq z*RW5aK7)GElt+tBtSYi+!IYVqv0wwyWnMZopolNkuI*9_;qK8p%taCz3^UiUz9YH} zeG%%qCzY5k?O0l7XDU88S7ec~ z>fh+5XP9zwK>2TUSZC|AXVh8%_wWJfVR9tNN=sx4{4rhw#f-;&nA{~0|Jk?B*dR1V zIS-D;cKE&{@GEV|RuWGw`yq-nCnhm{k?o2M^k zVY#xuGbTQIe01cPq=+GL(PWG~uIA<7mSs7Y<{4T9QsA44aRc4uW}|L2JuQXY>NIW_ zGzl44K~_$tI5;~e2Qz;Tg7$R1R*x+Q>~~Puo0fuj6$?+Yr`mGdRA660yixM(fb`&i z^e5%y0K;VHG(wkZ#CAy9Ksid6o$2({Glu^vg6AEL>3hW;VN*!YeLts4TwND=G;u$##j&zNo45ai1*(Yl1_ z(IdtrMMrr{%GeO)x(67#)5a6uVS=cNczm@cc*3jSi)UTAorVi{;A9v=V5L83>BJWM zm=j7VBt-ezC3-!eLd0$0o6_LL{+d9b{;tLu%=j{G$BAX)K5|q-N-` zoq+L5F$(tSSf7e=LY{)2`8^>K+zp#%$X2MyP$HQY(;~G}u|tk=nhl9H(>O*hqjQ#r zB25UKN4tR9sL|08kuhYrOhC+wCfb+doEBgXs_Ti} z<0clH(P{OL8mNH=eGcndlvV~Pc_3~kYOM@I=1~A`oXCXO*k#Qpvk;hxc zMCc>M4rR0sF45Sb7y^-ETnYO+m+HqV9vUlzMIvQfL~K$D7tDcY)v+As!u`3llo=a8 zj9)l7^l_#fz%%0_5|dI$J}0>!;aN$sBckh75aLW2>U_~#=}6XgZD4P7T3$g)kc19M zkbAS)kR|)nCi}7^vo8^91S?ys!E)_1&I5Gv;kXAx4vu1UJ_>2~#}TC{yRuSlb}>9J z-3#aUwAs{xyMGjy3J(+{F$Pj{K)N;{eKJ-!R3rfRk>FM&H48-t!G}_UW-(ZIL6(e& z6lzZ=yI0qNSSw&}hdX0z=_Cg ziq$QN#?(%AVYE?&Ne0uWXcw)s^f?(?+JKhyIR<^htXS7d@G=PS^RVTZ4L#6A(w&NQ zmzj1A63iqb&ULcX_QB*5rtJgI*E@{;M?{g6PDpZDtl!w2DAPth#nmj(q22V_&cpJ_ zq&Khtj3s#l#*)%>wzEXB8N2Q#aSBXZv~t5Q5oj9mb}7q>IANx1X$whd_;h7vRw8NT zT5J#@>MBZ|NoHU)72I(#q3QC@`0%Gx?k}udMK~*Toj>$j8=@-nA?hVi;_PW7MT%uK*+g>0Km*Djy5hxZ$U1V@C_kEP}B0T+Losy z0wSr&=q0|(!#A+SeF(OfS759SPZ6PrxtMBa3P5+WTf(d!-t}Da6jL5;gr=uRBNH%7 zj806Fm|vA5hKwAY#0{M3h{7VNS?6;_MS!^j|#t2hC;<&_U3R4eo zT*AYKsr%Pn68kW9KL>)<8m8{+KtPl*bsxtii5I5sEvcEQ($t7wq`+Fk)YuY)XkluR zMH6NtSu}Gtl7&)3>SxiPF=-iuB~)AP)^5B-q%& zLPhLuvKujj=!4mKbdo%Bs2n*VGA?>BeQ5Qj?37V!)uZuKBrIYvH-Li>0C*QNwwsfY zZ_1+r#uR2O>_<_l*hnC^%eS*w+l12k(C>~6K}zFr4nbmMm^^nFGc%qZ&C=v=$;FUw z3X`1GBUng^TGE5m$xsQLEwvciXU-W6;hj|5xFpP`V4Rq5DooRB6Pae?=uQLe85HQC zN%q@}fwEqQ0X0xg)$vGqpp>7HA!RGKt1;(^+u%s?o8y##7sLgn_-#gs?chj`yWG++ z@e>&4ENQ)ENG)>gMg?GN))9UOYBPdpB-8Ek91y|>vF#tR5u(L;lcS@f#zaOtwu{(? zDeVE|z$ZztO(~3~?J$Wp8>BDL@ZcX#bpz_F+A+FLilvmbzgfad|}p;tRj zyDb2`|Hr%bMSw2@t_N&>=C1t!U^w7ez$Cm1DY&U5^|qlMfGL1EfR%tHfUg6-2pD?t zu6;A$SimEIMKyQrzX5Irq?18U0CoiI{@Y!92;d~ZIKUSHivbV+j`jm?`|Ga#IN-!9 zckQxTl2-kV`T$i|At&JDfbRot1KbBV_8RmKxaKDGj{UYZx1e{xmUkd8;B$cZNttvS za1r3LyWkIK1GEBugU3cfn&GzucxZeI;2k{O@;+cD9vu1`FcA+TMKwo#fRg~X<8jjh zzy)|l;2_&nfo!1aK?0k*^$R{b=RL~nZxZVNdh?DizU zH%Hp-YXG+bZU)RA1v%PbFAvYdhXdXOoCH{b=eA!2yal)!u+=!b{Vd=gINn0OUy^!E zz`>t@krVCqEWqSsyL|=VX~5%vO(xmxmjK@aY}X$BpJKO<2b{GWbbybpu-kV520aJ9 zfHBX5ZwEYgv=a3L4&7w8zX4bccm%M+J7^c+OhB)WIOGTCVfzD~eh>Np4E(@u&jIxN z5XamC7JUpk0MBhf`#MR|hMjma5AZDu6%kr!@zX+pN)& zTd|*8hvrSambx|dBRp72rw-k<_YgD$8m5;df8-JU_%ARP-I4J18|vF`xTaZ=SBdm! z`+*Pj_3sL-{SYgf4uhU3Nq#=w8~?I=Ih(dlNX~O&@|s@ZA6$%%6P-cOKtWz`=Cchj2IWT@Ds`db%Yq^d)Cc;6*%*}704@wuYK2%m+ei=VsQOF^1R`HHKfELzJ5#G zhxoR8#$$-DTcpW-^ z*S?bKacRTj&P`x#2t<8hC+^xi6D>Z}mO;Qp1DDS*lGF>3Y-J5_9fW*~NiPdLB79}D z=P=(jp6;J``^rF}IwlF}xD>Pt;p;J!U`)P#W1tDr(aXS>18)}iT&4x|39h#y?-KF~ zC=blc?oqzs?o+)Ly%XQ>K{E(*Mn4A)Y!d0efgcY%9g6d>I!y2w<=%)E$qvFXFUsHF zwf{i#RILt&`M&R!;jBc`R}N^8p1W)Bi8Or(R{~s(6OQDjclN4&68ebYHb?r{1bkEA zmmw{U^gCD25mdgK0S=xn1x+w*voz^{#!b;C;_=li)Gmt&u(_`{{?i?t@q$;=k~k;t}Z9&>#dK(kI0= z-4Q=Lfi#!bJ&W||k4uVmOvsxc@|=83g5qLG@B2Wv5p>B!hY#US0rxv_uP_W^9l+m! zn}L{QIO%4B(C=azn+r(4W>u7LFOMiUU$4DYUw-ujbgf$8x!B_wcaMqCMj*&AZWRwQ ziBqw#sOWCNChS>qGo%eF5f#Y^A$cy++Wj1s$DtB0c8oS4nnWrytyZ_6>>l z4WH=S%Y9)z<-21RqIyw09N&H57mZl)iF@$#Xj#7x=LjyO3yNc>T}NDtv^4x*b#d@s zx}ZKC4}MK=+_h&AKk_-LzFuS(1;CF1-VM43KAgrtDR4s&vwn#*;oN6(Cq#VKAn!8r zXg$LCOy_*I0-u2Rww1sWpD%$M3EXppV{<|dV-$!>EAkE?kJ*w--?%3^`)L|?tr2r4 zB4(Z~_&ANbLZu_AzCobd2s#!|p^YiRcT#=hk@qq3J|`Y^{GR)sTE|DUrBokcb2{qD z)o$D|f!D?oL`&;~Aa}dH80k8+3C^@3$o?L*CeXe}d?7u{rHXQ`nPeO;PJJ4L&k@q zWG_d+>pdJA(+z2|m&f5u2~X>x?Z9Js!SFO`MNt~-p!b2#qx8Sk9qvA+p{oDJ_=^Fb zli;(SI?2Vprc?0MYlv^i5Z~}(r*uIh>BeZB@$;O@I^+L)I-1F2^pz+7FR^kIPj)I^ z^dHiVwb~i~U-*`f~o4x*DTt41aIg{(C<*#^?WZz5j*(f1zni{(JY)z5T%dyY)Kz zgd*43(Ag}VC)QjgB%@d{90BN4L3X~*a+&wtS15E8Pi2AbI_Sny0CMj*1KT7X?wcA} z%}@-z8NA#=aA-5q6yp&81Hk?Bh}}-FB>orvQNAT^BN|~Z(K@{~0;beZyIn2fv4+>- z9z`N@bY6n9HEj~gKQz#8UkF|z-YcUuEybh-$a@ZX%kCAE&UbTNZlWB;+nZ3fW{{ol zH?jC0p*!})DC9bTyumo6>3+f2d7r_fg_|SbruO{}+8%@L_S1s4k@kJmSo`|5!AX*j z+8ui)qn+aZ1ms;nUOVFLY7ZYe$LA#T9MFCp{_nIT^BbVGU?02$Y3kpGWp)gNYI~?81_NhOrc9utyOM+yFH#{Cp4(vXez6VFm6>FQCrlMLXXkaj|iaNf_sjMK;yj8uxy_#l0NbSE2sBXT1d;{To~RQv0TW*Qm92es6^C z4&3BQq`W!E3wsS~PfuKsUa~!zUV7p3MdU5sXtxi8zDb6L$2;~ykxic{e7{7QH*haW zPl#H%qaF7KV(8vL4BZ{1Nb>VgCQir=&$VYifdkWUBO0Alp~R z^+17W&T?U=zTqr|+nnrk+&6+jbOrldnw-iYZvU|lOq+e!y$+;qi2RNMujG?S(C4gs zIR4`Pk+{twd-7{+<+6|L#jj~QjXp6VAKM-5Lx*b8hs=mRWOwwzbl~!#A;vyaxV%c= zPZ1fIGTDcQ1byIA*vIM}&Y*%{B(9ZqOkufn51N0J`f)HKyKNLA=MV5bF z9WF}#Uj~nJJ=CprhUo7F0zNO`Mgg}7SS8>|0e=0iPFeqkvlktP=2~fWHcOO~598qJ9A%6mWomLj@cwV1|G*1Y98C^8#)Zu&%!D zbzM^0liflg8alDn`9tXR_RkB;6ecx3+NyO2l}Uc=tV5_nUbE$Q3CFo zDy}(})lEryPXK+~*k9cLQp$;I{De_S)rD^ONa8LjqBOp2{691y5q0%tS<1v_23UP{2fQTR6! z_ohZlW2Eu;H&IHKCP|a=Z>*Gp?-VIbN|*FfCjMpNU#j#3zSE>!{L8~XJfVc|bi9cI z53t}jOEb{6Vti*xv+-{Z{>_r+;yX{8kAF|$Ux`$TZ<(|}S|pXbwAb}Q(T{?4)*ty^ zC7=8*_kD|{O6eJCiL{g#QF>7^9EFj9N_hpnOxP`vlkZmY$!|AjL>?0T^Ta=Qyl=xD zwUUp;FF*L_;RpsxUQOljB!}T89Ip9>Lpr^iKJd5fBYn*A*C#FB$8X`o zdo)Fp+PuDP@8#mA$NK!3-0R6bJ#K&0VMFzc-S4DizC3^FlSO}Bez)nv%e>zGME`a2 z?0uttU;D?zRlScN{LH>2H#D==o!7ePQ@uK`EPZ@`a_quY9=(E=Z`krxns)Tv_nKXs zXX(7^#+bIdjFt)e&kp-1dw}KZu?wS1ueYArcAtOH2iLtT2Xy`MXSa@nV+R+#H^F~K za*Lp&3*K9osMhVt-7<2=N6(M?;e-44-d=DjV9k}+)1KMj^t-M?tmt=mN}7$?_BD{5~4h?x`!CXQ`Tf|Kl^glYdw`;Yvzc|3jy< zM%okn#udJQ`t*Rb7}EpqnOC-bIP$`UBfFDp{_e7S&jX7>KfcneFw+g z-&Q>;cV+A9K69;;KfSZrn3FUrPo}YU6C``^uzq*+gBeyetG1sh!-l?`}FD(@x9xyLoL@n_F*^o3!kli zV|M2Uvd+9)b)nmduRC{py~EhsL&C3)${f}HM6%bR6GMkwnB1&wg{^F*|MizgBzNof ztS$7)u9Q)iZbW>LAN2I7)k~*7cTyGn#Xpa$|1!3Db8pooO^?rC>$ZEas%rk(`)ghZ z?Vvk!W&ivAlTZEf*NzW5F6q9c`QF&4MpbS}UH!_lXW!Wy^lDMricP2Aj6D~u_Kyp= z-7i@#Z~yjzvVh^!9{bj#+qMO3mu$#=D)ya6!j2tm*DPz^j{NmEgM(olhp$)kDBbK+ zY(78DbU0)FBcBZ3(Dw5PO^2HkzRkS7Ow)Ig_vuI7hQ8OY$-ur>{g=M(w&wZe-+b2Q zgU-FfDh57Vd}i|SS9-5%*Vp{it8dzZzPR3f_{o;`g4ch4!M)Gx8(I(Ak>BRX^Us}b z1i@O{(nEBAb} z$(^z%J$j72vO9TY#f7MI*{h8YjJuS(F7v)W4u5iA#NwalrLVaDO8Kwz%e&;xT-xNX zzU|A7n*Z_tTU9XBf5Ll<-)Z&TFYRx(oDuuy(QAGx``;Ivd8CAQ@*J2Qy-_cJH2t^L znhrbmu4}vO^5k;?niqO3KCV6d^jE85f||JbCbyrk>qs9<`T%X;kd%EL#>_jh|JiSM ztp4tW)o<c6K>Rh@IH>fYN`b^OcL)IM|CagRSSX3pLrxvML;zr1!qaOabgmS+qoxj$#vNj0mI z->dwx^X--sPAV;1z2u1q@d#x>`@Iq|a-KRIw^!Q($) z{mJN}6Cb(iw)sV$tbg@~mumlg{&T-6U$}JKaf2T`@cuJ3AMCmC?q2_~@$t%xzRxW` zwcnP3AKkp@%7L41e)Lf9K!en$OluyJYh9jc?hBp@MO{UOD5^+28pa z-d^|i4ZVMT@xSgKb=%s9o(+vT_s@G;Jjc~-y6AAqdtcu=;NxHaP;%(vVXv(}b!6kr zNhxb*KI|^EQ{PH%oAqMxfgP)@Lk|^Yu3BETDbhCnlC3}A+wb|5oQKN;zgT)`Z^?n{ z#-8gQ-us)n1K)pq;mJ$O?pd%T`Qszw_unyhz~2WQxUFu)n&FwrJGWl<{1Y#a_~Vmv zZj7w|!(DriG##)H-Cyxm=?~u|`gi^A;)chc+kNSI-;67oKKkyAaicHlHSFW?8sEEz z-|h9!z~bLtv~p|0qCqRa9`wWwCwOkWui~{Kb4MlDwEb#t!1uck5}uAMy7nJ?-y1w} z=iE15$rw8Eety>I-EZJm#-|JUfZj}M%G!&zh6-)VfS zPsS4$-ZbREmf>R$G>u=rt!nL#Z-!*vJK>76A1Hlxll^@0pVFTBAuwm>st5BABqpDf z{OmVZKlsL}&0D`e(>G(pCr@2>Br)-^x63!|zw)E|Mm|@1)At*j9)55}-w|UfKRbNo zAIn!g^QYy1`_0@9Wv3VCH5UE;Uf=N}AKkrea>7e{SN-WvI-+kBj=he)-?yWC- zJ^G&K3{PS0t}t-N!KE34O|vj?RuxekNcK&pl_AVzPhsS#!=Aoi#4EC^uil023I9e_A*dQT-07-vqbF z`@xuavaT4t|0du`5;IY{u-E{7w@XlW;ikTC-n*sX%Di`*_vYBN6xQiGyV9R8?_uUW zdXK!fo47OmDFCEC{AgtA^RCp3=;@uF9a`#FCvbJHIghwa zMv)WNP!QanM*3b>lC_GWuB4lgGI=sid)$Zmf~U2LIDR(|ca=4jXntHyLF;`mb^n{f z9%}{|x{pve)B2dgKT$Z#I+4ouGljELXjy<;xhRsKLeJ4|7e|Uy5~=739Py?ExH=pu zOL?5gdU2#8WdSix;>g038scWT<^iipnM-87T?-MZPkEEd)z?J@4yRl}+&mnKrkqRp z3~*K9PDhG|B7trq&~BDKJdzuho`L;o~v^<4s^I=n@A~l7uqw>2(~jOeh5Rq_eIBnq<+(dJm<1 z9)UDIksQ+w(CHAJz(=L^r4y0y3F)?hJef*WpEREmSdSo_bZ!Uelr;)vNLsKAVauWw z8cF9-QjhfnUsxK-zq35%H{=fN-((E~WJ?K-g>9 z;FeTNJj<+&6b?{$mh~y6t)p;-^#FzIDLmgIw_Qn%6kcczBfObZRE26>i&*jw+|EyG zr7ByUu&AVH60%WNkdn1g*s?CiIcW*8@K_s&<`N1YXDuLhmr^*>YQZ^a<&~h!vYLth za?(yVvLQhxSwG@DAdiSFVwz;>Fj+_fO@vRHHH_hrIC~-hsODNHM5z)6(e3gnOho!* z#gRyuNF~sW!K8|6zF&`XdZg>#aX(RIECQ0aG6Pm|L8yeuCj<2)UDb(;MgFIfuAwq1 zYa>ywA)~Og+^!`Ok4h!6?L=@O8KUa%O&)!a(q4{8@|d*@C3@8oJ%YQjm61*dos<<&U9~}CT~r|$-R++$~qJL-1ku9w=A1T z?`M^uP9uONS=WFlqc4aO$Hg2YXx7$Y z;{5zDdSSP&LMrzQG#}Nn)`7;o{U(GxRyiemWiP^+)?bN!*S82~S#3n~7Yb)vcTn2D z4#P`-zV!jozfO3uRZTQ+k`%mFKGD2I;T0;KI+Zj!q4-qXB#X-9xd_2?%&jyssx*%B zsfun;+tH_hPJIC`1E?QQvWP0lB8ntyB*M(@CImPq&F-l5t%mT`ctUE(X?)@vyXh{U z$iE>npj#+4XH0mKbqCIDoK$yHxsMGbFQ`pjD(OwFB^jNfy!kKz3`hdb&mIX%c4=J2&@lf;;h4U>QiT+OEVv7f&PbloQ zcpUl%h081+hCZWkh4n2dZ9lb_g;q8x^9u@BSv)p;Nt&x4!o$e{Dsr}K$W9{qie}E{ zyHqNP$Bi)e-RL=PX3^0PIs*vizMV!Mxu0YWVOtmpUVLw|xtFev{|9(ktEm+ne>2R` zx`Kj3+fdPz%tfF}aqpAol>yW|c=1ny^1<{i7qvAy$SS&@NN9Obf{HN3U~u;$PHW}5 zDO_pjBGOy~T<(6y_dBT{4KvD>=0d0sAs&43PZ*@!{Z8w1dY>8TsOyQUPoFb!4{cF` zC|R%mKw%+tA*$qb@axlu61fnyQoA_t$~1}gnvqV?-ohVI{9=*e>Q2|UI~~O3a?MC5 zZv9568R>aQ*grjn)-%v`@?cGn)(Zqsz$m_?(+x^@TslfYE5HU419VEJUg%pAxx6#d zO^GwJK|2(A4Cb2jGWd}05*3r4#&%U~@?c^;G!{sp&uc8;bCTl33z5em^k|r%A0k~p z_Dj{Dd65)QE?(t+RdM94uIEisUslROi+C{ZgnLSp|?w-6G7|)0^L!UUv?$v~F0_K!jsiftT8yV_6RxA|07I?zS+tBl&`^gc zS_>FAgb+lVrS-Y+^FT)x{uA(Rya&O?l-VfFkBzvxb!OgU+>>3i+9u^CB+y6wlmzoS z~X>b4Pwg4c14KqQ+uEtVyjx1_x4r>m+j(85pt{QtpwS|SaTd7>U z(t-m0vYM6C9L4@tlh}(v12)xcrk$H6K_fZi$6{}8{MFS|XXTU^X5~P|lVG(-niHs) zQHpag1dz6h&!J`Y0qp$?5G2JDa~guY=Sfb0wr{M>!G_*BFc;K|wt>w-HL<`Rn~Weo z>^LTzP+;;S5XFW}A#B7Kh&DxXc%}FxGAV4@icQsO{Ui%4ANRLMZQd9JacmzD^7AHn zxYb6x9g%r*+hFlvV;>QsBn&kwoA(J1b!&$94x&ZoS@bq(+idDKKs(^q`XkX3k&S)z zkPq#* #}9L5%4QLVi$7PM1aOqpf>S!H84E;0^m?Ll{IPzhYAqB_H_O4fvIz0rvs z3~_7ku0L*JhmHD%0I`5@(E}n7sfRt<*kh`u31%V{sg8yg`!(mq*v`{#=S`Bi%usnF zBt|V5MF?PLa_n4XlfYOU$N}3VV$TFE7bAPnzyl8W*Z877=EEDnYXg@|S#lBL#DY9EhSJn>GhQh|3f!Tx)r42r+eJE08+IXiS?-LolGN ziV97IM_ZgeW7ah3NMqTCSn25WQ72XctB*QgEe_HM2?sW(E03L2M1mw4ppZ~CE=Ki6 zIbtbV>Z~^ug7vPorL`Ype$p;rP$WX^LsEw=!KEW7IiOK-HYggloI#K`r@$5aH&m13 z1_YrNkuj{9bwk_L;s&gI{8*6$cY<9V7%N;$v#a4!QkaZJ!@inv3Pw&sfaYWMrnPTs zjFL;KyDXTtjzALXQjPMphDcgsws8$y8*q2wv?4^$O(7q3(4p!@=$>GG=x+Qut+h}x z#=4`22pP+Iyg>s{_hEipG>94Z%-CcGJTopCI&*cVH|cEoj%U)nC(p$u-T&l@4_PXl z;5~}ejZwX`N8H^tFDEt;{W_bK=#7Oq?8cLXnU@oL(~U<8Gk+%@PgXt6dvW7KkeM$N zPoJX9yqkEuH`YCQV<8T^F&oIpKlY{@zcg2gJmc|HWu7hL@qS(3UE}fo%DkV%;~sVR zsQDRqlfXBqr>2y|l5*Is1}HOsD)y#ZrFYGnipMcasfT$xZp?N%X!~MGh5sNty!C`< zD6g+4JX2u@?;iNzdB2Cl&2Lvn-*7848!Y~wn`f`aV-$1KCJ;RwZnNow6=0VHvib?@gmfHT#6v!o-}Vah|rCKn|XES=5G;jVK!Qs z$kQb^o@V@L{q6%!{LMT)Ay;28{n2*P2Ml{Ee;RPg_uz6Lv!MFZLG#85|I~qx5PV-q z)AIyL(2o-QDZve&Qw3Kt@512Y1h*XcX@Ywk_+-HkJIXUv@J>g*6@qVf;J*}npMy`W z;13BsUV-?C3clHaUoQ9t2miH#Z*kDyXXt}I%@}by$a8m3dZF*xF7yL^e_5glW6nL% zj{-ej?2qaP=!>K_i_nW@ELQu1>eV@q1I6>&EguiLO zd4g|t@EI@ojUqS0|1{x0XPlS$@*WBZl?wjBB#r-*?_v)t!9Tf0dp|2LkF&@dhL!&SHQE5Od0|~EXJXLL-?PUb-`+VFY{Ht!(ayI(COYnLJzESWM zg5%MHkIjsuJk^>{RKw~qp*Q2B;s281BlFVGIQbX=f-KA;c8;?<4E^1jKRSIr{v!D0 z4t>1|yeB!({vSQzy`WH%^NNka-=q1b8~ibiXK7f`4>mpV$zwcKHJN4X*O!EW$0EivRldXCLcporg}(J_I>~q@K8BIpHap6{RQPlXZuGTM_%mPdzSM$=AWSsHfg;Wx!odsrVY}3M2%{*;H%|1q?hntfQCcm?{Kv1 zM}&WsJntF)j|-n!Cush>zmLM+b4;J9IvPx}lW|R>jSKkVsbH{oazd-1Z2)_P^#*KXXK)*fN z`Eb#@nI~%OEnD!+r**zYZn?}SRsC&<=Fj^;A#eH#mg;rSPa5YnFTm-yKf+&|rSUPq z=$OL%Gw>Lt`5XPt5c-)byiCXIDG{10_+hb!NBFK%*YUV>^m_{ZphEd>xmNSxb(2U_ z#rbBcEslO>kQiZtMn0DbpGTH!KI@Su9ajkcnCQ#k z*9reJM?1ZZ>2=!J^BJ)7p7i+eG3d7n|Exd8>v22d=*Ma`4zuCoRpyhb=E^v0^zxSQ z$re6_{vDzJUiAC2@Yyf)H#+3}mC!ef{e*=6UqZi6=#4!8Ex1?m%@X=v_*zfxu}W}L z&VGW|JLEZ3aClQ>4yOF01P?pplMlQnIZtCeRlRzOm-)<-^3d9m-pGyiT%vISj)Ryp z?Q2QLTH*7%8D5V6na@hyCVVyspUVZmQ|Qm!ujwxpd^6(`iMc$>d@@w0qh0(-@a>L% z_+`d3Ri;B z+|q!PUc7H;{=5bhylDT@p6nr0_~bkI3>7{rZ`6E@ozu_3l$}{ zCkgJAe6vtSI;I1s^3NaRfd7jrk}YTzc4fZ9r5M&fS#Tc zoX^R_fcIo?1&pVv*<#P;J?J#S)4%X?`FOoALT3S|eqfhloUJ?t|2pAgPtkn7U~ZV5 z$9ytXSnSZ$cd5{?IYZM=7y1=Kzroa31aXzn-=CrB`%49iaG&I}`PF#&+#-BB1vh#* z{TSom9m4;O3eBJQw?dgV89qBT|K3v02Y_cuIQByOkCEKMj{fRDg#QgiUM628iM9*A zTfQ5Z=bYCVkL9ex9}@qB3{@ul4aEV%Nneis^T%WG>6fDAwoB>-GCtB7@BU6}?C=EO zWY729;bl6SK1fHl@M(7Fw@~PRl6u{%$<;)r&rn+&LvB|yo}u=MelvysI^nZQ+HaQN8wK|XZtU|h!K>uEQ?1ZH&-}sl z_4soBS#ZmN?-bl4I9{Lmp#7(N>Sw+X`WmShxLDq=vH$VF$*#VZae1)V z)nuXf3V&m_Qv|=l!KX~{phNHTh5w!M-5@CCJYVRmg#QY`3n3p5SkcDhOUDEYpm?<)16&>!+@g!j5c-cJZ_ zeWh{UD*||@@Yx{kD;pRcI|M)Mum{>Vo$Tg#RwF2V*}+fRlbbf(v_8QaLkPT92>lA7H~rY<27gQI(a7N{!Ogl{^IiQ~ z!Jl==;b!2Z_l?);eEUoJHwwN??9=qaj~o7P$LIUB(2sas^Wi;kz-t^56907~=Lw?6 zPUe%Lo|5)r%KstrkwU~=wjBe1hxufxJ011<;28AepMc79t@M-qBo7qXVes@?P@`(z5`fa-WnWD#Kf`?Ag_#~lU#r!kWVaNB? zwM;KWF_%qDpQ#$9oWfo`DEJnVlIb|f%nFDY0`_5@mJ@98OQv+I#rFlRU<~ugM~ii zkk3e_kI7Ji6Nnzq`Of~oRQRV!z0C9E65;Qa@|b?OT<{i0zUK+P(9s`O3IDHT+`nEF z84!HunYvzuQqE@K^LvN<+XcVE!T%D*GgQ5dzowikg?@#D&(*-Gz4u-Y<9@*t<@b@X8di@AK4G_)kE`M=*{##$5ghM3Gd+vizc+xjq|rQ6c$cw zs1Fneo0=9cs$W`H-Cox*t|mVRliPE6iR*tq)m@WeR$O&0yt(Iw;Qp-@Axy=?1kYyp zwu28+n*E4*eA*?OU4u!$5!=_+0UwFYVfG%FJ0ZVlLeE5)&Kqp7*|#$0^hH~js6ZNxT;#*X}j-=G0LVe{q!*gs*lqFtuf3lw7aojw_fj7Ebqk zVU)}^&bo5P7Ec_fXg)FKp5~4lJF!^(f2#&lE}_ObKsYomPScVV8U{eTFJEzwxcKp@c7OlmcRhlAP zan5`-*AA%=rawpOu@Hnz2lJ*Et8iPCrp$W1XU&>1rPRh`{oHXnx!=YdVKo~w)I)w% z*Ve!;0jbiewmBSKg30<=xDml*V$3g%s!F?rnUZr~RTGGid0?6~T!Gs2&c(FQ)}TMU zBtDm5WxcP4jfEW-lIK=XHHYJ=;E0-L!>S18=AtGu3*m5$r_+kRL-NQWncKvm2upE6CAl~k75bLJ`Ii#-%3W3dLTs2MY-BQQ7cgrYF59HP)= zjKW*8AM@Kuh4l_grAg#u!trG!kI8Bdl4+?e3Sk2O!iDH%cxegANLy!32yVeufZZye zUs6%2+8ZJ|&pEA?q;I$_r&SA>uZ}Ysa<^|k?%&uBQLLlOB`yJNzb_0YthL;WwT03C z{LMAA0E7k^ZpSU!nCnPZ(4SV3Hl5P)Iq=mP38McaFU%?&h7;FXf1`HbO?H9q!clRU zmmO(r2&#!Rner zL0vG6Nb_fxPo0Kt5(1%hdC(O)W@EO;OR$M(_%V-@+YbuPMK zzq;t!wMHYziQVl+F*XGnI@I|=HJ=1Nom?cB*z>UZ56wtFy+mLkt!PcYKy7r1I=@~` z_u(ESNR2;&jsoV3g+IX%wSE<70>@bE2 zNEWXIxmlo{?gnV_l?nu)j{11I2tT}-4jw~}?&ucRH~8yy!|ig)Tv-Vnkb1}|=n`3q zg*u@}hlWsUg%9%%}dqNC@JDTVXhtrbQ%S5~3z5#K5aZV~Qh$h8MN{@XOt( ztzVaf6v~-!>A0W5=sX`!Yb-b{m8!89`!I}mK)B#UR@I_P>#^>N9yF^X5wUeJs^bQX zu9zJfLxku^+k$WtUJX&BrTN2cFn8|W+akU?@y!j3XbVMsusx%Q)-G44su{~5<|bJxs>vzYR}3sC_%Dr!7cb0j!ZbK$NrH7-z6@lvZ`dTSc&TvF>20rc{i8mPI_3Uq30* z6Rmlg-2@AS$sKbI~p9>&`5!zRZ7vC8Zgu^^0oU^fL8>?C%5hS zvrFaSSU=tCCfI;C8LSCH_eLupG1zG5<`^@eQuLBduv&jDjb?s4MxwGf&-QgxhiaD4 z2&MZ-j9=QBI+AglCAY^mm6%q3p|8Me2W(PXYdx+ZjJfsH3a5~$M6}u*xf?}?&SR?d z-Gz9XV!2BkEj-$azxXP)n0~T4)B+Q2;WewapPqK?YU;$g$&2v#VRJ8tZY_#uItME* zseVR|D3u#o(u|7Yir$*9^(F*8)wYIJE*_+7b4#Yo$icXwaAPV zi=*Ey>8Rqf))57r^=|=2>8H?59A^F8rzX9~kK{iH|IYNk0!A{S^3h?|*_Gk@6df7* z(sdTKbj8~dicN3U<5fxe3R5vj;c;9qb)+}H_ihow6Mm8ej&ufH?MQFdWxn1|Yg*K3 z$XQlh5d_vqdQ(iZ4sf5O&&-dd?v|fHZ*rtJ>je*=sq-h_ goto ESTABLISHED; :: rcv ? _ -> skip; od - /* We may want to consider putting a timeout -> CLOSED here. */ ESTABLISHED: state[i] = EstState; do @@ -139,8 +133,8 @@ end: init { state[0] = ClosedState; state[1] = ClosedState; - run TCP(AtoN, NtoA, 0); - run TCP(BtoN, NtoB, 1); + run TCP(AtoB, BtoA, 0); + run TCP(BtoA, AtoB, 1); } /* safety: half-open prevention */ diff --git a/tests/tcp/tcp-phi2.pml b/tests/tcp/tcp-phi2.pml index 960a173..620854f 100644 --- a/tests/tcp/tcp-phi2.pml +++ b/tests/tcp/tcp-phi2.pml @@ -1,12 +1,7 @@ -// models: phi1, phi2, phi3, phi5 -// does not model: phi4, phi7 -// not yet implemented: phi6 mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } -chan AtoN = [2] of { mtype }; -chan NtoA = [2] of { mtype }; -chan BtoN = [2] of { mtype }; -chan NtoB = [2] of { mtype }; +chan AtoB = [2] of { mtype }; +chan BtoA = [2] of { mtype }; int state[2]; int pids[2]; @@ -80,7 +75,6 @@ SYN_RECEIVED: :: rcv ? ACK -> goto ESTABLISHED; :: rcv ? _ -> skip; od - /* We may want to consider putting a timeout -> CLOSED here. */ ESTABLISHED: state[i] = EstState; do @@ -139,8 +133,8 @@ end: init { state[0] = ClosedState; state[1] = ClosedState; - run TCP(AtoN, NtoA, 0); - run TCP(BtoN, NtoB, 1); + run TCP(AtoB, BtoA, 0); + run TCP(BtoA, AtoB, 1); } /* liveness: verifying connection establishment */ diff --git a/tests/tcp/tcp-phi2.pml.trail b/tests/tcp/tcp-phi2.pml.trail index 319ff39..7c3fba0 100644 --- a/tests/tcp/tcp-phi2.pml.trail +++ b/tests/tcp/tcp-phi2.pml.trail @@ -1,55 +1,53 @@ --2:2:-2 +-2:3:-2 -4:-4:-4 -1:0:121 -2:1:114 -3:0:121 -4:1:115 -5:0:121 -6:1:116 -7:0:121 -8:1:117 -9:0:121 -10:3:0 -11:0:121 -12:3:1 -13:0:121 -14:3:2 -15:0:121 -16:3:9 -17:0:121 -18:2:0 -19:0:121 -20:2:1 -21:0:121 -22:2:2 -23:0:121 -24:2:9 -25:0:121 -26:3:17 -27:0:121 -28:3:1 -29:0:121 -30:3:3 -31:0:121 -32:3:22 -33:0:119 -34:2:17 -35:0:126 -36:2:1 -37:0:121 -38:2:3 -39:0:121 -40:2:22 -41:0:121 -42:2:42 -43:0:121 -44:2:1 +1:0:129 +2:2:122 +3:0:129 +4:2:123 +5:0:129 +6:2:124 +7:0:129 +8:2:125 +9:0:129 +10:4:0 +11:0:129 +12:4:1 +13:0:129 +14:4:2 +15:0:129 +16:4:9 +17:0:129 +18:3:0 +19:0:129 +20:3:1 +21:0:129 +22:3:2 +23:0:129 +24:3:9 +25:0:129 +26:4:17 +27:0:129 +28:4:1 +29:0:129 +30:4:3 +31:0:129 +32:4:22 +33:0:127 +34:1:116 -1:-1:-1 -45:0:121 -46:2:2 -47:0:121 -48:2:9 -49:0:119 -50:2:17 -51:0:126 -52:2:1 +35:0:134 +36:1:117 +37:0:127 +38:3:15 +39:0:134 +40:3:16 +41:0:127 +42:4:42 +43:0:134 +44:4:1 +45:0:129 +46:4:3 +47:0:129 +48:4:22 +49:0:127 +50:1:116 diff --git a/tests/tcp/tcp-phi3.pml b/tests/tcp/tcp-phi3.pml index 35a9049..45f6418 100644 --- a/tests/tcp/tcp-phi3.pml +++ b/tests/tcp/tcp-phi3.pml @@ -1,12 +1,7 @@ -// models: phi1, phi2, phi3, phi5 -// does not model: phi4, phi7 -// not yet implemented: phi6 mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } -chan AtoN = [2] of { mtype }; -chan NtoA = [2] of { mtype }; -chan BtoN = [2] of { mtype }; -chan NtoB = [2] of { mtype }; +chan AtoB = [2] of { mtype }; +chan BtoA = [2] of { mtype }; int state[2]; int pids[2]; @@ -80,7 +75,6 @@ SYN_RECEIVED: :: rcv ? ACK -> goto ESTABLISHED; :: rcv ? _ -> skip; od - /* We may want to consider putting a timeout -> CLOSED here. */ ESTABLISHED: state[i] = EstState; do @@ -139,8 +133,8 @@ end: init { state[0] = ClosedState; state[1] = ClosedState; - run TCP(AtoN, NtoA, 0); - run TCP(BtoN, NtoB, 1); + run TCP(AtoB, BtoA, 0); + run TCP(BtoA, AtoB, 1); } /* liveness: no infinite stalls/deadlocks */ diff --git a/tests/tcp/tcp-phi3.pml.trail b/tests/tcp/tcp-phi3.pml.trail new file mode 100644 index 0000000..bb2a009 --- /dev/null +++ b/tests/tcp/tcp-phi3.pml.trail @@ -0,0 +1,62 @@ +-2:3:-2 +-4:-4:-4 +1:0:289 +2:2:122 +3:0:289 +4:2:123 +5:0:289 +6:2:124 +7:0:289 +8:2:125 +9:0:289 +10:4:0 +11:0:289 +12:4:1 +13:0:289 +14:4:2 +15:0:289 +16:4:9 +17:0:289 +18:3:0 +19:0:289 +20:3:1 +21:0:289 +22:3:2 +23:0:289 +24:3:9 +25:0:289 +26:4:17 +27:0:289 +28:4:1 +29:0:289 +30:4:3 +31:0:289 +32:4:22 +33:0:289 +34:1:116 +35:0:289 +36:1:117 +37:0:289 +38:3:10 +39:0:289 +40:3:11 +41:3:12 +42:0:289 +43:3:47 +44:0:249 +45:1:114 +46:0:599 +47:1:115 +48:0:599 +49:4:40 +50:0:599 +51:4:41 +52:0:599 +53:1:114 +54:0:599 +55:1:115 +56:0:599 +57:4:31 +-1:-1:-1 +58:0:599 +59:0:599 diff --git a/tests/tcp/tcp-phi4.pml b/tests/tcp/tcp-phi4.pml index 68c2d48..b34fa36 100644 --- a/tests/tcp/tcp-phi4.pml +++ b/tests/tcp/tcp-phi4.pml @@ -1,12 +1,7 @@ -// models: phi1, phi2, phi3, phi5 -// does not model: phi4, phi7 -// not yet implemented: phi6 mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } -chan AtoN = [2] of { mtype }; -chan NtoA = [2] of { mtype }; -chan BtoN = [2] of { mtype }; -chan NtoB = [2] of { mtype }; +chan AtoB = [2] of { mtype }; +chan BtoA = [2] of { mtype }; int state[2]; int pids[2]; @@ -80,7 +75,6 @@ SYN_RECEIVED: :: rcv ? ACK -> goto ESTABLISHED; :: rcv ? _ -> skip; od - /* We may want to consider putting a timeout -> CLOSED here. */ ESTABLISHED: state[i] = EstState; do @@ -139,8 +133,8 @@ end: init { state[0] = ClosedState; state[1] = ClosedState; - run TCP(AtoN, NtoA, 0); - run TCP(BtoN, NtoB, 1); + run TCP(AtoB, BtoA, 0); + run TCP(BtoA, AtoB, 1); } /* liveness: simultanous open */ diff --git a/tests/tcp/tcp-phi4.pml.trail b/tests/tcp/tcp-phi4.pml.trail index 08508a0..88bdbca 100644 --- a/tests/tcp/tcp-phi4.pml.trail +++ b/tests/tcp/tcp-phi4.pml.trail @@ -1,43 +1,322 @@ --2:2:-2 +-2:3:-2 -4:-4:-4 -1:0:122 -2:1:114 -3:0:122 -4:1:115 -5:0:122 -6:1:116 -7:0:122 -8:1:117 -9:0:122 -10:3:0 -11:0:122 -12:3:1 -13:0:122 -14:3:2 -15:0:122 -16:3:9 -17:0:122 -18:2:0 -19:0:122 -20:2:1 -21:0:122 -22:2:2 -23:0:122 -24:2:9 -25:0:122 -26:3:17 -27:0:122 -28:3:1 -29:0:122 -30:3:3 -31:0:122 -32:3:22 -33:0:122 -34:2:17 -35:0:122 -36:2:1 -37:0:122 -38:2:3 -39:0:122 -40:2:22 -41:0:119 +1:0:130 +2:2:122 +3:0:130 +4:2:123 +5:0:130 +6:2:124 +7:0:130 +8:2:125 +9:0:130 +10:4:0 +11:0:130 +12:4:1 +13:0:130 +14:4:2 +15:0:130 +16:4:9 +17:0:130 +18:3:0 +19:0:130 +20:3:1 +21:0:130 +22:3:2 +23:0:130 +24:3:9 +25:0:130 +26:4:17 +27:0:130 +28:4:1 +29:0:130 +30:4:3 +31:0:130 +32:4:22 +33:0:130 +34:1:116 +35:0:130 +36:1:117 +37:0:130 +38:3:10 +39:0:130 +40:3:11 +41:3:12 +42:0:130 +43:3:47 +44:0:130 +45:1:114 +46:0:130 +47:1:115 +48:0:130 +49:4:23 +50:0:130 +51:4:27 +52:0:130 +53:4:47 +54:0:130 +55:1:114 +56:0:130 +57:1:115 +58:0:130 +59:4:48 +60:0:130 +61:4:55 +62:0:130 +63:4:56 +64:0:130 +65:4:66 +66:0:130 +67:1:116 +68:0:130 +69:1:117 +70:0:130 +71:3:48 +72:0:130 +73:3:55 +74:0:130 +75:3:56 +76:0:130 +77:3:66 +78:0:130 +79:1:114 +80:0:130 +81:1:115 +82:0:130 +83:4:67 +84:0:130 +85:4:68 +86:0:130 +87:4:94 +88:0:130 +89:1:116 +90:0:130 +91:1:117 +92:0:130 +93:3:67 +94:0:130 +95:3:68 +96:0:130 +97:3:94 +98:0:130 +99:1:114 +100:0:130 +101:1:115 +102:0:130 +103:4:95 +104:0:130 +105:4:110 +106:0:130 +107:4:1 +108:0:130 +109:4:2 +110:0:130 +111:4:9 +112:0:130 +113:1:116 +114:0:130 +115:1:117 +116:0:130 +117:3:95 +118:0:130 +119:3:110 +120:0:130 +121:3:1 +122:0:130 +123:3:2 +124:0:130 +125:3:9 +126:0:130 +127:4:17 +128:0:130 +129:4:1 +130:0:130 +131:4:3 +132:0:130 +133:1:116 +134:0:130 +135:1:117 +136:0:130 +137:3:10 +138:0:130 +139:3:11 +140:3:12 +141:0:130 +142:3:47 +143:0:130 +144:1:114 +145:0:130 +146:1:115 +147:0:130 +148:1:114 +149:0:130 +150:4:22 +151:0:130 +152:4:23 +153:0:130 +154:4:27 +155:0:130 +156:1:115 +157:0:130 +158:1:116 +159:0:130 +160:4:47 +161:0:130 +162:4:48 +163:0:130 +164:4:55 +165:0:130 +166:4:56 +167:0:130 +168:1:117 +169:0:130 +170:3:48 +171:0:130 +172:3:55 +173:0:130 +174:3:56 +175:0:130 +176:3:66 +177:0:130 +178:1:114 +179:0:130 +180:1:115 +181:0:130 +182:1:116 +183:0:130 +184:4:66 +185:0:130 +186:4:67 +187:0:130 +188:4:68 +189:0:130 +190:1:117 +191:0:130 +192:3:67 +193:0:130 +194:3:68 +195:0:130 +196:3:94 +197:0:130 +198:1:114 +199:0:130 +200:1:115 +201:0:130 +202:1:116 +203:0:130 +204:4:94 +205:0:130 +206:4:95 +207:0:130 +208:4:110 +209:0:130 +210:4:1 +211:0:130 +212:4:2 +213:0:130 +214:1:117 +215:0:130 +216:3:95 +217:0:130 +218:3:110 +219:0:130 +220:3:1 +221:0:130 +222:3:3 +223:0:130 +224:4:9 +225:0:130 +226:3:22 +227:0:130 +228:1:114 +229:0:130 +230:1:115 +231:0:130 +232:4:10 +233:0:130 +234:4:11 +235:4:12 +236:0:130 +237:4:47 +238:0:130 +239:1:116 +240:0:130 +241:1:117 +242:0:130 +243:3:23 +244:0:130 +245:3:27 +246:0:130 +247:1:114 +248:0:130 +249:1:115 +250:0:130 +251:4:48 +252:0:130 +253:4:55 +254:0:130 +255:4:56 +256:0:130 +257:4:66 +258:0:130 +259:1:116 +260:0:130 +261:1:117 +262:0:130 +263:1:116 +264:0:130 +265:3:47 +266:0:130 +267:3:48 +268:0:130 +269:3:55 +270:0:130 +271:3:56 +272:0:130 +273:3:66 +274:0:130 +275:1:117 +276:0:130 +277:3:67 +278:0:130 +279:3:68 +280:0:130 +281:1:114 +282:0:130 +283:1:115 +284:0:130 +285:4:67 +286:0:130 +287:1:114 +288:0:130 +289:4:68 +290:0:130 +291:4:94 +292:0:130 +293:1:115 +294:0:130 +295:4:95 +296:0:130 +297:4:110 +298:0:130 +299:4:1 +300:0:130 +301:4:3 +302:0:130 +303:4:22 +304:0:130 +305:3:94 +306:0:130 +307:1:116 +308:0:130 +309:1:117 +310:0:130 +311:3:95 +312:0:130 +313:3:110 +314:0:130 +315:3:1 +316:0:130 +317:3:3 +318:0:130 +319:3:22 +320:0:127 diff --git a/tests/tcp/tcp-phi5.pml b/tests/tcp/tcp-phi5.pml index 417ac59..3b65921 100644 --- a/tests/tcp/tcp-phi5.pml +++ b/tests/tcp/tcp-phi5.pml @@ -1,12 +1,7 @@ -// models: phi1, phi2, phi3, phi5 -// does not model: phi4, phi7 -// not yet implemented: phi6 mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } -chan AtoN = [2] of { mtype }; -chan NtoA = [2] of { mtype }; -chan BtoN = [2] of { mtype }; -chan NtoB = [2] of { mtype }; +chan AtoB = [2] of { mtype }; +chan BtoA = [2] of { mtype }; int state[2]; int pids[2]; @@ -80,7 +75,6 @@ SYN_RECEIVED: :: rcv ? ACK -> goto ESTABLISHED; :: rcv ? _ -> skip; od - /* We may want to consider putting a timeout -> CLOSED here. */ ESTABLISHED: state[i] = EstState; do @@ -139,8 +133,8 @@ end: init { state[0] = ClosedState; state[1] = ClosedState; - run TCP(AtoN, NtoA, 0); - run TCP(BtoN, NtoB, 1); + run TCP(AtoB, BtoA, 0); + run TCP(BtoA, AtoB, 1); } /* liveness: SYN_RECEIVED resolution*/ diff --git a/tests/tcp/tcp-phi5.pml.trail b/tests/tcp/tcp-phi5.pml.trail new file mode 100644 index 0000000..3ac1dc9 --- /dev/null +++ b/tests/tcp/tcp-phi5.pml.trail @@ -0,0 +1,86 @@ +-2:3:-2 +-4:-4:-4 +1:0:129 +2:2:122 +3:0:129 +4:2:123 +5:0:129 +6:2:124 +7:0:129 +8:2:125 +9:0:129 +10:4:0 +11:0:129 +12:4:1 +13:0:129 +14:4:2 +15:0:129 +16:4:9 +17:0:129 +18:3:0 +19:0:129 +20:3:1 +21:0:129 +22:3:2 +23:0:129 +24:3:9 +25:0:129 +26:4:17 +27:0:129 +28:4:1 +29:0:129 +30:4:3 +31:0:129 +32:4:22 +33:0:129 +34:1:116 +35:0:129 +36:1:117 +37:0:129 +38:3:10 +39:0:129 +40:3:11 +41:3:12 +42:0:129 +43:3:47 +44:0:127 +45:1:114 +46:0:134 +47:1:115 +48:0:134 +49:4:23 +50:0:134 +51:4:27 +52:0:134 +53:4:47 +54:0:134 +55:1:114 +56:0:134 +57:1:115 +58:0:134 +59:4:48 +60:0:134 +61:4:55 +62:0:134 +63:4:56 +64:0:134 +65:4:66 +66:0:134 +67:1:116 +68:0:134 +69:1:117 +70:0:134 +71:3:50 +72:0:134 +73:3:51 +74:0:134 +75:1:116 +76:0:134 +77:1:117 +78:0:134 +79:3:50 +80:0:134 +81:3:51 +-1:-1:-1 +82:0:134 +83:0:134 diff --git a/tests/tcp/tcp-phi6.pml b/tests/tcp/tcp-phi6.pml index 2cf306a..d0cf9a0 100644 --- a/tests/tcp/tcp-phi6.pml +++ b/tests/tcp/tcp-phi6.pml @@ -1,12 +1,7 @@ -// models: phi1, phi2, phi3, phi5 -// does not model: phi4, phi7 -// not yet implemented: phi6 mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } -chan AtoN = [2] of { mtype }; -chan NtoA = [2] of { mtype }; -chan BtoN = [2] of { mtype }; -chan NtoB = [2] of { mtype }; +chan AtoB = [2] of { mtype }; +chan BtoA = [2] of { mtype }; int state[2]; int pids[2]; @@ -80,7 +75,6 @@ SYN_RECEIVED: :: rcv ? ACK -> goto ESTABLISHED; :: rcv ? _ -> skip; od - /* We may want to consider putting a timeout -> CLOSED here. */ ESTABLISHED: state[i] = EstState; do @@ -139,8 +133,8 @@ end: init { state[0] = ClosedState; state[1] = ClosedState; - run TCP(AtoN, NtoA, 0); - run TCP(BtoN, NtoB, 1); + run TCP(AtoB, BtoA, 0); + run TCP(BtoA, AtoB, 1); } /* safety: strict closing transitions */ diff --git a/tests/tcp/tcp-phi6.pml.trail b/tests/tcp/tcp-phi6.pml.trail new file mode 100644 index 0000000..8bc7191 --- /dev/null +++ b/tests/tcp/tcp-phi6.pml.trail @@ -0,0 +1,122 @@ +-2:3:-2 +-4:-4:-4 +1:0:129 +2:2:122 +3:0:129 +4:2:123 +5:0:129 +6:2:124 +7:0:129 +8:2:125 +9:0:129 +10:4:0 +11:0:129 +12:4:1 +13:0:129 +14:4:2 +15:0:129 +16:4:9 +17:0:129 +18:3:0 +19:0:129 +20:3:1 +21:0:129 +22:3:2 +23:0:129 +24:3:9 +25:0:129 +26:4:17 +27:0:129 +28:4:1 +29:0:129 +30:4:3 +31:0:129 +32:4:22 +33:0:129 +34:1:116 +35:0:129 +36:1:117 +37:0:129 +38:3:10 +39:0:129 +40:3:11 +41:3:12 +42:0:129 +43:3:47 +44:0:129 +45:1:114 +46:0:129 +47:1:115 +48:0:129 +49:4:23 +50:0:129 +51:4:27 +52:0:129 +53:4:47 +54:0:129 +55:1:114 +56:0:129 +57:1:115 +58:0:129 +59:4:48 +60:0:129 +61:4:55 +62:0:129 +63:4:56 +64:0:129 +65:4:66 +66:0:129 +67:1:116 +68:0:129 +69:1:117 +70:0:129 +71:3:48 +72:0:129 +73:3:55 +74:0:129 +75:3:56 +76:0:129 +77:3:66 +78:0:129 +79:1:114 +80:0:129 +81:1:115 +82:0:129 +83:4:67 +84:0:129 +85:4:68 +86:0:129 +87:4:94 +88:0:129 +89:1:116 +90:0:129 +91:1:117 +92:0:129 +93:3:67 +94:0:129 +95:3:68 +96:0:129 +97:3:94 +98:0:129 +99:1:114 +100:0:129 +101:1:115 +102:0:129 +103:4:95 +104:0:129 +105:4:110 +106:0:129 +107:4:1 +108:0:129 +109:4:2 +110:0:129 +111:4:9 +112:0:129 +113:1:116 +114:0:129 +115:1:117 +116:0:129 +117:3:95 +118:0:127 +119:3:110 +120:0:134 diff --git a/tests/tcp/tcp.pml b/tests/tcp/tcp.pml index 4e39675..1792fbe 100644 --- a/tests/tcp/tcp.pml +++ b/tests/tcp/tcp.pml @@ -1,12 +1,7 @@ -// models: phi1, phi2, phi3, phi5 -// does not model: phi4, phi7 -// not yet implemented: phi6 mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } -chan AtoN = [2] of { mtype }; -chan NtoA = [2] of { mtype }; -chan BtoN = [2] of { mtype }; -chan NtoB = [2] of { mtype }; +chan AtoB = [2] of { mtype }; +chan BtoA = [2] of { mtype }; int state[2]; int pids[2]; @@ -80,7 +75,6 @@ SYN_RECEIVED: :: rcv ? ACK -> goto ESTABLISHED; :: rcv ? _ -> skip; od - /* We may want to consider putting a timeout -> CLOSED here. */ ESTABLISHED: state[i] = EstState; do @@ -139,6 +133,6 @@ end: init { state[0] = ClosedState; state[1] = ClosedState; - run TCP(AtoN, NtoA, 0); - run TCP(BtoN, NtoB, 1); + run TCP(AtoB, BtoA, 0); + run TCP(BtoA, AtoB, 1); }