%The formula after virtual sub, has 3 forall quantifiers left;
%qepcad runs forever;
%slfq can simplify the formula, IF we remove the last two conjuncts.
% We get the following...it does not have the FORALL variables!!
% [ c >= 0 /\ b >= 0 /\ [ 2000 c b - b + 2000 c = 0 \/ [ 2200 c - 1 > 0 /\ b > 0 ] \/ [ 2200 c - 1 < 0 /\ b > 0 ] ] ]
% There were 3174 QEPCADB calls!
% System time: 3320 milliseconds.
% System time after the initialization: 2800 milliseconds.
% c = 1/2000, b = anything! or c=1/2200 and b=10;
% subbing c=1/2200 and b=10 yield TRUE; hence verified.
% subbing c=1/2000 and b left as param gives big formula; not tried simplifying

on echo;
load_package redlog;
rlset r;
load_package qepcad;
on rlqefbqepcad;      % use QEPCAD as the fallback QE
rlqepcadn(100*10^6);  % The number of cells used by QEPCAD. The
		      % default is (only) 1 * 10^6.
rlqepcadl(200*10^3);  % The size of the prime list used by QEPCAD. The
		      % default is (only) 2 * 10^3.
on rlverbose;
on time;
off rlqefb;		% No fallback QE


phi1 :=
  (  	beta^2 <= 1 impl
    ( 2*(we + b*intwe)*(b*we -5*we-10*intwe+(L-optL)*beta) + 2*a*intwe*we + 2*c*(L-optL)*(-1000*intwe-2200*we)*beta <= 0));

phi3 :=
  (  	beta^2 <= 1 impl
    ( 2*(we + (10/22)*intwe)*((10/22)*we -5*we-10*intwe+(L-optL)*beta) + 2*a*intwe*we + 2*(1/2200)*(L-optL)*(-1000*intwe-2200*we)*beta <= 0));
%we get c=1/2200 and b = 1000*c
% we also get 14641*a^2  - 353320*a + 921600 <= 0
% which wolfram tells me is 360/121 <= a <= 2560/121...i.e. 3 <= a <= 21
%phi := phi1 and phi2 and phi3;
% we get (we+ b*intwe)^2 + a*intwe^2 + c*(L-Lopt)^2 as a Lyapunov....

phi := phi1;

phi :=  all({intwe, we, L, optL, beta}, phi ) ;
psi := rlqe( phi );
%psi1 := second psi;
psi1 := psi;
psi2 := rlqepcad( rlex(psi1), "adaptive-final.qepcad" );
%psi2 := rlqepcad( psi );
%psi3 := rlqepcad( rlex(psi2), "adaptive2-final.qepcad" );
off nat;	% Output same syntax as input (for reduce)
out "adaptive-final.out";
psi;
%psi3;
shut "adaptive-final.out";
end;