MAYBE
Time: 1.439351
TRS:
 {              le(0(), y) -> true(),
              le(s x, 0()) -> false(),
              le(s x, s y) -> le(x, y),
               mod(x, 0()) -> modZeroErro(),
               mod(x, s y) -> modIter(x, s y, 0(), 0()),
     modIter(x, s y, z, u) -> if(le(x, z), x, s y, z, u),
    if(true(), x, y, z, u) -> u,
   if(false(), x, y, z, u) -> if2(le(y, s u), x, y, s z, s u),
   if2(true(), x, y, z, u) -> modIter(x, y, z, 0()),
  if2(false(), x, y, z, u) -> modIter(x, y, z, u)}
 DP:
  DP:
   {            le#(s x, s y) -> le#(x, y),
                 mod#(x, s y) -> modIter#(x, s y, 0(), 0()),
       modIter#(x, s y, z, u) -> le#(x, z),
       modIter#(x, s y, z, u) -> if#(le(x, z), x, s y, z, u),
     if#(false(), x, y, z, u) -> le#(y, s u),
     if#(false(), x, y, z, u) -> if2#(le(y, s u), x, y, s z, s u),
     if2#(true(), x, y, z, u) -> modIter#(x, y, z, 0()),
    if2#(false(), x, y, z, u) -> modIter#(x, y, z, u)}
  TRS:
  {              le(0(), y) -> true(),
               le(s x, 0()) -> false(),
               le(s x, s y) -> le(x, y),
                mod(x, 0()) -> modZeroErro(),
                mod(x, s y) -> modIter(x, s y, 0(), 0()),
      modIter(x, s y, z, u) -> if(le(x, z), x, s y, z, u),
     if(true(), x, y, z, u) -> u,
    if(false(), x, y, z, u) -> if2(le(y, s u), x, y, s z, s u),
    if2(true(), x, y, z, u) -> modIter(x, y, z, 0()),
   if2(false(), x, y, z, u) -> modIter(x, y, z, u)}
  UR:
   {  le(0(), y) -> true(),
    le(s x, 0()) -> false(),
    le(s x, s y) -> le(x, y),
         a(w, v) -> w,
         a(w, v) -> v}
   EDG:
    {(if2#(false(), x, y, z, u) -> modIter#(x, y, z, u), modIter#(x, s y, z, u) -> if#(le(x, z), x, s y, z, u))
     (if2#(false(), x, y, z, u) -> modIter#(x, y, z, u), modIter#(x, s y, z, u) -> le#(x, z))
     (mod#(x, s y) -> modIter#(x, s y, 0(), 0()), modIter#(x, s y, z, u) -> if#(le(x, z), x, s y, z, u))
     (mod#(x, s y) -> modIter#(x, s y, 0(), 0()), modIter#(x, s y, z, u) -> le#(x, z))
     (if#(false(), x, y, z, u) -> le#(y, s u), le#(s x, s y) -> le#(x, y))
     (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y))
     (if2#(true(), x, y, z, u) -> modIter#(x, y, z, 0()), modIter#(x, s y, z, u) -> le#(x, z))
     (if2#(true(), x, y, z, u) -> modIter#(x, y, z, 0()), modIter#(x, s y, z, u) -> if#(le(x, z), x, s y, z, u))
     (modIter#(x, s y, z, u) -> le#(x, z), le#(s x, s y) -> le#(x, y))
     (if#(false(), x, y, z, u) -> if2#(le(y, s u), x, y, s z, s u), if2#(true(), x, y, z, u) -> modIter#(x, y, z, 0()))
     (if#(false(), x, y, z, u) -> if2#(le(y, s u), x, y, s z, s u), if2#(false(), x, y, z, u) -> modIter#(x, y, z, u))
     (modIter#(x, s y, z, u) -> if#(le(x, z), x, s y, z, u), if#(false(), x, y, z, u) -> le#(y, s u))
     (modIter#(x, s y, z, u) -> if#(le(x, z), x, s y, z, u), if#(false(), x, y, z, u) -> if2#(le(y, s u), x, y, s z, s u))}
    STATUS:
     arrows: 0.796875
     SCCS (2):
      Scc:
       {   modIter#(x, s y, z, u) -> if#(le(x, z), x, s y, z, u),
         if#(false(), x, y, z, u) -> if2#(le(y, s u), x, y, s z, s u),
         if2#(true(), x, y, z, u) -> modIter#(x, y, z, 0()),
        if2#(false(), x, y, z, u) -> modIter#(x, y, z, u)}
      Scc:
       {le#(s x, s y) -> le#(x, y)}
      
      
      SCC (4):
       Strict:
        {   modIter#(x, s y, z, u) -> if#(le(x, z), x, s y, z, u),
          if#(false(), x, y, z, u) -> if2#(le(y, s u), x, y, s z, s u),
          if2#(true(), x, y, z, u) -> modIter#(x, y, z, 0()),
         if2#(false(), x, y, z, u) -> modIter#(x, y, z, u)}
       Weak:
       {              le(0(), y) -> true(),
                    le(s x, 0()) -> false(),
                    le(s x, s y) -> le(x, y),
                     mod(x, 0()) -> modZeroErro(),
                     mod(x, s y) -> modIter(x, s y, 0(), 0()),
           modIter(x, s y, z, u) -> if(le(x, z), x, s y, z, u),
          if(true(), x, y, z, u) -> u,
         if(false(), x, y, z, u) -> if2(le(y, s u), x, y, s z, s u),
         if2(true(), x, y, z, u) -> modIter(x, y, z, 0()),
        if2(false(), x, y, z, u) -> modIter(x, y, z, u)}
       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),
                     mod(x, 0()) -> modZeroErro(),
                     mod(x, s y) -> modIter(x, s y, 0(), 0()),
           modIter(x, s y, z, u) -> if(le(x, z), x, s y, z, u),
          if(true(), x, y, z, u) -> u,
         if(false(), x, y, z, u) -> if2(le(y, s u), x, y, s z, s u),
         if2(true(), x, y, z, u) -> modIter(x, y, z, 0()),
        if2(false(), x, y, z, u) -> modIter(x, y, z, u)}
       Open