%% The LC which belongs to the CNS [-1,-x3,x3,1] is Root[43m^3-93m^2+53m-11,1]~1.42292.
%%
%% polys
%%
   -m x3^2-x3^2+2x^2+m-1
   -m x3^3+x3^3-x^2 x3+m x3+x^3-x
%%
%% input formula QEPCAD
%% 
   (Ex3)(Ax)[[0<x3 /\ x3<1] /\
   [[[-x3<x /\ x<x3] ==> -m x3^2-x3^2+2x^2+m-1>=0] /\
   [[x3<x /\ x<=1] ==> -m x3^3+x3^3-x^2 x3+m x3+x^3-x>=0]]].
%%
t
%% input formula MMA
%%
   Exists[x3,(0<x3<1) \[And]
   ForAll[x,((-x3<x<x3) \[Implies] -m x3^2-x3^2+2x^2+m-1>=0) \[And]
            ((x3<x<=1)  \[Implies] -m x3^3+x3^3-x^2 x3+m x3+x^3-x>=0)]]