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