MAYBE

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

Strict Trs:
  { fstsplit(0(), x) -> nil()
  , fstsplit(s(n), nil()) -> nil()
  , fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
  , sndsplit(0(), x) -> x
  , sndsplit(s(n), nil()) -> nil()
  , sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
  , empty(nil()) -> true()
  , empty(cons(h, t)) -> false()
  , leq(0(), m) -> true()
  , leq(s(n), 0()) -> false()
  , leq(s(n), s(m)) -> leq(n, m)
  , length(nil()) -> 0()
  , length(cons(h, t)) -> s(length(t))
  , app(nil(), x) -> x
  , app(cons(h, t), x) -> cons(h, app(t, x))
  , map_f(pid, nil()) -> nil()
  , map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
  , process(store, m) -> if1(store, m, leq(m, length(store)))
  , if1(store, m, true()) -> if2(store, m, empty(fstsplit(m, store)))
  , if1(store, m, false()) ->
    if3(store, m, empty(fstsplit(m, app(map_f(self(), nil()), 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) }
Obligation:
  runtime complexity
Answer:
  MAYBE

None of the processors succeeded.

Details of failed attempt(s):
-----------------------------
1) 'WithProblem (timeout of 60 seconds)' failed due to the
   following reason:
   
   Computation stopped due to timeout after 60.0 seconds.

2) 'Best' failed due to the following reason:
   
   None of the processors succeeded.
   
   Details of failed attempt(s):
   -----------------------------
   1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)'
      failed due to the following reason:
      
      Computation stopped due to timeout after 30.0 seconds.
   
   2) 'Best' failed due to the following reason:
      
      None of the processors succeeded.
      
      Details of failed attempt(s):
      -----------------------------
      1) 'bsearch-popstar (timeout of 60 seconds)' failed due to the
         following reason:
         
         The processor is inapplicable, reason:
           Processor only applicable for innermost runtime complexity analysis
      
      2) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due
         to the following reason:
         
         The processor is inapplicable, reason:
           Processor only applicable for innermost runtime complexity analysis
      
   
   3) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed
      due to the following reason:
      
      None of the processors succeeded.
      
      Details of failed attempt(s):
      -----------------------------
      1) 'Bounds with perSymbol-enrichment and initial automaton 'match''
         failed due to the following reason:
         
         match-boundness of the problem could not be verified.
      
      2) 'Bounds with minimal-enrichment and initial automaton 'match''
         failed due to the following reason:
         
         match-boundness of the problem could not be verified.
      
   

3) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed
   due to the following reason:
   
   We add the following weak dependency pairs:
   
   Strict DPs:
     { fstsplit^#(0(), x) -> c_1()
     , fstsplit^#(s(n), nil()) -> c_2()
     , fstsplit^#(s(n), cons(h, t)) -> c_3(h, fstsplit^#(n, t))
     , sndsplit^#(0(), x) -> c_4(x)
     , sndsplit^#(s(n), nil()) -> c_5()
     , sndsplit^#(s(n), cons(h, t)) -> c_6(sndsplit^#(n, t))
     , empty^#(nil()) -> c_7()
     , empty^#(cons(h, t)) -> c_8()
     , leq^#(0(), m) -> c_9()
     , leq^#(s(n), 0()) -> c_10()
     , leq^#(s(n), s(m)) -> c_11(leq^#(n, m))
     , length^#(nil()) -> c_12()
     , length^#(cons(h, t)) -> c_13(length^#(t))
     , app^#(nil(), x) -> c_14(x)
     , app^#(cons(h, t), x) -> c_15(h, app^#(t, x))
     , map_f^#(pid, nil()) -> c_16()
     , map_f^#(pid, cons(h, t)) -> c_17(app^#(f(pid, h), map_f(pid, t)))
     , process^#(store, m) ->
       c_18(if1^#(store, m, leq(m, length(store))))
     , if1^#(store, m, true()) ->
       c_19(if2^#(store, m, empty(fstsplit(m, store))))
     , if1^#(store, m, false()) ->
       c_20(if3^#(store,
                  m,
                  empty(fstsplit(m, app(map_f(self(), nil()), store)))))
     , if2^#(store, m, false()) ->
       c_21(process^#(app(map_f(self(), nil()), sndsplit(m, store)), m))
     , if3^#(store, m, false()) ->
       c_22(process^#(sndsplit(m, app(map_f(self(), nil()), store)), m)) }
   
   and mark the set of starting terms.
   
   We are left with following problem, upon which TcT provides the
   certificate MAYBE.
   
   Strict DPs:
     { fstsplit^#(0(), x) -> c_1()
     , fstsplit^#(s(n), nil()) -> c_2()
     , fstsplit^#(s(n), cons(h, t)) -> c_3(h, fstsplit^#(n, t))
     , sndsplit^#(0(), x) -> c_4(x)
     , sndsplit^#(s(n), nil()) -> c_5()
     , sndsplit^#(s(n), cons(h, t)) -> c_6(sndsplit^#(n, t))
     , empty^#(nil()) -> c_7()
     , empty^#(cons(h, t)) -> c_8()
     , leq^#(0(), m) -> c_9()
     , leq^#(s(n), 0()) -> c_10()
     , leq^#(s(n), s(m)) -> c_11(leq^#(n, m))
     , length^#(nil()) -> c_12()
     , length^#(cons(h, t)) -> c_13(length^#(t))
     , app^#(nil(), x) -> c_14(x)
     , app^#(cons(h, t), x) -> c_15(h, app^#(t, x))
     , map_f^#(pid, nil()) -> c_16()
     , map_f^#(pid, cons(h, t)) -> c_17(app^#(f(pid, h), map_f(pid, t)))
     , process^#(store, m) ->
       c_18(if1^#(store, m, leq(m, length(store))))
     , if1^#(store, m, true()) ->
       c_19(if2^#(store, m, empty(fstsplit(m, store))))
     , if1^#(store, m, false()) ->
       c_20(if3^#(store,
                  m,
                  empty(fstsplit(m, app(map_f(self(), nil()), store)))))
     , if2^#(store, m, false()) ->
       c_21(process^#(app(map_f(self(), nil()), sndsplit(m, store)), m))
     , if3^#(store, m, false()) ->
       c_22(process^#(sndsplit(m, app(map_f(self(), nil()), store)), m)) }
   Strict Trs:
     { fstsplit(0(), x) -> nil()
     , fstsplit(s(n), nil()) -> nil()
     , fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
     , sndsplit(0(), x) -> x
     , sndsplit(s(n), nil()) -> nil()
     , sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
     , empty(nil()) -> true()
     , empty(cons(h, t)) -> false()
     , leq(0(), m) -> true()
     , leq(s(n), 0()) -> false()
     , leq(s(n), s(m)) -> leq(n, m)
     , length(nil()) -> 0()
     , length(cons(h, t)) -> s(length(t))
     , app(nil(), x) -> x
     , app(cons(h, t), x) -> cons(h, app(t, x))
     , map_f(pid, nil()) -> nil()
     , map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
     , process(store, m) -> if1(store, m, leq(m, length(store)))
     , if1(store, m, true()) -> if2(store, m, empty(fstsplit(m, store)))
     , if1(store, m, false()) ->
       if3(store, m, empty(fstsplit(m, app(map_f(self(), nil()), 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) }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   We estimate the number of application of {1,2,5,7,8,9,10,12,16,17}
   by applications of Pre({1,2,5,7,8,9,10,12,16,17}) =
   {3,4,6,11,13,14,15}. Here rules are labeled as follows:
   
     DPs:
       { 1: fstsplit^#(0(), x) -> c_1()
       , 2: fstsplit^#(s(n), nil()) -> c_2()
       , 3: fstsplit^#(s(n), cons(h, t)) -> c_3(h, fstsplit^#(n, t))
       , 4: sndsplit^#(0(), x) -> c_4(x)
       , 5: sndsplit^#(s(n), nil()) -> c_5()
       , 6: sndsplit^#(s(n), cons(h, t)) -> c_6(sndsplit^#(n, t))
       , 7: empty^#(nil()) -> c_7()
       , 8: empty^#(cons(h, t)) -> c_8()
       , 9: leq^#(0(), m) -> c_9()
       , 10: leq^#(s(n), 0()) -> c_10()
       , 11: leq^#(s(n), s(m)) -> c_11(leq^#(n, m))
       , 12: length^#(nil()) -> c_12()
       , 13: length^#(cons(h, t)) -> c_13(length^#(t))
       , 14: app^#(nil(), x) -> c_14(x)
       , 15: app^#(cons(h, t), x) -> c_15(h, app^#(t, x))
       , 16: map_f^#(pid, nil()) -> c_16()
       , 17: map_f^#(pid, cons(h, t)) ->
             c_17(app^#(f(pid, h), map_f(pid, t)))
       , 18: process^#(store, m) ->
             c_18(if1^#(store, m, leq(m, length(store))))
       , 19: if1^#(store, m, true()) ->
             c_19(if2^#(store, m, empty(fstsplit(m, store))))
       , 20: if1^#(store, m, false()) ->
             c_20(if3^#(store,
                        m,
                        empty(fstsplit(m, app(map_f(self(), nil()), store)))))
       , 21: if2^#(store, m, false()) ->
             c_21(process^#(app(map_f(self(), nil()), sndsplit(m, store)), m))
       , 22: if3^#(store, m, false()) ->
             c_22(process^#(sndsplit(m, app(map_f(self(), nil()), store)), m)) }
   
   We are left with following problem, upon which TcT provides the
   certificate MAYBE.
   
   Strict DPs:
     { fstsplit^#(s(n), cons(h, t)) -> c_3(h, fstsplit^#(n, t))
     , sndsplit^#(0(), x) -> c_4(x)
     , sndsplit^#(s(n), cons(h, t)) -> c_6(sndsplit^#(n, t))
     , leq^#(s(n), s(m)) -> c_11(leq^#(n, m))
     , length^#(cons(h, t)) -> c_13(length^#(t))
     , app^#(nil(), x) -> c_14(x)
     , app^#(cons(h, t), x) -> c_15(h, app^#(t, x))
     , process^#(store, m) ->
       c_18(if1^#(store, m, leq(m, length(store))))
     , if1^#(store, m, true()) ->
       c_19(if2^#(store, m, empty(fstsplit(m, store))))
     , if1^#(store, m, false()) ->
       c_20(if3^#(store,
                  m,
                  empty(fstsplit(m, app(map_f(self(), nil()), store)))))
     , if2^#(store, m, false()) ->
       c_21(process^#(app(map_f(self(), nil()), sndsplit(m, store)), m))
     , if3^#(store, m, false()) ->
       c_22(process^#(sndsplit(m, app(map_f(self(), nil()), store)), m)) }
   Strict Trs:
     { fstsplit(0(), x) -> nil()
     , fstsplit(s(n), nil()) -> nil()
     , fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
     , sndsplit(0(), x) -> x
     , sndsplit(s(n), nil()) -> nil()
     , sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
     , empty(nil()) -> true()
     , empty(cons(h, t)) -> false()
     , leq(0(), m) -> true()
     , leq(s(n), 0()) -> false()
     , leq(s(n), s(m)) -> leq(n, m)
     , length(nil()) -> 0()
     , length(cons(h, t)) -> s(length(t))
     , app(nil(), x) -> x
     , app(cons(h, t), x) -> cons(h, app(t, x))
     , map_f(pid, nil()) -> nil()
     , map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
     , process(store, m) -> if1(store, m, leq(m, length(store)))
     , if1(store, m, true()) -> if2(store, m, empty(fstsplit(m, store)))
     , if1(store, m, false()) ->
       if3(store, m, empty(fstsplit(m, app(map_f(self(), nil()), 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) }
   Weak DPs:
     { fstsplit^#(0(), x) -> c_1()
     , fstsplit^#(s(n), nil()) -> c_2()
     , sndsplit^#(s(n), nil()) -> c_5()
     , empty^#(nil()) -> c_7()
     , empty^#(cons(h, t)) -> c_8()
     , leq^#(0(), m) -> c_9()
     , leq^#(s(n), 0()) -> c_10()
     , length^#(nil()) -> c_12()
     , map_f^#(pid, nil()) -> c_16()
     , map_f^#(pid, cons(h, t)) ->
       c_17(app^#(f(pid, h), map_f(pid, t))) }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   Empty strict component of the problem is NOT empty.


Arrrr..