signature { automatic } theory
{
N1: N2;
N1: [R1] P1;
N2: <R1> !P1
}