signature { automatic } theory { A(N0 & E true) }