MAYBE

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict Trs:
  { __(X, nil()) -> X
  , __(__(X, Y), Z) -> __(X, __(Y, Z))
  , __(nil(), X) -> X
  , U11(tt()) -> U12(isPalListKind())
  , U12(tt()) -> U13(isNeList())
  , isPalListKind() -> tt()
  , isPalListKind() -> U91(isPalListKind())
  , U13(tt()) -> tt()
  , isNeList() -> U31(isPalListKind())
  , isNeList() -> U41(isPalListKind())
  , isNeList() -> U51(isPalListKind())
  , U21(tt()) -> U22(isPalListKind())
  , U22(tt()) -> U23(isPalListKind())
  , U23(tt()) -> U24(isPalListKind())
  , U24(tt()) -> U25(isList())
  , U25(tt()) -> U26(isList())
  , isList() -> U11(isPalListKind())
  , isList() -> tt()
  , isList() -> U21(isPalListKind())
  , U26(tt()) -> tt()
  , U31(tt()) -> U32(isPalListKind())
  , U32(tt()) -> U33(isQid())
  , U33(tt()) -> tt()
  , isQid() -> tt()
  , U41(tt()) -> U42(isPalListKind())
  , U42(tt()) -> U43(isPalListKind())
  , U43(tt()) -> U44(isPalListKind())
  , U44(tt()) -> U45(isList())
  , U45(tt()) -> U46(isNeList())
  , U46(tt()) -> tt()
  , U51(tt()) -> U52(isPalListKind())
  , U52(tt()) -> U53(isPalListKind())
  , U53(tt()) -> U54(isPalListKind())
  , U54(tt()) -> U55(isNeList())
  , U55(tt()) -> U56(isList())
  , U56(tt()) -> tt()
  , U61(tt()) -> U62(isPalListKind())
  , U62(tt()) -> U63(isQid())
  , U63(tt()) -> tt()
  , U71(tt()) -> U72(isPalListKind())
  , U72(tt()) -> U73(isPal())
  , U73(tt()) -> U74(isPalListKind())
  , isPal() -> tt()
  , isPal() -> U81(isPalListKind())
  , U74(tt()) -> tt()
  , U81(tt()) -> U82(isPalListKind())
  , U82(tt()) -> U83(isNePal())
  , U83(tt()) -> tt()
  , isNePal() -> U61(isPalListKind())
  , isNePal() -> U71(isQid())
  , U91(tt()) -> U92(isPalListKind())
  , U92(tt()) -> tt() }
Obligation:
  runtime complexity
Answer:
  MAYBE

None of the processors succeeded.

Details of failed attempt(s):
-----------------------------
1) 'WithProblem (timeout of 60 seconds)' failed due to the
   following reason:
   
   Computation stopped due to timeout after 60.0 seconds.

2) 'Best' failed due to the following reason:
   
   None of the processors succeeded.
   
   Details of failed attempt(s):
   -----------------------------
   1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)'
      failed due to the following reason:
      
      Computation stopped due to timeout after 30.0 seconds.
   
   2) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed
      due to the following reason:
      
      Computation stopped due to timeout after 5.0 seconds.
   
   3) 'Best' failed due to the following reason:
      
      None of the processors succeeded.
      
      Details of failed attempt(s):
      -----------------------------
      1) 'bsearch-popstar (timeout of 60 seconds)' failed due to the
         following reason:
         
         The processor is inapplicable, reason:
           Processor only applicable for innermost runtime complexity analysis
      
      2) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due
         to the following reason:
         
         The processor is inapplicable, reason:
           Processor only applicable for innermost runtime complexity analysis
      
   

3) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed
   due to the following reason:
   
   We add the following weak dependency pairs:
   
   Strict DPs:
     { __^#(X, nil()) -> c_1(X)
     , __^#(__(X, Y), Z) -> c_2(__^#(X, __(Y, Z)))
     , __^#(nil(), X) -> c_3(X)
     , U11^#(tt()) -> c_4(U12^#(isPalListKind()))
     , U12^#(tt()) -> c_5(U13^#(isNeList()))
     , U13^#(tt()) -> c_8()
     , isPalListKind^#() -> c_6()
     , isPalListKind^#() -> c_7(U91^#(isPalListKind()))
     , U91^#(tt()) -> c_51(U92^#(isPalListKind()))
     , isNeList^#() -> c_9(U31^#(isPalListKind()))
     , isNeList^#() -> c_10(U41^#(isPalListKind()))
     , isNeList^#() -> c_11(U51^#(isPalListKind()))
     , U31^#(tt()) -> c_21(U32^#(isPalListKind()))
     , U41^#(tt()) -> c_25(U42^#(isPalListKind()))
     , U51^#(tt()) -> c_31(U52^#(isPalListKind()))
     , U21^#(tt()) -> c_12(U22^#(isPalListKind()))
     , U22^#(tt()) -> c_13(U23^#(isPalListKind()))
     , U23^#(tt()) -> c_14(U24^#(isPalListKind()))
     , U24^#(tt()) -> c_15(U25^#(isList()))
     , U25^#(tt()) -> c_16(U26^#(isList()))
     , U26^#(tt()) -> c_20()
     , isList^#() -> c_17(U11^#(isPalListKind()))
     , isList^#() -> c_18()
     , isList^#() -> c_19(U21^#(isPalListKind()))
     , U32^#(tt()) -> c_22(U33^#(isQid()))
     , U33^#(tt()) -> c_23()
     , isQid^#() -> c_24()
     , U42^#(tt()) -> c_26(U43^#(isPalListKind()))
     , U43^#(tt()) -> c_27(U44^#(isPalListKind()))
     , U44^#(tt()) -> c_28(U45^#(isList()))
     , U45^#(tt()) -> c_29(U46^#(isNeList()))
     , U46^#(tt()) -> c_30()
     , U52^#(tt()) -> c_32(U53^#(isPalListKind()))
     , U53^#(tt()) -> c_33(U54^#(isPalListKind()))
     , U54^#(tt()) -> c_34(U55^#(isNeList()))
     , U55^#(tt()) -> c_35(U56^#(isList()))
     , U56^#(tt()) -> c_36()
     , U61^#(tt()) -> c_37(U62^#(isPalListKind()))
     , U62^#(tt()) -> c_38(U63^#(isQid()))
     , U63^#(tt()) -> c_39()
     , U71^#(tt()) -> c_40(U72^#(isPalListKind()))
     , U72^#(tt()) -> c_41(U73^#(isPal()))
     , U73^#(tt()) -> c_42(U74^#(isPalListKind()))
     , U74^#(tt()) -> c_45()
     , isPal^#() -> c_43()
     , isPal^#() -> c_44(U81^#(isPalListKind()))
     , U81^#(tt()) -> c_46(U82^#(isPalListKind()))
     , U82^#(tt()) -> c_47(U83^#(isNePal()))
     , U83^#(tt()) -> c_48()
     , isNePal^#() -> c_49(U61^#(isPalListKind()))
     , isNePal^#() -> c_50(U71^#(isQid()))
     , U92^#(tt()) -> c_52() }
   
   and mark the set of starting terms.
   
   We are left with following problem, upon which TcT provides the
   certificate MAYBE.
   
   Strict DPs:
     { __^#(X, nil()) -> c_1(X)
     , __^#(__(X, Y), Z) -> c_2(__^#(X, __(Y, Z)))
     , __^#(nil(), X) -> c_3(X)
     , U11^#(tt()) -> c_4(U12^#(isPalListKind()))
     , U12^#(tt()) -> c_5(U13^#(isNeList()))
     , U13^#(tt()) -> c_8()
     , isPalListKind^#() -> c_6()
     , isPalListKind^#() -> c_7(U91^#(isPalListKind()))
     , U91^#(tt()) -> c_51(U92^#(isPalListKind()))
     , isNeList^#() -> c_9(U31^#(isPalListKind()))
     , isNeList^#() -> c_10(U41^#(isPalListKind()))
     , isNeList^#() -> c_11(U51^#(isPalListKind()))
     , U31^#(tt()) -> c_21(U32^#(isPalListKind()))
     , U41^#(tt()) -> c_25(U42^#(isPalListKind()))
     , U51^#(tt()) -> c_31(U52^#(isPalListKind()))
     , U21^#(tt()) -> c_12(U22^#(isPalListKind()))
     , U22^#(tt()) -> c_13(U23^#(isPalListKind()))
     , U23^#(tt()) -> c_14(U24^#(isPalListKind()))
     , U24^#(tt()) -> c_15(U25^#(isList()))
     , U25^#(tt()) -> c_16(U26^#(isList()))
     , U26^#(tt()) -> c_20()
     , isList^#() -> c_17(U11^#(isPalListKind()))
     , isList^#() -> c_18()
     , isList^#() -> c_19(U21^#(isPalListKind()))
     , U32^#(tt()) -> c_22(U33^#(isQid()))
     , U33^#(tt()) -> c_23()
     , isQid^#() -> c_24()
     , U42^#(tt()) -> c_26(U43^#(isPalListKind()))
     , U43^#(tt()) -> c_27(U44^#(isPalListKind()))
     , U44^#(tt()) -> c_28(U45^#(isList()))
     , U45^#(tt()) -> c_29(U46^#(isNeList()))
     , U46^#(tt()) -> c_30()
     , U52^#(tt()) -> c_32(U53^#(isPalListKind()))
     , U53^#(tt()) -> c_33(U54^#(isPalListKind()))
     , U54^#(tt()) -> c_34(U55^#(isNeList()))
     , U55^#(tt()) -> c_35(U56^#(isList()))
     , U56^#(tt()) -> c_36()
     , U61^#(tt()) -> c_37(U62^#(isPalListKind()))
     , U62^#(tt()) -> c_38(U63^#(isQid()))
     , U63^#(tt()) -> c_39()
     , U71^#(tt()) -> c_40(U72^#(isPalListKind()))
     , U72^#(tt()) -> c_41(U73^#(isPal()))
     , U73^#(tt()) -> c_42(U74^#(isPalListKind()))
     , U74^#(tt()) -> c_45()
     , isPal^#() -> c_43()
     , isPal^#() -> c_44(U81^#(isPalListKind()))
     , U81^#(tt()) -> c_46(U82^#(isPalListKind()))
     , U82^#(tt()) -> c_47(U83^#(isNePal()))
     , U83^#(tt()) -> c_48()
     , isNePal^#() -> c_49(U61^#(isPalListKind()))
     , isNePal^#() -> c_50(U71^#(isQid()))
     , U92^#(tt()) -> c_52() }
   Strict Trs:
     { __(X, nil()) -> X
     , __(__(X, Y), Z) -> __(X, __(Y, Z))
     , __(nil(), X) -> X
     , U11(tt()) -> U12(isPalListKind())
     , U12(tt()) -> U13(isNeList())
     , isPalListKind() -> tt()
     , isPalListKind() -> U91(isPalListKind())
     , U13(tt()) -> tt()
     , isNeList() -> U31(isPalListKind())
     , isNeList() -> U41(isPalListKind())
     , isNeList() -> U51(isPalListKind())
     , U21(tt()) -> U22(isPalListKind())
     , U22(tt()) -> U23(isPalListKind())
     , U23(tt()) -> U24(isPalListKind())
     , U24(tt()) -> U25(isList())
     , U25(tt()) -> U26(isList())
     , isList() -> U11(isPalListKind())
     , isList() -> tt()
     , isList() -> U21(isPalListKind())
     , U26(tt()) -> tt()
     , U31(tt()) -> U32(isPalListKind())
     , U32(tt()) -> U33(isQid())
     , U33(tt()) -> tt()
     , isQid() -> tt()
     , U41(tt()) -> U42(isPalListKind())
     , U42(tt()) -> U43(isPalListKind())
     , U43(tt()) -> U44(isPalListKind())
     , U44(tt()) -> U45(isList())
     , U45(tt()) -> U46(isNeList())
     , U46(tt()) -> tt()
     , U51(tt()) -> U52(isPalListKind())
     , U52(tt()) -> U53(isPalListKind())
     , U53(tt()) -> U54(isPalListKind())
     , U54(tt()) -> U55(isNeList())
     , U55(tt()) -> U56(isList())
     , U56(tt()) -> tt()
     , U61(tt()) -> U62(isPalListKind())
     , U62(tt()) -> U63(isQid())
     , U63(tt()) -> tt()
     , U71(tt()) -> U72(isPalListKind())
     , U72(tt()) -> U73(isPal())
     , U73(tt()) -> U74(isPalListKind())
     , isPal() -> tt()
     , isPal() -> U81(isPalListKind())
     , U74(tt()) -> tt()
     , U81(tt()) -> U82(isPalListKind())
     , U82(tt()) -> U83(isNePal())
     , U83(tt()) -> tt()
     , isNePal() -> U61(isPalListKind())
     , isNePal() -> U71(isQid())
     , U91(tt()) -> U92(isPalListKind())
     , U92(tt()) -> tt() }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   We estimate the number of application of
   {6,7,21,23,26,27,32,37,40,44,45,49,52} by applications of
   Pre({6,7,21,23,26,27,32,37,40,44,45,49,52}) =
   {1,3,5,9,20,25,31,36,39,43,48}. Here rules are labeled as follows:
   
     DPs:
       { 1: __^#(X, nil()) -> c_1(X)
       , 2: __^#(__(X, Y), Z) -> c_2(__^#(X, __(Y, Z)))
       , 3: __^#(nil(), X) -> c_3(X)
       , 4: U11^#(tt()) -> c_4(U12^#(isPalListKind()))
       , 5: U12^#(tt()) -> c_5(U13^#(isNeList()))
       , 6: U13^#(tt()) -> c_8()
       , 7: isPalListKind^#() -> c_6()
       , 8: isPalListKind^#() -> c_7(U91^#(isPalListKind()))
       , 9: U91^#(tt()) -> c_51(U92^#(isPalListKind()))
       , 10: isNeList^#() -> c_9(U31^#(isPalListKind()))
       , 11: isNeList^#() -> c_10(U41^#(isPalListKind()))
       , 12: isNeList^#() -> c_11(U51^#(isPalListKind()))
       , 13: U31^#(tt()) -> c_21(U32^#(isPalListKind()))
       , 14: U41^#(tt()) -> c_25(U42^#(isPalListKind()))
       , 15: U51^#(tt()) -> c_31(U52^#(isPalListKind()))
       , 16: U21^#(tt()) -> c_12(U22^#(isPalListKind()))
       , 17: U22^#(tt()) -> c_13(U23^#(isPalListKind()))
       , 18: U23^#(tt()) -> c_14(U24^#(isPalListKind()))
       , 19: U24^#(tt()) -> c_15(U25^#(isList()))
       , 20: U25^#(tt()) -> c_16(U26^#(isList()))
       , 21: U26^#(tt()) -> c_20()
       , 22: isList^#() -> c_17(U11^#(isPalListKind()))
       , 23: isList^#() -> c_18()
       , 24: isList^#() -> c_19(U21^#(isPalListKind()))
       , 25: U32^#(tt()) -> c_22(U33^#(isQid()))
       , 26: U33^#(tt()) -> c_23()
       , 27: isQid^#() -> c_24()
       , 28: U42^#(tt()) -> c_26(U43^#(isPalListKind()))
       , 29: U43^#(tt()) -> c_27(U44^#(isPalListKind()))
       , 30: U44^#(tt()) -> c_28(U45^#(isList()))
       , 31: U45^#(tt()) -> c_29(U46^#(isNeList()))
       , 32: U46^#(tt()) -> c_30()
       , 33: U52^#(tt()) -> c_32(U53^#(isPalListKind()))
       , 34: U53^#(tt()) -> c_33(U54^#(isPalListKind()))
       , 35: U54^#(tt()) -> c_34(U55^#(isNeList()))
       , 36: U55^#(tt()) -> c_35(U56^#(isList()))
       , 37: U56^#(tt()) -> c_36()
       , 38: U61^#(tt()) -> c_37(U62^#(isPalListKind()))
       , 39: U62^#(tt()) -> c_38(U63^#(isQid()))
       , 40: U63^#(tt()) -> c_39()
       , 41: U71^#(tt()) -> c_40(U72^#(isPalListKind()))
       , 42: U72^#(tt()) -> c_41(U73^#(isPal()))
       , 43: U73^#(tt()) -> c_42(U74^#(isPalListKind()))
       , 44: U74^#(tt()) -> c_45()
       , 45: isPal^#() -> c_43()
       , 46: isPal^#() -> c_44(U81^#(isPalListKind()))
       , 47: U81^#(tt()) -> c_46(U82^#(isPalListKind()))
       , 48: U82^#(tt()) -> c_47(U83^#(isNePal()))
       , 49: U83^#(tt()) -> c_48()
       , 50: isNePal^#() -> c_49(U61^#(isPalListKind()))
       , 51: isNePal^#() -> c_50(U71^#(isQid()))
       , 52: U92^#(tt()) -> c_52() }
   
   We are left with following problem, upon which TcT provides the
   certificate MAYBE.
   
   Strict DPs:
     { __^#(X, nil()) -> c_1(X)
     , __^#(__(X, Y), Z) -> c_2(__^#(X, __(Y, Z)))
     , __^#(nil(), X) -> c_3(X)
     , U11^#(tt()) -> c_4(U12^#(isPalListKind()))
     , U12^#(tt()) -> c_5(U13^#(isNeList()))
     , isPalListKind^#() -> c_7(U91^#(isPalListKind()))
     , U91^#(tt()) -> c_51(U92^#(isPalListKind()))
     , isNeList^#() -> c_9(U31^#(isPalListKind()))
     , isNeList^#() -> c_10(U41^#(isPalListKind()))
     , isNeList^#() -> c_11(U51^#(isPalListKind()))
     , U31^#(tt()) -> c_21(U32^#(isPalListKind()))
     , U41^#(tt()) -> c_25(U42^#(isPalListKind()))
     , U51^#(tt()) -> c_31(U52^#(isPalListKind()))
     , U21^#(tt()) -> c_12(U22^#(isPalListKind()))
     , U22^#(tt()) -> c_13(U23^#(isPalListKind()))
     , U23^#(tt()) -> c_14(U24^#(isPalListKind()))
     , U24^#(tt()) -> c_15(U25^#(isList()))
     , U25^#(tt()) -> c_16(U26^#(isList()))
     , isList^#() -> c_17(U11^#(isPalListKind()))
     , isList^#() -> c_19(U21^#(isPalListKind()))
     , U32^#(tt()) -> c_22(U33^#(isQid()))
     , U42^#(tt()) -> c_26(U43^#(isPalListKind()))
     , U43^#(tt()) -> c_27(U44^#(isPalListKind()))
     , U44^#(tt()) -> c_28(U45^#(isList()))
     , U45^#(tt()) -> c_29(U46^#(isNeList()))
     , U52^#(tt()) -> c_32(U53^#(isPalListKind()))
     , U53^#(tt()) -> c_33(U54^#(isPalListKind()))
     , U54^#(tt()) -> c_34(U55^#(isNeList()))
     , U55^#(tt()) -> c_35(U56^#(isList()))
     , U61^#(tt()) -> c_37(U62^#(isPalListKind()))
     , U62^#(tt()) -> c_38(U63^#(isQid()))
     , U71^#(tt()) -> c_40(U72^#(isPalListKind()))
     , U72^#(tt()) -> c_41(U73^#(isPal()))
     , U73^#(tt()) -> c_42(U74^#(isPalListKind()))
     , isPal^#() -> c_44(U81^#(isPalListKind()))
     , U81^#(tt()) -> c_46(U82^#(isPalListKind()))
     , U82^#(tt()) -> c_47(U83^#(isNePal()))
     , isNePal^#() -> c_49(U61^#(isPalListKind()))
     , isNePal^#() -> c_50(U71^#(isQid())) }
   Strict Trs:
     { __(X, nil()) -> X
     , __(__(X, Y), Z) -> __(X, __(Y, Z))
     , __(nil(), X) -> X
     , U11(tt()) -> U12(isPalListKind())
     , U12(tt()) -> U13(isNeList())
     , isPalListKind() -> tt()
     , isPalListKind() -> U91(isPalListKind())
     , U13(tt()) -> tt()
     , isNeList() -> U31(isPalListKind())
     , isNeList() -> U41(isPalListKind())
     , isNeList() -> U51(isPalListKind())
     , U21(tt()) -> U22(isPalListKind())
     , U22(tt()) -> U23(isPalListKind())
     , U23(tt()) -> U24(isPalListKind())
     , U24(tt()) -> U25(isList())
     , U25(tt()) -> U26(isList())
     , isList() -> U11(isPalListKind())
     , isList() -> tt()
     , isList() -> U21(isPalListKind())
     , U26(tt()) -> tt()
     , U31(tt()) -> U32(isPalListKind())
     , U32(tt()) -> U33(isQid())
     , U33(tt()) -> tt()
     , isQid() -> tt()
     , U41(tt()) -> U42(isPalListKind())
     , U42(tt()) -> U43(isPalListKind())
     , U43(tt()) -> U44(isPalListKind())
     , U44(tt()) -> U45(isList())
     , U45(tt()) -> U46(isNeList())
     , U46(tt()) -> tt()
     , U51(tt()) -> U52(isPalListKind())
     , U52(tt()) -> U53(isPalListKind())
     , U53(tt()) -> U54(isPalListKind())
     , U54(tt()) -> U55(isNeList())
     , U55(tt()) -> U56(isList())
     , U56(tt()) -> tt()
     , U61(tt()) -> U62(isPalListKind())
     , U62(tt()) -> U63(isQid())
     , U63(tt()) -> tt()
     , U71(tt()) -> U72(isPalListKind())
     , U72(tt()) -> U73(isPal())
     , U73(tt()) -> U74(isPalListKind())
     , isPal() -> tt()
     , isPal() -> U81(isPalListKind())
     , U74(tt()) -> tt()
     , U81(tt()) -> U82(isPalListKind())
     , U82(tt()) -> U83(isNePal())
     , U83(tt()) -> tt()
     , isNePal() -> U61(isPalListKind())
     , isNePal() -> U71(isQid())
     , U91(tt()) -> U92(isPalListKind())
     , U92(tt()) -> tt() }
   Weak DPs:
     { U13^#(tt()) -> c_8()
     , isPalListKind^#() -> c_6()
     , U26^#(tt()) -> c_20()
     , isList^#() -> c_18()
     , U33^#(tt()) -> c_23()
     , isQid^#() -> c_24()
     , U46^#(tt()) -> c_30()
     , U56^#(tt()) -> c_36()
     , U63^#(tt()) -> c_39()
     , U74^#(tt()) -> c_45()
     , isPal^#() -> c_43()
     , U83^#(tt()) -> c_48()
     , U92^#(tt()) -> c_52() }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   We estimate the number of application of {5,7,18,21,25,29,31,34,37}
   by applications of Pre({5,7,18,21,25,29,31,34,37}) =
   {1,3,4,6,11,17,24,28,30,33,36}. Here rules are labeled as follows:
   
     DPs:
       { 1: __^#(X, nil()) -> c_1(X)
       , 2: __^#(__(X, Y), Z) -> c_2(__^#(X, __(Y, Z)))
       , 3: __^#(nil(), X) -> c_3(X)
       , 4: U11^#(tt()) -> c_4(U12^#(isPalListKind()))
       , 5: U12^#(tt()) -> c_5(U13^#(isNeList()))
       , 6: isPalListKind^#() -> c_7(U91^#(isPalListKind()))
       , 7: U91^#(tt()) -> c_51(U92^#(isPalListKind()))
       , 8: isNeList^#() -> c_9(U31^#(isPalListKind()))
       , 9: isNeList^#() -> c_10(U41^#(isPalListKind()))
       , 10: isNeList^#() -> c_11(U51^#(isPalListKind()))
       , 11: U31^#(tt()) -> c_21(U32^#(isPalListKind()))
       , 12: U41^#(tt()) -> c_25(U42^#(isPalListKind()))
       , 13: U51^#(tt()) -> c_31(U52^#(isPalListKind()))
       , 14: U21^#(tt()) -> c_12(U22^#(isPalListKind()))
       , 15: U22^#(tt()) -> c_13(U23^#(isPalListKind()))
       , 16: U23^#(tt()) -> c_14(U24^#(isPalListKind()))
       , 17: U24^#(tt()) -> c_15(U25^#(isList()))
       , 18: U25^#(tt()) -> c_16(U26^#(isList()))
       , 19: isList^#() -> c_17(U11^#(isPalListKind()))
       , 20: isList^#() -> c_19(U21^#(isPalListKind()))
       , 21: U32^#(tt()) -> c_22(U33^#(isQid()))
       , 22: U42^#(tt()) -> c_26(U43^#(isPalListKind()))
       , 23: U43^#(tt()) -> c_27(U44^#(isPalListKind()))
       , 24: U44^#(tt()) -> c_28(U45^#(isList()))
       , 25: U45^#(tt()) -> c_29(U46^#(isNeList()))
       , 26: U52^#(tt()) -> c_32(U53^#(isPalListKind()))
       , 27: U53^#(tt()) -> c_33(U54^#(isPalListKind()))
       , 28: U54^#(tt()) -> c_34(U55^#(isNeList()))
       , 29: U55^#(tt()) -> c_35(U56^#(isList()))
       , 30: U61^#(tt()) -> c_37(U62^#(isPalListKind()))
       , 31: U62^#(tt()) -> c_38(U63^#(isQid()))
       , 32: U71^#(tt()) -> c_40(U72^#(isPalListKind()))
       , 33: U72^#(tt()) -> c_41(U73^#(isPal()))
       , 34: U73^#(tt()) -> c_42(U74^#(isPalListKind()))
       , 35: isPal^#() -> c_44(U81^#(isPalListKind()))
       , 36: U81^#(tt()) -> c_46(U82^#(isPalListKind()))
       , 37: U82^#(tt()) -> c_47(U83^#(isNePal()))
       , 38: isNePal^#() -> c_49(U61^#(isPalListKind()))
       , 39: isNePal^#() -> c_50(U71^#(isQid()))
       , 40: U13^#(tt()) -> c_8()
       , 41: isPalListKind^#() -> c_6()
       , 42: U26^#(tt()) -> c_20()
       , 43: isList^#() -> c_18()
       , 44: U33^#(tt()) -> c_23()
       , 45: isQid^#() -> c_24()
       , 46: U46^#(tt()) -> c_30()
       , 47: U56^#(tt()) -> c_36()
       , 48: U63^#(tt()) -> c_39()
       , 49: U74^#(tt()) -> c_45()
       , 50: isPal^#() -> c_43()
       , 51: U83^#(tt()) -> c_48()
       , 52: U92^#(tt()) -> c_52() }
   
   We are left with following problem, upon which TcT provides the
   certificate MAYBE.
   
   Strict DPs:
     { __^#(X, nil()) -> c_1(X)
     , __^#(__(X, Y), Z) -> c_2(__^#(X, __(Y, Z)))
     , __^#(nil(), X) -> c_3(X)
     , U11^#(tt()) -> c_4(U12^#(isPalListKind()))
     , isPalListKind^#() -> c_7(U91^#(isPalListKind()))
     , isNeList^#() -> c_9(U31^#(isPalListKind()))
     , isNeList^#() -> c_10(U41^#(isPalListKind()))
     , isNeList^#() -> c_11(U51^#(isPalListKind()))
     , U31^#(tt()) -> c_21(U32^#(isPalListKind()))
     , U41^#(tt()) -> c_25(U42^#(isPalListKind()))
     , U51^#(tt()) -> c_31(U52^#(isPalListKind()))
     , U21^#(tt()) -> c_12(U22^#(isPalListKind()))
     , U22^#(tt()) -> c_13(U23^#(isPalListKind()))
     , U23^#(tt()) -> c_14(U24^#(isPalListKind()))
     , U24^#(tt()) -> c_15(U25^#(isList()))
     , isList^#() -> c_17(U11^#(isPalListKind()))
     , isList^#() -> c_19(U21^#(isPalListKind()))
     , U42^#(tt()) -> c_26(U43^#(isPalListKind()))
     , U43^#(tt()) -> c_27(U44^#(isPalListKind()))
     , U44^#(tt()) -> c_28(U45^#(isList()))
     , U52^#(tt()) -> c_32(U53^#(isPalListKind()))
     , U53^#(tt()) -> c_33(U54^#(isPalListKind()))
     , U54^#(tt()) -> c_34(U55^#(isNeList()))
     , U61^#(tt()) -> c_37(U62^#(isPalListKind()))
     , U71^#(tt()) -> c_40(U72^#(isPalListKind()))
     , U72^#(tt()) -> c_41(U73^#(isPal()))
     , isPal^#() -> c_44(U81^#(isPalListKind()))
     , U81^#(tt()) -> c_46(U82^#(isPalListKind()))
     , isNePal^#() -> c_49(U61^#(isPalListKind()))
     , isNePal^#() -> c_50(U71^#(isQid())) }
   Strict Trs:
     { __(X, nil()) -> X
     , __(__(X, Y), Z) -> __(X, __(Y, Z))
     , __(nil(), X) -> X
     , U11(tt()) -> U12(isPalListKind())
     , U12(tt()) -> U13(isNeList())
     , isPalListKind() -> tt()
     , isPalListKind() -> U91(isPalListKind())
     , U13(tt()) -> tt()
     , isNeList() -> U31(isPalListKind())
     , isNeList() -> U41(isPalListKind())
     , isNeList() -> U51(isPalListKind())
     , U21(tt()) -> U22(isPalListKind())
     , U22(tt()) -> U23(isPalListKind())
     , U23(tt()) -> U24(isPalListKind())
     , U24(tt()) -> U25(isList())
     , U25(tt()) -> U26(isList())
     , isList() -> U11(isPalListKind())
     , isList() -> tt()
     , isList() -> U21(isPalListKind())
     , U26(tt()) -> tt()
     , U31(tt()) -> U32(isPalListKind())
     , U32(tt()) -> U33(isQid())
     , U33(tt()) -> tt()
     , isQid() -> tt()
     , U41(tt()) -> U42(isPalListKind())
     , U42(tt()) -> U43(isPalListKind())
     , U43(tt()) -> U44(isPalListKind())
     , U44(tt()) -> U45(isList())
     , U45(tt()) -> U46(isNeList())
     , U46(tt()) -> tt()
     , U51(tt()) -> U52(isPalListKind())
     , U52(tt()) -> U53(isPalListKind())
     , U53(tt()) -> U54(isPalListKind())
     , U54(tt()) -> U55(isNeList())
     , U55(tt()) -> U56(isList())
     , U56(tt()) -> tt()
     , U61(tt()) -> U62(isPalListKind())
     , U62(tt()) -> U63(isQid())
     , U63(tt()) -> tt()
     , U71(tt()) -> U72(isPalListKind())
     , U72(tt()) -> U73(isPal())
     , U73(tt()) -> U74(isPalListKind())
     , isPal() -> tt()
     , isPal() -> U81(isPalListKind())
     , U74(tt()) -> tt()
     , U81(tt()) -> U82(isPalListKind())
     , U82(tt()) -> U83(isNePal())
     , U83(tt()) -> tt()
     , isNePal() -> U61(isPalListKind())
     , isNePal() -> U71(isQid())
     , U91(tt()) -> U92(isPalListKind())
     , U92(tt()) -> tt() }
   Weak DPs:
     { U12^#(tt()) -> c_5(U13^#(isNeList()))
     , U13^#(tt()) -> c_8()
     , isPalListKind^#() -> c_6()
     , U91^#(tt()) -> c_51(U92^#(isPalListKind()))
     , U25^#(tt()) -> c_16(U26^#(isList()))
     , U26^#(tt()) -> c_20()
     , isList^#() -> c_18()
     , U32^#(tt()) -> c_22(U33^#(isQid()))
     , U33^#(tt()) -> c_23()
     , isQid^#() -> c_24()
     , U45^#(tt()) -> c_29(U46^#(isNeList()))
     , U46^#(tt()) -> c_30()
     , U55^#(tt()) -> c_35(U56^#(isList()))
     , U56^#(tt()) -> c_36()
     , U62^#(tt()) -> c_38(U63^#(isQid()))
     , U63^#(tt()) -> c_39()
     , U73^#(tt()) -> c_42(U74^#(isPalListKind()))
     , U74^#(tt()) -> c_45()
     , isPal^#() -> c_43()
     , U82^#(tt()) -> c_47(U83^#(isNePal()))
     , U83^#(tt()) -> c_48()
     , U92^#(tt()) -> c_52() }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   We estimate the number of application of {4,5,9,15,20,23,24,26,28}
   by applications of Pre({4,5,9,15,20,23,24,26,28}) =
   {1,3,6,14,16,19,22,25,27,29}. Here rules are labeled as follows:
   
     DPs:
       { 1: __^#(X, nil()) -> c_1(X)
       , 2: __^#(__(X, Y), Z) -> c_2(__^#(X, __(Y, Z)))
       , 3: __^#(nil(), X) -> c_3(X)
       , 4: U11^#(tt()) -> c_4(U12^#(isPalListKind()))
       , 5: isPalListKind^#() -> c_7(U91^#(isPalListKind()))
       , 6: isNeList^#() -> c_9(U31^#(isPalListKind()))
       , 7: isNeList^#() -> c_10(U41^#(isPalListKind()))
       , 8: isNeList^#() -> c_11(U51^#(isPalListKind()))
       , 9: U31^#(tt()) -> c_21(U32^#(isPalListKind()))
       , 10: U41^#(tt()) -> c_25(U42^#(isPalListKind()))
       , 11: U51^#(tt()) -> c_31(U52^#(isPalListKind()))
       , 12: U21^#(tt()) -> c_12(U22^#(isPalListKind()))
       , 13: U22^#(tt()) -> c_13(U23^#(isPalListKind()))
       , 14: U23^#(tt()) -> c_14(U24^#(isPalListKind()))
       , 15: U24^#(tt()) -> c_15(U25^#(isList()))
       , 16: isList^#() -> c_17(U11^#(isPalListKind()))
       , 17: isList^#() -> c_19(U21^#(isPalListKind()))
       , 18: U42^#(tt()) -> c_26(U43^#(isPalListKind()))
       , 19: U43^#(tt()) -> c_27(U44^#(isPalListKind()))
       , 20: U44^#(tt()) -> c_28(U45^#(isList()))
       , 21: U52^#(tt()) -> c_32(U53^#(isPalListKind()))
       , 22: U53^#(tt()) -> c_33(U54^#(isPalListKind()))
       , 23: U54^#(tt()) -> c_34(U55^#(isNeList()))
       , 24: U61^#(tt()) -> c_37(U62^#(isPalListKind()))
       , 25: U71^#(tt()) -> c_40(U72^#(isPalListKind()))
       , 26: U72^#(tt()) -> c_41(U73^#(isPal()))
       , 27: isPal^#() -> c_44(U81^#(isPalListKind()))
       , 28: U81^#(tt()) -> c_46(U82^#(isPalListKind()))
       , 29: isNePal^#() -> c_49(U61^#(isPalListKind()))
       , 30: isNePal^#() -> c_50(U71^#(isQid()))
       , 31: U12^#(tt()) -> c_5(U13^#(isNeList()))
       , 32: U13^#(tt()) -> c_8()
       , 33: isPalListKind^#() -> c_6()
       , 34: U91^#(tt()) -> c_51(U92^#(isPalListKind()))
       , 35: U25^#(tt()) -> c_16(U26^#(isList()))
       , 36: U26^#(tt()) -> c_20()
       , 37: isList^#() -> c_18()
       , 38: U32^#(tt()) -> c_22(U33^#(isQid()))
       , 39: U33^#(tt()) -> c_23()
       , 40: isQid^#() -> c_24()
       , 41: U45^#(tt()) -> c_29(U46^#(isNeList()))
       , 42: U46^#(tt()) -> c_30()
       , 43: U55^#(tt()) -> c_35(U56^#(isList()))
       , 44: U56^#(tt()) -> c_36()
       , 45: U62^#(tt()) -> c_38(U63^#(isQid()))
       , 46: U63^#(tt()) -> c_39()
       , 47: U73^#(tt()) -> c_42(U74^#(isPalListKind()))
       , 48: U74^#(tt()) -> c_45()
       , 49: isPal^#() -> c_43()
       , 50: U82^#(tt()) -> c_47(U83^#(isNePal()))
       , 51: U83^#(tt()) -> c_48()
       , 52: U92^#(tt()) -> c_52() }
   
   We are left with following problem, upon which TcT provides the
   certificate MAYBE.
   
   Strict DPs:
     { __^#(X, nil()) -> c_1(X)
     , __^#(__(X, Y), Z) -> c_2(__^#(X, __(Y, Z)))
     , __^#(nil(), X) -> c_3(X)
     , isNeList^#() -> c_9(U31^#(isPalListKind()))
     , isNeList^#() -> c_10(U41^#(isPalListKind()))
     , isNeList^#() -> c_11(U51^#(isPalListKind()))
     , U41^#(tt()) -> c_25(U42^#(isPalListKind()))
     , U51^#(tt()) -> c_31(U52^#(isPalListKind()))
     , U21^#(tt()) -> c_12(U22^#(isPalListKind()))
     , U22^#(tt()) -> c_13(U23^#(isPalListKind()))
     , U23^#(tt()) -> c_14(U24^#(isPalListKind()))
     , isList^#() -> c_17(U11^#(isPalListKind()))
     , isList^#() -> c_19(U21^#(isPalListKind()))
     , U42^#(tt()) -> c_26(U43^#(isPalListKind()))
     , U43^#(tt()) -> c_27(U44^#(isPalListKind()))
     , U52^#(tt()) -> c_32(U53^#(isPalListKind()))
     , U53^#(tt()) -> c_33(U54^#(isPalListKind()))
     , U71^#(tt()) -> c_40(U72^#(isPalListKind()))
     , isPal^#() -> c_44(U81^#(isPalListKind()))
     , isNePal^#() -> c_49(U61^#(isPalListKind()))
     , isNePal^#() -> c_50(U71^#(isQid())) }
   Strict Trs:
     { __(X, nil()) -> X
     , __(__(X, Y), Z) -> __(X, __(Y, Z))
     , __(nil(), X) -> X
     , U11(tt()) -> U12(isPalListKind())
     , U12(tt()) -> U13(isNeList())
     , isPalListKind() -> tt()
     , isPalListKind() -> U91(isPalListKind())
     , U13(tt()) -> tt()
     , isNeList() -> U31(isPalListKind())
     , isNeList() -> U41(isPalListKind())
     , isNeList() -> U51(isPalListKind())
     , U21(tt()) -> U22(isPalListKind())
     , U22(tt()) -> U23(isPalListKind())
     , U23(tt()) -> U24(isPalListKind())
     , U24(tt()) -> U25(isList())
     , U25(tt()) -> U26(isList())
     , isList() -> U11(isPalListKind())
     , isList() -> tt()
     , isList() -> U21(isPalListKind())
     , U26(tt()) -> tt()
     , U31(tt()) -> U32(isPalListKind())
     , U32(tt()) -> U33(isQid())
     , U33(tt()) -> tt()
     , isQid() -> tt()
     , U41(tt()) -> U42(isPalListKind())
     , U42(tt()) -> U43(isPalListKind())
     , U43(tt()) -> U44(isPalListKind())
     , U44(tt()) -> U45(isList())
     , U45(tt()) -> U46(isNeList())
     , U46(tt()) -> tt()
     , U51(tt()) -> U52(isPalListKind())
     , U52(tt()) -> U53(isPalListKind())
     , U53(tt()) -> U54(isPalListKind())
     , U54(tt()) -> U55(isNeList())
     , U55(tt()) -> U56(isList())
     , U56(tt()) -> tt()
     , U61(tt()) -> U62(isPalListKind())
     , U62(tt()) -> U63(isQid())
     , U63(tt()) -> tt()
     , U71(tt()) -> U72(isPalListKind())
     , U72(tt()) -> U73(isPal())
     , U73(tt()) -> U74(isPalListKind())
     , isPal() -> tt()
     , isPal() -> U81(isPalListKind())
     , U74(tt()) -> tt()
     , U81(tt()) -> U82(isPalListKind())
     , U82(tt()) -> U83(isNePal())
     , U83(tt()) -> tt()
     , isNePal() -> U61(isPalListKind())
     , isNePal() -> U71(isQid())
     , U91(tt()) -> U92(isPalListKind())
     , U92(tt()) -> tt() }
   Weak DPs:
     { U11^#(tt()) -> c_4(U12^#(isPalListKind()))
     , U12^#(tt()) -> c_5(U13^#(isNeList()))
     , U13^#(tt()) -> c_8()
     , isPalListKind^#() -> c_6()
     , isPalListKind^#() -> c_7(U91^#(isPalListKind()))
     , U91^#(tt()) -> c_51(U92^#(isPalListKind()))
     , U31^#(tt()) -> c_21(U32^#(isPalListKind()))
     , U24^#(tt()) -> c_15(U25^#(isList()))
     , U25^#(tt()) -> c_16(U26^#(isList()))
     , U26^#(tt()) -> c_20()
     , isList^#() -> c_18()
     , U32^#(tt()) -> c_22(U33^#(isQid()))
     , U33^#(tt()) -> c_23()
     , isQid^#() -> c_24()
     , U44^#(tt()) -> c_28(U45^#(isList()))
     , U45^#(tt()) -> c_29(U46^#(isNeList()))
     , U46^#(tt()) -> c_30()
     , U54^#(tt()) -> c_34(U55^#(isNeList()))
     , U55^#(tt()) -> c_35(U56^#(isList()))
     , U56^#(tt()) -> c_36()
     , U61^#(tt()) -> c_37(U62^#(isPalListKind()))
     , U62^#(tt()) -> c_38(U63^#(isQid()))
     , U63^#(tt()) -> c_39()
     , U72^#(tt()) -> c_41(U73^#(isPal()))
     , U73^#(tt()) -> c_42(U74^#(isPalListKind()))
     , U74^#(tt()) -> c_45()
     , isPal^#() -> c_43()
     , U81^#(tt()) -> c_46(U82^#(isPalListKind()))
     , U82^#(tt()) -> c_47(U83^#(isNePal()))
     , U83^#(tt()) -> c_48()
     , U92^#(tt()) -> c_52() }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   We estimate the number of application of {4,11,12,15,17,18,19,20}
   by applications of Pre({4,11,12,15,17,18,19,20}) =
   {1,3,10,14,16,21}. Here rules are labeled as follows:
   
     DPs:
       { 1: __^#(X, nil()) -> c_1(X)
       , 2: __^#(__(X, Y), Z) -> c_2(__^#(X, __(Y, Z)))
       , 3: __^#(nil(), X) -> c_3(X)
       , 4: isNeList^#() -> c_9(U31^#(isPalListKind()))
       , 5: isNeList^#() -> c_10(U41^#(isPalListKind()))
       , 6: isNeList^#() -> c_11(U51^#(isPalListKind()))
       , 7: U41^#(tt()) -> c_25(U42^#(isPalListKind()))
       , 8: U51^#(tt()) -> c_31(U52^#(isPalListKind()))
       , 9: U21^#(tt()) -> c_12(U22^#(isPalListKind()))
       , 10: U22^#(tt()) -> c_13(U23^#(isPalListKind()))
       , 11: U23^#(tt()) -> c_14(U24^#(isPalListKind()))
       , 12: isList^#() -> c_17(U11^#(isPalListKind()))
       , 13: isList^#() -> c_19(U21^#(isPalListKind()))
       , 14: U42^#(tt()) -> c_26(U43^#(isPalListKind()))
       , 15: U43^#(tt()) -> c_27(U44^#(isPalListKind()))
       , 16: U52^#(tt()) -> c_32(U53^#(isPalListKind()))
       , 17: U53^#(tt()) -> c_33(U54^#(isPalListKind()))
       , 18: U71^#(tt()) -> c_40(U72^#(isPalListKind()))
       , 19: isPal^#() -> c_44(U81^#(isPalListKind()))
       , 20: isNePal^#() -> c_49(U61^#(isPalListKind()))
       , 21: isNePal^#() -> c_50(U71^#(isQid()))
       , 22: U11^#(tt()) -> c_4(U12^#(isPalListKind()))
       , 23: U12^#(tt()) -> c_5(U13^#(isNeList()))
       , 24: U13^#(tt()) -> c_8()
       , 25: isPalListKind^#() -> c_6()
       , 26: isPalListKind^#() -> c_7(U91^#(isPalListKind()))
       , 27: U91^#(tt()) -> c_51(U92^#(isPalListKind()))
       , 28: U31^#(tt()) -> c_21(U32^#(isPalListKind()))
       , 29: U24^#(tt()) -> c_15(U25^#(isList()))
       , 30: U25^#(tt()) -> c_16(U26^#(isList()))
       , 31: U26^#(tt()) -> c_20()
       , 32: isList^#() -> c_18()
       , 33: U32^#(tt()) -> c_22(U33^#(isQid()))
       , 34: U33^#(tt()) -> c_23()
       , 35: isQid^#() -> c_24()
       , 36: U44^#(tt()) -> c_28(U45^#(isList()))
       , 37: U45^#(tt()) -> c_29(U46^#(isNeList()))
       , 38: U46^#(tt()) -> c_30()
       , 39: U54^#(tt()) -> c_34(U55^#(isNeList()))
       , 40: U55^#(tt()) -> c_35(U56^#(isList()))
       , 41: U56^#(tt()) -> c_36()
       , 42: U61^#(tt()) -> c_37(U62^#(isPalListKind()))
       , 43: U62^#(tt()) -> c_38(U63^#(isQid()))
       , 44: U63^#(tt()) -> c_39()
       , 45: U72^#(tt()) -> c_41(U73^#(isPal()))
       , 46: U73^#(tt()) -> c_42(U74^#(isPalListKind()))
       , 47: U74^#(tt()) -> c_45()
       , 48: isPal^#() -> c_43()
       , 49: U81^#(tt()) -> c_46(U82^#(isPalListKind()))
       , 50: U82^#(tt()) -> c_47(U83^#(isNePal()))
       , 51: U83^#(tt()) -> c_48()
       , 52: U92^#(tt()) -> c_52() }
   
   We are left with following problem, upon which TcT provides the
   certificate MAYBE.
   
   Strict DPs:
     { __^#(X, nil()) -> c_1(X)
     , __^#(__(X, Y), Z) -> c_2(__^#(X, __(Y, Z)))
     , __^#(nil(), X) -> c_3(X)
     , isNeList^#() -> c_10(U41^#(isPalListKind()))
     , isNeList^#() -> c_11(U51^#(isPalListKind()))
     , U41^#(tt()) -> c_25(U42^#(isPalListKind()))
     , U51^#(tt()) -> c_31(U52^#(isPalListKind()))
     , U21^#(tt()) -> c_12(U22^#(isPalListKind()))
     , U22^#(tt()) -> c_13(U23^#(isPalListKind()))
     , isList^#() -> c_19(U21^#(isPalListKind()))
     , U42^#(tt()) -> c_26(U43^#(isPalListKind()))
     , U52^#(tt()) -> c_32(U53^#(isPalListKind()))
     , isNePal^#() -> c_50(U71^#(isQid())) }
   Strict Trs:
     { __(X, nil()) -> X
     , __(__(X, Y), Z) -> __(X, __(Y, Z))
     , __(nil(), X) -> X
     , U11(tt()) -> U12(isPalListKind())
     , U12(tt()) -> U13(isNeList())
     , isPalListKind() -> tt()
     , isPalListKind() -> U91(isPalListKind())
     , U13(tt()) -> tt()
     , isNeList() -> U31(isPalListKind())
     , isNeList() -> U41(isPalListKind())
     , isNeList() -> U51(isPalListKind())
     , U21(tt()) -> U22(isPalListKind())
     , U22(tt()) -> U23(isPalListKind())
     , U23(tt()) -> U24(isPalListKind())
     , U24(tt()) -> U25(isList())
     , U25(tt()) -> U26(isList())
     , isList() -> U11(isPalListKind())
     , isList() -> tt()
     , isList() -> U21(isPalListKind())
     , U26(tt()) -> tt()
     , U31(tt()) -> U32(isPalListKind())
     , U32(tt()) -> U33(isQid())
     , U33(tt()) -> tt()
     , isQid() -> tt()
     , U41(tt()) -> U42(isPalListKind())
     , U42(tt()) -> U43(isPalListKind())
     , U43(tt()) -> U44(isPalListKind())
     , U44(tt()) -> U45(isList())
     , U45(tt()) -> U46(isNeList())
     , U46(tt()) -> tt()
     , U51(tt()) -> U52(isPalListKind())
     , U52(tt()) -> U53(isPalListKind())
     , U53(tt()) -> U54(isPalListKind())
     , U54(tt()) -> U55(isNeList())
     , U55(tt()) -> U56(isList())
     , U56(tt()) -> tt()
     , U61(tt()) -> U62(isPalListKind())
     , U62(tt()) -> U63(isQid())
     , U63(tt()) -> tt()
     , U71(tt()) -> U72(isPalListKind())
     , U72(tt()) -> U73(isPal())
     , U73(tt()) -> U74(isPalListKind())
     , isPal() -> tt()
     , isPal() -> U81(isPalListKind())
     , U74(tt()) -> tt()
     , U81(tt()) -> U82(isPalListKind())
     , U82(tt()) -> U83(isNePal())
     , U83(tt()) -> tt()
     , isNePal() -> U61(isPalListKind())
     , isNePal() -> U71(isQid())
     , U91(tt()) -> U92(isPalListKind())
     , U92(tt()) -> tt() }
   Weak DPs:
     { U11^#(tt()) -> c_4(U12^#(isPalListKind()))
     , U12^#(tt()) -> c_5(U13^#(isNeList()))
     , U13^#(tt()) -> c_8()
     , isPalListKind^#() -> c_6()
     , isPalListKind^#() -> c_7(U91^#(isPalListKind()))
     , U91^#(tt()) -> c_51(U92^#(isPalListKind()))
     , isNeList^#() -> c_9(U31^#(isPalListKind()))
     , U31^#(tt()) -> c_21(U32^#(isPalListKind()))
     , U23^#(tt()) -> c_14(U24^#(isPalListKind()))
     , U24^#(tt()) -> c_15(U25^#(isList()))
     , U25^#(tt()) -> c_16(U26^#(isList()))
     , U26^#(tt()) -> c_20()
     , isList^#() -> c_17(U11^#(isPalListKind()))
     , isList^#() -> c_18()
     , U32^#(tt()) -> c_22(U33^#(isQid()))
     , U33^#(tt()) -> c_23()
     , isQid^#() -> c_24()
     , U43^#(tt()) -> c_27(U44^#(isPalListKind()))
     , U44^#(tt()) -> c_28(U45^#(isList()))
     , U45^#(tt()) -> c_29(U46^#(isNeList()))
     , U46^#(tt()) -> c_30()
     , U53^#(tt()) -> c_33(U54^#(isPalListKind()))
     , U54^#(tt()) -> c_34(U55^#(isNeList()))
     , U55^#(tt()) -> c_35(U56^#(isList()))
     , U56^#(tt()) -> c_36()
     , U61^#(tt()) -> c_37(U62^#(isPalListKind()))
     , U62^#(tt()) -> c_38(U63^#(isQid()))
     , U63^#(tt()) -> c_39()
     , U71^#(tt()) -> c_40(U72^#(isPalListKind()))
     , U72^#(tt()) -> c_41(U73^#(isPal()))
     , U73^#(tt()) -> c_42(U74^#(isPalListKind()))
     , U74^#(tt()) -> c_45()
     , isPal^#() -> c_43()
     , isPal^#() -> c_44(U81^#(isPalListKind()))
     , U81^#(tt()) -> c_46(U82^#(isPalListKind()))
     , U82^#(tt()) -> c_47(U83^#(isNePal()))
     , U83^#(tt()) -> c_48()
     , isNePal^#() -> c_49(U61^#(isPalListKind()))
     , U92^#(tt()) -> c_52() }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   We estimate the number of application of {9,11,12,13} by
   applications of Pre({9,11,12,13}) = {1,3,6,7,8}. Here rules are
   labeled as follows:
   
     DPs:
       { 1: __^#(X, nil()) -> c_1(X)
       , 2: __^#(__(X, Y), Z) -> c_2(__^#(X, __(Y, Z)))
       , 3: __^#(nil(), X) -> c_3(X)
       , 4: isNeList^#() -> c_10(U41^#(isPalListKind()))
       , 5: isNeList^#() -> c_11(U51^#(isPalListKind()))
       , 6: U41^#(tt()) -> c_25(U42^#(isPalListKind()))
       , 7: U51^#(tt()) -> c_31(U52^#(isPalListKind()))
       , 8: U21^#(tt()) -> c_12(U22^#(isPalListKind()))
       , 9: U22^#(tt()) -> c_13(U23^#(isPalListKind()))
       , 10: isList^#() -> c_19(U21^#(isPalListKind()))
       , 11: U42^#(tt()) -> c_26(U43^#(isPalListKind()))
       , 12: U52^#(tt()) -> c_32(U53^#(isPalListKind()))
       , 13: isNePal^#() -> c_50(U71^#(isQid()))
       , 14: U11^#(tt()) -> c_4(U12^#(isPalListKind()))
       , 15: U12^#(tt()) -> c_5(U13^#(isNeList()))
       , 16: U13^#(tt()) -> c_8()
       , 17: isPalListKind^#() -> c_6()
       , 18: isPalListKind^#() -> c_7(U91^#(isPalListKind()))
       , 19: U91^#(tt()) -> c_51(U92^#(isPalListKind()))
       , 20: isNeList^#() -> c_9(U31^#(isPalListKind()))
       , 21: U31^#(tt()) -> c_21(U32^#(isPalListKind()))
       , 22: U23^#(tt()) -> c_14(U24^#(isPalListKind()))
       , 23: U24^#(tt()) -> c_15(U25^#(isList()))
       , 24: U25^#(tt()) -> c_16(U26^#(isList()))
       , 25: U26^#(tt()) -> c_20()
       , 26: isList^#() -> c_17(U11^#(isPalListKind()))
       , 27: isList^#() -> c_18()
       , 28: U32^#(tt()) -> c_22(U33^#(isQid()))
       , 29: U33^#(tt()) -> c_23()
       , 30: isQid^#() -> c_24()
       , 31: U43^#(tt()) -> c_27(U44^#(isPalListKind()))
       , 32: U44^#(tt()) -> c_28(U45^#(isList()))
       , 33: U45^#(tt()) -> c_29(U46^#(isNeList()))
       , 34: U46^#(tt()) -> c_30()
       , 35: U53^#(tt()) -> c_33(U54^#(isPalListKind()))
       , 36: U54^#(tt()) -> c_34(U55^#(isNeList()))
       , 37: U55^#(tt()) -> c_35(U56^#(isList()))
       , 38: U56^#(tt()) -> c_36()
       , 39: U61^#(tt()) -> c_37(U62^#(isPalListKind()))
       , 40: U62^#(tt()) -> c_38(U63^#(isQid()))
       , 41: U63^#(tt()) -> c_39()
       , 42: U71^#(tt()) -> c_40(U72^#(isPalListKind()))
       , 43: U72^#(tt()) -> c_41(U73^#(isPal()))
       , 44: U73^#(tt()) -> c_42(U74^#(isPalListKind()))
       , 45: U74^#(tt()) -> c_45()
       , 46: isPal^#() -> c_43()
       , 47: isPal^#() -> c_44(U81^#(isPalListKind()))
       , 48: U81^#(tt()) -> c_46(U82^#(isPalListKind()))
       , 49: U82^#(tt()) -> c_47(U83^#(isNePal()))
       , 50: U83^#(tt()) -> c_48()
       , 51: isNePal^#() -> c_49(U61^#(isPalListKind()))
       , 52: U92^#(tt()) -> c_52() }
   
   We are left with following problem, upon which TcT provides the
   certificate MAYBE.
   
   Strict DPs:
     { __^#(X, nil()) -> c_1(X)
     , __^#(__(X, Y), Z) -> c_2(__^#(X, __(Y, Z)))
     , __^#(nil(), X) -> c_3(X)
     , isNeList^#() -> c_10(U41^#(isPalListKind()))
     , isNeList^#() -> c_11(U51^#(isPalListKind()))
     , U41^#(tt()) -> c_25(U42^#(isPalListKind()))
     , U51^#(tt()) -> c_31(U52^#(isPalListKind()))
     , U21^#(tt()) -> c_12(U22^#(isPalListKind()))
     , isList^#() -> c_19(U21^#(isPalListKind())) }
   Strict Trs:
     { __(X, nil()) -> X
     , __(__(X, Y), Z) -> __(X, __(Y, Z))
     , __(nil(), X) -> X
     , U11(tt()) -> U12(isPalListKind())
     , U12(tt()) -> U13(isNeList())
     , isPalListKind() -> tt()
     , isPalListKind() -> U91(isPalListKind())
     , U13(tt()) -> tt()
     , isNeList() -> U31(isPalListKind())
     , isNeList() -> U41(isPalListKind())
     , isNeList() -> U51(isPalListKind())
     , U21(tt()) -> U22(isPalListKind())
     , U22(tt()) -> U23(isPalListKind())
     , U23(tt()) -> U24(isPalListKind())
     , U24(tt()) -> U25(isList())
     , U25(tt()) -> U26(isList())
     , isList() -> U11(isPalListKind())
     , isList() -> tt()
     , isList() -> U21(isPalListKind())
     , U26(tt()) -> tt()
     , U31(tt()) -> U32(isPalListKind())
     , U32(tt()) -> U33(isQid())
     , U33(tt()) -> tt()
     , isQid() -> tt()
     , U41(tt()) -> U42(isPalListKind())
     , U42(tt()) -> U43(isPalListKind())
     , U43(tt()) -> U44(isPalListKind())
     , U44(tt()) -> U45(isList())
     , U45(tt()) -> U46(isNeList())
     , U46(tt()) -> tt()
     , U51(tt()) -> U52(isPalListKind())
     , U52(tt()) -> U53(isPalListKind())
     , U53(tt()) -> U54(isPalListKind())
     , U54(tt()) -> U55(isNeList())
     , U55(tt()) -> U56(isList())
     , U56(tt()) -> tt()
     , U61(tt()) -> U62(isPalListKind())
     , U62(tt()) -> U63(isQid())
     , U63(tt()) -> tt()
     , U71(tt()) -> U72(isPalListKind())
     , U72(tt()) -> U73(isPal())
     , U73(tt()) -> U74(isPalListKind())
     , isPal() -> tt()
     , isPal() -> U81(isPalListKind())
     , U74(tt()) -> tt()
     , U81(tt()) -> U82(isPalListKind())
     , U82(tt()) -> U83(isNePal())
     , U83(tt()) -> tt()
     , isNePal() -> U61(isPalListKind())
     , isNePal() -> U71(isQid())
     , U91(tt()) -> U92(isPalListKind())
     , U92(tt()) -> tt() }
   Weak DPs:
     { U11^#(tt()) -> c_4(U12^#(isPalListKind()))
     , U12^#(tt()) -> c_5(U13^#(isNeList()))
     , U13^#(tt()) -> c_8()
     , isPalListKind^#() -> c_6()
     , isPalListKind^#() -> c_7(U91^#(isPalListKind()))
     , U91^#(tt()) -> c_51(U92^#(isPalListKind()))
     , isNeList^#() -> c_9(U31^#(isPalListKind()))
     , U31^#(tt()) -> c_21(U32^#(isPalListKind()))
     , U22^#(tt()) -> c_13(U23^#(isPalListKind()))
     , U23^#(tt()) -> c_14(U24^#(isPalListKind()))
     , U24^#(tt()) -> c_15(U25^#(isList()))
     , U25^#(tt()) -> c_16(U26^#(isList()))
     , U26^#(tt()) -> c_20()
     , isList^#() -> c_17(U11^#(isPalListKind()))
     , isList^#() -> c_18()
     , U32^#(tt()) -> c_22(U33^#(isQid()))
     , U33^#(tt()) -> c_23()
     , isQid^#() -> c_24()
     , U42^#(tt()) -> c_26(U43^#(isPalListKind()))
     , U43^#(tt()) -> c_27(U44^#(isPalListKind()))
     , U44^#(tt()) -> c_28(U45^#(isList()))
     , U45^#(tt()) -> c_29(U46^#(isNeList()))
     , U46^#(tt()) -> c_30()
     , U52^#(tt()) -> c_32(U53^#(isPalListKind()))
     , U53^#(tt()) -> c_33(U54^#(isPalListKind()))
     , U54^#(tt()) -> c_34(U55^#(isNeList()))
     , U55^#(tt()) -> c_35(U56^#(isList()))
     , U56^#(tt()) -> c_36()
     , U61^#(tt()) -> c_37(U62^#(isPalListKind()))
     , U62^#(tt()) -> c_38(U63^#(isQid()))
     , U63^#(tt()) -> c_39()
     , U71^#(tt()) -> c_40(U72^#(isPalListKind()))
     , U72^#(tt()) -> c_41(U73^#(isPal()))
     , U73^#(tt()) -> c_42(U74^#(isPalListKind()))
     , U74^#(tt()) -> c_45()
     , isPal^#() -> c_43()
     , isPal^#() -> c_44(U81^#(isPalListKind()))
     , U81^#(tt()) -> c_46(U82^#(isPalListKind()))
     , U82^#(tt()) -> c_47(U83^#(isNePal()))
     , U83^#(tt()) -> c_48()
     , isNePal^#() -> c_49(U61^#(isPalListKind()))
     , isNePal^#() -> c_50(U71^#(isQid()))
     , U92^#(tt()) -> c_52() }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   We estimate the number of application of {6,7,8} by applications of
   Pre({6,7,8}) = {1,3,4,5,9}. Here rules are labeled as follows:
   
     DPs:
       { 1: __^#(X, nil()) -> c_1(X)
       , 2: __^#(__(X, Y), Z) -> c_2(__^#(X, __(Y, Z)))
       , 3: __^#(nil(), X) -> c_3(X)
       , 4: isNeList^#() -> c_10(U41^#(isPalListKind()))
       , 5: isNeList^#() -> c_11(U51^#(isPalListKind()))
       , 6: U41^#(tt()) -> c_25(U42^#(isPalListKind()))
       , 7: U51^#(tt()) -> c_31(U52^#(isPalListKind()))
       , 8: U21^#(tt()) -> c_12(U22^#(isPalListKind()))
       , 9: isList^#() -> c_19(U21^#(isPalListKind()))
       , 10: U11^#(tt()) -> c_4(U12^#(isPalListKind()))
       , 11: U12^#(tt()) -> c_5(U13^#(isNeList()))
       , 12: U13^#(tt()) -> c_8()
       , 13: isPalListKind^#() -> c_6()
       , 14: isPalListKind^#() -> c_7(U91^#(isPalListKind()))
       , 15: U91^#(tt()) -> c_51(U92^#(isPalListKind()))
       , 16: isNeList^#() -> c_9(U31^#(isPalListKind()))
       , 17: U31^#(tt()) -> c_21(U32^#(isPalListKind()))
       , 18: U22^#(tt()) -> c_13(U23^#(isPalListKind()))
       , 19: U23^#(tt()) -> c_14(U24^#(isPalListKind()))
       , 20: U24^#(tt()) -> c_15(U25^#(isList()))
       , 21: U25^#(tt()) -> c_16(U26^#(isList()))
       , 22: U26^#(tt()) -> c_20()
       , 23: isList^#() -> c_17(U11^#(isPalListKind()))
       , 24: isList^#() -> c_18()
       , 25: U32^#(tt()) -> c_22(U33^#(isQid()))
       , 26: U33^#(tt()) -> c_23()
       , 27: isQid^#() -> c_24()
       , 28: U42^#(tt()) -> c_26(U43^#(isPalListKind()))
       , 29: U43^#(tt()) -> c_27(U44^#(isPalListKind()))
       , 30: U44^#(tt()) -> c_28(U45^#(isList()))
       , 31: U45^#(tt()) -> c_29(U46^#(isNeList()))
       , 32: U46^#(tt()) -> c_30()
       , 33: U52^#(tt()) -> c_32(U53^#(isPalListKind()))
       , 34: U53^#(tt()) -> c_33(U54^#(isPalListKind()))
       , 35: U54^#(tt()) -> c_34(U55^#(isNeList()))
       , 36: U55^#(tt()) -> c_35(U56^#(isList()))
       , 37: U56^#(tt()) -> c_36()
       , 38: U61^#(tt()) -> c_37(U62^#(isPalListKind()))
       , 39: U62^#(tt()) -> c_38(U63^#(isQid()))
       , 40: U63^#(tt()) -> c_39()
       , 41: U71^#(tt()) -> c_40(U72^#(isPalListKind()))
       , 42: U72^#(tt()) -> c_41(U73^#(isPal()))
       , 43: U73^#(tt()) -> c_42(U74^#(isPalListKind()))
       , 44: U74^#(tt()) -> c_45()
       , 45: isPal^#() -> c_43()
       , 46: isPal^#() -> c_44(U81^#(isPalListKind()))
       , 47: U81^#(tt()) -> c_46(U82^#(isPalListKind()))
       , 48: U82^#(tt()) -> c_47(U83^#(isNePal()))
       , 49: U83^#(tt()) -> c_48()
       , 50: isNePal^#() -> c_49(U61^#(isPalListKind()))
       , 51: isNePal^#() -> c_50(U71^#(isQid()))
       , 52: U92^#(tt()) -> c_52() }
   
   We are left with following problem, upon which TcT provides the
   certificate MAYBE.
   
   Strict DPs:
     { __^#(X, nil()) -> c_1(X)
     , __^#(__(X, Y), Z) -> c_2(__^#(X, __(Y, Z)))
     , __^#(nil(), X) -> c_3(X)
     , isNeList^#() -> c_10(U41^#(isPalListKind()))
     , isNeList^#() -> c_11(U51^#(isPalListKind()))
     , isList^#() -> c_19(U21^#(isPalListKind())) }
   Strict Trs:
     { __(X, nil()) -> X
     , __(__(X, Y), Z) -> __(X, __(Y, Z))
     , __(nil(), X) -> X
     , U11(tt()) -> U12(isPalListKind())
     , U12(tt()) -> U13(isNeList())
     , isPalListKind() -> tt()
     , isPalListKind() -> U91(isPalListKind())
     , U13(tt()) -> tt()
     , isNeList() -> U31(isPalListKind())
     , isNeList() -> U41(isPalListKind())
     , isNeList() -> U51(isPalListKind())
     , U21(tt()) -> U22(isPalListKind())
     , U22(tt()) -> U23(isPalListKind())
     , U23(tt()) -> U24(isPalListKind())
     , U24(tt()) -> U25(isList())
     , U25(tt()) -> U26(isList())
     , isList() -> U11(isPalListKind())
     , isList() -> tt()
     , isList() -> U21(isPalListKind())
     , U26(tt()) -> tt()
     , U31(tt()) -> U32(isPalListKind())
     , U32(tt()) -> U33(isQid())
     , U33(tt()) -> tt()
     , isQid() -> tt()
     , U41(tt()) -> U42(isPalListKind())
     , U42(tt()) -> U43(isPalListKind())
     , U43(tt()) -> U44(isPalListKind())
     , U44(tt()) -> U45(isList())
     , U45(tt()) -> U46(isNeList())
     , U46(tt()) -> tt()
     , U51(tt()) -> U52(isPalListKind())
     , U52(tt()) -> U53(isPalListKind())
     , U53(tt()) -> U54(isPalListKind())
     , U54(tt()) -> U55(isNeList())
     , U55(tt()) -> U56(isList())
     , U56(tt()) -> tt()
     , U61(tt()) -> U62(isPalListKind())
     , U62(tt()) -> U63(isQid())
     , U63(tt()) -> tt()
     , U71(tt()) -> U72(isPalListKind())
     , U72(tt()) -> U73(isPal())
     , U73(tt()) -> U74(isPalListKind())
     , isPal() -> tt()
     , isPal() -> U81(isPalListKind())
     , U74(tt()) -> tt()
     , U81(tt()) -> U82(isPalListKind())
     , U82(tt()) -> U83(isNePal())
     , U83(tt()) -> tt()
     , isNePal() -> U61(isPalListKind())
     , isNePal() -> U71(isQid())
     , U91(tt()) -> U92(isPalListKind())
     , U92(tt()) -> tt() }
   Weak DPs:
     { U11^#(tt()) -> c_4(U12^#(isPalListKind()))
     , U12^#(tt()) -> c_5(U13^#(isNeList()))
     , U13^#(tt()) -> c_8()
     , isPalListKind^#() -> c_6()
     , isPalListKind^#() -> c_7(U91^#(isPalListKind()))
     , U91^#(tt()) -> c_51(U92^#(isPalListKind()))
     , isNeList^#() -> c_9(U31^#(isPalListKind()))
     , U31^#(tt()) -> c_21(U32^#(isPalListKind()))
     , U41^#(tt()) -> c_25(U42^#(isPalListKind()))
     , U51^#(tt()) -> c_31(U52^#(isPalListKind()))
     , U21^#(tt()) -> c_12(U22^#(isPalListKind()))
     , U22^#(tt()) -> c_13(U23^#(isPalListKind()))
     , U23^#(tt()) -> c_14(U24^#(isPalListKind()))
     , U24^#(tt()) -> c_15(U25^#(isList()))
     , U25^#(tt()) -> c_16(U26^#(isList()))
     , U26^#(tt()) -> c_20()
     , isList^#() -> c_17(U11^#(isPalListKind()))
     , isList^#() -> c_18()
     , U32^#(tt()) -> c_22(U33^#(isQid()))
     , U33^#(tt()) -> c_23()
     , isQid^#() -> c_24()
     , U42^#(tt()) -> c_26(U43^#(isPalListKind()))
     , U43^#(tt()) -> c_27(U44^#(isPalListKind()))
     , U44^#(tt()) -> c_28(U45^#(isList()))
     , U45^#(tt()) -> c_29(U46^#(isNeList()))
     , U46^#(tt()) -> c_30()
     , U52^#(tt()) -> c_32(U53^#(isPalListKind()))
     , U53^#(tt()) -> c_33(U54^#(isPalListKind()))
     , U54^#(tt()) -> c_34(U55^#(isNeList()))
     , U55^#(tt()) -> c_35(U56^#(isList()))
     , U56^#(tt()) -> c_36()
     , U61^#(tt()) -> c_37(U62^#(isPalListKind()))
     , U62^#(tt()) -> c_38(U63^#(isQid()))
     , U63^#(tt()) -> c_39()
     , U71^#(tt()) -> c_40(U72^#(isPalListKind()))
     , U72^#(tt()) -> c_41(U73^#(isPal()))
     , U73^#(tt()) -> c_42(U74^#(isPalListKind()))
     , U74^#(tt()) -> c_45()
     , isPal^#() -> c_43()
     , isPal^#() -> c_44(U81^#(isPalListKind()))
     , U81^#(tt()) -> c_46(U82^#(isPalListKind()))
     , U82^#(tt()) -> c_47(U83^#(isNePal()))
     , U83^#(tt()) -> c_48()
     , isNePal^#() -> c_49(U61^#(isPalListKind()))
     , isNePal^#() -> c_50(U71^#(isQid()))
     , U92^#(tt()) -> c_52() }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   We estimate the number of application of {4,5,6} by applications of
   Pre({4,5,6}) = {1,3}. Here rules are labeled as follows:
   
     DPs:
       { 1: __^#(X, nil()) -> c_1(X)
       , 2: __^#(__(X, Y), Z) -> c_2(__^#(X, __(Y, Z)))
       , 3: __^#(nil(), X) -> c_3(X)
       , 4: isNeList^#() -> c_10(U41^#(isPalListKind()))
       , 5: isNeList^#() -> c_11(U51^#(isPalListKind()))
       , 6: isList^#() -> c_19(U21^#(isPalListKind()))
       , 7: U11^#(tt()) -> c_4(U12^#(isPalListKind()))
       , 8: U12^#(tt()) -> c_5(U13^#(isNeList()))
       , 9: U13^#(tt()) -> c_8()
       , 10: isPalListKind^#() -> c_6()
       , 11: isPalListKind^#() -> c_7(U91^#(isPalListKind()))
       , 12: U91^#(tt()) -> c_51(U92^#(isPalListKind()))
       , 13: isNeList^#() -> c_9(U31^#(isPalListKind()))
       , 14: U31^#(tt()) -> c_21(U32^#(isPalListKind()))
       , 15: U41^#(tt()) -> c_25(U42^#(isPalListKind()))
       , 16: U51^#(tt()) -> c_31(U52^#(isPalListKind()))
       , 17: U21^#(tt()) -> c_12(U22^#(isPalListKind()))
       , 18: U22^#(tt()) -> c_13(U23^#(isPalListKind()))
       , 19: U23^#(tt()) -> c_14(U24^#(isPalListKind()))
       , 20: U24^#(tt()) -> c_15(U25^#(isList()))
       , 21: U25^#(tt()) -> c_16(U26^#(isList()))
       , 22: U26^#(tt()) -> c_20()
       , 23: isList^#() -> c_17(U11^#(isPalListKind()))
       , 24: isList^#() -> c_18()
       , 25: U32^#(tt()) -> c_22(U33^#(isQid()))
       , 26: U33^#(tt()) -> c_23()
       , 27: isQid^#() -> c_24()
       , 28: U42^#(tt()) -> c_26(U43^#(isPalListKind()))
       , 29: U43^#(tt()) -> c_27(U44^#(isPalListKind()))
       , 30: U44^#(tt()) -> c_28(U45^#(isList()))
       , 31: U45^#(tt()) -> c_29(U46^#(isNeList()))
       , 32: U46^#(tt()) -> c_30()
       , 33: U52^#(tt()) -> c_32(U53^#(isPalListKind()))
       , 34: U53^#(tt()) -> c_33(U54^#(isPalListKind()))
       , 35: U54^#(tt()) -> c_34(U55^#(isNeList()))
       , 36: U55^#(tt()) -> c_35(U56^#(isList()))
       , 37: U56^#(tt()) -> c_36()
       , 38: U61^#(tt()) -> c_37(U62^#(isPalListKind()))
       , 39: U62^#(tt()) -> c_38(U63^#(isQid()))
       , 40: U63^#(tt()) -> c_39()
       , 41: U71^#(tt()) -> c_40(U72^#(isPalListKind()))
       , 42: U72^#(tt()) -> c_41(U73^#(isPal()))
       , 43: U73^#(tt()) -> c_42(U74^#(isPalListKind()))
       , 44: U74^#(tt()) -> c_45()
       , 45: isPal^#() -> c_43()
       , 46: isPal^#() -> c_44(U81^#(isPalListKind()))
       , 47: U81^#(tt()) -> c_46(U82^#(isPalListKind()))
       , 48: U82^#(tt()) -> c_47(U83^#(isNePal()))
       , 49: U83^#(tt()) -> c_48()
       , 50: isNePal^#() -> c_49(U61^#(isPalListKind()))
       , 51: isNePal^#() -> c_50(U71^#(isQid()))
       , 52: U92^#(tt()) -> c_52() }
   
   We are left with following problem, upon which TcT provides the
   certificate MAYBE.
   
   Strict DPs:
     { __^#(X, nil()) -> c_1(X)
     , __^#(__(X, Y), Z) -> c_2(__^#(X, __(Y, Z)))
     , __^#(nil(), X) -> c_3(X) }
   Strict Trs:
     { __(X, nil()) -> X
     , __(__(X, Y), Z) -> __(X, __(Y, Z))
     , __(nil(), X) -> X
     , U11(tt()) -> U12(isPalListKind())
     , U12(tt()) -> U13(isNeList())
     , isPalListKind() -> tt()
     , isPalListKind() -> U91(isPalListKind())
     , U13(tt()) -> tt()
     , isNeList() -> U31(isPalListKind())
     , isNeList() -> U41(isPalListKind())
     , isNeList() -> U51(isPalListKind())
     , U21(tt()) -> U22(isPalListKind())
     , U22(tt()) -> U23(isPalListKind())
     , U23(tt()) -> U24(isPalListKind())
     , U24(tt()) -> U25(isList())
     , U25(tt()) -> U26(isList())
     , isList() -> U11(isPalListKind())
     , isList() -> tt()
     , isList() -> U21(isPalListKind())
     , U26(tt()) -> tt()
     , U31(tt()) -> U32(isPalListKind())
     , U32(tt()) -> U33(isQid())
     , U33(tt()) -> tt()
     , isQid() -> tt()
     , U41(tt()) -> U42(isPalListKind())
     , U42(tt()) -> U43(isPalListKind())
     , U43(tt()) -> U44(isPalListKind())
     , U44(tt()) -> U45(isList())
     , U45(tt()) -> U46(isNeList())
     , U46(tt()) -> tt()
     , U51(tt()) -> U52(isPalListKind())
     , U52(tt()) -> U53(isPalListKind())
     , U53(tt()) -> U54(isPalListKind())
     , U54(tt()) -> U55(isNeList())
     , U55(tt()) -> U56(isList())
     , U56(tt()) -> tt()
     , U61(tt()) -> U62(isPalListKind())
     , U62(tt()) -> U63(isQid())
     , U63(tt()) -> tt()
     , U71(tt()) -> U72(isPalListKind())
     , U72(tt()) -> U73(isPal())
     , U73(tt()) -> U74(isPalListKind())
     , isPal() -> tt()
     , isPal() -> U81(isPalListKind())
     , U74(tt()) -> tt()
     , U81(tt()) -> U82(isPalListKind())
     , U82(tt()) -> U83(isNePal())
     , U83(tt()) -> tt()
     , isNePal() -> U61(isPalListKind())
     , isNePal() -> U71(isQid())
     , U91(tt()) -> U92(isPalListKind())
     , U92(tt()) -> tt() }
   Weak DPs:
     { U11^#(tt()) -> c_4(U12^#(isPalListKind()))
     , U12^#(tt()) -> c_5(U13^#(isNeList()))
     , U13^#(tt()) -> c_8()
     , isPalListKind^#() -> c_6()
     , isPalListKind^#() -> c_7(U91^#(isPalListKind()))
     , U91^#(tt()) -> c_51(U92^#(isPalListKind()))
     , isNeList^#() -> c_9(U31^#(isPalListKind()))
     , isNeList^#() -> c_10(U41^#(isPalListKind()))
     , isNeList^#() -> c_11(U51^#(isPalListKind()))
     , U31^#(tt()) -> c_21(U32^#(isPalListKind()))
     , U41^#(tt()) -> c_25(U42^#(isPalListKind()))
     , U51^#(tt()) -> c_31(U52^#(isPalListKind()))
     , U21^#(tt()) -> c_12(U22^#(isPalListKind()))
     , U22^#(tt()) -> c_13(U23^#(isPalListKind()))
     , U23^#(tt()) -> c_14(U24^#(isPalListKind()))
     , U24^#(tt()) -> c_15(U25^#(isList()))
     , U25^#(tt()) -> c_16(U26^#(isList()))
     , U26^#(tt()) -> c_20()
     , isList^#() -> c_17(U11^#(isPalListKind()))
     , isList^#() -> c_18()
     , isList^#() -> c_19(U21^#(isPalListKind()))
     , U32^#(tt()) -> c_22(U33^#(isQid()))
     , U33^#(tt()) -> c_23()
     , isQid^#() -> c_24()
     , U42^#(tt()) -> c_26(U43^#(isPalListKind()))
     , U43^#(tt()) -> c_27(U44^#(isPalListKind()))
     , U44^#(tt()) -> c_28(U45^#(isList()))
     , U45^#(tt()) -> c_29(U46^#(isNeList()))
     , U46^#(tt()) -> c_30()
     , U52^#(tt()) -> c_32(U53^#(isPalListKind()))
     , U53^#(tt()) -> c_33(U54^#(isPalListKind()))
     , U54^#(tt()) -> c_34(U55^#(isNeList()))
     , U55^#(tt()) -> c_35(U56^#(isList()))
     , U56^#(tt()) -> c_36()
     , U61^#(tt()) -> c_37(U62^#(isPalListKind()))
     , U62^#(tt()) -> c_38(U63^#(isQid()))
     , U63^#(tt()) -> c_39()
     , U71^#(tt()) -> c_40(U72^#(isPalListKind()))
     , U72^#(tt()) -> c_41(U73^#(isPal()))
     , U73^#(tt()) -> c_42(U74^#(isPalListKind()))
     , U74^#(tt()) -> c_45()
     , isPal^#() -> c_43()
     , isPal^#() -> c_44(U81^#(isPalListKind()))
     , U81^#(tt()) -> c_46(U82^#(isPalListKind()))
     , U82^#(tt()) -> c_47(U83^#(isNePal()))
     , U83^#(tt()) -> c_48()
     , isNePal^#() -> c_49(U61^#(isPalListKind()))
     , isNePal^#() -> c_50(U71^#(isQid()))
     , U92^#(tt()) -> c_52() }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   Empty strict component of the problem is NOT empty.


Arrrr..