MAYBE
Time: 0.004531
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:
  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)}
  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}
  EDG:
   {(cond#(true(), x, y, z) -> plus#(s y, z), 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) -> ge#(x, z), ge#(s u, s v) -> ge#(u, v))
    (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) -> cond#(ge(x, z), x, y, z), cond#(true(), x, y, z) -> plus#(s y, z))
    (plus#(n, s m) -> plus#(n, m), plus#(n, s m) -> plus#(n, m))
    (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))
    (ge#(s u, s v) -> ge#(u, v), ge#(s u, s v) -> ge#(u, v))}
   EDG:
    {(cond#(true(), x, y, z) -> plus#(s y, z), 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) -> ge#(x, z), ge#(s u, s v) -> ge#(u, v))
     (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) -> cond#(ge(x, z), x, y, z), cond#(true(), x, y, z) -> plus#(s y, z))
     (plus#(n, s m) -> plus#(n, m), plus#(n, s m) -> plus#(n, m))
     (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))
     (ge#(s u, s v) -> ge#(u, v), ge#(s u, s v) -> ge#(u, v))}
    EDG:
     {(cond#(true(), x, y, z) -> plus#(s y, z), 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) -> ge#(x, z), ge#(s u, s v) -> ge#(u, v))
      (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) -> cond#(ge(x, z), x, y, z), cond#(true(), x, y, z) -> plus#(s y, z))
      (plus#(n, s m) -> plus#(n, m), plus#(n, s m) -> plus#(n, m))
      (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))
      (ge#(s u, s v) -> ge#(u, v), ge#(s u, s v) -> ge#(u, v))}
     STATUS:
      arrows: 0.795918
      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)}
       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}
        Open
       
       
       SCC (1):
        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}
        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}
        Open