MAYBE
Time: 1.002830
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,
   if(true(), true(), x, y) -> id_inc div(minus(x, y), y),
  if(true(), false(), x, y) -> 0(),
       if(false(), b, x, y) -> div_by_zero(),
                  div(x, y) -> if(ge(y, s 0()), ge(x, y), x, y)}
 DP:
  DP:
   {            ge#(s x, s y) -> ge#(x, y),
             minus#(s x, s y) -> minus#(x, y),
    if#(true(), true(), x, y) -> minus#(x, y),
    if#(true(), true(), x, y) -> id_inc# div(minus(x, y), y),
    if#(true(), true(), x, y) -> div#(minus(x, y), y),
                   div#(x, y) -> ge#(x, y),
                   div#(x, y) -> ge#(y, s 0()),
                   div#(x, y) -> if#(ge(y, s 0()), ge(x, y), x, y)}
  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,
    if(true(), true(), x, y) -> id_inc div(minus(x, y), y),
   if(true(), false(), x, y) -> 0(),
        if(false(), b, x, y) -> div_by_zero(),
                   div(x, y) -> if(ge(y, s 0()), ge(x, y), x, y)}
  EDG:
   {(if#(true(), true(), x, y) -> div#(minus(x, y), y), div#(x, y) -> if#(ge(y, s 0()), ge(x, y), x, y))
    (if#(true(), true(), x, y) -> div#(minus(x, y), y), div#(x, y) -> ge#(y, s 0()))
    (if#(true(), true(), x, y) -> div#(minus(x, y), y), div#(x, y) -> ge#(x, y))
    (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
    (div#(x, y) -> ge#(x, y), ge#(s x, s y) -> ge#(x, y))
    (div#(x, y) -> if#(ge(y, s 0()), ge(x, y), x, y), if#(true(), true(), x, y) -> minus#(x, y))
    (div#(x, y) -> if#(ge(y, s 0()), ge(x, y), x, y), if#(true(), true(), x, y) -> id_inc# div(minus(x, y), y))
    (div#(x, y) -> if#(ge(y, s 0()), ge(x, y), x, y), if#(true(), true(), x, y) -> div#(minus(x, y), y))
    (if#(true(), true(), x, y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
    (ge#(s x, s y) -> ge#(x, y), ge#(s x, s y) -> ge#(x, y))
    (div#(x, y) -> ge#(y, s 0()), ge#(s x, s y) -> ge#(x, y))}
   EDG:
    {(if#(true(), true(), x, y) -> div#(minus(x, y), y), div#(x, y) -> if#(ge(y, s 0()), ge(x, y), x, y))
     (if#(true(), true(), x, y) -> div#(minus(x, y), y), div#(x, y) -> ge#(y, s 0()))
     (if#(true(), true(), x, y) -> div#(minus(x, y), y), div#(x, y) -> ge#(x, y))
     (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
     (div#(x, y) -> ge#(x, y), ge#(s x, s y) -> ge#(x, y))
     (div#(x, y) -> if#(ge(y, s 0()), ge(x, y), x, y), if#(true(), true(), x, y) -> minus#(x, y))
     (div#(x, y) -> if#(ge(y, s 0()), ge(x, y), x, y), if#(true(), true(), x, y) -> id_inc# div(minus(x, y), y))
     (div#(x, y) -> if#(ge(y, s 0()), ge(x, y), x, y), if#(true(), true(), x, y) -> div#(minus(x, y), y))
     (if#(true(), true(), x, y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
     (ge#(s x, s y) -> ge#(x, y), ge#(s x, s y) -> ge#(x, y))
     (div#(x, y) -> ge#(y, s 0()), ge#(s x, s y) -> ge#(x, y))}
    STATUS:
     arrows: 0.828125
     SCCS (3):
      Scc:
       {if#(true(), true(), x, y) -> div#(minus(x, y), y),
                       div#(x, y) -> if#(ge(y, s 0()), ge(x, y), x, y)}
      Scc:
       {minus#(s x, s y) -> minus#(x, y)}
      Scc:
       {ge#(s x, s y) -> ge#(x, y)}
      
      SCC (2):
       Strict:
        {if#(true(), true(), x, y) -> div#(minus(x, y), y),
                        div#(x, y) -> if#(ge(y, s 0()), ge(x, y), 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,
         if(true(), true(), x, y) -> id_inc div(minus(x, y), y),
        if(true(), false(), x, y) -> 0(),
             if(false(), b, x, y) -> div_by_zero(),
                        div(x, y) -> if(ge(y, s 0()), ge(x, y), x, y)}
       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,
         if(true(), true(), x, y) -> id_inc div(minus(x, y), y),
        if(true(), false(), x, y) -> 0(),
             if(false(), b, x, y) -> div_by_zero(),
                        div(x, y) -> if(ge(y, s 0()), ge(x, y), x, y)}
       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,
         if(true(), true(), x, y) -> id_inc div(minus(x, y), y),
        if(true(), false(), x, y) -> 0(),
             if(false(), b, x, y) -> div_by_zero(),
                        div(x, y) -> if(ge(y, s 0()), ge(x, y), x, y)}
       Open