MAYBE Proof: ConCon could not decide confluence of the system. \cite{ALS94}, Theorem 4.1 does not apply. ConCon could not decide whether all critical pairs are joinable or not. ring($2, $5, $1, tail($3), $4, $6) = ring($2, tail($5), $1, $3, $4, $6) <= empty(map_f(two, head($5))) = true, empty(map_f(three, head($3))) = true: For all conditions c 'tcap(c.lhs)' is unifiable with c.rhs.