MAYBE
* Step 1: Failure MAYBE
  + Considered Problem:
      - Strict TRS:
          app(cons(h,t),x) -> cons(h,app(t,x))
          app(nil(),x) -> x
          empty(cons(h,t)) -> false()
          empty(nil()) -> true()
          fstsplit(0(),x) -> nil()
          fstsplit(s(n),cons(h,t)) -> cons(h,fstsplit(n,t))
          fstsplit(s(n),nil()) -> nil()
          if1(store,m,false()) -> if3(store,m,empty(fstsplit(m,app(map_f(self(),nil()),store))))
          if1(store,m,true()) -> if2(store,m,empty(fstsplit(m,store)))
          if2(store,m,false()) -> process(app(map_f(self(),nil()),sndsplit(m,store)),m)
          if3(store,m,false()) -> process(sndsplit(m,app(map_f(self(),nil()),store)),m)
          length(cons(h,t)) -> s(length(t))
          length(nil()) -> 0()
          leq(0(),m) -> true()
          leq(s(n),0()) -> false()
          leq(s(n),s(m)) -> leq(n,m)
          map_f(pid,cons(h,t)) -> app(f(pid,h),map_f(pid,t))
          map_f(pid,nil()) -> nil()
          process(store,m) -> if1(store,m,leq(m,length(store)))
          sndsplit(0(),x) -> x
          sndsplit(s(n),cons(h,t)) -> sndsplit(n,t)
          sndsplit(s(n),nil()) -> nil()
      - Signature:
          {app/2,empty/1,fstsplit/2,if1/3,if2/3,if3/3,length/1,leq/2,map_f/2,process/2,sndsplit/2} / {0/0,cons/2,f/2
          ,false/0,nil/0,s/1,self/0,true/0}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {app,empty,fstsplit,if1,if2,if3,length,leq,map_f,process
          ,sndsplit} and constructors {0,cons,f,false,nil,s,self,true}
  + Applied Processor:
      Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 3, araTimeout = 60, araFindStrictRules = Nothing, araSmtSolver = MiniSMT}
  + Details:
      The input can not be schown compatible.
MAYBE