MAYBE

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

Proof:
 DP Processor:
  DPs:
   active#(U11(tt(),M,N)) -> U12#(tt(),M,N)
   active#(U11(tt(),M,N)) -> mark#(U12(tt(),M,N))
   active#(U12(tt(),M,N)) -> plus#(N,M)
   active#(U12(tt(),M,N)) -> s#(plus(N,M))
   active#(U12(tt(),M,N)) -> mark#(s(plus(N,M)))
   active#(plus(N,0())) -> mark#(N)
   active#(plus(N,s(M))) -> U11#(tt(),M,N)
   active#(plus(N,s(M))) -> mark#(U11(tt(),M,N))
   mark#(U11(X1,X2,X3)) -> mark#(X1)
   mark#(U11(X1,X2,X3)) -> U11#(mark(X1),X2,X3)
   mark#(U11(X1,X2,X3)) -> active#(U11(mark(X1),X2,X3))
   mark#(tt()) -> active#(tt())
   mark#(U12(X1,X2,X3)) -> mark#(X1)
   mark#(U12(X1,X2,X3)) -> U12#(mark(X1),X2,X3)
   mark#(U12(X1,X2,X3)) -> active#(U12(mark(X1),X2,X3))
   mark#(s(X)) -> mark#(X)
   mark#(s(X)) -> s#(mark(X))
   mark#(s(X)) -> active#(s(mark(X)))
   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())
   U11#(mark(X1),X2,X3) -> U11#(X1,X2,X3)
   U11#(X1,mark(X2),X3) -> U11#(X1,X2,X3)
   U11#(X1,X2,mark(X3)) -> U11#(X1,X2,X3)
   U11#(active(X1),X2,X3) -> U11#(X1,X2,X3)
   U11#(X1,active(X2),X3) -> U11#(X1,X2,X3)
   U11#(X1,X2,active(X3)) -> U11#(X1,X2,X3)
   U12#(mark(X1),X2,X3) -> U12#(X1,X2,X3)
   U12#(X1,mark(X2),X3) -> U12#(X1,X2,X3)
   U12#(X1,X2,mark(X3)) -> U12#(X1,X2,X3)
   U12#(active(X1),X2,X3) -> U12#(X1,X2,X3)
   U12#(X1,active(X2),X3) -> U12#(X1,X2,X3)
   U12#(X1,X2,active(X3)) -> U12#(X1,X2,X3)
   s#(mark(X)) -> s#(X)
   s#(active(X)) -> s#(X)
   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)
  TRS:
   active(U11(tt(),M,N)) -> mark(U12(tt(),M,N))
   active(U12(tt(),M,N)) -> mark(s(plus(N,M)))
   active(plus(N,0())) -> mark(N)
   active(plus(N,s(M))) -> mark(U11(tt(),M,N))
   mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
   mark(tt()) -> active(tt())
   mark(U12(X1,X2,X3)) -> active(U12(mark(X1),X2,X3))
   mark(s(X)) -> active(s(mark(X)))
   mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
   mark(0()) -> active(0())
   U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
   U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
   U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
   U11(active(X1),X2,X3) -> U11(X1,X2,X3)
   U11(X1,active(X2),X3) -> U11(X1,X2,X3)
   U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
   U12(mark(X1),X2,X3) -> U12(X1,X2,X3)
   U12(X1,mark(X2),X3) -> U12(X1,X2,X3)
   U12(X1,X2,mark(X3)) -> U12(X1,X2,X3)
   U12(active(X1),X2,X3) -> U12(X1,X2,X3)
   U12(X1,active(X2),X3) -> U12(X1,X2,X3)
   U12(X1,X2,active(X3)) -> U12(X1,X2,X3)
   s(mark(X)) -> s(X)
   s(active(X)) -> s(X)
   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)
  EDG Processor:
   DPs:
    active#(U11(tt(),M,N)) -> U12#(tt(),M,N)
    active#(U11(tt(),M,N)) -> mark#(U12(tt(),M,N))
    active#(U12(tt(),M,N)) -> plus#(N,M)
    active#(U12(tt(),M,N)) -> s#(plus(N,M))
    active#(U12(tt(),M,N)) -> mark#(s(plus(N,M)))
    active#(plus(N,0())) -> mark#(N)
    active#(plus(N,s(M))) -> U11#(tt(),M,N)
    active#(plus(N,s(M))) -> mark#(U11(tt(),M,N))
    mark#(U11(X1,X2,X3)) -> mark#(X1)
    mark#(U11(X1,X2,X3)) -> U11#(mark(X1),X2,X3)
    mark#(U11(X1,X2,X3)) -> active#(U11(mark(X1),X2,X3))
    mark#(tt()) -> active#(tt())
    mark#(U12(X1,X2,X3)) -> mark#(X1)
    mark#(U12(X1,X2,X3)) -> U12#(mark(X1),X2,X3)
    mark#(U12(X1,X2,X3)) -> active#(U12(mark(X1),X2,X3))
    mark#(s(X)) -> mark#(X)
    mark#(s(X)) -> s#(mark(X))
    mark#(s(X)) -> active#(s(mark(X)))
    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())
    U11#(mark(X1),X2,X3) -> U11#(X1,X2,X3)
    U11#(X1,mark(X2),X3) -> U11#(X1,X2,X3)
    U11#(X1,X2,mark(X3)) -> U11#(X1,X2,X3)
    U11#(active(X1),X2,X3) -> U11#(X1,X2,X3)
    U11#(X1,active(X2),X3) -> U11#(X1,X2,X3)
    U11#(X1,X2,active(X3)) -> U11#(X1,X2,X3)
    U12#(mark(X1),X2,X3) -> U12#(X1,X2,X3)
    U12#(X1,mark(X2),X3) -> U12#(X1,X2,X3)
    U12#(X1,X2,mark(X3)) -> U12#(X1,X2,X3)
    U12#(active(X1),X2,X3) -> U12#(X1,X2,X3)
    U12#(X1,active(X2),X3) -> U12#(X1,X2,X3)
    U12#(X1,X2,active(X3)) -> U12#(X1,X2,X3)
    s#(mark(X)) -> s#(X)
    s#(active(X)) -> s#(X)
    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)
   TRS:
    active(U11(tt(),M,N)) -> mark(U12(tt(),M,N))
    active(U12(tt(),M,N)) -> mark(s(plus(N,M)))
    active(plus(N,0())) -> mark(N)
    active(plus(N,s(M))) -> mark(U11(tt(),M,N))
    mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
    mark(tt()) -> active(tt())
    mark(U12(X1,X2,X3)) -> active(U12(mark(X1),X2,X3))
    mark(s(X)) -> active(s(mark(X)))
    mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
    mark(0()) -> active(0())
    U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
    U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
    U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
    U11(active(X1),X2,X3) -> U11(X1,X2,X3)
    U11(X1,active(X2),X3) -> U11(X1,X2,X3)
    U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
    U12(mark(X1),X2,X3) -> U12(X1,X2,X3)
    U12(X1,mark(X2),X3) -> U12(X1,X2,X3)
    U12(X1,X2,mark(X3)) -> U12(X1,X2,X3)
    U12(active(X1),X2,X3) -> U12(X1,X2,X3)
    U12(X1,active(X2),X3) -> U12(X1,X2,X3)
    U12(X1,X2,active(X3)) -> U12(X1,X2,X3)
    s(mark(X)) -> s(X)
    s(active(X)) -> s(X)
    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)
   graph:
    U11#(mark(X1),X2,X3) -> U11#(X1,X2,X3) ->
    U11#(mark(X1),X2,X3) -> U11#(X1,X2,X3)
    U11#(mark(X1),X2,X3) -> U11#(X1,X2,X3) ->
    U11#(X1,mark(X2),X3) -> U11#(X1,X2,X3)
    U11#(mark(X1),X2,X3) -> U11#(X1,X2,X3) ->
    U11#(X1,X2,mark(X3)) -> U11#(X1,X2,X3)
    U11#(mark(X1),X2,X3) -> U11#(X1,X2,X3) ->
    U11#(active(X1),X2,X3) -> U11#(X1,X2,X3)
    U11#(mark(X1),X2,X3) -> U11#(X1,X2,X3) ->
    U11#(X1,active(X2),X3) -> U11#(X1,X2,X3)
    U11#(mark(X1),X2,X3) -> U11#(X1,X2,X3) ->
    U11#(X1,X2,active(X3)) -> U11#(X1,X2,X3)
    U11#(active(X1),X2,X3) -> U11#(X1,X2,X3) ->
    U11#(mark(X1),X2,X3) -> U11#(X1,X2,X3)
    U11#(active(X1),X2,X3) -> U11#(X1,X2,X3) ->
    U11#(X1,mark(X2),X3) -> U11#(X1,X2,X3)
    U11#(active(X1),X2,X3) -> U11#(X1,X2,X3) ->
    U11#(X1,X2,mark(X3)) -> U11#(X1,X2,X3)
    U11#(active(X1),X2,X3) -> U11#(X1,X2,X3) ->
    U11#(active(X1),X2,X3) -> U11#(X1,X2,X3)
    U11#(active(X1),X2,X3) -> U11#(X1,X2,X3) ->
    U11#(X1,active(X2),X3) -> U11#(X1,X2,X3)
    U11#(active(X1),X2,X3) -> U11#(X1,X2,X3) ->
    U11#(X1,X2,active(X3)) -> U11#(X1,X2,X3)
    U11#(X1,mark(X2),X3) -> U11#(X1,X2,X3) ->
    U11#(mark(X1),X2,X3) -> U11#(X1,X2,X3)
    U11#(X1,mark(X2),X3) -> U11#(X1,X2,X3) ->
    U11#(X1,mark(X2),X3) -> U11#(X1,X2,X3)
    U11#(X1,mark(X2),X3) -> U11#(X1,X2,X3) ->
    U11#(X1,X2,mark(X3)) -> U11#(X1,X2,X3)
    U11#(X1,mark(X2),X3) -> U11#(X1,X2,X3) ->
    U11#(active(X1),X2,X3) -> U11#(X1,X2,X3)
    U11#(X1,mark(X2),X3) -> U11#(X1,X2,X3) ->
    U11#(X1,active(X2),X3) -> U11#(X1,X2,X3)
    U11#(X1,mark(X2),X3) -> U11#(X1,X2,X3) ->
    U11#(X1,X2,active(X3)) -> U11#(X1,X2,X3)
    U11#(X1,active(X2),X3) -> U11#(X1,X2,X3) ->
    U11#(mark(X1),X2,X3) -> U11#(X1,X2,X3)
    U11#(X1,active(X2),X3) -> U11#(X1,X2,X3) ->
    U11#(X1,mark(X2),X3) -> U11#(X1,X2,X3)
    U11#(X1,active(X2),X3) -> U11#(X1,X2,X3) ->
    U11#(X1,X2,mark(X3)) -> U11#(X1,X2,X3)
    U11#(X1,active(X2),X3) -> U11#(X1,X2,X3) ->
    U11#(active(X1),X2,X3) -> U11#(X1,X2,X3)
    U11#(X1,active(X2),X3) -> U11#(X1,X2,X3) ->
    U11#(X1,active(X2),X3) -> U11#(X1,X2,X3)
    U11#(X1,active(X2),X3) -> U11#(X1,X2,X3) ->
    U11#(X1,X2,active(X3)) -> U11#(X1,X2,X3)
    U11#(X1,X2,mark(X3)) -> U11#(X1,X2,X3) ->
    U11#(mark(X1),X2,X3) -> U11#(X1,X2,X3)
    U11#(X1,X2,mark(X3)) -> U11#(X1,X2,X3) ->
    U11#(X1,mark(X2),X3) -> U11#(X1,X2,X3)
    U11#(X1,X2,mark(X3)) -> U11#(X1,X2,X3) ->
    U11#(X1,X2,mark(X3)) -> U11#(X1,X2,X3)
    U11#(X1,X2,mark(X3)) -> U11#(X1,X2,X3) ->
    U11#(active(X1),X2,X3) -> U11#(X1,X2,X3)
    U11#(X1,X2,mark(X3)) -> U11#(X1,X2,X3) ->
    U11#(X1,active(X2),X3) -> U11#(X1,X2,X3)
    U11#(X1,X2,mark(X3)) -> U11#(X1,X2,X3) ->
    U11#(X1,X2,active(X3)) -> U11#(X1,X2,X3)
    U11#(X1,X2,active(X3)) -> U11#(X1,X2,X3) ->
    U11#(mark(X1),X2,X3) -> U11#(X1,X2,X3)
    U11#(X1,X2,active(X3)) -> U11#(X1,X2,X3) ->
    U11#(X1,mark(X2),X3) -> U11#(X1,X2,X3)
    U11#(X1,X2,active(X3)) -> U11#(X1,X2,X3) ->
    U11#(X1,X2,mark(X3)) -> U11#(X1,X2,X3)
    U11#(X1,X2,active(X3)) -> U11#(X1,X2,X3) ->
    U11#(active(X1),X2,X3) -> U11#(X1,X2,X3)
    U11#(X1,X2,active(X3)) -> U11#(X1,X2,X3) ->
    U11#(X1,active(X2),X3) -> U11#(X1,X2,X3)
    U11#(X1,X2,active(X3)) -> U11#(X1,X2,X3) ->
    U11#(X1,X2,active(X3)) -> U11#(X1,X2,X3)
    s#(mark(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
    s#(mark(X)) -> s#(X) -> s#(active(X)) -> s#(X)
    s#(active(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
    s#(active(X)) -> s#(X) -> s#(active(X)) -> s#(X)
    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#(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#(U11(X1,X2,X3)) -> mark#(X1)
    mark#(s(X)) -> mark#(X) -> mark#(U11(X1,X2,X3)) -> U11#(mark(X1),X2,X3)
    mark#(s(X)) -> mark#(X) ->
    mark#(U11(X1,X2,X3)) -> active#(U11(mark(X1),X2,X3))
    mark#(s(X)) -> mark#(X) -> mark#(tt()) -> active#(tt())
    mark#(s(X)) -> mark#(X) -> mark#(U12(X1,X2,X3)) -> mark#(X1)
    mark#(s(X)) -> mark#(X) -> mark#(U12(X1,X2,X3)) -> U12#(mark(X1),X2,X3)
    mark#(s(X)) -> mark#(X) ->
    mark#(U12(X1,X2,X3)) -> active#(U12(mark(X1),X2,X3))
    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#(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)) -> active#(s(mark(X))) ->
    active#(U11(tt(),M,N)) -> U12#(tt(),M,N)
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(U11(tt(),M,N)) -> mark#(U12(tt(),M,N))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(U12(tt(),M,N)) -> plus#(N,M)
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(U12(tt(),M,N)) -> s#(plus(N,M))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(U12(tt(),M,N)) -> mark#(s(plus(N,M)))
    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))) -> U11#(tt(),M,N)
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(plus(N,s(M))) -> mark#(U11(tt(),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#(U11(X1,X2,X3)) -> mark#(X1)
    mark#(plus(X1,X2)) -> mark#(X2) ->
    mark#(U11(X1,X2,X3)) -> U11#(mark(X1),X2,X3)
    mark#(plus(X1,X2)) -> mark#(X2) ->
    mark#(U11(X1,X2,X3)) -> active#(U11(mark(X1),X2,X3))
    mark#(plus(X1,X2)) -> mark#(X2) -> mark#(tt()) -> active#(tt())
    mark#(plus(X1,X2)) -> mark#(X2) ->
    mark#(U12(X1,X2,X3)) -> mark#(X1)
    mark#(plus(X1,X2)) -> mark#(X2) ->
    mark#(U12(X1,X2,X3)) -> U12#(mark(X1),X2,X3)
    mark#(plus(X1,X2)) -> mark#(X2) ->
    mark#(U12(X1,X2,X3)) -> active#(U12(mark(X1),X2,X3))
    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#(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#(X1) ->
    mark#(U11(X1,X2,X3)) -> mark#(X1)
    mark#(plus(X1,X2)) -> mark#(X1) ->
    mark#(U11(X1,X2,X3)) -> U11#(mark(X1),X2,X3)
    mark#(plus(X1,X2)) -> mark#(X1) ->
    mark#(U11(X1,X2,X3)) -> active#(U11(mark(X1),X2,X3))
    mark#(plus(X1,X2)) -> mark#(X1) -> mark#(tt()) -> active#(tt())
    mark#(plus(X1,X2)) -> mark#(X1) ->
    mark#(U12(X1,X2,X3)) -> mark#(X1)
    mark#(plus(X1,X2)) -> mark#(X1) ->
    mark#(U12(X1,X2,X3)) -> U12#(mark(X1),X2,X3)
    mark#(plus(X1,X2)) -> mark#(X1) ->
    mark#(U12(X1,X2,X3)) -> active#(U12(mark(X1),X2,X3))
    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#(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)) -> active#(plus(mark(X1),mark(X2))) ->
    active#(U11(tt(),M,N)) -> U12#(tt(),M,N)
    mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) ->
    active#(U11(tt(),M,N)) -> mark#(U12(tt(),M,N))
    mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) ->
    active#(U12(tt(),M,N)) -> plus#(N,M)
    mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) ->
    active#(U12(tt(),M,N)) -> s#(plus(N,M))
    mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) ->
    active#(U12(tt(),M,N)) -> mark#(s(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#(plus(N,s(M))) -> U11#(tt(),M,N)
    mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2))) ->
    active#(plus(N,s(M))) -> mark#(U11(tt(),M,N))
    mark#(U12(X1,X2,X3)) -> mark#(X1) ->
    mark#(U11(X1,X2,X3)) -> mark#(X1)
    mark#(U12(X1,X2,X3)) -> mark#(X1) ->
    mark#(U11(X1,X2,X3)) -> U11#(mark(X1),X2,X3)
    mark#(U12(X1,X2,X3)) -> mark#(X1) ->
    mark#(U11(X1,X2,X3)) -> active#(U11(mark(X1),X2,X3))
    mark#(U12(X1,X2,X3)) -> mark#(X1) ->
    mark#(tt()) -> active#(tt())
    mark#(U12(X1,X2,X3)) -> mark#(X1) ->
    mark#(U12(X1,X2,X3)) -> mark#(X1)
    mark#(U12(X1,X2,X3)) -> mark#(X1) ->
    mark#(U12(X1,X2,X3)) -> U12#(mark(X1),X2,X3)
    mark#(U12(X1,X2,X3)) -> mark#(X1) ->
    mark#(U12(X1,X2,X3)) -> active#(U12(mark(X1),X2,X3))
    mark#(U12(X1,X2,X3)) -> mark#(X1) -> mark#(s(X)) -> mark#(X)
    mark#(U12(X1,X2,X3)) -> mark#(X1) ->
    mark#(s(X)) -> s#(mark(X))
    mark#(U12(X1,X2,X3)) -> mark#(X1) ->
    mark#(s(X)) -> active#(s(mark(X)))
    mark#(U12(X1,X2,X3)) -> mark#(X1) ->
    mark#(plus(X1,X2)) -> mark#(X2)
    mark#(U12(X1,X2,X3)) -> mark#(X1) ->
    mark#(plus(X1,X2)) -> mark#(X1)
    mark#(U12(X1,X2,X3)) -> mark#(X1) ->
    mark#(plus(X1,X2)) -> plus#(mark(X1),mark(X2))
    mark#(U12(X1,X2,X3)) -> mark#(X1) ->
    mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
    mark#(U12(X1,X2,X3)) -> mark#(X1) ->
    mark#(0()) -> active#(0())
    mark#(U12(X1,X2,X3)) -> U12#(mark(X1),X2,X3) ->
    U12#(mark(X1),X2,X3) -> U12#(X1,X2,X3)
    mark#(U12(X1,X2,X3)) -> U12#(mark(X1),X2,X3) ->
    U12#(X1,mark(X2),X3) -> U12#(X1,X2,X3)
    mark#(U12(X1,X2,X3)) -> U12#(mark(X1),X2,X3) ->
    U12#(X1,X2,mark(X3)) -> U12#(X1,X2,X3)
    mark#(U12(X1,X2,X3)) -> U12#(mark(X1),X2,X3) ->
    U12#(active(X1),X2,X3) -> U12#(X1,X2,X3)
    mark#(U12(X1,X2,X3)) -> U12#(mark(X1),X2,X3) ->
    U12#(X1,active(X2),X3) -> U12#(X1,X2,X3)
    mark#(U12(X1,X2,X3)) -> U12#(mark(X1),X2,X3) ->
    U12#(X1,X2,active(X3)) -> U12#(X1,X2,X3)
    mark#(U12(X1,X2,X3)) -> active#(U12(mark(X1),X2,X3)) ->
    active#(U11(tt(),M,N)) -> U12#(tt(),M,N)
    mark#(U12(X1,X2,X3)) -> active#(U12(mark(X1),X2,X3)) ->
    active#(U11(tt(),M,N)) -> mark#(U12(tt(),M,N))
    mark#(U12(X1,X2,X3)) -> active#(U12(mark(X1),X2,X3)) ->
    active#(U12(tt(),M,N)) -> plus#(N,M)
    mark#(U12(X1,X2,X3)) -> active#(U12(mark(X1),X2,X3)) ->
    active#(U12(tt(),M,N)) -> s#(plus(N,M))
    mark#(U12(X1,X2,X3)) -> active#(U12(mark(X1),X2,X3)) ->
    active#(U12(tt(),M,N)) -> mark#(s(plus(N,M)))
    mark#(U12(X1,X2,X3)) -> active#(U12(mark(X1),X2,X3)) ->
    active#(plus(N,0())) -> mark#(N)
    mark#(U12(X1,X2,X3)) -> active#(U12(mark(X1),X2,X3)) ->
    active#(plus(N,s(M))) -> U11#(tt(),M,N)
    mark#(U12(X1,X2,X3)) -> active#(U12(mark(X1),X2,X3)) ->
    active#(plus(N,s(M))) -> mark#(U11(tt(),M,N))
    mark#(U11(X1,X2,X3)) -> U11#(mark(X1),X2,X3) ->
    U11#(mark(X1),X2,X3) -> U11#(X1,X2,X3)
    mark#(U11(X1,X2,X3)) -> U11#(mark(X1),X2,X3) ->
    U11#(X1,mark(X2),X3) -> U11#(X1,X2,X3)
    mark#(U11(X1,X2,X3)) -> U11#(mark(X1),X2,X3) ->
    U11#(X1,X2,mark(X3)) -> U11#(X1,X2,X3)
    mark#(U11(X1,X2,X3)) -> U11#(mark(X1),X2,X3) ->
    U11#(active(X1),X2,X3) -> U11#(X1,X2,X3)
    mark#(U11(X1,X2,X3)) -> U11#(mark(X1),X2,X3) ->
    U11#(X1,active(X2),X3) -> U11#(X1,X2,X3)
    mark#(U11(X1,X2,X3)) -> U11#(mark(X1),X2,X3) ->
    U11#(X1,X2,active(X3)) -> U11#(X1,X2,X3)
    mark#(U11(X1,X2,X3)) -> mark#(X1) ->
    mark#(U11(X1,X2,X3)) -> mark#(X1)
    mark#(U11(X1,X2,X3)) -> mark#(X1) ->
    mark#(U11(X1,X2,X3)) -> U11#(mark(X1),X2,X3)
    mark#(U11(X1,X2,X3)) -> mark#(X1) ->
    mark#(U11(X1,X2,X3)) -> active#(U11(mark(X1),X2,X3))
    mark#(U11(X1,X2,X3)) -> mark#(X1) ->
    mark#(tt()) -> active#(tt())
    mark#(U11(X1,X2,X3)) -> mark#(X1) ->
    mark#(U12(X1,X2,X3)) -> mark#(X1)
    mark#(U11(X1,X2,X3)) -> mark#(X1) ->
    mark#(U12(X1,X2,X3)) -> U12#(mark(X1),X2,X3)
    mark#(U11(X1,X2,X3)) -> mark#(X1) ->
    mark#(U12(X1,X2,X3)) -> active#(U12(mark(X1),X2,X3))
    mark#(U11(X1,X2,X3)) -> mark#(X1) -> mark#(s(X)) -> mark#(X)
    mark#(U11(X1,X2,X3)) -> mark#(X1) ->
    mark#(s(X)) -> s#(mark(X))
    mark#(U11(X1,X2,X3)) -> mark#(X1) ->
    mark#(s(X)) -> active#(s(mark(X)))
    mark#(U11(X1,X2,X3)) -> mark#(X1) ->
    mark#(plus(X1,X2)) -> mark#(X2)
    mark#(U11(X1,X2,X3)) -> mark#(X1) ->
    mark#(plus(X1,X2)) -> mark#(X1)
    mark#(U11(X1,X2,X3)) -> mark#(X1) ->
    mark#(plus(X1,X2)) -> plus#(mark(X1),mark(X2))
    mark#(U11(X1,X2,X3)) -> mark#(X1) ->
    mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
    mark#(U11(X1,X2,X3)) -> mark#(X1) ->
    mark#(0()) -> active#(0())
    mark#(U11(X1,X2,X3)) -> active#(U11(mark(X1),X2,X3)) ->
    active#(U11(tt(),M,N)) -> U12#(tt(),M,N)
    mark#(U11(X1,X2,X3)) -> active#(U11(mark(X1),X2,X3)) ->
    active#(U11(tt(),M,N)) -> mark#(U12(tt(),M,N))
    mark#(U11(X1,X2,X3)) -> active#(U11(mark(X1),X2,X3)) ->
    active#(U12(tt(),M,N)) -> plus#(N,M)
    mark#(U11(X1,X2,X3)) -> active#(U11(mark(X1),X2,X3)) ->
    active#(U12(tt(),M,N)) -> s#(plus(N,M))
    mark#(U11(X1,X2,X3)) -> active#(U11(mark(X1),X2,X3)) ->
    active#(U12(tt(),M,N)) -> mark#(s(plus(N,M)))
    mark#(U11(X1,X2,X3)) -> active#(U11(mark(X1),X2,X3)) ->
    active#(plus(N,0())) -> mark#(N)
    mark#(U11(X1,X2,X3)) -> active#(U11(mark(X1),X2,X3)) ->
    active#(plus(N,s(M))) -> U11#(tt(),M,N)
    mark#(U11(X1,X2,X3)) -> active#(U11(mark(X1),X2,X3)) ->
    active#(plus(N,s(M))) -> mark#(U11(tt(),M,N))
    U12#(mark(X1),X2,X3) -> U12#(X1,X2,X3) ->
    U12#(mark(X1),X2,X3) -> U12#(X1,X2,X3)
    U12#(mark(X1),X2,X3) -> U12#(X1,X2,X3) ->
    U12#(X1,mark(X2),X3) -> U12#(X1,X2,X3)
    U12#(mark(X1),X2,X3) -> U12#(X1,X2,X3) ->
    U12#(X1,X2,mark(X3)) -> U12#(X1,X2,X3)
    U12#(mark(X1),X2,X3) -> U12#(X1,X2,X3) ->
    U12#(active(X1),X2,X3) -> U12#(X1,X2,X3)
    U12#(mark(X1),X2,X3) -> U12#(X1,X2,X3) ->
    U12#(X1,active(X2),X3) -> U12#(X1,X2,X3)
    U12#(mark(X1),X2,X3) -> U12#(X1,X2,X3) ->
    U12#(X1,X2,active(X3)) -> U12#(X1,X2,X3)
    U12#(active(X1),X2,X3) -> U12#(X1,X2,X3) ->
    U12#(mark(X1),X2,X3) -> U12#(X1,X2,X3)
    U12#(active(X1),X2,X3) -> U12#(X1,X2,X3) ->
    U12#(X1,mark(X2),X3) -> U12#(X1,X2,X3)
    U12#(active(X1),X2,X3) -> U12#(X1,X2,X3) ->
    U12#(X1,X2,mark(X3)) -> U12#(X1,X2,X3)
    U12#(active(X1),X2,X3) -> U12#(X1,X2,X3) ->
    U12#(active(X1),X2,X3) -> U12#(X1,X2,X3)
    U12#(active(X1),X2,X3) -> U12#(X1,X2,X3) ->
    U12#(X1,active(X2),X3) -> U12#(X1,X2,X3)
    U12#(active(X1),X2,X3) -> U12#(X1,X2,X3) ->
    U12#(X1,X2,active(X3)) -> U12#(X1,X2,X3)
    U12#(X1,mark(X2),X3) -> U12#(X1,X2,X3) ->
    U12#(mark(X1),X2,X3) -> U12#(X1,X2,X3)
    U12#(X1,mark(X2),X3) -> U12#(X1,X2,X3) ->
    U12#(X1,mark(X2),X3) -> U12#(X1,X2,X3)
    U12#(X1,mark(X2),X3) -> U12#(X1,X2,X3) ->
    U12#(X1,X2,mark(X3)) -> U12#(X1,X2,X3)
    U12#(X1,mark(X2),X3) -> U12#(X1,X2,X3) ->
    U12#(active(X1),X2,X3) -> U12#(X1,X2,X3)
    U12#(X1,mark(X2),X3) -> U12#(X1,X2,X3) ->
    U12#(X1,active(X2),X3) -> U12#(X1,X2,X3)
    U12#(X1,mark(X2),X3) -> U12#(X1,X2,X3) ->
    U12#(X1,X2,active(X3)) -> U12#(X1,X2,X3)
    U12#(X1,active(X2),X3) -> U12#(X1,X2,X3) ->
    U12#(mark(X1),X2,X3) -> U12#(X1,X2,X3)
    U12#(X1,active(X2),X3) -> U12#(X1,X2,X3) ->
    U12#(X1,mark(X2),X3) -> U12#(X1,X2,X3)
    U12#(X1,active(X2),X3) -> U12#(X1,X2,X3) ->
    U12#(X1,X2,mark(X3)) -> U12#(X1,X2,X3)
    U12#(X1,active(X2),X3) -> U12#(X1,X2,X3) ->
    U12#(active(X1),X2,X3) -> U12#(X1,X2,X3)
    U12#(X1,active(X2),X3) -> U12#(X1,X2,X3) ->
    U12#(X1,active(X2),X3) -> U12#(X1,X2,X3)
    U12#(X1,active(X2),X3) -> U12#(X1,X2,X3) ->
    U12#(X1,X2,active(X3)) -> U12#(X1,X2,X3)
    U12#(X1,X2,mark(X3)) -> U12#(X1,X2,X3) ->
    U12#(mark(X1),X2,X3) -> U12#(X1,X2,X3)
    U12#(X1,X2,mark(X3)) -> U12#(X1,X2,X3) ->
    U12#(X1,mark(X2),X3) -> U12#(X1,X2,X3)
    U12#(X1,X2,mark(X3)) -> U12#(X1,X2,X3) ->
    U12#(X1,X2,mark(X3)) -> U12#(X1,X2,X3)
    U12#(X1,X2,mark(X3)) -> U12#(X1,X2,X3) ->
    U12#(active(X1),X2,X3) -> U12#(X1,X2,X3)
    U12#(X1,X2,mark(X3)) -> U12#(X1,X2,X3) ->
    U12#(X1,active(X2),X3) -> U12#(X1,X2,X3)
    U12#(X1,X2,mark(X3)) -> U12#(X1,X2,X3) ->
    U12#(X1,X2,active(X3)) -> U12#(X1,X2,X3)
    U12#(X1,X2,active(X3)) -> U12#(X1,X2,X3) ->
    U12#(mark(X1),X2,X3) -> U12#(X1,X2,X3)
    U12#(X1,X2,active(X3)) -> U12#(X1,X2,X3) ->
    U12#(X1,mark(X2),X3) -> U12#(X1,X2,X3)
    U12#(X1,X2,active(X3)) -> U12#(X1,X2,X3) ->
    U12#(X1,X2,mark(X3)) -> U12#(X1,X2,X3)
    U12#(X1,X2,active(X3)) -> U12#(X1,X2,X3) ->
    U12#(active(X1),X2,X3) -> U12#(X1,X2,X3)
    U12#(X1,X2,active(X3)) -> U12#(X1,X2,X3) ->
    U12#(X1,active(X2),X3) -> U12#(X1,X2,X3)
    U12#(X1,X2,active(X3)) -> U12#(X1,X2,X3) ->
    U12#(X1,X2,active(X3)) -> U12#(X1,X2,X3)
    active#(plus(N,0())) -> mark#(N) ->
    mark#(U11(X1,X2,X3)) -> mark#(X1)
    active#(plus(N,0())) -> mark#(N) ->
    mark#(U11(X1,X2,X3)) -> U11#(mark(X1),X2,X3)
    active#(plus(N,0())) -> mark#(N) ->
    mark#(U11(X1,X2,X3)) -> active#(U11(mark(X1),X2,X3))
    active#(plus(N,0())) -> mark#(N) ->
    mark#(tt()) -> active#(tt())
    active#(plus(N,0())) -> mark#(N) ->
    mark#(U12(X1,X2,X3)) -> mark#(X1)
    active#(plus(N,0())) -> mark#(N) ->
    mark#(U12(X1,X2,X3)) -> U12#(mark(X1),X2,X3)
    active#(plus(N,0())) -> mark#(N) ->
    mark#(U12(X1,X2,X3)) -> active#(U12(mark(X1),X2,X3))
    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#(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,s(M))) -> U11#(tt(),M,N) ->
    U11#(X1,mark(X2),X3) -> U11#(X1,X2,X3)
    active#(plus(N,s(M))) -> U11#(tt(),M,N) ->
    U11#(X1,X2,mark(X3)) -> U11#(X1,X2,X3)
    active#(plus(N,s(M))) -> U11#(tt(),M,N) ->
    U11#(X1,active(X2),X3) -> U11#(X1,X2,X3)
    active#(plus(N,s(M))) -> U11#(tt(),M,N) ->
    U11#(X1,X2,active(X3)) -> U11#(X1,X2,X3)
    active#(plus(N,s(M))) -> mark#(U11(tt(),M,N)) ->
    mark#(U11(X1,X2,X3)) -> mark#(X1)
    active#(plus(N,s(M))) -> mark#(U11(tt(),M,N)) ->
    mark#(U11(X1,X2,X3)) -> U11#(mark(X1),X2,X3)
    active#(plus(N,s(M))) -> mark#(U11(tt(),M,N)) ->
    mark#(U11(X1,X2,X3)) -> active#(U11(mark(X1),X2,X3))
    active#(plus(N,s(M))) -> mark#(U11(tt(),M,N)) ->
    mark#(U12(X1,X2,X3)) -> mark#(X1)
    active#(plus(N,s(M))) -> mark#(U11(tt(),M,N)) ->
    mark#(U12(X1,X2,X3)) -> U12#(mark(X1),X2,X3)
    active#(plus(N,s(M))) -> mark#(U11(tt(),M,N)) ->
    mark#(U12(X1,X2,X3)) -> active#(U12(mark(X1),X2,X3))
    active#(plus(N,s(M))) -> mark#(U11(tt(),M,N)) ->
    mark#(s(X)) -> mark#(X)
    active#(plus(N,s(M))) -> mark#(U11(tt(),M,N)) ->
    mark#(s(X)) -> s#(mark(X))
    active#(plus(N,s(M))) -> mark#(U11(tt(),M,N)) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(plus(N,s(M))) -> mark#(U11(tt(),M,N)) ->
    mark#(plus(X1,X2)) -> mark#(X2)
    active#(plus(N,s(M))) -> mark#(U11(tt(),M,N)) ->
    mark#(plus(X1,X2)) -> mark#(X1)
    active#(plus(N,s(M))) -> mark#(U11(tt(),M,N)) ->
    mark#(plus(X1,X2)) -> plus#(mark(X1),mark(X2))
    active#(plus(N,s(M))) -> mark#(U11(tt(),M,N)) ->
    mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
    active#(U12(tt(),M,N)) -> s#(plus(N,M)) ->
    s#(mark(X)) -> s#(X)
    active#(U12(tt(),M,N)) -> s#(plus(N,M)) ->
    s#(active(X)) -> s#(X)
    active#(U12(tt(),M,N)) -> plus#(N,M) ->
    plus#(mark(X1),X2) -> plus#(X1,X2)
    active#(U12(tt(),M,N)) -> plus#(N,M) ->
    plus#(X1,mark(X2)) -> plus#(X1,X2)
    active#(U12(tt(),M,N)) -> plus#(N,M) ->
    plus#(active(X1),X2) -> plus#(X1,X2)
    active#(U12(tt(),M,N)) -> plus#(N,M) ->
    plus#(X1,active(X2)) -> plus#(X1,X2)
    active#(U12(tt(),M,N)) -> mark#(s(plus(N,M))) ->
    mark#(U11(X1,X2,X3)) -> mark#(X1)
    active#(U12(tt(),M,N)) -> mark#(s(plus(N,M))) ->
    mark#(U11(X1,X2,X3)) -> U11#(mark(X1),X2,X3)
    active#(U12(tt(),M,N)) -> mark#(s(plus(N,M))) ->
    mark#(U11(X1,X2,X3)) -> active#(U11(mark(X1),X2,X3))
    active#(U12(tt(),M,N)) -> mark#(s(plus(N,M))) ->
    mark#(U12(X1,X2,X3)) -> mark#(X1)
    active#(U12(tt(),M,N)) -> mark#(s(plus(N,M))) ->
    mark#(U12(X1,X2,X3)) -> U12#(mark(X1),X2,X3)
    active#(U12(tt(),M,N)) -> mark#(s(plus(N,M))) ->
    mark#(U12(X1,X2,X3)) -> active#(U12(mark(X1),X2,X3))
    active#(U12(tt(),M,N)) -> mark#(s(plus(N,M))) ->
    mark#(s(X)) -> mark#(X)
    active#(U12(tt(),M,N)) -> mark#(s(plus(N,M))) ->
    mark#(s(X)) -> s#(mark(X))
    active#(U12(tt(),M,N)) -> mark#(s(plus(N,M))) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(U12(tt(),M,N)) -> mark#(s(plus(N,M))) ->
    mark#(plus(X1,X2)) -> mark#(X2)
    active#(U12(tt(),M,N)) -> mark#(s(plus(N,M))) ->
    mark#(plus(X1,X2)) -> mark#(X1)
    active#(U12(tt(),M,N)) -> mark#(s(plus(N,M))) ->
    mark#(plus(X1,X2)) -> plus#(mark(X1),mark(X2))
    active#(U12(tt(),M,N)) -> mark#(s(plus(N,M))) ->
    mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
    active#(U11(tt(),M,N)) -> mark#(U12(tt(),M,N)) ->
    mark#(U11(X1,X2,X3)) -> mark#(X1)
    active#(U11(tt(),M,N)) -> mark#(U12(tt(),M,N)) ->
    mark#(U11(X1,X2,X3)) -> U11#(mark(X1),X2,X3)
    active#(U11(tt(),M,N)) -> mark#(U12(tt(),M,N)) ->
    mark#(U11(X1,X2,X3)) -> active#(U11(mark(X1),X2,X3))
    active#(U11(tt(),M,N)) -> mark#(U12(tt(),M,N)) ->
    mark#(U12(X1,X2,X3)) -> mark#(X1)
    active#(U11(tt(),M,N)) -> mark#(U12(tt(),M,N)) ->
    mark#(U12(X1,X2,X3)) -> U12#(mark(X1),X2,X3)
    active#(U11(tt(),M,N)) -> mark#(U12(tt(),M,N)) ->
    mark#(U12(X1,X2,X3)) -> active#(U12(mark(X1),X2,X3))
    active#(U11(tt(),M,N)) -> mark#(U12(tt(),M,N)) ->
    mark#(s(X)) -> mark#(X)
    active#(U11(tt(),M,N)) -> mark#(U12(tt(),M,N)) ->
    mark#(s(X)) -> s#(mark(X))
    active#(U11(tt(),M,N)) -> mark#(U12(tt(),M,N)) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(U11(tt(),M,N)) -> mark#(U12(tt(),M,N)) ->
    mark#(plus(X1,X2)) -> mark#(X2)
    active#(U11(tt(),M,N)) -> mark#(U12(tt(),M,N)) ->
    mark#(plus(X1,X2)) -> mark#(X1)
    active#(U11(tt(),M,N)) -> mark#(U12(tt(),M,N)) ->
    mark#(plus(X1,X2)) -> plus#(mark(X1),mark(X2))
    active#(U11(tt(),M,N)) -> mark#(U12(tt(),M,N)) ->
    mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
    active#(U11(tt(),M,N)) -> U12#(tt(),M,N) ->
    U12#(X1,mark(X2),X3) -> U12#(X1,X2,X3)
    active#(U11(tt(),M,N)) -> U12#(tt(),M,N) ->
    U12#(X1,X2,mark(X3)) -> U12#(X1,X2,X3)
    active#(U11(tt(),M,N)) -> U12#(tt(),M,N) ->
    U12#(X1,active(X2),X3) -> U12#(X1,X2,X3)
    active#(U11(tt(),M,N)) -> U12#(tt(),M,N) -> U12#(X1,X2,active(X3)) -> U12#(X1,X2,X3)
   SCC Processor:
    #sccs: 5
    #rules: 31
    #arcs: 285/1681
    DPs:
     mark#(s(X)) -> mark#(X)
     mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
     active#(plus(N,s(M))) -> mark#(U11(tt(),M,N))
     mark#(plus(X1,X2)) -> mark#(X1)
     mark#(plus(X1,X2)) -> mark#(X2)
     mark#(s(X)) -> active#(s(mark(X)))
     active#(plus(N,0())) -> mark#(N)
     mark#(U12(X1,X2,X3)) -> active#(U12(mark(X1),X2,X3))
     active#(U12(tt(),M,N)) -> mark#(s(plus(N,M)))
     mark#(U12(X1,X2,X3)) -> mark#(X1)
     mark#(U11(X1,X2,X3)) -> active#(U11(mark(X1),X2,X3))
     active#(U11(tt(),M,N)) -> mark#(U12(tt(),M,N))
     mark#(U11(X1,X2,X3)) -> mark#(X1)
    TRS:
     active(U11(tt(),M,N)) -> mark(U12(tt(),M,N))
     active(U12(tt(),M,N)) -> mark(s(plus(N,M)))
     active(plus(N,0())) -> mark(N)
     active(plus(N,s(M))) -> mark(U11(tt(),M,N))
     mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
     mark(tt()) -> active(tt())
     mark(U12(X1,X2,X3)) -> active(U12(mark(X1),X2,X3))
     mark(s(X)) -> active(s(mark(X)))
     mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
     mark(0()) -> active(0())
     U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
     U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
     U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
     U11(active(X1),X2,X3) -> U11(X1,X2,X3)
     U11(X1,active(X2),X3) -> U11(X1,X2,X3)
     U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
     U12(mark(X1),X2,X3) -> U12(X1,X2,X3)
     U12(X1,mark(X2),X3) -> U12(X1,X2,X3)
     U12(X1,X2,mark(X3)) -> U12(X1,X2,X3)
     U12(active(X1),X2,X3) -> U12(X1,X2,X3)
     U12(X1,active(X2),X3) -> U12(X1,X2,X3)
     U12(X1,X2,active(X3)) -> U12(X1,X2,X3)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     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)
    Open
    
    DPs:
     U12#(X1,X2,active(X3)) -> U12#(X1,X2,X3)
     U12#(X1,active(X2),X3) -> U12#(X1,X2,X3)
     U12#(active(X1),X2,X3) -> U12#(X1,X2,X3)
     U12#(X1,X2,mark(X3)) -> U12#(X1,X2,X3)
     U12#(X1,mark(X2),X3) -> U12#(X1,X2,X3)
     U12#(mark(X1),X2,X3) -> U12#(X1,X2,X3)
    TRS:
     active(U11(tt(),M,N)) -> mark(U12(tt(),M,N))
     active(U12(tt(),M,N)) -> mark(s(plus(N,M)))
     active(plus(N,0())) -> mark(N)
     active(plus(N,s(M))) -> mark(U11(tt(),M,N))
     mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
     mark(tt()) -> active(tt())
     mark(U12(X1,X2,X3)) -> active(U12(mark(X1),X2,X3))
     mark(s(X)) -> active(s(mark(X)))
     mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
     mark(0()) -> active(0())
     U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
     U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
     U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
     U11(active(X1),X2,X3) -> U11(X1,X2,X3)
     U11(X1,active(X2),X3) -> U11(X1,X2,X3)
     U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
     U12(mark(X1),X2,X3) -> U12(X1,X2,X3)
     U12(X1,mark(X2),X3) -> U12(X1,X2,X3)
     U12(X1,X2,mark(X3)) -> U12(X1,X2,X3)
     U12(active(X1),X2,X3) -> U12(X1,X2,X3)
     U12(X1,active(X2),X3) -> U12(X1,X2,X3)
     U12(X1,X2,active(X3)) -> U12(X1,X2,X3)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     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)
    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(U11(tt(),M,N)) -> mark(U12(tt(),M,N))
     active(U12(tt(),M,N)) -> mark(s(plus(N,M)))
     active(plus(N,0())) -> mark(N)
     active(plus(N,s(M))) -> mark(U11(tt(),M,N))
     mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
     mark(tt()) -> active(tt())
     mark(U12(X1,X2,X3)) -> active(U12(mark(X1),X2,X3))
     mark(s(X)) -> active(s(mark(X)))
     mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
     mark(0()) -> active(0())
     U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
     U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
     U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
     U11(active(X1),X2,X3) -> U11(X1,X2,X3)
     U11(X1,active(X2),X3) -> U11(X1,X2,X3)
     U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
     U12(mark(X1),X2,X3) -> U12(X1,X2,X3)
     U12(X1,mark(X2),X3) -> U12(X1,X2,X3)
     U12(X1,X2,mark(X3)) -> U12(X1,X2,X3)
     U12(active(X1),X2,X3) -> U12(X1,X2,X3)
     U12(X1,active(X2),X3) -> U12(X1,X2,X3)
     U12(X1,X2,active(X3)) -> U12(X1,X2,X3)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     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)
    Open
    
    DPs:
     s#(mark(X)) -> s#(X)
     s#(active(X)) -> s#(X)
    TRS:
     active(U11(tt(),M,N)) -> mark(U12(tt(),M,N))
     active(U12(tt(),M,N)) -> mark(s(plus(N,M)))
     active(plus(N,0())) -> mark(N)
     active(plus(N,s(M))) -> mark(U11(tt(),M,N))
     mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
     mark(tt()) -> active(tt())
     mark(U12(X1,X2,X3)) -> active(U12(mark(X1),X2,X3))
     mark(s(X)) -> active(s(mark(X)))
     mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
     mark(0()) -> active(0())
     U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
     U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
     U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
     U11(active(X1),X2,X3) -> U11(X1,X2,X3)
     U11(X1,active(X2),X3) -> U11(X1,X2,X3)
     U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
     U12(mark(X1),X2,X3) -> U12(X1,X2,X3)
     U12(X1,mark(X2),X3) -> U12(X1,X2,X3)
     U12(X1,X2,mark(X3)) -> U12(X1,X2,X3)
     U12(active(X1),X2,X3) -> U12(X1,X2,X3)
     U12(X1,active(X2),X3) -> U12(X1,X2,X3)
     U12(X1,X2,active(X3)) -> U12(X1,X2,X3)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     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)
    Open
    
    DPs:
     U11#(mark(X1),X2,X3) -> U11#(X1,X2,X3)
     U11#(X1,X2,active(X3)) -> U11#(X1,X2,X3)
     U11#(X1,active(X2),X3) -> U11#(X1,X2,X3)
     U11#(active(X1),X2,X3) -> U11#(X1,X2,X3)
     U11#(X1,X2,mark(X3)) -> U11#(X1,X2,X3)
     U11#(X1,mark(X2),X3) -> U11#(X1,X2,X3)
    TRS:
     active(U11(tt(),M,N)) -> mark(U12(tt(),M,N))
     active(U12(tt(),M,N)) -> mark(s(plus(N,M)))
     active(plus(N,0())) -> mark(N)
     active(plus(N,s(M))) -> mark(U11(tt(),M,N))
     mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
     mark(tt()) -> active(tt())
     mark(U12(X1,X2,X3)) -> active(U12(mark(X1),X2,X3))
     mark(s(X)) -> active(s(mark(X)))
     mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
     mark(0()) -> active(0())
     U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
     U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
     U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
     U11(active(X1),X2,X3) -> U11(X1,X2,X3)
     U11(X1,active(X2),X3) -> U11(X1,X2,X3)
     U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
     U12(mark(X1),X2,X3) -> U12(X1,X2,X3)
     U12(X1,mark(X2),X3) -> U12(X1,X2,X3)
     U12(X1,X2,mark(X3)) -> U12(X1,X2,X3)
     U12(active(X1),X2,X3) -> U12(X1,X2,X3)
     U12(X1,active(X2),X3) -> U12(X1,X2,X3)
     U12(X1,X2,active(X3)) -> U12(X1,X2,X3)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     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)
    Open