begin
!N1 v !A(!N1 v !P1);
N1 v !N1:(!P1 v !N1);
P1 v [R1](N1 v P1);
!P1 v [R1](!P1 v !N1);
!N1 v A(!P1 v !N1)
end