#===================================================
#
#  Examples for CAD - QEPCAD file
#   Each example is given with their inputs for
#   QEPCAD for easy copy/pasting
#
#  Version 4.0 - 1/4/13
#===================================================

#===================================================
# CMXY09 Examples
# Examples sourced from "Computing Cylindrical Alg-
# -ebraic Decomposition via Triangular Decomposition"

#1: Parametric Parabola
[Parametric Parabola]
(a,b,c,x)
3
(E x)[a x^2 + b x + c = 0].

#2: Whitney Umbrella
[Whitney Umbrella]
(x,y,z,u,v)
3
(E u)(E v)[[x - u v = 0] /\ [y - v = 0] /\ [z - u^2 = 0]].

#3: Quartic
[Positivity of Quartic] 
(r,q,p,x)
3
(A x)[x^4 + p x^2 + q x + r >= 0].

#4: Sphere and Catastrophe
[Sphere and Catastrophe]
(z,y,x)
3
[[z^2 + y^2 + x^2 - 1 = 0] /\ [z^3 + x z + y = 0]].

#5: Arnon-84
[Arnon-84]
(x,y)
2
[y^4 - 2 y^3 + y^2 - 3 x^2 y + 2 x^4 = 0].

#6: Arnon-84-2
[Arnon-84-2]
(x,y)
2
[[144 y^2 + 96 x^2 y + 9 x^4 + 105 x^2 + 70 x - 98 = 0] /\ [x y^2 + 6 x y + x^3 + 9 x = 0]].

#7: A Real Implicitization Problem
[A Real Implicitization Problem]
(x,y,z,u,v)
3
(E u)(E v)[[x - u v = 0] /\ [y - u v^2 = 0] /\ [z - u^2 = 0]].

#8: Ball and Circular Cylinder
[Ball and Circular Cylinder]
(x,y,z)
0
(E z)(E x)(E y)[[x^2 + y^2 + z^2 - 1 < 0] /\ [x^2 + (y + z - 2)^2 - 1 < 0]].

#9: Termination of Term Rewrite System
[Term Rewrite]
(r,x,y)
0
(E r)(A x)(A y)[[[x - r > 0] /\ [y - r > 0]] ==> [x^2 (1 + 2 y)^2 - y^2 (1 + 2 x^2) > 0]].

#10: Collins and Johnson
[Collins and Johnson]
(b,a,r)
2
(E r)[[3 a^2 r + 3 b^2 - 2 a r - a^2 - b^2 < 0] /\ [3 a^2 r + 3 b^2 r - 4 a r + r - 2 a^2 - 2 b^2 + 2 a > 0] /\ [2 a - 1 >= 0] /\ [b > 0] /\ [r > 0] /\ [r - 1 < 0]].

#11: Range of Lower Bounds
[Range of Lower Bounds]
(y,x,a,b,c,z)
1
(A x)(A a)(A b)(A c)(E z)[[[a > 0] /\ [a z^2 + b z + c /= 0]] ==> [y < a x^2 + b x + c]].

#12: X-axis Ellipse Problem
[X-axis Ellipse Problem]
(a,c,b,x,y)
3
(A x)(A y)[[a b /= 0] /\ [[b^2 (x - c)^2 + a^2 y^2 - a^2 b^2 = 0]==>[x^2 + y^2 - 1 <= 0]]].

#13: Davenport and Heintz
[Davenport and Heintz]
(d,c,b,a)
1
(E c)(A b)(A a)[[[[a - d = 0] /\ [b - c = 0]] \/ [[a - c = 0] /\ [b - 1 = 0]]] ==> [a^2 - b = 0]].

#14: Hong-90
[Hong-90]
(r,s,t,a,b)
3
(E a)(E b)[[r + s + t = 0] /\ [r s + s t + t r - a = 0] /\ [r s t - b = 0]].

#15: Solotareff-3
[Solotareff-3]
(a,r,b,u,v)
3
(E u)(E v)[[r > 1] /\ [u + 1 > 0] /\ [u - v < 0] /\ [v - 1 < 0] /\ [3 u^2 + 2 r u - a = 0] /\ [3 v^2 + 2 r v - a = 0] /\ [u^3 + r u^2 - a u + a - r - 1 = 0] /\ [v^3 +r v^2 - a v - 2 b - a + r + 1 = 0]].

#16: Collision Problem
[Collision of Circle and Square]
(y,x,t)
0
(E y)(E x)(E t)[[17 t - 96 >= 0] /\ [17 t - 160 <= 0] /\ [16 x - 17 t + 16 >= 0] /\ [16 x - 17 t - 16 <= 0] /\ [16 y - 17 t + 144 >= 0] /\ [16 y - 17 t + 112 <= 0] /\ [(x - t)^2 + y^2 - 1 <= 0]].

#17: McCallum Trivariate Random Polynomial
[McCallum Trivariate Random Polynomial]
(x,y,z)
0
(E x)(E y)(E z)[(y - 1) z^4 + x z^3 + x (1 - y) z^2 + (y - x - 1) z + y = 0].

#18: Ellipse Problem
[Ellipse Problem]
(a,b,c,d,x,y)
4
(A x)(A y)[[a b /= 0] /\ [[b^2 (x - c)^2 + a^2 (y - d)^2 - a^2 b^2 = 0] ==> [x^2 + y^2 - 1 <= 0]]].


#===================================================
# Branch Cut Examples
# Examples from using CAD to deal with branch cuts

#1: Kahan A
[Kahan A]
(x,y)
2
[[[4 y (2 y^2 x + 2 x^3 + 5 y^2 + 21 x^2 + 72 x + 81) = 0] /\ [ -225 x^2 - 324 x + 63 y^2 - 4 x^4 - 52 x^3 + 12 y^2 x + 4 y^4 < 0]] \/ [[2 y = 0] /\ [2 x + 9 < 0]] \/ [[8 y = 0] /\ [8 x^2 + 56 x + 8 y^2 + 96 < 0]] \/ [[y = 0] /\ [x^2 + 7 x + y^2 + 12 < 0]] \/ [[4 y (2 y^2 x + 2 x^3 + 5 y^2 + 21 x^2 + 72 x + 81) = 0] /\ [ -4 x^4 - 52 x^3 - 252 x^2 + 12 y^2 x - 540 x + 36 y^2 + 4 y^4 - 432 <= 0] /\ [4 x^4 + 52 x^3 + 225 x^2 - 12 y^2 x + 324 x - 63 y^2 - 4 y^4 < 0]] \/ [[2 y = 0] /\ [ -2 x - 6 < 0] /\ [ 2 x <= 0]] \/ [[8 y = 0] /\ [ -8 x^2 - 56 x - 8 y^2 - 96 < 0] /\ [2 x^2 + 8 x + 2 y^2 <= 0]]].

#2: Kahan B
[Kahan B]
(y,x)
2
[[[4 y (2 y^2 x + 2 x^3 + 5 y^2 + 21 x^2 + 72 x + 81) = 0] /\ [ -225 x^2 - 324 x + 63 y^2 - 4 x^4 - 52 x^3 + 12 y^2 x + 4 y^4 < 0]] \/ [[2 y = 0] /\ [2 x + 9 < 0]] \/ [[8 y = 0] /\ [8 x^2 + 56 x + 8 y^2 + 96 < 0]] \/ [[y = 0] /\ [x^2 + 7 x + y^2 + 12 < 0]] \/ [[4 y (2 y^2 x + 2 x^3 + 5 y^2 + 21 x^2 + 72 x + 81) = 0] /\ [ -4 x^4 - 52 x^3 - 252 x^2 + 12 y^2 x - 540 x + 36 y^2 + 4 y^4 - 432 <= 0] /\ [4 x^4 + 52 x^3 + 225 x^2 - 12 y^2 x + 324 x - 63 y^2 - 4 y^4 < 0]] \/ [[2 y = 0] /\ [ -2 x - 6 < 0] /\ [ 2 x <= 0]] \/ [[8 y = 0] /\ [ -8 x^2 - 56 x - 8 y^2 - 96 < 0] /\ [2 x^2 + 8 x + 2 y^2 <= 0]]].

#3: ArcSin A
[ArcSin A]
(x,y)
2
[[-2 x y = 0 /\ -x^2 + y^2 < -1] \/ [-8 x y (2 x^2 - 2 y^2 - 1) = 0 /\ 4 x^2 - 4 y^2 - 4 x^4 + 24 x^2 y^2 - 4 y^4 >= 1] \/ [y = 0 /\ 1 <= x] \/ [y = 0 /\ x <= -1]].

#4: ArcSin B
[ArcSin B]
(y,x)
2
[[-2 x y = 0 /\ -x^2 + y^2 < -1] \/ [-8 x y (2 x^2 - 2 y^2 - 1) = 0 /\ 4 x^2 - 4 y^2 - 4 x^4 + 24 x^2 y^2 - 4 y^4 >= 1] \/ [y = 0 /\ 1 <= x] \/ [y = 0 /\ x <= -1]].

#===================================================
# Motion Planning Examples
# Examples from using CAD to solve problems in robot
# motion planning

#1: Piano Mover's Problem (Davenport)
[Piano Mover's Problem (Davenport)]
(b,a,y,x)
2
(E y)(E x)[[(x - a)^2 + (y - b)^2 - 9 = 0] /\ [[y b >= 0] \/ [x (y - b)^2 + y (a - x) (y - b) >= 0]] /\ [[(y - 1) (b - 1) >= 0] \/ [(x + 1) (y - b)^2 + (y - 1) (a - x) (y - b) >= 0]] /\ [[x a >= 0] \/ [y (x - a)^2 + x (b - y) (x - a) >= 0]] /\ [[(x + 1) (a + 1) >= 0] \/ [(y - 1)(x - a)^2 + (x + 1) (b - y) (x - a) >= 0]]].


#===================================================
# Buchberger-Hong Examples
# Examples from Buchberger and Hong's 1991 paper

#1: Intersection A
[Intersection A from Buchberger-Hong]
(x,y,z)
2
(E z)[[x^2 - 1/2 y^2 - 1/2 z^2 = 0] /\ [x z + z y - 2 x = 0] /\ [ z^2 - y = 0]].

#2: Intersection A Grobner
[Intersection A Grobner from Buchberger-Hong]
(x,y,z)
2
(E z)[[x^5 + 18 x^4 - 21 x^3 + 4 x^2 - 2 x = 0] /\ [y + 5/19 x^4 + 88/19 x^3 - 144/19 x^2 + 32/19 x = 0] /\ [z x - 7/38 x^4 - 127/38 x^3 + 59/19 x^2 - 11/19 x = 0] /\ [z^2 + 5/19 x^4 + 88/19 x^3 - 144/19 x^2 + 32/19 x = 0]].

#3: Intersection B
[Intersection B from Buchberger-Hong]
(y,x,z)
2 
(E z)[[x^2 - 1/2 y^2 - 1/2 z^2 = 0] /\ [x z + z y - 2 x = 0] /\ [ z^2 - y = 0]].

#4: Intersection B Grobner 
[Intersection B Grobner from Buchberger-Hong]
(y,x,z)
2
(E z)[[y^5 - 26 y^4 - 15 y^3 + 24 y^2 + 16 y = 0] /\ [x - 3/64 y^4 + 41/32 y^3 - 59/64 y^2 - 21/16 y = 0] /\ [z y - 1/8 y^4 + 27/8 y^3 - 5/4 y^2 - 3 y = 0] /\ [z^2 - y = 0]].

#5: Random A
[Random A from Buchberger-Hong]
(x,y,z)
0
(E x)(A y)(E z)[[4 x^2 + x y^2 - z + 1/4 = 0] /\ [2 x + y^2 z + 1/2 = 0] /\ [x^2 z - 1/2 x - y^2 = 0 ]].

#6: Random A Grobner
[Random A Grobner from Buchberger-Hong]
(x,y,z)
0
(E x)(A y)(E z)[[x^7 + 29/4 x^6 - 17/16 x^4 - 11/8 x^3 + 1/32 x^2 + 15/16 x + 14 = 0] /\ [y^2 + 112/2745 x^6 - 84/305 x^5 - 1264/305 x^4 - 13/549 x^3 + 84/305 x^2 + 1772/2745 x + 2/2745 = 0] /\ [z - 1568/2745 x^6 - 1264/305 x^5 + 6/305 x^4 + 182/549 x^3 - 2047/610 x^2 - 103/2745 x - 2857/10980]].

#7: Random B
[Random B from Buchberger-Hong]
(z,y,x)
0
(E z)(A y)(E x)[[4 x^2 + x y^2 - z + 1/4 = 0] /\ [2 x + y^2 z + 1/2 = 0] /\ [x^2 z - 1/2 x - y^2 = 0 ]].

#8: Random B Grobner
[Random B Grobner from Buchberger-Hong]
(z,y,x)
0
(E z)(A y)(E x)[[z^7 - 1/2 z^6 + 1/16 z^5 + 13/4 z^4 + 75/16 z^3 - 171/8 z^2 + 133/8 z - 15/4 = 0] /\ [y^2 - 19188/497 z^6 + 318/497 z^5 - 4197/1988 z^4 - 251555/1988 z^3 - 481837/1988 z^2 + 1407741/1988 z - 297833/994 = 0] /\ [x + 4638/497 z^6 - 75/497 z^5 + 2111/3976 z^4 + 61031/1988 z^3 + 232833/3976 z^2 - 85042/497 z + 144407/1988 = 0]].

#9: Ellipse A
[Ellipse A from Buchberger-Hong]
(a,b,c,x,y)
3
(E x)(E y)[[x^2 + y^2 - 1 = 0] /\ [b^2 (x - c)^2 + a^2 y^2 - a^2 b^2 = 0] /\ [a > 0] /\ [a < 1] /\ [b > 0] /\ [b < 1] /\ [c >= 0] /\ [c < 1]].

#10: Ellipse A Grobner
[Ellipse A Grobner from Buchberger-Hong]
(a,b,c,x,y)
3
(E x)(E y)[[x^2 b^2 - x^2 a^2 - 2 x c b^2 + c^2 b^2 - b^2 a^2 + a^2 = 0] /\ [y^2 + x^2 -1 = 0] /\ [a > 0] /\ [a < 1] /\ [b > 0] /\ [b < 1] /\ [c >= 0] /\ [c < 1]].

#11: Ellipse B
[Ellipse B from Buchberger-Hong]
(a,b,c,y,x)
3
(E y)(E x)[[x^2 + y^2 - 1 = 0] /\ [b^2 (x - c)^2 + a^2 y^2 - a^2 b^2 = 0] /\ [a > 0] /\ [a < 1] /\ [b > 0] /\ [b < 1] /\ [c >= 0] /\ [c < 1]].

#12: Ellipse B Grobner
[Ellipse B Grobner from Buchberger-Hong]
(a,b,c,y,x)
3
(E y)(E x)[[y^4 b^4 - 2 y^4 b^2 a^2 + y^4 a^4 + 2 y^2 c^2 b^4 + 2 y^2 c^2 b^2 a^2 + 2 y^2 b^4 a^2 - 2 y^2 b^4 - 2 y^2 b^2 a^4 + 2 y^2 b^2 a^2 + c^4 b^4 - 2 c^2 b^4 a^2 - 2 c^2 b^4 + b^4 a^4 - 2 b^4 a^2 + b^4 = 0] /\ [x y^2 c a^2 + 1/2 y^4 b^2 - 1/2 y^4 a^2 + y^2 c^2 b^2 + 1/2 y^2 c^2 a^2 + y^2 b^2 a^2 - y^2 b^2 - 1/2 y^2 a^4 + 1/2 y^2 a^2 + 1/2 c^4 b^2 - c^2 b^2 a^2 - c^2 b^2 + 1/2 b^2 a^4 - b^2 a^2 + 1/2 b^2 = 0] /\ [x y^2 b^2 - x y^2 a^2 + x b^2 a^2 - x b^2 - 3/2 y^2 c b^2 - 1/2 y^2 c a^2 - 1/2 c^3 b^2 + 1/2 c b^2 a^2 + 3/2 c b^2 = 0] /\ [x c b^2 + 1/2 y^2 b^2 - 1/2 y^2 a^2 - 1/2 c^2 b^2 + 1/2 b^2 a^2 - 1/2 b^2 = 0] /\ [x^2 + y^2 - 1 = 0] /\ [a > 0] /\ [a < 1] /\ [b > 0] /\ [b < 1] /\ [c >= 0] /\ [c < 1]].

#13: Solotareff A
[Solotareff A from Buchberger-Hong]
(a,b,x,y)
2
(E x)(E y)[[3 x^2 - 2 x - a = 0] /\ [x^3 - x^2 - a x - 2 b + a - 2 = 0] /\ [3 y^2 - 2 y - a = 0] /\ [y^3 - y^2 - a y - a + 2 = 0] /\ [1 <= 4 a] /\ [4 a <= 7] /\ [-3 <= 4 b] /\ [4 b <= 3] /\ [-1 <= x] /\ [x <= 0] /\ [0 <= y] /\ [y <= 1]].

#14: Solotareff A Grobner
[Solotareff A Grobner from Buchberger-Hong]
(a,b,x,y)
2
(E x)(E y)[[a^3 - 11 a^2 + 35 a - 25 = 0] /\ [b^2 - 2/3 b a + 56/27 b - 1/3 a^2 + 16/27 a + 4/27 = 0] /\ [x + 81/1024 b a^2 - 459/512 b a + 3141/1024 b + 93/1024 a^2 - 527/512 a + 2241/1024 = 0] /\ [y - 3/32 a^2 + 17/16 a - 63/32 = 0] /\ [1 <= 4 a] /\ [4 a <= 7] /\ [-3 <= 4 b] /\ [4 b <= 3] /\ [-1 <= x] /\ [x <= 0] /\ [0 <= y] /\ [y <= 1]].

#15: Solotareff B
[Solotareff B from Buchberger-Hong]
(b,a,x,y)
2
(E x)(E y)[[3 x^2 - 2 x - a = 0] /\ [x^3 - x^2 - a x - 2 b + a - 2 = 0] /\ [3 y^2 - 2 y - a = 0] /\ [y^3 - y^2 - a y - a + 2 = 0] /\ [1 <= 4 a] /\ [4 a <= 7] /\ [-3 <= 4 b] /\ [4 b <= 3] /\ [-1 <= x] /\ [x <= 0] /\ [0 <= y] /\ [y <= 1]].

#16: Solotareff B Grobner
[Solotareff B Grobner from Buchberger-Hong]
(b,a,x,y)
2
(E x)(E y)[[b^6 - 10/9 b^5 - 2915/243 b^4 - 6724/19683 b^3 + 830093/19683 b^2 + 286982/6561 b + 24299/2187 = 0] /\ [a - 537286851/1733427200 b^5 + 1274021541/1733427200 b^4 + 2556627057/866713600 b^3 - 3694037643/866713600 b^2 - 3091197667/346685440 b - 6499394527/1733427200 = 0] /\ [x + 1227687759/27734835200 b^5 - 897078969/27734835200 b^4 - 8587423413/13867417600 b^3 - 1285658313/13867417600 b^2 + 16457320943/5546967040 b + 42073006043/27734835200 = 0] /\ [y + 2835001539/13867417600 b^5 - 7132522149/13867417600 b^4 - 12643778673/6933708800 b^3 + 19121535627/6933708800 b^2 + 15435163363/2773483520 b + 9745294303/13867417600 = 0] /\ [1 <= 4 a] /\ [4 a <= 7] /\ [-3 <= 4 b] /\ [4 b <= 3] /\ [-1 <= x] /\ [x <= 0] /\ [0 <= y] /\ [y <= 1]].

#17: Collision A
[Collision A from Buchberger-Hong]
(a,t,x,y)
1
(E t)(E x)(E y)[[1/4 (x - t)^2 + (y - 10)^2 - 1 = 0] /\ [1/4 (x - a t)^2 + (y - a t)^2 - 1 = 0] /\ [t > 0] /\ [a > 0]].

#18: Collision A Grobner
[Collision A Grobner from Buchberger-Hong]
(a,t,x,y)
1
(E t)(E x)(E y)[[x^2 t^2 a^2 - 2/5 x^2 t^2 a + 1/5 x^2 t^2 - 16 x^2 t a + 80 x^2 - x t^3 a^3 - 3/5 x t^3 a^2 + 1/5 x t^3 a - 1/5 x t^3 + 16 x t^2 a^2 + 16 x t^2 a - 80 x t a - 80 x t + 5/4 t^4 a^4 + 3/10 t^4 a^2 + 1/20 t^4 - 40 t^3 a^3 - 8 t^3 a + 2584/5 t^2 a^2 + 40 t^2 - 3136 t a + 7680 = 0] /\ [y x a - y x + 1/2 y t - 5 y a - 1/8 x^2 t a^2 + 1/20 x^2 t a - 1/40 x^2 t + x^2 a + 1/8 x t^2 a^3 + 3/40 x t^2 a^2 - 1/40 x t^2 a + 1/40 x t^2 - 11/8 x t a^2 - 5/8 x t a - 5 x a + 5 x - 5/32 t^3 a^4 - 3/80 t^3 a^2 - 1/160 t^3 + 55/16 t^2 a^3 + 5/16 t^2 a - 271/10 t a^2 - 5/2 t + 121 a = 0] /\ [y x t - 10 y x - 1/2 y t^2 + 50 y + 5/4 x^2 t a - 1/4 x^2 t - 10 x^2 - 5/4 x t^2 a^2 - 11/8 x t^2 a + 1/8 x t^2 + 55/4 x t a + 25/4 x t + 50 x + 25/16 t^3 a^3 + 11/16 t^3 a - 275/8 t^2 a^2 - 25/8 t^2 + 271 t a - 1210 = 0] /\ [y t a - 10 y + 1/4 x t a - 1/4 x t - 5/8 t^2 a^2 + 1/8 t^2 + 50 = 0] /\ [y^2 - 20 y + 1/4 x^2 - 1/2 x t + 1/4 t^2 + 99 = 0] /\ [t > 0] /\ [a > 0]].

#19: Collision B
[Collision B from Buchberger-Hong]
(a,y,x,t)
1
(E y)(E x)(E t)[[1/4 (x - t)^2 + (y - 10)^2 - 1 = 0] /\ [1/4 (x - a t)^2 + (y - a t)^2 - 1 = 0] /\ [t > 0] /\ [a > 0]].

#20: Collision B Grobner
[Collision B Grobner from Buchberger-Hong]
(a,y,x,t)
1
(E y)(E x)(E t)[[ x^4 a^4 - 4/5 x^4 a^3 + 14/25 x^4 a^2 - 4/25 x^4 a + 1/25 x^4 - 16/5 x^3 y a^3 + 32/15 x^3 y a^2 - 16/25 x^3 y a + 8 x^2 y^2 a^4 - 16/5 x^2 y^2 a^3 + 16/5 x^2 y^2 a^2 - 16/25 x^2 y^2 a + 8/25 x^2 y^2 - 160 x^2 y a^4 + 64 x^2 y a^3 + 96/5 x^2 y a^2 + 792 x^2 a^4 - 1584/5 x^2 a^3 - 2416/25 x^2 a^2 + 16/25 x^2 a - 8/25 x^2 - 64/5 x y^3 a^3 + 128/25 x y^3 a^2 - 64/25 x y^3 a + 256 x y^2 a^3 - 512/5 x y^2 a^2 - 6336/5 x y a^3 + 12672/25 x y a^2 + 64/25 x y a + 16 y^4 a^4 + 96/25 y^4 a^2 + 16/25 y^4 - 640 y^3 a^4 - 384/5 y^3 a^2 + 9568 y^2 a^4 + 9664/25 y^2 a^2 - 32/25 y^2 - 63360 y a^4 - 128 y a^2 + 156816 a^4 + 3168/5 a^2 + 16/25 = 0] /\ [t y^2 a^5 - 2/5 t y^2 a^4 + 2/25 t y^2 a^2 - 1/25 t y^2 a - 20 t y a^5 + 8 t y a^4 - 4/5 t y a^3 + 99 t a^5 - 198/5 t a^4 + 104/25 t a^3 - 2/25 t a^2 + 1/125 t a + 1/8 x^3 a^5 - 1/8 x^3 a^4 + 9/100 x^3 a^3 - 17/500 x^3 a^2 + 9/1000 x^3 a - 1/1000 x^3 - 3/10 x^2 y a^4 + 4/25 x^2 y a^3 - 7/125 x^2 y a^2 + 1/250 x^2 y + 1/2 x y^2 a^5 - 1/2 x y^2 a^4 + 9/25 x y^2 a^3 - 17/125 x y^2 a^2 + 9/250 x y^2 a - 1/250 x y^2 - 10 x y a^5 + 10 x y a^4 - 6/5 x y a^3 - 2/25 x y a^2 + 99/2 x a^5 - 99/2 x a^4 + 141/25 x a^3 + 67/125 x a^2 - 9/250 x a + 1/250 x - 6/5 y^3 a^4 + 16/25 y^3 a^3 - 28/125 y^3 a^2 + 2/125 y^3 + 24 y^2 a^4 - 64/5 y^2 a^3 + 72/25 y^2 a^2 - 594/5 y a^4 + 1584/25 y a^3 - 1772/125 y a^2 - 2/125 y = 0] /\ [t x y a - 125/4 t y^2 a^4 + 25/4 t y^2 a^3 + 5/4 t y^2 a^2 - 9/4 t y^2 a + 625 t y a^4 - 125 t y a^3 - 12375/4 t a^4 + 2475/4 t a^3 - 25/4 t a^2 + 5/4 t a - 125/32 x^3 a^4 + 25/8 x^3 a^3 - 35/16 x^3 a^2 + 5/8 x^3 a - 5/32 x^3 + 75/8 x^2 y a^3 - 25/8 x^2 y a^2 + 5/8 x^2 y a + 1/8 x^2 y - 125/8 x y^2 a^4 + 25/2 x y^2 a^3 - 35/4 x y^2 a^2 + 5/2 x y^2 a - 5/8 x Y62 + 625/2 x y a^4 - 250 x y a^3 - 25/2 x y a^2 - 12375/8 x a^4 + 2475/2 x a^3 + 285/4 x a^2 - 5/2 x a + 5/8 x + 75/2 y^3 a^3 - 25/2 y^3 a^2 + 5/2 y^3 a + 1/2 y^3 - 750 y^2 a^3 + 250 y^2 a^2 + 7425/2 y a^3 - 2475/2 y a^2 - 5/2 y a - 1/2 y = 0] /\ [t x^2 - 375/2 t y^2 a^4 + 25/2 t y^2 a^3 - 25/2 t y^2 a^2 - 25/2 t y^2 a + 4 t y^2 + 3750 t y a^4 - 250 t y a^3 + 400 t y a^2 - 37125/2 t a^4 + 2475/2 t a^3 - 4035/2 t a^2 + 5/2 t a - 4 t - 375/16 x^3 a^4 + 125/8 x^3 a^3 - 55/4 x^3 a^2 + 31/8 x^3 a - 37/16 x^3 + 225/4 x^2 y a^3 - 45/4 x^2 y a^2 + 47/4 x^2 y a + 5/4 x^2 y - 375/4 x y^2 a^4 + 125/2 x y^2 a^3 - 55 x y^2 a^2 + 31/2 x y^2 a - 37/4 x y^2 + 1875 x y a^4 - 1250 x y a^3 - 25 x y a^2 - 160 x y a - 37125/4 x a^4 + 12375/2 x a^3 + 180 x a^2 + 1569/2 x a + 37/4 x + 225 y^3 a^3 - 45 y^3 a^2 + 47 y^3 a + 5 y^3 - 4500 y^2 a^3 + 900 y^2 a^2 - 640 y^2 a + 22275 y a^3 - 4455 y a^2 + 3153 y a - 5 y = 0] /\ [ t x a^2 - 1/5 t x a - 4/5 t y a - 1/2 x^2 a^2 + 1/10 x^2 - 2 y^2 a^2 + 2/5 y^2 + 40 y a^2 - 198 a^2 - 2/5 = 0] /\ [t^2 - 2 t x + x^2 + 4 y^2 - 80 y + 396 = 0] /\ [t > 0] /\ [a > 0]].

#===================================================
# Other Examples

#1: Off-Center Ellipse
[Off-Center Ellipse]
(a,x,y)
1
(A x)(A y)[[a /= 0] /\ [[16 a^2 y^2 - 8 a^2 y + 4 x^2 - 4 x - 3 a^2 + 1 = 0] ==> [y^2 + x^2 - 1 <= 0]]].

#2: Concentric Circles
[Concentric Circles]
(x,y)
2
[[x^2 + y^2 - 9 = 0] \/ [x^2 + y^2 - 1 = 0]].

#3: Non-Concentric Circles
[Non-Concentric Circles]
(x,y)
2
[[x^2 + y^2 - 9 = 0] \/ [x^2 + (y - 1)^2 - 1 = 0]].

#4: Edges Square Product
[Edges Square Product]
(x,y,a,b,c)
2
(E a)(E b)(E c)[[x = a b - c] /\ [y = a c + x + 2] /\ [0 <= a] /\ [a <= 2] /\ [2 <= b] /\ [b <= 4] /\ [-1 <= c] /\ [c <= 1] /\ [-1 <= x] /\ [x <= 9] /\ [-6 <= y] /\ [y <= 6]].

#5: Simplified Edges Square Product
[Simplified Edges Square Product]
(x,y,a)
2
(E a)[[-a <= 0] /\ [a <= 2] /\ [0 <= 1 + x] /\ [x <= 9] /\ [0 <= y + 6] /\ [y <= 6] /\ [0 <= -(a^2 + 1) (-y - a x + 2 a^2 + 2)] /\ [((-x + a y) (a^2 + 1)) <= ((a^2 + 1)^2)] /\ [a^2 + 1 /= 0] /\ [0 <= (a^2 + 1) (a^2 + 1 - x + a y)] /\ [((a^2 + 1) (y + a x)) <= 4 (a^2 + 1)^2]].

#6: Putnum Example
[Putnum Example]
(x,y,a,b,c,d)
2
(E a)(E b)(E c)(E d)[[a^2 + b^2 - 1 = 0] /\ [(c - 10)^2 + d^2 - 9 = 0] /\ [2 x = a + c] /\ [2 y = b + d]].

#7: Simplified Putnum Example
[Simplified Putnum Example]
(x,y,a,d)
2
(E a)(E d)[[a^2 + 4 y^2 - 4 y d + d^2 - 1 = 0] /\ [4 x^2 - 4 x a - 40 x + a^2 + 20 a + 91 + d^2 = 0]].

#8: YangXia
[YangXia]
(a,h,R,s,b,c)
3
(E s)(E b)(E c)[[a^2 h^2 - 4 s (s - a) (s - b) (s - c) = 0] /\ [2 R h - b c = 0] /\ [2 s - a - b - c = 0] /\ [b > 0] /\ [c > 0] /\ [R > 0] /\ [h > 0] /\ [a + b - c > 0] /\ [b + c - a > 0] /\ [c + a - b > 0]].

#9: Simplified YangXia
[Simplified YangXia]
(R,h,a,b)
3
(E b)[[b /= 0] /\ [0 < R] /\ [0 < b] /\ [0 < h] /\ [4 a^2 h^2 b^4 - 2 a^2 b^6 - 8 a^2 R^2 h^2 b^2 - 8 R^2 h^2 b^4 + b^8 + a^4 b^4 + 16 R^4 h^4 = 0] /\ [0 < (a b + b^2 - 2 R h) b] /\ [0 < R h b] /\ [0 < (2 R h + a b - b^2) b] /\ [0 < (b^2 + 2 R h - a b) b]].

#10: SEIT Model
[SEIT Model]
(b,c,d,q,r,u,v,s,F,J,T)
7
(E s)(E F)(E J)(E T)[[d - d s - b J s = 0] /\ [v F - (d + u) J = 0] /\ [b J + c J T - (d + v + r) F + (1 - q) u J = 0] /\ [-d T + r F + q u J - b^2 T J = 0] /\ [F > 0] /\ [J > 0] /\ [T > 0] /\ [s > 0] /\ [b > 0] /\ [d > 0] /\ [v > 0] /\ [r > 0] /\ [u > 0] /\ [q > 0] /\ [b > c]].

#11: Simplified SEIT Model
[Simplified SEIT Model]
(b,d,v,c,u,q,r,J)
7
(E J)[[0 < d] /\ [0 < r] /\ [0 < u] /\ [0 < q] /\ [c < b] /\ [0 < v] /\ [0 < J] /\ [0 < b] /\ [0 < c] /\ [d + J b /= 0] /\ [-v /= 0] /\ [0 < (d + u) J v] /\ [v c /= 0] /\ [0 < d (d + J b)] /\ [0 < (d + J b) c v (-d v c + d^2 v + d^2 u + d v u q + d^3 + d^2 r + J b v u q + d u r + J b d v + J b d u + J b u r + J b d^2 + J b d r)] /\ [-(d + J b) c v^3 d (-d v b - J b v c + d^2 v + d^2 r + d v u q + d^3 + c J d^2 + d^2 u + d u r + c J d v + c J d u + J b d v + J b d r + J b v u q + J b d^2 + J^2 b d c + J b d u + J b u r + J^2 b c v + J^2 b u c) = 0]].

#12: Cyclic-3
[Cyclic-3]
(c,b,a)
1
(E b)(E a)[[a + b + c = 0] /\ [a b + b c + c a = 0] /\ [a b c - 1 = 0]].

#13: Cyclic-4
[Cyclic-4]
(d,c,b,a)
1
(E c)(E b)(E a)[[a + b + c + d = 0] /\ [a b + b c + c d + d a = 0] /\ [a b c + b c d + c d a + d a b = 0] /\ [a b c d - 1 = 0]].

#15: Joukowsky Transformation
[Joukowsky Transformation]
(a,b,c,d)
0
(A a)(A b)(A c)(A d)[[[a (c^2 + d^2) (a^2 + b^2 + 1) - c (a^2 + b^2) (c^2 + d^2 + 1) = 0] /\ [b (c^2 + d^2) (a^2 + b^2 - 1) - d (a^2 + b^2) (c^2 + d^2 - 1) = 0] /\ [b d > 0] /\ [c^2 + d^2 - 1 > 0]] ==> [[a = c] /\ [b = d]]].



#===================================================
# Joukowsky Transformation

#1: Joukowsky Transformation
[Joukowsky Transformation]
(a,b,c,d)
0
(A a)(A b)(A c)(A d)[[[a (c^2 + d^2) (a^2 + b^2 + 1) - c (a^2 + b^2) (c^2 + d^2 + 1) = 0] /\ [b (c^2 + d^2) (a^2 + b^2 - 1) - d (a^2 + b^2) (c^2 + d^2 - 1) = 0] /\ [b d > 0] /\ [c^2 + d^2 - 1 > 0]] ==> [[a = c] /\ [b = d]]].

#2: Separate Clauses
[Separate Clauses]
(a,b,c,d)
0
(E a)(E b)(E c)(E d)[b^2 c d^2 + a^2 c d^2 - a b^2 d^2 - a^3 d^2 - a d^2 + b^2 c^3 + a^2 c^3 - a b^2 c^2 - a^3 c^2 - a c^2 + b^2 c + a^2 c = 0 /\ b^2 d^3 + a^2 d^3 - b^3 d^2 - a^2 b d^2 + b d^2 + b^2 c^2 d + a^2 c^2 d - b^2 d - a^2 d - b^3 c^2 - a^2 b c^2 + b c^2 = 0 /\ (d)(b) > 0 /\ d^2 + c^2 - 1 > 0 /\ c - a /= 0]].

#3: Upper Half Plane
[Upper Half Plane]
(a,b,c,d)
0
(A a)(A b)(A c)(A d)[[[a (c^2 + d^2) (a^2 + b^2 + 1) - c (a^2 + b^2) (c^2 + d^2 + 1) = 0] /\ [b (c^2 + d^2) (a^2 + b^2 - 1) - d (a^2 + b^2) (c^2 + d^2 - 1) = 0] /\ [b > 0] /\ [d > 0]] ==> [[a = c] /\ [b = d]]].


#===================================================
# TTICAD Examples

#1: Intersection \dagger A
[Intersection \dagger A]
(x,y,z)
0
[[x z+z y-2 x=0] \/ [[z^2-y=0] /\ [2 x^2-y^2-z^2<0]]].

#2: Intersection \dagger B
[Intersection \dagger B]
(y,x,z)
0
[[x z+z y-2 x=0] \/ [[z^2-y=0] /\ [2 x^2-y^2-z^2<0]]].

#3: Random \dagger A
[Random \dagger A]
(x,y,z)
0
[[16 x^2+4 x y^2-4 z+1=0] \/ [[4 x+2 y^2 z+1=0] /\ [2 x^2 z-x-2 y^2<0]]].

#4: Random \dagger B
[Random \dagger B]
(y,x,z)
0
[[16 x^2+4 x y^2-4 z+1=0] \/ [[4 x+2 y^2 z+1=0] /\ [2 x^2 z-x-2 y^2<0]]].

#5: Ellipse \dagger A
[Ellipse \dagger A]
(a,b,c,x,y)
0
[[x^2+y^2-1=0] \/ [[ b^2 x^2-2 b^2 x c+b^2 c^2+a^2 y^2-a^2 b^2=0] /\ [a>0] /\ [a-1< 0] /\ [b>0] /\ [b-1<0] /\ [c>0] /\ [c-1<0]]].

#6: Ellipse \dagger B
[Ellipse \dagger B]
(a,b,c,y,x)
0
[[x^2+y^2-1=0] \/ [[ b^2 x^2-2 b^2 x c+b^2 c^2+a^2 y^2-a^2 b^2=0] /\ [a>0] /\ [a-1< 0] /\ [b>0] /\ [b-1<0] /\ [c>0] /\ [c-1<0]]].

#7: Solotareff \dagger A
[Solotareff \dagger A]
(a,b,x,y)
0
[[[3 x^2-2 x-a=0] /\ [x^3-x^2-a x-2 b+a-2>0] /\ [4 a-1>0] /\ [4 a-7<0] /\ [x+1>0] /\ [x<0]] \/ [[3 y^2-2 y-a=0] /\ [y^3-y^2-a y-a+2>0] /\ [4 b+3>0] /\ [4 b-3<0] /\ [y>0] /\ [y-1<0]]].

#8: Solotareff \dagger B
[Solotareff \dagger B]
(b,a,x,y)
0
[[[3 x^2-2 x-a=0] /\ [x^3-x^2-a x-2 b+a-2>0] /\ [4 a-1>0] /\ [4 a-7<0] /\ [x+1>0] /\ [x<0]] \/ [[3 y^2-2 y-a=0] /\ [y^3-y^2-a y-a+2>0] /\ [4 b+3>0] /\ [4 b-3<0] /\ [y>0] /\ [y-1<0]]].

#9: Collision \dagger A
[Collision \dagger A]
(a,t,x,y)
0
[[[x^2-2 x t+t^2+4 y^2-80 y+396=0] /\ [t>0]] \/ [[x^2-2 x a t+5 a^2 t^2+4 y^2-8 y a t-4=0] /\ [a>0]]].

#10: Collision \dagger B
[Collision \dagger B]
(a,y,x,t)
0
[[[x^2-2 x t+t^2+4 y^2-80 y+396=0] /\ [t>0]] \/ [[x^2-2 x a t+5 a^2 t^2+4 y^2-8 y a t-4=0] /\ [a>0]]].

#11: Kahan A
[Kahan A]
(x,y)
0
[[[8 y^3 x+8 y x^3+20 y^3+84 y x^2+288 y x+324 y=0] /\ [-225 x^2-324 x+63 y^2-4 x^4-52 x^3+12 y^2 x+4 y^4<0]] \/ [[2 y=0] /\ [2 x+9<0]] \/ [[8 y=0] /\ [8 x^2+56 x+8 y^2+96<0]] \/ [[y=0] /\ [x^2+7 x+y^2+12<0]] \/ [[8 y^3 x+8 y x^3+20 y^3+84 y x^2+288 y x+324 y=0] /\ [-4 x^4-52 x^3-252 x^2+12 y^2 x-540 x+36 y^2+4 y^4-432<=0] /\ [4 x^4+52 x^3+225 x^2-12 y^2 x+324 x-63 y^2-4 y^4<0]] \/ [[2 y=0] /\ [-2 x-6<0] /\[2 x<=]] \/ [[8 y=0] /\ [-8 x^2-56 x-8 y^2-96<0] /\ [2 x^2+8 x+2 y^2<=0]]].

#12: Kahan B
[Kahan B]
(y,x)
0
[[[8 y^3 x+8 y x^3+20 y^3+84 y x^2+288 y x+324 y=0] /\ [-225 x^2-324 x+63 y^2-4 x^4-52 x^3+12 y^2 x+4 y^4<0]] \/ [[2 y=0] /\ [2 x+9<0]] \/ [[8 y=0] /\ [8 x^2+56 x+8 y^2+96<0]] \/ [[y=0] /\ [x^2+7 x+y^2+12<0]] \/ [[8 y^3 x+8 y x^3+20 y^3+84 y x^2+288 y x+324 y=0] /\ [-4 x^4-52 x^3-252 x^2+12 y^2 x-540 x+36 y^2+4 y^4-432<=0] /\ [4 x^4+52 x^3+225 x^2-12 y^2 x+324 x-63 y^2-4 y^4<0]] \/ [[2 y=0] /\ [-2 x-6<0] /\[2 x<=]] \/ [[8 y=0] /\ [-8 x^2-56 x-8 y^2-96<0] /\ [2 x^2+8 x+2 y^2<=0]]].

#13: ArcSin A 
[ArcSin A]
(x,y)
0
[[[-2 x y=0] /\ [y^2-x^2+1<0]] \/ [[16 y^3 x-16 y x^3+8 y x=0] /\ [1-4 x^2+4 y^2+4 x^4-24 x^2 y^2+4 y^4<=0]] \/ [[y=0] /\ [1-x<=0]] \/ [[y=0] /\ [x+1<=0]]].

#14: ArcSin B 
[ArcSin B]
(y,x)
0
[[[-2 x y=0] /\ [y^2-x^2+1<0]] \/ [[16 y^3 x-16 y x^3+8 y x=0] /\ [1-4 x^2+4 y^2+4 x^4-24 x^2 y^2+4 y^4<=0]] \/ [[y=0] /\ [1-x<=0]] \/ [[y=0] /\ [x+1<=0]]].

#15: 2D Example A
[2D Example A]
(x,y)
0
[[[x^2+y^2-1=0] /\ [4 x y-1<0]] \/ [[x^2-8 x+16+y^2-2 y=0] /\ [4 x y-4 x-17<0]]].

#16: 2D Example B
[2D Example B]
(y,x)
0
[[[x^2+y^2-1=0] /\ [4 x y-1<0]] \/ [[x^2-8 x+16+y^2-2 y=0] /\ [4 x y-4 x-17<0]]].

#17: 3D Example A
[3D Example A]
(x,y,z)
0
[[[x^2+y^2+z^2-1=0] /\ [4 x y z-1<0]] \/ [[x^2-8 x+y^2-2 y+z^2-4 z+20=0] /\ [4 y x z-8 y x-4 x z+8 x-16 y z+32 y+16 z-33<0]]].

#18: 3D Example B
[3D Example B]
(y,x,z)
0
[[[x^2+y^2+z^2-1=0] /\ [4 x y z-1<0]] \/ [[x^2-8 x+y^2-2 y+z^2-4 z+20=0] /\ [4 y x z-8 y x-4 x z+8 x-16 y z+32 y+16 z-33<0]]].