Commit dcd1cd96 authored by MARCHE Claude's avatar MARCHE Claude

minor update sessions (time only)

parent c3aa905c
......@@ -442,7 +442,7 @@
<proof prover="2"><result status="valid" time="0.02" steps="13"/></proof>
</goal>
<goal name="if_rule.0.1" proved="true">
<proof prover="10" timelimit="10" memlimit="4000"><result status="valid" time="2.72"/></proof>
<proof prover="10" timelimit="10" memlimit="4000"><result status="valid" time="3.10"/></proof>
<transf name="inversion_pr" proved="true" >
<goal name="if_rule.0.1.0" proved="true">
<proof prover="10"><result status="valid" time="0.08"/></proof>
......
......@@ -507,7 +507,7 @@
<proof prover="4"><result status="valid" time="0.03" steps="67"/></proof>
</goal>
<goal name="VC remove_count.1" expl="postcondition" proved="true">
<proof prover="1" timelimit="10"><result status="valid" time="4.68"/></proof>
<proof prover="1" timelimit="10"><result status="valid" time="5.42"/></proof>
</goal>
<goal name="VC remove_count.2" expl="postcondition" proved="true">
<proof prover="1" timelimit="10"><result status="valid" time="0.47"/></proof>
......
......@@ -683,7 +683,7 @@
<proof prover="6"><result status="valid" time="0.03" steps="79"/></proof>
</goal>
<goal name="VC triangleInequalityInt.0.1" expl="VC for triangleInequalityInt" proved="true">
<proof prover="0" timelimit="10"><result status="valid" time="4.92"/></proof>
<proof prover="0" timelimit="10"><result status="valid" time="5.72"/></proof>
</goal>
</transf>
</goal>
......
......@@ -181,7 +181,7 @@
<proof prover="4" timelimit="30"><result status="valid" time="6.45" steps="2706"/></proof>
</goal>
<goal name="to_nat_0x00000003" proved="true">
<proof prover="6" timelimit="120"><result status="valid" time="53.64"/></proof>
<proof prover="6" timelimit="120"><result status="valid" time="68.07"/></proof>
</goal>
<goal name="to_nat_0x00000007" proved="true">
<proof prover="4" timelimit="30"><result status="valid" time="9.99" steps="2976"/></proof>
......
......@@ -581,7 +581,7 @@
</transf>
</goal>
<goal name="Power_sum" proved="true">
<proof prover="1"><result status="valid" time="3.21"/></proof>
<proof prover="1"><result status="valid" time="3.92"/></proof>
</goal>
<goal name="Pow2_int_real" proved="true">
<transf name="introduce_premises" proved="true" >
......
......@@ -108,7 +108,7 @@
<proof prover="7"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC shortest_path_code.6" expl="loop invariant init" proved="true">
<proof prover="2"><result status="valid" time="3.52"/></proof>
<proof prover="2"><result status="valid" time="2.45"/></proof>
<proof prover="5"><result status="valid" time="1.46"/></proof>
</goal>
<goal name="VC shortest_path_code.7" expl="loop invariant init" proved="true">
......
......@@ -78,7 +78,7 @@
</transf>
</goal>
<goal name="min_dist_diff" proved="true">
<proof prover="2" edited="edit_distance_Word_min_dist_diff_1.v"><result status="valid" time="0.47"/></proof>
<proof prover="2" edited="edit_distance_Word_min_dist_diff_1.v"><result status="valid" time="0.28"/></proof>
</goal>
<goal name="min_dist_eps" proved="true">
<transf name="inline_goal" proved="true" >
......@@ -144,10 +144,10 @@
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC distance.5" expl="index in array bounds" proved="true">
<proof prover="11"><result status="valid" time="0.03"/></proof>
<proof prover="11"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC distance.6" expl="index in array bounds" proved="true">
<proof prover="11"><result status="valid" time="0.02"/></proof>
<proof prover="11"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC distance.7" expl="index in array bounds" proved="true">
<proof prover="11"><result status="valid" time="0.03"/></proof>
......
......@@ -21,10 +21,10 @@
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC gcd.4" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC gcd.5" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC gcd.6" expl="loop variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.06"/></proof>
......
......@@ -587,7 +587,7 @@
<proof prover="4" timelimit="10" memlimit="4000"><result status="valid" time="2.80" steps="571"/></proof>
</goal>
<goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.0.0.1.0.0.0.0.1.0.0.0.1" proved="true">
<proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="1.84"/></proof>
<proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="2.16"/></proof>
</goal>
</transf>
</goal>
......@@ -611,7 +611,7 @@
</transf>
</goal>
<goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.0.0.1.0.0.1" proved="true">
<proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="1.87"/></proof>
<proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="2.37"/></proof>
</goal>
</transf>
</goal>
......@@ -650,7 +650,7 @@
</transf>
</goal>
<goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.0.0.1.0.1.0.0.1.0.0.0.0.1" proved="true">
<proof prover="3" timelimit="5"><result status="valid" time="1.86"/></proof>
<proof prover="3" timelimit="5"><result status="valid" time="2.32"/></proof>
</goal>
</transf>
</goal>
......@@ -674,12 +674,12 @@
</transf>
</goal>
<goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.0.0.1.0.1.0.1" proved="true">
<proof prover="3" timelimit="5"><result status="valid" time="1.21"/></proof>
<proof prover="3" timelimit="5"><result status="valid" time="1.47"/></proof>
</goal>
</transf>
</goal>
<goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.0.0.1.0.1.1" proved="true">
<proof prover="3" timelimit="5"><result status="valid" time="1.87"/></proof>
<proof prover="3" timelimit="5"><result status="valid" time="2.25"/></proof>
</goal>
</transf>
</goal>
......
......@@ -509,7 +509,7 @@
</transf>
</goal>
<goal name="VC sub_valid_coloring_white.8.1.0.1.0.2" expl="VC for sub_valid_coloring_white" proved="true">
<proof prover="4" timelimit="10" memlimit="4000"><result status="valid" time="6.68"/></proof>
<proof prover="4" timelimit="10" memlimit="4000"><result status="valid" time="7.51"/></proof>
</goal>
</transf>
</goal>
......
......@@ -19,7 +19,7 @@
<proof prover="6"><result status="valid" time="0.01" steps="13"/></proof>
</goal>
<goal name="NumOfDummy.VC numof_eq" expl="VC for numof_eq" proved="true">
<proof prover="2"><result status="valid" time="3.49"/></proof>
<proof prover="2"><result status="valid" time="3.96"/></proof>
</goal>
<goal name="NumOfDummy.VC dummy_const" expl="VC for dummy_const" proved="true">
<proof prover="6"><result status="valid" time="0.22" steps="356"/></proof>
......@@ -346,7 +346,7 @@
</transf>
</goal>
<goal name="VC copy" expl="VC for copy" proved="true">
<proof prover="2"><result status="valid" time="2.03"/></proof>
<proof prover="2"><result status="valid" time="2.38"/></proof>
</goal>
<goal name="VC find_dummy" expl="VC for find_dummy" proved="true">
<proof prover="6"><result status="valid" time="1.02" steps="1301"/></proof>
......
......@@ -378,7 +378,7 @@
</goal>
<goal name="VC list_seg_no_repet.9" expl="assertion" proved="true">
<proof prover="2" timelimit="10"><result status="valid" time="1.27"/></proof>
<proof prover="4"><result status="valid" time="6.55"/></proof>
<proof prover="4"><result status="valid" time="9.06"/></proof>
</goal>
<goal name="VC list_seg_no_repet.10" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.20"/></proof>
......
......@@ -65,7 +65,7 @@
<proof prover="4"><result status="valid" time="0.03"/></proof>
<proof prover="5"><result status="unknown" time="0.00"/></proof>
<proof prover="7"><result status="unknown" time="0.00"/></proof>
<proof prover="8"><result status="valid" time="5.80"/></proof>
<proof prover="8"><result status="valid" time="6.80"/></proof>
<proof prover="9"><result status="valid" time="0.04"/></proof>
<proof prover="10"><result status="valid" time="0.00"/></proof>
<proof prover="11"><result status="valid" time="0.01"/></proof>
......
......@@ -62,7 +62,7 @@
</goal>
<goal name="CauchySchwarz_aux_non_null" proved="true">
<proof prover="4"><result status="valid" time="0.03"/></proof>
<proof prover="8" edited="triangle_inequality_CauchySchwarzInequality_CauchySchwarz_aux_non_null_1.v"><result status="valid" time="0.42"/></proof>
<proof prover="8" edited="triangle_inequality_CauchySchwarzInequality_CauchySchwarz_aux_non_null_1.v"><result status="valid" time="0.23"/></proof>
</goal>
<goal name="norm_null" proved="true">
<proof prover="4"><result status="valid" time="0.06"/></proof>
......
......@@ -314,7 +314,7 @@
<proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.48"/></proof>
</goal>
<goal name="VC sort.16.7" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="4.93"/></proof>
<proof prover="0"><result status="valid" time="5.66"/></proof>
</goal>
<goal name="VC sort.16.8" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.02" steps="27"/></proof>
......
......@@ -857,7 +857,7 @@
<proof prover="5" timelimit="1"><result status="valid" time="0.02" steps="62"/></proof>
</goal>
<goal name="VC wmpn_add_in_place.13" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.84"/></proof>
<proof prover="0"><result status="valid" time="0.65"/></proof>
</goal>
<goal name="VC wmpn_add_in_place.14" expl="precondition" proved="true">
<proof prover="5" memlimit="2000"><result status="valid" time="0.08" steps="38"/></proof>
......
......@@ -3003,7 +3003,7 @@
<goal name="VC submul_limb.22" expl="assertion" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC submul_limb.22.0" expl="VC for submul_limb" proved="true">
<proof prover="0" timelimit="10"><result status="valid" time="3.80"/></proof>
<proof prover="0" timelimit="10"><result status="valid" time="4.32"/></proof>
</goal>
<goal name="VC submul_limb.22.1" expl="VC for submul_limb" proved="true">
<proof prover="0"><result status="valid" time="0.06"/></proof>
......@@ -3308,7 +3308,7 @@
<proof prover="5"><result status="valid" time="0.03" steps="94"/></proof>
</goal>
<goal name="VC div_sb_qr.39.1" expl="VC for div_sb_qr" proved="true">
<proof prover="2" timelimit="5"><result status="valid" time="0.26"/></proof>
<proof prover="2" timelimit="5"><result status="valid" time="0.13"/></proof>
</goal>
</transf>
</goal>
......@@ -3357,7 +3357,7 @@
<proof prover="1"><result status="valid" time="2.45"/></proof>
</goal>
<goal name="VC div_sb_qr.44.9" expl="VC for div_sb_qr" proved="true">
<proof prover="1"><result status="valid" time="2.38"/></proof>
<proof prover="1"><result status="valid" time="2.72"/></proof>
</goal>
<goal name="VC div_sb_qr.44.10" expl="VC for div_sb_qr" proved="true">
<proof prover="1"><result status="valid" time="0.33"/></proof>
......@@ -4220,7 +4220,7 @@
<proof prover="5"><result status="valid" time="0.38" steps="152"/></proof>
</goal>
<goal name="VC div_sb_qr.122.3" expl="VC for div_sb_qr" proved="true">
<proof prover="5"><result status="valid" time="0.44" steps="158"/></proof>
<proof prover="5"><result status="valid" time="0.29" steps="158"/></proof>
</goal>
<goal name="VC div_sb_qr.122.4" expl="VC for div_sb_qr" proved="true">
<proof prover="2"><result status="valid" time="0.32"/></proof>
......@@ -4304,7 +4304,7 @@
<goal name="VC div_sb_qr.134.0.0.0" expl="precondition" proved="true">
<transf name="inline_goal" proved="true" >
<goal name="VC div_sb_qr.134.0.0.0.0" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="3.78"/></proof>
<proof prover="3"><result status="valid" time="4.32"/></proof>
</goal>
</transf>
</goal>
......@@ -4539,7 +4539,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC div_sb_qr.157.0.0.0.31" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC div_sb_qr.157.0.0.0.32" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......@@ -4563,7 +4563,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC div_sb_qr.157.0.0.0.39" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC div_sb_qr.157.0.0.0.40" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......@@ -6890,7 +6890,7 @@
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC div_sb_qr.239.0.0.0.86" proved="true">
<proof prover="3"><result status="valid" time="0.33"/></proof>
<proof prover="3"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC div_sb_qr.239.0.0.0.87" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
......@@ -7627,7 +7627,7 @@
<goal name="VC div_sb_qr.271" expl="postcondition" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC div_sb_qr.271.0" expl="postcondition" proved="true">
<proof prover="5"><result status="valid" time="0.61" steps="157"/></proof>
<proof prover="5"><result status="valid" time="0.41" steps="157"/></proof>
</goal>
<goal name="VC div_sb_qr.271.1" expl="postcondition" proved="true">
<proof prover="5"><result status="valid" time="0.20" steps="157"/></proof>
......@@ -9473,7 +9473,7 @@
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC div_qr.148" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="3.20"/></proof>
<proof prover="0"><result status="valid" time="3.64"/></proof>
</goal>
<goal name="VC div_qr.149" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.24"/></proof>
......
......@@ -1043,7 +1043,7 @@
<proof prover="0"><result status="valid" time="0.30"/></proof>
</goal>
<goal name="VC wmpn_lshift_in_place.43.1" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.43"/></proof>
<proof prover="0"><result status="valid" time="0.28"/></proof>
</goal>
<goal name="VC wmpn_lshift_in_place.43.2" expl="VC for wmpn_lshift_in_place" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
......
......@@ -606,7 +606,7 @@
<proof prover="5" timelimit="20"><result status="valid" time="0.02" steps="29"/></proof>
</goal>
<goal name="VC wmpn_addmul_n.3" expl="precondition" proved="true">
<proof prover="5" timelimit="20"><result status="valid" time="0.12" steps="29"/></proof>
<proof prover="5" timelimit="20"><result status="valid" time="0.00" steps="29"/></proof>
</goal>
<goal name="VC wmpn_addmul_n.4" expl="integer overflow" proved="true">
<proof prover="5" timelimit="20"><result status="valid" time="0.04" steps="37"/></proof>
......@@ -1153,7 +1153,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_mul_basecase.41.0.0.0.0.0.0.29" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_mul_basecase.41.0.0.0.0.0.0.30" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......@@ -1165,7 +1165,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_mul_basecase.41.0.0.0.0.0.0.33" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC wmpn_mul_basecase.41.0.0.0.0.0.0.34" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......
......@@ -1138,7 +1138,7 @@
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC wmpn_decr.24.2" expl="VC for wmpn_decr" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.52" steps="76"/></proof>
<proof prover="5" timelimit="1"><result status="valid" time="0.68" steps="76"/></proof>
</goal>
<goal name="VC wmpn_decr.24.3" expl="VC for wmpn_decr" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
......
......@@ -100,7 +100,7 @@
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC wmpn_toom22_mul.15" expl="integer overflow" proved="true">
<proof prover="0"><result status="valid" time="3.00"/></proof>
<proof prover="0"><result status="valid" time="3.44"/></proof>
</goal>
<goal name="VC wmpn_toom22_mul.16" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
......@@ -341,7 +341,7 @@
<proof prover="5"><result status="valid" time="0.60" steps="194"/></proof>
</goal>
<goal name="VC wmpn_toom22_mul.81" expl="integer overflow" proved="true">
<proof prover="4" timelimit="20" memlimit="1000"><result status="valid" time="5.70"/></proof>
<proof prover="4" timelimit="20" memlimit="1000"><result status="valid" time="6.50"/></proof>
<proof prover="5" timelimit="20"><result status="valid" time="12.04" steps="380"/></proof>
</goal>
<goal name="VC wmpn_toom22_mul.82" expl="precondition" proved="true">
......@@ -1889,7 +1889,7 @@
<goal name="VC wmpn_toom22_mul.319.0.0.0.0.0" expl="precondition" proved="true">
<transf name="apply" proved="true" arg1="H6">
<goal name="VC wmpn_toom22_mul.319.0.0.0.0.0.0" proved="true">
<proof prover="1" memlimit="2000"><result status="valid" time="0.23"/></proof>
<proof prover="1" memlimit="2000"><result status="valid" time="0.10"/></proof>
</goal>
</transf>
</goal>
......@@ -2117,10 +2117,10 @@
</transf>
</goal>
<goal name="VC wmpn_toom22_mul.335.3.1" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC wmpn_toom22_mul.335.3.2" proved="true">
<proof prover="3"><result status="valid" time="0.06"/></proof>
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
</goal>
......@@ -3296,7 +3296,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_toom22_mul.353.8" expl="VC for wmpn_toom22_mul" proved="true">
<proof prover="4"><result status="valid" time="0.48"/></proof>
<proof prover="4"><result status="valid" time="0.30"/></proof>
</goal>
<goal name="VC wmpn_toom22_mul.353.9" expl="VC for wmpn_toom22_mul" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
......@@ -5041,7 +5041,7 @@
<proof prover="3" timelimit="1"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.121.2" expl="VC for wmpn_toom32_mul" proved="true">
<proof prover="3"><result status="valid" time="0.49"/></proof>
<proof prover="3"><result status="valid" time="0.32"/></proof>
</goal>
</transf>
</goal>
......@@ -5403,7 +5403,7 @@
<proof prover="1"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.188" expl="integer overflow" proved="true">
<proof prover="1"><result status="valid" time="0.30"/></proof>
<proof prover="1"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.189" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.12"/></proof>
......@@ -5475,7 +5475,7 @@
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.197.13" expl="VC for wmpn_toom32_mul" proved="true">
<proof prover="4"><result status="valid" time="0.33"/></proof>
<proof prover="4"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.197.14" expl="VC for wmpn_toom32_mul" proved="true">
<proof prover="1"><result status="valid" time="0.06"/></proof>
......@@ -5647,13 +5647,13 @@
<proof prover="1"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.237" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.06"/></proof>
<proof prover="1"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.238" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.239" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.09"/></proof>
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.240" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
......@@ -5905,13 +5905,13 @@
<proof prover="0" timelimit="1"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.253.15" expl="VC for wmpn_toom32_mul" proved="true">
<proof prover="1"><result status="valid" time="0.24"/></proof>
<proof prover="1"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.253.16" expl="VC for wmpn_toom32_mul" proved="true">
<proof prover="1"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.253.17" expl="VC for wmpn_toom32_mul" proved="true">
<proof prover="1"><result status="valid" time="0.24"/></proof>
<proof prover="1"><result status="valid" time="0.11"/></proof>
</goal>
</transf>
</goal>
......@@ -6069,7 +6069,7 @@
<proof prover="1"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.272.10" expl="VC for wmpn_toom32_mul" proved="true">
<proof prover="1"><result status="valid" time="0.24"/></proof>
<proof prover="1"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.272.11" expl="VC for wmpn_toom32_mul" proved="true">
<proof prover="1"><result status="valid" time="0.33"/></proof>
......@@ -6725,7 +6725,7 @@
<proof prover="1"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.357.5" expl="VC for wmpn_toom32_mul" proved="true">
<proof prover="1"><result status="valid" time="0.26"/></proof>
<proof prover="1"><result status="valid" time="0.13"/></proof>
</goal>
</transf>
</goal>
......@@ -6735,10 +6735,10 @@
<proof prover="1"><result status="valid" time="0.23"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.358.1" expl="VC for wmpn_toom32_mul" proved="true">
<proof prover="1"><result status="valid" time="0.09"/></proof>
<proof prover="1"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.358.2" expl="VC for wmpn_toom32_mul" proved="true">
<proof prover="1"><result status="valid" time="0.08"/></proof>
<proof prover="1"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.358.3" expl="VC for wmpn_toom32_mul" proved="true">
<proof prover="1"><result status="valid" time="0.09"/></proof>
......@@ -6843,7 +6843,7 @@
<proof prover="4"><result status="valid" time="0.32"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.366" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.25"/></proof>
<proof prover="1"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.367" expl="postcondition" proved="true">
<proof prover="1" timelimit="1"><result status="valid" time="0.06"/></proof>
......@@ -7122,7 +7122,7 @@
<proof prover="1" timelimit="1"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.421" expl="assertion" proved="true">
<proof prover="0" timelimit="10"><result status="valid" time="8.46"/></proof>
<proof prover="0" timelimit="10"><result status="valid" time="9.63"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.422" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.04"/></proof>
......@@ -7131,7 +7131,7 @@
<proof prover="4"><result status="valid" time="0.26"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.424" expl="precondition" proved="true">
<proof prover="1" timelimit="1"><result status="valid" time="0.25"/></proof>
<proof prover="1" timelimit="1"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.425" expl="precondition" proved="true">
<transf name="inline_goal" proved="true" >
......@@ -7472,10 +7472,10 @@
<proof prover="1" timelimit="1"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.473.0.0.0.1" proved="true">
<proof prover="1" timelimit="1"><result status="valid" time="0.26"/></proof>
<proof prover="1" timelimit="1"><result status="valid" time="0.15"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.473.0.0.0.2" proved="true">
<proof prover="1" timelimit="1"><result status="valid" time="0.28"/></proof>
<proof prover="1" timelimit="1"><result status="valid" time="0.26"/></proof>
</goal>
</transf>
</goal>
......
......@@ -446,7 +446,7 @@
<goal name="VC backtrack.40" expl="postcondition" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="VC backtrack.40.0" expl="postcondition" proved="true">
<proof prover="0" memlimit="2000"><result status="valid" time="0.78"/></proof>
<proof prover="0" memlimit="2000"><result status="valid" time="1.08"/></proof>
</goal>
</transf>
</goal>
......
......@@ -255,7 +255,7 @@
<proof prover="0"><result status="valid" time="0.14" steps="73"/></proof>
</goal>
<goal name="VC bound_depth_of_fo_term_in_fo_formula_nonnegative.9" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.16" steps="29"/></proof>
<proof prover="0"><result status="valid" time="0.04" steps="29"/></proof>
</goal>
<goal name="VC bound_depth_of_fo_term_in_fo_formula_nonnegative.10" expl="variant decrease" proved="true">
<proof prover="0"><result status="valid" time="0.14" steps="78"/></proof>
......@@ -487,7 +487,7 @@
<proof prover="0"><result status="valid" time="0.05" steps="13"/></proof>
</goal>
<goal name="VC bind_var_symbol_in_fo_formula.16" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.16" steps="13"/></proof>
<proof prover="0"><result status="valid" time="0.04" steps="13"/></proof>
</goal>
<goal name="VC bind_var_symbol_in_fo_formula.17" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.11" steps="13"/></proof>
......@@ -671,7 +671,7 @@
<proof prover="0"><result status="valid" time="0.08" steps="46"/></proof>
</goal>
<goal name="VC bind_var_fo_term_in_fo_formula.20" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.18" steps="77"/></proof>
<proof prover="0"><result status="valid" time="0.06" steps="77"/></proof>
</goal>
<goal name="VC bind_var_fo_term_in_fo_formula.21" expl="variant decrease" proved="true">
<proof prover="0"><result status="valid" time="0.14" steps="120"/></proof>
......@@ -864,7 +864,7 @@
<proof prover="0"><result status="valid" time="0.14" steps="20"/></proof>
</goal>
<goal name="VC unbind_var_symbol_in_fo_formula.32" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.17" steps="70"/></proof>
<proof prover="0"><result status="valid" time="0.05" steps="70"/></proof>
</goal>
<goal name="VC unbind_var_symbol_in_fo_formula.33" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.16" steps="98"/></proof>
......@@ -918,7 +918,7 @@
<proof prover="0"><result status="valid" time="0.14" steps="20"/></proof>
</goal>
<goal name="VC unbind_var_symbol_in_fo_formula.50" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.16" steps="70"/></proof>
<proof prover="0"><result status="valid" time="0.04" steps="70"/></proof>
</goal>
<goal name="VC unbind_var_symbol_in_fo_formula.51" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.10" steps="98"/></proof>
......@@ -1219,7 +1219,7 @@
<proof prover="0"><result status="valid" time="0.15" steps="19"/></proof>
</goal>
<goal name="VC unbind_var_fo_term_in_fo_formula.66" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.17" steps="20"/></proof>
<proof prover="0"><result status="valid" time="0.05" steps="20"/></proof>
</goal>
<goal name="VC unbind_var_fo_term_in_fo_formula.67" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.13" steps="20"/></proof>
......@@ -1258,7 +1258,7 @@
<proof prover="0"><result status="valid" time="0.13" steps="20"/></proof>
</goal>
<goal name="VC unbind_var_fo_term_in_fo_formula.79" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.16" steps="20"/></proof>
<proof prover="0"><result status="valid" time="0.04" steps="20"/></proof>
</goal>
<goal name="VC unbind_var_fo_term_in_fo_formula.80" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.12" steps="20"/></proof>
......@@ -1292,7 +1292,7 @@
<proof prover="0" timelimit="5"><result status="valid" time="0.15" steps="14"/></proof>
</goal>
<goal name="VC subst_base_symbol_in_fo_formula.3" expl="variant decrease" proved="true">
<proof prover="0" timelimit="5"><result status="valid" time="0.17" steps="22"/></proof>
<proof prover="0" timelimit="5"><result status="valid" time="0.05" steps="22"/></proof>
</goal>
<goal name="VC subst_base_symbol_in_fo_formula.4" expl="precondition" proved="true">
<proof prover="0" timelimit="5"><result status="valid" time="0.05" steps="15"/></proof>
......@@ -1485,7 +1485,7 @@
<proof prover="0" timelimit="5"><result status="valid" time="0.14" steps="13"/></proof>
</goal>
<goal name="VC subst_base_fo_term_in_fo_formula.1" expl="assertion" proved="true">
<proof prover="0" timelimit="5"><result status="valid" time="0.17" steps="65"/></proof>
<proof prover="0" timelimit="5"><result status="valid" time="0.05" steps="65"/></proof>
</goal>
<goal name="VC subst_base_fo_term_in_fo_formula.2" expl="assertion" proved="true">
<proof prover="0" timelimit="5"><result status="valid" time="0.14" steps="15"/></proof>
......@@ -2303,7 +2303,7 @@
<proof prover="0" timelimit="5"><result status="valid" time="0.10" steps="138"/></proof>
</goal>
<goal name="VC destruct_fo_formula.19.3" expl="assertion" proved="true">
<proof prover="0" timelimit="5"><result status="valid" time="0.18" steps="38"/></proof>
<proof prover="0" timelimit="5"><result status="valid" time="0.06" steps="38"/></proof>
</goal>
<goal name="VC destruct_fo_formula.19.4" expl="assertion" proved="true">
<proof prover="0" timelimit="5"><result status="valid" time="0.10" steps="146"/></proof>
......@@ -2334,7 +2334,7 @@
<proof prover="0" timelimit="5"><result status="valid" time="0.17" steps="38"/></proof>
</goal>
<goal name="VC destruct_fo_formula.23.4" expl="assertion" proved="true">
<proof prover="0" timelimit="5"><result status="valid" time="0.19" steps="132"/></proof>
<proof prover="0" timelimit="5"><result status="valid" time="0.06" steps="132"/></proof>
</goal>
<goal name="VC destruct_fo_formula.23.5" expl="assertion" proved="true">
<proof prover="0" timelimit="5"><result status="valid" time="0.28" steps="662"/></proof>
......@@ -2814,7 +2814,7 @@
<proof prover="0"><result status="valid" time="0.05" steps="21"/></proof>
</goal>
<goal name="VC destruct_fo_formula.166" expl="unreachable point" proved="true">
<proof prover="0"><result status="valid" time="0.17" steps="21"/></proof>
<proof prover="0"><result status="valid" time="0.05" steps="21"/></proof>
</goal>
<goal name="VC destruct_fo_formula.167" expl="unreachable point" proved="true">
<proof prover="0"><result status="valid" time="0.08" steps="23"/></proof>
......
......@@ -526,7 +526,7 @@
<proof prover="0"><result status="valid" time="0.16" steps="18"/></proof>
</goal>
<goal name="VC construct_fo_formula_list.24" expl="assertion" proved="true">
<proof prover="1"><result status="valid" time="0.26"/></proof>
<proof prover="1"><result status="valid" time="0.13"/></proof>
</goal>
<goal name="VC construct_fo_formula_list.25" expl="precondition" proved="true">
<proof prover="0" timelimit="1"><result status="valid" time="0.11" steps="8"/></proof>
......
......@@ -166,10 +166,10 @@
<proof prover="1"><result status="valid" time="0.18" steps="41"/></proof>
</goal>
<goal name="VC construct_tableau.7" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.19" steps="45"/></proof>
<proof prover="1"><result status="valid" time="0.07" steps="45"/></proof>
</goal>
<goal name="VC construct_tableau.8" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.07" steps="45"/></proof>
<proof prover="1"><result status="valid" time="0.19" steps="45"/></proof>
</goal>
<goal name="VC construct_tableau.9" expl="assertion" proved="true">
<proof prover="1"><result status="valid" time="0.15" steps="90"/></proof>
......@@ -341,7 +341,7 @@
<proof prover="1"><result status="valid" time="0.08" steps="87"/></proof>
</goal>
<goal name="VC destruct_tableau.18" expl="assertion" proved="true">
<proof prover="1"><result status="valid" time="0.19" steps="35"/></proof>
<proof prover="1"><result status="valid" time="0.07" steps="35"/></proof>
</goal>
<goal name="VC destruct_tableau.19" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.18" steps="22"/></proof>
......@@ -525,7 +525,7 @@
<proof prover="1"><result status="valid" time="0.06" steps="14"/></proof>
</goal>
<goal name="VC nlsubst_fo_term_in_tableau.5" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.18" steps="31"/></proof>
<proof prover="1"><result status="valid" time="0.06" steps="31"/></proof>
</goal>