Commit 467c7a6b authored by MARCHE Claude's avatar MARCHE Claude

short test

parent 07bcbc0e
......@@ -2,9 +2,11 @@
theory T
use import int.Int
use import real.RealInfix
use import int.Power
use real.PowerInt as P
goal g: power 2 3321941 < power 10 (power 10 6 + 4) < power 2 3321942
goal g: 0x1p3321941 <. P.power 10.0 (power 10 6 + 4) <. 0x1p3321942
end
This diff is collapsed.
......@@ -38,24 +38,25 @@
<goal
name="g"
locfile="../computation.why"
loclnum="7" loccnumb="5" loccnume="6"
sum="d360b93003fb60f5e122e2f5936933a3"
loclnum="9" loccnumb="5" loccnume="6"
sum="b9dc114f4226fbd89c982952733f6c91"
proved="false"
expanded="true"
shape="ainfix &lt;apowerc10ainfix +apowerc10c6c4apowerc2c3321942Aainfix &lt;apowerc2c3321941apowerc10ainfix +apowerc10c6c4">
shape="ainfix &lt;.apowerc10.0ainfix +apowerc10c6c4c0x1.p3321942Aainfix &lt;.c0x1.p3321941apowerc10.0ainfix +apowerc10c6c4">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
edited="computation-T-g_1.why"
obsolete="true"
archived="false">
<result status="timeout" time="4.99"/>
<undone/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
obsolete="true"
archived="false">
<result status="timeout" time="5.00"/>
</proof>
......@@ -63,7 +64,7 @@
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
obsolete="true"
archived="false">
<result status="timeout" time="4.93"/>
</proof>
......@@ -80,7 +81,7 @@
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
obsolete="true"
archived="false">
<result status="timeout" time="5.20"/>
</proof>
......@@ -88,7 +89,7 @@
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
obsolete="true"
archived="false">
<result status="timeout" time="5.02"/>
</proof>
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment