MAYBE
Time: 0.037394
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,
     plus(plus(n, m), u) -> plus(n, plus(m, u))}
 DP:
  DP:
   {         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),
      plus#(plus(n, m), u) -> plus#(n, plus(m, u)),
      plus#(plus(n, m), u) -> plus#(m, u)}
  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,
      plus(plus(n, m), u) -> plus(n, plus(m, u))}
  UR:
   {         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,
    plus(plus(n, m), u) -> plus(n, plus(m, u))}
   EDG:
    {(plus#(n, s m) -> plus#(n, m), plus#(plus(n, m), u) -> plus#(m, u))
     (plus#(n, s m) -> plus#(n, m), plus#(plus(n, m), u) -> plus#(n, plus(m, u)))
     (plus#(n, s m) -> plus#(n, m), plus#(n, s m) -> plus#(n, m))
     (cond#(true(), x, y, z) -> plus#(s y, z), plus#(n, s m) -> plus#(n, m))
     (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)))
     (plus#(plus(n, m), u) -> plus#(n, plus(m, u)), plus#(plus(n, m), u) -> plus#(m, u))
     (plus#(plus(n, m), u) -> plus#(n, plus(m, u)), plus#(plus(n, m), u) -> plus#(n, plus(m, u)))
     (plus#(plus(n, m), u) -> plus#(n, plus(m, u)), 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) -> cond#(ge(x, z), x, y, z))
     (cond#(true(), x, y, z) -> d#(x, s y, plus(s y, z)), d#(x, s y, z) -> ge#(x, z))
     (d#(x, s y, z) -> ge#(x, z), ge#(s u, s v) -> ge#(u, v))
     (plus#(plus(n, m), u) -> plus#(m, u), plus#(n, s m) -> plus#(n, m))
     (plus#(plus(n, m), u) -> plus#(m, u), plus#(plus(n, m), u) -> plus#(n, plus(m, u)))
     (plus#(plus(n, m), u) -> plus#(m, u), plus#(plus(n, m), u) -> plus#(m, u))
     (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))}
    STATUS:
     arrows: 0.777778
     SCCS (3):
      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:
       {       plus#(n, s m) -> plus#(n, m),
        plus#(plus(n, m), u) -> plus#(n, plus(m, u)),
        plus#(plus(n, m), u) -> plus#(m, u)}
      Scc:
       {ge#(s u, s v) -> ge#(u, v)}
      
      
      SCC (2):
       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,
           plus(plus(n, m), u) -> plus(n, plus(m, u))}
       Open
      
      SCC (3):
       Strict:
        {       plus#(n, s m) -> plus#(n, m),
         plus#(plus(n, m), u) -> plus#(n, plus(m, u)),
         plus#(plus(n, m), u) -> plus#(m, u)}
       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,
           plus(plus(n, m), u) -> plus(n, plus(m, u))}
       Open
      
      SCC (1):
       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,
           plus(plus(n, m), u) -> plus(n, plus(m, u))}
       Open