MAYBE
Time: 0.001289
TRS:
 {            lt(x, 0()) -> false(),
            lt(0(), s y) -> true(),
            lt(s x, s y) -> lt(x, y),
            plus(x, 0()) -> x,
            plus(x, s y) -> s plus(x, y),
         help(x, s y, c) -> if(lt(c, x), x, s y, c),
            quot(x, s y) -> help(x, s y, 0()),
  if(false(), x, s y, c) -> 0(),
   if(true(), x, s y, c) -> s help(x, s y, plus(c, s y))}
 DP:
  DP:
   {         lt#(s x, s y) -> lt#(x, y),
             plus#(x, s y) -> plus#(x, y),
          help#(x, s y, c) -> lt#(c, x),
          help#(x, s y, c) -> if#(lt(c, x), x, s y, c),
             quot#(x, s y) -> help#(x, s y, 0()),
    if#(true(), x, s y, c) -> plus#(c, s y),
    if#(true(), x, s y, c) -> help#(x, s y, plus(c, s y))}
  TRS:
  {            lt(x, 0()) -> false(),
             lt(0(), s y) -> true(),
             lt(s x, s y) -> lt(x, y),
             plus(x, 0()) -> x,
             plus(x, s y) -> s plus(x, y),
          help(x, s y, c) -> if(lt(c, x), x, s y, c),
             quot(x, s y) -> help(x, s y, 0()),
   if(false(), x, s y, c) -> 0(),
    if(true(), x, s y, c) -> s help(x, s y, plus(c, s y))}
  UR:
   {  lt(x, 0()) -> false(),
    lt(0(), s y) -> true(),
    lt(s x, s y) -> lt(x, y),
    plus(x, 0()) -> x,
    plus(x, s y) -> s plus(x, y),
         a(z, w) -> z,
         a(z, w) -> w}
   EDG:
    {(if#(true(), x, s y, c) -> plus#(c, s y), plus#(x, s y) -> plus#(x, y))
     (plus#(x, s y) -> plus#(x, y), plus#(x, s y) -> plus#(x, y))
     (quot#(x, s y) -> help#(x, s y, 0()), help#(x, s y, c) -> if#(lt(c, x), x, s y, c))
     (quot#(x, s y) -> help#(x, s y, 0()), help#(x, s y, c) -> lt#(c, x))
     (help#(x, s y, c) -> if#(lt(c, x), x, s y, c), if#(true(), x, s y, c) -> plus#(c, s y))
     (help#(x, s y, c) -> if#(lt(c, x), x, s y, c), if#(true(), x, s y, c) -> help#(x, s y, plus(c, s y)))
     (if#(true(), x, s y, c) -> help#(x, s y, plus(c, s y)), help#(x, s y, c) -> lt#(c, x))
     (if#(true(), x, s y, c) -> help#(x, s y, plus(c, s y)), help#(x, s y, c) -> if#(lt(c, x), x, s y, c))
     (lt#(s x, s y) -> lt#(x, y), lt#(s x, s y) -> lt#(x, y))
     (help#(x, s y, c) -> lt#(c, x), lt#(s x, s y) -> lt#(x, y))}
    STATUS:
     arrows: 0.795918
     SCCS (3):
      Scc:
       {      help#(x, s y, c) -> if#(lt(c, x), x, s y, c),
        if#(true(), x, s y, c) -> help#(x, s y, plus(c, s y))}
      Scc:
       {plus#(x, s y) -> plus#(x, y)}
      Scc:
       {lt#(s x, s y) -> lt#(x, y)}
      
      
      SCC (2):
       Strict:
        {      help#(x, s y, c) -> if#(lt(c, x), x, s y, c),
         if#(true(), x, s y, c) -> help#(x, s y, plus(c, s y))}
       Weak:
       {            lt(x, 0()) -> false(),
                  lt(0(), s y) -> true(),
                  lt(s x, s y) -> lt(x, y),
                  plus(x, 0()) -> x,
                  plus(x, s y) -> s plus(x, y),
               help(x, s y, c) -> if(lt(c, x), x, s y, c),
                  quot(x, s y) -> help(x, s y, 0()),
        if(false(), x, s y, c) -> 0(),
         if(true(), x, s y, c) -> s help(x, s y, plus(c, s y))}
       Open
      
      SCC (1):
       Strict:
        {plus#(x, s y) -> plus#(x, y)}
       Weak:
       {            lt(x, 0()) -> false(),
                  lt(0(), s y) -> true(),
                  lt(s x, s y) -> lt(x, y),
                  plus(x, 0()) -> x,
                  plus(x, s y) -> s plus(x, y),
               help(x, s y, c) -> if(lt(c, x), x, s y, c),
                  quot(x, s y) -> help(x, s y, 0()),
        if(false(), x, s y, c) -> 0(),
         if(true(), x, s y, c) -> s help(x, s y, plus(c, s y))}
       Open
      
      SCC (1):
       Strict:
        {lt#(s x, s y) -> lt#(x, y)}
       Weak:
       {            lt(x, 0()) -> false(),
                  lt(0(), s y) -> true(),
                  lt(s x, s y) -> lt(x, y),
                  plus(x, 0()) -> x,
                  plus(x, s y) -> s plus(x, y),
               help(x, s y, c) -> if(lt(c, x), x, s y, c),
                  quot(x, s y) -> help(x, s y, 0()),
        if(false(), x, s y, c) -> 0(),
         if(true(), x, s y, c) -> s help(x, s y, plus(c, s y))}
       Open