MAYBE
Time: 0.686468
TRS:
 {                  ge(x, 0()) -> true(),
                  ge(0(), s y) -> false(),
                  ge(s x, s y) -> ge(x, y),
                 minus(x, 0()) -> x,
                 minus(0(), y) -> 0(),
               minus(s x, s y) -> minus(x, y),
                      id_inc x -> x,
                      id_inc x -> s x,
                  div(x, y, z) -> if(ge(y, s 0()), ge(x, y), x, y, z),
                    quot(x, y) -> div(x, y, 0()),
   if(true(), true(), x, y, z) -> div(minus(x, y), y, id_inc z),
  if(true(), false(), x, y, z) -> z,
       if(false(), b, x, y, z) -> div_by_zero()}
 DP:
  DP:
   {               ge#(s x, s y) -> ge#(x, y),
                minus#(s x, s y) -> minus#(x, y),
                   div#(x, y, z) -> ge#(x, y),
                   div#(x, y, z) -> ge#(y, s 0()),
                   div#(x, y, z) -> if#(ge(y, s 0()), ge(x, y), x, y, z),
                     quot#(x, y) -> div#(x, y, 0()),
    if#(true(), true(), x, y, z) -> minus#(x, y),
    if#(true(), true(), x, y, z) -> id_inc# z,
    if#(true(), true(), x, y, z) -> div#(minus(x, y), y, id_inc z)}
  TRS:
  {                  ge(x, 0()) -> true(),
                   ge(0(), s y) -> false(),
                   ge(s x, s y) -> ge(x, y),
                  minus(x, 0()) -> x,
                  minus(0(), y) -> 0(),
                minus(s x, s y) -> minus(x, y),
                       id_inc x -> x,
                       id_inc x -> s x,
                   div(x, y, z) -> if(ge(y, s 0()), ge(x, y), x, y, z),
                     quot(x, y) -> div(x, y, 0()),
    if(true(), true(), x, y, z) -> div(minus(x, y), y, id_inc z),
   if(true(), false(), x, y, z) -> z,
        if(false(), b, x, y, z) -> div_by_zero()}
  UR:
   {     ge(x, 0()) -> true(),
       ge(0(), s y) -> false(),
       ge(s x, s y) -> ge(x, y),
      minus(x, 0()) -> x,
      minus(0(), y) -> 0(),
    minus(s x, s y) -> minus(x, y),
           id_inc x -> x,
           id_inc x -> s x}
   EDG:
    {(minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
     (if#(true(), true(), x, y, z) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
     (div#(x, y, z) -> if#(ge(y, s 0()), ge(x, y), x, y, z), if#(true(), true(), x, y, z) -> div#(minus(x, y), y, id_inc z))
     (div#(x, y, z) -> if#(ge(y, s 0()), ge(x, y), x, y, z), if#(true(), true(), x, y, z) -> id_inc# z)
     (div#(x, y, z) -> if#(ge(y, s 0()), ge(x, y), x, y, z), if#(true(), true(), x, y, z) -> minus#(x, y))
     (if#(true(), true(), x, y, z) -> div#(minus(x, y), y, id_inc z), div#(x, y, z) -> ge#(x, y))
     (if#(true(), true(), x, y, z) -> div#(minus(x, y), y, id_inc z), div#(x, y, z) -> ge#(y, s 0()))
     (if#(true(), true(), x, y, z) -> div#(minus(x, y), y, id_inc z), div#(x, y, z) -> if#(ge(y, s 0()), ge(x, y), x, y, z))
     (div#(x, y, z) -> ge#(y, s 0()), ge#(s x, s y) -> ge#(x, y))
     (div#(x, y, z) -> ge#(x, y), ge#(s x, s y) -> ge#(x, y))
     (ge#(s x, s y) -> ge#(x, y), ge#(s x, s y) -> ge#(x, y))
     (quot#(x, y) -> div#(x, y, 0()), div#(x, y, z) -> ge#(x, y))
     (quot#(x, y) -> div#(x, y, 0()), div#(x, y, z) -> ge#(y, s 0()))
     (quot#(x, y) -> div#(x, y, 0()), div#(x, y, z) -> if#(ge(y, s 0()), ge(x, y), x, y, z))}
    STATUS:
     arrows: 0.827160
     SCCS (3):
      Scc:
       {               div#(x, y, z) -> if#(ge(y, s 0()), ge(x, y), x, y, z),
        if#(true(), true(), x, y, z) -> div#(minus(x, y), y, id_inc z)}
      Scc:
       {minus#(s x, s y) -> minus#(x, y)}
      Scc:
       {ge#(s x, s y) -> ge#(x, y)}
      
      
      SCC (2):
       Strict:
        {               div#(x, y, z) -> if#(ge(y, s 0()), ge(x, y), x, y, z),
         if#(true(), true(), x, y, z) -> div#(minus(x, y), y, id_inc z)}
       Weak:
       {                  ge(x, 0()) -> true(),
                        ge(0(), s y) -> false(),
                        ge(s x, s y) -> ge(x, y),
                       minus(x, 0()) -> x,
                       minus(0(), y) -> 0(),
                     minus(s x, s y) -> minus(x, y),
                            id_inc x -> x,
                            id_inc x -> s x,
                        div(x, y, z) -> if(ge(y, s 0()), ge(x, y), x, y, z),
                          quot(x, y) -> div(x, y, 0()),
         if(true(), true(), x, y, z) -> div(minus(x, y), y, id_inc z),
        if(true(), false(), x, y, z) -> z,
             if(false(), b, x, y, z) -> div_by_zero()}
       Open
      
      
      SCC (1):
       Strict:
        {minus#(s x, s y) -> minus#(x, y)}
       Weak:
       {                  ge(x, 0()) -> true(),
                        ge(0(), s y) -> false(),
                        ge(s x, s y) -> ge(x, y),
                       minus(x, 0()) -> x,
                       minus(0(), y) -> 0(),
                     minus(s x, s y) -> minus(x, y),
                            id_inc x -> x,
                            id_inc x -> s x,
                        div(x, y, z) -> if(ge(y, s 0()), ge(x, y), x, y, z),
                          quot(x, y) -> div(x, y, 0()),
         if(true(), true(), x, y, z) -> div(minus(x, y), y, id_inc z),
        if(true(), false(), x, y, z) -> z,
             if(false(), b, x, y, z) -> div_by_zero()}
       Open
      
      
      SCC (1):
       Strict:
        {ge#(s x, s y) -> ge#(x, y)}
       Weak:
       {                  ge(x, 0()) -> true(),
                        ge(0(), s y) -> false(),
                        ge(s x, s y) -> ge(x, y),
                       minus(x, 0()) -> x,
                       minus(0(), y) -> 0(),
                     minus(s x, s y) -> minus(x, y),
                            id_inc x -> x,
                            id_inc x -> s x,
                        div(x, y, z) -> if(ge(y, s 0()), ge(x, y), x, y, z),
                          quot(x, y) -> div(x, y, 0()),
         if(true(), true(), x, y, z) -> div(minus(x, y), y, id_inc z),
        if(true(), false(), x, y, z) -> z,
             if(false(), b, x, y, z) -> div_by_zero()}
       Open