We consider the two-pronged fork frame $F$ and the variety $\mathbf{Eq}(B_F)$ generated by its dual closure algebra $B_F$. We describe the finite projective algebras in $\mathbf{Eq}(B_F)$ and give a purely semantic proof that unification in $\mathbf{Eq}(B_F)$ is finitary and not unitary.

翻译：我们考虑双叉框架$F$及其对偶闭包代数$B_F$生成的簇$\mathbf{Eq}(B_F)$。我们刻画了$\mathbf{Eq}(B_F)$中的有限投射代数，并给出了一个纯语义证明，表明$\mathbf{Eq}(B_F)$中的统一化是有限型而非单一型。