MAYBE

Problem:
 active(and(tt(),X)) -> mark(X)
 active(plus(N,0())) -> mark(N)
 active(plus(N,s(M))) -> mark(s(plus(N,M)))
 active(x(N,0())) -> mark(0())
 active(x(N,s(M))) -> mark(plus(x(N,M),N))
 mark(and(X1,X2)) -> active(and(mark(X1),X2))
 mark(tt()) -> active(tt())
 mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
 mark(0()) -> active(0())
 mark(s(X)) -> active(s(mark(X)))
 mark(x(X1,X2)) -> active(x(mark(X1),mark(X2)))
 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)
 plus(mark(X1),X2) -> plus(X1,X2)
 plus(X1,mark(X2)) -> plus(X1,X2)
 plus(active(X1),X2) -> plus(X1,X2)
 plus(X1,active(X2)) -> plus(X1,X2)
 s(mark(X)) -> s(X)
 s(active(X)) -> s(X)
 x(mark(X1),X2) -> x(X1,X2)
 x(X1,mark(X2)) -> x(X1,X2)
 x(active(X1),X2) -> x(X1,X2)
 x(X1,active(X2)) -> x(X1,X2)

Proof:
 DP Processor:
  DPs:
   active#(and(tt(),X)) -> mark#(X)
   active#(plus(N,0())) -> mark#(N)
   active#(plus(N,s(M))) -> plus#(N,M)
   active#(plus(N,s(M))) -> s#(plus(N,M))
   active#(plus(N,s(M))) -> mark#(s(plus(N,M)))
   active#(x(N,0())) -> mark#(0())
   active#(x(N,s(M))) -> x#(N,M)
   active#(x(N,s(M))) -> plus#(x(N,M),N)
   active#(x(N,s(M))) -> mark#(plus(x(N,M),N))
   mark#(and(X1,X2)) -> mark#(X1)
   mark#(and(X1,X2)) -> and#(mark(X1),X2)
   mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
   mark#(tt()) -> active#(tt())
   mark#(plus(X1,X2)) -> mark#(X2)
   mark#(plus(X1,X2)) -> mark#(X1)
   mark#(plus(X1,X2)) -> plus#(mark(X1),mark(X2))
   mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
   mark#(0()) -> active#(0())
   mark#(s(X)) -> mark#(X)
   mark#(s(X)) -> s#(mark(X))
   mark#(s(X)) -> active#(s(mark(X)))
   mark#(x(X1,X2)) -> mark#(X2)
   mark#(x(X1,X2)) -> mark#(X1)
   mark#(x(X1,X2)) -> x#(mark(X1),mark(X2))
   mark#(x(X1,X2)) -> active#(x(mark(X1),mark(X2)))
   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)
   plus#(mark(X1),X2) -> plus#(X1,X2)
   plus#(X1,mark(X2)) -> plus#(X1,X2)
   plus#(active(X1),X2) -> plus#(X1,X2)
   plus#(X1,active(X2)) -> plus#(X1,X2)
   s#(mark(X)) -> s#(X)
   s#(active(X)) -> s#(X)
   x#(mark(X1),X2) -> x#(X1,X2)
   x#(X1,mark(X2)) -> x#(X1,X2)
   x#(active(X1),X2) -> x#(X1,X2)
   x#(X1,active(X2)) -> x#(X1,X2)
  TRS:
   active(and(tt(),X)) -> mark(X)
   active(plus(N,0())) -> mark(N)
   active(plus(N,s(M))) -> mark(s(plus(N,M)))
   active(x(N,0())) -> mark(0())
   active(x(N,s(M))) -> mark(plus(x(N,M),N))
   mark(and(X1,X2)) -> active(and(mark(X1),X2))
   mark(tt()) -> active(tt())
   mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
   mark(0()) -> active(0())
   mark(s(X)) -> active(s(mark(X)))
   mark(x(X1,X2)) -> active(x(mark(X1),mark(X2)))
   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)
   plus(mark(X1),X2) -> plus(X1,X2)
   plus(X1,mark(X2)) -> plus(X1,X2)
   plus(active(X1),X2) -> plus(X1,X2)
   plus(X1,active(X2)) -> plus(X1,X2)
   s(mark(X)) -> s(X)
   s(active(X)) -> s(X)
   x(mark(X1),X2) -> x(X1,X2)
   x(X1,mark(X2)) -> x(X1,X2)
   x(active(X1),X2) -> x(X1,X2)
   x(X1,active(X2)) -> x(X1,X2)
  TDG Processor:
   DPs:
    active#(and(tt(),X)) -> mark#(X)
    active#(plus(N,0())) -> mark#(N)
    active#(plus(N,s(M))) -> plus#(N,M)
    active#(plus(N,s(M))) -> s#(plus(N,M))
    active#(plus(N,s(M))) -> mark#(s(plus(N,M)))
    active#(x(N,0())) -> mark#(0())
    active#(x(N,s(M))) -> x#(N,M)
    active#(x(N,s(M))) -> plus#(x(N,M),N)
    active#(x(N,s(M))) -> mark#(plus(x(N,M),N))
    mark#(and(X1,X2)) -> mark#(X1)
    mark#(and(X1,X2)) -> and#(mark(X1),X2)
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    mark#(tt()) -> active#(tt())
    mark#(plus(X1,X2)) -> mark#(X2)
    mark#(plus(X1,X2)) -> mark#(X1)
    mark#(plus(X1,X2)) -> plus#(mark(X1),mark(X2))
    mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
    mark#(0()) -> active#(0())
    mark#(s(X)) -> mark#(X)
    mark#(s(X)) -> s#(mark(X))
    mark#(s(X)) -> active#(s(mark(X)))
    mark#(x(X1,X2)) -> mark#(X2)
    mark#(x(X1,X2)) -> mark#(X1)
    mark#(x(X1,X2)) -> x#(mark(X1),mark(X2))
    mark#(x(X1,X2)) -> active#(x(mark(X1),mark(X2)))
    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)
    plus#(mark(X1),X2) -> plus#(X1,X2)
    plus#(X1,mark(X2)) -> plus#(X1,X2)
    plus#(active(X1),X2) -> plus#(X1,X2)
    plus#(X1,active(X2)) -> plus#(X1,X2)
    s#(mark(X)) -> s#(X)
    s#(active(X)) -> s#(X)
    x#(mark(X1),X2) -> x#(X1,X2)
    x#(X1,mark(X2)) -> x#(X1,X2)
    x#(active(X1),X2) -> x#(X1,X2)
    x#(X1,active(X2)) -> x#(X1,X2)
   TRS:
    active(and(tt(),X)) -> mark(X)
    active(plus(N,0())) -> mark(N)
    active(plus(N,s(M))) -> mark(s(plus(N,M)))
    active(x(N,0())) -> mark(0())
    active(x(N,s(M))) -> mark(plus(x(N,M),N))
    mark(and(X1,X2)) -> active(and(mark(X1),X2))
    mark(tt()) -> active(tt())
    mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
    mark(0()) -> active(0())
    mark(s(X)) -> active(s(mark(X)))
    mark(x(X1,X2)) -> active(x(mark(X1),mark(X2)))
    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)
    plus(mark(X1),X2) -> plus(X1,X2)
    plus(X1,mark(X2)) -> plus(X1,X2)
    plus(active(X1),X2) -> plus(X1,X2)
    plus(X1,active(X2)) -> plus(X1,X2)
    s(mark(X)) -> s(X)
    s(active(X)) -> s(X)
    x(mark(X1),X2) -> x(X1,X2)
    x(X1,mark(X2)) -> x(X1,X2)
    x(active(X1),X2) -> x(X1,X2)
    x(X1,active(X2)) -> x(X1,X2)
   graph:
    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)
    x#(mark(X1),X2) -> x#(X1,X2) -> x#(X1,active(X2)) -> x#(X1,X2)
    x#(mark(X1),X2) -> x#(X1,X2) -> x#(active(X1),X2) -> x#(X1,X2)
    x#(mark(X1),X2) -> x#(X1,X2) -> x#(X1,mark(X2)) -> x#(X1,X2)
    x#(mark(X1),X2) -> x#(X1,X2) -> x#(mark(X1),X2) -> x#(X1,X2)
    x#(active(X1),X2) -> x#(X1,X2) -> x#(X1,active(X2)) -> x#(X1,X2)
    x#(active(X1),X2) -> x#(X1,X2) -> x#(active(X1),X2) -> x#(X1,X2)
    x#(active(X1),X2) -> x#(X1,X2) -> x#(X1,mark(X2)) -> x#(X1,X2)
    x#(active(X1),X2) -> x#(X1,X2) -> x#(mark(X1),X2) -> x#(X1,X2)
    x#(X1,mark(X2)) -> x#(X1,X2) -> x#(X1,active(X2)) -> x#(X1,X2)
    x#(X1,mark(X2)) -> x#(X1,X2) -> x#(active(X1),X2) -> x#(X1,X2)
    x#(X1,mark(X2)) -> x#(X1,X2) -> x#(X1,mark(X2)) -> x#(X1,X2)
    x#(X1,mark(X2)) -> x#(X1,X2) -> x#(mark(X1),X2) -> x#(X1,X2)
    x#(X1,active(X2)) -> x#(X1,X2) -> x#(X1,active(X2)) -> x#(X1,X2)
    x#(X1,active(X2)) -> x#(X1,X2) -> x#(active(X1),X2) -> x#(X1,X2)
    x#(X1,active(X2)) -> x#(X1,X2) -> x#(X1,mark(X2)) -> x#(X1,X2)
    x#(X1,active(X2)) -> x#(X1,X2) -> x#(mark(X1),X2) -> x#(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)
    plus#(mark(X1),X2) -> plus#(X1,X2) ->
    plus#(X1,active(X2)) -> plus#(X1,X2)
    plus#(mark(X1),X2) -> plus#(X1,X2) ->
    plus#(active(X1),X2) -> plus#(X1,X2)
    plus#(mark(X1),X2) -> plus#(X1,X2) ->
    plus#(X1,mark(X2)) -> plus#(X1,X2)
    plus#(mark(X1),X2) -> plus#(X1,X2) ->
    plus#(mark(X1),X2) -> plus#(X1,X2)
    plus#(active(X1),X2) -> plus#(X1,X2) ->
    plus#(X1,active(X2)) -> plus#(X1,X2)
    plus#(active(X1),X2) -> plus#(X1,X2) ->
    plus#(active(X1),X2) -> plus#(X1,X2)
    plus#(active(X1),X2) -> plus#(X1,X2) ->
    plus#(X1,mark(X2)) -> plus#(X1,X2)
    plus#(active(X1),X2) -> plus#(X1,X2) ->
    plus#(mark(X1),X2) -> plus#(X1,X2)
    plus#(X1,mark(X2)) -> plus#(X1,X2) ->
    plus#(X1,active(X2)) -> plus#(X1,X2)
    plus#(X1,mark(X2)) -> plus#(X1,X2) ->
    plus#(active(X1),X2) -> plus#(X1,X2)
    plus#(X1,mark(X2)) -> plus#(X1,X2) ->
    plus#(X1,mark(X2)) -> plus#(X1,X2)
    plus#(X1,mark(X2)) -> plus#(X1,X2) ->
    plus#(mark(X1),X2) -> plus#(X1,X2)
    plus#(X1,active(X2)) -> plus#(X1,X2) ->
    plus#(X1,active(X2)) -> plus#(X1,X2)
    plus#(X1,active(X2)) -> plus#(X1,X2) ->
    plus#(active(X1),X2) -> plus#(X1,X2)
    plus#(X1,active(X2)) -> plus#(X1,X2) ->
    plus#(X1,mark(X2)) -> plus#(X1,X2)
    plus#(X1,active(X2)) -> plus#(X1,X2) ->
    plus#(mark(X1),X2) -> plus#(X1,X2)
    mark#(x(X1,X2)) -> x#(mark(X1),mark(X2)) ->
    x#(X1,active(X2)) -> x#(X1,X2)
    mark#(x(X1,X2)) -> x#(mark(X1),mark(X2)) ->
    x#(active(X1),X2) -> x#(X1,X2)
    mark#(x(X1,X2)) -> x#(mark(X1),mark(X2)) ->
    x#(X1,mark(X2)) -> x#(X1,X2)
    mark#(x(X1,X2)) -> x#(mark(X1),mark(X2)) ->
    x#(mark(X1),X2) -> x#(X1,X2)
    mark#(x(X1,X2)) -> mark#(X2) ->
    mark#(x(X1,X2)) -> active#(x(mark(X1),mark(X2)))
    mark#(x(X1,X2)) -> mark#(X2) ->
    mark#(x(X1,X2)) -> x#(mark(X1),mark(X2))
    mark#(x(X1,X2)) -> mark#(X2) -> mark#(x(X1,X2)) -> mark#(X1)
    mark#(x(X1,X2)) -> mark#(X2) -> mark#(x(X1,X2)) -> mark#(X2)
    mark#(x(X1,X2)) -> mark#(X2) -> mark#(s(X)) -> active#(s(mark(X)))
    mark#(x(X1,X2)) -> mark#(X2) -> mark#(s(X)) -> s#(mark(X))
    mark#(x(X1,X2)) -> mark#(X2) -> mark#(s(X)) -> mark#(X)
    mark#(x(X1,X2)) -> mark#(X2) -> mark#(0()) -> active#(0())
    mark#(x(X1,X2)) -> mark#(X2) ->
    mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
    mark#(x(X1,X2)) -> mark#(X2) ->
    mark#(plus(X1,X2)) -> plus#(mark(X1),mark(X2))
    mark#(x(X1,X2)) -> mark#(X2) -> mark#(plus(X1,X2)) -> mark#(X1)
    mark#(x(X1,X2)) -> mark#(X2) -> mark#(plus(X1,X2)) -> mark#(X2)
    mark#(x(X1,X2)) -> mark#(X2) -> mark#(tt()) -> active#(tt())
    mark#(x(X1,X2)) -> mark#(X2) ->
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    mark#(x(X1,X2)) -> mark#(X2) ->
    mark#(and(X1,X2)) -> and#(mark(X1),X2)
    mark#(x(X1,X2)) -> mark#(X2) -> mark#(and(X1,X2)) -> mark#(X1)
    mark#(x(X1,X2)) -> mark#(X1) ->
    mark#(x(X1,X2)) -> active#(x(mark(X1),mark(X2)))
    mark#(x(X1,X2)) -> mark#(X1) ->
    mark#(x(X1,X2)) -> x#(mark(X1),mark(X2))
    mark#(x(X1,X2)) -> mark#(X1) -> mark#(x(X1,X2)) -> mark#(X1)
    mark#(x(X1,X2)) -> mark#(X1) -> mark#(x(X1,X2)) -> mark#(X2)
    mark#(x(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> active#(s(mark(X)))
    mark#(x(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> s#(mark(X))
    mark#(x(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X)
    mark#(x(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
    mark#(x(X1,X2)) -> mark#(X1) ->
    mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
    mark#(x(X1,X2)) -> mark#(X1) ->
    mark#(plus(X1,X2)) -> plus#(mark(X1),mark(X2))
    mark#(x(X1,X2)) -> mark#(X1) -> mark#(plus(X1,X2)) -> mark#(X1)
    mark#(x(X1,X2)) -> mark#(X1) -> mark#(plus(X1,X2)) -> mark#(X2)
    mark#(x(X1,X2)) -> mark#(X1) -> mark#(tt()) -> active#(tt())
    mark#(x(X1,X2)) -> mark#(X1) ->
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    mark#(x(X1,X2)) -> mark#(X1) ->
    mark#(and(X1,X2)) -> and#(mark(X1),X2)
    mark#(x(X1,X2)) -> mark#(X1) ->
    mark#(and(X1,X2)) -> mark#(X1)
    mark#(x(X1,X2)) -> active#(x(mark(X1),mark(X2))) ->
    active#(x(N,s(M))) -> mark#(plus(x(N,M),N))
    mark#(x(X1,X2)) -> active#(x(mark(X1),mark(X2))) ->
    active#(x(N,s(M))) -> plus#(x(N,M),N)
    mark#(x(X1,X2)) -> active#(x(mark(X1),mark(X2))) ->
    active#(x(N,s(M))) -> x#(N,M)
    mark#(x(X1,X2)) -> active#(x(mark(X1),mark(X2))) ->
    active#(x(N,0())) -> mark#(0())
    mark#(x(X1,X2)) -> active#(x(mark(X1),mark(X2))) ->
    active#(plus(N,s(M))) -> mark#(s(plus(N,M)))
    mark#(x(X1,X2)) -> active#(x(mark(X1),mark(X2))) ->
    active#(plus(N,s(M))) -> s#(plus(N,M))
    mark#(x(X1,X2)) -> active#(x(mark(X1),mark(X2))) ->
    active#(plus(N,s(M))) -> plus#(N,M)
    mark#(x(X1,X2)) -> active#(x(mark(X1),mark(X2))) ->
    active#(plus(N,0())) -> mark#(N)
    mark#(x(X1,X2)) -> active#(x(mark(X1),mark(X2))) ->
    active#(and(tt(),X)) -> mark#(X)
    mark#(s(X)) -> s#(mark(X)) -> s#(active(X)) -> s#(X)
    mark#(s(X)) -> s#(mark(X)) -> s#(mark(X)) -> s#(X)
    mark#(s(X)) -> mark#(X) ->
    mark#(x(X1,X2)) -> active#(x(mark(X1),mark(X2)))
    mark#(s(X)) -> mark#(X) -> mark#(x(X1,X2)) -> x#(mark(X1),mark(X2))
    mark#(s(X)) -> mark#(X) -> mark#(x(X1,X2)) -> mark#(X1)
    mark#(s(X)) -> mark#(X) -> mark#(x(X1,X2)) -> mark#(X2)
    mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
    mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> s#(mark(X))
    mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    mark#(s(X)) -> mark#(X) -> mark#(0()) -> active#(0())
    mark#(s(X)) -> mark#(X) ->
    mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
    mark#(s(X)) -> mark#(X) ->
    mark#(plus(X1,X2)) -> plus#(mark(X1),mark(X2))
    mark#(s(X)) -> mark#(X) -> mark#(plus(X1,X2)) -> mark#(X1)
    mark#(s(X)) -> mark#(X) -> mark#(plus(X1,X2)) -> mark#(X2)
    mark#(s(X)) -> mark#(X) -> mark#(tt()) -> active#(tt())
    mark#(s(X)) -> mark#(X) ->
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    mark#(s(X)) -> mark#(X) -> mark#(and(X1,X2)) -> and#(mark(X1),X2)
    mark#(s(X)) -> mark#(X) -> mark#(and(X1,X2)) -> mark#(X1)
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(x(N,s(M))) -> mark#(plus(x(N,M),N))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(x(N,s(M))) -> plus#(x(N,M),N)
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(x(N,s(M))) -> x#(N,M)
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(x(N,0())) -> mark#(0())
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(plus(N,s(M))) -> mark#(s(plus(N,M)))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(plus(N,s(M))) -> s#(plus(N,M))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(plus(N,s(M))) -> plus#(N,M)
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(plus(N,0())) -> mark#(N)
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(and(tt(),X)) -> mark#(X)
    mark#(plus(X1,X2)) -> plus#(mark(X1),mark(X2)) ->
    plus#(X1,active(X2)) -> plus#(X1,X2)
    mark#(plus(X1,X2)) -> plus#(mark(X1),mark(X2)) ->
    plus#(active(X1),X2) -> plus#(X1,X2)
    mark#(plus(X1,X2)) -> plus#(mark(X1),mark(X2)) ->
    plus#(X1,mark(X2)) -> plus#(X1,X2)
    mark#(plus(X1,X2)) -> plus#(mark(X1),mark(X2)) ->
    plus#(mark(X1),X2) -> plus#(X1,X2)
    mark#(plus(X1,X2)) -> mark#(X2) ->
    mark#(x(X1,X2)) -> active#(x(mark(X1),mark(X2)))
    mark#(plus(X1,X2)) -> mark#(X2) ->
    mark#(x(X1,X2)) -> x#(mark(X1),mark(X2))
    mark#(plus(X1,X2)) -> mark#(X2) -> mark#(x(X1,X2)) -> mark#(X1)
    mark#(plus(X1,X2)) -> mark#(X2) -> mark#(x(X1,X2)) -> mark#(X2)
    mark#(plus(X1,X2)) -> mark#(X2) ->
    mark#(s(X)) -> active#(s(mark(X)))
    mark#(plus(X1,X2)) -> mark#(X2) -> mark#(s(X)) -> s#(mark(X))
    mark#(plus(X1,X2)) -> mark#(X2) -> mark#(s(X)) -> mark#(X)
    mark#(plus(X1,X2)) -> mark#(X2) -> mark#(0()) -> active#(0())
    mark#(plus(X1,X2)) -> mark#(X2) ->
    mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
    mark#(plus(X1,X2)) -> mark#(X2) ->
    mark#(plus(X1,X2)) -> plus#(mark(X1),mark(X2))
    mark#(plus(X1,X2)) -> mark#(X2) ->
    mark#(plus(X1,X2)) -> mark#(X1)
    mark#(plus(X1,X2)) -> mark#(X2) ->
    mark#(plus(X1,X2)) -> mark#(X2)
    mark#(plus(X1,X2)) -> mark#(X2) -> mark#(tt()) -> active#(tt())
    mark#(plus(X1,X2)) -> mark#(X2) ->
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    mark#(plus(X1,X2)) -> mark#(X2) ->
    mark#(and(X1,X2)) -> and#(mark(X1),X2)
    mark#(plus(X1,X2)) -> mark#(X2) ->
    mark#(and(X1,X2)) -> mark#(X1)
    mark#(plus(X1,X2)) -> mark#(X1) ->
    mark#(x(X1,X2)) -> active#(x(mark(X1),mark(X2)))
    mark#(plus(X1,X2)) -> mark#(X1) ->
    mark#(x(X1,X2)) -> x#(mark(X1),mark(X2))
    mark#(plus(X1,X2)) -> mark#(X1) -> mark#(x(X1,X2)) -> mark#(X1)
    mark#(plus(X1,X2)) -> mark#(X1) -> mark#(x(X1,X2)) -> mark#(X2)
    mark#(plus(X1,X2)) -> mark#(X1) ->
    mark#(s(X)) -> active#(s(mark(X)))
    mark#(plus(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> s#(mark(X))
    mark#(plus(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X)
    mark#(plus(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
    mark#(plus(X1,X2)) -> mark#(X1) ->
    mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
    mark#(plus(X1,X2)) -> mark#(X1) ->
    mark#(plus(X1,X2)) -> plus#(mark(X1),mark(X2))
    mark#(plus(X1,X2)) -> mark#(X1) ->
    mark#(plus(X1,X2)) -> mark#(X1)
    mark#(plus(X1,X2)) -> mark#(X1) ->
    mark#(plus(X1,X2)) -> mark#(X2)
    mark#(plus(X1,X2)) -> mark#(X1) -> mark#(tt()) -> active#(tt())
    mark#(plus(X1,X2)) -> mark#(X1) ->
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    mark#(plus(X1,X2)) -> mark#(X1) ->
    mark#(and(X1,X2)) -> and#(mark(X1),X2)
    mark#(plus(X1,X2)) -> mark#(X1) ->
    mark#(and(X1,X2)) -> mark#(X1)
    mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) ->
    active#(x(N,s(M))) -> mark#(plus(x(N,M),N))
    mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) ->
    active#(x(N,s(M))) -> plus#(x(N,M),N)
    mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) ->
    active#(x(N,s(M))) -> x#(N,M)
    mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) ->
    active#(x(N,0())) -> mark#(0())
    mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) ->
    active#(plus(N,s(M))) -> mark#(s(plus(N,M)))
    mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) ->
    active#(plus(N,s(M))) -> s#(plus(N,M))
    mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) ->
    active#(plus(N,s(M))) -> plus#(N,M)
    mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) ->
    active#(plus(N,0())) -> mark#(N)
    mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) ->
    active#(and(tt(),X)) -> mark#(X)
    mark#(0()) -> active#(0()) ->
    active#(x(N,s(M))) -> mark#(plus(x(N,M),N))
    mark#(0()) -> active#(0()) -> active#(x(N,s(M))) -> plus#(x(N,M),N)
    mark#(0()) -> active#(0()) -> active#(x(N,s(M))) -> x#(N,M)
    mark#(0()) -> active#(0()) -> active#(x(N,0())) -> mark#(0())
    mark#(0()) -> active#(0()) ->
    active#(plus(N,s(M))) -> mark#(s(plus(N,M)))
    mark#(0()) -> active#(0()) -> active#(plus(N,s(M))) -> s#(plus(N,M))
    mark#(0()) -> active#(0()) -> active#(plus(N,s(M))) -> plus#(N,M)
    mark#(0()) -> active#(0()) -> active#(plus(N,0())) -> mark#(N)
    mark#(0()) -> active#(0()) ->
    active#(and(tt(),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#(x(X1,X2)) -> active#(x(mark(X1),mark(X2)))
    mark#(and(X1,X2)) -> mark#(X1) ->
    mark#(x(X1,X2)) -> x#(mark(X1),mark(X2))
    mark#(and(X1,X2)) -> mark#(X1) -> mark#(x(X1,X2)) -> mark#(X1)
    mark#(and(X1,X2)) -> mark#(X1) -> mark#(x(X1,X2)) -> mark#(X2)
    mark#(and(X1,X2)) -> mark#(X1) ->
    mark#(s(X)) -> active#(s(mark(X)))
    mark#(and(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> s#(mark(X))
    mark#(and(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X)
    mark#(and(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
    mark#(and(X1,X2)) -> mark#(X1) ->
    mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
    mark#(and(X1,X2)) -> mark#(X1) ->
    mark#(plus(X1,X2)) -> plus#(mark(X1),mark(X2))
    mark#(and(X1,X2)) -> mark#(X1) -> mark#(plus(X1,X2)) -> mark#(X1)
    mark#(and(X1,X2)) -> mark#(X1) -> mark#(plus(X1,X2)) -> mark#(X2)
    mark#(and(X1,X2)) -> mark#(X1) -> mark#(tt()) -> active#(tt())
    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#(x(N,s(M))) -> mark#(plus(x(N,M),N))
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(x(N,s(M))) -> plus#(x(N,M),N)
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(x(N,s(M))) -> x#(N,M)
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(x(N,0())) -> mark#(0())
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(plus(N,s(M))) -> mark#(s(plus(N,M)))
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(plus(N,s(M))) -> s#(plus(N,M))
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(plus(N,s(M))) -> plus#(N,M)
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(plus(N,0())) -> mark#(N)
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(and(tt(),X)) -> mark#(X)
    mark#(tt()) -> active#(tt()) ->
    active#(x(N,s(M))) -> mark#(plus(x(N,M),N))
    mark#(tt()) -> active#(tt()) ->
    active#(x(N,s(M))) -> plus#(x(N,M),N)
    mark#(tt()) -> active#(tt()) -> active#(x(N,s(M))) -> x#(N,M)
    mark#(tt()) -> active#(tt()) -> active#(x(N,0())) -> mark#(0())
    mark#(tt()) -> active#(tt()) ->
    active#(plus(N,s(M))) -> mark#(s(plus(N,M)))
    mark#(tt()) -> active#(tt()) ->
    active#(plus(N,s(M))) -> s#(plus(N,M))
    mark#(tt()) -> active#(tt()) -> active#(plus(N,s(M))) -> plus#(N,M)
    mark#(tt()) -> active#(tt()) -> active#(plus(N,0())) -> mark#(N)
    mark#(tt()) -> active#(tt()) -> active#(and(tt(),X)) -> mark#(X)
    active#(x(N,s(M))) -> x#(N,M) -> x#(X1,active(X2)) -> x#(X1,X2)
    active#(x(N,s(M))) -> x#(N,M) -> x#(active(X1),X2) -> x#(X1,X2)
    active#(x(N,s(M))) -> x#(N,M) -> x#(X1,mark(X2)) -> x#(X1,X2)
    active#(x(N,s(M))) -> x#(N,M) ->
    x#(mark(X1),X2) -> x#(X1,X2)
    active#(x(N,s(M))) -> plus#(x(N,M),N) ->
    plus#(X1,active(X2)) -> plus#(X1,X2)
    active#(x(N,s(M))) -> plus#(x(N,M),N) ->
    plus#(active(X1),X2) -> plus#(X1,X2)
    active#(x(N,s(M))) -> plus#(x(N,M),N) ->
    plus#(X1,mark(X2)) -> plus#(X1,X2)
    active#(x(N,s(M))) -> plus#(x(N,M),N) ->
    plus#(mark(X1),X2) -> plus#(X1,X2)
    active#(x(N,s(M))) -> mark#(plus(x(N,M),N)) ->
    mark#(x(X1,X2)) -> active#(x(mark(X1),mark(X2)))
    active#(x(N,s(M))) -> mark#(plus(x(N,M),N)) ->
    mark#(x(X1,X2)) -> x#(mark(X1),mark(X2))
    active#(x(N,s(M))) -> mark#(plus(x(N,M),N)) ->
    mark#(x(X1,X2)) -> mark#(X1)
    active#(x(N,s(M))) -> mark#(plus(x(N,M),N)) ->
    mark#(x(X1,X2)) -> mark#(X2)
    active#(x(N,s(M))) -> mark#(plus(x(N,M),N)) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(x(N,s(M))) -> mark#(plus(x(N,M),N)) ->
    mark#(s(X)) -> s#(mark(X))
    active#(x(N,s(M))) -> mark#(plus(x(N,M),N)) ->
    mark#(s(X)) -> mark#(X)
    active#(x(N,s(M))) -> mark#(plus(x(N,M),N)) ->
    mark#(0()) -> active#(0())
    active#(x(N,s(M))) -> mark#(plus(x(N,M),N)) ->
    mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
    active#(x(N,s(M))) -> mark#(plus(x(N,M),N)) ->
    mark#(plus(X1,X2)) -> plus#(mark(X1),mark(X2))
    active#(x(N,s(M))) -> mark#(plus(x(N,M),N)) ->
    mark#(plus(X1,X2)) -> mark#(X1)
    active#(x(N,s(M))) -> mark#(plus(x(N,M),N)) ->
    mark#(plus(X1,X2)) -> mark#(X2)
    active#(x(N,s(M))) -> mark#(plus(x(N,M),N)) ->
    mark#(tt()) -> active#(tt())
    active#(x(N,s(M))) -> mark#(plus(x(N,M),N)) ->
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    active#(x(N,s(M))) -> mark#(plus(x(N,M),N)) ->
    mark#(and(X1,X2)) -> and#(mark(X1),X2)
    active#(x(N,s(M))) -> mark#(plus(x(N,M),N)) ->
    mark#(and(X1,X2)) -> mark#(X1)
    active#(x(N,0())) -> mark#(0()) ->
    mark#(x(X1,X2)) -> active#(x(mark(X1),mark(X2)))
    active#(x(N,0())) -> mark#(0()) ->
    mark#(x(X1,X2)) -> x#(mark(X1),mark(X2))
    active#(x(N,0())) -> mark#(0()) -> mark#(x(X1,X2)) -> mark#(X1)
    active#(x(N,0())) -> mark#(0()) -> mark#(x(X1,X2)) -> mark#(X2)
    active#(x(N,0())) -> mark#(0()) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(x(N,0())) -> mark#(0()) -> mark#(s(X)) -> s#(mark(X))
    active#(x(N,0())) -> mark#(0()) -> mark#(s(X)) -> mark#(X)
    active#(x(N,0())) -> mark#(0()) -> mark#(0()) -> active#(0())
    active#(x(N,0())) -> mark#(0()) ->
    mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
    active#(x(N,0())) -> mark#(0()) ->
    mark#(plus(X1,X2)) -> plus#(mark(X1),mark(X2))
    active#(x(N,0())) -> mark#(0()) ->
    mark#(plus(X1,X2)) -> mark#(X1)
    active#(x(N,0())) -> mark#(0()) ->
    mark#(plus(X1,X2)) -> mark#(X2)
    active#(x(N,0())) -> mark#(0()) -> mark#(tt()) -> active#(tt())
    active#(x(N,0())) -> mark#(0()) ->
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    active#(x(N,0())) -> mark#(0()) ->
    mark#(and(X1,X2)) -> and#(mark(X1),X2)
    active#(x(N,0())) -> mark#(0()) ->
    mark#(and(X1,X2)) -> mark#(X1)
    active#(plus(N,s(M))) -> s#(plus(N,M)) ->
    s#(active(X)) -> s#(X)
    active#(plus(N,s(M))) -> s#(plus(N,M)) ->
    s#(mark(X)) -> s#(X)
    active#(plus(N,s(M))) -> plus#(N,M) ->
    plus#(X1,active(X2)) -> plus#(X1,X2)
    active#(plus(N,s(M))) -> plus#(N,M) ->
    plus#(active(X1),X2) -> plus#(X1,X2)
    active#(plus(N,s(M))) -> plus#(N,M) ->
    plus#(X1,mark(X2)) -> plus#(X1,X2)
    active#(plus(N,s(M))) -> plus#(N,M) ->
    plus#(mark(X1),X2) -> plus#(X1,X2)
    active#(plus(N,s(M))) -> mark#(s(plus(N,M))) ->
    mark#(x(X1,X2)) -> active#(x(mark(X1),mark(X2)))
    active#(plus(N,s(M))) -> mark#(s(plus(N,M))) ->
    mark#(x(X1,X2)) -> x#(mark(X1),mark(X2))
    active#(plus(N,s(M))) -> mark#(s(plus(N,M))) ->
    mark#(x(X1,X2)) -> mark#(X1)
    active#(plus(N,s(M))) -> mark#(s(plus(N,M))) ->
    mark#(x(X1,X2)) -> mark#(X2)
    active#(plus(N,s(M))) -> mark#(s(plus(N,M))) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(plus(N,s(M))) -> mark#(s(plus(N,M))) ->
    mark#(s(X)) -> s#(mark(X))
    active#(plus(N,s(M))) -> mark#(s(plus(N,M))) ->
    mark#(s(X)) -> mark#(X)
    active#(plus(N,s(M))) -> mark#(s(plus(N,M))) ->
    mark#(0()) -> active#(0())
    active#(plus(N,s(M))) -> mark#(s(plus(N,M))) ->
    mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
    active#(plus(N,s(M))) -> mark#(s(plus(N,M))) ->
    mark#(plus(X1,X2)) -> plus#(mark(X1),mark(X2))
    active#(plus(N,s(M))) -> mark#(s(plus(N,M))) ->
    mark#(plus(X1,X2)) -> mark#(X1)
    active#(plus(N,s(M))) -> mark#(s(plus(N,M))) ->
    mark#(plus(X1,X2)) -> mark#(X2)
    active#(plus(N,s(M))) -> mark#(s(plus(N,M))) ->
    mark#(tt()) -> active#(tt())
    active#(plus(N,s(M))) -> mark#(s(plus(N,M))) ->
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    active#(plus(N,s(M))) -> mark#(s(plus(N,M))) ->
    mark#(and(X1,X2)) -> and#(mark(X1),X2)
    active#(plus(N,s(M))) -> mark#(s(plus(N,M))) ->
    mark#(and(X1,X2)) -> mark#(X1)
    active#(plus(N,0())) -> mark#(N) ->
    mark#(x(X1,X2)) -> active#(x(mark(X1),mark(X2)))
    active#(plus(N,0())) -> mark#(N) ->
    mark#(x(X1,X2)) -> x#(mark(X1),mark(X2))
    active#(plus(N,0())) -> mark#(N) ->
    mark#(x(X1,X2)) -> mark#(X1)
    active#(plus(N,0())) -> mark#(N) ->
    mark#(x(X1,X2)) -> mark#(X2)
    active#(plus(N,0())) -> mark#(N) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(plus(N,0())) -> mark#(N) -> mark#(s(X)) -> s#(mark(X))
    active#(plus(N,0())) -> mark#(N) -> mark#(s(X)) -> mark#(X)
    active#(plus(N,0())) -> mark#(N) -> mark#(0()) -> active#(0())
    active#(plus(N,0())) -> mark#(N) ->
    mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
    active#(plus(N,0())) -> mark#(N) ->
    mark#(plus(X1,X2)) -> plus#(mark(X1),mark(X2))
    active#(plus(N,0())) -> mark#(N) ->
    mark#(plus(X1,X2)) -> mark#(X1)
    active#(plus(N,0())) -> mark#(N) ->
    mark#(plus(X1,X2)) -> mark#(X2)
    active#(plus(N,0())) -> mark#(N) ->
    mark#(tt()) -> active#(tt())
    active#(plus(N,0())) -> mark#(N) ->
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    active#(plus(N,0())) -> mark#(N) ->
    mark#(and(X1,X2)) -> and#(mark(X1),X2)
    active#(plus(N,0())) -> mark#(N) ->
    mark#(and(X1,X2)) -> mark#(X1)
    active#(and(tt(),X)) -> mark#(X) ->
    mark#(x(X1,X2)) -> active#(x(mark(X1),mark(X2)))
    active#(and(tt(),X)) -> mark#(X) ->
    mark#(x(X1,X2)) -> x#(mark(X1),mark(X2))
    active#(and(tt(),X)) -> mark#(X) ->
    mark#(x(X1,X2)) -> mark#(X1)
    active#(and(tt(),X)) -> mark#(X) ->
    mark#(x(X1,X2)) -> mark#(X2)
    active#(and(tt(),X)) -> mark#(X) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(and(tt(),X)) -> mark#(X) -> mark#(s(X)) -> s#(mark(X))
    active#(and(tt(),X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    active#(and(tt(),X)) -> mark#(X) -> mark#(0()) -> active#(0())
    active#(and(tt(),X)) -> mark#(X) ->
    mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
    active#(and(tt(),X)) -> mark#(X) ->
    mark#(plus(X1,X2)) -> plus#(mark(X1),mark(X2))
    active#(and(tt(),X)) -> mark#(X) ->
    mark#(plus(X1,X2)) -> mark#(X1)
    active#(and(tt(),X)) -> mark#(X) ->
    mark#(plus(X1,X2)) -> mark#(X2)
    active#(and(tt(),X)) -> mark#(X) ->
    mark#(tt()) -> active#(tt())
    active#(and(tt(),X)) -> mark#(X) ->
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    active#(and(tt(),X)) -> mark#(X) ->
    mark#(and(X1,X2)) -> and#(mark(X1),X2)
    active#(and(tt(),X)) -> mark#(X) -> mark#(and(X1,X2)) -> mark#(X1)
   EDG Processor:
    DPs:
     active#(and(tt(),X)) -> mark#(X)
     active#(plus(N,0())) -> mark#(N)
     active#(plus(N,s(M))) -> plus#(N,M)
     active#(plus(N,s(M))) -> s#(plus(N,M))
     active#(plus(N,s(M))) -> mark#(s(plus(N,M)))
     active#(x(N,0())) -> mark#(0())
     active#(x(N,s(M))) -> x#(N,M)
     active#(x(N,s(M))) -> plus#(x(N,M),N)
     active#(x(N,s(M))) -> mark#(plus(x(N,M),N))
     mark#(and(X1,X2)) -> mark#(X1)
     mark#(and(X1,X2)) -> and#(mark(X1),X2)
     mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
     mark#(tt()) -> active#(tt())
     mark#(plus(X1,X2)) -> mark#(X2)
     mark#(plus(X1,X2)) -> mark#(X1)
     mark#(plus(X1,X2)) -> plus#(mark(X1),mark(X2))
     mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
     mark#(0()) -> active#(0())
     mark#(s(X)) -> mark#(X)
     mark#(s(X)) -> s#(mark(X))
     mark#(s(X)) -> active#(s(mark(X)))
     mark#(x(X1,X2)) -> mark#(X2)
     mark#(x(X1,X2)) -> mark#(X1)
     mark#(x(X1,X2)) -> x#(mark(X1),mark(X2))
     mark#(x(X1,X2)) -> active#(x(mark(X1),mark(X2)))
     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)
     plus#(mark(X1),X2) -> plus#(X1,X2)
     plus#(X1,mark(X2)) -> plus#(X1,X2)
     plus#(active(X1),X2) -> plus#(X1,X2)
     plus#(X1,active(X2)) -> plus#(X1,X2)
     s#(mark(X)) -> s#(X)
     s#(active(X)) -> s#(X)
     x#(mark(X1),X2) -> x#(X1,X2)
     x#(X1,mark(X2)) -> x#(X1,X2)
     x#(active(X1),X2) -> x#(X1,X2)
     x#(X1,active(X2)) -> x#(X1,X2)
    TRS:
     active(and(tt(),X)) -> mark(X)
     active(plus(N,0())) -> mark(N)
     active(plus(N,s(M))) -> mark(s(plus(N,M)))
     active(x(N,0())) -> mark(0())
     active(x(N,s(M))) -> mark(plus(x(N,M),N))
     mark(and(X1,X2)) -> active(and(mark(X1),X2))
     mark(tt()) -> active(tt())
     mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
     mark(0()) -> active(0())
     mark(s(X)) -> active(s(mark(X)))
     mark(x(X1,X2)) -> active(x(mark(X1),mark(X2)))
     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)
     plus(mark(X1),X2) -> plus(X1,X2)
     plus(X1,mark(X2)) -> plus(X1,X2)
     plus(active(X1),X2) -> plus(X1,X2)
     plus(X1,active(X2)) -> plus(X1,X2)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     x(mark(X1),X2) -> x(X1,X2)
     x(X1,mark(X2)) -> x(X1,X2)
     x(active(X1),X2) -> x(X1,X2)
     x(X1,active(X2)) -> x(X1,X2)
    graph:
     and#(mark(X1),X2) -> and#(X1,X2) ->
     and#(mark(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#(active(X1),X2) -> and#(X1,X2)
     and#(mark(X1),X2) -> and#(X1,X2) ->
     and#(X1,active(X2)) -> and#(X1,X2)
     and#(active(X1),X2) -> and#(X1,X2) ->
     and#(mark(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#(active(X1),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#(mark(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#(active(X1),X2) -> and#(X1,X2)
     and#(X1,mark(X2)) -> and#(X1,X2) ->
     and#(X1,active(X2)) -> and#(X1,X2)
     and#(X1,active(X2)) -> and#(X1,X2) ->
     and#(mark(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#(active(X1),X2) -> and#(X1,X2)
     and#(X1,active(X2)) -> and#(X1,X2) ->
     and#(X1,active(X2)) -> and#(X1,X2)
     x#(mark(X1),X2) -> x#(X1,X2) -> x#(mark(X1),X2) -> x#(X1,X2)
     x#(mark(X1),X2) -> x#(X1,X2) -> x#(X1,mark(X2)) -> x#(X1,X2)
     x#(mark(X1),X2) -> x#(X1,X2) -> x#(active(X1),X2) -> x#(X1,X2)
     x#(mark(X1),X2) -> x#(X1,X2) -> x#(X1,active(X2)) -> x#(X1,X2)
     x#(active(X1),X2) -> x#(X1,X2) -> x#(mark(X1),X2) -> x#(X1,X2)
     x#(active(X1),X2) -> x#(X1,X2) -> x#(X1,mark(X2)) -> x#(X1,X2)
     x#(active(X1),X2) -> x#(X1,X2) -> x#(active(X1),X2) -> x#(X1,X2)
     x#(active(X1),X2) -> x#(X1,X2) -> x#(X1,active(X2)) -> x#(X1,X2)
     x#(X1,mark(X2)) -> x#(X1,X2) -> x#(mark(X1),X2) -> x#(X1,X2)
     x#(X1,mark(X2)) -> x#(X1,X2) -> x#(X1,mark(X2)) -> x#(X1,X2)
     x#(X1,mark(X2)) -> x#(X1,X2) -> x#(active(X1),X2) -> x#(X1,X2)
     x#(X1,mark(X2)) -> x#(X1,X2) -> x#(X1,active(X2)) -> x#(X1,X2)
     x#(X1,active(X2)) -> x#(X1,X2) -> x#(mark(X1),X2) -> x#(X1,X2)
     x#(X1,active(X2)) -> x#(X1,X2) -> x#(X1,mark(X2)) -> x#(X1,X2)
     x#(X1,active(X2)) -> x#(X1,X2) -> x#(active(X1),X2) -> x#(X1,X2)
     x#(X1,active(X2)) -> x#(X1,X2) -> x#(X1,active(X2)) -> x#(X1,X2)
     s#(mark(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
     s#(mark(X)) -> s#(X) -> s#(active(X)) -> s#(X)
     s#(active(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
     s#(active(X)) -> s#(X) -> s#(active(X)) -> s#(X)
     plus#(mark(X1),X2) -> plus#(X1,X2) ->
     plus#(mark(X1),X2) -> plus#(X1,X2)
     plus#(mark(X1),X2) -> plus#(X1,X2) ->
     plus#(X1,mark(X2)) -> plus#(X1,X2)
     plus#(mark(X1),X2) -> plus#(X1,X2) ->
     plus#(active(X1),X2) -> plus#(X1,X2)
     plus#(mark(X1),X2) -> plus#(X1,X2) ->
     plus#(X1,active(X2)) -> plus#(X1,X2)
     plus#(active(X1),X2) -> plus#(X1,X2) ->
     plus#(mark(X1),X2) -> plus#(X1,X2)
     plus#(active(X1),X2) -> plus#(X1,X2) ->
     plus#(X1,mark(X2)) -> plus#(X1,X2)
     plus#(active(X1),X2) -> plus#(X1,X2) ->
     plus#(active(X1),X2) -> plus#(X1,X2)
     plus#(active(X1),X2) -> plus#(X1,X2) ->
     plus#(X1,active(X2)) -> plus#(X1,X2)
     plus#(X1,mark(X2)) -> plus#(X1,X2) ->
     plus#(mark(X1),X2) -> plus#(X1,X2)
     plus#(X1,mark(X2)) -> plus#(X1,X2) ->
     plus#(X1,mark(X2)) -> plus#(X1,X2)
     plus#(X1,mark(X2)) -> plus#(X1,X2) ->
     plus#(active(X1),X2) -> plus#(X1,X2)
     plus#(X1,mark(X2)) -> plus#(X1,X2) ->
     plus#(X1,active(X2)) -> plus#(X1,X2)
     plus#(X1,active(X2)) -> plus#(X1,X2) ->
     plus#(mark(X1),X2) -> plus#(X1,X2)
     plus#(X1,active(X2)) -> plus#(X1,X2) ->
     plus#(X1,mark(X2)) -> plus#(X1,X2)
     plus#(X1,active(X2)) -> plus#(X1,X2) ->
     plus#(active(X1),X2) -> plus#(X1,X2)
     plus#(X1,active(X2)) -> plus#(X1,X2) ->
     plus#(X1,active(X2)) -> plus#(X1,X2)
     mark#(x(X1,X2)) -> x#(mark(X1),mark(X2)) ->
     x#(mark(X1),X2) -> x#(X1,X2)
     mark#(x(X1,X2)) -> x#(mark(X1),mark(X2)) ->
     x#(X1,mark(X2)) -> x#(X1,X2)
     mark#(x(X1,X2)) -> x#(mark(X1),mark(X2)) ->
     x#(active(X1),X2) -> x#(X1,X2)
     mark#(x(X1,X2)) -> x#(mark(X1),mark(X2)) ->
     x#(X1,active(X2)) -> x#(X1,X2)
     mark#(x(X1,X2)) -> mark#(X2) -> mark#(and(X1,X2)) -> mark#(X1)
     mark#(x(X1,X2)) -> mark#(X2) ->
     mark#(and(X1,X2)) -> and#(mark(X1),X2)
     mark#(x(X1,X2)) -> mark#(X2) ->
     mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
     mark#(x(X1,X2)) -> mark#(X2) -> mark#(tt()) -> active#(tt())
     mark#(x(X1,X2)) -> mark#(X2) -> mark#(plus(X1,X2)) -> mark#(X2)
     mark#(x(X1,X2)) -> mark#(X2) -> mark#(plus(X1,X2)) -> mark#(X1)
     mark#(x(X1,X2)) -> mark#(X2) ->
     mark#(plus(X1,X2)) -> plus#(mark(X1),mark(X2))
     mark#(x(X1,X2)) -> mark#(X2) ->
     mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
     mark#(x(X1,X2)) -> mark#(X2) -> mark#(0()) -> active#(0())
     mark#(x(X1,X2)) -> mark#(X2) -> mark#(s(X)) -> mark#(X)
     mark#(x(X1,X2)) -> mark#(X2) -> mark#(s(X)) -> s#(mark(X))
     mark#(x(X1,X2)) -> mark#(X2) -> mark#(s(X)) -> active#(s(mark(X)))
     mark#(x(X1,X2)) -> mark#(X2) -> mark#(x(X1,X2)) -> mark#(X2)
     mark#(x(X1,X2)) -> mark#(X2) -> mark#(x(X1,X2)) -> mark#(X1)
     mark#(x(X1,X2)) -> mark#(X2) ->
     mark#(x(X1,X2)) -> x#(mark(X1),mark(X2))
     mark#(x(X1,X2)) -> mark#(X2) ->
     mark#(x(X1,X2)) -> active#(x(mark(X1),mark(X2)))
     mark#(x(X1,X2)) -> mark#(X1) -> mark#(and(X1,X2)) -> mark#(X1)
     mark#(x(X1,X2)) -> mark#(X1) ->
     mark#(and(X1,X2)) -> and#(mark(X1),X2)
     mark#(x(X1,X2)) -> mark#(X1) ->
     mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
     mark#(x(X1,X2)) -> mark#(X1) -> mark#(tt()) -> active#(tt())
     mark#(x(X1,X2)) -> mark#(X1) -> mark#(plus(X1,X2)) -> mark#(X2)
     mark#(x(X1,X2)) -> mark#(X1) -> mark#(plus(X1,X2)) -> mark#(X1)
     mark#(x(X1,X2)) -> mark#(X1) ->
     mark#(plus(X1,X2)) -> plus#(mark(X1),mark(X2))
     mark#(x(X1,X2)) -> mark#(X1) ->
     mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
     mark#(x(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
     mark#(x(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X)
     mark#(x(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> s#(mark(X))
     mark#(x(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> active#(s(mark(X)))
     mark#(x(X1,X2)) -> mark#(X1) -> mark#(x(X1,X2)) -> mark#(X2)
     mark#(x(X1,X2)) -> mark#(X1) -> mark#(x(X1,X2)) -> mark#(X1)
     mark#(x(X1,X2)) -> mark#(X1) ->
     mark#(x(X1,X2)) -> x#(mark(X1),mark(X2))
     mark#(x(X1,X2)) -> mark#(X1) ->
     mark#(x(X1,X2)) -> active#(x(mark(X1),mark(X2)))
     mark#(x(X1,X2)) -> active#(x(mark(X1),mark(X2))) ->
     active#(and(tt(),X)) -> mark#(X)
     mark#(x(X1,X2)) -> active#(x(mark(X1),mark(X2))) ->
     active#(plus(N,0())) -> mark#(N)
     mark#(x(X1,X2)) -> active#(x(mark(X1),mark(X2))) ->
     active#(plus(N,s(M))) -> plus#(N,M)
     mark#(x(X1,X2)) -> active#(x(mark(X1),mark(X2))) ->
     active#(plus(N,s(M))) -> s#(plus(N,M))
     mark#(x(X1,X2)) -> active#(x(mark(X1),mark(X2))) ->
     active#(plus(N,s(M))) -> mark#(s(plus(N,M)))
     mark#(x(X1,X2)) -> active#(x(mark(X1),mark(X2))) ->
     active#(x(N,0())) -> mark#(0())
     mark#(x(X1,X2)) -> active#(x(mark(X1),mark(X2))) ->
     active#(x(N,s(M))) -> x#(N,M)
     mark#(x(X1,X2)) -> active#(x(mark(X1),mark(X2))) ->
     active#(x(N,s(M))) -> plus#(x(N,M),N)
     mark#(x(X1,X2)) -> active#(x(mark(X1),mark(X2))) ->
     active#(x(N,s(M))) -> mark#(plus(x(N,M),N))
     mark#(s(X)) -> s#(mark(X)) -> s#(mark(X)) -> s#(X)
     mark#(s(X)) -> s#(mark(X)) -> s#(active(X)) -> s#(X)
     mark#(s(X)) -> mark#(X) -> mark#(and(X1,X2)) -> mark#(X1)
     mark#(s(X)) -> mark#(X) -> mark#(and(X1,X2)) -> and#(mark(X1),X2)
     mark#(s(X)) -> mark#(X) ->
     mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
     mark#(s(X)) -> mark#(X) -> mark#(tt()) -> active#(tt())
     mark#(s(X)) -> mark#(X) -> mark#(plus(X1,X2)) -> mark#(X2)
     mark#(s(X)) -> mark#(X) -> mark#(plus(X1,X2)) -> mark#(X1)
     mark#(s(X)) -> mark#(X) ->
     mark#(plus(X1,X2)) -> plus#(mark(X1),mark(X2))
     mark#(s(X)) -> mark#(X) ->
     mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
     mark#(s(X)) -> mark#(X) -> mark#(0()) -> active#(0())
     mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
     mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> s#(mark(X))
     mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
     mark#(s(X)) -> mark#(X) -> mark#(x(X1,X2)) -> mark#(X2)
     mark#(s(X)) -> mark#(X) -> mark#(x(X1,X2)) -> mark#(X1)
     mark#(s(X)) -> mark#(X) -> mark#(x(X1,X2)) -> x#(mark(X1),mark(X2))
     mark#(s(X)) -> mark#(X) ->
     mark#(x(X1,X2)) -> active#(x(mark(X1),mark(X2)))
     mark#(s(X)) -> active#(s(mark(X))) ->
     active#(and(tt(),X)) -> mark#(X)
     mark#(s(X)) -> active#(s(mark(X))) ->
     active#(plus(N,0())) -> mark#(N)
     mark#(s(X)) -> active#(s(mark(X))) ->
     active#(plus(N,s(M))) -> plus#(N,M)
     mark#(s(X)) -> active#(s(mark(X))) ->
     active#(plus(N,s(M))) -> s#(plus(N,M))
     mark#(s(X)) -> active#(s(mark(X))) ->
     active#(plus(N,s(M))) -> mark#(s(plus(N,M)))
     mark#(s(X)) -> active#(s(mark(X))) ->
     active#(x(N,0())) -> mark#(0())
     mark#(s(X)) -> active#(s(mark(X))) ->
     active#(x(N,s(M))) -> x#(N,M)
     mark#(s(X)) -> active#(s(mark(X))) ->
     active#(x(N,s(M))) -> plus#(x(N,M),N)
     mark#(s(X)) -> active#(s(mark(X))) ->
     active#(x(N,s(M))) -> mark#(plus(x(N,M),N))
     mark#(plus(X1,X2)) -> plus#(mark(X1),mark(X2)) ->
     plus#(mark(X1),X2) -> plus#(X1,X2)
     mark#(plus(X1,X2)) -> plus#(mark(X1),mark(X2)) ->
     plus#(X1,mark(X2)) -> plus#(X1,X2)
     mark#(plus(X1,X2)) -> plus#(mark(X1),mark(X2)) ->
     plus#(active(X1),X2) -> plus#(X1,X2)
     mark#(plus(X1,X2)) -> plus#(mark(X1),mark(X2)) ->
     plus#(X1,active(X2)) -> plus#(X1,X2)
     mark#(plus(X1,X2)) -> mark#(X2) ->
     mark#(and(X1,X2)) -> mark#(X1)
     mark#(plus(X1,X2)) -> mark#(X2) ->
     mark#(and(X1,X2)) -> and#(mark(X1),X2)
     mark#(plus(X1,X2)) -> mark#(X2) ->
     mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
     mark#(plus(X1,X2)) -> mark#(X2) -> mark#(tt()) -> active#(tt())
     mark#(plus(X1,X2)) -> mark#(X2) ->
     mark#(plus(X1,X2)) -> mark#(X2)
     mark#(plus(X1,X2)) -> mark#(X2) ->
     mark#(plus(X1,X2)) -> mark#(X1)
     mark#(plus(X1,X2)) -> mark#(X2) ->
     mark#(plus(X1,X2)) -> plus#(mark(X1),mark(X2))
     mark#(plus(X1,X2)) -> mark#(X2) ->
     mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
     mark#(plus(X1,X2)) -> mark#(X2) -> mark#(0()) -> active#(0())
     mark#(plus(X1,X2)) -> mark#(X2) -> mark#(s(X)) -> mark#(X)
     mark#(plus(X1,X2)) -> mark#(X2) -> mark#(s(X)) -> s#(mark(X))
     mark#(plus(X1,X2)) -> mark#(X2) ->
     mark#(s(X)) -> active#(s(mark(X)))
     mark#(plus(X1,X2)) -> mark#(X2) -> mark#(x(X1,X2)) -> mark#(X2)
     mark#(plus(X1,X2)) -> mark#(X2) -> mark#(x(X1,X2)) -> mark#(X1)
     mark#(plus(X1,X2)) -> mark#(X2) ->
     mark#(x(X1,X2)) -> x#(mark(X1),mark(X2))
     mark#(plus(X1,X2)) -> mark#(X2) ->
     mark#(x(X1,X2)) -> active#(x(mark(X1),mark(X2)))
     mark#(plus(X1,X2)) -> mark#(X1) ->
     mark#(and(X1,X2)) -> mark#(X1)
     mark#(plus(X1,X2)) -> mark#(X1) ->
     mark#(and(X1,X2)) -> and#(mark(X1),X2)
     mark#(plus(X1,X2)) -> mark#(X1) ->
     mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
     mark#(plus(X1,X2)) -> mark#(X1) -> mark#(tt()) -> active#(tt())
     mark#(plus(X1,X2)) -> mark#(X1) ->
     mark#(plus(X1,X2)) -> mark#(X2)
     mark#(plus(X1,X2)) -> mark#(X1) ->
     mark#(plus(X1,X2)) -> mark#(X1)
     mark#(plus(X1,X2)) -> mark#(X1) ->
     mark#(plus(X1,X2)) -> plus#(mark(X1),mark(X2))
     mark#(plus(X1,X2)) -> mark#(X1) ->
     mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
     mark#(plus(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
     mark#(plus(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X)
     mark#(plus(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> s#(mark(X))
     mark#(plus(X1,X2)) -> mark#(X1) ->
     mark#(s(X)) -> active#(s(mark(X)))
     mark#(plus(X1,X2)) -> mark#(X1) -> mark#(x(X1,X2)) -> mark#(X2)
     mark#(plus(X1,X2)) -> mark#(X1) -> mark#(x(X1,X2)) -> mark#(X1)
     mark#(plus(X1,X2)) -> mark#(X1) ->
     mark#(x(X1,X2)) -> x#(mark(X1),mark(X2))
     mark#(plus(X1,X2)) -> mark#(X1) ->
     mark#(x(X1,X2)) -> active#(x(mark(X1),mark(X2)))
     mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) ->
     active#(and(tt(),X)) -> mark#(X)
     mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) ->
     active#(plus(N,0())) -> mark#(N)
     mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) ->
     active#(plus(N,s(M))) -> plus#(N,M)
     mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) ->
     active#(plus(N,s(M))) -> s#(plus(N,M))
     mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) ->
     active#(plus(N,s(M))) -> mark#(s(plus(N,M)))
     mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) ->
     active#(x(N,0())) -> mark#(0())
     mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) ->
     active#(x(N,s(M))) -> x#(N,M)
     mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) ->
     active#(x(N,s(M))) -> plus#(x(N,M),N)
     mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) ->
     active#(x(N,s(M))) -> mark#(plus(x(N,M),N))
     mark#(and(X1,X2)) -> and#(mark(X1),X2) ->
     and#(mark(X1),X2) -> and#(X1,X2)
     mark#(and(X1,X2)) -> and#(mark(X1),X2) ->
     and#(active(X1),X2) -> and#(X1,X2)
     mark#(and(X1,X2)) -> mark#(X1) -> mark#(and(X1,X2)) -> mark#(X1)
     mark#(and(X1,X2)) -> mark#(X1) ->
     mark#(and(X1,X2)) -> and#(mark(X1),X2)
     mark#(and(X1,X2)) -> mark#(X1) ->
     mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
     mark#(and(X1,X2)) -> mark#(X1) -> mark#(tt()) -> active#(tt())
     mark#(and(X1,X2)) -> mark#(X1) ->
     mark#(plus(X1,X2)) -> mark#(X2)
     mark#(and(X1,X2)) -> mark#(X1) ->
     mark#(plus(X1,X2)) -> mark#(X1)
     mark#(and(X1,X2)) -> mark#(X1) ->
     mark#(plus(X1,X2)) -> plus#(mark(X1),mark(X2))
     mark#(and(X1,X2)) -> mark#(X1) ->
     mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
     mark#(and(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
     mark#(and(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X)
     mark#(and(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> s#(mark(X))
     mark#(and(X1,X2)) -> mark#(X1) ->
     mark#(s(X)) -> active#(s(mark(X)))
     mark#(and(X1,X2)) -> mark#(X1) -> mark#(x(X1,X2)) -> mark#(X2)
     mark#(and(X1,X2)) -> mark#(X1) -> mark#(x(X1,X2)) -> mark#(X1)
     mark#(and(X1,X2)) -> mark#(X1) ->
     mark#(x(X1,X2)) -> x#(mark(X1),mark(X2))
     mark#(and(X1,X2)) -> mark#(X1) ->
     mark#(x(X1,X2)) -> active#(x(mark(X1),mark(X2)))
     mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
     active#(and(tt(),X)) -> mark#(X)
     mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
     active#(plus(N,0())) -> mark#(N)
     mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
     active#(plus(N,s(M))) -> plus#(N,M)
     mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
     active#(plus(N,s(M))) -> s#(plus(N,M))
     mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
     active#(plus(N,s(M))) -> mark#(s(plus(N,M)))
     mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
     active#(x(N,0())) -> mark#(0())
     mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
     active#(x(N,s(M))) -> x#(N,M)
     mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
     active#(x(N,s(M))) -> plus#(x(N,M),N)
     mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
     active#(x(N,s(M))) -> mark#(plus(x(N,M),N))
     active#(x(N,s(M))) -> plus#(x(N,M),N) ->
     plus#(mark(X1),X2) -> plus#(X1,X2)
     active#(x(N,s(M))) -> plus#(x(N,M),N) ->
     plus#(active(X1),X2) -> plus#(X1,X2)
     active#(x(N,s(M))) -> mark#(plus(x(N,M),N)) ->
     mark#(and(X1,X2)) -> mark#(X1)
     active#(x(N,s(M))) -> mark#(plus(x(N,M),N)) ->
     mark#(and(X1,X2)) -> and#(mark(X1),X2)
     active#(x(N,s(M))) -> mark#(plus(x(N,M),N)) ->
     mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
     active#(x(N,s(M))) -> mark#(plus(x(N,M),N)) ->
     mark#(plus(X1,X2)) -> mark#(X2)
     active#(x(N,s(M))) -> mark#(plus(x(N,M),N)) ->
     mark#(plus(X1,X2)) -> mark#(X1)
     active#(x(N,s(M))) -> mark#(plus(x(N,M),N)) ->
     mark#(plus(X1,X2)) -> plus#(mark(X1),mark(X2))
     active#(x(N,s(M))) -> mark#(plus(x(N,M),N)) ->
     mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
     active#(x(N,s(M))) -> mark#(plus(x(N,M),N)) ->
     mark#(s(X)) -> mark#(X)
     active#(x(N,s(M))) -> mark#(plus(x(N,M),N)) ->
     mark#(s(X)) -> s#(mark(X))
     active#(x(N,s(M))) -> mark#(plus(x(N,M),N)) ->
     mark#(s(X)) -> active#(s(mark(X)))
     active#(x(N,s(M))) -> mark#(plus(x(N,M),N)) ->
     mark#(x(X1,X2)) -> mark#(X2)
     active#(x(N,s(M))) -> mark#(plus(x(N,M),N)) ->
     mark#(x(X1,X2)) -> mark#(X1)
     active#(x(N,s(M))) -> mark#(plus(x(N,M),N)) ->
     mark#(x(X1,X2)) -> x#(mark(X1),mark(X2))
     active#(x(N,s(M))) -> mark#(plus(x(N,M),N)) ->
     mark#(x(X1,X2)) -> active#(x(mark(X1),mark(X2)))
     active#(x(N,0())) -> mark#(0()) ->
     mark#(0()) -> active#(0())
     active#(plus(N,s(M))) -> s#(plus(N,M)) ->
     s#(mark(X)) -> s#(X)
     active#(plus(N,s(M))) -> s#(plus(N,M)) ->
     s#(active(X)) -> s#(X)
     active#(plus(N,s(M))) -> mark#(s(plus(N,M))) ->
     mark#(and(X1,X2)) -> mark#(X1)
     active#(plus(N,s(M))) -> mark#(s(plus(N,M))) ->
     mark#(and(X1,X2)) -> and#(mark(X1),X2)
     active#(plus(N,s(M))) -> mark#(s(plus(N,M))) ->
     mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
     active#(plus(N,s(M))) -> mark#(s(plus(N,M))) ->
     mark#(plus(X1,X2)) -> mark#(X2)
     active#(plus(N,s(M))) -> mark#(s(plus(N,M))) ->
     mark#(plus(X1,X2)) -> mark#(X1)
     active#(plus(N,s(M))) -> mark#(s(plus(N,M))) ->
     mark#(plus(X1,X2)) -> plus#(mark(X1),mark(X2))
     active#(plus(N,s(M))) -> mark#(s(plus(N,M))) ->
     mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
     active#(plus(N,s(M))) -> mark#(s(plus(N,M))) ->
     mark#(s(X)) -> mark#(X)
     active#(plus(N,s(M))) -> mark#(s(plus(N,M))) ->
     mark#(s(X)) -> s#(mark(X))
     active#(plus(N,s(M))) -> mark#(s(plus(N,M))) ->
     mark#(s(X)) -> active#(s(mark(X)))
     active#(plus(N,s(M))) -> mark#(s(plus(N,M))) ->
     mark#(x(X1,X2)) -> mark#(X2)
     active#(plus(N,s(M))) -> mark#(s(plus(N,M))) ->
     mark#(x(X1,X2)) -> mark#(X1)
     active#(plus(N,s(M))) -> mark#(s(plus(N,M))) ->
     mark#(x(X1,X2)) -> x#(mark(X1),mark(X2))
     active#(plus(N,s(M))) -> mark#(s(plus(N,M))) ->
     mark#(x(X1,X2)) -> active#(x(mark(X1),mark(X2)))
     active#(plus(N,0())) -> mark#(N) ->
     mark#(and(X1,X2)) -> mark#(X1)
     active#(plus(N,0())) -> mark#(N) ->
     mark#(and(X1,X2)) -> and#(mark(X1),X2)
     active#(plus(N,0())) -> mark#(N) ->
     mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
     active#(plus(N,0())) -> mark#(N) ->
     mark#(tt()) -> active#(tt())
     active#(plus(N,0())) -> mark#(N) ->
     mark#(plus(X1,X2)) -> mark#(X2)
     active#(plus(N,0())) -> mark#(N) ->
     mark#(plus(X1,X2)) -> mark#(X1)
     active#(plus(N,0())) -> mark#(N) ->
     mark#(plus(X1,X2)) -> plus#(mark(X1),mark(X2))
     active#(plus(N,0())) -> mark#(N) ->
     mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
     active#(plus(N,0())) -> mark#(N) -> mark#(0()) -> active#(0())
     active#(plus(N,0())) -> mark#(N) -> mark#(s(X)) -> mark#(X)
     active#(plus(N,0())) -> mark#(N) -> mark#(s(X)) -> s#(mark(X))
     active#(plus(N,0())) -> mark#(N) ->
     mark#(s(X)) -> active#(s(mark(X)))
     active#(plus(N,0())) -> mark#(N) ->
     mark#(x(X1,X2)) -> mark#(X2)
     active#(plus(N,0())) -> mark#(N) ->
     mark#(x(X1,X2)) -> mark#(X1)
     active#(plus(N,0())) -> mark#(N) ->
     mark#(x(X1,X2)) -> x#(mark(X1),mark(X2))
     active#(plus(N,0())) -> mark#(N) ->
     mark#(x(X1,X2)) -> active#(x(mark(X1),mark(X2)))
     active#(and(tt(),X)) -> mark#(X) ->
     mark#(and(X1,X2)) -> mark#(X1)
     active#(and(tt(),X)) -> mark#(X) ->
     mark#(and(X1,X2)) -> and#(mark(X1),X2)
     active#(and(tt(),X)) -> mark#(X) ->
     mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
     active#(and(tt(),X)) -> mark#(X) ->
     mark#(tt()) -> active#(tt())
     active#(and(tt(),X)) -> mark#(X) ->
     mark#(plus(X1,X2)) -> mark#(X2)
     active#(and(tt(),X)) -> mark#(X) ->
     mark#(plus(X1,X2)) -> mark#(X1)
     active#(and(tt(),X)) -> mark#(X) ->
     mark#(plus(X1,X2)) -> plus#(mark(X1),mark(X2))
     active#(and(tt(),X)) -> mark#(X) ->
     mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
     active#(and(tt(),X)) -> mark#(X) -> mark#(0()) -> active#(0())
     active#(and(tt(),X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
     active#(and(tt(),X)) -> mark#(X) -> mark#(s(X)) -> s#(mark(X))
     active#(and(tt(),X)) -> mark#(X) ->
     mark#(s(X)) -> active#(s(mark(X)))
     active#(and(tt(),X)) -> mark#(X) ->
     mark#(x(X1,X2)) -> mark#(X2)
     active#(and(tt(),X)) -> mark#(X) ->
     mark#(x(X1,X2)) -> mark#(X1)
     active#(and(tt(),X)) -> mark#(X) ->
     mark#(x(X1,X2)) -> x#(mark(X1),mark(X2))
     active#(and(tt(),X)) -> mark#(X) -> mark#(x(X1,X2)) -> active#(x(mark(X1),mark(X2)))
    SCC Processor:
     #sccs: 5
     #rules: 28
     #arcs: 261/1521
     DPs:
      mark#(x(X1,X2)) -> mark#(X2)
      mark#(x(X1,X2)) -> active#(x(mark(X1),mark(X2)))
      active#(x(N,s(M))) -> mark#(plus(x(N,M),N))
      mark#(x(X1,X2)) -> mark#(X1)
      mark#(s(X)) -> active#(s(mark(X)))
      active#(plus(N,s(M))) -> mark#(s(plus(N,M)))
      mark#(s(X)) -> mark#(X)
      mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
      active#(plus(N,0())) -> mark#(N)
      mark#(plus(X1,X2)) -> mark#(X1)
      mark#(plus(X1,X2)) -> mark#(X2)
      mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
      active#(and(tt(),X)) -> mark#(X)
      mark#(and(X1,X2)) -> mark#(X1)
     TRS:
      active(and(tt(),X)) -> mark(X)
      active(plus(N,0())) -> mark(N)
      active(plus(N,s(M))) -> mark(s(plus(N,M)))
      active(x(N,0())) -> mark(0())
      active(x(N,s(M))) -> mark(plus(x(N,M),N))
      mark(and(X1,X2)) -> active(and(mark(X1),X2))
      mark(tt()) -> active(tt())
      mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
      mark(0()) -> active(0())
      mark(s(X)) -> active(s(mark(X)))
      mark(x(X1,X2)) -> active(x(mark(X1),mark(X2)))
      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)
      plus(mark(X1),X2) -> plus(X1,X2)
      plus(X1,mark(X2)) -> plus(X1,X2)
      plus(active(X1),X2) -> plus(X1,X2)
      plus(X1,active(X2)) -> plus(X1,X2)
      s(mark(X)) -> s(X)
      s(active(X)) -> s(X)
      x(mark(X1),X2) -> x(X1,X2)
      x(X1,mark(X2)) -> x(X1,X2)
      x(active(X1),X2) -> x(X1,X2)
      x(X1,active(X2)) -> x(X1,X2)
     Open
     
     DPs:
      plus#(mark(X1),X2) -> plus#(X1,X2)
      plus#(X1,active(X2)) -> plus#(X1,X2)
      plus#(active(X1),X2) -> plus#(X1,X2)
      plus#(X1,mark(X2)) -> plus#(X1,X2)
     TRS:
      active(and(tt(),X)) -> mark(X)
      active(plus(N,0())) -> mark(N)
      active(plus(N,s(M))) -> mark(s(plus(N,M)))
      active(x(N,0())) -> mark(0())
      active(x(N,s(M))) -> mark(plus(x(N,M),N))
      mark(and(X1,X2)) -> active(and(mark(X1),X2))
      mark(tt()) -> active(tt())
      mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
      mark(0()) -> active(0())
      mark(s(X)) -> active(s(mark(X)))
      mark(x(X1,X2)) -> active(x(mark(X1),mark(X2)))
      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)
      plus(mark(X1),X2) -> plus(X1,X2)
      plus(X1,mark(X2)) -> plus(X1,X2)
      plus(active(X1),X2) -> plus(X1,X2)
      plus(X1,active(X2)) -> plus(X1,X2)
      s(mark(X)) -> s(X)
      s(active(X)) -> s(X)
      x(mark(X1),X2) -> x(X1,X2)
      x(X1,mark(X2)) -> x(X1,X2)
      x(active(X1),X2) -> x(X1,X2)
      x(X1,active(X2)) -> x(X1,X2)
     Open
     
     DPs:
      s#(mark(X)) -> s#(X)
      s#(active(X)) -> s#(X)
     TRS:
      active(and(tt(),X)) -> mark(X)
      active(plus(N,0())) -> mark(N)
      active(plus(N,s(M))) -> mark(s(plus(N,M)))
      active(x(N,0())) -> mark(0())
      active(x(N,s(M))) -> mark(plus(x(N,M),N))
      mark(and(X1,X2)) -> active(and(mark(X1),X2))
      mark(tt()) -> active(tt())
      mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
      mark(0()) -> active(0())
      mark(s(X)) -> active(s(mark(X)))
      mark(x(X1,X2)) -> active(x(mark(X1),mark(X2)))
      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)
      plus(mark(X1),X2) -> plus(X1,X2)
      plus(X1,mark(X2)) -> plus(X1,X2)
      plus(active(X1),X2) -> plus(X1,X2)
      plus(X1,active(X2)) -> plus(X1,X2)
      s(mark(X)) -> s(X)
      s(active(X)) -> s(X)
      x(mark(X1),X2) -> x(X1,X2)
      x(X1,mark(X2)) -> x(X1,X2)
      x(active(X1),X2) -> x(X1,X2)
      x(X1,active(X2)) -> x(X1,X2)
     Open
     
     DPs:
      x#(mark(X1),X2) -> x#(X1,X2)
      x#(X1,active(X2)) -> x#(X1,X2)
      x#(active(X1),X2) -> x#(X1,X2)
      x#(X1,mark(X2)) -> x#(X1,X2)
     TRS:
      active(and(tt(),X)) -> mark(X)
      active(plus(N,0())) -> mark(N)
      active(plus(N,s(M))) -> mark(s(plus(N,M)))
      active(x(N,0())) -> mark(0())
      active(x(N,s(M))) -> mark(plus(x(N,M),N))
      mark(and(X1,X2)) -> active(and(mark(X1),X2))
      mark(tt()) -> active(tt())
      mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
      mark(0()) -> active(0())
      mark(s(X)) -> active(s(mark(X)))
      mark(x(X1,X2)) -> active(x(mark(X1),mark(X2)))
      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)
      plus(mark(X1),X2) -> plus(X1,X2)
      plus(X1,mark(X2)) -> plus(X1,X2)
      plus(active(X1),X2) -> plus(X1,X2)
      plus(X1,active(X2)) -> plus(X1,X2)
      s(mark(X)) -> s(X)
      s(active(X)) -> s(X)
      x(mark(X1),X2) -> x(X1,X2)
      x(X1,mark(X2)) -> x(X1,X2)
      x(active(X1),X2) -> x(X1,X2)
      x(X1,active(X2)) -> x(X1,X2)
     Open
     
     DPs:
      and#(mark(X1),X2) -> and#(X1,X2)
      and#(X1,active(X2)) -> and#(X1,X2)
      and#(active(X1),X2) -> and#(X1,X2)
      and#(X1,mark(X2)) -> and#(X1,X2)
     TRS:
      active(and(tt(),X)) -> mark(X)
      active(plus(N,0())) -> mark(N)
      active(plus(N,s(M))) -> mark(s(plus(N,M)))
      active(x(N,0())) -> mark(0())
      active(x(N,s(M))) -> mark(plus(x(N,M),N))
      mark(and(X1,X2)) -> active(and(mark(X1),X2))
      mark(tt()) -> active(tt())
      mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
      mark(0()) -> active(0())
      mark(s(X)) -> active(s(mark(X)))
      mark(x(X1,X2)) -> active(x(mark(X1),mark(X2)))
      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)
      plus(mark(X1),X2) -> plus(X1,X2)
      plus(X1,mark(X2)) -> plus(X1,X2)
      plus(active(X1),X2) -> plus(X1,X2)
      plus(X1,active(X2)) -> plus(X1,X2)
      s(mark(X)) -> s(X)
      s(active(X)) -> s(X)
      x(mark(X1),X2) -> x(X1,X2)
      x(X1,mark(X2)) -> x(X1,X2)
      x(active(X1),X2) -> x(X1,X2)
      x(X1,active(X2)) -> x(X1,X2)
     Open