MAYBE

Problem:
 minus_active(0(),y) -> 0()
 mark(0()) -> 0()
 minus_active(s(x),s(y)) -> minus_active(x,y)
 mark(s(x)) -> s(mark(x))
 ge_active(x,0()) -> true()
 mark(minus(x,y)) -> minus_active(x,y)
 ge_active(0(),s(y)) -> false()
 mark(ge(x,y)) -> ge_active(x,y)
 ge_active(s(x),s(y)) -> ge_active(x,y)
 mark(div(x,y)) -> div_active(mark(x),y)
 div_active(0(),s(y)) -> 0()
 mark(if(x,y,z)) -> if_active(mark(x),y,z)
 div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0())
 if_active(true(),x,y) -> mark(x)
 minus_active(x,y) -> minus(x,y)
 if_active(false(),x,y) -> mark(y)
 ge_active(x,y) -> ge(x,y)
 if_active(x,y,z) -> if(x,y,z)
 div_active(x,y) -> div(x,y)

Proof:
 DP Processor:
  DPs:
   minus_active#(s(x),s(y)) -> minus_active#(x,y)
   mark#(s(x)) -> mark#(x)
   mark#(minus(x,y)) -> minus_active#(x,y)
   mark#(ge(x,y)) -> ge_active#(x,y)
   ge_active#(s(x),s(y)) -> ge_active#(x,y)
   mark#(div(x,y)) -> mark#(x)
   mark#(div(x,y)) -> div_active#(mark(x),y)
   mark#(if(x,y,z)) -> mark#(x)
   mark#(if(x,y,z)) -> if_active#(mark(x),y,z)
   div_active#(s(x),s(y)) -> ge_active#(x,y)
   div_active#(s(x),s(y)) -> if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0())
   if_active#(true(),x,y) -> mark#(x)
   if_active#(false(),x,y) -> mark#(y)
  TRS:
   minus_active(0(),y) -> 0()
   mark(0()) -> 0()
   minus_active(s(x),s(y)) -> minus_active(x,y)
   mark(s(x)) -> s(mark(x))
   ge_active(x,0()) -> true()
   mark(minus(x,y)) -> minus_active(x,y)
   ge_active(0(),s(y)) -> false()
   mark(ge(x,y)) -> ge_active(x,y)
   ge_active(s(x),s(y)) -> ge_active(x,y)
   mark(div(x,y)) -> div_active(mark(x),y)
   div_active(0(),s(y)) -> 0()
   mark(if(x,y,z)) -> if_active(mark(x),y,z)
   div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0())
   if_active(true(),x,y) -> mark(x)
   minus_active(x,y) -> minus(x,y)
   if_active(false(),x,y) -> mark(y)
   ge_active(x,y) -> ge(x,y)
   if_active(x,y,z) -> if(x,y,z)
   div_active(x,y) -> div(x,y)
  ADG Processor:
   DPs:
    minus_active#(s(x),s(y)) -> minus_active#(x,y)
    mark#(s(x)) -> mark#(x)
    mark#(minus(x,y)) -> minus_active#(x,y)
    mark#(ge(x,y)) -> ge_active#(x,y)
    ge_active#(s(x),s(y)) -> ge_active#(x,y)
    mark#(div(x,y)) -> mark#(x)
    mark#(div(x,y)) -> div_active#(mark(x),y)
    mark#(if(x,y,z)) -> mark#(x)
    mark#(if(x,y,z)) -> if_active#(mark(x),y,z)
    div_active#(s(x),s(y)) -> ge_active#(x,y)
    div_active#(s(x),s(y)) -> if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0())
    if_active#(true(),x,y) -> mark#(x)
    if_active#(false(),x,y) -> mark#(y)
   TRS:
    minus_active(0(),y) -> 0()
    mark(0()) -> 0()
    minus_active(s(x),s(y)) -> minus_active(x,y)
    mark(s(x)) -> s(mark(x))
    ge_active(x,0()) -> true()
    mark(minus(x,y)) -> minus_active(x,y)
    ge_active(0(),s(y)) -> false()
    mark(ge(x,y)) -> ge_active(x,y)
    ge_active(s(x),s(y)) -> ge_active(x,y)
    mark(div(x,y)) -> div_active(mark(x),y)
    div_active(0(),s(y)) -> 0()
    mark(if(x,y,z)) -> if_active(mark(x),y,z)
    div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0())
    if_active(true(),x,y) -> mark(x)
    minus_active(x,y) -> minus(x,y)
    if_active(false(),x,y) -> mark(y)
    ge_active(x,y) -> ge(x,y)
    if_active(x,y,z) -> if(x,y,z)
    div_active(x,y) -> div(x,y)
   graph:
    if_active#(false(),x,y) -> mark#(y) ->
    mark#(s(x)) -> mark#(x)
    if_active#(false(),x,y) -> mark#(y) ->
    mark#(minus(x,y)) -> minus_active#(x,y)
    if_active#(false(),x,y) -> mark#(y) ->
    mark#(ge(x,y)) -> ge_active#(x,y)
    if_active#(false(),x,y) -> mark#(y) ->
    mark#(div(x,y)) -> mark#(x)
    if_active#(false(),x,y) -> mark#(y) ->
    mark#(div(x,y)) -> div_active#(mark(x),y)
    if_active#(false(),x,y) -> mark#(y) ->
    mark#(if(x,y,z)) -> mark#(x)
    if_active#(false(),x,y) -> mark#(y) ->
    mark#(if(x,y,z)) -> if_active#(mark(x),y,z)
    if_active#(true(),x,y) -> mark#(x) -> mark#(s(x)) -> mark#(x)
    if_active#(true(),x,y) -> mark#(x) ->
    mark#(minus(x,y)) -> minus_active#(x,y)
    if_active#(true(),x,y) -> mark#(x) ->
    mark#(ge(x,y)) -> ge_active#(x,y)
    if_active#(true(),x,y) -> mark#(x) ->
    mark#(div(x,y)) -> mark#(x)
    if_active#(true(),x,y) -> mark#(x) ->
    mark#(div(x,y)) -> div_active#(mark(x),y)
    if_active#(true(),x,y) -> mark#(x) ->
    mark#(if(x,y,z)) -> mark#(x)
    if_active#(true(),x,y) -> mark#(x) ->
    mark#(if(x,y,z)) -> if_active#(mark(x),y,z)
    div_active#(s(x),s(y)) -> if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()) ->
    if_active#(true(),x,y) -> mark#(x)
    div_active#(s(x),s(y)) -> if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()) ->
    if_active#(false(),x,y) -> mark#(y)
    div_active#(s(x),s(y)) -> ge_active#(x,y) ->
    ge_active#(s(x),s(y)) -> ge_active#(x,y)
    ge_active#(s(x),s(y)) -> ge_active#(x,y) ->
    ge_active#(s(x),s(y)) -> ge_active#(x,y)
    mark#(if(x,y,z)) -> if_active#(mark(x),y,z) ->
    if_active#(true(),x,y) -> mark#(x)
    mark#(if(x,y,z)) -> if_active#(mark(x),y,z) ->
    if_active#(false(),x,y) -> mark#(y)
    mark#(if(x,y,z)) -> mark#(x) -> mark#(s(x)) -> mark#(x)
    mark#(if(x,y,z)) -> mark#(x) ->
    mark#(minus(x,y)) -> minus_active#(x,y)
    mark#(if(x,y,z)) -> mark#(x) -> mark#(ge(x,y)) -> ge_active#(x,y)
    mark#(if(x,y,z)) -> mark#(x) -> mark#(div(x,y)) -> mark#(x)
    mark#(if(x,y,z)) -> mark#(x) ->
    mark#(div(x,y)) -> div_active#(mark(x),y)
    mark#(if(x,y,z)) -> mark#(x) -> mark#(if(x,y,z)) -> mark#(x)
    mark#(if(x,y,z)) -> mark#(x) ->
    mark#(if(x,y,z)) -> if_active#(mark(x),y,z)
    mark#(div(x,y)) -> div_active#(mark(x),y) ->
    div_active#(s(x),s(y)) -> ge_active#(x,y)
    mark#(div(x,y)) -> div_active#(mark(x),y) ->
    div_active#(s(x),s(y)) -> if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0())
    mark#(div(x,y)) -> mark#(x) -> mark#(s(x)) -> mark#(x)
    mark#(div(x,y)) -> mark#(x) ->
    mark#(minus(x,y)) -> minus_active#(x,y)
    mark#(div(x,y)) -> mark#(x) -> mark#(ge(x,y)) -> ge_active#(x,y)
    mark#(div(x,y)) -> mark#(x) -> mark#(div(x,y)) -> mark#(x)
    mark#(div(x,y)) -> mark#(x) ->
    mark#(div(x,y)) -> div_active#(mark(x),y)
    mark#(div(x,y)) -> mark#(x) -> mark#(if(x,y,z)) -> mark#(x)
    mark#(div(x,y)) -> mark#(x) ->
    mark#(if(x,y,z)) -> if_active#(mark(x),y,z)
    mark#(ge(x,y)) -> ge_active#(x,y) ->
    ge_active#(s(x),s(y)) -> ge_active#(x,y)
    mark#(minus(x,y)) -> minus_active#(x,y) ->
    minus_active#(s(x),s(y)) -> minus_active#(x,y)
    mark#(s(x)) -> mark#(x) -> mark#(s(x)) -> mark#(x)
    mark#(s(x)) -> mark#(x) -> mark#(minus(x,y)) -> minus_active#(x,y)
    mark#(s(x)) -> mark#(x) -> mark#(ge(x,y)) -> ge_active#(x,y)
    mark#(s(x)) -> mark#(x) -> mark#(div(x,y)) -> mark#(x)
    mark#(s(x)) -> mark#(x) -> mark#(div(x,y)) -> div_active#(mark(x),y)
    mark#(s(x)) -> mark#(x) -> mark#(if(x,y,z)) -> mark#(x)
    mark#(s(x)) -> mark#(x) ->
    mark#(if(x,y,z)) -> if_active#(mark(x),y,z)
    minus_active#(s(x),s(y)) -> minus_active#(x,y) ->
    minus_active#(s(x),s(y)) -> minus_active#(x,y)
   Restore Modifier:
    DPs:
     minus_active#(s(x),s(y)) -> minus_active#(x,y)
     mark#(s(x)) -> mark#(x)
     mark#(minus(x,y)) -> minus_active#(x,y)
     mark#(ge(x,y)) -> ge_active#(x,y)
     ge_active#(s(x),s(y)) -> ge_active#(x,y)
     mark#(div(x,y)) -> mark#(x)
     mark#(div(x,y)) -> div_active#(mark(x),y)
     mark#(if(x,y,z)) -> mark#(x)
     mark#(if(x,y,z)) -> if_active#(mark(x),y,z)
     div_active#(s(x),s(y)) -> ge_active#(x,y)
     div_active#(s(x),s(y)) -> if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0())
     if_active#(true(),x,y) -> mark#(x)
     if_active#(false(),x,y) -> mark#(y)
    TRS:
     minus_active(0(),y) -> 0()
     mark(0()) -> 0()
     minus_active(s(x),s(y)) -> minus_active(x,y)
     mark(s(x)) -> s(mark(x))
     ge_active(x,0()) -> true()
     mark(minus(x,y)) -> minus_active(x,y)
     ge_active(0(),s(y)) -> false()
     mark(ge(x,y)) -> ge_active(x,y)
     ge_active(s(x),s(y)) -> ge_active(x,y)
     mark(div(x,y)) -> div_active(mark(x),y)
     div_active(0(),s(y)) -> 0()
     mark(if(x,y,z)) -> if_active(mark(x),y,z)
     div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0())
     if_active(true(),x,y) -> mark(x)
     minus_active(x,y) -> minus(x,y)
     if_active(false(),x,y) -> mark(y)
     ge_active(x,y) -> ge(x,y)
     if_active(x,y,z) -> if(x,y,z)
     div_active(x,y) -> div(x,y)
    SCC Processor:
     #sccs: 3
     #rules: 10
     #arcs: 46/169
     DPs:
      if_active#(false(),x,y) -> mark#(y)
      mark#(if(x,y,z)) -> if_active#(mark(x),y,z)
      if_active#(true(),x,y) -> mark#(x)
      mark#(if(x,y,z)) -> mark#(x)
      mark#(div(x,y)) -> div_active#(mark(x),y)
      div_active#(s(x),s(y)) -> if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0())
      mark#(div(x,y)) -> mark#(x)
      mark#(s(x)) -> mark#(x)
     TRS:
      minus_active(0(),y) -> 0()
      mark(0()) -> 0()
      minus_active(s(x),s(y)) -> minus_active(x,y)
      mark(s(x)) -> s(mark(x))
      ge_active(x,0()) -> true()
      mark(minus(x,y)) -> minus_active(x,y)
      ge_active(0(),s(y)) -> false()
      mark(ge(x,y)) -> ge_active(x,y)
      ge_active(s(x),s(y)) -> ge_active(x,y)
      mark(div(x,y)) -> div_active(mark(x),y)
      div_active(0(),s(y)) -> 0()
      mark(if(x,y,z)) -> if_active(mark(x),y,z)
      div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0())
      if_active(true(),x,y) -> mark(x)
      minus_active(x,y) -> minus(x,y)
      if_active(false(),x,y) -> mark(y)
      ge_active(x,y) -> ge(x,y)
      if_active(x,y,z) -> if(x,y,z)
      div_active(x,y) -> div(x,y)
     Open
     
     DPs:
      minus_active#(s(x),s(y)) -> minus_active#(x,y)
     TRS:
      minus_active(0(),y) -> 0()
      mark(0()) -> 0()
      minus_active(s(x),s(y)) -> minus_active(x,y)
      mark(s(x)) -> s(mark(x))
      ge_active(x,0()) -> true()
      mark(minus(x,y)) -> minus_active(x,y)
      ge_active(0(),s(y)) -> false()
      mark(ge(x,y)) -> ge_active(x,y)
      ge_active(s(x),s(y)) -> ge_active(x,y)
      mark(div(x,y)) -> div_active(mark(x),y)
      div_active(0(),s(y)) -> 0()
      mark(if(x,y,z)) -> if_active(mark(x),y,z)
      div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0())
      if_active(true(),x,y) -> mark(x)
      minus_active(x,y) -> minus(x,y)
      if_active(false(),x,y) -> mark(y)
      ge_active(x,y) -> ge(x,y)
      if_active(x,y,z) -> if(x,y,z)
      div_active(x,y) -> div(x,y)
     Open
     
     DPs:
      ge_active#(s(x),s(y)) -> ge_active#(x,y)
     TRS:
      minus_active(0(),y) -> 0()
      mark(0()) -> 0()
      minus_active(s(x),s(y)) -> minus_active(x,y)
      mark(s(x)) -> s(mark(x))
      ge_active(x,0()) -> true()
      mark(minus(x,y)) -> minus_active(x,y)
      ge_active(0(),s(y)) -> false()
      mark(ge(x,y)) -> ge_active(x,y)
      ge_active(s(x),s(y)) -> ge_active(x,y)
      mark(div(x,y)) -> div_active(mark(x),y)
      div_active(0(),s(y)) -> 0()
      mark(if(x,y,z)) -> if_active(mark(x),y,z)
      div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0())
      if_active(true(),x,y) -> mark(x)
      minus_active(x,y) -> minus(x,y)
      if_active(false(),x,y) -> mark(y)
      ge_active(x,y) -> ge(x,y)
      if_active(x,y,z) -> if(x,y,z)
      div_active(x,y) -> div(x,y)
     Open