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 (U21 1) 0.003/0.003 (U22 1) 0.003/0.003 (U23 1) 0.003/0.003 (U31 1) 0.003/0.003 (U32 1) 0.003/0.003 (U41 1) 0.003/0.003 (U42 1) 0.003/0.003 (U43 1) 0.003/0.003 (U51 1) 0.003/0.003 (U52 1) 0.003/0.003 (U53 1) 0.003/0.003 (U61 1) 0.003/0.003 (U62 1) 0.003/0.003 (U71 1) 0.003/0.003 (U72 1) 0.003/0.003 (__ 1 2) 0.003/0.003 (and 1) 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(isNeList(V:S:S)) 0.003/0.003 U12(tt) -> tt 0.003/0.003 U21(tt,V1:S:S,V2:S:S) -> U22(isList(V1:S:S),V2:S:S) 0.003/0.003 U22(tt,V2:S:S) -> U23(isList(V2:S:S)) 0.003/0.003 U23(tt) -> tt 0.003/0.003 U31(tt,V:S:S) -> U32(isQid(V:S:S)) 0.003/0.003 U32(tt) -> tt 0.003/0.003 U41(tt,V1:S:S,V2:S:S) -> U42(isList(V1:S:S),V2:S:S) 0.003/0.003 U42(tt,V2:S:S) -> U43(isNeList(V2:S:S)) 0.003/0.003 U43(tt) -> tt 0.003/0.003 U51(tt,V1:S:S,V2:S:S) -> U52(isNeList(V1:S:S),V2:S:S) 0.003/0.003 U52(tt,V2:S:S) -> U53(isList(V2:S:S)) 0.003/0.003 U53(tt) -> tt 0.003/0.003 U61(tt,V:S:S) -> U62(isQid(V:S:S)) 0.003/0.003 U62(tt) -> tt 0.003/0.003 U71(tt,V:S:S) -> U72(isNePal(V:S:S)) 0.003/0.003 U72(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 and(tt,X:S:S) -> X:S:S 0.003/0.003 isList(__(V1:S:S,V2:S:S)) -> U21(and(isPalListKind(V1:S:S),isPalListKind(V2: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(and(isPalListKind(V1:S:S),isPalListKind(V2:S:S)),V1:S:S,V2:S:S) 0.003/0.003 isNeList(__(V1:S:S,V2:S:S)) -> U51(and(isPalListKind(V1:S:S),isPalListKind(V2: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))) -> and(and(isQid(I:S:S),isPalListKind(I:S:S)),and(isPal(P:S:S),isPalListKind(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) -> U71(isPalListKind(V:S:S),V:S:S) 0.003/0.003 isPalListKind(__(V1:S:S,V2:S:S)) -> and(isPalListKind(V1:S:S),isPalListKind(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 (U21 1) 0.003/0.003 (U22 1) 0.003/0.003 (U23 1) 0.003/0.003 (U31 1) 0.003/0.003 (U32 1) 0.003/0.003 (U41 1) 0.003/0.003 (U42 1) 0.003/0.003 (U43 1) 0.003/0.003 (U51 1) 0.003/0.003 (U52 1) 0.003/0.003 (U53 1) 0.003/0.003 (U61 1) 0.003/0.003 (U62 1) 0.003/0.003 (U71 1) 0.003/0.003 (U72 1) 0.003/0.003 (__ 1 2) 0.003/0.003 (and 1) 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(isNeList(V:S:S)) 0.003/0.003 U12(tt) -> tt 0.003/0.003 U21(tt,V1:S:S,V2:S:S) -> U22(isList(V1:S:S),V2:S:S) 0.003/0.003 U22(tt,V2:S:S) -> U23(isList(V2:S:S)) 0.003/0.003 U23(tt) -> tt 0.003/0.003 U31(tt,V:S:S) -> U32(isQid(V:S:S)) 0.003/0.003 U32(tt) -> tt 0.003/0.003 U41(tt,V1:S:S,V2:S:S) -> U42(isList(V1:S:S),V2:S:S) 0.003/0.003 U42(tt,V2:S:S) -> U43(isNeList(V2:S:S)) 0.003/0.003 U43(tt) -> tt 0.003/0.003 U51(tt,V1:S:S,V2:S:S) -> U52(isNeList(V1:S:S),V2:S:S) 0.003/0.003 U52(tt,V2:S:S) -> U53(isList(V2:S:S)) 0.003/0.003 U53(tt) -> tt 0.003/0.003 U61(tt,V:S:S) -> U62(isQid(V:S:S)) 0.003/0.003 U62(tt) -> tt 0.003/0.003 U71(tt,V:S:S) -> U72(isNePal(V:S:S)) 0.003/0.003 U72(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 and(tt,X:S:S) -> X:S:S 0.003/0.003 isList(__(V1:S:S,V2:S:S)) -> U21(and(isPalListKind(V1:S:S),isPalListKind(V2: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(and(isPalListKind(V1:S:S),isPalListKind(V2:S:S)),V1:S:S,V2:S:S) 0.003/0.003 isNeList(__(V1:S:S,V2:S:S)) -> U51(and(isPalListKind(V1:S:S),isPalListKind(V2: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))) -> and(and(isQid(I:S:S),isPalListKind(I:S:S)),and(isPal(P:S:S),isPalListKind(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) -> U71(isPalListKind(V:S:S),V:S:S) 0.003/0.003 isPalListKind(__(V1:S:S,V2:S:S)) -> and(isPalListKind(V1:S:S),isPalListKind(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 (U21 1) 0.003/0.003 (U22 1) 0.003/0.003 (U23 1) 0.003/0.003 (U31 1) 0.003/0.003 (U32 1) 0.003/0.003 (U41 1) 0.003/0.003 (U42 1) 0.003/0.003 (U43 1) 0.003/0.003 (U51 1) 0.003/0.003 (U52 1) 0.003/0.003 (U53 1) 0.003/0.003 (U61 1) 0.003/0.003 (U62 1) 0.003/0.003 (U71 1) 0.003/0.003 (U72 1) 0.003/0.003 (__ 1 2) 0.003/0.003 (and 1) 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(isNeList(V:S:S)) 0.003/0.003 U12(tt) -> tt 0.003/0.003 U21(tt,V1:S:S,V2:S:S) -> U22(isList(V1:S:S),V2:S:S) 0.003/0.003 U22(tt,V2:S:S) -> U23(isList(V2:S:S)) 0.003/0.003 U23(tt) -> tt 0.003/0.003 U31(tt,V:S:S) -> U32(isQid(V:S:S)) 0.003/0.003 U32(tt) -> tt 0.003/0.003 U41(tt,V1:S:S,V2:S:S) -> U42(isList(V1:S:S),V2:S:S) 0.003/0.003 U42(tt,V2:S:S) -> U43(isNeList(V2:S:S)) 0.003/0.003 U43(tt) -> tt 0.003/0.003 U51(tt,V1:S:S,V2:S:S) -> U52(isNeList(V1:S:S),V2:S:S) 0.003/0.003 U52(tt,V2:S:S) -> U53(isList(V2:S:S)) 0.003/0.003 U53(tt) -> tt 0.003/0.003 U61(tt,V:S:S) -> U62(isQid(V:S:S)) 0.003/0.003 U62(tt) -> tt 0.003/0.003 U71(tt,V:S:S) -> U72(isNePal(V:S:S)) 0.003/0.003 U72(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 and(tt,X:S:S) -> X:S:S 0.003/0.003 isList(__(V1:S:S,V2:S:S)) -> U21(and(isPalListKind(V1:S:S),isPalListKind(V2: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(and(isPalListKind(V1:S:S),isPalListKind(V2:S:S)),V1:S:S,V2:S:S) 0.003/0.003 isNeList(__(V1:S:S,V2:S:S)) -> U51(and(isPalListKind(V1:S:S),isPalListKind(V2: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))) -> and(and(isQid(I:S:S),isPalListKind(I:S:S)),and(isPal(P:S:S),isPalListKind(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) -> U71(isPalListKind(V:S:S),V:S:S) 0.003/0.003 isPalListKind(__(V1:S:S,V2:S:S)) -> and(isPalListKind(V1:S:S),isPalListKind(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(isNeList(V:S:S)) 0.003/0.003 U12(tt) -> tt 0.003/0.003 U21(tt,V1:S:S,V2:S:S) -> U22(isList(V1:S:S),V2:S:S) 0.003/0.003 U22(tt,V2:S:S) -> U23(isList(V2:S:S)) 0.003/0.003 U23(tt) -> tt 0.003/0.003 U31(tt,V:S:S) -> U32(isQid(V:S:S)) 0.003/0.003 U32(tt) -> tt 0.003/0.003 U41(tt,V1:S:S,V2:S:S) -> U42(isList(V1:S:S),V2:S:S) 0.003/0.003 U42(tt,V2:S:S) -> U43(isNeList(V2:S:S)) 0.003/0.003 U43(tt) -> tt 0.003/0.003 U51(tt,V1:S:S,V2:S:S) -> U52(isNeList(V1:S:S),V2:S:S) 0.003/0.003 U52(tt,V2:S:S) -> U53(isList(V2:S:S)) 0.003/0.003 U53(tt) -> tt 0.003/0.003 U61(tt,V:S:S) -> U62(isQid(V:S:S)) 0.003/0.003 U62(tt) -> tt 0.003/0.003 U71(tt,V:S:S) -> U72(isNePal(V:S:S)) 0.003/0.003 U72(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 and(tt,X:S:S) -> X:S:S 0.003/0.003 isList(__(V1:S:S,V2:S:S)) -> U21(and(isPalListKind(V1:S:S),isPalListKind(V2: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(and(isPalListKind(V1:S:S),isPalListKind(V2:S:S)),V1:S:S,V2:S:S) 0.003/0.003 isNeList(__(V1:S:S,V2:S:S)) -> U51(and(isPalListKind(V1:S:S),isPalListKind(V2: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))) -> and(and(isQid(I:S:S),isPalListKind(I:S:S)),and(isPal(P:S:S),isPalListKind(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) -> U71(isPalListKind(V:S:S),V:S:S) 0.003/0.003 isPalListKind(__(V1:S:S,V2:S:S)) -> and(isPalListKind(V1:S:S),isPalListKind(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, V1:S, V2:S, V2:S, V:S, V1:S, V2:S, V2:S, V1:S, V2:S, V2:S, V:S, V:S, X:S, Y:S, Z:S, X: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: []) 0.003/0.003 (UV-RuleId: 2, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 3, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V2:S]) 0.003/0.003 (UV-RuleId: 4, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V2:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 5, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 6, UV-LActive: [], UV-RActive: [V:S], UV-LFrozen: [V:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 7, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 8, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V2:S]) 0.003/0.003 (UV-RuleId: 9, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V2:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 10, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 11, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V2:S]) 0.003/0.003 (UV-RuleId: 12, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V2:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 13, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 14, UV-LActive: [], UV-RActive: [V:S], UV-LFrozen: [V:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 15, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 16, UV-LActive: [], UV-RActive: [V:S], UV-LFrozen: [V:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 17, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 18, 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: 19, UV-LActive: [X:S], UV-RActive: [X:S], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 20, UV-LActive: [X:S], UV-RActive: [X:S], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 21, UV-LActive: [], UV-RActive: [X:S], UV-LFrozen: [X:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 22, UV-LActive: [V1:S, V2:S], UV-RActive: [V1:S], UV-LFrozen: [], UV-RFrozen: [V1:S, V2:S]) 0.003/0.003 (UV-RuleId: 23, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 24, UV-LActive: [V:S], UV-RActive: [V:S], UV-LFrozen: [], UV-RFrozen: [V:S]) 0.003/0.003 (UV-RuleId: 25, UV-LActive: [V1:S, V2:S], UV-RActive: [V1:S], UV-LFrozen: [], UV-RFrozen: [V1:S, V2:S]) 0.003/0.003 (UV-RuleId: 26, UV-LActive: [V1:S, V2:S], UV-RActive: [V1:S], UV-LFrozen: [], UV-RFrozen: [V1:S, V2:S]) 0.003/0.003 (UV-RuleId: 27, UV-LActive: [V:S], UV-RActive: [V:S], UV-LFrozen: [], UV-RFrozen: [V:S]) 0.003/0.003 (UV-RuleId: 28, UV-LActive: [I:S, P:S], UV-RActive: [I:S], UV-LFrozen: [], UV-RFrozen: [I:S, P:S]) 0.003/0.003 (UV-RuleId: 29, UV-LActive: [V:S], UV-RActive: [V:S], UV-LFrozen: [], UV-RFrozen: [V:S]) 0.003/0.003 (UV-RuleId: 30, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 31, UV-LActive: [V:S], UV-RActive: [V:S], UV-LFrozen: [], UV-RFrozen: [V:S]) 0.003/0.003 (UV-RuleId: 32, UV-LActive: [V1:S, V2:S], UV-RActive: [V1:S], UV-LFrozen: [], UV-RFrozen: [V2:S]) 0.003/0.003 (UV-RuleId: 33, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], 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: [], UV-LFrozen: [], 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: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 38, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 39, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 40, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 41, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 42, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 43, 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 0.003/0.003 -> PVars: 0.003/0.003 V:S: [x10, x14, x21, x22, x31, x36, x39, x40], V1:S: [x11, x15, x18, x29, x32, x34, x41], V2:S: [x12, x13, x16, x17, x19, x20, x30, x33, x35, x42], X:S: [x23, x26, x27, x28], Y:S: [x24], Z:S: [x25], I:S: [x37], P:S: [x38] 0.003/0.003 0.003/0.003 -> Rlps: 0.003/0.003 (rule: U11(tt,x10:S) -> U12(isNeList(x10:S)), id: 1, possubterms: U11(tt,x10:S)->[], tt->[1]) 0.003/0.003 (rule: U12(tt) -> tt, id: 2, possubterms: U12(tt)->[], tt->[1]) 0.003/0.003 (rule: U21(tt,x11:S,x12:S) -> U22(isList(x11:S),x12:S), id: 3, possubterms: U21(tt,x11:S,x12:S)->[], tt->[1]) 0.003/0.003 (rule: U22(tt,x13:S) -> U23(isList(x13:S)), id: 4, possubterms: U22(tt,x13:S)->[], tt->[1]) 0.003/0.003 (rule: U23(tt) -> tt, id: 5, possubterms: U23(tt)->[], tt->[1]) 0.003/0.003 (rule: U31(tt,x14:S) -> U32(isQid(x14:S)), id: 6, possubterms: U31(tt,x14:S)->[], tt->[1]) 0.003/0.003 (rule: U32(tt) -> tt, id: 7, possubterms: U32(tt)->[], tt->[1]) 0.003/0.003 (rule: U41(tt,x15:S,x16:S) -> U42(isList(x15:S),x16:S), id: 8, possubterms: U41(tt,x15:S,x16:S)->[], tt->[1]) 0.003/0.003 (rule: U42(tt,x17:S) -> U43(isNeList(x17:S)), id: 9, possubterms: U42(tt,x17:S)->[], tt->[1]) 0.003/0.003 (rule: U43(tt) -> tt, id: 10, possubterms: U43(tt)->[], tt->[1]) 0.003/0.003 (rule: U51(tt,x18:S,x19:S) -> U52(isNeList(x18:S),x19:S), id: 11, possubterms: U51(tt,x18:S,x19:S)->[], tt->[1]) 0.003/0.003 (rule: U52(tt,x20:S) -> U53(isList(x20:S)), id: 12, possubterms: U52(tt,x20:S)->[], tt->[1]) 0.003/0.003 (rule: U53(tt) -> tt, id: 13, possubterms: U53(tt)->[], tt->[1]) 0.003/0.003 (rule: U61(tt,x21:S) -> U62(isQid(x21:S)), id: 14, possubterms: U61(tt,x21:S)->[], tt->[1]) 0.003/0.003 (rule: U62(tt) -> tt, id: 15, possubterms: U62(tt)->[], tt->[1]) 0.003/0.003 (rule: U71(tt,x22:S) -> U72(isNePal(x22:S)), id: 16, possubterms: U71(tt,x22:S)->[], tt->[1]) 0.003/0.003 (rule: U72(tt) -> tt, id: 17, possubterms: U72(tt)->[], tt->[1]) 0.003/0.003 (rule: __(__(x23:S,x24:S),x25:S) -> __(x23:S,__(x24:S,x25:S)), id: 18, possubterms: __(__(x23:S,x24:S),x25:S)->[], __(x23:S,x24:S)->[1]) 0.003/0.003 (rule: __(nil,x26:S) -> x26:S, id: 19, possubterms: __(nil,x26:S)->[], nil->[1]) 0.003/0.003 (rule: __(x27:S,nil) -> x27:S, id: 20, possubterms: __(x27:S,nil)->[], nil->[2]) 0.003/0.003 (rule: and(tt,x28:S) -> x28:S, id: 21, possubterms: and(tt,x28:S)->[], tt->[1]) 0.003/0.003 (rule: isList(__(x29:S,x30:S)) -> U21(and(isPalListKind(x29:S),isPalListKind(x30:S)),x29:S,x30:S), id: 22, possubterms: isList(__(x29:S,x30:S))->[], __(x29:S,x30:S)->[1]) 0.003/0.003 (rule: isList(nil) -> tt, id: 23, possubterms: isList(nil)->[], nil->[1]) 0.003/0.003 (rule: isList(x31:S) -> U11(isPalListKind(x31:S),x31:S), id: 24, possubterms: isList(x31:S)->[]) 0.003/0.003 (rule: isNeList(__(x32:S,x33:S)) -> U41(and(isPalListKind(x32:S),isPalListKind(x33:S)),x32:S,x33:S), id: 25, possubterms: isNeList(__(x32:S,x33:S))->[], __(x32:S,x33:S)->[1]) 0.003/0.003 (rule: isNeList(__(x34:S,x35:S)) -> U51(and(isPalListKind(x34:S),isPalListKind(x35:S)),x34:S,x35:S), id: 26, possubterms: isNeList(__(x34:S,x35:S))->[], __(x34:S,x35:S)->[1]) 0.003/0.003 (rule: isNeList(x36:S) -> U31(isPalListKind(x36:S),x36:S), id: 27, possubterms: isNeList(x36:S)->[]) 0.003/0.003 (rule: isNePal(__(x37:S,__(x38:S,x37:S))) -> and(and(isQid(x37:S),isPalListKind(x37:S)),and(isPal(x38:S),isPalListKind(x38:S))), id: 28, possubterms: isNePal(__(x37:S,__(x38:S,x37:S)))->[], __(x37:S,__(x38:S,x37:S))->[1], __(x38:S,x37:S)->[1, 2]) 0.003/0.003 (rule: isNePal(x39:S) -> U61(isPalListKind(x39:S),x39:S), id: 29, possubterms: isNePal(x39:S)->[]) 0.003/0.003 (rule: isPal(nil) -> tt, id: 30, possubterms: isPal(nil)->[], nil->[1]) 0.003/0.003 (rule: isPal(x40:S) -> U71(isPalListKind(x40:S),x40:S), id: 31, possubterms: isPal(x40:S)->[]) 0.003/0.003 (rule: isPalListKind(__(x41:S,x42:S)) -> and(isPalListKind(x41:S),isPalListKind(x42:S)), id: 32, possubterms: isPalListKind(__(x41:S,x42:S))->[], __(x41:S,x42:S)->[1]) 0.003/0.003 (rule: isPalListKind(a) -> tt, id: 33, possubterms: isPalListKind(a)->[], a->[1]) 0.003/0.003 (rule: isPalListKind(e) -> tt, id: 34, possubterms: isPalListKind(e)->[], e->[1]) 0.003/0.003 (rule: isPalListKind(i) -> tt, id: 35, possubterms: isPalListKind(i)->[], i->[1]) 0.003/0.003 (rule: isPalListKind(nil) -> tt, id: 36, possubterms: isPalListKind(nil)->[], nil->[1]) 0.003/0.003 (rule: isPalListKind(o) -> tt, id: 37, possubterms: isPalListKind(o)->[], o->[1]) 0.003/0.003 (rule: isPalListKind(u) -> tt, id: 38, possubterms: isPalListKind(u)->[], u->[1]) 0.003/0.003 (rule: isQid(a) -> tt, id: 39, possubterms: isQid(a)->[], a->[1]) 0.003/0.003 (rule: isQid(e) -> tt, id: 40, possubterms: isQid(e)->[], e->[1]) 0.003/0.003 (rule: isQid(i) -> tt, id: 41, possubterms: isQid(i)->[], i->[1]) 0.003/0.003 (rule: isQid(o) -> tt, id: 42, possubterms: isQid(o)->[], o->[1]) 0.003/0.003 (rule: isQid(u) -> tt, id: 43, possubterms: isQid(u)->[], u->[1]) 0.003/0.003 0.003/0.003 -> Unifications: 0.003/0.003 (R18 unifies with R18 at p: [1], l: __(__(x23:S,x24:S),x25:S), lp: __(x23:S,x24:S), sig: {x23:S -> __(X:S:S,Y:S:S),x24:S -> Z:S:S}, l': __(__(X:S:S,Y:S:S),Z:S:S), r: __(x23:S,__(x24:S,x25:S)), r': __(X:S:S,__(Y:S:S,Z:S:S))) 0.003/0.003 (R18 unifies with R19 at p: [1], l: __(__(x23:S,x24:S),x25:S), lp: __(x23:S,x24:S), sig: {x23:S -> nil,x24:S -> X:S:S}, l': __(nil,X:S:S), r: __(x23:S,__(x24:S,x25:S)), r': X:S:S) 0.003/0.003 (R18 unifies with R20 at p: [1], l: __(__(x23:S,x24:S),x25:S), lp: __(x23:S,x24:S), sig: {x23:S -> X:S:S,x24:S -> nil}, l': __(X:S:S,nil), r: __(x23:S,__(x24:S,x25:S)), r': X:S:S) 0.003/0.003 (R20 unifies with R18 at p: [], l: __(x27:S,nil), lp: __(x27:S,nil), sig: {Z:S:S -> nil,x27:S -> __(X:S:S,Y:S:S)}, l': __(__(X:S:S,Y:S:S),Z:S:S), r: x27:S, r': __(X:S:S,__(Y:S:S,Z:S:S))) 0.003/0.003 (R20 unifies with R19 at p: [], l: __(x27:S,nil), lp: __(x27:S,nil), sig: {X:S:S -> nil,x27:S -> nil}, l': __(nil,X:S:S), r: x27:S, r': X:S:S) 0.003/0.003 (R22 unifies with R18 at p: [1], l: isList(__(x29:S,x30:S)), lp: __(x29:S,x30:S), sig: {x29:S -> __(X:S:S,Y:S:S),x30:S -> Z:S:S}, l': __(__(X:S:S,Y:S:S),Z:S:S), r: U21(and(isPalListKind(x29:S),isPalListKind(x30:S)),x29:S,x30:S), r': __(X:S:S,__(Y:S:S,Z:S:S))) 0.003/0.003 (R22 unifies with R19 at p: [1], l: isList(__(x29:S,x30:S)), lp: __(x29:S,x30:S), sig: {x29:S -> nil,x30:S -> X:S:S}, l': __(nil,X:S:S), r: U21(and(isPalListKind(x29:S),isPalListKind(x30:S)),x29:S,x30:S), r': X:S:S) 0.003/0.003 (R22 unifies with R20 at p: [1], l: isList(__(x29:S,x30:S)), lp: __(x29:S,x30:S), sig: {x29:S -> X:S:S,x30:S -> nil}, l': __(X:S:S,nil), r: U21(and(isPalListKind(x29:S),isPalListKind(x30:S)),x29:S,x30:S), r': X:S:S) 0.003/0.003 (R24 unifies with R22 at p: [], l: isList(x31:S), lp: isList(x31:S), sig: {x31:S -> __(V1:S:S,V2:S:S)}, l': isList(__(V1:S:S,V2:S:S)), r: U11(isPalListKind(x31:S),x31:S), r': U21(and(isPalListKind(V1:S:S),isPalListKind(V2:S:S)),V1:S:S,V2:S:S)) 0.003/0.003 (R24 unifies with R23 at p: [], l: isList(x31:S), lp: isList(x31:S), sig: {x31:S -> nil}, l': isList(nil), r: U11(isPalListKind(x31:S),x31:S), r': tt) 0.003/0.003 (R25 unifies with R18 at p: [1], l: isNeList(__(x32:S,x33:S)), lp: __(x32:S,x33:S), sig: {x32:S -> __(X:S:S,Y:S:S),x33:S -> Z:S:S}, l': __(__(X:S:S,Y:S:S),Z:S:S), r: U41(and(isPalListKind(x32:S),isPalListKind(x33:S)),x32:S,x33:S), r': __(X:S:S,__(Y:S:S,Z:S:S))) 0.003/0.003 (R25 unifies with R19 at p: [1], l: isNeList(__(x32:S,x33:S)), lp: __(x32:S,x33:S), sig: {x32:S -> nil,x33:S -> X:S:S}, l': __(nil,X:S:S), r: U41(and(isPalListKind(x32:S),isPalListKind(x33:S)),x32:S,x33:S), r': X:S:S) 0.003/0.003 (R25 unifies with R20 at p: [1], l: isNeList(__(x32:S,x33:S)), lp: __(x32:S,x33:S), sig: {x32:S -> X:S:S,x33:S -> nil}, l': __(X:S:S,nil), r: U41(and(isPalListKind(x32:S),isPalListKind(x33:S)),x32:S,x33:S), r': X:S:S) 0.003/0.003 (R26 unifies with R25 at p: [], l: isNeList(__(x34:S,x35:S)), lp: isNeList(__(x34:S,x35:S)), sig: {x34:S -> V1:S:S,x35:S -> V2:S:S}, l': isNeList(__(V1:S:S,V2:S:S)), r: U51(and(isPalListKind(x34:S),isPalListKind(x35:S)),x34:S,x35:S), r': U41(and(isPalListKind(V1:S:S),isPalListKind(V2:S:S)),V1:S:S,V2:S:S)) 0.003/0.003 (R26 unifies with R18 at p: [1], l: isNeList(__(x34:S,x35:S)), lp: __(x34:S,x35:S), sig: {x34:S -> __(X:S:S,Y:S:S),x35:S -> Z:S:S}, l': __(__(X:S:S,Y:S:S),Z:S:S), r: U51(and(isPalListKind(x34:S),isPalListKind(x35:S)),x34:S,x35:S), r': __(X:S:S,__(Y:S:S,Z:S:S))) 0.003/0.003 (R26 unifies with R19 at p: [1], l: isNeList(__(x34:S,x35:S)), lp: __(x34:S,x35:S), sig: {x34:S -> nil,x35:S -> X:S:S}, l': __(nil,X:S:S), r: U51(and(isPalListKind(x34:S),isPalListKind(x35:S)),x34:S,x35:S), r': X:S:S) 0.003/0.003 (R26 unifies with R20 at p: [1], l: isNeList(__(x34:S,x35:S)), lp: __(x34:S,x35:S), sig: {x34:S -> X:S:S,x35:S -> nil}, l': __(X:S:S,nil), r: U51(and(isPalListKind(x34:S),isPalListKind(x35:S)),x34:S,x35:S), r': X:S:S) 0.003/0.003 (R27 unifies with R25 at p: [], l: isNeList(x36:S), lp: isNeList(x36:S), sig: {x36:S -> __(V1:S:S,V2:S:S)}, l': isNeList(__(V1:S:S,V2:S:S)), r: U31(isPalListKind(x36:S),x36:S), r': U41(and(isPalListKind(V1:S:S),isPalListKind(V2:S:S)),V1:S:S,V2:S:S)) 0.003/0.003 (R27 unifies with R26 at p: [], l: isNeList(x36:S), lp: isNeList(x36:S), sig: {x36:S -> __(V1:S:S,V2:S:S)}, l': isNeList(__(V1:S:S,V2:S:S)), r: U31(isPalListKind(x36:S),x36:S), r': U51(and(isPalListKind(V1:S:S),isPalListKind(V2:S:S)),V1:S:S,V2:S:S)) 0.003/0.003 (R28 unifies with R18 at p: [1], l: isNePal(__(x37:S,__(x38:S,x37:S))), lp: __(x37:S,__(x38:S,x37:S)), sig: {Z:S:S -> __(x38:S,__(X:S:S,Y:S:S)),x37:S -> __(X:S:S,Y:S:S)}, l': __(__(X:S:S,Y:S:S),Z:S:S), r: and(and(isQid(x37:S),isPalListKind(x37:S)),and(isPal(x38:S),isPalListKind(x38:S))), r': __(X:S:S,__(Y:S:S,Z:S:S))) 0.003/0.003 (R28 unifies with R19 at p: [1], l: isNePal(__(x37:S,__(x38:S,x37:S))), lp: __(x37:S,__(x38:S,x37:S)), sig: {X:S:S -> __(x38:S,nil),x37:S -> nil}, l': __(nil,X:S:S), r: and(and(isQid(x37:S),isPalListKind(x37:S)),and(isPal(x38:S),isPalListKind(x38:S))), r': X:S:S) 0.003/0.003 (R28 unifies with R18 at p: [1,2], l: isNePal(__(x37:S,__(x38:S,x37:S))), lp: __(x38:S,x37:S), sig: {x37:S -> Z:S:S,x38:S -> __(X:S:S,Y:S:S)}, l': __(__(X:S:S,Y:S:S),Z:S:S), r: and(and(isQid(x37:S),isPalListKind(x37:S)),and(isPal(x38:S),isPalListKind(x38:S))), r': __(X:S:S,__(Y:S:S,Z:S:S))) 0.003/0.003 (R28 unifies with R19 at p: [1,2], l: isNePal(__(x37:S,__(x38:S,x37:S))), lp: __(x38:S,x37:S), sig: {x37:S -> X:S:S,x38:S -> nil}, l': __(nil,X:S:S), r: and(and(isQid(x37:S),isPalListKind(x37:S)),and(isPal(x38:S),isPalListKind(x38:S))), r': X:S:S) 0.003/0.003 (R28 unifies with R20 at p: [1,2], l: isNePal(__(x37:S,__(x38:S,x37:S))), lp: __(x38:S,x37:S), sig: {x37:S -> nil,x38:S -> X:S:S}, l': __(X:S:S,nil), r: and(and(isQid(x37:S),isPalListKind(x37:S)),and(isPal(x38:S),isPalListKind(x38:S))), r': X:S:S) 0.003/0.003 (R29 unifies with R28 at p: [], l: isNePal(x39:S), lp: isNePal(x39:S), sig: {x39:S -> __(I:S:S,__(P:S:S,I:S:S))}, l': isNePal(__(I:S:S,__(P:S:S,I:S:S))), r: U61(isPalListKind(x39:S),x39:S), r': and(and(isQid(I:S:S),isPalListKind(I:S:S)),and(isPal(P:S:S),isPalListKind(P:S:S)))) 0.003/0.003 (R31 unifies with R30 at p: [], l: isPal(x40:S), lp: isPal(x40:S), sig: {x40:S -> nil}, l': isPal(nil), r: U71(isPalListKind(x40:S),x40:S), r': tt) 0.003/0.003 (R32 unifies with R18 at p: [1], l: isPalListKind(__(x41:S,x42:S)), lp: __(x41:S,x42:S), sig: {x41:S -> __(X:S:S,Y:S:S),x42:S -> Z:S:S}, l': __(__(X:S:S,Y:S:S),Z:S:S), r: and(isPalListKind(x41:S),isPalListKind(x42:S)), r': __(X:S:S,__(Y:S:S,Z:S:S))) 0.003/0.003 (R32 unifies with R19 at p: [1], l: isPalListKind(__(x41:S,x42:S)), lp: __(x41:S,x42:S), sig: {x41:S -> nil,x42:S -> X:S:S}, l': __(nil,X:S:S), r: and(isPalListKind(x41:S),isPalListKind(x42:S)), r': X:S:S) 0.003/0.003 (R32 unifies with R20 at p: [1], l: isPalListKind(__(x41:S,x42:S)), lp: __(x41:S,x42:S), sig: {x41:S -> X:S:S,x42:S -> nil}, l': __(X:S:S,nil), r: and(isPalListKind(x41:S),isPalListKind(x42:S)), r': X:S:S) 0.003/0.003 0.003/0.003 -> Critical pairs info: 0.003/0.003 => Not trivial, Not overlay, NW0, N1 0.003/0.003 => Not trivial, Not overlay, NW0, N2 0.003/0.003 => Not trivial, Overlay, NW0, N3 0.003/0.003 => Not trivial, Not overlay, NW0, N4 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, N5 0.003/0.003 => Not trivial, Not overlay, NW0, N6 0.003/0.003 => Not trivial, Overlay, NW0, N7 0.003/0.003 => Not trivial, Not overlay, NW0, N8 0.003/0.003 => Not trivial, Not overlay, NW0, N9 0.003/0.003 => Not trivial, Overlay, NW0, N10 0.003/0.003 => Not trivial, Not overlay, NW0, N11 0.003/0.003 => Not trivial, Overlay, NW0, N12 0.003/0.003 => Not trivial, Not overlay, NW0, N13 0.003/0.003 => Not trivial, Not overlay, NW0, N14 0.003/0.003 => Not trivial, Overlay, NW0, N15 0.003/0.003 => Not trivial, Not overlay, NW0, N16 0.003/0.003 => Not trivial, Not overlay, NW0, N17 0.003/0.003 <__(X:S:S,__(Y:S:S,nil)),__(X:S:S,Y:S:S)> => Not trivial, Overlay, NW0, N18 0.003/0.003 <__(X:S:S,Z:S:S),__(nil,__(X: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, Overlay, NW0, N25 0.003/0.003 => Not trivial, Overlay, NW0, N26 0.003/0.003 <__(X:S:S,Z:S:S),__(X:S:S,__(nil,Z:S:S))> => Not trivial, Not overlay, NW0, N27 0.003/0.003 => Not trivial, Not overlay, NW0, N28 0.003/0.003 => 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: isList(X:S:S) 0.003/0.003 Nodes: [0,1] 0.003/0.003 Edges: [(0,1)] 0.003/0.003 ID: 0 => ('isList(X:S:S)', D0) 0.003/0.003 ID: 1 => ('U11(isPalListKind(X:S:S),X:S:S)', D1, R24, P[], S{x31:S -> X:S:S}), NR: 'U11(isPalListKind(X:S:S),X:S:S)' 0.003/0.003 t: U21(and(isPalListKind(X:S:S),isPalListKind(nil)),X:S:S,nil) 0.003/0.003 Nodes: [0] 0.003/0.003 Edges: [] 0.003/0.003 ID: 0 => ('U21(and(isPalListKind(X:S:S),isPalListKind(nil)),X:S:S,nil)', D0) 0.003/0.003 isList(X:S:S) ->* no union *<- U21(and(isPalListKind(X:S:S),isPalListKind(nil)),X:S:S,nil) 0.003/0.003 "Not joinable" 0.003/0.003 0.003/0.003 The problem is not joinable. 0.003/0.003 0.01user 0.01system 0:00.03elapsed 71%CPU (0avgtext+0avgdata 12420maxresident)k 0.003/0.003 8inputs+0outputs (0major+1306minor)pagefaults 0swaps