MAYBE

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

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


Arrrr..