MAYBE
Time: 0.008357
TRS:
 {                   le(0(), y) -> true(),
                   le(s x, 0()) -> false(),
                   le(s x, s y) -> le(x, y),
                       zero 0() -> true(),
                       zero s x -> false(),
                         id 0() -> 0(),
                         id s x -> s id x,
                  minus(x, 0()) -> x,
                minus(s x, s y) -> minus(x, y),
   if_mod(true(), b1, b2, x, y) -> 0(),
  if_mod(false(), b1, b2, x, y) -> if2(b1, b2, x, y),
                      mod(x, y) -> if_mod(zero x, zero y, le(y, x), id x, id y),
          if2(true(), b2, x, y) -> 0(),
         if2(false(), b2, x, y) -> if3(b2, x, y),
              if3(true(), x, y) -> mod(minus(x, y), s y),
             if3(false(), x, y) -> x}
 DP:
  DP:
   {                 le#(s x, s y) -> le#(x, y),
                           id# s x -> id# x,
                  minus#(s x, s y) -> minus#(x, y),
    if_mod#(false(), b1, b2, x, y) -> if2#(b1, b2, x, y),
                        mod#(x, y) -> le#(y, x),
                        mod#(x, y) -> zero# y,
                        mod#(x, y) -> zero# x,
                        mod#(x, y) -> id# y,
                        mod#(x, y) -> id# x,
                        mod#(x, y) -> if_mod#(zero x, zero y, le(y, x), id x, id y),
           if2#(false(), b2, x, y) -> if3#(b2, x, y),
                if3#(true(), x, y) -> minus#(x, y),
                if3#(true(), x, y) -> mod#(minus(x, y), s y)}
  TRS:
  {                   le(0(), y) -> true(),
                    le(s x, 0()) -> false(),
                    le(s x, s y) -> le(x, y),
                        zero 0() -> true(),
                        zero s x -> false(),
                          id 0() -> 0(),
                          id s x -> s id x,
                   minus(x, 0()) -> x,
                 minus(s x, s y) -> minus(x, y),
    if_mod(true(), b1, b2, x, y) -> 0(),
   if_mod(false(), b1, b2, x, y) -> if2(b1, b2, x, y),
                       mod(x, y) -> if_mod(zero x, zero y, le(y, x), id x, id y),
           if2(true(), b2, x, y) -> 0(),
          if2(false(), b2, x, y) -> if3(b2, x, y),
               if3(true(), x, y) -> mod(minus(x, y), s y),
              if3(false(), x, y) -> x}
  EDG:
   {(if2#(false(), b2, x, y) -> if3#(b2, x, y), if3#(true(), x, y) -> mod#(minus(x, y), s y))
    (if2#(false(), b2, x, y) -> if3#(b2, x, y), if3#(true(), x, y) -> minus#(x, y))
    (mod#(x, y) -> id# y, id# s x -> id# x)
    (if_mod#(false(), b1, b2, x, y) -> if2#(b1, b2, x, y), if2#(false(), b2, x, y) -> if3#(b2, x, y))
    (mod#(x, y) -> if_mod#(zero x, zero y, le(y, x), id x, id y), if_mod#(false(), b1, b2, x, y) -> if2#(b1, b2, x, y))
    (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
    (if3#(true(), x, y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
    (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y))
    (if3#(true(), x, y) -> mod#(minus(x, y), s y), mod#(x, y) -> le#(y, x))
    (if3#(true(), x, y) -> mod#(minus(x, y), s y), mod#(x, y) -> zero# y)
    (if3#(true(), x, y) -> mod#(minus(x, y), s y), mod#(x, y) -> zero# x)
    (if3#(true(), x, y) -> mod#(minus(x, y), s y), mod#(x, y) -> id# y)
    (if3#(true(), x, y) -> mod#(minus(x, y), s y), mod#(x, y) -> id# x)
    (if3#(true(), x, y) -> mod#(minus(x, y), s y), mod#(x, y) -> if_mod#(zero x, zero y, le(y, x), id x, id y))
    (mod#(x, y) -> id# x, id# s x -> id# x)
    (id# s x -> id# x, id# s x -> id# x)
    (mod#(x, y) -> le#(y, x), le#(s x, s y) -> le#(x, y))}
   STATUS:
    arrows: 0.899408
    SCCS (4):
     Scc:
      {if_mod#(false(), b1, b2, x, y) -> if2#(b1, b2, x, y),
                           mod#(x, y) -> if_mod#(zero x, zero y, le(y, x), id x, id y),
              if2#(false(), b2, x, y) -> if3#(b2, x, y),
                   if3#(true(), x, y) -> mod#(minus(x, y), s y)}
     Scc:
      {id# s x -> id# x}
     Scc:
      {minus#(s x, s y) -> minus#(x, y)}
     Scc:
      {le#(s x, s y) -> le#(x, y)}
     
     SCC (4):
      Strict:
       {if_mod#(false(), b1, b2, x, y) -> if2#(b1, b2, x, y),
                            mod#(x, y) -> if_mod#(zero x, zero y, le(y, x), id x, id y),
               if2#(false(), b2, x, y) -> if3#(b2, x, y),
                    if3#(true(), x, y) -> mod#(minus(x, y), s y)}
      Weak:
      {                   le(0(), y) -> true(),
                        le(s x, 0()) -> false(),
                        le(s x, s y) -> le(x, y),
                            zero 0() -> true(),
                            zero s x -> false(),
                              id 0() -> 0(),
                              id s x -> s id x,
                       minus(x, 0()) -> x,
                     minus(s x, s y) -> minus(x, y),
        if_mod(true(), b1, b2, x, y) -> 0(),
       if_mod(false(), b1, b2, x, y) -> if2(b1, b2, x, y),
                           mod(x, y) -> if_mod(zero x, zero y, le(y, x), id x, id y),
               if2(true(), b2, x, y) -> 0(),
              if2(false(), b2, x, y) -> if3(b2, x, y),
                   if3(true(), x, y) -> mod(minus(x, y), s y),
                  if3(false(), x, y) -> x}
      Open
     
     
     SCC (1):
      Strict:
       {id# s x -> id# x}
      Weak:
      {                   le(0(), y) -> true(),
                        le(s x, 0()) -> false(),
                        le(s x, s y) -> le(x, y),
                            zero 0() -> true(),
                            zero s x -> false(),
                              id 0() -> 0(),
                              id s x -> s id x,
                       minus(x, 0()) -> x,
                     minus(s x, s y) -> minus(x, y),
        if_mod(true(), b1, b2, x, y) -> 0(),
       if_mod(false(), b1, b2, x, y) -> if2(b1, b2, x, y),
                           mod(x, y) -> if_mod(zero x, zero y, le(y, x), id x, id y),
               if2(true(), b2, x, y) -> 0(),
              if2(false(), b2, x, y) -> if3(b2, x, y),
                   if3(true(), x, y) -> mod(minus(x, y), s y),
                  if3(false(), x, y) -> x}
      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),
                            zero 0() -> true(),
                            zero s x -> false(),
                              id 0() -> 0(),
                              id s x -> s id x,
                       minus(x, 0()) -> x,
                     minus(s x, s y) -> minus(x, y),
        if_mod(true(), b1, b2, x, y) -> 0(),
       if_mod(false(), b1, b2, x, y) -> if2(b1, b2, x, y),
                           mod(x, y) -> if_mod(zero x, zero y, le(y, x), id x, id y),
               if2(true(), b2, x, y) -> 0(),
              if2(false(), b2, x, y) -> if3(b2, x, y),
                   if3(true(), x, y) -> mod(minus(x, y), s y),
                  if3(false(), x, y) -> x}
      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),
                            zero 0() -> true(),
                            zero s x -> false(),
                              id 0() -> 0(),
                              id s x -> s id x,
                       minus(x, 0()) -> x,
                     minus(s x, s y) -> minus(x, y),
        if_mod(true(), b1, b2, x, y) -> 0(),
       if_mod(false(), b1, b2, x, y) -> if2(b1, b2, x, y),
                           mod(x, y) -> if_mod(zero x, zero y, le(y, x), id x, id y),
               if2(true(), b2, x, y) -> 0(),
              if2(false(), b2, x, y) -> if3(b2, x, y),
                   if3(true(), x, y) -> mod(minus(x, y), s y),
                  if3(false(), x, y) -> x}
      Open