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

Scottish Club and Einstein

parent 61e9958d
......@@ -146,8 +146,6 @@ why.conf
# /examples/
/examples/my_cosine/
/examples/scottish-private-club/
/examples/einstein/
/examples/genealogy/
/examples/programs/isqrt/
/examples/programs/course/
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/einstein/why3session.xml">
<file name="../einstein.why" verified="false" expanded="true">
<theory name="Bijection" verified="true" expanded="true">
</theory>
<theory name="Einstein" verified="true" expanded="true">
</theory>
<theory name="EinsteinHints" verified="true" expanded="true">
</theory>
<theory name="Goals" verified="false" expanded="true">
<goal name="G1" sum="3ac4d6944c1b5acf60b54d125510b5ce" proved="true" expanded="true">
<proof prover="z3" edited="" obsolete="false">
<result status="valid" time="0.08"/>
</proof>
</goal>
<goal name="G2" sum="1dfddc09f50e2271f110483bc42e7472" proved="false" expanded="true">
<proof prover="cvc3" edited="" obsolete="false">
<result status="unknown" time="0.42"/>
</proof>
<proof prover="simplify" edited="" obsolete="false">
<result status="timeout" time="10.06"/>
</proof>
<proof prover="alt-ergo" edited="" obsolete="false">
<result status="unknown" time="1.00"/>
</proof>
<proof prover="z3" edited="" obsolete="false">
<result status="timeout" time="10.03"/>
</proof>
<proof prover="gappa" edited="" obsolete="false">
<result status="unknown" time="0.01"/>
</proof>
</goal>
</theory>
</file>
</why3session>
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/scottish-private-club/why3session.xml">
<file name="../scottish-private-club.why" verified="true" expanded="true">
<theory name="ScottishClubProblem" verified="true" expanded="true">
<goal name="ThereIsNobodyInTheClub" sum="fdd6f04d95bf043a8b2934a2bd2c47ad" proved="true" expanded="true">
<proof prover="coq" edited="" obsolete="false">
<result status="unknown" time="0.46"/>
</proof>
<proof prover="cvc3" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="alt-ergo" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="simplify" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="gappa" edited="" obsolete="false">
<result status="unknown" time="0.01"/>
</proof>
<proof prover="z3" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
</theory>
</file>
</why3session>
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