Commit 403a2cb0 authored by MARCHE Claude's avatar MARCHE Claude

updated sessions on moloch

parent 2a7f9f61
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="./einstein/why3session.xml">
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.2pl1"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="gappa" name="Gappa" version="0.13.0"/>
<prover id="simplify" name="Simplify" version="1.5.4"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../einstein.why" verified="false" expanded="true">
<theory name="Bijection" verified="true" expanded="true">
<why3session
name="examples/einstein/why3session.xml">
<prover
id="alt-ergo"
name="Alt-Ergo"
version="0.93"/>
<prover
id="coq"
name="Coq"
version="8.3pl2"/>
<prover
id="cvc3"
name="CVC3"
version="2.2"/>
<prover
id="eprover"
name="Eprover"
version="1.4 Namring"/>
<prover
id="gappa"
name="Gappa"
version="0.15.1"/>
<prover
id="simplify"
name="Simplify"
version="1.5.4"/>
<prover
id="spass"
name="Spass"
version="3.7"/>
<prover
id="vampire"
name="Vampire"
version="0.6"/>
<prover
id="verit"
name="veriT"
version="dev"/>
<prover
id="yices"
name="Yices"
version="1.0.25"/>
<prover
id="z3"
name="Z3"
version="2.19"/>
<file
name="../einstein.why"
verified="false"
expanded="true">
<theory
name="Bijection"
verified="true"
expanded="true">
</theory>
<theory name="Einstein" verified="true" expanded="true">
<theory
name="Einstein"
verified="true"
expanded="true">
</theory>
<theory name="EinsteinClues" verified="true" expanded="true">
<theory
name="EinsteinClues"
verified="true"
expanded="true">
</theory>
<theory name="Goals" verified="false" expanded="true">
<goal name="G1" sum="4e666b5243bdb1064743ec6e271cb8ec" proved="true" expanded="true" shape="ainfix =ato_aFishaGerman">
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.05"/>
<theory
name="Goals"
verified="false"
expanded="true">
<goal
name="G1"
sum="4e666b5243bdb1064743ec6e271cb8ec"
proved="true"
expanded="true"
shape="ainfix =ato_aFishaGerman">
<proof
prover="cvc3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="2.44"/>
</proof>
<proof
prover="eprover"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="4.98"/>
</proof>
<proof
prover="z3"
timelimit="2"
edited=""
obsolete="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="yices"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.11"/>
</proof>
<proof
prover="vampire"
timelimit="5"
edited=""
obsolete="false">
<result status="unknown" time="4.98"/>
</proof>
<proof
prover="spass"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.00"/>
</proof>
</goal>
<goal name="Wrong" sum="1a0ed387ff3cda5c8323f4eb21fd248c" proved="false" expanded="true" shape="ainfix =ato_aCatsaSwede">
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<goal
name="Wrong"
sum="1a0ed387ff3cda5c8323f4eb21fd248c"
proved="false"
expanded="true"
shape="ainfix =ato_aCatsaSwede">
<proof
prover="simplify"
timelimit="2"
edited=""
obsolete="false">
<result status="timeout" time="2.31"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.81"/>
<proof
prover="cvc3"
timelimit="2"
edited=""
obsolete="false">
<result status="timeout" time="5.02"/>
</proof>
<proof
prover="eprover"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="4.98"/>
</proof>
<proof
prover="z3"
timelimit="2"
edited=""
obsolete="false">
<result status="timeout" time="5.03"/>
</proof>
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.01"/>
<proof
prover="yices"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.12"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="3.01"/>
<proof
prover="vampire"
timelimit="5"
edited=""
obsolete="false">
<result status="unknown" time="4.99"/>
</proof>
<proof
prover="spass"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.04"/>
</proof>
</goal>
<goal name="G2" sum="44df905be1d95d899616a903f2a08529" proved="true" expanded="true" shape="ainfix =ato_aCatsaNorwegian">
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.08"/>
<goal
name="G2"
sum="44df905be1d95d899616a903f2a08529"
proved="true"
expanded="true"
shape="ainfix =ato_aCatsaNorwegian">
<proof
prover="cvc3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="1.88"/>
</proof>
<proof
prover="eprover"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="4.99"/>
</proof>
<proof
prover="z3"
timelimit="2"
edited=""
obsolete="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="yices"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.02"/>
</proof>
<proof
prover="vampire"
timelimit="5"
edited=""
obsolete="false">
<result status="unknown" time="4.99"/>
</proof>
<proof
prover="spass"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="4.99"/>
</proof>
</goal>
</theory>
......
......@@ -14,10 +14,14 @@
id="cvc3"
name="CVC3"
version="2.2"/>
<prover
id="eprover"
name="Eprover"
version="1.4 Namring"/>
<prover
id="gappa"
name="Gappa"
version="0.15.0"/>
version="0.15.1"/>
<prover
id="simplify"
name="Simplify"
......@@ -30,6 +34,10 @@
id="vampire"
name="Vampire"
version="0.6"/>
<prover
id="verit"
name="veriT"
version="dev"/>
<prover
id="yices"
name="Yices"
......@@ -62,6 +70,13 @@
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="eprover"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
......@@ -97,7 +112,14 @@
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.10"/>
<result status="valid" time="0.09"/>
</proof>
<proof
prover="eprover"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="1.08"/>
</proof>
<proof
prover="z3"
......@@ -134,6 +156,13 @@
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="eprover"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="z3"
timelimit="5"
......@@ -167,7 +196,14 @@
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="eprover"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="z3"
......@@ -202,7 +238,14 @@
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.18"/>
<result status="valid" time="0.17"/>
</proof>
<proof
prover="eprover"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.06"/>
</proof>
<proof
prover="z3"
......@@ -232,6 +275,13 @@
proved="true"
expanded="true"
shape="LaLambdaaLambdaaappaVaraZeroaVaraSaZeroainfix =aappaappV0aaaidaa">
<proof
prover="eprover"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.20"/>
</proof>
<proof
prover="z3"
timelimit="5"
......@@ -265,7 +315,14 @@
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="4.77"/>
<result status="valid" time="4.35"/>
</proof>
<proof
prover="eprover"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.21"/>
</proof>
<proof
prover="z3"
......@@ -305,6 +362,13 @@
proved="true"
expanded="true"
shape="ainfix =aappalambdaavaraZeroaaaa">
<proof
prover="eprover"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="z3"
timelimit="5"
......@@ -333,6 +397,13 @@
proved="true"
expanded="true"
shape="ainfix =aappalambdaavaraZeroaaab">
<proof
prover="eprover"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="z3"
timelimit="5"
......@@ -361,6 +432,13 @@
proved="true"
expanded="true"
shape="LalambdaasubstavaraSaZeroaSaZeroaaLalambdaaaainfix =V0V1">
<proof
prover="eprover"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="z3"
timelimit="5"
......@@ -389,6 +467,13 @@
proved="true"
expanded="true"
shape="LasubstalambdaavaraSaZeroaZeroaaLalambdaaaainfix =V0V1">
<proof
prover="eprover"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="z3"
timelimit="5"
......@@ -408,7 +493,7 @@
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
......@@ -417,6 +502,13 @@
proved="true"
expanded="true"
shape="LalambdaalambdaavaraSaZeroLalambdaaaainfix =aappV0aaV1">
<proof
prover="eprover"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="z3"
timelimit="5"
......@@ -445,6 +537,13 @@
proved="true"
expanded="true"
shape="LalambdaalambdaaappavaraZeroavaraSaZeroainfix =aappaappV0aaaidaa">
<proof
prover="eprover"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="vampire"
timelimit="5"
......@@ -466,6 +565,13 @@
proved="true"
expanded="true"
shape="LalambdaalambdaaappavaraZeroavaraSaZeroLalambdaaappavaraZeroaaainfix =aappV0aaV1">
<proof
prover="eprover"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="vampire"
timelimit="5"
......@@ -478,7 +584,7 @@
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
</theory>
......
......@@ -14,10 +14,14 @@
id="cvc3"
name="CVC3"
version="2.2"/>
<prover
id="eprover"
name="Eprover"
version="1.4 Namring"/>
<prover
id="gappa"
name="Gappa"
version="0.15.0"/>
version="0.15.1"/>
<prover
id="simplify"
name="Simplify"
......@@ -30,6 +34,10 @@
id="vampire"
name="Vampire"
version="0.6"/>
<prover
id="verit"
name="veriT"
version="dev"/>
<prover
id="yices"
name="Yices"
......@@ -52,6 +60,20 @@
proved="true"
expanded="true"
shape="adaughterV0V1OasonV0V1qachildV0V1F">
<proof
prover="simplify"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.02"/>
</proof>
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="unknown" time="0.01"/>
</proof>
<proof
prover="cvc3"
timelimit="5"
......@@ -60,11 +82,11 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="alt-ergo"
prover="eprover"
timelimit="5"
edited=""
obsolete="false">
<result status="unknown" time="0.02"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="z3"
......@@ -73,6 +95,13 @@
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="yices"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="vampire"
timelimit="5"
......@@ -94,6 +123,13 @@
proved="true"
expanded="true"
shape="asiblingV1V0IasiblingV0V1F">
<proof
prover="simplify"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.02"/>
</proof>
<proof
prover="cvc3"
timelimit="5"
......@@ -108,6 +144,13 @@
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="eprover"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="z3"
timelimit="5"
......@@ -115,12 +158,19 @@
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="yices"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="vampire"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="spass"
......@@ -137,11 +187,11 @@
expanded="true"
shape="asisterV0V1OabrotherV0V1qasiblingV0V1F">
<proof
prover="cvc3"
prover="simplify"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
<result status="timeout" time="5.12"/>
</proof>
<proof
prover="alt-ergo"
......@@ -150,6 +200,20 @@
obsolete="false">
<result status="unknown" time="0.01"/>
</proof>
<proof
prover="cvc3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="eprover"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="z3"
timelimit="5"
......@@ -157,6 +221,13 @@
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="yices"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="vampire"
timelimit="5"
......@@ -169,7 +240,7 @@
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
......@@ -178,6 +249,13 @@
proved="true"
expanded="true"
shape="agrandmotherV0V1OagrandfatherV0V1qagrandparentV0V1F">
<proof
prover="simplify"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.12"/>
</proof>
<proof
prover="cvc3"
timelimit="5"
......@@ -192,6 +270,13 @@
obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="eprover"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="z3"
timelimit="5"
......@@ -200,11 +285,11 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="vampire"
prover="yices"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.97"/>
<result status="valid" time="0.04"/>
</proof>
<proof
prover="spass"
......@@ -220,6 +305,13 @@
proved="true"
expanded="true"
shape="ainfix =agenderV0aMaleIagrandfatherV0V1F">
<proof
prover="simplify"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.03"/>
</proof>
<proof
prover="cvc3"
timelimit="5"
......@@ -232,7 +324,14 @@
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="eprover"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="z3"
......@@ -242,12 +341,19 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="vampire"
prover="yices"
timelimit="5"
edited=""