MAYBE
Time: 0.930736
TRS:
 {      leq(0(), y) -> true(),
      leq(s x, 0()) -> false(),
      leq(s x, s y) -> leq(x, y),
   if(true(), x, y) -> x,
  if(false(), x, y) -> y,
          -(x, 0()) -> x,
        -(s x, s y) -> -(x, y),
        mod(0(), y) -> 0(),
      mod(s x, 0()) -> 0(),
      mod(s x, s y) -> if(leq(y, x), mod(-(s x, s y), s y), s x)}
 DP:
  DP:
   {leq#(s x, s y) -> leq#(x, y),
      -#(s x, s y) -> -#(x, y),
    mod#(s x, s y) -> leq#(y, x),
    mod#(s x, s y) -> if#(leq(y, x), mod(-(s x, s y), s y), s x),
    mod#(s x, s y) -> -#(s x, s y),
    mod#(s x, s y) -> mod#(-(s x, s y), s y)}
  TRS:
  {      leq(0(), y) -> true(),
       leq(s x, 0()) -> false(),
       leq(s x, s y) -> leq(x, y),
    if(true(), x, y) -> x,
   if(false(), x, y) -> y,
           -(x, 0()) -> x,
         -(s x, s y) -> -(x, y),
         mod(0(), y) -> 0(),
       mod(s x, 0()) -> 0(),
       mod(s x, s y) -> if(leq(y, x), mod(-(s x, s y), s y), s x)}
  UR:
   {      leq(0(), y) -> true(),
        leq(s x, 0()) -> false(),
        leq(s x, s y) -> leq(x, y),
     if(true(), x, y) -> x,
    if(false(), x, y) -> y,
            -(x, 0()) -> x,
          -(s x, s y) -> -(x, y),
          mod(0(), y) -> 0(),
        mod(s x, s y) -> if(leq(y, x), mod(-(s x, s y), s y), s x),
              a(z, w) -> z,
              a(z, w) -> w}
   EDG:
    {(leq#(s x, s y) -> leq#(x, y), leq#(s x, s y) -> leq#(x, y))
     (mod#(s x, s y) -> mod#(-(s x, s y), s y), mod#(s x, s y) -> mod#(-(s x, s y), s y))
     (mod#(s x, s y) -> mod#(-(s x, s y), s y), mod#(s x, s y) -> -#(s x, s y))
     (mod#(s x, s y) -> mod#(-(s x, s y), s y), mod#(s x, s y) -> if#(leq(y, x), mod(-(s x, s y), s y), s x))
     (mod#(s x, s y) -> mod#(-(s x, s y), s y), mod#(s x, s y) -> leq#(y, x))
     (mod#(s x, s y) -> -#(s x, s y), -#(s x, s y) -> -#(x, y))
     (-#(s x, s y) -> -#(x, y), -#(s x, s y) -> -#(x, y))
     (mod#(s x, s y) -> leq#(y, x), leq#(s x, s y) -> leq#(x, y))}
    STATUS:
     arrows: 0.777778
     SCCS (3):
      Scc:
       {mod#(s x, s y) -> mod#(-(s x, s y), s y)}
      Scc:
       {-#(s x, s y) -> -#(x, y)}
      Scc:
       {leq#(s x, s y) -> leq#(x, y)}
      
      SCC (1):
       Strict:
        {mod#(s x, s y) -> mod#(-(s x, s y), s y)}
       Weak:
       {      leq(0(), y) -> true(),
            leq(s x, 0()) -> false(),
            leq(s x, s y) -> leq(x, y),
         if(true(), x, y) -> x,
        if(false(), x, y) -> y,
                -(x, 0()) -> x,
              -(s x, s y) -> -(x, y),
              mod(0(), y) -> 0(),
            mod(s x, 0()) -> 0(),
            mod(s x, s y) -> if(leq(y, x), mod(-(s x, s y), s y), s x)}
       Open
      
      
      SCC (1):
       Strict:
        {-#(s x, s y) -> -#(x, y)}
       Weak:
       {      leq(0(), y) -> true(),
            leq(s x, 0()) -> false(),
            leq(s x, s y) -> leq(x, y),
         if(true(), x, y) -> x,
        if(false(), x, y) -> y,
                -(x, 0()) -> x,
              -(s x, s y) -> -(x, y),
              mod(0(), y) -> 0(),
            mod(s x, 0()) -> 0(),
            mod(s x, s y) -> if(leq(y, x), mod(-(s x, s y), s y), s x)}
       Open
      
      SCC (1):
       Strict:
        {leq#(s x, s y) -> leq#(x, y)}
       Weak:
       {      leq(0(), y) -> true(),
            leq(s x, 0()) -> false(),
            leq(s x, s y) -> leq(x, y),
         if(true(), x, y) -> x,
        if(false(), x, y) -> y,
                -(x, 0()) -> x,
              -(s x, s y) -> -(x, y),
              mod(0(), y) -> 0(),
            mod(s x, 0()) -> 0(),
            mod(s x, s y) -> if(leq(y, x), mod(-(s x, s y), s y), s x)}
       Open