YES

Problem:
 minus(n__0(),Y) -> 0()
 minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
 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(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)
 0() -> n__0()
 s(X) -> n__s(X)
 div(X1,X2) -> n__div(X1,X2)
 minus(X1,X2) -> n__minus(X1,X2)
 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)
 activate(X) -> X

Proof:
 DP Processor:
  DPs:
   minus#(n__0(),Y) -> 0#()
   minus#(n__s(X),n__s(Y)) -> activate#(Y)
   minus#(n__s(X),n__s(Y)) -> activate#(X)
   minus#(n__s(X),n__s(Y)) -> minus#(activate(X),activate(Y))
   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)
   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)
  TRS:
   minus(n__0(),Y) -> 0()
   minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
   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(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)
   0() -> n__0()
   s(X) -> n__s(X)
   div(X1,X2) -> n__div(X1,X2)
   minus(X1,X2) -> n__minus(X1,X2)
   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)
   activate(X) -> X
  TDG Processor:
   DPs:
    minus#(n__0(),Y) -> 0#()
    minus#(n__s(X),n__s(Y)) -> activate#(Y)
    minus#(n__s(X),n__s(Y)) -> activate#(X)
    minus#(n__s(X),n__s(Y)) -> minus#(activate(X),activate(Y))
    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)
    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)
   TRS:
    minus(n__0(),Y) -> 0()
    minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
    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(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)
    0() -> n__0()
    s(X) -> n__s(X)
    div(X1,X2) -> n__div(X1,X2)
    minus(X1,X2) -> n__minus(X1,X2)
    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)
    activate(X) -> X
   graph:
    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#()
    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#()
    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)
    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)) -> geq#(X,activate(Y)) ->
    geq#(n__s(X),n__s(Y)) -> geq#(activate(X),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)) -> activate#(Y)
    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#()
    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)
    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#()
    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__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#()
    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__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__0(),Y) -> 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#()
    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#()
    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#()
    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#(X)
    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__0(),Y) -> 0#()
   SCC Processor:
    #sccs: 1
    #rules: 15
    #arcs: 73/324
    DPs:
     if#(false(),X,Y) -> activate#(Y)
     activate#(n__s(X)) -> activate#(X)
     activate#(n__div(X1,X2)) -> activate#(X1)
     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)
     minus#(n__s(X),n__s(Y)) -> activate#(X)
     minus#(n__s(X),n__s(Y)) -> minus#(activate(X),activate(Y))
     div#(s(X),n__s(Y)) -> geq#(X,activate(Y))
     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)) ->
     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)
    TRS:
     minus(n__0(),Y) -> 0()
     minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
     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(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)
     0() -> n__0()
     s(X) -> n__s(X)
     div(X1,X2) -> n__div(X1,X2)
     minus(X1,X2) -> n__minus(X1,X2)
     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)
     activate(X) -> X
    Arctic Interpretation Processor:
     dimension: 1
     usable rules:
      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(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)
      0() -> n__0()
      s(X) -> n__s(X)
      div(X1,X2) -> n__div(X1,X2)
      minus(X1,X2) -> n__minus(X1,X2)
      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)
      activate(X) -> X
     interpretation:
      [if#](x0, x1, x2) = x1 + x2 + 0,
      
      [div#](x0, x1) = x0 + 3x1 + 0,
      
      [geq#](x0, x1) = x0 + 3x1 + 0,
      
      [activate#](x0) = x0,
      
      [minus#](x0, x1) = x0 + 2x1,
      
      [if](x0, x1, x2) = x1 + x2 + 0,
      
      [n__div](x0, x1) = x0 + 3x1 + 0,
      
      [n__minus](x0, x1) = x0 + 2x1 + 0,
      
      [s](x0) = x0,
      
      [div](x0, x1) = x0 + 3x1 + 0,
      
      [false] = 2,
      
      [true] = 0,
      
      [geq](x0, x1) = x0 + x1 + 0,
      
      [activate](x0) = x0,
      
      [n__s](x0) = x0,
      
      [0] = 0,
      
      [minus](x0, x1) = x0 + 2x1 + 0,
      
      [n__0] = 0
     orientation:
      if#(false(),X,Y) = X + Y + 0 >= Y = activate#(Y)
      
      activate#(n__s(X)) = X >= X = activate#(X)
      
      activate#(n__div(X1,X2)) = X1 + 3X2 + 0 >= X1 = activate#(X1)
      
      activate#(n__div(X1,X2)) = X1 + 3X2 + 0 >= X1 + 3X2 + 0 = div#(activate(X1),X2)
      
      div#(s(X),n__s(Y)) = X + 3Y + 0 >= Y = activate#(Y)
      
      activate#(n__minus(X1,X2)) = X1 + 2X2 + 0 >= X1 + 2X2 = minus#(X1,X2)
      
      minus#(n__s(X),n__s(Y)) = X + 2Y >= Y = activate#(Y)
      
      minus#(n__s(X),n__s(Y)) = X + 2Y >= X = activate#(X)
      
      minus#(n__s(X),n__s(Y)) = X + 2Y >= X + 2Y = minus#(activate(X),activate(Y))
      
      div#(s(X),n__s(Y)) = X + 3Y + 0 >= X + 3Y + 0 = geq#(X,activate(Y))
      
      geq#(n__s(X),n__s(Y)) = X + 3Y + 0 >= Y = activate#(Y)
      
      geq#(n__s(X),n__s(Y)) = X + 3Y + 0 >= X = activate#(X)
      
      geq#(n__s(X),n__s(Y)) = X + 3Y + 0 >= X + 3Y + 0 = geq#(activate(X),activate(Y))
      
      div#(s(X),n__s(Y)) = X + 3Y + 0 >= X + 3Y + 0 = if#(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),
    n__0())
      
      if#(true(),X,Y) = X + Y + 0 >= X = activate#(X)
      
      minus(n__0(),Y) = 2Y + 0 >= 0 = 0()
      
      minus(n__s(X),n__s(Y)) = X + 2Y + 0 >= X + 2Y + 0 = minus(activate(X),activate(Y))
      
      geq(X,n__0()) = X + 0 >= 0 = true()
      
      geq(n__0(),n__s(Y)) = Y + 0 >= 2 = false()
      
      geq(n__s(X),n__s(Y)) = X + Y + 0 >= X + Y + 0 = geq(activate(X),activate(Y))
      
      div(0(),n__s(Y)) = 3Y + 0 >= 0 = 0()
      
      div(s(X),n__s(Y)) = X + 3Y + 0 >= X + 3Y + 0 = if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),
   n__0())
      
      if(true(),X,Y) = X + Y + 0 >= X = activate(X)
      
      if(false(),X,Y) = X + Y + 0 >= Y = activate(Y)
      
      0() = 0 >= 0 = n__0()
      
      s(X) = X >= X = n__s(X)
      
      div(X1,X2) = X1 + 3X2 + 0 >= X1 + 3X2 + 0 = n__div(X1,X2)
      
      minus(X1,X2) = X1 + 2X2 + 0 >= X1 + 2X2 + 0 = n__minus(X1,X2)
      
      activate(n__0()) = 0 >= 0 = 0()
      
      activate(n__s(X)) = X >= X = s(activate(X))
      
      activate(n__div(X1,X2)) = X1 + 3X2 + 0 >= X1 + 3X2 + 0 = div(activate(X1),X2)
      
      activate(n__minus(X1,X2)) = X1 + 2X2 + 0 >= X1 + 2X2 + 0 = minus(X1,X2)
      
      activate(X) = X >= X = X
     problem:
      DPs:
       if#(false(),X,Y) -> activate#(Y)
       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)
       minus#(n__s(X),n__s(Y)) -> activate#(X)
       minus#(n__s(X),n__s(Y)) -> minus#(activate(X),activate(Y))
       div#(s(X),n__s(Y)) -> geq#(X,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)) ->
       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)
      TRS:
       minus(n__0(),Y) -> 0()
       minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
       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(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)
       0() -> n__0()
       s(X) -> n__s(X)
       div(X1,X2) -> n__div(X1,X2)
       minus(X1,X2) -> n__minus(X1,X2)
       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)
       activate(X) -> X
     Restore Modifier:
      DPs:
       if#(false(),X,Y) -> activate#(Y)
       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)
       minus#(n__s(X),n__s(Y)) -> activate#(X)
       minus#(n__s(X),n__s(Y)) -> minus#(activate(X),activate(Y))
       div#(s(X),n__s(Y)) -> geq#(X,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)) ->
       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)
      TRS:
       minus(n__0(),Y) -> 0()
       minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
       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(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)
       0() -> n__0()
       s(X) -> n__s(X)
       div(X1,X2) -> n__div(X1,X2)
       minus(X1,X2) -> n__minus(X1,X2)
       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)
       activate(X) -> X
      Arctic Interpretation Processor:
       dimension: 1
       usable rules:
        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(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)
        0() -> n__0()
        s(X) -> n__s(X)
        div(X1,X2) -> n__div(X1,X2)
        minus(X1,X2) -> n__minus(X1,X2)
        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)
        activate(X) -> X
       interpretation:
        [if#](x0, x1, x2) = x1 + 7x2 + 6,
        
        [div#](x0, x1) = x0 + 7x1 + 7,
        
        [geq#](x0, x1) = x0 + 7,
        
        [activate#](x0) = x0 + 0,
        
        [minus#](x0, x1) = x0 + 0,
        
        [if](x0, x1, x2) = x1 + 7x2,
        
        [n__div](x0, x1) = x0 + 7x1 + 7,
        
        [n__minus](x0, x1) = x0 + x1 + 0,
        
        [s](x0) = x0 + 0,
        
        [div](x0, x1) = x0 + 7x1 + 7,
        
        [false] = 4,
        
        [true] = 4,
        
        [geq](x0, x1) = x1,
        
        [activate](x0) = x0,
        
        [n__s](x0) = x0 + 0,
        
        [0] = 0,
        
        [minus](x0, x1) = x0 + x1 + 0,
        
        [n__0] = 0
       orientation:
        if#(false(),X,Y) = X + 7Y + 6 >= Y + 0 = activate#(Y)
        
        activate#(n__s(X)) = X + 0 >= X + 0 = activate#(X)
        
        activate#(n__div(X1,X2)) = X1 + 7X2 + 7 >= X1 + 0 = activate#(X1)
        
        activate#(n__div(X1,X2)) = X1 + 7X2 + 7 >= X1 + 7X2 + 7 = div#(activate(X1),X2)
        
        activate#(n__minus(X1,X2)) = X1 + X2 + 0 >= X1 + 0 = minus#(X1,X2)
        
        minus#(n__s(X),n__s(Y)) = X + 0 >= X + 0 = activate#(X)
        
        minus#(n__s(X),n__s(Y)) = X + 0 >= X + 0 = minus#(activate(X),activate(Y))
        
        div#(s(X),n__s(Y)) = X + 7Y + 7 >= X + 7 = geq#(X,activate(Y))
        
        geq#(n__s(X),n__s(Y)) = X + 7 >= X + 0 = activate#(X)
        
        geq#(n__s(X),n__s(Y)) = X + 7 >= X + 7 = geq#(activate(X),activate(Y))
        
        div#(s(X),n__s(Y)) = X + 7Y + 7 >= X + 7Y + 7 = if#(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),
    n__0())
        
        if#(true(),X,Y) = X + 7Y + 6 >= X + 0 = activate#(X)
        
        minus(n__0(),Y) = Y + 0 >= 0 = 0()
        
        minus(n__s(X),n__s(Y)) = X + Y + 0 >= X + Y + 0 = minus(activate(X),activate(Y))
        
        geq(X,n__0()) = 0 >= 4 = true()
        
        geq(n__0(),n__s(Y)) = Y + 0 >= 4 = false()
        
        geq(n__s(X),n__s(Y)) = Y + 0 >= Y = geq(activate(X),activate(Y))
        
        div(0(),n__s(Y)) = 7Y + 7 >= 0 = 0()
        
        div(s(X),n__s(Y)) = X + 7Y + 7 >= X + 7Y + 7 = if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),
   n__0())
        
        if(true(),X,Y) = X + 7Y >= X = activate(X)
        
        if(false(),X,Y) = X + 7Y >= Y = activate(Y)
        
        0() = 0 >= 0 = n__0()
        
        s(X) = X + 0 >= X + 0 = n__s(X)
        
        div(X1,X2) = X1 + 7X2 + 7 >= X1 + 7X2 + 7 = n__div(X1,X2)
        
        minus(X1,X2) = X1 + X2 + 0 >= X1 + X2 + 0 = n__minus(X1,X2)
        
        activate(n__0()) = 0 >= 0 = 0()
        
        activate(n__s(X)) = X + 0 >= X + 0 = s(activate(X))
        
        activate(n__div(X1,X2)) = X1 + 7X2 + 7 >= X1 + 7X2 + 7 = div(activate(X1),X2)
        
        activate(n__minus(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = minus(X1,X2)
        
        activate(X) = X >= X = X
       problem:
        DPs:
         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)
         minus#(n__s(X),n__s(Y)) -> activate#(X)
         minus#(n__s(X),n__s(Y)) -> minus#(activate(X),activate(Y))
         div#(s(X),n__s(Y)) -> geq#(X,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)) ->
         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)
        TRS:
         minus(n__0(),Y) -> 0()
         minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
         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(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)
         0() -> n__0()
         s(X) -> n__s(X)
         div(X1,X2) -> n__div(X1,X2)
         minus(X1,X2) -> n__minus(X1,X2)
         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)
         activate(X) -> X
       Restore Modifier:
        DPs:
         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)
         minus#(n__s(X),n__s(Y)) -> activate#(X)
         minus#(n__s(X),n__s(Y)) -> minus#(activate(X),activate(Y))
         div#(s(X),n__s(Y)) -> geq#(X,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)) ->
         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)
        TRS:
         minus(n__0(),Y) -> 0()
         minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
         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(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)
         0() -> n__0()
         s(X) -> n__s(X)
         div(X1,X2) -> n__div(X1,X2)
         minus(X1,X2) -> n__minus(X1,X2)
         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)
         activate(X) -> X
        Arctic Interpretation Processor:
         dimension: 1
         usable rules:
          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(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)
          0() -> n__0()
          s(X) -> n__s(X)
          div(X1,X2) -> n__div(X1,X2)
          minus(X1,X2) -> n__minus(X1,X2)
          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)
          activate(X) -> X
         interpretation:
          [if#](x0, x1, x2) = x1 + 4x2 + 0,
          
          [div#](x0, x1) = 4x0 + 6x1,
          
          [geq#](x0, x1) = x0,
          
          [activate#](x0) = x0,
          
          [minus#](x0, x1) = x0,
          
          [if](x0, x1, x2) = x1 + 2x2 + 0,
          
          [n__div](x0, x1) = 4x0 + 6x1 + 0,
          
          [n__minus](x0, x1) = x0,
          
          [s](x0) = x0 + 0,
          
          [div](x0, x1) = 4x0 + 6x1 + 0,
          
          [false] = 2,
          
          [true] = 2,
          
          [geq](x0, x1) = 4x1 + 0,
          
          [activate](x0) = x0,
          
          [n__s](x0) = x0 + 0,
          
          [0] = 0,
          
          [minus](x0, x1) = x0,
          
          [n__0] = 0
         orientation:
          activate#(n__s(X)) = X + 0 >= X = activate#(X)
          
          activate#(n__div(X1,X2)) = 4X1 + 6X2 + 0 >= X1 = activate#(X1)
          
          activate#(n__div(X1,X2)) = 4X1 + 6X2 + 0 >= 4X1 + 6X2 = div#(activate(X1),X2)
          
          activate#(n__minus(X1,X2)) = X1 >= X1 = minus#(X1,X2)
          
          minus#(n__s(X),n__s(Y)) = X + 0 >= X = activate#(X)
          
          minus#(n__s(X),n__s(Y)) = X + 0 >= X = minus#(activate(X),activate(Y))
          
          div#(s(X),n__s(Y)) = 4X + 6Y + 6 >= X = geq#(X,activate(Y))
          
          geq#(n__s(X),n__s(Y)) = X + 0 >= X = activate#(X)
          
          geq#(n__s(X),n__s(Y)) = X + 0 >= X = geq#(activate(X),activate(Y))
          
          div#(s(X),n__s(Y)) = 4X + 6Y + 6 >= 4X + 6Y + 6 = if#(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),
    n__0())
          
          if#(true(),X,Y) = X + 4Y + 0 >= X = activate#(X)
          
          minus(n__0(),Y) = 0 >= 0 = 0()
          
          minus(n__s(X),n__s(Y)) = X + 0 >= X = minus(activate(X),activate(Y))
          
          geq(X,n__0()) = 4 >= 2 = true()
          
          geq(n__0(),n__s(Y)) = 4Y + 4 >= 2 = false()
          
          geq(n__s(X),n__s(Y)) = 4Y + 4 >= 4Y + 0 = geq(activate(X),activate(Y))
          
          div(0(),n__s(Y)) = 6Y + 6 >= 0 = 0()
          
          div(s(X),n__s(Y)) = 4X + 6Y + 6 >= 4X + 6Y + 6 = if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),
   n__0())
          
          if(true(),X,Y) = X + 2Y + 0 >= X = activate(X)
          
          if(false(),X,Y) = X + 2Y + 0 >= Y = activate(Y)
          
          0() = 0 >= 0 = n__0()
          
          s(X) = X + 0 >= X + 0 = n__s(X)
          
          div(X1,X2) = 4X1 + 6X2 + 0 >= 4X1 + 6X2 + 0 = n__div(X1,X2)
          
          minus(X1,X2) = X1 >= X1 = n__minus(X1,X2)
          
          activate(n__0()) = 0 >= 0 = 0()
          
          activate(n__s(X)) = X + 0 >= X + 0 = s(activate(X))
          
          activate(n__div(X1,X2)) = 4X1 + 6X2 + 0 >= 4X1 + 6X2 + 0 = div(activate(X1),X2)
          
          activate(n__minus(X1,X2)) = X1 >= X1 = minus(X1,X2)
          
          activate(X) = X >= X = X
         problem:
          DPs:
           activate#(n__s(X)) -> activate#(X)
           activate#(n__div(X1,X2)) -> div#(activate(X1),X2)
           activate#(n__minus(X1,X2)) -> minus#(X1,X2)
           minus#(n__s(X),n__s(Y)) -> activate#(X)
           minus#(n__s(X),n__s(Y)) -> minus#(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))
           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)
          TRS:
           minus(n__0(),Y) -> 0()
           minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
           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(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)
           0() -> n__0()
           s(X) -> n__s(X)
           div(X1,X2) -> n__div(X1,X2)
           minus(X1,X2) -> n__minus(X1,X2)
           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)
           activate(X) -> X
         Restore Modifier:
          DPs:
           activate#(n__s(X)) -> activate#(X)
           activate#(n__div(X1,X2)) -> div#(activate(X1),X2)
           activate#(n__minus(X1,X2)) -> minus#(X1,X2)
           minus#(n__s(X),n__s(Y)) -> activate#(X)
           minus#(n__s(X),n__s(Y)) -> minus#(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))
           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)
          TRS:
           minus(n__0(),Y) -> 0()
           minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
           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(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)
           0() -> n__0()
           s(X) -> n__s(X)
           div(X1,X2) -> n__div(X1,X2)
           minus(X1,X2) -> n__minus(X1,X2)
           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)
           activate(X) -> X
          SCC Processor:
           #sccs: 2
           #rules: 8
           #arcs: 53/81
           DPs:
            geq#(n__s(X),n__s(Y)) -> geq#(activate(X),activate(Y))
           TRS:
            minus(n__0(),Y) -> 0()
            minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
            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(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)
            0() -> n__0()
            s(X) -> n__s(X)
            div(X1,X2) -> n__div(X1,X2)
            minus(X1,X2) -> n__minus(X1,X2)
            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)
            activate(X) -> X
           Arctic Interpretation Processor:
            dimension: 1
            usable rules:
             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(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)
             0() -> n__0()
             s(X) -> n__s(X)
             div(X1,X2) -> n__div(X1,X2)
             minus(X1,X2) -> n__minus(X1,X2)
             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)
             activate(X) -> X
            interpretation:
             [geq#](x0, x1) = x0 + x1 + 0,
             
             [if](x0, x1, x2) = x1 + x2 + 0,
             
             [n__div](x0, x1) = x0 + 0,
             
             [n__minus](x0, x1) = x0 + 3,
             
             [s](x0) = 1x0 + 4,
             
             [div](x0, x1) = x0 + 0,
             
             [false] = 2,
             
             [true] = 1,
             
             [geq](x0, x1) = 0,
             
             [activate](x0) = x0,
             
             [n__s](x0) = 1x0 + 4,
             
             [0] = 4,
             
             [minus](x0, x1) = x0 + 3,
             
             [n__0] = 4
            orientation:
             geq#(n__s(X),n__s(Y)) = 1X + 1Y + 4 >= X + Y + 0 = geq#(activate(X),activate(Y))
             
             minus(n__0(),Y) = 4 >= 4 = 0()
             
             minus(n__s(X),n__s(Y)) = 1X + 4 >= X + 3 = minus(activate(X),activate(Y))
             
             geq(X,n__0()) = 0 >= 1 = true()
             
             geq(n__0(),n__s(Y)) = 0 >= 2 = false()
             
             geq(n__s(X),n__s(Y)) = 0 >= 0 = geq(activate(X),activate(Y))
             
             div(0(),n__s(Y)) = 4 >= 4 = 0()
             
             div(s(X),n__s(Y)) = 1X + 4 >= 1X + 4 = if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),
   n__0())
             
             if(true(),X,Y) = X + Y + 0 >= X = activate(X)
             
             if(false(),X,Y) = X + Y + 0 >= Y = activate(Y)
             
             0() = 4 >= 4 = n__0()
             
             s(X) = 1X + 4 >= 1X + 4 = n__s(X)
             
             div(X1,X2) = X1 + 0 >= X1 + 0 = n__div(X1,X2)
             
             minus(X1,X2) = X1 + 3 >= X1 + 3 = n__minus(X1,X2)
             
             activate(n__0()) = 4 >= 4 = 0()
             
             activate(n__s(X)) = 1X + 4 >= 1X + 4 = s(activate(X))
             
             activate(n__div(X1,X2)) = X1 + 0 >= X1 + 0 = div(activate(X1),X2)
             
             activate(n__minus(X1,X2)) = X1 + 3 >= X1 + 3 = minus(X1,X2)
             
             activate(X) = X >= X = X
            problem:
             DPs:
              
             TRS:
              minus(n__0(),Y) -> 0()
              minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
              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(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)
              0() -> n__0()
              s(X) -> n__s(X)
              div(X1,X2) -> n__div(X1,X2)
              minus(X1,X2) -> n__minus(X1,X2)
              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)
              activate(X) -> X
            Qed
           
           DPs:
            if#(true(),X,Y) -> activate#(X)
            activate#(n__s(X)) -> activate#(X)
            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__minus(X1,X2)) -> minus#(X1,X2)
            minus#(n__s(X),n__s(Y)) -> activate#(X)
            minus#(n__s(X),n__s(Y)) -> minus#(activate(X),activate(Y))
           TRS:
            minus(n__0(),Y) -> 0()
            minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
            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(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)
            0() -> n__0()
            s(X) -> n__s(X)
            div(X1,X2) -> n__div(X1,X2)
            minus(X1,X2) -> n__minus(X1,X2)
            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)
            activate(X) -> X
           Arctic Interpretation Processor:
            dimension: 1
            usable rules:
             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(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)
             0() -> n__0()
             s(X) -> n__s(X)
             div(X1,X2) -> n__div(X1,X2)
             minus(X1,X2) -> n__minus(X1,X2)
             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)
             activate(X) -> X
            interpretation:
             [if#](x0, x1, x2) = x1 + x2,
             
             [div#](x0, x1) = x1,
             
             [activate#](x0) = x0,
             
             [minus#](x0, x1) = x0 + x1 + 0,
             
             [if](x0, x1, x2) = x1 + x2 + 0,
             
             [n__div](x0, x1) = x1,
             
             [n__minus](x0, x1) = 4x0 + 1x1 + 4,
             
             [s](x0) = x0 + 0,
             
             [div](x0, x1) = x1,
             
             [false] = 2,
             
             [true] = 4,
             
             [geq](x0, x1) = 5x0 + 7x1 + 0,
             
             [activate](x0) = x0 + 0,
             
             [n__s](x0) = x0 + 0,
             
             [0] = 0,
             
             [minus](x0, x1) = 4x0 + 1x1 + 4,
             
             [n__0] = 0
            orientation:
             if#(true(),X,Y) = X + Y >= X = activate#(X)
             
             activate#(n__s(X)) = X + 0 >= X = activate#(X)
             
             activate#(n__div(X1,X2)) = X2 >= X2 = div#(activate(X1),X2)
             
             div#(s(X),n__s(Y)) = Y + 0 >= Y + 0 = if#(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),
    n__0())
             
             activate#(n__minus(X1,X2)) = 4X1 + 1X2 + 4 >= X1 + X2 + 0 = minus#(X1,X2)
             
             minus#(n__s(X),n__s(Y)) = X + Y + 0 >= X = activate#(X)
             
             minus#(n__s(X),n__s(Y)) = X + Y + 0 >= X + Y + 0 = minus#(activate(X),activate(Y))
             
             minus(n__0(),Y) = 1Y + 4 >= 0 = 0()
             
             minus(n__s(X),n__s(Y)) = 4X + 1Y + 4 >= 4X + 1Y + 4 = minus(activate(X),activate(Y))
             
             geq(X,n__0()) = 5X + 7 >= 4 = true()
             
             geq(n__0(),n__s(Y)) = 7Y + 7 >= 2 = false()
             
             geq(n__s(X),n__s(Y)) = 5X + 7Y + 7 >= 5X + 7Y + 7 = geq(activate(X),activate(Y))
             
             div(0(),n__s(Y)) = Y + 0 >= 0 = 0()
             
             div(s(X),n__s(Y)) = Y + 0 >= Y + 0 = if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),
   n__0())
             
             if(true(),X,Y) = X + Y + 0 >= X + 0 = activate(X)
             
             if(false(),X,Y) = X + Y + 0 >= Y + 0 = activate(Y)
             
             0() = 0 >= 0 = n__0()
             
             s(X) = X + 0 >= X + 0 = n__s(X)
             
             div(X1,X2) = X2 >= X2 = n__div(X1,X2)
             
             minus(X1,X2) = 4X1 + 1X2 + 4 >= 4X1 + 1X2 + 4 = n__minus(X1,X2)
             
             activate(n__0()) = 0 >= 0 = 0()
             
             activate(n__s(X)) = X + 0 >= X + 0 = s(activate(X))
             
             activate(n__div(X1,X2)) = X2 + 0 >= X2 = div(activate(X1),X2)
             
             activate(n__minus(X1,X2)) = 4X1 + 1X2 + 4 >= 4X1 + 1X2 + 4 = minus(X1,X2)
             
             activate(X) = X + 0 >= X = X
            problem:
             DPs:
              if#(true(),X,Y) -> activate#(X)
              activate#(n__s(X)) -> activate#(X)
              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())
              minus#(n__s(X),n__s(Y)) -> activate#(X)
              minus#(n__s(X),n__s(Y)) -> minus#(activate(X),activate(Y))
             TRS:
              minus(n__0(),Y) -> 0()
              minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
              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(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)
              0() -> n__0()
              s(X) -> n__s(X)
              div(X1,X2) -> n__div(X1,X2)
              minus(X1,X2) -> n__minus(X1,X2)
              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)
              activate(X) -> X
            Restore Modifier:
             DPs:
              if#(true(),X,Y) -> activate#(X)
              activate#(n__s(X)) -> activate#(X)
              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())
              minus#(n__s(X),n__s(Y)) -> activate#(X)
              minus#(n__s(X),n__s(Y)) -> minus#(activate(X),activate(Y))
             TRS:
              minus(n__0(),Y) -> 0()
              minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
              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(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)
              0() -> n__0()
              s(X) -> n__s(X)
              div(X1,X2) -> n__div(X1,X2)
              minus(X1,X2) -> n__minus(X1,X2)
              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)
              activate(X) -> X
             SCC Processor:
              #sccs: 2
              #rules: 5
              #arcs: 15/36
              DPs:
               minus#(n__s(X),n__s(Y)) -> minus#(activate(X),activate(Y))
              TRS:
               minus(n__0(),Y) -> 0()
               minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
               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(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)
               0() -> n__0()
               s(X) -> n__s(X)
               div(X1,X2) -> n__div(X1,X2)
               minus(X1,X2) -> n__minus(X1,X2)
               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)
               activate(X) -> X
              Arctic Interpretation Processor:
               dimension: 1
               usable rules:
                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(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)
                0() -> n__0()
                s(X) -> n__s(X)
                div(X1,X2) -> n__div(X1,X2)
                minus(X1,X2) -> n__minus(X1,X2)
                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)
                activate(X) -> X
               interpretation:
                [minus#](x0, x1) = x0 + x1 + 0,
                
                [if](x0, x1, x2) = x1 + x2 + 0,
                
                [n__div](x0, x1) = x0 + 0,
                
                [n__minus](x0, x1) = x0 + 3,
                
                [s](x0) = 1x0 + 4,
                
                [div](x0, x1) = x0 + 0,
                
                [false] = 2,
                
                [true] = 1,
                
                [geq](x0, x1) = 0,
                
                [activate](x0) = x0,
                
                [n__s](x0) = 1x0 + 4,
                
                [0] = 4,
                
                [minus](x0, x1) = x0 + 3,
                
                [n__0] = 4
               orientation:
                minus#(n__s(X),n__s(Y)) = 1X + 1Y + 4 >= X + Y + 0 = minus#(activate(X),activate(Y))
                
                minus(n__0(),Y) = 4 >= 4 = 0()
                
                minus(n__s(X),n__s(Y)) = 1X + 4 >= X + 3 = minus(activate(X),activate(Y))
                
                geq(X,n__0()) = 0 >= 1 = true()
                
                geq(n__0(),n__s(Y)) = 0 >= 2 = false()
                
                geq(n__s(X),n__s(Y)) = 0 >= 0 = geq(activate(X),activate(Y))
                
                div(0(),n__s(Y)) = 4 >= 4 = 0()
                
                div(s(X),n__s(Y)) = 1X + 4 >= 1X + 4 = if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),
   n__0())
                
                if(true(),X,Y) = X + Y + 0 >= X = activate(X)
                
                if(false(),X,Y) = X + Y + 0 >= Y = activate(Y)
                
                0() = 4 >= 4 = n__0()
                
                s(X) = 1X + 4 >= 1X + 4 = n__s(X)
                
                div(X1,X2) = X1 + 0 >= X1 + 0 = n__div(X1,X2)
                
                minus(X1,X2) = X1 + 3 >= X1 + 3 = n__minus(X1,X2)
                
                activate(n__0()) = 4 >= 4 = 0()
                
                activate(n__s(X)) = 1X + 4 >= 1X + 4 = s(activate(X))
                
                activate(n__div(X1,X2)) = X1 + 0 >= X1 + 0 = div(activate(X1),X2)
                
                activate(n__minus(X1,X2)) = X1 + 3 >= X1 + 3 = minus(X1,X2)
                
                activate(X) = X >= X = X
               problem:
                DPs:
                 
                TRS:
                 minus(n__0(),Y) -> 0()
                 minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
                 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(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)
                 0() -> n__0()
                 s(X) -> n__s(X)
                 div(X1,X2) -> n__div(X1,X2)
                 minus(X1,X2) -> n__minus(X1,X2)
                 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)
                 activate(X) -> X
               Qed
              
              DPs:
               if#(true(),X,Y) -> activate#(X)
               activate#(n__s(X)) -> activate#(X)
               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())
              TRS:
               minus(n__0(),Y) -> 0()
               minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
               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(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)
               0() -> n__0()
               s(X) -> n__s(X)
               div(X1,X2) -> n__div(X1,X2)
               minus(X1,X2) -> n__minus(X1,X2)
               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)
               activate(X) -> X
              Arctic Interpretation Processor:
               dimension: 1
               usable rules:
                minus(n__0(),Y) -> 0()
                minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
                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(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)
                0() -> n__0()
                s(X) -> n__s(X)
                div(X1,X2) -> n__div(X1,X2)
                minus(X1,X2) -> n__minus(X1,X2)
                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)
                activate(X) -> X
               interpretation:
                [if#](x0, x1, x2) = 1x0 + x1 + 6x2 + 0,
                
                [div#](x0, x1) = x0,
                
                [activate#](x0) = x0 + 4,
                
                [if](x0, x1, x2) = x1 + 7x2 + 0,
                
                [n__div](x0, x1) = 1x0 + 0,
                
                [n__minus](x0, x1) = 0,
                
                [s](x0) = x0 + 6,
                
                [div](x0, x1) = 1x0 + 0,
                
                [false] = 0,
                
                [true] = 3,
                
                [geq](x0, x1) = 3,
                
                [activate](x0) = x0,
                
                [n__s](x0) = x0 + 6,
                
                [0] = 0,
                
                [minus](x0, x1) = 0,
                
                [n__0] = 0
               orientation:
                if#(true(),X,Y) = X + 6Y + 4 >= X + 4 = activate#(X)
                
                activate#(n__s(X)) = X + 6 >= X + 4 = activate#(X)
                
                activate#(n__div(X1,X2)) = 1X1 + 4 >= X1 = div#(activate(X1),X2)
                
                div#(s(X),n__s(Y)) = X + 6 >= 6 = if#(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),
    n__0())
                
                minus(n__0(),Y) = 0 >= 0 = 0()
                
                minus(n__s(X),n__s(Y)) = 0 >= 0 = minus(activate(X),activate(Y))
                
                geq(X,n__0()) = 3 >= 3 = true()
                
                geq(n__0(),n__s(Y)) = 3 >= 0 = false()
                
                geq(n__s(X),n__s(Y)) = 3 >= 3 = geq(activate(X),activate(Y))
                
                div(0(),n__s(Y)) = 1 >= 0 = 0()
                
                div(s(X),n__s(Y)) = 1X + 7 >= 7 = if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),
   n__0())
                
                if(true(),X,Y) = X + 7Y + 0 >= X = activate(X)
                
                if(false(),X,Y) = X + 7Y + 0 >= Y = activate(Y)
                
                0() = 0 >= 0 = n__0()
                
                s(X) = X + 6 >= X + 6 = n__s(X)
                
                div(X1,X2) = 1X1 + 0 >= 1X1 + 0 = n__div(X1,X2)
                
                minus(X1,X2) = 0 >= 0 = n__minus(X1,X2)
                
                activate(n__0()) = 0 >= 0 = 0()
                
                activate(n__s(X)) = X + 6 >= X + 6 = s(activate(X))
                
                activate(n__div(X1,X2)) = 1X1 + 0 >= 1X1 + 0 = div(activate(X1),X2)
                
                activate(n__minus(X1,X2)) = 0 >= 0 = minus(X1,X2)
                
                activate(X) = X >= X = X
               problem:
                DPs:
                 if#(true(),X,Y) -> activate#(X)
                 activate#(n__s(X)) -> 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())
                TRS:
                 minus(n__0(),Y) -> 0()
                 minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
                 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(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)
                 0() -> n__0()
                 s(X) -> n__s(X)
                 div(X1,X2) -> n__div(X1,X2)
                 minus(X1,X2) -> n__minus(X1,X2)
                 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)
                 activate(X) -> X
               Restore Modifier:
                DPs:
                 if#(true(),X,Y) -> activate#(X)
                 activate#(n__s(X)) -> 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())
                TRS:
                 minus(n__0(),Y) -> 0()
                 minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
                 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(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)
                 0() -> n__0()
                 s(X) -> n__s(X)
                 div(X1,X2) -> n__div(X1,X2)
                 minus(X1,X2) -> n__minus(X1,X2)
                 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)
                 activate(X) -> X
                SCC Processor:
                 #sccs: 1
                 #rules: 1
                 #arcs: 6/9
                 DPs:
                  activate#(n__s(X)) -> activate#(X)
                 TRS:
                  minus(n__0(),Y) -> 0()
                  minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
                  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(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)
                  0() -> n__0()
                  s(X) -> n__s(X)
                  div(X1,X2) -> n__div(X1,X2)
                  minus(X1,X2) -> n__minus(X1,X2)
                  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)
                  activate(X) -> X
                 Subterm Criterion Processor:
                  simple projection:
                   pi(activate#) = 0
                  problem:
                   DPs:
                    
                   TRS:
                    minus(n__0(),Y) -> 0()
                    minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
                    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(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)
                    0() -> n__0()
                    s(X) -> n__s(X)
                    div(X1,X2) -> n__div(X1,X2)
                    minus(X1,X2) -> n__minus(X1,X2)
                    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)
                    activate(X) -> X
                  Qed