diff --git a/examples/bts/12475/why3session.xml b/examples/bts/12475/why3session.xml
index 6fe1a6632b5f4a09e28aa19af163aaeea8fdb63d..84d57ccc28eadd1f8756d87d8bd7d92c934de03f 100644
--- a/examples/bts/12475/why3session.xml
+++ b/examples/bts/12475/why3session.xml
@@ -2,14 +2,14 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
-<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
+<prover id="1" name="Alt-Ergo" version="2.2.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="2" name="CVC3" version="2.4.1" timelimit="2" steplimit="0" memlimit="0"/>
 <prover id="3" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="4" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
 <file name="../12475.why" proved="true">
 <theory name="Stmt" proved="true">
  <goal name="toto" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="3"/></proof>
+ <proof prover="1"><result status="valid" time="0.01" steps="6"/></proof>
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="3"><result status="valid" time="0.01"/></proof>
  <proof prover="4"><result status="valid" time="0.00"/></proof>
diff --git a/examples/bts/13375/why3session.xml b/examples/bts/13375/why3session.xml
index 7e3c21067ea4850b9232b4b95c076488d9c66570..b1c874d6afd8bbaab6e42de6df59cf4de62a5501 100644
--- a/examples/bts/13375/why3session.xml
+++ b/examples/bts/13375/why3session.xml
@@ -2,11 +2,11 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
-<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
+<prover id="0" name="Alt-Ergo" version="2.2.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <file name="../13375.mlw" proved="true">
 <theory name="Spec" proved="true">
  <goal name="VC to_int_" expl="VC for to_int_" proved="true">
- <proof prover="1"><result status="valid" time="0.00" steps="2"/></proof>
+ <proof prover="0"><result status="valid" time="0.00" steps="4"/></proof>
  </goal>
 </theory>
 </file>
diff --git a/examples/bts/13853/why3session.xml b/examples/bts/13853/why3session.xml
index d9c7f228106057569b610934b0aae54099c09e95..2e296ed16482eb473cd65547dbafd08be9f02ea4 100644
--- a/examples/bts/13853/why3session.xml
+++ b/examples/bts/13853/why3session.xml
@@ -2,14 +2,14 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
-<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
+<prover id="0" name="Alt-Ergo" version="2.2.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <file name="../13853.mlw" proved="true">
 <theory name="T" proved="true">
  <goal name="VC f" expl="VC for f" proved="true">
- <proof prover="1"><result status="valid" time="0.00" steps="0"/></proof>
+ <proof prover="0"><result status="valid" time="0.00" steps="0"/></proof>
  </goal>
  <goal name="VC g" expl="VC for g" proved="true">
- <proof prover="1"><result status="valid" time="0.00" steps="0"/></proof>
+ <proof prover="0"><result status="valid" time="0.00" steps="0"/></proof>
  </goal>
 </theory>
 </file>
diff --git a/examples/bts/16972/why3session.xml b/examples/bts/16972/why3session.xml
index f7e03484bacc7980e8d0a4200f003582534baa07..fa693cbfcbaa8abcea80d0e4517e1ca54d6866cc 100644
--- a/examples/bts/16972/why3session.xml
+++ b/examples/bts/16972/why3session.xml
@@ -2,11 +2,11 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
-<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
+<prover id="1" name="Alt-Ergo" version="2.2.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <file name="../16972.mlw" proved="true">
 <theory name="M" proved="true">
  <goal name="VC fail" expl="VC for fail" proved="true">
- <proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
+ <proof prover="1"><result status="valid" time="0.00" steps="4"/></proof>
  </goal>
 </theory>
 </file>
diff --git a/examples/bts/20445/why3session.xml b/examples/bts/20445/why3session.xml
index 640e7231f8f51fbca5f8a74213aa57a4d0df4cab..3f2beef82ba4beab14bbe05c2744339e3f805958 100644
--- a/examples/bts/20445/why3session.xml
+++ b/examples/bts/20445/why3session.xml
@@ -2,14 +2,14 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
-<prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
+<prover id="1" name="Alt-Ergo" version="2.2.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <file name="../20445.mlw">
 <theory name="B">
  <goal name="G">
- <proof prover="0" timelimit="1"><result status="unknown" time="0.00"/></proof>
+ <proof prover="1" timelimit="1"><result status="unknown" time="0.00"/></proof>
  </goal>
  <goal name="A.G" proved="true">
- <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
+ <proof prover="1"><result status="valid" time="0.00" steps="0"/></proof>
  </goal>
 </theory>
 </file>
diff --git a/examples/bts/fsetint/why3session.xml b/examples/bts/fsetint/why3session.xml
index 0c874708e02e1fee1dca0b2a57e6eaf17475065b..d78c4b4edc3ccde99d8a3e6ca0a91971f09b0123 100644
--- a/examples/bts/fsetint/why3session.xml
+++ b/examples/bts/fsetint/why3session.xml
@@ -3,18 +3,16 @@
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
 <prover id="0" name="CVC3" version="2.4.1" timelimit="1" steplimit="0" memlimit="1000"/>
-<prover id="1" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
+<prover id="2" name="Alt-Ergo" version="2.2.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="4" name="Z3" version="3.2" timelimit="1" steplimit="0" memlimit="1000"/>
-<prover id="5" name="Alt-Ergo" version="0.99.1" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="6" name="CVC4" version="1.4" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="7" name="Z3" version="4.3.2" timelimit="1" steplimit="0" memlimit="1000"/>
 <file name="../fsetint.why">
 <theory name="Th1">
  <goal name="l_false">
  <proof prover="0"><result status="timeout" time="1.00"/></proof>
- <proof prover="1"><result status="unknown" time="0.01"/></proof>
+ <proof prover="2"><result status="unknown" time="0.01"/></proof>
  <proof prover="4"><result status="timeout" time="1.00"/></proof>
- <proof prover="5"><result status="unknown" time="0.01"/></proof>
  <proof prover="6"><result status="unknown" time="0.01"/></proof>
  <proof prover="7"><result status="timeout" time="1.00"/></proof>
  </goal>
@@ -22,17 +20,15 @@
 <theory name="Th2">
  <goal name="mem_integer">
  <proof prover="0"><result status="timeout" time="1.00"/></proof>
- <proof prover="1"><result status="unknown" time="0.01"/></proof>
+ <proof prover="2"><result status="unknown" time="0.00"/></proof>
  <proof prover="4"><result status="timeout" time="1.00"/></proof>
- <proof prover="5"><result status="unknown" time="0.00"/></proof>
  <proof prover="6"><result status="timeout" time="1.00"/></proof>
  <proof prover="7"><result status="timeout" time="1.00"/></proof>
  </goal>
  <goal name="foo">
  <proof prover="0"><result status="timeout" time="1.00"/></proof>
- <proof prover="1"><result status="unknown" time="0.01"/></proof>
+ <proof prover="2"><result status="unknown" time="0.00"/></proof>
  <proof prover="4"><result status="timeout" time="1.00"/></proof>
- <proof prover="5"><result status="unknown" time="0.00"/></proof>
  <proof prover="6"><result status="unknown" time="0.02"/></proof>
  <proof prover="7"><result status="timeout" time="1.00"/></proof>
  </goal>
@@ -40,9 +36,8 @@
 <theory name="Th3">
  <goal name="foo">
  <proof prover="0"><result status="unknown" time="0.00"/></proof>
- <proof prover="1"><result status="unknown" time="0.01"/></proof>
+ <proof prover="2"><result status="unknown" time="0.00"/></proof>
  <proof prover="4"><result status="timeout" time="1.00"/></proof>
- <proof prover="5"><result status="unknown" time="0.00"/></proof>
  <proof prover="6"><result status="unknown" time="0.00"/></proof>
  <proof prover="7"><result status="timeout" time="1.00"/></proof>
  </goal>
diff --git a/examples/check-builtin/ac/why3session.xml b/examples/check-builtin/ac/why3session.xml
index e5b2275169d5e98ad92e4bcf19e5aedcca46e7f1..3eaa5edccda93f6ff0c3b76402ddcfcb9908b5c3 100644
--- a/examples/check-builtin/ac/why3session.xml
+++ b/examples/check-builtin/ac/why3session.xml
@@ -3,21 +3,21 @@
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
 <prover id="0" name="CVC3" version="2.4.1" timelimit="10" steplimit="0" memlimit="0"/>
+<prover id="1" name="Alt-Ergo" version="2.2.0" timelimit="10" steplimit="0" memlimit="0"/>
 <prover id="3" name="Spass" version="3.7" timelimit="10" steplimit="0" memlimit="0"/>
-<prover id="4" name="Alt-Ergo" version="0.99.1" timelimit="10" steplimit="0" memlimit="0"/>
 <prover id="5" name="Z3" version="4.3.2" timelimit="10" steplimit="0" memlimit="0"/>
 <file name="../ac.why" proved="true">
 <theory name="Test" proved="true">
  <goal name="G1" proved="true">
  <proof prover="0"><result status="valid" time="0.00"/></proof>
+ <proof prover="1"><result status="valid" time="0.00" steps="0"/></proof>
  <proof prover="3"><result status="valid" time="0.01"/></proof>
- <proof prover="4"><result status="valid" time="0.00" steps="0"/></proof>
  <proof prover="5"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="G2" proved="true">
  <proof prover="0"><result status="valid" time="0.00"/></proof>
+ <proof prover="1"><result status="valid" time="0.00" steps="0"/></proof>
  <proof prover="3"><result status="valid" time="0.01"/></proof>
- <proof prover="4"><result status="valid" time="0.00" steps="0"/></proof>
  <proof prover="5"><result status="valid" time="0.00"/></proof>
  </goal>
 </theory>
diff --git a/examples/check-builtin/array/why3session.xml b/examples/check-builtin/array/why3session.xml
index c3b3489e6cd90f61c2ac98d3cfef4adb79eeed79..aeab6df6a167e37aad371e3c8ed0b73182cd8ba0 100644
--- a/examples/check-builtin/array/why3session.xml
+++ b/examples/check-builtin/array/why3session.xml
@@ -3,38 +3,38 @@
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
 <prover id="0" name="CVC3" version="2.4.1" timelimit="3" steplimit="0" memlimit="0"/>
+<prover id="1" name="Alt-Ergo" version="2.2.0" timelimit="10" steplimit="0" memlimit="0"/>
 <prover id="3" name="Spass" version="3.7" timelimit="10" steplimit="0" memlimit="0"/>
 <prover id="5" name="Z3" version="3.2" timelimit="3" steplimit="0" memlimit="0"/>
-<prover id="6" name="Alt-Ergo" version="0.99.1" timelimit="10" steplimit="0" memlimit="0"/>
 <prover id="7" name="Z3" version="4.3.2" timelimit="10" steplimit="0" memlimit="0"/>
 <file name="../array.why" proved="true">
 <theory name="Test_simplify_array" proved="true">
  <goal name="G1" proved="true">
  <proof prover="0"><result status="valid" time="0.00"/></proof>
+ <proof prover="1"><result status="valid" time="0.01" steps="0"/></proof>
  <proof prover="3"><result status="valid" time="0.02"/></proof>
  <proof prover="5"><result status="valid" time="0.00"/></proof>
- <proof prover="6"><result status="valid" time="0.01" steps="0"/></proof>
  <proof prover="7"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="G2" proved="true">
  <proof prover="0"><result status="valid" time="0.00"/></proof>
+ <proof prover="1"><result status="valid" time="0.01" steps="4"/></proof>
  <proof prover="3"><result status="valid" time="0.01"/></proof>
  <proof prover="5"><result status="valid" time="0.02"/></proof>
- <proof prover="6"><result status="valid" time="0.01" steps="2"/></proof>
  <proof prover="7"><result status="valid" time="0.01"/></proof>
  </goal>
  <goal name="G3" proved="true">
  <proof prover="0"><result status="valid" time="0.00"/></proof>
+ <proof prover="1"><result status="valid" time="0.00" steps="2"/></proof>
  <proof prover="3"><result status="valid" time="0.02"/></proof>
  <proof prover="5"><result status="valid" time="0.00"/></proof>
- <proof prover="6"><result status="valid" time="0.00" steps="1"/></proof>
  <proof prover="7"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="G4" proved="true">
  <proof prover="0"><result status="valid" time="0.00"/></proof>
+ <proof prover="1"><result status="valid" time="0.01" steps="0"/></proof>
  <proof prover="3"><result status="valid" time="0.02"/></proof>
  <proof prover="5"><result status="valid" time="0.00"/></proof>
- <proof prover="6"><result status="valid" time="0.01" steps="0"/></proof>
  <proof prover="7"><result status="valid" time="0.00"/></proof>
  </goal>
 </theory>
diff --git a/examples/check-builtin/bool/why3session.xml b/examples/check-builtin/bool/why3session.xml
index e8d4de7afa7b1db17afc804aaf5635818b3df012..796ae9abf1d0f2cef811fac372be670d36a06309 100644
--- a/examples/check-builtin/bool/why3session.xml
+++ b/examples/check-builtin/bool/why3session.xml
@@ -3,27 +3,27 @@
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
 <prover id="0" name="CVC3" version="2.4.1" timelimit="10" steplimit="0" memlimit="0"/>
+<prover id="1" name="Alt-Ergo" version="2.2.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="3" name="Spass" version="3.7" timelimit="10" steplimit="0" memlimit="0"/>
-<prover id="4" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="5" name="Z3" version="4.3.2" timelimit="10" steplimit="0" memlimit="0"/>
 <file name="../bool.why" proved="true">
 <theory name="Test" proved="true">
  <goal name="G1" proved="true">
  <proof prover="0"><result status="valid" time="0.00"/></proof>
+ <proof prover="1"><result status="valid" time="0.00" steps="0"/></proof>
  <proof prover="3"><result status="valid" time="0.01"/></proof>
- <proof prover="4"><result status="valid" time="0.00" steps="0"/></proof>
  <proof prover="5"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="G2" proved="true">
  <proof prover="0"><result status="valid" time="0.00"/></proof>
+ <proof prover="1"><result status="valid" time="0.01" steps="0"/></proof>
  <proof prover="3"><result status="valid" time="0.01"/></proof>
- <proof prover="4"><result status="valid" time="0.01" steps="0"/></proof>
  <proof prover="5"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="G3" proved="true">
  <proof prover="0"><result status="valid" time="0.00"/></proof>
+ <proof prover="1"><result status="valid" time="0.01" steps="0"/></proof>
  <proof prover="3"><result status="valid" time="0.01"/></proof>
- <proof prover="4"><result status="valid" time="0.01" steps="6"/></proof>
  <proof prover="5"><result status="valid" time="0.01"/></proof>
  </goal>
 </theory>
diff --git a/examples/check-builtin/euclideandivision/why3session.xml b/examples/check-builtin/euclideandivision/why3session.xml
index 23b5e3848bc8dc867d151bae36e2355a418f37fb..1ddd9bd9c25a5605b6cae25407bbeefe433a6968 100644
--- a/examples/check-builtin/euclideandivision/why3session.xml
+++ b/examples/check-builtin/euclideandivision/why3session.xml
@@ -3,26 +3,26 @@
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
 <prover id="0" name="Z3" version="4.4.0" timelimit="5" steplimit="0" memlimit="4000"/>
+<prover id="1" name="Alt-Ergo" version="2.2.0" timelimit="3" steplimit="0" memlimit="1000"/>
 <prover id="3" name="CVC3" version="2.4.1" timelimit="10" steplimit="0" memlimit="0"/>
 <prover id="6" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/>
-<prover id="7" name="Alt-Ergo" version="0.99.1" timelimit="3" steplimit="0" memlimit="1000"/>
 <prover id="8" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="9" name="Z3" version="4.3.2" timelimit="10" steplimit="0" memlimit="0"/>
 <file name="../euclideandivision.why" proved="true">
 <theory name="Test" proved="true">
  <goal name="G1" proved="true">
  <proof prover="0"><result status="valid" time="0.00"/></proof>
+ <proof prover="1"><result status="valid" time="0.01" steps="0"/></proof>
  <proof prover="3"><result status="valid" time="0.00"/></proof>
  <proof prover="6"><result status="valid" time="0.00"/></proof>
- <proof prover="7"><result status="valid" time="0.01" steps="0"/></proof>
  <proof prover="8"><result status="valid" time="0.00"/></proof>
  <proof prover="9"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="G2" proved="true">
  <proof prover="0"><result status="valid" time="0.01"/></proof>
+ <proof prover="1"><result status="valid" time="0.00" steps="0"/></proof>
  <proof prover="3"><result status="valid" time="0.00"/></proof>
  <proof prover="6"><result status="valid" time="0.00"/></proof>
- <proof prover="7"><result status="valid" time="0.00" steps="0"/></proof>
  <proof prover="8"><result status="valid" time="0.00"/></proof>
  <proof prover="9"><result status="valid" time="0.00"/></proof>
  </goal>
diff --git a/examples/check-builtin/floats/why3session.xml b/examples/check-builtin/floats/why3session.xml
index 44c7c6df00c8240aa6346e85b63273ee054e8ee2..ee4b88b8143ab0df426498b47f70128189896cdf 100644
--- a/examples/check-builtin/floats/why3session.xml
+++ b/examples/check-builtin/floats/why3session.xml
@@ -4,7 +4,7 @@
 <why3session shape_version="4">
 <prover id="0" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="0"/>
 <prover id="1" name="Gappa" version="1.3.0" timelimit="5" steplimit="0" memlimit="0"/>
-<prover id="4" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="0"/>
+<prover id="2" name="Alt-Ergo" version="2.2.0" timelimit="5" steplimit="0" memlimit="0"/>
 <prover id="5" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="0"/>
 <file name="../floats.why" proved="true">
 <theory name="TestGappa" proved="true">
@@ -17,7 +17,7 @@
  <goal name="Test00" proved="true">
  <proof prover="0"><result status="valid" time="0.02"/></proof>
  <proof prover="1"><result status="valid" time="0.00"/></proof>
- <proof prover="4"><result status="valid" time="0.01" steps="6"/></proof>
+ <proof prover="2"><result status="valid" time="0.01" steps="8"/></proof>
  <proof prover="5"><result status="valid" time="0.02"/></proof>
  </goal>
  <goal name="Test01" proved="true">
diff --git a/examples/check-builtin/int/why3session.xml b/examples/check-builtin/int/why3session.xml
index 7b00518ebbe7bb3072feb4baeaa13fc21106cd73..a336e782d78bb9c246f1fd1cbb315c05a19f8368 100644
--- a/examples/check-builtin/int/why3session.xml
+++ b/examples/check-builtin/int/why3session.xml
@@ -2,113 +2,113 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
+<prover id="0" name="Alt-Ergo" version="2.2.0" timelimit="10" steplimit="0" memlimit="0"/>
 <prover id="1" name="CVC3" version="2.4.1" timelimit="3" steplimit="0" memlimit="0"/>
 <prover id="4" name="Spass" version="3.7" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="5" name="Z3" version="3.2" timelimit="3" steplimit="0" memlimit="0"/>
 <prover id="6" name="Vampire" version="0.6" timelimit="1" steplimit="0" memlimit="1000"/>
-<prover id="7" name="Alt-Ergo" version="0.99.1" timelimit="10" steplimit="0" memlimit="0"/>
 <prover id="8" name="Eprover" version="1.8-001" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="9" name="Z3" version="4.3.2" timelimit="10" steplimit="0" memlimit="0"/>
 <file name="../int.why" proved="true">
 <theory name="Test" proved="true">
  <goal name="G1" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="0"/></proof>
  <proof prover="1"><result status="valid" time="0.00"/></proof>
  <proof prover="4"><result status="timeout" time="1.00"/></proof>
  <proof prover="5"><result status="valid" time="0.00"/></proof>
  <proof prover="6"><result status="timeout" time="1.00"/></proof>
- <proof prover="7"><result status="valid" time="0.00" steps="0"/></proof>
  <proof prover="8"><result status="timeout" time="1.00"/></proof>
  <proof prover="9"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="G2" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="0"/></proof>
  <proof prover="1"><result status="valid" time="0.00"/></proof>
  <proof prover="4"><result status="timeout" time="1.00"/></proof>
  <proof prover="5"><result status="valid" time="0.00"/></proof>
  <proof prover="6"><result status="timeout" time="1.00"/></proof>
- <proof prover="7"><result status="valid" time="0.00" steps="0"/></proof>
  <proof prover="8"><result status="timeout" time="1.00"/></proof>
  <proof prover="9"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="CompatOrderAdd" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
  <proof prover="1"><result status="valid" time="0.00"/></proof>
  <proof prover="4"><result status="valid" time="0.01"/></proof>
  <proof prover="5"><result status="valid" time="0.00"/></proof>
  <proof prover="6"><result status="valid" time="0.00"/></proof>
- <proof prover="7"><result status="valid" time="0.00" steps="1"/></proof>
  <proof prover="8"><result status="valid" time="0.00"/></proof>
  <proof prover="9"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="CompatOrderMult" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="6"/></proof>
  <proof prover="1"><result status="valid" time="0.00"/></proof>
  <proof prover="4"><result status="valid" time="0.01"/></proof>
  <proof prover="5"><result status="valid" time="0.00"/></proof>
  <proof prover="6"><result status="valid" time="0.00"/></proof>
- <proof prover="7"><result status="valid" time="0.00" steps="3"/></proof>
  <proof prover="8"><result status="valid" time="0.00"/></proof>
  <proof prover="9"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="InvMult" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="0"/></proof>
  <proof prover="1"><result status="valid" time="0.00"/></proof>
  <proof prover="4"><result status="valid" time="0.86"/></proof>
  <proof prover="5"><result status="valid" time="0.00"/></proof>
  <proof prover="6"><result status="valid" time="0.03"/></proof>
- <proof prover="7"><result status="valid" time="0.00" steps="0"/></proof>
  <proof prover="8"><result status="valid" time="0.01"/></proof>
  <proof prover="9"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="InvSquare" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="0"/></proof>
  <proof prover="1"><result status="valid" time="0.00"/></proof>
  <proof prover="4"><result status="valid" time="0.78"/></proof>
  <proof prover="5"><result status="valid" time="0.00"/></proof>
  <proof prover="6"><result status="valid" time="0.04"/></proof>
- <proof prover="7"><result status="valid" time="0.00" steps="0"/></proof>
  <proof prover="8"><result status="valid" time="0.00"/></proof>
  <proof prover="9"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="ZeroMult" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="0"/></proof>
  <proof prover="1"><result status="valid" time="0.00"/></proof>
  <proof prover="4"><result status="valid" time="0.05"/></proof>
  <proof prover="5"><result status="valid" time="0.00"/></proof>
  <proof prover="6"><result status="valid" time="0.02"/></proof>
- <proof prover="7"><result status="valid" time="0.00" steps="0"/></proof>
  <proof prover="8"><result status="valid" time="0.00"/></proof>
  <proof prover="9"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="SquareNonNeg1" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
  <proof prover="1"><result status="valid" time="0.00"/></proof>
  <proof prover="4"><result status="timeout" time="1.00"/></proof>
  <proof prover="5"><result status="valid" time="0.00"/></proof>
  <proof prover="6"><result status="timeout" time="1.00"/></proof>
- <proof prover="7"><result status="valid" time="0.00" steps="1"/></proof>
  <proof prover="8"><result status="valid" time="0.58"/></proof>
  <proof prover="9"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="SquareNonNeg" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="0"/></proof>
  <proof prover="1"><result status="valid" time="0.00"/></proof>
  <proof prover="4"><result status="timeout" time="1.00"/></proof>
  <proof prover="5"><result status="valid" time="0.00"/></proof>
  <proof prover="6"><result status="timeout" time="1.00"/></proof>
- <proof prover="7"><result status="valid" time="0.00" steps="0"/></proof>
  <proof prover="8"><result status="valid" time="0.09"/></proof>
  <proof prover="9"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="ZeroLessOne" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="0"/></proof>
  <proof prover="1"><result status="valid" time="0.00"/></proof>
  <proof prover="4"><result status="valid" time="0.00"/></proof>
  <proof prover="5"><result status="valid" time="0.00"/></proof>
  <proof prover="6"><result status="valid" time="0.00"/></proof>
- <proof prover="7"><result status="valid" time="0.00" steps="0"/></proof>
  <proof prover="8"><result status="valid" time="0.00"/></proof>
  <proof prover="9"><result status="valid" time="0.00"/></proof>
  </goal>
 </theory>
 <theory name="MinMax" proved="true">
  <goal name="G" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
  <proof prover="1"><result status="valid" time="0.00"/></proof>
  <proof prover="4"><result status="timeout" time="1.00"/></proof>
  <proof prover="5"><result status="valid" time="0.01"/></proof>
  <proof prover="6"><result status="timeout" time="1.00"/></proof>
- <proof prover="7"><result status="valid" time="0.00" steps="5"/></proof>
  <proof prover="8"><result status="timeout" time="1.00"/></proof>
  <proof prover="9"><result status="valid" time="0.01"/></proof>
  </goal>
diff --git a/examples/check-builtin/minmax/why3session.xml b/examples/check-builtin/minmax/why3session.xml
index fc700d2ff73b7b2aa23b3ad5d322fc574148da12..131a24da16a58c986a67d144c089f66ffc6009b1 100644
--- a/examples/check-builtin/minmax/why3session.xml
+++ b/examples/check-builtin/minmax/why3session.xml
@@ -3,21 +3,21 @@
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
 <prover id="0" name="CVC3" version="2.4.1" timelimit="10" steplimit="0" memlimit="0"/>
+<prover id="1" name="Alt-Ergo" version="2.2.0" timelimit="10" steplimit="0" memlimit="0"/>
 <prover id="3" name="Spass" version="3.7" timelimit="10" steplimit="0" memlimit="0"/>
-<prover id="4" name="Alt-Ergo" version="0.99.1" timelimit="10" steplimit="0" memlimit="0"/>
 <prover id="5" name="Z3" version="4.3.2" timelimit="10" steplimit="0" memlimit="0"/>
 <file name="../minmax.why" proved="true">
 <theory name="MinMax" proved="true">
  <goal name="G" proved="true">
  <proof prover="0"><result status="valid" time="0.00"/></proof>
+ <proof prover="1"><result status="valid" time="0.00" steps="8"/></proof>
  <proof prover="3"><result status="valid" time="0.01"/></proof>
- <proof prover="4"><result status="valid" time="0.00" steps="10"/></proof>
  <proof prover="5"><result status="valid" time="0.01"/></proof>
  </goal>
  <goal name="G2" proved="true">
  <proof prover="0"><result status="valid" time="0.00"/></proof>
+ <proof prover="1"><result status="valid" time="0.00" steps="4"/></proof>
  <proof prover="3"><result status="valid" time="0.00"/></proof>
- <proof prover="4"><result status="valid" time="0.00" steps="10"/></proof>
  <proof prover="5"><result status="valid" time="0.01"/></proof>
  </goal>
 </theory>
diff --git a/examples/check-builtin/propositional/why3session.xml b/examples/check-builtin/propositional/why3session.xml
index 61493eff901a479c609fd64e5c0ced8995da0e3d..6c18a907850c05a6574d581038072a78fff0d9c7 100644
--- a/examples/check-builtin/propositional/why3session.xml
+++ b/examples/check-builtin/propositional/why3session.xml
@@ -4,15 +4,15 @@
 <why3session shape_version="4">
 <prover id="0" name="CVC3" version="2.4.1" timelimit="10" steplimit="0" memlimit="0"/>
 <prover id="1" name="Z3" version="3.2" timelimit="10" steplimit="0" memlimit="0"/>
+<prover id="2" name="Alt-Ergo" version="2.2.0" timelimit="10" steplimit="0" memlimit="0"/>
 <prover id="3" name="Spass" version="3.7" timelimit="10" steplimit="0" memlimit="0"/>
-<prover id="4" name="Alt-Ergo" version="0.99.1" timelimit="10" steplimit="0" memlimit="0"/>
 <file name="../propositional.why" proved="true">
 <theory name="Prop" proved="true">
  <goal name="G" proved="true">
  <proof prover="0"><result status="valid" time="0.00"/></proof>
  <proof prover="1"><result status="valid" time="0.00"/></proof>
+ <proof prover="2"><result status="valid" time="0.00" steps="4"/></proof>
  <proof prover="3"><result status="valid" time="0.00"/></proof>
- <proof prover="4"><result status="valid" time="0.00" steps="2"/></proof>
  </goal>
 </theory>
 </file>
diff --git a/examples/check-builtin/real/why3session.xml b/examples/check-builtin/real/why3session.xml
index af9f61e7ea3a18ea5506bfd6ba4895458c757df1..e327df9bf99756aa4909241269b8785d55ca5a81 100644
--- a/examples/check-builtin/real/why3session.xml
+++ b/examples/check-builtin/real/why3session.xml
@@ -3,135 +3,135 @@
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
 <prover id="0" name="Coq" version="8.7.1" timelimit="5" steplimit="0" memlimit="1000"/>
+<prover id="1" name="Alt-Ergo" version="2.2.0" timelimit="3" steplimit="0" memlimit="0"/>
 <prover id="2" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="0"/>
 <prover id="7" name="Yices" version="1.0.38" timelimit="10" steplimit="0" memlimit="0"/>
 <prover id="8" name="Z3" version="3.2" timelimit="3" steplimit="0" memlimit="0"/>
 <prover id="9" name="Gappa" version="1.3.0" timelimit="5" steplimit="0" memlimit="0"/>
-<prover id="12" name="Alt-Ergo" version="0.99.1" timelimit="3" steplimit="0" memlimit="0"/>
 <prover id="14" name="Z3" version="4.3.2" timelimit="3" steplimit="0" memlimit="0"/>
 <file name="../real.why" proved="true">
 <theory name="Test" proved="true">
  <goal name="G1" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="0"/></proof>
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="7"><result status="valid" time="0.01"/></proof>
  <proof prover="8"><result status="valid" time="0.00"/></proof>
  <proof prover="9"><result status="valid" time="0.00"/></proof>
- <proof prover="12"><result status="valid" time="0.01" steps="0"/></proof>
  <proof prover="14"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="G2" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="0"/></proof>
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="8"><result status="valid" time="0.00"/></proof>
  <proof prover="9"><result status="valid" time="0.00"/></proof>
- <proof prover="12"><result status="valid" time="0.01" steps="0"/></proof>
  <proof prover="14"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="G3" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="0"/></proof>
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="8"><result status="valid" time="0.00"/></proof>
- <proof prover="12"><result status="valid" time="0.00" steps="0"/></proof>
  <proof prover="14"><result status="valid" time="0.00"/></proof>
  </goal>
 </theory>
 <theory name="TestInfix" proved="true">
  <goal name="Add" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="0"/></proof>
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="8"><result status="valid" time="0.00"/></proof>
  <proof prover="9"><result status="valid" time="0.00"/></proof>
- <proof prover="12"><result status="valid" time="0.00" steps="0"/></proof>
  <proof prover="14"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="Sub" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="0"/></proof>
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="8"><result status="valid" time="0.00"/></proof>
  <proof prover="9"><result status="valid" time="0.00"/></proof>
- <proof prover="12"><result status="valid" time="0.00" steps="0"/></proof>
  <proof prover="14"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="Neg" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="0"/></proof>
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="8"><result status="valid" time="0.00"/></proof>
  <proof prover="9"><result status="valid" time="0.00"/></proof>
- <proof prover="12"><result status="valid" time="0.01" steps="0"/></proof>
  <proof prover="14"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="Mul" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="0"/></proof>
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="8"><result status="valid" time="0.00"/></proof>
  <proof prover="9"><result status="valid" time="0.00"/></proof>
- <proof prover="12"><result status="valid" time="0.01" steps="0"/></proof>
  <proof prover="14"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="Div" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="0"/></proof>
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="8"><result status="valid" time="0.00"/></proof>
  <proof prover="9"><result status="valid" time="0.00"/></proof>
- <proof prover="12"><result status="valid" time="0.00" steps="0"/></proof>
  <proof prover="14"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="Inv" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="0"/></proof>
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="8"><result status="valid" time="0.00"/></proof>
- <proof prover="12"><result status="valid" time="0.01" steps="0"/></proof>
  <proof prover="14"><result status="valid" time="0.00"/></proof>
  </goal>
 </theory>
 <theory name="SquareTest" proved="true">
  <goal name="Sqrt_zero" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="7"/></proof>
  <proof prover="2"><result status="valid" time="0.01"/></proof>
  <proof prover="8" timelimit="60" memlimit="1000"><result status="valid" time="0.02"/></proof>
  <proof prover="9"><result status="valid" time="0.00"/></proof>
- <proof prover="12"><result status="valid" time="0.01" steps="3"/></proof>
  <proof prover="14" timelimit="60" memlimit="1000"><result status="valid" time="0.02"/></proof>
  </goal>
  <goal name="Sqrt_one" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="8"><result status="valid" time="0.01"/></proof>
  <proof prover="9"><result status="valid" time="0.00"/></proof>
- <proof prover="12"><result status="valid" time="0.01" steps="6"/></proof>
  <proof prover="14"><result status="valid" time="0.01"/></proof>
  </goal>
  <goal name="Sqrt_four" proved="true">
+ <proof prover="1" timelimit="5" memlimit="1000"><result status="valid" time="0.00" steps="27"/></proof>
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="8" timelimit="67" memlimit="1000"><result status="valid" time="22.59"/></proof>
  <proof prover="9"><result status="valid" time="0.00"/></proof>
- <proof prover="12" timelimit="5" memlimit="1000"><result status="valid" time="0.00" steps="8"/></proof>
  </goal>
 </theory>
 <theory name="ExpLogTest" proved="true">
  <goal name="Log_e" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="6"/></proof>
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="8"><result status="valid" time="0.01"/></proof>
- <proof prover="12"><result status="valid" time="0.01" steps="3"/></proof>
  <proof prover="14"><result status="valid" time="0.01"/></proof>
  </goal>
 </theory>
 <theory name="PowerIntTest" proved="true">
  <goal name="Pow_2_2" proved="true">
+ <proof prover="1" timelimit="60" memlimit="1000"><result status="valid" time="0.02" steps="12"/></proof>
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="8"><result status="valid" time="0.01"/></proof>
- <proof prover="12" timelimit="60" memlimit="1000"><result status="valid" time="0.02" steps="4"/></proof>
  <proof prover="14"><result status="valid" time="0.01"/></proof>
  </goal>
 </theory>
 <theory name="PowerRealTest" proved="true">
  <goal name="Pow_2_2" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="24"/></proof>
  <proof prover="8"><result status="valid" time="0.01"/></proof>
- <proof prover="12"><result status="valid" time="0.01" steps="8"/></proof>
  <proof prover="14"><result status="valid" time="0.01"/></proof>
  </goal>
 </theory>
 <theory name="TrigonometryTest" proved="true">
  <goal name="Cos_2_pi" proved="true">
+ <proof prover="1"><result status="valid" time="0.12" steps="114"/></proof>
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="8"><result status="valid" time="0.09"/></proof>
- <proof prover="12"><result status="valid" time="0.12" steps="37"/></proof>
  <proof prover="14"><result status="valid" time="0.11"/></proof>
  </goal>
  <goal name="Sin_2_pi" proved="true">
+ <proof prover="1" timelimit="60" memlimit="1000"><result status="valid" time="0.10" steps="52"/></proof>
  <proof prover="2"><result status="valid" time="0.01"/></proof>
  <proof prover="8"><result status="valid" time="0.12"/></proof>
- <proof prover="12" timelimit="60" memlimit="1000"><result status="valid" time="0.10" steps="87"/></proof>
  <proof prover="14"><result status="valid" time="0.17"/></proof>
  </goal>
  <goal name="Tan_pi_4" proved="true">
diff --git a/examples/logic/First/why3session.xml b/examples/logic/First/why3session.xml
index 91c86bcfd39c38c5544f8c6e3b03d81d3e273b17..377a9f40d7c48d9bc92dc8cce4e8d462615ea469 100644
--- a/examples/logic/First/why3session.xml
+++ b/examples/logic/First/why3session.xml
@@ -2,41 +2,38 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
+<prover id="0" name="Alt-Ergo" version="2.2.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="4" name="Spass" version="3.7" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="5" name="Z3" version="4.3.1" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="6" name="Simplify" version="1.5.4" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="7" name="Yices" version="1.0.38" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="8" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/>
-<prover id="9" name="Alt-Ergo" version="0.95.2" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="10" name="CVC4" version="1.3" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="11" name="Vampire" version="0.6" timelimit="5" steplimit="0" memlimit="1000"/>
-<prover id="12" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="13" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/>
 <file name="../First.why" proved="true">
 <theory name="First" proved="true">
  <goal name="P1" proved="true">
+ <proof prover="0"><result status="unknown" time="0.02"/></proof>
  <proof prover="1"><result status="unknown" time="0.00"/></proof>
  <proof prover="4"><result status="valid" time="0.04"/></proof>
  <proof prover="5"><result status="valid" time="0.02"/></proof>
  <proof prover="8"><result status="valid" time="0.01"/></proof>
- <proof prover="9"><result status="unknown" time="0.01"/></proof>
  <proof prover="10"><result status="valid" time="0.00"/></proof>
  <proof prover="11"><result status="valid" time="0.01"/></proof>
- <proof prover="12"><result status="unknown" time="0.02"/></proof>
  <proof prover="13"><result status="valid" time="0.01"/></proof>
  </goal>
  <goal name="P5" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
  <proof prover="1"><result status="valid" time="0.01"/></proof>
  <proof prover="4"><result status="valid" time="0.04"/></proof>
  <proof prover="5"><result status="valid" time="0.02"/></proof>
  <proof prover="6"><result status="valid" time="0.01"/></proof>
  <proof prover="7"><result status="valid" time="0.01"/></proof>
  <proof prover="8"><result status="valid" time="0.01"/></proof>
- <proof prover="9"><result status="valid" time="0.01" steps="3"/></proof>
  <proof prover="10"><result status="valid" time="0.00"/></proof>
  <proof prover="11"><result status="valid" time="0.01"/></proof>
- <proof prover="12"><result status="valid" time="0.01" steps="3"/></proof>
  <proof prover="13"><result status="valid" time="0.01"/></proof>
  </goal>
 </theory>
diff --git a/examples/logic/einstein/why3session.xml b/examples/logic/einstein/why3session.xml
index 0f9f00765abe3a40a68831220426728805580f67..2ebecaf92c4b22bf69b9552587923a8e8ee1f570 100644
--- a/examples/logic/einstein/why3session.xml
+++ b/examples/logic/einstein/why3session.xml
@@ -2,7 +2,6 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
-<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="1" name="Eprover" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="2" name="CVC3" version="2.4.1" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="3" name="CVC4" version="1.4" timelimit="1" steplimit="0" memlimit="1000"/>
@@ -13,19 +12,17 @@
 <prover id="8" name="Metis" version="2.3" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="9" name="Z3" version="3.2" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="10" name="Eprover" version="1.8-001" timelimit="1" steplimit="0" memlimit="1000"/>
-<prover id="11" name="Alt-Ergo" version="0.95.2" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="12" name="Alt-Ergo" version="2.2.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="13" name="CVC4" version="1.3" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="14" name="Vampire" version="0.6" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="16" name="veriT" version="201410" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="17" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
-<prover id="18" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="19" name="Z3" version="4.6.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="20" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="21" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
 <file name="../einstein.why">
 <theory name="Goals">
  <goal name="G1" proved="true">
- <proof prover="0"><result status="timeout" time="1.00"/></proof>
  <proof prover="1"><result status="timeout" time="1.00"/></proof>
  <proof prover="2"><result status="unknown" time="0.17"/></proof>
  <proof prover="3"><result status="unknown" time="0.04"/></proof>
@@ -36,18 +33,16 @@
  <proof prover="8"><result status="timeout" time="1.00"/></proof>
  <proof prover="9"><result status="valid" time="0.48"/></proof>
  <proof prover="10"><result status="timeout" time="1.00"/></proof>
- <proof prover="11"><result status="timeout" time="1.00"/></proof>
+ <proof prover="12"><result status="valid" time="0.10" steps="374"/></proof>
  <proof prover="13"><result status="unknown" time="0.06"/></proof>
  <proof prover="14"><result status="valid" time="1.50"/></proof>
  <proof prover="16"><result status="timeout" time="1.00"/></proof>
  <proof prover="17"><result status="valid" time="1.17" steps="983"/></proof>
- <proof prover="18"><result status="valid" time="1.41" steps="989"/></proof>
  <proof prover="19"><result status="valid" time="0.21"/></proof>
  <proof prover="20"><result status="valid" time="0.21"/></proof>
  <proof prover="21"><result status="valid" time="0.08"/></proof>
  </goal>
  <goal name="Wrong">
- <proof prover="0"><result status="timeout" time="1.00"/></proof>
  <proof prover="1"><result status="timeout" time="1.00"/></proof>
  <proof prover="2"><result status="unknown" time="0.06"/></proof>
  <proof prover="3"><result status="unknown" time="0.04"/></proof>
@@ -58,18 +53,16 @@
  <proof prover="8"><result status="timeout" time="1.00"/></proof>
  <proof prover="9"><result status="timeout" time="1.00"/></proof>
  <proof prover="10"><result status="timeout" time="1.00"/></proof>
- <proof prover="11"><result status="timeout" time="1.00"/></proof>
+ <proof prover="12" timelimit="1"><result status="unknown" time="0.16"/></proof>
  <proof prover="13"><result status="unknown" time="0.06"/></proof>
  <proof prover="14"><result status="timeout" time="1.00"/></proof>
  <proof prover="16"><result status="timeout" time="1.00"/></proof>
  <proof prover="17"><result status="unknown" time="0.57"/></proof>
- <proof prover="18"><result status="unknown" time="0.66"/></proof>
  <proof prover="19"><result status="timeout" time="1.00"/></proof>
  <proof prover="20"><result status="timeout" time="1.00"/></proof>
  <proof prover="21"><result status="unknown" time="0.07"/></proof>
  </goal>
  <goal name="G2" proved="true">
- <proof prover="0"><result status="timeout" time="1.00"/></proof>
  <proof prover="1"><result status="timeout" time="1.00"/></proof>
  <proof prover="2"><result status="unknown" time="0.06"/></proof>
  <proof prover="3"><result status="unknown" time="0.04"/></proof>
@@ -80,12 +73,11 @@
  <proof prover="8"><result status="timeout" time="1.00"/></proof>
  <proof prover="9"><result status="valid" time="0.62"/></proof>
  <proof prover="10"><result status="valid" time="0.79"/></proof>
- <proof prover="11"><result status="valid" time="7.80" steps="1007"/></proof>
+ <proof prover="12"><result status="valid" time="0.11" steps="385"/></proof>
  <proof prover="13"><result status="unknown" time="0.06"/></proof>
  <proof prover="14"><result status="valid" time="1.27"/></proof>
  <proof prover="16"><result status="timeout" time="1.00"/></proof>
  <proof prover="17"><result status="valid" time="0.96" steps="1152"/></proof>
- <proof prover="18"><result status="valid" time="0.95" steps="1156"/></proof>
  <proof prover="19"><result status="valid" time="0.20"/></proof>
  <proof prover="20"><result status="valid" time="0.18"/></proof>
  <proof prover="21"><result status="valid" time="0.05"/></proof>
diff --git a/examples/logic/ffx/why3session.xml b/examples/logic/ffx/why3session.xml
index dff267f30b18685f91a1a633909eb148847c8533..1577d100e5b798e19e9bdaa7713392e5ff5b630f 100644
--- a/examples/logic/ffx/why3session.xml
+++ b/examples/logic/ffx/why3session.xml
@@ -8,7 +8,6 @@
 <prover id="3" name="Spass" version="3.7" timelimit="15" steplimit="0" memlimit="4000"/>
 <prover id="4" name="Z3" version="4.3.1" timelimit="15" steplimit="0" memlimit="4000"/>
 <prover id="5" name="Simplify" version="1.5.4" timelimit="15" steplimit="0" memlimit="4000"/>
-<prover id="6" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="7" name="Yices" version="1.0.38" timelimit="15" steplimit="0" memlimit="4000"/>
 <prover id="8" name="Zenon" version="0.7.1" timelimit="15" steplimit="0" memlimit="4000"/>
 <prover id="9" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
@@ -20,6 +19,7 @@
 <prover id="15" name="CVC4" version="1.3" timelimit="15" steplimit="0" memlimit="4000"/>
 <prover id="16" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="17" name="Vampire" version="0.6" timelimit="15" steplimit="0" memlimit="4000"/>
+<prover id="18" name="Alt-Ergo" version="2.2.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <file name="../ffx.why" proved="true">
 <theory name="T" proved="true">
  <goal name="g1" proved="true">
@@ -28,7 +28,6 @@
  <proof prover="3"><result status="valid" time="0.00"/></proof>
  <proof prover="4"><result status="valid" time="0.00"/></proof>
  <proof prover="5"><result status="unknown" time="0.00"/></proof>
- <proof prover="6"><result status="unknown" time="0.01"/></proof>
  <proof prover="7"><result status="unknown" time="0.00"/></proof>
  <proof prover="8"><result status="valid" time="0.04"/></proof>
  <proof prover="9"><result status="valid" time="0.01"/></proof>
@@ -39,6 +38,7 @@
  <proof prover="15"><result status="valid" time="0.00"/></proof>
  <proof prover="16"><result status="unknown" time="0.00"/></proof>
  <proof prover="17"><result status="valid" time="0.00"/></proof>
+ <proof prover="18"><result status="unknown" time="0.01"/></proof>
  </goal>
  <goal name="g2" proved="true">
  <proof prover="0"><result status="unknown" time="0.00"/></proof>
@@ -46,7 +46,6 @@
  <proof prover="3"><result status="valid" time="0.01"/></proof>
  <proof prover="4"><result status="valid" time="0.00"/></proof>
  <proof prover="5"><result status="unknown" time="0.00"/></proof>
- <proof prover="6"><result status="unknown" time="0.00"/></proof>
  <proof prover="7"><result status="unknown" time="0.00"/></proof>
  <proof prover="8"><result status="valid" time="0.97"/></proof>
  <proof prover="9"><result status="valid" time="0.01"/></proof>
@@ -57,6 +56,7 @@
  <proof prover="15"><result status="valid" time="0.00"/></proof>
  <proof prover="16"><result status="unknown" time="0.00"/></proof>
  <proof prover="17"><result status="valid" time="0.00"/></proof>
+ <proof prover="18"><result status="unknown" time="0.00"/></proof>
  </goal>
  <goal name="g3" proved="true">
  <proof prover="0"><result status="unknown" time="0.00"/></proof>
@@ -135,7 +135,6 @@
  <proof prover="3"><result status="valid" time="0.01"/></proof>
  <proof prover="4"><result status="valid" time="1.00"/></proof>
  <proof prover="5"><result status="unknown" time="0.00"/></proof>
- <proof prover="6" timelimit="1"><result status="unknown" time="0.01"/></proof>
  <proof prover="7"><result status="unknown" time="0.00"/></proof>
  <proof prover="8"><result status="timeout" time="15.00"/></proof>
  <proof prover="9"><result status="timeout" time="1.00"/></proof>
@@ -146,6 +145,7 @@
  <proof prover="15"><result status="valid" time="0.00"/></proof>
  <proof prover="16"><result status="unknown" time="0.00"/></proof>
  <proof prover="17"><result status="valid" time="0.00"/></proof>
+ <proof prover="18" timelimit="1"><result status="unknown" time="0.01"/></proof>
  </goal>
 </theory>
 </file>
diff --git a/examples/tests-provers/ceil/why3session.xml b/examples/tests-provers/ceil/why3session.xml
index 994d012451f3c5c7f5d78651a9993a8fcc4709e3..d971e43df3e3a9a611be957d4370956d85656412 100644
--- a/examples/tests-provers/ceil/why3session.xml
+++ b/examples/tests-provers/ceil/why3session.xml
@@ -3,42 +3,42 @@
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
 <prover id="0" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
+<prover id="1" name="Alt-Ergo" version="2.2.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="6" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="8" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
-<prover id="9" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
 <file name="../ceil.why" proved="true">
 <theory name="Ceil" proved="true">
  <goal name="ceil_obvious" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="29"/></proof>
  <proof prover="6"><result status="valid" time="0.01"/></proof>
  <proof prover="8"><result status="valid" time="0.01"/></proof>
- <proof prover="9"><result status="valid" time="0.01" steps="20"/></proof>
  </goal>
  <goal name="unity" proved="true">
  <proof prover="0"><result status="valid" time="0.00"/></proof>
+ <proof prover="1"><result status="valid" time="0.01" steps="6"/></proof>
  <proof prover="6"><result status="valid" time="0.00"/></proof>
  <proof prover="8"><result status="valid" time="0.00"/></proof>
- <proof prover="9"><result status="valid" time="0.01" steps="3"/></proof>
  </goal>
  <goal name="unity2" proved="true">
  <proof prover="0"><result status="valid" time="0.00"/></proof>
+ <proof prover="1"><result status="valid" time="0.01" steps="6"/></proof>
  <proof prover="6"><result status="valid" time="0.00"/></proof>
  <proof prover="8"><result status="valid" time="0.00"/></proof>
- <proof prover="9"><result status="valid" time="0.01" steps="3"/></proof>
  </goal>
  <goal name="perm_div" proved="true">
  <proof prover="0"><result status="valid" time="0.00"/></proof>
+ <proof prover="1"><result status="valid" time="0.01" steps="10"/></proof>
  <proof prover="6"><result status="valid" time="0.00"/></proof>
  <proof prover="8"><result status="valid" time="0.00"/></proof>
- <proof prover="9"><result status="valid" time="0.01" steps="5"/></proof>
  </goal>
  <goal name="perm_div2" proved="true">
  <proof prover="6"><result status="valid" time="0.01"/></proof>
  <proof prover="8"><result status="valid" time="0.01"/></proof>
  </goal>
  <goal name="div_mult_perm" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="8"/></proof>
  <proof prover="6"><result status="valid" time="0.01"/></proof>
  <proof prover="8"><result status="valid" time="0.01"/></proof>
- <proof prover="9"><result status="valid" time="0.01" steps="4"/></proof>
  </goal>
  <goal name="b_div_b_is_one" proved="true">
  <proof prover="0"><result status="valid" time="0.00"/></proof>
@@ -46,30 +46,30 @@
  <proof prover="8"><result status="valid" time="0.01"/></proof>
  </goal>
  <goal name="inverse_inverse_is_same" proved="true">
+ <proof prover="1"><result status="valid" time="0.02" steps="8"/></proof>
  <proof prover="6"><result status="valid" time="0.01"/></proof>
  <proof prover="8"><result status="valid" time="0.01"/></proof>
- <proof prover="9"><result status="valid" time="0.02" steps="12"/></proof>
  </goal>
  <goal name="inverse_bigger_zero" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="6"/></proof>
  <proof prover="6"><result status="valid" time="0.02"/></proof>
  <proof prover="8"><result status="valid" time="0.02"/></proof>
- <proof prover="9"><result status="valid" time="0.00" steps="4"/></proof>
  </goal>
  <goal name="div_equals_mult_w_inverse" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="8"/></proof>
  <proof prover="6"><result status="valid" time="0.02"/></proof>
  <proof prover="8"><result status="valid" time="0.01"/></proof>
- <proof prover="9"><result status="valid" time="0.01" steps="7"/></proof>
  </goal>
  <goal name="mult_bigger_zero" proved="true">
  <proof prover="0"><result status="valid" time="0.00"/></proof>
+ <proof prover="1"><result status="valid" time="0.01" steps="8"/></proof>
  <proof prover="6"><result status="valid" time="0.01"/></proof>
  <proof prover="8"><result status="valid" time="0.02"/></proof>
- <proof prover="9"><result status="valid" time="0.01" steps="4"/></proof>
  </goal>
  <goal name="ceil_never_zero" proved="true">
+ <proof prover="1"><result status="valid" time="0.10" steps="10"/></proof>
  <proof prover="6"><result status="valid" time="0.01"/></proof>
  <proof prover="8"><result status="valid" time="0.01"/></proof>
- <proof prover="9"><result status="valid" time="0.10" steps="23"/></proof>
  </goal>
 </theory>
 </file>
diff --git a/examples/tests-provers/div/why3session.xml b/examples/tests-provers/div/why3session.xml
index 13e9bb1cb5d69177893207b3f91e44d4db4f1670..8b3cfdbbd7c1f20e1721cf3b06d9cd8834329774 100644
--- a/examples/tests-provers/div/why3session.xml
+++ b/examples/tests-provers/div/why3session.xml
@@ -2,8 +2,7 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
-<prover id="0" name="Alt-Ergo" version="1.01" timelimit="2" steplimit="0" memlimit="1000"/>
-<prover id="1" name="Alt-Ergo" version="2.2.0" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="1" name="Alt-Ergo" version="2.2.0" timelimit="2" steplimit="0" memlimit="1000"/>
 <prover id="2" name="CVC3" version="2.4.1" timelimit="2" steplimit="0" memlimit="4000"/>
 <prover id="3" name="Z3" version="4.4.1" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="5" name="Eprover" version="2.0" timelimit="1" steplimit="0" memlimit="1000"/>
@@ -12,25 +11,22 @@
 <prover id="8" name="Z3" version="4.3.1" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="9" name="Spass" version="3.7" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="10" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
-<prover id="11" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="12" name="Yices" version="1.0.38" timelimit="2" steplimit="0" memlimit="4000"/>
 <prover id="13" name="Z3" version="3.2" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="14" name="Metis" version="2.3" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="15" name="Gappa" version="1.3.0" timelimit="2" steplimit="0" memlimit="4000"/>
 <prover id="16" name="Eprover" version="1.8-001" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="18" name="iProver" version="0.8.1" timelimit="5" steplimit="0" memlimit="1000"/>
-<prover id="19" name="Alt-Ergo" version="0.95.2" timelimit="2" steplimit="0" memlimit="1000"/>
 <prover id="20" name="CVC4" version="1.3" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="21" name="Vampire" version="0.6" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="22" name="veriT" version="201410" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="23" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
-<prover id="24" name="Alt-Ergo" version="0.99.1" timelimit="2" steplimit="0" memlimit="1000"/>
 <prover id="25" name="MetiTarski" version="2.4" timelimit="2" steplimit="0" memlimit="4000"/>
 <prover id="26" name="Z3" version="4.3.2" timelimit="1" steplimit="0" memlimit="1000"/>
 <file name="../div.why">
 <theory name="EuclideanDivTest">
  <goal name="ok1" proved="true">
- <proof prover="0"><result status="valid" time="0.00" steps="0"/></proof>
+ <proof prover="1"><result status="valid" time="0.00" steps="0"/></proof>
  <proof prover="2"><result status="valid" time="0.01"/></proof>
  <proof prover="5"><result status="timeout" time="1.00"/></proof>
  <proof prover="6"><result status="valid" time="0.00"/></proof>
@@ -38,20 +34,17 @@
  <proof prover="8"><result status="valid" time="0.00"/></proof>
  <proof prover="9"><result status="timeout" time="1.00"/></proof>
  <proof prover="10"><result status="valid" time="0.00" steps="1"/></proof>
- <proof prover="11"><result status="valid" time="0.00" steps="1"/></proof>
  <proof prover="13"><result status="valid" time="0.00"/></proof>
  <proof prover="14"><result status="timeout" time="1.00"/></proof>
  <proof prover="16"><result status="timeout" time="1.00"/></proof>
- <proof prover="19"><result status="valid" time="0.01" steps="0"/></proof>
  <proof prover="20"><result status="valid" time="0.00"/></proof>
  <proof prover="21"><result status="timeout" time="1.00"/></proof>
  <proof prover="22"><result status="valid" time="0.00"/></proof>
  <proof prover="23"><result status="valid" time="0.02"/></proof>
- <proof prover="24"><result status="valid" time="0.00" steps="0"/></proof>
  <proof prover="26"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="ok2" proved="true">
- <proof prover="0"><result status="valid" time="0.00" steps="0"/></proof>
+ <proof prover="1"><result status="valid" time="0.01" steps="0"/></proof>
  <proof prover="2"><result status="valid" time="0.01"/></proof>
  <proof prover="5"><result status="timeout" time="1.00"/></proof>
  <proof prover="6"><result status="valid" time="0.00"/></proof>
@@ -59,20 +52,17 @@
  <proof prover="8"><result status="valid" time="0.00"/></proof>
  <proof prover="9"><result status="timeout" time="1.00"/></proof>
  <proof prover="10"><result status="valid" time="0.00" steps="1"/></proof>
- <proof prover="11"><result status="valid" time="0.00" steps="1"/></proof>
  <proof prover="13"><result status="valid" time="0.00"/></proof>
  <proof prover="14"><result status="timeout" time="1.00"/></proof>
  <proof prover="16"><result status="timeout" time="1.00"/></proof>
- <proof prover="19"><result status="valid" time="0.01" steps="0"/></proof>
  <proof prover="20"><result status="valid" time="0.01"/></proof>
  <proof prover="21"><result status="timeout" time="1.00"/></proof>
  <proof prover="22"><result status="valid" time="0.00"/></proof>
  <proof prover="23"><result status="valid" time="0.02"/></proof>
- <proof prover="24"><result status="valid" time="0.01" steps="0"/></proof>
  <proof prover="26"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="ok3" proved="true">
- <proof prover="0"><result status="valid" time="0.00" steps="0"/></proof>
+ <proof prover="1"><result status="valid" time="0.01" steps="0"/></proof>
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="5"><result status="timeout" time="1.00"/></proof>
  <proof prover="6"><result status="valid" time="0.00"/></proof>
@@ -80,20 +70,17 @@
  <proof prover="8"><result status="valid" time="0.00"/></proof>
  <proof prover="9"><result status="timeout" time="1.00"/></proof>
  <proof prover="10"><result status="valid" time="0.00" steps="1"/></proof>
- <proof prover="11"><result status="valid" time="0.00" steps="1"/></proof>
  <proof prover="13"><result status="valid" time="0.00"/></proof>
  <proof prover="14"><result status="timeout" time="1.00"/></proof>
  <proof prover="16"><result status="timeout" time="1.00"/></proof>
- <proof prover="19"><result status="valid" time="0.02" steps="0"/></proof>
  <proof prover="20"><result status="valid" time="0.01"/></proof>
  <proof prover="21"><result status="timeout" time="1.00"/></proof>
  <proof prover="22"><result status="valid" time="0.00"/></proof>
  <proof prover="23"><result status="valid" time="0.01"/></proof>
- <proof prover="24"><result status="valid" time="0.01" steps="0"/></proof>
  <proof prover="26"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="ok4" proved="true">
- <proof prover="0"><result status="valid" time="0.00" steps="0"/></proof>
+ <proof prover="1"><result status="valid" time="0.00" steps="0"/></proof>
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="5"><result status="timeout" time="1.00"/></proof>
  <proof prover="6"><result status="valid" time="0.00"/></proof>
@@ -101,20 +88,17 @@
  <proof prover="8"><result status="valid" time="0.00"/></proof>
  <proof prover="9"><result status="timeout" time="1.00"/></proof>
  <proof prover="10"><result status="valid" time="0.00" steps="1"/></proof>
- <proof prover="11"><result status="valid" time="0.00" steps="1"/></proof>
  <proof prover="13"><result status="valid" time="0.00"/></proof>
  <proof prover="14"><result status="timeout" time="1.00"/></proof>
  <proof prover="16"><result status="timeout" time="1.00"/></proof>
- <proof prover="19"><result status="valid" time="0.02" steps="0"/></proof>
  <proof prover="20"><result status="valid" time="0.01"/></proof>
  <proof prover="21"><result status="timeout" time="1.00"/></proof>
  <proof prover="22"><result status="valid" time="0.00"/></proof>
  <proof prover="23"><result status="valid" time="0.01"/></proof>
- <proof prover="24"><result status="valid" time="0.00" steps="0"/></proof>
  <proof prover="26"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="ok5" proved="true">
- <proof prover="0"><result status="valid" time="0.00" steps="0"/></proof>
+ <proof prover="1"><result status="valid" time="0.01" steps="0"/></proof>
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="5"><result status="timeout" time="1.00"/></proof>
  <proof prover="6"><result status="valid" time="0.00"/></proof>
@@ -122,19 +106,16 @@
  <proof prover="8"><result status="valid" time="0.00"/></proof>
  <proof prover="9"><result status="timeout" time="1.00"/></proof>
  <proof prover="10"><result status="valid" time="0.00" steps="1"/></proof>
- <proof prover="11"><result status="valid" time="0.00" steps="1"/></proof>
  <proof prover="13"><result status="valid" time="0.00"/></proof>
  <proof prover="14"><result status="timeout" time="1.00"/></proof>
  <proof prover="16"><result status="timeout" time="1.00"/></proof>
- <proof prover="19"><result status="valid" time="0.01" steps="0"/></proof>
  <proof prover="20"><result status="valid" time="0.01"/></proof>
  <proof prover="21"><result status="timeout" time="1.00"/></proof>
  <proof prover="23"><result status="valid" time="0.01"/></proof>
- <proof prover="24"><result status="valid" time="0.01" steps="0"/></proof>
  <proof prover="26"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="ok6" proved="true">
- <proof prover="0"><result status="valid" time="0.00" steps="0"/></proof>
+ <proof prover="1"><result status="valid" time="0.01" steps="0"/></proof>
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="5"><result status="timeout" time="1.00"/></proof>
  <proof prover="6"><result status="valid" time="0.00"/></proof>
@@ -142,16 +123,13 @@
  <proof prover="8"><result status="valid" time="0.00"/></proof>
  <proof prover="9"><result status="timeout" time="1.00"/></proof>
  <proof prover="10"><result status="valid" time="0.00" steps="1"/></proof>
- <proof prover="11"><result status="valid" time="0.00" steps="1"/></proof>
  <proof prover="13"><result status="valid" time="0.00"/></proof>
  <proof prover="14"><result status="timeout" time="1.00"/></proof>
  <proof prover="16"><result status="timeout" time="1.00"/></proof>
- <proof prover="19"><result status="valid" time="0.02" steps="0"/></proof>
  <proof prover="20"><result status="valid" time="0.01"/></proof>
  <proof prover="21"><result status="timeout" time="1.00"/></proof>
  <proof prover="22"><result status="valid" time="0.00"/></proof>
  <proof prover="23"><result status="valid" time="0.01"/></proof>
- <proof prover="24"><result status="valid" time="0.01" steps="0"/></proof>
  <proof prover="26"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="smoke1">
@@ -216,6 +194,7 @@
  <proof prover="26"><result status="timeout" time="1.00"/></proof>
  </goal>
  <goal name="smoke4">
+ <proof prover="1" timelimit="1"><result status="timeout" time="1.00"/></proof>
  <proof prover="2"><result status="unknown" time="0.06"/></proof>
  <proof prover="5"><result status="timeout" time="1.00"/></proof>
  <proof prover="6"><result status="unknown" time="0.01"/></proof>
@@ -223,7 +202,6 @@
  <proof prover="8"><result status="timeout" time="1.00"/></proof>
  <proof prover="9"><result status="timeout" time="1.00"/></proof>
  <proof prover="10"><result status="timeout" time="1.00"/></proof>
- <proof prover="11"><result status="timeout" time="1.00"/></proof>
  <proof prover="12"><result status="unknown" time="0.01"/></proof>
  <proof prover="13"><result status="timeout" time="1.00"/></proof>
  <proof prover="14"><result status="timeout" time="1.00"/></proof>
@@ -279,7 +257,7 @@
 </theory>
 <theory name="ComputerDivTest">
  <goal name="ok1" proved="true">
- <proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
+ <proof prover="1"><result status="valid" time="0.02" steps="2"/></proof>
  <proof prover="2"><result status="valid" time="0.01"/></proof>
  <proof prover="5"><result status="timeout" time="1.00"/></proof>
  <proof prover="6"><result status="valid" time="0.01"/></proof>
@@ -287,20 +265,17 @@
  <proof prover="8"><result status="valid" time="0.02"/></proof>
  <proof prover="9"><result status="timeout" time="1.00"/></proof>
  <proof prover="10"><result status="valid" time="0.01" steps="4"/></proof>
- <proof prover="11"><result status="valid" time="0.00" steps="4"/></proof>
  <proof prover="13"><result status="valid" time="0.01"/></proof>
  <proof prover="14"><result status="timeout" time="1.00"/></proof>
  <proof prover="16"><result status="timeout" time="1.00"/></proof>
- <proof prover="19"><result status="valid" time="0.02" steps="3"/></proof>
  <proof prover="20"><result status="valid" time="0.01"/></proof>
  <proof prover="21"><result status="timeout" time="1.00"/></proof>
  <proof prover="22"><result status="valid" time="0.00"/></proof>
  <proof prover="23"><result status="valid" time="0.02"/></proof>
- <proof prover="24"><result status="valid" time="0.02" steps="3"/></proof>
  <proof prover="26"><result status="valid" time="0.01"/></proof>
  </goal>
  <goal name="ok2" proved="true">
- <proof prover="0"><result status="valid" time="0.00" steps="4"/></proof>
+ <proof prover="1"><result status="valid" time="0.02" steps="2"/></proof>
  <proof prover="2"><result status="valid" time="0.01"/></proof>
  <proof prover="5"><result status="timeout" time="1.00"/></proof>
  <proof prover="6"><result status="valid" time="0.01"/></proof>
@@ -308,20 +283,17 @@
  <proof prover="8"><result status="valid" time="0.02"/></proof>
  <proof prover="9"><result status="timeout" time="1.00"/></proof>
  <proof prover="10"><result status="valid" time="0.00" steps="5"/></proof>
- <proof prover="11"><result status="valid" time="0.01" steps="5"/></proof>
  <proof prover="13"><result status="valid" time="0.01"/></proof>
  <proof prover="14"><result status="timeout" time="1.00"/></proof>
  <proof prover="16"><result status="timeout" time="1.00"/></proof>
- <proof prover="19"><result status="valid" time="0.02" steps="4"/></proof>
  <proof prover="20"><result status="valid" time="0.00"/></proof>
  <proof prover="21"><result status="timeout" time="1.00"/></proof>
  <proof prover="22"><result status="valid" time="0.00"/></proof>
  <proof prover="23"><result status="valid" time="0.02"/></proof>
- <proof prover="24"><result status="valid" time="0.02" steps="4"/></proof>
  <proof prover="26"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="ok3" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="3"/></proof>
+ <proof prover="1"><result status="valid" time="0.02" steps="2"/></proof>
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="5"><result status="timeout" time="1.00"/></proof>
  <proof prover="6"><result status="valid" time="0.01"/></proof>
@@ -329,20 +301,17 @@
  <proof prover="8"><result status="valid" time="0.02"/></proof>
  <proof prover="9"><result status="timeout" time="1.00"/></proof>
  <proof prover="10"><result status="valid" time="0.01" steps="4"/></proof>
- <proof prover="11"><result status="valid" time="0.01" steps="4"/></proof>
  <proof prover="13"><result status="valid" time="0.01"/></proof>
  <proof prover="14"><result status="timeout" time="1.00"/></proof>
  <proof prover="16"><result status="timeout" time="1.00"/></proof>
- <proof prover="19"><result status="valid" time="0.02" steps="3"/></proof>
  <proof prover="20"><result status="valid" time="0.00"/></proof>
  <proof prover="21"><result status="timeout" time="1.00"/></proof>
  <proof prover="22"><result status="valid" time="0.00"/></proof>
  <proof prover="23"><result status="valid" time="0.02"/></proof>
- <proof prover="24"><result status="valid" time="0.02" steps="3"/></proof>
  <proof prover="26"><result status="valid" time="0.01"/></proof>
  </goal>
  <goal name="ok4" proved="true">
- <proof prover="0"><result status="valid" time="0.00" steps="4"/></proof>
+ <proof prover="1"><result status="valid" time="0.03" steps="2"/></proof>
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="5"><result status="timeout" time="1.00"/></proof>
  <proof prover="6"><result status="valid" time="0.00"/></proof>
@@ -350,20 +319,17 @@
  <proof prover="8"><result status="valid" time="0.03"/></proof>
  <proof prover="9"><result status="timeout" time="1.00"/></proof>
  <proof prover="10"><result status="valid" time="0.00" steps="5"/></proof>
- <proof prover="11"><result status="valid" time="0.01" steps="5"/></proof>
  <proof prover="13"><result status="valid" time="0.02"/></proof>
  <proof prover="14"><result status="timeout" time="1.00"/></proof>
  <proof prover="16"><result status="timeout" time="1.00"/></proof>
- <proof prover="19"><result status="valid" time="0.01" steps="4"/></proof>
  <proof prover="20"><result status="valid" time="0.01"/></proof>
  <proof prover="21"><result status="timeout" time="1.00"/></proof>
  <proof prover="22"><result status="valid" time="0.00"/></proof>
  <proof prover="23"><result status="valid" time="0.02"/></proof>
- <proof prover="24"><result status="valid" time="0.03" steps="4"/></proof>
  <proof prover="26"><result status="valid" time="0.02"/></proof>
  </goal>
  <goal name="ok5" proved="true">
- <proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
+ <proof prover="1"><result status="valid" time="0.01" steps="2"/></proof>
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="5"><result status="timeout" time="1.00"/></proof>
  <proof prover="6"><result status="valid" time="0.01"/></proof>
@@ -371,20 +337,17 @@
  <proof prover="8"><result status="valid" time="0.00"/></proof>
  <proof prover="9"><result status="timeout" time="1.00"/></proof>
  <proof prover="10"><result status="valid" time="0.00" steps="4"/></proof>
- <proof prover="11"><result status="valid" time="0.01" steps="4"/></proof>
  <proof prover="13"><result status="valid" time="0.01"/></proof>
  <proof prover="14"><result status="timeout" time="1.00"/></proof>
  <proof prover="16"><result status="timeout" time="1.00"/></proof>
- <proof prover="19"><result status="valid" time="0.02" steps="3"/></proof>
  <proof prover="20"><result status="valid" time="0.00"/></proof>
  <proof prover="21"><result status="timeout" time="1.00"/></proof>
  <proof prover="22"><result status="valid" time="0.00"/></proof>
  <proof prover="23"><result status="valid" time="0.02"/></proof>
- <proof prover="24"><result status="valid" time="0.01" steps="3"/></proof>
  <proof prover="26"><result status="valid" time="0.01"/></proof>
  </goal>
  <goal name="ok6" proved="true">
- <proof prover="0"><result status="valid" time="0.00" steps="4"/></proof>
+ <proof prover="1"><result status="valid" time="0.01" steps="2"/></proof>
  <proof prover="2"><result status="valid" time="0.01"/></proof>
  <proof prover="5"><result status="timeout" time="1.00"/></proof>
  <proof prover="6"><result status="valid" time="0.00"/></proof>
@@ -392,16 +355,13 @@
  <proof prover="8"><result status="valid" time="0.00"/></proof>
  <proof prover="9"><result status="timeout" time="1.00"/></proof>
  <proof prover="10"><result status="valid" time="0.00" steps="5"/></proof>
- <proof prover="11"><result status="valid" time="0.01" steps="5"/></proof>
  <proof prover="13"><result status="valid" time="0.01"/></proof>
  <proof prover="14"><result status="timeout" time="1.00"/></proof>
  <proof prover="16"><result status="timeout" time="1.00"/></proof>
- <proof prover="19"><result status="valid" time="0.01" steps="4"/></proof>
  <proof prover="20"><result status="valid" time="0.01"/></proof>
  <proof prover="21"><result status="timeout" time="1.00"/></proof>
  <proof prover="22"><result status="valid" time="0.00"/></proof>
  <proof prover="23"><result status="valid" time="0.02"/></proof>
- <proof prover="24"><result status="valid" time="0.01" steps="4"/></proof>
  <proof prover="26"><result status="valid" time="0.01"/></proof>
  </goal>
  <goal name="smoke1">
@@ -526,7 +486,7 @@
  <proof prover="26"><result status="timeout" time="1.00"/></proof>
  </goal>
  <goal name="div_pos_neg" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="6"/></proof>
+ <proof prover="1" timelimit="1"><result status="valid" time="0.01" steps="6"/></proof>
  <proof prover="3"><result status="valid" time="0.04"/></proof>
  </goal>
 </theory>