MAYBE

Problem:
 active(U11(tt(),N)) -> mark(N)
 active(U21(tt(),M,N)) -> mark(s(plus(N,M)))
 active(U31(tt())) -> mark(0())
 active(U41(tt(),M,N)) -> mark(plus(x(N,M),N))
 active(and(tt(),X)) -> mark(X)
 active(isNat(0())) -> mark(tt())
 active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2)))
 active(isNat(s(V1))) -> mark(isNat(V1))
 active(isNat(x(V1,V2))) -> mark(and(isNat(V1),isNat(V2)))
 active(plus(N,0())) -> mark(U11(isNat(N),N))
 active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N))
 active(x(N,0())) -> mark(U31(isNat(N)))
 active(x(N,s(M))) -> mark(U41(and(isNat(M),isNat(N)),M,N))
 mark(U11(X1,X2)) -> active(U11(mark(X1),X2))
 mark(tt()) -> active(tt())
 mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3))
 mark(s(X)) -> active(s(mark(X)))
 mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
 mark(U31(X)) -> active(U31(mark(X)))
 mark(0()) -> active(0())
 mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
 mark(x(X1,X2)) -> active(x(mark(X1),mark(X2)))
 mark(and(X1,X2)) -> active(and(mark(X1),X2))
 mark(isNat(X)) -> active(isNat(X))
 U11(mark(X1),X2) -> U11(X1,X2)
 U11(X1,mark(X2)) -> U11(X1,X2)
 U11(active(X1),X2) -> U11(X1,X2)
 U11(X1,active(X2)) -> U11(X1,X2)
 U21(mark(X1),X2,X3) -> U21(X1,X2,X3)
 U21(X1,mark(X2),X3) -> U21(X1,X2,X3)
 U21(X1,X2,mark(X3)) -> U21(X1,X2,X3)
 U21(active(X1),X2,X3) -> U21(X1,X2,X3)
 U21(X1,active(X2),X3) -> U21(X1,X2,X3)
 U21(X1,X2,active(X3)) -> U21(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)
 U31(mark(X)) -> U31(X)
 U31(active(X)) -> U31(X)
 U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
 U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
 U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
 U41(active(X1),X2,X3) -> U41(X1,X2,X3)
 U41(X1,active(X2),X3) -> U41(X1,X2,X3)
 U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
 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)
 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)
 isNat(mark(X)) -> isNat(X)
 isNat(active(X)) -> isNat(X)

Proof:
 DP Processor:
  DPs:
   active#(U11(tt(),N)) -> mark#(N)
   active#(U21(tt(),M,N)) -> plus#(N,M)
   active#(U21(tt(),M,N)) -> s#(plus(N,M))
   active#(U21(tt(),M,N)) -> mark#(s(plus(N,M)))
   active#(U31(tt())) -> mark#(0())
   active#(U41(tt(),M,N)) -> x#(N,M)
   active#(U41(tt(),M,N)) -> plus#(x(N,M),N)
   active#(U41(tt(),M,N)) -> mark#(plus(x(N,M),N))
   active#(and(tt(),X)) -> mark#(X)
   active#(isNat(0())) -> mark#(tt())
   active#(isNat(plus(V1,V2))) -> isNat#(V2)
   active#(isNat(plus(V1,V2))) -> isNat#(V1)
   active#(isNat(plus(V1,V2))) -> and#(isNat(V1),isNat(V2))
   active#(isNat(plus(V1,V2))) -> mark#(and(isNat(V1),isNat(V2)))
   active#(isNat(s(V1))) -> isNat#(V1)
   active#(isNat(s(V1))) -> mark#(isNat(V1))
   active#(isNat(x(V1,V2))) -> isNat#(V2)
   active#(isNat(x(V1,V2))) -> isNat#(V1)
   active#(isNat(x(V1,V2))) -> and#(isNat(V1),isNat(V2))
   active#(isNat(x(V1,V2))) -> mark#(and(isNat(V1),isNat(V2)))
   active#(plus(N,0())) -> isNat#(N)
   active#(plus(N,0())) -> U11#(isNat(N),N)
   active#(plus(N,0())) -> mark#(U11(isNat(N),N))
   active#(plus(N,s(M))) -> isNat#(N)
   active#(plus(N,s(M))) -> isNat#(M)
   active#(plus(N,s(M))) -> and#(isNat(M),isNat(N))
   active#(plus(N,s(M))) -> U21#(and(isNat(M),isNat(N)),M,N)
   active#(plus(N,s(M))) -> mark#(U21(and(isNat(M),isNat(N)),M,N))
   active#(x(N,0())) -> isNat#(N)
   active#(x(N,0())) -> U31#(isNat(N))
   active#(x(N,0())) -> mark#(U31(isNat(N)))
   active#(x(N,s(M))) -> isNat#(N)
   active#(x(N,s(M))) -> isNat#(M)
   active#(x(N,s(M))) -> and#(isNat(M),isNat(N))
   active#(x(N,s(M))) -> U41#(and(isNat(M),isNat(N)),M,N)
   active#(x(N,s(M))) -> mark#(U41(and(isNat(M),isNat(N)),M,N))
   mark#(U11(X1,X2)) -> mark#(X1)
   mark#(U11(X1,X2)) -> U11#(mark(X1),X2)
   mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
   mark#(tt()) -> active#(tt())
   mark#(U21(X1,X2,X3)) -> mark#(X1)
   mark#(U21(X1,X2,X3)) -> U21#(mark(X1),X2,X3)
   mark#(U21(X1,X2,X3)) -> active#(U21(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#(U31(X)) -> mark#(X)
   mark#(U31(X)) -> U31#(mark(X))
   mark#(U31(X)) -> active#(U31(mark(X)))
   mark#(0()) -> active#(0())
   mark#(U41(X1,X2,X3)) -> mark#(X1)
   mark#(U41(X1,X2,X3)) -> U41#(mark(X1),X2,X3)
   mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3))
   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)))
   mark#(and(X1,X2)) -> mark#(X1)
   mark#(and(X1,X2)) -> and#(mark(X1),X2)
   mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
   mark#(isNat(X)) -> active#(isNat(X))
   U11#(mark(X1),X2) -> U11#(X1,X2)
   U11#(X1,mark(X2)) -> U11#(X1,X2)
   U11#(active(X1),X2) -> U11#(X1,X2)
   U11#(X1,active(X2)) -> U11#(X1,X2)
   U21#(mark(X1),X2,X3) -> U21#(X1,X2,X3)
   U21#(X1,mark(X2),X3) -> U21#(X1,X2,X3)
   U21#(X1,X2,mark(X3)) -> U21#(X1,X2,X3)
   U21#(active(X1),X2,X3) -> U21#(X1,X2,X3)
   U21#(X1,active(X2),X3) -> U21#(X1,X2,X3)
   U21#(X1,X2,active(X3)) -> U21#(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)
   U31#(mark(X)) -> U31#(X)
   U31#(active(X)) -> U31#(X)
   U41#(mark(X1),X2,X3) -> U41#(X1,X2,X3)
   U41#(X1,mark(X2),X3) -> U41#(X1,X2,X3)
   U41#(X1,X2,mark(X3)) -> U41#(X1,X2,X3)
   U41#(active(X1),X2,X3) -> U41#(X1,X2,X3)
   U41#(X1,active(X2),X3) -> U41#(X1,X2,X3)
   U41#(X1,X2,active(X3)) -> U41#(X1,X2,X3)
   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)
   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)
   isNat#(mark(X)) -> isNat#(X)
   isNat#(active(X)) -> isNat#(X)
  TRS:
   active(U11(tt(),N)) -> mark(N)
   active(U21(tt(),M,N)) -> mark(s(plus(N,M)))
   active(U31(tt())) -> mark(0())
   active(U41(tt(),M,N)) -> mark(plus(x(N,M),N))
   active(and(tt(),X)) -> mark(X)
   active(isNat(0())) -> mark(tt())
   active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2)))
   active(isNat(s(V1))) -> mark(isNat(V1))
   active(isNat(x(V1,V2))) -> mark(and(isNat(V1),isNat(V2)))
   active(plus(N,0())) -> mark(U11(isNat(N),N))
   active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N))
   active(x(N,0())) -> mark(U31(isNat(N)))
   active(x(N,s(M))) -> mark(U41(and(isNat(M),isNat(N)),M,N))
   mark(U11(X1,X2)) -> active(U11(mark(X1),X2))
   mark(tt()) -> active(tt())
   mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3))
   mark(s(X)) -> active(s(mark(X)))
   mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
   mark(U31(X)) -> active(U31(mark(X)))
   mark(0()) -> active(0())
   mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
   mark(x(X1,X2)) -> active(x(mark(X1),mark(X2)))
   mark(and(X1,X2)) -> active(and(mark(X1),X2))
   mark(isNat(X)) -> active(isNat(X))
   U11(mark(X1),X2) -> U11(X1,X2)
   U11(X1,mark(X2)) -> U11(X1,X2)
   U11(active(X1),X2) -> U11(X1,X2)
   U11(X1,active(X2)) -> U11(X1,X2)
   U21(mark(X1),X2,X3) -> U21(X1,X2,X3)
   U21(X1,mark(X2),X3) -> U21(X1,X2,X3)
   U21(X1,X2,mark(X3)) -> U21(X1,X2,X3)
   U21(active(X1),X2,X3) -> U21(X1,X2,X3)
   U21(X1,active(X2),X3) -> U21(X1,X2,X3)
   U21(X1,X2,active(X3)) -> U21(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)
   U31(mark(X)) -> U31(X)
   U31(active(X)) -> U31(X)
   U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
   U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
   U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
   U41(active(X1),X2,X3) -> U41(X1,X2,X3)
   U41(X1,active(X2),X3) -> U41(X1,X2,X3)
   U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
   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)
   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)
   isNat(mark(X)) -> isNat(X)
   isNat(active(X)) -> isNat(X)
  TDG Processor:
   DPs:
    active#(U11(tt(),N)) -> mark#(N)
    active#(U21(tt(),M,N)) -> plus#(N,M)
    active#(U21(tt(),M,N)) -> s#(plus(N,M))
    active#(U21(tt(),M,N)) -> mark#(s(plus(N,M)))
    active#(U31(tt())) -> mark#(0())
    active#(U41(tt(),M,N)) -> x#(N,M)
    active#(U41(tt(),M,N)) -> plus#(x(N,M),N)
    active#(U41(tt(),M,N)) -> mark#(plus(x(N,M),N))
    active#(and(tt(),X)) -> mark#(X)
    active#(isNat(0())) -> mark#(tt())
    active#(isNat(plus(V1,V2))) -> isNat#(V2)
    active#(isNat(plus(V1,V2))) -> isNat#(V1)
    active#(isNat(plus(V1,V2))) -> and#(isNat(V1),isNat(V2))
    active#(isNat(plus(V1,V2))) -> mark#(and(isNat(V1),isNat(V2)))
    active#(isNat(s(V1))) -> isNat#(V1)
    active#(isNat(s(V1))) -> mark#(isNat(V1))
    active#(isNat(x(V1,V2))) -> isNat#(V2)
    active#(isNat(x(V1,V2))) -> isNat#(V1)
    active#(isNat(x(V1,V2))) -> and#(isNat(V1),isNat(V2))
    active#(isNat(x(V1,V2))) -> mark#(and(isNat(V1),isNat(V2)))
    active#(plus(N,0())) -> isNat#(N)
    active#(plus(N,0())) -> U11#(isNat(N),N)
    active#(plus(N,0())) -> mark#(U11(isNat(N),N))
    active#(plus(N,s(M))) -> isNat#(N)
    active#(plus(N,s(M))) -> isNat#(M)
    active#(plus(N,s(M))) -> and#(isNat(M),isNat(N))
    active#(plus(N,s(M))) -> U21#(and(isNat(M),isNat(N)),M,N)
    active#(plus(N,s(M))) -> mark#(U21(and(isNat(M),isNat(N)),M,N))
    active#(x(N,0())) -> isNat#(N)
    active#(x(N,0())) -> U31#(isNat(N))
    active#(x(N,0())) -> mark#(U31(isNat(N)))
    active#(x(N,s(M))) -> isNat#(N)
    active#(x(N,s(M))) -> isNat#(M)
    active#(x(N,s(M))) -> and#(isNat(M),isNat(N))
    active#(x(N,s(M))) -> U41#(and(isNat(M),isNat(N)),M,N)
    active#(x(N,s(M))) -> mark#(U41(and(isNat(M),isNat(N)),M,N))
    mark#(U11(X1,X2)) -> mark#(X1)
    mark#(U11(X1,X2)) -> U11#(mark(X1),X2)
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
    mark#(tt()) -> active#(tt())
    mark#(U21(X1,X2,X3)) -> mark#(X1)
    mark#(U21(X1,X2,X3)) -> U21#(mark(X1),X2,X3)
    mark#(U21(X1,X2,X3)) -> active#(U21(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#(U31(X)) -> mark#(X)
    mark#(U31(X)) -> U31#(mark(X))
    mark#(U31(X)) -> active#(U31(mark(X)))
    mark#(0()) -> active#(0())
    mark#(U41(X1,X2,X3)) -> mark#(X1)
    mark#(U41(X1,X2,X3)) -> U41#(mark(X1),X2,X3)
    mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3))
    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)))
    mark#(and(X1,X2)) -> mark#(X1)
    mark#(and(X1,X2)) -> and#(mark(X1),X2)
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    mark#(isNat(X)) -> active#(isNat(X))
    U11#(mark(X1),X2) -> U11#(X1,X2)
    U11#(X1,mark(X2)) -> U11#(X1,X2)
    U11#(active(X1),X2) -> U11#(X1,X2)
    U11#(X1,active(X2)) -> U11#(X1,X2)
    U21#(mark(X1),X2,X3) -> U21#(X1,X2,X3)
    U21#(X1,mark(X2),X3) -> U21#(X1,X2,X3)
    U21#(X1,X2,mark(X3)) -> U21#(X1,X2,X3)
    U21#(active(X1),X2,X3) -> U21#(X1,X2,X3)
    U21#(X1,active(X2),X3) -> U21#(X1,X2,X3)
    U21#(X1,X2,active(X3)) -> U21#(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)
    U31#(mark(X)) -> U31#(X)
    U31#(active(X)) -> U31#(X)
    U41#(mark(X1),X2,X3) -> U41#(X1,X2,X3)
    U41#(X1,mark(X2),X3) -> U41#(X1,X2,X3)
    U41#(X1,X2,mark(X3)) -> U41#(X1,X2,X3)
    U41#(active(X1),X2,X3) -> U41#(X1,X2,X3)
    U41#(X1,active(X2),X3) -> U41#(X1,X2,X3)
    U41#(X1,X2,active(X3)) -> U41#(X1,X2,X3)
    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)
    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)
    isNat#(mark(X)) -> isNat#(X)
    isNat#(active(X)) -> isNat#(X)
   TRS:
    active(U11(tt(),N)) -> mark(N)
    active(U21(tt(),M,N)) -> mark(s(plus(N,M)))
    active(U31(tt())) -> mark(0())
    active(U41(tt(),M,N)) -> mark(plus(x(N,M),N))
    active(and(tt(),X)) -> mark(X)
    active(isNat(0())) -> mark(tt())
    active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2)))
    active(isNat(s(V1))) -> mark(isNat(V1))
    active(isNat(x(V1,V2))) -> mark(and(isNat(V1),isNat(V2)))
    active(plus(N,0())) -> mark(U11(isNat(N),N))
    active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N))
    active(x(N,0())) -> mark(U31(isNat(N)))
    active(x(N,s(M))) -> mark(U41(and(isNat(M),isNat(N)),M,N))
    mark(U11(X1,X2)) -> active(U11(mark(X1),X2))
    mark(tt()) -> active(tt())
    mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3))
    mark(s(X)) -> active(s(mark(X)))
    mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
    mark(U31(X)) -> active(U31(mark(X)))
    mark(0()) -> active(0())
    mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
    mark(x(X1,X2)) -> active(x(mark(X1),mark(X2)))
    mark(and(X1,X2)) -> active(and(mark(X1),X2))
    mark(isNat(X)) -> active(isNat(X))
    U11(mark(X1),X2) -> U11(X1,X2)
    U11(X1,mark(X2)) -> U11(X1,X2)
    U11(active(X1),X2) -> U11(X1,X2)
    U11(X1,active(X2)) -> U11(X1,X2)
    U21(mark(X1),X2,X3) -> U21(X1,X2,X3)
    U21(X1,mark(X2),X3) -> U21(X1,X2,X3)
    U21(X1,X2,mark(X3)) -> U21(X1,X2,X3)
    U21(active(X1),X2,X3) -> U21(X1,X2,X3)
    U21(X1,active(X2),X3) -> U21(X1,X2,X3)
    U21(X1,X2,active(X3)) -> U21(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)
    U31(mark(X)) -> U31(X)
    U31(active(X)) -> U31(X)
    U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
    U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
    U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
    U41(active(X1),X2,X3) -> U41(X1,X2,X3)
    U41(X1,active(X2),X3) -> U41(X1,X2,X3)
    U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
    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)
    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)
    isNat(mark(X)) -> isNat(X)
    isNat(active(X)) -> isNat(X)
   graph:
    ...
   EDG Processor:
    DPs:
     active#(U11(tt(),N)) -> mark#(N)
     active#(U21(tt(),M,N)) -> plus#(N,M)
     active#(U21(tt(),M,N)) -> s#(plus(N,M))
     active#(U21(tt(),M,N)) -> mark#(s(plus(N,M)))
     active#(U31(tt())) -> mark#(0())
     active#(U41(tt(),M,N)) -> x#(N,M)
     active#(U41(tt(),M,N)) -> plus#(x(N,M),N)
     active#(U41(tt(),M,N)) -> mark#(plus(x(N,M),N))
     active#(and(tt(),X)) -> mark#(X)
     active#(isNat(0())) -> mark#(tt())
     active#(isNat(plus(V1,V2))) -> isNat#(V2)
     active#(isNat(plus(V1,V2))) -> isNat#(V1)
     active#(isNat(plus(V1,V2))) -> and#(isNat(V1),isNat(V2))
     active#(isNat(plus(V1,V2))) -> mark#(and(isNat(V1),isNat(V2)))
     active#(isNat(s(V1))) -> isNat#(V1)
     active#(isNat(s(V1))) -> mark#(isNat(V1))
     active#(isNat(x(V1,V2))) -> isNat#(V2)
     active#(isNat(x(V1,V2))) -> isNat#(V1)
     active#(isNat(x(V1,V2))) -> and#(isNat(V1),isNat(V2))
     active#(isNat(x(V1,V2))) -> mark#(and(isNat(V1),isNat(V2)))
     active#(plus(N,0())) -> isNat#(N)
     active#(plus(N,0())) -> U11#(isNat(N),N)
     active#(plus(N,0())) -> mark#(U11(isNat(N),N))
     active#(plus(N,s(M))) -> isNat#(N)
     active#(plus(N,s(M))) -> isNat#(M)
     active#(plus(N,s(M))) -> and#(isNat(M),isNat(N))
     active#(plus(N,s(M))) -> U21#(and(isNat(M),isNat(N)),M,N)
     active#(plus(N,s(M))) -> mark#(U21(and(isNat(M),isNat(N)),M,N))
     active#(x(N,0())) -> isNat#(N)
     active#(x(N,0())) -> U31#(isNat(N))
     active#(x(N,0())) -> mark#(U31(isNat(N)))
     active#(x(N,s(M))) -> isNat#(N)
     active#(x(N,s(M))) -> isNat#(M)
     active#(x(N,s(M))) -> and#(isNat(M),isNat(N))
     active#(x(N,s(M))) -> U41#(and(isNat(M),isNat(N)),M,N)
     active#(x(N,s(M))) -> mark#(U41(and(isNat(M),isNat(N)),M,N))
     mark#(U11(X1,X2)) -> mark#(X1)
     mark#(U11(X1,X2)) -> U11#(mark(X1),X2)
     mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
     mark#(tt()) -> active#(tt())
     mark#(U21(X1,X2,X3)) -> mark#(X1)
     mark#(U21(X1,X2,X3)) -> U21#(mark(X1),X2,X3)
     mark#(U21(X1,X2,X3)) -> active#(U21(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#(U31(X)) -> mark#(X)
     mark#(U31(X)) -> U31#(mark(X))
     mark#(U31(X)) -> active#(U31(mark(X)))
     mark#(0()) -> active#(0())
     mark#(U41(X1,X2,X3)) -> mark#(X1)
     mark#(U41(X1,X2,X3)) -> U41#(mark(X1),X2,X3)
     mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3))
     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)))
     mark#(and(X1,X2)) -> mark#(X1)
     mark#(and(X1,X2)) -> and#(mark(X1),X2)
     mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
     mark#(isNat(X)) -> active#(isNat(X))
     U11#(mark(X1),X2) -> U11#(X1,X2)
     U11#(X1,mark(X2)) -> U11#(X1,X2)
     U11#(active(X1),X2) -> U11#(X1,X2)
     U11#(X1,active(X2)) -> U11#(X1,X2)
     U21#(mark(X1),X2,X3) -> U21#(X1,X2,X3)
     U21#(X1,mark(X2),X3) -> U21#(X1,X2,X3)
     U21#(X1,X2,mark(X3)) -> U21#(X1,X2,X3)
     U21#(active(X1),X2,X3) -> U21#(X1,X2,X3)
     U21#(X1,active(X2),X3) -> U21#(X1,X2,X3)
     U21#(X1,X2,active(X3)) -> U21#(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)
     U31#(mark(X)) -> U31#(X)
     U31#(active(X)) -> U31#(X)
     U41#(mark(X1),X2,X3) -> U41#(X1,X2,X3)
     U41#(X1,mark(X2),X3) -> U41#(X1,X2,X3)
     U41#(X1,X2,mark(X3)) -> U41#(X1,X2,X3)
     U41#(active(X1),X2,X3) -> U41#(X1,X2,X3)
     U41#(X1,active(X2),X3) -> U41#(X1,X2,X3)
     U41#(X1,X2,active(X3)) -> U41#(X1,X2,X3)
     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)
     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)
     isNat#(mark(X)) -> isNat#(X)
     isNat#(active(X)) -> isNat#(X)
    TRS:
     active(U11(tt(),N)) -> mark(N)
     active(U21(tt(),M,N)) -> mark(s(plus(N,M)))
     active(U31(tt())) -> mark(0())
     active(U41(tt(),M,N)) -> mark(plus(x(N,M),N))
     active(and(tt(),X)) -> mark(X)
     active(isNat(0())) -> mark(tt())
     active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2)))
     active(isNat(s(V1))) -> mark(isNat(V1))
     active(isNat(x(V1,V2))) -> mark(and(isNat(V1),isNat(V2)))
     active(plus(N,0())) -> mark(U11(isNat(N),N))
     active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N))
     active(x(N,0())) -> mark(U31(isNat(N)))
     active(x(N,s(M))) -> mark(U41(and(isNat(M),isNat(N)),M,N))
     mark(U11(X1,X2)) -> active(U11(mark(X1),X2))
     mark(tt()) -> active(tt())
     mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3))
     mark(s(X)) -> active(s(mark(X)))
     mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
     mark(U31(X)) -> active(U31(mark(X)))
     mark(0()) -> active(0())
     mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
     mark(x(X1,X2)) -> active(x(mark(X1),mark(X2)))
     mark(and(X1,X2)) -> active(and(mark(X1),X2))
     mark(isNat(X)) -> active(isNat(X))
     U11(mark(X1),X2) -> U11(X1,X2)
     U11(X1,mark(X2)) -> U11(X1,X2)
     U11(active(X1),X2) -> U11(X1,X2)
     U11(X1,active(X2)) -> U11(X1,X2)
     U21(mark(X1),X2,X3) -> U21(X1,X2,X3)
     U21(X1,mark(X2),X3) -> U21(X1,X2,X3)
     U21(X1,X2,mark(X3)) -> U21(X1,X2,X3)
     U21(active(X1),X2,X3) -> U21(X1,X2,X3)
     U21(X1,active(X2),X3) -> U21(X1,X2,X3)
     U21(X1,X2,active(X3)) -> U21(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)
     U31(mark(X)) -> U31(X)
     U31(active(X)) -> U31(X)
     U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
     U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
     U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
     U41(active(X1),X2,X3) -> U41(X1,X2,X3)
     U41(X1,active(X2),X3) -> U41(X1,X2,X3)
     U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
     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)
     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)
     isNat(mark(X)) -> isNat(X)
     isNat(active(X)) -> isNat(X)
    graph:
     ...
    SCC Processor:
     #sccs: 10
     #rules: 64
     #arcs: 1088/9801
     DPs:
      mark#(isNat(X)) -> active#(isNat(X))
      active#(isNat(x(V1,V2))) -> mark#(and(isNat(V1),isNat(V2)))
      mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
      active#(x(N,s(M))) -> mark#(U41(and(isNat(M),isNat(N)),M,N))
      mark#(and(X1,X2)) -> mark#(X1)
      mark#(x(X1,X2)) -> active#(x(mark(X1),mark(X2)))
      active#(x(N,0())) -> mark#(U31(isNat(N)))
      mark#(x(X1,X2)) -> mark#(X1)
      mark#(x(X1,X2)) -> mark#(X2)
      mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3))
      active#(plus(N,s(M))) -> mark#(U21(and(isNat(M),isNat(N)),M,N))
      mark#(U41(X1,X2,X3)) -> mark#(X1)
      mark#(U31(X)) -> active#(U31(mark(X)))
      active#(plus(N,0())) -> mark#(U11(isNat(N),N))
      mark#(U31(X)) -> mark#(X)
      mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
      active#(isNat(s(V1))) -> mark#(isNat(V1))
      mark#(plus(X1,X2)) -> mark#(X1)
      mark#(plus(X1,X2)) -> mark#(X2)
      mark#(s(X)) -> active#(s(mark(X)))
      active#(isNat(plus(V1,V2))) -> mark#(and(isNat(V1),isNat(V2)))
      mark#(s(X)) -> mark#(X)
      mark#(U21(X1,X2,X3)) -> active#(U21(mark(X1),X2,X3))
      active#(and(tt(),X)) -> mark#(X)
      mark#(U21(X1,X2,X3)) -> mark#(X1)
      mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
      active#(U41(tt(),M,N)) -> mark#(plus(x(N,M),N))
      mark#(U11(X1,X2)) -> mark#(X1)
      active#(U21(tt(),M,N)) -> mark#(s(plus(N,M)))
      active#(U11(tt(),N)) -> mark#(N)
     TRS:
      active(U11(tt(),N)) -> mark(N)
      active(U21(tt(),M,N)) -> mark(s(plus(N,M)))
      active(U31(tt())) -> mark(0())
      active(U41(tt(),M,N)) -> mark(plus(x(N,M),N))
      active(and(tt(),X)) -> mark(X)
      active(isNat(0())) -> mark(tt())
      active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2)))
      active(isNat(s(V1))) -> mark(isNat(V1))
      active(isNat(x(V1,V2))) -> mark(and(isNat(V1),isNat(V2)))
      active(plus(N,0())) -> mark(U11(isNat(N),N))
      active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N))
      active(x(N,0())) -> mark(U31(isNat(N)))
      active(x(N,s(M))) -> mark(U41(and(isNat(M),isNat(N)),M,N))
      mark(U11(X1,X2)) -> active(U11(mark(X1),X2))
      mark(tt()) -> active(tt())
      mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3))
      mark(s(X)) -> active(s(mark(X)))
      mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
      mark(U31(X)) -> active(U31(mark(X)))
      mark(0()) -> active(0())
      mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
      mark(x(X1,X2)) -> active(x(mark(X1),mark(X2)))
      mark(and(X1,X2)) -> active(and(mark(X1),X2))
      mark(isNat(X)) -> active(isNat(X))
      U11(mark(X1),X2) -> U11(X1,X2)
      U11(X1,mark(X2)) -> U11(X1,X2)
      U11(active(X1),X2) -> U11(X1,X2)
      U11(X1,active(X2)) -> U11(X1,X2)
      U21(mark(X1),X2,X3) -> U21(X1,X2,X3)
      U21(X1,mark(X2),X3) -> U21(X1,X2,X3)
      U21(X1,X2,mark(X3)) -> U21(X1,X2,X3)
      U21(active(X1),X2,X3) -> U21(X1,X2,X3)
      U21(X1,active(X2),X3) -> U21(X1,X2,X3)
      U21(X1,X2,active(X3)) -> U21(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)
      U31(mark(X)) -> U31(X)
      U31(active(X)) -> U31(X)
      U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
      U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
      U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
      U41(active(X1),X2,X3) -> U41(X1,X2,X3)
      U41(X1,active(X2),X3) -> U41(X1,X2,X3)
      U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
      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)
      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)
      isNat(mark(X)) -> isNat(X)
      isNat(active(X)) -> isNat(X)
     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(),N)) -> mark(N)
      active(U21(tt(),M,N)) -> mark(s(plus(N,M)))
      active(U31(tt())) -> mark(0())
      active(U41(tt(),M,N)) -> mark(plus(x(N,M),N))
      active(and(tt(),X)) -> mark(X)
      active(isNat(0())) -> mark(tt())
      active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2)))
      active(isNat(s(V1))) -> mark(isNat(V1))
      active(isNat(x(V1,V2))) -> mark(and(isNat(V1),isNat(V2)))
      active(plus(N,0())) -> mark(U11(isNat(N),N))
      active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N))
      active(x(N,0())) -> mark(U31(isNat(N)))
      active(x(N,s(M))) -> mark(U41(and(isNat(M),isNat(N)),M,N))
      mark(U11(X1,X2)) -> active(U11(mark(X1),X2))
      mark(tt()) -> active(tt())
      mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3))
      mark(s(X)) -> active(s(mark(X)))
      mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
      mark(U31(X)) -> active(U31(mark(X)))
      mark(0()) -> active(0())
      mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
      mark(x(X1,X2)) -> active(x(mark(X1),mark(X2)))
      mark(and(X1,X2)) -> active(and(mark(X1),X2))
      mark(isNat(X)) -> active(isNat(X))
      U11(mark(X1),X2) -> U11(X1,X2)
      U11(X1,mark(X2)) -> U11(X1,X2)
      U11(active(X1),X2) -> U11(X1,X2)
      U11(X1,active(X2)) -> U11(X1,X2)
      U21(mark(X1),X2,X3) -> U21(X1,X2,X3)
      U21(X1,mark(X2),X3) -> U21(X1,X2,X3)
      U21(X1,X2,mark(X3)) -> U21(X1,X2,X3)
      U21(active(X1),X2,X3) -> U21(X1,X2,X3)
      U21(X1,active(X2),X3) -> U21(X1,X2,X3)
      U21(X1,X2,active(X3)) -> U21(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)
      U31(mark(X)) -> U31(X)
      U31(active(X)) -> U31(X)
      U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
      U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
      U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
      U41(active(X1),X2,X3) -> U41(X1,X2,X3)
      U41(X1,active(X2),X3) -> U41(X1,X2,X3)
      U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
      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)
      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)
      isNat(mark(X)) -> isNat(X)
      isNat(active(X)) -> isNat(X)
     Open
     
     DPs:
      s#(mark(X)) -> s#(X)
      s#(active(X)) -> s#(X)
     TRS:
      active(U11(tt(),N)) -> mark(N)
      active(U21(tt(),M,N)) -> mark(s(plus(N,M)))
      active(U31(tt())) -> mark(0())
      active(U41(tt(),M,N)) -> mark(plus(x(N,M),N))
      active(and(tt(),X)) -> mark(X)
      active(isNat(0())) -> mark(tt())
      active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2)))
      active(isNat(s(V1))) -> mark(isNat(V1))
      active(isNat(x(V1,V2))) -> mark(and(isNat(V1),isNat(V2)))
      active(plus(N,0())) -> mark(U11(isNat(N),N))
      active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N))
      active(x(N,0())) -> mark(U31(isNat(N)))
      active(x(N,s(M))) -> mark(U41(and(isNat(M),isNat(N)),M,N))
      mark(U11(X1,X2)) -> active(U11(mark(X1),X2))
      mark(tt()) -> active(tt())
      mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3))
      mark(s(X)) -> active(s(mark(X)))
      mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
      mark(U31(X)) -> active(U31(mark(X)))
      mark(0()) -> active(0())
      mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
      mark(x(X1,X2)) -> active(x(mark(X1),mark(X2)))
      mark(and(X1,X2)) -> active(and(mark(X1),X2))
      mark(isNat(X)) -> active(isNat(X))
      U11(mark(X1),X2) -> U11(X1,X2)
      U11(X1,mark(X2)) -> U11(X1,X2)
      U11(active(X1),X2) -> U11(X1,X2)
      U11(X1,active(X2)) -> U11(X1,X2)
      U21(mark(X1),X2,X3) -> U21(X1,X2,X3)
      U21(X1,mark(X2),X3) -> U21(X1,X2,X3)
      U21(X1,X2,mark(X3)) -> U21(X1,X2,X3)
      U21(active(X1),X2,X3) -> U21(X1,X2,X3)
      U21(X1,active(X2),X3) -> U21(X1,X2,X3)
      U21(X1,X2,active(X3)) -> U21(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)
      U31(mark(X)) -> U31(X)
      U31(active(X)) -> U31(X)
      U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
      U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
      U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
      U41(active(X1),X2,X3) -> U41(X1,X2,X3)
      U41(X1,active(X2),X3) -> U41(X1,X2,X3)
      U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
      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)
      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)
      isNat(mark(X)) -> isNat(X)
      isNat(active(X)) -> isNat(X)
     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(U11(tt(),N)) -> mark(N)
      active(U21(tt(),M,N)) -> mark(s(plus(N,M)))
      active(U31(tt())) -> mark(0())
      active(U41(tt(),M,N)) -> mark(plus(x(N,M),N))
      active(and(tt(),X)) -> mark(X)
      active(isNat(0())) -> mark(tt())
      active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2)))
      active(isNat(s(V1))) -> mark(isNat(V1))
      active(isNat(x(V1,V2))) -> mark(and(isNat(V1),isNat(V2)))
      active(plus(N,0())) -> mark(U11(isNat(N),N))
      active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N))
      active(x(N,0())) -> mark(U31(isNat(N)))
      active(x(N,s(M))) -> mark(U41(and(isNat(M),isNat(N)),M,N))
      mark(U11(X1,X2)) -> active(U11(mark(X1),X2))
      mark(tt()) -> active(tt())
      mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3))
      mark(s(X)) -> active(s(mark(X)))
      mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
      mark(U31(X)) -> active(U31(mark(X)))
      mark(0()) -> active(0())
      mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
      mark(x(X1,X2)) -> active(x(mark(X1),mark(X2)))
      mark(and(X1,X2)) -> active(and(mark(X1),X2))
      mark(isNat(X)) -> active(isNat(X))
      U11(mark(X1),X2) -> U11(X1,X2)
      U11(X1,mark(X2)) -> U11(X1,X2)
      U11(active(X1),X2) -> U11(X1,X2)
      U11(X1,active(X2)) -> U11(X1,X2)
      U21(mark(X1),X2,X3) -> U21(X1,X2,X3)
      U21(X1,mark(X2),X3) -> U21(X1,X2,X3)
      U21(X1,X2,mark(X3)) -> U21(X1,X2,X3)
      U21(active(X1),X2,X3) -> U21(X1,X2,X3)
      U21(X1,active(X2),X3) -> U21(X1,X2,X3)
      U21(X1,X2,active(X3)) -> U21(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)
      U31(mark(X)) -> U31(X)
      U31(active(X)) -> U31(X)
      U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
      U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
      U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
      U41(active(X1),X2,X3) -> U41(X1,X2,X3)
      U41(X1,active(X2),X3) -> U41(X1,X2,X3)
      U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
      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)
      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)
      isNat(mark(X)) -> isNat(X)
      isNat(active(X)) -> isNat(X)
     Open
     
     DPs:
      isNat#(mark(X)) -> isNat#(X)
      isNat#(active(X)) -> isNat#(X)
     TRS:
      active(U11(tt(),N)) -> mark(N)
      active(U21(tt(),M,N)) -> mark(s(plus(N,M)))
      active(U31(tt())) -> mark(0())
      active(U41(tt(),M,N)) -> mark(plus(x(N,M),N))
      active(and(tt(),X)) -> mark(X)
      active(isNat(0())) -> mark(tt())
      active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2)))
      active(isNat(s(V1))) -> mark(isNat(V1))
      active(isNat(x(V1,V2))) -> mark(and(isNat(V1),isNat(V2)))
      active(plus(N,0())) -> mark(U11(isNat(N),N))
      active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N))
      active(x(N,0())) -> mark(U31(isNat(N)))
      active(x(N,s(M))) -> mark(U41(and(isNat(M),isNat(N)),M,N))
      mark(U11(X1,X2)) -> active(U11(mark(X1),X2))
      mark(tt()) -> active(tt())
      mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3))
      mark(s(X)) -> active(s(mark(X)))
      mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
      mark(U31(X)) -> active(U31(mark(X)))
      mark(0()) -> active(0())
      mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
      mark(x(X1,X2)) -> active(x(mark(X1),mark(X2)))
      mark(and(X1,X2)) -> active(and(mark(X1),X2))
      mark(isNat(X)) -> active(isNat(X))
      U11(mark(X1),X2) -> U11(X1,X2)
      U11(X1,mark(X2)) -> U11(X1,X2)
      U11(active(X1),X2) -> U11(X1,X2)
      U11(X1,active(X2)) -> U11(X1,X2)
      U21(mark(X1),X2,X3) -> U21(X1,X2,X3)
      U21(X1,mark(X2),X3) -> U21(X1,X2,X3)
      U21(X1,X2,mark(X3)) -> U21(X1,X2,X3)
      U21(active(X1),X2,X3) -> U21(X1,X2,X3)
      U21(X1,active(X2),X3) -> U21(X1,X2,X3)
      U21(X1,X2,active(X3)) -> U21(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)
      U31(mark(X)) -> U31(X)
      U31(active(X)) -> U31(X)
      U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
      U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
      U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
      U41(active(X1),X2,X3) -> U41(X1,X2,X3)
      U41(X1,active(X2),X3) -> U41(X1,X2,X3)
      U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
      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)
      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)
      isNat(mark(X)) -> isNat(X)
      isNat(active(X)) -> isNat(X)
     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(U11(tt(),N)) -> mark(N)
      active(U21(tt(),M,N)) -> mark(s(plus(N,M)))
      active(U31(tt())) -> mark(0())
      active(U41(tt(),M,N)) -> mark(plus(x(N,M),N))
      active(and(tt(),X)) -> mark(X)
      active(isNat(0())) -> mark(tt())
      active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2)))
      active(isNat(s(V1))) -> mark(isNat(V1))
      active(isNat(x(V1,V2))) -> mark(and(isNat(V1),isNat(V2)))
      active(plus(N,0())) -> mark(U11(isNat(N),N))
      active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N))
      active(x(N,0())) -> mark(U31(isNat(N)))
      active(x(N,s(M))) -> mark(U41(and(isNat(M),isNat(N)),M,N))
      mark(U11(X1,X2)) -> active(U11(mark(X1),X2))
      mark(tt()) -> active(tt())
      mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3))
      mark(s(X)) -> active(s(mark(X)))
      mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
      mark(U31(X)) -> active(U31(mark(X)))
      mark(0()) -> active(0())
      mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
      mark(x(X1,X2)) -> active(x(mark(X1),mark(X2)))
      mark(and(X1,X2)) -> active(and(mark(X1),X2))
      mark(isNat(X)) -> active(isNat(X))
      U11(mark(X1),X2) -> U11(X1,X2)
      U11(X1,mark(X2)) -> U11(X1,X2)
      U11(active(X1),X2) -> U11(X1,X2)
      U11(X1,active(X2)) -> U11(X1,X2)
      U21(mark(X1),X2,X3) -> U21(X1,X2,X3)
      U21(X1,mark(X2),X3) -> U21(X1,X2,X3)
      U21(X1,X2,mark(X3)) -> U21(X1,X2,X3)
      U21(active(X1),X2,X3) -> U21(X1,X2,X3)
      U21(X1,active(X2),X3) -> U21(X1,X2,X3)
      U21(X1,X2,active(X3)) -> U21(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)
      U31(mark(X)) -> U31(X)
      U31(active(X)) -> U31(X)
      U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
      U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
      U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
      U41(active(X1),X2,X3) -> U41(X1,X2,X3)
      U41(X1,active(X2),X3) -> U41(X1,X2,X3)
      U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
      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)
      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)
      isNat(mark(X)) -> isNat(X)
      isNat(active(X)) -> isNat(X)
     Open
     
     DPs:
      U11#(mark(X1),X2) -> U11#(X1,X2)
      U11#(X1,active(X2)) -> U11#(X1,X2)
      U11#(active(X1),X2) -> U11#(X1,X2)
      U11#(X1,mark(X2)) -> U11#(X1,X2)
     TRS:
      active(U11(tt(),N)) -> mark(N)
      active(U21(tt(),M,N)) -> mark(s(plus(N,M)))
      active(U31(tt())) -> mark(0())
      active(U41(tt(),M,N)) -> mark(plus(x(N,M),N))
      active(and(tt(),X)) -> mark(X)
      active(isNat(0())) -> mark(tt())
      active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2)))
      active(isNat(s(V1))) -> mark(isNat(V1))
      active(isNat(x(V1,V2))) -> mark(and(isNat(V1),isNat(V2)))
      active(plus(N,0())) -> mark(U11(isNat(N),N))
      active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N))
      active(x(N,0())) -> mark(U31(isNat(N)))
      active(x(N,s(M))) -> mark(U41(and(isNat(M),isNat(N)),M,N))
      mark(U11(X1,X2)) -> active(U11(mark(X1),X2))
      mark(tt()) -> active(tt())
      mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3))
      mark(s(X)) -> active(s(mark(X)))
      mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
      mark(U31(X)) -> active(U31(mark(X)))
      mark(0()) -> active(0())
      mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
      mark(x(X1,X2)) -> active(x(mark(X1),mark(X2)))
      mark(and(X1,X2)) -> active(and(mark(X1),X2))
      mark(isNat(X)) -> active(isNat(X))
      U11(mark(X1),X2) -> U11(X1,X2)
      U11(X1,mark(X2)) -> U11(X1,X2)
      U11(active(X1),X2) -> U11(X1,X2)
      U11(X1,active(X2)) -> U11(X1,X2)
      U21(mark(X1),X2,X3) -> U21(X1,X2,X3)
      U21(X1,mark(X2),X3) -> U21(X1,X2,X3)
      U21(X1,X2,mark(X3)) -> U21(X1,X2,X3)
      U21(active(X1),X2,X3) -> U21(X1,X2,X3)
      U21(X1,active(X2),X3) -> U21(X1,X2,X3)
      U21(X1,X2,active(X3)) -> U21(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)
      U31(mark(X)) -> U31(X)
      U31(active(X)) -> U31(X)
      U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
      U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
      U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
      U41(active(X1),X2,X3) -> U41(X1,X2,X3)
      U41(X1,active(X2),X3) -> U41(X1,X2,X3)
      U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
      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)
      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)
      isNat(mark(X)) -> isNat(X)
      isNat(active(X)) -> isNat(X)
     Open
     
     DPs:
      U21#(mark(X1),X2,X3) -> U21#(X1,X2,X3)
      U21#(X1,X2,active(X3)) -> U21#(X1,X2,X3)
      U21#(X1,active(X2),X3) -> U21#(X1,X2,X3)
      U21#(active(X1),X2,X3) -> U21#(X1,X2,X3)
      U21#(X1,X2,mark(X3)) -> U21#(X1,X2,X3)
      U21#(X1,mark(X2),X3) -> U21#(X1,X2,X3)
     TRS:
      active(U11(tt(),N)) -> mark(N)
      active(U21(tt(),M,N)) -> mark(s(plus(N,M)))
      active(U31(tt())) -> mark(0())
      active(U41(tt(),M,N)) -> mark(plus(x(N,M),N))
      active(and(tt(),X)) -> mark(X)
      active(isNat(0())) -> mark(tt())
      active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2)))
      active(isNat(s(V1))) -> mark(isNat(V1))
      active(isNat(x(V1,V2))) -> mark(and(isNat(V1),isNat(V2)))
      active(plus(N,0())) -> mark(U11(isNat(N),N))
      active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N))
      active(x(N,0())) -> mark(U31(isNat(N)))
      active(x(N,s(M))) -> mark(U41(and(isNat(M),isNat(N)),M,N))
      mark(U11(X1,X2)) -> active(U11(mark(X1),X2))
      mark(tt()) -> active(tt())
      mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3))
      mark(s(X)) -> active(s(mark(X)))
      mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
      mark(U31(X)) -> active(U31(mark(X)))
      mark(0()) -> active(0())
      mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
      mark(x(X1,X2)) -> active(x(mark(X1),mark(X2)))
      mark(and(X1,X2)) -> active(and(mark(X1),X2))
      mark(isNat(X)) -> active(isNat(X))
      U11(mark(X1),X2) -> U11(X1,X2)
      U11(X1,mark(X2)) -> U11(X1,X2)
      U11(active(X1),X2) -> U11(X1,X2)
      U11(X1,active(X2)) -> U11(X1,X2)
      U21(mark(X1),X2,X3) -> U21(X1,X2,X3)
      U21(X1,mark(X2),X3) -> U21(X1,X2,X3)
      U21(X1,X2,mark(X3)) -> U21(X1,X2,X3)
      U21(active(X1),X2,X3) -> U21(X1,X2,X3)
      U21(X1,active(X2),X3) -> U21(X1,X2,X3)
      U21(X1,X2,active(X3)) -> U21(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)
      U31(mark(X)) -> U31(X)
      U31(active(X)) -> U31(X)
      U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
      U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
      U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
      U41(active(X1),X2,X3) -> U41(X1,X2,X3)
      U41(X1,active(X2),X3) -> U41(X1,X2,X3)
      U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
      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)
      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)
      isNat(mark(X)) -> isNat(X)
      isNat(active(X)) -> isNat(X)
     Open
     
     DPs:
      U31#(mark(X)) -> U31#(X)
      U31#(active(X)) -> U31#(X)
     TRS:
      active(U11(tt(),N)) -> mark(N)
      active(U21(tt(),M,N)) -> mark(s(plus(N,M)))
      active(U31(tt())) -> mark(0())
      active(U41(tt(),M,N)) -> mark(plus(x(N,M),N))
      active(and(tt(),X)) -> mark(X)
      active(isNat(0())) -> mark(tt())
      active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2)))
      active(isNat(s(V1))) -> mark(isNat(V1))
      active(isNat(x(V1,V2))) -> mark(and(isNat(V1),isNat(V2)))
      active(plus(N,0())) -> mark(U11(isNat(N),N))
      active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N))
      active(x(N,0())) -> mark(U31(isNat(N)))
      active(x(N,s(M))) -> mark(U41(and(isNat(M),isNat(N)),M,N))
      mark(U11(X1,X2)) -> active(U11(mark(X1),X2))
      mark(tt()) -> active(tt())
      mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3))
      mark(s(X)) -> active(s(mark(X)))
      mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
      mark(U31(X)) -> active(U31(mark(X)))
      mark(0()) -> active(0())
      mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
      mark(x(X1,X2)) -> active(x(mark(X1),mark(X2)))
      mark(and(X1,X2)) -> active(and(mark(X1),X2))
      mark(isNat(X)) -> active(isNat(X))
      U11(mark(X1),X2) -> U11(X1,X2)
      U11(X1,mark(X2)) -> U11(X1,X2)
      U11(active(X1),X2) -> U11(X1,X2)
      U11(X1,active(X2)) -> U11(X1,X2)
      U21(mark(X1),X2,X3) -> U21(X1,X2,X3)
      U21(X1,mark(X2),X3) -> U21(X1,X2,X3)
      U21(X1,X2,mark(X3)) -> U21(X1,X2,X3)
      U21(active(X1),X2,X3) -> U21(X1,X2,X3)
      U21(X1,active(X2),X3) -> U21(X1,X2,X3)
      U21(X1,X2,active(X3)) -> U21(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)
      U31(mark(X)) -> U31(X)
      U31(active(X)) -> U31(X)
      U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
      U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
      U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
      U41(active(X1),X2,X3) -> U41(X1,X2,X3)
      U41(X1,active(X2),X3) -> U41(X1,X2,X3)
      U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
      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)
      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)
      isNat(mark(X)) -> isNat(X)
      isNat(active(X)) -> isNat(X)
     Open
     
     DPs:
      U41#(mark(X1),X2,X3) -> U41#(X1,X2,X3)
      U41#(X1,X2,active(X3)) -> U41#(X1,X2,X3)
      U41#(X1,active(X2),X3) -> U41#(X1,X2,X3)
      U41#(active(X1),X2,X3) -> U41#(X1,X2,X3)
      U41#(X1,X2,mark(X3)) -> U41#(X1,X2,X3)
      U41#(X1,mark(X2),X3) -> U41#(X1,X2,X3)
     TRS:
      active(U11(tt(),N)) -> mark(N)
      active(U21(tt(),M,N)) -> mark(s(plus(N,M)))
      active(U31(tt())) -> mark(0())
      active(U41(tt(),M,N)) -> mark(plus(x(N,M),N))
      active(and(tt(),X)) -> mark(X)
      active(isNat(0())) -> mark(tt())
      active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2)))
      active(isNat(s(V1))) -> mark(isNat(V1))
      active(isNat(x(V1,V2))) -> mark(and(isNat(V1),isNat(V2)))
      active(plus(N,0())) -> mark(U11(isNat(N),N))
      active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N))
      active(x(N,0())) -> mark(U31(isNat(N)))
      active(x(N,s(M))) -> mark(U41(and(isNat(M),isNat(N)),M,N))
      mark(U11(X1,X2)) -> active(U11(mark(X1),X2))
      mark(tt()) -> active(tt())
      mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3))
      mark(s(X)) -> active(s(mark(X)))
      mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
      mark(U31(X)) -> active(U31(mark(X)))
      mark(0()) -> active(0())
      mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
      mark(x(X1,X2)) -> active(x(mark(X1),mark(X2)))
      mark(and(X1,X2)) -> active(and(mark(X1),X2))
      mark(isNat(X)) -> active(isNat(X))
      U11(mark(X1),X2) -> U11(X1,X2)
      U11(X1,mark(X2)) -> U11(X1,X2)
      U11(active(X1),X2) -> U11(X1,X2)
      U11(X1,active(X2)) -> U11(X1,X2)
      U21(mark(X1),X2,X3) -> U21(X1,X2,X3)
      U21(X1,mark(X2),X3) -> U21(X1,X2,X3)
      U21(X1,X2,mark(X3)) -> U21(X1,X2,X3)
      U21(active(X1),X2,X3) -> U21(X1,X2,X3)
      U21(X1,active(X2),X3) -> U21(X1,X2,X3)
      U21(X1,X2,active(X3)) -> U21(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)
      U31(mark(X)) -> U31(X)
      U31(active(X)) -> U31(X)
      U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
      U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
      U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
      U41(active(X1),X2,X3) -> U41(X1,X2,X3)
      U41(X1,active(X2),X3) -> U41(X1,X2,X3)
      U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
      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)
      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)
      isNat(mark(X)) -> isNat(X)
      isNat(active(X)) -> isNat(X)
     Open