Commit 4a863010 authored by MARCHE Claude's avatar MARCHE Claude

updated proofs of queens

parent 06ec684d
......@@ -15,8 +15,8 @@
version="2.2"/>
<prover
id="3"
name="CVC3"
version="2.4.1"/>
name="CVC4"
version="1.0"/>
<prover
id="4"
name="Coq"
......@@ -537,16 +537,24 @@
name="expl:VC for t3"/>
<proof
prover="0"
timelimit="30"
memlimit="0"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.45"/>
</proof>
<proof
prover="5"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.20"/>
</proof>
<proof
prover="6"
timelimit="15"
memlimit="0"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.64"/>
......@@ -565,32 +573,40 @@
name="expl:VC for t3"/>
<proof
prover="0"
timelimit="30"
memlimit="0"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.10"/>
</proof>
<proof
prover="2"
timelimit="30"
memlimit="0"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.82"/>
<result status="valid" time="0.58"/>
</proof>
<proof
prover="3"
timelimit="30"
memlimit="0"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="12.52"/>
<result status="valid" time="0.74"/>
</proof>
<proof
prover="5"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.11"/>
</proof>
<proof
prover="6"
timelimit="15"
memlimit="0"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.59"/>
......@@ -615,6 +631,14 @@
archived="false">
<result status="valid" time="1.41"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.12"/>
</proof>
</goal>
<goal
name="WP_parameter t3.3.12.1.4"
......@@ -635,6 +659,14 @@
archived="false">
<result status="valid" time="2.18"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="1.46"/>
</proof>
</goal>
<goal
name="WP_parameter t3.3.12.1.5"
......@@ -647,10 +679,18 @@
shape="ainfix =ainfix -amixfix []V13V15amixfix []V13V16ainfix -V16V15NIainfix &lt;V16V15Aainfix &lt;=c0V16FIainfix &lt;V15V14Aainfix &lt;=c0V15FIainfix =V14ainfix +V11c1FIainfix =V13asetV12V11amin_eltV8FIamemV17V8NFNIainfix =amixfix []V4V18amixfix []V10V18Iainfix &lt;V18V3Aainfix &lt;=c0V18FAainfix =amixfix []V6V19amixfix []V12V19Iainfix &lt;V19V11Aainfix &lt;=c0V19FAaeq_prefixV20amixfix []V10V21anAainfix &lt;V21V9Aainfix =V3V21Oainfix &lt;V3V21Eqamemamixfix []V20V11adiffadiffadiffV0V1V2V8Aainfix =amixfix []V12V22amixfix []V20V22Iainfix &lt;V22V11Aainfix &lt;=c0V22FAapartial_solutionanV20FAainfix &lt;V23V24IamemV24V8IamemV23adiffadiffadiffV0V1V2V8FAalt_solamixfix []V10V25amixfix []V10V26Iainfix &lt;V26V9Aainfix &lt;V25V26Aainfix &lt;=V3V25FAainfix =ainfix -amixfix []V12V27amixfix []V12V28ainfix -V28V27NAainfix =ainfix -amixfix []V12V27amixfix []V12V28ainfix -V27V28NAainfix =amixfix []V12V27amixfix []V12V28NIainfix &lt;V28V27Aainfix &lt;=c0V28FAainfix &lt;amixfix []V12V27anAainfix &lt;=c0amixfix []V12V27Iainfix &lt;V27V11Aainfix &lt;=c0V27FAamemV29adiffadiffV0V1V2IamemV29V8FAainfix =V11V5Aainfix &lt;=c0ainfix -V9V3Aainfix =V7ainfix +V9aprefix -V3FIamemV30V0NFNIainfix =ainfix -amixfix []V6V31amixfix []V6V32ainfix -V32V31NAainfix =ainfix -amixfix []V6V31amixfix []V6V32ainfix -V31V32NAainfix =amixfix []V6V31amixfix []V6V32NIainfix &lt;V32V31Aainfix &lt;=c0V32FAainfix &lt;amixfix []V6V31anAainfix &lt;=c0amixfix []V6V31Iainfix &lt;V31V5Aainfix &lt;=c0V31FAainfix =agetV6V34ainfix +ainfix +V33V5aprefix -V34NIainfix &lt;V34V5Aainfix =c0V34Oainfix &lt;c0V34FqamemV33V2NIainfix &lt;=c0V33FAainfix =agetV6V36ainfix +ainfix +V35V36aprefix -V5NIainfix &lt;V36V5Aainfix =c0V36Oainfix &lt;c0V36FqamemV35V1NIainfix &lt;=c0V35FAainfix =agetV6V38V37NIainfix &lt;V38V5Aainfix =c0V38Oainfix &lt;c0V38FAainfix &lt;V37anAainfix =c0V37Oainfix &lt;c0V37qamemV37V0FAainfix &lt;=c0V3Aainfix =ainfix +V5acardinalV0anAainfix =c0V5Oainfix &lt;c0V5FF">
<label
name="expl:VC for t3"/>
<proof
prover="5"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.72"/>
</proof>
<proof
prover="6"
timelimit="15"
memlimit="0"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="2.16"/>
......
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