A new decidable Horn fragment of the predicate calculus

We describe an extension of the class $\forall\exists$ of Horn formulas in the 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. If one fixes the maximum arity of predicates, our class splits into subclasses belonging to NP.