bitvectors: updated proof session

parent d53814ed
......@@ -30,7 +30,7 @@
</goal>
<goal name="nth_j6" proved="true">
<proof prover="1"><result status="valid" time="0.07" steps="76"/></proof>
<proof prover="4"><result status="valid" time="3.72"/></proof>
<proof prover="4"><result status="valid" time="4.40"/></proof>
</goal>
<goal name="nth_j7" proved="true">
<proof prover="1"><result status="valid" time="0.04" steps="76"/></proof>
......@@ -51,12 +51,12 @@
</goal>
<goal name="nth_const4" proved="true">
<proof prover="1"><result status="valid" time="0.10" steps="100"/></proof>
<proof prover="4"><result status="valid" time="1.57"/></proof>
<proof prover="4"><result status="valid" time="1.87"/></proof>
<proof prover="8"><result status="valid" time="0.76"/></proof>
</goal>
<goal name="nth_const5" proved="true">
<proof prover="1"><result status="valid" time="0.11" steps="100"/></proof>
<proof prover="4"><result status="valid" time="1.65"/></proof>
<proof prover="4"><result status="valid" time="2.05"/></proof>
<proof prover="8"><result status="valid" time="0.74"/></proof>
</goal>
<goal name="nth_const6" proved="true">
......@@ -66,7 +66,7 @@
</goal>
<goal name="nth_const7" proved="true">
<proof prover="1"><result status="valid" time="0.11" steps="100"/></proof>
<proof prover="4"><result status="valid" time="1.60"/></proof>
<proof prover="4"><result status="valid" time="1.92"/></proof>
<proof prover="8"><result status="valid" time="0.73"/></proof>
</goal>
<goal name="nth_const8" proved="true">
......@@ -92,7 +92,7 @@
</goal>
<goal name="to_nat_mantissa_1" proved="true">
<proof prover="1"><result status="valid" time="0.05" steps="91"/></proof>
<proof prover="4"><result status="valid" time="1.18"/></proof>
<proof prover="4"><result status="valid" time="1.43"/></proof>
<proof prover="6" timelimit="10"><result status="valid" time="2.87"/></proof>
<proof prover="8"><result status="valid" time="0.76"/></proof>
</goal>
......@@ -104,13 +104,13 @@
</goal>
<goal name="mantissa_const_to_nat51" proved="true">
<proof prover="1"><result status="valid" time="0.18" steps="132"/></proof>
<proof prover="4"><result status="valid" time="1.13"/></proof>
<proof prover="4"><result status="valid" time="1.44"/></proof>
<proof prover="6" timelimit="11"><result status="valid" time="3.71"/></proof>
<proof prover="8"><result status="valid" time="0.75"/></proof>
</goal>
<goal name="mantissa_const" proved="true">
<proof prover="1"><result status="valid" time="0.08" steps="104"/></proof>
<proof prover="4"><result status="valid" time="3.18"/></proof>
<proof prover="4"><result status="valid" time="4.19"/></proof>
</goal>
<goal name="real1075m1023" proved="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
......@@ -140,7 +140,7 @@
</goal>
<goal name="nth_0_30" proved="true">
<proof prover="2"><result status="valid" time="0.46"/></proof>
<proof prover="4"><result status="valid" time="3.40"/></proof>
<proof prover="4"><result status="valid" time="3.97"/></proof>
</goal>
<goal name="nth_jpxor_0_30" proved="true">
<proof prover="1"><result status="valid" time="0.08" steps="98"/></proof>
......@@ -149,11 +149,11 @@
</goal>
<goal name="nth_var31" proved="true">
<proof prover="1" timelimit="125"><result status="valid" time="3.53" steps="253"/></proof>
<proof prover="4"><result status="valid" time="2.96"/></proof>
<proof prover="4"><result status="valid" time="3.55"/></proof>
</goal>
<goal name="to_nat_sub_0_30" proved="true">
<proof prover="4"><result status="valid" time="1.28"/></proof>
<proof prover="6" timelimit="10"><result status="valid" time="2.78"/></proof>
<proof prover="4"><result status="valid" time="1.75"/></proof>
<proof prover="6" timelimit="10"><result status="valid" time="3.16"/></proof>
<proof prover="8"><result status="valid" time="0.84"/></proof>
</goal>
<goal name="jpxorx_pos" proved="true">
......@@ -169,7 +169,7 @@
<goal name="lemma1_pos" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="lemma1_pos.0" proved="true">
<proof prover="10" timelimit="10"><result status="valid" time="6.18" steps="1022"/></proof>
<proof prover="10" timelimit="10"><result status="valid" time="7.27" steps="1022"/></proof>
</goal>
</transf>
</goal>
......@@ -180,12 +180,12 @@
<proof prover="8"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="from_int2c_to_nat_sub_neg" proved="true">
<proof prover="5" timelimit="5" edited="double_of_int_DoubleOfInt_from_int2c_to_nat_sub_neg_1.v"><result status="valid" time="1.93"/></proof>
<proof prover="5" timelimit="5" edited="double_of_int_DoubleOfInt_from_int2c_to_nat_sub_neg_1.v"><result status="valid" time="2.23"/></proof>
</goal>
<goal name="lemma1_neg" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="lemma1_neg.0" proved="true">
<proof prover="10" timelimit="10"><result status="valid" time="4.16" steps="827"/></proof>
<proof prover="10" timelimit="10"><result status="valid" time="4.97" steps="827"/></proof>
</goal>
</transf>
</goal>
......@@ -197,7 +197,7 @@
<proof prover="8"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="nth_var_0_31" proved="true">
<proof prover="4" timelimit="10"><result status="valid" time="2.79"/></proof>
<proof prover="4" timelimit="10"><result status="valid" time="3.72"/></proof>
</goal>
<goal name="to_nat_bv32_bv64_aux" proved="true">
<transf name="introduce_premises" proved="true" >
......@@ -221,16 +221,16 @@
<proof prover="8"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="to_nat_var_0_31" proved="true">
<proof prover="4"><result status="valid" time="1.33"/></proof>
<proof prover="4"><result status="valid" time="1.64"/></proof>
<proof prover="6" timelimit="11"><result status="valid" time="0.14"/></proof>
<proof prover="8"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="nth_var32to63" proved="true">
<proof prover="4"><result status="valid" time="3.14"/></proof>
<proof prover="4"><result status="valid" time="3.64"/></proof>
</goal>
<goal name="nth_var3" proved="true">
<proof prover="1"><result status="valid" time="1.39" steps="146"/></proof>
<proof prover="4"><result status="valid" time="1.26"/></proof>
<proof prover="4"><result status="valid" time="1.55"/></proof>
<proof prover="8"><result status="valid" time="0.88"/></proof>
</goal>
<goal name="lemma2" proved="true">
......@@ -240,7 +240,7 @@
<goal name="lemma2.0.0" proved="true">
<transf name="inline_goal" proved="true" >
<goal name="lemma2.0.0.0" proved="true">
<proof prover="11"><result status="valid" time="3.80"/></proof>
<proof prover="11"><result status="valid" time="5.66"/></proof>
</goal>
</transf>
</goal>
......@@ -255,17 +255,17 @@
</goal>
<goal name="nth_var5" proved="true">
<proof prover="1"><result status="valid" time="1.20" steps="148"/></proof>
<proof prover="4"><result status="valid" time="1.78"/></proof>
<proof prover="4"><result status="valid" time="2.07"/></proof>
<proof prover="8"><result status="valid" time="0.85"/></proof>
</goal>
<goal name="nth_var6" proved="true">
<proof prover="1"><result status="valid" time="1.17" steps="148"/></proof>
<proof prover="4"><result status="valid" time="1.74"/></proof>
<proof prover="4"><result status="valid" time="2.14"/></proof>
<proof prover="8"><result status="valid" time="0.83"/></proof>
</goal>
<goal name="nth_var7" proved="true">
<proof prover="1"><result status="valid" time="1.39" steps="148"/></proof>
<proof prover="4"><result status="valid" time="1.69"/></proof>
<proof prover="4"><result status="valid" time="2.06"/></proof>
<proof prover="8"><result status="valid" time="0.82"/></proof>
</goal>
<goal name="nth_var8" proved="true">
......@@ -276,7 +276,7 @@
<proof prover="8"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="lemma3" proved="true">
<proof prover="4"><result status="valid" time="3.15"/></proof>
<proof prover="4"><result status="valid" time="3.82"/></proof>
</goal>
<goal name="nth_var9" proved="true">
<proof prover="1"><result status="valid" time="0.10" steps="95"/></proof>
......@@ -300,7 +300,7 @@
<proof prover="8"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="var_value0" proved="true">
<proof prover="5" timelimit="0" memlimit="0" edited="double_of_int_DoubleOfInt_var_value0_1.v"><result status="valid" time="3.39"/></proof>
<proof prover="5" timelimit="0" memlimit="0" edited="double_of_int_DoubleOfInt_var_value0_1.v"><result status="valid" time="3.95"/></proof>
</goal>
<goal name="from_int_sum" proved="true">
<proof prover="1"><result status="valid" time="0.05" steps="92"/></proof>
......@@ -336,9 +336,9 @@
<goal name="MainResult" proved="true">
<proof prover="1"><result status="valid" time="1.56" steps="143"/></proof>
<proof prover="2"><result status="valid" time="0.26"/></proof>
<proof prover="4"><result status="valid" time="4.00"/></proof>
<proof prover="4"><result status="valid" time="4.72"/></proof>
<proof prover="6" timelimit="11"><result status="valid" time="3.12"/></proof>
<proof prover="8"><result status="valid" time="0.76"/></proof>
<proof prover="8"><result status="valid" time="0.95"/></proof>
</goal>
</theory>
</file>
......
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