Problem:
 and(tt()) -> X
 __(__(X,Y),Z) -> __(X,__(Y,Z))
 __(X,nil()) -> X
 __(nil(),X) -> X
 U11(tt()) -> U12(isNeList())
 U12(tt()) -> tt()
 U21(tt()) -> U22(isList())
 U22(tt()) -> U23(isList())
 U23(tt()) -> tt()
 U31(tt()) -> U32(isQid())
 U32(tt()) -> tt()
 U41(tt()) -> U42(isList())
 U42(tt()) -> U43(isNeList())
 U43(tt()) -> tt()
 U51(tt()) -> U52(isNeList())
 U52(tt()) -> U53(isList())
 U53(tt()) -> tt()
 U61(tt()) -> U62(isQid())
 U62(tt()) -> tt()
 U71(tt()) -> U72(isNePal())
 U72(tt()) -> tt()
 isList() -> U11(isPalListKind())
 isList() -> tt()
 isList() -> U21(and(isPalListKind()))
 isNeList() -> U31(isPalListKind())
 isNeList() -> U41(and(isPalListKind()))
 isNeList() -> U51(and(isPalListKind()))
 isNePal() -> U61(isPalListKind())
 isNePal() -> and(and(isQid()))
 isPal() -> U71(isPalListKind())
 isPal() -> tt()
 isPalListKind() -> tt()
 isPalListKind() -> and(isPalListKind())
 isQid() -> tt()

Proof:
 Fresh Variable Processor: loop length: 1
                           terms:
                            and(tt())
                           context: []
                           substitution:
                            X -> and(tt())
  Qed