MAYBE

Problem:
 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)

Proof:
 DP Processor:
  DPs:
   fstsplit#(s(n),cons(h,t)) -> fstsplit#(n,t)
   sndsplit#(s(n),cons(h,t)) -> sndsplit#(n,t)
   leq#(s(n),s(m)) -> leq#(n,m)
   length#(cons(h,t)) -> length#(t)
   app#(cons(h,t),x) -> app#(t,x)
   map_f#(pid,cons(h,t)) -> map_f#(pid,t)
   map_f#(pid,cons(h,t)) -> app#(f(pid,h),map_f(pid,t))
   ring#(st_1,in_2,st_2,in_3,st_3,m) -> fstsplit#(m,st_1)
   ring#(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_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()) -> fstsplit#(m,st_1)
   if_1#(st_1,in_2,st_2,in_3,st_3,m,false()) -> sndsplit#(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) -> length#(st_2)
   ring#(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_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()) -> fstsplit#(m,st_2)
   if_2#(st_1,in_2,st_2,in_3,st_3,m,true()) -> empty#(fstsplit(m,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()) -> fstsplit#(m,st_2)
   if_3#(st_1,in_2,st_2,in_3,st_3,m,false()) -> sndsplit#(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()) -> head#(in_2)
   if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> map_f#(two(),head(in_2))
   if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> app#(map_f(two(),head(in_2)),st_2)
   if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> fstsplit#(m,app(map_f(two(),head(in_2)),st_2))
   if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) ->
   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,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()) -> 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()) -> head#(in_2)
   if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> map_f#(two(),head(in_2))
   if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> app#(map_f(two(),head(in_2)),st_2)
   if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> sndsplit#(m,app(map_f(two(),head(in_2)),st_2))
   if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> tail#(in_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) -> head#(in_2)
   ring#(st_1,in_2,st_2,in_3,st_3,m) -> map_f#(two(),head(in_2))
   ring#(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_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()) -> tail#(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) -> length#(st_3)
   ring#(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_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()) -> fstsplit#(m,st_3)
   if_6#(st_1,in_2,st_2,in_3,st_3,m,true()) -> empty#(fstsplit(m,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()) -> sndsplit#(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()) -> head#(in_3)
   if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> map_f#(three(),head(in_3))
   if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> app#(map_f(three(),head(in_3)),st_3)
   if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> fstsplit#(m,app(map_f(three(),head(in_3)),st_3))
   if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) ->
   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,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()) -> head#(in_3)
   if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> map_f#(three(),head(in_3))
   if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> app#(map_f(three(),head(in_3)),st_3)
   if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> sndsplit#(m,app(map_f(three(),head(in_3)),st_3))
   if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> tail#(in_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) -> head#(in_3)
   ring#(st_1,in_2,st_2,in_3,st_3,m) -> map_f#(three(),head(in_3))
   ring#(st_1,in_2,st_2,in_3,st_3,m) -> empty#(map_f(three(),head(in_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_9#(st_1,in_2,st_2,in_3,st_3,m,true()) -> tail#(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)
  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)
  TDG Processor:
   DPs:
    fstsplit#(s(n),cons(h,t)) -> fstsplit#(n,t)
    sndsplit#(s(n),cons(h,t)) -> sndsplit#(n,t)
    leq#(s(n),s(m)) -> leq#(n,m)
    length#(cons(h,t)) -> length#(t)
    app#(cons(h,t),x) -> app#(t,x)
    map_f#(pid,cons(h,t)) -> map_f#(pid,t)
    map_f#(pid,cons(h,t)) -> app#(f(pid,h),map_f(pid,t))
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> fstsplit#(m,st_1)
    ring#(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_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()) -> fstsplit#(m,st_1)
    if_1#(st_1,in_2,st_2,in_3,st_3,m,false()) -> sndsplit#(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) -> length#(st_2)
    ring#(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_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()) -> fstsplit#(m,st_2)
    if_2#(st_1,in_2,st_2,in_3,st_3,m,true()) -> empty#(fstsplit(m,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()) -> fstsplit#(m,st_2)
    if_3#(st_1,in_2,st_2,in_3,st_3,m,false()) -> sndsplit#(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()) -> head#(in_2)
    if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> map_f#(two(),head(in_2))
    if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> app#(map_f(two(),head(in_2)),st_2)
    if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> fstsplit#(m,app(map_f(two(),head(in_2)),st_2))
    if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) ->
    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,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()) -> 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()) -> head#(in_2)
    if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> map_f#(two(),head(in_2))
    if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> app#(map_f(two(),head(in_2)),st_2)
    if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> sndsplit#(m,app(map_f(two(),head(in_2)),st_2))
    if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> tail#(in_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) -> head#(in_2)
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> map_f#(two(),head(in_2))
    ring#(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_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()) -> tail#(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) -> length#(st_3)
    ring#(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_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()) -> fstsplit#(m,st_3)
    if_6#(st_1,in_2,st_2,in_3,st_3,m,true()) -> empty#(fstsplit(m,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()) -> sndsplit#(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()) -> head#(in_3)
    if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> map_f#(three(),head(in_3))
    if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> app#(map_f(three(),head(in_3)),st_3)
    if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> fstsplit#(m,app(map_f(three(),head(in_3)),st_3))
    if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) ->
    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,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()) -> head#(in_3)
    if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> map_f#(three(),head(in_3))
    if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> app#(map_f(three(),head(in_3)),st_3)
    if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> sndsplit#(m,app(map_f(three(),head(in_3)),st_3))
    if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> tail#(in_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) -> head#(in_3)
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> map_f#(three(),head(in_3))
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> empty#(map_f(three(),head(in_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_9#(st_1,in_2,st_2,in_3,st_3,m,true()) -> tail#(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)
   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)
   graph:
    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) ->
    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) ->
    ring#(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) ->
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> 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) ->
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> 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) ->
    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_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) ->
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> leq#(m,length(st_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) ->
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> length#(st_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) ->
    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_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) ->
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> empty#(map_f(two(),head(in_2)))
    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) ->
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> map_f#(two(),head(in_2))
    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) ->
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> head#(in_2)
    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) ->
    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_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) ->
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> leq#(m,length(st_2))
    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) ->
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> length#(st_2)
    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) ->
    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_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) ->
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> empty#(fstsplit(m,st_1))
    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) ->
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> fstsplit#(m,st_1)
    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_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) -> empty#(map_f(three(),head(in_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) -> map_f#(three(),head(in_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) -> head#(in_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_6#(st_1,in_2,st_2,in_3,st_3,m,leq(m,length(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) -> leq#(m,length(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) -> length#(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_5#(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(two(),head(in_2))))
    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) -> empty#(map_f(two(),head(in_2)))
    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) -> map_f#(two(),head(in_2))
    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) -> head#(in_2)
    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_2#(st_1,in_2,st_2,in_3,st_3,m,leq(m,length(st_2)))
    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) -> leq#(m,length(st_2))
    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) -> length#(st_2)
    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_1#(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_1)))
    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) -> empty#(fstsplit(m,st_1))
    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) -> fstsplit#(m,st_1)
    if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> map_f#(three(),head(in_3)) ->
    map_f#(pid,cons(h,t)) -> app#(f(pid,h),map_f(pid,t))
    if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> map_f#(three(),head(in_3)) ->
    map_f#(pid,cons(h,t)) -> map_f#(pid,t)
    if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> app#(map_f(three(),head(in_3)),st_3) ->
    app#(cons(h,t),x) -> app#(t,x)
    if_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> sndsplit#(m,app(map_f(three(),head(in_3)),st_3))
    ->
    sndsplit#(s(n),cons(h,t)) -> sndsplit#(n,t)
    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) ->
    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_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) ->
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> empty#(map_f(three(),head(in_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) ->
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> map_f#(three(),head(in_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) ->
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> head#(in_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) ->
    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_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) ->
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> leq#(m,length(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) ->
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> length#(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) ->
    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_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) ->
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> empty#(map_f(two(),head(in_2)))
    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) ->
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> map_f#(two(),head(in_2))
    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) ->
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> head#(in_2)
    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) ->
    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_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) ->
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> leq#(m,length(st_2))
    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) ->
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> length#(st_2)
    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) ->
    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_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) ->
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> empty#(fstsplit(m,st_1))
    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) ->
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> fstsplit#(m,st_1)
    if_7#(st_1,in_2,st_2,in_3,st_3,m,false()) -> sndsplit#(m,st_3) ->
    sndsplit#(s(n),cons(h,t)) -> sndsplit#(n,t)
    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)
    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()) -> tail#(in_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_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> sndsplit#(m,app(map_f(three(),head(in_3)),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_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> app#(map_f(three(),head(in_3)),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_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> map_f#(three(),head(in_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_8#(st_1,in_2,st_2,in_3,st_3,m,false()) -> head#(in_3)
    if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> map_f#(three(),head(in_3)) ->
    map_f#(pid,cons(h,t)) -> app#(f(pid,h),map_f(pid,t))
    if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> map_f#(three(),head(in_3)) ->
    map_f#(pid,cons(h,t)) -> map_f#(pid,t)
    if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> app#(map_f(three(),head(in_3)),st_3) ->
    app#(cons(h,t),x) -> app#(t,x)
    if_6#(st_1,in_2,st_2,in_3,st_3,m,false()) -> fstsplit#(m,app(map_f(three(),head(in_3)),st_3))
    ->
    fstsplit#(s(n),cons(h,t)) -> fstsplit#(n,t)
    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,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()) -> sndsplit#(m,st_3)
    if_6#(st_1,in_2,st_2,in_3,st_3,m,true()) -> fstsplit#(m,st_3) ->
    fstsplit#(s(n),cons(h,t)) -> fstsplit#(n,t)
    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_9#(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(three(),head(in_3))))
    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) -> empty#(map_f(three(),head(in_3)))
    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) -> map_f#(three(),head(in_3))
    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) -> head#(in_3)
    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_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) -> leq#(m,length(st_3))
    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) -> length#(st_3)
    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_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) -> 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) -> 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) -> 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_2#(st_1,in_2,st_2,in_3,st_3,m,leq(m,length(st_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) -> leq#(m,length(st_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) -> length#(st_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_1#(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_1)))
    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) -> empty#(fstsplit(m,st_1))
    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) -> fstsplit#(m,st_1)
    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_9#(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(three(),head(in_3))))
    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) -> empty#(map_f(three(),head(in_3)))
    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) -> map_f#(three(),head(in_3))
    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) -> head#(in_3)
    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_6#(st_1,in_2,st_2,in_3,st_3,m,leq(m,length(st_3)))
    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) -> leq#(m,length(st_3))
    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) -> length#(st_3)
    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_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) -> empty#(map_f(two(),head(in_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) -> map_f#(two(),head(in_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) -> head#(in_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_2#(st_1,in_2,st_2,in_3,st_3,m,leq(m,length(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) -> leq#(m,length(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) -> length#(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_1#(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_1)))
    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) -> empty#(fstsplit(m,st_1))
    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) -> fstsplit#(m,st_1)
    if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> map_f#(two(),head(in_2)) ->
    map_f#(pid,cons(h,t)) -> app#(f(pid,h),map_f(pid,t))
    if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> map_f#(two(),head(in_2)) ->
    map_f#(pid,cons(h,t)) -> map_f#(pid,t)
    if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> app#(map_f(two(),head(in_2)),st_2) ->
    app#(cons(h,t),x) -> app#(t,x)
    if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> sndsplit#(m,app(map_f(two(),head(in_2)),st_2)) ->
    sndsplit#(s(n),cons(h,t)) -> sndsplit#(n,t)
    if_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> fstsplit#(m,app(map_f(two(),head(in_2)),st_2)) ->
    fstsplit#(s(n),cons(h,t)) -> fstsplit#(n,t)
    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) ->
    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_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) ->
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> empty#(map_f(three(),head(in_3)))
    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) ->
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> map_f#(three(),head(in_3))
    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) ->
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> head#(in_3)
    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) ->
    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_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) ->
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> leq#(m,length(st_3))
    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) ->
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> length#(st_3)
    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) ->
    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_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) ->
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> empty#(map_f(two(),head(in_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) ->
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> map_f#(two(),head(in_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) ->
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> head#(in_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) ->
    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_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) ->
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> leq#(m,length(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) ->
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> length#(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) ->
    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_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) ->
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> empty#(fstsplit(m,st_1))
    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) ->
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> fstsplit#(m,st_1)
    if_3#(st_1,in_2,st_2,in_3,st_3,m,false()) -> sndsplit#(m,st_2) ->
    sndsplit#(s(n),cons(h,t)) -> sndsplit#(n,t)
    if_3#(st_1,in_2,st_2,in_3,st_3,m,false()) -> fstsplit#(m,st_2) ->
    fstsplit#(s(n),cons(h,t)) -> fstsplit#(n,t)
    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)
    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()) -> tail#(in_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_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> sndsplit#(m,app(map_f(two(),head(in_2)),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_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> app#(map_f(two(),head(in_2)),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_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> map_f#(two(),head(in_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_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> head#(in_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_4#(st_1,in_2,st_2,in_3,st_3,m,false()) -> fstsplit#(m,app(map_f(two(),head(in_2)),st_2))
    if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> map_f#(two(),head(in_2)) ->
    map_f#(pid,cons(h,t)) -> app#(f(pid,h),map_f(pid,t))
    if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> map_f#(two(),head(in_2)) ->
    map_f#(pid,cons(h,t)) -> map_f#(pid,t)
    if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> app#(map_f(two(),head(in_2)),st_2) ->
    app#(cons(h,t),x) -> app#(t,x)
    if_2#(st_1,in_2,st_2,in_3,st_3,m,false()) -> fstsplit#(m,app(map_f(two(),head(in_2)),st_2)) ->
    fstsplit#(s(n),cons(h,t)) -> fstsplit#(n,t)
    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,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()) -> sndsplit#(m,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()) -> fstsplit#(m,st_2)
    if_2#(st_1,in_2,st_2,in_3,st_3,m,true()) -> fstsplit#(m,st_2) ->
    fstsplit#(s(n),cons(h,t)) -> fstsplit#(n,t)
    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_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) ->
    ring#(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) ->
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> 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) ->
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> 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) ->
    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_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) -> leq#(m,length(st_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) ->
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> length#(st_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) ->
    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_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) -> empty#(map_f(two(),head(in_2)))
    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) -> map_f#(two(),head(in_2))
    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) -> head#(in_2)
    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_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) -> leq#(m,length(st_2))
    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) -> length#(st_2)
    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_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) -> 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) -> fstsplit#(m,st_1)
    if_1#(st_1,in_2,st_2,in_3,st_3,m,false()) -> sndsplit#(m,st_1) ->
    sndsplit#(s(n),cons(h,t)) -> sndsplit#(n,t)
    if_1#(st_1,in_2,st_2,in_3,st_3,m,false()) -> fstsplit#(m,st_1) ->
    fstsplit#(s(n),cons(h,t)) -> fstsplit#(n,t)
    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)
    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()) -> tail#(in_3)
    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,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))))
    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,false()) ->
    empty#(fstsplit(m,app(map_f(three(),head(in_3)),st_3)))
    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,false()) -> fstsplit#(m,app(map_f(three(),head(in_3)),st_3))
    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,false()) -> app#(map_f(three(),head(in_3)),st_3)
    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,false()) -> map_f#(three(),head(in_3))
    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,false()) -> head#(in_3)
    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)))
    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()) -> empty#(fstsplit(m,st_3))
    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()) -> fstsplit#(m,st_3)
    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_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()) -> tail#(in_2)
    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,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))))
    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,false()) ->
    empty#(fstsplit(m,app(map_f(two(),head(in_2)),st_2)))
    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,false()) -> fstsplit#(m,app(map_f(two(),head(in_2)),st_2))
    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,false()) -> app#(map_f(two(),head(in_2)),st_2)
    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,false()) -> map_f#(two(),head(in_2))
    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,false()) -> head#(in_2)
    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)))
    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()) -> empty#(fstsplit(m,st_2))
    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()) -> fstsplit#(m,st_2)
    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_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()) -> sndsplit#(m,st_1)
    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()) -> fstsplit#(m,st_1)
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> map_f#(three(),head(in_3)) ->
    map_f#(pid,cons(h,t)) -> app#(f(pid,h),map_f(pid,t))
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> map_f#(three(),head(in_3)) ->
    map_f#(pid,cons(h,t)) -> map_f#(pid,t)
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> map_f#(two(),head(in_2)) ->
    map_f#(pid,cons(h,t)) -> app#(f(pid,h),map_f(pid,t))
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> map_f#(two(),head(in_2)) ->
    map_f#(pid,cons(h,t)) -> map_f#(pid,t)
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> length#(st_3) ->
    length#(cons(h,t)) -> length#(t)
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> length#(st_2) ->
    length#(cons(h,t)) -> length#(t)
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> leq#(m,length(st_3)) ->
    leq#(s(n),s(m)) -> leq#(n,m)
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> leq#(m,length(st_2)) ->
    leq#(s(n),s(m)) -> leq#(n,m)
    ring#(st_1,in_2,st_2,in_3,st_3,m) -> fstsplit#(m,st_1) ->
    fstsplit#(s(n),cons(h,t)) -> fstsplit#(n,t)
    map_f#(pid,cons(h,t)) -> map_f#(pid,t) ->
    map_f#(pid,cons(h,t)) -> app#(f(pid,h),map_f(pid,t))
    map_f#(pid,cons(h,t)) -> map_f#(pid,t) ->
    map_f#(pid,cons(h,t)) -> map_f#(pid,t)
    map_f#(pid,cons(h,t)) -> app#(f(pid,h),map_f(pid,t)) ->
    app#(cons(h,t),x) -> app#(t,x)
    app#(cons(h,t),x) -> app#(t,x) ->
    app#(cons(h,t),x) -> app#(t,x)
    length#(cons(h,t)) -> length#(t) ->
    length#(cons(h,t)) -> length#(t)
    leq#(s(n),s(m)) -> leq#(n,m) ->
    leq#(s(n),s(m)) -> leq#(n,m)
    sndsplit#(s(n),cons(h,t)) -> sndsplit#(n,t) ->
    sndsplit#(s(n),cons(h,t)) -> sndsplit#(n,t)
    fstsplit#(s(n),cons(h,t)) -> fstsplit#(n,t) -> fstsplit#(s(n),cons(h,t)) -> fstsplit#(n,t)
   SCC Processor:
    #sccs: 7
    #rules: 22
    #arcs: 203/4489
    DPs:
     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)
     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)
     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)
     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_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)
     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)
    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)
    Open
    
    DPs:
     map_f#(pid,cons(h,t)) -> map_f#(pid,t)
    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)
    Subterm Criterion Processor:
     simple projection:
      pi(map_f#) = 1
     problem:
      DPs:
       
      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)
     Qed
    
    DPs:
     app#(cons(h,t),x) -> app#(t,x)
    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)
    Subterm Criterion Processor:
     simple projection:
      pi(app#) = 0
     problem:
      DPs:
       
      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)
     Qed
    
    DPs:
     leq#(s(n),s(m)) -> leq#(n,m)
    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)
    Subterm Criterion Processor:
     simple projection:
      pi(leq#) = 1
     problem:
      DPs:
       
      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)
     Qed
    
    DPs:
     length#(cons(h,t)) -> length#(t)
    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)
    Subterm Criterion Processor:
     simple projection:
      pi(length#) = 0
     problem:
      DPs:
       
      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)
     Qed
    
    DPs:
     sndsplit#(s(n),cons(h,t)) -> sndsplit#(n,t)
    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)
    Subterm Criterion Processor:
     simple projection:
      pi(sndsplit#) = 1
     problem:
      DPs:
       
      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)
     Qed
    
    DPs:
     fstsplit#(s(n),cons(h,t)) -> fstsplit#(n,t)
    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)
    Subterm Criterion Processor:
     simple projection:
      pi(fstsplit#) = 1
     problem:
      DPs:
       
      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)
     Qed