Consider a propositional language over the set of propositional variables $\{p^+,p^-,q^+,q^-,\ldots\}$ and connectives $\{\wedge,\vee,\rightarrow,\equiv\}$ (conjunction, disjunction, implication, equivalence). We call a formula $\phi$ monotone if it only contains $\wedge$ and $\vee$. Additionally, we call $\phi^\partial$ the dual of $\phi$ if all $\wedge$'s are swapped for $\vee$'s (and vice versa) and all $p^+$'s with $p^-$'s (and vice versa).
E.g., $p^+\wedge(q^-\vee p^-)$ is dual to $p^-\vee(q^+\wedge p^+)$.
Now let $\phi$ and $\chi$ be two monotone formulas. What is the complexity of determining whether the following formula is valid in classical logic? $$(\phi\equiv\phi^\partial)\rightarrow(\chi\equiv\chi^\partial)$$
It seems that it should be in $\mathsf{coNP}$ but showing hardness turned out to be not straightforward — I did not find a reduction from the classical validity…