Commit d8c610a0 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

add COQ and PVS proofs to examples/logic/genealogy.why

parent 6ea71416
......@@ -23,50 +23,58 @@
version="1.2"/>
<prover
id="5"
name="Coq"
version="8.4pl2"/>
<prover
id="6"
name="Eprover"
version="1.4"/>
<prover
id="6"
id="7"
name="Eprover"
version="1.6"/>
<prover
id="7"
id="8"
name="Metis"
version="2.3"/>
<prover
id="8"
id="9"
name="PVS"
version="6.0"/>
<prover
id="10"
name="Simplify"
version="1.5.4"/>
<prover
id="9"
id="11"
name="Spass"
version="3.7"/>
<prover
id="10"
id="12"
name="Vampire"
version="0.6"/>
<prover
id="11"
id="13"
name="Yices"
version="1.0.38"/>
<prover
id="12"
id="14"
name="Z3"
version="2.19"/>
<prover
id="13"
id="15"
name="Z3"
version="3.2"/>
<prover
id="14"
id="16"
name="Z3"
version="4.3.1"/>
<prover
id="15"
id="17"
name="Zenon"
version="0.7.1"/>
<prover
id="16"
id="18"
name="veriT"
version="201310"/>
<file
......@@ -129,6 +137,15 @@
</proof>
<proof
prover="5"
timelimit="5"
memlimit="4000"
edited="genealogy_Genealogy_Child_is_son_or_daughter_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.94"/>
</proof>
<proof
prover="6"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -136,7 +153,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="6"
prover="7"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -144,7 +161,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="7"
prover="8"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -152,7 +169,16 @@
<result status="valid" time="0.02"/>
</proof>
<proof
prover="8"
prover="9"
timelimit="5"
memlimit="4000"
edited="genealogy_Genealogy_Child_is_son_or_daughter_1.pvs"
obsolete="false"
archived="false">
<result status="highfailure" time="0.00"/>
</proof>
<proof
prover="10"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -160,7 +186,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="9"
prover="11"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -168,7 +194,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="10"
prover="12"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -176,7 +202,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="11"
prover="13"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -184,7 +210,7 @@
<result status="unknown" time="0.01"/>
</proof>
<proof
prover="12"
prover="14"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -192,7 +218,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="13"
prover="15"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -200,7 +226,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="14"
prover="16"
timelimit="5"
memlimit="4000"
obsolete="false"
......@@ -208,7 +234,7 @@
<result status="unknown" time="1.88"/>
</proof>
<proof
prover="15"
prover="17"
timelimit="5"
memlimit="4000"
obsolete="false"
......@@ -216,7 +242,7 @@
<result status="valid" time="0.04"/>
</proof>
<proof
prover="16"
prover="18"
timelimit="60"
memlimit="1000"
obsolete="false"
......@@ -273,7 +299,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="5"
prover="6"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -281,7 +307,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="6"
prover="7"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -289,7 +315,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="7"
prover="8"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -297,7 +323,7 @@
<result status="valid" time="0.12"/>
</proof>
<proof
prover="8"
prover="10"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -305,7 +331,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="9"
prover="11"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -313,7 +339,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="10"
prover="12"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -321,7 +347,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="11"
prover="13"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -329,7 +355,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="12"
prover="14"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -337,7 +363,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="13"
prover="15"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -345,7 +371,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="14"
prover="16"
timelimit="5"
memlimit="4000"
obsolete="false"
......@@ -353,7 +379,7 @@
<result status="valid" time="0.02"/>
</proof>
<proof
prover="15"
prover="17"
timelimit="5"
memlimit="4000"
obsolete="false"
......@@ -361,7 +387,7 @@
<result status="timeout" time="5.23"/>
</proof>
<proof
prover="16"
prover="18"
timelimit="5"
memlimit="4000"
obsolete="false"
......@@ -418,7 +444,7 @@
<result status="unknown" time="0.01"/>
</proof>
<proof
prover="5"
prover="6"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -426,7 +452,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="6"
prover="7"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -434,7 +460,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="7"
prover="8"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -442,7 +468,7 @@
<result status="valid" time="0.04"/>
</proof>
<proof
prover="8"
prover="10"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -450,7 +476,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="9"
prover="11"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -458,7 +484,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="10"
prover="12"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -466,7 +492,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="11"
prover="13"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -474,7 +500,7 @@
<result status="unknown" time="0.02"/>
</proof>
<proof
prover="12"
prover="14"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -482,7 +508,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="13"
prover="15"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -490,7 +516,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="14"
prover="16"
timelimit="5"
memlimit="4000"
obsolete="false"
......@@ -498,7 +524,7 @@
<result status="unknown" time="2.12"/>
</proof>
<proof
prover="15"
prover="17"
timelimit="5"
memlimit="4000"
obsolete="false"
......@@ -506,7 +532,7 @@
<result status="valid" time="0.03"/>
</proof>
<proof
prover="16"
prover="18"
timelimit="5"
memlimit="4000"
obsolete="false"
......@@ -563,7 +589,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="5"
prover="6"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -571,7 +597,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="6"
prover="7"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -579,7 +605,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="7"
prover="8"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -587,7 +613,7 @@
<result status="valid" time="0.07"/>
</proof>
<proof
prover="8"
prover="10"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -595,7 +621,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="10"
prover="12"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -603,7 +629,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="11"
prover="13"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -611,7 +637,7 @@
<result status="valid" time="0.04"/>
</proof>
<proof
prover="12"
prover="14"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -619,7 +645,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="13"
prover="15"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -627,7 +653,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="14"
prover="16"
timelimit="5"
memlimit="4000"
obsolete="false"
......@@ -635,7 +661,7 @@
<result status="valid" time="0.03"/>
</proof>
<proof
prover="15"
prover="17"
timelimit="5"
memlimit="4000"
obsolete="false"
......@@ -643,7 +669,7 @@
<result status="timeout" time="5.26"/>
</proof>
<proof
prover="16"
prover="18"
timelimit="5"
memlimit="4000"
obsolete="false"
......@@ -700,7 +726,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="5"
prover="6"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -708,7 +734,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="6"
prover="7"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -716,7 +742,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="7"
prover="8"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -724,7 +750,7 @@
<result status="valid" time="0.03"/>
</proof>
<proof
prover="8"
prover="10"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -732,7 +758,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="9"
prover="11"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -740,7 +766,7 @@
<result status="valid" time="0.02"/>
</proof>
<proof
prover="10"
prover="12"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -748,7 +774,7 @@
<result status="valid" time="0.03"/>
</proof>
<proof
prover="11"
prover="13"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -756,7 +782,7 @@
<result status="valid" time="0.02"/>
</proof>
<proof
prover="12"
prover="14"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -764,7 +790,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="13"
prover="15"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -772,7 +798,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="14"
prover="16"
timelimit="5"
memlimit="4000"
obsolete="false"
......@@ -780,7 +806,7 @@
<result status="valid" time="0.03"/>
</proof>
<proof
prover="15"
prover="17"
timelimit="5"
memlimit="4000"
obsolete="false"
......@@ -788,7 +814,7 @@
<result status="timeout" time="5.10"/>
</proof>
<proof
prover="16"
prover="18"
timelimit="5"
memlimit="4000"
obsolete="false"
......@@ -845,7 +871,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="5"
prover="6"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -853,7 +879,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="6"
prover="7"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -861,7 +887,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="7"
prover="8"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -869,7 +895,7 @@
<result status="valid" time="0.03"/>
</proof>
<proof
prover="8"
prover="10"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -877,7 +903,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="9"
prover="11"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -885,7 +911,7 @@
<result status="valid" time="0.02"/>
</proof>
<proof
prover="10"
prover="12"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -893,7 +919,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="11"
prover="13"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -901,7 +927,7 @@
<result status="valid" time="0.03"/>
</proof>
<proof
prover="12"
prover="14"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -909,7 +935,7 @@