Commit 2e1113a0 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

update sessions

parent 9bf1998f
......@@ -4,7 +4,7 @@
<prover
id="0"
name="Alt-Ergo"
version="0.94"/>
version="0.95.1"/>
<prover
id="1"
name="CVC3"
......
......@@ -4,25 +4,21 @@
<prover
id="0"
name="Alt-Ergo"
version="0.94"/>
<prover
id="1"
name="Alt-Ergo"
version="0.95.1"/>
<prover
id="2"
id="1"
name="CVC3"
version="2.2"/>
<prover
id="3"
id="2"
name="CVC3"
version="2.4.1"/>
<prover
id="4"
id="3"
name="Z3"
version="2.19"/>
<prover
id="5"
id="4"
name="Z3"
version="3.2"/>
<file
......@@ -45,11 +41,11 @@
shape="f">
<proof
prover="0"
timelimit="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.02"/>
<result status="unknown" time="0.01"/>
</proof>
<proof
prover="1"
......@@ -57,7 +53,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.01"/>
<result status="timeout" time="3.01"/>
</proof>
<proof
prover="2"
......@@ -83,14 +79,6 @@
archived="false">
<result status="timeout" time="3.01"/>
</proof>
<proof
prover="5"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="3.01"/>
</proof>
</goal>
</theory>
<theory
......@@ -121,18 +109,10 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
</proof>
<proof
prover="2"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="3.02"/>
</proof>
<proof
prover="3"
prover="2"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -140,7 +120,7 @@
<result status="timeout" time="3.11"/>
</proof>
<proof
prover="4"
prover="3"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -148,7 +128,7 @@
<result status="timeout" time="3.01"/>
</proof>
<proof
prover="5"
prover="4"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -178,7 +158,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
<result status="timeout" time="3.11"/>
</proof>
<proof
prover="2"
......@@ -194,18 +174,10 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="3.11"/>
</proof>
<proof
prover="4"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="3.01"/>
</proof>
<proof
prover="5"
prover="4"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -258,18 +230,10 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
</proof>
<proof
prover="4"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.01"/>
</proof>
<proof
prover="5"
prover="4"
timelimit="3"
memlimit="1000"
obsolete="false"
......
......@@ -15,12 +15,20 @@
version="2.4.1"/>
<prover
id="3"
name="Spass"
version="3.7"/>
name="CVC4"
version="1.2"/>
<prover
id="4"
name="Z3"
version="2.19"/>
<prover
id="5"
name="Z3"
version="3.2"/>
<prover
id="6"
name="Z3"
version="4.3.1"/>
<file
name="../euclideandivision.why"
verified="true"
......@@ -65,11 +73,11 @@
</proof>
<proof
prover="3"
timelimit="10"
memlimit="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="10.57"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="4"
......@@ -79,6 +87,22 @@
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="G2"
......@@ -114,11 +138,11 @@
</proof>
<proof
prover="3"
timelimit="10"
memlimit="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="10.68"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="4"
......@@ -128,6 +152,22 @@
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
</theory>
</file>
......
......@@ -4,7 +4,7 @@
<prover
id="0"
name="Alt-Ergo"
version="0.94"/>
version="0.95.1"/>
<prover
id="1"
name="CVC3"
......
......@@ -4,33 +4,29 @@
<prover
id="0"
name="Alt-Ergo"
version="0.94"/>
<prover
id="1"
name="Alt-Ergo"
version="0.95.1"/>
<prover
id="2"
id="1"
name="CVC3"
version="2.2"/>
<prover
id="3"
id="2"
name="CVC3"
version="2.4.1"/>
<prover
id="4"
id="3"
name="Gappa"
version="0.16.6"/>
<prover
id="5"
id="4"
name="Yices"
version="1.0.38"/>
<prover
id="6"
id="5"
name="Z3"
version="2.19"/>
<prover
id="7"
id="6"
name="Z3"
version="3.2"/>
<file
......@@ -42,14 +38,14 @@
locfile="../real.why"
loclnum="1" loccnumb="7" loccnume="11"
verified="true"
expanded="false">
expanded="true">
<goal
name="G1"
locfile="../real.why"
loclnum="3" loccnumb="7" loccnume="9"
sum="1b55b6a0ae65e52aaee305d27a4a34e1"
proved="true"
expanded="false"
expanded="true"
shape="ainfix =ainfix *c5.5c10.c55.">
<proof
prover="0"
......@@ -60,7 +56,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="2"
prover="1"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -68,7 +64,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="3"
prover="2"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -76,7 +72,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="4"
prover="3"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -84,7 +80,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="5"
prover="4"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -92,7 +88,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="6"
prover="5"
timelimit="3"
memlimit="0"
obsolete="false"
......@@ -100,7 +96,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="7"
prover="6"
timelimit="3"
memlimit="0"
obsolete="false"
......@@ -114,7 +110,7 @@
loclnum="4" loccnumb="7" loccnume="9"
sum="0d2cb993e61eda0e088fdaa9deb94d63"
proved="true"
expanded="false"
expanded="true"
shape="ainfix =ainfix /c9.c3.c3.">
<proof
prover="0"
......@@ -125,7 +121,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="2"
prover="1"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -133,7 +129,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="3"
prover="2"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -141,7 +137,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="4"
prover="3"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -149,7 +145,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="6"
prover="5"
timelimit="3"
memlimit="0"
obsolete="false"
......@@ -157,7 +153,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="7"
prover="6"
timelimit="3"
memlimit="0"
obsolete="false"
......@@ -171,7 +167,7 @@
loclnum="5" loccnumb="7" loccnume="9"
sum="08aff9ffa7d85a1553b4d5f6869a41c6"
proved="true"
expanded="false"
expanded="true"
shape="ainfix =ainvc5.c0.2">
<proof
prover="0"
......@@ -182,7 +178,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
prover="1"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -190,7 +186,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="3"
prover="2"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -198,7 +194,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="6"
prover="5"
timelimit="3"
memlimit="0"
obsolete="false"
......@@ -206,7 +202,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="7"
prover="6"
timelimit="3"
memlimit="0"
obsolete="false"
......@@ -220,14 +216,14 @@
locfile="../real.why"
loclnum="8" loccnumb="7" loccnume="16"
verified="true"
expanded="false">
expanded="true">
<goal
name="Add"
locfile="../real.why"
loclnum="10" loccnumb="7" loccnume="10"
sum="aa1993a8c86e0410db2a7ab0664fae39"
proved="true"
expanded="false"
expanded="true"
shape="ainfix =ainfix +.c5.5c10.c15.5">
<proof
prover="0"
......@@ -238,7 +234,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
prover="1"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -246,7 +242,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="3"
prover="2"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -254,7 +250,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="4"
prover="3"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -262,7 +258,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="6"
prover="5"
timelimit="3"
memlimit="0"
obsolete="false"
......@@ -270,7 +266,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="7"
prover="6"
timelimit="3"
memlimit="0"
obsolete="false"
......@@ -284,7 +280,7 @@
loclnum="11" loccnumb="7" loccnume="10"
sum="c315d4874a1a6950ddf714b967372fbb"
proved="true"
expanded="false"
expanded="true"
shape="ainfix =ainfix -.c9.c3.c6.">
<proof
prover="0"
......@@ -295,7 +291,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
prover="1"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -303,7 +299,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="3"
prover="2"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -311,7 +307,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="4"
prover="3"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -319,7 +315,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="6"
prover="5"
timelimit="3"
memlimit="0"
obsolete="false"
......@@ -327,7 +323,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="7"
prover="6"
timelimit="3"
memlimit="0"
obsolete="false"
......@@ -341,7 +337,7 @@
loclnum="12" loccnumb="7" loccnume="10"
sum="01b43991c342b0adb9ba4d95b0974860"
proved="true"
expanded="false"
expanded="true"
shape="ainfix =ainfix +.aprefix -.c5.c3.5aprefix -.c1.5">
<proof
prover="0"
......@@ -352,7 +348,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="2"
prover="1"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -360,7 +356,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="3"
prover="2"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -368,7 +364,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="4"
prover="3"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -376,7 +372,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="6"
prover="5"
timelimit="3"
memlimit="0"
obsolete="false"
......@@ -384,7 +380,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="7"
prover="6"
timelimit="3"
memlimit="0"
obsolete="false"
......@@ -398,7 +394,7 @@
loclnum="13" loccnumb="7" loccnume="10"
sum="191100b1821f56f8515f5f7e10df8172"
proved="true"
expanded="false"
expanded="true"
shape="ainfix =ainfix *.c5.5c10.c55.">
<proof
prover="0"