It is well known that Satisfiability of Horn Formulae can be checked in polynomial time using unit propagation.

But if we relax the condition for horn clauses from at most one un-negated literals to two un-nagated literals. Then is it possible to prove that satisfiability of such a formula can be checked in polynomial time of the size of the formula?

It is well known that satisfiability of Horn formulae can be checked in polynomial time using unit propagation.

But suppose we relax the condition for horn clauses from at most one un-negated literals to two un-negated literals. Then is it possible to prove that satisfiability of such a formula can be checked in time polynomial in the size of the formula?