[Termtools] Re: Final run will be tomorrow

renewed. I guess this resulted in former timeouts to turn to success.

but in these cases (complexity) I think that Aprove has some (trivial) bound very early, but keeps looking for better bounds, and prints the trivial bound only at the very last moment.

"faster stareexec" does not help here - but exact timing does.

One could have a different mode for competition: output is a sequence of (true) statements BOUNDS(low,hi) (of nested intervals), and the last (narrowest) one counts. I think applications would prefer something like this as well.

- J.