Commit 3b2c1733 authored by MARCHE Claude's avatar MARCHE Claude

updated sessions

parent 30fc66d6
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="examples/einstein/why3session.xml">
name="einstein/why3session.xml">
<prover
id="alt-ergo"
name="Alt-Ergo"
version="0.93"/>
<prover
id="alt-ergo-0.93.1"
name="Alt-Ergo"
version="0.93.1"/>
<prover
id="coq"
name="Coq"
......@@ -14,6 +18,10 @@
id="cvc3"
name="CVC3"
version="2.2"/>
<prover
id="cvc3-2.4"
name="CVC3"
version="2.4.1"/>
<prover
id="eprover"
name="Eprover"
......@@ -46,6 +54,10 @@
id="z3"
name="Z3"
version="2.19"/>
<prover
id="z3-3"
name="Z3"
version="3.2"/>
<file
name="../einstein.why"
verified="false"
......@@ -75,16 +87,30 @@
proved="true"
expanded="true"
shape="ainfix =ato_aFishaGerman">
<proof
prover="alt-ergo-0.93.1"
timelimit="10"
edited=""
obsolete="false">
<result status="unknown" time="0.45"/>
</proof>
<proof
prover="z3-3"
timelimit="2"
edited=""
obsolete="false">
<result status="valid" time="0.05"/>
</proof>
<proof
prover="cvc3"
timelimit="3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="2.53"/>
<result status="valid" time="2.42"/>
</proof>
<proof
prover="z3"
timelimit="3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.03"/>
......@@ -96,6 +122,13 @@
obsolete="false">
<result status="timeout" time="4.96"/>
</proof>
<proof
prover="cvc3-2.4"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="1.92"/>
</proof>
<proof
prover="yices"
timelimit="3"
......@@ -124,19 +157,33 @@
proved="false"
expanded="true"
shape="ainfix =ato_aCatsaSwede">
<proof
prover="alt-ergo-0.93.1"
timelimit="10"
edited=""
obsolete="false">
<result status="unknown" time="0.43"/>
</proof>
<proof
prover="z3-3"
timelimit="2"
edited=""
obsolete="false">
<result status="timeout" time="10.09"/>
</proof>
<proof
prover="cvc3"
timelimit="3"
timelimit="10"
edited=""
obsolete="false">
<result status="timeout" time="5.04"/>
<result status="timeout" time="10.06"/>
</proof>
<proof
prover="z3"
timelimit="3"
timelimit="10"
edited=""
obsolete="false">
<result status="timeout" time="3.02"/>
<result status="timeout" time="10.09"/>
</proof>
<proof
prover="eprover"
......@@ -145,6 +192,13 @@
obsolete="false">
<result status="timeout" time="4.97"/>
</proof>
<proof
prover="cvc3-2.4"
timelimit="10"
edited=""
obsolete="false">
<result status="timeout" time="10.10"/>
</proof>
<proof
prover="yices"
timelimit="3"
......@@ -173,19 +227,33 @@
proved="true"
expanded="true"
shape="ainfix =ato_aCatsaNorwegian">
<proof
prover="alt-ergo-0.93.1"
timelimit="10"
edited=""
obsolete="false">
<result status="unknown" time="0.43"/>
</proof>
<proof
prover="z3-3"
timelimit="2"
edited=""
obsolete="false">
<result status="valid" time="0.05"/>
</proof>
<proof
prover="cvc3"
timelimit="3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="1.94"/>
<result status="valid" time="1.87"/>
</proof>
<proof
prover="z3"
timelimit="3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="eprover"
......@@ -194,6 +262,13 @@
obsolete="false">
<result status="timeout" time="4.98"/>
</proof>
<proof
prover="cvc3-2.4"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="2.02"/>
</proof>
<proof
prover="yices"
timelimit="3"
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="./explicit_subst/why3session.xml">
name="explicit_subst/why3session.xml">
<prover
id="alt-ergo"
name="Alt-Ergo"
version="0.93"/>
<prover
id="alt-ergo-0.93.1"
name="Alt-Ergo"
version="0.93.1"/>
<prover
id="coq"
name="Coq"
......@@ -14,6 +18,10 @@
id="cvc3"
name="CVC3"
version="2.2"/>
<prover
id="cvc3-2.4"
name="CVC3"
version="2.4.1"/>
<prover
id="eprover"
name="Eprover"
......@@ -46,6 +54,10 @@
id="z3"
name="Z3"
version="2.19"/>
<prover
id="z3-3"
name="Z3"
version="3.2"/>
<file
name="../explicit_subst.why"
verified="true"
......@@ -65,6 +77,20 @@
proved="true"
expanded="true"
shape="ainfix =aappaLambdaaVaraZeroaaaa">
<proof
prover="z3-3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="alt-ergo-0.93.1"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="cvc3"
timelimit="5"
......@@ -86,6 +112,13 @@
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="cvc3-2.4"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="vampire"
timelimit="5"
......@@ -107,6 +140,20 @@
proved="true"
expanded="true"
shape="ainfix =aappaLambdaaVaraZeroaaab">
<proof
prover="z3-3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="alt-ergo-0.93.1"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="4.90"/>
</proof>
<proof
prover="cvc3"
timelimit="5"
......@@ -128,6 +175,13 @@
obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="cvc3-2.4"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.11"/>
</proof>
<proof
prover="vampire"
timelimit="5"
......@@ -149,6 +203,20 @@
proved="true"
expanded="true"
shape="LaLambdaasubstaVaraSaZeroaSaZeroaaLaLambdaaaainfix =V0V1">
<proof
prover="z3-3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="alt-ergo-0.93.1"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="cvc3"
timelimit="5"
......@@ -170,6 +238,13 @@
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="cvc3-2.4"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="vampire"
timelimit="5"
......@@ -191,6 +266,20 @@
proved="true"
expanded="true"
shape="LasubstaLambdaaVaraSaZeroaZeroaaLaLambdaaaainfix =V0V1">
<proof
prover="z3-3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="alt-ergo-0.93.1"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="cvc3"
timelimit="5"
......@@ -212,6 +301,13 @@
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="cvc3-2.4"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="vampire"
timelimit="5"
......@@ -233,6 +329,20 @@
proved="true"
expanded="true"
shape="LaLambdaaLambdaaVaraSaZeroLaLambdaaaainfix =aappV0aaV1">
<proof
prover="z3-3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="alt-ergo-0.93.1"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="cvc3"
timelimit="5"
......@@ -254,6 +364,13 @@
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="cvc3-2.4"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.23"/>
</proof>
<proof
prover="vampire"
timelimit="5"
......@@ -275,6 +392,20 @@
proved="true"
expanded="true"
shape="LaLambdaaLambdaaappaVaraZeroaVaraSaZeroainfix =aappaappV0aaaidaa">
<proof
prover="z3-3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="alt-ergo-0.93.1"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.06"/>
</proof>
<proof
prover="eprover"
timelimit="5"
......@@ -289,6 +420,13 @@
obsolete="false">
<result status="valid" time="0.04"/>
</proof>
<proof
prover="cvc3-2.4"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.04"/>
</proof>
<proof
prover="vampire"
timelimit="5"
......@@ -310,6 +448,27 @@
proved="true"
expanded="true"
shape="LaLambdaaLambdaaappaVaraZeroaVaraSaZeroLaLambdaaappaVaraZeroaaainfix =aappV0aaV1">
<proof
prover="z3-3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="alt-ergo-0.93.1"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.06"/>
</proof>
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="unknown" time="0.08"/>
</proof>
<proof
prover="cvc3"
timelimit="5"
......@@ -331,6 +490,13 @@
obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="cvc3-2.4"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.04"/>
</proof>
<proof
prover="vampire"
timelimit="5"
......@@ -362,6 +528,20 @@
proved="true"
expanded="true"
shape="ainfix =aappalambdaavaraZeroaaaa">
<proof
prover="z3-3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="alt-ergo-0.93.1"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.06"/>
</proof>
<proof
prover="eprover"
timelimit="5"
......@@ -376,6 +556,13 @@
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="cvc3-2.4"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.04"/>
</proof>
<proof
prover="vampire"
timelimit="5"
......@@ -397,6 +584,20 @@
proved="true"
expanded="true"
shape="ainfix =aappalambdaavaraZeroaaab">
<proof
prover="z3-3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="2.12"/>
</proof>
<proof
prover="alt-ergo-0.93.1"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.10"/>
</proof>
<proof
prover="eprover"
timelimit="5"
......@@ -411,6 +612,13 @@
obsolete="false">
<result status="valid" time="2.82"/>
</proof>
<proof
prover="cvc3-2.4"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.04"/>
</proof>
<proof
prover="vampire"
timelimit="5"
......@@ -432,6 +640,20 @@
proved="true"
expanded="true"
shape="LalambdaasubstavaraSaZeroaSaZeroaaLalambdaaaainfix =V0V1">
<proof
prover="z3-3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="alt-ergo-0.93.1"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.08"/>
</proof>
<proof
prover="eprover"
timelimit="5"
......@@ -446,6 +668,13 @@
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="cvc3-2.4"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.03"/>
</proof>
<proof
prover="vampire"
timelimit="5"
......@@ -467,6 +696,20 @@
proved="true"
expanded="true"
shape="LasubstalambdaavaraSaZeroaZeroaaLalambdaaaainfix =V0V1">
<proof
prover="z3-3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="alt-ergo-0.93.1"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.08"/>
</proof>
<proof
prover="eprover"
timelimit="5"
......@@ -481,6 +724,13 @@
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="cvc3-2.4"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.04"/>
</proof>
<proof
prover="vampire"
timelimit="5"
......@@ -502,6 +752,20 @@
proved="true"
expanded="true"
shape="LalambdaalambdaavaraSaZeroLalambdaaaainfix =aappV0aaV1">
<proof
prover="z3-3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="alt-ergo-0.93.1"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.08"/>
</proof>
<proof
prover="eprover"
timelimit="5"
......@@ -516,6 +780,13 @@
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="cvc3-2.4"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.04"/>
</proof>
<proof
prover="vampire"
timelimit="5"
......@@ -537,6 +808,20 @@
proved="true"
expanded="true"
shape="LalambdaalambdaaappavaraZeroavaraSaZeroainfix =aappaappV0aaaidaa">
<proof
prover="z3-3"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.03"/>
</proof>
<proof
prover="alt-ergo-0.93.1"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.04"/>
</proof>
<proof
prover="eprover"
timelimit="5"
......@@ -544,6 +829,13 @@
obsolete="false">
<result status="valid" time="0.00"/>
</proof>