YES

Problem:
 active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
 active(__(X,nil())) -> mark(X)
 active(__(nil(),X)) -> mark(X)
 active(U11(tt())) -> mark(U12(tt()))
 active(U12(tt())) -> mark(tt())
 active(isNePal(__(I,__(P,I)))) -> mark(U11(tt()))
 mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
 mark(nil()) -> active(nil())
 mark(U11(X)) -> active(U11(mark(X)))
 mark(tt()) -> active(tt())
 mark(U12(X)) -> active(U12(mark(X)))
 mark(isNePal(X)) -> active(isNePal(mark(X)))
 __(mark(X1),X2) -> __(X1,X2)
 __(X1,mark(X2)) -> __(X1,X2)
 __(active(X1),X2) -> __(X1,X2)
 __(X1,active(X2)) -> __(X1,X2)
 U11(mark(X)) -> U11(X)
 U11(active(X)) -> U11(X)
 U12(mark(X)) -> U12(X)
 U12(active(X)) -> U12(X)
 isNePal(mark(X)) -> isNePal(X)
 isNePal(active(X)) -> isNePal(X)

Proof:
 Matrix Interpretation Processor: dim=1
  
  interpretation:
   [isNePal](x0) = x0 + 4,
   
   [U12](x0) = 2x0 + 2,
   
   [U11](x0) = 2x0 + 2,
   
   [tt] = 4,
   
   [nil] = 1,
   
   [mark](x0) = x0,
   
   [active](x0) = x0,
   
   [__](x0, x1) = x0 + x1 + 3
  orientation:
   active(__(__(X,Y),Z)) = X + Y + Z + 6 >= X + Y + Z + 6 = mark(__(X,__(Y,Z)))
   
   active(__(X,nil())) = X + 4 >= X = mark(X)
   
   active(__(nil(),X)) = X + 4 >= X = mark(X)
   
   active(U11(tt())) = 10 >= 10 = mark(U12(tt()))
   
   active(U12(tt())) = 10 >= 4 = mark(tt())
   
   active(isNePal(__(I,__(P,I)))) = 2I + P + 10 >= 10 = mark(U11(tt()))
   
   mark(__(X1,X2)) = X1 + X2 + 3 >= X1 + X2 + 3 = active(__(mark(X1),mark(X2)))
   
   mark(nil()) = 1 >= 1 = active(nil())
   
   mark(U11(X)) = 2X + 2 >= 2X + 2 = active(U11(mark(X)))
   
   mark(tt()) = 4 >= 4 = active(tt())
   
   mark(U12(X)) = 2X + 2 >= 2X + 2 = active(U12(mark(X)))
   
   mark(isNePal(X)) = X + 4 >= X + 4 = active(isNePal(mark(X)))
   
   __(mark(X1),X2) = X1 + X2 + 3 >= X1 + X2 + 3 = __(X1,X2)
   
   __(X1,mark(X2)) = X1 + X2 + 3 >= X1 + X2 + 3 = __(X1,X2)
   
   __(active(X1),X2) = X1 + X2 + 3 >= X1 + X2 + 3 = __(X1,X2)
   
   __(X1,active(X2)) = X1 + X2 + 3 >= X1 + X2 + 3 = __(X1,X2)
   
   U11(mark(X)) = 2X + 2 >= 2X + 2 = U11(X)
   
   U11(active(X)) = 2X + 2 >= 2X + 2 = U11(X)
   
   U12(mark(X)) = 2X + 2 >= 2X + 2 = U12(X)
   
   U12(active(X)) = 2X + 2 >= 2X + 2 = U12(X)
   
   isNePal(mark(X)) = X + 4 >= X + 4 = isNePal(X)
   
   isNePal(active(X)) = X + 4 >= X + 4 = isNePal(X)
  problem:
   active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
   active(U11(tt())) -> mark(U12(tt()))
   active(isNePal(__(I,__(P,I)))) -> mark(U11(tt()))
   mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
   mark(nil()) -> active(nil())
   mark(U11(X)) -> active(U11(mark(X)))
   mark(tt()) -> active(tt())
   mark(U12(X)) -> active(U12(mark(X)))
   mark(isNePal(X)) -> active(isNePal(mark(X)))
   __(mark(X1),X2) -> __(X1,X2)
   __(X1,mark(X2)) -> __(X1,X2)
   __(active(X1),X2) -> __(X1,X2)
   __(X1,active(X2)) -> __(X1,X2)
   U11(mark(X)) -> U11(X)
   U11(active(X)) -> U11(X)
   U12(mark(X)) -> U12(X)
   U12(active(X)) -> U12(X)
   isNePal(mark(X)) -> isNePal(X)
   isNePal(active(X)) -> isNePal(X)
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [isNePal](x0) = x0 + 2,
    
    [U12](x0) = x0,
    
    [U11](x0) = x0 + 3,
    
    [tt] = 4,
    
    [nil] = 2,
    
    [mark](x0) = x0,
    
    [active](x0) = x0,
    
    [__](x0, x1) = x0 + x1 + 3
   orientation:
    active(__(__(X,Y),Z)) = X + Y + Z + 6 >= X + Y + Z + 6 = mark(__(X,__(Y,Z)))
    
    active(U11(tt())) = 7 >= 4 = mark(U12(tt()))
    
    active(isNePal(__(I,__(P,I)))) = 2I + P + 8 >= 7 = mark(U11(tt()))
    
    mark(__(X1,X2)) = X1 + X2 + 3 >= X1 + X2 + 3 = active(__(mark(X1),mark(X2)))
    
    mark(nil()) = 2 >= 2 = active(nil())
    
    mark(U11(X)) = X + 3 >= X + 3 = active(U11(mark(X)))
    
    mark(tt()) = 4 >= 4 = active(tt())
    
    mark(U12(X)) = X >= X = active(U12(mark(X)))
    
    mark(isNePal(X)) = X + 2 >= X + 2 = active(isNePal(mark(X)))
    
    __(mark(X1),X2) = X1 + X2 + 3 >= X1 + X2 + 3 = __(X1,X2)
    
    __(X1,mark(X2)) = X1 + X2 + 3 >= X1 + X2 + 3 = __(X1,X2)
    
    __(active(X1),X2) = X1 + X2 + 3 >= X1 + X2 + 3 = __(X1,X2)
    
    __(X1,active(X2)) = X1 + X2 + 3 >= X1 + X2 + 3 = __(X1,X2)
    
    U11(mark(X)) = X + 3 >= X + 3 = U11(X)
    
    U11(active(X)) = X + 3 >= X + 3 = U11(X)
    
    U12(mark(X)) = X >= X = U12(X)
    
    U12(active(X)) = X >= X = U12(X)
    
    isNePal(mark(X)) = X + 2 >= X + 2 = isNePal(X)
    
    isNePal(active(X)) = X + 2 >= X + 2 = isNePal(X)
   problem:
    active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
    mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
    mark(nil()) -> active(nil())
    mark(U11(X)) -> active(U11(mark(X)))
    mark(tt()) -> active(tt())
    mark(U12(X)) -> active(U12(mark(X)))
    mark(isNePal(X)) -> active(isNePal(mark(X)))
    __(mark(X1),X2) -> __(X1,X2)
    __(X1,mark(X2)) -> __(X1,X2)
    __(active(X1),X2) -> __(X1,X2)
    __(X1,active(X2)) -> __(X1,X2)
    U11(mark(X)) -> U11(X)
    U11(active(X)) -> U11(X)
    U12(mark(X)) -> U12(X)
    U12(active(X)) -> U12(X)
    isNePal(mark(X)) -> isNePal(X)
    isNePal(active(X)) -> isNePal(X)
   DP Processor:
    DPs:
     active#(__(__(X,Y),Z)) -> __#(Y,Z)
     active#(__(__(X,Y),Z)) -> __#(X,__(Y,Z))
     active#(__(__(X,Y),Z)) -> mark#(__(X,__(Y,Z)))
     mark#(__(X1,X2)) -> mark#(X2)
     mark#(__(X1,X2)) -> mark#(X1)
     mark#(__(X1,X2)) -> __#(mark(X1),mark(X2))
     mark#(__(X1,X2)) -> active#(__(mark(X1),mark(X2)))
     mark#(nil()) -> active#(nil())
     mark#(U11(X)) -> mark#(X)
     mark#(U11(X)) -> U11#(mark(X))
     mark#(U11(X)) -> active#(U11(mark(X)))
     mark#(tt()) -> active#(tt())
     mark#(U12(X)) -> mark#(X)
     mark#(U12(X)) -> U12#(mark(X))
     mark#(U12(X)) -> active#(U12(mark(X)))
     mark#(isNePal(X)) -> mark#(X)
     mark#(isNePal(X)) -> isNePal#(mark(X))
     mark#(isNePal(X)) -> active#(isNePal(mark(X)))
     __#(mark(X1),X2) -> __#(X1,X2)
     __#(X1,mark(X2)) -> __#(X1,X2)
     __#(active(X1),X2) -> __#(X1,X2)
     __#(X1,active(X2)) -> __#(X1,X2)
     U11#(mark(X)) -> U11#(X)
     U11#(active(X)) -> U11#(X)
     U12#(mark(X)) -> U12#(X)
     U12#(active(X)) -> U12#(X)
     isNePal#(mark(X)) -> isNePal#(X)
     isNePal#(active(X)) -> isNePal#(X)
    TRS:
     active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
     mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
     mark(nil()) -> active(nil())
     mark(U11(X)) -> active(U11(mark(X)))
     mark(tt()) -> active(tt())
     mark(U12(X)) -> active(U12(mark(X)))
     mark(isNePal(X)) -> active(isNePal(mark(X)))
     __(mark(X1),X2) -> __(X1,X2)
     __(X1,mark(X2)) -> __(X1,X2)
     __(active(X1),X2) -> __(X1,X2)
     __(X1,active(X2)) -> __(X1,X2)
     U11(mark(X)) -> U11(X)
     U11(active(X)) -> U11(X)
     U12(mark(X)) -> U12(X)
     U12(active(X)) -> U12(X)
     isNePal(mark(X)) -> isNePal(X)
     isNePal(active(X)) -> isNePal(X)
    TDG Processor:
     DPs:
      active#(__(__(X,Y),Z)) -> __#(Y,Z)
      active#(__(__(X,Y),Z)) -> __#(X,__(Y,Z))
      active#(__(__(X,Y),Z)) -> mark#(__(X,__(Y,Z)))
      mark#(__(X1,X2)) -> mark#(X2)
      mark#(__(X1,X2)) -> mark#(X1)
      mark#(__(X1,X2)) -> __#(mark(X1),mark(X2))
      mark#(__(X1,X2)) -> active#(__(mark(X1),mark(X2)))
      mark#(nil()) -> active#(nil())
      mark#(U11(X)) -> mark#(X)
      mark#(U11(X)) -> U11#(mark(X))
      mark#(U11(X)) -> active#(U11(mark(X)))
      mark#(tt()) -> active#(tt())
      mark#(U12(X)) -> mark#(X)
      mark#(U12(X)) -> U12#(mark(X))
      mark#(U12(X)) -> active#(U12(mark(X)))
      mark#(isNePal(X)) -> mark#(X)
      mark#(isNePal(X)) -> isNePal#(mark(X))
      mark#(isNePal(X)) -> active#(isNePal(mark(X)))
      __#(mark(X1),X2) -> __#(X1,X2)
      __#(X1,mark(X2)) -> __#(X1,X2)
      __#(active(X1),X2) -> __#(X1,X2)
      __#(X1,active(X2)) -> __#(X1,X2)
      U11#(mark(X)) -> U11#(X)
      U11#(active(X)) -> U11#(X)
      U12#(mark(X)) -> U12#(X)
      U12#(active(X)) -> U12#(X)
      isNePal#(mark(X)) -> isNePal#(X)
      isNePal#(active(X)) -> isNePal#(X)
     TRS:
      active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
      mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
      mark(nil()) -> active(nil())
      mark(U11(X)) -> active(U11(mark(X)))
      mark(tt()) -> active(tt())
      mark(U12(X)) -> active(U12(mark(X)))
      mark(isNePal(X)) -> active(isNePal(mark(X)))
      __(mark(X1),X2) -> __(X1,X2)
      __(X1,mark(X2)) -> __(X1,X2)
      __(active(X1),X2) -> __(X1,X2)
      __(X1,active(X2)) -> __(X1,X2)
      U11(mark(X)) -> U11(X)
      U11(active(X)) -> U11(X)
      U12(mark(X)) -> U12(X)
      U12(active(X)) -> U12(X)
      isNePal(mark(X)) -> isNePal(X)
      isNePal(active(X)) -> isNePal(X)
     graph:
      isNePal#(mark(X)) -> isNePal#(X) ->
      isNePal#(active(X)) -> isNePal#(X)
      isNePal#(mark(X)) -> isNePal#(X) ->
      isNePal#(mark(X)) -> isNePal#(X)
      isNePal#(active(X)) -> isNePal#(X) ->
      isNePal#(active(X)) -> isNePal#(X)
      isNePal#(active(X)) -> isNePal#(X) ->
      isNePal#(mark(X)) -> isNePal#(X)
      U12#(mark(X)) -> U12#(X) -> U12#(active(X)) -> U12#(X)
      U12#(mark(X)) -> U12#(X) -> U12#(mark(X)) -> U12#(X)
      U12#(active(X)) -> U12#(X) -> U12#(active(X)) -> U12#(X)
      U12#(active(X)) -> U12#(X) -> U12#(mark(X)) -> U12#(X)
      U11#(mark(X)) -> U11#(X) -> U11#(active(X)) -> U11#(X)
      U11#(mark(X)) -> U11#(X) -> U11#(mark(X)) -> U11#(X)
      U11#(active(X)) -> U11#(X) -> U11#(active(X)) -> U11#(X)
      U11#(active(X)) -> U11#(X) -> U11#(mark(X)) -> U11#(X)
      mark#(isNePal(X)) -> isNePal#(mark(X)) ->
      isNePal#(active(X)) -> isNePal#(X)
      mark#(isNePal(X)) -> isNePal#(mark(X)) ->
      isNePal#(mark(X)) -> isNePal#(X)
      mark#(isNePal(X)) -> mark#(X) ->
      mark#(isNePal(X)) -> active#(isNePal(mark(X)))
      mark#(isNePal(X)) -> mark#(X) ->
      mark#(isNePal(X)) -> isNePal#(mark(X))
      mark#(isNePal(X)) -> mark#(X) -> mark#(isNePal(X)) -> mark#(X)
      mark#(isNePal(X)) -> mark#(X) ->
      mark#(U12(X)) -> active#(U12(mark(X)))
      mark#(isNePal(X)) -> mark#(X) -> mark#(U12(X)) -> U12#(mark(X))
      mark#(isNePal(X)) -> mark#(X) -> mark#(U12(X)) -> mark#(X)
      mark#(isNePal(X)) -> mark#(X) -> mark#(tt()) -> active#(tt())
      mark#(isNePal(X)) -> mark#(X) ->
      mark#(U11(X)) -> active#(U11(mark(X)))
      mark#(isNePal(X)) -> mark#(X) -> mark#(U11(X)) -> U11#(mark(X))
      mark#(isNePal(X)) -> mark#(X) -> mark#(U11(X)) -> mark#(X)
      mark#(isNePal(X)) -> mark#(X) -> mark#(nil()) -> active#(nil())
      mark#(isNePal(X)) -> mark#(X) ->
      mark#(__(X1,X2)) -> active#(__(mark(X1),mark(X2)))
      mark#(isNePal(X)) -> mark#(X) ->
      mark#(__(X1,X2)) -> __#(mark(X1),mark(X2))
      mark#(isNePal(X)) -> mark#(X) -> mark#(__(X1,X2)) -> mark#(X1)
      mark#(isNePal(X)) -> mark#(X) ->
      mark#(__(X1,X2)) -> mark#(X2)
      mark#(isNePal(X)) -> active#(isNePal(mark(X))) ->
      active#(__(__(X,Y),Z)) -> mark#(__(X,__(Y,Z)))
      mark#(isNePal(X)) -> active#(isNePal(mark(X))) ->
      active#(__(__(X,Y),Z)) -> __#(X,__(Y,Z))
      mark#(isNePal(X)) -> active#(isNePal(mark(X))) ->
      active#(__(__(X,Y),Z)) -> __#(Y,Z)
      mark#(U12(X)) -> U12#(mark(X)) -> U12#(active(X)) -> U12#(X)
      mark#(U12(X)) -> U12#(mark(X)) -> U12#(mark(X)) -> U12#(X)
      mark#(U12(X)) -> mark#(X) ->
      mark#(isNePal(X)) -> active#(isNePal(mark(X)))
      mark#(U12(X)) -> mark#(X) -> mark#(isNePal(X)) -> isNePal#(mark(X))
      mark#(U12(X)) -> mark#(X) -> mark#(isNePal(X)) -> mark#(X)
      mark#(U12(X)) -> mark#(X) -> mark#(U12(X)) -> active#(U12(mark(X)))
      mark#(U12(X)) -> mark#(X) -> mark#(U12(X)) -> U12#(mark(X))
      mark#(U12(X)) -> mark#(X) -> mark#(U12(X)) -> mark#(X)
      mark#(U12(X)) -> mark#(X) -> mark#(tt()) -> active#(tt())
      mark#(U12(X)) -> mark#(X) -> mark#(U11(X)) -> active#(U11(mark(X)))
      mark#(U12(X)) -> mark#(X) -> mark#(U11(X)) -> U11#(mark(X))
      mark#(U12(X)) -> mark#(X) -> mark#(U11(X)) -> mark#(X)
      mark#(U12(X)) -> mark#(X) -> mark#(nil()) -> active#(nil())
      mark#(U12(X)) -> mark#(X) ->
      mark#(__(X1,X2)) -> active#(__(mark(X1),mark(X2)))
      mark#(U12(X)) -> mark#(X) ->
      mark#(__(X1,X2)) -> __#(mark(X1),mark(X2))
      mark#(U12(X)) -> mark#(X) -> mark#(__(X1,X2)) -> mark#(X1)
      mark#(U12(X)) -> mark#(X) ->
      mark#(__(X1,X2)) -> mark#(X2)
      mark#(U12(X)) -> active#(U12(mark(X))) ->
      active#(__(__(X,Y),Z)) -> mark#(__(X,__(Y,Z)))
      mark#(U12(X)) -> active#(U12(mark(X))) ->
      active#(__(__(X,Y),Z)) -> __#(X,__(Y,Z))
      mark#(U12(X)) -> active#(U12(mark(X))) ->
      active#(__(__(X,Y),Z)) -> __#(Y,Z)
      mark#(U11(X)) -> U11#(mark(X)) -> U11#(active(X)) -> U11#(X)
      mark#(U11(X)) -> U11#(mark(X)) -> U11#(mark(X)) -> U11#(X)
      mark#(U11(X)) -> mark#(X) ->
      mark#(isNePal(X)) -> active#(isNePal(mark(X)))
      mark#(U11(X)) -> mark#(X) -> mark#(isNePal(X)) -> isNePal#(mark(X))
      mark#(U11(X)) -> mark#(X) -> mark#(isNePal(X)) -> mark#(X)
      mark#(U11(X)) -> mark#(X) -> mark#(U12(X)) -> active#(U12(mark(X)))
      mark#(U11(X)) -> mark#(X) -> mark#(U12(X)) -> U12#(mark(X))
      mark#(U11(X)) -> mark#(X) -> mark#(U12(X)) -> mark#(X)
      mark#(U11(X)) -> mark#(X) -> mark#(tt()) -> active#(tt())
      mark#(U11(X)) -> mark#(X) -> mark#(U11(X)) -> active#(U11(mark(X)))
      mark#(U11(X)) -> mark#(X) -> mark#(U11(X)) -> U11#(mark(X))
      mark#(U11(X)) -> mark#(X) -> mark#(U11(X)) -> mark#(X)
      mark#(U11(X)) -> mark#(X) -> mark#(nil()) -> active#(nil())
      mark#(U11(X)) -> mark#(X) ->
      mark#(__(X1,X2)) -> active#(__(mark(X1),mark(X2)))
      mark#(U11(X)) -> mark#(X) ->
      mark#(__(X1,X2)) -> __#(mark(X1),mark(X2))
      mark#(U11(X)) -> mark#(X) -> mark#(__(X1,X2)) -> mark#(X1)
      mark#(U11(X)) -> mark#(X) ->
      mark#(__(X1,X2)) -> mark#(X2)
      mark#(U11(X)) -> active#(U11(mark(X))) ->
      active#(__(__(X,Y),Z)) -> mark#(__(X,__(Y,Z)))
      mark#(U11(X)) -> active#(U11(mark(X))) ->
      active#(__(__(X,Y),Z)) -> __#(X,__(Y,Z))
      mark#(U11(X)) -> active#(U11(mark(X))) ->
      active#(__(__(X,Y),Z)) -> __#(Y,Z)
      mark#(tt()) -> active#(tt()) ->
      active#(__(__(X,Y),Z)) -> mark#(__(X,__(Y,Z)))
      mark#(tt()) -> active#(tt()) ->
      active#(__(__(X,Y),Z)) -> __#(X,__(Y,Z))
      mark#(tt()) -> active#(tt()) ->
      active#(__(__(X,Y),Z)) -> __#(Y,Z)
      mark#(nil()) -> active#(nil()) ->
      active#(__(__(X,Y),Z)) -> mark#(__(X,__(Y,Z)))
      mark#(nil()) -> active#(nil()) ->
      active#(__(__(X,Y),Z)) -> __#(X,__(Y,Z))
      mark#(nil()) -> active#(nil()) ->
      active#(__(__(X,Y),Z)) -> __#(Y,Z)
      mark#(__(X1,X2)) -> mark#(X2) ->
      mark#(isNePal(X)) -> active#(isNePal(mark(X)))
      mark#(__(X1,X2)) -> mark#(X2) ->
      mark#(isNePal(X)) -> isNePal#(mark(X))
      mark#(__(X1,X2)) -> mark#(X2) -> mark#(isNePal(X)) -> mark#(X)
      mark#(__(X1,X2)) -> mark#(X2) ->
      mark#(U12(X)) -> active#(U12(mark(X)))
      mark#(__(X1,X2)) -> mark#(X2) -> mark#(U12(X)) -> U12#(mark(X))
      mark#(__(X1,X2)) -> mark#(X2) -> mark#(U12(X)) -> mark#(X)
      mark#(__(X1,X2)) -> mark#(X2) -> mark#(tt()) -> active#(tt())
      mark#(__(X1,X2)) -> mark#(X2) ->
      mark#(U11(X)) -> active#(U11(mark(X)))
      mark#(__(X1,X2)) -> mark#(X2) -> mark#(U11(X)) -> U11#(mark(X))
      mark#(__(X1,X2)) -> mark#(X2) -> mark#(U11(X)) -> mark#(X)
      mark#(__(X1,X2)) -> mark#(X2) -> mark#(nil()) -> active#(nil())
      mark#(__(X1,X2)) -> mark#(X2) ->
      mark#(__(X1,X2)) -> active#(__(mark(X1),mark(X2)))
      mark#(__(X1,X2)) -> mark#(X2) ->
      mark#(__(X1,X2)) -> __#(mark(X1),mark(X2))
      mark#(__(X1,X2)) -> mark#(X2) -> mark#(__(X1,X2)) -> mark#(X1)
      mark#(__(X1,X2)) -> mark#(X2) -> mark#(__(X1,X2)) -> mark#(X2)
      mark#(__(X1,X2)) -> mark#(X1) ->
      mark#(isNePal(X)) -> active#(isNePal(mark(X)))
      mark#(__(X1,X2)) -> mark#(X1) ->
      mark#(isNePal(X)) -> isNePal#(mark(X))
      mark#(__(X1,X2)) -> mark#(X1) -> mark#(isNePal(X)) -> mark#(X)
      mark#(__(X1,X2)) -> mark#(X1) ->
      mark#(U12(X)) -> active#(U12(mark(X)))
      mark#(__(X1,X2)) -> mark#(X1) -> mark#(U12(X)) -> U12#(mark(X))
      mark#(__(X1,X2)) -> mark#(X1) -> mark#(U12(X)) -> mark#(X)
      mark#(__(X1,X2)) -> mark#(X1) -> mark#(tt()) -> active#(tt())
      mark#(__(X1,X2)) -> mark#(X1) ->
      mark#(U11(X)) -> active#(U11(mark(X)))
      mark#(__(X1,X2)) -> mark#(X1) -> mark#(U11(X)) -> U11#(mark(X))
      mark#(__(X1,X2)) -> mark#(X1) -> mark#(U11(X)) -> mark#(X)
      mark#(__(X1,X2)) -> mark#(X1) -> mark#(nil()) -> active#(nil())
      mark#(__(X1,X2)) -> mark#(X1) ->
      mark#(__(X1,X2)) -> active#(__(mark(X1),mark(X2)))
      mark#(__(X1,X2)) -> mark#(X1) ->
      mark#(__(X1,X2)) -> __#(mark(X1),mark(X2))
      mark#(__(X1,X2)) -> mark#(X1) -> mark#(__(X1,X2)) -> mark#(X1)
      mark#(__(X1,X2)) -> mark#(X1) ->
      mark#(__(X1,X2)) -> mark#(X2)
      mark#(__(X1,X2)) -> __#(mark(X1),mark(X2)) ->
      __#(X1,active(X2)) -> __#(X1,X2)
      mark#(__(X1,X2)) -> __#(mark(X1),mark(X2)) ->
      __#(active(X1),X2) -> __#(X1,X2)
      mark#(__(X1,X2)) -> __#(mark(X1),mark(X2)) ->
      __#(X1,mark(X2)) -> __#(X1,X2)
      mark#(__(X1,X2)) -> __#(mark(X1),mark(X2)) ->
      __#(mark(X1),X2) -> __#(X1,X2)
      mark#(__(X1,X2)) -> active#(__(mark(X1),mark(X2))) ->
      active#(__(__(X,Y),Z)) -> mark#(__(X,__(Y,Z)))
      mark#(__(X1,X2)) -> active#(__(mark(X1),mark(X2))) ->
      active#(__(__(X,Y),Z)) -> __#(X,__(Y,Z))
      mark#(__(X1,X2)) -> active#(__(mark(X1),mark(X2))) ->
      active#(__(__(X,Y),Z)) -> __#(Y,Z)
      __#(mark(X1),X2) -> __#(X1,X2) ->
      __#(X1,active(X2)) -> __#(X1,X2)
      __#(mark(X1),X2) -> __#(X1,X2) ->
      __#(active(X1),X2) -> __#(X1,X2)
      __#(mark(X1),X2) -> __#(X1,X2) ->
      __#(X1,mark(X2)) -> __#(X1,X2)
      __#(mark(X1),X2) -> __#(X1,X2) ->
      __#(mark(X1),X2) -> __#(X1,X2)
      __#(active(X1),X2) -> __#(X1,X2) ->
      __#(X1,active(X2)) -> __#(X1,X2)
      __#(active(X1),X2) -> __#(X1,X2) ->
      __#(active(X1),X2) -> __#(X1,X2)
      __#(active(X1),X2) -> __#(X1,X2) ->
      __#(X1,mark(X2)) -> __#(X1,X2)
      __#(active(X1),X2) -> __#(X1,X2) ->
      __#(mark(X1),X2) -> __#(X1,X2)
      __#(X1,mark(X2)) -> __#(X1,X2) ->
      __#(X1,active(X2)) -> __#(X1,X2)
      __#(X1,mark(X2)) -> __#(X1,X2) ->
      __#(active(X1),X2) -> __#(X1,X2)
      __#(X1,mark(X2)) -> __#(X1,X2) ->
      __#(X1,mark(X2)) -> __#(X1,X2)
      __#(X1,mark(X2)) -> __#(X1,X2) ->
      __#(mark(X1),X2) -> __#(X1,X2)
      __#(X1,active(X2)) -> __#(X1,X2) ->
      __#(X1,active(X2)) -> __#(X1,X2)
      __#(X1,active(X2)) -> __#(X1,X2) ->
      __#(active(X1),X2) -> __#(X1,X2)
      __#(X1,active(X2)) -> __#(X1,X2) ->
      __#(X1,mark(X2)) -> __#(X1,X2)
      __#(X1,active(X2)) -> __#(X1,X2) ->
      __#(mark(X1),X2) -> __#(X1,X2)
      active#(__(__(X,Y),Z)) -> mark#(__(X,__(Y,Z))) ->
      mark#(isNePal(X)) -> active#(isNePal(mark(X)))
      active#(__(__(X,Y),Z)) -> mark#(__(X,__(Y,Z))) ->
      mark#(isNePal(X)) -> isNePal#(mark(X))
      active#(__(__(X,Y),Z)) -> mark#(__(X,__(Y,Z))) ->
      mark#(isNePal(X)) -> mark#(X)
      active#(__(__(X,Y),Z)) -> mark#(__(X,__(Y,Z))) ->
      mark#(U12(X)) -> active#(U12(mark(X)))
      active#(__(__(X,Y),Z)) -> mark#(__(X,__(Y,Z))) ->
      mark#(U12(X)) -> U12#(mark(X))
      active#(__(__(X,Y),Z)) -> mark#(__(X,__(Y,Z))) ->
      mark#(U12(X)) -> mark#(X)
      active#(__(__(X,Y),Z)) -> mark#(__(X,__(Y,Z))) ->
      mark#(tt()) -> active#(tt())
      active#(__(__(X,Y),Z)) -> mark#(__(X,__(Y,Z))) ->
      mark#(U11(X)) -> active#(U11(mark(X)))
      active#(__(__(X,Y),Z)) -> mark#(__(X,__(Y,Z))) ->
      mark#(U11(X)) -> U11#(mark(X))
      active#(__(__(X,Y),Z)) -> mark#(__(X,__(Y,Z))) ->
      mark#(U11(X)) -> mark#(X)
      active#(__(__(X,Y),Z)) -> mark#(__(X,__(Y,Z))) ->
      mark#(nil()) -> active#(nil())
      active#(__(__(X,Y),Z)) -> mark#(__(X,__(Y,Z))) ->
      mark#(__(X1,X2)) -> active#(__(mark(X1),mark(X2)))
      active#(__(__(X,Y),Z)) -> mark#(__(X,__(Y,Z))) ->
      mark#(__(X1,X2)) -> __#(mark(X1),mark(X2))
      active#(__(__(X,Y),Z)) -> mark#(__(X,__(Y,Z))) ->
      mark#(__(X1,X2)) -> mark#(X1)
      active#(__(__(X,Y),Z)) -> mark#(__(X,__(Y,Z))) ->
      mark#(__(X1,X2)) -> mark#(X2)
      active#(__(__(X,Y),Z)) -> __#(Y,Z) ->
      __#(X1,active(X2)) -> __#(X1,X2)
      active#(__(__(X,Y),Z)) -> __#(Y,Z) ->
      __#(active(X1),X2) -> __#(X1,X2)
      active#(__(__(X,Y),Z)) -> __#(Y,Z) ->
      __#(X1,mark(X2)) -> __#(X1,X2)
      active#(__(__(X,Y),Z)) -> __#(Y,Z) ->
      __#(mark(X1),X2) -> __#(X1,X2)
      active#(__(__(X,Y),Z)) -> __#(X,__(Y,Z)) ->
      __#(X1,active(X2)) -> __#(X1,X2)
      active#(__(__(X,Y),Z)) -> __#(X,__(Y,Z)) ->
      __#(active(X1),X2) -> __#(X1,X2)
      active#(__(__(X,Y),Z)) -> __#(X,__(Y,Z)) ->
      __#(X1,mark(X2)) -> __#(X1,X2)
      active#(__(__(X,Y),Z)) -> __#(X,__(Y,Z)) -> __#(mark(X1),X2) -> __#(X1,X2)
     SCC Processor:
      #sccs: 5
      #rules: 22
      #arcs: 154/784
      DPs:
       mark#(isNePal(X)) -> mark#(X)
       mark#(__(X1,X2)) -> mark#(X2)
       mark#(__(X1,X2)) -> mark#(X1)
       mark#(__(X1,X2)) -> active#(__(mark(X1),mark(X2)))
       active#(__(__(X,Y),Z)) -> mark#(__(X,__(Y,Z)))
       mark#(nil()) -> active#(nil())
       mark#(U11(X)) -> mark#(X)
       mark#(U11(X)) -> active#(U11(mark(X)))
       mark#(tt()) -> active#(tt())
       mark#(U12(X)) -> mark#(X)
       mark#(U12(X)) -> active#(U12(mark(X)))
       mark#(isNePal(X)) -> active#(isNePal(mark(X)))
      TRS:
       active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
       mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
       mark(nil()) -> active(nil())
       mark(U11(X)) -> active(U11(mark(X)))
       mark(tt()) -> active(tt())
       mark(U12(X)) -> active(U12(mark(X)))
       mark(isNePal(X)) -> active(isNePal(mark(X)))
       __(mark(X1),X2) -> __(X1,X2)
       __(X1,mark(X2)) -> __(X1,X2)
       __(active(X1),X2) -> __(X1,X2)
       __(X1,active(X2)) -> __(X1,X2)
       U11(mark(X)) -> U11(X)
       U11(active(X)) -> U11(X)
       U12(mark(X)) -> U12(X)
       U12(active(X)) -> U12(X)
       isNePal(mark(X)) -> isNePal(X)
       isNePal(active(X)) -> isNePal(X)
      EDG Processor:
       DPs:
        mark#(isNePal(X)) -> mark#(X)
        mark#(__(X1,X2)) -> mark#(X2)
        mark#(__(X1,X2)) -> mark#(X1)
        mark#(__(X1,X2)) -> active#(__(mark(X1),mark(X2)))
        active#(__(__(X,Y),Z)) -> mark#(__(X,__(Y,Z)))
        mark#(nil()) -> active#(nil())
        mark#(U11(X)) -> mark#(X)
        mark#(U11(X)) -> active#(U11(mark(X)))
        mark#(tt()) -> active#(tt())
        mark#(U12(X)) -> mark#(X)
        mark#(U12(X)) -> active#(U12(mark(X)))
        mark#(isNePal(X)) -> active#(isNePal(mark(X)))
       TRS:
        active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
        mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
        mark(nil()) -> active(nil())
        mark(U11(X)) -> active(U11(mark(X)))
        mark(tt()) -> active(tt())
        mark(U12(X)) -> active(U12(mark(X)))
        mark(isNePal(X)) -> active(isNePal(mark(X)))
        __(mark(X1),X2) -> __(X1,X2)
        __(X1,mark(X2)) -> __(X1,X2)
        __(active(X1),X2) -> __(X1,X2)
        __(X1,active(X2)) -> __(X1,X2)
        U11(mark(X)) -> U11(X)
        U11(active(X)) -> U11(X)
        U12(mark(X)) -> U12(X)
        U12(active(X)) -> U12(X)
        isNePal(mark(X)) -> isNePal(X)
        isNePal(active(X)) -> isNePal(X)
       graph:
        mark#(isNePal(X)) -> mark#(X) -> mark#(__(X1,X2)) -> mark#(X2)
        mark#(isNePal(X)) -> mark#(X) -> mark#(__(X1,X2)) -> mark#(X1)
        mark#(isNePal(X)) -> mark#(X) ->
        mark#(__(X1,X2)) -> active#(__(mark(X1),mark(X2)))
        mark#(isNePal(X)) -> mark#(X) ->
        mark#(nil()) -> active#(nil())
        mark#(isNePal(X)) -> mark#(X) -> mark#(U11(X)) -> mark#(X)
        mark#(isNePal(X)) -> mark#(X) ->
        mark#(U11(X)) -> active#(U11(mark(X)))
        mark#(isNePal(X)) -> mark#(X) -> mark#(tt()) -> active#(tt())
        mark#(isNePal(X)) -> mark#(X) -> mark#(U12(X)) -> mark#(X)
        mark#(isNePal(X)) -> mark#(X) ->
        mark#(U12(X)) -> active#(U12(mark(X)))
        mark#(isNePal(X)) -> mark#(X) -> mark#(isNePal(X)) -> mark#(X)
        mark#(isNePal(X)) -> mark#(X) ->
        mark#(isNePal(X)) -> active#(isNePal(mark(X)))
        mark#(isNePal(X)) -> active#(isNePal(mark(X))) ->
        active#(__(__(X,Y),Z)) -> mark#(__(X,__(Y,Z)))
        mark#(U12(X)) -> mark#(X) -> mark#(__(X1,X2)) -> mark#(X2)
        mark#(U12(X)) -> mark#(X) -> mark#(__(X1,X2)) -> mark#(X1)
        mark#(U12(X)) -> mark#(X) ->
        mark#(__(X1,X2)) -> active#(__(mark(X1),mark(X2)))
        mark#(U12(X)) -> mark#(X) -> mark#(nil()) -> active#(nil())
        mark#(U12(X)) -> mark#(X) -> mark#(U11(X)) -> mark#(X)
        mark#(U12(X)) -> mark#(X) ->
        mark#(U11(X)) -> active#(U11(mark(X)))
        mark#(U12(X)) -> mark#(X) -> mark#(tt()) -> active#(tt())
        mark#(U12(X)) -> mark#(X) -> mark#(U12(X)) -> mark#(X)
        mark#(U12(X)) -> mark#(X) ->
        mark#(U12(X)) -> active#(U12(mark(X)))
        mark#(U12(X)) -> mark#(X) -> mark#(isNePal(X)) -> mark#(X)
        mark#(U12(X)) -> mark#(X) ->
        mark#(isNePal(X)) -> active#(isNePal(mark(X)))
        mark#(U12(X)) -> active#(U12(mark(X))) ->
        active#(__(__(X,Y),Z)) -> mark#(__(X,__(Y,Z)))
        mark#(U11(X)) -> mark#(X) -> mark#(__(X1,X2)) -> mark#(X2)
        mark#(U11(X)) -> mark#(X) -> mark#(__(X1,X2)) -> mark#(X1)
        mark#(U11(X)) -> mark#(X) ->
        mark#(__(X1,X2)) -> active#(__(mark(X1),mark(X2)))
        mark#(U11(X)) -> mark#(X) -> mark#(nil()) -> active#(nil())
        mark#(U11(X)) -> mark#(X) -> mark#(U11(X)) -> mark#(X)
        mark#(U11(X)) -> mark#(X) ->
        mark#(U11(X)) -> active#(U11(mark(X)))
        mark#(U11(X)) -> mark#(X) -> mark#(tt()) -> active#(tt())
        mark#(U11(X)) -> mark#(X) -> mark#(U12(X)) -> mark#(X)
        mark#(U11(X)) -> mark#(X) ->
        mark#(U12(X)) -> active#(U12(mark(X)))
        mark#(U11(X)) -> mark#(X) -> mark#(isNePal(X)) -> mark#(X)
        mark#(U11(X)) -> mark#(X) ->
        mark#(isNePal(X)) -> active#(isNePal(mark(X)))
        mark#(U11(X)) -> active#(U11(mark(X))) ->
        active#(__(__(X,Y),Z)) -> mark#(__(X,__(Y,Z)))
        mark#(__(X1,X2)) -> mark#(X2) -> mark#(__(X1,X2)) -> mark#(X2)
        mark#(__(X1,X2)) -> mark#(X2) -> mark#(__(X1,X2)) -> mark#(X1)
        mark#(__(X1,X2)) -> mark#(X2) ->
        mark#(__(X1,X2)) -> active#(__(mark(X1),mark(X2)))
        mark#(__(X1,X2)) -> mark#(X2) ->
        mark#(nil()) -> active#(nil())
        mark#(__(X1,X2)) -> mark#(X2) -> mark#(U11(X)) -> mark#(X)
        mark#(__(X1,X2)) -> mark#(X2) ->
        mark#(U11(X)) -> active#(U11(mark(X)))
        mark#(__(X1,X2)) -> mark#(X2) -> mark#(tt()) -> active#(tt())
        mark#(__(X1,X2)) -> mark#(X2) -> mark#(U12(X)) -> mark#(X)
        mark#(__(X1,X2)) -> mark#(X2) ->
        mark#(U12(X)) -> active#(U12(mark(X)))
        mark#(__(X1,X2)) -> mark#(X2) -> mark#(isNePal(X)) -> mark#(X)
        mark#(__(X1,X2)) -> mark#(X2) ->
        mark#(isNePal(X)) -> active#(isNePal(mark(X)))
        mark#(__(X1,X2)) -> mark#(X1) -> mark#(__(X1,X2)) -> mark#(X2)
        mark#(__(X1,X2)) -> mark#(X1) -> mark#(__(X1,X2)) -> mark#(X1)
        mark#(__(X1,X2)) -> mark#(X1) ->
        mark#(__(X1,X2)) -> active#(__(mark(X1),mark(X2)))
        mark#(__(X1,X2)) -> mark#(X1) ->
        mark#(nil()) -> active#(nil())
        mark#(__(X1,X2)) -> mark#(X1) -> mark#(U11(X)) -> mark#(X)
        mark#(__(X1,X2)) -> mark#(X1) ->
        mark#(U11(X)) -> active#(U11(mark(X)))
        mark#(__(X1,X2)) -> mark#(X1) -> mark#(tt()) -> active#(tt())
        mark#(__(X1,X2)) -> mark#(X1) -> mark#(U12(X)) -> mark#(X)
        mark#(__(X1,X2)) -> mark#(X1) ->
        mark#(U12(X)) -> active#(U12(mark(X)))
        mark#(__(X1,X2)) -> mark#(X1) -> mark#(isNePal(X)) -> mark#(X)
        mark#(__(X1,X2)) -> mark#(X1) ->
        mark#(isNePal(X)) -> active#(isNePal(mark(X)))
        mark#(__(X1,X2)) -> active#(__(mark(X1),mark(X2))) ->
        active#(__(__(X,Y),Z)) -> mark#(__(X,__(Y,Z)))
        active#(__(__(X,Y),Z)) -> mark#(__(X,__(Y,Z))) ->
        mark#(__(X1,X2)) -> mark#(X2)
        active#(__(__(X,Y),Z)) -> mark#(__(X,__(Y,Z))) ->
        mark#(__(X1,X2)) -> mark#(X1)
        active#(__(__(X,Y),Z)) -> mark#(__(X,__(Y,Z))) ->
        mark#(__(X1,X2)) -> active#(__(mark(X1),mark(X2)))
        active#(__(__(X,Y),Z)) -> mark#(__(X,__(Y,Z))) ->
        mark#(U11(X)) -> mark#(X)
        active#(__(__(X,Y),Z)) -> mark#(__(X,__(Y,Z))) ->
        mark#(U11(X)) -> active#(U11(mark(X)))
        active#(__(__(X,Y),Z)) -> mark#(__(X,__(Y,Z))) ->
        mark#(U12(X)) -> mark#(X)
        active#(__(__(X,Y),Z)) -> mark#(__(X,__(Y,Z))) ->
        mark#(U12(X)) -> active#(U12(mark(X)))
        active#(__(__(X,Y),Z)) -> mark#(__(X,__(Y,Z))) ->
        mark#(isNePal(X)) -> mark#(X)
        active#(__(__(X,Y),Z)) -> mark#(__(X,__(Y,Z))) ->
        mark#(isNePal(X)) -> active#(isNePal(mark(X)))
       SCC Processor:
        #sccs: 1
        #rules: 10
        #arcs: 68/144
        DPs:
         mark#(isNePal(X)) -> mark#(X)
         mark#(isNePal(X)) -> active#(isNePal(mark(X)))
         active#(__(__(X,Y),Z)) -> mark#(__(X,__(Y,Z)))
         mark#(U12(X)) -> active#(U12(mark(X)))
         mark#(U12(X)) -> mark#(X)
         mark#(U11(X)) -> active#(U11(mark(X)))
         mark#(U11(X)) -> mark#(X)
         mark#(__(X1,X2)) -> active#(__(mark(X1),mark(X2)))
         mark#(__(X1,X2)) -> mark#(X1)
         mark#(__(X1,X2)) -> mark#(X2)
        TRS:
         active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
         mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
         mark(nil()) -> active(nil())
         mark(U11(X)) -> active(U11(mark(X)))
         mark(tt()) -> active(tt())
         mark(U12(X)) -> active(U12(mark(X)))
         mark(isNePal(X)) -> active(isNePal(mark(X)))
         __(mark(X1),X2) -> __(X1,X2)
         __(X1,mark(X2)) -> __(X1,X2)
         __(active(X1),X2) -> __(X1,X2)
         __(X1,active(X2)) -> __(X1,X2)
         U11(mark(X)) -> U11(X)
         U11(active(X)) -> U11(X)
         U12(mark(X)) -> U12(X)
         U12(active(X)) -> U12(X)
         isNePal(mark(X)) -> isNePal(X)
         isNePal(active(X)) -> isNePal(X)
        Semantic Labeling Processor:
         dimension: 1
         usable rules:
          active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
          mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
          mark(nil()) -> active(nil())
          mark(U11(X)) -> active(U11(mark(X)))
          mark(tt()) -> active(tt())
          mark(U12(X)) -> active(U12(mark(X)))
          mark(isNePal(X)) -> active(isNePal(mark(X)))
          __(mark(X1),X2) -> __(X1,X2)
          __(X1,mark(X2)) -> __(X1,X2)
          __(active(X1),X2) -> __(X1,X2)
          __(X1,active(X2)) -> __(X1,X2)
          U11(mark(X)) -> U11(X)
          U11(active(X)) -> U11(X)
          U12(mark(X)) -> U12(X)
          U12(active(X)) -> U12(X)
          isNePal(mark(X)) -> isNePal(X)
          isNePal(active(X)) -> isNePal(X)
         interpretation:
          [isNePal](x0) = 0,
          
          [U12](x0) = x0,
          
          [U11](x0) = 0,
          
          [tt] = 0,
          
          [nil] = 0,
          
          [mark](x0) = 1,
          
          [active](x0) = 1,
          
          [__](x0, x1) = x1
          labeled:
          usable (for model):
          argument filtering:
           pi(__) = [0,1]
           pi(active) = 0
           pi(mark) = 0
           pi(nil) = []
           pi(tt) = []
           pi(U11) = [0]
           pi(U12) = 0
           pi(isNePal) = 0
           pi(active#) = 0
           pi(mark#) = 0
         precedence:
          mark# ~ active# ~ isNePal ~ U12 ~ U11 ~ tt ~ nil ~ mark ~ active ~ __
         problem:
          DPs:
           mark#(isNePal(X)) -> mark#(X)
           mark#(isNePal(X)) -> active#(isNePal(mark(X)))
           mark#(U12(X)) -> active#(U12(mark(X)))
           mark#(U12(X)) -> mark#(X)
           mark#(U11(X)) -> active#(U11(mark(X)))
           mark#(__(X1,X2)) -> active#(__(mark(X1),mark(X2)))
          TRS:
           active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
           mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
           mark(nil()) -> active(nil())
           mark(U11(X)) -> active(U11(mark(X)))
           mark(tt()) -> active(tt())
           mark(U12(X)) -> active(U12(mark(X)))
           mark(isNePal(X)) -> active(isNePal(mark(X)))
           __(mark(X1),X2) -> __(X1,X2)
           __(X1,mark(X2)) -> __(X1,X2)
           __(active(X1),X2) -> __(X1,X2)
           __(X1,active(X2)) -> __(X1,X2)
           U11(mark(X)) -> U11(X)
           U11(active(X)) -> U11(X)
           U12(mark(X)) -> U12(X)
           U12(active(X)) -> U12(X)
           isNePal(mark(X)) -> isNePal(X)
           isNePal(active(X)) -> isNePal(X)
         Restore Modifier:
          DPs:
           mark#(isNePal(X)) -> mark#(X)
           mark#(isNePal(X)) -> active#(isNePal(mark(X)))
           mark#(U12(X)) -> active#(U12(mark(X)))
           mark#(U12(X)) -> mark#(X)
           mark#(U11(X)) -> active#(U11(mark(X)))
           mark#(__(X1,X2)) -> active#(__(mark(X1),mark(X2)))
          TRS:
           active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
           mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
           mark(nil()) -> active(nil())
           mark(U11(X)) -> active(U11(mark(X)))
           mark(tt()) -> active(tt())
           mark(U12(X)) -> active(U12(mark(X)))
           mark(isNePal(X)) -> active(isNePal(mark(X)))
           __(mark(X1),X2) -> __(X1,X2)
           __(X1,mark(X2)) -> __(X1,X2)
           __(active(X1),X2) -> __(X1,X2)
           __(X1,active(X2)) -> __(X1,X2)
           U11(mark(X)) -> U11(X)
           U11(active(X)) -> U11(X)
           U12(mark(X)) -> U12(X)
           U12(active(X)) -> U12(X)
           isNePal(mark(X)) -> isNePal(X)
           isNePal(active(X)) -> isNePal(X)
          SCC Processor:
           #sccs: 1
           #rules: 2
           #arcs: 58/36
           DPs:
            mark#(isNePal(X)) -> mark#(X)
            mark#(U12(X)) -> mark#(X)
           TRS:
            active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
            mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
            mark(nil()) -> active(nil())
            mark(U11(X)) -> active(U11(mark(X)))
            mark(tt()) -> active(tt())
            mark(U12(X)) -> active(U12(mark(X)))
            mark(isNePal(X)) -> active(isNePal(mark(X)))
            __(mark(X1),X2) -> __(X1,X2)
            __(X1,mark(X2)) -> __(X1,X2)
            __(active(X1),X2) -> __(X1,X2)
            __(X1,active(X2)) -> __(X1,X2)
            U11(mark(X)) -> U11(X)
            U11(active(X)) -> U11(X)
            U12(mark(X)) -> U12(X)
            U12(active(X)) -> U12(X)
            isNePal(mark(X)) -> isNePal(X)
            isNePal(active(X)) -> isNePal(X)
           Bounds Processor:
            bound: 0
            enrichment: match-dp
            automaton:
             final states: {3}
             transitions:
              f680() -> 4*
              mark{#,0}(4) -> 3*
            problem:
             DPs:
              mark#(isNePal(X)) -> mark#(X)
             TRS:
              active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
              mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
              mark(nil()) -> active(nil())
              mark(U11(X)) -> active(U11(mark(X)))
              mark(tt()) -> active(tt())
              mark(U12(X)) -> active(U12(mark(X)))
              mark(isNePal(X)) -> active(isNePal(mark(X)))
              __(mark(X1),X2) -> __(X1,X2)
              __(X1,mark(X2)) -> __(X1,X2)
              __(active(X1),X2) -> __(X1,X2)
              __(X1,active(X2)) -> __(X1,X2)
              U11(mark(X)) -> U11(X)
              U11(active(X)) -> U11(X)
              U12(mark(X)) -> U12(X)
              U12(active(X)) -> U12(X)
              isNePal(mark(X)) -> isNePal(X)
              isNePal(active(X)) -> isNePal(X)
            Bounds Processor:
             bound: 0
             enrichment: match-dp
             automaton:
              final states: {1}
              transitions:
               mark{#,0}(2) -> 1*
               f710() -> 2*
             problem:
              DPs:
               
              TRS:
               active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
               mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
               mark(nil()) -> active(nil())
               mark(U11(X)) -> active(U11(mark(X)))
               mark(tt()) -> active(tt())
               mark(U12(X)) -> active(U12(mark(X)))
               mark(isNePal(X)) -> active(isNePal(mark(X)))
               __(mark(X1),X2) -> __(X1,X2)
               __(X1,mark(X2)) -> __(X1,X2)
               __(active(X1),X2) -> __(X1,X2)
               __(X1,active(X2)) -> __(X1,X2)
               U11(mark(X)) -> U11(X)
               U11(active(X)) -> U11(X)
               U12(mark(X)) -> U12(X)
               U12(active(X)) -> U12(X)
               isNePal(mark(X)) -> isNePal(X)
               isNePal(active(X)) -> isNePal(X)
             Qed
      
      DPs:
       __#(mark(X1),X2) -> __#(X1,X2)
       __#(X1,mark(X2)) -> __#(X1,X2)
       __#(active(X1),X2) -> __#(X1,X2)
       __#(X1,active(X2)) -> __#(X1,X2)
      TRS:
       active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
       mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
       mark(nil()) -> active(nil())
       mark(U11(X)) -> active(U11(mark(X)))
       mark(tt()) -> active(tt())
       mark(U12(X)) -> active(U12(mark(X)))
       mark(isNePal(X)) -> active(isNePal(mark(X)))
       __(mark(X1),X2) -> __(X1,X2)
       __(X1,mark(X2)) -> __(X1,X2)
       __(active(X1),X2) -> __(X1,X2)
       __(X1,active(X2)) -> __(X1,X2)
       U11(mark(X)) -> U11(X)
       U11(active(X)) -> U11(X)
       U12(mark(X)) -> U12(X)
       U12(active(X)) -> U12(X)
       isNePal(mark(X)) -> isNePal(X)
       isNePal(active(X)) -> isNePal(X)
      Subterm Criterion Processor:
       simple projection:
        pi(__#) = 1
       problem:
        DPs:
         __#(mark(X1),X2) -> __#(X1,X2)
         __#(active(X1),X2) -> __#(X1,X2)
        TRS:
         active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
         mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
         mark(nil()) -> active(nil())
         mark(U11(X)) -> active(U11(mark(X)))
         mark(tt()) -> active(tt())
         mark(U12(X)) -> active(U12(mark(X)))
         mark(isNePal(X)) -> active(isNePal(mark(X)))
         __(mark(X1),X2) -> __(X1,X2)
         __(X1,mark(X2)) -> __(X1,X2)
         __(active(X1),X2) -> __(X1,X2)
         __(X1,active(X2)) -> __(X1,X2)
         U11(mark(X)) -> U11(X)
         U11(active(X)) -> U11(X)
         U12(mark(X)) -> U12(X)
         U12(active(X)) -> U12(X)
         isNePal(mark(X)) -> isNePal(X)
         isNePal(active(X)) -> isNePal(X)
       Subterm Criterion Processor:
        simple projection:
         pi(__#) = 0
        problem:
         DPs:
          
         TRS:
          active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
          mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
          mark(nil()) -> active(nil())
          mark(U11(X)) -> active(U11(mark(X)))
          mark(tt()) -> active(tt())
          mark(U12(X)) -> active(U12(mark(X)))
          mark(isNePal(X)) -> active(isNePal(mark(X)))
          __(mark(X1),X2) -> __(X1,X2)
          __(X1,mark(X2)) -> __(X1,X2)
          __(active(X1),X2) -> __(X1,X2)
          __(X1,active(X2)) -> __(X1,X2)
          U11(mark(X)) -> U11(X)
          U11(active(X)) -> U11(X)
          U12(mark(X)) -> U12(X)
          U12(active(X)) -> U12(X)
          isNePal(mark(X)) -> isNePal(X)
          isNePal(active(X)) -> isNePal(X)
        Qed
      
      DPs:
       U11#(mark(X)) -> U11#(X)
       U11#(active(X)) -> U11#(X)
      TRS:
       active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
       mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
       mark(nil()) -> active(nil())
       mark(U11(X)) -> active(U11(mark(X)))
       mark(tt()) -> active(tt())
       mark(U12(X)) -> active(U12(mark(X)))
       mark(isNePal(X)) -> active(isNePal(mark(X)))
       __(mark(X1),X2) -> __(X1,X2)
       __(X1,mark(X2)) -> __(X1,X2)
       __(active(X1),X2) -> __(X1,X2)
       __(X1,active(X2)) -> __(X1,X2)
       U11(mark(X)) -> U11(X)
       U11(active(X)) -> U11(X)
       U12(mark(X)) -> U12(X)
       U12(active(X)) -> U12(X)
       isNePal(mark(X)) -> isNePal(X)
       isNePal(active(X)) -> isNePal(X)
      Subterm Criterion Processor:
       simple projection:
        pi(U11#) = 0
       problem:
        DPs:
         
        TRS:
         active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
         mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
         mark(nil()) -> active(nil())
         mark(U11(X)) -> active(U11(mark(X)))
         mark(tt()) -> active(tt())
         mark(U12(X)) -> active(U12(mark(X)))
         mark(isNePal(X)) -> active(isNePal(mark(X)))
         __(mark(X1),X2) -> __(X1,X2)
         __(X1,mark(X2)) -> __(X1,X2)
         __(active(X1),X2) -> __(X1,X2)
         __(X1,active(X2)) -> __(X1,X2)
         U11(mark(X)) -> U11(X)
         U11(active(X)) -> U11(X)
         U12(mark(X)) -> U12(X)
         U12(active(X)) -> U12(X)
         isNePal(mark(X)) -> isNePal(X)
         isNePal(active(X)) -> isNePal(X)
       Qed
      
      DPs:
       U12#(mark(X)) -> U12#(X)
       U12#(active(X)) -> U12#(X)
      TRS:
       active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
       mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
       mark(nil()) -> active(nil())
       mark(U11(X)) -> active(U11(mark(X)))
       mark(tt()) -> active(tt())
       mark(U12(X)) -> active(U12(mark(X)))
       mark(isNePal(X)) -> active(isNePal(mark(X)))
       __(mark(X1),X2) -> __(X1,X2)
       __(X1,mark(X2)) -> __(X1,X2)
       __(active(X1),X2) -> __(X1,X2)
       __(X1,active(X2)) -> __(X1,X2)
       U11(mark(X)) -> U11(X)
       U11(active(X)) -> U11(X)
       U12(mark(X)) -> U12(X)
       U12(active(X)) -> U12(X)
       isNePal(mark(X)) -> isNePal(X)
       isNePal(active(X)) -> isNePal(X)
      Subterm Criterion Processor:
       simple projection:
        pi(U12#) = 0
       problem:
        DPs:
         
        TRS:
         active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
         mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
         mark(nil()) -> active(nil())
         mark(U11(X)) -> active(U11(mark(X)))
         mark(tt()) -> active(tt())
         mark(U12(X)) -> active(U12(mark(X)))
         mark(isNePal(X)) -> active(isNePal(mark(X)))
         __(mark(X1),X2) -> __(X1,X2)
         __(X1,mark(X2)) -> __(X1,X2)
         __(active(X1),X2) -> __(X1,X2)
         __(X1,active(X2)) -> __(X1,X2)
         U11(mark(X)) -> U11(X)
         U11(active(X)) -> U11(X)
         U12(mark(X)) -> U12(X)
         U12(active(X)) -> U12(X)
         isNePal(mark(X)) -> isNePal(X)
         isNePal(active(X)) -> isNePal(X)
       Qed
      
      DPs:
       isNePal#(mark(X)) -> isNePal#(X)
       isNePal#(active(X)) -> isNePal#(X)
      TRS:
       active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
       mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
       mark(nil()) -> active(nil())
       mark(U11(X)) -> active(U11(mark(X)))
       mark(tt()) -> active(tt())
       mark(U12(X)) -> active(U12(mark(X)))
       mark(isNePal(X)) -> active(isNePal(mark(X)))
       __(mark(X1),X2) -> __(X1,X2)
       __(X1,mark(X2)) -> __(X1,X2)
       __(active(X1),X2) -> __(X1,X2)
       __(X1,active(X2)) -> __(X1,X2)
       U11(mark(X)) -> U11(X)
       U11(active(X)) -> U11(X)
       U12(mark(X)) -> U12(X)
       U12(active(X)) -> U12(X)
       isNePal(mark(X)) -> isNePal(X)
       isNePal(active(X)) -> isNePal(X)
      Subterm Criterion Processor:
       simple projection:
        pi(isNePal#) = 0
       problem:
        DPs:
         
        TRS:
         active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
         mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
         mark(nil()) -> active(nil())
         mark(U11(X)) -> active(U11(mark(X)))
         mark(tt()) -> active(tt())
         mark(U12(X)) -> active(U12(mark(X)))
         mark(isNePal(X)) -> active(isNePal(mark(X)))
         __(mark(X1),X2) -> __(X1,X2)
         __(X1,mark(X2)) -> __(X1,X2)
         __(active(X1),X2) -> __(X1,X2)
         __(X1,active(X2)) -> __(X1,X2)
         U11(mark(X)) -> U11(X)
         U11(active(X)) -> U11(X)
         U12(mark(X)) -> U12(X)
         U12(active(X)) -> U12(X)
         isNePal(mark(X)) -> isNePal(X)
         isNePal(active(X)) -> isNePal(X)
       Qed