MAYBE
TRS:
 {                       0() -> n__0(),
               minus(X1, X2) -> n__minus(X1, X2),
            minus(n__0(), Y) -> 0(),
     minus(n__s(X), n__s(Y)) -> minus(activate(X), activate(Y)),
                 activate(X) -> X,
            activate(n__0()) -> 0(),
           activate(n__s(X)) -> s(activate(X)),
    activate(n__div(X1, X2)) -> div(activate(X1), X2),
  activate(n__minus(X1, X2)) -> minus(X1, X2),
              geq(X, n__0()) -> true(),
        geq(n__0(), n__s(Y)) -> false(),
       geq(n__s(X), n__s(Y)) -> geq(activate(X), activate(Y)),
                 div(X1, X2) -> n__div(X1, X2),
           div(0(), n__s(Y)) -> 0(),
          div(s(X), n__s(Y)) -> if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0()),
            if(true(), X, Y) -> activate(X),
           if(false(), X, Y) -> activate(Y),
                        s(X) -> n__s(X)}
 DP:
  Strict:
   {          minus#(n__0(), Y) -> 0#(),
       minus#(n__s(X), n__s(Y)) -> minus#(activate(X), activate(Y)),
       minus#(n__s(X), n__s(Y)) -> activate#(Y),
       minus#(n__s(X), n__s(Y)) -> activate#(X),
              activate#(n__0()) -> 0#(),
             activate#(n__s(X)) -> activate#(X),
             activate#(n__s(X)) -> s#(activate(X)),
      activate#(n__div(X1, X2)) -> activate#(X1),
      activate#(n__div(X1, X2)) -> div#(activate(X1), X2),
    activate#(n__minus(X1, X2)) -> minus#(X1, X2),
         geq#(n__s(X), n__s(Y)) -> activate#(Y),
         geq#(n__s(X), n__s(Y)) -> activate#(X),
         geq#(n__s(X), n__s(Y)) -> geq#(activate(X), activate(Y)),
            div#(s(X), n__s(Y)) -> activate#(Y),
            div#(s(X), n__s(Y)) -> geq#(X, activate(Y)),
            div#(s(X), n__s(Y)) -> if#(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0()),
              if#(true(), X, Y) -> activate#(X),
             if#(false(), X, Y) -> activate#(Y)}
  Weak:
  {                       0() -> n__0(),
                minus(X1, X2) -> n__minus(X1, X2),
             minus(n__0(), Y) -> 0(),
      minus(n__s(X), n__s(Y)) -> minus(activate(X), activate(Y)),
                  activate(X) -> X,
             activate(n__0()) -> 0(),
            activate(n__s(X)) -> s(activate(X)),
     activate(n__div(X1, X2)) -> div(activate(X1), X2),
   activate(n__minus(X1, X2)) -> minus(X1, X2),
               geq(X, n__0()) -> true(),
         geq(n__0(), n__s(Y)) -> false(),
        geq(n__s(X), n__s(Y)) -> geq(activate(X), activate(Y)),
                  div(X1, X2) -> n__div(X1, X2),
            div(0(), n__s(Y)) -> 0(),
           div(s(X), n__s(Y)) -> if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0()),
             if(true(), X, Y) -> activate(X),
            if(false(), X, Y) -> activate(Y),
                         s(X) -> n__s(X)}
  EDG:
   {(activate#(n__div(X1, X2)) -> div#(activate(X1), X2), div#(s(X), n__s(Y)) -> if#(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0()))
    (activate#(n__div(X1, X2)) -> div#(activate(X1), X2), div#(s(X), n__s(Y)) -> geq#(X, activate(Y)))
    (activate#(n__div(X1, X2)) -> div#(activate(X1), X2), div#(s(X), n__s(Y)) -> activate#(Y))
    (activate#(n__div(X1, X2)) -> activate#(X1), activate#(n__minus(X1, X2)) -> minus#(X1, X2))
    (activate#(n__div(X1, X2)) -> activate#(X1), activate#(n__div(X1, X2)) -> div#(activate(X1), X2))
    (activate#(n__div(X1, X2)) -> activate#(X1), activate#(n__div(X1, X2)) -> activate#(X1))
    (activate#(n__div(X1, X2)) -> activate#(X1), activate#(n__s(X)) -> s#(activate(X)))
    (activate#(n__div(X1, X2)) -> activate#(X1), activate#(n__s(X)) -> activate#(X))
    (activate#(n__div(X1, X2)) -> activate#(X1), activate#(n__0()) -> 0#())
    (geq#(n__s(X), n__s(Y)) -> geq#(activate(X), activate(Y)), geq#(n__s(X), n__s(Y)) -> geq#(activate(X), activate(Y)))
    (geq#(n__s(X), n__s(Y)) -> geq#(activate(X), activate(Y)), geq#(n__s(X), n__s(Y)) -> activate#(X))
    (geq#(n__s(X), n__s(Y)) -> geq#(activate(X), activate(Y)), geq#(n__s(X), n__s(Y)) -> activate#(Y))
    (minus#(n__s(X), n__s(Y)) -> activate#(X), activate#(n__minus(X1, X2)) -> minus#(X1, X2))
    (minus#(n__s(X), n__s(Y)) -> activate#(X), activate#(n__div(X1, X2)) -> div#(activate(X1), X2))
    (minus#(n__s(X), n__s(Y)) -> activate#(X), activate#(n__div(X1, X2)) -> activate#(X1))
    (minus#(n__s(X), n__s(Y)) -> activate#(X), activate#(n__s(X)) -> s#(activate(X)))
    (minus#(n__s(X), n__s(Y)) -> activate#(X), activate#(n__s(X)) -> activate#(X))
    (minus#(n__s(X), n__s(Y)) -> activate#(X), activate#(n__0()) -> 0#())
    (geq#(n__s(X), n__s(Y)) -> activate#(X), activate#(n__minus(X1, X2)) -> minus#(X1, X2))
    (geq#(n__s(X), n__s(Y)) -> activate#(X), activate#(n__div(X1, X2)) -> div#(activate(X1), X2))
    (geq#(n__s(X), n__s(Y)) -> activate#(X), activate#(n__div(X1, X2)) -> activate#(X1))
    (geq#(n__s(X), n__s(Y)) -> activate#(X), activate#(n__s(X)) -> s#(activate(X)))
    (geq#(n__s(X), n__s(Y)) -> activate#(X), activate#(n__s(X)) -> activate#(X))
    (geq#(n__s(X), n__s(Y)) -> activate#(X), activate#(n__0()) -> 0#())
    (activate#(n__minus(X1, X2)) -> minus#(X1, X2), minus#(n__s(X), n__s(Y)) -> activate#(X))
    (activate#(n__minus(X1, X2)) -> minus#(X1, X2), minus#(n__s(X), n__s(Y)) -> activate#(Y))
    (activate#(n__minus(X1, X2)) -> minus#(X1, X2), minus#(n__s(X), n__s(Y)) -> minus#(activate(X), activate(Y)))
    (activate#(n__minus(X1, X2)) -> minus#(X1, X2), minus#(n__0(), Y) -> 0#())
    (geq#(n__s(X), n__s(Y)) -> activate#(Y), activate#(n__minus(X1, X2)) -> minus#(X1, X2))
    (geq#(n__s(X), n__s(Y)) -> activate#(Y), activate#(n__div(X1, X2)) -> div#(activate(X1), X2))
    (geq#(n__s(X), n__s(Y)) -> activate#(Y), activate#(n__div(X1, X2)) -> activate#(X1))
    (geq#(n__s(X), n__s(Y)) -> activate#(Y), activate#(n__s(X)) -> s#(activate(X)))
    (geq#(n__s(X), n__s(Y)) -> activate#(Y), activate#(n__s(X)) -> activate#(X))
    (geq#(n__s(X), n__s(Y)) -> activate#(Y), activate#(n__0()) -> 0#())
    (if#(false(), X, Y) -> activate#(Y), activate#(n__minus(X1, X2)) -> minus#(X1, X2))
    (if#(false(), X, Y) -> activate#(Y), activate#(n__div(X1, X2)) -> div#(activate(X1), X2))
    (if#(false(), X, Y) -> activate#(Y), activate#(n__div(X1, X2)) -> activate#(X1))
    (if#(false(), X, Y) -> activate#(Y), activate#(n__s(X)) -> s#(activate(X)))
    (if#(false(), X, Y) -> activate#(Y), activate#(n__s(X)) -> activate#(X))
    (if#(false(), X, Y) -> activate#(Y), activate#(n__0()) -> 0#())
    (div#(s(X), n__s(Y)) -> activate#(Y), activate#(n__0()) -> 0#())
    (div#(s(X), n__s(Y)) -> activate#(Y), activate#(n__s(X)) -> activate#(X))
    (div#(s(X), n__s(Y)) -> activate#(Y), activate#(n__s(X)) -> s#(activate(X)))
    (div#(s(X), n__s(Y)) -> activate#(Y), activate#(n__div(X1, X2)) -> activate#(X1))
    (div#(s(X), n__s(Y)) -> activate#(Y), activate#(n__div(X1, X2)) -> div#(activate(X1), X2))
    (div#(s(X), n__s(Y)) -> activate#(Y), activate#(n__minus(X1, X2)) -> minus#(X1, X2))
    (minus#(n__s(X), n__s(Y)) -> activate#(Y), activate#(n__0()) -> 0#())
    (minus#(n__s(X), n__s(Y)) -> activate#(Y), activate#(n__s(X)) -> activate#(X))
    (minus#(n__s(X), n__s(Y)) -> activate#(Y), activate#(n__s(X)) -> s#(activate(X)))
    (minus#(n__s(X), n__s(Y)) -> activate#(Y), activate#(n__div(X1, X2)) -> activate#(X1))
    (minus#(n__s(X), n__s(Y)) -> activate#(Y), activate#(n__div(X1, X2)) -> div#(activate(X1), X2))
    (minus#(n__s(X), n__s(Y)) -> activate#(Y), activate#(n__minus(X1, X2)) -> minus#(X1, X2))
    (if#(true(), X, Y) -> activate#(X), activate#(n__0()) -> 0#())
    (if#(true(), X, Y) -> activate#(X), activate#(n__s(X)) -> activate#(X))
    (if#(true(), X, Y) -> activate#(X), activate#(n__s(X)) -> s#(activate(X)))
    (if#(true(), X, Y) -> activate#(X), activate#(n__div(X1, X2)) -> activate#(X1))
    (if#(true(), X, Y) -> activate#(X), activate#(n__div(X1, X2)) -> div#(activate(X1), X2))
    (if#(true(), X, Y) -> activate#(X), activate#(n__minus(X1, X2)) -> minus#(X1, X2))
    (activate#(n__s(X)) -> activate#(X), activate#(n__0()) -> 0#())
    (activate#(n__s(X)) -> activate#(X), activate#(n__s(X)) -> activate#(X))
    (activate#(n__s(X)) -> activate#(X), activate#(n__s(X)) -> s#(activate(X)))
    (activate#(n__s(X)) -> activate#(X), activate#(n__div(X1, X2)) -> activate#(X1))
    (activate#(n__s(X)) -> activate#(X), activate#(n__div(X1, X2)) -> div#(activate(X1), X2))
    (activate#(n__s(X)) -> activate#(X), activate#(n__minus(X1, X2)) -> minus#(X1, X2))
    (div#(s(X), n__s(Y)) -> geq#(X, activate(Y)), geq#(n__s(X), n__s(Y)) -> activate#(Y))
    (div#(s(X), n__s(Y)) -> geq#(X, activate(Y)), geq#(n__s(X), n__s(Y)) -> activate#(X))
    (div#(s(X), n__s(Y)) -> geq#(X, activate(Y)), geq#(n__s(X), n__s(Y)) -> geq#(activate(X), activate(Y)))
    (minus#(n__s(X), n__s(Y)) -> minus#(activate(X), activate(Y)), minus#(n__0(), Y) -> 0#())
    (minus#(n__s(X), n__s(Y)) -> minus#(activate(X), activate(Y)), minus#(n__s(X), n__s(Y)) -> minus#(activate(X), activate(Y)))
    (minus#(n__s(X), n__s(Y)) -> minus#(activate(X), activate(Y)), minus#(n__s(X), n__s(Y)) -> activate#(Y))
    (minus#(n__s(X), n__s(Y)) -> minus#(activate(X), activate(Y)), minus#(n__s(X), n__s(Y)) -> activate#(X))
    (div#(s(X), n__s(Y)) -> if#(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0()), if#(true(), X, Y) -> activate#(X))
    (div#(s(X), n__s(Y)) -> if#(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0()), if#(false(), X, Y) -> activate#(Y))}
   SCCS:
    Scc:
     {   minus#(n__s(X), n__s(Y)) -> minus#(activate(X), activate(Y)),
         minus#(n__s(X), n__s(Y)) -> activate#(Y),
         minus#(n__s(X), n__s(Y)) -> activate#(X),
               activate#(n__s(X)) -> activate#(X),
        activate#(n__div(X1, X2)) -> activate#(X1),
        activate#(n__div(X1, X2)) -> div#(activate(X1), X2),
      activate#(n__minus(X1, X2)) -> minus#(X1, X2),
           geq#(n__s(X), n__s(Y)) -> activate#(Y),
           geq#(n__s(X), n__s(Y)) -> activate#(X),
           geq#(n__s(X), n__s(Y)) -> geq#(activate(X), activate(Y)),
              div#(s(X), n__s(Y)) -> activate#(Y),
              div#(s(X), n__s(Y)) -> geq#(X, activate(Y)),
              div#(s(X), n__s(Y)) -> if#(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0()),
                if#(true(), X, Y) -> activate#(X),
               if#(false(), X, Y) -> activate#(Y)}
    SCC:
     Strict:
      {   minus#(n__s(X), n__s(Y)) -> minus#(activate(X), activate(Y)),
          minus#(n__s(X), n__s(Y)) -> activate#(Y),
          minus#(n__s(X), n__s(Y)) -> activate#(X),
                activate#(n__s(X)) -> activate#(X),
         activate#(n__div(X1, X2)) -> activate#(X1),
         activate#(n__div(X1, X2)) -> div#(activate(X1), X2),
       activate#(n__minus(X1, X2)) -> minus#(X1, X2),
            geq#(n__s(X), n__s(Y)) -> activate#(Y),
            geq#(n__s(X), n__s(Y)) -> activate#(X),
            geq#(n__s(X), n__s(Y)) -> geq#(activate(X), activate(Y)),
               div#(s(X), n__s(Y)) -> activate#(Y),
               div#(s(X), n__s(Y)) -> geq#(X, activate(Y)),
               div#(s(X), n__s(Y)) -> if#(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0()),
                 if#(true(), X, Y) -> activate#(X),
                if#(false(), X, Y) -> activate#(Y)}
     Weak:
     {                       0() -> n__0(),
                   minus(X1, X2) -> n__minus(X1, X2),
                minus(n__0(), Y) -> 0(),
         minus(n__s(X), n__s(Y)) -> minus(activate(X), activate(Y)),
                     activate(X) -> X,
                activate(n__0()) -> 0(),
               activate(n__s(X)) -> s(activate(X)),
        activate(n__div(X1, X2)) -> div(activate(X1), X2),
      activate(n__minus(X1, X2)) -> minus(X1, X2),
                  geq(X, n__0()) -> true(),
            geq(n__0(), n__s(Y)) -> false(),
           geq(n__s(X), n__s(Y)) -> geq(activate(X), activate(Y)),
                     div(X1, X2) -> n__div(X1, X2),
               div(0(), n__s(Y)) -> 0(),
              div(s(X), n__s(Y)) -> if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0()),
                if(true(), X, Y) -> activate(X),
               if(false(), X, Y) -> activate(Y),
                            s(X) -> n__s(X)}
     Fail