kyodai-2021-2.txt

[kyodai-2021-2]
(l,t,s,dx,dy)
1
(E t)(E s)(E dx)(E dy)[
    [t s = 1] /\
    [2 dx = t + s] /\
    [2 dy = t^2 + 1] /\
    [l^2 = dx^2 + dy^2]
].
finish

出力.txt

$ bin/qepcadd <kyodai-2021-2.txt 
=======================================================
                Quantifier Elimination                 
                          in                           
            Elementary Algebra and Geometry            
                          by                           
      Partial Cylindrical Algebraic Decomposition      
                                                       
               Version B 1.69, 16 Mar 2012
                                                       
                          by                           
                       Hoon Hong                       
                  (hhong@math.ncsu.edu)                
                                                       
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 ']':
[kyodai-2021-2]Enter a variable list:
(l,t,s,dx,dy)Enter the number of free variables:
1
Enter a prenex formula:
(E t)(E s)(E dx)(E dy)[
    [t s = 1] /\
    [2 dx = t + s] /\
    [2 dy = t^2 + 1] /\
    [l^2 = dx^2 + dy^2]
].

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

Before Normalization >
finish

An equivalent quantifier-free formula:

16 l^2 - 27 >= 0


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

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

System time: 51 milliseconds.
System time after the initialization: 46 milliseconds.
-----------------------------------------------------------------------------