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