Commit 0ee272e6 authored by Andrei Paskevich's avatar Andrei Paskevich

update sessions

parent 3438e2db
......@@ -2,30 +2,30 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.95.1" timelimit="5" memlimit="1000"/>
<prover id="0" name="Alt-Ergo" version="0.95.1" timelimit="5" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
<prover id="2" name="Z3" version="3.2" timelimit="5" memlimit="1000"/>
<file name="../add_list.mlw" expanded="true">
<theory name="SumList" sum="3880e7768b9fbb987ee1c04cefb36cde">
<theory name="SumList" sum="f3a2d317efe6eddf41eac0ece9e8d2e4">
</theory>
<theory name="AddListRec" sum="0e8ef89f2db251f08e2ead111b715f73" expanded="true">
<theory name="AddListRec" sum="5643b575103f0531dc30435fcf1c0530" expanded="true">
<goal name="WP_parameter sum" expl="VC for sum" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter main" expl="VC for main" expanded="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
</theory>
<theory name="AddListImp" sum="e32a291b70f70653cf52bd57a896af4d" expanded="true">
<theory name="AddListImp" sum="147c5200701a0989a7074713bedae134" expanded="true">
<goal name="WP_parameter sum" expl="VC for sum" expanded="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter main" expl="VC for main" expanded="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
</theory>
......
......@@ -7,7 +7,7 @@
<prover id="2" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<prover id="3" name="Vampire" version="0.6" timelimit="6" memlimit="1000"/>
<file name="../algo63.mlw" expanded="true">
<theory name="Algo63" sum="39524f328d620876c4043a001b22f3de" expanded="true">
<theory name="Algo63" sum="b6665076843efa8c48db39e5c86d119a" expanded="true">
<goal name="WP_parameter exchange" expl="VC for exchange">
<proof prover="2"><result status="valid" time="0.05"/></proof>
</goal>
......@@ -491,36 +491,11 @@
<goal name="WP_parameter partition.4" expl="4. postcondition">
<proof prover="1"><result status="valid" time="1.92"/></proof>
<metas>
<ts_pos name="real" arity="0" id="2"
ip_theory="BuiltIn">
<ip_library name="why3"/>
<ip_qualid name="real"/>
</ts_pos>
<ts_pos name="bool" arity="0" id="3"
ip_theory="Bool">
<ip_library name="why3"/>
<ip_qualid name="bool"/>
</ts_pos>
<ts_pos name="tuple0" arity="0" id="20"
ip_theory="Tuple0">
<ip_library name="why3"/>
<ip_qualid name="tuple0"/>
</ts_pos>
<ts_pos name="unit" arity="0" id="21"
ip_theory="Unit">
<ip_library name="why3"/>
<ip_qualid name="unit"/>
</ts_pos>
<ts_pos name="ref" arity="1" id="2336"
ip_theory="Ref">
<ip_library name="ref"/>
<ip_qualid name="ref"/>
</ts_pos>
<ls_pos name="infix =" id="10"
ip_theory="BuiltIn">
<ip_library name="why3"/>
<ip_qualid name="infix ="/>
</ls_pos>
<ls_pos name="zero" id="288"
ip_theory="Int">
<ip_library name="int"/>
......@@ -765,9 +740,6 @@
<ip_library name="map"/>
<ip_qualid name="occ_pos"/>
</pr_pos>
<meta name="remove_logic">
<meta_arg_ls id="10"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="288"/>
</meta>
......@@ -909,18 +881,6 @@
<meta name="remove_prop">
<meta_arg_pr id="3001"/>
</meta>
<meta name="remove_type">
<meta_arg_ts id="2"/>
</meta>
<meta name="remove_type">
<meta_arg_ts id="3"/>
</meta>
<meta name="remove_type">
<meta_arg_ts id="20"/>
</meta>
<meta name="remove_type">
<meta_arg_ts id="21"/>
</meta>
<meta name="remove_type">
<meta_arg_ts id="2336"/>
</meta>
......
......@@ -4,7 +4,7 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<file name="../algo64.mlw" expanded="true">
<theory name="Algo64" sum="103ff1827edf820d54c612b484b267e3" expanded="true">
<theory name="Algo64" sum="3c5834bf498c814018fd7764cc3f7fe7" expanded="true">
<goal name="WP_parameter quicksort" expl="VC for quicksort" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter quicksort.1" expl="1. precondition">
......
......@@ -4,7 +4,7 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<file name="../algo65.mlw" expanded="true">
<theory name="Algo65" sum="a79e01fdec32b266dcbb4b6cfabd8ee7" expanded="true">
<theory name="Algo65" sum="0b5f4012ece51782edee31f59e5f2271" expanded="true">
<goal name="WP_parameter find" expl="VC for find" expanded="true">
<transf name="split_goal" expanded="true">
<goal name="WP_parameter find.1" expl="1. precondition">
......@@ -103,7 +103,7 @@
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter find.28" expl="28. postcondition">
<proof prover="0"><result status="valid" time="0.32"/></proof>
<proof prover="0"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="WP_parameter find.29" expl="29. postcondition">
<proof prover="0"><result status="valid" time="0.02"/></proof>
......
......@@ -4,7 +4,7 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.95.2" timelimit="6" memlimit="1000"/>
<file name="../all_distinct.mlw" expanded="true">
<theory name="AllDistinct" sum="cdb61a5905b9fa18eb71d98750f2c5ce" expanded="true">
<theory name="AllDistinct" sum="cfde60d3babd38652ded2118a56af1b2" expanded="true">
<goal name="WP_parameter all_distinct" expl="VC for all_distinct" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter all_distinct.1" expl="1. array creation size" expanded="true">
......
......@@ -6,7 +6,7 @@
<prover id="1" name="Z3" version="3.2" timelimit="5" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<file name="../arm.mlw" expanded="true">
<theory name="M" sum="605769bd5022610ed3b9e18df3b7e809" expanded="true">
<theory name="M" sum="3f27a6f28f257d6bf1582b31abcf4954" expanded="true">
<goal name="WP_parameter insertion_sort" expl="VC for insertion_sort">
<transf name="split_goal_wp">
<goal name="WP_parameter insertion_sort.1" expl="1. loop invariant init">
......@@ -57,9 +57,9 @@
</transf>
</goal>
</theory>
<theory name="ARM" sum="6fdfd89191311a6afa067259cb777bdf" expanded="true">
<theory name="ARM" sum="891ea07eb40eeb5ae28be52ac9b685bc" expanded="true">
</theory>
<theory name="InsertionSortExample" sum="ac3eca2f27a321a7daec35ac3b3866c8" expanded="true">
<theory name="InsertionSortExample" sum="50fb19c04bece76475d571ab9160070b" expanded="true">
<goal name="WP_parameter path_init_l2" expl="VC for path_init_l2">
<proof prover="0" memlimit="1000"><result status="valid" time="0.02"/></proof>
<proof prover="1"><result status="valid" time="0.14"/></proof>
......
......@@ -5,12 +5,12 @@
<prover id="0" name="CVC3" version="2.4.1" timelimit="10" memlimit="0"/>
<prover id="1" name="Alt-Ergo" version="0.95.1" timelimit="10" memlimit="0"/>
<file name="../assigning_meanings_to_programs.mlw">
<theory name="Sum" sum="4c5c970c12a40d8008ac700a67e7b66a" expanded="true">
<theory name="Sum" sum="e1ea7bffe6727627d6719af6bb639449" expanded="true">
<goal name="WP_parameter sum" expl="VC for sum" expanded="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
</theory>
<theory name="Division" sum="156aa84f43774442d62d816ca30a5b75" expanded="true">
<theory name="Division" sum="7d333da7874d94b2efa38ff9a68d6cdb" expanded="true">
<goal name="WP_parameter division" expl="VC for division" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
......
......@@ -7,7 +7,7 @@
<prover id="2" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.3" timelimit="5" memlimit="1000"/>
<file name="../association_list.mlw" expanded="true">
<theory name="Assoc" sum="51b4c11f081064e3b4d325b694706c49">
<theory name="Assoc" sum="ffc1f1f886cca401e3295d48a24cf809">
<goal name="appear_append">
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
......@@ -74,7 +74,7 @@
</transf>
</goal>
</theory>
<theory name="AssocSorted" sum="d893e987157b1d0812b75c65f363bef5" expanded="true">
<theory name="AssocSorted" sum="fa64a1dacec1a0b389a9fa85e2448c1a" expanded="true">
<goal name="Refl">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
......
......@@ -6,12 +6,12 @@
<prover id="1" name="Alt-Ergo" version="0.95.2" timelimit="2" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.3" timelimit="2" memlimit="0"/>
<file name="../avl.mlw">
<theory name="SelectionTypes" sum="889610463ddab805c0b8619b38c84a3f">
<theory name="SelectionTypes" sum="cccf360bc09a887b7b6466255a36df93">
<goal name="rebuild_aternative_def">
<proof prover="1" memlimit="0"><result status="valid" time="0.07"/></proof>
</goal>
</theory>
<theory name="AVL" sum="d9afb554df4681295c3ff2120867d09a">
<theory name="AVL" sum="b06f96c3605f40076db787a2d22432b0">
<goal name="assoc">
<proof prover="1" memlimit="0"><result status="valid" time="0.02"/></proof>
</goal>
......
......@@ -4,14 +4,14 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<file name="../monoid.mlw">
<theory name="Monoid" sum="17d1ff16242df7a3b2e7d4292aca9c4c">
<theory name="Monoid" sum="df9c37248338b5a152b2dacc196da8eb">
</theory>
<theory name="MonoidSum" sum="664c08bfadf863f0189070400301b285">
<theory name="MonoidSum" sum="fad19597d32d34cf2fb4f6e0be4b25e8">
<goal name="WP_parameter sum_append" expl="VC for sum_append">
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
</theory>
<theory name="MonoidSumDef" sum="fa955d3a9aa320fff31c6ec120555b0c">
<theory name="MonoidSumDef" sum="cee1e1bb2e0c3faf58b751c0d5f8689c">
<goal name="sum_def_nil">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
......@@ -19,7 +19,7 @@
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
</theory>
<theory name="ComputableMonoid" sum="c2e44e6bbfbd447428a63f1982102329">
<theory name="ComputableMonoid" sum="fb4bf0350f1941fb8154ca8fdf6fabad">
</theory>
</file>
</why3session>
......@@ -4,7 +4,7 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<file name="../preorder.mlw" expanded="true">
<theory name="Full" sum="04f153879aff3c7914e9fbcce574722d" expanded="true">
<theory name="Full" sum="0df41be1fb7bb26bae15dbe14d586fe2" expanded="true">
<goal name="Refl" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
......@@ -21,7 +21,7 @@
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
</theory>
<theory name="TotalFull" sum="3eacffe3af898f23ee229ae1e031e9af" expanded="true">
<theory name="TotalFull" sum="61c9ee6dbbea5bfd91d2f112d248610f" expanded="true">
<goal name="Total" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
......@@ -29,7 +29,7 @@
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
</theory>
<theory name="Computable" sum="79b4e8156a6eaddae8cb167a05ea3621" expanded="true">
<theory name="Computable" sum="ef6a8a7f312f6483dc02c98e04f9a75e" expanded="true">
</theory>
</file>
</why3session>
......@@ -7,7 +7,7 @@
<prover id="2" name="Z3" version="4.3.1" timelimit="5" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<file name="../priority_queue.mlw">
<theory name="PQueue" sum="676f1bd969386fee8625cf44dbec8564">
<theory name="PQueue" sum="43d94f2f459569d40d93b24723828ae5">
<goal name="Trans">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
......@@ -78,31 +78,6 @@
</goal>
<goal name="WP_parameter monoid_sum_is_min.2.3" expl="3. postcondition">
<metas>
<ts_pos name="real" arity="0" id="2"
ip_theory="BuiltIn">
<ip_library name="why3"/>
<ip_qualid name="real"/>
</ts_pos>
<ts_pos name="bool" arity="0" id="3"
ip_theory="Bool">
<ip_library name="why3"/>
<ip_qualid name="bool"/>
</ts_pos>
<ts_pos name="pred" arity="1" id="8"
ip_theory="HighOrd">
<ip_library name="why3"/>
<ip_qualid name="pred"/>
</ts_pos>
<ts_pos name="tuple0" arity="0" id="20"
ip_theory="Tuple0">
<ip_library name="why3"/>
<ip_qualid name="tuple0"/>
</ts_pos>
<ts_pos name="unit" arity="0" id="21"
ip_theory="Unit">
<ip_library name="why3"/>
<ip_qualid name="unit"/>
</ts_pos>
<ts_pos name="split" arity="1" id="4666"
ip_theory="SelectionTypes">
<ip_library name="avl"/>
......@@ -118,11 +93,6 @@
<ip_library name="ref"/>
<ip_qualid name="ref"/>
</ts_pos>
<ts_pos name="tuple3" arity="3" id="7646"
ip_theory="Tuple3">
<ip_library name="why3"/>
<ip_qualid name="tuple3"/>
</ts_pos>
<ts_pos name="t" arity="0" id="8490"
ip_theory="PQueue">
<ip_qualid name="M"/>
......@@ -132,16 +102,6 @@
ip_theory="PQueue">
<ip_qualid name="selector"/>
</ts_pos>
<ls_pos name="infix =" id="10"
ip_theory="BuiltIn">
<ip_library name="why3"/>
<ip_qualid name="infix ="/>
</ls_pos>
<ls_pos name="infix @" id="15"
ip_theory="HighOrd">
<ip_library name="why3"/>
<ip_qualid name="infix @"/>
</ls_pos>
<ls_pos name="zero" id="454"
ip_theory="Int">
<ip_library name="int"/>
......@@ -480,12 +440,6 @@
<ip_qualid name="M"/>
<ip_qualid name="neutral"/>
</pr_pos>
<meta name="remove_logic">
<meta_arg_ls id="10"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="15"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="454"/>
</meta>
......@@ -687,21 +641,6 @@
<meta name="remove_prop">
<meta_arg_pr id="8626"/>
</meta>
<meta name="remove_type">
<meta_arg_ts id="2"/>
</meta>
<meta name="remove_type">
<meta_arg_ts id="3"/>
</meta>
<meta name="remove_type">
<meta_arg_ts id="8"/>
</meta>
<meta name="remove_type">
<meta_arg_ts id="20"/>
</meta>
<meta name="remove_type">
<meta_arg_ts id="21"/>
</meta>
<meta name="remove_type">
<meta_arg_ts id="4666"/>
</meta>
......@@ -711,9 +650,6 @@
<meta name="remove_type">
<meta_arg_ts id="4739"/>
</meta>
<meta name="remove_type">
<meta_arg_ts id="7646"/>
</meta>
<meta name="remove_type">
<meta_arg_ts id="8490"/>
</meta>
......@@ -744,7 +680,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter selected_is_min.1.2" expl="2. postcondition">
<proof prover="3"><result status="valid" time="1.73"/></proof>
<proof prover="3"><result status="valid" time="1.42"/></proof>
</goal>
<goal name="WP_parameter selected_is_min.1.3" expl="3. postcondition">
<proof prover="3"><result status="valid" time="0.03"/></proof>
......@@ -1152,31 +1088,6 @@
</goal>
<goal name="WP_parameter pop_min.3.4" expl="4.">
<metas>
<ts_pos name="real" arity="0" id="2"
ip_theory="BuiltIn">
<ip_library name="why3"/>
<ip_qualid name="real"/>
</ts_pos>
<ts_pos name="bool" arity="0" id="3"
ip_theory="Bool">
<ip_library name="why3"/>
<ip_qualid name="bool"/>
</ts_pos>
<ts_pos name="pred" arity="1" id="8"
ip_theory="HighOrd">
<ip_library name="why3"/>
<ip_qualid name="pred"/>
</ts_pos>
<ts_pos name="unit" arity="0" id="21"
ip_theory="Unit">
<ip_library name="why3"/>
<ip_qualid name="unit"/>
</ts_pos>
<ts_pos name="tuple2" arity="2" id="1170"
ip_theory="Tuple2">
<ip_library name="why3"/>
<ip_qualid name="tuple2"/>
</ts_pos>
<ts_pos name="part_base" arity="1" id="4671"
ip_theory="SelectionTypes">
<ip_library name="avl"/>
......@@ -1187,11 +1098,6 @@
<ip_library name="ref"/>
<ip_qualid name="ref"/>
</ts_pos>
<ts_pos name="tuple3" arity="3" id="7646"
ip_theory="Tuple3">
<ip_library name="why3"/>
<ip_qualid name="tuple3"/>
</ts_pos>
<ts_pos name="t" arity="0" id="8490"
ip_theory="PQueue">
<ip_qualid name="M"/>
......@@ -1215,16 +1121,6 @@
ip_theory="PQueue">
<ip_qualid name="t"/>
</ts_pos>
<ls_pos name="infix =" id="10"
ip_theory="BuiltIn">
<ip_library name="why3"/>
<ip_qualid name="infix ="/>
</ls_pos>
<ls_pos name="infix @" id="15"
ip_theory="HighOrd">
<ip_library name="why3"/>
<ip_qualid name="infix @"/>
</ls_pos>
<ls_pos name="zero" id="454"
ip_theory="Int">
<ip_library name="int"/>
......@@ -1648,12 +1544,6 @@
ip_theory="PQueue">
<ip_qualid name="correction"/>
</pr_pos>
<meta name="remove_logic">
<meta_arg_ls id="10"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="15"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="454"/>
</meta>
......@@ -1906,30 +1796,12 @@
<meta name="remove_prop">
<meta_arg_pr id="11433"/>
</meta>
<meta name="remove_type">
<meta_arg_ts id="2"/>
</meta>
<meta name="remove_type">
<meta_arg_ts id="3"/>
</meta>
<meta name="remove_type">
<meta_arg_ts id="8"/>
</meta>
<meta name="remove_type">
<meta_arg_ts id="21"/>
</meta>
<meta name="remove_type">
<meta_arg_ts id="1170"/>
</meta>
<meta name="remove_type">
<meta_arg_ts id="4671"/>
</meta>
<meta name="remove_type">
<meta_arg_ts id="4739"/>
</meta>
<meta name="remove_type">
<meta_arg_ts id="7646"/>
</meta>
<meta name="remove_type">
<meta_arg_ts id="8490"/>
</meta>
......
......@@ -5,7 +5,7 @@
<prover id="0" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<file name="../ral.mlw">
<theory name="RAL" sum="c2971a890b46469bf12d3271b7ec1242">
<theory name="RAL" sum="b85ea65c6b3b2e84fb0a259ea33ee2c5">
<goal name="assoc">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
......@@ -105,7 +105,7 @@
<proof prover="1"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="WP_parameter set.3" expl="3. postcondition">
<proof prover="1"><result status="valid" time="1.01"/></proof>
<proof prover="1"><result status="valid" time="0.78"/></proof>
</goal>
<goal name="WP_parameter set.4" expl="4. postcondition">
<proof prover="1"><result status="valid" time="0.04"/></proof>
......
......@@ -4,7 +4,7 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<file name="../sorted.mlw">
<theory name="Increasing" sum="bcc64f427a1238869e3e039391cf9ce5">
<theory name="Increasing" sum="9cba90971f4296cb90f0f0657b3d1a6a">
<goal name="smaller_lower_bound">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
......
......@@ -116,7 +116,7 @@
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter selected_part.1.1.1.3" expl="3.">
<proof prover="0" timelimit="5"><result status="valid" time="1.35"/></proof>
<proof prover="0" timelimit="5"><result status="valid" time="1.09"/></proof>
</goal>
<goal name="WP_parameter selected_part.1.1.1.4" expl="4.">
<proof prover="2"><result status="valid" time="0.05"/></proof>
......@@ -155,13 +155,13 @@
<proof prover="2"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="WP_parameter selected_part.2.1.1.5" expl="5. postcondition">
<proof prover="1" timelimit="20"><result status="valid" time="7.44"/></proof>