Complexity of deciding Tarski algebra

Let a formula of Tarski algebra contain k atomic subformulas of the kind (fi ⩾ 0), 1 ⩽ t ⩽ k, where the polynomials fi ∈ ℤ [X1,...,Xn] have degrees deg (fi) < d, let 2M be an upper bound for the absolute value of every coeffieient of the polynomials fi, 1 ⩽ i ⩽ k, let a ⩽ n be the number of quantifier alternations in the prenex form of the formula. A decision method for Tarski algebra is described with the running time polynomial in M(kd)(O(n))4n−2. Previously known decision procedures have a time complexity polynomial in (Mkd)2O(n)