https://github.com/koba-e964/qepcad-image を使う。

todai-2012-1_0.txt

[todai-2012-1_0]
(L,t,s,s23,q)
1
(E t)(X1 s)(X1 s23)(X1 q)[
    [s^2 = t^2 + 1] /\ [s >= 0] /\
    [9 s23^2 = 2] /\ [s23 > 0] /\
    [q (1 + t^2) = 2 t] /\
    [L = (q - s23) s]
].
finish

todai-2012-1_1.txt

[todai-2012-1_1]
(t,L,s,s23,q)
1
(E L)(X1 s)(X1 s23)(X1 q)[
    [s^2 = t^2 + 1] /\ [s >= 0] /\
    [9 s23^2 = 2] /\ [s23 > 0] /\
    [q (1 + t^2) = 2 t] /\
    [L = (q - s23) s] /\
    [3 L^2 = 2] /\ [L > 0]
].
finish

出力_0.txt

$ time docker run --rm --platform linux/amd64 -i qepcad +N10000000 <todai-2012-1_0.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 ']':
[todai-2012-1_0]Enter a variable list:
(L,t,s,s23,q)Enter the number of free variables:
1
Enter a prenex formula:
(E t)(X1 s)(X1 s23)(X1 q)[
    [s^2 = t^2 + 1] /\ [s >= 0] /\
    [9 s23^2 = 2] /\ [s23 > 0] /\
    [q (1 + t^2) = 2 t] /\
    [L = (q - s23) s]
].

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

Before Normalization >
finish

An equivalent quantifier-free formula:

3 L^2 - 2 <= 0 \/ L < 0


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

-----------------------------------------------------------------------------
253 Garbage collections, 1149728916 Cells and 1759 Arrays reclaimed, in 9463 milliseconds.
1007427 Cells in AVAIL, 5000000 Cells in SPACE.

System time: 47507 milliseconds.
System time after the initialization: 47487 milliseconds.
-----------------------------------------------------------------------------
docker run --rm --platform linux/amd64 -i qepcad +N10000000 <   0.04s user 0.07s system 0% cpu 49.353 total

出力_1.txt

$ time docker run --rm --platform linux/amd64 -i qepcad +N10000000 <todai-2012-1_1.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 ']':
[todai-2012-1_1]Enter a variable list:
(t,L,s,s23,q)Enter the number of free variables:
1
Enter a prenex formula:
(E L)(X1 s)(X1 s23)(X1 q)[
    [s^2 = t^2 + 1] /\ [s >= 0] /\
    [9 s23^2 = 2] /\ [s23 > 0] /\
    [q (1 + t^2) = 2 t] /\
    [L = (q - s23) s] /\
    [3 L^2 = 2] /\ [L > 0]
].

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

Before Normalization >
finish

An equivalent quantifier-free formula:

t > 0 /\ t^2 - 2 = 0


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

-----------------------------------------------------------------------------
1 Garbage collections, 4950904 Cells and 159 Arrays reclaimed, in 30 milliseconds.
4446183 Cells in AVAIL, 5000000 Cells in SPACE.

System time: 270 milliseconds.
System time after the initialization: 257 milliseconds.
-----------------------------------------------------------------------------
docker run --rm --platform linux/amd64 -i qepcad +N10000000 <   0.03s user 0.05s system 8% cpu 0.951 total