-(((p3 v (-p4 & p5)) <-> (p7 v (p4 -> p2))) <-> 
  (((p3 v (-p4 & p5)) -> (p7 v (p4 -> p2))) & 
   ((p7 v (p4 -> p2)) -> (p3 v (-p4 & p5)))))