begin

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

end