MAYBE

Proof:
ConCon could not decide confluence of the system.
\cite{SMI95}, Corollary 4.7 or 5.3 do not apply.
Some critical pairs are not trivial and ConCon could not decide whether those all are infeasible.
ring($2, tail($5), sndsplit($6, app(map_f(two, head($5)), $1)), cons(fstsplit($6, app(map_f(two, head($5)), $1)), $3), $4, $6) = ring($2, $5, $1, $3, sndsplit($6, $4), $6) <= leq($6, length($4)) = true, empty(fstsplit($6, $4)) = false, leq($6, length($1)) = false, empty(fstsplit($6, app(map_f(two, head($5)), $1))) = false:
For all conditions c 'tcap(c.lhs)' is unifiable with c.rhs.