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(sndsplit($6, $2), cons(fstsplit($6, $2), $5), $1, $3, $4, $6) = ring($2, $5, sndsplit($6, $1), cons(fstsplit($6, $1), $3), $4, $6) <= leq($6, length($1)) = true, empty(fstsplit($6, $1)) = false, empty(fstsplit($6, $2)) = false:
For all conditions c 'tcap(c.lhs)' is unifiable with c.rhs.
\cite{GNG13}, Theorem 9 does not apply.
System R transformed to optimized U(R).
Call external tool:
csi - trs 30
Input:
  fstsplit(0, x) -> nil
  fstsplit(s(n), nil) -> nil
  fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
  sndsplit(0, x) -> x
  sndsplit(s(n), nil) -> nil
  sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
  empty(nil) -> true
  empty(cons(h, t)) -> false
  leq(0, m) -> true
  leq(s(n), 0) -> false
  leq(s(n), s(m)) -> leq(n, m)
  length(nil) -> 0
  length(cons(h, t)) -> s(length(t))
  app(nil, x) -> x
  app(cons(h, t), x) -> cons(h, app(t, x))
  map_f(pid, nil) -> nil
  map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
  head(cons(h, t)) -> h
  tail(cons(h, t)) -> t
  ?1(false, st_2, in_2, st_3, m, st_1, in_3) -> ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
  ring(st_1, in_2, st_2, in_3, st_3, m) -> ?1(empty(fstsplit(m, st_1)), st_2, in_2, st_3, m, st_1, in_3)
  ?5(false, st_2, in_2, st_3, m, st_1, in_3) -> ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
  ?6(true, st_2, in_2, st_3, m, st_1, in_3) -> ?5(empty(fstsplit(m, st_2)), st_2, in_2, st_3, m, st_1, in_3)
  ring(st_1, in_2, st_2, in_3, st_3, m) -> ?6(leq(m, length(st_2)), st_2, in_2, st_3, m, st_1, in_3)
  ?4(false, st_2, in_2, st_3, m, st_1, in_3) -> ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
  ?6(false, st_2, in_2, st_3, m, st_1, in_3) -> ?4(empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))), st_2, in_2, st_3, m, st_1, in_3)
  ?3(true, st_2, in_2, st_3, m, st_1, in_3) -> ring(st_1, tail(in_2), st_2, in_3, st_3, m)
  ring(st_1, in_2, st_2, in_3, st_3, m) -> ?3(empty(map_f(two, head(in_2))), st_2, in_2, st_3, m, st_1, in_3)
  ?8(false, st_2, in_2, st_3, m, st_1, in_3) -> ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
  ?9(true, st_2, in_2, st_3, m, st_1, in_3) -> ?8(empty(fstsplit(m, st_3)), st_2, in_2, st_3, m, st_1, in_3)
  ring(st_1, in_2, st_2, in_3, st_3, m) -> ?9(leq(m, length(st_3)), st_2, in_2, st_3, m, st_1, in_3)
  ?7(false, st_2, in_2, st_3, m, st_1, in_3) -> ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
  ?9(false, st_2, in_2, st_3, m, st_1, in_3) -> ?7(empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))), st_2, in_2, st_3, m, st_1, in_3)
  ?2(true, st_2, in_2, st_3, m, st_1, in_3) -> ring(st_1, in_2, st_2, tail(in_3), st_3, m)
  ring(st_1, in_2, st_2, in_3, st_3, m) -> ?2(empty(map_f(three, head(in_3))), st_2, in_2, st_3, m, st_1, in_3)

The external tool could not decide confluence.
\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, $5, $1, tail($3), sndsplit($6, app(map_f(three, head($3)), $4)), $6) = ring($2, $5, sndsplit($6, $1), cons(fstsplit($6, $1), $3), $4, $6) <= leq($6, length($1)) = true, empty(fstsplit($6, $1)) = false, leq($6, length($4)) = false, empty(fstsplit($6, app(map_f(three, head($3)), $4))) = false:
For all conditions c 'tcap(c.lhs)' is unifiable with c.rhs.