metis solves one goal of einstein.why

examples/logic/einstein/why3session.xml

@@ -125,10 +125,10 @@
     <proof
      prover="4"
      timelimit="5"
-     memlimit="1000"
+     memlimit="4000"
      obsolete="false"
      archived="false">
-     <result status="unknown" time="4.95"/>
+     <result status="unknown" time="9.97"/>
     </proof>
     <proof
      prover="5"
@@ -222,10 +222,10 @@
     <proof
      prover="4"
      timelimit="5"
-     memlimit="1000"
+     memlimit="4000"
      obsolete="false"
      archived="false">
-     <result status="unknown" time="4.50"/>
+     <result status="unknown" time="9.95"/>
     </proof>
     <proof
      prover="5"
@@ -319,10 +319,10 @@
     <proof
      prover="4"
      timelimit="5"
-     memlimit="1000"
+     memlimit="4000"
      obsolete="false"
      archived="false">
-     <result status="unknown" time="4.99"/>
+     <result status="valid" time="3.88"/>
     </proof>
     <proof
      prover="5"