MAYBE
Time: 0.480262
TRS:
 {                       le(0(), y) -> true(),
                       le(s x, 0()) -> false(),
                       le(s x, s y) -> le(x, y),
                        minus(x, x) -> 0(),
                      minus(x, 0()) -> x,
                      minus(0(), x) -> 0(),
                    minus(s x, s y) -> minus(x, y),
                         isZero 0() -> true(),
                         isZero s x -> false(),
         if_mod(true(), b, x, y, z) -> divByZeroError(),
   if_mod(false(), true(), x, y, z) -> mod(z, y),
  if_mod(false(), false(), x, y, z) -> x,
                          mod(x, y) -> if_mod(isZero y, le(y, x), x, y, minus(x, y))}
 DP:
  DP:
   {                    le#(s x, s y) -> le#(x, y),
                     minus#(s x, s y) -> minus#(x, y),
    if_mod#(false(), true(), x, y, z) -> mod#(z, y),
                           mod#(x, y) -> le#(y, x),
                           mod#(x, y) -> minus#(x, y),
                           mod#(x, y) -> isZero# y,
                           mod#(x, y) -> if_mod#(isZero y, le(y, x), x, y, minus(x, y))}
  TRS:
  {                       le(0(), y) -> true(),
                        le(s x, 0()) -> false(),
                        le(s x, s y) -> le(x, y),
                         minus(x, x) -> 0(),
                       minus(x, 0()) -> x,
                       minus(0(), x) -> 0(),
                     minus(s x, s y) -> minus(x, y),
                          isZero 0() -> true(),
                          isZero s x -> false(),
          if_mod(true(), b, x, y, z) -> divByZeroError(),
    if_mod(false(), true(), x, y, z) -> mod(z, y),
   if_mod(false(), false(), x, y, z) -> x,
                           mod(x, y) -> if_mod(isZero y, le(y, x), x, y, minus(x, y))}
  UR:
   {     le(0(), y) -> true(),
       le(s x, 0()) -> false(),
       le(s x, s y) -> le(x, y),
        minus(x, x) -> 0(),
      minus(x, 0()) -> x,
      minus(0(), x) -> 0(),
    minus(s x, s y) -> minus(x, y),
         isZero 0() -> true(),
         isZero s x -> false(),
            a(w, v) -> w,
            a(w, v) -> v}
   EDG:
    {(minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
     (mod#(x, y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
     (mod#(x, y) -> le#(y, x), le#(s x, s y) -> le#(x, y))
     (mod#(x, y) -> if_mod#(isZero y, le(y, x), x, y, minus(x, y)), if_mod#(false(), true(), x, y, z) -> mod#(z, y))
     (if_mod#(false(), true(), x, y, z) -> mod#(z, y), mod#(x, y) -> le#(y, x))
     (if_mod#(false(), true(), x, y, z) -> mod#(z, y), mod#(x, y) -> minus#(x, y))
     (if_mod#(false(), true(), x, y, z) -> mod#(z, y), mod#(x, y) -> isZero# y)
     (if_mod#(false(), true(), x, y, z) -> mod#(z, y), mod#(x, y) -> if_mod#(isZero y, le(y, x), x, y, minus(x, y)))
     (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y))}
    EDG:
     {(minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
      (mod#(x, y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
      (mod#(x, y) -> le#(y, x), le#(s x, s y) -> le#(x, y))
      (mod#(x, y) -> if_mod#(isZero y, le(y, x), x, y, minus(x, y)), if_mod#(false(), true(), x, y, z) -> mod#(z, y))
      (if_mod#(false(), true(), x, y, z) -> mod#(z, y), mod#(x, y) -> le#(y, x))
      (if_mod#(false(), true(), x, y, z) -> mod#(z, y), mod#(x, y) -> minus#(x, y))
      (if_mod#(false(), true(), x, y, z) -> mod#(z, y), mod#(x, y) -> isZero# y)
      (if_mod#(false(), true(), x, y, z) -> mod#(z, y), mod#(x, y) -> if_mod#(isZero y, le(y, x), x, y, minus(x, y)))
      (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y))}
     EDG:
      {(minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
       (mod#(x, y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
       (mod#(x, y) -> le#(y, x), le#(s x, s y) -> le#(x, y))
       (mod#(x, y) -> if_mod#(isZero y, le(y, x), x, y, minus(x, y)), if_mod#(false(), true(), x, y, z) -> mod#(z, y))
       (if_mod#(false(), true(), x, y, z) -> mod#(z, y), mod#(x, y) -> le#(y, x))
       (if_mod#(false(), true(), x, y, z) -> mod#(z, y), mod#(x, y) -> minus#(x, y))
       (if_mod#(false(), true(), x, y, z) -> mod#(z, y), mod#(x, y) -> isZero# y)
       (if_mod#(false(), true(), x, y, z) -> mod#(z, y), mod#(x, y) -> if_mod#(isZero y, le(y, x), x, y, minus(x, y)))
       (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y))}
      EDG:
       {(minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
        (mod#(x, y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
        (mod#(x, y) -> le#(y, x), le#(s x, s y) -> le#(x, y))
        (mod#(x, y) -> if_mod#(isZero y, le(y, x), x, y, minus(x, y)), if_mod#(false(), true(), x, y, z) -> mod#(z, y))
        (if_mod#(false(), true(), x, y, z) -> mod#(z, y), mod#(x, y) -> le#(y, x))
        (if_mod#(false(), true(), x, y, z) -> mod#(z, y), mod#(x, y) -> minus#(x, y))
        (if_mod#(false(), true(), x, y, z) -> mod#(z, y), mod#(x, y) -> isZero# y)
        (if_mod#(false(), true(), x, y, z) -> mod#(z, y), mod#(x, y) -> if_mod#(isZero y, le(y, x), x, y, minus(x, y)))
        (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y))}
       STATUS:
        arrows: 0.816327
        SCCS (3):
         Scc:
          {if_mod#(false(), true(), x, y, z) -> mod#(z, y),
                                  mod#(x, y) -> if_mod#(isZero y, le(y, x), x, y, minus(x, y))}
         Scc:
          {minus#(s x, s y) -> minus#(x, y)}
         Scc:
          {le#(s x, s y) -> le#(x, y)}
         
         SCC (2):
          Strict:
           {if_mod#(false(), true(), x, y, z) -> mod#(z, y),
                                   mod#(x, y) -> if_mod#(isZero y, le(y, x), x, y, minus(x, y))}
          Weak:
          {                       le(0(), y) -> true(),
                                le(s x, 0()) -> false(),
                                le(s x, s y) -> le(x, y),
                                 minus(x, x) -> 0(),
                               minus(x, 0()) -> x,
                               minus(0(), x) -> 0(),
                             minus(s x, s y) -> minus(x, y),
                                  isZero 0() -> true(),
                                  isZero s x -> false(),
                  if_mod(true(), b, x, y, z) -> divByZeroError(),
            if_mod(false(), true(), x, y, z) -> mod(z, y),
           if_mod(false(), false(), x, y, z) -> x,
                                   mod(x, y) -> if_mod(isZero y, le(y, x), x, y, minus(x, 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, x) -> 0(),
                               minus(x, 0()) -> x,
                               minus(0(), x) -> 0(),
                             minus(s x, s y) -> minus(x, y),
                                  isZero 0() -> true(),
                                  isZero s x -> false(),
                  if_mod(true(), b, x, y, z) -> divByZeroError(),
            if_mod(false(), true(), x, y, z) -> mod(z, y),
           if_mod(false(), false(), x, y, z) -> x,
                                   mod(x, y) -> if_mod(isZero y, le(y, x), x, y, minus(x, 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, x) -> 0(),
                               minus(x, 0()) -> x,
                               minus(0(), x) -> 0(),
                             minus(s x, s y) -> minus(x, y),
                                  isZero 0() -> true(),
                                  isZero s x -> false(),
                  if_mod(true(), b, x, y, z) -> divByZeroError(),
            if_mod(false(), true(), x, y, z) -> mod(z, y),
           if_mod(false(), false(), x, y, z) -> x,
                                   mod(x, y) -> if_mod(isZero y, le(y, x), x, y, minus(x, y))}
          Open