Commit 1f929208 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

more outdated proof sessions replayed

parent 3309c2c1
......@@ -2,16 +2,19 @@
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/programs/euler001/why3session.xml">
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.2pl1"/>
<prover id="coq" name="Coq" version="8.3pl2"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="gappa" name="Gappa" version="0.13.0"/>
<prover id="gappa" name="Gappa" version="0.15.0"/>
<prover id="simplify" name="Simplify" version="1.5.4"/>
<prover id="spass" name="Spass" version="3.7"/>
<prover id="vampire" name="Vampire" version="0.6"/>
<prover id="yices" name="Yices" version="1.0.25"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../euler001.mlw" verified="false" expanded="true">
<theory name="SumMultiple" verified="false" expanded="true">
<goal name="div_minus1_1" sum="5266791566cb9e131f79837e51b72de8" proved="true" expanded="true" shape="ainfix =adivainfix +V0c1V1ainfix +adivV0V1c1Iainfix =amodainfix +V0c1V1c0Iainfix >V1c0Aainfix >=V0c0F">
<proof prover="coq" timelimit="5" edited="euler001_SumMultiple_div_minus1_1_1.v" obsolete="false">
<result status="valid" time="0.48"/>
<result status="valid" time="0.52"/>
</proof>
</goal>
<goal name="div_minus1_2" sum="b75e15f7119a97ac29920a7a789b8e15" proved="false" expanded="true" shape="ainfix =adivainfix +V0c1V1adivV0V1Iainfix =amodainfix +V0c1V1c0NIainfix >V1c0Aainfix >=V0c0F">
......@@ -24,9 +27,6 @@
<proof prover="alt-ergo" timelimit="5" edited="" obsolete="false">
<result status="unknown" time="0.23"/>
</proof>
<proof prover="z3" timelimit="5" edited="" obsolete="false">
<result status="timeout" time="5.06"/>
</proof>
</goal>
<goal name="Closed_formula_0" sum="9d635abb360eeba223e62aea7d54449e" proved="true" expanded="true" shape="apc0">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
......
......@@ -84,9 +84,6 @@
</proof>
</goal>
<goal name="consistent" sum="a65f10bfef659ef89fea02a802b02814" proved="false" expanded="true" shape="fIais_listV0V2Iais_listV0V1F">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="highfailure" time="0.10"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="unknown" time="0.09"/>
</proof>
......@@ -108,9 +105,6 @@
</proof>
</goal>
<goal name="consistent_behv" sum="0b862bd8bf335fb1f4d954cba7927dd5" proved="false" expanded="true" shape="fIais_listV0V2Iais_listV0V1F">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="highfailure" time="0.10"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="unknown" time="0.10"/>
</proof>
......
......@@ -2,56 +2,101 @@
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/programs/muller/why3session.xml">
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.2pl1"/>
<prover id="coq" name="Coq" version="8.3pl2"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="eprover" name="Eprover" version="1.0-004 Temi"/>
<prover id="gappa" name="Gappa" version="0.14.0"/>
<prover id="gappa" name="Gappa" version="0.15.0"/>
<prover id="simplify" name="Simplify" version="1.5.4"/>
<prover id="spass" name="Spass" version="3.5"/>
<prover id="yices" name="Yices" version="1.0.27"/>
<prover id="spass" name="Spass" version="3.7"/>
<prover id="vampire" name="Vampire" version="0.6"/>
<prover id="yices" name="Yices" version="1.0.25"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../muller.mlw" verified="true" expanded="true">
<theory name="WP Muller" verified="true" expanded="true">
<goal name="WP_parameter compact" expl="correctness of parameter compact" sum="575477ba237807b1bdc6273424ac9032" proved="true" expanded="true" shape="iainfix =agetV1V6c0Nainfix <=anum_ofV1c0ainfix +V6c1ainfix +V6c1Aainfix =V8anum_ofV1c0ainfix +V6c1Aainfix <=c0V8Iainfix =V8ainfix +V5c1FIainfix =V7asetV4V5agetV1V6FAainfix <V5V2Aainfix <=c0V5Aainfix <V6V0Aainfix <=c0V6ainfix <=anum_ofV1c0ainfix +V6c1ainfix +V6c1Aainfix =V5anum_ofV1c0ainfix +V6c1Aainfix <=c0V5Aainfix <V6V0Aainfix <=c0V6Iainfix <=anum_ofV1c0V6V6Aainfix =V5anum_ofV1c0V6Aainfix <=c0V5Iainfix <=V6ainfix -V0c1Aainfix <=c0V6FFFAainfix <=anum_ofV1c0c0c0Aainfix =V3anum_ofV1c0c0Aainfix <=c0V3Iainfix <=c0ainfix -V0c1Iainfix =V3c0FAainfix >=V2c0Iainfix <=anum_ofV1c0ainfix +ainfix -V0c1c1ainfix +ainfix -V0c1c1Aainfix =V2anum_ofV1c0ainfix +ainfix -V0c1c1Aainfix <=c0V2Aiainfix =agetV1V9c0Nainfix <=anum_ofV1c0ainfix +V9c1ainfix +V9c1Aainfix =V10anum_ofV1c0ainfix +V9c1Aainfix <=c0V10Iainfix =V10ainfix +V2c1Fainfix <=anum_ofV1c0ainfix +V9c1ainfix +V9c1Aainfix =V2anum_ofV1c0ainfix +V9c1Aainfix <=c0V2Aainfix <V9V0Aainfix <=c0V9Iainfix <=anum_ofV1c0V9V9Aainfix =V2anum_ofV1c0V9Aainfix <=c0V2Iainfix <=V9ainfix -V0c1Aainfix <=c0V9FFAainfix <=anum_ofV1c0c0c0Aainfix =c0anum_ofV1c0c0Aainfix <=c0c0Iainfix <=c0ainfix -V0c1Aiainfix =agetV1V14c0Nainfix <=anum_ofV1c0ainfix +V14c1ainfix +V14c1Aainfix =V16anum_ofV1c0ainfix +V14c1Aainfix <=c0V16Iainfix =V16ainfix +V13c1FIainfix =V15asetV12V13agetV1V14FAainfix <V13c0Aainfix <=c0V13Aainfix <V14V0Aainfix <=c0V14ainfix <=anum_ofV1c0ainfix +V14c1ainfix +V14c1Aainfix =V13anum_ofV1c0ainfix +V14c1Aainfix <=c0V13Aainfix <V14V0Aainfix <=c0V14Iainfix <=anum_ofV1c0V14V14Aainfix =V13anum_ofV1c0V14Aainfix <=c0V13Iainfix <=V14ainfix -V0c1Aainfix <=c0V14FFFAainfix <=anum_ofV1c0c0c0Aainfix =V11anum_ofV1c0c0Aainfix <=c0V11Iainfix <=c0ainfix -V0c1Iainfix =V11c0FAainfix >=c0c0Iainfix >c0ainfix -V0c1FF">
<goal name="WP_parameter compact" expl="correctness of parameter compact" sum="2a667703ae0bd2546e6a5bcce68215e2" proved="true" expanded="true" shape="iainfix =agetV1V6c0Nainfix <=anum_ofV1c0ainfix +V6c1ainfix +V6c1Aainfix =V8anum_ofV1c0ainfix +V6c1Aainfix <=c0V8Iainfix =V8ainfix +V5c1FIainfix =V7asetV4V5agetV1V6FAainfix <V5V2Aainfix <=c0V5Aainfix <V6V0Aainfix <=c0V6ainfix <=anum_ofV1c0ainfix +V6c1ainfix +V6c1Aainfix =V5anum_ofV1c0ainfix +V6c1Aainfix <=c0V5Aainfix <V6V0Aainfix <=c0V6Iainfix <=anum_ofV1c0V6V6Aainfix =V5anum_ofV1c0V6Aainfix <=c0V5Iainfix <=V6ainfix -V0c1Aainfix <=c0V6FFFAainfix <=anum_ofV1c0c0c0Aainfix =V3anum_ofV1c0c0Aainfix <=c0V3Iainfix <=c0ainfix -V0c1Iainfix =V3c0FAainfix >=V2c0Iainfix <=anum_ofV1c0ainfix +ainfix -V0c1c1ainfix +ainfix -V0c1c1Aainfix =V2anum_ofV1c0ainfix +ainfix -V0c1c1Aainfix <=c0V2Aiainfix =agetV1V9c0Nainfix <=anum_ofV1c0ainfix +V9c1ainfix +V9c1Aainfix =V10anum_ofV1c0ainfix +V9c1Aainfix <=c0V10Iainfix =V10ainfix +V2c1Fainfix <=anum_ofV1c0ainfix +V9c1ainfix +V9c1Aainfix =V2anum_ofV1c0ainfix +V9c1Aainfix <=c0V2Aainfix <V9V0Aainfix <=c0V9Iainfix <=anum_ofV1c0V9V9Aainfix =V2anum_ofV1c0V9Aainfix <=c0V2Iainfix <=V9ainfix -V0c1Aainfix <=c0V9FFAainfix <=anum_ofV1c0c0c0Aainfix =c0anum_ofV1c0c0Aainfix <=c0c0Iainfix <=c0ainfix -V0c1Aiainfix =agetV1V14c0Nainfix <=anum_ofV1c0ainfix +V14c1ainfix +V14c1Aainfix =V16anum_ofV1c0ainfix +V14c1Aainfix <=c0V16Iainfix =V16ainfix +V13c1FIainfix =V15asetV12V13agetV1V14FAainfix <V13c0Aainfix <=c0V13Aainfix <V14V0Aainfix <=c0V14ainfix <=anum_ofV1c0ainfix +V14c1ainfix +V14c1Aainfix =V13anum_ofV1c0ainfix +V14c1Aainfix <=c0V13Aainfix <V14V0Aainfix <=c0V14Iainfix <=anum_ofV1c0V14V14Aainfix =V13anum_ofV1c0V14Aainfix <=c0V13Iainfix <=V14ainfix -V0c1Aainfix <=c0V14FFFAainfix <=anum_ofV1c0c0c0Aainfix =V11anum_ofV1c0c0Aainfix <=c0V11Iainfix <=c0ainfix -V0c1Iainfix =V11c0FAainfix >=c0c0Iainfix >c0ainfix -V0c1FF">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter compact.1" expl="precondition" sum="8d7dd66c74645ad012bcb4ba69b4e9c5" proved="true" expanded="true" shape="ainfix >=c0c0Iainfix >c0ainfix -V0c1FF">
<goal name="WP_parameter compact.1" expl="precondition" sum="fe1ed72558fa02c7649baf75440eddee" proved="true" expanded="true" shape="ainfix >=c0c0Iainfix >c0ainfix -V0c1FF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal name="WP_parameter compact.2" expl="for loop initialization" sum="03fd0c9f0990b675ae4c9900f71ae387" proved="true" expanded="true" shape="ainfix <=anum_ofV1c0c0c0Aainfix =V2anum_ofV1c0c0Aainfix <=c0V2Iainfix <=c0ainfix -V0c1Iainfix =V2c0FIainfix >=c0c0Iainfix >c0ainfix -V0c1FF">
<goal name="WP_parameter compact.2" expl="for loop initialization" sum="3ed1b773959ceb7a52024ebc4194974e" proved="true" expanded="true" shape="ainfix <=anum_ofV1c0c0c0Aainfix =V2anum_ofV1c0c0Aainfix <=c0V2Iainfix <=c0ainfix -V0c1Iainfix =V2c0FIainfix >=c0c0Iainfix >c0ainfix -V0c1FF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter compact.3" expl="for loop preservation" sum="827e0ca995f60293b5d5e0adbd67f154" proved="true" expanded="true" shape="iainfix =agetV1V5c0Nainfix <=anum_ofV1c0ainfix +V5c1ainfix +V5c1Aainfix =V7anum_ofV1c0ainfix +V5c1Aainfix <=c0V7Iainfix =V7ainfix +V4c1FIainfix =V6asetV3V4agetV1V5FAainfix <V4c0Aainfix <=c0V4Aainfix <V5V0Aainfix <=c0V5ainfix <=anum_ofV1c0ainfix +V5c1ainfix +V5c1Aainfix =V4anum_ofV1c0ainfix +V5c1Aainfix <=c0V4Aainfix <V5V0Aainfix <=c0V5Iainfix <=anum_ofV1c0V5V5Aainfix =V4anum_ofV1c0V5Aainfix <=c0V4Iainfix <=V5ainfix -V0c1Aainfix <=c0V5FFFIainfix <=c0ainfix -V0c1Iainfix =V2c0FIainfix >=c0c0Iainfix >c0ainfix -V0c1FF">
<goal name="WP_parameter compact.3" expl="for loop preservation" sum="677d99d5ecc6e5ac8368b9d09fed6856" proved="true" expanded="true" shape="iainfix =agetV1V5c0Nainfix <=anum_ofV1c0ainfix +V5c1ainfix +V5c1Aainfix =V7anum_ofV1c0ainfix +V5c1Aainfix <=c0V7Iainfix =V7ainfix +V4c1FIainfix =V6asetV3V4agetV1V5FAainfix <V4c0Aainfix <=c0V4Aainfix <V5V0Aainfix <=c0V5ainfix <=anum_ofV1c0ainfix +V5c1ainfix +V5c1Aainfix =V4anum_ofV1c0ainfix +V5c1Aainfix <=c0V4Aainfix <V5V0Aainfix <=c0V5Iainfix <=anum_ofV1c0V5V5Aainfix =V4anum_ofV1c0V5Aainfix <=c0V4Iainfix <=V5ainfix -V0c1Aainfix <=c0V5FFFIainfix <=c0ainfix -V0c1Iainfix =V2c0FIainfix >=c0c0Iainfix >c0ainfix -V0c1FF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter compact.4" expl="for loop initialization" sum="c0e3d5971e572acd3db62fb9e102a17c" proved="true" expanded="true" shape="ainfix <=anum_ofV1c0c0c0Aainfix =c0anum_ofV1c0c0Aainfix <=c0c0Iainfix <=c0ainfix -V0c1FF">
<goal name="WP_parameter compact.4" expl="for loop initialization" sum="54fd31df334ff5908f557f9f523bf127" proved="true" expanded="true" shape="ainfix <=anum_ofV1c0c0c0Aainfix =c0anum_ofV1c0c0Aainfix <=c0c0Iainfix <=c0ainfix -V0c1FF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter compact.5" expl="for loop preservation" sum="4eac813b68d3b337fe13742d52c581ec" proved="true" expanded="true" shape="iainfix =agetV1V3c0Nainfix <=anum_ofV1c0ainfix +V3c1ainfix +V3c1Aainfix =V4anum_ofV1c0ainfix +V3c1Aainfix <=c0V4Iainfix =V4ainfix +V2c1Fainfix <=anum_ofV1c0ainfix +V3c1ainfix +V3c1Aainfix =V2anum_ofV1c0ainfix +V3c1Aainfix <=c0V2Aainfix <V3V0Aainfix <=c0V3Iainfix <=anum_ofV1c0V3V3Aainfix =V2anum_ofV1c0V3Aainfix <=c0V2Iainfix <=V3ainfix -V0c1Aainfix <=c0V3FFIainfix <=c0ainfix -V0c1FF">
<goal name="WP_parameter compact.5" expl="for loop preservation" sum="82366ff46d2e0bce36cdb8a1eb367eab" proved="true" expanded="true" shape="iainfix =agetV1V3c0Nainfix <=anum_ofV1c0ainfix +V3c1ainfix +V3c1Aainfix =V4anum_ofV1c0ainfix +V3c1Aainfix <=c0V4Iainfix =V4ainfix +V2c1Fainfix <=anum_ofV1c0ainfix +V3c1ainfix +V3c1Aainfix =V2anum_ofV1c0ainfix +V3c1Aainfix <=c0V2Aainfix <V3V0Aainfix <=c0V3Iainfix <=anum_ofV1c0V3V3Aainfix =V2anum_ofV1c0V3Aainfix <=c0V2Iainfix <=V3ainfix -V0c1Aainfix <=c0V3FFIainfix <=c0ainfix -V0c1FF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.05"/>
<result status="valid" time="0.04"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter compact.6" expl="precondition" sum="ac8613151f21c8de359a74b14fe8d685" proved="true" expanded="true" shape="ainfix >=V2c0Iainfix <=anum_ofV1c0ainfix +ainfix -V0c1c1ainfix +ainfix -V0c1c1Aainfix =V2anum_ofV1c0ainfix +ainfix -V0c1c1Aainfix <=c0V2FIainfix <=c0ainfix -V0c1FF">
<goal name="WP_parameter compact.6" expl="precondition" sum="c3bcae7570c08fd26367c6590f50f999" proved="true" expanded="true" shape="ainfix >=V2c0Iainfix <=anum_ofV1c0ainfix +ainfix -V0c1c1ainfix +ainfix -V0c1c1Aainfix =V2anum_ofV1c0ainfix +ainfix -V0c1c1Aainfix <=c0V2FIainfix <=c0ainfix -V0c1FF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter compact.7" expl="for loop initialization" sum="91b3b71e3aa4085f46b334874ed43523" proved="true" expanded="true" shape="ainfix <=anum_ofV1c0c0c0Aainfix =V3anum_ofV1c0c0Aainfix <=c0V3Iainfix <=c0ainfix -V0c1Iainfix =V3c0FIainfix >=V2c0Iainfix <=anum_ofV1c0ainfix +ainfix -V0c1c1ainfix +ainfix -V0c1c1Aainfix =V2anum_ofV1c0ainfix +ainfix -V0c1c1Aainfix <=c0V2FIainfix <=c0ainfix -V0c1FF">
<goal name="WP_parameter compact.7" expl="for loop initialization" sum="c0c622258ee68d32ea97e4ca350cad11" proved="true" expanded="true" shape="ainfix <=anum_ofV1c0c0c0Aainfix =V3anum_ofV1c0c0Aainfix <=c0V3Iainfix <=c0ainfix -V0c1Iainfix =V3c0FIainfix >=V2c0Iainfix <=anum_ofV1c0ainfix +ainfix -V0c1c1ainfix +ainfix -V0c1c1Aainfix =V2anum_ofV1c0ainfix +ainfix -V0c1c1Aainfix <=c0V2FIainfix <=c0ainfix -V0c1FF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter compact.8" expl="for loop preservation" sum="2d023239305c16adcd550f8e1e0ab414" proved="true" expanded="true" shape="iainfix =agetV1V6c0Nainfix <=anum_ofV1c0ainfix +V6c1ainfix +V6c1Aainfix =V8anum_ofV1c0ainfix +V6c1Aainfix <=c0V8Iainfix =V8ainfix +V5c1FIainfix =V7asetV4V5agetV1V6FAainfix <V5V2Aainfix <=c0V5Aainfix <V6V0Aainfix <=c0V6ainfix <=anum_ofV1c0ainfix +V6c1ainfix +V6c1Aainfix =V5anum_ofV1c0ainfix +V6c1Aainfix <=c0V5Aainfix <V6V0Aainfix <=c0V6Iainfix <=anum_ofV1c0V6V6Aainfix =V5anum_ofV1c0V6Aainfix <=c0V5Iainfix <=V6ainfix -V0c1Aainfix <=c0V6FFFIainfix <=c0ainfix -V0c1Iainfix =V3c0FIainfix >=V2c0Iainfix <=anum_ofV1c0ainfix +ainfix -V0c1c1ainfix +ainfix -V0c1c1Aainfix =V2anum_ofV1c0ainfix +ainfix -V0c1c1Aainfix <=c0V2FIainfix <=c0ainfix -V0c1FF">
<goal name="WP_parameter compact.8" expl="for loop preservation" sum="84526c6dc897baeb2f377018fec741e0" proved="true" expanded="true" shape="iainfix =agetV1V6c0Nainfix <=anum_ofV1c0ainfix +V6c1ainfix +V6c1Aainfix =V8anum_ofV1c0ainfix +V6c1Aainfix <=c0V8Iainfix =V8ainfix +V5c1FIainfix =V7asetV4V5agetV1V6FAainfix <V5V2Aainfix <=c0V5Aainfix <V6V0Aainfix <=c0V6ainfix <=anum_ofV1c0ainfix +V6c1ainfix +V6c1Aainfix =V5anum_ofV1c0ainfix +V6c1Aainfix <=c0V5Aainfix <V6V0Aainfix <=c0V6Iainfix <=anum_ofV1c0V6V6Aainfix =V5anum_ofV1c0V6Aainfix <=c0V5Iainfix <=V6ainfix -V0c1Aainfix <=c0V6FFFIainfix <=c0ainfix -V0c1Iainfix =V3c0FIainfix >=V2c0Iainfix <=anum_ofV1c0ainfix +ainfix -V0c1c1ainfix +ainfix -V0c1c1Aainfix =V2anum_ofV1c0ainfix +ainfix -V0c1c1Aainfix <=c0V2FIainfix <=c0ainfix -V0c1FF">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.12"/>
<result status="valid" time="0.08"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
</transf>
......
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