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