let is_composition deps p f d =
  Formula.exists (fun d' ->
    not (Disj.equiv d d') && not (Disj.equiv (Disj.lit p) d') && (
      Formula.exists (fun d'' -> Disj.implies d d'') (
        Disj.fold (fun p f -> 
          Formula.disj (PTbl.get deps p) f
        ) d' Formula._false
      )
    )
  ) f