MAYBE
Time: 0.003263
TRS:
 {                 le(0(), y) -> true(),
                 le(s x, 0()) -> false(),
                 le(s x, s y) -> le(x, y),
                 quot(x, 0()) -> quotZeroErro(),
                 quot(x, s y) -> quotIter(x, s y, 0(), 0(), 0()),
    quotIter(x, s y, z, u, v) -> if(le(x, z), x, s y, z, u, v),
    if(true(), x, y, z, u, v) -> v,
   if(false(), x, y, z, u, v) -> if2(le(y, s u), x, y, s z, s u, v),
   if2(true(), x, y, z, u, v) -> quotIter(x, y, z, 0(), s v),
  if2(false(), x, y, z, u, v) -> quotIter(x, y, z, u, v)}
 DP:
  DP:
   {               le#(s x, s y) -> le#(x, y),
                   quot#(x, s y) -> quotIter#(x, s y, 0(), 0(), 0()),
      quotIter#(x, s y, z, u, v) -> le#(x, z),
      quotIter#(x, s y, z, u, v) -> if#(le(x, z), x, s y, z, u, v),
     if#(false(), x, y, z, u, v) -> le#(y, s u),
     if#(false(), x, y, z, u, v) -> if2#(le(y, s u), x, y, s z, s u, v),
     if2#(true(), x, y, z, u, v) -> quotIter#(x, y, z, 0(), s v),
    if2#(false(), x, y, z, u, v) -> quotIter#(x, y, z, u, v)}
  TRS:
  {                 le(0(), y) -> true(),
                  le(s x, 0()) -> false(),
                  le(s x, s y) -> le(x, y),
                  quot(x, 0()) -> quotZeroErro(),
                  quot(x, s y) -> quotIter(x, s y, 0(), 0(), 0()),
     quotIter(x, s y, z, u, v) -> if(le(x, z), x, s y, z, u, v),
     if(true(), x, y, z, u, v) -> v,
    if(false(), x, y, z, u, v) -> if2(le(y, s u), x, y, s z, s u, v),
    if2(true(), x, y, z, u, v) -> quotIter(x, y, z, 0(), s v),
   if2(false(), x, y, z, u, v) -> quotIter(x, y, z, u, v)}
  EDG:
   {(if#(false(), x, y, z, u, v) -> if2#(le(y, s u), x, y, s z, s u, v), if2#(false(), x, y, z, u, v) -> quotIter#(x, y, z, u, v))
    (if#(false(), x, y, z, u, v) -> if2#(le(y, s u), x, y, s z, s u, v), if2#(true(), x, y, z, u, v) -> quotIter#(x, y, z, 0(), s v))
    (quot#(x, s y) -> quotIter#(x, s y, 0(), 0(), 0()), quotIter#(x, s y, z, u, v) -> if#(le(x, z), x, s y, z, u, v))
    (quot#(x, s y) -> quotIter#(x, s y, 0(), 0(), 0()), quotIter#(x, s y, z, u, v) -> le#(x, z))
    (quotIter#(x, s y, z, u, v) -> le#(x, z), le#(s x, s y) -> le#(x, y))
    (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y))
    (if#(false(), x, y, z, u, v) -> le#(y, s u), le#(s x, s y) -> le#(x, y))
    (if2#(true(), x, y, z, u, v) -> quotIter#(x, y, z, 0(), s v), quotIter#(x, s y, z, u, v) -> le#(x, z))
    (if2#(true(), x, y, z, u, v) -> quotIter#(x, y, z, 0(), s v), quotIter#(x, s y, z, u, v) -> if#(le(x, z), x, s y, z, u, v))
    (if2#(false(), x, y, z, u, v) -> quotIter#(x, y, z, u, v), quotIter#(x, s y, z, u, v) -> le#(x, z))
    (if2#(false(), x, y, z, u, v) -> quotIter#(x, y, z, u, v), quotIter#(x, s y, z, u, v) -> if#(le(x, z), x, s y, z, u, v))
    (quotIter#(x, s y, z, u, v) -> if#(le(x, z), x, s y, z, u, v), if#(false(), x, y, z, u, v) -> le#(y, s u))
    (quotIter#(x, s y, z, u, v) -> if#(le(x, z), x, s y, z, u, v), if#(false(), x, y, z, u, v) -> if2#(le(y, s u), x, y, s z, s u, v))}
   STATUS:
    arrows: 0.796875
    SCCS (2):
     Scc:
      {  quotIter#(x, s y, z, u, v) -> if#(le(x, z), x, s y, z, u, v),
        if#(false(), x, y, z, u, v) -> if2#(le(y, s u), x, y, s z, s u, v),
        if2#(true(), x, y, z, u, v) -> quotIter#(x, y, z, 0(), s v),
       if2#(false(), x, y, z, u, v) -> quotIter#(x, y, z, u, v)}
     Scc:
      {le#(s x, s y) -> le#(x, y)}
     
     
     SCC (4):
      Strict:
       {  quotIter#(x, s y, z, u, v) -> if#(le(x, z), x, s y, z, u, v),
         if#(false(), x, y, z, u, v) -> if2#(le(y, s u), x, y, s z, s u, v),
         if2#(true(), x, y, z, u, v) -> quotIter#(x, y, z, 0(), s v),
        if2#(false(), x, y, z, u, v) -> quotIter#(x, y, z, u, v)}
      Weak:
      {                 le(0(), y) -> true(),
                      le(s x, 0()) -> false(),
                      le(s x, s y) -> le(x, y),
                      quot(x, 0()) -> quotZeroErro(),
                      quot(x, s y) -> quotIter(x, s y, 0(), 0(), 0()),
         quotIter(x, s y, z, u, v) -> if(le(x, z), x, s y, z, u, v),
         if(true(), x, y, z, u, v) -> v,
        if(false(), x, y, z, u, v) -> if2(le(y, s u), x, y, s z, s u, v),
        if2(true(), x, y, z, u, v) -> quotIter(x, y, z, 0(), s v),
       if2(false(), x, y, z, u, v) -> quotIter(x, y, z, u, v)}
      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),
                      quot(x, 0()) -> quotZeroErro(),
                      quot(x, s y) -> quotIter(x, s y, 0(), 0(), 0()),
         quotIter(x, s y, z, u, v) -> if(le(x, z), x, s y, z, u, v),
         if(true(), x, y, z, u, v) -> v,
        if(false(), x, y, z, u, v) -> if2(le(y, s u), x, y, s z, s u, v),
        if2(true(), x, y, z, u, v) -> quotIter(x, y, z, 0(), s v),
       if2(false(), x, y, z, u, v) -> quotIter(x, y, z, u, v)}
      Open