MAYBE

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

Strict Trs:
  { l5(x, y, res, tmp, mtmp, True()) -> 0()
  , l5(x, y, res, tmp, mtmp, False()) ->
    l7(x, y, res, tmp, mtmp, False())
  , l1(x, y, res, tmp, mtmp, t) -> l2(x, y, res, tmp, mtmp, False())
  , l13(x, y, res, tmp, True(), t) ->
    l16(x, y, gcd(S(0()), y), tmp, True(), t)
  , l13(x, y, res, tmp, False(), t) ->
    l16(x, y, gcd(0(), y), tmp, False(), t)
  , help1(S(S(x))) -> True()
  , help1(S(0())) -> False()
  , help1(0()) -> False()
  , gcd(x, y) -> l1(x, y, 0(), False(), False(), False())
  , e7(a, b, res, t) -> False()
  , m3(S(S(x)), b, res, t) -> True()
  , m3(S(0()), b, res, t) -> False()
  , m3(0(), b, res, t) -> False()
  , e2(a, b, res, True()) -> e3(a, b, res, True())
  , e2(a, b, res, False()) -> False()
  , e3(a, b, res, t) -> e4(a, b, res, <(b, a))
  , e6(a, b, res, t) -> False()
  , l14(x, y, res, tmp, mtmp, t) ->
    l15(x, y, res, tmp, monus(x, y), t)
  , l9(res, y, res', tmp, mtmp, t) -> res
  , bool2Nat(True()) -> S(0())
  , bool2Nat(False()) -> 0()
  , l6(x, y, res, tmp, mtmp, t) -> 0()
  , l8(res, y, res', True(), mtmp, t) -> res
  , l8(x, y, res, False(), mtmp, t) ->
    l10(x, y, res, False(), mtmp, t)
  , m5(a, b, res, t) -> res
  , e1(a, b, res, t) -> e2(a, b, res, <(a, b))
  , m4(S(x'), S(x), res, t) -> m5(S(x'), S(x), monus(x', x), t)
  , equal0(a, b) -> e1(a, b, False(), False())
  , l12(x, y, res, tmp, mtmp, t) ->
    l13(x, y, res, tmp, monus(x, y), t)
  , e8(a, b, res, t) -> res
  , l7(x, y, res, tmp, mtmp, t) ->
    l8(x, y, res, equal0(x, y), mtmp, t)
  , l11(x, y, res, tmp, mtmp, True()) ->
    l12(x, y, res, tmp, mtmp, True())
  , l11(x, y, res, tmp, mtmp, False()) ->
    l14(x, y, res, tmp, mtmp, False())
  , e5(a, b, res, t) -> True()
  , l3(x, y, res, tmp, mtmp, t) -> l4(x, y, 0(), tmp, mtmp, t)
  , m2(a, b, res, False()) -> m4(a, b, res, False())
  , m2(S(S(x)), b, res, True()) -> True()
  , m2(S(0()), b, res, True()) -> False()
  , m2(0(), b, res, True()) -> False()
  , monus(a, b) -> m1(a, b, False(), False())
  , l2(x, y, res, tmp, mtmp, True()) -> res
  , l2(x, y, res, tmp, mtmp, False()) ->
    l3(x, y, res, tmp, mtmp, False())
  , l4(x', x, res, tmp, mtmp, t) ->
    l5(x', x, res, tmp, mtmp, False())
  , l10(x, y, res, tmp, mtmp, t) ->
    l11(x, y, res, tmp, mtmp, <(x, y))
  , l15(x, y, res, tmp, True(), t) ->
    l16(x, y, gcd(y, S(0())), tmp, True(), t)
  , l15(x, y, res, tmp, False(), t) ->
    l16(x, y, gcd(y, 0()), tmp, False(), t)
  , l16(x, y, res, tmp, mtmp, t) -> res
  , m1(a, x, res, t) -> m2(a, x, res, False())
  , e4(a, b, res, True()) -> True()
  , e4(a, b, res, False()) -> False() }
Weak Trs:
  { <(x, 0()) -> False()
  , <(S(x), S(y)) -> <(x, y)
  , <(0(), S(y)) -> True() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

None of the processors succeeded.

Details of failed attempt(s):
-----------------------------
1) 'empty' failed due to the following reason:
   
   Empty strict component of the problem is NOT empty.

2) 'Best' failed due to the following reason:
   
   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 input cannot be shown compatible
         
         2) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due
            to the following reason:
            
            The input cannot be shown compatible
         
      
      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 minimal-enrichment and initial automaton 'match''
            failed due to the following reason:
            
            match-boundness of the problem could not be verified.
         
         2) 'Bounds with perSymbol-enrichment and initial automaton 'match''
            failed due to the following reason:
            
            match-boundness of the problem could not be verified.
         
      
   


Arrrr..