Commit b183e3fb authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

updated sessions

parent 6b553a1e
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="einstein/why3session.xml">
name="examples/einstein/why3session.xml">
<prover
id="alt-ergo"
id="0"
name="Alt-Ergo"
version="0.94"/>
<prover
id="coq"
name="Coq"
version="8.3pl3"/>
<prover
id="cvc3-2.2"
id="1"
name="CVC3"
version="2.2"/>
<prover
id="cvc3-2.4"
id="2"
name="CVC3"
version="2.4.1"/>
<prover
id="eprover"
id="3"
name="Eprover"
version="1.4"/>
<prover
id="gappa"
name="Gappa"
version="0.15.1"/>
<prover
id="simplify"
name="Simplify"
version="1.5.4"/>
<prover
id="spass"
id="4"
name="Spass"
version="3.7"/>
<prover
id="vampire"
id="5"
name="Vampire"
version="0.6"/>
<prover
id="verit"
name="veriT"
version="dev"/>
<prover
id="yices"
id="6"
name="Yices"
version="1.0.25"/>
version="1.0.27"/>
<prover
id="z3-2"
id="7"
name="Z3"
version="2.19"/>
<prover
id="z3-3"
id="8"
name="Z3"
version="3.2"/>
<file
......@@ -60,231 +44,254 @@
expanded="true">
<theory
name="Bijection"
locfile="examples/einstein/../einstein.why"
loclnum="7" loccnumb="7" loccnume="16"
verified="true"
expanded="true">
</theory>
<theory
name="Einstein"
locfile="examples/einstein/../einstein.why"
loclnum="18" loccnumb="7" loccnume="15"
verified="true"
expanded="true">
<label
name="Einstein's problem">
</label>
</theory>
<theory
name="EinsteinClues"
locfile="examples/einstein/../einstein.why"
loclnum="51" loccnumb="7" loccnume="20"
verified="true"
expanded="true">
<label
name="Clues">
</label>
</theory>
<theory
name="Goals"
locfile="examples/einstein/../einstein.why"
loclnum="107" loccnumb="7" loccnume="12"
verified="false"
expanded="true">
<label
name="Goals about Einstein's problem">
</label>
<goal
name="G1"
locfile="examples/einstein/../einstein.why"
loclnum="125" loccnumb="7" loccnume="9"
sum="b29963ab2946f6e953e24adc18bc2422"
proved="true"
expanded="true"
shape="ainfix =ato_aFishaGerman">
<proof
prover="alt-ergo"
prover="7"
timelimit="10"
edited=""
obsolete="false">
<result status="unknown" time="0.45"/>
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="z3-3"
timelimit="2"
edited=""
obsolete="false">
<result status="valid" time="0.05"/>
prover="4"
timelimit="3"
obsolete="false"
archived="false">
<result status="timeout" time="2.99"/>
</proof>
<proof
prover="cvc3-2.2"
prover="0"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="2.42"/>
obsolete="false"
archived="false">
<result status="unknown" time="0.17"/>
</proof>
<proof
prover="z3-2"
prover="1"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="eprover"
timelimit="3"
edited=""
obsolete="false">
<result status="timeout" time="4.96"/>
obsolete="false"
archived="false">
<result status="valid" time="2.58"/>
</proof>
<proof
prover="cvc3-2.4"
prover="2"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="1.92"/>
obsolete="false"
archived="false">
<result status="valid" time="2.15"/>
</proof>
<proof
prover="yices"
prover="6"
timelimit="3"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="timeout" time="3.02"/>
</proof>
<proof
prover="vampire"
prover="8"
timelimit="2"
obsolete="false"
archived="false">
<result status="valid" time="0.06"/>
</proof>
<proof
prover="5"
timelimit="3"
edited=""
obsolete="false">
<result status="unknown" time="5.08"/>
obsolete="false"
archived="false">
<result status="unknown" time="2.99"/>
</proof>
<proof
prover="spass"
prover="3"
timelimit="3"
edited=""
obsolete="false">
<result status="timeout" time="4.99"/>
obsolete="false"
archived="false">
<result status="timeout" time="2.98"/>
</proof>
</goal>
<goal
name="Wrong"
locfile="examples/einstein/../einstein.why"
loclnum="126" loccnumb="7" loccnume="12"
sum="b6ada39e4ed1ac554d7bdbccbfadcff3"
proved="false"
expanded="true"
shape="ainfix =ato_aCatsaSwede">
<proof
prover="alt-ergo"
prover="7"
timelimit="10"
edited=""
obsolete="false">
<result status="unknown" time="0.43"/>
obsolete="false"
archived="false">
<result status="timeout" time="10.08"/>
</proof>
<proof
prover="z3-3"
timelimit="2"
edited=""
obsolete="false">
<result status="timeout" time="10.09"/>
prover="4"
timelimit="3"
obsolete="false"
archived="false">
<result status="timeout" time="3.01"/>
</proof>
<proof
prover="cvc3-2.2"
prover="0"
timelimit="10"
edited=""
obsolete="false">
<result status="timeout" time="10.06"/>
obsolete="false"
archived="false">
<result status="unknown" time="0.17"/>
</proof>
<proof
prover="z3-2"
prover="1"
timelimit="10"
edited=""
obsolete="false">
<result status="timeout" time="10.09"/>
</proof>
<proof
prover="eprover"
timelimit="3"
edited=""
obsolete="false">
<result status="timeout" time="4.97"/>
obsolete="false"
archived="false">
<result status="timeout" time="10.08"/>
</proof>
<proof
prover="cvc3-2.4"
prover="2"
timelimit="10"
edited=""
obsolete="false">
<result status="timeout" time="10.10"/>
obsolete="false"
archived="false">
<result status="timeout" time="10.09"/>
</proof>
<proof
prover="yices"
prover="6"
timelimit="3"
edited=""
obsolete="false">
<result status="timeout" time="3.02"/>
obsolete="false"
archived="false">
<result status="timeout" time="3.03"/>
</proof>
<proof
prover="8"
timelimit="2"
obsolete="false"
archived="false">
<result status="timeout" time="2.02"/>
</proof>
<proof
prover="vampire"
prover="5"
timelimit="3"
edited=""
obsolete="false">
<result status="unknown" time="4.88"/>
obsolete="false"
archived="false">
<result status="unknown" time="3.00"/>
</proof>
<proof
prover="spass"
prover="3"
timelimit="3"
edited=""
obsolete="false">
<result status="timeout" time="4.69"/>
obsolete="false"
archived="false">
<result status="timeout" time="2.98"/>
</proof>
</goal>
<goal
name="G2"
locfile="examples/einstein/../einstein.why"
loclnum="127" loccnumb="7" loccnume="9"
sum="ad118f1b69459bb42f50fa8c2063d069"
proved="true"
expanded="true"
shape="ainfix =ato_aCatsaNorwegian">
<proof
prover="alt-ergo"
prover="7"
timelimit="10"
edited=""
obsolete="false">
<result status="unknown" time="0.43"/>
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="z3-3"
timelimit="2"
edited=""
obsolete="false">
<result status="valid" time="0.05"/>
prover="4"
timelimit="3"
obsolete="false"
archived="false">
<result status="timeout" time="2.99"/>
</proof>
<proof
prover="cvc3-2.2"
prover="0"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="1.87"/>
obsolete="false"
archived="false">
<result status="unknown" time="0.16"/>
</proof>
<proof
prover="z3-2"
prover="1"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="eprover"
timelimit="3"
edited=""
obsolete="false">
<result status="timeout" time="4.98"/>
obsolete="false"
archived="false">
<result status="valid" time="2.05"/>
</proof>
<proof
prover="cvc3-2.4"
prover="2"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="2.02"/>
obsolete="false"
archived="false">
<result status="valid" time="2.36"/>
</proof>
<proof
prover="yices"
prover="6"
timelimit="3"
edited=""
obsolete="false">
<result status="timeout" time="3.02"/>
obsolete="false"
archived="false">
<result status="timeout" time="3.03"/>
</proof>
<proof
prover="8"
timelimit="2"
obsolete="false"
archived="false">
<result status="valid" time="0.05"/>
</proof>
<proof
prover="vampire"
prover="5"
timelimit="3"
edited=""
obsolete="false">
<result status="unknown" time="4.97"/>
obsolete="false"
archived="false">
<result status="unknown" time="3.00"/>
</proof>
<proof
prover="spass"
prover="3"
timelimit="3"
edited=""
obsolete="false">
<result status="timeout" time="4.77"/>
obsolete="false"
archived="false">
<result status="timeout" time="2.98"/>
</proof>
</goal>
</theory>
......
This diff is collapsed.
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