TRS:
 {                              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,
           ring(st_1, in_2, st_2, in_3, st_3, m) -> if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1))),
  if_1(st_1, in_2, st_2, in_3, st_3, m, false()) -> 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) -> if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2))),
   if_2(st_1, in_2, st_2, in_3, st_3, m, true()) -> if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2))),
  if_3(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m),
  if_2(st_1, in_2, st_2, in_3, st_3, m, false()) -> if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two(), head(in_2)), st_2)))),
  if_4(st_1, in_2, st_2, in_3, st_3, m, false()) -> 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),
           ring(st_1, in_2, st_2, in_3, st_3, m) -> if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two(), head(in_2)))),
   if_5(st_1, in_2, st_2, in_3, st_3, m, true()) -> 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) -> if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3))),
   if_6(st_1, in_2, st_2, in_3, st_3, m, true()) -> if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3))),
  if_7(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m),
  if_6(st_1, in_2, st_2, in_3, st_3, m, false()) -> if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three(), head(in_3)), st_3)))),
  if_8(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three(), head(in_3)), st_3)), m),
           ring(st_1, in_2, st_2, in_3, st_3, m) -> if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three(), head(in_3)))),
   if_9(st_1, in_2, st_2, in_3, st_3, m, true()) -> ring(st_1, in_2, st_2, tail(in_3), st_3, m)}
 Fail