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)$ 中的统一化是有限型而非单一型。