%% The infintely many (zero-symmetric) extremal NS of type [-x3,0,x3]
%% (except for x3=1).
%%
%% polys
%%
   -8x^2+9x3^2
%%
%% input formula QEPCAD
%% 
   (Ax)[[0<x3 /\ x3<1]/\[[x3<x /\ x<=1] ==>-8x^2+9x3^2>=0]].
%%
%% input formula MMA
%%
   0<x3<1\[And]ForAll[x,x3<x<=1\[Implies]-8x^2+9x3^2>=0]