YES
Welcome to CiME version 2.02 - Built on 14/04/2004 13:29:51

- : unit = ()
- : unit = ()
X : variable_set = <variable set>

F : signature = <signature>
R : HTRS = { __(__(X,Y),Z) -> __(X,__(Y,Z)),
             __(X,nil) -> X,
             __(nil,X) -> X,
             U11(tt,V) -> U12(isPalListKind(V),V),
             U12(tt,V) -> U13(isNeList(V)),
             U13(tt) -> tt,
             U21(tt,V1,V2) -> U22(isPalListKind(V1),V1,V2),
             U22(tt,V1,V2) -> U23(isPalListKind(V2),V1,V2),
             U23(tt,V1,V2) -> U24(isPalListKind(V2),V1,V2),
             U24(tt,V1,V2) -> U25(isList(V1),V2),
             U25(tt,V2) -> U26(isList(V2)),
             U26(tt) -> tt,
             U31(tt,V) -> U32(isPalListKind(V),V),
             U32(tt,V) -> U33(isQid(V)),
             U33(tt) -> tt,
             U41(tt,V1,V2) -> U42(isPalListKind(V1),V1,V2),
             U42(tt,V1,V2) -> U43(isPalListKind(V2),V1,V2),
             U43(tt,V1,V2) -> U44(isPalListKind(V2),V1,V2),
             U44(tt,V1,V2) -> U45(isList(V1),V2),
             U45(tt,V2) -> U46(isNeList(V2)),
             U46(tt) -> tt,
             U51(tt,V1,V2) -> U52(isPalListKind(V1),V1,V2),
             U52(tt,V1,V2) -> U53(isPalListKind(V2),V1,V2),
             U53(tt,V1,V2) -> U54(isPalListKind(V2),V1,V2),
             U54(tt,V1,V2) -> U55(isNeList(V1),V2),
             U55(tt,V2) -> U56(isList(V2)),
             U56(tt) -> tt,
             U61(tt,V) -> U62(isPalListKind(V),V),
             U62(tt,V) -> U63(isQid(V)),
             U63(tt) -> tt,
             U71(tt,I,P) -> U72(isPalListKind(I),P),
             U72(tt,P) -> U73(isPal(P),P),
             U73(tt,P) -> U74(isPalListKind(P)),
             U74(tt) -> tt,
             U81(tt,V) -> U82(isPalListKind(V),V),
             U82(tt,V) -> U83(isNePal(V)),
             U83(tt) -> tt,
             U91(tt,V2) -> U92(isPalListKind(V2)),
             U92(tt) -> tt,
             isList(V) -> U11(isPalListKind(V),V),
             isList(nil) -> tt,
             isList(__(V1,V2)) -> U21(isPalListKind(V1),V1,V2),
             isNeList(V) -> U31(isPalListKind(V),V),
             isNeList(__(V1,V2)) -> U41(isPalListKind(V1),V1,V2),
             isNeList(__(V1,V2)) -> U51(isPalListKind(V1),V1,V2),
             isNePal(V) -> U61(isPalListKind(V),V),
             isNePal(__(I,__(P,I))) -> U71(isQid(I),I,P),
             isPal(V) -> U81(isPalListKind(V),V),
             isPal(nil) -> tt,
             isPalListKind(a) -> tt,
             isPalListKind(e) -> tt,
             isPalListKind(i) -> tt,
             isPalListKind(nil) -> tt,
             isPalListKind(o) -> tt,
             isPalListKind(u) -> tt,
             isPalListKind(__(V1,V2)) -> U91(isPalListKind(V1),V2),
             isQid(a) -> tt,
             isQid(e) -> tt,
             isQid(i) -> tt,
             isQid(o) -> tt,
             isQid(u) -> tt } (61 rules)
Termination now uses minimal decomposition
- : unit = ()
Entering the termination expert for modules. Verbose level = 0
Checking module:
{}

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{}

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{}

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{}

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{}

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{}

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U92(tt) -> tt } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{}

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ __(__(V_7,V_6),V_5) -> __(V_7,__(V_6,V_5)),
  __(V_7,nil) -> V_7,
  __(nil,V_7) -> V_7 } (3 rules)

The dependency graph is
(1 nodes)
Checking each of the 1 strongly connected components :
Checking component 1
Trying simple graph criterion.
Trying to solve the following constraints:
(5 termination constraints)
Search parameters: linear polynomials, coefficient bound is 2.
Solution found for these constraints:
[nil] = 0;  [__](X0,X1) = X1 + X0 + 1;  ['__`](X0,X1) = X0;  

Checking module:
{ U91(tt,V_3) -> U92(isPalListKind(V_3)),
  isPalListKind(a) -> tt,
  isPalListKind(e) -> tt,
  isPalListKind(i) -> tt,
  isPalListKind(nil) -> tt,
  isPalListKind(o) -> tt,
  isPalListKind(u) -> tt,
  isPalListKind(__(V_2,V_3)) -> U91(isPalListKind(V_2),V_3) } (8 rules)

The dependency graph is
(1 nodes)
Checking each of the 1 strongly connected components :
Checking component 1
Trying simple graph criterion.
Trying to solve the following constraints:
(15 termination constraints)
Search parameters: linear polynomials, coefficient bound is 2.
Solution found for these constraints:
[tt] = 0; 
[U92](X0) = 0; 
[nil] = 0; 
[__](X0,X1) = X1 + X0 + 1; 
[a] = 0; 
[e] = 0; 
[i] = 0; 
[o] = 0; 
[u] = 0; 
[isPalListKind](X0) = 0; 
[U91](X0,X1) = 0; 
['isPalListKind`](X0) = 2*X0; 
['U91`](X0,X1) = 2*X1 + 1; 


Checking module:
{ U83(tt) -> tt } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U74(tt) -> tt } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U73(tt,V_1) -> U74(isPalListKind(V_1)) } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U63(tt) -> tt } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ isQid(u) -> tt,
  isQid(o) -> tt,
  isQid(i) -> tt,
  isQid(e) -> tt,
  isQid(a) -> tt } (5 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U62(tt,V_4) -> U63(isQid(V_4)) } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U61(tt,V_4) -> U62(isPalListKind(V_4),V_4) } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ isNePal(V_4) -> U61(isPalListKind(V_4),V_4),
  isNePal(__(V_0,__(V_1,V_0))) -> U71(isQid(V_0),V_0,V_1),
  U82(tt,V_4) -> U83(isNePal(V_4)),
  U81(tt,V_4) -> U82(isPalListKind(V_4),V_4),
  isPal(nil) -> tt,
  isPal(V_4) -> U81(isPalListKind(V_4),V_4),
  U72(tt,V_1) -> U73(isPal(V_1),V_1),
  U71(tt,V_0,V_1) -> U72(isPalListKind(V_0),V_1) } (8 rules)

The dependency graph is
(1 nodes)
Checking each of the 1 strongly connected components :
Checking component 1
Trying simple graph criterion.
Trying to solve the following constraints:
(37 termination constraints)
Search parameters: linear polynomials, coefficient bound is 2.
Solution found for these constraints:
[tt] = 2; 
[U92](X0) = X0; 
[nil] = 2; 
[__](X0,X1) = X1 + 2*X0 + 1; 
[a] = 2; 
[e] = 2; 
[i] = 2; 
[o] = 2; 
[u] = 2; 
[isPalListKind](X0) = X0; 
[isQid](X0) = X0; 
[U63](X0) = 2; 
[U62](X0,X1) = 2; 
[U61](X0,X1) = 2; 
[U83](X0) = 2; 
[U74](X0) = 2; 
[U73](X0,X1) = 2; 
[U71](X0,X1,X2) = 2; 
[U91](X0,X1) = X1; 
[U72](X0,X1) = 2; 
[isPal](X0) = X0; 
[U81](X0,X1) = X0; 
[U82](X0,X1) = 2; 
[isNePal](X0) = 2; 
['U71`](X0,X1,X2) = 2*X2 + X1 + 1; 
['U72`](X0,X1) = 2*X1 + X0; 
['isPal`](X0) = 2*X0 + 1; 
['U81`](X0,X1) = X1 + X0; 
['U82`](X0,X1) = X1 + 1; 
['isNePal`](X0) = X0; 


Checking module:
{ U56(tt) -> tt } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U26(tt) -> tt } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U13(tt) -> tt } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U46(tt) -> tt } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U33(tt) -> tt } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U32(tt,V_4) -> U33(isQid(V_4)) } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U31(tt,V_4) -> U32(isPalListKind(V_4),V_4) } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U55(tt,V_3) -> U56(isList(V_3)),
  U54(tt,V_2,V_3) -> U55(isNeList(V_2),V_3),
  U53(tt,V_2,V_3) -> U54(isPalListKind(V_3),V_2,V_3),
  U52(tt,V_2,V_3) -> U53(isPalListKind(V_3),V_2,V_3),
  U51(tt,V_2,V_3) -> U52(isPalListKind(V_2),V_2,V_3),
  isNeList(V_4) -> U31(isPalListKind(V_4),V_4),
  isNeList(__(V_2,V_3)) -> U41(isPalListKind(V_2),V_2,V_3),
  isNeList(__(V_2,V_3)) -> U51(isPalListKind(V_2),V_2,V_3),
  U12(tt,V_4) -> U13(isNeList(V_4)),
  U11(tt,V_4) -> U12(isPalListKind(V_4),V_4),
  isList(__(V_2,V_3)) -> U21(isPalListKind(V_2),V_2,V_3),
  isList(nil) -> tt,
  isList(V_4) -> U11(isPalListKind(V_4),V_4),
  U25(tt,V_3) -> U26(isList(V_3)),
  U24(tt,V_2,V_3) -> U25(isList(V_2),V_3),
  U23(tt,V_2,V_3) -> U24(isPalListKind(V_3),V_2,V_3),
  U22(tt,V_2,V_3) -> U23(isPalListKind(V_3),V_2,V_3),
  U21(tt,V_2,V_3) -> U22(isPalListKind(V_2),V_2,V_3),
  U45(tt,V_3) -> U46(isNeList(V_3)),
  U44(tt,V_2,V_3) -> U45(isList(V_2),V_3),
  U43(tt,V_2,V_3) -> U44(isPalListKind(V_3),V_2,V_3),
  U42(tt,V_2,V_3) -> U43(isPalListKind(V_3),V_2,V_3),
  U41(tt,V_2,V_3) -> U42(isPalListKind(V_2),V_2,V_3) } (23 rules)

The dependency graph is
(1 nodes)
Checking each of the 1 strongly connected components :
Checking component 1
Trying simple graph criterion.
Trying to solve the following constraints:
(71 termination constraints)
Search parameters: linear polynomials, coefficient bound is 2.
Time out for these parameters.
Search parameters: simple polynomials, coefficient bound is 3.
Solution found for these constraints:
[tt] = 3; 
[U56](X0) = 3; 
[U92](X0) = 3; 
[nil] = 3; 
[__](X0,X1) = 2*X1*X0 + 3*X1 + 3*X0 + 3; 
[a] = 3; 
[e] = 3; 
[i] = 3; 
[o] = 3; 
[u] = 3; 
[isPalListKind](X0) = X0; 
[isQid](X0) = X0; 
[U33](X0) = X0; 
[U32](X0,X1) = X1; 
[U31](X0,X1) = X1; 
[U13](X0) = 3; 
[U26](X0) = 3; 
[U46](X0) = 3; 
[U41](X0,X1,X2) = 3; 
[U91](X0,X1) = 3; 
[U42](X0,X1,X2) = 3; 
[U43](X0,X1,X2) = 3; 
[U44](X0,X1,X2) = 3; 
[U45](X0,X1) = 3; 
[U21](X0,X1,X2) = 3; 
[U22](X0,X1,X2) = 3; 
[U23](X0,X1,X2) = 3; 
[U24](X0,X1,X2) = 3; 
[U25](X0,X1) = 3; 
[isList](X0) = 3; 
[U11](X0,X1) = 3; 
[U12](X0,X1) = 3; 
[isNeList](X0) = X0; 
[U51](X0,X1,X2) = 3; 
[U52](X0,X1,X2) = 3; 
[U53](X0,X1,X2) = 3; 
[U54](X0,X1,X2) = 3; 
[U55](X0,X1) = 3; 
['U41`](X0,X1,X2) = 2*X2 + X1 + X0; 
['U42`](X0,X1,X2) = 2*X2 + X1 + 2; 
['U43`](X0,X1,X2) = 2*X2 + X1 + 1; 
['U44`](X0,X1,X2) = X2 + X1 + X0; 
['U45`](X0,X1) = X1 + 1; 
['U21`](X0,X1,X2) = 3*X2 + X1 + 3; 
['U22`](X0,X1,X2) = 3*X2 + X1 + 2; 
['U23`](X0,X1,X2) = 3*X2 + X1 + 1; 
['U24`](X0,X1,X2) = X2 + X1 + 2*X0; 
['U25`](X0,X1) = X1 + X0 + 1; 
['isList`](X0) = X0 + 3; 
['U11`](X0,X1) = X1 + 2; 
['U12`](X0,X1) = X1 + 1; 
['isNeList`](X0) = X0; 
['U51`](X0,X1,X2) = X2 + 2*X1 + X0 + 1; 
['U52`](X0,X1,X2) = X2 + 2*X1 + 3; 
['U53`](X0,X1,X2) = X2 + 2*X1 + 2; 
['U54`](X0,X1,X2) = X2 + 2*X1 + 1; 
['U55`](X0,X1) = X1 + 2*X0; 


Modular termination proof found.
- : unit = ()
The module
  {}
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

The module
  {}
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

The module
  {}
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

The module
  {}
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

The module
  {}
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

The module
  {}
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

The module
  { U92(tt) -> tt } (1 rules)
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

The module
  {}
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

The module
  { __(__(V_7,V_6),V_5) -> __(V_7,__(V_6,V_5)),
    __(V_7,nil) -> V_7,
    __(nil,V_7) -> V_7 } (3 rules)
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has one strongly connected component:
    0: '__`(__(V_7,V_6),V_5) ; '__`(V_6,V_5)
    1: '__`(__(V_7,V_6),V_5) ; '__`(V_7,__(V_6,V_5)) 
    0 -> 0, 0 -> 1, 1 -> 0, 1 -> 1, 
    On this component, the interpretation
    [nil] = 0;  [__](X0,X1) = X1 + X0 + 1;  ['__`](X0,X1) = X0;  
    strictly decreases on every cycle

The module
  { U91(tt,V_3) -> U92(isPalListKind(V_3)),
    isPalListKind(a) -> tt,
    isPalListKind(e) -> tt,
    isPalListKind(i) -> tt,
    isPalListKind(nil) -> tt,
    isPalListKind(o) -> tt,
    isPalListKind(u) -> tt,
    isPalListKind(__(V_2,V_3)) -> U91(isPalListKind(V_2),V_3) } (8 rules)
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has one strongly connected component:
    0: 'isPalListKind`(__(V_2,V_3)) ; 'isPalListKind`(V_2)
    1: 'isPalListKind`(__(V_2,V_3)) ; 'U91`(isPalListKind(V_2),V_3)
    2: 'U91`(tt,V_3) ; 'isPalListKind`(V_3) 
    0 -> 0, 0 -> 1, 1 -> 2, 2 -> 0, 2 -> 1, 
    On this component, the interpretation
    [tt] = 0; 
    [U92](X0) = 0; 
    [nil] = 0; 
    [__](X0,X1) = X1 + X0 + 1; 
    [a] = 0; 
    [e] = 0; 
    [i] = 0; 
    [o] = 0; 
    [u] = 0; 
    [isPalListKind](X0) = 0; 
    [U91](X0,X1) = 0; 
    ['isPalListKind`](X0) = 2*X0; 
    ['U91`](X0,X1) = 2*X1 + 1; 
     strictly decreases on every cycle

The module
  { U83(tt) -> tt } (1 rules)
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

The module
  { U74(tt) -> tt } (1 rules)
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

The module
  { U73(tt,V_1) -> U74(isPalListKind(V_1)) } (1 rules)
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

The module
  { U63(tt) -> tt } (1 rules)
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

The module
  { isQid(u) -> tt,
    isQid(o) -> tt,
    isQid(i) -> tt,
    isQid(e) -> tt,
    isQid(a) -> tt } (5 rules)
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

The module
  { U62(tt,V_4) -> U63(isQid(V_4)) } (1 rules)
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

The module
  { U61(tt,V_4) -> U62(isPalListKind(V_4),V_4) } (1 rules)
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

The module
  { isNePal(V_4) -> U61(isPalListKind(V_4),V_4),
    isNePal(__(V_0,__(V_1,V_0))) -> U71(isQid(V_0),V_0,V_1),
    U82(tt,V_4) -> U83(isNePal(V_4)),
    U81(tt,V_4) -> U82(isPalListKind(V_4),V_4),
    isPal(nil) -> tt,
    isPal(V_4) -> U81(isPalListKind(V_4),V_4),
    U72(tt,V_1) -> U73(isPal(V_1),V_1),
    U71(tt,V_0,V_1) -> U72(isPalListKind(V_0),V_1) } (8 rules)
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has one strongly connected component:
    0: 'U71`(tt,V_0,V_1) ; 'U72`(isPalListKind(V_0),V_1)
    1: 'U72`(tt,V_1) ; 'isPal`(V_1)
    2: 'isPal`(V_4) ; 'U81`(isPalListKind(V_4),V_4)
    3: 'U81`(tt,V_4) ; 'U82`(isPalListKind(V_4),V_4)
    4: 'U82`(tt,V_4) ; 'isNePal`(V_4)
    5: 'isNePal`(__(V_0,__(V_1,V_0))) ; 'U71`(isQid(V_0),V_0,V_1) 
    0 -> 1, 1 -> 2, 2 -> 3, 3 -> 4, 4 -> 5, 5 -> 0, 
    On this component, the interpretation
    [tt] = 2; 
    [U92](X0) = X0; 
    [nil] = 2; 
    [__](X0,X1) = X1 + 2*X0 + 1; 
    [a] = 2; 
    [e] = 2; 
    [i] = 2; 
    [o] = 2; 
    [u] = 2; 
    [isPalListKind](X0) = X0; 
    [isQid](X0) = X0; 
    [U63](X0) = 2; 
    [U62](X0,X1) = 2; 
    [U61](X0,X1) = 2; 
    [U83](X0) = 2; 
    [U74](X0) = 2; 
    [U73](X0,X1) = 2; 
    [U71](X0,X1,X2) = 2; 
    [U91](X0,X1) = X1; 
    [U72](X0,X1) = 2; 
    [isPal](X0) = X0; 
    [U81](X0,X1) = X0; 
    [U82](X0,X1) = 2; 
    [isNePal](X0) = 2; 
    ['U71`](X0,X1,X2) = 2*X2 + X1 + 1; 
    ['U72`](X0,X1) = 2*X1 + X0; 
    ['isPal`](X0) = 2*X0 + 1; 
    ['U81`](X0,X1) = X1 + X0; 
    ['U82`](X0,X1) = X1 + 1; 
    ['isNePal`](X0) = X0; 
     strictly decreases on every cycle

The module
  { U56(tt) -> tt } (1 rules)
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

The module
  { U26(tt) -> tt } (1 rules)
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

The module
  { U13(tt) -> tt } (1 rules)
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

The module
  { U46(tt) -> tt } (1 rules)
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

The module
  { U33(tt) -> tt } (1 rules)
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

The module
  { U32(tt,V_4) -> U33(isQid(V_4)) } (1 rules)
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

The module
  { U31(tt,V_4) -> U32(isPalListKind(V_4),V_4) } (1 rules)
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

The module
  { U55(tt,V_3) -> U56(isList(V_3)),
    U54(tt,V_2,V_3) -> U55(isNeList(V_2),V_3),
    U53(tt,V_2,V_3) -> U54(isPalListKind(V_3),V_2,V_3),
    U52(tt,V_2,V_3) -> U53(isPalListKind(V_3),V_2,V_3),
    U51(tt,V_2,V_3) -> U52(isPalListKind(V_2),V_2,V_3),
    isNeList(V_4) -> U31(isPalListKind(V_4),V_4),
    isNeList(__(V_2,V_3)) -> U41(isPalListKind(V_2),V_2,V_3),
    isNeList(__(V_2,V_3)) -> U51(isPalListKind(V_2),V_2,V_3),
    U12(tt,V_4) -> U13(isNeList(V_4)),
    U11(tt,V_4) -> U12(isPalListKind(V_4),V_4),
    isList(__(V_2,V_3)) -> U21(isPalListKind(V_2),V_2,V_3),
    isList(nil) -> tt,
    isList(V_4) -> U11(isPalListKind(V_4),V_4),
    U25(tt,V_3) -> U26(isList(V_3)),
    U24(tt,V_2,V_3) -> U25(isList(V_2),V_3),
    U23(tt,V_2,V_3) -> U24(isPalListKind(V_3),V_2,V_3),
    U22(tt,V_2,V_3) -> U23(isPalListKind(V_3),V_2,V_3),
    U21(tt,V_2,V_3) -> U22(isPalListKind(V_2),V_2,V_3),
    U45(tt,V_3) -> U46(isNeList(V_3)),
    U44(tt,V_2,V_3) -> U45(isList(V_2),V_3),
    U43(tt,V_2,V_3) -> U44(isPalListKind(V_3),V_2,V_3),
    U42(tt,V_2,V_3) -> U43(isPalListKind(V_3),V_2,V_3),
    U41(tt,V_2,V_3) -> U42(isPalListKind(V_2),V_2,V_3) } (23 rules)
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has one strongly connected component:
    0: 'U41`(tt,V_2,V_3) ; 'U42`(isPalListKind(V_2),V_2,V_3)
    1: 'U42`(tt,V_2,V_3) ; 'U43`(isPalListKind(V_3),V_2,V_3)
    2: 'U43`(tt,V_2,V_3) ; 'U44`(isPalListKind(V_3),V_2,V_3)
    3: 'U44`(tt,V_2,V_3) ; 'isList`(V_2)
    4: 'U44`(tt,V_2,V_3) ; 'U45`(isList(V_2),V_3)
    5: 'U45`(tt,V_3) ; 'isNeList`(V_3)
    6: 'U21`(tt,V_2,V_3) ; 'U22`(isPalListKind(V_2),V_2,V_3)
    7: 'U22`(tt,V_2,V_3) ; 'U23`(isPalListKind(V_3),V_2,V_3)
    8: 'U23`(tt,V_2,V_3) ; 'U24`(isPalListKind(V_3),V_2,V_3)
    9: 'U24`(tt,V_2,V_3) ; 'isList`(V_2)
    10: 'U24`(tt,V_2,V_3) ; 'U25`(isList(V_2),V_3)
    11: 'U25`(tt,V_3) ; 'isList`(V_3)
    12: 'isList`(V_4) ; 'U11`(isPalListKind(V_4),V_4)
    13: 'isList`(__(V_2,V_3)) ; 'U21`(isPalListKind(V_2),V_2,V_3)
    14: 'U11`(tt,V_4) ; 'U12`(isPalListKind(V_4),V_4)
    15: 'U12`(tt,V_4) ; 'isNeList`(V_4)
    16: 'isNeList`(__(V_2,V_3)) ; 'U51`(isPalListKind(V_2),V_2,V_3)
    17: 'isNeList`(__(V_2,V_3)) ; 'U41`(isPalListKind(V_2),V_2,V_3)
    18: 'U51`(tt,V_2,V_3) ; 'U52`(isPalListKind(V_2),V_2,V_3)
    19: 'U52`(tt,V_2,V_3) ; 'U53`(isPalListKind(V_3),V_2,V_3)
    20: 'U53`(tt,V_2,V_3) ; 'U54`(isPalListKind(V_3),V_2,V_3)
    21: 'U54`(tt,V_2,V_3) ; 'isNeList`(V_2)
    22: 'U54`(tt,V_2,V_3) ; 'U55`(isNeList(V_2),V_3)
    23: 'U55`(tt,V_3) ; 'isList`(V_3) 
    0 -> 1, 1 -> 2, 2 -> 3, 2 -> 4, 3 -> 12, 3 -> 13, 4 -> 5, 5 -> 16,
    5 -> 17, 6 -> 7, 7 -> 8, 8 -> 9, 8 -> 10, 9 -> 12, 9 -> 13, 10 -> 11,
    11 -> 12, 11 -> 13, 12 -> 14, 13 -> 6, 14 -> 15, 15 -> 16, 15 -> 17,
    16 -> 18, 17 -> 0, 18 -> 19, 19 -> 20, 20 -> 21, 20 -> 22, 21 -> 16,
    21 -> 17, 22 -> 23, 23 -> 12, 23 -> 13, 
    On this component, the interpretation
    [tt] = 3; 
    [U56](X0) = 3; 
    [U92](X0) = 3; 
    [nil] = 3; 
    [__](X0,X1) = 2*X1*X0 + 3*X1 + 3*X0 + 3; 
    [a] = 3; 
    [e] = 3; 
    [i] = 3; 
    [o] = 3; 
    [u] = 3; 
    [isPalListKind](X0) = X0; 
    [isQid](X0) = X0; 
    [U33](X0) = X0; 
    [U32](X0,X1) = X1; 
    [U31](X0,X1) = X1; 
    [U13](X0) = 3; 
    [U26](X0) = 3; 
    [U46](X0) = 3; 
    [U41](X0,X1,X2) = 3; 
    [U91](X0,X1) = 3; 
    [U42](X0,X1,X2) = 3; 
    [U43](X0,X1,X2) = 3; 
    [U44](X0,X1,X2) = 3; 
    [U45](X0,X1) = 3; 
    [U21](X0,X1,X2) = 3; 
    [U22](X0,X1,X2) = 3; 
    [U23](X0,X1,X2) = 3; 
    [U24](X0,X1,X2) = 3; 
    [U25](X0,X1) = 3; 
    [isList](X0) = 3; 
    [U11](X0,X1) = 3; 
    [U12](X0,X1) = 3; 
    [isNeList](X0) = X0; 
    [U51](X0,X1,X2) = 3; 
    [U52](X0,X1,X2) = 3; 
    [U53](X0,X1,X2) = 3; 
    [U54](X0,X1,X2) = 3; 
    [U55](X0,X1) = 3; 
    ['U41`](X0,X1,X2) = 2*X2 + X1 + X0; 
    ['U42`](X0,X1,X2) = 2*X2 + X1 + 2; 
    ['U43`](X0,X1,X2) = 2*X2 + X1 + 1; 
    ['U44`](X0,X1,X2) = X2 + X1 + X0; 
    ['U45`](X0,X1) = X1 + 1; 
    ['U21`](X0,X1,X2) = 3*X2 + X1 + 3; 
    ['U22`](X0,X1,X2) = 3*X2 + X1 + 2; 
    ['U23`](X0,X1,X2) = 3*X2 + X1 + 1; 
    ['U24`](X0,X1,X2) = X2 + X1 + 2*X0; 
    ['U25`](X0,X1) = X1 + X0 + 1; 
    ['isList`](X0) = X0 + 3; 
    ['U11`](X0,X1) = X1 + 2; 
    ['U12`](X0,X1) = X1 + 1; 
    ['isNeList`](X0) = X0; 
    ['U51`](X0,X1,X2) = X2 + 2*X1 + X0 + 1; 
    ['U52`](X0,X1,X2) = X2 + 2*X1 + 3; 
    ['U53`](X0,X1,X2) = X2 + 2*X1 + 2; 
    ['U54`](X0,X1,X2) = X2 + 2*X1 + 1; 
    ['U55`](X0,X1) = X1 + 2*X0; 
     strictly decreases on every cycle

- : unit = ()

Quitting.
Standard error: