From 3dcbf9715088e7b06a9a0ed70275fdbd4f1e46aa Mon Sep 17 00:00:00 2001
From: Xavier Denis <xldenis@gmail.com>
Date: Fri, 26 Jul 2024 10:31:38 +0200
Subject: [PATCH] stabilize proof

---
 .../list_reversal_lasso/why3session.xml       | 162 ++++--------------
 .../list_reversal_lasso/why3shapes.gz         | Bin 7478 -> 7562 bytes
 2 files changed, 36 insertions(+), 126 deletions(-)

diff --git a/creusot/tests/should_succeed/list_reversal_lasso/why3session.xml b/creusot/tests/should_succeed/list_reversal_lasso/why3session.xml
index 1fdd2a63f0..e039e18042 100644
--- a/creusot/tests/should_succeed/list_reversal_lasso/why3session.xml
+++ b/creusot/tests/should_succeed/list_reversal_lasso/why3session.xml
@@ -5,86 +5,26 @@
 <prover id="0" name="Z3" version="4.12.4" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="1" name="Alt-Ergo" version="2.5.3" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="2" name="CVC5" version="1.0.5" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="3" name="CVC4" version="1.8" timelimit="1" steplimit="0" memlimit="1000"/>
 <file format="coma" proved="true">
 <path name=".."/><path name="list_reversal_lasso.coma"/>
-<theory name="Core_Ptr_NonNull_NonNull_Type" proved="true">
- <goal name="vc_t_nonnull" proved="true">
- <proof prover="2"><result status="valid" time="0.008053" steps="27"/></proof>
- </goal>
-</theory>
-<theory name="Core_Marker_PhantomData_Type" proved="true">
- <goal name="vc_t_phantomdata" proved="true">
- <proof prover="2"><result status="valid" time="0.008700" steps="27"/></proof>
- </goal>
-</theory>
-<theory name="Core_Ptr_Unique_Unique_Type" proved="true">
- <goal name="vc_t_unique" proved="true">
- <proof prover="2"><result status="valid" time="0.007423" steps="27"/></proof>
- </goal>
-</theory>
-<theory name="Alloc_RawVec_Cap_Type" proved="true">
- <goal name="vc_t_cap" proved="true">
- <proof prover="2"><result status="valid" time="0.000001" steps="189"/></proof>
- </goal>
-</theory>
-<theory name="Alloc_RawVec_RawVec_Type" proved="true">
- <goal name="vc_t_rawvec" proved="true">
- <proof prover="2"><result status="valid" time="0.002921" steps="189"/></proof>
- </goal>
-</theory>
-<theory name="Alloc_Vec_Vec_Type" proved="true">
- <goal name="vc_t_vec" proved="true">
- <proof prover="2"><result status="valid" time="0.004360" steps="189"/></proof>
- </goal>
-</theory>
-<theory name="Alloc_Alloc_Global_Type" proved="true">
- <goal name="vc_t_global" proved="true">
- <proof prover="2"><result status="valid" time="0.000001" steps="27"/></proof>
- </goal>
-</theory>
-<theory name="ListReversalLasso_Memory_Type" proved="true">
- <goal name="vc_t_memory" proved="true">
- <proof prover="2"><result status="valid" time="0.000001" steps="189"/></proof>
- </goal>
-</theory>
 <theory name="ListReversalLasso_Impl1_Index" proved="true">
- <goal name="vc_index&#39;0" proved="true">
- <proof prover="2"><result status="valid" time="0.010572" steps="4967"/></proof>
- </goal>
  <goal name="vc_index" proved="true">
  <proof prover="2"><result status="valid" time="0.028439" steps="9477"/></proof>
  </goal>
 </theory>
 <theory name="ListReversalLasso_Impl2_IndexMut" proved="true">
- <goal name="vc_index_mut&#39;0" proved="true">
- <proof prover="2"><result status="valid" time="0.007065" steps="5210"/></proof>
- </goal>
  <goal name="vc_index_mut" proved="true">
  <proof prover="2"><result status="valid" time="0.056447" steps="13839"/></proof>
  </goal>
 </theory>
 <theory name="ListReversalLasso_Impl4_ListReversalSafe" proved="true">
- <goal name="vc_index_mut&#39;0" proved="true">
- <proof prover="2"><result status="valid" time="0.009311" steps="4924"/></proof>
- </goal>
- <goal name="vc_index&#39;0" proved="true">
- <proof prover="2"><result status="valid" time="0.007023" steps="4924"/></proof>
- </goal>
  <goal name="vc_list_reversal_safe" proved="true">
  <proof prover="2"><result status="valid" time="0.124100" steps="25894"/></proof>
  </goal>
 </theory>
 <theory name="ListReversalLasso_Impl4_ListReversalList" proved="true">
- <goal name="vc_replace&#39;0" proved="true">
- <proof prover="2"><result status="valid" time="0.010478" steps="5187"/></proof>
- </goal>
- <goal name="vc_index_mut&#39;0" proved="true">
- <proof prover="2"><result status="valid" time="0.017108" steps="5187"/></proof>
- </goal>
  <goal name="vc_list_reversal_list" proved="true">
- <proof prover="0"><result status="timeout" time="1.000000" steps="2284627"/></proof>
- <proof prover="1"><result status="timeout" time="1.000000" steps="9923"/></proof>
- <proof prover="2"><result status="timeout" time="1.000000" steps="178269"/></proof>
  <transf name="split_vc" proved="true" >
   <goal name="vc_list_reversal_list.0" expl="loop invariant" proved="true">
   <proof prover="2"><result status="valid" time="0.014781" steps="7045"/></proof>
@@ -132,16 +72,7 @@
  </goal>
 </theory>
 <theory name="ListReversalLasso_Impl4_ListReversalLoop" proved="true">
- <goal name="vc_replace&#39;0" proved="true">
- <proof prover="2"><result status="valid" time="0.009838" steps="5187"/></proof>
- </goal>
- <goal name="vc_index_mut&#39;0" proved="true">
- <proof prover="2"><result status="valid" time="0.007594" steps="5187"/></proof>
- </goal>
  <goal name="vc_list_reversal_loop" proved="true">
- <proof prover="0"><result status="timeout" time="1.000000" steps="2306363"/></proof>
- <proof prover="1"><result status="timeout" time="1.000000" steps="11663"/></proof>
- <proof prover="2"><result status="timeout" time="1.000000" steps="173651"/></proof>
  <transf name="split_vc" proved="true" >
   <goal name="vc_list_reversal_loop.0" expl="loop invariant" proved="true">
   <proof prover="2"><result status="valid" time="0.024544" steps="9418"/></proof>
@@ -162,9 +93,6 @@
   <proof prover="1"><result status="valid" time="0.068348" steps="665"/></proof>
   </goal>
   <goal name="vc_list_reversal_loop.6" expl="postcondition" proved="true">
-  <proof prover="0"><result status="timeout" time="1.000000" steps="1729074"/></proof>
-  <proof prover="1"><result status="timeout" time="1.000000" steps="10836"/></proof>
-  <proof prover="2"><result status="timeout" time="1.000000" steps="133050"/></proof>
   <transf name="split_vc" proved="true" >
    <goal name="vc_list_reversal_loop.6.0" expl="postcondition" proved="true">
    <proof prover="1" timelimit="5" memlimit="2000"><result status="valid" time="4.168868" steps="38855"/></proof>
@@ -208,16 +136,7 @@
  </goal>
 </theory>
 <theory name="ListReversalLasso_Impl4_ListReversalLasso" proved="true">
- <goal name="vc_replace&#39;0" proved="true">
- <proof prover="2"><result status="valid" time="0.010438" steps="5187"/></proof>
- </goal>
- <goal name="vc_index_mut&#39;0" proved="true">
- <proof prover="2"><result status="valid" time="0.013574" steps="5187"/></proof>
- </goal>
  <goal name="vc_list_reversal_lasso" proved="true">
- <proof prover="0"><result status="timeout" time="1.000000" steps="1688325"/></proof>
- <proof prover="1"><result status="timeout" time="1.000000" steps="8476"/></proof>
- <proof prover="2"><result status="timeout" time="1.000000" steps="216314"/></proof>
  <transf name="split_vc" proved="true" >
   <goal name="vc_list_reversal_lasso.0" expl="loop invariant" proved="true">
   <proof prover="2"><result status="valid" time="0.025380" steps="7295"/></proof>
@@ -235,14 +154,8 @@
   <proof prover="2"><result status="valid" time="0.056178" steps="15791"/></proof>
   </goal>
   <goal name="vc_list_reversal_lasso.5" expl="postcondition" proved="true">
-  <proof prover="0"><result status="timeout" time="1.000000" steps="1639253"/></proof>
-  <proof prover="1"><result status="timeout" time="1.000000" steps="7532"/></proof>
-  <proof prover="2"><result status="timeout" time="1.000000" steps="211553"/></proof>
   <transf name="split_vc" proved="true" >
    <goal name="vc_list_reversal_lasso.5.0" expl="postcondition" proved="true">
-   <proof prover="0" timelimit="5" memlimit="2000"><result status="timeout" time="5.000000" steps="8943428"/></proof>
-   <proof prover="1" timelimit="5" memlimit="2000"><result status="timeout" time="5.000000" steps="50619"/></proof>
-   <proof prover="2" timelimit="5" memlimit="2000"><result status="timeout" time="5.000000" steps="704220"/></proof>
    <transf name="inline_goal" proved="true" >
     <goal name="vc_list_reversal_lasso.5.0.0" expl="postcondition" proved="true">
     <transf name="split_all_full" proved="true" >
@@ -256,9 +169,6 @@
      <proof prover="2"><result status="valid" time="0.796825" steps="185143"/></proof>
      </goal>
      <goal name="vc_list_reversal_lasso.5.0.0.3" expl="postcondition" proved="true">
-     <proof prover="0"><result status="timeout" time="1.000000" steps="2602128"/></proof>
-     <proof prover="1"><result status="timeout" time="1.000000" steps="8692"/></proof>
-     <proof prover="2"><result status="timeout" time="1.000000" steps="169372"/></proof>
      <transf name="split_vc" proved="true" >
       <goal name="vc_list_reversal_lasso.5.0.0.3.0" expl="postcondition" proved="true">
       <proof prover="1" timelimit="5" memlimit="2000"><result status="valid" time="3.299007" steps="31068"/></proof>
@@ -290,14 +200,8 @@
   <proof prover="2"><result status="valid" time="0.018920" steps="10575"/></proof>
   </goal>
   <goal name="vc_list_reversal_lasso.12" expl="loop invariant" proved="true">
-  <proof prover="0"><result status="timeout" time="1.000000" steps="2685935"/></proof>
-  <proof prover="1"><result status="timeout" time="1.000000" steps="10097"/></proof>
-  <proof prover="2"><result status="timeout" time="1.000000" steps="202665"/></proof>
   <transf name="split_vc" proved="true" >
    <goal name="vc_list_reversal_lasso.12.0" expl="loop invariant" proved="true">
-   <proof prover="0" timelimit="5" memlimit="2000"><result status="timeout" time="5.000000" steps="9836895"/></proof>
-   <proof prover="1" timelimit="5" memlimit="2000"><result status="timeout" time="5.000000" steps="43348"/></proof>
-   <proof prover="2" timelimit="5" memlimit="2000"><result status="timeout" time="5.000000" steps="680508"/></proof>
    <transf name="inline_goal" proved="true" >
     <goal name="vc_list_reversal_lasso.12.0.0" expl="loop invariant" proved="true">
     <transf name="split_all_full" proved="true" >
@@ -318,12 +222,13 @@
    </transf>
    </goal>
    <goal name="vc_list_reversal_lasso.12.1" expl="loop invariant" proved="true">
-   <proof prover="1" timelimit="5" memlimit="2000"><result status="valid" time="3.640039" steps="29914"/></proof>
+   <transf name="remove" proved="true" arg1="zero,one,(-),(&gt;),(&lt;=),(&gt;=),abs,snoc,(++),borrow_logic,get_id,usize&#39;maxInt,usize&#39;minInt,usize&#39;eq,min,max,to_int,in_bounds,memory_0,invariant&#39;3,max&#39;0,invariant&#39;2,invariant&#39;1,invariant&#39;0,index_logic&#39;1,resolve&#39;1,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Abs_le,Abs_pos,Div_mod,Div_bound,Mod_bound,Mod_sign_neg,Div_1,Mod_1,Div_inf,(==)&#39;spec,create&#39;spec&#39;0,empty&#39;def,snoc&#39;spec,snoc&#39;spec&#39;0,snoc&#39;spec&#39;1,([..])&#39;spec,([..])&#39;spec&#39;0,([..])&#39;def,([_..])&#39;def,([.._])&#39;def,(++)&#39;spec,(++)&#39;spec&#39;0,(++)&#39;spec&#39;1,usize&#39;inj,to_int_in_bounds,extensionality,inner_spec,inv&#39;3,shallow_model&#39;0_spec,inv&#39;2,inv&#39;0,Assert18,Assert7,Assert4,H10,H4">
+    <goal name="vc_list_reversal_lasso.12.1.0" expl="loop invariant" proved="true">
+    <proof prover="1" timelimit="0.31527" memlimit="2000"><result status="valid" time="0.316375" steps="5473"/></proof>
+    </goal>
+   </transf>
    </goal>
    <goal name="vc_list_reversal_lasso.12.2" expl="loop invariant" proved="true">
-   <proof prover="0" timelimit="5" memlimit="2000"><result status="timeout" time="5.000000" steps="9817082"/></proof>
-   <proof prover="1" timelimit="5" memlimit="2000"><result status="timeout" time="5.000000" steps="52172"/></proof>
-   <proof prover="2" timelimit="5" memlimit="2000"><result status="timeout" time="5.000000" steps="641962"/></proof>
    <transf name="inline_goal" proved="true" >
     <goal name="vc_list_reversal_lasso.12.2.0" expl="loop invariant" proved="true">
     <transf name="split_all_full" proved="true" >
@@ -334,9 +239,6 @@
      <proof prover="2"><result status="valid" time="0.230872" steps="60151"/></proof>
      </goal>
      <goal name="vc_list_reversal_lasso.12.2.0.2" proved="true">
-     <proof prover="0"><result status="timeout" time="1.000000" steps="2417205"/></proof>
-     <proof prover="1"><result status="timeout" time="1.000000" steps="10762"/></proof>
-     <proof prover="2"><result status="timeout" time="1.000000" steps="214458"/></proof>
      <transf name="split_vc" proved="true" >
       <goal name="vc_list_reversal_lasso.12.2.0.2.0" proved="true">
       <proof prover="1" timelimit="5" memlimit="2000"><result status="valid" time="1.046999" steps="9229"/></proof>
@@ -353,34 +255,53 @@
   </transf>
   </goal>
   <goal name="vc_list_reversal_lasso.13" expl="loop invariant" proved="true">
-  <proof prover="0"><result status="timeout" time="1.000000" steps="2690227"/></proof>
-  <proof prover="1"><result status="timeout" time="1.000000" steps="8793"/></proof>
-  <proof prover="2"><result status="timeout" time="1.000000" steps="211519"/></proof>
   <transf name="split_vc" proved="true" >
    <goal name="vc_list_reversal_lasso.13.0" expl="loop invariant" proved="true">
-   <proof prover="1" timelimit="5" memlimit="2000"><result status="valid" time="1.519904" steps="12367"/></proof>
+   <transf name="inline_goal" proved="true" >
+    <goal name="vc_list_reversal_lasso.13.0.0" expl="loop invariant" proved="true">
+    <transf name="split_all_full" proved="true" >
+     <goal name="vc_list_reversal_lasso.13.0.0.0" proved="true">
+     <proof prover="1"><result status="valid" time="0.046121" steps="683"/></proof>
+     </goal>
+     <goal name="vc_list_reversal_lasso.13.0.0.1" proved="true">
+     <proof prover="3"><result status="valid" time="0.420334" steps="83508"/></proof>
+     </goal>
+     <goal name="vc_list_reversal_lasso.13.0.0.2" proved="true">
+     <proof prover="1"><result status="valid" time="0.069163" steps="1173"/></proof>
+     </goal>
+     <goal name="vc_list_reversal_lasso.13.0.0.3" proved="true">
+     <proof prover="2"><result status="valid" time="0.710538" steps="154593"/></proof>
+     </goal>
+    </transf>
+    </goal>
+   </transf>
    </goal>
    <goal name="vc_list_reversal_lasso.13.1" expl="loop invariant" proved="true">
-   <proof prover="1" timelimit="5" memlimit="2000"><result status="valid" time="1.229106" steps="10855"/></proof>
+   <proof prover="1"><result status="valid" time="0.610102" steps="10855"/></proof>
    </goal>
    <goal name="vc_list_reversal_lasso.13.2" expl="loop invariant" proved="true">
-   <proof prover="1" timelimit="5" memlimit="2000"><result status="valid" time="1.617694" steps="15894"/></proof>
+   <transf name="remove" proved="true" arg1="zero,one,(-),(&gt;),(&lt;=),(&gt;=),abs,(++),borrow_logic,get_id,usize&#39;maxInt,usize&#39;minInt,usize&#39;eq,min,max,to_int,in_bounds,memory_0,invariant&#39;3,max&#39;0,invariant&#39;2,invariant&#39;1,invariant&#39;0,index_logic&#39;2,resolve&#39;1,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Abs_le,Abs_pos,Div_mod,Div_bound,Mod_bound,Div_sign_pos,Div_sign_neg,Mod_sign_pos,Mod_sign_neg,Rounds_toward_zero,Div_1,Mod_1,Div_inf,snoc&#39;spec,snoc&#39;spec&#39;0,([..])&#39;spec,([..])&#39;spec&#39;0,([..])&#39;def,([_..])&#39;def,([.._])&#39;def,(++)&#39;spec,(++)&#39;spec&#39;0,(++)&#39;spec&#39;1,usize&#39;inj,to_int_in_bounds,extensionality,inv&#39;3,shallow_model&#39;0_spec,inv&#39;2,inv&#39;1,inv&#39;0,Assert18,Assert14,Assert12,Assert9,Assert8,Assert7,Assert6,Assert5,Assert4,Assert3,Assert2,Assert1,Assert,Assert16,H6,H4,H15,H11,H3,H2">
+    <goal name="vc_list_reversal_lasso.13.2.0" expl="loop invariant" proved="true">
+    <proof prover="1" timelimit="0.092563"><result status="valid" time="0.091017" steps="1673"/></proof>
+    </goal>
+   </transf>
    </goal>
   </transf>
   </goal>
   <goal name="vc_list_reversal_lasso.14" expl="loop invariant" proved="true">
-  <proof prover="0"><result status="timeout" time="1.000000" steps="2640458"/></proof>
-  <proof prover="1"><result status="timeout" time="1.000000" steps="9517"/></proof>
-  <proof prover="2"><result status="timeout" time="1.000000" steps="248681"/></proof>
   <transf name="split_vc" proved="true" >
    <goal name="vc_list_reversal_lasso.14.0" expl="loop invariant" proved="true">
    <proof prover="1"><result status="valid" time="0.528542" steps="4590"/></proof>
    </goal>
    <goal name="vc_list_reversal_lasso.14.1" expl="loop invariant" proved="true">
-   <proof prover="1" timelimit="5" memlimit="2000"><result status="valid" time="2.082820" steps="17515"/></proof>
+   <proof prover="3"><result status="valid" time="0.510933" steps="77148"/></proof>
    </goal>
    <goal name="vc_list_reversal_lasso.14.2" expl="loop invariant" proved="true">
-   <proof prover="1" timelimit="5" memlimit="2000"><result status="valid" time="1.895103" steps="17720"/></proof>
+   <transf name="remove" proved="true" arg1="zero,one,(-),(&gt;),(&lt;=),(&gt;=),abs,singleton,cons,snoc,(++),borrow_logic,get_id,usize&#39;maxInt,usize&#39;minInt,usize&#39;eq,in_bounds,memory_0,invariant&#39;3,invariant&#39;2,invariant&#39;1,invariant&#39;0,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Abs_le,Abs_pos,Div_mod,Div_bound,Mod_bound,Div_sign_pos,Div_sign_neg,Mod_sign_pos,Mod_sign_neg,Rounds_toward_zero,Div_1,Mod_1,Div_inf,Mod_inf,Div_mult,Mod_mult,(==)&#39;spec,(==)&#39;spec&#39;0,empty&#39;def,set&#39;spec,set&#39;spec&#39;0,set&#39;spec&#39;1,set&#39;def,([&lt;-])&#39;def,singleton&#39;spec,singleton&#39;spec&#39;0,cons&#39;spec,cons&#39;spec&#39;0,cons&#39;spec&#39;1,snoc&#39;spec,snoc&#39;spec&#39;0,snoc&#39;spec&#39;1,([..])&#39;spec,([..])&#39;spec&#39;0,([_..])&#39;def,([.._])&#39;def,(++)&#39;spec,(++)&#39;spec&#39;0,(++)&#39;spec&#39;1,usize&#39;inj,inv&#39;3,inv&#39;1,inv&#39;0,Assert21,Assert17,Assert10,Assert7,Assert3,H13,Assert20,Assert19,Assert18,H5,H3,H14,H12,H11,H10,H4,H2,H1,Assert2,Assert1,Assert">
+    <goal name="vc_list_reversal_lasso.14.2.0" expl="loop invariant" proved="true">
+    <proof prover="1" timelimit="0.187113"><result status="valid" time="0.189428" steps="2659"/></proof>
+    </goal>
+   </transf>
    </goal>
   </transf>
   </goal>
@@ -390,14 +311,6 @@
  </transf>
  </goal>
 </theory>
-<theory name="Core_Option_Option_Type" proved="true">
- <goal name="vc_none" proved="true">
- <proof prover="2"><result status="valid" time="0.006672" steps="27"/></proof>
- </goal>
- <goal name="vc_some" proved="true">
- <proof prover="2"><result status="valid" time="0.004238" steps="27"/></proof>
- </goal>
-</theory>
 <theory name="ListReversalLasso_Impl4_FindPtrInSeq_Impl" proved="true">
  <goal name="vc_find_ptr_in_seq" proved="true">
  <proof prover="2"><result status="valid" time="0.029070" steps="8450"/></proof>
@@ -410,9 +323,6 @@
 </theory>
 <theory name="ListReversalLasso_Impl4_FindLassoAux_Impl" proved="true">
  <goal name="vc_find_lasso_aux" proved="true">
- <proof prover="0"><result status="timeout" time="1.000000" steps="3029666"/></proof>
- <proof prover="1"><result status="timeout" time="1.000000" steps="8072"/></proof>
- <proof prover="2"><result status="timeout" time="1.000000" steps="130948"/></proof>
  <transf name="split_vc" proved="true" >
   <goal name="vc_find_lasso_aux.0" proved="true">
   <proof prover="2"><result status="valid" time="0.032432" steps="10396"/></proof>
diff --git a/creusot/tests/should_succeed/list_reversal_lasso/why3shapes.gz b/creusot/tests/should_succeed/list_reversal_lasso/why3shapes.gz
index a4565a20d7117689494b8544be9b7a2a7477e15f..5d6ad97e77599e69f4c23ade57594bed8af1778d 100644
GIT binary patch
literal 7562
zcmV;59d+U#iwFP!00000|LuKAZzMUg=3T!cZ#7ee0=O@OssV%qgb*;(b$AbPY=LXF
zdX!SOr0lBx_w$h+t8d}1SW;QYgEAxBNi(C-md{AK$N%{8!^=P1=k)U7-|6|~{^{|5
zeNZ2M{GV5^|8n<_|NcQN$<3Af<yZHR9)ExRheO+kho?X8K0U?s@B>{^_xf~q|M==Y
zxj%m(*G->ptJ`{mFX_#iFkiCGXSU><&vYp^pUF~!`L9chZ!!IO_we-leZW<<)VB_@
z-2K}<d`Y;VTO7&KEbZ-zw!JB0-T9|4kMX6y@%4(`>H{tGe{~=4{%`v9^!y(XQ#ZHn
z@#*pL%frLn=hx>(hMTMO>GSJ<?yCNVl|&{fiR>u}+<$cb>G}ETj}(9S^#8`cEh$vY
z-0$i2?mpHpeD&o}JJH+jG}QMe4fmn4YYgn~f3bo6eLb-L*>|6+5#3b{9Bcz(g;bXV
zl|A~T^7e1=4~-Ak`}VoI4YPetFHaBuPCwASL9K0je>RHSfXzSB^L<srYRD>3m+v3l
z0|rpOZi$jTqTl|^)={3vW@ZVzjfP|4w?DGbp~ymZ!Y?V|w{0?Glev`DI2tpM#SG+9
z{RZPxu8=6qkE7Nx?}mQg<qb!;&E5UW-5&{D^V9PuP@m7ZiAnd5kLlSxrazXv)#osU
z0e?WIX<AWIno&}c%8&Ki{+Rk06fc8Z-PXP0G_4N?px%)j3`u>xZo5IMSFUav7-&`l
z8A28vx1()`o11AZRkvNSp@v_eMhK;aAew7prKF0=f4$!J^w7oF^~&`68ti$)?SO3-
zW9gV1U`|&?-YXk;^j;rw!X;mdB9|ETnJp-rA8z<ixM4fthV7s|x`XyeL3{4u{^hmK
z-%EPPh`)_;Uas~v)!hAi{qO4G>FM(aP;k%p?(wxDarcsb-;n9o(sL>(H?29Wl;VC~
z4|sij!!(fAtsYieiP!YTy8rU)$n9&~4txDalt6oAq3(I^AP*0ax(7Ni#F62R4(;l1
zC0@~f|HCZ=)GrUO?!TYEq^td}#c|hW_^>v}UOGD+Z`{KR2yL;@j{a)ws%q`1?&|Z?
z%WHUgjQ6jojIP>pjfS6<=1K-Y?th?HpP$nnsnPJc*Snh>M;qTZx?OfL;b^y7b<9j5
ztwGMqBzv73J8#t6LD&a0TdSr1u7@UNg_zc#$OuS#F5L={tNmFY?Atb36CMM>GYO7Y
zPP2&B@y^Ha^LTWz^v=!u$VN3cHWAyoMxPD*-nlkVB8>E!GF@k3d#D^fIm=U8<TML9
zFa+4h#&uy78_m3>#5}#W`U=9a_HDbKF#Vm}J~rOH_|*v4Tq=zFK*4duT3vSRV>Xg<
zKdnCpIu1FG6#2qFJc#{92fT{{M;f;A;BM1?BB+d7RLbI1Kb6|{db09SPElSKV4AAd
z6x3i2E%V4FRhxAUe9;5TCHw8xk`F4if0)OOWPd4)qL4u|yKm`Rk$!G*pDN>i^(PN3
zHuMSlrscOc&qPlI?9SE!A`>O<=iM-<R1RdzH;-||hBtPwWTc1K=JxFr1o2h@uX`~O
z!X~QV-op8Rx8g{tBS#C*3s%s#vnAOnu=mmZOBk=UPetjV$oqGHYHPo*Qf~{;QDNvN
z*^bPitN9Yq_lrw9I-!Tf=$4U#)UJn?r#h0?4U?7ieAmvHc5WwF*Dr^f^err%Ve#m8
zc>U+ly3(LO9?9b3hE%lpR<l9hLbgL-Wf8P%5(muTpebCfzTtm&-`3|n_#g?npMG*L
z_m96nq}Qj%o{3uP@8yesN&oti9z)vEZrgAw#kR_ScK2v{4sKlnP);%bmzVUsUW=Qo
z+1|N1)M;R*5A%Avc^#sCNk=(st^4LU*7yt-2@KwAkxO|Fi|nlBR*M8LSkW)I*;oJ7
zwb>Qc+bmU|P^KOH(sKvC(eJT+7CX7|?I_QE!=JG>-UZ;NTO03Ro*ox(ba{GQ*xGgC
zI>9%%=yUsZ#`d*Vhepbc?_)pKK!(~K%zQ^G^rG1ETu%KKta>I{y2k^D<!m7FrA@lG
zVEt}I->v8kR&+ZnZVd**!^Qs8U4wl}OFc~KBs&NDhq`rVMZInJb&Y+mOOM?*QqQvc
zS-Sy;g`Rg1at7~?T@Ok%!K&Z9Rz708!&da3x0pJ*8yeXDu=?T2x3DjDRbuJOQ_rIK
z2C}iT9MldhZQRASq<fbW-KQGz_A(c12VmOC6i{Gig`Hhb-JjUVTA2TgG5i?VoN=_<
z_Ass|7WPI(x61!{j97<p>wb?Cmz^z_i>VN-zcmHk&NbWr(^(*79c{AEfepPX-yWaa
zbS&F$9dY)&=D^B*NB9YQCH=w;XnfLyP1*{aW|!5Z-fm8PR=ka0lSP<eV&4^hVTE@#
zTMvqVJ=4h!N8L&Kr$g&sbc|b{K1;4TeRSW=>st=*Qw8P8vU4h6L%&y`1N-~5CrgC(
zb2+neLfgP6<k-F)-0d?Pho8h4d8~u&J=U@A!&YSL)46W*Y_8jRGPju3*%N60w($f2
zaaQm!uzh|E{5-upCj{Wf3$xwppPM!2WQ?P-#k4aKr_Z~W9nfjf%L!$z@r0f@){a_Y
zbrCu+4RqwFN&go54zXh#Z64E(eI8EA^9H&%zZ2rw*t1=?ho9{l=-EBgNNf4lv)x<_
zrd-|#IBG22&UFC01eT_kO<e?9>LEg_&HHlv8U#8RsNOU;H)k5duBmJe4Q%01FUYx&
z9G{v8Jz7Ea5SOjQ?XEpMfcH+w;9{!jTkUzf*w^DWAbXH`$MSW*<*Q=(>VV~|>s|L~
zS-vh0a9_@)H*209J&c>vD$1U98IJDF%CWGqm%%$g%;#TfJ3H1Hn7fPP!=WkuYvAko
z_@z%DXIW9$!;afEg*kZYd}|4BSx1<8*iN?^kDi*->%(?>)?qt+GgBxvM<}%xO3e~V
z-OSt(+uw7)_z{ENBue+US4NIhbqBU`$+ig|L2}mXho+nd=^JqiqVHmmw@cn@qGu9+
zU?P92$0OF0(m97v<HeaqzJ`b$S$m5l+Ju3nY3iVp%QIM99YGXD+3+ZP0Wn>@P)IkJ
zSDjd(VIY0fRNkE7fLOm}3|g_-wPMp}#V0>D)-U1hS?uU594`ANBLBC1s(I4Ug;^Tz
zthmjBKXaZbSkg88IrN^jR=1lAJz=oXQC%aNef(rh?W^@=Hn_g<b_{<02-RL|+(+{j
zkaVBlW0yfG(0{*9%WO<9=<oYh11>az0i4BFIBVJndQceaM`1hDHh?qO@RIWgni^el
zX4@s_VXlMAeIw{*bh(f1F85t#F8k32TcM4KbJ@ir>@rw{^<$Ck>|LKPj-4{Z_b>9l
zZ6)U9lAUQW_Yzt0v`O)_1NciqvBuXfxpe(~7LM3vXfM5e>#+6R4E~e>{is2W9QHi?
zq*L!BQ#}>xSE}1LW1s3eZwon7$)BaPnNZS9mG68jvF*y>5*5LmQMWeg*Y(1TI$=7u
z!D?bMiQSr`Rcp+sF($Jcu0&?2_+0f$yH0uU^~r>~WQHAlwH48K7g@h$$TutfzmH|&
zsV_A-$5S;UqwZOw8(r-sZpLaaS+DjU_;r?cw-c@Q(z6`GIqS<8-ji&IwcqA4MNLlM
z7b(7h^7z7M^4^uNUdSoFa(el;edim*8GlI?jl7HNxTkZ!!dl%|cF1o~mFIh4?2HPS
z`0}{FMj=*LXZhC{@DAT2w)cjgO(v6ma&Gg`GTHgbxz3@L&I#__$KuD#^nePt+logj
zVw~r!I+3{<bs}5WiELJ#$S!p%=nZcjxSR)kN2T9U>37I=N&h{q^_>3YE8nI$w_Xx+
zxd8f2noa$o^zTNq)x+Uq3=;wQIbXKZ3Zrj$?aq{Usj^<;tqsYg8GgAcoAu62yQE_K
zYgx7+GuwV?BwhW2)e%2t#*TThWuJ^o#@4FXpWfcrs<s@csP8xp9eAs#+P+A%elY`Y
z72R*QmUlC@LpmIKjcB)J+b@=;?H2v-(EYWgxAJn><23h%7x(tU-J>mNnw3v_({LNw
zcD%KBlCC~}-1#}`vd#R0iuH5ZDBldV{)mUWM``Ll-u><AF||8T_qm)`pzRJ6?f>iP
zQ(CV3l~<(nFk}rw*6z=S81jZ8Z+GB349oxSzG2znC>oBUO+XBBlnqDO?jScDF|D!G
zoah8|_?LTGJv{LFw#!~M?A1QC+J32qM9_^0y04QyEJlIU8?#wo-MMhTistQ0tCqV=
z>l@$7#rmt{_sxG*(=C~y|IfXRHV=BNek7qy{=O_0w1!evNtUSa@9+EWxSy6tps=Bp
zBIuqdP0x*DH>O&aTUyhz<V&@byVJAeMXIG3m>P7@<>y$oQ?uzXI4zKv<9=cD>&6P3
zZh@4S)P3AtQF4#h&Fh8QS0Tse``^>kV|`zJfdus>M0>63^?{a+O_XnsE5$!<tf2P#
zW#0r%bA9g^&H5*P%+2QAD~JeW^}*INQIsrgQIKtSs#hs#U#8?{t?J<+m){TC`E8(=
z(vR+6Dn_yMI_n`Ny_wR<q?tDnZ{UScznweEju`oRir99(-z1NCdsp5V6|yO>_QOvw
zoQ9G(0VT1q-Hs18(cq76G}uyWCh22;{HrmeH~w+-7lCf`k!Z&#QSYtd-!|lQ<DUXj
zsVC*u-day1mV=G9KmMuW-)7H~H(hXLI0Py*Ff|0~y?(3b0oT4&-UA9?#O^=tUT{A*
z7;_ya*0)+ySF~EDw{@+kn{OtsL$1kFgVVJ`VAE}AkcI!cRg?Y7XR`Y~(*_t`?+v&@
z#my__ikizMz4_D}Hl@&TJu6Dpme$%3n;W`&L*Lxo?nRVJ(bQik{-qQOogSuisGsEi
zl6k4!G3e))lI>B{zituoOZ)6~ZCl#>R(~86UDiKF^C^A0yMMX+BcW}6dj147+%$&~
zw2;G2zts!)iZm@r#=F%U&9C+~<@K)2U9d*&`g<W#HPp#twBI!fwk5m0%Z#v2x?>|w
zQh#k~heB^)Xg6BPvU=5RQSa09f9}>QZGPvuwFA{|G`OL)-*9hpYwr=>mz8G!S+4$b
zd-ZP>{{3@vntJ_%nlHQ8O7*$=P#^flcYLba>jd1@b=JAgZt6qDEkHVDRPAm{#wYcw
zRSfS4!f#quHqLt+28vHjnS{m>cC*biP6Lko_!L&&++MX>d+^R!wvBuJeSpAkt<Aul
zTbroRDn~{&uw!&{yX=g1F0+pxyV0ju=qePf-`KZzvlz(A+l$fu_m|HPi7i*2UwhoS
zFMsaN$B>@(RR8O71XgmmKR2PH8&>~3DVJKG|4FZUw1oSA(zp1*DzZ<Dkc|Mn{9Diu
z)$X66gZ}EZaZ^B|Sk3R4Nt6(_)2>MbD^0!ZFP-$-8=Jy}FPZ2tIchR*dxeoxgi%YT
zPb<vzCH=m$QZljEAk1kWS~xCpUY|Iwua+KqCfiJzY`f&-pm{f7ZKl89&Q5vPZ%nS&
zlk#^rJ{BZz8xMz{-haGbD}rqnqxw6vR(#7fTIZxeLc68H4)Ph0tHz<GplM>sO8Gk#
z5i46%KOszPYMIvU_03gjz}QI1Q;9Xfb|<v4o%J`i-U=-%U5#NOJ|TJx+tm7guQ_#;
zxN2Mi&Fzjmtgma_+RSHdv*&=dnfk2=sy4qD*XO-xxE;Z+)pI(*H8@*xesC<iF5LW^
zK7D@uPjC3;VhUTi<m#<#=SH#G^|$I6&j%w^<<NZIdRsHvVYauE*<QU~T`4Ps@PQK&
z45u-(EU17NTAu`G%74%cwU7(3;0v~(3vxwM^u)3x40k+xVPXz3aLrO?oaTrQcGJP2
zgLj&HN(J#Qlf(>3ktZgY6x=J%G&)eeprB3{lw3s}h09(!Yl6>=2|{U1na3P0mzJZs
zR10br6#ei)E~vOlAWoA`BqbgrH%Wvbv?fWWkf{nE7+o;3ptjx7tC%g7p8D*RvYLd*
zU6w>x>4oO1c4Ym1ZRXr+YDfkVj7_-U2-QlMOrux1_T_`!r6XPjrz2&_1Zk{x-dVy-
zP)SH{YIiY40X!8aN^4J@&x9sNUFOOYE&|4$K5)zeUvReIbiv7j*#$ETrWZ^tnCu~_
ztklGoLAZozb^)3U%CY3B(oCukTrap<a5;&ZBa(8NS@6!|e@RU+4zsRYgkiZ*s0p?Z
zbRo!s+XXjMDJMb<G29pn`w%915A_jINE^mfl~eFH5|1Y8U;|MxGEIe|++^ca6fscv
zimk-OLa2q1^}~D?P6b$|p<X1*q>L<58ZsfmXpyyXmBrCql%bp(#e@wqMay(ZIl!hh
z7c?8Hi-AeDkocD@gk1=896J%ccZdO$I^mU6MrdIzW{1S&ptr(~pOT|XCi|4LN`?rk
z2&c(gs~C||K*geR6sKnD1EPiJFhDD<j!DAZI8wZZp?ls8Q=Xo$jU+oBO6XMJ#l2Q6
zX9Pw?6Um|kYHQk^3}Q^QS!ISGlaq5cQy`t3jgr|!zlw{}ETnGtrLL%wvaA&NL=i+#
z6k(OSkOK{J6&j@-q!1WM+&f7TP*RA_78l~qGQ%(u?+OJ)3k5|6iLgu<(u!8us!X{}
zG~=7I5Dx*xkxE1?6kjMdO2=v+9i;}^Q^*uHATwwdMUo;5Q-`C}LdgSkl$OeI>kXGK
zBtbRL+A2iLOhRHA=}as%Uud?_bT9O3vQQYQStwm*xL;$EXhbw_5pQA$*4k)|0WTh*
z$>>T%H+*5(Y|2i^pdhKCf<+Lc&|wkYd6RgSte>)>3quwfEX+ddg;onK4=^Guk`mgY
z)y$R%06V3~9gHf;nc+o0MlOul8vYddg_6!iCp8bSM+)1I@H?0#K#DOX*VWWy)I73A
zJA}ySn1yhe00YouVH*)K1)-9!a+HB8Oz~Hv=d<u6a4B`<(nI!?7=k}>K*Wqu%gr`f
z9m6GhSsX3spsaBgNhDyJ3CUVRZC19k)-k+*lMq01L@cqcU`ODVtf4YsD63QMNngjX
zb18do0yQ=TACV(-#tfOH9JNttHI~PYQfUr`VA6618e#}MQaZ%mf<-kl3|S>KOU}YQ
z6Hky&;6XgVLY1J7!%z)T(o5lMp0TWOx91r?QUnhc5F!ZXr9y@Uf)JQsPf@Ot8ojMt
zSh2ADTrzkLD6Emwy>no%7$dn@8aEOM*Rm=D5}!Jw48{fp|IJ#_C@CY_az&6r86{Tn
zC`<ifI~55BD9AK(hr*g8bVmm8XyK%QU&`>b%DlFd=YtUdgvNSBm0+-TB&x)aWVmtg
z=&E)kRQ!>C0uD*Uu;P>%6Q}_jbe4fxf`k{P@(lqrB?5n_ya?+jqzlg=P#-bNi_QTD
zqA@5i0wNh(NrFBEoroGHL{pMT2-0hKj*`YXP9nlnX87zAuY@Qn9Ad`_2?flBGRp(y
z2OgmykJ1uw0z>4C%aX)sNd!A7i~?(+_{4R52He6lcL}51G6*v=WG9*C$wSr5QlUe^
z3|{pT23|vQgjwPbgbHdyy+&CnW>L+SL6x$tK)J$>>VDozBaB*!#Gp7s{bD7t!l06o
zSy>uf!&{w&x8q(oA`*->aiarq@OsZIkQ$Xbn1=Tbj-lo6C;<xZ!knUYsrzf;Pp`bO
zfIL<x#t~+Gac~)tIW@@vh*LC@unS0%yn#OpN3#IHB+NSk44kP?&<OLnk%V7B63f9|
zp}q%xAkHBb0JurSp@2}rTxukd7m$Q`2G4a8*%ui=ieTZxz+wP01;*G$5^(`Zq$^QL
zmNe`H3NF+m0l65s86m|rrSt9*#U%GfHIoy{8-yq?5vvJ;FwMv{h63cTz|#&s1BRZ-
z!Dyx+e$p;S2Ek>t9w-@sG;@<f9|)Y!grm9xq@-TJZ*(#oYA;yd$z-ghaS#K}XN5Qw
zIF*)jlqbl=I#7kYj35Rpl_rcqz&CKSm|LVCAb=c@K>-AlQ7DQG!k2BZ(81I{pDnzc
zqO{0{MQ@Ptv|uPgBZHy9I&uY`R24$v9P9-mpU)bALlA&os)<Z6&Zv#_!uTeUgX1Lj
z06tspC(0gFST2auWwn%ZCjeJz1VByFJCif50t)-}1O(h69xjaBE|Al`0G?4o0hAeH
zJPH-G6>{qQ@s)sQi*2ZtT`5P2A(8v!qRQ|kD>zl&CeN$5>fMMdd2}fA2{DQCXsMM(
zN0Ws@`H4EE(XM_s;wDs!!8=7I!aB1I27nS06~9C(O}Y`+yc=<K$rDsXTNd>*6C_HM
z5WvwwWs{oqDhffrnsbq4G9V(duM7m0jnpYx6fZ^#5s?rE1+3C-Rf!w@vW?4C1R_^u
zsYAm#Q0cIsQ{u!>BfJn^0>P)$gy^prBO@vt5(P;%qXNr5L*i^TYWRrYFIl6duNWf<
z3MWQW<XTI@EXrDhbk8{aI+Pu{;uey>8@J%pXUmepw9^zEMX0en3(XiUwRQDkDc+5^
zWp9q5v<fr=#|x7or}EnS6g(p;R&n1?j4Wl2^^_176GH_iLjV9)S>_mkxM>x)SdJ{K
z+wVo{WP>9dxrlq`yvsZpqY@)T%A^35s?_f%vQtk;$~kK#f|CI;-MIws%g*N*b49aM
zqrWO{3L4s+16~FjlgrFTUBahD7FP->l0}pY0kNPFgKx!9=%z3fRj#qG6s@R(8x>!Y
z%qJ98nxpEd)hPoCS?P|wFQE;p2UMsqQDPnQQAz`QB^vt95WcP;D)V-kFJQCAvTQO<
z@FO2+k~tHqkSv6Znx$qDRM~eu1Qcx|BaTV!ctqASiIov0K-P%fHPLDEu7|)a1ISL<
z3R+eRc@kNp@?y>sA+ry42=rYK!5}!>=z;|-0_YYPN_GSw33WBf?FO)E@xC0GNXD#J
z!s!Gdt<_~kUgrYp7?;U3LhJV>G|Q!ew26nZ;+_+yBsm@^b%d~FSD{kv2+gVu=qgA@
z0^Z?l?NwGO*q|ASNNOerYp4~vobmBK14mRI7F`YgEIU^!%hWnaIoD3wQrNRdjZOq1
z%jkd^t6~_@h+!axDc{Nan5UStl2SU<r<f*ZP(39WnvNk_X`8ca)X4WKyodEC>xpLG
zSV^SjKoC;$Saz*Qj*S7(_bI&L!62lT^N#Qil(S4L?gDpATS61t6@IXMwPYpOS|U^U
zH1(+|U)2@d&ZM$(4rWGkl*^K5#BCa+QhHSb+H&YeoYPAzmx#3Gm=r)gz_Iozi_B@=
zQXrz%B355<m7;Re3m3J44@YJdXH2S`fTf8*GeB!JErT~#$!qO2L--5AaU@s?eS1{7
zGMBhhz&8_RuT$WU<FD-Pl?hrj=RF0=BWe(-zycvE7%dfO@I;7)rhH{r&KO}-q<mKR
zlf(3+L+DW~8YPrbK_XCVA<C{{&M34?nrCRqD49l2kw{SfNa1<%Ns^egP%1=LH)?Gi
z9~w`lr?nzVhk(pygj2~T?J;^`&@uy$S9<7=yvdL^C(||MoK`tFN<0Y+;V>KJSO|_e
zmP4v?mV>1A)D~#MIT#E?7gZFNYCcP=V-^Utfo01bz9GZ#7zJ2bbZA(L4V!Y3^{uQT
zvMwb`8Smk!PFSZ6F(j20Xd@e=EGOq+_($;(+((fNj~*&SDx*@^sK7}2gppQjEJyXq
zLA`Qbul)a3UQiY?G%F|cfI=~8N)YXWw3$bw>9Ul;ihG}mUzCBD9Ry-*COnqI+W@`{
zP73@Lldhh2VxBY!?F7sN5l;hWBLrnBQj!t15ci~xk)DQEwoc$CqcLK#1R=<#-Uy;F
z+7N=Ryx3`Y1q1`jyf%n((5AQL_%{-cPYy-2t@eoM%y>D#%}>KK2}hiklm#7A4kpV?
z5ttFIjVVVmD$nw#PRCPPl&%VO0hAd%0tyFImt31{3fSZ8=v;En(c?47E?Jl$0=KAa
z3LY{6!{a(i5>m}1pvCRXFh!8i1>D-9;?@Bu7=j}aXOekJ!Bx8Gi{gg~HcW@{z*yO_
gEgK2M2Vx8@&YGeZRI;jnA*VL`|0#^NiKx*40JT-afB*mh

literal 7478
zcmV-69m(P!iwFP!00000|Lt8_ZzMO8e%G()H}Bdo!24L(3kVGeC17{_u#0+}22YP>
z)lyqh+n#^FADMOKSy`7_ZS+G)RheW&Fc`-dOlIc4egE$HAMR6ne)oHNdcJ#n_>Xt$
z-S_`~^>URyetP-WhkEkr<u`Zt@cVaSNp7y(Pd~f+^ziG;KO9cp-#`BG;p1aW_utVa
zbuW(}?jBy;NB8G<<htq8Z*^Nw@Fl%j6Xr{{`OcPn^PMim<~vzRF#maJ@hhf3Kioh5
zdKYk1E%mK~EFXS%_n#9E=nhA+G)sHCqHS-ASRef3=ZE+_-1vIMZuNy0`aiq(AO1Ui
ze0=&Bh^d=f_we}e@cI7!!>5<0MurK+kXec$EyaN2_s%~)Jw5)B;&&haZ~E7gLaogG
znqEHK#rlJ<e(Y-}2HTy7dV8X99%{PA!2bRh8`$610~?-w_putzhpK_SZ9uG$>T{rS
zK%Z3J{tZ5%@#VU0ldID()u;6Qc>jC)j<yE1w&(V26juS8f260os)p5&RiG~4J-B-e
zp#0ntB`u;~|IF4=UdCn)5_lT{r$X*<WT9h`h3te}QbKOmWTqx_DXVcbW+00h$ff!P
z#;05%QJ9}bt!Lg1{h`Afj&Pd~ch4XGNZ^_upFV>6;f$M@bocO(p4>zFW63*x_EQ+~
z2V|F~6(yw^B_)x3Uw^g7G{m5I8RY7>9u%i(y*B_2j%0608tQf14^o42_0zyevl_?{
zvgouOZ9ClD%xkIo?TQUG`~o#XC@lohToWrLRaE}=ay!sN7h~5e(;I5g@`l?H+bqV?
zGdDn+zKncOHt-lcKIVi=z7$0+G3hf~Aa;1T;bY;3?Svb)gYf7M!XpLYx%<24mpXsX
z={_U=Hp+RvYHO-F`}g|q>i+TZ(>qXbPj~L&r6KX*IsLjJGpwbjRB&!ub66?G{kR_R
z`uK)vAe~bKthN%b=}mS2>F0^l*Ek(o{U?+_2V|k{>Ci#$A0T!2bYzGV!<!u1)!$0I
zqQm}&QwXS^?_b>iK7CGC?VrVQ*JgOXHpoFbI~{M_{WAz{vCxkGYV4|N?WykS)8q3?
zczlR=FQ|>Kx^hj1pOxlH20-q=r&phzQj64N_-ys=C&$Ugw~cO>eM~sntyUcerjX7c
z56dL2&W)Wn>g^%yJ({i6(s0*(ld?ig>u+QNq&<~x1<2L@YzX#ko2&^>f#3rPPFGF`
z5v$`p9K#>RqmQL`PToZ}sky0%*v>WjY~c6Kv5^vCqSu`1x(M5S<?z{Ap3@@dS<s##
zz(zK%3!~U*=9m)m{Ms5S2&dY2?Rv)a_j3Excw6zS5w1B@7!QGh(};Dt?AXV_NXq@N
z{vPNw<Tz2}SN7pi>^C{!T@*Ocu!{$Gn+_8}Wz?Zk7N>@()V9~Nm5*|Y^0ENaRJEp{
z2D5LOM=q(_tZU$h9$7AFw_8g-s?_0Oo;H&9QW!-cgJ!mE>06P0>~NneW4rp3dlnmp
z1U+i`?dX{ph=Bds+CyZf#KXKB29?U5Y<ct;Cv13Q2TMi<h;2^a&Os2z3V1z;i4ZnX
z1rHX^|JjKnrH-5|JYTVbzCBoyodUa!?w`YSt$i*^dqr-a{h_P<p-R0gKu?9CpJaP7
zhrZ@ZL~j?DbaF!Xi_tG5N2y(pEl>3%uNO>K*7Hp}Q`)(mVO>A%YcjO3bb-aA+wt|E
zed|i2{&*sbS2v`h#beC|eGAzhft5wjzDevchrOn7wfcqs?yjrPJMcjgazFgwp6?!h
zy-zQX4+9gm*5C7I|D1mNoE}2j(QempD#fnKe{^?fdI@fQ0#Hsd|L5oQv|fvwt=Yl3
z+1F`gruXwY-n{nFeoaT&Z>?=}oN9aliv$KAw8*8rghlq&a;rsx7p&+foE)nE>e}oI
z>ur{*&nVLlei=9e-x&7TA&Z^e_;!+K+wc!q8}9?~^R0~!FHcX4H@Q4LEo|*NbDiKT
zT=cp9GGqHvt3wmz#<#JbY9M3n_GZ2l75b{!@={KH3|766EdA|)<8n5T__a-XuweaW
zMc=IG2rIfhC~l1g!~Mnn+^Ys{N=rRX=`2?c+8eobZ$-Up_jQfE)n&l$8>tVn`-83q
z>=*j5jgSZM?%DOIR5Psl=(X|*+a0%}w|t4Ir@OI%wTCqfPriohQdcFGK0gjDif<qr
zE6YLMz|zHCY)g7@InjNrA+MFWST_LEUZ#Kodn@ehdhYd!jjV<Fj~K)EfgLiAZrcII
zb;m+$RCKHSAE$`*7<bMOC~?`l<nn4N1naL&fwza6?SJ(a2w6{?Ec9T*pvt$~=QbV7
zWw)L<Ew9<La^Dkv#<h}R;YKt*Yr<w-3Y=$`)ufI$ry(oe#;@5T9AIMK6#mKz?_F%&
zEB^I?PPRYl&eA^}TmPa{+=ld7a@F~x`)*#}a(J66D0h}!QUM$Kg97cjzE20TMCjg^
zb5Ks`8u*MHJ9Gtid(X!HJ2571>tL<hI@W#Iifp|j*KO{{bvt+C7PGo|0v*0=JOe;n
z6g-SvK0gJ1o?o6b0`Sv?*<R~EG;17^F;2=B^Y%oXKkvTofX<6v&M0e*C-ls*cG427
zi_np2pc7k7hA*M-5Ie=u4rAK0&;3dHuz|MbcSby$y0`0g|Gix!J^Py)X)WIdE;kp0
zDTg-#P8v(Ua~;4gfu$K_Qx}1jdW_KO;(ghE4FWw3R8N|ln+uI$*Hku}2DWf$5ahg)
z93Pt-Jvu>kAD6Af-L3;XfcMVG;MG(!wAypL*w@oGAP10n&+_%K<*Q=(YLDfs>s|Ng
zSiUYdaKD~QZ`M3}dYCq+Rg}HxG8}Eq%Biq%kii>3%$HwkyExVvnY&lVhhtOx*TC0@
z<Ch_QTx3O|g&ntR3WwmS%dI6GvyO1!W;@+!Jh^L5uQ%K2gErggn*)VXhX|$CLaBp<
zQa1-)5o=#_fAuW}gGrROFRx5&sp=1G<&s?!Jb~mvj~|+|A7p669f-b*L5`Pv&_pjJ
z{>ViBP`5{{C#AO!p~i~~jeHFed$JA|Nwf(AOViXrXP0NRxH^F-in8%h4gzAjdZ3VQ
zFt0kZK;uCAq^Z2Qzy`5l%NVs{vunj>$coRtZERS=+l$!I7ua0(RYd-;c~|qStqTWf
zczTuZayvFx;?(7sgLisNjc~P;%SKE2<Kgb*gF$y$uMM1=N4@rLm1D012%!IAotD{{
zUpwCo72dBjf)Pl=R*+`i2nGNT8wNZ((>9XQ+4$=21aO&L-DTU=-Epp?D{B)#Vsd4T
z?XIl7&Rh;BcD73FGv~6O_Sx&CeKwr-x3hPBxj1&t5I?-0e%zwR*(JNsy6J0V#q%b`
z^A6xIh<et(_L{52-)7;275(li*VhhP-^}388PHD})Wp8Z{Wld2-ktOpD+UjmoVQUg
z&%L|*65ER>Mt$Z{p7+AvS!Dy@{5mmFMe5%W(N~a*U-?@5oAT9Ha*8h;Ex&Hx`3lqK
zUs6RA&)7KauA47V7<^%e{0dchxsBi#RKU!K!kk%EU&#AwDagOXfOq)5k+sCRjz8y~
zwAa()H*E6_+k8vhuj#+%wVw0en)`K{bLSS~*9)LurP<WiXnr%AtseHTyw8Mnm%J6b
z6Go4?DSOV7w%8!?&ei<#`r)xhZ?S`(sAQK^Y~Q6|%VuWVeWVawz2D%3S6#4E9(yz-
z<C3wpD%#UK_|UD60~Ph1rlCF0oKoAzOw}J|<e5|Lc58VzW80_0v4>3cTXy|oX}WGP
z{DifiJ9;aR4m(YAM?BVT5bmCALG!G9)^q5((6;BTgOhai{{7C&3d<If=OuBU%AS+W
zQ0pU}-QAMhxc49a_V|#x9jN<MHv7<S2a5Lp^Y}3>*Zs;3v;z!T!;p3RvoVIeVaU53
z_zuJJ-`zDVdmKf>QFIB2F^;m~D7zixh9jmmmW@E@1atV!J+Jn=eY)+lR}FjBrdHc8
z)tCsn5kU`i()-0Ika}Y_>!Ujd?pD#fduY{imuY<-NI6*FS$Ws|tD5e}4E=u^Y_!>%
zxO#+cm;7DXYS9@A44*9NlHJ`6opC=bkw9TXD@D+jC{53eVmGE*9!%1io+V$Z@(SGT
z^elOiYAHsh1|4*HSod~nHXTN%1rl?dFKm9^SYgvG)ECaa-+dN}d$?|HKJOld9G~uf
zO^*-tX{H4d)LYbBt?KcSmW@r6Uk@wAKWwa^_WG%9f~Gm%+L89W-HNu}NBCS`3Eh0L
zb*msHOIs9VyPfJ$O1g(Bxml}ve8}bL@;gtCe=hxK`%p28orfKcDd}iRXOrfzi8z8+
zd3F0{?kGE9<m)M7+xb399&vnE-WV0KDX;d!&oG>Zk~jk;v9aBr4>!@^kA5`RQfnsZ
z{c!xNF=H_Par75~Zu61o#wbzGt>WJ{<n-g80#d1)PS@UAxAK<#zIHhNsp8+J<;j~a
zI5Hjr6&jct0(Gn3Y76_?x5`tZ0F2n(``rWX#|C4r!^HYjXX=Vp%k*}R6?OB?<n_ok
zd1`dJb_i^`jSaH!U$<(qU-{m8iFpGIuUiAIP;v9Xk)q~uNN>J1d$1`qTsK-%wWYN-
z#O8$VpU^iqx2=d$DVqBJx}Qp+(CcAJhx$$4wAM~a?T$e|J(p~cqW)!zke|DELe#dU
z%`f%UQRuRMRQceG=u2}LK?gbP^jkfiW%YvWT}h_9t=_a<#?zG7yE6B|8nv5ud4ovR
zP%n?sVb>_wmhAQ}Gs1f5j!ig8eHXzFg~7nkZM2eQ{hs2@+pQawHg5qOeFb*YX!KER
z?S`$#vbF9yd0uJupXKO3w@3e0;om<uHyx~BxAeSwtW=+?FSHsuWB69J*9*9-<E(d_
z-PHSFI)HS}sJh*jjL+&<s~FxBgx_?mY?}8r3>2T5GYO3&>}H#JoJJh^;W4bdxw~q$
z_TZhdY#R^y`v`$wI(L8UoZ3W%PB}8EfgPhew9C$D4`ufLeLwmX3tfeR_48a>CyRls
zyuBFh|9<{-pV)Hc`L)Lf_xaD=`54nvOZ7jWMqnj}`*RaI`eF6YvvR5R`JeP^Kub9P
zCq2dwR*`*Pglq&D<lljQsCNGhJ@i+PO`8G|#cF=1OrnIaopwzkSZV6Hy>v2YZ)^?|
zzGR}u<fO^G9TY~+5k@VUKCdv>uj%)_m6DmgMqy6(PO{S?=k=N6`fBN6V6x4e$+k;Q
z_L_GC)(-Ud+k;cy^^wW-dRG4K$H#)?ZR6qa)4TU~YelflV$^Vl&Wdk2M(dn3NNBfI
z*g-xca@9E06f{jNSt);~B4Xtd)ei_0n_8xGdVO+L8Zb6d@>F6?u-yr5Y-jzAtuKX^
zm9ECH5T6h|#%*eSe$bqHN?bKAf#!C{9oEM+PHpD1wrM$FZKi%Hf~w8iM25T<4YwoM
zwR%oxxCUoS&i9UG*M*zE>EoxDe+`CTF6OY6ORkP(duSA^U4N;L@w7KWRSwPft+zF!
z9cOzxo9)$AN}fedSd1b@E;R9hdPOoNQRpnlJGvlONz)LLk4njC42y~A#F_V&3G0(>
z8o5La4VgG8g49&-pp}(|Q7@E}L^hNhi76UtxymAE?g(Q-QXdoiJ{Vmac`9j8$x-2@
z$VnK>iC_+7Y!o108-+xe#BsvB$uwq4tzjOdk|C5c)3EbWGHG*^NvPnWuufB+DTj>7
z7*`u{Zb&8(k|{-V)Dl0H=Y&SdS@aD%Die4|XO-1~g=q0zTImVVloFOpqlI3mg<OaQ
zU$84>g%Cb)LW1Ftk7Ypx1_^};&Xh+7)9PRoC)`S!4W-FRpCnJ5XBiXA+G^k8V9|l5
z=!s>}4|hC!VPXz3aLrO?90NfI+U}uqbiyPnZITepac79;$z$qm5UCji<qOIdlpfgH
zJIy_%f_RrnVuqy16BA4d?v-a{W~taVH#BQyl!N#(BrYt|nMWQ}<Tj?P8{&3B&4TI$
zRSPPQ>Jv4lEqj=b2|mNv2&HJtV~&<f%h5;bZl{Dn(4-SdiNh;Q5+Mk!Ns=jKs=_<Q
z7K|=fkDFI9TPi*E*(q2G36Z-jiGZaD%~kElhx^*hxz)57Uxd37;esPnD^bkbt6ckv
z(eBa_FN4#OvSflZRy*%3VFsQgq&Ky@oT31piW8-^r_N^rBcv{K<p~!7V^8n6TyWSb
zUvReIbiv7j!K%!H=><~*1mXUg*fI#0V5=@blc7wXr%E%a-f^?wdcoB!YK}<wZDzqc
zkN=XIU=R!txFg)jg+fj6g<uOo7lJIfol7|pVu<0!Sl9<F-g~Hzh(g*hrmCDm97#Ny
zsDlke#mEp973C%yrx0!fMTD@GI2=?jgsNW-XW>+UWf}z9WSNwaMOp$e5k`xw5#<Vt
zles8E5h)cyen2dQ?}d~DY+7?sVwNrjCiz0*FMNtDgguR&h~7H{GD@BBN-86?uokm}
z4C0`-!cLr%qe~|Hl(Rwx5mXUQlebneBBg+eMdc{Z&C~}(3y&0J5NLHw67I%<7c~ss
z^JbXp{CtT~nh1%&!kG1%d8HJ7XQ33*P9j6G^q4+2lI(aWsX$>&+-t>hMgUeckt|A9
zv$hxL5zC^@Dl-JLoSd_n0-on=l*}gjRs5B9Ax*b0b!EyZ%SwSy6hQ<9^dh(mInW?i
zAy|=73W1Tty^|DyD+Q$d;;P(PW*A1|U7?^@p`hp}5ta!nU_xc9fH!QS8NZx`cnDmM
zR3dVr#6s~&I>`LdQEH$)g^XkaGLU9bBtRo!>TnctyxK!YX{j8y-f-zc5>#`53Wcbg
zNhkp0ot6tN7Md?KYlV1C7aAkA3uTHW4QosijmXI@;#v&BS{tn~;Kd^}8C}U7Ml1|J
zn6g8rSCG_D0f?Faq_iu-J8u%O5gVp#*unr_frVXYpe()6Y7ZkIU{XS8w3^uxX<(-m
zIf_vQ6li$Sk5LOFw+=Q(exal*NKpf&zz$&h5&jLc1Ozmu<kXr1jXsR5(GH<FI%Xjp
zAUA+3V7Lttu?r!YuX3S<Dr|`h#vIPVlfb3akpuiGl@ddeAr566V}S2wn-ovs61^;r
z7IaY7IE!QzFwKNytqa(e-RyV@FW@l*kc?6xSyzxb@KM%K8L*nwz_a}{c?vt1viBxX
zV^i=Exj1LckV(o>8<kd5`SK){qK+b%w48yu7y^%!D4jyVyc(H|tP-cC7vY|XC&*jy
zARb_$N>ImPsD>zsV$RomW_jUmFEf0k2p%k;N)RXqk)J4#iogVW%BUkXdRw)y;36(1
zgXe(U8rZ=*2lhypBo|BLMgmD&R%I{?t1l=61#64iLqHj@_~0_C>V!m{N>b8sC|MuV
z$Jn3{Cs3K8UZ#v_l=cLvno(jEkEQIVh|ry093UrC)c;Hcjua6Yz_3Ly0Gw2Yr&Wfh
zq{lB9AP{D(S5yfGw?alt4B3nuhtN^y7X>*!bcBLKx-zV|e}<`O02G~NV3r`YMyY&5
z0Zoa-2ci=`LP-~{L7?PgmY3-T@`%QuW(o+JY$Xf&5OgAXf)Y)stb$0d;iXC%=QxQ7
zg_+^IPrOp1=!%MdnvzfelBgX$N|(SRl;lyD1G`|9oN-w)CM{WKCto7D;!_IrQqbFC
zQv;MyL>dG&8M2eCECfK`%u=C4K`34gQU(e|Dh7XiK&Vhg6-rTtQdZUiz_^T~0Mx>c
zni1woBWhcTJft{7S!N}%!k|EtSy>uf!(3m6x#M0qA`*-?aZ}zlj40!o1u~>k2h%X$
z!A-P&PLiN7FWf1bmxYtEazfdaHx?Mn3dK0$nlBLrfE)>w<N$~(8d3Obh?2aaRtZP5
z0Hh_%I|9_5sZY=e^SKd4yoM;2lTwXn4ah>AL-qkyln6-yQH8nGh@xIY6y_N`*hyr3
zWStU9;mg2(08a%v*+vxk8lp&7;*%`7-w9NcD1rh20Kht8i)+>ecGq9#g#px1IiaXR
zu<{a-n;;_7j0|TeN{ba_+d+jCKMrJJG*gInNxK{wM3>QefO7=Z%uNnM*z*W3991Qt
zEcF8Jqm$uKd#N#;OvYLoN3rJ-yb!Shr_yqcx(FaZ2dV%F5YAw$(u67Oc?>&?2`)?Z
zNZSE96%aHTg>uXwkl6->?FAi2@I~aIsA{rd(HmqyEg0(G$Y3onkz6q^RfUSY2!DYf
z=(7e05d?snY9bR%G-@NgFuqCcawdO(t}Xj>r4lME7sTnZB+R)Jz{)fN9Vh9X$(c41
zk}oJBAQ16zW#oE+9Pb4njuHw`%@E`3vOk3!GpA6jB)nXdL#ggcHB1bN+$R@RhDTY!
zsq!{?UggzqM_$RJ^U)Gw66MiSD~*mOm#bSEbyA~W^LFG-C|84bib_OyW*KY%HLO!g
zBC#gj$ZOw@yt<?es-i8IFESG(N)#8eT!zdhH7jORvM=aiWuZgEHc@@Bpi|<+phWUQ
zcnL(EQWGV=XbeEnL82hZW|T$QXNa7wMhPDgd?jmiICIi3A|XL7!)S_JYe|?zxrwOi
z8HZnma>cP&B_w+@R>`T)mL-LmFNHOQuUnplW{j4iw|bEjZ%5v86_BCW2{Zy$3zH$J
z^4j|pJR_=JT$XPrs+PLLdbDscG1Npd1fWrsWsU*(msWX;<;b$Y{bs~YHaNnO54d;E
zyUdd@DltN&ObU>tiv5O?0riBWoU>LUI2jODol9`R?0k+fS71qtf>m);^w%?%8IJ&Z
z!N%k=vr(5YYLQEoLY`s~;5{HBG$GV%<xm)h!Z;Mhq2{f)T_EsddTm6Jgy@RQDJ%*n
zM-XcPk%637f#1F{sfjF?`%viX1Szf6WxY-3k{lREt<=mpd1F#%m4XeLkqDbb(P#~|
zLYMsl-e&}gDs|zc(cF-WS!$-%Nz_H!Nn7wUi`3{uST;rn=(EwDZsgDysm4e(e<NCq
zIV&lp0|<03J0k@APA45hw9+;^VW>85RC*8VOx6?4ys?r<%@HCb0C-t5COJ0J+czqG
za%Ja{LFon1t+@<D@{FR92C0-@fiMG#hF#QxE&M2#fJKaA%y1S2AdEDqVnYdGb${Hv
zMqDD?m7Ntx&d6~Z<)p}*)}=ZkDyT5>imMcrL&fe;xWiQ=vx+k&RZd8WMAT*w&_F_?
zu9DZ<X$B_>!ttD=ME3GPtTLB{^pZmnz%VKd)}kwPL7|MzRx|;eLk;Riu;7#gqoo23
zo(R!UdfB1?xP}k3VKI@mT+QI)^rS<CQ7jr%%|-=@V5x;DYx1b?;WU+Ak;lxVr${7#
zF;aM*e3B$)EtCq8)k`6^j<3$zOnO=?qI4+JVuVx4ChakLVHlzkl4_;L@nQJT`E*U$
za#8l05l;ehWhbL@ECk0K%OO=cDFICw8iCOhjgKmDj1h^CIGm-`F$)CLz_R72sv;$2
z$DRO7i!n4T*@g|J$Fqvae3U3<yr;>yvXj&hLsD7KF|ryZY7l(*X?#$;M3D@S9x6n}
zLRDa+0wd`YM(QgcXb!*(h`jlKEH5Z4xyZ_9o0K9ZO$nl1kT&xeD9x3ZIUm0$11}45
z#Mn%DESpv%P$ircASkA~N7Tym@}x;<Ctw~3o;ss^mE{6wN-{cPxhHju_B_0@bpjn3
zjS-V2P>cW<8$lFC8$z%(5|Q)p3J3<4d2JBopiOVfj!`5OpB#{|t@c=UdX@{RWxMA&
zcqZWx&n0C+$CQIXbwv@F5v+|Vmpm&^&@P)y&&5+(<B3Arf-<8=K;gj4l53Mq!E}5T
zomtuCcJlZPvP%{wh`_DLx_}-NFg&iKBq7!D!8XgLx`V<LaZC%iwbRJlfh1?j7Ik1~
z6nrU^ZRm`bZE58{8K=W|V60pPDNAz12Vx8@&YGeZRI<87d|spf2j|!Q{6xk80FJ(9
AJOBUy