{ satisfiable }
conj (
      ([R1](<R3>p1 v p3) <-> [R3](p3 -> <R2>-p3)),
      [R2](p1 -> <R2>(p1 <-> disj (p3, p4, -p5))),
      [R1][R2][R3]disj (p1, -p3, -p5)
     )