Q E P C A D - A Problem Due to Anai

This example problem comes from a paper by H. Anai in the on-line proceedings of IMACS-ACA 1998 (H. Anai, Solving LMI and BMI problems by quantifier elimination, Proc. of IMACS-ACA '98, Edited by R. Liska, http://www-troja.fjfi.cvut.cz/aca98/proceedings.html). In the last problem from that paper, he ends up with the following formula describing the solution to his problem:
```[
[s z  + s - 1 >= 0 /\ s = 0 /\  z  + 1 >= 0]
\/ [s z  + s >= 0 /\ s = 0 /\  z  = 0] \/
[s^2  + 4 s z  >= 0 /\ [[
s^2  - 2 s <= 0 /\ s z  + s - 1 <= 0 /\ s = 0 /\ [
s^2  + 3 s z  - s - 2 z  <= 0
\/ [s +  z  - 1 <= 0 /\ [s z  + s - 1 = 0 \/
z  = 0]]] /\ [s + 2 z  >= 0 \/  z  = 0]] \/
[s^2  - 2 s <= 0 /\ s + 2 z  >= 0 /\ s = 0 /\ [
[s^2  + 3 s z  - s - 2 z  <= 0 /\ [s z  + s - 1 <= 0
\/ z  = 0]] \/ [s +  z  - 1 >= 0 /\
[s z  + s - 1 >= 0 \/  z  = 0]]]]]] \/
[s = 0 /\  z  >= 0]
].
```
This formula is already quantifier-free, but we might try using QEPCAD anyway to see if it can simplify the formula. In this case, it simplifies it to `s = 0 /\ z >= 0`. Here's what the QEPCAD session looks like:
```=======================================================
Quantifier Elimination
in
Elementary Algebra and Geometry
by
Partial Cylindrical Algebraic Decomposition

Version B 0.1, 30 Jul 2002

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 Robiduex, and Stanly Steinberg
=======================================================
Enter an informal description  between '[' and ']':
[ Anai's Problem ]
Enter a variable list:
(s,z)
Enter the number of free variables:
2
Enter a prenex formula:
[
[s z  + s - 1 >= 0 /\ s = 0 /\  z  + 1 >= 0]
\/ [s z  + s >= 0 /\ s = 0 /\  z  = 0] \/
[s^2  + 4 s z  >= 0 /\ [[
s^2  - 2 s <= 0 /\ s z  + s - 1 <= 0 /\ s = 0 /\ [
s^2  + 3 s z  - s - 2 z  <= 0
\/ [s +  z  - 1 <= 0 /\ [s z  + s - 1 = 0 \/
z  = 0]]] /\ [s + 2 z  >= 0 \/  z  = 0]] \/
[s^2  - 2 s <= 0 /\ s + 2 z  >= 0 /\ s = 0 /\ [
[s^2  + 3 s z  - s - 2 z  <= 0 /\ [s z  + s - 1 <= 0
\/ z  = 0]] \/ [s +  z  - 1 >= 0 /\
[s z  + s - 1 >= 0 \/  z  = 0]]]]]] \/
[s = 0 /\  z  >= 0]
].

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

Before Normalization >
finish
An equivalent quantifier-free formula:

s = 0 /\ z >= 0

==========================================
```

Christopher W Brown