MAYBE
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:
  Strict:
   {           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)}
  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)}
  EDG:
   {(div#(x, y, z) -> if#(lt(x, y), x, y, inc(z)), if#(false(), x, s(y), z) -> minus#(x, s(y)))
    (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), lt#(s(x), s(y)) -> lt#(x, y))
    (minus#(s(x), s(y)) -> minus#(x, y), minus#(s(x), s(y)) -> minus#(x, y))
    (div#(x, y, z) -> inc#(z), inc#(s(x)) -> inc#(x))
    (if#(false(), x, s(y), z) -> minus#(x, s(y)), minus#(s(x), s(y)) -> minus#(x, y))
    (inc#(s(x)) -> inc#(x), inc#(s(x)) -> inc#(x))
    (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))
    (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))}
   SCCS:
    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:
     {           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:
     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)}
     SPSC:
      Simple Projection:
       pi(minus#) = 0
      Strict:
       {}
      Qed
    SCC:
     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)}
     SPSC:
      Simple Projection:
       pi(inc#) = 0
      Strict:
       {}
      Qed
    SCC:
     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)}
     SPSC:
      Simple Projection:
       pi(lt#) = 0
      Strict:
       {}
      Qed
    SCC:
     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)}
     Fail