YES

Problem:
 active(and(true(),X)) -> mark(X)
 active(and(false(),Y)) -> mark(false())
 active(if(true(),X,Y)) -> mark(X)
 active(if(false(),X,Y)) -> mark(Y)
 active(add(0(),X)) -> mark(X)
 active(add(s(X),Y)) -> mark(s(add(X,Y)))
 active(first(0(),X)) -> mark(nil())
 active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
 active(from(X)) -> mark(cons(X,from(s(X))))
 mark(and(X1,X2)) -> active(and(mark(X1),X2))
 mark(true()) -> active(true())
 mark(false()) -> active(false())
 mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
 mark(add(X1,X2)) -> active(add(mark(X1),X2))
 mark(0()) -> active(0())
 mark(s(X)) -> active(s(X))
 mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
 mark(nil()) -> active(nil())
 mark(cons(X1,X2)) -> active(cons(X1,X2))
 mark(from(X)) -> active(from(X))
 and(mark(X1),X2) -> and(X1,X2)
 and(X1,mark(X2)) -> and(X1,X2)
 and(active(X1),X2) -> and(X1,X2)
 and(X1,active(X2)) -> and(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)
 add(mark(X1),X2) -> add(X1,X2)
 add(X1,mark(X2)) -> add(X1,X2)
 add(active(X1),X2) -> add(X1,X2)
 add(X1,active(X2)) -> add(X1,X2)
 s(mark(X)) -> s(X)
 s(active(X)) -> s(X)
 first(mark(X1),X2) -> first(X1,X2)
 first(X1,mark(X2)) -> first(X1,X2)
 first(active(X1),X2) -> first(X1,X2)
 first(X1,active(X2)) -> first(X1,X2)
 cons(mark(X1),X2) -> cons(X1,X2)
 cons(X1,mark(X2)) -> cons(X1,X2)
 cons(active(X1),X2) -> cons(X1,X2)
 cons(X1,active(X2)) -> cons(X1,X2)
 from(mark(X)) -> from(X)
 from(active(X)) -> from(X)

Proof:
 DP Processor:
  DPs:
   active#(and(true(),X)) -> mark#(X)
   active#(and(false(),Y)) -> mark#(false())
   active#(if(true(),X,Y)) -> mark#(X)
   active#(if(false(),X,Y)) -> mark#(Y)
   active#(add(0(),X)) -> mark#(X)
   active#(add(s(X),Y)) -> add#(X,Y)
   active#(add(s(X),Y)) -> s#(add(X,Y))
   active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
   active#(first(0(),X)) -> mark#(nil())
   active#(first(s(X),cons(Y,Z))) -> first#(X,Z)
   active#(first(s(X),cons(Y,Z))) -> cons#(Y,first(X,Z))
   active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z)))
   active#(from(X)) -> s#(X)
   active#(from(X)) -> from#(s(X))
   active#(from(X)) -> cons#(X,from(s(X)))
   active#(from(X)) -> mark#(cons(X,from(s(X))))
   mark#(and(X1,X2)) -> mark#(X1)
   mark#(and(X1,X2)) -> and#(mark(X1),X2)
   mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
   mark#(true()) -> active#(true())
   mark#(false()) -> active#(false())
   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))
   mark#(add(X1,X2)) -> mark#(X1)
   mark#(add(X1,X2)) -> add#(mark(X1),X2)
   mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
   mark#(0()) -> active#(0())
   mark#(s(X)) -> active#(s(X))
   mark#(first(X1,X2)) -> mark#(X2)
   mark#(first(X1,X2)) -> mark#(X1)
   mark#(first(X1,X2)) -> first#(mark(X1),mark(X2))
   mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
   mark#(nil()) -> active#(nil())
   mark#(cons(X1,X2)) -> active#(cons(X1,X2))
   mark#(from(X)) -> active#(from(X))
   and#(mark(X1),X2) -> and#(X1,X2)
   and#(X1,mark(X2)) -> and#(X1,X2)
   and#(active(X1),X2) -> and#(X1,X2)
   and#(X1,active(X2)) -> and#(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)
   add#(mark(X1),X2) -> add#(X1,X2)
   add#(X1,mark(X2)) -> add#(X1,X2)
   add#(active(X1),X2) -> add#(X1,X2)
   add#(X1,active(X2)) -> add#(X1,X2)
   s#(mark(X)) -> s#(X)
   s#(active(X)) -> s#(X)
   first#(mark(X1),X2) -> first#(X1,X2)
   first#(X1,mark(X2)) -> first#(X1,X2)
   first#(active(X1),X2) -> first#(X1,X2)
   first#(X1,active(X2)) -> first#(X1,X2)
   cons#(mark(X1),X2) -> cons#(X1,X2)
   cons#(X1,mark(X2)) -> cons#(X1,X2)
   cons#(active(X1),X2) -> cons#(X1,X2)
   cons#(X1,active(X2)) -> cons#(X1,X2)
   from#(mark(X)) -> from#(X)
   from#(active(X)) -> from#(X)
  TRS:
   active(and(true(),X)) -> mark(X)
   active(and(false(),Y)) -> mark(false())
   active(if(true(),X,Y)) -> mark(X)
   active(if(false(),X,Y)) -> mark(Y)
   active(add(0(),X)) -> mark(X)
   active(add(s(X),Y)) -> mark(s(add(X,Y)))
   active(first(0(),X)) -> mark(nil())
   active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
   active(from(X)) -> mark(cons(X,from(s(X))))
   mark(and(X1,X2)) -> active(and(mark(X1),X2))
   mark(true()) -> active(true())
   mark(false()) -> active(false())
   mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
   mark(add(X1,X2)) -> active(add(mark(X1),X2))
   mark(0()) -> active(0())
   mark(s(X)) -> active(s(X))
   mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
   mark(nil()) -> active(nil())
   mark(cons(X1,X2)) -> active(cons(X1,X2))
   mark(from(X)) -> active(from(X))
   and(mark(X1),X2) -> and(X1,X2)
   and(X1,mark(X2)) -> and(X1,X2)
   and(active(X1),X2) -> and(X1,X2)
   and(X1,active(X2)) -> and(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)
   add(mark(X1),X2) -> add(X1,X2)
   add(X1,mark(X2)) -> add(X1,X2)
   add(active(X1),X2) -> add(X1,X2)
   add(X1,active(X2)) -> add(X1,X2)
   s(mark(X)) -> s(X)
   s(active(X)) -> s(X)
   first(mark(X1),X2) -> first(X1,X2)
   first(X1,mark(X2)) -> first(X1,X2)
   first(active(X1),X2) -> first(X1,X2)
   first(X1,active(X2)) -> first(X1,X2)
   cons(mark(X1),X2) -> cons(X1,X2)
   cons(X1,mark(X2)) -> cons(X1,X2)
   cons(active(X1),X2) -> cons(X1,X2)
   cons(X1,active(X2)) -> cons(X1,X2)
   from(mark(X)) -> from(X)
   from(active(X)) -> from(X)
  TDG Processor:
   DPs:
    active#(and(true(),X)) -> mark#(X)
    active#(and(false(),Y)) -> mark#(false())
    active#(if(true(),X,Y)) -> mark#(X)
    active#(if(false(),X,Y)) -> mark#(Y)
    active#(add(0(),X)) -> mark#(X)
    active#(add(s(X),Y)) -> add#(X,Y)
    active#(add(s(X),Y)) -> s#(add(X,Y))
    active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
    active#(first(0(),X)) -> mark#(nil())
    active#(first(s(X),cons(Y,Z))) -> first#(X,Z)
    active#(first(s(X),cons(Y,Z))) -> cons#(Y,first(X,Z))
    active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z)))
    active#(from(X)) -> s#(X)
    active#(from(X)) -> from#(s(X))
    active#(from(X)) -> cons#(X,from(s(X)))
    active#(from(X)) -> mark#(cons(X,from(s(X))))
    mark#(and(X1,X2)) -> mark#(X1)
    mark#(and(X1,X2)) -> and#(mark(X1),X2)
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    mark#(true()) -> active#(true())
    mark#(false()) -> active#(false())
    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))
    mark#(add(X1,X2)) -> mark#(X1)
    mark#(add(X1,X2)) -> add#(mark(X1),X2)
    mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
    mark#(0()) -> active#(0())
    mark#(s(X)) -> active#(s(X))
    mark#(first(X1,X2)) -> mark#(X2)
    mark#(first(X1,X2)) -> mark#(X1)
    mark#(first(X1,X2)) -> first#(mark(X1),mark(X2))
    mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
    mark#(nil()) -> active#(nil())
    mark#(cons(X1,X2)) -> active#(cons(X1,X2))
    mark#(from(X)) -> active#(from(X))
    and#(mark(X1),X2) -> and#(X1,X2)
    and#(X1,mark(X2)) -> and#(X1,X2)
    and#(active(X1),X2) -> and#(X1,X2)
    and#(X1,active(X2)) -> and#(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)
    add#(mark(X1),X2) -> add#(X1,X2)
    add#(X1,mark(X2)) -> add#(X1,X2)
    add#(active(X1),X2) -> add#(X1,X2)
    add#(X1,active(X2)) -> add#(X1,X2)
    s#(mark(X)) -> s#(X)
    s#(active(X)) -> s#(X)
    first#(mark(X1),X2) -> first#(X1,X2)
    first#(X1,mark(X2)) -> first#(X1,X2)
    first#(active(X1),X2) -> first#(X1,X2)
    first#(X1,active(X2)) -> first#(X1,X2)
    cons#(mark(X1),X2) -> cons#(X1,X2)
    cons#(X1,mark(X2)) -> cons#(X1,X2)
    cons#(active(X1),X2) -> cons#(X1,X2)
    cons#(X1,active(X2)) -> cons#(X1,X2)
    from#(mark(X)) -> from#(X)
    from#(active(X)) -> from#(X)
   TRS:
    active(and(true(),X)) -> mark(X)
    active(and(false(),Y)) -> mark(false())
    active(if(true(),X,Y)) -> mark(X)
    active(if(false(),X,Y)) -> mark(Y)
    active(add(0(),X)) -> mark(X)
    active(add(s(X),Y)) -> mark(s(add(X,Y)))
    active(first(0(),X)) -> mark(nil())
    active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
    active(from(X)) -> mark(cons(X,from(s(X))))
    mark(and(X1,X2)) -> active(and(mark(X1),X2))
    mark(true()) -> active(true())
    mark(false()) -> active(false())
    mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
    mark(add(X1,X2)) -> active(add(mark(X1),X2))
    mark(0()) -> active(0())
    mark(s(X)) -> active(s(X))
    mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
    mark(nil()) -> active(nil())
    mark(cons(X1,X2)) -> active(cons(X1,X2))
    mark(from(X)) -> active(from(X))
    and(mark(X1),X2) -> and(X1,X2)
    and(X1,mark(X2)) -> and(X1,X2)
    and(active(X1),X2) -> and(X1,X2)
    and(X1,active(X2)) -> and(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)
    add(mark(X1),X2) -> add(X1,X2)
    add(X1,mark(X2)) -> add(X1,X2)
    add(active(X1),X2) -> add(X1,X2)
    add(X1,active(X2)) -> add(X1,X2)
    s(mark(X)) -> s(X)
    s(active(X)) -> s(X)
    first(mark(X1),X2) -> first(X1,X2)
    first(X1,mark(X2)) -> first(X1,X2)
    first(active(X1),X2) -> first(X1,X2)
    first(X1,active(X2)) -> first(X1,X2)
    cons(mark(X1),X2) -> cons(X1,X2)
    cons(X1,mark(X2)) -> cons(X1,X2)
    cons(active(X1),X2) -> cons(X1,X2)
    cons(X1,active(X2)) -> cons(X1,X2)
    from(mark(X)) -> from(X)
    from(active(X)) -> from(X)
   graph:
    if#(mark(X1),X2,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,active(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#(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#(X1,mark(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#(active(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,active(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#(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#(X1,mark(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,mark(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,active(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,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#(X1,mark(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,active(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,active(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,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#(X1,mark(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,mark(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,active(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,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#(X1,mark(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#(X1,X2,active(X3)) -> if#(X1,X2,X3) ->
    if#(X1,X2,active(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#(active(X1),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#(X1,mark(X2),X3) -> if#(X1,X2,X3)
    if#(X1,X2,active(X3)) -> if#(X1,X2,X3) ->
    if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
    and#(mark(X1),X2) -> and#(X1,X2) ->
    and#(X1,active(X2)) -> and#(X1,X2)
    and#(mark(X1),X2) -> and#(X1,X2) ->
    and#(active(X1),X2) -> and#(X1,X2)
    and#(mark(X1),X2) -> and#(X1,X2) ->
    and#(X1,mark(X2)) -> and#(X1,X2)
    and#(mark(X1),X2) -> and#(X1,X2) ->
    and#(mark(X1),X2) -> and#(X1,X2)
    and#(active(X1),X2) -> and#(X1,X2) ->
    and#(X1,active(X2)) -> and#(X1,X2)
    and#(active(X1),X2) -> and#(X1,X2) ->
    and#(active(X1),X2) -> and#(X1,X2)
    and#(active(X1),X2) -> and#(X1,X2) ->
    and#(X1,mark(X2)) -> and#(X1,X2)
    and#(active(X1),X2) -> and#(X1,X2) ->
    and#(mark(X1),X2) -> and#(X1,X2)
    and#(X1,mark(X2)) -> and#(X1,X2) ->
    and#(X1,active(X2)) -> and#(X1,X2)
    and#(X1,mark(X2)) -> and#(X1,X2) ->
    and#(active(X1),X2) -> and#(X1,X2)
    and#(X1,mark(X2)) -> and#(X1,X2) ->
    and#(X1,mark(X2)) -> and#(X1,X2)
    and#(X1,mark(X2)) -> and#(X1,X2) ->
    and#(mark(X1),X2) -> and#(X1,X2)
    and#(X1,active(X2)) -> and#(X1,X2) ->
    and#(X1,active(X2)) -> and#(X1,X2)
    and#(X1,active(X2)) -> and#(X1,X2) ->
    and#(active(X1),X2) -> and#(X1,X2)
    and#(X1,active(X2)) -> and#(X1,X2) ->
    and#(X1,mark(X2)) -> and#(X1,X2)
    and#(X1,active(X2)) -> and#(X1,X2) ->
    and#(mark(X1),X2) -> and#(X1,X2)
    from#(mark(X)) -> from#(X) -> from#(active(X)) -> from#(X)
    from#(mark(X)) -> from#(X) -> from#(mark(X)) -> from#(X)
    from#(active(X)) -> from#(X) -> from#(active(X)) -> from#(X)
    from#(active(X)) -> from#(X) -> from#(mark(X)) -> from#(X)
    cons#(mark(X1),X2) -> cons#(X1,X2) ->
    cons#(X1,active(X2)) -> cons#(X1,X2)
    cons#(mark(X1),X2) -> cons#(X1,X2) ->
    cons#(active(X1),X2) -> cons#(X1,X2)
    cons#(mark(X1),X2) -> cons#(X1,X2) ->
    cons#(X1,mark(X2)) -> cons#(X1,X2)
    cons#(mark(X1),X2) -> cons#(X1,X2) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    cons#(active(X1),X2) -> cons#(X1,X2) ->
    cons#(X1,active(X2)) -> cons#(X1,X2)
    cons#(active(X1),X2) -> cons#(X1,X2) ->
    cons#(active(X1),X2) -> cons#(X1,X2)
    cons#(active(X1),X2) -> cons#(X1,X2) ->
    cons#(X1,mark(X2)) -> cons#(X1,X2)
    cons#(active(X1),X2) -> cons#(X1,X2) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    cons#(X1,mark(X2)) -> cons#(X1,X2) ->
    cons#(X1,active(X2)) -> cons#(X1,X2)
    cons#(X1,mark(X2)) -> cons#(X1,X2) ->
    cons#(active(X1),X2) -> cons#(X1,X2)
    cons#(X1,mark(X2)) -> cons#(X1,X2) ->
    cons#(X1,mark(X2)) -> cons#(X1,X2)
    cons#(X1,mark(X2)) -> cons#(X1,X2) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    cons#(X1,active(X2)) -> cons#(X1,X2) ->
    cons#(X1,active(X2)) -> cons#(X1,X2)
    cons#(X1,active(X2)) -> cons#(X1,X2) ->
    cons#(active(X1),X2) -> cons#(X1,X2)
    cons#(X1,active(X2)) -> cons#(X1,X2) ->
    cons#(X1,mark(X2)) -> cons#(X1,X2)
    cons#(X1,active(X2)) -> cons#(X1,X2) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    first#(mark(X1),X2) -> first#(X1,X2) ->
    first#(X1,active(X2)) -> first#(X1,X2)
    first#(mark(X1),X2) -> first#(X1,X2) ->
    first#(active(X1),X2) -> first#(X1,X2)
    first#(mark(X1),X2) -> first#(X1,X2) ->
    first#(X1,mark(X2)) -> first#(X1,X2)
    first#(mark(X1),X2) -> first#(X1,X2) ->
    first#(mark(X1),X2) -> first#(X1,X2)
    first#(active(X1),X2) -> first#(X1,X2) ->
    first#(X1,active(X2)) -> first#(X1,X2)
    first#(active(X1),X2) -> first#(X1,X2) ->
    first#(active(X1),X2) -> first#(X1,X2)
    first#(active(X1),X2) -> first#(X1,X2) ->
    first#(X1,mark(X2)) -> first#(X1,X2)
    first#(active(X1),X2) -> first#(X1,X2) ->
    first#(mark(X1),X2) -> first#(X1,X2)
    first#(X1,mark(X2)) -> first#(X1,X2) ->
    first#(X1,active(X2)) -> first#(X1,X2)
    first#(X1,mark(X2)) -> first#(X1,X2) ->
    first#(active(X1),X2) -> first#(X1,X2)
    first#(X1,mark(X2)) -> first#(X1,X2) ->
    first#(X1,mark(X2)) -> first#(X1,X2)
    first#(X1,mark(X2)) -> first#(X1,X2) ->
    first#(mark(X1),X2) -> first#(X1,X2)
    first#(X1,active(X2)) -> first#(X1,X2) ->
    first#(X1,active(X2)) -> first#(X1,X2)
    first#(X1,active(X2)) -> first#(X1,X2) ->
    first#(active(X1),X2) -> first#(X1,X2)
    first#(X1,active(X2)) -> first#(X1,X2) ->
    first#(X1,mark(X2)) -> first#(X1,X2)
    first#(X1,active(X2)) -> first#(X1,X2) ->
    first#(mark(X1),X2) -> first#(X1,X2)
    s#(mark(X)) -> s#(X) -> s#(active(X)) -> s#(X)
    s#(mark(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
    s#(active(X)) -> s#(X) -> s#(active(X)) -> s#(X)
    s#(active(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
    add#(mark(X1),X2) -> add#(X1,X2) ->
    add#(X1,active(X2)) -> add#(X1,X2)
    add#(mark(X1),X2) -> add#(X1,X2) ->
    add#(active(X1),X2) -> add#(X1,X2)
    add#(mark(X1),X2) -> add#(X1,X2) ->
    add#(X1,mark(X2)) -> add#(X1,X2)
    add#(mark(X1),X2) -> add#(X1,X2) ->
    add#(mark(X1),X2) -> add#(X1,X2)
    add#(active(X1),X2) -> add#(X1,X2) ->
    add#(X1,active(X2)) -> add#(X1,X2)
    add#(active(X1),X2) -> add#(X1,X2) ->
    add#(active(X1),X2) -> add#(X1,X2)
    add#(active(X1),X2) -> add#(X1,X2) ->
    add#(X1,mark(X2)) -> add#(X1,X2)
    add#(active(X1),X2) -> add#(X1,X2) ->
    add#(mark(X1),X2) -> add#(X1,X2)
    add#(X1,mark(X2)) -> add#(X1,X2) ->
    add#(X1,active(X2)) -> add#(X1,X2)
    add#(X1,mark(X2)) -> add#(X1,X2) ->
    add#(active(X1),X2) -> add#(X1,X2)
    add#(X1,mark(X2)) -> add#(X1,X2) ->
    add#(X1,mark(X2)) -> add#(X1,X2)
    add#(X1,mark(X2)) -> add#(X1,X2) ->
    add#(mark(X1),X2) -> add#(X1,X2)
    add#(X1,active(X2)) -> add#(X1,X2) ->
    add#(X1,active(X2)) -> add#(X1,X2)
    add#(X1,active(X2)) -> add#(X1,X2) ->
    add#(active(X1),X2) -> add#(X1,X2)
    add#(X1,active(X2)) -> add#(X1,X2) ->
    add#(X1,mark(X2)) -> add#(X1,X2)
    add#(X1,active(X2)) -> add#(X1,X2) ->
    add#(mark(X1),X2) -> add#(X1,X2)
    mark#(from(X)) -> active#(from(X)) ->
    active#(from(X)) -> mark#(cons(X,from(s(X))))
    mark#(from(X)) -> active#(from(X)) ->
    active#(from(X)) -> cons#(X,from(s(X)))
    mark#(from(X)) -> active#(from(X)) ->
    active#(from(X)) -> from#(s(X))
    mark#(from(X)) -> active#(from(X)) ->
    active#(from(X)) -> s#(X)
    mark#(from(X)) -> active#(from(X)) ->
    active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z)))
    mark#(from(X)) -> active#(from(X)) ->
    active#(first(s(X),cons(Y,Z))) -> cons#(Y,first(X,Z))
    mark#(from(X)) -> active#(from(X)) ->
    active#(first(s(X),cons(Y,Z))) -> first#(X,Z)
    mark#(from(X)) -> active#(from(X)) ->
    active#(first(0(),X)) -> mark#(nil())
    mark#(from(X)) -> active#(from(X)) ->
    active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
    mark#(from(X)) -> active#(from(X)) ->
    active#(add(s(X),Y)) -> s#(add(X,Y))
    mark#(from(X)) -> active#(from(X)) ->
    active#(add(s(X),Y)) -> add#(X,Y)
    mark#(from(X)) -> active#(from(X)) ->
    active#(add(0(),X)) -> mark#(X)
    mark#(from(X)) -> active#(from(X)) ->
    active#(if(false(),X,Y)) -> mark#(Y)
    mark#(from(X)) -> active#(from(X)) ->
    active#(if(true(),X,Y)) -> mark#(X)
    mark#(from(X)) -> active#(from(X)) ->
    active#(and(false(),Y)) -> mark#(false())
    mark#(from(X)) -> active#(from(X)) ->
    active#(and(true(),X)) -> mark#(X)
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(from(X)) -> mark#(cons(X,from(s(X))))
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(from(X)) -> cons#(X,from(s(X)))
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(from(X)) -> from#(s(X))
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(from(X)) -> s#(X)
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z)))
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(first(s(X),cons(Y,Z))) -> cons#(Y,first(X,Z))
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(first(s(X),cons(Y,Z))) -> first#(X,Z)
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(first(0(),X)) -> mark#(nil())
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(add(s(X),Y)) -> s#(add(X,Y))
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(add(s(X),Y)) -> add#(X,Y)
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(add(0(),X)) -> mark#(X)
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(if(false(),X,Y)) -> mark#(Y)
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(if(true(),X,Y)) -> mark#(X)
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(and(false(),Y)) -> mark#(false())
    mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
    active#(and(true(),X)) -> mark#(X)
    mark#(nil()) -> active#(nil()) ->
    active#(from(X)) -> mark#(cons(X,from(s(X))))
    mark#(nil()) -> active#(nil()) ->
    active#(from(X)) -> cons#(X,from(s(X)))
    mark#(nil()) -> active#(nil()) -> active#(from(X)) -> from#(s(X))
    mark#(nil()) -> active#(nil()) -> active#(from(X)) -> s#(X)
    mark#(nil()) -> active#(nil()) ->
    active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z)))
    mark#(nil()) -> active#(nil()) ->
    active#(first(s(X),cons(Y,Z))) -> cons#(Y,first(X,Z))
    mark#(nil()) -> active#(nil()) ->
    active#(first(s(X),cons(Y,Z))) -> first#(X,Z)
    mark#(nil()) -> active#(nil()) ->
    active#(first(0(),X)) -> mark#(nil())
    mark#(nil()) -> active#(nil()) ->
    active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
    mark#(nil()) -> active#(nil()) ->
    active#(add(s(X),Y)) -> s#(add(X,Y))
    mark#(nil()) -> active#(nil()) ->
    active#(add(s(X),Y)) -> add#(X,Y)
    mark#(nil()) -> active#(nil()) -> active#(add(0(),X)) -> mark#(X)
    mark#(nil()) -> active#(nil()) ->
    active#(if(false(),X,Y)) -> mark#(Y)
    mark#(nil()) -> active#(nil()) ->
    active#(if(true(),X,Y)) -> mark#(X)
    mark#(nil()) -> active#(nil()) ->
    active#(and(false(),Y)) -> mark#(false())
    mark#(nil()) -> active#(nil()) ->
    active#(and(true(),X)) -> mark#(X)
    mark#(first(X1,X2)) -> first#(mark(X1),mark(X2)) ->
    first#(X1,active(X2)) -> first#(X1,X2)
    mark#(first(X1,X2)) -> first#(mark(X1),mark(X2)) ->
    first#(active(X1),X2) -> first#(X1,X2)
    mark#(first(X1,X2)) -> first#(mark(X1),mark(X2)) ->
    first#(X1,mark(X2)) -> first#(X1,X2)
    mark#(first(X1,X2)) -> first#(mark(X1),mark(X2)) ->
    first#(mark(X1),X2) -> first#(X1,X2)
    mark#(first(X1,X2)) -> mark#(X2) ->
    mark#(from(X)) -> active#(from(X))
    mark#(first(X1,X2)) -> mark#(X2) ->
    mark#(cons(X1,X2)) -> active#(cons(X1,X2))
    mark#(first(X1,X2)) -> mark#(X2) ->
    mark#(nil()) -> active#(nil())
    mark#(first(X1,X2)) -> mark#(X2) ->
    mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
    mark#(first(X1,X2)) -> mark#(X2) ->
    mark#(first(X1,X2)) -> first#(mark(X1),mark(X2))
    mark#(first(X1,X2)) -> mark#(X2) ->
    mark#(first(X1,X2)) -> mark#(X1)
    mark#(first(X1,X2)) -> mark#(X2) ->
    mark#(first(X1,X2)) -> mark#(X2)
    mark#(first(X1,X2)) -> mark#(X2) ->
    mark#(s(X)) -> active#(s(X))
    mark#(first(X1,X2)) -> mark#(X2) -> mark#(0()) -> active#(0())
    mark#(first(X1,X2)) -> mark#(X2) ->
    mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
    mark#(first(X1,X2)) -> mark#(X2) ->
    mark#(add(X1,X2)) -> add#(mark(X1),X2)
    mark#(first(X1,X2)) -> mark#(X2) ->
    mark#(add(X1,X2)) -> mark#(X1)
    mark#(first(X1,X2)) -> mark#(X2) ->
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
    mark#(first(X1,X2)) -> mark#(X2) ->
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
    mark#(first(X1,X2)) -> mark#(X2) ->
    mark#(if(X1,X2,X3)) -> mark#(X1)
    mark#(first(X1,X2)) -> mark#(X2) ->
    mark#(false()) -> active#(false())
    mark#(first(X1,X2)) -> mark#(X2) ->
    mark#(true()) -> active#(true())
    mark#(first(X1,X2)) -> mark#(X2) ->
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    mark#(first(X1,X2)) -> mark#(X2) ->
    mark#(and(X1,X2)) -> and#(mark(X1),X2)
    mark#(first(X1,X2)) -> mark#(X2) ->
    mark#(and(X1,X2)) -> mark#(X1)
    mark#(first(X1,X2)) -> mark#(X1) ->
    mark#(from(X)) -> active#(from(X))
    mark#(first(X1,X2)) -> mark#(X1) ->
    mark#(cons(X1,X2)) -> active#(cons(X1,X2))
    mark#(first(X1,X2)) -> mark#(X1) ->
    mark#(nil()) -> active#(nil())
    mark#(first(X1,X2)) -> mark#(X1) ->
    mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
    mark#(first(X1,X2)) -> mark#(X1) ->
    mark#(first(X1,X2)) -> first#(mark(X1),mark(X2))
    mark#(first(X1,X2)) -> mark#(X1) ->
    mark#(first(X1,X2)) -> mark#(X1)
    mark#(first(X1,X2)) -> mark#(X1) ->
    mark#(first(X1,X2)) -> mark#(X2)
    mark#(first(X1,X2)) -> mark#(X1) ->
    mark#(s(X)) -> active#(s(X))
    mark#(first(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
    mark#(first(X1,X2)) -> mark#(X1) ->
    mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
    mark#(first(X1,X2)) -> mark#(X1) ->
    mark#(add(X1,X2)) -> add#(mark(X1),X2)
    mark#(first(X1,X2)) -> mark#(X1) ->
    mark#(add(X1,X2)) -> mark#(X1)
    mark#(first(X1,X2)) -> mark#(X1) ->
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
    mark#(first(X1,X2)) -> mark#(X1) ->
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
    mark#(first(X1,X2)) -> mark#(X1) ->
    mark#(if(X1,X2,X3)) -> mark#(X1)
    mark#(first(X1,X2)) -> mark#(X1) ->
    mark#(false()) -> active#(false())
    mark#(first(X1,X2)) -> mark#(X1) ->
    mark#(true()) -> active#(true())
    mark#(first(X1,X2)) -> mark#(X1) ->
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    mark#(first(X1,X2)) -> mark#(X1) ->
    mark#(and(X1,X2)) -> and#(mark(X1),X2)
    mark#(first(X1,X2)) -> mark#(X1) ->
    mark#(and(X1,X2)) -> mark#(X1)
    mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) ->
    active#(from(X)) -> mark#(cons(X,from(s(X))))
    mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) ->
    active#(from(X)) -> cons#(X,from(s(X)))
    mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) ->
    active#(from(X)) -> from#(s(X))
    mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) ->
    active#(from(X)) -> s#(X)
    mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) ->
    active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z)))
    mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) ->
    active#(first(s(X),cons(Y,Z))) -> cons#(Y,first(X,Z))
    mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) ->
    active#(first(s(X),cons(Y,Z))) -> first#(X,Z)
    mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) ->
    active#(first(0(),X)) -> mark#(nil())
    mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) ->
    active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
    mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) ->
    active#(add(s(X),Y)) -> s#(add(X,Y))
    mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) ->
    active#(add(s(X),Y)) -> add#(X,Y)
    mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) ->
    active#(add(0(),X)) -> mark#(X)
    mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) ->
    active#(if(false(),X,Y)) -> mark#(Y)
    mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) ->
    active#(if(true(),X,Y)) -> mark#(X)
    mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) ->
    active#(and(false(),Y)) -> mark#(false())
    mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) ->
    active#(and(true(),X)) -> mark#(X)
    mark#(s(X)) -> active#(s(X)) ->
    active#(from(X)) -> mark#(cons(X,from(s(X))))
    mark#(s(X)) -> active#(s(X)) ->
    active#(from(X)) -> cons#(X,from(s(X)))
    mark#(s(X)) -> active#(s(X)) -> active#(from(X)) -> from#(s(X))
    mark#(s(X)) -> active#(s(X)) -> active#(from(X)) -> s#(X)
    mark#(s(X)) -> active#(s(X)) ->
    active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z)))
    mark#(s(X)) -> active#(s(X)) ->
    active#(first(s(X),cons(Y,Z))) -> cons#(Y,first(X,Z))
    mark#(s(X)) -> active#(s(X)) ->
    active#(first(s(X),cons(Y,Z))) -> first#(X,Z)
    mark#(s(X)) -> active#(s(X)) ->
    active#(first(0(),X)) -> mark#(nil())
    mark#(s(X)) -> active#(s(X)) ->
    active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
    mark#(s(X)) -> active#(s(X)) ->
    active#(add(s(X),Y)) -> s#(add(X,Y))
    mark#(s(X)) -> active#(s(X)) -> active#(add(s(X),Y)) -> add#(X,Y)
    mark#(s(X)) -> active#(s(X)) -> active#(add(0(),X)) -> mark#(X)
    mark#(s(X)) -> active#(s(X)) ->
    active#(if(false(),X,Y)) -> mark#(Y)
    mark#(s(X)) -> active#(s(X)) -> active#(if(true(),X,Y)) -> mark#(X)
    mark#(s(X)) -> active#(s(X)) ->
    active#(and(false(),Y)) -> mark#(false())
    mark#(s(X)) -> active#(s(X)) ->
    active#(and(true(),X)) -> mark#(X)
    mark#(add(X1,X2)) -> add#(mark(X1),X2) ->
    add#(X1,active(X2)) -> add#(X1,X2)
    mark#(add(X1,X2)) -> add#(mark(X1),X2) ->
    add#(active(X1),X2) -> add#(X1,X2)
    mark#(add(X1,X2)) -> add#(mark(X1),X2) ->
    add#(X1,mark(X2)) -> add#(X1,X2)
    mark#(add(X1,X2)) -> add#(mark(X1),X2) ->
    add#(mark(X1),X2) -> add#(X1,X2)
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(from(X)) -> active#(from(X))
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(cons(X1,X2)) -> active#(cons(X1,X2))
    mark#(add(X1,X2)) -> mark#(X1) -> mark#(nil()) -> active#(nil())
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(first(X1,X2)) -> first#(mark(X1),mark(X2))
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(first(X1,X2)) -> mark#(X1)
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(first(X1,X2)) -> mark#(X2)
    mark#(add(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> active#(s(X))
    mark#(add(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(add(X1,X2)) -> add#(mark(X1),X2)
    mark#(add(X1,X2)) -> mark#(X1) -> mark#(add(X1,X2)) -> mark#(X1)
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(if(X1,X2,X3)) -> mark#(X1)
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(false()) -> active#(false())
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(true()) -> active#(true())
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(and(X1,X2)) -> and#(mark(X1),X2)
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(and(X1,X2)) -> mark#(X1)
    mark#(add(X1,X2)) -> active#(add(mark(X1),X2)) ->
    active#(from(X)) -> mark#(cons(X,from(s(X))))
    mark#(add(X1,X2)) -> active#(add(mark(X1),X2)) ->
    active#(from(X)) -> cons#(X,from(s(X)))
    mark#(add(X1,X2)) -> active#(add(mark(X1),X2)) ->
    active#(from(X)) -> from#(s(X))
    mark#(add(X1,X2)) -> active#(add(mark(X1),X2)) ->
    active#(from(X)) -> s#(X)
    mark#(add(X1,X2)) -> active#(add(mark(X1),X2)) ->
    active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z)))
    mark#(add(X1,X2)) -> active#(add(mark(X1),X2)) ->
    active#(first(s(X),cons(Y,Z))) -> cons#(Y,first(X,Z))
    mark#(add(X1,X2)) -> active#(add(mark(X1),X2)) ->
    active#(first(s(X),cons(Y,Z))) -> first#(X,Z)
    mark#(add(X1,X2)) -> active#(add(mark(X1),X2)) ->
    active#(first(0(),X)) -> mark#(nil())
    mark#(add(X1,X2)) -> active#(add(mark(X1),X2)) ->
    active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
    mark#(add(X1,X2)) -> active#(add(mark(X1),X2)) ->
    active#(add(s(X),Y)) -> s#(add(X,Y))
    mark#(add(X1,X2)) -> active#(add(mark(X1),X2)) ->
    active#(add(s(X),Y)) -> add#(X,Y)
    mark#(add(X1,X2)) -> active#(add(mark(X1),X2)) ->
    active#(add(0(),X)) -> mark#(X)
    mark#(add(X1,X2)) -> active#(add(mark(X1),X2)) ->
    active#(if(false(),X,Y)) -> mark#(Y)
    mark#(add(X1,X2)) -> active#(add(mark(X1),X2)) ->
    active#(if(true(),X,Y)) -> mark#(X)
    mark#(add(X1,X2)) -> active#(add(mark(X1),X2)) ->
    active#(and(false(),Y)) -> mark#(false())
    mark#(add(X1,X2)) -> active#(add(mark(X1),X2)) ->
    active#(and(true(),X)) -> mark#(X)
    mark#(0()) -> active#(0()) ->
    active#(from(X)) -> mark#(cons(X,from(s(X))))
    mark#(0()) -> active#(0()) -> active#(from(X)) -> cons#(X,from(s(X)))
    mark#(0()) -> active#(0()) -> active#(from(X)) -> from#(s(X))
    mark#(0()) -> active#(0()) -> active#(from(X)) -> s#(X)
    mark#(0()) -> active#(0()) ->
    active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z)))
    mark#(0()) -> active#(0()) ->
    active#(first(s(X),cons(Y,Z))) -> cons#(Y,first(X,Z))
    mark#(0()) -> active#(0()) ->
    active#(first(s(X),cons(Y,Z))) -> first#(X,Z)
    mark#(0()) -> active#(0()) -> active#(first(0(),X)) -> mark#(nil())
    mark#(0()) -> active#(0()) ->
    active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
    mark#(0()) -> active#(0()) -> active#(add(s(X),Y)) -> s#(add(X,Y))
    mark#(0()) -> active#(0()) -> active#(add(s(X),Y)) -> add#(X,Y)
    mark#(0()) -> active#(0()) -> active#(add(0(),X)) -> mark#(X)
    mark#(0()) -> active#(0()) -> active#(if(false(),X,Y)) -> mark#(Y)
    mark#(0()) -> active#(0()) -> active#(if(true(),X,Y)) -> mark#(X)
    mark#(0()) -> active#(0()) ->
    active#(and(false(),Y)) -> mark#(false())
    mark#(0()) -> active#(0()) ->
    active#(and(true(),X)) -> mark#(X)
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3) ->
    if#(X1,X2,active(X3)) -> if#(X1,X2,X3)
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3) ->
    if#(X1,active(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)) -> if#(mark(X1),X2,X3) ->
    if#(X1,X2,mark(X3)) -> if#(X1,X2,X3)
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3) ->
    if#(X1,mark(X2),X3) -> if#(X1,X2,X3)
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3) ->
    if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(from(X)) -> active#(from(X))
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(cons(X1,X2)) -> active#(cons(X1,X2))
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(nil()) -> active#(nil())
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(first(X1,X2)) -> first#(mark(X1),mark(X2))
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(first(X1,X2)) -> mark#(X1)
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(first(X1,X2)) -> mark#(X2)
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(s(X)) -> active#(s(X))
    mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(0()) -> active#(0())
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(add(X1,X2)) -> add#(mark(X1),X2)
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(add(X1,X2)) -> mark#(X1)
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
    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)) -> mark#(X1)
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(false()) -> active#(false())
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(true()) -> active#(true())
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(and(X1,X2)) -> and#(mark(X1),X2)
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(and(X1,X2)) -> mark#(X1)
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(from(X)) -> mark#(cons(X,from(s(X))))
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(from(X)) -> cons#(X,from(s(X)))
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(from(X)) -> from#(s(X))
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(from(X)) -> s#(X)
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z)))
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(first(s(X),cons(Y,Z))) -> cons#(Y,first(X,Z))
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(first(s(X),cons(Y,Z))) -> first#(X,Z)
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(first(0(),X)) -> mark#(nil())
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(add(s(X),Y)) -> s#(add(X,Y))
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(add(s(X),Y)) -> add#(X,Y)
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(add(0(),X)) -> mark#(X)
    mark#(if(X1,X2,X3)) -> active#(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#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(and(false(),Y)) -> mark#(false())
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(and(true(),X)) -> mark#(X)
    mark#(false()) -> active#(false()) ->
    active#(from(X)) -> mark#(cons(X,from(s(X))))
    mark#(false()) -> active#(false()) ->
    active#(from(X)) -> cons#(X,from(s(X)))
    mark#(false()) -> active#(false()) ->
    active#(from(X)) -> from#(s(X))
    mark#(false()) -> active#(false()) ->
    active#(from(X)) -> s#(X)
    mark#(false()) -> active#(false()) ->
    active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z)))
    mark#(false()) -> active#(false()) ->
    active#(first(s(X),cons(Y,Z))) -> cons#(Y,first(X,Z))
    mark#(false()) -> active#(false()) ->
    active#(first(s(X),cons(Y,Z))) -> first#(X,Z)
    mark#(false()) -> active#(false()) ->
    active#(first(0(),X)) -> mark#(nil())
    mark#(false()) -> active#(false()) ->
    active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
    mark#(false()) -> active#(false()) ->
    active#(add(s(X),Y)) -> s#(add(X,Y))
    mark#(false()) -> active#(false()) ->
    active#(add(s(X),Y)) -> add#(X,Y)
    mark#(false()) -> active#(false()) ->
    active#(add(0(),X)) -> mark#(X)
    mark#(false()) -> active#(false()) ->
    active#(if(false(),X,Y)) -> mark#(Y)
    mark#(false()) -> active#(false()) ->
    active#(if(true(),X,Y)) -> mark#(X)
    mark#(false()) -> active#(false()) ->
    active#(and(false(),Y)) -> mark#(false())
    mark#(false()) -> active#(false()) ->
    active#(and(true(),X)) -> mark#(X)
    mark#(and(X1,X2)) -> and#(mark(X1),X2) ->
    and#(X1,active(X2)) -> and#(X1,X2)
    mark#(and(X1,X2)) -> and#(mark(X1),X2) ->
    and#(active(X1),X2) -> and#(X1,X2)
    mark#(and(X1,X2)) -> and#(mark(X1),X2) ->
    and#(X1,mark(X2)) -> and#(X1,X2)
    mark#(and(X1,X2)) -> and#(mark(X1),X2) ->
    and#(mark(X1),X2) -> and#(X1,X2)
    mark#(and(X1,X2)) -> mark#(X1) ->
    mark#(from(X)) -> active#(from(X))
    mark#(and(X1,X2)) -> mark#(X1) ->
    mark#(cons(X1,X2)) -> active#(cons(X1,X2))
    mark#(and(X1,X2)) -> mark#(X1) -> mark#(nil()) -> active#(nil())
    mark#(and(X1,X2)) -> mark#(X1) ->
    mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
    mark#(and(X1,X2)) -> mark#(X1) ->
    mark#(first(X1,X2)) -> first#(mark(X1),mark(X2))
    mark#(and(X1,X2)) -> mark#(X1) ->
    mark#(first(X1,X2)) -> mark#(X1)
    mark#(and(X1,X2)) -> mark#(X1) ->
    mark#(first(X1,X2)) -> mark#(X2)
    mark#(and(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> active#(s(X))
    mark#(and(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
    mark#(and(X1,X2)) -> mark#(X1) ->
    mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
    mark#(and(X1,X2)) -> mark#(X1) ->
    mark#(add(X1,X2)) -> add#(mark(X1),X2)
    mark#(and(X1,X2)) -> mark#(X1) -> mark#(add(X1,X2)) -> mark#(X1)
    mark#(and(X1,X2)) -> mark#(X1) ->
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
    mark#(and(X1,X2)) -> mark#(X1) ->
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
    mark#(and(X1,X2)) -> mark#(X1) ->
    mark#(if(X1,X2,X3)) -> mark#(X1)
    mark#(and(X1,X2)) -> mark#(X1) ->
    mark#(false()) -> active#(false())
    mark#(and(X1,X2)) -> mark#(X1) ->
    mark#(true()) -> active#(true())
    mark#(and(X1,X2)) -> mark#(X1) ->
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    mark#(and(X1,X2)) -> mark#(X1) ->
    mark#(and(X1,X2)) -> and#(mark(X1),X2)
    mark#(and(X1,X2)) -> mark#(X1) ->
    mark#(and(X1,X2)) -> mark#(X1)
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(from(X)) -> mark#(cons(X,from(s(X))))
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(from(X)) -> cons#(X,from(s(X)))
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(from(X)) -> from#(s(X))
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(from(X)) -> s#(X)
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z)))
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(first(s(X),cons(Y,Z))) -> cons#(Y,first(X,Z))
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(first(s(X),cons(Y,Z))) -> first#(X,Z)
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(first(0(),X)) -> mark#(nil())
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(add(s(X),Y)) -> s#(add(X,Y))
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(add(s(X),Y)) -> add#(X,Y)
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(add(0(),X)) -> mark#(X)
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(if(false(),X,Y)) -> mark#(Y)
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(if(true(),X,Y)) -> mark#(X)
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(and(false(),Y)) -> mark#(false())
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(and(true(),X)) -> mark#(X)
    mark#(true()) -> active#(true()) ->
    active#(from(X)) -> mark#(cons(X,from(s(X))))
    mark#(true()) -> active#(true()) ->
    active#(from(X)) -> cons#(X,from(s(X)))
    mark#(true()) -> active#(true()) ->
    active#(from(X)) -> from#(s(X))
    mark#(true()) -> active#(true()) -> active#(from(X)) -> s#(X)
    mark#(true()) -> active#(true()) ->
    active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z)))
    mark#(true()) -> active#(true()) ->
    active#(first(s(X),cons(Y,Z))) -> cons#(Y,first(X,Z))
    mark#(true()) -> active#(true()) ->
    active#(first(s(X),cons(Y,Z))) -> first#(X,Z)
    mark#(true()) -> active#(true()) ->
    active#(first(0(),X)) -> mark#(nil())
    mark#(true()) -> active#(true()) ->
    active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
    mark#(true()) -> active#(true()) ->
    active#(add(s(X),Y)) -> s#(add(X,Y))
    mark#(true()) -> active#(true()) ->
    active#(add(s(X),Y)) -> add#(X,Y)
    mark#(true()) -> active#(true()) ->
    active#(add(0(),X)) -> mark#(X)
    mark#(true()) -> active#(true()) ->
    active#(if(false(),X,Y)) -> mark#(Y)
    mark#(true()) -> active#(true()) ->
    active#(if(true(),X,Y)) -> mark#(X)
    mark#(true()) -> active#(true()) ->
    active#(and(false(),Y)) -> mark#(false())
    mark#(true()) -> active#(true()) ->
    active#(and(true(),X)) -> mark#(X)
    active#(from(X)) -> from#(s(X)) -> from#(active(X)) -> from#(X)
    active#(from(X)) -> from#(s(X)) ->
    from#(mark(X)) -> from#(X)
    active#(from(X)) -> cons#(X,from(s(X))) ->
    cons#(X1,active(X2)) -> cons#(X1,X2)
    active#(from(X)) -> cons#(X,from(s(X))) ->
    cons#(active(X1),X2) -> cons#(X1,X2)
    active#(from(X)) -> cons#(X,from(s(X))) ->
    cons#(X1,mark(X2)) -> cons#(X1,X2)
    active#(from(X)) -> cons#(X,from(s(X))) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    active#(from(X)) -> s#(X) -> s#(active(X)) -> s#(X)
    active#(from(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(from(X)) -> active#(from(X))
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(cons(X1,X2)) -> active#(cons(X1,X2))
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(nil()) -> active#(nil())
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(first(X1,X2)) -> first#(mark(X1),mark(X2))
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(first(X1,X2)) -> mark#(X1)
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(first(X1,X2)) -> mark#(X2)
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(s(X)) -> active#(s(X))
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(0()) -> active#(0())
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(add(X1,X2)) -> add#(mark(X1),X2)
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(add(X1,X2)) -> mark#(X1)
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(if(X1,X2,X3)) -> mark#(X1)
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(false()) -> active#(false())
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(true()) -> active#(true())
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(and(X1,X2)) -> and#(mark(X1),X2)
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(and(X1,X2)) -> mark#(X1)
    active#(first(s(X),cons(Y,Z))) -> cons#(Y,first(X,Z)) ->
    cons#(X1,active(X2)) -> cons#(X1,X2)
    active#(first(s(X),cons(Y,Z))) -> cons#(Y,first(X,Z)) ->
    cons#(active(X1),X2) -> cons#(X1,X2)
    active#(first(s(X),cons(Y,Z))) -> cons#(Y,first(X,Z)) ->
    cons#(X1,mark(X2)) -> cons#(X1,X2)
    active#(first(s(X),cons(Y,Z))) -> cons#(Y,first(X,Z)) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    active#(first(s(X),cons(Y,Z))) -> first#(X,Z) ->
    first#(X1,active(X2)) -> first#(X1,X2)
    active#(first(s(X),cons(Y,Z))) -> first#(X,Z) ->
    first#(active(X1),X2) -> first#(X1,X2)
    active#(first(s(X),cons(Y,Z))) -> first#(X,Z) ->
    first#(X1,mark(X2)) -> first#(X1,X2)
    active#(first(s(X),cons(Y,Z))) -> first#(X,Z) ->
    first#(mark(X1),X2) -> first#(X1,X2)
    active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) ->
    mark#(from(X)) -> active#(from(X))
    active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) ->
    mark#(cons(X1,X2)) -> active#(cons(X1,X2))
    active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) ->
    mark#(nil()) -> active#(nil())
    active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) ->
    mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
    active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) ->
    mark#(first(X1,X2)) -> first#(mark(X1),mark(X2))
    active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) ->
    mark#(first(X1,X2)) -> mark#(X1)
    active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) ->
    mark#(first(X1,X2)) -> mark#(X2)
    active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) ->
    mark#(s(X)) -> active#(s(X))
    active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) ->
    mark#(0()) -> active#(0())
    active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) ->
    mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
    active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) ->
    mark#(add(X1,X2)) -> add#(mark(X1),X2)
    active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) ->
    mark#(add(X1,X2)) -> mark#(X1)
    active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) ->
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
    active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) ->
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
    active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) ->
    mark#(if(X1,X2,X3)) -> mark#(X1)
    active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) ->
    mark#(false()) -> active#(false())
    active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) ->
    mark#(true()) -> active#(true())
    active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) ->
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) ->
    mark#(and(X1,X2)) -> and#(mark(X1),X2)
    active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) ->
    mark#(and(X1,X2)) -> mark#(X1)
    active#(first(0(),X)) -> mark#(nil()) ->
    mark#(from(X)) -> active#(from(X))
    active#(first(0(),X)) -> mark#(nil()) ->
    mark#(cons(X1,X2)) -> active#(cons(X1,X2))
    active#(first(0(),X)) -> mark#(nil()) ->
    mark#(nil()) -> active#(nil())
    active#(first(0(),X)) -> mark#(nil()) ->
    mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
    active#(first(0(),X)) -> mark#(nil()) ->
    mark#(first(X1,X2)) -> first#(mark(X1),mark(X2))
    active#(first(0(),X)) -> mark#(nil()) ->
    mark#(first(X1,X2)) -> mark#(X1)
    active#(first(0(),X)) -> mark#(nil()) ->
    mark#(first(X1,X2)) -> mark#(X2)
    active#(first(0(),X)) -> mark#(nil()) ->
    mark#(s(X)) -> active#(s(X))
    active#(first(0(),X)) -> mark#(nil()) ->
    mark#(0()) -> active#(0())
    active#(first(0(),X)) -> mark#(nil()) ->
    mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
    active#(first(0(),X)) -> mark#(nil()) ->
    mark#(add(X1,X2)) -> add#(mark(X1),X2)
    active#(first(0(),X)) -> mark#(nil()) ->
    mark#(add(X1,X2)) -> mark#(X1)
    active#(first(0(),X)) -> mark#(nil()) ->
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
    active#(first(0(),X)) -> mark#(nil()) ->
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
    active#(first(0(),X)) -> mark#(nil()) ->
    mark#(if(X1,X2,X3)) -> mark#(X1)
    active#(first(0(),X)) -> mark#(nil()) ->
    mark#(false()) -> active#(false())
    active#(first(0(),X)) -> mark#(nil()) ->
    mark#(true()) -> active#(true())
    active#(first(0(),X)) -> mark#(nil()) ->
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    active#(first(0(),X)) -> mark#(nil()) ->
    mark#(and(X1,X2)) -> and#(mark(X1),X2)
    active#(first(0(),X)) -> mark#(nil()) ->
    mark#(and(X1,X2)) -> mark#(X1)
    active#(add(s(X),Y)) -> s#(add(X,Y)) ->
    s#(active(X)) -> s#(X)
    active#(add(s(X),Y)) -> s#(add(X,Y)) -> s#(mark(X)) -> s#(X)
    active#(add(s(X),Y)) -> add#(X,Y) ->
    add#(X1,active(X2)) -> add#(X1,X2)
    active#(add(s(X),Y)) -> add#(X,Y) ->
    add#(active(X1),X2) -> add#(X1,X2)
    active#(add(s(X),Y)) -> add#(X,Y) ->
    add#(X1,mark(X2)) -> add#(X1,X2)
    active#(add(s(X),Y)) -> add#(X,Y) ->
    add#(mark(X1),X2) -> add#(X1,X2)
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(from(X)) -> active#(from(X))
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(cons(X1,X2)) -> active#(cons(X1,X2))
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(nil()) -> active#(nil())
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(first(X1,X2)) -> first#(mark(X1),mark(X2))
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(first(X1,X2)) -> mark#(X1)
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(first(X1,X2)) -> mark#(X2)
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(s(X)) -> active#(s(X))
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(0()) -> active#(0())
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(add(X1,X2)) -> add#(mark(X1),X2)
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(add(X1,X2)) -> mark#(X1)
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(if(X1,X2,X3)) -> mark#(X1)
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(false()) -> active#(false())
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(true()) -> active#(true())
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(and(X1,X2)) -> and#(mark(X1),X2)
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(and(X1,X2)) -> mark#(X1)
    active#(add(0(),X)) -> mark#(X) ->
    mark#(from(X)) -> active#(from(X))
    active#(add(0(),X)) -> mark#(X) ->
    mark#(cons(X1,X2)) -> active#(cons(X1,X2))
    active#(add(0(),X)) -> mark#(X) ->
    mark#(nil()) -> active#(nil())
    active#(add(0(),X)) -> mark#(X) ->
    mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
    active#(add(0(),X)) -> mark#(X) ->
    mark#(first(X1,X2)) -> first#(mark(X1),mark(X2))
    active#(add(0(),X)) -> mark#(X) ->
    mark#(first(X1,X2)) -> mark#(X1)
    active#(add(0(),X)) -> mark#(X) ->
    mark#(first(X1,X2)) -> mark#(X2)
    active#(add(0(),X)) -> mark#(X) -> mark#(s(X)) -> active#(s(X))
    active#(add(0(),X)) -> mark#(X) -> mark#(0()) -> active#(0())
    active#(add(0(),X)) -> mark#(X) ->
    mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
    active#(add(0(),X)) -> mark#(X) ->
    mark#(add(X1,X2)) -> add#(mark(X1),X2)
    active#(add(0(),X)) -> mark#(X) ->
    mark#(add(X1,X2)) -> mark#(X1)
    active#(add(0(),X)) -> mark#(X) ->
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
    active#(add(0(),X)) -> mark#(X) ->
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
    active#(add(0(),X)) -> mark#(X) ->
    mark#(if(X1,X2,X3)) -> mark#(X1)
    active#(add(0(),X)) -> mark#(X) ->
    mark#(false()) -> active#(false())
    active#(add(0(),X)) -> mark#(X) ->
    mark#(true()) -> active#(true())
    active#(add(0(),X)) -> mark#(X) ->
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    active#(add(0(),X)) -> mark#(X) ->
    mark#(and(X1,X2)) -> and#(mark(X1),X2)
    active#(add(0(),X)) -> mark#(X) ->
    mark#(and(X1,X2)) -> mark#(X1)
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(from(X)) -> active#(from(X))
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(cons(X1,X2)) -> active#(cons(X1,X2))
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(nil()) -> active#(nil())
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(first(X1,X2)) -> first#(mark(X1),mark(X2))
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(first(X1,X2)) -> mark#(X1)
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(first(X1,X2)) -> mark#(X2)
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(s(X)) -> active#(s(X))
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(0()) -> active#(0())
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(add(X1,X2)) -> add#(mark(X1),X2)
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(add(X1,X2)) -> mark#(X1)
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
    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)) -> mark#(X1)
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(false()) -> active#(false())
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(true()) -> active#(true())
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(and(X1,X2)) -> and#(mark(X1),X2)
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(and(X1,X2)) -> mark#(X1)
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(from(X)) -> active#(from(X))
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(cons(X1,X2)) -> active#(cons(X1,X2))
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(nil()) -> active#(nil())
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(first(X1,X2)) -> first#(mark(X1),mark(X2))
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(first(X1,X2)) -> mark#(X1)
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(first(X1,X2)) -> mark#(X2)
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(s(X)) -> active#(s(X))
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(0()) -> active#(0())
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(add(X1,X2)) -> add#(mark(X1),X2)
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(add(X1,X2)) -> mark#(X1)
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
    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)) -> mark#(X1)
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(false()) -> active#(false())
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(true()) -> active#(true())
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(and(X1,X2)) -> and#(mark(X1),X2)
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(and(X1,X2)) -> mark#(X1)
    active#(and(false(),Y)) -> mark#(false()) ->
    mark#(from(X)) -> active#(from(X))
    active#(and(false(),Y)) -> mark#(false()) ->
    mark#(cons(X1,X2)) -> active#(cons(X1,X2))
    active#(and(false(),Y)) -> mark#(false()) ->
    mark#(nil()) -> active#(nil())
    active#(and(false(),Y)) -> mark#(false()) ->
    mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
    active#(and(false(),Y)) -> mark#(false()) ->
    mark#(first(X1,X2)) -> first#(mark(X1),mark(X2))
    active#(and(false(),Y)) -> mark#(false()) ->
    mark#(first(X1,X2)) -> mark#(X1)
    active#(and(false(),Y)) -> mark#(false()) ->
    mark#(first(X1,X2)) -> mark#(X2)
    active#(and(false(),Y)) -> mark#(false()) ->
    mark#(s(X)) -> active#(s(X))
    active#(and(false(),Y)) -> mark#(false()) ->
    mark#(0()) -> active#(0())
    active#(and(false(),Y)) -> mark#(false()) ->
    mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
    active#(and(false(),Y)) -> mark#(false()) ->
    mark#(add(X1,X2)) -> add#(mark(X1),X2)
    active#(and(false(),Y)) -> mark#(false()) ->
    mark#(add(X1,X2)) -> mark#(X1)
    active#(and(false(),Y)) -> mark#(false()) ->
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
    active#(and(false(),Y)) -> mark#(false()) ->
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
    active#(and(false(),Y)) -> mark#(false()) ->
    mark#(if(X1,X2,X3)) -> mark#(X1)
    active#(and(false(),Y)) -> mark#(false()) ->
    mark#(false()) -> active#(false())
    active#(and(false(),Y)) -> mark#(false()) ->
    mark#(true()) -> active#(true())
    active#(and(false(),Y)) -> mark#(false()) ->
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    active#(and(false(),Y)) -> mark#(false()) ->
    mark#(and(X1,X2)) -> and#(mark(X1),X2)
    active#(and(false(),Y)) -> mark#(false()) ->
    mark#(and(X1,X2)) -> mark#(X1)
    active#(and(true(),X)) -> mark#(X) ->
    mark#(from(X)) -> active#(from(X))
    active#(and(true(),X)) -> mark#(X) ->
    mark#(cons(X1,X2)) -> active#(cons(X1,X2))
    active#(and(true(),X)) -> mark#(X) ->
    mark#(nil()) -> active#(nil())
    active#(and(true(),X)) -> mark#(X) ->
    mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
    active#(and(true(),X)) -> mark#(X) ->
    mark#(first(X1,X2)) -> first#(mark(X1),mark(X2))
    active#(and(true(),X)) -> mark#(X) ->
    mark#(first(X1,X2)) -> mark#(X1)
    active#(and(true(),X)) -> mark#(X) ->
    mark#(first(X1,X2)) -> mark#(X2)
    active#(and(true(),X)) -> mark#(X) ->
    mark#(s(X)) -> active#(s(X))
    active#(and(true(),X)) -> mark#(X) ->
    mark#(0()) -> active#(0())
    active#(and(true(),X)) -> mark#(X) ->
    mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
    active#(and(true(),X)) -> mark#(X) ->
    mark#(add(X1,X2)) -> add#(mark(X1),X2)
    active#(and(true(),X)) -> mark#(X) ->
    mark#(add(X1,X2)) -> mark#(X1)
    active#(and(true(),X)) -> mark#(X) ->
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
    active#(and(true(),X)) -> mark#(X) ->
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
    active#(and(true(),X)) -> mark#(X) ->
    mark#(if(X1,X2,X3)) -> mark#(X1)
    active#(and(true(),X)) -> mark#(X) ->
    mark#(false()) -> active#(false())
    active#(and(true(),X)) -> mark#(X) ->
    mark#(true()) -> active#(true())
    active#(and(true(),X)) -> mark#(X) ->
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    active#(and(true(),X)) -> mark#(X) ->
    mark#(and(X1,X2)) -> and#(mark(X1),X2)
    active#(and(true(),X)) -> mark#(X) -> mark#(and(X1,X2)) -> mark#(X1)
   SCC Processor:
    #sccs: 8
    #rules: 51
    #arcs: 604/3844
    DPs:
     mark#(from(X)) -> active#(from(X))
     active#(and(true(),X)) -> mark#(X)
     mark#(and(X1,X2)) -> mark#(X1)
     mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
     active#(and(false(),Y)) -> mark#(false())
     mark#(true()) -> active#(true())
     active#(if(true(),X,Y)) -> mark#(X)
     mark#(false()) -> active#(false())
     active#(if(false(),X,Y)) -> mark#(Y)
     mark#(if(X1,X2,X3)) -> mark#(X1)
     mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
     active#(add(0(),X)) -> mark#(X)
     mark#(add(X1,X2)) -> mark#(X1)
     mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
     active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
     mark#(0()) -> active#(0())
     active#(first(0(),X)) -> mark#(nil())
     mark#(s(X)) -> active#(s(X))
     active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z)))
     mark#(first(X1,X2)) -> mark#(X2)
     mark#(first(X1,X2)) -> mark#(X1)
     mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
     active#(from(X)) -> mark#(cons(X,from(s(X))))
     mark#(nil()) -> active#(nil())
     mark#(cons(X1,X2)) -> active#(cons(X1,X2))
    TRS:
     active(and(true(),X)) -> mark(X)
     active(and(false(),Y)) -> mark(false())
     active(if(true(),X,Y)) -> mark(X)
     active(if(false(),X,Y)) -> mark(Y)
     active(add(0(),X)) -> mark(X)
     active(add(s(X),Y)) -> mark(s(add(X,Y)))
     active(first(0(),X)) -> mark(nil())
     active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
     active(from(X)) -> mark(cons(X,from(s(X))))
     mark(and(X1,X2)) -> active(and(mark(X1),X2))
     mark(true()) -> active(true())
     mark(false()) -> active(false())
     mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
     mark(add(X1,X2)) -> active(add(mark(X1),X2))
     mark(0()) -> active(0())
     mark(s(X)) -> active(s(X))
     mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
     mark(nil()) -> active(nil())
     mark(cons(X1,X2)) -> active(cons(X1,X2))
     mark(from(X)) -> active(from(X))
     and(mark(X1),X2) -> and(X1,X2)
     and(X1,mark(X2)) -> and(X1,X2)
     and(active(X1),X2) -> and(X1,X2)
     and(X1,active(X2)) -> and(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)
     add(mark(X1),X2) -> add(X1,X2)
     add(X1,mark(X2)) -> add(X1,X2)
     add(active(X1),X2) -> add(X1,X2)
     add(X1,active(X2)) -> add(X1,X2)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     first(mark(X1),X2) -> first(X1,X2)
     first(X1,mark(X2)) -> first(X1,X2)
     first(active(X1),X2) -> first(X1,X2)
     first(X1,active(X2)) -> first(X1,X2)
     cons(mark(X1),X2) -> cons(X1,X2)
     cons(X1,mark(X2)) -> cons(X1,X2)
     cons(active(X1),X2) -> cons(X1,X2)
     cons(X1,active(X2)) -> cons(X1,X2)
     from(mark(X)) -> from(X)
     from(active(X)) -> from(X)
    EDG Processor:
     DPs:
      mark#(from(X)) -> active#(from(X))
      active#(and(true(),X)) -> mark#(X)
      mark#(and(X1,X2)) -> mark#(X1)
      mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
      active#(and(false(),Y)) -> mark#(false())
      mark#(true()) -> active#(true())
      active#(if(true(),X,Y)) -> mark#(X)
      mark#(false()) -> active#(false())
      active#(if(false(),X,Y)) -> mark#(Y)
      mark#(if(X1,X2,X3)) -> mark#(X1)
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
      active#(add(0(),X)) -> mark#(X)
      mark#(add(X1,X2)) -> mark#(X1)
      mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
      active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
      mark#(0()) -> active#(0())
      active#(first(0(),X)) -> mark#(nil())
      mark#(s(X)) -> active#(s(X))
      active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z)))
      mark#(first(X1,X2)) -> mark#(X2)
      mark#(first(X1,X2)) -> mark#(X1)
      mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
      active#(from(X)) -> mark#(cons(X,from(s(X))))
      mark#(nil()) -> active#(nil())
      mark#(cons(X1,X2)) -> active#(cons(X1,X2))
     TRS:
      active(and(true(),X)) -> mark(X)
      active(and(false(),Y)) -> mark(false())
      active(if(true(),X,Y)) -> mark(X)
      active(if(false(),X,Y)) -> mark(Y)
      active(add(0(),X)) -> mark(X)
      active(add(s(X),Y)) -> mark(s(add(X,Y)))
      active(first(0(),X)) -> mark(nil())
      active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
      active(from(X)) -> mark(cons(X,from(s(X))))
      mark(and(X1,X2)) -> active(and(mark(X1),X2))
      mark(true()) -> active(true())
      mark(false()) -> active(false())
      mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
      mark(add(X1,X2)) -> active(add(mark(X1),X2))
      mark(0()) -> active(0())
      mark(s(X)) -> active(s(X))
      mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
      mark(nil()) -> active(nil())
      mark(cons(X1,X2)) -> active(cons(X1,X2))
      mark(from(X)) -> active(from(X))
      and(mark(X1),X2) -> and(X1,X2)
      and(X1,mark(X2)) -> and(X1,X2)
      and(active(X1),X2) -> and(X1,X2)
      and(X1,active(X2)) -> and(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)
      add(mark(X1),X2) -> add(X1,X2)
      add(X1,mark(X2)) -> add(X1,X2)
      add(active(X1),X2) -> add(X1,X2)
      add(X1,active(X2)) -> add(X1,X2)
      s(mark(X)) -> s(X)
      s(active(X)) -> s(X)
      first(mark(X1),X2) -> first(X1,X2)
      first(X1,mark(X2)) -> first(X1,X2)
      first(active(X1),X2) -> first(X1,X2)
      first(X1,active(X2)) -> first(X1,X2)
      cons(mark(X1),X2) -> cons(X1,X2)
      cons(X1,mark(X2)) -> cons(X1,X2)
      cons(active(X1),X2) -> cons(X1,X2)
      cons(X1,active(X2)) -> cons(X1,X2)
      from(mark(X)) -> from(X)
      from(active(X)) -> from(X)
     graph:
      mark#(from(X)) -> active#(from(X)) ->
      active#(and(true(),X)) -> mark#(X)
      mark#(from(X)) -> active#(from(X)) ->
      active#(and(false(),Y)) -> mark#(false())
      mark#(from(X)) -> active#(from(X)) ->
      active#(if(true(),X,Y)) -> mark#(X)
      mark#(from(X)) -> active#(from(X)) ->
      active#(if(false(),X,Y)) -> mark#(Y)
      mark#(from(X)) -> active#(from(X)) ->
      active#(add(0(),X)) -> mark#(X)
      mark#(from(X)) -> active#(from(X)) ->
      active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
      mark#(from(X)) -> active#(from(X)) ->
      active#(first(0(),X)) -> mark#(nil())
      mark#(from(X)) -> active#(from(X)) ->
      active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z)))
      mark#(from(X)) -> active#(from(X)) ->
      active#(from(X)) -> mark#(cons(X,from(s(X))))
      mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
      active#(and(true(),X)) -> mark#(X)
      mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
      active#(and(false(),Y)) -> mark#(false())
      mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
      active#(if(true(),X,Y)) -> mark#(X)
      mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
      active#(if(false(),X,Y)) -> mark#(Y)
      mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
      active#(add(0(),X)) -> mark#(X)
      mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
      active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
      mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
      active#(first(0(),X)) -> mark#(nil())
      mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
      active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z)))
      mark#(cons(X1,X2)) -> active#(cons(X1,X2)) ->
      active#(from(X)) -> mark#(cons(X,from(s(X))))
      mark#(first(X1,X2)) -> mark#(X2) ->
      mark#(and(X1,X2)) -> mark#(X1)
      mark#(first(X1,X2)) -> mark#(X2) ->
      mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
      mark#(first(X1,X2)) -> mark#(X2) ->
      mark#(true()) -> active#(true())
      mark#(first(X1,X2)) -> mark#(X2) ->
      mark#(false()) -> active#(false())
      mark#(first(X1,X2)) -> mark#(X2) ->
      mark#(if(X1,X2,X3)) -> mark#(X1)
      mark#(first(X1,X2)) -> mark#(X2) ->
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
      mark#(first(X1,X2)) -> mark#(X2) ->
      mark#(add(X1,X2)) -> mark#(X1)
      mark#(first(X1,X2)) -> mark#(X2) ->
      mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
      mark#(first(X1,X2)) -> mark#(X2) ->
      mark#(0()) -> active#(0())
      mark#(first(X1,X2)) -> mark#(X2) ->
      mark#(s(X)) -> active#(s(X))
      mark#(first(X1,X2)) -> mark#(X2) ->
      mark#(first(X1,X2)) -> mark#(X2)
      mark#(first(X1,X2)) -> mark#(X2) ->
      mark#(first(X1,X2)) -> mark#(X1)
      mark#(first(X1,X2)) -> mark#(X2) ->
      mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
      mark#(first(X1,X2)) -> mark#(X2) ->
      mark#(nil()) -> active#(nil())
      mark#(first(X1,X2)) -> mark#(X2) ->
      mark#(cons(X1,X2)) -> active#(cons(X1,X2))
      mark#(first(X1,X2)) -> mark#(X2) ->
      mark#(from(X)) -> active#(from(X))
      mark#(first(X1,X2)) -> mark#(X1) ->
      mark#(and(X1,X2)) -> mark#(X1)
      mark#(first(X1,X2)) -> mark#(X1) ->
      mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
      mark#(first(X1,X2)) -> mark#(X1) ->
      mark#(true()) -> active#(true())
      mark#(first(X1,X2)) -> mark#(X1) ->
      mark#(false()) -> active#(false())
      mark#(first(X1,X2)) -> mark#(X1) ->
      mark#(if(X1,X2,X3)) -> mark#(X1)
      mark#(first(X1,X2)) -> mark#(X1) ->
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
      mark#(first(X1,X2)) -> mark#(X1) ->
      mark#(add(X1,X2)) -> mark#(X1)
      mark#(first(X1,X2)) -> mark#(X1) ->
      mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
      mark#(first(X1,X2)) -> mark#(X1) ->
      mark#(0()) -> active#(0())
      mark#(first(X1,X2)) -> mark#(X1) ->
      mark#(s(X)) -> active#(s(X))
      mark#(first(X1,X2)) -> mark#(X1) ->
      mark#(first(X1,X2)) -> mark#(X2)
      mark#(first(X1,X2)) -> mark#(X1) ->
      mark#(first(X1,X2)) -> mark#(X1)
      mark#(first(X1,X2)) -> mark#(X1) ->
      mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
      mark#(first(X1,X2)) -> mark#(X1) ->
      mark#(nil()) -> active#(nil())
      mark#(first(X1,X2)) -> mark#(X1) ->
      mark#(cons(X1,X2)) -> active#(cons(X1,X2))
      mark#(first(X1,X2)) -> mark#(X1) ->
      mark#(from(X)) -> active#(from(X))
      mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) ->
      active#(and(true(),X)) -> mark#(X)
      mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) ->
      active#(and(false(),Y)) -> mark#(false())
      mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) ->
      active#(if(true(),X,Y)) -> mark#(X)
      mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) ->
      active#(if(false(),X,Y)) -> mark#(Y)
      mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) ->
      active#(add(0(),X)) -> mark#(X)
      mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) ->
      active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
      mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) ->
      active#(first(0(),X)) -> mark#(nil())
      mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) ->
      active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z)))
      mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) ->
      active#(from(X)) -> mark#(cons(X,from(s(X))))
      mark#(s(X)) -> active#(s(X)) ->
      active#(and(true(),X)) -> mark#(X)
      mark#(s(X)) -> active#(s(X)) ->
      active#(and(false(),Y)) -> mark#(false())
      mark#(s(X)) -> active#(s(X)) ->
      active#(if(true(),X,Y)) -> mark#(X)
      mark#(s(X)) -> active#(s(X)) ->
      active#(if(false(),X,Y)) -> mark#(Y)
      mark#(s(X)) -> active#(s(X)) -> active#(add(0(),X)) -> mark#(X)
      mark#(s(X)) -> active#(s(X)) ->
      active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
      mark#(s(X)) -> active#(s(X)) ->
      active#(first(0(),X)) -> mark#(nil())
      mark#(s(X)) -> active#(s(X)) ->
      active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z)))
      mark#(s(X)) -> active#(s(X)) ->
      active#(from(X)) -> mark#(cons(X,from(s(X))))
      mark#(add(X1,X2)) -> mark#(X1) ->
      mark#(and(X1,X2)) -> mark#(X1)
      mark#(add(X1,X2)) -> mark#(X1) ->
      mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
      mark#(add(X1,X2)) -> mark#(X1) ->
      mark#(true()) -> active#(true())
      mark#(add(X1,X2)) -> mark#(X1) ->
      mark#(false()) -> active#(false())
      mark#(add(X1,X2)) -> mark#(X1) ->
      mark#(if(X1,X2,X3)) -> mark#(X1)
      mark#(add(X1,X2)) -> mark#(X1) ->
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
      mark#(add(X1,X2)) -> mark#(X1) ->
      mark#(add(X1,X2)) -> mark#(X1)
      mark#(add(X1,X2)) -> mark#(X1) ->
      mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
      mark#(add(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
      mark#(add(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> active#(s(X))
      mark#(add(X1,X2)) -> mark#(X1) ->
      mark#(first(X1,X2)) -> mark#(X2)
      mark#(add(X1,X2)) -> mark#(X1) ->
      mark#(first(X1,X2)) -> mark#(X1)
      mark#(add(X1,X2)) -> mark#(X1) ->
      mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
      mark#(add(X1,X2)) -> mark#(X1) ->
      mark#(nil()) -> active#(nil())
      mark#(add(X1,X2)) -> mark#(X1) ->
      mark#(cons(X1,X2)) -> active#(cons(X1,X2))
      mark#(add(X1,X2)) -> mark#(X1) ->
      mark#(from(X)) -> active#(from(X))
      mark#(add(X1,X2)) -> active#(add(mark(X1),X2)) ->
      active#(and(true(),X)) -> mark#(X)
      mark#(add(X1,X2)) -> active#(add(mark(X1),X2)) ->
      active#(and(false(),Y)) -> mark#(false())
      mark#(add(X1,X2)) -> active#(add(mark(X1),X2)) ->
      active#(if(true(),X,Y)) -> mark#(X)
      mark#(add(X1,X2)) -> active#(add(mark(X1),X2)) ->
      active#(if(false(),X,Y)) -> mark#(Y)
      mark#(add(X1,X2)) -> active#(add(mark(X1),X2)) ->
      active#(add(0(),X)) -> mark#(X)
      mark#(add(X1,X2)) -> active#(add(mark(X1),X2)) ->
      active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
      mark#(add(X1,X2)) -> active#(add(mark(X1),X2)) ->
      active#(first(0(),X)) -> mark#(nil())
      mark#(add(X1,X2)) -> active#(add(mark(X1),X2)) ->
      active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z)))
      mark#(add(X1,X2)) -> active#(add(mark(X1),X2)) ->
      active#(from(X)) -> mark#(cons(X,from(s(X))))
      mark#(if(X1,X2,X3)) -> mark#(X1) ->
      mark#(and(X1,X2)) -> mark#(X1)
      mark#(if(X1,X2,X3)) -> mark#(X1) ->
      mark#(and(X1,X2)) -> active#(and(mark(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#(if(X1,X2,X3)) -> mark#(X1)
      mark#(if(X1,X2,X3)) -> mark#(X1) ->
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
      mark#(if(X1,X2,X3)) -> mark#(X1) ->
      mark#(add(X1,X2)) -> mark#(X1)
      mark#(if(X1,X2,X3)) -> mark#(X1) ->
      mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
      mark#(if(X1,X2,X3)) -> mark#(X1) ->
      mark#(0()) -> active#(0())
      mark#(if(X1,X2,X3)) -> mark#(X1) ->
      mark#(s(X)) -> active#(s(X))
      mark#(if(X1,X2,X3)) -> mark#(X1) ->
      mark#(first(X1,X2)) -> mark#(X2)
      mark#(if(X1,X2,X3)) -> mark#(X1) ->
      mark#(first(X1,X2)) -> mark#(X1)
      mark#(if(X1,X2,X3)) -> mark#(X1) ->
      mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
      mark#(if(X1,X2,X3)) -> mark#(X1) ->
      mark#(nil()) -> active#(nil())
      mark#(if(X1,X2,X3)) -> mark#(X1) ->
      mark#(cons(X1,X2)) -> active#(cons(X1,X2))
      mark#(if(X1,X2,X3)) -> mark#(X1) ->
      mark#(from(X)) -> active#(from(X))
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
      active#(and(true(),X)) -> mark#(X)
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
      active#(and(false(),Y)) -> mark#(false())
      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#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
      active#(add(0(),X)) -> mark#(X)
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
      active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
      active#(first(0(),X)) -> mark#(nil())
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
      active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z)))
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
      active#(from(X)) -> mark#(cons(X,from(s(X))))
      mark#(and(X1,X2)) -> mark#(X1) ->
      mark#(and(X1,X2)) -> mark#(X1)
      mark#(and(X1,X2)) -> mark#(X1) ->
      mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
      mark#(and(X1,X2)) -> mark#(X1) ->
      mark#(true()) -> active#(true())
      mark#(and(X1,X2)) -> mark#(X1) ->
      mark#(false()) -> active#(false())
      mark#(and(X1,X2)) -> mark#(X1) ->
      mark#(if(X1,X2,X3)) -> mark#(X1)
      mark#(and(X1,X2)) -> mark#(X1) ->
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
      mark#(and(X1,X2)) -> mark#(X1) ->
      mark#(add(X1,X2)) -> mark#(X1)
      mark#(and(X1,X2)) -> mark#(X1) ->
      mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
      mark#(and(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
      mark#(and(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> active#(s(X))
      mark#(and(X1,X2)) -> mark#(X1) ->
      mark#(first(X1,X2)) -> mark#(X2)
      mark#(and(X1,X2)) -> mark#(X1) ->
      mark#(first(X1,X2)) -> mark#(X1)
      mark#(and(X1,X2)) -> mark#(X1) ->
      mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
      mark#(and(X1,X2)) -> mark#(X1) ->
      mark#(nil()) -> active#(nil())
      mark#(and(X1,X2)) -> mark#(X1) ->
      mark#(cons(X1,X2)) -> active#(cons(X1,X2))
      mark#(and(X1,X2)) -> mark#(X1) ->
      mark#(from(X)) -> active#(from(X))
      mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
      active#(and(true(),X)) -> mark#(X)
      mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
      active#(and(false(),Y)) -> mark#(false())
      mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
      active#(if(true(),X,Y)) -> mark#(X)
      mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
      active#(if(false(),X,Y)) -> mark#(Y)
      mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
      active#(add(0(),X)) -> mark#(X)
      mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
      active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
      mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
      active#(first(0(),X)) -> mark#(nil())
      mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
      active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z)))
      mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
      active#(from(X)) -> mark#(cons(X,from(s(X))))
      active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
      mark#(and(X1,X2)) -> mark#(X1)
      active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
      mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
      active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
      mark#(if(X1,X2,X3)) -> mark#(X1)
      active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
      active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
      mark#(add(X1,X2)) -> mark#(X1)
      active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
      mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
      active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
      mark#(s(X)) -> active#(s(X))
      active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
      mark#(first(X1,X2)) -> mark#(X2)
      active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
      mark#(first(X1,X2)) -> mark#(X1)
      active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
      mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
      active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
      mark#(cons(X1,X2)) -> active#(cons(X1,X2))
      active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
      mark#(from(X)) -> active#(from(X))
      active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) ->
      mark#(and(X1,X2)) -> mark#(X1)
      active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) ->
      mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
      active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) ->
      mark#(if(X1,X2,X3)) -> mark#(X1)
      active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) ->
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
      active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) ->
      mark#(add(X1,X2)) -> mark#(X1)
      active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) ->
      mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
      active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) ->
      mark#(s(X)) -> active#(s(X))
      active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) ->
      mark#(first(X1,X2)) -> mark#(X2)
      active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) ->
      mark#(first(X1,X2)) -> mark#(X1)
      active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) ->
      mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
      active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) ->
      mark#(cons(X1,X2)) -> active#(cons(X1,X2))
      active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) ->
      mark#(from(X)) -> active#(from(X))
      active#(first(0(),X)) -> mark#(nil()) ->
      mark#(nil()) -> active#(nil())
      active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
      mark#(and(X1,X2)) -> mark#(X1)
      active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
      mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
      active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
      mark#(if(X1,X2,X3)) -> mark#(X1)
      active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
      active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
      mark#(add(X1,X2)) -> mark#(X1)
      active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
      mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
      active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
      mark#(s(X)) -> active#(s(X))
      active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
      mark#(first(X1,X2)) -> mark#(X2)
      active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
      mark#(first(X1,X2)) -> mark#(X1)
      active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
      mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
      active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
      mark#(cons(X1,X2)) -> active#(cons(X1,X2))
      active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
      mark#(from(X)) -> active#(from(X))
      active#(add(0(),X)) -> mark#(X) ->
      mark#(and(X1,X2)) -> mark#(X1)
      active#(add(0(),X)) -> mark#(X) ->
      mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
      active#(add(0(),X)) -> mark#(X) ->
      mark#(true()) -> active#(true())
      active#(add(0(),X)) -> mark#(X) ->
      mark#(false()) -> active#(false())
      active#(add(0(),X)) -> mark#(X) ->
      mark#(if(X1,X2,X3)) -> mark#(X1)
      active#(add(0(),X)) -> mark#(X) ->
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
      active#(add(0(),X)) -> mark#(X) ->
      mark#(add(X1,X2)) -> mark#(X1)
      active#(add(0(),X)) -> mark#(X) ->
      mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
      active#(add(0(),X)) -> mark#(X) -> mark#(0()) -> active#(0())
      active#(add(0(),X)) -> mark#(X) ->
      mark#(s(X)) -> active#(s(X))
      active#(add(0(),X)) -> mark#(X) ->
      mark#(first(X1,X2)) -> mark#(X2)
      active#(add(0(),X)) -> mark#(X) ->
      mark#(first(X1,X2)) -> mark#(X1)
      active#(add(0(),X)) -> mark#(X) ->
      mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
      active#(add(0(),X)) -> mark#(X) ->
      mark#(nil()) -> active#(nil())
      active#(add(0(),X)) -> mark#(X) ->
      mark#(cons(X1,X2)) -> active#(cons(X1,X2))
      active#(add(0(),X)) -> mark#(X) ->
      mark#(from(X)) -> active#(from(X))
      active#(if(false(),X,Y)) -> mark#(Y) ->
      mark#(and(X1,X2)) -> mark#(X1)
      active#(if(false(),X,Y)) -> mark#(Y) ->
      mark#(and(X1,X2)) -> active#(and(mark(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#(if(X1,X2,X3)) -> mark#(X1)
      active#(if(false(),X,Y)) -> mark#(Y) ->
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
      active#(if(false(),X,Y)) -> mark#(Y) ->
      mark#(add(X1,X2)) -> mark#(X1)
      active#(if(false(),X,Y)) -> mark#(Y) ->
      mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
      active#(if(false(),X,Y)) -> mark#(Y) ->
      mark#(0()) -> active#(0())
      active#(if(false(),X,Y)) -> mark#(Y) ->
      mark#(s(X)) -> active#(s(X))
      active#(if(false(),X,Y)) -> mark#(Y) ->
      mark#(first(X1,X2)) -> mark#(X2)
      active#(if(false(),X,Y)) -> mark#(Y) ->
      mark#(first(X1,X2)) -> mark#(X1)
      active#(if(false(),X,Y)) -> mark#(Y) ->
      mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
      active#(if(false(),X,Y)) -> mark#(Y) ->
      mark#(nil()) -> active#(nil())
      active#(if(false(),X,Y)) -> mark#(Y) ->
      mark#(cons(X1,X2)) -> active#(cons(X1,X2))
      active#(if(false(),X,Y)) -> mark#(Y) ->
      mark#(from(X)) -> active#(from(X))
      active#(if(true(),X,Y)) -> mark#(X) ->
      mark#(and(X1,X2)) -> mark#(X1)
      active#(if(true(),X,Y)) -> mark#(X) ->
      mark#(and(X1,X2)) -> active#(and(mark(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#(if(X1,X2,X3)) -> mark#(X1)
      active#(if(true(),X,Y)) -> mark#(X) ->
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
      active#(if(true(),X,Y)) -> mark#(X) ->
      mark#(add(X1,X2)) -> mark#(X1)
      active#(if(true(),X,Y)) -> mark#(X) ->
      mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
      active#(if(true(),X,Y)) -> mark#(X) ->
      mark#(0()) -> active#(0())
      active#(if(true(),X,Y)) -> mark#(X) ->
      mark#(s(X)) -> active#(s(X))
      active#(if(true(),X,Y)) -> mark#(X) ->
      mark#(first(X1,X2)) -> mark#(X2)
      active#(if(true(),X,Y)) -> mark#(X) ->
      mark#(first(X1,X2)) -> mark#(X1)
      active#(if(true(),X,Y)) -> mark#(X) ->
      mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
      active#(if(true(),X,Y)) -> mark#(X) ->
      mark#(nil()) -> active#(nil())
      active#(if(true(),X,Y)) -> mark#(X) ->
      mark#(cons(X1,X2)) -> active#(cons(X1,X2))
      active#(if(true(),X,Y)) -> mark#(X) ->
      mark#(from(X)) -> active#(from(X))
      active#(and(false(),Y)) -> mark#(false()) ->
      mark#(false()) -> active#(false())
      active#(and(true(),X)) -> mark#(X) ->
      mark#(and(X1,X2)) -> mark#(X1)
      active#(and(true(),X)) -> mark#(X) ->
      mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
      active#(and(true(),X)) -> mark#(X) ->
      mark#(true()) -> active#(true())
      active#(and(true(),X)) -> mark#(X) ->
      mark#(false()) -> active#(false())
      active#(and(true(),X)) -> mark#(X) ->
      mark#(if(X1,X2,X3)) -> mark#(X1)
      active#(and(true(),X)) -> mark#(X) ->
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
      active#(and(true(),X)) -> mark#(X) ->
      mark#(add(X1,X2)) -> mark#(X1)
      active#(and(true(),X)) -> mark#(X) ->
      mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
      active#(and(true(),X)) -> mark#(X) ->
      mark#(0()) -> active#(0())
      active#(and(true(),X)) -> mark#(X) ->
      mark#(s(X)) -> active#(s(X))
      active#(and(true(),X)) -> mark#(X) ->
      mark#(first(X1,X2)) -> mark#(X2)
      active#(and(true(),X)) -> mark#(X) ->
      mark#(first(X1,X2)) -> mark#(X1)
      active#(and(true(),X)) -> mark#(X) ->
      mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
      active#(and(true(),X)) -> mark#(X) ->
      mark#(nil()) -> active#(nil())
      active#(and(true(),X)) -> mark#(X) ->
      mark#(cons(X1,X2)) -> active#(cons(X1,X2))
      active#(and(true(),X)) -> mark#(X) -> mark#(from(X)) -> active#(from(X))
     CDG Processor:
      DPs:
       mark#(from(X)) -> active#(from(X))
       active#(and(true(),X)) -> mark#(X)
       mark#(and(X1,X2)) -> mark#(X1)
       mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
       active#(and(false(),Y)) -> mark#(false())
       mark#(true()) -> active#(true())
       active#(if(true(),X,Y)) -> mark#(X)
       mark#(false()) -> active#(false())
       active#(if(false(),X,Y)) -> mark#(Y)
       mark#(if(X1,X2,X3)) -> mark#(X1)
       mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
       active#(add(0(),X)) -> mark#(X)
       mark#(add(X1,X2)) -> mark#(X1)
       mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
       active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
       mark#(0()) -> active#(0())
       active#(first(0(),X)) -> mark#(nil())
       mark#(s(X)) -> active#(s(X))
       active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z)))
       mark#(first(X1,X2)) -> mark#(X2)
       mark#(first(X1,X2)) -> mark#(X1)
       mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
       active#(from(X)) -> mark#(cons(X,from(s(X))))
       mark#(nil()) -> active#(nil())
       mark#(cons(X1,X2)) -> active#(cons(X1,X2))
      TRS:
       active(and(true(),X)) -> mark(X)
       active(and(false(),Y)) -> mark(false())
       active(if(true(),X,Y)) -> mark(X)
       active(if(false(),X,Y)) -> mark(Y)
       active(add(0(),X)) -> mark(X)
       active(add(s(X),Y)) -> mark(s(add(X,Y)))
       active(first(0(),X)) -> mark(nil())
       active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
       active(from(X)) -> mark(cons(X,from(s(X))))
       mark(and(X1,X2)) -> active(and(mark(X1),X2))
       mark(true()) -> active(true())
       mark(false()) -> active(false())
       mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
       mark(add(X1,X2)) -> active(add(mark(X1),X2))
       mark(0()) -> active(0())
       mark(s(X)) -> active(s(X))
       mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
       mark(nil()) -> active(nil())
       mark(cons(X1,X2)) -> active(cons(X1,X2))
       mark(from(X)) -> active(from(X))
       and(mark(X1),X2) -> and(X1,X2)
       and(X1,mark(X2)) -> and(X1,X2)
       and(active(X1),X2) -> and(X1,X2)
       and(X1,active(X2)) -> and(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)
       add(mark(X1),X2) -> add(X1,X2)
       add(X1,mark(X2)) -> add(X1,X2)
       add(active(X1),X2) -> add(X1,X2)
       add(X1,active(X2)) -> add(X1,X2)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(X)
       first(mark(X1),X2) -> first(X1,X2)
       first(X1,mark(X2)) -> first(X1,X2)
       first(active(X1),X2) -> first(X1,X2)
       first(X1,active(X2)) -> first(X1,X2)
       cons(mark(X1),X2) -> cons(X1,X2)
       cons(X1,mark(X2)) -> cons(X1,X2)
       cons(active(X1),X2) -> cons(X1,X2)
       cons(X1,active(X2)) -> cons(X1,X2)
       from(mark(X)) -> from(X)
       from(active(X)) -> from(X)
      graph:
       mark#(from(X)) -> active#(from(X)) ->
       active#(from(X)) -> mark#(cons(X,from(s(X))))
       mark#(first(X1,X2)) -> mark#(X2) ->
       mark#(from(X)) -> active#(from(X))
       mark#(first(X1,X2)) -> mark#(X2) ->
       mark#(cons(X1,X2)) -> active#(cons(X1,X2))
       mark#(first(X1,X2)) -> mark#(X2) ->
       mark#(nil()) -> active#(nil())
       mark#(first(X1,X2)) -> mark#(X2) ->
       mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
       mark#(first(X1,X2)) -> mark#(X2) ->
       mark#(first(X1,X2)) -> mark#(X1)
       mark#(first(X1,X2)) -> mark#(X2) ->
       mark#(first(X1,X2)) -> mark#(X2)
       mark#(first(X1,X2)) -> mark#(X2) ->
       mark#(s(X)) -> active#(s(X))
       mark#(first(X1,X2)) -> mark#(X2) ->
       mark#(0()) -> active#(0())
       mark#(first(X1,X2)) -> mark#(X2) ->
       mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
       mark#(first(X1,X2)) -> mark#(X2) ->
       mark#(add(X1,X2)) -> mark#(X1)
       mark#(first(X1,X2)) -> mark#(X2) ->
       mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
       mark#(first(X1,X2)) -> mark#(X2) ->
       mark#(if(X1,X2,X3)) -> mark#(X1)
       mark#(first(X1,X2)) -> mark#(X2) ->
       mark#(false()) -> active#(false())
       mark#(first(X1,X2)) -> mark#(X2) ->
       mark#(true()) -> active#(true())
       mark#(first(X1,X2)) -> mark#(X2) ->
       mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
       mark#(first(X1,X2)) -> mark#(X2) ->
       mark#(and(X1,X2)) -> mark#(X1)
       mark#(first(X1,X2)) -> mark#(X1) ->
       mark#(from(X)) -> active#(from(X))
       mark#(first(X1,X2)) -> mark#(X1) ->
       mark#(cons(X1,X2)) -> active#(cons(X1,X2))
       mark#(first(X1,X2)) -> mark#(X1) ->
       mark#(nil()) -> active#(nil())
       mark#(first(X1,X2)) -> mark#(X1) ->
       mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
       mark#(first(X1,X2)) -> mark#(X1) ->
       mark#(first(X1,X2)) -> mark#(X1)
       mark#(first(X1,X2)) -> mark#(X1) ->
       mark#(first(X1,X2)) -> mark#(X2)
       mark#(first(X1,X2)) -> mark#(X1) ->
       mark#(s(X)) -> active#(s(X))
       mark#(first(X1,X2)) -> mark#(X1) ->
       mark#(0()) -> active#(0())
       mark#(first(X1,X2)) -> mark#(X1) ->
       mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
       mark#(first(X1,X2)) -> mark#(X1) ->
       mark#(add(X1,X2)) -> mark#(X1)
       mark#(first(X1,X2)) -> mark#(X1) ->
       mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
       mark#(first(X1,X2)) -> mark#(X1) ->
       mark#(if(X1,X2,X3)) -> mark#(X1)
       mark#(first(X1,X2)) -> mark#(X1) ->
       mark#(false()) -> active#(false())
       mark#(first(X1,X2)) -> mark#(X1) ->
       mark#(true()) -> active#(true())
       mark#(first(X1,X2)) -> mark#(X1) ->
       mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
       mark#(first(X1,X2)) -> mark#(X1) ->
       mark#(and(X1,X2)) -> mark#(X1)
       mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) ->
       active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z)))
       mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2))) ->
       active#(first(0(),X)) -> mark#(nil())
       mark#(add(X1,X2)) -> mark#(X1) ->
       mark#(from(X)) -> active#(from(X))
       mark#(add(X1,X2)) -> mark#(X1) ->
       mark#(cons(X1,X2)) -> active#(cons(X1,X2))
       mark#(add(X1,X2)) -> mark#(X1) ->
       mark#(nil()) -> active#(nil())
       mark#(add(X1,X2)) -> mark#(X1) ->
       mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
       mark#(add(X1,X2)) -> mark#(X1) ->
       mark#(first(X1,X2)) -> mark#(X1)
       mark#(add(X1,X2)) -> mark#(X1) ->
       mark#(first(X1,X2)) -> mark#(X2)
       mark#(add(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> active#(s(X))
       mark#(add(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
       mark#(add(X1,X2)) -> mark#(X1) ->
       mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
       mark#(add(X1,X2)) -> mark#(X1) ->
       mark#(add(X1,X2)) -> mark#(X1)
       mark#(add(X1,X2)) -> mark#(X1) ->
       mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
       mark#(add(X1,X2)) -> mark#(X1) ->
       mark#(if(X1,X2,X3)) -> mark#(X1)
       mark#(add(X1,X2)) -> mark#(X1) ->
       mark#(false()) -> active#(false())
       mark#(add(X1,X2)) -> mark#(X1) ->
       mark#(true()) -> active#(true())
       mark#(add(X1,X2)) -> mark#(X1) ->
       mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
       mark#(add(X1,X2)) -> mark#(X1) ->
       mark#(and(X1,X2)) -> mark#(X1)
       mark#(add(X1,X2)) -> active#(add(mark(X1),X2)) ->
       active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
       mark#(add(X1,X2)) -> active#(add(mark(X1),X2)) ->
       active#(add(0(),X)) -> mark#(X)
       mark#(if(X1,X2,X3)) -> mark#(X1) ->
       mark#(from(X)) -> active#(from(X))
       mark#(if(X1,X2,X3)) -> mark#(X1) ->
       mark#(cons(X1,X2)) -> active#(cons(X1,X2))
       mark#(if(X1,X2,X3)) -> mark#(X1) ->
       mark#(nil()) -> active#(nil())
       mark#(if(X1,X2,X3)) -> mark#(X1) ->
       mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
       mark#(if(X1,X2,X3)) -> mark#(X1) ->
       mark#(first(X1,X2)) -> mark#(X1)
       mark#(if(X1,X2,X3)) -> mark#(X1) ->
       mark#(first(X1,X2)) -> mark#(X2)
       mark#(if(X1,X2,X3)) -> mark#(X1) ->
       mark#(s(X)) -> active#(s(X))
       mark#(if(X1,X2,X3)) -> mark#(X1) ->
       mark#(0()) -> active#(0())
       mark#(if(X1,X2,X3)) -> mark#(X1) ->
       mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
       mark#(if(X1,X2,X3)) -> mark#(X1) ->
       mark#(add(X1,X2)) -> mark#(X1)
       mark#(if(X1,X2,X3)) -> mark#(X1) ->
       mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
       mark#(if(X1,X2,X3)) -> mark#(X1) ->
       mark#(if(X1,X2,X3)) -> mark#(X1)
       mark#(if(X1,X2,X3)) -> mark#(X1) ->
       mark#(false()) -> active#(false())
       mark#(if(X1,X2,X3)) -> mark#(X1) ->
       mark#(true()) -> active#(true())
       mark#(if(X1,X2,X3)) -> mark#(X1) ->
       mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
       mark#(if(X1,X2,X3)) -> mark#(X1) ->
       mark#(and(X1,X2)) -> mark#(X1)
       mark#(if(X1,X2,X3)) -> active#(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#(and(X1,X2)) -> mark#(X1) ->
       mark#(from(X)) -> active#(from(X))
       mark#(and(X1,X2)) -> mark#(X1) ->
       mark#(cons(X1,X2)) -> active#(cons(X1,X2))
       mark#(and(X1,X2)) -> mark#(X1) ->
       mark#(nil()) -> active#(nil())
       mark#(and(X1,X2)) -> mark#(X1) ->
       mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
       mark#(and(X1,X2)) -> mark#(X1) ->
       mark#(first(X1,X2)) -> mark#(X1)
       mark#(and(X1,X2)) -> mark#(X1) ->
       mark#(first(X1,X2)) -> mark#(X2)
       mark#(and(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> active#(s(X))
       mark#(and(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
       mark#(and(X1,X2)) -> mark#(X1) ->
       mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
       mark#(and(X1,X2)) -> mark#(X1) ->
       mark#(add(X1,X2)) -> mark#(X1)
       mark#(and(X1,X2)) -> mark#(X1) ->
       mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
       mark#(and(X1,X2)) -> mark#(X1) ->
       mark#(if(X1,X2,X3)) -> mark#(X1)
       mark#(and(X1,X2)) -> mark#(X1) ->
       mark#(false()) -> active#(false())
       mark#(and(X1,X2)) -> mark#(X1) ->
       mark#(true()) -> active#(true())
       mark#(and(X1,X2)) -> mark#(X1) ->
       mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
       mark#(and(X1,X2)) -> mark#(X1) ->
       mark#(and(X1,X2)) -> mark#(X1)
       mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
       active#(and(false(),Y)) -> mark#(false())
       mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
       active#(and(true(),X)) -> mark#(X)
       active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
       mark#(cons(X1,X2)) -> active#(cons(X1,X2))
       active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z))) ->
       mark#(cons(X1,X2)) -> active#(cons(X1,X2))
       active#(first(0(),X)) -> mark#(nil()) ->
       mark#(nil()) -> active#(nil())
       active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
       mark#(s(X)) -> active#(s(X))
       active#(add(0(),X)) -> mark#(X) ->
       mark#(from(X)) -> active#(from(X))
       active#(add(0(),X)) -> mark#(X) ->
       mark#(cons(X1,X2)) -> active#(cons(X1,X2))
       active#(add(0(),X)) -> mark#(X) ->
       mark#(nil()) -> active#(nil())
       active#(add(0(),X)) -> mark#(X) ->
       mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
       active#(add(0(),X)) -> mark#(X) ->
       mark#(first(X1,X2)) -> mark#(X1)
       active#(add(0(),X)) -> mark#(X) ->
       mark#(first(X1,X2)) -> mark#(X2)
       active#(add(0(),X)) -> mark#(X) ->
       mark#(s(X)) -> active#(s(X))
       active#(add(0(),X)) -> mark#(X) -> mark#(0()) -> active#(0())
       active#(add(0(),X)) -> mark#(X) ->
       mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
       active#(add(0(),X)) -> mark#(X) ->
       mark#(add(X1,X2)) -> mark#(X1)
       active#(add(0(),X)) -> mark#(X) ->
       mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
       active#(add(0(),X)) -> mark#(X) ->
       mark#(if(X1,X2,X3)) -> mark#(X1)
       active#(add(0(),X)) -> mark#(X) ->
       mark#(false()) -> active#(false())
       active#(add(0(),X)) -> mark#(X) ->
       mark#(true()) -> active#(true())
       active#(add(0(),X)) -> mark#(X) ->
       mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
       active#(add(0(),X)) -> mark#(X) ->
       mark#(and(X1,X2)) -> mark#(X1)
       active#(if(false(),X,Y)) -> mark#(Y) ->
       mark#(from(X)) -> active#(from(X))
       active#(if(false(),X,Y)) -> mark#(Y) ->
       mark#(cons(X1,X2)) -> active#(cons(X1,X2))
       active#(if(false(),X,Y)) -> mark#(Y) ->
       mark#(nil()) -> active#(nil())
       active#(if(false(),X,Y)) -> mark#(Y) ->
       mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
       active#(if(false(),X,Y)) -> mark#(Y) ->
       mark#(first(X1,X2)) -> mark#(X1)
       active#(if(false(),X,Y)) -> mark#(Y) ->
       mark#(first(X1,X2)) -> mark#(X2)
       active#(if(false(),X,Y)) -> mark#(Y) ->
       mark#(s(X)) -> active#(s(X))
       active#(if(false(),X,Y)) -> mark#(Y) ->
       mark#(0()) -> active#(0())
       active#(if(false(),X,Y)) -> mark#(Y) ->
       mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
       active#(if(false(),X,Y)) -> mark#(Y) ->
       mark#(add(X1,X2)) -> mark#(X1)
       active#(if(false(),X,Y)) -> mark#(Y) ->
       mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
       active#(if(false(),X,Y)) -> mark#(Y) ->
       mark#(if(X1,X2,X3)) -> mark#(X1)
       active#(if(false(),X,Y)) -> mark#(Y) ->
       mark#(false()) -> active#(false())
       active#(if(false(),X,Y)) -> mark#(Y) ->
       mark#(true()) -> active#(true())
       active#(if(false(),X,Y)) -> mark#(Y) ->
       mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
       active#(if(false(),X,Y)) -> mark#(Y) ->
       mark#(and(X1,X2)) -> mark#(X1)
       active#(if(true(),X,Y)) -> mark#(X) ->
       mark#(from(X)) -> active#(from(X))
       active#(if(true(),X,Y)) -> mark#(X) ->
       mark#(cons(X1,X2)) -> active#(cons(X1,X2))
       active#(if(true(),X,Y)) -> mark#(X) ->
       mark#(nil()) -> active#(nil())
       active#(if(true(),X,Y)) -> mark#(X) ->
       mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
       active#(if(true(),X,Y)) -> mark#(X) ->
       mark#(first(X1,X2)) -> mark#(X1)
       active#(if(true(),X,Y)) -> mark#(X) ->
       mark#(first(X1,X2)) -> mark#(X2)
       active#(if(true(),X,Y)) -> mark#(X) ->
       mark#(s(X)) -> active#(s(X))
       active#(if(true(),X,Y)) -> mark#(X) ->
       mark#(0()) -> active#(0())
       active#(if(true(),X,Y)) -> mark#(X) ->
       mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
       active#(if(true(),X,Y)) -> mark#(X) ->
       mark#(add(X1,X2)) -> mark#(X1)
       active#(if(true(),X,Y)) -> mark#(X) ->
       mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
       active#(if(true(),X,Y)) -> mark#(X) ->
       mark#(if(X1,X2,X3)) -> mark#(X1)
       active#(if(true(),X,Y)) -> mark#(X) ->
       mark#(false()) -> active#(false())
       active#(if(true(),X,Y)) -> mark#(X) ->
       mark#(true()) -> active#(true())
       active#(if(true(),X,Y)) -> mark#(X) ->
       mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
       active#(if(true(),X,Y)) -> mark#(X) ->
       mark#(and(X1,X2)) -> mark#(X1)
       active#(and(false(),Y)) -> mark#(false()) ->
       mark#(false()) -> active#(false())
       active#(and(true(),X)) -> mark#(X) ->
       mark#(from(X)) -> active#(from(X))
       active#(and(true(),X)) -> mark#(X) ->
       mark#(cons(X1,X2)) -> active#(cons(X1,X2))
       active#(and(true(),X)) -> mark#(X) ->
       mark#(nil()) -> active#(nil())
       active#(and(true(),X)) -> mark#(X) ->
       mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
       active#(and(true(),X)) -> mark#(X) ->
       mark#(first(X1,X2)) -> mark#(X1)
       active#(and(true(),X)) -> mark#(X) ->
       mark#(first(X1,X2)) -> mark#(X2)
       active#(and(true(),X)) -> mark#(X) ->
       mark#(s(X)) -> active#(s(X))
       active#(and(true(),X)) -> mark#(X) ->
       mark#(0()) -> active#(0())
       active#(and(true(),X)) -> mark#(X) ->
       mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
       active#(and(true(),X)) -> mark#(X) ->
       mark#(add(X1,X2)) -> mark#(X1)
       active#(and(true(),X)) -> mark#(X) ->
       mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
       active#(and(true(),X)) -> mark#(X) ->
       mark#(if(X1,X2,X3)) -> mark#(X1)
       active#(and(true(),X)) -> mark#(X) ->
       mark#(false()) -> active#(false())
       active#(and(true(),X)) -> mark#(X) ->
       mark#(true()) -> active#(true())
       active#(and(true(),X)) -> mark#(X) ->
       mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
       active#(and(true(),X)) -> mark#(X) -> mark#(and(X1,X2)) -> mark#(X1)
      SCC Processor:
       #sccs: 1
       #rules: 12
       #arcs: 158/625
       DPs:
        mark#(first(X1,X2)) -> mark#(X2)
        mark#(and(X1,X2)) -> mark#(X1)
        mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
        active#(and(true(),X)) -> mark#(X)
        mark#(if(X1,X2,X3)) -> mark#(X1)
        mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
        active#(if(true(),X,Y)) -> mark#(X)
        mark#(add(X1,X2)) -> mark#(X1)
        mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
        active#(add(0(),X)) -> mark#(X)
        mark#(first(X1,X2)) -> mark#(X1)
        active#(if(false(),X,Y)) -> mark#(Y)
       TRS:
        active(and(true(),X)) -> mark(X)
        active(and(false(),Y)) -> mark(false())
        active(if(true(),X,Y)) -> mark(X)
        active(if(false(),X,Y)) -> mark(Y)
        active(add(0(),X)) -> mark(X)
        active(add(s(X),Y)) -> mark(s(add(X,Y)))
        active(first(0(),X)) -> mark(nil())
        active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
        active(from(X)) -> mark(cons(X,from(s(X))))
        mark(and(X1,X2)) -> active(and(mark(X1),X2))
        mark(true()) -> active(true())
        mark(false()) -> active(false())
        mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
        mark(add(X1,X2)) -> active(add(mark(X1),X2))
        mark(0()) -> active(0())
        mark(s(X)) -> active(s(X))
        mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
        mark(nil()) -> active(nil())
        mark(cons(X1,X2)) -> active(cons(X1,X2))
        mark(from(X)) -> active(from(X))
        and(mark(X1),X2) -> and(X1,X2)
        and(X1,mark(X2)) -> and(X1,X2)
        and(active(X1),X2) -> and(X1,X2)
        and(X1,active(X2)) -> and(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)
        add(mark(X1),X2) -> add(X1,X2)
        add(X1,mark(X2)) -> add(X1,X2)
        add(active(X1),X2) -> add(X1,X2)
        add(X1,active(X2)) -> add(X1,X2)
        s(mark(X)) -> s(X)
        s(active(X)) -> s(X)
        first(mark(X1),X2) -> first(X1,X2)
        first(X1,mark(X2)) -> first(X1,X2)
        first(active(X1),X2) -> first(X1,X2)
        first(X1,active(X2)) -> first(X1,X2)
        cons(mark(X1),X2) -> cons(X1,X2)
        cons(X1,mark(X2)) -> cons(X1,X2)
        cons(active(X1),X2) -> cons(X1,X2)
        cons(X1,active(X2)) -> cons(X1,X2)
        from(mark(X)) -> from(X)
        from(active(X)) -> from(X)
       KBO Processor:
        argument filtering:
         pi(true) = []
         pi(and) = [0,1]
         pi(active) = 0
         pi(mark) = 0
         pi(false) = []
         pi(if) = [0,1,2]
         pi(0) = []
         pi(add) = [0,1]
         pi(s) = []
         pi(first) = [0,1]
         pi(nil) = []
         pi(cons) = 0
         pi(from) = 0
         pi(active#) = 0
         pi(mark#) = [0]
        usable rules:
         active(and(true(),X)) -> mark(X)
         active(and(false(),Y)) -> mark(false())
         active(if(true(),X,Y)) -> mark(X)
         active(if(false(),X,Y)) -> mark(Y)
         active(add(0(),X)) -> mark(X)
         active(add(s(X),Y)) -> mark(s(add(X,Y)))
         active(first(0(),X)) -> mark(nil())
         active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
         active(from(X)) -> mark(cons(X,from(s(X))))
         mark(and(X1,X2)) -> active(and(mark(X1),X2))
         mark(true()) -> active(true())
         mark(false()) -> active(false())
         mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
         mark(add(X1,X2)) -> active(add(mark(X1),X2))
         mark(0()) -> active(0())
         mark(s(X)) -> active(s(X))
         mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
         mark(nil()) -> active(nil())
         mark(cons(X1,X2)) -> active(cons(X1,X2))
         mark(from(X)) -> active(from(X))
         and(mark(X1),X2) -> and(X1,X2)
         and(X1,mark(X2)) -> and(X1,X2)
         and(active(X1),X2) -> and(X1,X2)
         and(X1,active(X2)) -> and(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)
         add(mark(X1),X2) -> add(X1,X2)
         add(X1,mark(X2)) -> add(X1,X2)
         add(active(X1),X2) -> add(X1,X2)
         add(X1,active(X2)) -> add(X1,X2)
         s(mark(X)) -> s(X)
         s(active(X)) -> s(X)
         first(mark(X1),X2) -> first(X1,X2)
         first(X1,mark(X2)) -> first(X1,X2)
         first(active(X1),X2) -> first(X1,X2)
         first(X1,active(X2)) -> first(X1,X2)
         cons(mark(X1),X2) -> cons(X1,X2)
         cons(X1,mark(X2)) -> cons(X1,X2)
         cons(active(X1),X2) -> cons(X1,X2)
         cons(X1,active(X2)) -> cons(X1,X2)
         from(mark(X)) -> from(X)
         from(active(X)) -> from(X)
        weight function:
         w0 = 1
         w(mark#) = w(from) = w(nil) = w(first) = w(s) = w(0) = w(if) = w(
         false) = w(mark) = w(active) = w(true) = 1
         w(active#) = w(cons) = w(add) = w(and) = 0
        precedence:
         nil ~ first ~ s ~ add ~ 0 ~ if ~ false ~ active ~ and ~ true > 
         mark# ~ active# ~ from ~ cons ~ mark
        problem:
         DPs:
          
         TRS:
          active(and(true(),X)) -> mark(X)
          active(and(false(),Y)) -> mark(false())
          active(if(true(),X,Y)) -> mark(X)
          active(if(false(),X,Y)) -> mark(Y)
          active(add(0(),X)) -> mark(X)
          active(add(s(X),Y)) -> mark(s(add(X,Y)))
          active(first(0(),X)) -> mark(nil())
          active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
          active(from(X)) -> mark(cons(X,from(s(X))))
          mark(and(X1,X2)) -> active(and(mark(X1),X2))
          mark(true()) -> active(true())
          mark(false()) -> active(false())
          mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
          mark(add(X1,X2)) -> active(add(mark(X1),X2))
          mark(0()) -> active(0())
          mark(s(X)) -> active(s(X))
          mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
          mark(nil()) -> active(nil())
          mark(cons(X1,X2)) -> active(cons(X1,X2))
          mark(from(X)) -> active(from(X))
          and(mark(X1),X2) -> and(X1,X2)
          and(X1,mark(X2)) -> and(X1,X2)
          and(active(X1),X2) -> and(X1,X2)
          and(X1,active(X2)) -> and(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)
          add(mark(X1),X2) -> add(X1,X2)
          add(X1,mark(X2)) -> add(X1,X2)
          add(active(X1),X2) -> add(X1,X2)
          add(X1,active(X2)) -> add(X1,X2)
          s(mark(X)) -> s(X)
          s(active(X)) -> s(X)
          first(mark(X1),X2) -> first(X1,X2)
          first(X1,mark(X2)) -> first(X1,X2)
          first(active(X1),X2) -> first(X1,X2)
          first(X1,active(X2)) -> first(X1,X2)
          cons(mark(X1),X2) -> cons(X1,X2)
          cons(X1,mark(X2)) -> cons(X1,X2)
          cons(active(X1),X2) -> cons(X1,X2)
          cons(X1,active(X2)) -> cons(X1,X2)
          from(mark(X)) -> from(X)
          from(active(X)) -> from(X)
        Qed
    
    DPs:
     add#(mark(X1),X2) -> add#(X1,X2)
     add#(X1,mark(X2)) -> add#(X1,X2)
     add#(active(X1),X2) -> add#(X1,X2)
     add#(X1,active(X2)) -> add#(X1,X2)
    TRS:
     active(and(true(),X)) -> mark(X)
     active(and(false(),Y)) -> mark(false())
     active(if(true(),X,Y)) -> mark(X)
     active(if(false(),X,Y)) -> mark(Y)
     active(add(0(),X)) -> mark(X)
     active(add(s(X),Y)) -> mark(s(add(X,Y)))
     active(first(0(),X)) -> mark(nil())
     active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
     active(from(X)) -> mark(cons(X,from(s(X))))
     mark(and(X1,X2)) -> active(and(mark(X1),X2))
     mark(true()) -> active(true())
     mark(false()) -> active(false())
     mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
     mark(add(X1,X2)) -> active(add(mark(X1),X2))
     mark(0()) -> active(0())
     mark(s(X)) -> active(s(X))
     mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
     mark(nil()) -> active(nil())
     mark(cons(X1,X2)) -> active(cons(X1,X2))
     mark(from(X)) -> active(from(X))
     and(mark(X1),X2) -> and(X1,X2)
     and(X1,mark(X2)) -> and(X1,X2)
     and(active(X1),X2) -> and(X1,X2)
     and(X1,active(X2)) -> and(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)
     add(mark(X1),X2) -> add(X1,X2)
     add(X1,mark(X2)) -> add(X1,X2)
     add(active(X1),X2) -> add(X1,X2)
     add(X1,active(X2)) -> add(X1,X2)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     first(mark(X1),X2) -> first(X1,X2)
     first(X1,mark(X2)) -> first(X1,X2)
     first(active(X1),X2) -> first(X1,X2)
     first(X1,active(X2)) -> first(X1,X2)
     cons(mark(X1),X2) -> cons(X1,X2)
     cons(X1,mark(X2)) -> cons(X1,X2)
     cons(active(X1),X2) -> cons(X1,X2)
     cons(X1,active(X2)) -> cons(X1,X2)
     from(mark(X)) -> from(X)
     from(active(X)) -> from(X)
    Subterm Criterion Processor:
     simple projection:
      pi(add#) = 1
     problem:
      DPs:
       add#(mark(X1),X2) -> add#(X1,X2)
       add#(active(X1),X2) -> add#(X1,X2)
      TRS:
       active(and(true(),X)) -> mark(X)
       active(and(false(),Y)) -> mark(false())
       active(if(true(),X,Y)) -> mark(X)
       active(if(false(),X,Y)) -> mark(Y)
       active(add(0(),X)) -> mark(X)
       active(add(s(X),Y)) -> mark(s(add(X,Y)))
       active(first(0(),X)) -> mark(nil())
       active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
       active(from(X)) -> mark(cons(X,from(s(X))))
       mark(and(X1,X2)) -> active(and(mark(X1),X2))
       mark(true()) -> active(true())
       mark(false()) -> active(false())
       mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
       mark(add(X1,X2)) -> active(add(mark(X1),X2))
       mark(0()) -> active(0())
       mark(s(X)) -> active(s(X))
       mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
       mark(nil()) -> active(nil())
       mark(cons(X1,X2)) -> active(cons(X1,X2))
       mark(from(X)) -> active(from(X))
       and(mark(X1),X2) -> and(X1,X2)
       and(X1,mark(X2)) -> and(X1,X2)
       and(active(X1),X2) -> and(X1,X2)
       and(X1,active(X2)) -> and(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)
       add(mark(X1),X2) -> add(X1,X2)
       add(X1,mark(X2)) -> add(X1,X2)
       add(active(X1),X2) -> add(X1,X2)
       add(X1,active(X2)) -> add(X1,X2)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(X)
       first(mark(X1),X2) -> first(X1,X2)
       first(X1,mark(X2)) -> first(X1,X2)
       first(active(X1),X2) -> first(X1,X2)
       first(X1,active(X2)) -> first(X1,X2)
       cons(mark(X1),X2) -> cons(X1,X2)
       cons(X1,mark(X2)) -> cons(X1,X2)
       cons(active(X1),X2) -> cons(X1,X2)
       cons(X1,active(X2)) -> cons(X1,X2)
       from(mark(X)) -> from(X)
       from(active(X)) -> from(X)
     Subterm Criterion Processor:
      simple projection:
       pi(add#) = 0
      problem:
       DPs:
        
       TRS:
        active(and(true(),X)) -> mark(X)
        active(and(false(),Y)) -> mark(false())
        active(if(true(),X,Y)) -> mark(X)
        active(if(false(),X,Y)) -> mark(Y)
        active(add(0(),X)) -> mark(X)
        active(add(s(X),Y)) -> mark(s(add(X,Y)))
        active(first(0(),X)) -> mark(nil())
        active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
        active(from(X)) -> mark(cons(X,from(s(X))))
        mark(and(X1,X2)) -> active(and(mark(X1),X2))
        mark(true()) -> active(true())
        mark(false()) -> active(false())
        mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
        mark(add(X1,X2)) -> active(add(mark(X1),X2))
        mark(0()) -> active(0())
        mark(s(X)) -> active(s(X))
        mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
        mark(nil()) -> active(nil())
        mark(cons(X1,X2)) -> active(cons(X1,X2))
        mark(from(X)) -> active(from(X))
        and(mark(X1),X2) -> and(X1,X2)
        and(X1,mark(X2)) -> and(X1,X2)
        and(active(X1),X2) -> and(X1,X2)
        and(X1,active(X2)) -> and(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)
        add(mark(X1),X2) -> add(X1,X2)
        add(X1,mark(X2)) -> add(X1,X2)
        add(active(X1),X2) -> add(X1,X2)
        add(X1,active(X2)) -> add(X1,X2)
        s(mark(X)) -> s(X)
        s(active(X)) -> s(X)
        first(mark(X1),X2) -> first(X1,X2)
        first(X1,mark(X2)) -> first(X1,X2)
        first(active(X1),X2) -> first(X1,X2)
        first(X1,active(X2)) -> first(X1,X2)
        cons(mark(X1),X2) -> cons(X1,X2)
        cons(X1,mark(X2)) -> cons(X1,X2)
        cons(active(X1),X2) -> cons(X1,X2)
        cons(X1,active(X2)) -> cons(X1,X2)
        from(mark(X)) -> from(X)
        from(active(X)) -> from(X)
      Qed
    
    DPs:
     s#(mark(X)) -> s#(X)
     s#(active(X)) -> s#(X)
    TRS:
     active(and(true(),X)) -> mark(X)
     active(and(false(),Y)) -> mark(false())
     active(if(true(),X,Y)) -> mark(X)
     active(if(false(),X,Y)) -> mark(Y)
     active(add(0(),X)) -> mark(X)
     active(add(s(X),Y)) -> mark(s(add(X,Y)))
     active(first(0(),X)) -> mark(nil())
     active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
     active(from(X)) -> mark(cons(X,from(s(X))))
     mark(and(X1,X2)) -> active(and(mark(X1),X2))
     mark(true()) -> active(true())
     mark(false()) -> active(false())
     mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
     mark(add(X1,X2)) -> active(add(mark(X1),X2))
     mark(0()) -> active(0())
     mark(s(X)) -> active(s(X))
     mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
     mark(nil()) -> active(nil())
     mark(cons(X1,X2)) -> active(cons(X1,X2))
     mark(from(X)) -> active(from(X))
     and(mark(X1),X2) -> and(X1,X2)
     and(X1,mark(X2)) -> and(X1,X2)
     and(active(X1),X2) -> and(X1,X2)
     and(X1,active(X2)) -> and(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)
     add(mark(X1),X2) -> add(X1,X2)
     add(X1,mark(X2)) -> add(X1,X2)
     add(active(X1),X2) -> add(X1,X2)
     add(X1,active(X2)) -> add(X1,X2)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     first(mark(X1),X2) -> first(X1,X2)
     first(X1,mark(X2)) -> first(X1,X2)
     first(active(X1),X2) -> first(X1,X2)
     first(X1,active(X2)) -> first(X1,X2)
     cons(mark(X1),X2) -> cons(X1,X2)
     cons(X1,mark(X2)) -> cons(X1,X2)
     cons(active(X1),X2) -> cons(X1,X2)
     cons(X1,active(X2)) -> cons(X1,X2)
     from(mark(X)) -> from(X)
     from(active(X)) -> from(X)
    Subterm Criterion Processor:
     simple projection:
      pi(s#) = 0
     problem:
      DPs:
       
      TRS:
       active(and(true(),X)) -> mark(X)
       active(and(false(),Y)) -> mark(false())
       active(if(true(),X,Y)) -> mark(X)
       active(if(false(),X,Y)) -> mark(Y)
       active(add(0(),X)) -> mark(X)
       active(add(s(X),Y)) -> mark(s(add(X,Y)))
       active(first(0(),X)) -> mark(nil())
       active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
       active(from(X)) -> mark(cons(X,from(s(X))))
       mark(and(X1,X2)) -> active(and(mark(X1),X2))
       mark(true()) -> active(true())
       mark(false()) -> active(false())
       mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
       mark(add(X1,X2)) -> active(add(mark(X1),X2))
       mark(0()) -> active(0())
       mark(s(X)) -> active(s(X))
       mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
       mark(nil()) -> active(nil())
       mark(cons(X1,X2)) -> active(cons(X1,X2))
       mark(from(X)) -> active(from(X))
       and(mark(X1),X2) -> and(X1,X2)
       and(X1,mark(X2)) -> and(X1,X2)
       and(active(X1),X2) -> and(X1,X2)
       and(X1,active(X2)) -> and(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)
       add(mark(X1),X2) -> add(X1,X2)
       add(X1,mark(X2)) -> add(X1,X2)
       add(active(X1),X2) -> add(X1,X2)
       add(X1,active(X2)) -> add(X1,X2)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(X)
       first(mark(X1),X2) -> first(X1,X2)
       first(X1,mark(X2)) -> first(X1,X2)
       first(active(X1),X2) -> first(X1,X2)
       first(X1,active(X2)) -> first(X1,X2)
       cons(mark(X1),X2) -> cons(X1,X2)
       cons(X1,mark(X2)) -> cons(X1,X2)
       cons(active(X1),X2) -> cons(X1,X2)
       cons(X1,active(X2)) -> cons(X1,X2)
       from(mark(X)) -> from(X)
       from(active(X)) -> from(X)
     Qed
    
    DPs:
     first#(mark(X1),X2) -> first#(X1,X2)
     first#(X1,mark(X2)) -> first#(X1,X2)
     first#(active(X1),X2) -> first#(X1,X2)
     first#(X1,active(X2)) -> first#(X1,X2)
    TRS:
     active(and(true(),X)) -> mark(X)
     active(and(false(),Y)) -> mark(false())
     active(if(true(),X,Y)) -> mark(X)
     active(if(false(),X,Y)) -> mark(Y)
     active(add(0(),X)) -> mark(X)
     active(add(s(X),Y)) -> mark(s(add(X,Y)))
     active(first(0(),X)) -> mark(nil())
     active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
     active(from(X)) -> mark(cons(X,from(s(X))))
     mark(and(X1,X2)) -> active(and(mark(X1),X2))
     mark(true()) -> active(true())
     mark(false()) -> active(false())
     mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
     mark(add(X1,X2)) -> active(add(mark(X1),X2))
     mark(0()) -> active(0())
     mark(s(X)) -> active(s(X))
     mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
     mark(nil()) -> active(nil())
     mark(cons(X1,X2)) -> active(cons(X1,X2))
     mark(from(X)) -> active(from(X))
     and(mark(X1),X2) -> and(X1,X2)
     and(X1,mark(X2)) -> and(X1,X2)
     and(active(X1),X2) -> and(X1,X2)
     and(X1,active(X2)) -> and(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)
     add(mark(X1),X2) -> add(X1,X2)
     add(X1,mark(X2)) -> add(X1,X2)
     add(active(X1),X2) -> add(X1,X2)
     add(X1,active(X2)) -> add(X1,X2)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     first(mark(X1),X2) -> first(X1,X2)
     first(X1,mark(X2)) -> first(X1,X2)
     first(active(X1),X2) -> first(X1,X2)
     first(X1,active(X2)) -> first(X1,X2)
     cons(mark(X1),X2) -> cons(X1,X2)
     cons(X1,mark(X2)) -> cons(X1,X2)
     cons(active(X1),X2) -> cons(X1,X2)
     cons(X1,active(X2)) -> cons(X1,X2)
     from(mark(X)) -> from(X)
     from(active(X)) -> from(X)
    Subterm Criterion Processor:
     simple projection:
      pi(first#) = 1
     problem:
      DPs:
       first#(mark(X1),X2) -> first#(X1,X2)
       first#(active(X1),X2) -> first#(X1,X2)
      TRS:
       active(and(true(),X)) -> mark(X)
       active(and(false(),Y)) -> mark(false())
       active(if(true(),X,Y)) -> mark(X)
       active(if(false(),X,Y)) -> mark(Y)
       active(add(0(),X)) -> mark(X)
       active(add(s(X),Y)) -> mark(s(add(X,Y)))
       active(first(0(),X)) -> mark(nil())
       active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
       active(from(X)) -> mark(cons(X,from(s(X))))
       mark(and(X1,X2)) -> active(and(mark(X1),X2))
       mark(true()) -> active(true())
       mark(false()) -> active(false())
       mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
       mark(add(X1,X2)) -> active(add(mark(X1),X2))
       mark(0()) -> active(0())
       mark(s(X)) -> active(s(X))
       mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
       mark(nil()) -> active(nil())
       mark(cons(X1,X2)) -> active(cons(X1,X2))
       mark(from(X)) -> active(from(X))
       and(mark(X1),X2) -> and(X1,X2)
       and(X1,mark(X2)) -> and(X1,X2)
       and(active(X1),X2) -> and(X1,X2)
       and(X1,active(X2)) -> and(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)
       add(mark(X1),X2) -> add(X1,X2)
       add(X1,mark(X2)) -> add(X1,X2)
       add(active(X1),X2) -> add(X1,X2)
       add(X1,active(X2)) -> add(X1,X2)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(X)
       first(mark(X1),X2) -> first(X1,X2)
       first(X1,mark(X2)) -> first(X1,X2)
       first(active(X1),X2) -> first(X1,X2)
       first(X1,active(X2)) -> first(X1,X2)
       cons(mark(X1),X2) -> cons(X1,X2)
       cons(X1,mark(X2)) -> cons(X1,X2)
       cons(active(X1),X2) -> cons(X1,X2)
       cons(X1,active(X2)) -> cons(X1,X2)
       from(mark(X)) -> from(X)
       from(active(X)) -> from(X)
     Subterm Criterion Processor:
      simple projection:
       pi(first#) = 0
      problem:
       DPs:
        
       TRS:
        active(and(true(),X)) -> mark(X)
        active(and(false(),Y)) -> mark(false())
        active(if(true(),X,Y)) -> mark(X)
        active(if(false(),X,Y)) -> mark(Y)
        active(add(0(),X)) -> mark(X)
        active(add(s(X),Y)) -> mark(s(add(X,Y)))
        active(first(0(),X)) -> mark(nil())
        active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
        active(from(X)) -> mark(cons(X,from(s(X))))
        mark(and(X1,X2)) -> active(and(mark(X1),X2))
        mark(true()) -> active(true())
        mark(false()) -> active(false())
        mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
        mark(add(X1,X2)) -> active(add(mark(X1),X2))
        mark(0()) -> active(0())
        mark(s(X)) -> active(s(X))
        mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
        mark(nil()) -> active(nil())
        mark(cons(X1,X2)) -> active(cons(X1,X2))
        mark(from(X)) -> active(from(X))
        and(mark(X1),X2) -> and(X1,X2)
        and(X1,mark(X2)) -> and(X1,X2)
        and(active(X1),X2) -> and(X1,X2)
        and(X1,active(X2)) -> and(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)
        add(mark(X1),X2) -> add(X1,X2)
        add(X1,mark(X2)) -> add(X1,X2)
        add(active(X1),X2) -> add(X1,X2)
        add(X1,active(X2)) -> add(X1,X2)
        s(mark(X)) -> s(X)
        s(active(X)) -> s(X)
        first(mark(X1),X2) -> first(X1,X2)
        first(X1,mark(X2)) -> first(X1,X2)
        first(active(X1),X2) -> first(X1,X2)
        first(X1,active(X2)) -> first(X1,X2)
        cons(mark(X1),X2) -> cons(X1,X2)
        cons(X1,mark(X2)) -> cons(X1,X2)
        cons(active(X1),X2) -> cons(X1,X2)
        cons(X1,active(X2)) -> cons(X1,X2)
        from(mark(X)) -> from(X)
        from(active(X)) -> from(X)
      Qed
    
    DPs:
     cons#(mark(X1),X2) -> cons#(X1,X2)
     cons#(X1,mark(X2)) -> cons#(X1,X2)
     cons#(active(X1),X2) -> cons#(X1,X2)
     cons#(X1,active(X2)) -> cons#(X1,X2)
    TRS:
     active(and(true(),X)) -> mark(X)
     active(and(false(),Y)) -> mark(false())
     active(if(true(),X,Y)) -> mark(X)
     active(if(false(),X,Y)) -> mark(Y)
     active(add(0(),X)) -> mark(X)
     active(add(s(X),Y)) -> mark(s(add(X,Y)))
     active(first(0(),X)) -> mark(nil())
     active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
     active(from(X)) -> mark(cons(X,from(s(X))))
     mark(and(X1,X2)) -> active(and(mark(X1),X2))
     mark(true()) -> active(true())
     mark(false()) -> active(false())
     mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
     mark(add(X1,X2)) -> active(add(mark(X1),X2))
     mark(0()) -> active(0())
     mark(s(X)) -> active(s(X))
     mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
     mark(nil()) -> active(nil())
     mark(cons(X1,X2)) -> active(cons(X1,X2))
     mark(from(X)) -> active(from(X))
     and(mark(X1),X2) -> and(X1,X2)
     and(X1,mark(X2)) -> and(X1,X2)
     and(active(X1),X2) -> and(X1,X2)
     and(X1,active(X2)) -> and(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)
     add(mark(X1),X2) -> add(X1,X2)
     add(X1,mark(X2)) -> add(X1,X2)
     add(active(X1),X2) -> add(X1,X2)
     add(X1,active(X2)) -> add(X1,X2)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     first(mark(X1),X2) -> first(X1,X2)
     first(X1,mark(X2)) -> first(X1,X2)
     first(active(X1),X2) -> first(X1,X2)
     first(X1,active(X2)) -> first(X1,X2)
     cons(mark(X1),X2) -> cons(X1,X2)
     cons(X1,mark(X2)) -> cons(X1,X2)
     cons(active(X1),X2) -> cons(X1,X2)
     cons(X1,active(X2)) -> cons(X1,X2)
     from(mark(X)) -> from(X)
     from(active(X)) -> from(X)
    Subterm Criterion Processor:
     simple projection:
      pi(cons#) = 1
     problem:
      DPs:
       cons#(mark(X1),X2) -> cons#(X1,X2)
       cons#(active(X1),X2) -> cons#(X1,X2)
      TRS:
       active(and(true(),X)) -> mark(X)
       active(and(false(),Y)) -> mark(false())
       active(if(true(),X,Y)) -> mark(X)
       active(if(false(),X,Y)) -> mark(Y)
       active(add(0(),X)) -> mark(X)
       active(add(s(X),Y)) -> mark(s(add(X,Y)))
       active(first(0(),X)) -> mark(nil())
       active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
       active(from(X)) -> mark(cons(X,from(s(X))))
       mark(and(X1,X2)) -> active(and(mark(X1),X2))
       mark(true()) -> active(true())
       mark(false()) -> active(false())
       mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
       mark(add(X1,X2)) -> active(add(mark(X1),X2))
       mark(0()) -> active(0())
       mark(s(X)) -> active(s(X))
       mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
       mark(nil()) -> active(nil())
       mark(cons(X1,X2)) -> active(cons(X1,X2))
       mark(from(X)) -> active(from(X))
       and(mark(X1),X2) -> and(X1,X2)
       and(X1,mark(X2)) -> and(X1,X2)
       and(active(X1),X2) -> and(X1,X2)
       and(X1,active(X2)) -> and(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)
       add(mark(X1),X2) -> add(X1,X2)
       add(X1,mark(X2)) -> add(X1,X2)
       add(active(X1),X2) -> add(X1,X2)
       add(X1,active(X2)) -> add(X1,X2)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(X)
       first(mark(X1),X2) -> first(X1,X2)
       first(X1,mark(X2)) -> first(X1,X2)
       first(active(X1),X2) -> first(X1,X2)
       first(X1,active(X2)) -> first(X1,X2)
       cons(mark(X1),X2) -> cons(X1,X2)
       cons(X1,mark(X2)) -> cons(X1,X2)
       cons(active(X1),X2) -> cons(X1,X2)
       cons(X1,active(X2)) -> cons(X1,X2)
       from(mark(X)) -> from(X)
       from(active(X)) -> from(X)
     Subterm Criterion Processor:
      simple projection:
       pi(cons#) = 0
      problem:
       DPs:
        
       TRS:
        active(and(true(),X)) -> mark(X)
        active(and(false(),Y)) -> mark(false())
        active(if(true(),X,Y)) -> mark(X)
        active(if(false(),X,Y)) -> mark(Y)
        active(add(0(),X)) -> mark(X)
        active(add(s(X),Y)) -> mark(s(add(X,Y)))
        active(first(0(),X)) -> mark(nil())
        active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
        active(from(X)) -> mark(cons(X,from(s(X))))
        mark(and(X1,X2)) -> active(and(mark(X1),X2))
        mark(true()) -> active(true())
        mark(false()) -> active(false())
        mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
        mark(add(X1,X2)) -> active(add(mark(X1),X2))
        mark(0()) -> active(0())
        mark(s(X)) -> active(s(X))
        mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
        mark(nil()) -> active(nil())
        mark(cons(X1,X2)) -> active(cons(X1,X2))
        mark(from(X)) -> active(from(X))
        and(mark(X1),X2) -> and(X1,X2)
        and(X1,mark(X2)) -> and(X1,X2)
        and(active(X1),X2) -> and(X1,X2)
        and(X1,active(X2)) -> and(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)
        add(mark(X1),X2) -> add(X1,X2)
        add(X1,mark(X2)) -> add(X1,X2)
        add(active(X1),X2) -> add(X1,X2)
        add(X1,active(X2)) -> add(X1,X2)
        s(mark(X)) -> s(X)
        s(active(X)) -> s(X)
        first(mark(X1),X2) -> first(X1,X2)
        first(X1,mark(X2)) -> first(X1,X2)
        first(active(X1),X2) -> first(X1,X2)
        first(X1,active(X2)) -> first(X1,X2)
        cons(mark(X1),X2) -> cons(X1,X2)
        cons(X1,mark(X2)) -> cons(X1,X2)
        cons(active(X1),X2) -> cons(X1,X2)
        cons(X1,active(X2)) -> cons(X1,X2)
        from(mark(X)) -> from(X)
        from(active(X)) -> from(X)
      Qed
    
    DPs:
     from#(mark(X)) -> from#(X)
     from#(active(X)) -> from#(X)
    TRS:
     active(and(true(),X)) -> mark(X)
     active(and(false(),Y)) -> mark(false())
     active(if(true(),X,Y)) -> mark(X)
     active(if(false(),X,Y)) -> mark(Y)
     active(add(0(),X)) -> mark(X)
     active(add(s(X),Y)) -> mark(s(add(X,Y)))
     active(first(0(),X)) -> mark(nil())
     active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
     active(from(X)) -> mark(cons(X,from(s(X))))
     mark(and(X1,X2)) -> active(and(mark(X1),X2))
     mark(true()) -> active(true())
     mark(false()) -> active(false())
     mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
     mark(add(X1,X2)) -> active(add(mark(X1),X2))
     mark(0()) -> active(0())
     mark(s(X)) -> active(s(X))
     mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
     mark(nil()) -> active(nil())
     mark(cons(X1,X2)) -> active(cons(X1,X2))
     mark(from(X)) -> active(from(X))
     and(mark(X1),X2) -> and(X1,X2)
     and(X1,mark(X2)) -> and(X1,X2)
     and(active(X1),X2) -> and(X1,X2)
     and(X1,active(X2)) -> and(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)
     add(mark(X1),X2) -> add(X1,X2)
     add(X1,mark(X2)) -> add(X1,X2)
     add(active(X1),X2) -> add(X1,X2)
     add(X1,active(X2)) -> add(X1,X2)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     first(mark(X1),X2) -> first(X1,X2)
     first(X1,mark(X2)) -> first(X1,X2)
     first(active(X1),X2) -> first(X1,X2)
     first(X1,active(X2)) -> first(X1,X2)
     cons(mark(X1),X2) -> cons(X1,X2)
     cons(X1,mark(X2)) -> cons(X1,X2)
     cons(active(X1),X2) -> cons(X1,X2)
     cons(X1,active(X2)) -> cons(X1,X2)
     from(mark(X)) -> from(X)
     from(active(X)) -> from(X)
    Subterm Criterion Processor:
     simple projection:
      pi(from#) = 0
     problem:
      DPs:
       
      TRS:
       active(and(true(),X)) -> mark(X)
       active(and(false(),Y)) -> mark(false())
       active(if(true(),X,Y)) -> mark(X)
       active(if(false(),X,Y)) -> mark(Y)
       active(add(0(),X)) -> mark(X)
       active(add(s(X),Y)) -> mark(s(add(X,Y)))
       active(first(0(),X)) -> mark(nil())
       active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
       active(from(X)) -> mark(cons(X,from(s(X))))
       mark(and(X1,X2)) -> active(and(mark(X1),X2))
       mark(true()) -> active(true())
       mark(false()) -> active(false())
       mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
       mark(add(X1,X2)) -> active(add(mark(X1),X2))
       mark(0()) -> active(0())
       mark(s(X)) -> active(s(X))
       mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
       mark(nil()) -> active(nil())
       mark(cons(X1,X2)) -> active(cons(X1,X2))
       mark(from(X)) -> active(from(X))
       and(mark(X1),X2) -> and(X1,X2)
       and(X1,mark(X2)) -> and(X1,X2)
       and(active(X1),X2) -> and(X1,X2)
       and(X1,active(X2)) -> and(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)
       add(mark(X1),X2) -> add(X1,X2)
       add(X1,mark(X2)) -> add(X1,X2)
       add(active(X1),X2) -> add(X1,X2)
       add(X1,active(X2)) -> add(X1,X2)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(X)
       first(mark(X1),X2) -> first(X1,X2)
       first(X1,mark(X2)) -> first(X1,X2)
       first(active(X1),X2) -> first(X1,X2)
       first(X1,active(X2)) -> first(X1,X2)
       cons(mark(X1),X2) -> cons(X1,X2)
       cons(X1,mark(X2)) -> cons(X1,X2)
       cons(active(X1),X2) -> cons(X1,X2)
       cons(X1,active(X2)) -> cons(X1,X2)
       from(mark(X)) -> from(X)
       from(active(X)) -> from(X)
     Qed
    
    DPs:
     and#(mark(X1),X2) -> and#(X1,X2)
     and#(X1,mark(X2)) -> and#(X1,X2)
     and#(active(X1),X2) -> and#(X1,X2)
     and#(X1,active(X2)) -> and#(X1,X2)
    TRS:
     active(and(true(),X)) -> mark(X)
     active(and(false(),Y)) -> mark(false())
     active(if(true(),X,Y)) -> mark(X)
     active(if(false(),X,Y)) -> mark(Y)
     active(add(0(),X)) -> mark(X)
     active(add(s(X),Y)) -> mark(s(add(X,Y)))
     active(first(0(),X)) -> mark(nil())
     active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
     active(from(X)) -> mark(cons(X,from(s(X))))
     mark(and(X1,X2)) -> active(and(mark(X1),X2))
     mark(true()) -> active(true())
     mark(false()) -> active(false())
     mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
     mark(add(X1,X2)) -> active(add(mark(X1),X2))
     mark(0()) -> active(0())
     mark(s(X)) -> active(s(X))
     mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
     mark(nil()) -> active(nil())
     mark(cons(X1,X2)) -> active(cons(X1,X2))
     mark(from(X)) -> active(from(X))
     and(mark(X1),X2) -> and(X1,X2)
     and(X1,mark(X2)) -> and(X1,X2)
     and(active(X1),X2) -> and(X1,X2)
     and(X1,active(X2)) -> and(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)
     add(mark(X1),X2) -> add(X1,X2)
     add(X1,mark(X2)) -> add(X1,X2)
     add(active(X1),X2) -> add(X1,X2)
     add(X1,active(X2)) -> add(X1,X2)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     first(mark(X1),X2) -> first(X1,X2)
     first(X1,mark(X2)) -> first(X1,X2)
     first(active(X1),X2) -> first(X1,X2)
     first(X1,active(X2)) -> first(X1,X2)
     cons(mark(X1),X2) -> cons(X1,X2)
     cons(X1,mark(X2)) -> cons(X1,X2)
     cons(active(X1),X2) -> cons(X1,X2)
     cons(X1,active(X2)) -> cons(X1,X2)
     from(mark(X)) -> from(X)
     from(active(X)) -> from(X)
    Subterm Criterion Processor:
     simple projection:
      pi(and#) = 1
     problem:
      DPs:
       and#(mark(X1),X2) -> and#(X1,X2)
       and#(active(X1),X2) -> and#(X1,X2)
      TRS:
       active(and(true(),X)) -> mark(X)
       active(and(false(),Y)) -> mark(false())
       active(if(true(),X,Y)) -> mark(X)
       active(if(false(),X,Y)) -> mark(Y)
       active(add(0(),X)) -> mark(X)
       active(add(s(X),Y)) -> mark(s(add(X,Y)))
       active(first(0(),X)) -> mark(nil())
       active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
       active(from(X)) -> mark(cons(X,from(s(X))))
       mark(and(X1,X2)) -> active(and(mark(X1),X2))
       mark(true()) -> active(true())
       mark(false()) -> active(false())
       mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
       mark(add(X1,X2)) -> active(add(mark(X1),X2))
       mark(0()) -> active(0())
       mark(s(X)) -> active(s(X))
       mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
       mark(nil()) -> active(nil())
       mark(cons(X1,X2)) -> active(cons(X1,X2))
       mark(from(X)) -> active(from(X))
       and(mark(X1),X2) -> and(X1,X2)
       and(X1,mark(X2)) -> and(X1,X2)
       and(active(X1),X2) -> and(X1,X2)
       and(X1,active(X2)) -> and(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)
       add(mark(X1),X2) -> add(X1,X2)
       add(X1,mark(X2)) -> add(X1,X2)
       add(active(X1),X2) -> add(X1,X2)
       add(X1,active(X2)) -> add(X1,X2)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(X)
       first(mark(X1),X2) -> first(X1,X2)
       first(X1,mark(X2)) -> first(X1,X2)
       first(active(X1),X2) -> first(X1,X2)
       first(X1,active(X2)) -> first(X1,X2)
       cons(mark(X1),X2) -> cons(X1,X2)
       cons(X1,mark(X2)) -> cons(X1,X2)
       cons(active(X1),X2) -> cons(X1,X2)
       cons(X1,active(X2)) -> cons(X1,X2)
       from(mark(X)) -> from(X)
       from(active(X)) -> from(X)
     Subterm Criterion Processor:
      simple projection:
       pi(and#) = 0
      problem:
       DPs:
        
       TRS:
        active(and(true(),X)) -> mark(X)
        active(and(false(),Y)) -> mark(false())
        active(if(true(),X,Y)) -> mark(X)
        active(if(false(),X,Y)) -> mark(Y)
        active(add(0(),X)) -> mark(X)
        active(add(s(X),Y)) -> mark(s(add(X,Y)))
        active(first(0(),X)) -> mark(nil())
        active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
        active(from(X)) -> mark(cons(X,from(s(X))))
        mark(and(X1,X2)) -> active(and(mark(X1),X2))
        mark(true()) -> active(true())
        mark(false()) -> active(false())
        mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
        mark(add(X1,X2)) -> active(add(mark(X1),X2))
        mark(0()) -> active(0())
        mark(s(X)) -> active(s(X))
        mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
        mark(nil()) -> active(nil())
        mark(cons(X1,X2)) -> active(cons(X1,X2))
        mark(from(X)) -> active(from(X))
        and(mark(X1),X2) -> and(X1,X2)
        and(X1,mark(X2)) -> and(X1,X2)
        and(active(X1),X2) -> and(X1,X2)
        and(X1,active(X2)) -> and(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)
        add(mark(X1),X2) -> add(X1,X2)
        add(X1,mark(X2)) -> add(X1,X2)
        add(active(X1),X2) -> add(X1,X2)
        add(X1,active(X2)) -> add(X1,X2)
        s(mark(X)) -> s(X)
        s(active(X)) -> s(X)
        first(mark(X1),X2) -> first(X1,X2)
        first(X1,mark(X2)) -> first(X1,X2)
        first(active(X1),X2) -> first(X1,X2)
        first(X1,active(X2)) -> first(X1,X2)
        cons(mark(X1),X2) -> cons(X1,X2)
        cons(X1,mark(X2)) -> cons(X1,X2)
        cons(active(X1),X2) -> cons(X1,X2)
        cons(X1,active(X2)) -> cons(X1,X2)
        from(mark(X)) -> from(X)
        from(active(X)) -> from(X)
      Qed
    
    DPs:
     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(and(true(),X)) -> mark(X)
     active(and(false(),Y)) -> mark(false())
     active(if(true(),X,Y)) -> mark(X)
     active(if(false(),X,Y)) -> mark(Y)
     active(add(0(),X)) -> mark(X)
     active(add(s(X),Y)) -> mark(s(add(X,Y)))
     active(first(0(),X)) -> mark(nil())
     active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
     active(from(X)) -> mark(cons(X,from(s(X))))
     mark(and(X1,X2)) -> active(and(mark(X1),X2))
     mark(true()) -> active(true())
     mark(false()) -> active(false())
     mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
     mark(add(X1,X2)) -> active(add(mark(X1),X2))
     mark(0()) -> active(0())
     mark(s(X)) -> active(s(X))
     mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
     mark(nil()) -> active(nil())
     mark(cons(X1,X2)) -> active(cons(X1,X2))
     mark(from(X)) -> active(from(X))
     and(mark(X1),X2) -> and(X1,X2)
     and(X1,mark(X2)) -> and(X1,X2)
     and(active(X1),X2) -> and(X1,X2)
     and(X1,active(X2)) -> and(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)
     add(mark(X1),X2) -> add(X1,X2)
     add(X1,mark(X2)) -> add(X1,X2)
     add(active(X1),X2) -> add(X1,X2)
     add(X1,active(X2)) -> add(X1,X2)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     first(mark(X1),X2) -> first(X1,X2)
     first(X1,mark(X2)) -> first(X1,X2)
     first(active(X1),X2) -> first(X1,X2)
     first(X1,active(X2)) -> first(X1,X2)
     cons(mark(X1),X2) -> cons(X1,X2)
     cons(X1,mark(X2)) -> cons(X1,X2)
     cons(active(X1),X2) -> cons(X1,X2)
     cons(X1,active(X2)) -> cons(X1,X2)
     from(mark(X)) -> from(X)
     from(active(X)) -> from(X)
    Subterm Criterion Processor:
     simple projection:
      pi(if#) = 2
     problem:
      DPs:
       if#(mark(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,active(X2),X3) -> if#(X1,X2,X3)
      TRS:
       active(and(true(),X)) -> mark(X)
       active(and(false(),Y)) -> mark(false())
       active(if(true(),X,Y)) -> mark(X)
       active(if(false(),X,Y)) -> mark(Y)
       active(add(0(),X)) -> mark(X)
       active(add(s(X),Y)) -> mark(s(add(X,Y)))
       active(first(0(),X)) -> mark(nil())
       active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
       active(from(X)) -> mark(cons(X,from(s(X))))
       mark(and(X1,X2)) -> active(and(mark(X1),X2))
       mark(true()) -> active(true())
       mark(false()) -> active(false())
       mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
       mark(add(X1,X2)) -> active(add(mark(X1),X2))
       mark(0()) -> active(0())
       mark(s(X)) -> active(s(X))
       mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
       mark(nil()) -> active(nil())
       mark(cons(X1,X2)) -> active(cons(X1,X2))
       mark(from(X)) -> active(from(X))
       and(mark(X1),X2) -> and(X1,X2)
       and(X1,mark(X2)) -> and(X1,X2)
       and(active(X1),X2) -> and(X1,X2)
       and(X1,active(X2)) -> and(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)
       add(mark(X1),X2) -> add(X1,X2)
       add(X1,mark(X2)) -> add(X1,X2)
       add(active(X1),X2) -> add(X1,X2)
       add(X1,active(X2)) -> add(X1,X2)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(X)
       first(mark(X1),X2) -> first(X1,X2)
       first(X1,mark(X2)) -> first(X1,X2)
       first(active(X1),X2) -> first(X1,X2)
       first(X1,active(X2)) -> first(X1,X2)
       cons(mark(X1),X2) -> cons(X1,X2)
       cons(X1,mark(X2)) -> cons(X1,X2)
       cons(active(X1),X2) -> cons(X1,X2)
       cons(X1,active(X2)) -> cons(X1,X2)
       from(mark(X)) -> from(X)
       from(active(X)) -> from(X)
     Subterm Criterion Processor:
      simple projection:
       pi(if#) = 1
      problem:
       DPs:
        if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
        if#(active(X1),X2,X3) -> if#(X1,X2,X3)
       TRS:
        active(and(true(),X)) -> mark(X)
        active(and(false(),Y)) -> mark(false())
        active(if(true(),X,Y)) -> mark(X)
        active(if(false(),X,Y)) -> mark(Y)
        active(add(0(),X)) -> mark(X)
        active(add(s(X),Y)) -> mark(s(add(X,Y)))
        active(first(0(),X)) -> mark(nil())
        active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
        active(from(X)) -> mark(cons(X,from(s(X))))
        mark(and(X1,X2)) -> active(and(mark(X1),X2))
        mark(true()) -> active(true())
        mark(false()) -> active(false())
        mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
        mark(add(X1,X2)) -> active(add(mark(X1),X2))
        mark(0()) -> active(0())
        mark(s(X)) -> active(s(X))
        mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
        mark(nil()) -> active(nil())
        mark(cons(X1,X2)) -> active(cons(X1,X2))
        mark(from(X)) -> active(from(X))
        and(mark(X1),X2) -> and(X1,X2)
        and(X1,mark(X2)) -> and(X1,X2)
        and(active(X1),X2) -> and(X1,X2)
        and(X1,active(X2)) -> and(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)
        add(mark(X1),X2) -> add(X1,X2)
        add(X1,mark(X2)) -> add(X1,X2)
        add(active(X1),X2) -> add(X1,X2)
        add(X1,active(X2)) -> add(X1,X2)
        s(mark(X)) -> s(X)
        s(active(X)) -> s(X)
        first(mark(X1),X2) -> first(X1,X2)
        first(X1,mark(X2)) -> first(X1,X2)
        first(active(X1),X2) -> first(X1,X2)
        first(X1,active(X2)) -> first(X1,X2)
        cons(mark(X1),X2) -> cons(X1,X2)
        cons(X1,mark(X2)) -> cons(X1,X2)
        cons(active(X1),X2) -> cons(X1,X2)
        cons(X1,active(X2)) -> cons(X1,X2)
        from(mark(X)) -> from(X)
        from(active(X)) -> from(X)
      Subterm Criterion Processor:
       simple projection:
        pi(if#) = 0
       problem:
        DPs:
         
        TRS:
         active(and(true(),X)) -> mark(X)
         active(and(false(),Y)) -> mark(false())
         active(if(true(),X,Y)) -> mark(X)
         active(if(false(),X,Y)) -> mark(Y)
         active(add(0(),X)) -> mark(X)
         active(add(s(X),Y)) -> mark(s(add(X,Y)))
         active(first(0(),X)) -> mark(nil())
         active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
         active(from(X)) -> mark(cons(X,from(s(X))))
         mark(and(X1,X2)) -> active(and(mark(X1),X2))
         mark(true()) -> active(true())
         mark(false()) -> active(false())
         mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
         mark(add(X1,X2)) -> active(add(mark(X1),X2))
         mark(0()) -> active(0())
         mark(s(X)) -> active(s(X))
         mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
         mark(nil()) -> active(nil())
         mark(cons(X1,X2)) -> active(cons(X1,X2))
         mark(from(X)) -> active(from(X))
         and(mark(X1),X2) -> and(X1,X2)
         and(X1,mark(X2)) -> and(X1,X2)
         and(active(X1),X2) -> and(X1,X2)
         and(X1,active(X2)) -> and(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)
         add(mark(X1),X2) -> add(X1,X2)
         add(X1,mark(X2)) -> add(X1,X2)
         add(active(X1),X2) -> add(X1,X2)
         add(X1,active(X2)) -> add(X1,X2)
         s(mark(X)) -> s(X)
         s(active(X)) -> s(X)
         first(mark(X1),X2) -> first(X1,X2)
         first(X1,mark(X2)) -> first(X1,X2)
         first(active(X1),X2) -> first(X1,X2)
         first(X1,active(X2)) -> first(X1,X2)
         cons(mark(X1),X2) -> cons(X1,X2)
         cons(X1,mark(X2)) -> cons(X1,X2)
         cons(active(X1),X2) -> cons(X1,X2)
         cons(X1,active(X2)) -> cons(X1,X2)
         from(mark(X)) -> from(X)
         from(active(X)) -> from(X)
       Qed