MAYBE

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict 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)))
  , 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)))
  , 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))))
  , 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)))
  , 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_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)
  , 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_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_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_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)
  , 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)
  , 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_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_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_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)
  , 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) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following dependency tuples:

Strict DPs:
  { fstsplit^#(0(), x) -> c_1()
  , fstsplit^#(s(n), nil()) -> c_2()
  , fstsplit^#(s(n), cons(h, t)) -> c_3(fstsplit^#(n, t))
  , sndsplit^#(0(), x) -> c_4()
  , sndsplit^#(s(n), nil()) -> c_5()
  , sndsplit^#(s(n), cons(h, t)) -> c_6(sndsplit^#(n, t))
  , empty^#(nil()) -> c_7()
  , empty^#(cons(h, t)) -> c_8()
  , leq^#(0(), m) -> c_9()
  , leq^#(s(n), 0()) -> c_10()
  , leq^#(s(n), s(m)) -> c_11(leq^#(n, m))
  , length^#(nil()) -> c_12()
  , length^#(cons(h, t)) -> c_13(length^#(t))
  , app^#(nil(), x) -> c_14()
  , app^#(cons(h, t), x) -> c_15(app^#(t, x))
  , map_f^#(pid, nil()) -> c_16()
  , map_f^#(pid, cons(h, t)) ->
    c_17(app^#(f(pid, h), map_f(pid, t)), map_f^#(pid, t))
  , head^#(cons(h, t)) -> c_18()
  , tail^#(cons(h, t)) -> c_19()
  , ring^#(st_1, in_2, st_2, in_3, st_3, m) ->
    c_20(if_1^#(st_1,
                in_2,
                st_2,
                in_3,
                st_3,
                m,
                empty(fstsplit(m, st_1))),
         empty^#(fstsplit(m, st_1)),
         fstsplit^#(m, st_1))
  , ring^#(st_1, in_2, st_2, in_3, st_3, m) ->
    c_21(if_2^#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2))),
         leq^#(m, length(st_2)),
         length^#(st_2))
  , ring^#(st_1, in_2, st_2, in_3, st_3, m) ->
    c_22(if_5^#(st_1,
                in_2,
                st_2,
                in_3,
                st_3,
                m,
                empty(map_f(two(), head(in_2)))),
         empty^#(map_f(two(), head(in_2))),
         map_f^#(two(), head(in_2)),
         head^#(in_2))
  , ring^#(st_1, in_2, st_2, in_3, st_3, m) ->
    c_23(if_6^#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3))),
         leq^#(m, length(st_3)),
         length^#(st_3))
  , ring^#(st_1, in_2, st_2, in_3, st_3, m) ->
    c_24(if_9^#(st_1,
                in_2,
                st_2,
                in_3,
                st_3,
                m,
                empty(map_f(three(), head(in_3)))),
         empty^#(map_f(three(), head(in_3))),
         map_f^#(three(), head(in_3)),
         head^#(in_3))
  , if_1^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
    c_25(ring^#(sndsplit(m, st_1),
                cons(fstsplit(m, st_1), in_2),
                st_2,
                in_3,
                st_3,
                m),
         sndsplit^#(m, st_1),
         fstsplit^#(m, st_1))
  , if_2^#(st_1, in_2, st_2, in_3, st_3, m, true()) ->
    c_26(if_3^#(st_1,
                in_2,
                st_2,
                in_3,
                st_3,
                m,
                empty(fstsplit(m, st_2))),
         empty^#(fstsplit(m, st_2)),
         fstsplit^#(m, st_2))
  , if_2^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
    c_27(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)))),
         empty^#(fstsplit(m, app(map_f(two(), head(in_2)), st_2))),
         fstsplit^#(m, app(map_f(two(), head(in_2)), st_2)),
         app^#(map_f(two(), head(in_2)), st_2),
         map_f^#(two(), head(in_2)),
         head^#(in_2))
  , if_5^#(st_1, in_2, st_2, in_3, st_3, m, true()) ->
    c_30(ring^#(st_1, tail(in_2), st_2, in_3, st_3, m), tail^#(in_2))
  , if_6^#(st_1, in_2, st_2, in_3, st_3, m, true()) ->
    c_31(if_7^#(st_1,
                in_2,
                st_2,
                in_3,
                st_3,
                m,
                empty(fstsplit(m, st_3))),
         empty^#(fstsplit(m, st_3)),
         fstsplit^#(m, st_3))
  , if_6^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
    c_32(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)))),
         empty^#(fstsplit(m, app(map_f(three(), head(in_3)), st_3))),
         fstsplit^#(m, app(map_f(three(), head(in_3)), st_3)),
         app^#(map_f(three(), head(in_3)), st_3),
         map_f^#(three(), head(in_3)),
         head^#(in_3))
  , if_9^#(st_1, in_2, st_2, in_3, st_3, m, true()) ->
    c_35(ring^#(st_1, in_2, st_2, tail(in_3), st_3, m), tail^#(in_3))
  , if_3^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
    c_28(ring^#(st_1,
                in_2,
                sndsplit(m, st_2),
                cons(fstsplit(m, st_2), in_3),
                st_3,
                m),
         sndsplit^#(m, st_2),
         fstsplit^#(m, st_2))
  , if_4^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
    c_29(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),
         tail^#(in_2),
         sndsplit^#(m, app(map_f(two(), head(in_2)), st_2)),
         app^#(map_f(two(), head(in_2)), st_2),
         map_f^#(two(), head(in_2)),
         head^#(in_2),
         fstsplit^#(m, app(map_f(two(), head(in_2)), st_2)),
         app^#(map_f(two(), head(in_2)), st_2),
         map_f^#(two(), head(in_2)),
         head^#(in_2))
  , if_7^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
    c_33(ring^#(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m),
         sndsplit^#(m, st_3))
  , if_8^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
    c_34(ring^#(st_1,
                in_2,
                st_2,
                tail(in_3),
                sndsplit(m, app(map_f(three(), head(in_3)), st_3)),
                m),
         tail^#(in_3),
         sndsplit^#(m, app(map_f(three(), head(in_3)), st_3)),
         app^#(map_f(three(), head(in_3)), st_3),
         map_f^#(three(), head(in_3)),
         head^#(in_3)) }

and mark the set of starting terms.

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { fstsplit^#(0(), x) -> c_1()
  , fstsplit^#(s(n), nil()) -> c_2()
  , fstsplit^#(s(n), cons(h, t)) -> c_3(fstsplit^#(n, t))
  , sndsplit^#(0(), x) -> c_4()
  , sndsplit^#(s(n), nil()) -> c_5()
  , sndsplit^#(s(n), cons(h, t)) -> c_6(sndsplit^#(n, t))
  , empty^#(nil()) -> c_7()
  , empty^#(cons(h, t)) -> c_8()
  , leq^#(0(), m) -> c_9()
  , leq^#(s(n), 0()) -> c_10()
  , leq^#(s(n), s(m)) -> c_11(leq^#(n, m))
  , length^#(nil()) -> c_12()
  , length^#(cons(h, t)) -> c_13(length^#(t))
  , app^#(nil(), x) -> c_14()
  , app^#(cons(h, t), x) -> c_15(app^#(t, x))
  , map_f^#(pid, nil()) -> c_16()
  , map_f^#(pid, cons(h, t)) ->
    c_17(app^#(f(pid, h), map_f(pid, t)), map_f^#(pid, t))
  , head^#(cons(h, t)) -> c_18()
  , tail^#(cons(h, t)) -> c_19()
  , ring^#(st_1, in_2, st_2, in_3, st_3, m) ->
    c_20(if_1^#(st_1,
                in_2,
                st_2,
                in_3,
                st_3,
                m,
                empty(fstsplit(m, st_1))),
         empty^#(fstsplit(m, st_1)),
         fstsplit^#(m, st_1))
  , ring^#(st_1, in_2, st_2, in_3, st_3, m) ->
    c_21(if_2^#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2))),
         leq^#(m, length(st_2)),
         length^#(st_2))
  , ring^#(st_1, in_2, st_2, in_3, st_3, m) ->
    c_22(if_5^#(st_1,
                in_2,
                st_2,
                in_3,
                st_3,
                m,
                empty(map_f(two(), head(in_2)))),
         empty^#(map_f(two(), head(in_2))),
         map_f^#(two(), head(in_2)),
         head^#(in_2))
  , ring^#(st_1, in_2, st_2, in_3, st_3, m) ->
    c_23(if_6^#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3))),
         leq^#(m, length(st_3)),
         length^#(st_3))
  , ring^#(st_1, in_2, st_2, in_3, st_3, m) ->
    c_24(if_9^#(st_1,
                in_2,
                st_2,
                in_3,
                st_3,
                m,
                empty(map_f(three(), head(in_3)))),
         empty^#(map_f(three(), head(in_3))),
         map_f^#(three(), head(in_3)),
         head^#(in_3))
  , if_1^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
    c_25(ring^#(sndsplit(m, st_1),
                cons(fstsplit(m, st_1), in_2),
                st_2,
                in_3,
                st_3,
                m),
         sndsplit^#(m, st_1),
         fstsplit^#(m, st_1))
  , if_2^#(st_1, in_2, st_2, in_3, st_3, m, true()) ->
    c_26(if_3^#(st_1,
                in_2,
                st_2,
                in_3,
                st_3,
                m,
                empty(fstsplit(m, st_2))),
         empty^#(fstsplit(m, st_2)),
         fstsplit^#(m, st_2))
  , if_2^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
    c_27(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)))),
         empty^#(fstsplit(m, app(map_f(two(), head(in_2)), st_2))),
         fstsplit^#(m, app(map_f(two(), head(in_2)), st_2)),
         app^#(map_f(two(), head(in_2)), st_2),
         map_f^#(two(), head(in_2)),
         head^#(in_2))
  , if_5^#(st_1, in_2, st_2, in_3, st_3, m, true()) ->
    c_30(ring^#(st_1, tail(in_2), st_2, in_3, st_3, m), tail^#(in_2))
  , if_6^#(st_1, in_2, st_2, in_3, st_3, m, true()) ->
    c_31(if_7^#(st_1,
                in_2,
                st_2,
                in_3,
                st_3,
                m,
                empty(fstsplit(m, st_3))),
         empty^#(fstsplit(m, st_3)),
         fstsplit^#(m, st_3))
  , if_6^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
    c_32(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)))),
         empty^#(fstsplit(m, app(map_f(three(), head(in_3)), st_3))),
         fstsplit^#(m, app(map_f(three(), head(in_3)), st_3)),
         app^#(map_f(three(), head(in_3)), st_3),
         map_f^#(three(), head(in_3)),
         head^#(in_3))
  , if_9^#(st_1, in_2, st_2, in_3, st_3, m, true()) ->
    c_35(ring^#(st_1, in_2, st_2, tail(in_3), st_3, m), tail^#(in_3))
  , if_3^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
    c_28(ring^#(st_1,
                in_2,
                sndsplit(m, st_2),
                cons(fstsplit(m, st_2), in_3),
                st_3,
                m),
         sndsplit^#(m, st_2),
         fstsplit^#(m, st_2))
  , if_4^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
    c_29(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),
         tail^#(in_2),
         sndsplit^#(m, app(map_f(two(), head(in_2)), st_2)),
         app^#(map_f(two(), head(in_2)), st_2),
         map_f^#(two(), head(in_2)),
         head^#(in_2),
         fstsplit^#(m, app(map_f(two(), head(in_2)), st_2)),
         app^#(map_f(two(), head(in_2)), st_2),
         map_f^#(two(), head(in_2)),
         head^#(in_2))
  , if_7^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
    c_33(ring^#(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m),
         sndsplit^#(m, st_3))
  , if_8^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
    c_34(ring^#(st_1,
                in_2,
                st_2,
                tail(in_3),
                sndsplit(m, app(map_f(three(), head(in_3)), st_3)),
                m),
         tail^#(in_3),
         sndsplit^#(m, app(map_f(three(), head(in_3)), st_3)),
         app^#(map_f(three(), head(in_3)), st_3),
         map_f^#(three(), head(in_3)),
         head^#(in_3)) }
Weak 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)))
  , 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)))
  , 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))))
  , 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)))
  , 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_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)
  , 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_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_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_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)
  , 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)
  , 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_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_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_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)
  , 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) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We estimate the number of application of
{1,2,4,5,7,8,9,10,12,14,16,18,19} by applications of
Pre({1,2,4,5,7,8,9,10,12,14,16,18,19}) =
{3,6,11,13,15,17,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35}.
Here rules are labeled as follows:

  DPs:
    { 1: fstsplit^#(0(), x) -> c_1()
    , 2: fstsplit^#(s(n), nil()) -> c_2()
    , 3: fstsplit^#(s(n), cons(h, t)) -> c_3(fstsplit^#(n, t))
    , 4: sndsplit^#(0(), x) -> c_4()
    , 5: sndsplit^#(s(n), nil()) -> c_5()
    , 6: sndsplit^#(s(n), cons(h, t)) -> c_6(sndsplit^#(n, t))
    , 7: empty^#(nil()) -> c_7()
    , 8: empty^#(cons(h, t)) -> c_8()
    , 9: leq^#(0(), m) -> c_9()
    , 10: leq^#(s(n), 0()) -> c_10()
    , 11: leq^#(s(n), s(m)) -> c_11(leq^#(n, m))
    , 12: length^#(nil()) -> c_12()
    , 13: length^#(cons(h, t)) -> c_13(length^#(t))
    , 14: app^#(nil(), x) -> c_14()
    , 15: app^#(cons(h, t), x) -> c_15(app^#(t, x))
    , 16: map_f^#(pid, nil()) -> c_16()
    , 17: map_f^#(pid, cons(h, t)) ->
          c_17(app^#(f(pid, h), map_f(pid, t)), map_f^#(pid, t))
    , 18: head^#(cons(h, t)) -> c_18()
    , 19: tail^#(cons(h, t)) -> c_19()
    , 20: ring^#(st_1, in_2, st_2, in_3, st_3, m) ->
          c_20(if_1^#(st_1,
                      in_2,
                      st_2,
                      in_3,
                      st_3,
                      m,
                      empty(fstsplit(m, st_1))),
               empty^#(fstsplit(m, st_1)),
               fstsplit^#(m, st_1))
    , 21: ring^#(st_1, in_2, st_2, in_3, st_3, m) ->
          c_21(if_2^#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2))),
               leq^#(m, length(st_2)),
               length^#(st_2))
    , 22: ring^#(st_1, in_2, st_2, in_3, st_3, m) ->
          c_22(if_5^#(st_1,
                      in_2,
                      st_2,
                      in_3,
                      st_3,
                      m,
                      empty(map_f(two(), head(in_2)))),
               empty^#(map_f(two(), head(in_2))),
               map_f^#(two(), head(in_2)),
               head^#(in_2))
    , 23: ring^#(st_1, in_2, st_2, in_3, st_3, m) ->
          c_23(if_6^#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3))),
               leq^#(m, length(st_3)),
               length^#(st_3))
    , 24: ring^#(st_1, in_2, st_2, in_3, st_3, m) ->
          c_24(if_9^#(st_1,
                      in_2,
                      st_2,
                      in_3,
                      st_3,
                      m,
                      empty(map_f(three(), head(in_3)))),
               empty^#(map_f(three(), head(in_3))),
               map_f^#(three(), head(in_3)),
               head^#(in_3))
    , 25: if_1^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
          c_25(ring^#(sndsplit(m, st_1),
                      cons(fstsplit(m, st_1), in_2),
                      st_2,
                      in_3,
                      st_3,
                      m),
               sndsplit^#(m, st_1),
               fstsplit^#(m, st_1))
    , 26: if_2^#(st_1, in_2, st_2, in_3, st_3, m, true()) ->
          c_26(if_3^#(st_1,
                      in_2,
                      st_2,
                      in_3,
                      st_3,
                      m,
                      empty(fstsplit(m, st_2))),
               empty^#(fstsplit(m, st_2)),
               fstsplit^#(m, st_2))
    , 27: if_2^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
          c_27(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)))),
               empty^#(fstsplit(m, app(map_f(two(), head(in_2)), st_2))),
               fstsplit^#(m, app(map_f(two(), head(in_2)), st_2)),
               app^#(map_f(two(), head(in_2)), st_2),
               map_f^#(two(), head(in_2)),
               head^#(in_2))
    , 28: if_5^#(st_1, in_2, st_2, in_3, st_3, m, true()) ->
          c_30(ring^#(st_1, tail(in_2), st_2, in_3, st_3, m), tail^#(in_2))
    , 29: if_6^#(st_1, in_2, st_2, in_3, st_3, m, true()) ->
          c_31(if_7^#(st_1,
                      in_2,
                      st_2,
                      in_3,
                      st_3,
                      m,
                      empty(fstsplit(m, st_3))),
               empty^#(fstsplit(m, st_3)),
               fstsplit^#(m, st_3))
    , 30: if_6^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
          c_32(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)))),
               empty^#(fstsplit(m, app(map_f(three(), head(in_3)), st_3))),
               fstsplit^#(m, app(map_f(three(), head(in_3)), st_3)),
               app^#(map_f(three(), head(in_3)), st_3),
               map_f^#(three(), head(in_3)),
               head^#(in_3))
    , 31: if_9^#(st_1, in_2, st_2, in_3, st_3, m, true()) ->
          c_35(ring^#(st_1, in_2, st_2, tail(in_3), st_3, m), tail^#(in_3))
    , 32: if_3^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
          c_28(ring^#(st_1,
                      in_2,
                      sndsplit(m, st_2),
                      cons(fstsplit(m, st_2), in_3),
                      st_3,
                      m),
               sndsplit^#(m, st_2),
               fstsplit^#(m, st_2))
    , 33: if_4^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
          c_29(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),
               tail^#(in_2),
               sndsplit^#(m, app(map_f(two(), head(in_2)), st_2)),
               app^#(map_f(two(), head(in_2)), st_2),
               map_f^#(two(), head(in_2)),
               head^#(in_2),
               fstsplit^#(m, app(map_f(two(), head(in_2)), st_2)),
               app^#(map_f(two(), head(in_2)), st_2),
               map_f^#(two(), head(in_2)),
               head^#(in_2))
    , 34: if_7^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
          c_33(ring^#(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m),
               sndsplit^#(m, st_3))
    , 35: if_8^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
          c_34(ring^#(st_1,
                      in_2,
                      st_2,
                      tail(in_3),
                      sndsplit(m, app(map_f(three(), head(in_3)), st_3)),
                      m),
               tail^#(in_3),
               sndsplit^#(m, app(map_f(three(), head(in_3)), st_3)),
               app^#(map_f(three(), head(in_3)), st_3),
               map_f^#(three(), head(in_3)),
               head^#(in_3)) }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { fstsplit^#(s(n), cons(h, t)) -> c_3(fstsplit^#(n, t))
  , sndsplit^#(s(n), cons(h, t)) -> c_6(sndsplit^#(n, t))
  , leq^#(s(n), s(m)) -> c_11(leq^#(n, m))
  , length^#(cons(h, t)) -> c_13(length^#(t))
  , app^#(cons(h, t), x) -> c_15(app^#(t, x))
  , map_f^#(pid, cons(h, t)) ->
    c_17(app^#(f(pid, h), map_f(pid, t)), map_f^#(pid, t))
  , ring^#(st_1, in_2, st_2, in_3, st_3, m) ->
    c_20(if_1^#(st_1,
                in_2,
                st_2,
                in_3,
                st_3,
                m,
                empty(fstsplit(m, st_1))),
         empty^#(fstsplit(m, st_1)),
         fstsplit^#(m, st_1))
  , ring^#(st_1, in_2, st_2, in_3, st_3, m) ->
    c_21(if_2^#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2))),
         leq^#(m, length(st_2)),
         length^#(st_2))
  , ring^#(st_1, in_2, st_2, in_3, st_3, m) ->
    c_22(if_5^#(st_1,
                in_2,
                st_2,
                in_3,
                st_3,
                m,
                empty(map_f(two(), head(in_2)))),
         empty^#(map_f(two(), head(in_2))),
         map_f^#(two(), head(in_2)),
         head^#(in_2))
  , ring^#(st_1, in_2, st_2, in_3, st_3, m) ->
    c_23(if_6^#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3))),
         leq^#(m, length(st_3)),
         length^#(st_3))
  , ring^#(st_1, in_2, st_2, in_3, st_3, m) ->
    c_24(if_9^#(st_1,
                in_2,
                st_2,
                in_3,
                st_3,
                m,
                empty(map_f(three(), head(in_3)))),
         empty^#(map_f(three(), head(in_3))),
         map_f^#(three(), head(in_3)),
         head^#(in_3))
  , if_1^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
    c_25(ring^#(sndsplit(m, st_1),
                cons(fstsplit(m, st_1), in_2),
                st_2,
                in_3,
                st_3,
                m),
         sndsplit^#(m, st_1),
         fstsplit^#(m, st_1))
  , if_2^#(st_1, in_2, st_2, in_3, st_3, m, true()) ->
    c_26(if_3^#(st_1,
                in_2,
                st_2,
                in_3,
                st_3,
                m,
                empty(fstsplit(m, st_2))),
         empty^#(fstsplit(m, st_2)),
         fstsplit^#(m, st_2))
  , if_2^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
    c_27(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)))),
         empty^#(fstsplit(m, app(map_f(two(), head(in_2)), st_2))),
         fstsplit^#(m, app(map_f(two(), head(in_2)), st_2)),
         app^#(map_f(two(), head(in_2)), st_2),
         map_f^#(two(), head(in_2)),
         head^#(in_2))
  , if_5^#(st_1, in_2, st_2, in_3, st_3, m, true()) ->
    c_30(ring^#(st_1, tail(in_2), st_2, in_3, st_3, m), tail^#(in_2))
  , if_6^#(st_1, in_2, st_2, in_3, st_3, m, true()) ->
    c_31(if_7^#(st_1,
                in_2,
                st_2,
                in_3,
                st_3,
                m,
                empty(fstsplit(m, st_3))),
         empty^#(fstsplit(m, st_3)),
         fstsplit^#(m, st_3))
  , if_6^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
    c_32(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)))),
         empty^#(fstsplit(m, app(map_f(three(), head(in_3)), st_3))),
         fstsplit^#(m, app(map_f(three(), head(in_3)), st_3)),
         app^#(map_f(three(), head(in_3)), st_3),
         map_f^#(three(), head(in_3)),
         head^#(in_3))
  , if_9^#(st_1, in_2, st_2, in_3, st_3, m, true()) ->
    c_35(ring^#(st_1, in_2, st_2, tail(in_3), st_3, m), tail^#(in_3))
  , if_3^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
    c_28(ring^#(st_1,
                in_2,
                sndsplit(m, st_2),
                cons(fstsplit(m, st_2), in_3),
                st_3,
                m),
         sndsplit^#(m, st_2),
         fstsplit^#(m, st_2))
  , if_4^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
    c_29(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),
         tail^#(in_2),
         sndsplit^#(m, app(map_f(two(), head(in_2)), st_2)),
         app^#(map_f(two(), head(in_2)), st_2),
         map_f^#(two(), head(in_2)),
         head^#(in_2),
         fstsplit^#(m, app(map_f(two(), head(in_2)), st_2)),
         app^#(map_f(two(), head(in_2)), st_2),
         map_f^#(two(), head(in_2)),
         head^#(in_2))
  , if_7^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
    c_33(ring^#(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m),
         sndsplit^#(m, st_3))
  , if_8^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
    c_34(ring^#(st_1,
                in_2,
                st_2,
                tail(in_3),
                sndsplit(m, app(map_f(three(), head(in_3)), st_3)),
                m),
         tail^#(in_3),
         sndsplit^#(m, app(map_f(three(), head(in_3)), st_3)),
         app^#(map_f(three(), head(in_3)), st_3),
         map_f^#(three(), head(in_3)),
         head^#(in_3)) }
Weak DPs:
  { fstsplit^#(0(), x) -> c_1()
  , fstsplit^#(s(n), nil()) -> c_2()
  , sndsplit^#(0(), x) -> c_4()
  , sndsplit^#(s(n), nil()) -> c_5()
  , empty^#(nil()) -> c_7()
  , empty^#(cons(h, t)) -> c_8()
  , leq^#(0(), m) -> c_9()
  , leq^#(s(n), 0()) -> c_10()
  , length^#(nil()) -> c_12()
  , app^#(nil(), x) -> c_14()
  , map_f^#(pid, nil()) -> c_16()
  , head^#(cons(h, t)) -> c_18()
  , tail^#(cons(h, t)) -> c_19() }
Weak 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)))
  , 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)))
  , 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))))
  , 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)))
  , 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_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)
  , 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_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_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_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)
  , 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)
  , 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_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_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_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)
  , 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) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ fstsplit^#(0(), x) -> c_1()
, fstsplit^#(s(n), nil()) -> c_2()
, sndsplit^#(0(), x) -> c_4()
, sndsplit^#(s(n), nil()) -> c_5()
, empty^#(nil()) -> c_7()
, empty^#(cons(h, t)) -> c_8()
, leq^#(0(), m) -> c_9()
, leq^#(s(n), 0()) -> c_10()
, length^#(nil()) -> c_12()
, app^#(nil(), x) -> c_14()
, map_f^#(pid, nil()) -> c_16()
, head^#(cons(h, t)) -> c_18()
, tail^#(cons(h, t)) -> c_19() }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { fstsplit^#(s(n), cons(h, t)) -> c_3(fstsplit^#(n, t))
  , sndsplit^#(s(n), cons(h, t)) -> c_6(sndsplit^#(n, t))
  , leq^#(s(n), s(m)) -> c_11(leq^#(n, m))
  , length^#(cons(h, t)) -> c_13(length^#(t))
  , app^#(cons(h, t), x) -> c_15(app^#(t, x))
  , map_f^#(pid, cons(h, t)) ->
    c_17(app^#(f(pid, h), map_f(pid, t)), map_f^#(pid, t))
  , ring^#(st_1, in_2, st_2, in_3, st_3, m) ->
    c_20(if_1^#(st_1,
                in_2,
                st_2,
                in_3,
                st_3,
                m,
                empty(fstsplit(m, st_1))),
         empty^#(fstsplit(m, st_1)),
         fstsplit^#(m, st_1))
  , ring^#(st_1, in_2, st_2, in_3, st_3, m) ->
    c_21(if_2^#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2))),
         leq^#(m, length(st_2)),
         length^#(st_2))
  , ring^#(st_1, in_2, st_2, in_3, st_3, m) ->
    c_22(if_5^#(st_1,
                in_2,
                st_2,
                in_3,
                st_3,
                m,
                empty(map_f(two(), head(in_2)))),
         empty^#(map_f(two(), head(in_2))),
         map_f^#(two(), head(in_2)),
         head^#(in_2))
  , ring^#(st_1, in_2, st_2, in_3, st_3, m) ->
    c_23(if_6^#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3))),
         leq^#(m, length(st_3)),
         length^#(st_3))
  , ring^#(st_1, in_2, st_2, in_3, st_3, m) ->
    c_24(if_9^#(st_1,
                in_2,
                st_2,
                in_3,
                st_3,
                m,
                empty(map_f(three(), head(in_3)))),
         empty^#(map_f(three(), head(in_3))),
         map_f^#(three(), head(in_3)),
         head^#(in_3))
  , if_1^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
    c_25(ring^#(sndsplit(m, st_1),
                cons(fstsplit(m, st_1), in_2),
                st_2,
                in_3,
                st_3,
                m),
         sndsplit^#(m, st_1),
         fstsplit^#(m, st_1))
  , if_2^#(st_1, in_2, st_2, in_3, st_3, m, true()) ->
    c_26(if_3^#(st_1,
                in_2,
                st_2,
                in_3,
                st_3,
                m,
                empty(fstsplit(m, st_2))),
         empty^#(fstsplit(m, st_2)),
         fstsplit^#(m, st_2))
  , if_2^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
    c_27(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)))),
         empty^#(fstsplit(m, app(map_f(two(), head(in_2)), st_2))),
         fstsplit^#(m, app(map_f(two(), head(in_2)), st_2)),
         app^#(map_f(two(), head(in_2)), st_2),
         map_f^#(two(), head(in_2)),
         head^#(in_2))
  , if_5^#(st_1, in_2, st_2, in_3, st_3, m, true()) ->
    c_30(ring^#(st_1, tail(in_2), st_2, in_3, st_3, m), tail^#(in_2))
  , if_6^#(st_1, in_2, st_2, in_3, st_3, m, true()) ->
    c_31(if_7^#(st_1,
                in_2,
                st_2,
                in_3,
                st_3,
                m,
                empty(fstsplit(m, st_3))),
         empty^#(fstsplit(m, st_3)),
         fstsplit^#(m, st_3))
  , if_6^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
    c_32(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)))),
         empty^#(fstsplit(m, app(map_f(three(), head(in_3)), st_3))),
         fstsplit^#(m, app(map_f(three(), head(in_3)), st_3)),
         app^#(map_f(three(), head(in_3)), st_3),
         map_f^#(three(), head(in_3)),
         head^#(in_3))
  , if_9^#(st_1, in_2, st_2, in_3, st_3, m, true()) ->
    c_35(ring^#(st_1, in_2, st_2, tail(in_3), st_3, m), tail^#(in_3))
  , if_3^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
    c_28(ring^#(st_1,
                in_2,
                sndsplit(m, st_2),
                cons(fstsplit(m, st_2), in_3),
                st_3,
                m),
         sndsplit^#(m, st_2),
         fstsplit^#(m, st_2))
  , if_4^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
    c_29(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),
         tail^#(in_2),
         sndsplit^#(m, app(map_f(two(), head(in_2)), st_2)),
         app^#(map_f(two(), head(in_2)), st_2),
         map_f^#(two(), head(in_2)),
         head^#(in_2),
         fstsplit^#(m, app(map_f(two(), head(in_2)), st_2)),
         app^#(map_f(two(), head(in_2)), st_2),
         map_f^#(two(), head(in_2)),
         head^#(in_2))
  , if_7^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
    c_33(ring^#(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m),
         sndsplit^#(m, st_3))
  , if_8^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
    c_34(ring^#(st_1,
                in_2,
                st_2,
                tail(in_3),
                sndsplit(m, app(map_f(three(), head(in_3)), st_3)),
                m),
         tail^#(in_3),
         sndsplit^#(m, app(map_f(three(), head(in_3)), st_3)),
         app^#(map_f(three(), head(in_3)), st_3),
         map_f^#(three(), head(in_3)),
         head^#(in_3)) }
Weak 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)))
  , 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)))
  , 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))))
  , 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)))
  , 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_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)
  , 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_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_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_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)
  , 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)
  , 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_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_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_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)
  , 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) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:

  { map_f^#(pid, cons(h, t)) ->
    c_17(app^#(f(pid, h), map_f(pid, t)), map_f^#(pid, t))
  , ring^#(st_1, in_2, st_2, in_3, st_3, m) ->
    c_20(if_1^#(st_1,
                in_2,
                st_2,
                in_3,
                st_3,
                m,
                empty(fstsplit(m, st_1))),
         empty^#(fstsplit(m, st_1)),
         fstsplit^#(m, st_1))
  , ring^#(st_1, in_2, st_2, in_3, st_3, m) ->
    c_22(if_5^#(st_1,
                in_2,
                st_2,
                in_3,
                st_3,
                m,
                empty(map_f(two(), head(in_2)))),
         empty^#(map_f(two(), head(in_2))),
         map_f^#(two(), head(in_2)),
         head^#(in_2))
  , ring^#(st_1, in_2, st_2, in_3, st_3, m) ->
    c_24(if_9^#(st_1,
                in_2,
                st_2,
                in_3,
                st_3,
                m,
                empty(map_f(three(), head(in_3)))),
         empty^#(map_f(three(), head(in_3))),
         map_f^#(three(), head(in_3)),
         head^#(in_3))
  , if_2^#(st_1, in_2, st_2, in_3, st_3, m, true()) ->
    c_26(if_3^#(st_1,
                in_2,
                st_2,
                in_3,
                st_3,
                m,
                empty(fstsplit(m, st_2))),
         empty^#(fstsplit(m, st_2)),
         fstsplit^#(m, st_2))
  , if_2^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
    c_27(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)))),
         empty^#(fstsplit(m, app(map_f(two(), head(in_2)), st_2))),
         fstsplit^#(m, app(map_f(two(), head(in_2)), st_2)),
         app^#(map_f(two(), head(in_2)), st_2),
         map_f^#(two(), head(in_2)),
         head^#(in_2))
  , if_5^#(st_1, in_2, st_2, in_3, st_3, m, true()) ->
    c_30(ring^#(st_1, tail(in_2), st_2, in_3, st_3, m), tail^#(in_2))
  , if_6^#(st_1, in_2, st_2, in_3, st_3, m, true()) ->
    c_31(if_7^#(st_1,
                in_2,
                st_2,
                in_3,
                st_3,
                m,
                empty(fstsplit(m, st_3))),
         empty^#(fstsplit(m, st_3)),
         fstsplit^#(m, st_3))
  , if_6^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
    c_32(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)))),
         empty^#(fstsplit(m, app(map_f(three(), head(in_3)), st_3))),
         fstsplit^#(m, app(map_f(three(), head(in_3)), st_3)),
         app^#(map_f(three(), head(in_3)), st_3),
         map_f^#(three(), head(in_3)),
         head^#(in_3))
  , if_9^#(st_1, in_2, st_2, in_3, st_3, m, true()) ->
    c_35(ring^#(st_1, in_2, st_2, tail(in_3), st_3, m), tail^#(in_3))
  , if_4^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
    c_29(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),
         tail^#(in_2),
         sndsplit^#(m, app(map_f(two(), head(in_2)), st_2)),
         app^#(map_f(two(), head(in_2)), st_2),
         map_f^#(two(), head(in_2)),
         head^#(in_2),
         fstsplit^#(m, app(map_f(two(), head(in_2)), st_2)),
         app^#(map_f(two(), head(in_2)), st_2),
         map_f^#(two(), head(in_2)),
         head^#(in_2))
  , if_8^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
    c_34(ring^#(st_1,
                in_2,
                st_2,
                tail(in_3),
                sndsplit(m, app(map_f(three(), head(in_3)), st_3)),
                m),
         tail^#(in_3),
         sndsplit^#(m, app(map_f(three(), head(in_3)), st_3)),
         app^#(map_f(three(), head(in_3)), st_3),
         map_f^#(three(), head(in_3)),
         head^#(in_3)) }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { fstsplit^#(s(n), cons(h, t)) -> c_1(fstsplit^#(n, t))
  , sndsplit^#(s(n), cons(h, t)) -> c_2(sndsplit^#(n, t))
  , leq^#(s(n), s(m)) -> c_3(leq^#(n, m))
  , length^#(cons(h, t)) -> c_4(length^#(t))
  , app^#(cons(h, t), x) -> c_5(app^#(t, x))
  , map_f^#(pid, cons(h, t)) -> c_6(map_f^#(pid, t))
  , ring^#(st_1, in_2, st_2, in_3, st_3, m) ->
    c_7(if_2^#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2))),
        leq^#(m, length(st_2)),
        length^#(st_2))
  , ring^#(st_1, in_2, st_2, in_3, st_3, m) ->
    c_8(if_6^#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3))),
        leq^#(m, length(st_3)),
        length^#(st_3))
  , ring^#(st_1, in_2, st_2, in_3, st_3, m) ->
    c_9(if_1^#(st_1,
               in_2,
               st_2,
               in_3,
               st_3,
               m,
               empty(fstsplit(m, st_1))),
        fstsplit^#(m, st_1))
  , ring^#(st_1, in_2, st_2, in_3, st_3, m) ->
    c_10(if_5^#(st_1,
                in_2,
                st_2,
                in_3,
                st_3,
                m,
                empty(map_f(two(), head(in_2)))),
         map_f^#(two(), head(in_2)))
  , ring^#(st_1, in_2, st_2, in_3, st_3, m) ->
    c_11(if_9^#(st_1,
                in_2,
                st_2,
                in_3,
                st_3,
                m,
                empty(map_f(three(), head(in_3)))),
         map_f^#(three(), head(in_3)))
  , if_1^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
    c_12(ring^#(sndsplit(m, st_1),
                cons(fstsplit(m, st_1), in_2),
                st_2,
                in_3,
                st_3,
                m),
         sndsplit^#(m, st_1),
         fstsplit^#(m, st_1))
  , if_2^#(st_1, in_2, st_2, in_3, st_3, m, true()) ->
    c_13(if_3^#(st_1,
                in_2,
                st_2,
                in_3,
                st_3,
                m,
                empty(fstsplit(m, st_2))),
         fstsplit^#(m, st_2))
  , if_2^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
    c_14(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)))),
         fstsplit^#(m, app(map_f(two(), head(in_2)), st_2)),
         app^#(map_f(two(), head(in_2)), st_2),
         map_f^#(two(), head(in_2)))
  , if_5^#(st_1, in_2, st_2, in_3, st_3, m, true()) ->
    c_15(ring^#(st_1, tail(in_2), st_2, in_3, st_3, m))
  , if_6^#(st_1, in_2, st_2, in_3, st_3, m, true()) ->
    c_16(if_7^#(st_1,
                in_2,
                st_2,
                in_3,
                st_3,
                m,
                empty(fstsplit(m, st_3))),
         fstsplit^#(m, st_3))
  , if_6^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
    c_17(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)))),
         fstsplit^#(m, app(map_f(three(), head(in_3)), st_3)),
         app^#(map_f(three(), head(in_3)), st_3),
         map_f^#(three(), head(in_3)))
  , if_9^#(st_1, in_2, st_2, in_3, st_3, m, true()) ->
    c_18(ring^#(st_1, in_2, st_2, tail(in_3), st_3, m))
  , if_3^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
    c_19(ring^#(st_1,
                in_2,
                sndsplit(m, st_2),
                cons(fstsplit(m, st_2), in_3),
                st_3,
                m),
         sndsplit^#(m, st_2),
         fstsplit^#(m, st_2))
  , if_4^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
    c_20(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),
         sndsplit^#(m, app(map_f(two(), head(in_2)), st_2)),
         app^#(map_f(two(), head(in_2)), st_2),
         map_f^#(two(), head(in_2)),
         fstsplit^#(m, app(map_f(two(), head(in_2)), st_2)),
         app^#(map_f(two(), head(in_2)), st_2),
         map_f^#(two(), head(in_2)))
  , if_7^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
    c_21(ring^#(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m),
         sndsplit^#(m, st_3))
  , if_8^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
    c_22(ring^#(st_1,
                in_2,
                st_2,
                tail(in_3),
                sndsplit(m, app(map_f(three(), head(in_3)), st_3)),
                m),
         sndsplit^#(m, app(map_f(three(), head(in_3)), st_3)),
         app^#(map_f(three(), head(in_3)), st_3),
         map_f^#(three(), head(in_3))) }
Weak 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)))
  , 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)))
  , 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))))
  , 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)))
  , 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_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)
  , 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_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_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_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)
  , 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)
  , 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_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_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_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)
  , 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) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We replace rewrite rules by usable rules:

  Weak Usable Rules:
    { 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 }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { fstsplit^#(s(n), cons(h, t)) -> c_1(fstsplit^#(n, t))
  , sndsplit^#(s(n), cons(h, t)) -> c_2(sndsplit^#(n, t))
  , leq^#(s(n), s(m)) -> c_3(leq^#(n, m))
  , length^#(cons(h, t)) -> c_4(length^#(t))
  , app^#(cons(h, t), x) -> c_5(app^#(t, x))
  , map_f^#(pid, cons(h, t)) -> c_6(map_f^#(pid, t))
  , ring^#(st_1, in_2, st_2, in_3, st_3, m) ->
    c_7(if_2^#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2))),
        leq^#(m, length(st_2)),
        length^#(st_2))
  , ring^#(st_1, in_2, st_2, in_3, st_3, m) ->
    c_8(if_6^#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3))),
        leq^#(m, length(st_3)),
        length^#(st_3))
  , ring^#(st_1, in_2, st_2, in_3, st_3, m) ->
    c_9(if_1^#(st_1,
               in_2,
               st_2,
               in_3,
               st_3,
               m,
               empty(fstsplit(m, st_1))),
        fstsplit^#(m, st_1))
  , ring^#(st_1, in_2, st_2, in_3, st_3, m) ->
    c_10(if_5^#(st_1,
                in_2,
                st_2,
                in_3,
                st_3,
                m,
                empty(map_f(two(), head(in_2)))),
         map_f^#(two(), head(in_2)))
  , ring^#(st_1, in_2, st_2, in_3, st_3, m) ->
    c_11(if_9^#(st_1,
                in_2,
                st_2,
                in_3,
                st_3,
                m,
                empty(map_f(three(), head(in_3)))),
         map_f^#(three(), head(in_3)))
  , if_1^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
    c_12(ring^#(sndsplit(m, st_1),
                cons(fstsplit(m, st_1), in_2),
                st_2,
                in_3,
                st_3,
                m),
         sndsplit^#(m, st_1),
         fstsplit^#(m, st_1))
  , if_2^#(st_1, in_2, st_2, in_3, st_3, m, true()) ->
    c_13(if_3^#(st_1,
                in_2,
                st_2,
                in_3,
                st_3,
                m,
                empty(fstsplit(m, st_2))),
         fstsplit^#(m, st_2))
  , if_2^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
    c_14(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)))),
         fstsplit^#(m, app(map_f(two(), head(in_2)), st_2)),
         app^#(map_f(two(), head(in_2)), st_2),
         map_f^#(two(), head(in_2)))
  , if_5^#(st_1, in_2, st_2, in_3, st_3, m, true()) ->
    c_15(ring^#(st_1, tail(in_2), st_2, in_3, st_3, m))
  , if_6^#(st_1, in_2, st_2, in_3, st_3, m, true()) ->
    c_16(if_7^#(st_1,
                in_2,
                st_2,
                in_3,
                st_3,
                m,
                empty(fstsplit(m, st_3))),
         fstsplit^#(m, st_3))
  , if_6^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
    c_17(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)))),
         fstsplit^#(m, app(map_f(three(), head(in_3)), st_3)),
         app^#(map_f(three(), head(in_3)), st_3),
         map_f^#(three(), head(in_3)))
  , if_9^#(st_1, in_2, st_2, in_3, st_3, m, true()) ->
    c_18(ring^#(st_1, in_2, st_2, tail(in_3), st_3, m))
  , if_3^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
    c_19(ring^#(st_1,
                in_2,
                sndsplit(m, st_2),
                cons(fstsplit(m, st_2), in_3),
                st_3,
                m),
         sndsplit^#(m, st_2),
         fstsplit^#(m, st_2))
  , if_4^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
    c_20(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),
         sndsplit^#(m, app(map_f(two(), head(in_2)), st_2)),
         app^#(map_f(two(), head(in_2)), st_2),
         map_f^#(two(), head(in_2)),
         fstsplit^#(m, app(map_f(two(), head(in_2)), st_2)),
         app^#(map_f(two(), head(in_2)), st_2),
         map_f^#(two(), head(in_2)))
  , if_7^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
    c_21(ring^#(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m),
         sndsplit^#(m, st_3))
  , if_8^#(st_1, in_2, st_2, in_3, st_3, m, false()) ->
    c_22(ring^#(st_1,
                in_2,
                st_2,
                tail(in_3),
                sndsplit(m, app(map_f(three(), head(in_3)), st_3)),
                m),
         sndsplit^#(m, app(map_f(three(), head(in_3)), st_3)),
         app^#(map_f(three(), head(in_3)), st_3),
         map_f^#(three(), head(in_3))) }
Weak 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 }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..