MAYBE
Time: 1.113566
TRS:
 {                    minus(x, x) -> 0(),
                    minus(x, 0()) -> x,
                    minus(0(), x) -> 0(),
                  minus(s x, s y) -> minus(x, y),
                       le(0(), y) -> true(),
                     le(s x, 0()) -> false(),
                     le(s x, s y) -> le(x, y),
         if_quot(x, y, true(), z) -> divByZeroError(),
   if_quot(x, y, false(), true()) -> s quot(x, y),
  if_quot(x, y, false(), false()) -> 0(),
                       quot(x, y) -> if_quot(minus(x, y), y, le(y, 0()), le(y, x))}
 DP:
  DP:
   {               minus#(s x, s y) -> minus#(x, y),
                      le#(s x, s y) -> le#(x, y),
    if_quot#(x, y, false(), true()) -> quot#(x, y),
                        quot#(x, y) -> minus#(x, y),
                        quot#(x, y) -> le#(y, x),
                        quot#(x, y) -> le#(y, 0()),
                        quot#(x, y) -> if_quot#(minus(x, y), y, le(y, 0()), le(y, x))}
  TRS:
  {                    minus(x, x) -> 0(),
                     minus(x, 0()) -> x,
                     minus(0(), x) -> 0(),
                   minus(s x, s y) -> minus(x, y),
                        le(0(), y) -> true(),
                      le(s x, 0()) -> false(),
                      le(s x, s y) -> le(x, y),
          if_quot(x, y, true(), z) -> divByZeroError(),
    if_quot(x, y, false(), true()) -> s quot(x, y),
   if_quot(x, y, false(), false()) -> 0(),
                        quot(x, y) -> if_quot(minus(x, y), y, le(y, 0()), le(y, x))}
  UR:
   {    minus(x, x) -> 0(),
      minus(x, 0()) -> x,
      minus(0(), x) -> 0(),
    minus(s x, s y) -> minus(x, y),
         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:
    {(quot#(x, y) -> le#(y, x), le#(s x, s y) -> le#(x, y))
     (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
     (if_quot#(x, y, false(), true()) -> quot#(x, y), quot#(x, y) -> if_quot#(minus(x, y), y, le(y, 0()), le(y, x)))
     (if_quot#(x, y, false(), true()) -> quot#(x, y), quot#(x, y) -> le#(y, 0()))
     (if_quot#(x, y, false(), true()) -> quot#(x, y), quot#(x, y) -> le#(y, x))
     (if_quot#(x, y, false(), true()) -> quot#(x, y), quot#(x, y) -> minus#(x, y))
     (quot#(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))
     (quot#(x, y) -> if_quot#(minus(x, y), y, le(y, 0()), le(y, x)), if_quot#(x, y, false(), true()) -> quot#(x, y))}
    STATUS:
     arrows: 0.816327
     SCCS (3):
      Scc:
       {if_quot#(x, y, false(), true()) -> quot#(x, y),
                            quot#(x, y) -> if_quot#(minus(x, y), y, le(y, 0()), le(y, x))}
      Scc:
       {minus#(s x, s y) -> minus#(x, y)}
      Scc:
       {le#(s x, s y) -> le#(x, y)}
      
      SCC (2):
       Strict:
        {if_quot#(x, y, false(), true()) -> quot#(x, y),
                             quot#(x, y) -> if_quot#(minus(x, y), y, le(y, 0()), le(y, x))}
       Weak:
       {                    minus(x, x) -> 0(),
                          minus(x, 0()) -> x,
                          minus(0(), x) -> 0(),
                        minus(s x, s y) -> minus(x, y),
                             le(0(), y) -> true(),
                           le(s x, 0()) -> false(),
                           le(s x, s y) -> le(x, y),
               if_quot(x, y, true(), z) -> divByZeroError(),
         if_quot(x, y, false(), true()) -> s quot(x, y),
        if_quot(x, y, false(), false()) -> 0(),
                             quot(x, y) -> if_quot(minus(x, y), y, le(y, 0()), le(y, x))}
       Open
      
      SCC (1):
       Strict:
        {minus#(s x, s y) -> minus#(x, y)}
       Weak:
       {                    minus(x, x) -> 0(),
                          minus(x, 0()) -> x,
                          minus(0(), x) -> 0(),
                        minus(s x, s y) -> minus(x, y),
                             le(0(), y) -> true(),
                           le(s x, 0()) -> false(),
                           le(s x, s y) -> le(x, y),
               if_quot(x, y, true(), z) -> divByZeroError(),
         if_quot(x, y, false(), true()) -> s quot(x, y),
        if_quot(x, y, false(), false()) -> 0(),
                             quot(x, y) -> if_quot(minus(x, y), y, le(y, 0()), le(y, x))}
       Open
      
      SCC (1):
       Strict:
        {le#(s x, s y) -> le#(x, y)}
       Weak:
       {                    minus(x, x) -> 0(),
                          minus(x, 0()) -> x,
                          minus(0(), x) -> 0(),
                        minus(s x, s y) -> minus(x, y),
                             le(0(), y) -> true(),
                           le(s x, 0()) -> false(),
                           le(s x, s y) -> le(x, y),
               if_quot(x, y, true(), z) -> divByZeroError(),
         if_quot(x, y, false(), true()) -> s quot(x, y),
        if_quot(x, y, false(), false()) -> 0(),
                             quot(x, y) -> if_quot(minus(x, y), y, le(y, 0()), le(y, x))}
       Open