Is NAE-HORN-SAT in P or NP-hard? I am interested to know the complexity of the NAE-HORN-SAT problem
(not all equal).  We know that HORNSAT is $\mathsf{P}$-complete, but
on the other hand, NAE-SAT is $\mathsf{NP}$-complete.  I want to know
what can we say about NAE-HORN-SAT problem.  Let me define the problem
formally:


  Given: One Boolean formula $\phi$ is given to us in CNF where each
  clause has at most one positive literal (HORN-property).
  Question: Is there any assignment for the input variables of
  $\phi$ such that any clause has at least one False and at least one
  True literal (NAE-property) ?


N.B.:


Positive literal: any variable directly,
Negative literal: negation of any variable.
True literal: literal is assigned to Boolean True by any assignment,
False literal: literal is assigned to Boolean False by any assignment.


According to Schaefer's dichotomy theorem, this problem must be either
in $\mathsf{P}$ or $\mathsf{NP}$-complete.  I can just find one
polynomial reduction from HORNSAT to this problem, which proves
actually nothing.  Is there a polynomial time algorithm to solve this
problem?

Or, is there any way to prove this problem to be $\mathsf{NP}$-hard?
Any thoughts about this ?
Your problem, NAE-HORN-SAT is $NP$-complete. Monotone NAE-SAT is $NP$-complete and it is a special case of your NAE-HORN-SAT. Literals in monotone SAT formula are either all positive or all negative.

Take any instance of Monotone NAE-SAT problem (all its literals are negative) then this formula is an instance of NAE-HORN-SAT problem.