SLFQ - An example simplification problem

The file examples/Ex5 from the SLFQ installation contains a formula that was sent to me by Andreas Weber. It was the output of a session with the Redlog system. The formula is quite large but, as we'll see, it actually defines a very simple set. The following is a session with SLFQ:

% time ./slfq examples/Ex5 -q -a "beta4 > 0 /\ nu > 0"
511000 beta4 - 60850 nu - 1217 > 0
316.020u 3.010s 10:43.80 49.5%  0+0k 0+0io 276pf+0w
%

The -a option has been used to add the assumptions that beta4 and nu are both positive. Thus, the equivalent formula is really:

beta4 > 0 /\ nu > 0 /\ 60850 nu - 511000 beta4 + 1217 < 0

In the original formula as I recieved it, the contents of examples/Ex5 were actually conjoined with beta4 > 0 /\ nu > 0. The user, not the system, must recognize that such constraints are actually fundamental to the problem and should be made explicit assumptions. Without this assumption, SLFQ spends a lot of time trying to find a simple way of expressing sets in the plane that are outside of beta4 > 0 /\ nu > 0, which is wasted effort.

The -q option asks the program to run in a "quiet" mode, where intermediate information is not printed out.