todai-2023-3-1.txt

[todai-2023-3-1]
(a,x,y)
1
(A x)(A y)[
    [x^2 + (y-a)^2 = 1] ==> [y > x^2]
].
finish

出力.txt

$ time docker run --rm --platform linux/amd64 -i kobae964/qepcad +N10000000 <todai-2023-3-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-2023-3-1]Enter a variable list:
(a,x,y)Enter the number of free variables:
1
Enter a prenex formula:
(A x)(A y)[
    [x^2 + (y-a)^2 = 1] ==> [y > x^2]
].

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

Before Normalization >
finish

An equivalent quantifier-free formula:

4 a - 5 > 0


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

-----------------------------------------------------------------------------
0 Garbage collections, 0 Cells and 0 Arrays reclaimed, in 0 milliseconds.
4962190 Cells in AVAIL, 5000000 Cells in SPACE.

System time: 59 milliseconds.
System time after the initialization: 47 milliseconds.
-----------------------------------------------------------------------------
docker run --rm --platform linux/amd64 -i kobae964/qepcad +N10000000 <   0.03s user 0.05s system 3% cpu 2.478 total