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