Termination proof

1: switching to dependency pairs

a____#( __( X , Y ) , Z )	→	a____#( mark( X ) , a____( mark( Y ) , mark( Z ) ) )
a____#( __( X , Y ) , Z )	→	mark#( X )
a____#( __( X , Y ) , Z )	→	a____#( mark( Y ) , mark( Z ) )
a____#( __( X , Y ) , Z )	→	mark#( Y )
a____#( __( X , Y ) , Z )	→	mark#( Z )
a____#( X , nil )	→	mark#( X )
a____#( nil , X )	→	mark#( X )
a__U11#( tt , V )	→	a__U12#( a__isNeList( V ) )
a__U11#( tt , V )	→	a__isNeList#( V )
a__U21#( tt , V1 , V2 )	→	a__U22#( a__isList( V1 ) , V2 )
a__U21#( tt , V1 , V2 )	→	a__isList#( V1 )
a__U22#( tt , V2 )	→	a__U23#( a__isList( V2 ) )
a__U22#( tt , V2 )	→	a__isList#( V2 )
a__U31#( tt , V )	→	a__U32#( a__isQid( V ) )
a__U31#( tt , V )	→	a__isQid#( V )
a__U41#( tt , V1 , V2 )	→	a__U42#( a__isList( V1 ) , V2 )
a__U41#( tt , V1 , V2 )	→	a__isList#( V1 )
a__U42#( tt , V2 )	→	a__U43#( a__isNeList( V2 ) )
a__U42#( tt , V2 )	→	a__isNeList#( V2 )
a__U51#( tt , V1 , V2 )	→	a__U52#( a__isNeList( V1 ) , V2 )
a__U51#( tt , V1 , V2 )	→	a__isNeList#( V1 )
a__U52#( tt , V2 )	→	a__U53#( a__isList( V2 ) )
a__U52#( tt , V2 )	→	a__isList#( V2 )
a__U61#( tt , V )	→	a__U62#( a__isQid( V ) )
a__U61#( tt , V )	→	a__isQid#( V )
a__U71#( tt , V )	→	a__U72#( a__isNePal( V ) )
a__U71#( tt , V )	→	a__isNePal#( V )
a__and#( tt , X )	→	mark#( X )
a__isList#( V )	→	a__U11#( a__isPalListKind( V ) , V )
a__isList#( V )	→	a__isPalListKind#( V )
a__isList#( __( V1 , V2 ) )	→	a__U21#( a__and( a__isPalListKind( V1 ) , isPalListKind( V2 ) ) , V1 , V2 )
a__isList#( __( V1 , V2 ) )	→	a__and#( a__isPalListKind( V1 ) , isPalListKind( V2 ) )
a__isList#( __( V1 , V2 ) )	→	a__isPalListKind#( V1 )
a__isNeList#( V )	→	a__U31#( a__isPalListKind( V ) , V )
a__isNeList#( V )	→	a__isPalListKind#( V )
a__isNeList#( __( V1 , V2 ) )	→	a__U41#( a__and( a__isPalListKind( V1 ) , isPalListKind( V2 ) ) , V1 , V2 )
a__isNeList#( __( V1 , V2 ) )	→	a__and#( a__isPalListKind( V1 ) , isPalListKind( V2 ) )
a__isNeList#( __( V1 , V2 ) )	→	a__isPalListKind#( V1 )
a__isNeList#( __( V1 , V2 ) )	→	a__U51#( a__and( a__isPalListKind( V1 ) , isPalListKind( V2 ) ) , V1 , V2 )
a__isNeList#( __( V1 , V2 ) )	→	a__and#( a__isPalListKind( V1 ) , isPalListKind( V2 ) )
a__isNeList#( __( V1 , V2 ) )	→	a__isPalListKind#( V1 )
a__isNePal#( V )	→	a__U61#( a__isPalListKind( V ) , V )
a__isNePal#( V )	→	a__isPalListKind#( V )
a__isNePal#( __( I , __( P , I ) ) )	→	a__and#( a__and( a__isQid( I ) , isPalListKind( I ) ) , and( isPal( P ) , isPalListKind( P ) ) )
a__isNePal#( __( I , __( P , I ) ) )	→	a__and#( a__isQid( I ) , isPalListKind( I ) )
a__isNePal#( __( I , __( P , I ) ) )	→	a__isQid#( I )
a__isPal#( V )	→	a__U71#( a__isPalListKind( V ) , V )
a__isPal#( V )	→	a__isPalListKind#( V )
a__isPalListKind#( __( V1 , V2 ) )	→	a__and#( a__isPalListKind( V1 ) , isPalListKind( V2 ) )
a__isPalListKind#( __( V1 , V2 ) )	→	a__isPalListKind#( V1 )
mark#( __( X1 , X2 ) )	→	a____#( mark( X1 ) , mark( X2 ) )
mark#( __( X1 , X2 ) )	→	mark#( X1 )
mark#( __( X1 , X2 ) )	→	mark#( X2 )
mark#( U11( X1 , X2 ) )	→	a__U11#( mark( X1 ) , X2 )
mark#( U11( X1 , X2 ) )	→	mark#( X1 )
mark#( U12( X ) )	→	a__U12#( mark( X ) )
mark#( U12( X ) )	→	mark#( X )
mark#( isNeList( X ) )	→	a__isNeList#( X )
mark#( U21( X1 , X2 , X3 ) )	→	a__U21#( mark( X1 ) , X2 , X3 )
mark#( U21( X1 , X2 , X3 ) )	→	mark#( X1 )
mark#( U22( X1 , X2 ) )	→	a__U22#( mark( X1 ) , X2 )
mark#( U22( X1 , X2 ) )	→	mark#( X1 )
mark#( isList( X ) )	→	a__isList#( X )
mark#( U23( X ) )	→	a__U23#( mark( X ) )
mark#( U23( X ) )	→	mark#( X )
mark#( U31( X1 , X2 ) )	→	a__U31#( mark( X1 ) , X2 )
mark#( U31( X1 , X2 ) )	→	mark#( X1 )
mark#( U32( X ) )	→	a__U32#( mark( X ) )
mark#( U32( X ) )	→	mark#( X )
mark#( isQid( X ) )	→	a__isQid#( X )
mark#( U41( X1 , X2 , X3 ) )	→	a__U41#( mark( X1 ) , X2 , X3 )
mark#( U41( X1 , X2 , X3 ) )	→	mark#( X1 )
mark#( U42( X1 , X2 ) )	→	a__U42#( mark( X1 ) , X2 )
mark#( U42( X1 , X2 ) )	→	mark#( X1 )
mark#( U43( X ) )	→	a__U43#( mark( X ) )
mark#( U43( X ) )	→	mark#( X )
mark#( U51( X1 , X2 , X3 ) )	→	a__U51#( mark( X1 ) , X2 , X3 )
mark#( U51( X1 , X2 , X3 ) )	→	mark#( X1 )
mark#( U52( X1 , X2 ) )	→	a__U52#( mark( X1 ) , X2 )
mark#( U52( X1 , X2 ) )	→	mark#( X1 )
mark#( U53( X ) )	→	a__U53#( mark( X ) )
mark#( U53( X ) )	→	mark#( X )
mark#( U61( X1 , X2 ) )	→	a__U61#( mark( X1 ) , X2 )
mark#( U61( X1 , X2 ) )	→	mark#( X1 )
mark#( U62( X ) )	→	a__U62#( mark( X ) )
mark#( U62( X ) )	→	mark#( X )
mark#( U71( X1 , X2 ) )	→	a__U71#( mark( X1 ) , X2 )
mark#( U71( X1 , X2 ) )	→	mark#( X1 )
mark#( U72( X ) )	→	a__U72#( mark( X ) )
mark#( U72( X ) )	→	mark#( X )
mark#( isNePal( X ) )	→	a__isNePal#( X )
mark#( and( X1 , X2 ) )	→	a__and#( mark( X1 ) , X2 )
mark#( and( X1 , X2 ) )	→	mark#( X1 )
mark#( isPalListKind( X ) )	→	a__isPalListKind#( X )
mark#( isPal( X ) )	→	a__isPal#( X )

1.1: dependency graph processor

The dependency pairs are split into 1 component(s).

• The 1st component contains the pair(s)

  a____#( __( X , Y ) , Z )	→	mark#( X )
  mark#( __( X1 , X2 ) )	→	a____#( mark( X1 ) , mark( X2 ) )
  a____#( __( X , Y ) , Z )	→	a____#( mark( X ) , a____( mark( Y ) , mark( Z ) ) )
  a____#( __( X , Y ) , Z )	→	a____#( mark( Y ) , mark( Z ) )
  a____#( __( X , Y ) , Z )	→	mark#( Y )
  mark#( __( X1 , X2 ) )	→	mark#( X1 )
  mark#( __( X1 , X2 ) )	→	mark#( X2 )
  mark#( U11( X1 , X2 ) )	→	a__U11#( mark( X1 ) , X2 )
  a__U11#( tt , V )	→	a__isNeList#( V )
  a__isNeList#( V )	→	a__isPalListKind#( V )
  a__isPalListKind#( __( V1 , V2 ) )	→	a__and#( a__isPalListKind( V1 ) , isPalListKind( V2 ) )
  a__and#( tt , X )	→	mark#( X )
  mark#( U11( X1 , X2 ) )	→	mark#( X1 )
  mark#( U12( X ) )	→	mark#( X )
  mark#( isNeList( X ) )	→	a__isNeList#( X )
  a__isNeList#( __( V1 , V2 ) )	→	a__U41#( a__and( a__isPalListKind( V1 ) , isPalListKind( V2 ) ) , V1 , V2 )
  a__U41#( tt , V1 , V2 )	→	a__U42#( a__isList( V1 ) , V2 )
  a__U42#( tt , V2 )	→	a__isNeList#( V2 )
  a__isNeList#( __( V1 , V2 ) )	→	a__and#( a__isPalListKind( V1 ) , isPalListKind( V2 ) )
  a__isNeList#( __( V1 , V2 ) )	→	a__isPalListKind#( V1 )
  a__isPalListKind#( __( V1 , V2 ) )	→	a__isPalListKind#( V1 )
  a__isNeList#( __( V1 , V2 ) )	→	a__U51#( a__and( a__isPalListKind( V1 ) , isPalListKind( V2 ) ) , V1 , V2 )
  a__U51#( tt , V1 , V2 )	→	a__U52#( a__isNeList( V1 ) , V2 )
  a__U52#( tt , V2 )	→	a__isList#( V2 )
  a__isList#( V )	→	a__U11#( a__isPalListKind( V ) , V )
  a__isList#( V )	→	a__isPalListKind#( V )
  a__isList#( __( V1 , V2 ) )	→	a__U21#( a__and( a__isPalListKind( V1 ) , isPalListKind( V2 ) ) , V1 , V2 )
  a__U21#( tt , V1 , V2 )	→	a__U22#( a__isList( V1 ) , V2 )
  a__U22#( tt , V2 )	→	a__isList#( V2 )
  a__isList#( __( V1 , V2 ) )	→	a__and#( a__isPalListKind( V1 ) , isPalListKind( V2 ) )
  a__isList#( __( V1 , V2 ) )	→	a__isPalListKind#( V1 )
  a__U21#( tt , V1 , V2 )	→	a__isList#( V1 )
  a__U51#( tt , V1 , V2 )	→	a__isNeList#( V1 )
  a__U41#( tt , V1 , V2 )	→	a__isList#( V1 )
  mark#( U21( X1 , X2 , X3 ) )	→	a__U21#( mark( X1 ) , X2 , X3 )
  mark#( U21( X1 , X2 , X3 ) )	→	mark#( X1 )
  mark#( U22( X1 , X2 ) )	→	a__U22#( mark( X1 ) , X2 )
  mark#( U22( X1 , X2 ) )	→	mark#( X1 )
  mark#( isList( X ) )	→	a__isList#( X )
  mark#( U23( X ) )	→	mark#( X )
  mark#( U31( X1 , X2 ) )	→	mark#( X1 )
  mark#( U32( X ) )	→	mark#( X )
  mark#( U41( X1 , X2 , X3 ) )	→	a__U41#( mark( X1 ) , X2 , X3 )
  mark#( U41( X1 , X2 , X3 ) )	→	mark#( X1 )
  mark#( U42( X1 , X2 ) )	→	a__U42#( mark( X1 ) , X2 )
  mark#( U42( X1 , X2 ) )	→	mark#( X1 )
  mark#( U43( X ) )	→	mark#( X )
  mark#( U51( X1 , X2 , X3 ) )	→	a__U51#( mark( X1 ) , X2 , X3 )
  mark#( U51( X1 , X2 , X3 ) )	→	mark#( X1 )
  mark#( U52( X1 , X2 ) )	→	a__U52#( mark( X1 ) , X2 )
  mark#( U52( X1 , X2 ) )	→	mark#( X1 )
  mark#( U53( X ) )	→	mark#( X )
  mark#( U61( X1 , X2 ) )	→	mark#( X1 )
  mark#( U62( X ) )	→	mark#( X )
  mark#( U71( X1 , X2 ) )	→	a__U71#( mark( X1 ) , X2 )
  a__U71#( tt , V )	→	a__isNePal#( V )
  a__isNePal#( V )	→	a__isPalListKind#( V )
  a__isNePal#( __( I , __( P , I ) ) )	→	a__and#( a__and( a__isQid( I ) , isPalListKind( I ) ) , and( isPal( P ) , isPalListKind( P ) ) )
  a__isNePal#( __( I , __( P , I ) ) )	→	a__and#( a__isQid( I ) , isPalListKind( I ) )
  mark#( U71( X1 , X2 ) )	→	mark#( X1 )
  mark#( U72( X ) )	→	mark#( X )
  mark#( isNePal( X ) )	→	a__isNePal#( X )
  mark#( and( X1 , X2 ) )	→	a__and#( mark( X1 ) , X2 )
  mark#( and( X1 , X2 ) )	→	mark#( X1 )
  mark#( isPalListKind( X ) )	→	a__isPalListKind#( X )
  mark#( isPal( X ) )	→	a__isPal#( X )
  a__isPal#( V )	→	a__U71#( a__isPalListKind( V ) , V )
  a__isPal#( V )	→	a__isPalListKind#( V )
  a____#( __( X , Y ) , Z )	→	mark#( Z )
  a____#( X , nil )	→	mark#( X )
  a____#( nil , X )	→	mark#( X )

  1.1.1: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [a]	=	0
  [__ (x1, x2) ]	=	x1 + x2
  [isNePal (x1) ]	=	0
  [a__U21# (x1, x2, x3) ]	=	1
  [U21 (x1, x2, x3) ]	=	x1
  [U41 (x1, x2, x3) ]	=	x1
  [i]	=	3
  [a__U22# (x1, x2) ]	=	1
  [U72 (x1) ]	=	2 x1
  [a__isPal# (x1) ]	=	1
  [U31 (x1, x2) ]	=	x1
  [U61 (x1, x2) ]	=	x1
  [and (x1, x2) ]	=	2 x1 + 2 x2
  [U71 (x1, x2) ]	=	2 x1
  [a__isNeList# (x1) ]	=	1
  [isNeList (x1) ]	=	0
  [a__U23 (x1) ]	=	x1
  [a__U42# (x1, x2) ]	=	1
  [a__isPal (x1) ]	=	0
  [a__U11# (x1, x2) ]	=	1
  [isPal (x1) ]	=	0
  [a__U52# (x1, x2) ]	=	1
  [a____# (x1, x2) ]	=	x1 + x2 + 1
  [a__U72 (x1) ]	=	2 x1
  [mark# (x1) ]	=	x1 + 1
  [a__U71 (x1, x2) ]	=	2 x1
  [tt]	=	0
  [o]	=	1
  [a__and (x1, x2) ]	=	2 x1 + 2 x2
  [e]	=	0
  [a__U22 (x1, x2) ]	=	x1
  [a__U21 (x1, x2, x3) ]	=	x1
  [a__isNePal (x1) ]	=	0
  [a__U32 (x1) ]	=	x1
  [a__U41# (x1, x2, x3) ]	=	1
  [U23 (x1) ]	=	x1
  [U51 (x1, x2, x3) ]	=	2 x1
  [U53 (x1) ]	=	x1
  [a__U41 (x1, x2, x3) ]	=	x1
  [a__isQid (x1) ]	=	0
  [a____ (x1, x2) ]	=	x1 + x2
  [U62 (x1) ]	=	x1
  [a__U62 (x1) ]	=	x1
  [a__isPalListKind# (x1) ]	=	1
  [a__U53 (x1) ]	=	x1
  [a__U42 (x1, x2) ]	=	2 x1
  [a__U31 (x1, x2) ]	=	x1
  [u]	=	0
  [U22 (x1, x2) ]	=	x1
  [U32 (x1) ]	=	x1
  [a__U61 (x1, x2) ]	=	x1
  [isList (x1) ]	=	0
  [a__U11 (x1, x2) ]	=	2 x1
  [mark (x1) ]	=	x1
  [a__isList# (x1) ]	=	1
  [a__U52 (x1, x2) ]	=	x1
  [a__isPalListKind (x1) ]	=	0
  [U52 (x1, x2) ]	=	x1
  [a__and# (x1, x2) ]	=	x1 + 1
  [nil]	=	2
  [U42 (x1, x2) ]	=	2 x1
  [a__isNeList (x1) ]	=	0
  [isPalListKind (x1) ]	=	0
  [a__U51 (x1, x2, x3) ]	=	2 x1
  [U11 (x1, x2) ]	=	2 x1
  [a__isNePal# (x1) ]	=	1
  [a__U51# (x1, x2, x3) ]	=	2 x1 + 1
  [a__U71# (x1, x2) ]	=	1
  [isQid (x1) ]	=	0
  [a__isList (x1) ]	=	0
  [a__U12 (x1) ]	=	2 x1
  [U43 (x1) ]	=	2 x1
  [a__U43 (x1) ]	=	2 x1
  [U12 (x1) ]	=	2 x1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  a____#( __( X , Y ) , Z )	→	mark#( X )
  mark#( __( X1 , X2 ) )	→	a____#( mark( X1 ) , mark( X2 ) )
  a____#( __( X , Y ) , Z )	→	a____#( mark( X ) , a____( mark( Y ) , mark( Z ) ) )
  a____#( __( X , Y ) , Z )	→	a____#( mark( Y ) , mark( Z ) )
  a____#( __( X , Y ) , Z )	→	mark#( Y )
  mark#( __( X1 , X2 ) )	→	mark#( X1 )
  mark#( __( X1 , X2 ) )	→	mark#( X2 )
  mark#( U11( X1 , X2 ) )	→	a__U11#( mark( X1 ) , X2 )
  a__U11#( tt , V )	→	a__isNeList#( V )
  a__isNeList#( V )	→	a__isPalListKind#( V )
  a__isPalListKind#( __( V1 , V2 ) )	→	a__and#( a__isPalListKind( V1 ) , isPalListKind( V2 ) )
  a__and#( tt , X )	→	mark#( X )
  mark#( U11( X1 , X2 ) )	→	mark#( X1 )
  mark#( U12( X ) )	→	mark#( X )
  mark#( isNeList( X ) )	→	a__isNeList#( X )
  a__isNeList#( __( V1 , V2 ) )	→	a__U41#( a__and( a__isPalListKind( V1 ) , isPalListKind( V2 ) ) , V1 , V2 )
  a__U41#( tt , V1 , V2 )	→	a__U42#( a__isList( V1 ) , V2 )
  a__U42#( tt , V2 )	→	a__isNeList#( V2 )
  a__isNeList#( __( V1 , V2 ) )	→	a__and#( a__isPalListKind( V1 ) , isPalListKind( V2 ) )
  a__isNeList#( __( V1 , V2 ) )	→	a__isPalListKind#( V1 )
  a__isPalListKind#( __( V1 , V2 ) )	→	a__isPalListKind#( V1 )
  a__isNeList#( __( V1 , V2 ) )	→	a__U51#( a__and( a__isPalListKind( V1 ) , isPalListKind( V2 ) ) , V1 , V2 )
  a__U51#( tt , V1 , V2 )	→	a__U52#( a__isNeList( V1 ) , V2 )
  a__U52#( tt , V2 )	→	a__isList#( V2 )
  a__isList#( V )	→	a__U11#( a__isPalListKind( V ) , V )
  a__isList#( V )	→	a__isPalListKind#( V )
  a__isList#( __( V1 , V2 ) )	→	a__U21#( a__and( a__isPalListKind( V1 ) , isPalListKind( V2 ) ) , V1 , V2 )
  a__U21#( tt , V1 , V2 )	→	a__U22#( a__isList( V1 ) , V2 )
  a__U22#( tt , V2 )	→	a__isList#( V2 )
  a__isList#( __( V1 , V2 ) )	→	a__and#( a__isPalListKind( V1 ) , isPalListKind( V2 ) )
  a__isList#( __( V1 , V2 ) )	→	a__isPalListKind#( V1 )
  a__U21#( tt , V1 , V2 )	→	a__isList#( V1 )
  a__U51#( tt , V1 , V2 )	→	a__isNeList#( V1 )
  a__U41#( tt , V1 , V2 )	→	a__isList#( V1 )
  mark#( U21( X1 , X2 , X3 ) )	→	a__U21#( mark( X1 ) , X2 , X3 )
  mark#( U21( X1 , X2 , X3 ) )	→	mark#( X1 )
  mark#( U22( X1 , X2 ) )	→	a__U22#( mark( X1 ) , X2 )
  mark#( U22( X1 , X2 ) )	→	mark#( X1 )
  mark#( isList( X ) )	→	a__isList#( X )
  mark#( U23( X ) )	→	mark#( X )
  mark#( U31( X1 , X2 ) )	→	mark#( X1 )
  mark#( U32( X ) )	→	mark#( X )
  mark#( U41( X1 , X2 , X3 ) )	→	a__U41#( mark( X1 ) , X2 , X3 )
  mark#( U41( X1 , X2 , X3 ) )	→	mark#( X1 )
  mark#( U42( X1 , X2 ) )	→	a__U42#( mark( X1 ) , X2 )
  mark#( U42( X1 , X2 ) )	→	mark#( X1 )
  mark#( U43( X ) )	→	mark#( X )
  mark#( U51( X1 , X2 , X3 ) )	→	a__U51#( mark( X1 ) , X2 , X3 )
  mark#( U51( X1 , X2 , X3 ) )	→	mark#( X1 )
  mark#( U52( X1 , X2 ) )	→	a__U52#( mark( X1 ) , X2 )
  mark#( U52( X1 , X2 ) )	→	mark#( X1 )
  mark#( U53( X ) )	→	mark#( X )
  mark#( U61( X1 , X2 ) )	→	mark#( X1 )
  mark#( U62( X ) )	→	mark#( X )
  mark#( U71( X1 , X2 ) )	→	a__U71#( mark( X1 ) , X2 )
  a__U71#( tt , V )	→	a__isNePal#( V )
  a__isNePal#( V )	→	a__isPalListKind#( V )
  a__isNePal#( __( I , __( P , I ) ) )	→	a__and#( a__and( a__isQid( I ) , isPalListKind( I ) ) , and( isPal( P ) , isPalListKind( P ) ) )
  a__isNePal#( __( I , __( P , I ) ) )	→	a__and#( a__isQid( I ) , isPalListKind( I ) )
  mark#( U71( X1 , X2 ) )	→	mark#( X1 )
  mark#( U72( X ) )	→	mark#( X )
  mark#( isNePal( X ) )	→	a__isNePal#( X )
  mark#( and( X1 , X2 ) )	→	a__and#( mark( X1 ) , X2 )
  mark#( and( X1 , X2 ) )	→	mark#( X1 )
  mark#( isPalListKind( X ) )	→	a__isPalListKind#( X )
  mark#( isPal( X ) )	→	a__isPal#( X )
  a__isPal#( V )	→	a__U71#( a__isPalListKind( V ) , V )
  a__isPal#( V )	→	a__isPalListKind#( V )
  a____#( __( X , Y ) , Z )	→	mark#( Z )

  1.1.1.1: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [a]	=	0
  [__ (x1, x2) ]	=	2 x1 + x2 + 2
  [isNePal (x1) ]	=	0
  [a__U21# (x1, x2, x3) ]	=	0
  [U21 (x1, x2, x3) ]	=	2 x1
  [U41 (x1, x2, x3) ]	=	2 x1
  [i]	=	0
  [a__U22# (x1, x2) ]	=	0
  [U72 (x1) ]	=	2 x1
  [a__isPal# (x1) ]	=	0
  [U31 (x1, x2) ]	=	x1
  [U61 (x1, x2) ]	=	2 x1
  [and (x1, x2) ]	=	2 x1 + 2 x2
  [U71 (x1, x2) ]	=	x1
  [a__isNeList# (x1) ]	=	0
  [isNeList (x1) ]	=	0
  [a__U23 (x1) ]	=	2 x1
  [a__U42# (x1, x2) ]	=	0
  [a__isPal (x1) ]	=	0
  [a__U11# (x1, x2) ]	=	0
  [isPal (x1) ]	=	0
  [a__U52# (x1, x2) ]	=	x1
  [a____# (x1, x2) ]	=	2 x1 + x2
  [a__U72 (x1) ]	=	2 x1
  [mark# (x1) ]	=	x1
  [a__U71 (x1, x2) ]	=	x1
  [tt]	=	0
  [o]	=	0
  [a__and (x1, x2) ]	=	2 x1 + 2 x2
  [e]	=	0
  [a__U22 (x1, x2) ]	=	x1
  [a__U21 (x1, x2, x3) ]	=	2 x1
  [a__isNePal (x1) ]	=	0
  [a__U32 (x1) ]	=	2 x1
  [a__U41# (x1, x2, x3) ]	=	2 x1
  [U23 (x1) ]	=	2 x1
  [U51 (x1, x2, x3) ]	=	2 x1
  [U53 (x1) ]	=	2 x1
  [a__U41 (x1, x2, x3) ]	=	2 x1
  [a__isQid (x1) ]	=	0
  [a____ (x1, x2) ]	=	2 x1 + x2 + 2
  [U62 (x1) ]	=	x1
  [a__U62 (x1) ]	=	x1
  [a__isPalListKind# (x1) ]	=	0
  [a__U53 (x1) ]	=	2 x1
  [a__U42 (x1, x2) ]	=	x1
  [a__U31 (x1, x2) ]	=	x1
  [u]	=	1
  [U22 (x1, x2) ]	=	x1
  [U32 (x1) ]	=	2 x1
  [a__U61 (x1, x2) ]	=	2 x1
  [isList (x1) ]	=	0
  [a__U11 (x1, x2) ]	=	x1
  [mark (x1) ]	=	x1
  [a__isList# (x1) ]	=	0
  [a__U52 (x1, x2) ]	=	x1
  [a__isPalListKind (x1) ]	=	0
  [U52 (x1, x2) ]	=	x1
  [a__and# (x1, x2) ]	=	2 x1
  [nil]	=	0
  [U42 (x1, x2) ]	=	x1
  [a__isNeList (x1) ]	=	0
  [isPalListKind (x1) ]	=	0
  [a__U51 (x1, x2, x3) ]	=	2 x1
  [U11 (x1, x2) ]	=	x1
  [a__isNePal# (x1) ]	=	0
  [a__U51# (x1, x2, x3) ]	=	0
  [a__U71# (x1, x2) ]	=	0
  [isQid (x1) ]	=	0
  [a__isList (x1) ]	=	0
  [a__U12 (x1) ]	=	2 x1
  [U43 (x1) ]	=	x1
  [a__U43 (x1) ]	=	x1
  [U12 (x1) ]	=	2 x1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  mark#( U11( X1 , X2 ) )	→	a__U11#( mark( X1 ) , X2 )
  a__U11#( tt , V )	→	a__isNeList#( V )
  a__isNeList#( V )	→	a__isPalListKind#( V )
  a__isPalListKind#( __( V1 , V2 ) )	→	a__and#( a__isPalListKind( V1 ) , isPalListKind( V2 ) )
  a__and#( tt , X )	→	mark#( X )
  mark#( U11( X1 , X2 ) )	→	mark#( X1 )
  mark#( U12( X ) )	→	mark#( X )
  mark#( isNeList( X ) )	→	a__isNeList#( X )
  a__isNeList#( __( V1 , V2 ) )	→	a__U41#( a__and( a__isPalListKind( V1 ) , isPalListKind( V2 ) ) , V1 , V2 )
  a__U41#( tt , V1 , V2 )	→	a__U42#( a__isList( V1 ) , V2 )
  a__U42#( tt , V2 )	→	a__isNeList#( V2 )
  a__isNeList#( __( V1 , V2 ) )	→	a__and#( a__isPalListKind( V1 ) , isPalListKind( V2 ) )
  a__isNeList#( __( V1 , V2 ) )	→	a__isPalListKind#( V1 )
  a__isPalListKind#( __( V1 , V2 ) )	→	a__isPalListKind#( V1 )
  a__isNeList#( __( V1 , V2 ) )	→	a__U51#( a__and( a__isPalListKind( V1 ) , isPalListKind( V2 ) ) , V1 , V2 )
  a__U51#( tt , V1 , V2 )	→	a__U52#( a__isNeList( V1 ) , V2 )
  a__U52#( tt , V2 )	→	a__isList#( V2 )
  a__isList#( V )	→	a__U11#( a__isPalListKind( V ) , V )
  a__isList#( V )	→	a__isPalListKind#( V )
  a__isList#( __( V1 , V2 ) )	→	a__U21#( a__and( a__isPalListKind( V1 ) , isPalListKind( V2 ) ) , V1 , V2 )
  a__U21#( tt , V1 , V2 )	→	a__U22#( a__isList( V1 ) , V2 )
  a__U22#( tt , V2 )	→	a__isList#( V2 )
  a__isList#( __( V1 , V2 ) )	→	a__and#( a__isPalListKind( V1 ) , isPalListKind( V2 ) )
  a__isList#( __( V1 , V2 ) )	→	a__isPalListKind#( V1 )
  a__U21#( tt , V1 , V2 )	→	a__isList#( V1 )
  a__U51#( tt , V1 , V2 )	→	a__isNeList#( V1 )
  a__U41#( tt , V1 , V2 )	→	a__isList#( V1 )
  mark#( U21( X1 , X2 , X3 ) )	→	a__U21#( mark( X1 ) , X2 , X3 )
  mark#( U21( X1 , X2 , X3 ) )	→	mark#( X1 )
  mark#( U22( X1 , X2 ) )	→	a__U22#( mark( X1 ) , X2 )
  mark#( U22( X1 , X2 ) )	→	mark#( X1 )
  mark#( isList( X ) )	→	a__isList#( X )
  mark#( U23( X ) )	→	mark#( X )
  mark#( U31( X1 , X2 ) )	→	mark#( X1 )
  mark#( U32( X ) )	→	mark#( X )
  mark#( U41( X1 , X2 , X3 ) )	→	a__U41#( mark( X1 ) , X2 , X3 )
  mark#( U41( X1 , X2 , X3 ) )	→	mark#( X1 )
  mark#( U42( X1 , X2 ) )	→	a__U42#( mark( X1 ) , X2 )
  mark#( U42( X1 , X2 ) )	→	mark#( X1 )
  mark#( U43( X ) )	→	mark#( X )
  mark#( U51( X1 , X2 , X3 ) )	→	a__U51#( mark( X1 ) , X2 , X3 )
  mark#( U51( X1 , X2 , X3 ) )	→	mark#( X1 )
  mark#( U52( X1 , X2 ) )	→	a__U52#( mark( X1 ) , X2 )
  mark#( U52( X1 , X2 ) )	→	mark#( X1 )
  mark#( U53( X ) )	→	mark#( X )
  mark#( U61( X1 , X2 ) )	→	mark#( X1 )
  mark#( U62( X ) )	→	mark#( X )
  mark#( U71( X1 , X2 ) )	→	a__U71#( mark( X1 ) , X2 )
  a__U71#( tt , V )	→	a__isNePal#( V )
  a__isNePal#( V )	→	a__isPalListKind#( V )
  a__isNePal#( __( I , __( P , I ) ) )	→	a__and#( a__and( a__isQid( I ) , isPalListKind( I ) ) , and( isPal( P ) , isPalListKind( P ) ) )
  a__isNePal#( __( I , __( P , I ) ) )	→	a__and#( a__isQid( I ) , isPalListKind( I ) )
  mark#( U71( X1 , X2 ) )	→	mark#( X1 )
  mark#( U72( X ) )	→	mark#( X )
  mark#( isNePal( X ) )	→	a__isNePal#( X )
  mark#( and( X1 , X2 ) )	→	a__and#( mark( X1 ) , X2 )
  mark#( and( X1 , X2 ) )	→	mark#( X1 )
  mark#( isPalListKind( X ) )	→	a__isPalListKind#( X )
  mark#( isPal( X ) )	→	a__isPal#( X )
  a__isPal#( V )	→	a__U71#( a__isPalListKind( V ) , V )
  a__isPal#( V )	→	a__isPalListKind#( V )

  1.1.1.1.1: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [a]	=	0
  [__ (x1, x2) ]	=	2 x1 + x2 + 2
  [isNePal (x1) ]	=	x1
  [a__U21# (x1, x2, x3) ]	=	2 x1
  [U21 (x1, x2, x3) ]	=	2 x1
  [U41 (x1, x2, x3) ]	=	2 x1
  [i]	=	1
  [a__U22# (x1, x2) ]	=	0
  [U72 (x1) ]	=	x1 + 2
  [a__isPal# (x1) ]	=	2 x1 + 3
  [U31 (x1, x2) ]	=	x1
  [U61 (x1, x2) ]	=	x1 + x2
  [and (x1, x2) ]	=	2 x1 + x2
  [U71 (x1, x2) ]	=	x1 + x2 + 2
  [a__isNeList# (x1) ]	=	0
  [isNeList (x1) ]	=	0
  [a__U23 (x1) ]	=	2 x1
  [a__U42# (x1, x2) ]	=	0
  [a__isPal (x1) ]	=	x1 + 2
  [a__U11# (x1, x2) ]	=	0
  [isPal (x1) ]	=	x1 + 2
  [a__U52# (x1, x2) ]	=	0
  [a__U72 (x1) ]	=	x1 + 2
  [mark# (x1) ]	=	2 x1
  [a__U71 (x1, x2) ]	=	x1 + x2 + 2
  [tt]	=	0
  [o]	=	0
  [a__and (x1, x2) ]	=	2 x1 + x2
  [e]	=	0
  [a__U22 (x1, x2) ]	=	2 x1
  [a__U21 (x1, x2, x3) ]	=	2 x1
  [a__isNePal (x1) ]	=	x1
  [a__U32 (x1) ]	=	x1
  [a__U41# (x1, x2, x3) ]	=	0
  [U23 (x1) ]	=	2 x1
  [U51 (x1, x2, x3) ]	=	x1
  [U53 (x1) ]	=	2 x1
  [a__U41 (x1, x2, x3) ]	=	2 x1
  [a__isQid (x1) ]	=	0
  [a____ (x1, x2) ]	=	2 x1 + x2 + 2
  [U62 (x1) ]	=	x1
  [a__U62 (x1) ]	=	x1
  [a__isPalListKind# (x1) ]	=	0
  [a__U53 (x1) ]	=	2 x1
  [a__U42 (x1, x2) ]	=	2 x1
  [a__U31 (x1, x2) ]	=	x1
  [u]	=	0
  [U22 (x1, x2) ]	=	2 x1
  [U32 (x1) ]	=	x1
  [a__U61 (x1, x2) ]	=	x1 + x2
  [isList (x1) ]	=	0
  [a__U11 (x1, x2) ]	=	x1
  [mark (x1) ]	=	x1
  [a__isList# (x1) ]	=	0
  [a__U52 (x1, x2) ]	=	2 x1
  [a__isPalListKind (x1) ]	=	0
  [U52 (x1, x2) ]	=	2 x1
  [a__and# (x1, x2) ]	=	2 x1
  [nil]	=	1
  [U42 (x1, x2) ]	=	2 x1
  [a__isNeList (x1) ]	=	0
  [isPalListKind (x1) ]	=	0
  [a__U51 (x1, x2, x3) ]	=	x1
  [U11 (x1, x2) ]	=	x1
  [a__isNePal# (x1) ]	=	2 x1
  [a__U51# (x1, x2, x3) ]	=	0
  [a__U71# (x1, x2) ]	=	2 x1 + 2
  [isQid (x1) ]	=	0
  [a__isList (x1) ]	=	0
  [a__U12 (x1) ]	=	2 x1
  [U43 (x1) ]	=	2 x1
  [a__U43 (x1) ]	=	2 x1
  [U12 (x1) ]	=	2 x1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  mark#( U11( X1 , X2 ) )	→	a__U11#( mark( X1 ) , X2 )
  a__U11#( tt , V )	→	a__isNeList#( V )
  a__isNeList#( V )	→	a__isPalListKind#( V )
  a__isPalListKind#( __( V1 , V2 ) )	→	a__and#( a__isPalListKind( V1 ) , isPalListKind( V2 ) )
  a__and#( tt , X )	→	mark#( X )
  mark#( U11( X1 , X2 ) )	→	mark#( X1 )
  mark#( U12( X ) )	→	mark#( X )
  mark#( isNeList( X ) )	→	a__isNeList#( X )
  a__isNeList#( __( V1 , V2 ) )	→	a__U41#( a__and( a__isPalListKind( V1 ) , isPalListKind( V2 ) ) , V1 , V2 )
  a__U41#( tt , V1 , V2 )	→	a__U42#( a__isList( V1 ) , V2 )
  a__U42#( tt , V2 )	→	a__isNeList#( V2 )
  a__isNeList#( __( V1 , V2 ) )	→	a__and#( a__isPalListKind( V1 ) , isPalListKind( V2 ) )
  a__isNeList#( __( V1 , V2 ) )	→	a__isPalListKind#( V1 )
  a__isPalListKind#( __( V1 , V2 ) )	→	a__isPalListKind#( V1 )
  a__isNeList#( __( V1 , V2 ) )	→	a__U51#( a__and( a__isPalListKind( V1 ) , isPalListKind( V2 ) ) , V1 , V2 )
  a__U51#( tt , V1 , V2 )	→	a__U52#( a__isNeList( V1 ) , V2 )
  a__U52#( tt , V2 )	→	a__isList#( V2 )
  a__isList#( V )	→	a__U11#( a__isPalListKind( V ) , V )
  a__isList#( V )	→	a__isPalListKind#( V )
  a__isList#( __( V1 , V2 ) )	→	a__U21#( a__and( a__isPalListKind( V1 ) , isPalListKind( V2 ) ) , V1 , V2 )
  a__U21#( tt , V1 , V2 )	→	a__U22#( a__isList( V1 ) , V2 )
  a__U22#( tt , V2 )	→	a__isList#( V2 )
  a__isList#( __( V1 , V2 ) )	→	a__and#( a__isPalListKind( V1 ) , isPalListKind( V2 ) )
  a__isList#( __( V1 , V2 ) )	→	a__isPalListKind#( V1 )
  a__U21#( tt , V1 , V2 )	→	a__isList#( V1 )
  a__U51#( tt , V1 , V2 )	→	a__isNeList#( V1 )
  a__U41#( tt , V1 , V2 )	→	a__isList#( V1 )
  mark#( U21( X1 , X2 , X3 ) )	→	a__U21#( mark( X1 ) , X2 , X3 )
  mark#( U21( X1 , X2 , X3 ) )	→	mark#( X1 )
  mark#( U22( X1 , X2 ) )	→	a__U22#( mark( X1 ) , X2 )
  mark#( U22( X1 , X2 ) )	→	mark#( X1 )
  mark#( isList( X ) )	→	a__isList#( X )
  mark#( U23( X ) )	→	mark#( X )
  mark#( U31( X1 , X2 ) )	→	mark#( X1 )
  mark#( U32( X ) )	→	mark#( X )
  mark#( U41( X1 , X2 , X3 ) )	→	a__U41#( mark( X1 ) , X2 , X3 )
  mark#( U41( X1 , X2 , X3 ) )	→	mark#( X1 )
  mark#( U42( X1 , X2 ) )	→	a__U42#( mark( X1 ) , X2 )
  mark#( U42( X1 , X2 ) )	→	mark#( X1 )
  mark#( U43( X ) )	→	mark#( X )
  mark#( U51( X1 , X2 , X3 ) )	→	a__U51#( mark( X1 ) , X2 , X3 )
  mark#( U51( X1 , X2 , X3 ) )	→	mark#( X1 )
  mark#( U52( X1 , X2 ) )	→	a__U52#( mark( X1 ) , X2 )
  mark#( U52( X1 , X2 ) )	→	mark#( X1 )
  mark#( U53( X ) )	→	mark#( X )
  mark#( U61( X1 , X2 ) )	→	mark#( X1 )
  mark#( U62( X ) )	→	mark#( X )
  a__isNePal#( V )	→	a__isPalListKind#( V )
  a__isNePal#( __( I , __( P , I ) ) )	→	a__and#( a__and( a__isQid( I ) , isPalListKind( I ) ) , and( isPal( P ) , isPalListKind( P ) ) )
  mark#( isNePal( X ) )	→	a__isNePal#( X )
  mark#( and( X1 , X2 ) )	→	a__and#( mark( X1 ) , X2 )
  mark#( and( X1 , X2 ) )	→	mark#( X1 )
  mark#( isPalListKind( X ) )	→	a__isPalListKind#( X )

  1.1.1.1.1.1: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [a]	=	0
  [__ (x1, x2) ]	=	x1 + x2
  [isNePal (x1) ]	=	1
  [a__U21# (x1, x2, x3) ]	=	1
  [U21 (x1, x2, x3) ]	=	2 x1
  [U41 (x1, x2, x3) ]	=	2 x1
  [i]	=	3
  [a__U22# (x1, x2) ]	=	1
  [U72 (x1) ]	=	0
  [U31 (x1, x2) ]	=	2 x1
  [U61 (x1, x2) ]	=	x1 + 1
  [and (x1, x2) ]	=	x1 + 2 x2
  [a__isNeList# (x1) ]	=	1
  [U71 (x1, x2) ]	=	0
  [a__U23 (x1) ]	=	2 x1
  [isNeList (x1) ]	=	0
  [a__U42# (x1, x2) ]	=	1
  [a__isPal (x1) ]	=	0
  [a__U11# (x1, x2) ]	=	1
  [isPal (x1) ]	=	0
  [a__U52# (x1, x2) ]	=	1
  [a__U72 (x1) ]	=	0
  [mark# (x1) ]	=	2 x1 + 1
  [a__U71 (x1, x2) ]	=	0
  [tt]	=	0
  [o]	=	0
  [a__and (x1, x2) ]	=	x1 + 2 x2
  [e]	=	0
  [a__U22 (x1, x2) ]	=	2 x1
  [a__U21 (x1, x2, x3) ]	=	2 x1
  [a__isNePal (x1) ]	=	1
  [a__U32 (x1) ]	=	x1
  [a__U41# (x1, x2, x3) ]	=	2 x1 + 1
  [U23 (x1) ]	=	2 x1
  [U51 (x1, x2, x3) ]	=	x1
  [U53 (x1) ]	=	2 x1
  [a__U41 (x1, x2, x3) ]	=	2 x1
  [a__isQid (x1) ]	=	0
  [a____ (x1, x2) ]	=	x1 + x2
  [U62 (x1) ]	=	x1 + 1
  [a__U62 (x1) ]	=	x1 + 1
  [a__isPalListKind# (x1) ]	=	1
  [a__U53 (x1) ]	=	2 x1
  [a__U42 (x1, x2) ]	=	x1
  [a__U31 (x1, x2) ]	=	2 x1
  [u]	=	0
  [U22 (x1, x2) ]	=	2 x1
  [a__U61 (x1, x2) ]	=	x1 + 1
  [U32 (x1) ]	=	x1
  [isList (x1) ]	=	0
  [a__U11 (x1, x2) ]	=	2 x1
  [mark (x1) ]	=	x1
  [a__isList# (x1) ]	=	1
  [a__U52 (x1, x2) ]	=	2 x1
  [a__isPalListKind (x1) ]	=	0
  [U52 (x1, x2) ]	=	2 x1
  [a__and# (x1, x2) ]	=	2 x1 + 1
  [nil]	=	0
  [U42 (x1, x2) ]	=	x1
  [a__isNeList (x1) ]	=	0
  [isPalListKind (x1) ]	=	0
  [a__U51 (x1, x2, x3) ]	=	x1
  [U11 (x1, x2) ]	=	2 x1
  [a__isNePal# (x1) ]	=	2
  [a__U51# (x1, x2, x3) ]	=	1
  [isQid (x1) ]	=	0
  [a__U12 (x1) ]	=	x1
  [a__isList (x1) ]	=	0
  [U43 (x1) ]	=	2 x1
  [a__U43 (x1) ]	=	2 x1
  [U12 (x1) ]	=	x1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  mark#( U11( X1 , X2 ) )	→	a__U11#( mark( X1 ) , X2 )
  a__U11#( tt , V )	→	a__isNeList#( V )
  a__isNeList#( V )	→	a__isPalListKind#( V )
  a__isPalListKind#( __( V1 , V2 ) )	→	a__and#( a__isPalListKind( V1 ) , isPalListKind( V2 ) )
  a__and#( tt , X )	→	mark#( X )
  mark#( U11( X1 , X2 ) )	→	mark#( X1 )
  mark#( U12( X ) )	→	mark#( X )
  mark#( isNeList( X ) )	→	a__isNeList#( X )
  a__isNeList#( __( V1 , V2 ) )	→	a__U41#( a__and( a__isPalListKind( V1 ) , isPalListKind( V2 ) ) , V1 , V2 )
  a__U41#( tt , V1 , V2 )	→	a__U42#( a__isList( V1 ) , V2 )
  a__U42#( tt , V2 )	→	a__isNeList#( V2 )
  a__isNeList#( __( V1 , V2 ) )	→	a__and#( a__isPalListKind( V1 ) , isPalListKind( V2 ) )
  a__isNeList#( __( V1 , V2 ) )	→	a__isPalListKind#( V1 )
  a__isPalListKind#( __( V1 , V2 ) )	→	a__isPalListKind#( V1 )
  a__isNeList#( __( V1 , V2 ) )	→	a__U51#( a__and( a__isPalListKind( V1 ) , isPalListKind( V2 ) ) , V1 , V2 )
  a__U51#( tt , V1 , V2 )	→	a__U52#( a__isNeList( V1 ) , V2 )
  a__U52#( tt , V2 )	→	a__isList#( V2 )
  a__isList#( V )	→	a__U11#( a__isPalListKind( V ) , V )
  a__isList#( V )	→	a__isPalListKind#( V )
  a__isList#( __( V1 , V2 ) )	→	a__U21#( a__and( a__isPalListKind( V1 ) , isPalListKind( V2 ) ) , V1 , V2 )
  a__U21#( tt , V1 , V2 )	→	a__U22#( a__isList( V1 ) , V2 )
  a__U22#( tt , V2 )	→	a__isList#( V2 )
  a__isList#( __( V1 , V2 ) )	→	a__and#( a__isPalListKind( V1 ) , isPalListKind( V2 ) )
  a__isList#( __( V1 , V2 ) )	→	a__isPalListKind#( V1 )
  a__U21#( tt , V1 , V2 )	→	a__isList#( V1 )
  a__U51#( tt , V1 , V2 )	→	a__isNeList#( V1 )
  a__U41#( tt , V1 , V2 )	→	a__isList#( V1 )
  mark#( U21( X1 , X2 , X3 ) )	→	a__U21#( mark( X1 ) , X2 , X3 )
  mark#( U21( X1 , X2 , X3 ) )	→	mark#( X1 )
  mark#( U22( X1 , X2 ) )	→	a__U22#( mark( X1 ) , X2 )
  mark#( U22( X1 , X2 ) )	→	mark#( X1 )
  mark#( isList( X ) )	→	a__isList#( X )
  mark#( U23( X ) )	→	mark#( X )
  mark#( U31( X1 , X2 ) )	→	mark#( X1 )
  mark#( U32( X ) )	→	mark#( X )
  mark#( U41( X1 , X2 , X3 ) )	→	a__U41#( mark( X1 ) , X2 , X3 )
  mark#( U41( X1 , X2 , X3 ) )	→	mark#( X1 )
  mark#( U42( X1 , X2 ) )	→	a__U42#( mark( X1 ) , X2 )
  mark#( U42( X1 , X2 ) )	→	mark#( X1 )
  mark#( U43( X ) )	→	mark#( X )
  mark#( U51( X1 , X2 , X3 ) )	→	a__U51#( mark( X1 ) , X2 , X3 )
  mark#( U51( X1 , X2 , X3 ) )	→	mark#( X1 )
  mark#( U52( X1 , X2 ) )	→	a__U52#( mark( X1 ) , X2 )
  mark#( U52( X1 , X2 ) )	→	mark#( X1 )
  mark#( U53( X ) )	→	mark#( X )
  mark#( and( X1 , X2 ) )	→	a__and#( mark( X1 ) , X2 )
  mark#( and( X1 , X2 ) )	→	mark#( X1 )
  mark#( isPalListKind( X ) )	→	a__isPalListKind#( X )

  1.1.1.1.1.1.1: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [a]	=	0
  [__ (x1, x2) ]	=	2 x1 + x2 + 1
  [isNePal (x1) ]	=	0
  [a__U21# (x1, x2, x3) ]	=	x1 + x2
  [U21 (x1, x2, x3) ]	=	x1 + x2 + x3
  [U41 (x1, x2, x3) ]	=	2 x1 + x2 + x3
  [i]	=	0
  [a__U22# (x1, x2) ]	=	x1
  [U72 (x1) ]	=	0
  [U61 (x1, x2) ]	=	0
  [U31 (x1, x2) ]	=	x1
  [and (x1, x2) ]	=	2 x1 + 2 x2
  [a__isNeList# (x1) ]	=	x1
  [U71 (x1, x2) ]	=	0
  [a__U23 (x1) ]	=	x1
  [isNeList (x1) ]	=	x1
  [a__U42# (x1, x2) ]	=	x1
  [a__isPal (x1) ]	=	0
  [a__U11# (x1, x2) ]	=	x1
  [isPal (x1) ]	=	0
  [a__U52# (x1, x2) ]	=	x1
  [a__U72 (x1) ]	=	0
  [mark# (x1) ]	=	2 x1
  [a__U71 (x1, x2) ]	=	0
  [tt]	=	0
  [o]	=	1
  [a__and (x1, x2) ]	=	2 x1 + 2 x2
  [e]	=	0
  [a__U22 (x1, x2) ]	=	x1 + x2
  [a__U21 (x1, x2, x3) ]	=	x1 + x2 + x3
  [a__isNePal (x1) ]	=	0
  [a__U32 (x1) ]	=	2 x1
  [a__U41# (x1, x2, x3) ]	=	2 x1 + x2
  [U23 (x1) ]	=	x1
  [U51 (x1, x2, x3) ]	=	2 x1 + 2 x2 + x3
  [U53 (x1) ]	=	x1
  [a__U41 (x1, x2, x3) ]	=	2 x1 + x2 + x3
  [a__isQid (x1) ]	=	0
  [a____ (x1, x2) ]	=	2 x1 + x2 + 1
  [U62 (x1) ]	=	0
  [a__U62 (x1) ]	=	0
  [a__isPalListKind# (x1) ]	=	0
  [a__U53 (x1) ]	=	x1
  [a__U42 (x1, x2) ]	=	x1 + x2
  [a__U31 (x1, x2) ]	=	x1
  [u]	=	0
  [U22 (x1, x2) ]	=	x1 + x2
  [a__U61 (x1, x2) ]	=	0
  [U32 (x1) ]	=	2 x1
  [isList (x1) ]	=	x1
  [a__U11 (x1, x2) ]	=	x1 + x2
  [mark (x1) ]	=	x1
  [a__isList# (x1) ]	=	x1
  [a__U52 (x1, x2) ]	=	x1 + x2
  [a__isPalListKind (x1) ]	=	0
  [U52 (x1, x2) ]	=	x1 + x2
  [a__and# (x1, x2) ]	=	2 x1
  [nil]	=	0
  [U42 (x1, x2) ]	=	x1 + x2
  [a__isNeList (x1) ]	=	x1
  [isPalListKind (x1) ]	=	0
  [a__U51 (x1, x2, x3) ]	=	2 x1 + 2 x2 + x3
  [U11 (x1, x2) ]	=	x1 + x2
  [a__U51# (x1, x2, x3) ]	=	2 x1 + x2
  [isQid (x1) ]	=	0
  [a__U12 (x1) ]	=	x1
  [a__isList (x1) ]	=	x1
  [U43 (x1) ]	=	x1
  [a__U43 (x1) ]	=	x1
  [U12 (x1) ]	=	x1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  mark#( U11( X1 , X2 ) )	→	a__U11#( mark( X1 ) , X2 )
  a__U11#( tt , V )	→	a__isNeList#( V )
  a__isNeList#( V )	→	a__isPalListKind#( V )
  a__isPalListKind#( __( V1 , V2 ) )	→	a__and#( a__isPalListKind( V1 ) , isPalListKind( V2 ) )
  a__and#( tt , X )	→	mark#( X )
  mark#( U11( X1 , X2 ) )	→	mark#( X1 )
  mark#( U12( X ) )	→	mark#( X )
  mark#( isNeList( X ) )	→	a__isNeList#( X )
  a__U41#( tt , V1 , V2 )	→	a__U42#( a__isList( V1 ) , V2 )
  a__U42#( tt , V2 )	→	a__isNeList#( V2 )
  a__isPalListKind#( __( V1 , V2 ) )	→	a__isPalListKind#( V1 )
  a__U51#( tt , V1 , V2 )	→	a__U52#( a__isNeList( V1 ) , V2 )
  a__U52#( tt , V2 )	→	a__isList#( V2 )
  a__isList#( V )	→	a__U11#( a__isPalListKind( V ) , V )
  a__isList#( V )	→	a__isPalListKind#( V )
  a__U21#( tt , V1 , V2 )	→	a__U22#( a__isList( V1 ) , V2 )
  a__U22#( tt , V2 )	→	a__isList#( V2 )
  a__U21#( tt , V1 , V2 )	→	a__isList#( V1 )
  a__U51#( tt , V1 , V2 )	→	a__isNeList#( V1 )
  a__U41#( tt , V1 , V2 )	→	a__isList#( V1 )
  mark#( U21( X1 , X2 , X3 ) )	→	a__U21#( mark( X1 ) , X2 , X3 )
  mark#( U21( X1 , X2 , X3 ) )	→	mark#( X1 )
  mark#( U22( X1 , X2 ) )	→	a__U22#( mark( X1 ) , X2 )
  mark#( U22( X1 , X2 ) )	→	mark#( X1 )
  mark#( isList( X ) )	→	a__isList#( X )
  mark#( U23( X ) )	→	mark#( X )
  mark#( U31( X1 , X2 ) )	→	mark#( X1 )
  mark#( U32( X ) )	→	mark#( X )
  mark#( U41( X1 , X2 , X3 ) )	→	a__U41#( mark( X1 ) , X2 , X3 )
  mark#( U41( X1 , X2 , X3 ) )	→	mark#( X1 )
  mark#( U42( X1 , X2 ) )	→	a__U42#( mark( X1 ) , X2 )
  mark#( U42( X1 , X2 ) )	→	mark#( X1 )
  mark#( U43( X ) )	→	mark#( X )
  mark#( U51( X1 , X2 , X3 ) )	→	a__U51#( mark( X1 ) , X2 , X3 )
  mark#( U51( X1 , X2 , X3 ) )	→	mark#( X1 )
  mark#( U52( X1 , X2 ) )	→	a__U52#( mark( X1 ) , X2 )
  mark#( U52( X1 , X2 ) )	→	mark#( X1 )
  mark#( U53( X ) )	→	mark#( X )
  mark#( and( X1 , X2 ) )	→	a__and#( mark( X1 ) , X2 )
  mark#( and( X1 , X2 ) )	→	mark#( X1 )
  mark#( isPalListKind( X ) )	→	a__isPalListKind#( X )

  1.1.1.1.1.1.1.1: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [a]	=	0
  [__ (x1, x2) ]	=	2 x1 + x2 + 2
  [isNePal (x1) ]	=	1
  [a__U21# (x1, x2, x3) ]	=	3 x1 + 1
  [U21 (x1, x2, x3) ]	=	2 x1 + 2 x2 + 2 x3 + 1
  [U41 (x1, x2, x3) ]	=	x1 + 2 x2 + 2 x3
  [i]	=	0
  [a__U22# (x1, x2) ]	=	0
  [U72 (x1) ]	=	0
  [U61 (x1, x2) ]	=	1
  [U31 (x1, x2) ]	=	2 x1
  [and (x1, x2) ]	=	2 x1 + 2 x2
  [a__isNeList# (x1) ]	=	0
  [U71 (x1, x2) ]	=	0
  [a__U23 (x1) ]	=	x1
  [isNeList (x1) ]	=	2 x1
  [a__U42# (x1, x2) ]	=	x1
  [a__isPal (x1) ]	=	0
  [a__U11# (x1, x2) ]	=	0
  [isPal (x1) ]	=	0
  [a__U52# (x1, x2) ]	=	2 x1 + 1
  [a__U72 (x1) ]	=	0
  [mark# (x1) ]	=	2 x1
  [a__U71 (x1, x2) ]	=	0
  [tt]	=	0
  [o]	=	1
  [a__and (x1, x2) ]	=	2 x1 + 2 x2
  [e]	=	0
  [a__U22 (x1, x2) ]	=	x1 + 2 x2
  [a__U21 (x1, x2, x3) ]	=	2 x1 + 2 x2 + 2 x3 + 1
  [a__isNePal (x1) ]	=	1
  [a__U32 (x1) ]	=	x1
  [a__U41# (x1, x2, x3) ]	=	2 x1
  [U23 (x1) ]	=	x1
  [U51 (x1, x2, x3) ]	=	x1 + 2 x2 + 2 x3 + 1
  [U53 (x1) ]	=	x1
  [a__U41 (x1, x2, x3) ]	=	x1 + 2 x2 + 2 x3
  [a__isQid (x1) ]	=	0
  [a____ (x1, x2) ]	=	2 x1 + x2 + 2
  [U62 (x1) ]	=	0
  [a__U62 (x1) ]	=	0
  [a__isPalListKind# (x1) ]	=	0
  [a__U53 (x1) ]	=	x1
  [a__U42 (x1, x2) ]	=	x1 + 2 x2
  [a__U31 (x1, x2) ]	=	2 x1
  [u]	=	0
  [U22 (x1, x2) ]	=	x1 + 2 x2
  [a__U61 (x1, x2) ]	=	1
  [U32 (x1) ]	=	x1
  [isList (x1) ]	=	2 x1
  [a__U11 (x1, x2) ]	=	2 x1 + 2 x2
  [mark (x1) ]	=	x1
  [a__isList# (x1) ]	=	0
  [a__U52 (x1, x2) ]	=	x1 + 2 x2 + 1
  [a__isPalListKind (x1) ]	=	0
  [U52 (x1, x2) ]	=	x1 + 2 x2 + 1
  [a__and# (x1, x2) ]	=	2 x1
  [nil]	=	0
  [U42 (x1, x2) ]	=	x1 + 2 x2
  [a__isNeList (x1) ]	=	2 x1
  [a__U51 (x1, x2, x3) ]	=	x1 + 2 x2 + 2 x3 + 1
  [isPalListKind (x1) ]	=	0
  [U11 (x1, x2) ]	=	2 x1 + 2 x2
  [a__U51# (x1, x2, x3) ]	=	3 x1 + 3 x2 + 1
  [isQid (x1) ]	=	0
  [a__U12 (x1) ]	=	x1
  [a__isList (x1) ]	=	2 x1
  [U43 (x1) ]	=	x1
  [a__U43 (x1) ]	=	x1
  [U12 (x1) ]	=	x1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  mark#( U11( X1 , X2 ) )	→	a__U11#( mark( X1 ) , X2 )
  a__U11#( tt , V )	→	a__isNeList#( V )
  a__isNeList#( V )	→	a__isPalListKind#( V )
  a__isPalListKind#( __( V1 , V2 ) )	→	a__and#( a__isPalListKind( V1 ) , isPalListKind( V2 ) )
  a__and#( tt , X )	→	mark#( X )
  mark#( U11( X1 , X2 ) )	→	mark#( X1 )
  mark#( U12( X ) )	→	mark#( X )
  mark#( isNeList( X ) )	→	a__isNeList#( X )
  a__U41#( tt , V1 , V2 )	→	a__U42#( a__isList( V1 ) , V2 )
  a__U42#( tt , V2 )	→	a__isNeList#( V2 )
  a__isPalListKind#( __( V1 , V2 ) )	→	a__isPalListKind#( V1 )
  a__U51#( tt , V1 , V2 )	→	a__U52#( a__isNeList( V1 ) , V2 )
  a__isList#( V )	→	a__U11#( a__isPalListKind( V ) , V )
  a__isList#( V )	→	a__isPalListKind#( V )
  a__U22#( tt , V2 )	→	a__isList#( V2 )
  a__U41#( tt , V1 , V2 )	→	a__isList#( V1 )
  mark#( U22( X1 , X2 ) )	→	a__U22#( mark( X1 ) , X2 )
  mark#( U22( X1 , X2 ) )	→	mark#( X1 )
  mark#( isList( X ) )	→	a__isList#( X )
  mark#( U23( X ) )	→	mark#( X )
  mark#( U31( X1 , X2 ) )	→	mark#( X1 )
  mark#( U32( X ) )	→	mark#( X )
  mark#( U41( X1 , X2 , X3 ) )	→	a__U41#( mark( X1 ) , X2 , X3 )
  mark#( U41( X1 , X2 , X3 ) )	→	mark#( X1 )
  mark#( U42( X1 , X2 ) )	→	a__U42#( mark( X1 ) , X2 )
  mark#( U42( X1 , X2 ) )	→	mark#( X1 )
  mark#( U43( X ) )	→	mark#( X )
  mark#( U53( X ) )	→	mark#( X )
  mark#( and( X1 , X2 ) )	→	a__and#( mark( X1 ) , X2 )
  mark#( and( X1 , X2 ) )	→	mark#( X1 )
  mark#( isPalListKind( X ) )	→	a__isPalListKind#( X )

  1.1.1.1.1.1.1.1.1: dependency graph processor

  The dependency pairs are split into 1 component(s).

  • The 1st component contains the pair(s)

    a__U11#( tt , V )	→	a__isNeList#( V )
    a__isNeList#( V )	→	a__isPalListKind#( V )
    a__isPalListKind#( __( V1 , V2 ) )	→	a__and#( a__isPalListKind( V1 ) , isPalListKind( V2 ) )
    a__and#( tt , X )	→	mark#( X )
    mark#( U11( X1 , X2 ) )	→	a__U11#( mark( X1 ) , X2 )
    mark#( U11( X1 , X2 ) )	→	mark#( X1 )
    mark#( U12( X ) )	→	mark#( X )
    mark#( isNeList( X ) )	→	a__isNeList#( X )
    mark#( U22( X1 , X2 ) )	→	a__U22#( mark( X1 ) , X2 )
    a__U22#( tt , V2 )	→	a__isList#( V2 )
    a__isList#( V )	→	a__U11#( a__isPalListKind( V ) , V )
    a__isList#( V )	→	a__isPalListKind#( V )
    a__isPalListKind#( __( V1 , V2 ) )	→	a__isPalListKind#( V1 )
    mark#( U22( X1 , X2 ) )	→	mark#( X1 )
    mark#( isList( X ) )	→	a__isList#( X )
    mark#( U23( X ) )	→	mark#( X )
    mark#( U31( X1 , X2 ) )	→	mark#( X1 )
    mark#( U32( X ) )	→	mark#( X )
    mark#( U41( X1 , X2 , X3 ) )	→	a__U41#( mark( X1 ) , X2 , X3 )
    a__U41#( tt , V1 , V2 )	→	a__U42#( a__isList( V1 ) , V2 )
    a__U42#( tt , V2 )	→	a__isNeList#( V2 )
    a__U41#( tt , V1 , V2 )	→	a__isList#( V1 )
    mark#( U41( X1 , X2 , X3 ) )	→	mark#( X1 )
    mark#( U42( X1 , X2 ) )	→	a__U42#( mark( X1 ) , X2 )
    mark#( U42( X1 , X2 ) )	→	mark#( X1 )
    mark#( U43( X ) )	→	mark#( X )
    mark#( U53( X ) )	→	mark#( X )
    mark#( and( X1 , X2 ) )	→	a__and#( mark( X1 ) , X2 )
    mark#( and( X1 , X2 ) )	→	mark#( X1 )
    mark#( isPalListKind( X ) )	→	a__isPalListKind#( X )

    1.1.1.1.1.1.1.1.1.1: reduction pair processor

    Using the following reduction pair

    Linear polynomial interpretation over the naturals

    [a]	=	0
    [__ (x1, x2) ]	=	2 x1 + x2 + 1
    [isNePal (x1) ]	=	0
    [U21 (x1, x2, x3) ]	=	2 x1 + x2 + 2
    [U41 (x1, x2, x3) ]	=	x1 + 2 x2 + x3 + 1
    [i]	=	0
    [a__U22# (x1, x2) ]	=	x1 + 1
    [U72 (x1) ]	=	0
    [U61 (x1, x2) ]	=	0
    [U31 (x1, x2) ]	=	x1
    [and (x1, x2) ]	=	2 x1 + 2 x2
    [U71 (x1, x2) ]	=	0
    [a__isNeList# (x1) ]	=	x1
    [a__U23 (x1) ]	=	x1
    [isNeList (x1) ]	=	x1
    [a__U42# (x1, x2) ]	=	x1 + x2
    [a__isPal (x1) ]	=	0
    [a__U11# (x1, x2) ]	=	x1 + 1
    [isPal (x1) ]	=	0
    [a__U72 (x1) ]	=	0
    [mark# (x1) ]	=	x1
    [a__U71 (x1, x2) ]	=	0
    [tt]	=	0
    [a__and (x1, x2) ]	=	2 x1 + 2 x2
    [o]	=	2
    [e]	=	0
    [a__U22 (x1, x2) ]	=	x1 + x2 + 1
    [a__U21 (x1, x2, x3) ]	=	2 x1 + x2 + 2
    [a__isNePal (x1) ]	=	0
    [a__U32 (x1) ]	=	x1
    [a__U41# (x1, x2, x3) ]	=	2 x1 + x2 + 1
    [U23 (x1) ]	=	x1
    [U51 (x1, x2, x3) ]	=	x1 + 1
    [U53 (x1) ]	=	x1
    [a__U41 (x1, x2, x3) ]	=	x1 + 2 x2 + x3 + 1
    [a__isQid (x1) ]	=	0
    [a____ (x1, x2) ]	=	2 x1 + x2 + 1
    [U62 (x1) ]	=	0
    [a__isPalListKind# (x1) ]	=	0
    [a__U62 (x1) ]	=	0
    [a__U53 (x1) ]	=	x1
    [a__U42 (x1, x2) ]	=	x1 + x2
    [a__U31 (x1, x2) ]	=	x1
    [u]	=	0
    [U22 (x1, x2) ]	=	x1 + x2 + 1
    [U32 (x1) ]	=	x1
    [a__U61 (x1, x2) ]	=	0
    [isList (x1) ]	=	x1 + 1
    [a__U11 (x1, x2) ]	=	x1 + x2 + 1
    [mark (x1) ]	=	x1
    [a__isList# (x1) ]	=	x1 + 1
    [a__U52 (x1, x2) ]	=	x1 + 1
    [a__isPalListKind (x1) ]	=	0
    [a__and# (x1, x2) ]	=	2 x1
    [U52 (x1, x2) ]	=	x1 + 1
    [nil]	=	0
    [a__isNeList (x1) ]	=	x1
    [U42 (x1, x2) ]	=	x1 + x2
    [a__U51 (x1, x2, x3) ]	=	x1 + 1
    [isPalListKind (x1) ]	=	0
    [U11 (x1, x2) ]	=	x1 + x2 + 1
    [isQid (x1) ]	=	0
    [a__U12 (x1) ]	=	x1 + 1
    [a__isList (x1) ]	=	x1 + 1
    [U43 (x1) ]	=	x1
    [a__U43 (x1) ]	=	x1
    [U12 (x1) ]	=	x1 + 1
    [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

    one remains with the following pair(s).

    a__isNeList#( V )	→	a__isPalListKind#( V )
    a__isPalListKind#( __( V1 , V2 ) )	→	a__and#( a__isPalListKind( V1 ) , isPalListKind( V2 ) )
    a__and#( tt , X )	→	mark#( X )
    mark#( U11( X1 , X2 ) )	→	a__U11#( mark( X1 ) , X2 )
    mark#( isNeList( X ) )	→	a__isNeList#( X )
    mark#( U22( X1 , X2 ) )	→	a__U22#( mark( X1 ) , X2 )
    a__U22#( tt , V2 )	→	a__isList#( V2 )
    a__isList#( V )	→	a__U11#( a__isPalListKind( V ) , V )
    a__isPalListKind#( __( V1 , V2 ) )	→	a__isPalListKind#( V1 )
    mark#( isList( X ) )	→	a__isList#( X )
    mark#( U23( X ) )	→	mark#( X )
    mark#( U31( X1 , X2 ) )	→	mark#( X1 )
    mark#( U32( X ) )	→	mark#( X )
    mark#( U41( X1 , X2 , X3 ) )	→	a__U41#( mark( X1 ) , X2 , X3 )
    a__U41#( tt , V1 , V2 )	→	a__U42#( a__isList( V1 ) , V2 )
    a__U42#( tt , V2 )	→	a__isNeList#( V2 )
    a__U41#( tt , V1 , V2 )	→	a__isList#( V1 )
    mark#( U42( X1 , X2 ) )	→	a__U42#( mark( X1 ) , X2 )
    mark#( U42( X1 , X2 ) )	→	mark#( X1 )
    mark#( U43( X ) )	→	mark#( X )
    mark#( U53( X ) )	→	mark#( X )
    mark#( and( X1 , X2 ) )	→	a__and#( mark( X1 ) , X2 )
    mark#( and( X1 , X2 ) )	→	mark#( X1 )
    mark#( isPalListKind( X ) )	→	a__isPalListKind#( X )

    1.1.1.1.1.1.1.1.1.1.1: dependency graph processor

    The dependency pairs are split into 1 component(s).

    • The 1st component contains the pair(s)

      a__isPalListKind#( __( V1 , V2 ) )	→	a__and#( a__isPalListKind( V1 ) , isPalListKind( V2 ) )
      a__and#( tt , X )	→	mark#( X )
      mark#( isNeList( X ) )	→	a__isNeList#( X )
      a__isNeList#( V )	→	a__isPalListKind#( V )
      a__isPalListKind#( __( V1 , V2 ) )	→	a__isPalListKind#( V1 )
      mark#( U23( X ) )	→	mark#( X )
      mark#( U31( X1 , X2 ) )	→	mark#( X1 )
      mark#( U32( X ) )	→	mark#( X )
      mark#( U41( X1 , X2 , X3 ) )	→	a__U41#( mark( X1 ) , X2 , X3 )
      a__U41#( tt , V1 , V2 )	→	a__U42#( a__isList( V1 ) , V2 )
      a__U42#( tt , V2 )	→	a__isNeList#( V2 )
      mark#( U42( X1 , X2 ) )	→	a__U42#( mark( X1 ) , X2 )
      mark#( U42( X1 , X2 ) )	→	mark#( X1 )
      mark#( U43( X ) )	→	mark#( X )
      mark#( U53( X ) )	→	mark#( X )
      mark#( and( X1 , X2 ) )	→	a__and#( mark( X1 ) , X2 )
      mark#( and( X1 , X2 ) )	→	mark#( X1 )
      mark#( isPalListKind( X ) )	→	a__isPalListKind#( X )

      1.1.1.1.1.1.1.1.1.1.1.1: reduction pair processor

      Using the following reduction pair

      Linear polynomial interpretation over the naturals

      [__ (x1, x2) ]	=	x1 + x2
      [a]	=	0
      [isNePal (x1) ]	=	0
      [U21 (x1, x2, x3) ]	=	0
      [U41 (x1, x2, x3) ]	=	1
      [i]	=	0
      [U72 (x1) ]	=	0
      [U61 (x1, x2) ]	=	x1
      [and (x1, x2) ]	=	x1 + 2 x2
      [U31 (x1, x2) ]	=	x1 + 1
      [U71 (x1, x2) ]	=	0
      [a__isNeList# (x1) ]	=	1
      [a__U23 (x1) ]	=	2 x1
      [isNeList (x1) ]	=	1
      [a__isPal (x1) ]	=	0
      [a__U42# (x1, x2) ]	=	2
      [isPal (x1) ]	=	0
      [a__U72 (x1) ]	=	0
      [mark# (x1) ]	=	2 x1
      [a__U71 (x1, x2) ]	=	0
      [tt]	=	0
      [a__and (x1, x2) ]	=	x1 + 2 x2
      [o]	=	0
      [e]	=	0
      [a__U22 (x1, x2) ]	=	0
      [a__U21 (x1, x2, x3) ]	=	0
      [a__U32 (x1) ]	=	x1 + 1
      [a__isNePal (x1) ]	=	0
      [a__U41# (x1, x2, x3) ]	=	2
      [U23 (x1) ]	=	2 x1
      [U51 (x1, x2, x3) ]	=	0
      [U53 (x1) ]	=	2 x1
      [a__U41 (x1, x2, x3) ]	=	1
      [a__isQid (x1) ]	=	0
      [a____ (x1, x2) ]	=	x1 + x2
      [U62 (x1) ]	=	0
      [a__isPalListKind# (x1) ]	=	0
      [a__U62 (x1) ]	=	0
      [a__U53 (x1) ]	=	2 x1
      [a__U42 (x1, x2) ]	=	x1 + 1
      [a__U31 (x1, x2) ]	=	x1 + 1
      [u]	=	1
      [U22 (x1, x2) ]	=	0
      [U32 (x1) ]	=	x1 + 1
      [a__U61 (x1, x2) ]	=	x1
      [isList (x1) ]	=	0
      [a__U11 (x1, x2) ]	=	0
      [mark (x1) ]	=	x1
      [a__U52 (x1, x2) ]	=	0
      [a__isPalListKind (x1) ]	=	0
      [a__and# (x1, x2) ]	=	2 x1
      [U52 (x1, x2) ]	=	0
      [nil]	=	0
      [a__isNeList (x1) ]	=	1
      [U42 (x1, x2) ]	=	x1 + 1
      [a__U51 (x1, x2, x3) ]	=	0
      [isPalListKind (x1) ]	=	0
      [U11 (x1, x2) ]	=	0
      [isQid (x1) ]	=	0
      [a__isList (x1) ]	=	0
      [a__U12 (x1) ]	=	0
      [U43 (x1) ]	=	x1
      [a__U43 (x1) ]	=	x1
      [U12 (x1) ]	=	0
      [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

      one remains with the following pair(s).

      a__isPalListKind#( __( V1 , V2 ) )	→	a__and#( a__isPalListKind( V1 ) , isPalListKind( V2 ) )
      a__and#( tt , X )	→	mark#( X )
      a__isPalListKind#( __( V1 , V2 ) )	→	a__isPalListKind#( V1 )
      mark#( U23( X ) )	→	mark#( X )
      mark#( U41( X1 , X2 , X3 ) )	→	a__U41#( mark( X1 ) , X2 , X3 )
      a__U41#( tt , V1 , V2 )	→	a__U42#( a__isList( V1 ) , V2 )
      mark#( U42( X1 , X2 ) )	→	a__U42#( mark( X1 ) , X2 )
      mark#( U43( X ) )	→	mark#( X )
      mark#( U53( X ) )	→	mark#( X )
      mark#( and( X1 , X2 ) )	→	a__and#( mark( X1 ) , X2 )
      mark#( and( X1 , X2 ) )	→	mark#( X1 )
      mark#( isPalListKind( X ) )	→	a__isPalListKind#( X )

      1.1.1.1.1.1.1.1.1.1.1.1.1: dependency graph processor

      The dependency pairs are split into 1 component(s).

      • The 1st component contains the pair(s)

        a__and#( tt , X )	→	mark#( X )
        mark#( U23( X ) )	→	mark#( X )
        mark#( U43( X ) )	→	mark#( X )
        mark#( U53( X ) )	→	mark#( X )
        mark#( and( X1 , X2 ) )	→	a__and#( mark( X1 ) , X2 )
        mark#( and( X1 , X2 ) )	→	mark#( X1 )
        mark#( isPalListKind( X ) )	→	a__isPalListKind#( X )
        a__isPalListKind#( __( V1 , V2 ) )	→	a__and#( a__isPalListKind( V1 ) , isPalListKind( V2 ) )
        a__isPalListKind#( __( V1 , V2 ) )	→	a__isPalListKind#( V1 )

        1.1.1.1.1.1.1.1.1.1.1.1.1.1: reduction pair processor

        Using the following reduction pair

        Linear polynomial interpretation over the naturals

        [__ (x1, x2) ]	=	2 x1 + x2
        [a]	=	0
        [isNePal (x1) ]	=	0
        [U21 (x1, x2, x3) ]	=	0
        [U41 (x1, x2, x3) ]	=	2
        [i]	=	0
        [U72 (x1) ]	=	0
        [U61 (x1, x2) ]	=	0
        [U31 (x1, x2) ]	=	0
        [and (x1, x2) ]	=	2 x1 + 2 x2
        [U71 (x1, x2) ]	=	0
        [a__U23 (x1) ]	=	2 x1
        [isNeList (x1) ]	=	2
        [a__isPal (x1) ]	=	0
        [isPal (x1) ]	=	0
        [a__U72 (x1) ]	=	0
        [mark# (x1) ]	=	x1
        [a__U71 (x1, x2) ]	=	0
        [tt]	=	0
        [o]	=	0
        [a__and (x1, x2) ]	=	2 x1 + 2 x2
        [e]	=	0
        [a__U22 (x1, x2) ]	=	x1
        [a__U21 (x1, x2, x3) ]	=	0
        [a__U32 (x1) ]	=	2 x1
        [a__isNePal (x1) ]	=	0
        [U23 (x1) ]	=	2 x1
        [U51 (x1, x2, x3) ]	=	2 x1 + 1
        [U53 (x1) ]	=	x1 + 1
        [a__U41 (x1, x2, x3) ]	=	2
        [a__isQid (x1) ]	=	0
        [a____ (x1, x2) ]	=	2 x1 + x2
        [U62 (x1) ]	=	0
        [a__isPalListKind# (x1) ]	=	0
        [a__U62 (x1) ]	=	0
        [a__U53 (x1) ]	=	x1 + 1
        [a__U42 (x1, x2) ]	=	2
        [a__U31 (x1, x2) ]	=	0
        [u]	=	0
        [U22 (x1, x2) ]	=	x1
        [U32 (x1) ]	=	2 x1
        [a__U61 (x1, x2) ]	=	0
        [isList (x1) ]	=	0
        [a__U11 (x1, x2) ]	=	0
        [mark (x1) ]	=	x1
        [a__U52 (x1, x2) ]	=	1
        [a__isPalListKind (x1) ]	=	0
        [U52 (x1, x2) ]	=	1
        [a__and# (x1, x2) ]	=	x1
        [nil]	=	1
        [a__isNeList (x1) ]	=	2
        [U42 (x1, x2) ]	=	2
        [a__U51 (x1, x2, x3) ]	=	2 x1 + 1
        [isPalListKind (x1) ]	=	0
        [U11 (x1, x2) ]	=	0
        [isQid (x1) ]	=	0
        [a__U12 (x1) ]	=	0
        [a__isList (x1) ]	=	0
        [U43 (x1) ]	=	x1
        [a__U43 (x1) ]	=	x1
        [U12 (x1) ]	=	0
        [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

        one remains with the following pair(s).

        a__and#( tt , X )	→	mark#( X )
        mark#( U23( X ) )	→	mark#( X )
        mark#( U43( X ) )	→	mark#( X )
        mark#( and( X1 , X2 ) )	→	a__and#( mark( X1 ) , X2 )
        mark#( and( X1 , X2 ) )	→	mark#( X1 )
        mark#( isPalListKind( X ) )	→	a__isPalListKind#( X )
        a__isPalListKind#( __( V1 , V2 ) )	→	a__and#( a__isPalListKind( V1 ) , isPalListKind( V2 ) )
        a__isPalListKind#( __( V1 , V2 ) )	→	a__isPalListKind#( V1 )

        1.1.1.1.1.1.1.1.1.1.1.1.1.1.1: reduction pair processor

        Using the following reduction pair

        Linear polynomial interpretation over the naturals

        [__ (x1, x2) ]	=	x1 + x2 + 2
        [a]	=	0
        [isNePal (x1) ]	=	0
        [U21 (x1, x2, x3) ]	=	x1 + 2
        [U41 (x1, x2, x3) ]	=	x1 + 2 x2 + 2
        [i]	=	0
        [U72 (x1) ]	=	0
        [U61 (x1, x2) ]	=	2 x1
        [and (x1, x2) ]	=	x1 + 2 x2
        [U31 (x1, x2) ]	=	2 x1 + 2 x2
        [U71 (x1, x2) ]	=	0
        [a__U23 (x1) ]	=	x1 + 2
        [isNeList (x1) ]	=	2 x1
        [a__isPal (x1) ]	=	0
        [isPal (x1) ]	=	0
        [a__U72 (x1) ]	=	0
        [mark# (x1) ]	=	2 x1
        [a__U71 (x1, x2) ]	=	0
        [tt]	=	0
        [o]	=	0
        [a__and (x1, x2) ]	=	x1 + 2 x2
        [e]	=	0
        [a__U22 (x1, x2) ]	=	x1 + 2
        [a__U21 (x1, x2, x3) ]	=	x1 + 2
        [a__U32 (x1) ]	=	0
        [a__isNePal (x1) ]	=	0
        [U23 (x1) ]	=	x1 + 2
        [U53 (x1) ]	=	0
        [U51 (x1, x2, x3) ]	=	0
        [a__U41 (x1, x2, x3) ]	=	x1 + 2 x2 + 2
        [a__isQid (x1) ]	=	0
        [a____ (x1, x2) ]	=	x1 + x2 + 2
        [U62 (x1) ]	=	0
        [a__isPalListKind# (x1) ]	=	0
        [a__U62 (x1) ]	=	0
        [a__U53 (x1) ]	=	0
        [a__U42 (x1, x2) ]	=	2 x1 + 1
        [a__U31 (x1, x2) ]	=	2 x1 + 2 x2
        [u]	=	0
        [U22 (x1, x2) ]	=	x1 + 2
        [U32 (x1) ]	=	0
        [a__U61 (x1, x2) ]	=	2 x1
        [isList (x1) ]	=	x1
        [a__U11 (x1, x2) ]	=	0
        [mark (x1) ]	=	x1
        [a__U52 (x1, x2) ]	=	0
        [a__isPalListKind (x1) ]	=	0
        [U52 (x1, x2) ]	=	0
        [a__and# (x1, x2) ]	=	2 x1
        [nil]	=	2
        [a__isNeList (x1) ]	=	2 x1
        [U42 (x1, x2) ]	=	2 x1 + 1
        [a__U51 (x1, x2, x3) ]	=	0
        [isPalListKind (x1) ]	=	0
        [U11 (x1, x2) ]	=	0
        [isQid (x1) ]	=	0
        [a__U12 (x1) ]	=	0
        [a__isList (x1) ]	=	x1
        [U43 (x1) ]	=	x1
        [a__U43 (x1) ]	=	x1
        [U12 (x1) ]	=	0
        [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

        one remains with the following pair(s).

        a__and#( tt , X )	→	mark#( X )
        mark#( U43( X ) )	→	mark#( X )
        mark#( and( X1 , X2 ) )	→	a__and#( mark( X1 ) , X2 )
        mark#( and( X1 , X2 ) )	→	mark#( X1 )
        mark#( isPalListKind( X ) )	→	a__isPalListKind#( X )
        a__isPalListKind#( __( V1 , V2 ) )	→	a__and#( a__isPalListKind( V1 ) , isPalListKind( V2 ) )
        a__isPalListKind#( __( V1 , V2 ) )	→	a__isPalListKind#( V1 )

        1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1: reduction pair processor

        Using the following reduction pair

        Linear polynomial interpretation over the naturals

        [__ (x1, x2) ]	=	3 x1 + x2 + 2
        [a]	=	0
        [isNePal (x1) ]	=	x1
        [U21 (x1, x2, x3) ]	=	0
        [U41 (x1, x2, x3) ]	=	0
        [i]	=	0
        [U72 (x1) ]	=	0
        [U61 (x1, x2) ]	=	0
        [and (x1, x2) ]	=	2 x1 + x2
        [U31 (x1, x2) ]	=	0
        [U71 (x1, x2) ]	=	0
        [a__U23 (x1) ]	=	0
        [isNeList (x1) ]	=	0
        [a__isPal (x1) ]	=	0
        [isPal (x1) ]	=	0
        [a__U72 (x1) ]	=	0
        [mark# (x1) ]	=	x1
        [a__U71 (x1, x2) ]	=	0
        [tt]	=	0
        [o]	=	0
        [a__and (x1, x2) ]	=	2 x1 + x2
        [e]	=	2
        [a__U22 (x1, x2) ]	=	0
        [a__U21 (x1, x2, x3) ]	=	0
        [a__U32 (x1) ]	=	0
        [a__isNePal (x1) ]	=	x1
        [U23 (x1) ]	=	0
        [U53 (x1) ]	=	0
        [U51 (x1, x2, x3) ]	=	0
        [a__U41 (x1, x2, x3) ]	=	0
        [a__isQid (x1) ]	=	0
        [a____ (x1, x2) ]	=	3 x1 + x2 + 2
        [U62 (x1) ]	=	0
        [a__isPalListKind# (x1) ]	=	2 x1
        [a__U62 (x1) ]	=	0
        [a__U53 (x1) ]	=	0
        [a__U42 (x1, x2) ]	=	0
        [a__U31 (x1, x2) ]	=	0
        [u]	=	2
        [U22 (x1, x2) ]	=	0
        [U32 (x1) ]	=	0
        [a__U61 (x1, x2) ]	=	0
        [isList (x1) ]	=	0
        [a__U11 (x1, x2) ]	=	0
        [mark (x1) ]	=	x1
        [a__U52 (x1, x2) ]	=	0
        [a__isPalListKind (x1) ]	=	2 x1
        [U52 (x1, x2) ]	=	0
        [a__and# (x1, x2) ]	=	x1
        [nil]	=	0
        [a__isNeList (x1) ]	=	0
        [U42 (x1, x2) ]	=	0
        [a__U51 (x1, x2, x3) ]	=	0
        [isPalListKind (x1) ]	=	2 x1
        [U11 (x1, x2) ]	=	0
        [isQid (x1) ]	=	0
        [a__U12 (x1) ]	=	0
        [a__isList (x1) ]	=	0
        [U43 (x1) ]	=	2 x1
        [a__U43 (x1) ]	=	2 x1
        [U12 (x1) ]	=	0
        [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

        one remains with the following pair(s).

        a__and#( tt , X )	→	mark#( X )
        mark#( U43( X ) )	→	mark#( X )
        mark#( and( X1 , X2 ) )	→	a__and#( mark( X1 ) , X2 )
        mark#( and( X1 , X2 ) )	→	mark#( X1 )
        mark#( isPalListKind( X ) )	→	a__isPalListKind#( X )

        1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1: dependency graph processor

        The dependency pairs are split into 1 component(s).

        • The 1st component contains the pair(s)

          mark#( U43( X ) )	→	mark#( X )
          mark#( and( X1 , X2 ) )	→	a__and#( mark( X1 ) , X2 )
          a__and#( tt , X )	→	mark#( X )
          mark#( and( X1 , X2 ) )	→	mark#( X1 )

          1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1: reduction pair processor

          Using the following reduction pair

          Linear polynomial interpretation over the naturals

          [__ (x1, x2) ]	=	3 x1 + x2 + 1
          [a]	=	0
          [isNePal (x1) ]	=	2 x1 + 2
          [U21 (x1, x2, x3) ]	=	0
          [U41 (x1, x2, x3) ]	=	0
          [i]	=	0
          [U72 (x1) ]	=	0
          [U61 (x1, x2) ]	=	x1
          [and (x1, x2) ]	=	2 x1 + x2 + 1
          [U31 (x1, x2) ]	=	0
          [U71 (x1, x2) ]	=	0
          [a__U23 (x1) ]	=	0
          [isNeList (x1) ]	=	0
          [a__isPal (x1) ]	=	2 x1 + 1
          [isPal (x1) ]	=	2 x1 + 1
          [a__U72 (x1) ]	=	0
          [mark# (x1) ]	=	x1
          [a__U71 (x1, x2) ]	=	0
          [tt]	=	0
          [o]	=	0
          [a__and (x1, x2) ]	=	2 x1 + x2 + 1
          [e]	=	0
          [a__U22 (x1, x2) ]	=	0
          [a__U21 (x1, x2, x3) ]	=	0
          [a__U32 (x1) ]	=	0
          [a__isNePal (x1) ]	=	2 x1 + 2
          [U23 (x1) ]	=	0
          [U53 (x1) ]	=	0
          [U51 (x1, x2, x3) ]	=	0
          [a__U41 (x1, x2, x3) ]	=	0
          [a__isQid (x1) ]	=	0
          [a____ (x1, x2) ]	=	3 x1 + x2 + 1
          [U62 (x1) ]	=	0
          [a__U62 (x1) ]	=	0
          [a__U53 (x1) ]	=	0
          [a__U42 (x1, x2) ]	=	0
          [a__U31 (x1, x2) ]	=	0
          [u]	=	3
          [U22 (x1, x2) ]	=	0
          [a__U61 (x1, x2) ]	=	x1
          [U32 (x1) ]	=	0
          [isList (x1) ]	=	0
          [a__U11 (x1, x2) ]	=	0
          [mark (x1) ]	=	x1
          [a__U52 (x1, x2) ]	=	0
          [a__isPalListKind (x1) ]	=	x1
          [U52 (x1, x2) ]	=	0
          [a__and# (x1, x2) ]	=	x1
          [nil]	=	0
          [a__isNeList (x1) ]	=	0
          [U42 (x1, x2) ]	=	0
          [isPalListKind (x1) ]	=	x1
          [a__U51 (x1, x2, x3) ]	=	0
          [U11 (x1, x2) ]	=	0
          [isQid (x1) ]	=	0
          [a__U12 (x1) ]	=	0
          [a__isList (x1) ]	=	0
          [U43 (x1) ]	=	2 x1
          [a__U43 (x1) ]	=	2 x1
          [U12 (x1) ]	=	0
          [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

          one remains with the following pair(s).

          mark#( U43( X ) )	→	mark#( X )
          a__and#( tt , X )	→	mark#( X )

          1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1: dependency graph processor

          The dependency pairs are split into 1 component(s).

          • The 1st component contains the pair(s)

            mark#( U43( X ) )

            →

            mark#( X )

            1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1: reduction pair processor

            Using the following reduction pair

            Linear polynomial interpretation over the naturals

            [__ (x1, x2) ]	=	2 x1 + x2 + 2
            [a]	=	0
            [isNePal (x1) ]	=	0
            [U21 (x1, x2, x3) ]	=	0
            [U41 (x1, x2, x3) ]	=	2 x1 + 1
            [i]	=	0
            [U72 (x1) ]	=	0
            [U61 (x1, x2) ]	=	0
            [and (x1, x2) ]	=	2 x1
            [U31 (x1, x2) ]	=	2 x1
            [U71 (x1, x2) ]	=	0
            [a__U23 (x1) ]	=	0
            [isNeList (x1) ]	=	2 x1
            [a__isPal (x1) ]	=	0
            [isPal (x1) ]	=	0
            [a__U72 (x1) ]	=	0
            [mark# (x1) ]	=	x1
            [a__U71 (x1, x2) ]	=	0
            [tt]	=	0
            [o]	=	0
            [a__and (x1, x2) ]	=	2 x1
            [e]	=	0
            [a__U22 (x1, x2) ]	=	0
            [a__U21 (x1, x2, x3) ]	=	0
            [a__U32 (x1) ]	=	0
            [a__isNePal (x1) ]	=	0
            [U23 (x1) ]	=	0
            [U53 (x1) ]	=	0
            [U51 (x1, x2, x3) ]	=	0
            [a__U41 (x1, x2, x3) ]	=	2 x1 + 1
            [a__isQid (x1) ]	=	0
            [a____ (x1, x2) ]	=	2 x1 + x2 + 2
            [U62 (x1) ]	=	0
            [a__U62 (x1) ]	=	0
            [a__U53 (x1) ]	=	0
            [a__U42 (x1, x2) ]	=	2 x1 + 1
            [a__U31 (x1, x2) ]	=	2 x1
            [u]	=	0
            [U22 (x1, x2) ]	=	0
            [a__U61 (x1, x2) ]	=	0
            [U32 (x1) ]	=	0
            [isList (x1) ]	=	0
            [a__U11 (x1, x2) ]	=	0
            [mark (x1) ]	=	x1
            [a__U52 (x1, x2) ]	=	0
            [a__isPalListKind (x1) ]	=	0
            [U52 (x1, x2) ]	=	0
            [nil]	=	0
            [a__isNeList (x1) ]	=	2 x1
            [U42 (x1, x2) ]	=	2 x1 + 1
            [isPalListKind (x1) ]	=	0
            [a__U51 (x1, x2, x3) ]	=	0
            [U11 (x1, x2) ]	=	0
            [isQid (x1) ]	=	0
            [a__isList (x1) ]	=	0
            [a__U12 (x1) ]	=	0
            [U43 (x1) ]	=	x1 + 1
            [a__U43 (x1) ]	=	x1 + 1
            [U12 (x1) ]	=	0
            [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

            one remains with the following pair(s).

            none

            1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1: P is empty

            All dependency pairs have been removed.