Commit c7fbd10a authored by Sylvain Dailler's avatar Sylvain Dailler

Update obsolete sessions

parent b4b79ae2
...@@ -33,7 +33,7 @@ ...@@ -33,7 +33,7 @@
<goal name="mantissa_one" proved="true"> <goal name="mantissa_one" proved="true">
<proof prover="2"><result status="valid" time="0.09" steps="88"/></proof> <proof prover="2"><result status="valid" time="0.09" steps="88"/></proof>
<proof prover="3"><result status="valid" time="1.04"/></proof> <proof prover="3"><result status="valid" time="1.04"/></proof>
<proof prover="5" timelimit="11"><result status="valid" time="3.11"/></proof> <proof prover="5" timelimit="11"><result status="valid" time="2.58"/></proof>
</goal> </goal>
<goal name="double_value_of_1" proved="true"> <goal name="double_value_of_1" proved="true">
<proof prover="1"><result status="valid" time="0.03"/></proof> <proof prover="1"><result status="valid" time="0.03"/></proof>
......
...@@ -62,7 +62,7 @@ ...@@ -62,7 +62,7 @@
<proof prover="10"><result status="valid" time="0.11" steps="101"/></proof> <proof prover="10"><result status="valid" time="0.11" steps="101"/></proof>
</goal> </goal>
<goal name="nth_const6" proved="true"> <goal name="nth_const6" proved="true">
<proof prover="4"><result status="valid" time="1.72"/></proof> <proof prover="4"><result status="valid" time="1.39"/></proof>
<proof prover="8"><result status="valid" time="0.79"/></proof> <proof prover="8"><result status="valid" time="0.79"/></proof>
<proof prover="10"><result status="valid" time="0.09" steps="101"/></proof> <proof prover="10"><result status="valid" time="0.09" steps="101"/></proof>
</goal> </goal>
...@@ -94,7 +94,7 @@ ...@@ -94,7 +94,7 @@
</goal> </goal>
<goal name="to_nat_mantissa_1" proved="true"> <goal name="to_nat_mantissa_1" proved="true">
<proof prover="4"><result status="valid" time="1.11"/></proof> <proof prover="4"><result status="valid" time="1.11"/></proof>
<proof prover="6" timelimit="10"><result status="valid" time="2.87"/></proof> <proof prover="6" timelimit="10"><result status="valid" time="2.38"/></proof>
<proof prover="8"><result status="valid" time="0.76"/></proof> <proof prover="8"><result status="valid" time="0.76"/></proof>
<proof prover="10"><result status="valid" time="0.05" steps="93"/></proof> <proof prover="10"><result status="valid" time="0.05" steps="93"/></proof>
</goal> </goal>
...@@ -142,7 +142,7 @@ ...@@ -142,7 +142,7 @@
</goal> </goal>
<goal name="nth_0_30" proved="true"> <goal name="nth_0_30" proved="true">
<proof prover="2"><result status="valid" time="0.46"/></proof> <proof prover="2"><result status="valid" time="0.46"/></proof>
<proof prover="4"><result status="valid" time="3.60"/></proof> <proof prover="4"><result status="valid" time="3.04"/></proof>
</goal> </goal>
<goal name="nth_jpxor_0_30" proved="true"> <goal name="nth_jpxor_0_30" proved="true">
<proof prover="2"><result status="valid" time="0.06"/></proof> <proof prover="2"><result status="valid" time="0.06"/></proof>
...@@ -363,9 +363,9 @@ ...@@ -363,9 +363,9 @@
<proof prover="10"><result status="valid" time="0.07" steps="97"/></proof> <proof prover="10"><result status="valid" time="0.07" steps="97"/></proof>
</goal> </goal>
<goal name="MainResult" proved="true"> <goal name="MainResult" proved="true">
<proof prover="2"><result status="valid" time="0.26"/></proof> <proof prover="2"><result status="valid" time="0.07"/></proof>
<proof prover="4"><result status="valid" time="3.62"/></proof> <proof prover="4"><result status="valid" time="0.09"/></proof>
<proof prover="6" timelimit="11"><result status="valid" time="2.70"/></proof> <proof prover="6" timelimit="11"><result status="valid" time="3.15"/></proof>
<proof prover="8"><result status="valid" time="0.74"/></proof> <proof prover="8"><result status="valid" time="0.74"/></proof>
<proof prover="10"><result status="valid" time="0.26" steps="146"/></proof> <proof prover="10"><result status="valid" time="0.26" steps="146"/></proof>
</goal> </goal>
......
...@@ -15,7 +15,7 @@ ...@@ -15,7 +15,7 @@
</goal> </goal>
<goal name="sign_of_j" proved="true"> <goal name="sign_of_j" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="75"/></proof> <proof prover="0"><result status="valid" time="0.02" steps="75"/></proof>
<proof prover="3"><result status="valid" time="4.98"/></proof> <proof prover="3"><result status="valid" time="4.15"/></proof>
</goal> </goal>
<goal name="mantissa_of_j" proved="true"> <goal name="mantissa_of_j" proved="true">
<proof prover="0"><result status="valid" time="0.16" steps="121"/></proof> <proof prover="0"><result status="valid" time="0.16" steps="121"/></proof>
...@@ -57,7 +57,7 @@ ...@@ -57,7 +57,7 @@
</goal> </goal>
<goal name="Mantissa_of_xor_j" proved="true"> <goal name="Mantissa_of_xor_j" proved="true">
<proof prover="3"><result status="valid" time="1.75"/></proof> <proof prover="3"><result status="valid" time="1.75"/></proof>
<proof prover="5"><result status="valid" time="3.22"/></proof> <proof prover="5"><result status="valid" time="2.49"/></proof>
<proof prover="9"><result status="valid" time="0.75"/></proof> <proof prover="9"><result status="valid" time="0.75"/></proof>
</goal> </goal>
<goal name="MainResultZero" proved="true"> <goal name="MainResultZero" proved="true">
......
...@@ -583,7 +583,7 @@ ...@@ -583,7 +583,7 @@
</transf> </transf>
</goal> </goal>
<goal name="Power_sum" proved="true"> <goal name="Power_sum" proved="true">
<proof prover="1"><result status="valid" time="1.87"/></proof> <proof prover="1"><result status="valid" time="3.46"/></proof>
</goal> </goal>
<goal name="Pow2_int_real" proved="true"> <goal name="Pow2_int_real" proved="true">
<transf name="introduce_premises" proved="true" > <transf name="introduce_premises" proved="true" >
......
<?xml version="1.0" encoding="UTF-8"?> <?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN" <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd"> "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="5"> <why3session shape_version="6">
<prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file proved="true"> <file proved="true">
<path name=".."/> <path name=".."/>
......
...@@ -57,7 +57,7 @@ ...@@ -57,7 +57,7 @@
<proof prover="3"><result status="timeout" time="5.00"/></proof> <proof prover="3"><result status="timeout" time="5.00"/></proof>
<proof prover="4"><result status="valid" time="1.27"/></proof> <proof prover="4"><result status="valid" time="1.27"/></proof>
<proof prover="5"><result status="timeout" time="5.00"/></proof> <proof prover="5"><result status="timeout" time="5.00"/></proof>
<proof prover="6"><result status="valid" time="4.15"/></proof> <proof prover="6"><result status="valid" time="2.88"/></proof>
<proof prover="10"><result status="timeout" time="5.00"/></proof> <proof prover="10"><result status="timeout" time="5.00"/></proof>
</goal> </goal>
<goal name="VC triplet.4" expl="assertion" proved="true"> <goal name="VC triplet.4" expl="assertion" proved="true">
...@@ -78,7 +78,7 @@ ...@@ -78,7 +78,7 @@
<proof prover="10"><result status="valid" time="0.08" steps="184"/></proof> <proof prover="10"><result status="valid" time="0.08" steps="184"/></proof>
</goal> </goal>
<goal name="VC triplet.7" expl="assertion" proved="true"> <goal name="VC triplet.7" expl="assertion" proved="true">
<proof prover="6"><result status="valid" time="5.01"/></proof> <proof prover="6"><result status="valid" time="4.01"/></proof>
<proof prover="7"><result status="timeout" time="5.00"/></proof> <proof prover="7"><result status="timeout" time="5.00"/></proof>
<proof prover="8"><result status="timeout" time="5.00"/></proof> <proof prover="8"><result status="timeout" time="5.00"/></proof>
<proof prover="9"><result status="timeout" time="5.00"/></proof> <proof prover="9"><result status="timeout" time="5.00"/></proof>
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment