signature { automatic } theory
{
n1 & B <>n1
}