MAYBE
Time: 0.005004
TRS:
 {            le(0(), y) -> true(),
            le(s x, 0()) -> false(),
            le(s x, s y) -> le(x, y),
           minus(x, 0()) -> x,
         minus(0(), s y) -> 0(),
         minus(s x, s y) -> minus(x, y),
            plus(x, 0()) -> x,
            plus(x, s y) -> s plus(x, y),
             mod(x, s y) -> help(x, s y, 0()),
           mod(s x, 0()) -> 0(),
         help(x, s y, c) -> if(le(c, x), x, s y, c),
   if(true(), x, s y, c) -> help(x, s y, plus(c, s y)),
  if(false(), x, s y, c) -> minus(x, minus(c, s y))}
 DP:
  DP:
   {          le#(s x, s y) -> le#(x, y),
           minus#(s x, s y) -> minus#(x, y),
              plus#(x, s y) -> plus#(x, y),
               mod#(x, s y) -> help#(x, s y, 0()),
           help#(x, s y, c) -> le#(c, x),
           help#(x, s y, c) -> if#(le(c, x), x, s y, c),
     if#(true(), x, s y, c) -> plus#(c, s y),
     if#(true(), x, s y, c) -> help#(x, s y, plus(c, s y)),
    if#(false(), x, s y, c) -> minus#(x, minus(c, s y)),
    if#(false(), x, s y, c) -> minus#(c, s y)}
  TRS:
  {            le(0(), y) -> true(),
             le(s x, 0()) -> false(),
             le(s x, s y) -> le(x, y),
            minus(x, 0()) -> x,
          minus(0(), s y) -> 0(),
          minus(s x, s y) -> minus(x, y),
             plus(x, 0()) -> x,
             plus(x, s y) -> s plus(x, y),
              mod(x, s y) -> help(x, s y, 0()),
            mod(s x, 0()) -> 0(),
          help(x, s y, c) -> if(le(c, x), x, s y, c),
    if(true(), x, s y, c) -> help(x, s y, plus(c, s y)),
   if(false(), x, s y, c) -> minus(x, minus(c, s y))}
  EDG:
   {(if#(true(), x, s y, c) -> plus#(c, s y), plus#(x, s y) -> plus#(x, y))
    (help#(x, s y, c) -> if#(le(c, x), x, s y, c), if#(false(), x, s y, c) -> minus#(c, s y))
    (help#(x, s y, c) -> if#(le(c, x), x, s y, c), if#(false(), x, s y, c) -> minus#(x, minus(c, s y)))
    (help#(x, s y, c) -> if#(le(c, x), x, s y, c), if#(true(), x, s y, c) -> help#(x, s y, plus(c, s y)))
    (help#(x, s y, c) -> if#(le(c, x), x, s y, c), if#(true(), x, s y, c) -> plus#(c, s y))
    (if#(true(), x, s y, c) -> help#(x, s y, plus(c, s y)), help#(x, s y, c) -> if#(le(c, x), x, s y, c))
    (if#(true(), x, s y, c) -> help#(x, s y, plus(c, s y)), help#(x, s y, c) -> le#(c, x))
    (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
    (mod#(x, s y) -> help#(x, s y, 0()), help#(x, s y, c) -> if#(le(c, x), x, s y, c))
    (mod#(x, s y) -> help#(x, s y, 0()), help#(x, s y, c) -> le#(c, x))
    (plus#(x, s y) -> plus#(x, y), plus#(x, s y) -> plus#(x, y))
    (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y))
    (help#(x, s y, c) -> le#(c, x), le#(s x, s y) -> le#(x, y))
    (if#(false(), x, s y, c) -> minus#(c, s y), minus#(s x, s y) -> minus#(x, y))
    (if#(false(), x, s y, c) -> minus#(x, minus(c, s y)), minus#(s x, s y) -> minus#(x, y))}
   STATUS:
    arrows: 0.850000
    SCCS (4):
     Scc:
      {      help#(x, s y, c) -> if#(le(c, x), x, s y, c),
       if#(true(), x, s y, c) -> help#(x, s y, plus(c, s y))}
     Scc:
      {le#(s x, s y) -> le#(x, y)}
     Scc:
      {plus#(x, s y) -> plus#(x, y)}
     Scc:
      {minus#(s x, s y) -> minus#(x, y)}
     
     
     SCC (2):
      Strict:
       {      help#(x, s y, c) -> if#(le(c, x), x, s y, c),
        if#(true(), x, s y, c) -> help#(x, s y, plus(c, s y))}
      Weak:
      {            le(0(), y) -> true(),
                 le(s x, 0()) -> false(),
                 le(s x, s y) -> le(x, y),
                minus(x, 0()) -> x,
              minus(0(), s y) -> 0(),
              minus(s x, s y) -> minus(x, y),
                 plus(x, 0()) -> x,
                 plus(x, s y) -> s plus(x, y),
                  mod(x, s y) -> help(x, s y, 0()),
                mod(s x, 0()) -> 0(),
              help(x, s y, c) -> if(le(c, x), x, s y, c),
        if(true(), x, s y, c) -> help(x, s y, plus(c, s y)),
       if(false(), x, s y, c) -> minus(x, minus(c, s y))}
      Open
     
     SCC (1):
      Strict:
       {le#(s x, s y) -> le#(x, y)}
      Weak:
      {            le(0(), y) -> true(),
                 le(s x, 0()) -> false(),
                 le(s x, s y) -> le(x, y),
                minus(x, 0()) -> x,
              minus(0(), s y) -> 0(),
              minus(s x, s y) -> minus(x, y),
                 plus(x, 0()) -> x,
                 plus(x, s y) -> s plus(x, y),
                  mod(x, s y) -> help(x, s y, 0()),
                mod(s x, 0()) -> 0(),
              help(x, s y, c) -> if(le(c, x), x, s y, c),
        if(true(), x, s y, c) -> help(x, s y, plus(c, s y)),
       if(false(), x, s y, c) -> minus(x, minus(c, s y))}
      Open
     
     
     SCC (1):
      Strict:
       {plus#(x, s y) -> plus#(x, y)}
      Weak:
      {            le(0(), y) -> true(),
                 le(s x, 0()) -> false(),
                 le(s x, s y) -> le(x, y),
                minus(x, 0()) -> x,
              minus(0(), s y) -> 0(),
              minus(s x, s y) -> minus(x, y),
                 plus(x, 0()) -> x,
                 plus(x, s y) -> s plus(x, y),
                  mod(x, s y) -> help(x, s y, 0()),
                mod(s x, 0()) -> 0(),
              help(x, s y, c) -> if(le(c, x), x, s y, c),
        if(true(), x, s y, c) -> help(x, s y, plus(c, s y)),
       if(false(), x, s y, c) -> minus(x, minus(c, s y))}
      Open
     
     SCC (1):
      Strict:
       {minus#(s x, s y) -> minus#(x, y)}
      Weak:
      {            le(0(), y) -> true(),
                 le(s x, 0()) -> false(),
                 le(s x, s y) -> le(x, y),
                minus(x, 0()) -> x,
              minus(0(), s y) -> 0(),
              minus(s x, s y) -> minus(x, y),
                 plus(x, 0()) -> x,
                 plus(x, s y) -> s plus(x, y),
                  mod(x, s y) -> help(x, s y, 0()),
                mod(s x, 0()) -> 0(),
              help(x, s y, c) -> if(le(c, x), x, s y, c),
        if(true(), x, s y, c) -> help(x, s y, plus(c, s y)),
       if(false(), x, s y, c) -> minus(x, minus(c, s y))}
      Open