MAYBE

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

Strict Trs:
  { minus_active(x, y) -> minus(x, y)
  , minus_active(0(), y) -> 0()
  , minus_active(s(x), s(y)) -> minus_active(x, y)
  , mark(0()) -> 0()
  , mark(s(x)) -> s(mark(x))
  , mark(minus(x, y)) -> minus_active(x, y)
  , mark(ge(x, y)) -> ge_active(x, y)
  , mark(div(x, y)) -> div_active(mark(x), y)
  , mark(if(x, y, z)) -> if_active(mark(x), y, z)
  , ge_active(x, y) -> ge(x, y)
  , ge_active(x, 0()) -> true()
  , ge_active(0(), s(y)) -> false()
  , ge_active(s(x), s(y)) -> ge_active(x, y)
  , div_active(x, y) -> div(x, y)
  , div_active(0(), s(y)) -> 0()
  , div_active(s(x), s(y)) ->
    if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0())
  , if_active(x, y, z) -> if(x, y, z)
  , if_active(true(), x, y) -> mark(x)
  , if_active(false(), x, y) -> mark(y) }
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) '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
      
      2) '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
      
   
   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:
     { minus_active^#(x, y) -> c_1(x, y)
     , minus_active^#(0(), y) -> c_2()
     , minus_active^#(s(x), s(y)) -> c_3(minus_active^#(x, y))
     , mark^#(0()) -> c_4()
     , mark^#(s(x)) -> c_5(mark^#(x))
     , mark^#(minus(x, y)) -> c_6(minus_active^#(x, y))
     , mark^#(ge(x, y)) -> c_7(ge_active^#(x, y))
     , mark^#(div(x, y)) -> c_8(div_active^#(mark(x), y))
     , mark^#(if(x, y, z)) -> c_9(if_active^#(mark(x), y, z))
     , ge_active^#(x, y) -> c_10(x, y)
     , ge_active^#(x, 0()) -> c_11()
     , ge_active^#(0(), s(y)) -> c_12()
     , ge_active^#(s(x), s(y)) -> c_13(ge_active^#(x, y))
     , div_active^#(x, y) -> c_14(x, y)
     , div_active^#(0(), s(y)) -> c_15()
     , div_active^#(s(x), s(y)) ->
       c_16(if_active^#(ge_active(x, y), s(div(minus(x, y), s(y))), 0()))
     , if_active^#(x, y, z) -> c_17(x, y, z)
     , if_active^#(true(), x, y) -> c_18(mark^#(x))
     , if_active^#(false(), x, y) -> c_19(mark^#(y)) }
   
   and mark the set of starting terms.
   
   We are left with following problem, upon which TcT provides the
   certificate MAYBE.
   
   Strict DPs:
     { minus_active^#(x, y) -> c_1(x, y)
     , minus_active^#(0(), y) -> c_2()
     , minus_active^#(s(x), s(y)) -> c_3(minus_active^#(x, y))
     , mark^#(0()) -> c_4()
     , mark^#(s(x)) -> c_5(mark^#(x))
     , mark^#(minus(x, y)) -> c_6(minus_active^#(x, y))
     , mark^#(ge(x, y)) -> c_7(ge_active^#(x, y))
     , mark^#(div(x, y)) -> c_8(div_active^#(mark(x), y))
     , mark^#(if(x, y, z)) -> c_9(if_active^#(mark(x), y, z))
     , ge_active^#(x, y) -> c_10(x, y)
     , ge_active^#(x, 0()) -> c_11()
     , ge_active^#(0(), s(y)) -> c_12()
     , ge_active^#(s(x), s(y)) -> c_13(ge_active^#(x, y))
     , div_active^#(x, y) -> c_14(x, y)
     , div_active^#(0(), s(y)) -> c_15()
     , div_active^#(s(x), s(y)) ->
       c_16(if_active^#(ge_active(x, y), s(div(minus(x, y), s(y))), 0()))
     , if_active^#(x, y, z) -> c_17(x, y, z)
     , if_active^#(true(), x, y) -> c_18(mark^#(x))
     , if_active^#(false(), x, y) -> c_19(mark^#(y)) }
   Strict Trs:
     { minus_active(x, y) -> minus(x, y)
     , minus_active(0(), y) -> 0()
     , minus_active(s(x), s(y)) -> minus_active(x, y)
     , mark(0()) -> 0()
     , mark(s(x)) -> s(mark(x))
     , mark(minus(x, y)) -> minus_active(x, y)
     , mark(ge(x, y)) -> ge_active(x, y)
     , mark(div(x, y)) -> div_active(mark(x), y)
     , mark(if(x, y, z)) -> if_active(mark(x), y, z)
     , ge_active(x, y) -> ge(x, y)
     , ge_active(x, 0()) -> true()
     , ge_active(0(), s(y)) -> false()
     , ge_active(s(x), s(y)) -> ge_active(x, y)
     , div_active(x, y) -> div(x, y)
     , div_active(0(), s(y)) -> 0()
     , div_active(s(x), s(y)) ->
       if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0())
     , if_active(x, y, z) -> if(x, y, z)
     , if_active(true(), x, y) -> mark(x)
     , if_active(false(), x, y) -> mark(y) }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   We estimate the number of application of {2,4,11,12,15} by
   applications of Pre({2,4,11,12,15}) =
   {1,3,5,6,7,8,10,13,14,17,18,19}. Here rules are labeled as follows:
   
     DPs:
       { 1: minus_active^#(x, y) -> c_1(x, y)
       , 2: minus_active^#(0(), y) -> c_2()
       , 3: minus_active^#(s(x), s(y)) -> c_3(minus_active^#(x, y))
       , 4: mark^#(0()) -> c_4()
       , 5: mark^#(s(x)) -> c_5(mark^#(x))
       , 6: mark^#(minus(x, y)) -> c_6(minus_active^#(x, y))
       , 7: mark^#(ge(x, y)) -> c_7(ge_active^#(x, y))
       , 8: mark^#(div(x, y)) -> c_8(div_active^#(mark(x), y))
       , 9: mark^#(if(x, y, z)) -> c_9(if_active^#(mark(x), y, z))
       , 10: ge_active^#(x, y) -> c_10(x, y)
       , 11: ge_active^#(x, 0()) -> c_11()
       , 12: ge_active^#(0(), s(y)) -> c_12()
       , 13: ge_active^#(s(x), s(y)) -> c_13(ge_active^#(x, y))
       , 14: div_active^#(x, y) -> c_14(x, y)
       , 15: div_active^#(0(), s(y)) -> c_15()
       , 16: div_active^#(s(x), s(y)) ->
             c_16(if_active^#(ge_active(x, y), s(div(minus(x, y), s(y))), 0()))
       , 17: if_active^#(x, y, z) -> c_17(x, y, z)
       , 18: if_active^#(true(), x, y) -> c_18(mark^#(x))
       , 19: if_active^#(false(), x, y) -> c_19(mark^#(y)) }
   
   We are left with following problem, upon which TcT provides the
   certificate MAYBE.
   
   Strict DPs:
     { minus_active^#(x, y) -> c_1(x, y)
     , minus_active^#(s(x), s(y)) -> c_3(minus_active^#(x, y))
     , mark^#(s(x)) -> c_5(mark^#(x))
     , mark^#(minus(x, y)) -> c_6(minus_active^#(x, y))
     , mark^#(ge(x, y)) -> c_7(ge_active^#(x, y))
     , mark^#(div(x, y)) -> c_8(div_active^#(mark(x), y))
     , mark^#(if(x, y, z)) -> c_9(if_active^#(mark(x), y, z))
     , ge_active^#(x, y) -> c_10(x, y)
     , ge_active^#(s(x), s(y)) -> c_13(ge_active^#(x, y))
     , div_active^#(x, y) -> c_14(x, y)
     , div_active^#(s(x), s(y)) ->
       c_16(if_active^#(ge_active(x, y), s(div(minus(x, y), s(y))), 0()))
     , if_active^#(x, y, z) -> c_17(x, y, z)
     , if_active^#(true(), x, y) -> c_18(mark^#(x))
     , if_active^#(false(), x, y) -> c_19(mark^#(y)) }
   Strict Trs:
     { minus_active(x, y) -> minus(x, y)
     , minus_active(0(), y) -> 0()
     , minus_active(s(x), s(y)) -> minus_active(x, y)
     , mark(0()) -> 0()
     , mark(s(x)) -> s(mark(x))
     , mark(minus(x, y)) -> minus_active(x, y)
     , mark(ge(x, y)) -> ge_active(x, y)
     , mark(div(x, y)) -> div_active(mark(x), y)
     , mark(if(x, y, z)) -> if_active(mark(x), y, z)
     , ge_active(x, y) -> ge(x, y)
     , ge_active(x, 0()) -> true()
     , ge_active(0(), s(y)) -> false()
     , ge_active(s(x), s(y)) -> ge_active(x, y)
     , div_active(x, y) -> div(x, y)
     , div_active(0(), s(y)) -> 0()
     , div_active(s(x), s(y)) ->
       if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0())
     , if_active(x, y, z) -> if(x, y, z)
     , if_active(true(), x, y) -> mark(x)
     , if_active(false(), x, y) -> mark(y) }
   Weak DPs:
     { minus_active^#(0(), y) -> c_2()
     , mark^#(0()) -> c_4()
     , ge_active^#(x, 0()) -> c_11()
     , ge_active^#(0(), s(y)) -> c_12()
     , div_active^#(0(), s(y)) -> c_15() }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   Empty strict component of the problem is NOT empty.


Arrrr..