Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

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

updated proof sessions

parent 99349928
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/jcf/why3/share/why3session.dtd">
<why3session
name="./genealogy/why3session.xml">
name="examples/genealogy/why3session.xml">
<prover
id="0"
name="Alt-Ergo"
......@@ -40,495 +40,495 @@
version="3.2"/>
<file
name="../genealogy.why"
verified="false"
expanded="false">
verified="true"
expanded="true">
<theory
name="Genealogy"
locfile="./genealogy/../genealogy.why"
locfile="examples/genealogy/../genealogy.why"
loclnum="2" loccnumb="7" loccnume="16"
verified="false"
verified="true"
expanded="true">
<goal
name="Child_is_son_or_daughter"
locfile="./genealogy/../genealogy.why"
locfile="examples/genealogy/../genealogy.why"
loclnum="23" loccnumb="7" loccnume="31"
sum="0fde3c4f7583ff6e9fdaf0ce7b4f3389"
proved="false"
proved="true"
expanded="true"
shape="adaughterV0V1OasonV0V1qachildV0V1F">
<proof
prover="7"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="4"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="0"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="unknown" time="0.01"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="8"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="5"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="6"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="3"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Sibling_sym"
locfile="./genealogy/../genealogy.why"
locfile="examples/genealogy/../genealogy.why"
loclnum="29" loccnumb="7" loccnume="18"
sum="9a92a8e0fe47bbd3fabeaf95bdb6478a"
proved="false"
proved="true"
expanded="true"
shape="asiblingV1V0IasiblingV0V1F">
<proof
prover="7"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="4"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="0"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="1"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="8"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="5"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="6"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="3"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Sibling_is_brother_or_sister"
locfile="./genealogy/../genealogy.why"
locfile="examples/genealogy/../genealogy.why"
loclnum="34" loccnumb="7" loccnume="35"
sum="54165903233e74eef52a31f1d35b8b51"
proved="false"
proved="true"
expanded="true"
shape="asisterV0V1OabrotherV0V1qasiblingV0V1F">
<proof
prover="7"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="4"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="0"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="unknown" time="0.01"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="8"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="5"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="6"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="3"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Grandparent_is_grandfather_or_grandmother"
locfile="./genealogy/../genealogy.why"
locfile="examples/genealogy/../genealogy.why"
loclnum="45" loccnumb="7" loccnume="48"
sum="c61ec3544cb1baa038f6db3e31109756"
proved="false"
proved="true"
expanded="true"
shape="agrandmotherV0V1OagrandfatherV0V1qagrandparentV0V1F">
<proof
prover="7"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="0"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="8"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="6"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
</proof>
<proof
prover="3"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="Grandfather_male"
locfile="./genealogy/../genealogy.why"
locfile="examples/genealogy/../genealogy.why"
loclnum="48" loccnumb="7" loccnume="23"
sum="f21f5bc53305ec525334fbfe7d8ee21b"
proved="false"
proved="true"
expanded="true"
shape="ainfix =agenderV0aMaleIagrandfatherV0V1F">
<proof
prover="7"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="4"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="0"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="8"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="5"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="6"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="3"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Grandmother_female"
locfile="./genealogy/../genealogy.why"
locfile="examples/genealogy/../genealogy.why"
loclnum="50" loccnumb="7" loccnume="25"
sum="6046a0d8dba383c5e7e8a8521140862d"
proved="false"
proved="true"
expanded="true"
shape="ainfix =agenderV0aFemaleIagrandmotherV0V1F">
<proof
prover="7"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="4"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="0"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="8"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="5"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="6"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="3"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Only_two_grandfathers"
locfile="./genealogy/../genealogy.why"
locfile="examples/genealogy/../genealogy.why"
loclnum="53" loccnumb="7" loccnume="28"
sum="2644ef6a6d637a753381302d35a2bf73"
proved="false"
proved="true"
expanded="true"
shape="ainfix =V0V2Oainfix =V1V2Oainfix =V0V1IagrandfatherV2V3IagrandfatherV1V3IagrandfatherV0V3F">
<proof
prover="7"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="4"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="0"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="8"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="6"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="3"
timelimit="5"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
</theory>
......
This source diff could not be displayed because it is too large. You can view the blob instead.
This diff is collapsed.
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