MAYBE
TRS:
 {         d(x, s(y), z) -> cond(ge(x, z), x, y, z),
            div(x, s(y)) -> d(x, s(y), 0()),
   cond(true(), x, y, z) -> s(d(x, s(y), plus(s(y), z))),
  cond(false(), x, y, z) -> 0(),
              ge(u, 0()) -> true(),
          ge(s(u), s(v)) -> ge(u, v),
           ge(0(), s(v)) -> false(),
           plus(n, s(m)) -> s(plus(n, m)),
            plus(n, 0()) -> n}
 DP:
  Strict:
   {        d#(x, s(y), z) -> cond#(ge(x, z), x, y, z),
            d#(x, s(y), z) -> ge#(x, z),
             div#(x, s(y)) -> d#(x, s(y), 0()),
    cond#(true(), x, y, z) -> d#(x, s(y), plus(s(y), z)),
    cond#(true(), x, y, z) -> plus#(s(y), z),
           ge#(s(u), s(v)) -> ge#(u, v),
            plus#(n, s(m)) -> plus#(n, m)}
  Weak:
  {         d(x, s(y), z) -> cond(ge(x, z), x, y, z),
             div(x, s(y)) -> d(x, s(y), 0()),
    cond(true(), x, y, z) -> s(d(x, s(y), plus(s(y), z))),
   cond(false(), x, y, z) -> 0(),
               ge(u, 0()) -> true(),
           ge(s(u), s(v)) -> ge(u, v),
            ge(0(), s(v)) -> false(),
            plus(n, s(m)) -> s(plus(n, m)),
             plus(n, 0()) -> n}
  EDG:
   {(plus#(n, s(m)) -> plus#(n, m), plus#(n, s(m)) -> plus#(n, m))
    (cond#(true(), x, y, z) -> d#(x, s(y), plus(s(y), z)), d#(x, s(y), z) -> ge#(x, z))
    (cond#(true(), x, y, z) -> d#(x, s(y), plus(s(y), z)), d#(x, s(y), z) -> cond#(ge(x, z), x, y, z))
    (d#(x, s(y), z) -> cond#(ge(x, z), x, y, z), cond#(true(), x, y, z) -> plus#(s(y), z))
    (d#(x, s(y), z) -> cond#(ge(x, z), x, y, z), cond#(true(), x, y, z) -> d#(x, s(y), plus(s(y), z)))
    (ge#(s(u), s(v)) -> ge#(u, v), ge#(s(u), s(v)) -> ge#(u, v))
    (div#(x, s(y)) -> d#(x, s(y), 0()), d#(x, s(y), z) -> cond#(ge(x, z), x, y, z))
    (div#(x, s(y)) -> d#(x, s(y), 0()), d#(x, s(y), z) -> ge#(x, z))
    (d#(x, s(y), z) -> ge#(x, z), ge#(s(u), s(v)) -> ge#(u, v))
    (cond#(true(), x, y, z) -> plus#(s(y), z), plus#(n, s(m)) -> plus#(n, m))}
   SCCS:
    Scc:
     {plus#(n, s(m)) -> plus#(n, m)}
    Scc:
     {ge#(s(u), s(v)) -> ge#(u, v)}
    Scc:
     {        d#(x, s(y), z) -> cond#(ge(x, z), x, y, z),
      cond#(true(), x, y, z) -> d#(x, s(y), plus(s(y), z))}
    SCC:
     Strict:
      {plus#(n, s(m)) -> plus#(n, m)}
     Weak:
     {         d(x, s(y), z) -> cond(ge(x, z), x, y, z),
                div(x, s(y)) -> d(x, s(y), 0()),
       cond(true(), x, y, z) -> s(d(x, s(y), plus(s(y), z))),
      cond(false(), x, y, z) -> 0(),
                  ge(u, 0()) -> true(),
              ge(s(u), s(v)) -> ge(u, v),
               ge(0(), s(v)) -> false(),
               plus(n, s(m)) -> s(plus(n, m)),
                plus(n, 0()) -> n}
     SPSC:
      Simple Projection:
       pi(plus#) = 1
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {ge#(s(u), s(v)) -> ge#(u, v)}
     Weak:
     {         d(x, s(y), z) -> cond(ge(x, z), x, y, z),
                div(x, s(y)) -> d(x, s(y), 0()),
       cond(true(), x, y, z) -> s(d(x, s(y), plus(s(y), z))),
      cond(false(), x, y, z) -> 0(),
                  ge(u, 0()) -> true(),
              ge(s(u), s(v)) -> ge(u, v),
               ge(0(), s(v)) -> false(),
               plus(n, s(m)) -> s(plus(n, m)),
                plus(n, 0()) -> n}
     SPSC:
      Simple Projection:
       pi(ge#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {        d#(x, s(y), z) -> cond#(ge(x, z), x, y, z),
       cond#(true(), x, y, z) -> d#(x, s(y), plus(s(y), z))}
     Weak:
     {         d(x, s(y), z) -> cond(ge(x, z), x, y, z),
                div(x, s(y)) -> d(x, s(y), 0()),
       cond(true(), x, y, z) -> s(d(x, s(y), plus(s(y), z))),
      cond(false(), x, y, z) -> 0(),
                  ge(u, 0()) -> true(),
              ge(s(u), s(v)) -> ge(u, v),
               ge(0(), s(v)) -> false(),
               plus(n, s(m)) -> s(plus(n, m)),
                plus(n, 0()) -> n}
     Fail