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