%% The optimal LC which belongs to the NS of type [-x3,0,x3] is m=5/4.
%%
%% polys
%%
   x^2+(-x3)x+(x3^2(m-1))
   -2x^2+(x3^2(m+1))
%%
%% input formula QEPCAD
%% 
   (Ex3)(Ax)[[0<x3 /\ x3<1]/\[[0<=x /\ x<x3] ==> x^2+(-x3)x+(x3^2(m-1))>=0] /\ [[x3<x /\ x<=1] ==> -2x^2+(x3^2(m+1))>=0]].
%%
%% input formula MMA
%%
   Exists[x3,0<x3<1\[And]ForAll[x,(0<=x<x3\[Implies]x^2+(-x3)x+(x3^2(m-1))>=0)\[And](x3<x<=1\[Implies]-2x^2+(x3^2(m+1))>=0)]]