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