Commit 09da8804 authored by Andrei Paskevich's avatar Andrei Paskevich

update session for the hanoi towers

parent 4160347c
......@@ -11,18 +11,22 @@
version="2.4.1"/>
<prover
id="2"
name="CVC4"
version="1.0"/>
<prover
id="3"
name="Coq"
version="8.3pl4"/>
<prover
id="3"
id="4"
name="Eprover"
version="1.4"/>
<prover
id="4"
id="5"
name="Spass"
version="3.7"/>
<prover
id="5"
id="6"
name="Z3"
version="4.2"/>
<file
......@@ -290,7 +294,7 @@
<result status="valid" time="0.06"/>
</proof>
<proof
prover="5"
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -476,7 +480,7 @@
expanded="true"
shape="ainfix =arev_appendainfix ++V0V1V2arev_appendV1arev_appendV0V2F">
<proof
prover="2"
prover="3"
timelimit="5"
memlimit="1000"
edited="tower_of_hanoi_ListRevAppend_rev_append_append_l_1.v"
......@@ -494,7 +498,7 @@
expanded="true"
shape="ainfix =arev_appendV0ainfix ++V1V2arev_appendarev_appendV1V0V2F">
<proof
prover="2"
prover="3"
timelimit="5"
memlimit="1000"
edited="tower_of_hanoi_ListRevAppend_rev_append_append_r_1.v"
......@@ -512,7 +516,7 @@
expanded="true"
shape="ainfix =alengtharev_appendV0V1ainfix +alengthV0alengthV1F">
<proof
prover="2"
prover="3"
timelimit="5"
memlimit="1000"
edited="tower_of_hanoi_ListRevAppend_rev_append_length_1.v"
......@@ -537,7 +541,7 @@
expanded="true"
shape="acompatV0V1AasortedV1AasortedV0qasortedarev_appendV0V1F">
<proof
prover="2"
prover="3"
timelimit="5"
memlimit="1000"
edited="tower_of_hanoi_ListRevSorted_rev_append_sorted_incr_1.v"
......@@ -555,7 +559,7 @@
expanded="true"
shape="acompatV1V0AasortedV1AasortedV0qasortedarev_appendV0V1F">
<proof
prover="2"
prover="3"
timelimit="5"
memlimit="1000"
edited="tower_of_hanoi_ListRevSorted_rev_append_sorted_decr_1.v"
......@@ -604,10 +608,10 @@
locfile="../tower_of_hanoi.mlw"
loclnum="163" loccnumb="10" loccnume="19"
expl="VC for hanoi_rec"
sum="05384269daf0b413064e96a5fefa6961"
sum="0a54f275ec12423702d445ecec1a1cba"
proved="true"
expanded="true"
shape="iainfix &gt;V0c0CV1aConsVwCV1aConswVainfix =V13V3Aainfix =V14arev_appendV1V4Aainfix =V15V2AasortedV15Iainfix =V15V12Aainfix =V14arev_appendV7V11Aainfix =V13V3AasortedV14AasortedV13FACV12aConsVVCV7aConsVVainfix &lt;V18V16wtwtACV11aConsVVCV7aConsVVainfix &lt;V22V20wtwtAainfix =V8arev_appendV7V3AasortedV7Aainfix =alengthV7ainfix -V0c1Aainfix &lt;ainfix -V0c1V0Aainfix &lt;=c0V0Iainfix =V11aConsV6V9Aainfix =V12V2AasortedV11AasortedV12FACV9aNiltaConsVwainfix &lt;V6V24Aainfix =V10aConsV6V2AasortedV9Iainfix =V9V4Aainfix =V8arev_appendV7V3Aainfix =V10aConsV6V2AasortedV8AasortedV10FACV4aConsVVCV7aConsVVainfix &lt;V27V25wtwtACV3aConsVVCV7aConsVVainfix &lt;V31V29wtwtAainfix =V5arev_appendV7aConsV6V2AasortedV7Aainfix =alengthV7ainfix -V0c1Aainfix &lt;ainfix -V0c1V0Aainfix &lt;=c0V0aNilfaNilfainfix =V3V3Aainfix =V4arev_appendV1V4Aainfix =V5V2ICV3aConsVVCV1aConsVVainfix &lt;V35V33wtwtACV4aConsVVCV1aConsVVainfix &lt;V39V37wtwtAainfix =V5arev_appendV1V2AasortedV1Aainfix =alengthV1V0AasortedV3AasortedV4AasortedV5FF">
shape="iainfix &gt;V0c0CV1aConsVVainfix =V13V3Aainfix =V14arev_appendV1V4Aainfix =V15V2AasortedV15Iainfix =V15V12Aainfix =V14arev_appendV7V11Aainfix =V13V3AasortedV14AasortedV13FACV12aConsVVCV7aConsVVainfix &lt;V18V16wtwtACV11aConsVVCV7aConsVVainfix &lt;V22V20wtwtAainfix =V8arev_appendV7V3AasortedV7Aainfix =alengthV7ainfix -V0c1Aainfix &lt;ainfix -V0c1V0Aainfix &lt;=c0V0Iainfix =V11aConsV6V9Aainfix =V12V2AasortedV11AasortedV12FACV9aNiltaConsVwainfix &lt;V6V24Aainfix =V10aConsV6V2AasortedV9Iainfix =V9V4Aainfix =V8arev_appendV7V3Aainfix =V10aConsV6V2AasortedV8AasortedV10FACV4aConsVVCV7aConsVVainfix &lt;V27V25wtwtACV3aConsVVCV7aConsVVainfix &lt;V31V29wtwtAainfix =V5arev_appendV7aConsV6V2AasortedV7Aainfix =alengthV7ainfix -V0c1Aainfix &lt;ainfix -V0c1V0Aainfix &lt;=c0V0aNilfainfix =V3V3Aainfix =V4arev_appendV1V4Aainfix =V5V2ICV3aConsVVCV1aConsVVainfix &lt;V35V33wtwtACV4aConsVVCV1aConsVVainfix &lt;V39V37wtwtAainfix =V5arev_appendV1V2AasortedV1Aainfix =alengthV1V0AasortedV3AasortedV4AasortedV5FF">
<label
name="expl:VC for hanoi_rec"/>
<transf
......@@ -619,10 +623,10 @@
locfile="../tower_of_hanoi.mlw"
loclnum="163" loccnumb="10" loccnume="19"
expl="1. variant decrease"
sum="37214e8b4014e92e82cd2eb411232c64"
sum="e97714fec705d2cfaf2cbac52b2c855e"
proved="true"
expanded="true"
shape="CV1aConsVwCV1aConswVainfix &lt;ainfix -V0c1V0Aainfix &lt;=c0V0aNiltaNiltIainfix &gt;V0c0ICV3aConsVVCV1aConsVVainfix &lt;V10V8wtwtACV4aConsVVCV1aConsVVainfix &lt;V14V12wtwtAainfix =V5arev_appendV1V2AasortedV1Aainfix =alengthV1V0AasortedV3AasortedV4AasortedV5FF">
shape="CV1aConsVVainfix &lt;ainfix -V0c1V0Aainfix &lt;=c0V0aNiltIainfix &gt;V0c0ICV3aConsVVCV1aConsVVainfix &lt;V10V8wtwtACV4aConsVVCV1aConsVVainfix &lt;V14V12wtwtAainfix =V5arev_appendV1V2AasortedV1Aainfix =alengthV1V0AasortedV3AasortedV4AasortedV5FF">
<label
name="expl:VC for hanoi_rec"/>
<proof
......@@ -631,7 +635,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.04"/>
</proof>
<proof
prover="1"
......@@ -642,12 +646,20 @@
<result status="valid" time="0.02"/>
</proof>
<proof
prover="5"
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.12"/>
</proof>
</goal>
<goal
......@@ -655,10 +667,10 @@
locfile="../tower_of_hanoi.mlw"
loclnum="163" loccnumb="10" loccnume="19"
expl="2. precondition"
sum="38b9b938e461f6ce61e254957b405801"
sum="d3cf63591934c21f37895bb76f59b98f"
proved="true"
expanded="true"
shape="CV1aConsVwCV1aConswVasortedV7Aainfix =alengthV7ainfix -V0c1aNiltaNiltIainfix &gt;V0c0ICV3aConsVVCV1aConsVVainfix &lt;V10V8wtwtACV4aConsVVCV1aConsVVainfix &lt;V14V12wtwtAainfix =V5arev_appendV1V2AasortedV1Aainfix =alengthV1V0AasortedV3AasortedV4AasortedV5FF">
shape="CV1aConsVVasortedV7Aainfix =alengthV7ainfix -V0c1aNiltIainfix &gt;V0c0ICV3aConsVVCV1aConsVVainfix &lt;V10V8wtwtACV4aConsVVCV1aConsVVainfix &lt;V14V12wtwtAainfix =V5arev_appendV1V2AasortedV1Aainfix =alengthV1V0AasortedV3AasortedV4AasortedV5FF">
<label
name="expl:VC for hanoi_rec"/>
<proof
......@@ -667,7 +679,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.07"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="1"
......@@ -675,7 +687,15 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.12"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="3.92"/>
</proof>
</goal>
<goal
......@@ -683,10 +703,10 @@
locfile="../tower_of_hanoi.mlw"
loclnum="163" loccnumb="10" loccnume="19"
expl="3. precondition"
sum="73ee91b3a3dcb042eea6683de379cda4"
sum="247c48c4d95b5ecbfde707b8def41fff"
proved="true"
expanded="true"
shape="CV1aConsVwCV1aConswVainfix =V5arev_appendV7aConsV6V2aNiltaNiltIainfix &gt;V0c0ICV3aConsVVCV1aConsVVainfix &lt;V10V8wtwtACV4aConsVVCV1aConsVVainfix &lt;V14V12wtwtAainfix =V5arev_appendV1V2AasortedV1Aainfix =alengthV1V0AasortedV3AasortedV4AasortedV5FF">
shape="CV1aConsVVainfix =V5arev_appendV7aConsV6V2aNiltIainfix &gt;V0c0ICV3aConsVVCV1aConsVVainfix &lt;V10V8wtwtACV4aConsVVCV1aConsVVainfix &lt;V14V12wtwtAainfix =V5arev_appendV1V2AasortedV1Aainfix =alengthV1V0AasortedV3AasortedV4AasortedV5FF">
<label
name="expl:VC for hanoi_rec"/>
<proof
......@@ -695,7 +715,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="1"
......@@ -706,12 +726,12 @@
<result status="valid" time="0.02"/>
</proof>
<proof
prover="3"
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="3.71"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="4"
......@@ -719,7 +739,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="1.19"/>
<result status="valid" time="0.40"/>
</proof>
<proof
prover="5"
......@@ -727,7 +747,15 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.12"/>
<result status="valid" time="1.14"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal
......@@ -735,10 +763,10 @@
locfile="../tower_of_hanoi.mlw"
loclnum="163" loccnumb="10" loccnume="19"
expl="4. precondition"
sum="1cffa83279f6cf326114aaf13ef06de5"
sum="0a16678e03aca02e41d3009cab850c23"
proved="true"
expanded="true"
shape="CV1aConsVwCV1aConswVCV3aConsVVCV7aConsVVainfix &lt;V10V8wtwtaNiltaNiltIainfix &gt;V0c0ICV3aConsVVCV1aConsVVainfix &lt;V14V12wtwtACV4aConsVVCV1aConsVVainfix &lt;V18V16wtwtAainfix =V5arev_appendV1V2AasortedV1Aainfix =alengthV1V0AasortedV3AasortedV4AasortedV5FF">
shape="CV1aConsVVCV3aConsVVCV7aConsVVainfix &lt;V10V8wtwtaNiltIainfix &gt;V0c0ICV3aConsVVCV1aConsVVainfix &lt;V14V12wtwtACV4aConsVVCV1aConsVVainfix &lt;V18V16wtwtAainfix =V5arev_appendV1V2AasortedV1Aainfix =alengthV1V0AasortedV3AasortedV4AasortedV5FF">
<label
name="expl:VC for hanoi_rec"/>
<proof
......@@ -747,23 +775,23 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.12"/>
<result status="valid" time="0.14"/>
</proof>
<proof
prover="3"
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.06"/>
<result status="valid" time="0.05"/>
</proof>
<proof
prover="4"
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.61"/>
<result status="valid" time="0.38"/>
</proof>
</goal>
<goal
......@@ -771,10 +799,10 @@
locfile="../tower_of_hanoi.mlw"
loclnum="163" loccnumb="10" loccnume="19"
expl="5. precondition"
sum="1a4aaa2578f3addacbc79349a339e3d4"
sum="3eedb1a4f116434f0de9f631c698ddc6"
proved="true"
expanded="true"
shape="CV1aConsVwCV1aConswVCV4aConsVVCV7aConsVVainfix &lt;V10V8wtwtaNiltaNiltIainfix &gt;V0c0ICV3aConsVVCV1aConsVVainfix &lt;V14V12wtwtACV4aConsVVCV1aConsVVainfix &lt;V18V16wtwtAainfix =V5arev_appendV1V2AasortedV1Aainfix =alengthV1V0AasortedV3AasortedV4AasortedV5FF">
shape="CV1aConsVVCV4aConsVVCV7aConsVVainfix &lt;V10V8wtwtaNiltIainfix &gt;V0c0ICV3aConsVVCV1aConsVVainfix &lt;V14V12wtwtACV4aConsVVCV1aConsVVainfix &lt;V18V16wtwtAainfix =V5arev_appendV1V2AasortedV1Aainfix =alengthV1V0AasortedV3AasortedV4AasortedV5FF">
<label
name="expl:VC for hanoi_rec"/>
<proof
......@@ -783,23 +811,23 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.16"/>
<result status="valid" time="0.15"/>
</proof>
<proof
prover="3"
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.06"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="4"
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.63"/>
<result status="valid" time="0.38"/>
</proof>
</goal>
<goal
......@@ -807,10 +835,10 @@
locfile="../tower_of_hanoi.mlw"
loclnum="163" loccnumb="10" loccnume="19"
expl="6. type invariant"
sum="c5704b50ce49d57dd5fe6f5cad785174"
sum="e43bad6cd6cd72d01e5a530ef3008343"
proved="true"
expanded="true"
shape="CV1aConsVwCV1aConswVasortedV9Iainfix =V9V4Aainfix =V8arev_appendV7V3Aainfix =V10aConsV6V2AasortedV8AasortedV10FICV4aConsVVCV7aConsVVainfix &lt;V13V11wtwtACV3aConsVVCV7aConsVVainfix &lt;V17V15wtwtAainfix =V5arev_appendV7aConsV6V2AasortedV7Aainfix =alengthV7ainfix -V0c1aNiltaNiltIainfix &gt;V0c0ICV3aConsVVCV1aConsVVainfix &lt;V21V19wtwtACV4aConsVVCV1aConsVVainfix &lt;V25V23wtwtAainfix =V5arev_appendV1V2AasortedV1Aainfix =alengthV1V0AasortedV3AasortedV4AasortedV5FF">
shape="CV1aConsVVasortedV9Iainfix =V9V4Aainfix =V8arev_appendV7V3Aainfix =V10aConsV6V2AasortedV8AasortedV10FICV4aConsVVCV7aConsVVainfix &lt;V13V11wtwtACV3aConsVVCV7aConsVVainfix &lt;V17V15wtwtAainfix =V5arev_appendV7aConsV6V2AasortedV7Aainfix =alengthV7ainfix -V0c1aNiltIainfix &gt;V0c0ICV3aConsVVCV1aConsVVainfix &lt;V21V19wtwtACV4aConsVVCV1aConsVVainfix &lt;V25V23wtwtAainfix =V5arev_appendV1V2AasortedV1Aainfix =alengthV1V0AasortedV3AasortedV4AasortedV5FF">
<label
name="expl:VC for hanoi_rec"/>
<proof
......@@ -827,15 +855,15 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="3"
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="4"
......@@ -843,7 +871,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="5"
......@@ -851,6 +879,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
......@@ -859,10 +895,10 @@
locfile="../tower_of_hanoi.mlw"
loclnum="163" loccnumb="10" loccnume="19"
expl="7. precondition"
sum="9d49b48e29812737b11980e1396d76ec"
sum="f0b4ff3d8dff11e940e7f902fa04cbc4"
proved="true"
expanded="true"
shape="CV1aConsVwCV1aConswVainfix =V10aConsV6V2IasortedV9Iainfix =V9V4Aainfix =V8arev_appendV7V3Aainfix =V10aConsV6V2AasortedV8AasortedV10FICV4aConsVVCV7aConsVVainfix &lt;V13V11wtwtACV3aConsVVCV7aConsVVainfix &lt;V17V15wtwtAainfix =V5arev_appendV7aConsV6V2AasortedV7Aainfix =alengthV7ainfix -V0c1aNiltaNiltIainfix &gt;V0c0ICV3aConsVVCV1aConsVVainfix &lt;V21V19wtwtACV4aConsVVCV1aConsVVainfix &lt;V25V23wtwtAainfix =V5arev_appendV1V2AasortedV1Aainfix =alengthV1V0AasortedV3AasortedV4AasortedV5FF">
shape="CV1aConsVVainfix =V10aConsV6V2IasortedV9Iainfix =V9V4Aainfix =V8arev_appendV7V3Aainfix =V10aConsV6V2AasortedV8AasortedV10FICV4aConsVVCV7aConsVVainfix &lt;V13V11wtwtACV3aConsVVCV7aConsVVainfix &lt;V17V15wtwtAainfix =V5arev_appendV7aConsV6V2AasortedV7Aainfix =alengthV7ainfix -V0c1aNiltIainfix &gt;V0c0ICV3aConsVVCV1aConsVVainfix &lt;V21V19wtwtACV4aConsVVCV1aConsVVainfix &lt;V25V23wtwtAainfix =V5arev_appendV1V2AasortedV1Aainfix =alengthV1V0AasortedV3AasortedV4AasortedV5FF">
<label
name="expl:VC for hanoi_rec"/>
<proof
......@@ -879,15 +915,15 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="3"
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="4"
......@@ -895,7 +931,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.05"/>
</proof>
<proof
prover="5"
......@@ -903,6 +939,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.05"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
......@@ -911,10 +955,10 @@
locfile="../tower_of_hanoi.mlw"
loclnum="163" loccnumb="10" loccnume="19"
expl="8. precondition"
sum="790679518f5666dfe573c743aaf261c3"
sum="a5519ceb11a37c0be645fc0d944084f3"
proved="true"
expanded="true"
shape="CV1aConsVwCV1aConswVCV9aNiltaConsVwainfix &lt;V6V11IasortedV9Iainfix =V9V4Aainfix =V8arev_appendV7V3Aainfix =V10aConsV6V2AasortedV8AasortedV10FICV4aConsVVCV7aConsVVainfix &lt;V14V12wtwtACV3aConsVVCV7aConsVVainfix &lt;V18V16wtwtAainfix =V5arev_appendV7aConsV6V2AasortedV7Aainfix =alengthV7ainfix -V0c1aNiltaNiltIainfix &gt;V0c0ICV3aConsVVCV1aConsVVainfix &lt;V22V20wtwtACV4aConsVVCV1aConsVVainfix &lt;V26V24wtwtAainfix =V5arev_appendV1V2AasortedV1Aainfix =alengthV1V0AasortedV3AasortedV4AasortedV5FF">
shape="CV1aConsVVCV9aNiltaConsVwainfix &lt;V6V11IasortedV9Iainfix =V9V4Aainfix =V8arev_appendV7V3Aainfix =V10aConsV6V2AasortedV8AasortedV10FICV4aConsVVCV7aConsVVainfix &lt;V14V12wtwtACV3aConsVVCV7aConsVVainfix &lt;V18V16wtwtAainfix =V5arev_appendV7aConsV6V2AasortedV7Aainfix =alengthV7ainfix -V0c1aNiltIainfix &gt;V0c0ICV3aConsVVCV1aConsVVainfix &lt;V22V20wtwtACV4aConsVVCV1aConsVVainfix &lt;V26V24wtwtAainfix =V5arev_appendV1V2AasortedV1Aainfix =alengthV1V0AasortedV3AasortedV4AasortedV5FF">
<label
name="expl:VC for hanoi_rec"/>
<proof
......@@ -923,23 +967,23 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.18"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="3"
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.05"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="4"
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.11"/>
<result status="valid" time="0.05"/>
</proof>
</goal>
<goal
......@@ -947,10 +991,10 @@
locfile="../tower_of_hanoi.mlw"
loclnum="163" loccnumb="10" loccnume="19"
expl="9. variant decrease"
sum="a15b409e22887d62557eec8321ca1ea5"
sum="bcade33d438ca4dfea69a9b3b9fd510e"
proved="true"
expanded="true"
shape="CV1aConsVwCV1aConswVainfix &lt;ainfix -V0c1V0Aainfix &lt;=c0V0Iainfix =V11aConsV6V9Aainfix =V12V2AasortedV11AasortedV12FICV9aNiltaConsVwainfix &lt;V6V13Aainfix =V10aConsV6V2AasortedV9Iainfix =V9V4Aainfix =V8arev_appendV7V3Aainfix =V10aConsV6V2AasortedV8AasortedV10FICV4aConsVVCV7aConsVVainfix &lt;V16V14wtwtACV3aConsVVCV7aConsVVainfix &lt;V20V18wtwtAainfix =V5arev_appendV7aConsV6V2AasortedV7Aainfix =alengthV7ainfix -V0c1aNiltaNiltIainfix &gt;V0c0ICV3aConsVVCV1aConsVVainfix &lt;V24V22wtwtACV4aConsVVCV1aConsVVainfix &lt;V28V26wtwtAainfix =V5arev_appendV1V2AasortedV1Aainfix =alengthV1V0AasortedV3AasortedV4AasortedV5FF">
shape="CV1aConsVVainfix &lt;ainfix -V0c1V0Aainfix &lt;=c0V0Iainfix =V11aConsV6V9Aainfix =V12V2AasortedV11AasortedV12FICV9aNiltaConsVwainfix &lt;V6V13Aainfix =V10aConsV6V2AasortedV9Iainfix =V9V4Aainfix =V8arev_appendV7V3Aainfix =V10aConsV6V2AasortedV8AasortedV10FICV4aConsVVCV7aConsVVainfix &lt;V16V14wtwtACV3aConsVVCV7aConsVVainfix &lt;V20V18wtwtAainfix =V5arev_appendV7aConsV6V2AasortedV7Aainfix =alengthV7ainfix -V0c1aNiltIainfix &gt;V0c0ICV3aConsVVCV1aConsVVainfix &lt;V24V22wtwtACV4aConsVVCV1aConsVVainfix &lt;V28V26wtwtAainfix =V5arev_appendV1V2AasortedV1Aainfix =alengthV1V0AasortedV3AasortedV4AasortedV5FF">
<label
name="expl:VC for hanoi_rec"/>
<proof
......@@ -967,10 +1011,18 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="5"
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -983,10 +1035,10 @@
locfile="../tower_of_hanoi.mlw"
loclnum="163" loccnumb="10" loccnume="19"
expl="10. precondition"
sum="f8edefec9b01b38e755985b90052e079"
sum="0be65f982fa44e7b34b2c72dbcde0315"
proved="true"
expanded="true"
shape="CV1aConsVwCV1aConswVasortedV7Aainfix =alengthV7ainfix -V0c1Iainfix =V11aConsV6V9Aainfix =V12V2AasortedV11AasortedV12FICV9aNiltaConsVwainfix &lt;V6V13Aainfix =V10aConsV6V2AasortedV9Iainfix =V9V4Aainfix =V8arev_appendV7V3Aainfix =V10aConsV6V2AasortedV8AasortedV10FICV4aConsVVCV7aConsVVainfix &lt;V16V14wtwtACV3aConsVVCV7aConsVVainfix &lt;V20V18wtwtAainfix =V5arev_appendV7aConsV6V2AasortedV7Aainfix =alengthV7ainfix -V0c1aNiltaNiltIainfix &gt;V0c0ICV3aConsVVCV1aConsVVainfix &lt;V24V22wtwtACV4aConsVVCV1aConsVVainfix &lt;V28V26wtwtAainfix =V5arev_appendV1V2AasortedV1Aainfix =alengthV1V0AasortedV3AasortedV4AasortedV5FF">
shape="CV1aConsVVasortedV7Aainfix =alengthV7ainfix -V0c1Iainfix =V11aConsV6V9Aainfix =V12V2AasortedV11AasortedV12FICV9aNiltaConsVwainfix &lt;V6V13Aainfix =V10aConsV6V2AasortedV9Iainfix =V9V4Aainfix =V8arev_appendV7V3Aainfix =V10aConsV6V2AasortedV8AasortedV10FICV4aConsVVCV7aConsVVainfix &lt;V16V14wtwtACV3aConsVVCV7aConsVVainfix &lt;V20V18wtwtAainfix =V5arev_appendV7aConsV6V2AasortedV7Aainfix =alengthV7ainfix -V0c1aNiltIainfix &gt;V0c0ICV3aConsVVCV1aConsVVainfix &lt;V24V22wtwtACV4aConsVVCV1aConsVVainfix &lt;V28V26wtwtAainfix =V5arev_appendV1V2AasortedV1Aainfix =alengthV1V0AasortedV3AasortedV4AasortedV5FF">
<label
name="expl:VC for hanoi_rec"/>
<proof
......@@ -995,7 +1047,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
......@@ -1003,15 +1055,15 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="3"
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="4"
......@@ -1019,7 +1071,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.05"/>
<result status="valid" time="0.06"/>
</proof>
<proof
prover="5"
......@@ -1027,7 +1079,15 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.04"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
......@@ -1035,10 +1095,10 @@
locfile="../tower_of_hanoi.mlw"
loclnum="163" loccnumb="10" loccnume="19"
expl="11. precondition"
sum="7228a7199363a95c8663280f27bc2652"
sum="94cac2599af8b1715ef1595a4e5e9836"
proved="true"
expanded="true"
shape="CV1aConsVwCV1aConswVainfix =V8arev_appendV7V3Iainfix =V11aConsV6V9Aainfix =V12V2AasortedV11AasortedV12FICV9aNiltaConsVwainfix &lt;V6V13Aainfix =V10aConsV6V2AasortedV9Iainfix =V9V4Aainfix =V8arev_appendV7V3Aainfix =V10aConsV6V2AasortedV8AasortedV10FICV4aConsVVCV7aConsVVainfix &lt;V16V14wtwtACV3aConsVVCV7aConsVVainfix &lt;V20V18wtwtAainfix =V5arev_appendV7aConsV6V2AasortedV7Aainfix =alengthV7ainfix -V0c1aNiltaNiltIainfix &gt;V0c0ICV3aConsVVCV1aConsVVainfix &lt;V24V22wtwtACV4aConsVVCV1aConsVVainfix &lt;V28V26wtwtAainfix =V5arev_appendV1V2AasortedV1Aainfix =alengthV1V0AasortedV3AasortedV4AasortedV5FF">
shape="CV1aConsVVainfix =V8arev_appendV7V3Iainfix =V11aConsV6V9Aainfix =V12V2AasortedV11AasortedV12FICV9aNiltaConsVwainfix &lt;V6V13Aainfix =V10aConsV6V2AasortedV9Iainfix =V9V4Aainfix =V8arev_appendV7V3Aainfix =V10aConsV6V2AasortedV8AasortedV10FICV4aConsVVCV7aConsVVainfix &lt;V16V14wtwtACV3aConsVVCV7aConsVVainfix &lt;V20V18wtwtAainfix =V5arev_appendV7aConsV6V2AasortedV7Aainfix =alengthV7ainfix -V0c1aNiltIainfix &gt;V0c0ICV3aConsVVCV1aConsVVainfix &lt;V24V22wtwtACV4aConsVVCV1aConsVVainfix &lt;V28V26wtwtAainfix =V5arev_appendV1V2AasortedV1Aainfix =alengthV1V0AasortedV3AasortedV4AasortedV5FF">
<label
name="expl:VC for hanoi_rec"/>
<proof
......@@ -1055,15 +1115,15 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="3"
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="4"
......@@ -1071,7 +1131,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="5"
......@@ -1079,6 +1139,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
......@@ -1087,10 +1155,10 @@
locfile="../tower_of_hanoi.mlw"
loclnum="163" loccnumb="10" loccnume="19"
expl="12. precondition"
sum="b126f37280ff52da3327ac68a4c82767"
sum="b660a20de0639f67b9c39d8c3ba0f3d4"
proved="true"
expanded="true"
shape="CV1aConsVwCV1aConswVCV11aConsVVCV7aConsVVainfix &lt;V15V13wtwtIainfix =V11aConsV6V9Aainfix =V12V2AasortedV11AasortedV12FICV9aNiltaConsVwainfix &lt;V6V17Aainfix =V10aConsV6V2AasortedV9Iainfix =V9V4Aainfix =V8arev_appendV7V3Aainfix =V10aConsV6V2AasortedV8AasortedV10FICV4aConsVVCV7aConsVVainfix &lt;V20V18wtwtACV3aConsVVCV7aConsVVainfix &lt;V24V22wtwtAainfix =V5arev_appendV7aConsV6V2AasortedV7Aainfix =alengthV7ainfix -V0c1aNiltaNiltIainfix &gt;V0c0ICV3aConsVVCV1aConsVVainfix &lt;V28V26wtwtACV4aConsVVCV1aConsVVainfix &lt;V32V30wtwtAainfix =V5arev_appendV1V2AasortedV1Aainfix =alengthV1V0AasortedV3AasortedV4AasortedV5FF">
shape="CV1aConsVVCV11aConsVVCV7aConsVVainfix &lt;V15V13wtwtIainfix =V11aConsV6V9Aainfix =V12V2AasortedV11AasortedV12FICV9aNiltaConsVwainfix &lt;V6V17Aainfix =V10aConsV6V2AasortedV9Iainfix =V9V4Aainfix =V8arev_appendV7V3Aainfix =V10aConsV6V2AasortedV8AasortedV10FICV4aConsVVCV7aConsVVainfix &lt;V20V18wtwtACV3aConsVVCV7aConsVVainfix &lt;V24V22wtwtAainfix =V5arev_appendV7aConsV6V2AasortedV7Aainfix =alengthV7ainfix -V0c1aNiltIainfix &gt;V0c0ICV3aConsVVCV1aConsVVainfix &lt;V28V26wtwtACV4aConsVVCV1aConsVVainfix &lt;V32V30wtwtAainfix =V5arev_appendV1V2AasortedV1Aainfix =alengthV1V0AasortedV3AasortedV4AasortedV5FF">
<label
name="expl:VC for hanoi_rec"/>
<proof
......@@ -1099,23 +1167,23 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.24"/>
<result status="valid" time="0.39"/>
</proof>
<proof
prover="3"
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.07"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="4"
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.46"/>