MAYBE
Time: 0.001560
TRS:
 {          div(x, y, z) -> if(lt(x, y), x, y, inc z),
          division(x, y) -> div(x, y, 0()),
     if(true(), x, y, z) -> z,
  if(false(), x, s y, z) -> div(minus(x, s y), s y, z),
              lt(x, 0()) -> false(),
            lt(0(), s y) -> true(),
            lt(s x, s y) -> lt(x, y),
                 inc 0() -> s 0(),
                 inc s x -> s inc x,
           minus(x, 0()) -> x,
         minus(s x, s y) -> minus(x, y)}
 DP:
  DP:
   {          div#(x, y, z) -> if#(lt(x, y), x, y, inc z),
              div#(x, y, z) -> lt#(x, y),
              div#(x, y, z) -> inc# z,
            division#(x, y) -> div#(x, y, 0()),
    if#(false(), x, s y, z) -> div#(minus(x, s y), s y, z),
    if#(false(), x, s y, z) -> minus#(x, s y),
              lt#(s x, s y) -> lt#(x, y),
                   inc# s x -> inc# x,
           minus#(s x, s y) -> minus#(x, y)}
  TRS:
  {          div(x, y, z) -> if(lt(x, y), x, y, inc z),
           division(x, y) -> div(x, y, 0()),
      if(true(), x, y, z) -> z,
   if(false(), x, s y, z) -> div(minus(x, s y), s y, z),
               lt(x, 0()) -> false(),
             lt(0(), s y) -> true(),
             lt(s x, s y) -> lt(x, y),
                  inc 0() -> s 0(),
                  inc s x -> s inc x,
            minus(x, 0()) -> x,
          minus(s x, s y) -> minus(x, y)}
  UR:
   {     lt(x, 0()) -> false(),
       lt(0(), s y) -> true(),
       lt(s x, s y) -> lt(x, y),
            inc 0() -> s 0(),
            inc s x -> s inc x,
      minus(x, 0()) -> x,
    minus(s x, s y) -> minus(x, y),
            a(w, v) -> w,
            a(w, v) -> v}
   EDG:
    {(inc# s x -> inc# x, inc# s x -> inc# x)
     (div#(x, y, z) -> inc# z, inc# s x -> inc# x)
     (div#(x, y, z) -> lt#(x, y), lt#(s x, s y) -> lt#(x, y))
     (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
     (if#(false(), x, s y, z) -> minus#(x, s y), minus#(s x, s y) -> minus#(x, y))
     (lt#(s x, s y) -> lt#(x, y), lt#(s x, s y) -> lt#(x, y))
     (if#(false(), x, s y, z) -> div#(minus(x, s y), s y, z), div#(x, y, z) -> if#(lt(x, y), x, y, inc z))
     (if#(false(), x, s y, z) -> div#(minus(x, s y), s y, z), div#(x, y, z) -> lt#(x, y))
     (if#(false(), x, s y, z) -> div#(minus(x, s y), s y, z), div#(x, y, z) -> inc# z)
     (div#(x, y, z) -> if#(lt(x, y), x, y, inc z), if#(false(), x, s y, z) -> div#(minus(x, s y), s y, z))
     (div#(x, y, z) -> if#(lt(x, y), x, y, inc z), if#(false(), x, s y, z) -> minus#(x, s y))
     (division#(x, y) -> div#(x, y, 0()), div#(x, y, z) -> if#(lt(x, y), x, y, inc z))
     (division#(x, y) -> div#(x, y, 0()), div#(x, y, z) -> lt#(x, y))
     (division#(x, y) -> div#(x, y, 0()), div#(x, y, z) -> inc# z)}
    STATUS:
     arrows: 0.827160
     SCCS (4):
      Scc:
       {          div#(x, y, z) -> if#(lt(x, y), x, y, inc z),
        if#(false(), x, s y, z) -> div#(minus(x, s y), s y, z)}
      Scc:
       {minus#(s x, s y) -> minus#(x, y)}
      Scc:
       {inc# s x -> inc# x}
      Scc:
       {lt#(s x, s y) -> lt#(x, y)}
      
      
      SCC (2):
       Strict:
        {          div#(x, y, z) -> if#(lt(x, y), x, y, inc z),
         if#(false(), x, s y, z) -> div#(minus(x, s y), s y, z)}
       Weak:
       {          div(x, y, z) -> if(lt(x, y), x, y, inc z),
                division(x, y) -> div(x, y, 0()),
           if(true(), x, y, z) -> z,
        if(false(), x, s y, z) -> div(minus(x, s y), s y, z),
                    lt(x, 0()) -> false(),
                  lt(0(), s y) -> true(),
                  lt(s x, s y) -> lt(x, y),
                       inc 0() -> s 0(),
                       inc s x -> s inc x,
                 minus(x, 0()) -> x,
               minus(s x, s y) -> minus(x, y)}
       Open
      
      SCC (1):
       Strict:
        {minus#(s x, s y) -> minus#(x, y)}
       Weak:
       {          div(x, y, z) -> if(lt(x, y), x, y, inc z),
                division(x, y) -> div(x, y, 0()),
           if(true(), x, y, z) -> z,
        if(false(), x, s y, z) -> div(minus(x, s y), s y, z),
                    lt(x, 0()) -> false(),
                  lt(0(), s y) -> true(),
                  lt(s x, s y) -> lt(x, y),
                       inc 0() -> s 0(),
                       inc s x -> s inc x,
                 minus(x, 0()) -> x,
               minus(s x, s y) -> minus(x, y)}
       Open
      
      SCC (1):
       Strict:
        {inc# s x -> inc# x}
       Weak:
       {          div(x, y, z) -> if(lt(x, y), x, y, inc z),
                division(x, y) -> div(x, y, 0()),
           if(true(), x, y, z) -> z,
        if(false(), x, s y, z) -> div(minus(x, s y), s y, z),
                    lt(x, 0()) -> false(),
                  lt(0(), s y) -> true(),
                  lt(s x, s y) -> lt(x, y),
                       inc 0() -> s 0(),
                       inc s x -> s inc x,
                 minus(x, 0()) -> x,
               minus(s x, s y) -> minus(x, y)}
       Open
      
      SCC (1):
       Strict:
        {lt#(s x, s y) -> lt#(x, y)}
       Weak:
       {          div(x, y, z) -> if(lt(x, y), x, y, inc z),
                division(x, y) -> div(x, y, 0()),
           if(true(), x, y, z) -> z,
        if(false(), x, s y, z) -> div(minus(x, s y), s y, z),
                    lt(x, 0()) -> false(),
                  lt(0(), s y) -> true(),
                  lt(s x, s y) -> lt(x, y),
                       inc 0() -> s 0(),
                       inc s x -> s inc x,
                 minus(x, 0()) -> x,
               minus(s x, s y) -> minus(x, y)}
       Open