MAYBE

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

Strict Trs:
  { eq(0(), 0()) -> true()
  , eq(0(), s(x)) -> false()
  , eq(s(x), 0()) -> false()
  , eq(s(x), s(y)) -> eq(x, y)
  , or(true(), y) -> true()
  , or(false(), y) -> y
  , and(true(), y) -> y
  , and(false(), y) -> false()
  , size(empty()) -> 0()
  , size(edge(x, y, i)) -> s(size(i))
  , le(0(), y) -> true()
  , le(s(x), 0()) -> false()
  , le(s(x), s(y)) -> le(x, y)
  , reachable(x, y, i) -> reach(x, y, 0(), i, i)
  , reach(x, y, c, i, j) -> if1(eq(x, y), x, y, c, i, j)
  , if1(true(), x, y, c, i, j) -> true()
  , if1(false(), x, y, c, i, j) -> if2(le(c, size(j)), x, y, c, i, j)
  , if2(true(), x, y, c, empty(), j) -> false()
  , if2(true(), x, y, c, edge(u, v, i), j) ->
    or(if2(true(), x, y, c, i, j),
       and(eq(x, u), reach(v, y, s(c), j, j)))
  , if2(false(), x, y, c, i, j) -> false() }
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) '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) '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) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed
   due to the following reason:
   
   We add the following weak dependency pairs:
   
   Strict DPs:
     { eq^#(0(), 0()) -> c_1()
     , eq^#(0(), s(x)) -> c_2()
     , eq^#(s(x), 0()) -> c_3()
     , eq^#(s(x), s(y)) -> c_4(eq^#(x, y))
     , or^#(true(), y) -> c_5()
     , or^#(false(), y) -> c_6(y)
     , and^#(true(), y) -> c_7(y)
     , and^#(false(), y) -> c_8()
     , size^#(empty()) -> c_9()
     , size^#(edge(x, y, i)) -> c_10(size^#(i))
     , le^#(0(), y) -> c_11()
     , le^#(s(x), 0()) -> c_12()
     , le^#(s(x), s(y)) -> c_13(le^#(x, y))
     , reachable^#(x, y, i) -> c_14(reach^#(x, y, 0(), i, i))
     , reach^#(x, y, c, i, j) -> c_15(if1^#(eq(x, y), x, y, c, i, j))
     , if1^#(true(), x, y, c, i, j) -> c_16()
     , if1^#(false(), x, y, c, i, j) ->
       c_17(if2^#(le(c, size(j)), x, y, c, i, j))
     , if2^#(true(), x, y, c, empty(), j) -> c_18()
     , if2^#(true(), x, y, c, edge(u, v, i), j) ->
       c_19(or^#(if2(true(), x, y, c, i, j),
                 and(eq(x, u), reach(v, y, s(c), j, j))))
     , if2^#(false(), x, y, c, i, j) -> c_20() }
   
   and mark the set of starting terms.
   
   We are left with following problem, upon which TcT provides the
   certificate MAYBE.
   
   Strict DPs:
     { eq^#(0(), 0()) -> c_1()
     , eq^#(0(), s(x)) -> c_2()
     , eq^#(s(x), 0()) -> c_3()
     , eq^#(s(x), s(y)) -> c_4(eq^#(x, y))
     , or^#(true(), y) -> c_5()
     , or^#(false(), y) -> c_6(y)
     , and^#(true(), y) -> c_7(y)
     , and^#(false(), y) -> c_8()
     , size^#(empty()) -> c_9()
     , size^#(edge(x, y, i)) -> c_10(size^#(i))
     , le^#(0(), y) -> c_11()
     , le^#(s(x), 0()) -> c_12()
     , le^#(s(x), s(y)) -> c_13(le^#(x, y))
     , reachable^#(x, y, i) -> c_14(reach^#(x, y, 0(), i, i))
     , reach^#(x, y, c, i, j) -> c_15(if1^#(eq(x, y), x, y, c, i, j))
     , if1^#(true(), x, y, c, i, j) -> c_16()
     , if1^#(false(), x, y, c, i, j) ->
       c_17(if2^#(le(c, size(j)), x, y, c, i, j))
     , if2^#(true(), x, y, c, empty(), j) -> c_18()
     , if2^#(true(), x, y, c, edge(u, v, i), j) ->
       c_19(or^#(if2(true(), x, y, c, i, j),
                 and(eq(x, u), reach(v, y, s(c), j, j))))
     , if2^#(false(), x, y, c, i, j) -> c_20() }
   Strict Trs:
     { eq(0(), 0()) -> true()
     , eq(0(), s(x)) -> false()
     , eq(s(x), 0()) -> false()
     , eq(s(x), s(y)) -> eq(x, y)
     , or(true(), y) -> true()
     , or(false(), y) -> y
     , and(true(), y) -> y
     , and(false(), y) -> false()
     , size(empty()) -> 0()
     , size(edge(x, y, i)) -> s(size(i))
     , le(0(), y) -> true()
     , le(s(x), 0()) -> false()
     , le(s(x), s(y)) -> le(x, y)
     , reachable(x, y, i) -> reach(x, y, 0(), i, i)
     , reach(x, y, c, i, j) -> if1(eq(x, y), x, y, c, i, j)
     , if1(true(), x, y, c, i, j) -> true()
     , if1(false(), x, y, c, i, j) -> if2(le(c, size(j)), x, y, c, i, j)
     , if2(true(), x, y, c, empty(), j) -> false()
     , if2(true(), x, y, c, edge(u, v, i), j) ->
       or(if2(true(), x, y, c, i, j),
          and(eq(x, u), reach(v, y, s(c), j, j)))
     , if2(false(), x, y, c, i, j) -> false() }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   We estimate the number of application of
   {1,2,3,5,8,9,11,12,16,18,20} by applications of
   Pre({1,2,3,5,8,9,11,12,16,18,20}) = {4,6,7,10,13,15,17,19}. Here
   rules are labeled as follows:
   
     DPs:
       { 1: eq^#(0(), 0()) -> c_1()
       , 2: eq^#(0(), s(x)) -> c_2()
       , 3: eq^#(s(x), 0()) -> c_3()
       , 4: eq^#(s(x), s(y)) -> c_4(eq^#(x, y))
       , 5: or^#(true(), y) -> c_5()
       , 6: or^#(false(), y) -> c_6(y)
       , 7: and^#(true(), y) -> c_7(y)
       , 8: and^#(false(), y) -> c_8()
       , 9: size^#(empty()) -> c_9()
       , 10: size^#(edge(x, y, i)) -> c_10(size^#(i))
       , 11: le^#(0(), y) -> c_11()
       , 12: le^#(s(x), 0()) -> c_12()
       , 13: le^#(s(x), s(y)) -> c_13(le^#(x, y))
       , 14: reachable^#(x, y, i) -> c_14(reach^#(x, y, 0(), i, i))
       , 15: reach^#(x, y, c, i, j) ->
             c_15(if1^#(eq(x, y), x, y, c, i, j))
       , 16: if1^#(true(), x, y, c, i, j) -> c_16()
       , 17: if1^#(false(), x, y, c, i, j) ->
             c_17(if2^#(le(c, size(j)), x, y, c, i, j))
       , 18: if2^#(true(), x, y, c, empty(), j) -> c_18()
       , 19: if2^#(true(), x, y, c, edge(u, v, i), j) ->
             c_19(or^#(if2(true(), x, y, c, i, j),
                       and(eq(x, u), reach(v, y, s(c), j, j))))
       , 20: if2^#(false(), x, y, c, i, j) -> c_20() }
   
   We are left with following problem, upon which TcT provides the
   certificate MAYBE.
   
   Strict DPs:
     { eq^#(s(x), s(y)) -> c_4(eq^#(x, y))
     , or^#(false(), y) -> c_6(y)
     , and^#(true(), y) -> c_7(y)
     , size^#(edge(x, y, i)) -> c_10(size^#(i))
     , le^#(s(x), s(y)) -> c_13(le^#(x, y))
     , reachable^#(x, y, i) -> c_14(reach^#(x, y, 0(), i, i))
     , reach^#(x, y, c, i, j) -> c_15(if1^#(eq(x, y), x, y, c, i, j))
     , if1^#(false(), x, y, c, i, j) ->
       c_17(if2^#(le(c, size(j)), x, y, c, i, j))
     , if2^#(true(), x, y, c, edge(u, v, i), j) ->
       c_19(or^#(if2(true(), x, y, c, i, j),
                 and(eq(x, u), reach(v, y, s(c), j, j)))) }
   Strict Trs:
     { eq(0(), 0()) -> true()
     , eq(0(), s(x)) -> false()
     , eq(s(x), 0()) -> false()
     , eq(s(x), s(y)) -> eq(x, y)
     , or(true(), y) -> true()
     , or(false(), y) -> y
     , and(true(), y) -> y
     , and(false(), y) -> false()
     , size(empty()) -> 0()
     , size(edge(x, y, i)) -> s(size(i))
     , le(0(), y) -> true()
     , le(s(x), 0()) -> false()
     , le(s(x), s(y)) -> le(x, y)
     , reachable(x, y, i) -> reach(x, y, 0(), i, i)
     , reach(x, y, c, i, j) -> if1(eq(x, y), x, y, c, i, j)
     , if1(true(), x, y, c, i, j) -> true()
     , if1(false(), x, y, c, i, j) -> if2(le(c, size(j)), x, y, c, i, j)
     , if2(true(), x, y, c, empty(), j) -> false()
     , if2(true(), x, y, c, edge(u, v, i), j) ->
       or(if2(true(), x, y, c, i, j),
          and(eq(x, u), reach(v, y, s(c), j, j)))
     , if2(false(), x, y, c, i, j) -> false() }
   Weak DPs:
     { eq^#(0(), 0()) -> c_1()
     , eq^#(0(), s(x)) -> c_2()
     , eq^#(s(x), 0()) -> c_3()
     , or^#(true(), y) -> c_5()
     , and^#(false(), y) -> c_8()
     , size^#(empty()) -> c_9()
     , le^#(0(), y) -> c_11()
     , le^#(s(x), 0()) -> c_12()
     , if1^#(true(), x, y, c, i, j) -> c_16()
     , if2^#(true(), x, y, c, empty(), j) -> c_18()
     , if2^#(false(), x, y, c, i, j) -> c_20() }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   Empty strict component of the problem is NOT empty.


Arrrr..