signature { automatic } theory
{
B !N1
}