Convert propositional logic to CNF

Question

Q: a<->(b->d)&a<->(c->d)&d&c|!(d&d)

Steps I've tried:

d&c|!(d&d) -> (c&!d)

Using SNF:

1.) a<->(b->d) -> (a|b&!d) & (!a|!b|d)

2.) a<->(c->d) -> (a|c&!d) & (!a|!c|d)

(a|b&!d)&(!a|!b|d)&(a|c&!d)&(!a|!c|d)&(c&!d)

The accepted answer is (c|!d)&(d|!a|!b)

I notice that the formula of the accepted answer exists in my last stage but I cannot figure out what further simplifications can I proceed with.

Comments

d&c|!(d&d) is not a subformula of your formula, note that conjunction binds stronger than disjunction.

Answer 1

Why not proceeding this way (using Shannon decomposition)?

Note that we have (x⇒φ|ψ) ⇔ (¬x ∨ φ) ∧ (x ∨ ψ)

    a<->(b->d)&a<->(c->d)&d&c|!(d&d)

    <=> (¬d ∨ (a<->(b->1)&a<->(c->1)&1&c|!(1&1))) ∧ (d ∨ (a<->(b->0)&a<->(c->0)&0&c|!(0&0)))

    <=> (¬d ∨ (a<->a<->c)) ∧ (d ∨ (a<->(!b)&a))

    <=> (¬d ∨ c) ∧ (d ∨ (a<->!b&a))

    <=> (¬d ∨ c) ∧ (d ∨ (¬a ∨ (1<->!b&1)) ∧ (a ∨ (0<->!b&0)))

    <=> (¬d ∨ c) ∧ (d ∨ (¬a ∨ !b) ∧ (a ∨ 1))

    <=> (¬d ∨ c) ∧ (d ∨ (¬a ∨ !b) )

    <=> (¬d ∨ c) ∧ (d ∨ ¬a ∨ !b )

Comments

It didn't occur to me to try Shannon Decomp from the get go. That's why I tried to simplify first. It's clear now.