YES

Problem:
 active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
 active(__(X,nil())) -> mark(X)
 active(__(nil(),X)) -> mark(X)
 active(and(tt(),X)) -> mark(X)
 active(isNePal(__(I,__(P,I)))) -> mark(tt())
 mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
 mark(nil()) -> active(nil())
 mark(and(X1,X2)) -> active(and(mark(X1),X2))
 mark(tt()) -> active(tt())
 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)
 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)
 isNePal(mark(X)) -> isNePal(X)
 isNePal(active(X)) -> isNePal(X)

Proof:
 Matrix Interpretation Processor: dim=3
  
  interpretation:
                   [1 0 0]  
   [isNePal](x0) = [0 0 0]x0
                   [0 0 0]  ,
   
                   [1 0 0]     [1 0 0]     [1]
   [and](x0, x1) = [0 0 0]x0 + [0 0 0]x1 + [0]
                   [0 0 0]     [0 0 0]     [0],
   
          [0]
   [tt] = [0]
          [0],
   
           [0]
   [nil] = [0]
           [0],
   
                [1 0 0]  
   [mark](x0) = [1 0 0]x0
                [0 0 0]  ,
   
                  [1 0 0]  
   [active](x0) = [1 0 0]x0
                  [0 0 0]  ,
   
                  [1 0 0]     [1 0 0]  
   [__](x0, x1) = [0 0 0]x0 + [0 0 0]x1
                  [0 0 0]     [0 0 0]  
  orientation:
                           [1 0 0]    [1 0 0]    [1 0 0]     [1 0 0]    [1 0 0]    [1 0 0]                       
   active(__(__(X,Y),Z)) = [1 0 0]X + [1 0 0]Y + [1 0 0]Z >= [1 0 0]X + [1 0 0]Y + [1 0 0]Z = mark(__(X,__(Y,Z)))
                           [0 0 0]    [0 0 0]    [0 0 0]     [0 0 0]    [0 0 0]    [0 0 0]                       
   
                         [1 0 0]     [1 0 0]           
   active(__(X,nil())) = [1 0 0]X >= [1 0 0]X = mark(X)
                         [0 0 0]     [0 0 0]           
   
                         [1 0 0]     [1 0 0]           
   active(__(nil(),X)) = [1 0 0]X >= [1 0 0]X = mark(X)
                         [0 0 0]     [0 0 0]           
   
                         [1 0 0]    [1]    [1 0 0]           
   active(and(tt(),X)) = [1 0 0]X + [1] >= [1 0 0]X = mark(X)
                         [0 0 0]    [0]    [0 0 0]           
   
                                    [2 0 0]    [1 0 0]     [0]             
   active(isNePal(__(I,__(P,I)))) = [2 0 0]I + [1 0 0]P >= [0] = mark(tt())
                                    [0 0 0]    [0 0 0]     [0]             
   
                     [1 0 0]     [1 0 0]      [1 0 0]     [1 0 0]                                  
   mark(__(X1,X2)) = [1 0 0]X1 + [1 0 0]X2 >= [1 0 0]X1 + [1 0 0]X2 = active(__(mark(X1),mark(X2)))
                     [0 0 0]     [0 0 0]      [0 0 0]     [0 0 0]                                  
   
                 [0]    [0]                
   mark(nil()) = [0] >= [0] = active(nil())
                 [0]    [0]                
   
                      [1 0 0]     [1 0 0]     [1]    [1 0 0]     [1 0 0]     [1]                           
   mark(and(X1,X2)) = [1 0 0]X1 + [1 0 0]X2 + [1] >= [1 0 0]X1 + [1 0 0]X2 + [1] = active(and(mark(X1),X2))
                      [0 0 0]     [0 0 0]     [0]    [0 0 0]     [0 0 0]     [0]                           
   
                [0]    [0]               
   mark(tt()) = [0] >= [0] = active(tt())
                [0]    [0]               
   
                      [1 0 0]     [1 0 0]                            
   mark(isNePal(X)) = [1 0 0]X >= [1 0 0]X = active(isNePal(mark(X)))
                      [0 0 0]     [0 0 0]                            
   
                     [1 0 0]     [1 0 0]      [1 0 0]     [1 0 0]              
   __(mark(X1),X2) = [0 0 0]X1 + [0 0 0]X2 >= [0 0 0]X1 + [0 0 0]X2 = __(X1,X2)
                     [0 0 0]     [0 0 0]      [0 0 0]     [0 0 0]              
   
                     [1 0 0]     [1 0 0]      [1 0 0]     [1 0 0]              
   __(X1,mark(X2)) = [0 0 0]X1 + [0 0 0]X2 >= [0 0 0]X1 + [0 0 0]X2 = __(X1,X2)
                     [0 0 0]     [0 0 0]      [0 0 0]     [0 0 0]              
   
                       [1 0 0]     [1 0 0]      [1 0 0]     [1 0 0]              
   __(active(X1),X2) = [0 0 0]X1 + [0 0 0]X2 >= [0 0 0]X1 + [0 0 0]X2 = __(X1,X2)
                       [0 0 0]     [0 0 0]      [0 0 0]     [0 0 0]              
   
                       [1 0 0]     [1 0 0]      [1 0 0]     [1 0 0]              
   __(X1,active(X2)) = [0 0 0]X1 + [0 0 0]X2 >= [0 0 0]X1 + [0 0 0]X2 = __(X1,X2)
                       [0 0 0]     [0 0 0]      [0 0 0]     [0 0 0]              
   
                      [1 0 0]     [1 0 0]     [1]    [1 0 0]     [1 0 0]     [1]             
   and(mark(X1),X2) = [0 0 0]X1 + [0 0 0]X2 + [0] >= [0 0 0]X1 + [0 0 0]X2 + [0] = and(X1,X2)
                      [0 0 0]     [0 0 0]     [0]    [0 0 0]     [0 0 0]     [0]             
   
                      [1 0 0]     [1 0 0]     [1]    [1 0 0]     [1 0 0]     [1]             
   and(X1,mark(X2)) = [0 0 0]X1 + [0 0 0]X2 + [0] >= [0 0 0]X1 + [0 0 0]X2 + [0] = and(X1,X2)
                      [0 0 0]     [0 0 0]     [0]    [0 0 0]     [0 0 0]     [0]             
   
                        [1 0 0]     [1 0 0]     [1]    [1 0 0]     [1 0 0]     [1]             
   and(active(X1),X2) = [0 0 0]X1 + [0 0 0]X2 + [0] >= [0 0 0]X1 + [0 0 0]X2 + [0] = and(X1,X2)
                        [0 0 0]     [0 0 0]     [0]    [0 0 0]     [0 0 0]     [0]             
   
                        [1 0 0]     [1 0 0]     [1]    [1 0 0]     [1 0 0]     [1]             
   and(X1,active(X2)) = [0 0 0]X1 + [0 0 0]X2 + [0] >= [0 0 0]X1 + [0 0 0]X2 + [0] = and(X1,X2)
                        [0 0 0]     [0 0 0]     [0]    [0 0 0]     [0 0 0]     [0]             
   
                      [1 0 0]     [1 0 0]              
   isNePal(mark(X)) = [0 0 0]X >= [0 0 0]X = isNePal(X)
                      [0 0 0]     [0 0 0]              
   
                        [1 0 0]     [1 0 0]              
   isNePal(active(X)) = [0 0 0]X >= [0 0 0]X = isNePal(X)
                        [0 0 0]     [0 0 0]              
  problem:
   active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
   active(__(X,nil())) -> mark(X)
   active(__(nil(),X)) -> mark(X)
   active(isNePal(__(I,__(P,I)))) -> mark(tt())
   mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
   mark(nil()) -> active(nil())
   mark(and(X1,X2)) -> active(and(mark(X1),X2))
   mark(tt()) -> active(tt())
   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)
   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)
   isNePal(mark(X)) -> isNePal(X)
   isNePal(active(X)) -> isNePal(X)
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [isNePal](x0) = 2x0,
    
    [and](x0, x1) = 2x0 + x1,
    
    [tt] = 0,
    
    [nil] = 4,
    
    [mark](x0) = x0,
    
    [active](x0) = x0,
    
    [__](x0, x1) = 4x0 + x1 + 1
   orientation:
    active(__(__(X,Y),Z)) = 16X + 4Y + Z + 5 >= 4X + 4Y + Z + 2 = mark(__(X,__(Y,Z)))
    
    active(__(X,nil())) = 4X + 5 >= X = mark(X)
    
    active(__(nil(),X)) = X + 17 >= X = mark(X)
    
    active(isNePal(__(I,__(P,I)))) = 10I + 8P + 4 >= 0 = mark(tt())
    
    mark(__(X1,X2)) = 4X1 + X2 + 1 >= 4X1 + X2 + 1 = active(__(mark(X1),mark(X2)))
    
    mark(nil()) = 4 >= 4 = active(nil())
    
    mark(and(X1,X2)) = 2X1 + X2 >= 2X1 + X2 = active(and(mark(X1),X2))
    
    mark(tt()) = 0 >= 0 = active(tt())
    
    mark(isNePal(X)) = 2X >= 2X = active(isNePal(mark(X)))
    
    __(mark(X1),X2) = 4X1 + X2 + 1 >= 4X1 + X2 + 1 = __(X1,X2)
    
    __(X1,mark(X2)) = 4X1 + X2 + 1 >= 4X1 + X2 + 1 = __(X1,X2)
    
    __(active(X1),X2) = 4X1 + X2 + 1 >= 4X1 + X2 + 1 = __(X1,X2)
    
    __(X1,active(X2)) = 4X1 + X2 + 1 >= 4X1 + X2 + 1 = __(X1,X2)
    
    and(mark(X1),X2) = 2X1 + X2 >= 2X1 + X2 = and(X1,X2)
    
    and(X1,mark(X2)) = 2X1 + X2 >= 2X1 + X2 = and(X1,X2)
    
    and(active(X1),X2) = 2X1 + X2 >= 2X1 + X2 = and(X1,X2)
    
    and(X1,active(X2)) = 2X1 + X2 >= 2X1 + X2 = and(X1,X2)
    
    isNePal(mark(X)) = 2X >= 2X = isNePal(X)
    
    isNePal(active(X)) = 2X >= 2X = isNePal(X)
   problem:
    mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
    mark(nil()) -> active(nil())
    mark(and(X1,X2)) -> active(and(mark(X1),X2))
    mark(tt()) -> active(tt())
    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)
    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)
    isNePal(mark(X)) -> isNePal(X)
    isNePal(active(X)) -> isNePal(X)
   DP Processor:
    DPs:
     mark#(__(X1,X2)) -> mark#(X2)
     mark#(__(X1,X2)) -> mark#(X1)
     mark#(__(X1,X2)) -> __#(mark(X1),mark(X2))
     mark#(and(X1,X2)) -> mark#(X1)
     mark#(and(X1,X2)) -> and#(mark(X1),X2)
     mark#(isNePal(X)) -> mark#(X)
     mark#(isNePal(X)) -> isNePal#(mark(X))
     __#(mark(X1),X2) -> __#(X1,X2)
     __#(X1,mark(X2)) -> __#(X1,X2)
     __#(active(X1),X2) -> __#(X1,X2)
     __#(X1,active(X2)) -> __#(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)
     isNePal#(mark(X)) -> isNePal#(X)
     isNePal#(active(X)) -> isNePal#(X)
    TRS:
     mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
     mark(nil()) -> active(nil())
     mark(and(X1,X2)) -> active(and(mark(X1),X2))
     mark(tt()) -> active(tt())
     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)
     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)
     isNePal(mark(X)) -> isNePal(X)
     isNePal(active(X)) -> isNePal(X)
    TDG Processor:
     DPs:
      mark#(__(X1,X2)) -> mark#(X2)
      mark#(__(X1,X2)) -> mark#(X1)
      mark#(__(X1,X2)) -> __#(mark(X1),mark(X2))
      mark#(and(X1,X2)) -> mark#(X1)
      mark#(and(X1,X2)) -> and#(mark(X1),X2)
      mark#(isNePal(X)) -> mark#(X)
      mark#(isNePal(X)) -> isNePal#(mark(X))
      __#(mark(X1),X2) -> __#(X1,X2)
      __#(X1,mark(X2)) -> __#(X1,X2)
      __#(active(X1),X2) -> __#(X1,X2)
      __#(X1,active(X2)) -> __#(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)
      isNePal#(mark(X)) -> isNePal#(X)
      isNePal#(active(X)) -> isNePal#(X)
     TRS:
      mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
      mark(nil()) -> active(nil())
      mark(and(X1,X2)) -> active(and(mark(X1),X2))
      mark(tt()) -> active(tt())
      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)
      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)
      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)
      and#(mark(X1),X2) -> and#(X1,X2) ->
      and#(X1,active(X2)) -> and#(X1,X2)
      and#(mark(X1),X2) -> and#(X1,X2) ->
      and#(active(X1),X2) -> and#(X1,X2)
      and#(mark(X1),X2) -> and#(X1,X2) ->
      and#(X1,mark(X2)) -> and#(X1,X2)
      and#(mark(X1),X2) -> and#(X1,X2) ->
      and#(mark(X1),X2) -> and#(X1,X2)
      and#(active(X1),X2) -> and#(X1,X2) ->
      and#(X1,active(X2)) -> and#(X1,X2)
      and#(active(X1),X2) -> and#(X1,X2) ->
      and#(active(X1),X2) -> and#(X1,X2)
      and#(active(X1),X2) -> and#(X1,X2) ->
      and#(X1,mark(X2)) -> and#(X1,X2)
      and#(active(X1),X2) -> and#(X1,X2) ->
      and#(mark(X1),X2) -> and#(X1,X2)
      and#(X1,mark(X2)) -> and#(X1,X2) ->
      and#(X1,active(X2)) -> and#(X1,X2)
      and#(X1,mark(X2)) -> and#(X1,X2) ->
      and#(active(X1),X2) -> and#(X1,X2)
      and#(X1,mark(X2)) -> and#(X1,X2) ->
      and#(X1,mark(X2)) -> and#(X1,X2)
      and#(X1,mark(X2)) -> and#(X1,X2) ->
      and#(mark(X1),X2) -> and#(X1,X2)
      and#(X1,active(X2)) -> and#(X1,X2) ->
      and#(X1,active(X2)) -> and#(X1,X2)
      and#(X1,active(X2)) -> and#(X1,X2) ->
      and#(active(X1),X2) -> and#(X1,X2)
      and#(X1,active(X2)) -> and#(X1,X2) ->
      and#(X1,mark(X2)) -> and#(X1,X2)
      and#(X1,active(X2)) -> and#(X1,X2) ->
      and#(mark(X1),X2) -> and#(X1,X2)
      __#(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)
      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)) -> isNePal#(mark(X))
      mark#(isNePal(X)) -> mark#(X) -> mark#(isNePal(X)) -> mark#(X)
      mark#(isNePal(X)) -> mark#(X) ->
      mark#(and(X1,X2)) -> and#(mark(X1),X2)
      mark#(isNePal(X)) -> mark#(X) -> mark#(and(X1,X2)) -> mark#(X1)
      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#(and(X1,X2)) -> and#(mark(X1),X2) ->
      and#(X1,active(X2)) -> and#(X1,X2)
      mark#(and(X1,X2)) -> and#(mark(X1),X2) ->
      and#(active(X1),X2) -> and#(X1,X2)
      mark#(and(X1,X2)) -> and#(mark(X1),X2) ->
      and#(X1,mark(X2)) -> and#(X1,X2)
      mark#(and(X1,X2)) -> and#(mark(X1),X2) ->
      and#(mark(X1),X2) -> and#(X1,X2)
      mark#(and(X1,X2)) -> mark#(X1) ->
      mark#(isNePal(X)) -> isNePal#(mark(X))
      mark#(and(X1,X2)) -> mark#(X1) -> mark#(isNePal(X)) -> mark#(X)
      mark#(and(X1,X2)) -> mark#(X1) ->
      mark#(and(X1,X2)) -> and#(mark(X1),X2)
      mark#(and(X1,X2)) -> mark#(X1) ->
      mark#(and(X1,X2)) -> mark#(X1)
      mark#(and(X1,X2)) -> mark#(X1) ->
      mark#(__(X1,X2)) -> __#(mark(X1),mark(X2))
      mark#(and(X1,X2)) -> mark#(X1) -> mark#(__(X1,X2)) -> mark#(X1)
      mark#(and(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)) -> mark#(X2) ->
      mark#(isNePal(X)) -> isNePal#(mark(X))
      mark#(__(X1,X2)) -> mark#(X2) -> mark#(isNePal(X)) -> mark#(X)
      mark#(__(X1,X2)) -> mark#(X2) ->
      mark#(and(X1,X2)) -> and#(mark(X1),X2)
      mark#(__(X1,X2)) -> mark#(X2) -> mark#(and(X1,X2)) -> mark#(X1)
      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)) -> isNePal#(mark(X))
      mark#(__(X1,X2)) -> mark#(X1) -> mark#(isNePal(X)) -> mark#(X)
      mark#(__(X1,X2)) -> mark#(X1) ->
      mark#(and(X1,X2)) -> and#(mark(X1),X2)
      mark#(__(X1,X2)) -> mark#(X1) -> mark#(and(X1,X2)) -> mark#(X1)
      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)
     SCC Processor:
      #sccs: 4
      #rules: 14
      #arcs: 74/289
      DPs:
       mark#(isNePal(X)) -> mark#(X)
       mark#(__(X1,X2)) -> mark#(X2)
       mark#(__(X1,X2)) -> mark#(X1)
       mark#(and(X1,X2)) -> mark#(X1)
      TRS:
       mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
       mark(nil()) -> active(nil())
       mark(and(X1,X2)) -> active(and(mark(X1),X2))
       mark(tt()) -> active(tt())
       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)
       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)
       isNePal(mark(X)) -> isNePal(X)
       isNePal(active(X)) -> isNePal(X)
      Subterm Criterion Processor:
       simple projection:
        pi(mark#) = 0
       problem:
        DPs:
         
        TRS:
         mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
         mark(nil()) -> active(nil())
         mark(and(X1,X2)) -> active(and(mark(X1),X2))
         mark(tt()) -> active(tt())
         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)
         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)
         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:
       mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
       mark(nil()) -> active(nil())
       mark(and(X1,X2)) -> active(and(mark(X1),X2))
       mark(tt()) -> active(tt())
       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)
       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)
       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:
         mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
         mark(nil()) -> active(nil())
         mark(and(X1,X2)) -> active(and(mark(X1),X2))
         mark(tt()) -> active(tt())
         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)
         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)
         isNePal(mark(X)) -> isNePal(X)
         isNePal(active(X)) -> isNePal(X)
       Subterm Criterion Processor:
        simple projection:
         pi(__#) = 0
        problem:
         DPs:
          
         TRS:
          mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
          mark(nil()) -> active(nil())
          mark(and(X1,X2)) -> active(and(mark(X1),X2))
          mark(tt()) -> active(tt())
          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)
          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)
          isNePal(mark(X)) -> isNePal(X)
          isNePal(active(X)) -> isNePal(X)
        Qed
      
      DPs:
       and#(mark(X1),X2) -> and#(X1,X2)
       and#(X1,mark(X2)) -> and#(X1,X2)
       and#(active(X1),X2) -> and#(X1,X2)
       and#(X1,active(X2)) -> and#(X1,X2)
      TRS:
       mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
       mark(nil()) -> active(nil())
       mark(and(X1,X2)) -> active(and(mark(X1),X2))
       mark(tt()) -> active(tt())
       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)
       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)
       isNePal(mark(X)) -> isNePal(X)
       isNePal(active(X)) -> isNePal(X)
      Subterm Criterion Processor:
       simple projection:
        pi(and#) = 1
       problem:
        DPs:
         and#(mark(X1),X2) -> and#(X1,X2)
         and#(active(X1),X2) -> and#(X1,X2)
        TRS:
         mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
         mark(nil()) -> active(nil())
         mark(and(X1,X2)) -> active(and(mark(X1),X2))
         mark(tt()) -> active(tt())
         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)
         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)
         isNePal(mark(X)) -> isNePal(X)
         isNePal(active(X)) -> isNePal(X)
       Subterm Criterion Processor:
        simple projection:
         pi(and#) = 0
        problem:
         DPs:
          
         TRS:
          mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
          mark(nil()) -> active(nil())
          mark(and(X1,X2)) -> active(and(mark(X1),X2))
          mark(tt()) -> active(tt())
          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)
          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)
          isNePal(mark(X)) -> isNePal(X)
          isNePal(active(X)) -> isNePal(X)
        Qed
      
      DPs:
       isNePal#(mark(X)) -> isNePal#(X)
       isNePal#(active(X)) -> isNePal#(X)
      TRS:
       mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
       mark(nil()) -> active(nil())
       mark(and(X1,X2)) -> active(and(mark(X1),X2))
       mark(tt()) -> active(tt())
       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)
       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)
       isNePal(mark(X)) -> isNePal(X)
       isNePal(active(X)) -> isNePal(X)
      Subterm Criterion Processor:
       simple projection:
        pi(isNePal#) = 0
       problem:
        DPs:
         
        TRS:
         mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
         mark(nil()) -> active(nil())
         mark(and(X1,X2)) -> active(and(mark(X1),X2))
         mark(tt()) -> active(tt())
         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)
         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)
         isNePal(mark(X)) -> isNePal(X)
         isNePal(active(X)) -> isNePal(X)
       Qed