Termination proof

1: switching to dependency pairs

__#( __( X , Y ) , Z )	→	__#( X , __( Y , Z ) )
__#( __( X , Y ) , Z )	→	__#( Y , Z )
U11#( tt , V )	→	U12#( isPalListKind( activate( V ) ) , activate( V ) )
U11#( tt , V )	→	isPalListKind#( activate( V ) )
U11#( tt , V )	→	activate#( V )
U11#( tt , V )	→	activate#( V )
U12#( tt , V )	→	U13#( isNeList( activate( V ) ) )
U12#( tt , V )	→	isNeList#( activate( V ) )
U12#( tt , V )	→	activate#( V )
U21#( tt , V1 , V2 )	→	U22#( isPalListKind( activate( V1 ) ) , activate( V1 ) , activate( V2 ) )
U21#( tt , V1 , V2 )	→	isPalListKind#( activate( V1 ) )
U21#( tt , V1 , V2 )	→	activate#( V1 )
U21#( tt , V1 , V2 )	→	activate#( V1 )
U21#( tt , V1 , V2 )	→	activate#( V2 )
U22#( tt , V1 , V2 )	→	U23#( isPalListKind( activate( V2 ) ) , activate( V1 ) , activate( V2 ) )
U22#( tt , V1 , V2 )	→	isPalListKind#( activate( V2 ) )
U22#( tt , V1 , V2 )	→	activate#( V2 )
U22#( tt , V1 , V2 )	→	activate#( V1 )
U22#( tt , V1 , V2 )	→	activate#( V2 )
U23#( tt , V1 , V2 )	→	U24#( isPalListKind( activate( V2 ) ) , activate( V1 ) , activate( V2 ) )
U23#( tt , V1 , V2 )	→	isPalListKind#( activate( V2 ) )
U23#( tt , V1 , V2 )	→	activate#( V2 )
U23#( tt , V1 , V2 )	→	activate#( V1 )
U23#( tt , V1 , V2 )	→	activate#( V2 )
U24#( tt , V1 , V2 )	→	U25#( isList( activate( V1 ) ) , activate( V2 ) )
U24#( tt , V1 , V2 )	→	isList#( activate( V1 ) )
U24#( tt , V1 , V2 )	→	activate#( V1 )
U24#( tt , V1 , V2 )	→	activate#( V2 )
U25#( tt , V2 )	→	U26#( isList( activate( V2 ) ) )
U25#( tt , V2 )	→	isList#( activate( V2 ) )
U25#( tt , V2 )	→	activate#( V2 )
U31#( tt , V )	→	U32#( isPalListKind( activate( V ) ) , activate( V ) )
U31#( tt , V )	→	isPalListKind#( activate( V ) )
U31#( tt , V )	→	activate#( V )
U31#( tt , V )	→	activate#( V )
U32#( tt , V )	→	U33#( isQid( activate( V ) ) )
U32#( tt , V )	→	isQid#( activate( V ) )
U32#( tt , V )	→	activate#( V )
U41#( tt , V1 , V2 )	→	U42#( isPalListKind( activate( V1 ) ) , activate( V1 ) , activate( V2 ) )
U41#( tt , V1 , V2 )	→	isPalListKind#( activate( V1 ) )
U41#( tt , V1 , V2 )	→	activate#( V1 )
U41#( tt , V1 , V2 )	→	activate#( V1 )
U41#( tt , V1 , V2 )	→	activate#( V2 )
U42#( tt , V1 , V2 )	→	U43#( isPalListKind( activate( V2 ) ) , activate( V1 ) , activate( V2 ) )
U42#( tt , V1 , V2 )	→	isPalListKind#( activate( V2 ) )
U42#( tt , V1 , V2 )	→	activate#( V2 )
U42#( tt , V1 , V2 )	→	activate#( V1 )
U42#( tt , V1 , V2 )	→	activate#( V2 )
U43#( tt , V1 , V2 )	→	U44#( isPalListKind( activate( V2 ) ) , activate( V1 ) , activate( V2 ) )
U43#( tt , V1 , V2 )	→	isPalListKind#( activate( V2 ) )
U43#( tt , V1 , V2 )	→	activate#( V2 )
U43#( tt , V1 , V2 )	→	activate#( V1 )
U43#( tt , V1 , V2 )	→	activate#( V2 )
U44#( tt , V1 , V2 )	→	U45#( isList( activate( V1 ) ) , activate( V2 ) )
U44#( tt , V1 , V2 )	→	isList#( activate( V1 ) )
U44#( tt , V1 , V2 )	→	activate#( V1 )
U44#( tt , V1 , V2 )	→	activate#( V2 )
U45#( tt , V2 )	→	U46#( isNeList( activate( V2 ) ) )
U45#( tt , V2 )	→	isNeList#( activate( V2 ) )
U45#( tt , V2 )	→	activate#( V2 )
U51#( tt , V1 , V2 )	→	U52#( isPalListKind( activate( V1 ) ) , activate( V1 ) , activate( V2 ) )
U51#( tt , V1 , V2 )	→	isPalListKind#( activate( V1 ) )
U51#( tt , V1 , V2 )	→	activate#( V1 )
U51#( tt , V1 , V2 )	→	activate#( V1 )
U51#( tt , V1 , V2 )	→	activate#( V2 )
U52#( tt , V1 , V2 )	→	U53#( isPalListKind( activate( V2 ) ) , activate( V1 ) , activate( V2 ) )
U52#( tt , V1 , V2 )	→	isPalListKind#( activate( V2 ) )
U52#( tt , V1 , V2 )	→	activate#( V2 )
U52#( tt , V1 , V2 )	→	activate#( V1 )
U52#( tt , V1 , V2 )	→	activate#( V2 )
U53#( tt , V1 , V2 )	→	U54#( isPalListKind( activate( V2 ) ) , activate( V1 ) , activate( V2 ) )
U53#( tt , V1 , V2 )	→	isPalListKind#( activate( V2 ) )
U53#( tt , V1 , V2 )	→	activate#( V2 )
U53#( tt , V1 , V2 )	→	activate#( V1 )
U53#( tt , V1 , V2 )	→	activate#( V2 )
U54#( tt , V1 , V2 )	→	U55#( isNeList( activate( V1 ) ) , activate( V2 ) )
U54#( tt , V1 , V2 )	→	isNeList#( activate( V1 ) )
U54#( tt , V1 , V2 )	→	activate#( V1 )
U54#( tt , V1 , V2 )	→	activate#( V2 )
U55#( tt , V2 )	→	U56#( isList( activate( V2 ) ) )
U55#( tt , V2 )	→	isList#( activate( V2 ) )
U55#( tt , V2 )	→	activate#( V2 )
U61#( tt , V )	→	U62#( isPalListKind( activate( V ) ) , activate( V ) )
U61#( tt , V )	→	isPalListKind#( activate( V ) )
U61#( tt , V )	→	activate#( V )
U61#( tt , V )	→	activate#( V )
U62#( tt , V )	→	U63#( isQid( activate( V ) ) )
U62#( tt , V )	→	isQid#( activate( V ) )
U62#( tt , V )	→	activate#( V )
U71#( tt , I , P )	→	U72#( isPalListKind( activate( I ) ) , activate( P ) )
U71#( tt , I , P )	→	isPalListKind#( activate( I ) )
U71#( tt , I , P )	→	activate#( I )
U71#( tt , I , P )	→	activate#( P )
U72#( tt , P )	→	U73#( isPal( activate( P ) ) , activate( P ) )
U72#( tt , P )	→	isPal#( activate( P ) )
U72#( tt , P )	→	activate#( P )
U72#( tt , P )	→	activate#( P )
U73#( tt , P )	→	U74#( isPalListKind( activate( P ) ) )
U73#( tt , P )	→	isPalListKind#( activate( P ) )
U73#( tt , P )	→	activate#( P )
U81#( tt , V )	→	U82#( isPalListKind( activate( V ) ) , activate( V ) )
U81#( tt , V )	→	isPalListKind#( activate( V ) )
U81#( tt , V )	→	activate#( V )
U81#( tt , V )	→	activate#( V )
U82#( tt , V )	→	U83#( isNePal( activate( V ) ) )
U82#( tt , V )	→	isNePal#( activate( V ) )
U82#( tt , V )	→	activate#( V )
U91#( tt , V2 )	→	U92#( isPalListKind( activate( V2 ) ) )
U91#( tt , V2 )	→	isPalListKind#( activate( V2 ) )
U91#( tt , V2 )	→	activate#( V2 )
isList#( V )	→	U11#( isPalListKind( activate( V ) ) , activate( V ) )
isList#( V )	→	isPalListKind#( activate( V ) )
isList#( V )	→	activate#( V )
isList#( V )	→	activate#( V )
isList#( n____( V1 , V2 ) )	→	U21#( isPalListKind( activate( V1 ) ) , activate( V1 ) , activate( V2 ) )
isList#( n____( V1 , V2 ) )	→	isPalListKind#( activate( V1 ) )
isList#( n____( V1 , V2 ) )	→	activate#( V1 )
isList#( n____( V1 , V2 ) )	→	activate#( V1 )
isList#( n____( V1 , V2 ) )	→	activate#( V2 )
isNeList#( V )	→	U31#( isPalListKind( activate( V ) ) , activate( V ) )
isNeList#( V )	→	isPalListKind#( activate( V ) )
isNeList#( V )	→	activate#( V )
isNeList#( V )	→	activate#( V )
isNeList#( n____( V1 , V2 ) )	→	U41#( isPalListKind( activate( V1 ) ) , activate( V1 ) , activate( V2 ) )
isNeList#( n____( V1 , V2 ) )	→	isPalListKind#( activate( V1 ) )
isNeList#( n____( V1 , V2 ) )	→	activate#( V1 )
isNeList#( n____( V1 , V2 ) )	→	activate#( V1 )
isNeList#( n____( V1 , V2 ) )	→	activate#( V2 )
isNeList#( n____( V1 , V2 ) )	→	U51#( isPalListKind( activate( V1 ) ) , activate( V1 ) , activate( V2 ) )
isNeList#( n____( V1 , V2 ) )	→	isPalListKind#( activate( V1 ) )
isNeList#( n____( V1 , V2 ) )	→	activate#( V1 )
isNeList#( n____( V1 , V2 ) )	→	activate#( V1 )
isNeList#( n____( V1 , V2 ) )	→	activate#( V2 )
isNePal#( V )	→	U61#( isPalListKind( activate( V ) ) , activate( V ) )
isNePal#( V )	→	isPalListKind#( activate( V ) )
isNePal#( V )	→	activate#( V )
isNePal#( V )	→	activate#( V )
isNePal#( n____( I , __( P , I ) ) )	→	U71#( isQid( activate( I ) ) , activate( I ) , activate( P ) )
isNePal#( n____( I , __( P , I ) ) )	→	isQid#( activate( I ) )
isNePal#( n____( I , __( P , I ) ) )	→	activate#( I )
isNePal#( n____( I , __( P , I ) ) )	→	activate#( I )
isNePal#( n____( I , __( P , I ) ) )	→	activate#( P )
isPal#( V )	→	U81#( isPalListKind( activate( V ) ) , activate( V ) )
isPal#( V )	→	isPalListKind#( activate( V ) )
isPal#( V )	→	activate#( V )
isPal#( V )	→	activate#( V )
isPalListKind#( n____( V1 , V2 ) )	→	U91#( isPalListKind( activate( V1 ) ) , activate( V2 ) )
isPalListKind#( n____( V1 , V2 ) )	→	isPalListKind#( activate( V1 ) )
isPalListKind#( n____( V1 , V2 ) )	→	activate#( V1 )
isPalListKind#( n____( V1 , V2 ) )	→	activate#( V2 )
activate#( n__nil )	→	nil#
activate#( n____( X1 , X2 ) )	→	__#( X1 , X2 )
activate#( n__a )	→	a#
activate#( n__e )	→	e#
activate#( n__i )	→	i#
activate#( n__o )	→	o#
activate#( n__u )	→	u#

1.1: dependency graph processor

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

• The 1st component contains the pair(s)

  U11#( tt , V )	→	U12#( isPalListKind( activate( V ) ) , activate( V ) )
  U12#( tt , V )	→	isNeList#( activate( V ) )
  isNeList#( n____( V1 , V2 ) )	→	U41#( isPalListKind( activate( V1 ) ) , activate( V1 ) , activate( V2 ) )
  U41#( tt , V1 , V2 )	→	U42#( isPalListKind( activate( V1 ) ) , activate( V1 ) , activate( V2 ) )
  U42#( tt , V1 , V2 )	→	U43#( isPalListKind( activate( V2 ) ) , activate( V1 ) , activate( V2 ) )
  U43#( tt , V1 , V2 )	→	U44#( isPalListKind( activate( V2 ) ) , activate( V1 ) , activate( V2 ) )
  U44#( tt , V1 , V2 )	→	U45#( isList( activate( V1 ) ) , activate( V2 ) )
  U45#( tt , V2 )	→	isNeList#( activate( V2 ) )
  isNeList#( n____( V1 , V2 ) )	→	U51#( isPalListKind( activate( V1 ) ) , activate( V1 ) , activate( V2 ) )
  U51#( tt , V1 , V2 )	→	U52#( isPalListKind( activate( V1 ) ) , activate( V1 ) , activate( V2 ) )
  U52#( tt , V1 , V2 )	→	U53#( isPalListKind( activate( V2 ) ) , activate( V1 ) , activate( V2 ) )
  U53#( tt , V1 , V2 )	→	U54#( isPalListKind( activate( V2 ) ) , activate( V1 ) , activate( V2 ) )
  U54#( tt , V1 , V2 )	→	U55#( isNeList( activate( V1 ) ) , activate( V2 ) )
  U55#( tt , V2 )	→	isList#( activate( V2 ) )
  isList#( V )	→	U11#( isPalListKind( activate( V ) ) , activate( V ) )
  isList#( n____( V1 , V2 ) )	→	U21#( isPalListKind( activate( V1 ) ) , activate( V1 ) , activate( V2 ) )
  U21#( tt , V1 , V2 )	→	U22#( isPalListKind( activate( V1 ) ) , activate( V1 ) , activate( V2 ) )
  U22#( tt , V1 , V2 )	→	U23#( isPalListKind( activate( V2 ) ) , activate( V1 ) , activate( V2 ) )
  U23#( tt , V1 , V2 )	→	U24#( isPalListKind( activate( V2 ) ) , activate( V1 ) , activate( V2 ) )
  U24#( tt , V1 , V2 )	→	U25#( isList( activate( V1 ) ) , activate( V2 ) )
  U25#( tt , V2 )	→	isList#( activate( V2 ) )
  U24#( tt , V1 , V2 )	→	isList#( activate( V1 ) )
  U54#( tt , V1 , V2 )	→	isNeList#( activate( V1 ) )
  U44#( tt , V1 , V2 )	→	isList#( activate( V1 ) )

  1.1.1: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [U72 (x1, x2) ]	=	1
  [U55# (x1, x2) ]	=	2 x1 + 3
  [U45# (x1, x2) ]	=	2 x1 + 2
  [a]	=	0
  [__ (x1, x2) ]	=	2 x1 + x2 + 3
  [isNePal (x1) ]	=	2
  [U25 (x1, x2) ]	=	0
  [U21 (x1, x2, x3) ]	=	0
  [U12 (x1, x2) ]	=	0
  [U41# (x1, x2, x3) ]	=	3 x1 + 2 x2 + 3
  [U41 (x1, x2, x3) ]	=	3 x1 + x2
  [i]	=	0
  [U52# (x1, x2, x3) ]	=	2 x1 + 2 x2 + 3
  [activate (x1) ]	=	x1
  [U42# (x1, x2, x3) ]	=	2 x1 + 2 x2 + 3
  [U33 (x1) ]	=	0
  [U31 (x1, x2) ]	=	2 x1
  [U61 (x1, x2) ]	=	0
  [n__o]	=	0
  [isNeList (x1) ]	=	2 x1
  [U45 (x1, x2) ]	=	0
  [isPal (x1) ]	=	2
  [U23 (x1, x2, x3) ]	=	0
  [n____ (x1, x2) ]	=	2 x1 + x2 + 3
  [U22# (x1, x2, x3) ]	=	3 x1 + 2 x2 + 3
  [U51# (x1, x2, x3) ]	=	3 x1 + 2 x2 + 3
  [n__e]	=	0
  [U71 (x1, x2, x3) ]	=	2
  [U73 (x1, x2) ]	=	1
  [tt]	=	0
  [o]	=	0
  [U21# (x1, x2, x3) ]	=	3 x1 + 2 x2 + 3
  [e]	=	0
  [n__a]	=	0
  [n__u]	=	0
  [U25# (x1, x2) ]	=	2 x1 + 3
  [U51 (x1, x2, x3) ]	=	3 x1 + 2 x2
  [U44# (x1, x2, x3) ]	=	2 x1 + 2 x2 + 3
  [U74 (x1) ]	=	1
  [isList# (x1) ]	=	2 x1 + 3
  [U24# (x1, x2, x3) ]	=	2 x1 + 2 x2 + 3
  [U63 (x1) ]	=	0
  [U13 (x1) ]	=	0
  [U52 (x1, x2, x3) ]	=	2 x1
  [U55 (x1, x2) ]	=	0
  [U32 (x1, x2) ]	=	0
  [U91 (x1, x2) ]	=	0
  [u]	=	0
  [U53# (x1, x2, x3) ]	=	2 x1 + 2 x2 + 3
  [U56 (x1) ]	=	0
  [U43 (x1, x2, x3) ]	=	0
  [U44 (x1, x2, x3) ]	=	0
  [U42 (x1, x2, x3) ]	=	0
  [isList (x1) ]	=	0
  [U11# (x1, x2) ]	=	2 x1 + 3
  [U92 (x1) ]	=	0
  [U23# (x1, x2, x3) ]	=	2 x1 + 2 x2 + 3
  [U53 (x1, x2, x3) ]	=	x1
  [U24 (x1, x2, x3) ]	=	0
  [U46 (x1) ]	=	0
  [n__nil]	=	0
  [U62 (x1, x2) ]	=	0
  [nil]	=	0
  [U12# (x1, x2) ]	=	2 x1 + 2
  [isPalListKind (x1) ]	=	0
  [U26 (x1) ]	=	0
  [U11 (x1, x2) ]	=	0
  [U81 (x1, x2) ]	=	1
  [isNeList# (x1) ]	=	2 x1 + 2
  [n__i]	=	0
  [U54# (x1, x2, x3) ]	=	2 x1 + 2 x2 + 3
  [U43# (x1, x2, x3) ]	=	2 x1 + 2 x2 + 3
  [isQid (x1) ]	=	0
  [U54 (x1, x2, x3) ]	=	0
  [U82 (x1, x2) ]	=	1
  [U22 (x1, x2, x3) ]	=	0
  [U83 (x1) ]	=	1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  U12#( tt , V )	→	isNeList#( activate( V ) )
  U41#( tt , V1 , V2 )	→	U42#( isPalListKind( activate( V1 ) ) , activate( V1 ) , activate( V2 ) )
  U42#( tt , V1 , V2 )	→	U43#( isPalListKind( activate( V2 ) ) , activate( V1 ) , activate( V2 ) )
  U43#( tt , V1 , V2 )	→	U44#( isPalListKind( activate( V2 ) ) , activate( V1 ) , activate( V2 ) )
  U45#( tt , V2 )	→	isNeList#( activate( V2 ) )
  U51#( tt , V1 , V2 )	→	U52#( isPalListKind( activate( V1 ) ) , activate( V1 ) , activate( V2 ) )
  U52#( tt , V1 , V2 )	→	U53#( isPalListKind( activate( V2 ) ) , activate( V1 ) , activate( V2 ) )
  U53#( tt , V1 , V2 )	→	U54#( isPalListKind( activate( V2 ) ) , activate( V1 ) , activate( V2 ) )
  U54#( tt , V1 , V2 )	→	U55#( isNeList( activate( V1 ) ) , activate( V2 ) )
  U55#( tt , V2 )	→	isList#( activate( V2 ) )
  isList#( V )	→	U11#( isPalListKind( activate( V ) ) , activate( V ) )
  U21#( tt , V1 , V2 )	→	U22#( isPalListKind( activate( V1 ) ) , activate( V1 ) , activate( V2 ) )
  U22#( tt , V1 , V2 )	→	U23#( isPalListKind( activate( V2 ) ) , activate( V1 ) , activate( V2 ) )
  U23#( tt , V1 , V2 )	→	U24#( isPalListKind( activate( V2 ) ) , activate( V1 ) , activate( V2 ) )
  U24#( tt , V1 , V2 )	→	U25#( isList( activate( V1 ) ) , activate( V2 ) )
  U25#( tt , V2 )	→	isList#( activate( V2 ) )
  U24#( tt , V1 , V2 )	→	isList#( activate( V1 ) )
  U44#( tt , V1 , V2 )	→	isList#( activate( V1 ) )

  1.1.1.1: dependency graph processor

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

• The 2nd component contains the pair(s)

  isNePal#( n____( I , __( P , I ) ) )	→	U71#( isQid( activate( I ) ) , activate( I ) , activate( P ) )
  U71#( tt , I , P )	→	U72#( isPalListKind( activate( I ) ) , activate( P ) )
  U72#( tt , P )	→	isPal#( activate( P ) )
  isPal#( V )	→	U81#( isPalListKind( activate( V ) ) , activate( V ) )
  U81#( tt , V )	→	U82#( isPalListKind( activate( V ) ) , activate( V ) )
  U82#( tt , V )	→	isNePal#( activate( V ) )

  1.1.2: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [U72 (x1, x2) ]	=	3 x1 + 3
  [a]	=	0
  [__ (x1, x2) ]	=	2 x1 + x2 + 2
  [isNePal (x1) ]	=	2 x1
  [U25 (x1, x2) ]	=	0
  [U21 (x1, x2, x3) ]	=	3 x1 + x2 + 3
  [U12 (x1, x2) ]	=	x1
  [U41 (x1, x2, x3) ]	=	2 x1 + 2 x2 + 3
  [i]	=	0
  [U71# (x1, x2, x3) ]	=	2 x1
  [activate (x1) ]	=	x1
  [U61 (x1, x2) ]	=	x1
  [U31 (x1, x2) ]	=	x1 + 3
  [U33 (x1) ]	=	0
  [n__o]	=	0
  [isNeList (x1) ]	=	2 x1 + 3
  [U45 (x1, x2) ]	=	2 x1 + 1
  [isPal (x1) ]	=	0
  [n____ (x1, x2) ]	=	2 x1 + x2 + 2
  [U23 (x1, x2, x3) ]	=	3 x1 + x2
  [U72# (x1, x2) ]	=	2 x1
  [n__e]	=	0
  [U71 (x1, x2, x3) ]	=	3 x1 + 3 x2 + 3
  [U73 (x1, x2) ]	=	3
  [tt]	=	0
  [o]	=	0
  [e]	=	0
  [n__a]	=	0
  [n__u]	=	0
  [U51 (x1, x2, x3) ]	=	3 x1 + x2 + 2
  [U74 (x1) ]	=	2
  [isPal# (x1) ]	=	2 x1
  [U63 (x1) ]	=	0
  [U13 (x1) ]	=	0
  [U52 (x1, x2, x3) ]	=	x1 + 2
  [U55 (x1, x2) ]	=	0
  [U32 (x1, x2) ]	=	3
  [U91 (x1, x2) ]	=	0
  [U82# (x1, x2) ]	=	2 x1
  [u]	=	0
  [U56 (x1) ]	=	0
  [U43 (x1, x2, x3) ]	=	x1 + 2 x2 + 2
  [U44 (x1, x2, x3) ]	=	2 x1 + 1
  [isList (x1) ]	=	2 x1 + 2
  [U42 (x1, x2, x3) ]	=	x1 + 2 x2 + 3
  [U92 (x1) ]	=	0
  [U24 (x1, x2, x3) ]	=	x1
  [U53 (x1, x2, x3) ]	=	x1 + 1
  [U46 (x1) ]	=	0
  [n__nil]	=	0
  [U62 (x1, x2) ]	=	0
  [nil]	=	0
  [U81# (x1, x2) ]	=	2 x1
  [isPalListKind (x1) ]	=	0
  [U11 (x1, x2) ]	=	2 x1 + 2
  [U26 (x1) ]	=	0
  [U81 (x1, x2) ]	=	0
  [n__i]	=	0
  [isNePal# (x1) ]	=	2 x1
  [isQid (x1) ]	=	0
  [U54 (x1, x2, x3) ]	=	x1
  [U82 (x1, x2) ]	=	0
  [U22 (x1, x2, x3) ]	=	3 x1 + x2 + 3
  [U83 (x1) ]	=	0
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  U71#( tt , I , P )	→	U72#( isPalListKind( activate( I ) ) , activate( P ) )
  U72#( tt , P )	→	isPal#( activate( P ) )
  isPal#( V )	→	U81#( isPalListKind( activate( V ) ) , activate( V ) )
  U81#( tt , V )	→	U82#( isPalListKind( activate( V ) ) , activate( V ) )
  U82#( tt , V )	→	isNePal#( activate( V ) )

  1.1.2.1: dependency graph processor

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

• The 3rd component contains the pair(s)

  U91#( tt , V2 )	→	isPalListKind#( activate( V2 ) )
  isPalListKind#( n____( V1 , V2 ) )	→	U91#( isPalListKind( activate( V1 ) ) , activate( V2 ) )
  isPalListKind#( n____( V1 , V2 ) )	→	isPalListKind#( activate( V1 ) )

  1.1.3: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [U72 (x1, x2) ]	=	0
  [a]	=	0
  [__ (x1, x2) ]	=	x1 + x2 + 1
  [U25 (x1, x2) ]	=	0
  [isNePal (x1) ]	=	1
  [U21 (x1, x2, x3) ]	=	0
  [U12 (x1, x2) ]	=	0
  [U41 (x1, x2, x3) ]	=	0
  [i]	=	0
  [activate (x1) ]	=	x1
  [U33 (x1) ]	=	0
  [U31 (x1, x2) ]	=	0
  [U61 (x1, x2) ]	=	1
  [n__o]	=	0
  [isNeList (x1) ]	=	0
  [U45 (x1, x2) ]	=	0
  [isPal (x1) ]	=	0
  [isPalListKind# (x1) ]	=	x1
  [n____ (x1, x2) ]	=	x1 + x2 + 1
  [U23 (x1, x2, x3) ]	=	0
  [n__e]	=	0
  [U71 (x1, x2, x3) ]	=	0
  [U73 (x1, x2) ]	=	0
  [tt]	=	0
  [o]	=	0
  [e]	=	0
  [n__a]	=	0
  [n__u]	=	0
  [U51 (x1, x2, x3) ]	=	0
  [U74 (x1) ]	=	0
  [U63 (x1) ]	=	1
  [U13 (x1) ]	=	0
  [U52 (x1, x2, x3) ]	=	0
  [U55 (x1, x2) ]	=	0
  [U32 (x1, x2) ]	=	0
  [U91# (x1, x2) ]	=	x1
  [U91 (x1, x2) ]	=	0
  [u]	=	0
  [U56 (x1) ]	=	0
  [U43 (x1, x2, x3) ]	=	0
  [U44 (x1, x2, x3) ]	=	0
  [U42 (x1, x2, x3) ]	=	0
  [isList (x1) ]	=	0
  [U92 (x1) ]	=	0
  [U24 (x1, x2, x3) ]	=	0
  [U53 (x1, x2, x3) ]	=	0
  [n__nil]	=	0
  [U46 (x1) ]	=	0
  [U62 (x1, x2) ]	=	1
  [nil]	=	0
  [isPalListKind (x1) ]	=	0
  [U11 (x1, x2) ]	=	0
  [U26 (x1) ]	=	0
  [U81 (x1, x2) ]	=	0
  [n__i]	=	0
  [isQid (x1) ]	=	0
  [U54 (x1, x2, x3) ]	=	0
  [U82 (x1, x2) ]	=	0
  [U83 (x1) ]	=	0
  [U22 (x1, x2, x3) ]	=	0
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  U91#( tt , V2 )

  →

  isPalListKind#( activate( V2 ) )

  1.1.3.1: dependency graph processor

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

• The 4th component contains the pair(s)

  __#( __( X , Y ) , Z )	→	__#( Y , Z )
  __#( __( X , Y ) , Z )	→	__#( X , __( Y , Z ) )

  1.1.4: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [U72 (x1, x2) ]	=	0
  [a]	=	0
  [__ (x1, x2) ]	=	x1 + x2 + 2
  [U25 (x1, x2) ]	=	0
  [isNePal (x1) ]	=	0
  [U21 (x1, x2, x3) ]	=	0
  [U12 (x1, x2) ]	=	0
  [U41 (x1, x2, x3) ]	=	x1 + 3
  [i]	=	0
  [activate (x1) ]	=	2 x1
  [U33 (x1) ]	=	1
  [U31 (x1, x2) ]	=	1
  [U61 (x1, x2) ]	=	0
  [n__o]	=	0
  [isNeList (x1) ]	=	2 x1 + 1
  [U45 (x1, x2) ]	=	2
  [isPal (x1) ]	=	x1 + 2
  [n____ (x1, x2) ]	=	x1 + x2 + 2
  [U23 (x1, x2, x3) ]	=	0
  [n__e]	=	0
  [U71 (x1, x2, x3) ]	=	0
  [U73 (x1, x2) ]	=	0
  [tt]	=	0
  [o]	=	0
  [e]	=	0
  [n__a]	=	0
  [n__u]	=	1
  [U51 (x1, x2, x3) ]	=	x1 + 1
  [U74 (x1) ]	=	0
  [U63 (x1) ]	=	0
  [U13 (x1) ]	=	0
  [U52 (x1, x2, x3) ]	=	0
  [__# (x1, x2) ]	=	2 x1 + 2 x2
  [U55 (x1, x2) ]	=	0
  [U32 (x1, x2) ]	=	1
  [U91 (x1, x2) ]	=	0
  [u]	=	2
  [U56 (x1) ]	=	0
  [U43 (x1, x2, x3) ]	=	3
  [U44 (x1, x2, x3) ]	=	3
  [U42 (x1, x2, x3) ]	=	3
  [isList (x1) ]	=	x1
  [U92 (x1) ]	=	0
  [U24 (x1, x2, x3) ]	=	0
  [U53 (x1, x2, x3) ]	=	0
  [U46 (x1) ]	=	1
  [n__nil]	=	2
  [U62 (x1, x2) ]	=	0
  [nil]	=	3
  [isPalListKind (x1) ]	=	0
  [U11 (x1, x2) ]	=	0
  [U26 (x1) ]	=	0
  [U81 (x1, x2) ]	=	2
  [n__i]	=	0
  [isQid (x1) ]	=	1
  [U54 (x1, x2, x3) ]	=	0
  [U82 (x1, x2) ]	=	0
  [U83 (x1) ]	=	0
  [U22 (x1, x2, x3) ]	=	0
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  __#( __( X , Y ) , Z )

  →

  __#( X , __( Y , Z ) )

  1.1.4.1: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [U72 (x1, x2) ]	=	0
  [a]	=	2
  [__ (x1, x2) ]	=	2 x1 + x2 + 2
  [U25 (x1, x2) ]	=	1
  [isNePal (x1) ]	=	0
  [U21 (x1, x2, x3) ]	=	1
  [U12 (x1, x2) ]	=	0
  [U41 (x1, x2, x3) ]	=	3 x1
  [i]	=	2
  [activate (x1) ]	=	x1 + 2
  [U33 (x1) ]	=	1
  [U31 (x1, x2) ]	=	2
  [U61 (x1, x2) ]	=	0
  [n__o]	=	0
  [isNeList (x1) ]	=	3 x1 + 3
  [U45 (x1, x2) ]	=	0
  [isPal (x1) ]	=	1
  [n____ (x1, x2) ]	=	2 x1 + x2 + 2
  [U23 (x1, x2, x3) ]	=	1
  [n__e]	=	0
  [U71 (x1, x2, x3) ]	=	0
  [U73 (x1, x2) ]	=	0
  [tt]	=	0
  [o]	=	2
  [e]	=	1
  [n__a]	=	0
  [n__u]	=	2
  [U51 (x1, x2, x3) ]	=	2 x1
  [U74 (x1) ]	=	0
  [U63 (x1) ]	=	0
  [U13 (x1) ]	=	0
  [U52 (x1, x2, x3) ]	=	0
  [__# (x1, x2) ]	=	2 x1
  [U55 (x1, x2) ]	=	0
  [U32 (x1, x2) ]	=	2
  [U91 (x1, x2) ]	=	0
  [u]	=	3
  [U56 (x1) ]	=	0
  [U43 (x1, x2, x3) ]	=	0
  [U44 (x1, x2, x3) ]	=	0
  [U42 (x1, x2, x3) ]	=	0
  [isList (x1) ]	=	2
  [U92 (x1) ]	=	0
  [U24 (x1, x2, x3) ]	=	1
  [U53 (x1, x2, x3) ]	=	0
  [U46 (x1) ]	=	0
  [n__nil]	=	0
  [U62 (x1, x2) ]	=	0
  [nil]	=	0
  [isPalListKind (x1) ]	=	0
  [U11 (x1, x2) ]	=	2
  [U26 (x1) ]	=	1
  [U81 (x1, x2) ]	=	1
  [n__i]	=	0
  [isQid (x1) ]	=	x1
  [U54 (x1, x2, x3) ]	=	0
  [U82 (x1, x2) ]	=	1
  [U83 (x1) ]	=	0
  [U22 (x1, x2, x3) ]	=	1
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  none

  1.1.4.1.1: P is empty

  All dependency pairs have been removed.