Skip to content

Instantly share code, notes, and snippets.

@koba-e964
Created March 10, 2021 06:25
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save koba-e964/84372990b9d00b9ca5342e05f0c0ef34 to your computer and use it in GitHub Desktop.
Save koba-e964/84372990b9d00b9ca5342e05f0c0ef34 to your computer and use it in GitHub Desktop.
[todai-2021-3]
(x)
1
[
8 x = (x + 1) (x^2 + 3) /\
x /= 1
].
finish
$ bin/qepcadd <todai-2021-3.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-2021-3]Enter a variable list:
(x)Enter the number of free variables:
1
Enter a prenex formula:
[
8 x = (x + 1) (x^2 + 3) /\
x /= 1
].
=======================================================
Before Normalization >
finish
An equivalent quantifier-free formula:
x + 3 = 0
===================== The End =======================
-----------------------------------------------------------------------------
0 Garbage collections, 0 Cells and 0 Arrays reclaimed, in 0 milliseconds.
491841 Cells in AVAIL, 500000 Cells in SPACE.
System time: 9 milliseconds.
System time after the initialization: 5 milliseconds.
-----------------------------------------------------------------------------
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment