Commit e761ccdc authored by MARCHE Claude's avatar MARCHE Claude

update sessions

parent 07ae5db7
......@@ -75,17 +75,17 @@
</goal>
</theory>
<theory name="AssocSorted" sum="fa64a1dacec1a0b389a9fa85e2448c1a" expanded="true">
<goal name="Refl">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<goal name="Eq.Refl" expanded="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="Trans">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<goal name="Eq.Trans" expanded="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="Symm">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<goal name="Eq.Symm" expanded="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="Trans">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<goal name="S.O.Trans" expanded="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter increasing_unique" expl="VC for increasing_unique">
<proof prover="2"><result status="valid" time="0.07"/></proof>
......
......@@ -5,18 +5,18 @@
<prover id="0" name="CVC3" version="2.4.1" timelimit="5" memlimit="0"/>
<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">
<file name="../avl.mlw" expanded="true">
<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="b06f96c3605f40076db787a2d22432b0">
<goal name="assoc">
<proof prover="1" memlimit="0"><result status="valid" time="0.02"/></proof>
<theory name="AVL" sum="b06f96c3605f40076db787a2d22432b0" expanded="true">
<goal name="M.M.assoc">
<proof prover="1" timelimit="5"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="neutral">
<proof prover="1" memlimit="0"><result status="valid" time="0.02"/></proof>
<goal name="M.M.neutral">
<proof prover="1" timelimit="5"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter real_height_nonnegative" expl="VC for real_height_nonnegative">
<proof prover="1" memlimit="0"><result status="valid" time="0.02"/></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