We describe an extension of the class ∀∃ of Horn formulas in predicate calculus. We prove the decidability of this class. We describe complexity characteristics such that fixing them splits this extended class into polynomially decidable subclasses. Fixing the maximum arity of predicates splits our class into subclasses belonging to NP. Bibliography: 11 titles.