0.002/0.002 NO 0.002/0.002 0.002/0.002 Problem 1: 0.002/0.002 0.002/0.002 0.002/0.002 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.002/0.002 Confluence Problem: 0.002/0.002 (VAR vNonEmpty:S I:S P:S V:S V1:S V2:S X:S Y:S Z:S) 0.002/0.002 (STRATEGY CONTEXTSENSITIVE 0.002/0.002 (U11 1) 0.002/0.002 (U12 1) 0.002/0.002 (U13 1) 0.002/0.002 (U21 1) 0.002/0.002 (U22 1) 0.002/0.002 (U23 1) 0.002/0.002 (U24 1) 0.002/0.002 (U25 1) 0.002/0.002 (U26 1) 0.002/0.002 (U31 1) 0.002/0.002 (U32 1) 0.002/0.002 (U33 1) 0.002/0.002 (U41 1) 0.002/0.002 (U42 1) 0.002/0.002 (U43 1) 0.002/0.002 (U44 1) 0.002/0.002 (U45 1) 0.002/0.002 (U46 1) 0.002/0.002 (U51 1) 0.002/0.002 (U52 1) 0.002/0.002 (U53 1) 0.002/0.002 (U54 1) 0.002/0.002 (U55 1) 0.002/0.002 (U56 1) 0.002/0.002 (U61 1) 0.002/0.002 (U62 1) 0.002/0.002 (U63 1) 0.002/0.002 (U71 1) 0.002/0.002 (U72 1) 0.002/0.002 (U73 1) 0.002/0.002 (U74 1) 0.002/0.002 (U81 1) 0.002/0.002 (U82 1) 0.002/0.002 (U83 1) 0.002/0.002 (U91 1) 0.002/0.002 (U92 1) 0.002/0.002 (__ 1 2) 0.002/0.002 (isList) 0.002/0.002 (isNeList) 0.002/0.002 (isNePal) 0.002/0.002 (isPal) 0.002/0.002 (isPalListKind) 0.002/0.002 (isQid) 0.002/0.002 (a) 0.002/0.002 (e) 0.002/0.002 (fSNonEmpty) 0.002/0.002 (i) 0.002/0.002 (nil) 0.002/0.002 (o) 0.002/0.002 (tt) 0.002/0.002 (u) 0.002/0.002 ) 0.002/0.002 (RULES 0.002/0.002 U11(tt,V:S) -> U12(isPalListKind(V:S),V:S) 0.002/0.002 U12(tt,V:S) -> U13(isNeList(V:S)) 0.002/0.002 U13(tt) -> tt 0.002/0.002 U21(tt,V1:S,V2:S) -> U22(isPalListKind(V1:S),V1:S,V2:S) 0.002/0.002 U22(tt,V1:S,V2:S) -> U23(isPalListKind(V2:S),V1:S,V2:S) 0.002/0.002 U23(tt,V1:S,V2:S) -> U24(isPalListKind(V2:S),V1:S,V2:S) 0.002/0.002 U24(tt,V1:S,V2:S) -> U25(isList(V1:S),V2:S) 0.002/0.002 U25(tt,V2:S) -> U26(isList(V2:S)) 0.002/0.002 U26(tt) -> tt 0.002/0.002 U31(tt,V:S) -> U32(isPalListKind(V:S),V:S) 0.002/0.002 U32(tt,V:S) -> U33(isQid(V:S)) 0.002/0.002 U33(tt) -> tt 0.002/0.002 U41(tt,V1:S,V2:S) -> U42(isPalListKind(V1:S),V1:S,V2:S) 0.002/0.002 U42(tt,V1:S,V2:S) -> U43(isPalListKind(V2:S),V1:S,V2:S) 0.002/0.002 U43(tt,V1:S,V2:S) -> U44(isPalListKind(V2:S),V1:S,V2:S) 0.002/0.002 U44(tt,V1:S,V2:S) -> U45(isList(V1:S),V2:S) 0.002/0.002 U45(tt,V2:S) -> U46(isNeList(V2:S)) 0.002/0.002 U46(tt) -> tt 0.002/0.002 U51(tt,V1:S,V2:S) -> U52(isPalListKind(V1:S),V1:S,V2:S) 0.002/0.002 U52(tt,V1:S,V2:S) -> U53(isPalListKind(V2:S),V1:S,V2:S) 0.002/0.002 U53(tt,V1:S,V2:S) -> U54(isPalListKind(V2:S),V1:S,V2:S) 0.002/0.002 U54(tt,V1:S,V2:S) -> U55(isNeList(V1:S),V2:S) 0.002/0.002 U55(tt,V2:S) -> U56(isList(V2:S)) 0.002/0.002 U56(tt) -> tt 0.002/0.002 U61(tt,V:S) -> U62(isPalListKind(V:S),V:S) 0.002/0.002 U62(tt,V:S) -> U63(isQid(V:S)) 0.002/0.002 U63(tt) -> tt 0.002/0.002 U71(tt,I:S,P:S) -> U72(isPalListKind(I:S),P:S) 0.002/0.002 U72(tt,P:S) -> U73(isPal(P:S),P:S) 0.002/0.002 U73(tt,P:S) -> U74(isPalListKind(P:S)) 0.002/0.002 U74(tt) -> tt 0.002/0.002 U81(tt,V:S) -> U82(isPalListKind(V:S),V:S) 0.002/0.002 U82(tt,V:S) -> U83(isNePal(V:S)) 0.002/0.002 U83(tt) -> tt 0.002/0.002 U91(tt,V2:S) -> U92(isPalListKind(V2:S)) 0.002/0.002 U92(tt) -> tt 0.002/0.002 __(__(X:S,Y:S),Z:S) -> __(X:S,__(Y:S,Z:S)) 0.002/0.002 __(nil,X:S) -> X:S 0.002/0.002 __(X:S,nil) -> X:S 0.002/0.002 isList(__(V1:S,V2:S)) -> U21(isPalListKind(V1:S),V1:S,V2:S) 0.002/0.002 isList(nil) -> tt 0.002/0.002 isList(V:S) -> U11(isPalListKind(V:S),V:S) 0.002/0.002 isNeList(__(V1:S,V2:S)) -> U41(isPalListKind(V1:S),V1:S,V2:S) 0.002/0.002 isNeList(__(V1:S,V2:S)) -> U51(isPalListKind(V1:S),V1:S,V2:S) 0.002/0.002 isNeList(V:S) -> U31(isPalListKind(V:S),V:S) 0.002/0.002 isNePal(__(I:S,__(P:S,I:S))) -> U71(isQid(I:S),I:S,P:S) 0.002/0.002 isNePal(V:S) -> U61(isPalListKind(V:S),V:S) 0.002/0.002 isPal(nil) -> tt 0.002/0.002 isPal(V:S) -> U81(isPalListKind(V:S),V:S) 0.002/0.002 isPalListKind(__(V1:S,V2:S)) -> U91(isPalListKind(V1:S),V2:S) 0.002/0.002 isPalListKind(a) -> tt 0.002/0.002 isPalListKind(e) -> tt 0.002/0.002 isPalListKind(i) -> tt 0.002/0.002 isPalListKind(nil) -> tt 0.002/0.002 isPalListKind(o) -> tt 0.002/0.002 isPalListKind(u) -> tt 0.002/0.002 isQid(a) -> tt 0.002/0.002 isQid(e) -> tt 0.002/0.002 isQid(i) -> tt 0.002/0.002 isQid(o) -> tt 0.002/0.002 isQid(u) -> tt 0.002/0.002 ) 0.002/0.002 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.002/0.002 0.002/0.002 0.002/0.002 Problem 1: 0.002/0.002 0.002/0.002 CleanTRS Processor: 0.002/0.002 0.002/0.002 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.002/0.002 Confluence Problem: 0.002/0.002 (VAR vNonEmpty:S I:S P:S V:S V1:S V2:S X:S Y:S Z:S) 0.002/0.002 (STRATEGY CONTEXTSENSITIVE 0.002/0.002 (U11 1) 0.002/0.002 (U12 1) 0.002/0.002 (U13 1) 0.002/0.002 (U21 1) 0.002/0.002 (U22 1) 0.002/0.002 (U23 1) 0.002/0.002 (U24 1) 0.002/0.002 (U25 1) 0.002/0.002 (U26 1) 0.002/0.002 (U31 1) 0.002/0.002 (U32 1) 0.002/0.002 (U33 1) 0.002/0.002 (U41 1) 0.002/0.002 (U42 1) 0.002/0.002 (U43 1) 0.002/0.002 (U44 1) 0.002/0.002 (U45 1) 0.002/0.002 (U46 1) 0.002/0.002 (U51 1) 0.002/0.002 (U52 1) 0.002/0.002 (U53 1) 0.002/0.002 (U54 1) 0.002/0.002 (U55 1) 0.002/0.002 (U56 1) 0.002/0.002 (U61 1) 0.002/0.002 (U62 1) 0.002/0.002 (U63 1) 0.002/0.002 (U71 1) 0.002/0.002 (U72 1) 0.002/0.002 (U73 1) 0.002/0.002 (U74 1) 0.002/0.002 (U81 1) 0.002/0.002 (U82 1) 0.002/0.002 (U83 1) 0.002/0.002 (U91 1) 0.002/0.002 (U92 1) 0.002/0.002 (__ 1 2) 0.002/0.002 (isList) 0.002/0.002 (isNeList) 0.002/0.002 (isNePal) 0.002/0.002 (isPal) 0.002/0.002 (isPalListKind) 0.002/0.002 (isQid) 0.002/0.002 (a) 0.002/0.002 (e) 0.002/0.002 (fSNonEmpty) 0.002/0.002 (i) 0.002/0.002 (nil) 0.002/0.002 (o) 0.002/0.002 (tt) 0.002/0.002 (u) 0.002/0.002 ) 0.002/0.002 (RULES 0.002/0.002 U11(tt,V:S) -> U12(isPalListKind(V:S),V:S) 0.002/0.002 U12(tt,V:S) -> U13(isNeList(V:S)) 0.002/0.002 U13(tt) -> tt 0.002/0.002 U21(tt,V1:S,V2:S) -> U22(isPalListKind(V1:S),V1:S,V2:S) 0.002/0.002 U22(tt,V1:S,V2:S) -> U23(isPalListKind(V2:S),V1:S,V2:S) 0.002/0.002 U23(tt,V1:S,V2:S) -> U24(isPalListKind(V2:S),V1:S,V2:S) 0.002/0.002 U24(tt,V1:S,V2:S) -> U25(isList(V1:S),V2:S) 0.002/0.002 U25(tt,V2:S) -> U26(isList(V2:S)) 0.002/0.002 U26(tt) -> tt 0.002/0.002 U31(tt,V:S) -> U32(isPalListKind(V:S),V:S) 0.002/0.002 U32(tt,V:S) -> U33(isQid(V:S)) 0.002/0.002 U33(tt) -> tt 0.002/0.002 U41(tt,V1:S,V2:S) -> U42(isPalListKind(V1:S),V1:S,V2:S) 0.002/0.002 U42(tt,V1:S,V2:S) -> U43(isPalListKind(V2:S),V1:S,V2:S) 0.002/0.002 U43(tt,V1:S,V2:S) -> U44(isPalListKind(V2:S),V1:S,V2:S) 0.002/0.002 U44(tt,V1:S,V2:S) -> U45(isList(V1:S),V2:S) 0.002/0.002 U45(tt,V2:S) -> U46(isNeList(V2:S)) 0.002/0.002 U46(tt) -> tt 0.002/0.002 U51(tt,V1:S,V2:S) -> U52(isPalListKind(V1:S),V1:S,V2:S) 0.002/0.002 U52(tt,V1:S,V2:S) -> U53(isPalListKind(V2:S),V1:S,V2:S) 0.002/0.002 U53(tt,V1:S,V2:S) -> U54(isPalListKind(V2:S),V1:S,V2:S) 0.002/0.002 U54(tt,V1:S,V2:S) -> U55(isNeList(V1:S),V2:S) 0.002/0.002 U55(tt,V2:S) -> U56(isList(V2:S)) 0.002/0.002 U56(tt) -> tt 0.002/0.002 U61(tt,V:S) -> U62(isPalListKind(V:S),V:S) 0.002/0.002 U62(tt,V:S) -> U63(isQid(V:S)) 0.002/0.002 U63(tt) -> tt 0.002/0.002 U71(tt,I:S,P:S) -> U72(isPalListKind(I:S),P:S) 0.002/0.002 U72(tt,P:S) -> U73(isPal(P:S),P:S) 0.002/0.002 U73(tt,P:S) -> U74(isPalListKind(P:S)) 0.002/0.002 U74(tt) -> tt 0.002/0.002 U81(tt,V:S) -> U82(isPalListKind(V:S),V:S) 0.002/0.002 U82(tt,V:S) -> U83(isNePal(V:S)) 0.002/0.002 U83(tt) -> tt 0.002/0.002 U91(tt,V2:S) -> U92(isPalListKind(V2:S)) 0.002/0.002 U92(tt) -> tt 0.002/0.002 __(__(X:S,Y:S),Z:S) -> __(X:S,__(Y:S,Z:S)) 0.002/0.002 __(nil,X:S) -> X:S 0.002/0.002 __(X:S,nil) -> X:S 0.002/0.002 isList(__(V1:S,V2:S)) -> U21(isPalListKind(V1:S),V1:S,V2:S) 0.002/0.002 isList(nil) -> tt 0.002/0.002 isList(V:S) -> U11(isPalListKind(V:S),V:S) 0.002/0.002 isNeList(__(V1:S,V2:S)) -> U41(isPalListKind(V1:S),V1:S,V2:S) 0.002/0.002 isNeList(__(V1:S,V2:S)) -> U51(isPalListKind(V1:S),V1:S,V2:S) 0.002/0.002 isNeList(V:S) -> U31(isPalListKind(V:S),V:S) 0.002/0.002 isNePal(__(I:S,__(P:S,I:S))) -> U71(isQid(I:S),I:S,P:S) 0.002/0.002 isNePal(V:S) -> U61(isPalListKind(V:S),V:S) 0.002/0.002 isPal(nil) -> tt 0.002/0.002 isPal(V:S) -> U81(isPalListKind(V:S),V:S) 0.002/0.002 isPalListKind(__(V1:S,V2:S)) -> U91(isPalListKind(V1:S),V2:S) 0.002/0.002 isPalListKind(a) -> tt 0.002/0.002 isPalListKind(e) -> tt 0.002/0.002 isPalListKind(i) -> tt 0.002/0.002 isPalListKind(nil) -> tt 0.002/0.002 isPalListKind(o) -> tt 0.002/0.002 isPalListKind(u) -> tt 0.002/0.002 isQid(a) -> tt 0.002/0.002 isQid(e) -> tt 0.002/0.002 isQid(i) -> tt 0.002/0.002 isQid(o) -> tt 0.002/0.002 isQid(u) -> tt 0.002/0.002 ) 0.002/0.002 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.002/0.002 0.002/0.002 0.002/0.002 Problem 1: 0.002/0.002 0.002/0.002 Modular Confluence Combinations Decomposition Processor: 0.002/0.002 It is a CTRS -> No modular confluence 0.002/0.002 0.002/0.002 Problem 1: 0.002/0.002 Left-Homogeneous u-Replacing Variables Processor: 0.002/0.002 R satisfies LHRV condition 0.002/0.002 0.002/0.002 Problem 1: 0.002/0.002 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.002/0.002 Confluence Problem: 0.002/0.002 (VAR vNonEmpty:S I:S P:S V:S V1:S V2:S X:S Y:S Z:S) 0.002/0.002 (STRATEGY CONTEXTSENSITIVE 0.002/0.002 (U11 1) 0.002/0.002 (U12 1) 0.002/0.002 (U13 1) 0.002/0.002 (U21 1) 0.002/0.002 (U22 1) 0.002/0.002 (U23 1) 0.002/0.002 (U24 1) 0.002/0.002 (U25 1) 0.002/0.002 (U26 1) 0.002/0.002 (U31 1) 0.002/0.002 (U32 1) 0.002/0.002 (U33 1) 0.002/0.002 (U41 1) 0.002/0.002 (U42 1) 0.002/0.002 (U43 1) 0.002/0.002 (U44 1) 0.002/0.002 (U45 1) 0.002/0.002 (U46 1) 0.002/0.002 (U51 1) 0.002/0.002 (U52 1) 0.002/0.002 (U53 1) 0.002/0.002 (U54 1) 0.002/0.002 (U55 1) 0.002/0.002 (U56 1) 0.002/0.002 (U61 1) 0.002/0.002 (U62 1) 0.002/0.002 (U63 1) 0.002/0.002 (U71 1) 0.002/0.002 (U72 1) 0.002/0.002 (U73 1) 0.002/0.002 (U74 1) 0.002/0.002 (U81 1) 0.002/0.002 (U82 1) 0.002/0.002 (U83 1) 0.002/0.002 (U91 1) 0.002/0.002 (U92 1) 0.002/0.002 (__ 1 2) 0.002/0.002 (isList) 0.002/0.002 (isNeList) 0.002/0.002 (isNePal) 0.002/0.002 (isPal) 0.002/0.002 (isPalListKind) 0.002/0.002 (isQid) 0.002/0.002 (a) 0.002/0.002 (e) 0.002/0.002 (fSNonEmpty) 0.002/0.002 (i) 0.002/0.002 (nil) 0.002/0.002 (o) 0.002/0.002 (tt) 0.002/0.002 (u) 0.002/0.002 ) 0.002/0.002 (RULES 0.002/0.002 U11(tt,V:S) -> U12(isPalListKind(V:S),V:S) 0.002/0.002 U12(tt,V:S) -> U13(isNeList(V:S)) 0.002/0.002 U13(tt) -> tt 0.002/0.002 U21(tt,V1:S,V2:S) -> U22(isPalListKind(V1:S),V1:S,V2:S) 0.002/0.002 U22(tt,V1:S,V2:S) -> U23(isPalListKind(V2:S),V1:S,V2:S) 0.002/0.002 U23(tt,V1:S,V2:S) -> U24(isPalListKind(V2:S),V1:S,V2:S) 0.002/0.002 U24(tt,V1:S,V2:S) -> U25(isList(V1:S),V2:S) 0.002/0.002 U25(tt,V2:S) -> U26(isList(V2:S)) 0.002/0.002 U26(tt) -> tt 0.002/0.002 U31(tt,V:S) -> U32(isPalListKind(V:S),V:S) 0.002/0.002 U32(tt,V:S) -> U33(isQid(V:S)) 0.002/0.002 U33(tt) -> tt 0.002/0.002 U41(tt,V1:S,V2:S) -> U42(isPalListKind(V1:S),V1:S,V2:S) 0.002/0.002 U42(tt,V1:S,V2:S) -> U43(isPalListKind(V2:S),V1:S,V2:S) 0.002/0.002 U43(tt,V1:S,V2:S) -> U44(isPalListKind(V2:S),V1:S,V2:S) 0.002/0.002 U44(tt,V1:S,V2:S) -> U45(isList(V1:S),V2:S) 0.002/0.002 U45(tt,V2:S) -> U46(isNeList(V2:S)) 0.002/0.002 U46(tt) -> tt 0.002/0.002 U51(tt,V1:S,V2:S) -> U52(isPalListKind(V1:S),V1:S,V2:S) 0.002/0.002 U52(tt,V1:S,V2:S) -> U53(isPalListKind(V2:S),V1:S,V2:S) 0.002/0.002 U53(tt,V1:S,V2:S) -> U54(isPalListKind(V2:S),V1:S,V2:S) 0.002/0.002 U54(tt,V1:S,V2:S) -> U55(isNeList(V1:S),V2:S) 0.002/0.002 U55(tt,V2:S) -> U56(isList(V2:S)) 0.002/0.002 U56(tt) -> tt 0.002/0.002 U61(tt,V:S) -> U62(isPalListKind(V:S),V:S) 0.002/0.002 U62(tt,V:S) -> U63(isQid(V:S)) 0.002/0.002 U63(tt) -> tt 0.002/0.002 U71(tt,I:S,P:S) -> U72(isPalListKind(I:S),P:S) 0.002/0.002 U72(tt,P:S) -> U73(isPal(P:S),P:S) 0.002/0.002 U73(tt,P:S) -> U74(isPalListKind(P:S)) 0.002/0.002 U74(tt) -> tt 0.002/0.002 U81(tt,V:S) -> U82(isPalListKind(V:S),V:S) 0.002/0.002 U82(tt,V:S) -> U83(isNePal(V:S)) 0.002/0.002 U83(tt) -> tt 0.002/0.002 U91(tt,V2:S) -> U92(isPalListKind(V2:S)) 0.002/0.002 U92(tt) -> tt 0.002/0.002 __(__(X:S,Y:S),Z:S) -> __(X:S,__(Y:S,Z:S)) 0.002/0.002 __(nil,X:S) -> X:S 0.002/0.002 __(X:S,nil) -> X:S 0.002/0.002 isList(__(V1:S,V2:S)) -> U21(isPalListKind(V1:S),V1:S,V2:S) 0.002/0.002 isList(nil) -> tt 0.002/0.002 isList(V:S) -> U11(isPalListKind(V:S),V:S) 0.002/0.002 isNeList(__(V1:S,V2:S)) -> U41(isPalListKind(V1:S),V1:S,V2:S) 0.002/0.002 isNeList(__(V1:S,V2:S)) -> U51(isPalListKind(V1:S),V1:S,V2:S) 0.002/0.002 isNeList(V:S) -> U31(isPalListKind(V:S),V:S) 0.002/0.002 isNePal(__(I:S,__(P:S,I:S))) -> U71(isQid(I:S),I:S,P:S) 0.002/0.002 isNePal(V:S) -> U61(isPalListKind(V:S),V:S) 0.002/0.002 isPal(nil) -> tt 0.002/0.002 isPal(V:S) -> U81(isPalListKind(V:S),V:S) 0.002/0.002 isPalListKind(__(V1:S,V2:S)) -> U91(isPalListKind(V1:S),V2:S) 0.002/0.002 isPalListKind(a) -> tt 0.002/0.002 isPalListKind(e) -> tt 0.002/0.002 isPalListKind(i) -> tt 0.002/0.002 isPalListKind(nil) -> tt 0.002/0.002 isPalListKind(o) -> tt 0.002/0.002 isPalListKind(u) -> tt 0.002/0.002 isQid(a) -> tt 0.002/0.002 isQid(e) -> tt 0.002/0.002 isQid(i) -> tt 0.002/0.002 isQid(o) -> tt 0.002/0.002 isQid(u) -> tt 0.002/0.002 ) 0.002/0.002 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.002/0.002 0.002/0.002 Huet Levy Processor: 0.002/0.002 -> Rules: 0.002/0.002 U11(tt,V:S) -> U12(isPalListKind(V:S),V:S) 0.002/0.002 U12(tt,V:S) -> U13(isNeList(V:S)) 0.002/0.002 U13(tt) -> tt 0.002/0.002 U21(tt,V1:S,V2:S) -> U22(isPalListKind(V1:S),V1:S,V2:S) 0.002/0.002 U22(tt,V1:S,V2:S) -> U23(isPalListKind(V2:S),V1:S,V2:S) 0.002/0.002 U23(tt,V1:S,V2:S) -> U24(isPalListKind(V2:S),V1:S,V2:S) 0.002/0.002 U24(tt,V1:S,V2:S) -> U25(isList(V1:S),V2:S) 0.002/0.002 U25(tt,V2:S) -> U26(isList(V2:S)) 0.002/0.002 U26(tt) -> tt 0.002/0.002 U31(tt,V:S) -> U32(isPalListKind(V:S),V:S) 0.002/0.002 U32(tt,V:S) -> U33(isQid(V:S)) 0.002/0.002 U33(tt) -> tt 0.002/0.002 U41(tt,V1:S,V2:S) -> U42(isPalListKind(V1:S),V1:S,V2:S) 0.002/0.002 U42(tt,V1:S,V2:S) -> U43(isPalListKind(V2:S),V1:S,V2:S) 0.002/0.002 U43(tt,V1:S,V2:S) -> U44(isPalListKind(V2:S),V1:S,V2:S) 0.002/0.002 U44(tt,V1:S,V2:S) -> U45(isList(V1:S),V2:S) 0.002/0.002 U45(tt,V2:S) -> U46(isNeList(V2:S)) 0.002/0.002 U46(tt) -> tt 0.002/0.002 U51(tt,V1:S,V2:S) -> U52(isPalListKind(V1:S),V1:S,V2:S) 0.002/0.002 U52(tt,V1:S,V2:S) -> U53(isPalListKind(V2:S),V1:S,V2:S) 0.002/0.002 U53(tt,V1:S,V2:S) -> U54(isPalListKind(V2:S),V1:S,V2:S) 0.002/0.002 U54(tt,V1:S,V2:S) -> U55(isNeList(V1:S),V2:S) 0.002/0.002 U55(tt,V2:S) -> U56(isList(V2:S)) 0.002/0.002 U56(tt) -> tt 0.002/0.002 U61(tt,V:S) -> U62(isPalListKind(V:S),V:S) 0.002/0.002 U62(tt,V:S) -> U63(isQid(V:S)) 0.002/0.002 U63(tt) -> tt 0.002/0.002 U71(tt,I:S,P:S) -> U72(isPalListKind(I:S),P:S) 0.002/0.002 U72(tt,P:S) -> U73(isPal(P:S),P:S) 0.002/0.002 U73(tt,P:S) -> U74(isPalListKind(P:S)) 0.002/0.002 U74(tt) -> tt 0.002/0.002 U81(tt,V:S) -> U82(isPalListKind(V:S),V:S) 0.002/0.002 U82(tt,V:S) -> U83(isNePal(V:S)) 0.002/0.002 U83(tt) -> tt 0.002/0.002 U91(tt,V2:S) -> U92(isPalListKind(V2:S)) 0.002/0.002 U92(tt) -> tt 0.002/0.002 __(__(X:S,Y:S),Z:S) -> __(X:S,__(Y:S,Z:S)) 0.002/0.002 __(nil,X:S) -> X:S 0.002/0.002 __(X:S,nil) -> X:S 0.002/0.002 isList(__(V1:S,V2:S)) -> U21(isPalListKind(V1:S),V1:S,V2:S) 0.002/0.002 isList(nil) -> tt 0.002/0.002 isList(V:S) -> U11(isPalListKind(V:S),V:S) 0.002/0.002 isNeList(__(V1:S,V2:S)) -> U41(isPalListKind(V1:S),V1:S,V2:S) 0.002/0.002 isNeList(__(V1:S,V2:S)) -> U51(isPalListKind(V1:S),V1:S,V2:S) 0.002/0.002 isNeList(V:S) -> U31(isPalListKind(V:S),V:S) 0.002/0.002 isNePal(__(I:S,__(P:S,I:S))) -> U71(isQid(I:S),I:S,P:S) 0.002/0.002 isNePal(V:S) -> U61(isPalListKind(V:S),V:S) 0.002/0.002 isPal(nil) -> tt 0.002/0.002 isPal(V:S) -> U81(isPalListKind(V:S),V:S) 0.002/0.002 isPalListKind(__(V1:S,V2:S)) -> U91(isPalListKind(V1:S),V2:S) 0.002/0.002 isPalListKind(a) -> tt 0.002/0.002 isPalListKind(e) -> tt 0.002/0.002 isPalListKind(i) -> tt 0.002/0.002 isPalListKind(nil) -> tt 0.002/0.002 isPalListKind(o) -> tt 0.002/0.002 isPalListKind(u) -> tt 0.002/0.002 isQid(a) -> tt 0.002/0.002 isQid(e) -> tt 0.002/0.002 isQid(i) -> tt 0.002/0.002 isQid(o) -> tt 0.002/0.002 isQid(u) -> tt 0.002/0.002 -> Vars: 0.002/0.002 V, V, V1, V2, V1, V2, V1, V2, V1, V2, V2, V, V, V1, V2, V1, V2, V1, V2, V1, V2, V2, V1, V2, V1, V2, V1, V2, V1, V2, V2, V, V, I, P, P, P, V, V, V2, X, Y, Z, X, X, V1, V2, V, V1, V2, V1, V2, V, I, P, V, V, V1, V2 0.002/0.002 -> UVars: 0.002/0.002 (UV-RuleId: 1, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V], UV-RFrozen: [V]) 0.002/0.002 (UV-RuleId: 2, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V], UV-RFrozen: [V]) 0.002/0.002 (UV-RuleId: 3, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 4, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2]) 0.002/0.002 (UV-RuleId: 5, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2]) 0.002/0.002 (UV-RuleId: 6, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2]) 0.002/0.002 (UV-RuleId: 7, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2]) 0.002/0.002 (UV-RuleId: 8, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V2], UV-RFrozen: [V2]) 0.002/0.002 (UV-RuleId: 9, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 10, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V], UV-RFrozen: [V]) 0.002/0.002 (UV-RuleId: 11, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V], UV-RFrozen: [V]) 0.002/0.002 (UV-RuleId: 12, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 13, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2]) 0.002/0.002 (UV-RuleId: 14, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2]) 0.002/0.002 (UV-RuleId: 15, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2]) 0.002/0.002 (UV-RuleId: 16, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2]) 0.002/0.002 (UV-RuleId: 17, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V2], UV-RFrozen: [V2]) 0.002/0.002 (UV-RuleId: 18, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 19, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2]) 0.002/0.002 (UV-RuleId: 20, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2]) 0.002/0.002 (UV-RuleId: 21, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2]) 0.002/0.002 (UV-RuleId: 22, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2]) 0.002/0.002 (UV-RuleId: 23, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V2], UV-RFrozen: [V2]) 0.002/0.002 (UV-RuleId: 24, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 25, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V], UV-RFrozen: [V]) 0.002/0.002 (UV-RuleId: 26, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V], UV-RFrozen: [V]) 0.002/0.002 (UV-RuleId: 27, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 28, UV-LActive: [], UV-RActive: [], UV-LFrozen: [I, P], UV-RFrozen: [I, P]) 0.002/0.002 (UV-RuleId: 29, UV-LActive: [], UV-RActive: [], UV-LFrozen: [P], UV-RFrozen: [P]) 0.002/0.002 (UV-RuleId: 30, UV-LActive: [], UV-RActive: [], UV-LFrozen: [P], UV-RFrozen: [P]) 0.002/0.002 (UV-RuleId: 31, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 32, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V], UV-RFrozen: [V]) 0.002/0.002 (UV-RuleId: 33, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V], UV-RFrozen: [V]) 0.002/0.002 (UV-RuleId: 34, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 35, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V2], UV-RFrozen: [V2]) 0.002/0.002 (UV-RuleId: 36, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 37, UV-LActive: [X, Y, Z], UV-RActive: [X, Y, Z], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 38, UV-LActive: [X], UV-RActive: [X], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 39, UV-LActive: [X], UV-RActive: [X], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 40, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2]) 0.002/0.002 (UV-RuleId: 41, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 42, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V], UV-RFrozen: [V]) 0.002/0.002 (UV-RuleId: 43, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2]) 0.002/0.002 (UV-RuleId: 44, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2]) 0.002/0.002 (UV-RuleId: 45, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V], UV-RFrozen: [V]) 0.002/0.002 (UV-RuleId: 46, UV-LActive: [], UV-RActive: [], UV-LFrozen: [I, P], UV-RFrozen: [I, P]) 0.002/0.002 (UV-RuleId: 47, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V], UV-RFrozen: [V]) 0.002/0.002 (UV-RuleId: 48, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 49, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V], UV-RFrozen: [V]) 0.002/0.002 (UV-RuleId: 50, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2]) 0.002/0.002 (UV-RuleId: 51, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 52, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 53, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 54, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 55, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 56, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 57, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 58, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 59, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 60, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 61, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 -> FVars: 0.002/0.002 x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26, x27, x28, x29, x30, x31, x32, x33, x34, x35, x36, x37, x38, x39, x40, x41, x42, x43, x44, x45, x46, x47, x48, x49, x50, x51, x52, x53, x54, x55, x56, x57, x58, x59, x60, x61, x62, x63, x64, x65, x66, x67 0.002/0.002 -> PVars: 0.002/0.002 V: [x9, x10, x20, x21, x40, x41, x46, x47, x56, x61, x64, x65], V1: [x11, x13, x15, x17, x22, x24, x26, x28, x31, x33, x35, x37, x54, x57, x59, x66], V2: [x12, x14, x16, x18, x19, x23, x25, x27, x29, x30, x32, x34, x36, x38, x39, x48, x55, x58, x60, x67], I: [x42, x62], P: [x43, x44, x45, x63], X: [x49, x52, x53], Y: [x50], Z: [x51] 0.002/0.002 0.002/0.002 -> Rlps: 0.002/0.002 (rule: U11(tt,x9:S) -> U12(isPalListKind(x9:S),x9:S), id: 1, possubterms: U11(tt,x9:S)->[], tt->[1]) 0.002/0.002 (rule: U12(tt,x10:S) -> U13(isNeList(x10:S)), id: 2, possubterms: U12(tt,x10:S)->[], tt->[1]) 0.002/0.002 (rule: U13(tt) -> tt, id: 3, possubterms: U13(tt)->[], tt->[1]) 0.002/0.002 (rule: U21(tt,x11:S,x12:S) -> U22(isPalListKind(x11:S),x11:S,x12:S), id: 4, possubterms: U21(tt,x11:S,x12:S)->[], tt->[1]) 0.002/0.002 (rule: U22(tt,x13:S,x14:S) -> U23(isPalListKind(x14:S),x13:S,x14:S), id: 5, possubterms: U22(tt,x13:S,x14:S)->[], tt->[1]) 0.002/0.002 (rule: U23(tt,x15:S,x16:S) -> U24(isPalListKind(x16:S),x15:S,x16:S), id: 6, possubterms: U23(tt,x15:S,x16:S)->[], tt->[1]) 0.002/0.002 (rule: U24(tt,x17:S,x18:S) -> U25(isList(x17:S),x18:S), id: 7, possubterms: U24(tt,x17:S,x18:S)->[], tt->[1]) 0.002/0.002 (rule: U25(tt,x19:S) -> U26(isList(x19:S)), id: 8, possubterms: U25(tt,x19:S)->[], tt->[1]) 0.002/0.002 (rule: U26(tt) -> tt, id: 9, possubterms: U26(tt)->[], tt->[1]) 0.002/0.002 (rule: U31(tt,x20:S) -> U32(isPalListKind(x20:S),x20:S), id: 10, possubterms: U31(tt,x20:S)->[], tt->[1]) 0.002/0.002 (rule: U32(tt,x21:S) -> U33(isQid(x21:S)), id: 11, possubterms: U32(tt,x21:S)->[], tt->[1]) 0.002/0.002 (rule: U33(tt) -> tt, id: 12, possubterms: U33(tt)->[], tt->[1]) 0.002/0.002 (rule: U41(tt,x22:S,x23:S) -> U42(isPalListKind(x22:S),x22:S,x23:S), id: 13, possubterms: U41(tt,x22:S,x23:S)->[], tt->[1]) 0.002/0.002 (rule: U42(tt,x24:S,x25:S) -> U43(isPalListKind(x25:S),x24:S,x25:S), id: 14, possubterms: U42(tt,x24:S,x25:S)->[], tt->[1]) 0.002/0.002 (rule: U43(tt,x26:S,x27:S) -> U44(isPalListKind(x27:S),x26:S,x27:S), id: 15, possubterms: U43(tt,x26:S,x27:S)->[], tt->[1]) 0.002/0.002 (rule: U44(tt,x28:S,x29:S) -> U45(isList(x28:S),x29:S), id: 16, possubterms: U44(tt,x28:S,x29:S)->[], tt->[1]) 0.002/0.002 (rule: U45(tt,x30:S) -> U46(isNeList(x30:S)), id: 17, possubterms: U45(tt,x30:S)->[], tt->[1]) 0.002/0.002 (rule: U46(tt) -> tt, id: 18, possubterms: U46(tt)->[], tt->[1]) 0.002/0.002 (rule: U51(tt,x31:S,x32:S) -> U52(isPalListKind(x31:S),x31:S,x32:S), id: 19, possubterms: U51(tt,x31:S,x32:S)->[], tt->[1]) 0.002/0.002 (rule: U52(tt,x33:S,x34:S) -> U53(isPalListKind(x34:S),x33:S,x34:S), id: 20, possubterms: U52(tt,x33:S,x34:S)->[], tt->[1]) 0.002/0.002 (rule: U53(tt,x35:S,x36:S) -> U54(isPalListKind(x36:S),x35:S,x36:S), id: 21, possubterms: U53(tt,x35:S,x36:S)->[], tt->[1]) 0.002/0.002 (rule: U54(tt,x37:S,x38:S) -> U55(isNeList(x37:S),x38:S), id: 22, possubterms: U54(tt,x37:S,x38:S)->[], tt->[1]) 0.002/0.002 (rule: U55(tt,x39:S) -> U56(isList(x39:S)), id: 23, possubterms: U55(tt,x39:S)->[], tt->[1]) 0.002/0.002 (rule: U56(tt) -> tt, id: 24, possubterms: U56(tt)->[], tt->[1]) 0.002/0.002 (rule: U61(tt,x40:S) -> U62(isPalListKind(x40:S),x40:S), id: 25, possubterms: U61(tt,x40:S)->[], tt->[1]) 0.002/0.002 (rule: U62(tt,x41:S) -> U63(isQid(x41:S)), id: 26, possubterms: U62(tt,x41:S)->[], tt->[1]) 0.002/0.002 (rule: U63(tt) -> tt, id: 27, possubterms: U63(tt)->[], tt->[1]) 0.002/0.002 (rule: U71(tt,x42:S,x43:S) -> U72(isPalListKind(x42:S),x43:S), id: 28, possubterms: U71(tt,x42:S,x43:S)->[], tt->[1]) 0.002/0.002 (rule: U72(tt,x44:S) -> U73(isPal(x44:S),x44:S), id: 29, possubterms: U72(tt,x44:S)->[], tt->[1]) 0.002/0.002 (rule: U73(tt,x45:S) -> U74(isPalListKind(x45:S)), id: 30, possubterms: U73(tt,x45:S)->[], tt->[1]) 0.002/0.002 (rule: U74(tt) -> tt, id: 31, possubterms: U74(tt)->[], tt->[1]) 0.002/0.002 (rule: U81(tt,x46:S) -> U82(isPalListKind(x46:S),x46:S), id: 32, possubterms: U81(tt,x46:S)->[], tt->[1]) 0.002/0.002 (rule: U82(tt,x47:S) -> U83(isNePal(x47:S)), id: 33, possubterms: U82(tt,x47:S)->[], tt->[1]) 0.002/0.002 (rule: U83(tt) -> tt, id: 34, possubterms: U83(tt)->[], tt->[1]) 0.002/0.002 (rule: U91(tt,x48:S) -> U92(isPalListKind(x48:S)), id: 35, possubterms: U91(tt,x48:S)->[], tt->[1]) 0.002/0.002 (rule: U92(tt) -> tt, id: 36, possubterms: U92(tt)->[], tt->[1]) 0.002/0.002 (rule: __(__(x49:S,x50:S),x51:S) -> __(x49:S,__(x50:S,x51:S)), id: 37, possubterms: __(__(x49:S,x50:S),x51:S)->[], __(x49:S,x50:S)->[1]) 0.002/0.002 (rule: __(nil,x52:S) -> x52:S, id: 38, possubterms: __(nil,x52:S)->[], nil->[1]) 0.002/0.002 (rule: __(x53:S,nil) -> x53:S, id: 39, possubterms: __(x53:S,nil)->[], nil->[2]) 0.002/0.002 (rule: isList(__(x54:S,x55:S)) -> U21(isPalListKind(x54:S),x54:S,x55:S), id: 40, possubterms: isList(__(x54:S,x55:S))->[]) 0.002/0.002 (rule: isList(nil) -> tt, id: 41, possubterms: isList(nil)->[]) 0.002/0.002 (rule: isList(x56:S) -> U11(isPalListKind(x56:S),x56:S), id: 42, possubterms: isList(x56:S)->[]) 0.002/0.002 (rule: isNeList(__(x57:S,x58:S)) -> U41(isPalListKind(x57:S),x57:S,x58:S), id: 43, possubterms: isNeList(__(x57:S,x58:S))->[]) 0.002/0.002 (rule: isNeList(__(x59:S,x60:S)) -> U51(isPalListKind(x59:S),x59:S,x60:S), id: 44, possubterms: isNeList(__(x59:S,x60:S))->[]) 0.002/0.002 (rule: isNeList(x61:S) -> U31(isPalListKind(x61:S),x61:S), id: 45, possubterms: isNeList(x61:S)->[]) 0.002/0.002 (rule: isNePal(__(x62:S,__(x63:S,x62:S))) -> U71(isQid(x62:S),x62:S,x63:S), id: 46, possubterms: isNePal(__(x62:S,__(x63:S,x62:S)))->[]) 0.002/0.002 (rule: isNePal(x64:S) -> U61(isPalListKind(x64:S),x64:S), id: 47, possubterms: isNePal(x64:S)->[]) 0.002/0.002 (rule: isPal(nil) -> tt, id: 48, possubterms: isPal(nil)->[]) 0.002/0.002 (rule: isPal(x65:S) -> U81(isPalListKind(x65:S),x65:S), id: 49, possubterms: isPal(x65:S)->[]) 0.002/0.002 (rule: isPalListKind(__(x66:S,x67:S)) -> U91(isPalListKind(x66:S),x67:S), id: 50, possubterms: isPalListKind(__(x66:S,x67:S))->[]) 0.002/0.002 (rule: isPalListKind(a) -> tt, id: 51, possubterms: isPalListKind(a)->[]) 0.002/0.002 (rule: isPalListKind(e) -> tt, id: 52, possubterms: isPalListKind(e)->[]) 0.002/0.002 (rule: isPalListKind(i) -> tt, id: 53, possubterms: isPalListKind(i)->[]) 0.002/0.002 (rule: isPalListKind(nil) -> tt, id: 54, possubterms: isPalListKind(nil)->[]) 0.002/0.002 (rule: isPalListKind(o) -> tt, id: 55, possubterms: isPalListKind(o)->[]) 0.002/0.002 (rule: isPalListKind(u) -> tt, id: 56, possubterms: isPalListKind(u)->[]) 0.002/0.002 (rule: isQid(a) -> tt, id: 57, possubterms: isQid(a)->[]) 0.002/0.002 (rule: isQid(e) -> tt, id: 58, possubterms: isQid(e)->[]) 0.002/0.002 (rule: isQid(i) -> tt, id: 59, possubterms: isQid(i)->[]) 0.002/0.002 (rule: isQid(o) -> tt, id: 60, possubterms: isQid(o)->[]) 0.002/0.002 (rule: isQid(u) -> tt, id: 61, possubterms: isQid(u)->[]) 0.002/0.002 0.002/0.002 -> Unifications: 0.002/0.002 (R37 unifies with R37 at p: [1], l: __(__(x49:S,x50:S),x51:S), lp: __(x49:S,x50:S), sig: {x49:S -> __(X:S,Y:S),x50:S -> Z:S}, l': __(__(X:S,Y:S),Z:S), r: __(x49:S,__(x50:S,x51:S)), r': __(X:S,__(Y:S,Z:S))) 0.002/0.002 (R37 unifies with R38 at p: [1], l: __(__(x49:S,x50:S),x51:S), lp: __(x49:S,x50:S), sig: {x49:S -> nil,x50:S -> X:S}, l': __(nil,X:S), r: __(x49:S,__(x50:S,x51:S)), r': X:S) 0.002/0.002 (R37 unifies with R39 at p: [1], l: __(__(x49:S,x50:S),x51:S), lp: __(x49:S,x50:S), sig: {x49:S -> X:S,x50:S -> nil}, l': __(X:S,nil), r: __(x49:S,__(x50:S,x51:S)), r': X:S) 0.002/0.002 (R39 unifies with R37 at p: [], l: __(x53:S,nil), lp: __(x53:S,nil), sig: {Z:S -> nil,x53:S -> __(X:S,Y:S)}, l': __(__(X:S,Y:S),Z:S), r: x53:S, r': __(X:S,__(Y:S,Z:S))) 0.002/0.002 (R39 unifies with R38 at p: [], l: __(x53:S,nil), lp: __(x53:S,nil), sig: {X:S -> nil,x53:S -> nil}, l': __(nil,X:S), r: x53:S, r': X:S) 0.002/0.002 (R42 unifies with R40 at p: [], l: isList(x56:S), lp: isList(x56:S), sig: {x56:S -> __(V1:S,V2:S)}, l': isList(__(V1:S,V2:S)), r: U11(isPalListKind(x56:S),x56:S), r': U21(isPalListKind(V1:S),V1:S,V2:S)) 0.002/0.002 (R42 unifies with R41 at p: [], l: isList(x56:S), lp: isList(x56:S), sig: {x56:S -> nil}, l': isList(nil), r: U11(isPalListKind(x56:S),x56:S), r': tt) 0.002/0.002 (R44 unifies with R43 at p: [], l: isNeList(__(x59:S,x60:S)), lp: isNeList(__(x59:S,x60:S)), sig: {x59:S -> V1:S,x60:S -> V2:S}, l': isNeList(__(V1:S,V2:S)), r: U51(isPalListKind(x59:S),x59:S,x60:S), r': U41(isPalListKind(V1:S),V1:S,V2:S)) 0.002/0.002 (R45 unifies with R43 at p: [], l: isNeList(x61:S), lp: isNeList(x61:S), sig: {x61:S -> __(V1:S,V2:S)}, l': isNeList(__(V1:S,V2:S)), r: U31(isPalListKind(x61:S),x61:S), r': U41(isPalListKind(V1:S),V1:S,V2:S)) 0.002/0.002 (R45 unifies with R44 at p: [], l: isNeList(x61:S), lp: isNeList(x61:S), sig: {x61:S -> __(V1:S,V2:S)}, l': isNeList(__(V1:S,V2:S)), r: U31(isPalListKind(x61:S),x61:S), r': U51(isPalListKind(V1:S),V1:S,V2:S)) 0.002/0.002 (R47 unifies with R46 at p: [], l: isNePal(x64:S), lp: isNePal(x64:S), sig: {x64:S -> __(I:S,__(P:S,I:S))}, l': isNePal(__(I:S,__(P:S,I:S))), r: U61(isPalListKind(x64:S),x64:S), r': U71(isQid(I:S),I:S,P:S)) 0.002/0.002 (R49 unifies with R48 at p: [], l: isPal(x65:S), lp: isPal(x65:S), sig: {x65:S -> nil}, l': isPal(nil), r: U81(isPalListKind(x65:S),x65:S), r': tt) 0.002/0.002 0.002/0.002 -> Critical pairs info: 0.002/0.002 => Not trivial, Overlay, NW0, N1 0.002/0.002 <__(X:S,Z:S),__(nil,__(X:S,Z:S))> => Not trivial, Not overlay, NW0, N2 0.002/0.002 => Trivial, Overlay, NW0, N3 0.002/0.002 => Not trivial, Overlay, NW0, N4 0.002/0.002 <__(X:S,Z:S),__(X:S,__(nil,Z:S))> => Not trivial, Not overlay, NW0, N5 0.002/0.002 => Not trivial, Overlay, NW0, N6 0.002/0.002 <__(__(X:S,__(Y:S,Z:S)),Z:S),__(__(X:S,Y:S),__(Z:S,Z:S))> => Not trivial, Not overlay, NW0, N7 0.002/0.002 <__(X:S,__(Y:S,nil)),__(X:S,Y:S)> => Not trivial, Overlay, NW0, N8 0.002/0.002 => Not trivial, Overlay, NW0, N9 0.002/0.002 => Not trivial, Overlay, NW0, N10 0.002/0.002 => Not trivial, Overlay, NW0, N11 0.002/0.002 => Not trivial, Overlay, NW0, N12 0.002/0.002 0.002/0.002 -> Problem conclusions: 0.002/0.002 Not left linear, Not right linear, Not linear 0.002/0.002 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 0.002/0.002 Not Huet-Levy confluent, Not Newman confluent 0.002/0.002 R is a CS-TRS, Left-homogeneous u-replacing variables 0.002/0.002 0.002/0.002 0.002/0.002 Problem 1: 0.002/0.002 No Convergence Brute Force Processor: 0.002/0.002 -> Rewritings: 0.002/0.002 s: U71(isQid(I:S),I:S,P:S) 0.002/0.002 Nodes: [0] 0.002/0.002 Edges: [] 0.002/0.002 ID: 0 => ('U71(isQid(I:S),I:S,P:S)', D0) 0.002/0.002 t: U61(isPalListKind(__(I:S,__(P:S,I:S))),__(I:S,__(P:S,I:S))) 0.002/0.002 Nodes: [0,1] 0.002/0.002 Edges: [(0,1)] 0.002/0.002 ID: 0 => ('U61(isPalListKind(__(I:S,__(P:S,I:S))),__(I:S,__(P:S,I:S)))', D0) 0.002/0.002 ID: 1 => ('U61(U91(isPalListKind(I:S),__(P:S,I:S)),__(I:S,__(P:S,I:S)))', D1, R50, P[1], S{x66:S -> I:S, x67:S -> __(P:S,I:S)}), NR: 'U91(isPalListKind(I:S),__(P:S,I:S))' 0.002/0.002 U71(isQid(I:S),I:S,P:S) ->* no union *<- U61(isPalListKind(__(I:S,__(P:S,I:S))),__(I:S,__(P:S,I:S))) 0.002/0.002 "Not joinable" 0.002/0.002 0.002/0.002 The problem is not joinable. 0.002/0.002 0.00user 0.01system 0:00.02elapsed 86%CPU (0avgtext+0avgdata 12092maxresident)k 0.002/0.002 0inputs+0outputs (0major+1206minor)pagefaults 0swaps