From a385c0a71176a49811bb584dc2af3fd89f4c9cce 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       | 173 +++++-------------
 .../list_reversal_lasso/why3shapes.gz         | Bin 7478 -> 7641 bytes
 2 files changed, 46 insertions(+), 127 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..199ca0ae8c 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,19 +200,17 @@
   <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" >
      <goal name="vc_list_reversal_lasso.12.0.0.0" proved="true">
-     <proof prover="1"><result status="valid" time="0.781007" steps="8157"/></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,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,index_logic&#39;1,nonnull_ptr&#39;0,resolve&#39;1,resolve&#39;0,mid,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,Rounds_toward_zero,create&#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;def,(++)&#39;spec,(++)&#39;spec&#39;0,(++)&#39;spec&#39;1,usize&#39;inj,to_int_in_bounds,extensionality,inner_spec,inv&#39;3,inv&#39;2,inv&#39;1,inv&#39;0,Assert19,Assert13,Assert11,Assert10,Assert9,Assert7,Assert6,Assert5,Assert4,Assert3,Assert2,Assert1,Assert,Assert17,H2,H10,H8,H7,H6,Abs_le2,Abs_le1,Div_bound,Mod_bound1,shallow_model&#39;0_spec1,shallow_model&#39;0_spec,Assert14">
+      <goal name="vc_list_reversal_lasso.12.0.0.0.0" proved="true">
+      <proof prover="1" timelimit="0.02816"><result status="valid" time="0.028186" steps="443"/></proof>
+      </goal>
+     </transf>
      </goal>
      <goal name="vc_list_reversal_lasso.12.0.0.1" proved="true">
      <proof prover="2"><result status="valid" time="0.129765" steps="35671"/></proof>
@@ -318,12 +226,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 +243,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 +259,58 @@
   </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>
+   <transf name="remove" proved="true" arg1="zero,one,(-),(&gt;),(&lt;=),(&gt;=),(++),get_id,usize&#39;maxInt,usize&#39;minInt,usize&#39;eq,invariant&#39;3,max&#39;0,invariant&#39;2,invariant&#39;1,invariant&#39;0,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,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;0,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,inner_spec,inv&#39;3,shallow_model&#39;0_spec,inv&#39;2,inv&#39;1,inv&#39;0,Assert12,Assert7,Assert15">
+    <goal name="vc_list_reversal_lasso.13.1.0" expl="loop invariant" proved="true">
+    <proof prover="1" timelimit="0.266202"><result status="valid" time="0.261099" steps="4672"/></proof>
+    </goal>
+   </transf>
    </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 +320,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 +332,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..87af96d21afc177cd4dfcd7e322134056d2abf65 100644
GIT binary patch
literal 7641
zcmV;~9VX%*iwFP!00000|Lt8#Zyd*xzVlb;<{29Xa$g4a0E7Ud3C!4s8T9cHx%%-9
zMam>)%m049%<8qau3kkMI#BAa%8ZDNjOB~Wtm=RJ{@u$z-N*Fu?vM2Ra{u)BAMez=
z@BjVk^>=sw_{Vo*PHwK;Pd~ed^!VHBKONdWJUsn*_u(m~hwtc|y4R<>`^Q)J!F~RY
zTsM8Xt#0cLKBqTJ!hFtFpV^$RKGV5aeI|1W=0DFZzQy$U?&0aT`+%!zu5TS=x%<OC
zd`h^WTO7&U%<b)hw!JB0-T9|akMX6y@%4h;;sY)8e|GQh{yTkmdj1Q<)XlAXe0qHR
z^zd-^@%6cp;pQrR`1tzQUDe;PlE@?_ku4>G`}fX2JwHGFnc{aJ{%`!-oI=IS{gz(u
z?qmJJ7hiU@6TR(DLw$SFa33nW#=!pZHyhYLmILdbefOan(OuQR&Nd)cNOd_-*`rS?
zZ-0S*XneTdw$H_FnC)|Vd3yLGeMh$jwY2T+*(h!UHvde|_f-vxA*(=LzJGKN7(n^D
zCQ7!5e*H6BM|mEb*-PMcG#m@R{gH(ZMHaFVen|<xZIc<B%(<+_(U^fOW+3P4R~Vmi
zg+yU~9JP*lH}v~1uQ<YO?(Sdi{!HMSpPoN}`u>cYm~{X6n4aBZ`g6`(eRfkA@CRg?
zrWGZn86_pDd|$t9kExGA@iNHOZQUzQ(|TtB>K)0>kkr@fwi~2+<?5z^fo3(3A!N~U
zJ6d<RxtZ2db=wsiYWM|egiu-tqPZqkN~);*{q?q|hc3ph7pB+OV9OhB2W+z#OUK**
zbGkC}UfIB-_xg|%&iPyvxx}c?tU=lS;f4=|8@3T{*aq688)%OdwC5h~Uta6{y`+bX
z_}eJw<!W0~&E0?0|E?aMo<6<<1^0aK9$y<0cQ5I;6`6i5J*R?l(~`qNDelMRfS1=-
zOap1%>S48(cu8-p`%gcQ+`h)`u+@J=3A9HR>Yn!<<n94d_do}RI5ND^p<Vq_;uY=p
zKion<{q*qa{`dJ)y4wC)9CvAk4@-mWrL)oT#yz}%&>9PE=&#1Es@9I`u0B4!yoRU8
zc>jvZ=&CK(X!u!Zu4Dk@{s(&X@i}dg8V#RYy}QYAwDE1D+j$ogj&`e6$DS#qHOT!k
z$yVpa&Kvc15cUqu)@rH0>#j*zAg1LfG6K?`OSb~#YJb)T`_@gCgvUVeo&?7$r@e^P
z@$Qe|_v6vU(i=DLBOBG+*hH-78huvqd*j+bi7?V@%5<HD?XGh8<Sb8Vk<%<_#}Hs6
zE7yfltTb~-iFtZ$^%aC;?b~)eVfs6{eQdm2@v9N8xl|bUfr8_RwYqHB$KFWF{jmHT
z=s4s!QsfK!@F4aZ9q=X!9BJ6bgPTqJiJ&rSQ7Ma4{Zwk(>&ePTIYoI{fN82)Q&5B1
zwag>uRIS!E@I?<Smu$CNN<OI6{$U<BlI^81ib4j>?6#$^Mf$PDeX5Mx)t}t4*w82F
zLCbFk&qPlI?9SE>A`>O<=iM-<RCZ*`gU2{x!z(+OGtxtBb^CS-f;d#b>t0NRu!$<T
zw{ZT?RvamH<Y?h}!3z3zZ%H-^>}_=a62@!oQ&HL}^7h>y+S>1{)Y}4dR2aHRwj*=s
zYQ9AD?c$P-PUvnix@F`bwd<kfsgC4z!(?GS-?THPo!bf4_0z5<eG5xxSUkENUjNy(
zt~BV6N3yuMAr&niYBuOw$aV-UEP{4TVuv~GG=;0hH~jDJ+xol*A0#37!w>G|{_(em
z^!oJJGf_+Zy?pX7>Gx0RF{BOcwhgCJY^(f7caNs$;MOGo<rMROc}dU9wYbTe?VX!l
zod#xlH?PCZYZvWHI?8Tq-8RRu#%HidVDMgxoXc}qWM?h6S|oVEihjb)zWT4O%`ULs
zYN`5!GHu|Oo;&c3evj?5*vXA=M|o}={vK=NT>yT%wekMt>2dK!m#4>ttz9Rs6MTh>
zKDS?HY+q`1Xr$cuHuhr;WT@TF%y*<hFN!VC<<y5@)icS`JsvnLX9I~ZZPL93>o+U<
zW<>{B(d}MwYcLq@F7~JH8f;UV>tRYK**Vxg)U7)!>TSEPYwTNHdhEWDdM~@*Yd2uG
z(EA;P+=F+=t_P)>VATh&m5<o&uob=KEvAm{h6c7htbTa%HS9}Wm00@n)UznQf^4iT
z2ekuB8+Wla>E7i;_o0Tot<1&R0ho3&1r*p>VQ1G<_a|1e7Un-<4BrQ~&p6s`dl=Uf
z3tOY2YvunqMy$iQb-zc6^Ujvb#Z(B^Uz-AN_ch!9>MRhljy757z=mFxuaD2II+ks>
zjyPLhvt#AHBm9KDl78U^G(Ks<CT#^yv&(8yhnrKM6|dvhWD)i-v2O~$u);f=tvkiP
z-qXo;N8L&Kr$g&sbc|b{K1;4TeRSW<>uU~gQw8P8vU4h6MZZ^|9sB#VCrgC(b2)qE
zgtmcC$gzDpxa(&&c0Y+R@>mDkdaPsFhb_p~r*qxv*<82rWNtC5vnSC0ZQ}_5;;i6d
zVEg<S_<4GHP6)t{7iPWJzi-yqCu1CyEvB7`IDOu|?0`;-UQQ@$jVJWPv3ArFtBcTq
zX`mxVP5QUcH;5hMX!|kk*yrw~yx%~#=66Co8+*3vcK5Sg13kNk8fh)xdbXR3!IaA@
z0Y{Cc+qn*4lfc~cvZ;$eb3H_8v3XyPUxPpg1J#@6=H^Ue*ff>Zp@B6V>IFF$lH)`3
zphqjH?&7kRxZSmf2k_nr8C*;?eXBi(i+w$A1F{F1cPwA`TfQomuXb3zy54k;mgVd6
z0QcowdbQ@+(ZjeoEu!pMm*MEvtQ-p)dl|d|#C-mxwzFfMfw{XlJ{+3jzX!hFAHVeJ
z<18x*Ti9{Ermzp5I^SBtA?pZx9=6l1#-pd^^zyKs-s`ZPzL^5r4}-D;HS$>@`(8T|
z+gtT}oJ^oSClh)f;2rJNn|tZ@uFS|utnR=Tp4_(FBS`LPv1%WSRZELids(cS@WQr}
zA0qiGrs~8ee)>k-D#A8V=HZgpAawG>Q~lx(Oym#s0L*eyIwwtPC_2-~mqkEF*4{Fh
zHi3R_no9TN@(h;GM-WBXJv_?Zl7}u{8Ks-5Mx9uo;Zo_Ssk}ME5x{=S7_?%uX~m|`
zicfwpuwTO4v)IuWI6nAQME<Y&-1?-$DSK(S0}A)TF#9|;GN(%nv+GTIt!{19eZGUj
zYY@-&KVUSb_QehY8(cv;yvjO%glexQZ`W%TkaVBW>_Nk4k<H!r>$J?q^d+17zV)69
zjbH$0u?5bWHi8}$#`;m%#<UIK3^u%}FoLE=Hx<}=Q(>6v;DYW5x*1*2Wt$7Smzm3c
zw80i=W8z$Pu?V{i7GeEZWIcP==Zj;f4DtQjIEO8voLsUqE!STnE1otfo^}9#ODNX(
z+9fw9zRkiB8%ga|(ytx1zL~+FGN2zdsFCBmyPsw2eJHMX8TpIU?W?g*b)CaP&Q$Ve
zDQzZ{G*jg}-%4z|GPp!Vu+OMlM=_T5!X9<PbZ&#y#AFhiHAkz~*rUdn%x<_6*+a$W
zs#n@|%3H5bCe$T+*ufWD5q)!!^=pQFd!_#i?d6hDXKgoLu7mFQWtw)kORa-m;9;(j
zsW?%=P0w=7>a4HVcuTS&)_$GK6g4@0Tcr33%Hs>4x_nc<dLgIy!jb&z_MHpijBhI1
zp`wwutsVFL^%q#H`@#<S6{_-lj|84k0TW*j`1dHp>gp{25(D1gd&KtM@YCmH(vJ$R
z9!n=1KPpIj)&@r_NapsaAlb5lWP4SR><d+pQ{KgJIji}G<h~)fZ!qPO{(D;MIsGeX
zzD{#)y*lS|0raahoBH$d-;8FhhuvHM6G7}bUqRFgqX)c<Xv!OASugR{Cf?i(zjBuC
z^(Ij}r(*pZVzwYN+kTZMUHq=s5kK+9j(Oc@pNw<Hma5pE-rkqZwj8La?>G(Zc-N|0
zzh1R|F$3>f-EOy(cQv+MIvjerYPV(EFXpE07X5D){<)>M^2*%fG<U%3jC<kk(H1n#
z$|t>lxeaYQ-r74!SMT3%{784%ntef)_pxj)uZCKG+Qi+XoOAE*etCLK?GDs^EPMR4
z-GQS0|2%z2^JTyC;+P(WtYOI7{n-#h-Z13t4t#@Q`QP0)EIS-U!%?&eh#`)$;V9c3
z<ccGvHI|waonQ{XyO+g*`;WI>_Nrm8wyD+jb2TJ_ZbZ<1o%C)o3Z!0{&GPETh5JP`
zZ(mxp++<qcgI6xr-)g^a{;Qg9$qfB}>}|AqIAZbB5pDAKWwD?&l(MogM}>cX-*?CT
zFh>G~4J{Nww?t`rt`xg6)v`p<nw~kItGV2qo;fd4&Begfpo1<yQnQ|#RfoZ8fy5m5
z3!9%;R@ih4q`bQC{pKo+d%SL5y41c3IX>S1mYyE#Tl@<osIO+)YE`cfv}|mme0y9d
z{&8gmwbxJECTN=LTSrfpKYV0vR&S(1L?DX~ww@!RWNwRsY`asvN=f@NB{xe|4-dKg
zs?x?UCcTt?bo){<ij9|i4=L$jN+*+Mzlk`27ef7d?kGEA<jW~y>-j!N9&vbA-WV0K
zDX;d!PcWQ@k~je+v9jHc4>!@^&u%nWQ)?#aeSiF`F{3yBar75~uJe&-$0$+nE#lug
z<aFbo0#d1`%a-0+Pw<t)fVMyWsp8*e%ad1KaAi0IDl{-P1nRARi)ZMTzE$3i3Sh+U
z-)~-UKQ<V1877vuT2oiFTBf&kt*D!?Ca*)T$y0;VwLxIjZD^2%|FTt+{mN&u`IgrP
z7+!A;xI)F%i}s3|%O$<~)Ev;H&~QCpN!6Ox(h!>)x_d+4+}v(OluFUm-);V>6bhXl
zrgW&E<o1$zsogQ?=a-W0QPjV#5%Np>ymD<@+WcC7G8J8xKhg6ceYm@Sx%)GrZGL+G
z05se*hY_@p!$!ZwYYB@qElI|^)f>%k88+qhrp#TiM(y%@AyPHe$z!zNH43&Ro4w17
zuui&TBTiC(gKL9AZ(wLQTFA0^0dP_8)AL_<OO-aie%;!&X*U|&1ln%6wIQ_i*z3ze
zv;Qhr|FypQOND>`TAe^%{><ph=Cx9NE<V(Ur12e}s`feocX6F{uCtr^AZ`ngP8n6Z
z+nn)9{c07%JA&|=mX(e3UWb9=Q&T3PafHomGmX=LBR@Wcg*UfXt(G3VF_v}XUVk4T
z@M~)`aO2i0DzwUxQ4MSu-M(EmM!PSw_wT#Wr&#DB6fECkxOKA_$imx;(f;qJj}M8>
z7oJ~x+__JmH|JwWPg|=0`8Wa#Io#(}=;(&k&nM+l>+{d_sz*z>|Ct`*2aCu)EkZT|
z^zv^(KUBM)LkIoUYvZPXM6sCPF_S1EY@=P12o{=p*<L#7wKq0}37<33VRF=D-u4P3
zrwF6wOrKVm>r485XQgCfuR)m8KD2OL<h(v{Twg3b^h~yyGTC;{$xicbz}lYve!F+d
zyFM_vUQf#3-S}9Lylp%jetQ4@eyIqyT8!%N&|2{=*Jz!S1_^DJ3LD60K&~2xnu4Z@
zB@5+mR79+7QT>20v8rWSx0g2;r2%6jB~K;R1lx_!#x~a9*m5hhtaLSoh4_T%F>F)I
z`@QDWQR1R;2{gAG?y$VBacec7wau0T)@JJ0BB)yZie8`hqTzZ3n^w>11lQnf&iT%<
zY`SpsZ~E}@^{?LW%f%G7a?aJEZ1;^~wd=3dF`jousLG-Fy!N(cw8Ly~C$qhJy}D9X
z2;l=KBp6O(W?4`HFSI@h&Xj+rXKE&AV#a4|MrY)Trs#=fNf_>U_QJ#*V&Iyk%s9;v
z9qg)uK?m<N_mm3aT_%Yck|Iw`Fe$iKo@sQTd`3Z?&M3KxItrJ)a@GW&854xkm@<z!
zS}rX|bE#(3%qaTdgPc)ul|Y;(ok&VNMsAV_L1;~qOd(Sh-Z463WJYbfqgOFoDn0et
zDP=VYk-IF3u+j_7Rqe?7``XO8)zpv-A{d)+!4ayJFquZLa_!3pyGuvB3{FSNk_pmS
z?Yy&unV^!8-qh}5i~@KnPL$T3I-dzmj=Id1CtL)KJ-y?Y1wP|!#_5cc8M8BHW=zkR
znlaf!P+6&oErW0g)9eB?8I)tmQ>B?y@3@|EHREy;HAf`nGPB^F$N!R=U>s&$xd_8@
zp->ZSCg@C%8MiZTrczFX7-G0F7WN@b@*e6VqL4O>sVb-72NI7a>R<y=F)~esqTFQT
zR1`5#_=>H>#Z0J~koCj<ESw6kOhdg$mPr{|q%>qggwY~v<0^}zxhO+9H;M@xWQvyQ
zkaB=cYc6OuR2Ku2Y$ow9nF%`+<~VjDdhZYeD0RXssf^IVTFefK$w6<09X};UmrV94
zXO#>QR1r>-w^lJCrGSb><tR?g)CWWh&tZU8S{;*wyK$s=4MX?58KyivUmHnwJe1I>
zz>9mWSk4HHiYAgp3DnlKI~l~7XtT-;K_(~XY^FduIU6OjiGC3mrI|_H?n_-!C1qJD
z@QEUbpeVvBcOeHF<RUamJ4higlDK!0BA}!Yoh>fJon?k$B;FMYiWUlr3=(0PFr*c&
zvQ?RKn`p*2XCWQ}iX)YXm?=I}Y?O}GJ~~Pbw5O0MY(QqvEQ%yW7N!nIshN^H=qN3f
z<JKE4T}Xmzp0!nomYIaaGSZotX+G0zrs-Db)nukHQZrM!%y7TPB+-ay+#=q@5UjP)
z8UtQDLX**zh;I1Iu)QfeA%lXXh6)xzj6#P+c;`*xS+ai0hRzI`X|OOet!G-zwA{gn
zut-X1i&isRA^_}^B6l#VBxi;f{TMkjVr}?S<QGah7oF5Rz#b`VKf>=|mH;Wnlw4O+
zlTrJTHQFIWM#n6K%LEvJCJWn$h$#q_e37FJRAGw08ofUYPXd=xM=m{NPl+M;69+`h
z7`5E2lhrX?qL;<df)2_WXOTn#rkRkeHPmKhJ8K=o3pfb@BuB&&>k4)RZpj)d1BS9X
z<(~9)3_F*y_a;zdQ}7WvGH1+?Ny<?hl~!YU>?oDyU<f8HXP_a5z$2wY>@8SSBg2qI
zLbK#7+%xe6`2-%s11wYt>NpJ55GB17zUCRr3U_;+;Uh)xU;!b5U|uR@SRe?23HB7_
zDyh-i%9#~2%g-f)=YYZ*Io&%4_KGo*i=}ZRfp9IWG9dA(Gs<9WQ1IWZ6^)WIqAgbh
zDU?xS6_2viFSgT*0~BPMxkF*i5xOG-c(ia*z%ONZT4Y|^$@9So077HEqDnAWI}%l5
zNHW|wcyv`e5-R>kKLLj%Vpws?j0x0$4LZxfEJ4DHQu&4eni7FOR9=Mj6Vioe5U7us
z<wfU!1JM{17y*%tEhIr7f=)yY6QU_eBn0U-JV#06948UsDKmWbiC01t6%MiEgoFa-
zLYd`(@&k`hkVk0=IDsK@#$`!jv?PL!6h?uyP<-M#J_BxHn!AKiZW)9b8M2d1^W>pw
zW~tDjU<R*x2?MVoIl?UQ2SNq4p<bh`6tk#i%b-fxR-jyAM|D4Mr4dH0L}E~!p?<NF
zSYc4f$gC_4uHmiD!rO5#91#h|nz+${IC#Bh7D$as9ZbV}1IN(vca#8ycVSM^y43x(
z@TXVaSU?^t6ypdpzBssy$efzw0K_R8N!SG>N#0PagriviU=rpX0S3<0CuoHE+(^PN
zAc^JRu2A0tKM?1T3IN<B;!r>+VJ<b2$O}lqJcH*tiR_CEAVsk7VPG);nF3>MBZ;_x
zB+`|rBug500tFZ9k$_wb+>DUon$mf5iDHubqngPH<qblVmx$E_L6~Ob8bbl{7vO0F
zp8-Sf$-!u*Ab!#=M+U)Vv>qrKfi!cILmvp-p9x2G2S`c1fZyn3IMiOSzLUvVOXDC0
z+@BTVRNz!v&QYEq7wbS3@-l)LtW=sX1_2M?W-+%&JwO0CAcF!3CZkXk8H6v}V4<C<
ze}A^{a*EO-8y3Am#?ykK2#pMe0_(^Xcp?X(sXPaJfyn2x2H+3`pqFYQ6O1!zBfT)b
zN#p>alh_0Jtht{kdr)DyAWoOnQqG+KT%{2JHA(MG&a@GbeK`REcZi1zBex6WbT5Es
zlu!U=h8T}R1#KbB#Q9qac)lDcB7zyyk^<3i<XsfzDuIoGb0H~Jaa9!;VsW{WqKY7j
zA@T)#T3K3qh5Fl-5|<bfxlb;t4F9x(Q{`>)ywbF9Mg@{b=c6UWB+8?uRvH~m778UT
zYM(k|knpXDn^1uU?-Z3t70fai70Oblltg+?x)GPY8F6*VJyb<oHVQHmBubPez~(|_
zlbSU!RJmWyVM#I>uoD?w27+oy>J%*sBBO<fNHT*0R_WHNlwv@(ak+{><f<&6XgCL|
zCl+){oEU0^7s5+a1t~RQ{|m<5h^mQ1L6Xg=>ax#}I9n|t9}<dWjeuV;?h+JZjHbx7
zmV{Z9%19HQarkv8yMEOz)SGb&PJOm4DNH*}!J(RWmS>?EqorPNyjZ^(am#)mL%9}c
zL~S5UhMdZ4?^E!MsImh~)!T`YrF62M65?WFsOn@00M#nX90O21t=cU<Ys!lGTah~1
z;0Q-9;@&y$GEc^+#0ZfxDZsC)<hLU(^@OCHvsNNF84%N*OYpwze2y_!gbY*xF9lUq
z9QG`TIoOz7W;W^)J}t7iQb>_3q67(u1yu~K)?z61SA_tssV^0+sDm37Uy{rx6l$8I
zlBpFh0}5$$r{&uc+Mpsq)e93P)-fNYG_Y5qq3;ag>#AgNr$c4FfXy1qvdJ{T^L?O6
z=1d?eV2O;HrDkDOvo}2i6oMinj!Er!MAkEjl@TRC)`;FU(P{pshrlfZ$WGY`T2>%=
z5?P~~W6lyGvk!F$;!O|1AUNCTf(0xB=oT1Cb_5^^wK_`p2C!-Kwj5X@Qc_!vTiJxf
z5{wAhSQ9OiWoI@YB=lPATJMr~MAj=J8M9sqrxP@2tu9*-Iv2#rxJ;%=C**Bul;u+1
z+JqX~IF}QrBsm@^b%d~F7jfKf2rV~M)scXAI72a6rC@_*BqHOQ94yLmq06Br?=wJ7
z<zXSb0U68Bm1i@xPEyXbleVm6ut<$g1o719fEjD%M>k>^bTLIF{x;?*=B%WY4#hL3
z$r+S(35KR)h*sL>upTw$Z3^#U{mFWwnKxDvsX5?{lsuMgI+9~!0PJlFZ+I|>_vL^m
zyaTm1(~7&m9n+T3#5RQ=tgS6w2)2}HvG7#bSzI#q3T|go*(v}tqd97M$up7)4N@t+
zC{S(j5P427v0NezlyhOIIDp)>Pg#_OwX%moL@ku8x#B8C<)jxbY6BmR%qq^9R5=0Y
z6M<%ol-*jeLkLJ-Yo{5)Mi7o8`%CECqXd_^#GO(ZFi|!zCH@5dIR45c&6)$Q0<{}8
zh*V&K5EYD;3N&~kL_<^MAQz)$Z?_z*!pKNruZHPKhtQ)~G)gF=f<&O!LX>UNoKaY*
zN)Pf-I*pzpk)Sq{!t>;lBr$8DREVtZOxrp>B;U#Ov{ppv5RjIQa4OlPJw`7KT4fXq
zl^*(I&S06->6&sdt(=r4o&<()n2mBQ1jii9Ayql+;aQBm9#w-*;UECT40ghbkL=6R
z>X-#WZD84Qhi}L*JVpVQ7L6O0a>b^c-aV96MAoH5DdRmH)d}mgA%>)~<ZfhRl;yNw
zIWBk%AHjVT$?)i*LZmV(g^db~q)!-WwZ`Id<#1v-qgehwloynR49&`sL_lOrni532
zAZ_LmX*yS4^mP2947_Za5Mwjpv7A;1Dray~fWw${b!>B5o-_%-H<$+^o<<RX5R|1z
zNk$ZE+><&+b{byUI)NLE#)!!hgdm%GBZ$IiLkPC=;-}#i5DYBy+91k7o8Ff5?npR3
zIaK(z+9OAQL}<pvX?P~#h|`j?pkvCxWSJ=fGlI1-<qS&YS>{ilj;FM!s}=GYlo>q&
z3P&9wxi;Apu*a9tncEYL&mg;GVS)(UqU<Vo$OH_J>nKS`HItNw0LY$UiXfp2xV6(r
zw*e>^f+G=Ul6gwORl4Yl?8*cmro(t(tZY%2T@K;{F@_drP0<S~S=GN#Q=9!iYKW4l
HuhRek$PeuK

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