MAYBE
Time: 0.007735
TRS:
 {              le(0(), Y) -> true(),
              le(s X, 0()) -> false(),
              le(s X, s Y) -> le(X, Y),
             minus(0(), Y) -> 0(),
             minus(s X, Y) -> ifMinus(le(s X, Y), s X, Y),
   ifMinus(true(), s X, Y) -> 0(),
  ifMinus(false(), s X, Y) -> s minus(X, Y),
            quot(0(), s Y) -> 0(),
            quot(s X, s Y) -> s quot(minus(X, Y), s Y)}
 DP:
  DP:
   {            le#(s X, s Y) -> le#(X, Y),
               minus#(s X, Y) -> le#(s X, Y),
               minus#(s X, Y) -> ifMinus#(le(s X, Y), s X, Y),
    ifMinus#(false(), s X, Y) -> minus#(X, Y),
              quot#(s X, s Y) -> minus#(X, Y),
              quot#(s X, s Y) -> quot#(minus(X, Y), s Y)}
  TRS:
  {              le(0(), Y) -> true(),
               le(s X, 0()) -> false(),
               le(s X, s Y) -> le(X, Y),
              minus(0(), Y) -> 0(),
              minus(s X, Y) -> ifMinus(le(s X, Y), s X, Y),
    ifMinus(true(), s X, Y) -> 0(),
   ifMinus(false(), s X, Y) -> s minus(X, Y),
             quot(0(), s Y) -> 0(),
             quot(s X, s Y) -> s quot(minus(X, Y), s Y)}
  EDG:
   {(ifMinus#(false(), s X, Y) -> minus#(X, Y), minus#(s X, Y) -> ifMinus#(le(s X, Y), s X, Y))
    (ifMinus#(false(), s X, Y) -> minus#(X, Y), minus#(s X, Y) -> le#(s X, Y))
    (quot#(s X, s Y) -> quot#(minus(X, Y), s Y), quot#(s X, s Y) -> quot#(minus(X, Y), s Y))
    (quot#(s X, s Y) -> quot#(minus(X, Y), s Y), quot#(s X, s Y) -> minus#(X, Y))
    (minus#(s X, Y) -> ifMinus#(le(s X, Y), s X, Y), ifMinus#(false(), s X, Y) -> minus#(X, Y))
    (minus#(s X, Y) -> le#(s X, Y), le#(s X, s Y) -> le#(X, Y))
    (quot#(s X, s Y) -> minus#(X, Y), minus#(s X, Y) -> le#(s X, Y))
    (quot#(s X, s Y) -> minus#(X, Y), minus#(s X, Y) -> ifMinus#(le(s X, Y), s X, Y))
    (le#(s X, s Y) -> le#(X, Y), le#(s X, s Y) -> le#(X, Y))}
   STATUS:
    arrows: 0.750000
    SCCS (3):
     Scc:
      {quot#(s X, s Y) -> quot#(minus(X, Y), s Y)}
     Scc:
      {           minus#(s X, Y) -> ifMinus#(le(s X, Y), s X, Y),
       ifMinus#(false(), s X, Y) -> minus#(X, Y)}
     Scc:
      {le#(s X, s Y) -> le#(X, Y)}
     
     SCC (1):
      Strict:
       {quot#(s X, s Y) -> quot#(minus(X, Y), s Y)}
      Weak:
      {              le(0(), Y) -> true(),
                   le(s X, 0()) -> false(),
                   le(s X, s Y) -> le(X, Y),
                  minus(0(), Y) -> 0(),
                  minus(s X, Y) -> ifMinus(le(s X, Y), s X, Y),
        ifMinus(true(), s X, Y) -> 0(),
       ifMinus(false(), s X, Y) -> s minus(X, Y),
                 quot(0(), s Y) -> 0(),
                 quot(s X, s Y) -> s quot(minus(X, Y), s Y)}
      Open
     
     SCC (2):
      Strict:
       {           minus#(s X, Y) -> ifMinus#(le(s X, Y), s X, Y),
        ifMinus#(false(), s X, Y) -> minus#(X, Y)}
      Weak:
      {              le(0(), Y) -> true(),
                   le(s X, 0()) -> false(),
                   le(s X, s Y) -> le(X, Y),
                  minus(0(), Y) -> 0(),
                  minus(s X, Y) -> ifMinus(le(s X, Y), s X, Y),
        ifMinus(true(), s X, Y) -> 0(),
       ifMinus(false(), s X, Y) -> s minus(X, Y),
                 quot(0(), s Y) -> 0(),
                 quot(s X, s Y) -> s quot(minus(X, Y), s 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(0(), Y) -> 0(),
                  minus(s X, Y) -> ifMinus(le(s X, Y), s X, Y),
        ifMinus(true(), s X, Y) -> 0(),
       ifMinus(false(), s X, Y) -> s minus(X, Y),
                 quot(0(), s Y) -> 0(),
                 quot(s X, s Y) -> s quot(minus(X, Y), s Y)}
      Open