signature { automatic } theory
{
n3:[R3](down (N1 [R1]([R1]( down( N2 (N1:<R1>N2)))))) ;
n3:<R3>n1;
n3:<R3>n2;
n3:<R3>n3;
n1:<R1>n2;
n2:<R1>n3;
n1:!<R1>n3
}