diff --git a/examples/paxosNoRefinement/paxos/why3session.xml b/examples/paxosNoRefinement/paxos/why3session.xml
index 0135389..1c2dc12 100644
--- a/examples/paxosNoRefinement/paxos/why3session.xml
+++ b/examples/paxosNoRefinement/paxos/why3session.xml
@@ -3,7 +3,7 @@
 "https://www.why3.org/why3session.dtd">
 <why3session shape_version="6">
 <prover id="0" name="CVC5" version="1.0.3" timelimit="1" steplimit="0" memlimit="1000"/>
-<prover id="1" name="Alt-Ergo" version="2.5.3" timelimit="30" steplimit="0" memlimit="4000"/>
+<prover id="1" name="Alt-Ergo" version="2.5.3" timelimit="10000" steplimit="0" memlimit="5000"/>
 <prover id="2" name="CVC4" version="1.8" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="3" name="Alt-Ergo" version="2.4.2" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="4" name="Eprover" version="2.6" timelimit="1" steplimit="0" memlimit="1000"/>
@@ -119,7 +119,7 @@
        <goal name="propose&#39;vc.0.0.13.0.0.0" expl="VC for propose" proved="true">
        <transf name="split_vc" proved="true" >
         <goal name="propose&#39;vc.0.0.13.0.0.0.0" expl="VC for propose" proved="true">
-        <proof prover="1"><result status="valid" time="5.681226" steps="101850"/></proof>
+        <proof prover="1"><result status="valid" time="5.198745" steps="101850"/></proof>
         </goal>
        </transf>
        </goal>