Overview - Maple Help

Overview of the QuantifierElimination Package

Description

 • The QuantifierElimination package contains routines for quantifier elimination (QE) over the reals, as well as other related auxiliary tools for working with Tarski formulae and other related formulae.
 • QuantifierEliminate, PartialCylindricalAlgebraicDecompose, InsertFormula, and DeleteFormula are all routines to perform QE. The latter two routines are "evolutionary" methods [Ton19], which is a term usually referred to in other academic literature as "incremental".
 • CylindricalAlgebraicDecompose is a routine to produce "stock" Cylindrical Algebraic Decompositions (CADs) for sets of polynomials or formulae. CADs have many uses in real algebraic geometry.
 • PartialCylindricalAlgebraicDecompose can also be used for such purposes, where partial CAD is used to attempt to construct minimal geometry depending on truth values. Generally, PartialCylindricalAlgebraicDecompose is a quantifier elimination tool in the same manner as QuantifierEliminate. Where CAD is used for the purposes of quantifier elimination, the methodology is partial CAD [CH91] for lifting to aim for early termination.
 • QuantifierEliminate, InsertFormula, and DeleteFormula use poly-algorithmic methodology for quantifier elimination between two prolific algorithms for QE, Virtual Term Substitution (VTS) and Cylindrical Algebraic Decomposition (CAD) [Ton20].
 • Where VTS is implemented, the main sources of algorithms is [Kos16]. VTS is an algorithm best suited to elimination of quantified variables appearing at low degree in the input formula. VTS within QuantifierElimination is implemented to eliminate variables appearing up to quadratically in a formula, pending factorization of polynomials.
 • Where quantifier elimination is offered by the package, routines follow an output syntax defined by a keyword option output. This option enables production of the quantifier-free answer for a QE problem, as well as "witnesses" that prove equivalence of QE to a quantifier-free answer. Additionally, requesting data provides QEData or CADData objects that enable QE in an incremental fashion, along with other methods to enable inspection of the data structures in greater detail. For more information, see the help page QuantifierElimination options.
 • Witnesses can be requested for any QE formula that is fully quantified with only one type of quantifier symbol ($\mathrm{forall}$ or $\mathrm{exists}$). Production of witnesses is possible under any methodology within QuantifierElimination, including poly-algorithmic or pure CAD. Production of witnesses from VTS is discussed in [Ton20, KS16].
 • The methodology for production of CADs within QuantifierElimination is always projection and lifting, where the projection operator implemented is the Lazard projection operator [Laz94, MPP19].
 • The QuantifierTools subpackage is a source of auxiliary tools for working with formulae and other outputs from QuantifierElimination.
 • Where equational constraints are used within CAD in the package, curtain occurrences may prevent the output from being mathematically correct. The package implements algorithms to try to recover from such occurrences to maximize the chance of success [NDS19, Ton21].
 • The package uses a number of keyword options that are common across routines for the package, especially those offering quantifier elimination. These options are dependent and specific to the methodology used within the routine on request.
 • The work [Ton21] is the main academic source of reference for the package.
 List of QuantifierElimination Commands
 List of QuantifierElimination Subpackages

Examples

 > $\mathrm{with}\left(\mathrm{QuantifierElimination}\right)$
 $\left[{\mathrm{CylindricalAlgebraicDecompose}}{,}{\mathrm{DeleteFormula}}{,}{\mathrm{InsertFormula}}{,}{\mathrm{PartialCylindricalAlgebraicDecompose}}{,}{\mathrm{QuantifierEliminate}}{,}{\mathrm{QuantifierTools}}\right]$ (1)
 > $\mathrm{QuantifierEliminate}\left(\mathrm{exists}\left(x,a{x}^{2}+bx+c=0\right)\right)$
 $\left({a}{=}{0}{\wedge }{b}{=}{0}{\wedge }{c}{=}{0}\right){\vee }\left({a}{=}{0}{\wedge }{b}{\ne }{0}{\wedge }{a}{}{{c}}^{{2}}{=}{0}\right){\vee }\left({a}{<}{0}{\wedge }{4}{}{a}{}{c}{-}{{b}}^{{2}}{<}{0}\right){\vee }\left({a}{\ne }{0}{\wedge }{4}{}{a}{}{c}{-}{{b}}^{{2}}{\le }{0}\right){\vee }\left({-}{a}{<}{0}{\wedge }{4}{}{a}{}{c}{-}{{b}}^{{2}}{<}{0}\right)$ (2)
 > $\mathrm{PartialCylindricalAlgebraicDecompose}\left(\mathrm{exists}\left(x,a{x}^{3}+b{x}^{2}+cx+d=0\right)\right)$
 $\left({d}{<}{0}{\wedge }{c}{<}{0}{\wedge }{b}{<}\frac{{{c}}^{{2}}}{{3}{}{d}}{\wedge }{a}{<}{0}\right){\vee }\left({d}{<}{0}{\wedge }{c}{<}{0}{\wedge }{b}{<}\frac{{{c}}^{{2}}}{{3}{}{d}}{\wedge }{0}{<}{a}\right){\vee }\left({d}{<}{0}{\wedge }{c}{<}{0}{\wedge }{b}{=}\frac{{{c}}^{{2}}}{{3}{}{d}}{\wedge }{a}{<}{\mathrm{RootOf}}{}\left({729}{}{{d}}^{{4}}{}{{\mathrm{_Z}}}^{{2}}{-}{54}{}{{c}}^{{3}}{}{\mathrm{_Z}}{}{{d}}^{{2}}{+}{{c}}^{{6}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{c}{<}{0}{\wedge }{b}{=}\frac{{{c}}^{{2}}}{{3}{}{d}}{\wedge }{a}{=}{\mathrm{RootOf}}{}\left({729}{}{{d}}^{{4}}{}{{\mathrm{_Z}}}^{{2}}{-}{54}{}{{c}}^{{3}}{}{\mathrm{_Z}}{}{{d}}^{{2}}{+}{{c}}^{{6}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{c}{<}{0}{\wedge }{b}{=}\frac{{{c}}^{{2}}}{{3}{}{d}}{\wedge }{\mathrm{RootOf}}{}\left({729}{}{{d}}^{{4}}{}{{\mathrm{_Z}}}^{{2}}{-}{54}{}{{c}}^{{3}}{}{\mathrm{_Z}}{}{{d}}^{{2}}{+}{{c}}^{{6}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right){<}{a}{\wedge }{a}{<}{0}\right){\vee }\left({d}{<}{0}{\wedge }{c}{<}{0}{\wedge }{b}{=}\frac{{{c}}^{{2}}}{{3}{}{d}}{\wedge }{0}{<}{a}\right){\vee }\left({d}{<}{0}{\wedge }{c}{<}{0}{\wedge }\frac{{{c}}^{{2}}}{{3}{}{d}}{<}{b}{\wedge }{b}{<}\frac{{{c}}^{{2}}}{{4}{}{d}}{\wedge }{a}{<}{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{c}{<}{0}{\wedge }\frac{{{c}}^{{2}}}{{3}{}{d}}{<}{b}{\wedge }{b}{<}\frac{{{c}}^{{2}}}{{4}{}{d}}{\wedge }{a}{=}{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{c}{<}{0}{\wedge }\frac{{{c}}^{{2}}}{{3}{}{d}}{<}{b}{\wedge }{b}{<}\frac{{{c}}^{{2}}}{{4}{}{d}}{\wedge }{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right){<}{a}{\wedge }{a}{<}{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{c}{<}{0}{\wedge }\frac{{{c}}^{{2}}}{{3}{}{d}}{<}{b}{\wedge }{b}{<}\frac{{{c}}^{{2}}}{{4}{}{d}}{\wedge }{a}{=}{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{c}{<}{0}{\wedge }\frac{{{c}}^{{2}}}{{3}{}{d}}{<}{b}{\wedge }{b}{<}\frac{{{c}}^{{2}}}{{4}{}{d}}{\wedge }{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right){<}{a}{\wedge }{a}{<}{0}\right){\vee }\left({d}{<}{0}{\wedge }{c}{<}{0}{\wedge }\frac{{{c}}^{{2}}}{{3}{}{d}}{<}{b}{\wedge }{b}{<}\frac{{{c}}^{{2}}}{{4}{}{d}}{\wedge }{0}{<}{a}\right){\vee }\left({d}{<}{0}{\wedge }{c}{<}{0}{\wedge }{b}{=}\frac{{{c}}^{{2}}}{{4}{}{d}}{\wedge }{a}{<}{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({54}{}{{d}}^{{2}}{}{\mathrm{_Z}}{-}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{c}{<}{0}{\wedge }{b}{=}\frac{{{c}}^{{2}}}{{4}{}{d}}{\wedge }{a}{=}{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({54}{}{{d}}^{{2}}{}{\mathrm{_Z}}{-}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{c}{<}{0}{\wedge }{b}{=}\frac{{{c}}^{{2}}}{{4}{}{d}}{\wedge }{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({54}{}{{d}}^{{2}}{}{\mathrm{_Z}}{-}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right){<}{a}{\wedge }{a}{<}{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({54}{}{{d}}^{{2}}{}{\mathrm{_Z}}{-}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{c}{<}{0}{\wedge }{b}{=}\frac{{{c}}^{{2}}}{{4}{}{d}}{\wedge }{a}{=}{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({54}{}{{d}}^{{2}}{}{\mathrm{_Z}}{-}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{c}{<}{0}{\wedge }{b}{=}\frac{{{c}}^{{2}}}{{4}{}{d}}{\wedge }{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({54}{}{{d}}^{{2}}{}{\mathrm{_Z}}{-}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right){<}{a}\right){\vee }\left({d}{<}{0}{\wedge }{c}{<}{0}{\wedge }\frac{{{c}}^{{2}}}{{4}{}{d}}{<}{b}{\wedge }{b}{<}{0}{\wedge }{a}{<}{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{c}{<}{0}{\wedge }\frac{{{c}}^{{2}}}{{4}{}{d}}{<}{b}{\wedge }{b}{<}{0}{\wedge }{a}{=}{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{c}{<}{0}{\wedge }\frac{{{c}}^{{2}}}{{4}{}{d}}{<}{b}{\wedge }{b}{<}{0}{\wedge }{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right){<}{a}{\wedge }{a}{<}{0}\right){\vee }\left({d}{<}{0}{\wedge }{c}{<}{0}{\wedge }\frac{{{c}}^{{2}}}{{4}{}{d}}{<}{b}{\wedge }{b}{<}{0}{\wedge }{a}{=}{0}\right){\vee }\left({d}{<}{0}{\wedge }{c}{<}{0}{\wedge }\frac{{{c}}^{{2}}}{{4}{}{d}}{<}{b}{\wedge }{b}{<}{0}{\wedge }{0}{<}{a}{\wedge }{a}{<}{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{c}{<}{0}{\wedge }\frac{{{c}}^{{2}}}{{4}{}{d}}{<}{b}{\wedge }{b}{<}{0}{\wedge }{a}{=}{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{c}{<}{0}{\wedge }\frac{{{c}}^{{2}}}{{4}{}{d}}{<}{b}{\wedge }{b}{<}{0}{\wedge }{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right){<}{a}\right){\vee }\left({d}{<}{0}{\wedge }{c}{<}{0}{\wedge }{b}{=}{0}{\wedge }{a}{<}{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({27}{}{{d}}^{{2}}{}{\mathrm{_Z}}{+}{4}{}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{c}{<}{0}{\wedge }{b}{=}{0}{\wedge }{a}{=}{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({27}{}{{d}}^{{2}}{}{\mathrm{_Z}}{+}{4}{}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{c}{<}{0}{\wedge }{b}{=}{0}{\wedge }{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({27}{}{{d}}^{{2}}{}{\mathrm{_Z}}{+}{4}{}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right){<}{a}{\wedge }{a}{<}{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({27}{}{{d}}^{{2}}{}{\mathrm{_Z}}{+}{4}{}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{c}{<}{0}{\wedge }{b}{=}{0}{\wedge }{a}{=}{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({27}{}{{d}}^{{2}}{}{\mathrm{_Z}}{+}{4}{}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{c}{<}{0}{\wedge }{b}{=}{0}{\wedge }{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({27}{}{{d}}^{{2}}{}{\mathrm{_Z}}{+}{4}{}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right){<}{a}\right){\vee }\left({d}{<}{0}{\wedge }{c}{<}{0}{\wedge }{0}{<}{b}{\wedge }{a}{<}{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{c}{<}{0}{\wedge }{0}{<}{b}{\wedge }{a}{=}{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{c}{<}{0}{\wedge }{0}{<}{b}{\wedge }{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right){<}{a}{\wedge }{a}{<}{0}\right){\vee }\left({d}{<}{0}{\wedge }{c}{<}{0}{\wedge }{0}{<}{b}{\wedge }{a}{=}{0}\right){\vee }\left({d}{<}{0}{\wedge }{c}{<}{0}{\wedge }{0}{<}{b}{\wedge }{0}{<}{a}{\wedge }{a}{<}{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{c}{<}{0}{\wedge }{0}{<}{b}{\wedge }{a}{=}{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{c}{<}{0}{\wedge }{0}{<}{b}{\wedge }{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right){<}{a}\right){\vee }\left({d}{<}{0}{\wedge }{c}{=}{0}{\wedge }{b}{<}{0}{\wedge }{a}{<}{0}\right){\vee }\left({d}{<}{0}{\wedge }{c}{=}{0}{\wedge }{b}{<}{0}{\wedge }{0}{<}{a}\right){\vee }\left({d}{<}{0}{\wedge }{c}{=}{0}{\wedge }{b}{=}{0}{\wedge }{a}{<}{0}\right){\vee }\left({d}{<}{0}{\wedge }{c}{=}{0}{\wedge }{b}{=}{0}{\wedge }{0}{<}{a}\right){\vee }\left({d}{<}{0}{\wedge }{c}{=}{0}{\wedge }{0}{<}{b}{\wedge }{a}{<}{\mathrm{RootOf}}{}\left({27}{}{{\mathrm{_Z}}}^{{2}}{}{d}{+}{4}{}{{b}}^{{3}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{c}{=}{0}{\wedge }{0}{<}{b}{\wedge }{a}{=}{\mathrm{RootOf}}{}\left({27}{}{{\mathrm{_Z}}}^{{2}}{}{d}{+}{4}{}{{b}}^{{3}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{c}{=}{0}{\wedge }{0}{<}{b}{\wedge }{\mathrm{RootOf}}{}\left({27}{}{{\mathrm{_Z}}}^{{2}}{}{d}{+}{4}{}{{b}}^{{3}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right){<}{a}{\wedge }{a}{<}{0}\right){\vee }\left({d}{<}{0}{\wedge }{c}{=}{0}{\wedge }{0}{<}{b}{\wedge }{a}{=}{0}\right){\vee }\left({d}{<}{0}{\wedge }{c}{=}{0}{\wedge }{0}{<}{b}{\wedge }{0}{<}{a}{\wedge }{a}{<}{\mathrm{RootOf}}{}\left({27}{}{{\mathrm{_Z}}}^{{2}}{}{d}{+}{4}{}{{b}}^{{3}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{c}{=}{0}{\wedge }{0}{<}{b}{\wedge }{a}{=}{\mathrm{RootOf}}{}\left({27}{}{{\mathrm{_Z}}}^{{2}}{}{d}{+}{4}{}{{b}}^{{3}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{c}{=}{0}{\wedge }{0}{<}{b}{\wedge }{\mathrm{RootOf}}{}\left({27}{}{{\mathrm{_Z}}}^{{2}}{}{d}{+}{4}{}{{b}}^{{3}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right){<}{a}\right){\vee }\left({d}{<}{0}{\wedge }{0}{<}{c}{\wedge }{b}{<}\frac{{{c}}^{{2}}}{{3}{}{d}}{\wedge }{a}{<}{0}\right){\vee }\left({d}{<}{0}{\wedge }{0}{<}{c}{\wedge }{b}{<}\frac{{{c}}^{{2}}}{{3}{}{d}}{\wedge }{0}{<}{a}\right){\vee }\left({d}{<}{0}{\wedge }{0}{<}{c}{\wedge }{b}{=}\frac{{{c}}^{{2}}}{{3}{}{d}}{\wedge }{a}{<}{0}\right){\vee }\left({d}{<}{0}{\wedge }{0}{<}{c}{\wedge }{b}{=}\frac{{{c}}^{{2}}}{{3}{}{d}}{\wedge }{0}{<}{a}{\wedge }{a}{<}{\mathrm{RootOf}}{}\left({729}{}{{d}}^{{4}}{}{{\mathrm{_Z}}}^{{2}}{-}{54}{}{{c}}^{{3}}{}{\mathrm{_Z}}{}{{d}}^{{2}}{+}{{c}}^{{6}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{0}{<}{c}{\wedge }{b}{=}\frac{{{c}}^{{2}}}{{3}{}{d}}{\wedge }{a}{=}{\mathrm{RootOf}}{}\left({729}{}{{d}}^{{4}}{}{{\mathrm{_Z}}}^{{2}}{-}{54}{}{{c}}^{{3}}{}{\mathrm{_Z}}{}{{d}}^{{2}}{+}{{c}}^{{6}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{0}{<}{c}{\wedge }{b}{=}\frac{{{c}}^{{2}}}{{3}{}{d}}{\wedge }{\mathrm{RootOf}}{}\left({729}{}{{d}}^{{4}}{}{{\mathrm{_Z}}}^{{2}}{-}{54}{}{{c}}^{{3}}{}{\mathrm{_Z}}{}{{d}}^{{2}}{+}{{c}}^{{6}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right){<}{a}\right){\vee }\left({d}{<}{0}{\wedge }{0}{<}{c}{\wedge }\frac{{{c}}^{{2}}}{{3}{}{d}}{<}{b}{\wedge }{b}{<}\frac{{{c}}^{{2}}}{{4}{}{d}}{\wedge }{a}{<}{0}\right){\vee }\left({d}{<}{0}{\wedge }{0}{<}{c}{\wedge }\frac{{{c}}^{{2}}}{{3}{}{d}}{<}{b}{\wedge }{b}{<}\frac{{{c}}^{{2}}}{{4}{}{d}}{\wedge }{0}{<}{a}{\wedge }{a}{<}{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{0}{<}{c}{\wedge }\frac{{{c}}^{{2}}}{{3}{}{d}}{<}{b}{\wedge }{b}{<}\frac{{{c}}^{{2}}}{{4}{}{d}}{\wedge }{a}{=}{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{0}{<}{c}{\wedge }\frac{{{c}}^{{2}}}{{3}{}{d}}{<}{b}{\wedge }{b}{<}\frac{{{c}}^{{2}}}{{4}{}{d}}{\wedge }{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right){<}{a}{\wedge }{a}{<}{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{0}{<}{c}{\wedge }\frac{{{c}}^{{2}}}{{3}{}{d}}{<}{b}{\wedge }{b}{<}\frac{{{c}}^{{2}}}{{4}{}{d}}{\wedge }{a}{=}{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{0}{<}{c}{\wedge }\frac{{{c}}^{{2}}}{{3}{}{d}}{<}{b}{\wedge }{b}{<}\frac{{{c}}^{{2}}}{{4}{}{d}}{\wedge }{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right){<}{a}\right){\vee }\left({d}{<}{0}{\wedge }{0}{<}{c}{\wedge }{b}{=}\frac{{{c}}^{{2}}}{{4}{}{d}}{\wedge }{a}{<}{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({54}{}{{d}}^{{2}}{}{\mathrm{_Z}}{-}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{0}{<}{c}{\wedge }{b}{=}\frac{{{c}}^{{2}}}{{4}{}{d}}{\wedge }{a}{=}{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({54}{}{{d}}^{{2}}{}{\mathrm{_Z}}{-}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{0}{<}{c}{\wedge }{b}{=}\frac{{{c}}^{{2}}}{{4}{}{d}}{\wedge }{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({54}{}{{d}}^{{2}}{}{\mathrm{_Z}}{-}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right){<}{a}{\wedge }{a}{<}{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({54}{}{{d}}^{{2}}{}{\mathrm{_Z}}{-}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{0}{<}{c}{\wedge }{b}{=}\frac{{{c}}^{{2}}}{{4}{}{d}}{\wedge }{a}{=}{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({54}{}{{d}}^{{2}}{}{\mathrm{_Z}}{-}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{0}{<}{c}{\wedge }{b}{=}\frac{{{c}}^{{2}}}{{4}{}{d}}{\wedge }{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({54}{}{{d}}^{{2}}{}{\mathrm{_Z}}{-}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right){<}{a}\right){\vee }\left({d}{<}{0}{\wedge }{0}{<}{c}{\wedge }\frac{{{c}}^{{2}}}{{4}{}{d}}{<}{b}{\wedge }{b}{<}{0}{\wedge }{a}{<}{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{0}{<}{c}{\wedge }\frac{{{c}}^{{2}}}{{4}{}{d}}{<}{b}{\wedge }{b}{<}{0}{\wedge }{a}{=}{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{0}{<}{c}{\wedge }\frac{{{c}}^{{2}}}{{4}{}{d}}{<}{b}{\wedge }{b}{<}{0}{\wedge }{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right){<}{a}{\wedge }{a}{<}{0}\right){\vee }\left({d}{<}{0}{\wedge }{0}{<}{c}{\wedge }\frac{{{c}}^{{2}}}{{4}{}{d}}{<}{b}{\wedge }{b}{<}{0}{\wedge }{a}{=}{0}\right){\vee }\left({d}{<}{0}{\wedge }{0}{<}{c}{\wedge }\frac{{{c}}^{{2}}}{{4}{}{d}}{<}{b}{\wedge }{b}{<}{0}{\wedge }{0}{<}{a}{\wedge }{a}{<}{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{0}{<}{c}{\wedge }\frac{{{c}}^{{2}}}{{4}{}{d}}{<}{b}{\wedge }{b}{<}{0}{\wedge }{a}{=}{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{0}{<}{c}{\wedge }\frac{{{c}}^{{2}}}{{4}{}{d}}{<}{b}{\wedge }{b}{<}{0}{\wedge }{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right){<}{a}\right){\vee }\left({d}{<}{0}{\wedge }{0}{<}{c}{\wedge }{b}{=}{0}{\wedge }{a}{<}{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({27}{}{{d}}^{{2}}{}{\mathrm{_Z}}{+}{4}{}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{0}{<}{c}{\wedge }{b}{=}{0}{\wedge }{a}{=}{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({27}{}{{d}}^{{2}}{}{\mathrm{_Z}}{+}{4}{}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{0}{<}{c}{\wedge }{b}{=}{0}{\wedge }{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({27}{}{{d}}^{{2}}{}{\mathrm{_Z}}{+}{4}{}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right){<}{a}{\wedge }{a}{<}{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({27}{}{{d}}^{{2}}{}{\mathrm{_Z}}{+}{4}{}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{0}{<}{c}{\wedge }{b}{=}{0}{\wedge }{a}{=}{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({27}{}{{d}}^{{2}}{}{\mathrm{_Z}}{+}{4}{}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{0}{<}{c}{\wedge }{b}{=}{0}{\wedge }{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({27}{}{{d}}^{{2}}{}{\mathrm{_Z}}{+}{4}{}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right){<}{a}\right){\vee }\left({d}{<}{0}{\wedge }{0}{<}{c}{\wedge }{0}{<}{b}{\wedge }{a}{<}{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{0}{<}{c}{\wedge }{0}{<}{b}{\wedge }{a}{=}{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{0}{<}{c}{\wedge }{0}{<}{b}{\wedge }{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right){<}{a}{\wedge }{a}{<}{0}\right){\vee }\left({d}{<}{0}{\wedge }{0}{<}{c}{\wedge }{0}{<}{b}{\wedge }{a}{=}{0}\right){\vee }\left({d}{<}{0}{\wedge }{0}{<}{c}{\wedge }{0}{<}{b}{\wedge }{0}{<}{a}{\wedge }{a}{<}{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{0}{<}{c}{\wedge }{0}{<}{b}{\wedge }{a}{=}{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right)\right){\vee }\left({d}{<}{0}{\wedge }{0}{<}{c}{\wedge }{0}{<}{b}{\wedge }{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right){<}{a}\right){\vee }\left({d}{=}{0}{\wedge }{c}{<}{0}{\wedge }{b}{<}{0}{\wedge }{a}{<}\frac{{{b}}^{{2}}}{{4}{}{c}}\right){\vee }\left({d}{=}{0}{\wedge }{c}{<}{0}{\wedge }{b}{<}{0}{\wedge }{a}{=}\frac{{{b}}^{{2}}}{{4}{}{c}}\right){\vee }\left({d}{=}{0}{\wedge }{c}{<}{0}{\wedge }{b}{<}{0}{\wedge }\frac{{{b}}^{{2}}}{{4}{}{c}}{<}{a}{\wedge }{a}{<}{0}\right){\vee }\left({d}{=}{0}{\wedge }{c}{<}{0}{\wedge }{b}{<}{0}{\wedge }{a}{=}{0}\right){\vee }\left({d}{=}{0}{\wedge }{c}{<}{0}{\wedge }{b}{<}{0}{\wedge }{0}{<}{a}\right){\vee }\left({d}{=}{0}{\wedge }{c}{<}{0}{\wedge }{b}{=}{0}{\wedge }{a}{<}{0}\right){\vee }\left({d}{=}{0}{\wedge }{c}{<}{0}{\wedge }{b}{=}{0}{\wedge }{a}{=}{0}\right){\vee }\left({d}{=}{0}{\wedge }{c}{<}{0}{\wedge }{b}{=}{0}{\wedge }{0}{<}{a}\right){\vee }\left({d}{=}{0}{\wedge }{c}{<}{0}{\wedge }{0}{<}{b}{\wedge }{a}{<}\frac{{{b}}^{{2}}}{{4}{}{c}}\right){\vee }\left({d}{=}{0}{\wedge }{c}{<}{0}{\wedge }{0}{<}{b}{\wedge }{a}{=}\frac{{{b}}^{{2}}}{{4}{}{c}}\right){\vee }\left({d}{=}{0}{\wedge }{c}{<}{0}{\wedge }{0}{<}{b}{\wedge }\frac{{{b}}^{{2}}}{{4}{}{c}}{<}{a}{\wedge }{a}{<}{0}\right){\vee }\left({d}{=}{0}{\wedge }{c}{<}{0}{\wedge }{0}{<}{b}{\wedge }{a}{=}{0}\right){\vee }\left({d}{=}{0}{\wedge }{c}{<}{0}{\wedge }{0}{<}{b}{\wedge }{0}{<}{a}\right){\vee }\left({d}{=}{0}{\wedge }{c}{=}{0}{\wedge }{b}{<}{0}{\wedge }{a}{<}{0}\right){\vee }\left({d}{=}{0}{\wedge }{c}{=}{0}{\wedge }{b}{<}{0}{\wedge }{a}{=}{0}\right){\vee }\left({d}{=}{0}{\wedge }{c}{=}{0}{\wedge }{b}{<}{0}{\wedge }{0}{<}{a}\right){\vee }\left({d}{=}{0}{\wedge }{c}{=}{0}{\wedge }{b}{=}{0}{\wedge }{a}{=}{0}\right){\vee }\left({d}{=}{0}{\wedge }{c}{=}{0}{\wedge }{b}{=}{0}{\wedge }{a}{<}{0}\right){\vee }\left({d}{=}{0}{\wedge }{c}{=}{0}{\wedge }{b}{=}{0}{\wedge }{0}{<}{a}\right){\vee }\left({d}{=}{0}{\wedge }{c}{=}{0}{\wedge }{0}{<}{b}{\wedge }{a}{<}{0}\right){\vee }\left({d}{=}{0}{\wedge }{c}{=}{0}{\wedge }{0}{<}{b}{\wedge }{a}{=}{0}\right){\vee }\left({d}{=}{0}{\wedge }{c}{=}{0}{\wedge }{0}{<}{b}{\wedge }{0}{<}{a}\right){\vee }\left({d}{=}{0}{\wedge }{0}{<}{c}{\wedge }{b}{<}{0}{\wedge }{a}{<}{0}\right){\vee }\left({d}{=}{0}{\wedge }{0}{<}{c}{\wedge }{b}{<}{0}{\wedge }{a}{=}{0}\right){\vee }\left({d}{=}{0}{\wedge }{0}{<}{c}{\wedge }{b}{<}{0}{\wedge }{0}{<}{a}{\wedge }{a}{<}\frac{{{b}}^{{2}}}{{4}{}{c}}\right){\vee }\left({d}{=}{0}{\wedge }{0}{<}{c}{\wedge }{b}{<}{0}{\wedge }{a}{=}\frac{{{b}}^{{2}}}{{4}{}{c}}\right){\vee }\left({d}{=}{0}{\wedge }{0}{<}{c}{\wedge }{b}{<}{0}{\wedge }\frac{{{b}}^{{2}}}{{4}{}{c}}{<}{a}\right){\vee }\left({d}{=}{0}{\wedge }{0}{<}{c}{\wedge }{b}{=}{0}{\wedge }{a}{<}{0}\right){\vee }\left({d}{=}{0}{\wedge }{0}{<}{c}{\wedge }{b}{=}{0}{\wedge }{a}{=}{0}\right){\vee }\left({d}{=}{0}{\wedge }{0}{<}{c}{\wedge }{b}{=}{0}{\wedge }{0}{<}{a}\right){\vee }\left({d}{=}{0}{\wedge }{0}{<}{c}{\wedge }{0}{<}{b}{\wedge }{a}{<}{0}\right){\vee }\left({d}{=}{0}{\wedge }{0}{<}{c}{\wedge }{0}{<}{b}{\wedge }{a}{=}{0}\right){\vee }\left({d}{=}{0}{\wedge }{0}{<}{c}{\wedge }{0}{<}{b}{\wedge }{0}{<}{a}{\wedge }{a}{<}\frac{{{b}}^{{2}}}{{4}{}{c}}\right){\vee }\left({d}{=}{0}{\wedge }{0}{<}{c}{\wedge }{0}{<}{b}{\wedge }{a}{=}\frac{{{b}}^{{2}}}{{4}{}{c}}\right){\vee }\left({d}{=}{0}{\wedge }{0}{<}{c}{\wedge }{0}{<}{b}{\wedge }\frac{{{b}}^{{2}}}{{4}{}{c}}{<}{a}\right){\vee }\left({0}{<}{d}{\wedge }{c}{<}{0}{\wedge }{b}{<}{0}{\wedge }{a}{<}{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({0}{<}{d}{\wedge }{c}{<}{0}{\wedge }{b}{<}{0}{\wedge }{a}{=}{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({0}{<}{d}{\wedge }{c}{<}{0}{\wedge }{b}{<}{0}{\wedge }{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right){<}{a}{\wedge }{a}{<}{0}\right){\vee }\left({0}{<}{d}{\wedge }{c}{<}{0}{\wedge }{b}{<}{0}{\wedge }{a}{=}{0}\right){\vee }\left({0}{<}{d}{\wedge }{c}{<}{0}{\wedge }{b}{<}{0}{\wedge }{0}{<}{a}{\wedge }{a}{<}{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right)\right){\vee }\left({0}{<}{d}{\wedge }{c}{<}{0}{\wedge }{b}{<}{0}{\wedge }{a}{=}{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right)\right){\vee }\left({0}{<}{d}{\wedge }{c}{<}{0}{\wedge }{b}{<}{0}{\wedge }{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right){<}{a}\right){\vee }\left({0}{<}{d}{\wedge }{c}{<}{0}{\wedge }{b}{=}{0}{\wedge }{a}{<}{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({27}{}{{d}}^{{2}}{}{\mathrm{_Z}}{+}{4}{}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({0}{<}{d}{\wedge }{c}{<}{0}{\wedge }{b}{=}{0}{\wedge }{a}{=}{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({27}{}{{d}}^{{2}}{}{\mathrm{_Z}}{+}{4}{}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({0}{<}{d}{\wedge }{c}{<}{0}{\wedge }{b}{=}{0}{\wedge }{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({27}{}{{d}}^{{2}}{}{\mathrm{_Z}}{+}{4}{}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right){<}{a}{\wedge }{a}{<}{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({27}{}{{d}}^{{2}}{}{\mathrm{_Z}}{+}{4}{}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right)\right){\vee }\left({0}{<}{d}{\wedge }{c}{<}{0}{\wedge }{b}{=}{0}{\wedge }{a}{=}{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({27}{}{{d}}^{{2}}{}{\mathrm{_Z}}{+}{4}{}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right)\right){\vee }\left({0}{<}{d}{\wedge }{c}{<}{0}{\wedge }{b}{=}{0}{\wedge }{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({27}{}{{d}}^{{2}}{}{\mathrm{_Z}}{+}{4}{}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right){<}{a}\right){\vee }\left({0}{<}{d}{\wedge }{c}{<}{0}{\wedge }{0}{<}{b}{\wedge }{b}{<}\frac{{{c}}^{{2}}}{{4}{}{d}}{\wedge }{a}{<}{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({0}{<}{d}{\wedge }{c}{<}{0}{\wedge }{0}{<}{b}{\wedge }{b}{<}\frac{{{c}}^{{2}}}{{4}{}{d}}{\wedge }{a}{=}{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({0}{<}{d}{\wedge }{c}{<}{0}{\wedge }{0}{<}{b}{\wedge }{b}{<}\frac{{{c}}^{{2}}}{{4}{}{d}}{\wedge }{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right){<}{a}{\wedge }{a}{<}{0}\right){\vee }\left({0}{<}{d}{\wedge }{c}{<}{0}{\wedge }{0}{<}{b}{\wedge }{b}{<}\frac{{{c}}^{{2}}}{{4}{}{d}}{\wedge }{a}{=}{0}\right){\vee }\left({0}{<}{d}{\wedge }{c}{<}{0}{\wedge }{0}{<}{b}{\wedge }{b}{<}\frac{{{c}}^{{2}}}{{4}{}{d}}{\wedge }{0}{<}{a}{\wedge }{a}{<}{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right)\right){\vee }\left({0}{<}{d}{\wedge }{c}{<}{0}{\wedge }{0}{<}{b}{\wedge }{b}{<}\frac{{{c}}^{{2}}}{{4}{}{d}}{\wedge }{a}{=}{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right)\right){\vee }\left({0}{<}{d}{\wedge }{c}{<}{0}{\wedge }{0}{<}{b}{\wedge }{b}{<}\frac{{{c}}^{{2}}}{{4}{}{d}}{\wedge }{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right){<}{a}\right){\vee }\left({0}{<}{d}{\wedge }{c}{<}{0}{\wedge }{b}{=}\frac{{{c}}^{{2}}}{{4}{}{d}}{\wedge }{a}{<}{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({54}{}{{d}}^{{2}}{}{\mathrm{_Z}}{-}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({0}{<}{d}{\wedge }{c}{<}{0}{\wedge }{b}{=}\frac{{{c}}^{{2}}}{{4}{}{d}}{\wedge }{a}{=}{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({54}{}{{d}}^{{2}}{}{\mathrm{_Z}}{-}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({0}{<}{d}{\wedge }{c}{<}{0}{\wedge }{b}{=}\frac{{{c}}^{{2}}}{{4}{}{d}}{\wedge }{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({54}{}{{d}}^{{2}}{}{\mathrm{_Z}}{-}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right){<}{a}{\wedge }{a}{<}{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({54}{}{{d}}^{{2}}{}{\mathrm{_Z}}{-}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right)\right){\vee }\left({0}{<}{d}{\wedge }{c}{<}{0}{\wedge }{b}{=}\frac{{{c}}^{{2}}}{{4}{}{d}}{\wedge }{a}{=}{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({54}{}{{d}}^{{2}}{}{\mathrm{_Z}}{-}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right)\right){\vee }\left({0}{<}{d}{\wedge }{c}{<}{0}{\wedge }{b}{=}\frac{{{c}}^{{2}}}{{4}{}{d}}{\wedge }{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({54}{}{{d}}^{{2}}{}{\mathrm{_Z}}{-}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right){<}{a}\right){\vee }\left({0}{<}{d}{\wedge }{c}{<}{0}{\wedge }\frac{{{c}}^{{2}}}{{4}{}{d}}{<}{b}{\wedge }{b}{<}\frac{{{c}}^{{2}}}{{3}{}{d}}{\wedge }{a}{<}{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({0}{<}{d}{\wedge }{c}{<}{0}{\wedge }\frac{{{c}}^{{2}}}{{4}{}{d}}{<}{b}{\wedge }{b}{<}\frac{{{c}}^{{2}}}{{3}{}{d}}{\wedge }{a}{=}{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({0}{<}{d}{\wedge }{c}{<}{0}{\wedge }\frac{{{c}}^{{2}}}{{4}{}{d}}{<}{b}{\wedge }{b}{<}\frac{{{c}}^{{2}}}{{3}{}{d}}{\wedge }{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right){<}{a}{\wedge }{a}{<}{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right)\right){\vee }\left({0}{<}{d}{\wedge }{c}{<}{0}{\wedge }\frac{{{c}}^{{2}}}{{4}{}{d}}{<}{b}{\wedge }{b}{<}\frac{{{c}}^{{2}}}{{3}{}{d}}{\wedge }{a}{=}{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right)\right){\vee }\left({0}{<}{d}{\wedge }{c}{<}{0}{\wedge }\frac{{{c}}^{{2}}}{{4}{}{d}}{<}{b}{\wedge }{b}{<}\frac{{{c}}^{{2}}}{{3}{}{d}}{\wedge }{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right){<}{a}{\wedge }{a}{<}{0}\right){\vee }\left({0}{<}{d}{\wedge }{c}{<}{0}{\wedge }\frac{{{c}}^{{2}}}{{4}{}{d}}{<}{b}{\wedge }{b}{<}\frac{{{c}}^{{2}}}{{3}{}{d}}{\wedge }{0}{<}{a}\right){\vee }\left({0}{<}{d}{\wedge }{c}{<}{0}{\wedge }{b}{=}\frac{{{c}}^{{2}}}{{3}{}{d}}{\wedge }{a}{<}{\mathrm{RootOf}}{}\left({729}{}{{d}}^{{4}}{}{{\mathrm{_Z}}}^{{2}}{-}{54}{}{{c}}^{{3}}{}{\mathrm{_Z}}{}{{d}}^{{2}}{+}{{c}}^{{6}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({0}{<}{d}{\wedge }{c}{<}{0}{\wedge }{b}{=}\frac{{{c}}^{{2}}}{{3}{}{d}}{\wedge }{a}{=}{\mathrm{RootOf}}{}\left({729}{}{{d}}^{{4}}{}{{\mathrm{_Z}}}^{{2}}{-}{54}{}{{c}}^{{3}}{}{\mathrm{_Z}}{}{{d}}^{{2}}{+}{{c}}^{{6}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({0}{<}{d}{\wedge }{c}{<}{0}{\wedge }{b}{=}\frac{{{c}}^{{2}}}{{3}{}{d}}{\wedge }{\mathrm{RootOf}}{}\left({729}{}{{d}}^{{4}}{}{{\mathrm{_Z}}}^{{2}}{-}{54}{}{{c}}^{{3}}{}{\mathrm{_Z}}{}{{d}}^{{2}}{+}{{c}}^{{6}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right){<}{a}{\wedge }{a}{<}{0}\right){\vee }\left({0}{<}{d}{\wedge }{c}{<}{0}{\wedge }{b}{=}\frac{{{c}}^{{2}}}{{3}{}{d}}{\wedge }{0}{<}{a}\right){\vee }\left({0}{<}{d}{\wedge }{c}{<}{0}{\wedge }\frac{{{c}}^{{2}}}{{3}{}{d}}{<}{b}{\wedge }{a}{<}{0}\right){\vee }\left({0}{<}{d}{\wedge }{c}{<}{0}{\wedge }\frac{{{c}}^{{2}}}{{3}{}{d}}{<}{b}{\wedge }{0}{<}{a}\right){\vee }\left({0}{<}{d}{\wedge }{c}{=}{0}{\wedge }{b}{<}{0}{\wedge }{a}{<}{\mathrm{RootOf}}{}\left({27}{}{{\mathrm{_Z}}}^{{2}}{}{d}{+}{4}{}{{b}}^{{3}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({0}{<}{d}{\wedge }{c}{=}{0}{\wedge }{b}{<}{0}{\wedge }{a}{=}{\mathrm{RootOf}}{}\left({27}{}{{\mathrm{_Z}}}^{{2}}{}{d}{+}{4}{}{{b}}^{{3}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({0}{<}{d}{\wedge }{c}{=}{0}{\wedge }{b}{<}{0}{\wedge }{\mathrm{RootOf}}{}\left({27}{}{{\mathrm{_Z}}}^{{2}}{}{d}{+}{4}{}{{b}}^{{3}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right){<}{a}{\wedge }{a}{<}{0}\right){\vee }\left({0}{<}{d}{\wedge }{c}{=}{0}{\wedge }{b}{<}{0}{\wedge }{a}{=}{0}\right){\vee }\left({0}{<}{d}{\wedge }{c}{=}{0}{\wedge }{b}{<}{0}{\wedge }{0}{<}{a}{\wedge }{a}{<}{\mathrm{RootOf}}{}\left({27}{}{{\mathrm{_Z}}}^{{2}}{}{d}{+}{4}{}{{b}}^{{3}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right)\right){\vee }\left({0}{<}{d}{\wedge }{c}{=}{0}{\wedge }{b}{<}{0}{\wedge }{a}{=}{\mathrm{RootOf}}{}\left({27}{}{{\mathrm{_Z}}}^{{2}}{}{d}{+}{4}{}{{b}}^{{3}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right)\right){\vee }\left({0}{<}{d}{\wedge }{c}{=}{0}{\wedge }{b}{<}{0}{\wedge }{\mathrm{RootOf}}{}\left({27}{}{{\mathrm{_Z}}}^{{2}}{}{d}{+}{4}{}{{b}}^{{3}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right){<}{a}\right){\vee }\left({0}{<}{d}{\wedge }{c}{=}{0}{\wedge }{b}{=}{0}{\wedge }{a}{<}{0}\right){\vee }\left({0}{<}{d}{\wedge }{c}{=}{0}{\wedge }{b}{=}{0}{\wedge }{0}{<}{a}\right){\vee }\left({0}{<}{d}{\wedge }{c}{=}{0}{\wedge }{0}{<}{b}{\wedge }{a}{<}{0}\right){\vee }\left({0}{<}{d}{\wedge }{c}{=}{0}{\wedge }{0}{<}{b}{\wedge }{0}{<}{a}\right){\vee }\left({0}{<}{d}{\wedge }{0}{<}{c}{\wedge }{b}{<}{0}{\wedge }{a}{<}{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({0}{<}{d}{\wedge }{0}{<}{c}{\wedge }{b}{<}{0}{\wedge }{a}{=}{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({0}{<}{d}{\wedge }{0}{<}{c}{\wedge }{b}{<}{0}{\wedge }{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right){<}{a}{\wedge }{a}{<}{0}\right){\vee }\left({0}{<}{d}{\wedge }{0}{<}{c}{\wedge }{b}{<}{0}{\wedge }{a}{=}{0}\right){\vee }\left({0}{<}{d}{\wedge }{0}{<}{c}{\wedge }{b}{<}{0}{\wedge }{0}{<}{a}{\wedge }{a}{<}{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right)\right){\vee }\left({0}{<}{d}{\wedge }{0}{<}{c}{\wedge }{b}{<}{0}{\wedge }{a}{=}{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right)\right){\vee }\left({0}{<}{d}{\wedge }{0}{<}{c}{\wedge }{b}{<}{0}{\wedge }{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right){<}{a}\right){\vee }\left({0}{<}{d}{\wedge }{0}{<}{c}{\wedge }{b}{=}{0}{\wedge }{a}{<}{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({27}{}{{d}}^{{2}}{}{\mathrm{_Z}}{+}{4}{}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({0}{<}{d}{\wedge }{0}{<}{c}{\wedge }{b}{=}{0}{\wedge }{a}{=}{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({27}{}{{d}}^{{2}}{}{\mathrm{_Z}}{+}{4}{}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({0}{<}{d}{\wedge }{0}{<}{c}{\wedge }{b}{=}{0}{\wedge }{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({27}{}{{d}}^{{2}}{}{\mathrm{_Z}}{+}{4}{}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right){<}{a}{\wedge }{a}{<}{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({27}{}{{d}}^{{2}}{}{\mathrm{_Z}}{+}{4}{}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right)\right){\vee }\left({0}{<}{d}{\wedge }{0}{<}{c}{\wedge }{b}{=}{0}{\wedge }{a}{=}{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({27}{}{{d}}^{{2}}{}{\mathrm{_Z}}{+}{4}{}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right)\right){\vee }\left({0}{<}{d}{\wedge }{0}{<}{c}{\wedge }{b}{=}{0}{\wedge }{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({27}{}{{d}}^{{2}}{}{\mathrm{_Z}}{+}{4}{}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right){<}{a}\right){\vee }\left({0}{<}{d}{\wedge }{0}{<}{c}{\wedge }{0}{<}{b}{\wedge }{b}{<}\frac{{{c}}^{{2}}}{{4}{}{d}}{\wedge }{a}{<}{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({0}{<}{d}{\wedge }{0}{<}{c}{\wedge }{0}{<}{b}{\wedge }{b}{<}\frac{{{c}}^{{2}}}{{4}{}{d}}{\wedge }{a}{=}{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({0}{<}{d}{\wedge }{0}{<}{c}{\wedge }{0}{<}{b}{\wedge }{b}{<}\frac{{{c}}^{{2}}}{{4}{}{d}}{\wedge }{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right){<}{a}{\wedge }{a}{<}{0}\right){\vee }\left({0}{<}{d}{\wedge }{0}{<}{c}{\wedge }{0}{<}{b}{\wedge }{b}{<}\frac{{{c}}^{{2}}}{{4}{}{d}}{\wedge }{a}{=}{0}\right){\vee }\left({0}{<}{d}{\wedge }{0}{<}{c}{\wedge }{0}{<}{b}{\wedge }{b}{<}\frac{{{c}}^{{2}}}{{4}{}{d}}{\wedge }{0}{<}{a}{\wedge }{a}{<}{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right)\right){\vee }\left({0}{<}{d}{\wedge }{0}{<}{c}{\wedge }{0}{<}{b}{\wedge }{b}{<}\frac{{{c}}^{{2}}}{{4}{}{d}}{\wedge }{a}{=}{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right)\right){\vee }\left({0}{<}{d}{\wedge }{0}{<}{c}{\wedge }{0}{<}{b}{\wedge }{b}{<}\frac{{{c}}^{{2}}}{{4}{}{d}}{\wedge }{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right){<}{a}\right){\vee }\left({0}{<}{d}{\wedge }{0}{<}{c}{\wedge }{b}{=}\frac{{{c}}^{{2}}}{{4}{}{d}}{\wedge }{a}{<}{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({54}{}{{d}}^{{2}}{}{\mathrm{_Z}}{-}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({0}{<}{d}{\wedge }{0}{<}{c}{\wedge }{b}{=}\frac{{{c}}^{{2}}}{{4}{}{d}}{\wedge }{a}{=}{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({54}{}{{d}}^{{2}}{}{\mathrm{_Z}}{-}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({0}{<}{d}{\wedge }{0}{<}{c}{\wedge }{b}{=}\frac{{{c}}^{{2}}}{{4}{}{d}}{\wedge }{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({54}{}{{d}}^{{2}}{}{\mathrm{_Z}}{-}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right){<}{a}{\wedge }{a}{<}{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({54}{}{{d}}^{{2}}{}{\mathrm{_Z}}{-}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right)\right){\vee }\left({0}{<}{d}{\wedge }{0}{<}{c}{\wedge }{b}{=}\frac{{{c}}^{{2}}}{{4}{}{d}}{\wedge }{a}{=}{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({54}{}{{d}}^{{2}}{}{\mathrm{_Z}}{-}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right)\right){\vee }\left({0}{<}{d}{\wedge }{0}{<}{c}{\wedge }{b}{=}\frac{{{c}}^{{2}}}{{4}{}{d}}{\wedge }{\mathrm{RootOf}}{}\left({\mathrm{_Z}}{}\left({54}{}{{d}}^{{2}}{}{\mathrm{_Z}}{-}{{c}}^{{3}}\right){,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right){<}{a}\right){\vee }\left({0}{<}{d}{\wedge }{0}{<}{c}{\wedge }\frac{{{c}}^{{2}}}{{4}{}{d}}{<}{b}{\wedge }{b}{<}\frac{{{c}}^{{2}}}{{3}{}{d}}{\wedge }{a}{<}{0}\right){\vee }\left({0}{<}{d}{\wedge }{0}{<}{c}{\wedge }\frac{{{c}}^{{2}}}{{4}{}{d}}{<}{b}{\wedge }{b}{<}\frac{{{c}}^{{2}}}{{3}{}{d}}{\wedge }{0}{<}{a}{\wedge }{a}{<}{\mathrm{RootOf}}{}\left({27}{}{{d}}^{{2}}{}{{\mathrm{_Z}}}^{{2}}{+}\left({-}{18}{}{b}{}{c}{}{d}{+}{4}{}{{c}}^{{3}}\right){}{\mathrm{_Z}}{+}{4}{}{{b}}^{{3}}{}{d}{-}{{b}}^{{2}}{}{{c}}^{{2}}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right)\right){\vee }\left({0}{<}{d}{\wedge }{0}{<}{c}{\wedge }\frac{{{c}}^{{2}}}{{4}{}{d}}\right)$