YES

Problem:
 active(minus(0(),Y)) -> mark(0())
 active(minus(s(X),s(Y))) -> mark(minus(X,Y))
 active(geq(X,0())) -> mark(true())
 active(geq(0(),s(Y))) -> mark(false())
 active(geq(s(X),s(Y))) -> mark(geq(X,Y))
 active(div(0(),s(Y))) -> mark(0())
 active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
 active(if(true(),X,Y)) -> mark(X)
 active(if(false(),X,Y)) -> mark(Y)
 mark(minus(X1,X2)) -> active(minus(X1,X2))
 mark(0()) -> active(0())
 mark(s(X)) -> active(s(mark(X)))
 mark(geq(X1,X2)) -> active(geq(X1,X2))
 mark(true()) -> active(true())
 mark(false()) -> active(false())
 mark(div(X1,X2)) -> active(div(mark(X1),X2))
 mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
 minus(mark(X1),X2) -> minus(X1,X2)
 minus(X1,mark(X2)) -> minus(X1,X2)
 minus(active(X1),X2) -> minus(X1,X2)
 minus(X1,active(X2)) -> minus(X1,X2)
 s(mark(X)) -> s(X)
 s(active(X)) -> s(X)
 geq(mark(X1),X2) -> geq(X1,X2)
 geq(X1,mark(X2)) -> geq(X1,X2)
 geq(active(X1),X2) -> geq(X1,X2)
 geq(X1,active(X2)) -> geq(X1,X2)
 div(mark(X1),X2) -> div(X1,X2)
 div(X1,mark(X2)) -> div(X1,X2)
 div(active(X1),X2) -> div(X1,X2)
 div(X1,active(X2)) -> div(X1,X2)
 if(mark(X1),X2,X3) -> if(X1,X2,X3)
 if(X1,mark(X2),X3) -> if(X1,X2,X3)
 if(X1,X2,mark(X3)) -> if(X1,X2,X3)
 if(active(X1),X2,X3) -> if(X1,X2,X3)
 if(X1,active(X2),X3) -> if(X1,X2,X3)
 if(X1,X2,active(X3)) -> if(X1,X2,X3)

Proof:
 DP Processor:
  DPs:
   active#(minus(0(),Y)) -> mark#(0())
   active#(minus(s(X),s(Y))) -> minus#(X,Y)
   active#(minus(s(X),s(Y))) -> mark#(minus(X,Y))
   active#(geq(X,0())) -> mark#(true())
   active#(geq(0(),s(Y))) -> mark#(false())
   active#(geq(s(X),s(Y))) -> geq#(X,Y)
   active#(geq(s(X),s(Y))) -> mark#(geq(X,Y))
   active#(div(0(),s(Y))) -> mark#(0())
   active#(div(s(X),s(Y))) -> minus#(X,Y)
   active#(div(s(X),s(Y))) -> div#(minus(X,Y),s(Y))
   active#(div(s(X),s(Y))) -> s#(div(minus(X,Y),s(Y)))
   active#(div(s(X),s(Y))) -> geq#(X,Y)
   active#(div(s(X),s(Y))) -> if#(geq(X,Y),s(div(minus(X,Y),s(Y))),0())
   active#(div(s(X),s(Y))) -> mark#(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
   active#(if(true(),X,Y)) -> mark#(X)
   active#(if(false(),X,Y)) -> mark#(Y)
   mark#(minus(X1,X2)) -> active#(minus(X1,X2))
   mark#(0()) -> active#(0())
   mark#(s(X)) -> mark#(X)
   mark#(s(X)) -> s#(mark(X))
   mark#(s(X)) -> active#(s(mark(X)))
   mark#(geq(X1,X2)) -> active#(geq(X1,X2))
   mark#(true()) -> active#(true())
   mark#(false()) -> active#(false())
   mark#(div(X1,X2)) -> mark#(X1)
   mark#(div(X1,X2)) -> div#(mark(X1),X2)
   mark#(div(X1,X2)) -> active#(div(mark(X1),X2))
   mark#(if(X1,X2,X3)) -> mark#(X1)
   mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
   mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
   minus#(mark(X1),X2) -> minus#(X1,X2)
   minus#(X1,mark(X2)) -> minus#(X1,X2)
   minus#(active(X1),X2) -> minus#(X1,X2)
   minus#(X1,active(X2)) -> minus#(X1,X2)
   s#(mark(X)) -> s#(X)
   s#(active(X)) -> s#(X)
   geq#(mark(X1),X2) -> geq#(X1,X2)
   geq#(X1,mark(X2)) -> geq#(X1,X2)
   geq#(active(X1),X2) -> geq#(X1,X2)
   geq#(X1,active(X2)) -> geq#(X1,X2)
   div#(mark(X1),X2) -> div#(X1,X2)
   div#(X1,mark(X2)) -> div#(X1,X2)
   div#(active(X1),X2) -> div#(X1,X2)
   div#(X1,active(X2)) -> div#(X1,X2)
   if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
   if#(X1,mark(X2),X3) -> if#(X1,X2,X3)
   if#(X1,X2,mark(X3)) -> if#(X1,X2,X3)
   if#(active(X1),X2,X3) -> if#(X1,X2,X3)
   if#(X1,active(X2),X3) -> if#(X1,X2,X3)
   if#(X1,X2,active(X3)) -> if#(X1,X2,X3)
  TRS:
   active(minus(0(),Y)) -> mark(0())
   active(minus(s(X),s(Y))) -> mark(minus(X,Y))
   active(geq(X,0())) -> mark(true())
   active(geq(0(),s(Y))) -> mark(false())
   active(geq(s(X),s(Y))) -> mark(geq(X,Y))
   active(div(0(),s(Y))) -> mark(0())
   active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
   active(if(true(),X,Y)) -> mark(X)
   active(if(false(),X,Y)) -> mark(Y)
   mark(minus(X1,X2)) -> active(minus(X1,X2))
   mark(0()) -> active(0())
   mark(s(X)) -> active(s(mark(X)))
   mark(geq(X1,X2)) -> active(geq(X1,X2))
   mark(true()) -> active(true())
   mark(false()) -> active(false())
   mark(div(X1,X2)) -> active(div(mark(X1),X2))
   mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
   minus(mark(X1),X2) -> minus(X1,X2)
   minus(X1,mark(X2)) -> minus(X1,X2)
   minus(active(X1),X2) -> minus(X1,X2)
   minus(X1,active(X2)) -> minus(X1,X2)
   s(mark(X)) -> s(X)
   s(active(X)) -> s(X)
   geq(mark(X1),X2) -> geq(X1,X2)
   geq(X1,mark(X2)) -> geq(X1,X2)
   geq(active(X1),X2) -> geq(X1,X2)
   geq(X1,active(X2)) -> geq(X1,X2)
   div(mark(X1),X2) -> div(X1,X2)
   div(X1,mark(X2)) -> div(X1,X2)
   div(active(X1),X2) -> div(X1,X2)
   div(X1,active(X2)) -> div(X1,X2)
   if(mark(X1),X2,X3) -> if(X1,X2,X3)
   if(X1,mark(X2),X3) -> if(X1,X2,X3)
   if(X1,X2,mark(X3)) -> if(X1,X2,X3)
   if(active(X1),X2,X3) -> if(X1,X2,X3)
   if(X1,active(X2),X3) -> if(X1,X2,X3)
   if(X1,X2,active(X3)) -> if(X1,X2,X3)
  EDG Processor:
   DPs:
    active#(minus(0(),Y)) -> mark#(0())
    active#(minus(s(X),s(Y))) -> minus#(X,Y)
    active#(minus(s(X),s(Y))) -> mark#(minus(X,Y))
    active#(geq(X,0())) -> mark#(true())
    active#(geq(0(),s(Y))) -> mark#(false())
    active#(geq(s(X),s(Y))) -> geq#(X,Y)
    active#(geq(s(X),s(Y))) -> mark#(geq(X,Y))
    active#(div(0(),s(Y))) -> mark#(0())
    active#(div(s(X),s(Y))) -> minus#(X,Y)
    active#(div(s(X),s(Y))) -> div#(minus(X,Y),s(Y))
    active#(div(s(X),s(Y))) -> s#(div(minus(X,Y),s(Y)))
    active#(div(s(X),s(Y))) -> geq#(X,Y)
    active#(div(s(X),s(Y))) -> if#(geq(X,Y),s(div(minus(X,Y),s(Y))),0())
    active#(div(s(X),s(Y))) -> mark#(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
    active#(if(true(),X,Y)) -> mark#(X)
    active#(if(false(),X,Y)) -> mark#(Y)
    mark#(minus(X1,X2)) -> active#(minus(X1,X2))
    mark#(0()) -> active#(0())
    mark#(s(X)) -> mark#(X)
    mark#(s(X)) -> s#(mark(X))
    mark#(s(X)) -> active#(s(mark(X)))
    mark#(geq(X1,X2)) -> active#(geq(X1,X2))
    mark#(true()) -> active#(true())
    mark#(false()) -> active#(false())
    mark#(div(X1,X2)) -> mark#(X1)
    mark#(div(X1,X2)) -> div#(mark(X1),X2)
    mark#(div(X1,X2)) -> active#(div(mark(X1),X2))
    mark#(if(X1,X2,X3)) -> mark#(X1)
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
    minus#(mark(X1),X2) -> minus#(X1,X2)
    minus#(X1,mark(X2)) -> minus#(X1,X2)
    minus#(active(X1),X2) -> minus#(X1,X2)
    minus#(X1,active(X2)) -> minus#(X1,X2)
    s#(mark(X)) -> s#(X)
    s#(active(X)) -> s#(X)
    geq#(mark(X1),X2) -> geq#(X1,X2)
    geq#(X1,mark(X2)) -> geq#(X1,X2)
    geq#(active(X1),X2) -> geq#(X1,X2)
    geq#(X1,active(X2)) -> geq#(X1,X2)
    div#(mark(X1),X2) -> div#(X1,X2)
    div#(X1,mark(X2)) -> div#(X1,X2)
    div#(active(X1),X2) -> div#(X1,X2)
    div#(X1,active(X2)) -> div#(X1,X2)
    if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
    if#(X1,mark(X2),X3) -> if#(X1,X2,X3)
    if#(X1,X2,mark(X3)) -> if#(X1,X2,X3)
    if#(active(X1),X2,X3) -> if#(X1,X2,X3)
    if#(X1,active(X2),X3) -> if#(X1,X2,X3)
    if#(X1,X2,active(X3)) -> if#(X1,X2,X3)
   TRS:
    active(minus(0(),Y)) -> mark(0())
    active(minus(s(X),s(Y))) -> mark(minus(X,Y))
    active(geq(X,0())) -> mark(true())
    active(geq(0(),s(Y))) -> mark(false())
    active(geq(s(X),s(Y))) -> mark(geq(X,Y))
    active(div(0(),s(Y))) -> mark(0())
    active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
    active(if(true(),X,Y)) -> mark(X)
    active(if(false(),X,Y)) -> mark(Y)
    mark(minus(X1,X2)) -> active(minus(X1,X2))
    mark(0()) -> active(0())
    mark(s(X)) -> active(s(mark(X)))
    mark(geq(X1,X2)) -> active(geq(X1,X2))
    mark(true()) -> active(true())
    mark(false()) -> active(false())
    mark(div(X1,X2)) -> active(div(mark(X1),X2))
    mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
    minus(mark(X1),X2) -> minus(X1,X2)
    minus(X1,mark(X2)) -> minus(X1,X2)
    minus(active(X1),X2) -> minus(X1,X2)
    minus(X1,active(X2)) -> minus(X1,X2)
    s(mark(X)) -> s(X)
    s(active(X)) -> s(X)
    geq(mark(X1),X2) -> geq(X1,X2)
    geq(X1,mark(X2)) -> geq(X1,X2)
    geq(active(X1),X2) -> geq(X1,X2)
    geq(X1,active(X2)) -> geq(X1,X2)
    div(mark(X1),X2) -> div(X1,X2)
    div(X1,mark(X2)) -> div(X1,X2)
    div(active(X1),X2) -> div(X1,X2)
    div(X1,active(X2)) -> div(X1,X2)
    if(mark(X1),X2,X3) -> if(X1,X2,X3)
    if(X1,mark(X2),X3) -> if(X1,X2,X3)
    if(X1,X2,mark(X3)) -> if(X1,X2,X3)
    if(active(X1),X2,X3) -> if(X1,X2,X3)
    if(X1,active(X2),X3) -> if(X1,X2,X3)
    if(X1,X2,active(X3)) -> if(X1,X2,X3)
   graph:
    if#(mark(X1),X2,X3) -> if#(X1,X2,X3) ->
    if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
    if#(mark(X1),X2,X3) -> if#(X1,X2,X3) ->
    if#(X1,mark(X2),X3) -> if#(X1,X2,X3)
    if#(mark(X1),X2,X3) -> if#(X1,X2,X3) ->
    if#(X1,X2,mark(X3)) -> if#(X1,X2,X3)
    if#(mark(X1),X2,X3) -> if#(X1,X2,X3) ->
    if#(active(X1),X2,X3) -> if#(X1,X2,X3)
    if#(mark(X1),X2,X3) -> if#(X1,X2,X3) ->
    if#(X1,active(X2),X3) -> if#(X1,X2,X3)
    if#(mark(X1),X2,X3) -> if#(X1,X2,X3) ->
    if#(X1,X2,active(X3)) -> if#(X1,X2,X3)
    if#(active(X1),X2,X3) -> if#(X1,X2,X3) ->
    if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
    if#(active(X1),X2,X3) -> if#(X1,X2,X3) ->
    if#(X1,mark(X2),X3) -> if#(X1,X2,X3)
    if#(active(X1),X2,X3) -> if#(X1,X2,X3) ->
    if#(X1,X2,mark(X3)) -> if#(X1,X2,X3)
    if#(active(X1),X2,X3) -> if#(X1,X2,X3) ->
    if#(active(X1),X2,X3) -> if#(X1,X2,X3)
    if#(active(X1),X2,X3) -> if#(X1,X2,X3) ->
    if#(X1,active(X2),X3) -> if#(X1,X2,X3)
    if#(active(X1),X2,X3) -> if#(X1,X2,X3) ->
    if#(X1,X2,active(X3)) -> if#(X1,X2,X3)
    if#(X1,mark(X2),X3) -> if#(X1,X2,X3) ->
    if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
    if#(X1,mark(X2),X3) -> if#(X1,X2,X3) ->
    if#(X1,mark(X2),X3) -> if#(X1,X2,X3)
    if#(X1,mark(X2),X3) -> if#(X1,X2,X3) ->
    if#(X1,X2,mark(X3)) -> if#(X1,X2,X3)
    if#(X1,mark(X2),X3) -> if#(X1,X2,X3) ->
    if#(active(X1),X2,X3) -> if#(X1,X2,X3)
    if#(X1,mark(X2),X3) -> if#(X1,X2,X3) ->
    if#(X1,active(X2),X3) -> if#(X1,X2,X3)
    if#(X1,mark(X2),X3) -> if#(X1,X2,X3) ->
    if#(X1,X2,active(X3)) -> if#(X1,X2,X3)
    if#(X1,active(X2),X3) -> if#(X1,X2,X3) ->
    if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
    if#(X1,active(X2),X3) -> if#(X1,X2,X3) ->
    if#(X1,mark(X2),X3) -> if#(X1,X2,X3)
    if#(X1,active(X2),X3) -> if#(X1,X2,X3) ->
    if#(X1,X2,mark(X3)) -> if#(X1,X2,X3)
    if#(X1,active(X2),X3) -> if#(X1,X2,X3) ->
    if#(active(X1),X2,X3) -> if#(X1,X2,X3)
    if#(X1,active(X2),X3) -> if#(X1,X2,X3) ->
    if#(X1,active(X2),X3) -> if#(X1,X2,X3)
    if#(X1,active(X2),X3) -> if#(X1,X2,X3) ->
    if#(X1,X2,active(X3)) -> if#(X1,X2,X3)
    if#(X1,X2,mark(X3)) -> if#(X1,X2,X3) ->
    if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
    if#(X1,X2,mark(X3)) -> if#(X1,X2,X3) ->
    if#(X1,mark(X2),X3) -> if#(X1,X2,X3)
    if#(X1,X2,mark(X3)) -> if#(X1,X2,X3) ->
    if#(X1,X2,mark(X3)) -> if#(X1,X2,X3)
    if#(X1,X2,mark(X3)) -> if#(X1,X2,X3) ->
    if#(active(X1),X2,X3) -> if#(X1,X2,X3)
    if#(X1,X2,mark(X3)) -> if#(X1,X2,X3) ->
    if#(X1,active(X2),X3) -> if#(X1,X2,X3)
    if#(X1,X2,mark(X3)) -> if#(X1,X2,X3) ->
    if#(X1,X2,active(X3)) -> if#(X1,X2,X3)
    if#(X1,X2,active(X3)) -> if#(X1,X2,X3) ->
    if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
    if#(X1,X2,active(X3)) -> if#(X1,X2,X3) ->
    if#(X1,mark(X2),X3) -> if#(X1,X2,X3)
    if#(X1,X2,active(X3)) -> if#(X1,X2,X3) ->
    if#(X1,X2,mark(X3)) -> if#(X1,X2,X3)
    if#(X1,X2,active(X3)) -> if#(X1,X2,X3) ->
    if#(active(X1),X2,X3) -> if#(X1,X2,X3)
    if#(X1,X2,active(X3)) -> if#(X1,X2,X3) ->
    if#(X1,active(X2),X3) -> if#(X1,X2,X3)
    if#(X1,X2,active(X3)) -> if#(X1,X2,X3) ->
    if#(X1,X2,active(X3)) -> if#(X1,X2,X3)
    s#(mark(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
    s#(mark(X)) -> s#(X) -> s#(active(X)) -> s#(X)
    s#(active(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
    s#(active(X)) -> s#(X) -> s#(active(X)) -> s#(X)
    div#(mark(X1),X2) -> div#(X1,X2) ->
    div#(mark(X1),X2) -> div#(X1,X2)
    div#(mark(X1),X2) -> div#(X1,X2) ->
    div#(X1,mark(X2)) -> div#(X1,X2)
    div#(mark(X1),X2) -> div#(X1,X2) ->
    div#(active(X1),X2) -> div#(X1,X2)
    div#(mark(X1),X2) -> div#(X1,X2) ->
    div#(X1,active(X2)) -> div#(X1,X2)
    div#(active(X1),X2) -> div#(X1,X2) ->
    div#(mark(X1),X2) -> div#(X1,X2)
    div#(active(X1),X2) -> div#(X1,X2) ->
    div#(X1,mark(X2)) -> div#(X1,X2)
    div#(active(X1),X2) -> div#(X1,X2) ->
    div#(active(X1),X2) -> div#(X1,X2)
    div#(active(X1),X2) -> div#(X1,X2) ->
    div#(X1,active(X2)) -> div#(X1,X2)
    div#(X1,mark(X2)) -> div#(X1,X2) ->
    div#(mark(X1),X2) -> div#(X1,X2)
    div#(X1,mark(X2)) -> div#(X1,X2) ->
    div#(X1,mark(X2)) -> div#(X1,X2)
    div#(X1,mark(X2)) -> div#(X1,X2) ->
    div#(active(X1),X2) -> div#(X1,X2)
    div#(X1,mark(X2)) -> div#(X1,X2) ->
    div#(X1,active(X2)) -> div#(X1,X2)
    div#(X1,active(X2)) -> div#(X1,X2) ->
    div#(mark(X1),X2) -> div#(X1,X2)
    div#(X1,active(X2)) -> div#(X1,X2) ->
    div#(X1,mark(X2)) -> div#(X1,X2)
    div#(X1,active(X2)) -> div#(X1,X2) ->
    div#(active(X1),X2) -> div#(X1,X2)
    div#(X1,active(X2)) -> div#(X1,X2) ->
    div#(X1,active(X2)) -> div#(X1,X2)
    geq#(mark(X1),X2) -> geq#(X1,X2) ->
    geq#(mark(X1),X2) -> geq#(X1,X2)
    geq#(mark(X1),X2) -> geq#(X1,X2) ->
    geq#(X1,mark(X2)) -> geq#(X1,X2)
    geq#(mark(X1),X2) -> geq#(X1,X2) ->
    geq#(active(X1),X2) -> geq#(X1,X2)
    geq#(mark(X1),X2) -> geq#(X1,X2) ->
    geq#(X1,active(X2)) -> geq#(X1,X2)
    geq#(active(X1),X2) -> geq#(X1,X2) ->
    geq#(mark(X1),X2) -> geq#(X1,X2)
    geq#(active(X1),X2) -> geq#(X1,X2) ->
    geq#(X1,mark(X2)) -> geq#(X1,X2)
    geq#(active(X1),X2) -> geq#(X1,X2) ->
    geq#(active(X1),X2) -> geq#(X1,X2)
    geq#(active(X1),X2) -> geq#(X1,X2) ->
    geq#(X1,active(X2)) -> geq#(X1,X2)
    geq#(X1,mark(X2)) -> geq#(X1,X2) ->
    geq#(mark(X1),X2) -> geq#(X1,X2)
    geq#(X1,mark(X2)) -> geq#(X1,X2) ->
    geq#(X1,mark(X2)) -> geq#(X1,X2)
    geq#(X1,mark(X2)) -> geq#(X1,X2) ->
    geq#(active(X1),X2) -> geq#(X1,X2)
    geq#(X1,mark(X2)) -> geq#(X1,X2) ->
    geq#(X1,active(X2)) -> geq#(X1,X2)
    geq#(X1,active(X2)) -> geq#(X1,X2) ->
    geq#(mark(X1),X2) -> geq#(X1,X2)
    geq#(X1,active(X2)) -> geq#(X1,X2) ->
    geq#(X1,mark(X2)) -> geq#(X1,X2)
    geq#(X1,active(X2)) -> geq#(X1,X2) ->
    geq#(active(X1),X2) -> geq#(X1,X2)
    geq#(X1,active(X2)) -> geq#(X1,X2) ->
    geq#(X1,active(X2)) -> geq#(X1,X2)
    minus#(mark(X1),X2) -> minus#(X1,X2) ->
    minus#(mark(X1),X2) -> minus#(X1,X2)
    minus#(mark(X1),X2) -> minus#(X1,X2) ->
    minus#(X1,mark(X2)) -> minus#(X1,X2)
    minus#(mark(X1),X2) -> minus#(X1,X2) ->
    minus#(active(X1),X2) -> minus#(X1,X2)
    minus#(mark(X1),X2) -> minus#(X1,X2) ->
    minus#(X1,active(X2)) -> minus#(X1,X2)
    minus#(active(X1),X2) -> minus#(X1,X2) ->
    minus#(mark(X1),X2) -> minus#(X1,X2)
    minus#(active(X1),X2) -> minus#(X1,X2) ->
    minus#(X1,mark(X2)) -> minus#(X1,X2)
    minus#(active(X1),X2) -> minus#(X1,X2) ->
    minus#(active(X1),X2) -> minus#(X1,X2)
    minus#(active(X1),X2) -> minus#(X1,X2) ->
    minus#(X1,active(X2)) -> minus#(X1,X2)
    minus#(X1,mark(X2)) -> minus#(X1,X2) ->
    minus#(mark(X1),X2) -> minus#(X1,X2)
    minus#(X1,mark(X2)) -> minus#(X1,X2) ->
    minus#(X1,mark(X2)) -> minus#(X1,X2)
    minus#(X1,mark(X2)) -> minus#(X1,X2) ->
    minus#(active(X1),X2) -> minus#(X1,X2)
    minus#(X1,mark(X2)) -> minus#(X1,X2) ->
    minus#(X1,active(X2)) -> minus#(X1,X2)
    minus#(X1,active(X2)) -> minus#(X1,X2) ->
    minus#(mark(X1),X2) -> minus#(X1,X2)
    minus#(X1,active(X2)) -> minus#(X1,X2) ->
    minus#(X1,mark(X2)) -> minus#(X1,X2)
    minus#(X1,active(X2)) -> minus#(X1,X2) ->
    minus#(active(X1),X2) -> minus#(X1,X2)
    minus#(X1,active(X2)) -> minus#(X1,X2) ->
    minus#(X1,active(X2)) -> minus#(X1,X2)
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3) ->
    if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3) ->
    if#(active(X1),X2,X3) -> if#(X1,X2,X3)
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(minus(X1,X2)) -> active#(minus(X1,X2))
    mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(0()) -> active#(0())
    mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(s(X)) -> mark#(X)
    mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(s(X)) -> s#(mark(X))
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(s(X)) -> active#(s(mark(X)))
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(geq(X1,X2)) -> active#(geq(X1,X2))
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(true()) -> active#(true())
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(false()) -> active#(false())
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(div(X1,X2)) -> mark#(X1)
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(div(X1,X2)) -> div#(mark(X1),X2)
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(div(X1,X2)) -> active#(div(mark(X1),X2))
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(if(X1,X2,X3)) -> mark#(X1)
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(minus(0(),Y)) -> mark#(0())
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(minus(s(X),s(Y))) -> minus#(X,Y)
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(minus(s(X),s(Y))) -> mark#(minus(X,Y))
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(geq(X,0())) -> mark#(true())
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(geq(0(),s(Y))) -> mark#(false())
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(geq(s(X),s(Y))) -> geq#(X,Y)
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(geq(s(X),s(Y))) -> mark#(geq(X,Y))
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(div(0(),s(Y))) -> mark#(0())
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(div(s(X),s(Y))) -> minus#(X,Y)
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(div(s(X),s(Y))) -> div#(minus(X,Y),s(Y))
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(div(s(X),s(Y))) -> s#(div(minus(X,Y),s(Y)))
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(div(s(X),s(Y))) -> geq#(X,Y)
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(div(s(X),s(Y))) -> if#(geq(X,Y),s(div(minus(X,Y),s(Y))),0())
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(div(s(X),s(Y))) -> mark#(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(if(true(),X,Y)) -> mark#(X)
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(if(false(),X,Y)) -> mark#(Y)
    mark#(div(X1,X2)) -> div#(mark(X1),X2) ->
    div#(mark(X1),X2) -> div#(X1,X2)
    mark#(div(X1,X2)) -> div#(mark(X1),X2) ->
    div#(active(X1),X2) -> div#(X1,X2)
    mark#(div(X1,X2)) -> mark#(X1) ->
    mark#(minus(X1,X2)) -> active#(minus(X1,X2))
    mark#(div(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
    mark#(div(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X)
    mark#(div(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> s#(mark(X))
    mark#(div(X1,X2)) -> mark#(X1) ->
    mark#(s(X)) -> active#(s(mark(X)))
    mark#(div(X1,X2)) -> mark#(X1) ->
    mark#(geq(X1,X2)) -> active#(geq(X1,X2))
    mark#(div(X1,X2)) -> mark#(X1) ->
    mark#(true()) -> active#(true())
    mark#(div(X1,X2)) -> mark#(X1) ->
    mark#(false()) -> active#(false())
    mark#(div(X1,X2)) -> mark#(X1) -> mark#(div(X1,X2)) -> mark#(X1)
    mark#(div(X1,X2)) -> mark#(X1) ->
    mark#(div(X1,X2)) -> div#(mark(X1),X2)
    mark#(div(X1,X2)) -> mark#(X1) ->
    mark#(div(X1,X2)) -> active#(div(mark(X1),X2))
    mark#(div(X1,X2)) -> mark#(X1) ->
    mark#(if(X1,X2,X3)) -> mark#(X1)
    mark#(div(X1,X2)) -> mark#(X1) ->
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
    mark#(div(X1,X2)) -> mark#(X1) ->
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
    mark#(div(X1,X2)) -> active#(div(mark(X1),X2)) ->
    active#(minus(0(),Y)) -> mark#(0())
    mark#(div(X1,X2)) -> active#(div(mark(X1),X2)) ->
    active#(minus(s(X),s(Y))) -> minus#(X,Y)
    mark#(div(X1,X2)) -> active#(div(mark(X1),X2)) ->
    active#(minus(s(X),s(Y))) -> mark#(minus(X,Y))
    mark#(div(X1,X2)) -> active#(div(mark(X1),X2)) ->
    active#(geq(X,0())) -> mark#(true())
    mark#(div(X1,X2)) -> active#(div(mark(X1),X2)) ->
    active#(geq(0(),s(Y))) -> mark#(false())
    mark#(div(X1,X2)) -> active#(div(mark(X1),X2)) ->
    active#(geq(s(X),s(Y))) -> geq#(X,Y)
    mark#(div(X1,X2)) -> active#(div(mark(X1),X2)) ->
    active#(geq(s(X),s(Y))) -> mark#(geq(X,Y))
    mark#(div(X1,X2)) -> active#(div(mark(X1),X2)) ->
    active#(div(0(),s(Y))) -> mark#(0())
    mark#(div(X1,X2)) -> active#(div(mark(X1),X2)) ->
    active#(div(s(X),s(Y))) -> minus#(X,Y)
    mark#(div(X1,X2)) -> active#(div(mark(X1),X2)) ->
    active#(div(s(X),s(Y))) -> div#(minus(X,Y),s(Y))
    mark#(div(X1,X2)) -> active#(div(mark(X1),X2)) ->
    active#(div(s(X),s(Y))) -> s#(div(minus(X,Y),s(Y)))
    mark#(div(X1,X2)) -> active#(div(mark(X1),X2)) ->
    active#(div(s(X),s(Y))) -> geq#(X,Y)
    mark#(div(X1,X2)) -> active#(div(mark(X1),X2)) ->
    active#(div(s(X),s(Y))) -> if#(geq(X,Y),s(div(minus(X,Y),s(Y))),0())
    mark#(div(X1,X2)) -> active#(div(mark(X1),X2)) ->
    active#(div(s(X),s(Y))) -> mark#(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
    mark#(div(X1,X2)) -> active#(div(mark(X1),X2)) ->
    active#(if(true(),X,Y)) -> mark#(X)
    mark#(div(X1,X2)) -> active#(div(mark(X1),X2)) ->
    active#(if(false(),X,Y)) -> mark#(Y)
    mark#(geq(X1,X2)) -> active#(geq(X1,X2)) ->
    active#(geq(X,0())) -> mark#(true())
    mark#(geq(X1,X2)) -> active#(geq(X1,X2)) ->
    active#(geq(0(),s(Y))) -> mark#(false())
    mark#(geq(X1,X2)) -> active#(geq(X1,X2)) ->
    active#(geq(s(X),s(Y))) -> geq#(X,Y)
    mark#(geq(X1,X2)) -> active#(geq(X1,X2)) ->
    active#(geq(s(X),s(Y))) -> mark#(geq(X,Y))
    mark#(s(X)) -> s#(mark(X)) -> s#(mark(X)) -> s#(X)
    mark#(s(X)) -> s#(mark(X)) -> s#(active(X)) -> s#(X)
    mark#(s(X)) -> mark#(X) -> mark#(minus(X1,X2)) -> active#(minus(X1,X2))
    mark#(s(X)) -> mark#(X) -> mark#(0()) -> active#(0())
    mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> s#(mark(X))
    mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
    mark#(s(X)) -> mark#(X) -> mark#(geq(X1,X2)) -> active#(geq(X1,X2))
    mark#(s(X)) -> mark#(X) -> mark#(true()) -> active#(true())
    mark#(s(X)) -> mark#(X) -> mark#(false()) -> active#(false())
    mark#(s(X)) -> mark#(X) -> mark#(div(X1,X2)) -> mark#(X1)
    mark#(s(X)) -> mark#(X) -> mark#(div(X1,X2)) -> div#(mark(X1),X2)
    mark#(s(X)) -> mark#(X) ->
    mark#(div(X1,X2)) -> active#(div(mark(X1),X2))
    mark#(s(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X1)
    mark#(s(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
    mark#(s(X)) -> mark#(X) ->
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(minus(0(),Y)) -> mark#(0())
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(minus(s(X),s(Y))) -> minus#(X,Y)
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(minus(s(X),s(Y))) -> mark#(minus(X,Y))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(geq(X,0())) -> mark#(true())
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(geq(0(),s(Y))) -> mark#(false())
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(geq(s(X),s(Y))) -> geq#(X,Y)
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(geq(s(X),s(Y))) -> mark#(geq(X,Y))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(div(0(),s(Y))) -> mark#(0())
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(div(s(X),s(Y))) -> minus#(X,Y)
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(div(s(X),s(Y))) -> div#(minus(X,Y),s(Y))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(div(s(X),s(Y))) -> s#(div(minus(X,Y),s(Y)))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(div(s(X),s(Y))) -> geq#(X,Y)
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(div(s(X),s(Y))) -> if#(geq(X,Y),s(div(minus(X,Y),s(Y))),0())
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(div(s(X),s(Y))) -> mark#(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(if(true(),X,Y)) -> mark#(X)
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(if(false(),X,Y)) -> mark#(Y)
    mark#(minus(X1,X2)) -> active#(minus(X1,X2)) ->
    active#(minus(0(),Y)) -> mark#(0())
    mark#(minus(X1,X2)) -> active#(minus(X1,X2)) ->
    active#(minus(s(X),s(Y))) -> minus#(X,Y)
    mark#(minus(X1,X2)) -> active#(minus(X1,X2)) ->
    active#(minus(s(X),s(Y))) -> mark#(minus(X,Y))
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(minus(X1,X2)) -> active#(minus(X1,X2))
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(0()) -> active#(0())
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(s(X)) -> mark#(X)
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(s(X)) -> s#(mark(X))
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(geq(X1,X2)) -> active#(geq(X1,X2))
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(true()) -> active#(true())
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(false()) -> active#(false())
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(div(X1,X2)) -> mark#(X1)
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(div(X1,X2)) -> div#(mark(X1),X2)
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(div(X1,X2)) -> active#(div(mark(X1),X2))
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(if(X1,X2,X3)) -> mark#(X1)
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(minus(X1,X2)) -> active#(minus(X1,X2))
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(0()) -> active#(0())
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(s(X)) -> mark#(X)
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(s(X)) -> s#(mark(X))
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(geq(X1,X2)) -> active#(geq(X1,X2))
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(true()) -> active#(true())
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(false()) -> active#(false())
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(div(X1,X2)) -> mark#(X1)
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(div(X1,X2)) -> div#(mark(X1),X2)
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(div(X1,X2)) -> active#(div(mark(X1),X2))
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(if(X1,X2,X3)) -> mark#(X1)
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
    active#(div(s(X),s(Y))) -> if#(geq(X,Y),s(div(minus(X,Y),s(Y))),0()) ->
    if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
    active#(div(s(X),s(Y))) -> if#(geq(X,Y),s(div(minus(X,Y),s(Y))),0()) ->
    if#(X1,mark(X2),X3) -> if#(X1,X2,X3)
    active#(div(s(X),s(Y))) -> if#(geq(X,Y),s(div(minus(X,Y),s(Y))),0()) ->
    if#(active(X1),X2,X3) -> if#(X1,X2,X3)
    active#(div(s(X),s(Y))) -> if#(geq(X,Y),s(div(minus(X,Y),s(Y))),0()) ->
    if#(X1,active(X2),X3) -> if#(X1,X2,X3)
    active#(div(s(X),s(Y))) -> s#(div(minus(X,Y),s(Y))) ->
    s#(mark(X)) -> s#(X)
    active#(div(s(X),s(Y))) -> s#(div(minus(X,Y),s(Y))) ->
    s#(active(X)) -> s#(X)
    active#(div(s(X),s(Y))) -> div#(minus(X,Y),s(Y)) ->
    div#(mark(X1),X2) -> div#(X1,X2)
    active#(div(s(X),s(Y))) -> div#(minus(X,Y),s(Y)) ->
    div#(X1,mark(X2)) -> div#(X1,X2)
    active#(div(s(X),s(Y))) -> div#(minus(X,Y),s(Y)) ->
    div#(active(X1),X2) -> div#(X1,X2)
    active#(div(s(X),s(Y))) -> div#(minus(X,Y),s(Y)) ->
    div#(X1,active(X2)) -> div#(X1,X2)
    active#(div(s(X),s(Y))) -> mark#(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) ->
    mark#(minus(X1,X2)) -> active#(minus(X1,X2))
    active#(div(s(X),s(Y))) -> mark#(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) ->
    mark#(s(X)) -> mark#(X)
    active#(div(s(X),s(Y))) -> mark#(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) ->
    mark#(s(X)) -> s#(mark(X))
    active#(div(s(X),s(Y))) -> mark#(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(div(s(X),s(Y))) -> mark#(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) ->
    mark#(geq(X1,X2)) -> active#(geq(X1,X2))
    active#(div(s(X),s(Y))) -> mark#(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) ->
    mark#(div(X1,X2)) -> mark#(X1)
    active#(div(s(X),s(Y))) -> mark#(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) ->
    mark#(div(X1,X2)) -> div#(mark(X1),X2)
    active#(div(s(X),s(Y))) -> mark#(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) ->
    mark#(div(X1,X2)) -> active#(div(mark(X1),X2))
    active#(div(s(X),s(Y))) -> mark#(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) ->
    mark#(if(X1,X2,X3)) -> mark#(X1)
    active#(div(s(X),s(Y))) -> mark#(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) ->
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
    active#(div(s(X),s(Y))) -> mark#(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) ->
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
    active#(div(0(),s(Y))) -> mark#(0()) ->
    mark#(0()) -> active#(0())
    active#(geq(s(X),s(Y))) -> mark#(geq(X,Y)) ->
    mark#(minus(X1,X2)) -> active#(minus(X1,X2))
    active#(geq(s(X),s(Y))) -> mark#(geq(X,Y)) ->
    mark#(s(X)) -> mark#(X)
    active#(geq(s(X),s(Y))) -> mark#(geq(X,Y)) ->
    mark#(s(X)) -> s#(mark(X))
    active#(geq(s(X),s(Y))) -> mark#(geq(X,Y)) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(geq(s(X),s(Y))) -> mark#(geq(X,Y)) ->
    mark#(geq(X1,X2)) -> active#(geq(X1,X2))
    active#(geq(s(X),s(Y))) -> mark#(geq(X,Y)) ->
    mark#(div(X1,X2)) -> mark#(X1)
    active#(geq(s(X),s(Y))) -> mark#(geq(X,Y)) ->
    mark#(div(X1,X2)) -> div#(mark(X1),X2)
    active#(geq(s(X),s(Y))) -> mark#(geq(X,Y)) ->
    mark#(div(X1,X2)) -> active#(div(mark(X1),X2))
    active#(geq(s(X),s(Y))) -> mark#(geq(X,Y)) ->
    mark#(if(X1,X2,X3)) -> mark#(X1)
    active#(geq(s(X),s(Y))) -> mark#(geq(X,Y)) ->
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
    active#(geq(s(X),s(Y))) -> mark#(geq(X,Y)) ->
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
    active#(geq(0(),s(Y))) -> mark#(false()) ->
    mark#(false()) -> active#(false())
    active#(geq(X,0())) -> mark#(true()) ->
    mark#(true()) -> active#(true())
    active#(minus(s(X),s(Y))) -> mark#(minus(X,Y)) ->
    mark#(minus(X1,X2)) -> active#(minus(X1,X2))
    active#(minus(s(X),s(Y))) -> mark#(minus(X,Y)) ->
    mark#(s(X)) -> mark#(X)
    active#(minus(s(X),s(Y))) -> mark#(minus(X,Y)) ->
    mark#(s(X)) -> s#(mark(X))
    active#(minus(s(X),s(Y))) -> mark#(minus(X,Y)) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(minus(s(X),s(Y))) -> mark#(minus(X,Y)) ->
    mark#(geq(X1,X2)) -> active#(geq(X1,X2))
    active#(minus(s(X),s(Y))) -> mark#(minus(X,Y)) ->
    mark#(div(X1,X2)) -> mark#(X1)
    active#(minus(s(X),s(Y))) -> mark#(minus(X,Y)) ->
    mark#(div(X1,X2)) -> div#(mark(X1),X2)
    active#(minus(s(X),s(Y))) -> mark#(minus(X,Y)) ->
    mark#(div(X1,X2)) -> active#(div(mark(X1),X2))
    active#(minus(s(X),s(Y))) -> mark#(minus(X,Y)) ->
    mark#(if(X1,X2,X3)) -> mark#(X1)
    active#(minus(s(X),s(Y))) -> mark#(minus(X,Y)) ->
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
    active#(minus(s(X),s(Y))) -> mark#(minus(X,Y)) ->
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
    active#(minus(0(),Y)) -> mark#(0()) -> mark#(0()) -> active#(0())
   SCC Processor:
    #sccs: 6
    #rules: 33
    #arcs: 266/2500
    DPs:
     mark#(if(X1,X2,X3)) -> mark#(X1)
     mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
     active#(if(false(),X,Y)) -> mark#(Y)
     mark#(div(X1,X2)) -> active#(div(mark(X1),X2))
     active#(if(true(),X,Y)) -> mark#(X)
     mark#(div(X1,X2)) -> mark#(X1)
     mark#(geq(X1,X2)) -> active#(geq(X1,X2))
     active#(geq(s(X),s(Y))) -> mark#(geq(X,Y))
     mark#(s(X)) -> active#(s(mark(X)))
     active#(div(s(X),s(Y))) -> mark#(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
     mark#(s(X)) -> mark#(X)
     mark#(minus(X1,X2)) -> active#(minus(X1,X2))
     active#(minus(s(X),s(Y))) -> mark#(minus(X,Y))
    TRS:
     active(minus(0(),Y)) -> mark(0())
     active(minus(s(X),s(Y))) -> mark(minus(X,Y))
     active(geq(X,0())) -> mark(true())
     active(geq(0(),s(Y))) -> mark(false())
     active(geq(s(X),s(Y))) -> mark(geq(X,Y))
     active(div(0(),s(Y))) -> mark(0())
     active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
     active(if(true(),X,Y)) -> mark(X)
     active(if(false(),X,Y)) -> mark(Y)
     mark(minus(X1,X2)) -> active(minus(X1,X2))
     mark(0()) -> active(0())
     mark(s(X)) -> active(s(mark(X)))
     mark(geq(X1,X2)) -> active(geq(X1,X2))
     mark(true()) -> active(true())
     mark(false()) -> active(false())
     mark(div(X1,X2)) -> active(div(mark(X1),X2))
     mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
     minus(mark(X1),X2) -> minus(X1,X2)
     minus(X1,mark(X2)) -> minus(X1,X2)
     minus(active(X1),X2) -> minus(X1,X2)
     minus(X1,active(X2)) -> minus(X1,X2)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     geq(mark(X1),X2) -> geq(X1,X2)
     geq(X1,mark(X2)) -> geq(X1,X2)
     geq(active(X1),X2) -> geq(X1,X2)
     geq(X1,active(X2)) -> geq(X1,X2)
     div(mark(X1),X2) -> div(X1,X2)
     div(X1,mark(X2)) -> div(X1,X2)
     div(active(X1),X2) -> div(X1,X2)
     div(X1,active(X2)) -> div(X1,X2)
     if(mark(X1),X2,X3) -> if(X1,X2,X3)
     if(X1,mark(X2),X3) -> if(X1,X2,X3)
     if(X1,X2,mark(X3)) -> if(X1,X2,X3)
     if(active(X1),X2,X3) -> if(X1,X2,X3)
     if(X1,active(X2),X3) -> if(X1,X2,X3)
     if(X1,X2,active(X3)) -> if(X1,X2,X3)
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [mark#](x0) = x0,
      
      [active#](x0) = x0,
      
      [if](x0, x1, x2) = x0 + x1 + x2,
      
      [div](x0, x1) = x0,
      
      [false] = 0,
      
      [true] = 0,
      
      [geq](x0, x1) = x0,
      
      [s](x0) = x0 + 1,
      
      [mark](x0) = x0,
      
      [active](x0) = x0,
      
      [minus](x0, x1) = 0,
      
      [0] = 0
     orientation:
      mark#(if(X1,X2,X3)) = X1 + X2 + X3 >= X1 = mark#(X1)
      
      mark#(if(X1,X2,X3)) = X1 + X2 + X3 >= X1 + X2 + X3 = active#(if(mark(X1),X2,X3))
      
      active#(if(false(),X,Y)) = X + Y >= Y = mark#(Y)
      
      mark#(div(X1,X2)) = X1 >= X1 = active#(div(mark(X1),X2))
      
      active#(if(true(),X,Y)) = X + Y >= X = mark#(X)
      
      mark#(div(X1,X2)) = X1 >= X1 = mark#(X1)
      
      mark#(geq(X1,X2)) = X1 >= X1 = active#(geq(X1,X2))
      
      active#(geq(s(X),s(Y))) = X + 1 >= X = mark#(geq(X,Y))
      
      mark#(s(X)) = X + 1 >= X + 1 = active#(s(mark(X)))
      
      active#(div(s(X),s(Y))) = X + 1 >= X + 1 = mark#(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
      
      mark#(s(X)) = X + 1 >= X = mark#(X)
      
      mark#(minus(X1,X2)) = 0 >= 0 = active#(minus(X1,X2))
      
      active#(minus(s(X),s(Y))) = 0 >= 0 = mark#(minus(X,Y))
      
      active(minus(0(),Y)) = 0 >= 0 = mark(0())
      
      active(minus(s(X),s(Y))) = 0 >= 0 = mark(minus(X,Y))
      
      active(geq(X,0())) = X >= 0 = mark(true())
      
      active(geq(0(),s(Y))) = 0 >= 0 = mark(false())
      
      active(geq(s(X),s(Y))) = X + 1 >= X = mark(geq(X,Y))
      
      active(div(0(),s(Y))) = 0 >= 0 = mark(0())
      
      active(div(s(X),s(Y))) = X + 1 >= X + 1 = mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
      
      active(if(true(),X,Y)) = X + Y >= X = mark(X)
      
      active(if(false(),X,Y)) = X + Y >= Y = mark(Y)
      
      mark(minus(X1,X2)) = 0 >= 0 = active(minus(X1,X2))
      
      mark(0()) = 0 >= 0 = active(0())
      
      mark(s(X)) = X + 1 >= X + 1 = active(s(mark(X)))
      
      mark(geq(X1,X2)) = X1 >= X1 = active(geq(X1,X2))
      
      mark(true()) = 0 >= 0 = active(true())
      
      mark(false()) = 0 >= 0 = active(false())
      
      mark(div(X1,X2)) = X1 >= X1 = active(div(mark(X1),X2))
      
      mark(if(X1,X2,X3)) = X1 + X2 + X3 >= X1 + X2 + X3 = active(if(mark(X1),X2,X3))
      
      minus(mark(X1),X2) = 0 >= 0 = minus(X1,X2)
      
      minus(X1,mark(X2)) = 0 >= 0 = minus(X1,X2)
      
      minus(active(X1),X2) = 0 >= 0 = minus(X1,X2)
      
      minus(X1,active(X2)) = 0 >= 0 = minus(X1,X2)
      
      s(mark(X)) = X + 1 >= X + 1 = s(X)
      
      s(active(X)) = X + 1 >= X + 1 = s(X)
      
      geq(mark(X1),X2) = X1 >= X1 = geq(X1,X2)
      
      geq(X1,mark(X2)) = X1 >= X1 = geq(X1,X2)
      
      geq(active(X1),X2) = X1 >= X1 = geq(X1,X2)
      
      geq(X1,active(X2)) = X1 >= X1 = geq(X1,X2)
      
      div(mark(X1),X2) = X1 >= X1 = div(X1,X2)
      
      div(X1,mark(X2)) = X1 >= X1 = div(X1,X2)
      
      div(active(X1),X2) = X1 >= X1 = div(X1,X2)
      
      div(X1,active(X2)) = X1 >= X1 = div(X1,X2)
      
      if(mark(X1),X2,X3) = X1 + X2 + X3 >= X1 + X2 + X3 = if(X1,X2,X3)
      
      if(X1,mark(X2),X3) = X1 + X2 + X3 >= X1 + X2 + X3 = if(X1,X2,X3)
      
      if(X1,X2,mark(X3)) = X1 + X2 + X3 >= X1 + X2 + X3 = if(X1,X2,X3)
      
      if(active(X1),X2,X3) = X1 + X2 + X3 >= X1 + X2 + X3 = if(X1,X2,X3)
      
      if(X1,active(X2),X3) = X1 + X2 + X3 >= X1 + X2 + X3 = if(X1,X2,X3)
      
      if(X1,X2,active(X3)) = X1 + X2 + X3 >= X1 + X2 + X3 = if(X1,X2,X3)
     problem:
      DPs:
       mark#(if(X1,X2,X3)) -> mark#(X1)
       mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
       active#(if(false(),X,Y)) -> mark#(Y)
       mark#(div(X1,X2)) -> active#(div(mark(X1),X2))
       active#(if(true(),X,Y)) -> mark#(X)
       mark#(div(X1,X2)) -> mark#(X1)
       mark#(geq(X1,X2)) -> active#(geq(X1,X2))
       mark#(s(X)) -> active#(s(mark(X)))
       active#(div(s(X),s(Y))) -> mark#(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
       mark#(minus(X1,X2)) -> active#(minus(X1,X2))
       active#(minus(s(X),s(Y))) -> mark#(minus(X,Y))
      TRS:
       active(minus(0(),Y)) -> mark(0())
       active(minus(s(X),s(Y))) -> mark(minus(X,Y))
       active(geq(X,0())) -> mark(true())
       active(geq(0(),s(Y))) -> mark(false())
       active(geq(s(X),s(Y))) -> mark(geq(X,Y))
       active(div(0(),s(Y))) -> mark(0())
       active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
       active(if(true(),X,Y)) -> mark(X)
       active(if(false(),X,Y)) -> mark(Y)
       mark(minus(X1,X2)) -> active(minus(X1,X2))
       mark(0()) -> active(0())
       mark(s(X)) -> active(s(mark(X)))
       mark(geq(X1,X2)) -> active(geq(X1,X2))
       mark(true()) -> active(true())
       mark(false()) -> active(false())
       mark(div(X1,X2)) -> active(div(mark(X1),X2))
       mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
       minus(mark(X1),X2) -> minus(X1,X2)
       minus(X1,mark(X2)) -> minus(X1,X2)
       minus(active(X1),X2) -> minus(X1,X2)
       minus(X1,active(X2)) -> minus(X1,X2)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(X)
       geq(mark(X1),X2) -> geq(X1,X2)
       geq(X1,mark(X2)) -> geq(X1,X2)
       geq(active(X1),X2) -> geq(X1,X2)
       geq(X1,active(X2)) -> geq(X1,X2)
       div(mark(X1),X2) -> div(X1,X2)
       div(X1,mark(X2)) -> div(X1,X2)
       div(active(X1),X2) -> div(X1,X2)
       div(X1,active(X2)) -> div(X1,X2)
       if(mark(X1),X2,X3) -> if(X1,X2,X3)
       if(X1,mark(X2),X3) -> if(X1,X2,X3)
       if(X1,X2,mark(X3)) -> if(X1,X2,X3)
       if(active(X1),X2,X3) -> if(X1,X2,X3)
       if(X1,active(X2),X3) -> if(X1,X2,X3)
       if(X1,X2,active(X3)) -> if(X1,X2,X3)
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [mark#](x0) = x0 + 1,
       
       [active#](x0) = x0 + 1,
       
       [if](x0, x1, x2) = x0 + x1 + x2 + 1,
       
       [div](x0, x1) = x0 + 1,
       
       [false] = 0,
       
       [true] = 0,
       
       [geq](x0, x1) = 0,
       
       [s](x0) = 0,
       
       [mark](x0) = x0,
       
       [active](x0) = x0,
       
       [minus](x0, x1) = 0,
       
       [0] = 0
      orientation:
       mark#(if(X1,X2,X3)) = X1 + X2 + X3 + 2 >= X1 + 1 = mark#(X1)
       
       mark#(if(X1,X2,X3)) = X1 + X2 + X3 + 2 >= X1 + X2 + X3 + 2 = active#(if(mark(X1),X2,X3))
       
       active#(if(false(),X,Y)) = X + Y + 2 >= Y + 1 = mark#(Y)
       
       mark#(div(X1,X2)) = X1 + 2 >= X1 + 2 = active#(div(mark(X1),X2))
       
       active#(if(true(),X,Y)) = X + Y + 2 >= X + 1 = mark#(X)
       
       mark#(div(X1,X2)) = X1 + 2 >= X1 + 1 = mark#(X1)
       
       mark#(geq(X1,X2)) = 1 >= 1 = active#(geq(X1,X2))
       
       mark#(s(X)) = 1 >= 1 = active#(s(mark(X)))
       
       active#(div(s(X),s(Y))) = 2 >= 2 = mark#(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
       
       mark#(minus(X1,X2)) = 1 >= 1 = active#(minus(X1,X2))
       
       active#(minus(s(X),s(Y))) = 1 >= 1 = mark#(minus(X,Y))
       
       active(minus(0(),Y)) = 0 >= 0 = mark(0())
       
       active(minus(s(X),s(Y))) = 0 >= 0 = mark(minus(X,Y))
       
       active(geq(X,0())) = 0 >= 0 = mark(true())
       
       active(geq(0(),s(Y))) = 0 >= 0 = mark(false())
       
       active(geq(s(X),s(Y))) = 0 >= 0 = mark(geq(X,Y))
       
       active(div(0(),s(Y))) = 1 >= 0 = mark(0())
       
       active(div(s(X),s(Y))) = 1 >= 1 = mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
       
       active(if(true(),X,Y)) = X + Y + 1 >= X = mark(X)
       
       active(if(false(),X,Y)) = X + Y + 1 >= Y = mark(Y)
       
       mark(minus(X1,X2)) = 0 >= 0 = active(minus(X1,X2))
       
       mark(0()) = 0 >= 0 = active(0())
       
       mark(s(X)) = 0 >= 0 = active(s(mark(X)))
       
       mark(geq(X1,X2)) = 0 >= 0 = active(geq(X1,X2))
       
       mark(true()) = 0 >= 0 = active(true())
       
       mark(false()) = 0 >= 0 = active(false())
       
       mark(div(X1,X2)) = X1 + 1 >= X1 + 1 = active(div(mark(X1),X2))
       
       mark(if(X1,X2,X3)) = X1 + X2 + X3 + 1 >= X1 + X2 + X3 + 1 = active(if(mark(X1),X2,X3))
       
       minus(mark(X1),X2) = 0 >= 0 = minus(X1,X2)
       
       minus(X1,mark(X2)) = 0 >= 0 = minus(X1,X2)
       
       minus(active(X1),X2) = 0 >= 0 = minus(X1,X2)
       
       minus(X1,active(X2)) = 0 >= 0 = minus(X1,X2)
       
       s(mark(X)) = 0 >= 0 = s(X)
       
       s(active(X)) = 0 >= 0 = s(X)
       
       geq(mark(X1),X2) = 0 >= 0 = geq(X1,X2)
       
       geq(X1,mark(X2)) = 0 >= 0 = geq(X1,X2)
       
       geq(active(X1),X2) = 0 >= 0 = geq(X1,X2)
       
       geq(X1,active(X2)) = 0 >= 0 = geq(X1,X2)
       
       div(mark(X1),X2) = X1 + 1 >= X1 + 1 = div(X1,X2)
       
       div(X1,mark(X2)) = X1 + 1 >= X1 + 1 = div(X1,X2)
       
       div(active(X1),X2) = X1 + 1 >= X1 + 1 = div(X1,X2)
       
       div(X1,active(X2)) = X1 + 1 >= X1 + 1 = div(X1,X2)
       
       if(mark(X1),X2,X3) = X1 + X2 + X3 + 1 >= X1 + X2 + X3 + 1 = if(X1,X2,X3)
       
       if(X1,mark(X2),X3) = X1 + X2 + X3 + 1 >= X1 + X2 + X3 + 1 = if(X1,X2,X3)
       
       if(X1,X2,mark(X3)) = X1 + X2 + X3 + 1 >= X1 + X2 + X3 + 1 = if(X1,X2,X3)
       
       if(active(X1),X2,X3) = X1 + X2 + X3 + 1 >= X1 + X2 + X3 + 1 = if(X1,X2,X3)
       
       if(X1,active(X2),X3) = X1 + X2 + X3 + 1 >= X1 + X2 + X3 + 1 = if(X1,X2,X3)
       
       if(X1,X2,active(X3)) = X1 + X2 + X3 + 1 >= X1 + X2 + X3 + 1 = if(X1,X2,X3)
      problem:
       DPs:
        mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
        mark#(div(X1,X2)) -> active#(div(mark(X1),X2))
        mark#(geq(X1,X2)) -> active#(geq(X1,X2))
        mark#(s(X)) -> active#(s(mark(X)))
        active#(div(s(X),s(Y))) -> mark#(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
        mark#(minus(X1,X2)) -> active#(minus(X1,X2))
        active#(minus(s(X),s(Y))) -> mark#(minus(X,Y))
       TRS:
        active(minus(0(),Y)) -> mark(0())
        active(minus(s(X),s(Y))) -> mark(minus(X,Y))
        active(geq(X,0())) -> mark(true())
        active(geq(0(),s(Y))) -> mark(false())
        active(geq(s(X),s(Y))) -> mark(geq(X,Y))
        active(div(0(),s(Y))) -> mark(0())
        active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
        active(if(true(),X,Y)) -> mark(X)
        active(if(false(),X,Y)) -> mark(Y)
        mark(minus(X1,X2)) -> active(minus(X1,X2))
        mark(0()) -> active(0())
        mark(s(X)) -> active(s(mark(X)))
        mark(geq(X1,X2)) -> active(geq(X1,X2))
        mark(true()) -> active(true())
        mark(false()) -> active(false())
        mark(div(X1,X2)) -> active(div(mark(X1),X2))
        mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
        minus(mark(X1),X2) -> minus(X1,X2)
        minus(X1,mark(X2)) -> minus(X1,X2)
        minus(active(X1),X2) -> minus(X1,X2)
        minus(X1,active(X2)) -> minus(X1,X2)
        s(mark(X)) -> s(X)
        s(active(X)) -> s(X)
        geq(mark(X1),X2) -> geq(X1,X2)
        geq(X1,mark(X2)) -> geq(X1,X2)
        geq(active(X1),X2) -> geq(X1,X2)
        geq(X1,active(X2)) -> geq(X1,X2)
        div(mark(X1),X2) -> div(X1,X2)
        div(X1,mark(X2)) -> div(X1,X2)
        div(active(X1),X2) -> div(X1,X2)
        div(X1,active(X2)) -> div(X1,X2)
        if(mark(X1),X2,X3) -> if(X1,X2,X3)
        if(X1,mark(X2),X3) -> if(X1,X2,X3)
        if(X1,X2,mark(X3)) -> if(X1,X2,X3)
        if(active(X1),X2,X3) -> if(X1,X2,X3)
        if(X1,active(X2),X3) -> if(X1,X2,X3)
        if(X1,X2,active(X3)) -> if(X1,X2,X3)
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [mark#](x0) = x0,
        
        [active#](x0) = 0,
        
        [if](x0, x1, x2) = 0,
        
        [div](x0, x1) = 0,
        
        [false] = 0,
        
        [true] = 0,
        
        [geq](x0, x1) = 0,
        
        [s](x0) = 1,
        
        [mark](x0) = 1,
        
        [active](x0) = 1,
        
        [minus](x0, x1) = 0,
        
        [0] = 0
       orientation:
        mark#(if(X1,X2,X3)) = 0 >= 0 = active#(if(mark(X1),X2,X3))
        
        mark#(div(X1,X2)) = 0 >= 0 = active#(div(mark(X1),X2))
        
        mark#(geq(X1,X2)) = 0 >= 0 = active#(geq(X1,X2))
        
        mark#(s(X)) = 1 >= 0 = active#(s(mark(X)))
        
        active#(div(s(X),s(Y))) = 0 >= 0 = mark#(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
        
        mark#(minus(X1,X2)) = 0 >= 0 = active#(minus(X1,X2))
        
        active#(minus(s(X),s(Y))) = 0 >= 0 = mark#(minus(X,Y))
        
        active(minus(0(),Y)) = 1 >= 1 = mark(0())
        
        active(minus(s(X),s(Y))) = 1 >= 1 = mark(minus(X,Y))
        
        active(geq(X,0())) = 1 >= 1 = mark(true())
        
        active(geq(0(),s(Y))) = 1 >= 1 = mark(false())
        
        active(geq(s(X),s(Y))) = 1 >= 1 = mark(geq(X,Y))
        
        active(div(0(),s(Y))) = 1 >= 1 = mark(0())
        
        active(div(s(X),s(Y))) = 1 >= 1 = mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
        
        active(if(true(),X,Y)) = 1 >= 1 = mark(X)
        
        active(if(false(),X,Y)) = 1 >= 1 = mark(Y)
        
        mark(minus(X1,X2)) = 1 >= 1 = active(minus(X1,X2))
        
        mark(0()) = 1 >= 1 = active(0())
        
        mark(s(X)) = 1 >= 1 = active(s(mark(X)))
        
        mark(geq(X1,X2)) = 1 >= 1 = active(geq(X1,X2))
        
        mark(true()) = 1 >= 1 = active(true())
        
        mark(false()) = 1 >= 1 = active(false())
        
        mark(div(X1,X2)) = 1 >= 1 = active(div(mark(X1),X2))
        
        mark(if(X1,X2,X3)) = 1 >= 1 = active(if(mark(X1),X2,X3))
        
        minus(mark(X1),X2) = 0 >= 0 = minus(X1,X2)
        
        minus(X1,mark(X2)) = 0 >= 0 = minus(X1,X2)
        
        minus(active(X1),X2) = 0 >= 0 = minus(X1,X2)
        
        minus(X1,active(X2)) = 0 >= 0 = minus(X1,X2)
        
        s(mark(X)) = 1 >= 1 = s(X)
        
        s(active(X)) = 1 >= 1 = s(X)
        
        geq(mark(X1),X2) = 0 >= 0 = geq(X1,X2)
        
        geq(X1,mark(X2)) = 0 >= 0 = geq(X1,X2)
        
        geq(active(X1),X2) = 0 >= 0 = geq(X1,X2)
        
        geq(X1,active(X2)) = 0 >= 0 = geq(X1,X2)
        
        div(mark(X1),X2) = 0 >= 0 = div(X1,X2)
        
        div(X1,mark(X2)) = 0 >= 0 = div(X1,X2)
        
        div(active(X1),X2) = 0 >= 0 = div(X1,X2)
        
        div(X1,active(X2)) = 0 >= 0 = div(X1,X2)
        
        if(mark(X1),X2,X3) = 0 >= 0 = if(X1,X2,X3)
        
        if(X1,mark(X2),X3) = 0 >= 0 = if(X1,X2,X3)
        
        if(X1,X2,mark(X3)) = 0 >= 0 = if(X1,X2,X3)
        
        if(active(X1),X2,X3) = 0 >= 0 = if(X1,X2,X3)
        
        if(X1,active(X2),X3) = 0 >= 0 = if(X1,X2,X3)
        
        if(X1,X2,active(X3)) = 0 >= 0 = if(X1,X2,X3)
       problem:
        DPs:
         mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
         mark#(div(X1,X2)) -> active#(div(mark(X1),X2))
         mark#(geq(X1,X2)) -> active#(geq(X1,X2))
         active#(div(s(X),s(Y))) -> mark#(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
         mark#(minus(X1,X2)) -> active#(minus(X1,X2))
         active#(minus(s(X),s(Y))) -> mark#(minus(X,Y))
        TRS:
         active(minus(0(),Y)) -> mark(0())
         active(minus(s(X),s(Y))) -> mark(minus(X,Y))
         active(geq(X,0())) -> mark(true())
         active(geq(0(),s(Y))) -> mark(false())
         active(geq(s(X),s(Y))) -> mark(geq(X,Y))
         active(div(0(),s(Y))) -> mark(0())
         active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
         active(if(true(),X,Y)) -> mark(X)
         active(if(false(),X,Y)) -> mark(Y)
         mark(minus(X1,X2)) -> active(minus(X1,X2))
         mark(0()) -> active(0())
         mark(s(X)) -> active(s(mark(X)))
         mark(geq(X1,X2)) -> active(geq(X1,X2))
         mark(true()) -> active(true())
         mark(false()) -> active(false())
         mark(div(X1,X2)) -> active(div(mark(X1),X2))
         mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
         minus(mark(X1),X2) -> minus(X1,X2)
         minus(X1,mark(X2)) -> minus(X1,X2)
         minus(active(X1),X2) -> minus(X1,X2)
         minus(X1,active(X2)) -> minus(X1,X2)
         s(mark(X)) -> s(X)
         s(active(X)) -> s(X)
         geq(mark(X1),X2) -> geq(X1,X2)
         geq(X1,mark(X2)) -> geq(X1,X2)
         geq(active(X1),X2) -> geq(X1,X2)
         geq(X1,active(X2)) -> geq(X1,X2)
         div(mark(X1),X2) -> div(X1,X2)
         div(X1,mark(X2)) -> div(X1,X2)
         div(active(X1),X2) -> div(X1,X2)
         div(X1,active(X2)) -> div(X1,X2)
         if(mark(X1),X2,X3) -> if(X1,X2,X3)
         if(X1,mark(X2),X3) -> if(X1,X2,X3)
         if(X1,X2,mark(X3)) -> if(X1,X2,X3)
         if(active(X1),X2,X3) -> if(X1,X2,X3)
         if(X1,active(X2),X3) -> if(X1,X2,X3)
         if(X1,X2,active(X3)) -> if(X1,X2,X3)
       Matrix Interpretation Processor:
        dimension: 1
        interpretation:
         [mark#](x0) = x0,
         
         [active#](x0) = 0,
         
         [if](x0, x1, x2) = 0,
         
         [div](x0, x1) = 0,
         
         [false] = 0,
         
         [true] = 0,
         
         [geq](x0, x1) = 1,
         
         [s](x0) = 0,
         
         [mark](x0) = 1,
         
         [active](x0) = 1,
         
         [minus](x0, x1) = 0,
         
         [0] = 0
        orientation:
         mark#(if(X1,X2,X3)) = 0 >= 0 = active#(if(mark(X1),X2,X3))
         
         mark#(div(X1,X2)) = 0 >= 0 = active#(div(mark(X1),X2))
         
         mark#(geq(X1,X2)) = 1 >= 0 = active#(geq(X1,X2))
         
         active#(div(s(X),s(Y))) = 0 >= 0 = mark#(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
         
         mark#(minus(X1,X2)) = 0 >= 0 = active#(minus(X1,X2))
         
         active#(minus(s(X),s(Y))) = 0 >= 0 = mark#(minus(X,Y))
         
         active(minus(0(),Y)) = 1 >= 1 = mark(0())
         
         active(minus(s(X),s(Y))) = 1 >= 1 = mark(minus(X,Y))
         
         active(geq(X,0())) = 1 >= 1 = mark(true())
         
         active(geq(0(),s(Y))) = 1 >= 1 = mark(false())
         
         active(geq(s(X),s(Y))) = 1 >= 1 = mark(geq(X,Y))
         
         active(div(0(),s(Y))) = 1 >= 1 = mark(0())
         
         active(div(s(X),s(Y))) = 1 >= 1 = mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
         
         active(if(true(),X,Y)) = 1 >= 1 = mark(X)
         
         active(if(false(),X,Y)) = 1 >= 1 = mark(Y)
         
         mark(minus(X1,X2)) = 1 >= 1 = active(minus(X1,X2))
         
         mark(0()) = 1 >= 1 = active(0())
         
         mark(s(X)) = 1 >= 1 = active(s(mark(X)))
         
         mark(geq(X1,X2)) = 1 >= 1 = active(geq(X1,X2))
         
         mark(true()) = 1 >= 1 = active(true())
         
         mark(false()) = 1 >= 1 = active(false())
         
         mark(div(X1,X2)) = 1 >= 1 = active(div(mark(X1),X2))
         
         mark(if(X1,X2,X3)) = 1 >= 1 = active(if(mark(X1),X2,X3))
         
         minus(mark(X1),X2) = 0 >= 0 = minus(X1,X2)
         
         minus(X1,mark(X2)) = 0 >= 0 = minus(X1,X2)
         
         minus(active(X1),X2) = 0 >= 0 = minus(X1,X2)
         
         minus(X1,active(X2)) = 0 >= 0 = minus(X1,X2)
         
         s(mark(X)) = 0 >= 0 = s(X)
         
         s(active(X)) = 0 >= 0 = s(X)
         
         geq(mark(X1),X2) = 1 >= 1 = geq(X1,X2)
         
         geq(X1,mark(X2)) = 1 >= 1 = geq(X1,X2)
         
         geq(active(X1),X2) = 1 >= 1 = geq(X1,X2)
         
         geq(X1,active(X2)) = 1 >= 1 = geq(X1,X2)
         
         div(mark(X1),X2) = 0 >= 0 = div(X1,X2)
         
         div(X1,mark(X2)) = 0 >= 0 = div(X1,X2)
         
         div(active(X1),X2) = 0 >= 0 = div(X1,X2)
         
         div(X1,active(X2)) = 0 >= 0 = div(X1,X2)
         
         if(mark(X1),X2,X3) = 0 >= 0 = if(X1,X2,X3)
         
         if(X1,mark(X2),X3) = 0 >= 0 = if(X1,X2,X3)
         
         if(X1,X2,mark(X3)) = 0 >= 0 = if(X1,X2,X3)
         
         if(active(X1),X2,X3) = 0 >= 0 = if(X1,X2,X3)
         
         if(X1,active(X2),X3) = 0 >= 0 = if(X1,X2,X3)
         
         if(X1,X2,active(X3)) = 0 >= 0 = if(X1,X2,X3)
        problem:
         DPs:
          mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
          mark#(div(X1,X2)) -> active#(div(mark(X1),X2))
          active#(div(s(X),s(Y))) -> mark#(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
          mark#(minus(X1,X2)) -> active#(minus(X1,X2))
          active#(minus(s(X),s(Y))) -> mark#(minus(X,Y))
         TRS:
          active(minus(0(),Y)) -> mark(0())
          active(minus(s(X),s(Y))) -> mark(minus(X,Y))
          active(geq(X,0())) -> mark(true())
          active(geq(0(),s(Y))) -> mark(false())
          active(geq(s(X),s(Y))) -> mark(geq(X,Y))
          active(div(0(),s(Y))) -> mark(0())
          active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
          active(if(true(),X,Y)) -> mark(X)
          active(if(false(),X,Y)) -> mark(Y)
          mark(minus(X1,X2)) -> active(minus(X1,X2))
          mark(0()) -> active(0())
          mark(s(X)) -> active(s(mark(X)))
          mark(geq(X1,X2)) -> active(geq(X1,X2))
          mark(true()) -> active(true())
          mark(false()) -> active(false())
          mark(div(X1,X2)) -> active(div(mark(X1),X2))
          mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
          minus(mark(X1),X2) -> minus(X1,X2)
          minus(X1,mark(X2)) -> minus(X1,X2)
          minus(active(X1),X2) -> minus(X1,X2)
          minus(X1,active(X2)) -> minus(X1,X2)
          s(mark(X)) -> s(X)
          s(active(X)) -> s(X)
          geq(mark(X1),X2) -> geq(X1,X2)
          geq(X1,mark(X2)) -> geq(X1,X2)
          geq(active(X1),X2) -> geq(X1,X2)
          geq(X1,active(X2)) -> geq(X1,X2)
          div(mark(X1),X2) -> div(X1,X2)
          div(X1,mark(X2)) -> div(X1,X2)
          div(active(X1),X2) -> div(X1,X2)
          div(X1,active(X2)) -> div(X1,X2)
          if(mark(X1),X2,X3) -> if(X1,X2,X3)
          if(X1,mark(X2),X3) -> if(X1,X2,X3)
          if(X1,X2,mark(X3)) -> if(X1,X2,X3)
          if(active(X1),X2,X3) -> if(X1,X2,X3)
          if(X1,active(X2),X3) -> if(X1,X2,X3)
          if(X1,X2,active(X3)) -> if(X1,X2,X3)
        Matrix Interpretation Processor:
         dimension: 1
         interpretation:
          [mark#](x0) = x0 + 1,
          
          [active#](x0) = 1,
          
          [if](x0, x1, x2) = 0,
          
          [div](x0, x1) = 1,
          
          [false] = 0,
          
          [true] = 0,
          
          [geq](x0, x1) = 0,
          
          [s](x0) = 0,
          
          [mark](x0) = 0,
          
          [active](x0) = 0,
          
          [minus](x0, x1) = 0,
          
          [0] = 0
         orientation:
          mark#(if(X1,X2,X3)) = 1 >= 1 = active#(if(mark(X1),X2,X3))
          
          mark#(div(X1,X2)) = 2 >= 1 = active#(div(mark(X1),X2))
          
          active#(div(s(X),s(Y))) = 1 >= 1 = mark#(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
          
          mark#(minus(X1,X2)) = 1 >= 1 = active#(minus(X1,X2))
          
          active#(minus(s(X),s(Y))) = 1 >= 1 = mark#(minus(X,Y))
          
          active(minus(0(),Y)) = 0 >= 0 = mark(0())
          
          active(minus(s(X),s(Y))) = 0 >= 0 = mark(minus(X,Y))
          
          active(geq(X,0())) = 0 >= 0 = mark(true())
          
          active(geq(0(),s(Y))) = 0 >= 0 = mark(false())
          
          active(geq(s(X),s(Y))) = 0 >= 0 = mark(geq(X,Y))
          
          active(div(0(),s(Y))) = 0 >= 0 = mark(0())
          
          active(div(s(X),s(Y))) = 0 >= 0 = mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
          
          active(if(true(),X,Y)) = 0 >= 0 = mark(X)
          
          active(if(false(),X,Y)) = 0 >= 0 = mark(Y)
          
          mark(minus(X1,X2)) = 0 >= 0 = active(minus(X1,X2))
          
          mark(0()) = 0 >= 0 = active(0())
          
          mark(s(X)) = 0 >= 0 = active(s(mark(X)))
          
          mark(geq(X1,X2)) = 0 >= 0 = active(geq(X1,X2))
          
          mark(true()) = 0 >= 0 = active(true())
          
          mark(false()) = 0 >= 0 = active(false())
          
          mark(div(X1,X2)) = 0 >= 0 = active(div(mark(X1),X2))
          
          mark(if(X1,X2,X3)) = 0 >= 0 = active(if(mark(X1),X2,X3))
          
          minus(mark(X1),X2) = 0 >= 0 = minus(X1,X2)
          
          minus(X1,mark(X2)) = 0 >= 0 = minus(X1,X2)
          
          minus(active(X1),X2) = 0 >= 0 = minus(X1,X2)
          
          minus(X1,active(X2)) = 0 >= 0 = minus(X1,X2)
          
          s(mark(X)) = 0 >= 0 = s(X)
          
          s(active(X)) = 0 >= 0 = s(X)
          
          geq(mark(X1),X2) = 0 >= 0 = geq(X1,X2)
          
          geq(X1,mark(X2)) = 0 >= 0 = geq(X1,X2)
          
          geq(active(X1),X2) = 0 >= 0 = geq(X1,X2)
          
          geq(X1,active(X2)) = 0 >= 0 = geq(X1,X2)
          
          div(mark(X1),X2) = 1 >= 1 = div(X1,X2)
          
          div(X1,mark(X2)) = 1 >= 1 = div(X1,X2)
          
          div(active(X1),X2) = 1 >= 1 = div(X1,X2)
          
          div(X1,active(X2)) = 1 >= 1 = div(X1,X2)
          
          if(mark(X1),X2,X3) = 0 >= 0 = if(X1,X2,X3)
          
          if(X1,mark(X2),X3) = 0 >= 0 = if(X1,X2,X3)
          
          if(X1,X2,mark(X3)) = 0 >= 0 = if(X1,X2,X3)
          
          if(active(X1),X2,X3) = 0 >= 0 = if(X1,X2,X3)
          
          if(X1,active(X2),X3) = 0 >= 0 = if(X1,X2,X3)
          
          if(X1,X2,active(X3)) = 0 >= 0 = if(X1,X2,X3)
         problem:
          DPs:
           mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
           active#(div(s(X),s(Y))) -> mark#(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
           mark#(minus(X1,X2)) -> active#(minus(X1,X2))
           active#(minus(s(X),s(Y))) -> mark#(minus(X,Y))
          TRS:
           active(minus(0(),Y)) -> mark(0())
           active(minus(s(X),s(Y))) -> mark(minus(X,Y))
           active(geq(X,0())) -> mark(true())
           active(geq(0(),s(Y))) -> mark(false())
           active(geq(s(X),s(Y))) -> mark(geq(X,Y))
           active(div(0(),s(Y))) -> mark(0())
           active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
           active(if(true(),X,Y)) -> mark(X)
           active(if(false(),X,Y)) -> mark(Y)
           mark(minus(X1,X2)) -> active(minus(X1,X2))
           mark(0()) -> active(0())
           mark(s(X)) -> active(s(mark(X)))
           mark(geq(X1,X2)) -> active(geq(X1,X2))
           mark(true()) -> active(true())
           mark(false()) -> active(false())
           mark(div(X1,X2)) -> active(div(mark(X1),X2))
           mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
           minus(mark(X1),X2) -> minus(X1,X2)
           minus(X1,mark(X2)) -> minus(X1,X2)
           minus(active(X1),X2) -> minus(X1,X2)
           minus(X1,active(X2)) -> minus(X1,X2)
           s(mark(X)) -> s(X)
           s(active(X)) -> s(X)
           geq(mark(X1),X2) -> geq(X1,X2)
           geq(X1,mark(X2)) -> geq(X1,X2)
           geq(active(X1),X2) -> geq(X1,X2)
           geq(X1,active(X2)) -> geq(X1,X2)
           div(mark(X1),X2) -> div(X1,X2)
           div(X1,mark(X2)) -> div(X1,X2)
           div(active(X1),X2) -> div(X1,X2)
           div(X1,active(X2)) -> div(X1,X2)
           if(mark(X1),X2,X3) -> if(X1,X2,X3)
           if(X1,mark(X2),X3) -> if(X1,X2,X3)
           if(X1,X2,mark(X3)) -> if(X1,X2,X3)
           if(active(X1),X2,X3) -> if(X1,X2,X3)
           if(X1,active(X2),X3) -> if(X1,X2,X3)
           if(X1,X2,active(X3)) -> if(X1,X2,X3)
         Matrix Interpretation Processor:
          dimension: 1
          interpretation:
           [mark#](x0) = 0,
           
           [active#](x0) = x0,
           
           [if](x0, x1, x2) = 0,
           
           [div](x0, x1) = 1,
           
           [false] = 0,
           
           [true] = 0,
           
           [geq](x0, x1) = 1,
           
           [s](x0) = 0,
           
           [mark](x0) = 0,
           
           [active](x0) = 0,
           
           [minus](x0, x1) = 0,
           
           [0] = 0
          orientation:
           mark#(if(X1,X2,X3)) = 0 >= 0 = active#(if(mark(X1),X2,X3))
           
           active#(div(s(X),s(Y))) = 1 >= 0 = mark#(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
           
           mark#(minus(X1,X2)) = 0 >= 0 = active#(minus(X1,X2))
           
           active#(minus(s(X),s(Y))) = 0 >= 0 = mark#(minus(X,Y))
           
           active(minus(0(),Y)) = 0 >= 0 = mark(0())
           
           active(minus(s(X),s(Y))) = 0 >= 0 = mark(minus(X,Y))
           
           active(geq(X,0())) = 0 >= 0 = mark(true())
           
           active(geq(0(),s(Y))) = 0 >= 0 = mark(false())
           
           active(geq(s(X),s(Y))) = 0 >= 0 = mark(geq(X,Y))
           
           active(div(0(),s(Y))) = 0 >= 0 = mark(0())
           
           active(div(s(X),s(Y))) = 0 >= 0 = mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
           
           active(if(true(),X,Y)) = 0 >= 0 = mark(X)
           
           active(if(false(),X,Y)) = 0 >= 0 = mark(Y)
           
           mark(minus(X1,X2)) = 0 >= 0 = active(minus(X1,X2))
           
           mark(0()) = 0 >= 0 = active(0())
           
           mark(s(X)) = 0 >= 0 = active(s(mark(X)))
           
           mark(geq(X1,X2)) = 0 >= 0 = active(geq(X1,X2))
           
           mark(true()) = 0 >= 0 = active(true())
           
           mark(false()) = 0 >= 0 = active(false())
           
           mark(div(X1,X2)) = 0 >= 0 = active(div(mark(X1),X2))
           
           mark(if(X1,X2,X3)) = 0 >= 0 = active(if(mark(X1),X2,X3))
           
           minus(mark(X1),X2) = 0 >= 0 = minus(X1,X2)
           
           minus(X1,mark(X2)) = 0 >= 0 = minus(X1,X2)
           
           minus(active(X1),X2) = 0 >= 0 = minus(X1,X2)
           
           minus(X1,active(X2)) = 0 >= 0 = minus(X1,X2)
           
           s(mark(X)) = 0 >= 0 = s(X)
           
           s(active(X)) = 0 >= 0 = s(X)
           
           geq(mark(X1),X2) = 1 >= 1 = geq(X1,X2)
           
           geq(X1,mark(X2)) = 1 >= 1 = geq(X1,X2)
           
           geq(active(X1),X2) = 1 >= 1 = geq(X1,X2)
           
           geq(X1,active(X2)) = 1 >= 1 = geq(X1,X2)
           
           div(mark(X1),X2) = 1 >= 1 = div(X1,X2)
           
           div(X1,mark(X2)) = 1 >= 1 = div(X1,X2)
           
           div(active(X1),X2) = 1 >= 1 = div(X1,X2)
           
           div(X1,active(X2)) = 1 >= 1 = div(X1,X2)
           
           if(mark(X1),X2,X3) = 0 >= 0 = if(X1,X2,X3)
           
           if(X1,mark(X2),X3) = 0 >= 0 = if(X1,X2,X3)
           
           if(X1,X2,mark(X3)) = 0 >= 0 = if(X1,X2,X3)
           
           if(active(X1),X2,X3) = 0 >= 0 = if(X1,X2,X3)
           
           if(X1,active(X2),X3) = 0 >= 0 = if(X1,X2,X3)
           
           if(X1,X2,active(X3)) = 0 >= 0 = if(X1,X2,X3)
          problem:
           DPs:
            mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
            mark#(minus(X1,X2)) -> active#(minus(X1,X2))
            active#(minus(s(X),s(Y))) -> mark#(minus(X,Y))
           TRS:
            active(minus(0(),Y)) -> mark(0())
            active(minus(s(X),s(Y))) -> mark(minus(X,Y))
            active(geq(X,0())) -> mark(true())
            active(geq(0(),s(Y))) -> mark(false())
            active(geq(s(X),s(Y))) -> mark(geq(X,Y))
            active(div(0(),s(Y))) -> mark(0())
            active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
            active(if(true(),X,Y)) -> mark(X)
            active(if(false(),X,Y)) -> mark(Y)
            mark(minus(X1,X2)) -> active(minus(X1,X2))
            mark(0()) -> active(0())
            mark(s(X)) -> active(s(mark(X)))
            mark(geq(X1,X2)) -> active(geq(X1,X2))
            mark(true()) -> active(true())
            mark(false()) -> active(false())
            mark(div(X1,X2)) -> active(div(mark(X1),X2))
            mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
            minus(mark(X1),X2) -> minus(X1,X2)
            minus(X1,mark(X2)) -> minus(X1,X2)
            minus(active(X1),X2) -> minus(X1,X2)
            minus(X1,active(X2)) -> minus(X1,X2)
            s(mark(X)) -> s(X)
            s(active(X)) -> s(X)
            geq(mark(X1),X2) -> geq(X1,X2)
            geq(X1,mark(X2)) -> geq(X1,X2)
            geq(active(X1),X2) -> geq(X1,X2)
            geq(X1,active(X2)) -> geq(X1,X2)
            div(mark(X1),X2) -> div(X1,X2)
            div(X1,mark(X2)) -> div(X1,X2)
            div(active(X1),X2) -> div(X1,X2)
            div(X1,active(X2)) -> div(X1,X2)
            if(mark(X1),X2,X3) -> if(X1,X2,X3)
            if(X1,mark(X2),X3) -> if(X1,X2,X3)
            if(X1,X2,mark(X3)) -> if(X1,X2,X3)
            if(active(X1),X2,X3) -> if(X1,X2,X3)
            if(X1,active(X2),X3) -> if(X1,X2,X3)
            if(X1,X2,active(X3)) -> if(X1,X2,X3)
          Matrix Interpretation Processor:
           dimension: 1
           interpretation:
            [mark#](x0) = x0 + 1,
            
            [active#](x0) = 1,
            
            [if](x0, x1, x2) = 1,
            
            [div](x0, x1) = 1,
            
            [false] = 0,
            
            [true] = 0,
            
            [geq](x0, x1) = 0,
            
            [s](x0) = 0,
            
            [mark](x0) = 0,
            
            [active](x0) = 0,
            
            [minus](x0, x1) = 0,
            
            [0] = 0
           orientation:
            mark#(if(X1,X2,X3)) = 2 >= 1 = active#(if(mark(X1),X2,X3))
            
            mark#(minus(X1,X2)) = 1 >= 1 = active#(minus(X1,X2))
            
            active#(minus(s(X),s(Y))) = 1 >= 1 = mark#(minus(X,Y))
            
            active(minus(0(),Y)) = 0 >= 0 = mark(0())
            
            active(minus(s(X),s(Y))) = 0 >= 0 = mark(minus(X,Y))
            
            active(geq(X,0())) = 0 >= 0 = mark(true())
            
            active(geq(0(),s(Y))) = 0 >= 0 = mark(false())
            
            active(geq(s(X),s(Y))) = 0 >= 0 = mark(geq(X,Y))
            
            active(div(0(),s(Y))) = 0 >= 0 = mark(0())
            
            active(div(s(X),s(Y))) = 0 >= 0 = mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
            
            active(if(true(),X,Y)) = 0 >= 0 = mark(X)
            
            active(if(false(),X,Y)) = 0 >= 0 = mark(Y)
            
            mark(minus(X1,X2)) = 0 >= 0 = active(minus(X1,X2))
            
            mark(0()) = 0 >= 0 = active(0())
            
            mark(s(X)) = 0 >= 0 = active(s(mark(X)))
            
            mark(geq(X1,X2)) = 0 >= 0 = active(geq(X1,X2))
            
            mark(true()) = 0 >= 0 = active(true())
            
            mark(false()) = 0 >= 0 = active(false())
            
            mark(div(X1,X2)) = 0 >= 0 = active(div(mark(X1),X2))
            
            mark(if(X1,X2,X3)) = 0 >= 0 = active(if(mark(X1),X2,X3))
            
            minus(mark(X1),X2) = 0 >= 0 = minus(X1,X2)
            
            minus(X1,mark(X2)) = 0 >= 0 = minus(X1,X2)
            
            minus(active(X1),X2) = 0 >= 0 = minus(X1,X2)
            
            minus(X1,active(X2)) = 0 >= 0 = minus(X1,X2)
            
            s(mark(X)) = 0 >= 0 = s(X)
            
            s(active(X)) = 0 >= 0 = s(X)
            
            geq(mark(X1),X2) = 0 >= 0 = geq(X1,X2)
            
            geq(X1,mark(X2)) = 0 >= 0 = geq(X1,X2)
            
            geq(active(X1),X2) = 0 >= 0 = geq(X1,X2)
            
            geq(X1,active(X2)) = 0 >= 0 = geq(X1,X2)
            
            div(mark(X1),X2) = 1 >= 1 = div(X1,X2)
            
            div(X1,mark(X2)) = 1 >= 1 = div(X1,X2)
            
            div(active(X1),X2) = 1 >= 1 = div(X1,X2)
            
            div(X1,active(X2)) = 1 >= 1 = div(X1,X2)
            
            if(mark(X1),X2,X3) = 1 >= 1 = if(X1,X2,X3)
            
            if(X1,mark(X2),X3) = 1 >= 1 = if(X1,X2,X3)
            
            if(X1,X2,mark(X3)) = 1 >= 1 = if(X1,X2,X3)
            
            if(active(X1),X2,X3) = 1 >= 1 = if(X1,X2,X3)
            
            if(X1,active(X2),X3) = 1 >= 1 = if(X1,X2,X3)
            
            if(X1,X2,active(X3)) = 1 >= 1 = if(X1,X2,X3)
           problem:
            DPs:
             mark#(minus(X1,X2)) -> active#(minus(X1,X2))
             active#(minus(s(X),s(Y))) -> mark#(minus(X,Y))
            TRS:
             active(minus(0(),Y)) -> mark(0())
             active(minus(s(X),s(Y))) -> mark(minus(X,Y))
             active(geq(X,0())) -> mark(true())
             active(geq(0(),s(Y))) -> mark(false())
             active(geq(s(X),s(Y))) -> mark(geq(X,Y))
             active(div(0(),s(Y))) -> mark(0())
             active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
             active(if(true(),X,Y)) -> mark(X)
             active(if(false(),X,Y)) -> mark(Y)
             mark(minus(X1,X2)) -> active(minus(X1,X2))
             mark(0()) -> active(0())
             mark(s(X)) -> active(s(mark(X)))
             mark(geq(X1,X2)) -> active(geq(X1,X2))
             mark(true()) -> active(true())
             mark(false()) -> active(false())
             mark(div(X1,X2)) -> active(div(mark(X1),X2))
             mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
             minus(mark(X1),X2) -> minus(X1,X2)
             minus(X1,mark(X2)) -> minus(X1,X2)
             minus(active(X1),X2) -> minus(X1,X2)
             minus(X1,active(X2)) -> minus(X1,X2)
             s(mark(X)) -> s(X)
             s(active(X)) -> s(X)
             geq(mark(X1),X2) -> geq(X1,X2)
             geq(X1,mark(X2)) -> geq(X1,X2)
             geq(active(X1),X2) -> geq(X1,X2)
             geq(X1,active(X2)) -> geq(X1,X2)
             div(mark(X1),X2) -> div(X1,X2)
             div(X1,mark(X2)) -> div(X1,X2)
             div(active(X1),X2) -> div(X1,X2)
             div(X1,active(X2)) -> div(X1,X2)
             if(mark(X1),X2,X3) -> if(X1,X2,X3)
             if(X1,mark(X2),X3) -> if(X1,X2,X3)
             if(X1,X2,mark(X3)) -> if(X1,X2,X3)
             if(active(X1),X2,X3) -> if(X1,X2,X3)
             if(X1,active(X2),X3) -> if(X1,X2,X3)
             if(X1,X2,active(X3)) -> if(X1,X2,X3)
           Matrix Interpretation Processor:
            dimension: 1
            interpretation:
             [mark#](x0) = x0 + 1,
             
             [active#](x0) = x0,
             
             [if](x0, x1, x2) = x1 + x2,
             
             [div](x0, x1) = x0,
             
             [false] = 0,
             
             [true] = 0,
             
             [geq](x0, x1) = x1,
             
             [s](x0) = x0 + 1,
             
             [mark](x0) = x0,
             
             [active](x0) = x0,
             
             [minus](x0, x1) = x0,
             
             [0] = 0
            orientation:
             mark#(minus(X1,X2)) = X1 + 1 >= X1 = active#(minus(X1,X2))
             
             active#(minus(s(X),s(Y))) = X + 1 >= X + 1 = mark#(minus(X,Y))
             
             active(minus(0(),Y)) = 0 >= 0 = mark(0())
             
             active(minus(s(X),s(Y))) = X + 1 >= X = mark(minus(X,Y))
             
             active(geq(X,0())) = 0 >= 0 = mark(true())
             
             active(geq(0(),s(Y))) = Y + 1 >= 0 = mark(false())
             
             active(geq(s(X),s(Y))) = Y + 1 >= Y = mark(geq(X,Y))
             
             active(div(0(),s(Y))) = 0 >= 0 = mark(0())
             
             active(div(s(X),s(Y))) = X + 1 >= X + 1 = mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
             
             active(if(true(),X,Y)) = X + Y >= X = mark(X)
             
             active(if(false(),X,Y)) = X + Y >= Y = mark(Y)
             
             mark(minus(X1,X2)) = X1 >= X1 = active(minus(X1,X2))
             
             mark(0()) = 0 >= 0 = active(0())
             
             mark(s(X)) = X + 1 >= X + 1 = active(s(mark(X)))
             
             mark(geq(X1,X2)) = X2 >= X2 = active(geq(X1,X2))
             
             mark(true()) = 0 >= 0 = active(true())
             
             mark(false()) = 0 >= 0 = active(false())
             
             mark(div(X1,X2)) = X1 >= X1 = active(div(mark(X1),X2))
             
             mark(if(X1,X2,X3)) = X2 + X3 >= X2 + X3 = active(if(mark(X1),X2,X3))
             
             minus(mark(X1),X2) = X1 >= X1 = minus(X1,X2)
             
             minus(X1,mark(X2)) = X1 >= X1 = minus(X1,X2)
             
             minus(active(X1),X2) = X1 >= X1 = minus(X1,X2)
             
             minus(X1,active(X2)) = X1 >= X1 = minus(X1,X2)
             
             s(mark(X)) = X + 1 >= X + 1 = s(X)
             
             s(active(X)) = X + 1 >= X + 1 = s(X)
             
             geq(mark(X1),X2) = X2 >= X2 = geq(X1,X2)
             
             geq(X1,mark(X2)) = X2 >= X2 = geq(X1,X2)
             
             geq(active(X1),X2) = X2 >= X2 = geq(X1,X2)
             
             geq(X1,active(X2)) = X2 >= X2 = geq(X1,X2)
             
             div(mark(X1),X2) = X1 >= X1 = div(X1,X2)
             
             div(X1,mark(X2)) = X1 >= X1 = div(X1,X2)
             
             div(active(X1),X2) = X1 >= X1 = div(X1,X2)
             
             div(X1,active(X2)) = X1 >= X1 = div(X1,X2)
             
             if(mark(X1),X2,X3) = X2 + X3 >= X2 + X3 = if(X1,X2,X3)
             
             if(X1,mark(X2),X3) = X2 + X3 >= X2 + X3 = if(X1,X2,X3)
             
             if(X1,X2,mark(X3)) = X2 + X3 >= X2 + X3 = if(X1,X2,X3)
             
             if(active(X1),X2,X3) = X2 + X3 >= X2 + X3 = if(X1,X2,X3)
             
             if(X1,active(X2),X3) = X2 + X3 >= X2 + X3 = if(X1,X2,X3)
             
             if(X1,X2,active(X3)) = X2 + X3 >= X2 + X3 = if(X1,X2,X3)
            problem:
             DPs:
              active#(minus(s(X),s(Y))) -> mark#(minus(X,Y))
             TRS:
              active(minus(0(),Y)) -> mark(0())
              active(minus(s(X),s(Y))) -> mark(minus(X,Y))
              active(geq(X,0())) -> mark(true())
              active(geq(0(),s(Y))) -> mark(false())
              active(geq(s(X),s(Y))) -> mark(geq(X,Y))
              active(div(0(),s(Y))) -> mark(0())
              active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
              active(if(true(),X,Y)) -> mark(X)
              active(if(false(),X,Y)) -> mark(Y)
              mark(minus(X1,X2)) -> active(minus(X1,X2))
              mark(0()) -> active(0())
              mark(s(X)) -> active(s(mark(X)))
              mark(geq(X1,X2)) -> active(geq(X1,X2))
              mark(true()) -> active(true())
              mark(false()) -> active(false())
              mark(div(X1,X2)) -> active(div(mark(X1),X2))
              mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
              minus(mark(X1),X2) -> minus(X1,X2)
              minus(X1,mark(X2)) -> minus(X1,X2)
              minus(active(X1),X2) -> minus(X1,X2)
              minus(X1,active(X2)) -> minus(X1,X2)
              s(mark(X)) -> s(X)
              s(active(X)) -> s(X)
              geq(mark(X1),X2) -> geq(X1,X2)
              geq(X1,mark(X2)) -> geq(X1,X2)
              geq(active(X1),X2) -> geq(X1,X2)
              geq(X1,active(X2)) -> geq(X1,X2)
              div(mark(X1),X2) -> div(X1,X2)
              div(X1,mark(X2)) -> div(X1,X2)
              div(active(X1),X2) -> div(X1,X2)
              div(X1,active(X2)) -> div(X1,X2)
              if(mark(X1),X2,X3) -> if(X1,X2,X3)
              if(X1,mark(X2),X3) -> if(X1,X2,X3)
              if(X1,X2,mark(X3)) -> if(X1,X2,X3)
              if(active(X1),X2,X3) -> if(X1,X2,X3)
              if(X1,active(X2),X3) -> if(X1,X2,X3)
              if(X1,X2,active(X3)) -> if(X1,X2,X3)
            Matrix Interpretation Processor:
             dimension: 1
             interpretation:
              [mark#](x0) = 0,
              
              [active#](x0) = x0,
              
              [if](x0, x1, x2) = 0,
              
              [div](x0, x1) = 0,
              
              [false] = 0,
              
              [true] = 0,
              
              [geq](x0, x1) = 1,
              
              [s](x0) = 0,
              
              [mark](x0) = 0,
              
              [active](x0) = 0,
              
              [minus](x0, x1) = 1,
              
              [0] = 0
             orientation:
              active#(minus(s(X),s(Y))) = 1 >= 0 = mark#(minus(X,Y))
              
              active(minus(0(),Y)) = 0 >= 0 = mark(0())
              
              active(minus(s(X),s(Y))) = 0 >= 0 = mark(minus(X,Y))
              
              active(geq(X,0())) = 0 >= 0 = mark(true())
              
              active(geq(0(),s(Y))) = 0 >= 0 = mark(false())
              
              active(geq(s(X),s(Y))) = 0 >= 0 = mark(geq(X,Y))
              
              active(div(0(),s(Y))) = 0 >= 0 = mark(0())
              
              active(div(s(X),s(Y))) = 0 >= 0 = mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
              
              active(if(true(),X,Y)) = 0 >= 0 = mark(X)
              
              active(if(false(),X,Y)) = 0 >= 0 = mark(Y)
              
              mark(minus(X1,X2)) = 0 >= 0 = active(minus(X1,X2))
              
              mark(0()) = 0 >= 0 = active(0())
              
              mark(s(X)) = 0 >= 0 = active(s(mark(X)))
              
              mark(geq(X1,X2)) = 0 >= 0 = active(geq(X1,X2))
              
              mark(true()) = 0 >= 0 = active(true())
              
              mark(false()) = 0 >= 0 = active(false())
              
              mark(div(X1,X2)) = 0 >= 0 = active(div(mark(X1),X2))
              
              mark(if(X1,X2,X3)) = 0 >= 0 = active(if(mark(X1),X2,X3))
              
              minus(mark(X1),X2) = 1 >= 1 = minus(X1,X2)
              
              minus(X1,mark(X2)) = 1 >= 1 = minus(X1,X2)
              
              minus(active(X1),X2) = 1 >= 1 = minus(X1,X2)
              
              minus(X1,active(X2)) = 1 >= 1 = minus(X1,X2)
              
              s(mark(X)) = 0 >= 0 = s(X)
              
              s(active(X)) = 0 >= 0 = s(X)
              
              geq(mark(X1),X2) = 1 >= 1 = geq(X1,X2)
              
              geq(X1,mark(X2)) = 1 >= 1 = geq(X1,X2)
              
              geq(active(X1),X2) = 1 >= 1 = geq(X1,X2)
              
              geq(X1,active(X2)) = 1 >= 1 = geq(X1,X2)
              
              div(mark(X1),X2) = 0 >= 0 = div(X1,X2)
              
              div(X1,mark(X2)) = 0 >= 0 = div(X1,X2)
              
              div(active(X1),X2) = 0 >= 0 = div(X1,X2)
              
              div(X1,active(X2)) = 0 >= 0 = div(X1,X2)
              
              if(mark(X1),X2,X3) = 0 >= 0 = if(X1,X2,X3)
              
              if(X1,mark(X2),X3) = 0 >= 0 = if(X1,X2,X3)
              
              if(X1,X2,mark(X3)) = 0 >= 0 = if(X1,X2,X3)
              
              if(active(X1),X2,X3) = 0 >= 0 = if(X1,X2,X3)
              
              if(X1,active(X2),X3) = 0 >= 0 = if(X1,X2,X3)
              
              if(X1,X2,active(X3)) = 0 >= 0 = if(X1,X2,X3)
             problem:
              DPs:
               
              TRS:
               active(minus(0(),Y)) -> mark(0())
               active(minus(s(X),s(Y))) -> mark(minus(X,Y))
               active(geq(X,0())) -> mark(true())
               active(geq(0(),s(Y))) -> mark(false())
               active(geq(s(X),s(Y))) -> mark(geq(X,Y))
               active(div(0(),s(Y))) -> mark(0())
               active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
               active(if(true(),X,Y)) -> mark(X)
               active(if(false(),X,Y)) -> mark(Y)
               mark(minus(X1,X2)) -> active(minus(X1,X2))
               mark(0()) -> active(0())
               mark(s(X)) -> active(s(mark(X)))
               mark(geq(X1,X2)) -> active(geq(X1,X2))
               mark(true()) -> active(true())
               mark(false()) -> active(false())
               mark(div(X1,X2)) -> active(div(mark(X1),X2))
               mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
               minus(mark(X1),X2) -> minus(X1,X2)
               minus(X1,mark(X2)) -> minus(X1,X2)
               minus(active(X1),X2) -> minus(X1,X2)
               minus(X1,active(X2)) -> minus(X1,X2)
               s(mark(X)) -> s(X)
               s(active(X)) -> s(X)
               geq(mark(X1),X2) -> geq(X1,X2)
               geq(X1,mark(X2)) -> geq(X1,X2)
               geq(active(X1),X2) -> geq(X1,X2)
               geq(X1,active(X2)) -> geq(X1,X2)
               div(mark(X1),X2) -> div(X1,X2)
               div(X1,mark(X2)) -> div(X1,X2)
               div(active(X1),X2) -> div(X1,X2)
               div(X1,active(X2)) -> div(X1,X2)
               if(mark(X1),X2,X3) -> if(X1,X2,X3)
               if(X1,mark(X2),X3) -> if(X1,X2,X3)
               if(X1,X2,mark(X3)) -> if(X1,X2,X3)
               if(active(X1),X2,X3) -> if(X1,X2,X3)
               if(X1,active(X2),X3) -> if(X1,X2,X3)
               if(X1,X2,active(X3)) -> if(X1,X2,X3)
             Qed
    
    DPs:
     minus#(mark(X1),X2) -> minus#(X1,X2)
     minus#(X1,active(X2)) -> minus#(X1,X2)
     minus#(active(X1),X2) -> minus#(X1,X2)
     minus#(X1,mark(X2)) -> minus#(X1,X2)
    TRS:
     active(minus(0(),Y)) -> mark(0())
     active(minus(s(X),s(Y))) -> mark(minus(X,Y))
     active(geq(X,0())) -> mark(true())
     active(geq(0(),s(Y))) -> mark(false())
     active(geq(s(X),s(Y))) -> mark(geq(X,Y))
     active(div(0(),s(Y))) -> mark(0())
     active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
     active(if(true(),X,Y)) -> mark(X)
     active(if(false(),X,Y)) -> mark(Y)
     mark(minus(X1,X2)) -> active(minus(X1,X2))
     mark(0()) -> active(0())
     mark(s(X)) -> active(s(mark(X)))
     mark(geq(X1,X2)) -> active(geq(X1,X2))
     mark(true()) -> active(true())
     mark(false()) -> active(false())
     mark(div(X1,X2)) -> active(div(mark(X1),X2))
     mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
     minus(mark(X1),X2) -> minus(X1,X2)
     minus(X1,mark(X2)) -> minus(X1,X2)
     minus(active(X1),X2) -> minus(X1,X2)
     minus(X1,active(X2)) -> minus(X1,X2)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     geq(mark(X1),X2) -> geq(X1,X2)
     geq(X1,mark(X2)) -> geq(X1,X2)
     geq(active(X1),X2) -> geq(X1,X2)
     geq(X1,active(X2)) -> geq(X1,X2)
     div(mark(X1),X2) -> div(X1,X2)
     div(X1,mark(X2)) -> div(X1,X2)
     div(active(X1),X2) -> div(X1,X2)
     div(X1,active(X2)) -> div(X1,X2)
     if(mark(X1),X2,X3) -> if(X1,X2,X3)
     if(X1,mark(X2),X3) -> if(X1,X2,X3)
     if(X1,X2,mark(X3)) -> if(X1,X2,X3)
     if(active(X1),X2,X3) -> if(X1,X2,X3)
     if(X1,active(X2),X3) -> if(X1,X2,X3)
     if(X1,X2,active(X3)) -> if(X1,X2,X3)
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [minus#](x0, x1) = x1,
      
      [if](x0, x1, x2) = x1 + x2,
      
      [div](x0, x1) = 0,
      
      [false] = 0,
      
      [true] = 0,
      
      [geq](x0, x1) = 0,
      
      [s](x0) = 0,
      
      [mark](x0) = x0 + 1,
      
      [active](x0) = x0 + 1,
      
      [minus](x0, x1) = 0,
      
      [0] = 0
     orientation:
      minus#(mark(X1),X2) = X2 >= X2 = minus#(X1,X2)
      
      minus#(X1,active(X2)) = X2 + 1 >= X2 = minus#(X1,X2)
      
      minus#(active(X1),X2) = X2 >= X2 = minus#(X1,X2)
      
      minus#(X1,mark(X2)) = X2 + 1 >= X2 = minus#(X1,X2)
      
      active(minus(0(),Y)) = 1 >= 1 = mark(0())
      
      active(minus(s(X),s(Y))) = 1 >= 1 = mark(minus(X,Y))
      
      active(geq(X,0())) = 1 >= 1 = mark(true())
      
      active(geq(0(),s(Y))) = 1 >= 1 = mark(false())
      
      active(geq(s(X),s(Y))) = 1 >= 1 = mark(geq(X,Y))
      
      active(div(0(),s(Y))) = 1 >= 1 = mark(0())
      
      active(div(s(X),s(Y))) = 1 >= 1 = mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
      
      active(if(true(),X,Y)) = X + Y + 1 >= X + 1 = mark(X)
      
      active(if(false(),X,Y)) = X + Y + 1 >= Y + 1 = mark(Y)
      
      mark(minus(X1,X2)) = 1 >= 1 = active(minus(X1,X2))
      
      mark(0()) = 1 >= 1 = active(0())
      
      mark(s(X)) = 1 >= 1 = active(s(mark(X)))
      
      mark(geq(X1,X2)) = 1 >= 1 = active(geq(X1,X2))
      
      mark(true()) = 1 >= 1 = active(true())
      
      mark(false()) = 1 >= 1 = active(false())
      
      mark(div(X1,X2)) = 1 >= 1 = active(div(mark(X1),X2))
      
      mark(if(X1,X2,X3)) = X2 + X3 + 1 >= X2 + X3 + 1 = active(if(mark(X1),X2,X3))
      
      minus(mark(X1),X2) = 0 >= 0 = minus(X1,X2)
      
      minus(X1,mark(X2)) = 0 >= 0 = minus(X1,X2)
      
      minus(active(X1),X2) = 0 >= 0 = minus(X1,X2)
      
      minus(X1,active(X2)) = 0 >= 0 = minus(X1,X2)
      
      s(mark(X)) = 0 >= 0 = s(X)
      
      s(active(X)) = 0 >= 0 = s(X)
      
      geq(mark(X1),X2) = 0 >= 0 = geq(X1,X2)
      
      geq(X1,mark(X2)) = 0 >= 0 = geq(X1,X2)
      
      geq(active(X1),X2) = 0 >= 0 = geq(X1,X2)
      
      geq(X1,active(X2)) = 0 >= 0 = geq(X1,X2)
      
      div(mark(X1),X2) = 0 >= 0 = div(X1,X2)
      
      div(X1,mark(X2)) = 0 >= 0 = div(X1,X2)
      
      div(active(X1),X2) = 0 >= 0 = div(X1,X2)
      
      div(X1,active(X2)) = 0 >= 0 = div(X1,X2)
      
      if(mark(X1),X2,X3) = X2 + X3 >= X2 + X3 = if(X1,X2,X3)
      
      if(X1,mark(X2),X3) = X2 + X3 + 1 >= X2 + X3 = if(X1,X2,X3)
      
      if(X1,X2,mark(X3)) = X2 + X3 + 1 >= X2 + X3 = if(X1,X2,X3)
      
      if(active(X1),X2,X3) = X2 + X3 >= X2 + X3 = if(X1,X2,X3)
      
      if(X1,active(X2),X3) = X2 + X3 + 1 >= X2 + X3 = if(X1,X2,X3)
      
      if(X1,X2,active(X3)) = X2 + X3 + 1 >= X2 + X3 = if(X1,X2,X3)
     problem:
      DPs:
       minus#(mark(X1),X2) -> minus#(X1,X2)
       minus#(active(X1),X2) -> minus#(X1,X2)
      TRS:
       active(minus(0(),Y)) -> mark(0())
       active(minus(s(X),s(Y))) -> mark(minus(X,Y))
       active(geq(X,0())) -> mark(true())
       active(geq(0(),s(Y))) -> mark(false())
       active(geq(s(X),s(Y))) -> mark(geq(X,Y))
       active(div(0(),s(Y))) -> mark(0())
       active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
       active(if(true(),X,Y)) -> mark(X)
       active(if(false(),X,Y)) -> mark(Y)
       mark(minus(X1,X2)) -> active(minus(X1,X2))
       mark(0()) -> active(0())
       mark(s(X)) -> active(s(mark(X)))
       mark(geq(X1,X2)) -> active(geq(X1,X2))
       mark(true()) -> active(true())
       mark(false()) -> active(false())
       mark(div(X1,X2)) -> active(div(mark(X1),X2))
       mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
       minus(mark(X1),X2) -> minus(X1,X2)
       minus(X1,mark(X2)) -> minus(X1,X2)
       minus(active(X1),X2) -> minus(X1,X2)
       minus(X1,active(X2)) -> minus(X1,X2)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(X)
       geq(mark(X1),X2) -> geq(X1,X2)
       geq(X1,mark(X2)) -> geq(X1,X2)
       geq(active(X1),X2) -> geq(X1,X2)
       geq(X1,active(X2)) -> geq(X1,X2)
       div(mark(X1),X2) -> div(X1,X2)
       div(X1,mark(X2)) -> div(X1,X2)
       div(active(X1),X2) -> div(X1,X2)
       div(X1,active(X2)) -> div(X1,X2)
       if(mark(X1),X2,X3) -> if(X1,X2,X3)
       if(X1,mark(X2),X3) -> if(X1,X2,X3)
       if(X1,X2,mark(X3)) -> if(X1,X2,X3)
       if(active(X1),X2,X3) -> if(X1,X2,X3)
       if(X1,active(X2),X3) -> if(X1,X2,X3)
       if(X1,X2,active(X3)) -> if(X1,X2,X3)
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [minus#](x0, x1) = x0 + 1,
       
       [if](x0, x1, x2) = x1 + x2,
       
       [div](x0, x1) = 0,
       
       [false] = 0,
       
       [true] = 0,
       
       [geq](x0, x1) = 0,
       
       [s](x0) = 0,
       
       [mark](x0) = x0 + 1,
       
       [active](x0) = x0 + 1,
       
       [minus](x0, x1) = 0,
       
       [0] = 0
      orientation:
       minus#(mark(X1),X2) = X1 + 2 >= X1 + 1 = minus#(X1,X2)
       
       minus#(active(X1),X2) = X1 + 2 >= X1 + 1 = minus#(X1,X2)
       
       active(minus(0(),Y)) = 1 >= 1 = mark(0())
       
       active(minus(s(X),s(Y))) = 1 >= 1 = mark(minus(X,Y))
       
       active(geq(X,0())) = 1 >= 1 = mark(true())
       
       active(geq(0(),s(Y))) = 1 >= 1 = mark(false())
       
       active(geq(s(X),s(Y))) = 1 >= 1 = mark(geq(X,Y))
       
       active(div(0(),s(Y))) = 1 >= 1 = mark(0())
       
       active(div(s(X),s(Y))) = 1 >= 1 = mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
       
       active(if(true(),X,Y)) = X + Y + 1 >= X + 1 = mark(X)
       
       active(if(false(),X,Y)) = X + Y + 1 >= Y + 1 = mark(Y)
       
       mark(minus(X1,X2)) = 1 >= 1 = active(minus(X1,X2))
       
       mark(0()) = 1 >= 1 = active(0())
       
       mark(s(X)) = 1 >= 1 = active(s(mark(X)))
       
       mark(geq(X1,X2)) = 1 >= 1 = active(geq(X1,X2))
       
       mark(true()) = 1 >= 1 = active(true())
       
       mark(false()) = 1 >= 1 = active(false())
       
       mark(div(X1,X2)) = 1 >= 1 = active(div(mark(X1),X2))
       
       mark(if(X1,X2,X3)) = X2 + X3 + 1 >= X2 + X3 + 1 = active(if(mark(X1),X2,X3))
       
       minus(mark(X1),X2) = 0 >= 0 = minus(X1,X2)
       
       minus(X1,mark(X2)) = 0 >= 0 = minus(X1,X2)
       
       minus(active(X1),X2) = 0 >= 0 = minus(X1,X2)
       
       minus(X1,active(X2)) = 0 >= 0 = minus(X1,X2)
       
       s(mark(X)) = 0 >= 0 = s(X)
       
       s(active(X)) = 0 >= 0 = s(X)
       
       geq(mark(X1),X2) = 0 >= 0 = geq(X1,X2)
       
       geq(X1,mark(X2)) = 0 >= 0 = geq(X1,X2)
       
       geq(active(X1),X2) = 0 >= 0 = geq(X1,X2)
       
       geq(X1,active(X2)) = 0 >= 0 = geq(X1,X2)
       
       div(mark(X1),X2) = 0 >= 0 = div(X1,X2)
       
       div(X1,mark(X2)) = 0 >= 0 = div(X1,X2)
       
       div(active(X1),X2) = 0 >= 0 = div(X1,X2)
       
       div(X1,active(X2)) = 0 >= 0 = div(X1,X2)
       
       if(mark(X1),X2,X3) = X2 + X3 >= X2 + X3 = if(X1,X2,X3)
       
       if(X1,mark(X2),X3) = X2 + X3 + 1 >= X2 + X3 = if(X1,X2,X3)
       
       if(X1,X2,mark(X3)) = X2 + X3 + 1 >= X2 + X3 = if(X1,X2,X3)
       
       if(active(X1),X2,X3) = X2 + X3 >= X2 + X3 = if(X1,X2,X3)
       
       if(X1,active(X2),X3) = X2 + X3 + 1 >= X2 + X3 = if(X1,X2,X3)
       
       if(X1,X2,active(X3)) = X2 + X3 + 1 >= X2 + X3 = if(X1,X2,X3)
      problem:
       DPs:
        
       TRS:
        active(minus(0(),Y)) -> mark(0())
        active(minus(s(X),s(Y))) -> mark(minus(X,Y))
        active(geq(X,0())) -> mark(true())
        active(geq(0(),s(Y))) -> mark(false())
        active(geq(s(X),s(Y))) -> mark(geq(X,Y))
        active(div(0(),s(Y))) -> mark(0())
        active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
        active(if(true(),X,Y)) -> mark(X)
        active(if(false(),X,Y)) -> mark(Y)
        mark(minus(X1,X2)) -> active(minus(X1,X2))
        mark(0()) -> active(0())
        mark(s(X)) -> active(s(mark(X)))
        mark(geq(X1,X2)) -> active(geq(X1,X2))
        mark(true()) -> active(true())
        mark(false()) -> active(false())
        mark(div(X1,X2)) -> active(div(mark(X1),X2))
        mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
        minus(mark(X1),X2) -> minus(X1,X2)
        minus(X1,mark(X2)) -> minus(X1,X2)
        minus(active(X1),X2) -> minus(X1,X2)
        minus(X1,active(X2)) -> minus(X1,X2)
        s(mark(X)) -> s(X)
        s(active(X)) -> s(X)
        geq(mark(X1),X2) -> geq(X1,X2)
        geq(X1,mark(X2)) -> geq(X1,X2)
        geq(active(X1),X2) -> geq(X1,X2)
        geq(X1,active(X2)) -> geq(X1,X2)
        div(mark(X1),X2) -> div(X1,X2)
        div(X1,mark(X2)) -> div(X1,X2)
        div(active(X1),X2) -> div(X1,X2)
        div(X1,active(X2)) -> div(X1,X2)
        if(mark(X1),X2,X3) -> if(X1,X2,X3)
        if(X1,mark(X2),X3) -> if(X1,X2,X3)
        if(X1,X2,mark(X3)) -> if(X1,X2,X3)
        if(active(X1),X2,X3) -> if(X1,X2,X3)
        if(X1,active(X2),X3) -> if(X1,X2,X3)
        if(X1,X2,active(X3)) -> if(X1,X2,X3)
      Qed
    
    DPs:
     geq#(mark(X1),X2) -> geq#(X1,X2)
     geq#(X1,active(X2)) -> geq#(X1,X2)
     geq#(active(X1),X2) -> geq#(X1,X2)
     geq#(X1,mark(X2)) -> geq#(X1,X2)
    TRS:
     active(minus(0(),Y)) -> mark(0())
     active(minus(s(X),s(Y))) -> mark(minus(X,Y))
     active(geq(X,0())) -> mark(true())
     active(geq(0(),s(Y))) -> mark(false())
     active(geq(s(X),s(Y))) -> mark(geq(X,Y))
     active(div(0(),s(Y))) -> mark(0())
     active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
     active(if(true(),X,Y)) -> mark(X)
     active(if(false(),X,Y)) -> mark(Y)
     mark(minus(X1,X2)) -> active(minus(X1,X2))
     mark(0()) -> active(0())
     mark(s(X)) -> active(s(mark(X)))
     mark(geq(X1,X2)) -> active(geq(X1,X2))
     mark(true()) -> active(true())
     mark(false()) -> active(false())
     mark(div(X1,X2)) -> active(div(mark(X1),X2))
     mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
     minus(mark(X1),X2) -> minus(X1,X2)
     minus(X1,mark(X2)) -> minus(X1,X2)
     minus(active(X1),X2) -> minus(X1,X2)
     minus(X1,active(X2)) -> minus(X1,X2)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     geq(mark(X1),X2) -> geq(X1,X2)
     geq(X1,mark(X2)) -> geq(X1,X2)
     geq(active(X1),X2) -> geq(X1,X2)
     geq(X1,active(X2)) -> geq(X1,X2)
     div(mark(X1),X2) -> div(X1,X2)
     div(X1,mark(X2)) -> div(X1,X2)
     div(active(X1),X2) -> div(X1,X2)
     div(X1,active(X2)) -> div(X1,X2)
     if(mark(X1),X2,X3) -> if(X1,X2,X3)
     if(X1,mark(X2),X3) -> if(X1,X2,X3)
     if(X1,X2,mark(X3)) -> if(X1,X2,X3)
     if(active(X1),X2,X3) -> if(X1,X2,X3)
     if(X1,active(X2),X3) -> if(X1,X2,X3)
     if(X1,X2,active(X3)) -> if(X1,X2,X3)
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [geq#](x0, x1) = x1,
      
      [if](x0, x1, x2) = x1 + x2,
      
      [div](x0, x1) = 0,
      
      [false] = 0,
      
      [true] = 0,
      
      [geq](x0, x1) = 0,
      
      [s](x0) = 0,
      
      [mark](x0) = x0 + 1,
      
      [active](x0) = x0 + 1,
      
      [minus](x0, x1) = 0,
      
      [0] = 0
     orientation:
      geq#(mark(X1),X2) = X2 >= X2 = geq#(X1,X2)
      
      geq#(X1,active(X2)) = X2 + 1 >= X2 = geq#(X1,X2)
      
      geq#(active(X1),X2) = X2 >= X2 = geq#(X1,X2)
      
      geq#(X1,mark(X2)) = X2 + 1 >= X2 = geq#(X1,X2)
      
      active(minus(0(),Y)) = 1 >= 1 = mark(0())
      
      active(minus(s(X),s(Y))) = 1 >= 1 = mark(minus(X,Y))
      
      active(geq(X,0())) = 1 >= 1 = mark(true())
      
      active(geq(0(),s(Y))) = 1 >= 1 = mark(false())
      
      active(geq(s(X),s(Y))) = 1 >= 1 = mark(geq(X,Y))
      
      active(div(0(),s(Y))) = 1 >= 1 = mark(0())
      
      active(div(s(X),s(Y))) = 1 >= 1 = mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
      
      active(if(true(),X,Y)) = X + Y + 1 >= X + 1 = mark(X)
      
      active(if(false(),X,Y)) = X + Y + 1 >= Y + 1 = mark(Y)
      
      mark(minus(X1,X2)) = 1 >= 1 = active(minus(X1,X2))
      
      mark(0()) = 1 >= 1 = active(0())
      
      mark(s(X)) = 1 >= 1 = active(s(mark(X)))
      
      mark(geq(X1,X2)) = 1 >= 1 = active(geq(X1,X2))
      
      mark(true()) = 1 >= 1 = active(true())
      
      mark(false()) = 1 >= 1 = active(false())
      
      mark(div(X1,X2)) = 1 >= 1 = active(div(mark(X1),X2))
      
      mark(if(X1,X2,X3)) = X2 + X3 + 1 >= X2 + X3 + 1 = active(if(mark(X1),X2,X3))
      
      minus(mark(X1),X2) = 0 >= 0 = minus(X1,X2)
      
      minus(X1,mark(X2)) = 0 >= 0 = minus(X1,X2)
      
      minus(active(X1),X2) = 0 >= 0 = minus(X1,X2)
      
      minus(X1,active(X2)) = 0 >= 0 = minus(X1,X2)
      
      s(mark(X)) = 0 >= 0 = s(X)
      
      s(active(X)) = 0 >= 0 = s(X)
      
      geq(mark(X1),X2) = 0 >= 0 = geq(X1,X2)
      
      geq(X1,mark(X2)) = 0 >= 0 = geq(X1,X2)
      
      geq(active(X1),X2) = 0 >= 0 = geq(X1,X2)
      
      geq(X1,active(X2)) = 0 >= 0 = geq(X1,X2)
      
      div(mark(X1),X2) = 0 >= 0 = div(X1,X2)
      
      div(X1,mark(X2)) = 0 >= 0 = div(X1,X2)
      
      div(active(X1),X2) = 0 >= 0 = div(X1,X2)
      
      div(X1,active(X2)) = 0 >= 0 = div(X1,X2)
      
      if(mark(X1),X2,X3) = X2 + X3 >= X2 + X3 = if(X1,X2,X3)
      
      if(X1,mark(X2),X3) = X2 + X3 + 1 >= X2 + X3 = if(X1,X2,X3)
      
      if(X1,X2,mark(X3)) = X2 + X3 + 1 >= X2 + X3 = if(X1,X2,X3)
      
      if(active(X1),X2,X3) = X2 + X3 >= X2 + X3 = if(X1,X2,X3)
      
      if(X1,active(X2),X3) = X2 + X3 + 1 >= X2 + X3 = if(X1,X2,X3)
      
      if(X1,X2,active(X3)) = X2 + X3 + 1 >= X2 + X3 = if(X1,X2,X3)
     problem:
      DPs:
       geq#(mark(X1),X2) -> geq#(X1,X2)
       geq#(active(X1),X2) -> geq#(X1,X2)
      TRS:
       active(minus(0(),Y)) -> mark(0())
       active(minus(s(X),s(Y))) -> mark(minus(X,Y))
       active(geq(X,0())) -> mark(true())
       active(geq(0(),s(Y))) -> mark(false())
       active(geq(s(X),s(Y))) -> mark(geq(X,Y))
       active(div(0(),s(Y))) -> mark(0())
       active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
       active(if(true(),X,Y)) -> mark(X)
       active(if(false(),X,Y)) -> mark(Y)
       mark(minus(X1,X2)) -> active(minus(X1,X2))
       mark(0()) -> active(0())
       mark(s(X)) -> active(s(mark(X)))
       mark(geq(X1,X2)) -> active(geq(X1,X2))
       mark(true()) -> active(true())
       mark(false()) -> active(false())
       mark(div(X1,X2)) -> active(div(mark(X1),X2))
       mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
       minus(mark(X1),X2) -> minus(X1,X2)
       minus(X1,mark(X2)) -> minus(X1,X2)
       minus(active(X1),X2) -> minus(X1,X2)
       minus(X1,active(X2)) -> minus(X1,X2)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(X)
       geq(mark(X1),X2) -> geq(X1,X2)
       geq(X1,mark(X2)) -> geq(X1,X2)
       geq(active(X1),X2) -> geq(X1,X2)
       geq(X1,active(X2)) -> geq(X1,X2)
       div(mark(X1),X2) -> div(X1,X2)
       div(X1,mark(X2)) -> div(X1,X2)
       div(active(X1),X2) -> div(X1,X2)
       div(X1,active(X2)) -> div(X1,X2)
       if(mark(X1),X2,X3) -> if(X1,X2,X3)
       if(X1,mark(X2),X3) -> if(X1,X2,X3)
       if(X1,X2,mark(X3)) -> if(X1,X2,X3)
       if(active(X1),X2,X3) -> if(X1,X2,X3)
       if(X1,active(X2),X3) -> if(X1,X2,X3)
       if(X1,X2,active(X3)) -> if(X1,X2,X3)
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [geq#](x0, x1) = x0 + 1,
       
       [if](x0, x1, x2) = x1 + x2,
       
       [div](x0, x1) = 0,
       
       [false] = 0,
       
       [true] = 0,
       
       [geq](x0, x1) = 0,
       
       [s](x0) = 0,
       
       [mark](x0) = x0 + 1,
       
       [active](x0) = x0 + 1,
       
       [minus](x0, x1) = 0,
       
       [0] = 0
      orientation:
       geq#(mark(X1),X2) = X1 + 2 >= X1 + 1 = geq#(X1,X2)
       
       geq#(active(X1),X2) = X1 + 2 >= X1 + 1 = geq#(X1,X2)
       
       active(minus(0(),Y)) = 1 >= 1 = mark(0())
       
       active(minus(s(X),s(Y))) = 1 >= 1 = mark(minus(X,Y))
       
       active(geq(X,0())) = 1 >= 1 = mark(true())
       
       active(geq(0(),s(Y))) = 1 >= 1 = mark(false())
       
       active(geq(s(X),s(Y))) = 1 >= 1 = mark(geq(X,Y))
       
       active(div(0(),s(Y))) = 1 >= 1 = mark(0())
       
       active(div(s(X),s(Y))) = 1 >= 1 = mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
       
       active(if(true(),X,Y)) = X + Y + 1 >= X + 1 = mark(X)
       
       active(if(false(),X,Y)) = X + Y + 1 >= Y + 1 = mark(Y)
       
       mark(minus(X1,X2)) = 1 >= 1 = active(minus(X1,X2))
       
       mark(0()) = 1 >= 1 = active(0())
       
       mark(s(X)) = 1 >= 1 = active(s(mark(X)))
       
       mark(geq(X1,X2)) = 1 >= 1 = active(geq(X1,X2))
       
       mark(true()) = 1 >= 1 = active(true())
       
       mark(false()) = 1 >= 1 = active(false())
       
       mark(div(X1,X2)) = 1 >= 1 = active(div(mark(X1),X2))
       
       mark(if(X1,X2,X3)) = X2 + X3 + 1 >= X2 + X3 + 1 = active(if(mark(X1),X2,X3))
       
       minus(mark(X1),X2) = 0 >= 0 = minus(X1,X2)
       
       minus(X1,mark(X2)) = 0 >= 0 = minus(X1,X2)
       
       minus(active(X1),X2) = 0 >= 0 = minus(X1,X2)
       
       minus(X1,active(X2)) = 0 >= 0 = minus(X1,X2)
       
       s(mark(X)) = 0 >= 0 = s(X)
       
       s(active(X)) = 0 >= 0 = s(X)
       
       geq(mark(X1),X2) = 0 >= 0 = geq(X1,X2)
       
       geq(X1,mark(X2)) = 0 >= 0 = geq(X1,X2)
       
       geq(active(X1),X2) = 0 >= 0 = geq(X1,X2)
       
       geq(X1,active(X2)) = 0 >= 0 = geq(X1,X2)
       
       div(mark(X1),X2) = 0 >= 0 = div(X1,X2)
       
       div(X1,mark(X2)) = 0 >= 0 = div(X1,X2)
       
       div(active(X1),X2) = 0 >= 0 = div(X1,X2)
       
       div(X1,active(X2)) = 0 >= 0 = div(X1,X2)
       
       if(mark(X1),X2,X3) = X2 + X3 >= X2 + X3 = if(X1,X2,X3)
       
       if(X1,mark(X2),X3) = X2 + X3 + 1 >= X2 + X3 = if(X1,X2,X3)
       
       if(X1,X2,mark(X3)) = X2 + X3 + 1 >= X2 + X3 = if(X1,X2,X3)
       
       if(active(X1),X2,X3) = X2 + X3 >= X2 + X3 = if(X1,X2,X3)
       
       if(X1,active(X2),X3) = X2 + X3 + 1 >= X2 + X3 = if(X1,X2,X3)
       
       if(X1,X2,active(X3)) = X2 + X3 + 1 >= X2 + X3 = if(X1,X2,X3)
      problem:
       DPs:
        
       TRS:
        active(minus(0(),Y)) -> mark(0())
        active(minus(s(X),s(Y))) -> mark(minus(X,Y))
        active(geq(X,0())) -> mark(true())
        active(geq(0(),s(Y))) -> mark(false())
        active(geq(s(X),s(Y))) -> mark(geq(X,Y))
        active(div(0(),s(Y))) -> mark(0())
        active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
        active(if(true(),X,Y)) -> mark(X)
        active(if(false(),X,Y)) -> mark(Y)
        mark(minus(X1,X2)) -> active(minus(X1,X2))
        mark(0()) -> active(0())
        mark(s(X)) -> active(s(mark(X)))
        mark(geq(X1,X2)) -> active(geq(X1,X2))
        mark(true()) -> active(true())
        mark(false()) -> active(false())
        mark(div(X1,X2)) -> active(div(mark(X1),X2))
        mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
        minus(mark(X1),X2) -> minus(X1,X2)
        minus(X1,mark(X2)) -> minus(X1,X2)
        minus(active(X1),X2) -> minus(X1,X2)
        minus(X1,active(X2)) -> minus(X1,X2)
        s(mark(X)) -> s(X)
        s(active(X)) -> s(X)
        geq(mark(X1),X2) -> geq(X1,X2)
        geq(X1,mark(X2)) -> geq(X1,X2)
        geq(active(X1),X2) -> geq(X1,X2)
        geq(X1,active(X2)) -> geq(X1,X2)
        div(mark(X1),X2) -> div(X1,X2)
        div(X1,mark(X2)) -> div(X1,X2)
        div(active(X1),X2) -> div(X1,X2)
        div(X1,active(X2)) -> div(X1,X2)
        if(mark(X1),X2,X3) -> if(X1,X2,X3)
        if(X1,mark(X2),X3) -> if(X1,X2,X3)
        if(X1,X2,mark(X3)) -> if(X1,X2,X3)
        if(active(X1),X2,X3) -> if(X1,X2,X3)
        if(X1,active(X2),X3) -> if(X1,X2,X3)
        if(X1,X2,active(X3)) -> if(X1,X2,X3)
      Qed
    
    DPs:
     div#(mark(X1),X2) -> div#(X1,X2)
     div#(X1,active(X2)) -> div#(X1,X2)
     div#(active(X1),X2) -> div#(X1,X2)
     div#(X1,mark(X2)) -> div#(X1,X2)
    TRS:
     active(minus(0(),Y)) -> mark(0())
     active(minus(s(X),s(Y))) -> mark(minus(X,Y))
     active(geq(X,0())) -> mark(true())
     active(geq(0(),s(Y))) -> mark(false())
     active(geq(s(X),s(Y))) -> mark(geq(X,Y))
     active(div(0(),s(Y))) -> mark(0())
     active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
     active(if(true(),X,Y)) -> mark(X)
     active(if(false(),X,Y)) -> mark(Y)
     mark(minus(X1,X2)) -> active(minus(X1,X2))
     mark(0()) -> active(0())
     mark(s(X)) -> active(s(mark(X)))
     mark(geq(X1,X2)) -> active(geq(X1,X2))
     mark(true()) -> active(true())
     mark(false()) -> active(false())
     mark(div(X1,X2)) -> active(div(mark(X1),X2))
     mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
     minus(mark(X1),X2) -> minus(X1,X2)
     minus(X1,mark(X2)) -> minus(X1,X2)
     minus(active(X1),X2) -> minus(X1,X2)
     minus(X1,active(X2)) -> minus(X1,X2)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     geq(mark(X1),X2) -> geq(X1,X2)
     geq(X1,mark(X2)) -> geq(X1,X2)
     geq(active(X1),X2) -> geq(X1,X2)
     geq(X1,active(X2)) -> geq(X1,X2)
     div(mark(X1),X2) -> div(X1,X2)
     div(X1,mark(X2)) -> div(X1,X2)
     div(active(X1),X2) -> div(X1,X2)
     div(X1,active(X2)) -> div(X1,X2)
     if(mark(X1),X2,X3) -> if(X1,X2,X3)
     if(X1,mark(X2),X3) -> if(X1,X2,X3)
     if(X1,X2,mark(X3)) -> if(X1,X2,X3)
     if(active(X1),X2,X3) -> if(X1,X2,X3)
     if(X1,active(X2),X3) -> if(X1,X2,X3)
     if(X1,X2,active(X3)) -> if(X1,X2,X3)
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [div#](x0, x1) = x1,
      
      [if](x0, x1, x2) = x1 + x2,
      
      [div](x0, x1) = 0,
      
      [false] = 0,
      
      [true] = 0,
      
      [geq](x0, x1) = 0,
      
      [s](x0) = 0,
      
      [mark](x0) = x0 + 1,
      
      [active](x0) = x0 + 1,
      
      [minus](x0, x1) = 0,
      
      [0] = 0
     orientation:
      div#(mark(X1),X2) = X2 >= X2 = div#(X1,X2)
      
      div#(X1,active(X2)) = X2 + 1 >= X2 = div#(X1,X2)
      
      div#(active(X1),X2) = X2 >= X2 = div#(X1,X2)
      
      div#(X1,mark(X2)) = X2 + 1 >= X2 = div#(X1,X2)
      
      active(minus(0(),Y)) = 1 >= 1 = mark(0())
      
      active(minus(s(X),s(Y))) = 1 >= 1 = mark(minus(X,Y))
      
      active(geq(X,0())) = 1 >= 1 = mark(true())
      
      active(geq(0(),s(Y))) = 1 >= 1 = mark(false())
      
      active(geq(s(X),s(Y))) = 1 >= 1 = mark(geq(X,Y))
      
      active(div(0(),s(Y))) = 1 >= 1 = mark(0())
      
      active(div(s(X),s(Y))) = 1 >= 1 = mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
      
      active(if(true(),X,Y)) = X + Y + 1 >= X + 1 = mark(X)
      
      active(if(false(),X,Y)) = X + Y + 1 >= Y + 1 = mark(Y)
      
      mark(minus(X1,X2)) = 1 >= 1 = active(minus(X1,X2))
      
      mark(0()) = 1 >= 1 = active(0())
      
      mark(s(X)) = 1 >= 1 = active(s(mark(X)))
      
      mark(geq(X1,X2)) = 1 >= 1 = active(geq(X1,X2))
      
      mark(true()) = 1 >= 1 = active(true())
      
      mark(false()) = 1 >= 1 = active(false())
      
      mark(div(X1,X2)) = 1 >= 1 = active(div(mark(X1),X2))
      
      mark(if(X1,X2,X3)) = X2 + X3 + 1 >= X2 + X3 + 1 = active(if(mark(X1),X2,X3))
      
      minus(mark(X1),X2) = 0 >= 0 = minus(X1,X2)
      
      minus(X1,mark(X2)) = 0 >= 0 = minus(X1,X2)
      
      minus(active(X1),X2) = 0 >= 0 = minus(X1,X2)
      
      minus(X1,active(X2)) = 0 >= 0 = minus(X1,X2)
      
      s(mark(X)) = 0 >= 0 = s(X)
      
      s(active(X)) = 0 >= 0 = s(X)
      
      geq(mark(X1),X2) = 0 >= 0 = geq(X1,X2)
      
      geq(X1,mark(X2)) = 0 >= 0 = geq(X1,X2)
      
      geq(active(X1),X2) = 0 >= 0 = geq(X1,X2)
      
      geq(X1,active(X2)) = 0 >= 0 = geq(X1,X2)
      
      div(mark(X1),X2) = 0 >= 0 = div(X1,X2)
      
      div(X1,mark(X2)) = 0 >= 0 = div(X1,X2)
      
      div(active(X1),X2) = 0 >= 0 = div(X1,X2)
      
      div(X1,active(X2)) = 0 >= 0 = div(X1,X2)
      
      if(mark(X1),X2,X3) = X2 + X3 >= X2 + X3 = if(X1,X2,X3)
      
      if(X1,mark(X2),X3) = X2 + X3 + 1 >= X2 + X3 = if(X1,X2,X3)
      
      if(X1,X2,mark(X3)) = X2 + X3 + 1 >= X2 + X3 = if(X1,X2,X3)
      
      if(active(X1),X2,X3) = X2 + X3 >= X2 + X3 = if(X1,X2,X3)
      
      if(X1,active(X2),X3) = X2 + X3 + 1 >= X2 + X3 = if(X1,X2,X3)
      
      if(X1,X2,active(X3)) = X2 + X3 + 1 >= X2 + X3 = if(X1,X2,X3)
     problem:
      DPs:
       div#(mark(X1),X2) -> div#(X1,X2)
       div#(active(X1),X2) -> div#(X1,X2)
      TRS:
       active(minus(0(),Y)) -> mark(0())
       active(minus(s(X),s(Y))) -> mark(minus(X,Y))
       active(geq(X,0())) -> mark(true())
       active(geq(0(),s(Y))) -> mark(false())
       active(geq(s(X),s(Y))) -> mark(geq(X,Y))
       active(div(0(),s(Y))) -> mark(0())
       active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
       active(if(true(),X,Y)) -> mark(X)
       active(if(false(),X,Y)) -> mark(Y)
       mark(minus(X1,X2)) -> active(minus(X1,X2))
       mark(0()) -> active(0())
       mark(s(X)) -> active(s(mark(X)))
       mark(geq(X1,X2)) -> active(geq(X1,X2))
       mark(true()) -> active(true())
       mark(false()) -> active(false())
       mark(div(X1,X2)) -> active(div(mark(X1),X2))
       mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
       minus(mark(X1),X2) -> minus(X1,X2)
       minus(X1,mark(X2)) -> minus(X1,X2)
       minus(active(X1),X2) -> minus(X1,X2)
       minus(X1,active(X2)) -> minus(X1,X2)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(X)
       geq(mark(X1),X2) -> geq(X1,X2)
       geq(X1,mark(X2)) -> geq(X1,X2)
       geq(active(X1),X2) -> geq(X1,X2)
       geq(X1,active(X2)) -> geq(X1,X2)
       div(mark(X1),X2) -> div(X1,X2)
       div(X1,mark(X2)) -> div(X1,X2)
       div(active(X1),X2) -> div(X1,X2)
       div(X1,active(X2)) -> div(X1,X2)
       if(mark(X1),X2,X3) -> if(X1,X2,X3)
       if(X1,mark(X2),X3) -> if(X1,X2,X3)
       if(X1,X2,mark(X3)) -> if(X1,X2,X3)
       if(active(X1),X2,X3) -> if(X1,X2,X3)
       if(X1,active(X2),X3) -> if(X1,X2,X3)
       if(X1,X2,active(X3)) -> if(X1,X2,X3)
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [div#](x0, x1) = x0 + 1,
       
       [if](x0, x1, x2) = x1 + x2,
       
       [div](x0, x1) = 0,
       
       [false] = 0,
       
       [true] = 0,
       
       [geq](x0, x1) = 0,
       
       [s](x0) = 0,
       
       [mark](x0) = x0 + 1,
       
       [active](x0) = x0 + 1,
       
       [minus](x0, x1) = 0,
       
       [0] = 0
      orientation:
       div#(mark(X1),X2) = X1 + 2 >= X1 + 1 = div#(X1,X2)
       
       div#(active(X1),X2) = X1 + 2 >= X1 + 1 = div#(X1,X2)
       
       active(minus(0(),Y)) = 1 >= 1 = mark(0())
       
       active(minus(s(X),s(Y))) = 1 >= 1 = mark(minus(X,Y))
       
       active(geq(X,0())) = 1 >= 1 = mark(true())
       
       active(geq(0(),s(Y))) = 1 >= 1 = mark(false())
       
       active(geq(s(X),s(Y))) = 1 >= 1 = mark(geq(X,Y))
       
       active(div(0(),s(Y))) = 1 >= 1 = mark(0())
       
       active(div(s(X),s(Y))) = 1 >= 1 = mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
       
       active(if(true(),X,Y)) = X + Y + 1 >= X + 1 = mark(X)
       
       active(if(false(),X,Y)) = X + Y + 1 >= Y + 1 = mark(Y)
       
       mark(minus(X1,X2)) = 1 >= 1 = active(minus(X1,X2))
       
       mark(0()) = 1 >= 1 = active(0())
       
       mark(s(X)) = 1 >= 1 = active(s(mark(X)))
       
       mark(geq(X1,X2)) = 1 >= 1 = active(geq(X1,X2))
       
       mark(true()) = 1 >= 1 = active(true())
       
       mark(false()) = 1 >= 1 = active(false())
       
       mark(div(X1,X2)) = 1 >= 1 = active(div(mark(X1),X2))
       
       mark(if(X1,X2,X3)) = X2 + X3 + 1 >= X2 + X3 + 1 = active(if(mark(X1),X2,X3))
       
       minus(mark(X1),X2) = 0 >= 0 = minus(X1,X2)
       
       minus(X1,mark(X2)) = 0 >= 0 = minus(X1,X2)
       
       minus(active(X1),X2) = 0 >= 0 = minus(X1,X2)
       
       minus(X1,active(X2)) = 0 >= 0 = minus(X1,X2)
       
       s(mark(X)) = 0 >= 0 = s(X)
       
       s(active(X)) = 0 >= 0 = s(X)
       
       geq(mark(X1),X2) = 0 >= 0 = geq(X1,X2)
       
       geq(X1,mark(X2)) = 0 >= 0 = geq(X1,X2)
       
       geq(active(X1),X2) = 0 >= 0 = geq(X1,X2)
       
       geq(X1,active(X2)) = 0 >= 0 = geq(X1,X2)
       
       div(mark(X1),X2) = 0 >= 0 = div(X1,X2)
       
       div(X1,mark(X2)) = 0 >= 0 = div(X1,X2)
       
       div(active(X1),X2) = 0 >= 0 = div(X1,X2)
       
       div(X1,active(X2)) = 0 >= 0 = div(X1,X2)
       
       if(mark(X1),X2,X3) = X2 + X3 >= X2 + X3 = if(X1,X2,X3)
       
       if(X1,mark(X2),X3) = X2 + X3 + 1 >= X2 + X3 = if(X1,X2,X3)
       
       if(X1,X2,mark(X3)) = X2 + X3 + 1 >= X2 + X3 = if(X1,X2,X3)
       
       if(active(X1),X2,X3) = X2 + X3 >= X2 + X3 = if(X1,X2,X3)
       
       if(X1,active(X2),X3) = X2 + X3 + 1 >= X2 + X3 = if(X1,X2,X3)
       
       if(X1,X2,active(X3)) = X2 + X3 + 1 >= X2 + X3 = if(X1,X2,X3)
      problem:
       DPs:
        
       TRS:
        active(minus(0(),Y)) -> mark(0())
        active(minus(s(X),s(Y))) -> mark(minus(X,Y))
        active(geq(X,0())) -> mark(true())
        active(geq(0(),s(Y))) -> mark(false())
        active(geq(s(X),s(Y))) -> mark(geq(X,Y))
        active(div(0(),s(Y))) -> mark(0())
        active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
        active(if(true(),X,Y)) -> mark(X)
        active(if(false(),X,Y)) -> mark(Y)
        mark(minus(X1,X2)) -> active(minus(X1,X2))
        mark(0()) -> active(0())
        mark(s(X)) -> active(s(mark(X)))
        mark(geq(X1,X2)) -> active(geq(X1,X2))
        mark(true()) -> active(true())
        mark(false()) -> active(false())
        mark(div(X1,X2)) -> active(div(mark(X1),X2))
        mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
        minus(mark(X1),X2) -> minus(X1,X2)
        minus(X1,mark(X2)) -> minus(X1,X2)
        minus(active(X1),X2) -> minus(X1,X2)
        minus(X1,active(X2)) -> minus(X1,X2)
        s(mark(X)) -> s(X)
        s(active(X)) -> s(X)
        geq(mark(X1),X2) -> geq(X1,X2)
        geq(X1,mark(X2)) -> geq(X1,X2)
        geq(active(X1),X2) -> geq(X1,X2)
        geq(X1,active(X2)) -> geq(X1,X2)
        div(mark(X1),X2) -> div(X1,X2)
        div(X1,mark(X2)) -> div(X1,X2)
        div(active(X1),X2) -> div(X1,X2)
        div(X1,active(X2)) -> div(X1,X2)
        if(mark(X1),X2,X3) -> if(X1,X2,X3)
        if(X1,mark(X2),X3) -> if(X1,X2,X3)
        if(X1,X2,mark(X3)) -> if(X1,X2,X3)
        if(active(X1),X2,X3) -> if(X1,X2,X3)
        if(X1,active(X2),X3) -> if(X1,X2,X3)
        if(X1,X2,active(X3)) -> if(X1,X2,X3)
      Qed
    
    DPs:
     s#(mark(X)) -> s#(X)
     s#(active(X)) -> s#(X)
    TRS:
     active(minus(0(),Y)) -> mark(0())
     active(minus(s(X),s(Y))) -> mark(minus(X,Y))
     active(geq(X,0())) -> mark(true())
     active(geq(0(),s(Y))) -> mark(false())
     active(geq(s(X),s(Y))) -> mark(geq(X,Y))
     active(div(0(),s(Y))) -> mark(0())
     active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
     active(if(true(),X,Y)) -> mark(X)
     active(if(false(),X,Y)) -> mark(Y)
     mark(minus(X1,X2)) -> active(minus(X1,X2))
     mark(0()) -> active(0())
     mark(s(X)) -> active(s(mark(X)))
     mark(geq(X1,X2)) -> active(geq(X1,X2))
     mark(true()) -> active(true())
     mark(false()) -> active(false())
     mark(div(X1,X2)) -> active(div(mark(X1),X2))
     mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
     minus(mark(X1),X2) -> minus(X1,X2)
     minus(X1,mark(X2)) -> minus(X1,X2)
     minus(active(X1),X2) -> minus(X1,X2)
     minus(X1,active(X2)) -> minus(X1,X2)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     geq(mark(X1),X2) -> geq(X1,X2)
     geq(X1,mark(X2)) -> geq(X1,X2)
     geq(active(X1),X2) -> geq(X1,X2)
     geq(X1,active(X2)) -> geq(X1,X2)
     div(mark(X1),X2) -> div(X1,X2)
     div(X1,mark(X2)) -> div(X1,X2)
     div(active(X1),X2) -> div(X1,X2)
     div(X1,active(X2)) -> div(X1,X2)
     if(mark(X1),X2,X3) -> if(X1,X2,X3)
     if(X1,mark(X2),X3) -> if(X1,X2,X3)
     if(X1,X2,mark(X3)) -> if(X1,X2,X3)
     if(active(X1),X2,X3) -> if(X1,X2,X3)
     if(X1,active(X2),X3) -> if(X1,X2,X3)
     if(X1,X2,active(X3)) -> if(X1,X2,X3)
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [s#](x0) = x0,
      
      [if](x0, x1, x2) = x1 + x2,
      
      [div](x0, x1) = x1,
      
      [false] = 0,
      
      [true] = 0,
      
      [geq](x0, x1) = 1,
      
      [s](x0) = 0,
      
      [mark](x0) = x0 + 1,
      
      [active](x0) = x0 + 1,
      
      [minus](x0, x1) = 0,
      
      [0] = 0
     orientation:
      s#(mark(X)) = X + 1 >= X = s#(X)
      
      s#(active(X)) = X + 1 >= X = s#(X)
      
      active(minus(0(),Y)) = 1 >= 1 = mark(0())
      
      active(minus(s(X),s(Y))) = 1 >= 1 = mark(minus(X,Y))
      
      active(geq(X,0())) = 2 >= 1 = mark(true())
      
      active(geq(0(),s(Y))) = 2 >= 1 = mark(false())
      
      active(geq(s(X),s(Y))) = 2 >= 2 = mark(geq(X,Y))
      
      active(div(0(),s(Y))) = 1 >= 1 = mark(0())
      
      active(div(s(X),s(Y))) = 1 >= 1 = mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
      
      active(if(true(),X,Y)) = X + Y + 1 >= X + 1 = mark(X)
      
      active(if(false(),X,Y)) = X + Y + 1 >= Y + 1 = mark(Y)
      
      mark(minus(X1,X2)) = 1 >= 1 = active(minus(X1,X2))
      
      mark(0()) = 1 >= 1 = active(0())
      
      mark(s(X)) = 1 >= 1 = active(s(mark(X)))
      
      mark(geq(X1,X2)) = 2 >= 2 = active(geq(X1,X2))
      
      mark(true()) = 1 >= 1 = active(true())
      
      mark(false()) = 1 >= 1 = active(false())
      
      mark(div(X1,X2)) = X2 + 1 >= X2 + 1 = active(div(mark(X1),X2))
      
      mark(if(X1,X2,X3)) = X2 + X3 + 1 >= X2 + X3 + 1 = active(if(mark(X1),X2,X3))
      
      minus(mark(X1),X2) = 0 >= 0 = minus(X1,X2)
      
      minus(X1,mark(X2)) = 0 >= 0 = minus(X1,X2)
      
      minus(active(X1),X2) = 0 >= 0 = minus(X1,X2)
      
      minus(X1,active(X2)) = 0 >= 0 = minus(X1,X2)
      
      s(mark(X)) = 0 >= 0 = s(X)
      
      s(active(X)) = 0 >= 0 = s(X)
      
      geq(mark(X1),X2) = 1 >= 1 = geq(X1,X2)
      
      geq(X1,mark(X2)) = 1 >= 1 = geq(X1,X2)
      
      geq(active(X1),X2) = 1 >= 1 = geq(X1,X2)
      
      geq(X1,active(X2)) = 1 >= 1 = geq(X1,X2)
      
      div(mark(X1),X2) = X2 >= X2 = div(X1,X2)
      
      div(X1,mark(X2)) = X2 + 1 >= X2 = div(X1,X2)
      
      div(active(X1),X2) = X2 >= X2 = div(X1,X2)
      
      div(X1,active(X2)) = X2 + 1 >= X2 = div(X1,X2)
      
      if(mark(X1),X2,X3) = X2 + X3 >= X2 + X3 = if(X1,X2,X3)
      
      if(X1,mark(X2),X3) = X2 + X3 + 1 >= X2 + X3 = if(X1,X2,X3)
      
      if(X1,X2,mark(X3)) = X2 + X3 + 1 >= X2 + X3 = if(X1,X2,X3)
      
      if(active(X1),X2,X3) = X2 + X3 >= X2 + X3 = if(X1,X2,X3)
      
      if(X1,active(X2),X3) = X2 + X3 + 1 >= X2 + X3 = if(X1,X2,X3)
      
      if(X1,X2,active(X3)) = X2 + X3 + 1 >= X2 + X3 = if(X1,X2,X3)
     problem:
      DPs:
       
      TRS:
       active(minus(0(),Y)) -> mark(0())
       active(minus(s(X),s(Y))) -> mark(minus(X,Y))
       active(geq(X,0())) -> mark(true())
       active(geq(0(),s(Y))) -> mark(false())
       active(geq(s(X),s(Y))) -> mark(geq(X,Y))
       active(div(0(),s(Y))) -> mark(0())
       active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
       active(if(true(),X,Y)) -> mark(X)
       active(if(false(),X,Y)) -> mark(Y)
       mark(minus(X1,X2)) -> active(minus(X1,X2))
       mark(0()) -> active(0())
       mark(s(X)) -> active(s(mark(X)))
       mark(geq(X1,X2)) -> active(geq(X1,X2))
       mark(true()) -> active(true())
       mark(false()) -> active(false())
       mark(div(X1,X2)) -> active(div(mark(X1),X2))
       mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
       minus(mark(X1),X2) -> minus(X1,X2)
       minus(X1,mark(X2)) -> minus(X1,X2)
       minus(active(X1),X2) -> minus(X1,X2)
       minus(X1,active(X2)) -> minus(X1,X2)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(X)
       geq(mark(X1),X2) -> geq(X1,X2)
       geq(X1,mark(X2)) -> geq(X1,X2)
       geq(active(X1),X2) -> geq(X1,X2)
       geq(X1,active(X2)) -> geq(X1,X2)
       div(mark(X1),X2) -> div(X1,X2)
       div(X1,mark(X2)) -> div(X1,X2)
       div(active(X1),X2) -> div(X1,X2)
       div(X1,active(X2)) -> div(X1,X2)
       if(mark(X1),X2,X3) -> if(X1,X2,X3)
       if(X1,mark(X2),X3) -> if(X1,X2,X3)
       if(X1,X2,mark(X3)) -> if(X1,X2,X3)
       if(active(X1),X2,X3) -> if(X1,X2,X3)
       if(X1,active(X2),X3) -> if(X1,X2,X3)
       if(X1,X2,active(X3)) -> if(X1,X2,X3)
     Qed
    
    DPs:
     if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
     if#(X1,X2,active(X3)) -> if#(X1,X2,X3)
     if#(X1,active(X2),X3) -> if#(X1,X2,X3)
     if#(active(X1),X2,X3) -> if#(X1,X2,X3)
     if#(X1,X2,mark(X3)) -> if#(X1,X2,X3)
     if#(X1,mark(X2),X3) -> if#(X1,X2,X3)
    TRS:
     active(minus(0(),Y)) -> mark(0())
     active(minus(s(X),s(Y))) -> mark(minus(X,Y))
     active(geq(X,0())) -> mark(true())
     active(geq(0(),s(Y))) -> mark(false())
     active(geq(s(X),s(Y))) -> mark(geq(X,Y))
     active(div(0(),s(Y))) -> mark(0())
     active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
     active(if(true(),X,Y)) -> mark(X)
     active(if(false(),X,Y)) -> mark(Y)
     mark(minus(X1,X2)) -> active(minus(X1,X2))
     mark(0()) -> active(0())
     mark(s(X)) -> active(s(mark(X)))
     mark(geq(X1,X2)) -> active(geq(X1,X2))
     mark(true()) -> active(true())
     mark(false()) -> active(false())
     mark(div(X1,X2)) -> active(div(mark(X1),X2))
     mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
     minus(mark(X1),X2) -> minus(X1,X2)
     minus(X1,mark(X2)) -> minus(X1,X2)
     minus(active(X1),X2) -> minus(X1,X2)
     minus(X1,active(X2)) -> minus(X1,X2)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     geq(mark(X1),X2) -> geq(X1,X2)
     geq(X1,mark(X2)) -> geq(X1,X2)
     geq(active(X1),X2) -> geq(X1,X2)
     geq(X1,active(X2)) -> geq(X1,X2)
     div(mark(X1),X2) -> div(X1,X2)
     div(X1,mark(X2)) -> div(X1,X2)
     div(active(X1),X2) -> div(X1,X2)
     div(X1,active(X2)) -> div(X1,X2)
     if(mark(X1),X2,X3) -> if(X1,X2,X3)
     if(X1,mark(X2),X3) -> if(X1,X2,X3)
     if(X1,X2,mark(X3)) -> if(X1,X2,X3)
     if(active(X1),X2,X3) -> if(X1,X2,X3)
     if(X1,active(X2),X3) -> if(X1,X2,X3)
     if(X1,X2,active(X3)) -> if(X1,X2,X3)
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [if#](x0, x1, x2) = x1,
      
      [if](x0, x1, x2) = x1 + x2,
      
      [div](x0, x1) = 0,
      
      [false] = 0,
      
      [true] = 0,
      
      [geq](x0, x1) = 1,
      
      [s](x0) = 0,
      
      [mark](x0) = x0 + 1,
      
      [active](x0) = x0 + 1,
      
      [minus](x0, x1) = 0,
      
      [0] = 0
     orientation:
      if#(mark(X1),X2,X3) = X2 >= X2 = if#(X1,X2,X3)
      
      if#(X1,X2,active(X3)) = X2 >= X2 = if#(X1,X2,X3)
      
      if#(X1,active(X2),X3) = X2 + 1 >= X2 = if#(X1,X2,X3)
      
      if#(active(X1),X2,X3) = X2 >= X2 = if#(X1,X2,X3)
      
      if#(X1,X2,mark(X3)) = X2 >= X2 = if#(X1,X2,X3)
      
      if#(X1,mark(X2),X3) = X2 + 1 >= X2 = if#(X1,X2,X3)
      
      active(minus(0(),Y)) = 1 >= 1 = mark(0())
      
      active(minus(s(X),s(Y))) = 1 >= 1 = mark(minus(X,Y))
      
      active(geq(X,0())) = 2 >= 1 = mark(true())
      
      active(geq(0(),s(Y))) = 2 >= 1 = mark(false())
      
      active(geq(s(X),s(Y))) = 2 >= 2 = mark(geq(X,Y))
      
      active(div(0(),s(Y))) = 1 >= 1 = mark(0())
      
      active(div(s(X),s(Y))) = 1 >= 1 = mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
      
      active(if(true(),X,Y)) = X + Y + 1 >= X + 1 = mark(X)
      
      active(if(false(),X,Y)) = X + Y + 1 >= Y + 1 = mark(Y)
      
      mark(minus(X1,X2)) = 1 >= 1 = active(minus(X1,X2))
      
      mark(0()) = 1 >= 1 = active(0())
      
      mark(s(X)) = 1 >= 1 = active(s(mark(X)))
      
      mark(geq(X1,X2)) = 2 >= 2 = active(geq(X1,X2))
      
      mark(true()) = 1 >= 1 = active(true())
      
      mark(false()) = 1 >= 1 = active(false())
      
      mark(div(X1,X2)) = 1 >= 1 = active(div(mark(X1),X2))
      
      mark(if(X1,X2,X3)) = X2 + X3 + 1 >= X2 + X3 + 1 = active(if(mark(X1),X2,X3))
      
      minus(mark(X1),X2) = 0 >= 0 = minus(X1,X2)
      
      minus(X1,mark(X2)) = 0 >= 0 = minus(X1,X2)
      
      minus(active(X1),X2) = 0 >= 0 = minus(X1,X2)
      
      minus(X1,active(X2)) = 0 >= 0 = minus(X1,X2)
      
      s(mark(X)) = 0 >= 0 = s(X)
      
      s(active(X)) = 0 >= 0 = s(X)
      
      geq(mark(X1),X2) = 1 >= 1 = geq(X1,X2)
      
      geq(X1,mark(X2)) = 1 >= 1 = geq(X1,X2)
      
      geq(active(X1),X2) = 1 >= 1 = geq(X1,X2)
      
      geq(X1,active(X2)) = 1 >= 1 = geq(X1,X2)
      
      div(mark(X1),X2) = 0 >= 0 = div(X1,X2)
      
      div(X1,mark(X2)) = 0 >= 0 = div(X1,X2)
      
      div(active(X1),X2) = 0 >= 0 = div(X1,X2)
      
      div(X1,active(X2)) = 0 >= 0 = div(X1,X2)
      
      if(mark(X1),X2,X3) = X2 + X3 >= X2 + X3 = if(X1,X2,X3)
      
      if(X1,mark(X2),X3) = X2 + X3 + 1 >= X2 + X3 = if(X1,X2,X3)
      
      if(X1,X2,mark(X3)) = X2 + X3 + 1 >= X2 + X3 = if(X1,X2,X3)
      
      if(active(X1),X2,X3) = X2 + X3 >= X2 + X3 = if(X1,X2,X3)
      
      if(X1,active(X2),X3) = X2 + X3 + 1 >= X2 + X3 = if(X1,X2,X3)
      
      if(X1,X2,active(X3)) = X2 + X3 + 1 >= X2 + X3 = if(X1,X2,X3)
     problem:
      DPs:
       if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
       if#(X1,X2,active(X3)) -> if#(X1,X2,X3)
       if#(active(X1),X2,X3) -> if#(X1,X2,X3)
       if#(X1,X2,mark(X3)) -> if#(X1,X2,X3)
      TRS:
       active(minus(0(),Y)) -> mark(0())
       active(minus(s(X),s(Y))) -> mark(minus(X,Y))
       active(geq(X,0())) -> mark(true())
       active(geq(0(),s(Y))) -> mark(false())
       active(geq(s(X),s(Y))) -> mark(geq(X,Y))
       active(div(0(),s(Y))) -> mark(0())
       active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
       active(if(true(),X,Y)) -> mark(X)
       active(if(false(),X,Y)) -> mark(Y)
       mark(minus(X1,X2)) -> active(minus(X1,X2))
       mark(0()) -> active(0())
       mark(s(X)) -> active(s(mark(X)))
       mark(geq(X1,X2)) -> active(geq(X1,X2))
       mark(true()) -> active(true())
       mark(false()) -> active(false())
       mark(div(X1,X2)) -> active(div(mark(X1),X2))
       mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
       minus(mark(X1),X2) -> minus(X1,X2)
       minus(X1,mark(X2)) -> minus(X1,X2)
       minus(active(X1),X2) -> minus(X1,X2)
       minus(X1,active(X2)) -> minus(X1,X2)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(X)
       geq(mark(X1),X2) -> geq(X1,X2)
       geq(X1,mark(X2)) -> geq(X1,X2)
       geq(active(X1),X2) -> geq(X1,X2)
       geq(X1,active(X2)) -> geq(X1,X2)
       div(mark(X1),X2) -> div(X1,X2)
       div(X1,mark(X2)) -> div(X1,X2)
       div(active(X1),X2) -> div(X1,X2)
       div(X1,active(X2)) -> div(X1,X2)
       if(mark(X1),X2,X3) -> if(X1,X2,X3)
       if(X1,mark(X2),X3) -> if(X1,X2,X3)
       if(X1,X2,mark(X3)) -> if(X1,X2,X3)
       if(active(X1),X2,X3) -> if(X1,X2,X3)
       if(X1,active(X2),X3) -> if(X1,X2,X3)
       if(X1,X2,active(X3)) -> if(X1,X2,X3)
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [if#](x0, x1, x2) = x0 + x2 + 1,
       
       [if](x0, x1, x2) = x1 + x2,
       
       [div](x0, x1) = 0,
       
       [false] = 1,
       
       [true] = 1,
       
       [geq](x0, x1) = 1,
       
       [s](x0) = 0,
       
       [mark](x0) = x0 + 1,
       
       [active](x0) = x0 + 1,
       
       [minus](x0, x1) = 0,
       
       [0] = 0
      orientation:
       if#(mark(X1),X2,X3) = X1 + X3 + 2 >= X1 + X3 + 1 = if#(X1,X2,X3)
       
       if#(X1,X2,active(X3)) = X1 + X3 + 2 >= X1 + X3 + 1 = if#(X1,X2,X3)
       
       if#(active(X1),X2,X3) = X1 + X3 + 2 >= X1 + X3 + 1 = if#(X1,X2,X3)
       
       if#(X1,X2,mark(X3)) = X1 + X3 + 2 >= X1 + X3 + 1 = if#(X1,X2,X3)
       
       active(minus(0(),Y)) = 1 >= 1 = mark(0())
       
       active(minus(s(X),s(Y))) = 1 >= 1 = mark(minus(X,Y))
       
       active(geq(X,0())) = 2 >= 2 = mark(true())
       
       active(geq(0(),s(Y))) = 2 >= 2 = mark(false())
       
       active(geq(s(X),s(Y))) = 2 >= 2 = mark(geq(X,Y))
       
       active(div(0(),s(Y))) = 1 >= 1 = mark(0())
       
       active(div(s(X),s(Y))) = 1 >= 1 = mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
       
       active(if(true(),X,Y)) = X + Y + 1 >= X + 1 = mark(X)
       
       active(if(false(),X,Y)) = X + Y + 1 >= Y + 1 = mark(Y)
       
       mark(minus(X1,X2)) = 1 >= 1 = active(minus(X1,X2))
       
       mark(0()) = 1 >= 1 = active(0())
       
       mark(s(X)) = 1 >= 1 = active(s(mark(X)))
       
       mark(geq(X1,X2)) = 2 >= 2 = active(geq(X1,X2))
       
       mark(true()) = 2 >= 2 = active(true())
       
       mark(false()) = 2 >= 2 = active(false())
       
       mark(div(X1,X2)) = 1 >= 1 = active(div(mark(X1),X2))
       
       mark(if(X1,X2,X3)) = X2 + X3 + 1 >= X2 + X3 + 1 = active(if(mark(X1),X2,X3))
       
       minus(mark(X1),X2) = 0 >= 0 = minus(X1,X2)
       
       minus(X1,mark(X2)) = 0 >= 0 = minus(X1,X2)
       
       minus(active(X1),X2) = 0 >= 0 = minus(X1,X2)
       
       minus(X1,active(X2)) = 0 >= 0 = minus(X1,X2)
       
       s(mark(X)) = 0 >= 0 = s(X)
       
       s(active(X)) = 0 >= 0 = s(X)
       
       geq(mark(X1),X2) = 1 >= 1 = geq(X1,X2)
       
       geq(X1,mark(X2)) = 1 >= 1 = geq(X1,X2)
       
       geq(active(X1),X2) = 1 >= 1 = geq(X1,X2)
       
       geq(X1,active(X2)) = 1 >= 1 = geq(X1,X2)
       
       div(mark(X1),X2) = 0 >= 0 = div(X1,X2)
       
       div(X1,mark(X2)) = 0 >= 0 = div(X1,X2)
       
       div(active(X1),X2) = 0 >= 0 = div(X1,X2)
       
       div(X1,active(X2)) = 0 >= 0 = div(X1,X2)
       
       if(mark(X1),X2,X3) = X2 + X3 >= X2 + X3 = if(X1,X2,X3)
       
       if(X1,mark(X2),X3) = X2 + X3 + 1 >= X2 + X3 = if(X1,X2,X3)
       
       if(X1,X2,mark(X3)) = X2 + X3 + 1 >= X2 + X3 = if(X1,X2,X3)
       
       if(active(X1),X2,X3) = X2 + X3 >= X2 + X3 = if(X1,X2,X3)
       
       if(X1,active(X2),X3) = X2 + X3 + 1 >= X2 + X3 = if(X1,X2,X3)
       
       if(X1,X2,active(X3)) = X2 + X3 + 1 >= X2 + X3 = if(X1,X2,X3)
      problem:
       DPs:
        
       TRS:
        active(minus(0(),Y)) -> mark(0())
        active(minus(s(X),s(Y))) -> mark(minus(X,Y))
        active(geq(X,0())) -> mark(true())
        active(geq(0(),s(Y))) -> mark(false())
        active(geq(s(X),s(Y))) -> mark(geq(X,Y))
        active(div(0(),s(Y))) -> mark(0())
        active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
        active(if(true(),X,Y)) -> mark(X)
        active(if(false(),X,Y)) -> mark(Y)
        mark(minus(X1,X2)) -> active(minus(X1,X2))
        mark(0()) -> active(0())
        mark(s(X)) -> active(s(mark(X)))
        mark(geq(X1,X2)) -> active(geq(X1,X2))
        mark(true()) -> active(true())
        mark(false()) -> active(false())
        mark(div(X1,X2)) -> active(div(mark(X1),X2))
        mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
        minus(mark(X1),X2) -> minus(X1,X2)
        minus(X1,mark(X2)) -> minus(X1,X2)
        minus(active(X1),X2) -> minus(X1,X2)
        minus(X1,active(X2)) -> minus(X1,X2)
        s(mark(X)) -> s(X)
        s(active(X)) -> s(X)
        geq(mark(X1),X2) -> geq(X1,X2)
        geq(X1,mark(X2)) -> geq(X1,X2)
        geq(active(X1),X2) -> geq(X1,X2)
        geq(X1,active(X2)) -> geq(X1,X2)
        div(mark(X1),X2) -> div(X1,X2)
        div(X1,mark(X2)) -> div(X1,X2)
        div(active(X1),X2) -> div(X1,X2)
        div(X1,active(X2)) -> div(X1,X2)
        if(mark(X1),X2,X3) -> if(X1,X2,X3)
        if(X1,mark(X2),X3) -> if(X1,X2,X3)
        if(X1,X2,mark(X3)) -> if(X1,X2,X3)
        if(active(X1),X2,X3) -> if(X1,X2,X3)
        if(X1,active(X2),X3) -> if(X1,X2,X3)
        if(X1,X2,active(X3)) -> if(X1,X2,X3)
      Qed