The CDA solvability problem is decidable (paper §6.4): the decision reduces to checking that all components of the companion shuffle automaton's recognised series are commutative, each decided by $ShuffleCommutativityDecidable$ (the meta-theorem applied to the effective prevariety of shuffle-finite series).