begin
[R1](<R3>p1 v p3) <--> [R3](p3 --> <R2>!p3);
[R2](p1 --> <R2>(p1 <--> (p3 v p4 v !p5)));
[R1][R2][R3](p1 v !p3 v !p5)
end