MAYBE
Time: 0.006697
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:
  DP:
   {         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}
  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}
  EDG:
   {(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#())
    (activate# n__s X -> activate# X, activate# n__minus(X1, X2) -> minus#(X1, X2))
    (activate# n__s X -> activate# X, activate# n__div(X1, X2) -> div#(activate X1, X2))
    (activate# n__s X -> activate# X, activate# n__div(X1, X2) -> activate# X1)
    (activate# n__s X -> activate# X, activate# n__s X -> s# activate X)
    (activate# n__s X -> activate# X, activate# n__s X -> activate# X)
    (activate# n__s X -> activate# X, activate# n__0() -> 0#())
    (if#(true(), X, Y) -> activate# X, activate# n__minus(X1, X2) -> minus#(X1, X2))
    (if#(true(), X, Y) -> activate# X, activate# n__div(X1, X2) -> div#(activate X1, X2))
    (if#(true(), X, Y) -> activate# X, activate# n__div(X1, X2) -> activate# X1)
    (if#(true(), X, Y) -> activate# X, activate# n__s X -> s# activate X)
    (if#(true(), X, Y) -> activate# X, activate# n__s X -> activate# X)
    (if#(true(), X, Y) -> activate# X, 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# Y, activate# n__minus(X1, X2) -> minus#(X1, X2))
    (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__div(X1, X2) -> activate# X1)
    (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__s X -> activate# X)
    (minus#(n__s X, n__s Y) -> activate# Y, activate# n__0() -> 0#())
    (div#(s X, n__s Y) -> activate# Y, activate# n__minus(X1, X2) -> minus#(X1, X2))
    (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__div(X1, X2) -> activate# X1)
    (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__s X -> activate# X)
    (div#(s X, n__s Y) -> activate# Y, 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#())
    (if#(false(), X, Y) -> activate# Y, activate# n__0() -> 0#())
    (if#(false(), X, Y) -> activate# Y, activate# n__s X -> activate# X)
    (if#(false(), X, Y) -> activate# Y, activate# n__s X -> s# activate X)
    (if#(false(), X, Y) -> activate# Y, activate# n__div(X1, X2) -> activate# X1)
    (if#(false(), X, Y) -> activate# Y, activate# n__div(X1, X2) -> div#(activate X1, X2))
    (if#(false(), X, Y) -> activate# Y, activate# n__minus(X1, X2) -> minus#(X1, X2))
    (geq#(n__s X, n__s Y) -> activate# Y, activate# n__0() -> 0#())
    (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__s X -> s# activate X)
    (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__div(X1, X2) -> div#(activate X1, X2))
    (geq#(n__s X, n__s Y) -> activate# Y, 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)
    (geq#(n__s X, n__s Y) -> activate# X, activate# n__0() -> 0#())
    (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__s X -> s# activate X)
    (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__div(X1, X2) -> div#(activate X1, X2))
    (geq#(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__0() -> 0#())
    (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__s X -> s# activate X)
    (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__div(X1, X2) -> div#(activate X1, X2))
    (minus#(n__s X, n__s Y) -> activate# X, activate# n__minus(X1, X2) -> minus#(X1, X2))
    (activate# n__div(X1, X2) -> div#(activate X1, X2), div#(s X, n__s Y) -> activate# Y)
    (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) -> if#(geq(X, activate Y), n__s n__div(n__minus(X, activate Y), n__s activate Y), n__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)
    (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)}
   STATUS:
    arrows: 0.774691
    SCCS (1):
     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 (15):
      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}
      Open