updated proof

examples/programs/decrease1/why3session.xml

 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session SYSTEM "why3session.dtd">
-<why3session name="programs/decrease1/why3session.xml">
- <prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
- <prover id="coq" name="Coq" version="8.2pl1"/>
- <prover id="cvc3" name="CVC3" version="2.2"/>
- <prover id="gappa" name="Gappa" version="0.13.0"/>
- <prover id="simplify" name="Simplify" version="1.5.4"/>
- <prover id="z3" name="Z3" version="2.19"/>
- <file name="../decrease1.mlw" verified="true" expanded="true">
-  <theory name="WP Decrease1" verified="true" expanded="true">
-   <goal name="decrease1_induction" sum="0b5a5fde45e86c1bc677f99c692e19db" proved="true" expanded="true" shape="ainfix >=amixfix []V0V2ainfix -ainfix +amixfix []V0V1V1V2Iainfix <V2alengthV0Aainfix <=V1V2Aainfix <=c0V1FIadecrease1V0F">
-    <proof prover="coq" timelimit="10" edited="decrease1_Decrease1_decrease1_induction_2.v" obsolete="false">
-     <result status="valid" time="0.89"/>
+<why3session
+ name="examples/programs/decrease1/why3session.xml">
+ <prover
+  id="alt-ergo"
+  name="Alt-Ergo"
+  version="0.93"/>
+ <prover
+  id="coq"
+  name="Coq"
+  version="8.3pl2"/>
+ <prover
+  id="cvc3"
+  name="CVC3"
+  version="2.2"/>
+ <prover
+  id="simplify"
+  name="Simplify"
+  version="1.5.4"/>
+ <prover
+  id="yices"
+  name="Yices"
+  version="1.0.27"/>
+ <prover
+  id="z3"
+  name="Z3"
+  version="2.19"/>
+ <file
+  name="../decrease1.mlw"
+  verified="true"
+  expanded="true">
+  <theory
+   name="WP Decrease1"
+   verified="true"
+   expanded="true">
+   <goal
+    name="decrease1_induction"
+    sum="0b5a5fde45e86c1bc677f99c692e19db"
+    proved="true"
+    expanded="true"
+    shape="ainfix >=amixfix []V0V2ainfix -ainfix +amixfix []V0V1V1V2Iainfix <V2alengthV0Aainfix <=V1V2Aainfix <=c0V1FIadecrease1V0F">
+    <proof
+     prover="coq"
+     timelimit="10"
+     edited="decrease1_Decrease1_decrease1_induction_2.v"
+     obsolete="false">
+     <result status="valid" time="0.85"/>
     </proof>
    </goal>
-   <goal name="WP_parameter search" expl="parameter search" sum="32db91f9d0b74d7901921f96c785e138" proved="true" expanded="true" shape="iainfix <V2V0iainfix =agetV1V2c0ainfix =agetV1V3c0NIainfix <V3V2Aainfix <=c0V3FAainfix =agetV1V2c0Aainfix <V2V0Aainfix <=c0V2Oainfix =agetV1V4c0NIainfix <V4V0Aainfix <=c0V4FAainfix =V2aprefix -c1iainfix >agetV1V2c0ainfix <ainfix -V0V5ainfix -V0V2Aainfix <=c0ainfix -V0V2Aainfix =agetV1V6c0NIainfix <V6V0Iainfix <V6V5Aainfix <=c0V6FAainfix <=c0V5Iainfix =V5ainfix +V2agetV1V2FAainfix <V2V0Aainfix <=c0V2ainfix <ainfix -V0V7ainfix -V0V2Aainfix <=c0ainfix -V0V2Aainfix =agetV1V8c0NIainfix <V8V0Iainfix <V8V7Aainfix <=c0V8FAainfix <=c0V7Iainfix =V7ainfix +V2c1FAainfix <V2V0Aainfix <=c0V2Aainfix <V2V0Aainfix <=c0V2ainfix =agetV1V9c0NIainfix <V9aprefix -c1Aainfix <=c0V9FAainfix =agetV1aprefix -c1c0Aainfix <aprefix -c1V0Aainfix <=c0aprefix -c1Oainfix =agetV1V10c0NIainfix <V10V0Aainfix <=c0V10FAainfix =aprefix -c1aprefix -c1Iainfix =agetV1V11c0NIainfix <V11V0Iainfix <V11V2Aainfix <=c0V11FAainfix <=c0V2FAainfix =agetV1V12c0NIainfix <V12V0Iainfix <V12c0Aainfix <=c0V12FAainfix <=c0c0Iadecrease1amk arrayV0V1FF">
-    <transf name="split_goal" proved="true" expanded="true">
-     <goal name="WP_parameter search.1" expl="loop invariant init" sum="f429462d6359f2a28844ffc1a8f1eec0" proved="true" expanded="true" shape="ainfix =agetV1V2c0NIainfix <V2V0Iainfix <V2c0Aainfix <=c0V2FAainfix <=c0c0Iadecrease1amk arrayV0V1FF">
-      <proof prover="cvc3" timelimit="10" edited="" obsolete="false">
+   <goal
+    name="WP_parameter search"
+    expl="parameter search"
+    sum="32db91f9d0b74d7901921f96c785e138"
+    proved="true"
+    expanded="true"
+    shape="iainfix <V2V0iainfix =agetV1V2c0ainfix =agetV1V3c0NIainfix <V3V2Aainfix <=c0V3FAainfix =agetV1V2c0Aainfix <V2V0Aainfix <=c0V2Oainfix =agetV1V4c0NIainfix <V4V0Aainfix <=c0V4FAainfix =V2aprefix -c1iainfix >agetV1V2c0ainfix <ainfix -V0V5ainfix -V0V2Aainfix <=c0ainfix -V0V2Aainfix =agetV1V6c0NIainfix <V6V0Iainfix <V6V5Aainfix <=c0V6FAainfix <=c0V5Iainfix =V5ainfix +V2agetV1V2FAainfix <V2V0Aainfix <=c0V2ainfix <ainfix -V0V7ainfix -V0V2Aainfix <=c0ainfix -V0V2Aainfix =agetV1V8c0NIainfix <V8V0Iainfix <V8V7Aainfix <=c0V8FAainfix <=c0V7Iainfix =V7ainfix +V2c1FAainfix <V2V0Aainfix <=c0V2Aainfix <V2V0Aainfix <=c0V2ainfix =agetV1V9c0NIainfix <V9aprefix -c1Aainfix <=c0V9FAainfix =agetV1aprefix -c1c0Aainfix <aprefix -c1V0Aainfix <=c0aprefix -c1Oainfix =agetV1V10c0NIainfix <V10V0Aainfix <=c0V10FAainfix =aprefix -c1aprefix -c1Iainfix =agetV1V11c0NIainfix <V11V0Iainfix <V11V2Aainfix <=c0V11FAainfix <=c0V2FAainfix =agetV1V12c0NIainfix <V12V0Iainfix <V12c0Aainfix <=c0V12FAainfix <=c0c0Iadecrease1amk arrayV0V1FF">
+    <transf
+     name="split_goal"
+     proved="true"
+     expanded="true">
+     <goal
+      name="WP_parameter search.1"
+      expl="loop invariant init"
+      sum="f429462d6359f2a28844ffc1a8f1eec0"
+      proved="true"
+      expanded="true"
+      shape="ainfix =agetV1V2c0NIainfix <V2V0Iainfix <V2c0Aainfix <=c0V2FAainfix <=c0c0Iadecrease1amk arrayV0V1FF">
+      <proof
+       prover="cvc3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.02"/>
       </proof>
-      <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
+      <proof
+       prover="alt-ergo"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.03"/>
       </proof>
-      <proof prover="z3" timelimit="10" edited="" obsolete="false">
+      <proof
+       prover="z3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.01"/>
       </proof>
      </goal>
-     <goal name="WP_parameter search.2" expl="precondition" sum="00f49e69817e47e187436aba2e90adce" proved="true" expanded="true" shape="ainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V3c0NIainfix <V3V0Iainfix <V3V2Aainfix <=c0V3FAainfix <=c0V2FIadecrease1amk arrayV0V1FF">
-      <proof prover="cvc3" timelimit="10" edited="" obsolete="false">
+     <goal
+      name="WP_parameter search.2"
+      expl="precondition"
+      sum="00f49e69817e47e187436aba2e90adce"
+      proved="true"
+      expanded="true"
+      shape="ainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V3c0NIainfix <V3V0Iainfix <V3V2Aainfix <=c0V3FAainfix <=c0V2FIadecrease1amk arrayV0V1FF">
+      <proof
+       prover="cvc3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.02"/>
       </proof>
-      <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
+      <proof
+       prover="alt-ergo"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.02"/>
       </proof>
-      <proof prover="z3" timelimit="10" edited="" obsolete="false">
+      <proof
+       prover="z3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.04"/>
       </proof>
      </goal>
-     <goal name="WP_parameter search.3" expl="normal postcondition" sum="1f5739e3fba1f66944af9f0ce685a8af" proved="true" expanded="true" shape="ainfix =agetV1V3c0NIainfix <V3V2Aainfix <=c0V3FAainfix =agetV1V2c0Aainfix <V2V0Aainfix <=c0V2Oainfix =agetV1V4c0NIainfix <V4V0Aainfix <=c0V4FAainfix =V2aprefix -c1Iainfix =agetV1V2c0Iainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V5c0NIainfix <V5V0Iainfix <V5V2Aainfix <=c0V5FAainfix <=c0V2FIadecrease1amk arrayV0V1FF">
-      <proof prover="cvc3" timelimit="10" edited="" obsolete="false">
+     <goal
+      name="WP_parameter search.3"
+      expl="normal postcondition"
+      sum="1f5739e3fba1f66944af9f0ce685a8af"
+      proved="true"
+      expanded="true"
+      shape="ainfix =agetV1V3c0NIainfix <V3V2Aainfix <=c0V3FAainfix =agetV1V2c0Aainfix <V2V0Aainfix <=c0V2Oainfix =agetV1V4c0NIainfix <V4V0Aainfix <=c0V4FAainfix =V2aprefix -c1Iainfix =agetV1V2c0Iainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V5c0NIainfix <V5V0Iainfix <V5V2Aainfix <=c0V5FAainfix <=c0V2FIadecrease1amk arrayV0V1FF">
+      <proof
+       prover="cvc3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.02"/>
       </proof>
-      <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
+      <proof
+       prover="alt-ergo"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.02"/>
       </proof>
-      <proof prover="z3" timelimit="10" edited="" obsolete="false">
+      <proof
+       prover="z3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.04"/>
       </proof>
      </goal>
-     <goal name="WP_parameter search.4" expl="precondition" sum="95604080b163273becaafe2a7359ed70" proved="true" expanded="true" shape="ainfix <V2V0Aainfix <=c0V2Iainfix =agetV1V2c0NIainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V3c0NIainfix <V3V0Iainfix <V3V2Aainfix <=c0V3FAainfix <=c0V2FIadecrease1amk arrayV0V1FF">
-      <proof prover="cvc3" timelimit="10" edited="" obsolete="false">
+     <goal
+      name="WP_parameter search.4"
+      expl="precondition"
+      sum="95604080b163273becaafe2a7359ed70"
+      proved="true"
+      expanded="true"
+      shape="ainfix <V2V0Aainfix <=c0V2Iainfix =agetV1V2c0NIainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V3c0NIainfix <V3V0Iainfix <V3V2Aainfix <=c0V3FAainfix <=c0V2FIadecrease1amk arrayV0V1FF">
+      <proof
+       prover="cvc3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.01"/>
       </proof>
-      <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
+      <proof
+       prover="alt-ergo"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.02"/>
       </proof>
-      <proof prover="z3" timelimit="10" edited="" obsolete="false">
+      <proof
+       prover="z3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.01"/>
       </proof>
      </goal>
-     <goal name="WP_parameter search.5" expl="precondition" sum="2b8983833e9bb6c69fd2af502f0fc8f1" proved="true" expanded="true" shape="ainfix <V2V0Aainfix <=c0V2Iainfix >agetV1V2c0Iainfix <V2V0Aainfix <=c0V2Iainfix =agetV1V2c0NIainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V3c0NIainfix <V3V0Iainfix <V3V2Aainfix <=c0V3FAainfix <=c0V2FIadecrease1amk arrayV0V1FF">
-      <proof prover="cvc3" timelimit="10" edited="" obsolete="false">
+     <goal
+      name="WP_parameter search.5"
+      expl="precondition"
+      sum="2b8983833e9bb6c69fd2af502f0fc8f1"
+      proved="true"
+      expanded="true"
+      shape="ainfix <V2V0Aainfix <=c0V2Iainfix >agetV1V2c0Iainfix <V2V0Aainfix <=c0V2Iainfix =agetV1V2c0NIainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V3c0NIainfix <V3V0Iainfix <V3V2Aainfix <=c0V3FAainfix <=c0V2FIadecrease1amk arrayV0V1FF">
+      <proof
+       prover="cvc3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.01"/>
       </proof>
-      <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
+      <proof
+       prover="alt-ergo"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.00"/>
       </proof>
-      <proof prover="z3" timelimit="10" edited="" obsolete="false">
+      <proof
+       prover="z3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.01"/>
       </proof>
      </goal>
-     <goal name="WP_parameter search.6" expl="loop invariant preservation" sum="6a36a0475249bf791db39eb5c7d764dd" proved="true" expanded="true" shape="ainfix =agetV1V4c0NIainfix <V4V0Iainfix <V4V3Aainfix <=c0V4FAainfix <=c0V3Iainfix =V3ainfix +V2agetV1V2FIainfix <V2V0Aainfix <=c0V2Iainfix >agetV1V2c0Iainfix <V2V0Aainfix <=c0V2Iainfix =agetV1V2c0NIainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V5c0NIainfix <V5V0Iainfix <V5V2Aainfix <=c0V5FAainfix <=c0V2FIadecrease1amk arrayV0V1FF">
-      <proof prover="z3" timelimit="10" edited="" obsolete="false">
+     <goal
+      name="WP_parameter search.6"
+      expl="loop invariant preservation"
+      sum="6a36a0475249bf791db39eb5c7d764dd"
+      proved="true"
+      expanded="true"
+      shape="ainfix =agetV1V4c0NIainfix <V4V0Iainfix <V4V3Aainfix <=c0V4FAainfix <=c0V3Iainfix =V3ainfix +V2agetV1V2FIainfix <V2V0Aainfix <=c0V2Iainfix >agetV1V2c0Iainfix <V2V0Aainfix <=c0V2Iainfix =agetV1V2c0NIainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V5c0NIainfix <V5V0Iainfix <V5V2Aainfix <=c0V5FAainfix <=c0V2FIadecrease1amk arrayV0V1FF">
+      <proof
+       prover="z3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.03"/>
       </proof>
      </goal>
-     <goal name="WP_parameter search.7" expl="loop variant decreases" sum="398b995dc98dce086663c5b3c6574fa4" proved="true" expanded="true" shape="ainfix <ainfix -V0V3ainfix -V0V2Aainfix <=c0ainfix -V0V2Iainfix =agetV1V4c0NIainfix <V4V0Iainfix <V4V3Aainfix <=c0V4FAainfix <=c0V3Iainfix =V3ainfix +V2agetV1V2FIainfix <V2V0Aainfix <=c0V2Iainfix >agetV1V2c0Iainfix <V2V0Aainfix <=c0V2Iainfix =agetV1V2c0NIainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V5c0NIainfix <V5V0Iainfix <V5V2Aainfix <=c0V5FAainfix <=c0V2FIadecrease1amk arrayV0V1FF">
-      <proof prover="cvc3" timelimit="10" edited="" obsolete="false">
+     <goal
+      name="WP_parameter search.7"
+      expl="loop variant decreases"
+      sum="398b995dc98dce086663c5b3c6574fa4"
+      proved="true"
+      expanded="true"
+      shape="ainfix <ainfix -V0V3ainfix -V0V2Aainfix <=c0ainfix -V0V2Iainfix =agetV1V4c0NIainfix <V4V0Iainfix <V4V3Aainfix <=c0V4FAainfix <=c0V3Iainfix =V3ainfix +V2agetV1V2FIainfix <V2V0Aainfix <=c0V2Iainfix >agetV1V2c0Iainfix <V2V0Aainfix <=c0V2Iainfix =agetV1V2c0NIainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V5c0NIainfix <V5V0Iainfix <V5V2Aainfix <=c0V5FAainfix <=c0V2FIadecrease1amk arrayV0V1FF">
+      <proof
+       prover="cvc3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.02"/>
       </proof>
-      <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
+      <proof
+       prover="alt-ergo"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.02"/>
       </proof>
-      <proof prover="z3" timelimit="10" edited="" obsolete="false">
+      <proof
+       prover="z3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.03"/>
       </proof>
      </goal>
-     <goal name="WP_parameter search.8" expl="loop invariant preservation" sum="1a3bff3b15bb3fdf49ebc51902f24106" proved="true" expanded="true" shape="ainfix =agetV1V4c0NIainfix <V4V0Iainfix <V4V3Aainfix <=c0V4FAainfix <=c0V3Iainfix =V3ainfix +V2c1FIainfix >agetV1V2c0NIainfix <V2V0Aainfix <=c0V2Iainfix =agetV1V2c0NIainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V5c0NIainfix <V5V0Iainfix <V5V2Aainfix <=c0V5FAainfix <=c0V2FIadecrease1amk arrayV0V1FF">
-      <proof prover="cvc3" timelimit="10" edited="" obsolete="false">
+     <goal
+      name="WP_parameter search.8"
+      expl="loop invariant preservation"
+      sum="1a3bff3b15bb3fdf49ebc51902f24106"
+      proved="true"
+      expanded="true"
+      shape="ainfix =agetV1V4c0NIainfix <V4V0Iainfix <V4V3Aainfix <=c0V4FAainfix <=c0V3Iainfix =V3ainfix +V2c1FIainfix >agetV1V2c0NIainfix <V2V0Aainfix <=c0V2Iainfix =agetV1V2c0NIainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V5c0NIainfix <V5V0Iainfix <V5V2Aainfix <=c0V5FAainfix <=c0V2FIadecrease1amk arrayV0V1FF">
+      <proof
+       prover="cvc3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.02"/>
       </proof>
-      <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
+      <proof
+       prover="alt-ergo"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.01"/>
       </proof>
-      <proof prover="z3" timelimit="10" edited="" obsolete="false">
+      <proof
+       prover="z3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.03"/>
       </proof>
      </goal>
-     <goal name="WP_parameter search.9" expl="loop variant decreases" sum="03a9f221f0aee9832c97b32f4d081dff" proved="true" expanded="true" shape="ainfix <ainfix -V0V3ainfix -V0V2Aainfix <=c0ainfix -V0V2Iainfix =agetV1V4c0NIainfix <V4V0Iainfix <V4V3Aainfix <=c0V4FAainfix <=c0V3Iainfix =V3ainfix +V2c1FIainfix >agetV1V2c0NIainfix <V2V0Aainfix <=c0V2Iainfix =agetV1V2c0NIainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V5c0NIainfix <V5V0Iainfix <V5V2Aainfix <=c0V5FAainfix <=c0V2FIadecrease1amk arrayV0V1FF">
-      <proof prover="cvc3" timelimit="10" edited="" obsolete="false">
+     <goal
+      name="WP_parameter search.9"
+      expl="loop variant decreases"
+      sum="03a9f221f0aee9832c97b32f4d081dff"
+      proved="true"
+      expanded="true"
+      shape="ainfix <ainfix -V0V3ainfix -V0V2Aainfix <=c0ainfix -V0V2Iainfix =agetV1V4c0NIainfix <V4V0Iainfix <V4V3Aainfix <=c0V4FAainfix <=c0V3Iainfix =V3ainfix +V2c1FIainfix >agetV1V2c0NIainfix <V2V0Aainfix <=c0V2Iainfix =agetV1V2c0NIainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V5c0NIainfix <V5V0Iainfix <V5V2Aainfix <=c0V5FAainfix <=c0V2FIadecrease1amk arrayV0V1FF">
+      <proof
+       prover="cvc3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.02"/>
       </proof>
-      <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
+      <proof
+       prover="alt-ergo"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.01"/>
       </proof>
-      <proof prover="z3" timelimit="10" edited="" obsolete="false">
+      <proof
+       prover="z3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.03"/>
       </proof>
      </goal>
-     <goal name="WP_parameter search.10" expl="normal postcondition" sum="b7a4163603ffae8e388b3b584fa1c482" proved="true" expanded="true" shape="ainfix =agetV1V3c0NIainfix <V3aprefix -c1Aainfix <=c0V3FAainfix =agetV1aprefix -c1c0Aainfix <aprefix -c1V0Aainfix <=c0aprefix -c1Oainfix =agetV1V4c0NIainfix <V4V0Aainfix <=c0V4FAainfix =aprefix -c1aprefix -c1Iainfix <V2V0NIainfix =agetV1V5c0NIainfix <V5V0Iainfix <V5V2Aainfix <=c0V5FAainfix <=c0V2FIadecrease1amk arrayV0V1FF">
-      <proof prover="cvc3" timelimit="10" edited="" obsolete="false">
+     <goal
+      name="WP_parameter search.10"
+      expl="normal postcondition"
+      sum="b7a4163603ffae8e388b3b584fa1c482"
+      proved="true"
+      expanded="true"
+      shape="ainfix =agetV1V3c0NIainfix <V3aprefix -c1Aainfix <=c0V3FAainfix =agetV1aprefix -c1c0Aainfix <aprefix -c1V0Aainfix <=c0aprefix -c1Oainfix =agetV1V4c0NIainfix <V4V0Aainfix <=c0V4FAainfix =aprefix -c1aprefix -c1Iainfix <V2V0NIainfix =agetV1V5c0NIainfix <V5V0Iainfix <V5V2Aainfix <=c0V5FAainfix <=c0V2FIadecrease1amk arrayV0V1FF">
+      <proof
+       prover="cvc3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.02"/>
       </proof>
-      <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
+      <proof
+       prover="alt-ergo"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.00"/>
       </proof>
-      <proof prover="z3" timelimit="10" edited="" obsolete="false">
+      <proof
+       prover="z3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.03"/>
       </proof>
      </goal>
     </transf>
    </goal>
-   <goal name="WP_parameter search_rec" expl="parameter search_rec" sum="218de42f33228231b48bf03e7dd8c864" proved="true" expanded="true" shape="Lamk arrayV0V2iainfix <V1V0iainfix =agetV2V1c0ainfix =agetV2V4c0NIainfix <V4V1Aainfix <=V1V4FAainfix =agetV2V1c0Aainfix <V1V0Aainfix <=V1V1Oainfix =agetV2V5c0NIainfix <V5V0Aainfix <=V1V5FAainfix =V1aprefix -c1iainfix >agetV2V1c0LagetV2V1ainfix =agetV2V8c0NIainfix <V8V7Aainfix <=V1V8FAainfix =agetV2V7c0Aainfix <V7V0Aainfix <=V1V7Oainfix =agetV2V9c0NIainfix <V9V0Aainfix <=V1V9FAainfix =V7aprefix -c1Iainfix =agetV2V10c0NIainfix <V10V7Aainfix <=ainfix +V1V6V10FAainfix =agetV2V7c0Aainfix <V7V0Aainfix <=ainfix +V1V6V7Oainfix =agetV2V11c0NIainfix <V11V0Aainfix <=ainfix +V1V6V11FAainfix =V7aprefix -c1FAainfix <=c0ainfix +V1V6Aadecrease1V3Aainfix <V1V0Aainfix <=c0V1ainfix =agetV2V13c0NIainfix <V13V12Aainfix <=V1V13FAainfix =agetV2V12c0Aainfix <V12V0Aainfix <=V1V12Oainfix =agetV2V14c0NIainfix <V14V0Aainfix <=V1V14FAainfix =V12aprefix -c1Iainfix =agetV2V15c0NIainfix <V15V12Aainfix <=ainfix +V1c1V15FAainfix =agetV2V12c0Aainfix <V12V0Aainfix <=ainfix +V1c1V12Oainfix =agetV2V16c0NIainfix <V16V0Aainfix <=ainfix +V1c1V16FAainfix =V12aprefix -c1FAainfix <=c0ainfix +V1c1Aadecrease1V3Aainfix <V1V0Aainfix <=c0V1Aainfix <V1V0Aainfix <=c0V1ainfix =agetV2V17c0NIainfix <V17aprefix -c1Aainfix <=V1V17FAainfix =agetV2aprefix -c1c0Aainfix <aprefix -c1V0Aainfix <=V1aprefix -c1Oainfix =agetV2V18c0NIainfix <V18V0Aainfix <=V1V18FAainfix =aprefix -c1aprefix -c1Iainfix <=c0V1Aadecrease1V3FFF">
-    <transf name="split_goal" proved="true" expanded="true">
-     <goal name="WP_parameter search_rec.1" expl="precondition" sum="d73590a15ec326b1799b3f5e0bfd8a07" proved="true" expanded="true" shape="Lamk arrayV0V2ainfix <V1V0Aainfix <=c0V1Iainfix <V1V0Iainfix <=c0V1Aadecrease1V3FFF">
-      <proof prover="cvc3" timelimit="10" edited="" obsolete="false">
+   <goal
+    name="WP_parameter search_rec"
+    expl="parameter search_rec"
+    sum="218de42f33228231b48bf03e7dd8c864"
+    proved="true"
+    expanded="true"
+    shape="Lamk arrayV0V2iainfix <V1V0iainfix =agetV2V1c0ainfix =agetV2V4c0NIainfix <V4V1Aainfix <=V1V4FAainfix =agetV2V1c0Aainfix <V1V0Aainfix <=V1V1Oainfix =agetV2V5c0NIainfix <V5V0Aainfix <=V1V5FAainfix =V1aprefix -c1iainfix >agetV2V1c0LagetV2V1ainfix =agetV2V8c0NIainfix <V8V7Aainfix <=V1V8FAainfix =agetV2V7c0Aainfix <V7V0Aainfix <=V1V7Oainfix =agetV2V9c0NIainfix <V9V0Aainfix <=V1V9FAainfix =V7aprefix -c1Iainfix =agetV2V10c0NIainfix <V10V7Aainfix <=ainfix +V1V6V10FAainfix =agetV2V7c0Aainfix <V7V0Aainfix <=ainfix +V1V6V7Oainfix =agetV2V11c0NIainfix <V11V0Aainfix <=ainfix +V1V6V11FAainfix =V7aprefix -c1FAainfix <=c0ainfix +V1V6Aadecrease1V3Aainfix <V1V0Aainfix <=c0V1ainfix =agetV2V13c0NIainfix <V13V12Aainfix <=V1V13FAainfix =agetV2V12c0Aainfix <V12V0Aainfix <=V1V12Oainfix =agetV2V14c0NIainfix <V14V0Aainfix <=V1V14FAainfix =V12aprefix -c1Iainfix =agetV2V15c0NIainfix <V15V12Aainfix <=ainfix +V1c1V15FAainfix =agetV2V12c0Aainfix <V12V0Aainfix <=ainfix +V1c1V12Oainfix =agetV2V16c0NIainfix <V16V0Aainfix <=ainfix +V1c1V16FAainfix =V12aprefix -c1FAainfix <=c0ainfix +V1c1Aadecrease1V3Aainfix <V1V0Aainfix <=c0V1Aainfix <V1V0Aainfix <=c0V1ainfix =agetV2V17c0NIainfix <V17aprefix -c1Aainfix <=V1V17FAainfix =agetV2aprefix -c1c0Aainfix <aprefix -c1V0Aainfix <=V1aprefix -c1Oainfix =agetV2V18c0NIainfix <V18V0Aainfix <=V1V18FAainfix =aprefix -c1aprefix -c1Iainfix <=c0V1Aadecrease1V3FFF">
+    <transf
+     name="split_goal"
+     proved="true"
+     expanded="true">
+     <goal
+      name="WP_parameter search_rec.1"
+      expl="precondition"
+      sum="d73590a15ec326b1799b3f5e0bfd8a07"
+      proved="true"
+      expanded="true"
+      shape="Lamk arrayV0V2ainfix <V1V0Aainfix <=c0V1Iainfix <V1V0Iainfix <=c0V1Aadecrease1V3FFF">
+      <proof
+       prover="cvc3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.01"/>
       </proof>
-      <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
+      <proof
+       prover="alt-ergo"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.02"/>
       </proof>
-      <proof prover="z3" timelimit="10" edited="" obsolete="false">
+      <proof
+       prover="z3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.02"/>
       </proof>
      </goal>
-     <goal name="WP_parameter search_rec.2" expl="normal postcondition" sum="cfc30e116e2d4b3eafc20cc5574fa133" proved="true" expanded="true" shape="Lamk arrayV0V2ainfix =agetV2V4c0NIainfix <V4V1Aainfix <=V1V4FAainfix =agetV2V1c0Aainfix <V1V0Aainfix <=V1V1Oainfix =agetV2V5c0NIainfix <V5V0Aainfix <=V1V5FAainfix =V1aprefix -c1Iainfix =agetV2V1c0Iainfix <V1V0Aainfix <=c0V1Iainfix <V1V0Iainfix <=c0V1Aadecrease1V3FFF">
-      <proof prover="cvc3" timelimit="10" edited="" obsolete="false">
+     <goal
+      name="WP_parameter search_rec.2"
+      expl="normal postcondition"
+      sum="cfc30e116e2d4b3eafc20cc5574fa133"
+      proved="true"
+      expanded="true"
+      shape="Lamk arrayV0V2ainfix =agetV2V4c0NIainfix <V4V1Aainfix <=V1V4FAainfix =agetV2V1c0Aainfix <V1V0Aainfix <=V1V1Oainfix =agetV2V5c0NIainfix <V5V0Aainfix <=V1V5FAainfix =V1aprefix -c1Iainfix =agetV2V1c0Iainfix <V1V0Aainfix <=c0V1Iainfix <V1V0Iainfix <=c0V1Aadecrease1V3FFF">
+      <proof
+       prover="cvc3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.02"/>
       </proof>
-      <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
+      <proof
+       prover="alt-ergo"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.01"/>
       </proof>
-      <proof prover="z3" timelimit="10" edited="" obsolete="false">
+      <proof
+       prover="z3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.03"/>
       </proof>
      </goal>
-     <goal name="WP_parameter search_rec.3" expl="precondition" sum="25a22039bc7fd9c5d248bbf31f4116cf" proved="true" expanded="true" shape="Lamk arrayV0V2ainfix <V1V0Aainfix <=c0V1Iainfix =agetV2V1c0NIainfix <V1V0Aainfix <=c0V1Iainfix <V1V0Iainfix <=c0V1Aadecrease1V3FFF">
-      <proof prover="cvc3" timelimit="10" edited="" obsolete="false">
+     <goal
+      name="WP_parameter search_rec.3"
+      expl="precondition"
+      sum="25a22039bc7fd9c5d248bbf31f4116cf"
+      proved="true"
+      expanded="true"
+      shape="Lamk arrayV0V2ainfix <V1V0Aainfix <=c0V1Iainfix =agetV2V1c0NIainfix <V1V0Aainfix <=c0V1Iainfix <V1V0Iainfix <=c0V1Aadecrease1V3FFF">
+      <proof
+       prover="cvc3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.01"/>
       </proof>
-      <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
+      <proof
+       prover="alt-ergo"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.02"/>
       </proof>
-      <proof prover="z3" timelimit="10" edited="" obsolete="false">
+      <proof
+       prover="z3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.01"/>
       </proof>
      </goal>
-     <goal name="WP_parameter search_rec.4" expl="precondition" sum="df6a7c082197b93687b09ec86cebc4fc" proved="true" expanded="true" shape="Lamk arrayV0V2ainfix <V1V0Aainfix <=c0V1Iainfix >agetV2V1c0Iainfix <V1V0Aainfix <=c0V1Iainfix =agetV2V1c0NIainfix <V1V0Aainfix <=c0V1Iainfix <V1V0Iainfix <=c0V1Aadecrease1V3FFF">
-      <proof prover="cvc3" timelimit="10" edited="" obsolete="false">
+     <goal
+      name="WP_parameter search_rec.4"
+      expl="precondition"
+      sum="df6a7c082197b93687b09ec86cebc4fc"
+      proved="true"
+      expanded="true"
+      shape="Lamk arrayV0V2ainfix <V1V0Aainfix <=c0V1Iainfix >agetV2V1c0Iainfix <V1V0Aainfix <=c0V1Iainfix =agetV2V1c0NIainfix <V1V0Aainfix <=c0V1Iainfix <V1V0Iainfix <=c0V1Aadecrease1V3FFF">
+      <proof
+       prover="cvc3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.01"/>
       </proof>
-      <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
+      <proof
+       prover="alt-ergo"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.02"/>
       </proof>
-      <proof prover="z3" timelimit="10" edited="" obsolete="false">
+      <proof
+       prover="z3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.01"/>
       </proof>
      </goal>
-     <goal name="WP_parameter search_rec.5" expl="precondition" sum="f31fa9539847d6b18ae221934087ea5e" proved="true" expanded="true" shape="Lamk arrayV0V2LagetV2V1ainfix <=c0ainfix +V1V4Aadecrease1V3Iainfix <V1V0Aainfix <=c0V1Iainfix >agetV2V1c0Iainfix <V1V0Aainfix <=c0V1Iainfix =agetV2V1c0NIainfix <V1V0Aainfix <=c0V1Iainfix <V1V0Iainfix <=c0V1Aadecrease1V3FFF">
-      <proof prover="cvc3" timelimit="10" edited="" obsolete="false">
+     <goal
+      name="WP_parameter search_rec.5"
+      expl="precondition"
+      sum="f31fa9539847d6b18ae221934087ea5e"
+      proved="true"
+      expanded="true"
+      shape="Lamk arrayV0V2LagetV2V1ainfix <=c0ainfix +V1V4Aadecrease1V3Iainfix <V1V0Aainfix <=c0V1Iainfix >agetV2V1c0Iainfix <V1V0Aainfix <=c0V1Iainfix =agetV2V1c0NIainfix <V1V0Aainfix <=c0V1Iainfix <V1V0Iainfix <=c0V1Aadecrease1V3FFF">
+      <proof
+       prover="cvc3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.02"/>
       </proof>
-      <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
+      <proof
+       prover="alt-ergo"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.03"/>
       </proof>
-      <proof prover="z3" timelimit="10" edited="" obsolete="false">
+      <proof
+       prover="z3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.03"/>
       </proof>
      </goal>
-     <goal name="WP_parameter search_rec.6" expl="normal postcondition" sum="829516cb4dd6801ad69e14bdc31565cd" proved="true" expanded="true" shape="Lamk arrayV0V2LagetV2V1ainfix =agetV2V6c0NIainfix <V6V5Aainfix <=V1V6FAainfix =agetV2V5c0Aainfix <V5V0Aainfix <=V1V5Oainfix =agetV2V7c0NIainfix <V7V0Aainfix <=V1V7FAainfix =V5aprefix -c1Iainfix =agetV2V8c0NIainfix <V8V5Aainfix <=ainfix +V1V4V8FAainfix =agetV2V5c0Aainfix <V5V0Aainfix <=ainfix +V1V4V5Oainfix =agetV2V9c0NIainfix <V9V0Aainfix <=ainfix +V1V4V9FAainfix =V5aprefix -c1FIainfix <=c0ainfix +V1V4Aadecrease1V3Iainfix <V1V0Aainfix <=c0V1Iainfix >agetV2V1c0Iainfix <V1V0Aainfix <=c0V1Iainfix =agetV2V1c0NIainfix <V1V0Aainfix <=c0V1Iainfix <V1V0Iainfix <=c0V1Aadecrease1V3FFF">
-      <proof prover="z3" timelimit="10" edited="" obsolete="false">
+     <goal
+      name="WP_parameter search_rec.6"
+      expl="normal postcondition"
+      sum="829516cb4dd6801ad69e14bdc31565cd"
+      proved="true"
+      expanded="true"
+      shape="Lamk arrayV0V2LagetV2V1ainfix =agetV2V6c0NIainfix <V6V5Aainfix <=V1V6FAainfix =agetV2V5c0Aainfix <V5V0Aainfix <=V1V5Oainfix =agetV2V7c0NIainfix <V7V0Aainfix <=V1V7FAainfix =V5aprefix -c1Iainfix =agetV2V8c0NIainfix <V8V5Aainfix <=ainfix +V1V4V8FAainfix =agetV2V5c0Aainfix <V5V0Aainfix <=ainfix +V1V4V5Oainfix =agetV2V9c0NIainfix <V9V0Aainfix <=ainfix +V1V4V9FAainfix =V5aprefix -c1FIainfix <=c0ainfix +V1V4Aadecrease1V3Iainfix <V1V0Aainfix <=c0V1Iainfix >agetV2V1c0Iainfix <V1V0Aainfix <=c0V1Iainfix =agetV2V1c0NIainfix <V1V0Aainfix <=c0V1Iainfix <V1V0Iainfix <=c0V1Aadecrease1V3FFF">
+      <proof
+       prover="z3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.04"/>
       </proof>
      </goal>
-     <goal name="WP_parameter search_rec.7" expl="precondition" sum="74e17e1b5b8562e2329750548ba8b7dc" proved="true" expanded="true" shape="Lamk arrayV0V2ainfix <=c0ainfix +V1c1Aadecrease1V3Iainfix >agetV2V1c0NIainfix <V1V0Aainfix <=c0V1Iainfix =agetV2V1c0NIainfix <V1V0Aainfix <=c0V1Iainfix <V1V0Iainfix <=c0V1Aadecrease1V3FFF">
-      <proof prover="cvc3" timelimit="10" edited="" obsolete="false">
+     <goal
+      name="WP_parameter search_rec.7"
+      expl="precondition"
+      sum="74e17e1b5b8562e2329750548ba8b7dc"
+      proved="true"
+      expanded="true"
+      shape="Lamk arrayV0V2ainfix <=c0ainfix +V1c1Aadecrease1V3Iainfix >agetV2V1c0NIainfix <V1V0Aainfix <=c0V1Iainfix =agetV2V1c0NIainfix <V1V0Aainfix <=c0V1Iainfix <V1V0Iainfix <=c0V1Aadecrease1V3FFF">
+      <proof
+       prover="cvc3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.01"/>
       </proof>
-      <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
+      <proof
+       prover="alt-ergo"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.02"/>
       </proof>
-      <proof prover="z3" timelimit="10" edited="" obsolete="false">
+      <proof
+       prover="z3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.03"/>
       </proof>
      </goal>
-     <goal name="WP_parameter search_rec.8" expl="normal postcondition" sum="0753a63864a318601818633033c5c922" proved="true" expanded="true" shape="Lamk arrayV0V2ainfix =agetV2V5c0NIainfix <V5V4Aainfix <=V1V5FAainfix =agetV2V4c0Aainfix <V4V0Aainfix <=V1V4Oainfix =agetV2V6c0NIainfix <V6V0Aainfix <=V1V6FAainfix =V4aprefix -c1Iainfix =agetV2V7c0NIainfix <V7V4Aainfix <=ainfix +V1c1V7FAainfix =agetV2V4c0Aainfix <V4V0Aainfix <=ainfix +V1c1V4Oainfix =agetV2V8c0NIainfix <V8V0Aainfix <=ainfix +V1c1V8FAainfix =V4aprefix -c1FIainfix <=c0ainfix +V1c1Aadecrease1V3Iainfix >agetV2V1c0NIainfix <V1V0Aainfix <=c0V1Iainfix =agetV2V1c0NIainfix <V1V0Aainfix <=c0V1Iainfix <V1V0Iainfix <=c0V1Aadecrease1V3FFF">
-      <proof prover="cvc3" timelimit="10" edited="" obsolete="false">
+     <goal
+      name="WP_parameter search_rec.8"
+      expl="normal postcondition"
+      sum="0753a63864a318601818633033c5c922"
+      proved="true"
+      expanded="true"
+      shape="Lamk arrayV0V2ainfix =agetV2V5c0NIainfix <V5V4Aainfix <=V1V5FAainfix =agetV2V4c0Aainfix <V4V0Aainfix <=V1V4Oainfix =agetV2V6c0NIainfix <V6V0Aainfix <=V1V6FAainfix =V4aprefix -c1Iainfix =agetV2V7c0NIainfix <V7V4Aainfix <=ainfix +V1c1V7FAainfix =agetV2V4c0Aainfix <V4V0Aainfix <=ainfix +V1c1V4Oainfix =agetV2V8c0NIainfix <V8V0Aainfix <=ainfix +V1c1V8FAainfix =V4aprefix -c1FIainfix <=c0ainfix +V1c1Aadecrease1V3Iainfix >agetV2V1c0NIainfix <V1V0Aainfix <=c0V1Iainfix =agetV2V1c0NIainfix <V1V0Aainfix <=c0V1Iainfix <V1V0Iainfix <=c0V1Aadecrease1V3FFF">
+      <proof
+       prover="cvc3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.02"/>
       </proof>
-      <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
+      <proof
+       prover="alt-ergo"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.02"/>
       </proof>
-      <proof prover="z3" timelimit="10" edited="" obsolete="false">
+      <proof
+       prover="z3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.03"/>
       </proof>
      </goal>
-     <goal name="WP_parameter search_rec.9" expl="normal postcondition" sum="d0f3f258ada86e676fe42c6f6d4cba7c" proved="true" expanded="true" shape="Lamk arrayV0V2ainfix =agetV2V4c0NIainfix <V4aprefix -c1Aainfix <=V1V4FAainfix =agetV2aprefix -c1c0Aainfix <aprefix -c1V0Aainfix <=V1aprefix -c1Oainfix =agetV2V5c0NIainfix <V5V0Aainfix <=V1V5FAainfix =aprefix -c1aprefix -c1Iainfix <V1V0NIainfix <=c0V1Aadecrease1V3FFF">
-      <proof prover="cvc3" timelimit="10" edited="" obsolete="false">
+     <goal
+      name="WP_parameter search_rec.9"
+      expl="normal postcondition"
+      sum="d0f3f258ada86e676fe42c6f6d4cba7c"
+      proved="true"
+      expanded="true"
+      shape="Lamk arrayV0V2ainfix =agetV2V4c0NIainfix <V4aprefix -c1Aainfix <=V1V4FAainfix =agetV2aprefix -c1c0Aainfix <aprefix -c1V0Aainfix <=V1aprefix -c1Oainfix =agetV2V5c0NIainfix <V5V0Aainfix <=V1V5FAainfix =aprefix -c1aprefix -c1Iainfix <V1V0NIainfix <=c0V1Aadecrease1V3FFF">
+      <proof
+       prover="cvc3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.02"/>
       </proof>
-      <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
+      <proof
+       prover="alt-ergo"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.00"/>
       </proof>
-      <proof prover="z3" timelimit="10" edited="" obsolete="false">
+      <proof
+       prover="z3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.03"/>
       </proof>
      </goal>