signature { automatic } theory

{
  !([R1](P1 | !P1))
}