%% The best constants/formulae which belongs to the unit square @var=3
%%
%% (1)  (u0,v0)=(u0,0)  (1,v1) (u2,1)
%%
%% input formula QEPCAD
%% 
   (Ex1)(Ex2)(Ex3)[ L>1 /\  0 <= x1 /\ x1<= 1 /\ 0 <= x2  /\ x2<= 1 /\ 0 <= x3 /\ x3<= 1 /\ 
  /\ 1-x1+x1 x2-x2 x3>0 /\ 1+x1+x1 x2-x2 x3<=L (1-x1+x1 x2-x2 x3) /\ 1-x1+2 x2-x1 x2-x2 x3<=L (1-x1+x1 x2-x2 x3) /\ 1-x1+x1 x2+2 x3-x2 x3<=L (1-x1+x1 x2-x2 x3) /\ 3-x1-2 x2+x1 x2-2 x3+x2 x3<=L (1-x1+x1 x2-x2 x3)]
%%
   (EL)(Ex1)(Ex2)(Ex3)[ L>1 /\ 5L^2-10L+1<0 /\ 0 <= x1 /\ x1<= 1 /\ 0 <= x2  /\ x2<= 1 /\ 0 <= x3 /\ x3<= 1 /\ 
  /\ 1-x1+x1 x2-x2 x3>0 /\ 1+x1+x1 x2-x2 x3<=L (1-x1+x1 x2-x2 x3) /\ 1-x1+2 x2-x1 x2-x2 x3<=L (1-x1+x1 x2-x2 x3) /\ 1-x1+x1 x2+2 x3-x2 x3<=L (1-x1+x1 x2-x2 x3) /\ 3-x1-2 x2+x1 x2-2 x3+x2 x3<=L (1-x1+x1 x2-x2 x3) ]
%%

%% input formula MMA
%%
   
   Exists[{x1,x2,x3}, L > 1 \[And] 0 <= x1 <= 1 \[And] 0 <= x2 <= 1 \[And] 0 <= x3 <= 1 \[And] 
  1-x1+x1 x2-x2 x3>0 \[And] 1+x1+x1 x2-x2 x3<=L (1-x1+x1 x2-x2 x3) \[And] 1-x1+2 x2-x1 x2-x2 x3<=L (1-x1+x1 x2-x2 x3) \[And] 1-x1+x1 x2+2 x3-x2 x3<=L (1-x1+x1 x2-x2 x3) \[And] 3-x1-2 x2+x1 x2-2 x3+x2 x3<=L (1-x1+x1 x2-x2 x3)]
   
%%
   Exists[{L,x1,x2,x3},L>1 \[And] 5L^2-10L+1<0 
   \[And] 0 <= x1 <= 1 \[And] 0 <= x2 <= 1 \[And] 0 <= x3 <= 1 \[And] 
  1-x1+x1 x2-x2 x3>0 \[And] 1+x1+x1 x2-x2 x3<=L (1-x1+x1 x2-x2 x3) \[And] 1-x1+2 x2-x1 x2-x2 x3<=L (1-x1+x1 x2-x2 x3) \[And] 1-x1+x1 x2+2 x3-x2 x3<=L (1-x1+x1 x2-x2 x3) \[And] 3-x1-2 x2+x1 x2-2 x3+x2 x3<=L (1-x1+x1 x2-x2 x3)]
  
   

%%
%% input formula for pari/gp

tst12([ex,ex,ex],[l,x1,x2,x3],(f1,f2,f3,f4,f5,f6,f7,f8,f9,f10,f11,f12,f13)->(f1*f2*f3*f4*f5*f6*f7*f8*f9*f10*f11*f12*f13),"l>1,l<2, 0<=x1, x1<=1, 0<=x2, x2<=1, 0<=x3, x3<=1,1 - x1 + x1*x2 - x2*x3 > 0 , 1 + x1 + x1*x2 - x2*x3 <= l*(1 - x1 + x1*x2 - x2*x3) , 1 - x1 + 2*x2 - x1*x2 - x2*x3 <= l*(1 - x1 + x1*x2 - x2*x3) ,1 - x1 + x1*x2 + 2*x3 - x2*x3 <= l*(1 - x1 + x1*x2 - x2*x3) , 3 - x1 - 2*x2 + x1*x2 - 2*x3 + x2*x3 <= l*(1 - x1 + x1*x2 - x2*x3) ",1)

tst12([ex,ex,ex,ex],[l,x1,x2,x3],(f1,f2,f3,f4,f5,f6,f7,f8,f9,f10,f11,f12,f13)->(f1*f2*f3*f4*f5*f6*f7*f8*f9*f10*f11*f12*f13),"l>1,5*l^2-10*l+1<0, 0<=x1, x1<=1, 0<=x2, x2<=1,0<=x3, x3<=1,1 - x1 + x1*x2 - x2*x3 > 0 , 1 + x1 + x1*x2 - x2*x3 <= l*(1 - x1 + x1*x2 - x2*x3) , 1 - x1 + 2*x2 - x1*x2 - x2*x3 <= l*(1 - x1 + x1*x2 - x2*x3) ,1 - x1 + x1*x2 + 2*x3 - x2*x3 <= l*(1 - x1 + x1*x2 - x2*x3) , 3 - x1 - 2*x2 + x1*x2 - 2*x3 + x2*x3 <= l*(1 - x1 + x1*x2 - x2*x3) ",1)



%% input formula INTLAB
%%
 
f03b=@(x) max(max(max((1+x(1,:)+x(1,:).*x(2,:)-x(2,:).*x(3,:))./abs(1-x(1,:)+x(1,:).*x(2,:)-x(2,:).*x(3,:)),(1-x(1,:)+2*x(2,:)-x(1,:).*x(2,:)-x(2,:).*x(3,:))./abs(1-x(1,:)+x(1,:).*x(2,:)-x(2,:).*x(3,:))),(1-x(1,:)+2*x(3,:)-x(1,:).*x(2,:)-x(2,:).*x(3,:))./abs(1-x(1,:)+x(1,:).*x(2,:)-x(2,:).*x(3,:))),  (3-x(1,:)-2*x(3,:)-2*x(2,:)+x(1,:).*x(2,:)+x(2,:).*x(3,:))./abs(1-x(1,:)+x(1,:).*x(2,:)-x(2,:).*x(3,:)))



[mu,L,Ls]=verifyglobalmin(f03b,infsup(0,1)*ones(3,1))


%%OUTPUTS:

L - 1 > 0 /\ 5 L^2 - 10 L + 1 >= 0

Counts for Projection Phase:

parisize = 8000000, primelimit = 500000
tst12, 08/06/2021 17:43:16
? default(parisize, 480000000)
  ***   Warning: new stack size = 480000000 (457.764 Mbytes).
? tst12([ex,ex,ex],[l,x1,x2,x3],(f1,f2,f3,f4,f5,f6,f7,f8,f9,f10,f11,f12,f13)->(f1*f2*f3*f4*f5*f6*f7*f8*f9*f10*f11*f12*f13),"l>1,l<2, 0<=x1, x1<=1, 0<=x2, x2<=1, 0<=x3, x3<=1,1 - x1 + x1*x2 - x2*x3 > 0 , 1 + x1 + x1*x2 - x2*x3 <= l*(1 - x1 + x1*x2 - x2*x3) , 1 - x1 + 2*x2 - x1*x2 - x2*x3 <= l*(1 - x1 + x1*x2 - x2*x3) ,1 - x1 + x1*x2 + 2*x3 - x2*x3 <= l*(1 - x1 + x1*x2 - x2*x3) , 3 - x1 - 2*x2 + x1*x2 - 2*x3 + x2*x3 <= l*(1 - x1 + x1*x2 - x2*x3) ",1)
 *** using Lazard's method (MPP17).
[x3,7]
[x2,16]
[x1,59]
[l,716]
proj = 17,013 ms.
441 50139(4,521) 1076843(1764,62669) 214(0,545568) 
 *** combined adjacent 213 cells.
time = 29min, 17,278 ms.
%1 = [[[[p12, 2]~, [p2, 1]], [-oo, +oo], [-oo, +oo], [-oo, +oo]]]
? Ans();
1[[5*l^2 - 10*l + 1, 2] <= l < [l - 2, 1],true,true,true]