MAYBE
* Step 1: Failure MAYBE
  + Considered Problem:
      - Strict TRS:
          app(cons(h,t),x) -> cons(h,app(t,x))
          app(nil(),x) -> x
          empty(cons(h,t)) -> false()
          empty(nil()) -> true()
          fstsplit(0(),x) -> nil()
          fstsplit(s(n),cons(h,t)) -> cons(h,fstsplit(n,t))
          fstsplit(s(n),nil()) -> nil()
          head(cons(h,t)) -> h
          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,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_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_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,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_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_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)
          length(cons(h,t)) -> s(length(t))
          length(nil()) -> 0()
          leq(0(),m) -> true()
          leq(s(n),0()) -> false()
          leq(s(n),s(m)) -> leq(n,m)
          map_f(pid,cons(h,t)) -> app(f(pid,h),map_f(pid,t))
          map_f(pid,nil()) -> nil()
          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))))
          sndsplit(0(),x) -> x
          sndsplit(s(n),cons(h,t)) -> sndsplit(n,t)
          sndsplit(s(n),nil()) -> nil()
          tail(cons(h,t)) -> t
      - Signature:
          {app/2,empty/1,fstsplit/2,head/1,if_1/7,if_2/7,if_3/7,if_4/7,if_5/7,if_6/7,if_7/7,if_8/7,if_9/7,length/1
          ,leq/2,map_f/2,ring/6,sndsplit/2,tail/1} / {0/0,cons/2,f/2,false/0,nil/0,s/1,three/0,true/0,two/0}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {app,empty,fstsplit,head,if_1,if_2,if_3,if_4,if_5,if_6
          ,if_7,if_8,if_9,length,leq,map_f,ring,sndsplit,tail} and constructors {0,cons,f,false,nil,s,three,true,two}
  + Applied Processor:
      NaturalMI {miDimension = 3, miDegree = 3, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}
  + Details:
      Incompatible
MAYBE