Commit 0cefbf9d authored by MARCHE Claude's avatar MARCHE Claude

update sessions after change in Vampire driver

parent f33839b6
......@@ -166,41 +166,6 @@
proved="false"
expanded="true"
shape="iainfix =V0c0ainfix =apoweramk tc1c1c1c0V0amk tainfix +c1c0c0c0c1Ciainfix =amodV0c2c0aTuple2ainfix +ainfix *V1V1ainfix *V2V2ainfix *V2ainfix +V1ainfix +V1V2aTuple2ainfix *V2ainfix +V1ainfix +V1V2ainfix +ainfix *ainfix +V1V2ainfix +V1V2ainfix *V2V2aTuple2VVainfix =apoweramk tc1c1c1c0V0amk tainfix +V3V4V4V4V3Iainfix =apoweramk tc1c1c1c0adivV0c2amk tainfix +V1V2V2V2V1FAainfix >=adivV0c2c0Aainfix <adivV0c2V0Aainfix <=c0V0Iainfix >=V0c0F">
<proof
prover="cvc3"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.04"/>
</proof>
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.03"/>
</proof>
<proof
prover="eprover"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="4.98"/>
</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>
<transf
name="split_goal"
proved="false"
......@@ -248,6 +213,13 @@
proved="true"
expanded="true"
shape="ainfix >=adivV0c2c0Aainfix <adivV0c2V0Aainfix <=c0V0Iainfix =V0c0NIainfix >=V0c0F">
<proof
prover="alt-ergo"
timelimit="3"
edited=""
obsolete="false">
<result status="unknown" time="0.02"/>
</proof>
<proof
prover="cvc3"
timelimit="5"
......@@ -267,7 +239,7 @@
timelimit="3"
edited=""
obsolete="false">
<result status="timeout" time="2.98"/>
<result status="timeout" time="2.99"/>
</proof>
</goal>
<goal
......@@ -289,7 +261,7 @@
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.02"/>
<result status="timeout" time="3.02"/>
</proof>
<proof
prover="z3"
......@@ -314,41 +286,6 @@
proved="false"
expanded="true"
shape="Lapoweram1110V0ainfix =afibV0aa21V1Aainfix =afibainfix +V0c1aa11V1Iainfix >=V0c0F">
<proof
prover="cvc3"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.05"/>
</proof>
<proof
prover="alt-ergo"
timelimit="5"
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="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.32"/>
</proof>
<transf
name="split_goal"
proved="false"
......@@ -420,7 +357,7 @@
timelimit="3"
edited=""
obsolete="false">
<result status="timeout" time="2.99"/>
<result status="timeout" time="2.98"/>
</proof>
</goal>
</transf>
......@@ -451,7 +388,7 @@
timelimit="3"
edited=""
obsolete="false">
<result status="timeout" time="3.02"/>
<result status="timeout" time="2.99"/>
</proof>
</goal>
</theory>
......
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