signature { automatic } theory

{
   !(((<R1>P1) | (<R1>P2)) --> (<R1>(P1 | P2)))
}