Commit 19a6fb9e authored by Andrei Paskevich's avatar Andrei Paskevich

update obsolete sessions

parent 747ee656
......@@ -20,10 +20,10 @@
<goal name="size_left.0" proved="true">
<transf name="destruct_alg" proved="true" arg1="t">
<goal name="size_left.0.0" 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="size_left.0.1" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
......
......@@ -782,7 +782,7 @@
<proof prover="7"><result status="valid" time="0.02" steps="21"/></proof>
</goal>
<goal name="VC enum.62" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="1.13"/></proof>
<proof prover="4"><result status="valid" time="0.90"/></proof>
</goal>
<goal name="VC enum.63" expl="index in array bounds" proved="true">
<proof prover="9"><result status="valid" time="0.39"/></proof>
......@@ -834,7 +834,7 @@
<proof prover="7"><result status="valid" time="0.18" steps="167"/></proof>
</goal>
<goal name="VC enum.76" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="1.82"/></proof>
<proof prover="4"><result status="valid" time="1.15"/></proof>
</goal>
<goal name="VC enum.77" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.07"/></proof>
......@@ -844,7 +844,7 @@
<proof prover="9"><result status="valid" time="0.61"/></proof>
</goal>
<goal name="VC enum.79" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="1.53"/></proof>
<proof prover="0"><result status="valid" time="1.14"/></proof>
<proof prover="4"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="VC enum.80" expl="precondition" proved="true">
......
......@@ -23,7 +23,7 @@
<proof prover="1"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
<goal name="NumOfDummy.VC numof_eq" expl="VC for numof_eq" proved="true">
<proof prover="2"><result status="valid" time="4.82"/></proof>
<proof prover="2"><result status="valid" time="3.57"/></proof>
</goal>
<goal name="NumOfDummy.VC dummy_const" expl="VC for dummy_const" proved="true">
<proof prover="1"><result status="valid" time="0.10" steps="251"/></proof>
......@@ -118,7 +118,7 @@
</transf>
</goal>
<goal name="VC mem" expl="VC for mem" proved="true">
<proof prover="2"><result status="valid" time="1.98"/></proof>
<proof prover="2"><result status="valid" time="1.59"/></proof>
</goal>
<goal name="VC resize" expl="VC for resize" proved="true">
<transf name="split_goal_right" proved="true" >
......@@ -144,7 +144,7 @@
<proof prover="1"><result status="valid" time="0.03" steps="80"/></proof>
</goal>
<goal name="VC resize.7" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="2.82"/></proof>
<proof prover="2"><result status="valid" time="2.03"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC resize.8" expl="index in array bounds" proved="true">
......@@ -252,7 +252,7 @@
<proof prover="1"><result status="valid" time="0.01" steps="21"/></proof>
</goal>
<goal name="VC add.6" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.35"/></proof>
<proof prover="3"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC add.7" expl="type invariant" proved="true">
<proof prover="7"><result status="valid" time="0.06"/></proof>
......@@ -353,7 +353,7 @@
</transf>
</goal>
<goal name="VC copy" expl="VC for copy" proved="true">
<proof prover="2"><result status="valid" time="3.00"/></proof>
<proof prover="2"><result status="valid" time="2.03"/></proof>
</goal>
<goal name="VC find_dummy" expl="VC for find_dummy" proved="true">
<proof prover="1"><result status="valid" time="0.42" steps="1062"/></proof>
......@@ -581,7 +581,7 @@
</goal>
<goal name="VC remove.25" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.16"/></proof>
<proof prover="3"><result status="valid" time="1.26"/></proof>
<proof prover="3"><result status="valid" time="0.25"/></proof>
</goal>
</transf>
</goal>
......
......@@ -6,8 +6,6 @@
<prover id="4" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="11" name="Alt-Ergo" version="1.30" timelimit="11" steplimit="0" memlimit="1000"/>
<file name="../mergesort_array.mlw" proved="true">
<theory name="Elt" proved="true">
</theory>
<theory name="Merge" proved="true">
<goal name="VC merge" expl="VC for merge" proved="true">
<transf name="split_goal_right" proved="true" >
......
......@@ -46,7 +46,7 @@
<proof prover="2"><result status="valid" time="0.04" steps="95"/></proof>
</goal>
<goal name="VC resize_for.5" expl="assertion" proved="true">
<proof prover="6"><result status="valid" time="1.01"/></proof>
<proof prover="6"><result status="valid" time="0.72"/></proof>
</goal>
<goal name="VC resize_for.6" expl="postcondition" proved="true">
<transf name="inline_goal" proved="true" >
......@@ -62,7 +62,7 @@
<proof prover="6"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC resize_for.6.0.3" expl="VC for resize_for" proved="true">
<proof prover="1"><result status="valid" time="2.55"/></proof>
<proof prover="1"><result status="valid" time="1.96"/></proof>
</goal>
</transf>
</goal>
......@@ -201,13 +201,13 @@
<goal name="VC iadd.5.0.0" expl="assertion" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC iadd.5.0.0.0" expl="VC for iadd" proved="true">
<proof prover="1"><result status="valid" time="0.74"/></proof>
<proof prover="1"><result status="valid" time="0.46"/></proof>
</goal>
<goal name="VC iadd.5.0.0.1" expl="VC for iadd" proved="true">
<proof prover="2"><result status="valid" time="0.03" steps="24"/></proof>
</goal>
<goal name="VC iadd.5.0.0.2" expl="VC for iadd" proved="true">
<proof prover="1"><result status="valid" time="0.73"/></proof>
<proof prover="1"><result status="valid" time="0.45"/></proof>
</goal>
</transf>
</goal>
......@@ -396,11 +396,7 @@
<proof prover="6"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="VC backtrack.20" expl="postcondition" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="VC backtrack.20.0" expl="postcondition" proved="true">
<proof prover="0" memlimit="2000"><result status="valid" time="2.29"/></proof>
</goal>
</transf>
<proof prover="1"><result status="valid" time="0.43"/></proof>
</goal>
<goal name="VC backtrack.21" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.07" steps="75"/></proof>
......@@ -460,7 +456,11 @@
<proof prover="1"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC backtrack.40" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.43"/></proof>
<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>
</goal>
</transf>
</goal>
<goal name="VC backtrack.41" expl="index in array bounds" proved="true">
<proof prover="2"><result status="valid" time="0.04" steps="30"/></proof>
......@@ -577,7 +577,7 @@
<proof prover="2"><result status="valid" time="0.04" steps="48"/></proof>
</goal>
<goal name="VC backtrack.78" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.13" steps="42"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="42"/></proof>
</goal>
<goal name="VC backtrack.79" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.12"/></proof>
......
......@@ -33,13 +33,13 @@
<proof prover="6"><result status="valid" time="0.13" steps="11"/></proof>
</goal>
<goal name="VC formula_semantic_subst_commutation.1" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="1.48"/></proof>
<proof prover="2"><result status="valid" time="1.15"/></proof>
</goal>
<goal name="VC formula_semantic_subst_commutation.2" expl="variant decrease" proved="true">
<proof prover="6"><result status="valid" time="0.10" steps="11"/></proof>
</goal>
<goal name="VC formula_semantic_subst_commutation.3" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="1.54"/></proof>
<proof prover="2"><result status="valid" time="1.17"/></proof>
</goal>
<goal name="VC formula_semantic_subst_commutation.4" expl="variant decrease" proved="true">
<proof prover="6"><result status="valid" time="0.13" steps="28"/></proof>
......@@ -57,7 +57,7 @@
<proof prover="6"><result status="valid" time="0.13" steps="9"/></proof>
</goal>
<goal name="VC formula_semantic_subst_commutation.9" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="1.66"/></proof>
<proof prover="2"><result status="valid" time="0.86"/></proof>
</goal>
<goal name="VC formula_semantic_subst_commutation.10" expl="assertion" proved="true">
<proof prover="6"><result status="valid" time="0.08" steps="18"/></proof>
......@@ -66,7 +66,7 @@
<proof prover="6"><result status="valid" time="0.09" steps="21"/></proof>
</goal>
<goal name="VC formula_semantic_subst_commutation.12" expl="postcondition" proved="true">
<proof prover="6"><result status="valid" time="0.52" steps="1816"/></proof>
<proof prover="6"><result status="valid" time="0.24" steps="1816"/></proof>
</goal>
<goal name="VC formula_semantic_subst_commutation.13" expl="postcondition" proved="true">
<proof prover="6"><result status="valid" time="0.11" steps="4"/></proof>
......@@ -93,10 +93,10 @@
<proof prover="6"><result status="valid" time="0.14" steps="36"/></proof>
</goal>
<goal name="VC formula_list_conj_semantic_subst_commutation" expl="VC for formula_list_conj_semantic_subst_commutation" proved="true">
<proof prover="6"><result status="valid" time="0.22" steps="379"/></proof>
<proof prover="6"><result status="valid" time="0.08" steps="379"/></proof>
</goal>
<goal name="VC formula_list_disj_semantic_subst_commutation" expl="VC for formula_list_disj_semantic_subst_commutation" proved="true">
<proof prover="6"><result status="valid" time="0.21" steps="332"/></proof>
<proof prover="6"><result status="valid" time="0.08" steps="332"/></proof>
</goal>
<goal name="VC formula_list_conj_semantic_term_subst_commutation" expl="VC for formula_list_conj_semantic_term_subst_commutation" proved="true">
<proof prover="6"><result status="valid" time="0.15" steps="54"/></proof>
......@@ -105,7 +105,7 @@
<proof prover="6"><result status="valid" time="0.14" steps="54"/></proof>
</goal>
<goal name="VC tableau_semantic_subst_commutation" expl="VC for tableau_semantic_subst_commutation" proved="true">
<proof prover="6"><result status="valid" time="0.64" steps="1090"/></proof>
<proof prover="6"><result status="valid" time="0.16" steps="1090"/></proof>
</goal>
<goal name="VC tableau_semantic_term_subst_commutation" expl="VC for tableau_semantic_term_subst_commutation" proved="true">
<proof prover="6"><result status="valid" time="0.14" steps="54"/></proof>
......@@ -133,7 +133,7 @@
</transf>
</goal>
<goal name="VC term_list_semantic_depend_only_free_var" expl="VC for term_list_semantic_depend_only_free_var" proved="true">
<proof prover="6"><result status="valid" time="0.54" steps="756"/></proof>
<proof prover="6"><result status="valid" time="0.34" steps="756"/></proof>
</goal>
<goal name="VC formula_semantic_depend_only_free_var" expl="VC for formula_semantic_depend_only_free_var" proved="true">
<transf name="split_goal_right" proved="true" >
......@@ -191,7 +191,7 @@
<goal name="VC formula_semantic_depend_only_free_var.17" expl="assertion" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC formula_semantic_depend_only_free_var.17.0" expl="assertion" proved="true">
<proof prover="1"><result status="valid" time="1.49"/></proof>
<proof prover="1"><result status="valid" time="1.19"/></proof>
</goal>
<goal name="VC formula_semantic_depend_only_free_var.17.1" expl="assertion" proved="true">
<proof prover="6"><result status="valid" time="0.08" steps="11"/></proof>
......@@ -252,10 +252,10 @@
<proof prover="6" timelimit="1"><result status="valid" time="0.10" steps="9"/></proof>
</goal>
<goal name="VC formula_semantic_depend_only_free_var.18.14" expl="postcondition" proved="true">
<proof prover="7" timelimit="5" memlimit="2000"><result status="valid" time="3.29"/></proof>
<proof prover="7" timelimit="5" memlimit="2000"><result status="valid" time="1.72"/></proof>
</goal>
<goal name="VC formula_semantic_depend_only_free_var.18.15" expl="postcondition" proved="true">
<proof prover="7" timelimit="5" memlimit="2000"><result status="valid" time="3.50"/></proof>
<proof prover="7" timelimit="5" memlimit="2000"><result status="valid" time="1.70"/></proof>
</goal>
</transf>
</goal>
......@@ -279,29 +279,29 @@
<proof prover="6" timelimit="1"><result status="valid" time="0.10" steps="26"/></proof>
</goal>
<goal name="VC formula_list_conj_semantic_depend_only_free_var.3" expl="precondition" proved="true">
<proof prover="7"><result status="valid" time="1.24"/></proof>
<proof prover="7"><result status="valid" time="0.73"/></proof>
</goal>
<goal name="VC formula_list_conj_semantic_depend_only_free_var.4" expl="precondition" proved="true">
<proof prover="7"><result status="valid" time="1.26"/></proof>
<proof prover="7"><result status="valid" time="0.78"/></proof>
</goal>
<goal name="VC formula_list_conj_semantic_depend_only_free_var.5" expl="postcondition" proved="true">
<proof prover="7"><result status="valid" time="1.49"/></proof>
<proof prover="7"><result status="valid" time="0.59"/></proof>
</goal>
<goal name="VC formula_list_conj_semantic_depend_only_free_var.6" expl="postcondition" proved="true">
<proof prover="7"><result status="valid" time="1.54"/></proof>
<proof prover="7"><result status="valid" time="0.62"/></proof>
</goal>
</transf>
</goal>
<goal name="VC formula_list_disj_semantic_depend_only_free_var" expl="VC for formula_list_disj_semantic_depend_only_free_var" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="VC formula_list_disj_semantic_depend_only_free_var.0" expl="precondition" proved="true">
<proof prover="6" timelimit="1"><result status="valid" time="0.22" steps="18"/></proof>
<proof prover="6" timelimit="1"><result status="valid" time="0.04" steps="18"/></proof>
</goal>
<goal name="VC formula_list_disj_semantic_depend_only_free_var.1" expl="precondition" proved="true">
<proof prover="6" timelimit="1"><result status="valid" time="0.35" steps="18"/></proof>
<proof prover="6" timelimit="1"><result status="valid" time="0.05" steps="18"/></proof>
</goal>
<goal name="VC formula_list_disj_semantic_depend_only_free_var.2" expl="variant decrease" proved="true">
<proof prover="6" timelimit="1"><result status="valid" time="0.23" steps="26"/></proof>
<proof prover="6" timelimit="1"><result status="valid" time="0.06" steps="26"/></proof>
</goal>
<goal name="VC formula_list_disj_semantic_depend_only_free_var.3" expl="precondition" proved="true">
<proof prover="6" timelimit="1"><result status="valid" time="0.09" steps="20"/></proof>
......@@ -310,18 +310,18 @@
<proof prover="6" timelimit="1"><result status="valid" time="0.10" steps="20"/></proof>
</goal>
<goal name="VC formula_list_disj_semantic_depend_only_free_var.5" expl="postcondition" proved="true">
<proof prover="7"><result status="valid" time="0.94"/></proof>
<proof prover="7"><result status="valid" time="0.62"/></proof>
</goal>
<goal name="VC formula_list_disj_semantic_depend_only_free_var.6" expl="postcondition" proved="true">
<proof prover="7"><result status="valid" time="1.42"/></proof>
<proof prover="7"><result status="valid" time="0.66"/></proof>
</goal>
</transf>
</goal>
<goal name="VC formula_list_conj_semantic_other_def" expl="VC for formula_list_conj_semantic_other_def" proved="true">
<proof prover="6"><result status="valid" time="0.20" steps="197"/></proof>
<proof prover="6"><result status="valid" time="0.06" steps="197"/></proof>
</goal>
<goal name="VC formula_list_disj_semantic_other_def" expl="VC for formula_list_disj_semantic_other_def" proved="true">
<proof prover="6"><result status="valid" time="0.21" steps="179"/></proof>
<proof prover="6"><result status="valid" time="0.07" steps="179"/></proof>
</goal>
<goal name="VC skolem_model_transformer" expl="VC for skolem_model_transformer" proved="true">
<transf name="split_goal_right" proved="true" >
......@@ -346,16 +346,16 @@
<proof prover="6"><result status="valid" time="0.08" steps="47"/></proof>
</goal>
<goal name="VC skolem_model_transformer.0.6" expl="assertion" proved="true">
<proof prover="6"><result status="valid" time="0.20" steps="53"/></proof>
<proof prover="6"><result status="valid" time="0.06" steps="53"/></proof>
</goal>
<goal name="VC skolem_model_transformer.0.7" expl="assertion" proved="true">
<proof prover="6"><result status="valid" time="0.32" steps="91"/></proof>
<proof prover="6"><result status="valid" time="0.06" steps="91"/></proof>
</goal>
<goal name="VC skolem_model_transformer.0.8" expl="assertion" proved="true">
<proof prover="6"><result status="valid" time="0.27" steps="45"/></proof>
<proof prover="6"><result status="valid" time="0.05" steps="45"/></proof>
</goal>
<goal name="VC skolem_model_transformer.0.9" expl="assertion" proved="true">
<proof prover="6"><result status="valid" time="0.18" steps="13"/></proof>
<proof prover="6"><result status="valid" time="0.05" steps="13"/></proof>
</goal>
<goal name="VC skolem_model_transformer.0.10" expl="assertion" proved="true">
<proof prover="6"><result status="valid" time="0.07" steps="12"/></proof>
......@@ -370,26 +370,26 @@
<proof prover="6"><result status="valid" time="0.12" steps="73"/></proof>
</goal>
<goal name="VC skolem_model_transformer.0.14" expl="assertion" proved="true">
<proof prover="6"><result status="valid" time="0.19" steps="77"/></proof>
<proof prover="6"><result status="valid" time="0.07" steps="77"/></proof>
</goal>
<goal name="VC skolem_model_transformer.0.15" expl="assertion" proved="true">
<proof prover="6"><result status="valid" time="0.08" steps="15"/></proof>
</goal>
<goal name="VC skolem_model_transformer.0.16" expl="assertion" proved="true">
<proof prover="1"><result status="valid" time="2.83"/></proof>
<proof prover="1"><result status="valid" time="1.95"/></proof>
</goal>
</transf>
</goal>
<goal name="VC skolem_model_transformer.1" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="2.09"/></proof>
<proof prover="2"><result status="valid" time="4.06"/></proof>
<proof prover="1"><result status="valid" time="1.39"/></proof>
<proof prover="2"><result status="valid" time="2.19"/></proof>
</goal>
<goal name="VC skolem_model_transformer.2" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="4.16"/></proof>
<proof prover="3"><result status="valid" time="1.30"/></proof>
<proof prover="2"><result status="valid" time="2.19"/></proof>
<proof prover="3"><result status="valid" time="0.63"/></proof>
</goal>
<goal name="VC skolem_model_transformer.3" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="1.44"/></proof>
<proof prover="3"><result status="valid" time="0.58"/></proof>
</goal>
</transf>
</goal>
......
This diff is collapsed.
......@@ -23,7 +23,7 @@
<goal name="VC main.3" expl="assertion" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC main.3.0" expl="VC for main" proved="true">
<proof prover="1"><result status="valid" time="0.62"/></proof>
<proof prover="1"><result status="valid" time="0.45"/></proof>
</goal>
<goal name="VC main.3.1" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.15" steps="53"/></proof>
......@@ -43,7 +43,7 @@
<proof prover="0"><result status="valid" time="0.15" steps="41"/></proof>
</goal>
<goal name="VC main.8" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.24" steps="24"/></proof>
<proof prover="0"><result status="valid" time="0.10" steps="24"/></proof>
</goal>
<goal name="VC main.9" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.14" steps="56"/></proof>
......@@ -52,7 +52,7 @@
<proof prover="0"><result status="valid" time="0.17" steps="132"/></proof>
</goal>
<goal name="VC main.11" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.24" steps="64"/></proof>
<proof prover="0"><result status="valid" time="0.10" steps="64"/></proof>
</goal>
<goal name="VC main.12" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.12" steps="26"/></proof>
......@@ -61,13 +61,13 @@
<proof prover="0"><result status="valid" time="0.12" steps="26"/></proof>
</goal>
<goal name="VC main.14" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.26" steps="26"/></proof>
<proof prover="0"><result status="valid" time="0.10" steps="26"/></proof>
</goal>
<goal name="VC main.15" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.27" steps="69"/></proof>
<proof prover="0"><result status="valid" time="0.11" steps="69"/></proof>
</goal>
<goal name="VC main.16" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.26" steps="43"/></proof>
<proof prover="0"><result status="valid" time="0.11" steps="43"/></proof>
</goal>
<goal name="VC main.17" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.14" steps="43"/></proof>
......
......@@ -7,34 +7,34 @@
<file name="../ProverTest.mlw" proved="true">
<theory name="Impl" proved="true">
<goal name="VC imply" expl="VC for imply" proved="true">
<proof prover="3"><result status="valid" time="0.40" steps="1195"/></proof>
<proof prover="3"><result status="valid" time="0.24" steps="1195"/></proof>
</goal>
<goal name="VC equiv" expl="VC for equiv" proved="true">
<proof prover="3"><result status="valid" time="0.60" steps="2387"/></proof>
</goal>
<goal name="VC drinker" expl="VC for drinker" proved="true">
<proof prover="3"><result status="valid" time="1.91" steps="6811"/></proof>
<proof prover="3"><result status="valid" time="1.30" steps="6811"/></proof>
</goal>
<goal name="VC group" expl="VC for group" proved="true">
<proof prover="1"><result status="valid" time="0.63"/></proof>
<proof prover="1"><result status="valid" time="0.38"/></proof>
</goal>
<goal name="VC bidon1" expl="VC for bidon1" proved="true">
<proof prover="3"><result status="valid" time="0.56" steps="1609"/></proof>
<proof prover="3"><result status="valid" time="0.36" steps="1609"/></proof>
</goal>
<goal name="VC bidon2" expl="VC for bidon2" proved="true">
<proof prover="3"><result status="valid" time="2.35" steps="6730"/></proof>
<proof prover="3"><result status="valid" time="1.40" steps="6730"/></proof>
</goal>
<goal name="VC bidon3" expl="VC for bidon3" proved="true">
<proof prover="1"><result status="valid" time="0.66"/></proof>
<proof prover="1"><result status="valid" time="0.32"/></proof>
</goal>
<goal name="VC bidon4" expl="VC for bidon4" proved="true">
<proof prover="1"><result status="valid" time="0.48"/></proof>
<proof prover="1"><result status="valid" time="0.33"/></proof>
</goal>
<goal name="VC pierce" expl="VC for pierce" proved="true">
<proof prover="3"><result status="valid" time="1.09" steps="3645"/></proof>
<proof prover="3"><result status="valid" time="0.75" steps="3645"/></proof>
</goal>
<goal name="VC generate" expl="VC for generate" proved="true">
<proof prover="3"><result status="valid" time="0.45" steps="911"/></proof>
<proof prover="3"><result status="valid" time="0.23" steps="911"/></proof>
</goal>
<goal name="VC zenon5" expl="VC for zenon5" proved="true">
<proof prover="1"><result status="valid" time="0.31"/></proof>
......
This diff is collapsed.
......@@ -5,8 +5,6 @@
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.4" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../remove_duplicate.mlw" proved="true">
<theory name="Spec" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="RemoveDuplicateQuadratic" proved="true">
<goal name="VC test_appears" expl="VC for test_appears" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="65"/></proof>
......
......@@ -4,10 +4,6 @@
<why3session shape_version="4">
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../remove_duplicate_hash.mlw" proved="true">
<theory name="Spec" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="MutableSet" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="RemoveDuplicate" proved="true">
<goal name="VC remove_duplicate" expl="VC for remove_duplicate" proved="true">
<transf name="split_goal_right" proved="true" >
......