Input TRS:
    1: __(__(X,Y),Z) -> __(X,__(Y,Z))
    2: __(X,nil()) -> X
    3: __(nil(),X) -> X
    4: U11(tt()) -> tt()
    5: U21(tt()) -> U22(isList())
    6: U22(tt()) -> tt()
    7: U31(tt()) -> tt()
    8: U41(tt()) -> U42(isNeList())
    9: U42(tt()) -> tt()
    10: U51(tt()) -> U52(isList())
    11: U52(tt()) -> tt()
    12: U61(tt()) -> tt()
    13: U71(tt()) -> U72(isPal())
    14: U72(tt()) -> tt()
    15: U81(tt()) -> tt()
    16: isList() -> U11(isNeList())
    17: isList() -> tt()
    18: isList() -> U21(isList())
    19: isNeList() -> U31(isQid())
    20: isNeList() -> U41(isList())
    21: isNeList() -> U51(isNeList())
    22: isNePal() -> U61(isQid())
    23: isNePal() -> U71(isQid())
    24: isPal() -> U81(isNePal())
    25: isPal() -> tt()
    26: isQid() -> tt()
Number of strict rules: 26
Direct Order(PosReal,>,Poly) ... removes: 1 3 2
   U21(x1)	weight: x1
   U11(x1)	weight: x1
isNeList()	weight: 0
 isPal()	weight: 0
   U42(x1)	weight: x1
   U71(x1)	weight: x1
isNePal()	weight: 0
   U72(x1)	weight: x1
 isQid()	weight: 0
isList()	weight: 0
   nil()	weight: 0
   U52(x1)	weight: x1
   U61(x1)	weight: x1
   U31(x1)	weight: x1
   U81(x1)	weight: x1
    tt()	weight: 0
   U22(x1)	weight: x1
   U51(x1)	weight: x1
   U41(x1)	weight: x1
    __(x1,x2)	weight: (/ 1 4) + 2 * x1 + x2
Number of strict rules: 23
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #U71(tt()) -> #U72(isPal())
   #2: #U71(tt()) -> #isPal()
   #3: #isPal() -> #U81(isNePal())
   #4: #isPal() -> #isNePal()
   #5: #isNePal() -> #U71(isQid())
   #6: #isNePal() -> #isQid()
   #7: #isNeList() -> #U41(isList())
   #8: #isNeList() -> #isList()
   #9: #U51(tt()) -> #U52(isList())
   #10: #U51(tt()) -> #isList()
   #11: #U21(tt()) -> #U22(isList())
   #12: #U21(tt()) -> #isList()
   #13: #isNePal() -> #U61(isQid())
   #14: #isNePal() -> #isQid()
   #15: #isNeList() -> #U31(isQid())
   #16: #isNeList() -> #isQid()
   #17: #isNeList() -> #U51(isNeList())
   #18: #isNeList() -> #isNeList()
   #19: #isList() -> #U11(isNeList())
   #20: #isList() -> #isNeList()
   #21: #U41(tt()) -> #U42(isNeList())
   #22: #U41(tt()) -> #isNeList()
   #23: #isList() -> #U21(isList())
   #24: #isList() -> #isList()
Number of SCCs: 2, DPs: 13, edges: 30
	SCC { #2 #4 #5 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... Order(PosReal,>,Sum-Sum; PosReal,≥,Sum-Sum)... Order(PosReal,>,Sum-Sum; NegReal,≥,Sum)... Order(PosReal,>,MaxSum-Sum; NegReal,≥,Sum)... failed.
Removing edges: failed.
Finding a loop...  found.
  #isPal()	-#4->
  #isNePal()	--->*
  #isNePal()	-#5->
  #U71(isQid())	--->*
  #U71(tt())	-#2->
  #isPal()	--->*
  #isPal()
  Looping with: [ ]
NO