I have the following formula in Z3(Python API):

from z3 import *

xOne = Real('xOne')
xTwo = Real('xTwo')
kOne = Real('kOne')
kTwo = Real('kTwo')
FETCH_xOne = Real('FETCH_xOne')
FETCH_xTwo = Real('FETCH_xTwo')
FETCH_kOne = Real('FETCH_kOne')
FETCH_kTwo = Real('FETCH_kTwo')

quantified_phi = Exists([xTwo, kOne, xOne, kTwo],
       Not(Or(3/2*FETCH_xOne + -kOne*xOne - kTwo*xTwo < xOne,
              Or(xOne <
                 3/2*FETCH_xOne + -kOne*xOne - kTwo*xTwo,
                 Or(1/5*FETCH_xTwo < xTwo,
                    Or(xTwo < 1/5*FETCH_xTwo,
                       Or(Or(Or(FETCH_kOne < kOne,
                                Or(kOne < FETCH_kOne,
                                   Or(FETCH_kTwo < kTwo,
                                      kTwo < FETCH_kTwo))),
                             Not(xTwo < FETCH_xTwo)),
                          Not(xOne < FETCH_xOne))))))))

First, I check its satisfiability:

solver = Solver()
solver.add(quantified_phi)
print(solver.check())

With the answer sat provided in no time. I guess this is normal, because quantification does not look complicated and the formula is not huge. However, when I try:

t = Tactic('qe2')
result = t(quantified_phi)

It gets stuck. Do you know why? Can I solve this or similar situations?

I tried to use other qe tactics, but they do not really produce a real elimination:

t = Tactic('qe-light')
result = t(quantified_phi)
print(result)

[[Exists([xTwo, kOne, xOne, kTwo],
         And(Not(FETCH_xOne <= xOne),
             xOne <=
             3/2*FETCH_xOne + -1*xOne*kOne + -1*kTwo*xTwo,
             3/2*FETCH_xOne + -1*xOne*kOne + -1*kTwo*xTwo <=
             xOne,
             xTwo <= 1/5*FETCH_xTwo,
             1/5*FETCH_xTwo <= xTwo,
             Not(FETCH_xTwo <= xTwo),
             FETCH_kTwo <= kTwo,
             kOne <= FETCH_kOne,
             FETCH_kOne <= kOne,
             kTwo <= FETCH_kTwo))]]

Or:

t = Tactic('qe')
result = t(quantified_phi)

[[Exists(x!44,
         And(3/2*FETCH_xOne +
             -1*FETCH_kOne*x!44 +
             -1/5*FETCH_kTwo*FETCH_xTwo <=
             x!44,
             x!44 <=
             3/2*FETCH_xOne +
             -1*FETCH_kOne*x!44 +
             -1/5*FETCH_kTwo*FETCH_xTwo,
             Not(0 <= x!44 + -1*FETCH_xOne),
             Not(FETCH_xTwo <= 0)))]]

Alternatively, are you aware of any other solver that is capable to solve such elimination?