Theory DLO, quantifier elimination

237 Views Asked by At

The sentence $E$ is: $\exists x\,\exists y\,\exists z\,\forall u\,((x < y) \wedge (x < z) \wedge (z < y) \wedge ((u = z) \vee (u < y) \vee (u = x)))$. We can assume that the language $A$ contains constants $\top$ and $\bot$ for true and false, respectively. How to decide whether $\mathrm{DLO}\vdash E$ or $\mathrm{DLO}\vdash \lnot E$?