Is this generalization of Boolean algebras a variety? I'm interested in the class of structures $\langle S,\top,\neg,\wedge\rangle$ defined by the axioms:


*

*$p \wedge q=q \wedge p$

*$p \wedge (q \wedge r) = (p\wedge q)\wedge r$

*$p = p \wedge p$

*$p = \neg\neg p$

*$p \vee(q\wedge r) = (p\vee q)\wedge(p\vee r)$

*$p = p\wedge \top$

*$p \vee\top = p \vee \neg p$

*If $p \wedge q = p \vee q$ and $q \wedge r = q \vee r$, then $p \wedge r = p \vee r$.


where $p \vee q =_{df} \neg(\neg p \wedge\neg q)$. 
I have three questions about this class of structures: 
(i) Do they form a variety? 
(ii) If so, what are some equations that define them? 
(iii) If not, what is an example of a structure satisfying 1-7 but not 8? 
(I've read about Birkhoff's HSP theorem, but having only a limited background in algebra I'm not sure how to go about trying to apply it.)
Some background: These structures are a generalization of Boolean algebras in which neither the absorption laws nor $p \vee \top = \top$ are guaranteed to hold. They are isomorphic to the class of structures $\langle P, \top, \neg, \wedge\rangle$ such that, for some Boolean algebra $A = \langle S_A,\top_A,\neg_A,\wedge_A\rangle$ and bounded meet-semilattice $B = \langle S_B,\wedge_B,\top_B\rangle$,


*

*$P\subseteq S_A\times S_B$;

*$\top = \langle\top_A,\top_B\rangle\in P$; 

*$\neg: P\to P$ such that $\neg\langle a,b\rangle = \langle\neg_Aa,b\rangle$;

*$\wedge: (P\times P)\to P$ such that $\langle a,b\rangle\wedge\langle a',b'\rangle=\langle a\wedge_A a',b\wedge_B b'\rangle$.


Intuitively, we might think of $\langle a,b\rangle\in P$ as a 'proposition' with 'logical content' $a$ and 'non-logical content' $b$, where the idea is that logical contents form a Boolean algebra, propositions' non-logical contents aggregate under conjunction and are unchanged by negation, and the tautology $\top$ has minimal non-logical content. 
Update: I figured out part (iii) of my question: Kleene's weak three-valued truth table is a model of (1)-(7) but not of (8). http://en.wikipedia.org/wiki/Many-valued_logic#Bochvar.27s_internal_three-valued_logic_.28also_known_as_Kleene.27s_weak_three-valued_logic.29
 A: Counterexample: By Birkhoff's theorem, they form a variety only if they are closed under homomorphic images. Let $S = \{0,1\}\times\{0,1\}$; $\top = \langle 1,1\rangle$; $\neg\langle x,y\rangle = \langle 1-x,y\rangle$; and $\langle x,y\rangle \wedge \langle x',y'\rangle = \langle x\cdot x',y\cdot y'\rangle$. Let $S' = \{-1,0,1\}$; $\top' = 1$; $\neg'x = -x$; and $x \wedge' y = x\cdot y\cdot\textrm{max}(x,y)$. It is easy to check that $A = \langle S,\top,\neg,\wedge\rangle$ is a member of the class of structures defined above, and that $B = \langle S',\top',\neg',\wedge'\rangle$ is isomorphic to the weak Kleene truth table mentioned in the updated version of the question. Now consider the homomorphism $f: A\to B$ s.t. $f(\langle 1,1\rangle) = 1$, $f(\langle 0,1\rangle) = -1$, and $f(\langle 0,0\rangle) = f(\langle 1,0\rangle) = 0$. Since $f$ is surjective, it suffices to show that $B$ is not a member of the defined class, which it is not, since substituting $-1,0,$ and $1$ for $p,q,$ and $r$ yields a counterexample to 8. 
