( 
   (@ c1 c2 & @ c1 ((p v @ c2 p1) -> p3))
    & 
   - (@ c2 (p v @ c2 p1) -> @c1 p3)
  )