MAYBE
Trs:
 {       minus(n__0(), Y) -> 0(),
  minus(n__s(X), n__s(Y)) -> minus(activate(X), activate(Y)),
        div(0(), n__s(Y)) -> 0(),
       div(s(X), n__s(Y)) -> if(geq(X, activate(Y)), n__s(div(minus(X, activate(Y)), n__s(activate(Y)))), n__0()),
     geq(n__0(), n__s(Y)) -> false(),
    geq(n__s(X), n__s(Y)) -> geq(activate(X), activate(Y)),
           geq(X, n__0()) -> true(),
         if(true(), X, Y) -> activate(X),
        if(false(), X, Y) -> activate(Y),
                      0() -> n__0(),
                     s(X) -> n__s(X),
         activate(n__0()) -> 0(),
        activate(n__s(X)) -> s(X),
              activate(X) -> X}
 Comment:
  We consider a duplicating trs.
  FAIL:
   Open