todai-2021-1.txt

[todai-2021-1]
(a,b,x1,x2)
2
(X1 x1)(X1 x2)[
    [x1^2 + a x1 + b = -x1^2 /\ -1 < x1 /\ x1 < 0] /\
    [x2^2 + a x2 + b = -x2^2 /\ 0 < x2 /\ x2 < 1]
].
finish

出力.txt

$ bin/qepcadd <todai-2021-1.txt 
=======================================================
                Quantifier Elimination                 
                          in                           
            Elementary Algebra and Geometry            
                          by                           
      Partial Cylindrical Algebraic Decomposition      
                                                       
               Version B 1.69, 16 Mar 2012
                                                       
                          by                           
                       Hoon Hong                       
                  ([email protected])                
                                                       
With contributions by: Christopher W. Brown, George E. 
Collins, Mark J. Encarnacion, Jeremy R. Johnson        
Werner Krandick, Richard Liska, Scott McCallum,        
Nicolas Robidoux, and Stanly Steinberg                 
=======================================================
Enter an informal description  between '[' and ']':
[todai-2021-1]Enter a variable list:
(a,b,x1,x2)Enter the number of free variables:
2
Enter a prenex formula:
(X1 x1)(X1 x2)[
    [x1^2 + a x1 + b = -x1^2 /\ -1 < x1 /\ x1 < 0] /\
    [x2^2 + a x2 + b = -x2^2 /\ 0 < x2 /\ x2 < 1]
].

=======================================================

Before Normalization >
finish

An equivalent quantifier-free formula:

b < 0 /\ b + a + 2 > 0 /\ b - a + 2 > 0


=====================  The End  =======================

-----------------------------------------------------------------------------
0 Garbage collections, 0 Cells and 0 Arrays reclaimed, in 0 milliseconds.
350606 Cells in AVAIL, 500000 Cells in SPACE.

System time: 20 milliseconds.
System time after the initialization: 15 milliseconds.
-----------------------------------------------------------------------------